equal
deleted
inserted
replaced
59 proof |
59 proof |
60 assume "finite T" |
60 assume "finite T" |
61 with T have "finite S" by (simp add: finite_subset) |
61 with T have "finite S" by (simp add: finite_subset) |
62 with S show False by simp |
62 with S show False by simp |
63 qed |
63 qed |
|
64 |
|
65 lemma infinite_coinduct [consumes 1, case_names infinite]: |
|
66 assumes "X A" |
|
67 and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})" |
|
68 shows "infinite A" |
|
69 proof |
|
70 assume "finite A" |
|
71 then show False using \<open>X A\<close> |
|
72 by(induction rule: finite_psubset_induct)(meson Diff_subset card_Diff1_less card_psubset finite_Diff step) |
|
73 qed |
64 |
74 |
65 text \<open> |
75 text \<open> |
66 As a concrete example, we prove that the set of natural numbers is |
76 As a concrete example, we prove that the set of natural numbers is |
67 infinite. |
77 infinite. |
68 \<close> |
78 \<close> |