9 imports Main Countable Order_Continuity |
9 imports Main Countable Order_Continuity |
10 begin |
10 begin |
11 |
11 |
12 class infinity = |
12 class infinity = |
13 fixes infinity :: "'a" ("\<infinity>") |
13 fixes infinity :: "'a" ("\<infinity>") |
|
14 |
|
15 context |
|
16 fixes f :: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add, linorder_topology, complete_linorder}" |
|
17 begin |
|
18 |
|
19 lemma sums_SUP[simp, intro]: "f sums (SUP n. \<Sum>i<n. f i)" |
|
20 unfolding sums_def by (intro LIMSEQ_SUP monoI setsum_mono2 zero_le) auto |
|
21 |
|
22 lemma suminf_eq_SUP: "suminf f = (SUP n. \<Sum>i<n. f i)" |
|
23 using sums_SUP by (rule sums_unique[symmetric]) |
|
24 |
|
25 end |
14 |
26 |
15 subsection \<open>Type definition\<close> |
27 subsection \<open>Type definition\<close> |
16 |
28 |
17 text \<open> |
29 text \<open> |
18 We extend the standard natural numbers by a special value indicating |
30 We extend the standard natural numbers by a special value indicating |
69 where "the_enat (enat n) = n" |
81 where "the_enat (enat n) = n" |
70 |
82 |
71 |
83 |
72 subsection \<open>Constructors and numbers\<close> |
84 subsection \<open>Constructors and numbers\<close> |
73 |
85 |
74 instantiation enat :: "{zero, one}" |
86 instantiation enat :: zero_neq_one |
75 begin |
87 begin |
76 |
88 |
77 definition |
89 definition |
78 "0 = enat 0" |
90 "0 = enat 0" |
79 |
91 |
80 definition |
92 definition |
81 "1 = enat 1" |
93 "1 = enat 1" |
82 |
94 |
83 instance .. |
95 instance |
|
96 proof qed (simp add: zero_enat_def one_enat_def) |
84 |
97 |
85 end |
98 end |
86 |
99 |
87 definition eSuc :: "enat \<Rightarrow> enat" where |
100 definition eSuc :: "enat \<Rightarrow> enat" where |
88 "eSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)" |
101 "eSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)" |
106 by (simp add: zero_enat_def) |
119 by (simp add: zero_enat_def) |
107 |
120 |
108 lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)" |
121 lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)" |
109 by (simp add: zero_enat_def) |
122 by (simp add: zero_enat_def) |
110 |
123 |
111 lemma zero_one_enat_neq [simp]: |
124 lemma zero_one_enat_neq: |
112 "\<not> 0 = (1::enat)" |
125 "\<not> 0 = (1::enat)" |
113 "\<not> 1 = (0::enat)" |
126 "\<not> 1 = (0::enat)" |
114 unfolding zero_enat_def one_enat_def by simp_all |
127 unfolding zero_enat_def one_enat_def by simp_all |
115 |
128 |
116 lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1" |
129 lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1" |
181 by (simp_all add: eSuc_plus_1 ac_simps) |
194 by (simp_all add: eSuc_plus_1 ac_simps) |
182 |
195 |
183 lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)" |
196 lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)" |
184 by (simp only: add.commute[of m] iadd_Suc) |
197 by (simp only: add.commute[of m] iadd_Suc) |
185 |
198 |
186 lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)" |
|
187 by (cases m, cases n, simp_all add: zero_enat_def) |
|
188 |
|
189 subsection \<open>Multiplication\<close> |
199 subsection \<open>Multiplication\<close> |
190 |
200 |
191 instantiation enat :: comm_semiring_1 |
201 instantiation enat :: "{comm_semiring_1, semiring_no_zero_divisors}" |
192 begin |
202 begin |
193 |
203 |
194 definition times_enat_def [nitpick_simp]: |
204 definition times_enat_def [nitpick_simp]: |
195 "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | enat m \<Rightarrow> |
205 "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | enat m \<Rightarrow> |
196 (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | enat n \<Rightarrow> enat (m * n)))" |
206 (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | enat n \<Rightarrow> enat (m * n)))" |
207 proof |
217 proof |
208 fix a b c :: enat |
218 fix a b c :: enat |
209 show "(a * b) * c = a * (b * c)" |
219 show "(a * b) * c = a * (b * c)" |
210 unfolding times_enat_def zero_enat_def |
220 unfolding times_enat_def zero_enat_def |
211 by (simp split: enat.split) |
221 by (simp split: enat.split) |
212 show "a * b = b * a" |
222 show comm: "a * b = b * a" |
213 unfolding times_enat_def zero_enat_def |
223 unfolding times_enat_def zero_enat_def |
214 by (simp split: enat.split) |
224 by (simp split: enat.split) |
215 show "1 * a = a" |
225 show "1 * a = a" |
216 unfolding times_enat_def zero_enat_def one_enat_def |
226 unfolding times_enat_def zero_enat_def one_enat_def |
217 by (simp split: enat.split) |
227 by (simp split: enat.split) |
218 show "(a + b) * c = a * c + b * c" |
228 show distr: "(a + b) * c = a * c + b * c" |
219 unfolding times_enat_def zero_enat_def |
229 unfolding times_enat_def zero_enat_def |
220 by (simp split: enat.split add: distrib_right) |
230 by (simp split: enat.split add: distrib_right) |
221 show "0 * a = 0" |
231 show "0 * a = 0" |
222 unfolding times_enat_def zero_enat_def |
232 unfolding times_enat_def zero_enat_def |
223 by (simp split: enat.split) |
233 by (simp split: enat.split) |
224 show "a * 0 = 0" |
234 show "a * 0 = 0" |
225 unfolding times_enat_def zero_enat_def |
235 unfolding times_enat_def zero_enat_def |
226 by (simp split: enat.split) |
236 by (simp split: enat.split) |
227 show "(0::enat) \<noteq> 1" |
237 show "a * (b + c) = a * b + a * c" |
228 unfolding zero_enat_def one_enat_def |
238 by (cases a b c rule: enat3_cases) (auto simp: times_enat_def zero_enat_def distrib_left) |
229 by simp |
239 show "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" |
|
240 by (cases a b rule: enat2_cases) (auto simp: times_enat_def zero_enat_def) |
230 qed |
241 qed |
231 |
242 |
232 end |
243 end |
233 |
244 |
234 lemma mult_eSuc: "eSuc m * n = n + m * n" |
245 lemma mult_eSuc: "eSuc m * n = n + m * n" |
247 proof |
258 proof |
248 have "inj enat" by (rule injI) simp |
259 have "inj enat" by (rule injI) simp |
249 then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat) |
260 then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat) |
250 qed |
261 qed |
251 |
262 |
252 lemma imult_is_0 [simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)" |
|
253 by (auto simp add: times_enat_def zero_enat_def split: enat.split) |
|
254 |
|
255 lemma imult_is_infinity: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)" |
263 lemma imult_is_infinity: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)" |
256 by (auto simp add: times_enat_def zero_enat_def split: enat.split) |
264 by (auto simp add: times_enat_def zero_enat_def split: enat.split) |
257 |
|
258 |
265 |
259 subsection \<open>Numerals\<close> |
266 subsection \<open>Numerals\<close> |
260 |
267 |
261 lemma numeral_eq_enat: |
268 lemma numeral_eq_enat: |
262 "numeral k = enat (numeral k)" |
269 "numeral k = enat (numeral k)" |
366 proof |
373 proof |
367 fix a b :: enat show "(a \<le> b) = (\<exists>c. b = a + c)" |
374 fix a b :: enat show "(a \<le> b) = (\<exists>c. b = a + c)" |
368 by (cases a b rule: enat2_cases) (auto simp: le_iff_add enat_ex_split) |
375 by (cases a b rule: enat2_cases) (auto simp: le_iff_add enat_ex_split) |
369 qed |
376 qed |
370 |
377 |
371 instance enat :: "ordered_comm_semiring" |
378 instance enat :: "{linordered_nonzero_semiring, strict_ordered_comm_monoid_add}" |
372 proof |
379 proof |
373 fix a b c :: enat |
380 fix a b c :: enat |
374 assume "a \<le> b" and "0 \<le> c" thus "c * a \<le> c * b" |
381 show "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow>c * a \<le> c * b" |
375 unfolding times_enat_def less_eq_enat_def zero_enat_def |
382 unfolding times_enat_def less_eq_enat_def zero_enat_def |
376 by (simp split: enat.splits) |
383 by (simp split: enat.splits) |
377 qed |
384 show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" for a b c d :: enat |
|
385 by (cases a b c d rule: enat2_cases[case_product enat2_cases]) auto |
|
386 qed (simp add: zero_enat_def one_enat_def) |
378 |
387 |
379 (* BH: These equations are already proven generally for any type in |
388 (* BH: These equations are already proven generally for any type in |
380 class linordered_semidom. However, enat is not in that class because |
389 class linordered_semidom. However, enat is not in that class because |
381 it does not have the cancellation property. Would it be worthwhile to |
390 it does not have the cancellation property. Would it be worthwhile to |
382 a generalize linordered_semidom to a new class that includes enat? *) |
391 a generalize linordered_semidom to a new class that includes enat? *) |
384 lemma enat_ord_number [simp]: |
393 lemma enat_ord_number [simp]: |
385 "(numeral m :: enat) \<le> numeral n \<longleftrightarrow> (numeral m :: nat) \<le> numeral n" |
394 "(numeral m :: enat) \<le> numeral n \<longleftrightarrow> (numeral m :: nat) \<le> numeral n" |
386 "(numeral m :: enat) < numeral n \<longleftrightarrow> (numeral m :: nat) < numeral n" |
395 "(numeral m :: enat) < numeral n \<longleftrightarrow> (numeral m :: nat) < numeral n" |
387 by (simp_all add: numeral_eq_enat) |
396 by (simp_all add: numeral_eq_enat) |
388 |
397 |
389 lemma i0_lb [simp]: "(0::enat) \<le> n" |
|
390 by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) |
|
391 |
|
392 lemma ile0_eq [simp]: "n \<le> (0::enat) \<longleftrightarrow> n = 0" |
|
393 by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) |
|
394 |
|
395 lemma infinity_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R" |
398 lemma infinity_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R" |
396 by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) |
399 by (simp add: zero_enat_def less_eq_enat_def split: enat.splits) |
397 |
400 |
398 lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R" |
401 lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R" |
399 by simp |
402 by simp |
400 |
403 |
401 lemma not_iless0 [simp]: "\<not> n < (0::enat)" |
|
402 by (simp add: zero_enat_def less_enat_def split: enat.splits) |
|
403 |
|
404 lemma i0_less [simp]: "(0::enat) < n \<longleftrightarrow> n \<noteq> 0" |
|
405 by (simp add: zero_enat_def less_enat_def split: enat.splits) |
|
406 |
|
407 lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m" |
404 lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m" |
408 by (simp add: eSuc_def less_eq_enat_def split: enat.splits) |
405 by (simp add: eSuc_def less_eq_enat_def split: enat.splits) |
409 |
406 |
410 lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m" |
407 lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m" |
411 by (simp add: eSuc_def less_enat_def split: enat.splits) |
408 by (simp add: eSuc_def less_enat_def split: enat.splits) |
436 |
433 |
437 lemma imult_infinity_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>" |
434 lemma imult_infinity_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>" |
438 by (simp add: zero_enat_def less_enat_def split: enat.splits) |
435 by (simp add: zero_enat_def less_enat_def split: enat.splits) |
439 |
436 |
440 lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)" |
437 lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)" |
441 by (simp only: i0_less imult_is_0, simp) |
438 by (simp only: zero_less_iff_neq_zero mult_eq_0_iff, simp) |
442 |
439 |
443 lemma mono_eSuc: "mono eSuc" |
440 lemma mono_eSuc: "mono eSuc" |
444 by (simp add: mono_def) |
441 by (simp add: mono_def) |
445 |
|
446 |
442 |
447 lemma min_enat_simps [simp]: |
443 lemma min_enat_simps [simp]: |
448 "min (enat m) (enat n) = enat (min m n)" |
444 "min (enat m) (enat n) = enat (min m n)" |
449 "min q 0 = 0" |
445 "min q 0 = 0" |
450 "min 0 q = 0" |
446 "min 0 q = 0" |
468 |
464 |
469 lemma iadd_le_enat_iff: |
465 lemma iadd_le_enat_iff: |
470 "x + y \<le> enat n \<longleftrightarrow> (\<exists>y' x'. x = enat x' \<and> y = enat y' \<and> x' + y' \<le> n)" |
466 "x + y \<le> enat n \<longleftrightarrow> (\<exists>y' x'. x = enat x' \<and> y = enat y' \<and> x' + y' \<le> n)" |
471 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all |
467 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all |
472 |
468 |
473 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j" |
469 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j \<Longrightarrow> \<exists>j. enat k < Y j" |
474 apply (induct_tac k) |
470 apply (induct_tac k) |
475 apply (simp (no_asm) only: enat_0) |
471 apply (simp (no_asm) only: enat_0) |
476 apply (fast intro: le_less_trans [OF i0_lb]) |
472 apply (fast intro: le_less_trans [OF zero_le]) |
477 apply (erule exE) |
473 apply (erule exE) |
478 apply (drule spec) |
474 apply (drule spec) |
479 apply (erule exE) |
475 apply (erule exE) |
480 apply (drule ileI1) |
476 apply (drule ileI1) |
481 apply (rule eSuc_enat [THEN subst]) |
477 apply (rule eSuc_enat [THEN subst]) |
676 subsection \<open>Traditional theorem names\<close> |
672 subsection \<open>Traditional theorem names\<close> |
677 |
673 |
678 lemmas enat_defs = zero_enat_def one_enat_def eSuc_def |
674 lemmas enat_defs = zero_enat_def one_enat_def eSuc_def |
679 plus_enat_def less_eq_enat_def less_enat_def |
675 plus_enat_def less_eq_enat_def less_enat_def |
680 |
676 |
681 end |
677 lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)" |
|
678 by (rule add_eq_0_iff_both_eq_0) |
|
679 |
|
680 lemma i0_lb : "(0::enat) \<le> n" |
|
681 by (rule zero_le) |
|
682 |
|
683 lemma ile0_eq: "n \<le> (0::enat) \<longleftrightarrow> n = 0" |
|
684 by (rule le_zero_eq) |
|
685 |
|
686 lemma not_iless0: "\<not> n < (0::enat)" |
|
687 by (rule not_less_zero) |
|
688 |
|
689 lemma i0_less[simp]: "(0::enat) < n \<longleftrightarrow> n \<noteq> 0" |
|
690 by (rule zero_less_iff_neq_zero) |
|
691 |
|
692 lemma imult_is_0: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)" |
|
693 by (rule mult_eq_0_iff) |
|
694 |
|
695 end |