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