src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41791 01d722707a36
parent 41472 f6ab14e61604
child 41792 ff3cb0c418b7
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 10:31:48 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 10:42:29 2011 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4       tac_timeout: Time.time option,
     1.5       evals: term list,
     1.6       case_names: (string * int) list,
     1.7 -     def_table: const_table,
     1.8 +     def_tables: const_table * const_table,
     1.9       nondef_table: const_table,
    1.10       user_nondefs: term list,
    1.11       simp_table: const_table Unsynchronized.ref,
    1.12 @@ -187,15 +187,17 @@
    1.13    val case_const_names :
    1.14      Proof.context -> (typ option * bool) list -> (string * int) list
    1.15    val unfold_defs_in_term : hol_context -> term -> term
    1.16 -  val const_def_table :
    1.17 -    Proof.context -> (term * term) list -> term list -> const_table
    1.18 +  val const_def_tables :
    1.19 +    Proof.context -> (term * term) list -> term list
    1.20 +    -> const_table * const_table
    1.21    val const_nondef_table : term list -> const_table
    1.22    val const_simp_table : Proof.context -> (term * term) list -> const_table
    1.23    val const_psimp_table : Proof.context -> (term * term) list -> const_table
    1.24    val const_choice_spec_table :
    1.25      Proof.context -> (term * term) list -> const_table
    1.26    val inductive_intro_table :
    1.27 -    Proof.context -> (term * term) list -> const_table -> const_table
    1.28 +    Proof.context -> (term * term) list -> const_table * const_table
    1.29 +    -> const_table
    1.30    val ground_theorem_table : theory -> term list Inttab.table
    1.31    val ersatz_table : Proof.context -> (string * string) list
    1.32    val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
    1.33 @@ -203,10 +205,10 @@
    1.34    val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
    1.35    val optimized_quot_type_axioms :
    1.36      Proof.context -> (typ option * bool) list -> string * typ list -> term list
    1.37 -  val def_of_const : theory -> const_table -> styp -> term option
    1.38 +  val def_of_const : theory -> const_table * const_table -> styp -> term option
    1.39    val fixpoint_kind_of_rhs : term -> fixpoint_kind
    1.40    val fixpoint_kind_of_const :
    1.41 -    theory -> const_table -> string * typ -> fixpoint_kind
    1.42 +    theory -> const_table * const_table -> string * typ -> fixpoint_kind
    1.43    val is_real_inductive_pred : hol_context -> styp -> bool
    1.44    val is_constr_pattern_lhs : Proof.context -> term -> bool
    1.45    val is_constr_pattern_formula : Proof.context -> term -> bool
    1.46 @@ -256,7 +258,7 @@
    1.47     tac_timeout: Time.time option,
    1.48     evals: term list,
    1.49     case_names: (string * int) list,
    1.50 -   def_table: const_table,
    1.51 +   def_tables: const_table * const_table,
    1.52     nondef_table: const_table,
    1.53     user_nondefs: term list,
    1.54     simp_table: const_table Unsynchronized.ref,
    1.55 @@ -1376,14 +1378,19 @@
    1.56      val args = strip_comb lhs |> snd
    1.57    in fold_rev aux args (SOME rhs) end
    1.58  
    1.59 -fun def_of_const thy table (x as (s, _)) =
    1.60 -  if is_built_in_const thy [(NONE, false)] x orelse
    1.61 -     original_name s <> s then
    1.62 +fun get_def_of_const thy table (x as (s, _)) =
    1.63 +  x |> def_props_for_const thy [(NONE, false)] table |> List.last
    1.64 +    |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
    1.65 +  handle List.Empty => NONE
    1.66 +
    1.67 +fun def_of_const_ext thy (unfold_table, fallback_table) (x as (s, _)) =
    1.68 +  if is_built_in_const thy [(NONE, false)] x orelse original_name s <> s then
    1.69      NONE
    1.70 -  else
    1.71 -    x |> def_props_for_const thy [(NONE, false)] table |> List.last
    1.72 -      |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
    1.73 -    handle List.Empty => NONE
    1.74 +  else case get_def_of_const thy unfold_table x of
    1.75 +    SOME def => SOME (true, def)
    1.76 +  | NONE => get_def_of_const thy fallback_table x |> Option.map (pair false)
    1.77 +
    1.78 +val def_of_const = Option.map snd ooo def_of_const_ext
    1.79  
    1.80  fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
    1.81    | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
    1.82 @@ -1434,9 +1441,9 @@
    1.83    else fixpoint_kind_of_rhs (the (def_of_const thy table x))
    1.84    handle Option.Option => NoFp
    1.85  
    1.86 -fun is_real_inductive_pred ({thy, stds, def_table, intro_table, ...}
    1.87 +fun is_real_inductive_pred ({thy, stds, def_tables, intro_table, ...}
    1.88                              : hol_context) x =
    1.89 -  fixpoint_kind_of_const thy def_table x <> NoFp andalso
    1.90 +  fixpoint_kind_of_const thy def_tables x <> NoFp andalso
    1.91    not (null (def_props_for_const thy stds intro_table x))
    1.92  fun is_inductive_pred hol_ctxt (x as (s, _)) =
    1.93    is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
    1.94 @@ -1502,11 +1509,11 @@
    1.95    #> Object_Logic.atomize_term thy
    1.96    #> Choice_Specification.close_form
    1.97    #> HOLogic.mk_Trueprop
    1.98 -fun is_choice_spec_fun ({thy, def_table, nondef_table, choice_spec_table, ...}
    1.99 +fun is_choice_spec_fun ({thy, def_tables, nondef_table, choice_spec_table, ...}
   1.100                          : hol_context) x =
   1.101    case nondef_props_for_const thy true choice_spec_table x of
   1.102      [] => false
   1.103 -  | ts => case def_of_const thy def_table x of
   1.104 +  | ts => case def_of_const thy def_tables x of
   1.105              SOME (Const (@{const_name Eps}, _) $ _) => true
   1.106            | SOME _ => false
   1.107            | NONE =>
   1.108 @@ -1614,7 +1621,7 @@
   1.109  val def_inline_threshold_for_non_booleans = 20
   1.110  
   1.111  fun unfold_defs_in_term
   1.112 -        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_table,
   1.113 +        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_tables,
   1.114                        ground_thm_table, ersatz_table, ...}) =
   1.115    let
   1.116      fun do_term depth Ts t =
   1.117 @@ -1781,8 +1788,8 @@
   1.118                else if is_equational_fun_but_no_plain_def hol_ctxt x orelse
   1.119                        is_choice_spec_fun hol_ctxt x then
   1.120                  (Const x, ts)
   1.121 -              else case def_of_const thy def_table x of
   1.122 -                SOME def =>
   1.123 +              else case def_of_const_ext thy def_tables x of
   1.124 +                SOME (unfold, def) =>
   1.125                  if depth > unfold_max_depth then
   1.126                    raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
   1.127                                     "too many nested definitions (" ^
   1.128 @@ -1790,7 +1797,8 @@
   1.129                                     quote s)
   1.130                  else if s = @{const_name wfrec'} then
   1.131                    (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
   1.132 -                else if size_of_term def > def_inline_threshold () then
   1.133 +                else if not unfold andalso
   1.134 +                     size_of_term def > def_inline_threshold () then
   1.135                    (Const x, ts)
   1.136                  else
   1.137                    (do_term (depth + 1) Ts def, ts)
   1.138 @@ -1841,10 +1849,10 @@
   1.139    ctxt |> get |> map (pair_for_prop o subst_atomic subst)
   1.140         |> AList.group (op =) |> Symtab.make
   1.141  
   1.142 -fun const_def_table ctxt subst ts =
   1.143 -  def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst
   1.144 -  |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
   1.145 -          (map pair_for_prop ts)
   1.146 +fun const_def_tables ctxt subst ts =
   1.147 +  (def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst,
   1.148 +   fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
   1.149 +        (map pair_for_prop ts) Symtab.empty)
   1.150  
   1.151  fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
   1.152  fun const_nondef_table ts =
   1.153 @@ -1861,10 +1869,10 @@
   1.154    map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
   1.155    |> const_nondef_table
   1.156  
   1.157 -fun inductive_intro_table ctxt subst def_table =
   1.158 +fun inductive_intro_table ctxt subst def_tables =
   1.159    let val thy = ProofContext.theory_of ctxt in
   1.160      def_table_for
   1.161 -        (maps (map (unfold_mutually_inductive_preds thy def_table o prop_of)
   1.162 +        (maps (map (unfold_mutually_inductive_preds thy def_tables o prop_of)
   1.163                 o snd o snd)
   1.164           o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
   1.165                                    cat = Spec_Rules.Co_Inductive)
   1.166 @@ -2086,7 +2094,7 @@
   1.167  (* The type constraint below is a workaround for a Poly/ML crash. *)
   1.168  
   1.169  fun is_well_founded_inductive_pred
   1.170 -        (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
   1.171 +        (hol_ctxt as {thy, wfs, def_tables, wf_cache, ...} : hol_context)
   1.172          (x as (s, _)) =
   1.173    case triple_lookup (const_match thy) wfs x of
   1.174      SOME (SOME b) => b
   1.175 @@ -2095,7 +2103,7 @@
   1.176             SOME (_, wf) => wf
   1.177           | NONE =>
   1.178             let
   1.179 -             val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   1.180 +             val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
   1.181               val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
   1.182             in
   1.183               Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
   1.184 @@ -2214,13 +2222,13 @@
   1.185    | is_good_starred_linear_pred_type _ = false
   1.186  
   1.187  fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
   1.188 -                                                def_table, simp_table, ...})
   1.189 +                                                def_tables, simp_table, ...})
   1.190                                    gfp (x as (s, T)) =
   1.191    let
   1.192      val iter_T = iterator_type_for_const gfp x
   1.193      val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
   1.194      val unrolled_const = Const x' $ zero_const iter_T
   1.195 -    val def = the (def_of_const thy def_table x)
   1.196 +    val def = the (def_of_const thy def_tables x)
   1.197    in
   1.198      if is_equational_fun_but_no_plain_def hol_ctxt x' then
   1.199        unrolled_const (* already done *)
   1.200 @@ -2251,9 +2259,9 @@
   1.201        in unrolled_const end
   1.202    end
   1.203  
   1.204 -fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
   1.205 +fun raw_inductive_pred_axiom ({thy, def_tables, ...} : hol_context) x =
   1.206    let
   1.207 -    val def = the (def_of_const thy def_table x)
   1.208 +    val def = the (def_of_const thy def_tables x)
   1.209      val (outer, fp_app) = strip_abs def
   1.210      val outer_bounds = map Bound (length outer - 1 downto 0)
   1.211      val rhs =
   1.212 @@ -2277,13 +2285,13 @@
   1.213    else
   1.214      raw_inductive_pred_axiom hol_ctxt x
   1.215  
   1.216 -fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_table, simp_table,
   1.217 +fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_tables, simp_table,
   1.218                                          psimp_table, ...}) x =
   1.219    case def_props_for_const thy stds (!simp_table) x of
   1.220      [] => (case def_props_for_const thy stds psimp_table x of
   1.221               [] => (if is_inductive_pred hol_ctxt x then
   1.222                        [inductive_pred_axiom hol_ctxt x]
   1.223 -                    else case def_of_const thy def_table x of
   1.224 +                    else case def_of_const thy def_tables x of
   1.225                        SOME def =>
   1.226                        @{const Trueprop} $ HOLogic.mk_eq (Const x, def)
   1.227                        |> equationalize_term ctxt "" |> the |> single