src/HOL/Arith.ML
changeset 3457 a8ab7c64817c
parent 3396 aa74c71c3982
child 3484 1e93eb09ebb9
     1.1 --- a/src/HOL/Arith.ML	Mon Jun 23 10:35:49 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Jun 23 10:42:03 1997 +0200
     1.3 @@ -12,11 +12,11 @@
     1.4  (*** Basic rewrite rules for the arithmetic operators ***)
     1.5  
     1.6  goalw Arith.thy [pred_def] "pred 0 = 0";
     1.7 -by(Simp_tac 1);
     1.8 +by (Simp_tac 1);
     1.9  qed "pred_0";
    1.10  
    1.11  goalw Arith.thy [pred_def] "pred(Suc n) = n";
    1.12 -by(Simp_tac 1);
    1.13 +by (Simp_tac 1);
    1.14  qed "pred_Suc";
    1.15  
    1.16  Addsimps [pred_0,pred_Suc];
    1.17 @@ -175,8 +175,8 @@
    1.18  qed "add_lessD1";
    1.19  
    1.20  goal Arith.thy "!!i::nat. ~ (i+j < i)";
    1.21 -br notI 1;
    1.22 -be (add_lessD1 RS less_irrefl) 1;
    1.23 +by (rtac notI 1);
    1.24 +by (etac (add_lessD1 RS less_irrefl) 1);
    1.25  qed "not_add_less1";
    1.26  
    1.27  goal Arith.thy "!!i::nat. ~ (j+i < i)";
    1.28 @@ -506,7 +506,7 @@
    1.29  qed "mult_less_mono2";
    1.30  
    1.31  goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
    1.32 -bd mult_less_mono2 1;
    1.33 +by (dtac mult_less_mono2 1);
    1.34  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [mult_commute])));
    1.35  qed "mult_less_mono1";
    1.36  
    1.37 @@ -531,21 +531,21 @@
    1.38  qed "mult_less_cancel2";
    1.39  
    1.40  goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";
    1.41 -bd mult_less_cancel2 1;
    1.42 +by (dtac mult_less_cancel2 1);
    1.43  by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
    1.44  qed "mult_less_cancel1";
    1.45  Addsimps [mult_less_cancel1, mult_less_cancel2];
    1.46  
    1.47  goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
    1.48  by (cut_facts_tac [less_linear] 1);
    1.49 -by(Step_tac 1);
    1.50 -ba 2;
    1.51 +by (Step_tac 1);
    1.52 +by (assume_tac 2);
    1.53  by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
    1.54  by (ALLGOALS Asm_full_simp_tac);
    1.55  qed "mult_cancel2";
    1.56  
    1.57  goal Arith.thy "!!k. 0<k ==> (k*m = k*n) = (m=n)";
    1.58 -bd mult_cancel2 1;
    1.59 +by (dtac mult_cancel2 1);
    1.60  by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
    1.61  qed "mult_cancel1";
    1.62  Addsimps [mult_cancel1, mult_cancel2];
    1.63 @@ -574,13 +574,13 @@
    1.64  qed "diff_less_mono";
    1.65  
    1.66  goal Arith.thy "!! a b c::nat. a+b < c ==> a < c-b";
    1.67 -bd diff_less_mono 1;
    1.68 -br le_add2 1;
    1.69 +by (dtac diff_less_mono 1);
    1.70 +by (rtac le_add2 1);
    1.71  by (Asm_full_simp_tac 1);
    1.72  qed "add_less_imp_less_diff";
    1.73  
    1.74  goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)";
    1.75 -br Suc_diff_n 1;
    1.76 +by (rtac Suc_diff_n 1);
    1.77  by (asm_full_simp_tac (!simpset addsimps [le_eq_less_Suc]) 1);
    1.78  qed "Suc_diff_le";
    1.79  
    1.80 @@ -597,7 +597,7 @@
    1.81  Addsimps [diff_diff_cancel];
    1.82  
    1.83  goal Arith.thy "!!k::nat. k <= n ==> m <= n + m - k";
    1.84 -be rev_mp 1;
    1.85 +by (etac rev_mp 1);
    1.86  by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
    1.87  by (Simp_tac 1);
    1.88  by (simp_tac (!simpset addsimps [less_add_Suc2, less_imp_le]) 1);