# HG changeset patch
# User nipkow
# Date 1234711516 -3600
# Node ID 24f56736c56f70b59007f31697f233cdebbe6270
# Parent  3d50e96bcd6b254981674c5671eac47224052b93
added finite_set_choice

diff -r 3d50e96bcd6b -r 24f56736c56f src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Feb 15 11:34:46 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Feb 15 16:25:16 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: *}