author | hoelzl |
Tue, 19 Jul 2011 14:37:49 +0200 | |
changeset 43922 | c6f35921056e |
parent 43921 | e8511be08ddd |
child 43923 | ab93d0190a5d |
permissions | -rw-r--r-- |
43919 | 1 |
(* Title: HOL/Library/Extended_Nat.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 |
|
43919 | 6 |
header {* Extended natural numbers (i.e. with infinity) *} |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
7 |
|
43919 | 8 |
theory Extended_Nat |
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 |
|
43921 | 12 |
class infinity = |
13 |
fixes infinity :: "'a" |
|
14 |
||
15 |
notation (xsymbols) |
|
16 |
infinity ("\<infinity>") |
|
17 |
||
18 |
notation (HTML output) |
|
19 |
infinity ("\<infinity>") |
|
20 |
||
27110 | 21 |
subsection {* Type definition *} |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
22 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
23 |
text {* |
11355 | 24 |
We extend the standard natural numbers by a special value indicating |
27110 | 25 |
infinity. |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
26 |
*} |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
27 |
|
43921 | 28 |
typedef (open) enat = "UNIV :: nat option set" .. |
29 |
||
30 |
definition Fin :: "nat \<Rightarrow> enat" where |
|
31 |
"Fin n = Abs_enat (Some n)" |
|
32 |
||
33 |
instantiation enat :: infinity |
|
34 |
begin |
|
35 |
definition "\<infinity> = Abs_enat None" |
|
36 |
instance proof qed |
|
37 |
end |
|
38 |
||
39 |
rep_datatype Fin "\<infinity> :: enat" |
|
40 |
proof - |
|
41 |
fix P i assume "\<And>j. P (Fin j)" "P \<infinity>" |
|
42 |
then show "P i" |
|
43 |
proof induct |
|
44 |
case (Abs_enat y) then show ?case |
|
45 |
by (cases y rule: option.exhaust) |
|
46 |
(auto simp: Fin_def infinity_enat_def) |
|
47 |
qed |
|
48 |
qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject) |
|
19736 | 49 |
|
43922 | 50 |
declare [[coercion_enabled]] |
51 |
declare [[coercion "Fin::nat\<Rightarrow>enat"]] |
|
19736 | 52 |
|
43921 | 53 |
lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)" |
31084 | 54 |
by (cases x) auto |
55 |
||
43921 | 56 |
lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \<infinity>)" |
31077 | 57 |
by (cases x) auto |
58 |
||
43919 | 59 |
primrec the_Fin :: "enat \<Rightarrow> nat" |
41855 | 60 |
where "the_Fin (Fin n) = n" |
61 |
||
27110 | 62 |
subsection {* Constructors and numbers *} |
63 |
||
43919 | 64 |
instantiation enat :: "{zero, one, number}" |
25594 | 65 |
begin |
66 |
||
67 |
definition |
|
27110 | 68 |
"0 = Fin 0" |
25594 | 69 |
|
70 |
definition |
|
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset
|
71 |
[code_unfold]: "1 = Fin 1" |
25594 | 72 |
|
73 |
definition |
|
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset
|
74 |
[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
|
75 |
|
25594 | 76 |
instance .. |
77 |
||
78 |
end |
|
79 |
||
43919 | 80 |
definition iSuc :: "enat \<Rightarrow> enat" where |
27110 | 81 |
"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
|
82 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
83 |
lemma Fin_0: "Fin 0 = 0" |
43919 | 84 |
by (simp add: zero_enat_def) |
27110 | 85 |
|
86 |
lemma Fin_1: "Fin 1 = 1" |
|
43919 | 87 |
by (simp add: one_enat_def) |
27110 | 88 |
|
89 |
lemma Fin_number: "Fin (number_of k) = number_of k" |
|
43919 | 90 |
by (simp add: number_of_enat_def) |
27110 | 91 |
|
92 |
lemma one_iSuc: "1 = iSuc 0" |
|
43919 | 93 |
by (simp add: zero_enat_def one_enat_def iSuc_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
94 |
|
43921 | 95 |
lemma Infty_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0" |
43919 | 96 |
by (simp add: zero_enat_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
97 |
|
43921 | 98 |
lemma i0_ne_Infty [simp]: "0 \<noteq> (\<infinity>::enat)" |
43919 | 99 |
by (simp add: zero_enat_def) |
27110 | 100 |
|
43919 | 101 |
lemma zero_enat_eq [simp]: |
102 |
"number_of k = (0\<Colon>enat) \<longleftrightarrow> number_of k = (0\<Colon>nat)" |
|
103 |
"(0\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)" |
|
104 |
unfolding zero_enat_def number_of_enat_def by simp_all |
|
27110 | 105 |
|
43919 | 106 |
lemma one_enat_eq [simp]: |
107 |
"number_of k = (1\<Colon>enat) \<longleftrightarrow> number_of k = (1\<Colon>nat)" |
|
108 |
"(1\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)" |
|
109 |
unfolding one_enat_def number_of_enat_def by simp_all |
|
27110 | 110 |
|
43919 | 111 |
lemma zero_one_enat_neq [simp]: |
112 |
"\<not> 0 = (1\<Colon>enat)" |
|
113 |
"\<not> 1 = (0\<Colon>enat)" |
|
114 |
unfolding zero_enat_def one_enat_def by simp_all |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
115 |
|
43921 | 116 |
lemma Infty_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1" |
43919 | 117 |
by (simp add: one_enat_def) |
27110 | 118 |
|
43921 | 119 |
lemma i1_ne_Infty [simp]: "1 \<noteq> (\<infinity>::enat)" |
43919 | 120 |
by (simp add: one_enat_def) |
27110 | 121 |
|
43921 | 122 |
lemma Infty_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k" |
43919 | 123 |
by (simp add: number_of_enat_def) |
27110 | 124 |
|
43921 | 125 |
lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)" |
43919 | 126 |
by (simp add: number_of_enat_def) |
27110 | 127 |
|
128 |
lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)" |
|
129 |
by (simp add: iSuc_def) |
|
130 |
||
131 |
lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))" |
|
43919 | 132 |
by (simp add: iSuc_Fin number_of_enat_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
133 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
134 |
lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>" |
27110 | 135 |
by (simp add: iSuc_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
136 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
137 |
lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0" |
43919 | 138 |
by (simp add: iSuc_def zero_enat_def split: enat.splits) |
27110 | 139 |
|
140 |
lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n" |
|
141 |
by (rule iSuc_ne_0 [symmetric]) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
142 |
|
27110 | 143 |
lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n" |
43919 | 144 |
by (simp add: iSuc_def split: enat.splits) |
27110 | 145 |
|
43919 | 146 |
lemma number_of_enat_inject [simp]: |
147 |
"(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l" |
|
148 |
by (simp add: number_of_enat_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
149 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
150 |
|
27110 | 151 |
subsection {* Addition *} |
152 |
||
43919 | 153 |
instantiation enat :: comm_monoid_add |
27110 | 154 |
begin |
155 |
||
38167 | 156 |
definition [nitpick_simp]: |
37765 | 157 |
"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
|
158 |
|
43919 | 159 |
lemma plus_enat_simps [simp, code]: |
43921 | 160 |
fixes q :: enat |
161 |
shows "Fin m + Fin n = Fin (m + n)" |
|
162 |
and "\<infinity> + q = \<infinity>" |
|
163 |
and "q + \<infinity> = \<infinity>" |
|
43919 | 164 |
by (simp_all add: plus_enat_def split: enat.splits) |
27110 | 165 |
|
166 |
instance proof |
|
43919 | 167 |
fix n m q :: enat |
27110 | 168 |
show "n + m + q = n + (m + q)" |
169 |
by (cases n, auto, cases m, auto, cases q, auto) |
|
170 |
show "n + m = m + n" |
|
171 |
by (cases n, auto, cases m, auto) |
|
172 |
show "0 + n = n" |
|
43919 | 173 |
by (cases n) (simp_all add: zero_enat_def) |
26089 | 174 |
qed |
175 |
||
27110 | 176 |
end |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
177 |
|
43919 | 178 |
lemma plus_enat_0 [simp]: |
179 |
"0 + (q\<Colon>enat) = q" |
|
180 |
"(q\<Colon>enat) + 0 = q" |
|
181 |
by (simp_all add: plus_enat_def zero_enat_def split: enat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
182 |
|
43919 | 183 |
lemma plus_enat_number [simp]: |
184 |
"(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l |
|
29012 | 185 |
else if l < Int.Pls then number_of k else number_of (k + l))" |
43919 | 186 |
unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] .. |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
187 |
|
27110 | 188 |
lemma iSuc_number [simp]: |
189 |
"iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))" |
|
190 |
unfolding iSuc_number_of |
|
43919 | 191 |
unfolding one_enat_def number_of_enat_def Suc_nat_number_of if_distrib [symmetric] .. |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
192 |
|
27110 | 193 |
lemma iSuc_plus_1: |
194 |
"iSuc n = n + 1" |
|
43919 | 195 |
by (cases n) (simp_all add: iSuc_Fin one_enat_def) |
27110 | 196 |
|
197 |
lemma plus_1_iSuc: |
|
198 |
"1 + q = iSuc q" |
|
199 |
"q + 1 = iSuc q" |
|
41853 | 200 |
by (simp_all add: iSuc_plus_1 add_ac) |
201 |
||
202 |
lemma iadd_Suc: "iSuc m + n = iSuc (m + n)" |
|
203 |
by (simp_all add: iSuc_plus_1 add_ac) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
204 |
|
41853 | 205 |
lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)" |
206 |
by (simp only: add_commute[of m] iadd_Suc) |
|
207 |
||
43919 | 208 |
lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)" |
209 |
by (cases m, cases n, simp_all add: zero_enat_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
210 |
|
29014 | 211 |
subsection {* Multiplication *} |
212 |
||
43919 | 213 |
instantiation enat :: comm_semiring_1 |
29014 | 214 |
begin |
215 |
||
43919 | 216 |
definition times_enat_def [nitpick_simp]: |
29014 | 217 |
"m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow> |
218 |
(case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))" |
|
219 |
||
43919 | 220 |
lemma times_enat_simps [simp, code]: |
29014 | 221 |
"Fin m * Fin n = Fin (m * n)" |
43921 | 222 |
"\<infinity> * \<infinity> = (\<infinity>::enat)" |
29014 | 223 |
"\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)" |
224 |
"Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)" |
|
43919 | 225 |
unfolding times_enat_def zero_enat_def |
226 |
by (simp_all split: enat.split) |
|
29014 | 227 |
|
228 |
instance proof |
|
43919 | 229 |
fix a b c :: enat |
29014 | 230 |
show "(a * b) * c = a * (b * c)" |
43919 | 231 |
unfolding times_enat_def zero_enat_def |
232 |
by (simp split: enat.split) |
|
29014 | 233 |
show "a * b = b * a" |
43919 | 234 |
unfolding times_enat_def zero_enat_def |
235 |
by (simp split: enat.split) |
|
29014 | 236 |
show "1 * a = a" |
43919 | 237 |
unfolding times_enat_def zero_enat_def one_enat_def |
238 |
by (simp split: enat.split) |
|
29014 | 239 |
show "(a + b) * c = a * c + b * c" |
43919 | 240 |
unfolding times_enat_def zero_enat_def |
241 |
by (simp split: enat.split add: left_distrib) |
|
29014 | 242 |
show "0 * a = 0" |
43919 | 243 |
unfolding times_enat_def zero_enat_def |
244 |
by (simp split: enat.split) |
|
29014 | 245 |
show "a * 0 = 0" |
43919 | 246 |
unfolding times_enat_def zero_enat_def |
247 |
by (simp split: enat.split) |
|
248 |
show "(0::enat) \<noteq> 1" |
|
249 |
unfolding zero_enat_def one_enat_def |
|
29014 | 250 |
by simp |
251 |
qed |
|
252 |
||
253 |
end |
|
254 |
||
255 |
lemma mult_iSuc: "iSuc m * n = n + m * n" |
|
29667 | 256 |
unfolding iSuc_plus_1 by (simp add: algebra_simps) |
29014 | 257 |
|
258 |
lemma mult_iSuc_right: "m * iSuc n = m + m * n" |
|
29667 | 259 |
unfolding iSuc_plus_1 by (simp add: algebra_simps) |
29014 | 260 |
|
29023 | 261 |
lemma of_nat_eq_Fin: "of_nat n = Fin n" |
262 |
apply (induct n) |
|
263 |
apply (simp add: Fin_0) |
|
264 |
apply (simp add: plus_1_iSuc iSuc_Fin) |
|
265 |
done |
|
266 |
||
43919 | 267 |
instance enat :: number_semiring |
43532 | 268 |
proof |
43919 | 269 |
fix n show "number_of (int n) = (of_nat n :: enat)" |
270 |
unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_Fin .. |
|
43532 | 271 |
qed |
272 |
||
43919 | 273 |
instance enat :: semiring_char_0 proof |
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
38167
diff
changeset
|
274 |
have "inj Fin" by (rule injI) simp |
43919 | 275 |
then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_Fin) |
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
38167
diff
changeset
|
276 |
qed |
29023 | 277 |
|
43919 | 278 |
lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)" |
279 |
by(auto simp add: times_enat_def zero_enat_def split: enat.split) |
|
41853 | 280 |
|
43919 | 281 |
lemma imult_is_Infty: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)" |
282 |
by(auto simp add: times_enat_def zero_enat_def split: enat.split) |
|
41853 | 283 |
|
284 |
||
285 |
subsection {* Subtraction *} |
|
286 |
||
43919 | 287 |
instantiation enat :: minus |
41853 | 288 |
begin |
289 |
||
43919 | 290 |
definition diff_enat_def: |
41853 | 291 |
"a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0) |
292 |
| \<infinity> \<Rightarrow> \<infinity>)" |
|
293 |
||
294 |
instance .. |
|
295 |
||
296 |
end |
|
297 |
||
298 |
lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)" |
|
43919 | 299 |
by(simp add: diff_enat_def) |
41853 | 300 |
|
43921 | 301 |
lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)" |
43919 | 302 |
by(simp add: diff_enat_def) |
41853 | 303 |
|
304 |
lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0" |
|
43919 | 305 |
by(simp add: diff_enat_def) |
41853 | 306 |
|
43919 | 307 |
lemma idiff_0[simp]: "(0::enat) - n = 0" |
308 |
by (cases n, simp_all add: zero_enat_def) |
|
41853 | 309 |
|
43919 | 310 |
lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_enat_def] |
41853 | 311 |
|
43919 | 312 |
lemma idiff_0_right[simp]: "(n::enat) - 0 = n" |
313 |
by (cases n) (simp_all add: zero_enat_def) |
|
41853 | 314 |
|
43919 | 315 |
lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_enat_def] |
41853 | 316 |
|
43919 | 317 |
lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0" |
318 |
by(auto simp: zero_enat_def) |
|
41853 | 319 |
|
41855 | 320 |
lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m" |
43919 | 321 |
by(simp add: iSuc_def split: enat.split) |
41855 | 322 |
|
323 |
lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n" |
|
43919 | 324 |
by(simp add: one_enat_def iSuc_Fin[symmetric] zero_enat_def[symmetric]) |
41855 | 325 |
|
43919 | 326 |
(*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*) |
41853 | 327 |
|
27110 | 328 |
subsection {* Ordering *} |
329 |
||
43919 | 330 |
instantiation enat :: linordered_ab_semigroup_add |
27110 | 331 |
begin |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
332 |
|
38167 | 333 |
definition [nitpick_simp]: |
37765 | 334 |
"m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False) |
27110 | 335 |
| \<infinity> \<Rightarrow> True)" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
336 |
|
38167 | 337 |
definition [nitpick_simp]: |
37765 | 338 |
"m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True) |
27110 | 339 |
| \<infinity> \<Rightarrow> False)" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
340 |
|
43919 | 341 |
lemma enat_ord_simps [simp]: |
27110 | 342 |
"Fin m \<le> Fin n \<longleftrightarrow> m \<le> n" |
343 |
"Fin m < Fin n \<longleftrightarrow> m < n" |
|
43921 | 344 |
"q \<le> (\<infinity>::enat)" |
345 |
"q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>" |
|
346 |
"(\<infinity>::enat) \<le> q \<longleftrightarrow> q = \<infinity>" |
|
347 |
"(\<infinity>::enat) < q \<longleftrightarrow> False" |
|
43919 | 348 |
by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
349 |
|
43919 | 350 |
lemma enat_ord_code [code]: |
27110 | 351 |
"Fin m \<le> Fin n \<longleftrightarrow> m \<le> n" |
352 |
"Fin m < Fin n \<longleftrightarrow> m < n" |
|
43921 | 353 |
"q \<le> (\<infinity>::enat) \<longleftrightarrow> True" |
27110 | 354 |
"Fin m < \<infinity> \<longleftrightarrow> True" |
355 |
"\<infinity> \<le> Fin n \<longleftrightarrow> False" |
|
43921 | 356 |
"(\<infinity>::enat) < q \<longleftrightarrow> False" |
27110 | 357 |
by simp_all |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
358 |
|
27110 | 359 |
instance by default |
43919 | 360 |
(auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
361 |
|
27110 | 362 |
end |
363 |
||
43919 | 364 |
instance enat :: ordered_comm_semiring |
29014 | 365 |
proof |
43919 | 366 |
fix a b c :: enat |
29014 | 367 |
assume "a \<le> b" and "0 \<le> c" |
368 |
thus "c * a \<le> c * b" |
|
43919 | 369 |
unfolding times_enat_def less_eq_enat_def zero_enat_def |
370 |
by (simp split: enat.splits) |
|
29014 | 371 |
qed |
372 |
||
43919 | 373 |
lemma enat_ord_number [simp]: |
374 |
"(number_of m \<Colon> enat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n" |
|
375 |
"(number_of m \<Colon> enat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n" |
|
376 |
by (simp_all add: number_of_enat_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
377 |
|
43919 | 378 |
lemma i0_lb [simp]: "(0\<Colon>enat) \<le> n" |
379 |
by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
380 |
|
43919 | 381 |
lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0" |
382 |
by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) |
|
27110 | 383 |
|
384 |
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R" |
|
43919 | 385 |
by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
386 |
|
27110 | 387 |
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R" |
388 |
by simp |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
389 |
|
43919 | 390 |
lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)" |
391 |
by (simp add: zero_enat_def less_enat_def split: enat.splits) |
|
27110 | 392 |
|
43919 | 393 |
lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 0" |
394 |
by (simp add: zero_enat_def less_enat_def split: enat.splits) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
395 |
|
27110 | 396 |
lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m" |
43919 | 397 |
by (simp add: iSuc_def less_eq_enat_def split: enat.splits) |
27110 | 398 |
|
399 |
lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m" |
|
43919 | 400 |
by (simp add: iSuc_def less_enat_def split: enat.splits) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
401 |
|
27110 | 402 |
lemma ile_iSuc [simp]: "n \<le> iSuc n" |
43919 | 403 |
by (simp add: iSuc_def less_eq_enat_def split: enat.splits) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
404 |
|
11355 | 405 |
lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0" |
43919 | 406 |
by (simp add: zero_enat_def iSuc_def less_eq_enat_def split: enat.splits) |
27110 | 407 |
|
408 |
lemma i0_iless_iSuc [simp]: "0 < iSuc n" |
|
43919 | 409 |
by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.splits) |
27110 | 410 |
|
41853 | 411 |
lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)" |
43919 | 412 |
by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.split) |
41853 | 413 |
|
27110 | 414 |
lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n" |
43919 | 415 |
by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits) |
27110 | 416 |
|
417 |
lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n" |
|
418 |
by (cases n) auto |
|
419 |
||
420 |
lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n" |
|
43919 | 421 |
by (auto simp add: iSuc_def less_enat_def split: enat.splits) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
422 |
|
43919 | 423 |
lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>" |
424 |
by (simp add: zero_enat_def less_enat_def split: enat.splits) |
|
41853 | 425 |
|
43919 | 426 |
lemma imult_Infty_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>" |
427 |
by (simp add: zero_enat_def less_enat_def split: enat.splits) |
|
41853 | 428 |
|
43919 | 429 |
lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)" |
41853 | 430 |
by (simp only: i0_less imult_is_0, simp) |
431 |
||
432 |
lemma mono_iSuc: "mono iSuc" |
|
433 |
by(simp add: mono_def) |
|
434 |
||
435 |
||
43919 | 436 |
lemma min_enat_simps [simp]: |
27110 | 437 |
"min (Fin m) (Fin n) = Fin (min m n)" |
438 |
"min q 0 = 0" |
|
439 |
"min 0 q = 0" |
|
43921 | 440 |
"min q (\<infinity>::enat) = q" |
441 |
"min (\<infinity>::enat) q = q" |
|
27110 | 442 |
by (auto simp add: min_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
443 |
|
43919 | 444 |
lemma max_enat_simps [simp]: |
27110 | 445 |
"max (Fin m) (Fin n) = Fin (max m n)" |
446 |
"max q 0 = q" |
|
447 |
"max 0 q = q" |
|
43921 | 448 |
"max q \<infinity> = (\<infinity>::enat)" |
449 |
"max \<infinity> q = (\<infinity>::enat)" |
|
27110 | 450 |
by (simp_all add: max_def) |
451 |
||
452 |
lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k" |
|
453 |
by (cases n) simp_all |
|
454 |
||
455 |
lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k" |
|
456 |
by (cases n) simp_all |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
457 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
458 |
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
|
459 |
apply (induct_tac k) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
460 |
apply (simp (no_asm) only: Fin_0) |
27110 | 461 |
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
|
462 |
apply (erule exE) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
463 |
apply (drule spec) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
464 |
apply (erule exE) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
465 |
apply (drule ileI1) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
466 |
apply (rule iSuc_Fin [THEN subst]) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
467 |
apply (rule exI) |
27110 | 468 |
apply (erule (1) le_less_trans) |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
469 |
done |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
470 |
|
43919 | 471 |
instantiation enat :: "{bot, top}" |
29337 | 472 |
begin |
473 |
||
43919 | 474 |
definition bot_enat :: enat where |
475 |
"bot_enat = 0" |
|
29337 | 476 |
|
43919 | 477 |
definition top_enat :: enat where |
478 |
"top_enat = \<infinity>" |
|
29337 | 479 |
|
480 |
instance proof |
|
43919 | 481 |
qed (simp_all add: bot_enat_def top_enat_def) |
29337 | 482 |
|
483 |
end |
|
484 |
||
42993 | 485 |
lemma finite_Fin_bounded: |
486 |
assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> Fin n" |
|
487 |
shows "finite A" |
|
488 |
proof (rule finite_subset) |
|
489 |
show "finite (Fin ` {..n})" by blast |
|
490 |
||
491 |
have "A \<subseteq> {..Fin n}" using le_fin by fastsimp |
|
492 |
also have "\<dots> \<subseteq> Fin ` {..n}" |
|
493 |
by (rule subsetI) (case_tac x, auto) |
|
494 |
finally show "A \<subseteq> Fin ` {..n}" . |
|
495 |
qed |
|
496 |
||
26089 | 497 |
|
27110 | 498 |
subsection {* Well-ordering *} |
26089 | 499 |
|
500 |
lemma less_FinE: |
|
501 |
"[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P" |
|
502 |
by (induct n) auto |
|
503 |
||
504 |
lemma less_InftyE: |
|
43921 | 505 |
"[| n < \<infinity>; !!k. n = Fin k ==> P |] ==> P" |
26089 | 506 |
by (induct n) auto |
507 |
||
43919 | 508 |
lemma enat_less_induct: |
509 |
assumes prem: "!!n. \<forall>m::enat. m < n --> P m ==> P n" shows "P n" |
|
26089 | 510 |
proof - |
511 |
have P_Fin: "!!k. P (Fin k)" |
|
512 |
apply (rule nat_less_induct) |
|
513 |
apply (rule prem, clarify) |
|
514 |
apply (erule less_FinE, simp) |
|
515 |
done |
|
516 |
show ?thesis |
|
517 |
proof (induct n) |
|
518 |
fix nat |
|
519 |
show "P (Fin nat)" by (rule P_Fin) |
|
520 |
next |
|
43921 | 521 |
show "P \<infinity>" |
26089 | 522 |
apply (rule prem, clarify) |
523 |
apply (erule less_InftyE) |
|
524 |
apply (simp add: P_Fin) |
|
525 |
done |
|
526 |
qed |
|
527 |
qed |
|
528 |
||
43919 | 529 |
instance enat :: wellorder |
26089 | 530 |
proof |
27823 | 531 |
fix P and n |
43919 | 532 |
assume hyp: "(\<And>n\<Colon>enat. (\<And>m\<Colon>enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)" |
533 |
show "P n" by (blast intro: enat_less_induct hyp) |
|
26089 | 534 |
qed |
535 |
||
42993 | 536 |
subsection {* Complete Lattice *} |
537 |
||
43919 | 538 |
instantiation enat :: complete_lattice |
42993 | 539 |
begin |
540 |
||
43919 | 541 |
definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where |
542 |
"inf_enat \<equiv> min" |
|
42993 | 543 |
|
43919 | 544 |
definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where |
545 |
"sup_enat \<equiv> max" |
|
42993 | 546 |
|
43919 | 547 |
definition Inf_enat :: "enat set \<Rightarrow> enat" where |
548 |
"Inf_enat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)" |
|
42993 | 549 |
|
43919 | 550 |
definition Sup_enat :: "enat set \<Rightarrow> enat" where |
551 |
"Sup_enat A \<equiv> if A = {} then 0 |
|
42993 | 552 |
else if finite A then Max A |
553 |
else \<infinity>" |
|
554 |
instance proof |
|
43919 | 555 |
fix x :: "enat" and A :: "enat set" |
42993 | 556 |
{ assume "x \<in> A" then show "Inf A \<le> x" |
43919 | 557 |
unfolding Inf_enat_def by (auto intro: Least_le) } |
42993 | 558 |
{ assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A" |
43919 | 559 |
unfolding Inf_enat_def |
42993 | 560 |
by (cases "A = {}") (auto intro: LeastI2_ex) } |
561 |
{ assume "x \<in> A" then show "x \<le> Sup A" |
|
43919 | 562 |
unfolding Sup_enat_def by (cases "finite A") auto } |
42993 | 563 |
{ assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x" |
43919 | 564 |
unfolding Sup_enat_def using finite_Fin_bounded by auto } |
565 |
qed (simp_all add: inf_enat_def sup_enat_def) |
|
42993 | 566 |
end |
567 |
||
27110 | 568 |
|
569 |
subsection {* Traditional theorem names *} |
|
570 |
||
43919 | 571 |
lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def iSuc_def |
572 |
plus_enat_def less_eq_enat_def less_enat_def |
|
27110 | 573 |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
574 |
end |