src/HOL/Nat.thy
changeset 62365 8a105c235b1f
parent 62344 759d684c0e60
child 62376 85f38d5f8807
     1.1 --- a/src/HOL/Nat.thy	Thu Feb 18 17:52:52 2016 +0100
     1.2 +++ b/src/HOL/Nat.thy	Thu Feb 18 17:52:53 2016 +0100
     1.3 @@ -290,29 +290,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 -text \<open>Difference distributes over multiplication\<close>
     1.8 -
     1.9 -lemma diff_mult_distrib:
    1.10 -  "((m::nat) - n) * k = (m * k) - (n * k)"
    1.11 -  by (fact left_diff_distrib')
    1.12 -
    1.13 -lemma diff_mult_distrib2:
    1.14 -  "k * ((m::nat) - n) = (k * m) - (k * n)"
    1.15 -  by (fact right_diff_distrib')
    1.16 -
    1.17  
    1.18  subsubsection \<open>Addition\<close>
    1.19  
    1.20 -lemma nat_add_left_cancel:
    1.21 -  fixes k m n :: nat
    1.22 -  shows "k + m = k + n \<longleftrightarrow> m = n"
    1.23 -  by (fact add_left_cancel)
    1.24 -
    1.25 -lemma nat_add_right_cancel:
    1.26 -  fixes k m n :: nat
    1.27 -  shows "m + k = n + k \<longleftrightarrow> m = n"
    1.28 -  by (fact add_right_cancel)
    1.29 -
    1.30  text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close>
    1.31  
    1.32  lemma add_is_0 [iff]:
    1.33 @@ -349,47 +329,17 @@
    1.34  
    1.35  subsubsection \<open>Difference\<close>
    1.36  
    1.37 -lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
    1.38 -  by (fact diff_cancel)
    1.39 -
    1.40 -lemma diff_diff_left: "(i::nat) - j - k = i - (j + k)"
    1.41 -  by (fact diff_diff_add)
    1.42 -
    1.43  lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
    1.44 -  by (simp add: diff_diff_left)
    1.45 -
    1.46 -lemma diff_commute: "(i::nat) - j - k = i - k - j"
    1.47 -  by (fact diff_right_commute)
    1.48 -
    1.49 -lemma diff_add_inverse: "(n + m) - n = (m::nat)"
    1.50 -  by (fact add_diff_cancel_left')
    1.51 -
    1.52 -lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
    1.53 -  by (fact add_diff_cancel_right')
    1.54 -
    1.55 -lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
    1.56 -  by (fact add_diff_cancel_left)
    1.57 -
    1.58 -lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
    1.59 -  by (fact add_diff_cancel_right)
    1.60 -
    1.61 -lemma diff_add_0: "n - (n + m) = (0::nat)"
    1.62 -  by (fact diff_add_zero)
    1.63 +  by (simp add: diff_diff_add)
    1.64  
    1.65  lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
    1.66    unfolding One_nat_def by simp
    1.67  
    1.68  subsubsection \<open>Multiplication\<close>
    1.69  
    1.70 -lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
    1.71 -  by (fact distrib_left)
    1.72 -
    1.73  lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
    1.74    by (induct m) auto
    1.75  
    1.76 -lemmas nat_distrib =
    1.77 -  add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
    1.78 -
    1.79  lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"
    1.80    apply (induct m)
    1.81     apply simp
    1.82 @@ -1150,7 +1100,7 @@
    1.83  by (simp add: add.commute diff_add_assoc)
    1.84  
    1.85  lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
    1.86 -by (auto simp add: diff_add_inverse2)
    1.87 +by auto
    1.88  
    1.89  lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m \<le> n)"
    1.90  by (induct m n rule: diff_induct) simp_all
    1.91 @@ -1176,16 +1126,17 @@
    1.92      by (simp add: max_def not_le order_less_imp_le)
    1.93  
    1.94  lemma nat_diff_split:
    1.95 -  "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
    1.96 +  fixes a b :: nat
    1.97 +  shows "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)"
    1.98      \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
    1.99 -by (cases "a < b")
   1.100 -  (auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse
   1.101 -    not_less le_less dest!: add_eq_self_zero add_eq_self_zero[OF sym])
   1.102 +  by (cases "a < b")
   1.103 +    (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym])
   1.104  
   1.105  lemma nat_diff_split_asm:
   1.106 -  "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
   1.107 +  fixes a b :: nat
   1.108 +  shows "P (a - b) \<longleftrightarrow> \<not> (a < b \<and> \<not> P 0 \<or> (\<exists>d. a = b + d \<and> \<not> P d))"
   1.109      \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
   1.110 -by (auto split: nat_diff_split)
   1.111 +  by (auto split: nat_diff_split)
   1.112  
   1.113  lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   1.114    by simp
   1.115 @@ -1752,15 +1703,9 @@
   1.116  lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
   1.117  by arith
   1.118  
   1.119 -lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
   1.120 -  by (fact le_diff_conv2) \<comment> \<open>FIXME delete\<close>
   1.121 -
   1.122  lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
   1.123  by arith
   1.124  
   1.125 -lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
   1.126 -  by (fact le_add_diff) \<comment> \<open>FIXME delete\<close>
   1.127 -
   1.128  (*Replaces the previous diff_less and le_diff_less, which had the stronger
   1.129    second premise n\<le>m*)
   1.130  lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
   1.131 @@ -1830,7 +1775,7 @@
   1.132        k \<le> j ==> i + (j - k) = i + j - k *)
   1.133  lemmas add_diff_assoc = diff_add_assoc [symmetric]
   1.134  lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
   1.135 -declare diff_diff_left [simp]  add_diff_assoc [simp] add_diff_assoc2[simp]
   1.136 +declare add_diff_assoc [simp] add_diff_assoc2[simp]
   1.137  
   1.138  text\<open>At present we prove no analogue of \<open>not_less_Least\<close> or \<open>Least_Suc\<close>, since there appears to be no need.\<close>
   1.139  
   1.140 @@ -1921,55 +1866,68 @@
   1.141  
   1.142  subsection \<open>The divides relation on @{typ nat}\<close>
   1.143  
   1.144 -lemma dvd_1_left [iff]: "Suc 0 dvd k"
   1.145 -unfolding dvd_def by simp
   1.146 -
   1.147 -lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
   1.148 -by (simp add: dvd_def)
   1.149 -
   1.150 -lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
   1.151 -by (simp add: dvd_def)
   1.152 -
   1.153 -lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   1.154 +lemma dvd_1_left [iff]:
   1.155 +  "Suc 0 dvd k"
   1.156 +  by (simp add: dvd_def)
   1.157 +
   1.158 +lemma dvd_1_iff_1 [simp]:
   1.159 +  "m dvd Suc 0 \<longleftrightarrow> m = Suc 0"
   1.160 +  by (simp add: dvd_def)
   1.161 +
   1.162 +lemma nat_dvd_1_iff_1 [simp]:
   1.163 +  "m dvd (1::nat) \<longleftrightarrow> m = 1"
   1.164 +  by (simp add: dvd_def)
   1.165 +
   1.166 +lemma dvd_antisym:
   1.167 +  "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = (n::nat)"
   1.168    unfolding dvd_def
   1.169    by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
   1.170  
   1.171 -lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
   1.172 -unfolding dvd_def
   1.173 -by (blast intro: diff_mult_distrib2 [symmetric])
   1.174 -
   1.175 -lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
   1.176 +lemma dvd_diff_nat [simp]:
   1.177 +  "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n :: nat)"
   1.178 +  unfolding dvd_def
   1.179 +  by (blast intro: right_diff_distrib' [symmetric])
   1.180 +
   1.181 +lemma dvd_diffD:
   1.182 +  "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd (m::nat)"
   1.183    apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
   1.184    apply (blast intro: dvd_add)
   1.185    done
   1.186  
   1.187 -lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
   1.188 -by (drule_tac m = m in dvd_diff_nat, auto)
   1.189 -
   1.190 -lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
   1.191 -  unfolding dvd_def
   1.192 -  apply (erule exE)
   1.193 -  apply (simp add: ac_simps)
   1.194 -  done
   1.195 -
   1.196 -lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
   1.197 +lemma dvd_diffD1:
   1.198 +  "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd (n::nat)"
   1.199 +  by (drule_tac m = m in dvd_diff_nat) auto
   1.200 +
   1.201 +lemma dvd_mult_cancel:
   1.202 +  fixes m n k :: nat
   1.203 +  assumes "k * m dvd k * n" and "0 < k"
   1.204 +  shows "m dvd n"
   1.205 +proof -
   1.206 +  from assms(1) obtain q where "k * n = (k * m) * q" ..
   1.207 +  then have "k * n = k * (m * q)" by (simp add: ac_simps)
   1.208 +  with \<open>0 < k\<close> have "n = m * q" by simp
   1.209 +  then show ?thesis ..
   1.210 +qed
   1.211 +  
   1.212 +lemma dvd_mult_cancel1:
   1.213 +  "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = (1::nat)"
   1.214    apply auto
   1.215     apply (subgoal_tac "m*n dvd m*1")
   1.216     apply (drule dvd_mult_cancel, auto)
   1.217    done
   1.218  
   1.219 -lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
   1.220 -  apply (subst mult.commute)
   1.221 -  apply (erule dvd_mult_cancel1)
   1.222 -  done
   1.223 -
   1.224 -lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
   1.225 -by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
   1.226 +lemma dvd_mult_cancel2:
   1.227 +  "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = (1::nat)"
   1.228 +  using dvd_mult_cancel1 [of m n] by (simp add: ac_simps)
   1.229 +
   1.230 +lemma dvd_imp_le:
   1.231 +  "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> (n::nat)"
   1.232 +  by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
   1.233  
   1.234  lemma nat_dvd_not_less:
   1.235    fixes m n :: nat
   1.236    shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
   1.237 -by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
   1.238 +  by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
   1.239  
   1.240  lemma less_eq_dvd_minus:
   1.241    fixes m n :: nat
   1.242 @@ -2000,7 +1958,7 @@
   1.243  qed
   1.244  
   1.245  
   1.246 -subsection \<open>Aliases\<close>
   1.247 +subsection \<open>Aliasses\<close>
   1.248  
   1.249  lemma nat_mult_1: "(1::nat) * n = n"
   1.250    by (fact mult_1_left)
   1.251 @@ -2008,6 +1966,60 @@
   1.252  lemma nat_mult_1_right: "n * (1::nat) = n"
   1.253    by (fact mult_1_right)
   1.254  
   1.255 +lemma nat_add_left_cancel:
   1.256 +  fixes k m n :: nat
   1.257 +  shows "k + m = k + n \<longleftrightarrow> m = n"
   1.258 +  by (fact add_left_cancel)
   1.259 +
   1.260 +lemma nat_add_right_cancel:
   1.261 +  fixes k m n :: nat
   1.262 +  shows "m + k = n + k \<longleftrightarrow> m = n"
   1.263 +  by (fact add_right_cancel)
   1.264 +
   1.265 +lemma diff_mult_distrib:
   1.266 +  "((m::nat) - n) * k = (m * k) - (n * k)"
   1.267 +  by (fact left_diff_distrib')
   1.268 +
   1.269 +lemma diff_mult_distrib2:
   1.270 +  "k * ((m::nat) - n) = (k * m) - (k * n)"
   1.271 +  by (fact right_diff_distrib')
   1.272 +
   1.273 +lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
   1.274 +  by (fact le_add_diff) \<comment> \<open>FIXME delete\<close>
   1.275 +
   1.276 +lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
   1.277 +  by (fact le_diff_conv2) \<comment> \<open>FIXME delete\<close>
   1.278 +
   1.279 +lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
   1.280 +  by (fact diff_cancel)
   1.281 +
   1.282 +lemma diff_diff_left [simp]: "(i::nat) - j - k = i - (j + k)"
   1.283 +  by (fact diff_diff_add)
   1.284 +
   1.285 +lemma diff_commute: "(i::nat) - j - k = i - k - j"
   1.286 +  by (fact diff_right_commute)
   1.287 +
   1.288 +lemma diff_add_inverse: "(n + m) - n = (m::nat)"
   1.289 +  by (fact add_diff_cancel_left')
   1.290 +
   1.291 +lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
   1.292 +  by (fact add_diff_cancel_right')
   1.293 +
   1.294 +lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
   1.295 +  by (fact add_diff_cancel_left)
   1.296 +
   1.297 +lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
   1.298 +  by (fact add_diff_cancel_right)
   1.299 +
   1.300 +lemma diff_add_0: "n - (n + m) = (0::nat)"
   1.301 +  by (fact diff_add_zero)
   1.302 +
   1.303 +lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
   1.304 +  by (fact distrib_left)
   1.305 +
   1.306 +lemmas nat_distrib =
   1.307 +  add_mult_distrib distrib_left diff_mult_distrib diff_mult_distrib2
   1.308 +
   1.309  
   1.310  subsection \<open>Size of a datatype value\<close>
   1.311