src/HOL/HOL.thy
changeset 13638 2b234b079245
parent 13598 8bc77b17f59f
child 13723 c7d104550205
     1.1 --- a/src/HOL/HOL.thy	Thu Oct 10 14:21:20 2002 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Oct 10 14:21:49 2002 +0200
     1.3 @@ -512,6 +512,24 @@
     1.4  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
     1.5  setup Splitter.setup setup Clasimp.setup
     1.6  
     1.7 +theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
     1.8 +  apply (rule iffI)
     1.9 +  apply (rule_tac a = "%x. THE y. P x y" in ex1I)
    1.10 +  apply (fast dest!: theI')
    1.11 +  apply (fast intro: ext the1_equality [symmetric])
    1.12 +  apply (erule ex1E)
    1.13 +  apply (rule allI)
    1.14 +  apply (rule ex1I)
    1.15 +  apply (erule spec)
    1.16 +  apply (rule ccontr)
    1.17 +  apply (erule_tac x = "%z. if z = x then y else f z" in allE)
    1.18 +  apply (erule impE)
    1.19 +  apply (rule allI)
    1.20 +  apply (rule_tac P = "xa = x" in case_split_thm)
    1.21 +  apply (drule_tac [3] x = x in fun_cong)
    1.22 +  apply simp_all
    1.23 +  done
    1.24 +
    1.25  text{*Needs only HOL-lemmas:*}
    1.26  lemma mk_left_commute:
    1.27    assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and