src/HOL/Nat.thy
changeset 57512 cc97b347b301
parent 57492 74bf65a1910a
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Nat.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -244,10 +244,10 @@
     1.4    by (induct m) simp_all
     1.5  
     1.6  lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
     1.7 -  by (induct m) (simp_all add: add_left_commute)
     1.8 +  by (induct m) (simp_all add: add.left_commute)
     1.9  
    1.10  lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
    1.11 -  by (induct m) (simp_all add: add_assoc)
    1.12 +  by (induct m) (simp_all add: add.assoc)
    1.13  
    1.14  instance proof
    1.15    fix n m q :: nat
    1.16 @@ -263,20 +263,15 @@
    1.17  
    1.18  subsubsection {* Addition *}
    1.19  
    1.20 -lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
    1.21 -  by (rule add_assoc)
    1.22 -
    1.23 -lemma nat_add_commute: "m + n = n + (m::nat)"
    1.24 -  by (rule add_commute)
    1.25 +lemma nat_add_left_cancel:
    1.26 +  fixes k m n :: nat
    1.27 +  shows "k + m = k + n \<longleftrightarrow> m = n"
    1.28 +  by (fact add_left_cancel)
    1.29  
    1.30 -lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
    1.31 -  by (rule add_left_commute)
    1.32 -
    1.33 -lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
    1.34 -  by (rule add_left_cancel)
    1.35 -
    1.36 -lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
    1.37 -  by (rule add_right_cancel)
    1.38 +lemma nat_add_right_cancel:
    1.39 +  fixes k m n :: nat
    1.40 +  shows "m + k = n + k \<longleftrightarrow> m = n"
    1.41 +  by (fact add_right_cancel)
    1.42  
    1.43  text {* Reasoning about @{text "m + 0 = 0"}, etc. *}
    1.44  
    1.45 @@ -315,31 +310,31 @@
    1.46  subsubsection {* Difference *}
    1.47  
    1.48  lemma diff_self_eq_0 [simp]: "(m\<Colon>nat) - m = 0"
    1.49 -  by (induct m) simp_all
    1.50 +  by (fact diff_cancel)
    1.51  
    1.52  lemma diff_diff_left: "(i::nat) - j - k = i - (j + k)"
    1.53 -  by (induct i j rule: diff_induct) simp_all
    1.54 +  by (fact diff_diff_add)
    1.55  
    1.56  lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
    1.57    by (simp add: diff_diff_left)
    1.58  
    1.59  lemma diff_commute: "(i::nat) - j - k = i - k - j"
    1.60 -  by (simp add: diff_diff_left add_commute)
    1.61 +  by (fact diff_right_commute)
    1.62  
    1.63  lemma diff_add_inverse: "(n + m) - n = (m::nat)"
    1.64 -  by (induct n) simp_all
    1.65 +  by (fact add_diff_cancel_left')
    1.66  
    1.67  lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
    1.68 -  by (simp add: diff_add_inverse add_commute [of m n])
    1.69 +  by (fact add_diff_cancel_right')
    1.70  
    1.71  lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
    1.72 -  by (induct k) simp_all
    1.73 +  by (fact comm_monoid_diff_class.add_diff_cancel_left)
    1.74  
    1.75  lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
    1.76 -  by (simp add: diff_cancel add_commute)
    1.77 +  by (fact add_diff_cancel_right)
    1.78  
    1.79  lemma diff_add_0: "n - (n + m) = (0::nat)"
    1.80 -  by (induct n) simp_all
    1.81 +  by (fact diff_add_zero)
    1.82  
    1.83  lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
    1.84    unfolding One_nat_def by simp
    1.85 @@ -350,20 +345,14 @@
    1.86  by (induct m n rule: diff_induct) (simp_all add: diff_cancel)
    1.87  
    1.88  lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)"
    1.89 -by (simp add: diff_mult_distrib mult_commute [of k])
    1.90 +by (simp add: diff_mult_distrib mult.commute [of k])
    1.91    -- {* NOT added as rewrites, since sometimes they are used from right-to-left *}
    1.92  
    1.93  
    1.94  subsubsection {* Multiplication *}
    1.95  
    1.96 -lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
    1.97 -  by (rule mult_assoc)
    1.98 -
    1.99 -lemma nat_mult_commute: "m * n = n * (m::nat)"
   1.100 -  by (rule mult_commute)
   1.101 -
   1.102  lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
   1.103 -  by (rule distrib_left)
   1.104 +  by (fact distrib_left)
   1.105  
   1.106  lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   1.107    by (induct m) auto
   1.108 @@ -402,7 +391,7 @@
   1.109  qed
   1.110  
   1.111  lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   1.112 -  by (simp add: mult_commute)
   1.113 +  by (simp add: mult.commute)
   1.114  
   1.115  lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
   1.116    by (subst mult_cancel1) simp
   1.117 @@ -950,7 +939,7 @@
   1.118    next
   1.119      case (Suc k)
   1.120      have "0 + i < Suc k + i" by (rule add_less_mono1) simp
   1.121 -    hence "i < Suc (i + k)" by (simp add: add_commute)
   1.122 +    hence "i < Suc (i + k)" by (simp add: add.commute)
   1.123      from trans[OF this lessI Suc step]
   1.124      show ?case by simp
   1.125    qed
   1.126 @@ -1036,7 +1025,7 @@
   1.127  by (insert add_right_mono [of 0 m n], simp)
   1.128  
   1.129  lemma le_add1: "n \<le> ((n + m)::nat)"
   1.130 -by (simp add: add_commute, rule le_add2)
   1.131 +by (simp add: add.commute, rule le_add2)
   1.132  
   1.133  lemma less_add_Suc1: "i < Suc (i + m)"
   1.134  by (rule le_less_trans, rule le_add1, rule lessI)
   1.135 @@ -1071,7 +1060,7 @@
   1.136  done
   1.137  
   1.138  lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
   1.139 -by (simp add: add_commute)
   1.140 +by (simp add: add.commute)
   1.141  
   1.142  lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
   1.143  apply (rule order_trans [of _ "m+k"])
   1.144 @@ -1079,7 +1068,7 @@
   1.145  done
   1.146  
   1.147  lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
   1.148 -apply (simp add: add_commute)
   1.149 +apply (simp add: add.commute)
   1.150  apply (erule add_leD1)
   1.151  done
   1.152  
   1.153 @@ -1103,7 +1092,7 @@
   1.154  by (simp add: add_diff_inverse linorder_not_less)
   1.155  
   1.156  lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
   1.157 -by (simp add: add_commute)
   1.158 +by (simp add: add.commute)
   1.159  
   1.160  lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
   1.161  by (induct m n rule: diff_induct) simp_all
   1.162 @@ -1135,7 +1124,7 @@
   1.163  by (induct j k rule: diff_induct) simp_all
   1.164  
   1.165  lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
   1.166 -by (simp add: add_commute diff_add_assoc)
   1.167 +by (simp add: add.commute diff_add_assoc)
   1.168  
   1.169  lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
   1.170  by (auto simp add: diff_add_inverse2)
   1.171 @@ -1233,7 +1222,7 @@
   1.172    done
   1.173  
   1.174  lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)"
   1.175 -by (simp add: mult_commute [of k])
   1.176 +by (simp add: mult.commute [of k])
   1.177  
   1.178  lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
   1.179  by (simp add: linorder_not_less [symmetric], auto)
   1.180 @@ -1435,7 +1424,7 @@
   1.181      by (induct n) simp_all
   1.182    from this [of 0] have "of_nat_aux (\<lambda>i. i + 1) n 1 = of_nat_aux (\<lambda>i. i + 1) n 0 + 1"
   1.183      by simp
   1.184 -  with Suc show ?case by (simp add: add_commute)
   1.185 +  with Suc show ?case by (simp add: add.commute)
   1.186  qed
   1.187  
   1.188  end
   1.189 @@ -1693,13 +1682,13 @@
   1.190  by arith
   1.191  
   1.192  lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
   1.193 -by arith
   1.194 +  by (fact le_diff_conv2) -- {* FIXME delete *}
   1.195  
   1.196  lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
   1.197  by arith
   1.198  
   1.199  lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
   1.200 -by arith
   1.201 +  by (fact le_add_diff) -- {* FIXME delete *}
   1.202  
   1.203  (*Replaces the previous diff_less and le_diff_less, which had the stronger
   1.204    second premise n\<le>m*)
   1.205 @@ -1847,7 +1836,7 @@
   1.206  
   1.207  lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   1.208    unfolding dvd_def
   1.209 -  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc)
   1.210 +  by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
   1.211  
   1.212  text {* @{term "op dvd"} is a partial order *}
   1.213  
   1.214 @@ -1890,7 +1879,7 @@
   1.215    done
   1.216  
   1.217  lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
   1.218 -  apply (subst mult_commute)
   1.219 +  apply (subst mult.commute)
   1.220    apply (erule dvd_mult_cancel1)
   1.221    done
   1.222  
   1.223 @@ -1940,7 +1929,7 @@
   1.224    fixes m n q :: nat
   1.225    assumes "m dvd q"
   1.226    shows "m dvd n + q \<longleftrightarrow> m dvd n"
   1.227 -  using assms by (simp add: dvd_plus_eq_right add_commute [of n])
   1.228 +  using assms by (simp add: dvd_plus_eq_right add.commute [of n])
   1.229  
   1.230  lemma less_eq_dvd_minus:
   1.231    fixes m n :: nat
   1.232 @@ -1949,7 +1938,7 @@
   1.233  proof -
   1.234    from assms have "n = m + (n - m)" by simp
   1.235    then obtain q where "n = m + q" ..
   1.236 -  then show ?thesis by (simp add: dvd_reduce add_commute [of m])
   1.237 +  then show ?thesis by (simp add: dvd_reduce add.commute [of m])
   1.238  qed
   1.239  
   1.240  lemma dvd_minus_self:
   1.241 @@ -1966,7 +1955,7 @@
   1.242      by (auto elim: dvd_plusE)
   1.243    also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
   1.244    also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
   1.245 -  also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add_commute)
   1.246 +  also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add.commute)
   1.247    finally show ?thesis .
   1.248  qed
   1.249