--- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 31 16:38:36 2011 +0200
@@ -143,6 +143,17 @@
fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
+fun raw_polarities_of_conn ANot = (SOME false, NONE)
+ | raw_polarities_of_conn AAnd = (SOME true, SOME true)
+ | raw_polarities_of_conn AOr = (SOME true, SOME true)
+ | raw_polarities_of_conn AImplies = (SOME false, SOME true)
+ | raw_polarities_of_conn AIf = (SOME true, SOME false)
+ | raw_polarities_of_conn AIff = (NONE, NONE)
+ | raw_polarities_of_conn ANotIff = (NONE, NONE)
+fun polarities_of_conn NONE = K (NONE, NONE)
+ | polarities_of_conn (SOME pos) =
+ raw_polarities_of_conn #> not pos ? pairself (Option.map not)
+
fun mk_anot (AConn (ANot, [phi])) = phi
| mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
@@ -286,7 +297,7 @@
problem
-(** CNF UEQ (Waldmeister) **)
+(** CNF (Metis) and CNF UEQ (Waldmeister) **)
fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
| is_problem_line_negated _ = false
@@ -298,9 +309,17 @@
fun open_conjecture_term (ATerm ((s, s'), tms)) =
ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
else (s, s'), tms |> map open_conjecture_term)
-fun open_formula conj (AQuant (AForall, _, phi)) = open_formula conj phi
- | open_formula true (AAtom t) = AAtom (open_conjecture_term t)
- | open_formula _ phi = phi
+fun open_formula conj =
+ let
+ fun opn (pos as SOME true) (AQuant (AForall, xs, phi)) = opn pos phi
+ | opn (pos as SOME false) (AQuant (AExists, xs, phi)) = opn pos phi
+ | opn pos (AConn (ANot, [phi])) = mk_anot (opn (Option.map not pos) phi)
+ | opn pos (AConn (c, [phi1, phi2])) =
+ let val (pos1, pos2) = polarities_of_conn pos c in
+ AConn (c, [opn pos1 phi1, opn pos2 phi2])
+ end
+ | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term)
+ in opn (SOME (not conj)) end
fun open_formula_line (Formula (ident, kind, phi, source, info)) =
Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info)
| open_formula_line line = line
@@ -309,7 +328,31 @@
Formula (ident, Hypothesis, mk_anot phi, source, info)
| negate_conjecture_line line = line
-fun ensure_cnf_problem problem = problem |> map (apsnd (map open_formula_line))
+exception CLAUSIFY of unit
+
+fun clausify_formula pos (phi as AAtom _) = phi |> not pos ? mk_anot
+ | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi
+ | clausify_formula false (AConn (AAnd, phis)) =
+ AConn (AOr, map (clausify_formula false) phis)
+ | clausify_formula true (AConn (AOr, phis)) =
+ AConn (AOr, map (clausify_formula true) phis)
+ | clausify_formula true (AConn (AImplies, [phi1, phi2])) =
+ AConn (AOr, [clausify_formula false phi1, clausify_formula true phi2])
+ | clausify_formula true (AConn (AIf, phis)) =
+ clausify_formula true (AConn (AImplies, rev phis))
+ | clausify_formula _ _ = raise CLAUSIFY ()
+
+fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =
+ (case try (clausify_formula true) phi of
+ SOME phi => SOME (Formula (ident, kind, phi, source, info))
+ | NONE => NONE)
+ | clausify_formula_line _ = NONE
+
+fun ensure_cnf_problem_line line =
+ line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line
+
+fun ensure_cnf_problem problem =
+ problem |> map (apsnd (map_filter ensure_cnf_problem_line))
fun filter_cnf_ueq_problem problem =
problem
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -618,9 +618,9 @@
general_type_arg_policy type_sys
(*Make literals for sorted type variables*)
-fun sorts_on_typs_aux (_, []) = []
- | sorts_on_typs_aux ((x, i), s :: ss) =
- sorts_on_typs_aux ((x, i), ss)
+fun generic_sorts_on_type (_, []) = []
+ | generic_sorts_on_type ((x, i), s :: ss) =
+ generic_sorts_on_type ((x, i), ss)
|> (if s = the_single @{sort HOL.type} then
I
else if i = ~1 then
@@ -628,21 +628,18 @@
else
cons (TyLitVar (`make_type_class s,
(make_schematic_type_var (x, i), x))))
-
-fun sorts_on_typs (TFree (a, s)) = sorts_on_typs_aux ((a, ~1), s)
- | sorts_on_typs (TVar (v, s)) = sorts_on_typs_aux (v, s)
- | sorts_on_typs _ = raise Fail "expected \"TVar\" or \"TFree\""
-
-(*Given a list of sorted type variables, return a list of type literals.*)
-val raw_type_literals_for_types = union_all o map sorts_on_typs
+fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S)
+ | sorts_on_tfree _ = []
+fun sorts_on_tvar (TVar z) = generic_sorts_on_type z
+ | sorts_on_tvar _ = []
-fun type_literals_for_types format type_sys kind Ts =
- if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then
- []
- else
- Ts |> raw_type_literals_for_types
- |> filter (fn TyLitVar _ => kind <> Conjecture
- | TyLitFree _ => kind = Conjecture)
+(* Given a list of sorted type variables, return a list of type literals. *)
+fun raw_type_literals_for_types Ts =
+ union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)
+
+fun type_literals_for_types type_sys sorts_on_typ Ts =
+ if level_of_type_sys type_sys = No_Types then []
+ else union_all (map sorts_on_typ Ts)
fun mk_aconns c phis =
let val (phis', phi') = split_last phis in
@@ -893,7 +890,6 @@
|> extensionalize_term ctxt
|> presimp ? presimplify_term ctxt
|> introduce_combinators_in_term ctxt kind
- |> kind <> Axiom ? freeze_term
end
(* making fact and conjecture formulas *)
@@ -933,7 +929,7 @@
if prem_kind = Conjecture then update_combformula mk_anot
else I)
in
- t |> preproc ? preprocess_prop ctxt true kind
+ t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
|> make_formula thy format type_sys true (string_of_int j)
General kind
|> maybe_negate
@@ -1458,9 +1454,9 @@
| do_formula _ (AAtom tm) = AAtom (do_term tm)
in do_formula o SOME end
-fun bound_atomic_types format type_sys Ts =
+fun bound_tvars type_sys Ts =
mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
- (type_literals_for_types format type_sys Axiom Ts))
+ (type_literals_for_types type_sys sorts_on_tvar Ts))
fun formula_for_fact ctxt format nonmono_Ts type_sys
({combformula, atomic_types, ...} : translated_formula) =
@@ -1468,7 +1464,7 @@
|> close_combformula_universally
|> formula_from_combformula ctxt format nonmono_Ts type_sys
is_var_nonmonotonic_in_formula true
- |> bound_atomic_types format type_sys atomic_types
+ |> bound_tvars type_sys atomic_types
|> close_formula_universally
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
@@ -1510,24 +1506,24 @@
|> close_formula_universally, intro_info, NONE)
fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
- ({name, kind, combformula, ...} : translated_formula) =
+ ({name, kind, combformula, atomic_types, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
formula_from_combformula ctxt format nonmono_Ts type_sys
is_var_nonmonotonic_in_formula false
(close_combformula_universally combformula)
+ |> bound_tvars type_sys atomic_types
|> close_formula_universally, NONE, NONE)
-fun free_type_literals format type_sys
- ({atomic_types, ...} : translated_formula) =
- atomic_types |> type_literals_for_types format type_sys Conjecture
+fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
+ atomic_types |> type_literals_for_types type_sys sorts_on_tfree
|> map fo_literal_from_type_literal
fun formula_line_for_free_type j lit =
Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
formula_from_fo_literal lit, NONE, NONE)
-fun formula_lines_for_free_types format type_sys facts =
+fun formula_lines_for_free_types type_sys facts =
let
- val litss = map (free_type_literals format type_sys) facts
+ val litss = map (free_type_literals type_sys) facts
val lits = fold (union (op =)) litss []
in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
@@ -1636,7 +1632,7 @@
|> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
|> formula_from_combformula ctxt format nonmono_Ts type_sys
(K (K (K (K true)))) true
- |> n > 1 ? bound_atomic_types format type_sys (atyps_of T)
+ |> n > 1 ? bound_tvars type_sys (atyps_of T)
|> close_formula_universally
|> maybe_negate,
intro_info, NONE)
@@ -1659,7 +1655,7 @@
fun eq tms =
(if pred_sym then AConn (AIff, map AAtom tms)
else AAtom (ATerm (`I tptp_equal, tms)))
- |> bound_atomic_types format type_sys atomic_Ts
+ |> bound_tvars type_sys atomic_Ts
|> close_formula_universally
|> maybe_negate
val should_encode = should_encode_type ctxt nonmono_Ts All_Types
@@ -1802,8 +1798,7 @@
(conjsN,
map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
conjs),
- (free_typesN,
- formula_lines_for_free_types format type_sys (facts @ conjs))]
+ (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
val problem =
problem
|> (case format of
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -299,11 +299,11 @@
uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2))
| metis_literals_from_atp phi = [metis_literal_from_atp phi]
fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
- let val j = ident |> unprefix conjecture_prefix |> Int.fromString |> the in
- (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
- |> Metis_Thm.axiom,
- Meson.make_meta_clause (nth clauses j))
- end
+ (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
+ |> Metis_Thm.axiom,
+ case try (unprefix conjecture_prefix) ident of
+ SOME s => Meson.make_meta_clause (nth clauses (the (Int.fromString s)))
+ | NONE => TrueI)
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
(* Function to generate metis clauses, including comb and type clauses *)
@@ -313,9 +313,8 @@
val explicit_apply = NONE
val clauses = conj_clauses @ fact_clauses
val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys
- explicit_apply false false (map prop_of clauses)
- @{prop False} []
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
+ false false (map prop_of clauses) @{prop False} []
val axioms =
atp_problem
|> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)