--- a/src/HOL/HOL.thy Thu Sep 02 12:30:22 2010 +0200
+++ b/src/HOL/HOL.thy Thu Sep 02 13:45:39 2010 +0200
@@ -32,6 +32,7 @@
("Tools/recfun_codegen.ML")
"Tools/async_manager.ML"
"Tools/try.ML"
+ ("Tools/cnf_funcs.ML")
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -1645,7 +1646,6 @@
"(\<not> \<not>(P)) = P"
by blast+
-
subsection {* Basic ML bindings *}
ML {*
@@ -1699,6 +1699,7 @@
val trans = @{thm trans}
*}
+use "Tools/cnf_funcs.ML"
subsection {* Code generator setup *}
--- a/src/HOL/Hilbert_Choice.thy Thu Sep 02 12:30:22 2010 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu Sep 02 13:45:39 2010 +0200
@@ -7,7 +7,8 @@
theory Hilbert_Choice
imports Nat Wellfounded Plain
-uses ("Tools/meson.ML") ("Tools/choice_specification.ML")
+uses ("Tools/meson.ML")
+ ("Tools/choice_specification.ML")
begin
subsection {* Hilbert's epsilon *}
--- a/src/HOL/SAT.thy Thu Sep 02 12:30:22 2010 +0200
+++ b/src/HOL/SAT.thy Thu Sep 02 13:45:39 2010 +0200
@@ -10,7 +10,6 @@
theory SAT
imports Refute
uses
- "Tools/cnf_funcs.ML"
"Tools/sat_funcs.ML"
begin
--- a/src/HOL/Sledgehammer.thy Thu Sep 02 12:30:22 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Sep 02 13:45:39 2010 +0200
@@ -26,6 +26,9 @@
("Tools/Sledgehammer/sledgehammer_isar.ML")
begin
+lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
+by simp
+
definition skolem_id :: "'a \<Rightarrow> 'a" where
[no_atp]: "skolem_id = (\<lambda>x. x)"
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 02 12:30:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 02 13:45:39 2010 +0200
@@ -10,7 +10,8 @@
val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
- val cnf_axiom: theory -> thm -> thm list
+ val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
+ val cnf_axiom : theory -> thm -> thm list
end;
structure Clausifier : CLAUSIFIER =
@@ -228,19 +229,26 @@
|> Meson.make_nnf ctxt
in (th3, ctxt) end
+fun to_definitional_cnf_with_quantifiers thy th =
+ let
+ val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
+ val eqth = eqth RS @{thm eq_reflection}
+ val eqth = eqth RS @{thm TruepropI}
+ in Thm.equal_elim eqth th end
+
(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
fun cnf_axiom thy th =
let
val ctxt0 = Variable.global_thm_context th
- val (nnfth, ctxt) = to_nnf th ctxt0
- val sko_ths = map (skolem_theorem_of_def thy)
- (assume_skolem_funs nnfth)
- val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
+ val (nnf_th, ctxt) = to_nnf th ctxt0
+ val def_th = to_definitional_cnf_with_quantifiers thy nnf_th
+ val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th)
+ val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt
in
- cnfs |> map introduce_combinators_in_theorem
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- |> map Thm.close_derivation
+ cnf_ths |> map introduce_combinators_in_theorem
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ |> map Thm.close_derivation
end
handle THM _ => []
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 12:30:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 13:45:39 2010 +0200
@@ -795,13 +795,15 @@
fun generic_metis_tac mode ctxt ths i st0 =
let
+ val thy = ProofContext.theory_of ctxt
val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- Meson.MESON (maps neg_clausify)
+ Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *)
+ (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
end
--- a/src/HOL/Tools/cnf_funcs.ML Thu Sep 02 12:30:22 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Sep 02 13:45:39 2010 +0200
@@ -430,7 +430,7 @@
in
make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
end
- | make_cnfx_disj_thm (Const (@{const_name Ex}, _) $ x') y' =
+ | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
val var = new_free ()
@@ -441,7 +441,7 @@
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
- | make_cnfx_disj_thm x' (Const (@{const_name Ex}, _) $ y') =
+ | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
val var = new_free ()
--- a/src/HOL/Tools/meson.ML Thu Sep 02 12:30:22 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Sep 02 13:45:39 2010 +0200
@@ -25,7 +25,9 @@
val depth_prolog_tac: thm list -> tactic
val gocls: thm list -> thm list
val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic
- val MESON: (thm list -> thm list) -> (thm list -> tactic) -> Proof.context -> int -> tactic
+ val MESON:
+ (int -> tactic) -> (thm list -> thm list) -> (thm list -> tactic)
+ -> Proof.context -> int -> tactic
val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
val safe_best_meson_tac: Proof.context -> int -> tactic
val depth_meson_tac: Proof.context -> int -> tactic
@@ -315,8 +317,8 @@
(nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
fun resop nf [prem] = resolve_tac (nf prem) 1;
-(*Any need to extend this list with
- "HOL.type_class","HOL.eq_class","Pure.term"?*)
+(* Any need to extend this list with "HOL.type_class", "HOL.eq_class",
+ and "Pure.term"? *)
val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
fun apply_skolem_theorem (th, rls) =
@@ -573,7 +575,8 @@
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
The resulting clauses are HOL disjunctions.*)
-fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
+fun make_clauses_unsorted ths = fold_rev add_clauses ths []
+handle exn => error (ML_Compiler.exn_message exn) (*###*)
val make_clauses = sort_clauses o make_clauses_unsorted;
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
@@ -598,20 +601,22 @@
(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
Function mkcl converts theorems to clauses.*)
-fun MESON mkcl cltac ctxt i st =
+fun MESON preskolem_tac mkcl cltac ctxt i st =
SELECT_GOAL
(EVERY [Object_Logic.atomize_prems_tac 1,
rtac ccontr 1,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
- EVERY1 [skolemize_prems_tac ctxt negs,
+ EVERY1 [preskolem_tac,
+ skolemize_prems_tac ctxt negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
+
(** Best-first search versions **)
(*ths is a list of additional clauses (HOL disjunctions) to use.*)
fun best_meson_tac sizef =
- MESON make_clauses
+ MESON (K all_tac) make_clauses
(fn cls =>
THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
(has_fewer_prems 1, sizef)
@@ -625,7 +630,7 @@
(** Depth-first search version **)
val depth_meson_tac =
- MESON make_clauses
+ MESON (K all_tac) make_clauses
(fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
@@ -645,7 +650,7 @@
fun iter_deepen_prolog_tac horns =
ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
-fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
+fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON (K all_tac) make_clauses
(fn cls =>
(case (gocls (cls @ ths)) of
[] => no_tac (*no goal clauses*)