22 from an infinite set, the result is still infinite. |
22 from an infinite set, the result is still infinite. |
23 *} |
23 *} |
24 |
24 |
25 lemma infinite_nonempty: |
25 lemma infinite_nonempty: |
26 "\<not> (infinite {})" |
26 "\<not> (infinite {})" |
27 by simp |
27 by simp |
28 |
28 |
29 lemma infinite_remove: |
29 lemma infinite_remove: |
30 "infinite S \<Longrightarrow> infinite (S - {a})" |
30 "infinite S \<Longrightarrow> infinite (S - {a})" |
31 by simp |
31 by simp |
32 |
32 |
33 lemma Diff_infinite_finite: |
33 lemma Diff_infinite_finite: |
34 assumes T: "finite T" and S: "infinite S" |
34 assumes T: "finite T" and S: "infinite S" |
35 shows "infinite (S-T)" |
35 shows "infinite (S-T)" |
36 using T |
36 using T |
37 proof (induct) |
37 proof induct |
38 from S |
38 from S |
39 show "infinite (S - {})" by auto |
39 show "infinite (S - {})" by auto |
40 next |
40 next |
41 fix T x |
41 fix T x |
42 assume ih: "infinite (S-T)" |
42 assume ih: "infinite (S-T)" |
47 by (simp add: infinite_remove) |
47 by (simp add: infinite_remove) |
48 qed |
48 qed |
49 |
49 |
50 lemma Un_infinite: |
50 lemma Un_infinite: |
51 "infinite S \<Longrightarrow> infinite (S \<union> T)" |
51 "infinite S \<Longrightarrow> infinite (S \<union> T)" |
52 by simp |
52 by simp |
53 |
53 |
54 lemma infinite_super: |
54 lemma infinite_super: |
55 assumes T: "S \<subseteq> T" and S: "infinite S" |
55 assumes T: "S \<subseteq> T" and S: "infinite S" |
56 shows "infinite T" |
56 shows "infinite T" |
57 proof (rule ccontr) |
57 proof (rule ccontr) |
58 assume "\<not>(infinite T)" |
58 assume "\<not>(infinite T)" |
59 with T |
59 with T have "finite S" by (simp add: finite_subset) |
60 have "finite S" by (simp add: finite_subset) |
60 with S show False by simp |
61 with S |
|
62 show False by simp |
|
63 qed |
61 qed |
64 |
62 |
65 text {* |
63 text {* |
66 As a concrete example, we prove that the set of natural |
64 As a concrete example, we prove that the set of natural |
67 numbers is infinite. |
65 numbers is infinite. |
354 |
352 |
355 defs |
353 defs |
356 INF_def: "Inf_many P \<equiv> infinite {x. P x}" |
354 INF_def: "Inf_many P \<equiv> infinite {x. P x}" |
357 MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)" |
355 MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)" |
358 |
356 |
359 syntax (xsymbols) |
357 abbreviation (xsymbols) |
360 "MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10) |
358 Inf_many1 (binder "\<exists>\<^sub>\<infinity>" 10) |
361 "INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10) |
359 "Inf_many1 == Inf_many" |
362 |
360 Alm_all1 (binder "\<forall>\<^sub>\<infinity>" 10) |
363 syntax (HTML output) |
361 "Alm_all1 == Alm_all" |
364 "MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10) |
362 |
365 "INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10) |
363 abbreviation (HTML output) |
|
364 Inf_many2 (binder "\<exists>\<^sub>\<infinity>" 10) |
|
365 "Inf_many2 == Inf_many" |
|
366 Alm_all2 (binder "\<forall>\<^sub>\<infinity>" 10) |
|
367 "Alm_all2 == Alm_all" |
366 |
368 |
367 lemma INF_EX: |
369 lemma INF_EX: |
368 "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" |
370 "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" |
369 proof (unfold INF_def, rule ccontr) |
371 proof (unfold INF_def, rule ccontr) |
370 assume inf: "infinite {x. P x}" |
372 assume inf: "infinite {x. P x}" |
419 constdefs |
421 constdefs |
420 atmost_one :: "'a set \<Rightarrow> bool" |
422 atmost_one :: "'a set \<Rightarrow> bool" |
421 "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y" |
423 "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y" |
422 |
424 |
423 lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S" |
425 lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S" |
424 by (simp add: atmost_one_def) |
426 by (simp add: atmost_one_def) |
425 |
427 |
426 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S" |
428 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S" |
427 by (simp add: atmost_one_def) |
429 by (simp add: atmost_one_def) |
428 |
430 |
429 lemma atmost_one_unique [elim]: "\<lbrakk> atmost_one S; x \<in> S; y \<in> S \<rbrakk> \<Longrightarrow> y=x" |
431 lemma atmost_one_unique [elim]: "\<lbrakk> atmost_one S; x \<in> S; y \<in> S \<rbrakk> \<Longrightarrow> y=x" |
430 by (simp add: atmost_one_def) |
432 by (simp add: atmost_one_def) |
431 |
433 |
432 end |
434 end |