1.1 --- a/src/HOL/IsaMakefile Thu Feb 04 13:36:52 2010 +0100
1.2 +++ b/src/HOL/IsaMakefile Thu Feb 04 16:03:15 2010 +0100
1.3 @@ -206,6 +206,7 @@
1.4 Tools/Nitpick/nitpick_mono.ML \
1.5 Tools/Nitpick/nitpick_nut.ML \
1.6 Tools/Nitpick/nitpick_peephole.ML \
1.7 + Tools/Nitpick/nitpick_preproc.ML \
1.8 Tools/Nitpick/nitpick_rep.ML \
1.9 Tools/Nitpick/nitpick_scope.ML \
1.10 Tools/Nitpick/nitpick_tests.ML \
2.1 --- a/src/HOL/Nitpick.thy Thu Feb 04 13:36:52 2010 +0100
2.2 +++ b/src/HOL/Nitpick.thy Thu Feb 04 16:03:15 2010 +0100
2.3 @@ -13,6 +13,7 @@
2.4 ("Tools/Nitpick/kodkod_sat.ML")
2.5 ("Tools/Nitpick/nitpick_util.ML")
2.6 ("Tools/Nitpick/nitpick_hol.ML")
2.7 + ("Tools/Nitpick/nitpick_preproc.ML")
2.8 ("Tools/Nitpick/nitpick_mono.ML")
2.9 ("Tools/Nitpick/nitpick_scope.ML")
2.10 ("Tools/Nitpick/nitpick_peephole.ML")
2.11 @@ -237,6 +238,7 @@
2.12 use "Tools/Nitpick/kodkod_sat.ML"
2.13 use "Tools/Nitpick/nitpick_util.ML"
2.14 use "Tools/Nitpick/nitpick_hol.ML"
2.15 +use "Tools/Nitpick/nitpick_preproc.ML"
2.16 use "Tools/Nitpick/nitpick_mono.ML"
2.17 use "Tools/Nitpick/nitpick_scope.ML"
2.18 use "Tools/Nitpick/nitpick_peephole.ML"
3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 04 13:36:52 2010 +0100
3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 04 16:03:15 2010 +0100
3.3 @@ -69,6 +69,7 @@
3.4
3.5 open Nitpick_Util
3.6 open Nitpick_HOL
3.7 +open Nitpick_Preproc
3.8 open Nitpick_Mono
3.9 open Nitpick_Scope
3.10 open Nitpick_Peephole
3.11 @@ -273,7 +274,7 @@
3.12 val intro_table = inductive_intro_table ctxt def_table
3.13 val ground_thm_table = ground_theorem_table thy
3.14 val ersatz_table = ersatz_table thy
3.15 - val (ext_ctxt as {wf_cache, ...}) =
3.16 + val (hol_ctxt as {wf_cache, ...}) =
3.17 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
3.18 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
3.19 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
3.20 @@ -292,7 +293,7 @@
3.21 val _ = null (Term.add_tvars assms_t []) orelse
3.22 raise NOT_SUPPORTED "schematic type variables"
3.23 val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
3.24 - core_t) = preprocess_term ext_ctxt assms_t
3.25 + core_t) = preprocess_term hol_ctxt assms_t
3.26 val got_all_user_axioms =
3.27 got_all_mono_user_axioms andalso no_poly_user_axioms
3.28
3.29 @@ -319,9 +320,9 @@
3.30 handle TYPE (_, Ts, ts) =>
3.31 raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
3.32
3.33 - val core_u = nut_from_term ext_ctxt Eq core_t
3.34 - val def_us = map (nut_from_term ext_ctxt DefEq) def_ts
3.35 - val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts
3.36 + val core_u = nut_from_term hol_ctxt Eq core_t
3.37 + val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
3.38 + val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
3.39 val (free_names, const_names) =
3.40 fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
3.41 val (sel_names, nonsel_names) =
3.42 @@ -344,12 +345,12 @@
3.43 case triple_lookup (type_match thy) monos T of
3.44 SOME (SOME b) => b
3.45 | _ => is_type_always_monotonic T orelse
3.46 - formulas_monotonic ext_ctxt T Plus def_ts nondef_ts core_t
3.47 + formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t
3.48 fun is_deep_datatype T =
3.49 is_datatype thy T andalso
3.50 (is_word_type T orelse
3.51 exists (curry (op =) T o domain_type o type_of) sel_names)
3.52 - val all_Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
3.53 + val all_Ts = ground_types_in_terms hol_ctxt (core_t :: def_ts @ nondef_ts)
3.54 |> sort TermOrd.typ_ord
3.55 val _ = if verbose andalso binary_ints = SOME true andalso
3.56 exists (member (op =) [nat_T, int_T]) all_Ts then
3.57 @@ -522,7 +523,7 @@
3.58 val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
3.59 val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
3.60 val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
3.61 - val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk
3.62 + val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk
3.63 rel_table datatypes
3.64 val declarative_axioms = plain_axioms @ dtype_axioms
3.65 val univ_card = univ_card nat_card int_card main_j0
3.66 @@ -553,7 +554,7 @@
3.67 if loc = "Nitpick_Kodkod.check_arity" andalso
3.68 not (Typtab.is_empty ofs) then
3.69 problem_for_scope liberal
3.70 - {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
3.71 + {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
3.72 bits = bits, bisim_depth = bisim_depth,
3.73 datatypes = datatypes, ofs = Typtab.empty}
3.74 else if loc = "Nitpick.pick_them_nits_in_term.\
3.75 @@ -891,7 +892,7 @@
3.76 end
3.77
3.78 val (skipped, the_scopes) =
3.79 - all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
3.80 + all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns
3.81 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
3.82 val _ = if skipped > 0 then
3.83 print_m (fn () => "Too many scopes. Skipping " ^
4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 04 13:36:52 2010 +0100
4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 04 16:03:15 2010 +0100
4.3 @@ -13,7 +13,7 @@
4.4 type unrolled = styp * styp
4.5 type wf_cache = (styp * (bool * bool)) list
4.6
4.7 - type extended_context = {
4.8 + type hol_context = {
4.9 thy: theory,
4.10 ctxt: Proof.context,
4.11 max_bisim_depth: int,
4.12 @@ -46,12 +46,24 @@
4.13 wf_cache: wf_cache Unsynchronized.ref,
4.14 constr_cache: (typ * styp list) list Unsynchronized.ref}
4.15
4.16 + datatype fixpoint_kind = Lfp | Gfp | NoFp
4.17 + datatype boxability =
4.18 + InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
4.19 +
4.20 val name_sep : string
4.21 val numeral_prefix : string
4.22 + val ubfp_prefix : string
4.23 + val lbfp_prefix : string
4.24 val skolem_prefix : string
4.25 + val special_prefix : string
4.26 + val uncurry_prefix : string
4.27 val eval_prefix : string
4.28 val original_name : string -> string
4.29 val s_conj : term * term -> term
4.30 + val s_disj : term * term -> term
4.31 + val strip_any_connective : term -> term list * term
4.32 + val conjuncts_of : term -> term list
4.33 + val disjuncts_of : term -> term list
4.34 val unbit_and_unbox_type : typ -> typ
4.35 val string_for_type : Proof.context -> typ -> string
4.36 val prefix_name : string -> string -> string
4.37 @@ -76,6 +88,7 @@
4.38 val is_record_type : typ -> bool
4.39 val is_number_type : theory -> typ -> bool
4.40 val const_for_iterator_type : typ -> styp
4.41 + val strip_n_binders : int -> typ -> typ list * typ
4.42 val nth_range_type : int -> typ -> typ
4.43 val num_factors_in_type : typ -> int
4.44 val num_binder_types : typ -> int
4.45 @@ -96,15 +109,18 @@
4.46 val is_rep_fun : theory -> styp -> bool
4.47 val is_quot_abs_fun : Proof.context -> styp -> bool
4.48 val is_quot_rep_fun : Proof.context -> styp -> bool
4.49 + val mate_of_rep_fun : theory -> styp -> styp
4.50 + val is_constr_like : theory -> styp -> bool
4.51 + val is_stale_constr : theory -> styp -> bool
4.52 val is_constr : theory -> styp -> bool
4.53 - val is_stale_constr : theory -> styp -> bool
4.54 val is_sel : string -> bool
4.55 val is_sel_like_and_no_discr : string -> bool
4.56 + val box_type : hol_context -> boxability -> typ -> typ
4.57 val discr_for_constr : styp -> styp
4.58 val num_sels_for_constr_type : typ -> int
4.59 val nth_sel_name_for_constr_name : string -> int -> string
4.60 val nth_sel_for_constr : styp -> int -> styp
4.61 - val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
4.62 + val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
4.63 val sel_no_from_name : string -> int
4.64 val eta_expand : typ list -> term -> int -> term
4.65 val extensionalize : term -> term
4.66 @@ -113,19 +129,25 @@
4.67 val unregister_frac_type : string -> theory -> theory
4.68 val register_codatatype : typ -> string -> styp list -> theory -> theory
4.69 val unregister_codatatype : typ -> theory -> theory
4.70 - val datatype_constrs : extended_context -> typ -> styp list
4.71 - val boxed_datatype_constrs : extended_context -> typ -> styp list
4.72 - val num_datatype_constrs : extended_context -> typ -> int
4.73 + val datatype_constrs : hol_context -> typ -> styp list
4.74 + val boxed_datatype_constrs : hol_context -> typ -> styp list
4.75 + val num_datatype_constrs : hol_context -> typ -> int
4.76 val constr_name_for_sel_like : string -> string
4.77 - val boxed_constr_for_sel : extended_context -> styp -> styp
4.78 + val boxed_constr_for_sel : hol_context -> styp -> styp
4.79 + val discriminate_value : hol_context -> styp -> term -> term
4.80 + val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
4.81 + val construct_value : theory -> styp -> term list -> term
4.82 val card_of_type : (typ * int) list -> typ -> int
4.83 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
4.84 val bounded_exact_card_of_type :
4.85 - extended_context -> int -> int -> (typ * int) list -> typ -> int
4.86 - val is_finite_type : extended_context -> typ -> bool
4.87 + hol_context -> int -> int -> (typ * int) list -> typ -> int
4.88 + val is_finite_type : hol_context -> typ -> bool
4.89 + val special_bounds : term list -> (indexname * typ) list
4.90 + val is_funky_typedef : theory -> typ -> bool
4.91 val all_axioms_of : theory -> term list * term list * term list
4.92 val arity_of_built_in_const : bool -> styp -> int option
4.93 val is_built_in_const : bool -> styp -> bool
4.94 + val term_under_def : term -> term
4.95 val case_const_names : theory -> (string * int) list
4.96 val const_def_table : Proof.context -> term list -> const_table
4.97 val const_nondef_table : term list -> const_table
4.98 @@ -134,22 +156,33 @@
4.99 val inductive_intro_table : Proof.context -> const_table -> const_table
4.100 val ground_theorem_table : theory -> term list Inttab.table
4.101 val ersatz_table : theory -> (string * string) list
4.102 + val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
4.103 + val inverse_axioms_for_rep_fun : theory -> styp -> term list
4.104 + val optimized_typedef_axioms : theory -> string * typ list -> term list
4.105 + val optimized_quot_type_axioms : theory -> string * typ list -> term list
4.106 val def_of_const : theory -> const_table -> styp -> term option
4.107 - val is_inductive_pred : extended_context -> styp -> bool
4.108 + val fixpoint_kind_of_const :
4.109 + theory -> const_table -> string * typ -> fixpoint_kind
4.110 + val is_inductive_pred : hol_context -> styp -> bool
4.111 + val is_equational_fun : hol_context -> styp -> bool
4.112 val is_constr_pattern_lhs : theory -> term -> bool
4.113 val is_constr_pattern_formula : theory -> term -> bool
4.114 + val unfold_defs_in_term : hol_context -> term -> term
4.115 + val codatatype_bisim_axioms : hol_context -> typ -> term list
4.116 + val is_well_founded_inductive_pred : hol_context -> styp -> bool
4.117 + val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
4.118 + val equational_fun_axioms : hol_context -> styp -> term list
4.119 + val is_equational_fun_surely_complete : hol_context -> styp -> bool
4.120 val merge_type_vars_in_terms : term list -> term list
4.121 - val ground_types_in_type : extended_context -> typ -> typ list
4.122 - val ground_types_in_terms : extended_context -> term list -> typ list
4.123 + val ground_types_in_type : hol_context -> typ -> typ list
4.124 + val ground_types_in_terms : hol_context -> term list -> typ list
4.125 val format_type : int list -> int list -> typ -> typ
4.126 val format_term_type :
4.127 theory -> const_table -> (term option * int list) list -> term -> typ
4.128 val user_friendly_const :
4.129 - extended_context -> string * string -> (term option * int list) list
4.130 + hol_context -> string * string -> (term option * int list) list
4.131 -> styp -> term * typ
4.132 val assign_operator_for_const : styp -> string
4.133 - val preprocess_term :
4.134 - extended_context -> term -> ((term list * term list) * (bool * bool)) * term
4.135 end;
4.136
4.137 structure Nitpick_HOL : NITPICK_HOL =
4.138 @@ -162,7 +195,7 @@
4.139 type unrolled = styp * styp
4.140 type wf_cache = (styp * (bool * bool)) list
4.141
4.142 -type extended_context = {
4.143 +type hol_context = {
4.144 thy: theory,
4.145 ctxt: Proof.context,
4.146 max_bisim_depth: int,
4.147 @@ -195,6 +228,10 @@
4.148 wf_cache: wf_cache Unsynchronized.ref,
4.149 constr_cache: (typ * styp list) list Unsynchronized.ref}
4.150
4.151 +datatype fixpoint_kind = Lfp | Gfp | NoFp
4.152 +datatype boxability =
4.153 + InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
4.154 +
4.155 structure Data = Theory_Data(
4.156 type T = {frac_types: (string * (string * string) list) list,
4.157 codatatypes: (string * (string * styp list)) list}
4.158 @@ -222,20 +259,11 @@
4.159 val special_prefix = nitpick_prefix ^ "sp"
4.160 val uncurry_prefix = nitpick_prefix ^ "unc"
4.161 val eval_prefix = nitpick_prefix ^ "eval"
4.162 -val bound_var_prefix = "b"
4.163 -val cong_var_prefix = "c"
4.164 val iter_var_prefix = "i"
4.165 -val val_var_prefix = nitpick_prefix ^ "v"
4.166 val arg_var_prefix = "x"
4.167
4.168 (* int -> string *)
4.169 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
4.170 -fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
4.171 -(* int -> int -> string *)
4.172 -fun skolem_prefix_for k j =
4.173 - skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
4.174 -fun uncurry_prefix_for k j =
4.175 - uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
4.176
4.177 (* string -> string * string *)
4.178 val strip_first_name_sep =
4.179 @@ -260,9 +288,6 @@
4.180 | s_disj (t1, t2) =
4.181 if t1 = @{const True} orelse t2 = @{const True} then @{const True}
4.182 else HOLogic.mk_disj (t1, t2)
4.183 -(* term -> term -> term *)
4.184 -fun mk_exists v t =
4.185 - HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
4.186
4.187 (* term -> term -> term list *)
4.188 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
4.189 @@ -276,8 +301,8 @@
4.190 ([t], @{const Not})
4.191 | strip_any_connective t = ([t], @{const Not})
4.192 (* term -> term list *)
4.193 -val conjuncts = strip_connective @{const "op &"}
4.194 -val disjuncts = strip_connective @{const "op |"}
4.195 +val conjuncts_of = strip_connective @{const "op &"}
4.196 +val disjuncts_of = strip_connective @{const "op |"}
4.197
4.198 (* When you add constants to these lists, make sure to handle them in
4.199 "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
4.200 @@ -373,8 +398,6 @@
4.201 fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
4.202 (* string -> term -> term *)
4.203 val prefix_abs_vars = Term.map_abs_vars o prefix_name
4.204 -(* term -> term *)
4.205 -val shorten_abs_vars = Term.map_abs_vars shortest_name
4.206 (* string -> string *)
4.207 fun short_name s =
4.208 case space_explode name_sep s of
4.209 @@ -441,7 +464,7 @@
4.210 | const_for_iterator_type T =
4.211 raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
4.212
4.213 -(* int -> typ -> typ * typ *)
4.214 +(* int -> typ -> typ list * typ *)
4.215 fun strip_n_binders 0 T = ([], T)
4.216 | strip_n_binders n (Type ("fun", [T1, T2])) =
4.217 strip_n_binders (n - 1) T2 |>> cons T1
4.218 @@ -552,7 +575,7 @@
4.219 val is_real_datatype = is_some oo Datatype.get_info
4.220 (* theory -> typ -> bool *)
4.221 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
4.222 - | is_quot_type _ (Type ("FSet.fset", _)) = true (* FIXME *)
4.223 + | is_quot_type _ (Type ("FSet.fset", _)) = true
4.224 | is_quot_type _ _ = false
4.225 fun is_codatatype thy (T as Type (s, _)) =
4.226 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
4.227 @@ -619,11 +642,11 @@
4.228 | NONE => false)
4.229 | is_rep_fun _ _ = false
4.230 (* Proof.context -> styp -> bool *)
4.231 -fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *)
4.232 - | is_quot_abs_fun _ ("FSet.abs_fset", _) = true (* FIXME *)
4.233 +fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true
4.234 + | is_quot_abs_fun _ ("FSet.abs_fset", _) = true
4.235 | is_quot_abs_fun _ _ = false
4.236 -fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *)
4.237 - | is_quot_rep_fun _ ("FSet.rep_fset", _) = true (* FIXME *)
4.238 +fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true
4.239 + | is_quot_rep_fun _ ("FSet.rep_fset", _) = true
4.240 | is_quot_rep_fun _ _ = false
4.241
4.242 (* theory -> styp -> styp *)
4.243 @@ -682,9 +705,6 @@
4.244 String.isPrefix sel_prefix
4.245 orf (member (op =) [@{const_name fst}, @{const_name snd}])
4.246
4.247 -datatype boxability =
4.248 - InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
4.249 -
4.250 (* boxability -> boxability *)
4.251 fun in_fun_lhs_for InConstr = InSel
4.252 | in_fun_lhs_for _ = InFunLHS
4.253 @@ -693,8 +713,8 @@
4.254 | in_fun_rhs_for InFunRHS1 = InFunRHS2
4.255 | in_fun_rhs_for _ = InFunRHS1
4.256
4.257 -(* extended_context -> boxability -> typ -> bool *)
4.258 -fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
4.259 +(* hol_context -> boxability -> typ -> bool *)
4.260 +fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
4.261 case T of
4.262 Type ("fun", _) =>
4.263 (boxy = InPair orelse boxy = InFunLHS) andalso
4.264 @@ -702,31 +722,31 @@
4.265 | Type ("*", Ts) =>
4.266 boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
4.267 ((boxy = InExpr orelse boxy = InFunLHS) andalso
4.268 - exists (is_boxing_worth_it ext_ctxt InPair)
4.269 - (map (box_type ext_ctxt InPair) Ts))
4.270 + exists (is_boxing_worth_it hol_ctxt InPair)
4.271 + (map (box_type hol_ctxt InPair) Ts))
4.272 | _ => false
4.273 -(* extended_context -> boxability -> string * typ list -> string *)
4.274 -and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
4.275 +(* hol_context -> boxability -> string * typ list -> string *)
4.276 +and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
4.277 case triple_lookup (type_match thy) boxes (Type z) of
4.278 SOME (SOME box_me) => box_me
4.279 - | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
4.280 -(* extended_context -> boxability -> typ -> typ *)
4.281 -and box_type ext_ctxt boxy T =
4.282 + | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
4.283 +(* hol_context -> boxability -> typ -> typ *)
4.284 +and box_type hol_ctxt boxy T =
4.285 case T of
4.286 Type (z as ("fun", [T1, T2])) =>
4.287 if boxy <> InConstr andalso boxy <> InSel andalso
4.288 - should_box_type ext_ctxt boxy z then
4.289 + should_box_type hol_ctxt boxy z then
4.290 Type (@{type_name fun_box},
4.291 - [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
4.292 + [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
4.293 else
4.294 - box_type ext_ctxt (in_fun_lhs_for boxy) T1
4.295 - --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
4.296 + box_type hol_ctxt (in_fun_lhs_for boxy) T1
4.297 + --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
4.298 | Type (z as ("*", Ts)) =>
4.299 if boxy <> InConstr andalso boxy <> InSel
4.300 - andalso should_box_type ext_ctxt boxy z then
4.301 - Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
4.302 + andalso should_box_type hol_ctxt boxy z then
4.303 + Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
4.304 else
4.305 - Type ("*", map (box_type ext_ctxt
4.306 + Type ("*", map (box_type hol_ctxt
4.307 (if boxy = InConstr orelse boxy = InSel then boxy
4.308 else InPair)) Ts)
4.309 | _ => T
4.310 @@ -747,9 +767,9 @@
4.311 | nth_sel_for_constr (s, T) n =
4.312 (nth_sel_name_for_constr_name s n,
4.313 body_type T --> nth (maybe_curried_binder_types T) n)
4.314 -(* extended_context -> styp -> int -> styp *)
4.315 -fun boxed_nth_sel_for_constr ext_ctxt =
4.316 - apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr
4.317 +(* hol_context -> styp -> int -> styp *)
4.318 +fun boxed_nth_sel_for_constr hol_ctxt =
4.319 + apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr
4.320
4.321 (* string -> int *)
4.322 fun sel_no_from_name s =
4.323 @@ -791,8 +811,8 @@
4.324 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
4.325 fun suc_const T = Const (@{const_name Suc}, T --> T)
4.326
4.327 -(* extended_context -> typ -> styp list *)
4.328 -fun uncached_datatype_constrs ({thy, stds, ...} : extended_context)
4.329 +(* hol_context -> typ -> styp list *)
4.330 +fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
4.331 (T as Type (s, Ts)) =
4.332 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
4.333 SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
4.334 @@ -829,49 +849,49 @@
4.335 else
4.336 [])
4.337 | uncached_datatype_constrs _ _ = []
4.338 -(* extended_context -> typ -> styp list *)
4.339 -fun datatype_constrs (ext_ctxt as {constr_cache, ...}) T =
4.340 +(* hol_context -> typ -> styp list *)
4.341 +fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
4.342 case AList.lookup (op =) (!constr_cache) T of
4.343 SOME xs => xs
4.344 | NONE =>
4.345 - let val xs = uncached_datatype_constrs ext_ctxt T in
4.346 + let val xs = uncached_datatype_constrs hol_ctxt T in
4.347 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
4.348 end
4.349 -fun boxed_datatype_constrs ext_ctxt =
4.350 - map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
4.351 -(* extended_context -> typ -> int *)
4.352 +fun boxed_datatype_constrs hol_ctxt =
4.353 + map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
4.354 +(* hol_context -> typ -> int *)
4.355 val num_datatype_constrs = length oo datatype_constrs
4.356
4.357 (* string -> string *)
4.358 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
4.359 | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
4.360 | constr_name_for_sel_like s' = original_name s'
4.361 -(* extended_context -> styp -> styp *)
4.362 -fun boxed_constr_for_sel ext_ctxt (s', T') =
4.363 +(* hol_context -> styp -> styp *)
4.364 +fun boxed_constr_for_sel hol_ctxt (s', T') =
4.365 let val s = constr_name_for_sel_like s' in
4.366 - AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
4.367 + AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s
4.368 |> the |> pair s
4.369 end
4.370
4.371 -(* extended_context -> styp -> term *)
4.372 -fun discr_term_for_constr ext_ctxt (x as (s, T)) =
4.373 +(* hol_context -> styp -> term *)
4.374 +fun discr_term_for_constr hol_ctxt (x as (s, T)) =
4.375 let val dataT = body_type T in
4.376 if s = @{const_name Suc} then
4.377 Abs (Name.uu, dataT,
4.378 @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
4.379 - else if num_datatype_constrs ext_ctxt dataT >= 2 then
4.380 + else if num_datatype_constrs hol_ctxt dataT >= 2 then
4.381 Const (discr_for_constr x)
4.382 else
4.383 Abs (Name.uu, dataT, @{const True})
4.384 end
4.385 -(* extended_context -> styp -> term -> term *)
4.386 -fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
4.387 +(* hol_context -> styp -> term -> term *)
4.388 +fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t =
4.389 case strip_comb t of
4.390 (Const x', args) =>
4.391 if x = x' then @{const True}
4.392 else if is_constr_like thy x' then @{const False}
4.393 - else betapply (discr_term_for_constr ext_ctxt x, t)
4.394 - | _ => betapply (discr_term_for_constr ext_ctxt x, t)
4.395 + else betapply (discr_term_for_constr hol_ctxt x, t)
4.396 + | _ => betapply (discr_term_for_constr hol_ctxt x, t)
4.397
4.398 (* styp -> term -> term *)
4.399 fun nth_arg_sel_term_for_constr (x as (s, T)) n =
4.400 @@ -920,26 +940,6 @@
4.401 | _ => list_comb (Const x, args)
4.402 end
4.403
4.404 -(* extended_context -> typ -> term -> term *)
4.405 -fun constr_expand (ext_ctxt as {thy, ...}) T t =
4.406 - (case head_of t of
4.407 - Const x => if is_constr_like thy x then t else raise SAME ()
4.408 - | _ => raise SAME ())
4.409 - handle SAME () =>
4.410 - let
4.411 - val x' as (_, T') =
4.412 - if is_pair_type T then
4.413 - let val (T1, T2) = HOLogic.dest_prodT T in
4.414 - (@{const_name Pair}, T1 --> T2 --> T)
4.415 - end
4.416 - else
4.417 - datatype_constrs ext_ctxt T |> hd
4.418 - val arg_Ts = binder_types T'
4.419 - in
4.420 - list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
4.421 - (index_seq 0 (length arg_Ts)) arg_Ts)
4.422 - end
4.423 -
4.424 (* (typ * int) list -> typ -> int *)
4.425 fun card_of_type assigns (Type ("fun", [T1, T2])) =
4.426 reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
4.427 @@ -975,8 +975,8 @@
4.428 card_of_type assigns T
4.429 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
4.430 default_card)
4.431 -(* extended_context -> int -> (typ * int) list -> typ -> int *)
4.432 -fun bounded_exact_card_of_type ext_ctxt max default_card assigns T =
4.433 +(* hol_context -> int -> (typ * int) list -> typ -> int *)
4.434 +fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
4.435 let
4.436 (* typ list -> typ -> int *)
4.437 fun aux avoid T =
4.438 @@ -1006,13 +1006,13 @@
4.439 | @{typ bool} => 2
4.440 | @{typ unit} => 1
4.441 | Type _ =>
4.442 - (case datatype_constrs ext_ctxt T of
4.443 + (case datatype_constrs hol_ctxt T of
4.444 [] => if is_integer_type T orelse is_bit_type T then 0
4.445 else raise SAME ()
4.446 | constrs =>
4.447 let
4.448 val constr_cards =
4.449 - datatype_constrs ext_ctxt T
4.450 + datatype_constrs hol_ctxt T
4.451 |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
4.452 o snd)
4.453 in
4.454 @@ -1024,9 +1024,9 @@
4.455 AList.lookup (op =) assigns T |> the_default default_card
4.456 in Int.min (max, aux [] T) end
4.457
4.458 -(* extended_context -> typ -> bool *)
4.459 -fun is_finite_type ext_ctxt =
4.460 - not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 []
4.461 +(* hol_context -> typ -> bool *)
4.462 +fun is_finite_type hol_ctxt =
4.463 + not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
4.464
4.465 (* term -> bool *)
4.466 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
4.467 @@ -1052,7 +1052,7 @@
4.468 member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
4.469 @{type_name int}] s orelse
4.470 is_frac_type thy (Type (s, []))
4.471 -(* theory -> term -> bool *)
4.472 +(* theory -> typ -> bool *)
4.473 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
4.474 | is_funky_typedef _ _ = false
4.475 (* term -> bool *)
4.476 @@ -1199,8 +1199,6 @@
4.477 |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
4.478 handle List.Empty => NONE
4.479
4.480 -datatype fixpoint_kind = Lfp | Gfp | NoFp
4.481 -
4.482 (* term -> fixpoint_kind *)
4.483 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
4.484 | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
4.485 @@ -1299,35 +1297,6 @@
4.486 Unsynchronized.change simp_table
4.487 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
4.488
4.489 -(* Similar to "Refute.specialize_type" but returns all matches rather than only
4.490 - the first (preorder) match. *)
4.491 -(* theory -> styp -> term -> term list *)
4.492 -fun multi_specialize_type thy slack (x as (s, T)) t =
4.493 - let
4.494 - (* term -> (typ * term) list -> (typ * term) list *)
4.495 - fun aux (Const (s', T')) ys =
4.496 - if s = s' then
4.497 - ys |> (if AList.defined (op =) ys T' then
4.498 - I
4.499 - else
4.500 - cons (T', Refute.monomorphic_term
4.501 - (Sign.typ_match thy (T', T) Vartab.empty) t)
4.502 - handle Type.TYPE_MATCH => I
4.503 - | Refute.REFUTE _ =>
4.504 - if slack then
4.505 - I
4.506 - else
4.507 - raise NOT_SUPPORTED ("too much polymorphism in \
4.508 - \axiom involving " ^ quote s))
4.509 - else
4.510 - ys
4.511 - | aux _ ys = ys
4.512 - in map snd (fold_aterms aux t []) end
4.513 -
4.514 -(* theory -> bool -> const_table -> styp -> term list *)
4.515 -fun nondef_props_for_const thy slack table (x as (s, _)) =
4.516 - these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
4.517 -
4.518 (* theory -> styp -> term list *)
4.519 fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
4.520 let val abs_T = domain_type T in
4.521 @@ -1336,7 +1305,7 @@
4.522 |> pairself (Refute.specialize_type thy x o prop_of o the)
4.523 ||> single |> op ::
4.524 end
4.525 -(* theory -> styp list -> term list *)
4.526 +(* theory -> string * typ list -> term list *)
4.527 fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
4.528 let val abs_T = Type abs_z in
4.529 if is_univ_typedef thy abs_T then
4.530 @@ -1392,15 +1361,15 @@
4.531 list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
4.532 (index_seq 0 (length arg_Ts)) arg_Ts)
4.533 end
4.534 -(* extended_context -> typ -> int * styp -> term -> term *)
4.535 -fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
4.536 +(* hol_context -> typ -> int * styp -> term -> term *)
4.537 +fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t =
4.538 Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
4.539 - $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
4.540 + $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x)
4.541 $ res_t
4.542 -(* extended_context -> typ -> typ -> term *)
4.543 -fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
4.544 +(* hol_context -> typ -> typ -> term *)
4.545 +fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
4.546 let
4.547 - val xs = datatype_constrs ext_ctxt dataT
4.548 + val xs = datatype_constrs hol_ctxt dataT
4.549 val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
4.550 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
4.551 in
4.552 @@ -1409,19 +1378,19 @@
4.553 val (xs'', x) = split_last xs'
4.554 in
4.555 constr_case_body thy (1, x)
4.556 - |> fold_rev (add_constr_case ext_ctxt res_T)
4.557 + |> fold_rev (add_constr_case hol_ctxt res_T)
4.558 (length xs' downto 2 ~~ xs'')
4.559 end
4.560 else
4.561 Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
4.562 - |> fold_rev (add_constr_case ext_ctxt res_T)
4.563 + |> fold_rev (add_constr_case hol_ctxt res_T)
4.564 (length xs' downto 1 ~~ xs'))
4.565 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
4.566 end
4.567
4.568 -(* extended_context -> string -> typ -> typ -> term -> term *)
4.569 -fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
4.570 - let val constr_x = hd (datatype_constrs ext_ctxt rec_T) in
4.571 +(* hol_context -> string -> typ -> typ -> term -> term *)
4.572 +fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t =
4.573 + let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
4.574 case no_of_record_field thy s rec_T of
4.575 ~1 => (case rec_T of
4.576 Type (_, Ts as _ :: _) =>
4.577 @@ -1430,16 +1399,16 @@
4.578 val j = num_record_fields thy rec_T - 1
4.579 in
4.580 select_nth_constr_arg thy constr_x t j res_T
4.581 - |> optimized_record_get ext_ctxt s rec_T' res_T
4.582 + |> optimized_record_get hol_ctxt s rec_T' res_T
4.583 end
4.584 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
4.585 []))
4.586 | j => select_nth_constr_arg thy constr_x t j res_T
4.587 end
4.588 -(* extended_context -> string -> typ -> term -> term -> term *)
4.589 -fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
4.590 +(* hol_context -> string -> typ -> term -> term -> term *)
4.591 +fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t =
4.592 let
4.593 - val constr_x as (_, constr_T) = hd (datatype_constrs ext_ctxt rec_T)
4.594 + val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
4.595 val Ts = binder_types constr_T
4.596 val n = length Ts
4.597 val special_j = no_of_record_field thy s rec_T
4.598 @@ -1450,7 +1419,7 @@
4.599 if j = special_j then
4.600 betapply (fun_t, t)
4.601 else if j = n - 1 andalso special_j = ~1 then
4.602 - optimized_record_update ext_ctxt s
4.603 + optimized_record_update hol_ctxt s
4.604 (rec_T |> dest_Type |> snd |> List.last) fun_t t
4.605 else
4.606 t
4.607 @@ -1473,19 +1442,19 @@
4.608 fixpoint_kind_of_rhs (the (def_of_const thy table x))
4.609 handle Option.Option => NoFp
4.610
4.611 -(* extended_context -> styp -> bool *)
4.612 +(* hol_context -> styp -> bool *)
4.613 fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
4.614 - : extended_context) x =
4.615 + : hol_context) x =
4.616 not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
4.617 fixpoint_kind_of_const thy def_table x <> NoFp
4.618 fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
4.619 - : extended_context) x =
4.620 + : hol_context) x =
4.621 exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
4.622 [!simp_table, psimp_table]
4.623 -fun is_inductive_pred ext_ctxt =
4.624 - is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
4.625 -fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
4.626 - (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
4.627 +fun is_inductive_pred hol_ctxt =
4.628 + is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
4.629 +fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
4.630 + (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
4.631 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
4.632 andf (not o has_trivial_definition thy def_table)
4.633
4.634 @@ -1522,11 +1491,11 @@
4.635 SOME t' => is_constr_pattern_lhs thy t'
4.636 | NONE => false
4.637
4.638 +(* Prevents divergence in case of cyclic or infinite definition dependencies. *)
4.639 val unfold_max_depth = 255
4.640 -val axioms_max_depth = 255
4.641
4.642 -(* extended_context -> term -> term *)
4.643 -fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
4.644 +(* hol_context -> term -> term *)
4.645 +fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs,
4.646 case_names, def_table, ground_thm_table,
4.647 ersatz_table, ...}) =
4.648 let
4.649 @@ -1600,7 +1569,7 @@
4.650 val (dataT, res_T) = nth_range_type n T
4.651 |> pairf domain_type range_type
4.652 in
4.653 - (optimized_case_def ext_ctxt dataT res_T
4.654 + (optimized_case_def hol_ctxt dataT res_T
4.655 |> do_term (depth + 1) Ts, ts)
4.656 end
4.657 | _ =>
4.658 @@ -1628,11 +1597,11 @@
4.659 else if is_record_get thy x then
4.660 case length ts of
4.661 0 => (do_term depth Ts (eta_expand Ts t 1), [])
4.662 - | _ => (optimized_record_get ext_ctxt s (domain_type T)
4.663 + | _ => (optimized_record_get hol_ctxt s (domain_type T)
4.664 (range_type T) (do_term depth Ts (hd ts)), tl ts)
4.665 else if is_record_update thy x then
4.666 case length ts of
4.667 - 2 => (optimized_record_update ext_ctxt
4.668 + 2 => (optimized_record_update hol_ctxt
4.669 (unsuffix Record.updateN s) (nth_range_type 2 T)
4.670 (do_term depth Ts (hd ts))
4.671 (do_term depth Ts (nth ts 1)), [])
4.672 @@ -1645,7 +1614,7 @@
4.673 else
4.674 (Const x, ts)
4.675 end
4.676 - else if is_equational_fun ext_ctxt x then
4.677 + else if is_equational_fun hol_ctxt x then
4.678 (Const x, ts)
4.679 else case def_of_const thy def_table x of
4.680 SOME def =>
4.681 @@ -1662,10 +1631,10 @@
4.682 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
4.683 in do_term 0 [] end
4.684
4.685 -(* extended_context -> typ -> term list *)
4.686 -fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
4.687 +(* hol_context -> typ -> term list *)
4.688 +fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T =
4.689 let
4.690 - val xs = datatype_constrs ext_ctxt T
4.691 + val xs = datatype_constrs hol_ctxt T
4.692 val set_T = T --> bool_T
4.693 val iter_T = @{typ bisim_iterator}
4.694 val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
4.695 @@ -1688,14 +1657,14 @@
4.696 let
4.697 val arg_Ts = binder_types T
4.698 val core_t =
4.699 - discriminate_value ext_ctxt x y_var ::
4.700 + discriminate_value hol_ctxt x y_var ::
4.701 map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
4.702 |> foldr1 s_conj
4.703 in List.foldr absdummy core_t arg_Ts end
4.704 in
4.705 [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
4.706 $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
4.707 - $ (betapplys (optimized_case_def ext_ctxt T bool_T,
4.708 + $ (betapplys (optimized_case_def hol_ctxt T bool_T,
4.709 map case_func xs @ [x_var]))),
4.710 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
4.711 $ (Const (@{const_name insert}, T --> set_T --> set_T)
4.712 @@ -1754,10 +1723,10 @@
4.713 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
4.714 ScnpReconstruct.sizechange_tac]
4.715
4.716 -(* extended_context -> const_table -> styp -> bool *)
4.717 +(* hol_context -> const_table -> styp -> bool *)
4.718 fun uncached_is_well_founded_inductive_pred
4.719 ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
4.720 - : extended_context) (x as (_, T)) =
4.721 + : hol_context) (x as (_, T)) =
4.722 case def_props_for_const thy fast_descrs intro_table x of
4.723 [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
4.724 [Const x])
4.725 @@ -1797,11 +1766,11 @@
4.726 handle List.Empty => false
4.727 | NO_TRIPLE () => false
4.728
4.729 -(* The type constraint below is a workaround for a Poly/ML bug. *)
4.730 +(* The type constraint below is a workaround for a Poly/ML crash. *)
4.731
4.732 -(* extended_context -> styp -> bool *)
4.733 +(* hol_context -> styp -> bool *)
4.734 fun is_well_founded_inductive_pred
4.735 - (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context)
4.736 + (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
4.737 (x as (s, _)) =
4.738 case triple_lookup (const_match thy) wfs x of
4.739 SOME (SOME b) => b
4.740 @@ -1811,7 +1780,7 @@
4.741 | NONE =>
4.742 let
4.743 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
4.744 - val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
4.745 + val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
4.746 in
4.747 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
4.748 end
4.749 @@ -1842,14 +1811,14 @@
4.750 | do_disjunct j t =
4.751 case num_occs_of_bound_in_term j t of
4.752 0 => true
4.753 - | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t)
4.754 + | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
4.755 | _ => false
4.756 (* term -> bool *)
4.757 fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
4.758 let val (xs, body) = strip_abs t2 in
4.759 case length xs of
4.760 1 => false
4.761 - | n => forall (do_disjunct (n - 1)) (disjuncts body)
4.762 + | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
4.763 end
4.764 | do_lfp_def _ = false
4.765 in do_lfp_def o strip_abs_body end
4.766 @@ -1887,7 +1856,7 @@
4.767 end
4.768 val (nonrecs, recs) =
4.769 List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
4.770 - (disjuncts body)
4.771 + (disjuncts_of body)
4.772 val base_body = nonrecs |> List.foldl s_disj @{const False}
4.773 val step_body = recs |> map (repair_rec j)
4.774 |> List.foldl s_disj @{const False}
4.775 @@ -1901,8 +1870,8 @@
4.776 raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
4.777 in aux end
4.778
4.779 -(* extended_context -> styp -> term -> term *)
4.780 -fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T))
4.781 +(* hol_context -> styp -> term -> term *)
4.782 +fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T))
4.783 def =
4.784 let
4.785 val j = maxidx_of_term def + 1
4.786 @@ -1933,11 +1902,11 @@
4.787 $ list_comb (Const step_x, outer_bounds)))
4.788 $ list_comb (Const base_x, outer_bounds)
4.789 |> ap_curry tuple_arg_Ts tuple_T bool_T)
4.790 - |> unfold_defs_in_term ext_ctxt
4.791 + |> unfold_defs_in_term hol_ctxt
4.792 end
4.793
4.794 -(* extended_context -> bool -> styp -> term *)
4.795 -fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds,
4.796 +(* hol_context -> bool -> styp -> term *)
4.797 +fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
4.798 def_table, simp_table, ...})
4.799 gfp (x as (s, T)) =
4.800 let
4.801 @@ -1946,11 +1915,11 @@
4.802 val unrolled_const = Const x' $ zero_const iter_T
4.803 val def = the (def_of_const thy def_table x)
4.804 in
4.805 - if is_equational_fun ext_ctxt x' then
4.806 + if is_equational_fun hol_ctxt x' then
4.807 unrolled_const (* already done *)
4.808 else if not gfp andalso is_linear_inductive_pred_def def andalso
4.809 star_linear_preds then
4.810 - starred_linear_pred_const ext_ctxt x def
4.811 + starred_linear_pred_const hol_ctxt x def
4.812 else
4.813 let
4.814 val j = maxidx_of_term def + 1
4.815 @@ -1973,8 +1942,8 @@
4.816 in unrolled_const end
4.817 end
4.818
4.819 -(* extended_context -> styp -> term *)
4.820 -fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x =
4.821 +(* hol_context -> styp -> term *)
4.822 +fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
4.823 let
4.824 val def = the (def_of_const thy def_table x)
4.825 val (outer, fp_app) = strip_abs def
4.826 @@ -1992,24 +1961,29 @@
4.827 HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
4.828 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
4.829 end
4.830 -fun inductive_pred_axiom ext_ctxt (x as (s, T)) =
4.831 +fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
4.832 if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
4.833 let val x' = (after_name_sep s, T) in
4.834 - raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)]
4.835 + raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
4.836 end
4.837 else
4.838 - raw_inductive_pred_axiom ext_ctxt x
4.839 + raw_inductive_pred_axiom hol_ctxt x
4.840
4.841 -(* extended_context -> styp -> term list *)
4.842 -fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
4.843 +(* hol_context -> styp -> term list *)
4.844 +fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table,
4.845 psimp_table, ...}) (x as (s, _)) =
4.846 case def_props_for_const thy fast_descrs (!simp_table) x of
4.847 [] => (case def_props_for_const thy fast_descrs psimp_table x of
4.848 - [] => [inductive_pred_axiom ext_ctxt x]
4.849 + [] => [inductive_pred_axiom hol_ctxt x]
4.850 | psimps => psimps)
4.851 | simps => simps
4.852 -
4.853 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
4.854 +(* hol_context -> styp -> bool *)
4.855 +fun is_equational_fun_surely_complete hol_ctxt x =
4.856 + case raw_equational_fun_axioms hol_ctxt x of
4.857 + [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
4.858 + strip_comb t1 |> snd |> forall is_Var
4.859 + | _ => false
4.860
4.861 (* term list -> term list *)
4.862 fun merge_type_vars_in_terms ts =
4.863 @@ -2028,1261 +2002,27 @@
4.864 | coalesce T = T
4.865 in map (map_types (map_atyps coalesce)) ts end
4.866
4.867 -(* extended_context -> typ -> typ list -> typ list *)
4.868 -fun add_ground_types ext_ctxt T accum =
4.869 +(* hol_context -> typ -> typ list -> typ list *)
4.870 +fun add_ground_types hol_ctxt T accum =
4.871 case T of
4.872 - Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum
4.873 - | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
4.874 - | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
4.875 + Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum
4.876 + | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
4.877 + | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
4.878 | Type (_, Ts) =>
4.879 if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
4.880 accum
4.881 else
4.882 T :: accum
4.883 - |> fold (add_ground_types ext_ctxt)
4.884 - (case boxed_datatype_constrs ext_ctxt T of
4.885 + |> fold (add_ground_types hol_ctxt)
4.886 + (case boxed_datatype_constrs hol_ctxt T of
4.887 [] => Ts
4.888 | xs => map snd xs)
4.889 | _ => insert (op =) T accum
4.890 -(* extended_context -> typ -> typ list *)
4.891 -fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T []
4.892 -(* extended_context -> term list -> typ list *)
4.893 -fun ground_types_in_terms ext_ctxt ts =
4.894 - fold (fold_types (add_ground_types ext_ctxt)) ts []
4.895 -
4.896 -(* typ list -> int -> term -> bool *)
4.897 -fun has_heavy_bounds_or_vars Ts level t =
4.898 - let
4.899 - (* typ list -> bool *)
4.900 - fun aux [] = false
4.901 - | aux [T] = is_fun_type T orelse is_pair_type T
4.902 - | aux _ = true
4.903 - in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
4.904 -
4.905 -(* typ list -> int -> int -> int -> term -> term *)
4.906 -fun fresh_value_var Ts k n j t =
4.907 - Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
4.908 -
4.909 -(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
4.910 - -> term * term list *)
4.911 -fun pull_out_constr_comb thy Ts relax k level t args seen =
4.912 - let val t_comb = list_comb (t, args) in
4.913 - case t of
4.914 - Const x =>
4.915 - if not relax andalso is_constr thy x andalso
4.916 - not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
4.917 - has_heavy_bounds_or_vars Ts level t_comb andalso
4.918 - not (loose_bvar (t_comb, level)) then
4.919 - let
4.920 - val (j, seen) = case find_index (curry (op =) t_comb) seen of
4.921 - ~1 => (0, t_comb :: seen)
4.922 - | j => (j, seen)
4.923 - in (fresh_value_var Ts k (length seen) j t_comb, seen) end
4.924 - else
4.925 - (t_comb, seen)
4.926 - | _ => (t_comb, seen)
4.927 - end
4.928 -
4.929 -(* (term -> term) -> typ list -> int -> term list -> term list *)
4.930 -fun equations_for_pulled_out_constrs mk_eq Ts k seen =
4.931 - let val n = length seen in
4.932 - map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
4.933 - (index_seq 0 n) seen
4.934 - end
4.935 -
4.936 -(* theory -> bool -> term -> term *)
4.937 -fun pull_out_universal_constrs thy def t =
4.938 - let
4.939 - val k = maxidx_of_term t + 1
4.940 - (* typ list -> bool -> term -> term list -> term list -> term * term list *)
4.941 - fun do_term Ts def t args seen =
4.942 - case t of
4.943 - (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
4.944 - do_eq_or_imp Ts true def t0 t1 t2 seen
4.945 - | (t0 as @{const "==>"}) $ t1 $ t2 =>
4.946 - if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
4.947 - | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
4.948 - do_eq_or_imp Ts true def t0 t1 t2 seen
4.949 - | (t0 as @{const "op -->"}) $ t1 $ t2 =>
4.950 - do_eq_or_imp Ts false def t0 t1 t2 seen
4.951 - | Abs (s, T, t') =>
4.952 - let val (t', seen) = do_term (T :: Ts) def t' [] seen in
4.953 - (list_comb (Abs (s, T, t'), args), seen)
4.954 - end
4.955 - | t1 $ t2 =>
4.956 - let val (t2, seen) = do_term Ts def t2 [] seen in
4.957 - do_term Ts def t1 (t2 :: args) seen
4.958 - end
4.959 - | _ => pull_out_constr_comb thy Ts def k 0 t args seen
4.960 - (* typ list -> bool -> bool -> term -> term -> term -> term list
4.961 - -> term * term list *)
4.962 - and do_eq_or_imp Ts eq def t0 t1 t2 seen =
4.963 - let
4.964 - val (t2, seen) = if eq andalso def then (t2, seen)
4.965 - else do_term Ts false t2 [] seen
4.966 - val (t1, seen) = do_term Ts false t1 [] seen
4.967 - in (t0 $ t1 $ t2, seen) end
4.968 - val (concl, seen) = do_term [] def t [] []
4.969 - in
4.970 - Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
4.971 - seen, concl)
4.972 - end
4.973 -
4.974 -(* extended_context -> bool -> term -> term *)
4.975 -fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
4.976 - let
4.977 - (* styp -> int *)
4.978 - val num_occs_of_var =
4.979 - fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
4.980 - | _ => I) t (K 0)
4.981 - (* bool -> term -> term *)
4.982 - fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
4.983 - aux_eq careful true t0 t1 t2
4.984 - | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
4.985 - t0 $ aux false t1 $ aux careful t2
4.986 - | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
4.987 - aux_eq careful true t0 t1 t2
4.988 - | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
4.989 - t0 $ aux false t1 $ aux careful t2
4.990 - | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
4.991 - | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
4.992 - | aux _ t = t
4.993 - (* bool -> bool -> term -> term -> term -> term *)
4.994 - and aux_eq careful pass1 t0 t1 t2 =
4.995 - ((if careful then
4.996 - raise SAME ()
4.997 - else if axiom andalso is_Var t2 andalso
4.998 - num_occs_of_var (dest_Var t2) = 1 then
4.999 - @{const True}
4.1000 - else case strip_comb t2 of
4.1001 - (* The first case is not as general as it could be. *)
4.1002 - (Const (@{const_name PairBox}, _),
4.1003 - [Const (@{const_name fst}, _) $ Var z1,
4.1004 - Const (@{const_name snd}, _) $ Var z2]) =>
4.1005 - if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
4.1006 - else raise SAME ()
4.1007 - | (Const (x as (s, T)), args) =>
4.1008 - let val arg_Ts = binder_types T in
4.1009 - if length arg_Ts = length args andalso
4.1010 - (is_constr thy x orelse s = @{const_name Pair} orelse
4.1011 - x = (@{const_name Suc}, nat_T --> nat_T)) andalso
4.1012 - (not careful orelse not (is_Var t1) orelse
4.1013 - String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
4.1014 - discriminate_value ext_ctxt x t1 ::
4.1015 - map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
4.1016 - |> foldr1 s_conj
4.1017 - else
4.1018 - raise SAME ()
4.1019 - end
4.1020 - | _ => raise SAME ())
4.1021 - |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
4.1022 - handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
4.1023 - else t0 $ aux false t2 $ aux false t1
4.1024 - (* styp -> term -> int -> typ -> term -> term *)
4.1025 - and sel_eq x t n nth_T nth_t =
4.1026 - HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
4.1027 - |> aux false
4.1028 - in aux axiom t end
4.1029 -
4.1030 -(* theory -> term -> term *)
4.1031 -fun simplify_constrs_and_sels thy t =
4.1032 - let
4.1033 - (* term -> int -> term *)
4.1034 - fun is_nth_sel_on t' n (Const (s, _) $ t) =
4.1035 - (t = t' andalso is_sel_like_and_no_discr s andalso
4.1036 - sel_no_from_name s = n)
4.1037 - | is_nth_sel_on _ _ _ = false
4.1038 - (* term -> term list -> term *)
4.1039 - fun do_term (Const (@{const_name Rep_Frac}, _)
4.1040 - $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
4.1041 - | do_term (Const (@{const_name Abs_Frac}, _)
4.1042 - $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
4.1043 - | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
4.1044 - | do_term (t as Const (x as (s, T))) (args as _ :: _) =
4.1045 - ((if is_constr_like thy x then
4.1046 - if length args = num_binder_types T then
4.1047 - case hd args of
4.1048 - Const (x' as (_, T')) $ t' =>
4.1049 - if domain_type T' = body_type T andalso
4.1050 - forall (uncurry (is_nth_sel_on t'))
4.1051 - (index_seq 0 (length args) ~~ args) then
4.1052 - t'
4.1053 - else
4.1054 - raise SAME ()
4.1055 - | _ => raise SAME ()
4.1056 - else
4.1057 - raise SAME ()
4.1058 - else if is_sel_like_and_no_discr s then
4.1059 - case strip_comb (hd args) of
4.1060 - (Const (x' as (s', T')), ts') =>
4.1061 - if is_constr_like thy x' andalso
4.1062 - constr_name_for_sel_like s = s' andalso
4.1063 - not (exists is_pair_type (binder_types T')) then
4.1064 - list_comb (nth ts' (sel_no_from_name s), tl args)
4.1065 - else
4.1066 - raise SAME ()
4.1067 - | _ => raise SAME ()
4.1068 - else
4.1069 - raise SAME ())
4.1070 - handle SAME () => betapplys (t, args))
4.1071 - | do_term (Abs (s, T, t')) args =
4.1072 - betapplys (Abs (s, T, do_term t' []), args)
4.1073 - | do_term t args = betapplys (t, args)
4.1074 - in do_term t [] end
4.1075 -
4.1076 -(* term -> term *)
4.1077 -fun curry_assms (@{const "==>"} $ (@{const Trueprop}
4.1078 - $ (@{const "op &"} $ t1 $ t2)) $ t3) =
4.1079 - curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
4.1080 - | curry_assms (@{const "==>"} $ t1 $ t2) =
4.1081 - @{const "==>"} $ curry_assms t1 $ curry_assms t2
4.1082 - | curry_assms t = t
4.1083 -
4.1084 -(* term -> term *)
4.1085 -val destroy_universal_equalities =
4.1086 - let
4.1087 - (* term list -> (indexname * typ) list -> term -> term *)
4.1088 - fun aux prems zs t =
4.1089 - case t of
4.1090 - @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
4.1091 - | _ => Logic.list_implies (rev prems, t)
4.1092 - (* term list -> (indexname * typ) list -> term -> term -> term *)
4.1093 - and aux_implies prems zs t1 t2 =
4.1094 - case t1 of
4.1095 - Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
4.1096 - | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
4.1097 - aux_eq prems zs z t' t1 t2
4.1098 - | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
4.1099 - aux_eq prems zs z t' t1 t2
4.1100 - | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
4.1101 - (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
4.1102 - -> term -> term *)
4.1103 - and aux_eq prems zs z t' t1 t2 =
4.1104 - if not (member (op =) zs z) andalso
4.1105 - not (exists_subterm (curry (op =) (Var z)) t') then
4.1106 - aux prems zs (subst_free [(Var z, t')] t2)
4.1107 - else
4.1108 - aux (t1 :: prems) (Term.add_vars t1 zs) t2
4.1109 - in aux [] [] end
4.1110 -
4.1111 -(* theory -> term -> term *)
4.1112 -fun pull_out_existential_constrs thy t =
4.1113 - let
4.1114 - val k = maxidx_of_term t + 1
4.1115 - (* typ list -> int -> term -> term list -> term list -> term * term list *)
4.1116 - fun aux Ts num_exists t args seen =
4.1117 - case t of
4.1118 - (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
4.1119 - let
4.1120 - val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
4.1121 - val n = length seen'
4.1122 - (* unit -> term list *)
4.1123 - fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
4.1124 - in
4.1125 - (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
4.1126 - |> List.foldl s_conj t1 |> fold mk_exists (vars ())
4.1127 - |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
4.1128 - end
4.1129 - | t1 $ t2 =>
4.1130 - let val (t2, seen) = aux Ts num_exists t2 [] seen in
4.1131 - aux Ts num_exists t1 (t2 :: args) seen
4.1132 - end
4.1133 - | Abs (s, T, t') =>
4.1134 - let
4.1135 - val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
4.1136 - in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
4.1137 - | _ =>
4.1138 - if num_exists > 0 then
4.1139 - pull_out_constr_comb thy Ts false k num_exists t args seen
4.1140 - else
4.1141 - (list_comb (t, args), seen)
4.1142 - in aux [] 0 t [] [] |> fst end
4.1143 -
4.1144 -(* theory -> int -> term list -> term list -> (term * term list) option *)
4.1145 -fun find_bound_assign _ _ _ [] = NONE
4.1146 - | find_bound_assign thy j seen (t :: ts) =
4.1147 - let
4.1148 - (* bool -> term -> term -> (term * term list) option *)
4.1149 - fun aux pass1 t1 t2 =
4.1150 - (if loose_bvar1 (t2, j) then
4.1151 - if pass1 then aux false t2 t1 else raise SAME ()
4.1152 - else case t1 of
4.1153 - Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
4.1154 - | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
4.1155 - if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then
4.1156 - SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
4.1157 - ts @ seen)
4.1158 - else
4.1159 - raise SAME ()
4.1160 - | _ => raise SAME ())
4.1161 - handle SAME () => find_bound_assign thy j (t :: seen) ts
4.1162 - in
4.1163 - case t of
4.1164 - Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
4.1165 - | _ => find_bound_assign thy j (t :: seen) ts
4.1166 - end
4.1167 -
4.1168 -(* int -> term -> term -> term *)
4.1169 -fun subst_one_bound j arg t =
4.1170 - let
4.1171 - fun aux (Bound i, lev) =
4.1172 - if i < lev then raise SAME ()
4.1173 - else if i = lev then incr_boundvars (lev - j) arg
4.1174 - else Bound (i - 1)
4.1175 - | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
4.1176 - | aux (f $ t, lev) =
4.1177 - (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
4.1178 - handle SAME () => f $ aux (t, lev))
4.1179 - | aux _ = raise SAME ()
4.1180 - in aux (t, j) handle SAME () => t end
4.1181 -
4.1182 -(* theory -> term -> term *)
4.1183 -fun destroy_existential_equalities thy =
4.1184 - let
4.1185 - (* string list -> typ list -> term list -> term *)
4.1186 - fun kill [] [] ts = foldr1 s_conj ts
4.1187 - | kill (s :: ss) (T :: Ts) ts =
4.1188 - (case find_bound_assign thy (length ss) [] ts of
4.1189 - SOME (_, []) => @{const True}
4.1190 - | SOME (arg_t, ts) =>
4.1191 - kill ss Ts (map (subst_one_bound (length ss)
4.1192 - (incr_bv (~1, length ss + 1, arg_t))) ts)
4.1193 - | NONE =>
4.1194 - Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
4.1195 - $ Abs (s, T, kill ss Ts ts))
4.1196 - | kill _ _ _ = raise UnequalLengths
4.1197 - (* string list -> typ list -> term -> term *)
4.1198 - fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
4.1199 - gather (ss @ [s1]) (Ts @ [T1]) t1
4.1200 - | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
4.1201 - | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
4.1202 - | gather [] [] t = t
4.1203 - | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t))
4.1204 - in gather [] [] end
4.1205 -
4.1206 -(* term -> term *)
4.1207 -fun distribute_quantifiers t =
4.1208 - case t of
4.1209 - (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
4.1210 - (case t1 of
4.1211 - (t10 as @{const "op &"}) $ t11 $ t12 =>
4.1212 - t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
4.1213 - $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
4.1214 - | (t10 as @{const Not}) $ t11 =>
4.1215 - t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
4.1216 - $ Abs (s, T1, t11))
4.1217 - | t1 =>
4.1218 - if not (loose_bvar1 (t1, 0)) then
4.1219 - distribute_quantifiers (incr_boundvars ~1 t1)
4.1220 - else
4.1221 - t0 $ Abs (s, T1, distribute_quantifiers t1))
4.1222 - | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
4.1223 - (case distribute_quantifiers t1 of
4.1224 - (t10 as @{const "op |"}) $ t11 $ t12 =>
4.1225 - t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
4.1226 - $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
4.1227 - | (t10 as @{const "op -->"}) $ t11 $ t12 =>
4.1228 - t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
4.1229 - $ Abs (s, T1, t11))
4.1230 - $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
4.1231 - | (t10 as @{const Not}) $ t11 =>
4.1232 - t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
4.1233 - $ Abs (s, T1, t11))
4.1234 - | t1 =>
4.1235 - if not (loose_bvar1 (t1, 0)) then
4.1236 - distribute_quantifiers (incr_boundvars ~1 t1)
4.1237 - else
4.1238 - t0 $ Abs (s, T1, distribute_quantifiers t1))
4.1239 - | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
4.1240 - | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
4.1241 - | _ => t
4.1242 -
4.1243 -(* int -> int -> (int -> int) -> term -> term *)
4.1244 -fun renumber_bounds j n f t =
4.1245 - case t of
4.1246 - t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
4.1247 - | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
4.1248 - | Bound j' =>
4.1249 - Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
4.1250 - | _ => t
4.1251 -
4.1252 -val quantifier_cluster_threshold = 7
4.1253 -
4.1254 -(* theory -> term -> term *)
4.1255 -fun push_quantifiers_inward thy =
4.1256 - let
4.1257 - (* string -> string list -> typ list -> term -> term *)
4.1258 - fun aux quant_s ss Ts t =
4.1259 - (case t of
4.1260 - (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
4.1261 - if s0 = quant_s then
4.1262 - aux s0 (s1 :: ss) (T1 :: Ts) t1
4.1263 - else if quant_s = "" andalso
4.1264 - (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
4.1265 - aux s0 [s1] [T1] t1
4.1266 - else
4.1267 - raise SAME ()
4.1268 - | _ => raise SAME ())
4.1269 - handle SAME () =>
4.1270 - case t of
4.1271 - t1 $ t2 =>
4.1272 - if quant_s = "" then
4.1273 - aux "" [] [] t1 $ aux "" [] [] t2
4.1274 - else
4.1275 - let
4.1276 - val typical_card = 4
4.1277 - (* ('a -> ''b list) -> 'a list -> ''b list *)
4.1278 - fun big_union proj ps =
4.1279 - fold (fold (insert (op =)) o proj) ps []
4.1280 - val (ts, connective) = strip_any_connective t
4.1281 - val T_costs =
4.1282 - map (bounded_card_of_type 65536 typical_card []) Ts
4.1283 - val t_costs = map size_of_term ts
4.1284 - val num_Ts = length Ts
4.1285 - (* int -> int *)
4.1286 - val flip = curry (op -) (num_Ts - 1)
4.1287 - val t_boundss = map (map flip o loose_bnos) ts
4.1288 - (* (int list * int) list -> int list
4.1289 - -> (int list * int) list *)
4.1290 - fun merge costly_boundss [] = costly_boundss
4.1291 - | merge costly_boundss (j :: js) =
4.1292 - let
4.1293 - val (yeas, nays) =
4.1294 - List.partition (fn (bounds, _) =>
4.1295 - member (op =) bounds j)
4.1296 - costly_boundss
4.1297 - val yeas_bounds = big_union fst yeas
4.1298 - val yeas_cost = Integer.sum (map snd yeas)
4.1299 - * nth T_costs j
4.1300 - in merge ((yeas_bounds, yeas_cost) :: nays) js end
4.1301 - (* (int list * int) list -> int list -> int *)
4.1302 - val cost = Integer.sum o map snd oo merge
4.1303 - (* Inspired by Claessen & Sörensson's polynomial binary
4.1304 - splitting heuristic (p. 5 of their MODEL 2003 paper). *)
4.1305 - (* (int list * int) list -> int list -> int list *)
4.1306 - fun heuristically_best_permutation _ [] = []
4.1307 - | heuristically_best_permutation costly_boundss js =
4.1308 - let
4.1309 - val (costly_boundss, (j, js)) =
4.1310 - js |> map (`(merge costly_boundss o single))
4.1311 - |> sort (int_ord
4.1312 - o pairself (Integer.sum o map snd o fst))
4.1313 - |> split_list |>> hd ||> pairf hd tl
4.1314 - in
4.1315 - j :: heuristically_best_permutation costly_boundss js
4.1316 - end
4.1317 - val js =
4.1318 - if length Ts <= quantifier_cluster_threshold then
4.1319 - all_permutations (index_seq 0 num_Ts)
4.1320 - |> map (`(cost (t_boundss ~~ t_costs)))
4.1321 - |> sort (int_ord o pairself fst) |> hd |> snd
4.1322 - else
4.1323 - heuristically_best_permutation (t_boundss ~~ t_costs)
4.1324 - (index_seq 0 num_Ts)
4.1325 - val back_js = map (fn j => find_index (curry (op =) j) js)
4.1326 - (index_seq 0 num_Ts)
4.1327 - val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
4.1328 - ts
4.1329 - (* (term * int list) list -> term *)
4.1330 - fun mk_connection [] =
4.1331 - raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
4.1332 - \mk_connection", "")
4.1333 - | mk_connection ts_cum_bounds =
4.1334 - ts_cum_bounds |> map fst
4.1335 - |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
4.1336 - (* (term * int list) list -> int list -> term *)
4.1337 - fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
4.1338 - | build ts_cum_bounds (j :: js) =
4.1339 - let
4.1340 - val (yeas, nays) =
4.1341 - List.partition (fn (_, bounds) =>
4.1342 - member (op =) bounds j)
4.1343 - ts_cum_bounds
4.1344 - ||> map (apfst (incr_boundvars ~1))
4.1345 - in
4.1346 - if null yeas then
4.1347 - build nays js
4.1348 - else
4.1349 - let val T = nth Ts (flip j) in
4.1350 - build ((Const (quant_s, (T --> bool_T) --> bool_T)
4.1351 - $ Abs (nth ss (flip j), T,
4.1352 - mk_connection yeas),
4.1353 - big_union snd yeas) :: nays) js
4.1354 - end
4.1355 - end
4.1356 - in build (ts ~~ t_boundss) js end
4.1357 - | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
4.1358 - | _ => t
4.1359 - in aux "" [] [] end
4.1360 -
4.1361 -(* polarity -> string -> bool *)
4.1362 -fun is_positive_existential polar quant_s =
4.1363 - (polar = Pos andalso quant_s = @{const_name Ex}) orelse
4.1364 - (polar = Neg andalso quant_s <> @{const_name Ex})
4.1365 -
4.1366 -(* extended_context -> int -> term -> term *)
4.1367 -fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
4.1368 - skolem_depth =
4.1369 - let
4.1370 - (* int list -> int list *)
4.1371 - val incrs = map (Integer.add 1)
4.1372 - (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
4.1373 - fun aux ss Ts js depth polar t =
4.1374 - let
4.1375 - (* string -> typ -> string -> typ -> term -> term *)
4.1376 - fun do_quantifier quant_s quant_T abs_s abs_T t =
4.1377 - if not (loose_bvar1 (t, 0)) then
4.1378 - aux ss Ts js depth polar (incr_boundvars ~1 t)
4.1379 - else if depth <= skolem_depth andalso
4.1380 - is_positive_existential polar quant_s then
4.1381 - let
4.1382 - val j = length (!skolems) + 1
4.1383 - val sko_s = skolem_prefix_for (length js) j ^ abs_s
4.1384 - val _ = Unsynchronized.change skolems (cons (sko_s, ss))
4.1385 - val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
4.1386 - map Bound (rev js))
4.1387 - val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
4.1388 - in
4.1389 - if null js then betapply (abs_t, sko_t)
4.1390 - else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
4.1391 - end
4.1392 - else
4.1393 - Const (quant_s, quant_T)
4.1394 - $ Abs (abs_s, abs_T,
4.1395 - if is_higher_order_type abs_T then
4.1396 - t
4.1397 - else
4.1398 - aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
4.1399 - (depth + 1) polar t)
4.1400 - in
4.1401 - case t of
4.1402 - Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
4.1403 - do_quantifier s0 T0 s1 T1 t1
4.1404 - | @{const "==>"} $ t1 $ t2 =>
4.1405 - @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
4.1406 - $ aux ss Ts js depth polar t2
4.1407 - | @{const Pure.conjunction} $ t1 $ t2 =>
4.1408 - @{const Pure.conjunction} $ aux ss Ts js depth polar t1
4.1409 - $ aux ss Ts js depth polar t2
4.1410 - | @{const Trueprop} $ t1 =>
4.1411 - @{const Trueprop} $ aux ss Ts js depth polar t1
4.1412 - | @{const Not} $ t1 =>
4.1413 - @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
4.1414 - | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
4.1415 - do_quantifier s0 T0 s1 T1 t1
4.1416 - | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
4.1417 - do_quantifier s0 T0 s1 T1 t1
4.1418 - | @{const "op &"} $ t1 $ t2 =>
4.1419 - @{const "op &"} $ aux ss Ts js depth polar t1
4.1420 - $ aux ss Ts js depth polar t2
4.1421 - | @{const "op |"} $ t1 $ t2 =>
4.1422 - @{const "op |"} $ aux ss Ts js depth polar t1
4.1423 - $ aux ss Ts js depth polar t2
4.1424 - | @{const "op -->"} $ t1 $ t2 =>
4.1425 - @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
4.1426 - $ aux ss Ts js depth polar t2
4.1427 - | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
4.1428 - t0 $ t1 $ aux ss Ts js depth polar t2
4.1429 - | Const (x as (s, T)) =>
4.1430 - if is_inductive_pred ext_ctxt x andalso
4.1431 - not (is_well_founded_inductive_pred ext_ctxt x) then
4.1432 - let
4.1433 - val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
4.1434 - val (pref, connective, set_oper) =
4.1435 - if gfp then
4.1436 - (lbfp_prefix,
4.1437 - @{const "op |"},
4.1438 - @{const_name upper_semilattice_fun_inst.sup_fun})
4.1439 - else
4.1440 - (ubfp_prefix,
4.1441 - @{const "op &"},
4.1442 - @{const_name lower_semilattice_fun_inst.inf_fun})
4.1443 - (* unit -> term *)
4.1444 - fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x
4.1445 - |> aux ss Ts js depth polar
4.1446 - fun neg () = Const (pref ^ s, T)
4.1447 - in
4.1448 - (case polar |> gfp ? flip_polarity of
4.1449 - Pos => pos ()
4.1450 - | Neg => neg ()
4.1451 - | Neut =>
4.1452 - if is_fun_type T then
4.1453 - let
4.1454 - val ((trunk_arg_Ts, rump_arg_T), body_T) =
4.1455 - T |> strip_type |>> split_last
4.1456 - val set_T = rump_arg_T --> body_T
4.1457 - (* (unit -> term) -> term *)
4.1458 - fun app f =
4.1459 - list_comb (f (),
4.1460 - map Bound (length trunk_arg_Ts - 1 downto 0))
4.1461 - in
4.1462 - List.foldr absdummy
4.1463 - (Const (set_oper, set_T --> set_T --> set_T)
4.1464 - $ app pos $ app neg) trunk_arg_Ts
4.1465 - end
4.1466 - else
4.1467 - connective $ pos () $ neg ())
4.1468 - end
4.1469 - else
4.1470 - Const x
4.1471 - | t1 $ t2 =>
4.1472 - betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
4.1473 - aux ss Ts [] depth Neut t2)
4.1474 - | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
4.1475 - | _ => t
4.1476 - end
4.1477 - in aux [] [] [] 0 Pos end
4.1478 -
4.1479 -(* extended_context -> styp -> (int * term option) list *)
4.1480 -fun static_args_in_term ({ersatz_table, ...} : extended_context) x t =
4.1481 - let
4.1482 - (* term -> term list -> term list -> term list list *)
4.1483 - fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
4.1484 - | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
4.1485 - | fun_calls t args =
4.1486 - (case t of
4.1487 - Const (x' as (s', T')) =>
4.1488 - x = x' orelse (case AList.lookup (op =) ersatz_table s' of
4.1489 - SOME s'' => x = (s'', T')
4.1490 - | NONE => false)
4.1491 - | _ => false) ? cons args
4.1492 - (* term list list -> term list list -> term list -> term list list *)
4.1493 - fun call_sets [] [] vs = [vs]
4.1494 - | call_sets [] uss vs = vs :: call_sets uss [] []
4.1495 - | call_sets ([] :: _) _ _ = []
4.1496 - | call_sets ((t :: ts) :: tss) uss vs =
4.1497 - OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
4.1498 - val sets = call_sets (fun_calls t [] []) [] []
4.1499 - val indexed_sets = sets ~~ (index_seq 0 (length sets))
4.1500 - in
4.1501 - fold_rev (fn (set, j) =>
4.1502 - case set of
4.1503 - [Var _] => AList.lookup (op =) indexed_sets set = SOME j
4.1504 - ? cons (j, NONE)
4.1505 - | [t as Const _] => cons (j, SOME t)
4.1506 - | [t as Free _] => cons (j, SOME t)
4.1507 - | _ => I) indexed_sets []
4.1508 - end
4.1509 -(* extended_context -> styp -> term list -> (int * term option) list *)
4.1510 -fun static_args_in_terms ext_ctxt x =
4.1511 - map (static_args_in_term ext_ctxt x)
4.1512 - #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
4.1513 -
4.1514 -(* term -> term list *)
4.1515 -fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
4.1516 - | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
4.1517 - | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
4.1518 - snd (strip_comb t1)
4.1519 - | params_in_equation _ = []
4.1520 -
4.1521 -(* styp -> styp -> int list -> term list -> term list -> term -> term *)
4.1522 -fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
4.1523 - let
4.1524 - val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
4.1525 - + 1
4.1526 - val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
4.1527 - val fixed_params = filter_indices fixed_js (params_in_equation t)
4.1528 - (* term list -> term -> term *)
4.1529 - fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
4.1530 - | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
4.1531 - | aux args t =
4.1532 - if t = Const x then
4.1533 - list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
4.1534 - else
4.1535 - let val j = find_index (curry (op =) t) fixed_params in
4.1536 - list_comb (if j >= 0 then nth fixed_args j else t, args)
4.1537 - end
4.1538 - in aux [] t end
4.1539 -
4.1540 -(* typ list -> term -> bool *)
4.1541 -fun is_eligible_arg Ts t =
4.1542 - let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
4.1543 - null bad_Ts orelse
4.1544 - (is_higher_order_type (fastype_of1 (Ts, t)) andalso
4.1545 - forall (not o is_higher_order_type) bad_Ts)
4.1546 - end
4.1547 -
4.1548 -(* (int * term option) list -> (int * term) list -> int list *)
4.1549 -fun overlapping_indices [] _ = []
4.1550 - | overlapping_indices _ [] = []
4.1551 - | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
4.1552 - if j1 < j2 then overlapping_indices ps1' ps2
4.1553 - else if j1 > j2 then overlapping_indices ps1 ps2'
4.1554 - else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
4.1555 -
4.1556 -val special_depth = 20
4.1557 -
4.1558 -(* extended_context -> int -> term -> term *)
4.1559 -fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table,
4.1560 - special_funs, ...}) depth t =
4.1561 - if not specialize orelse depth > special_depth then
4.1562 - t
4.1563 - else
4.1564 - let
4.1565 - val blacklist = if depth = 0 then []
4.1566 - else case term_under_def t of Const x => [x] | _ => []
4.1567 - (* term list -> typ list -> term -> term *)
4.1568 - fun aux args Ts (Const (x as (s, T))) =
4.1569 - ((if not (member (op =) blacklist x) andalso not (null args) andalso
4.1570 - not (String.isPrefix special_prefix s) andalso
4.1571 - is_equational_fun ext_ctxt x then
4.1572 - let
4.1573 - val eligible_args = filter (is_eligible_arg Ts o snd)
4.1574 - (index_seq 0 (length args) ~~ args)
4.1575 - val _ = not (null eligible_args) orelse raise SAME ()
4.1576 - val old_axs = equational_fun_axioms ext_ctxt x
4.1577 - |> map (destroy_existential_equalities thy)
4.1578 - val static_params = static_args_in_terms ext_ctxt x old_axs
4.1579 - val fixed_js = overlapping_indices static_params eligible_args
4.1580 - val _ = not (null fixed_js) orelse raise SAME ()
4.1581 - val fixed_args = filter_indices fixed_js args
4.1582 - val vars = fold Term.add_vars fixed_args []
4.1583 - |> sort (TermOrd.fast_indexname_ord o pairself fst)
4.1584 - val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
4.1585 - fixed_args []
4.1586 - |> sort int_ord
4.1587 - val live_args = filter_out_indices fixed_js args
4.1588 - val extra_args = map Var vars @ map Bound bound_js @ live_args
4.1589 - val extra_Ts = map snd vars @ filter_indices bound_js Ts
4.1590 - val k = maxidx_of_term t + 1
4.1591 - (* int -> term *)
4.1592 - fun var_for_bound_no j =
4.1593 - Var ((bound_var_prefix ^
4.1594 - nat_subscript (find_index (curry (op =) j) bound_js
4.1595 - + 1), k),
4.1596 - nth Ts j)
4.1597 - val fixed_args_in_axiom =
4.1598 - map (curry subst_bounds
4.1599 - (map var_for_bound_no (index_seq 0 (length Ts))))
4.1600 - fixed_args
4.1601 - in
4.1602 - case AList.lookup (op =) (!special_funs)
4.1603 - (x, fixed_js, fixed_args_in_axiom) of
4.1604 - SOME x' => list_comb (Const x', extra_args)
4.1605 - | NONE =>
4.1606 - let
4.1607 - val extra_args_in_axiom =
4.1608 - map Var vars @ map var_for_bound_no bound_js
4.1609 - val x' as (s', _) =
4.1610 - (special_prefix_for (length (!special_funs) + 1) ^ s,
4.1611 - extra_Ts @ filter_out_indices fixed_js (binder_types T)
4.1612 - ---> body_type T)
4.1613 - val new_axs =
4.1614 - map (specialize_fun_axiom x x' fixed_js
4.1615 - fixed_args_in_axiom extra_args_in_axiom) old_axs
4.1616 - val _ =
4.1617 - Unsynchronized.change special_funs
4.1618 - (cons ((x, fixed_js, fixed_args_in_axiom), x'))
4.1619 - val _ = add_simps simp_table s' new_axs
4.1620 - in list_comb (Const x', extra_args) end
4.1621 - end
4.1622 - else
4.1623 - raise SAME ())
4.1624 - handle SAME () => list_comb (Const x, args))
4.1625 - | aux args Ts (Abs (s, T, t)) =
4.1626 - list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
4.1627 - | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
4.1628 - | aux args _ t = list_comb (t, args)
4.1629 - in aux [] [] t end
4.1630 -
4.1631 -(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
4.1632 -fun add_to_uncurry_table thy t =
4.1633 - let
4.1634 - (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
4.1635 - fun aux (t1 $ t2) args table =
4.1636 - let val table = aux t2 [] table in aux t1 (t2 :: args) table end
4.1637 - | aux (Abs (_, _, t')) _ table = aux t' [] table
4.1638 - | aux (t as Const (x as (s, _))) args table =
4.1639 - if is_built_in_const true x orelse is_constr_like thy x orelse
4.1640 - is_sel s orelse s = @{const_name Sigma} then
4.1641 - table
4.1642 - else
4.1643 - Termtab.map_default (t, 65536) (curry Int.min (length args)) table
4.1644 - | aux _ _ table = table
4.1645 - in aux t [] end
4.1646 -
4.1647 -(* int Termtab.tab term -> term *)
4.1648 -fun uncurry_term table t =
4.1649 - let
4.1650 - (* term -> term list -> term *)
4.1651 - fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
4.1652 - | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
4.1653 - | aux (t as Const (s, T)) args =
4.1654 - (case Termtab.lookup table t of
4.1655 - SOME n =>
4.1656 - if n >= 2 then
4.1657 - let
4.1658 - val (arg_Ts, rest_T) = strip_n_binders n T
4.1659 - val j =
4.1660 - if hd arg_Ts = @{typ bisim_iterator} orelse
4.1661 - is_fp_iterator_type (hd arg_Ts) then
4.1662 - 1
4.1663 - else case find_index (not_equal bool_T) arg_Ts of
4.1664 - ~1 => n
4.1665 - | j => j
4.1666 - val ((before_args, tuple_args), after_args) =
4.1667 - args |> chop n |>> chop j
4.1668 - val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
4.1669 - T |> strip_n_binders n |>> chop j
4.1670 - val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
4.1671 - in
4.1672 - if n - j < 2 then
4.1673 - betapplys (t, args)
4.1674 - else
4.1675 - betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
4.1676 - before_arg_Ts ---> tuple_T --> rest_T),
4.1677 - before_args @ [mk_flat_tuple tuple_T tuple_args] @
4.1678 - after_args)
4.1679 - end
4.1680 - else
4.1681 - betapplys (t, args)
4.1682 - | NONE => betapplys (t, args))
4.1683 - | aux t args = betapplys (t, args)
4.1684 - in aux t [] end
4.1685 -
4.1686 -(* (term -> term) -> int -> term -> term *)
4.1687 -fun coerce_bound_no f j t =
4.1688 - case t of
4.1689 - t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
4.1690 - | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
4.1691 - | Bound j' => if j' = j then f t else t
4.1692 - | _ => t
4.1693 -
4.1694 -(* extended_context -> bool -> term -> term *)
4.1695 -fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t =
4.1696 - let
4.1697 - (* typ -> typ *)
4.1698 - fun box_relational_operator_type (Type ("fun", Ts)) =
4.1699 - Type ("fun", map box_relational_operator_type Ts)
4.1700 - | box_relational_operator_type (Type ("*", Ts)) =
4.1701 - Type ("*", map (box_type ext_ctxt InPair) Ts)
4.1702 - | box_relational_operator_type T = T
4.1703 - (* typ -> typ -> term -> term *)
4.1704 - fun coerce_bound_0_in_term new_T old_T =
4.1705 - old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
4.1706 - (* typ list -> typ -> term -> term *)
4.1707 - and coerce_term Ts new_T old_T t =
4.1708 - if old_T = new_T then
4.1709 - t
4.1710 - else
4.1711 - case (new_T, old_T) of
4.1712 - (Type (new_s, new_Ts as [new_T1, new_T2]),
4.1713 - Type ("fun", [old_T1, old_T2])) =>
4.1714 - (case eta_expand Ts t 1 of
4.1715 - Abs (s, _, t') =>
4.1716 - Abs (s, new_T1,
4.1717 - t' |> coerce_bound_0_in_term new_T1 old_T1
4.1718 - |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
4.1719 - |> Envir.eta_contract
4.1720 - |> new_s <> "fun"
4.1721 - ? construct_value thy (@{const_name FunBox},
4.1722 - Type ("fun", new_Ts) --> new_T) o single
4.1723 - | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
4.1724 - \coerce_term", [t']))
4.1725 - | (Type (new_s, new_Ts as [new_T1, new_T2]),
4.1726 - Type (old_s, old_Ts as [old_T1, old_T2])) =>
4.1727 - if old_s = @{type_name fun_box} orelse
4.1728 - old_s = @{type_name pair_box} orelse old_s = "*" then
4.1729 - case constr_expand ext_ctxt old_T t of
4.1730 - Const (@{const_name FunBox}, _) $ t1 =>
4.1731 - if new_s = "fun" then
4.1732 - coerce_term Ts new_T (Type ("fun", old_Ts)) t1
4.1733 - else
4.1734 - construct_value thy
4.1735 - (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
4.1736 - [coerce_term Ts (Type ("fun", new_Ts))
4.1737 - (Type ("fun", old_Ts)) t1]
4.1738 - | Const _ $ t1 $ t2 =>
4.1739 - construct_value thy
4.1740 - (if new_s = "*" then @{const_name Pair}
4.1741 - else @{const_name PairBox}, new_Ts ---> new_T)
4.1742 - [coerce_term Ts new_T1 old_T1 t1,
4.1743 - coerce_term Ts new_T2 old_T2 t2]
4.1744 - | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
4.1745 - \coerce_term", [t'])
4.1746 - else
4.1747 - raise TYPE ("coerce_term", [new_T, old_T], [t])
4.1748 - | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
4.1749 - (* indexname * typ -> typ * term -> typ option list -> typ option list *)
4.1750 - fun add_boxed_types_for_var (z as (_, T)) (T', t') =
4.1751 - case t' of
4.1752 - Var z' => z' = z ? insert (op =) T'
4.1753 - | Const (@{const_name Pair}, _) $ t1 $ t2 =>
4.1754 - (case T' of
4.1755 - Type (_, [T1, T2]) =>
4.1756 - fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
4.1757 - | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
4.1758 - \add_boxed_types_for_var", [T'], []))
4.1759 - | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
4.1760 - (* typ list -> typ list -> term -> indexname * typ -> typ *)
4.1761 - fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
4.1762 - case t of
4.1763 - @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
4.1764 - | Const (s0, _) $ t1 $ _ =>
4.1765 - if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
4.1766 - let
4.1767 - val (t', args) = strip_comb t1
4.1768 - val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
4.1769 - in
4.1770 - case fold (add_boxed_types_for_var z)
4.1771 - (fst (strip_n_binders (length args) T') ~~ args) [] of
4.1772 - [T''] => T''
4.1773 - | _ => T
4.1774 - end
4.1775 - else
4.1776 - T
4.1777 - | _ => T
4.1778 - (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
4.1779 - -> term -> term *)
4.1780 - and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
4.1781 - let
4.1782 - val abs_T' =
4.1783 - if polar = Neut orelse is_positive_existential polar quant_s then
4.1784 - box_type ext_ctxt InFunLHS abs_T
4.1785 - else
4.1786 - abs_T
4.1787 - val body_T = body_type quant_T
4.1788 - in
4.1789 - Const (quant_s, (abs_T' --> body_T) --> body_T)
4.1790 - $ Abs (abs_s, abs_T',
4.1791 - t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
4.1792 - end
4.1793 - (* typ list -> typ list -> string -> typ -> term -> term -> term *)
4.1794 - and do_equals new_Ts old_Ts s0 T0 t1 t2 =
4.1795 - let
4.1796 - val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
4.1797 - val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
4.1798 - val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
4.1799 - in
4.1800 - list_comb (Const (s0, T --> T --> body_type T0),
4.1801 - map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
4.1802 - end
4.1803 - (* string -> typ -> term *)
4.1804 - and do_description_operator s T =
4.1805 - let val T1 = box_type ext_ctxt InFunLHS (range_type T) in
4.1806 - Const (s, (T1 --> bool_T) --> T1)
4.1807 - end
4.1808 - (* typ list -> typ list -> polarity -> term -> term *)
4.1809 - and do_term new_Ts old_Ts polar t =
4.1810 - case t of
4.1811 - Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
4.1812 - do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
4.1813 - | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
4.1814 - do_equals new_Ts old_Ts s0 T0 t1 t2
4.1815 - | @{const "==>"} $ t1 $ t2 =>
4.1816 - @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
4.1817 - $ do_term new_Ts old_Ts polar t2
4.1818 - | @{const Pure.conjunction} $ t1 $ t2 =>
4.1819 - @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
4.1820 - $ do_term new_Ts old_Ts polar t2
4.1821 - | @{const Trueprop} $ t1 =>
4.1822 - @{const Trueprop} $ do_term new_Ts old_Ts polar t1
4.1823 - | @{const Not} $ t1 =>
4.1824 - @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
4.1825 - | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
4.1826 - do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
4.1827 - | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
4.1828 - do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
4.1829 - | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
4.1830 - do_equals new_Ts old_Ts s0 T0 t1 t2
4.1831 - | @{const "op &"} $ t1 $ t2 =>
4.1832 - @{const "op &"} $ do_term new_Ts old_Ts polar t1
4.1833 - $ do_term new_Ts old_Ts polar t2
4.1834 - | @{const "op |"} $ t1 $ t2 =>
4.1835 - @{const "op |"} $ do_term new_Ts old_Ts polar t1
4.1836 - $ do_term new_Ts old_Ts polar t2
4.1837 - | @{const "op -->"} $ t1 $ t2 =>
4.1838 - @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
4.1839 - $ do_term new_Ts old_Ts polar t2
4.1840 - | Const (s as @{const_name The}, T) => do_description_operator s T
4.1841 - | Const (s as @{const_name Eps}, T) => do_description_operator s T
4.1842 - | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
4.1843 - let val T' = box_type ext_ctxt InSel T2 in
4.1844 - Const (@{const_name quot_normal}, T' --> T')
4.1845 - end
4.1846 - | Const (s as @{const_name Tha}, T) => do_description_operator s T
4.1847 - | Const (x as (s, T)) =>
4.1848 - Const (s, if s = @{const_name converse} orelse
4.1849 - s = @{const_name trancl} then
4.1850 - box_relational_operator_type T
4.1851 - else if is_built_in_const fast_descrs x orelse
4.1852 - s = @{const_name Sigma} then
4.1853 - T
4.1854 - else if is_constr_like thy x then
4.1855 - box_type ext_ctxt InConstr T
4.1856 - else if is_sel s
4.1857 - orelse is_rep_fun thy x then
4.1858 - box_type ext_ctxt InSel T
4.1859 - else
4.1860 - box_type ext_ctxt InExpr T)
4.1861 - | t1 $ Abs (s, T, t2') =>
4.1862 - let
4.1863 - val t1 = do_term new_Ts old_Ts Neut t1
4.1864 - val T1 = fastype_of1 (new_Ts, t1)
4.1865 - val (s1, Ts1) = dest_Type T1
4.1866 - val T' = hd (snd (dest_Type (hd Ts1)))
4.1867 - val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
4.1868 - val T2 = fastype_of1 (new_Ts, t2)
4.1869 - val t2 = coerce_term new_Ts (hd Ts1) T2 t2
4.1870 - in
4.1871 - betapply (if s1 = "fun" then
4.1872 - t1
4.1873 - else
4.1874 - select_nth_constr_arg thy
4.1875 - (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
4.1876 - (Type ("fun", Ts1)), t2)
4.1877 - end
4.1878 - | t1 $ t2 =>
4.1879 - let
4.1880 - val t1 = do_term new_Ts old_Ts Neut t1
4.1881 - val T1 = fastype_of1 (new_Ts, t1)
4.1882 - val (s1, Ts1) = dest_Type T1
4.1883 - val t2 = do_term new_Ts old_Ts Neut t2
4.1884 - val T2 = fastype_of1 (new_Ts, t2)
4.1885 - val t2 = coerce_term new_Ts (hd Ts1) T2 t2
4.1886 - in
4.1887 - betapply (if s1 = "fun" then
4.1888 - t1
4.1889 - else
4.1890 - select_nth_constr_arg thy
4.1891 - (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
4.1892 - (Type ("fun", Ts1)), t2)
4.1893 - end
4.1894 - | Free (s, T) => Free (s, box_type ext_ctxt InExpr T)
4.1895 - | Var (z as (x, T)) =>
4.1896 - Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
4.1897 - else box_type ext_ctxt InExpr T)
4.1898 - | Bound _ => t
4.1899 - | Abs (s, T, t') =>
4.1900 - Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
4.1901 - in do_term [] [] Pos orig_t end
4.1902 -
4.1903 -(* int -> term -> term *)
4.1904 -fun eval_axiom_for_term j t =
4.1905 - Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
4.1906 -
4.1907 -(* extended_context -> styp -> bool *)
4.1908 -fun is_equational_fun_surely_complete ext_ctxt x =
4.1909 - case raw_equational_fun_axioms ext_ctxt x of
4.1910 - [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
4.1911 - strip_comb t1 |> snd |> forall is_Var
4.1912 - | _ => false
4.1913 -
4.1914 -type special = int list * term list * styp
4.1915 -
4.1916 -(* styp -> special -> special -> term *)
4.1917 -fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
4.1918 - let
4.1919 - val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
4.1920 - val Ts = binder_types T
4.1921 - val max_j = fold (fold Integer.max) [js1, js2] ~1
4.1922 - val (eqs, (args1, args2)) =
4.1923 - fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
4.1924 - (js1 ~~ ts1, js2 ~~ ts2) of
4.1925 - (SOME t1, SOME t2) => apfst (cons (t1, t2))
4.1926 - | (SOME t1, NONE) => apsnd (apsnd (cons t1))
4.1927 - | (NONE, SOME t2) => apsnd (apfst (cons t2))
4.1928 - | (NONE, NONE) =>
4.1929 - let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
4.1930 - nth Ts j) in
4.1931 - apsnd (pairself (cons v))
4.1932 - end) (max_j downto 0) ([], ([], []))
4.1933 - in
4.1934 - Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
4.1935 - |> map Logic.mk_equals,
4.1936 - Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
4.1937 - list_comb (Const x2, bounds2 @ args2)))
4.1938 - |> Refute.close_form (* TODO: needed? *)
4.1939 - end
4.1940 -
4.1941 -(* extended_context -> styp list -> term list *)
4.1942 -fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs =
4.1943 - let
4.1944 - val groups =
4.1945 - !special_funs
4.1946 - |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
4.1947 - |> AList.group (op =)
4.1948 - |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
4.1949 - |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
4.1950 - (* special -> int *)
4.1951 - fun generality (js, _, _) = ~(length js)
4.1952 - (* special -> special -> bool *)
4.1953 - fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
4.1954 - x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
4.1955 - (j2 ~~ t2, j1 ~~ t1)
4.1956 - (* styp -> special list -> special list -> special list -> term list
4.1957 - -> term list *)
4.1958 - fun do_pass_1 _ [] [_] [_] = I
4.1959 - | do_pass_1 x skipped _ [] = do_pass_2 x skipped
4.1960 - | do_pass_1 x skipped all (z :: zs) =
4.1961 - case filter (is_more_specific z) all
4.1962 - |> sort (int_ord o pairself generality) of
4.1963 - [] => do_pass_1 x (z :: skipped) all zs
4.1964 - | (z' :: _) => cons (special_congruence_axiom x z z')
4.1965 - #> do_pass_1 x skipped all zs
4.1966 - (* styp -> special list -> term list -> term list *)
4.1967 - and do_pass_2 _ [] = I
4.1968 - | do_pass_2 x (z :: zs) =
4.1969 - fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
4.1970 - in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
4.1971 -
4.1972 -(* term -> bool *)
4.1973 -val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
4.1974 -
4.1975 -(* 'a Symtab.table -> 'a list *)
4.1976 -fun all_table_entries table = Symtab.fold (append o snd) table []
4.1977 -(* const_table -> string -> const_table *)
4.1978 -fun extra_table table s = Symtab.make [(s, all_table_entries table)]
4.1979 -
4.1980 -(* extended_context -> term -> (term list * term list) * (bool * bool) *)
4.1981 -fun axioms_for_term
4.1982 - (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
4.1983 - def_table, nondef_table, user_nondefs, ...}) t =
4.1984 - let
4.1985 - type accumulator = styp list * (term list * term list)
4.1986 - (* (term list * term list -> term list)
4.1987 - -> ((term list -> term list) -> term list * term list
4.1988 - -> term list * term list)
4.1989 - -> int -> term -> accumulator -> accumulator *)
4.1990 - fun add_axiom get app depth t (accum as (xs, axs)) =
4.1991 - let
4.1992 - val t = t |> unfold_defs_in_term ext_ctxt
4.1993 - |> skolemize_term_and_more ext_ctxt ~1
4.1994 - in
4.1995 - if is_trivial_equation t then
4.1996 - accum
4.1997 - else
4.1998 - let val t' = t |> specialize_consts_in_term ext_ctxt depth in
4.1999 - if exists (member (op aconv) (get axs)) [t, t'] then accum
4.2000 - else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
4.2001 - end
4.2002 - end
4.2003 - (* int -> term -> accumulator -> accumulator *)
4.2004 - and add_def_axiom depth = add_axiom fst apfst depth
4.2005 - and add_nondef_axiom depth = add_axiom snd apsnd depth
4.2006 - and add_maybe_def_axiom depth t =
4.2007 - (if head_of t <> @{const "==>"} then add_def_axiom
4.2008 - else add_nondef_axiom) depth t
4.2009 - and add_eq_axiom depth t =
4.2010 - (if is_constr_pattern_formula thy t then add_def_axiom
4.2011 - else add_nondef_axiom) depth t
4.2012 - (* int -> term -> accumulator -> accumulator *)
4.2013 - and add_axioms_for_term depth t (accum as (xs, axs)) =
4.2014 - case t of
4.2015 - t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
4.2016 - | Const (x as (s, T)) =>
4.2017 - (if member (op =) xs x orelse is_built_in_const fast_descrs x then
4.2018 - accum
4.2019 - else
4.2020 - let val accum as (xs, _) = (x :: xs, axs) in
4.2021 - if depth > axioms_max_depth then
4.2022 - raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\
4.2023 - \add_axioms_for_term",
4.2024 - "too many nested axioms (" ^
4.2025 - string_of_int depth ^ ")")
4.2026 - else if Refute.is_const_of_class thy x then
4.2027 - let
4.2028 - val class = Logic.class_of_const s
4.2029 - val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
4.2030 - class)
4.2031 - val ax1 = try (Refute.specialize_type thy x) of_class
4.2032 - val ax2 = Option.map (Refute.specialize_type thy x o snd)
4.2033 - (Refute.get_classdef thy class)
4.2034 - in
4.2035 - fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
4.2036 - accum
4.2037 - end
4.2038 - else if is_constr thy x then
4.2039 - accum
4.2040 - else if is_equational_fun ext_ctxt x then
4.2041 - fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
4.2042 - accum
4.2043 - else if is_abs_fun thy x then
4.2044 - if is_quot_type thy (range_type T) then
4.2045 - raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
4.2046 - else
4.2047 - accum |> fold (add_nondef_axiom depth)
4.2048 - (nondef_props_for_const thy false nondef_table x)
4.2049 - |> is_funky_typedef thy (range_type T)
4.2050 - ? fold (add_maybe_def_axiom depth)
4.2051 - (nondef_props_for_const thy true
4.2052 - (extra_table def_table s) x)
4.2053 - else if is_rep_fun thy x then
4.2054 - if is_quot_type thy (domain_type T) then
4.2055 - raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
4.2056 - else
4.2057 - accum |> fold (add_nondef_axiom depth)
4.2058 - (nondef_props_for_const thy false nondef_table x)
4.2059 - |> is_funky_typedef thy (range_type T)
4.2060 - ? fold (add_maybe_def_axiom depth)
4.2061 - (nondef_props_for_const thy true
4.2062 - (extra_table def_table s) x)
4.2063 - |> add_axioms_for_term depth
4.2064 - (Const (mate_of_rep_fun thy x))
4.2065 - |> fold (add_def_axiom depth)
4.2066 - (inverse_axioms_for_rep_fun thy x)
4.2067 - else
4.2068 - accum |> user_axioms <> SOME false
4.2069 - ? fold (add_nondef_axiom depth)
4.2070 - (nondef_props_for_const thy false nondef_table x)
4.2071 - end)
4.2072 - |> add_axioms_for_type depth T
4.2073 - | Free (_, T) => add_axioms_for_type depth T accum
4.2074 - | Var (_, T) => add_axioms_for_type depth T accum
4.2075 - | Bound _ => accum
4.2076 - | Abs (_, T, t) => accum |> add_axioms_for_term depth t
4.2077 - |> add_axioms_for_type depth T
4.2078 - (* int -> typ -> accumulator -> accumulator *)
4.2079 - and add_axioms_for_type depth T =
4.2080 - case T of
4.2081 - Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
4.2082 - | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
4.2083 - | @{typ prop} => I
4.2084 - | @{typ bool} => I
4.2085 - | @{typ unit} => I
4.2086 - | TFree (_, S) => add_axioms_for_sort depth T S
4.2087 - | TVar (_, S) => add_axioms_for_sort depth T S
4.2088 - | Type (z as (s, Ts)) =>
4.2089 - fold (add_axioms_for_type depth) Ts
4.2090 - #> (if is_pure_typedef thy T then
4.2091 - fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
4.2092 - else if is_quot_type thy T then
4.2093 - fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
4.2094 - else if max_bisim_depth >= 0 andalso is_codatatype thy T then
4.2095 - fold (add_maybe_def_axiom depth)
4.2096 - (codatatype_bisim_axioms ext_ctxt T)
4.2097 - else
4.2098 - I)
4.2099 - (* int -> typ -> sort -> accumulator -> accumulator *)
4.2100 - and add_axioms_for_sort depth T S =
4.2101 - let
4.2102 - val supers = Sign.complete_sort thy S
4.2103 - val class_axioms =
4.2104 - maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
4.2105 - handle ERROR _ => [])) supers
4.2106 - val monomorphic_class_axioms =
4.2107 - map (fn t => case Term.add_tvars t [] of
4.2108 - [] => t
4.2109 - | [(x, S)] =>
4.2110 - Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
4.2111 - | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
4.2112 - \add_axioms_for_sort", [t]))
4.2113 - class_axioms
4.2114 - in fold (add_nondef_axiom depth) monomorphic_class_axioms end
4.2115 - val (mono_user_nondefs, poly_user_nondefs) =
4.2116 - List.partition (null o Term.hidden_polymorphism) user_nondefs
4.2117 - val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
4.2118 - evals
4.2119 - val (xs, (defs, nondefs)) =
4.2120 - ([], ([], [])) |> add_axioms_for_term 1 t
4.2121 - |> fold_rev (add_def_axiom 1) eval_axioms
4.2122 - |> user_axioms = SOME true
4.2123 - ? fold (add_nondef_axiom 1) mono_user_nondefs
4.2124 - val defs = defs @ special_congruence_axioms ext_ctxt xs
4.2125 - in
4.2126 - ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
4.2127 - null poly_user_nondefs))
4.2128 - end
4.2129 +(* hol_context -> typ -> typ list *)
4.2130 +fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T []
4.2131 +(* hol_context -> term list -> typ list *)
4.2132 +fun ground_types_in_terms hol_ctxt ts =
4.2133 + fold (fold_types (add_ground_types hol_ctxt)) ts []
4.2134
4.2135 (* theory -> const_table -> styp -> int list *)
4.2136 fun const_format thy def_table (x as (s, T)) =
4.2137 @@ -3356,10 +2096,10 @@
4.2138 |> map (rev o filter_out (member (op =) js))
4.2139 |> filter_out null |> map length |> rev
4.2140
4.2141 -(* extended_context -> string * string -> (term option * int list) list
4.2142 +(* hol_context -> string * string -> (term option * int list) list
4.2143 -> styp -> term * typ *)
4.2144 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
4.2145 - : extended_context) (base_name, step_name) formats =
4.2146 + : hol_context) (base_name, step_name) formats =
4.2147 let
4.2148 val default_format = the (AList.lookup (op =) formats NONE)
4.2149 (* styp -> term * typ *)
4.2150 @@ -3460,7 +2200,7 @@
4.2151 (t, format_term_type thy def_table formats t)
4.2152 end)
4.2153 |>> map_types unbit_and_unbox_type
4.2154 - |>> shorten_names_in_term |>> shorten_abs_vars
4.2155 + |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
4.2156 in do_const end
4.2157
4.2158 (* styp -> string *)
4.2159 @@ -3474,84 +2214,4 @@
4.2160 else
4.2161 "="
4.2162
4.2163 -val binary_int_threshold = 4
4.2164 -
4.2165 -(* term -> bool *)
4.2166 -fun may_use_binary_ints (t1 $ t2) =
4.2167 - may_use_binary_ints t1 andalso may_use_binary_ints t2
4.2168 - | may_use_binary_ints (t as Const (s, _)) =
4.2169 - t <> @{const Suc} andalso
4.2170 - not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
4.2171 - @{const_name nat_gcd}, @{const_name nat_lcm},
4.2172 - @{const_name Frac}, @{const_name norm_frac}] s)
4.2173 - | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
4.2174 - | may_use_binary_ints _ = true
4.2175 -fun should_use_binary_ints (t1 $ t2) =
4.2176 - should_use_binary_ints t1 orelse should_use_binary_ints t2
4.2177 - | should_use_binary_ints (Const (s, _)) =
4.2178 - member (op =) [@{const_name times_nat_inst.times_nat},
4.2179 - @{const_name div_nat_inst.div_nat},
4.2180 - @{const_name times_int_inst.times_int},
4.2181 - @{const_name div_int_inst.div_int}] s orelse
4.2182 - (String.isPrefix numeral_prefix s andalso
4.2183 - let val n = the (Int.fromString (unprefix numeral_prefix s)) in
4.2184 - n <= ~ binary_int_threshold orelse n >= binary_int_threshold
4.2185 - end)
4.2186 - | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
4.2187 - | should_use_binary_ints _ = false
4.2188 -
4.2189 -(* typ -> typ *)
4.2190 -fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
4.2191 - | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
4.2192 - | binarize_nat_and_int_in_type (Type (s, Ts)) =
4.2193 - Type (s, map binarize_nat_and_int_in_type Ts)
4.2194 - | binarize_nat_and_int_in_type T = T
4.2195 -(* term -> term *)
4.2196 -val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
4.2197 -
4.2198 -(* extended_context -> term
4.2199 - -> ((term list * term list) * (bool * bool)) * term *)
4.2200 -fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes,
4.2201 - skolemize, uncurry, ...}) t =
4.2202 - let
4.2203 - val skolem_depth = if skolemize then 4 else ~1
4.2204 - val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
4.2205 - core_t) = t |> unfold_defs_in_term ext_ctxt
4.2206 - |> Refute.close_form
4.2207 - |> skolemize_term_and_more ext_ctxt skolem_depth
4.2208 - |> specialize_consts_in_term ext_ctxt 0
4.2209 - |> `(axioms_for_term ext_ctxt)
4.2210 - val binarize =
4.2211 - case binary_ints of
4.2212 - SOME false => false
4.2213 - | _ =>
4.2214 - forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
4.2215 - (binary_ints = SOME true orelse
4.2216 - exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
4.2217 - val box = exists (not_equal (SOME false) o snd) boxes
4.2218 - val table =
4.2219 - Termtab.empty |> uncurry
4.2220 - ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
4.2221 - (* bool -> bool -> term -> term *)
4.2222 - fun do_rest def core =
4.2223 - binarize ? binarize_nat_and_int_in_term
4.2224 - #> uncurry ? uncurry_term table
4.2225 - #> box ? box_fun_and_pair_in_term ext_ctxt def
4.2226 - #> destroy_constrs ? (pull_out_universal_constrs thy def
4.2227 - #> pull_out_existential_constrs thy
4.2228 - #> destroy_pulled_out_constrs ext_ctxt def)
4.2229 - #> curry_assms
4.2230 - #> destroy_universal_equalities
4.2231 - #> destroy_existential_equalities thy
4.2232 - #> simplify_constrs_and_sels thy
4.2233 - #> distribute_quantifiers
4.2234 - #> push_quantifiers_inward thy
4.2235 - #> not core ? Refute.close_form
4.2236 - #> shorten_abs_vars
4.2237 - in
4.2238 - (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
4.2239 - (got_all_mono_user_axioms, no_poly_user_axioms)),
4.2240 - do_rest false true core_t)
4.2241 - end
4.2242 -
4.2243 end;
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 04 13:36:52 2010 +0100
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 04 16:03:15 2010 +0100
5.3 @@ -7,7 +7,7 @@
5.4
5.5 signature NITPICK_KODKOD =
5.6 sig
5.7 - type extended_context = Nitpick_HOL.extended_context
5.8 + type hol_context = Nitpick_HOL.hol_context
5.9 type dtype_spec = Nitpick_Scope.dtype_spec
5.10 type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
5.11 type nut = Nitpick_Nut.nut
5.12 @@ -33,7 +33,7 @@
5.13 val merge_bounds : Kodkod.bound list -> Kodkod.bound list
5.14 val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
5.15 val declarative_axioms_for_datatypes :
5.16 - extended_context -> int -> int Typtab.table -> kodkod_constrs
5.17 + hol_context -> int -> int Typtab.table -> kodkod_constrs
5.18 -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
5.19 val kodkod_formula_from_nut :
5.20 int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
5.21 @@ -732,12 +732,12 @@
5.22 (* nut NameTable.table -> styp -> KK.rel_expr *)
5.23 fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
5.24
5.25 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
5.26 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
5.27 -> styp -> int -> nfa_transition list *)
5.28 -fun nfa_transitions_for_sel ext_ctxt ({kk_project, ...} : kodkod_constrs)
5.29 +fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
5.30 rel_table (dtypes : dtype_spec list) constr_x n =
5.31 let
5.32 - val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt constr_x n
5.33 + val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
5.34 val (r, R, arity) = const_triple rel_table x
5.35 val type_schema = type_schema_of_rep T R
5.36 in
5.37 @@ -746,17 +746,17 @@
5.38 else SOME (kk_project r (map KK.Num [0, j]), T))
5.39 (index_seq 1 (arity - 1) ~~ tl type_schema)
5.40 end
5.41 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
5.42 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
5.43 -> styp -> nfa_transition list *)
5.44 -fun nfa_transitions_for_constr ext_ctxt kk rel_table dtypes (x as (_, T)) =
5.45 - maps (nfa_transitions_for_sel ext_ctxt kk rel_table dtypes x)
5.46 +fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
5.47 + maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
5.48 (index_seq 0 (num_sels_for_constr_type T))
5.49 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
5.50 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
5.51 -> dtype_spec -> nfa_entry option *)
5.52 fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
5.53 | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
5.54 - | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
5.55 - SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
5.56 + | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
5.57 + SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
5.58 o #const) constrs)
5.59
5.60 val empty_rel = KK.Product (KK.None, KK.None)
5.61 @@ -812,23 +812,23 @@
5.62 fun acyclicity_axiom_for_datatype dtypes kk nfa start =
5.63 #kk_no kk (#kk_intersect kk
5.64 (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
5.65 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
5.66 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
5.67 -> KK.formula list *)
5.68 -fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes =
5.69 - map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes
5.70 +fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
5.71 + map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
5.72 |> strongly_connected_sub_nfas
5.73 |> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst)
5.74 nfa)
5.75
5.76 -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
5.77 - -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
5.78 -fun sel_axiom_for_sel ext_ctxt j0
5.79 +(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
5.80 + -> constr_spec -> int -> KK.formula *)
5.81 +fun sel_axiom_for_sel hol_ctxt j0
5.82 (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
5.83 kk_join, ...}) rel_table dom_r
5.84 ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
5.85 n =
5.86 let
5.87 - val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt const n
5.88 + val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
5.89 val (r, R, arity) = const_triple rel_table x
5.90 val R2 = dest_Func R |> snd
5.91 val z = (epsilon - delta, delta + j0)
5.92 @@ -842,9 +842,9 @@
5.93 (kk_n_ary_function kk R2 r') (kk_no r'))
5.94 end
5.95 end
5.96 -(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
5.97 +(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
5.98 -> constr_spec -> KK.formula list *)
5.99 -fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
5.100 +fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
5.101 (constr as {const, delta, epsilon, explicit_max, ...}) =
5.102 let
5.103 val honors_explicit_max =
5.104 @@ -866,19 +866,19 @@
5.105 " too small for \"max\"")
5.106 in
5.107 max_axiom ::
5.108 - map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr)
5.109 + map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr)
5.110 (index_seq 0 (num_sels_for_constr_type (snd const)))
5.111 end
5.112 end
5.113 -(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
5.114 +(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
5.115 -> dtype_spec -> KK.formula list *)
5.116 -fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
5.117 +fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
5.118 ({constrs, ...} : dtype_spec) =
5.119 - maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
5.120 + maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
5.121
5.122 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
5.123 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
5.124 -> KK.formula list *)
5.125 -fun uniqueness_axiom_for_constr ext_ctxt
5.126 +fun uniqueness_axiom_for_constr hol_ctxt
5.127 ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
5.128 : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
5.129 let
5.130 @@ -887,7 +887,7 @@
5.131 kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
5.132 val num_sels = num_sels_for_constr_type (snd const)
5.133 val triples = map (const_triple rel_table
5.134 - o boxed_nth_sel_for_constr ext_ctxt const)
5.135 + o boxed_nth_sel_for_constr hol_ctxt const)
5.136 (~1 upto num_sels - 1)
5.137 val j0 = case triples |> hd |> #2 of
5.138 Func (Atom (_, j0), _) => j0
5.139 @@ -903,11 +903,11 @@
5.140 (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
5.141 (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
5.142 end
5.143 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
5.144 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
5.145 -> KK.formula list *)
5.146 -fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table
5.147 +fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
5.148 ({constrs, ...} : dtype_spec) =
5.149 - map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs
5.150 + map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
5.151
5.152 (* constr_spec -> int *)
5.153 fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
5.154 @@ -924,22 +924,22 @@
5.155 kk_disjoint_sets kk rs]
5.156 end
5.157
5.158 -(* extended_context -> int -> int Typtab.table -> kodkod_constrs
5.159 +(* hol_context -> int -> int Typtab.table -> kodkod_constrs
5.160 -> nut NameTable.table -> dtype_spec -> KK.formula list *)
5.161 fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
5.162 - | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
5.163 + | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
5.164 (dtype as {typ, ...}) =
5.165 let val j0 = offset_of_type ofs typ in
5.166 - sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @
5.167 - uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
5.168 + sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
5.169 + uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
5.170 partition_axioms_for_datatype j0 kk rel_table dtype
5.171 end
5.172
5.173 -(* extended_context -> int -> int Typtab.table -> kodkod_constrs
5.174 +(* hol_context -> int -> int Typtab.table -> kodkod_constrs
5.175 -> nut NameTable.table -> dtype_spec list -> KK.formula list *)
5.176 -fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
5.177 - acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
5.178 - maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
5.179 +fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
5.180 + acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
5.181 + maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
5.182
5.183 (* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
5.184 fun kodkod_formula_from_nut bits ofs liberal
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 04 13:36:52 2010 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 04 16:03:15 2010 +0100
6.3 @@ -251,7 +251,7 @@
6.4 -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
6.5 -> int list list -> term *)
6.6 fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
6.7 - ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
6.8 + ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
6.9 : scope) sel_names rel_table bounds =
6.10 let
6.11 val for_auto = (maybe_name = "")
6.12 @@ -400,7 +400,7 @@
6.13 else NONE)
6.14 (discr_jsss ~~ constrs) |> the
6.15 val arg_Ts = curried_binder_types constr_T
6.16 - val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x)
6.17 + val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x)
6.18 (index_seq 0 (length arg_Ts))
6.19 val sel_Rs =
6.20 map (fn x => get_first
6.21 @@ -586,7 +586,7 @@
6.22 -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
6.23 -> Pretty.T * bool *)
6.24 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
6.25 - ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
6.26 + ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
6.27 user_axioms, debug, binary_ints, destroy_constrs,
6.28 specialize, skolemize, star_linear_preds, uncurry,
6.29 fast_descrs, tac_timeout, evals, case_names, def_table,
6.30 @@ -598,7 +598,7 @@
6.31 let
6.32 val (wacky_names as (_, base_name, step_name, _), ctxt) =
6.33 add_wacky_syntax ctxt
6.34 - val ext_ctxt =
6.35 + val hol_ctxt =
6.36 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
6.37 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
6.38 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
6.39 @@ -612,7 +612,7 @@
6.40 ersatz_table = ersatz_table, skolems = skolems,
6.41 special_funs = special_funs, unrolled_preds = unrolled_preds,
6.42 wf_cache = wf_cache, constr_cache = constr_cache}
6.43 - val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
6.44 + val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
6.45 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
6.46 ofs = ofs}
6.47 (* typ -> typ -> rep -> int list list -> term *)
6.48 @@ -644,7 +644,7 @@
6.49 end
6.50 | ConstName (s, T, _) =>
6.51 (assign_operator_for_const (s, T),
6.52 - user_friendly_const ext_ctxt (base_name, step_name) formats (s, T),
6.53 + user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
6.54 T)
6.55 | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
6.56 \pretty_for_assign", [name])
6.57 @@ -724,7 +724,7 @@
6.58
6.59 (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
6.60 -> KK.raw_bound list -> term -> bool option *)
6.61 -fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, debug, ...},
6.62 +fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
6.63 card_assigns, ...})
6.64 auto_timeout free_names sel_names rel_table bounds prop =
6.65 let
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 04 13:36:52 2010 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 04 16:03:15 2010 +0100
7.3 @@ -8,10 +8,10 @@
7.4 signature NITPICK_MONO =
7.5 sig
7.6 datatype sign = Plus | Minus
7.7 - type extended_context = Nitpick_HOL.extended_context
7.8 + type hol_context = Nitpick_HOL.hol_context
7.9
7.10 val formulas_monotonic :
7.11 - extended_context -> typ -> sign -> term list -> term list -> term -> bool
7.12 + hol_context -> typ -> sign -> term list -> term list -> term -> bool
7.13 end;
7.14
7.15 structure Nitpick_Mono : NITPICK_MONO =
7.16 @@ -35,7 +35,7 @@
7.17 CRec of string * typ list
7.18
7.19 type cdata =
7.20 - {ext_ctxt: extended_context,
7.21 + {hol_ctxt: hol_context,
7.22 alpha_T: typ,
7.23 max_fresh: int Unsynchronized.ref,
7.24 datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
7.25 @@ -114,9 +114,9 @@
7.26 | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
7.27 | flatten_ctype C = [C]
7.28
7.29 -(* extended_context -> typ -> cdata *)
7.30 -fun initial_cdata ext_ctxt alpha_T =
7.31 - ({ext_ctxt = ext_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
7.32 +(* hol_context -> typ -> cdata *)
7.33 +fun initial_cdata hol_ctxt alpha_T =
7.34 + ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
7.35 datatype_cache = Unsynchronized.ref [],
7.36 constr_cache = Unsynchronized.ref []} : cdata)
7.37
7.38 @@ -188,7 +188,7 @@
7.39 in List.app repair_one (!constr_cache) end
7.40
7.41 (* cdata -> typ -> ctype *)
7.42 -fun fresh_ctype_for_type ({ext_ctxt as {thy, ...}, alpha_T, max_fresh,
7.43 +fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, alpha_T, max_fresh,
7.44 datatype_cache, constr_cache, ...} : cdata) =
7.45 let
7.46 (* typ -> typ -> ctype *)
7.47 @@ -217,7 +217,7 @@
7.48 | NONE =>
7.49 let
7.50 val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
7.51 - val xs = datatype_constrs ext_ctxt T
7.52 + val xs = datatype_constrs hol_ctxt T
7.53 val (all_Cs, constr_Cs) =
7.54 fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
7.55 let
7.56 @@ -264,7 +264,7 @@
7.57 end
7.58
7.59 (* cdata -> styp -> ctype *)
7.60 -fun ctype_for_constr (cdata as {ext_ctxt as {thy, ...}, alpha_T, constr_cache,
7.61 +fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
7.62 ...}) (x as (_, T)) =
7.63 if could_exist_alpha_sub_ctype thy alpha_T T then
7.64 case AList.lookup (op =) (!constr_cache) x of
7.65 @@ -278,8 +278,8 @@
7.66 AList.lookup (op =) (!constr_cache) x |> the)
7.67 else
7.68 fresh_ctype_for_type cdata T
7.69 -fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =
7.70 - x |> boxed_constr_for_sel ext_ctxt |> ctype_for_constr cdata
7.71 +fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
7.72 + x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
7.73 |> sel_ctype_from_constr_ctype s
7.74
7.75 (* literal list -> ctype -> ctype *)
7.76 @@ -549,7 +549,7 @@
7.77 handle List.Empty => initial_gamma
7.78
7.79 (* cdata -> term -> accumulator -> ctype * accumulator *)
7.80 -fun consider_term (cdata as {ext_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
7.81 +fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
7.82 max_fresh, ...}) =
7.83 let
7.84 (* typ -> ctype *)
7.85 @@ -806,7 +806,7 @@
7.86 in do_term end
7.87
7.88 (* cdata -> sign -> term -> accumulator -> accumulator *)
7.89 -fun consider_general_formula (cdata as {ext_ctxt as {ctxt, ...}, ...}) =
7.90 +fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
7.91 let
7.92 (* typ -> ctype *)
7.93 val ctype_for = fresh_ctype_for_type cdata
7.94 @@ -895,7 +895,7 @@
7.95 not (is_harmless_axiom t) ? consider_general_formula cdata sn t
7.96
7.97 (* cdata -> term -> accumulator -> accumulator *)
7.98 -fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =
7.99 +fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
7.100 if not (is_constr_pattern_formula thy t) then
7.101 consider_nondefinitional_axiom cdata Plus t
7.102 else if is_harmless_axiom t then
7.103 @@ -945,13 +945,13 @@
7.104 map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
7.105 |> cat_lines |> print_g
7.106
7.107 -(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *)
7.108 -fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
7.109 +(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
7.110 +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
7.111 core_t =
7.112 let
7.113 val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
7.114 Syntax.string_of_typ ctxt alpha_T)
7.115 - val cdata as {max_fresh, ...} = initial_cdata ext_ctxt alpha_T
7.116 + val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
7.117 val (gamma, cset) =
7.118 (initial_gamma, slack)
7.119 |> fold (consider_definitional_axiom cdata) def_ts
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 04 13:36:52 2010 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 04 16:03:15 2010 +0100
8.3 @@ -8,7 +8,7 @@
8.4 signature NITPICK_NUT =
8.5 sig
8.6 type special_fun = Nitpick_HOL.special_fun
8.7 - type extended_context = Nitpick_HOL.extended_context
8.8 + type hol_context = Nitpick_HOL.hol_context
8.9 type scope = Nitpick_Scope.scope
8.10 type name_pool = Nitpick_Peephole.name_pool
8.11 type rep = Nitpick_Rep.rep
8.12 @@ -106,7 +106,7 @@
8.13 val name_ord : (nut * nut) -> order
8.14 val the_name : 'a NameTable.table -> nut -> 'a
8.15 val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
8.16 - val nut_from_term : extended_context -> op2 -> term -> nut
8.17 + val nut_from_term : hol_context -> op2 -> term -> nut
8.18 val choose_reps_for_free_vars :
8.19 scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
8.20 val choose_reps_for_consts :
8.21 @@ -466,8 +466,8 @@
8.22 fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
8.23 | factorize z = [z]
8.24
8.25 -(* extended_context -> op2 -> term -> nut *)
8.26 -fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
8.27 +(* hol_context -> op2 -> term -> nut *)
8.28 +fun nut_from_term (hol_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
8.29 let
8.30 (* string list -> typ list -> term -> nut *)
8.31 fun aux eq ss Ts t =
8.32 @@ -597,7 +597,7 @@
8.33 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
8.34 | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
8.35 | (Const (@{const_name finite}, T), [t1]) =>
8.36 - (if is_finite_type ext_ctxt (domain_type T) then
8.37 + (if is_finite_type hol_ctxt (domain_type T) then
8.38 Cst (True, bool_T, Any)
8.39 else case t1 of
8.40 Const (@{const_name top}, _) => Cst (False, bool_T, Any)
8.41 @@ -712,7 +712,7 @@
8.42 in (v :: vs, NameTable.update (v, R) table) end
8.43 (* scope -> bool -> nut -> nut list * rep NameTable.table
8.44 -> nut list * rep NameTable.table *)
8.45 -fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes,
8.46 +fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes,
8.47 ofs, ...}) all_exact v (vs, table) =
8.48 let
8.49 val x as (s, T) = (nickname_of v, type_of v)
8.50 @@ -747,10 +747,10 @@
8.51
8.52 (* scope -> styp -> int -> nut list * rep NameTable.table
8.53 -> nut list * rep NameTable.table *)
8.54 -fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n
8.55 +fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n
8.56 (vs, table) =
8.57 let
8.58 - val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
8.59 + val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n
8.60 val R' = if n = ~1 orelse is_word_type (body_type T) orelse
8.61 (is_fun_type (range_type T') andalso
8.62 is_boolean_type (body_type T')) then
8.63 @@ -890,7 +890,7 @@
8.64 | untuple f u = if rep_of u = Unit then [] else [f u]
8.65
8.66 (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
8.67 -fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns,
8.68 +fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
8.69 bits, datatypes, ofs, ...})
8.70 liberal table def =
8.71 let
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Feb 04 16:03:15 2010 +0100
9.3 @@ -0,0 +1,1431 @@
9.4 +(* Title: HOL/Tools/Nitpick/nitpick_preproc.ML
9.5 + Author: Jasmin Blanchette, TU Muenchen
9.6 + Copyright 2008, 2009, 2010
9.7 +
9.8 +Nitpick's HOL preprocessor.
9.9 +*)
9.10 +
9.11 +signature NITPICK_PREPROC =
9.12 +sig
9.13 + type hol_context = Nitpick_HOL.hol_context
9.14 + val preprocess_term :
9.15 + hol_context -> term -> ((term list * term list) * (bool * bool)) * term
9.16 +end
9.17 +
9.18 +structure Nitpick_Preproc : NITPICK_PREPROC =
9.19 +struct
9.20 +
9.21 +open Nitpick_Util
9.22 +open Nitpick_HOL
9.23 +
9.24 +(* polarity -> string -> bool *)
9.25 +fun is_positive_existential polar quant_s =
9.26 + (polar = Pos andalso quant_s = @{const_name Ex}) orelse
9.27 + (polar = Neg andalso quant_s <> @{const_name Ex})
9.28 +
9.29 +(** Binary coding of integers **)
9.30 +
9.31 +(* If a formula contains a numeral whose absolute value is more than this
9.32 + threshold, the unary coding is likely not to work well and we prefer the
9.33 + binary coding. *)
9.34 +val binary_int_threshold = 3
9.35 +
9.36 +(* term -> bool *)
9.37 +fun may_use_binary_ints (t1 $ t2) =
9.38 + may_use_binary_ints t1 andalso may_use_binary_ints t2
9.39 + | may_use_binary_ints (t as Const (s, _)) =
9.40 + t <> @{const Suc} andalso
9.41 + not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
9.42 + @{const_name nat_gcd}, @{const_name nat_lcm},
9.43 + @{const_name Frac}, @{const_name norm_frac}] s)
9.44 + | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
9.45 + | may_use_binary_ints _ = true
9.46 +fun should_use_binary_ints (t1 $ t2) =
9.47 + should_use_binary_ints t1 orelse should_use_binary_ints t2
9.48 + | should_use_binary_ints (Const (s, _)) =
9.49 + member (op =) [@{const_name times_nat_inst.times_nat},
9.50 + @{const_name div_nat_inst.div_nat},
9.51 + @{const_name times_int_inst.times_int},
9.52 + @{const_name div_int_inst.div_int}] s orelse
9.53 + (String.isPrefix numeral_prefix s andalso
9.54 + let val n = the (Int.fromString (unprefix numeral_prefix s)) in
9.55 + n < ~ binary_int_threshold orelse n > binary_int_threshold
9.56 + end)
9.57 + | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
9.58 + | should_use_binary_ints _ = false
9.59 +
9.60 +(* typ -> typ *)
9.61 +fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
9.62 + | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
9.63 + | binarize_nat_and_int_in_type (Type (s, Ts)) =
9.64 + Type (s, map binarize_nat_and_int_in_type Ts)
9.65 + | binarize_nat_and_int_in_type T = T
9.66 +(* term -> term *)
9.67 +val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
9.68 +
9.69 +(** Uncurrying **)
9.70 +
9.71 +(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
9.72 +fun add_to_uncurry_table thy t =
9.73 + let
9.74 + (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
9.75 + fun aux (t1 $ t2) args table =
9.76 + let val table = aux t2 [] table in aux t1 (t2 :: args) table end
9.77 + | aux (Abs (_, _, t')) _ table = aux t' [] table
9.78 + | aux (t as Const (x as (s, _))) args table =
9.79 + if is_built_in_const true x orelse is_constr_like thy x orelse
9.80 + is_sel s orelse s = @{const_name Sigma} then
9.81 + table
9.82 + else
9.83 + Termtab.map_default (t, 65536) (curry Int.min (length args)) table
9.84 + | aux _ _ table = table
9.85 + in aux t [] end
9.86 +
9.87 +(* int -> int -> string *)
9.88 +fun uncurry_prefix_for k j =
9.89 + uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
9.90 +
9.91 +(* int Termtab.tab term -> term *)
9.92 +fun uncurry_term table t =
9.93 + let
9.94 + (* term -> term list -> term *)
9.95 + fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
9.96 + | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
9.97 + | aux (t as Const (s, T)) args =
9.98 + (case Termtab.lookup table t of
9.99 + SOME n =>
9.100 + if n >= 2 then
9.101 + let
9.102 + val (arg_Ts, rest_T) = strip_n_binders n T
9.103 + val j =
9.104 + if hd arg_Ts = @{typ bisim_iterator} orelse
9.105 + is_fp_iterator_type (hd arg_Ts) then
9.106 + 1
9.107 + else case find_index (not_equal bool_T) arg_Ts of
9.108 + ~1 => n
9.109 + | j => j
9.110 + val ((before_args, tuple_args), after_args) =
9.111 + args |> chop n |>> chop j
9.112 + val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
9.113 + T |> strip_n_binders n |>> chop j
9.114 + val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
9.115 + in
9.116 + if n - j < 2 then
9.117 + betapplys (t, args)
9.118 + else
9.119 + betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
9.120 + before_arg_Ts ---> tuple_T --> rest_T),
9.121 + before_args @ [mk_flat_tuple tuple_T tuple_args] @
9.122 + after_args)
9.123 + end
9.124 + else
9.125 + betapplys (t, args)
9.126 + | NONE => betapplys (t, args))
9.127 + | aux t args = betapplys (t, args)
9.128 + in aux t [] end
9.129 +
9.130 +(** Boxing **)
9.131 +
9.132 +(* hol_context -> typ -> term -> term *)
9.133 +fun constr_expand (hol_ctxt as {thy, ...}) T t =
9.134 + (case head_of t of
9.135 + Const x => if is_constr_like thy x then t else raise SAME ()
9.136 + | _ => raise SAME ())
9.137 + handle SAME () =>
9.138 + let
9.139 + val x' as (_, T') =
9.140 + if is_pair_type T then
9.141 + let val (T1, T2) = HOLogic.dest_prodT T in
9.142 + (@{const_name Pair}, T1 --> T2 --> T)
9.143 + end
9.144 + else
9.145 + datatype_constrs hol_ctxt T |> hd
9.146 + val arg_Ts = binder_types T'
9.147 + in
9.148 + list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
9.149 + (index_seq 0 (length arg_Ts)) arg_Ts)
9.150 + end
9.151 +
9.152 +(* hol_context -> bool -> term -> term *)
9.153 +fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =
9.154 + let
9.155 + (* typ -> typ *)
9.156 + fun box_relational_operator_type (Type ("fun", Ts)) =
9.157 + Type ("fun", map box_relational_operator_type Ts)
9.158 + | box_relational_operator_type (Type ("*", Ts)) =
9.159 + Type ("*", map (box_type hol_ctxt InPair) Ts)
9.160 + | box_relational_operator_type T = T
9.161 + (* (term -> term) -> int -> term -> term *)
9.162 + fun coerce_bound_no f j t =
9.163 + case t of
9.164 + t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
9.165 + | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
9.166 + | Bound j' => if j' = j then f t else t
9.167 + | _ => t
9.168 + (* typ -> typ -> term -> term *)
9.169 + fun coerce_bound_0_in_term new_T old_T =
9.170 + old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
9.171 + (* typ list -> typ -> term -> term *)
9.172 + and coerce_term Ts new_T old_T t =
9.173 + if old_T = new_T then
9.174 + t
9.175 + else
9.176 + case (new_T, old_T) of
9.177 + (Type (new_s, new_Ts as [new_T1, new_T2]),
9.178 + Type ("fun", [old_T1, old_T2])) =>
9.179 + (case eta_expand Ts t 1 of
9.180 + Abs (s, _, t') =>
9.181 + Abs (s, new_T1,
9.182 + t' |> coerce_bound_0_in_term new_T1 old_T1
9.183 + |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
9.184 + |> Envir.eta_contract
9.185 + |> new_s <> "fun"
9.186 + ? construct_value thy (@{const_name FunBox},
9.187 + Type ("fun", new_Ts) --> new_T) o single
9.188 + | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
9.189 + \coerce_term", [t']))
9.190 + | (Type (new_s, new_Ts as [new_T1, new_T2]),
9.191 + Type (old_s, old_Ts as [old_T1, old_T2])) =>
9.192 + if old_s = @{type_name fun_box} orelse
9.193 + old_s = @{type_name pair_box} orelse old_s = "*" then
9.194 + case constr_expand hol_ctxt old_T t of
9.195 + Const (@{const_name FunBox}, _) $ t1 =>
9.196 + if new_s = "fun" then
9.197 + coerce_term Ts new_T (Type ("fun", old_Ts)) t1
9.198 + else
9.199 + construct_value thy
9.200 + (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
9.201 + [coerce_term Ts (Type ("fun", new_Ts))
9.202 + (Type ("fun", old_Ts)) t1]
9.203 + | Const _ $ t1 $ t2 =>
9.204 + construct_value thy
9.205 + (if new_s = "*" then @{const_name Pair}
9.206 + else @{const_name PairBox}, new_Ts ---> new_T)
9.207 + [coerce_term Ts new_T1 old_T1 t1,
9.208 + coerce_term Ts new_T2 old_T2 t2]
9.209 + | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
9.210 + \coerce_term", [t'])
9.211 + else
9.212 + raise TYPE ("coerce_term", [new_T, old_T], [t])
9.213 + | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
9.214 + (* indexname * typ -> typ * term -> typ option list -> typ option list *)
9.215 + fun add_boxed_types_for_var (z as (_, T)) (T', t') =
9.216 + case t' of
9.217 + Var z' => z' = z ? insert (op =) T'
9.218 + | Const (@{const_name Pair}, _) $ t1 $ t2 =>
9.219 + (case T' of
9.220 + Type (_, [T1, T2]) =>
9.221 + fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
9.222 + | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\
9.223 + \add_boxed_types_for_var", [T'], []))
9.224 + | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
9.225 + (* typ list -> typ list -> term -> indexname * typ -> typ *)
9.226 + fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
9.227 + case t of
9.228 + @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
9.229 + | Const (s0, _) $ t1 $ _ =>
9.230 + if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
9.231 + let
9.232 + val (t', args) = strip_comb t1
9.233 + val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
9.234 + in
9.235 + case fold (add_boxed_types_for_var z)
9.236 + (fst (strip_n_binders (length args) T') ~~ args) [] of
9.237 + [T''] => T''
9.238 + | _ => T
9.239 + end
9.240 + else
9.241 + T
9.242 + | _ => T
9.243 + (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
9.244 + -> term -> term *)
9.245 + and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
9.246 + let
9.247 + val abs_T' =
9.248 + if polar = Neut orelse is_positive_existential polar quant_s then
9.249 + box_type hol_ctxt InFunLHS abs_T
9.250 + else
9.251 + abs_T
9.252 + val body_T = body_type quant_T
9.253 + in
9.254 + Const (quant_s, (abs_T' --> body_T) --> body_T)
9.255 + $ Abs (abs_s, abs_T',
9.256 + t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
9.257 + end
9.258 + (* typ list -> typ list -> string -> typ -> term -> term -> term *)
9.259 + and do_equals new_Ts old_Ts s0 T0 t1 t2 =
9.260 + let
9.261 + val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
9.262 + val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
9.263 + val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
9.264 + in
9.265 + list_comb (Const (s0, T --> T --> body_type T0),
9.266 + map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
9.267 + end
9.268 + (* string -> typ -> term *)
9.269 + and do_description_operator s T =
9.270 + let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
9.271 + Const (s, (T1 --> bool_T) --> T1)
9.272 + end
9.273 + (* typ list -> typ list -> polarity -> term -> term *)
9.274 + and do_term new_Ts old_Ts polar t =
9.275 + case t of
9.276 + Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
9.277 + do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
9.278 + | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
9.279 + do_equals new_Ts old_Ts s0 T0 t1 t2
9.280 + | @{const "==>"} $ t1 $ t2 =>
9.281 + @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
9.282 + $ do_term new_Ts old_Ts polar t2
9.283 + | @{const Pure.conjunction} $ t1 $ t2 =>
9.284 + @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
9.285 + $ do_term new_Ts old_Ts polar t2
9.286 + | @{const Trueprop} $ t1 =>
9.287 + @{const Trueprop} $ do_term new_Ts old_Ts polar t1
9.288 + | @{const Not} $ t1 =>
9.289 + @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
9.290 + | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
9.291 + do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
9.292 + | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
9.293 + do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
9.294 + | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
9.295 + do_equals new_Ts old_Ts s0 T0 t1 t2
9.296 + | @{const "op &"} $ t1 $ t2 =>
9.297 + @{const "op &"} $ do_term new_Ts old_Ts polar t1
9.298 + $ do_term new_Ts old_Ts polar t2
9.299 + | @{const "op |"} $ t1 $ t2 =>
9.300 + @{const "op |"} $ do_term new_Ts old_Ts polar t1
9.301 + $ do_term new_Ts old_Ts polar t2
9.302 + | @{const "op -->"} $ t1 $ t2 =>
9.303 + @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
9.304 + $ do_term new_Ts old_Ts polar t2
9.305 + | Const (s as @{const_name The}, T) => do_description_operator s T
9.306 + | Const (s as @{const_name Eps}, T) => do_description_operator s T
9.307 + | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
9.308 + let val T' = box_type hol_ctxt InSel T2 in
9.309 + Const (@{const_name quot_normal}, T' --> T')
9.310 + end
9.311 + | Const (s as @{const_name Tha}, T) => do_description_operator s T
9.312 + | Const (x as (s, T)) =>
9.313 + Const (s, if s = @{const_name converse} orelse
9.314 + s = @{const_name trancl} then
9.315 + box_relational_operator_type T
9.316 + else if is_built_in_const fast_descrs x orelse
9.317 + s = @{const_name Sigma} then
9.318 + T
9.319 + else if is_constr_like thy x then
9.320 + box_type hol_ctxt InConstr T
9.321 + else if is_sel s
9.322 + orelse is_rep_fun thy x then
9.323 + box_type hol_ctxt InSel T
9.324 + else
9.325 + box_type hol_ctxt InExpr T)
9.326 + | t1 $ Abs (s, T, t2') =>
9.327 + let
9.328 + val t1 = do_term new_Ts old_Ts Neut t1
9.329 + val T1 = fastype_of1 (new_Ts, t1)
9.330 + val (s1, Ts1) = dest_Type T1
9.331 + val T' = hd (snd (dest_Type (hd Ts1)))
9.332 + val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
9.333 + val T2 = fastype_of1 (new_Ts, t2)
9.334 + val t2 = coerce_term new_Ts (hd Ts1) T2 t2
9.335 + in
9.336 + betapply (if s1 = "fun" then
9.337 + t1
9.338 + else
9.339 + select_nth_constr_arg thy
9.340 + (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
9.341 + (Type ("fun", Ts1)), t2)
9.342 + end
9.343 + | t1 $ t2 =>
9.344 + let
9.345 + val t1 = do_term new_Ts old_Ts Neut t1
9.346 + val T1 = fastype_of1 (new_Ts, t1)
9.347 + val (s1, Ts1) = dest_Type T1
9.348 + val t2 = do_term new_Ts old_Ts Neut t2
9.349 + val T2 = fastype_of1 (new_Ts, t2)
9.350 + val t2 = coerce_term new_Ts (hd Ts1) T2 t2
9.351 + in
9.352 + betapply (if s1 = "fun" then
9.353 + t1
9.354 + else
9.355 + select_nth_constr_arg thy
9.356 + (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
9.357 + (Type ("fun", Ts1)), t2)
9.358 + end
9.359 + | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
9.360 + | Var (z as (x, T)) =>
9.361 + Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
9.362 + else box_type hol_ctxt InExpr T)
9.363 + | Bound _ => t
9.364 + | Abs (s, T, t') =>
9.365 + Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
9.366 + in do_term [] [] Pos orig_t end
9.367 +
9.368 +(** Destruction of constructors **)
9.369 +
9.370 +val val_var_prefix = nitpick_prefix ^ "v"
9.371 +
9.372 +(* typ list -> int -> int -> int -> term -> term *)
9.373 +fun fresh_value_var Ts k n j t =
9.374 + Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
9.375 +
9.376 +(* typ list -> int -> term -> bool *)
9.377 +fun has_heavy_bounds_or_vars Ts level t =
9.378 + let
9.379 + (* typ list -> bool *)
9.380 + fun aux [] = false
9.381 + | aux [T] = is_fun_type T orelse is_pair_type T
9.382 + | aux _ = true
9.383 + in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
9.384 +
9.385 +(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
9.386 + -> term * term list *)
9.387 +fun pull_out_constr_comb thy Ts relax k level t args seen =
9.388 + let val t_comb = list_comb (t, args) in
9.389 + case t of
9.390 + Const x =>
9.391 + if not relax andalso is_constr thy x andalso
9.392 + not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
9.393 + has_heavy_bounds_or_vars Ts level t_comb andalso
9.394 + not (loose_bvar (t_comb, level)) then
9.395 + let
9.396 + val (j, seen) = case find_index (curry (op =) t_comb) seen of
9.397 + ~1 => (0, t_comb :: seen)
9.398 + | j => (j, seen)
9.399 + in (fresh_value_var Ts k (length seen) j t_comb, seen) end
9.400 + else
9.401 + (t_comb, seen)
9.402 + | _ => (t_comb, seen)
9.403 + end
9.404 +
9.405 +(* (term -> term) -> typ list -> int -> term list -> term list *)
9.406 +fun equations_for_pulled_out_constrs mk_eq Ts k seen =
9.407 + let val n = length seen in
9.408 + map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
9.409 + (index_seq 0 n) seen
9.410 + end
9.411 +
9.412 +(* theory -> bool -> term -> term *)
9.413 +fun pull_out_universal_constrs thy def t =
9.414 + let
9.415 + val k = maxidx_of_term t + 1
9.416 + (* typ list -> bool -> term -> term list -> term list -> term * term list *)
9.417 + fun do_term Ts def t args seen =
9.418 + case t of
9.419 + (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
9.420 + do_eq_or_imp Ts true def t0 t1 t2 seen
9.421 + | (t0 as @{const "==>"}) $ t1 $ t2 =>
9.422 + if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
9.423 + | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
9.424 + do_eq_or_imp Ts true def t0 t1 t2 seen
9.425 + | (t0 as @{const "op -->"}) $ t1 $ t2 =>
9.426 + do_eq_or_imp Ts false def t0 t1 t2 seen
9.427 + | Abs (s, T, t') =>
9.428 + let val (t', seen) = do_term (T :: Ts) def t' [] seen in
9.429 + (list_comb (Abs (s, T, t'), args), seen)
9.430 + end
9.431 + | t1 $ t2 =>
9.432 + let val (t2, seen) = do_term Ts def t2 [] seen in
9.433 + do_term Ts def t1 (t2 :: args) seen
9.434 + end
9.435 + | _ => pull_out_constr_comb thy Ts def k 0 t args seen
9.436 + (* typ list -> bool -> bool -> term -> term -> term -> term list
9.437 + -> term * term list *)
9.438 + and do_eq_or_imp Ts eq def t0 t1 t2 seen =
9.439 + let
9.440 + val (t2, seen) = if eq andalso def then (t2, seen)
9.441 + else do_term Ts false t2 [] seen
9.442 + val (t1, seen) = do_term Ts false t1 [] seen
9.443 + in (t0 $ t1 $ t2, seen) end
9.444 + val (concl, seen) = do_term [] def t [] []
9.445 + in
9.446 + Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
9.447 + seen, concl)
9.448 + end
9.449 +
9.450 +(* term -> term -> term *)
9.451 +fun mk_exists v t =
9.452 + HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
9.453 +
9.454 +(* theory -> term -> term *)
9.455 +fun pull_out_existential_constrs thy t =
9.456 + let
9.457 + val k = maxidx_of_term t + 1
9.458 + (* typ list -> int -> term -> term list -> term list -> term * term list *)
9.459 + fun aux Ts num_exists t args seen =
9.460 + case t of
9.461 + (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
9.462 + let
9.463 + val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
9.464 + val n = length seen'
9.465 + (* unit -> term list *)
9.466 + fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
9.467 + in
9.468 + (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
9.469 + |> List.foldl s_conj t1 |> fold mk_exists (vars ())
9.470 + |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
9.471 + end
9.472 + | t1 $ t2 =>
9.473 + let val (t2, seen) = aux Ts num_exists t2 [] seen in
9.474 + aux Ts num_exists t1 (t2 :: args) seen
9.475 + end
9.476 + | Abs (s, T, t') =>
9.477 + let
9.478 + val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
9.479 + in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
9.480 + | _ =>
9.481 + if num_exists > 0 then
9.482 + pull_out_constr_comb thy Ts false k num_exists t args seen
9.483 + else
9.484 + (list_comb (t, args), seen)
9.485 + in aux [] 0 t [] [] |> fst end
9.486 +
9.487 +(* hol_context -> bool -> term -> term *)
9.488 +fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =
9.489 + let
9.490 + (* styp -> int *)
9.491 + val num_occs_of_var =
9.492 + fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
9.493 + | _ => I) t (K 0)
9.494 + (* bool -> term -> term *)
9.495 + fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
9.496 + aux_eq careful true t0 t1 t2
9.497 + | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
9.498 + t0 $ aux false t1 $ aux careful t2
9.499 + | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
9.500 + aux_eq careful true t0 t1 t2
9.501 + | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
9.502 + t0 $ aux false t1 $ aux careful t2
9.503 + | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
9.504 + | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
9.505 + | aux _ t = t
9.506 + (* bool -> bool -> term -> term -> term -> term *)
9.507 + and aux_eq careful pass1 t0 t1 t2 =
9.508 + ((if careful then
9.509 + raise SAME ()
9.510 + else if axiom andalso is_Var t2 andalso
9.511 + num_occs_of_var (dest_Var t2) = 1 then
9.512 + @{const True}
9.513 + else case strip_comb t2 of
9.514 + (* The first case is not as general as it could be. *)
9.515 + (Const (@{const_name PairBox}, _),
9.516 + [Const (@{const_name fst}, _) $ Var z1,
9.517 + Const (@{const_name snd}, _) $ Var z2]) =>
9.518 + if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
9.519 + else raise SAME ()
9.520 + | (Const (x as (s, T)), args) =>
9.521 + let val arg_Ts = binder_types T in
9.522 + if length arg_Ts = length args andalso
9.523 + (is_constr thy x orelse s = @{const_name Pair} orelse
9.524 + x = (@{const_name Suc}, nat_T --> nat_T)) andalso
9.525 + (not careful orelse not (is_Var t1) orelse
9.526 + String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
9.527 + discriminate_value hol_ctxt x t1 ::
9.528 + map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
9.529 + |> foldr1 s_conj
9.530 + else
9.531 + raise SAME ()
9.532 + end
9.533 + | _ => raise SAME ())
9.534 + |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
9.535 + handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
9.536 + else t0 $ aux false t2 $ aux false t1
9.537 + (* styp -> term -> int -> typ -> term -> term *)
9.538 + and sel_eq x t n nth_T nth_t =
9.539 + HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
9.540 + |> aux false
9.541 + in aux axiom t end
9.542 +
9.543 +(** Destruction of universal and existential equalities **)
9.544 +
9.545 +(* term -> term *)
9.546 +fun curry_assms (@{const "==>"} $ (@{const Trueprop}
9.547 + $ (@{const "op &"} $ t1 $ t2)) $ t3) =
9.548 + curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
9.549 + | curry_assms (@{const "==>"} $ t1 $ t2) =
9.550 + @{const "==>"} $ curry_assms t1 $ curry_assms t2
9.551 + | curry_assms t = t
9.552 +
9.553 +(* term -> term *)
9.554 +val destroy_universal_equalities =
9.555 + let
9.556 + (* term list -> (indexname * typ) list -> term -> term *)
9.557 + fun aux prems zs t =
9.558 + case t of
9.559 + @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
9.560 + | _ => Logic.list_implies (rev prems, t)
9.561 + (* term list -> (indexname * typ) list -> term -> term -> term *)
9.562 + and aux_implies prems zs t1 t2 =
9.563 + case t1 of
9.564 + Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
9.565 + | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
9.566 + aux_eq prems zs z t' t1 t2
9.567 + | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
9.568 + aux_eq prems zs z t' t1 t2
9.569 + | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
9.570 + (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
9.571 + -> term -> term *)
9.572 + and aux_eq prems zs z t' t1 t2 =
9.573 + if not (member (op =) zs z) andalso
9.574 + not (exists_subterm (curry (op =) (Var z)) t') then
9.575 + aux prems zs (subst_free [(Var z, t')] t2)
9.576 + else
9.577 + aux (t1 :: prems) (Term.add_vars t1 zs) t2
9.578 + in aux [] [] end
9.579 +
9.580 +(* theory -> int -> term list -> term list -> (term * term list) option *)
9.581 +fun find_bound_assign _ _ _ [] = NONE
9.582 + | find_bound_assign thy j seen (t :: ts) =
9.583 + let
9.584 + (* bool -> term -> term -> (term * term list) option *)
9.585 + fun aux pass1 t1 t2 =
9.586 + (if loose_bvar1 (t2, j) then
9.587 + if pass1 then aux false t2 t1 else raise SAME ()
9.588 + else case t1 of
9.589 + Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
9.590 + | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
9.591 + if j' = j andalso
9.592 + s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
9.593 + SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
9.594 + ts @ seen)
9.595 + else
9.596 + raise SAME ()
9.597 + | _ => raise SAME ())
9.598 + handle SAME () => find_bound_assign thy j (t :: seen) ts
9.599 + in
9.600 + case t of
9.601 + Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
9.602 + | _ => find_bound_assign thy j (t :: seen) ts
9.603 + end
9.604 +
9.605 +(* int -> term -> term -> term *)
9.606 +fun subst_one_bound j arg t =
9.607 + let
9.608 + fun aux (Bound i, lev) =
9.609 + if i < lev then raise SAME ()
9.610 + else if i = lev then incr_boundvars (lev - j) arg
9.611 + else Bound (i - 1)
9.612 + | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
9.613 + | aux (f $ t, lev) =
9.614 + (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
9.615 + handle SAME () => f $ aux (t, lev))
9.616 + | aux _ = raise SAME ()
9.617 + in aux (t, j) handle SAME () => t end
9.618 +
9.619 +(* theory -> term -> term *)
9.620 +fun destroy_existential_equalities thy =
9.621 + let
9.622 + (* string list -> typ list -> term list -> term *)
9.623 + fun kill [] [] ts = foldr1 s_conj ts
9.624 + | kill (s :: ss) (T :: Ts) ts =
9.625 + (case find_bound_assign thy (length ss) [] ts of
9.626 + SOME (_, []) => @{const True}
9.627 + | SOME (arg_t, ts) =>
9.628 + kill ss Ts (map (subst_one_bound (length ss)
9.629 + (incr_bv (~1, length ss + 1, arg_t))) ts)
9.630 + | NONE =>
9.631 + Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
9.632 + $ Abs (s, T, kill ss Ts ts))
9.633 + | kill _ _ _ = raise UnequalLengths
9.634 + (* string list -> typ list -> term -> term *)
9.635 + fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
9.636 + gather (ss @ [s1]) (Ts @ [T1]) t1
9.637 + | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
9.638 + | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
9.639 + | gather [] [] t = t
9.640 + | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))
9.641 + in gather [] [] end
9.642 +
9.643 +(** Skolemization **)
9.644 +
9.645 +(* int -> int -> string *)
9.646 +fun skolem_prefix_for k j =
9.647 + skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
9.648 +
9.649 +(* hol_context -> int -> term -> term *)
9.650 +fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
9.651 + skolem_depth =
9.652 + let
9.653 + (* int list -> int list *)
9.654 + val incrs = map (Integer.add 1)
9.655 + (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
9.656 + fun aux ss Ts js depth polar t =
9.657 + let
9.658 + (* string -> typ -> string -> typ -> term -> term *)
9.659 + fun do_quantifier quant_s quant_T abs_s abs_T t =
9.660 + if not (loose_bvar1 (t, 0)) then
9.661 + aux ss Ts js depth polar (incr_boundvars ~1 t)
9.662 + else if depth <= skolem_depth andalso
9.663 + is_positive_existential polar quant_s then
9.664 + let
9.665 + val j = length (!skolems) + 1
9.666 + val sko_s = skolem_prefix_for (length js) j ^ abs_s
9.667 + val _ = Unsynchronized.change skolems (cons (sko_s, ss))
9.668 + val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
9.669 + map Bound (rev js))
9.670 + val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
9.671 + in
9.672 + if null js then betapply (abs_t, sko_t)
9.673 + else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
9.674 + end
9.675 + else
9.676 + Const (quant_s, quant_T)
9.677 + $ Abs (abs_s, abs_T,
9.678 + if is_higher_order_type abs_T then
9.679 + t
9.680 + else
9.681 + aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
9.682 + (depth + 1) polar t)
9.683 + in
9.684 + case t of
9.685 + Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
9.686 + do_quantifier s0 T0 s1 T1 t1
9.687 + | @{const "==>"} $ t1 $ t2 =>
9.688 + @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
9.689 + $ aux ss Ts js depth polar t2
9.690 + | @{const Pure.conjunction} $ t1 $ t2 =>
9.691 + @{const Pure.conjunction} $ aux ss Ts js depth polar t1
9.692 + $ aux ss Ts js depth polar t2
9.693 + | @{const Trueprop} $ t1 =>
9.694 + @{const Trueprop} $ aux ss Ts js depth polar t1
9.695 + | @{const Not} $ t1 =>
9.696 + @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
9.697 + | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
9.698 + do_quantifier s0 T0 s1 T1 t1
9.699 + | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
9.700 + do_quantifier s0 T0 s1 T1 t1
9.701 + | @{const "op &"} $ t1 $ t2 =>
9.702 + @{const "op &"} $ aux ss Ts js depth polar t1
9.703 + $ aux ss Ts js depth polar t2
9.704 + | @{const "op |"} $ t1 $ t2 =>
9.705 + @{const "op |"} $ aux ss Ts js depth polar t1
9.706 + $ aux ss Ts js depth polar t2
9.707 + | @{const "op -->"} $ t1 $ t2 =>
9.708 + @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
9.709 + $ aux ss Ts js depth polar t2
9.710 + | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
9.711 + t0 $ t1 $ aux ss Ts js depth polar t2
9.712 + | Const (x as (s, T)) =>
9.713 + if is_inductive_pred hol_ctxt x andalso
9.714 + not (is_well_founded_inductive_pred hol_ctxt x) then
9.715 + let
9.716 + val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
9.717 + val (pref, connective, set_oper) =
9.718 + if gfp then
9.719 + (lbfp_prefix,
9.720 + @{const "op |"},
9.721 + @{const_name upper_semilattice_fun_inst.sup_fun})
9.722 + else
9.723 + (ubfp_prefix,
9.724 + @{const "op &"},
9.725 + @{const_name lower_semilattice_fun_inst.inf_fun})
9.726 + (* unit -> term *)
9.727 + fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
9.728 + |> aux ss Ts js depth polar
9.729 + fun neg () = Const (pref ^ s, T)
9.730 + in
9.731 + (case polar |> gfp ? flip_polarity of
9.732 + Pos => pos ()
9.733 + | Neg => neg ()
9.734 + | Neut =>
9.735 + if is_fun_type T then
9.736 + let
9.737 + val ((trunk_arg_Ts, rump_arg_T), body_T) =
9.738 + T |> strip_type |>> split_last
9.739 + val set_T = rump_arg_T --> body_T
9.740 + (* (unit -> term) -> term *)
9.741 + fun app f =
9.742 + list_comb (f (),
9.743 + map Bound (length trunk_arg_Ts - 1 downto 0))
9.744 + in
9.745 + List.foldr absdummy
9.746 + (Const (set_oper, set_T --> set_T --> set_T)
9.747 + $ app pos $ app neg) trunk_arg_Ts
9.748 + end
9.749 + else
9.750 + connective $ pos () $ neg ())
9.751 + end
9.752 + else
9.753 + Const x
9.754 + | t1 $ t2 =>
9.755 + betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
9.756 + aux ss Ts [] depth Neut t2)
9.757 + | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
9.758 + | _ => t
9.759 + end
9.760 + in aux [] [] [] 0 Pos end
9.761 +
9.762 +(** Function specialization **)
9.763 +
9.764 +(* term -> term list *)
9.765 +fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
9.766 + | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
9.767 + | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
9.768 + snd (strip_comb t1)
9.769 + | params_in_equation _ = []
9.770 +
9.771 +(* styp -> styp -> int list -> term list -> term list -> term -> term *)
9.772 +fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
9.773 + let
9.774 + val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
9.775 + + 1
9.776 + val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
9.777 + val fixed_params = filter_indices fixed_js (params_in_equation t)
9.778 + (* term list -> term -> term *)
9.779 + fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
9.780 + | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
9.781 + | aux args t =
9.782 + if t = Const x then
9.783 + list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
9.784 + else
9.785 + let val j = find_index (curry (op =) t) fixed_params in
9.786 + list_comb (if j >= 0 then nth fixed_args j else t, args)
9.787 + end
9.788 + in aux [] t end
9.789 +
9.790 +(* hol_context -> styp -> (int * term option) list *)
9.791 +fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =
9.792 + let
9.793 + (* term -> term list -> term list -> term list list *)
9.794 + fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
9.795 + | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
9.796 + | fun_calls t args =
9.797 + (case t of
9.798 + Const (x' as (s', T')) =>
9.799 + x = x' orelse (case AList.lookup (op =) ersatz_table s' of
9.800 + SOME s'' => x = (s'', T')
9.801 + | NONE => false)
9.802 + | _ => false) ? cons args
9.803 + (* term list list -> term list list -> term list -> term list list *)
9.804 + fun call_sets [] [] vs = [vs]
9.805 + | call_sets [] uss vs = vs :: call_sets uss [] []
9.806 + | call_sets ([] :: _) _ _ = []
9.807 + | call_sets ((t :: ts) :: tss) uss vs =
9.808 + OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
9.809 + val sets = call_sets (fun_calls t [] []) [] []
9.810 + val indexed_sets = sets ~~ (index_seq 0 (length sets))
9.811 + in
9.812 + fold_rev (fn (set, j) =>
9.813 + case set of
9.814 + [Var _] => AList.lookup (op =) indexed_sets set = SOME j
9.815 + ? cons (j, NONE)
9.816 + | [t as Const _] => cons (j, SOME t)
9.817 + | [t as Free _] => cons (j, SOME t)
9.818 + | _ => I) indexed_sets []
9.819 + end
9.820 +(* hol_context -> styp -> term list -> (int * term option) list *)
9.821 +fun static_args_in_terms hol_ctxt x =
9.822 + map (static_args_in_term hol_ctxt x)
9.823 + #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
9.824 +
9.825 +(* (int * term option) list -> (int * term) list -> int list *)
9.826 +fun overlapping_indices [] _ = []
9.827 + | overlapping_indices _ [] = []
9.828 + | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
9.829 + if j1 < j2 then overlapping_indices ps1' ps2
9.830 + else if j1 > j2 then overlapping_indices ps1 ps2'
9.831 + else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
9.832 +
9.833 +(* typ list -> term -> bool *)
9.834 +fun is_eligible_arg Ts t =
9.835 + let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
9.836 + null bad_Ts orelse
9.837 + (is_higher_order_type (fastype_of1 (Ts, t)) andalso
9.838 + forall (not o is_higher_order_type) bad_Ts)
9.839 + end
9.840 +
9.841 +(* int -> string *)
9.842 +fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
9.843 +
9.844 +(* If a constant's definition is picked up deeper than this threshold, we
9.845 + prevent excessive specialization by not specializing it. *)
9.846 +val special_max_depth = 20
9.847 +
9.848 +val bound_var_prefix = "b"
9.849 +
9.850 +(* hol_context -> int -> term -> term *)
9.851 +fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,
9.852 + special_funs, ...}) depth t =
9.853 + if not specialize orelse depth > special_max_depth then
9.854 + t
9.855 + else
9.856 + let
9.857 + val blacklist = if depth = 0 then []
9.858 + else case term_under_def t of Const x => [x] | _ => []
9.859 + (* term list -> typ list -> term -> term *)
9.860 + fun aux args Ts (Const (x as (s, T))) =
9.861 + ((if not (member (op =) blacklist x) andalso not (null args) andalso
9.862 + not (String.isPrefix special_prefix s) andalso
9.863 + is_equational_fun hol_ctxt x then
9.864 + let
9.865 + val eligible_args = filter (is_eligible_arg Ts o snd)
9.866 + (index_seq 0 (length args) ~~ args)
9.867 + val _ = not (null eligible_args) orelse raise SAME ()
9.868 + val old_axs = equational_fun_axioms hol_ctxt x
9.869 + |> map (destroy_existential_equalities thy)
9.870 + val static_params = static_args_in_terms hol_ctxt x old_axs
9.871 + val fixed_js = overlapping_indices static_params eligible_args
9.872 + val _ = not (null fixed_js) orelse raise SAME ()
9.873 + val fixed_args = filter_indices fixed_js args
9.874 + val vars = fold Term.add_vars fixed_args []
9.875 + |> sort (TermOrd.fast_indexname_ord o pairself fst)
9.876 + val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
9.877 + fixed_args []
9.878 + |> sort int_ord
9.879 + val live_args = filter_out_indices fixed_js args
9.880 + val extra_args = map Var vars @ map Bound bound_js @ live_args
9.881 + val extra_Ts = map snd vars @ filter_indices bound_js Ts
9.882 + val k = maxidx_of_term t + 1
9.883 + (* int -> term *)
9.884 + fun var_for_bound_no j =
9.885 + Var ((bound_var_prefix ^
9.886 + nat_subscript (find_index (curry (op =) j) bound_js
9.887 + + 1), k),
9.888 + nth Ts j)
9.889 + val fixed_args_in_axiom =
9.890 + map (curry subst_bounds
9.891 + (map var_for_bound_no (index_seq 0 (length Ts))))
9.892 + fixed_args
9.893 + in
9.894 + case AList.lookup (op =) (!special_funs)
9.895 + (x, fixed_js, fixed_args_in_axiom) of
9.896 + SOME x' => list_comb (Const x', extra_args)
9.897 + | NONE =>
9.898 + let
9.899 + val extra_args_in_axiom =
9.900 + map Var vars @ map var_for_bound_no bound_js
9.901 + val x' as (s', _) =
9.902 + (special_prefix_for (length (!special_funs) + 1) ^ s,
9.903 + extra_Ts @ filter_out_indices fixed_js (binder_types T)
9.904 + ---> body_type T)
9.905 + val new_axs =
9.906 + map (specialize_fun_axiom x x' fixed_js
9.907 + fixed_args_in_axiom extra_args_in_axiom) old_axs
9.908 + val _ =
9.909 + Unsynchronized.change special_funs
9.910 + (cons ((x, fixed_js, fixed_args_in_axiom), x'))
9.911 + val _ = add_simps simp_table s' new_axs
9.912 + in list_comb (Const x', extra_args) end
9.913 + end
9.914 + else
9.915 + raise SAME ())
9.916 + handle SAME () => list_comb (Const x, args))
9.917 + | aux args Ts (Abs (s, T, t)) =
9.918 + list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
9.919 + | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
9.920 + | aux args _ t = list_comb (t, args)
9.921 + in aux [] [] t end
9.922 +
9.923 +type special_triple = int list * term list * styp
9.924 +
9.925 +val cong_var_prefix = "c"
9.926 +
9.927 +(* styp -> special_triple -> special_triple -> term *)
9.928 +fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
9.929 + let
9.930 + val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
9.931 + val Ts = binder_types T
9.932 + val max_j = fold (fold Integer.max) [js1, js2] ~1
9.933 + val (eqs, (args1, args2)) =
9.934 + fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
9.935 + (js1 ~~ ts1, js2 ~~ ts2) of
9.936 + (SOME t1, SOME t2) => apfst (cons (t1, t2))
9.937 + | (SOME t1, NONE) => apsnd (apsnd (cons t1))
9.938 + | (NONE, SOME t2) => apsnd (apfst (cons t2))
9.939 + | (NONE, NONE) =>
9.940 + let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
9.941 + nth Ts j) in
9.942 + apsnd (pairself (cons v))
9.943 + end) (max_j downto 0) ([], ([], []))
9.944 + in
9.945 + Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
9.946 + |> map Logic.mk_equals,
9.947 + Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
9.948 + list_comb (Const x2, bounds2 @ args2)))
9.949 + |> Refute.close_form (* TODO: needed? *)
9.950 + end
9.951 +
9.952 +(* hol_context -> styp list -> term list *)
9.953 +fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
9.954 + let
9.955 + val groups =
9.956 + !special_funs
9.957 + |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
9.958 + |> AList.group (op =)
9.959 + |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
9.960 + |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
9.961 + (* special_triple -> int *)
9.962 + fun generality (js, _, _) = ~(length js)
9.963 + (* special_triple -> special_triple -> bool *)
9.964 + fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
9.965 + x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
9.966 + (j2 ~~ t2, j1 ~~ t1)
9.967 + (* styp -> special_triple list -> special_triple list -> special_triple list
9.968 + -> term list -> term list *)
9.969 + fun do_pass_1 _ [] [_] [_] = I
9.970 + | do_pass_1 x skipped _ [] = do_pass_2 x skipped
9.971 + | do_pass_1 x skipped all (z :: zs) =
9.972 + case filter (is_more_specific z) all
9.973 + |> sort (int_ord o pairself generality) of
9.974 + [] => do_pass_1 x (z :: skipped) all zs
9.975 + | (z' :: _) => cons (special_congruence_axiom x z z')
9.976 + #> do_pass_1 x skipped all zs
9.977 + (* styp -> special_triple list -> term list -> term list *)
9.978 + and do_pass_2 _ [] = I
9.979 + | do_pass_2 x (z :: zs) =
9.980 + fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
9.981 + in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
9.982 +
9.983 +(** Axiom selection **)
9.984 +
9.985 +(* Similar to "Refute.specialize_type" but returns all matches rather than only
9.986 + the first (preorder) match. *)
9.987 +(* theory -> styp -> term -> term list *)
9.988 +fun multi_specialize_type thy slack (x as (s, T)) t =
9.989 + let
9.990 + (* term -> (typ * term) list -> (typ * term) list *)
9.991 + fun aux (Const (s', T')) ys =
9.992 + if s = s' then
9.993 + ys |> (if AList.defined (op =) ys T' then
9.994 + I
9.995 + else
9.996 + cons (T', Refute.monomorphic_term
9.997 + (Sign.typ_match thy (T', T) Vartab.empty) t)
9.998 + handle Type.TYPE_MATCH => I
9.999 + | Refute.REFUTE _ =>
9.1000 + if slack then
9.1001 + I
9.1002 + else
9.1003 + raise NOT_SUPPORTED ("too much polymorphism in \
9.1004 + \axiom involving " ^ quote s))
9.1005 + else
9.1006 + ys
9.1007 + | aux _ ys = ys
9.1008 + in map snd (fold_aterms aux t []) end
9.1009 +
9.1010 +(* theory -> bool -> const_table -> styp -> term list *)
9.1011 +fun nondef_props_for_const thy slack table (x as (s, _)) =
9.1012 + these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
9.1013 +
9.1014 +(* 'a Symtab.table -> 'a list *)
9.1015 +fun all_table_entries table = Symtab.fold (append o snd) table []
9.1016 +(* const_table -> string -> const_table *)
9.1017 +fun extra_table table s = Symtab.make [(s, all_table_entries table)]
9.1018 +
9.1019 +(* int -> term -> term *)
9.1020 +fun eval_axiom_for_term j t =
9.1021 + Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
9.1022 +
9.1023 +(* term -> bool *)
9.1024 +val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
9.1025 +
9.1026 +(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
9.1027 +val axioms_max_depth = 255
9.1028 +
9.1029 +(* hol_context -> term -> (term list * term list) * (bool * bool) *)
9.1030 +fun axioms_for_term
9.1031 + (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
9.1032 + def_table, nondef_table, user_nondefs, ...}) t =
9.1033 + let
9.1034 + type accumulator = styp list * (term list * term list)
9.1035 + (* (term list * term list -> term list)
9.1036 + -> ((term list -> term list) -> term list * term list
9.1037 + -> term list * term list)
9.1038 + -> int -> term -> accumulator -> accumulator *)
9.1039 + fun add_axiom get app depth t (accum as (xs, axs)) =
9.1040 + let
9.1041 + val t = t |> unfold_defs_in_term hol_ctxt
9.1042 + |> skolemize_term_and_more hol_ctxt ~1
9.1043 + in
9.1044 + if is_trivial_equation t then
9.1045 + accum
9.1046 + else
9.1047 + let val t' = t |> specialize_consts_in_term hol_ctxt depth in
9.1048 + if exists (member (op aconv) (get axs)) [t, t'] then accum
9.1049 + else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
9.1050 + end
9.1051 + end
9.1052 + (* int -> term -> accumulator -> accumulator *)
9.1053 + and add_def_axiom depth = add_axiom fst apfst depth
9.1054 + and add_nondef_axiom depth = add_axiom snd apsnd depth
9.1055 + and add_maybe_def_axiom depth t =
9.1056 + (if head_of t <> @{const "==>"} then add_def_axiom
9.1057 + else add_nondef_axiom) depth t
9.1058 + and add_eq_axiom depth t =
9.1059 + (if is_constr_pattern_formula thy t then add_def_axiom
9.1060 + else add_nondef_axiom) depth t
9.1061 + (* int -> term -> accumulator -> accumulator *)
9.1062 + and add_axioms_for_term depth t (accum as (xs, axs)) =
9.1063 + case t of
9.1064 + t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
9.1065 + | Const (x as (s, T)) =>
9.1066 + (if member (op =) xs x orelse is_built_in_const fast_descrs x then
9.1067 + accum
9.1068 + else
9.1069 + let val accum as (xs, _) = (x :: xs, axs) in
9.1070 + if depth > axioms_max_depth then
9.1071 + raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
9.1072 + \add_axioms_for_term",
9.1073 + "too many nested axioms (" ^
9.1074 + string_of_int depth ^ ")")
9.1075 + else if Refute.is_const_of_class thy x then
9.1076 + let
9.1077 + val class = Logic.class_of_const s
9.1078 + val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
9.1079 + class)
9.1080 + val ax1 = try (Refute.specialize_type thy x) of_class
9.1081 + val ax2 = Option.map (Refute.specialize_type thy x o snd)
9.1082 + (Refute.get_classdef thy class)
9.1083 + in
9.1084 + fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
9.1085 + accum
9.1086 + end
9.1087 + else if is_constr thy x then
9.1088 + accum
9.1089 + else if is_equational_fun hol_ctxt x then
9.1090 + fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
9.1091 + accum
9.1092 + else if is_abs_fun thy x then
9.1093 + if is_quot_type thy (range_type T) then
9.1094 + raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
9.1095 + else
9.1096 + accum |> fold (add_nondef_axiom depth)
9.1097 + (nondef_props_for_const thy false nondef_table x)
9.1098 + |> is_funky_typedef thy (range_type T)
9.1099 + ? fold (add_maybe_def_axiom depth)
9.1100 + (nondef_props_for_const thy true
9.1101 + (extra_table def_table s) x)
9.1102 + else if is_rep_fun thy x then
9.1103 + if is_quot_type thy (domain_type T) then
9.1104 + raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
9.1105 + else
9.1106 + accum |> fold (add_nondef_axiom depth)
9.1107 + (nondef_props_for_const thy false nondef_table x)
9.1108 + |> is_funky_typedef thy (range_type T)
9.1109 + ? fold (add_maybe_def_axiom depth)
9.1110 + (nondef_props_for_const thy true
9.1111 + (extra_table def_table s) x)
9.1112 + |> add_axioms_for_term depth
9.1113 + (Const (mate_of_rep_fun thy x))
9.1114 + |> fold (add_def_axiom depth)
9.1115 + (inverse_axioms_for_rep_fun thy x)
9.1116 + else
9.1117 + accum |> user_axioms <> SOME false
9.1118 + ? fold (add_nondef_axiom depth)
9.1119 + (nondef_props_for_const thy false nondef_table x)
9.1120 + end)
9.1121 + |> add_axioms_for_type depth T
9.1122 + | Free (_, T) => add_axioms_for_type depth T accum
9.1123 + | Var (_, T) => add_axioms_for_type depth T accum
9.1124 + | Bound _ => accum
9.1125 + | Abs (_, T, t) => accum |> add_axioms_for_term depth t
9.1126 + |> add_axioms_for_type depth T
9.1127 + (* int -> typ -> accumulator -> accumulator *)
9.1128 + and add_axioms_for_type depth T =
9.1129 + case T of
9.1130 + Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
9.1131 + | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
9.1132 + | @{typ prop} => I
9.1133 + | @{typ bool} => I
9.1134 + | @{typ unit} => I
9.1135 + | TFree (_, S) => add_axioms_for_sort depth T S
9.1136 + | TVar (_, S) => add_axioms_for_sort depth T S
9.1137 + | Type (z as (s, Ts)) =>
9.1138 + fold (add_axioms_for_type depth) Ts
9.1139 + #> (if is_pure_typedef thy T then
9.1140 + fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
9.1141 + else if is_quot_type thy T then
9.1142 + fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
9.1143 + else if max_bisim_depth >= 0 andalso is_codatatype thy T then
9.1144 + fold (add_maybe_def_axiom depth)
9.1145 + (codatatype_bisim_axioms hol_ctxt T)
9.1146 + else
9.1147 + I)
9.1148 + (* int -> typ -> sort -> accumulator -> accumulator *)
9.1149 + and add_axioms_for_sort depth T S =
9.1150 + let
9.1151 + val supers = Sign.complete_sort thy S
9.1152 + val class_axioms =
9.1153 + maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
9.1154 + handle ERROR _ => [])) supers
9.1155 + val monomorphic_class_axioms =
9.1156 + map (fn t => case Term.add_tvars t [] of
9.1157 + [] => t
9.1158 + | [(x, S)] =>
9.1159 + Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
9.1160 + | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
9.1161 + \add_axioms_for_sort", [t]))
9.1162 + class_axioms
9.1163 + in fold (add_nondef_axiom depth) monomorphic_class_axioms end
9.1164 + val (mono_user_nondefs, poly_user_nondefs) =
9.1165 + List.partition (null o Term.hidden_polymorphism) user_nondefs
9.1166 + val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
9.1167 + evals
9.1168 + val (xs, (defs, nondefs)) =
9.1169 + ([], ([], [])) |> add_axioms_for_term 1 t
9.1170 + |> fold_rev (add_def_axiom 1) eval_axioms
9.1171 + |> user_axioms = SOME true
9.1172 + ? fold (add_nondef_axiom 1) mono_user_nondefs
9.1173 + val defs = defs @ special_congruence_axioms hol_ctxt xs
9.1174 + in
9.1175 + ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
9.1176 + null poly_user_nondefs))
9.1177 + end
9.1178 +
9.1179 +(** Simplification of constructor/selector terms **)
9.1180 +
9.1181 +(* theory -> term -> term *)
9.1182 +fun simplify_constrs_and_sels thy t =
9.1183 + let
9.1184 + (* term -> int -> term *)
9.1185 + fun is_nth_sel_on t' n (Const (s, _) $ t) =
9.1186 + (t = t' andalso is_sel_like_and_no_discr s andalso
9.1187 + sel_no_from_name s = n)
9.1188 + | is_nth_sel_on _ _ _ = false
9.1189 + (* term -> term list -> term *)
9.1190 + fun do_term (Const (@{const_name Rep_Frac}, _)
9.1191 + $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
9.1192 + | do_term (Const (@{const_name Abs_Frac}, _)
9.1193 + $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
9.1194 + | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
9.1195 + | do_term (t as Const (x as (s, T))) (args as _ :: _) =
9.1196 + ((if is_constr_like thy x then
9.1197 + if length args = num_binder_types T then
9.1198 + case hd args of
9.1199 + Const (x' as (_, T')) $ t' =>
9.1200 + if domain_type T' = body_type T andalso
9.1201 + forall (uncurry (is_nth_sel_on t'))
9.1202 + (index_seq 0 (length args) ~~ args) then
9.1203 + t'
9.1204 + else
9.1205 + raise SAME ()
9.1206 + | _ => raise SAME ()
9.1207 + else
9.1208 + raise SAME ()
9.1209 + else if is_sel_like_and_no_discr s then
9.1210 + case strip_comb (hd args) of
9.1211 + (Const (x' as (s', T')), ts') =>
9.1212 + if is_constr_like thy x' andalso
9.1213 + constr_name_for_sel_like s = s' andalso
9.1214 + not (exists is_pair_type (binder_types T')) then
9.1215 + list_comb (nth ts' (sel_no_from_name s), tl args)
9.1216 + else
9.1217 + raise SAME ()
9.1218 + | _ => raise SAME ()
9.1219 + else
9.1220 + raise SAME ())
9.1221 + handle SAME () => betapplys (t, args))
9.1222 + | do_term (Abs (s, T, t')) args =
9.1223 + betapplys (Abs (s, T, do_term t' []), args)
9.1224 + | do_term t args = betapplys (t, args)
9.1225 + in do_term t [] end
9.1226 +
9.1227 +(** Quantifier massaging: Distributing quantifiers **)
9.1228 +
9.1229 +(* term -> term *)
9.1230 +fun distribute_quantifiers t =
9.1231 + case t of
9.1232 + (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
9.1233 + (case t1 of
9.1234 + (t10 as @{const "op &"}) $ t11 $ t12 =>
9.1235 + t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
9.1236 + $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
9.1237 + | (t10 as @{const Not}) $ t11 =>
9.1238 + t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
9.1239 + $ Abs (s, T1, t11))
9.1240 + | t1 =>
9.1241 + if not (loose_bvar1 (t1, 0)) then
9.1242 + distribute_quantifiers (incr_boundvars ~1 t1)
9.1243 + else
9.1244 + t0 $ Abs (s, T1, distribute_quantifiers t1))
9.1245 + | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
9.1246 + (case distribute_quantifiers t1 of
9.1247 + (t10 as @{const "op |"}) $ t11 $ t12 =>
9.1248 + t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
9.1249 + $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
9.1250 + | (t10 as @{const "op -->"}) $ t11 $ t12 =>
9.1251 + t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
9.1252 + $ Abs (s, T1, t11))
9.1253 + $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
9.1254 + | (t10 as @{const Not}) $ t11 =>
9.1255 + t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
9.1256 + $ Abs (s, T1, t11))
9.1257 + | t1 =>
9.1258 + if not (loose_bvar1 (t1, 0)) then
9.1259 + distribute_quantifiers (incr_boundvars ~1 t1)
9.1260 + else
9.1261 + t0 $ Abs (s, T1, distribute_quantifiers t1))
9.1262 + | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
9.1263 + | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
9.1264 + | _ => t
9.1265 +
9.1266 +(** Quantifier massaging: Pushing quantifiers inward **)
9.1267 +
9.1268 +(* int -> int -> (int -> int) -> term -> term *)
9.1269 +fun renumber_bounds j n f t =
9.1270 + case t of
9.1271 + t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
9.1272 + | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
9.1273 + | Bound j' =>
9.1274 + Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
9.1275 + | _ => t
9.1276 +
9.1277 +(* Maximum number of quantifiers in a cluster for which the exponential
9.1278 + algorithm is used. Larger clusters use a heuristic inspired by Claessen &
9.1279 + Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
9.1280 + paper). *)
9.1281 +val quantifier_cluster_threshold = 7
9.1282 +
9.1283 +(* theory -> term -> term *)
9.1284 +fun push_quantifiers_inward thy =
9.1285 + let
9.1286 + (* string -> string list -> typ list -> term -> term *)
9.1287 + fun aux quant_s ss Ts t =
9.1288 + (case t of
9.1289 + (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
9.1290 + if s0 = quant_s then
9.1291 + aux s0 (s1 :: ss) (T1 :: Ts) t1
9.1292 + else if quant_s = "" andalso
9.1293 + (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
9.1294 + aux s0 [s1] [T1] t1
9.1295 + else
9.1296 + raise SAME ()
9.1297 + | _ => raise SAME ())
9.1298 + handle SAME () =>
9.1299 + case t of
9.1300 + t1 $ t2 =>
9.1301 + if quant_s = "" then
9.1302 + aux "" [] [] t1 $ aux "" [] [] t2
9.1303 + else
9.1304 + let
9.1305 + val typical_card = 4
9.1306 + (* ('a -> ''b list) -> 'a list -> ''b list *)
9.1307 + fun big_union proj ps =
9.1308 + fold (fold (insert (op =)) o proj) ps []
9.1309 + val (ts, connective) = strip_any_connective t
9.1310 + val T_costs =
9.1311 + map (bounded_card_of_type 65536 typical_card []) Ts
9.1312 + val t_costs = map size_of_term ts
9.1313 + val num_Ts = length Ts
9.1314 + (* int -> int *)
9.1315 + val flip = curry (op -) (num_Ts - 1)
9.1316 + val t_boundss = map (map flip o loose_bnos) ts
9.1317 + (* (int list * int) list -> int list
9.1318 + -> (int list * int) list *)
9.1319 + fun merge costly_boundss [] = costly_boundss
9.1320 + | merge costly_boundss (j :: js) =
9.1321 + let
9.1322 + val (yeas, nays) =
9.1323 + List.partition (fn (bounds, _) =>
9.1324 + member (op =) bounds j)
9.1325 + costly_boundss
9.1326 + val yeas_bounds = big_union fst yeas
9.1327 + val yeas_cost = Integer.sum (map snd yeas)
9.1328 + * nth T_costs j
9.1329 + in merge ((yeas_bounds, yeas_cost) :: nays) js end
9.1330 + (* (int list * int) list -> int list -> int *)
9.1331 + val cost = Integer.sum o map snd oo merge
9.1332 + (* (int list * int) list -> int list -> int list *)
9.1333 + fun heuristically_best_permutation _ [] = []
9.1334 + | heuristically_best_permutation costly_boundss js =
9.1335 + let
9.1336 + val (costly_boundss, (j, js)) =
9.1337 + js |> map (`(merge costly_boundss o single))
9.1338 + |> sort (int_ord
9.1339 + o pairself (Integer.sum o map snd o fst))
9.1340 + |> split_list |>> hd ||> pairf hd tl
9.1341 + in
9.1342 + j :: heuristically_best_permutation costly_boundss js
9.1343 + end
9.1344 + val js =
9.1345 + if length Ts <= quantifier_cluster_threshold then
9.1346 + all_permutations (index_seq 0 num_Ts)
9.1347 + |> map (`(cost (t_boundss ~~ t_costs)))
9.1348 + |> sort (int_ord o pairself fst) |> hd |> snd
9.1349 + else
9.1350 + heuristically_best_permutation (t_boundss ~~ t_costs)
9.1351 + (index_seq 0 num_Ts)
9.1352 + val back_js = map (fn j => find_index (curry (op =) j) js)
9.1353 + (index_seq 0 num_Ts)
9.1354 + val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
9.1355 + ts
9.1356 + (* (term * int list) list -> term *)
9.1357 + fun mk_connection [] =
9.1358 + raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\
9.1359 + \mk_connection", "")
9.1360 + | mk_connection ts_cum_bounds =
9.1361 + ts_cum_bounds |> map fst
9.1362 + |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
9.1363 + (* (term * int list) list -> int list -> term *)
9.1364 + fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
9.1365 + | build ts_cum_bounds (j :: js) =
9.1366 + let
9.1367 + val (yeas, nays) =
9.1368 + List.partition (fn (_, bounds) =>
9.1369 + member (op =) bounds j)
9.1370 + ts_cum_bounds
9.1371 + ||> map (apfst (incr_boundvars ~1))
9.1372 + in
9.1373 + if null yeas then
9.1374 + build nays js
9.1375 + else
9.1376 + let val T = nth Ts (flip j) in
9.1377 + build ((Const (quant_s, (T --> bool_T) --> bool_T)
9.1378 + $ Abs (nth ss (flip j), T,
9.1379 + mk_connection yeas),
9.1380 + big_union snd yeas) :: nays) js
9.1381 + end
9.1382 + end
9.1383 + in build (ts ~~ t_boundss) js end
9.1384 + | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
9.1385 + | _ => t
9.1386 + in aux "" [] [] end
9.1387 +
9.1388 +(** Preprocessor entry point **)
9.1389 +
9.1390 +(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
9.1391 +fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
9.1392 + skolemize, uncurry, ...}) t =
9.1393 + let
9.1394 + val skolem_depth = if skolemize then 4 else ~1
9.1395 + val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
9.1396 + core_t) = t |> unfold_defs_in_term hol_ctxt
9.1397 + |> Refute.close_form
9.1398 + |> skolemize_term_and_more hol_ctxt skolem_depth
9.1399 + |> specialize_consts_in_term hol_ctxt 0
9.1400 + |> `(axioms_for_term hol_ctxt)
9.1401 + val binarize =
9.1402 + case binary_ints of
9.1403 + SOME false => false
9.1404 + | _ =>
9.1405 + forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
9.1406 + (binary_ints = SOME true orelse
9.1407 + exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
9.1408 + val box = exists (not_equal (SOME false) o snd) boxes
9.1409 + val table =
9.1410 + Termtab.empty |> uncurry
9.1411 + ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
9.1412 + (* bool -> bool -> term -> term *)
9.1413 + fun do_rest def core =
9.1414 + binarize ? binarize_nat_and_int_in_term
9.1415 + #> uncurry ? uncurry_term table
9.1416 + #> box ? box_fun_and_pair_in_term hol_ctxt def
9.1417 + #> destroy_constrs ? (pull_out_universal_constrs thy def
9.1418 + #> pull_out_existential_constrs thy
9.1419 + #> destroy_pulled_out_constrs hol_ctxt def)
9.1420 + #> curry_assms
9.1421 + #> destroy_universal_equalities
9.1422 + #> destroy_existential_equalities thy
9.1423 + #> simplify_constrs_and_sels thy
9.1424 + #> distribute_quantifiers
9.1425 + #> push_quantifiers_inward thy
9.1426 + #> not core ? Refute.close_form
9.1427 + #> Term.map_abs_vars shortest_name
9.1428 + in
9.1429 + (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
9.1430 + (got_all_mono_user_axioms, no_poly_user_axioms)),
9.1431 + do_rest false true core_t)
9.1432 + end
9.1433 +
9.1434 +end;
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 04 13:36:52 2010 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 04 16:03:15 2010 +0100
10.3 @@ -8,7 +8,7 @@
10.4 signature NITPICK_SCOPE =
10.5 sig
10.6 type styp = Nitpick_Util.styp
10.7 - type extended_context = Nitpick_HOL.extended_context
10.8 + type hol_context = Nitpick_HOL.hol_context
10.9
10.10 type constr_spec = {
10.11 const: styp,
10.12 @@ -28,7 +28,7 @@
10.13 constrs: constr_spec list}
10.14
10.15 type scope = {
10.16 - ext_ctxt: extended_context,
10.17 + hol_ctxt: hol_context,
10.18 card_assigns: (typ * int) list,
10.19 bits: int,
10.20 bisim_depth: int,
10.21 @@ -47,7 +47,7 @@
10.22 val scopes_equivalent : scope -> scope -> bool
10.23 val scope_less_eq : scope -> scope -> bool
10.24 val all_scopes :
10.25 - extended_context -> int -> (typ option * int list) list
10.26 + hol_context -> int -> (typ option * int list) list
10.27 -> (styp option * int list) list -> (styp option * int list) list
10.28 -> int list -> int list -> typ list -> typ list -> typ list
10.29 -> int * scope list
10.30 @@ -77,7 +77,7 @@
10.31 constrs: constr_spec list}
10.32
10.33 type scope = {
10.34 - ext_ctxt: extended_context,
10.35 + hol_ctxt: hol_context,
10.36 card_assigns: (typ * int) list,
10.37 bits: int,
10.38 bisim_depth: int,
10.39 @@ -131,7 +131,7 @@
10.40
10.41 (* (string -> string) -> scope
10.42 -> string list * string list * string list * string list * string list *)
10.43 -fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
10.44 +fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
10.45 bits, bisim_depth, datatypes, ...} : scope) =
10.46 let
10.47 val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
10.48 @@ -240,10 +240,9 @@
10.49
10.50 val max_bits = 31 (* Kodkod limit *)
10.51
10.52 -(* extended_context -> (typ option * int list) list
10.53 - -> (styp option * int list) list -> (styp option * int list) list -> int list
10.54 - -> int list -> typ -> block *)
10.55 -fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns
10.56 +(* hol_context -> (typ option * int list) list -> (styp option * int list) list
10.57 + -> (styp option * int list) list -> int list -> int list -> typ -> block *)
10.58 +fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
10.59 iters_assigns bitss bisim_depths T =
10.60 if T = @{typ unsigned_bit} then
10.61 [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
10.62 @@ -261,18 +260,18 @@
10.63 (const_for_iterator_type T)))]
10.64 else
10.65 (Card T, lookup_type_ints_assign thy cards_assigns T) ::
10.66 - (case datatype_constrs ext_ctxt T of
10.67 + (case datatype_constrs hol_ctxt T of
10.68 [_] => []
10.69 | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
10.70
10.71 -(* extended_context -> (typ option * int list) list
10.72 - -> (styp option * int list) list -> (styp option * int list) list -> int list
10.73 - -> int list -> typ list -> typ list -> block list *)
10.74 -fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns bitss
10.75 +(* hol_context -> (typ option * int list) list -> (styp option * int list) list
10.76 + -> (styp option * int list) list -> int list -> int list -> typ list
10.77 + -> typ list -> block list *)
10.78 +fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
10.79 bisim_depths mono_Ts nonmono_Ts =
10.80 let
10.81 (* typ -> block *)
10.82 - val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns
10.83 + val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
10.84 iters_assigns bitss bisim_depths
10.85 val mono_block = maps block_for mono_Ts
10.86 val nonmono_blocks = map block_for nonmono_Ts
10.87 @@ -313,10 +312,10 @@
10.88
10.89 type scope_desc = (typ * int) list * (styp * int) list
10.90
10.91 -(* extended_context -> scope_desc -> typ * int -> bool *)
10.92 -fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns)
10.93 +(* hol_context -> scope_desc -> typ * int -> bool *)
10.94 +fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
10.95 (T, k) =
10.96 - case datatype_constrs ext_ctxt T of
10.97 + case datatype_constrs hol_ctxt T of
10.98 [] => false
10.99 | xs =>
10.100 let
10.101 @@ -329,20 +328,20 @@
10.102 | effective_max card max = Int.min (card, max)
10.103 val max = map2 effective_max dom_cards maxes |> Integer.sum
10.104 in max < k end
10.105 -(* extended_context -> (typ * int) list -> (typ * int) list
10.106 - -> (styp * int) list -> bool *)
10.107 -fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns =
10.108 - exists (is_surely_inconsistent_card_assign ext_ctxt
10.109 +(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
10.110 + -> bool *)
10.111 +fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
10.112 + exists (is_surely_inconsistent_card_assign hol_ctxt
10.113 (seen @ rest, max_assigns)) seen
10.114
10.115 -(* extended_context -> scope_desc -> (typ * int) list option *)
10.116 -fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
10.117 +(* hol_context -> scope_desc -> (typ * int) list option *)
10.118 +fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
10.119 let
10.120 (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
10.121 fun aux seen [] = SOME seen
10.122 | aux seen ((T, 0) :: _) = NONE
10.123 | aux seen ((T, k) :: rest) =
10.124 - (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen)
10.125 + (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
10.126 rest max_assigns then
10.127 raise SAME ()
10.128 else
10.129 @@ -374,12 +373,12 @@
10.130 (* block -> scope_desc *)
10.131 fun scope_descriptor_from_block block =
10.132 fold_rev add_row_to_scope_descriptor block ([], [])
10.133 -(* extended_context -> block list -> int list -> scope_desc option *)
10.134 -fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
10.135 +(* hol_context -> block list -> int list -> scope_desc option *)
10.136 +fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
10.137 let
10.138 val (card_assigns, max_assigns) =
10.139 maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
10.140 - val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns)
10.141 + val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
10.142 |> the
10.143 in
10.144 SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
10.145 @@ -449,25 +448,25 @@
10.146 explicit_max = max, total = total} :: constrs
10.147 end
10.148
10.149 -(* extended_context -> (typ * int) list -> typ -> bool *)
10.150 -fun has_exact_card ext_ctxt card_assigns T =
10.151 +(* hol_context -> (typ * int) list -> typ -> bool *)
10.152 +fun has_exact_card hol_ctxt card_assigns T =
10.153 let val card = card_of_type card_assigns T in
10.154 - card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T
10.155 + card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
10.156 end
10.157
10.158 -(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
10.159 -fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) deep_dataTs
10.160 +(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
10.161 +fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
10.162 (desc as (card_assigns, _)) (T, card) =
10.163 let
10.164 val deep = member (op =) deep_dataTs T
10.165 val co = is_codatatype thy T
10.166 - val xs = boxed_datatype_constrs ext_ctxt T
10.167 + val xs = boxed_datatype_constrs hol_ctxt T
10.168 val self_recs = map (is_self_recursive_constr_type o snd) xs
10.169 val (num_self_recs, num_non_self_recs) =
10.170 List.partition I self_recs |> pairself length
10.171 - val complete = has_exact_card ext_ctxt card_assigns T
10.172 + val complete = has_exact_card hol_ctxt card_assigns T
10.173 val concrete = xs |> maps (binder_types o snd) |> maps binder_types
10.174 - |> forall (has_exact_card ext_ctxt card_assigns)
10.175 + |> forall (has_exact_card hol_ctxt card_assigns)
10.176 (* int -> int *)
10.177 fun sum_dom_cards max =
10.178 map (domain_card max card_assigns o snd) xs |> Integer.sum
10.179 @@ -487,12 +486,12 @@
10.180 min_bits_for_nat_value (fold Integer.max
10.181 (map snd card_assigns @ map snd max_assigns) 0)
10.182
10.183 -(* extended_context -> int -> typ list -> scope_desc -> scope *)
10.184 -fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break deep_dataTs
10.185 +(* hol_context -> int -> typ list -> scope_desc -> scope *)
10.186 +fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
10.187 (desc as (card_assigns, _)) =
10.188 let
10.189 val datatypes =
10.190 - map (datatype_spec_from_scope_descriptor ext_ctxt deep_dataTs desc)
10.191 + map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
10.192 (filter (is_datatype thy o fst) card_assigns)
10.193 val bits = card_of_type card_assigns @{typ signed_bit} - 1
10.194 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
10.195 @@ -500,7 +499,7 @@
10.196 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
10.197 val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
10.198 in
10.199 - {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes,
10.200 + {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
10.201 bits = bits, bisim_depth = bisim_depth,
10.202 ofs = if sym_break <= 0 then Typtab.empty
10.203 else offset_table_for_card_assigns thy card_assigns datatypes}
10.204 @@ -521,26 +520,26 @@
10.205 val max_scopes = 4096
10.206 val distinct_threshold = 512
10.207
10.208 -(* extended_context -> int -> (typ option * int list) list
10.209 +(* hol_context -> int -> (typ option * int list) list
10.210 -> (styp option * int list) list -> (styp option * int list) list -> int list
10.211 -> typ list -> typ list -> typ list -> int * scope list *)
10.212 -fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
10.213 +fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
10.214 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
10.215 let
10.216 val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
10.217 cards_assigns
10.218 - val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns
10.219 + val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
10.220 iters_assigns bitss bisim_depths mono_Ts
10.221 nonmono_Ts
10.222 val ranks = map rank_of_block blocks
10.223 val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
10.224 val head = take max_scopes all
10.225 - val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
10.226 + val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
10.227 head
10.228 in
10.229 (length all - length head,
10.230 descs |> length descs <= distinct_threshold ? distinct (op =)
10.231 - |> map (scope_from_descriptor ext_ctxt sym_break deep_dataTs))
10.232 + |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
10.233 end
10.234
10.235 end;