src/HOL/Arith.ML
changeset 5143 b94cd208f073
parent 5078 7b5ea59c0275
child 5183 89f162de39cf
     1.1 --- a/src/HOL/Arith.ML	Tue Jul 14 13:33:12 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Wed Jul 15 10:15:13 1998 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  (* Could be (and is, below) generalized in various ways;
     1.5     However, none of the generalizations are currently in the simpset,
     1.6     and I dread to think what happens if I put them in *)
     1.7 -Goal "!!n. 0 < n ==> Suc(n-1) = n";
     1.8 +Goal "0 < n ==> Suc(n-1) = n";
     1.9  by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
    1.10  qed "Suc_pred";
    1.11  Addsimps [Suc_pred];
    1.12 @@ -111,7 +111,7 @@
    1.13  Addsimps [pred_add_is_0];
    1.14  
    1.15  (* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
    1.16 -Goal "!!n. 0<n ==> m + (n-1) = (m+n)-1";
    1.17 +Goal "0<n ==> m + (n-1) = (m+n)-1";
    1.18  by (exhaust_tac "m" 1);
    1.19  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    1.20                                        addsplits [split_nat_case])));
    1.21 @@ -128,7 +128,7 @@
    1.22  (**** Additional theorems about "less than" ****)
    1.23  
    1.24  (*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
    1.25 -Goal "!!m. m<n --> (? k. n=Suc(m+k))";
    1.26 +Goal "m<n --> (? k. n=Suc(m+k))";
    1.27  by (induct_tac "n" 1);
    1.28  by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
    1.29  by (blast_tac (claset() addSEs [less_SucE] 
    1.30 @@ -162,7 +162,7 @@
    1.31  (*"i < j ==> i < m+j"*)
    1.32  bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
    1.33  
    1.34 -Goal "!!i. i+j < (k::nat) ==> i<k";
    1.35 +Goal "i+j < (k::nat) ==> i<k";
    1.36  by (etac rev_mp 1);
    1.37  by (induct_tac "j" 1);
    1.38  by (ALLGOALS Asm_simp_tac);
    1.39 @@ -328,11 +328,11 @@
    1.40  by (ALLGOALS Asm_simp_tac);
    1.41  qed_spec_mp "add_diff_inverse";
    1.42  
    1.43 -Goal "!!m. n<=m ==> n+(m-n) = (m::nat)";
    1.44 +Goal "n<=m ==> n+(m-n) = (m::nat)";
    1.45  by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
    1.46  qed "le_add_diff_inverse";
    1.47  
    1.48 -Goal "!!m. n<=m ==> (m-n)+n = (m::nat)";
    1.49 +Goal "n<=m ==> (m-n)+n = (m::nat)";
    1.50  by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
    1.51  qed "le_add_diff_inverse2";
    1.52  
    1.53 @@ -372,7 +372,7 @@
    1.54  qed "Suc_diff_diff";
    1.55  Addsimps [Suc_diff_diff];
    1.56  
    1.57 -Goal "!!n. 0<n ==> n - Suc i < n";
    1.58 +Goal "0<n ==> n - Suc i < n";
    1.59  by (res_inst_tac [("n","n")] natE 1);
    1.60  by Safe_tac;
    1.61  by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
    1.62 @@ -557,13 +557,13 @@
    1.63  qed "mult_eq_1_iff";
    1.64  Addsimps [mult_eq_1_iff];
    1.65  
    1.66 -Goal "!!k. 0<k ==> (m*k < n*k) = (m<n)";
    1.67 +Goal "0<k ==> (m*k < n*k) = (m<n)";
    1.68  by (safe_tac (claset() addSIs [mult_less_mono1]));
    1.69  by (cut_facts_tac [less_linear] 1);
    1.70  by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
    1.71  qed "mult_less_cancel2";
    1.72  
    1.73 -Goal "!!k. 0<k ==> (k*m < k*n) = (m<n)";
    1.74 +Goal "0<k ==> (k*m < k*n) = (m<n)";
    1.75  by (dtac mult_less_cancel2 1);
    1.76  by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
    1.77  qed "mult_less_cancel1";
    1.78 @@ -579,7 +579,7 @@
    1.79  by (rtac Suc_mult_less_cancel1 1);
    1.80  qed "Suc_mult_le_cancel1";
    1.81  
    1.82 -Goal "!!k. 0<k ==> (m*k = n*k) = (m=n)";
    1.83 +Goal "0<k ==> (m*k = n*k) = (m=n)";
    1.84  by (cut_facts_tac [less_linear] 1);
    1.85  by Safe_tac;
    1.86  by (assume_tac 2);
    1.87 @@ -587,7 +587,7 @@
    1.88  by (ALLGOALS Asm_full_simp_tac);
    1.89  qed "mult_cancel2";
    1.90  
    1.91 -Goal "!!k. 0<k ==> (k*m = k*n) = (m=n)";
    1.92 +Goal "0<k ==> (k*m = k*n) = (m=n)";
    1.93  by (dtac mult_cancel2 1);
    1.94  by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
    1.95  qed "mult_cancel1";
    1.96 @@ -601,7 +601,7 @@
    1.97  
    1.98  (** Lemma for gcd **)
    1.99  
   1.100 -Goal "!!m n. m = m*n ==> n=1 | m=0";
   1.101 +Goal "m = m*n ==> n=1 | m=0";
   1.102  by (dtac sym 1);
   1.103  by (rtac disjCI 1);
   1.104  by (rtac nat_less_cases 1 THEN assume_tac 2);
   1.105 @@ -626,11 +626,11 @@
   1.106  by (Asm_full_simp_tac 1);
   1.107  qed "add_less_imp_less_diff";
   1.108  
   1.109 -Goal "!! n. n <= m ==> Suc m - n = Suc (m - n)";
   1.110 +Goal "n <= m ==> Suc m - n = Suc (m - n)";
   1.111  by (asm_full_simp_tac (simpset() addsimps [Suc_diff_n, le_eq_less_Suc]) 1);
   1.112  qed "Suc_diff_le";
   1.113  
   1.114 -Goal "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i";
   1.115 +Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
   1.116  by (asm_full_simp_tac
   1.117      (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
   1.118  qed "Suc_diff_Suc";