src/HOL/Nat.thy
 changeset 30240 5b25fee0362c parent 29879 4425849f5db7 child 30242 aea5d7fa7ef5
equal inserted replaced
30239:179ff9cb160b 30240:5b25fee0362c
`   194 lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"`
`   194 lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"`
`   195   by (induct m) (simp_all add: add_assoc)`
`   195   by (induct m) (simp_all add: add_assoc)`
`   196 `
`   196 `
`   197 instance proof`
`   197 instance proof`
`   198   fix n m q :: nat`
`   198   fix n m q :: nat`
`   199   show "0 \<noteq> (1::nat)" by simp`
`   199   show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp`
`   200   show "1 * n = n" by simp`
`   200   show "1 * n = n" unfolding One_nat_def by simp`
`   201   show "n * m = m * n" by (induct n) simp_all`
`   201   show "n * m = m * n" by (induct n) simp_all`
`   202   show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)`
`   202   show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)`
`   203   show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)`
`   203   show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)`
`   204   assume "n + m = n + q" thus "m = q" by (induct n) simp_all`
`   204   assume "n + m = n + q" thus "m = q" by (induct n) simp_all`
`   205 qed`
`   205 qed`
`   278   by (simp add: diff_cancel add_commute)`
`   278   by (simp add: diff_cancel add_commute)`
`   279 `
`   279 `
`   280 lemma diff_add_0: "n - (n + m) = (0::nat)"`
`   280 lemma diff_add_0: "n - (n + m) = (0::nat)"`
`   281   by (induct n) simp_all`
`   281   by (induct n) simp_all`
`   282 `
`   282 `
`       `
`   283 lemma diff_Suc_1 [simp]: "Suc n - 1 = n"`
`       `
`   284   unfolding One_nat_def by simp`
`       `
`   285 `
`   283 text {* Difference distributes over multiplication *}`
`   286 text {* Difference distributes over multiplication *}`
`   284 `
`   287 `
`   285 lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"`
`   288 lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"`
`   286 by (induct m n rule: diff_induct) (simp_all add: diff_cancel)`
`   289 by (induct m n rule: diff_induct) (simp_all add: diff_cancel)`
`   287 `
`   290 `
`   305   by (induct m) auto`
`   308   by (induct m) auto`
`   306 `
`   309 `
`   307 lemmas nat_distrib =`
`   310 lemmas nat_distrib =`
`   308   add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2`
`   311   add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2`
`   309 `
`   312 `
`   310 lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"`
`   313 lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"`
`   311   apply (induct m)`
`   314   apply (induct m)`
`   312    apply simp`
`   315    apply simp`
`   313   apply (induct n)`
`   316   apply (induct n)`
`   314    apply auto`
`   317    apply auto`
`   315   done`
`   318   done`
`   316 `
`   319 `
`   317 lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"`
`   320 lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"`
`   318   apply (rule trans)`
`   321   apply (rule trans)`
`   319   apply (rule_tac [2] mult_eq_1_iff, fastsimp)`
`   322   apply (rule_tac [2] mult_eq_1_iff, fastsimp)`
`   320   done`
`   323   done`
`       `
`   324 `
`       `
`   325 lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"`
`       `
`   326   unfolding One_nat_def by (rule mult_eq_1_iff)`
`       `
`   327 `
`       `
`   328 lemma nat_1_eq_mult_iff [simp]: "(1::nat) = m * n \<longleftrightarrow> m = 1 \<and> n = 1"`
`       `
`   329   unfolding One_nat_def by (rule one_eq_mult_iff)`
`   321 `
`   330 `
`   322 lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"`
`   331 lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"`
`   323 proof -`
`   332 proof -`
`   324   have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"`
`   333   have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"`
`   325   proof (induct n arbitrary: m)`
`   334   proof (induct n arbitrary: m)`
`   463   by (rule notE) (rule not_less0)`
`   472   by (rule notE) (rule not_less0)`
`   464 `
`   473 `
`   465 lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"`
`   474 lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"`
`   466   unfolding less_Suc_eq_le le_less ..`
`   475   unfolding less_Suc_eq_le le_less ..`
`   467 `
`   476 `
`   471 lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"`
`   477 lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"`
`   472   by (simp add: less_Suc_eq)`
`   478   by (simp add: less_Suc_eq)`
`       `
`   479 `
`       `
`   480 lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"`
`       `
`   481   unfolding One_nat_def by (rule less_Suc0)`
`   473 `
`   482 `
`   474 lemma Suc_mono: "m < n ==> Suc m < Suc n"`
`   483 lemma Suc_mono: "m < n ==> Suc m < Suc n"`
`   475   by simp`
`   484   by simp`
`   476 `
`   485 `
`   477 text {* "Less than" is antisymmetric, sort of *}`
`   486 text {* "Less than" is antisymmetric, sort of *}`
`   690 subsubsection {* Monotonicity of Addition *}`
`   699 subsubsection {* Monotonicity of Addition *}`
`   691 `
`   700 `
`   692 lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"`
`   701 lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"`
`   693 by (simp add: diff_Suc split: nat.split)`
`   702 by (simp add: diff_Suc split: nat.split)`
`   694 `
`   703 `
`       `
`   704 lemma Suc_diff_1 [simp]: "0 < n ==> Suc (n - 1) = n"`
`       `
`   705 unfolding One_nat_def by (rule Suc_pred)`
`       `
`   706 `
`   695 lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"`
`   707 lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"`
`   696 by (induct k) simp_all`
`   708 by (induct k) simp_all`
`   697 `
`   709 `
`   698 lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"`
`   710 lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"`
`   699 by (induct k) simp_all`
`   711 by (induct k) simp_all`
`   731 proof`
`   743 proof`
`   732   fix i j k :: nat`
`   744   fix i j k :: nat`
`   733   show "0 < (1::nat)" by simp`
`   745   show "0 < (1::nat)" by simp`
`   734   show "i \<le> j ==> k + i \<le> k + j" by simp`
`   746   show "i \<le> j ==> k + i \<le> k + j" by simp`
`   735   show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)`
`   747   show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)`
`       `
`   748 qed`
`       `
`   749 `
`       `
`   750 instance nat :: no_zero_divisors`
`       `
`   751 proof`
`       `
`   752   fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto`
`   736 qed`
`   753 qed`
`   737 `
`   754 `
`   738 lemma nat_mult_1: "(1::nat) * n = n"`
`   755 lemma nat_mult_1: "(1::nat) * n = n"`
`   739 by simp`
`   756 by simp`
`   740 `
`   757 `
`   793   apply (rule_tac x="LEAST k. P(k)" in exI)`
`   810   apply (rule_tac x="LEAST k. P(k)" in exI)`
`   794   apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)`
`   811   apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)`
`   795   done`
`   812   done`
`   796 `
`   813 `
`   797 lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"`
`   814 lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"`
`       `
`   815   unfolding One_nat_def`
`   798   apply (cases n)`
`   816   apply (cases n)`
`   799    apply blast`
`   817    apply blast`
`   800   apply (frule (1) ex_least_nat_le)`
`   818   apply (frule (1) ex_least_nat_le)`
`   801   apply (erule exE)`
`   819   apply (erule exE)`
`   802   apply (case_tac k)`
`   820   apply (case_tac k)`
`  1082    apply simp`
`  1100    apply simp`
`  1083   apply (case_tac n)`
`  1101   apply (case_tac n)`
`  1084    apply simp_all`
`  1102    apply simp_all`
`  1085   done`
`  1103   done`
`  1086 `
`  1104 `
`  1087 lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"`
`  1105 lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (Suc 0 \<le> m & Suc 0 \<le> n)"`
`  1088   apply (induct m)`
`  1106   apply (induct m)`
`  1089    apply simp`
`  1107    apply simp`
`  1090   apply (case_tac n)`
`  1108   apply (case_tac n)`
`  1091    apply simp_all`
`  1109    apply simp_all`
`  1092   done`
`  1110   done`
`  1157 where`
`  1175 where`
`  1158   of_nat_0:     "of_nat 0 = 0"`
`  1176   of_nat_0:     "of_nat 0 = 0"`
`  1159   | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"`
`  1177   | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"`
`  1160 `
`  1178 `
`  1161 lemma of_nat_1 [simp]: "of_nat 1 = 1"`
`  1179 lemma of_nat_1 [simp]: "of_nat 1 = 1"`
`  1162   by simp`
`  1180   unfolding One_nat_def by simp`
`  1163 `
`  1181 `
`  1164 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"`
`  1182 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"`
`  1165   by (induct m) (simp_all add: add_ac)`
`  1183   by (induct m) (simp_all add: add_ac)`
`  1166 `
`  1184 `
`  1167 lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"`
`  1185 lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"`
`  1269   unfolding abs_if by auto`
`  1287   unfolding abs_if by auto`
`  1270 `
`  1288 `
`  1271 end`
`  1289 end`
`  1272 `
`  1290 `
`  1273 lemma of_nat_id [simp]: "of_nat n = n"`
`  1291 lemma of_nat_id [simp]: "of_nat n = n"`
`  1274   by (induct n) auto`
`  1292   by (induct n) (auto simp add: One_nat_def)`
`  1275 `
`  1293 `
`  1276 lemma of_nat_eq_id [simp]: "of_nat = id"`
`  1294 lemma of_nat_eq_id [simp]: "of_nat = id"`
`  1277   by (auto simp add: expand_fun_eq)`
`  1295   by (auto simp add: expand_fun_eq)`
`  1278 `
`  1296 `
`  1279 `
`  1297 `
`  1374 lemma mono_nat_linear_lb:`
`  1392 lemma mono_nat_linear_lb:`
`  1375   "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"`
`  1393   "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"`
`  1376 apply(induct_tac k)`
`  1394 apply(induct_tac k)`
`  1377  apply simp`
`  1395  apply simp`
`  1378 apply(erule_tac x="m+n" in meta_allE)`
`  1396 apply(erule_tac x="m+n" in meta_allE)`
`  1379 apply(erule_tac x="m+n+1" in meta_allE)`
`  1397 apply(erule_tac x="Suc(m+n)" in meta_allE)`
`  1380 apply simp`
`  1398 apply simp`
`  1381 done`
`  1399 done`
`  1382 `
`  1400 `
`  1383 `
`  1401 `
`  1384 text{*Subtraction laws, mostly by Clemens Ballarin*}`
`  1402 text{*Subtraction laws, mostly by Clemens Ballarin*}`