author | haftmann |
Sat, 19 Dec 2015 17:03:17 +0100 | |
changeset 61891 | 76189756ff65 |
parent 61631 | 4f7ef088c4ed |
child 62374 | cb27a55d868a |
permissions | -rw-r--r-- |
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 |
|
15 |
||
60500 | 16 |
subsection \<open>Type definition\<close> |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
17 |
|
60500 | 18 |
text \<open> |
11355 | 19 |
We extend the standard natural numbers by a special value indicating |
27110 | 20 |
infinity. |
60500 | 21 |
\<close> |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
22 |
|
49834 | 23 |
typedef enat = "UNIV :: nat option set" .. |
54415 | 24 |
|
60500 | 25 |
text \<open>TODO: introduce enat as coinductive datatype, enat is just @{const of_nat}\<close> |
54415 | 26 |
|
43924 | 27 |
definition enat :: "nat \<Rightarrow> enat" where |
28 |
"enat n = Abs_enat (Some n)" |
|
43921 | 29 |
|
30 |
instantiation enat :: infinity |
|
31 |
begin |
|
60679 | 32 |
|
33 |
definition "\<infinity> = Abs_enat None" |
|
34 |
instance .. |
|
35 |
||
43921 | 36 |
end |
54415 | 37 |
|
38 |
instance enat :: countable |
|
39 |
proof |
|
40 |
show "\<exists>to_nat::enat \<Rightarrow> nat. inj to_nat" |
|
41 |
by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject) |
|
42 |
qed |
|
43921 | 43 |
|
58306
117ba6cbe414
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
blanchet
parents:
57514
diff
changeset
|
44 |
old_rep_datatype enat "\<infinity> :: enat" |
43921 | 45 |
proof - |
43924 | 46 |
fix P i assume "\<And>j. P (enat j)" "P \<infinity>" |
43921 | 47 |
then show "P i" |
48 |
proof induct |
|
49 |
case (Abs_enat y) then show ?case |
|
50 |
by (cases y rule: option.exhaust) |
|
43924 | 51 |
(auto simp: enat_def infinity_enat_def) |
43921 | 52 |
qed |
43924 | 53 |
qed (auto simp add: enat_def infinity_enat_def Abs_enat_inject) |
19736 | 54 |
|
43924 | 55 |
declare [[coercion "enat::nat\<Rightarrow>enat"]] |
19736 | 56 |
|
45934 | 57 |
lemmas enat2_cases = enat.exhaust[case_product enat.exhaust] |
58 |
lemmas enat3_cases = enat.exhaust[case_product enat.exhaust enat.exhaust] |
|
59 |
||
54416 | 60 |
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
|
61 |
by (cases x) auto |
31084 | 62 |
|
54416 | 63 |
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
|
64 |
by (cases x) auto |
31077 | 65 |
|
43924 | 66 |
primrec the_enat :: "enat \<Rightarrow> nat" |
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
67 |
where "the_enat (enat n) = n" |
41855 | 68 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
69 |
|
60500 | 70 |
subsection \<open>Constructors and numbers\<close> |
27110 | 71 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
72 |
instantiation enat :: "{zero, one}" |
25594 | 73 |
begin |
74 |
||
75 |
definition |
|
43924 | 76 |
"0 = enat 0" |
25594 | 77 |
|
78 |
definition |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
79 |
"1 = enat 1" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
80 |
|
25594 | 81 |
instance .. |
82 |
||
83 |
end |
|
84 |
||
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
85 |
definition eSuc :: "enat \<Rightarrow> enat" where |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
86 |
"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
|
87 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
88 |
lemma enat_0 [code_post]: "enat 0 = 0" |
43919 | 89 |
by (simp add: zero_enat_def) |
27110 | 90 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
91 |
lemma enat_1 [code_post]: "enat 1 = 1" |
43919 | 92 |
by (simp add: one_enat_def) |
27110 | 93 |
|
54416 | 94 |
lemma enat_0_iff: "enat x = 0 \<longleftrightarrow> x = 0" "0 = enat x \<longleftrightarrow> x = 0" |
95 |
by (auto simp add: zero_enat_def) |
|
96 |
||
97 |
lemma enat_1_iff: "enat x = 1 \<longleftrightarrow> x = 1" "1 = enat x \<longleftrightarrow> x = 1" |
|
98 |
by (auto simp add: one_enat_def) |
|
99 |
||
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
100 |
lemma one_eSuc: "1 = eSuc 0" |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
101 |
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
|
102 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
103 |
lemma infinity_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0" |
43919 | 104 |
by (simp add: zero_enat_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
105 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
106 |
lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)" |
43919 | 107 |
by (simp add: zero_enat_def) |
27110 | 108 |
|
43919 | 109 |
lemma zero_one_enat_neq [simp]: |
61076 | 110 |
"\<not> 0 = (1::enat)" |
111 |
"\<not> 1 = (0::enat)" |
|
43919 | 112 |
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
|
113 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
114 |
lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1" |
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 i1_ne_infinity [simp]: "1 \<noteq> (\<infinity>::enat)" |
43919 | 118 |
by (simp add: one_enat_def) |
27110 | 119 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
120 |
lemma eSuc_enat: "eSuc (enat n) = enat (Suc n)" |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
121 |
by (simp add: eSuc_def) |
27110 | 122 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
123 |
lemma eSuc_infinity [simp]: "eSuc \<infinity> = \<infinity>" |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
124 |
by (simp add: eSuc_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
125 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
126 |
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
|
127 |
by (simp add: eSuc_def zero_enat_def split: enat.splits) |
27110 | 128 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
129 |
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
|
130 |
by (rule eSuc_ne_0 [symmetric]) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
131 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
132 |
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
|
133 |
by (simp add: eSuc_def split: enat.splits) |
27110 | 134 |
|
59000 | 135 |
lemma eSuc_enat_iff: "eSuc x = enat y \<longleftrightarrow> (\<exists>n. y = Suc n \<and> x = enat n)" |
136 |
by (cases y) (auto simp: enat_0 eSuc_enat[symmetric]) |
|
137 |
||
138 |
lemma enat_eSuc_iff: "enat y = eSuc x \<longleftrightarrow> (\<exists>n. y = Suc n \<and> enat n = x)" |
|
139 |
by (cases y) (auto simp: enat_0 eSuc_enat[symmetric]) |
|
140 |
||
60500 | 141 |
subsection \<open>Addition\<close> |
27110 | 142 |
|
43919 | 143 |
instantiation enat :: comm_monoid_add |
27110 | 144 |
begin |
145 |
||
38167 | 146 |
definition [nitpick_simp]: |
43924 | 147 |
"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
|
148 |
|
43919 | 149 |
lemma plus_enat_simps [simp, code]: |
43921 | 150 |
fixes q :: enat |
43924 | 151 |
shows "enat m + enat n = enat (m + n)" |
43921 | 152 |
and "\<infinity> + q = \<infinity>" |
153 |
and "q + \<infinity> = \<infinity>" |
|
43919 | 154 |
by (simp_all add: plus_enat_def split: enat.splits) |
27110 | 155 |
|
60679 | 156 |
instance |
157 |
proof |
|
43919 | 158 |
fix n m q :: enat |
27110 | 159 |
show "n + m + q = n + (m + q)" |
45934 | 160 |
by (cases n m q rule: enat3_cases) auto |
27110 | 161 |
show "n + m = m + n" |
45934 | 162 |
by (cases n m rule: enat2_cases) auto |
27110 | 163 |
show "0 + n = n" |
43919 | 164 |
by (cases n) (simp_all add: zero_enat_def) |
26089 | 165 |
qed |
166 |
||
27110 | 167 |
end |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
168 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
169 |
lemma eSuc_plus_1: |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
170 |
"eSuc n = n + 1" |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
171 |
by (cases n) (simp_all add: eSuc_enat one_enat_def) |
27110 | 172 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
173 |
lemma plus_1_eSuc: |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
174 |
"1 + q = eSuc q" |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
175 |
"q + 1 = eSuc q" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
176 |
by (simp_all add: eSuc_plus_1 ac_simps) |
41853 | 177 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
178 |
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
|
179 |
by (simp_all add: eSuc_plus_1 ac_simps) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
180 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
181 |
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
|
182 |
by (simp only: add.commute[of m] iadd_Suc) |
41853 | 183 |
|
43919 | 184 |
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
|
185 |
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
|
186 |
|
60500 | 187 |
subsection \<open>Multiplication\<close> |
29014 | 188 |
|
43919 | 189 |
instantiation enat :: comm_semiring_1 |
29014 | 190 |
begin |
191 |
||
43919 | 192 |
definition times_enat_def [nitpick_simp]: |
43924 | 193 |
"m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | enat m \<Rightarrow> |
194 |
(case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | enat n \<Rightarrow> enat (m * n)))" |
|
29014 | 195 |
|
43919 | 196 |
lemma times_enat_simps [simp, code]: |
43924 | 197 |
"enat m * enat n = enat (m * n)" |
43921 | 198 |
"\<infinity> * \<infinity> = (\<infinity>::enat)" |
43924 | 199 |
"\<infinity> * enat n = (if n = 0 then 0 else \<infinity>)" |
200 |
"enat m * \<infinity> = (if m = 0 then 0 else \<infinity>)" |
|
43919 | 201 |
unfolding times_enat_def zero_enat_def |
202 |
by (simp_all split: enat.split) |
|
29014 | 203 |
|
60679 | 204 |
instance |
205 |
proof |
|
43919 | 206 |
fix a b c :: enat |
29014 | 207 |
show "(a * b) * c = a * (b * c)" |
43919 | 208 |
unfolding times_enat_def zero_enat_def |
209 |
by (simp split: enat.split) |
|
29014 | 210 |
show "a * b = b * a" |
43919 | 211 |
unfolding times_enat_def zero_enat_def |
212 |
by (simp split: enat.split) |
|
29014 | 213 |
show "1 * a = a" |
43919 | 214 |
unfolding times_enat_def zero_enat_def one_enat_def |
215 |
by (simp split: enat.split) |
|
29014 | 216 |
show "(a + b) * c = a * c + b * c" |
43919 | 217 |
unfolding times_enat_def zero_enat_def |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49834
diff
changeset
|
218 |
by (simp split: enat.split add: distrib_right) |
29014 | 219 |
show "0 * a = 0" |
43919 | 220 |
unfolding times_enat_def zero_enat_def |
221 |
by (simp split: enat.split) |
|
29014 | 222 |
show "a * 0 = 0" |
43919 | 223 |
unfolding times_enat_def zero_enat_def |
224 |
by (simp split: enat.split) |
|
225 |
show "(0::enat) \<noteq> 1" |
|
226 |
unfolding zero_enat_def one_enat_def |
|
29014 | 227 |
by simp |
228 |
qed |
|
229 |
||
230 |
end |
|
231 |
||
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
232 |
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
|
233 |
unfolding eSuc_plus_1 by (simp add: algebra_simps) |
29014 | 234 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
235 |
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
|
236 |
unfolding eSuc_plus_1 by (simp add: algebra_simps) |
29014 | 237 |
|
43924 | 238 |
lemma of_nat_eq_enat: "of_nat n = enat n" |
29023 | 239 |
apply (induct n) |
43924 | 240 |
apply (simp add: enat_0) |
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
241 |
apply (simp add: plus_1_eSuc eSuc_enat) |
29023 | 242 |
done |
243 |
||
60679 | 244 |
instance enat :: semiring_char_0 |
245 |
proof |
|
43924 | 246 |
have "inj enat" by (rule injI) simp |
247 |
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
|
248 |
qed |
29023 | 249 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
250 |
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
|
251 |
by (auto simp add: times_enat_def zero_enat_def split: enat.split) |
41853 | 252 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
253 |
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
|
254 |
by (auto simp add: times_enat_def zero_enat_def split: enat.split) |
41853 | 255 |
|
256 |
||
60500 | 257 |
subsection \<open>Numerals\<close> |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
258 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
259 |
lemma numeral_eq_enat: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
260 |
"numeral k = enat (numeral k)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
261 |
using of_nat_eq_enat [of "numeral k"] by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
262 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
263 |
lemma enat_numeral [code_abbrev]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
264 |
"enat (numeral k) = numeral k" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
265 |
using numeral_eq_enat .. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
266 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
267 |
lemma infinity_ne_numeral [simp]: "(\<infinity>::enat) \<noteq> numeral k" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
268 |
by (simp add: numeral_eq_enat) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
269 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
270 |
lemma numeral_ne_infinity [simp]: "numeral k \<noteq> (\<infinity>::enat)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
271 |
by (simp add: numeral_eq_enat) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
272 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
273 |
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
|
274 |
by (simp only: eSuc_plus_1 numeral_plus_one) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
275 |
|
60500 | 276 |
subsection \<open>Subtraction\<close> |
41853 | 277 |
|
43919 | 278 |
instantiation enat :: minus |
41853 | 279 |
begin |
280 |
||
43919 | 281 |
definition diff_enat_def: |
43924 | 282 |
"a - b = (case a of (enat x) \<Rightarrow> (case b of (enat y) \<Rightarrow> enat (x - y) | \<infinity> \<Rightarrow> 0) |
41853 | 283 |
| \<infinity> \<Rightarrow> \<infinity>)" |
284 |
||
285 |
instance .. |
|
286 |
||
287 |
end |
|
288 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
289 |
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
|
290 |
by (simp add: diff_enat_def) |
41853 | 291 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
292 |
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
|
293 |
by (simp add: diff_enat_def) |
41853 | 294 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
295 |
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
|
296 |
by (simp add: diff_enat_def) |
41853 | 297 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
298 |
lemma idiff_0 [simp]: "(0::enat) - n = 0" |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
299 |
by (cases n, simp_all add: zero_enat_def) |
41853 | 300 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
301 |
lemmas idiff_enat_0 [simp] = idiff_0 [unfolded zero_enat_def] |
41853 | 302 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
303 |
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
|
304 |
by (cases n) (simp_all add: zero_enat_def) |
41853 | 305 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
306 |
lemmas idiff_enat_0_right [simp] = idiff_0_right [unfolded zero_enat_def] |
41853 | 307 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
308 |
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
|
309 |
by (auto simp: zero_enat_def) |
41853 | 310 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
311 |
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
|
312 |
by (simp add: eSuc_def split: enat.split) |
41855 | 313 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
314 |
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
|
315 |
by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric]) |
41855 | 316 |
|
43924 | 317 |
(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*) |
41853 | 318 |
|
60500 | 319 |
subsection \<open>Ordering\<close> |
27110 | 320 |
|
43919 | 321 |
instantiation enat :: linordered_ab_semigroup_add |
27110 | 322 |
begin |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
323 |
|
38167 | 324 |
definition [nitpick_simp]: |
43924 | 325 |
"m \<le> n = (case n of enat n1 \<Rightarrow> (case m of enat m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False) |
27110 | 326 |
| \<infinity> \<Rightarrow> True)" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
327 |
|
38167 | 328 |
definition [nitpick_simp]: |
43924 | 329 |
"m < n = (case m of enat m1 \<Rightarrow> (case n of enat n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True) |
27110 | 330 |
| \<infinity> \<Rightarrow> False)" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
331 |
|
43919 | 332 |
lemma enat_ord_simps [simp]: |
43924 | 333 |
"enat m \<le> enat n \<longleftrightarrow> m \<le> n" |
334 |
"enat m < enat n \<longleftrightarrow> m < n" |
|
43921 | 335 |
"q \<le> (\<infinity>::enat)" |
336 |
"q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>" |
|
337 |
"(\<infinity>::enat) \<le> q \<longleftrightarrow> q = \<infinity>" |
|
338 |
"(\<infinity>::enat) < q \<longleftrightarrow> False" |
|
43919 | 339 |
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
|
340 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
341 |
lemma numeral_le_enat_iff[simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
342 |
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
|
343 |
by (auto simp: numeral_eq_enat) |
45934 | 344 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
345 |
lemma numeral_less_enat_iff[simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
346 |
shows "numeral m < enat n \<longleftrightarrow> numeral m < n" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
347 |
by (auto simp: numeral_eq_enat) |
45934 | 348 |
|
43919 | 349 |
lemma enat_ord_code [code]: |
43924 | 350 |
"enat m \<le> enat n \<longleftrightarrow> m \<le> n" |
351 |
"enat m < enat n \<longleftrightarrow> m < n" |
|
43921 | 352 |
"q \<le> (\<infinity>::enat) \<longleftrightarrow> True" |
43924 | 353 |
"enat m < \<infinity> \<longleftrightarrow> True" |
354 |
"\<infinity> \<le> enat n \<longleftrightarrow> False" |
|
43921 | 355 |
"(\<infinity>::enat) < q \<longleftrightarrow> False" |
27110 | 356 |
by simp_all |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
357 |
|
60679 | 358 |
instance |
359 |
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
|
360 |
|
27110 | 361 |
end |
362 |
||
43919 | 363 |
instance enat :: ordered_comm_semiring |
29014 | 364 |
proof |
43919 | 365 |
fix a b c :: enat |
29014 | 366 |
assume "a \<le> b" and "0 \<le> c" |
367 |
thus "c * a \<le> c * b" |
|
43919 | 368 |
unfolding times_enat_def less_eq_enat_def zero_enat_def |
369 |
by (simp split: enat.splits) |
|
29014 | 370 |
qed |
371 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
372 |
(* 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
|
373 |
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
|
374 |
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
|
375 |
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
|
376 |
|
43919 | 377 |
lemma enat_ord_number [simp]: |
61076 | 378 |
"(numeral m :: enat) \<le> numeral n \<longleftrightarrow> (numeral m :: nat) \<le> numeral n" |
379 |
"(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
|
380 |
by (simp_all add: numeral_eq_enat) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
381 |
|
61076 | 382 |
lemma i0_lb [simp]: "(0::enat) \<le> n" |
43919 | 383 |
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
|
384 |
|
61076 | 385 |
lemma ile0_eq [simp]: "n \<le> (0::enat) \<longleftrightarrow> n = 0" |
43919 | 386 |
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
|
387 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
388 |
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
|
389 |
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
|
390 |
|
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
391 |
lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R" |
27110 | 392 |
by simp |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
393 |
|
61076 | 394 |
lemma not_iless0 [simp]: "\<not> n < (0::enat)" |
43919 | 395 |
by (simp add: zero_enat_def less_enat_def split: enat.splits) |
27110 | 396 |
|
61076 | 397 |
lemma i0_less [simp]: "(0::enat) < n \<longleftrightarrow> n \<noteq> 0" |
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
398 |
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
|
399 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
400 |
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
|
401 |
by (simp add: eSuc_def less_eq_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 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
|
404 |
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
|
405 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
406 |
lemma ile_eSuc [simp]: "n \<le> eSuc 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 split: enat.splits) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
408 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
409 |
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
|
410 |
by (simp add: zero_enat_def eSuc_def less_eq_enat_def split: enat.splits) |
27110 | 411 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
412 |
lemma i0_iless_eSuc [simp]: "0 < eSuc n" |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
413 |
by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.splits) |
27110 | 414 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
415 |
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
|
416 |
by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.split) |
41853 | 417 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
418 |
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
|
419 |
by (simp add: eSuc_def less_eq_enat_def less_enat_def split: enat.splits) |
27110 | 420 |
|
43924 | 421 |
lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n" |
27110 | 422 |
by (cases n) auto |
423 |
||
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
424 |
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
|
425 |
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
|
426 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
427 |
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
|
428 |
by (simp add: zero_enat_def less_enat_def split: enat.splits) |
41853 | 429 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
430 |
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
|
431 |
by (simp add: zero_enat_def less_enat_def split: enat.splits) |
41853 | 432 |
|
43919 | 433 |
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
|
434 |
by (simp only: i0_less imult_is_0, simp) |
41853 | 435 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
436 |
lemma mono_eSuc: "mono eSuc" |
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
437 |
by (simp add: mono_def) |
41853 | 438 |
|
439 |
||
43919 | 440 |
lemma min_enat_simps [simp]: |
43924 | 441 |
"min (enat m) (enat n) = enat (min m n)" |
27110 | 442 |
"min q 0 = 0" |
443 |
"min 0 q = 0" |
|
43921 | 444 |
"min q (\<infinity>::enat) = q" |
445 |
"min (\<infinity>::enat) q = q" |
|
27110 | 446 |
by (auto simp add: min_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
447 |
|
43919 | 448 |
lemma max_enat_simps [simp]: |
43924 | 449 |
"max (enat m) (enat n) = enat (max m n)" |
27110 | 450 |
"max q 0 = q" |
451 |
"max 0 q = q" |
|
43921 | 452 |
"max q \<infinity> = (\<infinity>::enat)" |
453 |
"max \<infinity> q = (\<infinity>::enat)" |
|
27110 | 454 |
by (simp_all add: max_def) |
455 |
||
43924 | 456 |
lemma enat_ile: "n \<le> enat m \<Longrightarrow> \<exists>k. n = enat k" |
27110 | 457 |
by (cases n) simp_all |
458 |
||
43924 | 459 |
lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k" |
27110 | 460 |
by (cases n) simp_all |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
461 |
|
61631
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61384
diff
changeset
|
462 |
lemma iadd_le_enat_iff: |
4f7ef088c4ed
add lemmas for extended nats and reals
Andreas Lochbihler
parents:
61384
diff
changeset
|
463 |
"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
|
464 |
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
|
465 |
|
43924 | 466 |
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
|
467 |
apply (induct_tac k) |
43924 | 468 |
apply (simp (no_asm) only: enat_0) |
27110 | 469 |
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
|
470 |
apply (erule exE) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
471 |
apply (drule spec) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
472 |
apply (erule exE) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
473 |
apply (drule ileI1) |
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
474 |
apply (rule eSuc_enat [THEN subst]) |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
475 |
apply (rule exI) |
27110 | 476 |
apply (erule (1) le_less_trans) |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
477 |
done |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
478 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset
|
479 |
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
|
480 |
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
|
481 |
|
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: |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset
|
483 |
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
|
484 |
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
|
485 |
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
|
486 |
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
|
487 |
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
|
488 |
qed simp |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset
|
489 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51717
diff
changeset
|
490 |
instantiation enat :: "{order_bot, order_top}" |
29337 | 491 |
begin |
492 |
||
60679 | 493 |
definition bot_enat :: enat where "bot_enat = 0" |
494 |
definition top_enat :: enat where "top_enat = \<infinity>" |
|
29337 | 495 |
|
60679 | 496 |
instance |
497 |
by standard (simp_all add: bot_enat_def top_enat_def) |
|
29337 | 498 |
|
499 |
end |
|
500 |
||
43924 | 501 |
lemma finite_enat_bounded: |
502 |
assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> enat n" |
|
42993 | 503 |
shows "finite A" |
504 |
proof (rule finite_subset) |
|
43924 | 505 |
show "finite (enat ` {..n})" by blast |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44019
diff
changeset
|
506 |
have "A \<subseteq> {..enat n}" using le_fin by fastforce |
43924 | 507 |
also have "\<dots> \<subseteq> enat ` {..n}" |
60679 | 508 |
apply (rule subsetI) |
509 |
subgoal for x by (cases x) auto |
|
510 |
done |
|
43924 | 511 |
finally show "A \<subseteq> enat ` {..n}" . |
42993 | 512 |
qed |
513 |
||
26089 | 514 |
|
60500 | 515 |
subsection \<open>Cancellation simprocs\<close> |
45775 | 516 |
|
517 |
lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c" |
|
518 |
unfolding plus_enat_def by (simp split: enat.split) |
|
519 |
||
520 |
lemma enat_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b \<le> c" |
|
521 |
unfolding plus_enat_def by (simp split: enat.split) |
|
522 |
||
523 |
lemma enat_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::enat) \<and> b < c" |
|
524 |
unfolding plus_enat_def by (simp split: enat.split) |
|
525 |
||
60500 | 526 |
ML \<open> |
45775 | 527 |
structure Cancel_Enat_Common = |
528 |
struct |
|
529 |
(* copied from src/HOL/Tools/nat_numeral_simprocs.ML *) |
|
530 |
fun find_first_t _ _ [] = raise TERM("find_first_t", []) |
|
531 |
| find_first_t past u (t::terms) = |
|
532 |
if u aconv t then (rev past @ terms) |
|
533 |
else find_first_t (t::past) u terms |
|
534 |
||
51366
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
huffman
parents:
51301
diff
changeset
|
535 |
fun dest_summing (Const (@{const_name Groups.plus}, _) $ t $ u, ts) = |
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
huffman
parents:
51301
diff
changeset
|
536 |
dest_summing (t, dest_summing (u, ts)) |
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
huffman
parents:
51301
diff
changeset
|
537 |
| dest_summing (t, ts) = t :: ts |
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
huffman
parents:
51301
diff
changeset
|
538 |
|
45775 | 539 |
val mk_sum = Arith_Data.long_mk_sum |
51366
abdcf1a7cabf
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
huffman
parents:
51301
diff
changeset
|
540 |
fun dest_sum t = dest_summing (t, []) |
45775 | 541 |
val find_first = find_first_t [] |
542 |
val trans_tac = Numeral_Simprocs.trans_tac |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset
|
543 |
val norm_ss = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset
|
544 |
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
|
545 |
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
|
546 |
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
|
547 |
fun simplify_meta_eq ctxt cancel_th th = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51366
diff
changeset
|
548 |
Arith_Data.simplify_meta_eq [] ctxt |
45775 | 549 |
([th, cancel_th] MRS trans) |
550 |
fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) |
|
551 |
end |
|
552 |
||
553 |
structure Eq_Enat_Cancel = ExtractCommonTermFun |
|
554 |
(open Cancel_Enat_Common |
|
555 |
val mk_bal = HOLogic.mk_eq |
|
556 |
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} @{typ enat} |
|
557 |
fun simp_conv _ _ = SOME @{thm enat_add_left_cancel} |
|
558 |
) |
|
559 |
||
560 |
structure Le_Enat_Cancel = ExtractCommonTermFun |
|
561 |
(open Cancel_Enat_Common |
|
562 |
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} |
|
563 |
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} @{typ enat} |
|
564 |
fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_le} |
|
565 |
) |
|
566 |
||
567 |
structure Less_Enat_Cancel = ExtractCommonTermFun |
|
568 |
(open Cancel_Enat_Common |
|
569 |
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} |
|
570 |
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} @{typ enat} |
|
571 |
fun simp_conv _ _ = SOME @{thm enat_add_left_cancel_less} |
|
572 |
) |
|
60500 | 573 |
\<close> |
45775 | 574 |
|
575 |
simproc_setup enat_eq_cancel |
|
576 |
("(l::enat) + m = n" | "(l::enat) = m + n") = |
|
60500 | 577 |
\<open>fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close> |
45775 | 578 |
|
579 |
simproc_setup enat_le_cancel |
|
580 |
("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") = |
|
60500 | 581 |
\<open>fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close> |
45775 | 582 |
|
583 |
simproc_setup enat_less_cancel |
|
584 |
("(l::enat) + m < n" | "(l::enat) < m + n") = |
|
60500 | 585 |
\<open>fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close> |
45775 | 586 |
|
60500 | 587 |
text \<open>TODO: add regression tests for these simprocs\<close> |
45775 | 588 |
|
60500 | 589 |
text \<open>TODO: add simprocs for combining and cancelling numerals\<close> |
45775 | 590 |
|
60500 | 591 |
subsection \<open>Well-ordering\<close> |
26089 | 592 |
|
43924 | 593 |
lemma less_enatE: |
594 |
"[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P" |
|
26089 | 595 |
by (induct n) auto |
596 |
||
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
597 |
lemma less_infinityE: |
43924 | 598 |
"[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P" |
26089 | 599 |
by (induct n) auto |
600 |
||
43919 | 601 |
lemma enat_less_induct: |
602 |
assumes prem: "!!n. \<forall>m::enat. m < n --> P m ==> P n" shows "P n" |
|
26089 | 603 |
proof - |
43924 | 604 |
have P_enat: "!!k. P (enat k)" |
26089 | 605 |
apply (rule nat_less_induct) |
606 |
apply (rule prem, clarify) |
|
43924 | 607 |
apply (erule less_enatE, simp) |
26089 | 608 |
done |
609 |
show ?thesis |
|
610 |
proof (induct n) |
|
611 |
fix nat |
|
43924 | 612 |
show "P (enat nat)" by (rule P_enat) |
26089 | 613 |
next |
43921 | 614 |
show "P \<infinity>" |
26089 | 615 |
apply (rule prem, clarify) |
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43978
diff
changeset
|
616 |
apply (erule less_infinityE) |
43924 | 617 |
apply (simp add: P_enat) |
26089 | 618 |
done |
619 |
qed |
|
620 |
qed |
|
621 |
||
43919 | 622 |
instance enat :: wellorder |
26089 | 623 |
proof |
27823 | 624 |
fix P and n |
61076 | 625 |
assume hyp: "(\<And>n::enat. (\<And>m::enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)" |
43919 | 626 |
show "P n" by (blast intro: enat_less_induct hyp) |
26089 | 627 |
qed |
628 |
||
60500 | 629 |
subsection \<open>Complete Lattice\<close> |
42993 | 630 |
|
43919 | 631 |
instantiation enat :: complete_lattice |
42993 | 632 |
begin |
633 |
||
43919 | 634 |
definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where |
56777 | 635 |
"inf_enat = min" |
42993 | 636 |
|
43919 | 637 |
definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where |
56777 | 638 |
"sup_enat = max" |
42993 | 639 |
|
43919 | 640 |
definition Inf_enat :: "enat set \<Rightarrow> enat" where |
56777 | 641 |
"Inf_enat A = (if A = {} then \<infinity> else (LEAST x. x \<in> A))" |
42993 | 642 |
|
43919 | 643 |
definition Sup_enat :: "enat set \<Rightarrow> enat" where |
56777 | 644 |
"Sup_enat A = (if A = {} then 0 else if finite A then Max A else \<infinity>)" |
645 |
instance |
|
646 |
proof |
|
43919 | 647 |
fix x :: "enat" and A :: "enat set" |
42993 | 648 |
{ assume "x \<in> A" then show "Inf A \<le> x" |
43919 | 649 |
unfolding Inf_enat_def by (auto intro: Least_le) } |
42993 | 650 |
{ assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A" |
43919 | 651 |
unfolding Inf_enat_def |
42993 | 652 |
by (cases "A = {}") (auto intro: LeastI2_ex) } |
653 |
{ assume "x \<in> A" then show "x \<le> Sup A" |
|
43919 | 654 |
unfolding Sup_enat_def by (cases "finite A") auto } |
42993 | 655 |
{ assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x" |
43924 | 656 |
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
|
657 |
qed (simp_all add: |
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
51717
diff
changeset
|
658 |
inf_enat_def sup_enat_def bot_enat_def top_enat_def Inf_enat_def Sup_enat_def) |
42993 | 659 |
end |
660 |
||
43978 | 661 |
instance enat :: complete_linorder .. |
27110 | 662 |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset
|
663 |
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
|
664 |
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
|
665 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60500
diff
changeset
|
666 |
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
|
667 |
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
|
668 |
|
60500 | 669 |
subsection \<open>Traditional theorem names\<close> |
27110 | 670 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45934
diff
changeset
|
671 |
lemmas enat_defs = zero_enat_def one_enat_def eSuc_def |
43919 | 672 |
plus_enat_def less_eq_enat_def less_enat_def |
27110 | 673 |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
674 |
end |