1 (* Title: HOL/Nitpick/Tools/nitpick_hol.ML
2 Author: Jasmin Blanchette, TU Muenchen
5 Auxiliary HOL-related functions used by Nitpick.
8 signature NITPICK_HOL =
10 type styp = Nitpick_Util.styp
11 type const_table = term list Symtab.table
12 type special_fun = (styp * int list * term list) * styp
13 type unrolled = styp * styp
14 type wf_cache = (styp * (bool * bool)) list
16 type extended_context = {
20 boxes: (typ option * bool option) list,
21 wfs: (styp option * bool option) list,
22 user_axioms: bool option,
24 destroy_constrs: bool,
27 star_linear_preds: bool,
30 tac_timeout: Time.time option,
32 case_names: (string * int) list,
33 def_table: const_table,
34 nondef_table: const_table,
35 user_nondefs: term list,
36 simp_table: const_table Unsynchronized.ref,
37 psimp_table: const_table,
38 intro_table: const_table,
39 ground_thm_table: term list Inttab.table,
40 ersatz_table: (string * string) list,
41 skolems: (string * string list) list Unsynchronized.ref,
42 special_funs: special_fun list Unsynchronized.ref,
43 unrolled_preds: unrolled list Unsynchronized.ref,
44 wf_cache: wf_cache Unsynchronized.ref,
45 constr_cache: (typ * styp list) list Unsynchronized.ref}
48 val numeral_prefix : string
49 val skolem_prefix : string
50 val eval_prefix : string
51 val original_name : string -> string
52 val unbox_type : typ -> typ
53 val string_for_type : Proof.context -> typ -> string
54 val prefix_name : string -> string -> string
55 val short_name : string -> string
56 val short_const_name : string -> string
57 val shorten_const_names_in_term : term -> term
58 val type_match : theory -> typ * typ -> bool
59 val const_match : theory -> styp * styp -> bool
60 val term_match : theory -> term * term -> bool
61 val is_TFree : typ -> bool
62 val is_higher_order_type : typ -> bool
63 val is_fun_type : typ -> bool
64 val is_set_type : typ -> bool
65 val is_pair_type : typ -> bool
66 val is_lfp_iterator_type : typ -> bool
67 val is_gfp_iterator_type : typ -> bool
68 val is_fp_iterator_type : typ -> bool
69 val is_boolean_type : typ -> bool
70 val is_integer_type : typ -> bool
71 val is_record_type : typ -> bool
72 val is_number_type : theory -> typ -> bool
73 val const_for_iterator_type : typ -> styp
74 val nth_range_type : int -> typ -> typ
75 val num_factors_in_type : typ -> int
76 val num_binder_types : typ -> int
77 val curried_binder_types : typ -> typ list
78 val mk_flat_tuple : typ -> term list -> term
79 val dest_n_tuple : int -> term -> term list
80 val instantiate_type : theory -> typ -> typ -> typ -> typ
81 val is_codatatype : theory -> typ -> bool
82 val is_pure_typedef : theory -> typ -> bool
83 val is_univ_typedef : theory -> typ -> bool
84 val is_datatype : theory -> typ -> bool
85 val is_record_constr : styp -> bool
86 val is_record_get : theory -> styp -> bool
87 val is_record_update : theory -> styp -> bool
88 val is_abs_fun : theory -> styp -> bool
89 val is_rep_fun : theory -> styp -> bool
90 val is_constr : theory -> styp -> bool
91 val is_stale_constr : theory -> styp -> bool
92 val is_sel : string -> bool
93 val discr_for_constr : styp -> styp
94 val num_sels_for_constr_type : typ -> int
95 val nth_sel_name_for_constr_name : string -> int -> string
96 val nth_sel_for_constr : styp -> int -> styp
97 val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
98 val sel_no_from_name : string -> int
99 val eta_expand : typ list -> term -> int -> term
100 val extensionalize : term -> term
101 val distinctness_formula : typ -> term list -> term
102 val register_frac_type : string -> (string * string) list -> theory -> theory
103 val unregister_frac_type : string -> theory -> theory
104 val register_codatatype : typ -> string -> styp list -> theory -> theory
105 val unregister_codatatype : typ -> theory -> theory
106 val datatype_constrs : extended_context -> typ -> styp list
107 val boxed_datatype_constrs : extended_context -> typ -> styp list
108 val num_datatype_constrs : extended_context -> typ -> int
109 val constr_name_for_sel_like : string -> string
110 val boxed_constr_for_sel : extended_context -> styp -> styp
111 val card_of_type : (typ * int) list -> typ -> int
112 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
113 val bounded_precise_card_of_type :
114 extended_context -> int -> int -> (typ * int) list -> typ -> int
115 val is_finite_type : extended_context -> typ -> bool
116 val all_axioms_of : theory -> term list * term list * term list
117 val arity_of_built_in_const : bool -> styp -> int option
118 val is_built_in_const : bool -> styp -> bool
119 val case_const_names : theory -> (string * int) list
120 val const_def_table : Proof.context -> term list -> const_table
121 val const_nondef_table : term list -> const_table
122 val const_simp_table : Proof.context -> const_table
123 val const_psimp_table : Proof.context -> const_table
124 val inductive_intro_table : Proof.context -> const_table -> const_table
125 val ground_theorem_table : theory -> term list Inttab.table
126 val ersatz_table : theory -> (string * string) list
127 val def_of_const : theory -> const_table -> styp -> term option
128 val is_inductive_pred : extended_context -> styp -> bool
129 val is_constr_pattern_lhs : theory -> term -> bool
130 val is_constr_pattern_formula : theory -> term -> bool
131 val merge_type_vars_in_terms : term list -> term list
132 val ground_types_in_type : extended_context -> typ -> typ list
133 val ground_types_in_terms : extended_context -> term list -> typ list
134 val format_type : int list -> int list -> typ -> typ
135 val format_term_type :
136 theory -> const_table -> (term option * int list) list -> term -> typ
137 val user_friendly_const :
138 extended_context -> string * string -> (term option * int list) list
139 -> styp -> term * typ
140 val assign_operator_for_const : styp -> string
141 val preprocess_term :
142 extended_context -> term -> ((term list * term list) * (bool * bool)) * term
145 structure Nitpick_HOL : NITPICK_HOL =
150 type const_table = term list Symtab.table
151 type special_fun = (styp * int list * term list) * styp
152 type unrolled = styp * styp
153 type wf_cache = (styp * (bool * bool)) list
155 type extended_context = {
158 max_bisim_depth: int,
159 boxes: (typ option * bool option) list,
160 wfs: (styp option * bool option) list,
161 user_axioms: bool option,
163 destroy_constrs: bool,
166 star_linear_preds: bool,
169 tac_timeout: Time.time option,
171 case_names: (string * int) list,
172 def_table: const_table,
173 nondef_table: const_table,
174 user_nondefs: term list,
175 simp_table: const_table Unsynchronized.ref,
176 psimp_table: const_table,
177 intro_table: const_table,
178 ground_thm_table: term list Inttab.table,
179 ersatz_table: (string * string) list,
180 skolems: (string * string list) list Unsynchronized.ref,
181 special_funs: special_fun list Unsynchronized.ref,
182 unrolled_preds: unrolled list Unsynchronized.ref,
183 wf_cache: wf_cache Unsynchronized.ref,
184 constr_cache: (typ * styp list) list Unsynchronized.ref}
186 structure Data = Theory_Data(
187 type T = {frac_types: (string * (string * string) list) list,
188 codatatypes: (string * (string * styp list)) list}
189 val empty = {frac_types = [], codatatypes = []}
191 fun merge ({frac_types = fs1, codatatypes = cs1},
192 {frac_types = fs2, codatatypes = cs2}) : T =
193 {frac_types = AList.merge (op =) (K true) (fs1, fs2),
194 codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
196 (* term * term -> term *)
197 fun s_conj (t1, @{const True}) = t1
198 | s_conj (@{const True}, t2) = t2
199 | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}
200 else HOLogic.mk_conj (t1, t2)
201 fun s_disj (t1, @{const False}) = t1
202 | s_disj (@{const False}, t2) = t2
203 | s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True}
204 else HOLogic.mk_disj (t1, t2)
205 (* term -> term -> term *)
207 HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
209 (* term -> term -> term list *)
210 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
211 if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
212 | strip_connective _ t = [t]
213 (* term -> term list * term *)
214 fun strip_any_connective (t as (t0 $ t1 $ t2)) =
215 if t0 mem [@{const "op &"}, @{const "op |"}] then
216 (strip_connective t0 t, t0)
219 | strip_any_connective t = ([t], @{const Not})
220 (* term -> term list *)
221 val conjuncts = strip_connective @{const "op &"}
222 val disjuncts = strip_connective @{const "op |"}
225 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
226 val sel_prefix = nitpick_prefix ^ "sel"
227 val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
228 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
229 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
230 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
231 val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep
232 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
233 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
234 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
235 val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
236 val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
237 val skolem_prefix = nitpick_prefix ^ "sk"
238 val special_prefix = nitpick_prefix ^ "sp"
239 val uncurry_prefix = nitpick_prefix ^ "unc"
240 val eval_prefix = nitpick_prefix ^ "eval"
241 val bound_var_prefix = "b"
242 val cong_var_prefix = "c"
243 val iter_var_prefix = "i"
244 val val_var_prefix = nitpick_prefix ^ "v"
245 val arg_var_prefix = "x"
248 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
249 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
250 (* int -> int -> string *)
251 fun skolem_prefix_for k j =
252 skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
253 fun uncurry_prefix_for k j =
254 uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
256 (* string -> string * string *)
257 val strip_first_name_sep =
258 Substring.full #> Substring.position name_sep ##> Substring.triml 1
259 #> pairself Substring.string
260 (* string -> string *)
261 fun original_name s =
262 if String.isPrefix nitpick_prefix s then
263 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
266 val after_name_sep = snd o strip_first_name_sep
268 (* When you add constants to these lists, make sure to handle them in
269 "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
271 val built_in_consts =
272 [(@{const_name all}, 1),
273 (@{const_name "=="}, 2),
274 (@{const_name "==>"}, 2),
275 (@{const_name Pure.conjunction}, 2),
276 (@{const_name Trueprop}, 1),
277 (@{const_name Not}, 1),
278 (@{const_name False}, 0),
279 (@{const_name True}, 0),
280 (@{const_name All}, 1),
281 (@{const_name Ex}, 1),
282 (@{const_name "op ="}, 2),
283 (@{const_name "op &"}, 2),
284 (@{const_name "op |"}, 2),
285 (@{const_name "op -->"}, 2),
286 (@{const_name If}, 3),
287 (@{const_name Let}, 2),
288 (@{const_name Unity}, 0),
289 (@{const_name Pair}, 2),
290 (@{const_name fst}, 1),
291 (@{const_name snd}, 1),
292 (@{const_name Id}, 0),
293 (@{const_name insert}, 2),
294 (@{const_name converse}, 1),
295 (@{const_name trancl}, 1),
296 (@{const_name rel_comp}, 2),
297 (@{const_name image}, 2),
298 (@{const_name Suc}, 0),
299 (@{const_name finite}, 1),
300 (@{const_name nat}, 0),
301 (@{const_name zero_nat_inst.zero_nat}, 0),
302 (@{const_name one_nat_inst.one_nat}, 0),
303 (@{const_name plus_nat_inst.plus_nat}, 0),
304 (@{const_name minus_nat_inst.minus_nat}, 0),
305 (@{const_name times_nat_inst.times_nat}, 0),
306 (@{const_name div_nat_inst.div_nat}, 0),
307 (@{const_name div_nat_inst.mod_nat}, 0),
308 (@{const_name ord_nat_inst.less_nat}, 2),
309 (@{const_name ord_nat_inst.less_eq_nat}, 2),
310 (@{const_name nat_gcd}, 0),
311 (@{const_name nat_lcm}, 0),
312 (@{const_name zero_int_inst.zero_int}, 0),
313 (@{const_name one_int_inst.one_int}, 0),
314 (@{const_name plus_int_inst.plus_int}, 0),
315 (@{const_name minus_int_inst.minus_int}, 0),
316 (@{const_name times_int_inst.times_int}, 0),
317 (@{const_name div_int_inst.div_int}, 0),
318 (@{const_name div_int_inst.mod_int}, 0),
319 (@{const_name uminus_int_inst.uminus_int}, 0),
320 (@{const_name ord_int_inst.less_int}, 2),
321 (@{const_name ord_int_inst.less_eq_int}, 2),
322 (@{const_name Tha}, 1),
323 (@{const_name Frac}, 0),
324 (@{const_name norm_frac}, 0)]
325 val built_in_descr_consts =
326 [(@{const_name The}, 1),
327 (@{const_name Eps}, 1)]
328 val built_in_typed_consts =
329 [((@{const_name of_nat}, nat_T --> int_T), 0)]
330 val built_in_set_consts =
331 [(@{const_name lower_semilattice_fun_inst.inf_fun}, 2),
332 (@{const_name upper_semilattice_fun_inst.sup_fun}, 2),
333 (@{const_name minus_fun_inst.minus_fun}, 2),
334 (@{const_name ord_fun_inst.less_eq_fun}, 2)]
337 fun unbox_type (Type (@{type_name fun_box}, Ts)) =
338 Type ("fun", map unbox_type Ts)
339 | unbox_type (Type (@{type_name pair_box}, Ts)) =
340 Type ("*", map unbox_type Ts)
341 | unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts)
343 (* Proof.context -> typ -> string *)
344 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type
346 (* string -> string -> string *)
347 val prefix_name = Long_Name.qualify o Long_Name.base_name
348 (* string -> string *)
349 fun short_name s = List.last (space_explode "." s) handle List.Empty => ""
350 (* string -> term -> term *)
351 val prefix_abs_vars = Term.map_abs_vars o prefix_name
353 val shorten_abs_vars = Term.map_abs_vars short_name
354 (* string -> string *)
355 fun short_const_name s =
356 case space_explode name_sep s of
357 [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
358 | ss => map short_name ss |> space_implode "_"
360 val shorten_const_names_in_term =
361 map_aterms (fn Const (s, T) => Const (short_const_name s, T) | t => t)
363 (* theory -> typ * typ -> bool *)
364 fun type_match thy (T1, T2) =
365 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
366 handle Type.TYPE_MATCH => false
367 (* theory -> styp * styp -> bool *)
368 fun const_match thy ((s1, T1), (s2, T2)) =
369 s1 = s2 andalso type_match thy (T1, T2)
370 (* theory -> term * term -> bool *)
371 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
372 | term_match thy (Free (s1, T1), Free (s2, T2)) =
373 const_match thy ((short_name s1, T1), (short_name s2, T2))
374 | term_match thy (t1, t2) = t1 aconv t2
377 fun is_TFree (TFree _) = true
379 fun is_higher_order_type (Type ("fun", _)) = true
380 | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
381 | is_higher_order_type _ = false
382 fun is_fun_type (Type ("fun", _)) = true
383 | is_fun_type _ = false
384 fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
385 | is_set_type _ = false
386 fun is_pair_type (Type ("*", _)) = true
387 | is_pair_type _ = false
388 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
389 | is_lfp_iterator_type _ = false
390 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
391 | is_gfp_iterator_type _ = false
392 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
393 val is_boolean_type = equal prop_T orf equal bool_T
394 val is_integer_type =
395 member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
396 val is_record_type = not o null o Record.dest_recTs
397 (* theory -> typ -> bool *)
398 fun is_frac_type thy (Type (s, [])) =
399 not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
400 | is_frac_type _ _ = false
401 fun is_number_type thy = is_integer_type orf is_frac_type thy
403 (* bool -> styp -> typ *)
404 fun iterator_type_for_const gfp (s, T) =
405 Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
408 fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
409 | const_for_iterator_type T =
410 raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
412 (* int -> typ -> typ * typ *)
413 fun strip_n_binders 0 T = ([], T)
414 | strip_n_binders n (Type ("fun", [T1, T2])) =
415 strip_n_binders (n - 1) T2 |>> cons T1
416 | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
417 strip_n_binders n (Type ("fun", Ts))
418 | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
420 val nth_range_type = snd oo strip_n_binders
423 fun num_factors_in_type (Type ("*", [T1, T2])) =
424 fold (Integer.add o num_factors_in_type) [T1, T2] 0
425 | num_factors_in_type _ = 1
426 fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
427 | num_binder_types _ = 0
428 (* typ -> typ list *)
429 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
430 fun maybe_curried_binder_types T =
431 (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
433 (* typ -> term list -> term *)
434 fun mk_flat_tuple _ [t] = t
435 | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
436 HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
437 | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
438 (* int -> term -> term list *)
439 fun dest_n_tuple 1 t = [t]
440 | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
442 (* int -> typ -> typ list *)
443 fun dest_n_tuple_type 1 T = [T]
444 | dest_n_tuple_type n (Type (_, [T1, T2])) =
445 T1 :: dest_n_tuple_type (n - 1) T2
446 | dest_n_tuple_type _ T =
447 raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
449 (* (typ * typ) list -> typ -> typ *)
450 fun typ_subst [] T = T
455 case AList.lookup (op =) ps T of
457 | NONE => case T of Type (s, Ts) => Type (s, map subst Ts) | _ => T
460 (* theory -> typ -> typ -> typ -> typ *)
461 fun instantiate_type thy T1 T1' T2 =
462 Same.commit (Envir.subst_type_same
463 (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
465 handle Type.TYPE_MATCH =>
466 raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
468 (* theory -> typ -> typ -> styp *)
469 fun repair_constr_type thy body_T' T =
470 instantiate_type thy (body_type T) body_T' T
472 (* string -> (string * string) list -> theory -> theory *)
473 fun register_frac_type frac_s ersaetze thy =
475 val {frac_types, codatatypes} = Data.get thy
476 val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
477 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
478 (* string -> theory -> theory *)
479 fun unregister_frac_type frac_s = register_frac_type frac_s []
481 (* typ -> string -> styp list -> theory -> theory *)
482 fun register_codatatype co_T case_name constr_xs thy =
484 val {frac_types, codatatypes} = Data.get thy
485 val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
486 val (co_s, co_Ts) = dest_Type co_T
488 if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()
489 else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
490 val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
492 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
493 (* typ -> theory -> theory *)
494 fun unregister_codatatype co_T = register_codatatype co_T "" []
497 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
498 set_def: thm option, prop_of_Rep: thm, set_name: string,
499 Abs_inverse: thm option, Rep_inverse: thm option}
501 (* theory -> string -> typedef_info *)
502 fun typedef_info thy s =
503 if is_frac_type thy (Type (s, [])) then
504 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
505 Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
506 set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
508 set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
509 else case Typedef.get_info thy s of
510 SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
512 SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
513 Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
514 set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
515 Rep_inverse = SOME Rep_inverse}
518 (* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
519 e.g., by adding a field to "DatatypeAux.info". *)
521 fun is_basic_datatype s =
522 s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
523 @{type_name nat}, @{type_name int}, "Code_Numeral.code_numeral"]
524 (* theory -> string -> bool *)
525 val is_typedef = is_some oo typedef_info
526 val is_real_datatype = is_some oo Datatype.get_info
527 (* theory -> typ -> bool *)
528 fun is_codatatype thy (T as Type (s, _)) =
529 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
530 |> Option.map snd |> these))
531 | is_codatatype _ _ = false
532 fun is_pure_typedef thy (T as Type (s, _)) =
533 is_typedef thy s andalso
534 not (is_real_datatype thy s orelse is_codatatype thy T
535 orelse is_record_type T orelse is_integer_type T)
536 | is_pure_typedef _ _ = false
537 fun is_univ_typedef thy (Type (s, _)) =
538 (case typedef_info thy s of
539 SOME {set_def, prop_of_Rep, ...} =>
542 try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
544 try (fst o dest_Const o snd o HOLogic.dest_mem
545 o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
547 | is_univ_typedef _ _ = false
548 fun is_datatype thy (T as Type (s, _)) =
549 (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind})
550 andalso not (is_basic_datatype s)
551 | is_datatype _ _ = false
553 (* theory -> typ -> (string * typ) list * (string * typ) *)
554 fun all_record_fields thy T =
555 let val (recs, more) = Record.get_extT_fields thy T in
556 recs @ more :: all_record_fields thy (snd more)
560 fun is_record_constr (x as (s, T)) =
561 String.isSuffix Record.extN s andalso
562 let val dataT = body_type T in
563 is_record_type dataT andalso
564 s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
566 (* theory -> typ -> int *)
567 val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
568 (* theory -> string -> typ -> int *)
569 fun no_of_record_field thy s T1 =
570 find_index (equal s o fst) (Record.get_extT_fields thy T1 ||> single |> op @)
571 (* theory -> styp -> bool *)
572 fun is_record_get thy (s, Type ("fun", [T1, _])) =
573 exists (equal s o fst) (all_record_fields thy T1)
574 | is_record_get _ _ = false
575 fun is_record_update thy (s, T) =
576 String.isSuffix Record.updateN s andalso
577 exists (equal (unsuffix Record.updateN s) o fst)
578 (all_record_fields thy (body_type T))
579 handle TYPE _ => false
580 fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
581 (case typedef_info thy s' of
582 SOME {Abs_name, ...} => s = Abs_name
584 | is_abs_fun _ _ = false
585 fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
586 (case typedef_info thy s' of
587 SOME {Rep_name, ...} => s = Rep_name
589 | is_rep_fun _ _ = false
591 (* theory -> styp -> styp *)
592 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
593 (case typedef_info thy s' of
594 SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
595 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
596 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
598 (* theory -> styp -> bool *)
599 fun is_coconstr thy (s, T) =
601 val {codatatypes, ...} = Data.get thy
602 val co_T = body_type T
603 val co_s = dest_Type co_T |> fst
605 exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
606 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
608 handle TYPE ("dest_Type", _, _) => false
609 fun is_constr_like thy (s, T) =
610 s mem [@{const_name FunBox}, @{const_name PairBox}] orelse
611 let val (x as (s, T)) = (s, unbox_type T) in
612 Refute.is_IDT_constructor thy x orelse is_record_constr x
613 orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
614 orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]
615 orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
616 orelse is_coconstr thy x
618 fun is_stale_constr thy (x as (_, T)) =
619 is_codatatype thy (body_type T) andalso is_constr_like thy x
620 andalso not (is_coconstr thy x)
621 fun is_constr thy (x as (_, T)) =
623 andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
624 andalso not (is_stale_constr thy x)
626 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
627 val is_sel_like_and_no_discr =
628 String.isPrefix sel_prefix
629 orf (member (op =) [@{const_name fst}, @{const_name snd}])
631 datatype boxability =
632 InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
634 (* boxability -> boxability *)
635 fun in_fun_lhs_for InConstr = InSel
636 | in_fun_lhs_for _ = InFunLHS
637 fun in_fun_rhs_for InConstr = InConstr
638 | in_fun_rhs_for InSel = InSel
639 | in_fun_rhs_for InFunRHS1 = InFunRHS2
640 | in_fun_rhs_for _ = InFunRHS1
642 (* extended_context -> boxability -> typ -> bool *)
643 fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
646 boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T))
648 boxy mem [InPair, InFunRHS1, InFunRHS2]
649 orelse (boxy mem [InExpr, InFunLHS]
650 andalso exists (is_boxing_worth_it ext_ctxt InPair)
651 (map (box_type ext_ctxt InPair) Ts))
653 (* extended_context -> boxability -> string * typ list -> string *)
654 and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
655 case triple_lookup (type_match thy) boxes (Type z) of
656 SOME (SOME box_me) => box_me
657 | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
658 (* extended_context -> boxability -> typ -> typ *)
659 and box_type ext_ctxt boxy T =
661 Type (z as ("fun", [T1, T2])) =>
662 if not (boxy mem [InConstr, InSel])
663 andalso should_box_type ext_ctxt boxy z then
664 Type (@{type_name fun_box},
665 [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
667 box_type ext_ctxt (in_fun_lhs_for boxy) T1
668 --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
669 | Type (z as ("*", Ts)) =>
670 if should_box_type ext_ctxt boxy z then
671 Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
673 Type ("*", map (box_type ext_ctxt
674 (if boxy mem [InConstr, InSel] then boxy
679 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
682 fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
683 (* string -> int -> string *)
684 fun nth_sel_name_for_constr_name s n =
685 if s = @{const_name Pair} then
686 if n = 0 then @{const_name fst} else @{const_name snd}
689 (* styp -> int -> styp *)
690 fun nth_sel_for_constr x ~1 = discr_for_constr x
691 | nth_sel_for_constr (s, T) n =
692 (nth_sel_name_for_constr_name s n,
693 body_type T --> nth (maybe_curried_binder_types T) n)
694 (* extended_context -> styp -> int -> styp *)
695 fun boxed_nth_sel_for_constr ext_ctxt =
696 apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr
699 fun sel_no_from_name s =
700 if String.isPrefix discr_prefix s then
702 else if String.isPrefix sel_prefix s then
703 s |> unprefix sel_prefix |> Int.fromString |> the
704 else if s = @{const_name snd} then
709 (* typ list -> term -> int -> term *)
710 fun eta_expand _ t 0 = t
711 | eta_expand Ts (Abs (s, T, t')) n =
712 Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
713 | eta_expand Ts t n =
714 fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
715 (List.take (binder_types (fastype_of1 (Ts, t)), n))
716 (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
719 fun extensionalize t =
721 (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
722 | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>
723 let val v = Var ((s, maxidx_of_term t + 1), T) in
724 extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))
728 (* typ -> term list -> term *)
729 fun distinctness_formula T =
730 all_distinct_unordered_pairs_of
731 #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
732 #> List.foldr (s_conj o swap) @{const True}
735 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
736 fun suc_const T = Const (@{const_name Suc}, T --> T)
738 (* theory -> typ -> styp list *)
739 fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
740 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
741 SOME (_, xs' as (_ :: _)) =>
742 map (apsnd (repair_constr_type thy T)) xs'
744 if is_datatype thy T then
745 case Datatype.get_info thy s of
746 SOME {index, descr, ...} =>
748 val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
751 (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
755 if is_record_type T then
757 val s' = unsuffix Record.ext_typeN s ^ Record.extN
758 val T' = (Record.get_extT_fields thy T
759 |> apsnd single |> uncurry append |> map snd) ---> T
761 else case typedef_info thy s of
762 SOME {abs_type, rep_type, Abs_name, ...} =>
763 [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
765 if T = @{typ ind} then
766 [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
771 | uncached_datatype_constrs _ _ = []
772 (* extended_context -> typ -> styp list *)
773 fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
775 case AList.lookup (op =) (!constr_cache) T of
778 let val xs = uncached_datatype_constrs thy T in
779 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
781 fun boxed_datatype_constrs ext_ctxt =
782 map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
783 (* extended_context -> typ -> int *)
784 val num_datatype_constrs = length oo datatype_constrs
786 (* string -> string *)
787 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
788 | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
789 | constr_name_for_sel_like s' = original_name s'
790 (* extended_context -> styp -> styp *)
791 fun boxed_constr_for_sel ext_ctxt (s', T') =
792 let val s = constr_name_for_sel_like s' in
793 AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
796 (* extended_context -> styp -> term *)
797 fun discr_term_for_constr ext_ctxt (x as (s, T)) =
798 let val dataT = body_type T in
799 if s = @{const_name Suc} then
801 @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
802 else if num_datatype_constrs ext_ctxt dataT >= 2 then
803 Const (discr_for_constr x)
805 Abs (Name.uu, dataT, @{const True})
808 (* extended_context -> styp -> term -> term *)
809 fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
812 if x = x' then @{const True}
813 else if is_constr_like thy x' then @{const False}
814 else betapply (discr_term_for_constr ext_ctxt x, t)
815 | _ => betapply (discr_term_for_constr ext_ctxt x, t)
817 (* styp -> term -> term *)
818 fun nth_arg_sel_term_for_constr (x as (s, T)) n =
819 let val (arg_Ts, dataT) = strip_type T in
820 if dataT = nat_T then
821 @{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}
822 else if is_pair_type dataT then
823 Const (nth_sel_for_constr x n)
826 (* int -> typ -> int * term *)
827 fun aux m (Type ("*", [T1, T2])) =
829 val (m, t1) = aux m T1
830 val (m, t2) = aux m T2
831 in (m, HOLogic.mk_prod (t1, t2)) end
833 (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
835 val m = fold (Integer.add o num_factors_in_type)
836 (List.take (arg_Ts, n)) 0
837 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
839 (* theory -> styp -> term -> int -> typ -> term *)
840 fun select_nth_constr_arg thy x t n res_T =
843 if x = x' then nth args n
844 else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
845 else betapply (nth_arg_sel_term_for_constr x n, t)
846 | _ => betapply (nth_arg_sel_term_for_constr x n, t)
848 (* theory -> styp -> term list -> term *)
849 fun construct_value _ x [] = Const x
850 | construct_value thy (x as (s, _)) args =
851 let val args = map Envir.eta_contract args in
853 Const (x' as (s', _)) $ t =>
854 if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s
855 andalso forall (fn (n, t') =>
856 select_nth_constr_arg thy x t n dummyT = t')
857 (index_seq 0 (length args) ~~ args) then
860 list_comb (Const x, args)
861 | _ => list_comb (Const x, args)
864 (* extended_context -> typ -> term -> term *)
865 fun constr_expand (ext_ctxt as {thy, ...}) T t =
867 Const x => if is_constr_like thy x then t else raise SAME ()
868 | _ => raise SAME ())
872 if is_pair_type T then
873 let val (T1, T2) = HOLogic.dest_prodT T in
874 (@{const_name Pair}, [T1, T2] ---> T)
877 datatype_constrs ext_ctxt T |> the_single
878 val arg_Ts = binder_types T'
880 list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
881 (index_seq 0 (length arg_Ts)) arg_Ts)
884 (* (typ * int) list -> typ -> int *)
885 fun card_of_type asgns (Type ("fun", [T1, T2])) =
886 reasonable_power (card_of_type asgns T2) (card_of_type asgns T1)
887 | card_of_type asgns (Type ("*", [T1, T2])) =
888 card_of_type asgns T1 * card_of_type asgns T2
889 | card_of_type _ (Type (@{type_name itself}, _)) = 1
890 | card_of_type _ @{typ prop} = 2
891 | card_of_type _ @{typ bool} = 2
892 | card_of_type _ @{typ unit} = 1
893 | card_of_type asgns T =
894 case AList.lookup (op =) asgns T of
896 | NONE => if T = @{typ bisim_iterator} then 0
897 else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
898 (* int -> (typ * int) list -> typ -> int *)
899 fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) =
901 val k1 = bounded_card_of_type max default_card asgns T1
902 val k2 = bounded_card_of_type max default_card asgns T2
904 if k1 = max orelse k2 = max then max
905 else Int.min (max, reasonable_power k2 k1)
907 | bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) =
909 val k1 = bounded_card_of_type max default_card asgns T1
910 val k2 = bounded_card_of_type max default_card asgns T2
911 in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
912 | bounded_card_of_type max default_card asgns T =
913 Int.min (max, if default_card = ~1 then
917 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
919 (* extended_context -> int -> (typ * int) list -> typ -> int *)
920 fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
922 (* typ list -> typ -> int *)
927 Type ("fun", [T1, T2]) =>
929 val k1 = aux avoid T1
930 val k2 = aux avoid T2
932 if k1 = 0 orelse k2 = 0 then 0
933 else if k1 >= max orelse k2 >= max then max
934 else Int.min (max, reasonable_power k2 k1)
936 | Type ("*", [T1, T2]) =>
938 val k1 = aux avoid T1
939 val k2 = aux avoid T2
941 if k1 = 0 orelse k2 = 0 then 0
942 else if k1 >= max orelse k2 >= max then max
943 else Int.min (max, k1 * k2)
945 | Type (@{type_name itself}, _) => 1
950 (case datatype_constrs ext_ctxt T of
951 [] => if is_integer_type T then 0 else raise SAME ()
955 datatype_constrs ext_ctxt T
956 |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
959 if exists (equal 0) constr_cards then 0
960 else Integer.sum constr_cards
962 | _ => raise SAME ())
963 handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
964 in Int.min (max, aux [] T) end
966 (* extended_context -> typ -> bool *)
967 fun is_finite_type ext_ctxt =
968 not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []
971 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
972 | is_ground_term (Const _) = true
973 | is_ground_term _ = false
975 (* term -> word -> word *)
976 fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
977 | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
980 val hash_term = Word.toInt o hashw_term
982 (* term list -> (indexname * typ) list *)
983 fun special_bounds ts =
984 fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
986 (* indexname * typ -> term -> term *)
987 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
989 (* theory -> string -> bool *)
990 fun is_funky_typedef_name thy s =
991 s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
993 orelse is_frac_type thy (Type (s, []))
994 (* theory -> term -> bool *)
995 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
996 | is_funky_typedef _ _ = false
998 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
999 $ Const (@{const_name TYPE}, _)) = true
1000 | is_arity_type_axiom _ = false
1001 (* theory -> bool -> term -> bool *)
1002 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
1003 is_typedef_axiom thy boring t2
1004 | is_typedef_axiom thy boring
1005 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
1006 $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
1007 boring <> is_funky_typedef_name thy s andalso is_typedef thy s
1008 | is_typedef_axiom _ _ _ = false
1010 (* Distinguishes between (1) constant definition axioms, (2) type arity and
1011 typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
1012 Typedef axioms are uninteresting to Nitpick, because it can retrieve them
1013 using "typedef_info". *)
1014 (* theory -> (string * term) list -> string list -> term list * term list *)
1015 fun partition_axioms_by_definitionality thy axioms def_names =
1017 val axioms = sort (fast_string_ord o pairself fst) axioms
1018 val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
1020 OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
1021 |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
1022 in pairself (map snd) (defs, nondefs) end
1024 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
1025 will do as long as it contains all the "axioms" and "axiomatization"
1027 (* theory -> bool *)
1028 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
1031 val is_plain_definition =
1035 case strip_comb t1 of
1036 (Const _, args) => forall is_Var args
1037 andalso not (has_duplicates (op =) args)
1039 fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
1040 | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
1045 (* theory -> term list * term list * term list *)
1046 fun all_axioms_of thy =
1048 (* theory list -> term list *)
1049 val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
1050 val specs = Defs.all_specifications_of (Theory.defs_of thy)
1051 val def_names = specs |> maps snd |> map_filter #def
1052 |> OrdList.make fast_string_ord
1053 val thys = thy :: Theory.ancestors_of thy
1054 val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
1055 val built_in_axioms = axioms_of_thys built_in_thys
1056 val user_axioms = axioms_of_thys user_thys
1057 val (built_in_defs, built_in_nondefs) =
1058 partition_axioms_by_definitionality thy built_in_axioms def_names
1059 ||> filter (is_typedef_axiom thy false)
1060 val (user_defs, user_nondefs) =
1061 partition_axioms_by_definitionality thy user_axioms def_names
1062 val (built_in_nondefs, user_nondefs) =
1063 List.partition (is_typedef_axiom thy false) user_nondefs
1064 |>> append built_in_nondefs
1065 val defs = (thy |> PureThy.all_thms_of
1066 |> filter (equal Thm.definitionK o Thm.get_kind o snd)
1067 |> map (prop_of o snd) |> filter is_plain_definition) @
1068 user_defs @ built_in_defs
1069 in (defs, built_in_nondefs, user_nondefs) end
1071 (* bool -> styp -> int option *)
1072 fun arity_of_built_in_const fast_descrs (s, T) =
1073 if s = @{const_name If} then
1074 if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
1075 else case AList.lookup (op =)
1077 |> fast_descrs ? append built_in_descr_consts) s of
1080 case AList.lookup (op =) built_in_typed_consts (s, T) of
1083 if is_fun_type T andalso is_set_type (domain_type T) then
1084 AList.lookup (op =) built_in_set_consts s
1087 (* bool -> styp -> bool *)
1088 val is_built_in_const = is_some oo arity_of_built_in_const
1090 (* This function is designed to work for both real definition axioms and
1091 simplification rules (equational specifications). *)
1093 fun term_under_def t =
1095 @{const "==>"} $ _ $ t2 => term_under_def t2
1096 | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
1097 | @{const Trueprop} $ t1 => term_under_def t1
1098 | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
1099 | Abs (_, _, t') => term_under_def t'
1100 | t1 $ _ => term_under_def t1
1103 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
1104 traversal of the term, without which the wrong occurrence of a constant could
1105 be matched in the face of overloading. *)
1106 (* theory -> bool -> const_table -> styp -> term list *)
1107 fun def_props_for_const thy fast_descrs table (x as (s, _)) =
1108 if is_built_in_const fast_descrs x then
1111 these (Symtab.lookup table s)
1112 |> map_filter (try (Refute.specialize_type thy x))
1113 |> filter (equal (Const x) o term_under_def)
1115 (* theory -> term -> term option *)
1116 fun normalized_rhs_of thy t =
1118 (* term option -> term option *)
1119 fun aux (v as Var _) (SOME t) = SOME (lambda v t)
1120 | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
1124 Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
1125 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
1127 | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
1128 val args = strip_comb lhs |> snd
1129 in fold_rev aux args (SOME rhs) end
1131 (* theory -> const_table -> styp -> term option *)
1132 fun def_of_const thy table (x as (s, _)) =
1133 if is_built_in_const false x orelse original_name s <> s then
1136 x |> def_props_for_const thy false table |> List.last
1137 |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
1138 handle List.Empty => NONE
1140 datatype fixpoint_kind = Lfp | Gfp | NoFp
1142 (* term -> fixpoint_kind *)
1143 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
1144 | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
1145 | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
1146 | fixpoint_kind_of_rhs _ = NoFp
1148 (* theory -> const_table -> term -> bool *)
1149 fun is_mutually_inductive_pred_def thy table t =
1152 fun is_good_arg (Bound _) = true
1153 | is_good_arg (Const (s, _)) =
1154 s mem [@{const_name True}, @{const_name False}, @{const_name undefined}]
1155 | is_good_arg _ = false
1157 case t |> strip_abs_body |> strip_comb of
1158 (Const x, ts as (_ :: _)) =>
1159 (case def_of_const thy table x of
1160 SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
1164 (* theory -> const_table -> term -> term *)
1165 fun unfold_mutually_inductive_preds thy table =
1166 map_aterms (fn t as Const x =>
1167 (case def_of_const thy table x of
1169 let val t' = Envir.eta_contract t' in
1170 if is_mutually_inductive_pred_def thy table t' then t'
1176 (* term -> string * term *)
1177 fun pair_for_prop t =
1178 case term_under_def t of
1179 Const (s, _) => (s, t)
1180 | Free _ => raise NOT_SUPPORTED "local definitions"
1181 | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
1183 (* (Proof.context -> term list) -> Proof.context -> const_table *)
1184 fun table_for get ctxt =
1185 get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
1187 (* theory -> (string * int) list *)
1188 fun case_const_names thy =
1189 Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
1190 if is_basic_datatype dtype_s then
1193 cons (case_name, AList.lookup (op =) descr index
1194 |> the |> #3 |> length))
1195 (Datatype.get_all thy) [] @
1196 map (apsnd length o snd) (#codatatypes (Data.get thy))
1198 (* Proof.context -> term list -> const_table *)
1199 fun const_def_table ctxt ts =
1200 table_for (map prop_of o Nitpick_Defs.get) ctxt
1201 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
1202 (map pair_for_prop ts)
1203 (* term list -> const_table *)
1204 fun const_nondef_table ts =
1205 fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
1206 |> AList.group (op =) |> Symtab.make
1207 (* Proof.context -> const_table *)
1208 val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
1209 val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
1210 (* Proof.context -> const_table -> const_table *)
1211 fun inductive_intro_table ctxt def_table =
1212 table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
1213 def_table o prop_of)
1214 o Nitpick_Intros.get) ctxt
1215 (* theory -> term list Inttab.table *)
1216 fun ground_theorem_table thy =
1217 fold ((fn @{const Trueprop} $ t1 =>
1218 is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
1219 | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
1221 val basic_ersatz_table =
1222 [(@{const_name prod_case}, @{const_name split}),
1223 (@{const_name card}, @{const_name card'}),
1224 (@{const_name setsum}, @{const_name setsum'}),
1225 (@{const_name fold_graph}, @{const_name fold_graph'}),
1226 (@{const_name wf}, @{const_name wf'}),
1227 (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
1228 (@{const_name wfrec}, @{const_name wfrec'})]
1230 (* theory -> (string * string) list *)
1231 fun ersatz_table thy =
1232 fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
1234 (* const_table Unsynchronized.ref -> string -> term list -> unit *)
1235 fun add_simps simp_table s eqs =
1236 Unsynchronized.change simp_table
1237 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
1239 (* Similar to "Refute.specialize_type" but returns all matches rather than only
1240 the first (preorder) match. *)
1241 (* theory -> styp -> term -> term list *)
1242 fun multi_specialize_type thy slack (x as (s, T)) t =
1244 (* term -> (typ * term) list -> (typ * term) list *)
1245 fun aux (Const (s', T')) ys =
1247 ys |> (if AList.defined (op =) ys T' then
1250 cons (T', Refute.monomorphic_term
1251 (Sign.typ_match thy (T', T) Vartab.empty) t)
1252 handle Type.TYPE_MATCH => I
1253 | Refute.REFUTE _ =>
1257 raise NOT_SUPPORTED ("too much polymorphism in \
1258 \axiom involving " ^ quote s))
1262 in map snd (fold_aterms aux t []) end
1264 (* theory -> bool -> const_table -> styp -> term list *)
1265 fun nondef_props_for_const thy slack table (x as (s, _)) =
1266 these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
1268 (* theory -> styp list -> term list *)
1269 fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
1270 let val abs_T = Type (abs_s, abs_Ts) in
1271 if is_univ_typedef thy abs_T then
1273 else case typedef_info thy abs_s of
1274 SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,
1277 val rep_T = instantiate_type thy abs_type abs_T rep_type
1278 val rep_t = Const (Rep_name, abs_T --> rep_T)
1279 val set_t = Const (set_name, rep_T --> bool_T)
1281 prop_of_Rep |> HOLogic.dest_Trueprop
1282 |> Refute.specialize_type thy (dest_Const rep_t)
1283 |> HOLogic.dest_mem |> snd
1285 [HOLogic.all_const abs_T
1286 $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
1287 |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
1288 |> map HOLogic.mk_Trueprop
1292 (* theory -> styp -> term list *)
1293 fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
1294 let val abs_T = domain_type T in
1295 typedef_info thy (fst (dest_Type abs_T)) |> the
1296 |> pairf #Abs_inverse #Rep_inverse
1297 |> pairself (Refute.specialize_type thy x o prop_of o the)
1301 (* theory -> int * styp -> term *)
1302 fun constr_case_body thy (j, (x as (_, T))) =
1303 let val arg_Ts = binder_types T in
1304 list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
1305 (index_seq 0 (length arg_Ts)) arg_Ts)
1307 (* extended_context -> typ -> int * styp -> term -> term *)
1308 fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
1309 Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
1310 $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
1312 (* extended_context -> typ -> typ -> term *)
1313 fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
1315 val xs = datatype_constrs ext_ctxt dataT
1316 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
1317 val (xs', x) = split_last xs
1319 constr_case_body thy (1, x)
1320 |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
1321 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
1324 (* extended_context -> string -> typ -> typ -> term -> term *)
1325 fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
1326 let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
1327 case no_of_record_field thy s rec_T of
1328 ~1 => (case rec_T of
1329 Type (_, Ts as _ :: _) =>
1331 val rec_T' = List.last Ts
1332 val j = num_record_fields thy rec_T - 1
1334 select_nth_constr_arg thy constr_x t j res_T
1335 |> optimized_record_get ext_ctxt s rec_T' res_T
1337 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
1339 | j => select_nth_constr_arg thy constr_x t j res_T
1341 (* extended_context -> string -> typ -> term -> term -> term *)
1342 fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
1344 val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
1345 val Ts = binder_types constr_T
1347 val special_j = no_of_record_field thy s rec_T
1348 val ts = map2 (fn j => fn T =>
1350 val t = select_nth_constr_arg thy constr_x rec_t j T
1352 if j = special_j then
1354 else if j = n - 1 andalso special_j = ~1 then
1355 optimized_record_update ext_ctxt s
1356 (rec_T |> dest_Type |> snd |> List.last) fun_t t
1359 end) (index_seq 0 n) Ts
1360 in list_comb (Const constr_x, ts) end
1362 (* Constants "c" whose definition is of the form "c == c'", where "c'" is also a
1363 constant, are said to be trivial. For those, we ignore the simplification
1364 rules and use the definition instead, to ensure that built-in symbols like
1365 "ord_nat_inst.less_eq_nat" are picked up correctly. *)
1366 (* theory -> const_table -> styp -> bool *)
1367 fun has_trivial_definition thy table x =
1368 case def_of_const thy table x of SOME (Const _) => true | _ => false
1370 (* theory -> const_table -> string * typ -> fixpoint_kind *)
1371 fun fixpoint_kind_of_const thy table x =
1372 if is_built_in_const false x then
1375 fixpoint_kind_of_rhs (the (def_of_const thy table x))
1376 handle Option.Option => NoFp
1378 (* extended_context -> styp -> bool *)
1379 fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
1380 : extended_context) x =
1381 not (null (def_props_for_const thy fast_descrs intro_table x))
1382 andalso fixpoint_kind_of_const thy def_table x <> NoFp
1383 fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
1384 : extended_context) x =
1385 exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
1386 [!simp_table, psimp_table]
1387 fun is_inductive_pred ext_ctxt =
1388 is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
1389 fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
1390 (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
1391 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
1392 andf (not o has_trivial_definition thy def_table)
1394 (* term * term -> term *)
1395 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
1396 | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
1397 | s_betapply p = betapply p
1398 (* term * term list -> term *)
1399 val s_betapplys = Library.foldl s_betapply
1402 fun lhs_of_equation t =
1404 Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1405 | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
1406 | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
1407 | @{const Trueprop} $ t1 => lhs_of_equation t1
1408 | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1409 | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
1410 | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
1412 (* theory -> term -> bool *)
1413 fun is_constr_pattern _ (Bound _) = true
1414 | is_constr_pattern _ (Var _) = true
1415 | is_constr_pattern thy t =
1416 case strip_comb t of
1417 (Const (x as (s, _)), args) =>
1418 is_constr_like thy x andalso forall (is_constr_pattern thy) args
1420 fun is_constr_pattern_lhs thy t =
1421 forall (is_constr_pattern thy) (snd (strip_comb t))
1422 fun is_constr_pattern_formula thy t =
1423 case lhs_of_equation t of
1424 SOME t' => is_constr_pattern_lhs thy t'
1427 val unfold_max_depth = 255
1428 val axioms_max_depth = 255
1430 (* extended_context -> term -> term *)
1431 fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
1432 case_names, def_table, ground_thm_table,
1433 ersatz_table, ...}) =
1435 (* int -> typ list -> term -> term *)
1436 fun do_term depth Ts t =
1438 (t0 as Const (@{const_name Int.number_class.number_of},
1439 Type ("fun", [_, ran_T]))) $ t1 =>
1440 ((if is_number_type thy ran_T then
1442 val j = t1 |> HOLogic.dest_numeral
1443 |> ran_T = nat_T ? Integer.max 0
1444 val s = numeral_prefix ^ signed_string_of_int j
1446 if is_integer_type ran_T then
1449 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
1452 handle TERM _ => raise SAME ()
1455 handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
1456 | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
1457 do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
1458 | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
1459 $ (t2 as Abs (_, _, t2')) =>
1460 betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
1461 map (do_term depth Ts) [t1, t2])
1462 | Const (x as (@{const_name distinct},
1463 Type ("fun", [Type (@{type_name list}, [T']), _])))
1465 (t1 |> HOLogic.dest_list |> distinctness_formula T'
1466 handle TERM _ => do_const depth Ts t x [t1])
1467 | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
1468 if is_ground_term t1
1469 andalso exists (Pattern.matches thy o rpair t1)
1470 (Inttab.lookup_list ground_thm_table
1471 (hash_term t1)) then
1474 do_const depth Ts t x [t1, t2, t3]
1475 | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
1476 | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
1477 | Const x $ t1 => do_const depth Ts t x [t1]
1478 | Const x => do_const depth Ts t x []
1479 | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
1483 | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
1484 (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
1485 and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
1486 (Abs (Name.uu, body_type T,
1487 select_nth_constr_arg thy x (Bound 0) n res_T), [])
1488 | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
1489 (select_nth_constr_arg thy x (do_term depth Ts t) n res_T, ts)
1490 (* int -> typ list -> term -> styp -> term list -> term *)
1491 and do_const depth Ts t (x as (s, T)) ts =
1492 case AList.lookup (op =) ersatz_table s of
1494 do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
1498 if is_built_in_const fast_descrs x then
1500 else case AList.lookup (op =) case_names s of
1503 val (dataT, res_T) = nth_range_type n T
1504 |> pairf domain_type range_type
1506 (optimized_case_def ext_ctxt dataT res_T
1507 |> do_term (depth + 1) Ts, ts)
1510 if is_constr thy x then
1512 else if is_stale_constr thy x then
1513 raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
1515 else if is_record_get thy x then
1517 0 => (do_term depth Ts (eta_expand Ts t 1), [])
1518 | _ => (optimized_record_get ext_ctxt s (domain_type T)
1519 (range_type T) (hd ts), tl ts)
1520 else if is_record_update thy x then
1522 2 => (optimized_record_update ext_ctxt
1523 (unsuffix Record.updateN s) (nth_range_type 2 T)
1524 (do_term depth Ts (hd ts))
1525 (do_term depth Ts (nth ts 1)), [])
1526 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
1527 else if is_rep_fun thy x then
1528 let val x' = mate_of_rep_fun thy x in
1529 if is_constr thy x' then
1530 select_nth_constr_arg_with_args depth Ts x' ts 0
1535 else if is_equational_fun ext_ctxt x then
1537 else case def_of_const thy def_table x of
1539 if depth > unfold_max_depth then
1540 raise LIMIT ("Nitpick_HOL.unfold_defs_in_term",
1541 "too many nested definitions (" ^
1542 string_of_int depth ^ ") while expanding " ^
1544 else if s = @{const_name wfrec'} then
1545 (do_term (depth + 1) Ts (betapplys (def, ts)), [])
1547 (do_term (depth + 1) Ts def, ts)
1548 | NONE => (Const x, ts)
1549 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
1552 (* extended_context -> typ -> term list *)
1553 fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
1555 val xs = datatype_constrs ext_ctxt T
1556 val set_T = T --> bool_T
1557 val iter_T = @{typ bisim_iterator}
1558 val bisim_const = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
1559 val bisim_max = @{const bisim_iterator_max}
1560 val n_var = Var (("n", 0), iter_T)
1562 Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T)
1563 $ Abs ("m", iter_T, HOLogic.eq_const iter_T
1564 $ (suc_const iter_T $ Bound 0) $ n_var)
1565 val x_var = Var (("x", 0), T)
1566 val y_var = Var (("y", 0), T)
1567 (* styp -> int -> typ -> term *)
1568 fun nth_sub_bisim x n nth_T =
1569 (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
1570 else HOLogic.eq_const nth_T)
1571 $ select_nth_constr_arg thy x x_var n nth_T
1572 $ select_nth_constr_arg thy x y_var n nth_T
1574 fun case_func (x as (_, T)) =
1576 val arg_Ts = binder_types T
1578 discriminate_value ext_ctxt x y_var ::
1579 map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
1581 in List.foldr absdummy core_t arg_Ts end
1583 [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
1584 $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
1585 $ (betapplys (optimized_case_def ext_ctxt T bool_T,
1586 map case_func xs @ [x_var]))),
1587 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
1588 $ (Const (@{const_name insert}, [T, set_T] ---> set_T)
1589 $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
1590 |> map HOLogic.mk_Trueprop
1593 exception NO_TRIPLE of unit
1595 (* theory -> styp -> term -> term list * term list * term *)
1596 fun triple_for_intro_rule thy x t =
1598 val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
1599 val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
1600 val (main, side) = List.partition (exists_Const (equal x)) prems
1602 val is_good_head = equal (Const x) o head_of
1604 if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
1608 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
1610 (* indexname * typ -> term list -> term -> term -> term *)
1611 fun wf_constraint_for rel side concl main =
1613 val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
1614 tuple_for_args concl), Var rel)
1615 val t = List.foldl HOLogic.mk_imp core side
1616 val vars = filter (not_equal rel) (Term.add_vars t [])
1618 Library.foldl (fn (t', ((x, j), T)) =>
1620 $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
1624 (* indexname * typ -> term list * term list * term -> term *)
1625 fun wf_constraint_for_triple rel (side, main, concl) =
1626 map (wf_constraint_for rel side concl) main |> foldr1 s_conj
1628 (* Proof.context -> Time.time option -> thm
1629 -> (Proof.context -> tactic -> tactic) -> bool *)
1630 fun terminates_by ctxt timeout goal tac =
1631 can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
1632 #> SINGLE (DETERM_TIMEOUT timeout
1633 (tac ctxt (auto_tac (clasimpset_of ctxt))))
1634 #> the #> Goal.finish ctxt) goal
1636 val max_cached_wfs = 100
1637 val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
1638 val cached_wf_props : (term * bool) list Unsynchronized.ref =
1639 Unsynchronized.ref []
1641 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
1642 ScnpReconstruct.sizechange_tac]
1644 (* extended_context -> const_table -> styp -> bool *)
1645 fun uncached_is_well_founded_inductive_pred
1646 ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
1647 : extended_context) (x as (_, T)) =
1648 case def_props_for_const thy fast_descrs intro_table x of
1649 [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
1652 (case map (triple_for_intro_rule thy x) intro_ts
1653 |> filter_out (null o #2) of
1657 val binders_T = HOLogic.mk_tupleT (binder_types T)
1658 val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
1659 val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
1660 val rel = (("R", j), rel_T)
1661 val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
1662 map (wf_constraint_for_triple rel) triples
1663 |> foldr1 s_conj |> HOLogic.mk_Trueprop
1664 val _ = if debug then
1665 priority ("Wellfoundedness goal: " ^
1666 Syntax.string_of_term ctxt prop ^ ".")
1670 if tac_timeout = (!cached_timeout)
1671 andalso length (!cached_wf_props) < max_cached_wfs then
1674 (cached_wf_props := []; cached_timeout := tac_timeout);
1675 case AList.lookup (op =) (!cached_wf_props) prop of
1679 val goal = prop |> cterm_of thy |> Goal.init
1680 val wf = exists (terminates_by ctxt tac_timeout goal)
1682 in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
1684 handle List.Empty => false
1685 | NO_TRIPLE () => false
1687 (* The type constraint below is a workaround for a Poly/ML bug. *)
1689 (* extended_context -> styp -> bool *)
1690 fun is_well_founded_inductive_pred
1691 (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context)
1693 case triple_lookup (const_match thy) wfs x of
1695 | _ => s mem [@{const_name Nats}, @{const_name fold_graph'}]
1696 orelse case AList.lookup (op =) (!wf_cache) x of
1700 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
1701 val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
1703 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
1706 (* typ list -> typ -> typ -> term -> term *)
1707 fun ap_curry [_] _ _ t = t
1708 | ap_curry arg_Ts tuple_T body_T t =
1709 let val n = length arg_Ts in
1710 list_abs (map (pair "c") arg_Ts,
1712 $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
1715 (* int -> term -> int *)
1716 fun num_occs_of_bound_in_term j (t1 $ t2) =
1717 op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
1718 | num_occs_of_bound_in_term j (Abs (s, T, t')) =
1719 num_occs_of_bound_in_term (j + 1) t'
1720 | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
1721 | num_occs_of_bound_in_term _ _ = 0
1724 val is_linear_inductive_pred_def =
1726 (* int -> term -> bool *)
1727 fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
1728 do_disjunct (j + 1) t2
1730 case num_occs_of_bound_in_term j t of
1732 | 1 => exists (equal (Bound j) o head_of) (conjuncts t)
1735 fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
1736 let val (xs, body) = strip_abs t2 in
1739 | n => forall (do_disjunct (n - 1)) (disjuncts body)
1741 | do_lfp_def _ = false
1742 in do_lfp_def o strip_abs_body end
1744 (* int -> int list list *)
1745 fun n_ptuple_paths 0 = []
1746 | n_ptuple_paths 1 = []
1747 | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
1748 (* int -> typ -> typ -> term -> term *)
1749 val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
1751 (* term -> term * term *)
1752 val linear_pred_base_and_step_rhss =
1755 fun aux (Const (@{const_name lfp}, _) $ t2) =
1757 val (xs, body) = strip_abs t2
1758 val arg_Ts = map snd (tl xs)
1759 val tuple_T = HOLogic.mk_tupleT arg_Ts
1760 val j = length arg_Ts
1761 (* int -> term -> term *)
1762 fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
1763 Const (@{const_name Ex}, T1)
1764 $ Abs (s2, T2, repair_rec (j + 1) t2')
1765 | repair_rec j (@{const "op &"} $ t1 $ t2) =
1766 @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
1768 let val (head, args) = strip_comb t in
1769 if head = Bound j then
1770 HOLogic.eq_const tuple_T $ Bound j
1771 $ mk_flat_tuple tuple_T args
1775 val (nonrecs, recs) =
1776 List.partition (equal 0 o num_occs_of_bound_in_term j)
1778 val base_body = nonrecs |> List.foldl s_disj @{const False}
1779 val step_body = recs |> map (repair_rec j)
1780 |> List.foldl s_disj @{const False}
1782 (list_abs (tl xs, incr_bv (~1, j, base_body))
1783 |> ap_n_split (length arg_Ts) tuple_T bool_T,
1784 Abs ("y", tuple_T, list_abs (tl xs, step_body)
1785 |> ap_n_split (length arg_Ts) tuple_T bool_T))
1788 raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
1791 (* extended_context -> styp -> term -> term *)
1792 fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T))
1795 val j = maxidx_of_term def + 1
1796 val (outer, fp_app) = strip_abs def
1797 val outer_bounds = map Bound (length outer - 1 downto 0)
1798 val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer
1799 val fp_app = subst_bounds (rev outer_vars, fp_app)
1800 val (outer_Ts, rest_T) = strip_n_binders (length outer) T
1801 val tuple_arg_Ts = strip_type rest_T |> fst
1802 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
1803 val set_T = tuple_T --> bool_T
1804 val curried_T = tuple_T --> set_T
1805 val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
1806 val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
1807 val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
1808 val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
1809 |> HOLogic.mk_Trueprop
1810 val _ = add_simps simp_table base_s [base_eq]
1811 val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T)
1812 val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs)
1813 |> HOLogic.mk_Trueprop
1814 val _ = add_simps simp_table step_s [step_eq]
1817 Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
1818 $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
1819 $ (Const (@{const_name split}, curried_T --> uncurried_T)
1820 $ list_comb (Const step_x, outer_bounds)))
1821 $ list_comb (Const base_x, outer_bounds)
1822 |> ap_curry tuple_arg_Ts tuple_T bool_T)
1823 |> unfold_defs_in_term ext_ctxt
1826 (* extended_context -> bool -> styp -> term *)
1827 fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds,
1828 def_table, simp_table, ...})
1831 val iter_T = iterator_type_for_const gfp x
1832 val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
1833 val unrolled_const = Const x' $ zero_const iter_T
1834 val def = the (def_of_const thy def_table x)
1836 if is_equational_fun ext_ctxt x' then
1837 unrolled_const (* already done *)
1838 else if not gfp andalso is_linear_inductive_pred_def def
1839 andalso star_linear_preds then
1840 starred_linear_pred_const ext_ctxt x def
1843 val j = maxidx_of_term def + 1
1844 val (outer, fp_app) = strip_abs def
1845 val outer_bounds = map Bound (length outer - 1 downto 0)
1846 val cur = Var ((iter_var_prefix, j + 1), iter_T)
1847 val next = suc_const iter_T $ cur
1848 val rhs = case fp_app of
1850 betapply (t, list_comb (Const x', next :: outer_bounds))
1851 | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
1853 val (inner, naked_rhs) = strip_abs rhs
1854 val all = outer @ inner
1855 val bounds = map Bound (length all - 1 downto 0)
1856 val vars = map (fn (s, T) => Var ((s, j), T)) all
1857 val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs)
1858 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
1859 val _ = add_simps simp_table s' [eq]
1860 in unrolled_const end
1863 (* extended_context -> styp -> term *)
1864 fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x =
1866 val def = the (def_of_const thy def_table x)
1867 val (outer, fp_app) = strip_abs def
1868 val outer_bounds = map Bound (length outer - 1 downto 0)
1869 val rhs = case fp_app of
1870 Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
1871 | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
1873 val (inner, naked_rhs) = strip_abs rhs
1874 val all = outer @ inner
1875 val bounds = map Bound (length all - 1 downto 0)
1876 val j = maxidx_of_term def + 1
1877 val vars = map (fn (s, T) => Var ((s, j), T)) all
1879 HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
1880 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
1882 fun inductive_pred_axiom ext_ctxt (x as (s, T)) =
1883 if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
1884 let val x' = (after_name_sep s, T) in
1885 raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)]
1888 raw_inductive_pred_axiom ext_ctxt x
1890 (* extended_context -> styp -> term list *)
1891 fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
1892 psimp_table, ...}) (x as (s, _)) =
1893 case def_props_for_const thy fast_descrs (!simp_table) x of
1894 [] => (case def_props_for_const thy fast_descrs psimp_table x of
1895 [] => [inductive_pred_axiom ext_ctxt x]
1899 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
1901 (* term list -> term list *)
1902 fun merge_type_vars_in_terms ts =
1904 (* typ -> (sort * string) list -> (sort * string) list *)
1905 fun add_type (TFree (s, S)) table =
1906 (case AList.lookup (op =) table S of
1908 if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
1910 | NONE => (S, s) :: table)
1911 | add_type _ table = table
1912 val table = fold (fold_types (fold_atyps add_type)) ts []
1914 fun coalesce (TFree (s, S)) = TFree (AList.lookup (op =) table S |> the, S)
1916 in map (map_types (map_atyps coalesce)) ts end
1918 (* extended_context -> typ -> typ list -> typ list *)
1919 fun add_ground_types ext_ctxt T accum =
1921 Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum
1922 | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
1923 | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
1925 if T mem @{typ prop} :: @{typ bool} :: @{typ unit} :: accum then
1929 |> fold (add_ground_types ext_ctxt)
1930 (case boxed_datatype_constrs ext_ctxt T of
1933 | _ => insert (op =) T accum
1934 (* extended_context -> typ -> typ list *)
1935 fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T []
1936 (* extended_context -> term list -> typ list *)
1937 fun ground_types_in_terms ext_ctxt ts =
1938 fold (fold_types (add_ground_types ext_ctxt)) ts []
1940 (* typ list -> int -> term -> bool *)
1941 fun has_heavy_bounds_or_vars Ts level t =
1943 (* typ list -> bool *)
1945 | aux [T] = is_fun_type T orelse is_pair_type T
1947 in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
1949 (* typ list -> int -> int -> int -> term -> term *)
1950 fun fresh_value_var Ts k n j t =
1951 Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
1953 (* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
1954 -> term * term list *)
1955 fun pull_out_constr_comb thy Ts relax k level t args seen =
1956 let val t_comb = list_comb (t, args) in
1959 if not relax andalso is_constr thy x
1960 andalso not (is_fun_type (fastype_of1 (Ts, t_comb)))
1961 andalso has_heavy_bounds_or_vars Ts level t_comb
1962 andalso not (loose_bvar (t_comb, level)) then
1964 val (j, seen) = case find_index (equal t_comb) seen of
1965 ~1 => (0, t_comb :: seen)
1967 in (fresh_value_var Ts k (length seen) j t_comb, seen) end
1970 | _ => (t_comb, seen)
1973 (* (term -> term) -> typ list -> int -> term list -> term list *)
1974 fun equations_for_pulled_out_constrs mk_eq Ts k seen =
1975 let val n = length seen in
1976 map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
1977 (index_seq 0 n) seen
1980 (* theory -> bool -> term -> term *)
1981 fun pull_out_universal_constrs thy def t =
1983 val k = maxidx_of_term t + 1
1984 (* typ list -> bool -> term -> term list -> term list -> term * term list *)
1985 fun do_term Ts def t args seen =
1987 (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
1988 do_eq_or_imp Ts def t0 t1 t2 seen
1989 | (t0 as @{const "==>"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
1990 | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
1991 do_eq_or_imp Ts def t0 t1 t2 seen
1992 | (t0 as @{const "op -->"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
1994 let val (t', seen) = do_term (T :: Ts) def t' [] seen in
1995 (list_comb (Abs (s, T, t'), args), seen)
1998 let val (t2, seen) = do_term Ts def t2 [] seen in
1999 do_term Ts def t1 (t2 :: args) seen
2001 | _ => pull_out_constr_comb thy Ts def k 0 t args seen
2002 (* typ list -> bool -> term -> term -> term -> term list
2003 -> term * term list *)
2004 and do_eq_or_imp Ts def t0 t1 t2 seen =
2006 val (t2, seen) = do_term Ts def t2 [] seen
2007 val (t1, seen) = do_term Ts false t1 [] seen
2008 in (t0 $ t1 $ t2, seen) end
2009 val (concl, seen) = do_term [] def t [] []
2011 Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
2015 (* extended_context -> bool -> term -> term *)
2016 fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
2019 val num_occs_of_var =
2020 fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
2022 (* bool -> term -> term *)
2023 fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
2024 aux_eq careful true t0 t1 t2
2025 | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
2026 t0 $ aux false t1 $ aux careful t2
2027 | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
2028 aux_eq careful true t0 t1 t2
2029 | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
2030 t0 $ aux false t1 $ aux careful t2
2031 | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
2032 | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
2034 (* bool -> bool -> term -> term -> term -> term *)
2035 and aux_eq careful pass1 t0 t1 t2 =
2038 else if axiom andalso is_Var t2
2039 andalso num_occs_of_var (dest_Var t2) = 1 then
2041 else case strip_comb t2 of
2042 (Const (x as (s, T)), args) =>
2043 let val arg_Ts = binder_types T in
2044 if length arg_Ts = length args
2045 andalso (is_constr thy x orelse s mem [@{const_name Pair}]
2046 orelse x = dest_Const @{const Suc})
2047 andalso (not careful orelse not (is_Var t1)
2048 orelse String.isPrefix val_var_prefix
2049 (fst (fst (dest_Var t1)))) then
2050 discriminate_value ext_ctxt x t1 ::
2051 map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
2053 |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
2057 | _ => raise SAME ())
2058 handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
2059 else t0 $ aux false t2 $ aux false t1
2060 (* styp -> term -> int -> typ -> term -> term *)
2061 and sel_eq x t n nth_T nth_t =
2062 HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
2066 (* theory -> term -> term *)
2067 fun simplify_constrs_and_sels thy t =
2069 (* term -> int -> term *)
2070 fun is_nth_sel_on t' n (Const (s, _) $ t) =
2071 (t = t' andalso is_sel_like_and_no_discr s
2072 andalso sel_no_from_name s = n)
2073 | is_nth_sel_on _ _ _ = false
2074 (* term -> term list -> term *)
2075 fun do_term (Const (@{const_name Rep_Frac}, _)
2076 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
2077 | do_term (Const (@{const_name Abs_Frac}, _)
2078 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
2079 | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
2080 | do_term (t as Const (x as (s, T))) (args as _ :: _) =
2081 ((if is_constr_like thy x then
2082 if length args = num_binder_types T then
2084 Const (x' as (_, T')) $ t' =>
2085 if domain_type T' = body_type T
2086 andalso forall (uncurry (is_nth_sel_on t'))
2087 (index_seq 0 (length args) ~~ args) then
2091 | _ => raise SAME ()
2094 else if is_sel_like_and_no_discr s then
2095 case strip_comb (hd args) of
2096 (Const (x' as (s', T')), ts') =>
2097 if is_constr_like thy x'
2098 andalso constr_name_for_sel_like s = s'
2099 andalso not (exists is_pair_type (binder_types T')) then
2100 list_comb (nth ts' (sel_no_from_name s), tl args)
2103 | _ => raise SAME ()
2106 handle SAME () => betapplys (t, args))
2107 | do_term (Abs (s, T, t')) args =
2108 betapplys (Abs (s, T, do_term t' []), args)
2109 | do_term t args = betapplys (t, args)
2113 fun curry_assms (@{const "==>"} $ (@{const Trueprop}
2114 $ (@{const "op &"} $ t1 $ t2)) $ t3) =
2115 curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
2116 | curry_assms (@{const "==>"} $ t1 $ t2) =
2117 @{const "==>"} $ curry_assms t1 $ curry_assms t2
2121 val destroy_universal_equalities =
2123 (* term list -> (indexname * typ) list -> term -> term *)
2124 fun aux prems zs t =
2126 @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
2127 | _ => Logic.list_implies (rev prems, t)
2128 (* term list -> (indexname * typ) list -> term -> term -> term *)
2129 and aux_implies prems zs t1 t2 =
2131 Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
2132 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
2133 aux_eq prems zs z t' t1 t2
2134 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
2135 aux_eq prems zs z t' t1 t2
2136 | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
2137 (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
2139 and aux_eq prems zs z t' t1 t2 =
2140 if not (z mem zs) andalso not (exists_subterm (equal (Var z)) t') then
2141 aux prems zs (subst_free [(Var z, t')] t2)
2143 aux (t1 :: prems) (Term.add_vars t1 zs) t2
2146 (* theory -> term -> term *)
2147 fun pull_out_existential_constrs thy t =
2149 val k = maxidx_of_term t + 1
2150 (* typ list -> int -> term -> term list -> term list -> term * term list *)
2151 fun aux Ts num_exists t args seen =
2153 (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
2155 val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
2156 val n = length seen'
2157 (* unit -> term list *)
2158 fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
2160 (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
2161 |> List.foldl s_conj t1 |> fold mk_exists (vars ())
2162 |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
2165 let val (t2, seen) = aux Ts num_exists t2 [] seen in
2166 aux Ts num_exists t1 (t2 :: args) seen
2170 val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
2171 in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
2173 if num_exists > 0 then
2174 pull_out_constr_comb thy Ts false k num_exists t args seen
2176 (list_comb (t, args), seen)
2177 in aux [] 0 t [] [] |> fst end
2179 (* theory -> int -> term list -> term list -> (term * term list) option *)
2180 fun find_bound_assign _ _ _ [] = NONE
2181 | find_bound_assign thy j seen (t :: ts) =
2183 (* bool -> term -> term -> (term * term list) option *)
2184 fun aux pass1 t1 t2 =
2185 (if loose_bvar1 (t2, j) then
2186 if pass1 then aux false t2 t1 else raise SAME ()
2188 Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
2189 | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
2190 if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then
2191 SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
2195 | _ => raise SAME ())
2196 handle SAME () => find_bound_assign thy j (t :: seen) ts
2199 Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
2200 | _ => find_bound_assign thy j (t :: seen) ts
2203 (* int -> term -> term -> term *)
2204 fun subst_one_bound j arg t =
2206 fun aux (Bound i, lev) =
2207 if i < lev then raise SAME ()
2208 else if i = lev then incr_boundvars (lev - j) arg
2210 | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
2211 | aux (f $ t, lev) =
2212 (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
2213 handle SAME () => f $ aux (t, lev))
2214 | aux _ = raise SAME ()
2215 in aux (t, j) handle SAME () => t end
2217 (* theory -> term -> term *)
2218 fun destroy_existential_equalities thy =
2220 (* string list -> typ list -> term list -> term *)
2221 fun kill [] [] ts = foldr1 s_conj ts
2222 | kill (s :: ss) (T :: Ts) ts =
2223 (case find_bound_assign thy (length ss) [] ts of
2224 SOME (_, []) => @{const True}
2225 | SOME (arg_t, ts) =>
2226 kill ss Ts (map (subst_one_bound (length ss)
2227 (incr_bv (~1, length ss + 1, arg_t))) ts)
2229 Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
2230 $ Abs (s, T, kill ss Ts ts))
2231 | kill _ _ _ = raise UnequalLengths
2232 (* string list -> typ list -> term -> term *)
2233 fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
2234 gather (ss @ [s1]) (Ts @ [T1]) t1
2235 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
2236 | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
2237 | gather [] [] t = t
2238 | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t))
2242 fun distribute_quantifiers t =
2244 (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
2246 (t10 as @{const "op &"}) $ t11 $ t12 =>
2247 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
2248 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
2249 | (t10 as @{const Not}) $ t11 =>
2250 t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
2253 if not (loose_bvar1 (t1, 0)) then
2254 distribute_quantifiers (incr_boundvars ~1 t1)
2256 t0 $ Abs (s, T1, distribute_quantifiers t1))
2257 | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
2258 (case distribute_quantifiers t1 of
2259 (t10 as @{const "op |"}) $ t11 $ t12 =>
2260 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
2261 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
2262 | (t10 as @{const "op -->"}) $ t11 $ t12 =>
2263 t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
2265 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
2266 | (t10 as @{const Not}) $ t11 =>
2267 t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
2270 if not (loose_bvar1 (t1, 0)) then
2271 distribute_quantifiers (incr_boundvars ~1 t1)
2273 t0 $ Abs (s, T1, distribute_quantifiers t1))
2274 | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
2275 | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
2278 (* int -> int -> (int -> int) -> term -> term *)
2279 fun renumber_bounds j n f t =
2281 t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
2282 | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
2284 Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
2287 val quantifier_cluster_max_size = 8
2289 (* theory -> term -> term *)
2290 fun push_quantifiers_inward thy =
2292 (* string -> string list -> typ list -> term -> term *)
2293 fun aux quant_s ss Ts t =
2295 (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
2296 if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
2297 aux s0 (s1 :: ss) (T1 :: Ts) t1
2298 else if quant_s = ""
2299 andalso s0 mem [@{const_name All}, @{const_name Ex}] then
2303 | _ => raise SAME ())
2307 if quant_s = "" then
2308 aux "" [] [] t1 $ aux "" [] [] t2
2311 val typical_card = 4
2312 (* ('a -> ''b list) -> 'a list -> ''b list *)
2313 fun big_union proj ps =
2314 fold (fold (insert (op =)) o proj) ps []
2315 val (ts, connective) = strip_any_connective t
2317 map (bounded_card_of_type 65536 typical_card []) Ts
2318 val t_costs = map size_of_term ts
2319 val num_Ts = length Ts
2321 val flip = curry (op -) (num_Ts - 1)
2322 val t_boundss = map (map flip o loose_bnos) ts
2323 (* (int list * int) list -> int list -> int *)
2324 fun cost boundss_cum_costs [] =
2325 map snd boundss_cum_costs |> Integer.sum
2326 | cost boundss_cum_costs (j :: js) =
2329 List.partition (fn (bounds, _) => j mem bounds)
2331 val yeas_bounds = big_union fst yeas
2332 val yeas_cost = Integer.sum (map snd yeas)
2334 in cost ((yeas_bounds, yeas_cost) :: nays) js end
2335 val js = all_permutations (index_seq 0 num_Ts)
2336 |> map (`(cost (t_boundss ~~ t_costs)))
2337 |> sort (int_ord o pairself fst) |> hd |> snd
2338 val back_js = map (fn j => find_index (equal j) js)
2339 (index_seq 0 num_Ts)
2340 val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
2342 (* (term * int list) list -> term *)
2343 fun mk_connection [] =
2344 raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
2345 \mk_connection", "")
2346 | mk_connection ts_cum_bounds =
2347 ts_cum_bounds |> map fst
2348 |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
2349 (* (term * int list) list -> int list -> term *)
2350 fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
2351 | build ts_cum_bounds (j :: js) =
2354 List.partition (fn (_, bounds) => j mem bounds)
2356 ||> map (apfst (incr_boundvars ~1))
2361 let val T = nth Ts (flip j) in
2362 build ((Const (quant_s, (T --> bool_T) --> bool_T)
2363 $ Abs (nth ss (flip j), T,
2364 mk_connection yeas),
2365 big_union snd yeas) :: nays) js
2368 in build (ts ~~ t_boundss) js end
2369 | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
2373 (* polarity -> string -> bool *)
2374 fun is_positive_existential polar quant_s =
2375 (polar = Pos andalso quant_s = @{const_name Ex})
2376 orelse (polar = Neg andalso quant_s <> @{const_name Ex})
2378 (* extended_context -> int -> term -> term *)
2379 fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
2382 (* int list -> int list *)
2383 val incrs = map (Integer.add 1)
2384 (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
2385 fun aux ss Ts js depth polar t =
2387 (* string -> typ -> string -> typ -> term -> term *)
2388 fun do_quantifier quant_s quant_T abs_s abs_T t =
2389 if not (loose_bvar1 (t, 0)) then
2390 aux ss Ts js depth polar (incr_boundvars ~1 t)
2391 else if depth <= skolem_depth
2392 andalso is_positive_existential polar quant_s then
2394 val j = length (!skolems) + 1
2395 val sko_s = skolem_prefix_for (length js) j ^ abs_s
2396 val _ = Unsynchronized.change skolems (cons (sko_s, ss))
2397 val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
2399 val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
2401 if null js then betapply (abs_t, sko_t)
2402 else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
2405 Const (quant_s, quant_T)
2406 $ Abs (abs_s, abs_T,
2407 if is_higher_order_type abs_T then
2410 aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
2411 (depth + 1) polar t)
2414 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
2415 do_quantifier s0 T0 s1 T1 t1
2416 | @{const "==>"} $ t1 $ t2 =>
2417 @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
2418 $ aux ss Ts js depth polar t2
2419 | @{const Pure.conjunction} $ t1 $ t2 =>
2420 @{const Pure.conjunction} $ aux ss Ts js depth polar t1
2421 $ aux ss Ts js depth polar t2
2422 | @{const Trueprop} $ t1 =>
2423 @{const Trueprop} $ aux ss Ts js depth polar t1
2424 | @{const Not} $ t1 =>
2425 @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
2426 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
2427 do_quantifier s0 T0 s1 T1 t1
2428 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
2429 do_quantifier s0 T0 s1 T1 t1
2430 | @{const "op &"} $ t1 $ t2 =>
2431 @{const "op &"} $ aux ss Ts js depth polar t1
2432 $ aux ss Ts js depth polar t2
2433 | @{const "op |"} $ t1 $ t2 =>
2434 @{const "op |"} $ aux ss Ts js depth polar t1
2435 $ aux ss Ts js depth polar t2
2436 | @{const "op -->"} $ t1 $ t2 =>
2437 @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
2438 $ aux ss Ts js depth polar t2
2439 | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
2440 t0 $ t1 $ aux ss Ts js depth polar t2
2441 | Const (x as (s, T)) =>
2442 if is_inductive_pred ext_ctxt x
2443 andalso not (is_well_founded_inductive_pred ext_ctxt x) then
2445 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
2446 val (pref, connective, set_oper) =
2450 @{const_name upper_semilattice_fun_inst.sup_fun})
2454 @{const_name lower_semilattice_fun_inst.inf_fun})
2456 fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x
2457 |> aux ss Ts js depth polar
2458 fun neg () = Const (pref ^ s, T)
2460 (case polar |> gfp ? flip_polarity of
2464 if is_fun_type T then
2466 val ((trunk_arg_Ts, rump_arg_T), body_T) =
2467 T |> strip_type |>> split_last
2468 val set_T = rump_arg_T --> body_T
2469 (* (unit -> term) -> term *)
2472 map Bound (length trunk_arg_Ts - 1 downto 0))
2475 (Const (set_oper, [set_T, set_T] ---> set_T)
2476 $ app pos $ app neg) trunk_arg_Ts
2479 connective $ pos () $ neg ())
2484 betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
2485 aux ss Ts [] depth Neut t2)
2486 | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
2489 in aux [] [] [] 0 Pos end
2491 (* extended_context -> styp -> (int * term option) list *)
2492 fun static_args_in_term ({ersatz_table, ...} : extended_context) x t =
2494 (* term -> term list -> term list -> term list list *)
2495 fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
2496 | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
2497 | fun_calls t args =
2499 Const (x' as (s', T')) =>
2500 x = x' orelse (case AList.lookup (op =) ersatz_table s' of
2501 SOME s'' => x = (s'', T')
2503 | _ => false) ? cons args
2504 (* term list list -> term list list -> term list -> term list list *)
2505 fun call_sets [] [] vs = [vs]
2506 | call_sets [] uss vs = vs :: call_sets uss [] []
2507 | call_sets ([] :: _) _ _ = []
2508 | call_sets ((t :: ts) :: tss) uss vs =
2509 OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
2510 val sets = call_sets (fun_calls t [] []) [] []
2511 val indexed_sets = sets ~~ (index_seq 0 (length sets))
2513 fold_rev (fn (set, j) =>
2515 [Var _] => AList.lookup (op =) indexed_sets set = SOME j
2517 | [t as Const _] => cons (j, SOME t)
2518 | [t as Free _] => cons (j, SOME t)
2519 | _ => I) indexed_sets []
2521 (* extended_context -> styp -> term list -> (int * term option) list *)
2522 fun static_args_in_terms ext_ctxt x =
2523 map (static_args_in_term ext_ctxt x)
2524 #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
2526 (* term -> term list *)
2527 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
2528 | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
2529 | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
2531 | params_in_equation _ = []
2533 (* styp -> styp -> int list -> term list -> term list -> term -> term *)
2534 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
2536 val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
2538 val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
2539 val fixed_params = filter_indices fixed_js (params_in_equation t)
2540 (* term list -> term -> term *)
2541 fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
2542 | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
2545 list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
2547 let val j = find_index (equal t) fixed_params in
2548 list_comb (if j >= 0 then nth fixed_args j else t, args)
2552 (* typ list -> term -> bool *)
2553 fun is_eligible_arg Ts t =
2554 let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
2556 orelse (is_higher_order_type (fastype_of1 (Ts, t))
2557 andalso forall (not o is_higher_order_type) bad_Ts)
2560 (* (int * term option) list -> (int * term) list -> int list *)
2561 fun overlapping_indices [] _ = []
2562 | overlapping_indices _ [] = []
2563 | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
2564 if j1 < j2 then overlapping_indices ps1' ps2
2565 else if j1 > j2 then overlapping_indices ps1 ps2'
2566 else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
2568 val special_depth = 20
2570 (* extended_context -> int -> term -> term *)
2571 fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table,
2572 special_funs, ...}) depth t =
2573 if not specialize orelse depth > special_depth then
2577 val blacklist = if depth = 0 then []
2578 else case term_under_def t of Const x => [x] | _ => []
2579 (* term list -> typ list -> term -> term *)
2580 fun aux args Ts (Const (x as (s, T))) =
2581 ((if not (x mem blacklist) andalso not (null args)
2582 andalso not (String.isPrefix special_prefix s)
2583 andalso is_equational_fun ext_ctxt x then
2585 val eligible_args = filter (is_eligible_arg Ts o snd)
2586 (index_seq 0 (length args) ~~ args)
2587 val _ = not (null eligible_args) orelse raise SAME ()
2588 val old_axs = equational_fun_axioms ext_ctxt x
2589 |> map (destroy_existential_equalities thy)
2590 val static_params = static_args_in_terms ext_ctxt x old_axs
2591 val fixed_js = overlapping_indices static_params eligible_args
2592 val _ = not (null fixed_js) orelse raise SAME ()
2593 val fixed_args = filter_indices fixed_js args
2594 val vars = fold Term.add_vars fixed_args []
2595 |> sort (TermOrd.fast_indexname_ord o pairself fst)
2596 val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
2599 val live_args = filter_out_indices fixed_js args
2600 val extra_args = map Var vars @ map Bound bound_js @ live_args
2601 val extra_Ts = map snd vars @ filter_indices bound_js Ts
2602 val k = maxidx_of_term t + 1
2604 fun var_for_bound_no j =
2605 Var ((bound_var_prefix ^
2606 nat_subscript (find_index (equal j) bound_js + 1), k),
2608 val fixed_args_in_axiom =
2609 map (curry subst_bounds
2610 (map var_for_bound_no (index_seq 0 (length Ts))))
2613 case AList.lookup (op =) (!special_funs)
2614 (x, fixed_js, fixed_args_in_axiom) of
2615 SOME x' => list_comb (Const x', extra_args)
2618 val extra_args_in_axiom =
2619 map Var vars @ map var_for_bound_no bound_js
2621 (special_prefix_for (length (!special_funs) + 1) ^ s,
2622 extra_Ts @ filter_out_indices fixed_js (binder_types T)
2625 map (specialize_fun_axiom x x' fixed_js
2626 fixed_args_in_axiom extra_args_in_axiom) old_axs
2628 Unsynchronized.change special_funs
2629 (cons ((x, fixed_js, fixed_args_in_axiom), x'))
2630 val _ = add_simps simp_table s' new_axs
2631 in list_comb (Const x', extra_args) end
2635 handle SAME () => list_comb (Const x, args))
2636 | aux args Ts (Abs (s, T, t)) =
2637 list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
2638 | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
2639 | aux args _ t = list_comb (t, args)
2642 (* theory -> term -> int Termtab.tab -> int Termtab.tab *)
2643 fun add_to_uncurry_table thy t =
2645 (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
2646 fun aux (t1 $ t2) args table =
2647 let val table = aux t2 [] table in aux t1 (t2 :: args) table end
2648 | aux (Abs (_, _, t')) _ table = aux t' [] table
2649 | aux (t as Const (x as (s, _))) args table =
2650 if is_built_in_const false x orelse is_constr_like thy x orelse is_sel s
2651 orelse s = @{const_name Sigma} then
2654 Termtab.map_default (t, 65536) (curry Int.min (length args)) table
2655 | aux _ _ table = table
2658 (* int Termtab.tab term -> term *)
2659 fun uncurry_term table t =
2661 (* term -> term list -> term *)
2662 fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
2663 | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
2664 | aux (t as Const (s, T)) args =
2665 (case Termtab.lookup table t of
2669 val (arg_Ts, rest_T) = strip_n_binders n T
2671 if hd arg_Ts = @{typ bisim_iterator}
2672 orelse is_fp_iterator_type (hd arg_Ts) then
2674 else case find_index (not_equal bool_T) arg_Ts of
2677 val ((before_args, tuple_args), after_args) =
2678 args |> chop n |>> chop j
2679 val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
2680 T |> strip_n_binders n |>> chop j
2681 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
2686 betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
2687 before_arg_Ts ---> tuple_T --> rest_T),
2688 before_args @ [mk_flat_tuple tuple_T tuple_args] @
2693 | NONE => betapplys (t, args))
2694 | aux t args = betapplys (t, args)
2697 (* (term -> term) -> int -> term -> term *)
2698 fun coerce_bound_no f j t =
2700 t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
2701 | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
2702 | Bound j' => if j' = j then f t else t
2705 (* extended_context -> bool -> term -> term *)
2706 fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t =
2709 fun box_relational_operator_type (Type ("fun", Ts)) =
2710 Type ("fun", map box_relational_operator_type Ts)
2711 | box_relational_operator_type (Type ("*", Ts)) =
2712 Type ("*", map (box_type ext_ctxt InPair) Ts)
2713 | box_relational_operator_type T = T
2714 (* typ -> typ -> term -> term *)
2715 fun coerce_bound_0_in_term new_T old_T =
2716 old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
2717 (* typ list -> typ -> term -> term *)
2718 and coerce_term Ts new_T old_T t =
2719 if old_T = new_T then
2722 case (new_T, old_T) of
2723 (Type (new_s, new_Ts as [new_T1, new_T2]),
2724 Type ("fun", [old_T1, old_T2])) =>
2725 (case eta_expand Ts t 1 of
2728 t' |> coerce_bound_0_in_term new_T1 old_T1
2729 |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
2730 |> Envir.eta_contract
2732 ? construct_value thy (@{const_name FunBox},
2733 Type ("fun", new_Ts) --> new_T) o single
2734 | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
2735 \coerce_term", [t']))
2736 | (Type (new_s, new_Ts as [new_T1, new_T2]),
2737 Type (old_s, old_Ts as [old_T1, old_T2])) =>
2738 if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
2739 case constr_expand ext_ctxt old_T t of
2740 Const (@{const_name FunBox}, _) $ t1 =>
2741 if new_s = "fun" then
2742 coerce_term Ts new_T (Type ("fun", old_Ts)) t1
2745 (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
2746 [coerce_term Ts (Type ("fun", new_Ts))
2747 (Type ("fun", old_Ts)) t1]
2748 | Const _ $ t1 $ t2 =>
2750 (if new_s = "*" then @{const_name Pair}
2751 else @{const_name PairBox}, new_Ts ---> new_T)
2752 [coerce_term Ts new_T1 old_T1 t1,
2753 coerce_term Ts new_T2 old_T2 t2]
2754 | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
2755 \coerce_term", [t'])
2757 raise TYPE ("coerce_term", [new_T, old_T], [t])
2758 | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
2759 (* indexname * typ -> typ * term -> typ option list -> typ option list *)
2760 fun add_boxed_types_for_var (z as (_, T)) (T', t') =
2762 Var z' => z' = z ? insert (op =) T'
2763 | Const (@{const_name Pair}, _) $ t1 $ t2 =>
2765 Type (_, [T1, T2]) =>
2766 fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
2767 | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
2768 \add_boxed_types_for_var", [T'], []))
2769 | _ => exists_subterm (equal (Var z)) t' ? insert (op =) T
2770 (* typ list -> typ list -> term -> indexname * typ -> typ *)
2771 fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
2773 @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
2774 | Const (s0, _) $ t1 $ _ =>
2775 if s0 mem [@{const_name "=="}, @{const_name "op ="}] then
2777 val (t', args) = strip_comb t1
2778 val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
2780 case fold (add_boxed_types_for_var z)
2781 (fst (strip_n_binders (length args) T') ~~ args) [] of
2788 (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
2790 and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
2793 if polar = Neut orelse is_positive_existential polar quant_s then
2794 box_type ext_ctxt InFunLHS abs_T
2797 val body_T = body_type quant_T
2799 Const (quant_s, (abs_T' --> body_T) --> body_T)
2800 $ Abs (abs_s, abs_T',
2801 t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
2803 (* typ list -> typ list -> string -> typ -> term -> term -> term *)
2804 and do_equals new_Ts old_Ts s0 T0 t1 t2 =
2806 val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
2807 val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
2808 val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
2810 list_comb (Const (s0, [T, T] ---> body_type T0),
2811 map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
2813 (* string -> typ -> term *)
2814 and do_description_operator s T =
2815 let val T1 = box_type ext_ctxt InFunLHS (range_type T) in
2816 Const (s, (T1 --> bool_T) --> T1)
2818 (* typ list -> typ list -> polarity -> term -> term *)
2819 and do_term new_Ts old_Ts polar t =
2821 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
2822 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
2823 | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
2824 do_equals new_Ts old_Ts s0 T0 t1 t2
2825 | @{const "==>"} $ t1 $ t2 =>
2826 @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
2827 $ do_term new_Ts old_Ts polar t2
2828 | @{const Pure.conjunction} $ t1 $ t2 =>
2829 @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
2830 $ do_term new_Ts old_Ts polar t2
2831 | @{const Trueprop} $ t1 =>
2832 @{const Trueprop} $ do_term new_Ts old_Ts polar t1
2833 | @{const Not} $ t1 =>
2834 @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
2835 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
2836 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
2837 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
2838 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
2839 | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
2840 do_equals new_Ts old_Ts s0 T0 t1 t2
2841 | @{const "op &"} $ t1 $ t2 =>
2842 @{const "op &"} $ do_term new_Ts old_Ts polar t1
2843 $ do_term new_Ts old_Ts polar t2
2844 | @{const "op |"} $ t1 $ t2 =>
2845 @{const "op |"} $ do_term new_Ts old_Ts polar t1
2846 $ do_term new_Ts old_Ts polar t2
2847 | @{const "op -->"} $ t1 $ t2 =>
2848 @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
2849 $ do_term new_Ts old_Ts polar t2
2850 | Const (s as @{const_name The}, T) => do_description_operator s T
2851 | Const (s as @{const_name Eps}, T) => do_description_operator s T
2852 | Const (s as @{const_name Tha}, T) => do_description_operator s T
2853 | Const (x as (s, T)) =>
2854 Const (s, if s mem [@{const_name converse}, @{const_name trancl}] then
2855 box_relational_operator_type T
2856 else if is_built_in_const fast_descrs x
2857 orelse s = @{const_name Sigma} then
2859 else if is_constr_like thy x then
2860 box_type ext_ctxt InConstr T
2861 else if is_sel s orelse is_rep_fun thy x then
2862 box_type ext_ctxt InSel T
2864 box_type ext_ctxt InExpr T)
2865 | t1 $ Abs (s, T, t2') =>
2867 val t1 = do_term new_Ts old_Ts Neut t1
2868 val T1 = fastype_of1 (new_Ts, t1)
2869 val (s1, Ts1) = dest_Type T1
2870 val T' = hd (snd (dest_Type (hd Ts1)))
2871 val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
2872 val T2 = fastype_of1 (new_Ts, t2)
2873 val t2 = coerce_term new_Ts (hd Ts1) T2 t2
2875 betapply (if s1 = "fun" then
2878 select_nth_constr_arg thy
2879 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
2880 (Type ("fun", Ts1)), t2)
2884 val t1 = do_term new_Ts old_Ts Neut t1
2885 val T1 = fastype_of1 (new_Ts, t1)
2886 val (s1, Ts1) = dest_Type T1
2887 val t2 = do_term new_Ts old_Ts Neut t2
2888 val T2 = fastype_of1 (new_Ts, t2)
2889 val t2 = coerce_term new_Ts (hd Ts1) T2 t2
2891 betapply (if s1 = "fun" then
2894 select_nth_constr_arg thy
2895 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
2896 (Type ("fun", Ts1)), t2)
2898 | Free (s, T) => Free (s, box_type ext_ctxt InExpr T)
2899 | Var (z as (x, T)) =>
2900 Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
2901 else box_type ext_ctxt InExpr T)
2904 Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
2905 in do_term [] [] Pos orig_t end
2907 (* int -> term -> term *)
2908 fun eval_axiom_for_term j t =
2909 Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
2911 (* extended_context -> styp -> bool *)
2912 fun is_equational_fun_surely_complete ext_ctxt x =
2913 case raw_equational_fun_axioms ext_ctxt x of
2914 [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
2915 strip_comb t1 |> snd |> forall is_Var
2918 type special = int list * term list * styp
2920 (* styp -> special -> special -> term *)
2921 fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
2923 val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
2924 val Ts = binder_types T
2925 val max_j = fold (fold Integer.max) [js1, js2] ~1
2926 val (eqs, (args1, args2)) =
2927 fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
2928 (js1 ~~ ts1, js2 ~~ ts2) of
2929 (SOME t1, SOME t2) => apfst (cons (t1, t2))
2930 | (SOME t1, NONE) => apsnd (apsnd (cons t1))
2931 | (NONE, SOME t2) => apsnd (apfst (cons t2))
2933 let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
2935 apsnd (pairself (cons v))
2936 end) (max_j downto 0) ([], ([], []))
2938 Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
2939 |> map Logic.mk_equals,
2940 Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
2941 list_comb (Const x2, bounds2 @ args2)))
2942 |> Refute.close_form
2945 (* extended_context -> styp list -> term list *)
2946 fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs =
2950 |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
2951 |> AList.group (op =)
2952 |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
2953 |> map (fn (x, zs) => (x, zs |> (x mem xs) ? cons ([], [], x)))
2954 (* special -> int *)
2955 fun generality (js, _, _) = ~(length js)
2956 (* special -> special -> bool *)
2957 fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
2958 x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
2959 (j2 ~~ t2, j1 ~~ t1)
2960 (* styp -> special list -> special list -> special list -> term list
2962 fun do_pass_1 _ [] [_] [_] = I
2963 | do_pass_1 x skipped _ [] = do_pass_2 x skipped
2964 | do_pass_1 x skipped all (z :: zs) =
2965 case filter (is_more_specific z) all
2966 |> sort (int_ord o pairself generality) of
2967 [] => do_pass_1 x (z :: skipped) all zs
2968 | (z' :: _) => cons (special_congruence_axiom x z z')
2969 #> do_pass_1 x skipped all zs
2970 (* styp -> special list -> term list -> term list *)
2971 and do_pass_2 _ [] = I
2972 | do_pass_2 x (z :: zs) =
2973 fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
2974 in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
2977 val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
2979 (* 'a Symtab.table -> 'a list *)
2980 fun all_table_entries table = Symtab.fold (append o snd) table []
2981 (* const_table -> string -> const_table *)
2982 fun extra_table table s = Symtab.make [(s, all_table_entries table)]
2984 (* extended_context -> term -> (term list * term list) * (bool * bool) *)
2986 (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
2987 def_table, nondef_table, user_nondefs, ...}) t =
2989 type accumulator = styp list * (term list * term list)
2990 (* (term list * term list -> term list)
2991 -> ((term list -> term list) -> term list * term list
2992 -> term list * term list)
2993 -> int -> term -> accumulator -> accumulator *)
2994 fun add_axiom get app depth t (accum as (xs, axs)) =
2996 val t = t |> unfold_defs_in_term ext_ctxt
2997 |> skolemize_term_and_more ext_ctxt ~1
2999 if is_trivial_equation t then
3002 let val t' = t |> specialize_consts_in_term ext_ctxt depth in
3003 if exists (member (op aconv) (get axs)) [t, t'] then accum
3004 else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
3007 (* int -> term -> accumulator -> accumulator *)
3008 and add_def_axiom depth = add_axiom fst apfst depth
3009 and add_nondef_axiom depth = add_axiom snd apsnd depth
3010 and add_maybe_def_axiom depth t =
3011 (if head_of t <> @{const "==>"} then add_def_axiom
3012 else add_nondef_axiom) depth t
3013 and add_eq_axiom depth t =
3014 (if is_constr_pattern_formula thy t then add_def_axiom
3015 else add_nondef_axiom) depth t
3016 (* int -> term -> accumulator -> accumulator *)
3017 and add_axioms_for_term depth t (accum as (xs, axs)) =
3019 t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
3020 | Const (x as (s, T)) =>
3021 (if x mem xs orelse is_built_in_const fast_descrs x then
3024 let val accum as (xs, _) = (x :: xs, axs) in
3025 if depth > axioms_max_depth then
3026 raise LIMIT ("Nitpick_HOL.axioms_for_term.add_axioms_for_term",
3027 "too many nested axioms (" ^ string_of_int depth ^
3029 else if Refute.is_const_of_class thy x then
3031 val class = Logic.class_of_const s
3032 val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
3034 val ax1 = try (Refute.specialize_type thy x) of_class
3035 val ax2 = Option.map (Refute.specialize_type thy x o snd)
3036 (Refute.get_classdef thy class)
3038 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
3041 else if is_constr thy x then
3043 else if is_equational_fun ext_ctxt x then
3044 fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
3046 else if is_abs_fun thy x then
3047 accum |> fold (add_nondef_axiom depth)
3048 (nondef_props_for_const thy false nondef_table x)
3049 |> is_funky_typedef thy (range_type T)
3050 ? fold (add_maybe_def_axiom depth)
3051 (nondef_props_for_const thy true
3052 (extra_table def_table s) x)
3053 else if is_rep_fun thy x then
3054 accum |> fold (add_nondef_axiom depth)
3055 (nondef_props_for_const thy false nondef_table x)
3056 |> is_funky_typedef thy (range_type T)
3057 ? fold (add_maybe_def_axiom depth)
3058 (nondef_props_for_const thy true
3059 (extra_table def_table s) x)
3060 |> add_axioms_for_term depth
3061 (Const (mate_of_rep_fun thy x))
3062 |> fold (add_def_axiom depth)
3063 (inverse_axioms_for_rep_fun thy x)
3065 accum |> user_axioms <> SOME false
3066 ? fold (add_nondef_axiom depth)
3067 (nondef_props_for_const thy false nondef_table x)
3069 |> add_axioms_for_type depth T
3070 | Free (_, T) => add_axioms_for_type depth T accum
3071 | Var (_, T) => add_axioms_for_type depth T accum
3073 | Abs (_, T, t) => accum |> add_axioms_for_term depth t
3074 |> add_axioms_for_type depth T
3075 (* int -> typ -> accumulator -> accumulator *)
3076 and add_axioms_for_type depth T =
3078 Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
3079 | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
3083 | TFree (_, S) => add_axioms_for_sort depth T S
3084 | TVar (_, S) => add_axioms_for_sort depth T S
3085 | Type (z as (_, Ts)) =>
3086 fold (add_axioms_for_type depth) Ts
3087 #> (if is_pure_typedef thy T then
3088 fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
3089 else if max_bisim_depth >= 0 andalso is_codatatype thy T then
3090 fold (add_maybe_def_axiom depth)
3091 (codatatype_bisim_axioms ext_ctxt T)
3094 (* int -> typ -> sort -> accumulator -> accumulator *)
3095 and add_axioms_for_sort depth T S =
3097 val supers = Sign.complete_sort thy S
3099 maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
3100 handle ERROR _ => [])) supers
3101 val monomorphic_class_axioms =
3102 map (fn t => case Term.add_tvars t [] of
3105 Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
3106 | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
3107 \add_axioms_for_sort", [t]))
3109 in fold (add_nondef_axiom depth) monomorphic_class_axioms end
3110 val (mono_user_nondefs, poly_user_nondefs) =
3111 List.partition (null o Term.hidden_polymorphism) user_nondefs
3112 val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
3114 val (xs, (defs, nondefs)) =
3115 ([], ([], [])) |> add_axioms_for_term 1 t
3116 |> fold_rev (add_def_axiom 1) eval_axioms
3117 |> user_axioms = SOME true
3118 ? fold (add_nondef_axiom 1) mono_user_nondefs
3119 val defs = defs @ special_congruence_axioms ext_ctxt xs
3121 ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
3122 null poly_user_nondefs))
3125 (* theory -> const_table -> styp -> int list *)
3126 fun const_format thy def_table (x as (s, T)) =
3127 if String.isPrefix unrolled_prefix s then
3128 const_format thy def_table (original_name s, range_type T)
3129 else if String.isPrefix skolem_prefix s then
3131 val k = unprefix skolem_prefix s
3132 |> strip_first_name_sep |> fst |> space_explode "@"
3133 |> hd |> Int.fromString |> the
3134 in [k, num_binder_types T - k] end
3135 else if original_name s <> s then
3136 [num_binder_types T]
3137 else case def_of_const thy def_table x of
3138 SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
3139 let val k = length (strip_abs_vars t') in
3140 [k, num_binder_types T - k]
3143 [num_binder_types T]
3144 | NONE => [num_binder_types T]
3145 (* int list -> int list -> int list *)
3146 fun intersect_formats _ [] = []
3147 | intersect_formats [] _ = []
3148 | intersect_formats ks1 ks2 =
3149 let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
3150 intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
3151 (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
3155 (* theory -> const_table -> (term option * int list) list -> term -> int list *)
3156 fun lookup_format thy def_table formats t =
3157 case AList.lookup (fn (SOME x, SOME y) =>
3158 (term_match thy) (x, y) | _ => false)
3160 SOME format => format
3161 | NONE => let val format = the (AList.lookup (op =) formats NONE) in
3163 Const x => intersect_formats format
3164 (const_format thy def_table x)
3168 (* int list -> int list -> typ -> typ *)
3169 fun format_type default_format format T =
3171 val T = unbox_type T
3172 val format = format |> filter (curry (op <) 0)
3174 if forall (equal 1) format then
3178 val (binder_Ts, body_T) = strip_type T
3181 |> map (format_type default_format default_format)
3182 |> rev |> chunk_list_unevenly (rev format)
3183 |> map (HOLogic.mk_tupleT o rev)
3184 in List.foldl (op -->) body_T batched end
3186 (* theory -> const_table -> (term option * int list) list -> term -> typ *)
3187 fun format_term_type thy def_table formats t =
3188 format_type (the (AList.lookup (op =) formats NONE))
3189 (lookup_format thy def_table formats t) (fastype_of t)
3191 (* int list -> int -> int list -> int list *)
3192 fun repair_special_format js m format =
3193 m - 1 downto 0 |> chunk_list_unevenly (rev format)
3194 |> map (rev o filter_out (member (op =) js))
3195 |> filter_out null |> map length |> rev
3197 (* extended_context -> string * string -> (term option * int list) list
3198 -> styp -> term * typ *)
3199 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
3200 : extended_context) (base_name, step_name) formats =
3202 val default_format = the (AList.lookup (op =) formats NONE)
3203 (* styp -> term * typ *)
3204 fun do_const (x as (s, T)) =
3205 (if String.isPrefix special_prefix s then
3208 val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
3209 val (x' as (_, T'), js, ts) =
3210 AList.find (op =) (!special_funs) (s, unbox_type T) |> the_single
3211 val max_j = List.last js
3212 val Ts = List.take (binder_types T', max_j + 1)
3213 val missing_js = filter_out (member (op =) js) (0 upto max_j)
3214 val missing_Ts = filter_indices missing_js Ts
3215 (* int -> indexname *)
3216 fun nth_missing_var n =
3217 ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
3218 val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
3219 val vars = special_bounds ts @ missing_vars
3220 val ts' = map2 (fn T => fn j =>
3221 case AList.lookup (op =) (js ~~ ts) j of
3224 Var (nth missing_vars
3225 (find_index (equal j) missing_js)))
3227 val t = do_const x' |> fst
3229 case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
3230 | _ => false) formats (SOME t) of
3232 repair_special_format js (num_binder_types T') format
3234 const_format thy def_table x'
3235 |> repair_special_format js (num_binder_types T')
3236 |> intersect_formats default_format
3238 (list_comb (t, ts') |> fold_rev abs_var vars,
3239 format_type default_format format T)
3241 else if String.isPrefix uncurry_prefix s then
3243 val (ss, s') = unprefix uncurry_prefix s
3244 |> strip_first_name_sep |>> space_explode "@"
3246 if String.isPrefix step_prefix s' then
3250 val k = the (Int.fromString (hd ss))
3251 val j = the (Int.fromString (List.last ss))
3252 val (before_Ts, (tuple_T, rest_T)) =
3253 strip_n_binders j T ||> (strip_n_binders 1 #>> hd)
3254 val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T
3255 in do_const (s', T') end
3257 else if String.isPrefix unrolled_prefix s then
3258 let val t = Const (original_name s, range_type T) in
3259 (lambda (Free (iter_var_prefix, nat_T)) t,
3260 format_type default_format
3261 (lookup_format thy def_table formats t) T)
3263 else if String.isPrefix base_prefix s then
3264 (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
3265 format_type default_format default_format T)
3266 else if String.isPrefix step_prefix s then
3267 (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
3268 format_type default_format default_format T)
3269 else if String.isPrefix skolem_prefix s then
3271 val ss = the (AList.lookup (op =) (!skolems) s)
3272 val (Ts, Ts') = chop (length ss) (binder_types T)
3273 val frees = map Free (ss ~~ Ts)
3274 val s' = original_name s
3276 (fold lambda frees (Const (s', Ts' ---> T)),
3277 format_type default_format
3278 (lookup_format thy def_table formats (Const x)) T)
3280 else if String.isPrefix eval_prefix s then
3282 val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
3283 in (t, format_term_type thy def_table formats t) end
3284 else if s = @{const_name undefined_fast_The} then
3285 (Const (nitpick_prefix ^ "The fallback", T),
3286 format_type default_format
3287 (lookup_format thy def_table formats
3288 (Const (@{const_name The}, (T --> bool_T) --> T))) T)
3289 else if s = @{const_name undefined_fast_Eps} then
3290 (Const (nitpick_prefix ^ "Eps fallback", T),
3291 format_type default_format
3292 (lookup_format thy def_table formats
3293 (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
3295 let val t = Const (original_name s, T) in
3296 (t, format_term_type thy def_table formats t)
3298 |>> map_types (typ_subst [(@{typ bisim_iterator}, nat_T)] o unbox_type)
3299 |>> shorten_const_names_in_term |>> shorten_abs_vars
3302 (* styp -> string *)
3303 fun assign_operator_for_const (s, T) =
3304 if String.isPrefix ubfp_prefix s then
3305 if is_fun_type T then "\<subseteq>" else "\<le>"
3306 else if String.isPrefix lbfp_prefix s then
3307 if is_fun_type T then "\<supseteq>" else "\<ge>"
3308 else if original_name s <> s then
3309 assign_operator_for_const (after_name_sep s, T)
3313 (* extended_context -> term
3314 -> ((term list * term list) * (bool * bool)) * term *)
3315 fun preprocess_term (ext_ctxt as {thy, destroy_constrs, boxes, skolemize,
3318 val skolem_depth = if skolemize then 4 else ~1
3319 val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
3320 core_t) = t |> unfold_defs_in_term ext_ctxt
3321 |> Refute.close_form
3322 |> skolemize_term_and_more ext_ctxt skolem_depth
3323 |> specialize_consts_in_term ext_ctxt 0
3324 |> `(axioms_for_term ext_ctxt)
3325 val maybe_box = exists (not_equal (SOME false) o snd) boxes
3327 Termtab.empty |> uncurry
3328 ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
3329 (* bool -> bool -> term -> term *)
3330 fun do_rest def core =
3331 uncurry ? uncurry_term table
3332 #> maybe_box ? box_fun_and_pair_in_term ext_ctxt def
3333 #> destroy_constrs ? (pull_out_universal_constrs thy def
3334 #> pull_out_existential_constrs thy
3335 #> destroy_pulled_out_constrs ext_ctxt def)
3337 #> destroy_universal_equalities
3338 #> destroy_existential_equalities thy
3339 #> simplify_constrs_and_sels thy
3340 #> distribute_quantifiers
3341 #> push_quantifiers_inward thy
3342 #> not core ? Refute.close_form
3345 (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
3346 (got_all_mono_user_axioms, no_poly_user_axioms)),
3347 do_rest false true core_t)