# HG changeset patch # User blanchet # Date 1307542819 -7200 # Node ID 30aaab778416c8c31f4049a4d27485838fd3c4ba # Parent 0271fda2a83af65760a0ae8d00d97f029f2840e6 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 diff -r 0271fda2a83a -r 30aaab778416 src/HOL/Tools/ATP/atp_problem.ML --- 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 _ = [] diff -r 0271fda2a83a -r 30aaab778416 src/HOL/Tools/ATP/atp_translate.ML --- 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)) diff -r 0271fda2a83a -r 30aaab778416 src/HOL/Tools/Metis/metis_translate.ML --- 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)