src/HOL/Arith.ML
changeset 2922 580647a879cf
parent 2682 13cdbf95ed92
child 3234 503f4c8c29eb
     1.1 --- a/src/HOL/Arith.ML	Wed Apr 09 12:31:11 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Wed Apr 09 12:32:04 1997 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  by (etac rev_mp 1);
     1.5  by (nat_ind_tac "k" 1);
     1.6  by (Simp_tac 1);
     1.7 -by (Fast_tac 1);
     1.8 +by (Blast_tac 1);
     1.9  val lemma = result();
    1.10  
    1.11  (* [| 0 < k; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
    1.12 @@ -247,7 +247,7 @@
    1.13  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
    1.14  goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
    1.15  by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
    1.16 -by (Fast_tac 1);
    1.17 +by (Blast_tac 1);
    1.18  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.19  by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
    1.20  qed "diff_less";
    1.21 @@ -335,7 +335,7 @@
    1.22  
    1.23  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
    1.24  by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
    1.25 -by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Fast_tac));
    1.26 +by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Blast_tac));
    1.27  qed "zero_induct_lemma";
    1.28  
    1.29  val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
    1.30 @@ -385,7 +385,7 @@
    1.31  by (subgoal_tac "k mod 2 < 2" 1);
    1.32  by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
    1.33  by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.34 -by (Fast_tac 1);
    1.35 +by (Blast_tac 1);
    1.36  qed "mod2_cases";
    1.37  
    1.38  goal thy "Suc(Suc(m)) mod 2 = m mod 2";
    1.39 @@ -452,7 +452,7 @@
    1.40  by (etac rev_mp 1);
    1.41  by (nat_ind_tac "j" 1);
    1.42  by (ALLGOALS Asm_simp_tac);
    1.43 -by (fast_tac (!claset addDs [Suc_lessD]) 1);
    1.44 +by (blast_tac (!claset addDs [Suc_lessD]) 1);
    1.45  qed "add_lessD1";
    1.46  
    1.47  goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
    1.48 @@ -468,7 +468,7 @@
    1.49  goal Arith.thy "m+k<=n --> m<=(n::nat)";
    1.50  by (nat_ind_tac "k" 1);
    1.51  by (ALLGOALS Asm_simp_tac);
    1.52 -by (fast_tac (!claset addDs [Suc_leD]) 1);
    1.53 +by (blast_tac (!claset addDs [Suc_leD]) 1);
    1.54  qed_spec_mp "add_leD1";
    1.55  
    1.56  goal Arith.thy "!!n::nat. m+k<=n ==> k<=n";
    1.57 @@ -477,7 +477,7 @@
    1.58  qed_spec_mp "add_leD2";
    1.59  
    1.60  goal Arith.thy "!!n::nat. m+k<=n ==> m<=n & k<=n";
    1.61 -by (fast_tac (!claset addDs [add_leD1, add_leD2]) 1);
    1.62 +by (blast_tac (!claset addDs [add_leD1, add_leD2]) 1);
    1.63  bind_thm ("add_leE", result() RS conjE);
    1.64  
    1.65  goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
    1.66 @@ -513,7 +513,7 @@
    1.67  \     |] ==> f(i) <= (f(j)::nat)";
    1.68  by (cut_facts_tac [le] 1);
    1.69  by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
    1.70 -by (fast_tac (!claset addSIs [lt_mono]) 1);
    1.71 +by (blast_tac (!claset addSIs [lt_mono]) 1);
    1.72  qed "less_mono_imp_le_mono";
    1.73  
    1.74  (*non-strict, in 1st argument*)