added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
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 string_for_type : Proof.context -> typ -> string
69 val prefix_name : string -> string -> string
70 val shortest_name : string -> string
71 val short_name : string -> string
72 val shorten_names_in_term : term -> term
73 val type_match : theory -> typ * typ -> bool
74 val const_match : theory -> styp * styp -> bool
75 val term_match : theory -> term * term -> bool
76 val is_TFree : typ -> bool
77 val is_higher_order_type : typ -> bool
78 val is_fun_type : typ -> bool
79 val is_set_type : typ -> bool
80 val is_pair_type : typ -> bool
81 val is_lfp_iterator_type : typ -> bool
82 val is_gfp_iterator_type : typ -> bool
83 val is_fp_iterator_type : typ -> bool
84 val is_boolean_type : typ -> bool
85 val is_integer_type : typ -> bool
86 val is_bit_type : typ -> bool
87 val is_word_type : typ -> bool
88 val is_integer_like_type : typ -> bool
89 val is_record_type : typ -> bool
90 val is_number_type : theory -> typ -> bool
91 val const_for_iterator_type : typ -> styp
92 val strip_n_binders : int -> typ -> typ list * typ
93 val nth_range_type : int -> typ -> typ
94 val num_factors_in_type : typ -> int
95 val num_binder_types : typ -> int
96 val curried_binder_types : typ -> typ list
97 val mk_flat_tuple : typ -> term list -> term
98 val dest_n_tuple : int -> term -> term list
99 val is_real_datatype : theory -> string -> bool
100 val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
101 val is_quot_type : theory -> typ -> bool
102 val is_codatatype : theory -> typ -> bool
103 val is_pure_typedef : theory -> typ -> bool
104 val is_univ_typedef : theory -> typ -> bool
105 val is_datatype : theory -> (typ option * bool) list -> typ -> bool
106 val is_record_constr : styp -> bool
107 val is_record_get : theory -> styp -> bool
108 val is_record_update : theory -> styp -> bool
109 val is_abs_fun : theory -> styp -> bool
110 val is_rep_fun : theory -> styp -> bool
111 val is_quot_abs_fun : Proof.context -> styp -> bool
112 val is_quot_rep_fun : Proof.context -> styp -> bool
113 val mate_of_rep_fun : theory -> styp -> styp
114 val is_constr_like : theory -> styp -> bool
115 val is_stale_constr : theory -> styp -> bool
116 val is_constr : theory -> (typ option * bool) list -> styp -> bool
117 val is_sel : string -> bool
118 val is_sel_like_and_no_discr : string -> bool
119 val box_type : hol_context -> boxability -> typ -> typ
120 val binarize_nat_and_int_in_type : typ -> typ
121 val binarize_nat_and_int_in_term : term -> term
122 val discr_for_constr : styp -> styp
123 val num_sels_for_constr_type : typ -> int
124 val nth_sel_name_for_constr_name : string -> int -> string
125 val nth_sel_for_constr : styp -> int -> styp
126 val binarized_and_boxed_nth_sel_for_constr :
127 hol_context -> bool -> styp -> int -> styp
128 val sel_no_from_name : string -> int
129 val close_form : term -> term
130 val eta_expand : typ list -> term -> int -> term
131 val extensionalize : term -> term
132 val distinctness_formula : typ -> term list -> term
133 val register_frac_type : string -> (string * string) list -> theory -> theory
134 val unregister_frac_type : string -> theory -> theory
135 val register_codatatype : typ -> string -> styp list -> theory -> theory
136 val unregister_codatatype : typ -> theory -> theory
137 val datatype_constrs : hol_context -> typ -> styp list
138 val binarized_and_boxed_datatype_constrs :
139 hol_context -> bool -> typ -> styp list
140 val num_datatype_constrs : hol_context -> typ -> int
141 val constr_name_for_sel_like : string -> string
142 val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
143 val discriminate_value : hol_context -> styp -> term -> term
144 val select_nth_constr_arg :
145 theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
146 val construct_value :
147 theory -> (typ option * bool) list -> styp -> term list -> term
148 val card_of_type : (typ * int) list -> typ -> int
149 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
150 val bounded_exact_card_of_type :
151 hol_context -> int -> int -> (typ * int) list -> typ -> int
152 val is_finite_type : hol_context -> typ -> bool
153 val special_bounds : term list -> (indexname * typ) list
154 val is_funky_typedef : theory -> typ -> bool
155 val all_axioms_of : theory -> term list * term list * term list
156 val arity_of_built_in_const :
157 theory -> (typ option * bool) list -> bool -> styp -> int option
158 val is_built_in_const :
159 theory -> (typ option * bool) list -> bool -> styp -> bool
160 val term_under_def : term -> term
161 val case_const_names :
162 theory -> (typ option * bool) list -> (string * int) list
163 val const_def_table : Proof.context -> term list -> const_table
164 val const_nondef_table : term list -> const_table
165 val const_simp_table : Proof.context -> const_table
166 val const_psimp_table : Proof.context -> const_table
167 val inductive_intro_table : Proof.context -> const_table -> const_table
168 val ground_theorem_table : theory -> term list Inttab.table
169 val ersatz_table : theory -> (string * string) list
170 val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
171 val inverse_axioms_for_rep_fun : theory -> styp -> term list
172 val optimized_typedef_axioms : theory -> string * typ list -> term list
173 val optimized_quot_type_axioms :
174 theory -> (typ option * bool) list -> string * typ list -> term list
175 val def_of_const : theory -> const_table -> styp -> term option
176 val fixpoint_kind_of_const :
177 theory -> const_table -> string * typ -> fixpoint_kind
178 val is_inductive_pred : hol_context -> styp -> bool
179 val is_equational_fun : hol_context -> styp -> bool
180 val is_constr_pattern_lhs : theory -> term -> bool
181 val is_constr_pattern_formula : theory -> term -> bool
182 val unfold_defs_in_term : hol_context -> term -> term
183 val codatatype_bisim_axioms : hol_context -> typ -> term list
184 val is_well_founded_inductive_pred : hol_context -> styp -> bool
185 val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
186 val equational_fun_axioms : hol_context -> styp -> term list
187 val is_equational_fun_surely_complete : hol_context -> styp -> bool
188 val merge_type_vars_in_terms : term list -> term list
189 val ground_types_in_type : hol_context -> bool -> typ -> typ list
190 val ground_types_in_terms : hol_context -> bool -> term list -> typ list
191 val format_type : int list -> int list -> typ -> typ
192 val format_term_type :
193 theory -> const_table -> (term option * int list) list -> term -> typ
194 val user_friendly_const :
195 hol_context -> string * string -> (term option * int list) list
196 -> styp -> term * typ
197 val assign_operator_for_const : styp -> string
200 structure Nitpick_HOL : NITPICK_HOL =
205 type const_table = term list Symtab.table
206 type special_fun = (styp * int list * term list) * styp
207 type unrolled = styp * styp
208 type wf_cache = (styp * (bool * bool)) list
213 max_bisim_depth: int,
214 boxes: (typ option * bool option) list,
215 stds: (typ option * bool) list,
216 wfs: (styp option * bool option) list,
217 user_axioms: bool option,
219 binary_ints: bool option,
220 destroy_constrs: bool,
223 star_linear_preds: bool,
226 tac_timeout: Time.time option,
228 case_names: (string * int) list,
229 def_table: const_table,
230 nondef_table: const_table,
231 user_nondefs: term list,
232 simp_table: const_table Unsynchronized.ref,
233 psimp_table: const_table,
234 intro_table: const_table,
235 ground_thm_table: term list Inttab.table,
236 ersatz_table: (string * string) list,
237 skolems: (string * string list) list Unsynchronized.ref,
238 special_funs: special_fun list Unsynchronized.ref,
239 unrolled_preds: unrolled list Unsynchronized.ref,
240 wf_cache: wf_cache Unsynchronized.ref,
241 constr_cache: (typ * styp list) list Unsynchronized.ref}
243 datatype fixpoint_kind = Lfp | Gfp | NoFp
244 datatype boxability =
245 InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
247 structure Data = Theory_Data(
248 type T = {frac_types: (string * (string * string) list) list,
249 codatatypes: (string * (string * styp list)) list}
250 val empty = {frac_types = [], codatatypes = []}
252 fun merge ({frac_types = fs1, codatatypes = cs1},
253 {frac_types = fs2, codatatypes = cs2}) : T =
254 {frac_types = AList.merge (op =) (K true) (fs1, fs2),
255 codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
258 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
259 val sel_prefix = nitpick_prefix ^ "sel"
260 val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
261 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
262 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
263 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
264 val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep
265 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
266 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
267 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
268 val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
269 val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
270 val skolem_prefix = nitpick_prefix ^ "sk"
271 val special_prefix = nitpick_prefix ^ "sp"
272 val uncurry_prefix = nitpick_prefix ^ "unc"
273 val eval_prefix = nitpick_prefix ^ "eval"
274 val iter_var_prefix = "i"
275 val arg_var_prefix = "x"
278 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
280 (* string -> string * string *)
281 val strip_first_name_sep =
282 Substring.full #> Substring.position name_sep ##> Substring.triml 1
283 #> pairself Substring.string
284 (* string -> string *)
285 fun original_name s =
286 if String.isPrefix nitpick_prefix s then
287 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
290 val after_name_sep = snd o strip_first_name_sep
292 (* term * term -> term *)
293 fun s_conj (t1, @{const True}) = t1
294 | s_conj (@{const True}, t2) = t2
296 if t1 = @{const False} orelse t2 = @{const False} then @{const False}
297 else HOLogic.mk_conj (t1, t2)
298 fun s_disj (t1, @{const False}) = t1
299 | s_disj (@{const False}, t2) = t2
301 if t1 = @{const True} orelse t2 = @{const True} then @{const True}
302 else HOLogic.mk_disj (t1, t2)
304 (* term -> term -> term list *)
305 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
306 if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
307 | strip_connective _ t = [t]
308 (* term -> term list * term *)
309 fun strip_any_connective (t as (t0 $ t1 $ t2)) =
310 if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
311 (strip_connective t0 t, t0)
314 | strip_any_connective t = ([t], @{const Not})
315 (* term -> term list *)
316 val conjuncts_of = strip_connective @{const "op &"}
317 val disjuncts_of = strip_connective @{const "op |"}
319 (* When you add constants to these lists, make sure to handle them in
320 "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
322 val built_in_consts =
323 [(@{const_name all}, 1),
324 (@{const_name "=="}, 2),
325 (@{const_name "==>"}, 2),
326 (@{const_name Pure.conjunction}, 2),
327 (@{const_name Trueprop}, 1),
328 (@{const_name Not}, 1),
329 (@{const_name False}, 0),
330 (@{const_name True}, 0),
331 (@{const_name All}, 1),
332 (@{const_name Ex}, 1),
333 (@{const_name "op ="}, 2),
334 (@{const_name "op &"}, 2),
335 (@{const_name "op |"}, 2),
336 (@{const_name "op -->"}, 2),
337 (@{const_name If}, 3),
338 (@{const_name Let}, 2),
339 (@{const_name Unity}, 0),
340 (@{const_name Pair}, 2),
341 (@{const_name fst}, 1),
342 (@{const_name snd}, 1),
343 (@{const_name Id}, 0),
344 (@{const_name insert}, 2),
345 (@{const_name converse}, 1),
346 (@{const_name trancl}, 1),
347 (@{const_name rel_comp}, 2),
348 (@{const_name image}, 2),
349 (@{const_name finite}, 1),
350 (@{const_name unknown}, 0),
351 (@{const_name is_unknown}, 1),
352 (@{const_name Tha}, 1),
353 (@{const_name Frac}, 0),
354 (@{const_name norm_frac}, 0)]
355 val built_in_nat_consts =
356 [(@{const_name Suc}, 0),
357 (@{const_name nat}, 0),
358 (@{const_name nat_gcd}, 0),
359 (@{const_name nat_lcm}, 0)]
360 val built_in_descr_consts =
361 [(@{const_name The}, 1),
362 (@{const_name Eps}, 1)]
363 val built_in_typed_consts =
364 [((@{const_name zero_class.zero}, int_T), 0),
365 ((@{const_name one_class.one}, int_T), 0),
366 ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
367 ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
368 ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
369 ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
370 ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
371 ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
372 ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
373 val built_in_typed_nat_consts =
374 [((@{const_name zero_class.zero}, nat_T), 0),
375 ((@{const_name one_class.one}, nat_T), 0),
376 ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
377 ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
378 ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
379 ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
380 ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
381 ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
382 ((@{const_name of_nat}, nat_T --> int_T), 0)]
383 val built_in_set_consts =
384 [(@{const_name semilattice_inf_class.inf}, 2),
385 (@{const_name semilattice_sup_class.sup}, 2),
386 (@{const_name minus_class.minus}, 2),
387 (@{const_name ord_class.less_eq}, 2)]
390 fun unarize_type @{typ "unsigned_bit word"} = nat_T
391 | unarize_type @{typ "signed_bit word"} = int_T
392 | unarize_type @{typ bisim_iterator} = nat_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 @{typ bisim_iterator} = nat_T
402 | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
403 Type (s, map unarize_and_unbox_type Ts)
404 | unarize_and_unbox_type T = T
405 (* Proof.context -> typ -> string *)
406 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
408 (* string -> string -> string *)
409 val prefix_name = Long_Name.qualify o Long_Name.base_name
410 (* string -> string *)
411 fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
412 (* string -> term -> term *)
413 val prefix_abs_vars = Term.map_abs_vars o prefix_name
414 (* string -> string *)
416 case space_explode name_sep s of
417 [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
418 | ss => map shortest_name ss |> space_implode "_"
420 fun shorten_names_in_type (Type (s, Ts)) =
421 Type (short_name s, map shorten_names_in_type Ts)
422 | shorten_names_in_type T = T
424 val shorten_names_in_term =
425 map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
426 #> map_types shorten_names_in_type
428 (* theory -> typ * typ -> bool *)
429 fun type_match thy (T1, T2) =
430 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
431 handle Type.TYPE_MATCH => false
432 (* theory -> styp * styp -> bool *)
433 fun const_match thy ((s1, T1), (s2, T2)) =
434 s1 = s2 andalso type_match thy (T1, T2)
435 (* theory -> term * term -> bool *)
436 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
437 | term_match thy (Free (s1, T1), Free (s2, T2)) =
438 const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
439 | term_match thy (t1, t2) = t1 aconv t2
442 fun is_TFree (TFree _) = true
444 fun is_higher_order_type (Type ("fun", _)) = true
445 | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
446 | is_higher_order_type _ = false
447 fun is_fun_type (Type ("fun", _)) = true
448 | is_fun_type _ = false
449 fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
450 | is_set_type _ = false
451 fun is_pair_type (Type ("*", _)) = true
452 | is_pair_type _ = false
453 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
454 | is_lfp_iterator_type _ = false
455 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
456 | is_gfp_iterator_type _ = false
457 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
458 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
459 fun is_integer_type T = (T = nat_T orelse T = int_T)
460 fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
461 fun is_word_type (Type (@{type_name word}, _)) = true
462 | is_word_type _ = false
463 fun is_integer_like_type T =
464 is_fp_iterator_type T orelse is_integer_type T orelse is_word_type T orelse
465 T = @{typ bisim_iterator}
466 val is_record_type = not o null o Record.dest_recTs
467 (* theory -> typ -> bool *)
468 fun is_frac_type thy (Type (s, [])) =
469 not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
470 | is_frac_type _ _ = false
471 fun is_number_type thy = is_integer_like_type orf is_frac_type thy
473 (* bool -> styp -> typ *)
474 fun iterator_type_for_const gfp (s, T) =
475 Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
478 fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
479 | const_for_iterator_type T =
480 raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
482 (* int -> typ -> typ list * typ *)
483 fun strip_n_binders 0 T = ([], T)
484 | strip_n_binders n (Type ("fun", [T1, T2])) =
485 strip_n_binders (n - 1) T2 |>> cons T1
486 | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
487 strip_n_binders n (Type ("fun", Ts))
488 | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
490 val nth_range_type = snd oo strip_n_binders
493 fun num_factors_in_type (Type ("*", [T1, T2])) =
494 fold (Integer.add o num_factors_in_type) [T1, T2] 0
495 | num_factors_in_type _ = 1
496 fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
497 | num_binder_types _ = 0
498 (* typ -> typ list *)
499 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
500 fun maybe_curried_binder_types T =
501 (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
503 (* typ -> term list -> term *)
504 fun mk_flat_tuple _ [t] = t
505 | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
506 HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
507 | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
508 (* int -> term -> term list *)
509 fun dest_n_tuple 1 t = [t]
510 | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
512 (* int -> typ -> typ list *)
513 fun dest_n_tuple_type 1 T = [T]
514 | dest_n_tuple_type n (Type (_, [T1, T2])) =
515 T1 :: dest_n_tuple_type (n - 1) T2
516 | dest_n_tuple_type _ T =
517 raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
520 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
521 set_def: thm option, prop_of_Rep: thm, set_name: string,
522 Abs_inverse: thm option, Rep_inverse: thm option}
524 (* theory -> string -> typedef_info *)
525 fun typedef_info thy s =
526 if is_frac_type thy (Type (s, [])) then
527 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
528 Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
529 set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
531 set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
532 else case Typedef.get_info thy s of
533 SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
535 SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
536 Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
537 set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
538 Rep_inverse = SOME Rep_inverse}
541 (* theory -> string -> bool *)
542 val is_typedef = is_some oo typedef_info
543 val is_real_datatype = is_some oo Datatype.get_info
544 (* theory -> (typ option * bool) list -> typ -> bool *)
545 fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
547 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
548 e.g., by adding a field to "Datatype_Aux.info". *)
549 (* theory -> (typ option * bool) list -> string -> bool *)
550 fun is_basic_datatype thy stds s =
551 member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
552 @{type_name int}, "Code_Numeral.code_numeral"] s orelse
553 (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
555 (* theory -> typ -> typ -> typ -> typ *)
556 fun instantiate_type thy T1 T1' T2 =
557 Same.commit (Envir.subst_type_same
558 (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
560 handle Type.TYPE_MATCH =>
561 raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
563 (* theory -> typ -> typ -> styp *)
564 fun repair_constr_type thy body_T' T =
565 instantiate_type thy (body_type T) body_T' T
567 (* string -> (string * string) list -> theory -> theory *)
568 fun register_frac_type frac_s ersaetze thy =
570 val {frac_types, codatatypes} = Data.get thy
571 val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
572 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
573 (* string -> theory -> theory *)
574 fun unregister_frac_type frac_s = register_frac_type frac_s []
576 (* typ -> string -> styp list -> theory -> theory *)
577 fun register_codatatype co_T case_name constr_xs thy =
579 val {frac_types, codatatypes} = Data.get thy
580 val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
581 val (co_s, co_Ts) = dest_Type co_T
583 if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
584 co_s <> "fun" andalso
585 not (is_basic_datatype thy [(NONE, true)] co_s) then
588 raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
589 val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
591 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
592 (* typ -> theory -> theory *)
593 fun unregister_codatatype co_T = register_codatatype co_T "" []
595 (* theory -> typ -> bool *)
596 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
597 | is_quot_type _ (Type ("FSet.fset", _)) = true
598 | is_quot_type _ _ = false
599 fun is_codatatype thy (T as Type (s, _)) =
600 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
601 |> Option.map snd |> these))
602 | is_codatatype _ _ = false
603 fun is_pure_typedef thy (T as Type (s, _)) =
604 is_typedef thy s andalso
605 not (is_real_datatype thy s orelse is_quot_type thy T orelse
606 is_codatatype thy T orelse is_record_type T orelse
607 is_integer_like_type T)
608 | is_pure_typedef _ _ = false
609 fun is_univ_typedef thy (Type (s, _)) =
610 (case typedef_info thy s of
611 SOME {set_def, prop_of_Rep, ...} =>
614 try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
616 try (fst o dest_Const o snd o HOLogic.dest_mem
617 o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
619 | is_univ_typedef _ _ = false
620 (* theory -> (typ option * bool) list -> typ -> bool *)
621 fun is_datatype thy stds (T as Type (s, _)) =
622 (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
623 is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
624 | is_datatype _ _ _ = false
626 (* theory -> typ -> (string * typ) list * (string * typ) *)
627 fun all_record_fields thy T =
628 let val (recs, more) = Record.get_extT_fields thy T in
629 recs @ more :: all_record_fields thy (snd more)
633 fun is_record_constr (x as (s, T)) =
634 String.isSuffix Record.extN s andalso
635 let val dataT = body_type T in
636 is_record_type dataT andalso
637 s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
639 (* theory -> typ -> int *)
640 val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
641 (* theory -> string -> typ -> int *)
642 fun no_of_record_field thy s T1 =
643 find_index (curry (op =) s o fst)
644 (Record.get_extT_fields thy T1 ||> single |> op @)
645 (* theory -> styp -> bool *)
646 fun is_record_get thy (s, Type ("fun", [T1, _])) =
647 exists (curry (op =) s o fst) (all_record_fields thy T1)
648 | is_record_get _ _ = false
649 fun is_record_update thy (s, T) =
650 String.isSuffix Record.updateN s andalso
651 exists (curry (op =) (unsuffix Record.updateN s) o fst)
652 (all_record_fields thy (body_type T))
653 handle TYPE _ => false
654 fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
655 (case typedef_info thy s' of
656 SOME {Abs_name, ...} => s = Abs_name
658 | is_abs_fun _ _ = false
659 fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
660 (case typedef_info thy s' of
661 SOME {Rep_name, ...} => s = Rep_name
663 | is_rep_fun _ _ = false
664 (* Proof.context -> styp -> bool *)
665 fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true
666 | is_quot_abs_fun _ ("FSet.abs_fset", _) = true
667 | is_quot_abs_fun _ _ = false
668 fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true
669 | is_quot_rep_fun _ ("FSet.rep_fset", _) = true
670 | is_quot_rep_fun _ _ = false
672 (* theory -> styp -> styp *)
673 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
674 (case typedef_info thy s' of
675 SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
676 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
677 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
678 (* theory -> typ -> typ *)
679 fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"}
680 | rep_type_for_quot_type _ (Type ("FSet.fset", [T])) =
681 Type (@{type_name list}, [T])
682 | rep_type_for_quot_type _ T =
683 raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
684 (* theory -> typ -> term *)
685 fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) =
686 Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"})
687 | equiv_relation_for_quot_type _ (Type ("FSet.fset", [T])) =
688 Const ("FSet.list_eq",
689 Type (@{type_name list}, [T]) --> Type (@{type_name list}, [T])
691 | equiv_relation_for_quot_type _ T =
692 raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
694 (* theory -> styp -> bool *)
695 fun is_coconstr thy (s, T) =
697 val {codatatypes, ...} = Data.get thy
698 val co_T = body_type T
699 val co_s = dest_Type co_T |> fst
701 exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
702 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
704 handle TYPE ("dest_Type", _, _) => false
705 fun is_constr_like thy (s, T) =
706 member (op =) [@{const_name FunBox}, @{const_name PairBox},
707 @{const_name Quot}, @{const_name Zero_Rep},
708 @{const_name Suc_Rep}] s orelse
709 let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
710 Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
711 (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
714 fun is_stale_constr thy (x as (_, T)) =
715 is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
716 not (is_coconstr thy x)
717 (* theory -> (typ option * bool) list -> styp -> bool *)
718 fun is_constr thy stds (x as (_, T)) =
719 is_constr_like thy x andalso
720 not (is_basic_datatype thy stds
721 (fst (dest_Type (unarize_type (body_type T))))) andalso
722 not (is_stale_constr thy x)
724 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
725 val is_sel_like_and_no_discr =
726 String.isPrefix sel_prefix
727 orf (member (op =) [@{const_name fst}, @{const_name snd}])
729 (* boxability -> boxability *)
730 fun in_fun_lhs_for InConstr = InSel
731 | in_fun_lhs_for _ = InFunLHS
732 fun in_fun_rhs_for InConstr = InConstr
733 | in_fun_rhs_for InSel = InSel
734 | in_fun_rhs_for InFunRHS1 = InFunRHS2
735 | in_fun_rhs_for _ = InFunRHS1
737 (* hol_context -> boxability -> typ -> bool *)
738 fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
741 (boxy = InPair orelse boxy = InFunLHS) andalso
742 not (is_boolean_type (body_type T))
744 boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
745 ((boxy = InExpr orelse boxy = InFunLHS) andalso
746 exists (is_boxing_worth_it hol_ctxt InPair)
747 (map (box_type hol_ctxt InPair) Ts))
749 (* hol_context -> boxability -> string * typ list -> string *)
750 and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
751 case triple_lookup (type_match thy) boxes (Type z) of
752 SOME (SOME box_me) => box_me
753 | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
754 (* hol_context -> boxability -> typ -> typ *)
755 and box_type hol_ctxt boxy T =
757 Type (z as ("fun", [T1, T2])) =>
758 if boxy <> InConstr andalso boxy <> InSel andalso
759 should_box_type hol_ctxt boxy z then
760 Type (@{type_name fun_box},
761 [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
763 box_type hol_ctxt (in_fun_lhs_for boxy) T1
764 --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
765 | Type (z as ("*", Ts)) =>
766 if boxy <> InConstr andalso boxy <> InSel
767 andalso should_box_type hol_ctxt boxy z then
768 Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
770 Type ("*", map (box_type hol_ctxt
771 (if boxy = InConstr orelse boxy = InSel then boxy
776 fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
777 | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
778 | binarize_nat_and_int_in_type (Type (s, Ts)) =
779 Type (s, map binarize_nat_and_int_in_type Ts)
780 | binarize_nat_and_int_in_type T = T
782 val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
785 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
788 fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
789 (* string -> int -> string *)
790 fun nth_sel_name_for_constr_name s n =
791 if s = @{const_name Pair} then
792 if n = 0 then @{const_name fst} else @{const_name snd}
795 (* styp -> int -> styp *)
796 fun nth_sel_for_constr x ~1 = discr_for_constr x
797 | nth_sel_for_constr (s, T) n =
798 (nth_sel_name_for_constr_name s n,
799 body_type T --> nth (maybe_curried_binder_types T) n)
800 (* hol_context -> bool -> styp -> int -> styp *)
801 fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
802 apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
803 oo nth_sel_for_constr
806 fun sel_no_from_name s =
807 if String.isPrefix discr_prefix s then
809 else if String.isPrefix sel_prefix s then
810 s |> unprefix sel_prefix |> Int.fromString |> the
811 else if s = @{const_name snd} then
819 (* (indexname * typ) list -> (indexname * typ) list -> term -> term *)
820 fun close_up zs zs' =
821 fold (fn (z as ((s, _), T)) => fn t' =>
822 Term.all T $ Abs (s, T, abstract_over (Var z, t')))
823 (take (length zs' - length zs) zs')
824 (* (indexname * typ) list -> term -> term *)
825 fun aux zs (@{const "==>"} $ t1 $ t2) =
826 let val zs' = Term.add_vars t1 zs in
827 close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
829 | aux zs t = close_up zs (Term.add_vars t zs) t
832 (* typ list -> term -> int -> term *)
833 fun eta_expand _ t 0 = t
834 | eta_expand Ts (Abs (s, T, t')) n =
835 Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
836 | eta_expand Ts t n =
837 fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
838 (List.take (binder_types (fastype_of1 (Ts, t)), n))
839 (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
842 fun extensionalize t =
844 (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
845 | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>
846 let val v = Var ((s, maxidx_of_term t + 1), T) in
847 extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))
851 (* typ -> term list -> term *)
852 fun distinctness_formula T =
853 all_distinct_unordered_pairs_of
854 #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
855 #> List.foldr (s_conj o swap) @{const True}
858 fun zero_const T = Const (@{const_name zero_class.zero}, T)
859 fun suc_const T = Const (@{const_name Suc}, T --> T)
861 (* hol_context -> typ -> styp list *)
862 fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
863 (T as Type (s, Ts)) =
864 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
865 SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
867 if is_datatype thy stds T then
868 case Datatype.get_info thy s of
869 SOME {index, descr, ...} =>
871 val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
874 (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
878 if is_record_type T then
880 val s' = unsuffix Record.ext_typeN s ^ Record.extN
881 val T' = (Record.get_extT_fields thy T
882 |> apsnd single |> uncurry append |> map snd) ---> T
884 else if is_quot_type thy T then
885 [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
886 else case typedef_info thy s of
887 SOME {abs_type, rep_type, Abs_name, ...} =>
888 [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
890 if T = @{typ ind} then
891 [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
896 | uncached_datatype_constrs _ _ = []
897 (* hol_context -> typ -> styp list *)
898 fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
899 case AList.lookup (op =) (!constr_cache) T of
902 let val xs = uncached_datatype_constrs hol_ctxt T in
903 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
905 (* hol_context -> bool -> typ -> styp list *)
906 fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
907 map (apsnd ((binarize ? binarize_nat_and_int_in_type)
908 o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
909 (* hol_context -> typ -> int *)
910 val num_datatype_constrs = length oo datatype_constrs
912 (* string -> string *)
913 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
914 | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
915 | constr_name_for_sel_like s' = original_name s'
916 (* hol_context -> bool -> styp -> styp *)
917 fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
918 let val s = constr_name_for_sel_like s' in
920 (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
925 (* hol_context -> styp -> term *)
926 fun discr_term_for_constr hol_ctxt (x as (s, T)) =
927 let val dataT = body_type T in
928 if s = @{const_name Suc} then
930 @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
931 else if num_datatype_constrs hol_ctxt dataT >= 2 then
932 Const (discr_for_constr x)
934 Abs (Name.uu, dataT, @{const True})
936 (* hol_context -> styp -> term -> term *)
937 fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t =
940 if x = x' then @{const True}
941 else if is_constr_like thy x' then @{const False}
942 else betapply (discr_term_for_constr hol_ctxt x, t)
943 | _ => betapply (discr_term_for_constr hol_ctxt x, t)
945 (* theory -> (typ option * bool) list -> styp -> term -> term *)
946 fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
947 let val (arg_Ts, dataT) = strip_type T in
948 if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
949 @{term "%n::nat. n - 1"}
950 else if is_pair_type dataT then
951 Const (nth_sel_for_constr x n)
954 (* int -> typ -> int * term *)
955 fun aux m (Type ("*", [T1, T2])) =
957 val (m, t1) = aux m T1
958 val (m, t2) = aux m T2
959 in (m, HOLogic.mk_prod (t1, t2)) end
961 (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
963 val m = fold (Integer.add o num_factors_in_type)
964 (List.take (arg_Ts, n)) 0
965 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
967 (* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *)
968 fun select_nth_constr_arg thy stds x t n res_T =
969 (case strip_comb t of
971 if x = x' then nth args n
972 else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
975 handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
977 (* theory -> (typ option * bool) list -> styp -> term list -> term *)
978 fun construct_value _ _ x [] = Const x
979 | construct_value thy stds (x as (s, _)) args =
980 let val args = map Envir.eta_contract args in
982 Const (x' as (s', _)) $ t =>
983 if is_sel_like_and_no_discr s' andalso
984 constr_name_for_sel_like s' = s andalso
985 forall (fn (n, t') =>
986 select_nth_constr_arg thy stds x t n dummyT = t')
987 (index_seq 0 (length args) ~~ args) then
990 list_comb (Const x, args)
991 | _ => list_comb (Const x, args)
994 (* (typ * int) list -> typ -> int *)
995 fun card_of_type assigns (Type ("fun", [T1, T2])) =
996 reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
997 | card_of_type assigns (Type ("*", [T1, T2])) =
998 card_of_type assigns T1 * card_of_type assigns T2
999 | card_of_type _ (Type (@{type_name itself}, _)) = 1
1000 | card_of_type _ @{typ prop} = 2
1001 | card_of_type _ @{typ bool} = 2
1002 | card_of_type _ @{typ unit} = 1
1003 | card_of_type assigns T =
1004 case AList.lookup (op =) assigns T of
1006 | NONE => if T = @{typ bisim_iterator} then 0
1007 else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
1008 (* int -> (typ * int) list -> typ -> int *)
1009 fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
1011 val k1 = bounded_card_of_type max default_card assigns T1
1012 val k2 = bounded_card_of_type max default_card assigns T2
1014 if k1 = max orelse k2 = max then max
1015 else Int.min (max, reasonable_power k2 k1)
1017 | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
1019 val k1 = bounded_card_of_type max default_card assigns T1
1020 val k2 = bounded_card_of_type max default_card assigns T2
1021 in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
1022 | bounded_card_of_type max default_card assigns T =
1023 Int.min (max, if default_card = ~1 then
1024 card_of_type assigns T
1026 card_of_type assigns T
1027 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
1029 (* hol_context -> int -> (typ * int) list -> typ -> int *)
1030 fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
1032 (* typ list -> typ -> int *)
1034 (if member (op =) avoid T then
1037 Type ("fun", [T1, T2]) =>
1039 val k1 = aux avoid T1
1040 val k2 = aux avoid T2
1042 if k1 = 0 orelse k2 = 0 then 0
1043 else if k1 >= max orelse k2 >= max then max
1044 else Int.min (max, reasonable_power k2 k1)
1046 | Type ("*", [T1, T2]) =>
1048 val k1 = aux avoid T1
1049 val k2 = aux avoid T2
1051 if k1 = 0 orelse k2 = 0 then 0
1052 else if k1 >= max orelse k2 >= max then max
1053 else Int.min (max, k1 * k2)
1055 | Type (@{type_name itself}, _) => 1
1060 (case datatype_constrs hol_ctxt T of
1061 [] => if is_integer_type T orelse is_bit_type T then 0
1066 datatype_constrs hol_ctxt T
1067 |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
1070 if exists (curry (op =) 0) constr_cards then 0
1071 else Integer.sum constr_cards
1073 | _ => raise SAME ())
1075 AList.lookup (op =) assigns T |> the_default default_card
1076 in Int.min (max, aux [] T) end
1078 (* hol_context -> typ -> bool *)
1079 fun is_finite_type hol_ctxt =
1080 not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
1083 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
1084 | is_ground_term (Const _) = true
1085 | is_ground_term _ = false
1087 (* term -> word -> word *)
1088 fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
1089 | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
1090 | hashw_term _ = 0w0
1092 val hash_term = Word.toInt o hashw_term
1094 (* term list -> (indexname * typ) list *)
1095 fun special_bounds ts =
1096 fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
1098 (* indexname * typ -> term -> term *)
1099 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
1101 (* theory -> string -> bool *)
1102 fun is_funky_typedef_name thy s =
1103 member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
1104 @{type_name int}] s orelse
1105 is_frac_type thy (Type (s, []))
1106 (* theory -> typ -> bool *)
1107 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
1108 | is_funky_typedef _ _ = false
1110 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
1111 $ Const (@{const_name TYPE}, _)) = true
1112 | is_arity_type_axiom _ = false
1113 (* theory -> bool -> term -> bool *)
1114 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
1115 is_typedef_axiom thy boring t2
1116 | is_typedef_axiom thy boring
1117 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
1118 $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
1119 boring <> is_funky_typedef_name thy s andalso is_typedef thy s
1120 | is_typedef_axiom _ _ _ = false
1122 (* Distinguishes between (1) constant definition axioms, (2) type arity and
1123 typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
1124 Typedef axioms are uninteresting to Nitpick, because it can retrieve them
1125 using "typedef_info". *)
1126 (* theory -> (string * term) list -> string list -> term list * term list *)
1127 fun partition_axioms_by_definitionality thy axioms def_names =
1129 val axioms = sort (fast_string_ord o pairself fst) axioms
1130 val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
1132 OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
1133 |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
1134 in pairself (map snd) (defs, nondefs) end
1136 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
1137 will do as long as it contains all the "axioms" and "axiomatization"
1139 (* theory -> bool *)
1140 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
1143 val is_plain_definition =
1147 case strip_comb t1 of
1149 forall is_Var args andalso not (has_duplicates (op =) args)
1151 fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
1152 | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
1157 (* theory -> term list * term list * term list *)
1158 fun all_axioms_of thy =
1160 (* theory list -> term list *)
1161 val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
1162 val specs = Defs.all_specifications_of (Theory.defs_of thy)
1163 val def_names = specs |> maps snd |> map_filter #def
1164 |> OrdList.make fast_string_ord
1165 val thys = thy :: Theory.ancestors_of thy
1166 val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
1167 val built_in_axioms = axioms_of_thys built_in_thys
1168 val user_axioms = axioms_of_thys user_thys
1169 val (built_in_defs, built_in_nondefs) =
1170 partition_axioms_by_definitionality thy built_in_axioms def_names
1171 ||> filter (is_typedef_axiom thy false)
1172 val (user_defs, user_nondefs) =
1173 partition_axioms_by_definitionality thy user_axioms def_names
1174 val (built_in_nondefs, user_nondefs) =
1175 List.partition (is_typedef_axiom thy false) user_nondefs
1176 |>> append built_in_nondefs
1178 (thy |> PureThy.all_thms_of
1179 |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
1180 |> map (prop_of o snd) |> filter is_plain_definition) @
1181 user_defs @ built_in_defs
1182 in (defs, built_in_nondefs, user_nondefs) end
1184 (* theory -> (typ option * bool) list -> bool -> styp -> int option *)
1185 fun arity_of_built_in_const thy stds fast_descrs (s, T) =
1186 if s = @{const_name If} then
1187 if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
1189 let val std_nats = is_standard_datatype thy stds nat_T in
1190 case AList.lookup (op =)
1192 |> std_nats ? append built_in_nat_consts
1193 |> fast_descrs ? append built_in_descr_consts) s of
1196 case AList.lookup (op =)
1197 (built_in_typed_consts
1198 |> std_nats ? append built_in_typed_nat_consts)
1199 (s, unarize_type T) of
1202 if is_fun_type T andalso is_set_type (domain_type T) then
1203 AList.lookup (op =) built_in_set_consts s
1207 (* theory -> (typ option * bool) list -> bool -> styp -> bool *)
1208 val is_built_in_const = is_some oooo arity_of_built_in_const
1210 (* This function is designed to work for both real definition axioms and
1211 simplification rules (equational specifications). *)
1213 fun term_under_def t =
1215 @{const "==>"} $ _ $ t2 => term_under_def t2
1216 | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
1217 | @{const Trueprop} $ t1 => term_under_def t1
1218 | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
1219 | Abs (_, _, t') => term_under_def t'
1220 | t1 $ _ => term_under_def t1
1223 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
1224 traversal of the term, without which the wrong occurrence of a constant could
1225 be matched in the face of overloading. *)
1226 (* theory -> (typ option * bool) list -> bool -> const_table -> styp
1228 fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
1229 if is_built_in_const thy stds fast_descrs x then
1232 these (Symtab.lookup table s)
1233 |> map_filter (try (Refute.specialize_type thy x))
1234 |> filter (curry (op =) (Const x) o term_under_def)
1236 (* theory -> term -> term option *)
1237 fun normalized_rhs_of thy t =
1239 (* term option -> term option *)
1240 fun aux (v as Var _) (SOME t) = SOME (lambda v t)
1241 | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
1245 Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
1246 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
1248 | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
1249 val args = strip_comb lhs |> snd
1250 in fold_rev aux args (SOME rhs) end
1252 (* theory -> const_table -> styp -> term option *)
1253 fun def_of_const thy table (x as (s, _)) =
1254 if is_built_in_const thy [(NONE, false)] false x orelse
1255 original_name s <> s then
1258 x |> def_props_for_const thy [(NONE, false)] false table |> List.last
1259 |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
1260 handle List.Empty => NONE
1262 (* term -> fixpoint_kind *)
1263 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
1264 | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
1265 | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
1266 | fixpoint_kind_of_rhs _ = NoFp
1268 (* theory -> const_table -> term -> bool *)
1269 fun is_mutually_inductive_pred_def thy table t =
1272 fun is_good_arg (Bound _) = true
1273 | is_good_arg (Const (s, _)) =
1274 s = @{const_name True} orelse s = @{const_name False} orelse
1275 s = @{const_name undefined}
1276 | is_good_arg _ = false
1278 case t |> strip_abs_body |> strip_comb of
1279 (Const x, ts as (_ :: _)) =>
1280 (case def_of_const thy table x of
1281 SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
1285 (* theory -> const_table -> term -> term *)
1286 fun unfold_mutually_inductive_preds thy table =
1287 map_aterms (fn t as Const x =>
1288 (case def_of_const thy table x of
1290 let val t' = Envir.eta_contract t' in
1291 if is_mutually_inductive_pred_def thy table t' then t'
1297 (* term -> string * term *)
1298 fun pair_for_prop t =
1299 case term_under_def t of
1300 Const (s, _) => (s, t)
1301 | Free _ => raise NOT_SUPPORTED "local definitions"
1302 | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
1304 (* (Proof.context -> term list) -> Proof.context -> const_table *)
1305 fun table_for get ctxt =
1306 get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
1308 (* theory -> (typ option * bool) list -> (string * int) list *)
1309 fun case_const_names thy stds =
1310 Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
1311 if is_basic_datatype thy stds dtype_s then
1314 cons (case_name, AList.lookup (op =) descr index
1315 |> the |> #3 |> length))
1316 (Datatype.get_all thy) [] @
1317 map (apsnd length o snd) (#codatatypes (Data.get thy))
1319 (* Proof.context -> term list -> const_table *)
1320 fun const_def_table ctxt ts =
1321 table_for (map prop_of o Nitpick_Defs.get) ctxt
1322 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
1323 (map pair_for_prop ts)
1324 (* term list -> const_table *)
1325 fun const_nondef_table ts =
1326 fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
1327 |> AList.group (op =) |> Symtab.make
1328 (* Proof.context -> const_table *)
1329 val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
1330 val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
1331 (* Proof.context -> const_table -> const_table *)
1332 fun inductive_intro_table ctxt def_table =
1333 table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
1334 def_table o prop_of)
1335 o Nitpick_Intros.get) ctxt
1336 (* theory -> term list Inttab.table *)
1337 fun ground_theorem_table thy =
1338 fold ((fn @{const Trueprop} $ t1 =>
1339 is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
1340 | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
1342 val basic_ersatz_table =
1343 [(@{const_name prod_case}, @{const_name split}),
1344 (@{const_name card}, @{const_name card'}),
1345 (@{const_name setsum}, @{const_name setsum'}),
1346 (@{const_name fold_graph}, @{const_name fold_graph'}),
1347 (@{const_name wf}, @{const_name wf'}),
1348 (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
1349 (@{const_name wfrec}, @{const_name wfrec'})]
1351 (* theory -> (string * string) list *)
1352 fun ersatz_table thy =
1353 fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
1355 (* const_table Unsynchronized.ref -> string -> term list -> unit *)
1356 fun add_simps simp_table s eqs =
1357 Unsynchronized.change simp_table
1358 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
1360 (* theory -> styp -> term list *)
1361 fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
1362 let val abs_T = domain_type T in
1363 typedef_info thy (fst (dest_Type abs_T)) |> the
1364 |> pairf #Abs_inverse #Rep_inverse
1365 |> pairself (Refute.specialize_type thy x o prop_of o the)
1368 (* theory -> string * typ list -> term list *)
1369 fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
1370 let val abs_T = Type abs_z in
1371 if is_univ_typedef thy abs_T then
1373 else case typedef_info thy abs_s of
1374 SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,
1377 val rep_T = instantiate_type thy abs_type abs_T rep_type
1378 val rep_t = Const (Rep_name, abs_T --> rep_T)
1379 val set_t = Const (set_name, rep_T --> bool_T)
1381 prop_of_Rep |> HOLogic.dest_Trueprop
1382 |> Refute.specialize_type thy (dest_Const rep_t)
1383 |> HOLogic.dest_mem |> snd
1385 [HOLogic.all_const abs_T
1386 $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
1387 |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
1388 |> map HOLogic.mk_Trueprop
1392 fun optimized_quot_type_axioms thy stds abs_z =
1394 val abs_T = Type abs_z
1395 val rep_T = rep_type_for_quot_type thy abs_T
1396 val equiv_rel = equiv_relation_for_quot_type thy abs_T
1397 val a_var = Var (("a", 0), abs_T)
1398 val x_var = Var (("x", 0), rep_T)
1399 val y_var = Var (("y", 0), rep_T)
1400 val x = (@{const_name Quot}, rep_T --> abs_T)
1401 val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
1402 val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
1403 val normal_x = normal_t $ x_var
1404 val normal_y = normal_t $ y_var
1405 val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
1407 [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t),
1409 ([@{const Not} $ (is_unknown_t $ normal_x),
1410 @{const Not} $ (is_unknown_t $ normal_y),
1411 equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
1412 Logic.mk_equals (normal_x, normal_y)),
1414 $ (HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)))
1415 $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
1418 (* theory -> (typ option * bool) list -> int * styp -> term *)
1419 fun constr_case_body thy stds (j, (x as (_, T))) =
1420 let val arg_Ts = binder_types T in
1421 list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
1422 (index_seq 0 (length arg_Ts)) arg_Ts)
1424 (* hol_context -> typ -> int * styp -> term -> term *)
1425 fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
1426 Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
1427 $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
1429 (* hol_context -> typ -> typ -> term *)
1430 fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
1432 val xs = datatype_constrs hol_ctxt dataT
1433 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
1434 val (xs', x) = split_last xs
1436 constr_case_body thy stds (1, x)
1437 |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
1438 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
1441 (* hol_context -> string -> typ -> typ -> term -> term *)
1442 fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
1443 let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
1444 case no_of_record_field thy s rec_T of
1445 ~1 => (case rec_T of
1446 Type (_, Ts as _ :: _) =>
1448 val rec_T' = List.last Ts
1449 val j = num_record_fields thy rec_T - 1
1451 select_nth_constr_arg thy stds constr_x t j res_T
1452 |> optimized_record_get hol_ctxt s rec_T' res_T
1454 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
1456 | j => select_nth_constr_arg thy stds constr_x t j res_T
1458 (* hol_context -> string -> typ -> term -> term -> term *)
1459 fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
1461 val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
1462 val Ts = binder_types constr_T
1464 val special_j = no_of_record_field thy s rec_T
1466 map2 (fn j => fn T =>
1467 let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
1468 if j = special_j then
1470 else if j = n - 1 andalso special_j = ~1 then
1471 optimized_record_update hol_ctxt s
1472 (rec_T |> dest_Type |> snd |> List.last) fun_t t
1475 end) (index_seq 0 n) Ts
1476 in list_comb (Const constr_x, ts) end
1478 (* theory -> const_table -> string * typ -> fixpoint_kind *)
1479 fun fixpoint_kind_of_const thy table x =
1480 if is_built_in_const thy [(NONE, false)] false x then
1483 fixpoint_kind_of_rhs (the (def_of_const thy table x))
1484 handle Option.Option => NoFp
1486 (* hol_context -> styp -> bool *)
1487 fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
1488 ...} : hol_context) x =
1489 fixpoint_kind_of_const thy def_table x <> NoFp andalso
1490 not (null (def_props_for_const thy stds fast_descrs intro_table x))
1491 fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
1492 ...} : hol_context) x =
1493 exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
1495 [!simp_table, psimp_table]
1496 fun is_inductive_pred hol_ctxt =
1497 is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
1498 fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
1499 (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
1500 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
1502 (* term * term -> term *)
1503 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
1504 | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
1505 | s_betapply p = betapply p
1506 (* term * term list -> term *)
1507 val s_betapplys = Library.foldl s_betapply
1510 fun lhs_of_equation t =
1512 Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1513 | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
1514 | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
1515 | @{const Trueprop} $ t1 => lhs_of_equation t1
1516 | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1517 | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
1518 | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
1520 (* theory -> term -> bool *)
1521 fun is_constr_pattern _ (Bound _) = true
1522 | is_constr_pattern _ (Var _) = true
1523 | is_constr_pattern thy t =
1524 case strip_comb t of
1525 (Const (x as (s, _)), args) =>
1526 is_constr_like thy x andalso forall (is_constr_pattern thy) args
1528 fun is_constr_pattern_lhs thy t =
1529 forall (is_constr_pattern thy) (snd (strip_comb t))
1530 fun is_constr_pattern_formula thy t =
1531 case lhs_of_equation t of
1532 SOME t' => is_constr_pattern_lhs thy t'
1535 (* Prevents divergence in case of cyclic or infinite definition dependencies. *)
1536 val unfold_max_depth = 255
1538 (* hol_context -> term -> term *)
1539 fun unfold_defs_in_term (hol_ctxt as {thy, stds, destroy_constrs, fast_descrs,
1540 case_names, def_table, ground_thm_table,
1541 ersatz_table, ...}) =
1543 (* int -> typ list -> term -> term *)
1544 fun do_term depth Ts t =
1546 (t0 as Const (@{const_name Int.number_class.number_of},
1547 Type ("fun", [_, ran_T]))) $ t1 =>
1548 ((if is_number_type thy ran_T then
1550 val j = t1 |> HOLogic.dest_numeral
1551 |> ran_T = nat_T ? Integer.max 0
1552 val s = numeral_prefix ^ signed_string_of_int j
1554 if is_integer_like_type ran_T then
1555 if is_standard_datatype thy stds ran_T then
1558 funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
1560 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
1563 handle TERM _ => raise SAME ()
1566 handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
1567 | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
1568 do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
1569 | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
1570 $ (t2 as Abs (_, _, t2')) =>
1571 betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
1572 map (do_term depth Ts) [t1, t2])
1573 | Const (x as (@{const_name distinct},
1574 Type ("fun", [Type (@{type_name list}, [T']), _])))
1576 (t1 |> HOLogic.dest_list |> distinctness_formula T'
1577 handle TERM _ => do_const depth Ts t x [t1])
1578 | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
1579 if is_ground_term t1 andalso
1580 exists (Pattern.matches thy o rpair t1)
1581 (Inttab.lookup_list ground_thm_table (hash_term t1)) then
1584 do_const depth Ts t x [t1, t2, t3]
1585 | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
1586 | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
1587 | Const x $ t1 => do_const depth Ts t x [t1]
1588 | Const x => do_const depth Ts t x []
1589 | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
1593 | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
1594 (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
1595 and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
1596 (Abs (Name.uu, body_type T,
1597 select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
1598 | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
1599 (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
1600 (* int -> typ list -> term -> styp -> term list -> term *)
1601 and do_const depth Ts t (x as (s, T)) ts =
1602 case AList.lookup (op =) ersatz_table s of
1604 do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
1608 if is_built_in_const thy stds fast_descrs x then
1610 else case AList.lookup (op =) case_names s of
1613 val (dataT, res_T) = nth_range_type n T
1614 |> pairf domain_type range_type
1616 (optimized_case_def hol_ctxt dataT res_T
1617 |> do_term (depth + 1) Ts, ts)
1620 if is_constr thy stds x then
1622 else if is_stale_constr thy x then
1623 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
1625 else if is_quot_abs_fun thy x then
1627 val rep_T = domain_type T
1628 val abs_T = range_type T
1630 (Abs (Name.uu, rep_T,
1631 Const (@{const_name Quot}, rep_T --> abs_T)
1632 $ (Const (@{const_name quot_normal},
1633 rep_T --> rep_T) $ Bound 0)), ts)
1635 else if is_quot_rep_fun thy x then
1637 val abs_T = domain_type T
1638 val rep_T = range_type T
1639 val x' = (@{const_name Quot}, rep_T --> abs_T)
1640 in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end
1641 else if is_record_get thy x then
1643 0 => (do_term depth Ts (eta_expand Ts t 1), [])
1644 | _ => (optimized_record_get hol_ctxt s (domain_type T)
1645 (range_type T) (do_term depth Ts (hd ts)), tl ts)
1646 else if is_record_update thy x then
1648 2 => (optimized_record_update hol_ctxt
1649 (unsuffix Record.updateN s) (nth_range_type 2 T)
1650 (do_term depth Ts (hd ts))
1651 (do_term depth Ts (nth ts 1)), [])
1652 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
1653 else if is_rep_fun thy x then
1654 let val x' = mate_of_rep_fun thy x in
1655 if is_constr thy stds x' then
1656 select_nth_constr_arg_with_args depth Ts x' ts 0
1661 else if is_equational_fun hol_ctxt x then
1663 else case def_of_const thy def_table x of
1665 if depth > unfold_max_depth then
1666 raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
1667 "too many nested definitions (" ^
1668 string_of_int depth ^ ") while expanding " ^
1670 else if s = @{const_name wfrec'} then
1671 (do_term (depth + 1) Ts (betapplys (def, ts)), [])
1673 (do_term (depth + 1) Ts def, ts)
1674 | NONE => (Const x, ts)
1675 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
1678 (* hol_context -> typ -> term list *)
1679 fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
1681 val xs = datatype_constrs hol_ctxt T
1682 val set_T = T --> bool_T
1683 val iter_T = @{typ bisim_iterator}
1684 val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
1685 val bisim_max = @{const bisim_iterator_max}
1686 val n_var = Var (("n", 0), iter_T)
1688 Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T)
1689 $ Abs ("m", iter_T, HOLogic.eq_const iter_T
1690 $ (suc_const iter_T $ Bound 0) $ n_var)
1691 val x_var = Var (("x", 0), T)
1692 val y_var = Var (("y", 0), T)
1693 (* styp -> int -> typ -> term *)
1694 fun nth_sub_bisim x n nth_T =
1695 (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
1696 else HOLogic.eq_const nth_T)
1697 $ select_nth_constr_arg thy stds x x_var n nth_T
1698 $ select_nth_constr_arg thy stds x y_var n nth_T
1700 fun case_func (x as (_, T)) =
1702 val arg_Ts = binder_types T
1704 discriminate_value hol_ctxt x y_var ::
1705 map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
1707 in List.foldr absdummy core_t arg_Ts end
1709 [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
1710 $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
1711 $ (betapplys (optimized_case_def hol_ctxt T bool_T,
1712 map case_func xs @ [x_var]))),
1713 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
1714 $ (Const (@{const_name insert}, T --> set_T --> set_T)
1715 $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
1716 |> map HOLogic.mk_Trueprop
1719 exception NO_TRIPLE of unit
1721 (* theory -> styp -> term -> term list * term list * term *)
1722 fun triple_for_intro_rule thy x t =
1724 val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
1725 val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
1726 val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
1728 val is_good_head = curry (op =) (Const x) o head_of
1730 if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
1734 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
1736 (* indexname * typ -> term list -> term -> term -> term *)
1737 fun wf_constraint_for rel side concl main =
1739 val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
1740 tuple_for_args concl), Var rel)
1741 val t = List.foldl HOLogic.mk_imp core side
1742 val vars = filter (not_equal rel) (Term.add_vars t [])
1744 Library.foldl (fn (t', ((x, j), T)) =>
1746 $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
1750 (* indexname * typ -> term list * term list * term -> term *)
1751 fun wf_constraint_for_triple rel (side, main, concl) =
1752 map (wf_constraint_for rel side concl) main |> foldr1 s_conj
1754 (* Proof.context -> Time.time option -> thm
1755 -> (Proof.context -> tactic -> tactic) -> bool *)
1756 fun terminates_by ctxt timeout goal tac =
1757 can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
1758 #> SINGLE (DETERM_TIMEOUT timeout
1759 (tac ctxt (auto_tac (clasimpset_of ctxt))))
1760 #> the #> Goal.finish ctxt) goal
1762 val max_cached_wfs = 50
1763 val cached_timeout =
1764 Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
1765 val cached_wf_props =
1766 Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
1768 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
1769 ScnpReconstruct.sizechange_tac]
1771 (* hol_context -> const_table -> styp -> bool *)
1772 fun uncached_is_well_founded_inductive_pred
1773 ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
1774 : hol_context) (x as (_, T)) =
1775 case def_props_for_const thy stds fast_descrs intro_table x of
1776 [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
1779 (case map (triple_for_intro_rule thy x) intro_ts
1780 |> filter_out (null o #2) of
1784 val binders_T = HOLogic.mk_tupleT (binder_types T)
1785 val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
1786 val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
1787 val rel = (("R", j), rel_T)
1788 val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
1789 map (wf_constraint_for_triple rel) triples
1790 |> foldr1 s_conj |> HOLogic.mk_Trueprop
1791 val _ = if debug then
1792 priority ("Wellfoundedness goal: " ^
1793 Syntax.string_of_term ctxt prop ^ ".")
1797 if tac_timeout = Synchronized.value cached_timeout andalso
1798 length (Synchronized.value cached_wf_props) < max_cached_wfs then
1801 (Synchronized.change cached_wf_props (K []);
1802 Synchronized.change cached_timeout (K tac_timeout));
1803 case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
1807 val goal = prop |> cterm_of thy |> Goal.init
1808 val wf = exists (terminates_by ctxt tac_timeout goal)
1810 in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
1812 handle List.Empty => false
1813 | NO_TRIPLE () => false
1815 (* The type constraint below is a workaround for a Poly/ML crash. *)
1817 (* hol_context -> styp -> bool *)
1818 fun is_well_founded_inductive_pred
1819 (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
1821 case triple_lookup (const_match thy) wfs x of
1823 | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
1824 case AList.lookup (op =) (!wf_cache) x of
1828 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
1829 val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
1831 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
1834 (* typ list -> typ -> typ -> term -> term *)
1835 fun ap_curry [_] _ _ t = t
1836 | ap_curry arg_Ts tuple_T body_T t =
1837 let val n = length arg_Ts in
1838 list_abs (map (pair "c") arg_Ts,
1840 $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
1843 (* int -> term -> int *)
1844 fun num_occs_of_bound_in_term j (t1 $ t2) =
1845 op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
1846 | num_occs_of_bound_in_term j (Abs (s, T, t')) =
1847 num_occs_of_bound_in_term (j + 1) t'
1848 | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
1849 | num_occs_of_bound_in_term _ _ = 0
1852 val is_linear_inductive_pred_def =
1854 (* int -> term -> bool *)
1855 fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
1856 do_disjunct (j + 1) t2
1858 case num_occs_of_bound_in_term j t of
1860 | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
1863 fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
1864 let val (xs, body) = strip_abs t2 in
1867 | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
1869 | do_lfp_def _ = false
1870 in do_lfp_def o strip_abs_body end
1872 (* int -> int list list *)
1873 fun n_ptuple_paths 0 = []
1874 | n_ptuple_paths 1 = []
1875 | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
1876 (* int -> typ -> typ -> term -> term *)
1877 val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
1879 (* term -> term * term *)
1880 val linear_pred_base_and_step_rhss =
1883 fun aux (Const (@{const_name lfp}, _) $ t2) =
1885 val (xs, body) = strip_abs t2
1886 val arg_Ts = map snd (tl xs)
1887 val tuple_T = HOLogic.mk_tupleT arg_Ts
1888 val j = length arg_Ts
1889 (* int -> term -> term *)
1890 fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
1891 Const (@{const_name Ex}, T1)
1892 $ Abs (s2, T2, repair_rec (j + 1) t2')
1893 | repair_rec j (@{const "op &"} $ t1 $ t2) =
1894 @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
1896 let val (head, args) = strip_comb t in
1897 if head = Bound j then
1898 HOLogic.eq_const tuple_T $ Bound j
1899 $ mk_flat_tuple tuple_T args
1903 val (nonrecs, recs) =
1904 List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
1906 val base_body = nonrecs |> List.foldl s_disj @{const False}
1907 val step_body = recs |> map (repair_rec j)
1908 |> List.foldl s_disj @{const False}
1910 (list_abs (tl xs, incr_bv (~1, j, base_body))
1911 |> ap_n_split (length arg_Ts) tuple_T bool_T,
1912 Abs ("y", tuple_T, list_abs (tl xs, step_body)
1913 |> ap_n_split (length arg_Ts) tuple_T bool_T))
1916 raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
1919 (* hol_context -> styp -> term -> term *)
1920 fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T))
1923 val j = maxidx_of_term def + 1
1924 val (outer, fp_app) = strip_abs def
1925 val outer_bounds = map Bound (length outer - 1 downto 0)
1926 val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer
1927 val fp_app = subst_bounds (rev outer_vars, fp_app)
1928 val (outer_Ts, rest_T) = strip_n_binders (length outer) T
1929 val tuple_arg_Ts = strip_type rest_T |> fst
1930 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
1931 val set_T = tuple_T --> bool_T
1932 val curried_T = tuple_T --> set_T
1933 val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
1934 val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
1935 val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
1936 val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
1937 |> HOLogic.mk_Trueprop
1938 val _ = add_simps simp_table base_s [base_eq]
1939 val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T)
1940 val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs)
1941 |> HOLogic.mk_Trueprop
1942 val _ = add_simps simp_table step_s [step_eq]
1945 Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
1946 $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
1947 $ (Const (@{const_name split}, curried_T --> uncurried_T)
1948 $ list_comb (Const step_x, outer_bounds)))
1949 $ list_comb (Const base_x, outer_bounds)
1950 |> ap_curry tuple_arg_Ts tuple_T bool_T)
1951 |> unfold_defs_in_term hol_ctxt
1954 (* hol_context -> bool -> styp -> term *)
1955 fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
1956 def_table, simp_table, ...})
1959 val iter_T = iterator_type_for_const gfp x
1960 val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
1961 val unrolled_const = Const x' $ zero_const iter_T
1962 val def = the (def_of_const thy def_table x)
1964 if is_equational_fun hol_ctxt x' then
1965 unrolled_const (* already done *)
1966 else if not gfp andalso is_linear_inductive_pred_def def andalso
1967 star_linear_preds then
1968 starred_linear_pred_const hol_ctxt x def
1971 val j = maxidx_of_term def + 1
1972 val (outer, fp_app) = strip_abs def
1973 val outer_bounds = map Bound (length outer - 1 downto 0)
1974 val cur = Var ((iter_var_prefix, j + 1), iter_T)
1975 val next = suc_const iter_T $ cur
1976 val rhs = case fp_app of
1978 betapply (t, list_comb (Const x', next :: outer_bounds))
1979 | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
1981 val (inner, naked_rhs) = strip_abs rhs
1982 val all = outer @ inner
1983 val bounds = map Bound (length all - 1 downto 0)
1984 val vars = map (fn (s, T) => Var ((s, j), T)) all
1985 val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs)
1986 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
1987 val _ = add_simps simp_table s' [eq]
1988 in unrolled_const end
1991 (* hol_context -> styp -> term *)
1992 fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
1994 val def = the (def_of_const thy def_table x)
1995 val (outer, fp_app) = strip_abs def
1996 val outer_bounds = map Bound (length outer - 1 downto 0)
1997 val rhs = case fp_app of
1998 Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
1999 | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
2001 val (inner, naked_rhs) = strip_abs rhs
2002 val all = outer @ inner
2003 val bounds = map Bound (length all - 1 downto 0)
2004 val j = maxidx_of_term def + 1
2005 val vars = map (fn (s, T) => Var ((s, j), T)) all
2007 HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
2008 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
2010 fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
2011 if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
2012 let val x' = (after_name_sep s, T) in
2013 raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
2016 raw_inductive_pred_axiom hol_ctxt x
2018 (* hol_context -> styp -> term list *)
2019 fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
2020 psimp_table, ...}) (x as (s, _)) =
2021 case def_props_for_const thy stds fast_descrs (!simp_table) x of
2022 [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
2023 [] => [inductive_pred_axiom hol_ctxt x]
2026 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
2027 (* hol_context -> styp -> bool *)
2028 fun is_equational_fun_surely_complete hol_ctxt x =
2029 case raw_equational_fun_axioms hol_ctxt x of
2030 [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
2031 strip_comb t1 |> snd |> forall is_Var
2034 (* term list -> term list *)
2035 fun merge_type_vars_in_terms ts =
2037 (* typ -> (sort * string) list -> (sort * string) list *)
2038 fun add_type (TFree (s, S)) table =
2039 (case AList.lookup (op =) table S of
2041 if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
2043 | NONE => (S, s) :: table)
2044 | add_type _ table = table
2045 val table = fold (fold_types (fold_atyps add_type)) ts []
2047 fun coalesce (TFree (s, S)) = TFree (AList.lookup (op =) table S |> the, S)
2049 in map (map_types (map_atyps coalesce)) ts end
2051 (* hol_context -> bool -> typ -> typ list -> typ list *)
2052 fun add_ground_types hol_ctxt binarize =
2056 Type ("fun", Ts) => fold aux Ts accum
2057 | Type ("*", Ts) => fold aux Ts accum
2058 | Type (@{type_name itself}, [T1]) => aux T1 accum
2060 if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
2065 |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
2069 | _ => insert (op =) T accum
2072 (* hol_context -> bool -> typ -> typ list *)
2073 fun ground_types_in_type hol_ctxt binarize T =
2074 add_ground_types hol_ctxt binarize T []
2075 (* hol_context -> term list -> typ list *)
2076 fun ground_types_in_terms hol_ctxt binarize ts =
2077 fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
2079 (* theory -> const_table -> styp -> int list *)
2080 fun const_format thy def_table (x as (s, T)) =
2081 if String.isPrefix unrolled_prefix s then
2082 const_format thy def_table (original_name s, range_type T)
2083 else if String.isPrefix skolem_prefix s then
2085 val k = unprefix skolem_prefix s
2086 |> strip_first_name_sep |> fst |> space_explode "@"
2087 |> hd |> Int.fromString |> the
2088 in [k, num_binder_types T - k] end
2089 else if original_name s <> s then
2090 [num_binder_types T]
2091 else case def_of_const thy def_table x of
2092 SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
2093 let val k = length (strip_abs_vars t') in
2094 [k, num_binder_types T - k]
2097 [num_binder_types T]
2098 | NONE => [num_binder_types T]
2099 (* int list -> int list -> int list *)
2100 fun intersect_formats _ [] = []
2101 | intersect_formats [] _ = []
2102 | intersect_formats ks1 ks2 =
2103 let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
2104 intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
2105 (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
2109 (* theory -> const_table -> (term option * int list) list -> term -> int list *)
2110 fun lookup_format thy def_table formats t =
2111 case AList.lookup (fn (SOME x, SOME y) =>
2112 (term_match thy) (x, y) | _ => false)
2114 SOME format => format
2115 | NONE => let val format = the (AList.lookup (op =) formats NONE) in
2117 Const x => intersect_formats format
2118 (const_format thy def_table x)
2122 (* int list -> int list -> typ -> typ *)
2123 fun format_type default_format format T =
2125 val T = unarize_and_unbox_type T
2126 val format = format |> filter (curry (op <) 0)
2128 if forall (curry (op =) 1) format then
2132 val (binder_Ts, body_T) = strip_type T
2135 |> map (format_type default_format default_format)
2136 |> rev |> chunk_list_unevenly (rev format)
2137 |> map (HOLogic.mk_tupleT o rev)
2138 in List.foldl (op -->) body_T batched end
2140 (* theory -> const_table -> (term option * int list) list -> term -> typ *)
2141 fun format_term_type thy def_table formats t =
2142 format_type (the (AList.lookup (op =) formats NONE))
2143 (lookup_format thy def_table formats t) (fastype_of t)
2145 (* int list -> int -> int list -> int list *)
2146 fun repair_special_format js m format =
2147 m - 1 downto 0 |> chunk_list_unevenly (rev format)
2148 |> map (rev o filter_out (member (op =) js))
2149 |> filter_out null |> map length |> rev
2151 (* hol_context -> string * string -> (term option * int list) list
2152 -> styp -> term * typ *)
2153 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
2154 : hol_context) (base_name, step_name) formats =
2156 val default_format = the (AList.lookup (op =) formats NONE)
2157 (* styp -> term * typ *)
2158 fun do_const (x as (s, T)) =
2159 (if String.isPrefix special_prefix s then
2162 val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
2163 val (x' as (_, T'), js, ts) =
2164 AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
2166 val max_j = List.last js
2167 val Ts = List.take (binder_types T', max_j + 1)
2168 val missing_js = filter_out (member (op =) js) (0 upto max_j)
2169 val missing_Ts = filter_indices missing_js Ts
2170 (* int -> indexname *)
2171 fun nth_missing_var n =
2172 ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
2173 val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
2174 val vars = special_bounds ts @ missing_vars
2175 val ts' = map2 (fn T => fn j =>
2176 case AList.lookup (op =) (js ~~ ts) j of
2179 Var (nth missing_vars
2180 (find_index (curry (op =) j)
2183 val t = do_const x' |> fst
2185 case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
2186 | _ => false) formats (SOME t) of
2188 repair_special_format js (num_binder_types T') format
2190 const_format thy def_table x'
2191 |> repair_special_format js (num_binder_types T')
2192 |> intersect_formats default_format
2194 (list_comb (t, ts') |> fold_rev abs_var vars,
2195 format_type default_format format T)
2197 else if String.isPrefix uncurry_prefix s then
2199 val (ss, s') = unprefix uncurry_prefix s
2200 |> strip_first_name_sep |>> space_explode "@"
2202 if String.isPrefix step_prefix s' then
2206 val k = the (Int.fromString (hd ss))
2207 val j = the (Int.fromString (List.last ss))
2208 val (before_Ts, (tuple_T, rest_T)) =
2209 strip_n_binders j T ||> (strip_n_binders 1 #>> hd)
2210 val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T
2211 in do_const (s', T') end
2213 else if String.isPrefix unrolled_prefix s then
2214 let val t = Const (original_name s, range_type T) in
2215 (lambda (Free (iter_var_prefix, nat_T)) t,
2216 format_type default_format
2217 (lookup_format thy def_table formats t) T)
2219 else if String.isPrefix base_prefix s then
2220 (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
2221 format_type default_format default_format T)
2222 else if String.isPrefix step_prefix s then
2223 (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
2224 format_type default_format default_format T)
2225 else if String.isPrefix skolem_prefix s then
2227 val ss = the (AList.lookup (op =) (!skolems) s)
2228 val (Ts, Ts') = chop (length ss) (binder_types T)
2229 val frees = map Free (ss ~~ Ts)
2230 val s' = original_name s
2232 (fold lambda frees (Const (s', Ts' ---> T)),
2233 format_type default_format
2234 (lookup_format thy def_table formats (Const x)) T)
2236 else if String.isPrefix eval_prefix s then
2238 val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
2239 in (t, format_term_type thy def_table formats t) end
2240 else if s = @{const_name undefined_fast_The} then
2241 (Const (nitpick_prefix ^ "The fallback", T),
2242 format_type default_format
2243 (lookup_format thy def_table formats
2244 (Const (@{const_name The}, (T --> bool_T) --> T))) T)
2245 else if s = @{const_name undefined_fast_Eps} then
2246 (Const (nitpick_prefix ^ "Eps fallback", T),
2247 format_type default_format
2248 (lookup_format thy def_table formats
2249 (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
2251 let val t = Const (original_name s, T) in
2252 (t, format_term_type thy def_table formats t)
2254 |>> map_types unarize_and_unbox_type
2255 |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
2258 (* styp -> string *)
2259 fun assign_operator_for_const (s, T) =
2260 if String.isPrefix ubfp_prefix s then
2261 if is_fun_type T then "\<subseteq>" else "\<le>"
2262 else if String.isPrefix lbfp_prefix s then
2263 if is_fun_type T then "\<supseteq>" else "\<ge>"
2264 else if original_name s <> s then
2265 assign_operator_for_const (after_name_sep s, T)