1 (* Title: HOL/Tools/Nitpick/nitpick_hol.ML
2 Author: Jasmin Blanchette, TU Muenchen
3 Copyright 2008, 2009, 2010
5 Auxiliary HOL-related functions used by Nitpick.
8 signature NITPICK_HOL =
10 type styp = Nitpick_Util.styp
11 type const_table = term list Symtab.table
12 type special_fun = (styp * int list * term list) * styp
13 type unrolled = styp * styp
14 type wf_cache = (styp * (bool * bool)) list
20 boxes: (typ option * bool option) list,
21 stds: (typ option * bool) list,
22 wfs: (styp option * bool option) list,
23 user_axioms: bool option,
25 binary_ints: bool option,
26 destroy_constrs: bool,
29 star_linear_preds: bool,
32 tac_timeout: Time.time option,
34 case_names: (string * int) list,
35 def_table: const_table,
36 nondef_table: const_table,
37 user_nondefs: term list,
38 simp_table: const_table Unsynchronized.ref,
39 psimp_table: const_table,
40 intro_table: const_table,
41 ground_thm_table: term list Inttab.table,
42 ersatz_table: (string * string) list,
43 skolems: (string * string list) list Unsynchronized.ref,
44 special_funs: special_fun list Unsynchronized.ref,
45 unrolled_preds: unrolled list Unsynchronized.ref,
46 wf_cache: wf_cache Unsynchronized.ref,
47 constr_cache: (typ * styp list) list Unsynchronized.ref}
49 datatype fixpoint_kind = Lfp | Gfp | NoFp
51 InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
54 val numeral_prefix : string
55 val ubfp_prefix : string
56 val lbfp_prefix : string
57 val skolem_prefix : string
58 val special_prefix : string
59 val uncurry_prefix : string
60 val eval_prefix : string
61 val original_name : string -> string
62 val s_conj : term * term -> term
63 val s_disj : term * term -> term
64 val strip_any_connective : term -> term list * term
65 val conjuncts_of : term -> term list
66 val disjuncts_of : term -> term list
67 val unarize_and_unbox_type : typ -> typ
68 val unarize_unbox_and_uniterize_type : typ -> typ
69 val string_for_type : Proof.context -> typ -> string
70 val prefix_name : string -> string -> string
71 val shortest_name : string -> string
72 val short_name : string -> string
73 val shorten_names_in_term : term -> term
74 val type_match : theory -> typ * typ -> bool
75 val const_match : theory -> styp * styp -> bool
76 val term_match : theory -> term * term -> bool
77 val is_TFree : typ -> bool
78 val is_higher_order_type : typ -> bool
79 val is_fun_type : typ -> bool
80 val is_set_type : typ -> bool
81 val is_pair_type : typ -> bool
82 val is_lfp_iterator_type : typ -> bool
83 val is_gfp_iterator_type : typ -> bool
84 val is_fp_iterator_type : typ -> bool
85 val is_iterator_type : typ -> bool
86 val is_boolean_type : typ -> bool
87 val is_integer_type : typ -> bool
88 val is_bit_type : typ -> bool
89 val is_word_type : typ -> bool
90 val is_integer_like_type : typ -> bool
91 val is_record_type : typ -> bool
92 val is_number_type : theory -> typ -> bool
93 val const_for_iterator_type : typ -> styp
94 val strip_n_binders : int -> typ -> typ list * typ
95 val nth_range_type : int -> typ -> typ
96 val num_factors_in_type : typ -> int
97 val num_binder_types : typ -> int
98 val curried_binder_types : typ -> typ list
99 val mk_flat_tuple : typ -> term list -> term
100 val dest_n_tuple : int -> term -> term list
101 val is_real_datatype : theory -> string -> bool
102 val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
103 val is_quot_type : theory -> typ -> bool
104 val is_codatatype : theory -> typ -> bool
105 val is_pure_typedef : theory -> typ -> bool
106 val is_univ_typedef : theory -> typ -> bool
107 val is_datatype : theory -> (typ option * bool) list -> typ -> bool
108 val is_record_constr : styp -> bool
109 val is_record_get : theory -> styp -> bool
110 val is_record_update : theory -> styp -> bool
111 val is_abs_fun : theory -> styp -> bool
112 val is_rep_fun : theory -> styp -> bool
113 val is_quot_abs_fun : Proof.context -> styp -> bool
114 val is_quot_rep_fun : Proof.context -> styp -> bool
115 val mate_of_rep_fun : theory -> styp -> styp
116 val is_constr_like : theory -> styp -> bool
117 val is_stale_constr : theory -> styp -> bool
118 val is_constr : theory -> (typ option * bool) list -> styp -> bool
119 val is_sel : string -> bool
120 val is_sel_like_and_no_discr : string -> bool
121 val box_type : hol_context -> boxability -> typ -> typ
122 val binarize_nat_and_int_in_type : typ -> typ
123 val binarize_nat_and_int_in_term : term -> term
124 val discr_for_constr : styp -> styp
125 val num_sels_for_constr_type : typ -> int
126 val nth_sel_name_for_constr_name : string -> int -> string
127 val nth_sel_for_constr : styp -> int -> styp
128 val binarized_and_boxed_nth_sel_for_constr :
129 hol_context -> bool -> styp -> int -> styp
130 val sel_no_from_name : string -> int
131 val close_form : term -> term
132 val eta_expand : typ list -> term -> int -> term
133 val extensionalize : term -> term
134 val distinctness_formula : typ -> term list -> term
135 val register_frac_type : string -> (string * string) list -> theory -> theory
136 val unregister_frac_type : string -> theory -> theory
137 val register_codatatype : typ -> string -> styp list -> theory -> theory
138 val unregister_codatatype : typ -> theory -> theory
139 val datatype_constrs : hol_context -> typ -> styp list
140 val binarized_and_boxed_datatype_constrs :
141 hol_context -> bool -> typ -> styp list
142 val num_datatype_constrs : hol_context -> typ -> int
143 val constr_name_for_sel_like : string -> string
144 val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
145 val discriminate_value : hol_context -> styp -> term -> term
146 val select_nth_constr_arg :
147 theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
148 val construct_value :
149 theory -> (typ option * bool) list -> styp -> term list -> term
150 val card_of_type : (typ * int) list -> typ -> int
151 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
152 val bounded_exact_card_of_type :
153 hol_context -> int -> int -> (typ * int) list -> typ -> int
154 val is_finite_type : hol_context -> typ -> bool
155 val special_bounds : term list -> (indexname * typ) list
156 val is_funky_typedef : theory -> typ -> bool
157 val all_axioms_of : theory -> term list * term list * term list
158 val arity_of_built_in_const :
159 theory -> (typ option * bool) list -> bool -> styp -> int option
160 val is_built_in_const :
161 theory -> (typ option * bool) list -> bool -> styp -> bool
162 val term_under_def : term -> term
163 val case_const_names :
164 theory -> (typ option * bool) list -> (string * int) list
165 val const_def_table : Proof.context -> term list -> const_table
166 val const_nondef_table : term list -> const_table
167 val const_simp_table : Proof.context -> const_table
168 val const_psimp_table : Proof.context -> const_table
169 val inductive_intro_table : Proof.context -> const_table -> const_table
170 val ground_theorem_table : theory -> term list Inttab.table
171 val ersatz_table : theory -> (string * string) list
172 val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
173 val inverse_axioms_for_rep_fun : theory -> styp -> term list
174 val optimized_typedef_axioms : theory -> string * typ list -> term list
175 val optimized_quot_type_axioms :
176 theory -> (typ option * bool) list -> string * typ list -> term list
177 val def_of_const : theory -> const_table -> styp -> term option
178 val fixpoint_kind_of_const :
179 theory -> const_table -> string * typ -> fixpoint_kind
180 val is_inductive_pred : hol_context -> styp -> bool
181 val is_equational_fun : hol_context -> styp -> bool
182 val is_constr_pattern_lhs : theory -> term -> bool
183 val is_constr_pattern_formula : theory -> term -> bool
184 val unfold_defs_in_term : hol_context -> term -> term
185 val codatatype_bisim_axioms : hol_context -> typ -> term list
186 val is_well_founded_inductive_pred : hol_context -> styp -> bool
187 val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
188 val equational_fun_axioms : hol_context -> styp -> term list
189 val is_equational_fun_surely_complete : hol_context -> styp -> bool
190 val merge_type_vars_in_terms : term list -> term list
191 val ground_types_in_type : hol_context -> bool -> typ -> typ list
192 val ground_types_in_terms : hol_context -> bool -> term list -> typ list
193 val format_type : int list -> int list -> typ -> typ
194 val format_term_type :
195 theory -> const_table -> (term option * int list) list -> term -> typ
196 val user_friendly_const :
197 hol_context -> string * string -> (term option * int list) list
198 -> styp -> term * typ
199 val assign_operator_for_const : styp -> string
202 structure Nitpick_HOL : NITPICK_HOL =
207 type const_table = term list Symtab.table
208 type special_fun = (styp * int list * term list) * styp
209 type unrolled = styp * styp
210 type wf_cache = (styp * (bool * bool)) list
215 max_bisim_depth: int,
216 boxes: (typ option * bool option) list,
217 stds: (typ option * bool) list,
218 wfs: (styp option * bool option) list,
219 user_axioms: bool option,
221 binary_ints: bool option,
222 destroy_constrs: bool,
225 star_linear_preds: bool,
228 tac_timeout: Time.time option,
230 case_names: (string * int) list,
231 def_table: const_table,
232 nondef_table: const_table,
233 user_nondefs: term list,
234 simp_table: const_table Unsynchronized.ref,
235 psimp_table: const_table,
236 intro_table: const_table,
237 ground_thm_table: term list Inttab.table,
238 ersatz_table: (string * string) list,
239 skolems: (string * string list) list Unsynchronized.ref,
240 special_funs: special_fun list Unsynchronized.ref,
241 unrolled_preds: unrolled list Unsynchronized.ref,
242 wf_cache: wf_cache Unsynchronized.ref,
243 constr_cache: (typ * styp list) list Unsynchronized.ref}
245 datatype fixpoint_kind = Lfp | Gfp | NoFp
246 datatype boxability =
247 InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
249 structure Data = Theory_Data(
250 type T = {frac_types: (string * (string * string) list) list,
251 codatatypes: (string * (string * styp list)) list}
252 val empty = {frac_types = [], codatatypes = []}
254 fun merge ({frac_types = fs1, codatatypes = cs1},
255 {frac_types = fs2, codatatypes = cs2}) : T =
256 {frac_types = AList.merge (op =) (K true) (fs1, fs2),
257 codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
260 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
261 val sel_prefix = nitpick_prefix ^ "sel"
262 val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
263 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
264 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
265 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
266 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
267 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
268 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
269 val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
270 val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
271 val skolem_prefix = nitpick_prefix ^ "sk"
272 val special_prefix = nitpick_prefix ^ "sp"
273 val uncurry_prefix = nitpick_prefix ^ "unc"
274 val eval_prefix = nitpick_prefix ^ "eval"
275 val iter_var_prefix = "i"
276 val arg_var_prefix = "x"
279 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
281 (* string -> string * string *)
282 val strip_first_name_sep =
283 Substring.full #> Substring.position name_sep ##> Substring.triml 1
284 #> pairself Substring.string
285 (* string -> string *)
286 fun original_name s =
287 if String.isPrefix nitpick_prefix s then
288 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
291 val after_name_sep = snd o strip_first_name_sep
293 (* term * term -> term *)
294 fun s_conj (t1, @{const True}) = t1
295 | s_conj (@{const True}, t2) = t2
297 if t1 = @{const False} orelse t2 = @{const False} then @{const False}
298 else HOLogic.mk_conj (t1, t2)
299 fun s_disj (t1, @{const False}) = t1
300 | s_disj (@{const False}, t2) = t2
302 if t1 = @{const True} orelse t2 = @{const True} then @{const True}
303 else HOLogic.mk_disj (t1, t2)
305 (* term -> term -> term list *)
306 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
307 if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
308 | strip_connective _ t = [t]
309 (* term -> term list * term *)
310 fun strip_any_connective (t as (t0 $ _ $ _)) =
311 if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
312 (strip_connective t0 t, t0)
315 | strip_any_connective t = ([t], @{const Not})
316 (* term -> term list *)
317 val conjuncts_of = strip_connective @{const "op &"}
318 val disjuncts_of = strip_connective @{const "op |"}
320 (* When you add constants to these lists, make sure to handle them in
321 "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
323 val built_in_consts =
324 [(@{const_name all}, 1),
325 (@{const_name "=="}, 2),
326 (@{const_name "==>"}, 2),
327 (@{const_name Pure.conjunction}, 2),
328 (@{const_name Trueprop}, 1),
329 (@{const_name Not}, 1),
330 (@{const_name False}, 0),
331 (@{const_name True}, 0),
332 (@{const_name All}, 1),
333 (@{const_name Ex}, 1),
334 (@{const_name "op ="}, 2),
335 (@{const_name "op &"}, 2),
336 (@{const_name "op |"}, 2),
337 (@{const_name "op -->"}, 2),
338 (@{const_name If}, 3),
339 (@{const_name Let}, 2),
340 (@{const_name Unity}, 0),
341 (@{const_name Pair}, 2),
342 (@{const_name fst}, 1),
343 (@{const_name snd}, 1),
344 (@{const_name Id}, 0),
345 (@{const_name insert}, 2),
346 (@{const_name converse}, 1),
347 (@{const_name trancl}, 1),
348 (@{const_name rel_comp}, 2),
349 (@{const_name image}, 2),
350 (@{const_name finite}, 1),
351 (@{const_name unknown}, 0),
352 (@{const_name is_unknown}, 1),
353 (@{const_name Tha}, 1),
354 (@{const_name Frac}, 0),
355 (@{const_name norm_frac}, 0)]
356 val built_in_nat_consts =
357 [(@{const_name Suc}, 0),
358 (@{const_name nat}, 0),
359 (@{const_name nat_gcd}, 0),
360 (@{const_name nat_lcm}, 0)]
361 val built_in_descr_consts =
362 [(@{const_name The}, 1),
363 (@{const_name Eps}, 1)]
364 val built_in_typed_consts =
365 [((@{const_name zero_class.zero}, int_T), 0),
366 ((@{const_name one_class.one}, int_T), 0),
367 ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
368 ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
369 ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
370 ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
371 ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
372 ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
373 ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
374 val built_in_typed_nat_consts =
375 [((@{const_name zero_class.zero}, nat_T), 0),
376 ((@{const_name one_class.one}, nat_T), 0),
377 ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
378 ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
379 ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
380 ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
381 ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
382 ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
383 ((@{const_name of_nat}, nat_T --> int_T), 0)]
384 val built_in_set_consts =
385 [(@{const_name semilattice_inf_class.inf}, 2),
386 (@{const_name semilattice_sup_class.sup}, 2),
387 (@{const_name minus_class.minus}, 2),
388 (@{const_name ord_class.less_eq}, 2)]
391 fun unarize_type @{typ "unsigned_bit word"} = nat_T
392 | unarize_type @{typ "signed_bit word"} = int_T
393 | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
395 fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
396 unarize_and_unbox_type (Type ("fun", Ts))
397 | unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
398 Type ("*", map unarize_and_unbox_type Ts)
399 | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
400 | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
401 | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
402 Type (s, map unarize_and_unbox_type Ts)
403 | unarize_and_unbox_type T = T
404 fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
405 | uniterize_type @{typ bisim_iterator} = nat_T
406 | uniterize_type T = T
407 val unarize_unbox_and_uniterize_type = uniterize_type o unarize_and_unbox_type
409 (* Proof.context -> typ -> string *)
410 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
412 (* string -> string -> string *)
413 val prefix_name = Long_Name.qualify o Long_Name.base_name
414 (* string -> string *)
415 fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
416 (* string -> term -> term *)
417 val prefix_abs_vars = Term.map_abs_vars o prefix_name
418 (* string -> string *)
420 case space_explode name_sep s of
421 [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
422 | ss => map shortest_name ss |> space_implode "_"
424 fun shorten_names_in_type (Type (s, Ts)) =
425 Type (short_name s, map shorten_names_in_type Ts)
426 | shorten_names_in_type T = T
428 val shorten_names_in_term =
429 map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
430 #> map_types shorten_names_in_type
432 (* theory -> typ * typ -> bool *)
433 fun type_match thy (T1, T2) =
434 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
435 handle Type.TYPE_MATCH => false
436 (* theory -> styp * styp -> bool *)
437 fun const_match thy ((s1, T1), (s2, T2)) =
438 s1 = s2 andalso type_match thy (T1, T2)
439 (* theory -> term * term -> bool *)
440 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
441 | term_match thy (Free (s1, T1), Free (s2, T2)) =
442 const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
443 | term_match _ (t1, t2) = t1 aconv t2
446 fun is_TFree (TFree _) = true
448 fun is_higher_order_type (Type ("fun", _)) = true
449 | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
450 | is_higher_order_type _ = false
451 fun is_fun_type (Type ("fun", _)) = true
452 | is_fun_type _ = false
453 fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
454 | is_set_type _ = false
455 fun is_pair_type (Type ("*", _)) = true
456 | is_pair_type _ = false
457 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
458 | is_lfp_iterator_type _ = false
459 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
460 | is_gfp_iterator_type _ = false
461 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
462 fun is_iterator_type T =
463 (T = @{typ bisim_iterator} orelse is_fp_iterator_type T)
464 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
465 fun is_integer_type T = (T = nat_T orelse T = int_T)
466 fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
467 fun is_word_type (Type (@{type_name word}, _)) = true
468 | is_word_type _ = false
469 val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
470 val is_record_type = not o null o Record.dest_recTs
471 (* theory -> typ -> bool *)
472 fun is_frac_type thy (Type (s, [])) =
473 not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
474 | is_frac_type _ _ = false
475 fun is_number_type thy = is_integer_like_type orf is_frac_type thy
477 (* bool -> styp -> typ *)
478 fun iterator_type_for_const gfp (s, T) =
479 Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
482 fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
483 | const_for_iterator_type T =
484 raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
486 (* int -> typ -> typ list * typ *)
487 fun strip_n_binders 0 T = ([], T)
488 | strip_n_binders n (Type ("fun", [T1, T2])) =
489 strip_n_binders (n - 1) T2 |>> cons T1
490 | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
491 strip_n_binders n (Type ("fun", Ts))
492 | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
494 val nth_range_type = snd oo strip_n_binders
497 fun num_factors_in_type (Type ("*", [T1, T2])) =
498 fold (Integer.add o num_factors_in_type) [T1, T2] 0
499 | num_factors_in_type _ = 1
500 fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
501 | num_binder_types _ = 0
502 (* typ -> typ list *)
503 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
504 fun maybe_curried_binder_types T =
505 (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
507 (* typ -> term list -> term *)
508 fun mk_flat_tuple _ [t] = t
509 | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
510 HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
511 | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
512 (* int -> term -> term list *)
513 fun dest_n_tuple 1 t = [t]
514 | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
516 (* int -> typ -> typ list *)
517 fun dest_n_tuple_type 1 T = [T]
518 | dest_n_tuple_type n (Type (_, [T1, T2])) =
519 T1 :: dest_n_tuple_type (n - 1) T2
520 | dest_n_tuple_type _ T =
521 raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
524 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
525 set_def: thm option, prop_of_Rep: thm, set_name: string,
526 Abs_inverse: thm option, Rep_inverse: thm option}
528 (* theory -> string -> typedef_info *)
529 fun typedef_info thy s =
530 if is_frac_type thy (Type (s, [])) then
531 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
532 Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
533 set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
535 set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
536 else case Typedef.get_info thy s of
537 SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
539 SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
540 Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
541 set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
542 Rep_inverse = SOME Rep_inverse}
545 (* theory -> string -> bool *)
546 val is_typedef = is_some oo typedef_info
547 val is_real_datatype = is_some oo Datatype.get_info
548 (* theory -> (typ option * bool) list -> typ -> bool *)
549 fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
551 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
552 e.g., by adding a field to "Datatype_Aux.info". *)
553 (* theory -> (typ option * bool) list -> string -> bool *)
554 fun is_basic_datatype thy stds s =
555 member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
556 @{type_name int}, "Code_Numeral.code_numeral"] s orelse
557 (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
559 (* theory -> typ -> typ -> typ -> typ *)
560 fun instantiate_type thy T1 T1' T2 =
561 Same.commit (Envir.subst_type_same
562 (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
564 handle Type.TYPE_MATCH =>
565 raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
567 (* theory -> typ -> typ -> styp *)
568 fun repair_constr_type thy body_T' T =
569 instantiate_type thy (body_type T) body_T' T
571 (* string -> (string * string) list -> theory -> theory *)
572 fun register_frac_type frac_s ersaetze thy =
574 val {frac_types, codatatypes} = Data.get thy
575 val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
576 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
577 (* string -> theory -> theory *)
578 fun unregister_frac_type frac_s = register_frac_type frac_s []
580 (* typ -> string -> styp list -> theory -> theory *)
581 fun register_codatatype co_T case_name constr_xs thy =
583 val {frac_types, codatatypes} = Data.get thy
584 val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
585 val (co_s, co_Ts) = dest_Type co_T
587 if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
588 co_s <> "fun" andalso
589 not (is_basic_datatype thy [(NONE, true)] co_s) then
592 raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
593 val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
595 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
596 (* typ -> theory -> theory *)
597 fun unregister_codatatype co_T = register_codatatype co_T "" []
599 (* theory -> typ -> bool *)
600 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
601 | is_quot_type _ (Type ("FSet.fset", _)) = true
602 | is_quot_type _ _ = false
603 fun is_codatatype thy (Type (s, _)) =
604 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
605 |> Option.map snd |> these))
606 | is_codatatype _ _ = false
607 fun is_pure_typedef thy (T as Type (s, _)) =
608 is_typedef thy s andalso
609 not (is_real_datatype thy s orelse is_quot_type thy T orelse
610 is_codatatype thy T orelse is_record_type T orelse
611 is_integer_like_type T)
612 | is_pure_typedef _ _ = false
613 fun is_univ_typedef thy (Type (s, _)) =
614 (case typedef_info thy s of
615 SOME {set_def, prop_of_Rep, ...} =>
618 try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
620 try (fst o dest_Const o snd o HOLogic.dest_mem
621 o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
623 | is_univ_typedef _ _ = false
624 (* theory -> (typ option * bool) list -> typ -> bool *)
625 fun is_datatype thy stds (T as Type (s, _)) =
626 (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
627 is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
628 | is_datatype _ _ _ = false
630 (* theory -> typ -> (string * typ) list * (string * typ) *)
631 fun all_record_fields thy T =
632 let val (recs, more) = Record.get_extT_fields thy T in
633 recs @ more :: all_record_fields thy (snd more)
637 fun is_record_constr (s, T) =
638 String.isSuffix Record.extN s andalso
639 let val dataT = body_type T in
640 is_record_type dataT andalso
641 s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
643 (* theory -> typ -> int *)
644 val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
645 (* theory -> string -> typ -> int *)
646 fun no_of_record_field thy s T1 =
647 find_index (curry (op =) s o fst)
648 (Record.get_extT_fields thy T1 ||> single |> op @)
649 (* theory -> styp -> bool *)
650 fun is_record_get thy (s, Type ("fun", [T1, _])) =
651 exists (curry (op =) s o fst) (all_record_fields thy T1)
652 | is_record_get _ _ = false
653 fun is_record_update thy (s, T) =
654 String.isSuffix Record.updateN s andalso
655 exists (curry (op =) (unsuffix Record.updateN s) o fst)
656 (all_record_fields thy (body_type T))
657 handle TYPE _ => false
658 fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
659 (case typedef_info thy s' of
660 SOME {Abs_name, ...} => s = Abs_name
662 | is_abs_fun _ _ = false
663 fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
664 (case typedef_info thy s' of
665 SOME {Rep_name, ...} => s = Rep_name
667 | is_rep_fun _ _ = false
668 (* Proof.context -> styp -> bool *)
669 fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true
670 | is_quot_abs_fun _ ("FSet.abs_fset", _) = true
671 | is_quot_abs_fun _ _ = false
672 fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true
673 | is_quot_rep_fun _ ("FSet.rep_fset", _) = true
674 | is_quot_rep_fun _ _ = false
676 (* theory -> styp -> styp *)
677 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
678 (case typedef_info thy s' of
679 SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
680 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
681 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
682 (* theory -> typ -> typ *)
683 fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"}
684 | rep_type_for_quot_type _ (Type ("FSet.fset", [T])) =
685 Type (@{type_name list}, [T])
686 | rep_type_for_quot_type _ T =
687 raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
688 (* theory -> typ -> term *)
689 fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) =
690 Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"})
691 | equiv_relation_for_quot_type _ (Type ("FSet.fset", [T])) =
692 Const ("FSet.list_eq",
693 Type (@{type_name list}, [T]) --> Type (@{type_name list}, [T])
695 | equiv_relation_for_quot_type _ T =
696 raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
698 (* theory -> styp -> bool *)
699 fun is_coconstr thy (s, T) =
701 val {codatatypes, ...} = Data.get thy
702 val co_T = body_type T
703 val co_s = dest_Type co_T |> fst
705 exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
706 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
708 handle TYPE ("dest_Type", _, _) => false
709 fun is_constr_like thy (s, T) =
710 member (op =) [@{const_name FunBox}, @{const_name PairBox},
711 @{const_name Quot}, @{const_name Zero_Rep},
712 @{const_name Suc_Rep}] s orelse
713 let val (x as (_, T)) = (s, unarize_and_unbox_type T) in
714 Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
715 (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
718 fun is_stale_constr thy (x as (_, T)) =
719 is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
720 not (is_coconstr thy x)
721 (* theory -> (typ option * bool) list -> styp -> bool *)
722 fun is_constr thy stds (x as (_, T)) =
723 is_constr_like thy x andalso
724 not (is_basic_datatype thy stds
725 (fst (dest_Type (unarize_type (body_type T))))) andalso
726 not (is_stale_constr thy x)
728 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
729 val is_sel_like_and_no_discr =
730 String.isPrefix sel_prefix
731 orf (member (op =) [@{const_name fst}, @{const_name snd}])
733 (* boxability -> boxability *)
734 fun in_fun_lhs_for InConstr = InSel
735 | in_fun_lhs_for _ = InFunLHS
736 fun in_fun_rhs_for InConstr = InConstr
737 | in_fun_rhs_for InSel = InSel
738 | in_fun_rhs_for InFunRHS1 = InFunRHS2
739 | in_fun_rhs_for _ = InFunRHS1
741 (* hol_context -> boxability -> typ -> bool *)
742 fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
745 (boxy = InPair orelse boxy = InFunLHS) andalso
746 not (is_boolean_type (body_type T))
748 boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
749 ((boxy = InExpr orelse boxy = InFunLHS) andalso
750 exists (is_boxing_worth_it hol_ctxt InPair)
751 (map (box_type hol_ctxt InPair) Ts))
753 (* hol_context -> boxability -> string * typ list -> string *)
754 and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z =
755 case triple_lookup (type_match thy) boxes (Type z) of
756 SOME (SOME box_me) => box_me
757 | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
758 (* hol_context -> boxability -> typ -> typ *)
759 and box_type hol_ctxt boxy T =
761 Type (z as ("fun", [T1, T2])) =>
762 if boxy <> InConstr andalso boxy <> InSel andalso
763 should_box_type hol_ctxt boxy z then
764 Type (@{type_name fun_box},
765 [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
767 box_type hol_ctxt (in_fun_lhs_for boxy) T1
768 --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
769 | Type (z as ("*", Ts)) =>
770 if boxy <> InConstr andalso boxy <> InSel
771 andalso should_box_type hol_ctxt boxy z then
772 Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
774 Type ("*", map (box_type hol_ctxt
775 (if boxy = InConstr orelse boxy = InSel then boxy
780 fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
781 | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
782 | binarize_nat_and_int_in_type (Type (s, Ts)) =
783 Type (s, map binarize_nat_and_int_in_type Ts)
784 | binarize_nat_and_int_in_type T = T
786 val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
789 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
792 fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
793 (* string -> int -> string *)
794 fun nth_sel_name_for_constr_name s n =
795 if s = @{const_name Pair} then
796 if n = 0 then @{const_name fst} else @{const_name snd}
799 (* styp -> int -> styp *)
800 fun nth_sel_for_constr x ~1 = discr_for_constr x
801 | nth_sel_for_constr (s, T) n =
802 (nth_sel_name_for_constr_name s n,
803 body_type T --> nth (maybe_curried_binder_types T) n)
804 (* hol_context -> bool -> styp -> int -> styp *)
805 fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
806 apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
807 oo nth_sel_for_constr
810 fun sel_no_from_name s =
811 if String.isPrefix discr_prefix s then
813 else if String.isPrefix sel_prefix s then
814 s |> unprefix sel_prefix |> Int.fromString |> the
815 else if s = @{const_name snd} then
823 (* (indexname * typ) list -> (indexname * typ) list -> term -> term *)
824 fun close_up zs zs' =
825 fold (fn (z as ((s, _), T)) => fn t' =>
826 Term.all T $ Abs (s, T, abstract_over (Var z, t')))
827 (take (length zs' - length zs) zs')
828 (* (indexname * typ) list -> term -> term *)
829 fun aux zs (@{const "==>"} $ t1 $ t2) =
830 let val zs' = Term.add_vars t1 zs in
831 close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
833 | aux zs t = close_up zs (Term.add_vars t zs) t
836 (* typ list -> term -> int -> term *)
837 fun eta_expand _ t 0 = t
838 | eta_expand Ts (Abs (s, T, t')) n =
839 Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
840 | eta_expand Ts t n =
841 fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
842 (List.take (binder_types (fastype_of1 (Ts, t)), n))
843 (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
846 fun extensionalize t =
848 (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
849 | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>
850 let val v = Var ((s, maxidx_of_term t + 1), T) in
851 extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))
855 (* typ -> term list -> term *)
856 fun distinctness_formula T =
857 all_distinct_unordered_pairs_of
858 #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
859 #> List.foldr (s_conj o swap) @{const True}
862 fun zero_const T = Const (@{const_name zero_class.zero}, T)
863 fun suc_const T = Const (@{const_name Suc}, T --> T)
865 (* hol_context -> typ -> styp list *)
866 fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
867 (T as Type (s, Ts)) =
868 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
869 SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
871 if is_datatype thy stds T then
872 case Datatype.get_info thy s of
873 SOME {index, descr, ...} =>
875 val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
878 (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
882 if is_record_type T then
884 val s' = unsuffix Record.ext_typeN s ^ Record.extN
885 val T' = (Record.get_extT_fields thy T
886 |> apsnd single |> uncurry append |> map snd) ---> T
888 else if is_quot_type thy T then
889 [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
890 else case typedef_info thy s of
891 SOME {abs_type, rep_type, Abs_name, ...} =>
892 [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
894 if T = @{typ ind} then
895 [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
900 | uncached_datatype_constrs _ _ = []
901 (* hol_context -> typ -> styp list *)
902 fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
903 case AList.lookup (op =) (!constr_cache) T of
906 let val xs = uncached_datatype_constrs hol_ctxt T in
907 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
909 (* hol_context -> bool -> typ -> styp list *)
910 fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
911 map (apsnd ((binarize ? binarize_nat_and_int_in_type)
912 o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
913 (* hol_context -> typ -> int *)
914 val num_datatype_constrs = length oo datatype_constrs
916 (* string -> string *)
917 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
918 | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
919 | constr_name_for_sel_like s' = original_name s'
920 (* hol_context -> bool -> styp -> styp *)
921 fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
922 let val s = constr_name_for_sel_like s' in
924 (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
929 (* hol_context -> styp -> term *)
930 fun discr_term_for_constr hol_ctxt (x as (s, T)) =
931 let val dataT = body_type T in
932 if s = @{const_name Suc} then
934 @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
935 else if num_datatype_constrs hol_ctxt dataT >= 2 then
936 Const (discr_for_constr x)
938 Abs (Name.uu, dataT, @{const True})
940 (* hol_context -> styp -> term -> term *)
941 fun discriminate_value (hol_ctxt as {thy, ...}) x t =
944 if x = x' then @{const True}
945 else if is_constr_like thy x' then @{const False}
946 else betapply (discr_term_for_constr hol_ctxt x, t)
947 | _ => betapply (discr_term_for_constr hol_ctxt x, t)
949 (* theory -> (typ option * bool) list -> styp -> term -> term *)
950 fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
951 let val (arg_Ts, dataT) = strip_type T in
952 if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
953 @{term "%n::nat. n - 1"}
954 else if is_pair_type dataT then
955 Const (nth_sel_for_constr x n)
958 (* int -> typ -> int * term *)
959 fun aux m (Type ("*", [T1, T2])) =
961 val (m, t1) = aux m T1
962 val (m, t2) = aux m T2
963 in (m, HOLogic.mk_prod (t1, t2)) end
965 (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
967 val m = fold (Integer.add o num_factors_in_type)
968 (List.take (arg_Ts, n)) 0
969 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
971 (* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *)
972 fun select_nth_constr_arg thy stds x t n res_T =
973 (case strip_comb t of
975 if x = x' then nth args n
976 else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
979 handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
981 (* theory -> (typ option * bool) list -> styp -> term list -> term *)
982 fun construct_value _ _ x [] = Const x
983 | construct_value thy stds (x as (s, _)) args =
984 let val args = map Envir.eta_contract args in
987 if is_sel_like_and_no_discr s' andalso
988 constr_name_for_sel_like s' = s andalso
989 forall (fn (n, t') =>
990 select_nth_constr_arg thy stds x t n dummyT = t')
991 (index_seq 0 (length args) ~~ args) then
994 list_comb (Const x, args)
995 | _ => list_comb (Const x, args)
998 (* (typ * int) list -> typ -> int *)
999 fun card_of_type assigns (Type ("fun", [T1, T2])) =
1000 reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
1001 | card_of_type assigns (Type ("*", [T1, T2])) =
1002 card_of_type assigns T1 * card_of_type assigns T2
1003 | card_of_type _ (Type (@{type_name itself}, _)) = 1
1004 | card_of_type _ @{typ prop} = 2
1005 | card_of_type _ @{typ bool} = 2
1006 | card_of_type _ @{typ unit} = 1
1007 | card_of_type assigns T =
1008 case AList.lookup (op =) assigns T of
1010 | NONE => if T = @{typ bisim_iterator} then 0
1011 else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
1012 (* int -> (typ * int) list -> typ -> int *)
1013 fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
1015 val k1 = bounded_card_of_type max default_card assigns T1
1016 val k2 = bounded_card_of_type max default_card assigns T2
1018 if k1 = max orelse k2 = max then max
1019 else Int.min (max, reasonable_power k2 k1)
1021 | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
1023 val k1 = bounded_card_of_type max default_card assigns T1
1024 val k2 = bounded_card_of_type max default_card assigns T2
1025 in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
1026 | bounded_card_of_type max default_card assigns T =
1027 Int.min (max, if default_card = ~1 then
1028 card_of_type assigns T
1030 card_of_type assigns T
1031 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
1033 (* hol_context -> int -> (typ * int) list -> typ -> int *)
1034 fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
1036 (* typ list -> typ -> int *)
1038 (if member (op =) avoid T then
1041 Type ("fun", [T1, T2]) =>
1043 val k1 = aux avoid T1
1044 val k2 = aux avoid T2
1046 if k1 = 0 orelse k2 = 0 then 0
1047 else if k1 >= max orelse k2 >= max then max
1048 else Int.min (max, reasonable_power k2 k1)
1050 | Type ("*", [T1, T2]) =>
1052 val k1 = aux avoid T1
1053 val k2 = aux avoid T2
1055 if k1 = 0 orelse k2 = 0 then 0
1056 else if k1 >= max orelse k2 >= max then max
1057 else Int.min (max, k1 * k2)
1059 | Type (@{type_name itself}, _) => 1
1064 (case datatype_constrs hol_ctxt T of
1065 [] => if is_integer_type T orelse is_bit_type T then 0
1070 map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
1073 if exists (curry (op =) 0) constr_cards then 0
1074 else Integer.sum constr_cards
1076 | _ => raise SAME ())
1078 AList.lookup (op =) assigns T |> the_default default_card
1079 in Int.min (max, aux [] T) end
1081 (* hol_context -> typ -> bool *)
1082 fun is_finite_type hol_ctxt =
1083 not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
1086 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
1087 | is_ground_term (Const _) = true
1088 | is_ground_term _ = false
1090 (* term -> word -> word *)
1091 fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
1092 | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
1093 | hashw_term _ = 0w0
1095 val hash_term = Word.toInt o hashw_term
1097 (* term list -> (indexname * typ) list *)
1098 fun special_bounds ts =
1099 fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
1101 (* indexname * typ -> term -> term *)
1102 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
1104 (* theory -> string -> bool *)
1105 fun is_funky_typedef_name thy s =
1106 member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
1107 @{type_name int}] s orelse
1108 is_frac_type thy (Type (s, []))
1109 (* theory -> typ -> bool *)
1110 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
1111 | is_funky_typedef _ _ = false
1113 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
1114 $ Const (@{const_name TYPE}, _)) = true
1115 | is_arity_type_axiom _ = false
1116 (* theory -> bool -> term -> bool *)
1117 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
1118 is_typedef_axiom thy boring t2
1119 | is_typedef_axiom thy boring
1120 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
1121 $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
1122 boring <> is_funky_typedef_name thy s andalso is_typedef thy s
1123 | is_typedef_axiom _ _ _ = false
1125 (* Distinguishes between (1) constant definition axioms, (2) type arity and
1126 typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
1127 Typedef axioms are uninteresting to Nitpick, because it can retrieve them
1128 using "typedef_info". *)
1129 (* theory -> (string * term) list -> string list -> term list * term list *)
1130 fun partition_axioms_by_definitionality thy axioms def_names =
1132 val axioms = sort (fast_string_ord o pairself fst) axioms
1133 val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
1135 OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
1136 |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
1137 in pairself (map snd) (defs, nondefs) end
1139 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
1140 will do as long as it contains all the "axioms" and "axiomatization"
1142 (* theory -> bool *)
1143 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
1146 val is_plain_definition =
1150 case strip_comb t1 of
1152 forall is_Var args andalso not (has_duplicates (op =) args)
1154 fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
1155 | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
1160 (* theory -> term list * term list * term list *)
1161 fun all_axioms_of thy =
1163 (* theory list -> term list *)
1164 val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
1165 val specs = Defs.all_specifications_of (Theory.defs_of thy)
1166 val def_names = specs |> maps snd |> map_filter #def
1167 |> OrdList.make fast_string_ord
1168 val thys = thy :: Theory.ancestors_of thy
1169 val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
1170 val built_in_axioms = axioms_of_thys built_in_thys
1171 val user_axioms = axioms_of_thys user_thys
1172 val (built_in_defs, built_in_nondefs) =
1173 partition_axioms_by_definitionality thy built_in_axioms def_names
1174 ||> filter (is_typedef_axiom thy false)
1175 val (user_defs, user_nondefs) =
1176 partition_axioms_by_definitionality thy user_axioms def_names
1177 val (built_in_nondefs, user_nondefs) =
1178 List.partition (is_typedef_axiom thy false) user_nondefs
1179 |>> append built_in_nondefs
1181 (thy |> PureThy.all_thms_of
1182 |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
1183 |> map (prop_of o snd) |> filter is_plain_definition) @
1184 user_defs @ built_in_defs
1185 in (defs, built_in_nondefs, user_nondefs) end
1187 (* theory -> (typ option * bool) list -> bool -> styp -> int option *)
1188 fun arity_of_built_in_const thy stds fast_descrs (s, T) =
1189 if s = @{const_name If} then
1190 if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
1192 let val std_nats = is_standard_datatype thy stds nat_T in
1193 case AList.lookup (op =)
1195 |> std_nats ? append built_in_nat_consts
1196 |> fast_descrs ? append built_in_descr_consts) s of
1199 case AList.lookup (op =)
1200 (built_in_typed_consts
1201 |> std_nats ? append built_in_typed_nat_consts)
1202 (s, unarize_type T) of
1206 @{const_name zero_class.zero} =>
1207 if is_iterator_type T then SOME 0 else NONE
1208 | @{const_name Suc} =>
1209 if is_iterator_type (domain_type T) then SOME 0 else NONE
1210 | _ => if is_fun_type T andalso is_set_type (domain_type T) then
1211 AList.lookup (op =) built_in_set_consts s
1215 (* theory -> (typ option * bool) list -> bool -> styp -> bool *)
1216 val is_built_in_const = is_some oooo arity_of_built_in_const
1218 (* This function is designed to work for both real definition axioms and
1219 simplification rules (equational specifications). *)
1221 fun term_under_def t =
1223 @{const "==>"} $ _ $ t2 => term_under_def t2
1224 | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
1225 | @{const Trueprop} $ t1 => term_under_def t1
1226 | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
1227 | Abs (_, _, t') => term_under_def t'
1228 | t1 $ _ => term_under_def t1
1231 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
1232 traversal of the term, without which the wrong occurrence of a constant could
1233 be matched in the face of overloading. *)
1234 (* theory -> (typ option * bool) list -> bool -> const_table -> styp
1236 fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
1237 if is_built_in_const thy stds fast_descrs x then
1240 these (Symtab.lookup table s)
1241 |> map_filter (try (Refute.specialize_type thy x))
1242 |> filter (curry (op =) (Const x) o term_under_def)
1244 (* term -> term option *)
1245 fun normalized_rhs_of t =
1247 (* term option -> term option *)
1248 fun aux (v as Var _) (SOME t) = SOME (lambda v t)
1249 | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
1253 Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
1254 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
1256 | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
1257 val args = strip_comb lhs |> snd
1258 in fold_rev aux args (SOME rhs) end
1260 (* theory -> const_table -> styp -> term option *)
1261 fun def_of_const thy table (x as (s, _)) =
1262 if is_built_in_const thy [(NONE, false)] false x orelse
1263 original_name s <> s then
1266 x |> def_props_for_const thy [(NONE, false)] false table |> List.last
1267 |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
1268 handle List.Empty => NONE
1270 (* term -> fixpoint_kind *)
1271 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
1272 | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
1273 | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
1274 | fixpoint_kind_of_rhs _ = NoFp
1276 (* theory -> const_table -> term -> bool *)
1277 fun is_mutually_inductive_pred_def thy table t =
1280 fun is_good_arg (Bound _) = true
1281 | is_good_arg (Const (s, _)) =
1282 s = @{const_name True} orelse s = @{const_name False} orelse
1283 s = @{const_name undefined}
1284 | is_good_arg _ = false
1286 case t |> strip_abs_body |> strip_comb of
1287 (Const x, ts as (_ :: _)) =>
1288 (case def_of_const thy table x of
1289 SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
1293 (* theory -> const_table -> term -> term *)
1294 fun unfold_mutually_inductive_preds thy table =
1295 map_aterms (fn t as Const x =>
1296 (case def_of_const thy table x of
1298 let val t' = Envir.eta_contract t' in
1299 if is_mutually_inductive_pred_def thy table t' then t'
1305 (* term -> string * term *)
1306 fun pair_for_prop t =
1307 case term_under_def t of
1308 Const (s, _) => (s, t)
1309 | Free _ => raise NOT_SUPPORTED "local definitions"
1310 | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
1312 (* (Proof.context -> term list) -> Proof.context -> const_table *)
1313 fun table_for get ctxt =
1314 get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
1316 (* theory -> (typ option * bool) list -> (string * int) list *)
1317 fun case_const_names thy stds =
1318 Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
1319 if is_basic_datatype thy stds dtype_s then
1322 cons (case_name, AList.lookup (op =) descr index
1323 |> the |> #3 |> length))
1324 (Datatype.get_all thy) [] @
1325 map (apsnd length o snd) (#codatatypes (Data.get thy))
1327 (* Proof.context -> term list -> const_table *)
1328 fun const_def_table ctxt ts =
1329 table_for (map prop_of o Nitpick_Defs.get) ctxt
1330 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
1331 (map pair_for_prop ts)
1332 (* term list -> const_table *)
1333 fun const_nondef_table ts =
1334 fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
1335 |> AList.group (op =) |> Symtab.make
1336 (* Proof.context -> const_table *)
1337 val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
1338 val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
1339 (* Proof.context -> const_table -> const_table *)
1340 fun inductive_intro_table ctxt def_table =
1341 table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
1342 def_table o prop_of)
1343 o Nitpick_Intros.get) ctxt
1344 (* theory -> term list Inttab.table *)
1345 fun ground_theorem_table thy =
1346 fold ((fn @{const Trueprop} $ t1 =>
1347 is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
1348 | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
1350 val basic_ersatz_table =
1351 [(@{const_name prod_case}, @{const_name split}),
1352 (@{const_name card}, @{const_name card'}),
1353 (@{const_name setsum}, @{const_name setsum'}),
1354 (@{const_name fold_graph}, @{const_name fold_graph'}),
1355 (@{const_name wf}, @{const_name wf'}),
1356 (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
1357 (@{const_name wfrec}, @{const_name wfrec'})]
1359 (* theory -> (string * string) list *)
1360 fun ersatz_table thy =
1361 fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
1363 (* const_table Unsynchronized.ref -> string -> term list -> unit *)
1364 fun add_simps simp_table s eqs =
1365 Unsynchronized.change simp_table
1366 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
1368 (* theory -> styp -> term list *)
1369 fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
1370 let val abs_T = domain_type T in
1371 typedef_info thy (fst (dest_Type abs_T)) |> the
1372 |> pairf #Abs_inverse #Rep_inverse
1373 |> pairself (Refute.specialize_type thy x o prop_of o the)
1376 (* theory -> string * typ list -> term list *)
1377 fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
1378 let val abs_T = Type abs_z in
1379 if is_univ_typedef thy abs_T then
1381 else case typedef_info thy abs_s of
1382 SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
1384 val rep_T = instantiate_type thy abs_type abs_T rep_type
1385 val rep_t = Const (Rep_name, abs_T --> rep_T)
1386 val set_t = Const (set_name, rep_T --> bool_T)
1388 prop_of_Rep |> HOLogic.dest_Trueprop
1389 |> Refute.specialize_type thy (dest_Const rep_t)
1390 |> HOLogic.dest_mem |> snd
1392 [HOLogic.all_const abs_T
1393 $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
1394 |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
1395 |> map HOLogic.mk_Trueprop
1399 fun optimized_quot_type_axioms thy stds abs_z =
1401 val abs_T = Type abs_z
1402 val rep_T = rep_type_for_quot_type thy abs_T
1403 val equiv_rel = equiv_relation_for_quot_type thy abs_T
1404 val a_var = Var (("a", 0), abs_T)
1405 val x_var = Var (("x", 0), rep_T)
1406 val y_var = Var (("y", 0), rep_T)
1407 val x = (@{const_name Quot}, rep_T --> abs_T)
1408 val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
1409 val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
1410 val normal_x = normal_t $ x_var
1411 val normal_y = normal_t $ y_var
1412 val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
1414 [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t),
1416 ([@{const Not} $ (is_unknown_t $ normal_x),
1417 @{const Not} $ (is_unknown_t $ normal_y),
1418 equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
1419 Logic.mk_equals (normal_x, normal_y)),
1421 $ (HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)))
1422 $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
1425 (* theory -> (typ option * bool) list -> int * styp -> term *)
1426 fun constr_case_body thy stds (j, (x as (_, T))) =
1427 let val arg_Ts = binder_types T in
1428 list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
1429 (index_seq 0 (length arg_Ts)) arg_Ts)
1431 (* hol_context -> typ -> int * styp -> term -> term *)
1432 fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
1433 Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
1434 $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
1436 (* hol_context -> typ -> typ -> term *)
1437 fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
1439 val xs = datatype_constrs hol_ctxt dataT
1440 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
1441 val (xs', x) = split_last xs
1443 constr_case_body thy stds (1, x)
1444 |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
1445 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
1448 (* hol_context -> string -> typ -> typ -> term -> term *)
1449 fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
1450 let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
1451 case no_of_record_field thy s rec_T of
1452 ~1 => (case rec_T of
1453 Type (_, Ts as _ :: _) =>
1455 val rec_T' = List.last Ts
1456 val j = num_record_fields thy rec_T - 1
1458 select_nth_constr_arg thy stds constr_x t j res_T
1459 |> optimized_record_get hol_ctxt s rec_T' res_T
1461 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
1463 | j => select_nth_constr_arg thy stds constr_x t j res_T
1465 (* hol_context -> string -> typ -> term -> term -> term *)
1466 fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
1468 val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
1469 val Ts = binder_types constr_T
1471 val special_j = no_of_record_field thy s rec_T
1473 map2 (fn j => fn T =>
1474 let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
1475 if j = special_j then
1477 else if j = n - 1 andalso special_j = ~1 then
1478 optimized_record_update hol_ctxt s
1479 (rec_T |> dest_Type |> snd |> List.last) fun_t t
1482 end) (index_seq 0 n) Ts
1483 in list_comb (Const constr_x, ts) end
1485 (* theory -> const_table -> string * typ -> fixpoint_kind *)
1486 fun fixpoint_kind_of_const thy table x =
1487 if is_built_in_const thy [(NONE, false)] false x then
1490 fixpoint_kind_of_rhs (the (def_of_const thy table x))
1491 handle Option.Option => NoFp
1493 (* hol_context -> styp -> bool *)
1494 fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
1495 ...} : hol_context) x =
1496 fixpoint_kind_of_const thy def_table x <> NoFp andalso
1497 not (null (def_props_for_const thy stds fast_descrs intro_table x))
1498 fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
1499 ...} : hol_context) x =
1500 exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
1502 [!simp_table, psimp_table]
1503 fun is_inductive_pred hol_ctxt =
1504 is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
1505 fun is_equational_fun hol_ctxt =
1506 (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
1507 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
1509 (* term * term -> term *)
1510 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
1511 | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
1512 | s_betapply p = betapply p
1513 (* term * term list -> term *)
1514 val s_betapplys = Library.foldl s_betapply
1517 fun lhs_of_equation t =
1519 Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1520 | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
1521 | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
1522 | @{const Trueprop} $ t1 => lhs_of_equation t1
1523 | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1524 | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
1525 | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
1527 (* theory -> term -> bool *)
1528 fun is_constr_pattern _ (Bound _) = true
1529 | is_constr_pattern _ (Var _) = true
1530 | is_constr_pattern thy t =
1531 case strip_comb t of
1533 is_constr_like thy x andalso forall (is_constr_pattern thy) args
1535 fun is_constr_pattern_lhs thy t =
1536 forall (is_constr_pattern thy) (snd (strip_comb t))
1537 fun is_constr_pattern_formula thy t =
1538 case lhs_of_equation t of
1539 SOME t' => is_constr_pattern_lhs thy t'
1542 (* Prevents divergence in case of cyclic or infinite definition dependencies. *)
1543 val unfold_max_depth = 255
1545 (* hol_context -> term -> term *)
1546 fun unfold_defs_in_term (hol_ctxt as {thy, stds, fast_descrs, case_names,
1547 def_table, ground_thm_table, ersatz_table,
1550 (* int -> typ list -> term -> term *)
1551 fun do_term depth Ts t =
1553 (t0 as Const (@{const_name Int.number_class.number_of},
1554 Type ("fun", [_, ran_T]))) $ t1 =>
1555 ((if is_number_type thy ran_T then
1557 val j = t1 |> HOLogic.dest_numeral
1558 |> ran_T = nat_T ? Integer.max 0
1559 val s = numeral_prefix ^ signed_string_of_int j
1561 if is_integer_like_type ran_T then
1562 if is_standard_datatype thy stds ran_T then
1565 funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
1567 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
1570 handle TERM _ => raise SAME ()
1573 handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
1574 | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
1575 do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
1576 | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
1577 betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
1578 map (do_term depth Ts) [t1, t2])
1579 | Const (x as (@{const_name distinct},
1580 Type ("fun", [Type (@{type_name list}, [T']), _])))
1582 (t1 |> HOLogic.dest_list |> distinctness_formula T'
1583 handle TERM _ => do_const depth Ts t x [t1])
1584 | Const (x as (@{const_name If}, _)) $ t1 $ t2 $ t3 =>
1585 if is_ground_term t1 andalso
1586 exists (Pattern.matches thy o rpair t1)
1587 (Inttab.lookup_list ground_thm_table (hash_term t1)) then
1590 do_const depth Ts t x [t1, t2, t3]
1591 | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
1592 | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
1593 | Const x $ t1 => do_const depth Ts t x [t1]
1594 | Const x => do_const depth Ts t x []
1595 | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
1599 | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
1600 (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
1601 and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
1602 (Abs (Name.uu, body_type T,
1603 select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
1604 | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
1605 (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
1606 (* int -> typ list -> term -> styp -> term list -> term *)
1607 and do_const depth Ts t (x as (s, T)) ts =
1608 case AList.lookup (op =) ersatz_table s of
1610 do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
1614 if is_built_in_const thy stds fast_descrs x then
1616 else case AList.lookup (op =) case_names s of
1619 val (dataT, res_T) = nth_range_type n T
1620 |> pairf domain_type range_type
1622 (optimized_case_def hol_ctxt dataT res_T
1623 |> do_term (depth + 1) Ts, ts)
1626 if is_constr thy stds x then
1628 else if is_stale_constr thy x then
1629 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
1631 else if is_quot_abs_fun thy x then
1633 val rep_T = domain_type T
1634 val abs_T = range_type T
1636 (Abs (Name.uu, rep_T,
1637 Const (@{const_name Quot}, rep_T --> abs_T)
1638 $ (Const (@{const_name quot_normal},
1639 rep_T --> rep_T) $ Bound 0)), ts)
1641 else if is_quot_rep_fun thy x then
1643 val abs_T = domain_type T
1644 val rep_T = range_type T
1645 val x' = (@{const_name Quot}, rep_T --> abs_T)
1646 in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end
1647 else if is_record_get thy x then
1649 0 => (do_term depth Ts (eta_expand Ts t 1), [])
1650 | _ => (optimized_record_get hol_ctxt s (domain_type T)
1651 (range_type T) (do_term depth Ts (hd ts)), tl ts)
1652 else if is_record_update thy x then
1654 2 => (optimized_record_update hol_ctxt
1655 (unsuffix Record.updateN s) (nth_range_type 2 T)
1656 (do_term depth Ts (hd ts))
1657 (do_term depth Ts (nth ts 1)), [])
1658 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
1659 else if is_rep_fun thy x then
1660 let val x' = mate_of_rep_fun thy x in
1661 if is_constr thy stds x' then
1662 select_nth_constr_arg_with_args depth Ts x' ts 0
1667 else if is_equational_fun hol_ctxt x then
1669 else case def_of_const thy def_table x of
1671 if depth > unfold_max_depth then
1672 raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
1673 "too many nested definitions (" ^
1674 string_of_int depth ^ ") while expanding " ^
1676 else if s = @{const_name wfrec'} then
1677 (do_term (depth + 1) Ts (betapplys (def, ts)), [])
1679 (do_term (depth + 1) Ts def, ts)
1680 | NONE => (Const x, ts)
1681 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
1684 (* hol_context -> typ -> term list *)
1685 fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
1687 val xs = datatype_constrs hol_ctxt T
1688 val set_T = T --> bool_T
1689 val iter_T = @{typ bisim_iterator}
1690 val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
1691 val bisim_max = @{const bisim_iterator_max}
1692 val n_var = Var (("n", 0), iter_T)
1694 Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T)
1695 $ Abs ("m", iter_T, HOLogic.eq_const iter_T
1696 $ (suc_const iter_T $ Bound 0) $ n_var)
1697 val x_var = Var (("x", 0), T)
1698 val y_var = Var (("y", 0), T)
1699 (* styp -> int -> typ -> term *)
1700 fun nth_sub_bisim x n nth_T =
1701 (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
1702 else HOLogic.eq_const nth_T)
1703 $ select_nth_constr_arg thy stds x x_var n nth_T
1704 $ select_nth_constr_arg thy stds x y_var n nth_T
1706 fun case_func (x as (_, T)) =
1708 val arg_Ts = binder_types T
1710 discriminate_value hol_ctxt x y_var ::
1711 map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
1713 in List.foldr absdummy core_t arg_Ts end
1715 [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
1716 $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
1717 $ (betapplys (optimized_case_def hol_ctxt T bool_T,
1718 map case_func xs @ [x_var]))),
1719 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
1720 $ (Const (@{const_name insert}, T --> set_T --> set_T)
1721 $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
1722 |> map HOLogic.mk_Trueprop
1725 exception NO_TRIPLE of unit
1727 (* theory -> styp -> term -> term list * term list * term *)
1728 fun triple_for_intro_rule thy x t =
1730 val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
1731 val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
1732 val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
1734 val is_good_head = curry (op =) (Const x) o head_of
1736 if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
1740 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
1742 (* indexname * typ -> term list -> term -> term -> term *)
1743 fun wf_constraint_for rel side concl main =
1745 val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
1746 tuple_for_args concl), Var rel)
1747 val t = List.foldl HOLogic.mk_imp core side
1748 val vars = filter (not_equal rel) (Term.add_vars t [])
1750 Library.foldl (fn (t', ((x, j), T)) =>
1752 $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
1756 (* indexname * typ -> term list * term list * term -> term *)
1757 fun wf_constraint_for_triple rel (side, main, concl) =
1758 map (wf_constraint_for rel side concl) main |> foldr1 s_conj
1760 (* Proof.context -> Time.time option -> thm
1761 -> (Proof.context -> tactic -> tactic) -> bool *)
1762 fun terminates_by ctxt timeout goal tac =
1763 can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
1764 #> SINGLE (DETERM_TIMEOUT timeout
1765 (tac ctxt (auto_tac (clasimpset_of ctxt))))
1766 #> the #> Goal.finish ctxt) goal
1768 val max_cached_wfs = 50
1769 val cached_timeout =
1770 Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
1771 val cached_wf_props =
1772 Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
1774 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
1775 ScnpReconstruct.sizechange_tac]
1777 (* hol_context -> const_table -> styp -> bool *)
1778 fun uncached_is_well_founded_inductive_pred
1779 ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
1780 : hol_context) (x as (_, T)) =
1781 case def_props_for_const thy stds fast_descrs intro_table x of
1782 [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
1785 (case map (triple_for_intro_rule thy x) intro_ts
1786 |> filter_out (null o #2) of
1790 val binders_T = HOLogic.mk_tupleT (binder_types T)
1791 val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
1792 val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
1793 val rel = (("R", j), rel_T)
1794 val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
1795 map (wf_constraint_for_triple rel) triples
1796 |> foldr1 s_conj |> HOLogic.mk_Trueprop
1797 val _ = if debug then
1798 priority ("Wellfoundedness goal: " ^
1799 Syntax.string_of_term ctxt prop ^ ".")
1803 if tac_timeout = Synchronized.value cached_timeout andalso
1804 length (Synchronized.value cached_wf_props) < max_cached_wfs then
1807 (Synchronized.change cached_wf_props (K []);
1808 Synchronized.change cached_timeout (K tac_timeout));
1809 case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
1813 val goal = prop |> cterm_of thy |> Goal.init
1814 val wf = exists (terminates_by ctxt tac_timeout goal)
1816 in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
1818 handle List.Empty => false
1819 | NO_TRIPLE () => false
1821 (* The type constraint below is a workaround for a Poly/ML crash. *)
1823 (* hol_context -> styp -> bool *)
1824 fun is_well_founded_inductive_pred
1825 (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
1827 case triple_lookup (const_match thy) wfs x of
1829 | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
1830 case AList.lookup (op =) (!wf_cache) x of
1834 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
1835 val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
1837 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
1840 (* typ list -> typ -> term -> term *)
1841 fun ap_curry [_] _ t = t
1842 | ap_curry arg_Ts tuple_T t =
1843 let val n = length arg_Ts in
1844 list_abs (map (pair "c") arg_Ts,
1846 $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
1849 (* int -> term -> int *)
1850 fun num_occs_of_bound_in_term j (t1 $ t2) =
1851 op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
1852 | num_occs_of_bound_in_term j (Abs (_, _, t')) =
1853 num_occs_of_bound_in_term (j + 1) t'
1854 | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
1855 | num_occs_of_bound_in_term _ _ = 0
1858 val is_linear_inductive_pred_def =
1860 (* int -> term -> bool *)
1861 fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
1862 do_disjunct (j + 1) t2
1864 case num_occs_of_bound_in_term j t of
1866 | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
1869 fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
1870 let val (xs, body) = strip_abs t2 in
1873 | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
1875 | do_lfp_def _ = false
1876 in do_lfp_def o strip_abs_body end
1878 (* int -> int list list *)
1879 fun n_ptuple_paths 0 = []
1880 | n_ptuple_paths 1 = []
1881 | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
1882 (* int -> typ -> typ -> term -> term *)
1883 val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
1885 (* term -> term * term *)
1886 val linear_pred_base_and_step_rhss =
1889 fun aux (Const (@{const_name lfp}, _) $ t2) =
1891 val (xs, body) = strip_abs t2
1892 val arg_Ts = map snd (tl xs)
1893 val tuple_T = HOLogic.mk_tupleT arg_Ts
1894 val j = length arg_Ts
1895 (* int -> term -> term *)
1896 fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
1897 Const (@{const_name Ex}, T1)
1898 $ Abs (s2, T2, repair_rec (j + 1) t2')
1899 | repair_rec j (@{const "op &"} $ t1 $ t2) =
1900 @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
1902 let val (head, args) = strip_comb t in
1903 if head = Bound j then
1904 HOLogic.eq_const tuple_T $ Bound j
1905 $ mk_flat_tuple tuple_T args
1909 val (nonrecs, recs) =
1910 List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
1912 val base_body = nonrecs |> List.foldl s_disj @{const False}
1913 val step_body = recs |> map (repair_rec j)
1914 |> List.foldl s_disj @{const False}
1916 (list_abs (tl xs, incr_bv (~1, j, base_body))
1917 |> ap_n_split (length arg_Ts) tuple_T bool_T,
1918 Abs ("y", tuple_T, list_abs (tl xs, step_body)
1919 |> ap_n_split (length arg_Ts) tuple_T bool_T))
1922 raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
1925 (* hol_context -> styp -> term -> term *)
1926 fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
1928 val j = maxidx_of_term def + 1
1929 val (outer, fp_app) = strip_abs def
1930 val outer_bounds = map Bound (length outer - 1 downto 0)
1931 val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer
1932 val fp_app = subst_bounds (rev outer_vars, fp_app)
1933 val (outer_Ts, rest_T) = strip_n_binders (length outer) T
1934 val tuple_arg_Ts = strip_type rest_T |> fst
1935 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
1936 val set_T = tuple_T --> bool_T
1937 val curried_T = tuple_T --> set_T
1938 val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
1939 val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
1940 val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
1941 val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
1942 |> HOLogic.mk_Trueprop
1943 val _ = add_simps simp_table base_s [base_eq]
1944 val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T)
1945 val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs)
1946 |> HOLogic.mk_Trueprop
1947 val _ = add_simps simp_table step_s [step_eq]
1950 Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
1951 $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
1952 $ (Const (@{const_name split}, curried_T --> uncurried_T)
1953 $ list_comb (Const step_x, outer_bounds)))
1954 $ list_comb (Const base_x, outer_bounds)
1955 |> ap_curry tuple_arg_Ts tuple_T)
1956 |> unfold_defs_in_term hol_ctxt
1959 (* hol_context -> bool -> styp -> term *)
1960 fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
1961 def_table, simp_table, ...})
1964 val iter_T = iterator_type_for_const gfp x
1965 val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
1966 val unrolled_const = Const x' $ zero_const iter_T
1967 val def = the (def_of_const thy def_table x)
1969 if is_equational_fun hol_ctxt x' then
1970 unrolled_const (* already done *)
1971 else if not gfp andalso is_linear_inductive_pred_def def andalso
1972 star_linear_preds then
1973 starred_linear_pred_const hol_ctxt x def
1976 val j = maxidx_of_term def + 1
1977 val (outer, fp_app) = strip_abs def
1978 val outer_bounds = map Bound (length outer - 1 downto 0)
1979 val cur = Var ((iter_var_prefix, j + 1), iter_T)
1980 val next = suc_const iter_T $ cur
1981 val rhs = case fp_app of
1983 betapply (t, list_comb (Const x', next :: outer_bounds))
1984 | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
1986 val (inner, naked_rhs) = strip_abs rhs
1987 val all = outer @ inner
1988 val bounds = map Bound (length all - 1 downto 0)
1989 val vars = map (fn (s, T) => Var ((s, j), T)) all
1990 val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs)
1991 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
1992 val _ = add_simps simp_table s' [eq]
1993 in unrolled_const end
1996 (* hol_context -> styp -> term *)
1997 fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
1999 val def = the (def_of_const thy def_table x)
2000 val (outer, fp_app) = strip_abs def
2001 val outer_bounds = map Bound (length outer - 1 downto 0)
2002 val rhs = case fp_app of
2003 Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
2004 | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
2006 val (inner, naked_rhs) = strip_abs rhs
2007 val all = outer @ inner
2008 val bounds = map Bound (length all - 1 downto 0)
2009 val j = maxidx_of_term def + 1
2010 val vars = map (fn (s, T) => Var ((s, j), T)) all
2012 HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
2013 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
2015 fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
2016 if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
2017 let val x' = (after_name_sep s, T) in
2018 raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
2021 raw_inductive_pred_axiom hol_ctxt x
2023 (* hol_context -> styp -> term list *)
2024 fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
2025 psimp_table, ...}) x =
2026 case def_props_for_const thy stds fast_descrs (!simp_table) x of
2027 [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
2028 [] => [inductive_pred_axiom hol_ctxt x]
2031 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
2032 (* hol_context -> styp -> bool *)
2033 fun is_equational_fun_surely_complete hol_ctxt x =
2034 case raw_equational_fun_axioms hol_ctxt x of
2035 [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
2036 strip_comb t1 |> snd |> forall is_Var
2039 (* term list -> term list *)
2040 fun merge_type_vars_in_terms ts =
2042 (* typ -> (sort * string) list -> (sort * string) list *)
2043 fun add_type (TFree (s, S)) table =
2044 (case AList.lookup (op =) table S of
2046 if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
2048 | NONE => (S, s) :: table)
2049 | add_type _ table = table
2050 val table = fold (fold_types (fold_atyps add_type)) ts []
2052 fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S)
2054 in map (map_types (map_atyps coalesce)) ts end
2056 (* hol_context -> bool -> typ -> typ list -> typ list *)
2057 fun add_ground_types hol_ctxt binarize =
2061 Type ("fun", Ts) => fold aux Ts accum
2062 | Type ("*", Ts) => fold aux Ts accum
2063 | Type (@{type_name itself}, [T1]) => aux T1 accum
2065 if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
2070 |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
2074 | _ => insert (op =) T accum
2077 (* hol_context -> bool -> typ -> typ list *)
2078 fun ground_types_in_type hol_ctxt binarize T =
2079 add_ground_types hol_ctxt binarize T []
2080 (* hol_context -> term list -> typ list *)
2081 fun ground_types_in_terms hol_ctxt binarize ts =
2082 fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
2084 (* theory -> const_table -> styp -> int list *)
2085 fun const_format thy def_table (x as (s, T)) =
2086 if String.isPrefix unrolled_prefix s then
2087 const_format thy def_table (original_name s, range_type T)
2088 else if String.isPrefix skolem_prefix s then
2090 val k = unprefix skolem_prefix s
2091 |> strip_first_name_sep |> fst |> space_explode "@"
2092 |> hd |> Int.fromString |> the
2093 in [k, num_binder_types T - k] end
2094 else if original_name s <> s then
2095 [num_binder_types T]
2096 else case def_of_const thy def_table x of
2097 SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
2098 let val k = length (strip_abs_vars t') in
2099 [k, num_binder_types T - k]
2102 [num_binder_types T]
2103 | NONE => [num_binder_types T]
2104 (* int list -> int list -> int list *)
2105 fun intersect_formats _ [] = []
2106 | intersect_formats [] _ = []
2107 | intersect_formats ks1 ks2 =
2108 let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
2109 intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
2110 (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
2114 (* theory -> const_table -> (term option * int list) list -> term -> int list *)
2115 fun lookup_format thy def_table formats t =
2116 case AList.lookup (fn (SOME x, SOME y) =>
2117 (term_match thy) (x, y) | _ => false)
2119 SOME format => format
2120 | NONE => let val format = the (AList.lookup (op =) formats NONE) in
2122 Const x => intersect_formats format
2123 (const_format thy def_table x)
2127 (* int list -> int list -> typ -> typ *)
2128 fun format_type default_format format T =
2130 val T = unarize_unbox_and_uniterize_type T
2131 val format = format |> filter (curry (op <) 0)
2133 if forall (curry (op =) 1) format then
2137 val (binder_Ts, body_T) = strip_type T
2140 |> map (format_type default_format default_format)
2141 |> rev |> chunk_list_unevenly (rev format)
2142 |> map (HOLogic.mk_tupleT o rev)
2143 in List.foldl (op -->) body_T batched end
2145 (* theory -> const_table -> (term option * int list) list -> term -> typ *)
2146 fun format_term_type thy def_table formats t =
2147 format_type (the (AList.lookup (op =) formats NONE))
2148 (lookup_format thy def_table formats t) (fastype_of t)
2150 (* int list -> int -> int list -> int list *)
2151 fun repair_special_format js m format =
2152 m - 1 downto 0 |> chunk_list_unevenly (rev format)
2153 |> map (rev o filter_out (member (op =) js))
2154 |> filter_out null |> map length |> rev
2156 (* hol_context -> string * string -> (term option * int list) list
2157 -> styp -> term * typ *)
2158 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
2159 : hol_context) (base_name, step_name) formats =
2161 val default_format = the (AList.lookup (op =) formats NONE)
2162 (* styp -> term * typ *)
2163 fun do_const (x as (s, T)) =
2164 (if String.isPrefix special_prefix s then
2167 val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
2168 val (x' as (_, T'), js, ts) =
2169 AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
2171 val max_j = List.last js
2172 val Ts = List.take (binder_types T', max_j + 1)
2173 val missing_js = filter_out (member (op =) js) (0 upto max_j)
2174 val missing_Ts = filter_indices missing_js Ts
2175 (* int -> indexname *)
2176 fun nth_missing_var n =
2177 ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
2178 val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
2179 val vars = special_bounds ts @ missing_vars
2182 case AList.lookup (op =) (js ~~ ts) j of
2185 Var (nth missing_vars
2186 (find_index (curry (op =) j) missing_js)))
2188 val t = do_const x' |> fst
2190 case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
2191 | _ => false) formats (SOME t) of
2193 repair_special_format js (num_binder_types T') format
2195 const_format thy def_table x'
2196 |> repair_special_format js (num_binder_types T')
2197 |> intersect_formats default_format
2199 (list_comb (t, ts') |> fold_rev abs_var vars,
2200 format_type default_format format T)
2202 else if String.isPrefix uncurry_prefix s then
2204 val (ss, s') = unprefix uncurry_prefix s
2205 |> strip_first_name_sep |>> space_explode "@"
2207 if String.isPrefix step_prefix s' then
2211 val k = the (Int.fromString (hd ss))
2212 val j = the (Int.fromString (List.last ss))
2213 val (before_Ts, (tuple_T, rest_T)) =
2214 strip_n_binders j T ||> (strip_n_binders 1 #>> hd)
2215 val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T
2216 in do_const (s', T') end
2218 else if String.isPrefix unrolled_prefix s then
2219 let val t = Const (original_name s, range_type T) in
2220 (lambda (Free (iter_var_prefix, nat_T)) t,
2221 format_type default_format
2222 (lookup_format thy def_table formats t) T)
2224 else if String.isPrefix base_prefix s then
2225 (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
2226 format_type default_format default_format T)
2227 else if String.isPrefix step_prefix s then
2228 (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
2229 format_type default_format default_format T)
2230 else if String.isPrefix skolem_prefix s then
2232 val ss = the (AList.lookup (op =) (!skolems) s)
2233 val (Ts, Ts') = chop (length ss) (binder_types T)
2234 val frees = map Free (ss ~~ Ts)
2235 val s' = original_name s
2237 (fold lambda frees (Const (s', Ts' ---> T)),
2238 format_type default_format
2239 (lookup_format thy def_table formats (Const x)) T)
2241 else if String.isPrefix eval_prefix s then
2243 val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
2244 in (t, format_term_type thy def_table formats t) end
2245 else if s = @{const_name undefined_fast_The} then
2246 (Const (nitpick_prefix ^ "The fallback", T),
2247 format_type default_format
2248 (lookup_format thy def_table formats
2249 (Const (@{const_name The}, (T --> bool_T) --> T))) T)
2250 else if s = @{const_name undefined_fast_Eps} then
2251 (Const (nitpick_prefix ^ "Eps fallback", T),
2252 format_type default_format
2253 (lookup_format thy def_table formats
2254 (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
2256 let val t = Const (original_name s, T) in
2257 (t, format_term_type thy def_table formats t)
2259 |>> map_types unarize_unbox_and_uniterize_type
2260 |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
2263 (* styp -> string *)
2264 fun assign_operator_for_const (s, T) =
2265 if String.isPrefix ubfp_prefix s then
2266 if is_fun_type T then "\<subseteq>" else "\<le>"
2267 else if String.isPrefix lbfp_prefix s then
2268 if is_fun_type T then "\<supseteq>" else "\<ge>"
2269 else if original_name s <> s then
2270 assign_operator_for_const (after_name_sep s, T)