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
19 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
21 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
22 datatype strictness = Strict | Non_Strict
23 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
26 Noninf_Nonmono_Types of strictness * granularity |
27 Fin_Nonmono_Types of granularity |
32 val type_tag_idempotence : bool Config.T
33 val type_tag_arguments : bool Config.T
35 val hide_lamsN : string
36 val lam_liftingN : string
37 val combinatorsN : string
38 val hybrid_lamsN : string
39 val keep_lamsN : string
40 val schematic_var_prefix : string
41 val fixed_var_prefix : string
42 val tvar_prefix : string
43 val tfree_prefix : string
44 val const_prefix : string
45 val type_const_prefix : string
46 val class_prefix : string
47 val lam_lifted_prefix : string
48 val lam_lifted_mono_prefix : string
49 val lam_lifted_poly_prefix : string
50 val skolem_const_prefix : string
51 val old_skolem_const_prefix : string
52 val new_skolem_const_prefix : string
53 val combinator_prefix : string
54 val type_decl_prefix : string
55 val sym_decl_prefix : string
56 val guards_sym_formula_prefix : string
57 val tags_sym_formula_prefix : string
58 val fact_prefix : string
59 val conjecture_prefix : string
60 val helper_prefix : string
61 val class_rel_clause_prefix : string
62 val arity_clause_prefix : string
63 val tfree_clause_prefix : string
64 val lam_fact_prefix : string
65 val typed_helper_suffix : string
66 val untyped_helper_suffix : string
67 val type_tag_idempotence_helper_name : string
68 val predicator_name : string
69 val app_op_name : string
70 val type_guard_name : string
71 val type_tag_name : string
72 val simple_type_prefix : string
73 val prefixed_predicator_name : string
74 val prefixed_app_op_name : string
75 val prefixed_type_tag_name : string
76 val ascii_of : string -> string
77 val unascii_of : string -> string
78 val unprefix_and_unascii : string -> string -> string option
79 val proxy_table : (string * (string * (thm * (string * string)))) list
80 val proxify_const : string -> (string * string) option
81 val invert_const : string -> string
82 val unproxify_const : string -> string
83 val new_skolem_var_name_from_const : string -> string
84 val atp_irrelevant_consts : string list
85 val atp_schematic_consts_of : term -> typ list Symtab.table
86 val is_type_enc_higher_order : type_enc -> bool
87 val polymorphism_of_type_enc : type_enc -> polymorphism
88 val level_of_type_enc : type_enc -> type_level
89 val is_type_enc_quasi_sound : type_enc -> bool
90 val is_type_enc_fairly_sound : type_enc -> bool
91 val type_enc_from_string : strictness -> string -> type_enc
92 val adjust_type_enc : atp_format -> type_enc -> type_enc
94 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
95 val unmangled_const : string -> string * (string, 'b) ho_term list
96 val unmangled_const_name : string -> string
97 val helper_table : ((string * bool) * thm list) list
98 val trans_lams_from_string :
99 Proof.context -> type_enc -> string -> term list -> term list * term list
101 val prepare_atp_problem :
102 Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
103 -> bool -> string -> bool -> bool -> term list -> term
104 -> ((string * locality) * term) list
105 -> string problem * string Symtab.table * (string * locality) list vector
106 * (string * term) list * int Symtab.table
107 val atp_problem_weights : string problem -> (string * real) list
110 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
116 type name = string * string
118 val type_tag_idempotence =
119 Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
120 val type_tag_arguments =
121 Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
123 val no_lamsN = "no_lams" (* used internally; undocumented *)
124 val hide_lamsN = "hide_lams"
125 val lam_liftingN = "lam_lifting"
126 val combinatorsN = "combinators"
127 val hybrid_lamsN = "hybrid_lams"
128 val keep_lamsN = "keep_lams"
130 (* It's still unclear whether all TFF1 implementations will support type
131 signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
132 val avoid_first_order_ghost_type_vars = false
134 val bound_var_prefix = "B_"
135 val all_bound_var_prefix = "BA_"
136 val exist_bound_var_prefix = "BE_"
137 val schematic_var_prefix = "V_"
138 val fixed_var_prefix = "v_"
139 val tvar_prefix = "T_"
140 val tfree_prefix = "t_"
141 val const_prefix = "c_"
142 val type_const_prefix = "tc_"
143 val simple_type_prefix = "s_"
144 val class_prefix = "cl_"
146 (* Freshness almost guaranteed! *)
147 val atp_weak_prefix = "ATP:"
149 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
150 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
151 val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
153 val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
154 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
155 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
157 val combinator_prefix = "COMB"
159 val type_decl_prefix = "ty_"
160 val sym_decl_prefix = "sy_"
161 val guards_sym_formula_prefix = "gsy_"
162 val tags_sym_formula_prefix = "tsy_"
163 val fact_prefix = "fact_"
164 val conjecture_prefix = "conj_"
165 val helper_prefix = "help_"
166 val class_rel_clause_prefix = "clar_"
167 val arity_clause_prefix = "arity_"
168 val tfree_clause_prefix = "tfree_"
170 val lam_fact_prefix = "ATP.lambda_"
171 val typed_helper_suffix = "_T"
172 val untyped_helper_suffix = "_U"
173 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
175 val predicator_name = "pp"
176 val app_op_name = "aa"
177 val type_guard_name = "gg"
178 val type_tag_name = "tt"
180 val prefixed_predicator_name = const_prefix ^ predicator_name
181 val prefixed_app_op_name = const_prefix ^ app_op_name
182 val prefixed_type_tag_name = const_prefix ^ type_tag_name
184 (*Escaping of special characters.
185 Alphanumeric characters are left unchanged.
186 The character _ goes to __
187 Characters in the range ASCII space to / go to _A to _P, respectively.
188 Other characters go to _nnn where nnn is the decimal ASCII code.*)
189 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
191 fun stringN_of_int 0 _ = ""
192 | stringN_of_int k n =
193 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
195 fun ascii_of_char c =
196 if Char.isAlphaNum c then
198 else if c = #"_" then
200 else if #" " <= c andalso c <= #"/" then
201 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
203 (* fixed width, in case more digits follow *)
204 "_" ^ stringN_of_int 3 (Char.ord c)
206 val ascii_of = String.translate ascii_of_char
208 (** Remove ASCII armoring from names in proof files **)
210 (* We don't raise error exceptions because this code can run inside a worker
211 thread. Also, the errors are impossible. *)
214 fun un rcs [] = String.implode(rev rcs)
215 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
216 (* Three types of _ escapes: __, _A to _P, _nnn *)
217 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
218 | un rcs (#"_" :: c :: cs) =
219 if #"A" <= c andalso c<= #"P" then
220 (* translation of #" " to #"/" *)
221 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
223 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
224 case Int.fromString (String.implode digits) of
225 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
226 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
228 | un rcs (c :: cs) = un (c :: rcs) cs
229 in un [] o String.explode end
231 (* If string s has the prefix s1, return the result of deleting it,
233 fun unprefix_and_unascii s1 s =
234 if String.isPrefix s1 s then
235 SOME (unascii_of (String.extract (s, size s1, NONE)))
240 [("c_False", (@{const_name False}, (@{thm fFalse_def},
241 ("fFalse", @{const_name ATP.fFalse})))),
242 ("c_True", (@{const_name True}, (@{thm fTrue_def},
243 ("fTrue", @{const_name ATP.fTrue})))),
244 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
245 ("fNot", @{const_name ATP.fNot})))),
246 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
247 ("fconj", @{const_name ATP.fconj})))),
248 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
249 ("fdisj", @{const_name ATP.fdisj})))),
250 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
251 ("fimplies", @{const_name ATP.fimplies})))),
252 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
253 ("fequal", @{const_name ATP.fequal})))),
254 ("c_All", (@{const_name All}, (@{thm fAll_def},
255 ("fAll", @{const_name ATP.fAll})))),
256 ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
257 ("fEx", @{const_name ATP.fEx}))))]
259 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
261 (* Readable names for the more common symbolic functions. Do not mess with the
262 table unless you know what you are doing. *)
263 val const_trans_table =
264 [(@{type_name Product_Type.prod}, "prod"),
265 (@{type_name Sum_Type.sum}, "sum"),
266 (@{const_name False}, "False"),
267 (@{const_name True}, "True"),
268 (@{const_name Not}, "Not"),
269 (@{const_name conj}, "conj"),
270 (@{const_name disj}, "disj"),
271 (@{const_name implies}, "implies"),
272 (@{const_name HOL.eq}, "equal"),
273 (@{const_name All}, "All"),
274 (@{const_name Ex}, "Ex"),
275 (@{const_name If}, "If"),
276 (@{const_name Set.member}, "member"),
277 (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
278 (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
279 (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
280 (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
281 (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
283 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
285 (* Invert the table of translations between Isabelle and ATPs. *)
286 val const_trans_table_inv =
287 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
288 val const_trans_table_unprox =
290 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
292 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
293 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
296 case Symtab.lookup const_trans_table c of
300 fun ascii_of_indexname (v, 0) = ascii_of v
301 | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
303 fun make_bound_var x = bound_var_prefix ^ ascii_of x
304 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
305 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
306 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
307 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
309 fun make_schematic_type_var (x, i) =
310 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
311 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
313 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
315 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
316 fun default c = const_prefix ^ lookup_const c
318 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
319 | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
320 if c = choice_const then tptp_choice else default c
321 | make_fixed_const _ c = default c
324 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
326 fun make_type_class clas = class_prefix ^ ascii_of clas
328 fun new_skolem_var_name_from_const s =
329 let val ss = s |> space_explode Long_Name.separator in
330 nth ss (length ss - 2)
333 (* These are either simplified away by "Meson.presimplify" (most of the time) or
334 handled specially via "fFalse", "fTrue", ..., "fequal". *)
335 val atp_irrelevant_consts =
336 [@{const_name False}, @{const_name True}, @{const_name Not},
337 @{const_name conj}, @{const_name disj}, @{const_name implies},
338 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
340 val atp_monomorph_bad_consts =
341 atp_irrelevant_consts @
342 (* These are ignored anyway by the relevance filter (unless they appear in
343 higher-order places) but not by the monomorphizer. *)
344 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
345 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
346 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
348 fun add_schematic_const (x as (_, T)) =
349 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
350 val add_schematic_consts_of =
351 Term.fold_aterms (fn Const (x as (s, _)) =>
352 not (member (op =) atp_monomorph_bad_consts s)
353 ? add_schematic_const x
355 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
357 (** Definitions and functions for FOL clauses and formulas for TPTP **)
359 (** Isabelle arities **)
361 type arity_atom = name * name * name list
363 val type_class = the_single @{sort type}
367 prem_atoms : arity_atom list,
368 concl_atom : arity_atom}
370 fun add_prem_atom tvar =
371 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
373 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
374 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
376 val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
377 val tvars_srts = ListPair.zip (tvars, args)
380 prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
381 concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
385 fun arity_clause _ _ (_, []) = []
386 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
387 arity_clause seen n (tcons, ars)
388 | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
389 if member (op =) seen class then
390 (* multiple arities for the same (tycon, class) pair *)
391 make_axiom_arity_clause (tcons,
392 lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
394 arity_clause seen (n + 1) (tcons, ars)
396 make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
397 ascii_of class, ar) ::
398 arity_clause (class :: seen) n (tcons, ars)
400 fun multi_arity_clause [] = []
401 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
402 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
404 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
405 theory thy provided its arguments have the corresponding sorts. *)
406 fun type_class_pairs thy tycons classes =
408 val alg = Sign.classes_of thy
409 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
410 fun add_class tycon class =
411 cons (class, domain_sorts tycon class)
412 handle Sorts.CLASS_ERROR _ => I
413 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
414 in map try_classes tycons end
416 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
417 fun iter_type_class_pairs _ _ [] = ([], [])
418 | iter_type_class_pairs thy tycons classes =
420 fun maybe_insert_class s =
421 (s <> type_class andalso not (member (op =) classes s))
423 val cpairs = type_class_pairs thy tycons classes
425 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
426 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
427 in (classes' @ classes, union (op =) cpairs' cpairs) end
429 fun make_arity_clauses thy tycons =
430 iter_type_class_pairs thy tycons ##> multi_arity_clause
433 (** Isabelle class relations **)
435 type class_rel_clause =
440 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
442 fun class_pairs _ [] _ = []
443 | class_pairs thy subs supers =
445 val class_less = Sorts.class_less (Sign.classes_of thy)
446 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
447 fun add_supers sub = fold (add_super sub) supers
448 in fold add_supers subs [] end
450 fun make_class_rel_clause (sub, super) =
451 {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
452 superclass = `make_type_class super}
454 fun make_class_rel_clauses thy subs supers =
455 map make_class_rel_clause (class_pairs thy subs supers)
457 (* intermediate terms *)
459 IConst of name * typ * typ list |
461 IApp of iterm * iterm |
462 IAbs of (name * typ) * iterm
464 fun ityp_of (IConst (_, T, _)) = T
465 | ityp_of (IVar (_, T)) = T
466 | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
467 | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
469 (*gets the head of a combinator application, along with the list of arguments*)
470 fun strip_iterm_comb u =
472 fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
474 in stripc (u, []) end
476 fun atomic_types_of T = fold_atyps (insert (op =)) T []
478 val tvar_a_str = "'a"
479 val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
480 val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
481 val itself_name = `make_fixed_type_const @{type_name itself}
482 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
483 val tvar_a_atype = AType (tvar_a_name, [])
484 val a_itself_atype = AType (itself_name, [tvar_a_atype])
486 fun new_skolem_const_name s num_T_args =
487 [new_skolem_const_prefix, s, string_of_int num_T_args]
488 |> space_implode Long_Name.separator
490 fun robust_const_type thy s =
491 if s = app_op_name then
492 Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
493 else if String.isPrefix lam_lifted_prefix s then
494 Logic.varifyT_global @{typ "'a => 'b"}
496 (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
497 s |> Sign.the_const_type thy
499 (* This function only makes sense if "T" is as general as possible. *)
500 fun robust_const_typargs thy (s, T) =
501 if s = app_op_name then
502 let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
503 else if String.isPrefix old_skolem_const_prefix s then
504 [] |> Term.add_tvarsT T |> rev |> map TVar
505 else if String.isPrefix lam_lifted_prefix s then
506 if String.isPrefix lam_lifted_poly_prefix s then
507 let val (T1, T2) = T |> dest_funT in [T1, T2] end
511 (s, T) |> Sign.const_typargs thy
513 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
514 Also accumulates sort infomation. *)
515 fun iterm_from_term thy format bs (P $ Q) =
517 val (P', P_atomics_Ts) = iterm_from_term thy format bs P
518 val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
519 in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
520 | iterm_from_term thy format _ (Const (c, T)) =
521 (IConst (`(make_fixed_const (SOME format)) c, T,
522 robust_const_typargs thy (c, T)),
524 | iterm_from_term _ _ _ (Free (s, T)) =
525 (IConst (`make_fixed_var s, T, []), atomic_types_of T)
526 | iterm_from_term _ format _ (Var (v as (s, _), T)) =
527 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
529 val Ts = T |> strip_type |> swap |> op ::
530 val s' = new_skolem_const_name s (length Ts)
531 in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
533 IVar ((make_schematic_var v, s), T), atomic_types_of T)
534 | iterm_from_term _ _ bs (Bound j) =
535 nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
536 | iterm_from_term thy format bs (Abs (s, T, t)) =
538 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
540 val name = `make_bound_var s
541 val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
542 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
545 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
547 datatype order = First_Order | Higher_Order
548 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
549 datatype strictness = Strict | Non_Strict
550 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
551 datatype type_level =
553 Noninf_Nonmono_Types of strictness * granularity |
554 Fin_Nonmono_Types of granularity |
559 Simple_Types of order * polymorphism * type_level |
560 Guards of polymorphism * type_level |
561 Tags of polymorphism * type_level
563 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
564 | is_type_enc_higher_order _ = false
566 fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
567 | polymorphism_of_type_enc (Guards (poly, _)) = poly
568 | polymorphism_of_type_enc (Tags (poly, _)) = poly
570 fun level_of_type_enc (Simple_Types (_, _, level)) = level
571 | level_of_type_enc (Guards (_, level)) = level
572 | level_of_type_enc (Tags (_, level)) = level
574 fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
575 | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
576 | granularity_of_type_level _ = All_Vars
578 fun is_type_level_quasi_sound All_Types = true
579 | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
580 | is_type_level_quasi_sound _ = false
581 val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
583 fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
584 | is_type_level_fairly_sound level = is_type_level_quasi_sound level
585 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
587 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
588 | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
589 | is_type_level_monotonicity_based _ = false
591 (* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
593 val queries = ["?", "_query"]
594 val bangs = ["!", "_bang"]
595 val ats = ["@", "_at"]
597 fun try_unsuffixes ss s =
598 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
600 fun try_nonmono constr suffixes fallback s =
601 case try_unsuffixes suffixes s of
603 (case try_unsuffixes suffixes s of
604 SOME s => (constr Positively_Naked_Vars, s)
606 case try_unsuffixes ats s of
607 SOME s => (constr Ghost_Type_Arg_Vars, s)
608 | NONE => (constr All_Vars, s))
611 fun type_enc_from_string strictness s =
612 (case try (unprefix "poly_") s of
613 SOME s => (SOME Polymorphic, s)
615 case try (unprefix "raw_mono_") s of
616 SOME s => (SOME Raw_Monomorphic, s)
618 case try (unprefix "mono_") s of
619 SOME s => (SOME Mangled_Monomorphic, s)
622 |> try_nonmono Fin_Nonmono_Types bangs
623 |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
624 |> (fn (poly, (level, core)) =>
625 case (core, (poly, level)) of
626 ("simple", (SOME poly, _)) =>
627 (case (poly, level) of
628 (Polymorphic, All_Types) =>
629 Simple_Types (First_Order, Polymorphic, All_Types)
630 | (Mangled_Monomorphic, _) =>
631 if granularity_of_type_level level = All_Vars then
632 Simple_Types (First_Order, Mangled_Monomorphic, level)
635 | _ => raise Same.SAME)
636 | ("simple_higher", (SOME poly, _)) =>
637 (case (poly, level) of
638 (Polymorphic, All_Types) =>
639 Simple_Types (Higher_Order, Polymorphic, All_Types)
640 | (_, Noninf_Nonmono_Types _) => raise Same.SAME
641 | (Mangled_Monomorphic, _) =>
642 if granularity_of_type_level level = All_Vars then
643 Simple_Types (Higher_Order, Mangled_Monomorphic, level)
646 | _ => raise Same.SAME)
647 | ("guards", (SOME poly, _)) =>
648 if poly = Mangled_Monomorphic andalso
649 granularity_of_type_level level = Ghost_Type_Arg_Vars then
653 | ("tags", (SOME poly, _)) =>
654 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
658 | ("args", (SOME poly, All_Types (* naja *))) =>
659 Guards (poly, Const_Arg_Types)
660 | ("erased", (NONE, All_Types (* naja *))) =>
661 Guards (Polymorphic, No_Types)
662 | _ => raise Same.SAME)
663 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
665 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
666 (Simple_Types (order, _, level)) =
667 Simple_Types (order, Mangled_Monomorphic, level)
668 | adjust_type_enc (THF _) type_enc = type_enc
669 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
670 Simple_Types (First_Order, Mangled_Monomorphic, level)
671 | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
672 Simple_Types (First_Order, Mangled_Monomorphic, level)
673 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
674 Simple_Types (First_Order, poly, level)
675 | adjust_type_enc format (Simple_Types (_, poly, level)) =
676 adjust_type_enc format (Guards (poly, level))
677 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
678 (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
679 | adjust_type_enc _ type_enc = type_enc
681 fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
682 | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
683 | constify_lifted (Free (x as (s, _))) =
684 (if String.isPrefix lam_lifted_prefix s then Const else Free) x
685 | constify_lifted t = t
687 (* Requires bound variables not to clash with any schematic variables (as should
688 be the case right after lambda-lifting). *)
689 fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
691 val names = Name.make_context (map fst (Term.add_var_names t []))
692 val (s, _) = Name.variant s names
693 in open_form (subst_bound (Var ((s, 0), T), t)) end
696 fun lift_lams_part_1 ctxt type_enc =
697 map close_form #> rpair ctxt
698 #-> Lambda_Lifting.lift_lambdas
699 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
700 lam_lifted_poly_prefix
702 lam_lifted_mono_prefix) ^ "_a"))
703 Lambda_Lifting.is_quantifier
705 val lift_lams_part_2 = pairself (map (open_form o constify_lifted))
706 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1
708 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
710 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
712 fun lam T t = Abs (Name.uu, T, t)
713 val (head, args) = strip_comb t ||> rev
714 val head_T = fastype_of head
716 val arg_Ts = head_T |> binder_types |> take n |> rev
717 val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
718 in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
719 | intentionalize_def t = t
721 type translated_formula =
725 iformula : (name, typ, iterm) formula,
726 atomic_types : typ list}
728 fun update_iformula f ({name, locality, kind, iformula, atomic_types}
729 : translated_formula) =
730 {name = name, locality = locality, kind = kind, iformula = f iformula,
731 atomic_types = atomic_types} : translated_formula
733 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
735 fun insert_type ctxt get_T x xs =
736 let val T = get_T x in
737 if exists (type_instance ctxt T o get_T) xs then xs
738 else x :: filter_out (type_generalization ctxt T o get_T) xs
741 (* The Booleans indicate whether all type arguments should be kept. *)
742 datatype type_arg_policy =
743 Explicit_Type_Args of bool (* infer_from_term_args *) |
747 fun type_arg_policy monom_constrs type_enc s =
748 let val poly = polymorphism_of_type_enc type_enc in
749 if s = type_tag_name then
750 if poly = Mangled_Monomorphic then Mangled_Type_Args
751 else Explicit_Type_Args false
752 else case type_enc of
753 Simple_Types (_, Polymorphic, _) => Explicit_Type_Args false
754 | Tags (_, All_Types) => No_Type_Args
756 let val level = level_of_type_enc type_enc in
757 if level = No_Types orelse s = @{const_name HOL.eq} orelse
758 (s = app_op_name andalso level = Const_Arg_Types) then
760 else if poly = Mangled_Monomorphic then
762 else if member (op =) monom_constrs s andalso
763 granularity_of_type_level level = Positively_Naked_Vars then
767 (level = All_Types orelse
768 granularity_of_type_level level = Ghost_Type_Arg_Vars)
772 (* Make atoms for sorted type variables. *)
773 fun generic_add_sorts_on_type (_, []) = I
774 | generic_add_sorts_on_type ((x, i), s :: ss) =
775 generic_add_sorts_on_type ((x, i), ss)
776 #> (if s = the_single @{sort HOL.type} then
779 insert (op =) (`make_type_class s, `make_fixed_type_var x)
781 insert (op =) (`make_type_class s,
782 (make_schematic_type_var (x, i), x)))
783 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
784 | add_sorts_on_tfree _ = I
785 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
786 | add_sorts_on_tvar _ = I
788 fun type_class_formula type_enc class arg =
789 AAtom (ATerm (class, arg ::
791 Simple_Types (First_Order, Polymorphic, _) =>
792 if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
795 fun formulas_for_types type_enc add_sorts_on_typ Ts =
796 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
797 |> map (fn (class, name) =>
798 type_class_formula type_enc class (ATerm (name, [])))
800 fun mk_aconns c phis =
801 let val (phis', phi') = split_last phis in
802 fold_rev (mk_aconn c) phis' phi'
804 fun mk_ahorn [] phi = phi
805 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
806 fun mk_aquant _ [] phi = phi
807 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
808 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
809 | mk_aquant q xs phi = AQuant (q, xs, phi)
811 fun close_universally add_term_vars phi =
813 fun add_formula_vars bounds (AQuant (_, xs, phi)) =
814 add_formula_vars (map fst xs @ bounds) phi
815 | add_formula_vars bounds (AConn (_, phis)) =
816 fold (add_formula_vars bounds) phis
817 | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
818 in mk_aquant AForall (add_formula_vars [] phi []) phi end
820 fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
821 (if is_tptp_variable s andalso
822 not (String.isPrefix tvar_prefix s) andalso
823 not (member (op =) bounds name) then
824 insert (op =) (name, NONE)
827 #> fold (add_term_vars bounds) tms
828 | add_term_vars bounds (AAbs ((name, _), tm)) =
829 add_term_vars (name :: bounds) tm
830 fun close_formula_universally phi = close_universally add_term_vars phi
832 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
833 fold (add_iterm_vars bounds) [tm1, tm2]
834 | add_iterm_vars _ (IConst _) = I
835 | add_iterm_vars bounds (IVar (name, T)) =
836 not (member (op =) bounds name) ? insert (op =) (name, SOME T)
837 | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
838 fun close_iformula_universally phi = close_universally add_iterm_vars phi
840 val fused_infinite_type_name = @{type_name ind} (* any infinite type *)
841 val fused_infinite_type = Type (fused_infinite_type_name, [])
843 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
845 fun ho_term_from_typ format type_enc =
847 fun term (Type (s, Ts)) =
848 ATerm (case (is_type_enc_higher_order type_enc, s) of
849 (true, @{type_name bool}) => `I tptp_bool_type
850 | (true, @{type_name fun}) => `I tptp_fun_type
851 | _ => if s = fused_infinite_type_name andalso
852 is_format_typed format then
853 `I tptp_individual_type
855 `make_fixed_type_const s,
857 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
858 | term (TVar (x, _)) = ATerm (tvar_name x, [])
861 fun ho_term_for_type_arg format type_enc T =
862 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
864 (* This shouldn't clash with anything else. *)
865 val mangled_type_sep = "\000"
867 fun generic_mangled_type_name f (ATerm (name, [])) = f name
868 | generic_mangled_type_name f (ATerm (name, tys)) =
869 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
871 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
873 fun mangled_type format type_enc =
874 generic_mangled_type_name fst o ho_term_from_typ format type_enc
876 fun make_simple_type s =
877 if s = tptp_bool_type orelse s = tptp_fun_type orelse
878 s = tptp_individual_type then
881 simple_type_prefix ^ ascii_of s
883 fun ho_type_from_ho_term type_enc pred_sym ary =
885 fun to_mangled_atype ty =
886 AType ((make_simple_type (generic_mangled_type_name fst ty),
887 generic_mangled_type_name snd ty), [])
888 fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
889 | to_poly_atype _ = raise Fail "unexpected type abstraction"
891 if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
892 else to_mangled_atype
893 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
894 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
895 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
896 | to_fo _ _ = raise Fail "unexpected type abstraction"
897 fun to_ho (ty as ATerm ((s, _), tys)) =
898 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
899 | to_ho _ = raise Fail "unexpected type abstraction"
900 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
902 fun ho_type_from_typ format type_enc pred_sym ary =
903 ho_type_from_ho_term type_enc pred_sym ary
904 o ho_term_from_typ format type_enc
906 fun mangled_const_name format type_enc T_args (s, s') =
908 val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
909 fun type_suffix f g =
910 fold_rev (curry (op ^) o g o prefix mangled_type_sep
911 o generic_mangled_type_name f) ty_args ""
912 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
914 val parse_mangled_ident =
915 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
917 fun parse_mangled_type x =
919 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
921 and parse_mangled_types x =
922 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
924 fun unmangled_type s =
925 s |> suffix ")" |> raw_explode
926 |> Scan.finite Symbol.stopper
927 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
928 quote s)) parse_mangled_type))
931 val unmangled_const_name = space_explode mangled_type_sep #> hd
932 fun unmangled_const s =
933 let val ss = space_explode mangled_type_sep s in
934 (hd ss, map unmangled_type (tl ss))
937 fun introduce_proxies_in_iterm type_enc =
939 fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
940 | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
942 (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
943 limitation. This works in conjuction with special code in
944 "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
947 IApp (IConst (`I ho_quant, T, []),
949 IApp (IConst (`I "P", p_T, []),
950 IConst (`I "X", x_T, [])))))
951 | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
952 fun intro top_level args (IApp (tm1, tm2)) =
953 IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
954 | intro top_level args (IConst (name as (s, _), T, T_args)) =
955 (case proxify_const s of
957 if top_level orelse is_type_enc_higher_order type_enc then
958 case (top_level, s) of
959 (_, "c_False") => IConst (`I tptp_false, T, [])
960 | (_, "c_True") => IConst (`I tptp_true, T, [])
961 | (false, "c_Not") => IConst (`I tptp_not, T, [])
962 | (false, "c_conj") => IConst (`I tptp_and, T, [])
963 | (false, "c_disj") => IConst (`I tptp_or, T, [])
964 | (false, "c_implies") => IConst (`I tptp_implies, T, [])
965 | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
966 | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
968 if is_tptp_equal s andalso length args = 2 then
969 IConst (`I tptp_equal, T, [])
971 (* Use a proxy even for partially applied THF0 equality,
972 because the LEO-II and Satallax parsers complain about not
973 being able to infer the type of "=". *)
974 IConst (proxy_base |>> prefix const_prefix, T, T_args)
975 | _ => IConst (name, T, [])
977 IConst (proxy_base |>> prefix const_prefix, T, T_args)
978 | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
979 else IConst (name, T, T_args))
980 | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
984 fun mangle_type_args_in_iterm format type_enc =
985 if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
987 fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
988 | mangle (tm as IConst (_, _, [])) = tm
989 | mangle (tm as IConst (name as (s, _), T, T_args)) =
990 (case unprefix_and_unascii const_prefix s of
993 case type_arg_policy [] type_enc (invert_const s'') of
995 IConst (mangled_const_name format type_enc T_args name, T, [])
997 | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
1003 fun chop_fun 0 T = ([], T)
1004 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1005 chop_fun (n - 1) ran_T |>> cons dom_T
1006 | chop_fun _ T = ([], T)
1008 fun filter_const_type_args _ _ _ [] = []
1009 | filter_const_type_args thy s ary T_args =
1011 val U = robust_const_type thy s
1012 val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
1013 val U_args = (s, U) |> robust_const_typargs thy
1016 |> map (fn (U, T) =>
1017 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
1019 handle TYPE _ => T_args
1021 fun filter_type_args_in_iterm thy monom_constrs type_enc =
1023 fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
1024 | filt _ (tm as IConst (_, _, [])) = tm
1025 | filt ary (IConst (name as (s, _), T, T_args)) =
1026 (case unprefix_and_unascii const_prefix s of
1029 if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
1035 val s'' = invert_const s''
1036 fun filter_T_args false = T_args
1037 | filter_T_args true = filter_const_type_args thy s'' ary T_args
1039 case type_arg_policy monom_constrs type_enc s'' of
1040 Explicit_Type_Args infer_from_term_args =>
1041 (name, filter_T_args infer_from_term_args)
1042 | No_Type_Args => (name, [])
1043 | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
1045 |> (fn (name, T_args) => IConst (name, T, T_args))
1046 | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
1050 fun iformula_from_prop ctxt format type_enc eq_as_iff =
1052 val thy = Proof_Context.theory_of ctxt
1053 fun do_term bs t atomic_Ts =
1054 iterm_from_term thy format bs (Envir.eta_contract t)
1055 |>> (introduce_proxies_in_iterm type_enc
1056 #> mangle_type_args_in_iterm format type_enc
1058 ||> union (op =) atomic_Ts
1059 fun do_quant bs q pos s T t' =
1061 val s = singleton (Name.variant_list (map fst bs)) s
1062 val universal = Option.map (q = AExists ? not) pos
1064 s |> `(case universal of
1065 SOME true => make_all_bound_var
1066 | SOME false => make_exist_bound_var
1067 | NONE => make_bound_var)
1069 do_formula ((s, (name, T)) :: bs) pos t'
1070 #>> mk_aquant q [(name, SOME T)]
1071 ##> union (op =) (atomic_types_of T)
1073 and do_conn bs c pos1 t1 pos2 t2 =
1074 do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
1075 and do_formula bs pos t =
1077 @{const Trueprop} $ t1 => do_formula bs pos t1
1078 | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
1079 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
1080 do_quant bs AForall pos s T t'
1081 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1082 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1083 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
1084 do_quant bs AExists pos s T t'
1085 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1086 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1087 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
1088 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
1089 | @{const HOL.implies} $ t1 $ t2 =>
1090 do_conn bs AImplies (Option.map not pos) t1 pos t2
1091 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
1092 if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
1094 in do_formula [] end
1096 fun presimplify_term ctxt t =
1097 t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
1098 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
1099 #> Meson.presimplify
1102 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
1103 fun conceal_bounds Ts t =
1104 subst_bounds (map (Free o apfst concealed_bound_name)
1105 (0 upto length Ts - 1 ~~ Ts), t)
1106 fun reveal_bounds Ts =
1107 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
1108 (0 upto length Ts - 1 ~~ Ts))
1110 fun is_fun_equality (@{const_name HOL.eq},
1111 Type (_, [Type (@{type_name fun}, _), _])) = true
1112 | is_fun_equality _ = false
1114 fun extensionalize_term ctxt t =
1115 if exists_Const is_fun_equality t then
1116 let val thy = Proof_Context.theory_of ctxt in
1117 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
1118 |> prop_of |> Logic.dest_equals |> snd
1123 fun simple_translate_lambdas do_lambdas ctxt t =
1124 let val thy = Proof_Context.theory_of ctxt in
1125 if Meson.is_fol_term thy t then
1131 @{const Not} $ t1 => @{const Not} $ trans Ts t1
1132 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
1133 t0 $ Abs (s, T, trans (T :: Ts) t')
1134 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1135 trans Ts (t0 $ eta_expand Ts t1 1)
1136 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
1137 t0 $ Abs (s, T, trans (T :: Ts) t')
1138 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1139 trans Ts (t0 $ eta_expand Ts t1 1)
1140 | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
1141 t0 $ trans Ts t1 $ trans Ts t2
1142 | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
1143 t0 $ trans Ts t1 $ trans Ts t2
1144 | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
1145 t0 $ trans Ts t1 $ trans Ts t2
1146 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1148 t0 $ trans Ts t1 $ trans Ts t2
1150 if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1151 else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1152 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1153 in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
1156 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
1157 do_cheaply_conceal_lambdas Ts t1
1158 $ do_cheaply_conceal_lambdas Ts t2
1159 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
1160 Const (lam_lifted_poly_prefix ^ serial_string (),
1161 T --> fastype_of1 (T :: Ts, t))
1162 | do_cheaply_conceal_lambdas _ t = t
1164 fun do_introduce_combinators ctxt Ts t =
1165 let val thy = Proof_Context.theory_of ctxt in
1166 t |> conceal_bounds Ts
1168 |> Meson_Clausify.introduce_combinators_in_cterm
1169 |> prop_of |> Logic.dest_equals |> snd
1172 (* A type variable of sort "{}" will make abstraction fail. *)
1173 handle THM _ => t |> do_cheaply_conceal_lambdas Ts
1174 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
1176 fun preprocess_abstractions_in_terms trans_lams facts =
1178 val (facts, lambda_ts) =
1179 facts |> map (snd o snd) |> trans_lams
1180 |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
1182 map2 (fn t => fn j =>
1183 ((lam_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
1184 lambda_ts (1 upto length lambda_ts)
1185 in (facts, lam_facts) end
1187 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
1188 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
1191 fun freeze (t $ u) = freeze t $ freeze u
1192 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
1193 | freeze (Var ((s, i), T)) =
1194 Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
1196 in t |> exists_subterm is_Var t ? freeze end
1198 fun presimp_prop ctxt role t =
1200 val thy = Proof_Context.theory_of ctxt
1201 val t = t |> Envir.beta_eta_contract
1202 |> transform_elim_prop
1203 |> Object_Logic.atomize_term thy
1204 val need_trueprop = (fastype_of t = @{typ bool})
1206 t |> need_trueprop ? HOLogic.mk_Trueprop
1207 |> extensionalize_term ctxt
1208 |> presimplify_term ctxt
1209 |> HOLogic.dest_Trueprop
1211 handle TERM _ => if role = Conjecture then @{term False} else @{term True})
1214 fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
1216 val (iformula, atomic_Ts) =
1217 iformula_from_prop ctxt format type_enc eq_as_iff
1218 (SOME (kind <> Conjecture)) t []
1219 |>> close_iformula_universally
1221 {name = name, locality = loc, kind = kind, iformula = iformula,
1222 atomic_types = atomic_Ts}
1225 fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
1226 case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
1228 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1229 if s = tptp_true then NONE else SOME formula
1230 | formula => SOME formula
1232 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
1233 | s_not_trueprop t =
1234 if fastype_of t = @{typ bool} then s_not t else @{prop False} (* too meta *)
1236 fun make_conjecture ctxt format type_enc =
1237 map (fn ((name, loc), (kind, t)) =>
1238 t |> kind = Conjecture ? s_not_trueprop
1239 |> make_formula ctxt format type_enc (format <> CNF) name loc kind)
1241 (** Finite and infinite type inference **)
1243 fun tvar_footprint thy s ary =
1244 (case unprefix_and_unascii const_prefix s of
1246 s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
1247 |> map (fn T => Term.add_tvarsT T [] |> map fst)
1251 fun ghost_type_args thy s ary =
1252 if is_tptp_equal s then
1256 val footprint = tvar_footprint thy s ary
1257 val eq = (s = @{const_name HOL.eq})
1258 fun ghosts _ [] = []
1259 | ghosts seen ((i, tvars) :: args) =
1260 ghosts (union (op =) seen tvars) args
1261 |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
1264 if forall null footprint then
1267 0 upto length footprint - 1 ~~ footprint
1268 |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
1272 type monotonicity_info =
1273 {maybe_finite_Ts : typ list,
1274 surely_finite_Ts : typ list,
1275 maybe_infinite_Ts : typ list,
1276 surely_infinite_Ts : typ list,
1277 maybe_nonmono_Ts : typ list}
1279 (* These types witness that the type classes they belong to allow infinite
1280 models and hence that any types with these type classes is monotonic. *)
1281 val known_infinite_types =
1282 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
1284 fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
1285 strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
1287 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1288 dangerous because their "exhaust" properties can easily lead to unsound ATP
1289 proofs. On the other hand, all HOL infinite types can be given the same
1290 models in first-order logic (via Löwenheim-Skolem). *)
1292 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
1293 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
1294 maybe_nonmono_Ts, ...}
1295 (Noninf_Nonmono_Types (strictness, grain)) T =
1296 grain = Ghost_Type_Arg_Vars orelse
1297 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1298 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
1299 (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
1300 is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
1302 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
1303 maybe_nonmono_Ts, ...}
1304 (Fin_Nonmono_Types grain) T =
1305 grain = Ghost_Type_Arg_Vars orelse
1306 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1307 (exists (type_generalization ctxt T) surely_finite_Ts orelse
1308 (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
1309 is_type_surely_finite ctxt T)))
1310 | should_encode_type _ _ _ _ = false
1312 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
1313 should_guard_var () andalso should_encode_type ctxt mono level T
1314 | should_guard_type _ _ _ _ _ = false
1316 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
1317 String.isPrefix bound_var_prefix s orelse
1318 String.isPrefix all_bound_var_prefix s
1319 | is_maybe_universal_var (IVar _) = true
1320 | is_maybe_universal_var _ = false
1323 Top_Level of bool option |
1324 Eq_Arg of bool option |
1327 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1328 | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
1329 if granularity_of_type_level level = All_Vars then
1330 should_encode_type ctxt mono level T
1332 (case (site, is_maybe_universal_var u) of
1333 (Eq_Arg _, true) => should_encode_type ctxt mono level T
1335 | should_tag_with_type _ _ _ _ _ _ = false
1337 fun fused_type ctxt mono level =
1339 val should_encode = should_encode_type ctxt mono level
1340 fun fuse 0 T = if should_encode T then T else fused_infinite_type
1341 | fuse ary (Type (@{type_name fun}, [T1, T2])) =
1342 fuse 0 T1 --> fuse (ary - 1) T2
1343 | fuse _ _ = raise Fail "expected function type"
1346 (** predicators and application operators **)
1349 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
1352 fun default_sym_tab_entries type_enc =
1353 (make_fixed_const NONE @{const_name undefined},
1354 {pred_sym = false, min_ary = 0, max_ary = 0, types = [],
1355 in_conj = false}) ::
1356 ([tptp_false, tptp_true]
1357 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [],
1358 in_conj = false})) @
1359 ([tptp_equal, tptp_old_equal]
1360 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [],
1362 |> not (is_type_enc_higher_order type_enc)
1363 ? cons (prefixed_predicator_name,
1364 {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
1367 fun sym_table_for_facts ctxt type_enc explicit_apply conjs facts =
1369 fun consider_var_ary const_T var_T max_ary =
1372 if ary = max_ary orelse type_instance ctxt var_T T orelse
1373 type_instance ctxt T var_T then
1376 iter (ary + 1) (range_type T)
1377 in iter 0 const_T end
1378 fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1379 if explicit_apply = NONE andalso
1380 (can dest_funT T orelse T = @{typ bool}) then
1382 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1383 fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
1384 {pred_sym = pred_sym andalso not bool_vars',
1385 min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
1386 max_ary = max_ary, types = types, in_conj = in_conj}
1388 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1390 if bool_vars' = bool_vars andalso
1391 pointer_eq (fun_var_Ts', fun_var_Ts) then
1394 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
1398 fun add_fact_syms conj_fact =
1400 fun add_iterm_syms top_level tm
1401 (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1402 let val (head, args) = strip_iterm_comb tm in
1404 IConst ((s, _), T, _) =>
1405 if String.isPrefix bound_var_prefix s orelse
1406 String.isPrefix all_bound_var_prefix s then
1407 add_universal_var T accum
1408 else if String.isPrefix exist_bound_var_prefix s then
1411 let val ary = length args in
1412 ((bool_vars, fun_var_Ts),
1413 case Symtab.lookup sym_tab s of
1414 SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
1417 pred_sym andalso top_level andalso not bool_vars
1418 val types' = types |> insert_type ctxt I T
1419 val in_conj = in_conj orelse conj_fact
1421 if is_some explicit_apply orelse
1422 pointer_eq (types', types) then
1425 fold (consider_var_ary T) fun_var_Ts min_ary
1427 Symtab.update (s, {pred_sym = pred_sym,
1428 min_ary = Int.min (ary, min_ary),
1429 max_ary = Int.max (ary, max_ary),
1430 types = types', in_conj = in_conj})
1435 val pred_sym = top_level andalso not bool_vars
1437 case explicit_apply of
1440 | NONE => fold (consider_var_ary T) fun_var_Ts ary
1442 Symtab.update_new (s,
1443 {pred_sym = pred_sym, min_ary = min_ary,
1444 max_ary = ary, types = [T], in_conj = conj_fact})
1448 | IVar (_, T) => add_universal_var T accum
1449 | IAbs ((_, T), tm) =>
1450 accum |> add_universal_var T |> add_iterm_syms false tm
1452 |> fold (add_iterm_syms false) args
1454 in K (add_iterm_syms true) |> formula_fold NONE |> fact_lift end
1456 ((false, []), Symtab.empty)
1457 |> fold (add_fact_syms true) conjs
1458 |> fold (add_fact_syms false) facts
1460 |> fold Symtab.update (default_sym_tab_entries type_enc)
1463 fun min_ary_of sym_tab s =
1464 case Symtab.lookup sym_tab s of
1465 SOME ({min_ary, ...} : sym_info) => min_ary
1467 case unprefix_and_unascii const_prefix s of
1469 let val s = s |> unmangled_const_name |> invert_const in
1470 if s = predicator_name then 1
1471 else if s = app_op_name then 2
1472 else if s = type_guard_name then 1
1477 (* True if the constant ever appears outside of the top-level position in
1478 literals, or if it appears with different arities (e.g., because of different
1479 type instantiations). If false, the constant always receives all of its
1480 arguments and is used as a predicate. *)
1481 fun is_pred_sym sym_tab s =
1482 case Symtab.lookup sym_tab s of
1483 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1484 pred_sym andalso min_ary = max_ary
1487 val app_op = `(make_fixed_const NONE) app_op_name
1488 val predicator_combconst =
1489 IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
1491 fun list_app head args = fold (curry (IApp o swap)) args head
1492 fun predicator tm = IApp (predicator_combconst, tm)
1494 fun firstorderize_fact thy monom_constrs format type_enc sym_tab =
1496 fun do_app arg head =
1498 val head_T = ityp_of head
1499 val (arg_T, res_T) = dest_funT head_T
1501 IConst (app_op, head_T --> head_T, [arg_T, res_T])
1502 |> mangle_type_args_in_iterm format type_enc
1503 in list_app app [head, arg] end
1504 fun list_app_ops head args = fold do_app args head
1505 fun introduce_app_ops tm =
1506 case strip_iterm_comb tm of
1507 (head as IConst ((s, _), _, _), args) =>
1508 args |> map introduce_app_ops
1509 |> chop (min_ary_of sym_tab s)
1512 | (head, args) => list_app_ops head (map introduce_app_ops args)
1513 fun introduce_predicators tm =
1514 case strip_iterm_comb tm of
1515 (IConst ((s, _), _, _), _) =>
1516 if is_pred_sym sym_tab s then tm else predicator tm
1517 | _ => predicator tm
1519 not (is_type_enc_higher_order type_enc)
1520 ? (introduce_app_ops #> introduce_predicators)
1521 #> filter_type_args_in_iterm thy monom_constrs type_enc
1522 in update_iformula (formula_map do_iterm) end
1524 (** Helper facts **)
1526 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
1527 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
1529 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1531 [(("COMBI", false), @{thms Meson.COMBI_def}),
1532 (("COMBK", false), @{thms Meson.COMBK_def}),
1533 (("COMBB", false), @{thms Meson.COMBB_def}),
1534 (("COMBC", false), @{thms Meson.COMBC_def}),
1535 (("COMBS", false), @{thms Meson.COMBS_def}),
1536 ((predicator_name, false), [not_ffalse, ftrue]),
1537 (("fFalse", false), [not_ffalse]),
1538 (("fFalse", true), @{thms True_or_False}),
1539 (("fTrue", false), [ftrue]),
1540 (("fTrue", true), @{thms True_or_False}),
1542 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1543 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1545 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1546 by (unfold fconj_def) fast+}),
1548 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1549 by (unfold fdisj_def) fast+}),
1550 (("fimplies", false),
1551 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1552 by (unfold fimplies_def) fast+}),
1554 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1555 However, this is done so for backward compatibility: Including the
1556 equality helpers by default in Metis breaks a few existing proofs. *)
1557 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1558 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1559 (* Partial characterization of "fAll" and "fEx". A complete characterization
1560 would require the axiom of choice for replay with Metis. *)
1561 (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
1562 (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
1563 (("If", true), @{thms if_True if_False True_or_False})]
1564 |> map (apsnd (map zero_var_indexes))
1566 fun atype_of_type_vars (Simple_Types (_, Polymorphic, _)) = SOME atype_of_types
1567 | atype_of_type_vars _ = NONE
1569 fun bound_tvars type_enc sorts Ts =
1570 (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
1571 #> mk_aquant AForall
1572 (map_filter (fn TVar (x as (s, _), _) =>
1573 SOME ((make_schematic_type_var x, s),
1574 atype_of_type_vars type_enc)
1577 fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
1578 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1579 else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
1580 |> close_formula_universally
1581 |> bound_tvars type_enc true atomic_Ts
1583 val type_tag = `(make_fixed_const NONE) type_tag_name
1585 fun type_tag_idempotence_fact format type_enc =
1587 fun var s = ATerm (`I s, [])
1588 fun tag tm = ATerm (type_tag, [var "A", tm])
1589 val tagged_var = tag (var "X")
1591 Formula (type_tag_idempotence_helper_name, Axiom,
1592 eq_formula type_enc [] false (tag tagged_var) tagged_var,
1593 isabelle_info format simpN, NONE)
1596 fun should_specialize_helper type_enc t =
1597 polymorphism_of_type_enc type_enc <> Polymorphic andalso
1598 level_of_type_enc type_enc <> No_Types andalso
1599 not (null (Term.hidden_polymorphism t))
1601 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1602 case unprefix_and_unascii const_prefix s of
1605 val thy = Proof_Context.theory_of ctxt
1606 val unmangled_s = mangled_s |> unmangled_const_name
1607 fun dub needs_fairly_sound j k =
1608 (unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1609 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1610 (if needs_fairly_sound then typed_helper_suffix
1611 else untyped_helper_suffix),
1613 fun dub_and_inst needs_fairly_sound (th, j) =
1614 let val t = prop_of th in
1615 if should_specialize_helper type_enc t then
1616 map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
1621 |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
1622 val make_facts = map_filter (make_fact ctxt format type_enc false)
1623 val fairly_sound = is_type_enc_fairly_sound type_enc
1626 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1627 if helper_s <> unmangled_s orelse
1628 (needs_fairly_sound andalso not fairly_sound) then
1631 ths ~~ (1 upto length ths)
1632 |> maps (dub_and_inst needs_fairly_sound)
1636 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1637 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1640 (***************************************************************)
1641 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1642 (***************************************************************)
1644 fun set_insert (x, s) = Symtab.update (x, ()) s
1646 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1648 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1649 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1651 fun classes_of_terms get_Ts =
1652 map (map snd o get_Ts)
1653 #> List.foldl add_classes Symtab.empty
1654 #> delete_type #> Symtab.keys
1656 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
1657 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
1659 fun fold_type_constrs f (Type (s, Ts)) x =
1660 fold (fold_type_constrs f) Ts (f (s, x))
1661 | fold_type_constrs _ _ x = x
1663 (* Type constructors used to instantiate overloaded constants are the only ones
1665 fun add_type_constrs_in_term thy =
1667 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1668 | add (t $ u) = add t #> add u
1670 x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
1671 | add (Abs (_, _, u)) = add u
1675 fun type_constrs_of_terms thy ts =
1676 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1678 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
1679 let val (head, args) = strip_comb t in
1680 (head |> dest_Const |> fst,
1681 fold_rev (fn t as Var ((s, _), T) =>
1682 (fn u => Abs (s, T, abstract_over (t, u)))
1683 | _ => raise Fail "expected Var") args u)
1685 | extract_lambda_def _ = raise Fail "malformed lifted lambda"
1687 fun trans_lams_from_string ctxt type_enc lam_trans =
1688 if lam_trans = no_lamsN then
1690 else if lam_trans = hide_lamsN then
1691 lift_lams ctxt type_enc ##> K []
1692 else if lam_trans = lam_liftingN then
1693 lift_lams ctxt type_enc
1694 else if lam_trans = combinatorsN then
1695 map (introduce_combinators ctxt) #> rpair []
1696 else if lam_trans = hybrid_lamsN then
1697 lift_lams_part_1 ctxt type_enc
1698 ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
1700 else if lam_trans = keep_lamsN then
1701 map (Envir.eta_contract) #> rpair []
1703 error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
1705 fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
1708 val thy = Proof_Context.theory_of ctxt
1709 val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
1710 val fact_ts = facts |> map snd
1711 (* Remove existing facts from the conjecture, as this can dramatically
1712 boost an ATP's performance (for some reason). *)
1715 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1716 val facts = facts |> map (apsnd (pair Axiom))
1718 map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
1719 |> map (apsnd freeze_term)
1720 |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
1721 val ((conjs, facts), lam_facts) =
1723 |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
1724 |> (if lam_trans = no_lamsN then
1728 #> preprocess_abstractions_in_terms trans_lams
1729 #>> chop (length conjs))
1730 val conjs = conjs |> make_conjecture ctxt format type_enc
1731 val (fact_names, facts) =
1733 |> map_filter (fn (name, (_, t)) =>
1734 make_fact ctxt format type_enc true (name, t)
1735 |> Option.map (pair name))
1737 val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
1739 lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
1740 val all_ts = concl_t :: hyp_ts @ fact_ts
1741 val subs = tfree_classes_of_terms all_ts
1742 val supers = tvar_classes_of_terms all_ts
1743 val tycons = type_constrs_of_terms thy all_ts
1744 val (supers, arity_clauses) =
1745 if level_of_type_enc type_enc = No_Types then ([], [])
1746 else make_arity_clauses thy tycons supers
1747 val class_rel_clauses = make_class_rel_clauses thy subs supers
1749 (fact_names |> map single, union (op =) subs supers, conjs,
1750 facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
1753 val type_guard = `(make_fixed_const NONE) type_guard_name
1755 fun type_guard_iterm format type_enc T tm =
1756 IApp (IConst (type_guard, T --> @{typ bool}, [T])
1757 |> mangle_type_args_in_iterm format type_enc, tm)
1759 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1760 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1761 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1762 | is_var_positively_naked_in_term _ _ _ _ = true
1764 fun is_var_ghost_type_arg_in_term thy polym_constrs name pos tm accum =
1765 is_var_positively_naked_in_term name pos tm accum orelse
1767 val var = ATerm (name, [])
1768 fun is_nasty_in_term (ATerm (_, [])) = false
1769 | is_nasty_in_term (ATerm ((s, _), tms)) =
1771 val ary = length tms
1772 val polym_constr = member (op =) polym_constrs s
1773 val ghosts = ghost_type_args thy s ary
1775 exists (fn (j, tm) =>
1776 if polym_constr then
1777 member (op =) ghosts j andalso
1778 (tm = var orelse is_nasty_in_term tm)
1780 tm = var andalso member (op =) ghosts j)
1781 (0 upto ary - 1 ~~ tms)
1782 orelse (not polym_constr andalso exists is_nasty_in_term tms)
1784 | is_nasty_in_term _ = true
1785 in is_nasty_in_term tm end
1787 fun should_guard_var_in_formula thy polym_constrs level pos phi (SOME true)
1789 (case granularity_of_type_level level of
1791 | Positively_Naked_Vars =>
1792 formula_fold pos (is_var_positively_naked_in_term name) phi false
1793 | Ghost_Type_Arg_Vars =>
1794 formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name)
1796 | should_guard_var_in_formula _ _ _ _ _ _ _ = true
1798 fun always_guard_var_in_formula _ _ _ _ _ _ _ = true
1800 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
1801 | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
1802 granularity_of_type_level level <> All_Vars andalso
1803 should_encode_type ctxt mono level T
1804 | should_generate_tag_bound_decl _ _ _ _ _ = false
1806 fun mk_aterm format type_enc name T_args args =
1807 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1809 fun tag_with_type ctxt format mono type_enc pos T tm =
1810 IConst (type_tag, T --> T, [T])
1811 |> mangle_type_args_in_iterm format type_enc
1812 |> ho_term_from_iterm ctxt format mono type_enc pos
1813 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1814 | _ => raise Fail "unexpected lambda-abstraction")
1815 and ho_term_from_iterm ctxt format mono type_enc =
1819 val (head, args) = strip_iterm_comb u
1822 Top_Level pos => pos
1827 IConst (name as (s, _), _, T_args) =>
1829 val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1831 map (term arg_site) args |> mk_aterm format type_enc name T_args
1834 map (term Elsewhere) args |> mk_aterm format type_enc name []
1835 | IAbs ((name, T), tm) =>
1836 AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1838 | IApp _ => raise Fail "impossible \"IApp\""
1841 if should_tag_with_type ctxt mono type_enc site u T then
1842 tag_with_type ctxt format mono type_enc pos T t
1846 in term o Top_Level end
1847 and formula_from_iformula ctxt polym_constrs format mono type_enc
1850 val thy = Proof_Context.theory_of ctxt
1851 val level = level_of_type_enc type_enc
1852 val do_term = ho_term_from_iterm ctxt format mono type_enc
1855 Simple_Types _ => fused_type ctxt mono level 0
1856 #> ho_type_from_typ format type_enc false 0 #> SOME
1858 fun do_out_of_bound_type pos phi universal (name, T) =
1859 if should_guard_type ctxt mono type_enc
1860 (fn () => should_guard_var thy polym_constrs level pos phi
1861 universal name) T then
1863 |> type_guard_iterm format type_enc T
1864 |> do_term pos |> AAtom |> SOME
1865 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
1867 val var = ATerm (name, [])
1868 val tagged_var = tag_with_type ctxt format mono type_enc pos T var
1869 in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
1872 fun do_formula pos (AQuant (q, xs, phi)) =
1874 val phi = phi |> do_formula pos
1875 val universal = Option.map (q = AExists ? not) pos
1877 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1878 | SOME T => do_bound_type T)),
1879 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1881 (fn (_, NONE) => NONE
1883 do_out_of_bound_type pos phi universal (s, T))
1887 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1888 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1891 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1892 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1893 the remote provers might care. *)
1894 fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
1895 mono type_enc (j, {name, locality, kind, iformula, atomic_types}) =
1896 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
1898 |> formula_from_iformula ctxt polym_constrs format mono type_enc
1899 should_guard_var_in_formula (if pos then SOME true else NONE)
1900 |> close_formula_universally
1901 |> bound_tvars type_enc true atomic_types,
1904 Intro => isabelle_info format introN
1905 | Elim => isabelle_info format elimN
1906 | Simp => isabelle_info format simpN
1910 fun formula_line_for_class_rel_clause format type_enc
1911 ({name, subclass, superclass, ...} : class_rel_clause) =
1912 let val ty_arg = ATerm (tvar_a_name, []) in
1913 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1915 [type_class_formula type_enc subclass ty_arg,
1916 type_class_formula type_enc superclass ty_arg])
1917 |> mk_aquant AForall
1918 [(tvar_a_name, atype_of_type_vars type_enc)],
1919 isabelle_info format introN, NONE)
1922 fun formula_from_arity_atom type_enc (class, t, args) =
1923 ATerm (t, map (fn arg => ATerm (arg, [])) args)
1924 |> type_class_formula type_enc class
1926 fun formula_line_for_arity_clause format type_enc
1927 ({name, prem_atoms, concl_atom} : arity_clause) =
1928 Formula (arity_clause_prefix ^ name, Axiom,
1929 mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
1930 (formula_from_arity_atom type_enc concl_atom)
1931 |> mk_aquant AForall
1932 (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
1933 isabelle_info format introN, NONE)
1935 fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
1936 ({name, kind, iformula, atomic_types, ...} : translated_formula) =
1937 Formula (conjecture_prefix ^ name, kind,
1939 |> formula_from_iformula ctxt polym_constrs format mono type_enc
1940 should_guard_var_in_formula (SOME false)
1941 |> close_formula_universally
1942 |> bound_tvars type_enc true atomic_types, NONE, NONE)
1944 fun formula_line_for_free_type j phi =
1945 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
1946 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
1949 fold (union (op =)) (map #atomic_types facts) []
1950 |> formulas_for_types type_enc add_sorts_on_tfree
1951 in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
1953 (** Symbol declarations **)
1955 fun decl_line_for_class order s =
1956 let val name as (s, _) = `make_type_class s in
1957 Decl (sym_decl_prefix ^ s, name,
1958 if order = First_Order then
1959 ATyAbs ([tvar_a_name],
1960 if avoid_first_order_ghost_type_vars then
1961 AFun (a_itself_atype, bool_atype)
1965 AFun (atype_of_types, bool_atype))
1968 fun decl_lines_for_classes type_enc classes =
1970 Simple_Types (order, Polymorphic, _) =>
1971 map (decl_line_for_class order) classes
1974 fun sym_decl_table_for_facts ctxt format type_enc sym_tab (conjs, facts) =
1976 fun add_iterm_syms tm =
1977 let val (head, args) = strip_iterm_comb tm in
1979 IConst ((s, s'), T, T_args) =>
1981 val (pred_sym, in_conj) =
1982 case Symtab.lookup sym_tab s of
1983 SOME ({pred_sym, in_conj, ...} : sym_info) =>
1985 | NONE => (false, false)
1988 Guards _ => not pred_sym
1989 | _ => true) andalso
1990 is_tptp_user_symbol s
1993 Symtab.map_default (s, [])
1994 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
1999 | IAbs (_, tm) => add_iterm_syms tm
2001 #> fold add_iterm_syms args
2003 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
2004 fun add_formula_var_types (AQuant (_, xs, phi)) =
2005 fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
2006 #> add_formula_var_types phi
2007 | add_formula_var_types (AConn (_, phis)) =
2008 fold add_formula_var_types phis
2009 | add_formula_var_types _ = I
2011 if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
2012 else fold (fact_lift add_formula_var_types) (conjs @ facts) []
2013 fun add_undefined_const T =
2016 `(make_fixed_const NONE) @{const_name undefined}
2017 |> (case type_arg_policy [] type_enc @{const_name undefined} of
2018 Mangled_Type_Args => mangled_const_name format type_enc [T]
2021 Symtab.map_default (s, [])
2022 (insert_type ctxt #3 (s', [T], T, false, 0, false))
2024 fun add_TYPE_const () =
2025 let val (s, s') = TYPE_name in
2026 Symtab.map_default (s, [])
2027 (insert_type ctxt #3
2028 (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
2032 |> is_type_enc_fairly_sound type_enc
2033 ? (fold (fold add_fact_syms) [conjs, facts]
2034 #> (case type_enc of
2035 Simple_Types (First_Order, Polymorphic, _) =>
2036 if avoid_first_order_ghost_type_vars then add_TYPE_const ()
2038 | Simple_Types _ => I
2039 | _ => fold add_undefined_const (var_types ())))
2042 (* We add "bool" in case the helper "True_or_False" is included later. *)
2043 fun default_mono level =
2044 {maybe_finite_Ts = [@{typ bool}],
2045 surely_finite_Ts = [@{typ bool}],
2046 maybe_infinite_Ts = known_infinite_types,
2047 surely_infinite_Ts =
2049 Noninf_Nonmono_Types (Strict, _) => []
2050 | _ => known_infinite_types,
2051 maybe_nonmono_Ts = [@{typ bool}]}
2053 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
2054 out with monotonicity" paper presented at CADE 2011. *)
2055 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
2056 | add_iterm_mononotonicity_info ctxt level _
2057 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
2058 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
2059 surely_infinite_Ts, maybe_nonmono_Ts}) =
2060 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
2062 Noninf_Nonmono_Types (strictness, _) =>
2063 if exists (type_instance ctxt T) surely_infinite_Ts orelse
2064 member (type_equiv ctxt) maybe_finite_Ts T then
2066 else if is_type_kind_of_surely_infinite ctxt strictness
2067 surely_infinite_Ts T then
2068 {maybe_finite_Ts = maybe_finite_Ts,
2069 surely_finite_Ts = surely_finite_Ts,
2070 maybe_infinite_Ts = maybe_infinite_Ts,
2071 surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
2072 maybe_nonmono_Ts = maybe_nonmono_Ts}
2074 {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
2075 surely_finite_Ts = surely_finite_Ts,
2076 maybe_infinite_Ts = maybe_infinite_Ts,
2077 surely_infinite_Ts = surely_infinite_Ts,
2078 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2079 | Fin_Nonmono_Types _ =>
2080 if exists (type_instance ctxt T) surely_finite_Ts orelse
2081 member (type_equiv ctxt) maybe_infinite_Ts T then
2083 else if is_type_surely_finite ctxt T then
2084 {maybe_finite_Ts = maybe_finite_Ts,
2085 surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
2086 maybe_infinite_Ts = maybe_infinite_Ts,
2087 surely_infinite_Ts = surely_infinite_Ts,
2088 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2090 {maybe_finite_Ts = maybe_finite_Ts,
2091 surely_finite_Ts = surely_finite_Ts,
2092 maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
2093 surely_infinite_Ts = surely_infinite_Ts,
2094 maybe_nonmono_Ts = maybe_nonmono_Ts}
2098 | add_iterm_mononotonicity_info _ _ _ _ mono = mono
2099 fun add_fact_mononotonicity_info ctxt level
2100 ({kind, iformula, ...} : translated_formula) =
2101 formula_fold (SOME (kind <> Conjecture))
2102 (add_iterm_mononotonicity_info ctxt level) iformula
2103 fun mononotonicity_info_for_facts ctxt type_enc facts =
2104 let val level = level_of_type_enc type_enc in
2106 |> is_type_level_monotonicity_based level
2107 ? fold (add_fact_mononotonicity_info ctxt level) facts
2110 fun add_iformula_monotonic_types ctxt mono type_enc =
2112 val level = level_of_type_enc type_enc
2113 val should_encode = should_encode_type ctxt mono level
2114 fun add_type T = not (should_encode T) ? insert_type ctxt I T
2115 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
2117 and add_term tm = add_type (ityp_of tm) #> add_args tm
2118 in formula_fold NONE (K add_term) end
2119 fun add_fact_monotonic_types ctxt mono type_enc =
2120 add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
2121 fun monotonic_types_for_facts ctxt mono type_enc facts =
2122 let val level = level_of_type_enc type_enc in
2123 [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
2124 is_type_level_monotonicity_based level andalso
2125 granularity_of_type_level level <> Ghost_Type_Arg_Vars)
2126 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
2129 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
2130 Formula (guards_sym_formula_prefix ^
2131 ascii_of (mangled_type format type_enc T),
2133 IConst (`make_bound_var "X", T, [])
2134 |> type_guard_iterm format type_enc T
2136 |> formula_from_iformula ctxt [] format mono type_enc
2137 always_guard_var_in_formula (SOME true)
2138 |> close_formula_universally
2139 |> bound_tvars type_enc true (atomic_types_of T),
2140 isabelle_info format introN, NONE)
2142 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
2143 let val x_var = ATerm (`make_bound_var "X", []) in
2144 Formula (tags_sym_formula_prefix ^
2145 ascii_of (mangled_type format type_enc T),
2147 eq_formula type_enc (atomic_types_of T) false
2148 (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
2149 isabelle_info format simpN, NONE)
2152 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
2154 Simple_Types _ => []
2156 map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
2157 | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
2159 fun decl_line_for_sym ctxt format mono type_enc s
2160 (s', T_args, T, pred_sym, ary, _) =
2162 val thy = Proof_Context.theory_of ctxt
2166 else case unprefix_and_unascii const_prefix s of
2169 val s' = s' |> invert_const
2170 val T = s' |> robust_const_type thy
2171 in (T, robust_const_typargs thy (s', T)) end
2172 | NONE => raise Fail "unexpected type arguments"
2174 Decl (sym_decl_prefix ^ s, (s, s'),
2175 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
2176 |> ho_type_from_typ format type_enc pred_sym ary
2177 |> not (null T_args)
2178 ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
2181 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
2182 j (s', T_args, T, _, ary, in_conj) =
2184 val thy = Proof_Context.theory_of ctxt
2185 val (kind, maybe_negate) =
2186 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
2188 val (arg_Ts, res_T) = chop_fun ary T
2189 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2191 bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
2193 if exists (curry (op =) dummyT) T_args then
2194 case level_of_type_enc type_enc of
2195 All_Types => map SOME arg_Ts
2197 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
2198 let val ghosts = ghost_type_args thy s ary in
2199 map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
2200 (0 upto ary - 1) arg_Ts
2207 Formula (guards_sym_formula_prefix ^ s ^
2208 (if n > 1 then "_" ^ string_of_int j else ""), kind,
2209 IConst ((s, s'), T, T_args)
2210 |> fold (curry (IApp o swap)) bounds
2211 |> type_guard_iterm format type_enc res_T
2212 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
2213 |> formula_from_iformula ctxt [] format mono type_enc
2214 always_guard_var_in_formula (SOME true)
2215 |> close_formula_universally
2216 |> bound_tvars type_enc (n > 1) (atomic_types_of T)
2218 isabelle_info format introN, NONE)
2221 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
2222 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
2224 val thy = Proof_Context.theory_of ctxt
2225 val level = level_of_type_enc type_enc
2226 val grain = granularity_of_type_level level
2228 tags_sym_formula_prefix ^ s ^
2229 (if n > 1 then "_" ^ string_of_int j else "")
2230 val (kind, maybe_negate) =
2231 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
2233 val (arg_Ts, res_T) = chop_fun ary T
2234 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2235 val bounds = bound_names |> map (fn name => ATerm (name, []))
2236 val cst = mk_aterm format type_enc (s, s') T_args
2237 val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) pred_sym
2238 val should_encode = should_encode_type ctxt mono level
2239 val tag_with = tag_with_type ctxt format mono type_enc NONE
2240 val add_formula_for_res =
2241 if should_encode res_T then
2244 if grain = Ghost_Type_Arg_Vars then
2245 let val ghosts = ghost_type_args thy s ary in
2246 map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
2247 (0 upto ary - 1 ~~ arg_Ts) bounds
2252 cons (Formula (ident_base ^ "_res", kind,
2253 eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
2254 isabelle_info format simpN, NONE))
2258 fun add_formula_for_arg k =
2259 let val arg_T = nth arg_Ts k in
2260 if should_encode arg_T then
2261 case chop k bounds of
2262 (bounds1, bound :: bounds2) =>
2263 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
2264 eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
2266 isabelle_info format simpN, NONE))
2267 | _ => raise Fail "expected nonempty tail"
2272 [] |> not pred_sym ? add_formula_for_res
2273 |> (Config.get ctxt type_tag_arguments andalso
2274 grain = Positively_Naked_Vars)
2275 ? fold add_formula_for_arg (ary - 1 downto 0)
2278 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
2280 fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
2282 val T = result_type_of_decl decl
2283 |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
2285 if forall (type_generalization ctxt T o result_type_of_decl) decls' then
2290 | rationalize_decls _ decls = decls
2292 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
2295 Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
2296 | Guards (_, level) =>
2298 val decls = decls |> rationalize_decls ctxt
2299 val n = length decls
2301 decls |> filter (should_encode_type ctxt mono level
2302 o result_type_of_decl)
2304 (0 upto length decls - 1, decls)
2305 |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
2308 | Tags (_, level) =>
2309 if granularity_of_type_level level = All_Vars then
2312 let val n = length decls in
2313 (0 upto n - 1 ~~ decls)
2314 |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono
2318 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
2319 mono_Ts sym_decl_tab =
2321 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
2323 problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
2325 fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
2328 in mono_lines @ decl_lines end
2330 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
2331 Config.get ctxt type_tag_idempotence andalso
2332 is_type_level_monotonicity_based level andalso
2333 poly <> Mangled_Monomorphic
2334 | needs_type_tag_idempotence _ _ = false
2336 val implicit_declsN = "Should-be-implicit typings"
2337 val explicit_declsN = "Explicit typings"
2338 val factsN = "Relevant facts"
2339 val class_relsN = "Class relationships"
2340 val aritiesN = "Arities"
2341 val helpersN = "Helper facts"
2342 val conjsN = "Conjectures"
2343 val free_typesN = "Type variables"
2345 (* TFF allows implicit declarations of types, function symbols, and predicate
2346 symbols (with "$i" as the type of individuals), but some provers (e.g.,
2347 SNARK) require explicit declarations. The situation is similar for THF. *)
2349 fun default_type type_enc pred_sym s =
2354 if String.isPrefix type_const_prefix s then atype_of_types
2355 else individual_atype
2356 | _ => individual_atype
2357 fun typ 0 = if pred_sym then bool_atype else ind
2358 | typ ary = AFun (ind, typ (ary - 1))
2361 fun nary_type_constr_type n =
2362 funpow n (curry AFun atype_of_types) atype_of_types
2364 fun undeclared_syms_in_problem type_enc problem =
2366 val declared = declared_syms_in_problem problem
2367 fun do_sym name ty =
2368 if member (op =) declared name then I else AList.default (op =) (name, ty)
2369 fun do_type (AType (name as (s, _), tys)) =
2370 is_tptp_user_symbol s
2371 ? do_sym name (fn () => nary_type_constr_type (length tys))
2373 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
2374 | do_type (ATyAbs (_, ty)) = do_type ty
2375 fun do_term pred_sym (ATerm (name as (s, _), tms)) =
2376 is_tptp_user_symbol s
2377 ? do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
2378 #> fold (do_term false) tms
2379 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
2380 fun do_formula (AQuant (_, xs, phi)) =
2381 fold do_type (map_filter snd xs) #> do_formula phi
2382 | do_formula (AConn (_, phis)) = fold do_formula phis
2383 | do_formula (AAtom tm) = do_term true tm
2384 fun do_problem_line (Decl (_, _, ty)) = do_type ty
2385 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
2387 fold (fold do_problem_line o snd) problem []
2388 |> filter_out (is_built_in_tptp_symbol o fst o fst)
2391 fun declare_undeclared_syms_in_atp_problem type_enc problem =
2395 |> undeclared_syms_in_problem type_enc
2396 |> sort_wrt (fst o fst)
2397 |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
2398 in (implicit_declsN, decls) :: problem end
2400 fun exists_subdtype P =
2402 fun ex U = P U orelse
2403 (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false)
2406 fun is_poly_constr (_, Us) =
2407 exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
2409 fun all_constrs_of_polymorphic_datatypes thy =
2413 #> (fn cs => exists is_poly_constr cs ? append cs))
2414 (Datatype.get_all thy) []
2415 |> List.partition is_poly_constr
2416 |> pairself (map fst)
2418 (* Forcing explicit applications is expensive for polymorphic encodings, because
2419 it takes only one existential variable ranging over "'a => 'b" to ruin
2420 everything. Hence we do it only if there are few facts (is normally the case
2421 for "metis" and the minimizer. *)
2422 val explicit_apply_threshold = 50
2424 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
2425 lam_trans readable_names preproc hyp_ts concl_t facts =
2427 val thy = Proof_Context.theory_of ctxt
2428 val type_enc = type_enc |> adjust_type_enc format
2429 val explicit_apply =
2430 if polymorphism_of_type_enc type_enc <> Polymorphic orelse
2431 length facts <= explicit_apply_threshold then
2436 if lam_trans = keep_lamsN andalso
2437 not (is_type_enc_higher_order type_enc) then
2438 error ("Lambda translation scheme incompatible with first-order \
2442 val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
2444 translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
2446 val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts
2447 val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
2448 val (polym_constrs, monom_constrs) =
2449 all_constrs_of_polymorphic_datatypes thy
2450 |>> map (make_fixed_const (SOME format))
2452 firstorderize_fact thy monom_constrs format type_enc sym_tab
2453 val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
2454 val sym_tab = sym_table_for_facts ctxt type_enc (SOME false) conjs facts
2456 sym_tab |> helper_facts_for_sym_table ctxt format type_enc
2457 |> map firstorderize
2459 helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
2460 val class_decl_lines = decl_lines_for_classes type_enc classes
2461 val sym_decl_lines =
2462 (conjs, helpers @ facts)
2463 |> sym_decl_table_for_facts ctxt format type_enc sym_tab
2464 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
2467 0 upto length helpers - 1 ~~ helpers
2468 |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I
2469 false true mono type_enc)
2470 |> (if needs_type_tag_idempotence ctxt type_enc then
2471 cons (type_tag_idempotence_fact format type_enc)
2474 (* Reordering these might confuse the proof reconstruction code or the SPASS
2477 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
2479 map (formula_line_for_fact ctxt polym_constrs format fact_prefix
2480 ascii_of (not exporter) (not exporter) mono type_enc)
2481 (0 upto length facts - 1 ~~ facts)),
2483 map (formula_line_for_class_rel_clause format type_enc)
2486 map (formula_line_for_arity_clause format type_enc) arity_clauses),
2487 (helpersN, helper_lines),
2489 map (formula_line_for_conjecture ctxt polym_constrs format mono
2491 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
2495 CNF => ensure_cnf_problem
2496 | CNF_UEQ => filter_cnf_ueq_problem
2498 | TFF (_, TPTP_Implicit) => I
2499 | THF (_, TPTP_Implicit, _) => I
2500 | _ => declare_undeclared_syms_in_atp_problem type_enc)
2501 val (problem, pool) = problem |> nice_atp_problem readable_names format
2502 fun add_sym_ary (s, {min_ary, ...} : sym_info) =
2503 min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
2506 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
2507 fact_names |> Vector.fromList,
2509 Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
2513 val conj_weight = 0.0
2514 val hyp_weight = 0.1
2515 val fact_min_weight = 0.2
2516 val fact_max_weight = 1.0
2517 val type_info_default_weight = 0.8
2519 fun add_term_weights weight (ATerm (s, tms)) =
2520 is_tptp_user_symbol s ? Symtab.default (s, weight)
2521 #> fold (add_term_weights weight) tms
2522 | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
2523 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
2524 formula_fold NONE (K (add_term_weights weight)) phi
2525 | add_problem_line_weights _ _ = I
2527 fun add_conjectures_weights [] = I
2528 | add_conjectures_weights conjs =
2529 let val (hyps, conj) = split_last conjs in
2530 add_problem_line_weights conj_weight conj
2531 #> fold (add_problem_line_weights hyp_weight) hyps
2534 fun add_facts_weights facts =
2536 val num_facts = length facts
2538 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
2539 / Real.fromInt num_facts
2541 map weight_of (0 upto num_facts - 1) ~~ facts
2542 |> fold (uncurry add_problem_line_weights)
2545 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
2546 fun atp_problem_weights problem =
2547 let val get = these o AList.lookup (op =) problem in
2549 |> add_conjectures_weights (get free_typesN @ get conjsN)
2550 |> add_facts_weights (get factsN)
2551 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
2552 [explicit_declsN, class_relsN, aritiesN]
2554 |> sort (prod_ord Real.compare string_ord o pairself swap)