1 (* Title: HOL/Tools/ATP/atp_problem_generate.ML
2 Author: Fabian Immler, TU Muenchen
4 Author: Jasmin Blanchette, TU Muenchen
6 Translation of HOL to FOL for Metis and Sledgehammer.
9 signature ATP_PROBLEM_GENERATE =
11 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
12 type connective = ATP_Problem.connective
13 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
14 type atp_format = ATP_Problem.atp_format
15 type formula_kind = ATP_Problem.formula_kind
16 type 'a problem = 'a ATP_Problem.problem
18 datatype scope = Global | Local | Assum | Chained
19 datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
20 type stature = scope * status
22 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
23 datatype strictness = Strict | Non_Strict
24 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
27 Noninf_Nonmono_Types of strictness * granularity |
28 Fin_Nonmono_Types of granularity |
33 val type_tag_idempotence : bool Config.T
34 val type_tag_arguments : bool Config.T
36 val hide_lamsN : string
39 val combs_and_liftingN : string
40 val combs_or_liftingN : string
41 val lam_liftingN : string
42 val keep_lamsN : string
43 val schematic_var_prefix : string
44 val fixed_var_prefix : string
45 val tvar_prefix : string
46 val tfree_prefix : string
47 val const_prefix : string
48 val type_const_prefix : string
49 val class_prefix : string
50 val lam_lifted_prefix : string
51 val lam_lifted_mono_prefix : string
52 val lam_lifted_poly_prefix : string
53 val skolem_const_prefix : string
54 val old_skolem_const_prefix : string
55 val new_skolem_const_prefix : string
56 val combinator_prefix : string
57 val type_decl_prefix : string
58 val sym_decl_prefix : string
59 val guards_sym_formula_prefix : string
60 val tags_sym_formula_prefix : string
61 val fact_prefix : string
62 val conjecture_prefix : string
63 val helper_prefix : string
64 val class_rel_clause_prefix : string
65 val arity_clause_prefix : string
66 val tfree_clause_prefix : string
67 val lam_fact_prefix : string
68 val typed_helper_suffix : string
69 val untyped_helper_suffix : string
70 val type_tag_idempotence_helper_name : string
71 val predicator_name : string
72 val app_op_name : string
73 val type_guard_name : string
74 val type_tag_name : string
75 val native_type_prefix : string
76 val prefixed_predicator_name : string
77 val prefixed_app_op_name : string
78 val prefixed_type_tag_name : string
79 val ascii_of : string -> string
80 val unascii_of : string -> string
81 val unprefix_and_unascii : string -> string -> string option
82 val proxy_table : (string * (string * (thm * (string * string)))) list
83 val proxify_const : string -> (string * string) option
84 val invert_const : string -> string
85 val unproxify_const : string -> string
86 val new_skolem_var_name_from_const : string -> string
87 val atp_irrelevant_consts : string list
88 val atp_schematic_consts_of : term -> typ list Symtab.table
89 val is_type_enc_higher_order : type_enc -> bool
90 val polymorphism_of_type_enc : type_enc -> polymorphism
91 val level_of_type_enc : type_enc -> type_level
92 val is_type_enc_quasi_sound : type_enc -> bool
93 val is_type_enc_fairly_sound : type_enc -> bool
94 val type_enc_from_string : strictness -> string -> type_enc
95 val adjust_type_enc : atp_format -> type_enc -> type_enc
97 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
98 val unmangled_const : string -> string * (string, 'b) ho_term list
99 val unmangled_const_name : string -> string list
100 val helper_table : ((string * bool) * thm list) list
101 val trans_lams_from_string :
102 Proof.context -> type_enc -> string -> term list -> term list * term list
104 val prepare_atp_problem :
105 Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
106 -> bool -> string -> bool -> bool -> bool -> term list -> term
107 -> ((string * stature) * term) list
108 -> string problem * string Symtab.table * (string * stature) list vector
109 * (string * term) list * int Symtab.table
110 val atp_problem_weights : string problem -> (string * real) list
113 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
119 type name = string * string
121 val type_tag_idempotence =
122 Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
123 val type_tag_arguments =
124 Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
126 val no_lamsN = "no_lams" (* used internally; undocumented *)
127 val hide_lamsN = "hide_lams"
128 val liftingN = "lifting"
130 val combs_and_liftingN = "combs_and_lifting"
131 val combs_or_liftingN = "combs_or_lifting"
132 val keep_lamsN = "keep_lams"
133 val lam_liftingN = "lam_lifting" (* legacy *)
135 (* It's still unclear whether all TFF1 implementations will support type
136 signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
137 val avoid_first_order_ghost_type_vars = false
139 val bound_var_prefix = "B_"
140 val all_bound_var_prefix = "BA_"
141 val exist_bound_var_prefix = "BE_"
142 val schematic_var_prefix = "V_"
143 val fixed_var_prefix = "v_"
144 val tvar_prefix = "T_"
145 val tfree_prefix = "t_"
146 val const_prefix = "c_"
147 val type_const_prefix = "tc_"
148 val native_type_prefix = "n_"
149 val class_prefix = "cl_"
151 (* Freshness almost guaranteed! *)
152 val atp_prefix = "ATP" ^ Long_Name.separator
153 val atp_weak_prefix = "ATP:"
155 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
156 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
157 val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
159 val skolem_const_prefix = atp_prefix ^ "Sko"
160 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
161 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
163 val combinator_prefix = "COMB"
165 val type_decl_prefix = "ty_"
166 val sym_decl_prefix = "sy_"
167 val guards_sym_formula_prefix = "gsy_"
168 val tags_sym_formula_prefix = "tsy_"
169 val uncurried_alias_eq_prefix = "unc_"
170 val fact_prefix = "fact_"
171 val conjecture_prefix = "conj_"
172 val helper_prefix = "help_"
173 val class_rel_clause_prefix = "clar_"
174 val arity_clause_prefix = "arity_"
175 val tfree_clause_prefix = "tfree_"
177 val lam_fact_prefix = "ATP.lambda_"
178 val typed_helper_suffix = "_T"
179 val untyped_helper_suffix = "_U"
180 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
182 val predicator_name = "pp"
183 val app_op_name = "aa"
184 val type_guard_name = "gg"
185 val type_tag_name = "tt"
187 val prefixed_predicator_name = const_prefix ^ predicator_name
188 val prefixed_app_op_name = const_prefix ^ app_op_name
189 val prefixed_type_tag_name = const_prefix ^ type_tag_name
191 (*Escaping of special characters.
192 Alphanumeric characters are left unchanged.
193 The character _ goes to __
194 Characters in the range ASCII space to / go to _A to _P, respectively.
195 Other characters go to _nnn where nnn is the decimal ASCII code.*)
196 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
198 fun stringN_of_int 0 _ = ""
199 | stringN_of_int k n =
200 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
202 fun ascii_of_char c =
203 if Char.isAlphaNum c then
205 else if c = #"_" then
207 else if #" " <= c andalso c <= #"/" then
208 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
210 (* fixed width, in case more digits follow *)
211 "_" ^ stringN_of_int 3 (Char.ord c)
213 val ascii_of = String.translate ascii_of_char
215 (** Remove ASCII armoring from names in proof files **)
217 (* We don't raise error exceptions because this code can run inside a worker
218 thread. Also, the errors are impossible. *)
221 fun un rcs [] = String.implode(rev rcs)
222 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
223 (* Three types of _ escapes: __, _A to _P, _nnn *)
224 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
225 | un rcs (#"_" :: c :: cs) =
226 if #"A" <= c andalso c<= #"P" then
227 (* translation of #" " to #"/" *)
228 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
230 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
231 case Int.fromString (String.implode digits) of
232 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
233 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
235 | un rcs (c :: cs) = un (c :: rcs) cs
236 in un [] o String.explode end
238 (* If string s has the prefix s1, return the result of deleting it,
240 fun unprefix_and_unascii s1 s =
241 if String.isPrefix s1 s then
242 SOME (unascii_of (String.extract (s, size s1, NONE)))
247 [("c_False", (@{const_name False}, (@{thm fFalse_def},
248 ("fFalse", @{const_name ATP.fFalse})))),
249 ("c_True", (@{const_name True}, (@{thm fTrue_def},
250 ("fTrue", @{const_name ATP.fTrue})))),
251 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
252 ("fNot", @{const_name ATP.fNot})))),
253 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
254 ("fconj", @{const_name ATP.fconj})))),
255 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
256 ("fdisj", @{const_name ATP.fdisj})))),
257 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
258 ("fimplies", @{const_name ATP.fimplies})))),
259 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
260 ("fequal", @{const_name ATP.fequal})))),
261 ("c_All", (@{const_name All}, (@{thm fAll_def},
262 ("fAll", @{const_name ATP.fAll})))),
263 ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
264 ("fEx", @{const_name ATP.fEx}))))]
266 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
268 (* Readable names for the more common symbolic functions. Do not mess with the
269 table unless you know what you are doing. *)
270 val const_trans_table =
271 [(@{type_name Product_Type.prod}, "prod"),
272 (@{type_name Sum_Type.sum}, "sum"),
273 (@{const_name False}, "False"),
274 (@{const_name True}, "True"),
275 (@{const_name Not}, "Not"),
276 (@{const_name conj}, "conj"),
277 (@{const_name disj}, "disj"),
278 (@{const_name implies}, "implies"),
279 (@{const_name HOL.eq}, "equal"),
280 (@{const_name All}, "All"),
281 (@{const_name Ex}, "Ex"),
282 (@{const_name If}, "If"),
283 (@{const_name Set.member}, "member"),
284 (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
285 (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
286 (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
287 (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
288 (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
290 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
292 (* Invert the table of translations between Isabelle and ATPs. *)
293 val const_trans_table_inv =
294 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
295 val const_trans_table_unprox =
297 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
299 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
300 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
303 case Symtab.lookup const_trans_table c of
307 fun ascii_of_indexname (v, 0) = ascii_of v
308 | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
310 fun make_bound_var x = bound_var_prefix ^ ascii_of x
311 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
312 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
313 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
314 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
316 fun make_schematic_type_var (x, i) =
317 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
318 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
320 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
322 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
323 fun default c = const_prefix ^ lookup_const c
325 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
326 | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
327 if c = choice_const then tptp_choice else default c
328 | make_fixed_const _ c = default c
331 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
333 fun make_type_class clas = class_prefix ^ ascii_of clas
335 fun new_skolem_var_name_from_const s =
336 let val ss = s |> space_explode Long_Name.separator in
337 nth ss (length ss - 2)
340 (* These are either simplified away by "Meson.presimplify" (most of the time) or
341 handled specially via "fFalse", "fTrue", ..., "fequal". *)
342 val atp_irrelevant_consts =
343 [@{const_name False}, @{const_name True}, @{const_name Not},
344 @{const_name conj}, @{const_name disj}, @{const_name implies},
345 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
347 val atp_monomorph_bad_consts =
348 atp_irrelevant_consts @
349 (* These are ignored anyway by the relevance filter (unless they appear in
350 higher-order places) but not by the monomorphizer. *)
351 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
352 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
353 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
355 fun add_schematic_const (x as (_, T)) =
356 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
357 val add_schematic_consts_of =
358 Term.fold_aterms (fn Const (x as (s, _)) =>
359 not (member (op =) atp_monomorph_bad_consts s)
360 ? add_schematic_const x
362 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
364 (** Definitions and functions for FOL clauses and formulas for TPTP **)
366 (** Isabelle arities **)
368 type arity_atom = name * name * name list
370 val type_class = the_single @{sort type}
374 prem_atoms : arity_atom list,
375 concl_atom : arity_atom}
377 fun add_prem_atom tvar =
378 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
380 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
381 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
383 val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
384 val tvars_srts = ListPair.zip (tvars, args)
387 prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
388 concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
392 fun arity_clause _ _ (_, []) = []
393 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
394 arity_clause seen n (tcons, ars)
395 | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
396 if member (op =) seen class then
397 (* multiple arities for the same (tycon, class) pair *)
398 make_axiom_arity_clause (tcons,
399 lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
401 arity_clause seen (n + 1) (tcons, ars)
403 make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
404 ascii_of class, ar) ::
405 arity_clause (class :: seen) n (tcons, ars)
407 fun multi_arity_clause [] = []
408 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
409 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
411 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
412 theory thy provided its arguments have the corresponding sorts. *)
413 fun type_class_pairs thy tycons classes =
415 val alg = Sign.classes_of thy
416 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
417 fun add_class tycon class =
418 cons (class, domain_sorts tycon class)
419 handle Sorts.CLASS_ERROR _ => I
420 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
421 in map try_classes tycons end
423 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
424 fun iter_type_class_pairs _ _ [] = ([], [])
425 | iter_type_class_pairs thy tycons classes =
427 fun maybe_insert_class s =
428 (s <> type_class andalso not (member (op =) classes s))
430 val cpairs = type_class_pairs thy tycons classes
432 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
433 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
434 in (classes' @ classes, union (op =) cpairs' cpairs) end
436 fun make_arity_clauses thy tycons =
437 iter_type_class_pairs thy tycons ##> multi_arity_clause
440 (** Isabelle class relations **)
442 type class_rel_clause =
447 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
449 fun class_pairs _ [] _ = []
450 | class_pairs thy subs supers =
452 val class_less = Sorts.class_less (Sign.classes_of thy)
453 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
454 fun add_supers sub = fold (add_super sub) supers
455 in fold add_supers subs [] end
457 fun make_class_rel_clause (sub, super) =
458 {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
459 superclass = `make_type_class super}
461 fun make_class_rel_clauses thy subs supers =
462 map make_class_rel_clause (class_pairs thy subs supers)
464 (* intermediate terms *)
466 IConst of name * typ * typ list |
468 IApp of iterm * iterm |
469 IAbs of (name * typ) * iterm
471 fun ityp_of (IConst (_, T, _)) = T
472 | ityp_of (IVar (_, T)) = T
473 | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
474 | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
476 (*gets the head of a combinator application, along with the list of arguments*)
477 fun strip_iterm_comb u =
479 fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
481 in stripc (u, []) end
483 fun atomic_types_of T = fold_atyps (insert (op =)) T []
485 val tvar_a_str = "'a"
486 val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
487 val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
488 val itself_name = `make_fixed_type_const @{type_name itself}
489 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
490 val tvar_a_atype = AType (tvar_a_name, [])
491 val a_itself_atype = AType (itself_name, [tvar_a_atype])
493 fun new_skolem_const_name s num_T_args =
494 [new_skolem_const_prefix, s, string_of_int num_T_args]
495 |> space_implode Long_Name.separator
497 fun robust_const_type thy s =
498 if s = app_op_name then
499 Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
500 else if String.isPrefix lam_lifted_prefix s then
501 Logic.varifyT_global @{typ "'a => 'b"}
503 (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
504 s |> Sign.the_const_type thy
506 (* This function only makes sense if "T" is as general as possible. *)
507 fun robust_const_typargs thy (s, T) =
508 if s = app_op_name then
509 let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
510 else if String.isPrefix old_skolem_const_prefix s then
511 [] |> Term.add_tvarsT T |> rev |> map TVar
512 else if String.isPrefix lam_lifted_prefix s then
513 if String.isPrefix lam_lifted_poly_prefix s then
514 let val (T1, T2) = T |> dest_funT in [T1, T2] end
518 (s, T) |> Sign.const_typargs thy
520 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
521 Also accumulates sort infomation. *)
522 fun iterm_from_term thy format bs (P $ Q) =
524 val (P', P_atomics_Ts) = iterm_from_term thy format bs P
525 val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
526 in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
527 | iterm_from_term thy format _ (Const (c, T)) =
528 (IConst (`(make_fixed_const (SOME format)) c, T,
529 robust_const_typargs thy (c, T)),
531 | iterm_from_term _ _ _ (Free (s, T)) =
532 (IConst (`make_fixed_var s, T, []), atomic_types_of T)
533 | iterm_from_term _ format _ (Var (v as (s, _), T)) =
534 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
536 val Ts = T |> strip_type |> swap |> op ::
537 val s' = new_skolem_const_name s (length Ts)
538 in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
540 IVar ((make_schematic_var v, s), T), atomic_types_of T)
541 | iterm_from_term _ _ bs (Bound j) =
542 nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
543 | iterm_from_term thy format bs (Abs (s, T, t)) =
545 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
547 val name = `make_bound_var s
548 val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
549 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
551 datatype scope = Global | Local | Assum | Chained
552 datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
553 type stature = scope * status
555 datatype order = First_Order | Higher_Order
556 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
557 datatype strictness = Strict | Non_Strict
558 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
559 datatype type_level =
561 Noninf_Nonmono_Types of strictness * granularity |
562 Fin_Nonmono_Types of granularity |
567 Simple_Types of order * polymorphism * type_level |
568 Guards of polymorphism * type_level |
569 Tags of polymorphism * type_level
571 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
572 | is_type_enc_higher_order _ = false
574 fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
575 | polymorphism_of_type_enc (Guards (poly, _)) = poly
576 | polymorphism_of_type_enc (Tags (poly, _)) = poly
578 fun level_of_type_enc (Simple_Types (_, _, level)) = level
579 | level_of_type_enc (Guards (_, level)) = level
580 | level_of_type_enc (Tags (_, level)) = level
582 fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
583 | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
584 | granularity_of_type_level _ = All_Vars
586 fun is_type_level_quasi_sound All_Types = true
587 | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
588 | is_type_level_quasi_sound _ = false
589 val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
591 fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
592 | is_type_level_fairly_sound level = is_type_level_quasi_sound level
593 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
595 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
596 | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
597 | is_type_level_monotonicity_based _ = false
599 (* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
601 val queries = ["?", "_query"]
602 val bangs = ["!", "_bang"]
603 val ats = ["@", "_at"]
605 fun try_unsuffixes ss s =
606 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
608 fun try_nonmono constr suffixes fallback s =
609 case try_unsuffixes suffixes s of
611 (case try_unsuffixes suffixes s of
612 SOME s => (constr Positively_Naked_Vars, s)
614 case try_unsuffixes ats s of
615 SOME s => (constr Ghost_Type_Arg_Vars, s)
616 | NONE => (constr All_Vars, s))
619 fun type_enc_from_string strictness s =
620 (case try (unprefix "poly_") s of
621 SOME s => (SOME Polymorphic, s)
623 case try (unprefix "raw_mono_") s of
624 SOME s => (SOME Raw_Monomorphic, s)
626 case try (unprefix "mono_") s of
627 SOME s => (SOME Mangled_Monomorphic, s)
630 |> try_nonmono Fin_Nonmono_Types bangs
631 |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
632 |> (fn (poly, (level, core)) =>
633 case (core, (poly, level)) of
634 ("native", (SOME poly, _)) =>
635 (case (poly, level) of
636 (Polymorphic, All_Types) =>
637 Simple_Types (First_Order, Polymorphic, All_Types)
638 | (Mangled_Monomorphic, _) =>
639 if granularity_of_type_level level = All_Vars then
640 Simple_Types (First_Order, Mangled_Monomorphic, level)
643 | _ => raise Same.SAME)
644 | ("native_higher", (SOME poly, _)) =>
645 (case (poly, level) of
646 (Polymorphic, All_Types) =>
647 Simple_Types (Higher_Order, Polymorphic, All_Types)
648 | (_, Noninf_Nonmono_Types _) => raise Same.SAME
649 | (Mangled_Monomorphic, _) =>
650 if granularity_of_type_level level = All_Vars then
651 Simple_Types (Higher_Order, Mangled_Monomorphic, level)
654 | _ => raise Same.SAME)
655 | ("guards", (SOME poly, _)) =>
656 if poly = Mangled_Monomorphic andalso
657 granularity_of_type_level level = Ghost_Type_Arg_Vars then
661 | ("tags", (SOME poly, _)) =>
662 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
666 | ("args", (SOME poly, All_Types (* naja *))) =>
667 Guards (poly, Const_Arg_Types)
668 | ("erased", (NONE, All_Types (* naja *))) =>
669 Guards (Polymorphic, No_Types)
670 | _ => raise Same.SAME)
671 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
673 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
674 (Simple_Types (order, _, level)) =
675 Simple_Types (order, Mangled_Monomorphic, level)
676 | adjust_type_enc (THF _) type_enc = type_enc
677 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
678 Simple_Types (First_Order, Mangled_Monomorphic, level)
679 | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
680 Simple_Types (First_Order, Mangled_Monomorphic, level)
681 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
682 Simple_Types (First_Order, poly, level)
683 | adjust_type_enc format (Simple_Types (_, poly, level)) =
684 adjust_type_enc format (Guards (poly, level))
685 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
686 (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
687 | adjust_type_enc _ type_enc = type_enc
689 fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
690 | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
691 | constify_lifted (Free (x as (s, _))) =
692 (if String.isPrefix lam_lifted_prefix s then Const else Free) x
693 | constify_lifted t = t
695 (* Requires bound variables not to clash with any schematic variables (as should
696 be the case right after lambda-lifting). *)
697 fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
698 (case try unprefix s of
701 val names = Name.make_context (map fst (Term.add_var_names t' []))
702 val (s, _) = Name.variant s names
703 in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end
707 fun lift_lams_part_1 ctxt type_enc =
708 map close_form #> rpair ctxt
709 #-> Lambda_Lifting.lift_lambdas
710 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
711 lam_lifted_poly_prefix
713 lam_lifted_mono_prefix) ^ "_a"))
714 Lambda_Lifting.is_quantifier
716 fun lift_lams_part_2 (facts, lifted) =
717 (map (open_form (unprefix close_form_prefix) o constify_lifted) facts,
718 map (open_form I o constify_lifted) lifted)
719 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1
721 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
723 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
725 fun lam T t = Abs (Name.uu, T, t)
726 val (head, args) = strip_comb t ||> rev
727 val head_T = fastype_of head
729 val arg_Ts = head_T |> binder_types |> take n |> rev
730 val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
731 in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
732 | intentionalize_def t = t
734 type translated_formula =
738 iformula : (name, typ, iterm) formula,
739 atomic_types : typ list}
741 fun update_iformula f ({name, stature, kind, iformula, atomic_types}
742 : translated_formula) =
743 {name = name, stature = stature, kind = kind, iformula = f iformula,
744 atomic_types = atomic_types} : translated_formula
746 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
748 fun insert_type ctxt get_T x xs =
749 let val T = get_T x in
750 if exists (type_instance ctxt T o get_T) xs then xs
751 else x :: filter_out (type_generalization ctxt T o get_T) xs
754 (* The Booleans indicate whether all type arguments should be kept. *)
755 datatype type_arg_policy =
756 Explicit_Type_Args of bool (* infer_from_term_args *) |
760 fun type_arg_policy monom_constrs type_enc s =
761 let val poly = polymorphism_of_type_enc type_enc in
762 if s = type_tag_name then
763 if poly = Mangled_Monomorphic then Mangled_Type_Args
764 else Explicit_Type_Args false
765 else case type_enc of
766 Simple_Types (_, Polymorphic, _) => Explicit_Type_Args false
767 | Tags (_, All_Types) => No_Type_Args
769 let val level = level_of_type_enc type_enc in
770 if level = No_Types orelse s = @{const_name HOL.eq} orelse
771 (s = app_op_name andalso level = Const_Arg_Types) then
773 else if poly = Mangled_Monomorphic then
775 else if member (op =) monom_constrs s andalso
776 granularity_of_type_level level = Positively_Naked_Vars then
780 (level = All_Types orelse
781 granularity_of_type_level level = Ghost_Type_Arg_Vars)
785 (* Make atoms for sorted type variables. *)
786 fun generic_add_sorts_on_type (_, []) = I
787 | generic_add_sorts_on_type ((x, i), s :: ss) =
788 generic_add_sorts_on_type ((x, i), ss)
789 #> (if s = the_single @{sort HOL.type} then
792 insert (op =) (`make_type_class s, `make_fixed_type_var x)
794 insert (op =) (`make_type_class s,
795 (make_schematic_type_var (x, i), x)))
796 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
797 | add_sorts_on_tfree _ = I
798 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
799 | add_sorts_on_tvar _ = I
801 fun type_class_formula type_enc class arg =
802 AAtom (ATerm (class, arg ::
804 Simple_Types (First_Order, Polymorphic, _) =>
805 if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
808 fun formulas_for_types type_enc add_sorts_on_typ Ts =
809 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
810 |> map (fn (class, name) =>
811 type_class_formula type_enc class (ATerm (name, [])))
813 fun mk_aconns c phis =
814 let val (phis', phi') = split_last phis in
815 fold_rev (mk_aconn c) phis' phi'
817 fun mk_ahorn [] phi = phi
818 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
819 fun mk_aquant _ [] phi = phi
820 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
821 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
822 | mk_aquant q xs phi = AQuant (q, xs, phi)
824 fun close_universally add_term_vars phi =
826 fun add_formula_vars bounds (AQuant (_, xs, phi)) =
827 add_formula_vars (map fst xs @ bounds) phi
828 | add_formula_vars bounds (AConn (_, phis)) =
829 fold (add_formula_vars bounds) phis
830 | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
831 in mk_aquant AForall (add_formula_vars [] phi []) phi end
833 fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
834 (if is_tptp_variable s andalso
835 not (String.isPrefix tvar_prefix s) andalso
836 not (member (op =) bounds name) then
837 insert (op =) (name, NONE)
840 #> fold (add_term_vars bounds) tms
841 | add_term_vars bounds (AAbs ((name, _), tm)) =
842 add_term_vars (name :: bounds) tm
843 fun close_formula_universally phi = close_universally add_term_vars phi
845 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
846 fold (add_iterm_vars bounds) [tm1, tm2]
847 | add_iterm_vars _ (IConst _) = I
848 | add_iterm_vars bounds (IVar (name, T)) =
849 not (member (op =) bounds name) ? insert (op =) (name, SOME T)
850 | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
851 fun close_iformula_universally phi = close_universally add_iterm_vars phi
853 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
854 val fused_infinite_type = Type (fused_infinite_type_name, [])
856 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
858 fun ho_term_from_typ format type_enc =
860 fun term (Type (s, Ts)) =
861 ATerm (case (is_type_enc_higher_order type_enc, s) of
862 (true, @{type_name bool}) => `I tptp_bool_type
863 | (true, @{type_name fun}) => `I tptp_fun_type
864 | _ => if s = fused_infinite_type_name andalso
865 is_format_typed format then
866 `I tptp_individual_type
868 `make_fixed_type_const s,
870 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
871 | term (TVar (x, _)) = ATerm (tvar_name x, [])
874 fun ho_term_for_type_arg format type_enc T =
875 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
877 (* This shouldn't clash with anything else. *)
878 val uncurried_alias_sep = "\000"
879 val mangled_type_sep = "\001"
881 val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
883 fun generic_mangled_type_name f (ATerm (name, [])) = f name
884 | generic_mangled_type_name f (ATerm (name, tys)) =
885 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
887 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
889 fun mangled_type format type_enc =
890 generic_mangled_type_name fst o ho_term_from_typ format type_enc
892 fun make_native_type s =
893 if s = tptp_bool_type orelse s = tptp_fun_type orelse
894 s = tptp_individual_type then
897 native_type_prefix ^ ascii_of s
899 fun ho_type_from_ho_term type_enc pred_sym ary =
901 fun to_mangled_atype ty =
902 AType ((make_native_type (generic_mangled_type_name fst ty),
903 generic_mangled_type_name snd ty), [])
904 fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
905 | to_poly_atype _ = raise Fail "unexpected type abstraction"
907 if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
908 else to_mangled_atype
909 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
910 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
911 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
912 | to_fo _ _ = raise Fail "unexpected type abstraction"
913 fun to_ho (ty as ATerm ((s, _), tys)) =
914 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
915 | to_ho _ = raise Fail "unexpected type abstraction"
916 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
918 fun ho_type_from_typ format type_enc pred_sym ary =
919 ho_type_from_ho_term type_enc pred_sym ary
920 o ho_term_from_typ format type_enc
922 fun aliased_uncurried ary (s, s') =
923 (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
924 fun unaliased_uncurried (s, s') =
925 case space_explode uncurried_alias_sep s of
927 | [s1, s2] => (s1, unsuffix s2 s')
928 | _ => raise Fail "ill-formed explicit application alias"
930 fun raw_mangled_const_name type_name ty_args (s, s') =
932 fun type_suffix f g =
933 fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
935 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
936 fun mangled_const_name format type_enc =
937 map_filter (ho_term_for_type_arg format type_enc)
938 #> raw_mangled_const_name generic_mangled_type_name
940 val parse_mangled_ident =
941 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
943 fun parse_mangled_type x =
945 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
947 and parse_mangled_types x =
948 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
950 fun unmangled_type s =
951 s |> suffix ")" |> raw_explode
952 |> Scan.finite Symbol.stopper
953 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
954 quote s)) parse_mangled_type))
957 fun unmangled_const_name s =
958 (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
959 fun unmangled_const s =
960 let val ss = unmangled_const_name s in
961 (hd ss, map unmangled_type (tl ss))
964 fun introduce_proxies_in_iterm type_enc =
966 fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
967 | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
969 (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
970 limitation. This works in conjuction with special code in
971 "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
974 IApp (IConst (`I ho_quant, T, []),
976 IApp (IConst (`I "P", p_T, []),
977 IConst (`I "X", x_T, [])))))
978 | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
979 fun intro top_level args (IApp (tm1, tm2)) =
980 IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
981 | intro top_level args (IConst (name as (s, _), T, T_args)) =
982 (case proxify_const s of
984 if top_level orelse is_type_enc_higher_order type_enc then
985 case (top_level, s) of
986 (_, "c_False") => IConst (`I tptp_false, T, [])
987 | (_, "c_True") => IConst (`I tptp_true, T, [])
988 | (false, "c_Not") => IConst (`I tptp_not, T, [])
989 | (false, "c_conj") => IConst (`I tptp_and, T, [])
990 | (false, "c_disj") => IConst (`I tptp_or, T, [])
991 | (false, "c_implies") => IConst (`I tptp_implies, T, [])
992 | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
993 | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
995 if is_tptp_equal s andalso length args = 2 then
996 IConst (`I tptp_equal, T, [])
998 (* Use a proxy even for partially applied THF0 equality,
999 because the LEO-II and Satallax parsers complain about not
1000 being able to infer the type of "=". *)
1001 IConst (proxy_base |>> prefix const_prefix, T, T_args)
1002 | _ => IConst (name, T, [])
1004 IConst (proxy_base |>> prefix const_prefix, T, T_args)
1005 | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
1006 else IConst (name, T, T_args))
1007 | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
1009 in intro true [] end
1011 fun mangle_type_args_in_const format type_enc (name as (s, _)) T_args =
1012 case unprefix_and_unascii const_prefix s of
1013 NONE => (name, T_args)
1015 case type_arg_policy [] type_enc (invert_const s'') of
1016 Mangled_Type_Args => (mangled_const_name format type_enc T_args name, [])
1017 | _ => (name, T_args)
1018 fun mangle_type_args_in_iterm format type_enc =
1019 if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
1021 fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
1022 | mangle (tm as IConst (_, _, [])) = tm
1023 | mangle (IConst (name, T, T_args)) =
1024 mangle_type_args_in_const format type_enc name T_args
1025 |> (fn (name, T_args) => IConst (name, T, T_args))
1026 | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
1032 fun chop_fun 0 T = ([], T)
1033 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1034 chop_fun (n - 1) ran_T |>> cons dom_T
1035 | chop_fun _ T = ([], T)
1037 fun filter_const_type_args _ _ _ [] = []
1038 | filter_const_type_args thy s ary T_args =
1040 val U = robust_const_type thy s
1041 val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
1042 val U_args = (s, U) |> robust_const_typargs thy
1045 |> map (fn (U, T) =>
1046 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
1048 handle TYPE _ => T_args
1050 fun filter_type_args_in_const _ _ _ _ _ [] = []
1051 | filter_type_args_in_const thy monom_constrs type_enc ary s T_args =
1052 case unprefix_and_unascii const_prefix s of
1054 if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
1058 val s'' = invert_const s''
1059 fun filter_T_args false = T_args
1060 | filter_T_args true = filter_const_type_args thy s'' ary T_args
1062 case type_arg_policy monom_constrs type_enc s'' of
1063 Explicit_Type_Args infer_from_term_args =>
1064 filter_T_args infer_from_term_args
1065 | No_Type_Args => []
1066 | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
1068 fun filter_type_args_in_iterm thy monom_constrs type_enc =
1070 fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
1071 | filt ary (IConst (name as (s, _), T, T_args)) =
1072 filter_type_args_in_const thy monom_constrs type_enc ary s T_args
1073 |> (fn T_args => IConst (name, T, T_args))
1074 | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
1078 fun iformula_from_prop ctxt format type_enc eq_as_iff =
1080 val thy = Proof_Context.theory_of ctxt
1081 fun do_term bs t atomic_Ts =
1082 iterm_from_term thy format bs (Envir.eta_contract t)
1083 |>> (introduce_proxies_in_iterm type_enc
1084 #> mangle_type_args_in_iterm format type_enc #> AAtom)
1085 ||> union (op =) atomic_Ts
1086 fun do_quant bs q pos s T t' =
1088 val s = singleton (Name.variant_list (map fst bs)) s
1089 val universal = Option.map (q = AExists ? not) pos
1091 s |> `(case universal of
1092 SOME true => make_all_bound_var
1093 | SOME false => make_exist_bound_var
1094 | NONE => make_bound_var)
1096 do_formula ((s, (name, T)) :: bs) pos t'
1097 #>> mk_aquant q [(name, SOME T)]
1098 ##> union (op =) (atomic_types_of T)
1100 and do_conn bs c pos1 t1 pos2 t2 =
1101 do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
1102 and do_formula bs pos t =
1104 @{const Trueprop} $ t1 => do_formula bs pos t1
1105 | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
1106 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
1107 do_quant bs AForall pos s T t'
1108 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1109 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1110 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
1111 do_quant bs AExists pos s T t'
1112 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1113 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1114 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
1115 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
1116 | @{const HOL.implies} $ t1 $ t2 =>
1117 do_conn bs AImplies (Option.map not pos) t1 pos t2
1118 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
1119 if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
1121 in do_formula [] end
1123 fun presimplify_term ctxt t =
1124 t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
1125 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
1126 #> Meson.presimplify
1129 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
1130 fun conceal_bounds Ts t =
1131 subst_bounds (map (Free o apfst concealed_bound_name)
1132 (0 upto length Ts - 1 ~~ Ts), t)
1133 fun reveal_bounds Ts =
1134 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
1135 (0 upto length Ts - 1 ~~ Ts))
1137 fun is_fun_equality (@{const_name HOL.eq},
1138 Type (_, [Type (@{type_name fun}, _), _])) = true
1139 | is_fun_equality _ = false
1141 fun extensionalize_term ctxt t =
1142 if exists_Const is_fun_equality t then
1143 let val thy = Proof_Context.theory_of ctxt in
1144 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
1145 |> prop_of |> Logic.dest_equals |> snd
1150 fun simple_translate_lambdas do_lambdas ctxt t =
1151 let val thy = Proof_Context.theory_of ctxt in
1152 if Meson.is_fol_term thy t then
1158 @{const Not} $ t1 => @{const Not} $ trans Ts t1
1159 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
1160 t0 $ Abs (s, T, trans (T :: Ts) t')
1161 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1162 trans Ts (t0 $ eta_expand Ts t1 1)
1163 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
1164 t0 $ Abs (s, T, trans (T :: Ts) t')
1165 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1166 trans Ts (t0 $ eta_expand Ts t1 1)
1167 | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
1168 t0 $ trans Ts t1 $ trans Ts t2
1169 | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
1170 t0 $ trans Ts t1 $ trans Ts t2
1171 | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
1172 t0 $ trans Ts t1 $ trans Ts t2
1173 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1175 t0 $ trans Ts t1 $ trans Ts t2
1177 if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1178 else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1179 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1180 in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
1183 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
1184 do_cheaply_conceal_lambdas Ts t1
1185 $ do_cheaply_conceal_lambdas Ts t2
1186 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
1187 Const (lam_lifted_poly_prefix ^ serial_string (),
1188 T --> fastype_of1 (T :: Ts, t))
1189 | do_cheaply_conceal_lambdas _ t = t
1191 fun do_introduce_combinators ctxt Ts t =
1192 let val thy = Proof_Context.theory_of ctxt in
1193 t |> conceal_bounds Ts
1195 |> Meson_Clausify.introduce_combinators_in_cterm
1196 |> prop_of |> Logic.dest_equals |> snd
1199 (* A type variable of sort "{}" will make abstraction fail. *)
1200 handle THM _ => t |> do_cheaply_conceal_lambdas Ts
1201 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
1203 fun preprocess_abstractions_in_terms trans_lams facts =
1205 val (facts, lambda_ts) =
1206 facts |> map (snd o snd) |> trans_lams
1207 |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
1209 map2 (fn t => fn j =>
1210 ((lam_fact_prefix ^ Int.toString j, (Global, Spec_Eq)),
1212 lambda_ts (1 upto length lambda_ts)
1213 in (facts, lam_facts) end
1215 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
1216 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
1219 fun freeze (t $ u) = freeze t $ freeze u
1220 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
1221 | freeze (Var ((s, i), T)) =
1222 Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
1224 in t |> exists_subterm is_Var t ? freeze end
1226 fun presimp_prop ctxt role t =
1228 val thy = Proof_Context.theory_of ctxt
1229 val t = t |> Envir.beta_eta_contract
1230 |> transform_elim_prop
1231 |> Object_Logic.atomize_term thy
1232 val need_trueprop = (fastype_of t = @{typ bool})
1234 t |> need_trueprop ? HOLogic.mk_Trueprop
1235 |> extensionalize_term ctxt
1236 |> presimplify_term ctxt
1237 |> HOLogic.dest_Trueprop
1239 handle TERM _ => if role = Conjecture then @{term False} else @{term True})
1242 fun make_formula ctxt format type_enc eq_as_iff name stature kind t =
1244 val (iformula, atomic_Ts) =
1245 iformula_from_prop ctxt format type_enc eq_as_iff
1246 (SOME (kind <> Conjecture)) t []
1247 |>> close_iformula_universally
1249 {name = name, stature = stature, kind = kind, iformula = iformula,
1250 atomic_types = atomic_Ts}
1253 fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
1254 case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
1255 name stature Axiom of
1256 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1257 if s = tptp_true then NONE else SOME formula
1258 | formula => SOME formula
1260 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
1261 | s_not_trueprop t =
1262 if fastype_of t = @{typ bool} then s_not t
1263 else @{prop False} (* "t" is too meta *)
1265 fun make_conjecture ctxt format type_enc =
1266 map (fn ((name, stature), (kind, t)) =>
1267 t |> kind = Conjecture ? s_not_trueprop
1268 |> make_formula ctxt format type_enc (format <> CNF) name stature
1271 (** Finite and infinite type inference **)
1273 fun tvar_footprint thy s ary =
1274 (case unprefix_and_unascii const_prefix s of
1276 s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
1277 |> map (fn T => Term.add_tvarsT T [] |> map fst)
1281 fun ghost_type_args thy s ary =
1282 if is_tptp_equal s then
1286 val footprint = tvar_footprint thy s ary
1287 val eq = (s = @{const_name HOL.eq})
1288 fun ghosts _ [] = []
1289 | ghosts seen ((i, tvars) :: args) =
1290 ghosts (union (op =) seen tvars) args
1291 |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
1294 if forall null footprint then
1297 0 upto length footprint - 1 ~~ footprint
1298 |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
1302 type monotonicity_info =
1303 {maybe_finite_Ts : typ list,
1304 surely_finite_Ts : typ list,
1305 maybe_infinite_Ts : typ list,
1306 surely_infinite_Ts : typ list,
1307 maybe_nonmono_Ts : typ list}
1309 (* These types witness that the type classes they belong to allow infinite
1310 models and hence that any types with these type classes is monotonic. *)
1311 val known_infinite_types =
1312 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
1314 fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
1315 strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
1317 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1318 dangerous because their "exhaust" properties can easily lead to unsound ATP
1319 proofs. On the other hand, all HOL infinite types can be given the same
1320 models in first-order logic (via Löwenheim-Skolem). *)
1322 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
1323 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
1324 maybe_nonmono_Ts, ...}
1325 (Noninf_Nonmono_Types (strictness, grain)) T =
1326 grain = Ghost_Type_Arg_Vars orelse
1327 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1328 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
1329 (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
1330 is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
1332 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
1333 maybe_nonmono_Ts, ...}
1334 (Fin_Nonmono_Types grain) T =
1335 grain = Ghost_Type_Arg_Vars orelse
1336 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1337 (exists (type_generalization ctxt T) surely_finite_Ts orelse
1338 (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
1339 is_type_surely_finite ctxt T)))
1340 | should_encode_type _ _ _ _ = false
1342 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
1343 should_guard_var () andalso should_encode_type ctxt mono level T
1344 | should_guard_type _ _ _ _ _ = false
1346 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
1347 String.isPrefix bound_var_prefix s orelse
1348 String.isPrefix all_bound_var_prefix s
1349 | is_maybe_universal_var (IVar _) = true
1350 | is_maybe_universal_var _ = false
1353 Top_Level of bool option |
1354 Eq_Arg of bool option |
1357 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1358 | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
1359 if granularity_of_type_level level = All_Vars then
1360 should_encode_type ctxt mono level T
1362 (case (site, is_maybe_universal_var u) of
1363 (Eq_Arg _, true) => should_encode_type ctxt mono level T
1365 | should_tag_with_type _ _ _ _ _ _ = false
1367 fun fused_type ctxt mono level =
1369 val should_encode = should_encode_type ctxt mono level
1370 fun fuse 0 T = if should_encode T then T else fused_infinite_type
1371 | fuse ary (Type (@{type_name fun}, [T1, T2])) =
1372 fuse 0 T1 --> fuse (ary - 1) T2
1373 | fuse _ _ = raise Fail "expected function type"
1376 (** predicators and application operators **)
1379 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
1382 fun default_sym_tab_entries type_enc =
1383 (make_fixed_const NONE @{const_name undefined},
1384 {pred_sym = false, min_ary = 0, max_ary = 0, types = [],
1385 in_conj = false}) ::
1386 ([tptp_false, tptp_true]
1387 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [],
1388 in_conj = false})) @
1389 ([tptp_equal, tptp_old_equal]
1390 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [],
1392 |> not (is_type_enc_higher_order type_enc)
1393 ? cons (prefixed_predicator_name,
1394 {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
1397 datatype app_op_level = Incomplete_Apply | Sufficient_Apply | Full_Apply
1399 fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
1401 fun consider_var_ary const_T var_T max_ary =
1404 if ary = max_ary orelse type_instance ctxt var_T T orelse
1405 type_instance ctxt T var_T then
1408 iter (ary + 1) (range_type T)
1409 in iter 0 const_T end
1410 fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1411 if app_op_level = Sufficient_Apply andalso
1412 (can dest_funT T orelse T = @{typ bool}) then
1414 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1415 fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
1416 {pred_sym = pred_sym andalso not bool_vars',
1417 min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
1418 max_ary = max_ary, types = types, in_conj = in_conj}
1420 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1422 if bool_vars' = bool_vars andalso
1423 pointer_eq (fun_var_Ts', fun_var_Ts) then
1426 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
1430 fun add_iterm_syms conj_fact top_level tm
1431 (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1432 let val (head, args) = strip_iterm_comb tm in
1434 IConst ((s, _), T, _) =>
1435 if String.isPrefix bound_var_prefix s orelse
1436 String.isPrefix all_bound_var_prefix s then
1437 add_universal_var T accum
1438 else if String.isPrefix exist_bound_var_prefix s then
1441 let val ary = length args in
1442 ((bool_vars, fun_var_Ts),
1443 case Symtab.lookup sym_tab s of
1444 SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
1447 pred_sym andalso top_level andalso not bool_vars
1448 val types' = types |> insert_type ctxt I T
1449 val in_conj = in_conj orelse conj_fact
1451 if app_op_level = Sufficient_Apply andalso
1452 not (pointer_eq (types', types)) then
1453 fold (consider_var_ary T) fun_var_Ts min_ary
1457 Symtab.update (s, {pred_sym = pred_sym,
1458 min_ary = Int.min (ary, min_ary),
1459 max_ary = Int.max (ary, max_ary),
1460 types = types', in_conj = in_conj})
1465 val pred_sym = top_level andalso not bool_vars
1467 case app_op_level of
1468 Incomplete_Apply => ary
1469 | Sufficient_Apply =>
1470 fold (consider_var_ary T) fun_var_Ts ary
1473 Symtab.update_new (s,
1474 {pred_sym = pred_sym, min_ary = min_ary,
1475 max_ary = ary, types = [T], in_conj = conj_fact})
1479 | IVar (_, T) => add_universal_var T accum
1480 | IAbs ((_, T), tm) =>
1481 accum |> add_universal_var T |> add_iterm_syms conj_fact false tm
1483 |> fold (add_iterm_syms conj_fact false) args
1485 fun add_fact_syms conj_fact =
1486 K (add_iterm_syms conj_fact true) |> formula_fold NONE |> fact_lift
1488 ((false, []), Symtab.empty)
1489 |> fold (add_fact_syms true) conjs
1490 |> fold (add_fact_syms false) facts
1492 |> fold Symtab.update (default_sym_tab_entries type_enc)
1495 fun min_ary_of sym_tab s =
1496 case Symtab.lookup sym_tab s of
1497 SOME ({min_ary, ...} : sym_info) => min_ary
1499 case unprefix_and_unascii const_prefix s of
1501 let val s = s |> unmangled_const_name |> hd |> invert_const in
1502 if s = predicator_name then 1
1503 else if s = app_op_name then 2
1504 else if s = type_guard_name then 1
1509 (* True if the constant ever appears outside of the top-level position in
1510 literals, or if it appears with different arities (e.g., because of different
1511 type instantiations). If false, the constant always receives all of its
1512 arguments and is used as a predicate. *)
1513 fun is_pred_sym sym_tab s =
1514 case Symtab.lookup sym_tab s of
1515 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1516 pred_sym andalso min_ary = max_ary
1519 val app_op = `(make_fixed_const NONE) app_op_name
1520 val predicator_combconst =
1521 IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
1523 fun list_app head args = fold (curry (IApp o swap)) args head
1524 fun predicator tm = IApp (predicator_combconst, tm)
1526 fun mk_app_op format type_enc head arg =
1528 val head_T = ityp_of head
1529 val (arg_T, res_T) = dest_funT head_T
1531 IConst (app_op, head_T --> head_T, [arg_T, res_T])
1532 |> mangle_type_args_in_iterm format type_enc
1533 in list_app app [head, arg] end
1535 fun firstorderize_fact thy monom_constrs format type_enc sym_tab
1538 fun do_app arg head = mk_app_op format type_enc head arg
1539 fun list_app_ops head args = fold do_app args head
1540 fun introduce_app_ops tm =
1541 let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
1543 IConst (name as (s, _), T, T_args) =>
1544 if uncurried_aliases andalso String.isPrefix const_prefix s then
1546 val ary = length args
1547 val name = name |> ary > min_ary_of sym_tab s
1548 ? aliased_uncurried ary
1549 in list_app (IConst (name, T, T_args)) args end
1551 args |> chop (min_ary_of sym_tab s)
1552 |>> list_app head |-> list_app_ops
1553 | _ => list_app_ops head args
1555 fun introduce_predicators tm =
1556 case strip_iterm_comb tm of
1557 (IConst ((s, _), _, _), _) =>
1558 if is_pred_sym sym_tab s then tm else predicator tm
1559 | _ => predicator tm
1561 not (is_type_enc_higher_order type_enc)
1562 ? (introduce_app_ops #> introduce_predicators)
1563 #> filter_type_args_in_iterm thy monom_constrs type_enc
1564 in update_iformula (formula_map do_iterm) end
1566 (** Helper facts **)
1568 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
1569 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
1571 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1573 [(("COMBI", false), @{thms Meson.COMBI_def}),
1574 (("COMBK", false), @{thms Meson.COMBK_def}),
1575 (("COMBB", false), @{thms Meson.COMBB_def}),
1576 (("COMBC", false), @{thms Meson.COMBC_def}),
1577 (("COMBS", false), @{thms Meson.COMBS_def}),
1578 ((predicator_name, false), [not_ffalse, ftrue]),
1579 (("fFalse", false), [not_ffalse]),
1580 (("fFalse", true), @{thms True_or_False}),
1581 (("fTrue", false), [ftrue]),
1582 (("fTrue", true), @{thms True_or_False}),
1584 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1585 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1587 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1588 by (unfold fconj_def) fast+}),
1590 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1591 by (unfold fdisj_def) fast+}),
1592 (("fimplies", false),
1593 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1594 by (unfold fimplies_def) fast+}),
1596 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1597 However, this is done so for backward compatibility: Including the
1598 equality helpers by default in Metis breaks a few existing proofs. *)
1599 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1600 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1601 (* Partial characterization of "fAll" and "fEx". A complete characterization
1602 would require the axiom of choice for replay with Metis. *)
1603 (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
1604 (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
1605 (("If", true), @{thms if_True if_False True_or_False})]
1606 |> map (apsnd (map zero_var_indexes))
1608 fun atype_of_type_vars (Simple_Types (_, Polymorphic, _)) = SOME atype_of_types
1609 | atype_of_type_vars _ = NONE
1611 fun bound_tvars type_enc sorts Ts =
1612 (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
1613 #> mk_aquant AForall
1614 (map_filter (fn TVar (x as (s, _), _) =>
1615 SOME ((make_schematic_type_var x, s),
1616 atype_of_type_vars type_enc)
1619 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
1620 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1621 else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
1622 |> mk_aquant AForall bounds
1623 |> close_formula_universally
1624 |> bound_tvars type_enc true atomic_Ts
1626 val helper_rank = default_rank
1627 val min_rank = 9 * helper_rank div 10
1628 val max_rank = 4 * min_rank
1630 fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n
1632 val type_tag = `(make_fixed_const NONE) type_tag_name
1634 fun type_tag_idempotence_fact format type_enc =
1636 fun var s = ATerm (`I s, [])
1637 fun tag tm = ATerm (type_tag, [var "A", tm])
1638 val tagged_var = tag (var "X")
1640 Formula (type_tag_idempotence_helper_name, Axiom,
1641 eq_formula type_enc [] [] false (tag tagged_var) tagged_var,
1642 NONE, isabelle_info format spec_eqN helper_rank)
1645 fun should_specialize_helper type_enc t =
1646 polymorphism_of_type_enc type_enc <> Polymorphic andalso
1647 level_of_type_enc type_enc <> No_Types andalso
1648 not (null (Term.hidden_polymorphism t))
1650 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1651 case unprefix_and_unascii const_prefix s of
1654 val thy = Proof_Context.theory_of ctxt
1655 val unmangled_s = mangled_s |> unmangled_const_name |> hd
1656 fun dub needs_fairly_sound j k =
1657 unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1658 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1659 (if needs_fairly_sound then typed_helper_suffix
1660 else untyped_helper_suffix)
1661 fun dub_and_inst needs_fairly_sound (th, j) =
1662 let val t = prop_of th in
1663 if should_specialize_helper type_enc t then
1664 map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
1670 |> map (fn (k, t) =>
1671 ((dub needs_fairly_sound j k, (Global, Spec_Eq)), t))
1672 val make_facts = map_filter (make_fact ctxt format type_enc false)
1673 val fairly_sound = is_type_enc_fairly_sound type_enc
1676 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1677 if helper_s <> unmangled_s orelse
1678 (needs_fairly_sound andalso not fairly_sound) then
1681 ths ~~ (1 upto length ths)
1682 |> maps (dub_and_inst needs_fairly_sound)
1686 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1687 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1690 (***************************************************************)
1691 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1692 (***************************************************************)
1694 fun set_insert (x, s) = Symtab.update (x, ()) s
1696 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1698 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1699 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1701 fun classes_of_terms get_Ts =
1702 map (map snd o get_Ts)
1703 #> List.foldl add_classes Symtab.empty
1704 #> delete_type #> Symtab.keys
1706 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
1707 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
1709 fun fold_type_constrs f (Type (s, Ts)) x =
1710 fold (fold_type_constrs f) Ts (f (s, x))
1711 | fold_type_constrs _ _ x = x
1713 (* Type constructors used to instantiate overloaded constants are the only ones
1715 fun add_type_constrs_in_term thy =
1717 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1718 | add (t $ u) = add t #> add u
1720 x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
1721 | add (Abs (_, _, u)) = add u
1725 fun type_constrs_of_terms thy ts =
1726 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1728 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
1729 let val (head, args) = strip_comb t in
1730 (head |> dest_Const |> fst,
1731 fold_rev (fn t as Var ((s, _), T) =>
1732 (fn u => Abs (s, T, abstract_over (t, u)))
1733 | _ => raise Fail "expected Var") args u)
1735 | extract_lambda_def _ = raise Fail "malformed lifted lambda"
1737 fun trans_lams_from_string ctxt type_enc lam_trans =
1738 if lam_trans = no_lamsN then
1740 else if lam_trans = hide_lamsN then
1741 lift_lams ctxt type_enc ##> K []
1742 else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
1743 lift_lams ctxt type_enc
1744 else if lam_trans = combsN then
1745 map (introduce_combinators ctxt) #> rpair []
1746 else if lam_trans = combs_and_liftingN then
1747 lift_lams_part_1 ctxt type_enc
1748 ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
1750 else if lam_trans = combs_or_liftingN then
1751 lift_lams_part_1 ctxt type_enc
1752 ##> map (fn t => case head_of (strip_qnt_body @{const_name All} t) of
1753 @{term "op =::bool => bool => bool"} => t
1754 | _ => introduce_combinators ctxt (intentionalize_def t))
1756 else if lam_trans = keep_lamsN then
1757 map (Envir.eta_contract) #> rpair []
1759 error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
1761 fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
1764 val thy = Proof_Context.theory_of ctxt
1765 val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
1766 val fact_ts = facts |> map snd
1767 (* Remove existing facts from the conjecture, as this can dramatically
1768 boost an ATP's performance (for some reason). *)
1771 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1772 val facts = facts |> map (apsnd (pair Axiom))
1774 map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
1775 |> map (apsnd freeze_term)
1776 |> map2 (pair o rpair (Local, General) o string_of_int)
1777 (0 upto length hyp_ts)
1778 val ((conjs, facts), lam_facts) =
1780 |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
1781 |> (if lam_trans = no_lamsN then
1785 #> preprocess_abstractions_in_terms trans_lams
1786 #>> chop (length conjs))
1787 val conjs = conjs |> make_conjecture ctxt format type_enc
1788 val (fact_names, facts) =
1790 |> map_filter (fn (name, (_, t)) =>
1791 make_fact ctxt format type_enc true (name, t)
1792 |> Option.map (pair name))
1794 val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
1796 lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
1797 val all_ts = concl_t :: hyp_ts @ fact_ts
1798 val subs = tfree_classes_of_terms all_ts
1799 val supers = tvar_classes_of_terms all_ts
1800 val tycons = type_constrs_of_terms thy all_ts
1801 val (supers, arity_clauses) =
1802 if level_of_type_enc type_enc = No_Types then ([], [])
1803 else make_arity_clauses thy tycons supers
1804 val class_rel_clauses = make_class_rel_clauses thy subs supers
1806 (fact_names |> map single, union (op =) subs supers, conjs,
1807 facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
1810 val type_guard = `(make_fixed_const NONE) type_guard_name
1812 fun type_guard_iterm format type_enc T tm =
1813 IApp (IConst (type_guard, T --> @{typ bool}, [T])
1814 |> mangle_type_args_in_iterm format type_enc, tm)
1816 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1817 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1818 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1819 | is_var_positively_naked_in_term _ _ _ _ = true
1821 fun is_var_ghost_type_arg_in_term thy polym_constrs name pos tm accum =
1822 is_var_positively_naked_in_term name pos tm accum orelse
1824 val var = ATerm (name, [])
1825 fun is_nasty_in_term (ATerm (_, [])) = false
1826 | is_nasty_in_term (ATerm ((s, _), tms)) =
1828 val ary = length tms
1829 val polym_constr = member (op =) polym_constrs s
1830 val ghosts = ghost_type_args thy s ary
1832 exists (fn (j, tm) =>
1833 if polym_constr then
1834 member (op =) ghosts j andalso
1835 (tm = var orelse is_nasty_in_term tm)
1837 tm = var andalso member (op =) ghosts j)
1838 (0 upto ary - 1 ~~ tms)
1839 orelse (not polym_constr andalso exists is_nasty_in_term tms)
1841 | is_nasty_in_term _ = true
1842 in is_nasty_in_term tm end
1844 fun should_guard_var_in_formula thy polym_constrs level pos phi (SOME true)
1846 (case granularity_of_type_level level of
1848 | Positively_Naked_Vars =>
1849 formula_fold pos (is_var_positively_naked_in_term name) phi false
1850 | Ghost_Type_Arg_Vars =>
1851 formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name)
1853 | should_guard_var_in_formula _ _ _ _ _ _ _ = true
1855 fun always_guard_var_in_formula _ _ _ _ _ _ _ = true
1857 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
1858 | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
1859 granularity_of_type_level level <> All_Vars andalso
1860 should_encode_type ctxt mono level T
1861 | should_generate_tag_bound_decl _ _ _ _ _ = false
1863 fun mk_aterm format type_enc name T_args args =
1864 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1866 fun do_bound_type ctxt format mono type_enc =
1868 Simple_Types (_, _, level) =>
1869 fused_type ctxt mono level 0
1870 #> ho_type_from_typ format type_enc false 0 #> SOME
1873 fun tag_with_type ctxt format mono type_enc pos T tm =
1874 IConst (type_tag, T --> T, [T])
1875 |> mangle_type_args_in_iterm format type_enc
1876 |> ho_term_from_iterm ctxt format mono type_enc pos
1877 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1878 | _ => raise Fail "unexpected lambda-abstraction")
1879 and ho_term_from_iterm ctxt format mono type_enc =
1883 val (head, args) = strip_iterm_comb u
1886 Top_Level pos => pos
1891 IConst (name as (s, _), _, T_args) =>
1893 val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1895 map (term arg_site) args |> mk_aterm format type_enc name T_args
1898 map (term Elsewhere) args |> mk_aterm format type_enc name []
1899 | IAbs ((name, T), tm) =>
1900 AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1902 | IApp _ => raise Fail "impossible \"IApp\""
1905 if should_tag_with_type ctxt mono type_enc site u T then
1906 tag_with_type ctxt format mono type_enc pos T t
1910 in term o Top_Level end
1911 and formula_from_iformula ctxt polym_constrs format mono type_enc
1914 val thy = Proof_Context.theory_of ctxt
1915 val level = level_of_type_enc type_enc
1916 val do_term = ho_term_from_iterm ctxt format mono type_enc
1917 fun do_out_of_bound_type pos phi universal (name, T) =
1918 if should_guard_type ctxt mono type_enc
1919 (fn () => should_guard_var thy polym_constrs level pos phi
1920 universal name) T then
1922 |> type_guard_iterm format type_enc T
1923 |> do_term pos |> AAtom |> SOME
1924 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
1926 val var = ATerm (name, [])
1927 val tagged_var = tag_with_type ctxt format mono type_enc pos T var
1928 in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
1931 fun do_formula pos (AQuant (q, xs, phi)) =
1933 val phi = phi |> do_formula pos
1934 val universal = Option.map (q = AExists ? not) pos
1935 val do_bound_type = do_bound_type ctxt format mono type_enc
1937 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1938 | SOME T => do_bound_type T)),
1939 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1941 (fn (_, NONE) => NONE
1943 do_out_of_bound_type pos phi universal (s, T))
1947 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1948 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1951 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1952 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1953 the remote provers might care. *)
1954 fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
1955 mono type_enc rank (j, {name, stature, kind, iformula, atomic_types}) =
1956 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
1958 |> formula_from_iformula ctxt polym_constrs format mono type_enc
1959 should_guard_var_in_formula (if pos then SOME true else NONE)
1960 |> close_formula_universally
1961 |> bound_tvars type_enc true atomic_types,
1963 let val rank = rank j in
1965 Intro => isabelle_info format introN rank
1966 | Elim => isabelle_info format elimN rank
1967 | Simp => isabelle_info format simpN rank
1968 | Spec_Eq => isabelle_info format spec_eqN rank
1969 | _ => isabelle_info format "" rank
1973 fun formula_line_for_class_rel_clause format type_enc
1974 ({name, subclass, superclass, ...} : class_rel_clause) =
1975 let val ty_arg = ATerm (tvar_a_name, []) in
1976 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1978 [type_class_formula type_enc subclass ty_arg,
1979 type_class_formula type_enc superclass ty_arg])
1980 |> mk_aquant AForall
1981 [(tvar_a_name, atype_of_type_vars type_enc)],
1982 NONE, isabelle_info format introN helper_rank)
1985 fun formula_from_arity_atom type_enc (class, t, args) =
1986 ATerm (t, map (fn arg => ATerm (arg, [])) args)
1987 |> type_class_formula type_enc class
1989 fun formula_line_for_arity_clause format type_enc
1990 ({name, prem_atoms, concl_atom} : arity_clause) =
1991 Formula (arity_clause_prefix ^ name, Axiom,
1992 mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
1993 (formula_from_arity_atom type_enc concl_atom)
1994 |> mk_aquant AForall
1995 (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
1996 NONE, isabelle_info format introN helper_rank)
1998 fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
1999 ({name, kind, iformula, atomic_types, ...} : translated_formula) =
2000 Formula (conjecture_prefix ^ name, kind,
2002 |> formula_from_iformula ctxt polym_constrs format mono type_enc
2003 should_guard_var_in_formula (SOME false)
2004 |> close_formula_universally
2005 |> bound_tvars type_enc true atomic_types, NONE, [])
2007 fun formula_line_for_free_type j phi =
2008 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
2009 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
2012 fold (union (op =)) (map #atomic_types facts) []
2013 |> formulas_for_types type_enc add_sorts_on_tfree
2014 in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
2016 (** Symbol declarations **)
2018 fun decl_line_for_class order s =
2019 let val name as (s, _) = `make_type_class s in
2020 Decl (sym_decl_prefix ^ s, name,
2021 if order = First_Order then
2022 ATyAbs ([tvar_a_name],
2023 if avoid_first_order_ghost_type_vars then
2024 AFun (a_itself_atype, bool_atype)
2028 AFun (atype_of_types, bool_atype))
2031 fun decl_lines_for_classes type_enc classes =
2033 Simple_Types (order, Polymorphic, _) =>
2034 map (decl_line_for_class order) classes
2037 fun sym_decl_table_for_facts ctxt format type_enc sym_tab
2038 (conjs, facts, extra_tms) =
2040 fun add_iterm_syms tm =
2041 let val (head, args) = strip_iterm_comb tm in
2043 IConst ((s, s'), T, T_args) =>
2045 val (pred_sym, in_conj) =
2046 case Symtab.lookup sym_tab s of
2047 SOME ({pred_sym, in_conj, ...} : sym_info) =>
2049 | NONE => (false, false)
2052 Guards _ => not pred_sym
2053 | _ => true) andalso
2054 is_tptp_user_symbol s
2057 Symtab.map_default (s, [])
2058 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
2063 | IAbs (_, tm) => add_iterm_syms tm
2065 #> fold add_iterm_syms args
2067 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
2068 fun add_formula_var_types (AQuant (_, xs, phi)) =
2069 fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
2070 #> add_formula_var_types phi
2071 | add_formula_var_types (AConn (_, phis)) =
2072 fold add_formula_var_types phis
2073 | add_formula_var_types _ = I
2075 if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
2076 else fold (fact_lift add_formula_var_types) (conjs @ facts) []
2077 fun add_undefined_const T =
2080 `(make_fixed_const NONE) @{const_name undefined}
2081 |> (case type_arg_policy [] type_enc @{const_name undefined} of
2082 Mangled_Type_Args => mangled_const_name format type_enc [T]
2085 Symtab.map_default (s, [])
2086 (insert_type ctxt #3 (s', [T], T, false, 0, false))
2088 fun add_TYPE_const () =
2089 let val (s, s') = TYPE_name in
2090 Symtab.map_default (s, [])
2091 (insert_type ctxt #3
2092 (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
2096 |> is_type_enc_fairly_sound type_enc
2097 ? (fold (fold add_fact_syms) [conjs, facts]
2098 #> fold add_iterm_syms extra_tms
2099 #> (case type_enc of
2100 Simple_Types (First_Order, Polymorphic, _) =>
2101 if avoid_first_order_ghost_type_vars then add_TYPE_const ()
2103 | Simple_Types _ => I
2104 | _ => fold add_undefined_const (var_types ())))
2107 (* We add "bool" in case the helper "True_or_False" is included later. *)
2108 fun default_mono level =
2109 {maybe_finite_Ts = [@{typ bool}],
2110 surely_finite_Ts = [@{typ bool}],
2111 maybe_infinite_Ts = known_infinite_types,
2112 surely_infinite_Ts =
2114 Noninf_Nonmono_Types (Strict, _) => []
2115 | _ => known_infinite_types,
2116 maybe_nonmono_Ts = [@{typ bool}]}
2118 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
2119 out with monotonicity" paper presented at CADE 2011. *)
2120 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
2121 | add_iterm_mononotonicity_info ctxt level _
2122 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
2123 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
2124 surely_infinite_Ts, maybe_nonmono_Ts}) =
2125 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
2127 Noninf_Nonmono_Types (strictness, _) =>
2128 if exists (type_instance ctxt T) surely_infinite_Ts orelse
2129 member (type_equiv ctxt) maybe_finite_Ts T then
2131 else if is_type_kind_of_surely_infinite ctxt strictness
2132 surely_infinite_Ts T then
2133 {maybe_finite_Ts = maybe_finite_Ts,
2134 surely_finite_Ts = surely_finite_Ts,
2135 maybe_infinite_Ts = maybe_infinite_Ts,
2136 surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
2137 maybe_nonmono_Ts = maybe_nonmono_Ts}
2139 {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
2140 surely_finite_Ts = surely_finite_Ts,
2141 maybe_infinite_Ts = maybe_infinite_Ts,
2142 surely_infinite_Ts = surely_infinite_Ts,
2143 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2144 | Fin_Nonmono_Types _ =>
2145 if exists (type_instance ctxt T) surely_finite_Ts orelse
2146 member (type_equiv ctxt) maybe_infinite_Ts T then
2148 else if is_type_surely_finite ctxt T then
2149 {maybe_finite_Ts = maybe_finite_Ts,
2150 surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
2151 maybe_infinite_Ts = maybe_infinite_Ts,
2152 surely_infinite_Ts = surely_infinite_Ts,
2153 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2155 {maybe_finite_Ts = maybe_finite_Ts,
2156 surely_finite_Ts = surely_finite_Ts,
2157 maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
2158 surely_infinite_Ts = surely_infinite_Ts,
2159 maybe_nonmono_Ts = maybe_nonmono_Ts}
2163 | add_iterm_mononotonicity_info _ _ _ _ mono = mono
2164 fun add_fact_mononotonicity_info ctxt level
2165 ({kind, iformula, ...} : translated_formula) =
2166 formula_fold (SOME (kind <> Conjecture))
2167 (add_iterm_mononotonicity_info ctxt level) iformula
2168 fun mononotonicity_info_for_facts ctxt type_enc facts =
2169 let val level = level_of_type_enc type_enc in
2171 |> is_type_level_monotonicity_based level
2172 ? fold (add_fact_mononotonicity_info ctxt level) facts
2175 fun add_iformula_monotonic_types ctxt mono type_enc =
2177 val level = level_of_type_enc type_enc
2178 val should_encode = should_encode_type ctxt mono level
2179 fun add_type T = not (should_encode T) ? insert_type ctxt I T
2180 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
2182 and add_term tm = add_type (ityp_of tm) #> add_args tm
2183 in formula_fold NONE (K add_term) end
2184 fun add_fact_monotonic_types ctxt mono type_enc =
2185 add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
2186 fun monotonic_types_for_facts ctxt mono type_enc facts =
2187 let val level = level_of_type_enc type_enc in
2188 [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
2189 is_type_level_monotonicity_based level andalso
2190 granularity_of_type_level level <> Ghost_Type_Arg_Vars)
2191 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
2194 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
2195 Formula (guards_sym_formula_prefix ^
2196 ascii_of (mangled_type format type_enc T),
2198 IConst (`make_bound_var "X", T, [])
2199 |> type_guard_iterm format type_enc T
2201 |> formula_from_iformula ctxt [] format mono type_enc
2202 always_guard_var_in_formula (SOME true)
2203 |> close_formula_universally
2204 |> bound_tvars type_enc true (atomic_types_of T),
2205 NONE, isabelle_info format introN helper_rank)
2207 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
2208 let val x_var = ATerm (`make_bound_var "X", []) in
2209 Formula (tags_sym_formula_prefix ^
2210 ascii_of (mangled_type format type_enc T),
2212 eq_formula type_enc (atomic_types_of T) [] false
2213 (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
2214 NONE, isabelle_info format spec_eqN helper_rank)
2217 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
2219 Simple_Types _ => []
2221 map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
2222 | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
2224 fun decl_line_for_sym ctxt format mono type_enc s
2225 (s', T_args, T, pred_sym, ary, _) =
2227 val thy = Proof_Context.theory_of ctxt
2231 else case unprefix_and_unascii const_prefix s of
2234 val s' = s' |> invert_const
2235 val T = s' |> robust_const_type thy
2236 in (T, robust_const_typargs thy (s', T)) end
2237 | NONE => raise Fail "unexpected type arguments"
2239 Decl (sym_decl_prefix ^ s, (s, s'),
2240 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
2241 |> ho_type_from_typ format type_enc pred_sym ary
2242 |> not (null T_args)
2243 ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
2246 fun honor_conj_sym_kind in_conj conj_sym_kind =
2247 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
2250 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
2251 j (s', T_args, T, _, ary, in_conj) =
2253 val thy = Proof_Context.theory_of ctxt
2254 val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
2255 val (arg_Ts, res_T) = chop_fun ary T
2256 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2258 bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
2260 if exists (curry (op =) dummyT) T_args then
2261 case level_of_type_enc type_enc of
2262 All_Types => map SOME arg_Ts
2264 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
2265 let val ghosts = ghost_type_args thy s ary in
2266 map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
2267 (0 upto ary - 1) arg_Ts
2274 Formula (guards_sym_formula_prefix ^ s ^
2275 (if n > 1 then "_" ^ string_of_int j else ""), kind,
2276 IConst ((s, s'), T, T_args)
2277 |> fold (curry (IApp o swap)) bounds
2278 |> type_guard_iterm format type_enc res_T
2279 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
2280 |> formula_from_iformula ctxt [] format mono type_enc
2281 always_guard_var_in_formula (SOME true)
2282 |> close_formula_universally
2283 |> bound_tvars type_enc (n > 1) (atomic_types_of T)
2285 NONE, isabelle_info format introN helper_rank)
2288 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
2289 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
2291 val thy = Proof_Context.theory_of ctxt
2292 val level = level_of_type_enc type_enc
2293 val grain = granularity_of_type_level level
2295 tags_sym_formula_prefix ^ s ^
2296 (if n > 1 then "_" ^ string_of_int j else "")
2297 val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
2298 val (arg_Ts, res_T) = chop_fun ary T
2299 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2300 val bounds = bound_names |> map (fn name => ATerm (name, []))
2301 val cst = mk_aterm format type_enc (s, s') T_args
2302 val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
2303 val should_encode = should_encode_type ctxt mono level
2304 val tag_with = tag_with_type ctxt format mono type_enc NONE
2305 val add_formula_for_res =
2306 if should_encode res_T then
2309 if grain = Ghost_Type_Arg_Vars then
2310 let val ghosts = ghost_type_args thy s ary in
2311 map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
2312 (0 upto ary - 1 ~~ arg_Ts) bounds
2317 cons (Formula (ident_base ^ "_res", kind,
2318 eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
2319 NONE, isabelle_info format spec_eqN helper_rank))
2323 fun add_formula_for_arg k =
2324 let val arg_T = nth arg_Ts k in
2325 if should_encode arg_T then
2326 case chop k bounds of
2327 (bounds1, bound :: bounds2) =>
2328 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
2329 eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
2331 NONE, isabelle_info format spec_eqN helper_rank))
2332 | _ => raise Fail "expected nonempty tail"
2337 [] |> not pred_sym ? add_formula_for_res
2338 |> (Config.get ctxt type_tag_arguments andalso
2339 grain = Positively_Naked_Vars)
2340 ? fold add_formula_for_arg (ary - 1 downto 0)
2343 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
2345 fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
2347 val T = result_type_of_decl decl
2348 |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
2350 if forall (type_generalization ctxt T o result_type_of_decl) decls' then
2355 | rationalize_decls _ decls = decls
2357 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
2360 Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
2361 | Guards (_, level) =>
2363 val decls = decls |> rationalize_decls ctxt
2364 val n = length decls
2366 decls |> filter (should_encode_type ctxt mono level
2367 o result_type_of_decl)
2369 (0 upto length decls - 1, decls)
2370 |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
2373 | Tags (_, level) =>
2374 if granularity_of_type_level level = All_Vars then
2377 let val n = length decls in
2378 (0 upto n - 1 ~~ decls)
2379 |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono
2383 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
2384 mono_Ts sym_decl_tab =
2386 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
2388 problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
2390 fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
2393 in mono_lines @ decl_lines end
2395 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
2397 fun do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
2398 mono type_enc sym_tab0 sym_tab base_s0 types in_conj =
2402 val thy = Proof_Context.theory_of ctxt
2403 val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
2404 val base_name = base_s0 |> `(make_fixed_const (SOME format))
2405 val T = case types of [T] => T | _ => robust_const_type thy base_s0
2406 val T_args = robust_const_typargs thy (base_s0, T)
2407 val (base_name as (base_s, _), T_args) =
2408 mangle_type_args_in_const format type_enc base_name T_args
2409 val base_ary = min_ary_of sym_tab0 base_s
2410 fun do_const name = IConst (name, T, T_args)
2412 filter_type_args_in_iterm thy monom_constrs type_enc
2413 #> ho_term_from_iterm ctxt format mono type_enc (SOME true)
2414 val name1 as (s1, _) =
2415 base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
2416 val name2 as (s2, _) = base_name |> aliased_uncurried ary
2417 val (arg_Ts, _) = chop_fun ary T
2419 1 upto ary |> map (`I o make_bound_var o string_of_int)
2420 val bounds = bound_names ~~ arg_Ts
2421 val (first_bounds, last_bound) =
2422 bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last
2424 mk_app_op format type_enc (list_app (do_const name1) first_bounds)
2426 val tm2 = list_app (do_const name2) (first_bounds @ [last_bound])
2427 val do_bound_type = do_bound_type ctxt format mono type_enc
2429 eq_formula type_enc (atomic_types_of T)
2430 (map (apsnd do_bound_type) bounds) false
2431 (do_term tm1) (do_term tm2)
2434 [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
2435 NONE, isabelle_info format spec_eqN helper_rank)])
2436 |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
2437 else pair_append (do_alias (ary - 1)))
2440 fun uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
2441 type_enc sym_tab0 sym_tab
2442 (s, {min_ary, types, in_conj, ...} : sym_info) =
2443 case unprefix_and_unascii const_prefix s of
2445 if String.isSubstring uncurried_alias_sep mangled_s then
2447 val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
2449 do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
2450 mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary
2455 fun uncurried_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
2456 mono type_enc uncurried_aliases sym_tab0 sym_tab =
2458 |> uncurried_aliases
2461 o uncurried_alias_lines_for_sym ctxt monom_constrs format
2462 conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab
2464 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
2465 Config.get ctxt type_tag_idempotence andalso
2466 is_type_level_monotonicity_based level andalso
2467 poly <> Mangled_Monomorphic
2468 | needs_type_tag_idempotence _ _ = false
2470 val implicit_declsN = "Should-be-implicit typings"
2471 val explicit_declsN = "Explicit typings"
2472 val uncurried_alias_eqsN = "Uncurried aliases"
2473 val factsN = "Relevant facts"
2474 val class_relsN = "Class relationships"
2475 val aritiesN = "Arities"
2476 val helpersN = "Helper facts"
2477 val conjsN = "Conjectures"
2478 val free_typesN = "Type variables"
2480 (* TFF allows implicit declarations of types, function symbols, and predicate
2481 symbols (with "$i" as the type of individuals), but some provers (e.g.,
2482 SNARK) require explicit declarations. The situation is similar for THF. *)
2484 fun default_type type_enc pred_sym s =
2489 if String.isPrefix type_const_prefix s then atype_of_types
2490 else individual_atype
2491 | _ => individual_atype
2492 fun typ 0 = if pred_sym then bool_atype else ind
2493 | typ ary = AFun (ind, typ (ary - 1))
2496 fun nary_type_constr_type n =
2497 funpow n (curry AFun atype_of_types) atype_of_types
2499 fun undeclared_syms_in_problem type_enc problem =
2501 val declared = declared_syms_in_problem problem
2502 fun do_sym (name as (s, _)) ty =
2503 if is_tptp_user_symbol s andalso not (member (op =) declared name) then
2504 AList.default (op =) (name, ty)
2507 fun do_type (AType (name, tys)) =
2508 do_sym name (fn () => nary_type_constr_type (length tys))
2510 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
2511 | do_type (ATyAbs (_, ty)) = do_type ty
2512 fun do_term pred_sym (ATerm (name as (s, _), tms)) =
2513 do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
2514 #> fold (do_term false) tms
2515 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
2516 fun do_formula (AQuant (_, xs, phi)) =
2517 fold do_type (map_filter snd xs) #> do_formula phi
2518 | do_formula (AConn (_, phis)) = fold do_formula phis
2519 | do_formula (AAtom tm) = do_term true tm
2520 fun do_problem_line (Decl (_, _, ty)) = do_type ty
2521 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
2523 fold (fold do_problem_line o snd) problem []
2524 |> filter_out (is_built_in_tptp_symbol o fst o fst)
2527 fun declare_undeclared_syms_in_atp_problem type_enc problem =
2531 |> undeclared_syms_in_problem type_enc
2532 |> sort_wrt (fst o fst)
2533 |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
2534 in (implicit_declsN, decls) :: problem end
2536 fun exists_subdtype P =
2538 fun ex U = P U orelse
2539 (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false)
2542 fun is_poly_constr (_, Us) =
2543 exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
2545 fun all_constrs_of_polymorphic_datatypes thy =
2549 #> (fn cs => exists is_poly_constr cs ? append cs))
2550 (Datatype.get_all thy) []
2551 |> List.partition is_poly_constr
2552 |> pairself (map fst)
2554 val app_op_threshold = 50
2556 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
2557 lam_trans uncurried_aliases readable_names preproc
2558 hyp_ts concl_t facts =
2560 val thy = Proof_Context.theory_of ctxt
2561 val type_enc = type_enc |> adjust_type_enc format
2562 (* Forcing explicit applications is expensive for polymorphic encodings,
2563 because it takes only one existential variable ranging over "'a => 'b" to
2564 ruin everything. Hence we do it only if there are few facts (which is
2565 normally the case for "metis" and the minimizer). *)
2567 if polymorphism_of_type_enc type_enc = Polymorphic andalso
2568 length facts >= app_op_threshold then
2573 if lam_trans = keep_lamsN andalso
2574 not (is_type_enc_higher_order type_enc) then
2575 error ("Lambda translation scheme incompatible with first-order \
2579 val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
2581 translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
2583 val sym_tab0 = sym_table_for_facts ctxt type_enc app_op_level conjs facts
2584 val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
2585 val (polym_constrs, monom_constrs) =
2586 all_constrs_of_polymorphic_datatypes thy
2587 |>> map (make_fixed_const (SOME format))
2588 fun firstorderize in_helper =
2589 firstorderize_fact thy monom_constrs format type_enc sym_tab0
2590 (uncurried_aliases andalso not in_helper)
2591 val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
2592 val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
2594 sym_tab |> helper_facts_for_sym_table ctxt format type_enc
2595 |> map (firstorderize true)
2597 helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
2598 val class_decl_lines = decl_lines_for_classes type_enc classes
2599 val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
2600 uncurried_alias_lines_for_sym_table ctxt monom_constrs format
2601 conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
2602 val sym_decl_lines =
2603 (conjs, helpers @ facts, uncurried_alias_eq_tms)
2604 |> sym_decl_table_for_facts ctxt format type_enc sym_tab
2605 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
2607 val num_facts = length facts
2609 map (formula_line_for_fact ctxt polym_constrs format fact_prefix
2610 ascii_of (not exporter) (not exporter) mono type_enc
2611 (rank_of_fact_num num_facts))
2612 (0 upto num_facts - 1 ~~ facts)
2614 0 upto length helpers - 1 ~~ helpers
2615 |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I
2616 false true mono type_enc (K default_rank))
2617 |> (if needs_type_tag_idempotence ctxt type_enc then
2618 cons (type_tag_idempotence_fact format type_enc)
2621 (* Reordering these might confuse the proof reconstruction code or the SPASS
2624 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
2625 (uncurried_alias_eqsN, uncurried_alias_eq_lines),
2626 (factsN, fact_lines),
2628 map (formula_line_for_class_rel_clause format type_enc)
2631 map (formula_line_for_arity_clause format type_enc) arity_clauses),
2632 (helpersN, helper_lines),
2634 map (formula_line_for_conjecture ctxt polym_constrs format mono
2636 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
2640 CNF => ensure_cnf_problem
2641 | CNF_UEQ => filter_cnf_ueq_problem
2643 | TFF (_, TPTP_Implicit) => I
2644 | THF (_, TPTP_Implicit, _) => I
2645 | _ => declare_undeclared_syms_in_atp_problem type_enc)
2646 val (problem, pool) = problem |> nice_atp_problem readable_names format
2647 fun add_sym_ary (s, {min_ary, ...} : sym_info) =
2648 min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
2651 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
2652 fact_names |> Vector.fromList,
2654 Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
2658 val conj_weight = 0.0
2659 val hyp_weight = 0.1
2660 val fact_min_weight = 0.2
2661 val fact_max_weight = 1.0
2662 val type_info_default_weight = 0.8
2664 fun add_term_weights weight (ATerm (s, tms)) =
2665 is_tptp_user_symbol s ? Symtab.default (s, weight)
2666 #> fold (add_term_weights weight) tms
2667 | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
2668 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
2669 formula_fold NONE (K (add_term_weights weight)) phi
2670 | add_problem_line_weights _ _ = I
2672 fun add_conjectures_weights [] = I
2673 | add_conjectures_weights conjs =
2674 let val (hyps, conj) = split_last conjs in
2675 add_problem_line_weights conj_weight conj
2676 #> fold (add_problem_line_weights hyp_weight) hyps
2679 fun add_facts_weights facts =
2681 val num_facts = length facts
2683 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
2684 / Real.fromInt num_facts
2686 map weight_of (0 upto num_facts - 1) ~~ facts
2687 |> fold (uncurry add_problem_line_weights)
2690 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
2691 fun atp_problem_weights problem =
2692 let val get = these o AList.lookup (op =) problem in
2694 |> add_conjectures_weights (get free_typesN @ get conjsN)
2695 |> add_facts_weights (get factsN)
2696 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
2697 [explicit_declsN, class_relsN, aritiesN]
2699 |> sort (prod_ord Real.compare string_ord o pairself swap)