pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Jun 08 16:20:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Jun 08 16:20:19 2011 +0200
@@ -351,9 +351,8 @@
val (n, phis) = phi |> try (clausify_formula true) |> these |> `length
in
map2 (fn phi => fn j =>
- Formula (ident ^
- (if n > 1 then "_cls" ^ string_of_int j else ""),
- kind, phi, source, info))
+ Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source,
+ info))
phis (1 upto n)
end
| clausify_formula_line _ = []
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 16:20:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 16:20:19 2011 +0200
@@ -975,16 +975,15 @@
atomic_types = atomic_types}
end
-fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp_consts
+fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
- case (keep_trivial,
- t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
- |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
- (false,
- formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
+ case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
+ |> make_formula thy format type_sys (eq_as_iff andalso format <> CNF)
+ name loc Axiom of
+ formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
if s = tptp_true then NONE else SOME formula
- | (_, formula) => SOME formula
+ | formula => SOME formula
end
fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
@@ -1354,7 +1353,7 @@
| _ => I)
end)
val make_facts =
- map_filter (make_fact ctxt format type_sys false false false [])
+ map_filter (make_fact ctxt format type_sys false false [])
val fairly_sound = is_type_sys_fairly_sound type_sys
in
helper_table
@@ -1417,8 +1416,7 @@
val thy = Proof_Context.theory_of ctxt
val fact_ts = facts |> map snd
val presimp_consts = Meson.presimplified_consts ctxt
- val make_fact =
- make_fact ctxt format type_sys false true true presimp_consts
+ val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
val (facts, fact_names) =
facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
|> map_filter (try (apfst the))
--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 16:20:18 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 16:20:19 2011 +0200
@@ -145,6 +145,8 @@
if ident = type_tag_idempotence_helper_name orelse
String.isPrefix lightweight_tags_sym_formula_prefix ident then
Isa_Reflexive_or_Trivial |> some
+ else if String.isPrefix conjecture_prefix ident then
+ NONE
else if String.isPrefix helper_prefix ident then
case (String.isSuffix typed_helper_suffix ident,
space_explode "_" ident) of
@@ -155,12 +157,11 @@
|> prepare_helper
|> Isa_Raw |> some
| _ => raise Fail ("malformed helper identifier " ^ quote ident)
- else case try (unprefix conjecture_prefix) ident of
+ else case try (unprefix fact_prefix) ident of
SOME s =>
- let val j = the (Int.fromString s) in
- if j = length clauses then NONE
- else Meson.make_meta_clause (nth clauses j) |> Isa_Raw |> some
- end
+ let
+ val j = s |> space_explode "_" |> List.last |> Int.fromString |> the
+ in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
| NONE => TrueI |> Isa_Raw |> some
end
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
@@ -169,31 +170,40 @@
fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
let
val type_sys = type_sys_from_string type_sys
+ val (conj_clauses, fact_clauses) =
+ if polymorphism_of_type_sys type_sys = Polymorphic then
+ (conj_clauses, fact_clauses)
+ else
+ conj_clauses @ fact_clauses
+ |> map (pair 0)
+ |> rpair ctxt
+ |-> Monomorph.monomorph atp_schematic_consts_of
+ |> fst |> chop (length conj_clauses)
+ |> pairself (maps (map (zero_var_indexes o snd)))
+ val num_conjs = length conj_clauses
val clauses =
- conj_clauses @ fact_clauses
- |> (if polymorphism_of_type_sys type_sys = Polymorphic then
- I
- else
- map (pair 0)
- #> rpair ctxt
- #-> Monomorph.monomorph atp_schematic_consts_of
- #> fst #> maps (map (zero_var_indexes o snd)))
+ map2 (fn j => pair (Int.toString j, Local))
+ (0 upto num_conjs - 1) conj_clauses @
+ (* "General" below isn't quite correct; the fact could be local. *)
+ map2 (fn j => pair (Int.toString (num_conjs + j), General))
+ (0 upto length fact_clauses - 1) fact_clauses
val (old_skolems, props) =
- fold_rev (fn clause => fn (old_skolems, props) =>
- clause |> prop_of |> Logic.strip_imp_concl
- |> conceal_old_skolem_terms (length clauses)
- old_skolems
- ||> (fn prop => prop :: props))
- clauses ([], [])
-(*
-val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
-*)
+ fold_rev (fn (name, th) => fn (old_skolems, props) =>
+ th |> prop_of |> Logic.strip_imp_concl
+ |> conceal_old_skolem_terms (length clauses) old_skolems
+ ||> (fn prop => (name, prop) :: props))
+ clauses ([], [])
+ (*
+ val _ =
+ tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
+ *)
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props
- @{prop False} []
-(*
-val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
-*)
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false []
+ @{prop False} props
+ (*
+ val _ = tracing ("ATP PROBLEM: " ^
+ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
+ *)
(* "rev" is for compatibility *)
val axioms =
atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)