Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
authornipkow
Fri Feb 09 13:41:18 1996 +0100 (1996-02-09)
changeset 1485240cc98b94a7
parent 1484 b43cd8a8061f
child 1486 7b95d7b49f7a
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
src/HOL/Arith.ML
src/HOL/HOL.ML
src/HOL/List.ML
src/HOL/Nat.ML
src/HOL/Prod.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Feb 09 12:18:02 1996 +0100
     1.2 +++ b/src/HOL/Arith.ML	Fri Feb 09 13:41:18 1996 +0100
     1.3 @@ -252,10 +252,7 @@
     1.4  val prems = goal Arith.thy "m-n = 0  -->  n-m = 0  -->  m=n";
     1.5  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
     1.6  by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
     1.7 -qed "diffs0_imp_equal_lemma";
     1.8 -
     1.9 -(*  [| m-n = 0;  n-m = 0 |] ==> m=n  *)
    1.10 -bind_thm ("diffs0_imp_equal", (diffs0_imp_equal_lemma RS mp RS mp));
    1.11 +qed_spec_mp "diffs0_imp_equal";
    1.12  
    1.13  val [prem] = goal Arith.thy "m<n ==> 0<n-m";
    1.14  by (rtac (prem RS rev_mp) 1);
    1.15 @@ -298,11 +295,7 @@
    1.16  by (safe_tac HOL_cs);
    1.17  by (res_inst_tac [("x","Suc(k)")] exI 1);
    1.18  by (Simp_tac 1);
    1.19 -val less_eq_Suc_add_lemma = result();
    1.20 -
    1.21 -(*"m<n ==> ? k. n = Suc(m+k)"*)
    1.22 -bind_thm ("less_eq_Suc_add", less_eq_Suc_add_lemma RS mp);
    1.23 -
    1.24 +qed_spec_mp "less_eq_Suc_add";
    1.25  
    1.26  goal Arith.thy "n <= ((m + n)::nat)";
    1.27  by (nat_ind_tac "m" 1);
    1.28 @@ -352,8 +345,7 @@
    1.29  by (nat_ind_tac "k" 1);
    1.30  by (ALLGOALS Asm_simp_tac);
    1.31  by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
    1.32 -val add_leD1_lemma = result();
    1.33 -bind_thm ("add_leD1", add_leD1_lemma RS mp);
    1.34 +qed_spec_mp "add_leD1";
    1.35  
    1.36  goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
    1.37  by (safe_tac (HOL_cs addSDs [less_eq_Suc_add]));
     2.1 --- a/src/HOL/HOL.ML	Fri Feb 09 12:18:02 1996 +0100
     2.2 +++ b/src/HOL/HOL.ML	Fri Feb 09 13:41:18 1996 +0100
     2.3 @@ -266,9 +266,32 @@
     2.4  (** Standard abbreviations **)
     2.5  
     2.6  fun stac th = rtac(th RS ssubst);
     2.7 -fun sstac ths = EVERY' (map stac ths);
     2.8  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
     2.9  
    2.10 +(** strip proved goal while preserving !-bound var names **)
    2.11 +
    2.12 +local
    2.13 +
    2.14 +(* work around instantiation bug *)
    2.15 +val myspec = read_instantiate [("P","?XXX")] spec;
    2.16 +val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
    2.17 +val cvx = cterm_of (#sign(rep_thm myspec)) vx;
    2.18 +val aspec = forall_intr cvx myspec;
    2.19 +
    2.20 +fun specf th a =
    2.21 +  let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
    2.22 +  in th RS forall_elim ca aspec end;
    2.23 +
    2.24 +fun spec_mpf th = case concl_of th of
    2.25 +                    _ $ (Const("All",_) $ Abs(a,_,_)) => spec_mpf (specf th a)
    2.26 +                  | _ $ (Const("op -->",_)$_$_) => spec_mpf (th RS mp)
    2.27 +                  | _ => th
    2.28 +
    2.29 +in
    2.30 +
    2.31 +fun qed_spec_mp name = bind_thm(name, spec_mpf(result()));
    2.32 +
    2.33 +end;
    2.34  
    2.35  (*** Load simpdata.ML to be able to initialize HOL's simpset ***)
    2.36  
     3.1 --- a/src/HOL/List.ML	Fri Feb 09 12:18:02 1996 +0100
     3.2 +++ b/src/HOL/List.ML	Fri Feb 09 13:41:18 1996 +0100
     3.3 @@ -158,7 +158,7 @@
     3.4  by (rtac allI 1);
     3.5  by (nat_ind_tac "n" 1);
     3.6  by (ALLGOALS Asm_full_simp_tac);
     3.7 -bind_thm("nth_map", result() RS spec RS mp);
     3.8 +qed_spec_mp "nth_map";
     3.9  Addsimps [nth_map];
    3.10  
    3.11  goal List.thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
    3.12 @@ -169,7 +169,7 @@
    3.13  by (rtac allI 1);
    3.14  by (nat_ind_tac "n" 1);
    3.15  by (ALLGOALS Asm_full_simp_tac);
    3.16 -bind_thm("list_all_nth", result() RS spec RS mp RS mp);
    3.17 +qed_spec_mp "list_all_nth";
    3.18  
    3.19  goal List.thy "!n. n < length xs --> (nth n xs) mem xs";
    3.20  by (list.induct_tac "xs" 1);
    3.21 @@ -182,7 +182,7 @@
    3.22  by (Asm_full_simp_tac 1);
    3.23  (* case Suc x *)
    3.24  by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    3.25 -bind_thm ("nth_mem",result() RS spec RS mp);
    3.26 +qed_spec_mp "nth_mem";
    3.27  Addsimps [nth_mem];
    3.28  
    3.29  (** drop **)
     4.1 --- a/src/HOL/Nat.ML	Fri Feb 09 12:18:02 1996 +0100
     4.2 +++ b/src/HOL/Nat.ML	Fri Feb 09 13:41:18 1996 +0100
     4.3 @@ -343,7 +343,7 @@
     4.4  by(nat_ind_tac "k" 1);
     4.5  by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
     4.6  by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
     4.7 -bind_thm("less_trans_Suc",result() RS mp);
     4.8 +qed_spec_mp "less_trans_Suc";
     4.9  
    4.10  (*"Less than" is a linear ordering*)
    4.11  goal Nat.thy "m<n | m=n | n<(m::nat)";
     5.1 --- a/src/HOL/Prod.ML	Fri Feb 09 12:18:02 1996 +0100
     5.2 +++ b/src/HOL/Prod.ML	Fri Feb 09 13:41:18 1996 +0100
     5.3 @@ -82,7 +82,7 @@
     5.4  qed "split_paired_All";
     5.5  
     5.6  goalw Prod.thy [split_def] "split c (a,b) = c a b";
     5.7 -by (sstac [fst_conv, snd_conv] 1);
     5.8 +by (EVERY1[stac fst_conv, stac snd_conv]);
     5.9  by (rtac refl 1);
    5.10  qed "split";
    5.11  
     6.1 --- a/src/HOL/Univ.ML	Fri Feb 09 12:18:02 1996 +0100
     6.2 +++ b/src/HOL/Univ.ML	Fri Feb 09 13:41:18 1996 +0100
     6.3 @@ -256,7 +256,7 @@
     6.4  
     6.5  
     6.6  goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
     6.7 -by (sstac [Node_K0_I RS Abs_Node_inverse, split] 1);
     6.8 +by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
     6.9  by (rtac Least_equality 1);
    6.10  by (rtac refl 1);
    6.11  by (etac less_zeroE 1);
     7.1 --- a/src/HOL/WF.ML	Fri Feb 09 12:18:02 1996 +0100
     7.2 +++ b/src/HOL/WF.ML	Fri Feb 09 13:41:18 1996 +0100
     7.3 @@ -100,8 +100,7 @@
     7.4  by (etac wf_induct 1);
     7.5  by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
     7.6  by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
     7.7 -qed "is_recfun_equal_lemma";
     7.8 -bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
     7.9 +qed_spec_mp "is_recfun_equal";
    7.10  
    7.11  
    7.12  val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
    7.13 @@ -191,7 +190,7 @@
    7.14  by (rtac refl 2);
    7.15  by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
    7.16  by (strip_tac 1);
    7.17 -by (res_inst_tac [("r2","r^+")] (is_recfun_equal_lemma RS mp RS mp) 1);
    7.18 +by (res_inst_tac [("r","r^+")] is_recfun_equal 1);
    7.19  by (atac 1);
    7.20  by (rtac trans_trancl 1);
    7.21  by (rtac unfold_the_recfun 1);
     8.1 --- a/src/HOL/simpdata.ML	Fri Feb 09 12:18:02 1996 +0100
     8.2 +++ b/src/HOL/simpdata.ML	Fri Feb 09 13:41:18 1996 +0100
     8.3 @@ -173,3 +173,7 @@
     8.4  
     8.5  prove "conj_disj_distribL" "(P&(Q|R)) = (P&Q | P&R)";
     8.6  prove "conj_disj_distribR" "((P|Q)&R) = (P&R | Q&R)";
     8.7 +
     8.8 +prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
     8.9 +prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
    8.10 +