src/HOL/NatDef.ML
changeset 2935 998cb95fdd43
parent 2922 580647a879cf
child 3023 01364e2f30ad
     1.1 --- a/src/HOL/NatDef.ML	Fri Apr 11 11:33:51 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Fri Apr 11 15:21:36 1997 +0200
     1.3 @@ -278,7 +278,7 @@
     1.4  qed "less_SucE";
     1.5  
     1.6  goal thy "(m < Suc(n)) = (m < n | m = n)";
     1.7 -by (fast_tac (!claset addEs [less_trans, less_SucE]) 1);
     1.8 +by (blast_tac (!claset addSEs [less_SucE] addIs [less_trans]) 1);
     1.9  qed "less_Suc_eq";
    1.10  
    1.11  val prems = goal thy "m<n ==> n ~= 0";
    1.12 @@ -348,18 +348,18 @@
    1.13  by (nat_ind_tac "n" 1);
    1.14  by (rtac (refl RS disjI1 RS disjI2) 1);
    1.15  by (rtac (zero_less_Suc RS disjI1) 1);
    1.16 -by (fast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1);
    1.17 +by (blast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1);
    1.18  qed "less_linear";
    1.19  
    1.20  qed_goal "nat_less_cases" thy 
    1.21     "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"
    1.22 -( fn prems =>
    1.23 +( fn [major,eqCase,lessCase] =>
    1.24          [
    1.25 -        (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
    1.26 +        (rtac (less_linear RS disjE) 1),
    1.27          (etac disjE 2),
    1.28 -        (etac (hd (tl (tl prems))) 1),
    1.29 -        (etac (sym RS hd (tl prems)) 1),
    1.30 -        (etac (hd prems) 1)
    1.31 +        (etac lessCase 1),
    1.32 +        (etac (sym RS eqCase) 1),
    1.33 +        (etac major 1)
    1.34          ]);
    1.35  
    1.36  (*Can be used with less_Suc_eq to get n=m | n<m *)
    1.37 @@ -511,19 +511,19 @@
    1.38  
    1.39  val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
    1.40  by (dtac le_imp_less_or_eq 1);
    1.41 -by (fast_tac (!claset addIs [less_trans]) 1);
    1.42 +by (blast_tac (!claset addIs [less_trans]) 1);
    1.43  qed "le_less_trans";
    1.44  
    1.45  goal thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
    1.46  by (dtac le_imp_less_or_eq 1);
    1.47 -by (fast_tac (!claset addIs [less_trans]) 1);
    1.48 +by (blast_tac (!claset addIs [less_trans]) 1);
    1.49  qed "less_le_trans";
    1.50  
    1.51  goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
    1.52  by (EVERY1[dtac le_imp_less_or_eq, 
    1.53  	   dtac le_imp_less_or_eq,
    1.54  	   rtac less_or_eq_imp_le, 
    1.55 -	   fast_tac (!claset addIs [less_trans])]);
    1.56 +	   blast_tac (!claset addIs [less_trans])]);
    1.57  qed "le_trans";
    1.58  
    1.59  goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
    1.60 @@ -634,9 +634,9 @@
    1.61    (fn _ => [etac swap2 1, etac leD 1]);
    1.62  val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
    1.63    (fn _ => [etac less_SucE 1,
    1.64 -            fast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
    1.65 +            blast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
    1.66                                addDs [less_trans_Suc]) 1,
    1.67 -            atac 1]);
    1.68 +            assume_tac 1]);
    1.69  val leD = le_eq_less_Suc RS iffD1;
    1.70  val not_lessD = nat_leI RS leD;
    1.71  val not_leD = not_leE