--- a/src/HOL/TPTP/atp_theory_export.ML Thu Dec 13 22:49:07 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Dec 13 22:49:08 2012 +0100
@@ -34,8 +34,8 @@
fun inference infers ident =
these (AList.lookup (op =) infers ident) |> inference_term
fun add_inferences_to_problem_line infers
- (Formula (ident, Axiom, phi, NONE, tms)) =
- Formula (ident, Lemma, phi, inference infers ident, tms)
+ (Formula ((ident, alt), Axiom, phi, NONE, tms)) =
+ Formula ((ident, alt), Lemma, phi, inference infers ident, tms)
| add_inferences_to_problem_line _ line = line
fun add_inferences_to_problem infers =
map (apsnd (map (add_inferences_to_problem_line infers)))
@@ -44,7 +44,7 @@
| ident_of_problem_line (Type_Decl (ident, _, _)) = ident
| ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
| ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
- | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
+ | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
fun atp_for_format (THF (Polymorphic, _, _, _)) = dummy_thfN
| atp_for_format (THF (Monomorphic, _, _, _)) = satallaxN
@@ -83,11 +83,12 @@
[@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}]
|> map (fact_name_of o Context.theory_name)
-fun is_problem_line_tautology ctxt format (Formula (ident, _, phi, _, _)) =
+fun is_problem_line_tautology ctxt format
+ (Formula ((ident, alt), _, phi, _, _)) =
exists (fn prefix => String.isPrefix prefix ident)
tautology_prefixes andalso
is_none (run_some_atp ctxt format
- [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])])
+ [(factsN, [Formula ((ident, alt), Conjecture, phi, NONE, [])])])
| is_problem_line_tautology _ _ _ = false
fun order_facts ord = sort (ord o pairself ident_of_problem_line)
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 13 22:49:07 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 13 22:49:08 2012 +0100
@@ -51,7 +51,7 @@
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a ho_type |
Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
- Formula of string * formula_role
+ Formula of (string * string) * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
* (string, string ho_type) ho_term option
* (string, string ho_type) ho_term list
@@ -190,7 +190,7 @@
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a ho_type |
Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
- Formula of string * formula_role
+ Formula of (string * string) * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
* (string, string ho_type) ho_term option
* (string, string ho_type) ho_term list
@@ -479,15 +479,18 @@
fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types
+fun tptp_maybe_alt "" = ""
+ | tptp_maybe_alt s = " % " ^ s
+
fun tptp_string_for_line format (Type_Decl (ident, ty, ary)) =
tptp_string_for_line format (Sym_Decl (ident, ty, nary_type_decl_type ary))
| tptp_string_for_line format (Sym_Decl (ident, sym, ty)) =
tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
" : " ^ string_for_type format ty ^ ").\n"
- | tptp_string_for_line format (Formula (ident, kind, phi, source, _)) =
+ | tptp_string_for_line format (Formula ((ident, alt), kind, phi, source, _)) =
tptp_string_for_format format ^ "(" ^ ident ^ ", " ^
- tptp_string_for_role kind ^ ",\n (" ^
- tptp_string_for_formula format phi ^ ")" ^
+ tptp_string_for_role kind ^ "," ^ tptp_maybe_alt alt ^
+ "\n (" ^ tptp_string_for_formula format phi ^ ")" ^
(case source of
SOME tm => ", " ^ tptp_string_for_term format tm
| NONE => "") ^ ").\n"
@@ -582,7 +585,7 @@
else "[" ^ commas (map str_for_bound_tvar xs) ^ "], ") ^
str_for_typ ty ^ ", " ^ cl ^ ")."
fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
- fun formula pred (Formula (ident, kind, phi, _, info)) =
+ fun formula pred (Formula ((ident, _), kind, phi, _, info)) =
if pred kind then
let val rank = extract_isabelle_rank info in
"formula(" ^ dfg_string_for_formula poly gen_simp info phi ^
@@ -725,13 +728,13 @@
clausify_formula true (AConn (AImplies, rev phis))
| clausify_formula _ _ = raise CLAUSIFY ()
-fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =
+fun clausify_formula_line (Formula ((ident, alt), kind, phi, source, info)) =
let
val (n, phis) = phi |> try (clausify_formula true) |> these |> `length
in
map2 (fn phi => fn j =>
- Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source,
- info))
+ Formula ((ident ^ replicate_string (j - 1) "x", alt), kind, phi,
+ source, info))
phis (1 upto n)
end
| clausify_formula_line _ = []
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 13 22:49:07 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 13 22:49:08 2012 +0100
@@ -2128,8 +2128,8 @@
the remote provers might care. *)
fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank
(j, {name, stature = (_, status), role, iformula, atomic_types}) =
- Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
- encode name,
+ Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
+ encode name, name),
role,
iformula
|> formula_from_iformula ctxt mono type_enc
@@ -2139,7 +2139,7 @@
NONE, isabelle_info (string_of_status status) (rank j))
fun lines_for_subclass type_enc sub super =
- Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom,
+ Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
AConn (AImplies,
[sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
|> bound_tvars type_enc false [tvar_a],
@@ -2160,7 +2160,7 @@
prems,
native_ho_type_from_typ type_enc false 0 T, `make_class cl)
else
- Formula (tcon_clause_prefix ^ name, Axiom,
+ Formula ((tcon_clause_prefix ^ name, ""), Axiom,
mk_ahorn (maps (class_atoms type_enc) prems)
(class_atom type_enc (cl, T))
|> bound_tvars type_enc true (snd (dest_Type T)),
@@ -2168,7 +2168,7 @@
fun line_for_conjecture ctxt mono type_enc
({name, role, iformula, atomic_types, ...} : ifact) =
- Formula (conjecture_prefix ^ name, role,
+ Formula ((conjecture_prefix ^ name, ""), role,
iformula
|> formula_from_iformula ctxt mono type_enc
should_guard_var_in_formula (SOME false)
@@ -2186,7 +2186,7 @@
native_ho_type_from_typ type_enc false 0 T,
`make_class cl)
else
- Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
+ Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis,
class_atom type_enc (cl, T), NONE, [])
val membs =
fold (union (op =)) (map #atomic_types facts) []
@@ -2347,8 +2347,7 @@
end
fun line_for_guards_mono_type ctxt mono type_enc T =
- Formula (guards_sym_formula_prefix ^
- ascii_of (mangled_type type_enc T),
+ Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
Axiom,
IConst (`make_bound_var "X", T, [])
|> type_guard_iterm type_enc T
@@ -2361,8 +2360,7 @@
fun line_for_tags_mono_type ctxt mono type_enc T =
let val x_var = ATerm ((`make_bound_var "X", []), []) in
- Formula (tags_sym_formula_prefix ^
- ascii_of (mangled_type type_enc T),
+ Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
Axiom,
eq_formula type_enc (atomic_types_of T) [] false
(tag_with_type ctxt mono type_enc NONE T x_var) x_var,
@@ -2419,8 +2417,9 @@
end
| _ => replicate ary NONE
in
- Formula (guards_sym_formula_prefix ^ s ^
- (if n > 1 then "_" ^ string_of_int j else ""), role,
+ Formula ((guards_sym_formula_prefix ^ s ^
+ (if n > 1 then "_" ^ string_of_int j else ""), ""),
+ role,
IConst ((s, s'), T, T_args)
|> fold (curry (IApp o swap)) bounds
|> type_guard_iterm type_enc res_T
@@ -2449,8 +2448,8 @@
val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
val tag_with = tag_with_type ctxt mono type_enc NONE
fun formula c =
- [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info
- non_rec_defN helper_rank)]
+ [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE,
+ isabelle_info non_rec_defN helper_rank)]
in
if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
[]
@@ -2549,8 +2548,9 @@
(ho_term_of tm1) (ho_term_of tm2)
in
([tm1, tm2],
- [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate,
- NONE, isabelle_info non_rec_defN helper_rank)])
+ [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role,
+ eq |> maybe_negate, NONE,
+ isabelle_info non_rec_defN helper_rank)])
|> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
else pair_append (do_alias (ary - 1)))
end
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 13 22:49:07 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 13 22:49:08 2012 +0100
@@ -364,7 +364,7 @@
| is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
| is_same_formula _ _ _ _ = false
-fun matching_formula_line_identifier phi (Formula (ident, _, phi', _, _)) =
+fun matching_formula_line_identifier phi (Formula ((ident, _), _, phi', _, _)) =
if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE
| matching_formula_line_identifier _ _ = NONE
--- a/src/HOL/Tools/Metis/metis_generate.ML Thu Dec 13 22:49:07 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML Thu Dec 13 22:49:08 2012 +0100
@@ -161,7 +161,7 @@
fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
maps (metis_literals_from_atp type_enc) phis
| metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
-fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
+fun metis_axiom_from_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
let
fun some isa =
SOME (phi |> metis_literals_from_atp type_enc