author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64267  b9a1486e79be 
child 67091  1393c2340eec 
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 

60500  6 
section \<open>Extended natural numbers (i.e. with infinity)\<close> 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

7 

43919  8 
theory Extended_Nat 
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

9 
imports Main Countable Order_Continuity 
15131  10 
begin 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

11 

43921  12 
class infinity = 
61384  13 
fixes infinity :: "'a" ("\<infinity>") 
43921  14 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

15 
context 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

16 
fixes f :: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add, linorder_topology, complete_linorder}" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

17 
begin 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

18 

85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

19 
lemma sums_SUP[simp, intro]: "f sums (SUP n. \<Sum>i<n. f i)" 
64267  20 
unfolding sums_def by (intro LIMSEQ_SUP monoI sum_mono2 zero_le) auto 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

21 

85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

22 
lemma suminf_eq_SUP: "suminf f = (SUP n. \<Sum>i<n. f i)" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

23 
using sums_SUP by (rule sums_unique[symmetric]) 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

24 

85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

25 
end 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

26 

60500  27 
subsection \<open>Type definition\<close> 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

28 

60500  29 
text \<open> 
11355  30 
We extend the standard natural numbers by a special value indicating 
27110  31 
infinity. 
60500  32 
\<close> 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

33 

49834  34 
typedef enat = "UNIV :: nat option set" .. 
54415  35 

60500  36 
text \<open>TODO: introduce enat as coinductive datatype, enat is just @{const of_nat}\<close> 
54415  37 

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

62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
61631
diff
changeset

40 

43921  41 
instantiation enat :: infinity 
42 
begin 

60679  43 

44 
definition "\<infinity> = Abs_enat None" 

45 
instance .. 

46 

43921  47 
end 
54415  48 

49 
instance enat :: countable 

50 
proof 

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

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

53 
qed 

62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
61631
diff
changeset

54 

58306
117ba6cbe414
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
blanchet
parents:
57514
diff
changeset

55 
old_rep_datatype enat "\<infinity> :: enat" 
43921  56 
proof  
43924  57 
fix P i assume "\<And>j. P (enat j)" "P \<infinity>" 
43921  58 
then show "P i" 
59 
proof induct 

60 
case (Abs_enat y) then show ?case 

61 
by (cases y rule: option.exhaust) 

43924  62 
(auto simp: enat_def infinity_enat_def) 
43921  63 
qed 
43924  64 
qed (auto simp add: enat_def infinity_enat_def Abs_enat_inject) 
19736  65 

43924  66 
declare [[coercion "enat::nat\<Rightarrow>enat"]] 
19736  67 

45934  68 
lemmas enat2_cases = enat.exhaust[case_product enat.exhaust] 
69 
lemmas enat3_cases = enat.exhaust[case_product enat.exhaust enat.exhaust] 

70 

54416  71 
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

72 
by (cases x) auto 
31084  73 

54416  74 
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

75 
by (cases x) auto 
31077  76 

62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62374
diff
changeset

77 
lemma enat_ex_split: "(\<exists>c::enat. P c) \<longleftrightarrow> P \<infinity> \<or> (\<exists>c::nat. P c)" 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62374
diff
changeset

78 
by (metis enat.exhaust) 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62374
diff
changeset

79 

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

81 
where "the_enat (enat n) = n" 
41855  82 

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

83 

60500  84 
subsection \<open>Constructors and numbers\<close> 
27110  85 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

86 
instantiation enat :: zero_neq_one 
25594  87 
begin 
88 

89 
definition 

43924  90 
"0 = enat 0" 
25594  91 

92 
definition 

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

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

94 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

95 
instance 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

96 
proof qed (simp add: zero_enat_def one_enat_def) 
25594  97 

98 
end 

99 

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

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

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

102 

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

103 
lemma enat_0 [code_post]: "enat 0 = 0" 
43919  104 
by (simp add: zero_enat_def) 
27110  105 

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

106 
lemma enat_1 [code_post]: "enat 1 = 1" 
43919  107 
by (simp add: one_enat_def) 
27110  108 

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

111 

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

113 
by (auto simp add: one_enat_def) 

114 

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

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

116 
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

117 

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

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

120 

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

121 
lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)" 
43919  122 
by (simp add: zero_enat_def) 
27110  123 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

124 
lemma zero_one_enat_neq: 
61076  125 
"\<not> 0 = (1::enat)" 
126 
"\<not> 1 = (0::enat)" 

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

128 

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

129 
lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1" 
43919  130 
by (simp add: one_enat_def) 
27110  131 

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

132 
lemma i1_ne_infinity [simp]: "1 \<noteq> (\<infinity>::enat)" 
43919  133 
by (simp add: one_enat_def) 
27110  134 

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

135 
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

136 
by (simp add: eSuc_def) 
27110  137 

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

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

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

140 

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

141 
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

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

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

144 
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

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

146 

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

147 
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

148 
by (simp add: eSuc_def split: enat.splits) 
27110  149 

59000  150 
lemma eSuc_enat_iff: "eSuc x = enat y \<longleftrightarrow> (\<exists>n. y = Suc n \<and> x = enat n)" 
151 
by (cases y) (auto simp: enat_0 eSuc_enat[symmetric]) 

152 

153 
lemma enat_eSuc_iff: "enat y = eSuc x \<longleftrightarrow> (\<exists>n. y = Suc n \<and> enat n = x)" 

154 
by (cases y) (auto simp: enat_0 eSuc_enat[symmetric]) 

155 

60500  156 
subsection \<open>Addition\<close> 
27110  157 

43919  158 
instantiation enat :: comm_monoid_add 
27110  159 
begin 
160 

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

163 

43919  164 
lemma plus_enat_simps [simp, code]: 
43921  165 
fixes q :: enat 
43924  166 
shows "enat m + enat n = enat (m + n)" 
43921  167 
and "\<infinity> + q = \<infinity>" 
168 
and "q + \<infinity> = \<infinity>" 

43919  169 
by (simp_all add: plus_enat_def split: enat.splits) 
27110  170 

60679  171 
instance 
172 
proof 

43919  173 
fix n m q :: enat 
27110  174 
show "n + m + q = n + (m + q)" 
45934  175 
by (cases n m q rule: enat3_cases) auto 
27110  176 
show "n + m = m + n" 
45934  177 
by (cases n m rule: enat2_cases) auto 
27110  178 
show "0 + n = n" 
43919  179 
by (cases n) (simp_all add: zero_enat_def) 
26089  180 
qed 
181 

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

183 

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

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

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

186 
by (cases n) (simp_all add: eSuc_enat one_enat_def) 
62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
61631
diff
changeset

187 

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

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

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

190 
"q + 1 = eSuc q" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

191 
by (simp_all add: eSuc_plus_1 ac_simps) 
41853  192 

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

193 
lemma iadd_Suc: "eSuc m + n = eSuc (m + n)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

195 

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

196 
lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56777
diff
changeset

197 
by (simp only: add.commute[of m] iadd_Suc) 
41853  198 

60500  199 
subsection \<open>Multiplication\<close> 
29014  200 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

201 
instantiation enat :: "{comm_semiring_1, semiring_no_zero_divisors}" 
29014  202 
begin 
203 

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

29014  207 

43919  208 
lemma times_enat_simps [simp, code]: 
43924  209 
"enat m * enat n = enat (m * n)" 
43921  210 
"\<infinity> * \<infinity> = (\<infinity>::enat)" 
43924  211 
"\<infinity> * enat n = (if n = 0 then 0 else \<infinity>)" 
212 
"enat m * \<infinity> = (if m = 0 then 0 else \<infinity>)" 

43919  213 
unfolding times_enat_def zero_enat_def 
214 
by (simp_all split: enat.split) 

29014  215 

60679  216 
instance 
217 
proof 

43919  218 
fix a b c :: enat 
29014  219 
show "(a * b) * c = a * (b * c)" 
43919  220 
unfolding times_enat_def zero_enat_def 
221 
by (simp split: enat.split) 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

222 
show comm: "a * b = b * a" 
43919  223 
unfolding times_enat_def zero_enat_def 
224 
by (simp split: enat.split) 

29014  225 
show "1 * a = a" 
43919  226 
unfolding times_enat_def zero_enat_def one_enat_def 
227 
by (simp split: enat.split) 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

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

230 
by (simp split: enat.split add: distrib_right) 
29014  231 
show "0 * a = 0" 
43919  232 
unfolding times_enat_def zero_enat_def 
233 
by (simp split: enat.split) 

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

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

237 
show "a * (b + c) = a * b + a * c" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

238 
by (cases a b c rule: enat3_cases) (auto simp: times_enat_def zero_enat_def distrib_left) 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

239 
show "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

240 
by (cases a b rule: enat2_cases) (auto simp: times_enat_def zero_enat_def) 
29014  241 
qed 
242 

243 
end 

244 

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

245 
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

246 
unfolding eSuc_plus_1 by (simp add: algebra_simps) 
29014  247 

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

248 
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

249 
unfolding eSuc_plus_1 by (simp add: algebra_simps) 
29014  250 

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

254 
apply (simp add: plus_1_eSuc eSuc_enat) 
29023  255 
done 
256 

60679  257 
instance enat :: semiring_char_0 
258 
proof 

43924  259 
have "inj enat" by (rule injI) simp 
260 
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

261 
qed 
29023  262 

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

263 
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

264 
by (auto simp add: times_enat_def zero_enat_def split: enat.split) 
41853  265 

60500  266 
subsection \<open>Numerals\<close> 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset

267 

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

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

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

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

271 

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

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

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

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

275 

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

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

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

278 

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

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

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

281 

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

282 
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

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

284 

60500  285 
subsection \<open>Subtraction\<close> 
41853  286 

43919  287 
instantiation enat :: minus 
41853  288 
begin 
289 

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

294 
instance .. 

295 

296 
end 

297 

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

298 
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

299 
by (simp add: diff_enat_def) 
41853  300 

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

301 
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

302 
by (simp add: diff_enat_def) 
41853  303 

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

304 
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

305 
by (simp add: diff_enat_def) 
41853  306 

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

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

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

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

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

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

312 
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

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

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

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

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

317 
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

318 
by (auto simp: zero_enat_def) 
41853  319 

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

320 
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

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

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

323 
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

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

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

60500  328 
subsection \<open>Ordering\<close> 
27110  329 

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

332 

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

336 

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

340 

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

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

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

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

43919  348 
by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

349 

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

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

351 
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

352 
by (auto simp: numeral_eq_enat) 
45934  353 

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

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

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

356 
by (auto simp: numeral_eq_enat) 
45934  357 

43919  358 
lemma enat_ord_code [code]: 
43924  359 
"enat m \<le> enat n \<longleftrightarrow> m \<le> n" 
360 
"enat m < enat n \<longleftrightarrow> m < n" 

43921  361 
"q \<le> (\<infinity>::enat) \<longleftrightarrow> True" 
43924  362 
"enat m < \<infinity> \<longleftrightarrow> True" 
363 
"\<infinity> \<le> enat n \<longleftrightarrow> False" 

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

366 

60679  367 
instance 
368 
by standard (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

369 

27110  370 
end 
371 

62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62374
diff
changeset

372 
instance enat :: dioid 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62374
diff
changeset

373 
proof 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62374
diff
changeset

374 
fix a b :: enat show "(a \<le> b) = (\<exists>c. b = a + c)" 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62374
diff
changeset

375 
by (cases a b rule: enat2_cases) (auto simp: le_iff_add enat_ex_split) 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62374
diff
changeset

376 
qed 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62374
diff
changeset

377 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

378 
instance enat :: "{linordered_nonzero_semiring, strict_ordered_comm_monoid_add}" 
29014  379 
proof 
43919  380 
fix a b c :: enat 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

381 
show "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow>c * a \<le> c * b" 
43919  382 
unfolding times_enat_def less_eq_enat_def zero_enat_def 
383 
by (simp split: enat.splits) 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

384 
show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" for a b c d :: enat 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

385 
by (cases a b c d rule: enat2_cases[case_product enat2_cases]) auto 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

386 
qed (simp add: zero_enat_def one_enat_def) 
29014  387 

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

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

389 
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

390 
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

391 
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

392 

43919  393 
lemma enat_ord_number [simp]: 
61076  394 
"(numeral m :: enat) \<le> numeral n \<longleftrightarrow> (numeral m :: nat) \<le> numeral n" 
395 
"(numeral m :: enat) < numeral n \<longleftrightarrow> (numeral m :: nat) < numeral n" 

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

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

397 

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

398 
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

399 
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

400 

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

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

403 

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

404 
lemma 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

405 
by (simp add: eSuc_def less_eq_enat_def split: enat.splits) 
62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
61631
diff
changeset

406 

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

407 
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

408 
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

409 

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

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

411 
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

412 

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

413 
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

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

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

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

417 
by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.splits) 
27110  418 

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

419 
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

420 
by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.split) 
41853  421 

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

422 
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

423 
by (simp add: eSuc_def less_eq_enat_def less_enat_def split: enat.splits) 
27110  424 

43924  425 
lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n" 
27110  426 
by (cases n) auto 
427 

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

428 
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

429 
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

430 

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

431 
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

432 
by (simp add: zero_enat_def less_enat_def split: enat.splits) 
41853  433 

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

434 
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

435 
by (simp add: zero_enat_def less_enat_def split: enat.splits) 
41853  436 

43919  437 
lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)" 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

438 
by (simp only: zero_less_iff_neq_zero mult_eq_0_iff, simp) 
41853  439 

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

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

441 
by (simp add: mono_def) 
41853  442 

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

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

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

450 

43919  451 
lemma max_enat_simps [simp]: 
43924  452 
"max (enat m) (enat n) = enat (max m n)" 
27110  453 
"max q 0 = q" 
454 
"max 0 q = q" 

43921  455 
"max q \<infinity> = (\<infinity>::enat)" 
456 
"max \<infinity> q = (\<infinity>::enat)" 

27110  457 
by (simp_all add: max_def) 
458 

43924  459 
lemma enat_ile: "n \<le> enat m \<Longrightarrow> \<exists>k. n = enat k" 
27110  460 
by (cases n) simp_all 
461 

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

464 

61631
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61384
diff
changeset

465 
lemma iadd_le_enat_iff: 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61384
diff
changeset

466 
"x + y \<le> enat n \<longleftrightarrow> (\<exists>y' x'. x = enat x' \<and> y = enat y' \<and> x' + y' \<le> n)" 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61384
diff
changeset

467 
by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all 
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61384
diff
changeset

468 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

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

470 
apply (induct_tac k) 
43924  471 
apply (simp (no_asm) only: enat_0) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

472 
apply (fast intro: le_less_trans [OF zero_le]) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

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

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

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

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

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

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

481 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

482 
lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)" 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

483 
by (simp add: eSuc_def split: enat.split) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

484 

62374
cb27a55d868a
remove lattice syntax from countable complete lattice
hoelzl
parents:
61631
diff
changeset

485 
lemma eSuc_Max: 
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

486 
assumes "finite A" "A \<noteq> {}" 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

487 
shows "eSuc (Max A) = Max (eSuc ` A)" 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

488 
using assms proof induction 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

489 
case (insert x A) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

490 
thus ?case by(cases "A = {}")(simp_all add: eSuc_max) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

491 
qed simp 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

492 

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

493 
instantiation enat :: "{order_bot, order_top}" 
29337  494 
begin 
495 

60679  496 
definition bot_enat :: enat where "bot_enat = 0" 
497 
definition top_enat :: enat where "top_enat = \<infinity>" 

29337  498 

60679  499 
instance 
500 
by standard (simp_all add: bot_enat_def top_enat_def) 

29337  501 

502 
end 

503 

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

42993  506 
shows "finite A" 
507 
proof (rule finite_subset) 

43924  508 
show "finite (enat ` {..n})" by blast 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44019
diff
changeset

509 
have "A \<subseteq> {..enat n}" using le_fin by fastforce 
43924  510 
also have "\<dots> \<subseteq> enat ` {..n}" 
60679  511 
apply (rule subsetI) 
512 
subgoal for x by (cases x) auto 

513 
done 

43924  514 
finally show "A \<subseteq> enat ` {..n}" . 
42993  515 
qed 
516 

26089  517 

60500  518 
subsection \<open>Cancellation simprocs\<close> 
45775  519 

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

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

522 

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

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

525 

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

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

528 

60500  529 
ML \<open> 
45775  530 
structure Cancel_Enat_Common = 
531 
struct 

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

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

534 
 find_first_t past u (t::terms) = 

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

536 
else find_first_t (t::past) u terms 

537 

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

538 
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

539 
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

540 
 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

541 

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

543 
fun dest_sum t = dest_summing (t, []) 
45775  544 
val find_first = find_first_t [] 
545 
val trans_tac = Numeral_Simprocs.trans_tac 

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

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

547 
simpset_of (put_simpset HOL_basic_ss @{context} 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

549 
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

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

551 
Arith_Data.simplify_meta_eq [] ctxt 
45775  552 
([th, cancel_th] MRS trans) 
553 
fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) 

554 
end 

555 

556 
structure Eq_Enat_Cancel = ExtractCommonTermFun 

557 
(open Cancel_Enat_Common 

558 
val mk_bal = HOLogic.mk_eq 

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

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

561 
) 

562 

563 
structure Le_Enat_Cancel = ExtractCommonTermFun 

564 
(open Cancel_Enat_Common 

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

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

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

568 
) 

569 

570 
structure Less_Enat_Cancel = ExtractCommonTermFun 

571 
(open Cancel_Enat_Common 

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

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

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

575 
) 

60500  576 
\<close> 
45775  577 

578 
simproc_setup enat_eq_cancel 

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

60500  580 
\<open>fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close> 
45775  581 

582 
simproc_setup enat_le_cancel 

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

60500  584 
\<open>fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close> 
45775  585 

586 
simproc_setup enat_less_cancel 

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

60500  588 
\<open>fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close> 
45775  589 

60500  590 
text \<open>TODO: add regression tests for these simprocs\<close> 
45775  591 

60500  592 
text \<open>TODO: add simprocs for combining and cancelling numerals\<close> 
45775  593 

60500  594 
subsection \<open>Wellordering\<close> 
26089  595 

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

26089  598 
by (induct n) auto 
599 

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

600 
lemma less_infinityE: 
43924  601 
"[ n < \<infinity>; !!k. n = enat k ==> P ] ==> P" 
26089  602 
by (induct n) auto 
603 

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

26089  606 
proof  
43924  607 
have P_enat: "!!k. P (enat k)" 
26089  608 
apply (rule nat_less_induct) 
609 
apply (rule prem, clarify) 

43924  610 
apply (erule less_enatE, simp) 
26089  611 
done 
612 
show ?thesis 

613 
proof (induct n) 

614 
fix nat 

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

619 
apply (erule less_infinityE) 
43924  620 
apply (simp add: P_enat) 
26089  621 
done 
622 
qed 

623 
qed 

624 

43919  625 
instance enat :: wellorder 
26089  626 
proof 
27823  627 
fix P and n 
61076  628 
assume hyp: "(\<And>n::enat. (\<And>m::enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)" 
43919  629 
show "P n" by (blast intro: enat_less_induct hyp) 
26089  630 
qed 
631 

60500  632 
subsection \<open>Complete Lattice\<close> 
42993  633 

43919  634 
instantiation enat :: complete_lattice 
42993  635 
begin 
636 

43919  637 
definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where 
56777  638 
"inf_enat = min" 
42993  639 

43919  640 
definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where 
56777  641 
"sup_enat = max" 
42993  642 

43919  643 
definition Inf_enat :: "enat set \<Rightarrow> enat" where 
56777  644 
"Inf_enat A = (if A = {} then \<infinity> else (LEAST x. x \<in> A))" 
42993  645 

43919  646 
definition Sup_enat :: "enat set \<Rightarrow> enat" where 
56777  647 
"Sup_enat A = (if A = {} then 0 else if finite A then Max A else \<infinity>)" 
648 
instance 

649 
proof 

43919  650 
fix x :: "enat" and A :: "enat set" 
42993  651 
{ assume "x \<in> A" then show "Inf A \<le> x" 
43919  652 
unfolding Inf_enat_def by (auto intro: Least_le) } 
42993  653 
{ assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A" 
43919  654 
unfolding Inf_enat_def 
42993  655 
by (cases "A = {}") (auto intro: LeastI2_ex) } 
656 
{ assume "x \<in> A" then show "x \<le> Sup A" 

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

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

661 
inf_enat_def sup_enat_def bot_enat_def top_enat_def Inf_enat_def Sup_enat_def) 
42993  662 
end 
663 

43978  664 
instance enat :: complete_linorder .. 
27110  665 

60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

666 
lemma eSuc_Sup: "A \<noteq> {} \<Longrightarrow> eSuc (Sup A) = Sup (eSuc ` A)" 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

667 
by(auto simp add: Sup_enat_def eSuc_Max inj_on_def dest: finite_imageD) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

668 

ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

669 
lemma sup_continuous_eSuc: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. eSuc (f x))" 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

670 
using eSuc_Sup[of "_ ` UNIV"] by (auto simp: sup_continuous_def) 
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset

671 

60500  672 
subsection \<open>Traditional theorem names\<close> 
27110  673 

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

674 
lemmas enat_defs = zero_enat_def one_enat_def eSuc_def 
43919  675 
plus_enat_def less_eq_enat_def less_enat_def 
27110  676 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

677 
lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

678 
by (rule add_eq_0_iff_both_eq_0) 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

679 

85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

680 
lemma i0_lb : "(0::enat) \<le> n" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

681 
by (rule zero_le) 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

682 

85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

683 
lemma ile0_eq: "n \<le> (0::enat) \<longleftrightarrow> n = 0" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

684 
by (rule le_zero_eq) 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

685 

85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

686 
lemma not_iless0: "\<not> n < (0::enat)" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

687 
by (rule not_less_zero) 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

688 

85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

689 
lemma i0_less[simp]: "(0::enat) < n \<longleftrightarrow> n \<noteq> 0" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

690 
by (rule zero_less_iff_neq_zero) 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

691 

85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

692 
lemma imult_is_0: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)" 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

693 
by (rule mult_eq_0_iff) 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

694 

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

695 
end 