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 quot_normal_prefix : string
58 val skolem_prefix : string
59 val special_prefix : string
60 val uncurry_prefix : string
61 val eval_prefix : string
62 val original_name : string -> string
63 val s_conj : term * term -> term
64 val s_disj : term * term -> term
65 val strip_any_connective : term -> term list * term
66 val conjuncts_of : term -> term list
67 val disjuncts_of : term -> term list
68 val unarize_and_unbox_type : typ -> typ
69 val unarize_unbox_and_uniterize_type : typ -> typ
70 val string_for_type : Proof.context -> typ -> string
71 val prefix_name : string -> string -> string
72 val shortest_name : string -> string
73 val short_name : string -> string
74 val shorten_names_in_term : term -> term
75 val type_match : theory -> typ * typ -> bool
76 val const_match : theory -> styp * styp -> bool
77 val term_match : theory -> term * term -> bool
78 val is_TFree : typ -> bool
79 val is_higher_order_type : typ -> bool
80 val is_fun_type : typ -> bool
81 val is_set_type : typ -> bool
82 val is_pair_type : typ -> bool
83 val is_lfp_iterator_type : typ -> bool
84 val is_gfp_iterator_type : typ -> bool
85 val is_fp_iterator_type : typ -> bool
86 val is_iterator_type : typ -> bool
87 val is_boolean_type : typ -> bool
88 val is_integer_type : typ -> bool
89 val is_bit_type : typ -> bool
90 val is_word_type : typ -> bool
91 val is_integer_like_type : typ -> bool
92 val is_record_type : typ -> bool
93 val is_number_type : theory -> typ -> bool
94 val const_for_iterator_type : typ -> styp
95 val strip_n_binders : int -> typ -> typ list * typ
96 val nth_range_type : int -> typ -> typ
97 val num_factors_in_type : typ -> int
98 val num_binder_types : typ -> int
99 val curried_binder_types : typ -> typ list
100 val mk_flat_tuple : typ -> term list -> term
101 val dest_n_tuple : int -> term -> term list
102 val is_real_datatype : theory -> string -> bool
103 val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
104 val is_quot_type : theory -> typ -> bool
105 val is_codatatype : theory -> typ -> bool
106 val is_pure_typedef : theory -> typ -> bool
107 val is_univ_typedef : theory -> typ -> bool
108 val is_datatype : theory -> (typ option * bool) list -> typ -> bool
109 val is_record_constr : styp -> bool
110 val is_record_get : theory -> styp -> bool
111 val is_record_update : theory -> styp -> bool
112 val is_abs_fun : theory -> styp -> bool
113 val is_rep_fun : theory -> styp -> bool
114 val is_quot_abs_fun : Proof.context -> styp -> bool
115 val is_quot_rep_fun : Proof.context -> styp -> bool
116 val mate_of_rep_fun : theory -> styp -> styp
117 val is_constr_like : theory -> styp -> bool
118 val is_stale_constr : theory -> styp -> bool
119 val is_constr : theory -> (typ option * bool) list -> styp -> bool
120 val is_sel : string -> bool
121 val is_sel_like_and_no_discr : string -> bool
122 val box_type : hol_context -> boxability -> typ -> typ
123 val binarize_nat_and_int_in_type : typ -> typ
124 val binarize_nat_and_int_in_term : term -> term
125 val discr_for_constr : styp -> styp
126 val num_sels_for_constr_type : typ -> int
127 val nth_sel_name_for_constr_name : string -> int -> string
128 val nth_sel_for_constr : styp -> int -> styp
129 val binarized_and_boxed_nth_sel_for_constr :
130 hol_context -> bool -> styp -> int -> styp
131 val sel_no_from_name : string -> int
132 val close_form : term -> term
133 val eta_expand : typ list -> term -> int -> term
134 val extensionalize : term -> term
135 val distinctness_formula : typ -> term list -> term
136 val register_frac_type : string -> (string * string) list -> theory -> theory
137 val unregister_frac_type : string -> theory -> theory
138 val register_codatatype : typ -> string -> styp list -> theory -> theory
139 val unregister_codatatype : typ -> theory -> theory
140 val datatype_constrs : hol_context -> typ -> styp list
141 val binarized_and_boxed_datatype_constrs :
142 hol_context -> bool -> typ -> styp list
143 val num_datatype_constrs : hol_context -> typ -> int
144 val constr_name_for_sel_like : string -> string
145 val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
146 val discriminate_value : hol_context -> styp -> term -> term
147 val select_nth_constr_arg :
148 theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
149 val construct_value :
150 theory -> (typ option * bool) list -> styp -> term list -> term
151 val card_of_type : (typ * int) list -> typ -> int
152 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
153 val bounded_exact_card_of_type :
154 hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
155 val is_finite_type : hol_context -> typ -> bool
156 val special_bounds : term list -> (indexname * typ) list
157 val is_funky_typedef : theory -> typ -> bool
159 theory -> (term * term) list -> term list * term list * term list
160 val arity_of_built_in_const :
161 theory -> (typ option * bool) list -> bool -> styp -> int option
162 val is_built_in_const :
163 theory -> (typ option * bool) list -> bool -> styp -> bool
164 val term_under_def : term -> term
165 val case_const_names :
166 theory -> (typ option * bool) list -> (string * int) list
167 val const_def_table :
168 Proof.context -> (term * term) list -> term list -> const_table
169 val const_nondef_table : term list -> const_table
170 val const_simp_table : Proof.context -> (term * term) list -> const_table
171 val const_psimp_table : Proof.context -> (term * term) list -> const_table
172 val inductive_intro_table :
173 Proof.context -> (term * term) list -> const_table -> const_table
174 val ground_theorem_table : theory -> term list Inttab.table
175 val ersatz_table : theory -> (string * string) list
176 val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
177 val inverse_axioms_for_rep_fun : theory -> styp -> term list
178 val optimized_typedef_axioms : theory -> string * typ list -> term list
179 val optimized_quot_type_axioms :
180 Proof.context -> (typ option * bool) list -> string * typ list -> term list
181 val def_of_const : theory -> const_table -> styp -> term option
182 val fixpoint_kind_of_const :
183 theory -> const_table -> string * typ -> fixpoint_kind
184 val is_inductive_pred : hol_context -> styp -> bool
185 val is_equational_fun : hol_context -> styp -> bool
186 val is_constr_pattern_lhs : theory -> term -> bool
187 val is_constr_pattern_formula : theory -> term -> bool
188 val unfold_defs_in_term : hol_context -> term -> term
189 val codatatype_bisim_axioms : hol_context -> typ -> term list
190 val is_well_founded_inductive_pred : hol_context -> styp -> bool
191 val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
192 val equational_fun_axioms : hol_context -> styp -> term list
193 val is_equational_fun_surely_complete : hol_context -> styp -> bool
194 val merge_type_vars_in_terms : term list -> term list
195 val ground_types_in_type : hol_context -> bool -> typ -> typ list
196 val ground_types_in_terms : hol_context -> bool -> term list -> typ list
197 val format_type : int list -> int list -> typ -> typ
198 val format_term_type :
199 theory -> const_table -> (term option * int list) list -> term -> typ
200 val user_friendly_const :
201 hol_context -> string * string -> (term option * int list) list
202 -> styp -> term * typ
203 val assign_operator_for_const : styp -> string
206 structure Nitpick_HOL : NITPICK_HOL =
211 type const_table = term list Symtab.table
212 type special_fun = (styp * int list * term list) * styp
213 type unrolled = styp * styp
214 type wf_cache = (styp * (bool * bool)) list
219 max_bisim_depth: int,
220 boxes: (typ option * bool option) list,
221 stds: (typ option * bool) list,
222 wfs: (styp option * bool option) list,
223 user_axioms: bool option,
225 binary_ints: bool option,
226 destroy_constrs: bool,
229 star_linear_preds: bool,
232 tac_timeout: Time.time option,
234 case_names: (string * int) list,
235 def_table: const_table,
236 nondef_table: const_table,
237 user_nondefs: term list,
238 simp_table: const_table Unsynchronized.ref,
239 psimp_table: const_table,
240 intro_table: const_table,
241 ground_thm_table: term list Inttab.table,
242 ersatz_table: (string * string) list,
243 skolems: (string * string list) list Unsynchronized.ref,
244 special_funs: special_fun list Unsynchronized.ref,
245 unrolled_preds: unrolled list Unsynchronized.ref,
246 wf_cache: wf_cache Unsynchronized.ref,
247 constr_cache: (typ * styp list) list Unsynchronized.ref}
249 datatype fixpoint_kind = Lfp | Gfp | NoFp
250 datatype boxability =
251 InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
253 structure Data = Theory_Data(
254 type T = {frac_types: (string * (string * string) list) list,
255 codatatypes: (string * (string * styp list)) list}
256 val empty = {frac_types = [], codatatypes = []}
258 fun merge ({frac_types = fs1, codatatypes = cs1},
259 {frac_types = fs2, codatatypes = cs2}) : T =
260 {frac_types = AList.merge (op =) (K true) (fs1, fs2),
261 codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
264 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
265 val sel_prefix = nitpick_prefix ^ "sel"
266 val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
267 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
268 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
269 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
270 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
271 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
272 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
273 val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
274 val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
275 val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep
276 val skolem_prefix = nitpick_prefix ^ "sk"
277 val special_prefix = nitpick_prefix ^ "sp"
278 val uncurry_prefix = nitpick_prefix ^ "unc"
279 val eval_prefix = nitpick_prefix ^ "eval"
280 val iter_var_prefix = "i"
281 val arg_var_prefix = "x"
284 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
285 (* Proof.context -> typ -> string *)
286 fun quot_normal_name_for_type ctxt T =
287 quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T)
289 (* string -> string * string *)
290 val strip_first_name_sep =
291 Substring.full #> Substring.position name_sep ##> Substring.triml 1
292 #> pairself Substring.string
293 (* string -> string *)
294 fun original_name s =
295 if String.isPrefix nitpick_prefix s then
296 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
299 val after_name_sep = snd o strip_first_name_sep
301 (* term * term -> term *)
302 fun s_conj (t1, @{const True}) = t1
303 | s_conj (@{const True}, t2) = t2
305 if t1 = @{const False} orelse t2 = @{const False} then @{const False}
306 else HOLogic.mk_conj (t1, t2)
307 fun s_disj (t1, @{const False}) = t1
308 | s_disj (@{const False}, t2) = t2
310 if t1 = @{const True} orelse t2 = @{const True} then @{const True}
311 else HOLogic.mk_disj (t1, t2)
313 (* term -> term -> term list *)
314 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
315 if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
316 | strip_connective _ t = [t]
317 (* term -> term list * term *)
318 fun strip_any_connective (t as (t0 $ _ $ _)) =
319 if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
320 (strip_connective t0 t, t0)
323 | strip_any_connective t = ([t], @{const Not})
324 (* term -> term list *)
325 val conjuncts_of = strip_connective @{const "op &"}
326 val disjuncts_of = strip_connective @{const "op |"}
328 (* When you add constants to these lists, make sure to handle them in
329 "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
331 val built_in_consts =
332 [(@{const_name all}, 1),
333 (@{const_name "=="}, 2),
334 (@{const_name "==>"}, 2),
335 (@{const_name Pure.conjunction}, 2),
336 (@{const_name Trueprop}, 1),
337 (@{const_name Not}, 1),
338 (@{const_name False}, 0),
339 (@{const_name True}, 0),
340 (@{const_name All}, 1),
341 (@{const_name Ex}, 1),
342 (@{const_name "op ="}, 2),
343 (@{const_name "op &"}, 2),
344 (@{const_name "op |"}, 2),
345 (@{const_name "op -->"}, 2),
346 (@{const_name If}, 3),
347 (@{const_name Let}, 2),
348 (@{const_name Unity}, 0),
349 (@{const_name Pair}, 2),
350 (@{const_name fst}, 1),
351 (@{const_name snd}, 1),
352 (@{const_name Id}, 0),
353 (@{const_name insert}, 2),
354 (@{const_name converse}, 1),
355 (@{const_name trancl}, 1),
356 (@{const_name rel_comp}, 2),
357 (@{const_name image}, 2),
358 (@{const_name finite}, 1),
359 (@{const_name unknown}, 0),
360 (@{const_name is_unknown}, 1),
361 (@{const_name Tha}, 1),
362 (@{const_name Frac}, 0),
363 (@{const_name norm_frac}, 0)]
364 val built_in_nat_consts =
365 [(@{const_name Suc}, 0),
366 (@{const_name nat}, 0),
367 (@{const_name nat_gcd}, 0),
368 (@{const_name nat_lcm}, 0)]
369 val built_in_descr_consts =
370 [(@{const_name The}, 1),
371 (@{const_name Eps}, 1)]
372 val built_in_typed_consts =
373 [((@{const_name zero_class.zero}, int_T), 0),
374 ((@{const_name one_class.one}, int_T), 0),
375 ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
376 ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
377 ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
378 ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
379 ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
380 ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
381 ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
382 val built_in_typed_nat_consts =
383 [((@{const_name zero_class.zero}, nat_T), 0),
384 ((@{const_name one_class.one}, nat_T), 0),
385 ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
386 ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
387 ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
388 ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
389 ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
390 ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
391 ((@{const_name of_nat}, nat_T --> int_T), 0)]
392 val built_in_set_consts =
393 [(@{const_name semilattice_inf_class.inf}, 2),
394 (@{const_name semilattice_sup_class.sup}, 2),
395 (@{const_name minus_class.minus}, 2),
396 (@{const_name ord_class.less_eq}, 2)]
399 fun unarize_type @{typ "unsigned_bit word"} = nat_T
400 | unarize_type @{typ "signed_bit word"} = int_T
401 | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
403 fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
404 unarize_and_unbox_type (Type ("fun", Ts))
405 | unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
406 Type ("*", map unarize_and_unbox_type Ts)
407 | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
408 | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
409 | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
410 Type (s, map unarize_and_unbox_type Ts)
411 | unarize_and_unbox_type T = T
412 fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
413 | uniterize_type @{typ bisim_iterator} = nat_T
414 | uniterize_type T = T
415 val unarize_unbox_and_uniterize_type = uniterize_type o unarize_and_unbox_type
417 (* Proof.context -> typ -> string *)
418 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
420 (* string -> string -> string *)
421 val prefix_name = Long_Name.qualify o Long_Name.base_name
422 (* string -> string *)
423 fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
424 (* string -> term -> term *)
425 val prefix_abs_vars = Term.map_abs_vars o prefix_name
426 (* string -> string *)
428 case space_explode name_sep s of
429 [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
430 | ss => map shortest_name ss |> space_implode "_"
432 fun shorten_names_in_type (Type (s, Ts)) =
433 Type (short_name s, map shorten_names_in_type Ts)
434 | shorten_names_in_type T = T
436 val shorten_names_in_term =
437 map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
438 #> map_types shorten_names_in_type
440 (* theory -> typ * typ -> bool *)
441 fun type_match thy (T1, T2) =
442 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
443 handle Type.TYPE_MATCH => false
444 (* theory -> styp * styp -> bool *)
445 fun const_match thy ((s1, T1), (s2, T2)) =
446 s1 = s2 andalso type_match thy (T1, T2)
447 (* theory -> term * term -> bool *)
448 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
449 | term_match thy (Free (s1, T1), Free (s2, T2)) =
450 const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
451 | term_match _ (t1, t2) = t1 aconv t2
454 fun is_TFree (TFree _) = true
456 fun is_higher_order_type (Type ("fun", _)) = true
457 | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
458 | is_higher_order_type _ = false
459 fun is_fun_type (Type ("fun", _)) = true
460 | is_fun_type _ = false
461 fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
462 | is_set_type _ = false
463 fun is_pair_type (Type ("*", _)) = true
464 | is_pair_type _ = false
465 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
466 | is_lfp_iterator_type _ = false
467 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
468 | is_gfp_iterator_type _ = false
469 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
470 fun is_iterator_type T =
471 (T = @{typ bisim_iterator} orelse is_fp_iterator_type T)
472 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
473 fun is_integer_type T = (T = nat_T orelse T = int_T)
474 fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
475 fun is_word_type (Type (@{type_name word}, _)) = true
476 | is_word_type _ = false
477 val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
478 val is_record_type = not o null o Record.dest_recTs
479 (* theory -> typ -> bool *)
480 fun is_frac_type thy (Type (s, [])) =
481 not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
482 | is_frac_type _ _ = false
483 fun is_number_type thy = is_integer_like_type orf is_frac_type thy
485 (* bool -> styp -> typ *)
486 fun iterator_type_for_const gfp (s, T) =
487 Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
490 fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
491 | const_for_iterator_type T =
492 raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
494 (* int -> typ -> typ list * typ *)
495 fun strip_n_binders 0 T = ([], T)
496 | strip_n_binders n (Type ("fun", [T1, T2])) =
497 strip_n_binders (n - 1) T2 |>> cons T1
498 | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
499 strip_n_binders n (Type ("fun", Ts))
500 | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
502 val nth_range_type = snd oo strip_n_binders
505 fun num_factors_in_type (Type ("*", [T1, T2])) =
506 fold (Integer.add o num_factors_in_type) [T1, T2] 0
507 | num_factors_in_type _ = 1
508 fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
509 | num_binder_types _ = 0
510 (* typ -> typ list *)
511 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
512 fun maybe_curried_binder_types T =
513 (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
515 (* typ -> term list -> term *)
516 fun mk_flat_tuple _ [t] = t
517 | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
518 HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
519 | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
520 (* int -> term -> term list *)
521 fun dest_n_tuple 1 t = [t]
522 | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
524 (* int -> typ -> typ list *)
525 fun dest_n_tuple_type 1 T = [T]
526 | dest_n_tuple_type n (Type (_, [T1, T2])) =
527 T1 :: dest_n_tuple_type (n - 1) T2
528 | dest_n_tuple_type _ T =
529 raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
532 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
533 set_def: thm option, prop_of_Rep: thm, set_name: string,
534 Abs_inverse: thm option, Rep_inverse: thm option}
536 (* theory -> string -> typedef_info *)
537 fun typedef_info thy s =
538 if is_frac_type thy (Type (s, [])) then
539 SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
540 Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
541 set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
543 set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
544 else case Typedef.get_info thy s of
545 SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
547 SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
548 Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
549 set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
550 Rep_inverse = SOME Rep_inverse}
553 (* theory -> string -> bool *)
554 val is_typedef = is_some oo typedef_info
555 val is_real_datatype = is_some oo Datatype.get_info
556 (* theory -> (typ option * bool) list -> typ -> bool *)
557 fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
559 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
560 e.g., by adding a field to "Datatype_Aux.info". *)
561 (* theory -> (typ option * bool) list -> string -> bool *)
562 fun is_basic_datatype thy stds s =
563 member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
564 @{type_name int}, "Code_Numeral.code_numeral"] s orelse
565 (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
567 (* theory -> typ -> typ -> typ -> typ *)
568 fun instantiate_type thy T1 T1' T2 =
569 Same.commit (Envir.subst_type_same
570 (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
571 handle Type.TYPE_MATCH =>
572 raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
573 fun varify_and_instantiate_type thy T1 T1' T2 =
574 instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2)
576 (* theory -> typ -> typ -> styp *)
577 fun repair_constr_type thy body_T' T =
578 varify_and_instantiate_type thy (body_type T) body_T' T
580 (* string -> (string * string) list -> theory -> theory *)
581 fun register_frac_type frac_s ersaetze thy =
583 val {frac_types, codatatypes} = Data.get thy
584 val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
585 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
586 (* string -> theory -> theory *)
587 fun unregister_frac_type frac_s = register_frac_type frac_s []
589 (* typ -> string -> styp list -> theory -> theory *)
590 fun register_codatatype co_T case_name constr_xs thy =
592 val {frac_types, codatatypes} = Data.get thy
593 val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
594 val (co_s, co_Ts) = dest_Type co_T
596 if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
597 co_s <> "fun" andalso
598 not (is_basic_datatype thy [(NONE, true)] co_s) then
601 raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
602 val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
604 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
605 (* typ -> theory -> theory *)
606 fun unregister_codatatype co_T = register_codatatype co_T "" []
608 (* theory -> typ -> bool *)
609 fun is_quot_type thy (Type (s, _)) =
610 is_some (Quotient_Info.quotdata_lookup_raw thy s)
611 | is_quot_type _ _ = false
612 fun is_codatatype thy (Type (s, _)) =
613 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
614 |> Option.map snd |> these))
615 | is_codatatype _ _ = false
616 fun is_pure_typedef thy (T as Type (s, _)) =
617 is_typedef thy s andalso
618 not (is_real_datatype thy s orelse is_quot_type thy T orelse
619 is_codatatype thy T orelse is_record_type T orelse
620 is_integer_like_type T)
621 | is_pure_typedef _ _ = false
622 fun is_univ_typedef thy (Type (s, _)) =
623 (case typedef_info thy s of
624 SOME {set_def, prop_of_Rep, ...} =>
628 SOME thm => try (snd o Logic.dest_equals o prop_of) thm
629 | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop)
633 SOME (Const (@{const_name top}, _)) => true
634 | SOME (Const (@{const_name Collect}, _)
635 $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true
639 | is_univ_typedef _ _ = false
640 (* theory -> (typ option * bool) list -> typ -> bool *)
641 fun is_datatype thy stds (T as Type (s, _)) =
642 (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
643 is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
644 | is_datatype _ _ _ = false
646 (* theory -> typ -> (string * typ) list * (string * typ) *)
647 fun all_record_fields thy T =
648 let val (recs, more) = Record.get_extT_fields thy T in
649 recs @ more :: all_record_fields thy (snd more)
653 fun is_record_constr (s, T) =
654 String.isSuffix Record.extN s andalso
655 let val dataT = body_type T in
656 is_record_type dataT andalso
657 s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
659 (* theory -> typ -> int *)
660 val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
661 (* theory -> string -> typ -> int *)
662 fun no_of_record_field thy s T1 =
663 find_index (curry (op =) s o fst)
664 (Record.get_extT_fields thy T1 ||> single |> op @)
665 (* theory -> styp -> bool *)
666 fun is_record_get thy (s, Type ("fun", [T1, _])) =
667 exists (curry (op =) s o fst) (all_record_fields thy T1)
668 | is_record_get _ _ = false
669 fun is_record_update thy (s, T) =
670 String.isSuffix Record.updateN s andalso
671 exists (curry (op =) (unsuffix Record.updateN s) o fst)
672 (all_record_fields thy (body_type T))
673 handle TYPE _ => false
674 fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
675 (case typedef_info thy s' of
676 SOME {Abs_name, ...} => s = Abs_name
678 | is_abs_fun _ _ = false
679 fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
680 (case typedef_info thy s' of
681 SOME {Rep_name, ...} => s = Rep_name
683 | is_rep_fun _ _ = false
684 (* Proof.context -> styp -> bool *)
685 fun is_quot_abs_fun ctxt (x as (_, Type ("fun", [_, Type (s', _)]))) =
686 (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
688 | is_quot_abs_fun _ _ = false
689 fun is_quot_rep_fun ctxt (x as (_, Type ("fun", [Type (s', _), _]))) =
690 (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
692 | is_quot_rep_fun _ _ = false
694 (* theory -> styp -> styp *)
695 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
696 (case typedef_info thy s' of
697 SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
698 | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
699 | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
700 (* theory -> typ -> typ *)
701 fun rep_type_for_quot_type thy (T as Type (s, _)) =
702 let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
703 instantiate_type thy qtyp T rtyp
705 (* theory -> typ -> term *)
706 fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
708 val {qtyp, equiv_rel, ...} = Quotient_Info.quotdata_lookup thy s
709 val Ts' = qtyp |> dest_Type |> snd
710 in subst_atomic_types (Ts' ~~ Ts) equiv_rel end
711 | equiv_relation_for_quot_type _ T =
712 raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
714 (* theory -> styp -> bool *)
715 fun is_coconstr thy (s, T) =
717 val {codatatypes, ...} = Data.get thy
718 val co_T = body_type T
719 val co_s = dest_Type co_T |> fst
721 exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
722 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
724 handle TYPE ("dest_Type", _, _) => false
725 fun is_constr_like thy (s, T) =
726 member (op =) [@{const_name FunBox}, @{const_name PairBox},
727 @{const_name Quot}, @{const_name Zero_Rep},
728 @{const_name Suc_Rep}] s orelse
729 let val (x as (_, T)) = (s, unarize_and_unbox_type T) in
730 Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
731 (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
734 fun is_stale_constr thy (x as (_, T)) =
735 is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
736 not (is_coconstr thy x)
737 (* theory -> (typ option * bool) list -> styp -> bool *)
738 fun is_constr thy stds (x as (_, T)) =
739 is_constr_like thy x andalso
740 not (is_basic_datatype thy stds
741 (fst (dest_Type (unarize_type (body_type T))))) andalso
742 not (is_stale_constr thy x)
744 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
745 val is_sel_like_and_no_discr =
746 String.isPrefix sel_prefix
747 orf (member (op =) [@{const_name fst}, @{const_name snd}])
749 (* boxability -> boxability *)
750 fun in_fun_lhs_for InConstr = InSel
751 | in_fun_lhs_for _ = InFunLHS
752 fun in_fun_rhs_for InConstr = InConstr
753 | in_fun_rhs_for InSel = InSel
754 | in_fun_rhs_for InFunRHS1 = InFunRHS2
755 | in_fun_rhs_for _ = InFunRHS1
757 (* hol_context -> boxability -> typ -> bool *)
758 fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
761 (boxy = InPair orelse boxy = InFunLHS) andalso
762 not (is_boolean_type (body_type T))
764 boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
765 ((boxy = InExpr orelse boxy = InFunLHS) andalso
766 exists (is_boxing_worth_it hol_ctxt InPair)
767 (map (box_type hol_ctxt InPair) Ts))
769 (* hol_context -> boxability -> string * typ list -> string *)
770 and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z =
771 case triple_lookup (type_match thy) boxes (Type z) of
772 SOME (SOME box_me) => box_me
773 | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
774 (* hol_context -> boxability -> typ -> typ *)
775 and box_type hol_ctxt boxy T =
777 Type (z as ("fun", [T1, T2])) =>
778 if boxy <> InConstr andalso boxy <> InSel andalso
779 should_box_type hol_ctxt boxy z then
780 Type (@{type_name fun_box},
781 [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
783 box_type hol_ctxt (in_fun_lhs_for boxy) T1
784 --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
785 | Type (z as ("*", Ts)) =>
786 if boxy <> InConstr andalso boxy <> InSel
787 andalso should_box_type hol_ctxt boxy z then
788 Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
790 Type ("*", map (box_type hol_ctxt
791 (if boxy = InConstr orelse boxy = InSel then boxy
796 fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
797 | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
798 | binarize_nat_and_int_in_type (Type (s, Ts)) =
799 Type (s, map binarize_nat_and_int_in_type Ts)
800 | binarize_nat_and_int_in_type T = T
802 val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
805 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
808 fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
809 (* string -> int -> string *)
810 fun nth_sel_name_for_constr_name s n =
811 if s = @{const_name Pair} then
812 if n = 0 then @{const_name fst} else @{const_name snd}
815 (* styp -> int -> styp *)
816 fun nth_sel_for_constr x ~1 = discr_for_constr x
817 | nth_sel_for_constr (s, T) n =
818 (nth_sel_name_for_constr_name s n,
819 body_type T --> nth (maybe_curried_binder_types T) n)
820 (* hol_context -> bool -> styp -> int -> styp *)
821 fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
822 apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
823 oo nth_sel_for_constr
826 fun sel_no_from_name s =
827 if String.isPrefix discr_prefix s then
829 else if String.isPrefix sel_prefix s then
830 s |> unprefix sel_prefix |> Int.fromString |> the
831 else if s = @{const_name snd} then
839 (* (indexname * typ) list -> (indexname * typ) list -> term -> term *)
840 fun close_up zs zs' =
841 fold (fn (z as ((s, _), T)) => fn t' =>
842 Term.all T $ Abs (s, T, abstract_over (Var z, t')))
843 (take (length zs' - length zs) zs')
844 (* (indexname * typ) list -> term -> term *)
845 fun aux zs (@{const "==>"} $ t1 $ t2) =
846 let val zs' = Term.add_vars t1 zs in
847 close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
849 | aux zs t = close_up zs (Term.add_vars t zs) t
852 (* typ list -> term -> int -> term *)
853 fun eta_expand _ t 0 = t
854 | eta_expand Ts (Abs (s, T, t')) n =
855 Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
856 | eta_expand Ts t n =
857 fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
858 (List.take (binder_types (fastype_of1 (Ts, t)), n))
859 (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
862 fun extensionalize t =
864 (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
865 | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>
866 let val v = Var ((s, maxidx_of_term t + 1), T) in
867 extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))
871 (* typ -> term list -> term *)
872 fun distinctness_formula T =
873 all_distinct_unordered_pairs_of
874 #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
875 #> List.foldr (s_conj o swap) @{const True}
878 fun zero_const T = Const (@{const_name zero_class.zero}, T)
879 fun suc_const T = Const (@{const_name Suc}, T --> T)
881 (* hol_context -> typ -> styp list *)
882 fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
883 (T as Type (s, Ts)) =
884 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
885 SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
887 if is_datatype thy stds T then
888 case Datatype.get_info thy s of
889 SOME {index, descr, ...} =>
891 val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
894 (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
898 if is_record_type T then
900 val s' = unsuffix Record.ext_typeN s ^ Record.extN
901 val T' = (Record.get_extT_fields thy T
902 |> apsnd single |> uncurry append |> map snd) ---> T
904 else if is_quot_type thy T then
905 [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
906 else case typedef_info thy s of
907 SOME {abs_type, rep_type, Abs_name, ...} =>
909 varify_and_instantiate_type thy abs_type T rep_type --> T)]
911 if T = @{typ ind} then
912 [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
917 | uncached_datatype_constrs _ _ = []
918 (* hol_context -> typ -> styp list *)
919 fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
920 case AList.lookup (op =) (!constr_cache) T of
923 let val xs = uncached_datatype_constrs hol_ctxt T in
924 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
926 (* hol_context -> bool -> typ -> styp list *)
927 fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
928 map (apsnd ((binarize ? binarize_nat_and_int_in_type)
929 o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
930 (* hol_context -> typ -> int *)
931 val num_datatype_constrs = length oo datatype_constrs
933 (* string -> string *)
934 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
935 | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
936 | constr_name_for_sel_like s' = original_name s'
937 (* hol_context -> bool -> styp -> styp *)
938 fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
939 let val s = constr_name_for_sel_like s' in
941 (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
946 (* hol_context -> styp -> term *)
947 fun discr_term_for_constr hol_ctxt (x as (s, T)) =
948 let val dataT = body_type T in
949 if s = @{const_name Suc} then
951 @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
952 else if num_datatype_constrs hol_ctxt dataT >= 2 then
953 Const (discr_for_constr x)
955 Abs (Name.uu, dataT, @{const True})
957 (* hol_context -> styp -> term -> term *)
958 fun discriminate_value (hol_ctxt as {thy, ...}) x t =
961 if x = x' then @{const True}
962 else if is_constr_like thy x' then @{const False}
963 else betapply (discr_term_for_constr hol_ctxt x, t)
964 | _ => betapply (discr_term_for_constr hol_ctxt x, t)
966 (* theory -> (typ option * bool) list -> styp -> term -> term *)
967 fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
968 let val (arg_Ts, dataT) = strip_type T in
969 if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
970 @{term "%n::nat. n - 1"}
971 else if is_pair_type dataT then
972 Const (nth_sel_for_constr x n)
975 (* int -> typ -> int * term *)
976 fun aux m (Type ("*", [T1, T2])) =
978 val (m, t1) = aux m T1
979 val (m, t2) = aux m T2
980 in (m, HOLogic.mk_prod (t1, t2)) end
982 (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
984 val m = fold (Integer.add o num_factors_in_type)
985 (List.take (arg_Ts, n)) 0
986 in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
988 (* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *)
989 fun select_nth_constr_arg thy stds x t n res_T =
990 (case strip_comb t of
992 if x = x' then nth args n
993 else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
996 handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
998 (* theory -> (typ option * bool) list -> styp -> term list -> term *)
999 fun construct_value _ _ x [] = Const x
1000 | construct_value thy stds (x as (s, _)) args =
1001 let val args = map Envir.eta_contract args in
1003 Const (s', _) $ t =>
1004 if is_sel_like_and_no_discr s' andalso
1005 constr_name_for_sel_like s' = s andalso
1006 forall (fn (n, t') =>
1007 select_nth_constr_arg thy stds x t n dummyT = t')
1008 (index_seq 0 (length args) ~~ args) then
1011 list_comb (Const x, args)
1012 | _ => list_comb (Const x, args)
1015 (* (typ * int) list -> typ -> int *)
1016 fun card_of_type assigns (Type ("fun", [T1, T2])) =
1017 reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
1018 | card_of_type assigns (Type ("*", [T1, T2])) =
1019 card_of_type assigns T1 * card_of_type assigns T2
1020 | card_of_type _ (Type (@{type_name itself}, _)) = 1
1021 | card_of_type _ @{typ prop} = 2
1022 | card_of_type _ @{typ bool} = 2
1023 | card_of_type _ @{typ unit} = 1
1024 | card_of_type assigns T =
1025 case AList.lookup (op =) assigns T of
1027 | NONE => if T = @{typ bisim_iterator} then 0
1028 else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
1029 (* int -> (typ * int) list -> typ -> int *)
1030 fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
1032 val k1 = bounded_card_of_type max default_card assigns T1
1033 val k2 = bounded_card_of_type max default_card assigns T2
1035 if k1 = max orelse k2 = max then max
1036 else Int.min (max, reasonable_power k2 k1)
1038 | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
1040 val k1 = bounded_card_of_type max default_card assigns T1
1041 val k2 = bounded_card_of_type max default_card assigns T2
1042 in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
1043 | bounded_card_of_type max default_card assigns T =
1044 Int.min (max, if default_card = ~1 then
1045 card_of_type assigns T
1047 card_of_type assigns T
1048 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
1050 (* hol_context -> typ list -> int -> (typ * int) list -> typ -> int *)
1051 fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
1054 (* typ list -> typ -> int *)
1056 (if member (op =) avoid T then
1058 else if member (op =) finitizable_dataTs T then
1061 Type ("fun", [T1, T2]) =>
1063 val k1 = aux avoid T1
1064 val k2 = aux avoid T2
1066 if k1 = 0 orelse k2 = 0 then 0
1067 else if k1 >= max orelse k2 >= max then max
1068 else Int.min (max, reasonable_power k2 k1)
1070 | Type ("*", [T1, T2]) =>
1072 val k1 = aux avoid T1
1073 val k2 = aux avoid T2
1075 if k1 = 0 orelse k2 = 0 then 0
1076 else if k1 >= max orelse k2 >= max then max
1077 else Int.min (max, k1 * k2)
1079 | Type (@{type_name itself}, _) => 1
1084 (case datatype_constrs hol_ctxt T of
1085 [] => if is_integer_type T orelse is_bit_type T then 0
1090 map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
1093 if exists (curry (op =) 0) constr_cards then 0
1094 else Integer.sum constr_cards
1096 | _ => raise SAME ())
1098 AList.lookup (op =) assigns T |> the_default default_card
1099 in Int.min (max, aux [] T) end
1101 (* hol_context -> typ -> bool *)
1102 fun is_finite_type hol_ctxt T =
1103 bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0
1106 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
1107 | is_ground_term (Const _) = true
1108 | is_ground_term _ = false
1110 (* term -> word -> word *)
1111 fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
1112 | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
1113 | hashw_term _ = 0w0
1115 val hash_term = Word.toInt o hashw_term
1117 (* term list -> (indexname * typ) list *)
1118 fun special_bounds ts =
1119 fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
1121 (* indexname * typ -> term -> term *)
1122 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
1124 (* theory -> string -> bool *)
1125 fun is_funky_typedef_name thy s =
1126 member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
1127 @{type_name int}] s orelse
1128 is_frac_type thy (Type (s, []))
1129 (* theory -> typ -> bool *)
1130 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
1131 | is_funky_typedef _ _ = false
1133 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
1134 $ Const (@{const_name TYPE}, _)) = true
1135 | is_arity_type_axiom _ = false
1136 (* theory -> bool -> term -> bool *)
1137 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
1138 is_typedef_axiom thy boring t2
1139 | is_typedef_axiom thy boring
1140 (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
1141 $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
1142 boring <> is_funky_typedef_name thy s andalso is_typedef thy s
1143 | is_typedef_axiom _ _ _ = false
1145 (* Distinguishes between (1) constant definition axioms, (2) type arity and
1146 typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
1147 Typedef axioms are uninteresting to Nitpick, because it can retrieve them
1148 using "typedef_info". *)
1149 (* theory -> (string * term) list -> string list -> term list * term list *)
1150 fun partition_axioms_by_definitionality thy axioms def_names =
1152 val axioms = sort (fast_string_ord o pairself fst) axioms
1153 val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
1155 OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
1156 |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
1157 in pairself (map snd) (defs, nondefs) end
1159 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
1160 will do as long as it contains all the "axioms" and "axiomatization"
1162 (* theory -> bool *)
1163 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
1166 val is_trivial_definition =
1167 the_default false o try (op aconv o Logic.dest_equals)
1168 val is_plain_definition =
1172 case strip_comb t1 of
1174 forall is_Var args andalso not (has_duplicates (op =) args)
1176 fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
1177 | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
1182 (* theory -> (term * term) list -> term list * term list * term list *)
1183 fun all_axioms_of thy subst =
1185 (* theory list -> term list *)
1186 val axioms_of_thys =
1187 maps Thm.axioms_of #> map (apsnd (subst_atomic subst o prop_of))
1188 val specs = Defs.all_specifications_of (Theory.defs_of thy)
1189 val def_names = specs |> maps snd |> map_filter #def
1190 |> OrdList.make fast_string_ord
1191 val thys = thy :: Theory.ancestors_of thy
1192 val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
1193 val built_in_axioms = axioms_of_thys built_in_thys
1194 val user_axioms = axioms_of_thys user_thys
1195 val (built_in_defs, built_in_nondefs) =
1196 partition_axioms_by_definitionality thy built_in_axioms def_names
1197 ||> filter (is_typedef_axiom thy false)
1198 val (user_defs, user_nondefs) =
1199 partition_axioms_by_definitionality thy user_axioms def_names
1200 val (built_in_nondefs, user_nondefs) =
1201 List.partition (is_typedef_axiom thy false) user_nondefs
1202 |>> append built_in_nondefs
1204 (thy |> PureThy.all_thms_of
1205 |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
1206 |> map (prop_of o snd)
1207 |> filter_out is_trivial_definition
1208 |> filter is_plain_definition) @
1209 user_defs @ built_in_defs
1210 in (defs, built_in_nondefs, user_nondefs) end
1212 (* theory -> (typ option * bool) list -> bool -> styp -> int option *)
1213 fun arity_of_built_in_const thy stds fast_descrs (s, T) =
1214 if s = @{const_name If} then
1215 if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
1217 let val std_nats = is_standard_datatype thy stds nat_T in
1218 case AList.lookup (op =)
1220 |> std_nats ? append built_in_nat_consts
1221 |> fast_descrs ? append built_in_descr_consts) s of
1224 case AList.lookup (op =)
1225 (built_in_typed_consts
1226 |> std_nats ? append built_in_typed_nat_consts)
1227 (s, unarize_type T) of
1231 @{const_name zero_class.zero} =>
1232 if is_iterator_type T then SOME 0 else NONE
1233 | @{const_name Suc} =>
1234 if is_iterator_type (domain_type T) then SOME 0 else NONE
1235 | _ => if is_fun_type T andalso is_set_type (domain_type T) then
1236 AList.lookup (op =) built_in_set_consts s
1240 (* theory -> (typ option * bool) list -> bool -> styp -> bool *)
1241 val is_built_in_const = is_some oooo arity_of_built_in_const
1243 (* This function is designed to work for both real definition axioms and
1244 simplification rules (equational specifications). *)
1246 fun term_under_def t =
1248 @{const "==>"} $ _ $ t2 => term_under_def t2
1249 | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
1250 | @{const Trueprop} $ t1 => term_under_def t1
1251 | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
1252 | Abs (_, _, t') => term_under_def t'
1253 | t1 $ _ => term_under_def t1
1256 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
1257 traversal of the term, without which the wrong occurrence of a constant could
1258 be matched in the face of overloading. *)
1259 (* theory -> (typ option * bool) list -> bool -> const_table -> styp
1261 fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
1262 if is_built_in_const thy stds fast_descrs x then
1265 these (Symtab.lookup table s)
1266 |> map_filter (try (Refute.specialize_type thy x))
1267 |> filter (curry (op =) (Const x) o term_under_def)
1269 (* term -> term option *)
1270 fun normalized_rhs_of t =
1272 (* term option -> term option *)
1273 fun aux (v as Var _) (SOME t) = SOME (lambda v t)
1274 | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
1278 Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
1279 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
1281 | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
1282 val args = strip_comb lhs |> snd
1283 in fold_rev aux args (SOME rhs) end
1285 (* theory -> const_table -> styp -> term option *)
1286 fun def_of_const thy table (x as (s, _)) =
1287 if is_built_in_const thy [(NONE, false)] false x orelse
1288 original_name s <> s then
1291 x |> def_props_for_const thy [(NONE, false)] false table |> List.last
1292 |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
1293 handle List.Empty => NONE
1295 (* term -> fixpoint_kind *)
1296 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
1297 | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
1298 | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
1299 | fixpoint_kind_of_rhs _ = NoFp
1301 (* theory -> const_table -> term -> bool *)
1302 fun is_mutually_inductive_pred_def thy table t =
1305 fun is_good_arg (Bound _) = true
1306 | is_good_arg (Const (s, _)) =
1307 s = @{const_name True} orelse s = @{const_name False} orelse
1308 s = @{const_name undefined}
1309 | is_good_arg _ = false
1311 case t |> strip_abs_body |> strip_comb of
1312 (Const x, ts as (_ :: _)) =>
1313 (case def_of_const thy table x of
1314 SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
1318 (* theory -> const_table -> term -> term *)
1319 fun unfold_mutually_inductive_preds thy table =
1320 map_aterms (fn t as Const x =>
1321 (case def_of_const thy table x of
1323 let val t' = Envir.eta_contract t' in
1324 if is_mutually_inductive_pred_def thy table t' then t'
1330 (* term -> string * term *)
1331 fun pair_for_prop t =
1332 case term_under_def t of
1333 Const (s, _) => (s, t)
1334 | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
1336 (* (Proof.context -> term list) -> Proof.context -> (term * term) list
1338 fun table_for get ctxt subst =
1339 ctxt |> get |> map (pair_for_prop o subst_atomic subst)
1340 |> AList.group (op =) |> Symtab.make
1342 (* theory -> (typ option * bool) list -> (string * int) list *)
1343 fun case_const_names thy stds =
1344 Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
1345 if is_basic_datatype thy stds dtype_s then
1348 cons (case_name, AList.lookup (op =) descr index
1349 |> the |> #3 |> length))
1350 (Datatype.get_all thy) [] @
1351 map (apsnd length o snd) (#codatatypes (Data.get thy))
1353 (* Proof.context -> (term * term) list -> term list -> const_table *)
1354 fun const_def_table ctxt subst ts =
1355 table_for (map prop_of o Nitpick_Defs.get) ctxt subst
1356 |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
1357 (map pair_for_prop ts)
1358 (* term list -> const_table *)
1359 fun const_nondef_table ts =
1360 fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
1361 |> AList.group (op =) |> Symtab.make
1362 (* Proof.context -> (term * term) list -> const_table *)
1363 val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
1364 val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
1365 (* Proof.context -> (term * term) list -> const_table -> const_table *)
1366 fun inductive_intro_table ctxt subst def_table =
1367 table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
1368 def_table o prop_of)
1369 o Nitpick_Intros.get) ctxt subst
1370 (* theory -> term list Inttab.table *)
1371 fun ground_theorem_table thy =
1372 fold ((fn @{const Trueprop} $ t1 =>
1373 is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
1374 | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
1376 val basic_ersatz_table =
1377 [(@{const_name prod_case}, @{const_name split}),
1378 (@{const_name card}, @{const_name card'}),
1379 (@{const_name setsum}, @{const_name setsum'}),
1380 (@{const_name fold_graph}, @{const_name fold_graph'}),
1381 (@{const_name wf}, @{const_name wf'}),
1382 (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
1383 (@{const_name wfrec}, @{const_name wfrec'})]
1385 (* theory -> (string * string) list *)
1386 fun ersatz_table thy =
1387 fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
1389 (* const_table Unsynchronized.ref -> string -> term list -> unit *)
1390 fun add_simps simp_table s eqs =
1391 Unsynchronized.change simp_table
1392 (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
1394 (* theory -> styp -> term list *)
1395 fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
1396 let val abs_T = domain_type T in
1397 typedef_info thy (fst (dest_Type abs_T)) |> the
1398 |> pairf #Abs_inverse #Rep_inverse
1399 |> pairself (Refute.specialize_type thy x o prop_of o the)
1402 (* theory -> string * typ list -> term list *)
1403 fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
1404 let val abs_T = Type abs_z in
1405 if is_univ_typedef thy abs_T then
1407 else case typedef_info thy abs_s of
1408 SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
1410 val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type
1411 val rep_t = Const (Rep_name, abs_T --> rep_T)
1412 val set_t = Const (set_name, rep_T --> bool_T)
1414 prop_of_Rep |> HOLogic.dest_Trueprop
1415 |> Refute.specialize_type thy (dest_Const rep_t)
1416 |> HOLogic.dest_mem |> snd
1418 [HOLogic.all_const abs_T
1419 $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
1420 |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
1421 |> map HOLogic.mk_Trueprop
1425 (* Proof.context -> string * typ list -> term list *)
1426 fun optimized_quot_type_axioms ctxt stds abs_z =
1428 val thy = ProofContext.theory_of ctxt
1429 val abs_T = Type abs_z
1430 val rep_T = rep_type_for_quot_type thy abs_T
1431 val equiv_rel = equiv_relation_for_quot_type thy abs_T
1432 val a_var = Var (("a", 0), abs_T)
1433 val x_var = Var (("x", 0), rep_T)
1434 val y_var = Var (("y", 0), rep_T)
1435 val x = (@{const_name Quot}, rep_T --> abs_T)
1436 val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
1437 val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
1438 val normal_x = normal_t $ x_var
1439 val normal_y = normal_t $ y_var
1440 val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
1442 [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t),
1444 ([@{const Not} $ (is_unknown_t $ normal_x),
1445 @{const Not} $ (is_unknown_t $ normal_y),
1446 equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
1447 Logic.mk_equals (normal_x, normal_y)),
1449 $ (HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)))
1450 $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
1453 (* theory -> (typ option * bool) list -> int * styp -> term *)
1454 fun constr_case_body thy stds (j, (x as (_, T))) =
1455 let val arg_Ts = binder_types T in
1456 list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
1457 (index_seq 0 (length arg_Ts)) arg_Ts)
1459 (* hol_context -> typ -> int * styp -> term -> term *)
1460 fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
1461 Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
1462 $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
1464 (* hol_context -> typ -> typ -> term *)
1465 fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
1467 val xs = datatype_constrs hol_ctxt dataT
1468 val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
1469 val (xs', x) = split_last xs
1471 constr_case_body thy stds (1, x)
1472 |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
1473 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
1476 (* hol_context -> string -> typ -> typ -> term -> term *)
1477 fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
1478 let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
1479 case no_of_record_field thy s rec_T of
1480 ~1 => (case rec_T of
1481 Type (_, Ts as _ :: _) =>
1483 val rec_T' = List.last Ts
1484 val j = num_record_fields thy rec_T - 1
1486 select_nth_constr_arg thy stds constr_x t j res_T
1487 |> optimized_record_get hol_ctxt s rec_T' res_T
1489 | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
1491 | j => select_nth_constr_arg thy stds constr_x t j res_T
1493 (* hol_context -> string -> typ -> term -> term -> term *)
1494 fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
1496 val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
1497 val Ts = binder_types constr_T
1499 val special_j = no_of_record_field thy s rec_T
1501 map2 (fn j => fn T =>
1502 let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
1503 if j = special_j then
1505 else if j = n - 1 andalso special_j = ~1 then
1506 optimized_record_update hol_ctxt s
1507 (rec_T |> dest_Type |> snd |> List.last) fun_t t
1510 end) (index_seq 0 n) Ts
1511 in list_comb (Const constr_x, ts) end
1513 (* theory -> const_table -> string * typ -> fixpoint_kind *)
1514 fun fixpoint_kind_of_const thy table x =
1515 if is_built_in_const thy [(NONE, false)] false x then
1518 fixpoint_kind_of_rhs (the (def_of_const thy table x))
1519 handle Option.Option => NoFp
1521 (* hol_context -> styp -> bool *)
1522 fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
1523 ...} : hol_context) x =
1524 fixpoint_kind_of_const thy def_table x <> NoFp andalso
1525 not (null (def_props_for_const thy stds fast_descrs intro_table x))
1526 fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
1527 ...} : hol_context) x =
1528 exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
1530 [!simp_table, psimp_table]
1531 fun is_inductive_pred hol_ctxt =
1532 is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
1533 fun is_equational_fun hol_ctxt =
1534 (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
1535 orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
1537 (* term * term -> term *)
1538 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
1539 | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
1540 | s_betapply p = betapply p
1541 (* term * term list -> term *)
1542 val s_betapplys = Library.foldl s_betapply
1545 fun lhs_of_equation t =
1547 Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1548 | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
1549 | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
1550 | @{const Trueprop} $ t1 => lhs_of_equation t1
1551 | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
1552 | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
1553 | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
1555 (* theory -> term -> bool *)
1556 fun is_constr_pattern _ (Bound _) = true
1557 | is_constr_pattern _ (Var _) = true
1558 | is_constr_pattern thy t =
1559 case strip_comb t of
1561 is_constr_like thy x andalso forall (is_constr_pattern thy) args
1563 fun is_constr_pattern_lhs thy t =
1564 forall (is_constr_pattern thy) (snd (strip_comb t))
1565 fun is_constr_pattern_formula thy t =
1566 case lhs_of_equation t of
1567 SOME t' => is_constr_pattern_lhs thy t'
1570 (* Prevents divergence in case of cyclic or infinite definition dependencies. *)
1571 val unfold_max_depth = 255
1573 (* hol_context -> term -> term *)
1574 fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names,
1575 def_table, ground_thm_table, ersatz_table,
1578 (* int -> typ list -> term -> term *)
1579 fun do_term depth Ts t =
1581 (t0 as Const (@{const_name Int.number_class.number_of},
1582 Type ("fun", [_, ran_T]))) $ t1 =>
1583 ((if is_number_type thy ran_T then
1585 val j = t1 |> HOLogic.dest_numeral
1586 |> ran_T = nat_T ? Integer.max 0
1587 val s = numeral_prefix ^ signed_string_of_int j
1589 if is_integer_like_type ran_T then
1590 if is_standard_datatype thy stds ran_T then
1593 funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
1595 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
1598 handle TERM _ => raise SAME ()
1601 handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
1602 | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
1603 do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
1604 | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
1605 betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
1606 map (do_term depth Ts) [t1, t2])
1607 | Const (x as (@{const_name distinct},
1608 Type ("fun", [Type (@{type_name list}, [T']), _])))
1610 (t1 |> HOLogic.dest_list |> distinctness_formula T'
1611 handle TERM _ => do_const depth Ts t x [t1])
1612 | Const (x as (@{const_name If}, _)) $ t1 $ t2 $ t3 =>
1613 if is_ground_term t1 andalso
1614 exists (Pattern.matches thy o rpair t1)
1615 (Inttab.lookup_list ground_thm_table (hash_term t1)) then
1618 do_const depth Ts t x [t1, t2, t3]
1619 | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
1620 | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
1621 | Const x $ t1 => do_const depth Ts t x [t1]
1622 | Const x => do_const depth Ts t x []
1623 | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
1627 | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
1628 (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
1629 and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
1630 (Abs (Name.uu, body_type T,
1631 select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
1632 | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
1633 (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
1634 (* int -> typ list -> term -> styp -> term list -> term *)
1635 and do_const depth Ts t (x as (s, T)) ts =
1636 case AList.lookup (op =) ersatz_table s of
1638 do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
1642 if is_built_in_const thy stds fast_descrs x then
1644 else case AList.lookup (op =) case_names s of
1647 val (dataT, res_T) = nth_range_type n T
1648 |> pairf domain_type range_type
1650 (optimized_case_def hol_ctxt dataT res_T
1651 |> do_term (depth + 1) Ts, ts)
1654 if is_constr thy stds x then
1656 else if is_stale_constr thy x then
1657 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
1659 else if is_quot_abs_fun ctxt x then
1661 val rep_T = domain_type T
1662 val abs_T = range_type T
1664 (Abs (Name.uu, rep_T,
1665 Const (@{const_name Quot}, rep_T --> abs_T)
1666 $ (Const (quot_normal_name_for_type ctxt abs_T,
1667 rep_T --> rep_T) $ Bound 0)), ts)
1669 else if is_quot_rep_fun ctxt x then
1671 val abs_T = domain_type T
1672 val rep_T = range_type T
1673 val x' = (@{const_name Quot}, rep_T --> abs_T)
1674 in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end
1675 else if is_record_get thy x then
1677 0 => (do_term depth Ts (eta_expand Ts t 1), [])
1678 | _ => (optimized_record_get hol_ctxt s (domain_type T)
1679 (range_type T) (do_term depth Ts (hd ts)), tl ts)
1680 else if is_record_update thy x then
1682 2 => (optimized_record_update hol_ctxt
1683 (unsuffix Record.updateN s) (nth_range_type 2 T)
1684 (do_term depth Ts (hd ts))
1685 (do_term depth Ts (nth ts 1)), [])
1686 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
1687 else if is_rep_fun thy x then
1688 let val x' = mate_of_rep_fun thy x in
1689 if is_constr thy stds x' then
1690 select_nth_constr_arg_with_args depth Ts x' ts 0
1695 else if is_equational_fun hol_ctxt x then
1697 else case def_of_const thy def_table x of
1699 if depth > unfold_max_depth then
1700 raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
1701 "too many nested definitions (" ^
1702 string_of_int depth ^ ") while expanding " ^
1704 else if s = @{const_name wfrec'} then
1705 (do_term (depth + 1) Ts (betapplys (def, ts)), [])
1707 (do_term (depth + 1) Ts def, ts)
1708 | NONE => (Const x, ts)
1709 in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
1712 (* hol_context -> typ -> term list *)
1713 fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
1715 val xs = datatype_constrs hol_ctxt T
1716 val set_T = T --> bool_T
1717 val iter_T = @{typ bisim_iterator}
1718 val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
1719 val bisim_max = @{const bisim_iterator_max}
1720 val n_var = Var (("n", 0), iter_T)
1722 Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T)
1723 $ Abs ("m", iter_T, HOLogic.eq_const iter_T
1724 $ (suc_const iter_T $ Bound 0) $ n_var)
1725 val x_var = Var (("x", 0), T)
1726 val y_var = Var (("y", 0), T)
1727 (* styp -> int -> typ -> term *)
1728 fun nth_sub_bisim x n nth_T =
1729 (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
1730 else HOLogic.eq_const nth_T)
1731 $ select_nth_constr_arg thy stds x x_var n nth_T
1732 $ select_nth_constr_arg thy stds x y_var n nth_T
1734 fun case_func (x as (_, T)) =
1736 val arg_Ts = binder_types T
1738 discriminate_value hol_ctxt x y_var ::
1739 map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
1741 in List.foldr absdummy core_t arg_Ts end
1743 [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
1744 $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
1745 $ (betapplys (optimized_case_def hol_ctxt T bool_T,
1746 map case_func xs @ [x_var]))),
1747 HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
1748 $ (Const (@{const_name insert}, T --> set_T --> set_T)
1749 $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
1750 |> map HOLogic.mk_Trueprop
1753 exception NO_TRIPLE of unit
1755 (* theory -> styp -> term -> term list * term list * term *)
1756 fun triple_for_intro_rule thy x t =
1758 val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
1759 val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
1760 val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
1762 val is_good_head = curry (op =) (Const x) o head_of
1764 if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
1768 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
1770 (* indexname * typ -> term list -> term -> term -> term *)
1771 fun wf_constraint_for rel side concl main =
1773 val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
1774 tuple_for_args concl), Var rel)
1775 val t = List.foldl HOLogic.mk_imp core side
1776 val vars = filter (not_equal rel) (Term.add_vars t [])
1778 Library.foldl (fn (t', ((x, j), T)) =>
1780 $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
1784 (* indexname * typ -> term list * term list * term -> term *)
1785 fun wf_constraint_for_triple rel (side, main, concl) =
1786 map (wf_constraint_for rel side concl) main |> foldr1 s_conj
1788 (* Proof.context -> Time.time option -> thm
1789 -> (Proof.context -> tactic -> tactic) -> bool *)
1790 fun terminates_by ctxt timeout goal tac =
1791 can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
1792 #> SINGLE (DETERM_TIMEOUT timeout
1793 (tac ctxt (auto_tac (clasimpset_of ctxt))))
1794 #> the #> Goal.finish ctxt) goal
1796 val max_cached_wfs = 50
1797 val cached_timeout =
1798 Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
1799 val cached_wf_props =
1800 Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
1802 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
1803 ScnpReconstruct.sizechange_tac]
1805 (* hol_context -> const_table -> styp -> bool *)
1806 fun uncached_is_well_founded_inductive_pred
1807 ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
1808 : hol_context) (x as (_, T)) =
1809 case def_props_for_const thy stds fast_descrs intro_table x of
1810 [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
1813 (case map (triple_for_intro_rule thy x) intro_ts
1814 |> filter_out (null o #2) of
1818 val binders_T = HOLogic.mk_tupleT (binder_types T)
1819 val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
1820 val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
1821 val rel = (("R", j), rel_T)
1822 val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
1823 map (wf_constraint_for_triple rel) triples
1824 |> foldr1 s_conj |> HOLogic.mk_Trueprop
1825 val _ = if debug then
1826 priority ("Wellfoundedness goal: " ^
1827 Syntax.string_of_term ctxt prop ^ ".")
1831 if tac_timeout = Synchronized.value cached_timeout andalso
1832 length (Synchronized.value cached_wf_props) < max_cached_wfs then
1835 (Synchronized.change cached_wf_props (K []);
1836 Synchronized.change cached_timeout (K tac_timeout));
1837 case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
1841 val goal = prop |> cterm_of thy |> Goal.init
1842 val wf = exists (terminates_by ctxt tac_timeout goal)
1844 in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
1846 handle List.Empty => false | NO_TRIPLE () => false
1848 (* The type constraint below is a workaround for a Poly/ML crash. *)
1850 (* hol_context -> styp -> bool *)
1851 fun is_well_founded_inductive_pred
1852 (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
1854 case triple_lookup (const_match thy) wfs x of
1856 | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
1857 case AList.lookup (op =) (!wf_cache) x of
1861 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
1862 val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
1864 Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
1867 (* typ list -> typ -> term -> term *)
1868 fun ap_curry [_] _ t = t
1869 | ap_curry arg_Ts tuple_T t =
1870 let val n = length arg_Ts in
1871 list_abs (map (pair "c") arg_Ts,
1873 $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
1876 (* int -> term -> int *)
1877 fun num_occs_of_bound_in_term j (t1 $ t2) =
1878 op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
1879 | num_occs_of_bound_in_term j (Abs (_, _, t')) =
1880 num_occs_of_bound_in_term (j + 1) t'
1881 | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
1882 | num_occs_of_bound_in_term _ _ = 0
1885 val is_linear_inductive_pred_def =
1887 (* int -> term -> bool *)
1888 fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
1889 do_disjunct (j + 1) t2
1891 case num_occs_of_bound_in_term j t of
1893 | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
1896 fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
1897 let val (xs, body) = strip_abs t2 in
1900 | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
1902 | do_lfp_def _ = false
1903 in do_lfp_def o strip_abs_body end
1905 (* int -> int list list *)
1906 fun n_ptuple_paths 0 = []
1907 | n_ptuple_paths 1 = []
1908 | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
1909 (* int -> typ -> typ -> term -> term *)
1910 val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
1912 (* term -> term * term *)
1913 val linear_pred_base_and_step_rhss =
1916 fun aux (Const (@{const_name lfp}, _) $ t2) =
1918 val (xs, body) = strip_abs t2
1919 val arg_Ts = map snd (tl xs)
1920 val tuple_T = HOLogic.mk_tupleT arg_Ts
1921 val j = length arg_Ts
1922 (* int -> term -> term *)
1923 fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
1924 Const (@{const_name Ex}, T1)
1925 $ Abs (s2, T2, repair_rec (j + 1) t2')
1926 | repair_rec j (@{const "op &"} $ t1 $ t2) =
1927 @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
1929 let val (head, args) = strip_comb t in
1930 if head = Bound j then
1931 HOLogic.eq_const tuple_T $ Bound j
1932 $ mk_flat_tuple tuple_T args
1936 val (nonrecs, recs) =
1937 List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
1939 val base_body = nonrecs |> List.foldl s_disj @{const False}
1940 val step_body = recs |> map (repair_rec j)
1941 |> List.foldl s_disj @{const False}
1943 (list_abs (tl xs, incr_bv (~1, j, base_body))
1944 |> ap_n_split (length arg_Ts) tuple_T bool_T,
1945 Abs ("y", tuple_T, list_abs (tl xs, step_body)
1946 |> ap_n_split (length arg_Ts) tuple_T bool_T))
1949 raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
1952 (* hol_context -> styp -> term -> term *)
1953 fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
1955 val j = maxidx_of_term def + 1
1956 val (outer, fp_app) = strip_abs def
1957 val outer_bounds = map Bound (length outer - 1 downto 0)
1958 val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer
1959 val fp_app = subst_bounds (rev outer_vars, fp_app)
1960 val (outer_Ts, rest_T) = strip_n_binders (length outer) T
1961 val tuple_arg_Ts = strip_type rest_T |> fst
1962 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
1963 val set_T = tuple_T --> bool_T
1964 val curried_T = tuple_T --> set_T
1965 val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
1966 val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
1967 val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
1968 val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
1969 |> HOLogic.mk_Trueprop
1970 val _ = add_simps simp_table base_s [base_eq]
1971 val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T)
1972 val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs)
1973 |> HOLogic.mk_Trueprop
1974 val _ = add_simps simp_table step_s [step_eq]
1977 Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
1978 $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
1979 $ (Const (@{const_name split}, curried_T --> uncurried_T)
1980 $ list_comb (Const step_x, outer_bounds)))
1981 $ list_comb (Const base_x, outer_bounds)
1982 |> ap_curry tuple_arg_Ts tuple_T)
1983 |> unfold_defs_in_term hol_ctxt
1986 (* hol_context -> bool -> styp -> term *)
1987 fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
1988 def_table, simp_table, ...})
1991 val iter_T = iterator_type_for_const gfp x
1992 val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
1993 val unrolled_const = Const x' $ zero_const iter_T
1994 val def = the (def_of_const thy def_table x)
1996 if is_equational_fun hol_ctxt x' then
1997 unrolled_const (* already done *)
1998 else if not gfp andalso is_linear_inductive_pred_def def andalso
1999 star_linear_preds then
2000 starred_linear_pred_const hol_ctxt x def
2003 val j = maxidx_of_term def + 1
2004 val (outer, fp_app) = strip_abs def
2005 val outer_bounds = map Bound (length outer - 1 downto 0)
2006 val cur = Var ((iter_var_prefix, j + 1), iter_T)
2007 val next = suc_const iter_T $ cur
2008 val rhs = case fp_app of
2010 betapply (t, list_comb (Const x', next :: outer_bounds))
2011 | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
2013 val (inner, naked_rhs) = strip_abs rhs
2014 val all = outer @ inner
2015 val bounds = map Bound (length all - 1 downto 0)
2016 val vars = map (fn (s, T) => Var ((s, j), T)) all
2017 val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs)
2018 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
2019 val _ = add_simps simp_table s' [eq]
2020 in unrolled_const end
2023 (* hol_context -> styp -> term *)
2024 fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
2026 val def = the (def_of_const thy def_table x)
2027 val (outer, fp_app) = strip_abs def
2028 val outer_bounds = map Bound (length outer - 1 downto 0)
2029 val rhs = case fp_app of
2030 Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
2031 | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
2033 val (inner, naked_rhs) = strip_abs rhs
2034 val all = outer @ inner
2035 val bounds = map Bound (length all - 1 downto 0)
2036 val j = maxidx_of_term def + 1
2037 val vars = map (fn (s, T) => Var ((s, j), T)) all
2039 HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
2040 |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
2042 fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
2043 if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
2044 let val x' = (after_name_sep s, T) in
2045 raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
2048 raw_inductive_pred_axiom hol_ctxt x
2050 (* hol_context -> styp -> term list *)
2051 fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
2052 psimp_table, ...}) x =
2053 case def_props_for_const thy stds fast_descrs (!simp_table) x of
2054 [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
2055 [] => [inductive_pred_axiom hol_ctxt x]
2058 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
2059 (* hol_context -> styp -> bool *)
2060 fun is_equational_fun_surely_complete hol_ctxt x =
2061 case raw_equational_fun_axioms hol_ctxt x of
2062 [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
2063 strip_comb t1 |> snd |> forall is_Var
2066 (* term list -> term list *)
2067 fun merge_type_vars_in_terms ts =
2069 (* typ -> (sort * string) list -> (sort * string) list *)
2070 fun add_type (TFree (s, S)) table =
2071 (case AList.lookup (op =) table S of
2073 if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
2075 | NONE => (S, s) :: table)
2076 | add_type _ table = table
2077 val table = fold (fold_types (fold_atyps add_type)) ts []
2079 fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S)
2081 in map (map_types (map_atyps coalesce)) ts end
2083 (* hol_context -> bool -> typ -> typ list -> typ list *)
2084 fun add_ground_types hol_ctxt binarize =
2088 Type ("fun", Ts) => fold aux Ts accum
2089 | Type ("*", Ts) => fold aux Ts accum
2090 | Type (@{type_name itself}, [T1]) => aux T1 accum
2092 if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
2097 |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
2101 | _ => insert (op =) T accum
2104 (* hol_context -> bool -> typ -> typ list *)
2105 fun ground_types_in_type hol_ctxt binarize T =
2106 add_ground_types hol_ctxt binarize T []
2107 (* hol_context -> term list -> typ list *)
2108 fun ground_types_in_terms hol_ctxt binarize ts =
2109 fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
2111 (* theory -> const_table -> styp -> int list *)
2112 fun const_format thy def_table (x as (s, T)) =
2113 if String.isPrefix unrolled_prefix s then
2114 const_format thy def_table (original_name s, range_type T)
2115 else if String.isPrefix skolem_prefix s then
2117 val k = unprefix skolem_prefix s
2118 |> strip_first_name_sep |> fst |> space_explode "@"
2119 |> hd |> Int.fromString |> the
2120 in [k, num_binder_types T - k] end
2121 else if original_name s <> s then
2122 [num_binder_types T]
2123 else case def_of_const thy def_table x of
2124 SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
2125 let val k = length (strip_abs_vars t') in
2126 [k, num_binder_types T - k]
2129 [num_binder_types T]
2130 | NONE => [num_binder_types T]
2131 (* int list -> int list -> int list *)
2132 fun intersect_formats _ [] = []
2133 | intersect_formats [] _ = []
2134 | intersect_formats ks1 ks2 =
2135 let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
2136 intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
2137 (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
2141 (* theory -> const_table -> (term option * int list) list -> term -> int list *)
2142 fun lookup_format thy def_table formats t =
2143 case AList.lookup (fn (SOME x, SOME y) =>
2144 (term_match thy) (x, y) | _ => false)
2146 SOME format => format
2147 | NONE => let val format = the (AList.lookup (op =) formats NONE) in
2149 Const x => intersect_formats format
2150 (const_format thy def_table x)
2154 (* int list -> int list -> typ -> typ *)
2155 fun format_type default_format format T =
2157 val T = unarize_unbox_and_uniterize_type T
2158 val format = format |> filter (curry (op <) 0)
2160 if forall (curry (op =) 1) format then
2164 val (binder_Ts, body_T) = strip_type T
2167 |> map (format_type default_format default_format)
2168 |> rev |> chunk_list_unevenly (rev format)
2169 |> map (HOLogic.mk_tupleT o rev)
2170 in List.foldl (op -->) body_T batched end
2172 (* theory -> const_table -> (term option * int list) list -> term -> typ *)
2173 fun format_term_type thy def_table formats t =
2174 format_type (the (AList.lookup (op =) formats NONE))
2175 (lookup_format thy def_table formats t) (fastype_of t)
2177 (* int list -> int -> int list -> int list *)
2178 fun repair_special_format js m format =
2179 m - 1 downto 0 |> chunk_list_unevenly (rev format)
2180 |> map (rev o filter_out (member (op =) js))
2181 |> filter_out null |> map length |> rev
2183 (* hol_context -> string * string -> (term option * int list) list
2184 -> styp -> term * typ *)
2185 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
2186 : hol_context) (base_name, step_name) formats =
2188 val default_format = the (AList.lookup (op =) formats NONE)
2189 (* styp -> term * typ *)
2190 fun do_const (x as (s, T)) =
2191 (if String.isPrefix special_prefix s then
2194 val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
2195 val (x' as (_, T'), js, ts) =
2196 AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
2198 val max_j = List.last js
2199 val Ts = List.take (binder_types T', max_j + 1)
2200 val missing_js = filter_out (member (op =) js) (0 upto max_j)
2201 val missing_Ts = filter_indices missing_js Ts
2202 (* int -> indexname *)
2203 fun nth_missing_var n =
2204 ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
2205 val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
2206 val vars = special_bounds ts @ missing_vars
2209 case AList.lookup (op =) (js ~~ ts) j of
2212 Var (nth missing_vars
2213 (find_index (curry (op =) j) missing_js)))
2215 val t = do_const x' |> fst
2217 case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
2218 | _ => false) formats (SOME t) of
2220 repair_special_format js (num_binder_types T') format
2222 const_format thy def_table x'
2223 |> repair_special_format js (num_binder_types T')
2224 |> intersect_formats default_format
2226 (list_comb (t, ts') |> fold_rev abs_var vars,
2227 format_type default_format format T)
2229 else if String.isPrefix uncurry_prefix s then
2231 val (ss, s') = unprefix uncurry_prefix s
2232 |> strip_first_name_sep |>> space_explode "@"
2234 if String.isPrefix step_prefix s' then
2238 val k = the (Int.fromString (hd ss))
2239 val j = the (Int.fromString (List.last ss))
2240 val (before_Ts, (tuple_T, rest_T)) =
2241 strip_n_binders j T ||> (strip_n_binders 1 #>> hd)
2242 val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T
2243 in do_const (s', T') end
2245 else if String.isPrefix unrolled_prefix s then
2246 let val t = Const (original_name s, range_type T) in
2247 (lambda (Free (iter_var_prefix, nat_T)) t,
2248 format_type default_format
2249 (lookup_format thy def_table formats t) T)
2251 else if String.isPrefix base_prefix s then
2252 (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
2253 format_type default_format default_format T)
2254 else if String.isPrefix step_prefix s then
2255 (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
2256 format_type default_format default_format T)
2257 else if String.isPrefix quot_normal_prefix s then
2258 let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in
2259 (t, format_term_type thy def_table formats t)
2261 else if String.isPrefix skolem_prefix s then
2263 val ss = the (AList.lookup (op =) (!skolems) s)
2264 val (Ts, Ts') = chop (length ss) (binder_types T)
2265 val frees = map Free (ss ~~ Ts)
2266 val s' = original_name s
2268 (fold lambda frees (Const (s', Ts' ---> T)),
2269 format_type default_format
2270 (lookup_format thy def_table formats (Const x)) T)
2272 else if String.isPrefix eval_prefix s then
2274 val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
2275 in (t, format_term_type thy def_table formats t) end
2276 else if s = @{const_name undefined_fast_The} then
2277 (Const (nitpick_prefix ^ "The fallback", T),
2278 format_type default_format
2279 (lookup_format thy def_table formats
2280 (Const (@{const_name The}, (T --> bool_T) --> T))) T)
2281 else if s = @{const_name undefined_fast_Eps} then
2282 (Const (nitpick_prefix ^ "Eps fallback", T),
2283 format_type default_format
2284 (lookup_format thy def_table formats
2285 (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
2287 let val t = Const (original_name s, T) in
2288 (t, format_term_type thy def_table formats t)
2290 |>> map_types unarize_unbox_and_uniterize_type
2291 |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
2294 (* styp -> string *)
2295 fun assign_operator_for_const (s, T) =
2296 if String.isPrefix ubfp_prefix s then
2297 if is_fun_type T then "\<subseteq>" else "\<le>"
2298 else if String.isPrefix lbfp_prefix s then
2299 if is_fun_type T then "\<supseteq>" else "\<ge>"
2300 else if original_name s <> s then
2301 assign_operator_for_const (after_name_sep s, T)