equal
deleted
inserted
replaced
24 lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)" |
24 lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)" |
25 apply (rule AC_Pi) |
25 apply (rule AC_Pi) |
26 apply (erule bspec, assumption) |
26 apply (erule bspec, assumption) |
27 done |
27 done |
28 |
28 |
29 lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C)-{0}. X)" |
29 lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> Pow(C)-{0}. X)" |
30 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) |
30 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) |
31 apply (erule_tac [2] exI, blast) |
31 apply (erule_tac [2] exI, blast) |
32 done |
32 done |
33 |
33 |
34 lemma AC_func: |
34 lemma AC_func: |
50 apply (rule_tac [2] bexI) |
50 apply (rule_tac [2] bexI) |
51 prefer 2 apply assumption |
51 prefer 2 apply assumption |
52 apply (erule_tac [2] fun_weaken_type, blast+) |
52 apply (erule_tac [2] fun_weaken_type, blast+) |
53 done |
53 done |
54 |
54 |
55 lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)" |
55 lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> A. x)" |
56 apply (rule AC_Pi) |
56 apply (rule AC_Pi) |
57 apply (simp_all add: non_empty_family) |
57 apply (simp_all add: non_empty_family) |
58 done |
58 done |
59 |
59 |
60 end |
60 end |