author | haftmann |
Thu, 06 Dec 2007 16:36:19 +0100 | |
changeset 25559 | f14305fb698c |
parent 25534 | d0b74fdd6067 |
child 25563 | cab4f808f791 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Nat.thy |
2 |
ID: $Id$ |
|
21243 | 3 |
Author: Tobias Nipkow and Lawrence C Paulson and Markus Wenzel |
923 | 4 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
5 |
Type "nat" is a linear order, and a datatype; arithmetic operators + - |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
6 |
and * (for div, mod and dvd, see theory Divides). |
923 | 7 |
*) |
8 |
||
13449 | 9 |
header {* Natural numbers *} |
10 |
||
15131 | 11 |
theory Nat |
15140 | 12 |
imports Wellfounded_Recursion Ring_and_Field |
23263 | 13 |
uses |
14 |
"~~/src/Tools/rat.ML" |
|
15 |
"~~/src/Provers/Arith/cancel_sums.ML" |
|
16 |
("arith_data.ML") |
|
24091 | 17 |
"~~/src/Provers/Arith/fast_lin_arith.ML" |
18 |
("Tools/lin_arith.ML") |
|
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24523
diff
changeset
|
19 |
("Tools/function_package/size.ML") |
15131 | 20 |
begin |
13449 | 21 |
|
22 |
subsection {* Type @{text ind} *} |
|
23 |
||
24 |
typedecl ind |
|
25 |
||
19573 | 26 |
axiomatization |
27 |
Zero_Rep :: ind and |
|
28 |
Suc_Rep :: "ind => ind" |
|
29 |
where |
|
13449 | 30 |
-- {* the axiom of infinity in 2 parts *} |
19573 | 31 |
inj_Suc_Rep: "inj Suc_Rep" and |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
32 |
Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep" |
19573 | 33 |
|
13449 | 34 |
|
35 |
subsection {* Type nat *} |
|
36 |
||
37 |
text {* Type definition *} |
|
38 |
||
23740 | 39 |
inductive_set Nat :: "ind set" |
22262 | 40 |
where |
23740 | 41 |
Zero_RepI: "Zero_Rep : Nat" |
42 |
| Suc_RepI: "i : Nat ==> Suc_Rep i : Nat" |
|
13449 | 43 |
|
44 |
global |
|
45 |
||
46 |
typedef (open Nat) |
|
23740 | 47 |
nat = Nat |
21243 | 48 |
proof |
23740 | 49 |
show "Zero_Rep : Nat" by (rule Nat.Zero_RepI) |
21243 | 50 |
qed |
13449 | 51 |
|
52 |
consts |
|
53 |
Suc :: "nat => nat" |
|
54 |
||
55 |
local |
|
56 |
||
25510 | 57 |
instantiation nat :: zero |
58 |
begin |
|
59 |
||
60 |
definition Zero_nat_def [code func del]: |
|
61 |
"0 = Abs_Nat Zero_Rep" |
|
62 |
||
63 |
instance .. |
|
64 |
||
65 |
end |
|
24995 | 66 |
|
13449 | 67 |
defs |
18648 | 68 |
Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" |
22718 | 69 |
|
13449 | 70 |
theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" |
71 |
apply (unfold Zero_nat_def Suc_def) |
|
72 |
apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} |
|
23740 | 73 |
apply (erule Rep_Nat [THEN Nat.induct]) |
74 |
apply (iprover elim: Abs_Nat_inverse [THEN subst]) |
|
13449 | 75 |
done |
76 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
77 |
lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0" |
23740 | 78 |
by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI |
22718 | 79 |
Suc_Rep_not_Zero_Rep) |
13449 | 80 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
81 |
lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m" |
13449 | 82 |
by (rule not_sym, rule Suc_not_Zero not_sym) |
83 |
||
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16635
diff
changeset
|
84 |
lemma inj_Suc[simp]: "inj_on Suc N" |
23740 | 85 |
by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI |
22718 | 86 |
inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) |
13449 | 87 |
|
88 |
lemma Suc_Suc_eq [iff]: "(Suc m = Suc n) = (m = n)" |
|
15413 | 89 |
by (rule inj_Suc [THEN inj_eq]) |
13449 | 90 |
|
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
4640
diff
changeset
|
91 |
rep_datatype nat |
13449 | 92 |
distinct Suc_not_Zero Zero_not_Suc |
93 |
inject Suc_Suc_eq |
|
21411 | 94 |
induction nat_induct |
95 |
||
96 |
declare nat.induct [case_names 0 Suc, induct type: nat] |
|
97 |
declare nat.exhaust [case_names 0 Suc, cases type: nat] |
|
13449 | 98 |
|
21672 | 99 |
lemmas nat_rec_0 = nat.recs(1) |
100 |
and nat_rec_Suc = nat.recs(2) |
|
101 |
||
102 |
lemmas nat_case_0 = nat.cases(1) |
|
103 |
and nat_case_Suc = nat.cases(2) |
|
104 |
||
24995 | 105 |
|
106 |
text {* Injectiveness and distinctness lemmas *} |
|
107 |
||
108 |
lemma Suc_neq_Zero: "Suc m = 0 ==> R" |
|
25162 | 109 |
by (rule notE, rule Suc_not_Zero) |
24995 | 110 |
|
111 |
lemma Zero_neq_Suc: "0 = Suc m ==> R" |
|
25162 | 112 |
by (rule Suc_neq_Zero, erule sym) |
24995 | 113 |
|
114 |
lemma Suc_inject: "Suc x = Suc y ==> x = y" |
|
25162 | 115 |
by (rule inj_Suc [THEN injD]) |
24995 | 116 |
|
117 |
lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False" |
|
25162 | 118 |
by auto |
24995 | 119 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
120 |
lemma n_not_Suc_n: "n \<noteq> Suc n" |
25162 | 121 |
by (induct n) simp_all |
13449 | 122 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
123 |
lemma Suc_n_not_n: "Suc t \<noteq> t" |
25162 | 124 |
by (rule not_sym, rule n_not_Suc_n) |
13449 | 125 |
|
24995 | 126 |
|
13449 | 127 |
text {* A special form of induction for reasoning |
128 |
about @{term "m < n"} and @{term "m - n"} *} |
|
129 |
||
130 |
theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> |
|
131 |
(!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" |
|
14208 | 132 |
apply (rule_tac x = m in spec) |
15251 | 133 |
apply (induct n) |
13449 | 134 |
prefer 2 |
135 |
apply (rule allI) |
|
17589 | 136 |
apply (induct_tac x, iprover+) |
13449 | 137 |
done |
138 |
||
24995 | 139 |
|
140 |
subsection {* Arithmetic operators *} |
|
141 |
||
142 |
instance nat :: "{one, plus, minus, times}" |
|
143 |
One_nat_def [simp]: "1 == Suc 0" .. |
|
144 |
||
145 |
primrec |
|
146 |
add_0: "0 + n = n" |
|
147 |
add_Suc: "Suc m + n = Suc (m + n)" |
|
148 |
||
149 |
primrec |
|
150 |
diff_0: "m - 0 = m" |
|
151 |
diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)" |
|
152 |
||
153 |
primrec |
|
154 |
mult_0: "0 * n = 0" |
|
155 |
mult_Suc: "Suc m * n = n + (m * n)" |
|
156 |
||
157 |
||
158 |
subsection {* Orders on @{typ nat} *} |
|
159 |
||
160 |
definition |
|
161 |
pred_nat :: "(nat * nat) set" where |
|
162 |
"pred_nat = {(m, n). n = Suc m}" |
|
163 |
||
25510 | 164 |
instantiation nat :: ord |
165 |
begin |
|
166 |
||
167 |
definition |
|
168 |
less_def [code func del]: "m < n \<longleftrightarrow> (m, n) : pred_nat^+" |
|
24995 | 169 |
|
25510 | 170 |
definition |
171 |
le_def [code func del]: "m \<le> (n\<Colon>nat) \<longleftrightarrow> \<not> n < m" |
|
172 |
||
173 |
instance .. |
|
174 |
||
175 |
end |
|
13449 | 176 |
|
177 |
lemma wf_pred_nat: "wf pred_nat" |
|
14208 | 178 |
apply (unfold wf_def pred_nat_def, clarify) |
179 |
apply (induct_tac x, blast+) |
|
13449 | 180 |
done |
181 |
||
182 |
lemma wf_less: "wf {(x, y::nat). x < y}" |
|
183 |
apply (unfold less_def) |
|
14208 | 184 |
apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset], blast) |
13449 | 185 |
done |
186 |
||
187 |
lemma less_eq: "((m, n) : pred_nat^+) = (m < n)" |
|
188 |
apply (unfold less_def) |
|
189 |
apply (rule refl) |
|
190 |
done |
|
191 |
||
192 |
subsubsection {* Introduction properties *} |
|
193 |
||
194 |
lemma less_trans: "i < j ==> j < k ==> i < (k::nat)" |
|
195 |
apply (unfold less_def) |
|
14208 | 196 |
apply (rule trans_trancl [THEN transD], assumption+) |
13449 | 197 |
done |
198 |
||
199 |
lemma lessI [iff]: "n < Suc n" |
|
200 |
apply (unfold less_def pred_nat_def) |
|
201 |
apply (simp add: r_into_trancl) |
|
202 |
done |
|
203 |
||
204 |
lemma less_SucI: "i < j ==> i < Suc j" |
|
14208 | 205 |
apply (rule less_trans, assumption) |
13449 | 206 |
apply (rule lessI) |
207 |
done |
|
208 |
||
209 |
lemma zero_less_Suc [iff]: "0 < Suc n" |
|
210 |
apply (induct n) |
|
211 |
apply (rule lessI) |
|
212 |
apply (erule less_trans) |
|
213 |
apply (rule lessI) |
|
214 |
done |
|
215 |
||
216 |
subsubsection {* Elimination properties *} |
|
217 |
||
218 |
lemma less_not_sym: "n < m ==> ~ m < (n::nat)" |
|
219 |
apply (unfold less_def) |
|
220 |
apply (blast intro: wf_pred_nat wf_trancl [THEN wf_asym]) |
|
221 |
done |
|
222 |
||
223 |
lemma less_asym: |
|
224 |
assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P |
|
225 |
apply (rule contrapos_np) |
|
226 |
apply (rule less_not_sym) |
|
227 |
apply (rule h1) |
|
228 |
apply (erule h2) |
|
229 |
done |
|
230 |
||
231 |
lemma less_not_refl: "~ n < (n::nat)" |
|
232 |
apply (unfold less_def) |
|
233 |
apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_not_refl]) |
|
234 |
done |
|
235 |
||
236 |
lemma less_irrefl [elim!]: "(n::nat) < n ==> R" |
|
25162 | 237 |
by (rule notE, rule less_not_refl) |
13449 | 238 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
239 |
lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast |
13449 | 240 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
241 |
lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t" |
25162 | 242 |
by (rule not_sym, rule less_not_refl2) |
13449 | 243 |
|
244 |
lemma lessE: |
|
245 |
assumes major: "i < k" |
|
246 |
and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P" |
|
247 |
shows P |
|
14208 | 248 |
apply (rule major [unfolded less_def pred_nat_def, THEN tranclE], simp_all) |
13449 | 249 |
apply (erule p1) |
250 |
apply (rule p2) |
|
14208 | 251 |
apply (simp add: less_def pred_nat_def, assumption) |
13449 | 252 |
done |
253 |
||
254 |
lemma not_less0 [iff]: "~ n < (0::nat)" |
|
25162 | 255 |
by (blast elim: lessE) |
13449 | 256 |
|
257 |
lemma less_zeroE: "(n::nat) < 0 ==> R" |
|
25162 | 258 |
by (rule notE, rule not_less0) |
13449 | 259 |
|
260 |
lemma less_SucE: assumes major: "m < Suc n" |
|
261 |
and less: "m < n ==> P" and eq: "m = n ==> P" shows P |
|
262 |
apply (rule major [THEN lessE]) |
|
14208 | 263 |
apply (rule eq, blast) |
264 |
apply (rule less, blast) |
|
13449 | 265 |
done |
266 |
||
267 |
lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)" |
|
25162 | 268 |
by (blast elim!: less_SucE intro: less_trans) |
13449 | 269 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24196
diff
changeset
|
270 |
lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)" |
25162 | 271 |
by (simp add: less_Suc_eq) |
13449 | 272 |
|
273 |
lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)" |
|
25162 | 274 |
by (simp add: less_Suc_eq) |
13449 | 275 |
|
276 |
lemma Suc_mono: "m < n ==> Suc m < Suc n" |
|
25162 | 277 |
by (induct n) (fast elim: less_trans lessE)+ |
13449 | 278 |
|
279 |
text {* "Less than" is a linear ordering *} |
|
280 |
lemma less_linear: "m < n | m = n | n < (m::nat)" |
|
15251 | 281 |
apply (induct m) |
282 |
apply (induct n) |
|
13449 | 283 |
apply (rule refl [THEN disjI1, THEN disjI2]) |
284 |
apply (rule zero_less_Suc [THEN disjI1]) |
|
285 |
apply (blast intro: Suc_mono less_SucI elim: lessE) |
|
286 |
done |
|
287 |
||
14302 | 288 |
text {* "Less than" is antisymmetric, sort of *} |
289 |
lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n" |
|
22718 | 290 |
apply(simp only:less_Suc_eq) |
291 |
apply blast |
|
292 |
done |
|
14302 | 293 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
294 |
lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)" |
13449 | 295 |
using less_linear by blast |
296 |
||
297 |
lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m" |
|
298 |
and eqCase: "m = n ==> P n m" and lessCase: "n<m ==> P n m" |
|
299 |
shows "P n m" |
|
300 |
apply (rule less_linear [THEN disjE]) |
|
301 |
apply (erule_tac [2] disjE) |
|
302 |
apply (erule lessCase) |
|
303 |
apply (erule sym [THEN eqCase]) |
|
304 |
apply (erule major) |
|
305 |
done |
|
306 |
||
307 |
||
308 |
subsubsection {* Inductive (?) properties *} |
|
309 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
310 |
lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n" |
13449 | 311 |
apply (simp add: nat_neq_iff) |
312 |
apply (blast elim!: less_irrefl less_SucE elim: less_asym) |
|
313 |
done |
|
314 |
||
315 |
lemma Suc_lessD: "Suc m < n ==> m < n" |
|
316 |
apply (induct n) |
|
317 |
apply (fast intro!: lessI [THEN less_SucI] elim: less_trans lessE)+ |
|
318 |
done |
|
319 |
||
320 |
lemma Suc_lessE: assumes major: "Suc i < k" |
|
321 |
and minor: "!!j. i < j ==> k = Suc j ==> P" shows P |
|
322 |
apply (rule major [THEN lessE]) |
|
323 |
apply (erule lessI [THEN minor]) |
|
14208 | 324 |
apply (erule Suc_lessD [THEN minor], assumption) |
13449 | 325 |
done |
326 |
||
327 |
lemma Suc_less_SucD: "Suc m < Suc n ==> m < n" |
|
25162 | 328 |
by (blast elim: lessE dest: Suc_lessD) |
4104 | 329 |
|
16635 | 330 |
lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)" |
13449 | 331 |
apply (rule iffI) |
332 |
apply (erule Suc_less_SucD) |
|
333 |
apply (erule Suc_mono) |
|
334 |
done |
|
335 |
||
336 |
lemma less_trans_Suc: |
|
337 |
assumes le: "i < j" shows "j < k ==> Suc i < k" |
|
14208 | 338 |
apply (induct k, simp_all) |
13449 | 339 |
apply (insert le) |
340 |
apply (simp add: less_Suc_eq) |
|
341 |
apply (blast dest: Suc_lessD) |
|
342 |
done |
|
343 |
||
16635 | 344 |
lemma [code]: "((n::nat) < 0) = False" by simp |
345 |
lemma [code]: "(0 < Suc n) = True" by simp |
|
346 |
||
13449 | 347 |
text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *} |
348 |
lemma not_less_eq: "(~ m < n) = (n < Suc m)" |
|
25162 | 349 |
by (induct m n rule: diff_induct) simp_all |
13449 | 350 |
|
351 |
text {* Complete induction, aka course-of-values induction *} |
|
352 |
lemma nat_less_induct: |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
353 |
assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n" |
22718 | 354 |
apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]]) |
13449 | 355 |
apply (rule prem) |
14208 | 356 |
apply (unfold less_def, assumption) |
13449 | 357 |
done |
358 |
||
14131 | 359 |
lemmas less_induct = nat_less_induct [rule_format, case_names less] |
360 |
||
21243 | 361 |
|
24995 | 362 |
text {* Properties of "less than or equal" *} |
13449 | 363 |
|
364 |
text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
365 |
lemma less_Suc_eq_le: "(m < Suc n) = (m \<le> n)" |
22718 | 366 |
unfolding le_def by (rule not_less_eq [symmetric]) |
13449 | 367 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
368 |
lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n" |
25162 | 369 |
by (rule less_Suc_eq_le [THEN iffD2]) |
13449 | 370 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
371 |
lemma le0 [iff]: "(0::nat) \<le> n" |
22718 | 372 |
unfolding le_def by (rule not_less0) |
13449 | 373 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
374 |
lemma Suc_n_not_le_n: "~ Suc n \<le> n" |
25162 | 375 |
by (simp add: le_def) |
13449 | 376 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
377 |
lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)" |
25162 | 378 |
by (induct i) (simp_all add: le_def) |
13449 | 379 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
380 |
lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)" |
25162 | 381 |
by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq) |
13449 | 382 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
383 |
lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R" |
25162 | 384 |
by (drule le_Suc_eq [THEN iffD1], iprover+) |
13449 | 385 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
386 |
lemma Suc_leI: "m < n ==> Suc(m) \<le> n" |
13449 | 387 |
apply (simp add: le_def less_Suc_eq) |
388 |
apply (blast elim!: less_irrefl less_asym) |
|
389 |
done -- {* formerly called lessD *} |
|
390 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
391 |
lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n" |
25162 | 392 |
by (simp add: le_def less_Suc_eq) |
13449 | 393 |
|
394 |
text {* Stronger version of @{text Suc_leD} *} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
395 |
lemma Suc_le_lessD: "Suc m \<le> n ==> m < n" |
13449 | 396 |
apply (simp add: le_def less_Suc_eq) |
397 |
using less_linear |
|
398 |
apply blast |
|
399 |
done |
|
400 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
401 |
lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)" |
25162 | 402 |
by (blast intro: Suc_leI Suc_le_lessD) |
13449 | 403 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
404 |
lemma le_SucI: "m \<le> n ==> m \<le> Suc n" |
25162 | 405 |
by (unfold le_def) (blast dest: Suc_lessD) |
13449 | 406 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
407 |
lemma less_imp_le: "m < n ==> m \<le> (n::nat)" |
25162 | 408 |
by (unfold le_def) (blast elim: less_asym) |
13449 | 409 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
410 |
text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *} |
13449 | 411 |
lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq |
412 |
||
413 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
414 |
text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *} |
13449 | 415 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
416 |
lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)" |
22718 | 417 |
unfolding le_def |
13449 | 418 |
using less_linear |
22718 | 419 |
by (blast elim: less_irrefl less_asym) |
13449 | 420 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
421 |
lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)" |
22718 | 422 |
unfolding le_def |
13449 | 423 |
using less_linear |
22718 | 424 |
by (blast elim!: less_irrefl elim: less_asym) |
13449 | 425 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
426 |
lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)" |
25162 | 427 |
by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq) |
13449 | 428 |
|
22718 | 429 |
text {* Useful with @{text blast}. *} |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
430 |
lemma eq_imp_le: "(m::nat) = n ==> m \<le> n" |
25162 | 431 |
by (rule less_or_eq_imp_le) (rule disjI2) |
13449 | 432 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
433 |
lemma le_refl: "n \<le> (n::nat)" |
25162 | 434 |
by (simp add: le_eq_less_or_eq) |
13449 | 435 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
436 |
lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)" |
25162 | 437 |
by (blast dest!: le_imp_less_or_eq intro: less_trans) |
13449 | 438 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
439 |
lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)" |
25162 | 440 |
by (blast dest!: le_imp_less_or_eq intro: less_trans) |
13449 | 441 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
442 |
lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)" |
25162 | 443 |
by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans) |
13449 | 444 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
445 |
lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)" |
25162 | 446 |
by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym) |
13449 | 447 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
448 |
lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)" |
25162 | 449 |
by (simp add: le_simps) |
13449 | 450 |
|
451 |
text {* Axiom @{text order_less_le} of class @{text order}: *} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
452 |
lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)" |
25162 | 453 |
by (simp add: le_def nat_neq_iff) (blast elim!: less_asym) |
13449 | 454 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
455 |
lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n" |
25162 | 456 |
by (rule iffD2, rule nat_less_le, rule conjI) |
13449 | 457 |
|
458 |
text {* Axiom @{text linorder_linear} of class @{text linorder}: *} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
459 |
lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m" |
13449 | 460 |
apply (simp add: le_eq_less_or_eq) |
22718 | 461 |
using less_linear by blast |
13449 | 462 |
|
24995 | 463 |
text {* Type @{typ nat} is a wellfounded linear order *} |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
464 |
|
22318 | 465 |
instance nat :: wellorder |
14691 | 466 |
by intro_classes |
467 |
(assumption | |
|
468 |
rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+ |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
469 |
|
22718 | 470 |
lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat] |
15921 | 471 |
|
13449 | 472 |
lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)" |
25162 | 473 |
by (blast elim!: less_SucE) |
13449 | 474 |
|
475 |
text {* |
|
476 |
Rewrite @{term "n < Suc m"} to @{term "n = m"} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
477 |
if @{term "~ n < m"} or @{term "m \<le> n"} hold. |
13449 | 478 |
Not suitable as default simprules because they often lead to looping |
479 |
*} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
480 |
lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)" |
25162 | 481 |
by (rule not_less_less_Suc_eq, rule leD) |
13449 | 482 |
|
483 |
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq |
|
484 |
||
485 |
||
486 |
text {* |
|
22718 | 487 |
Re-orientation of the equations @{text "0 = x"} and @{text "1 = x"}. |
488 |
No longer added as simprules (they loop) |
|
13449 | 489 |
but via @{text reorient_simproc} in Bin |
490 |
*} |
|
491 |
||
492 |
text {* Polymorphic, not just for @{typ nat} *} |
|
493 |
lemma zero_reorient: "(0 = x) = (x = 0)" |
|
25162 | 494 |
by auto |
13449 | 495 |
|
496 |
lemma one_reorient: "(1 = x) = (x = 1)" |
|
25162 | 497 |
by auto |
13449 | 498 |
|
22718 | 499 |
text {* These two rules ease the use of primitive recursion. |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
500 |
NOTE USE OF @{text "=="} *} |
13449 | 501 |
lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c" |
25162 | 502 |
by simp |
13449 | 503 |
|
504 |
lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)" |
|
25162 | 505 |
by simp |
13449 | 506 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
507 |
lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m" |
25162 | 508 |
by (cases n) simp_all |
509 |
||
510 |
lemma gr0_implies_Suc: "n > 0 ==> \<exists>m. n = Suc m" |
|
511 |
by (cases n) simp_all |
|
13449 | 512 |
|
22718 | 513 |
lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0" |
25162 | 514 |
by (cases n) simp_all |
13449 | 515 |
|
25162 | 516 |
lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)" |
517 |
by (cases n) simp_all |
|
25140 | 518 |
|
13449 | 519 |
text {* This theorem is useful with @{text blast} *} |
520 |
lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n" |
|
25162 | 521 |
by (rule neq0_conv[THEN iffD1], iprover) |
13449 | 522 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
523 |
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)" |
25162 | 524 |
by (fast intro: not0_implies_Suc) |
13449 | 525 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24196
diff
changeset
|
526 |
lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)" |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
527 |
using neq0_conv by blast |
13449 | 528 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
529 |
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)" |
25162 | 530 |
by (induct m') simp_all |
13449 | 531 |
|
532 |
text {* Useful in certain inductive arguments *} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
533 |
lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))" |
25162 | 534 |
by (cases m) simp_all |
13449 | 535 |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
536 |
lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n" |
13449 | 537 |
apply (rule nat_less_induct) |
538 |
apply (case_tac n) |
|
539 |
apply (case_tac [2] nat) |
|
540 |
apply (blast intro: less_trans)+ |
|
541 |
done |
|
542 |
||
21243 | 543 |
|
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
15281
diff
changeset
|
544 |
subsection {* @{text LEAST} theorems for type @{typ nat}*} |
13449 | 545 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
546 |
lemma Least_Suc: |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
547 |
"[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
14208 | 548 |
apply (case_tac "n", auto) |
13449 | 549 |
apply (frule LeastI) |
550 |
apply (drule_tac P = "%x. P (Suc x) " in LeastI) |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
551 |
apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))") |
13449 | 552 |
apply (erule_tac [2] Least_le) |
14208 | 553 |
apply (case_tac "LEAST x. P x", auto) |
13449 | 554 |
apply (drule_tac P = "%x. P (Suc x) " in Least_le) |
555 |
apply (blast intro: order_antisym) |
|
556 |
done |
|
557 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
558 |
lemma Least_Suc2: |
25162 | 559 |
"[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)" |
560 |
by (erule (1) Least_Suc [THEN ssubst], simp) |
|
13449 | 561 |
|
562 |
||
563 |
subsection {* @{term min} and @{term max} *} |
|
564 |
||
25076 | 565 |
lemma mono_Suc: "mono Suc" |
25162 | 566 |
by (rule monoI) simp |
25076 | 567 |
|
13449 | 568 |
lemma min_0L [simp]: "min 0 n = (0::nat)" |
25162 | 569 |
by (rule min_leastL) simp |
13449 | 570 |
|
571 |
lemma min_0R [simp]: "min n 0 = (0::nat)" |
|
25162 | 572 |
by (rule min_leastR) simp |
13449 | 573 |
|
574 |
lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)" |
|
25162 | 575 |
by (simp add: mono_Suc min_of_mono) |
13449 | 576 |
|
22191 | 577 |
lemma min_Suc1: |
578 |
"min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))" |
|
25162 | 579 |
by (simp split: nat.split) |
22191 | 580 |
|
581 |
lemma min_Suc2: |
|
582 |
"min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))" |
|
25162 | 583 |
by (simp split: nat.split) |
22191 | 584 |
|
13449 | 585 |
lemma max_0L [simp]: "max 0 n = (n::nat)" |
25162 | 586 |
by (rule max_leastL) simp |
13449 | 587 |
|
588 |
lemma max_0R [simp]: "max n 0 = (n::nat)" |
|
25162 | 589 |
by (rule max_leastR) simp |
13449 | 590 |
|
591 |
lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)" |
|
25162 | 592 |
by (simp add: mono_Suc max_of_mono) |
13449 | 593 |
|
22191 | 594 |
lemma max_Suc1: |
595 |
"max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))" |
|
25162 | 596 |
by (simp split: nat.split) |
22191 | 597 |
|
598 |
lemma max_Suc2: |
|
599 |
"max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))" |
|
25162 | 600 |
by (simp split: nat.split) |
22191 | 601 |
|
13449 | 602 |
|
603 |
subsection {* Basic rewrite rules for the arithmetic operators *} |
|
604 |
||
605 |
text {* Difference *} |
|
606 |
||
14193
30e41f63712e
Improved efficiency of code generated for + and -
berghofe
parents:
14131
diff
changeset
|
607 |
lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)" |
25162 | 608 |
by (induct n) simp_all |
13449 | 609 |
|
14193
30e41f63712e
Improved efficiency of code generated for + and -
berghofe
parents:
14131
diff
changeset
|
610 |
lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n" |
25162 | 611 |
by (induct n) simp_all |
13449 | 612 |
|
613 |
||
614 |
text {* |
|
615 |
Could be (and is, below) generalized in various ways |
|
616 |
However, none of the generalizations are currently in the simpset, |
|
617 |
and I dread to think what happens if I put them in |
|
618 |
*} |
|
25162 | 619 |
lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n" |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
620 |
by (simp split add: nat.split) |
13449 | 621 |
|
14193
30e41f63712e
Improved efficiency of code generated for + and -
berghofe
parents:
14131
diff
changeset
|
622 |
declare diff_Suc [simp del, code del] |
13449 | 623 |
|
624 |
||
625 |
subsection {* Addition *} |
|
626 |
||
627 |
lemma add_0_right [simp]: "m + 0 = (m::nat)" |
|
25162 | 628 |
by (induct m) simp_all |
13449 | 629 |
|
630 |
lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)" |
|
25162 | 631 |
by (induct m) simp_all |
13449 | 632 |
|
19890 | 633 |
lemma add_Suc_shift [code]: "Suc m + n = m + Suc n" |
25162 | 634 |
by simp |
14193
30e41f63712e
Improved efficiency of code generated for + and -
berghofe
parents:
14131
diff
changeset
|
635 |
|
13449 | 636 |
|
637 |
text {* Associative law for addition *} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
638 |
lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)" |
25162 | 639 |
by (induct m) simp_all |
13449 | 640 |
|
641 |
text {* Commutative law for addition *} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
642 |
lemma nat_add_commute: "m + n = n + (m::nat)" |
25162 | 643 |
by (induct m) simp_all |
13449 | 644 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
645 |
lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)" |
13449 | 646 |
apply (rule mk_left_commute [of "op +"]) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
647 |
apply (rule nat_add_assoc) |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
648 |
apply (rule nat_add_commute) |
13449 | 649 |
done |
650 |
||
14331 | 651 |
lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))" |
25162 | 652 |
by (induct k) simp_all |
13449 | 653 |
|
14331 | 654 |
lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))" |
25162 | 655 |
by (induct k) simp_all |
13449 | 656 |
|
14331 | 657 |
lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))" |
25162 | 658 |
by (induct k) simp_all |
13449 | 659 |
|
14331 | 660 |
lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))" |
25162 | 661 |
by (induct k) simp_all |
13449 | 662 |
|
663 |
text {* Reasoning about @{text "m + 0 = 0"}, etc. *} |
|
664 |
||
22718 | 665 |
lemma add_is_0 [iff]: fixes m :: nat shows "(m + n = 0) = (m = 0 & n = 0)" |
25162 | 666 |
by (cases m) simp_all |
13449 | 667 |
|
668 |
lemma add_is_1: "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)" |
|
25162 | 669 |
by (cases m) simp_all |
13449 | 670 |
|
671 |
lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)" |
|
25162 | 672 |
by (rule trans, rule eq_commute, rule add_is_1) |
13449 | 673 |
|
25162 | 674 |
lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)" |
675 |
by(auto dest:gr0_implies_Suc) |
|
13449 | 676 |
|
677 |
lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0" |
|
678 |
apply (drule add_0_right [THEN ssubst]) |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
679 |
apply (simp add: nat_add_assoc del: add_0_right) |
13449 | 680 |
done |
681 |
||
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16635
diff
changeset
|
682 |
lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N" |
22718 | 683 |
apply (induct k) |
684 |
apply simp |
|
685 |
apply(drule comp_inj_on[OF _ inj_Suc]) |
|
686 |
apply (simp add:o_def) |
|
687 |
done |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16635
diff
changeset
|
688 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16635
diff
changeset
|
689 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
690 |
subsection {* Multiplication *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
691 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
692 |
text {* right annihilation in product *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
693 |
lemma mult_0_right [simp]: "(m::nat) * 0 = 0" |
25162 | 694 |
by (induct m) simp_all |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
695 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
696 |
text {* right successor law for multiplication *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
697 |
lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)" |
25162 | 698 |
by (induct m) (simp_all add: nat_add_left_commute) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
699 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
700 |
text {* Commutative law for multiplication *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
701 |
lemma nat_mult_commute: "m * n = n * (m::nat)" |
25162 | 702 |
by (induct m) simp_all |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
703 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
704 |
text {* addition distributes over multiplication *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
705 |
lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)" |
25162 | 706 |
by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
707 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
708 |
lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)" |
25162 | 709 |
by (induct m) (simp_all add: nat_add_assoc) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
710 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
711 |
text {* Associative law for multiplication *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
712 |
lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)" |
25162 | 713 |
by (induct m) (simp_all add: add_mult_distrib) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
714 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
715 |
|
14740 | 716 |
text{*The naturals form a @{text comm_semiring_1_cancel}*} |
14738 | 717 |
instance nat :: comm_semiring_1_cancel |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
718 |
proof |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
719 |
fix i j k :: nat |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
720 |
show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc) |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
721 |
show "i + j = j + i" by (rule nat_add_commute) |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
722 |
show "0 + i = i" by simp |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
723 |
show "(i * j) * k = i * (j * k)" by (rule nat_mult_assoc) |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
724 |
show "i * j = j * i" by (rule nat_mult_commute) |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
725 |
show "1 * i = i" by simp |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
726 |
show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib) |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
727 |
show "0 \<noteq> (1::nat)" by simp |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
728 |
assume "k+i = k+j" thus "i=j" by simp |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
729 |
qed |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
730 |
|
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
731 |
lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)" |
15251 | 732 |
apply (induct m) |
22718 | 733 |
apply (induct_tac [2] n) |
734 |
apply simp_all |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
735 |
done |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
736 |
|
21243 | 737 |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
738 |
subsection {* Monotonicity of Addition *} |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
739 |
|
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
740 |
text {* strict, in 1st argument *} |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
741 |
lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)" |
25162 | 742 |
by (induct k) simp_all |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
743 |
|
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
744 |
text {* strict, in both arguments *} |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
745 |
lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)" |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
746 |
apply (rule add_less_mono1 [THEN less_trans], assumption+) |
15251 | 747 |
apply (induct j, simp_all) |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
748 |
done |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
749 |
|
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
750 |
text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *} |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
751 |
lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))" |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
752 |
apply (induct n) |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
753 |
apply (simp_all add: order_le_less) |
22718 | 754 |
apply (blast elim!: less_SucE |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
755 |
intro!: add_0_right [symmetric] add_Suc_right [symmetric]) |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
756 |
done |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
757 |
|
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
758 |
text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *} |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
759 |
lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j" |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
760 |
apply(auto simp: gr0_conv_Suc) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
761 |
apply (induct_tac m) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
762 |
apply (simp_all add: add_less_mono) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
763 |
done |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
764 |
|
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
765 |
|
14740 | 766 |
text{*The naturals form an ordered @{text comm_semiring_1_cancel}*} |
14738 | 767 |
instance nat :: ordered_semidom |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
768 |
proof |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
769 |
fix i j k :: nat |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
770 |
show "0 < (1::nat)" by simp |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
771 |
show "i \<le> j ==> k + i \<le> k + j" by simp |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
772 |
show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2) |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
773 |
qed |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
774 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
775 |
lemma nat_mult_1: "(1::nat) * n = n" |
25162 | 776 |
by simp |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
777 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
778 |
lemma nat_mult_1_right: "n * (1::nat) = n" |
25162 | 779 |
by simp |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
780 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
781 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
782 |
subsection {* Additional theorems about "less than" *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
783 |
|
19870 | 784 |
text{*An induction rule for estabilishing binary relations*} |
22718 | 785 |
lemma less_Suc_induct: |
19870 | 786 |
assumes less: "i < j" |
787 |
and step: "!!i. P i (Suc i)" |
|
788 |
and trans: "!!i j k. P i j ==> P j k ==> P i k" |
|
789 |
shows "P i j" |
|
790 |
proof - |
|
22718 | 791 |
from less obtain k where j: "j = Suc(i+k)" by (auto dest: less_imp_Suc_add) |
792 |
have "P i (Suc (i + k))" |
|
19870 | 793 |
proof (induct k) |
22718 | 794 |
case 0 |
795 |
show ?case by (simp add: step) |
|
19870 | 796 |
next |
797 |
case (Suc k) |
|
22718 | 798 |
thus ?case by (auto intro: assms) |
19870 | 799 |
qed |
22718 | 800 |
thus "P i j" by (simp add: j) |
19870 | 801 |
qed |
802 |
||
24438 | 803 |
text {* The method of infinite descent, frequently used in number theory. |
804 |
Provided by Roelof Oosterhuis. |
|
805 |
$P(n)$ is true for all $n\in\mathbb{N}$ if |
|
806 |
\begin{itemize} |
|
807 |
\item case ``0'': given $n=0$ prove $P(n)$, |
|
808 |
\item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists |
|
809 |
a smaller integer $m$ such that $\neg P(m)$. |
|
810 |
\end{itemize} *} |
|
811 |
||
24523 | 812 |
lemma infinite_descent0[case_names 0 smaller]: |
24438 | 813 |
"\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n" |
814 |
by (induct n rule: less_induct, case_tac "n>0", auto) |
|
815 |
||
24523 | 816 |
text{* A compact version without explicit base case: *} |
817 |
lemma infinite_descent: |
|
818 |
"\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m \<rbrakk> \<Longrightarrow> P n" |
|
819 |
by (induct n rule: less_induct, auto) |
|
820 |
||
24438 | 821 |
|
822 |
text {* Infinite descent using a mapping to $\mathbb{N}$: |
|
823 |
$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and |
|
824 |
\begin{itemize} |
|
825 |
\item case ``0'': given $V(x)=0$ prove $P(x)$, |
|
826 |
\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$. |
|
827 |
\end{itemize} |
|
828 |
NB: the proof also shows how to use the previous lemma. *} |
|
25482 | 829 |
corollary infinite_descent0_measure [case_names 0 smaller]: |
830 |
assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x" |
|
831 |
and A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)" |
|
832 |
shows "P x" |
|
24438 | 833 |
proof - |
834 |
obtain n where "n = V x" by auto |
|
25482 | 835 |
moreover have "\<And>x. V x = n \<Longrightarrow> P x" |
24523 | 836 |
proof (induct n rule: infinite_descent0) |
24438 | 837 |
case 0 -- "i.e. $V(x) = 0$" |
25482 | 838 |
with A0 show "P x" by auto |
24438 | 839 |
next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$" |
840 |
case (smaller n) |
|
841 |
then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto |
|
25482 | 842 |
with A1 obtain y where "V y < V x \<and> \<not> P y" by auto |
24438 | 843 |
with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto |
844 |
thus ?case by auto |
|
845 |
qed |
|
846 |
ultimately show "P x" by auto |
|
847 |
qed |
|
19870 | 848 |
|
24523 | 849 |
text{* Again, without explicit base case: *} |
850 |
lemma infinite_descent_measure: |
|
851 |
assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x" |
|
852 |
proof - |
|
853 |
from assms obtain n where "n = V x" by auto |
|
854 |
moreover have "!!x. V x = n \<Longrightarrow> P x" |
|
855 |
proof (induct n rule: infinite_descent, auto) |
|
856 |
fix x assume "\<not> P x" |
|
857 |
with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto |
|
858 |
qed |
|
859 |
ultimately show "P x" by auto |
|
860 |
qed |
|
861 |
||
862 |
||
863 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
864 |
text {* A [clumsy] way of lifting @{text "<"} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
865 |
monotonicity to @{text "\<le>"} monotonicity *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
866 |
lemma less_mono_imp_le_mono: |
24438 | 867 |
"\<lbrakk> !!i j::nat. i < j \<Longrightarrow> f i < f j; i \<le> j \<rbrakk> \<Longrightarrow> f i \<le> ((f j)::nat)" |
868 |
by (simp add: order_le_less) (blast) |
|
869 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
870 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
871 |
text {* non-strict, in 1st argument *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
872 |
lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)" |
24438 | 873 |
by (rule add_right_mono) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
874 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
875 |
text {* non-strict, in both arguments *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
876 |
lemma add_le_mono: "[| i \<le> j; k \<le> l |] ==> i + k \<le> j + (l::nat)" |
24438 | 877 |
by (rule add_mono) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
878 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
879 |
lemma le_add2: "n \<le> ((m + n)::nat)" |
24438 | 880 |
by (insert add_right_mono [of 0 m n], simp) |
13449 | 881 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
882 |
lemma le_add1: "n \<le> ((n + m)::nat)" |
24438 | 883 |
by (simp add: add_commute, rule le_add2) |
13449 | 884 |
|
885 |
lemma less_add_Suc1: "i < Suc (i + m)" |
|
24438 | 886 |
by (rule le_less_trans, rule le_add1, rule lessI) |
13449 | 887 |
|
888 |
lemma less_add_Suc2: "i < Suc (m + i)" |
|
24438 | 889 |
by (rule le_less_trans, rule le_add2, rule lessI) |
13449 | 890 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
891 |
lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))" |
24438 | 892 |
by (iprover intro!: less_add_Suc1 less_imp_Suc_add) |
13449 | 893 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
894 |
lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m" |
24438 | 895 |
by (rule le_trans, assumption, rule le_add1) |
13449 | 896 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
897 |
lemma trans_le_add2: "(i::nat) \<le> j ==> i \<le> m + j" |
24438 | 898 |
by (rule le_trans, assumption, rule le_add2) |
13449 | 899 |
|
900 |
lemma trans_less_add1: "(i::nat) < j ==> i < j + m" |
|
24438 | 901 |
by (rule less_le_trans, assumption, rule le_add1) |
13449 | 902 |
|
903 |
lemma trans_less_add2: "(i::nat) < j ==> i < m + j" |
|
24438 | 904 |
by (rule less_le_trans, assumption, rule le_add2) |
13449 | 905 |
|
906 |
lemma add_lessD1: "i + j < (k::nat) ==> i < k" |
|
24438 | 907 |
apply (rule le_less_trans [of _ "i+j"]) |
908 |
apply (simp_all add: le_add1) |
|
909 |
done |
|
13449 | 910 |
|
911 |
lemma not_add_less1 [iff]: "~ (i + j < (i::nat))" |
|
24438 | 912 |
apply (rule notI) |
913 |
apply (erule add_lessD1 [THEN less_irrefl]) |
|
914 |
done |
|
13449 | 915 |
|
916 |
lemma not_add_less2 [iff]: "~ (j + i < (i::nat))" |
|
24438 | 917 |
by (simp add: add_commute not_add_less1) |
13449 | 918 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
919 |
lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)" |
24438 | 920 |
apply (rule order_trans [of _ "m+k"]) |
921 |
apply (simp_all add: le_add1) |
|
922 |
done |
|
13449 | 923 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
924 |
lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)" |
24438 | 925 |
apply (simp add: add_commute) |
926 |
apply (erule add_leD1) |
|
927 |
done |
|
13449 | 928 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
929 |
lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R" |
24438 | 930 |
by (blast dest: add_leD1 add_leD2) |
13449 | 931 |
|
932 |
text {* needs @{text "!!k"} for @{text add_ac} to work *} |
|
933 |
lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n" |
|
24438 | 934 |
by (force simp del: add_Suc_right |
13449 | 935 |
simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac) |
936 |
||
937 |
||
938 |
subsection {* Difference *} |
|
939 |
||
940 |
lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0" |
|
24438 | 941 |
by (induct m) simp_all |
13449 | 942 |
|
943 |
text {* Addition is the inverse of subtraction: |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
944 |
if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *} |
13449 | 945 |
lemma add_diff_inverse: "~ m < n ==> n + (m - n) = (m::nat)" |
24438 | 946 |
by (induct m n rule: diff_induct) simp_all |
13449 | 947 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
948 |
lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)" |
24438 | 949 |
by (simp add: add_diff_inverse linorder_not_less) |
13449 | 950 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
951 |
lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)" |
24438 | 952 |
by (simp add: le_add_diff_inverse add_commute) |
13449 | 953 |
|
954 |
||
955 |
subsection {* More results about difference *} |
|
956 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
957 |
lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)" |
24438 | 958 |
by (induct m n rule: diff_induct) simp_all |
13449 | 959 |
|
960 |
lemma diff_less_Suc: "m - n < Suc m" |
|
24438 | 961 |
apply (induct m n rule: diff_induct) |
962 |
apply (erule_tac [3] less_SucE) |
|
963 |
apply (simp_all add: less_Suc_eq) |
|
964 |
done |
|
13449 | 965 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
966 |
lemma diff_le_self [simp]: "m - n \<le> (m::nat)" |
24438 | 967 |
by (induct m n rule: diff_induct) (simp_all add: le_SucI) |
13449 | 968 |
|
969 |
lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k" |
|
24438 | 970 |
by (rule le_less_trans, rule diff_le_self) |
13449 | 971 |
|
972 |
lemma diff_diff_left: "(i::nat) - j - k = i - (j + k)" |
|
24438 | 973 |
by (induct i j rule: diff_induct) simp_all |
13449 | 974 |
|
975 |
lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k" |
|
24438 | 976 |
by (simp add: diff_diff_left) |
13449 | 977 |
|
978 |
lemma diff_Suc_less [simp]: "0<n ==> n - Suc i < n" |
|
24438 | 979 |
by (cases n) (auto simp add: le_simps) |
13449 | 980 |
|
981 |
text {* This and the next few suggested by Florian Kammueller *} |
|
982 |
lemma diff_commute: "(i::nat) - j - k = i - k - j" |
|
24438 | 983 |
by (simp add: diff_diff_left add_commute) |
13449 | 984 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
985 |
lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)" |
24438 | 986 |
by (induct j k rule: diff_induct) simp_all |
13449 | 987 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
988 |
lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i" |
24438 | 989 |
by (simp add: add_commute diff_add_assoc) |
13449 | 990 |
|
991 |
lemma diff_add_inverse: "(n + m) - n = (m::nat)" |
|
24438 | 992 |
by (induct n) simp_all |
13449 | 993 |
|
994 |
lemma diff_add_inverse2: "(m + n) - n = (m::nat)" |
|
24438 | 995 |
by (simp add: diff_add_assoc) |
13449 | 996 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
997 |
lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)" |
24438 | 998 |
by (auto simp add: diff_add_inverse2) |
13449 | 999 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1000 |
lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m \<le> n)" |
24438 | 1001 |
by (induct m n rule: diff_induct) simp_all |
13449 | 1002 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1003 |
lemma diff_is_0_eq' [simp]: "m \<le> n ==> (m::nat) - n = 0" |
24438 | 1004 |
by (rule iffD2, rule diff_is_0_eq) |
13449 | 1005 |
|
1006 |
lemma zero_less_diff [simp]: "(0 < n - (m::nat)) = (m < n)" |
|
24438 | 1007 |
by (induct m n rule: diff_induct) simp_all |
13449 | 1008 |
|
22718 | 1009 |
lemma less_imp_add_positive: |
1010 |
assumes "i < j" |
|
1011 |
shows "\<exists>k::nat. 0 < k & i + k = j" |
|
1012 |
proof |
|
1013 |
from assms show "0 < j - i & i + (j - i) = j" |
|
23476 | 1014 |
by (simp add: order_less_imp_le) |
22718 | 1015 |
qed |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
1016 |
|
13449 | 1017 |
lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)" |
24438 | 1018 |
by (induct k) simp_all |
13449 | 1019 |
|
1020 |
lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)" |
|
24438 | 1021 |
by (simp add: diff_cancel add_commute) |
13449 | 1022 |
|
1023 |
lemma diff_add_0: "n - (n + m) = (0::nat)" |
|
24438 | 1024 |
by (induct n) simp_all |
13449 | 1025 |
|
1026 |
||
1027 |
text {* Difference distributes over multiplication *} |
|
1028 |
||
1029 |
lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)" |
|
24438 | 1030 |
by (induct m n rule: diff_induct) (simp_all add: diff_cancel) |
13449 | 1031 |
|
1032 |
lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)" |
|
24438 | 1033 |
by (simp add: diff_mult_distrib mult_commute [of k]) |
13449 | 1034 |
-- {* NOT added as rewrites, since sometimes they are used from right-to-left *} |
1035 |
||
1036 |
lemmas nat_distrib = |
|
1037 |
add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2 |
|
1038 |
||
1039 |
||
1040 |
subsection {* Monotonicity of Multiplication *} |
|
1041 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1042 |
lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k" |
24438 | 1043 |
by (simp add: mult_right_mono) |
13449 | 1044 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1045 |
lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j" |
24438 | 1046 |
by (simp add: mult_left_mono) |
13449 | 1047 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1048 |
text {* @{text "\<le>"} monotonicity, BOTH arguments *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1049 |
lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l" |
24438 | 1050 |
by (simp add: mult_mono) |
13449 | 1051 |
|
1052 |
lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k" |
|
24438 | 1053 |
by (simp add: mult_strict_right_mono) |
13449 | 1054 |
|
14266 | 1055 |
text{*Differs from the standard @{text zero_less_mult_iff} in that |
1056 |
there are no negative numbers.*} |
|
1057 |
lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)" |
|
13449 | 1058 |
apply (induct m) |
22718 | 1059 |
apply simp |
1060 |
apply (case_tac n) |
|
1061 |
apply simp_all |
|
13449 | 1062 |
done |
1063 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1064 |
lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)" |
13449 | 1065 |
apply (induct m) |
22718 | 1066 |
apply simp |
1067 |
apply (case_tac n) |
|
1068 |
apply simp_all |
|
13449 | 1069 |
done |
1070 |
||
1071 |
lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)" |
|
22718 | 1072 |
apply (induct m) |
1073 |
apply simp |
|
1074 |
apply (induct n) |
|
1075 |
apply auto |
|
13449 | 1076 |
done |
1077 |
||
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24196
diff
changeset
|
1078 |
lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)" |
13449 | 1079 |
apply (rule trans) |
14208 | 1080 |
apply (rule_tac [2] mult_eq_1_iff, fastsimp) |
13449 | 1081 |
done |
1082 |
||
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
1083 |
lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)" |
13449 | 1084 |
apply (safe intro!: mult_less_mono1) |
14208 | 1085 |
apply (case_tac k, auto) |
13449 | 1086 |
apply (simp del: le_0_eq add: linorder_not_le [symmetric]) |
1087 |
apply (blast intro: mult_le_mono1) |
|
1088 |
done |
|
1089 |
||
1090 |
lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)" |
|
24438 | 1091 |
by (simp add: mult_commute [of k]) |
13449 | 1092 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1093 |
lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)" |
24438 | 1094 |
by (simp add: linorder_not_less [symmetric], auto) |
13449 | 1095 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1096 |
lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)" |
24438 | 1097 |
by (simp add: linorder_not_less [symmetric], auto) |
13449 | 1098 |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
1099 |
lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))" |
25162 | 1100 |
apply (cut_tac less_linear, safe, auto) |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
1101 |
apply (drule mult_less_mono1, assumption, simp)+ |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
1102 |
done |
13449 | 1103 |
|
1104 |
lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))" |
|
24438 | 1105 |
by (simp add: mult_commute [of k]) |
13449 | 1106 |
|
1107 |
lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)" |
|
24438 | 1108 |
by (subst mult_less_cancel1) simp |
13449 | 1109 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1110 |
lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)" |
24438 | 1111 |
by (subst mult_le_cancel1) simp |
13449 | 1112 |
|
1113 |
lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)" |
|
24438 | 1114 |
by (subst mult_cancel1) simp |
13449 | 1115 |
|
1116 |
text {* Lemma for @{text gcd} *} |
|
1117 |
lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0" |
|
1118 |
apply (drule sym) |
|
1119 |
apply (rule disjCI) |
|
1120 |
apply (rule nat_less_cases, erule_tac [2] _) |
|
25157 | 1121 |
apply (drule_tac [2] mult_less_mono2) |
25162 | 1122 |
apply (auto) |
13449 | 1123 |
done |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
1124 |
|
20588 | 1125 |
|
24995 | 1126 |
subsection {* size of a datatype value *} |
1127 |
||
1128 |
class size = type + |
|
1129 |
fixes size :: "'a \<Rightarrow> nat" |
|
1130 |
||
1131 |
use "Tools/function_package/size.ML" |
|
1132 |
||
1133 |
setup Size.setup |
|
1134 |
||
1135 |
lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n" |
|
25162 | 1136 |
by (induct n) simp_all |
24995 | 1137 |
|
1138 |
lemma size_bool [code func]: |
|
1139 |
"size (b\<Colon>bool) = 0" by (cases b) auto |
|
1140 |
||
1141 |
declare "*.size" [noatp] |
|
1142 |
||
1143 |
||
18702 | 1144 |
subsection {* Code generator setup *} |
1145 |
||
20588 | 1146 |
lemma [code func]: |
25145 | 1147 |
"(0\<Colon>nat) \<le> m \<longleftrightarrow> True" |
1148 |
"Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m" |
|
1149 |
"(n\<Colon>nat) < 0 \<longleftrightarrow> False" |
|
1150 |
"(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m" |
|
22348 | 1151 |
using Suc_le_eq less_Suc_eq_le by simp_all |
20588 | 1152 |
|
21243 | 1153 |
|
25193 | 1154 |
subsection {* Embedding of the Naturals into any |
1155 |
@{text semiring_1}: @{term of_nat} *} |
|
24196 | 1156 |
|
1157 |
context semiring_1 |
|
1158 |
begin |
|
1159 |
||
25559 | 1160 |
primrec |
1161 |
of_nat :: "nat \<Rightarrow> 'a" |
|
1162 |
where |
|
1163 |
of_nat_0: "of_nat 0 = 0" |
|
1164 |
| of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m" |
|
25193 | 1165 |
|
1166 |
lemma of_nat_1 [simp]: "of_nat 1 = 1" |
|
1167 |
by simp |
|
1168 |
||
1169 |
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n" |
|
1170 |
by (induct m) (simp_all add: add_ac) |
|
1171 |
||
1172 |
lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n" |
|
1173 |
by (induct m) (simp_all add: add_ac left_distrib) |
|
1174 |
||
24196 | 1175 |
end |
1176 |
||
25193 | 1177 |
context ordered_semidom |
1178 |
begin |
|
1179 |
||
1180 |
lemma zero_le_imp_of_nat: "0 \<le> of_nat m" |
|
1181 |
apply (induct m, simp_all) |
|
1182 |
apply (erule order_trans) |
|
1183 |
apply (rule ord_le_eq_trans [OF _ add_commute]) |
|
1184 |
apply (rule less_add_one [THEN less_imp_le]) |
|
1185 |
done |
|
1186 |
||
1187 |
lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n" |
|
1188 |
apply (induct m n rule: diff_induct, simp_all) |
|
1189 |
apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force) |
|
1190 |
done |
|
1191 |
||
1192 |
lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n" |
|
1193 |
apply (induct m n rule: diff_induct, simp_all) |
|
1194 |
apply (insert zero_le_imp_of_nat) |
|
1195 |
apply (force simp add: not_less [symmetric]) |
|
1196 |
done |
|
1197 |
||
1198 |
lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n" |
|
1199 |
by (blast intro: of_nat_less_imp_less less_imp_of_nat_less) |
|
1200 |
||
1201 |
text{*Special cases where either operand is zero*} |
|
1202 |
||
1203 |
lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n" |
|
1204 |
by (rule of_nat_less_iff [of 0, simplified]) |
|
1205 |
||
1206 |
lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0" |
|
1207 |
by (rule of_nat_less_iff [of _ 0, simplified]) |
|
1208 |
||
1209 |
lemma of_nat_le_iff [simp]: |
|
1210 |
"of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n" |
|
1211 |
by (simp add: not_less [symmetric] linorder_not_less [symmetric]) |
|
1212 |
||
1213 |
text{*Special cases where either operand is zero*} |
|
1214 |
||
1215 |
lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n" |
|
1216 |
by (rule of_nat_le_iff [of 0, simplified]) |
|
1217 |
||
1218 |
lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0" |
|
1219 |
by (rule of_nat_le_iff [of _ 0, simplified]) |
|
1220 |
||
1221 |
end |
|
1222 |
||
1223 |
lemma of_nat_id [simp]: "of_nat n = n" |
|
1224 |
by (induct n) auto |
|
1225 |
||
1226 |
lemma of_nat_eq_id [simp]: "of_nat = id" |
|
1227 |
by (auto simp add: expand_fun_eq) |
|
1228 |
||
1229 |
text{*Class for unital semirings with characteristic zero. |
|
1230 |
Includes non-ordered rings like the complex numbers.*} |
|
1231 |
||
1232 |
class semiring_char_0 = semiring_1 + |
|
1233 |
assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n" |
|
1234 |
||
1235 |
text{*Every @{text ordered_semidom} has characteristic zero.*} |
|
1236 |
||
1237 |
subclass (in ordered_semidom) semiring_char_0 |
|
1238 |
by unfold_locales (simp add: eq_iff order_eq_iff) |
|
1239 |
||
1240 |
context semiring_char_0 |
|
1241 |
begin |
|
1242 |
||
1243 |
text{*Special cases where either operand is zero*} |
|
1244 |
||
1245 |
lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n" |
|
1246 |
by (rule of_nat_eq_iff [of 0, simplified]) |
|
1247 |
||
1248 |
lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0" |
|
1249 |
by (rule of_nat_eq_iff [of _ 0, simplified]) |
|
1250 |
||
1251 |
lemma inj_of_nat: "inj of_nat" |
|
1252 |
by (simp add: inj_on_def) |
|
1253 |
||
1254 |
end |
|
1255 |
||
1256 |
||
21243 | 1257 |
subsection {* Further Arithmetic Facts Concerning the Natural Numbers *} |
1258 |
||
22845 | 1259 |
lemma subst_equals: |
1260 |
assumes 1: "t = s" and 2: "u = t" |
|
1261 |
shows "u = s" |
|
1262 |
using 2 1 by (rule trans) |
|
1263 |
||
21243 | 1264 |
use "arith_data.ML" |
24091 | 1265 |
declaration {* K arith_data_setup *} |
1266 |
||
1267 |
use "Tools/lin_arith.ML" |
|
1268 |
declaration {* K LinArith.setup *} |
|
1269 |
||
21243 | 1270 |
|
1271 |
text{*The following proofs may rely on the arithmetic proof procedures.*} |
|
1272 |
||
1273 |
lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)" |
|
24438 | 1274 |
by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add) |
21243 | 1275 |
|
1276 |
lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)" |
|
24438 | 1277 |
by (simp add: less_eq reflcl_trancl [symmetric] del: reflcl_trancl, arith) |
21243 | 1278 |
|
1279 |
lemma nat_diff_split: |
|
22718 | 1280 |
"P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))" |
21243 | 1281 |
-- {* elimination of @{text -} on @{text nat} *} |
24438 | 1282 |
by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2]) |
21243 | 1283 |
|
25193 | 1284 |
context ring_1 |
1285 |
begin |
|
1286 |
||
1287 |
lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n" |
|
1288 |
by (simp del: of_nat_add |
|
1289 |
add: compare_rls of_nat_add [symmetric] split add: nat_diff_split) |
|
1290 |
||
1291 |
end |
|
1292 |
||
1293 |
lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n" |
|
25231 | 1294 |
unfolding abs_if by auto |
25193 | 1295 |
|
21243 | 1296 |
lemma nat_diff_split_asm: |
25162 | 1297 |
"P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))" |
21243 | 1298 |
-- {* elimination of @{text -} on @{text nat} in assumptions *} |
24438 | 1299 |
by (simp split: nat_diff_split) |
21243 | 1300 |
|
1301 |
lemmas [arith_split] = nat_diff_split split_min split_max |
|
1302 |
||
1303 |
||
1304 |
lemma le_square: "m \<le> m * (m::nat)" |
|
24438 | 1305 |
by (induct m) auto |
21243 | 1306 |
|
1307 |
lemma le_cube: "(m::nat) \<le> m * (m * m)" |
|
24438 | 1308 |
by (induct m) auto |
21243 | 1309 |
|
1310 |
||
1311 |
text{*Subtraction laws, mostly by Clemens Ballarin*} |
|
1312 |
||
1313 |
lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c" |
|
24438 | 1314 |
by arith |
21243 | 1315 |
|
1316 |
lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))" |
|
24438 | 1317 |
by arith |
21243 | 1318 |
|
1319 |
lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)" |
|
24438 | 1320 |
by arith |
21243 | 1321 |
|
1322 |
lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))" |
|
24438 | 1323 |
by arith |
21243 | 1324 |
|
1325 |
lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i" |
|
24438 | 1326 |
by arith |
21243 | 1327 |
|
1328 |
lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k" |
|
24438 | 1329 |
by arith |
21243 | 1330 |
|
1331 |
(*Replaces the previous diff_less and le_diff_less, which had the stronger |
|
1332 |
second premise n\<le>m*) |
|
1333 |
lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m" |
|
24438 | 1334 |
by arith |
21243 | 1335 |
|
1336 |
||
1337 |
(** Simplification of relational expressions involving subtraction **) |
|
1338 |
||
1339 |
lemma diff_diff_eq: "[| k \<le> m; k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)" |
|
24438 | 1340 |
by (simp split add: nat_diff_split) |
21243 | 1341 |
|
1342 |
lemma eq_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)" |
|
24438 | 1343 |
by (auto split add: nat_diff_split) |
21243 | 1344 |
|
1345 |
lemma less_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)" |
|
24438 | 1346 |
by (auto split add: nat_diff_split) |
21243 | 1347 |
|
1348 |
lemma le_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)" |
|
24438 | 1349 |
by (auto split add: nat_diff_split) |
21243 | 1350 |
|
1351 |
||
1352 |
text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*} |
|
1353 |
||
1354 |
(* Monotonicity of subtraction in first argument *) |
|
1355 |
lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)" |
|
24438 | 1356 |
by (simp split add: nat_diff_split) |
21243 | 1357 |
|
1358 |
lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)" |
|
24438 | 1359 |
by (simp split add: nat_diff_split) |
21243 | 1360 |
|
1361 |
lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)" |
|
24438 | 1362 |
by (simp split add: nat_diff_split) |
21243 | 1363 |
|
1364 |
lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n" |
|
24438 | 1365 |
by (simp split add: nat_diff_split) |
21243 | 1366 |
|
1367 |
text{*Lemmas for ex/Factorization*} |
|
1368 |
||
1369 |
lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n" |
|
24438 | 1370 |
by (cases m) auto |
21243 | 1371 |
|
1372 |
lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n" |
|
24438 | 1373 |
by (cases m) auto |
21243 | 1374 |
|
1375 |
lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m" |
|
24438 | 1376 |
by (cases m) auto |
21243 | 1377 |
|
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1378 |
text {* Specialized induction principles that work "backwards": *} |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1379 |
|
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1380 |
lemma inc_induct[consumes 1, case_names base step]: |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1381 |
assumes less: "i <= j" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1382 |
assumes base: "P j" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1383 |
assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1384 |
shows "P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1385 |
using less |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1386 |
proof (induct d=="j - i" arbitrary: i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1387 |
case (0 i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1388 |
hence "i = j" by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1389 |
with base show ?case by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1390 |
next |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1391 |
case (Suc d i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1392 |
hence "i < j" "P (Suc i)" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1393 |
by simp_all |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1394 |
thus "P i" by (rule step) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1395 |
qed |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1396 |
|
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1397 |
lemma strict_inc_induct[consumes 1, case_names base step]: |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1398 |
assumes less: "i < j" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1399 |
assumes base: "!!i. j = Suc i ==> P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1400 |
assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1401 |
shows "P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1402 |
using less |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1403 |
proof (induct d=="j - i - 1" arbitrary: i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1404 |
case (0 i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1405 |
with `i < j` have "j = Suc i" by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1406 |
with base show ?case by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1407 |
next |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1408 |
case (Suc d i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1409 |
hence "i < j" "P (Suc i)" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1410 |
by simp_all |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1411 |
thus "P i" by (rule step) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1412 |
qed |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1413 |
|
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1414 |
lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1415 |
using inc_induct[of "k - i" k P, simplified] by blast |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1416 |
|
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1417 |
lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1418 |
using inc_induct[of 0 k P] by blast |
21243 | 1419 |
|
1420 |
text{*Rewriting to pull differences out*} |
|
1421 |
||
1422 |
lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j" |
|
24438 | 1423 |
by arith |
21243 | 1424 |
|
1425 |
lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j" |
|
24438 | 1426 |
by arith |
21243 | 1427 |
|
1428 |
lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)" |
|
24438 | 1429 |
by arith |
21243 | 1430 |
|
1431 |
(*The others are |
|
1432 |
i - j - k = i - (j + k), |
|
1433 |
k \<le> j ==> j - k + i = j + i - k, |
|
1434 |
k \<le> j ==> i + (j - k) = i + j - k *) |
|
1435 |
lemmas add_diff_assoc = diff_add_assoc [symmetric] |
|
1436 |
lemmas add_diff_assoc2 = diff_add_assoc2[symmetric] |
|
1437 |
declare diff_diff_left [simp] add_diff_assoc [simp] add_diff_assoc2[simp] |
|
1438 |
||
1439 |
text{*At present we prove no analogue of @{text not_less_Least} or @{text |
|
1440 |
Least_Suc}, since there appears to be no need.*} |
|
1441 |
||
22718 | 1442 |
|
25193 | 1443 |
subsection {*The Set of Natural Numbers*} |
21243 | 1444 |
|
24196 | 1445 |
context semiring_1 |
1446 |
begin |
|
21243 | 1447 |
|
25193 | 1448 |
definition |
25382 | 1449 |
Nats :: "'a set" where |
25193 | 1450 |
"Nats = range of_nat" |
24196 | 1451 |
|
23852 | 1452 |
notation (xsymbols) |
1453 |
Nats ("\<nat>") |
|
1454 |
||
25193 | 1455 |
lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>" |
1456 |
by (simp add: Nats_def) |
|
1457 |
||
1458 |
lemma Nats_0 [simp]: "0 \<in> \<nat>" |
|
23852 | 1459 |
apply (simp add: Nats_def) |
1460 |
apply (rule range_eqI) |
|
1461 |
apply (rule of_nat_0 [symmetric]) |
|
1462 |
done |
|
1463 |
||
25193 | 1464 |
lemma Nats_1 [simp]: "1 \<in> \<nat>" |
23852 | 1465 |
apply (simp add: Nats_def) |
1466 |
apply (rule range_eqI) |
|
1467 |
apply (rule of_nat_1 [symmetric]) |
|
1468 |
done |
|
1469 |
||
25193 | 1470 |
lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>" |
23852 | 1471 |
apply (auto simp add: Nats_def) |
1472 |
apply (rule range_eqI) |
|
1473 |
apply (rule of_nat_add [symmetric]) |
|
1474 |
done |
|
1475 |
||
25193 | 1476 |
lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>" |
23852 | 1477 |
apply (auto simp add: Nats_def) |
1478 |
apply (rule range_eqI) |
|
1479 |
apply (rule of_nat_mult [symmetric]) |
|
1480 |
done |
|
1481 |
||
25193 | 1482 |
end |
23852 | 1483 |
|
1484 |
||
24995 | 1485 |
text {* the lattice order on @{typ nat} *} |
1486 |
||
25559 | 1487 |
instantiation nat :: distrib_lattice |
1488 |
begin |
|
1489 |
||
1490 |
definition |
|
25510 | 1491 |
"(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min" |
25559 | 1492 |
|
1493 |
definition |
|
25510 | 1494 |
"(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max" |
25559 | 1495 |
|
1496 |
instance by intro_classes |
|
1497 |
(simp_all add: inf_nat_def sup_nat_def) |
|
1498 |
||
1499 |
end |
|
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24523
diff
changeset
|
1500 |
|
22157 | 1501 |
|
24196 | 1502 |
subsection {* legacy bindings *} |
1503 |
||
1504 |
ML |
|
1505 |
{* |
|
1506 |
val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le"; |
|
1507 |
val nat_diff_split = thm "nat_diff_split"; |
|
1508 |
val nat_diff_split_asm = thm "nat_diff_split_asm"; |
|
1509 |
val le_square = thm "le_square"; |
|
1510 |
val le_cube = thm "le_cube"; |
|
1511 |
val diff_less_mono = thm "diff_less_mono"; |
|
1512 |
val less_diff_conv = thm "less_diff_conv"; |
|
1513 |
val le_diff_conv = thm "le_diff_conv"; |
|
1514 |
val le_diff_conv2 = thm "le_diff_conv2"; |
|
1515 |
val diff_diff_cancel = thm "diff_diff_cancel"; |
|
1516 |
val le_add_diff = thm "le_add_diff"; |
|
1517 |
val diff_less = thm "diff_less"; |
|
1518 |
val diff_diff_eq = thm "diff_diff_eq"; |
|
1519 |
val eq_diff_iff = thm "eq_diff_iff"; |
|
1520 |
val less_diff_iff = thm "less_diff_iff"; |
|
1521 |
val le_diff_iff = thm "le_diff_iff"; |
|
1522 |
val diff_le_mono = thm "diff_le_mono"; |
|
1523 |
val diff_le_mono2 = thm "diff_le_mono2"; |
|
1524 |
val diff_less_mono2 = thm "diff_less_mono2"; |
|
1525 |
val diffs0_imp_equal = thm "diffs0_imp_equal"; |
|
1526 |
val one_less_mult = thm "one_less_mult"; |
|
1527 |
val n_less_m_mult_n = thm "n_less_m_mult_n"; |
|
1528 |
val n_less_n_mult_m = thm "n_less_n_mult_m"; |
|
1529 |
val diff_diff_right = thm "diff_diff_right"; |
|
1530 |
val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1"; |
|
1531 |
val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2"; |
|
1532 |
*} |
|
1533 |
||
923 | 1534 |
end |