new CLAUSIFY attribute for proof reconstruction with lemmas
authorpaulson
Thu Dec 02 11:09:19 2004 +0100 (2004-12-02)
changeset 153598bad1f42fec0
parent 15358 26c501c5024d
child 15360 300e09825d8b
new CLAUSIFY attribute for proof reconstruction with lemmas
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/HOL/Reconstruction.thy
src/HOL/Tools/reconstruction.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Dec 02 10:36:20 2004 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Dec 02 11:09:19 2004 +0100
     1.3 @@ -94,7 +94,8 @@
     1.4    Nat.thy NatArith.ML NatArith.thy \
     1.5    Power.thy PreList.thy Product_Type.ML Product_Type.thy \
     1.6    Refute.thy ROOT.ML \
     1.7 -  Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
     1.8 +  Recdef.thy Reconstruction.thy\
     1.9 +  Record.thy Relation.ML Relation.thy Relation_Power.ML \
    1.10    Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
    1.11    Set.ML Set.thy SetInterval.ML SetInterval.thy \
    1.12    Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
    1.13 @@ -104,7 +105,7 @@
    1.14    Tools/meson.ML Tools/numeral_syntax.ML \
    1.15    Tools/primrec_package.ML Tools/prop_logic.ML \
    1.16    Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
    1.17 -  Tools/refute.ML Tools/refute_isar.ML \
    1.18 +  Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
    1.19    Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
    1.20    Tools/res_axioms.ML Tools/res_types_sorts.ML Tools/res_atp.ML\
    1.21    Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
     2.1 --- a/src/HOL/ROOT.ML	Thu Dec 02 10:36:20 2004 +0100
     2.2 +++ b/src/HOL/ROOT.ML	Thu Dec 02 11:09:19 2004 +0100
     2.3 @@ -39,14 +39,6 @@
     2.4  
     2.5  with_path "Integ" use_thy "Main";
     2.6  
     2.7 -(*Linking to external resolution provers*)
     2.8 -use "Tools/res_lib.ML";
     2.9 -use "Tools/res_clause.ML";
    2.10 -use "Tools/res_skolem_function.ML";
    2.11 -use "Tools/res_axioms.ML";
    2.12 -use "Tools/res_types_sorts.ML";
    2.13 -use "Tools/res_atp.ML";
    2.14 -
    2.15  path_add "~~/src/HOL/Library";
    2.16  
    2.17  print_depth 8;
     3.1 --- a/src/HOL/Reconstruction.thy	Thu Dec 02 10:36:20 2004 +0100
     3.2 +++ b/src/HOL/Reconstruction.thy	Thu Dec 02 11:09:19 2004 +0100
     3.3 @@ -8,7 +8,13 @@
     3.4  
     3.5  theory Reconstruction
     3.6      imports Hilbert_Choice
     3.7 -    files   "Tools/reconstruction.ML"
     3.8 +    files "Tools/res_lib.ML"
     3.9 +	  "Tools/res_clause.ML"
    3.10 +	  "Tools/res_skolem_function.ML"
    3.11 +	  "Tools/res_axioms.ML"
    3.12 +	  "Tools/res_types_sorts.ML"
    3.13 +	  "Tools/res_atp.ML"
    3.14 +          "Tools/reconstruction.ML"
    3.15  
    3.16  begin
    3.17  
     4.1 --- a/src/HOL/Tools/reconstruction.ML	Thu Dec 02 10:36:20 2004 +0100
     4.2 +++ b/src/HOL/Tools/reconstruction.ML	Thu Dec 02 11:09:19 2004 +0100
     4.3 @@ -163,6 +163,18 @@
     4.4  val DEMOD_local = gen_DEMOD local_thm;
     4.5  
     4.6  
     4.7 +(** Conversion of a theorem into clauses **)
     4.8 +
     4.9 +fun clausify_rule (A,i) =
    4.10 +  standard
    4.11 +    (make_meta_clause
    4.12 +      (List.nth(ResAxioms.cnf_axiom A,i-1)));
    4.13 +
    4.14 +fun clausify_syntax i (x, A) = (x, clausify_rule (A,i));
    4.15 +
    4.16 +fun CLAUSIFY x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x;
    4.17 +
    4.18 +
    4.19  (** theory setup **)
    4.20  
    4.21  val setup =
    4.22 @@ -170,7 +182,8 @@
    4.23       [("BINARY", (BINARY_global, BINARY_local), "binary resolution"),
    4.24        ("PARAMOD", (PARAMOD_global, PARAMOD_local), "paramodulation"),
    4.25        ("DEMOD", (DEMOD_global, DEMOD_local), "demodulation"),
    4.26 -      ("FACTOR", (FACTOR, FACTOR), "factoring")]];
    4.27 +      ("FACTOR", (FACTOR, FACTOR), "factoring"),
    4.28 +      ("CLAUSIFY", (CLAUSIFY, CLAUSIFY), "conversion to clauses")]];
    4.29  
    4.30  end
    4.31  end
     5.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Dec 02 10:36:20 2004 +0100
     5.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Dec 02 11:09:19 2004 +0100
     5.3 @@ -122,8 +122,6 @@
     5.4  
     5.5  (* some lemmas *)
     5.6  
     5.7 -(* TO BE FIXED: the names of these lemmas should be made local, to avoid confusion with external global lemmas. *)
     5.8 -
     5.9  Goal "(P==True) ==> P";
    5.10  by(Blast_tac 1);
    5.11  qed "Eq_TrueD1";
    5.12 @@ -132,7 +130,6 @@
    5.13  by(Blast_tac 1);
    5.14  qed "Eq_TrueD2";
    5.15  
    5.16 -
    5.17  Goal "(P==False) ==> ~P";
    5.18  by(Blast_tac 1);
    5.19  qed "Eq_FalseD1";
    5.20 @@ -141,50 +138,22 @@
    5.21  by(Blast_tac 1);
    5.22  qed "Eq_FalseD2";
    5.23  
    5.24 -Goal "(P | True) == True";
    5.25 -by(Simp_tac 1);
    5.26 -qed "s1";
    5.27 -
    5.28 -Goal "(True | P) == True";
    5.29 -by(Simp_tac 1);
    5.30 -qed "s2";
    5.31 +local 
    5.32  
    5.33 -Goal "(P & True) == P";
    5.34 -by(Simp_tac 1);
    5.35 -qed "s3";
    5.36 -
    5.37 -Goal "(True & P) == P";
    5.38 -by(Simp_tac 1);
    5.39 -qed "s4";
    5.40 -
    5.41 -Goal "(False | P) == P";
    5.42 -by(Simp_tac 1);
    5.43 -qed "s5";
    5.44 -
    5.45 +    fun prove s = prove_goal (the_context()) s (fn _ => [Simp_tac 1]);
    5.46  
    5.47 -Goal "(P | False) == P";
    5.48 -by(Simp_tac 1);
    5.49 -qed "s6";
    5.50 -
    5.51 -Goal "(False & P) == False";
    5.52 -by(Simp_tac 1);
    5.53 -qed "s7";
    5.54 -
    5.55 -Goal "(P & False) == False";
    5.56 -by(Simp_tac 1);
    5.57 -qed "s8";
    5.58 +val small_simps = 
    5.59 +  map prove 
    5.60 +   ["(P | True) == True", "(True | P) == True",
    5.61 +    "(P & True) == P", "(True & P) == P",
    5.62 +    "(False | P) == P", "(P | False) == P",
    5.63 +    "(False & P) == False", "(P & False) == False",
    5.64 +    "~True == False", "~False == True"];
    5.65 +in
    5.66  
    5.67 -Goal "~True == False";
    5.68 -by(Simp_tac 1);
    5.69 -qed "s9";
    5.70 +val small_simpset = empty_ss addsimps small_simps
    5.71  
    5.72 -Goal "~False == True";
    5.73 -by(Simp_tac 1);
    5.74 -qed "s10";
    5.75 -
    5.76 -
    5.77 -val small_simpset = empty_ss addsimps [s1,s2,s3,s4,s5,s6,s7,s8,s9,s10];
    5.78 -
    5.79 +end;
    5.80  
    5.81  
    5.82  signature RES_AXIOMS =
    5.83 @@ -261,8 +230,13 @@
    5.84  
    5.85  
    5.86  
    5.87 -(* transfer a theorem in to theory Main.thy if it is not already inside Main.thy *)
    5.88 -fun transfer_to_Main thm = transfer Main.thy thm handle THM _ => thm;
    5.89 +(*Transfer a theorem in to theory Hilbert_Choice.thy if it is not already
    5.90 +  inside that theory -- because it's needed for Skolemization *)
    5.91 +
    5.92 +val hc_thy = ThyInfo.get_theory"Hilbert_Choice";
    5.93 +
    5.94 +fun transfer_to_Hilbert_Choice thm =
    5.95 +    transfer hc_thy thm handle THM _ => thm;
    5.96  
    5.97  (* remove "True" clause *)
    5.98  fun rm_redundant_cls [] = []
    5.99 @@ -275,7 +249,7 @@
   5.100  
   5.101  (* transform an Isabelle thm into CNF *)
   5.102  fun cnf_axiom thm =
   5.103 -    let val thm' = transfer_to_Main thm
   5.104 +    let val thm' = transfer_to_Hilbert_Choice thm
   5.105  	val thm'' = if (is_elimR thm') then (cnf_elim thm')
   5.106  		    else (if (is_introR thm') then cnf_intro thm' else cnf_rule thm')
   5.107      in