# HG changeset patch
# User nipkow
# Date 1234711539 -3600
# Node ID f270fe271a656bf995dd307ca8679356d53c63d8
# Parent  60a304bc5a07713f52bd2c01da7ced05c1c87926# Parent  24f56736c56f70b59007f31697f233cdebbe6270
merged

diff -r 60a304bc5a07 -r f270fe271a65 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Feb 15 14:02:27 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Feb 15 16:25:39 2009 +0100
@@ -93,6 +93,20 @@
   qed
 qed
 
+text{* A finite choice principle. Does not need the SOME choice operator. *}
+lemma finite_set_choice:
+  "finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)"
+proof (induct set: finite)
+  case empty thus ?case by simp
+next
+  case (insert a A)
+  then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto
+  show ?case (is "EX f. ?P f")
+  proof
+    show "?P(%x. if x = a then b else f x)" using f ab by auto
+  qed
+qed
+
 
 text{* Finite sets are the images of initial segments of natural numbers: *}