1 (* Title: HOL/Tools/Nitpick/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 binary_ints: bool option,
25 destroy_constrs: bool,
28 star_linear_preds: bool,
31 tac_timeout: Time.time option,
33 case_names: (string * int) list,
34 def_table: const_table,
35 nondef_table: const_table,
36 user_nondefs: term list,
37 simp_table: const_table Unsynchronized.ref,
38 psimp_table: const_table,
39 intro_table: const_table,
40 ground_thm_table: term list Inttab.table,
41 ersatz_table: (string * string) list,
42 skolems: (string * string list) list Unsynchronized.ref,
43 special_funs: special_fun list Unsynchronized.ref,
44 unrolled_preds: unrolled list Unsynchronized.ref,
45 wf_cache: wf_cache Unsynchronized.ref,
46 constr_cache: (typ * styp list) list Unsynchronized.ref}
49 val numeral_prefix : string
50 val skolem_prefix : string
51 val eval_prefix : string
52 val original_name : string -> string
53 val unbit_and_unbox_type : typ -> typ
54 val string_for_type : Proof.context -> typ -> string
55 val prefix_name : string -> string -> string
56 val shortest_name : string -> string
57 val short_name : string -> string
58 val shorten_names_in_term : term -> term
59 val type_match : theory -> typ * typ -> bool
60 val const_match : theory -> styp * styp -> bool
61 val term_match : theory -> term * term -> bool
62 val is_TFree : typ -> bool
63 val is_higher_order_type : typ -> bool
64 val is_fun_type : typ -> bool
65 val is_set_type : typ -> bool
66 val is_pair_type : typ -> bool
67 val is_lfp_iterator_type : typ -> bool
68 val is_gfp_iterator_type : typ -> bool
69 val is_fp_iterator_type : typ -> bool
70 val is_boolean_type : typ -> bool
71 val is_integer_type : typ -> bool
72 val is_bit_type : typ -> bool
73 val is_word_type : typ -> bool
74 val is_record_type : typ -> bool
75 val is_number_type : theory -> typ -> bool
76 val const_for_iterator_type : typ -> styp
77 val nth_range_type : int -> typ -> typ
78 val num_factors_in_type : typ -> int
79 val num_binder_types : typ -> int
80 val curried_binder_types : typ -> typ list
81 val mk_flat_tuple : typ -> term list -> term
82 val dest_n_tuple : int -> term -> term list
83 val instantiate_type : theory -> typ -> typ -> typ -> typ
84 val is_real_datatype : theory -> string -> bool
85 val is_codatatype : theory -> typ -> bool
86 val is_pure_typedef : theory -> typ -> bool
87 val is_univ_typedef : theory -> typ -> bool
88 val is_datatype : theory -> typ -> bool
89 val is_record_constr : styp -> bool
90 val is_record_get : theory -> styp -> bool
91 val is_record_update : theory -> styp -> bool
92 val is_abs_fun : theory -> styp -> bool
93 val is_rep_fun : theory -> styp -> bool
94 val is_constr : theory -> styp -> bool
95 val is_stale_constr : theory -> styp -> bool
96 val is_sel : string -> bool
97 val is_sel_like_and_no_discr : string -> bool
98 val discr_for_constr : styp -> styp
99 val num_sels_for_constr_type : typ -> int
100 val nth_sel_name_for_constr_name : string -> int -> string
101 val nth_sel_for_constr : styp -> int -> styp
102 val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
103 val sel_no_from_name : string -> int
104 val eta_expand : typ list -> term -> int -> term
105 val extensionalize : term -> term
106 val distinctness_formula : typ -> term list -> term
107 val register_frac_type : string -> (string * string) list -> theory -> theory
108 val unregister_frac_type : string -> theory -> theory
109 val register_codatatype : typ -> string -> styp list -> theory -> theory
110 val unregister_codatatype : typ -> theory -> theory
111 val datatype_constrs : extended_context -> typ -> styp list
112 val boxed_datatype_constrs : extended_context -> typ -> styp list
113 val num_datatype_constrs : extended_context -> typ -> int
114 val constr_name_for_sel_like : string -> string
115 val boxed_constr_for_sel : extended_context -> styp -> styp
116 val card_of_type : (typ * int) list -> typ -> int
117 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
118 val bounded_exact_card_of_type :
119 extended_context -> int -> int -> (typ * int) list -> typ -> int
120 val is_finite_type : extended_context -> typ -> bool
121 val all_axioms_of : theory -> term list * term list * term list
122 val arity_of_built_in_const : bool -> styp -> int option
123 val is_built_in_const : bool -> styp -> bool
124 val case_const_names : theory -> (string * int) list
125 val const_def_table : Proof.context -> term list -> const_table
126 val const_nondef_table : term list -> const_table
127 val const_simp_table : Proof.context -> const_table
128 val const_psimp_table : Proof.context -> const_table
129 val inductive_intro_table : Proof.context -> const_table -> const_table
130 val ground_theorem_table : theory -> term list Inttab.table
131 val ersatz_table : theory -> (string * string) list
132 val def_of_const : theory -> const_table -> styp -> term option
133 val is_inductive_pred : extended_context -> styp -> bool
134 val is_constr_pattern_lhs : theory -> term -> bool
135 val is_constr_pattern_formula : theory -> term -> bool
136 val merge_type_vars_in_terms : term list -> term list
137 val ground_types_in_type : extended_context -> typ -> typ list
138 val ground_types_in_terms : extended_context -> term list -> typ list
139 val format_type : int list -> int list -> typ -> typ
140 val format_term_type :
141 theory -> const_table -> (term option * int list) list -> term -> typ
142 val user_friendly_const :
143 extended_context -> string * string -> (term option * int list) list
144 -> styp -> term * typ
145 val assign_operator_for_const : styp -> string
146 val preprocess_term :
147 extended_context -> term -> ((term list * term list) * (bool * bool)) * term
150 structure Nitpick_HOL : NITPICK_HOL =
155 type const_table = term list Symtab.table
156 type special_fun = (styp * int list * term list) * styp
157 type unrolled = styp * styp
158 type wf_cache = (styp * (bool * bool)) list
160 type extended_context = {
163 max_bisim_depth: int,
164 boxes: (typ option * bool option) list,
165 wfs: (styp option * bool option) list,
166 user_axioms: bool option,
168 binary_ints: bool option,
169 destroy_constrs: bool,
172 star_linear_preds: bool,
175 tac_timeout: Time.time option,
177 case_names: (string * int) list,
178 def_table: const_table,
179 nondef_table: const_table,
180 user_nondefs: term list,
181 simp_table: const_table Unsynchronized.ref,
182 psimp_table: const_table,
183 intro_table: const_table,
184 ground_thm_table: term list Inttab.table,
185 ersatz_table: (string * string) list,
186 skolems: (string * string list) list Unsynchronized.ref,
187 special_funs: special_fun list Unsynchronized.ref,
188 unrolled_preds: unrolled list Unsynchronized.ref,
189 wf_cache: wf_cache Unsynchronized.ref,
190 constr_cache: (typ * styp list) list Unsynchronized.ref}
192 structure Data = Theory_Data(
193 type T = {frac_types: (string * (string * string) list) list,
194 codatatypes: (string * (string * styp list)) list}
195 val empty = {frac_types = [], codatatypes = []}
197 fun merge ({frac_types = fs1, codatatypes = cs1},
198 {frac_types = fs2, codatatypes = cs2}) : T =
199 {frac_types = AList.merge (op =) (K true) (fs1, fs2),
200 codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
202 (* term * term -> term *)
203 fun s_conj (t1, @{const True}) = t1
204 | s_conj (@{const True}, t2) = t2
206 if t1 = @{const False} orelse t2 = @{const False} then @{const False}
207 else HOLogic.mk_conj (t1, t2)
208 fun s_disj (t1, @{const False}) = t1
209 | s_disj (@{const False}, t2) = t2
211 if t1 = @{const True} orelse t2 = @{const True} then @{const True}
212 else HOLogic.mk_disj (t1, t2)
213 (* term -> term -> term *)
215 HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
217 (* term -> term -> term list *)
218 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
219 if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
220 | strip_connective _ t = [t]
221 (* term -> term list * term *)
222 fun strip_any_connective (t as (t0 $ t1 $ t2)) =
223 if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
224 (strip_connective t0 t, t0)
227 | strip_any_connective t = ([t], @{const Not})
228 (* term -> term list *)
229 val conjuncts = strip_connective @{const "op &"}
230 val disjuncts = strip_connective @{const "op |"}
233 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
234 val sel_prefix = nitpick_prefix ^ "sel"
235 val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
236 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
237 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
238 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
239 val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep
240 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
241 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
242 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
243 val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
244 val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
245 val skolem_prefix = nitpick_prefix ^ "sk"
246 val special_prefix = nitpick_prefix ^ "sp"
247 val uncurry_prefix = nitpick_prefix ^ "unc"
248 val eval_prefix = nitpick_prefix ^ "eval"
249 val bound_var_prefix = "b"
250 val cong_var_prefix = "c"
251 val iter_var_prefix = "i"
252 val val_var_prefix = nitpick_prefix ^ "v"
253 val arg_var_prefix = "x"
256 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
257 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
258 (* int -> int -> string *)
259 fun skolem_prefix_for k j =
260 skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
261 fun uncurry_prefix_for k j =
262 uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
264 (* string -> string * string *)
265 val strip_first_name_sep =
266 Substring.full #> Substring.position name_sep ##> Substring.triml 1
267 #> pairself Substring.string
268 (* string -> string *)
269 fun original_name s =
270 if String.isPrefix nitpick_prefix s then
271 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
274 val after_name_sep = snd o strip_first_name_sep
276 (* When you add constants to these lists, make sure to handle them in
277 "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
279 val built_in_consts =
280 [(@{const_name all}, 1),
281 (@{const_name "=="}, 2),
282 (@{const_name "==>"}, 2),
283 (@{const_name Pure.conjunction}, 2),
284 (@{const_name Trueprop}, 1),
285 (@{const_name Not}, 1),
286 (@{const_name False}, 0),
287 (@{const_name True}, 0),
288 (@{const_name All}, 1),
289 (@{const_name Ex}, 1),
290 (@{const_name "op ="}, 2),
291 (@{const_name "op &"}, 2),
292 (@{const_name "op |"}, 2),
293 (@{const_name "op -->"}, 2),
294 (@{const_name If}, 3),
295 (@{const_name Let}, 2),
296 (@{const_name Unity}, 0),
297 (@{const_name Pair}, 2),
298 (@{const_name fst}, 1),
299 (@{const_name snd}, 1),
300 (@{const_name Id}, 0),
301 (@{const_name insert}, 2),
302 (@{const_name converse}, 1),
303 (@{const_name trancl}, 1),
304 (@{const_name rel_comp}, 2),
305 (@{const_name image}, 2),
306 (@{const_name Suc}, 0),
307 (@{const_name finite}, 1),
308 (@{const_name nat}, 0),
309 (@{const_name zero_nat_inst.zero_nat}, 0),
310 (@{const_name one_nat_inst.one_nat}, 0),
311 (@{const_name plus_nat_inst.plus_nat}, 0),
312 (@{const_name minus_nat_inst.minus_nat}, 0),
313 (@{const_name times_nat_inst.times_nat}, 0),
314 (@{const_name div_nat_inst.div_nat}, 0),
315 (@{const_name ord_nat_inst.less_nat}, 2),
316 (@{const_name ord_nat_inst.less_eq_nat}, 2),
317 (@{const_name nat_gcd}, 0),
318 (@{const_name nat_lcm}, 0),
319 (@{const_name zero_int_inst.zero_int}, 0),
320 (@{const_name one_int_inst.one_int}, 0),
321 (@{const_name plus_int_inst.plus_int}, 0),
322 (@{const_name minus_int_inst.minus_int}, 0),
323 (@{const_name times_int_inst.times_int}, 0),
324 (@{const_name div_int_inst.div_int}, 0),
325 (@{const_name uminus_int_inst.uminus_int}, 0),
326 (@{const_name ord_int_inst.less_int}, 2),
327 (@{const_name ord_int_inst.less_eq_int}, 2),
328 (@{const_name Tha}, 1),
329 (@{const_name Frac}, 0),
330 (@{const_name norm_frac}, 0)]
331 val built_in_descr_consts =
332 [(@{const_name The}, 1),
333 (@{const_name Eps}, 1)]
334 val built_in_typed_consts =
335 [((@{const_name of_nat}, nat_T --> int_T), 0),
336 ((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)]
337 val built_in_set_consts =
338 [(@{const_name lower_semilattice_fun_inst.inf_fun}, 2),
339 (@{const_name upper_semilattice_fun_inst.sup_fun}, 2),
340 (@{const_name minus_fun_inst.minus_fun}, 2),
341 (@{const_name ord_fun_inst.less_eq_fun}, 2)]
344 fun unbit_type @{typ "unsigned_bit word"} = nat_T
345 | unbit_type @{typ "signed_bit word"} = int_T
346 | unbit_type @{typ bisim_iterator} = nat_T
347 | unbit_type (Type (s, Ts as _ :: _)) = Type (s, map unbit_type Ts)
349 fun unbit_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
350 unbit_and_unbox_type (Type ("fun", Ts))
351 | unbit_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
352 Type ("*", map unbit_and_unbox_type Ts)
353 | unbit_and_unbox_type @{typ "unsigned_bit word"} = nat_T
354 | unbit_and_unbox_type @{typ "signed_bit word"} = int_T
355 | unbit_and_unbox_type @{typ bisim_iterator} = nat_T
356 | unbit_and_unbox_type (Type (s, Ts as _ :: _)) =
357 Type (s, map unbit_and_unbox_type Ts)
358 | unbit_and_unbox_type T = T
359 (* Proof.context -> typ -> string *)
360 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type
362 (* string -> string -> string *)
363 val prefix_name = Long_Name.qualify o Long_Name.base_name
364 (* string -> string *)
365 fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
366 (* string -> term -> term *)
367 val prefix_abs_vars = Term.map_abs_vars o prefix_name
369 val shorten_abs_vars = Term.map_abs_vars shortest_name
370 (* string -> string *)
372 case space_explode name_sep s of
373 [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
374 | ss => map shortest_name ss |> space_implode "_"
376 fun shorten_names_in_type (Type (s, Ts)) =
377 Type (short_name s, map shorten_names_in_type Ts)
378 | shorten_names_in_type T = T
380 val shorten_names_in_term =
381 map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
382 #> map_types shorten_names_in_type
384 (* theory -> typ * typ -> bool *)
385 fun type_match thy (T1, T2) =
386 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
387 handle Type.TYPE_MATCH => false
388 (* theory -> styp * styp -> bool *)
389 fun const_match thy ((s1, T1), (s2, T2)) =
390 s1 = s2 andalso type_match thy (T1, T2)
391 (* theory -> term * term -> bool *)
392 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
393 | term_match thy (Free (s1, T1), Free (s2, T2)) =
394 const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
395 | term_match thy (t1, t2) = t1 aconv t2
398 fun is_TFree (TFree _) = true
400 fun is_higher_order_type (Type ("fun", _)) = true
401 | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
402 | is_higher_order_type _ = false
403 fun is_fun_type (Type ("fun", _)) = true
404 | is_fun_type _ = false
405 fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
406 | is_set_type _ = false
407 fun is_pair_type (Type ("*", _)) = true
408 | is_pair_type _ = false
409 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
410 | is_lfp_iterator_type _ = false
411 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
412 | is_gfp_iterator_type _ = false
413 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
414 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
415 val is_integer_type =
416 member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
417 fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
418 fun is_word_type (Type (@{type_name word}, _)) = true
419 | is_word_type _ = false
420 val is_record_type = not o null o Record.dest_recTs
421 (* theory -> typ -> bool *)
422 fun is_frac_type thy (Type (s, [])) =
423 not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
424 | is_frac_type _ _ = false
425 fun is_number_type thy = is_integer_type orf is_frac_type thy
427 (* bool -> styp -> typ *)
428 fun iterator_type_for_const gfp (s, T) =
429 Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
432 fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
433 | const_for_iterator_type T =
434 raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
436 (* int -> typ -> typ * typ *)
437 fun strip_n_binders 0 T = ([], T)
438 | strip_n_binders n (Type ("fun", [T1, T2])) =
439 strip_n_binders (n - 1) T2 |>> cons T1
440 | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
441 strip_n_binders n (Type ("fun", Ts))
442 | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
444 val nth_range_type = snd oo strip_n_binders
447 fun num_factors_in_type (Type ("*", [T1, T2])) =
448 fold (Integer.add o num_factors_in_type) [T1, T2] 0
449 | num_factors_in_type _ = 1
450 fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
451 | num_binder_types _ = 0
452 (* typ -> typ list *)
453 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
454 fun maybe_curried_binder_types T =
455 (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
457 (* typ -> term list -> term *)
458 fun mk_flat_tuple _ [t] = t
459 | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
460 HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
461 | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
462 (* int -> term -> term list *)
463 fun dest_n_tuple 1 t = [t]
464 | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
466 (* int -> typ -> typ list *)
467 fun dest_n_tuple_type 1 T = [T]
468 | dest_n_tuple_type n (Type (_, [T1, T2])) =
469 T1 :: dest_n_tuple_type (n - 1) T2
470 | dest_n_tuple_type _ T =
471 raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
473 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
474 e.g., by adding a field to "Datatype_Aux.info". *)
476 val is_basic_datatype =
477 member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
478 @{type_name nat}, @{type_name int},
479 "Code_Numeral.code_numeral"]
481 (* theory -> typ -> typ -> typ -> typ *)
482 fun instantiate_type thy T1 T1' T2 =
483 Same.commit (Envir.subst_type_same
484 (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
486 handle Type.TYPE_MATCH =>
487 raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
489 (* theory -> typ -> typ -> styp *)
490 fun repair_constr_type thy body_T' T =
491 instantiate_type thy (body_type T) body_T' T
493 (* string -> (string * string) list -> theory -> theory *)
494 fun register_frac_type frac_s ersaetze thy =
496 val {frac_types, codatatypes} = Data.get thy
497 val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
498 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
499 (* string -> theory -> theory *)
500 fun unregister_frac_type frac_s = register_frac_type frac_s []
502 (* typ -> string -> styp list -> theory -> theory *)
503 fun register_codatatype co_T case_name constr_xs thy =
505 val {frac_types, codatatypes} = Data.get thy
506 val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
507 val (co_s, co_Ts) = dest_Type co_T
509 if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts)
510 andalso co_s <> "fun" andalso not (is_basic_datatype co_s) then
513 raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
514 val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
516 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
517 (* typ -> theory -> theory *)
518 fun unregister_codatatype co_T = register_codatatype co_T "" []
521 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
522 set_def: thm option, prop_of_Rep: thm, set_name: string,
523 Abs_inverse: thm option, Rep_inverse: thm option}
525 (* theory -> string -> typedef_info *)
526 fun typedef_info thy s =
527 if is_frac_type thy (Type (s, [])) then
528 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
529 Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
530 set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
532 set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
533 else case Typedef.get_info thy s of
534 SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
536 SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
537 Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
538 set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
539 Rep_inverse = SOME Rep_inverse}
542 (* theory -> string -> bool *)
543 val is_typedef = is_some oo typedef_info
544 val is_real_datatype = is_some oo Datatype.get_info
545 (* theory -> typ -> bool *)
546 fun is_codatatype thy (T as Type (s, _)) =
547 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
548 |> Option.map snd |> these))
549 | is_codatatype _ _ = false
550 fun is_pure_typedef thy (T as Type (s, _)) =
551 is_typedef thy s andalso
552 not (is_real_datatype thy s orelse is_codatatype thy T
553 orelse is_record_type T orelse is_integer_type T)
554 | is_pure_typedef _ _ = false
555 fun is_univ_typedef thy (Type (s, _)) =
556 (case typedef_info thy s of
557 SOME {set_def, prop_of_Rep, ...} =>
560 try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
562 try (fst o dest_Const o snd o HOLogic.dest_mem
563 o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
565 | is_univ_typedef _ _ = false
566 fun is_datatype thy (T as Type (s, _)) =
567 (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind})
568 andalso not (is_basic_datatype s)
569 | is_datatype _ _ = false
571 (* theory -> typ -> (string * typ) list * (string * typ) *)
572 fun all_record_fields thy T =
573 let val (recs, more) = Record.get_extT_fields thy T in
574 recs @ more :: all_record_fields thy (snd more)
578 fun is_record_constr (x as (s, T)) =
579 String.isSuffix Record.extN s andalso
580 let val dataT = body_type T in
581 is_record_type dataT andalso
582 s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
584 (* theory -> typ -> int *)
585 val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
586 (* theory -> string -> typ -> int *)
587 fun no_of_record_field thy s T1 =
588 find_index (curry (op =) s o fst)
589 (Record.get_extT_fields thy T1 ||> single |> op @)
590 (* theory -> styp -> bool *)
591 fun is_record_get thy (s, Type ("fun", [T1, _])) =
592 exists (curry (op =) s o fst) (all_record_fields thy T1)
593 | is_record_get _ _ = false
594 fun is_record_update thy (s, T) =
595 String.isSuffix Record.updateN s andalso
596 exists (curry (op =) (unsuffix Record.updateN s) o fst)
597 (all_record_fields thy (body_type T))
598 handle TYPE _ => false
599 fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
600 (case typedef_info thy s' of
601 SOME {Abs_name, ...} => s = Abs_name
603 | is_abs_fun _ _ = false
604 fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
605 (case typedef_info thy s' of
606 SOME {Rep_name, ...} => s = Rep_name
608 | is_rep_fun _ _ = false
610 (* theory -> styp -> styp *)
611 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
612 (case typedef_info thy s' of
613 SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
614 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
615 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
617 (* theory -> styp -> bool *)
618 fun is_coconstr thy (s, T) =
620 val {codatatypes, ...} = Data.get thy
621 val co_T = body_type T
622 val co_s = dest_Type co_T |> fst
624 exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
625 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
627 handle TYPE ("dest_Type", _, _) => false
628 fun is_constr_like thy (s, T) =
629 s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
630 let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
631 Refute.is_IDT_constructor thy x orelse is_record_constr x
632 orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
633 orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep}
634 orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
635 orelse is_coconstr thy x
637 fun is_stale_constr thy (x as (_, T)) =
638 is_codatatype thy (body_type T) andalso is_constr_like thy x
639 andalso not (is_coconstr thy x)
640 fun is_constr thy (x as (_, T)) =
642 andalso not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T)))))
643 andalso not (is_stale_constr thy x)
645 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
646 val is_sel_like_and_no_discr =
647 String.isPrefix sel_prefix
648 orf (member (op =) [@{const_name fst}, @{const_name snd}])
650 datatype boxability =
651 InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
653 (* boxability -> boxability *)
654 fun in_fun_lhs_for InConstr = InSel
655 | in_fun_lhs_for _ = InFunLHS
656 fun in_fun_rhs_for InConstr = InConstr
657 | in_fun_rhs_for InSel = InSel
658 | in_fun_rhs_for InFunRHS1 = InFunRHS2
659 | in_fun_rhs_for _ = InFunRHS1
661 (* extended_context -> boxability -> typ -> bool *)
662 fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
665 (boxy = InPair orelse boxy = InFunLHS)
666 andalso not (is_boolean_type (body_type T))
668 boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2
669 orelse ((boxy = InExpr orelse boxy = InFunLHS)
670 andalso exists (is_boxing_worth_it ext_ctxt InPair)
671 (map (box_type ext_ctxt InPair) Ts))
673 (* extended_context -> boxability -> string * typ list -> string *)
674 and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
675 case triple_lookup (type_match thy) boxes (Type z) of
676 SOME (SOME box_me) => box_me
677 | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
678 (* extended_context -> boxability -> typ -> typ *)
679 and box_type ext_ctxt boxy T =
681 Type (z as ("fun", [T1, T2])) =>
682 if boxy <> InConstr andalso boxy <> InSel
683 andalso should_box_type ext_ctxt boxy z then
684 Type (@{type_name fun_box},
685 [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
687 box_type ext_ctxt (in_fun_lhs_for boxy) T1
688 --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
689 | Type (z as ("*", Ts)) =>
690 if should_box_type ext_ctxt boxy z then
691 Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
693 Type ("*", map (box_type ext_ctxt
694 (if boxy = InConstr orelse boxy = InSel then boxy
699 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
702 fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
703 (* string -> int -> string *)
704 fun nth_sel_name_for_constr_name s n =
705 if s = @{const_name Pair} then
706 if n = 0 then @{const_name fst} else @{const_name snd}
709 (* styp -> int -> styp *)
710 fun nth_sel_for_constr x ~1 = discr_for_constr x
711 | nth_sel_for_constr (s, T) n =
712 (nth_sel_name_for_constr_name s n,
713 body_type T --> nth (maybe_curried_binder_types T) n)
714 (* extended_context -> styp -> int -> styp *)
715 fun boxed_nth_sel_for_constr ext_ctxt =
716 apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr
719 fun sel_no_from_name s =
720 if String.isPrefix discr_prefix s then
722 else if String.isPrefix sel_prefix s then
723 s |> unprefix sel_prefix |> Int.fromString |> the
724 else if s = @{const_name snd} then
729 (* typ list -> term -> int -> term *)
730 fun eta_expand _ t 0 = t
731 | eta_expand Ts (Abs (s, T, t')) n =
732 Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
733 | eta_expand Ts t n =
734 fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
735 (List.take (binder_types (fastype_of1 (Ts, t)), n))
736 (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
739 fun extensionalize t =
741 (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
742 | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>
743 let val v = Var ((s, maxidx_of_term t + 1), T) in
744 extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))
748 (* typ -> term list -> term *)
749 fun distinctness_formula T =
750 all_distinct_unordered_pairs_of
751 #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
752 #> List.foldr (s_conj o swap) @{const True}
755 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
756 fun suc_const T = Const (@{const_name Suc}, T --> T)
758 (* theory -> typ -> styp list *)
759 fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
760 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
761 SOME (_, xs' as (_ :: _)) =>
762 map (apsnd (repair_constr_type thy T)) xs'
764 if is_datatype thy T then
765 case Datatype.get_info thy s of
766 SOME {index, descr, ...} =>
768 val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
771 (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
775 if is_record_type T then
777 val s' = unsuffix Record.ext_typeN s ^ Record.extN
778 val T' = (Record.get_extT_fields thy T
779 |> apsnd single |> uncurry append |> map snd) ---> T
781 else case typedef_info thy s of
782 SOME {abs_type, rep_type, Abs_name, ...} =>
783 [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
785 if T = @{typ ind} then
786 [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
791 | uncached_datatype_constrs _ _ = []
792 (* extended_context -> typ -> styp list *)
793 fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
795 case AList.lookup (op =) (!constr_cache) T of
798 let val xs = uncached_datatype_constrs thy T in
799 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
801 fun boxed_datatype_constrs ext_ctxt =
802 map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
803 (* extended_context -> typ -> int *)
804 val num_datatype_constrs = length oo datatype_constrs
806 (* string -> string *)
807 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
808 | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
809 | constr_name_for_sel_like s' = original_name s'
810 (* extended_context -> styp -> styp *)
811 fun boxed_constr_for_sel ext_ctxt (s', T') =
812 let val s = constr_name_for_sel_like s' in
813 AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
816 (* extended_context -> styp -> term *)
817 fun discr_term_for_constr ext_ctxt (x as (s, T)) =
818 let val dataT = body_type T in
819 if s = @{const_name Suc} then
821 @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
822 else if num_datatype_constrs ext_ctxt dataT >= 2 then
823 Const (discr_for_constr x)
825 Abs (Name.uu, dataT, @{const True})
828 (* extended_context -> styp -> term -> term *)
829 fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
832 if x = x' then @{const True}
833 else if is_constr_like thy x' then @{const False}
834 else betapply (discr_term_for_constr ext_ctxt x, t)
835 | _ => betapply (discr_term_for_constr ext_ctxt x, t)
837 (* styp -> term -> term *)
838 fun nth_arg_sel_term_for_constr (x as (s, T)) n =
839 let val (arg_Ts, dataT) = strip_type T in
840 if dataT = nat_T then
841 @{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}
842 else if is_pair_type dataT then
843 Const (nth_sel_for_constr x n)
846 (* int -> typ -> int * term *)
847 fun aux m (Type ("*", [T1, T2])) =
849 val (m, t1) = aux m T1
850 val (m, t2) = aux m T2
851 in (m, HOLogic.mk_prod (t1, t2)) end
853 (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
855 val m = fold (Integer.add o num_factors_in_type)
856 (List.take (arg_Ts, n)) 0
857 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
859 (* theory -> styp -> term -> int -> typ -> term *)
860 fun select_nth_constr_arg thy x t n res_T =
863 if x = x' then nth args n
864 else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
865 else betapply (nth_arg_sel_term_for_constr x n, t)
866 | _ => betapply (nth_arg_sel_term_for_constr x n, t)
868 (* theory -> styp -> term list -> term *)
869 fun construct_value _ x [] = Const x
870 | construct_value thy (x as (s, _)) args =
871 let val args = map Envir.eta_contract args in
873 Const (x' as (s', _)) $ t =>
874 if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s
875 andalso forall (fn (n, t') =>
876 select_nth_constr_arg thy x t n dummyT = t')
877 (index_seq 0 (length args) ~~ args) then
880 list_comb (Const x, args)
881 | _ => list_comb (Const x, args)
884 (* extended_context -> typ -> term -> term *)
885 fun constr_expand (ext_ctxt as {thy, ...}) T t =
887 Const x => if is_constr_like thy x then t else raise SAME ()
888 | _ => raise SAME ())
892 if is_pair_type T then
893 let val (T1, T2) = HOLogic.dest_prodT T in
894 (@{const_name Pair}, T1 --> T2 --> T)
897 datatype_constrs ext_ctxt T |> the_single
898 val arg_Ts = binder_types T'
900 list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
901 (index_seq 0 (length arg_Ts)) arg_Ts)
904 (* (typ * int) list -> typ -> int *)
905 fun card_of_type assigns (Type ("fun", [T1, T2])) =
906 reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
907 | card_of_type assigns (Type ("*", [T1, T2])) =
908 card_of_type assigns T1 * card_of_type assigns T2
909 | card_of_type _ (Type (@{type_name itself}, _)) = 1
910 | card_of_type _ @{typ prop} = 2
911 | card_of_type _ @{typ bool} = 2
912 | card_of_type _ @{typ unit} = 1
913 | card_of_type assigns T =
914 case AList.lookup (op =) assigns T of
916 | NONE => if T = @{typ bisim_iterator} then 0
917 else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
918 (* int -> (typ * int) list -> typ -> int *)
919 fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
921 val k1 = bounded_card_of_type max default_card assigns T1
922 val k2 = bounded_card_of_type max default_card assigns T2
924 if k1 = max orelse k2 = max then max
925 else Int.min (max, reasonable_power k2 k1)
927 | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
929 val k1 = bounded_card_of_type max default_card assigns T1
930 val k2 = bounded_card_of_type max default_card assigns T2
931 in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
932 | bounded_card_of_type max default_card assigns T =
933 Int.min (max, if default_card = ~1 then
934 card_of_type assigns T
936 card_of_type assigns T
937 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
939 (* extended_context -> int -> (typ * int) list -> typ -> int *)
940 fun bounded_exact_card_of_type ext_ctxt max default_card assigns T =
942 (* typ list -> typ -> int *)
944 (if member (op =) avoid T then
947 Type ("fun", [T1, T2]) =>
949 val k1 = aux avoid T1
950 val k2 = aux avoid T2
952 if k1 = 0 orelse k2 = 0 then 0
953 else if k1 >= max orelse k2 >= max then max
954 else Int.min (max, reasonable_power k2 k1)
956 | Type ("*", [T1, T2]) =>
958 val k1 = aux avoid T1
959 val k2 = aux avoid T2
961 if k1 = 0 orelse k2 = 0 then 0
962 else if k1 >= max orelse k2 >= max then max
963 else Int.min (max, k1 * k2)
965 | Type (@{type_name itself}, _) => 1
970 (case datatype_constrs ext_ctxt T of
971 [] => if is_integer_type T then 0 else raise SAME ()
975 datatype_constrs ext_ctxt T
976 |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
979 if exists (curry (op =) 0) constr_cards then 0
980 else Integer.sum constr_cards
982 | _ => raise SAME ())
984 AList.lookup (op =) assigns T |> the_default default_card
985 in Int.min (max, aux [] T) end
987 (* extended_context -> typ -> bool *)
988 fun is_finite_type ext_ctxt =
989 not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 []
992 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
993 | is_ground_term (Const _) = true
994 | is_ground_term _ = false
996 (* term -> word -> word *)
997 fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
998 | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
1001 val hash_term = Word.toInt o hashw_term
1003 (* term list -> (indexname * typ) list *)
1004 fun special_bounds ts =
1005 fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
1007 (* indexname * typ -> term -> term *)
1008 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
1010 (* theory -> string -> bool *)
1011 fun is_funky_typedef_name thy s =
1012 member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
1014 orelse is_frac_type thy (Type (s, []))
1015 (* theory -> term -> bool *)
1016 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
1017 | is_funky_typedef _ _ = false
1019 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
1020 $ Const (@{const_name TYPE}, _)) = true
1021 | is_arity_type_axiom _ = false
1022 (* theory -> bool -> term -> bool *)
1023 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
1024 is_typedef_axiom thy boring t2
1025 | is_typedef_axiom thy boring
1026 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
1027 $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
1028 boring <> is_funky_typedef_name thy s andalso is_typedef thy s
1029 | is_typedef_axiom _ _ _ = false
1031 (* Distinguishes between (1) constant definition axioms, (2) type arity and
1032 typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
1033 Typedef axioms are uninteresting to Nitpick, because it can retrieve them
1034 using "typedef_info". *)
1035 (* theory -> (string * term) list -> string list -> term list * term list *)
1036 fun partition_axioms_by_definitionality thy axioms def_names =
1038 val axioms = sort (fast_string_ord o pairself fst) axioms
1039 val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
1041 OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
1042 |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
1043 in pairself (map snd) (defs, nondefs) end
1045 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
1046 will do as long as it contains all the "axioms" and "axiomatization"
1048 (* theory -> bool *)
1049 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
1052 val is_plain_definition =
1056 case strip_comb t1 of
1057 (Const _, args) => forall is_Var args
1058 andalso not (has_duplicates (op =) args)
1060 fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
1061 | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
1066 (* theory -> term list * term list * term list *)
1067 fun all_axioms_of thy =
1069 (* theory list -> term list *)
1070 val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
1071 val specs = Defs.all_specifications_of (Theory.defs_of thy)
1072 val def_names = specs |> maps snd |> map_filter #def
1073 |> OrdList.make fast_string_ord
1074 val thys = thy :: Theory.ancestors_of thy
1075 val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
1076 val built_in_axioms = axioms_of_thys built_in_thys
1077 val user_axioms = axioms_of_thys user_thys
1078 val (built_in_defs, built_in_nondefs) =
1079 partition_axioms_by_definitionality thy built_in_axioms def_names
1080 ||> filter (is_typedef_axiom thy false)
1081 val (user_defs, user_nondefs) =
1082 partition_axioms_by_definitionality thy user_axioms def_names
1083 val (built_in_nondefs, user_nondefs) =
1084 List.partition (is_typedef_axiom thy false) user_nondefs
1085 |>> append built_in_nondefs
1087 (thy |> PureThy.all_thms_of
1088 |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
1089 |> map (prop_of o snd) |> filter is_plain_definition) @
1090 user_defs @ built_in_defs
1091 in (defs, built_in_nondefs, user_nondefs) end
1093 (* bool -> styp -> int option *)
1094 fun arity_of_built_in_const fast_descrs (s, T) =
1095 if s = @{const_name If} then
1096 if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
1097 else case AList.lookup (op =)
1099 |> fast_descrs ? append built_in_descr_consts) s of
1102 case AList.lookup (op =) built_in_typed_consts (s, T) of
1105 if is_fun_type T andalso is_set_type (domain_type T) then
1106 AList.lookup (op =) built_in_set_consts s
1109 (* bool -> styp -> bool *)
1110 val is_built_in_const = is_some oo arity_of_built_in_const
1112 (* This function is designed to work for both real definition axioms and
1113 simplification rules (equational specifications). *)
1115 fun term_under_def t =
1117 @{const "==>"} $ _ $ t2 => term_under_def t2
1118 | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
1119 | @{const Trueprop} $ t1 => term_under_def t1
1120 | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
1121 | Abs (_, _, t') => term_under_def t'
1122 | t1 $ _ => term_under_def t1
1125 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
1126 traversal of the term, without which the wrong occurrence of a constant could
1127 be matched in the face of overloading. *)
1128 (* theory -> bool -> const_table -> styp -> term list *)
1129 fun def_props_for_const thy fast_descrs table (x as (s, _)) =
1130 if is_built_in_const fast_descrs x then
1133 these (Symtab.lookup table s)
1134 |> map_filter (try (Refute.specialize_type thy x))
1135 |> filter (curry (op =) (Const x) o term_under_def)
1137 (* theory -> term -> term option *)
1138 fun normalized_rhs_of thy t =
1140 (* term option -> term option *)
1141 fun aux (v as Var _) (SOME t) = SOME (lambda v t)
1142 | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
1146 Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
1147 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
1149 | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
1150 val args = strip_comb lhs |> snd
1151 in fold_rev aux args (SOME rhs) end
1153 (* theory -> const_table -> styp -> term option *)
1154 fun def_of_const thy table (x as (s, _)) =
1155 if is_built_in_const false x orelse original_name s <> s then
1158 x |> def_props_for_const thy false table |> List.last
1159 |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
1160 handle List.Empty => NONE
1162 datatype fixpoint_kind = Lfp | Gfp | NoFp
1164 (* term -> fixpoint_kind *)
1165 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
1166 | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
1167 | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
1168 | fixpoint_kind_of_rhs _ = NoFp
1170 (* theory -> const_table -> term -> bool *)
1171 fun is_mutually_inductive_pred_def thy table t =
1174 fun is_good_arg (Bound _) = true
1175 | is_good_arg (Const (s, _)) =
1176 s = @{const_name True} orelse s = @{const_name False}
1177 orelse s = @{const_name undefined}
1178 | is_good_arg _ = false
1180 case t |> strip_abs_body |> strip_comb of
1181 (Const x, ts as (_ :: _)) =>
1182 (case def_of_const thy table x of
1183 SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
1187 (* theory -> const_table -> term -> term *)
1188 fun unfold_mutually_inductive_preds thy table =
1189 map_aterms (fn t as Const x =>
1190 (case def_of_const thy table x of
1192 let val t' = Envir.eta_contract t' in
1193 if is_mutually_inductive_pred_def thy table t' then t'
1199 (* term -> string * term *)
1200 fun pair_for_prop t =
1201 case term_under_def t of
1202 Const (s, _) => (s, t)
1203 | Free _ => raise NOT_SUPPORTED "local definitions"
1204 | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
1206 (* (Proof.context -> term list) -> Proof.context -> const_table *)
1207 fun table_for get ctxt =
1208 get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
1210 (* theory -> (string * int) list *)
1211 fun case_const_names thy =
1212 Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
1213 if is_basic_datatype dtype_s then
1216 cons (case_name, AList.lookup (op =) descr index
1217 |> the |> #3 |> length))
1218 (Datatype.get_all thy) [] @
1219 map (apsnd length o snd) (#codatatypes (Data.get thy))
1221 (* Proof.context -> term list -> const_table *)
1222 fun const_def_table ctxt ts =
1223 table_for (rev o map prop_of o Nitpick_Defs.get) ctxt
1224 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
1225 (map pair_for_prop ts)
1226 (* term list -> const_table *)
1227 fun const_nondef_table ts =
1228 fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
1229 |> AList.group (op =) |> Symtab.make
1230 (* Proof.context -> const_table *)
1231 val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
1232 val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
1233 (* Proof.context -> const_table -> const_table *)
1234 fun inductive_intro_table ctxt def_table =
1235 table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
1236 def_table o prop_of)
1237 o Nitpick_Intros.get) ctxt
1238 (* theory -> term list Inttab.table *)
1239 fun ground_theorem_table thy =
1240 fold ((fn @{const Trueprop} $ t1 =>
1241 is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
1242 | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
1244 val basic_ersatz_table =
1245 [(@{const_name prod_case}, @{const_name split}),
1246 (@{const_name card}, @{const_name card'}),
1247 (@{const_name setsum}, @{const_name setsum'}),
1248 (@{const_name fold_graph}, @{const_name fold_graph'}),
1249 (@{const_name wf}, @{const_name wf'}),
1250 (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
1251 (@{const_name wfrec}, @{const_name wfrec'})]
1253 (* theory -> (string * string) list *)
1254 fun ersatz_table thy =
1255 fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
1257 (* const_table Unsynchronized.ref -> string -> term list -> unit *)
1258 fun add_simps simp_table s eqs =
1259 Unsynchronized.change simp_table
1260 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
1262 (* Similar to "Refute.specialize_type" but returns all matches rather than only
1263 the first (preorder) match. *)
1264 (* theory -> styp -> term -> term list *)
1265 fun multi_specialize_type thy slack (x as (s, T)) t =
1267 (* term -> (typ * term) list -> (typ * term) list *)
1268 fun aux (Const (s', T')) ys =
1270 ys |> (if AList.defined (op =) ys T' then
1273 cons (T', Refute.monomorphic_term
1274 (Sign.typ_match thy (T', T) Vartab.empty) t)
1275 handle Type.TYPE_MATCH => I
1276 | Refute.REFUTE _ =>
1280 raise NOT_SUPPORTED ("too much polymorphism in \
1281 \axiom involving " ^ quote s))
1285 in map snd (fold_aterms aux t []) end
1287 (* theory -> bool -> const_table -> styp -> term list *)
1288 fun nondef_props_for_const thy slack table (x as (s, _)) =
1289 these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
1291 (* theory -> styp list -> term list *)
1292 fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
1293 let val abs_T = Type (abs_s, abs_Ts) in
1294 if is_univ_typedef thy abs_T then
1296 else case typedef_info thy abs_s of
1297 SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,
1300 val rep_T = instantiate_type thy abs_type abs_T rep_type
1301 val rep_t = Const (Rep_name, abs_T --> rep_T)
1302 val set_t = Const (set_name, rep_T --> bool_T)
1304 prop_of_Rep |> HOLogic.dest_Trueprop
1305 |> Refute.specialize_type thy (dest_Const rep_t)
1306 |> HOLogic.dest_mem |> snd
1308 [HOLogic.all_const abs_T
1309 $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
1310 |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
1311 |> map HOLogic.mk_Trueprop
1315 (* theory -> styp -> term list *)
1316 fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
1317 let val abs_T = domain_type T in
1318 typedef_info thy (fst (dest_Type abs_T)) |> the
1319 |> pairf #Abs_inverse #Rep_inverse
1320 |> pairself (Refute.specialize_type thy x o prop_of o the)
1324 (* theory -> int * styp -> term *)
1325 fun constr_case_body thy (j, (x as (_, T))) =
1326 let val arg_Ts = binder_types T in
1327 list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
1328 (index_seq 0 (length arg_Ts)) arg_Ts)
1330 (* extended_context -> typ -> int * styp -> term -> term *)
1331 fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
1332 Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
1333 $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
1335 (* extended_context -> typ -> typ -> term *)
1336 fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
1338 val xs = datatype_constrs ext_ctxt dataT
1339 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
1340 val (xs', x) = split_last xs
1342 constr_case_body thy (1, x)
1343 |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
1344 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
1347 (* extended_context -> string -> typ -> typ -> term -> term *)
1348 fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
1349 let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
1350 case no_of_record_field thy s rec_T of
1351 ~1 => (case rec_T of
1352 Type (_, Ts as _ :: _) =>
1354 val rec_T' = List.last Ts
1355 val j = num_record_fields thy rec_T - 1
1357 select_nth_constr_arg thy constr_x t j res_T
1358 |> optimized_record_get ext_ctxt s rec_T' res_T
1360 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
1362 | j => select_nth_constr_arg thy constr_x t j res_T
1364 (* extended_context -> string -> typ -> term -> term -> term *)
1365 fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
1367 val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
1368 val Ts = binder_types constr_T
1370 val special_j = no_of_record_field thy s rec_T
1371 val ts = map2 (fn j => fn T =>
1373 val t = select_nth_constr_arg thy constr_x rec_t j T
1375 if j = special_j then
1377 else if j = n - 1 andalso special_j = ~1 then
1378 optimized_record_update ext_ctxt s
1379 (rec_T |> dest_Type |> snd |> List.last) fun_t t
1382 end) (index_seq 0 n) Ts
1383 in list_comb (Const constr_x, ts) end
1385 (* Constants "c" whose definition is of the form "c == c'", where "c'" is also a
1386 constant, are said to be trivial. For those, we ignore the simplification
1387 rules and use the definition instead, to ensure that built-in symbols like
1388 "ord_nat_inst.less_eq_nat" are picked up correctly. *)
1389 (* theory -> const_table -> styp -> bool *)
1390 fun has_trivial_definition thy table x =
1391 case def_of_const thy table x of SOME (Const _) => true | _ => false
1393 (* theory -> const_table -> string * typ -> fixpoint_kind *)
1394 fun fixpoint_kind_of_const thy table x =
1395 if is_built_in_const false x then
1398 fixpoint_kind_of_rhs (the (def_of_const thy table x))
1399 handle Option.Option => NoFp
1401 (* extended_context -> styp -> bool *)
1402 fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
1403 : extended_context) x =
1404 not (null (def_props_for_const thy fast_descrs intro_table x))
1405 andalso fixpoint_kind_of_const thy def_table x <> NoFp
1406 fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
1407 : extended_context) x =
1408 exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
1409 [!simp_table, psimp_table]
1410 fun is_inductive_pred ext_ctxt =
1411 is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
1412 fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
1413 (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
1414 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
1415 andf (not o has_trivial_definition thy def_table)
1417 (* term * term -> term *)
1418 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
1419 | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
1420 | s_betapply p = betapply p
1421 (* term * term list -> term *)
1422 val s_betapplys = Library.foldl s_betapply
1425 fun lhs_of_equation t =
1427 Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1428 | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
1429 | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
1430 | @{const Trueprop} $ t1 => lhs_of_equation t1
1431 | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1432 | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
1433 | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
1435 (* theory -> term -> bool *)
1436 fun is_constr_pattern _ (Bound _) = true
1437 | is_constr_pattern _ (Var _) = true
1438 | is_constr_pattern thy t =
1439 case strip_comb t of
1440 (Const (x as (s, _)), args) =>
1441 is_constr_like thy x andalso forall (is_constr_pattern thy) args
1443 fun is_constr_pattern_lhs thy t =
1444 forall (is_constr_pattern thy) (snd (strip_comb t))
1445 fun is_constr_pattern_formula thy t =
1446 case lhs_of_equation t of
1447 SOME t' => is_constr_pattern_lhs thy t'
1450 val unfold_max_depth = 255
1451 val axioms_max_depth = 255
1453 (* extended_context -> term -> term *)
1454 fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
1455 case_names, def_table, ground_thm_table,
1456 ersatz_table, ...}) =
1458 (* int -> typ list -> term -> term *)
1459 fun do_term depth Ts t =
1461 (t0 as Const (@{const_name Int.number_class.number_of},
1462 Type ("fun", [_, ran_T]))) $ t1 =>
1463 ((if is_number_type thy ran_T then
1465 val j = t1 |> HOLogic.dest_numeral
1466 |> ran_T = nat_T ? Integer.max 0
1467 val s = numeral_prefix ^ signed_string_of_int j
1469 if is_integer_type ran_T then
1472 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
1475 handle TERM _ => raise SAME ()
1478 handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
1479 | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
1480 do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
1481 | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
1482 $ (t2 as Abs (_, _, t2')) =>
1483 betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
1484 map (do_term depth Ts) [t1, t2])
1485 | Const (x as (@{const_name distinct},
1486 Type ("fun", [Type (@{type_name list}, [T']), _])))
1488 (t1 |> HOLogic.dest_list |> distinctness_formula T'
1489 handle TERM _ => do_const depth Ts t x [t1])
1490 | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
1491 if is_ground_term t1
1492 andalso exists (Pattern.matches thy o rpair t1)
1493 (Inttab.lookup_list ground_thm_table
1494 (hash_term t1)) then
1497 do_const depth Ts t x [t1, t2, t3]
1498 | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
1499 | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
1500 | Const x $ t1 => do_const depth Ts t x [t1]
1501 | Const x => do_const depth Ts t x []
1502 | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
1506 | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
1507 (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
1508 and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
1509 (Abs (Name.uu, body_type T,
1510 select_nth_constr_arg thy x (Bound 0) n res_T), [])
1511 | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
1512 (select_nth_constr_arg thy x (do_term depth Ts t) n res_T, ts)
1513 (* int -> typ list -> term -> styp -> term list -> term *)
1514 and do_const depth Ts t (x as (s, T)) ts =
1515 case AList.lookup (op =) ersatz_table s of
1517 do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
1521 if is_built_in_const fast_descrs x then
1523 else case AList.lookup (op =) case_names s of
1526 val (dataT, res_T) = nth_range_type n T
1527 |> pairf domain_type range_type
1529 (optimized_case_def ext_ctxt dataT res_T
1530 |> do_term (depth + 1) Ts, ts)
1533 if is_constr thy x then
1535 else if is_stale_constr thy x then
1536 raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
1538 else if is_record_get thy x then
1540 0 => (do_term depth Ts (eta_expand Ts t 1), [])
1541 | _ => (optimized_record_get ext_ctxt s (domain_type T)
1542 (range_type T) (hd ts), tl ts)
1543 else if is_record_update thy x then
1545 2 => (optimized_record_update ext_ctxt
1546 (unsuffix Record.updateN s) (nth_range_type 2 T)
1547 (do_term depth Ts (hd ts))
1548 (do_term depth Ts (nth ts 1)), [])
1549 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
1550 else if is_rep_fun thy x then
1551 let val x' = mate_of_rep_fun thy x in
1552 if is_constr thy x' then
1553 select_nth_constr_arg_with_args depth Ts x' ts 0
1558 else if is_equational_fun ext_ctxt x then
1560 else case def_of_const thy def_table x of
1562 if depth > unfold_max_depth then
1563 raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
1564 "too many nested definitions (" ^
1565 string_of_int depth ^ ") while expanding " ^
1567 else if s = @{const_name wfrec'} then
1568 (do_term (depth + 1) Ts (betapplys (def, ts)), [])
1570 (do_term (depth + 1) Ts def, ts)
1571 | NONE => (Const x, ts)
1572 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
1575 (* extended_context -> typ -> term list *)
1576 fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
1578 val xs = datatype_constrs ext_ctxt T
1579 val set_T = T --> bool_T
1580 val iter_T = @{typ bisim_iterator}
1581 val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
1582 val bisim_max = @{const bisim_iterator_max}
1583 val n_var = Var (("n", 0), iter_T)
1585 Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T)
1586 $ Abs ("m", iter_T, HOLogic.eq_const iter_T
1587 $ (suc_const iter_T $ Bound 0) $ n_var)
1588 val x_var = Var (("x", 0), T)
1589 val y_var = Var (("y", 0), T)
1590 (* styp -> int -> typ -> term *)
1591 fun nth_sub_bisim x n nth_T =
1592 (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
1593 else HOLogic.eq_const nth_T)
1594 $ select_nth_constr_arg thy x x_var n nth_T
1595 $ select_nth_constr_arg thy x y_var n nth_T
1597 fun case_func (x as (_, T)) =
1599 val arg_Ts = binder_types T
1601 discriminate_value ext_ctxt x y_var ::
1602 map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
1604 in List.foldr absdummy core_t arg_Ts end
1606 [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
1607 $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
1608 $ (betapplys (optimized_case_def ext_ctxt T bool_T,
1609 map case_func xs @ [x_var]))),
1610 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
1611 $ (Const (@{const_name insert}, T --> set_T --> set_T)
1612 $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
1613 |> map HOLogic.mk_Trueprop
1616 exception NO_TRIPLE of unit
1618 (* theory -> styp -> term -> term list * term list * term *)
1619 fun triple_for_intro_rule thy x t =
1621 val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
1622 val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
1623 val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
1625 val is_good_head = curry (op =) (Const x) o head_of
1627 if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
1631 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
1633 (* indexname * typ -> term list -> term -> term -> term *)
1634 fun wf_constraint_for rel side concl main =
1636 val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
1637 tuple_for_args concl), Var rel)
1638 val t = List.foldl HOLogic.mk_imp core side
1639 val vars = filter (not_equal rel) (Term.add_vars t [])
1641 Library.foldl (fn (t', ((x, j), T)) =>
1643 $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
1647 (* indexname * typ -> term list * term list * term -> term *)
1648 fun wf_constraint_for_triple rel (side, main, concl) =
1649 map (wf_constraint_for rel side concl) main |> foldr1 s_conj
1651 (* Proof.context -> Time.time option -> thm
1652 -> (Proof.context -> tactic -> tactic) -> bool *)
1653 fun terminates_by ctxt timeout goal tac =
1654 can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
1655 #> SINGLE (DETERM_TIMEOUT timeout
1656 (tac ctxt (auto_tac (clasimpset_of ctxt))))
1657 #> the #> Goal.finish ctxt) goal
1659 val max_cached_wfs = 100
1660 val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
1661 val cached_wf_props : (term * bool) list Unsynchronized.ref =
1662 Unsynchronized.ref []
1664 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
1665 ScnpReconstruct.sizechange_tac]
1667 (* extended_context -> const_table -> styp -> bool *)
1668 fun uncached_is_well_founded_inductive_pred
1669 ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
1670 : extended_context) (x as (_, T)) =
1671 case def_props_for_const thy fast_descrs intro_table x of
1672 [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
1675 (case map (triple_for_intro_rule thy x) intro_ts
1676 |> filter_out (null o #2) of
1680 val binders_T = HOLogic.mk_tupleT (binder_types T)
1681 val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
1682 val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
1683 val rel = (("R", j), rel_T)
1684 val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
1685 map (wf_constraint_for_triple rel) triples
1686 |> foldr1 s_conj |> HOLogic.mk_Trueprop
1687 val _ = if debug then
1688 priority ("Wellfoundedness goal: " ^
1689 Syntax.string_of_term ctxt prop ^ ".")
1693 if tac_timeout = (!cached_timeout)
1694 andalso length (!cached_wf_props) < max_cached_wfs then
1697 (cached_wf_props := []; cached_timeout := tac_timeout);
1698 case AList.lookup (op =) (!cached_wf_props) prop of
1702 val goal = prop |> cterm_of thy |> Goal.init
1703 val wf = exists (terminates_by ctxt tac_timeout goal)
1705 in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
1707 handle List.Empty => false
1708 | NO_TRIPLE () => false
1710 (* The type constraint below is a workaround for a Poly/ML bug. *)
1712 (* extended_context -> styp -> bool *)
1713 fun is_well_founded_inductive_pred
1714 (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context)
1716 case triple_lookup (const_match thy) wfs x of
1718 | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'}
1719 orelse case AList.lookup (op =) (!wf_cache) x of
1723 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
1724 val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
1726 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
1729 (* typ list -> typ -> typ -> term -> term *)
1730 fun ap_curry [_] _ _ t = t
1731 | ap_curry arg_Ts tuple_T body_T t =
1732 let val n = length arg_Ts in
1733 list_abs (map (pair "c") arg_Ts,
1735 $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
1738 (* int -> term -> int *)
1739 fun num_occs_of_bound_in_term j (t1 $ t2) =
1740 op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
1741 | num_occs_of_bound_in_term j (Abs (s, T, t')) =
1742 num_occs_of_bound_in_term (j + 1) t'
1743 | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
1744 | num_occs_of_bound_in_term _ _ = 0
1747 val is_linear_inductive_pred_def =
1749 (* int -> term -> bool *)
1750 fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
1751 do_disjunct (j + 1) t2
1753 case num_occs_of_bound_in_term j t of
1755 | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t)
1758 fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
1759 let val (xs, body) = strip_abs t2 in
1762 | n => forall (do_disjunct (n - 1)) (disjuncts body)
1764 | do_lfp_def _ = false
1765 in do_lfp_def o strip_abs_body end
1767 (* int -> int list list *)
1768 fun n_ptuple_paths 0 = []
1769 | n_ptuple_paths 1 = []
1770 | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
1771 (* int -> typ -> typ -> term -> term *)
1772 val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
1774 (* term -> term * term *)
1775 val linear_pred_base_and_step_rhss =
1778 fun aux (Const (@{const_name lfp}, _) $ t2) =
1780 val (xs, body) = strip_abs t2
1781 val arg_Ts = map snd (tl xs)
1782 val tuple_T = HOLogic.mk_tupleT arg_Ts
1783 val j = length arg_Ts
1784 (* int -> term -> term *)
1785 fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
1786 Const (@{const_name Ex}, T1)
1787 $ Abs (s2, T2, repair_rec (j + 1) t2')
1788 | repair_rec j (@{const "op &"} $ t1 $ t2) =
1789 @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
1791 let val (head, args) = strip_comb t in
1792 if head = Bound j then
1793 HOLogic.eq_const tuple_T $ Bound j
1794 $ mk_flat_tuple tuple_T args
1798 val (nonrecs, recs) =
1799 List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
1801 val base_body = nonrecs |> List.foldl s_disj @{const False}
1802 val step_body = recs |> map (repair_rec j)
1803 |> List.foldl s_disj @{const False}
1805 (list_abs (tl xs, incr_bv (~1, j, base_body))
1806 |> ap_n_split (length arg_Ts) tuple_T bool_T,
1807 Abs ("y", tuple_T, list_abs (tl xs, step_body)
1808 |> ap_n_split (length arg_Ts) tuple_T bool_T))
1811 raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
1814 (* extended_context -> styp -> term -> term *)
1815 fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T))
1818 val j = maxidx_of_term def + 1
1819 val (outer, fp_app) = strip_abs def
1820 val outer_bounds = map Bound (length outer - 1 downto 0)
1821 val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer
1822 val fp_app = subst_bounds (rev outer_vars, fp_app)
1823 val (outer_Ts, rest_T) = strip_n_binders (length outer) T
1824 val tuple_arg_Ts = strip_type rest_T |> fst
1825 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
1826 val set_T = tuple_T --> bool_T
1827 val curried_T = tuple_T --> set_T
1828 val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
1829 val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
1830 val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
1831 val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
1832 |> HOLogic.mk_Trueprop
1833 val _ = add_simps simp_table base_s [base_eq]
1834 val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T)
1835 val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs)
1836 |> HOLogic.mk_Trueprop
1837 val _ = add_simps simp_table step_s [step_eq]
1840 Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
1841 $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
1842 $ (Const (@{const_name split}, curried_T --> uncurried_T)
1843 $ list_comb (Const step_x, outer_bounds)))
1844 $ list_comb (Const base_x, outer_bounds)
1845 |> ap_curry tuple_arg_Ts tuple_T bool_T)
1846 |> unfold_defs_in_term ext_ctxt
1849 (* extended_context -> bool -> styp -> term *)
1850 fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds,
1851 def_table, simp_table, ...})
1854 val iter_T = iterator_type_for_const gfp x
1855 val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
1856 val unrolled_const = Const x' $ zero_const iter_T
1857 val def = the (def_of_const thy def_table x)
1859 if is_equational_fun ext_ctxt x' then
1860 unrolled_const (* already done *)
1861 else if not gfp andalso is_linear_inductive_pred_def def
1862 andalso star_linear_preds then
1863 starred_linear_pred_const ext_ctxt x def
1866 val j = maxidx_of_term def + 1
1867 val (outer, fp_app) = strip_abs def
1868 val outer_bounds = map Bound (length outer - 1 downto 0)
1869 val cur = Var ((iter_var_prefix, j + 1), iter_T)
1870 val next = suc_const iter_T $ cur
1871 val rhs = case fp_app of
1873 betapply (t, list_comb (Const x', next :: outer_bounds))
1874 | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
1876 val (inner, naked_rhs) = strip_abs rhs
1877 val all = outer @ inner
1878 val bounds = map Bound (length all - 1 downto 0)
1879 val vars = map (fn (s, T) => Var ((s, j), T)) all
1880 val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs)
1881 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
1882 val _ = add_simps simp_table s' [eq]
1883 in unrolled_const end
1886 (* extended_context -> styp -> term *)
1887 fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x =
1889 val def = the (def_of_const thy def_table x)
1890 val (outer, fp_app) = strip_abs def
1891 val outer_bounds = map Bound (length outer - 1 downto 0)
1892 val rhs = case fp_app of
1893 Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
1894 | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
1896 val (inner, naked_rhs) = strip_abs rhs
1897 val all = outer @ inner
1898 val bounds = map Bound (length all - 1 downto 0)
1899 val j = maxidx_of_term def + 1
1900 val vars = map (fn (s, T) => Var ((s, j), T)) all
1902 HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
1903 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
1905 fun inductive_pred_axiom ext_ctxt (x as (s, T)) =
1906 if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
1907 let val x' = (after_name_sep s, T) in
1908 raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)]
1911 raw_inductive_pred_axiom ext_ctxt x
1913 (* extended_context -> styp -> term list *)
1914 fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
1915 psimp_table, ...}) (x as (s, _)) =
1916 case def_props_for_const thy fast_descrs (!simp_table) x of
1917 [] => (case def_props_for_const thy fast_descrs psimp_table x of
1918 [] => [inductive_pred_axiom ext_ctxt x]
1922 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
1924 (* term list -> term list *)
1925 fun merge_type_vars_in_terms ts =
1927 (* typ -> (sort * string) list -> (sort * string) list *)
1928 fun add_type (TFree (s, S)) table =
1929 (case AList.lookup (op =) table S of
1931 if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
1933 | NONE => (S, s) :: table)
1934 | add_type _ table = table
1935 val table = fold (fold_types (fold_atyps add_type)) ts []
1937 fun coalesce (TFree (s, S)) = TFree (AList.lookup (op =) table S |> the, S)
1939 in map (map_types (map_atyps coalesce)) ts end
1941 (* extended_context -> typ -> typ list -> typ list *)
1942 fun add_ground_types ext_ctxt T accum =
1944 Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum
1945 | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
1946 | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
1948 if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
1952 |> fold (add_ground_types ext_ctxt)
1953 (case boxed_datatype_constrs ext_ctxt T of
1956 | _ => insert (op =) T accum
1957 (* extended_context -> typ -> typ list *)
1958 fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T []
1959 (* extended_context -> term list -> typ list *)
1960 fun ground_types_in_terms ext_ctxt ts =
1961 fold (fold_types (add_ground_types ext_ctxt)) ts []
1963 (* typ list -> int -> term -> bool *)
1964 fun has_heavy_bounds_or_vars Ts level t =
1966 (* typ list -> bool *)
1968 | aux [T] = is_fun_type T orelse is_pair_type T
1970 in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
1972 (* typ list -> int -> int -> int -> term -> term *)
1973 fun fresh_value_var Ts k n j t =
1974 Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
1976 (* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
1977 -> term * term list *)
1978 fun pull_out_constr_comb thy Ts relax k level t args seen =
1979 let val t_comb = list_comb (t, args) in
1982 if not relax andalso is_constr thy x
1983 andalso not (is_fun_type (fastype_of1 (Ts, t_comb)))
1984 andalso has_heavy_bounds_or_vars Ts level t_comb
1985 andalso not (loose_bvar (t_comb, level)) then
1987 val (j, seen) = case find_index (curry (op =) t_comb) seen of
1988 ~1 => (0, t_comb :: seen)
1990 in (fresh_value_var Ts k (length seen) j t_comb, seen) end
1993 | _ => (t_comb, seen)
1996 (* (term -> term) -> typ list -> int -> term list -> term list *)
1997 fun equations_for_pulled_out_constrs mk_eq Ts k seen =
1998 let val n = length seen in
1999 map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
2000 (index_seq 0 n) seen
2003 (* theory -> bool -> term -> term *)
2004 fun pull_out_universal_constrs thy def t =
2006 val k = maxidx_of_term t + 1
2007 (* typ list -> bool -> term -> term list -> term list -> term * term list *)
2008 fun do_term Ts def t args seen =
2010 (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
2011 do_eq_or_imp Ts true def t0 t1 t2 seen
2012 | (t0 as @{const "==>"}) $ t1 $ t2 =>
2013 do_eq_or_imp Ts false def t0 t1 t2 seen
2014 | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
2015 do_eq_or_imp Ts true def t0 t1 t2 seen
2016 | (t0 as @{const "op -->"}) $ t1 $ t2 =>
2017 do_eq_or_imp Ts false def t0 t1 t2 seen
2019 let val (t', seen) = do_term (T :: Ts) def t' [] seen in
2020 (list_comb (Abs (s, T, t'), args), seen)
2023 let val (t2, seen) = do_term Ts def t2 [] seen in
2024 do_term Ts def t1 (t2 :: args) seen
2026 | _ => pull_out_constr_comb thy Ts def k 0 t args seen
2027 (* typ list -> bool -> bool -> term -> term -> term -> term list
2028 -> term * term list *)
2029 and do_eq_or_imp Ts eq def t0 t1 t2 seen =
2031 val (t2, seen) = if eq andalso def then (t2, seen)
2032 else do_term Ts false t2 [] seen
2033 val (t1, seen) = do_term Ts false t1 [] seen
2034 in (t0 $ t1 $ t2, seen) end
2035 val (concl, seen) = do_term [] def t [] []
2037 Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
2041 (* extended_context -> bool -> term -> term *)
2042 fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
2045 val num_occs_of_var =
2046 fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
2048 (* bool -> term -> term *)
2049 fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
2050 aux_eq careful true t0 t1 t2
2051 | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
2052 t0 $ aux false t1 $ aux careful t2
2053 | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
2054 aux_eq careful true t0 t1 t2
2055 | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
2056 t0 $ aux false t1 $ aux careful t2
2057 | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
2058 | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
2060 (* bool -> bool -> term -> term -> term -> term *)
2061 and aux_eq careful pass1 t0 t1 t2 =
2064 else if axiom andalso is_Var t2
2065 andalso num_occs_of_var (dest_Var t2) = 1 then
2067 else case strip_comb t2 of
2068 (Const (x as (s, T)), args) =>
2069 let val arg_Ts = binder_types T in
2070 if length arg_Ts = length args
2071 andalso (is_constr thy x orelse s = @{const_name Pair}
2072 orelse x = (@{const_name Suc}, nat_T --> nat_T))
2073 andalso (not careful orelse not (is_Var t1)
2074 orelse String.isPrefix val_var_prefix
2075 (fst (fst (dest_Var t1)))) then
2076 discriminate_value ext_ctxt x t1 ::
2077 map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
2079 |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
2083 | _ => raise SAME ())
2084 handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
2085 else t0 $ aux false t2 $ aux false t1
2086 (* styp -> term -> int -> typ -> term -> term *)
2087 and sel_eq x t n nth_T nth_t =
2088 HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
2092 (* theory -> term -> term *)
2093 fun simplify_constrs_and_sels thy t =
2095 (* term -> int -> term *)
2096 fun is_nth_sel_on t' n (Const (s, _) $ t) =
2097 (t = t' andalso is_sel_like_and_no_discr s
2098 andalso sel_no_from_name s = n)
2099 | is_nth_sel_on _ _ _ = false
2100 (* term -> term list -> term *)
2101 fun do_term (Const (@{const_name Rep_Frac}, _)
2102 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
2103 | do_term (Const (@{const_name Abs_Frac}, _)
2104 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
2105 | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
2106 | do_term (t as Const (x as (s, T))) (args as _ :: _) =
2107 ((if is_constr_like thy x then
2108 if length args = num_binder_types T then
2110 Const (x' as (_, T')) $ t' =>
2111 if domain_type T' = body_type T
2112 andalso forall (uncurry (is_nth_sel_on t'))
2113 (index_seq 0 (length args) ~~ args) then
2117 | _ => raise SAME ()
2120 else if is_sel_like_and_no_discr s then
2121 case strip_comb (hd args) of
2122 (Const (x' as (s', T')), ts') =>
2123 if is_constr_like thy x'
2124 andalso constr_name_for_sel_like s = s'
2125 andalso not (exists is_pair_type (binder_types T')) then
2126 list_comb (nth ts' (sel_no_from_name s), tl args)
2129 | _ => raise SAME ()
2132 handle SAME () => betapplys (t, args))
2133 | do_term (Abs (s, T, t')) args =
2134 betapplys (Abs (s, T, do_term t' []), args)
2135 | do_term t args = betapplys (t, args)
2139 fun curry_assms (@{const "==>"} $ (@{const Trueprop}
2140 $ (@{const "op &"} $ t1 $ t2)) $ t3) =
2141 curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
2142 | curry_assms (@{const "==>"} $ t1 $ t2) =
2143 @{const "==>"} $ curry_assms t1 $ curry_assms t2
2147 val destroy_universal_equalities =
2149 (* term list -> (indexname * typ) list -> term -> term *)
2150 fun aux prems zs t =
2152 @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
2153 | _ => Logic.list_implies (rev prems, t)
2154 (* term list -> (indexname * typ) list -> term -> term -> term *)
2155 and aux_implies prems zs t1 t2 =
2157 Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
2158 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
2159 aux_eq prems zs z t' t1 t2
2160 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
2161 aux_eq prems zs z t' t1 t2
2162 | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
2163 (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
2165 and aux_eq prems zs z t' t1 t2 =
2166 if not (member (op =) zs z)
2167 andalso not (exists_subterm (curry (op =) (Var z)) t') then
2168 aux prems zs (subst_free [(Var z, t')] t2)
2170 aux (t1 :: prems) (Term.add_vars t1 zs) t2
2173 (* theory -> term -> term *)
2174 fun pull_out_existential_constrs thy t =
2176 val k = maxidx_of_term t + 1
2177 (* typ list -> int -> term -> term list -> term list -> term * term list *)
2178 fun aux Ts num_exists t args seen =
2180 (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
2182 val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
2183 val n = length seen'
2184 (* unit -> term list *)
2185 fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
2187 (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
2188 |> List.foldl s_conj t1 |> fold mk_exists (vars ())
2189 |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
2192 let val (t2, seen) = aux Ts num_exists t2 [] seen in
2193 aux Ts num_exists t1 (t2 :: args) seen
2197 val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
2198 in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
2200 if num_exists > 0 then
2201 pull_out_constr_comb thy Ts false k num_exists t args seen
2203 (list_comb (t, args), seen)
2204 in aux [] 0 t [] [] |> fst end
2206 (* theory -> int -> term list -> term list -> (term * term list) option *)
2207 fun find_bound_assign _ _ _ [] = NONE
2208 | find_bound_assign thy j seen (t :: ts) =
2210 (* bool -> term -> term -> (term * term list) option *)
2211 fun aux pass1 t1 t2 =
2212 (if loose_bvar1 (t2, j) then
2213 if pass1 then aux false t2 t1 else raise SAME ()
2215 Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
2216 | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
2217 if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then
2218 SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
2222 | _ => raise SAME ())
2223 handle SAME () => find_bound_assign thy j (t :: seen) ts
2226 Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
2227 | _ => find_bound_assign thy j (t :: seen) ts
2230 (* int -> term -> term -> term *)
2231 fun subst_one_bound j arg t =
2233 fun aux (Bound i, lev) =
2234 if i < lev then raise SAME ()
2235 else if i = lev then incr_boundvars (lev - j) arg
2237 | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
2238 | aux (f $ t, lev) =
2239 (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
2240 handle SAME () => f $ aux (t, lev))
2241 | aux _ = raise SAME ()
2242 in aux (t, j) handle SAME () => t end
2244 (* theory -> term -> term *)
2245 fun destroy_existential_equalities thy =
2247 (* string list -> typ list -> term list -> term *)
2248 fun kill [] [] ts = foldr1 s_conj ts
2249 | kill (s :: ss) (T :: Ts) ts =
2250 (case find_bound_assign thy (length ss) [] ts of
2251 SOME (_, []) => @{const True}
2252 | SOME (arg_t, ts) =>
2253 kill ss Ts (map (subst_one_bound (length ss)
2254 (incr_bv (~1, length ss + 1, arg_t))) ts)
2256 Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
2257 $ Abs (s, T, kill ss Ts ts))
2258 | kill _ _ _ = raise UnequalLengths
2259 (* string list -> typ list -> term -> term *)
2260 fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
2261 gather (ss @ [s1]) (Ts @ [T1]) t1
2262 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
2263 | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
2264 | gather [] [] t = t
2265 | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t))
2269 fun distribute_quantifiers t =
2271 (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
2273 (t10 as @{const "op &"}) $ t11 $ t12 =>
2274 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
2275 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
2276 | (t10 as @{const Not}) $ t11 =>
2277 t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
2280 if not (loose_bvar1 (t1, 0)) then
2281 distribute_quantifiers (incr_boundvars ~1 t1)
2283 t0 $ Abs (s, T1, distribute_quantifiers t1))
2284 | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
2285 (case distribute_quantifiers t1 of
2286 (t10 as @{const "op |"}) $ t11 $ t12 =>
2287 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
2288 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
2289 | (t10 as @{const "op -->"}) $ t11 $ t12 =>
2290 t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
2292 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
2293 | (t10 as @{const Not}) $ t11 =>
2294 t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
2297 if not (loose_bvar1 (t1, 0)) then
2298 distribute_quantifiers (incr_boundvars ~1 t1)
2300 t0 $ Abs (s, T1, distribute_quantifiers t1))
2301 | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
2302 | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
2305 (* int -> int -> (int -> int) -> term -> term *)
2306 fun renumber_bounds j n f t =
2308 t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
2309 | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
2311 Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
2314 val quantifier_cluster_max_size = 8
2316 (* theory -> term -> term *)
2317 fun push_quantifiers_inward thy =
2319 (* string -> string list -> typ list -> term -> term *)
2320 fun aux quant_s ss Ts t =
2322 (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
2323 if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
2324 aux s0 (s1 :: ss) (T1 :: Ts) t1
2325 else if quant_s = "" andalso (s0 = @{const_name All}
2326 orelse s0 = @{const_name Ex}) then
2330 | _ => raise SAME ())
2334 if quant_s = "" then
2335 aux "" [] [] t1 $ aux "" [] [] t2
2338 val typical_card = 4
2339 (* ('a -> ''b list) -> 'a list -> ''b list *)
2340 fun big_union proj ps =
2341 fold (fold (insert (op =)) o proj) ps []
2342 val (ts, connective) = strip_any_connective t
2344 map (bounded_card_of_type 65536 typical_card []) Ts
2345 val t_costs = map size_of_term ts
2346 val num_Ts = length Ts
2348 val flip = curry (op -) (num_Ts - 1)
2349 val t_boundss = map (map flip o loose_bnos) ts
2350 (* (int list * int) list -> int list -> int *)
2351 fun cost boundss_cum_costs [] =
2352 map snd boundss_cum_costs |> Integer.sum
2353 | cost boundss_cum_costs (j :: js) =
2356 List.partition (fn (bounds, _) =>
2357 member (op =) bounds j)
2359 val yeas_bounds = big_union fst yeas
2360 val yeas_cost = Integer.sum (map snd yeas)
2362 in cost ((yeas_bounds, yeas_cost) :: nays) js end
2363 val js = all_permutations (index_seq 0 num_Ts)
2364 |> map (`(cost (t_boundss ~~ t_costs)))
2365 |> sort (int_ord o pairself fst) |> hd |> snd
2366 val back_js = map (fn j => find_index (curry (op =) j) js)
2367 (index_seq 0 num_Ts)
2368 val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
2370 (* (term * int list) list -> term *)
2371 fun mk_connection [] =
2372 raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
2373 \mk_connection", "")
2374 | mk_connection ts_cum_bounds =
2375 ts_cum_bounds |> map fst
2376 |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
2377 (* (term * int list) list -> int list -> term *)
2378 fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
2379 | build ts_cum_bounds (j :: js) =
2382 List.partition (fn (_, bounds) =>
2383 member (op =) bounds j)
2385 ||> map (apfst (incr_boundvars ~1))
2390 let val T = nth Ts (flip j) in
2391 build ((Const (quant_s, (T --> bool_T) --> bool_T)
2392 $ Abs (nth ss (flip j), T,
2393 mk_connection yeas),
2394 big_union snd yeas) :: nays) js
2397 in build (ts ~~ t_boundss) js end
2398 | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
2402 (* polarity -> string -> bool *)
2403 fun is_positive_existential polar quant_s =
2404 (polar = Pos andalso quant_s = @{const_name Ex})
2405 orelse (polar = Neg andalso quant_s <> @{const_name Ex})
2407 (* extended_context -> int -> term -> term *)
2408 fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
2411 (* int list -> int list *)
2412 val incrs = map (Integer.add 1)
2413 (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
2414 fun aux ss Ts js depth polar t =
2416 (* string -> typ -> string -> typ -> term -> term *)
2417 fun do_quantifier quant_s quant_T abs_s abs_T t =
2418 if not (loose_bvar1 (t, 0)) then
2419 aux ss Ts js depth polar (incr_boundvars ~1 t)
2420 else if depth <= skolem_depth
2421 andalso is_positive_existential polar quant_s then
2423 val j = length (!skolems) + 1
2424 val sko_s = skolem_prefix_for (length js) j ^ abs_s
2425 val _ = Unsynchronized.change skolems (cons (sko_s, ss))
2426 val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
2428 val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
2430 if null js then betapply (abs_t, sko_t)
2431 else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
2434 Const (quant_s, quant_T)
2435 $ Abs (abs_s, abs_T,
2436 if is_higher_order_type abs_T then
2439 aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
2440 (depth + 1) polar t)
2443 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
2444 do_quantifier s0 T0 s1 T1 t1
2445 | @{const "==>"} $ t1 $ t2 =>
2446 @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
2447 $ aux ss Ts js depth polar t2
2448 | @{const Pure.conjunction} $ t1 $ t2 =>
2449 @{const Pure.conjunction} $ aux ss Ts js depth polar t1
2450 $ aux ss Ts js depth polar t2
2451 | @{const Trueprop} $ t1 =>
2452 @{const Trueprop} $ aux ss Ts js depth polar t1
2453 | @{const Not} $ t1 =>
2454 @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
2455 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
2456 do_quantifier s0 T0 s1 T1 t1
2457 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
2458 do_quantifier s0 T0 s1 T1 t1
2459 | @{const "op &"} $ t1 $ t2 =>
2460 @{const "op &"} $ aux ss Ts js depth polar t1
2461 $ aux ss Ts js depth polar t2
2462 | @{const "op |"} $ t1 $ t2 =>
2463 @{const "op |"} $ aux ss Ts js depth polar t1
2464 $ aux ss Ts js depth polar t2
2465 | @{const "op -->"} $ t1 $ t2 =>
2466 @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
2467 $ aux ss Ts js depth polar t2
2468 | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
2469 t0 $ t1 $ aux ss Ts js depth polar t2
2470 | Const (x as (s, T)) =>
2471 if is_inductive_pred ext_ctxt x
2472 andalso not (is_well_founded_inductive_pred ext_ctxt x) then
2474 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
2475 val (pref, connective, set_oper) =
2479 @{const_name upper_semilattice_fun_inst.sup_fun})
2483 @{const_name lower_semilattice_fun_inst.inf_fun})
2485 fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x
2486 |> aux ss Ts js depth polar
2487 fun neg () = Const (pref ^ s, T)
2489 (case polar |> gfp ? flip_polarity of
2493 if is_fun_type T then
2495 val ((trunk_arg_Ts, rump_arg_T), body_T) =
2496 T |> strip_type |>> split_last
2497 val set_T = rump_arg_T --> body_T
2498 (* (unit -> term) -> term *)
2501 map Bound (length trunk_arg_Ts - 1 downto 0))
2504 (Const (set_oper, set_T --> set_T --> set_T)
2505 $ app pos $ app neg) trunk_arg_Ts
2508 connective $ pos () $ neg ())
2513 betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
2514 aux ss Ts [] depth Neut t2)
2515 | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
2518 in aux [] [] [] 0 Pos end
2520 (* extended_context -> styp -> (int * term option) list *)
2521 fun static_args_in_term ({ersatz_table, ...} : extended_context) x t =
2523 (* term -> term list -> term list -> term list list *)
2524 fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
2525 | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
2526 | fun_calls t args =
2528 Const (x' as (s', T')) =>
2529 x = x' orelse (case AList.lookup (op =) ersatz_table s' of
2530 SOME s'' => x = (s'', T')
2532 | _ => false) ? cons args
2533 (* term list list -> term list list -> term list -> term list list *)
2534 fun call_sets [] [] vs = [vs]
2535 | call_sets [] uss vs = vs :: call_sets uss [] []
2536 | call_sets ([] :: _) _ _ = []
2537 | call_sets ((t :: ts) :: tss) uss vs =
2538 OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
2539 val sets = call_sets (fun_calls t [] []) [] []
2540 val indexed_sets = sets ~~ (index_seq 0 (length sets))
2542 fold_rev (fn (set, j) =>
2544 [Var _] => AList.lookup (op =) indexed_sets set = SOME j
2546 | [t as Const _] => cons (j, SOME t)
2547 | [t as Free _] => cons (j, SOME t)
2548 | _ => I) indexed_sets []
2550 (* extended_context -> styp -> term list -> (int * term option) list *)
2551 fun static_args_in_terms ext_ctxt x =
2552 map (static_args_in_term ext_ctxt x)
2553 #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
2555 (* term -> term list *)
2556 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
2557 | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
2558 | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
2560 | params_in_equation _ = []
2562 (* styp -> styp -> int list -> term list -> term list -> term -> term *)
2563 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
2565 val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
2567 val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
2568 val fixed_params = filter_indices fixed_js (params_in_equation t)
2569 (* term list -> term -> term *)
2570 fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
2571 | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
2574 list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
2576 let val j = find_index (curry (op =) t) fixed_params in
2577 list_comb (if j >= 0 then nth fixed_args j else t, args)
2581 (* typ list -> term -> bool *)
2582 fun is_eligible_arg Ts t =
2583 let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
2585 orelse (is_higher_order_type (fastype_of1 (Ts, t))
2586 andalso forall (not o is_higher_order_type) bad_Ts)
2589 (* (int * term option) list -> (int * term) list -> int list *)
2590 fun overlapping_indices [] _ = []
2591 | overlapping_indices _ [] = []
2592 | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
2593 if j1 < j2 then overlapping_indices ps1' ps2
2594 else if j1 > j2 then overlapping_indices ps1 ps2'
2595 else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
2597 val special_depth = 20
2599 (* extended_context -> int -> term -> term *)
2600 fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table,
2601 special_funs, ...}) depth t =
2602 if not specialize orelse depth > special_depth then
2606 val blacklist = if depth = 0 then []
2607 else case term_under_def t of Const x => [x] | _ => []
2608 (* term list -> typ list -> term -> term *)
2609 fun aux args Ts (Const (x as (s, T))) =
2610 ((if not (member (op =) blacklist x) andalso not (null args)
2611 andalso not (String.isPrefix special_prefix s)
2612 andalso is_equational_fun ext_ctxt x then
2614 val eligible_args = filter (is_eligible_arg Ts o snd)
2615 (index_seq 0 (length args) ~~ args)
2616 val _ = not (null eligible_args) orelse raise SAME ()
2617 val old_axs = equational_fun_axioms ext_ctxt x
2618 |> map (destroy_existential_equalities thy)
2619 val static_params = static_args_in_terms ext_ctxt x old_axs
2620 val fixed_js = overlapping_indices static_params eligible_args
2621 val _ = not (null fixed_js) orelse raise SAME ()
2622 val fixed_args = filter_indices fixed_js args
2623 val vars = fold Term.add_vars fixed_args []
2624 |> sort (TermOrd.fast_indexname_ord o pairself fst)
2625 val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
2628 val live_args = filter_out_indices fixed_js args
2629 val extra_args = map Var vars @ map Bound bound_js @ live_args
2630 val extra_Ts = map snd vars @ filter_indices bound_js Ts
2631 val k = maxidx_of_term t + 1
2633 fun var_for_bound_no j =
2634 Var ((bound_var_prefix ^
2635 nat_subscript (find_index (curry (op =) j) bound_js
2638 val fixed_args_in_axiom =
2639 map (curry subst_bounds
2640 (map var_for_bound_no (index_seq 0 (length Ts))))
2643 case AList.lookup (op =) (!special_funs)
2644 (x, fixed_js, fixed_args_in_axiom) of
2645 SOME x' => list_comb (Const x', extra_args)
2648 val extra_args_in_axiom =
2649 map Var vars @ map var_for_bound_no bound_js
2651 (special_prefix_for (length (!special_funs) + 1) ^ s,
2652 extra_Ts @ filter_out_indices fixed_js (binder_types T)
2655 map (specialize_fun_axiom x x' fixed_js
2656 fixed_args_in_axiom extra_args_in_axiom) old_axs
2658 Unsynchronized.change special_funs
2659 (cons ((x, fixed_js, fixed_args_in_axiom), x'))
2660 val _ = add_simps simp_table s' new_axs
2661 in list_comb (Const x', extra_args) end
2665 handle SAME () => list_comb (Const x, args))
2666 | aux args Ts (Abs (s, T, t)) =
2667 list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
2668 | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
2669 | aux args _ t = list_comb (t, args)
2672 (* theory -> term -> int Termtab.tab -> int Termtab.tab *)
2673 fun add_to_uncurry_table thy t =
2675 (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
2676 fun aux (t1 $ t2) args table =
2677 let val table = aux t2 [] table in aux t1 (t2 :: args) table end
2678 | aux (Abs (_, _, t')) _ table = aux t' [] table
2679 | aux (t as Const (x as (s, _))) args table =
2680 if is_built_in_const true x orelse is_constr_like thy x orelse is_sel s
2681 orelse s = @{const_name Sigma} then
2684 Termtab.map_default (t, 65536) (curry Int.min (length args)) table
2685 | aux _ _ table = table
2688 (* int Termtab.tab term -> term *)
2689 fun uncurry_term table t =
2691 (* term -> term list -> term *)
2692 fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
2693 | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
2694 | aux (t as Const (s, T)) args =
2695 (case Termtab.lookup table t of
2699 val (arg_Ts, rest_T) = strip_n_binders n T
2701 if hd arg_Ts = @{typ bisim_iterator}
2702 orelse is_fp_iterator_type (hd arg_Ts) then
2704 else case find_index (not_equal bool_T) arg_Ts of
2707 val ((before_args, tuple_args), after_args) =
2708 args |> chop n |>> chop j
2709 val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
2710 T |> strip_n_binders n |>> chop j
2711 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
2716 betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
2717 before_arg_Ts ---> tuple_T --> rest_T),
2718 before_args @ [mk_flat_tuple tuple_T tuple_args] @
2723 | NONE => betapplys (t, args))
2724 | aux t args = betapplys (t, args)
2727 (* (term -> term) -> int -> term -> term *)
2728 fun coerce_bound_no f j t =
2730 t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
2731 | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
2732 | Bound j' => if j' = j then f t else t
2735 (* extended_context -> bool -> term -> term *)
2736 fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t =
2739 fun box_relational_operator_type (Type ("fun", Ts)) =
2740 Type ("fun", map box_relational_operator_type Ts)
2741 | box_relational_operator_type (Type ("*", Ts)) =
2742 Type ("*", map (box_type ext_ctxt InPair) Ts)
2743 | box_relational_operator_type T = T
2744 (* typ -> typ -> term -> term *)
2745 fun coerce_bound_0_in_term new_T old_T =
2746 old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
2747 (* typ list -> typ -> term -> term *)
2748 and coerce_term Ts new_T old_T t =
2749 if old_T = new_T then
2752 case (new_T, old_T) of
2753 (Type (new_s, new_Ts as [new_T1, new_T2]),
2754 Type ("fun", [old_T1, old_T2])) =>
2755 (case eta_expand Ts t 1 of
2758 t' |> coerce_bound_0_in_term new_T1 old_T1
2759 |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
2760 |> Envir.eta_contract
2762 ? construct_value thy (@{const_name FunBox},
2763 Type ("fun", new_Ts) --> new_T) o single
2764 | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
2765 \coerce_term", [t']))
2766 | (Type (new_s, new_Ts as [new_T1, new_T2]),
2767 Type (old_s, old_Ts as [old_T1, old_T2])) =>
2768 if old_s = @{type_name fun_box} orelse old_s = @{type_name pair_box}
2769 orelse old_s = "*" then
2770 case constr_expand ext_ctxt old_T t of
2771 Const (@{const_name FunBox}, _) $ t1 =>
2772 if new_s = "fun" then
2773 coerce_term Ts new_T (Type ("fun", old_Ts)) t1
2776 (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
2777 [coerce_term Ts (Type ("fun", new_Ts))
2778 (Type ("fun", old_Ts)) t1]
2779 | Const _ $ t1 $ t2 =>
2781 (if new_s = "*" then @{const_name Pair}
2782 else @{const_name PairBox}, new_Ts ---> new_T)
2783 [coerce_term Ts new_T1 old_T1 t1,
2784 coerce_term Ts new_T2 old_T2 t2]
2785 | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
2786 \coerce_term", [t'])
2788 raise TYPE ("coerce_term", [new_T, old_T], [t])
2789 | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
2790 (* indexname * typ -> typ * term -> typ option list -> typ option list *)
2791 fun add_boxed_types_for_var (z as (_, T)) (T', t') =
2793 Var z' => z' = z ? insert (op =) T'
2794 | Const (@{const_name Pair}, _) $ t1 $ t2 =>
2796 Type (_, [T1, T2]) =>
2797 fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
2798 | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
2799 \add_boxed_types_for_var", [T'], []))
2800 | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
2801 (* typ list -> typ list -> term -> indexname * typ -> typ *)
2802 fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
2804 @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
2805 | Const (s0, _) $ t1 $ _ =>
2806 if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
2808 val (t', args) = strip_comb t1
2809 val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
2811 case fold (add_boxed_types_for_var z)
2812 (fst (strip_n_binders (length args) T') ~~ args) [] of
2819 (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
2821 and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
2824 if polar = Neut orelse is_positive_existential polar quant_s then
2825 box_type ext_ctxt InFunLHS abs_T
2828 val body_T = body_type quant_T
2830 Const (quant_s, (abs_T' --> body_T) --> body_T)
2831 $ Abs (abs_s, abs_T',
2832 t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
2834 (* typ list -> typ list -> string -> typ -> term -> term -> term *)
2835 and do_equals new_Ts old_Ts s0 T0 t1 t2 =
2837 val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
2838 val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
2839 val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
2841 list_comb (Const (s0, T --> T --> body_type T0),
2842 map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
2844 (* string -> typ -> term *)
2845 and do_description_operator s T =
2846 let val T1 = box_type ext_ctxt InFunLHS (range_type T) in
2847 Const (s, (T1 --> bool_T) --> T1)
2849 (* typ list -> typ list -> polarity -> term -> term *)
2850 and do_term new_Ts old_Ts polar t =
2852 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
2853 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
2854 | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
2855 do_equals new_Ts old_Ts s0 T0 t1 t2
2856 | @{const "==>"} $ t1 $ t2 =>
2857 @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
2858 $ do_term new_Ts old_Ts polar t2
2859 | @{const Pure.conjunction} $ t1 $ t2 =>
2860 @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
2861 $ do_term new_Ts old_Ts polar t2
2862 | @{const Trueprop} $ t1 =>
2863 @{const Trueprop} $ do_term new_Ts old_Ts polar t1
2864 | @{const Not} $ t1 =>
2865 @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
2866 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
2867 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
2868 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
2869 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
2870 | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
2871 do_equals new_Ts old_Ts s0 T0 t1 t2
2872 | @{const "op &"} $ t1 $ t2 =>
2873 @{const "op &"} $ do_term new_Ts old_Ts polar t1
2874 $ do_term new_Ts old_Ts polar t2
2875 | @{const "op |"} $ t1 $ t2 =>
2876 @{const "op |"} $ do_term new_Ts old_Ts polar t1
2877 $ do_term new_Ts old_Ts polar t2
2878 | @{const "op -->"} $ t1 $ t2 =>
2879 @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
2880 $ do_term new_Ts old_Ts polar t2
2881 | Const (s as @{const_name The}, T) => do_description_operator s T
2882 | Const (s as @{const_name Eps}, T) => do_description_operator s T
2883 | Const (s as @{const_name Tha}, T) => do_description_operator s T
2884 | Const (x as (s, T)) =>
2885 Const (s, if s = @{const_name converse}
2886 orelse s = @{const_name trancl} then
2887 box_relational_operator_type T
2888 else if is_built_in_const fast_descrs x
2889 orelse s = @{const_name Sigma} then
2891 else if is_constr_like thy x then
2892 box_type ext_ctxt InConstr T
2893 else if is_sel s orelse is_rep_fun thy x then
2894 box_type ext_ctxt InSel T
2896 box_type ext_ctxt InExpr T)
2897 | t1 $ Abs (s, T, t2') =>
2899 val t1 = do_term new_Ts old_Ts Neut t1
2900 val T1 = fastype_of1 (new_Ts, t1)
2901 val (s1, Ts1) = dest_Type T1
2902 val T' = hd (snd (dest_Type (hd Ts1)))
2903 val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
2904 val T2 = fastype_of1 (new_Ts, t2)
2905 val t2 = coerce_term new_Ts (hd Ts1) T2 t2
2907 betapply (if s1 = "fun" then
2910 select_nth_constr_arg thy
2911 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
2912 (Type ("fun", Ts1)), t2)
2916 val t1 = do_term new_Ts old_Ts Neut t1
2917 val T1 = fastype_of1 (new_Ts, t1)
2918 val (s1, Ts1) = dest_Type T1
2919 val t2 = do_term new_Ts old_Ts Neut t2
2920 val T2 = fastype_of1 (new_Ts, t2)
2921 val t2 = coerce_term new_Ts (hd Ts1) T2 t2
2923 betapply (if s1 = "fun" then
2926 select_nth_constr_arg thy
2927 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
2928 (Type ("fun", Ts1)), t2)
2930 | Free (s, T) => Free (s, box_type ext_ctxt InExpr T)
2931 | Var (z as (x, T)) =>
2932 Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
2933 else box_type ext_ctxt InExpr T)
2936 Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
2937 in do_term [] [] Pos orig_t end
2939 (* int -> term -> term *)
2940 fun eval_axiom_for_term j t =
2941 Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
2943 (* extended_context -> styp -> bool *)
2944 fun is_equational_fun_surely_complete ext_ctxt x =
2945 case raw_equational_fun_axioms ext_ctxt x of
2946 [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
2947 strip_comb t1 |> snd |> forall is_Var
2950 type special = int list * term list * styp
2952 (* styp -> special -> special -> term *)
2953 fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
2955 val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
2956 val Ts = binder_types T
2957 val max_j = fold (fold Integer.max) [js1, js2] ~1
2958 val (eqs, (args1, args2)) =
2959 fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
2960 (js1 ~~ ts1, js2 ~~ ts2) of
2961 (SOME t1, SOME t2) => apfst (cons (t1, t2))
2962 | (SOME t1, NONE) => apsnd (apsnd (cons t1))
2963 | (NONE, SOME t2) => apsnd (apfst (cons t2))
2965 let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
2967 apsnd (pairself (cons v))
2968 end) (max_j downto 0) ([], ([], []))
2970 Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
2971 |> map Logic.mk_equals,
2972 Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
2973 list_comb (Const x2, bounds2 @ args2)))
2974 |> Refute.close_form
2977 (* extended_context -> styp list -> term list *)
2978 fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs =
2982 |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
2983 |> AList.group (op =)
2984 |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
2985 |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
2986 (* special -> int *)
2987 fun generality (js, _, _) = ~(length js)
2988 (* special -> special -> bool *)
2989 fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
2990 x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
2991 (j2 ~~ t2, j1 ~~ t1)
2992 (* styp -> special list -> special list -> special list -> term list
2994 fun do_pass_1 _ [] [_] [_] = I
2995 | do_pass_1 x skipped _ [] = do_pass_2 x skipped
2996 | do_pass_1 x skipped all (z :: zs) =
2997 case filter (is_more_specific z) all
2998 |> sort (int_ord o pairself generality) of
2999 [] => do_pass_1 x (z :: skipped) all zs
3000 | (z' :: _) => cons (special_congruence_axiom x z z')
3001 #> do_pass_1 x skipped all zs
3002 (* styp -> special list -> term list -> term list *)
3003 and do_pass_2 _ [] = I
3004 | do_pass_2 x (z :: zs) =
3005 fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
3006 in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
3009 val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
3011 (* 'a Symtab.table -> 'a list *)
3012 fun all_table_entries table = Symtab.fold (append o snd) table []
3013 (* const_table -> string -> const_table *)
3014 fun extra_table table s = Symtab.make [(s, all_table_entries table)]
3016 (* extended_context -> term -> (term list * term list) * (bool * bool) *)
3018 (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
3019 def_table, nondef_table, user_nondefs, ...}) t =
3021 type accumulator = styp list * (term list * term list)
3022 (* (term list * term list -> term list)
3023 -> ((term list -> term list) -> term list * term list
3024 -> term list * term list)
3025 -> int -> term -> accumulator -> accumulator *)
3026 fun add_axiom get app depth t (accum as (xs, axs)) =
3028 val t = t |> unfold_defs_in_term ext_ctxt
3029 |> skolemize_term_and_more ext_ctxt ~1
3031 if is_trivial_equation t then
3034 let val t' = t |> specialize_consts_in_term ext_ctxt depth in
3035 if exists (member (op aconv) (get axs)) [t, t'] then accum
3036 else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
3039 (* int -> term -> accumulator -> accumulator *)
3040 and add_def_axiom depth = add_axiom fst apfst depth
3041 and add_nondef_axiom depth = add_axiom snd apsnd depth
3042 and add_maybe_def_axiom depth t =
3043 (if head_of t <> @{const "==>"} then add_def_axiom
3044 else add_nondef_axiom) depth t
3045 and add_eq_axiom depth t =
3046 (if is_constr_pattern_formula thy t then add_def_axiom
3047 else add_nondef_axiom) depth t
3048 (* int -> term -> accumulator -> accumulator *)
3049 and add_axioms_for_term depth t (accum as (xs, axs)) =
3051 t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
3052 | Const (x as (s, T)) =>
3053 (if member (op =) xs x orelse is_built_in_const fast_descrs x then
3056 let val accum as (xs, _) = (x :: xs, axs) in
3057 if depth > axioms_max_depth then
3058 raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\
3059 \add_axioms_for_term",
3060 "too many nested axioms (" ^
3061 string_of_int depth ^ ")")
3062 else if Refute.is_const_of_class thy x then
3064 val class = Logic.class_of_const s
3065 val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
3067 val ax1 = try (Refute.specialize_type thy x) of_class
3068 val ax2 = Option.map (Refute.specialize_type thy x o snd)
3069 (Refute.get_classdef thy class)
3071 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
3074 else if is_constr thy x then
3076 else if is_equational_fun ext_ctxt x then
3077 fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
3079 else if is_abs_fun thy x then
3080 accum |> fold (add_nondef_axiom depth)
3081 (nondef_props_for_const thy false nondef_table x)
3082 |> is_funky_typedef thy (range_type T)
3083 ? fold (add_maybe_def_axiom depth)
3084 (nondef_props_for_const thy true
3085 (extra_table def_table s) x)
3086 else if is_rep_fun thy x then
3087 accum |> fold (add_nondef_axiom depth)
3088 (nondef_props_for_const thy false nondef_table x)
3089 |> is_funky_typedef thy (range_type T)
3090 ? fold (add_maybe_def_axiom depth)
3091 (nondef_props_for_const thy true
3092 (extra_table def_table s) x)
3093 |> add_axioms_for_term depth
3094 (Const (mate_of_rep_fun thy x))
3095 |> fold (add_def_axiom depth)
3096 (inverse_axioms_for_rep_fun thy x)
3098 accum |> user_axioms <> SOME false
3099 ? fold (add_nondef_axiom depth)
3100 (nondef_props_for_const thy false nondef_table x)
3102 |> add_axioms_for_type depth T
3103 | Free (_, T) => add_axioms_for_type depth T accum
3104 | Var (_, T) => add_axioms_for_type depth T accum
3106 | Abs (_, T, t) => accum |> add_axioms_for_term depth t
3107 |> add_axioms_for_type depth T
3108 (* int -> typ -> accumulator -> accumulator *)
3109 and add_axioms_for_type depth T =
3111 Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
3112 | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
3116 | TFree (_, S) => add_axioms_for_sort depth T S
3117 | TVar (_, S) => add_axioms_for_sort depth T S
3118 | Type (z as (_, Ts)) =>
3119 fold (add_axioms_for_type depth) Ts
3120 #> (if is_pure_typedef thy T then
3121 fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
3122 else if max_bisim_depth >= 0 andalso is_codatatype thy T then
3123 fold (add_maybe_def_axiom depth)
3124 (codatatype_bisim_axioms ext_ctxt T)
3127 (* int -> typ -> sort -> accumulator -> accumulator *)
3128 and add_axioms_for_sort depth T S =
3130 val supers = Sign.complete_sort thy S
3132 maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
3133 handle ERROR _ => [])) supers
3134 val monomorphic_class_axioms =
3135 map (fn t => case Term.add_tvars t [] of
3138 Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
3139 | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
3140 \add_axioms_for_sort", [t]))
3142 in fold (add_nondef_axiom depth) monomorphic_class_axioms end
3143 val (mono_user_nondefs, poly_user_nondefs) =
3144 List.partition (null o Term.hidden_polymorphism) user_nondefs
3145 val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
3147 val (xs, (defs, nondefs)) =
3148 ([], ([], [])) |> add_axioms_for_term 1 t
3149 |> fold_rev (add_def_axiom 1) eval_axioms
3150 |> user_axioms = SOME true
3151 ? fold (add_nondef_axiom 1) mono_user_nondefs
3152 val defs = defs @ special_congruence_axioms ext_ctxt xs
3154 ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
3155 null poly_user_nondefs))
3158 (* theory -> const_table -> styp -> int list *)
3159 fun const_format thy def_table (x as (s, T)) =
3160 if String.isPrefix unrolled_prefix s then
3161 const_format thy def_table (original_name s, range_type T)
3162 else if String.isPrefix skolem_prefix s then
3164 val k = unprefix skolem_prefix s
3165 |> strip_first_name_sep |> fst |> space_explode "@"
3166 |> hd |> Int.fromString |> the
3167 in [k, num_binder_types T - k] end
3168 else if original_name s <> s then
3169 [num_binder_types T]
3170 else case def_of_const thy def_table x of
3171 SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
3172 let val k = length (strip_abs_vars t') in
3173 [k, num_binder_types T - k]
3176 [num_binder_types T]
3177 | NONE => [num_binder_types T]
3178 (* int list -> int list -> int list *)
3179 fun intersect_formats _ [] = []
3180 | intersect_formats [] _ = []
3181 | intersect_formats ks1 ks2 =
3182 let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
3183 intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
3184 (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
3188 (* theory -> const_table -> (term option * int list) list -> term -> int list *)
3189 fun lookup_format thy def_table formats t =
3190 case AList.lookup (fn (SOME x, SOME y) =>
3191 (term_match thy) (x, y) | _ => false)
3193 SOME format => format
3194 | NONE => let val format = the (AList.lookup (op =) formats NONE) in
3196 Const x => intersect_formats format
3197 (const_format thy def_table x)
3201 (* int list -> int list -> typ -> typ *)
3202 fun format_type default_format format T =
3204 val T = unbit_and_unbox_type T
3205 val format = format |> filter (curry (op <) 0)
3207 if forall (curry (op =) 1) format then
3211 val (binder_Ts, body_T) = strip_type T
3214 |> map (format_type default_format default_format)
3215 |> rev |> chunk_list_unevenly (rev format)
3216 |> map (HOLogic.mk_tupleT o rev)
3217 in List.foldl (op -->) body_T batched end
3219 (* theory -> const_table -> (term option * int list) list -> term -> typ *)
3220 fun format_term_type thy def_table formats t =
3221 format_type (the (AList.lookup (op =) formats NONE))
3222 (lookup_format thy def_table formats t) (fastype_of t)
3224 (* int list -> int -> int list -> int list *)
3225 fun repair_special_format js m format =
3226 m - 1 downto 0 |> chunk_list_unevenly (rev format)
3227 |> map (rev o filter_out (member (op =) js))
3228 |> filter_out null |> map length |> rev
3230 (* extended_context -> string * string -> (term option * int list) list
3231 -> styp -> term * typ *)
3232 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
3233 : extended_context) (base_name, step_name) formats =
3235 val default_format = the (AList.lookup (op =) formats NONE)
3236 (* styp -> term * typ *)
3237 fun do_const (x as (s, T)) =
3238 (if String.isPrefix special_prefix s then
3241 val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
3242 val (x' as (_, T'), js, ts) =
3243 AList.find (op =) (!special_funs) (s, unbit_and_unbox_type T)
3245 val max_j = List.last js
3246 val Ts = List.take (binder_types T', max_j + 1)
3247 val missing_js = filter_out (member (op =) js) (0 upto max_j)
3248 val missing_Ts = filter_indices missing_js Ts
3249 (* int -> indexname *)
3250 fun nth_missing_var n =
3251 ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
3252 val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
3253 val vars = special_bounds ts @ missing_vars
3254 val ts' = map2 (fn T => fn j =>
3255 case AList.lookup (op =) (js ~~ ts) j of
3258 Var (nth missing_vars
3259 (find_index (curry (op =) j)
3262 val t = do_const x' |> fst
3264 case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
3265 | _ => false) formats (SOME t) of
3267 repair_special_format js (num_binder_types T') format
3269 const_format thy def_table x'
3270 |> repair_special_format js (num_binder_types T')
3271 |> intersect_formats default_format
3273 (list_comb (t, ts') |> fold_rev abs_var vars,
3274 format_type default_format format T)
3276 else if String.isPrefix uncurry_prefix s then
3278 val (ss, s') = unprefix uncurry_prefix s
3279 |> strip_first_name_sep |>> space_explode "@"
3281 if String.isPrefix step_prefix s' then
3285 val k = the (Int.fromString (hd ss))
3286 val j = the (Int.fromString (List.last ss))
3287 val (before_Ts, (tuple_T, rest_T)) =
3288 strip_n_binders j T ||> (strip_n_binders 1 #>> hd)
3289 val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T
3290 in do_const (s', T') end
3292 else if String.isPrefix unrolled_prefix s then
3293 let val t = Const (original_name s, range_type T) in
3294 (lambda (Free (iter_var_prefix, nat_T)) t,
3295 format_type default_format
3296 (lookup_format thy def_table formats t) T)
3298 else if String.isPrefix base_prefix s then
3299 (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
3300 format_type default_format default_format T)
3301 else if String.isPrefix step_prefix s then
3302 (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
3303 format_type default_format default_format T)
3304 else if String.isPrefix skolem_prefix s then
3306 val ss = the (AList.lookup (op =) (!skolems) s)
3307 val (Ts, Ts') = chop (length ss) (binder_types T)
3308 val frees = map Free (ss ~~ Ts)
3309 val s' = original_name s
3311 (fold lambda frees (Const (s', Ts' ---> T)),
3312 format_type default_format
3313 (lookup_format thy def_table formats (Const x)) T)
3315 else if String.isPrefix eval_prefix s then
3317 val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
3318 in (t, format_term_type thy def_table formats t) end
3319 else if s = @{const_name undefined_fast_The} then
3320 (Const (nitpick_prefix ^ "The fallback", T),
3321 format_type default_format
3322 (lookup_format thy def_table formats
3323 (Const (@{const_name The}, (T --> bool_T) --> T))) T)
3324 else if s = @{const_name undefined_fast_Eps} then
3325 (Const (nitpick_prefix ^ "Eps fallback", T),
3326 format_type default_format
3327 (lookup_format thy def_table formats
3328 (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
3330 let val t = Const (original_name s, T) in
3331 (t, format_term_type thy def_table formats t)
3333 |>> map_types unbit_and_unbox_type
3334 |>> shorten_names_in_term |>> shorten_abs_vars
3337 (* styp -> string *)
3338 fun assign_operator_for_const (s, T) =
3339 if String.isPrefix ubfp_prefix s then
3340 if is_fun_type T then "\<subseteq>" else "\<le>"
3341 else if String.isPrefix lbfp_prefix s then
3342 if is_fun_type T then "\<supseteq>" else "\<ge>"
3343 else if original_name s <> s then
3344 assign_operator_for_const (after_name_sep s, T)
3348 val binary_int_threshold = 4
3351 fun may_use_binary_ints (t1 $ t2) =
3352 may_use_binary_ints t1 andalso may_use_binary_ints t2
3353 | may_use_binary_ints (Const (s, _)) =
3354 not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
3355 @{const_name Frac}, @{const_name norm_frac},
3356 @{const_name nat_gcd}, @{const_name nat_lcm}] s)
3357 | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
3358 | may_use_binary_ints _ = true
3360 fun should_use_binary_ints (t1 $ t2) =
3361 should_use_binary_ints t1 orelse should_use_binary_ints t2
3362 | should_use_binary_ints (Const (s, _)) =
3363 member (op =) [@{const_name times_nat_inst.times_nat},
3364 @{const_name div_nat_inst.div_nat},
3365 @{const_name times_int_inst.times_int},
3366 @{const_name div_int_inst.div_int}] s
3367 orelse (String.isPrefix numeral_prefix s andalso
3368 let val n = the (Int.fromString (unprefix numeral_prefix s)) in
3369 n <= ~ binary_int_threshold orelse n >= binary_int_threshold
3371 | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
3372 | should_use_binary_ints _ = false
3375 fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
3376 | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
3377 | binarize_nat_and_int_in_type (Type (s, Ts)) =
3378 Type (s, map binarize_nat_and_int_in_type Ts)
3379 | binarize_nat_and_int_in_type T = T
3381 val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
3383 (* extended_context -> term
3384 -> ((term list * term list) * (bool * bool)) * term *)
3385 fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes,
3386 skolemize, uncurry, ...}) t =
3388 val skolem_depth = if skolemize then 4 else ~1
3389 val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
3390 core_t) = t |> unfold_defs_in_term ext_ctxt
3391 |> Refute.close_form
3392 |> skolemize_term_and_more ext_ctxt skolem_depth
3393 |> specialize_consts_in_term ext_ctxt 0
3394 |> `(axioms_for_term ext_ctxt)
3399 forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
3400 (binary_ints = SOME true
3401 orelse exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
3402 val box = exists (not_equal (SOME false) o snd) boxes
3404 Termtab.empty |> uncurry
3405 ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
3406 (* bool -> bool -> term -> term *)
3407 fun do_rest def core =
3408 binarize ? binarize_nat_and_int_in_term
3409 #> uncurry ? uncurry_term table
3410 #> box ? box_fun_and_pair_in_term ext_ctxt def
3411 #> destroy_constrs ? (pull_out_universal_constrs thy def
3412 #> pull_out_existential_constrs thy
3413 #> destroy_pulled_out_constrs ext_ctxt def)
3415 #> destroy_universal_equalities
3416 #> destroy_existential_equalities thy
3417 #> simplify_constrs_and_sels thy
3418 #> distribute_quantifiers
3419 #> push_quantifiers_inward thy
3420 #> not core ? Refute.close_form
3423 (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
3424 (got_all_mono_user_axioms, no_poly_user_axioms)),
3425 do_rest false true core_t)