third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
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 | 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 simple_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
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 -> 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 simple_type_prefix = "s_"
149 val class_prefix = "cl_"
151 (* Freshness almost guaranteed! *)
152 val atp_weak_prefix = "ATP:"
154 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
155 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
156 val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
158 val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
159 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
160 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
162 val combinator_prefix = "COMB"
164 val type_decl_prefix = "ty_"
165 val sym_decl_prefix = "sy_"
166 val guards_sym_formula_prefix = "gsy_"
167 val tags_sym_formula_prefix = "tsy_"
168 val fact_prefix = "fact_"
169 val conjecture_prefix = "conj_"
170 val helper_prefix = "help_"
171 val class_rel_clause_prefix = "clar_"
172 val arity_clause_prefix = "arity_"
173 val tfree_clause_prefix = "tfree_"
175 val lam_fact_prefix = "ATP.lambda_"
176 val typed_helper_suffix = "_T"
177 val untyped_helper_suffix = "_U"
178 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
180 val predicator_name = "pp"
181 val app_op_name = "aa"
182 val type_guard_name = "gg"
183 val type_tag_name = "tt"
185 val prefixed_predicator_name = const_prefix ^ predicator_name
186 val prefixed_app_op_name = const_prefix ^ app_op_name
187 val prefixed_type_tag_name = const_prefix ^ type_tag_name
189 (*Escaping of special characters.
190 Alphanumeric characters are left unchanged.
191 The character _ goes to __
192 Characters in the range ASCII space to / go to _A to _P, respectively.
193 Other characters go to _nnn where nnn is the decimal ASCII code.*)
194 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
196 fun stringN_of_int 0 _ = ""
197 | stringN_of_int k n =
198 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
200 fun ascii_of_char c =
201 if Char.isAlphaNum c then
203 else if c = #"_" then
205 else if #" " <= c andalso c <= #"/" then
206 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
208 (* fixed width, in case more digits follow *)
209 "_" ^ stringN_of_int 3 (Char.ord c)
211 val ascii_of = String.translate ascii_of_char
213 (** Remove ASCII armoring from names in proof files **)
215 (* We don't raise error exceptions because this code can run inside a worker
216 thread. Also, the errors are impossible. *)
219 fun un rcs [] = String.implode(rev rcs)
220 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
221 (* Three types of _ escapes: __, _A to _P, _nnn *)
222 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
223 | un rcs (#"_" :: c :: cs) =
224 if #"A" <= c andalso c<= #"P" then
225 (* translation of #" " to #"/" *)
226 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
228 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
229 case Int.fromString (String.implode digits) of
230 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
231 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
233 | un rcs (c :: cs) = un (c :: rcs) cs
234 in un [] o String.explode end
236 (* If string s has the prefix s1, return the result of deleting it,
238 fun unprefix_and_unascii s1 s =
239 if String.isPrefix s1 s then
240 SOME (unascii_of (String.extract (s, size s1, NONE)))
245 [("c_False", (@{const_name False}, (@{thm fFalse_def},
246 ("fFalse", @{const_name ATP.fFalse})))),
247 ("c_True", (@{const_name True}, (@{thm fTrue_def},
248 ("fTrue", @{const_name ATP.fTrue})))),
249 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
250 ("fNot", @{const_name ATP.fNot})))),
251 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
252 ("fconj", @{const_name ATP.fconj})))),
253 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
254 ("fdisj", @{const_name ATP.fdisj})))),
255 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
256 ("fimplies", @{const_name ATP.fimplies})))),
257 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
258 ("fequal", @{const_name ATP.fequal})))),
259 ("c_All", (@{const_name All}, (@{thm fAll_def},
260 ("fAll", @{const_name ATP.fAll})))),
261 ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
262 ("fEx", @{const_name ATP.fEx}))))]
264 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
266 (* Readable names for the more common symbolic functions. Do not mess with the
267 table unless you know what you are doing. *)
268 val const_trans_table =
269 [(@{type_name Product_Type.prod}, "prod"),
270 (@{type_name Sum_Type.sum}, "sum"),
271 (@{const_name False}, "False"),
272 (@{const_name True}, "True"),
273 (@{const_name Not}, "Not"),
274 (@{const_name conj}, "conj"),
275 (@{const_name disj}, "disj"),
276 (@{const_name implies}, "implies"),
277 (@{const_name HOL.eq}, "equal"),
278 (@{const_name All}, "All"),
279 (@{const_name Ex}, "Ex"),
280 (@{const_name If}, "If"),
281 (@{const_name Set.member}, "member"),
282 (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
283 (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
284 (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
285 (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
286 (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
288 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
290 (* Invert the table of translations between Isabelle and ATPs. *)
291 val const_trans_table_inv =
292 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
293 val const_trans_table_unprox =
295 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
297 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
298 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
301 case Symtab.lookup const_trans_table c of
305 fun ascii_of_indexname (v, 0) = ascii_of v
306 | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
308 fun make_bound_var x = bound_var_prefix ^ ascii_of x
309 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
310 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
311 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
312 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
314 fun make_schematic_type_var (x, i) =
315 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
316 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
318 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
320 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
321 fun default c = const_prefix ^ lookup_const c
323 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
324 | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
325 if c = choice_const then tptp_choice else default c
326 | make_fixed_const _ c = default c
329 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
331 fun make_type_class clas = class_prefix ^ ascii_of clas
333 fun new_skolem_var_name_from_const s =
334 let val ss = s |> space_explode Long_Name.separator in
335 nth ss (length ss - 2)
338 (* These are either simplified away by "Meson.presimplify" (most of the time) or
339 handled specially via "fFalse", "fTrue", ..., "fequal". *)
340 val atp_irrelevant_consts =
341 [@{const_name False}, @{const_name True}, @{const_name Not},
342 @{const_name conj}, @{const_name disj}, @{const_name implies},
343 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
345 val atp_monomorph_bad_consts =
346 atp_irrelevant_consts @
347 (* These are ignored anyway by the relevance filter (unless they appear in
348 higher-order places) but not by the monomorphizer. *)
349 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
350 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
351 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
353 fun add_schematic_const (x as (_, T)) =
354 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
355 val add_schematic_consts_of =
356 Term.fold_aterms (fn Const (x as (s, _)) =>
357 not (member (op =) atp_monomorph_bad_consts s)
358 ? add_schematic_const x
360 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
362 (** Definitions and functions for FOL clauses and formulas for TPTP **)
364 (** Isabelle arities **)
366 type arity_atom = name * name * name list
368 val type_class = the_single @{sort type}
372 prem_atoms : arity_atom list,
373 concl_atom : arity_atom}
375 fun add_prem_atom tvar =
376 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
378 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
379 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
381 val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
382 val tvars_srts = ListPair.zip (tvars, args)
385 prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
386 concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
390 fun arity_clause _ _ (_, []) = []
391 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
392 arity_clause seen n (tcons, ars)
393 | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
394 if member (op =) seen class then
395 (* multiple arities for the same (tycon, class) pair *)
396 make_axiom_arity_clause (tcons,
397 lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
399 arity_clause seen (n + 1) (tcons, ars)
401 make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
402 ascii_of class, ar) ::
403 arity_clause (class :: seen) n (tcons, ars)
405 fun multi_arity_clause [] = []
406 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
407 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
409 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
410 theory thy provided its arguments have the corresponding sorts. *)
411 fun type_class_pairs thy tycons classes =
413 val alg = Sign.classes_of thy
414 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
415 fun add_class tycon class =
416 cons (class, domain_sorts tycon class)
417 handle Sorts.CLASS_ERROR _ => I
418 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
419 in map try_classes tycons end
421 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
422 fun iter_type_class_pairs _ _ [] = ([], [])
423 | iter_type_class_pairs thy tycons classes =
425 fun maybe_insert_class s =
426 (s <> type_class andalso not (member (op =) classes s))
428 val cpairs = type_class_pairs thy tycons classes
430 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
431 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
432 in (classes' @ classes, union (op =) cpairs' cpairs) end
434 fun make_arity_clauses thy tycons =
435 iter_type_class_pairs thy tycons ##> multi_arity_clause
438 (** Isabelle class relations **)
440 type class_rel_clause =
445 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
447 fun class_pairs _ [] _ = []
448 | class_pairs thy subs supers =
450 val class_less = Sorts.class_less (Sign.classes_of thy)
451 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
452 fun add_supers sub = fold (add_super sub) supers
453 in fold add_supers subs [] end
455 fun make_class_rel_clause (sub, super) =
456 {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
457 superclass = `make_type_class super}
459 fun make_class_rel_clauses thy subs supers =
460 map make_class_rel_clause (class_pairs thy subs supers)
462 (* intermediate terms *)
464 IConst of name * typ * typ list |
466 IApp of iterm * iterm |
467 IAbs of (name * typ) * iterm
469 fun ityp_of (IConst (_, T, _)) = T
470 | ityp_of (IVar (_, T)) = T
471 | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
472 | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
474 (*gets the head of a combinator application, along with the list of arguments*)
475 fun strip_iterm_comb u =
477 fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
479 in stripc (u, []) end
481 fun atomic_types_of T = fold_atyps (insert (op =)) T []
483 val tvar_a_str = "'a"
484 val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
485 val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
486 val itself_name = `make_fixed_type_const @{type_name itself}
487 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
488 val tvar_a_atype = AType (tvar_a_name, [])
489 val a_itself_atype = AType (itself_name, [tvar_a_atype])
491 fun new_skolem_const_name s num_T_args =
492 [new_skolem_const_prefix, s, string_of_int num_T_args]
493 |> space_implode Long_Name.separator
495 fun robust_const_type thy s =
496 if s = app_op_name then
497 Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
498 else if String.isPrefix lam_lifted_prefix s then
499 Logic.varifyT_global @{typ "'a => 'b"}
501 (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
502 s |> Sign.the_const_type thy
504 (* This function only makes sense if "T" is as general as possible. *)
505 fun robust_const_typargs thy (s, T) =
506 if s = app_op_name then
507 let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
508 else if String.isPrefix old_skolem_const_prefix s then
509 [] |> Term.add_tvarsT T |> rev |> map TVar
510 else if String.isPrefix lam_lifted_prefix s then
511 if String.isPrefix lam_lifted_poly_prefix s then
512 let val (T1, T2) = T |> dest_funT in [T1, T2] end
516 (s, T) |> Sign.const_typargs thy
518 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
519 Also accumulates sort infomation. *)
520 fun iterm_from_term thy format bs (P $ Q) =
522 val (P', P_atomics_Ts) = iterm_from_term thy format bs P
523 val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
524 in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
525 | iterm_from_term thy format _ (Const (c, T)) =
526 (IConst (`(make_fixed_const (SOME format)) c, T,
527 robust_const_typargs thy (c, T)),
529 | iterm_from_term _ _ _ (Free (s, T)) =
530 (IConst (`make_fixed_var s, T, []), atomic_types_of T)
531 | iterm_from_term _ format _ (Var (v as (s, _), T)) =
532 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
534 val Ts = T |> strip_type |> swap |> op ::
535 val s' = new_skolem_const_name s (length Ts)
536 in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
538 IVar ((make_schematic_var v, s), T), atomic_types_of T)
539 | iterm_from_term _ _ bs (Bound j) =
540 nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
541 | iterm_from_term thy format bs (Abs (s, T, t)) =
543 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
545 val name = `make_bound_var s
546 val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
547 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
549 datatype scope = Global | Local | Assum | Chained
550 datatype status = General | Induct | Intro | Elim | Simp | Eq
551 type stature = scope * status
553 datatype order = First_Order | Higher_Order
554 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
555 datatype strictness = Strict | Non_Strict
556 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
557 datatype type_level =
559 Noninf_Nonmono_Types of strictness * granularity |
560 Fin_Nonmono_Types of granularity |
565 Simple_Types of order * polymorphism * type_level |
566 Guards of polymorphism * type_level |
567 Tags of polymorphism * type_level
569 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
570 | is_type_enc_higher_order _ = false
572 fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
573 | polymorphism_of_type_enc (Guards (poly, _)) = poly
574 | polymorphism_of_type_enc (Tags (poly, _)) = poly
576 fun level_of_type_enc (Simple_Types (_, _, level)) = level
577 | level_of_type_enc (Guards (_, level)) = level
578 | level_of_type_enc (Tags (_, level)) = level
580 fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
581 | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
582 | granularity_of_type_level _ = All_Vars
584 fun is_type_level_quasi_sound All_Types = true
585 | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
586 | is_type_level_quasi_sound _ = false
587 val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
589 fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
590 | is_type_level_fairly_sound level = is_type_level_quasi_sound level
591 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
593 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
594 | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
595 | is_type_level_monotonicity_based _ = false
597 (* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
599 val queries = ["?", "_query"]
600 val bangs = ["!", "_bang"]
601 val ats = ["@", "_at"]
603 fun try_unsuffixes ss s =
604 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
606 fun try_nonmono constr suffixes fallback s =
607 case try_unsuffixes suffixes s of
609 (case try_unsuffixes suffixes s of
610 SOME s => (constr Positively_Naked_Vars, s)
612 case try_unsuffixes ats s of
613 SOME s => (constr Ghost_Type_Arg_Vars, s)
614 | NONE => (constr All_Vars, s))
617 fun type_enc_from_string strictness s =
618 (case try (unprefix "poly_") s of
619 SOME s => (SOME Polymorphic, s)
621 case try (unprefix "raw_mono_") s of
622 SOME s => (SOME Raw_Monomorphic, s)
624 case try (unprefix "mono_") s of
625 SOME s => (SOME Mangled_Monomorphic, s)
628 |> try_nonmono Fin_Nonmono_Types bangs
629 |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
630 |> (fn (poly, (level, core)) =>
631 case (core, (poly, level)) of
632 ("simple", (SOME poly, _)) =>
633 (case (poly, level) of
634 (Polymorphic, All_Types) =>
635 Simple_Types (First_Order, Polymorphic, All_Types)
636 | (Mangled_Monomorphic, _) =>
637 if granularity_of_type_level level = All_Vars then
638 Simple_Types (First_Order, Mangled_Monomorphic, level)
641 | _ => raise Same.SAME)
642 | ("simple_higher", (SOME poly, _)) =>
643 (case (poly, level) of
644 (Polymorphic, All_Types) =>
645 Simple_Types (Higher_Order, Polymorphic, All_Types)
646 | (_, Noninf_Nonmono_Types _) => raise Same.SAME
647 | (Mangled_Monomorphic, _) =>
648 if granularity_of_type_level level = All_Vars then
649 Simple_Types (Higher_Order, Mangled_Monomorphic, level)
652 | _ => raise Same.SAME)
653 | ("guards", (SOME poly, _)) =>
654 if poly = Mangled_Monomorphic andalso
655 granularity_of_type_level level = Ghost_Type_Arg_Vars then
659 | ("tags", (SOME poly, _)) =>
660 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
664 | ("args", (SOME poly, All_Types (* naja *))) =>
665 Guards (poly, Const_Arg_Types)
666 | ("erased", (NONE, All_Types (* naja *))) =>
667 Guards (Polymorphic, No_Types)
668 | _ => raise Same.SAME)
669 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
671 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
672 (Simple_Types (order, _, level)) =
673 Simple_Types (order, Mangled_Monomorphic, level)
674 | adjust_type_enc (THF _) type_enc = type_enc
675 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
676 Simple_Types (First_Order, Mangled_Monomorphic, level)
677 | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
678 Simple_Types (First_Order, Mangled_Monomorphic, level)
679 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
680 Simple_Types (First_Order, poly, level)
681 | adjust_type_enc format (Simple_Types (_, poly, level)) =
682 adjust_type_enc format (Guards (poly, level))
683 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
684 (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
685 | adjust_type_enc _ type_enc = type_enc
687 fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
688 | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
689 | constify_lifted (Free (x as (s, _))) =
690 (if String.isPrefix lam_lifted_prefix s then Const else Free) x
691 | constify_lifted t = t
693 (* Requires bound variables not to clash with any schematic variables (as should
694 be the case right after lambda-lifting). *)
695 fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
696 (case try unprefix s of
699 val names = Name.make_context (map fst (Term.add_var_names t' []))
700 val (s, _) = Name.variant s names
701 in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end
705 fun lift_lams_part_1 ctxt type_enc =
706 map close_form #> rpair ctxt
707 #-> Lambda_Lifting.lift_lambdas
708 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
709 lam_lifted_poly_prefix
711 lam_lifted_mono_prefix) ^ "_a"))
712 Lambda_Lifting.is_quantifier
714 fun lift_lams_part_2 (facts, lifted) =
715 (map (open_form (unprefix close_form_prefix) o constify_lifted) facts,
716 map (open_form I o constify_lifted) lifted)
717 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1
719 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
721 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
723 fun lam T t = Abs (Name.uu, T, t)
724 val (head, args) = strip_comb t ||> rev
725 val head_T = fastype_of head
727 val arg_Ts = head_T |> binder_types |> take n |> rev
728 val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
729 in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
730 | intentionalize_def t = t
732 type translated_formula =
736 iformula : (name, typ, iterm) formula,
737 atomic_types : typ list}
739 fun update_iformula f ({name, stature, kind, iformula, atomic_types}
740 : translated_formula) =
741 {name = name, stature = stature, kind = kind, iformula = f iformula,
742 atomic_types = atomic_types} : translated_formula
744 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
746 fun insert_type ctxt get_T x xs =
747 let val T = get_T x in
748 if exists (type_instance ctxt T o get_T) xs then xs
749 else x :: filter_out (type_generalization ctxt T o get_T) xs
752 (* The Booleans indicate whether all type arguments should be kept. *)
753 datatype type_arg_policy =
754 Explicit_Type_Args of bool (* infer_from_term_args *) |
758 fun type_arg_policy monom_constrs type_enc s =
759 let val poly = polymorphism_of_type_enc type_enc in
760 if s = type_tag_name then
761 if poly = Mangled_Monomorphic then Mangled_Type_Args
762 else Explicit_Type_Args false
763 else case type_enc of
764 Simple_Types (_, Polymorphic, _) => Explicit_Type_Args false
765 | Tags (_, All_Types) => No_Type_Args
767 let val level = level_of_type_enc type_enc in
768 if level = No_Types orelse s = @{const_name HOL.eq} orelse
769 (s = app_op_name andalso level = Const_Arg_Types) then
771 else if poly = Mangled_Monomorphic then
773 else if member (op =) monom_constrs s andalso
774 granularity_of_type_level level = Positively_Naked_Vars then
778 (level = All_Types orelse
779 granularity_of_type_level level = Ghost_Type_Arg_Vars)
783 (* Make atoms for sorted type variables. *)
784 fun generic_add_sorts_on_type (_, []) = I
785 | generic_add_sorts_on_type ((x, i), s :: ss) =
786 generic_add_sorts_on_type ((x, i), ss)
787 #> (if s = the_single @{sort HOL.type} then
790 insert (op =) (`make_type_class s, `make_fixed_type_var x)
792 insert (op =) (`make_type_class s,
793 (make_schematic_type_var (x, i), x)))
794 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
795 | add_sorts_on_tfree _ = I
796 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
797 | add_sorts_on_tvar _ = I
799 fun type_class_formula type_enc class arg =
800 AAtom (ATerm (class, arg ::
802 Simple_Types (First_Order, Polymorphic, _) =>
803 if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
806 fun formulas_for_types type_enc add_sorts_on_typ Ts =
807 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
808 |> map (fn (class, name) =>
809 type_class_formula type_enc class (ATerm (name, [])))
811 fun mk_aconns c phis =
812 let val (phis', phi') = split_last phis in
813 fold_rev (mk_aconn c) phis' phi'
815 fun mk_ahorn [] phi = phi
816 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
817 fun mk_aquant _ [] phi = phi
818 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
819 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
820 | mk_aquant q xs phi = AQuant (q, xs, phi)
822 fun close_universally add_term_vars phi =
824 fun add_formula_vars bounds (AQuant (_, xs, phi)) =
825 add_formula_vars (map fst xs @ bounds) phi
826 | add_formula_vars bounds (AConn (_, phis)) =
827 fold (add_formula_vars bounds) phis
828 | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
829 in mk_aquant AForall (add_formula_vars [] phi []) phi end
831 fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
832 (if is_tptp_variable s andalso
833 not (String.isPrefix tvar_prefix s) andalso
834 not (member (op =) bounds name) then
835 insert (op =) (name, NONE)
838 #> fold (add_term_vars bounds) tms
839 | add_term_vars bounds (AAbs ((name, _), tm)) =
840 add_term_vars (name :: bounds) tm
841 fun close_formula_universally phi = close_universally add_term_vars phi
843 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
844 fold (add_iterm_vars bounds) [tm1, tm2]
845 | add_iterm_vars _ (IConst _) = I
846 | add_iterm_vars bounds (IVar (name, T)) =
847 not (member (op =) bounds name) ? insert (op =) (name, SOME T)
848 | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
849 fun close_iformula_universally phi = close_universally add_iterm_vars phi
851 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
852 val fused_infinite_type = Type (fused_infinite_type_name, [])
854 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
856 fun ho_term_from_typ format type_enc =
858 fun term (Type (s, Ts)) =
859 ATerm (case (is_type_enc_higher_order type_enc, s) of
860 (true, @{type_name bool}) => `I tptp_bool_type
861 | (true, @{type_name fun}) => `I tptp_fun_type
862 | _ => if s = fused_infinite_type_name andalso
863 is_format_typed format then
864 `I tptp_individual_type
866 `make_fixed_type_const s,
868 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
869 | term (TVar (x, _)) = ATerm (tvar_name x, [])
872 fun ho_term_for_type_arg format type_enc T =
873 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
875 (* This shouldn't clash with anything else. *)
876 val mangled_type_sep = "\000"
878 fun generic_mangled_type_name f (ATerm (name, [])) = f name
879 | generic_mangled_type_name f (ATerm (name, tys)) =
880 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
882 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
884 fun mangled_type format type_enc =
885 generic_mangled_type_name fst o ho_term_from_typ format type_enc
887 fun make_simple_type s =
888 if s = tptp_bool_type orelse s = tptp_fun_type orelse
889 s = tptp_individual_type then
892 simple_type_prefix ^ ascii_of s
894 fun ho_type_from_ho_term type_enc pred_sym ary =
896 fun to_mangled_atype ty =
897 AType ((make_simple_type (generic_mangled_type_name fst ty),
898 generic_mangled_type_name snd ty), [])
899 fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
900 | to_poly_atype _ = raise Fail "unexpected type abstraction"
902 if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
903 else to_mangled_atype
904 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
905 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
906 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
907 | to_fo _ _ = raise Fail "unexpected type abstraction"
908 fun to_ho (ty as ATerm ((s, _), tys)) =
909 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
910 | to_ho _ = raise Fail "unexpected type abstraction"
911 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
913 fun ho_type_from_typ format type_enc pred_sym ary =
914 ho_type_from_ho_term type_enc pred_sym ary
915 o ho_term_from_typ format type_enc
917 fun mangled_const_name format type_enc T_args (s, s') =
919 val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
920 fun type_suffix f g =
921 fold_rev (curry (op ^) o g o prefix mangled_type_sep
922 o generic_mangled_type_name f) ty_args ""
923 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
925 val parse_mangled_ident =
926 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
928 fun parse_mangled_type x =
930 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
932 and parse_mangled_types x =
933 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
935 fun unmangled_type s =
936 s |> suffix ")" |> raw_explode
937 |> Scan.finite Symbol.stopper
938 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
939 quote s)) parse_mangled_type))
942 val unmangled_const_name = space_explode mangled_type_sep #> hd
943 fun unmangled_const s =
944 let val ss = space_explode mangled_type_sep s in
945 (hd ss, map unmangled_type (tl ss))
948 fun introduce_proxies_in_iterm type_enc =
950 fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
951 | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
953 (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
954 limitation. This works in conjuction with special code in
955 "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
958 IApp (IConst (`I ho_quant, T, []),
960 IApp (IConst (`I "P", p_T, []),
961 IConst (`I "X", x_T, [])))))
962 | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
963 fun intro top_level args (IApp (tm1, tm2)) =
964 IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
965 | intro top_level args (IConst (name as (s, _), T, T_args)) =
966 (case proxify_const s of
968 if top_level orelse is_type_enc_higher_order type_enc then
969 case (top_level, s) of
970 (_, "c_False") => IConst (`I tptp_false, T, [])
971 | (_, "c_True") => IConst (`I tptp_true, T, [])
972 | (false, "c_Not") => IConst (`I tptp_not, T, [])
973 | (false, "c_conj") => IConst (`I tptp_and, T, [])
974 | (false, "c_disj") => IConst (`I tptp_or, T, [])
975 | (false, "c_implies") => IConst (`I tptp_implies, T, [])
976 | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
977 | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
979 if is_tptp_equal s andalso length args = 2 then
980 IConst (`I tptp_equal, T, [])
982 (* Use a proxy even for partially applied THF0 equality,
983 because the LEO-II and Satallax parsers complain about not
984 being able to infer the type of "=". *)
985 IConst (proxy_base |>> prefix const_prefix, T, T_args)
986 | _ => IConst (name, T, [])
988 IConst (proxy_base |>> prefix const_prefix, T, T_args)
989 | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
990 else IConst (name, T, T_args))
991 | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
995 fun mangle_type_args_in_iterm format type_enc =
996 if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
998 fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
999 | mangle (tm as IConst (_, _, [])) = tm
1000 | mangle (tm as IConst (name as (s, _), T, T_args)) =
1001 (case unprefix_and_unascii const_prefix s of
1004 case type_arg_policy [] type_enc (invert_const s'') of
1005 Mangled_Type_Args =>
1006 IConst (mangled_const_name format type_enc T_args name, T, [])
1008 | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
1014 fun chop_fun 0 T = ([], T)
1015 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1016 chop_fun (n - 1) ran_T |>> cons dom_T
1017 | chop_fun _ T = ([], T)
1019 fun filter_const_type_args _ _ _ [] = []
1020 | filter_const_type_args thy s ary T_args =
1022 val U = robust_const_type thy s
1023 val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
1024 val U_args = (s, U) |> robust_const_typargs thy
1027 |> map (fn (U, T) =>
1028 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
1030 handle TYPE _ => T_args
1032 fun filter_type_args_in_iterm thy monom_constrs type_enc =
1034 fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
1035 | filt _ (tm as IConst (_, _, [])) = tm
1036 | filt ary (IConst (name as (s, _), T, T_args)) =
1037 (case unprefix_and_unascii const_prefix s of
1040 if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
1046 val s'' = invert_const s''
1047 fun filter_T_args false = T_args
1048 | filter_T_args true = filter_const_type_args thy s'' ary T_args
1050 case type_arg_policy monom_constrs type_enc s'' of
1051 Explicit_Type_Args infer_from_term_args =>
1052 (name, filter_T_args infer_from_term_args)
1053 | No_Type_Args => (name, [])
1054 | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
1056 |> (fn (name, T_args) => IConst (name, T, T_args))
1057 | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
1061 fun iformula_from_prop ctxt format type_enc eq_as_iff =
1063 val thy = Proof_Context.theory_of ctxt
1064 fun do_term bs t atomic_Ts =
1065 iterm_from_term thy format bs (Envir.eta_contract t)
1066 |>> (introduce_proxies_in_iterm type_enc
1067 #> mangle_type_args_in_iterm format type_enc
1069 ||> union (op =) atomic_Ts
1070 fun do_quant bs q pos s T t' =
1072 val s = singleton (Name.variant_list (map fst bs)) s
1073 val universal = Option.map (q = AExists ? not) pos
1075 s |> `(case universal of
1076 SOME true => make_all_bound_var
1077 | SOME false => make_exist_bound_var
1078 | NONE => make_bound_var)
1080 do_formula ((s, (name, T)) :: bs) pos t'
1081 #>> mk_aquant q [(name, SOME T)]
1082 ##> union (op =) (atomic_types_of T)
1084 and do_conn bs c pos1 t1 pos2 t2 =
1085 do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
1086 and do_formula bs pos t =
1088 @{const Trueprop} $ t1 => do_formula bs pos t1
1089 | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
1090 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
1091 do_quant bs AForall pos s T t'
1092 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1093 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1094 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
1095 do_quant bs AExists pos s T t'
1096 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1097 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1098 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
1099 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
1100 | @{const HOL.implies} $ t1 $ t2 =>
1101 do_conn bs AImplies (Option.map not pos) t1 pos t2
1102 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
1103 if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
1105 in do_formula [] end
1107 fun presimplify_term ctxt t =
1108 t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
1109 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
1110 #> Meson.presimplify
1113 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
1114 fun conceal_bounds Ts t =
1115 subst_bounds (map (Free o apfst concealed_bound_name)
1116 (0 upto length Ts - 1 ~~ Ts), t)
1117 fun reveal_bounds Ts =
1118 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
1119 (0 upto length Ts - 1 ~~ Ts))
1121 fun is_fun_equality (@{const_name HOL.eq},
1122 Type (_, [Type (@{type_name fun}, _), _])) = true
1123 | is_fun_equality _ = false
1125 fun extensionalize_term ctxt t =
1126 if exists_Const is_fun_equality t then
1127 let val thy = Proof_Context.theory_of ctxt in
1128 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
1129 |> prop_of |> Logic.dest_equals |> snd
1134 fun simple_translate_lambdas do_lambdas ctxt t =
1135 let val thy = Proof_Context.theory_of ctxt in
1136 if Meson.is_fol_term thy t then
1142 @{const Not} $ t1 => @{const Not} $ trans Ts t1
1143 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
1144 t0 $ Abs (s, T, trans (T :: Ts) t')
1145 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1146 trans Ts (t0 $ eta_expand Ts t1 1)
1147 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
1148 t0 $ Abs (s, T, trans (T :: Ts) t')
1149 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1150 trans Ts (t0 $ eta_expand Ts t1 1)
1151 | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
1152 t0 $ trans Ts t1 $ trans Ts t2
1153 | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
1154 t0 $ trans Ts t1 $ trans Ts t2
1155 | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
1156 t0 $ trans Ts t1 $ trans Ts t2
1157 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1159 t0 $ trans Ts t1 $ trans Ts t2
1161 if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1162 else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1163 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1164 in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
1167 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
1168 do_cheaply_conceal_lambdas Ts t1
1169 $ do_cheaply_conceal_lambdas Ts t2
1170 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
1171 Const (lam_lifted_poly_prefix ^ serial_string (),
1172 T --> fastype_of1 (T :: Ts, t))
1173 | do_cheaply_conceal_lambdas _ t = t
1175 fun do_introduce_combinators ctxt Ts t =
1176 let val thy = Proof_Context.theory_of ctxt in
1177 t |> conceal_bounds Ts
1179 |> Meson_Clausify.introduce_combinators_in_cterm
1180 |> prop_of |> Logic.dest_equals |> snd
1183 (* A type variable of sort "{}" will make abstraction fail. *)
1184 handle THM _ => t |> do_cheaply_conceal_lambdas Ts
1185 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
1187 fun preprocess_abstractions_in_terms trans_lams facts =
1189 val (facts, lambda_ts) =
1190 facts |> map (snd o snd) |> trans_lams
1191 |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
1193 map2 (fn t => fn j =>
1194 ((lam_fact_prefix ^ Int.toString j, (Global, Eq)), (Axiom, t)))
1195 lambda_ts (1 upto length lambda_ts)
1196 in (facts, lam_facts) end
1198 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
1199 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
1202 fun freeze (t $ u) = freeze t $ freeze u
1203 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
1204 | freeze (Var ((s, i), T)) =
1205 Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
1207 in t |> exists_subterm is_Var t ? freeze end
1209 fun presimp_prop ctxt role t =
1211 val thy = Proof_Context.theory_of ctxt
1212 val t = t |> Envir.beta_eta_contract
1213 |> transform_elim_prop
1214 |> Object_Logic.atomize_term thy
1215 val need_trueprop = (fastype_of t = @{typ bool})
1217 t |> need_trueprop ? HOLogic.mk_Trueprop
1218 |> extensionalize_term ctxt
1219 |> presimplify_term ctxt
1220 |> HOLogic.dest_Trueprop
1222 handle TERM _ => if role = Conjecture then @{term False} else @{term True})
1225 fun make_formula ctxt format type_enc eq_as_iff name stature kind t =
1227 val (iformula, atomic_Ts) =
1228 iformula_from_prop ctxt format type_enc eq_as_iff
1229 (SOME (kind <> Conjecture)) t []
1230 |>> close_iformula_universally
1232 {name = name, stature = stature, kind = kind, iformula = iformula,
1233 atomic_types = atomic_Ts}
1236 fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
1237 case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
1238 name stature Axiom of
1239 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1240 if s = tptp_true then NONE else SOME formula
1241 | formula => SOME formula
1243 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
1244 | s_not_trueprop t =
1245 if fastype_of t = @{typ bool} then s_not t
1246 else @{prop False} (* "t" is too meta *)
1248 fun make_conjecture ctxt format type_enc =
1249 map (fn ((name, stature), (kind, t)) =>
1250 t |> kind = Conjecture ? s_not_trueprop
1251 |> make_formula ctxt format type_enc (format <> CNF) name stature
1254 (** Finite and infinite type inference **)
1256 fun tvar_footprint thy s ary =
1257 (case unprefix_and_unascii const_prefix s of
1259 s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
1260 |> map (fn T => Term.add_tvarsT T [] |> map fst)
1264 fun ghost_type_args thy s ary =
1265 if is_tptp_equal s then
1269 val footprint = tvar_footprint thy s ary
1270 val eq = (s = @{const_name HOL.eq})
1271 fun ghosts _ [] = []
1272 | ghosts seen ((i, tvars) :: args) =
1273 ghosts (union (op =) seen tvars) args
1274 |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
1277 if forall null footprint then
1280 0 upto length footprint - 1 ~~ footprint
1281 |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
1285 type monotonicity_info =
1286 {maybe_finite_Ts : typ list,
1287 surely_finite_Ts : typ list,
1288 maybe_infinite_Ts : typ list,
1289 surely_infinite_Ts : typ list,
1290 maybe_nonmono_Ts : typ list}
1292 (* These types witness that the type classes they belong to allow infinite
1293 models and hence that any types with these type classes is monotonic. *)
1294 val known_infinite_types =
1295 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
1297 fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
1298 strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
1300 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1301 dangerous because their "exhaust" properties can easily lead to unsound ATP
1302 proofs. On the other hand, all HOL infinite types can be given the same
1303 models in first-order logic (via Löwenheim-Skolem). *)
1305 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
1306 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
1307 maybe_nonmono_Ts, ...}
1308 (Noninf_Nonmono_Types (strictness, grain)) T =
1309 grain = Ghost_Type_Arg_Vars orelse
1310 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1311 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
1312 (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
1313 is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
1315 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
1316 maybe_nonmono_Ts, ...}
1317 (Fin_Nonmono_Types grain) T =
1318 grain = Ghost_Type_Arg_Vars orelse
1319 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1320 (exists (type_generalization ctxt T) surely_finite_Ts orelse
1321 (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
1322 is_type_surely_finite ctxt T)))
1323 | should_encode_type _ _ _ _ = false
1325 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
1326 should_guard_var () andalso should_encode_type ctxt mono level T
1327 | should_guard_type _ _ _ _ _ = false
1329 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
1330 String.isPrefix bound_var_prefix s orelse
1331 String.isPrefix all_bound_var_prefix s
1332 | is_maybe_universal_var (IVar _) = true
1333 | is_maybe_universal_var _ = false
1336 Top_Level of bool option |
1337 Eq_Arg of bool option |
1340 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1341 | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
1342 if granularity_of_type_level level = All_Vars then
1343 should_encode_type ctxt mono level T
1345 (case (site, is_maybe_universal_var u) of
1346 (Eq_Arg _, true) => should_encode_type ctxt mono level T
1348 | should_tag_with_type _ _ _ _ _ _ = false
1350 fun fused_type ctxt mono level =
1352 val should_encode = should_encode_type ctxt mono level
1353 fun fuse 0 T = if should_encode T then T else fused_infinite_type
1354 | fuse ary (Type (@{type_name fun}, [T1, T2])) =
1355 fuse 0 T1 --> fuse (ary - 1) T2
1356 | fuse _ _ = raise Fail "expected function type"
1359 (** predicators and application operators **)
1362 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
1365 fun default_sym_tab_entries type_enc =
1366 (make_fixed_const NONE @{const_name undefined},
1367 {pred_sym = false, min_ary = 0, max_ary = 0, types = [],
1368 in_conj = false}) ::
1369 ([tptp_false, tptp_true]
1370 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [],
1371 in_conj = false})) @
1372 ([tptp_equal, tptp_old_equal]
1373 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [],
1375 |> not (is_type_enc_higher_order type_enc)
1376 ? cons (prefixed_predicator_name,
1377 {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
1380 fun sym_table_for_facts ctxt type_enc explicit_apply conjs facts =
1382 fun consider_var_ary const_T var_T max_ary =
1385 if ary = max_ary orelse type_instance ctxt var_T T orelse
1386 type_instance ctxt T var_T then
1389 iter (ary + 1) (range_type T)
1390 in iter 0 const_T end
1391 fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1392 if explicit_apply = NONE andalso
1393 (can dest_funT T orelse T = @{typ bool}) then
1395 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1396 fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
1397 {pred_sym = pred_sym andalso not bool_vars',
1398 min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
1399 max_ary = max_ary, types = types, in_conj = in_conj}
1401 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1403 if bool_vars' = bool_vars andalso
1404 pointer_eq (fun_var_Ts', fun_var_Ts) then
1407 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
1411 fun add_fact_syms conj_fact =
1413 fun add_iterm_syms top_level tm
1414 (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1415 let val (head, args) = strip_iterm_comb tm in
1417 IConst ((s, _), T, _) =>
1418 if String.isPrefix bound_var_prefix s orelse
1419 String.isPrefix all_bound_var_prefix s then
1420 add_universal_var T accum
1421 else if String.isPrefix exist_bound_var_prefix s then
1424 let val ary = length args in
1425 ((bool_vars, fun_var_Ts),
1426 case Symtab.lookup sym_tab s of
1427 SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
1430 pred_sym andalso top_level andalso not bool_vars
1431 val types' = types |> insert_type ctxt I T
1432 val in_conj = in_conj orelse conj_fact
1434 if is_some explicit_apply orelse
1435 pointer_eq (types', types) then
1438 fold (consider_var_ary T) fun_var_Ts min_ary
1440 Symtab.update (s, {pred_sym = pred_sym,
1441 min_ary = Int.min (ary, min_ary),
1442 max_ary = Int.max (ary, max_ary),
1443 types = types', in_conj = in_conj})
1448 val pred_sym = top_level andalso not bool_vars
1450 case explicit_apply of
1453 | NONE => fold (consider_var_ary T) fun_var_Ts ary
1455 Symtab.update_new (s,
1456 {pred_sym = pred_sym, min_ary = min_ary,
1457 max_ary = ary, types = [T], in_conj = conj_fact})
1461 | IVar (_, T) => add_universal_var T accum
1462 | IAbs ((_, T), tm) =>
1463 accum |> add_universal_var T |> add_iterm_syms false tm
1465 |> fold (add_iterm_syms false) args
1467 in K (add_iterm_syms true) |> formula_fold NONE |> fact_lift end
1469 ((false, []), Symtab.empty)
1470 |> fold (add_fact_syms true) conjs
1471 |> fold (add_fact_syms false) facts
1473 |> fold Symtab.update (default_sym_tab_entries type_enc)
1476 fun min_ary_of sym_tab s =
1477 case Symtab.lookup sym_tab s of
1478 SOME ({min_ary, ...} : sym_info) => min_ary
1480 case unprefix_and_unascii const_prefix s of
1482 let val s = s |> unmangled_const_name |> invert_const in
1483 if s = predicator_name then 1
1484 else if s = app_op_name then 2
1485 else if s = type_guard_name then 1
1490 (* True if the constant ever appears outside of the top-level position in
1491 literals, or if it appears with different arities (e.g., because of different
1492 type instantiations). If false, the constant always receives all of its
1493 arguments and is used as a predicate. *)
1494 fun is_pred_sym sym_tab s =
1495 case Symtab.lookup sym_tab s of
1496 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1497 pred_sym andalso min_ary = max_ary
1500 val app_op = `(make_fixed_const NONE) app_op_name
1501 val predicator_combconst =
1502 IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
1504 fun list_app head args = fold (curry (IApp o swap)) args head
1505 fun predicator tm = IApp (predicator_combconst, tm)
1507 fun firstorderize_fact thy monom_constrs format type_enc sym_tab =
1509 fun do_app arg head =
1511 val head_T = ityp_of head
1512 val (arg_T, res_T) = dest_funT head_T
1514 IConst (app_op, head_T --> head_T, [arg_T, res_T])
1515 |> mangle_type_args_in_iterm format type_enc
1516 in list_app app [head, arg] end
1517 fun list_app_ops head args = fold do_app args head
1518 fun introduce_app_ops tm =
1519 case strip_iterm_comb tm of
1520 (head as IConst ((s, _), _, _), args) =>
1521 args |> map introduce_app_ops
1522 |> chop (min_ary_of sym_tab s)
1525 | (head, args) => list_app_ops head (map introduce_app_ops args)
1526 fun introduce_predicators tm =
1527 case strip_iterm_comb tm of
1528 (IConst ((s, _), _, _), _) =>
1529 if is_pred_sym sym_tab s then tm else predicator tm
1530 | _ => predicator tm
1532 not (is_type_enc_higher_order type_enc)
1533 ? (introduce_app_ops #> introduce_predicators)
1534 #> filter_type_args_in_iterm thy monom_constrs type_enc
1535 in update_iformula (formula_map do_iterm) end
1537 (** Helper facts **)
1539 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
1540 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
1542 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1544 [(("COMBI", false), @{thms Meson.COMBI_def}),
1545 (("COMBK", false), @{thms Meson.COMBK_def}),
1546 (("COMBB", false), @{thms Meson.COMBB_def}),
1547 (("COMBC", false), @{thms Meson.COMBC_def}),
1548 (("COMBS", false), @{thms Meson.COMBS_def}),
1549 ((predicator_name, false), [not_ffalse, ftrue]),
1550 (("fFalse", false), [not_ffalse]),
1551 (("fFalse", true), @{thms True_or_False}),
1552 (("fTrue", false), [ftrue]),
1553 (("fTrue", true), @{thms True_or_False}),
1555 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1556 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1558 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1559 by (unfold fconj_def) fast+}),
1561 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1562 by (unfold fdisj_def) fast+}),
1563 (("fimplies", false),
1564 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1565 by (unfold fimplies_def) fast+}),
1567 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1568 However, this is done so for backward compatibility: Including the
1569 equality helpers by default in Metis breaks a few existing proofs. *)
1570 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1571 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1572 (* Partial characterization of "fAll" and "fEx". A complete characterization
1573 would require the axiom of choice for replay with Metis. *)
1574 (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
1575 (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
1576 (("If", true), @{thms if_True if_False True_or_False})]
1577 |> map (apsnd (map zero_var_indexes))
1579 fun atype_of_type_vars (Simple_Types (_, Polymorphic, _)) = SOME atype_of_types
1580 | atype_of_type_vars _ = NONE
1582 fun bound_tvars type_enc sorts Ts =
1583 (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
1584 #> mk_aquant AForall
1585 (map_filter (fn TVar (x as (s, _), _) =>
1586 SOME ((make_schematic_type_var x, s),
1587 atype_of_type_vars type_enc)
1590 fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
1591 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1592 else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
1593 |> close_formula_universally
1594 |> bound_tvars type_enc true atomic_Ts
1596 val type_tag = `(make_fixed_const NONE) type_tag_name
1598 fun type_tag_idempotence_fact format type_enc =
1600 fun var s = ATerm (`I s, [])
1601 fun tag tm = ATerm (type_tag, [var "A", tm])
1602 val tagged_var = tag (var "X")
1604 Formula (type_tag_idempotence_helper_name, Axiom,
1605 eq_formula type_enc [] false (tag tagged_var) tagged_var,
1606 NONE, isabelle_info format eqN)
1609 fun should_specialize_helper type_enc t =
1610 polymorphism_of_type_enc type_enc <> Polymorphic andalso
1611 level_of_type_enc type_enc <> No_Types andalso
1612 not (null (Term.hidden_polymorphism t))
1614 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1615 case unprefix_and_unascii const_prefix s of
1618 val thy = Proof_Context.theory_of ctxt
1619 val unmangled_s = mangled_s |> unmangled_const_name
1620 fun dub needs_fairly_sound j k =
1621 unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1622 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1623 (if needs_fairly_sound then typed_helper_suffix
1624 else untyped_helper_suffix)
1625 fun dub_and_inst needs_fairly_sound (th, j) =
1626 let val t = prop_of th in
1627 if should_specialize_helper type_enc t then
1628 map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
1634 |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Eq)), t))
1635 val make_facts = map_filter (make_fact ctxt format type_enc false)
1636 val fairly_sound = is_type_enc_fairly_sound type_enc
1639 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1640 if helper_s <> unmangled_s orelse
1641 (needs_fairly_sound andalso not fairly_sound) then
1644 ths ~~ (1 upto length ths)
1645 |> maps (dub_and_inst needs_fairly_sound)
1649 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1650 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1653 (***************************************************************)
1654 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1655 (***************************************************************)
1657 fun set_insert (x, s) = Symtab.update (x, ()) s
1659 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1661 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1662 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1664 fun classes_of_terms get_Ts =
1665 map (map snd o get_Ts)
1666 #> List.foldl add_classes Symtab.empty
1667 #> delete_type #> Symtab.keys
1669 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
1670 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
1672 fun fold_type_constrs f (Type (s, Ts)) x =
1673 fold (fold_type_constrs f) Ts (f (s, x))
1674 | fold_type_constrs _ _ x = x
1676 (* Type constructors used to instantiate overloaded constants are the only ones
1678 fun add_type_constrs_in_term thy =
1680 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1681 | add (t $ u) = add t #> add u
1683 x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
1684 | add (Abs (_, _, u)) = add u
1688 fun type_constrs_of_terms thy ts =
1689 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1691 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
1692 let val (head, args) = strip_comb t in
1693 (head |> dest_Const |> fst,
1694 fold_rev (fn t as Var ((s, _), T) =>
1695 (fn u => Abs (s, T, abstract_over (t, u)))
1696 | _ => raise Fail "expected Var") args u)
1698 | extract_lambda_def _ = raise Fail "malformed lifted lambda"
1700 fun trans_lams_from_string ctxt type_enc lam_trans =
1701 if lam_trans = no_lamsN then
1703 else if lam_trans = hide_lamsN then
1704 lift_lams ctxt type_enc ##> K []
1705 else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
1706 lift_lams ctxt type_enc
1707 else if lam_trans = combsN then
1708 map (introduce_combinators ctxt) #> rpair []
1709 else if lam_trans = combs_and_liftingN then
1710 lift_lams_part_1 ctxt type_enc
1711 ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
1713 else if lam_trans = combs_or_liftingN then
1714 lift_lams_part_1 ctxt type_enc
1715 ##> map (fn t => case head_of (strip_qnt_body @{const_name All} t) of
1716 @{term "op =::bool => bool => bool"} => t
1717 | _ => introduce_combinators ctxt (intentionalize_def t))
1719 else if lam_trans = keep_lamsN then
1720 map (Envir.eta_contract) #> rpair []
1722 error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
1724 fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
1727 val thy = Proof_Context.theory_of ctxt
1728 val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
1729 val fact_ts = facts |> map snd
1730 (* Remove existing facts from the conjecture, as this can dramatically
1731 boost an ATP's performance (for some reason). *)
1734 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1735 val facts = facts |> map (apsnd (pair Axiom))
1737 map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
1738 |> map (apsnd freeze_term)
1739 |> map2 (pair o rpair (Local, General) o string_of_int)
1740 (0 upto length hyp_ts)
1741 val ((conjs, facts), lam_facts) =
1743 |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
1744 |> (if lam_trans = no_lamsN then
1748 #> preprocess_abstractions_in_terms trans_lams
1749 #>> chop (length conjs))
1750 val conjs = conjs |> make_conjecture ctxt format type_enc
1751 val (fact_names, facts) =
1753 |> map_filter (fn (name, (_, t)) =>
1754 make_fact ctxt format type_enc true (name, t)
1755 |> Option.map (pair name))
1757 val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
1759 lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
1760 val all_ts = concl_t :: hyp_ts @ fact_ts
1761 val subs = tfree_classes_of_terms all_ts
1762 val supers = tvar_classes_of_terms all_ts
1763 val tycons = type_constrs_of_terms thy all_ts
1764 val (supers, arity_clauses) =
1765 if level_of_type_enc type_enc = No_Types then ([], [])
1766 else make_arity_clauses thy tycons supers
1767 val class_rel_clauses = make_class_rel_clauses thy subs supers
1769 (fact_names |> map single, union (op =) subs supers, conjs,
1770 facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
1773 val type_guard = `(make_fixed_const NONE) type_guard_name
1775 fun type_guard_iterm format type_enc T tm =
1776 IApp (IConst (type_guard, T --> @{typ bool}, [T])
1777 |> mangle_type_args_in_iterm format type_enc, tm)
1779 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1780 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1781 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1782 | is_var_positively_naked_in_term _ _ _ _ = true
1784 fun is_var_ghost_type_arg_in_term thy polym_constrs name pos tm accum =
1785 is_var_positively_naked_in_term name pos tm accum orelse
1787 val var = ATerm (name, [])
1788 fun is_nasty_in_term (ATerm (_, [])) = false
1789 | is_nasty_in_term (ATerm ((s, _), tms)) =
1791 val ary = length tms
1792 val polym_constr = member (op =) polym_constrs s
1793 val ghosts = ghost_type_args thy s ary
1795 exists (fn (j, tm) =>
1796 if polym_constr then
1797 member (op =) ghosts j andalso
1798 (tm = var orelse is_nasty_in_term tm)
1800 tm = var andalso member (op =) ghosts j)
1801 (0 upto ary - 1 ~~ tms)
1802 orelse (not polym_constr andalso exists is_nasty_in_term tms)
1804 | is_nasty_in_term _ = true
1805 in is_nasty_in_term tm end
1807 fun should_guard_var_in_formula thy polym_constrs level pos phi (SOME true)
1809 (case granularity_of_type_level level of
1811 | Positively_Naked_Vars =>
1812 formula_fold pos (is_var_positively_naked_in_term name) phi false
1813 | Ghost_Type_Arg_Vars =>
1814 formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name)
1816 | should_guard_var_in_formula _ _ _ _ _ _ _ = true
1818 fun always_guard_var_in_formula _ _ _ _ _ _ _ = true
1820 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
1821 | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
1822 granularity_of_type_level level <> All_Vars andalso
1823 should_encode_type ctxt mono level T
1824 | should_generate_tag_bound_decl _ _ _ _ _ = false
1826 fun mk_aterm format type_enc name T_args args =
1827 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1829 fun tag_with_type ctxt format mono type_enc pos T tm =
1830 IConst (type_tag, T --> T, [T])
1831 |> mangle_type_args_in_iterm format type_enc
1832 |> ho_term_from_iterm ctxt format mono type_enc pos
1833 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1834 | _ => raise Fail "unexpected lambda-abstraction")
1835 and ho_term_from_iterm ctxt format mono type_enc =
1839 val (head, args) = strip_iterm_comb u
1842 Top_Level pos => pos
1847 IConst (name as (s, _), _, T_args) =>
1849 val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1851 map (term arg_site) args |> mk_aterm format type_enc name T_args
1854 map (term Elsewhere) args |> mk_aterm format type_enc name []
1855 | IAbs ((name, T), tm) =>
1856 AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1858 | IApp _ => raise Fail "impossible \"IApp\""
1861 if should_tag_with_type ctxt mono type_enc site u T then
1862 tag_with_type ctxt format mono type_enc pos T t
1866 in term o Top_Level end
1867 and formula_from_iformula ctxt polym_constrs format mono type_enc
1870 val thy = Proof_Context.theory_of ctxt
1871 val level = level_of_type_enc type_enc
1872 val do_term = ho_term_from_iterm ctxt format mono type_enc
1875 Simple_Types _ => fused_type ctxt mono level 0
1876 #> ho_type_from_typ format type_enc false 0 #> SOME
1878 fun do_out_of_bound_type pos phi universal (name, T) =
1879 if should_guard_type ctxt mono type_enc
1880 (fn () => should_guard_var thy polym_constrs level pos phi
1881 universal name) T then
1883 |> type_guard_iterm format type_enc T
1884 |> do_term pos |> AAtom |> SOME
1885 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
1887 val var = ATerm (name, [])
1888 val tagged_var = tag_with_type ctxt format mono type_enc pos T var
1889 in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
1892 fun do_formula pos (AQuant (q, xs, phi)) =
1894 val phi = phi |> do_formula pos
1895 val universal = Option.map (q = AExists ? not) pos
1897 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1898 | SOME T => do_bound_type T)),
1899 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1901 (fn (_, NONE) => NONE
1903 do_out_of_bound_type pos phi universal (s, T))
1907 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1908 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1911 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1912 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1913 the remote provers might care. *)
1914 fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
1915 mono type_enc (j, {name, stature, kind, iformula, atomic_types}) =
1916 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
1918 |> formula_from_iformula ctxt polym_constrs format mono type_enc
1919 should_guard_var_in_formula (if pos then SOME true else NONE)
1920 |> close_formula_universally
1921 |> bound_tvars type_enc true atomic_types,
1924 Intro => isabelle_info format introN
1925 | Elim => isabelle_info format elimN
1926 | Simp => isabelle_info format simpN
1927 | Eq => isabelle_info format eqN
1931 fun formula_line_for_class_rel_clause format type_enc
1932 ({name, subclass, superclass, ...} : class_rel_clause) =
1933 let val ty_arg = ATerm (tvar_a_name, []) in
1934 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1936 [type_class_formula type_enc subclass ty_arg,
1937 type_class_formula type_enc superclass ty_arg])
1938 |> mk_aquant AForall
1939 [(tvar_a_name, atype_of_type_vars type_enc)],
1940 NONE, isabelle_info format introN)
1943 fun formula_from_arity_atom type_enc (class, t, args) =
1944 ATerm (t, map (fn arg => ATerm (arg, [])) args)
1945 |> type_class_formula type_enc class
1947 fun formula_line_for_arity_clause format type_enc
1948 ({name, prem_atoms, concl_atom} : arity_clause) =
1949 Formula (arity_clause_prefix ^ name, Axiom,
1950 mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
1951 (formula_from_arity_atom type_enc concl_atom)
1952 |> mk_aquant AForall
1953 (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
1954 NONE, isabelle_info format introN)
1956 fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
1957 ({name, kind, iformula, atomic_types, ...} : translated_formula) =
1958 Formula (conjecture_prefix ^ name, kind,
1960 |> formula_from_iformula ctxt polym_constrs format mono type_enc
1961 should_guard_var_in_formula (SOME false)
1962 |> close_formula_universally
1963 |> bound_tvars type_enc true atomic_types, NONE, NONE)
1965 fun formula_line_for_free_type j phi =
1966 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
1967 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
1970 fold (union (op =)) (map #atomic_types facts) []
1971 |> formulas_for_types type_enc add_sorts_on_tfree
1972 in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
1974 (** Symbol declarations **)
1976 fun decl_line_for_class order s =
1977 let val name as (s, _) = `make_type_class s in
1978 Decl (sym_decl_prefix ^ s, name,
1979 if order = First_Order then
1980 ATyAbs ([tvar_a_name],
1981 if avoid_first_order_ghost_type_vars then
1982 AFun (a_itself_atype, bool_atype)
1986 AFun (atype_of_types, bool_atype))
1989 fun decl_lines_for_classes type_enc classes =
1991 Simple_Types (order, Polymorphic, _) =>
1992 map (decl_line_for_class order) classes
1995 fun sym_decl_table_for_facts ctxt format type_enc sym_tab (conjs, facts) =
1997 fun add_iterm_syms tm =
1998 let val (head, args) = strip_iterm_comb tm in
2000 IConst ((s, s'), T, T_args) =>
2002 val (pred_sym, in_conj) =
2003 case Symtab.lookup sym_tab s of
2004 SOME ({pred_sym, in_conj, ...} : sym_info) =>
2006 | NONE => (false, false)
2009 Guards _ => not pred_sym
2010 | _ => true) andalso
2011 is_tptp_user_symbol s
2014 Symtab.map_default (s, [])
2015 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
2020 | IAbs (_, tm) => add_iterm_syms tm
2022 #> fold add_iterm_syms args
2024 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
2025 fun add_formula_var_types (AQuant (_, xs, phi)) =
2026 fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
2027 #> add_formula_var_types phi
2028 | add_formula_var_types (AConn (_, phis)) =
2029 fold add_formula_var_types phis
2030 | add_formula_var_types _ = I
2032 if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
2033 else fold (fact_lift add_formula_var_types) (conjs @ facts) []
2034 fun add_undefined_const T =
2037 `(make_fixed_const NONE) @{const_name undefined}
2038 |> (case type_arg_policy [] type_enc @{const_name undefined} of
2039 Mangled_Type_Args => mangled_const_name format type_enc [T]
2042 Symtab.map_default (s, [])
2043 (insert_type ctxt #3 (s', [T], T, false, 0, false))
2045 fun add_TYPE_const () =
2046 let val (s, s') = TYPE_name in
2047 Symtab.map_default (s, [])
2048 (insert_type ctxt #3
2049 (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
2053 |> is_type_enc_fairly_sound type_enc
2054 ? (fold (fold add_fact_syms) [conjs, facts]
2055 #> (case type_enc of
2056 Simple_Types (First_Order, Polymorphic, _) =>
2057 if avoid_first_order_ghost_type_vars then add_TYPE_const ()
2059 | Simple_Types _ => I
2060 | _ => fold add_undefined_const (var_types ())))
2063 (* We add "bool" in case the helper "True_or_False" is included later. *)
2064 fun default_mono level =
2065 {maybe_finite_Ts = [@{typ bool}],
2066 surely_finite_Ts = [@{typ bool}],
2067 maybe_infinite_Ts = known_infinite_types,
2068 surely_infinite_Ts =
2070 Noninf_Nonmono_Types (Strict, _) => []
2071 | _ => known_infinite_types,
2072 maybe_nonmono_Ts = [@{typ bool}]}
2074 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
2075 out with monotonicity" paper presented at CADE 2011. *)
2076 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
2077 | add_iterm_mononotonicity_info ctxt level _
2078 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
2079 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
2080 surely_infinite_Ts, maybe_nonmono_Ts}) =
2081 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
2083 Noninf_Nonmono_Types (strictness, _) =>
2084 if exists (type_instance ctxt T) surely_infinite_Ts orelse
2085 member (type_equiv ctxt) maybe_finite_Ts T then
2087 else if is_type_kind_of_surely_infinite ctxt strictness
2088 surely_infinite_Ts T then
2089 {maybe_finite_Ts = maybe_finite_Ts,
2090 surely_finite_Ts = surely_finite_Ts,
2091 maybe_infinite_Ts = maybe_infinite_Ts,
2092 surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
2093 maybe_nonmono_Ts = maybe_nonmono_Ts}
2095 {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
2096 surely_finite_Ts = surely_finite_Ts,
2097 maybe_infinite_Ts = maybe_infinite_Ts,
2098 surely_infinite_Ts = surely_infinite_Ts,
2099 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2100 | Fin_Nonmono_Types _ =>
2101 if exists (type_instance ctxt T) surely_finite_Ts orelse
2102 member (type_equiv ctxt) maybe_infinite_Ts T then
2104 else if is_type_surely_finite ctxt T then
2105 {maybe_finite_Ts = maybe_finite_Ts,
2106 surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
2107 maybe_infinite_Ts = maybe_infinite_Ts,
2108 surely_infinite_Ts = surely_infinite_Ts,
2109 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2111 {maybe_finite_Ts = maybe_finite_Ts,
2112 surely_finite_Ts = surely_finite_Ts,
2113 maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
2114 surely_infinite_Ts = surely_infinite_Ts,
2115 maybe_nonmono_Ts = maybe_nonmono_Ts}
2119 | add_iterm_mononotonicity_info _ _ _ _ mono = mono
2120 fun add_fact_mononotonicity_info ctxt level
2121 ({kind, iformula, ...} : translated_formula) =
2122 formula_fold (SOME (kind <> Conjecture))
2123 (add_iterm_mononotonicity_info ctxt level) iformula
2124 fun mononotonicity_info_for_facts ctxt type_enc facts =
2125 let val level = level_of_type_enc type_enc in
2127 |> is_type_level_monotonicity_based level
2128 ? fold (add_fact_mononotonicity_info ctxt level) facts
2131 fun add_iformula_monotonic_types ctxt mono type_enc =
2133 val level = level_of_type_enc type_enc
2134 val should_encode = should_encode_type ctxt mono level
2135 fun add_type T = not (should_encode T) ? insert_type ctxt I T
2136 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
2138 and add_term tm = add_type (ityp_of tm) #> add_args tm
2139 in formula_fold NONE (K add_term) end
2140 fun add_fact_monotonic_types ctxt mono type_enc =
2141 add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
2142 fun monotonic_types_for_facts ctxt mono type_enc facts =
2143 let val level = level_of_type_enc type_enc in
2144 [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
2145 is_type_level_monotonicity_based level andalso
2146 granularity_of_type_level level <> Ghost_Type_Arg_Vars)
2147 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
2150 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
2151 Formula (guards_sym_formula_prefix ^
2152 ascii_of (mangled_type format type_enc T),
2154 IConst (`make_bound_var "X", T, [])
2155 |> type_guard_iterm format type_enc T
2157 |> formula_from_iformula ctxt [] format mono type_enc
2158 always_guard_var_in_formula (SOME true)
2159 |> close_formula_universally
2160 |> bound_tvars type_enc true (atomic_types_of T),
2161 NONE, isabelle_info format introN)
2163 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
2164 let val x_var = ATerm (`make_bound_var "X", []) in
2165 Formula (tags_sym_formula_prefix ^
2166 ascii_of (mangled_type format type_enc T),
2168 eq_formula type_enc (atomic_types_of T) false
2169 (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
2170 NONE, isabelle_info format eqN)
2173 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
2175 Simple_Types _ => []
2177 map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
2178 | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
2180 fun decl_line_for_sym ctxt format mono type_enc s
2181 (s', T_args, T, pred_sym, ary, _) =
2183 val thy = Proof_Context.theory_of ctxt
2187 else case unprefix_and_unascii const_prefix s of
2190 val s' = s' |> invert_const
2191 val T = s' |> robust_const_type thy
2192 in (T, robust_const_typargs thy (s', T)) end
2193 | NONE => raise Fail "unexpected type arguments"
2195 Decl (sym_decl_prefix ^ s, (s, s'),
2196 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
2197 |> ho_type_from_typ format type_enc pred_sym ary
2198 |> not (null T_args)
2199 ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
2202 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
2203 j (s', T_args, T, _, ary, in_conj) =
2205 val thy = Proof_Context.theory_of ctxt
2206 val (kind, maybe_negate) =
2207 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
2209 val (arg_Ts, res_T) = chop_fun ary T
2210 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2212 bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
2214 if exists (curry (op =) dummyT) T_args then
2215 case level_of_type_enc type_enc of
2216 All_Types => map SOME arg_Ts
2218 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
2219 let val ghosts = ghost_type_args thy s ary in
2220 map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
2221 (0 upto ary - 1) arg_Ts
2228 Formula (guards_sym_formula_prefix ^ s ^
2229 (if n > 1 then "_" ^ string_of_int j else ""), kind,
2230 IConst ((s, s'), T, T_args)
2231 |> fold (curry (IApp o swap)) bounds
2232 |> type_guard_iterm format type_enc res_T
2233 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
2234 |> formula_from_iformula ctxt [] format mono type_enc
2235 always_guard_var_in_formula (SOME true)
2236 |> close_formula_universally
2237 |> bound_tvars type_enc (n > 1) (atomic_types_of T)
2239 NONE, isabelle_info format introN)
2242 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
2243 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
2245 val thy = Proof_Context.theory_of ctxt
2246 val level = level_of_type_enc type_enc
2247 val grain = granularity_of_type_level level
2249 tags_sym_formula_prefix ^ s ^
2250 (if n > 1 then "_" ^ string_of_int j else "")
2251 val (kind, maybe_negate) =
2252 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
2254 val (arg_Ts, res_T) = chop_fun ary T
2255 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2256 val bounds = bound_names |> map (fn name => ATerm (name, []))
2257 val cst = mk_aterm format type_enc (s, s') T_args
2258 val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) pred_sym
2259 val should_encode = should_encode_type ctxt mono level
2260 val tag_with = tag_with_type ctxt format mono type_enc NONE
2261 val add_formula_for_res =
2262 if should_encode res_T then
2265 if grain = Ghost_Type_Arg_Vars then
2266 let val ghosts = ghost_type_args thy s ary in
2267 map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
2268 (0 upto ary - 1 ~~ arg_Ts) bounds
2273 cons (Formula (ident_base ^ "_res", kind,
2274 eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
2275 NONE, isabelle_info format eqN))
2279 fun add_formula_for_arg k =
2280 let val arg_T = nth arg_Ts k in
2281 if should_encode arg_T then
2282 case chop k bounds of
2283 (bounds1, bound :: bounds2) =>
2284 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
2285 eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
2287 NONE, isabelle_info format eqN))
2288 | _ => raise Fail "expected nonempty tail"
2293 [] |> not pred_sym ? add_formula_for_res
2294 |> (Config.get ctxt type_tag_arguments andalso
2295 grain = Positively_Naked_Vars)
2296 ? fold add_formula_for_arg (ary - 1 downto 0)
2299 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
2301 fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
2303 val T = result_type_of_decl decl
2304 |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
2306 if forall (type_generalization ctxt T o result_type_of_decl) decls' then
2311 | rationalize_decls _ decls = decls
2313 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
2316 Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
2317 | Guards (_, level) =>
2319 val decls = decls |> rationalize_decls ctxt
2320 val n = length decls
2322 decls |> filter (should_encode_type ctxt mono level
2323 o result_type_of_decl)
2325 (0 upto length decls - 1, decls)
2326 |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
2329 | Tags (_, level) =>
2330 if granularity_of_type_level level = All_Vars then
2333 let val n = length decls in
2334 (0 upto n - 1 ~~ decls)
2335 |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono
2339 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
2340 mono_Ts sym_decl_tab =
2342 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
2344 problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
2346 fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
2349 in mono_lines @ decl_lines end
2351 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
2352 Config.get ctxt type_tag_idempotence andalso
2353 is_type_level_monotonicity_based level andalso
2354 poly <> Mangled_Monomorphic
2355 | needs_type_tag_idempotence _ _ = false
2357 val implicit_declsN = "Should-be-implicit typings"
2358 val explicit_declsN = "Explicit typings"
2359 val factsN = "Relevant facts"
2360 val class_relsN = "Class relationships"
2361 val aritiesN = "Arities"
2362 val helpersN = "Helper facts"
2363 val conjsN = "Conjectures"
2364 val free_typesN = "Type variables"
2366 (* TFF allows implicit declarations of types, function symbols, and predicate
2367 symbols (with "$i" as the type of individuals), but some provers (e.g.,
2368 SNARK) require explicit declarations. The situation is similar for THF. *)
2370 fun default_type type_enc pred_sym s =
2375 if String.isPrefix type_const_prefix s then atype_of_types
2376 else individual_atype
2377 | _ => individual_atype
2378 fun typ 0 = if pred_sym then bool_atype else ind
2379 | typ ary = AFun (ind, typ (ary - 1))
2382 fun nary_type_constr_type n =
2383 funpow n (curry AFun atype_of_types) atype_of_types
2385 fun undeclared_syms_in_problem type_enc problem =
2387 val declared = declared_syms_in_problem problem
2388 fun do_sym name ty =
2389 if member (op =) declared name then I else AList.default (op =) (name, ty)
2390 fun do_type (AType (name as (s, _), tys)) =
2391 is_tptp_user_symbol s
2392 ? do_sym name (fn () => nary_type_constr_type (length tys))
2394 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
2395 | do_type (ATyAbs (_, ty)) = do_type ty
2396 fun do_term pred_sym (ATerm (name as (s, _), tms)) =
2397 is_tptp_user_symbol s
2398 ? do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
2399 #> fold (do_term false) tms
2400 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
2401 fun do_formula (AQuant (_, xs, phi)) =
2402 fold do_type (map_filter snd xs) #> do_formula phi
2403 | do_formula (AConn (_, phis)) = fold do_formula phis
2404 | do_formula (AAtom tm) = do_term true tm
2405 fun do_problem_line (Decl (_, _, ty)) = do_type ty
2406 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
2408 fold (fold do_problem_line o snd) problem []
2409 |> filter_out (is_built_in_tptp_symbol o fst o fst)
2412 fun declare_undeclared_syms_in_atp_problem type_enc problem =
2416 |> undeclared_syms_in_problem type_enc
2417 |> sort_wrt (fst o fst)
2418 |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
2419 in (implicit_declsN, decls) :: problem end
2421 fun exists_subdtype P =
2423 fun ex U = P U orelse
2424 (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false)
2427 fun is_poly_constr (_, Us) =
2428 exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
2430 fun all_constrs_of_polymorphic_datatypes thy =
2434 #> (fn cs => exists is_poly_constr cs ? append cs))
2435 (Datatype.get_all thy) []
2436 |> List.partition is_poly_constr
2437 |> pairself (map fst)
2439 (* Forcing explicit applications is expensive for polymorphic encodings, because
2440 it takes only one existential variable ranging over "'a => 'b" to ruin
2441 everything. Hence we do it only if there are few facts (which is normally the
2442 case for "metis" and the minimizer). *)
2443 val explicit_apply_threshold = 50
2445 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
2446 lam_trans readable_names preproc hyp_ts concl_t facts =
2448 val thy = Proof_Context.theory_of ctxt
2449 val type_enc = type_enc |> adjust_type_enc format
2450 val explicit_apply =
2451 if polymorphism_of_type_enc type_enc = Polymorphic andalso
2452 length facts >= explicit_apply_threshold then
2457 if lam_trans = keep_lamsN andalso
2458 not (is_type_enc_higher_order type_enc) then
2459 error ("Lambda translation scheme incompatible with first-order \
2463 val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
2465 translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
2467 val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts
2468 val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
2469 val (polym_constrs, monom_constrs) =
2470 all_constrs_of_polymorphic_datatypes thy
2471 |>> map (make_fixed_const (SOME format))
2473 firstorderize_fact thy monom_constrs format type_enc sym_tab
2474 val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
2475 val sym_tab = sym_table_for_facts ctxt type_enc (SOME false) conjs facts
2477 sym_tab |> helper_facts_for_sym_table ctxt format type_enc
2478 |> map firstorderize
2480 helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
2481 val class_decl_lines = decl_lines_for_classes type_enc classes
2482 val sym_decl_lines =
2483 (conjs, helpers @ facts)
2484 |> sym_decl_table_for_facts ctxt format type_enc sym_tab
2485 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
2488 0 upto length helpers - 1 ~~ helpers
2489 |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I
2490 false true mono type_enc)
2491 |> (if needs_type_tag_idempotence ctxt type_enc then
2492 cons (type_tag_idempotence_fact format type_enc)
2495 (* Reordering these might confuse the proof reconstruction code or the SPASS
2498 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
2500 map (formula_line_for_fact ctxt polym_constrs format fact_prefix
2501 ascii_of (not exporter) (not exporter) mono type_enc)
2502 (0 upto length facts - 1 ~~ facts)),
2504 map (formula_line_for_class_rel_clause format type_enc)
2507 map (formula_line_for_arity_clause format type_enc) arity_clauses),
2508 (helpersN, helper_lines),
2510 map (formula_line_for_conjecture ctxt polym_constrs format mono
2512 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
2516 CNF => ensure_cnf_problem
2517 | CNF_UEQ => filter_cnf_ueq_problem
2519 | TFF (_, TPTP_Implicit) => I
2520 | THF (_, TPTP_Implicit, _) => I
2521 | _ => declare_undeclared_syms_in_atp_problem type_enc)
2522 val (problem, pool) = problem |> nice_atp_problem readable_names format
2523 fun add_sym_ary (s, {min_ary, ...} : sym_info) =
2524 min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
2527 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
2528 fact_names |> Vector.fromList,
2530 Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
2534 val conj_weight = 0.0
2535 val hyp_weight = 0.1
2536 val fact_min_weight = 0.2
2537 val fact_max_weight = 1.0
2538 val type_info_default_weight = 0.8
2540 fun add_term_weights weight (ATerm (s, tms)) =
2541 is_tptp_user_symbol s ? Symtab.default (s, weight)
2542 #> fold (add_term_weights weight) tms
2543 | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
2544 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
2545 formula_fold NONE (K (add_term_weights weight)) phi
2546 | add_problem_line_weights _ _ = I
2548 fun add_conjectures_weights [] = I
2549 | add_conjectures_weights conjs =
2550 let val (hyps, conj) = split_last conjs in
2551 add_problem_line_weights conj_weight conj
2552 #> fold (add_problem_line_weights hyp_weight) hyps
2555 fun add_facts_weights facts =
2557 val num_facts = length facts
2559 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
2560 / Real.fromInt num_facts
2562 map weight_of (0 upto num_facts - 1) ~~ facts
2563 |> fold (uncurry add_problem_line_weights)
2566 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
2567 fun atp_problem_weights problem =
2568 let val get = these o AList.lookup (op =) problem in
2570 |> add_conjectures_weights (get free_typesN @ get conjsN)
2571 |> add_facts_weights (get factsN)
2572 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
2573 [explicit_declsN, class_relsN, aritiesN]
2575 |> sort (prod_ord Real.compare string_ord o pairself swap)