author  huffman 
Tue, 02 Aug 2011 08:28:34 0700  
changeset 44019  ee784502aed5 
parent 43978  da7d04d4023c 
child 44890  22f665a2e91c 
permissions  rwrr 
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 

43924  30 
definition enat :: "nat \<Rightarrow> enat" where 
31 
"enat n = Abs_enat (Some n)" 

43921  32 

33 
instantiation enat :: infinity 

34 
begin 

35 
definition "\<infinity> = Abs_enat None" 

36 
instance proof qed 

37 
end 

38 

43924  39 
rep_datatype enat "\<infinity> :: enat" 
43921  40 
proof  
43924  41 
fix P i assume "\<And>j. P (enat j)" "P \<infinity>" 
43921  42 
then show "P i" 
43 
proof induct 

44 
case (Abs_enat y) then show ?case 

45 
by (cases y rule: option.exhaust) 

43924  46 
(auto simp: enat_def infinity_enat_def) 
43921  47 
qed 
43924  48 
qed (auto simp add: enat_def infinity_enat_def Abs_enat_inject) 
19736  49 

43924  50 
declare [[coercion "enat::nat\<Rightarrow>enat"]] 
19736  51 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

52 
lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

53 
by (cases x) auto 
31084  54 

43924  55 
lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \<infinity>)" 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

56 
by (cases x) auto 
31077  57 

43924  58 
primrec the_enat :: "enat \<Rightarrow> nat" 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

59 
where "the_enat (enat n) = n" 
41855  60 

27110  61 
subsection {* Constructors and numbers *} 
62 

43919  63 
instantiation enat :: "{zero, one, number}" 
25594  64 
begin 
65 

66 
definition 

43924  67 
"0 = enat 0" 
25594  68 

69 
definition 

43924  70 
[code_unfold]: "1 = enat 1" 
25594  71 

72 
definition 

43924  73 
[code_unfold, code del]: "number_of k = enat (number_of k)" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

74 

25594  75 
instance .. 
76 

77 
end 

78 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

79 
definition eSuc :: "enat \<Rightarrow> enat" where 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

80 
"eSuc i = (case i of enat n \<Rightarrow> enat (Suc n)  \<infinity> \<Rightarrow> \<infinity>)" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

81 

43924  82 
lemma enat_0: "enat 0 = 0" 
43919  83 
by (simp add: zero_enat_def) 
27110  84 

43924  85 
lemma enat_1: "enat 1 = 1" 
43919  86 
by (simp add: one_enat_def) 
27110  87 

43924  88 
lemma enat_number: "enat (number_of k) = number_of k" 
43919  89 
by (simp add: number_of_enat_def) 
27110  90 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

91 
lemma one_eSuc: "1 = eSuc 0" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

92 
by (simp add: zero_enat_def one_enat_def eSuc_def) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

93 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

94 
lemma infinity_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0" 
43919  95 
by (simp add: zero_enat_def) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

96 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

97 
lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)" 
43919  98 
by (simp add: zero_enat_def) 
27110  99 

43919  100 
lemma zero_enat_eq [simp]: 
101 
"number_of k = (0\<Colon>enat) \<longleftrightarrow> number_of k = (0\<Colon>nat)" 

102 
"(0\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)" 

103 
unfolding zero_enat_def number_of_enat_def by simp_all 

27110  104 

43919  105 
lemma one_enat_eq [simp]: 
106 
"number_of k = (1\<Colon>enat) \<longleftrightarrow> number_of k = (1\<Colon>nat)" 

107 
"(1\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)" 

108 
unfolding one_enat_def number_of_enat_def by simp_all 

27110  109 

43919  110 
lemma zero_one_enat_neq [simp]: 
111 
"\<not> 0 = (1\<Colon>enat)" 

112 
"\<not> 1 = (0\<Colon>enat)" 

113 
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

114 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

115 
lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1" 
43919  116 
by (simp add: one_enat_def) 
27110  117 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

118 
lemma i1_ne_infinity [simp]: "1 \<noteq> (\<infinity>::enat)" 
43919  119 
by (simp add: one_enat_def) 
27110  120 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

121 
lemma infinity_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k" 
43919  122 
by (simp add: number_of_enat_def) 
27110  123 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

124 
lemma number_ne_infinity [simp]: "number_of k \<noteq> (\<infinity>::enat)" 
43919  125 
by (simp add: number_of_enat_def) 
27110  126 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

127 
lemma eSuc_enat: "eSuc (enat n) = enat (Suc n)" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

128 
by (simp add: eSuc_def) 
27110  129 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

130 
lemma eSuc_number_of: "eSuc (number_of k) = enat (Suc (number_of k))" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

131 
by (simp add: eSuc_enat number_of_enat_def) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

132 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

133 
lemma eSuc_infinity [simp]: "eSuc \<infinity> = \<infinity>" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

134 
by (simp add: eSuc_def) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

135 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

136 
lemma eSuc_ne_0 [simp]: "eSuc n \<noteq> 0" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

137 
by (simp add: eSuc_def zero_enat_def split: enat.splits) 
27110  138 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

139 
lemma zero_ne_eSuc [simp]: "0 \<noteq> eSuc n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

140 
by (rule eSuc_ne_0 [symmetric]) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

141 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

142 
lemma eSuc_inject [simp]: "eSuc m = eSuc n \<longleftrightarrow> m = n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

143 
by (simp add: eSuc_def split: enat.splits) 
27110  144 

43919  145 
lemma number_of_enat_inject [simp]: 
146 
"(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l" 

147 
by (simp add: number_of_enat_def) 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

148 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

149 

27110  150 
subsection {* Addition *} 
151 

43919  152 
instantiation enat :: comm_monoid_add 
27110  153 
begin 
154 

38167  155 
definition [nitpick_simp]: 
43924  156 
"m + n = (case m of \<infinity> \<Rightarrow> \<infinity>  enat m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity>  enat n \<Rightarrow> enat (m + n)))" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

157 

43919  158 
lemma plus_enat_simps [simp, code]: 
43921  159 
fixes q :: enat 
43924  160 
shows "enat m + enat n = enat (m + n)" 
43921  161 
and "\<infinity> + q = \<infinity>" 
162 
and "q + \<infinity> = \<infinity>" 

43919  163 
by (simp_all add: plus_enat_def split: enat.splits) 
27110  164 

165 
instance proof 

43919  166 
fix n m q :: enat 
27110  167 
show "n + m + q = n + (m + q)" 
168 
by (cases n, auto, cases m, auto, cases q, auto) 

169 
show "n + m = m + n" 

170 
by (cases n, auto, cases m, auto) 

171 
show "0 + n = n" 

43919  172 
by (cases n) (simp_all add: zero_enat_def) 
26089  173 
qed 
174 

27110  175 
end 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

176 

43919  177 
lemma plus_enat_0 [simp]: 
178 
"0 + (q\<Colon>enat) = q" 

179 
"(q\<Colon>enat) + 0 = q" 

180 
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

181 

43919  182 
lemma plus_enat_number [simp]: 
183 
"(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l 

29012  184 
else if l < Int.Pls then number_of k else number_of (k + l))" 
43924  185 
unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ enat] .. 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

186 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

187 
lemma eSuc_number [simp]: 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

188 
"eSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

189 
unfolding eSuc_number_of 
43919  190 
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

191 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

192 
lemma eSuc_plus_1: 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

193 
"eSuc n = n + 1" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

194 
by (cases n) (simp_all add: eSuc_enat one_enat_def) 
27110  195 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

196 
lemma plus_1_eSuc: 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

197 
"1 + q = eSuc q" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

198 
"q + 1 = eSuc q" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

199 
by (simp_all add: eSuc_plus_1 add_ac) 
41853  200 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

201 
lemma iadd_Suc: "eSuc m + n = eSuc (m + n)" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

202 
by (simp_all add: eSuc_plus_1 add_ac) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

203 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

204 
lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

205 
by (simp only: add_commute[of m] iadd_Suc) 
41853  206 

43919  207 
lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)" 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

208 
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

209 

29014  210 
subsection {* Multiplication *} 
211 

43919  212 
instantiation enat :: comm_semiring_1 
29014  213 
begin 
214 

43919  215 
definition times_enat_def [nitpick_simp]: 
43924  216 
"m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity>  enat m \<Rightarrow> 
217 
(case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity>  enat n \<Rightarrow> enat (m * n)))" 

29014  218 

43919  219 
lemma times_enat_simps [simp, code]: 
43924  220 
"enat m * enat n = enat (m * n)" 
43921  221 
"\<infinity> * \<infinity> = (\<infinity>::enat)" 
43924  222 
"\<infinity> * enat n = (if n = 0 then 0 else \<infinity>)" 
223 
"enat m * \<infinity> = (if m = 0 then 0 else \<infinity>)" 

43919  224 
unfolding times_enat_def zero_enat_def 
225 
by (simp_all split: enat.split) 

29014  226 

227 
instance proof 

43919  228 
fix a b c :: enat 
29014  229 
show "(a * b) * c = a * (b * c)" 
43919  230 
unfolding times_enat_def zero_enat_def 
231 
by (simp split: enat.split) 

29014  232 
show "a * b = b * a" 
43919  233 
unfolding times_enat_def zero_enat_def 
234 
by (simp split: enat.split) 

29014  235 
show "1 * a = a" 
43919  236 
unfolding times_enat_def zero_enat_def one_enat_def 
237 
by (simp split: enat.split) 

29014  238 
show "(a + b) * c = a * c + b * c" 
43919  239 
unfolding times_enat_def zero_enat_def 
240 
by (simp split: enat.split add: left_distrib) 

29014  241 
show "0 * a = 0" 
43919  242 
unfolding times_enat_def zero_enat_def 
243 
by (simp split: enat.split) 

29014  244 
show "a * 0 = 0" 
43919  245 
unfolding times_enat_def zero_enat_def 
246 
by (simp split: enat.split) 

247 
show "(0::enat) \<noteq> 1" 

248 
unfolding zero_enat_def one_enat_def 

29014  249 
by simp 
250 
qed 

251 

252 
end 

253 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

254 
lemma mult_eSuc: "eSuc m * n = n + m * n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

255 
unfolding eSuc_plus_1 by (simp add: algebra_simps) 
29014  256 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

257 
lemma mult_eSuc_right: "m * eSuc n = m + m * n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

258 
unfolding eSuc_plus_1 by (simp add: algebra_simps) 
29014  259 

43924  260 
lemma of_nat_eq_enat: "of_nat n = enat n" 
29023  261 
apply (induct n) 
43924  262 
apply (simp add: enat_0) 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

263 
apply (simp add: plus_1_eSuc eSuc_enat) 
29023  264 
done 
265 

43919  266 
instance enat :: number_semiring 
43532  267 
proof 
43919  268 
fix n show "number_of (int n) = (of_nat n :: enat)" 
43924  269 
unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_enat .. 
43532  270 
qed 
271 

43919  272 
instance enat :: semiring_char_0 proof 
43924  273 
have "inj enat" by (rule injI) simp 
274 
then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat) 

38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
38167
diff
changeset

275 
qed 
29023  276 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

277 
lemma imult_is_0 [simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

278 
by (auto simp add: times_enat_def zero_enat_def split: enat.split) 
41853  279 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

280 
lemma imult_is_infinity: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

281 
by (auto simp add: times_enat_def zero_enat_def split: enat.split) 
41853  282 

283 

284 
subsection {* Subtraction *} 

285 

43919  286 
instantiation enat :: minus 
41853  287 
begin 
288 

43919  289 
definition diff_enat_def: 
43924  290 
"a  b = (case a of (enat x) \<Rightarrow> (case b of (enat y) \<Rightarrow> enat (x  y)  \<infinity> \<Rightarrow> 0) 
41853  291 
 \<infinity> \<Rightarrow> \<infinity>)" 
292 

293 
instance .. 

294 

295 
end 

296 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

297 
lemma idiff_enat_enat [simp,code]: "enat a  enat b = enat (a  b)" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

298 
by (simp add: diff_enat_def) 
41853  299 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

300 
lemma idiff_infinity [simp,code]: "\<infinity>  n = (\<infinity>::enat)" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

301 
by (simp add: diff_enat_def) 
41853  302 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

303 
lemma idiff_infinity_right [simp,code]: "enat a  \<infinity> = 0" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

304 
by (simp add: diff_enat_def) 
41853  305 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

306 
lemma idiff_0 [simp]: "(0::enat)  n = 0" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

307 
by (cases n, simp_all add: zero_enat_def) 
41853  308 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

309 
lemmas idiff_enat_0 [simp] = idiff_0 [unfolded zero_enat_def] 
41853  310 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

311 
lemma idiff_0_right [simp]: "(n::enat)  0 = n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

312 
by (cases n) (simp_all add: zero_enat_def) 
41853  313 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

314 
lemmas idiff_enat_0_right [simp] = idiff_0_right [unfolded zero_enat_def] 
41853  315 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

316 
lemma idiff_self [simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat)  n = 0" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

317 
by (auto simp: zero_enat_def) 
41853  318 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

319 
lemma eSuc_minus_eSuc [simp]: "eSuc n  eSuc m = n  m" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

320 
by (simp add: eSuc_def split: enat.split) 
41855  321 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

322 
lemma eSuc_minus_1 [simp]: "eSuc n  1 = n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

323 
by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric]) 
41855  324 

43924  325 
(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*) 
41853  326 

27110  327 
subsection {* Ordering *} 
328 

43919  329 
instantiation enat :: linordered_ab_semigroup_add 
27110  330 
begin 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

331 

38167  332 
definition [nitpick_simp]: 
43924  333 
"m \<le> n = (case n of enat n1 \<Rightarrow> (case m of enat m1 \<Rightarrow> m1 \<le> n1  \<infinity> \<Rightarrow> False) 
27110  334 
 \<infinity> \<Rightarrow> True)" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

335 

38167  336 
definition [nitpick_simp]: 
43924  337 
"m < n = (case m of enat m1 \<Rightarrow> (case n of enat n1 \<Rightarrow> m1 < n1  \<infinity> \<Rightarrow> True) 
27110  338 
 \<infinity> \<Rightarrow> False)" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

339 

43919  340 
lemma enat_ord_simps [simp]: 
43924  341 
"enat m \<le> enat n \<longleftrightarrow> m \<le> n" 
342 
"enat m < enat n \<longleftrightarrow> m < n" 

43921  343 
"q \<le> (\<infinity>::enat)" 
344 
"q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>" 

345 
"(\<infinity>::enat) \<le> q \<longleftrightarrow> q = \<infinity>" 

346 
"(\<infinity>::enat) < q \<longleftrightarrow> False" 

43919  347 
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

348 

43919  349 
lemma enat_ord_code [code]: 
43924  350 
"enat m \<le> enat n \<longleftrightarrow> m \<le> n" 
351 
"enat m < enat n \<longleftrightarrow> m < n" 

43921  352 
"q \<le> (\<infinity>::enat) \<longleftrightarrow> True" 
43924  353 
"enat m < \<infinity> \<longleftrightarrow> True" 
354 
"\<infinity> \<le> enat n \<longleftrightarrow> False" 

43921  355 
"(\<infinity>::enat) < q \<longleftrightarrow> False" 
27110  356 
by simp_all 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

357 

27110  358 
instance by default 
43919  359 
(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

360 

27110  361 
end 
362 

43919  363 
instance enat :: ordered_comm_semiring 
29014  364 
proof 
43919  365 
fix a b c :: enat 
29014  366 
assume "a \<le> b" and "0 \<le> c" 
367 
thus "c * a \<le> c * b" 

43919  368 
unfolding times_enat_def less_eq_enat_def zero_enat_def 
369 
by (simp split: enat.splits) 

29014  370 
qed 
371 

43919  372 
lemma enat_ord_number [simp]: 
373 
"(number_of m \<Colon> enat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n" 

374 
"(number_of m \<Colon> enat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n" 

375 
by (simp_all add: number_of_enat_def) 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

376 

43919  377 
lemma i0_lb [simp]: "(0\<Colon>enat) \<le> n" 
378 
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

379 

43919  380 
lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0" 
381 
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

382 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

383 
lemma infinity_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

384 
by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

385 

ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

386 
lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R" 
27110  387 
by simp 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

388 

43919  389 
lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)" 
390 
by (simp add: zero_enat_def less_enat_def split: enat.splits) 

27110  391 

43919  392 
lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 0" 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

393 
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

394 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

395 
lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

396 
by (simp add: eSuc_def less_eq_enat_def split: enat.splits) 
27110  397 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

398 
lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

399 
by (simp add: eSuc_def less_enat_def split: enat.splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

400 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

401 
lemma ile_eSuc [simp]: "n \<le> eSuc n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

402 
by (simp add: eSuc_def less_eq_enat_def split: enat.splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

403 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

404 
lemma not_eSuc_ilei0 [simp]: "\<not> eSuc n \<le> 0" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

405 
by (simp add: zero_enat_def eSuc_def less_eq_enat_def split: enat.splits) 
27110  406 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

407 
lemma i0_iless_eSuc [simp]: "0 < eSuc n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

408 
by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.splits) 
27110  409 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

410 
lemma iless_eSuc0[simp]: "(n < eSuc 0) = (n = 0)" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

411 
by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.split) 
41853  412 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

413 
lemma ileI1: "m < n \<Longrightarrow> eSuc m \<le> n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

414 
by (simp add: eSuc_def less_eq_enat_def less_enat_def split: enat.splits) 
27110  415 

43924  416 
lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n" 
27110  417 
by (cases n) auto 
418 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

419 
lemma iless_Suc_eq [simp]: "enat m < eSuc n \<longleftrightarrow> enat m \<le> n" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

420 
by (auto simp add: eSuc_def less_enat_def split: enat.splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

421 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

422 
lemma imult_infinity: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

423 
by (simp add: zero_enat_def less_enat_def split: enat.splits) 
41853  424 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

425 
lemma imult_infinity_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

426 
by (simp add: zero_enat_def less_enat_def split: enat.splits) 
41853  427 

43919  428 
lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)" 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

429 
by (simp only: i0_less imult_is_0, simp) 
41853  430 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

431 
lemma mono_eSuc: "mono eSuc" 
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

432 
by (simp add: mono_def) 
41853  433 

434 

43919  435 
lemma min_enat_simps [simp]: 
43924  436 
"min (enat m) (enat n) = enat (min m n)" 
27110  437 
"min q 0 = 0" 
438 
"min 0 q = 0" 

43921  439 
"min q (\<infinity>::enat) = q" 
440 
"min (\<infinity>::enat) q = q" 

27110  441 
by (auto simp add: min_def) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

442 

43919  443 
lemma max_enat_simps [simp]: 
43924  444 
"max (enat m) (enat n) = enat (max m n)" 
27110  445 
"max q 0 = q" 
446 
"max 0 q = q" 

43921  447 
"max q \<infinity> = (\<infinity>::enat)" 
448 
"max \<infinity> q = (\<infinity>::enat)" 

27110  449 
by (simp_all add: max_def) 
450 

43924  451 
lemma enat_ile: "n \<le> enat m \<Longrightarrow> \<exists>k. n = enat k" 
27110  452 
by (cases n) simp_all 
453 

43924  454 
lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k" 
27110  455 
by (cases n) simp_all 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

456 

43924  457 
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

458 
apply (induct_tac k) 
43924  459 
apply (simp (no_asm) only: enat_0) 
27110  460 
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

461 
apply (erule exE) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

462 
apply (drule spec) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

463 
apply (erule exE) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

464 
apply (drule ileI1) 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

465 
apply (rule eSuc_enat [THEN subst]) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

466 
apply (rule exI) 
27110  467 
apply (erule (1) le_less_trans) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

468 
done 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

469 

43919  470 
instantiation enat :: "{bot, top}" 
29337  471 
begin 
472 

43919  473 
definition bot_enat :: enat where 
474 
"bot_enat = 0" 

29337  475 

43919  476 
definition top_enat :: enat where 
477 
"top_enat = \<infinity>" 

29337  478 

479 
instance proof 

43919  480 
qed (simp_all add: bot_enat_def top_enat_def) 
29337  481 

482 
end 

483 

43924  484 
lemma finite_enat_bounded: 
485 
assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> enat n" 

42993  486 
shows "finite A" 
487 
proof (rule finite_subset) 

43924  488 
show "finite (enat ` {..n})" by blast 
42993  489 

43924  490 
have "A \<subseteq> {..enat n}" using le_fin by fastsimp 
491 
also have "\<dots> \<subseteq> enat ` {..n}" 

42993  492 
by (rule subsetI) (case_tac x, auto) 
43924  493 
finally show "A \<subseteq> enat ` {..n}" . 
42993  494 
qed 
495 

26089  496 

27110  497 
subsection {* Wellordering *} 
26089  498 

43924  499 
lemma less_enatE: 
500 
"[ n < enat m; !!k. n = enat k ==> k < m ==> P ] ==> P" 

26089  501 
by (induct n) auto 
502 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

503 
lemma less_infinityE: 
43924  504 
"[ n < \<infinity>; !!k. n = enat k ==> P ] ==> P" 
26089  505 
by (induct n) auto 
506 

43919  507 
lemma enat_less_induct: 
508 
assumes prem: "!!n. \<forall>m::enat. m < n > P m ==> P n" shows "P n" 

26089  509 
proof  
43924  510 
have P_enat: "!!k. P (enat k)" 
26089  511 
apply (rule nat_less_induct) 
512 
apply (rule prem, clarify) 

43924  513 
apply (erule less_enatE, simp) 
26089  514 
done 
515 
show ?thesis 

516 
proof (induct n) 

517 
fix nat 

43924  518 
show "P (enat nat)" by (rule P_enat) 
26089  519 
next 
43921  520 
show "P \<infinity>" 
26089  521 
apply (rule prem, clarify) 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

522 
apply (erule less_infinityE) 
43924  523 
apply (simp add: P_enat) 
26089  524 
done 
525 
qed 

526 
qed 

527 

43919  528 
instance enat :: wellorder 
26089  529 
proof 
27823  530 
fix P and n 
43919  531 
assume hyp: "(\<And>n\<Colon>enat. (\<And>m\<Colon>enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)" 
532 
show "P n" by (blast intro: enat_less_induct hyp) 

26089  533 
qed 
534 

42993  535 
subsection {* Complete Lattice *} 
536 

43919  537 
instantiation enat :: complete_lattice 
42993  538 
begin 
539 

43919  540 
definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where 
541 
"inf_enat \<equiv> min" 

42993  542 

43919  543 
definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where 
544 
"sup_enat \<equiv> max" 

42993  545 

43919  546 
definition Inf_enat :: "enat set \<Rightarrow> enat" where 
547 
"Inf_enat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)" 

42993  548 

43919  549 
definition Sup_enat :: "enat set \<Rightarrow> enat" where 
550 
"Sup_enat A \<equiv> if A = {} then 0 

42993  551 
else if finite A then Max A 
552 
else \<infinity>" 

553 
instance proof 

43919  554 
fix x :: "enat" and A :: "enat set" 
42993  555 
{ assume "x \<in> A" then show "Inf A \<le> x" 
43919  556 
unfolding Inf_enat_def by (auto intro: Least_le) } 
42993  557 
{ assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A" 
43919  558 
unfolding Inf_enat_def 
42993  559 
by (cases "A = {}") (auto intro: LeastI2_ex) } 
560 
{ assume "x \<in> A" then show "x \<le> Sup A" 

43919  561 
unfolding Sup_enat_def by (cases "finite A") auto } 
42993  562 
{ assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x" 
43924  563 
unfolding Sup_enat_def using finite_enat_bounded by auto } 
43919  564 
qed (simp_all add: inf_enat_def sup_enat_def) 
42993  565 
end 
566 

43978  567 
instance enat :: complete_linorder .. 
27110  568 

569 
subsection {* Traditional theorem names *} 

570 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

571 
lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def eSuc_def 
43919  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 