src/HOL/NatArith.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 17688 91d3604ec4b5 child 21238 c46bc715bdfd permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
 nipkow@10214 ` 1` ```(* Title: HOL/NatArith.thy ``` nipkow@10214 ` 2` ``` ID: \$Id\$ ``` wenzelm@13297 ` 3` ``` Author: Tobias Nipkow and Markus Wenzel ``` wenzelm@13297 ` 4` ```*) ``` nipkow@10214 ` 5` paulson@15404 ` 6` ```header {*Further Arithmetic Facts Concerning the Natural Numbers*} ``` nipkow@10214 ` 7` nipkow@15131 ` 8` ```theory NatArith ``` nipkow@15140 ` 9` ```imports Nat ``` haftmann@16417 ` 10` ```uses "arith_data.ML" ``` nipkow@15131 ` 11` ```begin ``` nipkow@10214 ` 12` nipkow@10214 ` 13` ```setup arith_setup ``` nipkow@10214 ` 14` paulson@15404 ` 15` ```text{*The following proofs may rely on the arithmetic proof procedures.*} ``` wenzelm@13297 ` 16` paulson@17688 ` 17` ```lemma le_iff_add: "(m::nat) \ n = (\k. n = m + k)" ``` paulson@17688 ` 18` ``` by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add) ``` paulson@17688 ` 19` paulson@15404 ` 20` ```lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \ n)" ``` paulson@14208 ` 21` ```by (simp add: less_eq reflcl_trancl [symmetric] ``` paulson@14208 ` 22` ``` del: reflcl_trancl, arith) ``` paulson@11454 ` 23` nipkow@10214 ` 24` ```lemma nat_diff_split: ``` paulson@10599 ` 25` ``` "P(a - b::nat) = ((a P 0) & (ALL d. a = b + d --> P d))" ``` wenzelm@13297 ` 26` ``` -- {* elimination of @{text -} on @{text nat} *} ``` wenzelm@13297 ` 27` ``` by (cases "a m*(m::nat)" ``` paulson@15404 ` 40` ```by (induct_tac "m", auto) ``` paulson@15404 ` 41` paulson@15404 ` 42` ```lemma le_cube: "(m::nat) \ m*(m*m)" ``` paulson@15404 ` 43` ```by (induct_tac "m", auto) ``` paulson@15404 ` 44` paulson@15404 ` 45` paulson@15404 ` 46` ```text{*Subtraction laws, mostly by Clemens Ballarin*} ``` paulson@15404 ` 47` paulson@15404 ` 48` ```lemma diff_less_mono: "[| a < (b::nat); c \ a |] ==> a-c < b-c" ``` paulson@15404 ` 49` ```by arith ``` paulson@15404 ` 50` paulson@15404 ` 51` ```lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))" ``` paulson@15404 ` 52` ```by arith ``` paulson@15404 ` 53` paulson@15404 ` 54` ```lemma le_diff_conv: "(j-k \ (i::nat)) = (j \ i+k)" ``` paulson@15404 ` 55` ```by arith ``` paulson@15404 ` 56` paulson@15404 ` 57` ```lemma le_diff_conv2: "k \ j ==> (i \ j-k) = (i+k \ (j::nat))" ``` paulson@15404 ` 58` ```by arith ``` paulson@15404 ` 59` paulson@15404 ` 60` ```lemma diff_diff_cancel [simp]: "i \ (n::nat) ==> n - (n - i) = i" ``` paulson@15404 ` 61` ```by arith ``` paulson@15404 ` 62` paulson@15404 ` 63` ```lemma le_add_diff: "k \ (n::nat) ==> m \ n + m - k" ``` paulson@15404 ` 64` ```by arith ``` paulson@15404 ` 65` paulson@15404 ` 66` ```(*Replaces the previous diff_less and le_diff_less, which had the stronger ``` paulson@15404 ` 67` ``` second premise n\m*) ``` nipkow@15439 ` 68` ```lemma diff_less[simp]: "!!m::nat. [| 0 m - n < m" ``` paulson@15404 ` 69` ```by arith ``` paulson@15404 ` 70` paulson@15404 ` 71` paulson@15404 ` 72` ```(** Simplification of relational expressions involving subtraction **) ``` paulson@15404 ` 73` paulson@15404 ` 74` ```lemma diff_diff_eq: "[| k \ m; k \ (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)" ``` paulson@15404 ` 75` ```by (simp split add: nat_diff_split) ``` paulson@15404 ` 76` paulson@15404 ` 77` ```lemma eq_diff_iff: "[| k \ m; k \ (n::nat) |] ==> (m-k = n-k) = (m=n)" ``` paulson@15404 ` 78` ```by (auto split add: nat_diff_split) ``` paulson@15404 ` 79` paulson@15404 ` 80` ```lemma less_diff_iff: "[| k \ m; k \ (n::nat) |] ==> (m-k < n-k) = (m m; k \ (n::nat) |] ==> (m-k \ n-k) = (m\n)" ``` paulson@15404 ` 84` ```by (auto split add: nat_diff_split) ``` paulson@15404 ` 85` paulson@15404 ` 86` paulson@15404 ` 87` ```text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*} ``` paulson@15404 ` 88` paulson@15404 ` 89` ```(* Monotonicity of subtraction in first argument *) ``` paulson@15404 ` 90` ```lemma diff_le_mono: "m \ (n::nat) ==> (m-l) \ (n-l)" ``` paulson@15404 ` 91` ```by (simp split add: nat_diff_split) ``` paulson@15404 ` 92` paulson@15404 ` 93` ```lemma diff_le_mono2: "m \ (n::nat) ==> (l-n) \ (l-m)" ``` paulson@15404 ` 94` ```by (simp split add: nat_diff_split) ``` paulson@15404 ` 95` paulson@15404 ` 96` ```lemma diff_less_mono2: "[| m < (n::nat); m (l-n) < (l-m)" ``` paulson@15404 ` 97` ```by (simp split add: nat_diff_split) ``` paulson@15404 ` 98` paulson@15404 ` 99` ```lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n" ``` paulson@15404 ` 100` ```by (simp split add: nat_diff_split) ``` paulson@15404 ` 101` paulson@15404 ` 102` ```text{*Lemmas for ex/Factorization*} ``` paulson@15404 ` 103` paulson@15404 ` 104` ```lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n" ``` paulson@15404 ` 105` ```by (case_tac "m", auto) ``` paulson@15404 ` 106` paulson@15404 ` 107` ```lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n nj --> i - (j - k) = i + (k::nat) - j" ``` paulson@15404 ` 117` ```by arith ``` paulson@15404 ` 118` paulson@15404 ` 119` ```lemma diff_Suc_diff_eq1 [simp]: "k \ j ==> m - Suc (j - k) = m + k - Suc j" ``` paulson@15404 ` 120` ```by arith ``` paulson@15404 ` 121` paulson@15404 ` 122` ```lemma diff_Suc_diff_eq2 [simp]: "k \ j ==> Suc (j - k) - m = Suc j - (k + m)" ``` paulson@15404 ` 123` ```by arith ``` paulson@15404 ` 124` paulson@15404 ` 125` ```(*The others are ``` paulson@15404 ` 126` ``` i - j - k = i - (j + k), ``` paulson@15404 ` 127` ``` k \ j ==> j - k + i = j + i - k, ``` paulson@15404 ` 128` ``` k \ j ==> i + (j - k) = i + j - k *) ``` paulson@17085 ` 129` ```lemmas add_diff_assoc = diff_add_assoc [symmetric] ``` paulson@17085 ` 130` ```lemmas add_diff_assoc2 = diff_add_assoc2[symmetric] ``` paulson@17085 ` 131` ```declare diff_diff_left [simp] add_diff_assoc [simp] add_diff_assoc2[simp] ``` paulson@15404 ` 132` paulson@15404 ` 133` ```text{*At present we prove no analogue of @{text not_less_Least} or @{text ``` paulson@15404 ` 134` ```Least_Suc}, since there appears to be no need.*} ``` paulson@15404 ` 135` paulson@15404 ` 136` ```ML ``` paulson@15404 ` 137` ```{* ``` paulson@15404 ` 138` ```val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le"; ``` paulson@15404 ` 139` ```val nat_diff_split = thm "nat_diff_split"; ``` paulson@15404 ` 140` ```val nat_diff_split_asm = thm "nat_diff_split_asm"; ``` paulson@15404 ` 141` ```val le_square = thm "le_square"; ``` paulson@15404 ` 142` ```val le_cube = thm "le_cube"; ``` paulson@15404 ` 143` ```val diff_less_mono = thm "diff_less_mono"; ``` paulson@15404 ` 144` ```val less_diff_conv = thm "less_diff_conv"; ``` paulson@15404 ` 145` ```val le_diff_conv = thm "le_diff_conv"; ``` paulson@15404 ` 146` ```val le_diff_conv2 = thm "le_diff_conv2"; ``` paulson@15404 ` 147` ```val diff_diff_cancel = thm "diff_diff_cancel"; ``` paulson@15404 ` 148` ```val le_add_diff = thm "le_add_diff"; ``` paulson@15404 ` 149` ```val diff_less = thm "diff_less"; ``` paulson@15404 ` 150` ```val diff_diff_eq = thm "diff_diff_eq"; ``` paulson@15404 ` 151` ```val eq_diff_iff = thm "eq_diff_iff"; ``` paulson@15404 ` 152` ```val less_diff_iff = thm "less_diff_iff"; ``` paulson@15404 ` 153` ```val le_diff_iff = thm "le_diff_iff"; ``` paulson@15404 ` 154` ```val diff_le_mono = thm "diff_le_mono"; ``` paulson@15404 ` 155` ```val diff_le_mono2 = thm "diff_le_mono2"; ``` paulson@15404 ` 156` ```val diff_less_mono2 = thm "diff_less_mono2"; ``` paulson@15404 ` 157` ```val diffs0_imp_equal = thm "diffs0_imp_equal"; ``` paulson@15404 ` 158` ```val one_less_mult = thm "one_less_mult"; ``` paulson@15404 ` 159` ```val n_less_m_mult_n = thm "n_less_m_mult_n"; ``` paulson@15404 ` 160` ```val n_less_n_mult_m = thm "n_less_n_mult_m"; ``` paulson@15404 ` 161` ```val diff_diff_right = thm "diff_diff_right"; ``` paulson@15404 ` 162` ```val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1"; ``` paulson@15404 ` 163` ```val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2"; ``` paulson@15404 ` 164` ```*} ``` paulson@15404 ` 165` nipkow@15539 ` 166` ```subsection{*Embedding of the Naturals into any @{text ``` nipkow@15539 ` 167` ```comm_semiring_1_cancel}: @{term of_nat}*} ``` nipkow@15539 ` 168` nipkow@15539 ` 169` ```consts of_nat :: "nat => 'a::comm_semiring_1_cancel" ``` nipkow@15539 ` 170` nipkow@15539 ` 171` ```primrec ``` nipkow@15539 ` 172` ``` of_nat_0: "of_nat 0 = 0" ``` nipkow@15539 ` 173` ``` of_nat_Suc: "of_nat (Suc m) = of_nat m + 1" ``` nipkow@15539 ` 174` nipkow@15539 ` 175` ```lemma of_nat_1 [simp]: "of_nat 1 = 1" ``` nipkow@15539 ` 176` ```by simp ``` nipkow@15539 ` 177` nipkow@15539 ` 178` ```lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n" ``` nipkow@15539 ` 179` ```apply (induct m) ``` nipkow@15539 ` 180` ```apply (simp_all add: add_ac) ``` nipkow@15539 ` 181` ```done ``` nipkow@15539 ` 182` nipkow@15539 ` 183` ```lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n" ``` nipkow@15539 ` 184` ```apply (induct m) ``` nipkow@15539 ` 185` ```apply (simp_all add: mult_ac add_ac right_distrib) ``` nipkow@15539 ` 186` ```done ``` nipkow@15539 ` 187` nipkow@15539 ` 188` ```lemma zero_le_imp_of_nat: "0 \ (of_nat m::'a::ordered_semidom)" ``` nipkow@15539 ` 189` ```apply (induct m, simp_all) ``` nipkow@15539 ` 190` ```apply (erule order_trans) ``` nipkow@15539 ` 191` ```apply (rule less_add_one [THEN order_less_imp_le]) ``` nipkow@15539 ` 192` ```done ``` nipkow@15539 ` 193` nipkow@15539 ` 194` ```lemma less_imp_of_nat_less: ``` nipkow@15539 ` 195` ``` "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)" ``` nipkow@15539 ` 196` ```apply (induct m n rule: diff_induct, simp_all) ``` nipkow@15539 ` 197` ```apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force) ``` nipkow@15539 ` 198` ```done ``` nipkow@15539 ` 199` nipkow@15539 ` 200` ```lemma of_nat_less_imp_less: ``` nipkow@15539 ` 201` ``` "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n" ``` nipkow@15539 ` 202` ```apply (induct m n rule: diff_induct, simp_all) ``` nipkow@15539 ` 203` ```apply (insert zero_le_imp_of_nat) ``` nipkow@15539 ` 204` ```apply (force simp add: linorder_not_less [symmetric]) ``` nipkow@15539 ` 205` ```done ``` nipkow@15539 ` 206` nipkow@15539 ` 207` ```lemma of_nat_less_iff [simp]: ``` nipkow@15539 ` 208` ``` "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m (of_nat n::'a::ordered_semidom)) = (m \ n)" ``` nipkow@15539 ` 219` ```by (simp add: linorder_not_less [symmetric]) ``` nipkow@15539 ` 220` nipkow@15539 ` 221` ```text{*Special cases where either operand is zero*} ``` paulson@17085 ` 222` ```lemmas of_nat_0_le_iff = of_nat_le_iff [of 0, simplified] ``` paulson@17085 ` 223` ```lemmas of_nat_le_0_iff = of_nat_le_iff [of _ 0, simplified] ``` paulson@17085 ` 224` ```declare of_nat_0_le_iff [simp] ``` paulson@17085 ` 225` ```declare of_nat_le_0_iff [simp] ``` nipkow@15539 ` 226` nipkow@15539 ` 227` ```text{*The ordering on the @{text comm_semiring_1_cancel} is necessary ``` nipkow@15539 ` 228` ```to exclude the possibility of a finite field, which indeed wraps back to ``` nipkow@15539 ` 229` ```zero.*} ``` nipkow@15539 ` 230` ```lemma of_nat_eq_iff [simp]: ``` nipkow@15539 ` 231` ``` "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)" ``` nipkow@15539 ` 232` ```by (simp add: order_eq_iff) ``` nipkow@15539 ` 233` nipkow@15539 ` 234` ```text{*Special cases where either operand is zero*} ``` paulson@17085 ` 235` ```lemmas of_nat_0_eq_iff = of_nat_eq_iff [of 0, simplified] ``` paulson@17085 ` 236` ```lemmas of_nat_eq_0_iff = of_nat_eq_iff [of _ 0, simplified] ``` paulson@17085 ` 237` ```declare of_nat_0_eq_iff [simp] ``` paulson@17085 ` 238` ```declare of_nat_eq_0_iff [simp] ``` nipkow@15539 ` 239` nipkow@15539 ` 240` ```lemma of_nat_diff [simp]: ``` nipkow@15539 ` 241` ``` "n \ m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)" ``` nipkow@15539 ` 242` ```by (simp del: of_nat_add ``` nipkow@15539 ` 243` ``` add: compare_rls of_nat_add [symmetric] split add: nat_diff_split) ``` nipkow@15539 ` 244` paulson@15404 ` 245` nipkow@10214 ` 246` ```end ```