# HG changeset patch
# User paulson
# Date 1107538546 -3600
# Node ID 419dc5ffe8bc797dcd4b4f48b17caa1b467b3a3f
# Parent  3988e90613d4455de70feb0bc04662d2fa35eca9
clausification and proof reconstruction

diff -r 3988e90613d4 -r 419dc5ffe8bc src/HOL/Tools/reconstruction.ML
--- a/src/HOL/Tools/reconstruction.ML	Fri Feb 04 18:34:34 2005 +0100
+++ b/src/HOL/Tools/reconstruction.ML	Fri Feb 04 18:35:46 2005 +0100
@@ -101,12 +101,13 @@
   as the second to last premises of the result.*)
 val rev_subst = rotate_prems 1 subst;
 
-fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
+fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
     let  val eq_lit_th = select_literal (lit1+1) cl1
          val mod_lit_th = select_literal (lit2+1) cl2
          val eqsubst = eq_lit_th RSN (2,rev_subst)
          val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
-    in negated_asm_of_head newth end;
+         val newth' = Seq.hd (flexflex_rule newth)
+    in negated_asm_of_head newth' end;
 
 
 fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j)));
@@ -121,14 +122,13 @@
 
 fun demod_rule ((cl1, lit1), (cl2 , lit2)) = 
     let  val eq_lit_th = select_literal (lit1+1) cl1
-         val offset = #maxidx(rep_thm eq_lit_th) + 1
-	     (*ensures "renaming apart" even when Vars are frozen*)
          val mod_lit_th = select_literal (lit2+1) cl2
 	 val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
          val eqsubst = eq_lit_th RSN (2,rev_subst)
          val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst)
-    in negated_asm_of_head (thaw offset newth) end
-    handle _ => raise THM ("select_literal", lit1, [cl1,cl2]);
+         val offset = #maxidx(rep_thm newth) + 1
+	                  (*ensures "renaming apart" even when Vars are frozen*)
+    in negated_asm_of_head (thaw offset newth) end;
 
 fun demod_syntax ((i, B), j) (x, A) = (x, demod_rule ((A,i), (B,j)));
 
@@ -147,21 +147,21 @@
 
   fun memo_cnf th =
     case Thm.name_of_thm th of
-        "" => ResAxioms.cnf_axiom th (*no name, so can't cache*)
+        "" => ResAxioms.meta_cnf_axiom th (*no name, so can't cache*)
       | s  => case Symtab.lookup (!cc,s) of
       	        None => 
-      	        	let val cls = ResAxioms.cnf_axiom th
+      	        	let val cls = ResAxioms.meta_cnf_axiom th
       	        	in  cc := Symtab.update ((s, (th,cls)), !cc); cls
       	        	end
       	      | Some(th',cls) =>
       	      	    if eq_thm(th,th') then cls
       	      	    else (*New theorem stored under the same name? Possible??*)
-      	      	      let val cls = ResAxioms.cnf_axiom th
+      	      	      let val cls = ResAxioms.meta_cnf_axiom th
       	        	  in  cc := Symtab.update ((s, (th,cls)), !cc); cls
       	        	  end;
 
 in
-fun clausify_rule (A,i) = make_meta_clause (List.nth(memo_cnf A,i))
+fun clausify_rule (A,i) = List.nth (memo_cnf A,i)
 end;
 
 fun clausify_syntax i (x, A) = (x, clausify_rule (A,i));
diff -r 3988e90613d4 -r 419dc5ffe8bc src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Feb 04 18:34:34 2005 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Fri Feb 04 18:35:46 2005 +0100
@@ -182,8 +182,8 @@
 
 val clausify_axiom : Thm.thm -> ResClause.clause list
 val cnf_axiom : Thm.thm -> Thm.thm list
+val meta_cnf_axiom : Thm.thm -> Thm.thm list
 val cnf_elim : Thm.thm -> Thm.thm list
-val cnf_intro : Thm.thm -> Thm.thm list
 val cnf_rule : Thm.thm -> Thm.thm list
 val cnf_classical_rules_thy : Theory.theory -> Thm.thm list list * Thm.thm list
 val clausify_classical_rules_thy 
@@ -232,17 +232,13 @@
     end;
 
 
-fun isa_cls thm = map zero_var_indexes (make_clauses [skolem_axiom thm])
+fun isa_cls thm = make_clauses [skolem_axiom thm]
 
 fun cnf_elim thm = isa_cls (transform_elim thm);
 
-val cnf_intro = isa_cls;
 val cnf_rule = isa_cls;	
 
 
-fun is_introR thm = true;
-
-
 
 (*Transfer a theorem in to theory Reconstruction.thy if it is not already
   inside that theory -- because it's needed for Skolemization *)
@@ -264,12 +260,13 @@
 (* transform an Isabelle thm into CNF *)
 fun cnf_axiom thm =
     let val thm' = transfer_to_Reconstruction thm
-	val thm'' = if (is_elimR thm') then (cnf_elim thm')
-		    else (if (is_introR thm') then cnf_intro thm' else cnf_rule thm')
+	val thm'' = if (is_elimR thm') then (cnf_elim thm')  else cnf_rule thm'
     in
 	rm_redundant_cls thm''
     end;
 
+fun meta_cnf_axiom thm = map (zero_var_indexes o make_meta_clause) (cnf_axiom thm);
+
 
 (* changed: with one extra case added *)
 fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars