# HG changeset patch
# User berghofe
# Date 1034252509 -7200
# Node ID 2b234b07924599256ca346d87f1507c6acd5ec45
# Parent  02aa63636ab802e64c72ffb872637393f9da42e5
Added choice_eq.

diff -r 02aa63636ab8 -r 2b234b079245 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Thu Oct 10 14:21:20 2002 +0200
+++ b/src/HOL/HOL.ML	Thu Oct 10 14:21:49 2002 +0200
@@ -53,6 +53,7 @@
 val order_antisym = thm "order_antisym";
 val order_less_le = thm "order_less_le";
 val linorder_linear = thm "linorder_linear";
+val choice_eq = thm "choice_eq";
 
 structure HOL =
 struct
diff -r 02aa63636ab8 -r 2b234b079245 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Oct 10 14:21:20 2002 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 10 14:21:49 2002 +0200
@@ -512,6 +512,24 @@
 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
 setup Splitter.setup setup Clasimp.setup
 
+theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
+  apply (rule iffI)
+  apply (rule_tac a = "%x. THE y. P x y" in ex1I)
+  apply (fast dest!: theI')
+  apply (fast intro: ext the1_equality [symmetric])
+  apply (erule ex1E)
+  apply (rule allI)
+  apply (rule ex1I)
+  apply (erule spec)
+  apply (rule ccontr)
+  apply (erule_tac x = "%z. if z = x then y else f z" in allE)
+  apply (erule impE)
+  apply (rule allI)
+  apply (rule_tac P = "xa = x" in case_split_thm)
+  apply (drule_tac [3] x = x in fun_cong)
+  apply simp_all
+  done
+
 text{*Needs only HOL-lemmas:*}
 lemma mk_left_commute:
   assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and