1 (* Title: HOL/Tools/ATP/atp_problem_generate.ML
2 Author: Fabian Immler, TU Muenchen
4 Author: Jasmin Blanchette, TU Muenchen
6 Translation of HOL to FOL for Metis and Sledgehammer.
9 signature ATP_PROBLEM_GENERATE =
11 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
12 type connective = ATP_Problem.connective
13 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
14 type atp_format = ATP_Problem.atp_format
15 type formula_kind = ATP_Problem.formula_kind
16 type 'a problem = 'a ATP_Problem.problem
18 datatype scope = Global | Local | Assum | Chained
19 datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
20 type stature = scope * status
22 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
23 datatype strictness = Strict | Non_Strict
24 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
27 Noninf_Nonmono_Types of strictness * granularity |
28 Fin_Nonmono_Types of granularity |
33 val type_tag_idempotence : bool Config.T
34 val type_tag_arguments : bool Config.T
36 val hide_lamsN : string
39 val combs_and_liftingN : string
40 val combs_or_liftingN : string
41 val lam_liftingN : string
42 val keep_lamsN : string
43 val schematic_var_prefix : string
44 val fixed_var_prefix : string
45 val tvar_prefix : string
46 val tfree_prefix : string
47 val const_prefix : string
48 val type_const_prefix : string
49 val class_prefix : string
50 val lam_lifted_prefix : string
51 val lam_lifted_mono_prefix : string
52 val lam_lifted_poly_prefix : string
53 val skolem_const_prefix : string
54 val old_skolem_const_prefix : string
55 val new_skolem_const_prefix : string
56 val combinator_prefix : string
57 val type_decl_prefix : string
58 val sym_decl_prefix : string
59 val guards_sym_formula_prefix : string
60 val tags_sym_formula_prefix : string
61 val fact_prefix : string
62 val conjecture_prefix : string
63 val helper_prefix : string
64 val class_rel_clause_prefix : string
65 val arity_clause_prefix : string
66 val tfree_clause_prefix : string
67 val lam_fact_prefix : string
68 val typed_helper_suffix : string
69 val untyped_helper_suffix : string
70 val type_tag_idempotence_helper_name : string
71 val predicator_name : string
72 val app_op_name : string
73 val type_guard_name : string
74 val type_tag_name : string
75 val native_type_prefix : string
76 val prefixed_predicator_name : string
77 val prefixed_app_op_name : string
78 val prefixed_type_tag_name : string
79 val ascii_of : string -> string
80 val unascii_of : string -> string
81 val unprefix_and_unascii : string -> string -> string option
82 val proxy_table : (string * (string * (thm * (string * string)))) list
83 val proxify_const : string -> (string * string) option
84 val invert_const : string -> string
85 val unproxify_const : string -> string
86 val new_skolem_var_name_from_const : string -> string
87 val atp_irrelevant_consts : string list
88 val atp_schematic_consts_of : term -> typ list Symtab.table
89 val is_type_enc_higher_order : type_enc -> bool
90 val polymorphism_of_type_enc : type_enc -> polymorphism
91 val level_of_type_enc : type_enc -> type_level
92 val is_type_enc_quasi_sound : type_enc -> bool
93 val is_type_enc_fairly_sound : type_enc -> bool
94 val type_enc_from_string : strictness -> string -> type_enc
95 val adjust_type_enc : atp_format -> type_enc -> type_enc
97 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
98 val unmangled_const : string -> string * (string, 'b) ho_term list
99 val unmangled_const_name : string -> string list
100 val helper_table : ((string * bool) * thm list) list
101 val trans_lams_from_string :
102 Proof.context -> type_enc -> string -> term list -> term list * term list
104 val prepare_atp_problem :
105 Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
106 -> bool -> string -> bool -> bool -> bool -> term list -> term
107 -> ((string * stature) * term) list
108 -> string problem * string Symtab.table * (string * stature) list vector
109 * (string * term) list * int Symtab.table
110 val atp_problem_relevance_weights : string problem -> (string * real) list
111 val atp_problem_kbo_weights : string problem -> (string * int) list
114 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
120 type name = string * string
122 val type_tag_idempotence =
123 Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
124 val type_tag_arguments =
125 Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
127 val no_lamsN = "no_lams" (* used internally; undocumented *)
128 val hide_lamsN = "hide_lams"
129 val liftingN = "lifting"
131 val combs_and_liftingN = "combs_and_lifting"
132 val combs_or_liftingN = "combs_or_lifting"
133 val keep_lamsN = "keep_lams"
134 val lam_liftingN = "lam_lifting" (* legacy *)
136 (* It's still unclear whether all TFF1 implementations will support type
137 signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
138 val avoid_first_order_ghost_type_vars = false
140 val bound_var_prefix = "B_"
141 val all_bound_var_prefix = "BA_"
142 val exist_bound_var_prefix = "BE_"
143 val schematic_var_prefix = "V_"
144 val fixed_var_prefix = "v_"
145 val tvar_prefix = "T_"
146 val tfree_prefix = "t_"
147 val const_prefix = "c_"
148 val type_const_prefix = "tc_"
149 val native_type_prefix = "n_"
150 val class_prefix = "cl_"
152 (* Freshness almost guaranteed! *)
153 val atp_prefix = "ATP" ^ Long_Name.separator
154 val atp_weak_prefix = "ATP:"
156 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
157 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
158 val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
160 val skolem_const_prefix = atp_prefix ^ "Sko"
161 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
162 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
164 val combinator_prefix = "COMB"
166 val type_decl_prefix = "ty_"
167 val sym_decl_prefix = "sy_"
168 val guards_sym_formula_prefix = "gsy_"
169 val tags_sym_formula_prefix = "tsy_"
170 val uncurried_alias_eq_prefix = "unc_"
171 val fact_prefix = "fact_"
172 val conjecture_prefix = "conj_"
173 val helper_prefix = "help_"
174 val class_rel_clause_prefix = "clar_"
175 val arity_clause_prefix = "arity_"
176 val tfree_clause_prefix = "tfree_"
178 val lam_fact_prefix = "ATP.lambda_"
179 val typed_helper_suffix = "_T"
180 val untyped_helper_suffix = "_U"
181 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
183 val predicator_name = "pp"
184 val app_op_name = "aa"
185 val type_guard_name = "gg"
186 val type_tag_name = "tt"
188 val prefixed_predicator_name = const_prefix ^ predicator_name
189 val prefixed_app_op_name = const_prefix ^ app_op_name
190 val prefixed_type_tag_name = const_prefix ^ type_tag_name
192 (*Escaping of special characters.
193 Alphanumeric characters are left unchanged.
194 The character _ goes to __
195 Characters in the range ASCII space to / go to _A to _P, respectively.
196 Other characters go to _nnn where nnn is the decimal ASCII code.*)
197 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
199 fun stringN_of_int 0 _ = ""
200 | stringN_of_int k n =
201 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
203 fun ascii_of_char c =
204 if Char.isAlphaNum c then
206 else if c = #"_" then
208 else if #" " <= c andalso c <= #"/" then
209 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
211 (* fixed width, in case more digits follow *)
212 "_" ^ stringN_of_int 3 (Char.ord c)
214 val ascii_of = String.translate ascii_of_char
216 (** Remove ASCII armoring from names in proof files **)
218 (* We don't raise error exceptions because this code can run inside a worker
219 thread. Also, the errors are impossible. *)
222 fun un rcs [] = String.implode(rev rcs)
223 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
224 (* Three types of _ escapes: __, _A to _P, _nnn *)
225 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
226 | un rcs (#"_" :: c :: cs) =
227 if #"A" <= c andalso c<= #"P" then
228 (* translation of #" " to #"/" *)
229 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
231 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
232 case Int.fromString (String.implode digits) of
233 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
234 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
236 | un rcs (c :: cs) = un (c :: rcs) cs
237 in un [] o String.explode end
239 (* If string s has the prefix s1, return the result of deleting it,
241 fun unprefix_and_unascii s1 s =
242 if String.isPrefix s1 s then
243 SOME (unascii_of (String.extract (s, size s1, NONE)))
248 [("c_False", (@{const_name False}, (@{thm fFalse_def},
249 ("fFalse", @{const_name ATP.fFalse})))),
250 ("c_True", (@{const_name True}, (@{thm fTrue_def},
251 ("fTrue", @{const_name ATP.fTrue})))),
252 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
253 ("fNot", @{const_name ATP.fNot})))),
254 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
255 ("fconj", @{const_name ATP.fconj})))),
256 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
257 ("fdisj", @{const_name ATP.fdisj})))),
258 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
259 ("fimplies", @{const_name ATP.fimplies})))),
260 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
261 ("fequal", @{const_name ATP.fequal})))),
262 ("c_All", (@{const_name All}, (@{thm fAll_def},
263 ("fAll", @{const_name ATP.fAll})))),
264 ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
265 ("fEx", @{const_name ATP.fEx}))))]
267 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
269 (* Readable names for the more common symbolic functions. Do not mess with the
270 table unless you know what you are doing. *)
271 val const_trans_table =
272 [(@{type_name Product_Type.prod}, "prod"),
273 (@{type_name Sum_Type.sum}, "sum"),
274 (@{const_name False}, "False"),
275 (@{const_name True}, "True"),
276 (@{const_name Not}, "Not"),
277 (@{const_name conj}, "conj"),
278 (@{const_name disj}, "disj"),
279 (@{const_name implies}, "implies"),
280 (@{const_name HOL.eq}, "equal"),
281 (@{const_name All}, "All"),
282 (@{const_name Ex}, "Ex"),
283 (@{const_name If}, "If"),
284 (@{const_name Set.member}, "member"),
285 (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
286 (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
287 (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
288 (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
289 (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
291 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
293 (* Invert the table of translations between Isabelle and ATPs. *)
294 val const_trans_table_inv =
295 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
296 val const_trans_table_unprox =
298 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
300 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
301 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
304 case Symtab.lookup const_trans_table c of
308 fun ascii_of_indexname (v, 0) = ascii_of v
309 | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
311 fun make_bound_var x = bound_var_prefix ^ ascii_of x
312 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
313 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
314 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
315 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
317 fun make_schematic_type_var (x, i) =
318 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
319 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
321 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
323 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
324 fun default c = const_prefix ^ lookup_const c
326 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
327 | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
328 if c = choice_const then tptp_choice else default c
329 | make_fixed_const _ c = default c
332 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
334 fun make_type_class clas = class_prefix ^ ascii_of clas
336 fun new_skolem_var_name_from_const s =
337 let val ss = s |> space_explode Long_Name.separator in
338 nth ss (length ss - 2)
341 (* These are either simplified away by "Meson.presimplify" (most of the time) or
342 handled specially via "fFalse", "fTrue", ..., "fequal". *)
343 val atp_irrelevant_consts =
344 [@{const_name False}, @{const_name True}, @{const_name Not},
345 @{const_name conj}, @{const_name disj}, @{const_name implies},
346 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
348 val atp_monomorph_bad_consts =
349 atp_irrelevant_consts @
350 (* These are ignored anyway by the relevance filter (unless they appear in
351 higher-order places) but not by the monomorphizer. *)
352 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
353 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
354 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
356 fun add_schematic_const (x as (_, T)) =
357 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
358 val add_schematic_consts_of =
359 Term.fold_aterms (fn Const (x as (s, _)) =>
360 not (member (op =) atp_monomorph_bad_consts s)
361 ? add_schematic_const x
363 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
365 (** Definitions and functions for FOL clauses and formulas for TPTP **)
367 (** Isabelle arities **)
369 type arity_atom = name * name * name list
371 val type_class = the_single @{sort type}
375 prem_atoms : arity_atom list,
376 concl_atom : arity_atom}
378 fun add_prem_atom tvar =
379 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
381 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
382 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
384 val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
385 val tvars_srts = ListPair.zip (tvars, args)
388 prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
389 concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
393 fun arity_clause _ _ (_, []) = []
394 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
395 arity_clause seen n (tcons, ars)
396 | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
397 if member (op =) seen class then
398 (* multiple arities for the same (tycon, class) pair *)
399 make_axiom_arity_clause (tcons,
400 lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
402 arity_clause seen (n + 1) (tcons, ars)
404 make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
405 ascii_of class, ar) ::
406 arity_clause (class :: seen) n (tcons, ars)
408 fun multi_arity_clause [] = []
409 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
410 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
412 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
413 theory thy provided its arguments have the corresponding sorts. *)
414 fun type_class_pairs thy tycons classes =
416 val alg = Sign.classes_of thy
417 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
418 fun add_class tycon class =
419 cons (class, domain_sorts tycon class)
420 handle Sorts.CLASS_ERROR _ => I
421 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
422 in map try_classes tycons end
424 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
425 fun iter_type_class_pairs _ _ [] = ([], [])
426 | iter_type_class_pairs thy tycons classes =
428 fun maybe_insert_class s =
429 (s <> type_class andalso not (member (op =) classes s))
431 val cpairs = type_class_pairs thy tycons classes
433 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
434 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
435 in (classes' @ classes, union (op =) cpairs' cpairs) end
437 fun make_arity_clauses thy tycons =
438 iter_type_class_pairs thy tycons ##> multi_arity_clause
441 (** Isabelle class relations **)
443 type class_rel_clause =
448 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
450 fun class_pairs _ [] _ = []
451 | class_pairs thy subs supers =
453 val class_less = Sorts.class_less (Sign.classes_of thy)
454 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
455 fun add_supers sub = fold (add_super sub) supers
456 in fold add_supers subs [] end
458 fun make_class_rel_clause (sub, super) =
459 {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
460 superclass = `make_type_class super}
462 fun make_class_rel_clauses thy subs supers =
463 map make_class_rel_clause (class_pairs thy subs supers)
465 (* intermediate terms *)
467 IConst of name * typ * typ list |
469 IApp of iterm * iterm |
470 IAbs of (name * typ) * iterm
472 fun ityp_of (IConst (_, T, _)) = T
473 | ityp_of (IVar (_, T)) = T
474 | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
475 | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
477 (*gets the head of a combinator application, along with the list of arguments*)
478 fun strip_iterm_comb u =
480 fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
482 in stripc (u, []) end
484 fun atomic_types_of T = fold_atyps (insert (op =)) T []
486 val tvar_a_str = "'a"
487 val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
488 val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
489 val itself_name = `make_fixed_type_const @{type_name itself}
490 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
491 val tvar_a_atype = AType (tvar_a_name, [])
492 val a_itself_atype = AType (itself_name, [tvar_a_atype])
494 fun new_skolem_const_name s num_T_args =
495 [new_skolem_const_prefix, s, string_of_int num_T_args]
496 |> space_implode Long_Name.separator
498 fun robust_const_type thy s =
499 if s = app_op_name then
500 Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
501 else if String.isPrefix lam_lifted_prefix s then
502 Logic.varifyT_global @{typ "'a => 'b"}
504 (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
505 s |> Sign.the_const_type thy
507 (* This function only makes sense if "T" is as general as possible. *)
508 fun robust_const_typargs thy (s, T) =
509 if s = app_op_name then
510 let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
511 else if String.isPrefix old_skolem_const_prefix s then
512 [] |> Term.add_tvarsT T |> rev |> map TVar
513 else if String.isPrefix lam_lifted_prefix s then
514 if String.isPrefix lam_lifted_poly_prefix s then
515 let val (T1, T2) = T |> dest_funT in [T1, T2] end
519 (s, T) |> Sign.const_typargs thy
521 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
522 Also accumulates sort infomation. *)
523 fun iterm_from_term thy format bs (P $ Q) =
525 val (P', P_atomics_Ts) = iterm_from_term thy format bs P
526 val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
527 in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
528 | iterm_from_term thy format _ (Const (c, T)) =
529 (IConst (`(make_fixed_const (SOME format)) c, T,
530 robust_const_typargs thy (c, T)),
532 | iterm_from_term _ _ _ (Free (s, T)) =
533 (IConst (`make_fixed_var s, T, []), atomic_types_of T)
534 | iterm_from_term _ format _ (Var (v as (s, _), T)) =
535 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
537 val Ts = T |> strip_type |> swap |> op ::
538 val s' = new_skolem_const_name s (length Ts)
539 in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
541 IVar ((make_schematic_var v, s), T), atomic_types_of T)
542 | iterm_from_term _ _ bs (Bound j) =
543 nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
544 | iterm_from_term thy format bs (Abs (s, T, t)) =
546 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
548 val name = `make_bound_var s
549 val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
550 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
552 datatype scope = Global | Local | Assum | Chained
553 datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
554 type stature = scope * status
556 datatype order = First_Order | Higher_Order
557 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
558 datatype strictness = Strict | Non_Strict
559 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
560 datatype type_level =
562 Noninf_Nonmono_Types of strictness * granularity |
563 Fin_Nonmono_Types of granularity |
568 Simple_Types of order * polymorphism * type_level |
569 Guards of polymorphism * type_level |
570 Tags of polymorphism * type_level
572 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
573 | is_type_enc_higher_order _ = false
575 fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
576 | polymorphism_of_type_enc (Guards (poly, _)) = poly
577 | polymorphism_of_type_enc (Tags (poly, _)) = poly
579 fun level_of_type_enc (Simple_Types (_, _, level)) = level
580 | level_of_type_enc (Guards (_, level)) = level
581 | level_of_type_enc (Tags (_, level)) = level
583 fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
584 | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
585 | granularity_of_type_level _ = All_Vars
587 fun is_type_level_quasi_sound All_Types = true
588 | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
589 | is_type_level_quasi_sound _ = false
590 val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
592 fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
593 | is_type_level_fairly_sound level = is_type_level_quasi_sound level
594 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
596 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
597 | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
598 | is_type_level_monotonicity_based _ = false
600 (* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
602 val queries = ["?", "_query"]
603 val bangs = ["!", "_bang"]
604 val ats = ["@", "_at"]
606 fun try_unsuffixes ss s =
607 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
609 fun try_nonmono constr suffixes fallback s =
610 case try_unsuffixes suffixes s of
612 (case try_unsuffixes suffixes s of
613 SOME s => (constr Positively_Naked_Vars, s)
615 case try_unsuffixes ats s of
616 SOME s => (constr Ghost_Type_Arg_Vars, s)
617 | NONE => (constr All_Vars, s))
620 fun type_enc_from_string strictness s =
621 (case try (unprefix "poly_") s of
622 SOME s => (SOME Polymorphic, s)
624 case try (unprefix "raw_mono_") s of
625 SOME s => (SOME Raw_Monomorphic, s)
627 case try (unprefix "mono_") s of
628 SOME s => (SOME Mangled_Monomorphic, s)
631 |> try_nonmono Fin_Nonmono_Types bangs
632 |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
633 |> (fn (poly, (level, core)) =>
634 case (core, (poly, level)) of
635 ("native", (SOME poly, _)) =>
636 (case (poly, level) of
637 (Polymorphic, All_Types) =>
638 Simple_Types (First_Order, Polymorphic, All_Types)
639 | (Mangled_Monomorphic, _) =>
640 if granularity_of_type_level level = All_Vars then
641 Simple_Types (First_Order, Mangled_Monomorphic, level)
644 | _ => raise Same.SAME)
645 | ("native_higher", (SOME poly, _)) =>
646 (case (poly, level) of
647 (Polymorphic, All_Types) =>
648 Simple_Types (Higher_Order, Polymorphic, All_Types)
649 | (_, Noninf_Nonmono_Types _) => raise Same.SAME
650 | (Mangled_Monomorphic, _) =>
651 if granularity_of_type_level level = All_Vars then
652 Simple_Types (Higher_Order, Mangled_Monomorphic, level)
655 | _ => raise Same.SAME)
656 | ("guards", (SOME poly, _)) =>
657 if poly = Mangled_Monomorphic andalso
658 granularity_of_type_level level = Ghost_Type_Arg_Vars then
662 | ("tags", (SOME poly, _)) =>
663 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
667 | ("args", (SOME poly, All_Types (* naja *))) =>
668 Guards (poly, Const_Arg_Types)
669 | ("erased", (NONE, All_Types (* naja *))) =>
670 Guards (Polymorphic, No_Types)
671 | _ => raise Same.SAME)
672 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
674 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
675 (Simple_Types (order, _, level)) =
676 Simple_Types (order, Mangled_Monomorphic, level)
677 | adjust_type_enc (THF _) type_enc = type_enc
678 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
679 Simple_Types (First_Order, Mangled_Monomorphic, level)
680 | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
681 Simple_Types (First_Order, Mangled_Monomorphic, level)
682 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
683 Simple_Types (First_Order, poly, level)
684 | adjust_type_enc format (Simple_Types (_, poly, level)) =
685 adjust_type_enc format (Guards (poly, level))
686 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
687 (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
688 | adjust_type_enc _ type_enc = type_enc
690 fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
691 | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
692 | constify_lifted (Free (x as (s, _))) =
693 (if String.isPrefix lam_lifted_prefix s then Const else Free) x
694 | constify_lifted t = t
696 (* Requires bound variables not to clash with any schematic variables (as should
697 be the case right after lambda-lifting). *)
698 fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
699 (case try unprefix s of
702 val names = Name.make_context (map fst (Term.add_var_names t' []))
703 val (s, _) = Name.variant s names
704 in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end
708 fun lift_lams_part_1 ctxt type_enc =
709 map close_form #> rpair ctxt
710 #-> Lambda_Lifting.lift_lambdas
711 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
712 lam_lifted_poly_prefix
714 lam_lifted_mono_prefix) ^ "_a"))
715 Lambda_Lifting.is_quantifier
717 fun lift_lams_part_2 (facts, lifted) =
718 (map (open_form (unprefix close_form_prefix) o constify_lifted) facts,
719 map (open_form I o constify_lifted) lifted)
720 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1
722 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
724 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
726 fun lam T t = Abs (Name.uu, T, t)
727 val (head, args) = strip_comb t ||> rev
728 val head_T = fastype_of head
730 val arg_Ts = head_T |> binder_types |> take n |> rev
731 val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
732 in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
733 | intentionalize_def t = t
735 type translated_formula =
739 iformula : (name, typ, iterm) formula,
740 atomic_types : typ list}
742 fun update_iformula f ({name, stature, kind, iformula, atomic_types}
743 : translated_formula) =
744 {name = name, stature = stature, kind = kind, iformula = f iformula,
745 atomic_types = atomic_types} : translated_formula
747 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
749 fun insert_type ctxt get_T x xs =
750 let val T = get_T x in
751 if exists (type_instance ctxt T o get_T) xs then xs
752 else x :: filter_out (type_generalization ctxt T o get_T) xs
755 (* The Booleans indicate whether all type arguments should be kept. *)
756 datatype type_arg_policy =
757 Explicit_Type_Args of bool (* infer_from_term_args *) |
761 fun type_arg_policy monom_constrs type_enc s =
762 let val poly = polymorphism_of_type_enc type_enc in
763 if s = type_tag_name then
764 if poly = Mangled_Monomorphic then Mangled_Type_Args
765 else Explicit_Type_Args false
766 else case type_enc of
767 Simple_Types (_, Polymorphic, _) => Explicit_Type_Args false
768 | Tags (_, All_Types) => No_Type_Args
770 let val level = level_of_type_enc type_enc in
771 if level = No_Types orelse s = @{const_name HOL.eq} orelse
772 (s = app_op_name andalso level = Const_Arg_Types) then
774 else if poly = Mangled_Monomorphic then
776 else if member (op =) monom_constrs s andalso
777 granularity_of_type_level level = Positively_Naked_Vars then
781 (level = All_Types orelse
782 granularity_of_type_level level = Ghost_Type_Arg_Vars)
786 (* Make atoms for sorted type variables. *)
787 fun generic_add_sorts_on_type (_, []) = I
788 | generic_add_sorts_on_type ((x, i), s :: ss) =
789 generic_add_sorts_on_type ((x, i), ss)
790 #> (if s = the_single @{sort HOL.type} then
793 insert (op =) (`make_type_class s, `make_fixed_type_var x)
795 insert (op =) (`make_type_class s,
796 (make_schematic_type_var (x, i), x)))
797 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
798 | add_sorts_on_tfree _ = I
799 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
800 | add_sorts_on_tvar _ = I
802 fun type_class_formula type_enc class arg =
803 AAtom (ATerm (class, arg ::
805 Simple_Types (First_Order, Polymorphic, _) =>
806 if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
809 fun formulas_for_types type_enc add_sorts_on_typ Ts =
810 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
811 |> map (fn (class, name) =>
812 type_class_formula type_enc class (ATerm (name, [])))
814 fun mk_aconns c phis =
815 let val (phis', phi') = split_last phis in
816 fold_rev (mk_aconn c) phis' phi'
818 fun mk_ahorn [] phi = phi
819 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
820 fun mk_aquant _ [] phi = phi
821 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
822 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
823 | mk_aquant q xs phi = AQuant (q, xs, phi)
825 fun close_universally add_term_vars phi =
827 fun add_formula_vars bounds (AQuant (_, xs, phi)) =
828 add_formula_vars (map fst xs @ bounds) phi
829 | add_formula_vars bounds (AConn (_, phis)) =
830 fold (add_formula_vars bounds) phis
831 | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
832 in mk_aquant AForall (add_formula_vars [] phi []) phi end
834 fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
835 (if is_tptp_variable s andalso
836 not (String.isPrefix tvar_prefix s) andalso
837 not (member (op =) bounds name) then
838 insert (op =) (name, NONE)
841 #> fold (add_term_vars bounds) tms
842 | add_term_vars bounds (AAbs ((name, _), tm)) =
843 add_term_vars (name :: bounds) tm
844 fun close_formula_universally phi = close_universally add_term_vars phi
846 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
847 fold (add_iterm_vars bounds) [tm1, tm2]
848 | add_iterm_vars _ (IConst _) = I
849 | add_iterm_vars bounds (IVar (name, T)) =
850 not (member (op =) bounds name) ? insert (op =) (name, SOME T)
851 | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
852 fun close_iformula_universally phi = close_universally add_iterm_vars phi
854 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
855 val fused_infinite_type = Type (fused_infinite_type_name, [])
857 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
859 fun ho_term_from_typ format type_enc =
861 fun term (Type (s, Ts)) =
862 ATerm (case (is_type_enc_higher_order type_enc, s) of
863 (true, @{type_name bool}) => `I tptp_bool_type
864 | (true, @{type_name fun}) => `I tptp_fun_type
865 | _ => if s = fused_infinite_type_name andalso
866 is_format_typed format then
867 `I tptp_individual_type
869 `make_fixed_type_const s,
871 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
872 | term (TVar (x, _)) = ATerm (tvar_name x, [])
875 fun ho_term_for_type_arg format type_enc T =
876 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
878 (* This shouldn't clash with anything else. *)
879 val uncurried_alias_sep = "\000"
880 val mangled_type_sep = "\001"
882 val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
884 fun generic_mangled_type_name f (ATerm (name, [])) = f name
885 | generic_mangled_type_name f (ATerm (name, tys)) =
886 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
888 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
890 fun mangled_type format type_enc =
891 generic_mangled_type_name fst o ho_term_from_typ format type_enc
893 fun make_native_type s =
894 if s = tptp_bool_type orelse s = tptp_fun_type orelse
895 s = tptp_individual_type then
898 native_type_prefix ^ ascii_of s
900 fun ho_type_from_ho_term type_enc pred_sym ary =
902 fun to_mangled_atype ty =
903 AType ((make_native_type (generic_mangled_type_name fst ty),
904 generic_mangled_type_name snd ty), [])
905 fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
906 | to_poly_atype _ = raise Fail "unexpected type abstraction"
908 if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
909 else to_mangled_atype
910 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
911 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
912 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
913 | to_fo _ _ = raise Fail "unexpected type abstraction"
914 fun to_ho (ty as ATerm ((s, _), tys)) =
915 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
916 | to_ho _ = raise Fail "unexpected type abstraction"
917 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
919 fun ho_type_from_typ format type_enc pred_sym ary =
920 ho_type_from_ho_term type_enc pred_sym ary
921 o ho_term_from_typ format type_enc
923 fun aliased_uncurried ary (s, s') =
924 (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
925 fun unaliased_uncurried (s, s') =
926 case space_explode uncurried_alias_sep s of
928 | [s1, s2] => (s1, unsuffix s2 s')
929 | _ => raise Fail "ill-formed explicit application alias"
931 fun raw_mangled_const_name type_name ty_args (s, s') =
933 fun type_suffix f g =
934 fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
936 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
937 fun mangled_const_name format type_enc =
938 map_filter (ho_term_for_type_arg format type_enc)
939 #> raw_mangled_const_name generic_mangled_type_name
941 val parse_mangled_ident =
942 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
944 fun parse_mangled_type x =
946 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
948 and parse_mangled_types x =
949 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
951 fun unmangled_type s =
952 s |> suffix ")" |> raw_explode
953 |> Scan.finite Symbol.stopper
954 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
955 quote s)) parse_mangled_type))
958 fun unmangled_const_name s =
959 (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
960 fun unmangled_const s =
961 let val ss = unmangled_const_name s in
962 (hd ss, map unmangled_type (tl ss))
965 fun introduce_proxies_in_iterm type_enc =
967 fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
968 | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
970 (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
971 limitation. This works in conjuction with special code in
972 "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
975 IApp (IConst (`I ho_quant, T, []),
977 IApp (IConst (`I "P", p_T, []),
978 IConst (`I "X", x_T, [])))))
979 | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
980 fun intro top_level args (IApp (tm1, tm2)) =
981 IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
982 | intro top_level args (IConst (name as (s, _), T, T_args)) =
983 (case proxify_const s of
985 if top_level orelse is_type_enc_higher_order type_enc then
986 case (top_level, s) of
987 (_, "c_False") => IConst (`I tptp_false, T, [])
988 | (_, "c_True") => IConst (`I tptp_true, T, [])
989 | (false, "c_Not") => IConst (`I tptp_not, T, [])
990 | (false, "c_conj") => IConst (`I tptp_and, T, [])
991 | (false, "c_disj") => IConst (`I tptp_or, T, [])
992 | (false, "c_implies") => IConst (`I tptp_implies, T, [])
993 | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
994 | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
996 if is_tptp_equal s andalso length args = 2 then
997 IConst (`I tptp_equal, T, [])
999 (* Use a proxy even for partially applied THF0 equality,
1000 because the LEO-II and Satallax parsers complain about not
1001 being able to infer the type of "=". *)
1002 IConst (proxy_base |>> prefix const_prefix, T, T_args)
1003 | _ => IConst (name, T, [])
1005 IConst (proxy_base |>> prefix const_prefix, T, T_args)
1006 | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
1007 else IConst (name, T, T_args))
1008 | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
1010 in intro true [] end
1012 fun mangle_type_args_in_const format type_enc (name as (s, _)) T_args =
1013 case unprefix_and_unascii const_prefix s of
1014 NONE => (name, T_args)
1016 case type_arg_policy [] type_enc (invert_const s'') of
1017 Mangled_Type_Args => (mangled_const_name format type_enc T_args name, [])
1018 | _ => (name, T_args)
1019 fun mangle_type_args_in_iterm format type_enc =
1020 if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
1022 fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
1023 | mangle (tm as IConst (_, _, [])) = tm
1024 | mangle (IConst (name, T, T_args)) =
1025 mangle_type_args_in_const format type_enc name T_args
1026 |> (fn (name, T_args) => IConst (name, T, T_args))
1027 | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
1033 fun chop_fun 0 T = ([], T)
1034 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1035 chop_fun (n - 1) ran_T |>> cons dom_T
1036 | chop_fun _ T = ([], T)
1038 fun filter_const_type_args _ _ _ [] = []
1039 | filter_const_type_args thy s ary T_args =
1041 val U = robust_const_type thy s
1042 val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
1043 val U_args = (s, U) |> robust_const_typargs thy
1046 |> map (fn (U, T) =>
1047 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
1049 handle TYPE _ => T_args
1051 fun filter_type_args_in_const _ _ _ _ _ [] = []
1052 | filter_type_args_in_const thy monom_constrs type_enc ary s T_args =
1053 case unprefix_and_unascii const_prefix s of
1055 if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
1059 val s'' = invert_const s''
1060 fun filter_T_args false = T_args
1061 | filter_T_args true = filter_const_type_args thy s'' ary T_args
1063 case type_arg_policy monom_constrs type_enc s'' of
1064 Explicit_Type_Args infer_from_term_args =>
1065 filter_T_args infer_from_term_args
1066 | No_Type_Args => []
1067 | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
1069 fun filter_type_args_in_iterm thy monom_constrs type_enc =
1071 fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
1072 | filt ary (IConst (name as (s, _), T, T_args)) =
1073 filter_type_args_in_const thy monom_constrs type_enc ary s T_args
1074 |> (fn T_args => IConst (name, T, T_args))
1075 | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
1079 fun iformula_from_prop ctxt format type_enc eq_as_iff =
1081 val thy = Proof_Context.theory_of ctxt
1082 fun do_term bs t atomic_Ts =
1083 iterm_from_term thy format bs (Envir.eta_contract t)
1084 |>> (introduce_proxies_in_iterm type_enc
1085 #> mangle_type_args_in_iterm format type_enc #> AAtom)
1086 ||> union (op =) atomic_Ts
1087 fun do_quant bs q pos s T t' =
1089 val s = singleton (Name.variant_list (map fst bs)) s
1090 val universal = Option.map (q = AExists ? not) pos
1092 s |> `(case universal of
1093 SOME true => make_all_bound_var
1094 | SOME false => make_exist_bound_var
1095 | NONE => make_bound_var)
1097 do_formula ((s, (name, T)) :: bs) pos t'
1098 #>> mk_aquant q [(name, SOME T)]
1099 ##> union (op =) (atomic_types_of T)
1101 and do_conn bs c pos1 t1 pos2 t2 =
1102 do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
1103 and do_formula bs pos t =
1105 @{const Trueprop} $ t1 => do_formula bs pos t1
1106 | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
1107 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
1108 do_quant bs AForall pos s T t'
1109 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1110 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1111 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
1112 do_quant bs AExists pos s T t'
1113 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1114 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1115 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
1116 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
1117 | @{const HOL.implies} $ t1 $ t2 =>
1118 do_conn bs AImplies (Option.map not pos) t1 pos t2
1119 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
1120 if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
1122 in do_formula [] end
1124 fun presimplify_term ctxt t =
1125 t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
1126 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
1127 #> Meson.presimplify
1130 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
1131 fun conceal_bounds Ts t =
1132 subst_bounds (map (Free o apfst concealed_bound_name)
1133 (0 upto length Ts - 1 ~~ Ts), t)
1134 fun reveal_bounds Ts =
1135 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
1136 (0 upto length Ts - 1 ~~ Ts))
1138 fun is_fun_equality (@{const_name HOL.eq},
1139 Type (_, [Type (@{type_name fun}, _), _])) = true
1140 | is_fun_equality _ = false
1142 fun extensionalize_term ctxt t =
1143 if exists_Const is_fun_equality t then
1144 let val thy = Proof_Context.theory_of ctxt in
1145 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
1146 |> prop_of |> Logic.dest_equals |> snd
1151 fun simple_translate_lambdas do_lambdas ctxt t =
1152 let val thy = Proof_Context.theory_of ctxt in
1153 if Meson.is_fol_term thy t then
1159 @{const Not} $ t1 => @{const Not} $ trans Ts t1
1160 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
1161 t0 $ Abs (s, T, trans (T :: Ts) t')
1162 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1163 trans Ts (t0 $ eta_expand Ts t1 1)
1164 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
1165 t0 $ Abs (s, T, trans (T :: Ts) t')
1166 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1167 trans Ts (t0 $ eta_expand Ts t1 1)
1168 | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
1169 t0 $ trans Ts t1 $ trans Ts t2
1170 | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
1171 t0 $ trans Ts t1 $ trans Ts t2
1172 | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
1173 t0 $ trans Ts t1 $ trans Ts t2
1174 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1176 t0 $ trans Ts t1 $ trans Ts t2
1178 if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1179 else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1180 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1181 in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
1184 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
1185 do_cheaply_conceal_lambdas Ts t1
1186 $ do_cheaply_conceal_lambdas Ts t2
1187 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
1188 Const (lam_lifted_poly_prefix ^ serial_string (),
1189 T --> fastype_of1 (T :: Ts, t))
1190 | do_cheaply_conceal_lambdas _ t = t
1192 fun do_introduce_combinators ctxt Ts t =
1193 let val thy = Proof_Context.theory_of ctxt in
1194 t |> conceal_bounds Ts
1196 |> Meson_Clausify.introduce_combinators_in_cterm
1197 |> prop_of |> Logic.dest_equals |> snd
1200 (* A type variable of sort "{}" will make abstraction fail. *)
1201 handle THM _ => t |> do_cheaply_conceal_lambdas Ts
1202 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
1204 fun preprocess_abstractions_in_terms trans_lams facts =
1206 val (facts, lambda_ts) =
1207 facts |> map (snd o snd) |> trans_lams
1208 |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
1210 map2 (fn t => fn j =>
1211 ((lam_fact_prefix ^ Int.toString j, (Global, Spec_Eq)),
1213 lambda_ts (1 upto length lambda_ts)
1214 in (facts, lam_facts) end
1216 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
1217 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
1220 fun freeze (t $ u) = freeze t $ freeze u
1221 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
1222 | freeze (Var ((s, i), T)) =
1223 Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
1225 in t |> exists_subterm is_Var t ? freeze end
1227 fun presimp_prop ctxt role t =
1229 val thy = Proof_Context.theory_of ctxt
1230 val t = t |> Envir.beta_eta_contract
1231 |> transform_elim_prop
1232 |> Object_Logic.atomize_term thy
1233 val need_trueprop = (fastype_of t = @{typ bool})
1235 t |> need_trueprop ? HOLogic.mk_Trueprop
1236 |> extensionalize_term ctxt
1237 |> presimplify_term ctxt
1238 |> HOLogic.dest_Trueprop
1240 handle TERM _ => if role = Conjecture then @{term False} else @{term True})
1243 fun make_formula ctxt format type_enc eq_as_iff name stature kind t =
1245 val (iformula, atomic_Ts) =
1246 iformula_from_prop ctxt format type_enc eq_as_iff
1247 (SOME (kind <> Conjecture)) t []
1248 |>> close_iformula_universally
1250 {name = name, stature = stature, kind = kind, iformula = iformula,
1251 atomic_types = atomic_Ts}
1254 fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
1255 case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
1256 name stature Axiom of
1257 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1258 if s = tptp_true then NONE else SOME formula
1259 | formula => SOME formula
1261 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
1262 | s_not_trueprop t =
1263 if fastype_of t = @{typ bool} then s_not t
1264 else @{prop False} (* "t" is too meta *)
1266 fun make_conjecture ctxt format type_enc =
1267 map (fn ((name, stature), (kind, t)) =>
1268 t |> kind = Conjecture ? s_not_trueprop
1269 |> make_formula ctxt format type_enc (format <> CNF) name stature
1272 (** Finite and infinite type inference **)
1274 fun tvar_footprint thy s ary =
1275 (case unprefix_and_unascii const_prefix s of
1277 s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
1278 |> map (fn T => Term.add_tvarsT T [] |> map fst)
1282 fun ghost_type_args thy s ary =
1283 if is_tptp_equal s then
1287 val footprint = tvar_footprint thy s ary
1288 val eq = (s = @{const_name HOL.eq})
1289 fun ghosts _ [] = []
1290 | ghosts seen ((i, tvars) :: args) =
1291 ghosts (union (op =) seen tvars) args
1292 |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
1295 if forall null footprint then
1298 0 upto length footprint - 1 ~~ footprint
1299 |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
1303 type monotonicity_info =
1304 {maybe_finite_Ts : typ list,
1305 surely_finite_Ts : typ list,
1306 maybe_infinite_Ts : typ list,
1307 surely_infinite_Ts : typ list,
1308 maybe_nonmono_Ts : typ list}
1310 (* These types witness that the type classes they belong to allow infinite
1311 models and hence that any types with these type classes is monotonic. *)
1312 val known_infinite_types =
1313 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
1315 fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
1316 strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
1318 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1319 dangerous because their "exhaust" properties can easily lead to unsound ATP
1320 proofs. On the other hand, all HOL infinite types can be given the same
1321 models in first-order logic (via Löwenheim-Skolem). *)
1323 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
1324 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
1325 maybe_nonmono_Ts, ...}
1326 (Noninf_Nonmono_Types (strictness, grain)) T =
1327 grain = Ghost_Type_Arg_Vars orelse
1328 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1329 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
1330 (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
1331 is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
1333 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
1334 maybe_nonmono_Ts, ...}
1335 (Fin_Nonmono_Types grain) T =
1336 grain = Ghost_Type_Arg_Vars orelse
1337 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1338 (exists (type_generalization ctxt T) surely_finite_Ts orelse
1339 (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
1340 is_type_surely_finite ctxt T)))
1341 | should_encode_type _ _ _ _ = false
1343 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
1344 should_guard_var () andalso should_encode_type ctxt mono level T
1345 | should_guard_type _ _ _ _ _ = false
1347 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
1348 String.isPrefix bound_var_prefix s orelse
1349 String.isPrefix all_bound_var_prefix s
1350 | is_maybe_universal_var (IVar _) = true
1351 | is_maybe_universal_var _ = false
1354 Top_Level of bool option |
1355 Eq_Arg of bool option |
1358 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1359 | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
1360 if granularity_of_type_level level = All_Vars then
1361 should_encode_type ctxt mono level T
1363 (case (site, is_maybe_universal_var u) of
1364 (Eq_Arg _, true) => should_encode_type ctxt mono level T
1366 | should_tag_with_type _ _ _ _ _ _ = false
1368 fun fused_type ctxt mono level =
1370 val should_encode = should_encode_type ctxt mono level
1371 fun fuse 0 T = if should_encode T then T else fused_infinite_type
1372 | fuse ary (Type (@{type_name fun}, [T1, T2])) =
1373 fuse 0 T1 --> fuse (ary - 1) T2
1374 | fuse _ _ = raise Fail "expected function type"
1377 (** predicators and application operators **)
1380 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
1383 fun default_sym_tab_entries type_enc =
1384 (make_fixed_const NONE @{const_name undefined},
1385 {pred_sym = false, min_ary = 0, max_ary = 0, types = [],
1386 in_conj = false}) ::
1387 ([tptp_false, tptp_true]
1388 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [],
1389 in_conj = false})) @
1390 ([tptp_equal, tptp_old_equal]
1391 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [],
1393 |> not (is_type_enc_higher_order type_enc)
1394 ? cons (prefixed_predicator_name,
1395 {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
1398 datatype app_op_level = Incomplete_Apply | Sufficient_Apply | Full_Apply
1400 fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
1402 fun consider_var_ary const_T var_T max_ary =
1405 if ary = max_ary orelse type_instance ctxt var_T T orelse
1406 type_instance ctxt T var_T then
1409 iter (ary + 1) (range_type T)
1410 in iter 0 const_T end
1411 fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1412 if app_op_level = Sufficient_Apply andalso
1413 (can dest_funT T orelse T = @{typ bool}) then
1415 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1416 fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
1417 {pred_sym = pred_sym andalso not bool_vars',
1418 min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
1419 max_ary = max_ary, types = types, in_conj = in_conj}
1421 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1423 if bool_vars' = bool_vars andalso
1424 pointer_eq (fun_var_Ts', fun_var_Ts) then
1427 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
1431 fun add_iterm_syms conj_fact top_level tm
1432 (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1433 let val (head, args) = strip_iterm_comb tm in
1435 IConst ((s, _), T, _) =>
1436 if String.isPrefix bound_var_prefix s orelse
1437 String.isPrefix all_bound_var_prefix s then
1438 add_universal_var T accum
1439 else if String.isPrefix exist_bound_var_prefix s then
1442 let val ary = length args in
1443 ((bool_vars, fun_var_Ts),
1444 case Symtab.lookup sym_tab s of
1445 SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
1448 pred_sym andalso top_level andalso not bool_vars
1449 val types' = types |> insert_type ctxt I T
1450 val in_conj = in_conj orelse conj_fact
1452 if app_op_level = Sufficient_Apply andalso
1453 not (pointer_eq (types', types)) then
1454 fold (consider_var_ary T) fun_var_Ts min_ary
1458 Symtab.update (s, {pred_sym = pred_sym,
1459 min_ary = Int.min (ary, min_ary),
1460 max_ary = Int.max (ary, max_ary),
1461 types = types', in_conj = in_conj})
1466 val pred_sym = top_level andalso not bool_vars
1468 case app_op_level of
1469 Incomplete_Apply => ary
1470 | Sufficient_Apply =>
1471 fold (consider_var_ary T) fun_var_Ts ary
1474 Symtab.update_new (s,
1475 {pred_sym = pred_sym, min_ary = min_ary,
1476 max_ary = ary, types = [T], in_conj = conj_fact})
1480 | IVar (_, T) => add_universal_var T accum
1481 | IAbs ((_, T), tm) =>
1482 accum |> add_universal_var T |> add_iterm_syms conj_fact false tm
1484 |> fold (add_iterm_syms conj_fact false) args
1486 fun add_fact_syms conj_fact =
1487 K (add_iterm_syms conj_fact true) |> formula_fold NONE |> fact_lift
1489 ((false, []), Symtab.empty)
1490 |> fold (add_fact_syms true) conjs
1491 |> fold (add_fact_syms false) facts
1493 |> fold Symtab.update (default_sym_tab_entries type_enc)
1496 fun min_ary_of sym_tab s =
1497 case Symtab.lookup sym_tab s of
1498 SOME ({min_ary, ...} : sym_info) => min_ary
1500 case unprefix_and_unascii const_prefix s of
1502 let val s = s |> unmangled_const_name |> hd |> invert_const in
1503 if s = predicator_name then 1
1504 else if s = app_op_name then 2
1505 else if s = type_guard_name then 1
1510 (* True if the constant ever appears outside of the top-level position in
1511 literals, or if it appears with different arities (e.g., because of different
1512 type instantiations). If false, the constant always receives all of its
1513 arguments and is used as a predicate. *)
1514 fun is_pred_sym sym_tab s =
1515 case Symtab.lookup sym_tab s of
1516 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1517 pred_sym andalso min_ary = max_ary
1520 val app_op = `(make_fixed_const NONE) app_op_name
1521 val predicator_combconst =
1522 IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
1524 fun list_app head args = fold (curry (IApp o swap)) args head
1525 fun predicator tm = IApp (predicator_combconst, tm)
1527 fun mk_app_op format type_enc head arg =
1529 val head_T = ityp_of head
1530 val (arg_T, res_T) = dest_funT head_T
1532 IConst (app_op, head_T --> head_T, [arg_T, res_T])
1533 |> mangle_type_args_in_iterm format type_enc
1534 in list_app app [head, arg] end
1536 fun firstorderize_fact thy monom_constrs format type_enc sym_tab
1539 fun do_app arg head = mk_app_op format type_enc head arg
1540 fun list_app_ops head args = fold do_app args head
1541 fun introduce_app_ops tm =
1542 let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
1544 IConst (name as (s, _), T, T_args) =>
1545 if uncurried_aliases andalso String.isPrefix const_prefix s then
1547 val ary = length args
1548 val name = name |> ary > min_ary_of sym_tab s
1549 ? aliased_uncurried ary
1550 in list_app (IConst (name, T, T_args)) args end
1552 args |> chop (min_ary_of sym_tab s)
1553 |>> list_app head |-> list_app_ops
1554 | _ => list_app_ops head args
1556 fun introduce_predicators tm =
1557 case strip_iterm_comb tm of
1558 (IConst ((s, _), _, _), _) =>
1559 if is_pred_sym sym_tab s then tm else predicator tm
1560 | _ => predicator tm
1562 not (is_type_enc_higher_order type_enc)
1563 ? (introduce_app_ops #> introduce_predicators)
1564 #> filter_type_args_in_iterm thy monom_constrs type_enc
1565 in update_iformula (formula_map do_iterm) end
1567 (** Helper facts **)
1569 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
1570 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
1572 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1574 [(("COMBI", false), @{thms Meson.COMBI_def}),
1575 (("COMBK", false), @{thms Meson.COMBK_def}),
1576 (("COMBB", false), @{thms Meson.COMBB_def}),
1577 (("COMBC", false), @{thms Meson.COMBC_def}),
1578 (("COMBS", false), @{thms Meson.COMBS_def}),
1579 ((predicator_name, false), [not_ffalse, ftrue]),
1580 (("fFalse", false), [not_ffalse]),
1581 (("fFalse", true), @{thms True_or_False}),
1582 (("fTrue", false), [ftrue]),
1583 (("fTrue", true), @{thms True_or_False}),
1585 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1586 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1588 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1589 by (unfold fconj_def) fast+}),
1591 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1592 by (unfold fdisj_def) fast+}),
1593 (("fimplies", false),
1594 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1595 by (unfold fimplies_def) fast+}),
1597 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1598 However, this is done so for backward compatibility: Including the
1599 equality helpers by default in Metis breaks a few existing proofs. *)
1600 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1601 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1602 (* Partial characterization of "fAll" and "fEx". A complete characterization
1603 would require the axiom of choice for replay with Metis. *)
1604 (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
1605 (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
1606 (("If", true), @{thms if_True if_False True_or_False})]
1607 |> map (apsnd (map zero_var_indexes))
1609 fun atype_of_type_vars (Simple_Types (_, Polymorphic, _)) = SOME atype_of_types
1610 | atype_of_type_vars _ = NONE
1612 fun bound_tvars type_enc sorts Ts =
1613 (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
1614 #> mk_aquant AForall
1615 (map_filter (fn TVar (x as (s, _), _) =>
1616 SOME ((make_schematic_type_var x, s),
1617 atype_of_type_vars type_enc)
1620 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
1621 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1622 else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
1623 |> mk_aquant AForall bounds
1624 |> close_formula_universally
1625 |> bound_tvars type_enc true atomic_Ts
1627 val helper_rank = default_rank
1628 val min_rank = 9 * helper_rank div 10
1629 val max_rank = 4 * min_rank
1631 fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n
1633 val type_tag = `(make_fixed_const NONE) type_tag_name
1635 fun type_tag_idempotence_fact format type_enc =
1637 fun var s = ATerm (`I s, [])
1638 fun tag tm = ATerm (type_tag, [var "A", tm])
1639 val tagged_var = tag (var "X")
1641 Formula (type_tag_idempotence_helper_name, Axiom,
1642 eq_formula type_enc [] [] false (tag tagged_var) tagged_var,
1643 NONE, isabelle_info format spec_eqN helper_rank)
1646 fun should_specialize_helper type_enc t =
1647 polymorphism_of_type_enc type_enc <> Polymorphic andalso
1648 level_of_type_enc type_enc <> No_Types andalso
1649 not (null (Term.hidden_polymorphism t))
1651 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1652 case unprefix_and_unascii const_prefix s of
1655 val thy = Proof_Context.theory_of ctxt
1656 val unmangled_s = mangled_s |> unmangled_const_name |> hd
1657 fun dub needs_fairly_sound j k =
1658 unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1659 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1660 (if needs_fairly_sound then typed_helper_suffix
1661 else untyped_helper_suffix)
1662 fun dub_and_inst needs_fairly_sound (th, j) =
1663 let val t = prop_of th in
1664 if should_specialize_helper type_enc t then
1665 map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
1671 |> map (fn (k, t) =>
1672 ((dub needs_fairly_sound j k, (Global, Spec_Eq)), t))
1673 val make_facts = map_filter (make_fact ctxt format type_enc false)
1674 val fairly_sound = is_type_enc_fairly_sound type_enc
1677 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1678 if helper_s <> unmangled_s orelse
1679 (needs_fairly_sound andalso not fairly_sound) then
1682 ths ~~ (1 upto length ths)
1683 |> maps (dub_and_inst needs_fairly_sound)
1687 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1688 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1691 (***************************************************************)
1692 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1693 (***************************************************************)
1695 fun set_insert (x, s) = Symtab.update (x, ()) s
1697 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1699 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1700 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1702 fun classes_of_terms get_Ts =
1703 map (map snd o get_Ts)
1704 #> List.foldl add_classes Symtab.empty
1705 #> delete_type #> Symtab.keys
1707 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
1708 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
1710 fun fold_type_constrs f (Type (s, Ts)) x =
1711 fold (fold_type_constrs f) Ts (f (s, x))
1712 | fold_type_constrs _ _ x = x
1714 (* Type constructors used to instantiate overloaded constants are the only ones
1716 fun add_type_constrs_in_term thy =
1718 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1719 | add (t $ u) = add t #> add u
1721 x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
1722 | add (Abs (_, _, u)) = add u
1726 fun type_constrs_of_terms thy ts =
1727 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1729 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
1730 let val (head, args) = strip_comb t in
1731 (head |> dest_Const |> fst,
1732 fold_rev (fn t as Var ((s, _), T) =>
1733 (fn u => Abs (s, T, abstract_over (t, u)))
1734 | _ => raise Fail "expected Var") args u)
1736 | extract_lambda_def _ = raise Fail "malformed lifted lambda"
1738 fun trans_lams_from_string ctxt type_enc lam_trans =
1739 if lam_trans = no_lamsN then
1741 else if lam_trans = hide_lamsN then
1742 lift_lams ctxt type_enc ##> K []
1743 else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
1744 lift_lams ctxt type_enc
1745 else if lam_trans = combsN then
1746 map (introduce_combinators ctxt) #> rpair []
1747 else if lam_trans = combs_and_liftingN then
1748 lift_lams_part_1 ctxt type_enc
1749 ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
1751 else if lam_trans = combs_or_liftingN then
1752 lift_lams_part_1 ctxt type_enc
1753 ##> map (fn t => case head_of (strip_qnt_body @{const_name All} t) of
1754 @{term "op =::bool => bool => bool"} => t
1755 | _ => introduce_combinators ctxt (intentionalize_def t))
1757 else if lam_trans = keep_lamsN then
1758 map (Envir.eta_contract) #> rpair []
1760 error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
1762 fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
1765 val thy = Proof_Context.theory_of ctxt
1766 val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
1767 val fact_ts = facts |> map snd
1768 (* Remove existing facts from the conjecture, as this can dramatically
1769 boost an ATP's performance (for some reason). *)
1772 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1773 val facts = facts |> map (apsnd (pair Axiom))
1775 map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
1776 |> map (apsnd freeze_term)
1777 |> map2 (pair o rpair (Local, General) o string_of_int)
1778 (0 upto length hyp_ts)
1779 val ((conjs, facts), lam_facts) =
1781 |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
1782 |> (if lam_trans = no_lamsN then
1786 #> preprocess_abstractions_in_terms trans_lams
1787 #>> chop (length conjs))
1788 val conjs = conjs |> make_conjecture ctxt format type_enc
1789 val (fact_names, facts) =
1791 |> map_filter (fn (name, (_, t)) =>
1792 make_fact ctxt format type_enc true (name, t)
1793 |> Option.map (pair name))
1795 val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
1797 lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
1798 val all_ts = concl_t :: hyp_ts @ fact_ts
1799 val subs = tfree_classes_of_terms all_ts
1800 val supers = tvar_classes_of_terms all_ts
1801 val tycons = type_constrs_of_terms thy all_ts
1802 val (supers, arity_clauses) =
1803 if level_of_type_enc type_enc = No_Types then ([], [])
1804 else make_arity_clauses thy tycons supers
1805 val class_rel_clauses = make_class_rel_clauses thy subs supers
1807 (fact_names |> map single, union (op =) subs supers, conjs,
1808 facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
1811 val type_guard = `(make_fixed_const NONE) type_guard_name
1813 fun type_guard_iterm format type_enc T tm =
1814 IApp (IConst (type_guard, T --> @{typ bool}, [T])
1815 |> mangle_type_args_in_iterm format type_enc, tm)
1817 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1818 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1819 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1820 | is_var_positively_naked_in_term _ _ _ _ = true
1822 fun is_var_ghost_type_arg_in_term thy polym_constrs name pos tm accum =
1823 is_var_positively_naked_in_term name pos tm accum orelse
1825 val var = ATerm (name, [])
1826 fun is_nasty_in_term (ATerm (_, [])) = false
1827 | is_nasty_in_term (ATerm ((s, _), tms)) =
1829 val ary = length tms
1830 val polym_constr = member (op =) polym_constrs s
1831 val ghosts = ghost_type_args thy s ary
1833 exists (fn (j, tm) =>
1834 if polym_constr then
1835 member (op =) ghosts j andalso
1836 (tm = var orelse is_nasty_in_term tm)
1838 tm = var andalso member (op =) ghosts j)
1839 (0 upto ary - 1 ~~ tms)
1840 orelse (not polym_constr andalso exists is_nasty_in_term tms)
1842 | is_nasty_in_term _ = true
1843 in is_nasty_in_term tm end
1845 fun should_guard_var_in_formula thy polym_constrs level pos phi (SOME true)
1847 (case granularity_of_type_level level of
1849 | Positively_Naked_Vars =>
1850 formula_fold pos (is_var_positively_naked_in_term name) phi false
1851 | Ghost_Type_Arg_Vars =>
1852 formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name)
1854 | should_guard_var_in_formula _ _ _ _ _ _ _ = true
1856 fun always_guard_var_in_formula _ _ _ _ _ _ _ = true
1858 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
1859 | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
1860 granularity_of_type_level level <> All_Vars andalso
1861 should_encode_type ctxt mono level T
1862 | should_generate_tag_bound_decl _ _ _ _ _ = false
1864 fun mk_aterm format type_enc name T_args args =
1865 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1867 fun do_bound_type ctxt format mono type_enc =
1869 Simple_Types (_, _, level) =>
1870 fused_type ctxt mono level 0
1871 #> ho_type_from_typ format type_enc false 0 #> SOME
1874 fun tag_with_type ctxt format mono type_enc pos T tm =
1875 IConst (type_tag, T --> T, [T])
1876 |> mangle_type_args_in_iterm format type_enc
1877 |> ho_term_from_iterm ctxt format mono type_enc pos
1878 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1879 | _ => raise Fail "unexpected lambda-abstraction")
1880 and ho_term_from_iterm ctxt format mono type_enc =
1884 val (head, args) = strip_iterm_comb u
1887 Top_Level pos => pos
1892 IConst (name as (s, _), _, T_args) =>
1894 val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1896 map (term arg_site) args |> mk_aterm format type_enc name T_args
1899 map (term Elsewhere) args |> mk_aterm format type_enc name []
1900 | IAbs ((name, T), tm) =>
1901 AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1903 | IApp _ => raise Fail "impossible \"IApp\""
1906 if should_tag_with_type ctxt mono type_enc site u T then
1907 tag_with_type ctxt format mono type_enc pos T t
1911 in term o Top_Level end
1912 and formula_from_iformula ctxt polym_constrs format mono type_enc
1915 val thy = Proof_Context.theory_of ctxt
1916 val level = level_of_type_enc type_enc
1917 val do_term = ho_term_from_iterm ctxt format mono type_enc
1918 fun do_out_of_bound_type pos phi universal (name, T) =
1919 if should_guard_type ctxt mono type_enc
1920 (fn () => should_guard_var thy polym_constrs level pos phi
1921 universal name) T then
1923 |> type_guard_iterm format type_enc T
1924 |> do_term pos |> AAtom |> SOME
1925 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
1927 val var = ATerm (name, [])
1928 val tagged_var = tag_with_type ctxt format mono type_enc pos T var
1929 in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
1932 fun do_formula pos (AQuant (q, xs, phi)) =
1934 val phi = phi |> do_formula pos
1935 val universal = Option.map (q = AExists ? not) pos
1936 val do_bound_type = do_bound_type ctxt format mono type_enc
1938 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1939 | SOME T => do_bound_type T)),
1940 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1942 (fn (_, NONE) => NONE
1944 do_out_of_bound_type pos phi universal (s, T))
1948 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1949 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1952 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1953 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1954 the remote provers might care. *)
1955 fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
1956 mono type_enc rank (j, {name, stature, kind, iformula, atomic_types}) =
1957 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
1959 |> formula_from_iformula ctxt polym_constrs format mono type_enc
1960 should_guard_var_in_formula (if pos then SOME true else NONE)
1961 |> close_formula_universally
1962 |> bound_tvars type_enc true atomic_types,
1964 let val rank = rank j in
1966 Intro => isabelle_info format introN rank
1967 | Elim => isabelle_info format elimN rank
1968 | Simp => isabelle_info format simpN rank
1969 | Spec_Eq => isabelle_info format spec_eqN rank
1970 | _ => isabelle_info format "" rank
1974 fun formula_line_for_class_rel_clause format type_enc
1975 ({name, subclass, superclass, ...} : class_rel_clause) =
1976 let val ty_arg = ATerm (tvar_a_name, []) in
1977 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1979 [type_class_formula type_enc subclass ty_arg,
1980 type_class_formula type_enc superclass ty_arg])
1981 |> mk_aquant AForall
1982 [(tvar_a_name, atype_of_type_vars type_enc)],
1983 NONE, isabelle_info format introN helper_rank)
1986 fun formula_from_arity_atom type_enc (class, t, args) =
1987 ATerm (t, map (fn arg => ATerm (arg, [])) args)
1988 |> type_class_formula type_enc class
1990 fun formula_line_for_arity_clause format type_enc
1991 ({name, prem_atoms, concl_atom} : arity_clause) =
1992 Formula (arity_clause_prefix ^ name, Axiom,
1993 mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
1994 (formula_from_arity_atom type_enc concl_atom)
1995 |> mk_aquant AForall
1996 (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
1997 NONE, isabelle_info format introN helper_rank)
1999 fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
2000 ({name, kind, iformula, atomic_types, ...} : translated_formula) =
2001 Formula (conjecture_prefix ^ name, kind,
2003 |> formula_from_iformula ctxt polym_constrs format mono type_enc
2004 should_guard_var_in_formula (SOME false)
2005 |> close_formula_universally
2006 |> bound_tvars type_enc true atomic_types, NONE, [])
2008 fun formula_line_for_free_type j phi =
2009 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
2010 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
2013 fold (union (op =)) (map #atomic_types facts) []
2014 |> formulas_for_types type_enc add_sorts_on_tfree
2015 in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
2017 (** Symbol declarations **)
2019 fun decl_line_for_class order s =
2020 let val name as (s, _) = `make_type_class s in
2021 Decl (sym_decl_prefix ^ s, name,
2022 if order = First_Order then
2023 ATyAbs ([tvar_a_name],
2024 if avoid_first_order_ghost_type_vars then
2025 AFun (a_itself_atype, bool_atype)
2029 AFun (atype_of_types, bool_atype))
2032 fun decl_lines_for_classes type_enc classes =
2034 Simple_Types (order, Polymorphic, _) =>
2035 map (decl_line_for_class order) classes
2038 fun sym_decl_table_for_facts ctxt format type_enc sym_tab
2039 (conjs, facts, extra_tms) =
2041 fun add_iterm_syms tm =
2042 let val (head, args) = strip_iterm_comb tm in
2044 IConst ((s, s'), T, T_args) =>
2046 val (pred_sym, in_conj) =
2047 case Symtab.lookup sym_tab s of
2048 SOME ({pred_sym, in_conj, ...} : sym_info) =>
2050 | NONE => (false, false)
2053 Guards _ => not pred_sym
2054 | _ => true) andalso
2055 is_tptp_user_symbol s
2058 Symtab.map_default (s, [])
2059 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
2064 | IAbs (_, tm) => add_iterm_syms tm
2066 #> fold add_iterm_syms args
2068 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
2069 fun add_formula_var_types (AQuant (_, xs, phi)) =
2070 fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
2071 #> add_formula_var_types phi
2072 | add_formula_var_types (AConn (_, phis)) =
2073 fold add_formula_var_types phis
2074 | add_formula_var_types _ = I
2076 if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
2077 else fold (fact_lift add_formula_var_types) (conjs @ facts) []
2078 fun add_undefined_const T =
2081 `(make_fixed_const NONE) @{const_name undefined}
2082 |> (case type_arg_policy [] type_enc @{const_name undefined} of
2083 Mangled_Type_Args => mangled_const_name format type_enc [T]
2086 Symtab.map_default (s, [])
2087 (insert_type ctxt #3 (s', [T], T, false, 0, false))
2089 fun add_TYPE_const () =
2090 let val (s, s') = TYPE_name in
2091 Symtab.map_default (s, [])
2092 (insert_type ctxt #3
2093 (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
2097 |> is_type_enc_fairly_sound type_enc
2098 ? (fold (fold add_fact_syms) [conjs, facts]
2099 #> fold add_iterm_syms extra_tms
2100 #> (case type_enc of
2101 Simple_Types (First_Order, Polymorphic, _) =>
2102 if avoid_first_order_ghost_type_vars then add_TYPE_const ()
2104 | Simple_Types _ => I
2105 | _ => fold add_undefined_const (var_types ())))
2108 (* We add "bool" in case the helper "True_or_False" is included later. *)
2109 fun default_mono level =
2110 {maybe_finite_Ts = [@{typ bool}],
2111 surely_finite_Ts = [@{typ bool}],
2112 maybe_infinite_Ts = known_infinite_types,
2113 surely_infinite_Ts =
2115 Noninf_Nonmono_Types (Strict, _) => []
2116 | _ => known_infinite_types,
2117 maybe_nonmono_Ts = [@{typ bool}]}
2119 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
2120 out with monotonicity" paper presented at CADE 2011. *)
2121 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
2122 | add_iterm_mononotonicity_info ctxt level _
2123 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
2124 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
2125 surely_infinite_Ts, maybe_nonmono_Ts}) =
2126 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
2128 Noninf_Nonmono_Types (strictness, _) =>
2129 if exists (type_instance ctxt T) surely_infinite_Ts orelse
2130 member (type_equiv ctxt) maybe_finite_Ts T then
2132 else if is_type_kind_of_surely_infinite ctxt strictness
2133 surely_infinite_Ts T then
2134 {maybe_finite_Ts = maybe_finite_Ts,
2135 surely_finite_Ts = surely_finite_Ts,
2136 maybe_infinite_Ts = maybe_infinite_Ts,
2137 surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
2138 maybe_nonmono_Ts = maybe_nonmono_Ts}
2140 {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
2141 surely_finite_Ts = surely_finite_Ts,
2142 maybe_infinite_Ts = maybe_infinite_Ts,
2143 surely_infinite_Ts = surely_infinite_Ts,
2144 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2145 | Fin_Nonmono_Types _ =>
2146 if exists (type_instance ctxt T) surely_finite_Ts orelse
2147 member (type_equiv ctxt) maybe_infinite_Ts T then
2149 else if is_type_surely_finite ctxt T then
2150 {maybe_finite_Ts = maybe_finite_Ts,
2151 surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
2152 maybe_infinite_Ts = maybe_infinite_Ts,
2153 surely_infinite_Ts = surely_infinite_Ts,
2154 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2156 {maybe_finite_Ts = maybe_finite_Ts,
2157 surely_finite_Ts = surely_finite_Ts,
2158 maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
2159 surely_infinite_Ts = surely_infinite_Ts,
2160 maybe_nonmono_Ts = maybe_nonmono_Ts}
2164 | add_iterm_mononotonicity_info _ _ _ _ mono = mono
2165 fun add_fact_mononotonicity_info ctxt level
2166 ({kind, iformula, ...} : translated_formula) =
2167 formula_fold (SOME (kind <> Conjecture))
2168 (add_iterm_mononotonicity_info ctxt level) iformula
2169 fun mononotonicity_info_for_facts ctxt type_enc facts =
2170 let val level = level_of_type_enc type_enc in
2172 |> is_type_level_monotonicity_based level
2173 ? fold (add_fact_mononotonicity_info ctxt level) facts
2176 fun add_iformula_monotonic_types ctxt mono type_enc =
2178 val level = level_of_type_enc type_enc
2179 val should_encode = should_encode_type ctxt mono level
2180 fun add_type T = not (should_encode T) ? insert_type ctxt I T
2181 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
2183 and add_term tm = add_type (ityp_of tm) #> add_args tm
2184 in formula_fold NONE (K add_term) end
2185 fun add_fact_monotonic_types ctxt mono type_enc =
2186 add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
2187 fun monotonic_types_for_facts ctxt mono type_enc facts =
2188 let val level = level_of_type_enc type_enc in
2189 [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
2190 is_type_level_monotonicity_based level andalso
2191 granularity_of_type_level level <> Ghost_Type_Arg_Vars)
2192 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
2195 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
2196 Formula (guards_sym_formula_prefix ^
2197 ascii_of (mangled_type format type_enc T),
2199 IConst (`make_bound_var "X", T, [])
2200 |> type_guard_iterm format type_enc T
2202 |> formula_from_iformula ctxt [] format mono type_enc
2203 always_guard_var_in_formula (SOME true)
2204 |> close_formula_universally
2205 |> bound_tvars type_enc true (atomic_types_of T),
2206 NONE, isabelle_info format introN helper_rank)
2208 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
2209 let val x_var = ATerm (`make_bound_var "X", []) in
2210 Formula (tags_sym_formula_prefix ^
2211 ascii_of (mangled_type format type_enc T),
2213 eq_formula type_enc (atomic_types_of T) [] false
2214 (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
2215 NONE, isabelle_info format spec_eqN helper_rank)
2218 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
2220 Simple_Types _ => []
2222 map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
2223 | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
2225 fun decl_line_for_sym ctxt format mono type_enc s
2226 (s', T_args, T, pred_sym, ary, _) =
2228 val thy = Proof_Context.theory_of ctxt
2232 else case unprefix_and_unascii const_prefix s of
2235 val s' = s' |> invert_const
2236 val T = s' |> robust_const_type thy
2237 in (T, robust_const_typargs thy (s', T)) end
2238 | NONE => raise Fail "unexpected type arguments"
2240 Decl (sym_decl_prefix ^ s, (s, s'),
2241 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
2242 |> ho_type_from_typ format type_enc pred_sym ary
2243 |> not (null T_args)
2244 ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
2247 fun honor_conj_sym_kind in_conj conj_sym_kind =
2248 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
2251 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
2252 j (s', T_args, T, _, ary, in_conj) =
2254 val thy = Proof_Context.theory_of ctxt
2255 val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
2256 val (arg_Ts, res_T) = chop_fun ary T
2257 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2259 bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
2261 if exists (curry (op =) dummyT) T_args then
2262 case level_of_type_enc type_enc of
2263 All_Types => map SOME arg_Ts
2265 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
2266 let val ghosts = ghost_type_args thy s ary in
2267 map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
2268 (0 upto ary - 1) arg_Ts
2275 Formula (guards_sym_formula_prefix ^ s ^
2276 (if n > 1 then "_" ^ string_of_int j else ""), kind,
2277 IConst ((s, s'), T, T_args)
2278 |> fold (curry (IApp o swap)) bounds
2279 |> type_guard_iterm format type_enc res_T
2280 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
2281 |> formula_from_iformula ctxt [] format mono type_enc
2282 always_guard_var_in_formula (SOME true)
2283 |> close_formula_universally
2284 |> bound_tvars type_enc (n > 1) (atomic_types_of T)
2286 NONE, isabelle_info format introN helper_rank)
2289 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
2290 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
2292 val thy = Proof_Context.theory_of ctxt
2293 val level = level_of_type_enc type_enc
2294 val grain = granularity_of_type_level level
2296 tags_sym_formula_prefix ^ s ^
2297 (if n > 1 then "_" ^ string_of_int j else "")
2298 val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
2299 val (arg_Ts, res_T) = chop_fun ary T
2300 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2301 val bounds = bound_names |> map (fn name => ATerm (name, []))
2302 val cst = mk_aterm format type_enc (s, s') T_args
2303 val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
2304 val should_encode = should_encode_type ctxt mono level
2305 val tag_with = tag_with_type ctxt format mono type_enc NONE
2306 val add_formula_for_res =
2307 if should_encode res_T then
2310 if grain = Ghost_Type_Arg_Vars then
2311 let val ghosts = ghost_type_args thy s ary in
2312 map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
2313 (0 upto ary - 1 ~~ arg_Ts) bounds
2318 cons (Formula (ident_base ^ "_res", kind,
2319 eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
2320 NONE, isabelle_info format spec_eqN helper_rank))
2324 fun add_formula_for_arg k =
2325 let val arg_T = nth arg_Ts k in
2326 if should_encode arg_T then
2327 case chop k bounds of
2328 (bounds1, bound :: bounds2) =>
2329 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
2330 eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
2332 NONE, isabelle_info format spec_eqN helper_rank))
2333 | _ => raise Fail "expected nonempty tail"
2338 [] |> not pred_sym ? add_formula_for_res
2339 |> (Config.get ctxt type_tag_arguments andalso
2340 grain = Positively_Naked_Vars)
2341 ? fold add_formula_for_arg (ary - 1 downto 0)
2344 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
2346 fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
2348 val T = result_type_of_decl decl
2349 |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
2351 if forall (type_generalization ctxt T o result_type_of_decl) decls' then
2356 | rationalize_decls _ decls = decls
2358 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
2361 Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
2362 | Guards (_, level) =>
2364 val decls = decls |> rationalize_decls ctxt
2365 val n = length decls
2367 decls |> filter (should_encode_type ctxt mono level
2368 o result_type_of_decl)
2370 (0 upto length decls - 1, decls)
2371 |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
2374 | Tags (_, level) =>
2375 if granularity_of_type_level level = All_Vars then
2378 let val n = length decls in
2379 (0 upto n - 1 ~~ decls)
2380 |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono
2384 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
2385 mono_Ts sym_decl_tab =
2387 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
2389 problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
2391 fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
2394 in mono_lines @ decl_lines end
2396 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
2398 fun do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
2399 mono type_enc sym_tab0 sym_tab base_s0 types in_conj =
2403 val thy = Proof_Context.theory_of ctxt
2404 val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
2405 val base_name = base_s0 |> `(make_fixed_const (SOME format))
2406 val T = case types of [T] => T | _ => robust_const_type thy base_s0
2407 val T_args = robust_const_typargs thy (base_s0, T)
2408 val (base_name as (base_s, _), T_args) =
2409 mangle_type_args_in_const format type_enc base_name T_args
2410 val base_ary = min_ary_of sym_tab0 base_s
2411 fun do_const name = IConst (name, T, T_args)
2412 val filter_ty_args =
2413 filter_type_args_in_iterm thy monom_constrs type_enc
2415 ho_term_from_iterm ctxt format mono type_enc (SOME true)
2416 val name1 as (s1, _) =
2417 base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
2418 val name2 as (s2, _) = base_name |> aliased_uncurried ary
2419 val (arg_Ts, _) = chop_fun ary T
2421 1 upto ary |> map (`I o make_bound_var o string_of_int)
2422 val bounds = bound_names ~~ arg_Ts
2423 val (first_bounds, last_bound) =
2424 bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last
2426 mk_app_op format type_enc (list_app (do_const name1) first_bounds)
2430 list_app (do_const name2) (first_bounds @ [last_bound])
2432 val do_bound_type = do_bound_type ctxt format mono type_enc
2434 eq_formula type_enc (atomic_types_of T)
2435 (map (apsnd do_bound_type) bounds) false
2436 (ho_term_of tm1) (ho_term_of tm2)
2439 [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
2440 NONE, isabelle_info format spec_eqN helper_rank)])
2441 |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
2442 else pair_append (do_alias (ary - 1)))
2445 fun uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
2446 type_enc sym_tab0 sym_tab
2447 (s, {min_ary, types, in_conj, ...} : sym_info) =
2448 case unprefix_and_unascii const_prefix s of
2450 if String.isSubstring uncurried_alias_sep mangled_s then
2452 val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
2454 do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
2455 mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary
2460 fun uncurried_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
2461 mono type_enc uncurried_aliases sym_tab0 sym_tab =
2463 |> uncurried_aliases
2466 o uncurried_alias_lines_for_sym ctxt monom_constrs format
2467 conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab
2469 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
2470 Config.get ctxt type_tag_idempotence andalso
2471 is_type_level_monotonicity_based level andalso
2472 poly <> Mangled_Monomorphic
2473 | needs_type_tag_idempotence _ _ = false
2475 val implicit_declsN = "Should-be-implicit typings"
2476 val explicit_declsN = "Explicit typings"
2477 val uncurried_alias_eqsN = "Uncurried aliases"
2478 val factsN = "Relevant facts"
2479 val class_relsN = "Class relationships"
2480 val aritiesN = "Arities"
2481 val helpersN = "Helper facts"
2482 val conjsN = "Conjectures"
2483 val free_typesN = "Type variables"
2485 (* TFF allows implicit declarations of types, function symbols, and predicate
2486 symbols (with "$i" as the type of individuals), but some provers (e.g.,
2487 SNARK) require explicit declarations. The situation is similar for THF. *)
2489 fun default_type type_enc pred_sym s =
2494 if String.isPrefix type_const_prefix s then atype_of_types
2495 else individual_atype
2496 | _ => individual_atype
2497 fun typ 0 = if pred_sym then bool_atype else ind
2498 | typ ary = AFun (ind, typ (ary - 1))
2501 fun nary_type_constr_type n =
2502 funpow n (curry AFun atype_of_types) atype_of_types
2504 fun undeclared_syms_in_problem type_enc problem =
2506 val declared = declared_syms_in_problem problem
2507 fun do_sym (name as (s, _)) ty =
2508 if is_tptp_user_symbol s andalso not (member (op =) declared name) then
2509 AList.default (op =) (name, ty)
2512 fun do_type (AType (name, tys)) =
2513 do_sym name (fn () => nary_type_constr_type (length tys))
2515 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
2516 | do_type (ATyAbs (_, ty)) = do_type ty
2517 fun do_term pred_sym (ATerm (name as (s, _), tms)) =
2518 do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
2519 #> fold (do_term false) tms
2520 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
2521 fun do_formula (AQuant (_, xs, phi)) =
2522 fold do_type (map_filter snd xs) #> do_formula phi
2523 | do_formula (AConn (_, phis)) = fold do_formula phis
2524 | do_formula (AAtom tm) = do_term true tm
2525 fun do_problem_line (Decl (_, _, ty)) = do_type ty
2526 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
2528 fold (fold do_problem_line o snd) problem []
2529 |> filter_out (is_built_in_tptp_symbol o fst o fst)
2532 fun declare_undeclared_syms_in_atp_problem type_enc problem =
2536 |> undeclared_syms_in_problem type_enc
2537 |> sort_wrt (fst o fst)
2538 |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
2539 in (implicit_declsN, decls) :: problem end
2541 fun exists_subdtype P =
2543 fun ex U = P U orelse
2544 (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false)
2547 fun is_poly_constr (_, Us) =
2548 exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
2550 fun all_constrs_of_polymorphic_datatypes thy =
2554 #> (fn cs => exists is_poly_constr cs ? append cs))
2555 (Datatype.get_all thy) []
2556 |> List.partition is_poly_constr
2557 |> pairself (map fst)
2559 val app_op_threshold = 50
2561 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
2562 lam_trans uncurried_aliases readable_names preproc
2563 hyp_ts concl_t facts =
2565 val thy = Proof_Context.theory_of ctxt
2566 val type_enc = type_enc |> adjust_type_enc format
2567 (* Forcing explicit applications is expensive for polymorphic encodings,
2568 because it takes only one existential variable ranging over "'a => 'b" to
2569 ruin everything. Hence we do it only if there are few facts (which is
2570 normally the case for "metis" and the minimizer). *)
2572 if polymorphism_of_type_enc type_enc = Polymorphic andalso
2573 length facts >= app_op_threshold then
2578 if lam_trans = keep_lamsN andalso
2579 not (is_type_enc_higher_order type_enc) then
2580 error ("Lambda translation scheme incompatible with first-order \
2584 val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
2586 translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
2588 val sym_tab0 = sym_table_for_facts ctxt type_enc app_op_level conjs facts
2589 val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
2590 val (polym_constrs, monom_constrs) =
2591 all_constrs_of_polymorphic_datatypes thy
2592 |>> map (make_fixed_const (SOME format))
2593 fun firstorderize in_helper =
2594 firstorderize_fact thy monom_constrs format type_enc sym_tab0
2595 (uncurried_aliases andalso not in_helper)
2596 val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
2597 val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
2599 sym_tab |> helper_facts_for_sym_table ctxt format type_enc
2600 |> map (firstorderize true)
2602 helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
2603 val class_decl_lines = decl_lines_for_classes type_enc classes
2604 val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
2605 uncurried_alias_lines_for_sym_table ctxt monom_constrs format
2606 conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
2607 val sym_decl_lines =
2608 (conjs, helpers @ facts, uncurried_alias_eq_tms)
2609 |> sym_decl_table_for_facts ctxt format type_enc sym_tab
2610 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
2612 val num_facts = length facts
2614 map (formula_line_for_fact ctxt polym_constrs format fact_prefix
2615 ascii_of (not exporter) (not exporter) mono type_enc
2616 (rank_of_fact_num num_facts))
2617 (0 upto num_facts - 1 ~~ facts)
2619 0 upto length helpers - 1 ~~ helpers
2620 |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I
2621 false true mono type_enc (K default_rank))
2622 |> (if needs_type_tag_idempotence ctxt type_enc then
2623 cons (type_tag_idempotence_fact format type_enc)
2626 (* Reordering these might confuse the proof reconstruction code or the SPASS
2629 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
2630 (uncurried_alias_eqsN, uncurried_alias_eq_lines),
2631 (factsN, fact_lines),
2633 map (formula_line_for_class_rel_clause format type_enc)
2636 map (formula_line_for_arity_clause format type_enc) arity_clauses),
2637 (helpersN, helper_lines),
2639 map (formula_line_for_conjecture ctxt polym_constrs format mono
2641 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
2645 CNF => ensure_cnf_problem
2646 | CNF_UEQ => filter_cnf_ueq_problem
2648 | TFF (_, TPTP_Implicit) => I
2649 | THF (_, TPTP_Implicit, _) => I
2650 | _ => declare_undeclared_syms_in_atp_problem type_enc)
2651 val (problem, pool) = problem |> nice_atp_problem readable_names format
2652 fun add_sym_ary (s, {min_ary, ...} : sym_info) =
2653 min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
2656 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
2657 fact_names |> Vector.fromList,
2659 Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
2663 val conj_weight = 0.0
2664 val hyp_weight = 0.1
2665 val fact_min_weight = 0.2
2666 val fact_max_weight = 1.0
2667 val type_info_default_weight = 0.8
2669 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
2670 fun atp_problem_relevance_weights problem =
2672 fun add_term_weights weight (ATerm (s, tms)) =
2673 is_tptp_user_symbol s ? Symtab.default (s, weight)
2674 #> fold (add_term_weights weight) tms
2675 | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
2676 fun add_line_weights weight (Formula (_, _, phi, _, _)) =
2677 formula_fold NONE (K (add_term_weights weight)) phi
2678 | add_line_weights _ _ = I
2679 fun add_conjectures_weights [] = I
2680 | add_conjectures_weights conjs =
2681 let val (hyps, conj) = split_last conjs in
2682 add_line_weights conj_weight conj
2683 #> fold (add_line_weights hyp_weight) hyps
2685 fun add_facts_weights facts =
2687 val num_facts = length facts
2689 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
2690 / Real.fromInt num_facts
2692 map weight_of (0 upto num_facts - 1) ~~ facts
2693 |> fold (uncurry add_line_weights)
2695 val get = these o AList.lookup (op =) problem
2698 |> add_conjectures_weights (get free_typesN @ get conjsN)
2699 |> add_facts_weights (get factsN)
2700 |> fold (fold (add_line_weights type_info_default_weight) o get)
2701 [explicit_declsN, class_relsN, aritiesN]
2703 |> sort (prod_ord Real.compare string_ord o pairself swap)
2706 fun have_head_rolling (ATerm (s, args)) =
2707 (* ugly hack: may make innocent victims *)
2708 if String.isPrefix app_op_name s andalso length args = 2 then
2709 have_head_rolling (hd args) ||> append (tl args)
2712 | have_head_rolling _ = ("", [])
2714 val max_kbo_weight = 2147483647
2716 fun atp_problem_kbo_weights problem =
2718 fun add_term_deps head (ATerm (s, args)) =
2719 is_tptp_user_symbol s ? perhaps (try (Graph.add_edge_acyclic (s, head)))
2720 #> fold (add_term_deps head) args
2721 | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm
2722 fun add_eq_deps (ATerm (s, [lhs as _, rhs])) =
2723 if is_tptp_equal s then
2724 let val (head, rest) = have_head_rolling lhs in
2725 fold (add_term_deps head) (rhs :: rest)
2730 fun add_line_deps _ (Decl (_, s, ty)) =
2731 is_function_type ty ? Graph.default_node (s, ())
2732 | add_line_deps status (Formula (_, _, phi, _, info)) =
2733 if extract_isabelle_status info = SOME status then
2734 formula_fold NONE (K add_eq_deps) phi
2738 Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem
2739 |> fold (fold (add_line_deps simpN) o snd) problem
2740 fun next_weight w = if w + w <= max_kbo_weight then w + w else w + 1
2741 fun add_weights _ [] = I
2742 | add_weights weight syms =
2743 fold (AList.update (op =) o rpair weight) syms
2744 #> add_weights (next_weight weight)
2745 (fold (union (op =) o Graph.immediate_succs graph) syms [])
2747 [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o pairself snd)