# HG changeset patch
# User nipkow
# Date 823869678 -3600
# Node ID 240cc98b94a7d5894a44cd79059b35fba1d29354
# Parent  b43cd8a8061f0415f7aee526fccc32ec3d2ca247
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'

diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Feb 09 12:18:02 1996 +0100
+++ b/src/HOL/Arith.ML	Fri Feb 09 13:41:18 1996 +0100
@@ -252,10 +252,7 @@
 val prems = goal Arith.thy "m-n = 0  -->  n-m = 0  -->  m=n";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
-qed "diffs0_imp_equal_lemma";
-
-(*  [| m-n = 0;  n-m = 0 |] ==> m=n  *)
-bind_thm ("diffs0_imp_equal", (diffs0_imp_equal_lemma RS mp RS mp));
+qed_spec_mp "diffs0_imp_equal";
 
 val [prem] = goal Arith.thy "m<n ==> 0<n-m";
 by (rtac (prem RS rev_mp) 1);
@@ -298,11 +295,7 @@
 by (safe_tac HOL_cs);
 by (res_inst_tac [("x","Suc(k)")] exI 1);
 by (Simp_tac 1);
-val less_eq_Suc_add_lemma = result();
-
-(*"m<n ==> ? k. n = Suc(m+k)"*)
-bind_thm ("less_eq_Suc_add", less_eq_Suc_add_lemma RS mp);
-
+qed_spec_mp "less_eq_Suc_add";
 
 goal Arith.thy "n <= ((m + n)::nat)";
 by (nat_ind_tac "m" 1);
@@ -352,8 +345,7 @@
 by (nat_ind_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
-val add_leD1_lemma = result();
-bind_thm ("add_leD1", add_leD1_lemma RS mp);
+qed_spec_mp "add_leD1";
 
 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
 by (safe_tac (HOL_cs addSDs [less_eq_Suc_add]));
diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Fri Feb 09 12:18:02 1996 +0100
+++ b/src/HOL/HOL.ML	Fri Feb 09 13:41:18 1996 +0100
@@ -266,9 +266,32 @@
 (** Standard abbreviations **)
 
 fun stac th = rtac(th RS ssubst);
-fun sstac ths = EVERY' (map stac ths);
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
 
+(** strip proved goal while preserving !-bound var names **)
+
+local
+
+(* work around instantiation bug *)
+val myspec = read_instantiate [("P","?XXX")] spec;
+val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
+val cvx = cterm_of (#sign(rep_thm myspec)) vx;
+val aspec = forall_intr cvx myspec;
+
+fun specf th a =
+  let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
+  in th RS forall_elim ca aspec end;
+
+fun spec_mpf th = case concl_of th of
+                    _ $ (Const("All",_) $ Abs(a,_,_)) => spec_mpf (specf th a)
+                  | _ $ (Const("op -->",_)$_$_) => spec_mpf (th RS mp)
+                  | _ => th
+
+in
+
+fun qed_spec_mp name = bind_thm(name, spec_mpf(result()));
+
+end;
 
 (*** Load simpdata.ML to be able to initialize HOL's simpset ***)
 
diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Feb 09 12:18:02 1996 +0100
+++ b/src/HOL/List.ML	Fri Feb 09 13:41:18 1996 +0100
@@ -158,7 +158,7 @@
 by (rtac allI 1);
 by (nat_ind_tac "n" 1);
 by (ALLGOALS Asm_full_simp_tac);
-bind_thm("nth_map", result() RS spec RS mp);
+qed_spec_mp "nth_map";
 Addsimps [nth_map];
 
 goal List.thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
@@ -169,7 +169,7 @@
 by (rtac allI 1);
 by (nat_ind_tac "n" 1);
 by (ALLGOALS Asm_full_simp_tac);
-bind_thm("list_all_nth", result() RS spec RS mp RS mp);
+qed_spec_mp "list_all_nth";
 
 goal List.thy "!n. n < length xs --> (nth n xs) mem xs";
 by (list.induct_tac "xs" 1);
@@ -182,7 +182,7 @@
 by (Asm_full_simp_tac 1);
 (* case Suc x *)
 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-bind_thm ("nth_mem",result() RS spec RS mp);
+qed_spec_mp "nth_mem";
 Addsimps [nth_mem];
 
 (** drop **)
diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Feb 09 12:18:02 1996 +0100
+++ b/src/HOL/Nat.ML	Fri Feb 09 13:41:18 1996 +0100
@@ -343,7 +343,7 @@
 by(nat_ind_tac "k" 1);
 by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
 by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
-bind_thm("less_trans_Suc",result() RS mp);
+qed_spec_mp "less_trans_Suc";
 
 (*"Less than" is a linear ordering*)
 goal Nat.thy "m<n | m=n | n<(m::nat)";
diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Feb 09 12:18:02 1996 +0100
+++ b/src/HOL/Prod.ML	Fri Feb 09 13:41:18 1996 +0100
@@ -82,7 +82,7 @@
 qed "split_paired_All";
 
 goalw Prod.thy [split_def] "split c (a,b) = c a b";
-by (sstac [fst_conv, snd_conv] 1);
+by (EVERY1[stac fst_conv, stac snd_conv]);
 by (rtac refl 1);
 qed "split";
 
diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Fri Feb 09 12:18:02 1996 +0100
+++ b/src/HOL/Univ.ML	Fri Feb 09 13:41:18 1996 +0100
@@ -256,7 +256,7 @@
 
 
 goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
-by (sstac [Node_K0_I RS Abs_Node_inverse, split] 1);
+by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
 by (rtac Least_equality 1);
 by (rtac refl 1);
 by (etac less_zeroE 1);
diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Fri Feb 09 12:18:02 1996 +0100
+++ b/src/HOL/WF.ML	Fri Feb 09 13:41:18 1996 +0100
@@ -100,8 +100,7 @@
 by (etac wf_induct 1);
 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
 by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
-qed "is_recfun_equal_lemma";
-bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
+qed_spec_mp "is_recfun_equal";
 
 
 val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
@@ -191,7 +190,7 @@
 by (rtac refl 2);
 by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
 by (strip_tac 1);
-by (res_inst_tac [("r2","r^+")] (is_recfun_equal_lemma RS mp RS mp) 1);
+by (res_inst_tac [("r","r^+")] is_recfun_equal 1);
 by (atac 1);
 by (rtac trans_trancl 1);
 by (rtac unfold_the_recfun 1);
diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Feb 09 12:18:02 1996 +0100
+++ b/src/HOL/simpdata.ML	Fri Feb 09 13:41:18 1996 +0100
@@ -173,3 +173,7 @@
 
 prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)";
 prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)";
+
+prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
+prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
+