# HG changeset patch
# User paulson
# Date 1107443179 -3600
# Node ID 50fde6f04e4c3818bf5e6df6d25961cd61f26747
# Parent  b09b68746eb6d493db17b93a52f9a7e8eb35cb33
new treatment of demodulation in proof reconstruction

diff -r b09b68746eb6 -r 50fde6f04e4c src/HOL/Tools/reconstruction.ML
--- a/src/HOL/Tools/reconstruction.ML	Thu Feb 03 04:09:52 2005 +0100
+++ b/src/HOL/Tools/reconstruction.ML	Thu Feb 03 16:06:19 2005 +0100
@@ -119,15 +119,15 @@
 
 (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
 
-(*currently identical to paramod_rule: the "match" argument of biresolution cannot be used
-  to prevent instantiation of the rewritten literal, in mod_lit_th: it could only prevent
-  instantiation of eq_lit_th, which we do not want.*)
 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, mod_lit_th)] 1 eqsubst)
-    in negated_asm_of_head newth end
+         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]);
 
 fun demod_syntax ((i, B), j) (x, A) = (x, demod_rule ((A,i), (B,j)));
@@ -161,10 +161,7 @@
       	        	  end;
 
 in
-fun clausify_rule (A,i) =
-  standard
-    (make_meta_clause
-      (List.nth(memo_cnf A,i)))
+fun clausify_rule (A,i) = make_meta_clause (List.nth(memo_cnf A,i))
 end;
 
 fun clausify_syntax i (x, A) = (x, clausify_rule (A,i));
diff -r b09b68746eb6 -r 50fde6f04e4c src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Feb 03 04:09:52 2005 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Feb 03 16:06:19 2005 +0100
@@ -232,19 +232,9 @@
     end;
 
 
-fun isa_cls thm = 
-    let val thm' = skolem_axiom thm 
-    in
-	map standard (make_clauses [thm'])
-    end;
-
+fun isa_cls thm = map zero_var_indexes (make_clauses [skolem_axiom thm])
 
-fun cnf_elim thm = 
-    let val thm' = transform_elim thm;
-    in
-	isa_cls thm'
-    end;
-
+fun cnf_elim thm = isa_cls (transform_elim thm);
 
 val cnf_intro = isa_cls;
 val cnf_rule = isa_cls;	
diff -r b09b68746eb6 -r 50fde6f04e4c src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Feb 03 04:09:52 2005 +0100
+++ b/src/Pure/drule.ML	Thu Feb 03 16:06:19 2005 +0100
@@ -32,6 +32,7 @@
   val forall_elim_vars  : int -> thm -> thm
   val gen_all           : thm -> thm
   val freeze_thaw       : thm -> thm * (thm -> thm)
+  val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
   val implies_elim_list : thm -> thm list -> thm
   val implies_intr_list : cterm list -> thm -> thm
   val instantiate       :
@@ -413,6 +414,30 @@
 (*Convert all Vars in a theorem to Frees.  Also return a function for
   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
   Similar code in type/freeze_thaw*)
+
+fun freeze_thaw_robust th =
+ let val fth = freezeT th
+     val {prop, tpairs, sign, ...} = rep_thm fth
+ in
+   case foldr add_term_vars (prop :: Thm.terms_of_tpairs tpairs, []) of
+       [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
+     | vars =>
+         let fun newName (Var(ix,_), pairs) =
+                   let val v = gensym (string_of_indexname ix)
+                   in  ((ix,v)::pairs)  end;
+             val alist = foldr newName (vars,[])
+             fun mk_inst (Var(v,T)) =
+                 (cterm_of sign (Var(v,T)),
+                  cterm_of sign (Free(the (assoc(alist,v)), T)))
+             val insts = map mk_inst vars
+             fun thaw i th' = (*i is non-negative increment for Var indexes*)
+                 th' |> forall_intr_list (map #2 insts)
+                     |> forall_elim_list (map (Thm.cterm_incr_indexes i o #1) insts)
+         in  (Thm.instantiate ([],insts) fth, thaw)  end
+ end;
+
+(*Basic version of the function above. No option to rename Vars apart in thaw.
+  The Frees created from Vars have nice names.*)
 fun freeze_thaw th =
  let val fth = freezeT th
      val {prop, tpairs, sign, ...} = rep_thm fth
@@ -435,7 +460,6 @@
          in  (Thm.instantiate ([],insts) fth, thaw)  end
  end;
 
-
 (*Rotates a rule's premises to the left by k*)
 val rotate_prems = permute_prems 0;