1.1 --- a/doc-src/Nitpick/nitpick.tex Thu Feb 04 14:45:08 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Fri Feb 05 11:15:16 2010 +0100
1.3 @@ -1694,7 +1694,7 @@
1.4 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
1.5 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
1.6 \textbf{nitpick} \\[2\smallskipamount]
1.7 -{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
1.8 +{\slshape Nitpick found no counterexample.}
1.9 \postw
1.10
1.11 Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
1.12 @@ -1756,7 +1756,7 @@
1.13 \prew
1.14 \textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1.15 \textbf{nitpick} \\[2\smallskipamount]
1.16 -{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
1.17 +{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
1.18 \postw
1.19
1.20 Insertion should transform the set of elements represented by the tree in the
1.21 @@ -1766,14 +1766,14 @@
1.22 \textbf{theorem} \textit{dataset\_insort}:\kern.4em
1.23 ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
1.24 \textbf{nitpick} \\[2\smallskipamount]
1.25 -{\slshape Nitpick ran out of time after checking 5 of 8 scopes.}
1.26 +{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
1.27 \postw
1.28
1.29 -We could continue like this and sketch a complete theory of AA trees without
1.30 -performing a single proof. Once the definitions and main theorems are in place
1.31 -and have been thoroughly tested using Nitpick, we could start working on the
1.32 -proofs. Developing theories this way usually saves time, because faulty theorems
1.33 -and definitions are discovered much earlier in the process.
1.34 +We could continue like this and sketch a complete theory of AA trees. Once the
1.35 +definitions and main theorems are in place and have been thoroughly tested using
1.36 +Nitpick, we could start working on the proofs. Developing theories this way
1.37 +usually saves time, because faulty theorems and definitions are discovered much
1.38 +earlier in the process.
1.39
1.40 \section{Option Reference}
1.41 \label{option-reference}
2.1 --- a/src/HOL/IsaMakefile Thu Feb 04 14:45:08 2010 +0100
2.2 +++ b/src/HOL/IsaMakefile Fri Feb 05 11:15:16 2010 +0100
2.3 @@ -206,6 +206,7 @@
2.4 Tools/Nitpick/nitpick_mono.ML \
2.5 Tools/Nitpick/nitpick_nut.ML \
2.6 Tools/Nitpick/nitpick_peephole.ML \
2.7 + Tools/Nitpick/nitpick_preproc.ML \
2.8 Tools/Nitpick/nitpick_rep.ML \
2.9 Tools/Nitpick/nitpick_scope.ML \
2.10 Tools/Nitpick/nitpick_tests.ML \
3.1 --- a/src/HOL/Nitpick.thy Thu Feb 04 14:45:08 2010 +0100
3.2 +++ b/src/HOL/Nitpick.thy Fri Feb 05 11:15:16 2010 +0100
3.3 @@ -13,6 +13,7 @@
3.4 ("Tools/Nitpick/kodkod_sat.ML")
3.5 ("Tools/Nitpick/nitpick_util.ML")
3.6 ("Tools/Nitpick/nitpick_hol.ML")
3.7 + ("Tools/Nitpick/nitpick_preproc.ML")
3.8 ("Tools/Nitpick/nitpick_mono.ML")
3.9 ("Tools/Nitpick/nitpick_scope.ML")
3.10 ("Tools/Nitpick/nitpick_peephole.ML")
3.11 @@ -237,6 +238,7 @@
3.12 use "Tools/Nitpick/kodkod_sat.ML"
3.13 use "Tools/Nitpick/nitpick_util.ML"
3.14 use "Tools/Nitpick/nitpick_hol.ML"
3.15 +use "Tools/Nitpick/nitpick_preproc.ML"
3.16 use "Tools/Nitpick/nitpick_mono.ML"
3.17 use "Tools/Nitpick/nitpick_scope.ML"
3.18 use "Tools/Nitpick/nitpick_peephole.ML"
4.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Feb 04 14:45:08 2010 +0100
4.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Feb 05 11:15:16 2010 +0100
4.3 @@ -16,7 +16,7 @@
4.4
4.5 val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1
4.6 val def_table = Nitpick_HOL.const_def_table @{context} defs
4.7 -val ext_ctxt : Nitpick_HOL.extended_context =
4.8 +val hol_ctxt : Nitpick_HOL.hol_context =
4.9 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
4.10 stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
4.11 binary_ints = SOME false, destroy_constrs = false, specialize = false,
4.12 @@ -29,7 +29,7 @@
4.13 special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
4.14 wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
4.15 (* term -> bool *)
4.16 -val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a}
4.17 +val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt @{typ 'a}
4.18 Nitpick_Mono.Plus [] []
4.19 fun is_const t =
4.20 let val T = fastype_of t in
5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 04 14:45:08 2010 +0100
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 05 11:15:16 2010 +0100
5.3 @@ -69,6 +69,7 @@
5.4
5.5 open Nitpick_Util
5.6 open Nitpick_HOL
5.7 +open Nitpick_Preproc
5.8 open Nitpick_Mono
5.9 open Nitpick_Scope
5.10 open Nitpick_Peephole
5.11 @@ -273,7 +274,7 @@
5.12 val intro_table = inductive_intro_table ctxt def_table
5.13 val ground_thm_table = ground_theorem_table thy
5.14 val ersatz_table = ersatz_table thy
5.15 - val (ext_ctxt as {wf_cache, ...}) =
5.16 + val (hol_ctxt as {wf_cache, ...}) =
5.17 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
5.18 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
5.19 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
5.20 @@ -292,7 +293,7 @@
5.21 val _ = null (Term.add_tvars assms_t []) orelse
5.22 raise NOT_SUPPORTED "schematic type variables"
5.23 val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
5.24 - core_t) = preprocess_term ext_ctxt assms_t
5.25 + core_t) = preprocess_term hol_ctxt assms_t
5.26 val got_all_user_axioms =
5.27 got_all_mono_user_axioms andalso no_poly_user_axioms
5.28
5.29 @@ -319,9 +320,9 @@
5.30 handle TYPE (_, Ts, ts) =>
5.31 raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
5.32
5.33 - val core_u = nut_from_term ext_ctxt Eq core_t
5.34 - val def_us = map (nut_from_term ext_ctxt DefEq) def_ts
5.35 - val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts
5.36 + val core_u = nut_from_term hol_ctxt Eq core_t
5.37 + val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
5.38 + val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
5.39 val (free_names, const_names) =
5.40 fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
5.41 val (sel_names, nonsel_names) =
5.42 @@ -344,12 +345,12 @@
5.43 case triple_lookup (type_match thy) monos T of
5.44 SOME (SOME b) => b
5.45 | _ => is_type_always_monotonic T orelse
5.46 - formulas_monotonic ext_ctxt T Plus def_ts nondef_ts core_t
5.47 + formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t
5.48 fun is_deep_datatype T =
5.49 is_datatype thy T andalso
5.50 (is_word_type T orelse
5.51 exists (curry (op =) T o domain_type o type_of) sel_names)
5.52 - val all_Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
5.53 + val all_Ts = ground_types_in_terms hol_ctxt (core_t :: def_ts @ nondef_ts)
5.54 |> sort TermOrd.typ_ord
5.55 val _ = if verbose andalso binary_ints = SOME true andalso
5.56 exists (member (op =) [nat_T, int_T]) all_Ts then
5.57 @@ -522,7 +523,7 @@
5.58 val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
5.59 val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
5.60 val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
5.61 - val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk
5.62 + val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk
5.63 rel_table datatypes
5.64 val declarative_axioms = plain_axioms @ dtype_axioms
5.65 val univ_card = univ_card nat_card int_card main_j0
5.66 @@ -553,7 +554,7 @@
5.67 if loc = "Nitpick_Kodkod.check_arity" andalso
5.68 not (Typtab.is_empty ofs) then
5.69 problem_for_scope liberal
5.70 - {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
5.71 + {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
5.72 bits = bits, bisim_depth = bisim_depth,
5.73 datatypes = datatypes, ofs = Typtab.empty}
5.74 else if loc = "Nitpick.pick_them_nits_in_term.\
5.75 @@ -891,7 +892,7 @@
5.76 end
5.77
5.78 val (skipped, the_scopes) =
5.79 - all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
5.80 + all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns
5.81 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
5.82 val _ = if skipped > 0 then
5.83 print_m (fn () => "Too many scopes. Skipping " ^
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 04 14:45:08 2010 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 05 11:15:16 2010 +0100
6.3 @@ -13,7 +13,7 @@
6.4 type unrolled = styp * styp
6.5 type wf_cache = (styp * (bool * bool)) list
6.6
6.7 - type extended_context = {
6.8 + type hol_context = {
6.9 thy: theory,
6.10 ctxt: Proof.context,
6.11 max_bisim_depth: int,
6.12 @@ -46,12 +46,24 @@
6.13 wf_cache: wf_cache Unsynchronized.ref,
6.14 constr_cache: (typ * styp list) list Unsynchronized.ref}
6.15
6.16 + datatype fixpoint_kind = Lfp | Gfp | NoFp
6.17 + datatype boxability =
6.18 + InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
6.19 +
6.20 val name_sep : string
6.21 val numeral_prefix : string
6.22 + val ubfp_prefix : string
6.23 + val lbfp_prefix : string
6.24 val skolem_prefix : string
6.25 + val special_prefix : string
6.26 + val uncurry_prefix : string
6.27 val eval_prefix : string
6.28 val original_name : string -> string
6.29 val s_conj : term * term -> term
6.30 + val s_disj : term * term -> term
6.31 + val strip_any_connective : term -> term list * term
6.32 + val conjuncts_of : term -> term list
6.33 + val disjuncts_of : term -> term list
6.34 val unbit_and_unbox_type : typ -> typ
6.35 val string_for_type : Proof.context -> typ -> string
6.36 val prefix_name : string -> string -> string
6.37 @@ -76,6 +88,7 @@
6.38 val is_record_type : typ -> bool
6.39 val is_number_type : theory -> typ -> bool
6.40 val const_for_iterator_type : typ -> styp
6.41 + val strip_n_binders : int -> typ -> typ list * typ
6.42 val nth_range_type : int -> typ -> typ
6.43 val num_factors_in_type : typ -> int
6.44 val num_binder_types : typ -> int
6.45 @@ -96,15 +109,18 @@
6.46 val is_rep_fun : theory -> styp -> bool
6.47 val is_quot_abs_fun : Proof.context -> styp -> bool
6.48 val is_quot_rep_fun : Proof.context -> styp -> bool
6.49 + val mate_of_rep_fun : theory -> styp -> styp
6.50 + val is_constr_like : theory -> styp -> bool
6.51 + val is_stale_constr : theory -> styp -> bool
6.52 val is_constr : theory -> styp -> bool
6.53 - val is_stale_constr : theory -> styp -> bool
6.54 val is_sel : string -> bool
6.55 val is_sel_like_and_no_discr : string -> bool
6.56 + val box_type : hol_context -> boxability -> typ -> typ
6.57 val discr_for_constr : styp -> styp
6.58 val num_sels_for_constr_type : typ -> int
6.59 val nth_sel_name_for_constr_name : string -> int -> string
6.60 val nth_sel_for_constr : styp -> int -> styp
6.61 - val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
6.62 + val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
6.63 val sel_no_from_name : string -> int
6.64 val eta_expand : typ list -> term -> int -> term
6.65 val extensionalize : term -> term
6.66 @@ -113,19 +129,25 @@
6.67 val unregister_frac_type : string -> theory -> theory
6.68 val register_codatatype : typ -> string -> styp list -> theory -> theory
6.69 val unregister_codatatype : typ -> theory -> theory
6.70 - val datatype_constrs : extended_context -> typ -> styp list
6.71 - val boxed_datatype_constrs : extended_context -> typ -> styp list
6.72 - val num_datatype_constrs : extended_context -> typ -> int
6.73 + val datatype_constrs : hol_context -> typ -> styp list
6.74 + val boxed_datatype_constrs : hol_context -> typ -> styp list
6.75 + val num_datatype_constrs : hol_context -> typ -> int
6.76 val constr_name_for_sel_like : string -> string
6.77 - val boxed_constr_for_sel : extended_context -> styp -> styp
6.78 + val boxed_constr_for_sel : hol_context -> styp -> styp
6.79 + val discriminate_value : hol_context -> styp -> term -> term
6.80 + val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
6.81 + val construct_value : theory -> styp -> term list -> term
6.82 val card_of_type : (typ * int) list -> typ -> int
6.83 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
6.84 val bounded_exact_card_of_type :
6.85 - extended_context -> int -> int -> (typ * int) list -> typ -> int
6.86 - val is_finite_type : extended_context -> typ -> bool
6.87 + hol_context -> int -> int -> (typ * int) list -> typ -> int
6.88 + val is_finite_type : hol_context -> typ -> bool
6.89 + val special_bounds : term list -> (indexname * typ) list
6.90 + val is_funky_typedef : theory -> typ -> bool
6.91 val all_axioms_of : theory -> term list * term list * term list
6.92 val arity_of_built_in_const : bool -> styp -> int option
6.93 val is_built_in_const : bool -> styp -> bool
6.94 + val term_under_def : term -> term
6.95 val case_const_names : theory -> (string * int) list
6.96 val const_def_table : Proof.context -> term list -> const_table
6.97 val const_nondef_table : term list -> const_table
6.98 @@ -134,22 +156,33 @@
6.99 val inductive_intro_table : Proof.context -> const_table -> const_table
6.100 val ground_theorem_table : theory -> term list Inttab.table
6.101 val ersatz_table : theory -> (string * string) list
6.102 + val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
6.103 + val inverse_axioms_for_rep_fun : theory -> styp -> term list
6.104 + val optimized_typedef_axioms : theory -> string * typ list -> term list
6.105 + val optimized_quot_type_axioms : theory -> string * typ list -> term list
6.106 val def_of_const : theory -> const_table -> styp -> term option
6.107 - val is_inductive_pred : extended_context -> styp -> bool
6.108 + val fixpoint_kind_of_const :
6.109 + theory -> const_table -> string * typ -> fixpoint_kind
6.110 + val is_inductive_pred : hol_context -> styp -> bool
6.111 + val is_equational_fun : hol_context -> styp -> bool
6.112 val is_constr_pattern_lhs : theory -> term -> bool
6.113 val is_constr_pattern_formula : theory -> term -> bool
6.114 + val unfold_defs_in_term : hol_context -> term -> term
6.115 + val codatatype_bisim_axioms : hol_context -> typ -> term list
6.116 + val is_well_founded_inductive_pred : hol_context -> styp -> bool
6.117 + val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
6.118 + val equational_fun_axioms : hol_context -> styp -> term list
6.119 + val is_equational_fun_surely_complete : hol_context -> styp -> bool
6.120 val merge_type_vars_in_terms : term list -> term list
6.121 - val ground_types_in_type : extended_context -> typ -> typ list
6.122 - val ground_types_in_terms : extended_context -> term list -> typ list
6.123 + val ground_types_in_type : hol_context -> typ -> typ list
6.124 + val ground_types_in_terms : hol_context -> term list -> typ list
6.125 val format_type : int list -> int list -> typ -> typ
6.126 val format_term_type :
6.127 theory -> const_table -> (term option * int list) list -> term -> typ
6.128 val user_friendly_const :
6.129 - extended_context -> string * string -> (term option * int list) list
6.130 + hol_context -> string * string -> (term option * int list) list
6.131 -> styp -> term * typ
6.132 val assign_operator_for_const : styp -> string
6.133 - val preprocess_term :
6.134 - extended_context -> term -> ((term list * term list) * (bool * bool)) * term
6.135 end;
6.136
6.137 structure Nitpick_HOL : NITPICK_HOL =
6.138 @@ -162,7 +195,7 @@
6.139 type unrolled = styp * styp
6.140 type wf_cache = (styp * (bool * bool)) list
6.141
6.142 -type extended_context = {
6.143 +type hol_context = {
6.144 thy: theory,
6.145 ctxt: Proof.context,
6.146 max_bisim_depth: int,
6.147 @@ -195,6 +228,10 @@
6.148 wf_cache: wf_cache Unsynchronized.ref,
6.149 constr_cache: (typ * styp list) list Unsynchronized.ref}
6.150
6.151 +datatype fixpoint_kind = Lfp | Gfp | NoFp
6.152 +datatype boxability =
6.153 + InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
6.154 +
6.155 structure Data = Theory_Data(
6.156 type T = {frac_types: (string * (string * string) list) list,
6.157 codatatypes: (string * (string * styp list)) list}
6.158 @@ -222,20 +259,11 @@
6.159 val special_prefix = nitpick_prefix ^ "sp"
6.160 val uncurry_prefix = nitpick_prefix ^ "unc"
6.161 val eval_prefix = nitpick_prefix ^ "eval"
6.162 -val bound_var_prefix = "b"
6.163 -val cong_var_prefix = "c"
6.164 val iter_var_prefix = "i"
6.165 -val val_var_prefix = nitpick_prefix ^ "v"
6.166 val arg_var_prefix = "x"
6.167
6.168 (* int -> string *)
6.169 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
6.170 -fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
6.171 -(* int -> int -> string *)
6.172 -fun skolem_prefix_for k j =
6.173 - skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
6.174 -fun uncurry_prefix_for k j =
6.175 - uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
6.176
6.177 (* string -> string * string *)
6.178 val strip_first_name_sep =
6.179 @@ -260,9 +288,6 @@
6.180 | s_disj (t1, t2) =
6.181 if t1 = @{const True} orelse t2 = @{const True} then @{const True}
6.182 else HOLogic.mk_disj (t1, t2)
6.183 -(* term -> term -> term *)
6.184 -fun mk_exists v t =
6.185 - HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
6.186
6.187 (* term -> term -> term list *)
6.188 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
6.189 @@ -276,8 +301,8 @@
6.190 ([t], @{const Not})
6.191 | strip_any_connective t = ([t], @{const Not})
6.192 (* term -> term list *)
6.193 -val conjuncts = strip_connective @{const "op &"}
6.194 -val disjuncts = strip_connective @{const "op |"}
6.195 +val conjuncts_of = strip_connective @{const "op &"}
6.196 +val disjuncts_of = strip_connective @{const "op |"}
6.197
6.198 (* When you add constants to these lists, make sure to handle them in
6.199 "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
6.200 @@ -373,8 +398,6 @@
6.201 fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
6.202 (* string -> term -> term *)
6.203 val prefix_abs_vars = Term.map_abs_vars o prefix_name
6.204 -(* term -> term *)
6.205 -val shorten_abs_vars = Term.map_abs_vars shortest_name
6.206 (* string -> string *)
6.207 fun short_name s =
6.208 case space_explode name_sep s of
6.209 @@ -441,7 +464,7 @@
6.210 | const_for_iterator_type T =
6.211 raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
6.212
6.213 -(* int -> typ -> typ * typ *)
6.214 +(* int -> typ -> typ list * typ *)
6.215 fun strip_n_binders 0 T = ([], T)
6.216 | strip_n_binders n (Type ("fun", [T1, T2])) =
6.217 strip_n_binders (n - 1) T2 |>> cons T1
6.218 @@ -552,7 +575,7 @@
6.219 val is_real_datatype = is_some oo Datatype.get_info
6.220 (* theory -> typ -> bool *)
6.221 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
6.222 - | is_quot_type _ (Type ("FSet.fset", _)) = true (* FIXME *)
6.223 + | is_quot_type _ (Type ("FSet.fset", _)) = true
6.224 | is_quot_type _ _ = false
6.225 fun is_codatatype thy (T as Type (s, _)) =
6.226 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
6.227 @@ -619,11 +642,11 @@
6.228 | NONE => false)
6.229 | is_rep_fun _ _ = false
6.230 (* Proof.context -> styp -> bool *)
6.231 -fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *)
6.232 - | is_quot_abs_fun _ ("FSet.abs_fset", _) = true (* FIXME *)
6.233 +fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true
6.234 + | is_quot_abs_fun _ ("FSet.abs_fset", _) = true
6.235 | is_quot_abs_fun _ _ = false
6.236 -fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *)
6.237 - | is_quot_rep_fun _ ("FSet.rep_fset", _) = true (* FIXME *)
6.238 +fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true
6.239 + | is_quot_rep_fun _ ("FSet.rep_fset", _) = true
6.240 | is_quot_rep_fun _ _ = false
6.241
6.242 (* theory -> styp -> styp *)
6.243 @@ -682,9 +705,6 @@
6.244 String.isPrefix sel_prefix
6.245 orf (member (op =) [@{const_name fst}, @{const_name snd}])
6.246
6.247 -datatype boxability =
6.248 - InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
6.249 -
6.250 (* boxability -> boxability *)
6.251 fun in_fun_lhs_for InConstr = InSel
6.252 | in_fun_lhs_for _ = InFunLHS
6.253 @@ -693,8 +713,8 @@
6.254 | in_fun_rhs_for InFunRHS1 = InFunRHS2
6.255 | in_fun_rhs_for _ = InFunRHS1
6.256
6.257 -(* extended_context -> boxability -> typ -> bool *)
6.258 -fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
6.259 +(* hol_context -> boxability -> typ -> bool *)
6.260 +fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
6.261 case T of
6.262 Type ("fun", _) =>
6.263 (boxy = InPair orelse boxy = InFunLHS) andalso
6.264 @@ -702,31 +722,31 @@
6.265 | Type ("*", Ts) =>
6.266 boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
6.267 ((boxy = InExpr orelse boxy = InFunLHS) andalso
6.268 - exists (is_boxing_worth_it ext_ctxt InPair)
6.269 - (map (box_type ext_ctxt InPair) Ts))
6.270 + exists (is_boxing_worth_it hol_ctxt InPair)
6.271 + (map (box_type hol_ctxt InPair) Ts))
6.272 | _ => false
6.273 -(* extended_context -> boxability -> string * typ list -> string *)
6.274 -and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
6.275 +(* hol_context -> boxability -> string * typ list -> string *)
6.276 +and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
6.277 case triple_lookup (type_match thy) boxes (Type z) of
6.278 SOME (SOME box_me) => box_me
6.279 - | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
6.280 -(* extended_context -> boxability -> typ -> typ *)
6.281 -and box_type ext_ctxt boxy T =
6.282 + | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
6.283 +(* hol_context -> boxability -> typ -> typ *)
6.284 +and box_type hol_ctxt boxy T =
6.285 case T of
6.286 Type (z as ("fun", [T1, T2])) =>
6.287 if boxy <> InConstr andalso boxy <> InSel andalso
6.288 - should_box_type ext_ctxt boxy z then
6.289 + should_box_type hol_ctxt boxy z then
6.290 Type (@{type_name fun_box},
6.291 - [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
6.292 + [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
6.293 else
6.294 - box_type ext_ctxt (in_fun_lhs_for boxy) T1
6.295 - --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
6.296 + box_type hol_ctxt (in_fun_lhs_for boxy) T1
6.297 + --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
6.298 | Type (z as ("*", Ts)) =>
6.299 if boxy <> InConstr andalso boxy <> InSel
6.300 - andalso should_box_type ext_ctxt boxy z then
6.301 - Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
6.302 + andalso should_box_type hol_ctxt boxy z then
6.303 + Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
6.304 else
6.305 - Type ("*", map (box_type ext_ctxt
6.306 + Type ("*", map (box_type hol_ctxt
6.307 (if boxy = InConstr orelse boxy = InSel then boxy
6.308 else InPair)) Ts)
6.309 | _ => T
6.310 @@ -747,9 +767,9 @@
6.311 | nth_sel_for_constr (s, T) n =
6.312 (nth_sel_name_for_constr_name s n,
6.313 body_type T --> nth (maybe_curried_binder_types T) n)
6.314 -(* extended_context -> styp -> int -> styp *)
6.315 -fun boxed_nth_sel_for_constr ext_ctxt =
6.316 - apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr
6.317 +(* hol_context -> styp -> int -> styp *)
6.318 +fun boxed_nth_sel_for_constr hol_ctxt =
6.319 + apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr
6.320
6.321 (* string -> int *)
6.322 fun sel_no_from_name s =
6.323 @@ -791,8 +811,8 @@
6.324 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
6.325 fun suc_const T = Const (@{const_name Suc}, T --> T)
6.326
6.327 -(* extended_context -> typ -> styp list *)
6.328 -fun uncached_datatype_constrs ({thy, stds, ...} : extended_context)
6.329 +(* hol_context -> typ -> styp list *)
6.330 +fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
6.331 (T as Type (s, Ts)) =
6.332 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
6.333 SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
6.334 @@ -829,49 +849,49 @@
6.335 else
6.336 [])
6.337 | uncached_datatype_constrs _ _ = []
6.338 -(* extended_context -> typ -> styp list *)
6.339 -fun datatype_constrs (ext_ctxt as {constr_cache, ...}) T =
6.340 +(* hol_context -> typ -> styp list *)
6.341 +fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
6.342 case AList.lookup (op =) (!constr_cache) T of
6.343 SOME xs => xs
6.344 | NONE =>
6.345 - let val xs = uncached_datatype_constrs ext_ctxt T in
6.346 + let val xs = uncached_datatype_constrs hol_ctxt T in
6.347 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
6.348 end
6.349 -fun boxed_datatype_constrs ext_ctxt =
6.350 - map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
6.351 -(* extended_context -> typ -> int *)
6.352 +fun boxed_datatype_constrs hol_ctxt =
6.353 + map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
6.354 +(* hol_context -> typ -> int *)
6.355 val num_datatype_constrs = length oo datatype_constrs
6.356
6.357 (* string -> string *)
6.358 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
6.359 | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
6.360 | constr_name_for_sel_like s' = original_name s'
6.361 -(* extended_context -> styp -> styp *)
6.362 -fun boxed_constr_for_sel ext_ctxt (s', T') =
6.363 +(* hol_context -> styp -> styp *)
6.364 +fun boxed_constr_for_sel hol_ctxt (s', T') =
6.365 let val s = constr_name_for_sel_like s' in
6.366 - AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
6.367 + AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s
6.368 |> the |> pair s
6.369 end
6.370
6.371 -(* extended_context -> styp -> term *)
6.372 -fun discr_term_for_constr ext_ctxt (x as (s, T)) =
6.373 +(* hol_context -> styp -> term *)
6.374 +fun discr_term_for_constr hol_ctxt (x as (s, T)) =
6.375 let val dataT = body_type T in
6.376 if s = @{const_name Suc} then
6.377 Abs (Name.uu, dataT,
6.378 @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
6.379 - else if num_datatype_constrs ext_ctxt dataT >= 2 then
6.380 + else if num_datatype_constrs hol_ctxt dataT >= 2 then
6.381 Const (discr_for_constr x)
6.382 else
6.383 Abs (Name.uu, dataT, @{const True})
6.384 end
6.385 -(* extended_context -> styp -> term -> term *)
6.386 -fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
6.387 +(* hol_context -> styp -> term -> term *)
6.388 +fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t =
6.389 case strip_comb t of
6.390 (Const x', args) =>
6.391 if x = x' then @{const True}
6.392 else if is_constr_like thy x' then @{const False}
6.393 - else betapply (discr_term_for_constr ext_ctxt x, t)
6.394 - | _ => betapply (discr_term_for_constr ext_ctxt x, t)
6.395 + else betapply (discr_term_for_constr hol_ctxt x, t)
6.396 + | _ => betapply (discr_term_for_constr hol_ctxt x, t)
6.397
6.398 (* styp -> term -> term *)
6.399 fun nth_arg_sel_term_for_constr (x as (s, T)) n =
6.400 @@ -920,26 +940,6 @@
6.401 | _ => list_comb (Const x, args)
6.402 end
6.403
6.404 -(* extended_context -> typ -> term -> term *)
6.405 -fun constr_expand (ext_ctxt as {thy, ...}) T t =
6.406 - (case head_of t of
6.407 - Const x => if is_constr_like thy x then t else raise SAME ()
6.408 - | _ => raise SAME ())
6.409 - handle SAME () =>
6.410 - let
6.411 - val x' as (_, T') =
6.412 - if is_pair_type T then
6.413 - let val (T1, T2) = HOLogic.dest_prodT T in
6.414 - (@{const_name Pair}, T1 --> T2 --> T)
6.415 - end
6.416 - else
6.417 - datatype_constrs ext_ctxt T |> hd
6.418 - val arg_Ts = binder_types T'
6.419 - in
6.420 - list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
6.421 - (index_seq 0 (length arg_Ts)) arg_Ts)
6.422 - end
6.423 -
6.424 (* (typ * int) list -> typ -> int *)
6.425 fun card_of_type assigns (Type ("fun", [T1, T2])) =
6.426 reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
6.427 @@ -975,8 +975,8 @@
6.428 card_of_type assigns T
6.429 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
6.430 default_card)
6.431 -(* extended_context -> int -> (typ * int) list -> typ -> int *)
6.432 -fun bounded_exact_card_of_type ext_ctxt max default_card assigns T =
6.433 +(* hol_context -> int -> (typ * int) list -> typ -> int *)
6.434 +fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
6.435 let
6.436 (* typ list -> typ -> int *)
6.437 fun aux avoid T =
6.438 @@ -1006,13 +1006,13 @@
6.439 | @{typ bool} => 2
6.440 | @{typ unit} => 1
6.441 | Type _ =>
6.442 - (case datatype_constrs ext_ctxt T of
6.443 + (case datatype_constrs hol_ctxt T of
6.444 [] => if is_integer_type T orelse is_bit_type T then 0
6.445 else raise SAME ()
6.446 | constrs =>
6.447 let
6.448 val constr_cards =
6.449 - datatype_constrs ext_ctxt T
6.450 + datatype_constrs hol_ctxt T
6.451 |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
6.452 o snd)
6.453 in
6.454 @@ -1024,9 +1024,9 @@
6.455 AList.lookup (op =) assigns T |> the_default default_card
6.456 in Int.min (max, aux [] T) end
6.457
6.458 -(* extended_context -> typ -> bool *)
6.459 -fun is_finite_type ext_ctxt =
6.460 - not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 []
6.461 +(* hol_context -> typ -> bool *)
6.462 +fun is_finite_type hol_ctxt =
6.463 + not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
6.464
6.465 (* term -> bool *)
6.466 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
6.467 @@ -1052,7 +1052,7 @@
6.468 member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
6.469 @{type_name int}] s orelse
6.470 is_frac_type thy (Type (s, []))
6.471 -(* theory -> term -> bool *)
6.472 +(* theory -> typ -> bool *)
6.473 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
6.474 | is_funky_typedef _ _ = false
6.475 (* term -> bool *)
6.476 @@ -1199,8 +1199,6 @@
6.477 |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
6.478 handle List.Empty => NONE
6.479
6.480 -datatype fixpoint_kind = Lfp | Gfp | NoFp
6.481 -
6.482 (* term -> fixpoint_kind *)
6.483 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
6.484 | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
6.485 @@ -1299,35 +1297,6 @@
6.486 Unsynchronized.change simp_table
6.487 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
6.488
6.489 -(* Similar to "Refute.specialize_type" but returns all matches rather than only
6.490 - the first (preorder) match. *)
6.491 -(* theory -> styp -> term -> term list *)
6.492 -fun multi_specialize_type thy slack (x as (s, T)) t =
6.493 - let
6.494 - (* term -> (typ * term) list -> (typ * term) list *)
6.495 - fun aux (Const (s', T')) ys =
6.496 - if s = s' then
6.497 - ys |> (if AList.defined (op =) ys T' then
6.498 - I
6.499 - else
6.500 - cons (T', Refute.monomorphic_term
6.501 - (Sign.typ_match thy (T', T) Vartab.empty) t)
6.502 - handle Type.TYPE_MATCH => I
6.503 - | Refute.REFUTE _ =>
6.504 - if slack then
6.505 - I
6.506 - else
6.507 - raise NOT_SUPPORTED ("too much polymorphism in \
6.508 - \axiom involving " ^ quote s))
6.509 - else
6.510 - ys
6.511 - | aux _ ys = ys
6.512 - in map snd (fold_aterms aux t []) end
6.513 -
6.514 -(* theory -> bool -> const_table -> styp -> term list *)
6.515 -fun nondef_props_for_const thy slack table (x as (s, _)) =
6.516 - these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
6.517 -
6.518 (* theory -> styp -> term list *)
6.519 fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
6.520 let val abs_T = domain_type T in
6.521 @@ -1336,7 +1305,7 @@
6.522 |> pairself (Refute.specialize_type thy x o prop_of o the)
6.523 ||> single |> op ::
6.524 end
6.525 -(* theory -> styp list -> term list *)
6.526 +(* theory -> string * typ list -> term list *)
6.527 fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
6.528 let val abs_T = Type abs_z in
6.529 if is_univ_typedef thy abs_T then
6.530 @@ -1392,15 +1361,15 @@
6.531 list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
6.532 (index_seq 0 (length arg_Ts)) arg_Ts)
6.533 end
6.534 -(* extended_context -> typ -> int * styp -> term -> term *)
6.535 -fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
6.536 +(* hol_context -> typ -> int * styp -> term -> term *)
6.537 +fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t =
6.538 Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
6.539 - $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
6.540 + $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x)
6.541 $ res_t
6.542 -(* extended_context -> typ -> typ -> term *)
6.543 -fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
6.544 +(* hol_context -> typ -> typ -> term *)
6.545 +fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
6.546 let
6.547 - val xs = datatype_constrs ext_ctxt dataT
6.548 + val xs = datatype_constrs hol_ctxt dataT
6.549 val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
6.550 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
6.551 in
6.552 @@ -1409,19 +1378,19 @@
6.553 val (xs'', x) = split_last xs'
6.554 in
6.555 constr_case_body thy (1, x)
6.556 - |> fold_rev (add_constr_case ext_ctxt res_T)
6.557 + |> fold_rev (add_constr_case hol_ctxt res_T)
6.558 (length xs' downto 2 ~~ xs'')
6.559 end
6.560 else
6.561 Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
6.562 - |> fold_rev (add_constr_case ext_ctxt res_T)
6.563 + |> fold_rev (add_constr_case hol_ctxt res_T)
6.564 (length xs' downto 1 ~~ xs'))
6.565 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
6.566 end
6.567
6.568 -(* extended_context -> string -> typ -> typ -> term -> term *)
6.569 -fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
6.570 - let val constr_x = hd (datatype_constrs ext_ctxt rec_T) in
6.571 +(* hol_context -> string -> typ -> typ -> term -> term *)
6.572 +fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t =
6.573 + let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
6.574 case no_of_record_field thy s rec_T of
6.575 ~1 => (case rec_T of
6.576 Type (_, Ts as _ :: _) =>
6.577 @@ -1430,16 +1399,16 @@
6.578 val j = num_record_fields thy rec_T - 1
6.579 in
6.580 select_nth_constr_arg thy constr_x t j res_T
6.581 - |> optimized_record_get ext_ctxt s rec_T' res_T
6.582 + |> optimized_record_get hol_ctxt s rec_T' res_T
6.583 end
6.584 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
6.585 []))
6.586 | j => select_nth_constr_arg thy constr_x t j res_T
6.587 end
6.588 -(* extended_context -> string -> typ -> term -> term -> term *)
6.589 -fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
6.590 +(* hol_context -> string -> typ -> term -> term -> term *)
6.591 +fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t =
6.592 let
6.593 - val constr_x as (_, constr_T) = hd (datatype_constrs ext_ctxt rec_T)
6.594 + val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
6.595 val Ts = binder_types constr_T
6.596 val n = length Ts
6.597 val special_j = no_of_record_field thy s rec_T
6.598 @@ -1450,7 +1419,7 @@
6.599 if j = special_j then
6.600 betapply (fun_t, t)
6.601 else if j = n - 1 andalso special_j = ~1 then
6.602 - optimized_record_update ext_ctxt s
6.603 + optimized_record_update hol_ctxt s
6.604 (rec_T |> dest_Type |> snd |> List.last) fun_t t
6.605 else
6.606 t
6.607 @@ -1473,19 +1442,19 @@
6.608 fixpoint_kind_of_rhs (the (def_of_const thy table x))
6.609 handle Option.Option => NoFp
6.610
6.611 -(* extended_context -> styp -> bool *)
6.612 +(* hol_context -> styp -> bool *)
6.613 fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
6.614 - : extended_context) x =
6.615 + : hol_context) x =
6.616 not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
6.617 fixpoint_kind_of_const thy def_table x <> NoFp
6.618 fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
6.619 - : extended_context) x =
6.620 + : hol_context) x =
6.621 exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
6.622 [!simp_table, psimp_table]
6.623 -fun is_inductive_pred ext_ctxt =
6.624 - is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
6.625 -fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
6.626 - (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
6.627 +fun is_inductive_pred hol_ctxt =
6.628 + is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
6.629 +fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
6.630 + (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
6.631 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
6.632 andf (not o has_trivial_definition thy def_table)
6.633
6.634 @@ -1522,11 +1491,11 @@
6.635 SOME t' => is_constr_pattern_lhs thy t'
6.636 | NONE => false
6.637
6.638 +(* Prevents divergence in case of cyclic or infinite definition dependencies. *)
6.639 val unfold_max_depth = 255
6.640 -val axioms_max_depth = 255
6.641
6.642 -(* extended_context -> term -> term *)
6.643 -fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
6.644 +(* hol_context -> term -> term *)
6.645 +fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs,
6.646 case_names, def_table, ground_thm_table,
6.647 ersatz_table, ...}) =
6.648 let
6.649 @@ -1600,7 +1569,7 @@
6.650 val (dataT, res_T) = nth_range_type n T
6.651 |> pairf domain_type range_type
6.652 in
6.653 - (optimized_case_def ext_ctxt dataT res_T
6.654 + (optimized_case_def hol_ctxt dataT res_T
6.655 |> do_term (depth + 1) Ts, ts)
6.656 end
6.657 | _ =>
6.658 @@ -1628,11 +1597,11 @@
6.659 else if is_record_get thy x then
6.660 case length ts of
6.661 0 => (do_term depth Ts (eta_expand Ts t 1), [])
6.662 - | _ => (optimized_record_get ext_ctxt s (domain_type T)
6.663 + | _ => (optimized_record_get hol_ctxt s (domain_type T)
6.664 (range_type T) (do_term depth Ts (hd ts)), tl ts)
6.665 else if is_record_update thy x then
6.666 case length ts of
6.667 - 2 => (optimized_record_update ext_ctxt
6.668 + 2 => (optimized_record_update hol_ctxt
6.669 (unsuffix Record.updateN s) (nth_range_type 2 T)
6.670 (do_term depth Ts (hd ts))
6.671 (do_term depth Ts (nth ts 1)), [])
6.672 @@ -1645,7 +1614,7 @@
6.673 else
6.674 (Const x, ts)
6.675 end
6.676 - else if is_equational_fun ext_ctxt x then
6.677 + else if is_equational_fun hol_ctxt x then
6.678 (Const x, ts)
6.679 else case def_of_const thy def_table x of
6.680 SOME def =>
6.681 @@ -1662,10 +1631,10 @@
6.682 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
6.683 in do_term 0 [] end
6.684
6.685 -(* extended_context -> typ -> term list *)
6.686 -fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
6.687 +(* hol_context -> typ -> term list *)
6.688 +fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T =
6.689 let
6.690 - val xs = datatype_constrs ext_ctxt T
6.691 + val xs = datatype_constrs hol_ctxt T
6.692 val set_T = T --> bool_T
6.693 val iter_T = @{typ bisim_iterator}
6.694 val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
6.695 @@ -1688,14 +1657,14 @@
6.696 let
6.697 val arg_Ts = binder_types T
6.698 val core_t =
6.699 - discriminate_value ext_ctxt x y_var ::
6.700 + discriminate_value hol_ctxt x y_var ::
6.701 map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
6.702 |> foldr1 s_conj
6.703 in List.foldr absdummy core_t arg_Ts end
6.704 in
6.705 [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
6.706 $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
6.707 - $ (betapplys (optimized_case_def ext_ctxt T bool_T,
6.708 + $ (betapplys (optimized_case_def hol_ctxt T bool_T,
6.709 map case_func xs @ [x_var]))),
6.710 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
6.711 $ (Const (@{const_name insert}, T --> set_T --> set_T)
6.712 @@ -1754,10 +1723,10 @@
6.713 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
6.714 ScnpReconstruct.sizechange_tac]
6.715
6.716 -(* extended_context -> const_table -> styp -> bool *)
6.717 +(* hol_context -> const_table -> styp -> bool *)
6.718 fun uncached_is_well_founded_inductive_pred
6.719 ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
6.720 - : extended_context) (x as (_, T)) =
6.721 + : hol_context) (x as (_, T)) =
6.722 case def_props_for_const thy fast_descrs intro_table x of
6.723 [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
6.724 [Const x])
6.725 @@ -1797,11 +1766,11 @@
6.726 handle List.Empty => false
6.727 | NO_TRIPLE () => false
6.728
6.729 -(* The type constraint below is a workaround for a Poly/ML bug. *)
6.730 +(* The type constraint below is a workaround for a Poly/ML crash. *)
6.731
6.732 -(* extended_context -> styp -> bool *)
6.733 +(* hol_context -> styp -> bool *)
6.734 fun is_well_founded_inductive_pred
6.735 - (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context)
6.736 + (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
6.737 (x as (s, _)) =
6.738 case triple_lookup (const_match thy) wfs x of
6.739 SOME (SOME b) => b
6.740 @@ -1811,7 +1780,7 @@
6.741 | NONE =>
6.742 let
6.743 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
6.744 - val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
6.745 + val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
6.746 in
6.747 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
6.748 end
6.749 @@ -1842,14 +1811,14 @@
6.750 | do_disjunct j t =
6.751 case num_occs_of_bound_in_term j t of
6.752 0 => true
6.753 - | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t)
6.754 + | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
6.755 | _ => false
6.756 (* term -> bool *)
6.757 fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
6.758 let val (xs, body) = strip_abs t2 in
6.759 case length xs of
6.760 1 => false
6.761 - | n => forall (do_disjunct (n - 1)) (disjuncts body)
6.762 + | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
6.763 end
6.764 | do_lfp_def _ = false
6.765 in do_lfp_def o strip_abs_body end
6.766 @@ -1887,7 +1856,7 @@
6.767 end
6.768 val (nonrecs, recs) =
6.769 List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
6.770 - (disjuncts body)
6.771 + (disjuncts_of body)
6.772 val base_body = nonrecs |> List.foldl s_disj @{const False}
6.773 val step_body = recs |> map (repair_rec j)
6.774 |> List.foldl s_disj @{const False}
6.775 @@ -1901,8 +1870,8 @@
6.776 raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
6.777 in aux end
6.778
6.779 -(* extended_context -> styp -> term -> term *)
6.780 -fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T))
6.781 +(* hol_context -> styp -> term -> term *)
6.782 +fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T))
6.783 def =
6.784 let
6.785 val j = maxidx_of_term def + 1
6.786 @@ -1933,11 +1902,11 @@
6.787 $ list_comb (Const step_x, outer_bounds)))
6.788 $ list_comb (Const base_x, outer_bounds)
6.789 |> ap_curry tuple_arg_Ts tuple_T bool_T)
6.790 - |> unfold_defs_in_term ext_ctxt
6.791 + |> unfold_defs_in_term hol_ctxt
6.792 end
6.793
6.794 -(* extended_context -> bool -> styp -> term *)
6.795 -fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds,
6.796 +(* hol_context -> bool -> styp -> term *)
6.797 +fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
6.798 def_table, simp_table, ...})
6.799 gfp (x as (s, T)) =
6.800 let
6.801 @@ -1946,11 +1915,11 @@
6.802 val unrolled_const = Const x' $ zero_const iter_T
6.803 val def = the (def_of_const thy def_table x)
6.804 in
6.805 - if is_equational_fun ext_ctxt x' then
6.806 + if is_equational_fun hol_ctxt x' then
6.807 unrolled_const (* already done *)
6.808 else if not gfp andalso is_linear_inductive_pred_def def andalso
6.809 star_linear_preds then
6.810 - starred_linear_pred_const ext_ctxt x def
6.811 + starred_linear_pred_const hol_ctxt x def
6.812 else
6.813 let
6.814 val j = maxidx_of_term def + 1
6.815 @@ -1973,8 +1942,8 @@
6.816 in unrolled_const end
6.817 end
6.818
6.819 -(* extended_context -> styp -> term *)
6.820 -fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x =
6.821 +(* hol_context -> styp -> term *)
6.822 +fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
6.823 let
6.824 val def = the (def_of_const thy def_table x)
6.825 val (outer, fp_app) = strip_abs def
6.826 @@ -1992,24 +1961,29 @@
6.827 HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
6.828 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
6.829 end
6.830 -fun inductive_pred_axiom ext_ctxt (x as (s, T)) =
6.831 +fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
6.832 if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
6.833 let val x' = (after_name_sep s, T) in
6.834 - raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)]
6.835 + raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
6.836 end
6.837 else
6.838 - raw_inductive_pred_axiom ext_ctxt x
6.839 + raw_inductive_pred_axiom hol_ctxt x
6.840
6.841 -(* extended_context -> styp -> term list *)
6.842 -fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
6.843 +(* hol_context -> styp -> term list *)
6.844 +fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table,
6.845 psimp_table, ...}) (x as (s, _)) =
6.846 case def_props_for_const thy fast_descrs (!simp_table) x of
6.847 [] => (case def_props_for_const thy fast_descrs psimp_table x of
6.848 - [] => [inductive_pred_axiom ext_ctxt x]
6.849 + [] => [inductive_pred_axiom hol_ctxt x]
6.850 | psimps => psimps)
6.851 | simps => simps
6.852 -
6.853 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
6.854 +(* hol_context -> styp -> bool *)
6.855 +fun is_equational_fun_surely_complete hol_ctxt x =
6.856 + case raw_equational_fun_axioms hol_ctxt x of
6.857 + [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
6.858 + strip_comb t1 |> snd |> forall is_Var
6.859 + | _ => false
6.860
6.861 (* term list -> term list *)
6.862 fun merge_type_vars_in_terms ts =
6.863 @@ -2028,1261 +2002,27 @@
6.864 | coalesce T = T
6.865 in map (map_types (map_atyps coalesce)) ts end
6.866
6.867 -(* extended_context -> typ -> typ list -> typ list *)
6.868 -fun add_ground_types ext_ctxt T accum =
6.869 +(* hol_context -> typ -> typ list -> typ list *)
6.870 +fun add_ground_types hol_ctxt T accum =
6.871 case T of
6.872 - Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum
6.873 - | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
6.874 - | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
6.875 + Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum
6.876 + | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
6.877 + | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
6.878 | Type (_, Ts) =>
6.879 if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
6.880 accum
6.881 else
6.882 T :: accum
6.883 - |> fold (add_ground_types ext_ctxt)
6.884 - (case boxed_datatype_constrs ext_ctxt T of
6.885 + |> fold (add_ground_types hol_ctxt)
6.886 + (case boxed_datatype_constrs hol_ctxt T of
6.887 [] => Ts
6.888 | xs => map snd xs)
6.889 | _ => insert (op =) T accum
6.890 -(* extended_context -> typ -> typ list *)
6.891 -fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T []
6.892 -(* extended_context -> term list -> typ list *)
6.893 -fun ground_types_in_terms ext_ctxt ts =
6.894 - fold (fold_types (add_ground_types ext_ctxt)) ts []
6.895 -
6.896 -(* typ list -> int -> term -> bool *)
6.897 -fun has_heavy_bounds_or_vars Ts level t =
6.898 - let
6.899 - (* typ list -> bool *)
6.900 - fun aux [] = false
6.901 - | aux [T] = is_fun_type T orelse is_pair_type T
6.902 - | aux _ = true
6.903 - in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
6.904 -
6.905 -(* typ list -> int -> int -> int -> term -> term *)
6.906 -fun fresh_value_var Ts k n j t =
6.907 - Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
6.908 -
6.909 -(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
6.910 - -> term * term list *)
6.911 -fun pull_out_constr_comb thy Ts relax k level t args seen =
6.912 - let val t_comb = list_comb (t, args) in
6.913 - case t of
6.914 - Const x =>
6.915 - if not relax andalso is_constr thy x andalso
6.916 - not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
6.917 - has_heavy_bounds_or_vars Ts level t_comb andalso
6.918 - not (loose_bvar (t_comb, level)) then
6.919 - let
6.920 - val (j, seen) = case find_index (curry (op =) t_comb) seen of
6.921 - ~1 => (0, t_comb :: seen)
6.922 - | j => (j, seen)
6.923 - in (fresh_value_var Ts k (length seen) j t_comb, seen) end
6.924 - else
6.925 - (t_comb, seen)
6.926 - | _ => (t_comb, seen)
6.927 - end
6.928 -
6.929 -(* (term -> term) -> typ list -> int -> term list -> term list *)
6.930 -fun equations_for_pulled_out_constrs mk_eq Ts k seen =
6.931 - let val n = length seen in
6.932 - map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
6.933 - (index_seq 0 n) seen
6.934 - end
6.935 -
6.936 -(* theory -> bool -> term -> term *)
6.937 -fun pull_out_universal_constrs thy def t =
6.938 - let
6.939 - val k = maxidx_of_term t + 1
6.940 - (* typ list -> bool -> term -> term list -> term list -> term * term list *)
6.941 - fun do_term Ts def t args seen =
6.942 - case t of
6.943 - (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
6.944 - do_eq_or_imp Ts true def t0 t1 t2 seen
6.945 - | (t0 as @{const "==>"}) $ t1 $ t2 =>
6.946 - if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
6.947 - | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
6.948 - do_eq_or_imp Ts true def t0 t1 t2 seen
6.949 - | (t0 as @{const "op -->"}) $ t1 $ t2 =>
6.950 - do_eq_or_imp Ts false def t0 t1 t2 seen
6.951 - | Abs (s, T, t') =>
6.952 - let val (t', seen) = do_term (T :: Ts) def t' [] seen in
6.953 - (list_comb (Abs (s, T, t'), args), seen)
6.954 - end
6.955 - | t1 $ t2 =>
6.956 - let val (t2, seen) = do_term Ts def t2 [] seen in
6.957 - do_term Ts def t1 (t2 :: args) seen
6.958 - end
6.959 - | _ => pull_out_constr_comb thy Ts def k 0 t args seen
6.960 - (* typ list -> bool -> bool -> term -> term -> term -> term list
6.961 - -> term * term list *)
6.962 - and do_eq_or_imp Ts eq def t0 t1 t2 seen =
6.963 - let
6.964 - val (t2, seen) = if eq andalso def then (t2, seen)
6.965 - else do_term Ts false t2 [] seen
6.966 - val (t1, seen) = do_term Ts false t1 [] seen
6.967 - in (t0 $ t1 $ t2, seen) end
6.968 - val (concl, seen) = do_term [] def t [] []
6.969 - in
6.970 - Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
6.971 - seen, concl)
6.972 - end
6.973 -
6.974 -(* extended_context -> bool -> term -> term *)
6.975 -fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
6.976 - let
6.977 - (* styp -> int *)
6.978 - val num_occs_of_var =
6.979 - fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
6.980 - | _ => I) t (K 0)
6.981 - (* bool -> term -> term *)
6.982 - fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
6.983 - aux_eq careful true t0 t1 t2
6.984 - | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
6.985 - t0 $ aux false t1 $ aux careful t2
6.986 - | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
6.987 - aux_eq careful true t0 t1 t2
6.988 - | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
6.989 - t0 $ aux false t1 $ aux careful t2
6.990 - | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
6.991 - | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
6.992 - | aux _ t = t
6.993 - (* bool -> bool -> term -> term -> term -> term *)
6.994 - and aux_eq careful pass1 t0 t1 t2 =
6.995 - ((if careful then
6.996 - raise SAME ()
6.997 - else if axiom andalso is_Var t2 andalso
6.998 - num_occs_of_var (dest_Var t2) = 1 then
6.999 - @{const True}
6.1000 - else case strip_comb t2 of
6.1001 - (* The first case is not as general as it could be. *)
6.1002 - (Const (@{const_name PairBox}, _),
6.1003 - [Const (@{const_name fst}, _) $ Var z1,
6.1004 - Const (@{const_name snd}, _) $ Var z2]) =>
6.1005 - if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
6.1006 - else raise SAME ()
6.1007 - | (Const (x as (s, T)), args) =>
6.1008 - let val arg_Ts = binder_types T in
6.1009 - if length arg_Ts = length args andalso
6.1010 - (is_constr thy x orelse s = @{const_name Pair} orelse
6.1011 - x = (@{const_name Suc}, nat_T --> nat_T)) andalso
6.1012 - (not careful orelse not (is_Var t1) orelse
6.1013 - String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
6.1014 - discriminate_value ext_ctxt x t1 ::
6.1015 - map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
6.1016 - |> foldr1 s_conj
6.1017 - else
6.1018 - raise SAME ()
6.1019 - end
6.1020 - | _ => raise SAME ())
6.1021 - |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
6.1022 - handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
6.1023 - else t0 $ aux false t2 $ aux false t1
6.1024 - (* styp -> term -> int -> typ -> term -> term *)
6.1025 - and sel_eq x t n nth_T nth_t =
6.1026 - HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
6.1027 - |> aux false
6.1028 - in aux axiom t end
6.1029 -
6.1030 -(* theory -> term -> term *)
6.1031 -fun simplify_constrs_and_sels thy t =
6.1032 - let
6.1033 - (* term -> int -> term *)
6.1034 - fun is_nth_sel_on t' n (Const (s, _) $ t) =
6.1035 - (t = t' andalso is_sel_like_and_no_discr s andalso
6.1036 - sel_no_from_name s = n)
6.1037 - | is_nth_sel_on _ _ _ = false
6.1038 - (* term -> term list -> term *)
6.1039 - fun do_term (Const (@{const_name Rep_Frac}, _)
6.1040 - $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
6.1041 - | do_term (Const (@{const_name Abs_Frac}, _)
6.1042 - $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
6.1043 - | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
6.1044 - | do_term (t as Const (x as (s, T))) (args as _ :: _) =
6.1045 - ((if is_constr_like thy x then
6.1046 - if length args = num_binder_types T then
6.1047 - case hd args of
6.1048 - Const (x' as (_, T')) $ t' =>
6.1049 - if domain_type T' = body_type T andalso
6.1050 - forall (uncurry (is_nth_sel_on t'))
6.1051 - (index_seq 0 (length args) ~~ args) then
6.1052 - t'
6.1053 - else
6.1054 - raise SAME ()
6.1055 - | _ => raise SAME ()
6.1056 - else
6.1057 - raise SAME ()
6.1058 - else if is_sel_like_and_no_discr s then
6.1059 - case strip_comb (hd args) of
6.1060 - (Const (x' as (s', T')), ts') =>
6.1061 - if is_constr_like thy x' andalso
6.1062 - constr_name_for_sel_like s = s' andalso
6.1063 - not (exists is_pair_type (binder_types T')) then
6.1064 - list_comb (nth ts' (sel_no_from_name s), tl args)
6.1065 - else
6.1066 - raise SAME ()
6.1067 - | _ => raise SAME ()
6.1068 - else
6.1069 - raise SAME ())
6.1070 - handle SAME () => betapplys (t, args))
6.1071 - | do_term (Abs (s, T, t')) args =
6.1072 - betapplys (Abs (s, T, do_term t' []), args)
6.1073 - | do_term t args = betapplys (t, args)
6.1074 - in do_term t [] end
6.1075 -
6.1076 -(* term -> term *)
6.1077 -fun curry_assms (@{const "==>"} $ (@{const Trueprop}
6.1078 - $ (@{const "op &"} $ t1 $ t2)) $ t3) =
6.1079 - curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
6.1080 - | curry_assms (@{const "==>"} $ t1 $ t2) =
6.1081 - @{const "==>"} $ curry_assms t1 $ curry_assms t2
6.1082 - | curry_assms t = t
6.1083 -
6.1084 -(* term -> term *)
6.1085 -val destroy_universal_equalities =
6.1086 - let
6.1087 - (* term list -> (indexname * typ) list -> term -> term *)
6.1088 - fun aux prems zs t =
6.1089 - case t of
6.1090 - @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
6.1091 - | _ => Logic.list_implies (rev prems, t)
6.1092 - (* term list -> (indexname * typ) list -> term -> term -> term *)
6.1093 - and aux_implies prems zs t1 t2 =
6.1094 - case t1 of
6.1095 - Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
6.1096 - | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
6.1097 - aux_eq prems zs z t' t1 t2
6.1098 - | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
6.1099 - aux_eq prems zs z t' t1 t2
6.1100 - | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
6.1101 - (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
6.1102 - -> term -> term *)
6.1103 - and aux_eq prems zs z t' t1 t2 =
6.1104 - if not (member (op =) zs z) andalso
6.1105 - not (exists_subterm (curry (op =) (Var z)) t') then
6.1106 - aux prems zs (subst_free [(Var z, t')] t2)
6.1107 - else
6.1108 - aux (t1 :: prems) (Term.add_vars t1 zs) t2
6.1109 - in aux [] [] end
6.1110 -
6.1111 -(* theory -> term -> term *)
6.1112 -fun pull_out_existential_constrs thy t =
6.1113 - let
6.1114 - val k = maxidx_of_term t + 1
6.1115 - (* typ list -> int -> term -> term list -> term list -> term * term list *)
6.1116 - fun aux Ts num_exists t args seen =
6.1117 - case t of
6.1118 - (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
6.1119 - let
6.1120 - val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
6.1121 - val n = length seen'
6.1122 - (* unit -> term list *)
6.1123 - fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
6.1124 - in
6.1125 - (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
6.1126 - |> List.foldl s_conj t1 |> fold mk_exists (vars ())
6.1127 - |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
6.1128 - end
6.1129 - | t1 $ t2 =>
6.1130 - let val (t2, seen) = aux Ts num_exists t2 [] seen in
6.1131 - aux Ts num_exists t1 (t2 :: args) seen
6.1132 - end
6.1133 - | Abs (s, T, t') =>
6.1134 - let
6.1135 - val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
6.1136 - in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
6.1137 - | _ =>
6.1138 - if num_exists > 0 then
6.1139 - pull_out_constr_comb thy Ts false k num_exists t args seen
6.1140 - else
6.1141 - (list_comb (t, args), seen)
6.1142 - in aux [] 0 t [] [] |> fst end
6.1143 -
6.1144 -(* theory -> int -> term list -> term list -> (term * term list) option *)
6.1145 -fun find_bound_assign _ _ _ [] = NONE
6.1146 - | find_bound_assign thy j seen (t :: ts) =
6.1147 - let
6.1148 - (* bool -> term -> term -> (term * term list) option *)
6.1149 - fun aux pass1 t1 t2 =
6.1150 - (if loose_bvar1 (t2, j) then
6.1151 - if pass1 then aux false t2 t1 else raise SAME ()
6.1152 - else case t1 of
6.1153 - Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
6.1154 - | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
6.1155 - if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then
6.1156 - SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
6.1157 - ts @ seen)
6.1158 - else
6.1159 - raise SAME ()
6.1160 - | _ => raise SAME ())
6.1161 - handle SAME () => find_bound_assign thy j (t :: seen) ts
6.1162 - in
6.1163 - case t of
6.1164 - Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
6.1165 - | _ => find_bound_assign thy j (t :: seen) ts
6.1166 - end
6.1167 -
6.1168 -(* int -> term -> term -> term *)
6.1169 -fun subst_one_bound j arg t =
6.1170 - let
6.1171 - fun aux (Bound i, lev) =
6.1172 - if i < lev then raise SAME ()
6.1173 - else if i = lev then incr_boundvars (lev - j) arg
6.1174 - else Bound (i - 1)
6.1175 - | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
6.1176 - | aux (f $ t, lev) =
6.1177 - (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
6.1178 - handle SAME () => f $ aux (t, lev))
6.1179 - | aux _ = raise SAME ()
6.1180 - in aux (t, j) handle SAME () => t end
6.1181 -
6.1182 -(* theory -> term -> term *)
6.1183 -fun destroy_existential_equalities thy =
6.1184 - let
6.1185 - (* string list -> typ list -> term list -> term *)
6.1186 - fun kill [] [] ts = foldr1 s_conj ts
6.1187 - | kill (s :: ss) (T :: Ts) ts =
6.1188 - (case find_bound_assign thy (length ss) [] ts of
6.1189 - SOME (_, []) => @{const True}
6.1190 - | SOME (arg_t, ts) =>
6.1191 - kill ss Ts (map (subst_one_bound (length ss)
6.1192 - (incr_bv (~1, length ss + 1, arg_t))) ts)
6.1193 - | NONE =>
6.1194 - Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
6.1195 - $ Abs (s, T, kill ss Ts ts))
6.1196 - | kill _ _ _ = raise UnequalLengths
6.1197 - (* string list -> typ list -> term -> term *)
6.1198 - fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
6.1199 - gather (ss @ [s1]) (Ts @ [T1]) t1
6.1200 - | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
6.1201 - | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
6.1202 - | gather [] [] t = t
6.1203 - | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t))
6.1204 - in gather [] [] end
6.1205 -
6.1206 -(* term -> term *)
6.1207 -fun distribute_quantifiers t =
6.1208 - case t of
6.1209 - (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
6.1210 - (case t1 of
6.1211 - (t10 as @{const "op &"}) $ t11 $ t12 =>
6.1212 - t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
6.1213 - $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
6.1214 - | (t10 as @{const Not}) $ t11 =>
6.1215 - t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
6.1216 - $ Abs (s, T1, t11))
6.1217 - | t1 =>
6.1218 - if not (loose_bvar1 (t1, 0)) then
6.1219 - distribute_quantifiers (incr_boundvars ~1 t1)
6.1220 - else
6.1221 - t0 $ Abs (s, T1, distribute_quantifiers t1))
6.1222 - | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
6.1223 - (case distribute_quantifiers t1 of
6.1224 - (t10 as @{const "op |"}) $ t11 $ t12 =>
6.1225 - t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
6.1226 - $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
6.1227 - | (t10 as @{const "op -->"}) $ t11 $ t12 =>
6.1228 - t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
6.1229 - $ Abs (s, T1, t11))
6.1230 - $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
6.1231 - | (t10 as @{const Not}) $ t11 =>
6.1232 - t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
6.1233 - $ Abs (s, T1, t11))
6.1234 - | t1 =>
6.1235 - if not (loose_bvar1 (t1, 0)) then
6.1236 - distribute_quantifiers (incr_boundvars ~1 t1)
6.1237 - else
6.1238 - t0 $ Abs (s, T1, distribute_quantifiers t1))
6.1239 - | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
6.1240 - | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
6.1241 - | _ => t
6.1242 -
6.1243 -(* int -> int -> (int -> int) -> term -> term *)
6.1244 -fun renumber_bounds j n f t =
6.1245 - case t of
6.1246 - t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
6.1247 - | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
6.1248 - | Bound j' =>
6.1249 - Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
6.1250 - | _ => t
6.1251 -
6.1252 -val quantifier_cluster_threshold = 7
6.1253 -
6.1254 -(* theory -> term -> term *)
6.1255 -fun push_quantifiers_inward thy =
6.1256 - let
6.1257 - (* string -> string list -> typ list -> term -> term *)
6.1258 - fun aux quant_s ss Ts t =
6.1259 - (case t of
6.1260 - (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
6.1261 - if s0 = quant_s then
6.1262 - aux s0 (s1 :: ss) (T1 :: Ts) t1
6.1263 - else if quant_s = "" andalso
6.1264 - (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
6.1265 - aux s0 [s1] [T1] t1
6.1266 - else
6.1267 - raise SAME ()
6.1268 - | _ => raise SAME ())
6.1269 - handle SAME () =>
6.1270 - case t of
6.1271 - t1 $ t2 =>
6.1272 - if quant_s = "" then
6.1273 - aux "" [] [] t1 $ aux "" [] [] t2
6.1274 - else
6.1275 - let
6.1276 - val typical_card = 4
6.1277 - (* ('a -> ''b list) -> 'a list -> ''b list *)
6.1278 - fun big_union proj ps =
6.1279 - fold (fold (insert (op =)) o proj) ps []
6.1280 - val (ts, connective) = strip_any_connective t
6.1281 - val T_costs =
6.1282 - map (bounded_card_of_type 65536 typical_card []) Ts
6.1283 - val t_costs = map size_of_term ts
6.1284 - val num_Ts = length Ts
6.1285 - (* int -> int *)
6.1286 - val flip = curry (op -) (num_Ts - 1)
6.1287 - val t_boundss = map (map flip o loose_bnos) ts
6.1288 - (* (int list * int) list -> int list
6.1289 - -> (int list * int) list *)
6.1290 - fun merge costly_boundss [] = costly_boundss
6.1291 - | merge costly_boundss (j :: js) =
6.1292 - let
6.1293 - val (yeas, nays) =
6.1294 - List.partition (fn (bounds, _) =>
6.1295 - member (op =) bounds j)
6.1296 - costly_boundss
6.1297 - val yeas_bounds = big_union fst yeas
6.1298 - val yeas_cost = Integer.sum (map snd yeas)
6.1299 - * nth T_costs j
6.1300 - in merge ((yeas_bounds, yeas_cost) :: nays) js end
6.1301 - (* (int list * int) list -> int list -> int *)
6.1302 - val cost = Integer.sum o map snd oo merge
6.1303 - (* Inspired by Claessen & Sörensson's polynomial binary
6.1304 - splitting heuristic (p. 5 of their MODEL 2003 paper). *)
6.1305 - (* (int list * int) list -> int list -> int list *)
6.1306 - fun heuristically_best_permutation _ [] = []
6.1307 - | heuristically_best_permutation costly_boundss js =
6.1308 - let
6.1309 - val (costly_boundss, (j, js)) =
6.1310 - js |> map (`(merge costly_boundss o single))
6.1311 - |> sort (int_ord
6.1312 - o pairself (Integer.sum o map snd o fst))
6.1313 - |> split_list |>> hd ||> pairf hd tl
6.1314 - in
6.1315 - j :: heuristically_best_permutation costly_boundss js
6.1316 - end
6.1317 - val js =
6.1318 - if length Ts <= quantifier_cluster_threshold then
6.1319 - all_permutations (index_seq 0 num_Ts)
6.1320 - |> map (`(cost (t_boundss ~~ t_costs)))
6.1321 - |> sort (int_ord o pairself fst) |> hd |> snd
6.1322 - else
6.1323 - heuristically_best_permutation (t_boundss ~~ t_costs)
6.1324 - (index_seq 0 num_Ts)
6.1325 - val back_js = map (fn j => find_index (curry (op =) j) js)
6.1326 - (index_seq 0 num_Ts)
6.1327 - val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
6.1328 - ts
6.1329 - (* (term * int list) list -> term *)
6.1330 - fun mk_connection [] =
6.1331 - raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
6.1332 - \mk_connection", "")
6.1333 - | mk_connection ts_cum_bounds =
6.1334 - ts_cum_bounds |> map fst
6.1335 - |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
6.1336 - (* (term * int list) list -> int list -> term *)
6.1337 - fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
6.1338 - | build ts_cum_bounds (j :: js) =
6.1339 - let
6.1340 - val (yeas, nays) =
6.1341 - List.partition (fn (_, bounds) =>
6.1342 - member (op =) bounds j)
6.1343 - ts_cum_bounds
6.1344 - ||> map (apfst (incr_boundvars ~1))
6.1345 - in
6.1346 - if null yeas then
6.1347 - build nays js
6.1348 - else
6.1349 - let val T = nth Ts (flip j) in
6.1350 - build ((Const (quant_s, (T --> bool_T) --> bool_T)
6.1351 - $ Abs (nth ss (flip j), T,
6.1352 - mk_connection yeas),
6.1353 - big_union snd yeas) :: nays) js
6.1354 - end
6.1355 - end
6.1356 - in build (ts ~~ t_boundss) js end
6.1357 - | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
6.1358 - | _ => t
6.1359 - in aux "" [] [] end
6.1360 -
6.1361 -(* polarity -> string -> bool *)
6.1362 -fun is_positive_existential polar quant_s =
6.1363 - (polar = Pos andalso quant_s = @{const_name Ex}) orelse
6.1364 - (polar = Neg andalso quant_s <> @{const_name Ex})
6.1365 -
6.1366 -(* extended_context -> int -> term -> term *)
6.1367 -fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
6.1368 - skolem_depth =
6.1369 - let
6.1370 - (* int list -> int list *)
6.1371 - val incrs = map (Integer.add 1)
6.1372 - (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
6.1373 - fun aux ss Ts js depth polar t =
6.1374 - let
6.1375 - (* string -> typ -> string -> typ -> term -> term *)
6.1376 - fun do_quantifier quant_s quant_T abs_s abs_T t =
6.1377 - if not (loose_bvar1 (t, 0)) then
6.1378 - aux ss Ts js depth polar (incr_boundvars ~1 t)
6.1379 - else if depth <= skolem_depth andalso
6.1380 - is_positive_existential polar quant_s then
6.1381 - let
6.1382 - val j = length (!skolems) + 1
6.1383 - val sko_s = skolem_prefix_for (length js) j ^ abs_s
6.1384 - val _ = Unsynchronized.change skolems (cons (sko_s, ss))
6.1385 - val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
6.1386 - map Bound (rev js))
6.1387 - val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
6.1388 - in
6.1389 - if null js then betapply (abs_t, sko_t)
6.1390 - else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
6.1391 - end
6.1392 - else
6.1393 - Const (quant_s, quant_T)
6.1394 - $ Abs (abs_s, abs_T,
6.1395 - if is_higher_order_type abs_T then
6.1396 - t
6.1397 - else
6.1398 - aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
6.1399 - (depth + 1) polar t)
6.1400 - in
6.1401 - case t of
6.1402 - Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
6.1403 - do_quantifier s0 T0 s1 T1 t1
6.1404 - | @{const "==>"} $ t1 $ t2 =>
6.1405 - @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
6.1406 - $ aux ss Ts js depth polar t2
6.1407 - | @{const Pure.conjunction} $ t1 $ t2 =>
6.1408 - @{const Pure.conjunction} $ aux ss Ts js depth polar t1
6.1409 - $ aux ss Ts js depth polar t2
6.1410 - | @{const Trueprop} $ t1 =>
6.1411 - @{const Trueprop} $ aux ss Ts js depth polar t1
6.1412 - | @{const Not} $ t1 =>
6.1413 - @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
6.1414 - | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
6.1415 - do_quantifier s0 T0 s1 T1 t1
6.1416 - | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
6.1417 - do_quantifier s0 T0 s1 T1 t1
6.1418 - | @{const "op &"} $ t1 $ t2 =>
6.1419 - @{const "op &"} $ aux ss Ts js depth polar t1
6.1420 - $ aux ss Ts js depth polar t2
6.1421 - | @{const "op |"} $ t1 $ t2 =>
6.1422 - @{const "op |"} $ aux ss Ts js depth polar t1
6.1423 - $ aux ss Ts js depth polar t2
6.1424 - | @{const "op -->"} $ t1 $ t2 =>
6.1425 - @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
6.1426 - $ aux ss Ts js depth polar t2
6.1427 - | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
6.1428 - t0 $ t1 $ aux ss Ts js depth polar t2
6.1429 - | Const (x as (s, T)) =>
6.1430 - if is_inductive_pred ext_ctxt x andalso
6.1431 - not (is_well_founded_inductive_pred ext_ctxt x) then
6.1432 - let
6.1433 - val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
6.1434 - val (pref, connective, set_oper) =
6.1435 - if gfp then
6.1436 - (lbfp_prefix,
6.1437 - @{const "op |"},
6.1438 - @{const_name upper_semilattice_fun_inst.sup_fun})
6.1439 - else
6.1440 - (ubfp_prefix,
6.1441 - @{const "op &"},
6.1442 - @{const_name lower_semilattice_fun_inst.inf_fun})
6.1443 - (* unit -> term *)
6.1444 - fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x
6.1445 - |> aux ss Ts js depth polar
6.1446 - fun neg () = Const (pref ^ s, T)
6.1447 - in
6.1448 - (case polar |> gfp ? flip_polarity of
6.1449 - Pos => pos ()
6.1450 - | Neg => neg ()
6.1451 - | Neut =>
6.1452 - if is_fun_type T then
6.1453 - let
6.1454 - val ((trunk_arg_Ts, rump_arg_T), body_T) =
6.1455 - T |> strip_type |>> split_last
6.1456 - val set_T = rump_arg_T --> body_T
6.1457 - (* (unit -> term) -> term *)
6.1458 - fun app f =
6.1459 - list_comb (f (),
6.1460 - map Bound (length trunk_arg_Ts - 1 downto 0))
6.1461 - in
6.1462 - List.foldr absdummy
6.1463 - (Const (set_oper, set_T --> set_T --> set_T)
6.1464 - $ app pos $ app neg) trunk_arg_Ts
6.1465 - end
6.1466 - else
6.1467 - connective $ pos () $ neg ())
6.1468 - end
6.1469 - else
6.1470 - Const x
6.1471 - | t1 $ t2 =>
6.1472 - betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
6.1473 - aux ss Ts [] depth Neut t2)
6.1474 - | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
6.1475 - | _ => t
6.1476 - end
6.1477 - in aux [] [] [] 0 Pos end
6.1478 -
6.1479 -(* extended_context -> styp -> (int * term option) list *)
6.1480 -fun static_args_in_term ({ersatz_table, ...} : extended_context) x t =
6.1481 - let
6.1482 - (* term -> term list -> term list -> term list list *)
6.1483 - fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
6.1484 - | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
6.1485 - | fun_calls t args =
6.1486 - (case t of
6.1487 - Const (x' as (s', T')) =>
6.1488 - x = x' orelse (case AList.lookup (op =) ersatz_table s' of
6.1489 - SOME s'' => x = (s'', T')
6.1490 - | NONE => false)
6.1491 - | _ => false) ? cons args
6.1492 - (* term list list -> term list list -> term list -> term list list *)
6.1493 - fun call_sets [] [] vs = [vs]
6.1494 - | call_sets [] uss vs = vs :: call_sets uss [] []
6.1495 - | call_sets ([] :: _) _ _ = []
6.1496 - | call_sets ((t :: ts) :: tss) uss vs =
6.1497 - OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
6.1498 - val sets = call_sets (fun_calls t [] []) [] []
6.1499 - val indexed_sets = sets ~~ (index_seq 0 (length sets))
6.1500 - in
6.1501 - fold_rev (fn (set, j) =>
6.1502 - case set of
6.1503 - [Var _] => AList.lookup (op =) indexed_sets set = SOME j
6.1504 - ? cons (j, NONE)
6.1505 - | [t as Const _] => cons (j, SOME t)
6.1506 - | [t as Free _] => cons (j, SOME t)
6.1507 - | _ => I) indexed_sets []
6.1508 - end
6.1509 -(* extended_context -> styp -> term list -> (int * term option) list *)
6.1510 -fun static_args_in_terms ext_ctxt x =
6.1511 - map (static_args_in_term ext_ctxt x)
6.1512 - #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
6.1513 -
6.1514 -(* term -> term list *)
6.1515 -fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
6.1516 - | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
6.1517 - | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
6.1518 - snd (strip_comb t1)
6.1519 - | params_in_equation _ = []
6.1520 -
6.1521 -(* styp -> styp -> int list -> term list -> term list -> term -> term *)
6.1522 -fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
6.1523 - let
6.1524 - val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
6.1525 - + 1
6.1526 - val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
6.1527 - val fixed_params = filter_indices fixed_js (params_in_equation t)
6.1528 - (* term list -> term -> term *)
6.1529 - fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
6.1530 - | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
6.1531 - | aux args t =
6.1532 - if t = Const x then
6.1533 - list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
6.1534 - else
6.1535 - let val j = find_index (curry (op =) t) fixed_params in
6.1536 - list_comb (if j >= 0 then nth fixed_args j else t, args)
6.1537 - end
6.1538 - in aux [] t end
6.1539 -
6.1540 -(* typ list -> term -> bool *)
6.1541 -fun is_eligible_arg Ts t =
6.1542 - let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
6.1543 - null bad_Ts orelse
6.1544 - (is_higher_order_type (fastype_of1 (Ts, t)) andalso
6.1545 - forall (not o is_higher_order_type) bad_Ts)
6.1546 - end
6.1547 -
6.1548 -(* (int * term option) list -> (int * term) list -> int list *)
6.1549 -fun overlapping_indices [] _ = []
6.1550 - | overlapping_indices _ [] = []
6.1551 - | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
6.1552 - if j1 < j2 then overlapping_indices ps1' ps2
6.1553 - else if j1 > j2 then overlapping_indices ps1 ps2'
6.1554 - else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
6.1555 -
6.1556 -val special_depth = 20
6.1557 -
6.1558 -(* extended_context -> int -> term -> term *)
6.1559 -fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table,
6.1560 - special_funs, ...}) depth t =
6.1561 - if not specialize orelse depth > special_depth then
6.1562 - t
6.1563 - else
6.1564 - let
6.1565 - val blacklist = if depth = 0 then []
6.1566 - else case term_under_def t of Const x => [x] | _ => []
6.1567 - (* term list -> typ list -> term -> term *)
6.1568 - fun aux args Ts (Const (x as (s, T))) =
6.1569 - ((if not (member (op =) blacklist x) andalso not (null args) andalso
6.1570 - not (String.isPrefix special_prefix s) andalso
6.1571 - is_equational_fun ext_ctxt x then
6.1572 - let
6.1573 - val eligible_args = filter (is_eligible_arg Ts o snd)
6.1574 - (index_seq 0 (length args) ~~ args)
6.1575 - val _ = not (null eligible_args) orelse raise SAME ()
6.1576 - val old_axs = equational_fun_axioms ext_ctxt x
6.1577 - |> map (destroy_existential_equalities thy)
6.1578 - val static_params = static_args_in_terms ext_ctxt x old_axs
6.1579 - val fixed_js = overlapping_indices static_params eligible_args
6.1580 - val _ = not (null fixed_js) orelse raise SAME ()
6.1581 - val fixed_args = filter_indices fixed_js args
6.1582 - val vars = fold Term.add_vars fixed_args []
6.1583 - |> sort (TermOrd.fast_indexname_ord o pairself fst)
6.1584 - val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
6.1585 - fixed_args []
6.1586 - |> sort int_ord
6.1587 - val live_args = filter_out_indices fixed_js args
6.1588 - val extra_args = map Var vars @ map Bound bound_js @ live_args
6.1589 - val extra_Ts = map snd vars @ filter_indices bound_js Ts
6.1590 - val k = maxidx_of_term t + 1
6.1591 - (* int -> term *)
6.1592 - fun var_for_bound_no j =
6.1593 - Var ((bound_var_prefix ^
6.1594 - nat_subscript (find_index (curry (op =) j) bound_js
6.1595 - + 1), k),
6.1596 - nth Ts j)
6.1597 - val fixed_args_in_axiom =
6.1598 - map (curry subst_bounds
6.1599 - (map var_for_bound_no (index_seq 0 (length Ts))))
6.1600 - fixed_args
6.1601 - in
6.1602 - case AList.lookup (op =) (!special_funs)
6.1603 - (x, fixed_js, fixed_args_in_axiom) of
6.1604 - SOME x' => list_comb (Const x', extra_args)
6.1605 - | NONE =>
6.1606 - let
6.1607 - val extra_args_in_axiom =
6.1608 - map Var vars @ map var_for_bound_no bound_js
6.1609 - val x' as (s', _) =
6.1610 - (special_prefix_for (length (!special_funs) + 1) ^ s,
6.1611 - extra_Ts @ filter_out_indices fixed_js (binder_types T)
6.1612 - ---> body_type T)
6.1613 - val new_axs =
6.1614 - map (specialize_fun_axiom x x' fixed_js
6.1615 - fixed_args_in_axiom extra_args_in_axiom) old_axs
6.1616 - val _ =
6.1617 - Unsynchronized.change special_funs
6.1618 - (cons ((x, fixed_js, fixed_args_in_axiom), x'))
6.1619 - val _ = add_simps simp_table s' new_axs
6.1620 - in list_comb (Const x', extra_args) end
6.1621 - end
6.1622 - else
6.1623 - raise SAME ())
6.1624 - handle SAME () => list_comb (Const x, args))
6.1625 - | aux args Ts (Abs (s, T, t)) =
6.1626 - list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
6.1627 - | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
6.1628 - | aux args _ t = list_comb (t, args)
6.1629 - in aux [] [] t end
6.1630 -
6.1631 -(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
6.1632 -fun add_to_uncurry_table thy t =
6.1633 - let
6.1634 - (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
6.1635 - fun aux (t1 $ t2) args table =
6.1636 - let val table = aux t2 [] table in aux t1 (t2 :: args) table end
6.1637 - | aux (Abs (_, _, t')) _ table = aux t' [] table
6.1638 - | aux (t as Const (x as (s, _))) args table =
6.1639 - if is_built_in_const true x orelse is_constr_like thy x orelse
6.1640 - is_sel s orelse s = @{const_name Sigma} then
6.1641 - table
6.1642 - else
6.1643 - Termtab.map_default (t, 65536) (curry Int.min (length args)) table
6.1644 - | aux _ _ table = table
6.1645 - in aux t [] end
6.1646 -
6.1647 -(* int Termtab.tab term -> term *)
6.1648 -fun uncurry_term table t =
6.1649 - let
6.1650 - (* term -> term list -> term *)
6.1651 - fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
6.1652 - | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
6.1653 - | aux (t as Const (s, T)) args =
6.1654 - (case Termtab.lookup table t of
6.1655 - SOME n =>
6.1656 - if n >= 2 then
6.1657 - let
6.1658 - val (arg_Ts, rest_T) = strip_n_binders n T
6.1659 - val j =
6.1660 - if hd arg_Ts = @{typ bisim_iterator} orelse
6.1661 - is_fp_iterator_type (hd arg_Ts) then
6.1662 - 1
6.1663 - else case find_index (not_equal bool_T) arg_Ts of
6.1664 - ~1 => n
6.1665 - | j => j
6.1666 - val ((before_args, tuple_args), after_args) =
6.1667 - args |> chop n |>> chop j
6.1668 - val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
6.1669 - T |> strip_n_binders n |>> chop j
6.1670 - val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
6.1671 - in
6.1672 - if n - j < 2 then
6.1673 - betapplys (t, args)
6.1674 - else
6.1675 - betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
6.1676 - before_arg_Ts ---> tuple_T --> rest_T),
6.1677 - before_args @ [mk_flat_tuple tuple_T tuple_args] @
6.1678 - after_args)
6.1679 - end
6.1680 - else
6.1681 - betapplys (t, args)
6.1682 - | NONE => betapplys (t, args))
6.1683 - | aux t args = betapplys (t, args)
6.1684 - in aux t [] end
6.1685 -
6.1686 -(* (term -> term) -> int -> term -> term *)
6.1687 -fun coerce_bound_no f j t =
6.1688 - case t of
6.1689 - t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
6.1690 - | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
6.1691 - | Bound j' => if j' = j then f t else t
6.1692 - | _ => t
6.1693 -
6.1694 -(* extended_context -> bool -> term -> term *)
6.1695 -fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t =
6.1696 - let
6.1697 - (* typ -> typ *)
6.1698 - fun box_relational_operator_type (Type ("fun", Ts)) =
6.1699 - Type ("fun", map box_relational_operator_type Ts)
6.1700 - | box_relational_operator_type (Type ("*", Ts)) =
6.1701 - Type ("*", map (box_type ext_ctxt InPair) Ts)
6.1702 - | box_relational_operator_type T = T
6.1703 - (* typ -> typ -> term -> term *)
6.1704 - fun coerce_bound_0_in_term new_T old_T =
6.1705 - old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
6.1706 - (* typ list -> typ -> term -> term *)
6.1707 - and coerce_term Ts new_T old_T t =
6.1708 - if old_T = new_T then
6.1709 - t
6.1710 - else
6.1711 - case (new_T, old_T) of
6.1712 - (Type (new_s, new_Ts as [new_T1, new_T2]),
6.1713 - Type ("fun", [old_T1, old_T2])) =>
6.1714 - (case eta_expand Ts t 1 of
6.1715 - Abs (s, _, t') =>
6.1716 - Abs (s, new_T1,
6.1717 - t' |> coerce_bound_0_in_term new_T1 old_T1
6.1718 - |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
6.1719 - |> Envir.eta_contract
6.1720 - |> new_s <> "fun"
6.1721 - ? construct_value thy (@{const_name FunBox},
6.1722 - Type ("fun", new_Ts) --> new_T) o single
6.1723 - | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
6.1724 - \coerce_term", [t']))
6.1725 - | (Type (new_s, new_Ts as [new_T1, new_T2]),
6.1726 - Type (old_s, old_Ts as [old_T1, old_T2])) =>
6.1727 - if old_s = @{type_name fun_box} orelse
6.1728 - old_s = @{type_name pair_box} orelse old_s = "*" then
6.1729 - case constr_expand ext_ctxt old_T t of
6.1730 - Const (@{const_name FunBox}, _) $ t1 =>
6.1731 - if new_s = "fun" then
6.1732 - coerce_term Ts new_T (Type ("fun", old_Ts)) t1
6.1733 - else
6.1734 - construct_value thy
6.1735 - (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
6.1736 - [coerce_term Ts (Type ("fun", new_Ts))
6.1737 - (Type ("fun", old_Ts)) t1]
6.1738 - | Const _ $ t1 $ t2 =>
6.1739 - construct_value thy
6.1740 - (if new_s = "*" then @{const_name Pair}
6.1741 - else @{const_name PairBox}, new_Ts ---> new_T)
6.1742 - [coerce_term Ts new_T1 old_T1 t1,
6.1743 - coerce_term Ts new_T2 old_T2 t2]
6.1744 - | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
6.1745 - \coerce_term", [t'])
6.1746 - else
6.1747 - raise TYPE ("coerce_term", [new_T, old_T], [t])
6.1748 - | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
6.1749 - (* indexname * typ -> typ * term -> typ option list -> typ option list *)
6.1750 - fun add_boxed_types_for_var (z as (_, T)) (T', t') =
6.1751 - case t' of
6.1752 - Var z' => z' = z ? insert (op =) T'
6.1753 - | Const (@{const_name Pair}, _) $ t1 $ t2 =>
6.1754 - (case T' of
6.1755 - Type (_, [T1, T2]) =>
6.1756 - fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
6.1757 - | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
6.1758 - \add_boxed_types_for_var", [T'], []))
6.1759 - | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
6.1760 - (* typ list -> typ list -> term -> indexname * typ -> typ *)
6.1761 - fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
6.1762 - case t of
6.1763 - @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
6.1764 - | Const (s0, _) $ t1 $ _ =>
6.1765 - if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
6.1766 - let
6.1767 - val (t', args) = strip_comb t1
6.1768 - val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
6.1769 - in
6.1770 - case fold (add_boxed_types_for_var z)
6.1771 - (fst (strip_n_binders (length args) T') ~~ args) [] of
6.1772 - [T''] => T''
6.1773 - | _ => T
6.1774 - end
6.1775 - else
6.1776 - T
6.1777 - | _ => T
6.1778 - (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
6.1779 - -> term -> term *)
6.1780 - and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
6.1781 - let
6.1782 - val abs_T' =
6.1783 - if polar = Neut orelse is_positive_existential polar quant_s then
6.1784 - box_type ext_ctxt InFunLHS abs_T
6.1785 - else
6.1786 - abs_T
6.1787 - val body_T = body_type quant_T
6.1788 - in
6.1789 - Const (quant_s, (abs_T' --> body_T) --> body_T)
6.1790 - $ Abs (abs_s, abs_T',
6.1791 - t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
6.1792 - end
6.1793 - (* typ list -> typ list -> string -> typ -> term -> term -> term *)
6.1794 - and do_equals new_Ts old_Ts s0 T0 t1 t2 =
6.1795 - let
6.1796 - val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
6.1797 - val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
6.1798 - val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
6.1799 - in
6.1800 - list_comb (Const (s0, T --> T --> body_type T0),
6.1801 - map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
6.1802 - end
6.1803 - (* string -> typ -> term *)
6.1804 - and do_description_operator s T =
6.1805 - let val T1 = box_type ext_ctxt InFunLHS (range_type T) in
6.1806 - Const (s, (T1 --> bool_T) --> T1)
6.1807 - end
6.1808 - (* typ list -> typ list -> polarity -> term -> term *)
6.1809 - and do_term new_Ts old_Ts polar t =
6.1810 - case t of
6.1811 - Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
6.1812 - do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
6.1813 - | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
6.1814 - do_equals new_Ts old_Ts s0 T0 t1 t2
6.1815 - | @{const "==>"} $ t1 $ t2 =>
6.1816 - @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
6.1817 - $ do_term new_Ts old_Ts polar t2
6.1818 - | @{const Pure.conjunction} $ t1 $ t2 =>
6.1819 - @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
6.1820 - $ do_term new_Ts old_Ts polar t2
6.1821 - | @{const Trueprop} $ t1 =>
6.1822 - @{const Trueprop} $ do_term new_Ts old_Ts polar t1
6.1823 - | @{const Not} $ t1 =>
6.1824 - @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
6.1825 - | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
6.1826 - do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
6.1827 - | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
6.1828 - do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
6.1829 - | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
6.1830 - do_equals new_Ts old_Ts s0 T0 t1 t2
6.1831 - | @{const "op &"} $ t1 $ t2 =>
6.1832 - @{const "op &"} $ do_term new_Ts old_Ts polar t1
6.1833 - $ do_term new_Ts old_Ts polar t2
6.1834 - | @{const "op |"} $ t1 $ t2 =>
6.1835 - @{const "op |"} $ do_term new_Ts old_Ts polar t1
6.1836 - $ do_term new_Ts old_Ts polar t2
6.1837 - | @{const "op -->"} $ t1 $ t2 =>
6.1838 - @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
6.1839 - $ do_term new_Ts old_Ts polar t2
6.1840 - | Const (s as @{const_name The}, T) => do_description_operator s T
6.1841 - | Const (s as @{const_name Eps}, T) => do_description_operator s T
6.1842 - | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
6.1843 - let val T' = box_type ext_ctxt InSel T2 in
6.1844 - Const (@{const_name quot_normal}, T' --> T')
6.1845 - end
6.1846 - | Const (s as @{const_name Tha}, T) => do_description_operator s T
6.1847 - | Const (x as (s, T)) =>
6.1848 - Const (s, if s = @{const_name converse} orelse
6.1849 - s = @{const_name trancl} then
6.1850 - box_relational_operator_type T
6.1851 - else if is_built_in_const fast_descrs x orelse
6.1852 - s = @{const_name Sigma} then
6.1853 - T
6.1854 - else if is_constr_like thy x then
6.1855 - box_type ext_ctxt InConstr T
6.1856 - else if is_sel s
6.1857 - orelse is_rep_fun thy x then
6.1858 - box_type ext_ctxt InSel T
6.1859 - else
6.1860 - box_type ext_ctxt InExpr T)
6.1861 - | t1 $ Abs (s, T, t2') =>
6.1862 - let
6.1863 - val t1 = do_term new_Ts old_Ts Neut t1
6.1864 - val T1 = fastype_of1 (new_Ts, t1)
6.1865 - val (s1, Ts1) = dest_Type T1
6.1866 - val T' = hd (snd (dest_Type (hd Ts1)))
6.1867 - val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
6.1868 - val T2 = fastype_of1 (new_Ts, t2)
6.1869 - val t2 = coerce_term new_Ts (hd Ts1) T2 t2
6.1870 - in
6.1871 - betapply (if s1 = "fun" then
6.1872 - t1
6.1873 - else
6.1874 - select_nth_constr_arg thy
6.1875 - (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
6.1876 - (Type ("fun", Ts1)), t2)
6.1877 - end
6.1878 - | t1 $ t2 =>
6.1879 - let
6.1880 - val t1 = do_term new_Ts old_Ts Neut t1
6.1881 - val T1 = fastype_of1 (new_Ts, t1)
6.1882 - val (s1, Ts1) = dest_Type T1
6.1883 - val t2 = do_term new_Ts old_Ts Neut t2
6.1884 - val T2 = fastype_of1 (new_Ts, t2)
6.1885 - val t2 = coerce_term new_Ts (hd Ts1) T2 t2
6.1886 - in
6.1887 - betapply (if s1 = "fun" then
6.1888 - t1
6.1889 - else
6.1890 - select_nth_constr_arg thy
6.1891 - (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
6.1892 - (Type ("fun", Ts1)), t2)
6.1893 - end
6.1894 - | Free (s, T) => Free (s, box_type ext_ctxt InExpr T)
6.1895 - | Var (z as (x, T)) =>
6.1896 - Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
6.1897 - else box_type ext_ctxt InExpr T)
6.1898 - | Bound _ => t
6.1899 - | Abs (s, T, t') =>
6.1900 - Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
6.1901 - in do_term [] [] Pos orig_t end
6.1902 -
6.1903 -(* int -> term -> term *)
6.1904 -fun eval_axiom_for_term j t =
6.1905 - Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
6.1906 -
6.1907 -(* extended_context -> styp -> bool *)
6.1908 -fun is_equational_fun_surely_complete ext_ctxt x =
6.1909 - case raw_equational_fun_axioms ext_ctxt x of
6.1910 - [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
6.1911 - strip_comb t1 |> snd |> forall is_Var
6.1912 - | _ => false
6.1913 -
6.1914 -type special = int list * term list * styp
6.1915 -
6.1916 -(* styp -> special -> special -> term *)
6.1917 -fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
6.1918 - let
6.1919 - val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
6.1920 - val Ts = binder_types T
6.1921 - val max_j = fold (fold Integer.max) [js1, js2] ~1
6.1922 - val (eqs, (args1, args2)) =
6.1923 - fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
6.1924 - (js1 ~~ ts1, js2 ~~ ts2) of
6.1925 - (SOME t1, SOME t2) => apfst (cons (t1, t2))
6.1926 - | (SOME t1, NONE) => apsnd (apsnd (cons t1))
6.1927 - | (NONE, SOME t2) => apsnd (apfst (cons t2))
6.1928 - | (NONE, NONE) =>
6.1929 - let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
6.1930 - nth Ts j) in
6.1931 - apsnd (pairself (cons v))
6.1932 - end) (max_j downto 0) ([], ([], []))
6.1933 - in
6.1934 - Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
6.1935 - |> map Logic.mk_equals,
6.1936 - Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
6.1937 - list_comb (Const x2, bounds2 @ args2)))
6.1938 - |> Refute.close_form (* TODO: needed? *)
6.1939 - end
6.1940 -
6.1941 -(* extended_context -> styp list -> term list *)
6.1942 -fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs =
6.1943 - let
6.1944 - val groups =
6.1945 - !special_funs
6.1946 - |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
6.1947 - |> AList.group (op =)
6.1948 - |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
6.1949 - |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
6.1950 - (* special -> int *)
6.1951 - fun generality (js, _, _) = ~(length js)
6.1952 - (* special -> special -> bool *)
6.1953 - fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
6.1954 - x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
6.1955 - (j2 ~~ t2, j1 ~~ t1)
6.1956 - (* styp -> special list -> special list -> special list -> term list
6.1957 - -> term list *)
6.1958 - fun do_pass_1 _ [] [_] [_] = I
6.1959 - | do_pass_1 x skipped _ [] = do_pass_2 x skipped
6.1960 - | do_pass_1 x skipped all (z :: zs) =
6.1961 - case filter (is_more_specific z) all
6.1962 - |> sort (int_ord o pairself generality) of
6.1963 - [] => do_pass_1 x (z :: skipped) all zs
6.1964 - | (z' :: _) => cons (special_congruence_axiom x z z')
6.1965 - #> do_pass_1 x skipped all zs
6.1966 - (* styp -> special list -> term list -> term list *)
6.1967 - and do_pass_2 _ [] = I
6.1968 - | do_pass_2 x (z :: zs) =
6.1969 - fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
6.1970 - in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
6.1971 -
6.1972 -(* term -> bool *)
6.1973 -val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
6.1974 -
6.1975 -(* 'a Symtab.table -> 'a list *)
6.1976 -fun all_table_entries table = Symtab.fold (append o snd) table []
6.1977 -(* const_table -> string -> const_table *)
6.1978 -fun extra_table table s = Symtab.make [(s, all_table_entries table)]
6.1979 -
6.1980 -(* extended_context -> term -> (term list * term list) * (bool * bool) *)
6.1981 -fun axioms_for_term
6.1982 - (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
6.1983 - def_table, nondef_table, user_nondefs, ...}) t =
6.1984 - let
6.1985 - type accumulator = styp list * (term list * term list)
6.1986 - (* (term list * term list -> term list)
6.1987 - -> ((term list -> term list) -> term list * term list
6.1988 - -> term list * term list)
6.1989 - -> int -> term -> accumulator -> accumulator *)
6.1990 - fun add_axiom get app depth t (accum as (xs, axs)) =
6.1991 - let
6.1992 - val t = t |> unfold_defs_in_term ext_ctxt
6.1993 - |> skolemize_term_and_more ext_ctxt ~1
6.1994 - in
6.1995 - if is_trivial_equation t then
6.1996 - accum
6.1997 - else
6.1998 - let val t' = t |> specialize_consts_in_term ext_ctxt depth in
6.1999 - if exists (member (op aconv) (get axs)) [t, t'] then accum
6.2000 - else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
6.2001 - end
6.2002 - end
6.2003 - (* int -> term -> accumulator -> accumulator *)
6.2004 - and add_def_axiom depth = add_axiom fst apfst depth
6.2005 - and add_nondef_axiom depth = add_axiom snd apsnd depth
6.2006 - and add_maybe_def_axiom depth t =
6.2007 - (if head_of t <> @{const "==>"} then add_def_axiom
6.2008 - else add_nondef_axiom) depth t
6.2009 - and add_eq_axiom depth t =
6.2010 - (if is_constr_pattern_formula thy t then add_def_axiom
6.2011 - else add_nondef_axiom) depth t
6.2012 - (* int -> term -> accumulator -> accumulator *)
6.2013 - and add_axioms_for_term depth t (accum as (xs, axs)) =
6.2014 - case t of
6.2015 - t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
6.2016 - | Const (x as (s, T)) =>
6.2017 - (if member (op =) xs x orelse is_built_in_const fast_descrs x then
6.2018 - accum
6.2019 - else
6.2020 - let val accum as (xs, _) = (x :: xs, axs) in
6.2021 - if depth > axioms_max_depth then
6.2022 - raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\
6.2023 - \add_axioms_for_term",
6.2024 - "too many nested axioms (" ^
6.2025 - string_of_int depth ^ ")")
6.2026 - else if Refute.is_const_of_class thy x then
6.2027 - let
6.2028 - val class = Logic.class_of_const s
6.2029 - val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
6.2030 - class)
6.2031 - val ax1 = try (Refute.specialize_type thy x) of_class
6.2032 - val ax2 = Option.map (Refute.specialize_type thy x o snd)
6.2033 - (Refute.get_classdef thy class)
6.2034 - in
6.2035 - fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
6.2036 - accum
6.2037 - end
6.2038 - else if is_constr thy x then
6.2039 - accum
6.2040 - else if is_equational_fun ext_ctxt x then
6.2041 - fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
6.2042 - accum
6.2043 - else if is_abs_fun thy x then
6.2044 - if is_quot_type thy (range_type T) then
6.2045 - raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
6.2046 - else
6.2047 - accum |> fold (add_nondef_axiom depth)
6.2048 - (nondef_props_for_const thy false nondef_table x)
6.2049 - |> is_funky_typedef thy (range_type T)
6.2050 - ? fold (add_maybe_def_axiom depth)
6.2051 - (nondef_props_for_const thy true
6.2052 - (extra_table def_table s) x)
6.2053 - else if is_rep_fun thy x then
6.2054 - if is_quot_type thy (domain_type T) then
6.2055 - raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
6.2056 - else
6.2057 - accum |> fold (add_nondef_axiom depth)
6.2058 - (nondef_props_for_const thy false nondef_table x)
6.2059 - |> is_funky_typedef thy (range_type T)
6.2060 - ? fold (add_maybe_def_axiom depth)
6.2061 - (nondef_props_for_const thy true
6.2062 - (extra_table def_table s) x)
6.2063 - |> add_axioms_for_term depth
6.2064 - (Const (mate_of_rep_fun thy x))
6.2065 - |> fold (add_def_axiom depth)
6.2066 - (inverse_axioms_for_rep_fun thy x)
6.2067 - else
6.2068 - accum |> user_axioms <> SOME false
6.2069 - ? fold (add_nondef_axiom depth)
6.2070 - (nondef_props_for_const thy false nondef_table x)
6.2071 - end)
6.2072 - |> add_axioms_for_type depth T
6.2073 - | Free (_, T) => add_axioms_for_type depth T accum
6.2074 - | Var (_, T) => add_axioms_for_type depth T accum
6.2075 - | Bound _ => accum
6.2076 - | Abs (_, T, t) => accum |> add_axioms_for_term depth t
6.2077 - |> add_axioms_for_type depth T
6.2078 - (* int -> typ -> accumulator -> accumulator *)
6.2079 - and add_axioms_for_type depth T =
6.2080 - case T of
6.2081 - Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
6.2082 - | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
6.2083 - | @{typ prop} => I
6.2084 - | @{typ bool} => I
6.2085 - | @{typ unit} => I
6.2086 - | TFree (_, S) => add_axioms_for_sort depth T S
6.2087 - | TVar (_, S) => add_axioms_for_sort depth T S
6.2088 - | Type (z as (s, Ts)) =>
6.2089 - fold (add_axioms_for_type depth) Ts
6.2090 - #> (if is_pure_typedef thy T then
6.2091 - fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
6.2092 - else if is_quot_type thy T then
6.2093 - fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
6.2094 - else if max_bisim_depth >= 0 andalso is_codatatype thy T then
6.2095 - fold (add_maybe_def_axiom depth)
6.2096 - (codatatype_bisim_axioms ext_ctxt T)
6.2097 - else
6.2098 - I)
6.2099 - (* int -> typ -> sort -> accumulator -> accumulator *)
6.2100 - and add_axioms_for_sort depth T S =
6.2101 - let
6.2102 - val supers = Sign.complete_sort thy S
6.2103 - val class_axioms =
6.2104 - maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
6.2105 - handle ERROR _ => [])) supers
6.2106 - val monomorphic_class_axioms =
6.2107 - map (fn t => case Term.add_tvars t [] of
6.2108 - [] => t
6.2109 - | [(x, S)] =>
6.2110 - Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
6.2111 - | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
6.2112 - \add_axioms_for_sort", [t]))
6.2113 - class_axioms
6.2114 - in fold (add_nondef_axiom depth) monomorphic_class_axioms end
6.2115 - val (mono_user_nondefs, poly_user_nondefs) =
6.2116 - List.partition (null o Term.hidden_polymorphism) user_nondefs
6.2117 - val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
6.2118 - evals
6.2119 - val (xs, (defs, nondefs)) =
6.2120 - ([], ([], [])) |> add_axioms_for_term 1 t
6.2121 - |> fold_rev (add_def_axiom 1) eval_axioms
6.2122 - |> user_axioms = SOME true
6.2123 - ? fold (add_nondef_axiom 1) mono_user_nondefs
6.2124 - val defs = defs @ special_congruence_axioms ext_ctxt xs
6.2125 - in
6.2126 - ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
6.2127 - null poly_user_nondefs))
6.2128 - end
6.2129 +(* hol_context -> typ -> typ list *)
6.2130 +fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T []
6.2131 +(* hol_context -> term list -> typ list *)
6.2132 +fun ground_types_in_terms hol_ctxt ts =
6.2133 + fold (fold_types (add_ground_types hol_ctxt)) ts []
6.2134
6.2135 (* theory -> const_table -> styp -> int list *)
6.2136 fun const_format thy def_table (x as (s, T)) =
6.2137 @@ -3356,10 +2096,10 @@
6.2138 |> map (rev o filter_out (member (op =) js))
6.2139 |> filter_out null |> map length |> rev
6.2140
6.2141 -(* extended_context -> string * string -> (term option * int list) list
6.2142 +(* hol_context -> string * string -> (term option * int list) list
6.2143 -> styp -> term * typ *)
6.2144 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
6.2145 - : extended_context) (base_name, step_name) formats =
6.2146 + : hol_context) (base_name, step_name) formats =
6.2147 let
6.2148 val default_format = the (AList.lookup (op =) formats NONE)
6.2149 (* styp -> term * typ *)
6.2150 @@ -3460,7 +2200,7 @@
6.2151 (t, format_term_type thy def_table formats t)
6.2152 end)
6.2153 |>> map_types unbit_and_unbox_type
6.2154 - |>> shorten_names_in_term |>> shorten_abs_vars
6.2155 + |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
6.2156 in do_const end
6.2157
6.2158 (* styp -> string *)
6.2159 @@ -3474,84 +2214,4 @@
6.2160 else
6.2161 "="
6.2162
6.2163 -val binary_int_threshold = 4
6.2164 -
6.2165 -(* term -> bool *)
6.2166 -fun may_use_binary_ints (t1 $ t2) =
6.2167 - may_use_binary_ints t1 andalso may_use_binary_ints t2
6.2168 - | may_use_binary_ints (t as Const (s, _)) =
6.2169 - t <> @{const Suc} andalso
6.2170 - not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
6.2171 - @{const_name nat_gcd}, @{const_name nat_lcm},
6.2172 - @{const_name Frac}, @{const_name norm_frac}] s)
6.2173 - | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
6.2174 - | may_use_binary_ints _ = true
6.2175 -fun should_use_binary_ints (t1 $ t2) =
6.2176 - should_use_binary_ints t1 orelse should_use_binary_ints t2
6.2177 - | should_use_binary_ints (Const (s, _)) =
6.2178 - member (op =) [@{const_name times_nat_inst.times_nat},
6.2179 - @{const_name div_nat_inst.div_nat},
6.2180 - @{const_name times_int_inst.times_int},
6.2181 - @{const_name div_int_inst.div_int}] s orelse
6.2182 - (String.isPrefix numeral_prefix s andalso
6.2183 - let val n = the (Int.fromString (unprefix numeral_prefix s)) in
6.2184 - n <= ~ binary_int_threshold orelse n >= binary_int_threshold
6.2185 - end)
6.2186 - | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
6.2187 - | should_use_binary_ints _ = false
6.2188 -
6.2189 -(* typ -> typ *)
6.2190 -fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
6.2191 - | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
6.2192 - | binarize_nat_and_int_in_type (Type (s, Ts)) =
6.2193 - Type (s, map binarize_nat_and_int_in_type Ts)
6.2194 - | binarize_nat_and_int_in_type T = T
6.2195 -(* term -> term *)
6.2196 -val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
6.2197 -
6.2198 -(* extended_context -> term
6.2199 - -> ((term list * term list) * (bool * bool)) * term *)
6.2200 -fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes,
6.2201 - skolemize, uncurry, ...}) t =
6.2202 - let
6.2203 - val skolem_depth = if skolemize then 4 else ~1
6.2204 - val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
6.2205 - core_t) = t |> unfold_defs_in_term ext_ctxt
6.2206 - |> Refute.close_form
6.2207 - |> skolemize_term_and_more ext_ctxt skolem_depth
6.2208 - |> specialize_consts_in_term ext_ctxt 0
6.2209 - |> `(axioms_for_term ext_ctxt)
6.2210 - val binarize =
6.2211 - case binary_ints of
6.2212 - SOME false => false
6.2213 - | _ =>
6.2214 - forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
6.2215 - (binary_ints = SOME true orelse
6.2216 - exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
6.2217 - val box = exists (not_equal (SOME false) o snd) boxes
6.2218 - val table =
6.2219 - Termtab.empty |> uncurry
6.2220 - ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
6.2221 - (* bool -> bool -> term -> term *)
6.2222 - fun do_rest def core =
6.2223 - binarize ? binarize_nat_and_int_in_term
6.2224 - #> uncurry ? uncurry_term table
6.2225 - #> box ? box_fun_and_pair_in_term ext_ctxt def
6.2226 - #> destroy_constrs ? (pull_out_universal_constrs thy def
6.2227 - #> pull_out_existential_constrs thy
6.2228 - #> destroy_pulled_out_constrs ext_ctxt def)
6.2229 - #> curry_assms
6.2230 - #> destroy_universal_equalities
6.2231 - #> destroy_existential_equalities thy
6.2232 - #> simplify_constrs_and_sels thy
6.2233 - #> distribute_quantifiers
6.2234 - #> push_quantifiers_inward thy
6.2235 - #> not core ? Refute.close_form
6.2236 - #> shorten_abs_vars
6.2237 - in
6.2238 - (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
6.2239 - (got_all_mono_user_axioms, no_poly_user_axioms)),
6.2240 - do_rest false true core_t)
6.2241 - end
6.2242 -
6.2243 end;
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 04 14:45:08 2010 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 05 11:15:16 2010 +0100
7.3 @@ -7,7 +7,7 @@
7.4
7.5 signature NITPICK_KODKOD =
7.6 sig
7.7 - type extended_context = Nitpick_HOL.extended_context
7.8 + type hol_context = Nitpick_HOL.hol_context
7.9 type dtype_spec = Nitpick_Scope.dtype_spec
7.10 type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
7.11 type nut = Nitpick_Nut.nut
7.12 @@ -33,7 +33,7 @@
7.13 val merge_bounds : Kodkod.bound list -> Kodkod.bound list
7.14 val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
7.15 val declarative_axioms_for_datatypes :
7.16 - extended_context -> int -> int Typtab.table -> kodkod_constrs
7.17 + hol_context -> int -> int Typtab.table -> kodkod_constrs
7.18 -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
7.19 val kodkod_formula_from_nut :
7.20 int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
7.21 @@ -316,7 +316,15 @@
7.22 if R2 = Formula Neut then
7.23 [ts] |> not exclusive ? cons (KK.TupleSet [])
7.24 else
7.25 - [KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)]
7.26 + [KK.TupleSet [],
7.27 + if exclusive andalso T1 = T2 andalso epsilon > delta then
7.28 + index_seq delta (epsilon - delta)
7.29 + |> map (fn j =>
7.30 + KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
7.31 + KK.TupleAtomSeq (j, j0)))
7.32 + |> foldl1 KK.TupleUnion
7.33 + else
7.34 + KK.TupleProduct (ts, upper_bound_for_rep R2)]
7.35 end)
7.36 end
7.37 | bound_for_sel_rel _ _ _ u =
7.38 @@ -732,12 +740,12 @@
7.39 (* nut NameTable.table -> styp -> KK.rel_expr *)
7.40 fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
7.41
7.42 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
7.43 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
7.44 -> styp -> int -> nfa_transition list *)
7.45 -fun nfa_transitions_for_sel ext_ctxt ({kk_project, ...} : kodkod_constrs)
7.46 +fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
7.47 rel_table (dtypes : dtype_spec list) constr_x n =
7.48 let
7.49 - val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt constr_x n
7.50 + val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
7.51 val (r, R, arity) = const_triple rel_table x
7.52 val type_schema = type_schema_of_rep T R
7.53 in
7.54 @@ -746,17 +754,17 @@
7.55 else SOME (kk_project r (map KK.Num [0, j]), T))
7.56 (index_seq 1 (arity - 1) ~~ tl type_schema)
7.57 end
7.58 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
7.59 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
7.60 -> styp -> nfa_transition list *)
7.61 -fun nfa_transitions_for_constr ext_ctxt kk rel_table dtypes (x as (_, T)) =
7.62 - maps (nfa_transitions_for_sel ext_ctxt kk rel_table dtypes x)
7.63 +fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
7.64 + maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
7.65 (index_seq 0 (num_sels_for_constr_type T))
7.66 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
7.67 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
7.68 -> dtype_spec -> nfa_entry option *)
7.69 fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
7.70 | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
7.71 - | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
7.72 - SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
7.73 + | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
7.74 + SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
7.75 o #const) constrs)
7.76
7.77 val empty_rel = KK.Product (KK.None, KK.None)
7.78 @@ -812,23 +820,23 @@
7.79 fun acyclicity_axiom_for_datatype dtypes kk nfa start =
7.80 #kk_no kk (#kk_intersect kk
7.81 (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
7.82 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
7.83 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
7.84 -> KK.formula list *)
7.85 -fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes =
7.86 - map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes
7.87 +fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
7.88 + map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
7.89 |> strongly_connected_sub_nfas
7.90 |> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst)
7.91 nfa)
7.92
7.93 -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
7.94 - -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
7.95 -fun sel_axiom_for_sel ext_ctxt j0
7.96 +(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
7.97 + -> constr_spec -> int -> KK.formula *)
7.98 +fun sel_axiom_for_sel hol_ctxt j0
7.99 (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
7.100 kk_join, ...}) rel_table dom_r
7.101 ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
7.102 n =
7.103 let
7.104 - val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt const n
7.105 + val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
7.106 val (r, R, arity) = const_triple rel_table x
7.107 val R2 = dest_Func R |> snd
7.108 val z = (epsilon - delta, delta + j0)
7.109 @@ -842,9 +850,9 @@
7.110 (kk_n_ary_function kk R2 r') (kk_no r'))
7.111 end
7.112 end
7.113 -(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
7.114 +(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
7.115 -> constr_spec -> KK.formula list *)
7.116 -fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
7.117 +fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
7.118 (constr as {const, delta, epsilon, explicit_max, ...}) =
7.119 let
7.120 val honors_explicit_max =
7.121 @@ -866,19 +874,19 @@
7.122 " too small for \"max\"")
7.123 in
7.124 max_axiom ::
7.125 - map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr)
7.126 + map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr)
7.127 (index_seq 0 (num_sels_for_constr_type (snd const)))
7.128 end
7.129 end
7.130 -(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
7.131 +(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
7.132 -> dtype_spec -> KK.formula list *)
7.133 -fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
7.134 +fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
7.135 ({constrs, ...} : dtype_spec) =
7.136 - maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
7.137 + maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
7.138
7.139 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
7.140 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
7.141 -> KK.formula list *)
7.142 -fun uniqueness_axiom_for_constr ext_ctxt
7.143 +fun uniqueness_axiom_for_constr hol_ctxt
7.144 ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
7.145 : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
7.146 let
7.147 @@ -887,7 +895,7 @@
7.148 kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
7.149 val num_sels = num_sels_for_constr_type (snd const)
7.150 val triples = map (const_triple rel_table
7.151 - o boxed_nth_sel_for_constr ext_ctxt const)
7.152 + o boxed_nth_sel_for_constr hol_ctxt const)
7.153 (~1 upto num_sels - 1)
7.154 val j0 = case triples |> hd |> #2 of
7.155 Func (Atom (_, j0), _) => j0
7.156 @@ -903,11 +911,11 @@
7.157 (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
7.158 (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
7.159 end
7.160 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
7.161 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
7.162 -> KK.formula list *)
7.163 -fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table
7.164 +fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
7.165 ({constrs, ...} : dtype_spec) =
7.166 - map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs
7.167 + map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
7.168
7.169 (* constr_spec -> int *)
7.170 fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
7.171 @@ -924,31 +932,31 @@
7.172 kk_disjoint_sets kk rs]
7.173 end
7.174
7.175 -(* extended_context -> int -> int Typtab.table -> kodkod_constrs
7.176 +(* hol_context -> int -> int Typtab.table -> kodkod_constrs
7.177 -> nut NameTable.table -> dtype_spec -> KK.formula list *)
7.178 fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
7.179 - | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
7.180 + | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
7.181 (dtype as {typ, ...}) =
7.182 let val j0 = offset_of_type ofs typ in
7.183 - sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @
7.184 - uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
7.185 + sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
7.186 + uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
7.187 partition_axioms_for_datatype j0 kk rel_table dtype
7.188 end
7.189
7.190 -(* extended_context -> int -> int Typtab.table -> kodkod_constrs
7.191 +(* hol_context -> int -> int Typtab.table -> kodkod_constrs
7.192 -> nut NameTable.table -> dtype_spec list -> KK.formula list *)
7.193 -fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
7.194 - acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
7.195 - maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
7.196 +fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
7.197 + acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
7.198 + maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
7.199
7.200 (* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
7.201 fun kodkod_formula_from_nut bits ofs liberal
7.202 (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
7.203 - kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
7.204 - kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference,
7.205 - kk_intersect, kk_product, kk_join, kk_closure, kk_comprehension,
7.206 - kk_project, kk_project_seq, kk_not3, kk_nat_less, kk_int_less,
7.207 - ...}) u =
7.208 + kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
7.209 + kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
7.210 + kk_difference, kk_intersect, kk_product, kk_join, kk_closure,
7.211 + kk_comprehension, kk_project, kk_project_seq, kk_not3,
7.212 + kk_nat_less, kk_int_less, ...}) u =
7.213 let
7.214 val main_j0 = offset_of_type ofs bool_T
7.215 val bool_j0 = main_j0
7.216 @@ -1108,7 +1116,7 @@
7.217 else
7.218 if is_lone_rep min_R then
7.219 if arity_of_rep min_R = 1 then
7.220 - kk_subset (kk_product r1 r2) KK.Iden
7.221 + kk_lone (kk_union r1 r2)
7.222 else if not both_opt then
7.223 (r1, r2) |> is_opt_rep (rep_of u2) ? swap
7.224 |-> kk_subset
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 04 14:45:08 2010 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 05 11:15:16 2010 +0100
8.3 @@ -251,7 +251,7 @@
8.4 -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
8.5 -> int list list -> term *)
8.6 fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
8.7 - ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
8.8 + ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
8.9 : scope) sel_names rel_table bounds =
8.10 let
8.11 val for_auto = (maybe_name = "")
8.12 @@ -400,7 +400,7 @@
8.13 else NONE)
8.14 (discr_jsss ~~ constrs) |> the
8.15 val arg_Ts = curried_binder_types constr_T
8.16 - val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x)
8.17 + val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x)
8.18 (index_seq 0 (length arg_Ts))
8.19 val sel_Rs =
8.20 map (fn x => get_first
8.21 @@ -586,7 +586,7 @@
8.22 -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
8.23 -> Pretty.T * bool *)
8.24 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
8.25 - ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
8.26 + ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
8.27 user_axioms, debug, binary_ints, destroy_constrs,
8.28 specialize, skolemize, star_linear_preds, uncurry,
8.29 fast_descrs, tac_timeout, evals, case_names, def_table,
8.30 @@ -598,7 +598,7 @@
8.31 let
8.32 val (wacky_names as (_, base_name, step_name, _), ctxt) =
8.33 add_wacky_syntax ctxt
8.34 - val ext_ctxt =
8.35 + val hol_ctxt =
8.36 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
8.37 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
8.38 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
8.39 @@ -612,7 +612,7 @@
8.40 ersatz_table = ersatz_table, skolems = skolems,
8.41 special_funs = special_funs, unrolled_preds = unrolled_preds,
8.42 wf_cache = wf_cache, constr_cache = constr_cache}
8.43 - val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
8.44 + val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
8.45 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
8.46 ofs = ofs}
8.47 (* typ -> typ -> rep -> int list list -> term *)
8.48 @@ -644,7 +644,7 @@
8.49 end
8.50 | ConstName (s, T, _) =>
8.51 (assign_operator_for_const (s, T),
8.52 - user_friendly_const ext_ctxt (base_name, step_name) formats (s, T),
8.53 + user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
8.54 T)
8.55 | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
8.56 \pretty_for_assign", [name])
8.57 @@ -724,7 +724,7 @@
8.58
8.59 (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
8.60 -> KK.raw_bound list -> term -> bool option *)
8.61 -fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, debug, ...},
8.62 +fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
8.63 card_assigns, ...})
8.64 auto_timeout free_names sel_names rel_table bounds prop =
8.65 let
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 04 14:45:08 2010 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Feb 05 11:15:16 2010 +0100
9.3 @@ -8,10 +8,10 @@
9.4 signature NITPICK_MONO =
9.5 sig
9.6 datatype sign = Plus | Minus
9.7 - type extended_context = Nitpick_HOL.extended_context
9.8 + type hol_context = Nitpick_HOL.hol_context
9.9
9.10 val formulas_monotonic :
9.11 - extended_context -> typ -> sign -> term list -> term list -> term -> bool
9.12 + hol_context -> typ -> sign -> term list -> term list -> term -> bool
9.13 end;
9.14
9.15 structure Nitpick_Mono : NITPICK_MONO =
9.16 @@ -35,7 +35,7 @@
9.17 CRec of string * typ list
9.18
9.19 type cdata =
9.20 - {ext_ctxt: extended_context,
9.21 + {hol_ctxt: hol_context,
9.22 alpha_T: typ,
9.23 max_fresh: int Unsynchronized.ref,
9.24 datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
9.25 @@ -114,9 +114,9 @@
9.26 | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
9.27 | flatten_ctype C = [C]
9.28
9.29 -(* extended_context -> typ -> cdata *)
9.30 -fun initial_cdata ext_ctxt alpha_T =
9.31 - ({ext_ctxt = ext_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
9.32 +(* hol_context -> typ -> cdata *)
9.33 +fun initial_cdata hol_ctxt alpha_T =
9.34 + ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
9.35 datatype_cache = Unsynchronized.ref [],
9.36 constr_cache = Unsynchronized.ref []} : cdata)
9.37
9.38 @@ -188,7 +188,7 @@
9.39 in List.app repair_one (!constr_cache) end
9.40
9.41 (* cdata -> typ -> ctype *)
9.42 -fun fresh_ctype_for_type ({ext_ctxt as {thy, ...}, alpha_T, max_fresh,
9.43 +fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, alpha_T, max_fresh,
9.44 datatype_cache, constr_cache, ...} : cdata) =
9.45 let
9.46 (* typ -> typ -> ctype *)
9.47 @@ -217,7 +217,7 @@
9.48 | NONE =>
9.49 let
9.50 val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
9.51 - val xs = datatype_constrs ext_ctxt T
9.52 + val xs = datatype_constrs hol_ctxt T
9.53 val (all_Cs, constr_Cs) =
9.54 fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
9.55 let
9.56 @@ -264,7 +264,7 @@
9.57 end
9.58
9.59 (* cdata -> styp -> ctype *)
9.60 -fun ctype_for_constr (cdata as {ext_ctxt as {thy, ...}, alpha_T, constr_cache,
9.61 +fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
9.62 ...}) (x as (_, T)) =
9.63 if could_exist_alpha_sub_ctype thy alpha_T T then
9.64 case AList.lookup (op =) (!constr_cache) x of
9.65 @@ -278,8 +278,8 @@
9.66 AList.lookup (op =) (!constr_cache) x |> the)
9.67 else
9.68 fresh_ctype_for_type cdata T
9.69 -fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =
9.70 - x |> boxed_constr_for_sel ext_ctxt |> ctype_for_constr cdata
9.71 +fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
9.72 + x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
9.73 |> sel_ctype_from_constr_ctype s
9.74
9.75 (* literal list -> ctype -> ctype *)
9.76 @@ -549,7 +549,7 @@
9.77 handle List.Empty => initial_gamma
9.78
9.79 (* cdata -> term -> accumulator -> ctype * accumulator *)
9.80 -fun consider_term (cdata as {ext_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
9.81 +fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
9.82 max_fresh, ...}) =
9.83 let
9.84 (* typ -> ctype *)
9.85 @@ -806,7 +806,7 @@
9.86 in do_term end
9.87
9.88 (* cdata -> sign -> term -> accumulator -> accumulator *)
9.89 -fun consider_general_formula (cdata as {ext_ctxt as {ctxt, ...}, ...}) =
9.90 +fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
9.91 let
9.92 (* typ -> ctype *)
9.93 val ctype_for = fresh_ctype_for_type cdata
9.94 @@ -895,7 +895,7 @@
9.95 not (is_harmless_axiom t) ? consider_general_formula cdata sn t
9.96
9.97 (* cdata -> term -> accumulator -> accumulator *)
9.98 -fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =
9.99 +fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
9.100 if not (is_constr_pattern_formula thy t) then
9.101 consider_nondefinitional_axiom cdata Plus t
9.102 else if is_harmless_axiom t then
9.103 @@ -945,13 +945,13 @@
9.104 map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
9.105 |> cat_lines |> print_g
9.106
9.107 -(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *)
9.108 -fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
9.109 +(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
9.110 +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
9.111 core_t =
9.112 let
9.113 val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
9.114 Syntax.string_of_typ ctxt alpha_T)
9.115 - val cdata as {max_fresh, ...} = initial_cdata ext_ctxt alpha_T
9.116 + val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
9.117 val (gamma, cset) =
9.118 (initial_gamma, slack)
9.119 |> fold (consider_definitional_axiom cdata) def_ts
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 04 14:45:08 2010 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Feb 05 11:15:16 2010 +0100
10.3 @@ -8,7 +8,7 @@
10.4 signature NITPICK_NUT =
10.5 sig
10.6 type special_fun = Nitpick_HOL.special_fun
10.7 - type extended_context = Nitpick_HOL.extended_context
10.8 + type hol_context = Nitpick_HOL.hol_context
10.9 type scope = Nitpick_Scope.scope
10.10 type name_pool = Nitpick_Peephole.name_pool
10.11 type rep = Nitpick_Rep.rep
10.12 @@ -106,7 +106,7 @@
10.13 val name_ord : (nut * nut) -> order
10.14 val the_name : 'a NameTable.table -> nut -> 'a
10.15 val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
10.16 - val nut_from_term : extended_context -> op2 -> term -> nut
10.17 + val nut_from_term : hol_context -> op2 -> term -> nut
10.18 val choose_reps_for_free_vars :
10.19 scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
10.20 val choose_reps_for_consts :
10.21 @@ -466,8 +466,8 @@
10.22 fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
10.23 | factorize z = [z]
10.24
10.25 -(* extended_context -> op2 -> term -> nut *)
10.26 -fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
10.27 +(* hol_context -> op2 -> term -> nut *)
10.28 +fun nut_from_term (hol_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
10.29 let
10.30 (* string list -> typ list -> term -> nut *)
10.31 fun aux eq ss Ts t =
10.32 @@ -597,7 +597,7 @@
10.33 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
10.34 | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
10.35 | (Const (@{const_name finite}, T), [t1]) =>
10.36 - (if is_finite_type ext_ctxt (domain_type T) then
10.37 + (if is_finite_type hol_ctxt (domain_type T) then
10.38 Cst (True, bool_T, Any)
10.39 else case t1 of
10.40 Const (@{const_name top}, _) => Cst (False, bool_T, Any)
10.41 @@ -712,7 +712,7 @@
10.42 in (v :: vs, NameTable.update (v, R) table) end
10.43 (* scope -> bool -> nut -> nut list * rep NameTable.table
10.44 -> nut list * rep NameTable.table *)
10.45 -fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes,
10.46 +fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes,
10.47 ofs, ...}) all_exact v (vs, table) =
10.48 let
10.49 val x as (s, T) = (nickname_of v, type_of v)
10.50 @@ -747,10 +747,10 @@
10.51
10.52 (* scope -> styp -> int -> nut list * rep NameTable.table
10.53 -> nut list * rep NameTable.table *)
10.54 -fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n
10.55 +fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n
10.56 (vs, table) =
10.57 let
10.58 - val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
10.59 + val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n
10.60 val R' = if n = ~1 orelse is_word_type (body_type T) orelse
10.61 (is_fun_type (range_type T') andalso
10.62 is_boolean_type (body_type T')) then
10.63 @@ -890,7 +890,7 @@
10.64 | untuple f u = if rep_of u = Unit then [] else [f u]
10.65
10.66 (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
10.67 -fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns,
10.68 +fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
10.69 bits, datatypes, ofs, ...})
10.70 liberal table def =
10.71 let
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Feb 05 11:15:16 2010 +0100
11.3 @@ -0,0 +1,1431 @@
11.4 +(* Title: HOL/Tools/Nitpick/nitpick_preproc.ML
11.5 + Author: Jasmin Blanchette, TU Muenchen
11.6 + Copyright 2008, 2009, 2010
11.7 +
11.8 +Nitpick's HOL preprocessor.
11.9 +*)
11.10 +
11.11 +signature NITPICK_PREPROC =
11.12 +sig
11.13 + type hol_context = Nitpick_HOL.hol_context
11.14 + val preprocess_term :
11.15 + hol_context -> term -> ((term list * term list) * (bool * bool)) * term
11.16 +end
11.17 +
11.18 +structure Nitpick_Preproc : NITPICK_PREPROC =
11.19 +struct
11.20 +
11.21 +open Nitpick_Util
11.22 +open Nitpick_HOL
11.23 +
11.24 +(* polarity -> string -> bool *)
11.25 +fun is_positive_existential polar quant_s =
11.26 + (polar = Pos andalso quant_s = @{const_name Ex}) orelse
11.27 + (polar = Neg andalso quant_s <> @{const_name Ex})
11.28 +
11.29 +(** Binary coding of integers **)
11.30 +
11.31 +(* If a formula contains a numeral whose absolute value is more than this
11.32 + threshold, the unary coding is likely not to work well and we prefer the
11.33 + binary coding. *)
11.34 +val binary_int_threshold = 3
11.35 +
11.36 +(* term -> bool *)
11.37 +fun may_use_binary_ints (t1 $ t2) =
11.38 + may_use_binary_ints t1 andalso may_use_binary_ints t2
11.39 + | may_use_binary_ints (t as Const (s, _)) =
11.40 + t <> @{const Suc} andalso
11.41 + not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
11.42 + @{const_name nat_gcd}, @{const_name nat_lcm},
11.43 + @{const_name Frac}, @{const_name norm_frac}] s)
11.44 + | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
11.45 + | may_use_binary_ints _ = true
11.46 +fun should_use_binary_ints (t1 $ t2) =
11.47 + should_use_binary_ints t1 orelse should_use_binary_ints t2
11.48 + | should_use_binary_ints (Const (s, _)) =
11.49 + member (op =) [@{const_name times_nat_inst.times_nat},
11.50 + @{const_name div_nat_inst.div_nat},
11.51 + @{const_name times_int_inst.times_int},
11.52 + @{const_name div_int_inst.div_int}] s orelse
11.53 + (String.isPrefix numeral_prefix s andalso
11.54 + let val n = the (Int.fromString (unprefix numeral_prefix s)) in
11.55 + n < ~ binary_int_threshold orelse n > binary_int_threshold
11.56 + end)
11.57 + | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
11.58 + | should_use_binary_ints _ = false
11.59 +
11.60 +(* typ -> typ *)
11.61 +fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
11.62 + | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
11.63 + | binarize_nat_and_int_in_type (Type (s, Ts)) =
11.64 + Type (s, map binarize_nat_and_int_in_type Ts)
11.65 + | binarize_nat_and_int_in_type T = T
11.66 +(* term -> term *)
11.67 +val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
11.68 +
11.69 +(** Uncurrying **)
11.70 +
11.71 +(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
11.72 +fun add_to_uncurry_table thy t =
11.73 + let
11.74 + (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
11.75 + fun aux (t1 $ t2) args table =
11.76 + let val table = aux t2 [] table in aux t1 (t2 :: args) table end
11.77 + | aux (Abs (_, _, t')) _ table = aux t' [] table
11.78 + | aux (t as Const (x as (s, _))) args table =
11.79 + if is_built_in_const true x orelse is_constr_like thy x orelse
11.80 + is_sel s orelse s = @{const_name Sigma} then
11.81 + table
11.82 + else
11.83 + Termtab.map_default (t, 65536) (curry Int.min (length args)) table
11.84 + | aux _ _ table = table
11.85 + in aux t [] end
11.86 +
11.87 +(* int -> int -> string *)
11.88 +fun uncurry_prefix_for k j =
11.89 + uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
11.90 +
11.91 +(* int Termtab.tab term -> term *)
11.92 +fun uncurry_term table t =
11.93 + let
11.94 + (* term -> term list -> term *)
11.95 + fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
11.96 + | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
11.97 + | aux (t as Const (s, T)) args =
11.98 + (case Termtab.lookup table t of
11.99 + SOME n =>
11.100 + if n >= 2 then
11.101 + let
11.102 + val (arg_Ts, rest_T) = strip_n_binders n T
11.103 + val j =
11.104 + if hd arg_Ts = @{typ bisim_iterator} orelse
11.105 + is_fp_iterator_type (hd arg_Ts) then
11.106 + 1
11.107 + else case find_index (not_equal bool_T) arg_Ts of
11.108 + ~1 => n
11.109 + | j => j
11.110 + val ((before_args, tuple_args), after_args) =
11.111 + args |> chop n |>> chop j
11.112 + val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
11.113 + T |> strip_n_binders n |>> chop j
11.114 + val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
11.115 + in
11.116 + if n - j < 2 then
11.117 + betapplys (t, args)
11.118 + else
11.119 + betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
11.120 + before_arg_Ts ---> tuple_T --> rest_T),
11.121 + before_args @ [mk_flat_tuple tuple_T tuple_args] @
11.122 + after_args)
11.123 + end
11.124 + else
11.125 + betapplys (t, args)
11.126 + | NONE => betapplys (t, args))
11.127 + | aux t args = betapplys (t, args)
11.128 + in aux t [] end
11.129 +
11.130 +(** Boxing **)
11.131 +
11.132 +(* hol_context -> typ -> term -> term *)
11.133 +fun constr_expand (hol_ctxt as {thy, ...}) T t =
11.134 + (case head_of t of
11.135 + Const x => if is_constr_like thy x then t else raise SAME ()
11.136 + | _ => raise SAME ())
11.137 + handle SAME () =>
11.138 + let
11.139 + val x' as (_, T') =
11.140 + if is_pair_type T then
11.141 + let val (T1, T2) = HOLogic.dest_prodT T in
11.142 + (@{const_name Pair}, T1 --> T2 --> T)
11.143 + end
11.144 + else
11.145 + datatype_constrs hol_ctxt T |> hd
11.146 + val arg_Ts = binder_types T'
11.147 + in
11.148 + list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
11.149 + (index_seq 0 (length arg_Ts)) arg_Ts)
11.150 + end
11.151 +
11.152 +(* hol_context -> bool -> term -> term *)
11.153 +fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =
11.154 + let
11.155 + (* typ -> typ *)
11.156 + fun box_relational_operator_type (Type ("fun", Ts)) =
11.157 + Type ("fun", map box_relational_operator_type Ts)
11.158 + | box_relational_operator_type (Type ("*", Ts)) =
11.159 + Type ("*", map (box_type hol_ctxt InPair) Ts)
11.160 + | box_relational_operator_type T = T
11.161 + (* (term -> term) -> int -> term -> term *)
11.162 + fun coerce_bound_no f j t =
11.163 + case t of
11.164 + t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
11.165 + | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
11.166 + | Bound j' => if j' = j then f t else t
11.167 + | _ => t
11.168 + (* typ -> typ -> term -> term *)
11.169 + fun coerce_bound_0_in_term new_T old_T =
11.170 + old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
11.171 + (* typ list -> typ -> term -> term *)
11.172 + and coerce_term Ts new_T old_T t =
11.173 + if old_T = new_T then
11.174 + t
11.175 + else
11.176 + case (new_T, old_T) of
11.177 + (Type (new_s, new_Ts as [new_T1, new_T2]),
11.178 + Type ("fun", [old_T1, old_T2])) =>
11.179 + (case eta_expand Ts t 1 of
11.180 + Abs (s, _, t') =>
11.181 + Abs (s, new_T1,
11.182 + t' |> coerce_bound_0_in_term new_T1 old_T1
11.183 + |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
11.184 + |> Envir.eta_contract
11.185 + |> new_s <> "fun"
11.186 + ? construct_value thy (@{const_name FunBox},
11.187 + Type ("fun", new_Ts) --> new_T) o single
11.188 + | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
11.189 + \coerce_term", [t']))
11.190 + | (Type (new_s, new_Ts as [new_T1, new_T2]),
11.191 + Type (old_s, old_Ts as [old_T1, old_T2])) =>
11.192 + if old_s = @{type_name fun_box} orelse
11.193 + old_s = @{type_name pair_box} orelse old_s = "*" then
11.194 + case constr_expand hol_ctxt old_T t of
11.195 + Const (@{const_name FunBox}, _) $ t1 =>
11.196 + if new_s = "fun" then
11.197 + coerce_term Ts new_T (Type ("fun", old_Ts)) t1
11.198 + else
11.199 + construct_value thy
11.200 + (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
11.201 + [coerce_term Ts (Type ("fun", new_Ts))
11.202 + (Type ("fun", old_Ts)) t1]
11.203 + | Const _ $ t1 $ t2 =>
11.204 + construct_value thy
11.205 + (if new_s = "*" then @{const_name Pair}
11.206 + else @{const_name PairBox}, new_Ts ---> new_T)
11.207 + [coerce_term Ts new_T1 old_T1 t1,
11.208 + coerce_term Ts new_T2 old_T2 t2]
11.209 + | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
11.210 + \coerce_term", [t'])
11.211 + else
11.212 + raise TYPE ("coerce_term", [new_T, old_T], [t])
11.213 + | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
11.214 + (* indexname * typ -> typ * term -> typ option list -> typ option list *)
11.215 + fun add_boxed_types_for_var (z as (_, T)) (T', t') =
11.216 + case t' of
11.217 + Var z' => z' = z ? insert (op =) T'
11.218 + | Const (@{const_name Pair}, _) $ t1 $ t2 =>
11.219 + (case T' of
11.220 + Type (_, [T1, T2]) =>
11.221 + fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
11.222 + | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\
11.223 + \add_boxed_types_for_var", [T'], []))
11.224 + | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
11.225 + (* typ list -> typ list -> term -> indexname * typ -> typ *)
11.226 + fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
11.227 + case t of
11.228 + @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
11.229 + | Const (s0, _) $ t1 $ _ =>
11.230 + if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
11.231 + let
11.232 + val (t', args) = strip_comb t1
11.233 + val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
11.234 + in
11.235 + case fold (add_boxed_types_for_var z)
11.236 + (fst (strip_n_binders (length args) T') ~~ args) [] of
11.237 + [T''] => T''
11.238 + | _ => T
11.239 + end
11.240 + else
11.241 + T
11.242 + | _ => T
11.243 + (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
11.244 + -> term -> term *)
11.245 + and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
11.246 + let
11.247 + val abs_T' =
11.248 + if polar = Neut orelse is_positive_existential polar quant_s then
11.249 + box_type hol_ctxt InFunLHS abs_T
11.250 + else
11.251 + abs_T
11.252 + val body_T = body_type quant_T
11.253 + in
11.254 + Const (quant_s, (abs_T' --> body_T) --> body_T)
11.255 + $ Abs (abs_s, abs_T',
11.256 + t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
11.257 + end
11.258 + (* typ list -> typ list -> string -> typ -> term -> term -> term *)
11.259 + and do_equals new_Ts old_Ts s0 T0 t1 t2 =
11.260 + let
11.261 + val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
11.262 + val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
11.263 + val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
11.264 + in
11.265 + list_comb (Const (s0, T --> T --> body_type T0),
11.266 + map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
11.267 + end
11.268 + (* string -> typ -> term *)
11.269 + and do_description_operator s T =
11.270 + let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
11.271 + Const (s, (T1 --> bool_T) --> T1)
11.272 + end
11.273 + (* typ list -> typ list -> polarity -> term -> term *)
11.274 + and do_term new_Ts old_Ts polar t =
11.275 + case t of
11.276 + Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
11.277 + do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
11.278 + | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
11.279 + do_equals new_Ts old_Ts s0 T0 t1 t2
11.280 + | @{const "==>"} $ t1 $ t2 =>
11.281 + @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
11.282 + $ do_term new_Ts old_Ts polar t2
11.283 + | @{const Pure.conjunction} $ t1 $ t2 =>
11.284 + @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
11.285 + $ do_term new_Ts old_Ts polar t2
11.286 + | @{const Trueprop} $ t1 =>
11.287 + @{const Trueprop} $ do_term new_Ts old_Ts polar t1
11.288 + | @{const Not} $ t1 =>
11.289 + @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
11.290 + | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
11.291 + do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
11.292 + | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
11.293 + do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
11.294 + | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
11.295 + do_equals new_Ts old_Ts s0 T0 t1 t2
11.296 + | @{const "op &"} $ t1 $ t2 =>
11.297 + @{const "op &"} $ do_term new_Ts old_Ts polar t1
11.298 + $ do_term new_Ts old_Ts polar t2
11.299 + | @{const "op |"} $ t1 $ t2 =>
11.300 + @{const "op |"} $ do_term new_Ts old_Ts polar t1
11.301 + $ do_term new_Ts old_Ts polar t2
11.302 + | @{const "op -->"} $ t1 $ t2 =>
11.303 + @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
11.304 + $ do_term new_Ts old_Ts polar t2
11.305 + | Const (s as @{const_name The}, T) => do_description_operator s T
11.306 + | Const (s as @{const_name Eps}, T) => do_description_operator s T
11.307 + | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
11.308 + let val T' = box_type hol_ctxt InSel T2 in
11.309 + Const (@{const_name quot_normal}, T' --> T')
11.310 + end
11.311 + | Const (s as @{const_name Tha}, T) => do_description_operator s T
11.312 + | Const (x as (s, T)) =>
11.313 + Const (s, if s = @{const_name converse} orelse
11.314 + s = @{const_name trancl} then
11.315 + box_relational_operator_type T
11.316 + else if is_built_in_const fast_descrs x orelse
11.317 + s = @{const_name Sigma} then
11.318 + T
11.319 + else if is_constr_like thy x then
11.320 + box_type hol_ctxt InConstr T
11.321 + else if is_sel s
11.322 + orelse is_rep_fun thy x then
11.323 + box_type hol_ctxt InSel T
11.324 + else
11.325 + box_type hol_ctxt InExpr T)
11.326 + | t1 $ Abs (s, T, t2') =>
11.327 + let
11.328 + val t1 = do_term new_Ts old_Ts Neut t1
11.329 + val T1 = fastype_of1 (new_Ts, t1)
11.330 + val (s1, Ts1) = dest_Type T1
11.331 + val T' = hd (snd (dest_Type (hd Ts1)))
11.332 + val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
11.333 + val T2 = fastype_of1 (new_Ts, t2)
11.334 + val t2 = coerce_term new_Ts (hd Ts1) T2 t2
11.335 + in
11.336 + betapply (if s1 = "fun" then
11.337 + t1
11.338 + else
11.339 + select_nth_constr_arg thy
11.340 + (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
11.341 + (Type ("fun", Ts1)), t2)
11.342 + end
11.343 + | t1 $ t2 =>
11.344 + let
11.345 + val t1 = do_term new_Ts old_Ts Neut t1
11.346 + val T1 = fastype_of1 (new_Ts, t1)
11.347 + val (s1, Ts1) = dest_Type T1
11.348 + val t2 = do_term new_Ts old_Ts Neut t2
11.349 + val T2 = fastype_of1 (new_Ts, t2)
11.350 + val t2 = coerce_term new_Ts (hd Ts1) T2 t2
11.351 + in
11.352 + betapply (if s1 = "fun" then
11.353 + t1
11.354 + else
11.355 + select_nth_constr_arg thy
11.356 + (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
11.357 + (Type ("fun", Ts1)), t2)
11.358 + end
11.359 + | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
11.360 + | Var (z as (x, T)) =>
11.361 + Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
11.362 + else box_type hol_ctxt InExpr T)
11.363 + | Bound _ => t
11.364 + | Abs (s, T, t') =>
11.365 + Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
11.366 + in do_term [] [] Pos orig_t end
11.367 +
11.368 +(** Destruction of constructors **)
11.369 +
11.370 +val val_var_prefix = nitpick_prefix ^ "v"
11.371 +
11.372 +(* typ list -> int -> int -> int -> term -> term *)
11.373 +fun fresh_value_var Ts k n j t =
11.374 + Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
11.375 +
11.376 +(* typ list -> int -> term -> bool *)
11.377 +fun has_heavy_bounds_or_vars Ts level t =
11.378 + let
11.379 + (* typ list -> bool *)
11.380 + fun aux [] = false
11.381 + | aux [T] = is_fun_type T orelse is_pair_type T
11.382 + | aux _ = true
11.383 + in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
11.384 +
11.385 +(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
11.386 + -> term * term list *)
11.387 +fun pull_out_constr_comb thy Ts relax k level t args seen =
11.388 + let val t_comb = list_comb (t, args) in
11.389 + case t of
11.390 + Const x =>
11.391 + if not relax andalso is_constr thy x andalso
11.392 + not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
11.393 + has_heavy_bounds_or_vars Ts level t_comb andalso
11.394 + not (loose_bvar (t_comb, level)) then
11.395 + let
11.396 + val (j, seen) = case find_index (curry (op =) t_comb) seen of
11.397 + ~1 => (0, t_comb :: seen)
11.398 + | j => (j, seen)
11.399 + in (fresh_value_var Ts k (length seen) j t_comb, seen) end
11.400 + else
11.401 + (t_comb, seen)
11.402 + | _ => (t_comb, seen)
11.403 + end
11.404 +
11.405 +(* (term -> term) -> typ list -> int -> term list -> term list *)
11.406 +fun equations_for_pulled_out_constrs mk_eq Ts k seen =
11.407 + let val n = length seen in
11.408 + map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
11.409 + (index_seq 0 n) seen
11.410 + end
11.411 +
11.412 +(* theory -> bool -> term -> term *)
11.413 +fun pull_out_universal_constrs thy def t =
11.414 + let
11.415 + val k = maxidx_of_term t + 1
11.416 + (* typ list -> bool -> term -> term list -> term list -> term * term list *)
11.417 + fun do_term Ts def t args seen =
11.418 + case t of
11.419 + (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
11.420 + do_eq_or_imp Ts true def t0 t1 t2 seen
11.421 + | (t0 as @{const "==>"}) $ t1 $ t2 =>
11.422 + if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
11.423 + | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
11.424 + do_eq_or_imp Ts true def t0 t1 t2 seen
11.425 + | (t0 as @{const "op -->"}) $ t1 $ t2 =>
11.426 + do_eq_or_imp Ts false def t0 t1 t2 seen
11.427 + | Abs (s, T, t') =>
11.428 + let val (t', seen) = do_term (T :: Ts) def t' [] seen in
11.429 + (list_comb (Abs (s, T, t'), args), seen)
11.430 + end
11.431 + | t1 $ t2 =>
11.432 + let val (t2, seen) = do_term Ts def t2 [] seen in
11.433 + do_term Ts def t1 (t2 :: args) seen
11.434 + end
11.435 + | _ => pull_out_constr_comb thy Ts def k 0 t args seen
11.436 + (* typ list -> bool -> bool -> term -> term -> term -> term list
11.437 + -> term * term list *)
11.438 + and do_eq_or_imp Ts eq def t0 t1 t2 seen =
11.439 + let
11.440 + val (t2, seen) = if eq andalso def then (t2, seen)
11.441 + else do_term Ts false t2 [] seen
11.442 + val (t1, seen) = do_term Ts false t1 [] seen
11.443 + in (t0 $ t1 $ t2, seen) end
11.444 + val (concl, seen) = do_term [] def t [] []
11.445 + in
11.446 + Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
11.447 + seen, concl)
11.448 + end
11.449 +
11.450 +(* term -> term -> term *)
11.451 +fun mk_exists v t =
11.452 + HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
11.453 +
11.454 +(* theory -> term -> term *)
11.455 +fun pull_out_existential_constrs thy t =
11.456 + let
11.457 + val k = maxidx_of_term t + 1
11.458 + (* typ list -> int -> term -> term list -> term list -> term * term list *)
11.459 + fun aux Ts num_exists t args seen =
11.460 + case t of
11.461 + (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
11.462 + let
11.463 + val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
11.464 + val n = length seen'
11.465 + (* unit -> term list *)
11.466 + fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
11.467 + in
11.468 + (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
11.469 + |> List.foldl s_conj t1 |> fold mk_exists (vars ())
11.470 + |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
11.471 + end
11.472 + | t1 $ t2 =>
11.473 + let val (t2, seen) = aux Ts num_exists t2 [] seen in
11.474 + aux Ts num_exists t1 (t2 :: args) seen
11.475 + end
11.476 + | Abs (s, T, t') =>
11.477 + let
11.478 + val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
11.479 + in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
11.480 + | _ =>
11.481 + if num_exists > 0 then
11.482 + pull_out_constr_comb thy Ts false k num_exists t args seen
11.483 + else
11.484 + (list_comb (t, args), seen)
11.485 + in aux [] 0 t [] [] |> fst end
11.486 +
11.487 +(* hol_context -> bool -> term -> term *)
11.488 +fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =
11.489 + let
11.490 + (* styp -> int *)
11.491 + val num_occs_of_var =
11.492 + fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
11.493 + | _ => I) t (K 0)
11.494 + (* bool -> term -> term *)
11.495 + fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
11.496 + aux_eq careful true t0 t1 t2
11.497 + | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
11.498 + t0 $ aux false t1 $ aux careful t2
11.499 + | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
11.500 + aux_eq careful true t0 t1 t2
11.501 + | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
11.502 + t0 $ aux false t1 $ aux careful t2
11.503 + | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
11.504 + | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
11.505 + | aux _ t = t
11.506 + (* bool -> bool -> term -> term -> term -> term *)
11.507 + and aux_eq careful pass1 t0 t1 t2 =
11.508 + ((if careful then
11.509 + raise SAME ()
11.510 + else if axiom andalso is_Var t2 andalso
11.511 + num_occs_of_var (dest_Var t2) = 1 then
11.512 + @{const True}
11.513 + else case strip_comb t2 of
11.514 + (* The first case is not as general as it could be. *)
11.515 + (Const (@{const_name PairBox}, _),
11.516 + [Const (@{const_name fst}, _) $ Var z1,
11.517 + Const (@{const_name snd}, _) $ Var z2]) =>
11.518 + if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
11.519 + else raise SAME ()
11.520 + | (Const (x as (s, T)), args) =>
11.521 + let val arg_Ts = binder_types T in
11.522 + if length arg_Ts = length args andalso
11.523 + (is_constr thy x orelse s = @{const_name Pair} orelse
11.524 + x = (@{const_name Suc}, nat_T --> nat_T)) andalso
11.525 + (not careful orelse not (is_Var t1) orelse
11.526 + String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
11.527 + discriminate_value hol_ctxt x t1 ::
11.528 + map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
11.529 + |> foldr1 s_conj
11.530 + else
11.531 + raise SAME ()
11.532 + end
11.533 + | _ => raise SAME ())
11.534 + |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
11.535 + handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
11.536 + else t0 $ aux false t2 $ aux false t1
11.537 + (* styp -> term -> int -> typ -> term -> term *)
11.538 + and sel_eq x t n nth_T nth_t =
11.539 + HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
11.540 + |> aux false
11.541 + in aux axiom t end
11.542 +
11.543 +(** Destruction of universal and existential equalities **)
11.544 +
11.545 +(* term -> term *)
11.546 +fun curry_assms (@{const "==>"} $ (@{const Trueprop}
11.547 + $ (@{const "op &"} $ t1 $ t2)) $ t3) =
11.548 + curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
11.549 + | curry_assms (@{const "==>"} $ t1 $ t2) =
11.550 + @{const "==>"} $ curry_assms t1 $ curry_assms t2
11.551 + | curry_assms t = t
11.552 +
11.553 +(* term -> term *)
11.554 +val destroy_universal_equalities =
11.555 + let
11.556 + (* term list -> (indexname * typ) list -> term -> term *)
11.557 + fun aux prems zs t =
11.558 + case t of
11.559 + @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
11.560 + | _ => Logic.list_implies (rev prems, t)
11.561 + (* term list -> (indexname * typ) list -> term -> term -> term *)
11.562 + and aux_implies prems zs t1 t2 =
11.563 + case t1 of
11.564 + Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
11.565 + | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
11.566 + aux_eq prems zs z t' t1 t2
11.567 + | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
11.568 + aux_eq prems zs z t' t1 t2
11.569 + | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
11.570 + (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
11.571 + -> term -> term *)
11.572 + and aux_eq prems zs z t' t1 t2 =
11.573 + if not (member (op =) zs z) andalso
11.574 + not (exists_subterm (curry (op =) (Var z)) t') then
11.575 + aux prems zs (subst_free [(Var z, t')] t2)
11.576 + else
11.577 + aux (t1 :: prems) (Term.add_vars t1 zs) t2
11.578 + in aux [] [] end
11.579 +
11.580 +(* theory -> int -> term list -> term list -> (term * term list) option *)
11.581 +fun find_bound_assign _ _ _ [] = NONE
11.582 + | find_bound_assign thy j seen (t :: ts) =
11.583 + let
11.584 + (* bool -> term -> term -> (term * term list) option *)
11.585 + fun aux pass1 t1 t2 =
11.586 + (if loose_bvar1 (t2, j) then
11.587 + if pass1 then aux false t2 t1 else raise SAME ()
11.588 + else case t1 of
11.589 + Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
11.590 + | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
11.591 + if j' = j andalso
11.592 + s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
11.593 + SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
11.594 + ts @ seen)
11.595 + else
11.596 + raise SAME ()
11.597 + | _ => raise SAME ())
11.598 + handle SAME () => find_bound_assign thy j (t :: seen) ts
11.599 + in
11.600 + case t of
11.601 + Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
11.602 + | _ => find_bound_assign thy j (t :: seen) ts
11.603 + end
11.604 +
11.605 +(* int -> term -> term -> term *)
11.606 +fun subst_one_bound j arg t =
11.607 + let
11.608 + fun aux (Bound i, lev) =
11.609 + if i < lev then raise SAME ()
11.610 + else if i = lev then incr_boundvars (lev - j) arg
11.611 + else Bound (i - 1)
11.612 + | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
11.613 + | aux (f $ t, lev) =
11.614 + (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
11.615 + handle SAME () => f $ aux (t, lev))
11.616 + | aux _ = raise SAME ()
11.617 + in aux (t, j) handle SAME () => t end
11.618 +
11.619 +(* theory -> term -> term *)
11.620 +fun destroy_existential_equalities thy =
11.621 + let
11.622 + (* string list -> typ list -> term list -> term *)
11.623 + fun kill [] [] ts = foldr1 s_conj ts
11.624 + | kill (s :: ss) (T :: Ts) ts =
11.625 + (case find_bound_assign thy (length ss) [] ts of
11.626 + SOME (_, []) => @{const True}
11.627 + | SOME (arg_t, ts) =>
11.628 + kill ss Ts (map (subst_one_bound (length ss)
11.629 + (incr_bv (~1, length ss + 1, arg_t))) ts)
11.630 + | NONE =>
11.631 + Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
11.632 + $ Abs (s, T, kill ss Ts ts))
11.633 + | kill _ _ _ = raise UnequalLengths
11.634 + (* string list -> typ list -> term -> term *)
11.635 + fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
11.636 + gather (ss @ [s1]) (Ts @ [T1]) t1
11.637 + | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
11.638 + | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
11.639 + | gather [] [] t = t
11.640 + | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))
11.641 + in gather [] [] end
11.642 +
11.643 +(** Skolemization **)
11.644 +
11.645 +(* int -> int -> string *)
11.646 +fun skolem_prefix_for k j =
11.647 + skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
11.648 +
11.649 +(* hol_context -> int -> term -> term *)
11.650 +fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
11.651 + skolem_depth =
11.652 + let
11.653 + (* int list -> int list *)
11.654 + val incrs = map (Integer.add 1)
11.655 + (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
11.656 + fun aux ss Ts js depth polar t =
11.657 + let
11.658 + (* string -> typ -> string -> typ -> term -> term *)
11.659 + fun do_quantifier quant_s quant_T abs_s abs_T t =
11.660 + if not (loose_bvar1 (t, 0)) then
11.661 + aux ss Ts js depth polar (incr_boundvars ~1 t)
11.662 + else if depth <= skolem_depth andalso
11.663 + is_positive_existential polar quant_s then
11.664 + let
11.665 + val j = length (!skolems) + 1
11.666 + val sko_s = skolem_prefix_for (length js) j ^ abs_s
11.667 + val _ = Unsynchronized.change skolems (cons (sko_s, ss))
11.668 + val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
11.669 + map Bound (rev js))
11.670 + val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
11.671 + in
11.672 + if null js then betapply (abs_t, sko_t)
11.673 + else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
11.674 + end
11.675 + else
11.676 + Const (quant_s, quant_T)
11.677 + $ Abs (abs_s, abs_T,
11.678 + if is_higher_order_type abs_T then
11.679 + t
11.680 + else
11.681 + aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
11.682 + (depth + 1) polar t)
11.683 + in
11.684 + case t of
11.685 + Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
11.686 + do_quantifier s0 T0 s1 T1 t1
11.687 + | @{const "==>"} $ t1 $ t2 =>
11.688 + @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
11.689 + $ aux ss Ts js depth polar t2
11.690 + | @{const Pure.conjunction} $ t1 $ t2 =>
11.691 + @{const Pure.conjunction} $ aux ss Ts js depth polar t1
11.692 + $ aux ss Ts js depth polar t2
11.693 + | @{const Trueprop} $ t1 =>
11.694 + @{const Trueprop} $ aux ss Ts js depth polar t1
11.695 + | @{const Not} $ t1 =>
11.696 + @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
11.697 + | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
11.698 + do_quantifier s0 T0 s1 T1 t1
11.699 + | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
11.700 + do_quantifier s0 T0 s1 T1 t1
11.701 + | @{const "op &"} $ t1 $ t2 =>
11.702 + @{const "op &"} $ aux ss Ts js depth polar t1
11.703 + $ aux ss Ts js depth polar t2
11.704 + | @{const "op |"} $ t1 $ t2 =>
11.705 + @{const "op |"} $ aux ss Ts js depth polar t1
11.706 + $ aux ss Ts js depth polar t2
11.707 + | @{const "op -->"} $ t1 $ t2 =>
11.708 + @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
11.709 + $ aux ss Ts js depth polar t2
11.710 + | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
11.711 + t0 $ t1 $ aux ss Ts js depth polar t2
11.712 + | Const (x as (s, T)) =>
11.713 + if is_inductive_pred hol_ctxt x andalso
11.714 + not (is_well_founded_inductive_pred hol_ctxt x) then
11.715 + let
11.716 + val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
11.717 + val (pref, connective, set_oper) =
11.718 + if gfp then
11.719 + (lbfp_prefix,
11.720 + @{const "op |"},
11.721 + @{const_name upper_semilattice_fun_inst.sup_fun})
11.722 + else
11.723 + (ubfp_prefix,
11.724 + @{const "op &"},
11.725 + @{const_name lower_semilattice_fun_inst.inf_fun})
11.726 + (* unit -> term *)
11.727 + fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
11.728 + |> aux ss Ts js depth polar
11.729 + fun neg () = Const (pref ^ s, T)
11.730 + in
11.731 + (case polar |> gfp ? flip_polarity of
11.732 + Pos => pos ()
11.733 + | Neg => neg ()
11.734 + | Neut =>
11.735 + if is_fun_type T then
11.736 + let
11.737 + val ((trunk_arg_Ts, rump_arg_T), body_T) =
11.738 + T |> strip_type |>> split_last
11.739 + val set_T = rump_arg_T --> body_T
11.740 + (* (unit -> term) -> term *)
11.741 + fun app f =
11.742 + list_comb (f (),
11.743 + map Bound (length trunk_arg_Ts - 1 downto 0))
11.744 + in
11.745 + List.foldr absdummy
11.746 + (Const (set_oper, set_T --> set_T --> set_T)
11.747 + $ app pos $ app neg) trunk_arg_Ts
11.748 + end
11.749 + else
11.750 + connective $ pos () $ neg ())
11.751 + end
11.752 + else
11.753 + Const x
11.754 + | t1 $ t2 =>
11.755 + betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
11.756 + aux ss Ts [] depth Neut t2)
11.757 + | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
11.758 + | _ => t
11.759 + end
11.760 + in aux [] [] [] 0 Pos end
11.761 +
11.762 +(** Function specialization **)
11.763 +
11.764 +(* term -> term list *)
11.765 +fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
11.766 + | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
11.767 + | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
11.768 + snd (strip_comb t1)
11.769 + | params_in_equation _ = []
11.770 +
11.771 +(* styp -> styp -> int list -> term list -> term list -> term -> term *)
11.772 +fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
11.773 + let
11.774 + val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
11.775 + + 1
11.776 + val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
11.777 + val fixed_params = filter_indices fixed_js (params_in_equation t)
11.778 + (* term list -> term -> term *)
11.779 + fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
11.780 + | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
11.781 + | aux args t =
11.782 + if t = Const x then
11.783 + list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
11.784 + else
11.785 + let val j = find_index (curry (op =) t) fixed_params in
11.786 + list_comb (if j >= 0 then nth fixed_args j else t, args)
11.787 + end
11.788 + in aux [] t end
11.789 +
11.790 +(* hol_context -> styp -> (int * term option) list *)
11.791 +fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =
11.792 + let
11.793 + (* term -> term list -> term list -> term list list *)
11.794 + fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
11.795 + | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
11.796 + | fun_calls t args =
11.797 + (case t of
11.798 + Const (x' as (s', T')) =>
11.799 + x = x' orelse (case AList.lookup (op =) ersatz_table s' of
11.800 + SOME s'' => x = (s'', T')
11.801 + | NONE => false)
11.802 + | _ => false) ? cons args
11.803 + (* term list list -> term list list -> term list -> term list list *)
11.804 + fun call_sets [] [] vs = [vs]
11.805 + | call_sets [] uss vs = vs :: call_sets uss [] []
11.806 + | call_sets ([] :: _) _ _ = []
11.807 + | call_sets ((t :: ts) :: tss) uss vs =
11.808 + OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
11.809 + val sets = call_sets (fun_calls t [] []) [] []
11.810 + val indexed_sets = sets ~~ (index_seq 0 (length sets))
11.811 + in
11.812 + fold_rev (fn (set, j) =>
11.813 + case set of
11.814 + [Var _] => AList.lookup (op =) indexed_sets set = SOME j
11.815 + ? cons (j, NONE)
11.816 + | [t as Const _] => cons (j, SOME t)
11.817 + | [t as Free _] => cons (j, SOME t)
11.818 + | _ => I) indexed_sets []
11.819 + end
11.820 +(* hol_context -> styp -> term list -> (int * term option) list *)
11.821 +fun static_args_in_terms hol_ctxt x =
11.822 + map (static_args_in_term hol_ctxt x)
11.823 + #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
11.824 +
11.825 +(* (int * term option) list -> (int * term) list -> int list *)
11.826 +fun overlapping_indices [] _ = []
11.827 + | overlapping_indices _ [] = []
11.828 + | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
11.829 + if j1 < j2 then overlapping_indices ps1' ps2
11.830 + else if j1 > j2 then overlapping_indices ps1 ps2'
11.831 + else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
11.832 +
11.833 +(* typ list -> term -> bool *)
11.834 +fun is_eligible_arg Ts t =
11.835 + let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
11.836 + null bad_Ts orelse
11.837 + (is_higher_order_type (fastype_of1 (Ts, t)) andalso
11.838 + forall (not o is_higher_order_type) bad_Ts)
11.839 + end
11.840 +
11.841 +(* int -> string *)
11.842 +fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
11.843 +
11.844 +(* If a constant's definition is picked up deeper than this threshold, we
11.845 + prevent excessive specialization by not specializing it. *)
11.846 +val special_max_depth = 20
11.847 +
11.848 +val bound_var_prefix = "b"
11.849 +
11.850 +(* hol_context -> int -> term -> term *)
11.851 +fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,
11.852 + special_funs, ...}) depth t =
11.853 + if not specialize orelse depth > special_max_depth then
11.854 + t
11.855 + else
11.856 + let
11.857 + val blacklist = if depth = 0 then []
11.858 + else case term_under_def t of Const x => [x] | _ => []
11.859 + (* term list -> typ list -> term -> term *)
11.860 + fun aux args Ts (Const (x as (s, T))) =
11.861 + ((if not (member (op =) blacklist x) andalso not (null args) andalso
11.862 + not (String.isPrefix special_prefix s) andalso
11.863 + is_equational_fun hol_ctxt x then
11.864 + let
11.865 + val eligible_args = filter (is_eligible_arg Ts o snd)
11.866 + (index_seq 0 (length args) ~~ args)
11.867 + val _ = not (null eligible_args) orelse raise SAME ()
11.868 + val old_axs = equational_fun_axioms hol_ctxt x
11.869 + |> map (destroy_existential_equalities thy)
11.870 + val static_params = static_args_in_terms hol_ctxt x old_axs
11.871 + val fixed_js = overlapping_indices static_params eligible_args
11.872 + val _ = not (null fixed_js) orelse raise SAME ()
11.873 + val fixed_args = filter_indices fixed_js args
11.874 + val vars = fold Term.add_vars fixed_args []
11.875 + |> sort (TermOrd.fast_indexname_ord o pairself fst)
11.876 + val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
11.877 + fixed_args []
11.878 + |> sort int_ord
11.879 + val live_args = filter_out_indices fixed_js args
11.880 + val extra_args = map Var vars @ map Bound bound_js @ live_args
11.881 + val extra_Ts = map snd vars @ filter_indices bound_js Ts
11.882 + val k = maxidx_of_term t + 1
11.883 + (* int -> term *)
11.884 + fun var_for_bound_no j =
11.885 + Var ((bound_var_prefix ^
11.886 + nat_subscript (find_index (curry (op =) j) bound_js
11.887 + + 1), k),
11.888 + nth Ts j)
11.889 + val fixed_args_in_axiom =
11.890 + map (curry subst_bounds
11.891 + (map var_for_bound_no (index_seq 0 (length Ts))))
11.892 + fixed_args
11.893 + in
11.894 + case AList.lookup (op =) (!special_funs)
11.895 + (x, fixed_js, fixed_args_in_axiom) of
11.896 + SOME x' => list_comb (Const x', extra_args)
11.897 + | NONE =>
11.898 + let
11.899 + val extra_args_in_axiom =
11.900 + map Var vars @ map var_for_bound_no bound_js
11.901 + val x' as (s', _) =
11.902 + (special_prefix_for (length (!special_funs) + 1) ^ s,
11.903 + extra_Ts @ filter_out_indices fixed_js (binder_types T)
11.904 + ---> body_type T)
11.905 + val new_axs =
11.906 + map (specialize_fun_axiom x x' fixed_js
11.907 + fixed_args_in_axiom extra_args_in_axiom) old_axs
11.908 + val _ =
11.909 + Unsynchronized.change special_funs
11.910 + (cons ((x, fixed_js, fixed_args_in_axiom), x'))
11.911 + val _ = add_simps simp_table s' new_axs
11.912 + in list_comb (Const x', extra_args) end
11.913 + end
11.914 + else
11.915 + raise SAME ())
11.916 + handle SAME () => list_comb (Const x, args))
11.917 + | aux args Ts (Abs (s, T, t)) =
11.918 + list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
11.919 + | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
11.920 + | aux args _ t = list_comb (t, args)
11.921 + in aux [] [] t end
11.922 +
11.923 +type special_triple = int list * term list * styp
11.924 +
11.925 +val cong_var_prefix = "c"
11.926 +
11.927 +(* styp -> special_triple -> special_triple -> term *)
11.928 +fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
11.929 + let
11.930 + val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
11.931 + val Ts = binder_types T
11.932 + val max_j = fold (fold Integer.max) [js1, js2] ~1
11.933 + val (eqs, (args1, args2)) =
11.934 + fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
11.935 + (js1 ~~ ts1, js2 ~~ ts2) of
11.936 + (SOME t1, SOME t2) => apfst (cons (t1, t2))
11.937 + | (SOME t1, NONE) => apsnd (apsnd (cons t1))
11.938 + | (NONE, SOME t2) => apsnd (apfst (cons t2))
11.939 + | (NONE, NONE) =>
11.940 + let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
11.941 + nth Ts j) in
11.942 + apsnd (pairself (cons v))
11.943 + end) (max_j downto 0) ([], ([], []))
11.944 + in
11.945 + Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
11.946 + |> map Logic.mk_equals,
11.947 + Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
11.948 + list_comb (Const x2, bounds2 @ args2)))
11.949 + |> Refute.close_form (* TODO: needed? *)
11.950 + end
11.951 +
11.952 +(* hol_context -> styp list -> term list *)
11.953 +fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
11.954 + let
11.955 + val groups =
11.956 + !special_funs
11.957 + |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
11.958 + |> AList.group (op =)
11.959 + |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
11.960 + |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
11.961 + (* special_triple -> int *)
11.962 + fun generality (js, _, _) = ~(length js)
11.963 + (* special_triple -> special_triple -> bool *)
11.964 + fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
11.965 + x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
11.966 + (j2 ~~ t2, j1 ~~ t1)
11.967 + (* styp -> special_triple list -> special_triple list -> special_triple list
11.968 + -> term list -> term list *)
11.969 + fun do_pass_1 _ [] [_] [_] = I
11.970 + | do_pass_1 x skipped _ [] = do_pass_2 x skipped
11.971 + | do_pass_1 x skipped all (z :: zs) =
11.972 + case filter (is_more_specific z) all
11.973 + |> sort (int_ord o pairself generality) of
11.974 + [] => do_pass_1 x (z :: skipped) all zs
11.975 + | (z' :: _) => cons (special_congruence_axiom x z z')
11.976 + #> do_pass_1 x skipped all zs
11.977 + (* styp -> special_triple list -> term list -> term list *)
11.978 + and do_pass_2 _ [] = I
11.979 + | do_pass_2 x (z :: zs) =
11.980 + fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
11.981 + in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
11.982 +
11.983 +(** Axiom selection **)
11.984 +
11.985 +(* Similar to "Refute.specialize_type" but returns all matches rather than only
11.986 + the first (preorder) match. *)
11.987 +(* theory -> styp -> term -> term list *)
11.988 +fun multi_specialize_type thy slack (x as (s, T)) t =
11.989 + let
11.990 + (* term -> (typ * term) list -> (typ * term) list *)
11.991 + fun aux (Const (s', T')) ys =
11.992 + if s = s' then
11.993 + ys |> (if AList.defined (op =) ys T' then
11.994 + I
11.995 + else
11.996 + cons (T', Refute.monomorphic_term
11.997 + (Sign.typ_match thy (T', T) Vartab.empty) t)
11.998 + handle Type.TYPE_MATCH => I
11.999 + | Refute.REFUTE _ =>
11.1000 + if slack then
11.1001 + I
11.1002 + else
11.1003 + raise NOT_SUPPORTED ("too much polymorphism in \
11.1004 + \axiom involving " ^ quote s))
11.1005 + else
11.1006 + ys
11.1007 + | aux _ ys = ys
11.1008 + in map snd (fold_aterms aux t []) end
11.1009 +
11.1010 +(* theory -> bool -> const_table -> styp -> term list *)
11.1011 +fun nondef_props_for_const thy slack table (x as (s, _)) =
11.1012 + these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
11.1013 +
11.1014 +(* 'a Symtab.table -> 'a list *)
11.1015 +fun all_table_entries table = Symtab.fold (append o snd) table []
11.1016 +(* const_table -> string -> const_table *)
11.1017 +fun extra_table table s = Symtab.make [(s, all_table_entries table)]
11.1018 +
11.1019 +(* int -> term -> term *)
11.1020 +fun eval_axiom_for_term j t =
11.1021 + Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
11.1022 +
11.1023 +(* term -> bool *)
11.1024 +val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
11.1025 +
11.1026 +(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
11.1027 +val axioms_max_depth = 255
11.1028 +
11.1029 +(* hol_context -> term -> (term list * term list) * (bool * bool) *)
11.1030 +fun axioms_for_term
11.1031 + (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
11.1032 + def_table, nondef_table, user_nondefs, ...}) t =
11.1033 + let
11.1034 + type accumulator = styp list * (term list * term list)
11.1035 + (* (term list * term list -> term list)
11.1036 + -> ((term list -> term list) -> term list * term list
11.1037 + -> term list * term list)
11.1038 + -> int -> term -> accumulator -> accumulator *)
11.1039 + fun add_axiom get app depth t (accum as (xs, axs)) =
11.1040 + let
11.1041 + val t = t |> unfold_defs_in_term hol_ctxt
11.1042 + |> skolemize_term_and_more hol_ctxt ~1
11.1043 + in
11.1044 + if is_trivial_equation t then
11.1045 + accum
11.1046 + else
11.1047 + let val t' = t |> specialize_consts_in_term hol_ctxt depth in
11.1048 + if exists (member (op aconv) (get axs)) [t, t'] then accum
11.1049 + else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
11.1050 + end
11.1051 + end
11.1052 + (* int -> term -> accumulator -> accumulator *)
11.1053 + and add_def_axiom depth = add_axiom fst apfst depth
11.1054 + and add_nondef_axiom depth = add_axiom snd apsnd depth
11.1055 + and add_maybe_def_axiom depth t =
11.1056 + (if head_of t <> @{const "==>"} then add_def_axiom
11.1057 + else add_nondef_axiom) depth t
11.1058 + and add_eq_axiom depth t =
11.1059 + (if is_constr_pattern_formula thy t then add_def_axiom
11.1060 + else add_nondef_axiom) depth t
11.1061 + (* int -> term -> accumulator -> accumulator *)
11.1062 + and add_axioms_for_term depth t (accum as (xs, axs)) =
11.1063 + case t of
11.1064 + t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
11.1065 + | Const (x as (s, T)) =>
11.1066 + (if member (op =) xs x orelse is_built_in_const fast_descrs x then
11.1067 + accum
11.1068 + else
11.1069 + let val accum as (xs, _) = (x :: xs, axs) in
11.1070 + if depth > axioms_max_depth then
11.1071 + raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
11.1072 + \add_axioms_for_term",
11.1073 + "too many nested axioms (" ^
11.1074 + string_of_int depth ^ ")")
11.1075 + else if Refute.is_const_of_class thy x then
11.1076 + let
11.1077 + val class = Logic.class_of_const s
11.1078 + val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
11.1079 + class)
11.1080 + val ax1 = try (Refute.specialize_type thy x) of_class
11.1081 + val ax2 = Option.map (Refute.specialize_type thy x o snd)
11.1082 + (Refute.get_classdef thy class)
11.1083 + in
11.1084 + fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
11.1085 + accum
11.1086 + end
11.1087 + else if is_constr thy x then
11.1088 + accum
11.1089 + else if is_equational_fun hol_ctxt x then
11.1090 + fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
11.1091 + accum
11.1092 + else if is_abs_fun thy x then
11.1093 + if is_quot_type thy (range_type T) then
11.1094 + raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
11.1095 + else
11.1096 + accum |> fold (add_nondef_axiom depth)
11.1097 + (nondef_props_for_const thy false nondef_table x)
11.1098 + |> is_funky_typedef thy (range_type T)
11.1099 + ? fold (add_maybe_def_axiom depth)
11.1100 + (nondef_props_for_const thy true
11.1101 + (extra_table def_table s) x)
11.1102 + else if is_rep_fun thy x then
11.1103 + if is_quot_type thy (domain_type T) then
11.1104 + raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
11.1105 + else
11.1106 + accum |> fold (add_nondef_axiom depth)
11.1107 + (nondef_props_for_const thy false nondef_table x)
11.1108 + |> is_funky_typedef thy (range_type T)
11.1109 + ? fold (add_maybe_def_axiom depth)
11.1110 + (nondef_props_for_const thy true
11.1111 + (extra_table def_table s) x)
11.1112 + |> add_axioms_for_term depth
11.1113 + (Const (mate_of_rep_fun thy x))
11.1114 + |> fold (add_def_axiom depth)
11.1115 + (inverse_axioms_for_rep_fun thy x)
11.1116 + else
11.1117 + accum |> user_axioms <> SOME false
11.1118 + ? fold (add_nondef_axiom depth)
11.1119 + (nondef_props_for_const thy false nondef_table x)
11.1120 + end)
11.1121 + |> add_axioms_for_type depth T
11.1122 + | Free (_, T) => add_axioms_for_type depth T accum
11.1123 + | Var (_, T) => add_axioms_for_type depth T accum
11.1124 + | Bound _ => accum
11.1125 + | Abs (_, T, t) => accum |> add_axioms_for_term depth t
11.1126 + |> add_axioms_for_type depth T
11.1127 + (* int -> typ -> accumulator -> accumulator *)
11.1128 + and add_axioms_for_type depth T =
11.1129 + case T of
11.1130 + Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
11.1131 + | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
11.1132 + | @{typ prop} => I
11.1133 + | @{typ bool} => I
11.1134 + | @{typ unit} => I
11.1135 + | TFree (_, S) => add_axioms_for_sort depth T S
11.1136 + | TVar (_, S) => add_axioms_for_sort depth T S
11.1137 + | Type (z as (s, Ts)) =>
11.1138 + fold (add_axioms_for_type depth) Ts
11.1139 + #> (if is_pure_typedef thy T then
11.1140 + fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
11.1141 + else if is_quot_type thy T then
11.1142 + fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
11.1143 + else if max_bisim_depth >= 0 andalso is_codatatype thy T then
11.1144 + fold (add_maybe_def_axiom depth)
11.1145 + (codatatype_bisim_axioms hol_ctxt T)
11.1146 + else
11.1147 + I)
11.1148 + (* int -> typ -> sort -> accumulator -> accumulator *)
11.1149 + and add_axioms_for_sort depth T S =
11.1150 + let
11.1151 + val supers = Sign.complete_sort thy S
11.1152 + val class_axioms =
11.1153 + maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
11.1154 + handle ERROR _ => [])) supers
11.1155 + val monomorphic_class_axioms =
11.1156 + map (fn t => case Term.add_tvars t [] of
11.1157 + [] => t
11.1158 + | [(x, S)] =>
11.1159 + Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
11.1160 + | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
11.1161 + \add_axioms_for_sort", [t]))
11.1162 + class_axioms
11.1163 + in fold (add_nondef_axiom depth) monomorphic_class_axioms end
11.1164 + val (mono_user_nondefs, poly_user_nondefs) =
11.1165 + List.partition (null o Term.hidden_polymorphism) user_nondefs
11.1166 + val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
11.1167 + evals
11.1168 + val (xs, (defs, nondefs)) =
11.1169 + ([], ([], [])) |> add_axioms_for_term 1 t
11.1170 + |> fold_rev (add_def_axiom 1) eval_axioms
11.1171 + |> user_axioms = SOME true
11.1172 + ? fold (add_nondef_axiom 1) mono_user_nondefs
11.1173 + val defs = defs @ special_congruence_axioms hol_ctxt xs
11.1174 + in
11.1175 + ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
11.1176 + null poly_user_nondefs))
11.1177 + end
11.1178 +
11.1179 +(** Simplification of constructor/selector terms **)
11.1180 +
11.1181 +(* theory -> term -> term *)
11.1182 +fun simplify_constrs_and_sels thy t =
11.1183 + let
11.1184 + (* term -> int -> term *)
11.1185 + fun is_nth_sel_on t' n (Const (s, _) $ t) =
11.1186 + (t = t' andalso is_sel_like_and_no_discr s andalso
11.1187 + sel_no_from_name s = n)
11.1188 + | is_nth_sel_on _ _ _ = false
11.1189 + (* term -> term list -> term *)
11.1190 + fun do_term (Const (@{const_name Rep_Frac}, _)
11.1191 + $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
11.1192 + | do_term (Const (@{const_name Abs_Frac}, _)
11.1193 + $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
11.1194 + | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
11.1195 + | do_term (t as Const (x as (s, T))) (args as _ :: _) =
11.1196 + ((if is_constr_like thy x then
11.1197 + if length args = num_binder_types T then
11.1198 + case hd args of
11.1199 + Const (x' as (_, T')) $ t' =>
11.1200 + if domain_type T' = body_type T andalso
11.1201 + forall (uncurry (is_nth_sel_on t'))
11.1202 + (index_seq 0 (length args) ~~ args) then
11.1203 + t'
11.1204 + else
11.1205 + raise SAME ()
11.1206 + | _ => raise SAME ()
11.1207 + else
11.1208 + raise SAME ()
11.1209 + else if is_sel_like_and_no_discr s then
11.1210 + case strip_comb (hd args) of
11.1211 + (Const (x' as (s', T')), ts') =>
11.1212 + if is_constr_like thy x' andalso
11.1213 + constr_name_for_sel_like s = s' andalso
11.1214 + not (exists is_pair_type (binder_types T')) then
11.1215 + list_comb (nth ts' (sel_no_from_name s), tl args)
11.1216 + else
11.1217 + raise SAME ()
11.1218 + | _ => raise SAME ()
11.1219 + else
11.1220 + raise SAME ())
11.1221 + handle SAME () => betapplys (t, args))
11.1222 + | do_term (Abs (s, T, t')) args =
11.1223 + betapplys (Abs (s, T, do_term t' []), args)
11.1224 + | do_term t args = betapplys (t, args)
11.1225 + in do_term t [] end
11.1226 +
11.1227 +(** Quantifier massaging: Distributing quantifiers **)
11.1228 +
11.1229 +(* term -> term *)
11.1230 +fun distribute_quantifiers t =
11.1231 + case t of
11.1232 + (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
11.1233 + (case t1 of
11.1234 + (t10 as @{const "op &"}) $ t11 $ t12 =>
11.1235 + t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
11.1236 + $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
11.1237 + | (t10 as @{const Not}) $ t11 =>
11.1238 + t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
11.1239 + $ Abs (s, T1, t11))
11.1240 + | t1 =>
11.1241 + if not (loose_bvar1 (t1, 0)) then
11.1242 + distribute_quantifiers (incr_boundvars ~1 t1)
11.1243 + else
11.1244 + t0 $ Abs (s, T1, distribute_quantifiers t1))
11.1245 + | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
11.1246 + (case distribute_quantifiers t1 of
11.1247 + (t10 as @{const "op |"}) $ t11 $ t12 =>
11.1248 + t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
11.1249 + $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
11.1250 + | (t10 as @{const "op -->"}) $ t11 $ t12 =>
11.1251 + t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
11.1252 + $ Abs (s, T1, t11))
11.1253 + $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
11.1254 + | (t10 as @{const Not}) $ t11 =>
11.1255 + t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
11.1256 + $ Abs (s, T1, t11))
11.1257 + | t1 =>
11.1258 + if not (loose_bvar1 (t1, 0)) then
11.1259 + distribute_quantifiers (incr_boundvars ~1 t1)
11.1260 + else
11.1261 + t0 $ Abs (s, T1, distribute_quantifiers t1))
11.1262 + | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
11.1263 + | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
11.1264 + | _ => t
11.1265 +
11.1266 +(** Quantifier massaging: Pushing quantifiers inward **)
11.1267 +
11.1268 +(* int -> int -> (int -> int) -> term -> term *)
11.1269 +fun renumber_bounds j n f t =
11.1270 + case t of
11.1271 + t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
11.1272 + | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
11.1273 + | Bound j' =>
11.1274 + Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
11.1275 + | _ => t
11.1276 +
11.1277 +(* Maximum number of quantifiers in a cluster for which the exponential
11.1278 + algorithm is used. Larger clusters use a heuristic inspired by Claessen &
11.1279 + Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
11.1280 + paper). *)
11.1281 +val quantifier_cluster_threshold = 7
11.1282 +
11.1283 +(* theory -> term -> term *)
11.1284 +fun push_quantifiers_inward thy =
11.1285 + let
11.1286 + (* string -> string list -> typ list -> term -> term *)
11.1287 + fun aux quant_s ss Ts t =
11.1288 + (case t of
11.1289 + (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
11.1290 + if s0 = quant_s then
11.1291 + aux s0 (s1 :: ss) (T1 :: Ts) t1
11.1292 + else if quant_s = "" andalso
11.1293 + (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
11.1294 + aux s0 [s1] [T1] t1
11.1295 + else
11.1296 + raise SAME ()
11.1297 + | _ => raise SAME ())
11.1298 + handle SAME () =>
11.1299 + case t of
11.1300 + t1 $ t2 =>
11.1301 + if quant_s = "" then
11.1302 + aux "" [] [] t1 $ aux "" [] [] t2
11.1303 + else
11.1304 + let
11.1305 + val typical_card = 4
11.1306 + (* ('a -> ''b list) -> 'a list -> ''b list *)
11.1307 + fun big_union proj ps =
11.1308 + fold (fold (insert (op =)) o proj) ps []
11.1309 + val (ts, connective) = strip_any_connective t
11.1310 + val T_costs =
11.1311 + map (bounded_card_of_type 65536 typical_card []) Ts
11.1312 + val t_costs = map size_of_term ts
11.1313 + val num_Ts = length Ts
11.1314 + (* int -> int *)
11.1315 + val flip = curry (op -) (num_Ts - 1)
11.1316 + val t_boundss = map (map flip o loose_bnos) ts
11.1317 + (* (int list * int) list -> int list
11.1318 + -> (int list * int) list *)
11.1319 + fun merge costly_boundss [] = costly_boundss
11.1320 + | merge costly_boundss (j :: js) =
11.1321 + let
11.1322 + val (yeas, nays) =
11.1323 + List.partition (fn (bounds, _) =>
11.1324 + member (op =) bounds j)
11.1325 + costly_boundss
11.1326 + val yeas_bounds = big_union fst yeas
11.1327 + val yeas_cost = Integer.sum (map snd yeas)
11.1328 + * nth T_costs j
11.1329 + in merge ((yeas_bounds, yeas_cost) :: nays) js end
11.1330 + (* (int list * int) list -> int list -> int *)
11.1331 + val cost = Integer.sum o map snd oo merge
11.1332 + (* (int list * int) list -> int list -> int list *)
11.1333 + fun heuristically_best_permutation _ [] = []
11.1334 + | heuristically_best_permutation costly_boundss js =
11.1335 + let
11.1336 + val (costly_boundss, (j, js)) =
11.1337 + js |> map (`(merge costly_boundss o single))
11.1338 + |> sort (int_ord
11.1339 + o pairself (Integer.sum o map snd o fst))
11.1340 + |> split_list |>> hd ||> pairf hd tl
11.1341 + in
11.1342 + j :: heuristically_best_permutation costly_boundss js
11.1343 + end
11.1344 + val js =
11.1345 + if length Ts <= quantifier_cluster_threshold then
11.1346 + all_permutations (index_seq 0 num_Ts)
11.1347 + |> map (`(cost (t_boundss ~~ t_costs)))
11.1348 + |> sort (int_ord o pairself fst) |> hd |> snd
11.1349 + else
11.1350 + heuristically_best_permutation (t_boundss ~~ t_costs)
11.1351 + (index_seq 0 num_Ts)
11.1352 + val back_js = map (fn j => find_index (curry (op =) j) js)
11.1353 + (index_seq 0 num_Ts)
11.1354 + val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
11.1355 + ts
11.1356 + (* (term * int list) list -> term *)
11.1357 + fun mk_connection [] =
11.1358 + raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\
11.1359 + \mk_connection", "")
11.1360 + | mk_connection ts_cum_bounds =
11.1361 + ts_cum_bounds |> map fst
11.1362 + |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
11.1363 + (* (term * int list) list -> int list -> term *)
11.1364 + fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
11.1365 + | build ts_cum_bounds (j :: js) =
11.1366 + let
11.1367 + val (yeas, nays) =
11.1368 + List.partition (fn (_, bounds) =>
11.1369 + member (op =) bounds j)
11.1370 + ts_cum_bounds
11.1371 + ||> map (apfst (incr_boundvars ~1))
11.1372 + in
11.1373 + if null yeas then
11.1374 + build nays js
11.1375 + else
11.1376 + let val T = nth Ts (flip j) in
11.1377 + build ((Const (quant_s, (T --> bool_T) --> bool_T)
11.1378 + $ Abs (nth ss (flip j), T,
11.1379 + mk_connection yeas),
11.1380 + big_union snd yeas) :: nays) js
11.1381 + end
11.1382 + end
11.1383 + in build (ts ~~ t_boundss) js end
11.1384 + | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
11.1385 + | _ => t
11.1386 + in aux "" [] [] end
11.1387 +
11.1388 +(** Preprocessor entry point **)
11.1389 +
11.1390 +(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
11.1391 +fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
11.1392 + skolemize, uncurry, ...}) t =
11.1393 + let
11.1394 + val skolem_depth = if skolemize then 4 else ~1
11.1395 + val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
11.1396 + core_t) = t |> unfold_defs_in_term hol_ctxt
11.1397 + |> Refute.close_form
11.1398 + |> skolemize_term_and_more hol_ctxt skolem_depth
11.1399 + |> specialize_consts_in_term hol_ctxt 0
11.1400 + |> `(axioms_for_term hol_ctxt)
11.1401 + val binarize =
11.1402 + case binary_ints of
11.1403 + SOME false => false
11.1404 + | _ =>
11.1405 + forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
11.1406 + (binary_ints = SOME true orelse
11.1407 + exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
11.1408 + val box = exists (not_equal (SOME false) o snd) boxes
11.1409 + val table =
11.1410 + Termtab.empty |> uncurry
11.1411 + ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
11.1412 + (* bool -> bool -> term -> term *)
11.1413 + fun do_rest def core =
11.1414 + binarize ? binarize_nat_and_int_in_term
11.1415 + #> uncurry ? uncurry_term table
11.1416 + #> box ? box_fun_and_pair_in_term hol_ctxt def
11.1417 + #> destroy_constrs ? (pull_out_universal_constrs thy def
11.1418 + #> pull_out_existential_constrs thy
11.1419 + #> destroy_pulled_out_constrs hol_ctxt def)
11.1420 + #> curry_assms
11.1421 + #> destroy_universal_equalities
11.1422 + #> destroy_existential_equalities thy
11.1423 + #> simplify_constrs_and_sels thy
11.1424 + #> distribute_quantifiers
11.1425 + #> push_quantifiers_inward thy
11.1426 + #> not core ? Refute.close_form
11.1427 + #> Term.map_abs_vars shortest_name
11.1428 + in
11.1429 + (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
11.1430 + (got_all_mono_user_axioms, no_poly_user_axioms)),
11.1431 + do_rest false true core_t)
11.1432 + end
11.1433 +
11.1434 +end;
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 04 14:45:08 2010 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 05 11:15:16 2010 +0100
12.3 @@ -8,7 +8,7 @@
12.4 signature NITPICK_SCOPE =
12.5 sig
12.6 type styp = Nitpick_Util.styp
12.7 - type extended_context = Nitpick_HOL.extended_context
12.8 + type hol_context = Nitpick_HOL.hol_context
12.9
12.10 type constr_spec = {
12.11 const: styp,
12.12 @@ -28,7 +28,7 @@
12.13 constrs: constr_spec list}
12.14
12.15 type scope = {
12.16 - ext_ctxt: extended_context,
12.17 + hol_ctxt: hol_context,
12.18 card_assigns: (typ * int) list,
12.19 bits: int,
12.20 bisim_depth: int,
12.21 @@ -47,7 +47,7 @@
12.22 val scopes_equivalent : scope -> scope -> bool
12.23 val scope_less_eq : scope -> scope -> bool
12.24 val all_scopes :
12.25 - extended_context -> int -> (typ option * int list) list
12.26 + hol_context -> int -> (typ option * int list) list
12.27 -> (styp option * int list) list -> (styp option * int list) list
12.28 -> int list -> int list -> typ list -> typ list -> typ list
12.29 -> int * scope list
12.30 @@ -77,7 +77,7 @@
12.31 constrs: constr_spec list}
12.32
12.33 type scope = {
12.34 - ext_ctxt: extended_context,
12.35 + hol_ctxt: hol_context,
12.36 card_assigns: (typ * int) list,
12.37 bits: int,
12.38 bisim_depth: int,
12.39 @@ -131,7 +131,7 @@
12.40
12.41 (* (string -> string) -> scope
12.42 -> string list * string list * string list * string list * string list *)
12.43 -fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
12.44 +fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
12.45 bits, bisim_depth, datatypes, ...} : scope) =
12.46 let
12.47 val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
12.48 @@ -240,10 +240,9 @@
12.49
12.50 val max_bits = 31 (* Kodkod limit *)
12.51
12.52 -(* extended_context -> (typ option * int list) list
12.53 - -> (styp option * int list) list -> (styp option * int list) list -> int list
12.54 - -> int list -> typ -> block *)
12.55 -fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns
12.56 +(* hol_context -> (typ option * int list) list -> (styp option * int list) list
12.57 + -> (styp option * int list) list -> int list -> int list -> typ -> block *)
12.58 +fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
12.59 iters_assigns bitss bisim_depths T =
12.60 if T = @{typ unsigned_bit} then
12.61 [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
12.62 @@ -261,18 +260,18 @@
12.63 (const_for_iterator_type T)))]
12.64 else
12.65 (Card T, lookup_type_ints_assign thy cards_assigns T) ::
12.66 - (case datatype_constrs ext_ctxt T of
12.67 + (case datatype_constrs hol_ctxt T of
12.68 [_] => []
12.69 | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
12.70
12.71 -(* extended_context -> (typ option * int list) list
12.72 - -> (styp option * int list) list -> (styp option * int list) list -> int list
12.73 - -> int list -> typ list -> typ list -> block list *)
12.74 -fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns bitss
12.75 +(* hol_context -> (typ option * int list) list -> (styp option * int list) list
12.76 + -> (styp option * int list) list -> int list -> int list -> typ list
12.77 + -> typ list -> block list *)
12.78 +fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
12.79 bisim_depths mono_Ts nonmono_Ts =
12.80 let
12.81 (* typ -> block *)
12.82 - val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns
12.83 + val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
12.84 iters_assigns bitss bisim_depths
12.85 val mono_block = maps block_for mono_Ts
12.86 val nonmono_blocks = map block_for nonmono_Ts
12.87 @@ -313,10 +312,10 @@
12.88
12.89 type scope_desc = (typ * int) list * (styp * int) list
12.90
12.91 -(* extended_context -> scope_desc -> typ * int -> bool *)
12.92 -fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns)
12.93 +(* hol_context -> scope_desc -> typ * int -> bool *)
12.94 +fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
12.95 (T, k) =
12.96 - case datatype_constrs ext_ctxt T of
12.97 + case datatype_constrs hol_ctxt T of
12.98 [] => false
12.99 | xs =>
12.100 let
12.101 @@ -329,20 +328,20 @@
12.102 | effective_max card max = Int.min (card, max)
12.103 val max = map2 effective_max dom_cards maxes |> Integer.sum
12.104 in max < k end
12.105 -(* extended_context -> (typ * int) list -> (typ * int) list
12.106 - -> (styp * int) list -> bool *)
12.107 -fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns =
12.108 - exists (is_surely_inconsistent_card_assign ext_ctxt
12.109 +(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
12.110 + -> bool *)
12.111 +fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
12.112 + exists (is_surely_inconsistent_card_assign hol_ctxt
12.113 (seen @ rest, max_assigns)) seen
12.114
12.115 -(* extended_context -> scope_desc -> (typ * int) list option *)
12.116 -fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
12.117 +(* hol_context -> scope_desc -> (typ * int) list option *)
12.118 +fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
12.119 let
12.120 (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
12.121 fun aux seen [] = SOME seen
12.122 | aux seen ((T, 0) :: _) = NONE
12.123 | aux seen ((T, k) :: rest) =
12.124 - (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen)
12.125 + (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
12.126 rest max_assigns then
12.127 raise SAME ()
12.128 else
12.129 @@ -374,12 +373,12 @@
12.130 (* block -> scope_desc *)
12.131 fun scope_descriptor_from_block block =
12.132 fold_rev add_row_to_scope_descriptor block ([], [])
12.133 -(* extended_context -> block list -> int list -> scope_desc option *)
12.134 -fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
12.135 +(* hol_context -> block list -> int list -> scope_desc option *)
12.136 +fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
12.137 let
12.138 val (card_assigns, max_assigns) =
12.139 maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
12.140 - val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns)
12.141 + val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
12.142 |> the
12.143 in
12.144 SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
12.145 @@ -427,15 +426,21 @@
12.146 {delta = delta, epsilon = delta, exclusive = true, total = false}
12.147 end
12.148 else if not co andalso num_self_recs > 0 then
12.149 - if not self_rec andalso num_non_self_recs = 1 andalso
12.150 - domain_card 2 card_assigns T = 1 then
12.151 - {delta = 0, epsilon = 1,
12.152 - exclusive = (s = @{const_name Nil} andalso length constrs = 2),
12.153 - total = true}
12.154 - else if s = @{const_name Cons} andalso length constrs = 2 then
12.155 - {delta = 1, epsilon = card, exclusive = true, total = false}
12.156 - else
12.157 - {delta = 0, epsilon = card, exclusive = false, total = false}
12.158 + (if num_self_recs = 1 andalso num_non_self_recs = 1 then
12.159 + if self_rec then
12.160 + case constrs of
12.161 + [{delta = 0, epsilon = 1, exclusive = true, ...}] =>
12.162 + {delta = 1, epsilon = card, exclusive = true, total = false}
12.163 + | _ => raise SAME ()
12.164 + else
12.165 + if domain_card 2 card_assigns T = 1 then
12.166 + {delta = 0, epsilon = 1, exclusive = true, total = true}
12.167 + else
12.168 + raise SAME ()
12.169 + else
12.170 + raise SAME ())
12.171 + handle SAME () =>
12.172 + {delta = 0, epsilon = card, exclusive = false, total = false}
12.173 else if card = sum_dom_cards (card + 1) then
12.174 let val delta = next_delta () in
12.175 {delta = delta, epsilon = delta + domain_card card card_assigns T,
12.176 @@ -449,31 +454,32 @@
12.177 explicit_max = max, total = total} :: constrs
12.178 end
12.179
12.180 -(* extended_context -> (typ * int) list -> typ -> bool *)
12.181 -fun has_exact_card ext_ctxt card_assigns T =
12.182 +(* hol_context -> (typ * int) list -> typ -> bool *)
12.183 +fun has_exact_card hol_ctxt card_assigns T =
12.184 let val card = card_of_type card_assigns T in
12.185 - card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T
12.186 + card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
12.187 end
12.188
12.189 -(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
12.190 -fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) deep_dataTs
12.191 +(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
12.192 +fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
12.193 (desc as (card_assigns, _)) (T, card) =
12.194 let
12.195 val deep = member (op =) deep_dataTs T
12.196 val co = is_codatatype thy T
12.197 - val xs = boxed_datatype_constrs ext_ctxt T
12.198 + val xs = boxed_datatype_constrs hol_ctxt T
12.199 val self_recs = map (is_self_recursive_constr_type o snd) xs
12.200 val (num_self_recs, num_non_self_recs) =
12.201 List.partition I self_recs |> pairself length
12.202 - val complete = has_exact_card ext_ctxt card_assigns T
12.203 + val complete = has_exact_card hol_ctxt card_assigns T
12.204 val concrete = xs |> maps (binder_types o snd) |> maps binder_types
12.205 - |> forall (has_exact_card ext_ctxt card_assigns)
12.206 + |> forall (has_exact_card hol_ctxt card_assigns)
12.207 (* int -> int *)
12.208 fun sum_dom_cards max =
12.209 map (domain_card max card_assigns o snd) xs |> Integer.sum
12.210 val constrs =
12.211 fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
12.212 - num_non_self_recs) (self_recs ~~ xs) []
12.213 + num_non_self_recs)
12.214 + (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
12.215 in
12.216 {typ = T, card = card, co = co, complete = complete, concrete = concrete,
12.217 deep = deep, constrs = constrs}
12.218 @@ -487,12 +493,12 @@
12.219 min_bits_for_nat_value (fold Integer.max
12.220 (map snd card_assigns @ map snd max_assigns) 0)
12.221
12.222 -(* extended_context -> int -> typ list -> scope_desc -> scope *)
12.223 -fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break deep_dataTs
12.224 +(* hol_context -> int -> typ list -> scope_desc -> scope *)
12.225 +fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
12.226 (desc as (card_assigns, _)) =
12.227 let
12.228 val datatypes =
12.229 - map (datatype_spec_from_scope_descriptor ext_ctxt deep_dataTs desc)
12.230 + map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
12.231 (filter (is_datatype thy o fst) card_assigns)
12.232 val bits = card_of_type card_assigns @{typ signed_bit} - 1
12.233 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
12.234 @@ -500,7 +506,7 @@
12.235 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
12.236 val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
12.237 in
12.238 - {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes,
12.239 + {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
12.240 bits = bits, bisim_depth = bisim_depth,
12.241 ofs = if sym_break <= 0 then Typtab.empty
12.242 else offset_table_for_card_assigns thy card_assigns datatypes}
12.243 @@ -521,26 +527,26 @@
12.244 val max_scopes = 4096
12.245 val distinct_threshold = 512
12.246
12.247 -(* extended_context -> int -> (typ option * int list) list
12.248 +(* hol_context -> int -> (typ option * int list) list
12.249 -> (styp option * int list) list -> (styp option * int list) list -> int list
12.250 -> typ list -> typ list -> typ list -> int * scope list *)
12.251 -fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
12.252 +fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
12.253 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
12.254 let
12.255 val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
12.256 cards_assigns
12.257 - val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns
12.258 + val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
12.259 iters_assigns bitss bisim_depths mono_Ts
12.260 nonmono_Ts
12.261 val ranks = map rank_of_block blocks
12.262 val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
12.263 val head = take max_scopes all
12.264 - val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
12.265 + val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
12.266 head
12.267 in
12.268 (length all - length head,
12.269 descs |> length descs <= distinct_threshold ? distinct (op =)
12.270 - |> map (scope_from_descriptor ext_ctxt sym_break deep_dataTs))
12.271 + |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
12.272 end
12.273
12.274 end;