author | wenzelm |
Fri, 13 May 2011 23:58:40 +0200 | |
changeset 42795 | 66fcc9882784 |
parent 41855 | c3b6e69da386 |
child 42993 | da014b00d7a4 |
permissions | -rw-r--r-- |
11355 | 1 |
(* Title: HOL/Library/Nat_Infinity.thy |
27110 | 2 |
Author: David von Oheimb, TU Muenchen; Florian Haftmann, TU Muenchen |
41853 | 3 |
Contributions: David Trachtenherz, TU Muenchen |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
4 |
*) |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
5 |
|
14706 | 6 |
header {* Natural numbers with infinity *} |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
7 |
|
15131 | 8 |
theory Nat_Infinity |
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
29668
diff
changeset
|
9 |
imports Main |
15131 | 10 |
begin |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
11 |
|
27110 | 12 |
subsection {* Type definition *} |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
13 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
14 |
text {* |
11355 | 15 |
We extend the standard natural numbers by a special value indicating |
27110 | 16 |
infinity. |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
17 |
*} |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
18 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
19 |
datatype inat = Fin nat | Infty |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
20 |
|
21210 | 21 |
notation (xsymbols) |
19736 | 22 |
Infty ("\<infinity>") |
23 |
||
21210 | 24 |
notation (HTML output) |
19736 | 25 |
Infty ("\<infinity>") |
26 |
||
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
27 |
|
31084 | 28 |
lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)" |
29 |
by (cases x) auto |
|
30 |
||
31 |
lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)" |
|
31077 | 32 |
by (cases x) auto |
33 |
||
34 |
||
41855 | 35 |
primrec the_Fin :: "inat \<Rightarrow> nat" |
36 |
where "the_Fin (Fin n) = n" |
|
37 |
||
38 |
||
27110 | 39 |
subsection {* Constructors and numbers *} |
40 |
||
41 |
instantiation inat :: "{zero, one, number}" |
|
25594 | 42 |
begin |
43 |
||
44 |
definition |
|
27110 | 45 |
"0 = Fin 0" |
25594 | 46 |
|
47 |
definition |
|
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset
|
48 |
[code_unfold]: "1 = Fin 1" |
25594 | 49 |
|
50 |
definition |
|
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset
|
51 |
[code_unfold, code del]: "number_of k = Fin (number_of k)" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
52 |
|
25594 | 53 |
instance .. |
54 |
||
55 |
end |
|
56 |
||
27110 | 57 |
definition iSuc :: "inat \<Rightarrow> inat" where |
58 |
"iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)" |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
59 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
60 |
lemma Fin_0: "Fin 0 = 0" |
27110 | 61 |
by (simp add: zero_inat_def) |
62 |
||
63 |
lemma Fin_1: "Fin 1 = 1" |
|
64 |
by (simp add: one_inat_def) |
|
65 |
||
66 |
lemma Fin_number: "Fin (number_of k) = number_of k" |
|
67 |
by (simp add: number_of_inat_def) |
|
68 |
||
69 |
lemma one_iSuc: "1 = iSuc 0" |
|
70 |
by (simp add: zero_inat_def one_inat_def iSuc_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
71 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
72 |
lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0" |
27110 | 73 |
by (simp add: zero_inat_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
74 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
75 |
lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>" |
27110 | 76 |
by (simp add: zero_inat_def) |
77 |
||
78 |
lemma zero_inat_eq [simp]: |
|
79 |
"number_of k = (0\<Colon>inat) \<longleftrightarrow> number_of k = (0\<Colon>nat)" |
|
80 |
"(0\<Colon>inat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)" |
|
81 |
unfolding zero_inat_def number_of_inat_def by simp_all |
|
82 |
||
83 |
lemma one_inat_eq [simp]: |
|
84 |
"number_of k = (1\<Colon>inat) \<longleftrightarrow> number_of k = (1\<Colon>nat)" |
|
85 |
"(1\<Colon>inat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)" |
|
86 |
unfolding one_inat_def number_of_inat_def by simp_all |
|
87 |
||
88 |
lemma zero_one_inat_neq [simp]: |
|
89 |
"\<not> 0 = (1\<Colon>inat)" |
|
90 |
"\<not> 1 = (0\<Colon>inat)" |
|
91 |
unfolding zero_inat_def one_inat_def by simp_all |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
92 |
|
27110 | 93 |
lemma Infty_ne_i1 [simp]: "\<infinity> \<noteq> 1" |
94 |
by (simp add: one_inat_def) |
|
95 |
||
96 |
lemma i1_ne_Infty [simp]: "1 \<noteq> \<infinity>" |
|
97 |
by (simp add: one_inat_def) |
|
98 |
||
99 |
lemma Infty_ne_number [simp]: "\<infinity> \<noteq> number_of k" |
|
100 |
by (simp add: number_of_inat_def) |
|
101 |
||
102 |
lemma number_ne_Infty [simp]: "number_of k \<noteq> \<infinity>" |
|
103 |
by (simp add: number_of_inat_def) |
|
104 |
||
105 |
lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)" |
|
106 |
by (simp add: iSuc_def) |
|
107 |
||
108 |
lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))" |
|
109 |
by (simp add: iSuc_Fin number_of_inat_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
110 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
111 |
lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>" |
27110 | 112 |
by (simp add: iSuc_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
113 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
114 |
lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0" |
27110 | 115 |
by (simp add: iSuc_def zero_inat_def split: inat.splits) |
116 |
||
117 |
lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n" |
|
118 |
by (rule iSuc_ne_0 [symmetric]) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
119 |
|
27110 | 120 |
lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n" |
121 |
by (simp add: iSuc_def split: inat.splits) |
|
122 |
||
123 |
lemma number_of_inat_inject [simp]: |
|
124 |
"(number_of k \<Colon> inat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l" |
|
125 |
by (simp add: number_of_inat_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
126 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
127 |
|
27110 | 128 |
subsection {* Addition *} |
129 |
||
130 |
instantiation inat :: comm_monoid_add |
|
131 |
begin |
|
132 |
||
38167 | 133 |
definition [nitpick_simp]: |
37765 | 134 |
"m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
135 |
|
27110 | 136 |
lemma plus_inat_simps [simp, code]: |
137 |
"Fin m + Fin n = Fin (m + n)" |
|
138 |
"\<infinity> + q = \<infinity>" |
|
139 |
"q + \<infinity> = \<infinity>" |
|
140 |
by (simp_all add: plus_inat_def split: inat.splits) |
|
141 |
||
142 |
instance proof |
|
143 |
fix n m q :: inat |
|
144 |
show "n + m + q = n + (m + q)" |
|
145 |
by (cases n, auto, cases m, auto, cases q, auto) |
|
146 |
show "n + m = m + n" |
|
147 |
by (cases n, auto, cases m, auto) |
|
148 |
show "0 + n = n" |
|
149 |
by (cases n) (simp_all add: zero_inat_def) |
|
26089 | 150 |
qed |
151 |
||
27110 | 152 |
end |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
153 |
|
27110 | 154 |
lemma plus_inat_0 [simp]: |
155 |
"0 + (q\<Colon>inat) = q" |
|
156 |
"(q\<Colon>inat) + 0 = q" |
|
157 |
by (simp_all add: plus_inat_def zero_inat_def split: inat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
158 |
|
27110 | 159 |
lemma plus_inat_number [simp]: |
29012 | 160 |
"(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l |
161 |
else if l < Int.Pls then number_of k else number_of (k + l))" |
|
27110 | 162 |
unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] .. |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
163 |
|
27110 | 164 |
lemma iSuc_number [simp]: |
165 |
"iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))" |
|
166 |
unfolding iSuc_number_of |
|
167 |
unfolding one_inat_def number_of_inat_def Suc_nat_number_of if_distrib [symmetric] .. |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
168 |
|
27110 | 169 |
lemma iSuc_plus_1: |
170 |
"iSuc n = n + 1" |
|
171 |
by (cases n) (simp_all add: iSuc_Fin one_inat_def) |
|
172 |
||
173 |
lemma plus_1_iSuc: |
|
174 |
"1 + q = iSuc q" |
|
175 |
"q + 1 = iSuc q" |
|
41853 | 176 |
by (simp_all add: iSuc_plus_1 add_ac) |
177 |
||
178 |
lemma iadd_Suc: "iSuc m + n = iSuc (m + n)" |
|
179 |
by (simp_all add: iSuc_plus_1 add_ac) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
180 |
|
41853 | 181 |
lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)" |
182 |
by (simp only: add_commute[of m] iadd_Suc) |
|
183 |
||
184 |
lemma iadd_is_0: "(m + n = (0::inat)) = (m = 0 \<and> n = 0)" |
|
185 |
by (cases m, cases n, simp_all add: zero_inat_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
186 |
|
29014 | 187 |
subsection {* Multiplication *} |
188 |
||
189 |
instantiation inat :: comm_semiring_1 |
|
190 |
begin |
|
191 |
||
38167 | 192 |
definition times_inat_def [nitpick_simp]: |
29014 | 193 |
"m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow> |
194 |
(case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))" |
|
195 |
||
196 |
lemma times_inat_simps [simp, code]: |
|
197 |
"Fin m * Fin n = Fin (m * n)" |
|
198 |
"\<infinity> * \<infinity> = \<infinity>" |
|
199 |
"\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)" |
|
200 |
"Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)" |
|
201 |
unfolding times_inat_def zero_inat_def |
|
202 |
by (simp_all split: inat.split) |
|
203 |
||
204 |
instance proof |
|
205 |
fix a b c :: inat |
|
206 |
show "(a * b) * c = a * (b * c)" |
|
207 |
unfolding times_inat_def zero_inat_def |
|
208 |
by (simp split: inat.split) |
|
209 |
show "a * b = b * a" |
|
210 |
unfolding times_inat_def zero_inat_def |
|
211 |
by (simp split: inat.split) |
|
212 |
show "1 * a = a" |
|
213 |
unfolding times_inat_def zero_inat_def one_inat_def |
|
214 |
by (simp split: inat.split) |
|
215 |
show "(a + b) * c = a * c + b * c" |
|
216 |
unfolding times_inat_def zero_inat_def |
|
217 |
by (simp split: inat.split add: left_distrib) |
|
218 |
show "0 * a = 0" |
|
219 |
unfolding times_inat_def zero_inat_def |
|
220 |
by (simp split: inat.split) |
|
221 |
show "a * 0 = 0" |
|
222 |
unfolding times_inat_def zero_inat_def |
|
223 |
by (simp split: inat.split) |
|
224 |
show "(0::inat) \<noteq> 1" |
|
225 |
unfolding zero_inat_def one_inat_def |
|
226 |
by simp |
|
227 |
qed |
|
228 |
||
229 |
end |
|
230 |
||
231 |
lemma mult_iSuc: "iSuc m * n = n + m * n" |
|
29667 | 232 |
unfolding iSuc_plus_1 by (simp add: algebra_simps) |
29014 | 233 |
|
234 |
lemma mult_iSuc_right: "m * iSuc n = m + m * n" |
|
29667 | 235 |
unfolding iSuc_plus_1 by (simp add: algebra_simps) |
29014 | 236 |
|
29023 | 237 |
lemma of_nat_eq_Fin: "of_nat n = Fin n" |
238 |
apply (induct n) |
|
239 |
apply (simp add: Fin_0) |
|
240 |
apply (simp add: plus_1_iSuc iSuc_Fin) |
|
241 |
done |
|
242 |
||
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
38167
diff
changeset
|
243 |
instance inat :: semiring_char_0 proof |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
38167
diff
changeset
|
244 |
have "inj Fin" by (rule injI) simp |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
38167
diff
changeset
|
245 |
then show "inj (\<lambda>n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin) |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
38167
diff
changeset
|
246 |
qed |
29023 | 247 |
|
41853 | 248 |
lemma imult_is_0[simp]: "((m::inat) * n = 0) = (m = 0 \<or> n = 0)" |
249 |
by(auto simp add: times_inat_def zero_inat_def split: inat.split) |
|
250 |
||
251 |
lemma imult_is_Infty: "((a::inat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)" |
|
252 |
by(auto simp add: times_inat_def zero_inat_def split: inat.split) |
|
253 |
||
254 |
||
255 |
subsection {* Subtraction *} |
|
256 |
||
257 |
instantiation inat :: minus |
|
258 |
begin |
|
259 |
||
260 |
definition diff_inat_def: |
|
261 |
"a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0) |
|
262 |
| \<infinity> \<Rightarrow> \<infinity>)" |
|
263 |
||
264 |
instance .. |
|
265 |
||
266 |
end |
|
267 |
||
268 |
lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)" |
|
269 |
by(simp add: diff_inat_def) |
|
270 |
||
271 |
lemma idiff_Infty[simp,code]: "\<infinity> - n = \<infinity>" |
|
272 |
by(simp add: diff_inat_def) |
|
273 |
||
274 |
lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0" |
|
275 |
by(simp add: diff_inat_def) |
|
276 |
||
277 |
lemma idiff_0[simp]: "(0::inat) - n = 0" |
|
278 |
by (cases n, simp_all add: zero_inat_def) |
|
279 |
||
280 |
lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_inat_def] |
|
281 |
||
282 |
lemma idiff_0_right[simp]: "(n::inat) - 0 = n" |
|
283 |
by (cases n) (simp_all add: zero_inat_def) |
|
284 |
||
285 |
lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_inat_def] |
|
286 |
||
287 |
lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::inat) - n = 0" |
|
288 |
by(auto simp: zero_inat_def) |
|
289 |
||
41855 | 290 |
lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m" |
291 |
by(simp add: iSuc_def split: inat.split) |
|
292 |
||
293 |
lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n" |
|
294 |
by(simp add: one_inat_def iSuc_Fin[symmetric] zero_inat_def[symmetric]) |
|
295 |
||
41853 | 296 |
(*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_inat_def]*) |
297 |
||
29014 | 298 |
|
27110 | 299 |
subsection {* Ordering *} |
300 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32069
diff
changeset
|
301 |
instantiation inat :: linordered_ab_semigroup_add |
27110 | 302 |
begin |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
303 |
|
38167 | 304 |
definition [nitpick_simp]: |
37765 | 305 |
"m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False) |
27110 | 306 |
| \<infinity> \<Rightarrow> True)" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
307 |
|
38167 | 308 |
definition [nitpick_simp]: |
37765 | 309 |
"m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True) |
27110 | 310 |
| \<infinity> \<Rightarrow> False)" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
311 |
|
27110 | 312 |
lemma inat_ord_simps [simp]: |
313 |
"Fin m \<le> Fin n \<longleftrightarrow> m \<le> n" |
|
314 |
"Fin m < Fin n \<longleftrightarrow> m < n" |
|
315 |
"q \<le> \<infinity>" |
|
316 |
"q < \<infinity> \<longleftrightarrow> q \<noteq> \<infinity>" |
|
317 |
"\<infinity> \<le> q \<longleftrightarrow> q = \<infinity>" |
|
318 |
"\<infinity> < q \<longleftrightarrow> False" |
|
319 |
by (simp_all add: less_eq_inat_def less_inat_def split: inat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
320 |
|
27110 | 321 |
lemma inat_ord_code [code]: |
322 |
"Fin m \<le> Fin n \<longleftrightarrow> m \<le> n" |
|
323 |
"Fin m < Fin n \<longleftrightarrow> m < n" |
|
324 |
"q \<le> \<infinity> \<longleftrightarrow> True" |
|
325 |
"Fin m < \<infinity> \<longleftrightarrow> True" |
|
326 |
"\<infinity> \<le> Fin n \<longleftrightarrow> False" |
|
327 |
"\<infinity> < q \<longleftrightarrow> False" |
|
328 |
by simp_all |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
329 |
|
27110 | 330 |
instance by default |
331 |
(auto simp add: less_eq_inat_def less_inat_def plus_inat_def split: inat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
332 |
|
27110 | 333 |
end |
334 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32069
diff
changeset
|
335 |
instance inat :: ordered_comm_semiring |
29014 | 336 |
proof |
337 |
fix a b c :: inat |
|
338 |
assume "a \<le> b" and "0 \<le> c" |
|
339 |
thus "c * a \<le> c * b" |
|
340 |
unfolding times_inat_def less_eq_inat_def zero_inat_def |
|
341 |
by (simp split: inat.splits) |
|
342 |
qed |
|
343 |
||
27110 | 344 |
lemma inat_ord_number [simp]: |
345 |
"(number_of m \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n" |
|
346 |
"(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n" |
|
347 |
by (simp_all add: number_of_inat_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
348 |
|
27110 | 349 |
lemma i0_lb [simp]: "(0\<Colon>inat) \<le> n" |
350 |
by (simp add: zero_inat_def less_eq_inat_def split: inat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
351 |
|
41853 | 352 |
lemma ile0_eq [simp]: "n \<le> (0\<Colon>inat) \<longleftrightarrow> n = 0" |
353 |
by (simp add: zero_inat_def less_eq_inat_def split: inat.splits) |
|
27110 | 354 |
|
355 |
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R" |
|
356 |
by (simp add: zero_inat_def less_eq_inat_def split: inat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
357 |
|
27110 | 358 |
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R" |
359 |
by simp |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
360 |
|
41853 | 361 |
lemma not_iless0 [simp]: "\<not> n < (0\<Colon>inat)" |
27110 | 362 |
by (simp add: zero_inat_def less_inat_def split: inat.splits) |
363 |
||
41853 | 364 |
lemma i0_less [simp]: "(0\<Colon>inat) < n \<longleftrightarrow> n \<noteq> 0" |
365 |
by (simp add: zero_inat_def less_inat_def split: inat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
366 |
|
27110 | 367 |
lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m" |
368 |
by (simp add: iSuc_def less_eq_inat_def split: inat.splits) |
|
369 |
||
370 |
lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m" |
|
371 |
by (simp add: iSuc_def less_inat_def split: inat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
372 |
|
27110 | 373 |
lemma ile_iSuc [simp]: "n \<le> iSuc n" |
374 |
by (simp add: iSuc_def less_eq_inat_def split: inat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
375 |
|
11355 | 376 |
lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0" |
27110 | 377 |
by (simp add: zero_inat_def iSuc_def less_eq_inat_def split: inat.splits) |
378 |
||
379 |
lemma i0_iless_iSuc [simp]: "0 < iSuc n" |
|
380 |
by (simp add: zero_inat_def iSuc_def less_inat_def split: inat.splits) |
|
381 |
||
41853 | 382 |
lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)" |
383 |
by (simp add: zero_inat_def iSuc_def less_inat_def split: inat.split) |
|
384 |
||
27110 | 385 |
lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n" |
386 |
by (simp add: iSuc_def less_eq_inat_def less_inat_def split: inat.splits) |
|
387 |
||
388 |
lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n" |
|
389 |
by (cases n) auto |
|
390 |
||
391 |
lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n" |
|
392 |
by (auto simp add: iSuc_def less_inat_def split: inat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
393 |
|
41853 | 394 |
lemma imult_Infty: "(0::inat) < n \<Longrightarrow> \<infinity> * n = \<infinity>" |
395 |
by (simp add: zero_inat_def less_inat_def split: inat.splits) |
|
396 |
||
397 |
lemma imult_Infty_right: "(0::inat) < n \<Longrightarrow> n * \<infinity> = \<infinity>" |
|
398 |
by (simp add: zero_inat_def less_inat_def split: inat.splits) |
|
399 |
||
400 |
lemma inat_0_less_mult_iff: "(0 < (m::inat) * n) = (0 < m \<and> 0 < n)" |
|
401 |
by (simp only: i0_less imult_is_0, simp) |
|
402 |
||
403 |
lemma mono_iSuc: "mono iSuc" |
|
404 |
by(simp add: mono_def) |
|
405 |
||
406 |
||
27110 | 407 |
lemma min_inat_simps [simp]: |
408 |
"min (Fin m) (Fin n) = Fin (min m n)" |
|
409 |
"min q 0 = 0" |
|
410 |
"min 0 q = 0" |
|
411 |
"min q \<infinity> = q" |
|
412 |
"min \<infinity> q = q" |
|
413 |
by (auto simp add: min_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
414 |
|
27110 | 415 |
lemma max_inat_simps [simp]: |
416 |
"max (Fin m) (Fin n) = Fin (max m n)" |
|
417 |
"max q 0 = q" |
|
418 |
"max 0 q = q" |
|
419 |
"max q \<infinity> = \<infinity>" |
|
420 |
"max \<infinity> q = \<infinity>" |
|
421 |
by (simp_all add: max_def) |
|
422 |
||
423 |
lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k" |
|
424 |
by (cases n) simp_all |
|
425 |
||
426 |
lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k" |
|
427 |
by (cases n) simp_all |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
428 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
429 |
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j" |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
430 |
apply (induct_tac k) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
431 |
apply (simp (no_asm) only: Fin_0) |
27110 | 432 |
apply (fast intro: le_less_trans [OF i0_lb]) |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
433 |
apply (erule exE) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
434 |
apply (drule spec) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
435 |
apply (erule exE) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
436 |
apply (drule ileI1) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
437 |
apply (rule iSuc_Fin [THEN subst]) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
438 |
apply (rule exI) |
27110 | 439 |
apply (erule (1) le_less_trans) |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
440 |
done |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
441 |
|
29337 | 442 |
instantiation inat :: "{bot, top}" |
443 |
begin |
|
444 |
||
445 |
definition bot_inat :: inat where |
|
446 |
"bot_inat = 0" |
|
447 |
||
448 |
definition top_inat :: inat where |
|
449 |
"top_inat = \<infinity>" |
|
450 |
||
451 |
instance proof |
|
452 |
qed (simp_all add: bot_inat_def top_inat_def) |
|
453 |
||
454 |
end |
|
455 |
||
26089 | 456 |
|
27110 | 457 |
subsection {* Well-ordering *} |
26089 | 458 |
|
459 |
lemma less_FinE: |
|
460 |
"[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P" |
|
461 |
by (induct n) auto |
|
462 |
||
463 |
lemma less_InftyE: |
|
464 |
"[| n < Infty; !!k. n = Fin k ==> P |] ==> P" |
|
465 |
by (induct n) auto |
|
466 |
||
467 |
lemma inat_less_induct: |
|
468 |
assumes prem: "!!n. \<forall>m::inat. m < n --> P m ==> P n" shows "P n" |
|
469 |
proof - |
|
470 |
have P_Fin: "!!k. P (Fin k)" |
|
471 |
apply (rule nat_less_induct) |
|
472 |
apply (rule prem, clarify) |
|
473 |
apply (erule less_FinE, simp) |
|
474 |
done |
|
475 |
show ?thesis |
|
476 |
proof (induct n) |
|
477 |
fix nat |
|
478 |
show "P (Fin nat)" by (rule P_Fin) |
|
479 |
next |
|
480 |
show "P Infty" |
|
481 |
apply (rule prem, clarify) |
|
482 |
apply (erule less_InftyE) |
|
483 |
apply (simp add: P_Fin) |
|
484 |
done |
|
485 |
qed |
|
486 |
qed |
|
487 |
||
488 |
instance inat :: wellorder |
|
489 |
proof |
|
27823 | 490 |
fix P and n |
491 |
assume hyp: "(\<And>n\<Colon>inat. (\<And>m\<Colon>inat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)" |
|
492 |
show "P n" by (blast intro: inat_less_induct hyp) |
|
26089 | 493 |
qed |
494 |
||
27110 | 495 |
|
496 |
subsection {* Traditional theorem names *} |
|
497 |
||
498 |
lemmas inat_defs = zero_inat_def one_inat_def number_of_inat_def iSuc_def |
|
499 |
plus_inat_def less_eq_inat_def less_inat_def |
|
500 |
||
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
501 |
end |