added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
1 (* Title: HOL/Nitpick/Tools/nitpick_hol.ML
2 Author: Jasmin Blanchette, TU Muenchen
5 Auxiliary HOL-related functions used by Nitpick.
8 signature NITPICK_HOL =
10 type const_table = term list Symtab.table
11 type special_fun = (styp * int list * term list) * styp
12 type unrolled = styp * styp
13 type wf_cache = (styp * (bool * bool)) list
15 type extended_context = {
19 boxes: (typ option * bool option) list,
20 wfs: (styp option * bool option) list,
21 user_axioms: bool option,
23 destroy_constrs: bool,
26 star_linear_preds: bool,
29 tac_timeout: Time.time option,
31 case_names: (string * int) list,
32 def_table: const_table,
33 nondef_table: const_table,
34 user_nondefs: term list,
35 simp_table: const_table Unsynchronized.ref,
36 psimp_table: const_table,
37 intro_table: const_table,
38 ground_thm_table: term list Inttab.table,
39 ersatz_table: (string * string) list,
40 skolems: (string * string list) list Unsynchronized.ref,
41 special_funs: special_fun list Unsynchronized.ref,
42 unrolled_preds: unrolled list Unsynchronized.ref,
43 wf_cache: wf_cache Unsynchronized.ref,
44 constr_cache: (typ * styp list) list Unsynchronized.ref}
47 val numeral_prefix : string
48 val skolem_prefix : string
49 val eval_prefix : string
50 val original_name : string -> string
51 val unbox_type : typ -> typ
52 val string_for_type : Proof.context -> typ -> string
53 val prefix_name : string -> string -> string
54 val short_name : string -> string
55 val short_const_name : string -> string
56 val shorten_const_names_in_term : term -> term
57 val type_match : theory -> typ * typ -> bool
58 val const_match : theory -> styp * styp -> bool
59 val term_match : theory -> term * term -> bool
60 val is_TFree : typ -> bool
61 val is_higher_order_type : typ -> bool
62 val is_fun_type : typ -> bool
63 val is_set_type : typ -> bool
64 val is_pair_type : typ -> bool
65 val is_lfp_iterator_type : typ -> bool
66 val is_gfp_iterator_type : typ -> bool
67 val is_fp_iterator_type : typ -> bool
68 val is_boolean_type : typ -> bool
69 val is_integer_type : typ -> bool
70 val is_record_type : typ -> bool
71 val is_number_type : theory -> typ -> bool
72 val const_for_iterator_type : typ -> styp
73 val nth_range_type : int -> typ -> typ
74 val num_factors_in_type : typ -> int
75 val num_binder_types : typ -> int
76 val curried_binder_types : typ -> typ list
77 val mk_flat_tuple : typ -> term list -> term
78 val dest_n_tuple : int -> term -> term list
79 val instantiate_type : theory -> typ -> typ -> typ -> typ
80 val is_codatatype : theory -> typ -> bool
81 val is_pure_typedef : theory -> typ -> bool
82 val is_univ_typedef : theory -> typ -> bool
83 val is_datatype : theory -> typ -> bool
84 val is_record_constr : styp -> bool
85 val is_record_get : theory -> styp -> bool
86 val is_record_update : theory -> styp -> bool
87 val is_abs_fun : theory -> styp -> bool
88 val is_rep_fun : theory -> styp -> bool
89 val is_constr : theory -> styp -> bool
90 val is_sel : string -> bool
91 val discr_for_constr : styp -> styp
92 val num_sels_for_constr_type : typ -> int
93 val nth_sel_name_for_constr_name : string -> int -> string
94 val nth_sel_for_constr : styp -> int -> styp
95 val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
96 val sel_no_from_name : string -> int
97 val eta_expand : typ list -> term -> int -> term
98 val extensionalize : term -> term
99 val distinctness_formula : typ -> term list -> term
100 val register_frac_type : string -> (string * string) list -> theory -> theory
101 val unregister_frac_type : string -> theory -> theory
102 val register_codatatype : typ -> string -> styp list -> theory -> theory
103 val unregister_codatatype : typ -> theory -> theory
104 val datatype_constrs : extended_context -> typ -> styp list
105 val boxed_datatype_constrs : extended_context -> typ -> styp list
106 val num_datatype_constrs : extended_context -> typ -> int
107 val constr_name_for_sel_like : string -> string
108 val boxed_constr_for_sel : extended_context -> styp -> styp
109 val card_of_type : (typ * int) list -> typ -> int
110 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
111 val bounded_precise_card_of_type :
112 extended_context -> int -> int -> (typ * int) list -> typ -> int
113 val is_finite_type : extended_context -> typ -> bool
114 val all_axioms_of : theory -> term list * term list * term list
115 val arity_of_built_in_const : bool -> styp -> int option
116 val is_built_in_const : bool -> styp -> bool
117 val case_const_names : theory -> (string * int) list
118 val const_def_table : Proof.context -> term list -> const_table
119 val const_nondef_table : term list -> const_table
120 val const_simp_table : Proof.context -> const_table
121 val const_psimp_table : Proof.context -> const_table
122 val inductive_intro_table : Proof.context -> const_table -> const_table
123 val ground_theorem_table : theory -> term list Inttab.table
124 val ersatz_table : theory -> (string * string) list
125 val def_of_const : theory -> const_table -> styp -> term option
126 val is_inductive_pred : extended_context -> styp -> bool
127 val is_constr_pattern_lhs : theory -> term -> bool
128 val is_constr_pattern_formula : theory -> term -> bool
129 val merge_type_vars_in_terms : term list -> term list
130 val ground_types_in_type : extended_context -> typ -> typ list
131 val ground_types_in_terms : extended_context -> term list -> typ list
132 val format_type : int list -> int list -> typ -> typ
133 val format_term_type :
134 theory -> const_table -> (term option * int list) list -> term -> typ
135 val user_friendly_const :
136 extended_context -> string * string -> (term option * int list) list
137 -> styp -> term * typ
138 val assign_operator_for_const : styp -> string
139 val preprocess_term :
140 extended_context -> term -> ((term list * term list) * (bool * bool)) * term
143 structure Nitpick_HOL : NITPICK_HOL =
148 type const_table = term list Symtab.table
149 type special_fun = (styp * int list * term list) * styp
150 type unrolled = styp * styp
151 type wf_cache = (styp * (bool * bool)) list
153 type extended_context = {
156 max_bisim_depth: int,
157 boxes: (typ option * bool option) list,
158 wfs: (styp option * bool option) list,
159 user_axioms: bool option,
161 destroy_constrs: bool,
164 star_linear_preds: bool,
167 tac_timeout: Time.time option,
169 case_names: (string * int) list,
170 def_table: const_table,
171 nondef_table: const_table,
172 user_nondefs: term list,
173 simp_table: const_table Unsynchronized.ref,
174 psimp_table: const_table,
175 intro_table: const_table,
176 ground_thm_table: term list Inttab.table,
177 ersatz_table: (string * string) list,
178 skolems: (string * string list) list Unsynchronized.ref,
179 special_funs: special_fun list Unsynchronized.ref,
180 unrolled_preds: unrolled list Unsynchronized.ref,
181 wf_cache: wf_cache Unsynchronized.ref,
182 constr_cache: (typ * styp list) list Unsynchronized.ref}
184 structure TheoryData = TheoryDataFun(
185 type T = {frac_types: (string * (string * string) list) list,
186 codatatypes: (string * (string * styp list)) list}
187 val empty = {frac_types = [], codatatypes = []}
190 fun merge _ ({frac_types = fs1, codatatypes = cs1},
191 {frac_types = fs2, codatatypes = cs2}) =
192 {frac_types = AList.merge (op =) (op =) (fs1, fs2),
193 codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
195 (* term * term -> term *)
196 fun s_conj (t1, @{const True}) = t1
197 | s_conj (@{const True}, t2) = t2
198 | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}
199 else HOLogic.mk_conj (t1, t2)
200 fun s_disj (t1, @{const False}) = t1
201 | s_disj (@{const False}, t2) = t2
202 | s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True}
203 else HOLogic.mk_disj (t1, t2)
204 (* term -> term -> term *)
206 HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
208 (* term -> term -> term list *)
209 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
210 if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
211 | strip_connective _ t = [t]
212 (* term -> term list * term *)
213 fun strip_any_connective (t as (t0 $ t1 $ t2)) =
214 if t0 mem [@{const "op &"}, @{const "op |"}] then
215 (strip_connective t0 t, t0)
218 | strip_any_connective t = ([t], @{const Not})
219 (* term -> term list *)
220 val conjuncts = strip_connective @{const "op &"}
221 val disjuncts = strip_connective @{const "op |"}
224 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
225 val sel_prefix = nitpick_prefix ^ "sel"
226 val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
227 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
228 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
229 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
230 val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep
231 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
232 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
233 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
234 val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
235 val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
236 val skolem_prefix = nitpick_prefix ^ "sk"
237 val special_prefix = nitpick_prefix ^ "sp"
238 val uncurry_prefix = nitpick_prefix ^ "unc"
239 val eval_prefix = nitpick_prefix ^ "eval"
240 val bound_var_prefix = "b"
241 val cong_var_prefix = "c"
242 val iter_var_prefix = "i"
243 val val_var_prefix = nitpick_prefix ^ "v"
244 val arg_var_prefix = "x"
247 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
248 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
249 (* int -> int -> string *)
250 fun skolem_prefix_for k j =
251 skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
252 fun uncurry_prefix_for k j =
253 uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
255 (* string -> string * string *)
256 val strip_first_name_sep =
257 Substring.full #> Substring.position name_sep ##> Substring.triml 1
258 #> pairself Substring.string
259 (* string -> string *)
260 fun original_name s =
261 if String.isPrefix nitpick_prefix s then
262 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
265 val after_name_sep = snd o strip_first_name_sep
267 (* When you add constants to these lists, make sure to handle them in
268 "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
270 val built_in_consts =
271 [(@{const_name all}, 1),
272 (@{const_name "=="}, 2),
273 (@{const_name "==>"}, 2),
274 (@{const_name Pure.conjunction}, 2),
275 (@{const_name Trueprop}, 1),
276 (@{const_name Not}, 1),
277 (@{const_name False}, 0),
278 (@{const_name True}, 0),
279 (@{const_name All}, 1),
280 (@{const_name Ex}, 1),
281 (@{const_name "op ="}, 2),
282 (@{const_name "op &"}, 2),
283 (@{const_name "op |"}, 2),
284 (@{const_name "op -->"}, 2),
285 (@{const_name If}, 3),
286 (@{const_name Let}, 2),
287 (@{const_name Unity}, 0),
288 (@{const_name Pair}, 2),
289 (@{const_name fst}, 1),
290 (@{const_name snd}, 1),
291 (@{const_name Id}, 0),
292 (@{const_name insert}, 2),
293 (@{const_name converse}, 1),
294 (@{const_name trancl}, 1),
295 (@{const_name rel_comp}, 2),
296 (@{const_name image}, 2),
297 (@{const_name Suc}, 0),
298 (@{const_name finite}, 1),
299 (@{const_name nat}, 0),
300 (@{const_name zero_nat_inst.zero_nat}, 0),
301 (@{const_name one_nat_inst.one_nat}, 0),
302 (@{const_name plus_nat_inst.plus_nat}, 0),
303 (@{const_name minus_nat_inst.minus_nat}, 0),
304 (@{const_name times_nat_inst.times_nat}, 0),
305 (@{const_name div_nat_inst.div_nat}, 0),
306 (@{const_name div_nat_inst.mod_nat}, 0),
307 (@{const_name ord_nat_inst.less_nat}, 2),
308 (@{const_name ord_nat_inst.less_eq_nat}, 2),
309 (@{const_name nat_gcd}, 0),
310 (@{const_name nat_lcm}, 0),
311 (@{const_name zero_int_inst.zero_int}, 0),
312 (@{const_name one_int_inst.one_int}, 0),
313 (@{const_name plus_int_inst.plus_int}, 0),
314 (@{const_name minus_int_inst.minus_int}, 0),
315 (@{const_name times_int_inst.times_int}, 0),
316 (@{const_name div_int_inst.div_int}, 0),
317 (@{const_name div_int_inst.mod_int}, 0),
318 (@{const_name uminus_int_inst.uminus_int}, 0),
319 (@{const_name ord_int_inst.less_int}, 2),
320 (@{const_name ord_int_inst.less_eq_int}, 2),
321 (@{const_name Tha}, 1),
322 (@{const_name Frac}, 0),
323 (@{const_name norm_frac}, 0)]
324 val built_in_descr_consts =
325 [(@{const_name The}, 1),
326 (@{const_name Eps}, 1)]
327 val built_in_typed_consts =
328 [((@{const_name of_nat}, nat_T --> int_T), 0)]
329 val built_in_set_consts =
330 [(@{const_name lower_semilattice_fun_inst.inf_fun}, 2),
331 (@{const_name upper_semilattice_fun_inst.sup_fun}, 2),
332 (@{const_name minus_fun_inst.minus_fun}, 2),
333 (@{const_name ord_fun_inst.less_eq_fun}, 2)]
336 fun unbox_type (Type (@{type_name fun_box}, Ts)) =
337 Type ("fun", map unbox_type Ts)
338 | unbox_type (Type (@{type_name pair_box}, Ts)) =
339 Type ("*", map unbox_type Ts)
340 | unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts)
342 (* Proof.context -> typ -> string *)
343 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type
345 (* string -> string -> string *)
346 val prefix_name = Long_Name.qualify o Long_Name.base_name
347 (* string -> string *)
348 fun short_name s = List.last (space_explode "." s) handle List.Empty => ""
349 (* string -> term -> term *)
350 val prefix_abs_vars = Term.map_abs_vars o prefix_name
352 val shorten_abs_vars = Term.map_abs_vars short_name
353 (* string -> string *)
354 fun short_const_name s =
355 case space_explode name_sep s of
356 [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
357 | ss => map short_name ss |> space_implode "_"
359 val shorten_const_names_in_term =
360 map_aterms (fn Const (s, T) => Const (short_const_name s, T) | t => t)
362 (* theory -> typ * typ -> bool *)
363 fun type_match thy (T1, T2) =
364 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
365 handle Type.TYPE_MATCH => false
366 (* theory -> styp * styp -> bool *)
367 fun const_match thy ((s1, T1), (s2, T2)) =
368 s1 = s2 andalso type_match thy (T1, T2)
369 (* theory -> term * term -> bool *)
370 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
371 | term_match thy (Free (s1, T1), Free (s2, T2)) =
372 const_match thy ((short_name s1, T1), (short_name s2, T2))
373 | term_match thy (t1, t2) = t1 aconv t2
376 fun is_TFree (TFree _) = true
378 fun is_higher_order_type (Type ("fun", _)) = true
379 | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
380 | is_higher_order_type _ = false
381 fun is_fun_type (Type ("fun", _)) = true
382 | is_fun_type _ = false
383 fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
384 | is_set_type _ = false
385 fun is_pair_type (Type ("*", _)) = true
386 | is_pair_type _ = false
387 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
388 | is_lfp_iterator_type _ = false
389 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
390 | is_gfp_iterator_type _ = false
391 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
392 val is_boolean_type = equal prop_T orf equal bool_T
393 val is_integer_type =
394 member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
395 val is_record_type = not o null o Record.dest_recTs
396 (* theory -> typ -> bool *)
397 fun is_frac_type thy (Type (s, [])) =
398 not (null (these (AList.lookup (op =) (#frac_types (TheoryData.get thy))
400 | is_frac_type _ _ = false
401 fun is_number_type thy = is_integer_type orf is_frac_type thy
403 (* bool -> styp -> typ *)
404 fun iterator_type_for_const gfp (s, T) =
405 Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
408 fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
409 | const_for_iterator_type T =
410 raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
412 (* int -> typ -> typ * typ *)
413 fun strip_n_binders 0 T = ([], T)
414 | strip_n_binders n (Type ("fun", [T1, T2])) =
415 strip_n_binders (n - 1) T2 |>> cons T1
416 | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
417 strip_n_binders n (Type ("fun", Ts))
418 | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
420 val nth_range_type = snd oo strip_n_binders
423 fun num_factors_in_type (Type ("*", [T1, T2])) =
424 fold (Integer.add o num_factors_in_type) [T1, T2] 0
425 | num_factors_in_type _ = 1
426 fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
427 | num_binder_types _ = 0
428 (* typ -> typ list *)
429 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
430 fun maybe_curried_binder_types T =
431 (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
433 (* typ -> term list -> term *)
434 fun mk_flat_tuple _ [t] = t
435 | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
436 HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
437 | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
438 (* int -> term -> term list *)
439 fun dest_n_tuple 1 t = [t]
440 | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
442 (* int -> typ -> typ list *)
443 fun dest_n_tuple_type 1 T = [T]
444 | dest_n_tuple_type n (Type (_, [T1, T2])) =
445 T1 :: dest_n_tuple_type (n - 1) T2
446 | dest_n_tuple_type _ T =
447 raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
449 (* (typ * typ) list -> typ -> typ *)
450 fun typ_subst [] T = T
455 case AList.lookup (op =) ps T of
457 | NONE => case T of Type (s, Ts) => Type (s, map subst Ts) | _ => T
460 (* theory -> typ -> typ -> typ -> typ *)
461 fun instantiate_type thy T1 T1' T2 =
462 Same.commit (Envir.subst_type_same
463 (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
465 handle Type.TYPE_MATCH =>
466 raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
468 (* theory -> typ -> typ -> styp *)
469 fun repair_constr_type thy body_T' T =
470 instantiate_type thy (body_type T) body_T' T
472 (* string -> (string * string) list -> theory -> theory *)
473 fun register_frac_type frac_s ersaetze thy =
475 val {frac_types, codatatypes} = TheoryData.get thy
476 val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
477 in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
478 (* string -> theory -> theory *)
479 fun unregister_frac_type frac_s = register_frac_type frac_s []
481 (* typ -> string -> styp list -> theory -> theory *)
482 fun register_codatatype co_T case_name constr_xs thy =
484 val {frac_types, codatatypes} = TheoryData.get thy
485 val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
486 val (co_s, co_Ts) = dest_Type co_T
488 if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()
489 else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
490 val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
492 in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end
493 (* typ -> theory -> theory *)
494 fun unregister_codatatype co_T = register_codatatype co_T "" []
497 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
498 set_def: thm option, prop_of_Rep: thm, set_name: string,
499 Rep_inverse: thm option}
501 (* theory -> string -> typedef_info *)
502 fun typedef_info thy s =
503 if is_frac_type thy (Type (s, [])) then
504 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
505 Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
506 set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
508 set_name = @{const_name Frac}, Rep_inverse = NONE}
509 else case Typedef.get_info thy s of
510 SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse,
512 SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
513 Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
514 set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
518 fun is_basic_datatype s =
519 s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
520 @{type_name nat}, @{type_name int}]
521 (* theory -> string -> bool *)
522 val is_typedef = is_some oo typedef_info
523 val is_real_datatype = is_some oo Datatype.get_info
524 (* theory -> typ -> bool *)
525 fun is_codatatype thy (T as Type (s, _)) =
526 not (null (AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s
527 |> Option.map snd |> these))
528 | is_codatatype _ _ = false
529 fun is_pure_typedef thy (T as Type (s, _)) =
530 is_typedef thy s andalso
531 not (is_real_datatype thy s orelse is_codatatype thy T
532 orelse is_record_type T orelse is_integer_type T)
533 | is_pure_typedef _ _ = false
534 fun is_univ_typedef thy (Type (s, _)) =
535 (case typedef_info thy s of
536 SOME {set_def, prop_of_Rep, ...} =>
539 try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
541 try (fst o dest_Const o snd o HOLogic.dest_mem
542 o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name UNIV}
544 | is_univ_typedef _ _ = false
545 fun is_datatype thy (T as Type (s, _)) =
546 (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind})
547 andalso not (is_basic_datatype s)
548 | is_datatype _ _ = false
550 (* theory -> typ -> (string * typ) list * (string * typ) *)
551 fun all_record_fields thy T =
552 let val (recs, more) = Record.get_extT_fields thy T in
553 recs @ more :: all_record_fields thy (snd more)
557 fun is_record_constr (x as (s, T)) =
558 String.isSuffix Record.extN s andalso
559 let val dataT = body_type T in
560 is_record_type dataT andalso
561 s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
563 (* theory -> typ -> int *)
564 val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
565 (* theory -> string -> typ -> int *)
566 fun no_of_record_field thy s T1 =
567 find_index (equal s o fst) (Record.get_extT_fields thy T1 ||> single |> op @)
568 (* theory -> styp -> bool *)
569 fun is_record_get thy (s, Type ("fun", [T1, _])) =
570 exists (equal s o fst) (all_record_fields thy T1)
571 | is_record_get _ _ = false
572 fun is_record_update thy (s, T) =
573 String.isSuffix Record.updateN s andalso
574 exists (equal (unsuffix Record.updateN s) o fst)
575 (all_record_fields thy (body_type T))
576 handle TYPE _ => false
577 fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
578 (case typedef_info thy s' of
579 SOME {Abs_name, ...} => s = Abs_name
581 | is_abs_fun _ _ = false
582 fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
583 (case typedef_info thy s' of
584 SOME {Rep_name, ...} => s = Rep_name
586 | is_rep_fun _ _ = false
588 (* theory -> styp -> styp *)
589 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
590 (case typedef_info thy s' of
591 SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
592 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
593 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
595 (* theory -> styp -> bool *)
596 fun is_coconstr thy (s, T) =
598 val {codatatypes, ...} = TheoryData.get thy
599 val co_T = body_type T
600 val co_s = dest_Type co_T |> fst
602 exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
603 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
605 handle TYPE ("dest_Type", _, _) => false
606 fun is_constr_like thy (s, T) =
607 s mem [@{const_name FunBox}, @{const_name PairBox}] orelse
608 let val (x as (s, T)) = (s, unbox_type T) in
609 Refute.is_IDT_constructor thy x orelse is_record_constr x
610 orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
611 orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]
612 orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
613 orelse is_coconstr thy x
615 fun is_constr thy (x as (_, T)) =
617 andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
619 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
620 val is_sel_like_and_no_discr =
621 String.isPrefix sel_prefix
622 orf (member (op =) [@{const_name fst}, @{const_name snd}])
624 datatype boxability =
625 InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
627 (* boxability -> boxability *)
628 fun in_fun_lhs_for InConstr = InSel
629 | in_fun_lhs_for _ = InFunLHS
630 fun in_fun_rhs_for InConstr = InConstr
631 | in_fun_rhs_for InSel = InSel
632 | in_fun_rhs_for InFunRHS1 = InFunRHS2
633 | in_fun_rhs_for _ = InFunRHS1
635 (* extended_context -> boxability -> typ -> bool *)
636 fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
639 boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T))
641 boxy mem [InPair, InFunRHS1, InFunRHS2]
642 orelse (boxy mem [InExpr, InFunLHS]
643 andalso exists (is_boxing_worth_it ext_ctxt InPair)
644 (map (box_type ext_ctxt InPair) Ts))
646 (* extended_context -> boxability -> string * typ list -> string *)
647 and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
648 case triple_lookup (type_match thy) boxes (Type z) of
649 SOME (SOME box_me) => box_me
650 | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
651 (* extended_context -> boxability -> typ -> typ *)
652 and box_type ext_ctxt boxy T =
654 Type (z as ("fun", [T1, T2])) =>
655 if not (boxy mem [InConstr, InSel])
656 andalso should_box_type ext_ctxt boxy z then
657 Type (@{type_name fun_box},
658 [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
660 box_type ext_ctxt (in_fun_lhs_for boxy) T1
661 --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
662 | Type (z as ("*", Ts)) =>
663 if should_box_type ext_ctxt boxy z then
664 Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
666 Type ("*", map (box_type ext_ctxt
667 (if boxy mem [InConstr, InSel] then boxy
672 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
675 fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
676 (* string -> int -> string *)
677 fun nth_sel_name_for_constr_name s n =
678 if s = @{const_name Pair} then
679 if n = 0 then @{const_name fst} else @{const_name snd}
682 (* styp -> int -> styp *)
683 fun nth_sel_for_constr x ~1 = discr_for_constr x
684 | nth_sel_for_constr (s, T) n =
685 (nth_sel_name_for_constr_name s n,
686 body_type T --> nth (maybe_curried_binder_types T) n)
687 (* extended_context -> styp -> int -> styp *)
688 fun boxed_nth_sel_for_constr ext_ctxt =
689 apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr
692 fun sel_no_from_name s =
693 if String.isPrefix discr_prefix s then
695 else if String.isPrefix sel_prefix s then
696 s |> unprefix sel_prefix |> Int.fromString |> the
697 else if s = @{const_name snd} then
702 (* typ list -> term -> int -> term *)
703 fun eta_expand _ t 0 = t
704 | eta_expand Ts (Abs (s, T, t')) n =
705 Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
706 | eta_expand Ts t n =
707 fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
708 (List.take (binder_types (fastype_of1 (Ts, t)), n))
709 (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
712 fun extensionalize t =
714 (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
715 | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>
716 let val v = Var ((s, maxidx_of_term t + 1), T) in
717 extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))
721 (* typ -> term list -> term *)
722 fun distinctness_formula T =
723 all_distinct_unordered_pairs_of
724 #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
725 #> List.foldr (s_conj o swap) @{const True}
728 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
729 fun suc_const T = Const (@{const_name Suc}, T --> T)
731 (* theory -> typ -> styp list *)
732 fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
733 if is_datatype thy T then
734 case Datatype.get_info thy s of
735 SOME {index, descr, ...} =>
736 let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
738 (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
742 case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of
743 SOME (_, xs' as (_ :: _)) =>
744 map (apsnd (repair_constr_type thy T)) xs'
746 if is_record_type T then
748 val s' = unsuffix Record.ext_typeN s ^ Record.extN
749 val T' = (Record.get_extT_fields thy T
750 |> apsnd single |> uncurry append |> map snd) ---> T
752 else case typedef_info thy s of
753 SOME {abs_type, rep_type, Abs_name, ...} =>
754 [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
756 if T = @{typ ind} then
757 [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
762 | uncached_datatype_constrs _ _ = []
763 (* extended_context -> typ -> styp list *)
764 fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
766 case AList.lookup (op =) (!constr_cache) T of
769 let val xs = uncached_datatype_constrs thy T in
770 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
772 fun boxed_datatype_constrs ext_ctxt =
773 map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
774 (* extended_context -> typ -> int *)
775 val num_datatype_constrs = length oo datatype_constrs
777 (* string -> string *)
778 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
779 | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
780 | constr_name_for_sel_like s' = original_name s'
781 (* extended_context -> styp -> styp *)
782 fun boxed_constr_for_sel ext_ctxt (s', T') =
783 let val s = constr_name_for_sel_like s' in
784 AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
787 (* extended_context -> styp -> term *)
788 fun discr_term_for_constr ext_ctxt (x as (s, T)) =
789 let val dataT = body_type T in
790 if s = @{const_name Suc} then
792 @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
793 else if num_datatype_constrs ext_ctxt dataT >= 2 then
794 Const (discr_for_constr x)
796 Abs (Name.uu, dataT, @{const True})
799 (* extended_context -> styp -> term -> term *)
800 fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
803 if x = x' then @{const True}
804 else if is_constr_like thy x' then @{const False}
805 else betapply (discr_term_for_constr ext_ctxt x, t)
806 | _ => betapply (discr_term_for_constr ext_ctxt x, t)
808 (* styp -> term -> term *)
809 fun nth_arg_sel_term_for_constr (x as (s, T)) n =
810 let val (arg_Ts, dataT) = strip_type T in
811 if dataT = nat_T then
812 @{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}
813 else if is_pair_type dataT then
814 Const (nth_sel_for_constr x n)
817 (* int -> typ -> int * term *)
818 fun aux m (Type ("*", [T1, T2])) =
820 val (m, t1) = aux m T1
821 val (m, t2) = aux m T2
822 in (m, HOLogic.mk_prod (t1, t2)) end
824 (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
826 val m = fold (Integer.add o num_factors_in_type)
827 (List.take (arg_Ts, n)) 0
828 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
830 (* theory -> styp -> term -> int -> typ -> term *)
831 fun select_nth_constr_arg thy x t n res_T =
834 if x = x' then nth args n
835 else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
836 else betapply (nth_arg_sel_term_for_constr x n, t)
837 | _ => betapply (nth_arg_sel_term_for_constr x n, t)
839 (* theory -> styp -> term list -> term *)
840 fun construct_value _ x [] = Const x
841 | construct_value thy (x as (s, _)) args =
842 let val args = map Envir.eta_contract args in
844 Const (x' as (s', _)) $ t =>
845 if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s
846 andalso forall (fn (n, t') =>
847 select_nth_constr_arg thy x t n dummyT = t')
848 (index_seq 0 (length args) ~~ args) then
851 list_comb (Const x, args)
852 | _ => list_comb (Const x, args)
855 (* extended_context -> typ -> term -> term *)
856 fun constr_expand (ext_ctxt as {thy, ...}) T t =
858 Const x => if is_constr_like thy x then t else raise SAME ()
859 | _ => raise SAME ())
863 if is_pair_type T then
864 let val (T1, T2) = HOLogic.dest_prodT T in
865 (@{const_name Pair}, [T1, T2] ---> T)
868 datatype_constrs ext_ctxt T |> the_single
869 val arg_Ts = binder_types T'
871 list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
872 (index_seq 0 (length arg_Ts)) arg_Ts)
875 (* (typ * int) list -> typ -> int *)
876 fun card_of_type asgns (Type ("fun", [T1, T2])) =
877 reasonable_power (card_of_type asgns T2) (card_of_type asgns T1)
878 | card_of_type asgns (Type ("*", [T1, T2])) =
879 card_of_type asgns T1 * card_of_type asgns T2
880 | card_of_type _ (Type (@{type_name itself}, _)) = 1
881 | card_of_type _ @{typ prop} = 2
882 | card_of_type _ @{typ bool} = 2
883 | card_of_type _ @{typ unit} = 1
884 | card_of_type asgns T =
885 case AList.lookup (op =) asgns T of
887 | NONE => if T = @{typ bisim_iterator} then 0
888 else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
889 (* int -> (typ * int) list -> typ -> int *)
890 fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) =
892 val k1 = bounded_card_of_type max default_card asgns T1
893 val k2 = bounded_card_of_type max default_card asgns T2
895 if k1 = max orelse k2 = max then max
896 else Int.min (max, reasonable_power k2 k1)
898 | bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) =
900 val k1 = bounded_card_of_type max default_card asgns T1
901 val k2 = bounded_card_of_type max default_card asgns T2
902 in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
903 | bounded_card_of_type max default_card asgns T =
904 Int.min (max, if default_card = ~1 then
908 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
910 (* extended_context -> int -> (typ * int) list -> typ -> int *)
911 fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
913 (* typ list -> typ -> int *)
918 Type ("fun", [T1, T2]) =>
920 val k1 = aux avoid T1
921 val k2 = aux avoid T2
923 if k1 = 0 orelse k2 = 0 then 0
924 else if k1 >= max orelse k2 >= max then max
925 else Int.min (max, reasonable_power k2 k1)
927 | Type ("*", [T1, T2]) =>
929 val k1 = aux avoid T1
930 val k2 = aux avoid T2
932 if k1 = 0 orelse k2 = 0 then 0
933 else if k1 >= max orelse k2 >= max then max
934 else Int.min (max, k1 * k2)
936 | Type (@{type_name itself}, _) => 1
941 (case datatype_constrs ext_ctxt T of
942 [] => if is_integer_type T then 0 else raise SAME ()
946 datatype_constrs ext_ctxt T
947 |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
950 if exists (equal 0) constr_cards then 0
951 else Integer.sum constr_cards
953 | _ => raise SAME ())
954 handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
955 in Int.min (max, aux [] T) end
957 (* extended_context -> typ -> bool *)
958 fun is_finite_type ext_ctxt =
959 not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []
962 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
963 | is_ground_term (Const _) = true
964 | is_ground_term _ = false
966 (* term -> word -> word *)
967 fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
968 | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
971 val hash_term = Word.toInt o hashw_term
973 (* term list -> (indexname * typ) list *)
974 fun special_bounds ts =
975 fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
977 (* indexname * typ -> term -> term *)
978 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
980 (* theory -> string -> bool *)
981 fun is_funky_typedef_name thy s =
982 s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
984 orelse is_frac_type thy (Type (s, []))
985 (* theory -> term -> bool *)
986 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
987 | is_funky_typedef _ _ = false
989 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
990 $ Const (@{const_name TYPE}, _)) = true
991 | is_arity_type_axiom _ = false
992 (* theory -> bool -> term -> bool *)
993 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
994 is_typedef_axiom thy boring t2
995 | is_typedef_axiom thy boring
996 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
997 $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
998 boring <> is_funky_typedef_name thy s andalso is_typedef thy s
999 | is_typedef_axiom _ _ _ = false
1001 (* Distinguishes between (1) constant definition axioms, (2) type arity and
1002 typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
1003 Typedef axioms are uninteresting to Nitpick, because it can retrieve them
1004 using "typedef_info". *)
1005 (* theory -> (string * term) list -> string list -> term list * term list *)
1006 fun partition_axioms_by_definitionality thy axioms def_names =
1008 val axioms = sort (fast_string_ord o pairself fst) axioms
1009 val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
1011 OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
1012 |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
1013 in pairself (map snd) (defs, nondefs) end
1015 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
1016 will do as long as it contains all the "axioms" and "axiomatization"
1018 (* theory -> bool *)
1019 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
1022 val is_plain_definition =
1026 case strip_comb t1 of
1027 (Const _, args) => forall is_Var args
1028 andalso not (has_duplicates (op =) args)
1030 fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
1031 | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
1036 (* theory -> term list * term list * term list *)
1037 fun all_axioms_of thy =
1039 (* theory list -> term list *)
1040 val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
1041 val specs = Defs.all_specifications_of (Theory.defs_of thy)
1042 val def_names = specs |> maps snd |> filter #is_def |> map #name
1043 |> OrdList.make fast_string_ord
1044 val thys = thy :: Theory.ancestors_of thy
1045 val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
1046 val built_in_axioms = axioms_of_thys built_in_thys
1047 val user_axioms = axioms_of_thys user_thys
1048 val (built_in_defs, built_in_nondefs) =
1049 partition_axioms_by_definitionality thy built_in_axioms def_names
1050 ||> filter (is_typedef_axiom thy false)
1051 val (user_defs, user_nondefs) =
1052 partition_axioms_by_definitionality thy user_axioms def_names
1053 val (built_in_nondefs, user_nondefs) =
1054 List.partition (is_typedef_axiom thy false) user_nondefs
1055 |>> append built_in_nondefs
1056 val defs = (thy |> PureThy.all_thms_of
1057 |> filter (equal Thm.definitionK o Thm.get_kind o snd)
1058 |> map (prop_of o snd) |> filter is_plain_definition) @
1059 user_defs @ built_in_defs
1060 in (defs, built_in_nondefs, user_nondefs) end
1062 (* bool -> styp -> int option *)
1063 fun arity_of_built_in_const fast_descrs (s, T) =
1064 if s = @{const_name If} then
1065 if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
1066 else case AList.lookup (op =)
1068 |> fast_descrs ? append built_in_descr_consts) s of
1071 case AList.lookup (op =) built_in_typed_consts (s, T) of
1074 if is_fun_type T andalso is_set_type (domain_type T) then
1075 AList.lookup (op =) built_in_set_consts s
1078 (* bool -> styp -> bool *)
1079 val is_built_in_const = is_some oo arity_of_built_in_const
1081 (* This function is designed to work for both real definition axioms and
1082 simplification rules (equational specifications). *)
1084 fun term_under_def t =
1086 @{const "==>"} $ _ $ t2 => term_under_def t2
1087 | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
1088 | @{const Trueprop} $ t1 => term_under_def t1
1089 | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
1090 | Abs (_, _, t') => term_under_def t'
1091 | t1 $ _ => term_under_def t1
1094 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
1095 traversal of the term, without which the wrong occurrence of a constant could
1096 be matched in the face of overloading. *)
1097 (* theory -> bool -> const_table -> styp -> term list *)
1098 fun def_props_for_const thy fast_descrs table (x as (s, _)) =
1099 if is_built_in_const fast_descrs x then
1102 these (Symtab.lookup table s)
1103 |> map_filter (try (Refute.specialize_type thy x))
1104 |> filter (equal (Const x) o term_under_def)
1107 fun normalized_rhs_of thy t =
1110 fun aux (v as Var _) t = lambda v t
1111 | aux (c as Const (@{const_name TYPE}, T)) t = lambda c t
1112 | aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
1115 Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
1116 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
1118 | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
1119 val args = strip_comb lhs |> snd
1120 in fold_rev aux args rhs end
1122 (* theory -> const_table -> styp -> term option *)
1123 fun def_of_const thy table (x as (s, _)) =
1124 if is_built_in_const false x orelse original_name s <> s then
1127 x |> def_props_for_const thy false table |> List.last
1128 |> normalized_rhs_of thy |> prefix_abs_vars s |> SOME
1129 handle List.Empty => NONE
1131 datatype fixpoint_kind = Lfp | Gfp | NoFp
1133 (* term -> fixpoint_kind *)
1134 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
1135 | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
1136 | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
1137 | fixpoint_kind_of_rhs _ = NoFp
1139 (* theory -> const_table -> term -> bool *)
1140 fun is_mutually_inductive_pred_def thy table t =
1143 fun is_good_arg (Bound _) = true
1144 | is_good_arg (Const (s, _)) =
1145 s mem [@{const_name True}, @{const_name False}, @{const_name undefined}]
1146 | is_good_arg _ = false
1148 case t |> strip_abs_body |> strip_comb of
1149 (Const x, ts as (_ :: _)) =>
1150 (case def_of_const thy table x of
1151 SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
1155 (* theory -> const_table -> term -> term *)
1156 fun unfold_mutually_inductive_preds thy table =
1157 map_aterms (fn t as Const x =>
1158 (case def_of_const thy table x of
1160 let val t' = Envir.eta_contract t' in
1161 if is_mutually_inductive_pred_def thy table t' then t'
1167 (* term -> string * term *)
1168 fun pair_for_prop t =
1169 case term_under_def t of
1170 Const (s, _) => (s, t)
1171 | Free _ => raise NOT_SUPPORTED "local definitions"
1172 | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
1174 (* (Proof.context -> term list) -> Proof.context -> const_table *)
1175 fun table_for get ctxt =
1176 get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
1178 (* theory -> (string * int) list *)
1179 fun case_const_names thy =
1180 Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
1181 if is_basic_datatype dtype_s then
1184 cons (case_name, AList.lookup (op =) descr index
1185 |> the |> #3 |> length))
1186 (Datatype.get_all thy) [] @
1187 map (apsnd length o snd) (#codatatypes (TheoryData.get thy))
1189 (* Proof.context -> term list -> const_table *)
1190 fun const_def_table ctxt ts =
1191 table_for (map prop_of o Nitpick_Defs.get) ctxt
1192 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
1193 (map pair_for_prop ts)
1194 (* term list -> const_table *)
1195 fun const_nondef_table ts =
1196 fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
1197 |> AList.group (op =) |> Symtab.make
1198 (* Proof.context -> const_table *)
1199 val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
1200 val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
1201 (* Proof.context -> const_table -> const_table *)
1202 fun inductive_intro_table ctxt def_table =
1203 table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
1204 def_table o prop_of)
1205 o Nitpick_Intros.get) ctxt
1206 (* theory -> term list Inttab.table *)
1207 fun ground_theorem_table thy =
1208 fold ((fn @{const Trueprop} $ t1 =>
1209 is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
1210 | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
1212 val basic_ersatz_table =
1213 [(@{const_name prod_case}, @{const_name split}),
1214 (@{const_name card}, @{const_name card'}),
1215 (@{const_name setsum}, @{const_name setsum'}),
1216 (@{const_name fold_graph}, @{const_name fold_graph'}),
1217 (@{const_name wf}, @{const_name wf'}),
1218 (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
1219 (@{const_name wfrec}, @{const_name wfrec'})]
1221 (* theory -> (string * string) list *)
1222 fun ersatz_table thy =
1223 fold (append o snd) (#frac_types (TheoryData.get thy)) basic_ersatz_table
1225 (* const_table Unsynchronized.ref -> string -> term list -> unit *)
1226 fun add_simps simp_table s eqs =
1227 Unsynchronized.change simp_table
1228 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
1230 (* Similar to "Refute.specialize_type" but returns all matches rather than only
1231 the first (preorder) match. *)
1232 (* theory -> styp -> term -> term list *)
1233 fun multi_specialize_type thy slack (x as (s, T)) t =
1235 (* term -> (typ * term) list -> (typ * term) list *)
1236 fun aux (Const (s', T')) ys =
1238 ys |> (if AList.defined (op =) ys T' then
1241 cons (T', Refute.monomorphic_term
1242 (Sign.typ_match thy (T', T) Vartab.empty) t)
1243 handle Type.TYPE_MATCH => I
1244 | Refute.REFUTE _ =>
1248 raise NOT_SUPPORTED ("too much polymorphism in \
1249 \axiom involving " ^ quote s))
1253 in map snd (fold_aterms aux t []) end
1255 (* theory -> bool -> const_table -> styp -> term list *)
1256 fun nondef_props_for_const thy slack table (x as (s, _)) =
1257 these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
1259 (* theory -> styp list -> term list *)
1260 fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
1261 let val abs_T = Type (abs_s, abs_Ts) in
1262 if is_univ_typedef thy abs_T then
1264 else case typedef_info thy abs_s of
1265 SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,
1268 val rep_T = instantiate_type thy abs_type abs_T rep_type
1269 val rep_t = Const (Rep_name, abs_T --> rep_T)
1270 val set_t = Const (set_name, rep_T --> bool_T)
1272 prop_of_Rep |> HOLogic.dest_Trueprop
1273 |> Refute.specialize_type thy (dest_Const rep_t)
1274 |> HOLogic.dest_mem |> snd
1276 [HOLogic.all_const abs_T
1277 $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
1278 |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
1279 |> map HOLogic.mk_Trueprop
1283 (* theory -> styp -> term *)
1284 fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
1285 typedef_info thy (fst (dest_Type (domain_type T)))
1286 |> the |> #Rep_inverse |> the |> prop_of |> Refute.specialize_type thy x
1288 (* theory -> int * styp -> term *)
1289 fun constr_case_body thy (j, (x as (_, T))) =
1290 let val arg_Ts = binder_types T in
1291 list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
1292 (index_seq 0 (length arg_Ts)) arg_Ts)
1294 (* extended_context -> typ -> int * styp -> term -> term *)
1295 fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
1296 Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
1297 $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
1299 (* extended_context -> typ -> typ -> term *)
1300 fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
1302 val xs = datatype_constrs ext_ctxt dataT
1303 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
1304 val (xs', x) = split_last xs
1306 constr_case_body thy (1, x)
1307 |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
1308 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
1311 (* extended_context -> string -> typ -> typ -> term -> term *)
1312 fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
1313 let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
1314 case no_of_record_field thy s rec_T of
1315 ~1 => (case rec_T of
1316 Type (_, Ts as _ :: _) =>
1318 val rec_T' = List.last Ts
1319 val j = num_record_fields thy rec_T - 1
1321 select_nth_constr_arg thy constr_x t j res_T
1322 |> optimized_record_get ext_ctxt s rec_T' res_T
1324 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
1326 | j => select_nth_constr_arg thy constr_x t j res_T
1328 (* extended_context -> string -> typ -> term -> term -> term *)
1329 fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
1331 val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
1332 val Ts = binder_types constr_T
1334 val special_j = no_of_record_field thy s rec_T
1335 val ts = map2 (fn j => fn T =>
1337 val t = select_nth_constr_arg thy constr_x rec_t j T
1339 if j = special_j then
1341 else if j = n - 1 andalso special_j = ~1 then
1342 optimized_record_update ext_ctxt s
1343 (rec_T |> dest_Type |> snd |> List.last) fun_t t
1346 end) (index_seq 0 n) Ts
1347 in list_comb (Const constr_x, ts) end
1349 (* Constants "c" whose definition is of the form "c == c'", where "c'" is also a
1350 constant, are said to be trivial. For those, we ignore the simplification
1351 rules and use the definition instead, to ensure that built-in symbols like
1352 "ord_nat_inst.less_eq_nat" are picked up correctly. *)
1353 (* theory -> const_table -> styp -> bool *)
1354 fun has_trivial_definition thy table x =
1355 case def_of_const thy table x of SOME (Const _) => true | _ => false
1357 (* theory -> const_table -> string * typ -> fixpoint_kind *)
1358 fun fixpoint_kind_of_const thy table x =
1359 if is_built_in_const false x then
1362 fixpoint_kind_of_rhs (the (def_of_const thy table x))
1363 handle Option.Option => NoFp
1365 (* extended_context -> styp -> bool *)
1366 fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
1367 : extended_context) x =
1368 not (null (def_props_for_const thy fast_descrs intro_table x))
1369 andalso fixpoint_kind_of_const thy def_table x <> NoFp
1370 fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
1371 : extended_context) x =
1372 exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
1373 [!simp_table, psimp_table]
1374 fun is_inductive_pred ext_ctxt =
1375 is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
1376 fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
1377 (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
1378 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
1379 andf (not o has_trivial_definition thy def_table)
1381 (* term * term -> term *)
1382 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
1383 | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
1384 | s_betapply p = betapply p
1385 (* term * term list -> term *)
1386 val s_betapplys = Library.foldl s_betapply
1389 fun lhs_of_equation t =
1391 Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1392 | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
1393 | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
1394 | @{const Trueprop} $ t1 => lhs_of_equation t1
1395 | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1396 | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
1397 | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
1399 (* theory -> term -> bool *)
1400 fun is_constr_pattern _ (Bound _) = true
1401 | is_constr_pattern thy t =
1402 case strip_comb t of
1403 (Const (x as (s, _)), args) =>
1404 is_constr_like thy x andalso forall (is_constr_pattern thy) args
1406 fun is_constr_pattern_lhs thy t =
1407 forall (is_constr_pattern thy) (snd (strip_comb t))
1408 fun is_constr_pattern_formula thy t =
1409 case lhs_of_equation t of
1410 SOME t' => is_constr_pattern_lhs thy t'
1413 val unfold_max_depth = 63
1414 val axioms_max_depth = 63
1416 (* extended_context -> term -> term *)
1417 fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
1418 case_names, def_table, ground_thm_table,
1419 ersatz_table, ...}) =
1421 (* int -> typ list -> term -> term *)
1422 fun do_term depth Ts t =
1424 (t0 as Const (@{const_name Int.number_class.number_of},
1425 Type ("fun", [_, ran_T]))) $ t1 =>
1426 ((if is_number_type thy ran_T then
1428 val j = t1 |> HOLogic.dest_numeral
1429 |> ran_T <> int_T ? curry Int.max 0
1430 val s = numeral_prefix ^ signed_string_of_int j
1432 if is_integer_type ran_T then
1435 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
1438 handle TERM _ => raise SAME ()
1441 handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
1442 | Const (@{const_name refl_on}, T) $ Const (@{const_name UNIV}, _) $ t2 =>
1443 do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
1444 | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
1445 $ (t2 as Abs (_, _, t2')) =>
1446 betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
1447 map (do_term depth Ts) [t1, t2])
1448 | Const (x as (@{const_name distinct},
1449 Type ("fun", [Type (@{type_name list}, [T']), _])))
1451 (t1 |> HOLogic.dest_list |> distinctness_formula T'
1452 handle TERM _ => do_const depth Ts t x [t1])
1453 | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
1454 if is_ground_term t1
1455 andalso exists (Pattern.matches thy o rpair t1)
1456 (Inttab.lookup_list ground_thm_table
1457 (hash_term t1)) then
1460 do_const depth Ts t x [t1, t2, t3]
1461 | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
1462 | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
1463 | Const x $ t1 => do_const depth Ts t x [t1]
1464 | Const x => do_const depth Ts t x []
1465 | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
1469 | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
1470 (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
1471 and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
1472 (Abs (Name.uu, body_type T,
1473 select_nth_constr_arg thy x (Bound 0) n res_T), [])
1474 | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
1475 (select_nth_constr_arg thy x (do_term depth Ts t) n res_T, ts)
1476 (* int -> typ list -> term -> styp -> term list -> term *)
1477 and do_const depth Ts t (x as (s, T)) ts =
1478 case AList.lookup (op =) ersatz_table s of
1480 do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
1484 if is_built_in_const fast_descrs x then
1485 if s = @{const_name finite} then
1486 if is_finite_type ext_ctxt (domain_type T) then
1487 (Abs ("A", domain_type T, @{const True}), ts)
1489 [Const (@{const_name UNIV}, _)] => (@{const False}, [])
1490 | _ => (Const x, ts)
1493 else case AList.lookup (op =) case_names s of
1496 val (dataT, res_T) = nth_range_type n T
1497 |> domain_type pairf range_type
1499 (optimized_case_def ext_ctxt dataT res_T
1500 |> do_term (depth + 1) Ts, ts)
1503 if is_constr thy x then
1505 else if is_record_get thy x then
1507 0 => (do_term depth Ts (eta_expand Ts t 1), [])
1508 | _ => (optimized_record_get ext_ctxt s (domain_type T)
1509 (range_type T) (hd ts), tl ts)
1510 else if is_record_update thy x then
1512 2 => (optimized_record_update ext_ctxt
1513 (unsuffix Record.updateN s) (nth_range_type 2 T)
1514 (do_term depth Ts (hd ts))
1515 (do_term depth Ts (nth ts 1)), [])
1516 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
1517 else if is_rep_fun thy x then
1518 let val x' = mate_of_rep_fun thy x in
1519 if is_constr thy x' then
1520 select_nth_constr_arg_with_args depth Ts x' ts 0
1525 else if is_equational_fun ext_ctxt x then
1527 else case def_of_const thy def_table x of
1529 if depth > unfold_max_depth then
1530 raise LIMIT ("Nitpick_HOL.unfold_defs_in_term",
1531 "too many nested definitions (" ^
1532 string_of_int depth ^ ") while expanding " ^
1534 else if s = @{const_name wfrec'} then
1535 (do_term (depth + 1) Ts (betapplys (def, ts)), [])
1537 (do_term (depth + 1) Ts def, ts)
1538 | NONE => (Const x, ts)
1539 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
1542 (* extended_context -> typ -> term list *)
1543 fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
1545 val xs = datatype_constrs ext_ctxt T
1546 val set_T = T --> bool_T
1547 val iter_T = @{typ bisim_iterator}
1548 val bisim_const = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
1549 val bisim_max = @{const bisim_iterator_max}
1550 val n_var = Var (("n", 0), iter_T)
1552 Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T)
1553 $ Abs ("m", iter_T, HOLogic.eq_const iter_T
1554 $ (suc_const iter_T $ Bound 0) $ n_var)
1555 val x_var = Var (("x", 0), T)
1556 val y_var = Var (("y", 0), T)
1557 (* styp -> int -> typ -> term *)
1558 fun nth_sub_bisim x n nth_T =
1559 (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
1560 else HOLogic.eq_const nth_T)
1561 $ select_nth_constr_arg thy x x_var n nth_T
1562 $ select_nth_constr_arg thy x y_var n nth_T
1564 fun case_func (x as (_, T)) =
1566 val arg_Ts = binder_types T
1568 discriminate_value ext_ctxt x y_var ::
1569 map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
1571 in List.foldr absdummy core_t arg_Ts end
1573 [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
1574 $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
1575 $ (betapplys (optimized_case_def ext_ctxt T bool_T,
1576 map case_func xs @ [x_var]))),
1577 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
1578 $ (Const (@{const_name insert}, [T, set_T] ---> set_T)
1579 $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
1580 |> map HOLogic.mk_Trueprop
1583 exception NO_TRIPLE of unit
1585 (* theory -> styp -> term -> term list * term list * term *)
1586 fun triple_for_intro_rule thy x t =
1588 val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
1589 val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
1590 val (main, side) = List.partition (exists_Const (equal x)) prems
1592 val is_good_head = equal (Const x) o head_of
1594 if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
1598 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
1600 (* indexname * typ -> term list -> term -> term -> term *)
1601 fun wf_constraint_for rel side concl main =
1603 val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
1604 tuple_for_args concl), Var rel)
1605 val t = List.foldl HOLogic.mk_imp core side
1606 val vars = filter (not_equal rel) (Term.add_vars t [])
1608 Library.foldl (fn (t', ((x, j), T)) =>
1610 $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
1614 (* indexname * typ -> term list * term list * term -> term *)
1615 fun wf_constraint_for_triple rel (side, main, concl) =
1616 map (wf_constraint_for rel side concl) main |> foldr1 s_conj
1618 (* Proof.context -> Time.time option -> thm
1619 -> (Proof.context -> tactic -> tactic) -> bool *)
1620 fun terminates_by ctxt timeout goal tac =
1621 can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
1622 #> SINGLE (DETERM_TIMEOUT timeout
1623 (tac ctxt (auto_tac (clasimpset_of ctxt))))
1624 #> the #> Goal.finish ctxt) goal
1626 val max_cached_wfs = 100
1627 val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
1628 val cached_wf_props : (term * bool) list Unsynchronized.ref =
1629 Unsynchronized.ref []
1631 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
1632 ScnpReconstruct.sizechange_tac]
1634 (* extended_context -> const_table -> styp -> bool *)
1635 fun uncached_is_well_founded_inductive_pred
1636 ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
1637 : extended_context) (x as (_, T)) =
1638 case def_props_for_const thy fast_descrs intro_table x of
1639 [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
1642 (case map (triple_for_intro_rule thy x) intro_ts
1643 |> filter_out (null o #2) of
1647 val binders_T = HOLogic.mk_tupleT (binder_types T)
1648 val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
1649 val j = List.foldl Int.max 0 (map maxidx_of_term intro_ts) + 1
1650 val rel = (("R", j), rel_T)
1651 val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
1652 map (wf_constraint_for_triple rel) triples
1653 |> foldr1 s_conj |> HOLogic.mk_Trueprop
1654 val _ = if debug then
1655 priority ("Wellfoundedness goal: " ^
1656 Syntax.string_of_term ctxt prop ^ ".")
1660 if tac_timeout = (!cached_timeout)
1661 andalso length (!cached_wf_props) < max_cached_wfs then
1664 (cached_wf_props := []; cached_timeout := tac_timeout);
1665 case AList.lookup (op =) (!cached_wf_props) prop of
1669 val goal = prop |> cterm_of thy |> Goal.init
1670 val wf = silence (exists (terminates_by ctxt tac_timeout goal))
1672 in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
1674 handle List.Empty => false
1675 | NO_TRIPLE () => false
1677 (* The type constraint below is a workaround for a Poly/ML bug. *)
1679 (* extended_context -> styp -> bool *)
1680 fun is_well_founded_inductive_pred
1681 (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context)
1683 case triple_lookup (const_match thy) wfs x of
1685 | _ => s mem [@{const_name Nats}, @{const_name fold_graph'}]
1686 orelse case AList.lookup (op =) (!wf_cache) x of
1690 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
1691 val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
1693 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
1696 (* typ list -> typ -> typ -> term -> term *)
1697 fun ap_curry [_] _ _ t = t
1698 | ap_curry arg_Ts tuple_T body_T t =
1699 let val n = length arg_Ts in
1700 list_abs (map (pair "c") arg_Ts,
1702 $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
1705 (* int -> term -> int *)
1706 fun num_occs_of_bound_in_term j (t1 $ t2) =
1707 op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
1708 | num_occs_of_bound_in_term j (Abs (s, T, t')) =
1709 num_occs_of_bound_in_term (j + 1) t'
1710 | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
1711 | num_occs_of_bound_in_term _ _ = 0
1714 val is_linear_inductive_pred_def =
1716 (* int -> term -> bool *)
1717 fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
1718 do_disjunct (j + 1) t2
1720 case num_occs_of_bound_in_term j t of
1722 | 1 => exists (equal (Bound j) o head_of) (conjuncts t)
1725 fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
1726 let val (xs, body) = strip_abs t2 in
1729 | n => forall (do_disjunct (n - 1)) (disjuncts body)
1731 | do_lfp_def _ = false
1732 in do_lfp_def o strip_abs_body end
1734 (* typ -> typ -> term -> term *)
1735 fun ap_split tuple_T =
1736 HOLogic.mk_psplits (HOLogic.flat_tupleT_paths tuple_T) tuple_T
1738 (* term -> term * term *)
1739 val linear_pred_base_and_step_rhss =
1742 fun aux (Const (@{const_name lfp}, _) $ t2) =
1744 val (xs, body) = strip_abs t2
1745 val arg_Ts = map snd (tl xs)
1746 val tuple_T = HOLogic.mk_tupleT arg_Ts
1747 val j = length arg_Ts
1748 (* int -> term -> term *)
1749 fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
1750 Const (@{const_name Ex}, T1)
1751 $ Abs (s2, T2, repair_rec (j + 1) t2')
1752 | repair_rec j (@{const "op &"} $ t1 $ t2) =
1753 @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
1755 let val (head, args) = strip_comb t in
1756 if head = Bound j then
1757 HOLogic.eq_const tuple_T $ Bound j
1758 $ mk_flat_tuple tuple_T args
1762 val (nonrecs, recs) =
1763 List.partition (equal 0 o num_occs_of_bound_in_term j)
1765 val base_body = nonrecs |> List.foldl s_disj @{const False}
1766 val step_body = recs |> map (repair_rec j)
1767 |> List.foldl s_disj @{const False}
1769 (list_abs (tl xs, incr_bv (~1, j, base_body))
1770 |> ap_split tuple_T bool_T,
1771 Abs ("y", tuple_T, list_abs (tl xs, step_body)
1772 |> ap_split tuple_T bool_T))
1775 raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
1778 (* extended_context -> styp -> term -> term *)
1779 fun closed_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T)) def =
1781 val j = maxidx_of_term def + 1
1782 val (outer, fp_app) = strip_abs def
1783 val outer_bounds = map Bound (length outer - 1 downto 0)
1784 val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer
1785 val fp_app = subst_bounds (rev outer_vars, fp_app)
1786 val (outer_Ts, rest_T) = strip_n_binders (length outer) T
1787 val tuple_arg_Ts = strip_type rest_T |> fst
1788 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
1789 val set_T = tuple_T --> bool_T
1790 val curried_T = tuple_T --> set_T
1791 val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
1792 val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
1793 val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
1794 val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
1795 |> HOLogic.mk_Trueprop
1796 val _ = add_simps simp_table base_s [base_eq]
1797 val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T)
1798 val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs)
1799 |> HOLogic.mk_Trueprop
1800 val _ = add_simps simp_table step_s [step_eq]
1803 Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
1804 $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
1805 $ (Const (@{const_name split}, curried_T --> uncurried_T)
1806 $ list_comb (Const step_x, outer_bounds)))
1807 $ list_comb (Const base_x, outer_bounds)
1808 |> ap_curry tuple_arg_Ts tuple_T bool_T)
1809 |> unfold_defs_in_term ext_ctxt
1812 (* extended_context -> bool -> styp -> term *)
1813 fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds,
1814 def_table, simp_table, ...})
1817 val iter_T = iterator_type_for_const gfp x
1818 val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
1819 val unrolled_const = Const x' $ zero_const iter_T
1820 val def = the (def_of_const thy def_table x)
1822 if is_equational_fun ext_ctxt x' then
1823 unrolled_const (* already done *)
1824 else if not gfp andalso is_linear_inductive_pred_def def
1825 andalso star_linear_preds then
1826 closed_linear_pred_const ext_ctxt x def
1829 val j = maxidx_of_term def + 1
1830 val (outer, fp_app) = strip_abs def
1831 val outer_bounds = map Bound (length outer - 1 downto 0)
1832 val cur = Var ((iter_var_prefix, j + 1), iter_T)
1833 val next = suc_const iter_T $ cur
1834 val rhs = case fp_app of
1836 betapply (t, list_comb (Const x', next :: outer_bounds))
1837 | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
1839 val (inner, naked_rhs) = strip_abs rhs
1840 val all = outer @ inner
1841 val bounds = map Bound (length all - 1 downto 0)
1842 val vars = map (fn (s, T) => Var ((s, j), T)) all
1843 val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs)
1844 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
1845 val _ = add_simps simp_table s' [eq]
1846 in unrolled_const end
1849 (* extended_context -> styp -> term *)
1850 fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x =
1852 val def = the (def_of_const thy def_table x)
1853 val (outer, fp_app) = strip_abs def
1854 val outer_bounds = map Bound (length outer - 1 downto 0)
1855 val rhs = case fp_app of
1856 Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
1857 | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
1859 val (inner, naked_rhs) = strip_abs rhs
1860 val all = outer @ inner
1861 val bounds = map Bound (length all - 1 downto 0)
1862 val j = maxidx_of_term def + 1
1863 val vars = map (fn (s, T) => Var ((s, j), T)) all
1865 HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
1866 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
1868 fun inductive_pred_axiom ext_ctxt (x as (s, T)) =
1869 if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
1870 let val x' = (after_name_sep s, T) in
1871 raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)]
1874 raw_inductive_pred_axiom ext_ctxt x
1876 (* extended_context -> styp -> term list *)
1877 fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
1878 psimp_table, ...}) (x as (s, _)) =
1879 case def_props_for_const thy fast_descrs (!simp_table) x of
1880 [] => (case def_props_for_const thy fast_descrs psimp_table x of
1881 [] => [inductive_pred_axiom ext_ctxt x]
1885 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
1887 (* term list -> term list *)
1888 fun merge_type_vars_in_terms ts =
1890 (* typ -> (sort * string) list -> (sort * string) list *)
1891 fun add_type (TFree (s, S)) table =
1892 (case AList.lookup (op =) table S of
1894 if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
1896 | NONE => (S, s) :: table)
1897 | add_type _ table = table
1898 val table = fold (fold_types (fold_atyps add_type)) ts []
1900 fun coalesce (TFree (s, S)) = TFree (AList.lookup (op =) table S |> the, S)
1902 in map (map_types (map_atyps coalesce)) ts end
1904 (* extended_context -> typ -> typ list -> typ list *)
1905 fun add_ground_types ext_ctxt T accum =
1907 Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum
1908 | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
1909 | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
1911 if T mem @{typ prop} :: @{typ bool} :: @{typ unit} :: accum then
1915 |> fold (add_ground_types ext_ctxt)
1916 (case boxed_datatype_constrs ext_ctxt T of
1919 | _ => insert (op =) T accum
1920 (* extended_context -> typ -> typ list *)
1921 fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T []
1922 (* extended_context -> term list -> typ list *)
1923 fun ground_types_in_terms ext_ctxt ts =
1924 fold (fold_types (add_ground_types ext_ctxt)) ts []
1926 (* typ list -> int -> term -> bool *)
1927 fun has_heavy_bounds_or_vars Ts level t =
1929 (* typ list -> bool *)
1931 | aux [T] = is_fun_type T orelse is_pair_type T
1933 in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
1935 (* typ list -> int -> int -> int -> term -> term *)
1936 fun fresh_value_var Ts k n j t =
1937 Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
1939 (* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
1940 -> term * term list *)
1941 fun pull_out_constr_comb thy Ts relax k level t args seen =
1942 let val t_comb = list_comb (t, args) in
1945 if not relax andalso is_constr thy x
1946 andalso not (is_fun_type (fastype_of1 (Ts, t_comb)))
1947 andalso has_heavy_bounds_or_vars Ts level t_comb
1948 andalso not (loose_bvar (t_comb, level)) then
1950 val (j, seen) = case find_index (equal t_comb) seen of
1951 ~1 => (0, t_comb :: seen)
1953 in (fresh_value_var Ts k (length seen) j t_comb, seen) end
1956 | _ => (t_comb, seen)
1959 (* (term -> term) -> typ list -> int -> term list -> term list *)
1960 fun equations_for_pulled_out_constrs mk_eq Ts k seen =
1961 let val n = length seen in
1962 map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
1963 (index_seq 0 n) seen
1966 (* theory -> bool -> term -> term *)
1967 fun pull_out_universal_constrs thy def t =
1969 val k = maxidx_of_term t + 1
1970 (* typ list -> bool -> term -> term list -> term list -> term * term list *)
1971 fun do_term Ts def t args seen =
1973 (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
1974 do_eq_or_imp Ts def t0 t1 t2 seen
1975 | (t0 as @{const "==>"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
1976 | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
1977 do_eq_or_imp Ts def t0 t1 t2 seen
1978 | (t0 as @{const "op -->"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
1980 let val (t', seen) = do_term (T :: Ts) def t' [] seen in
1981 (list_comb (Abs (s, T, t'), args), seen)
1984 let val (t2, seen) = do_term Ts def t2 [] seen in
1985 do_term Ts def t1 (t2 :: args) seen
1987 | _ => pull_out_constr_comb thy Ts def k 0 t args seen
1988 (* typ list -> bool -> term -> term -> term -> term list
1989 -> term * term list *)
1990 and do_eq_or_imp Ts def t0 t1 t2 seen =
1992 val (t2, seen) = do_term Ts def t2 [] seen
1993 val (t1, seen) = do_term Ts false t1 [] seen
1994 in (t0 $ t1 $ t2, seen) end
1995 val (concl, seen) = do_term [] def t [] []
1997 Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
2001 (* extended_context -> bool -> term -> term *)
2002 fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
2005 val num_occs_of_var =
2006 fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
2008 (* bool -> term -> term *)
2009 fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
2010 aux_eq careful true t0 t1 t2
2011 | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
2012 t0 $ aux false t1 $ aux careful t2
2013 | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
2014 aux_eq careful true t0 t1 t2
2015 | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
2016 t0 $ aux false t1 $ aux careful t2
2017 | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
2018 | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
2020 (* bool -> bool -> term -> term -> term -> term *)
2021 and aux_eq careful pass1 t0 t1 t2 =
2024 else if axiom andalso is_Var t2
2025 andalso num_occs_of_var (dest_Var t2) = 1 then
2027 else case strip_comb t2 of
2028 (Const (x as (s, T)), args) =>
2029 let val arg_Ts = binder_types T in
2030 if length arg_Ts = length args
2031 andalso (is_constr thy x orelse s mem [@{const_name Pair}]
2032 orelse x = dest_Const @{const Suc})
2033 andalso (not careful orelse not (is_Var t1)
2034 orelse String.isPrefix val_var_prefix
2035 (fst (fst (dest_Var t1)))) then
2036 discriminate_value ext_ctxt x t1 ::
2037 map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
2039 |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
2043 | _ => raise SAME ())
2044 handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
2045 else t0 $ aux false t2 $ aux false t1
2046 (* styp -> term -> int -> typ -> term -> term *)
2047 and sel_eq x t n nth_T nth_t =
2048 HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
2052 (* theory -> term -> term *)
2053 fun simplify_constrs_and_sels thy t =
2055 (* term -> int -> term *)
2056 fun is_nth_sel_on t' n (Const (s, _) $ t) =
2057 (t = t' andalso is_sel_like_and_no_discr s
2058 andalso sel_no_from_name s = n)
2059 | is_nth_sel_on _ _ _ = false
2060 (* term -> term list -> term *)
2061 fun do_term (Const (@{const_name Rep_Frac}, _)
2062 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
2063 | do_term (Const (@{const_name Abs_Frac}, _)
2064 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
2065 | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
2066 | do_term (t as Const (x as (s, T))) (args as _ :: _) =
2067 ((if is_constr_like thy x then
2068 if length args = num_binder_types T then
2070 Const (x' as (_, T')) $ t' =>
2071 if domain_type T' = body_type T
2072 andalso forall (uncurry (is_nth_sel_on t'))
2073 (index_seq 0 (length args) ~~ args) then
2077 | _ => raise SAME ()
2080 else if is_sel_like_and_no_discr s then
2081 case strip_comb (hd args) of
2082 (Const (x' as (s', T')), ts') =>
2083 if is_constr_like thy x'
2084 andalso constr_name_for_sel_like s = s'
2085 andalso not (exists is_pair_type (binder_types T')) then
2086 list_comb (nth ts' (sel_no_from_name s), tl args)
2089 | _ => raise SAME ()
2092 handle SAME () => betapplys (t, args))
2093 | do_term (Abs (s, T, t')) args =
2094 betapplys (Abs (s, T, do_term t' []), args)
2095 | do_term t args = betapplys (t, args)
2099 fun curry_assms (@{const "==>"} $ (@{const Trueprop}
2100 $ (@{const "op &"} $ t1 $ t2)) $ t3) =
2101 curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
2102 | curry_assms (@{const "==>"} $ t1 $ t2) =
2103 @{const "==>"} $ curry_assms t1 $ curry_assms t2
2107 val destroy_universal_equalities =
2109 (* term list -> (indexname * typ) list -> term -> term *)
2110 fun aux prems zs t =
2112 @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
2113 | _ => Logic.list_implies (rev prems, t)
2114 (* term list -> (indexname * typ) list -> term -> term -> term *)
2115 and aux_implies prems zs t1 t2 =
2117 Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
2118 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
2119 aux_eq prems zs z t' t1 t2
2120 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
2121 aux_eq prems zs z t' t1 t2
2122 | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
2123 (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
2125 and aux_eq prems zs z t' t1 t2 =
2126 if not (z mem zs) andalso not (exists_subterm (equal (Var z)) t') then
2127 aux prems zs (subst_free [(Var z, t')] t2)
2129 aux (t1 :: prems) (Term.add_vars t1 zs) t2
2132 (* theory -> term -> term *)
2133 fun pull_out_existential_constrs thy t =
2135 val k = maxidx_of_term t + 1
2136 (* typ list -> int -> term -> term list -> term list -> term * term list *)
2137 fun aux Ts num_exists t args seen =
2139 (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
2141 val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
2142 val n = length seen'
2143 (* unit -> term list *)
2144 fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
2146 (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
2147 |> List.foldl s_conj t1 |> fold mk_exists (vars ())
2148 |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
2151 let val (t2, seen) = aux Ts num_exists t2 [] seen in
2152 aux Ts num_exists t1 (t2 :: args) seen
2156 val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
2157 in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
2159 if num_exists > 0 then
2160 pull_out_constr_comb thy Ts false k num_exists t args seen
2162 (list_comb (t, args), seen)
2163 in aux [] 0 t [] [] |> fst end
2165 (* theory -> int -> term list -> term list -> (term * term list) option *)
2166 fun find_bound_assign _ _ _ [] = NONE
2167 | find_bound_assign thy j seen (t :: ts) =
2169 (* bool -> term -> term -> (term * term list) option *)
2170 fun aux pass1 t1 t2 =
2171 (if loose_bvar1 (t2, j) then
2172 if pass1 then aux false t2 t1 else raise SAME ()
2174 Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
2175 | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
2176 if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then
2177 SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
2181 | _ => raise SAME ())
2182 handle SAME () => find_bound_assign thy j (t :: seen) ts
2185 Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
2186 | _ => find_bound_assign thy j (t :: seen) ts
2189 (* int -> term -> term -> term *)
2190 fun subst_one_bound j arg t =
2192 fun aux (Bound i, lev) =
2193 if i < lev then raise SAME ()
2194 else if i = lev then incr_boundvars (lev - j) arg
2196 | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
2197 | aux (f $ t, lev) =
2198 (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
2199 handle SAME () => f $ aux (t, lev))
2200 | aux _ = raise SAME ()
2201 in aux (t, j) handle SAME () => t end
2203 (* theory -> term -> term *)
2204 fun destroy_existential_equalities thy =
2206 (* string list -> typ list -> term list -> term *)
2207 fun kill [] [] ts = foldr1 s_conj ts
2208 | kill (s :: ss) (T :: Ts) ts =
2209 (case find_bound_assign thy (length ss) [] ts of
2210 SOME (_, []) => @{const True}
2211 | SOME (arg_t, ts) =>
2212 kill ss Ts (map (subst_one_bound (length ss)
2213 (incr_bv (~1, length ss + 1, arg_t))) ts)
2215 Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
2216 $ Abs (s, T, kill ss Ts ts))
2217 | kill _ _ _ = raise UnequalLengths
2218 (* string list -> typ list -> term -> term *)
2219 fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
2220 gather (ss @ [s1]) (Ts @ [T1]) t1
2221 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
2222 | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
2223 | gather [] [] t = t
2224 | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t))
2228 fun distribute_quantifiers t =
2230 (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
2232 (t10 as @{const "op &"}) $ t11 $ t12 =>
2233 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
2234 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
2235 | (t10 as @{const Not}) $ t11 =>
2236 t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
2239 if not (loose_bvar1 (t1, 0)) then
2240 distribute_quantifiers (incr_boundvars ~1 t1)
2242 t0 $ Abs (s, T1, distribute_quantifiers t1))
2243 | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
2244 (case distribute_quantifiers t1 of
2245 (t10 as @{const "op |"}) $ t11 $ t12 =>
2246 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
2247 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
2248 | (t10 as @{const "op -->"}) $ t11 $ t12 =>
2249 t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
2251 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
2252 | (t10 as @{const Not}) $ t11 =>
2253 t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
2256 if not (loose_bvar1 (t1, 0)) then
2257 distribute_quantifiers (incr_boundvars ~1 t1)
2259 t0 $ Abs (s, T1, distribute_quantifiers t1))
2260 | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
2261 | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
2264 (* int -> int -> (int -> int) -> term -> term *)
2265 fun renumber_bounds j n f t =
2267 t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
2268 | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
2270 Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
2273 val quantifier_cluster_max_size = 8
2275 (* theory -> term -> term *)
2276 fun push_quantifiers_inward thy =
2278 (* string -> string list -> typ list -> term -> term *)
2279 fun aux quant_s ss Ts t =
2281 (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
2282 if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
2283 aux s0 (s1 :: ss) (T1 :: Ts) t1
2284 else if quant_s = ""
2285 andalso s0 mem [@{const_name All}, @{const_name Ex}] then
2289 | _ => raise SAME ())
2293 if quant_s = "" then
2294 aux "" [] [] t1 $ aux "" [] [] t2
2297 val typical_card = 4
2298 (* ('a -> ''b list) -> 'a list -> ''b list *)
2299 fun big_union proj ps =
2300 fold (fold (insert (op =)) o proj) ps []
2301 val (ts, connective) = strip_any_connective t
2303 map (bounded_card_of_type 65536 typical_card []) Ts
2304 val t_costs = map size_of_term ts
2305 val num_Ts = length Ts
2307 val flip = curry (op -) (num_Ts - 1)
2308 val t_boundss = map (map flip o loose_bnos) ts
2309 (* (int list * int) list -> int list -> int *)
2310 fun cost boundss_cum_costs [] =
2311 map snd boundss_cum_costs |> Integer.sum
2312 | cost boundss_cum_costs (j :: js) =
2315 List.partition (fn (bounds, _) => j mem bounds)
2317 val yeas_bounds = big_union fst yeas
2318 val yeas_cost = Integer.sum (map snd yeas)
2320 in cost ((yeas_bounds, yeas_cost) :: nays) js end
2321 val js = all_permutations (index_seq 0 num_Ts)
2322 |> map (`(cost (t_boundss ~~ t_costs)))
2323 |> sort (int_ord o pairself fst) |> hd |> snd
2324 val back_js = map (fn j => find_index (equal j) js)
2325 (index_seq 0 num_Ts)
2326 val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
2328 (* (term * int list) list -> term *)
2329 fun mk_connection [] =
2330 raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
2331 \mk_connection", "")
2332 | mk_connection ts_cum_bounds =
2333 ts_cum_bounds |> map fst
2334 |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
2335 (* (term * int list) list -> int list -> term *)
2336 fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
2337 | build ts_cum_bounds (j :: js) =
2340 List.partition (fn (_, bounds) => j mem bounds)
2342 ||> map (apfst (incr_boundvars ~1))
2347 let val T = nth Ts (flip j) in
2348 build ((Const (quant_s, (T --> bool_T) --> bool_T)
2349 $ Abs (nth ss (flip j), T,
2350 mk_connection yeas),
2351 big_union snd yeas) :: nays) js
2354 in build (ts ~~ t_boundss) js end
2355 | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
2359 (* polarity -> string -> bool *)
2360 fun is_positive_existential polar quant_s =
2361 (polar = Pos andalso quant_s = @{const_name Ex})
2362 orelse (polar = Neg andalso quant_s <> @{const_name Ex})
2364 (* extended_context -> int -> term -> term *)
2365 fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
2368 (* int list -> int list *)
2369 val incrs = map (Integer.add 1)
2370 (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
2371 fun aux ss Ts js depth polar t =
2373 (* string -> typ -> string -> typ -> term -> term *)
2374 fun do_quantifier quant_s quant_T abs_s abs_T t =
2375 if not (loose_bvar1 (t, 0)) then
2376 aux ss Ts js depth polar (incr_boundvars ~1 t)
2377 else if depth <= skolem_depth
2378 andalso is_positive_existential polar quant_s then
2380 val j = length (!skolems) + 1
2381 val sko_s = skolem_prefix_for (length js) j ^ abs_s
2382 val _ = Unsynchronized.change skolems (cons (sko_s, ss))
2383 val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
2385 val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
2387 if null js then betapply (abs_t, sko_t)
2388 else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
2391 Const (quant_s, quant_T)
2392 $ Abs (abs_s, abs_T,
2393 if is_higher_order_type abs_T then
2396 aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
2397 (depth + 1) polar t)
2400 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
2401 do_quantifier s0 T0 s1 T1 t1
2402 | @{const "==>"} $ t1 $ t2 =>
2403 @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
2404 $ aux ss Ts js depth polar t2
2405 | @{const Pure.conjunction} $ t1 $ t2 =>
2406 @{const Pure.conjunction} $ aux ss Ts js depth polar t1
2407 $ aux ss Ts js depth polar t2
2408 | @{const Trueprop} $ t1 =>
2409 @{const Trueprop} $ aux ss Ts js depth polar t1
2410 | @{const Not} $ t1 =>
2411 @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
2412 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
2413 do_quantifier s0 T0 s1 T1 t1
2414 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
2415 do_quantifier s0 T0 s1 T1 t1
2416 | @{const "op &"} $ t1 $ t2 =>
2417 @{const "op &"} $ aux ss Ts js depth polar t1
2418 $ aux ss Ts js depth polar t2
2419 | @{const "op |"} $ t1 $ t2 =>
2420 @{const "op |"} $ aux ss Ts js depth polar t1
2421 $ aux ss Ts js depth polar t2
2422 | @{const "op -->"} $ t1 $ t2 =>
2423 @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
2424 $ aux ss Ts js depth polar t2
2425 | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
2426 t0 $ t1 $ aux ss Ts js depth polar t2
2427 | Const (x as (s, T)) =>
2428 if is_inductive_pred ext_ctxt x
2429 andalso not (is_well_founded_inductive_pred ext_ctxt x) then
2431 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
2432 val (pref, connective, set_oper) =
2436 @{const_name upper_semilattice_fun_inst.sup_fun})
2440 @{const_name lower_semilattice_fun_inst.inf_fun})
2442 fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x
2443 |> aux ss Ts js depth polar
2444 fun neg () = Const (pref ^ s, T)
2446 (case polar |> gfp ? flip_polarity of
2450 if is_fun_type T then
2452 val ((trunk_arg_Ts, rump_arg_T), body_T) =
2453 T |> strip_type |>> split_last
2454 val set_T = rump_arg_T --> body_T
2455 (* (unit -> term) -> term *)
2458 map Bound (length trunk_arg_Ts - 1 downto 0))
2461 (Const (set_oper, [set_T, set_T] ---> set_T)
2462 $ app pos $ app neg) trunk_arg_Ts
2465 connective $ pos () $ neg ())
2470 betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
2471 aux ss Ts [] depth Neut t2)
2472 | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
2475 in aux [] [] [] 0 Pos end
2477 (* extended_context -> styp -> (int * term option) list *)
2478 fun static_args_in_term ({ersatz_table, ...} : extended_context) x t =
2480 (* term -> term list -> term list -> term list list *)
2481 fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
2482 | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
2483 | fun_calls t args =
2485 Const (x' as (s', T')) =>
2486 x = x' orelse (case AList.lookup (op =) ersatz_table s' of
2487 SOME s'' => x = (s'', T')
2489 | _ => false) ? cons args
2490 (* term list list -> term list list -> term list -> term list list *)
2491 fun call_sets [] [] vs = [vs]
2492 | call_sets [] uss vs = vs :: call_sets uss [] []
2493 | call_sets ([] :: _) _ _ = []
2494 | call_sets ((t :: ts) :: tss) uss vs =
2495 OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
2496 val sets = call_sets (fun_calls t [] []) [] []
2497 val indexed_sets = sets ~~ (index_seq 0 (length sets))
2499 fold_rev (fn (set, j) =>
2501 [Var _] => AList.lookup (op =) indexed_sets set = SOME j
2503 | [t as Const _] => cons (j, SOME t)
2504 | [t as Free _] => cons (j, SOME t)
2505 | _ => I) indexed_sets []
2507 (* extended_context -> styp -> term list -> (int * term option) list *)
2508 fun static_args_in_terms ext_ctxt x =
2509 map (static_args_in_term ext_ctxt x)
2510 #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
2512 (* term -> term list *)
2513 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
2514 | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
2515 | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
2517 | params_in_equation _ = []
2519 (* styp -> styp -> int list -> term list -> term list -> term -> term *)
2520 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
2522 val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
2524 val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
2525 val fixed_params = filter_indices fixed_js (params_in_equation t)
2526 (* term list -> term -> term *)
2527 fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
2528 | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
2531 list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
2533 let val j = find_index (equal t) fixed_params in
2534 list_comb (if j >= 0 then nth fixed_args j else t, args)
2538 (* typ list -> term -> bool *)
2539 fun is_eligible_arg Ts t =
2540 let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
2542 orelse (is_higher_order_type (fastype_of1 (Ts, t))
2543 andalso forall (not o is_higher_order_type) bad_Ts)
2546 (* (int * term option) list -> (int * term) list -> int list *)
2547 fun overlapping_indices [] _ = []
2548 | overlapping_indices _ [] = []
2549 | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
2550 if j1 < j2 then overlapping_indices ps1' ps2
2551 else if j1 > j2 then overlapping_indices ps1 ps2'
2552 else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
2554 val special_depth = 20
2556 (* extended_context -> int -> term -> term *)
2557 fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table,
2558 special_funs, ...}) depth t =
2559 if not specialize orelse depth > special_depth then
2563 val blacklist = if depth = 0 then []
2564 else case term_under_def t of Const x => [x] | _ => []
2565 (* term list -> typ list -> term -> term *)
2566 fun aux args Ts (Const (x as (s, T))) =
2567 ((if not (x mem blacklist) andalso not (null args)
2568 andalso not (String.isPrefix special_prefix s)
2569 andalso is_equational_fun ext_ctxt x then
2571 val eligible_args = filter (is_eligible_arg Ts o snd)
2572 (index_seq 0 (length args) ~~ args)
2573 val _ = not (null eligible_args) orelse raise SAME ()
2574 val old_axs = equational_fun_axioms ext_ctxt x
2575 |> map (destroy_existential_equalities thy)
2576 val static_params = static_args_in_terms ext_ctxt x old_axs
2577 val fixed_js = overlapping_indices static_params eligible_args
2578 val _ = not (null fixed_js) orelse raise SAME ()
2579 val fixed_args = filter_indices fixed_js args
2580 val vars = fold Term.add_vars fixed_args []
2581 |> sort (TermOrd.fast_indexname_ord o pairself fst)
2582 val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
2585 val live_args = filter_out_indices fixed_js args
2586 val extra_args = map Var vars @ map Bound bound_js @ live_args
2587 val extra_Ts = map snd vars @ filter_indices bound_js Ts
2588 val k = maxidx_of_term t + 1
2590 fun var_for_bound_no j =
2591 Var ((bound_var_prefix ^
2592 nat_subscript (find_index (equal j) bound_js + 1), k),
2594 val fixed_args_in_axiom =
2595 map (curry subst_bounds
2596 (map var_for_bound_no (index_seq 0 (length Ts))))
2599 case AList.lookup (op =) (!special_funs)
2600 (x, fixed_js, fixed_args_in_axiom) of
2601 SOME x' => list_comb (Const x', extra_args)
2604 val extra_args_in_axiom =
2605 map Var vars @ map var_for_bound_no bound_js
2607 (special_prefix_for (length (!special_funs) + 1) ^ s,
2608 extra_Ts @ filter_out_indices fixed_js (binder_types T)
2611 map (specialize_fun_axiom x x' fixed_js
2612 fixed_args_in_axiom extra_args_in_axiom) old_axs
2614 Unsynchronized.change special_funs
2615 (cons ((x, fixed_js, fixed_args_in_axiom), x'))
2616 val _ = add_simps simp_table s' new_axs
2617 in list_comb (Const x', extra_args) end
2621 handle SAME () => list_comb (Const x, args))
2622 | aux args Ts (Abs (s, T, t)) =
2623 list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
2624 | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
2625 | aux args _ t = list_comb (t, args)
2628 (* theory -> term -> int Termtab.tab -> int Termtab.tab *)
2629 fun add_to_uncurry_table thy t =
2631 (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
2632 fun aux (t1 $ t2) args table =
2633 let val table = aux t2 [] table in aux t1 (t2 :: args) table end
2634 | aux (Abs (_, _, t')) _ table = aux t' [] table
2635 | aux (t as Const (x as (s, _))) args table =
2636 if is_built_in_const false x orelse is_constr_like thy x orelse is_sel s
2637 orelse s = @{const_name Sigma} then
2640 Termtab.map_default (t, 65536) (curry Int.min (length args)) table
2641 | aux _ _ table = table
2644 (* int Termtab.tab term -> term *)
2645 fun uncurry_term table t =
2647 (* term -> term list -> term *)
2648 fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
2649 | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
2650 | aux (t as Const (s, T)) args =
2651 (case Termtab.lookup table t of
2655 val (arg_Ts, rest_T) = strip_n_binders n T
2657 if hd arg_Ts = @{typ bisim_iterator}
2658 orelse is_fp_iterator_type (hd arg_Ts) then
2660 else case find_index (not_equal bool_T) arg_Ts of
2663 val ((before_args, tuple_args), after_args) =
2664 args |> chop n |>> chop j
2665 val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
2666 T |> strip_n_binders n |>> chop j
2667 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
2672 betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
2673 before_arg_Ts ---> tuple_T --> rest_T),
2674 before_args @ [mk_flat_tuple tuple_T tuple_args] @
2679 | NONE => betapplys (t, args))
2680 | aux t args = betapplys (t, args)
2683 (* (term -> term) -> int -> term -> term *)
2684 fun coerce_bound_no f j t =
2686 t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
2687 | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
2688 | Bound j' => if j' = j then f t else t
2691 (* extended_context -> bool -> term -> term *)
2692 fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t =
2695 fun box_relational_operator_type (Type ("fun", Ts)) =
2696 Type ("fun", map box_relational_operator_type Ts)
2697 | box_relational_operator_type (Type ("*", Ts)) =
2698 Type ("*", map (box_type ext_ctxt InPair) Ts)
2699 | box_relational_operator_type T = T
2700 (* typ -> typ -> term -> term *)
2701 fun coerce_bound_0_in_term new_T old_T =
2702 old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
2703 (* typ list -> typ -> term -> term *)
2704 and coerce_term Ts new_T old_T t =
2705 if old_T = new_T then
2708 case (new_T, old_T) of
2709 (Type (new_s, new_Ts as [new_T1, new_T2]),
2710 Type ("fun", [old_T1, old_T2])) =>
2711 (case eta_expand Ts t 1 of
2714 t' |> coerce_bound_0_in_term new_T1 old_T1
2715 |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
2716 |> Envir.eta_contract
2718 ? construct_value thy (@{const_name FunBox},
2719 Type ("fun", new_Ts) --> new_T) o single
2720 | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
2721 \coerce_term", [t']))
2722 | (Type (new_s, new_Ts as [new_T1, new_T2]),
2723 Type (old_s, old_Ts as [old_T1, old_T2])) =>
2724 if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
2725 case constr_expand ext_ctxt old_T t of
2726 Const (@{const_name FunBox}, _) $ t1 =>
2727 if new_s = "fun" then
2728 coerce_term Ts new_T (Type ("fun", old_Ts)) t1
2731 (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
2732 [coerce_term Ts (Type ("fun", new_Ts))
2733 (Type ("fun", old_Ts)) t1]
2734 | Const _ $ t1 $ t2 =>
2736 (if new_s = "*" then @{const_name Pair}
2737 else @{const_name PairBox}, new_Ts ---> new_T)
2738 [coerce_term Ts new_T1 old_T1 t1,
2739 coerce_term Ts new_T2 old_T2 t2]
2740 | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
2741 \coerce_term", [t'])
2743 raise TYPE ("coerce_term", [new_T, old_T], [t])
2744 | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
2745 (* indexname * typ -> typ * term -> typ option list -> typ option list *)
2746 fun add_boxed_types_for_var (z as (_, T)) (T', t') =
2748 Var z' => z' = z ? insert (op =) T'
2749 | Const (@{const_name Pair}, _) $ t1 $ t2 =>
2751 Type (_, [T1, T2]) =>
2752 fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
2753 | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
2754 \add_boxed_types_for_var", [T'], []))
2755 | _ => exists_subterm (equal (Var z)) t' ? insert (op =) T
2756 (* typ list -> typ list -> term -> indexname * typ -> typ *)
2757 fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
2759 @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
2760 | Const (s0, _) $ t1 $ _ =>
2761 if s0 mem [@{const_name "=="}, @{const_name "op ="}] then
2763 val (t', args) = strip_comb t1
2764 val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
2766 case fold (add_boxed_types_for_var z)
2767 (fst (strip_n_binders (length args) T') ~~ args) [] of
2774 (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
2776 and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
2779 if polar = Neut orelse is_positive_existential polar quant_s then
2780 box_type ext_ctxt InFunLHS abs_T
2783 val body_T = body_type quant_T
2785 Const (quant_s, (abs_T' --> body_T) --> body_T)
2786 $ Abs (abs_s, abs_T',
2787 t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
2789 (* typ list -> typ list -> string -> typ -> term -> term -> term *)
2790 and do_equals new_Ts old_Ts s0 T0 t1 t2 =
2792 val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
2793 val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
2794 val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
2796 list_comb (Const (s0, [T, T] ---> body_type T0),
2797 map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
2799 (* string -> typ -> term *)
2800 and do_description_operator s T =
2801 let val T1 = box_type ext_ctxt InFunLHS (range_type T) in
2802 Const (s, (T1 --> bool_T) --> T1)
2804 (* typ list -> typ list -> polarity -> term -> term *)
2805 and do_term new_Ts old_Ts polar t =
2807 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
2808 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
2809 | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
2810 do_equals new_Ts old_Ts s0 T0 t1 t2
2811 | @{const "==>"} $ t1 $ t2 =>
2812 @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
2813 $ do_term new_Ts old_Ts polar t2
2814 | @{const Pure.conjunction} $ t1 $ t2 =>
2815 @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
2816 $ do_term new_Ts old_Ts polar t2
2817 | @{const Trueprop} $ t1 =>
2818 @{const Trueprop} $ do_term new_Ts old_Ts polar t1
2819 | @{const Not} $ t1 =>
2820 @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
2821 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
2822 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
2823 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
2824 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
2825 | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
2826 do_equals new_Ts old_Ts s0 T0 t1 t2
2827 | @{const "op &"} $ t1 $ t2 =>
2828 @{const "op &"} $ do_term new_Ts old_Ts polar t1
2829 $ do_term new_Ts old_Ts polar t2
2830 | @{const "op |"} $ t1 $ t2 =>
2831 @{const "op |"} $ do_term new_Ts old_Ts polar t1
2832 $ do_term new_Ts old_Ts polar t2
2833 | @{const "op -->"} $ t1 $ t2 =>
2834 @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
2835 $ do_term new_Ts old_Ts polar t2
2836 | Const (s as @{const_name The}, T) => do_description_operator s T
2837 | Const (s as @{const_name Eps}, T) => do_description_operator s T
2838 | Const (s as @{const_name Tha}, T) => do_description_operator s T
2839 | Const (x as (s, T)) =>
2840 Const (s, if s mem [@{const_name converse}, @{const_name trancl}] then
2841 box_relational_operator_type T
2842 else if is_built_in_const fast_descrs x
2843 orelse s = @{const_name Sigma} then
2845 else if is_constr_like thy x then
2846 box_type ext_ctxt InConstr T
2847 else if is_sel s orelse is_rep_fun thy x then
2848 box_type ext_ctxt InSel T
2850 box_type ext_ctxt InExpr T)
2851 | t1 $ Abs (s, T, t2') =>
2853 val t1 = do_term new_Ts old_Ts Neut t1
2854 val T1 = fastype_of1 (new_Ts, t1)
2855 val (s1, Ts1) = dest_Type T1
2856 val T' = hd (snd (dest_Type (hd Ts1)))
2857 val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
2858 val T2 = fastype_of1 (new_Ts, t2)
2859 val t2 = coerce_term new_Ts (hd Ts1) T2 t2
2861 betapply (if s1 = "fun" then
2864 select_nth_constr_arg thy
2865 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
2866 (Type ("fun", Ts1)), t2)
2870 val t1 = do_term new_Ts old_Ts Neut t1
2871 val T1 = fastype_of1 (new_Ts, t1)
2872 val (s1, Ts1) = dest_Type T1
2873 val t2 = do_term new_Ts old_Ts Neut t2
2874 val T2 = fastype_of1 (new_Ts, t2)
2875 val t2 = coerce_term new_Ts (hd Ts1) T2 t2
2877 betapply (if s1 = "fun" then
2880 select_nth_constr_arg thy
2881 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
2882 (Type ("fun", Ts1)), t2)
2884 | Free (s, T) => Free (s, box_type ext_ctxt InExpr T)
2885 | Var (z as (x, T)) =>
2886 Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
2887 else box_type ext_ctxt InExpr T)
2890 Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
2891 in do_term [] [] Pos orig_t end
2893 (* int -> term -> term *)
2894 fun eval_axiom_for_term j t =
2895 Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
2897 (* extended_context -> styp -> bool *)
2898 fun is_equational_fun_surely_complete ext_ctxt x =
2899 case raw_equational_fun_axioms ext_ctxt x of
2900 [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
2901 strip_comb t1 |> snd |> forall is_Var
2904 type special = int list * term list * styp
2906 (* styp -> special -> special -> term *)
2907 fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
2909 val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
2910 val Ts = binder_types T
2911 val max_j = fold (fold (curry Int.max)) [js1, js2] ~1
2912 val (eqs, (args1, args2)) =
2913 fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
2914 (js1 ~~ ts1, js2 ~~ ts2) of
2915 (SOME t1, SOME t2) => apfst (cons (t1, t2))
2916 | (SOME t1, NONE) => apsnd (apsnd (cons t1))
2917 | (NONE, SOME t2) => apsnd (apfst (cons t2))
2919 let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
2921 apsnd (pairself (cons v))
2922 end) (max_j downto 0) ([], ([], []))
2924 Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
2925 |> map Logic.mk_equals,
2926 Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
2927 list_comb (Const x2, bounds2 @ args2)))
2928 |> Refute.close_form
2931 (* extended_context -> styp list -> term list *)
2932 fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs =
2936 |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
2937 |> AList.group (op =)
2938 |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
2939 |> map (fn (x, zs) => (x, zs |> (x mem xs) ? cons ([], [], x)))
2940 (* special -> int *)
2941 fun generality (js, _, _) = ~(length js)
2942 (* special -> special -> bool *)
2943 fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
2944 x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
2945 (j2 ~~ t2, j1 ~~ t1)
2946 (* styp -> special list -> special list -> special list -> term list
2948 fun do_pass_1 _ [] [_] [_] = I
2949 | do_pass_1 x skipped _ [] = do_pass_2 x skipped
2950 | do_pass_1 x skipped all (z :: zs) =
2951 case filter (is_more_specific z) all
2952 |> sort (int_ord o pairself generality) of
2953 [] => do_pass_1 x (z :: skipped) all zs
2954 | (z' :: _) => cons (special_congruence_axiom x z z')
2955 #> do_pass_1 x skipped all zs
2956 (* styp -> special list -> term list -> term list *)
2957 and do_pass_2 _ [] = I
2958 | do_pass_2 x (z :: zs) =
2959 fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
2960 in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
2963 val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
2965 (* 'a Symtab.table -> 'a list *)
2966 fun all_table_entries table = Symtab.fold (append o snd) table []
2967 (* const_table -> string -> const_table *)
2968 fun extra_table table s = Symtab.make [(s, all_table_entries table)]
2970 (* extended_context -> term -> (term list * term list) * (bool * bool) *)
2972 (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
2973 def_table, nondef_table, user_nondefs, ...}) t =
2975 type accumulator = styp list * (term list * term list)
2976 (* (term list * term list -> term list)
2977 -> ((term list -> term list) -> term list * term list
2978 -> term list * term list)
2979 -> int -> term -> accumulator -> accumulator *)
2980 fun add_axiom get app depth t (accum as (xs, axs)) =
2982 val t = t |> unfold_defs_in_term ext_ctxt
2983 |> skolemize_term_and_more ext_ctxt ~1
2985 if is_trivial_equation t then
2988 let val t' = t |> specialize_consts_in_term ext_ctxt depth in
2989 if exists (member (op aconv) (get axs)) [t, t'] then accum
2990 else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
2993 (* int -> term -> accumulator -> accumulator *)
2994 and add_nondef_axiom depth = add_axiom snd apsnd depth
2995 and add_def_axiom depth t =
2996 (if head_of t = @{const "==>"} then add_nondef_axiom
2997 else add_axiom fst apfst) depth t
2998 (* int -> term -> accumulator -> accumulator *)
2999 and add_axioms_for_term depth t (accum as (xs, axs)) =
3001 t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
3002 | Const (x as (s, T)) =>
3003 (if x mem xs orelse is_built_in_const fast_descrs x then
3006 let val accum as (xs, _) = (x :: xs, axs) in
3007 if depth > axioms_max_depth then
3008 raise LIMIT ("Nitpick_HOL.axioms_for_term.add_axioms_for_term",
3009 "too many nested axioms (" ^ string_of_int depth ^
3011 else if Refute.is_const_of_class thy x then
3013 val class = Logic.class_of_const s
3014 val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
3016 val ax1 = try (Refute.specialize_type thy x) of_class
3017 val ax2 = Option.map (Refute.specialize_type thy x o snd)
3018 (Refute.get_classdef thy class)
3019 in fold (add_def_axiom depth) (map_filter I [ax1, ax2]) accum end
3020 else if is_constr thy x then
3022 else if is_equational_fun ext_ctxt x then
3023 fold (add_def_axiom depth) (equational_fun_axioms ext_ctxt x)
3025 else if is_abs_fun thy x then
3026 accum |> fold (add_nondef_axiom depth)
3027 (nondef_props_for_const thy false nondef_table x)
3028 |> is_funky_typedef thy (range_type T)
3029 ? fold (add_def_axiom depth)
3030 (nondef_props_for_const thy true
3031 (extra_table def_table s) x)
3032 else if is_rep_fun thy x then
3033 accum |> fold (add_nondef_axiom depth)
3034 (nondef_props_for_const thy false nondef_table x)
3035 |> is_funky_typedef thy (range_type T)
3036 ? fold (add_def_axiom depth)
3037 (nondef_props_for_const thy true
3038 (extra_table def_table s) x)
3039 |> add_axioms_for_term depth
3040 (Const (mate_of_rep_fun thy x))
3041 |> add_def_axiom depth (inverse_axiom_for_rep_fun thy x)
3043 accum |> user_axioms <> SOME false
3044 ? fold (add_nondef_axiom depth)
3045 (nondef_props_for_const thy false nondef_table x)
3047 |> add_axioms_for_type depth T
3048 | Free (_, T) => add_axioms_for_type depth T accum
3049 | Var (_, T) => add_axioms_for_type depth T accum
3051 | Abs (_, T, t) => accum |> add_axioms_for_term depth t
3052 |> add_axioms_for_type depth T
3053 (* int -> typ -> accumulator -> accumulator *)
3054 and add_axioms_for_type depth T =
3056 Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
3057 | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
3061 | TFree (_, S) => add_axioms_for_sort depth T S
3062 | TVar (_, S) => add_axioms_for_sort depth T S
3063 | Type (z as (_, Ts)) =>
3064 fold (add_axioms_for_type depth) Ts
3065 #> (if is_pure_typedef thy T then
3066 fold (add_def_axiom depth) (optimized_typedef_axioms thy z)
3067 else if max_bisim_depth >= 0 andalso is_codatatype thy T then
3068 fold (add_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T)
3071 (* int -> typ -> sort -> accumulator -> accumulator *)
3072 and add_axioms_for_sort depth T S =
3074 val supers = Sign.complete_sort thy S
3076 maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
3077 handle ERROR _ => [])) supers
3078 val monomorphic_class_axioms =
3079 map (fn t => case Term.add_tvars t [] of
3082 Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
3083 | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
3084 \add_axioms_for_sort", [t]))
3086 in fold (add_nondef_axiom depth) monomorphic_class_axioms end
3087 val (mono_user_nondefs, poly_user_nondefs) =
3088 List.partition (null o Term.hidden_polymorphism) user_nondefs
3089 val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
3091 val (xs, (defs, nondefs)) =
3092 ([], ([], [])) |> add_axioms_for_term 1 t
3093 |> fold_rev (add_def_axiom 1) eval_axioms
3094 |> user_axioms = SOME true
3095 ? fold (add_nondef_axiom 1) mono_user_nondefs
3096 val defs = defs @ special_congruence_axioms ext_ctxt xs
3098 ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
3099 null poly_user_nondefs))
3102 (* theory -> const_table -> styp -> int list *)
3103 fun const_format thy def_table (x as (s, T)) =
3104 if String.isPrefix unrolled_prefix s then
3105 const_format thy def_table (original_name s, range_type T)
3106 else if String.isPrefix skolem_prefix s then
3108 val k = unprefix skolem_prefix s
3109 |> strip_first_name_sep |> fst |> space_explode "@"
3110 |> hd |> Int.fromString |> the
3111 in [k, num_binder_types T - k] end
3112 else if original_name s <> s then
3113 [num_binder_types T]
3114 else case def_of_const thy def_table x of
3115 SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
3116 let val k = length (strip_abs_vars t') in
3117 [k, num_binder_types T - k]
3120 [num_binder_types T]
3121 | NONE => [num_binder_types T]
3122 (* int list -> int list -> int list *)
3123 fun intersect_formats _ [] = []
3124 | intersect_formats [] _ = []
3125 | intersect_formats ks1 ks2 =
3126 let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
3127 intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
3128 (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
3132 (* theory -> const_table -> (term option * int list) list -> term -> int list *)
3133 fun lookup_format thy def_table formats t =
3134 case AList.lookup (fn (SOME x, SOME y) =>
3135 (term_match thy) (x, y) | _ => false)
3137 SOME format => format
3138 | NONE => let val format = the (AList.lookup (op =) formats NONE) in
3140 Const x => intersect_formats format
3141 (const_format thy def_table x)
3145 (* int list -> int list -> typ -> typ *)
3146 fun format_type default_format format T =
3148 val T = unbox_type T
3149 val format = format |> filter (curry (op <) 0)
3151 if forall (equal 1) format then
3155 val (binder_Ts, body_T) = strip_type T
3158 |> map (format_type default_format default_format)
3159 |> rev |> chunk_list_unevenly (rev format)
3160 |> map (HOLogic.mk_tupleT o rev)
3161 in List.foldl (op -->) body_T batched end
3163 (* theory -> const_table -> (term option * int list) list -> term -> typ *)
3164 fun format_term_type thy def_table formats t =
3165 format_type (the (AList.lookup (op =) formats NONE))
3166 (lookup_format thy def_table formats t) (fastype_of t)
3168 (* int list -> int -> int list -> int list *)
3169 fun repair_special_format js m format =
3170 m - 1 downto 0 |> chunk_list_unevenly (rev format)
3171 |> map (rev o filter_out (member (op =) js))
3172 |> filter_out null |> map length |> rev
3174 (* extended_context -> string * string -> (term option * int list) list
3175 -> styp -> term * typ *)
3176 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
3177 : extended_context) (base_name, step_name) formats =
3179 val default_format = the (AList.lookup (op =) formats NONE)
3180 (* styp -> term * typ *)
3181 fun do_const (x as (s, T)) =
3182 (if String.isPrefix special_prefix s then
3185 val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
3186 val (x' as (_, T'), js, ts) =
3187 AList.find (op =) (!special_funs) (s, unbox_type T) |> the_single
3188 val max_j = List.last js
3189 val Ts = List.take (binder_types T', max_j + 1)
3190 val missing_js = filter_out (member (op =) js) (0 upto max_j)
3191 val missing_Ts = filter_indices missing_js Ts
3192 (* int -> indexname *)
3193 fun nth_missing_var n =
3194 ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
3195 val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
3196 val vars = special_bounds ts @ missing_vars
3197 val ts' = map2 (fn T => fn j =>
3198 case AList.lookup (op =) (js ~~ ts) j of
3201 Var (nth missing_vars
3202 (find_index (equal j) missing_js)))
3204 val t = do_const x' |> fst
3206 case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
3207 | _ => false) formats (SOME t) of
3209 repair_special_format js (num_binder_types T') format
3211 const_format thy def_table x'
3212 |> repair_special_format js (num_binder_types T')
3213 |> intersect_formats default_format
3215 (list_comb (t, ts') |> fold_rev abs_var vars,
3216 format_type default_format format T)
3218 else if String.isPrefix uncurry_prefix s then
3220 val (ss, s') = unprefix uncurry_prefix s
3221 |> strip_first_name_sep |>> space_explode "@"
3223 if String.isPrefix step_prefix s' then
3227 val k = the (Int.fromString (hd ss))
3228 val j = the (Int.fromString (List.last ss))
3229 val (before_Ts, (tuple_T, rest_T)) =
3230 strip_n_binders j T ||> (strip_n_binders 1 #>> hd)
3231 val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T
3232 in do_const (s', T') end
3234 else if String.isPrefix unrolled_prefix s then
3235 let val t = Const (original_name s, range_type T) in
3236 (lambda (Free (iter_var_prefix, nat_T)) t,
3237 format_type default_format
3238 (lookup_format thy def_table formats t) T)
3240 else if String.isPrefix base_prefix s then
3241 (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
3242 format_type default_format default_format T)
3243 else if String.isPrefix step_prefix s then
3244 (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
3245 format_type default_format default_format T)
3246 else if String.isPrefix skolem_prefix s then
3248 val ss = the (AList.lookup (op =) (!skolems) s)
3249 val (Ts, Ts') = chop (length ss) (binder_types T)
3250 val frees = map Free (ss ~~ Ts)
3251 val s' = original_name s
3253 (fold lambda frees (Const (s', Ts' ---> T)),
3254 format_type default_format
3255 (lookup_format thy def_table formats (Const x)) T)
3257 else if String.isPrefix eval_prefix s then
3259 val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
3260 in (t, format_term_type thy def_table formats t) end
3261 else if s = @{const_name undefined_fast_The} then
3262 (Const (nitpick_prefix ^ "The fallback", T),
3263 format_type default_format
3264 (lookup_format thy def_table formats
3265 (Const (@{const_name The}, (T --> bool_T) --> T))) T)
3266 else if s = @{const_name undefined_fast_Eps} then
3267 (Const (nitpick_prefix ^ "Eps fallback", T),
3268 format_type default_format
3269 (lookup_format thy def_table formats
3270 (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
3272 let val t = Const (original_name s, T) in
3273 (t, format_term_type thy def_table formats t)
3275 |>> map_types (typ_subst [(@{typ bisim_iterator}, nat_T)] o unbox_type)
3276 |>> shorten_const_names_in_term |>> shorten_abs_vars
3279 (* styp -> string *)
3280 fun assign_operator_for_const (s, T) =
3281 if String.isPrefix ubfp_prefix s then
3282 if is_fun_type T then "\<subseteq>" else "\<le>"
3283 else if String.isPrefix lbfp_prefix s then
3284 if is_fun_type T then "\<supseteq>" else "\<ge>"
3285 else if original_name s <> s then
3286 assign_operator_for_const (after_name_sep s, T)
3290 (* extended_context -> term
3291 -> ((term list * term list) * (bool * bool)) * term *)
3292 fun preprocess_term (ext_ctxt as {thy, destroy_constrs, boxes, skolemize,
3295 val skolem_depth = if skolemize then 4 else ~1
3296 val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
3297 core_t) = t |> unfold_defs_in_term ext_ctxt
3298 |> Refute.close_form
3299 |> skolemize_term_and_more ext_ctxt skolem_depth
3300 |> specialize_consts_in_term ext_ctxt 0
3301 |> `(axioms_for_term ext_ctxt)
3302 val maybe_box = exists (not_equal (SOME false) o snd) boxes
3304 Termtab.empty |> uncurry
3305 ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
3306 (* bool -> bool -> term -> term *)
3307 fun do_rest def core =
3308 uncurry ? uncurry_term table
3309 #> maybe_box ? box_fun_and_pair_in_term ext_ctxt def
3310 #> destroy_constrs ? (pull_out_universal_constrs thy def
3311 #> pull_out_existential_constrs thy
3312 #> destroy_pulled_out_constrs ext_ctxt def)
3314 #> destroy_universal_equalities
3315 #> destroy_existential_equalities thy
3316 #> simplify_constrs_and_sels thy
3317 #> distribute_quantifiers
3318 #> push_quantifiers_inward thy
3319 #> not core ? Refute.close_form
3322 (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
3323 (got_all_mono_user_axioms, no_poly_user_axioms)),
3324 do_rest false true core_t)