(* Title: ZF/AC/AC15_WO6.thy ID: $Id: AC15_WO6.thy,v 1.11 2005/06/17 14:15:10 haftmann Exp $ Author: Krzysztof Grabczewski The proofs needed to state that AC10, ..., AC15 are equivalent to the rest. We need the following: WO1 ==> AC10(n) ==> AC11 ==> AC12 ==> AC15 ==> WO6 In order to add the formulations AC13 and AC14 we need: AC10(succ(n)) ==> AC13(n) ==> AC14 ==> AC15 or AC1 ==> AC13(1); AC13(m) ==> AC13(n) ==> AC14 ==> AC15 (m≤n) So we don't have to prove all implications of both cases. Moreover we don't need to prove AC13(1) ==> AC1 and AC11 ==> AC14 as Rubin & Rubin do. *) theory AC15_WO6 imports HH Cardinal_aux begin (* ********************************************************************** *) (* Lemmas used in the proofs in which the conclusion is AC13, AC14 *) (* or AC15 *) (* - cons_times_nat_not_Finite *) (* - ex_fun_AC13_AC15 *) (* ********************************************************************** *) lemma lepoll_Sigma: "A≠0 ==> B \<lesssim> A*B" apply (unfold lepoll_def) apply (erule not_emptyE) apply (rule_tac x = "λz ∈ B. <x,z>" in exI) apply (fast intro!: snd_conv lam_injective) done lemma cons_times_nat_not_Finite: "0∉A ==> ∀B ∈ {cons(0,x*nat). x ∈ A}. ~Finite(B)" apply clarify apply (rule nat_not_Finite [THEN notE] ) apply (subgoal_tac "x ~= 0") apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+ done lemma lemma1: "[| Union(C)=A; a ∈ A |] ==> ∃B ∈ C. a ∈ B & B ⊆ A" by fast lemma lemma2: "[| pairwise_disjoint(A); B ∈ A; C ∈ A; a ∈ B; a ∈ C |] ==> B=C" by (unfold pairwise_disjoint_def, blast) lemma lemma3: "∀B ∈ {cons(0, x*nat). x ∈ A}. pairwise_disjoint(f`B) & sets_of_size_between(f`B, 2, n) & Union(f`B)=B ==> ∀B ∈ A. ∃! u. u ∈ f`cons(0, B*nat) & u ⊆ cons(0, B*nat) & 0 ∈ u & 2 \<lesssim> u & u \<lesssim> n" apply (unfold sets_of_size_between_def) apply (rule ballI) apply (erule_tac x="cons(0, B*nat)" in ballE) apply (blast dest: lemma1 intro!: lemma2, blast) done lemma lemma4: "[| A \<lesssim> i; Ord(i) |] ==> {P(a). a ∈ A} \<lesssim> i" apply (unfold lepoll_def) apply (erule exE) apply (rule_tac x = "λx ∈ RepFun(A,P). LEAST j. ∃a∈A. x=P(a) & f`a=j" in exI) apply (rule_tac d = "%y. P (converse (f) `y) " in lam_injective) apply (erule RepFunE) apply (frule inj_is_fun [THEN apply_type], assumption) apply (fast intro: LeastI2 elim!: Ord_in_Ord inj_is_fun [THEN apply_type]) apply (erule RepFunE) apply (rule LeastI2) apply fast apply (fast elim!: Ord_in_Ord inj_is_fun [THEN apply_type]) apply (fast elim: sym left_inverse [THEN ssubst]) done lemma lemma5_1: "[| B ∈ A; 2 \<lesssim> u(B) |] ==> (λx ∈ A. {fst(x). x ∈ u(x)-{0}})`B ≠ 0" apply simp apply (fast dest: lepoll_Diff_sing elim: lepoll_trans [THEN succ_lepoll_natE] ssubst intro!: lepoll_refl) done lemma lemma5_2: "[| B ∈ A; u(B) ⊆ cons(0, B*nat) |] ==> (λx ∈ A. {fst(x). x ∈ u(x)-{0}})`B ⊆ B" apply auto done lemma lemma5_3: "[| n ∈ nat; B ∈ A; 0 ∈ u(B); u(B) \<lesssim> succ(n) |] ==> (λx ∈ A. {fst(x). x ∈ u(x)-{0}})`B \<lesssim> n" apply simp apply (fast elim!: Diff_lepoll [THEN lemma4 [OF _ nat_into_Ord]]) done lemma ex_fun_AC13_AC15: "[| ∀B ∈ {cons(0, x*nat). x ∈ A}. pairwise_disjoint(f`B) & sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B; n ∈ nat |] ==> ∃f. ∀B ∈ A. f`B ≠ 0 & f`B ⊆ B & f`B \<lesssim> n" by (fast del: subsetI notI dest!: lemma3 theI intro!: lemma5_1 lemma5_2 lemma5_3) (* ********************************************************************** *) (* The target proofs *) (* ********************************************************************** *) (* ********************************************************************** *) (* AC10(n) ==> AC11 *) (* ********************************************************************** *) theorem AC10_AC11: "[| n ∈ nat; 1≤n; AC10(n) |] ==> AC11" by (unfold AC10_def AC11_def, blast) (* ********************************************************************** *) (* AC11 ==> AC12 *) (* ********************************************************************** *) theorem AC11_AC12: "AC11 ==> AC12" by (unfold AC10_def AC11_def AC11_def AC12_def, blast) (* ********************************************************************** *) (* AC12 ==> AC15 *) (* ********************************************************************** *) theorem AC12_AC15: "AC12 ==> AC15" apply (unfold AC12_def AC15_def) apply (blast del: ballI intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15) done (* ********************************************************************** *) (* AC15 ==> WO6 *) (* ********************************************************************** *) lemma OUN_eq_UN: "Ord(x) ==> (\<Union>a<x. F(a)) = (\<Union>a ∈ x. F(a))" by (fast intro!: ltI dest!: ltD) lemma AC15_WO6_aux1: "∀x ∈ Pow(A)-{0}. f`x≠0 & f`x ⊆ x & f`x \<lesssim> m ==> (\<Union>i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A" apply (simp add: Ord_Least [THEN OUN_eq_UN]) apply (rule equalityI) apply (fast dest!: less_Least_subset_x) apply (blast del: subsetI intro!: f_subsets_imp_UN_HH_eq_x [THEN Diff_eq_0_iff [THEN iffD1]]) done lemma AC15_WO6_aux2: "∀x ∈ Pow(A)-{0}. f`x≠0 & f`x ⊆ x & f`x \<lesssim> m ==> ∀x < (LEAST x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m" apply (rule oallI) apply (drule ltD [THEN less_Least_subset_x]) apply (frule HH_subset_imp_eq) apply (erule ssubst) apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2]) (*but can't use del: DiffE despite the obvious conflict*) done theorem AC15_WO6: "AC15 ==> WO6" apply (unfold AC15_def WO6_def) apply (rule allI) apply (erule_tac x = "Pow (A) -{0}" in allE) apply (erule impE, fast) apply (elim bexE conjE exE) apply (rule bexI) apply (rule conjI, assumption) apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI) apply (rule_tac x = "λj ∈ (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI) apply (simp_all add: ltD) apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun] elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2) done (* ********************************************************************** *) (* The proof needed in the first case, not in the second *) (* ********************************************************************** *) (* ********************************************************************** *) (* AC10(n) ==> AC13(n-1) if 2≤n *) (* *) (* Because of the change to the formal definition of AC10(n) we prove *) (* the following obviously equivalent theorem ∈ *) (* AC10(n) implies AC13(n) for (1≤n) *) (* ********************************************************************** *) theorem AC10_AC13: "[| n ∈ nat; 1≤n; AC10(n) |] ==> AC13(n)" apply (unfold AC10_def AC13_def, safe) apply (erule allE) apply (erule impE [OF _ cons_times_nat_not_Finite], assumption) apply (fast elim!: impE [OF _ cons_times_nat_not_Finite] dest!: ex_fun_AC13_AC15) done (* ********************************************************************** *) (* The proofs needed in the second case, not in the first *) (* ********************************************************************** *) (* ********************************************************************** *) (* AC1 ==> AC13(1) *) (* ********************************************************************** *) lemma AC1_AC13: "AC1 ==> AC13(1)" apply (unfold AC1_def AC13_def) apply (rule allI) apply (erule allE) apply (rule impI) apply (drule mp, assumption) apply (elim exE) apply (rule_tac x = "λx ∈ A. {f`x}" in exI) apply (simp add: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll]) done (* ********************************************************************** *) (* AC13(m) ==> AC13(n) for m ⊆ n *) (* ********************************************************************** *) lemma AC13_mono: "[| m≤n; AC13(m) |] ==> AC13(n)" apply (unfold AC13_def) apply (drule le_imp_lepoll) apply (fast elim!: lepoll_trans) done (* ********************************************************************** *) (* The proofs necessary for both cases *) (* ********************************************************************** *) (* ********************************************************************** *) (* AC13(n) ==> AC14 if 1 ⊆ n *) (* ********************************************************************** *) theorem AC13_AC14: "[| n ∈ nat; 1≤n; AC13(n) |] ==> AC14" by (unfold AC13_def AC14_def, auto) (* ********************************************************************** *) (* AC14 ==> AC15 *) (* ********************************************************************** *) theorem AC14_AC15: "AC14 ==> AC15" by (unfold AC13_def AC14_def AC15_def, fast) (* ********************************************************************** *) (* The redundant proofs; however cited by Rubin & Rubin *) (* ********************************************************************** *) (* ********************************************************************** *) (* AC13(1) ==> AC1 *) (* ********************************************************************** *) lemma lemma_aux: "[| A≠0; A \<lesssim> 1 |] ==> ∃a. A={a}" by (fast elim!: not_emptyE lepoll_1_is_sing) lemma AC13_AC1_lemma: "∀B ∈ A. f(B)≠0 & f(B)<=B & f(B) \<lesssim> 1 ==> (λx ∈ A. THE y. f(x)={y}) ∈ (Π X ∈ A. X)" apply (rule lam_type) apply (drule bspec, assumption) apply (elim conjE) apply (erule lemma_aux [THEN exE], assumption) apply (simp add: the_equality) done theorem AC13_AC1: "AC13(1) ==> AC1" apply (unfold AC13_def AC1_def) apply (fast elim!: AC13_AC1_lemma) done (* ********************************************************************** *) (* AC11 ==> AC14 *) (* ********************************************************************** *) theorem AC11_AC14: "AC11 ==> AC14" apply (unfold AC11_def AC14_def) apply (fast intro!: AC10_AC13) done end
lemma lepoll_Sigma:
A ≠ 0 ==> B lepoll A × B
lemma cons_times_nat_not_Finite:
0 ∉ A ==> ∀B∈{cons(0, x × nat) . x ∈ A}. ¬ Finite(B)
lemma lemma1:
[| \<Union>C = A; a ∈ A |] ==> ∃B∈C. a ∈ B ∧ B ⊆ A
lemma lemma2:
[| pairwise_disjoint(A); B ∈ A; C ∈ A; a ∈ B; a ∈ C |] ==> B = C
lemma lemma3:
∀B∈{cons(0, x × nat) . x ∈ A}. pairwise_disjoint(f ` B) ∧ sets_of_size_between(f ` B, 2, n) ∧ \<Union>f ` B = B ==> ∀B∈A. ∃!u. u ∈ f ` cons(0, B × nat) ∧ u ⊆ cons(0, B × nat) ∧ 0 ∈ u ∧ 2 lepoll u ∧ u lepoll n
lemma lemma4:
[| A lepoll i; Ord(i) |] ==> {P(a) . a ∈ A} lepoll i
lemma lemma5_1:
[| B ∈ A; 2 lepoll u(B) |] ==> (λx∈A. {fst(x) . x ∈ u(x) - {0}}) ` B ≠ 0
lemma lemma5_2:
[| B ∈ A; u(B) ⊆ cons(0, B × nat) |] ==> (λx∈A. {fst(x) . x ∈ u(x) - {0}}) ` B ⊆ B
lemma lemma5_3:
[| n ∈ nat; B ∈ A; 0 ∈ u(B); u(B) lepoll succ(n) |] ==> (λx∈A. {fst(x) . x ∈ u(x) - {0}}) ` B lepoll n
lemma ex_fun_AC13_AC15:
[| ∀B∈{cons(0, x × nat) . x ∈ A}. pairwise_disjoint(f ` B) ∧ sets_of_size_between(f ` B, 2, succ(n)) ∧ \<Union>f ` B = B; n ∈ nat |] ==> ∃f. ∀B∈A. f ` B ≠ 0 ∧ f ` B ⊆ B ∧ f ` B lepoll n
theorem AC10_AC11:
[| n ∈ nat; 1 ≤ n; AC10(n) |] ==> AC11
theorem AC11_AC12:
AC11 ==> AC12
theorem AC12_AC15:
AC12 ==> AC15
lemma OUN_eq_UN:
Ord(x) ==> (\<Union>a<x. F(a)) = (\<Union>a∈x. F(a))
lemma AC15_WO6_aux1:
∀x∈Pow(A) - {0}. f ` x ≠ 0 ∧ f ` x ⊆ x ∧ f ` x lepoll m ==> (\<Union>i<μx. HH(f, A, x) = {A}. HH(f, A, i)) = A
lemma AC15_WO6_aux2:
∀x∈Pow(A) - {0}. f ` x ≠ 0 ∧ f ` x ⊆ x ∧ f ` x lepoll m ==> ∀x<μx. HH(f, A, x) = {A}. HH(f, A, x) lepoll m
theorem AC15_WO6:
AC15 ==> WO6
theorem AC10_AC13:
[| n ∈ nat; 1 ≤ n; AC10(n) |] ==> AC13(n)
lemma AC1_AC13:
AC1 ==> AC13(1)
lemma AC13_mono:
[| m ≤ n; AC13(m) |] ==> AC13(n)
theorem AC13_AC14:
[| n ∈ nat; 1 ≤ n; AC13(n) |] ==> AC14
theorem AC14_AC15:
AC14 ==> AC15
lemma lemma_aux:
[| A ≠ 0; A lepoll 1 |] ==> ∃a. A = {a}
lemma AC13_AC1_lemma:
∀B∈A. f(B) ≠ 0 ∧ f(B) ⊆ B ∧ f(B) lepoll 1 ==> (λx∈A. THE y. f(x) = {y}) ∈ (ΠX∈A. X)
theorem AC13_AC1:
AC13(1) ==> AC1
theorem AC11_AC14:
AC11 ==> AC14