--- 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));
--- 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;
--- 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;