equal
deleted
inserted
replaced
88 from i have "F \<subseteq> A" by blast |
88 from i have "F \<subseteq> A" by blast |
89 with P show "P F" . |
89 with P show "P F" . |
90 show "finite F" by fact |
90 show "finite F" by fact |
91 show "x \<notin> F" by fact |
91 show "x \<notin> F" by fact |
92 qed |
92 qed |
|
93 qed |
|
94 qed |
|
95 |
|
96 text{* A finite choice principle. Does not need the SOME choice operator. *} |
|
97 lemma finite_set_choice: |
|
98 "finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)" |
|
99 proof (induct set: finite) |
|
100 case empty thus ?case by simp |
|
101 next |
|
102 case (insert a A) |
|
103 then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto |
|
104 show ?case (is "EX f. ?P f") |
|
105 proof |
|
106 show "?P(%x. if x = a then b else f x)" using f ab by auto |
93 qed |
107 qed |
94 qed |
108 qed |
95 |
109 |
96 |
110 |
97 text{* Finite sets are the images of initial segments of natural numbers: *} |
111 text{* Finite sets are the images of initial segments of natural numbers: *} |