author  hoelzl 
Tue, 12 Nov 2013 20:08:29 +0100  
changeset 54419  0c50894fc0d9 
parent 54416  7fb88ed6ff3c 
child 56777  9c3f0ae99532 
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 
54415  9 
imports Main Countable 
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 

49834  28 
typedef enat = "UNIV :: nat option set" .. 
54415  29 

54419  30 
text {* TODO: introduce enat as coinductive datatype, enat is just @{const of_nat} *} 
54415  31 

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

43921  34 

35 
instantiation enat :: infinity 

36 
begin 

37 
definition "\<infinity> = Abs_enat None" 

38 
instance proof qed 

39 
end 

54415  40 

41 
instance enat :: countable 

42 
proof 

43 
show "\<exists>to_nat::enat \<Rightarrow> nat. inj to_nat" 

44 
by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject) 

45 
qed 

43921  46 

43924  47 
rep_datatype enat "\<infinity> :: enat" 
43921  48 
proof  
43924  49 
fix P i assume "\<And>j. P (enat j)" "P \<infinity>" 
43921  50 
then show "P i" 
51 
proof induct 

52 
case (Abs_enat y) then show ?case 

53 
by (cases y rule: option.exhaust) 

43924  54 
(auto simp: enat_def infinity_enat_def) 
43921  55 
qed 
43924  56 
qed (auto simp add: enat_def infinity_enat_def Abs_enat_inject) 
19736  57 

43924  58 
declare [[coercion "enat::nat\<Rightarrow>enat"]] 
19736  59 

45934  60 
lemmas enat2_cases = enat.exhaust[case_product enat.exhaust] 
61 
lemmas enat3_cases = enat.exhaust[case_product enat.exhaust enat.exhaust] 

62 

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

64 
by (cases x) auto 
31084  65 

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

67 
by (cases x) auto 
31077  68 

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

70 
where "the_enat (enat n) = n" 
41855  71 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

72 

27110  73 
subsection {* Constructors and numbers *} 
74 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

75 
instantiation enat :: "{zero, one}" 
25594  76 
begin 
77 

78 
definition 

43924  79 
"0 = enat 0" 
25594  80 

81 
definition 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

82 
"1 = enat 1" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

83 

25594  84 
instance .. 
85 

86 
end 

87 

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

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

89 
"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

90 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

91 
lemma enat_0 [code_post]: "enat 0 = 0" 
43919  92 
by (simp add: zero_enat_def) 
27110  93 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

94 
lemma enat_1 [code_post]: "enat 1 = 1" 
43919  95 
by (simp add: one_enat_def) 
27110  96 

54416  97 
lemma enat_0_iff: "enat x = 0 \<longleftrightarrow> x = 0" "0 = enat x \<longleftrightarrow> x = 0" 
98 
by (auto simp add: zero_enat_def) 

99 

100 
lemma enat_1_iff: "enat x = 1 \<longleftrightarrow> x = 1" "1 = enat x \<longleftrightarrow> x = 1" 

101 
by (auto simp add: one_enat_def) 

102 

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

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

104 
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

105 

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

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

108 

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

109 
lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)" 
43919  110 
by (simp add: zero_enat_def) 
27110  111 

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

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

115 
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

116 

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

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

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

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

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

123 
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

124 
by (simp add: eSuc_def) 
27110  125 

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

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

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

128 

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

129 
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

130 
by (simp add: eSuc_def zero_enat_def split: enat.splits) 
27110  131 

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

132 
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

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

134 

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

135 
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

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

138 
subsection {* Addition *} 

139 

43919  140 
instantiation enat :: comm_monoid_add 
27110  141 
begin 
142 

38167  143 
definition [nitpick_simp]: 
43924  144 
"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

145 

43919  146 
lemma plus_enat_simps [simp, code]: 
43921  147 
fixes q :: enat 
43924  148 
shows "enat m + enat n = enat (m + n)" 
43921  149 
and "\<infinity> + q = \<infinity>" 
150 
and "q + \<infinity> = \<infinity>" 

43919  151 
by (simp_all add: plus_enat_def split: enat.splits) 
27110  152 

153 
instance proof 

43919  154 
fix n m q :: enat 
27110  155 
show "n + m + q = n + (m + q)" 
45934  156 
by (cases n m q rule: enat3_cases) auto 
27110  157 
show "n + m = m + n" 
45934  158 
by (cases n m rule: enat2_cases) auto 
27110  159 
show "0 + n = n" 
43919  160 
by (cases n) (simp_all add: zero_enat_def) 
26089  161 
qed 
162 

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

164 

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

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

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

167 
by (cases n) (simp_all add: eSuc_enat one_enat_def) 
27110  168 

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

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

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

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

172 
by (simp_all add: eSuc_plus_1 add_ac) 
41853  173 

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

174 
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

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

176 

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

177 
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

178 
by (simp only: add_commute[of m] iadd_Suc) 
41853  179 

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

181 
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

182 

29014  183 
subsection {* Multiplication *} 
184 

43919  185 
instantiation enat :: comm_semiring_1 
29014  186 
begin 
187 

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

29014  191 

43919  192 
lemma times_enat_simps [simp, code]: 
43924  193 
"enat m * enat n = enat (m * n)" 
43921  194 
"\<infinity> * \<infinity> = (\<infinity>::enat)" 
43924  195 
"\<infinity> * enat n = (if n = 0 then 0 else \<infinity>)" 
196 
"enat m * \<infinity> = (if m = 0 then 0 else \<infinity>)" 

43919  197 
unfolding times_enat_def zero_enat_def 
198 
by (simp_all split: enat.split) 

29014  199 

200 
instance proof 

43919  201 
fix a b c :: enat 
29014  202 
show "(a * b) * c = a * (b * c)" 
43919  203 
unfolding times_enat_def zero_enat_def 
204 
by (simp split: enat.split) 

29014  205 
show "a * b = b * a" 
43919  206 
unfolding times_enat_def zero_enat_def 
207 
by (simp split: enat.split) 

29014  208 
show "1 * a = a" 
43919  209 
unfolding times_enat_def zero_enat_def one_enat_def 
210 
by (simp split: enat.split) 

29014  211 
show "(a + b) * c = a * c + b * c" 
43919  212 
unfolding times_enat_def zero_enat_def 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49834
diff
changeset

213 
by (simp split: enat.split add: distrib_right) 
29014  214 
show "0 * a = 0" 
43919  215 
unfolding times_enat_def zero_enat_def 
216 
by (simp split: enat.split) 

29014  217 
show "a * 0 = 0" 
43919  218 
unfolding times_enat_def zero_enat_def 
219 
by (simp split: enat.split) 

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

221 
unfolding zero_enat_def one_enat_def 

29014  222 
by simp 
223 
qed 

224 

225 
end 

226 

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

227 
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

228 
unfolding eSuc_plus_1 by (simp add: algebra_simps) 
29014  229 

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

230 
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

231 
unfolding eSuc_plus_1 by (simp add: algebra_simps) 
29014  232 

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

236 
apply (simp add: plus_1_eSuc eSuc_enat) 
29023  237 
done 
238 

43919  239 
instance enat :: semiring_char_0 proof 
43924  240 
have "inj enat" by (rule injI) simp 
241 
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

242 
qed 
29023  243 

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

244 
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

245 
by (auto simp add: times_enat_def zero_enat_def split: enat.split) 
41853  246 

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

247 
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

248 
by (auto simp add: times_enat_def zero_enat_def split: enat.split) 
41853  249 

250 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

251 
subsection {* Numerals *} 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

252 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

253 
lemma numeral_eq_enat: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

254 
"numeral k = enat (numeral k)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

255 
using of_nat_eq_enat [of "numeral k"] by simp 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

256 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

257 
lemma enat_numeral [code_abbrev]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

258 
"enat (numeral k) = numeral k" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

259 
using numeral_eq_enat .. 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

260 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

261 
lemma infinity_ne_numeral [simp]: "(\<infinity>::enat) \<noteq> numeral k" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

262 
by (simp add: numeral_eq_enat) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

263 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

264 
lemma numeral_ne_infinity [simp]: "numeral k \<noteq> (\<infinity>::enat)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

265 
by (simp add: numeral_eq_enat) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

266 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

267 
lemma eSuc_numeral [simp]: "eSuc (numeral k) = numeral (k + Num.One)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

268 
by (simp only: eSuc_plus_1 numeral_plus_one) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

269 

41853  270 
subsection {* Subtraction *} 
271 

43919  272 
instantiation enat :: minus 
41853  273 
begin 
274 

43919  275 
definition diff_enat_def: 
43924  276 
"a  b = (case a of (enat x) \<Rightarrow> (case b of (enat y) \<Rightarrow> enat (x  y)  \<infinity> \<Rightarrow> 0) 
41853  277 
 \<infinity> \<Rightarrow> \<infinity>)" 
278 

279 
instance .. 

280 

281 
end 

282 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

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

284 
by (simp add: diff_enat_def) 
41853  285 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

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

287 
by (simp add: diff_enat_def) 
41853  288 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

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

290 
by (simp add: diff_enat_def) 
41853  291 

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

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

293 
by (cases n, simp_all add: zero_enat_def) 
41853  294 

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

295 
lemmas idiff_enat_0 [simp] = idiff_0 [unfolded zero_enat_def] 
41853  296 

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

297 
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

298 
by (cases n) (simp_all add: zero_enat_def) 
41853  299 

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

300 
lemmas idiff_enat_0_right [simp] = idiff_0_right [unfolded zero_enat_def] 
41853  301 

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

302 
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

303 
by (auto simp: zero_enat_def) 
41853  304 

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

305 
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

306 
by (simp add: eSuc_def split: enat.split) 
41855  307 

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

308 
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

309 
by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric]) 
41855  310 

43924  311 
(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*) 
41853  312 

27110  313 
subsection {* Ordering *} 
314 

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

317 

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

321 

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

325 

43919  326 
lemma enat_ord_simps [simp]: 
43924  327 
"enat m \<le> enat n \<longleftrightarrow> m \<le> n" 
328 
"enat m < enat n \<longleftrightarrow> m < n" 

43921  329 
"q \<le> (\<infinity>::enat)" 
330 
"q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>" 

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

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

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

334 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

335 
lemma numeral_le_enat_iff[simp]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

336 
shows "numeral m \<le> enat n \<longleftrightarrow> numeral m \<le> n" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

337 
by (auto simp: numeral_eq_enat) 
45934  338 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

339 
lemma numeral_less_enat_iff[simp]: 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

340 
shows "numeral m < enat n \<longleftrightarrow> numeral m < n" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

341 
by (auto simp: numeral_eq_enat) 
45934  342 

43919  343 
lemma enat_ord_code [code]: 
43924  344 
"enat m \<le> enat n \<longleftrightarrow> m \<le> n" 
345 
"enat m < enat n \<longleftrightarrow> m < n" 

43921  346 
"q \<le> (\<infinity>::enat) \<longleftrightarrow> True" 
43924  347 
"enat m < \<infinity> \<longleftrightarrow> True" 
348 
"\<infinity> \<le> enat n \<longleftrightarrow> False" 

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

351 

27110  352 
instance by default 
43919  353 
(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

354 

27110  355 
end 
356 

43919  357 
instance enat :: ordered_comm_semiring 
29014  358 
proof 
43919  359 
fix a b c :: enat 
29014  360 
assume "a \<le> b" and "0 \<le> c" 
361 
thus "c * a \<le> c * b" 

43919  362 
unfolding times_enat_def less_eq_enat_def zero_enat_def 
363 
by (simp split: enat.splits) 

29014  364 
qed 
365 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

366 
(* BH: These equations are already proven generally for any type in 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

367 
class linordered_semidom. However, enat is not in that class because 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

368 
it does not have the cancellation property. Would it be worthwhile to 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

369 
a generalize linordered_semidom to a new class that includes enat? *) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

370 

43919  371 
lemma enat_ord_number [simp]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

372 
"(numeral m \<Colon> enat) \<le> numeral n \<longleftrightarrow> (numeral m \<Colon> nat) \<le> numeral n" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

373 
"(numeral m \<Colon> enat) < numeral n \<longleftrightarrow> (numeral m \<Colon> nat) < numeral n" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

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

375 

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

378 

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

381 

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

382 
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

383 
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

384 

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

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

387 

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

27110  390 

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

392 
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

393 

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

394 
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

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

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

397 
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

398 
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

399 

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

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

401 
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

402 

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

403 
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

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

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

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

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

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

409 
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

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

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

412 
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

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

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

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

418 
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

419 
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

420 

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

421 
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

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

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

424 
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

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

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

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

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

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

431 
by (simp add: mono_def) 
41853  432 

433 

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

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

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

441 

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

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

27110  448 
by (simp_all add: max_def) 
449 

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

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

455 

43924  456 
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

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

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

461 
apply (drule spec) 
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 ileI1) 
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset

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

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

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

468 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51717
diff
changeset

469 
instantiation enat :: "{order_bot, order_top}" 
29337  470 
begin 
471 

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

29337  474 

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

29337  477 

478 
instance proof 

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

481 
end 

482 

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

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

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

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44019
diff
changeset

489 
have "A \<subseteq> {..enat n}" using le_fin by fastforce 
43924  490 
also have "\<dots> \<subseteq> enat ` {..n}" 
42993  491 
by (rule subsetI) (case_tac x, auto) 
43924  492 
finally show "A \<subseteq> enat ` {..n}" . 
42993  493 
qed 
494 

26089  495 

45775  496 
subsection {* Cancellation simprocs *} 
497 

498 
lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c" 

499 
unfolding plus_enat_def by (simp split: enat.split) 

500 

501 
lemma enat_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b \<le> c" 

502 
unfolding plus_enat_def by (simp split: enat.split) 

503 

504 
lemma enat_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::enat) \<and> b < c" 

505 
unfolding plus_enat_def by (simp split: enat.split) 

506 

507 
ML {* 

508 
structure Cancel_Enat_Common = 

509 
struct 

510 
(* copied from src/HOL/Tools/nat_numeral_simprocs.ML *) 

511 
fun find_first_t _ _ [] = raise TERM("find_first_t", []) 

512 
 find_first_t past u (t::terms) = 

513 
if u aconv t then (rev past @ terms) 

514 
else find_first_t (t::past) u terms 

515 

51366
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extendednat simprocs (it treats 'x  y' as 'x +  y', which is not valid for enat)
huffman
parents:
51301
diff
changeset

516 
fun dest_summing (Const (@{const_name Groups.plus}, _) $ t $ u, ts) = 
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extendednat simprocs (it treats 'x  y' as 'x +  y', which is not valid for enat)
huffman
parents:
51301
diff
changeset

517 
dest_summing (t, dest_summing (u, ts)) 
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extendednat simprocs (it treats 'x  y' as 'x +  y', which is not valid for enat)
huffman
parents:
51301
diff
changeset

518 
 dest_summing (t, ts) = t :: ts 
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extendednat simprocs (it treats 'x  y' as 'x +  y', which is not valid for enat)
huffman
parents:
51301
diff
changeset

519 

45775  520 
val mk_sum = Arith_Data.long_mk_sum 
51366
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extendednat simprocs (it treats 'x  y' as 'x +  y', which is not valid for enat)
huffman
parents:
51301
diff
changeset

521 
fun dest_sum t = dest_summing (t, []) 
45775  522 
val find_first = find_first_t [] 
523 
val trans_tac = Numeral_Simprocs.trans_tac 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset

524 
val norm_ss = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset

525 
simpset_of (put_simpset HOL_basic_ss @{context} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset

526 
addsimps @{thms add_ac add_0_left add_0_right}) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset

527 
fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt)) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset

528 
fun simplify_meta_eq ctxt cancel_th th = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset

529 
Arith_Data.simplify_meta_eq [] ctxt 
45775  530 
([th, cancel_th] MRS trans) 
531 
fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) 

532 
end 

533 

534 
structure Eq_Enat_Cancel = ExtractCommonTermFun 

535 
(open Cancel_Enat_Common 

536 
val mk_bal = HOLogic.mk_eq 

537 
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} @{typ enat} 

538 
fun simp_conv _ _ = SOME @{thm enat_add_left_cancel} 

539 
) 

540 

541 
structure Le_Enat_Cancel = ExtractCommonTermFun 

542 
(open Cancel_Enat_Common 

543 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} 

544 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} @{typ enat} 

545 
fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_le} 

546 
) 

547 

548 
structure Less_Enat_Cancel = ExtractCommonTermFun 

549 
(open Cancel_Enat_Common 

550 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} 

551 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} @{typ enat} 

552 
fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_less} 

553 
) 

554 
*} 

555 

556 
simproc_setup enat_eq_cancel 

557 
("(l::enat) + m = n"  "(l::enat) = m + n") = 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset

558 
{* fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (term_of ct) *} 
45775  559 

560 
simproc_setup enat_le_cancel 

561 
("(l::enat) + m \<le> n"  "(l::enat) \<le> m + n") = 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset

562 
{* fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (term_of ct) *} 
45775  563 

564 
simproc_setup enat_less_cancel 

565 
("(l::enat) + m < n"  "(l::enat) < m + n") = 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset

566 
{* fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (term_of ct) *} 
45775  567 

568 
text {* TODO: add regression tests for these simprocs *} 

569 

570 
text {* TODO: add simprocs for combining and cancelling numerals *} 

571 

27110  572 
subsection {* Wellordering *} 
26089  573 

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

26089  576 
by (induct n) auto 
577 

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

578 
lemma less_infinityE: 
43924  579 
"[ n < \<infinity>; !!k. n = enat k ==> P ] ==> P" 
26089  580 
by (induct n) auto 
581 

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

26089  584 
proof  
43924  585 
have P_enat: "!!k. P (enat k)" 
26089  586 
apply (rule nat_less_induct) 
587 
apply (rule prem, clarify) 

43924  588 
apply (erule less_enatE, simp) 
26089  589 
done 
590 
show ?thesis 

591 
proof (induct n) 

592 
fix nat 

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

597 
apply (erule less_infinityE) 
43924  598 
apply (simp add: P_enat) 
26089  599 
done 
600 
qed 

601 
qed 

602 

43919  603 
instance enat :: wellorder 
26089  604 
proof 
27823  605 
fix P and n 
43919  606 
assume hyp: "(\<And>n\<Colon>enat. (\<And>m\<Colon>enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)" 
607 
show "P n" by (blast intro: enat_less_induct hyp) 

26089  608 
qed 
609 

42993  610 
subsection {* Complete Lattice *} 
611 

54415  612 
text {* TODO: enat as order topology? *} 
613 

43919  614 
instantiation enat :: complete_lattice 
42993  615 
begin 
616 

43919  617 
definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where 
618 
"inf_enat \<equiv> min" 

42993  619 

43919  620 
definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where 
621 
"sup_enat \<equiv> max" 

42993  622 

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

42993  625 

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

42993  628 
else if finite A then Max A 
629 
else \<infinity>" 

630 
instance proof 

43919  631 
fix x :: "enat" and A :: "enat set" 
42993  632 
{ assume "x \<in> A" then show "Inf A \<le> x" 
43919  633 
unfolding Inf_enat_def by (auto intro: Least_le) } 
42993  634 
{ assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A" 
43919  635 
unfolding Inf_enat_def 
42993  636 
by (cases "A = {}") (auto intro: LeastI2_ex) } 
637 
{ assume "x \<in> A" then show "x \<le> Sup A" 

43919  638 
unfolding Sup_enat_def by (cases "finite A") auto } 
42993  639 
{ assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x" 
43924  640 
unfolding Sup_enat_def using finite_enat_bounded by auto } 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51717
diff
changeset

641 
qed (simp_all add: 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51717
diff
changeset

642 
inf_enat_def sup_enat_def bot_enat_def top_enat_def Inf_enat_def Sup_enat_def) 
42993  643 
end 
644 

43978  645 
instance enat :: complete_linorder .. 
27110  646 

647 
subsection {* Traditional theorem names *} 

648 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

649 
lemmas enat_defs = zero_enat_def one_enat_def eSuc_def 
43919  650 
plus_enat_def less_eq_enat_def less_enat_def 
27110  651 

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

652 
end 