--- a/src/HOL/IsaMakefile Thu Dec 02 10:36:20 2004 +0100
+++ b/src/HOL/IsaMakefile Thu Dec 02 11:09:19 2004 +0100
@@ -94,7 +94,8 @@
Nat.thy NatArith.ML NatArith.thy \
Power.thy PreList.thy Product_Type.ML Product_Type.thy \
Refute.thy ROOT.ML \
- Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
+ Recdef.thy Reconstruction.thy\
+ Record.thy Relation.ML Relation.thy Relation_Power.ML \
Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
Set.ML Set.thy SetInterval.ML SetInterval.thy \
Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
@@ -104,7 +105,7 @@
Tools/meson.ML Tools/numeral_syntax.ML \
Tools/primrec_package.ML Tools/prop_logic.ML \
Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
- Tools/refute.ML Tools/refute_isar.ML \
+ Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
Tools/res_axioms.ML Tools/res_types_sorts.ML Tools/res_atp.ML\
Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
--- a/src/HOL/ROOT.ML Thu Dec 02 10:36:20 2004 +0100
+++ b/src/HOL/ROOT.ML Thu Dec 02 11:09:19 2004 +0100
@@ -39,14 +39,6 @@
with_path "Integ" use_thy "Main";
-(*Linking to external resolution provers*)
-use "Tools/res_lib.ML";
-use "Tools/res_clause.ML";
-use "Tools/res_skolem_function.ML";
-use "Tools/res_axioms.ML";
-use "Tools/res_types_sorts.ML";
-use "Tools/res_atp.ML";
-
path_add "~~/src/HOL/Library";
print_depth 8;
--- a/src/HOL/Reconstruction.thy Thu Dec 02 10:36:20 2004 +0100
+++ b/src/HOL/Reconstruction.thy Thu Dec 02 11:09:19 2004 +0100
@@ -8,7 +8,13 @@
theory Reconstruction
imports Hilbert_Choice
- files "Tools/reconstruction.ML"
+ files "Tools/res_lib.ML"
+ "Tools/res_clause.ML"
+ "Tools/res_skolem_function.ML"
+ "Tools/res_axioms.ML"
+ "Tools/res_types_sorts.ML"
+ "Tools/res_atp.ML"
+ "Tools/reconstruction.ML"
begin
--- a/src/HOL/Tools/reconstruction.ML Thu Dec 02 10:36:20 2004 +0100
+++ b/src/HOL/Tools/reconstruction.ML Thu Dec 02 11:09:19 2004 +0100
@@ -163,6 +163,18 @@
val DEMOD_local = gen_DEMOD local_thm;
+(** Conversion of a theorem into clauses **)
+
+fun clausify_rule (A,i) =
+ standard
+ (make_meta_clause
+ (List.nth(ResAxioms.cnf_axiom A,i-1)));
+
+fun clausify_syntax i (x, A) = (x, clausify_rule (A,i));
+
+fun CLAUSIFY x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x;
+
+
(** theory setup **)
val setup =
@@ -170,7 +182,8 @@
[("BINARY", (BINARY_global, BINARY_local), "binary resolution"),
("PARAMOD", (PARAMOD_global, PARAMOD_local), "paramodulation"),
("DEMOD", (DEMOD_global, DEMOD_local), "demodulation"),
- ("FACTOR", (FACTOR, FACTOR), "factoring")]];
+ ("FACTOR", (FACTOR, FACTOR), "factoring"),
+ ("CLAUSIFY", (CLAUSIFY, CLAUSIFY), "conversion to clauses")]];
end
end
--- a/src/HOL/Tools/res_axioms.ML Thu Dec 02 10:36:20 2004 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Dec 02 11:09:19 2004 +0100
@@ -122,8 +122,6 @@
(* some lemmas *)
-(* TO BE FIXED: the names of these lemmas should be made local, to avoid confusion with external global lemmas. *)
-
Goal "(P==True) ==> P";
by(Blast_tac 1);
qed "Eq_TrueD1";
@@ -132,7 +130,6 @@
by(Blast_tac 1);
qed "Eq_TrueD2";
-
Goal "(P==False) ==> ~P";
by(Blast_tac 1);
qed "Eq_FalseD1";
@@ -141,50 +138,22 @@
by(Blast_tac 1);
qed "Eq_FalseD2";
-Goal "(P | True) == True";
-by(Simp_tac 1);
-qed "s1";
-
-Goal "(True | P) == True";
-by(Simp_tac 1);
-qed "s2";
+local
-Goal "(P & True) == P";
-by(Simp_tac 1);
-qed "s3";
-
-Goal "(True & P) == P";
-by(Simp_tac 1);
-qed "s4";
-
-Goal "(False | P) == P";
-by(Simp_tac 1);
-qed "s5";
-
+ fun prove s = prove_goal (the_context()) s (fn _ => [Simp_tac 1]);
-Goal "(P | False) == P";
-by(Simp_tac 1);
-qed "s6";
-
-Goal "(False & P) == False";
-by(Simp_tac 1);
-qed "s7";
-
-Goal "(P & False) == False";
-by(Simp_tac 1);
-qed "s8";
+val small_simps =
+ map prove
+ ["(P | True) == True", "(True | P) == True",
+ "(P & True) == P", "(True & P) == P",
+ "(False | P) == P", "(P | False) == P",
+ "(False & P) == False", "(P & False) == False",
+ "~True == False", "~False == True"];
+in
-Goal "~True == False";
-by(Simp_tac 1);
-qed "s9";
+val small_simpset = empty_ss addsimps small_simps
-Goal "~False == True";
-by(Simp_tac 1);
-qed "s10";
-
-
-val small_simpset = empty_ss addsimps [s1,s2,s3,s4,s5,s6,s7,s8,s9,s10];
-
+end;
signature RES_AXIOMS =
@@ -261,8 +230,13 @@
-(* transfer a theorem in to theory Main.thy if it is not already inside Main.thy *)
-fun transfer_to_Main thm = transfer Main.thy thm handle THM _ => thm;
+(*Transfer a theorem in to theory Hilbert_Choice.thy if it is not already
+ inside that theory -- because it's needed for Skolemization *)
+
+val hc_thy = ThyInfo.get_theory"Hilbert_Choice";
+
+fun transfer_to_Hilbert_Choice thm =
+ transfer hc_thy thm handle THM _ => thm;
(* remove "True" clause *)
fun rm_redundant_cls [] = []
@@ -275,7 +249,7 @@
(* transform an Isabelle thm into CNF *)
fun cnf_axiom thm =
- let val thm' = transfer_to_Main thm
+ let val thm' = transfer_to_Hilbert_Choice thm
val thm'' = if (is_elimR thm') then (cnf_elim thm')
else (if (is_introR thm') then cnf_intro thm' else cnf_rule thm')
in