# HG changeset patch
# User paulson
# Date 1101982159 -3600
# Node ID 8bad1f42fec06c0c442f8008b22d857425f820d3
# Parent  26c501c5024def469438f2bf3374e3122d4bd215
new CLAUSIFY attribute for proof reconstruction with lemmas

diff -r 26c501c5024d -r 8bad1f42fec0 src/HOL/IsaMakefile
--- 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 \
diff -r 26c501c5024d -r 8bad1f42fec0 src/HOL/ROOT.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;
diff -r 26c501c5024d -r 8bad1f42fec0 src/HOL/Reconstruction.thy
--- 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
 
diff -r 26c501c5024d -r 8bad1f42fec0 src/HOL/Tools/reconstruction.ML
--- 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
diff -r 26c501c5024d -r 8bad1f42fec0 src/HOL/Tools/res_axioms.ML
--- 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