author  hoelzl 
Tue, 12 Nov 2013 19:28:55 +0100  
changeset 54415  eaf25431d4c4 
parent 52729  412c9e0381a1 
child 54416  7fb88ed6ff3c 
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 

30 
text {* TODO: introduce enat as coinductive datatype, enat is just of_nat *} 

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 

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

63 
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

64 
by (cases x) auto 
31084  65 

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

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 

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

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

98 
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

99 

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

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

102 

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

103 
lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)" 
43919  104 
by (simp add: zero_enat_def) 
27110  105 

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

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

109 
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

110 

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

111 
lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1" 
43919  112 
by (simp add: one_enat_def) 
27110  113 

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

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

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

117 
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

118 
by (simp add: eSuc_def) 
27110  119 

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

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

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

122 

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

123 
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

124 
by (simp add: eSuc_def zero_enat_def split: enat.splits) 
27110  125 

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

126 
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

127 
by (rule eSuc_ne_0 [symmetric]) 
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_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

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

132 
subsection {* Addition *} 

133 

43919  134 
instantiation enat :: comm_monoid_add 
27110  135 
begin 
136 

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

139 

43919  140 
lemma plus_enat_simps [simp, code]: 
43921  141 
fixes q :: enat 
43924  142 
shows "enat m + enat n = enat (m + n)" 
43921  143 
and "\<infinity> + q = \<infinity>" 
144 
and "q + \<infinity> = \<infinity>" 

43919  145 
by (simp_all add: plus_enat_def split: enat.splits) 
27110  146 

147 
instance proof 

43919  148 
fix n m q :: enat 
27110  149 
show "n + m + q = n + (m + q)" 
45934  150 
by (cases n m q rule: enat3_cases) auto 
27110  151 
show "n + m = m + n" 
45934  152 
by (cases n m rule: enat2_cases) auto 
27110  153 
show "0 + n = n" 
43919  154 
by (cases n) (simp_all add: zero_enat_def) 
26089  155 
qed 
156 

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

158 

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

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

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

161 
by (cases n) (simp_all add: eSuc_enat one_enat_def) 
27110  162 

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

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

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

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

166 
by (simp_all add: eSuc_plus_1 add_ac) 
41853  167 

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

168 
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

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

170 

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

171 
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

172 
by (simp only: add_commute[of m] iadd_Suc) 
41853  173 

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

175 
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

176 

29014  177 
subsection {* Multiplication *} 
178 

43919  179 
instantiation enat :: comm_semiring_1 
29014  180 
begin 
181 

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

29014  185 

43919  186 
lemma times_enat_simps [simp, code]: 
43924  187 
"enat m * enat n = enat (m * n)" 
43921  188 
"\<infinity> * \<infinity> = (\<infinity>::enat)" 
43924  189 
"\<infinity> * enat n = (if n = 0 then 0 else \<infinity>)" 
190 
"enat m * \<infinity> = (if m = 0 then 0 else \<infinity>)" 

43919  191 
unfolding times_enat_def zero_enat_def 
192 
by (simp_all split: enat.split) 

29014  193 

194 
instance proof 

43919  195 
fix a b c :: enat 
29014  196 
show "(a * b) * c = a * (b * c)" 
43919  197 
unfolding times_enat_def zero_enat_def 
198 
by (simp split: enat.split) 

29014  199 
show "a * b = b * a" 
43919  200 
unfolding times_enat_def zero_enat_def 
201 
by (simp split: enat.split) 

29014  202 
show "1 * a = a" 
43919  203 
unfolding times_enat_def zero_enat_def one_enat_def 
204 
by (simp split: enat.split) 

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

207 
by (simp split: enat.split add: distrib_right) 
29014  208 
show "0 * a = 0" 
43919  209 
unfolding times_enat_def zero_enat_def 
210 
by (simp split: enat.split) 

29014  211 
show "a * 0 = 0" 
43919  212 
unfolding times_enat_def zero_enat_def 
213 
by (simp split: enat.split) 

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

215 
unfolding zero_enat_def one_enat_def 

29014  216 
by simp 
217 
qed 

218 

219 
end 

220 

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

221 
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

222 
unfolding eSuc_plus_1 by (simp add: algebra_simps) 
29014  223 

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

224 
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

225 
unfolding eSuc_plus_1 by (simp add: algebra_simps) 
29014  226 

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

230 
apply (simp add: plus_1_eSuc eSuc_enat) 
29023  231 
done 
232 

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

236 
qed 
29023  237 

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

238 
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

239 
by (auto simp add: times_enat_def zero_enat_def split: enat.split) 
41853  240 

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

241 
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

242 
by (auto simp add: times_enat_def zero_enat_def split: enat.split) 
41853  243 

244 

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

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

246 

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

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

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

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

250 

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

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

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

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

254 

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

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

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

257 

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

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

259 
by (simp add: 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 eSuc_numeral [simp]: "eSuc (numeral k) = numeral (k + Num.One)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

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

263 

41853  264 
subsection {* Subtraction *} 
265 

43919  266 
instantiation enat :: minus 
41853  267 
begin 
268 

43919  269 
definition diff_enat_def: 
43924  270 
"a  b = (case a of (enat x) \<Rightarrow> (case b of (enat y) \<Rightarrow> enat (x  y)  \<infinity> \<Rightarrow> 0) 
41853  271 
 \<infinity> \<Rightarrow> \<infinity>)" 
272 

273 
instance .. 

274 

275 
end 

276 

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

277 
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

278 
by (simp add: diff_enat_def) 
41853  279 

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

280 
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

281 
by (simp add: diff_enat_def) 
41853  282 

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

283 
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

284 
by (simp add: diff_enat_def) 
41853  285 

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

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

287 
by (cases n, simp_all add: zero_enat_def) 
41853  288 

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

289 
lemmas idiff_enat_0 [simp] = idiff_0 [unfolded zero_enat_def] 
41853  290 

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

291 
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

292 
by (cases n) (simp_all add: zero_enat_def) 
41853  293 

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

294 
lemmas idiff_enat_0_right [simp] = idiff_0_right [unfolded zero_enat_def] 
41853  295 

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

296 
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

297 
by (auto simp: zero_enat_def) 
41853  298 

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

299 
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

300 
by (simp add: eSuc_def split: enat.split) 
41855  301 

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

302 
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

303 
by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric]) 
41855  304 

43924  305 
(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*) 
41853  306 

27110  307 
subsection {* Ordering *} 
308 

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

311 

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

315 

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

319 

43919  320 
lemma enat_ord_simps [simp]: 
43924  321 
"enat m \<le> enat n \<longleftrightarrow> m \<le> n" 
322 
"enat m < enat n \<longleftrightarrow> m < n" 

43921  323 
"q \<le> (\<infinity>::enat)" 
324 
"q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>" 

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

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

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

328 

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

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

330 
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

331 
by (auto simp: numeral_eq_enat) 
45934  332 

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

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

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

335 
by (auto simp: numeral_eq_enat) 
45934  336 

43919  337 
lemma enat_ord_code [code]: 
43924  338 
"enat m \<le> enat n \<longleftrightarrow> m \<le> n" 
339 
"enat m < enat n \<longleftrightarrow> m < n" 

43921  340 
"q \<le> (\<infinity>::enat) \<longleftrightarrow> True" 
43924  341 
"enat m < \<infinity> \<longleftrightarrow> True" 
342 
"\<infinity> \<le> enat n \<longleftrightarrow> False" 

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

345 

27110  346 
instance by default 
43919  347 
(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

348 

27110  349 
end 
350 

43919  351 
instance enat :: ordered_comm_semiring 
29014  352 
proof 
43919  353 
fix a b c :: enat 
29014  354 
assume "a \<le> b" and "0 \<le> c" 
355 
thus "c * a \<le> c * b" 

43919  356 
unfolding times_enat_def less_eq_enat_def zero_enat_def 
357 
by (simp split: enat.splits) 

29014  358 
qed 
359 

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

360 
(* 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

361 
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

362 
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

363 
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

364 

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

366 
"(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

367 
"(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

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

369 

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

372 

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

375 

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

376 
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

377 
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

378 

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

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

381 

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

27110  384 

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

386 
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

387 

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

388 
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

389 
by (simp add: eSuc_def less_eq_enat_def split: enat.splits) 
27110  390 

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

391 
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

392 
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

393 

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

394 
lemma ile_eSuc [simp]: "n \<le> eSuc n" 
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) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

396 

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

397 
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

398 
by (simp add: zero_enat_def eSuc_def less_eq_enat_def split: enat.splits) 
27110  399 

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

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

401 
by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.splits) 
27110  402 

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

403 
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

404 
by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.split) 
41853  405 

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

406 
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

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

43924  409 
lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n" 
27110  410 
by (cases n) auto 
411 

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

412 
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

413 
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

414 

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

415 
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

416 
by (simp add: zero_enat_def less_enat_def split: enat.splits) 
41853  417 

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

418 
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

419 
by (simp add: zero_enat_def less_enat_def split: enat.splits) 
41853  420 

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

422 
by (simp only: i0_less imult_is_0, simp) 
41853  423 

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

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

425 
by (simp add: mono_def) 
41853  426 

427 

43919  428 
lemma min_enat_simps [simp]: 
43924  429 
"min (enat m) (enat n) = enat (min m n)" 
27110  430 
"min q 0 = 0" 
431 
"min 0 q = 0" 

43921  432 
"min q (\<infinity>::enat) = q" 
433 
"min (\<infinity>::enat) q = q" 

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

435 

43919  436 
lemma max_enat_simps [simp]: 
43924  437 
"max (enat m) (enat n) = enat (max m n)" 
27110  438 
"max q 0 = q" 
439 
"max 0 q = q" 

43921  440 
"max q \<infinity> = (\<infinity>::enat)" 
441 
"max \<infinity> q = (\<infinity>::enat)" 

27110  442 
by (simp_all add: max_def) 
443 

43924  444 
lemma enat_ile: "n \<le> enat m \<Longrightarrow> \<exists>k. n = enat k" 
27110  445 
by (cases n) simp_all 
446 

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

449 

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

451 
apply (induct_tac k) 
43924  452 
apply (simp (no_asm) only: enat_0) 
27110  453 
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

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

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

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

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

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

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

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

462 

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

463 
instantiation enat :: "{order_bot, order_top}" 
29337  464 
begin 
465 

43919  466 
definition bot_enat :: enat where 
467 
"bot_enat = 0" 

29337  468 

43919  469 
definition top_enat :: enat where 
470 
"top_enat = \<infinity>" 

29337  471 

472 
instance proof 

43919  473 
qed (simp_all add: bot_enat_def top_enat_def) 
29337  474 

475 
end 

476 

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

42993  479 
shows "finite A" 
480 
proof (rule finite_subset) 

43924  481 
show "finite (enat ` {..n})" by blast 
42993  482 

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

483 
have "A \<subseteq> {..enat n}" using le_fin by fastforce 
43924  484 
also have "\<dots> \<subseteq> enat ` {..n}" 
42993  485 
by (rule subsetI) (case_tac x, auto) 
43924  486 
finally show "A \<subseteq> enat ` {..n}" . 
42993  487 
qed 
488 

26089  489 

45775  490 
subsection {* Cancellation simprocs *} 
491 

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

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

494 

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

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

497 

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

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

500 

501 
ML {* 

502 
structure Cancel_Enat_Common = 

503 
struct 

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

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

506 
 find_first_t past u (t::terms) = 

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

508 
else find_first_t (t::past) u terms 

509 

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

510 
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

511 
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

512 
 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

513 

45775  514 
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

515 
fun dest_sum t = dest_summing (t, []) 
45775  516 
val find_first = find_first_t [] 
517 
val trans_tac = Numeral_Simprocs.trans_tac 

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

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

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

520 
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

521 
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

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

523 
Arith_Data.simplify_meta_eq [] ctxt 
45775  524 
([th, cancel_th] MRS trans) 
525 
fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) 

526 
end 

527 

528 
structure Eq_Enat_Cancel = ExtractCommonTermFun 

529 
(open Cancel_Enat_Common 

530 
val mk_bal = HOLogic.mk_eq 

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

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

533 
) 

534 

535 
structure Le_Enat_Cancel = ExtractCommonTermFun 

536 
(open Cancel_Enat_Common 

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

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

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

540 
) 

541 

542 
structure Less_Enat_Cancel = ExtractCommonTermFun 

543 
(open Cancel_Enat_Common 

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

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

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

547 
) 

548 
*} 

549 

550 
simproc_setup enat_eq_cancel 

551 
("(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

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

554 
simproc_setup enat_le_cancel 

555 
("(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

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

558 
simproc_setup enat_less_cancel 

559 
("(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

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

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

563 

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

565 

27110  566 
subsection {* Wellordering *} 
26089  567 

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

26089  570 
by (induct n) auto 
571 

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

572 
lemma less_infinityE: 
43924  573 
"[ n < \<infinity>; !!k. n = enat k ==> P ] ==> P" 
26089  574 
by (induct n) auto 
575 

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

26089  578 
proof  
43924  579 
have P_enat: "!!k. P (enat k)" 
26089  580 
apply (rule nat_less_induct) 
581 
apply (rule prem, clarify) 

43924  582 
apply (erule less_enatE, simp) 
26089  583 
done 
584 
show ?thesis 

585 
proof (induct n) 

586 
fix nat 

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

591 
apply (erule less_infinityE) 
43924  592 
apply (simp add: P_enat) 
26089  593 
done 
594 
qed 

595 
qed 

596 

43919  597 
instance enat :: wellorder 
26089  598 
proof 
27823  599 
fix P and n 
43919  600 
assume hyp: "(\<And>n\<Colon>enat. (\<And>m\<Colon>enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)" 
601 
show "P n" by (blast intro: enat_less_induct hyp) 

26089  602 
qed 
603 

42993  604 
subsection {* Complete Lattice *} 
605 

54415  606 
text {* TODO: enat as order topology? *} 
607 

43919  608 
instantiation enat :: complete_lattice 
42993  609 
begin 
610 

43919  611 
definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where 
612 
"inf_enat \<equiv> min" 

42993  613 

43919  614 
definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where 
615 
"sup_enat \<equiv> max" 

42993  616 

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

42993  619 

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

42993  622 
else if finite A then Max A 
623 
else \<infinity>" 

624 
instance proof 

43919  625 
fix x :: "enat" and A :: "enat set" 
42993  626 
{ assume "x \<in> A" then show "Inf A \<le> x" 
43919  627 
unfolding Inf_enat_def by (auto intro: Least_le) } 
42993  628 
{ assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A" 
43919  629 
unfolding Inf_enat_def 
42993  630 
by (cases "A = {}") (auto intro: LeastI2_ex) } 
631 
{ assume "x \<in> A" then show "x \<le> Sup A" 

43919  632 
unfolding Sup_enat_def by (cases "finite A") auto } 
42993  633 
{ assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x" 
43924  634 
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

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

636 
inf_enat_def sup_enat_def bot_enat_def top_enat_def Inf_enat_def Sup_enat_def) 
42993  637 
end 
638 

43978  639 
instance enat :: complete_linorder .. 
27110  640 

641 
subsection {* Traditional theorem names *} 

642 

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

643 
lemmas enat_defs = zero_enat_def one_enat_def eSuc_def 
43919  644 
plus_enat_def less_eq_enat_def less_enat_def 
27110  645 

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

646 
end 