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