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