--- 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]));
--- 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 ***)
--- 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 **)
--- 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)";
--- 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";
--- 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);
--- 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);
--- 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)";
+