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
1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Jun 08 16:20:18 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Jun 08 16:20:19 2011 +0200
1.3 @@ -351,9 +351,8 @@
1.4 val (n, phis) = phi |> try (clausify_formula true) |> these |> `length
1.5 in
1.6 map2 (fn phi => fn j =>
1.7 - Formula (ident ^
1.8 - (if n > 1 then "_cls" ^ string_of_int j else ""),
1.9 - kind, phi, source, info))
1.10 + Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source,
1.11 + info))
1.12 phis (1 upto n)
1.13 end
1.14 | clausify_formula_line _ = []
2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 16:20:18 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 16:20:19 2011 +0200
2.3 @@ -975,16 +975,15 @@
2.4 atomic_types = atomic_types}
2.5 end
2.6
2.7 -fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp_consts
2.8 +fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
2.9 ((name, loc), t) =
2.10 let val thy = Proof_Context.theory_of ctxt in
2.11 - case (keep_trivial,
2.12 - t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
2.13 - |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
2.14 - (false,
2.15 - formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
2.16 + case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
2.17 + |> make_formula thy format type_sys (eq_as_iff andalso format <> CNF)
2.18 + name loc Axiom of
2.19 + formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
2.20 if s = tptp_true then NONE else SOME formula
2.21 - | (_, formula) => SOME formula
2.22 + | formula => SOME formula
2.23 end
2.24
2.25 fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
2.26 @@ -1354,7 +1353,7 @@
2.27 | _ => I)
2.28 end)
2.29 val make_facts =
2.30 - map_filter (make_fact ctxt format type_sys false false false [])
2.31 + map_filter (make_fact ctxt format type_sys false false [])
2.32 val fairly_sound = is_type_sys_fairly_sound type_sys
2.33 in
2.34 helper_table
2.35 @@ -1417,8 +1416,7 @@
2.36 val thy = Proof_Context.theory_of ctxt
2.37 val fact_ts = facts |> map snd
2.38 val presimp_consts = Meson.presimplified_consts ctxt
2.39 - val make_fact =
2.40 - make_fact ctxt format type_sys false true true presimp_consts
2.41 + val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
2.42 val (facts, fact_names) =
2.43 facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
2.44 |> map_filter (try (apfst the))
3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 16:20:18 2011 +0200
3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 16:20:19 2011 +0200
3.3 @@ -145,6 +145,8 @@
3.4 if ident = type_tag_idempotence_helper_name orelse
3.5 String.isPrefix lightweight_tags_sym_formula_prefix ident then
3.6 Isa_Reflexive_or_Trivial |> some
3.7 + else if String.isPrefix conjecture_prefix ident then
3.8 + NONE
3.9 else if String.isPrefix helper_prefix ident then
3.10 case (String.isSuffix typed_helper_suffix ident,
3.11 space_explode "_" ident) of
3.12 @@ -155,12 +157,11 @@
3.13 |> prepare_helper
3.14 |> Isa_Raw |> some
3.15 | _ => raise Fail ("malformed helper identifier " ^ quote ident)
3.16 - else case try (unprefix conjecture_prefix) ident of
3.17 + else case try (unprefix fact_prefix) ident of
3.18 SOME s =>
3.19 - let val j = the (Int.fromString s) in
3.20 - if j = length clauses then NONE
3.21 - else Meson.make_meta_clause (nth clauses j) |> Isa_Raw |> some
3.22 - end
3.23 + let
3.24 + val j = s |> space_explode "_" |> List.last |> Int.fromString |> the
3.25 + in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
3.26 | NONE => TrueI |> Isa_Raw |> some
3.27 end
3.28 | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
3.29 @@ -169,31 +170,40 @@
3.30 fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
3.31 let
3.32 val type_sys = type_sys_from_string type_sys
3.33 + val (conj_clauses, fact_clauses) =
3.34 + if polymorphism_of_type_sys type_sys = Polymorphic then
3.35 + (conj_clauses, fact_clauses)
3.36 + else
3.37 + conj_clauses @ fact_clauses
3.38 + |> map (pair 0)
3.39 + |> rpair ctxt
3.40 + |-> Monomorph.monomorph atp_schematic_consts_of
3.41 + |> fst |> chop (length conj_clauses)
3.42 + |> pairself (maps (map (zero_var_indexes o snd)))
3.43 + val num_conjs = length conj_clauses
3.44 val clauses =
3.45 - conj_clauses @ fact_clauses
3.46 - |> (if polymorphism_of_type_sys type_sys = Polymorphic then
3.47 - I
3.48 - else
3.49 - map (pair 0)
3.50 - #> rpair ctxt
3.51 - #-> Monomorph.monomorph atp_schematic_consts_of
3.52 - #> fst #> maps (map (zero_var_indexes o snd)))
3.53 + map2 (fn j => pair (Int.toString j, Local))
3.54 + (0 upto num_conjs - 1) conj_clauses @
3.55 + (* "General" below isn't quite correct; the fact could be local. *)
3.56 + map2 (fn j => pair (Int.toString (num_conjs + j), General))
3.57 + (0 upto length fact_clauses - 1) fact_clauses
3.58 val (old_skolems, props) =
3.59 - fold_rev (fn clause => fn (old_skolems, props) =>
3.60 - clause |> prop_of |> Logic.strip_imp_concl
3.61 - |> conceal_old_skolem_terms (length clauses)
3.62 - old_skolems
3.63 - ||> (fn prop => prop :: props))
3.64 - clauses ([], [])
3.65 -(*
3.66 -val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
3.67 -*)
3.68 + fold_rev (fn (name, th) => fn (old_skolems, props) =>
3.69 + th |> prop_of |> Logic.strip_imp_concl
3.70 + |> conceal_old_skolem_terms (length clauses) old_skolems
3.71 + ||> (fn prop => (name, prop) :: props))
3.72 + clauses ([], [])
3.73 + (*
3.74 + val _ =
3.75 + tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
3.76 + *)
3.77 val (atp_problem, _, _, _, _, _, sym_tab) =
3.78 - prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props
3.79 - @{prop False} []
3.80 -(*
3.81 -val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
3.82 -*)
3.83 + prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false []
3.84 + @{prop False} props
3.85 + (*
3.86 + val _ = tracing ("ATP PROBLEM: " ^
3.87 + cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
3.88 + *)
3.89 (* "rev" is for compatibility *)
3.90 val axioms =
3.91 atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)