Theory AC16_lemmas

(*  Title:      ZF/AC/AC16_lemmas.thy
    Author:     Krzysztof Grabczewski

Lemmas used in the proofs concerning AC16
*)

theory AC16_lemmas
imports AC_Equiv Hartog Cardinal_aux
begin

lemma cons_Diff_eq: "a∉A ⟹ cons(a,A)-{a}=A"
by fast

lemma nat_1_lepoll_iff: "1≲X ⟷ (∃x. x ∈ X)"
  unfolding lepoll_def
apply (rule iffI)
apply (fast intro: inj_is_fun [THEN apply_type])
apply (erule exE)
apply (rule_tac x = "λa ∈ 1. x" in exI)
apply (fast intro!: lam_injective)
done

lemma eqpoll_1_iff_singleton: "X≈1 ⟷ (∃x. X={x})"
apply (rule iffI)
apply (erule eqpollE)
apply (drule nat_1_lepoll_iff [THEN iffD1])
apply (fast intro!: lepoll_1_is_sing)
apply (fast intro!: singleton_eqpoll_1)
done

lemma cons_eqpoll_succ: "⟦x≈n; y∉x⟧ ⟹ cons(y,x)≈succ(n)"
  unfolding succ_def
apply (fast elim!: cons_eqpoll_cong mem_irrefl)
done

lemma subsets_eqpoll_1_eq: "{Y ∈ Pow(X). Y≈1} = {{x}. x ∈ X}"
apply (rule equalityI)
apply (rule subsetI)
apply (erule CollectE)
apply (drule eqpoll_1_iff_singleton [THEN iffD1])
apply (fast intro!: RepFunI)
apply (rule subsetI)
apply (erule RepFunE)
apply (rule CollectI, fast)
apply (fast intro!: singleton_eqpoll_1)
done

lemma eqpoll_RepFun_sing: "X≈{{x}. x ∈ X}"
  unfolding eqpoll_def bij_def
apply (rule_tac x = "λx ∈ X. {x}" in exI)
apply (rule IntI)
apply (unfold inj_def surj_def, simp)
apply (fast intro!: lam_type RepFunI intro: singleton_eq_iff [THEN iffD1], simp)
apply (fast intro!: lam_type)
done

lemma subsets_eqpoll_1_eqpoll: "{Y ∈ Pow(X). Y≈1}≈X"
apply (rule subsets_eqpoll_1_eq [THEN ssubst])
apply (rule eqpoll_RepFun_sing [THEN eqpoll_sym])
done

lemma InfCard_Least_in:
     "⟦InfCard(x); y ⊆ x; y ≈ succ(z)⟧ ⟹ (μ i. i ∈ y) ∈ y"
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, 
                         THEN succ_lepoll_imp_not_empty, THEN not_emptyE])
apply (fast intro: LeastI 
            dest!: InfCard_is_Card [THEN Card_is_Ord] 
            elim: Ord_in_Ord)
done

lemma subsets_lepoll_lemma1:
     "⟦InfCard(x); n ∈ nat⟧ 
      ⟹ {y ∈ Pow(x). y≈succ(succ(n))} ≲ x*{y ∈ Pow(x). y≈succ(n)}"
  unfolding lepoll_def
apply (rule_tac x = "λy ∈ {y ∈ Pow(x) . y≈succ (succ (n))}. 
                      <μ i. i ∈ y, y-{μ i. i ∈ y}>" in exI)
apply (rule_tac d = "λz. cons (fst(z), snd(z))" in lam_injective)
 apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in)
apply (simp, blast intro: InfCard_Least_in)
done

lemma set_of_Ord_succ_Union: "(∀y ∈ z. Ord(y)) ⟹ z ⊆ succ(⋃(z))"
apply (rule subsetI)
apply (case_tac "∀y ∈ z. y ⊆ x", blast )
apply (simp, erule bexE) 
apply (rule_tac i=y and j=x in Ord_linear_le)
apply (blast dest: le_imp_subset elim: leE ltE)+
done

lemma subset_not_mem: "j ⊆ i ⟹ i ∉ j"
by (fast elim!: mem_irrefl)

lemma succ_Union_not_mem:
     "(⋀y. y ∈ z ⟹ Ord(y)) ⟹ succ(⋃(z)) ∉ z"
apply (rule set_of_Ord_succ_Union [THEN subset_not_mem], blast)
done

lemma Union_cons_eq_succ_Union:
     "⋃(cons(succ(⋃(z)),z)) = succ(⋃(z))"
by fast

lemma Un_Ord_disj: "⟦Ord(i); Ord(j)⟧ ⟹ i ∪ j = i | i ∪ j = j"
by (fast dest!: le_imp_subset elim: Ord_linear_le)

lemma Union_eq_Un: "x ∈ X ⟹ ⋃(X) = x ∪ ⋃(X-{x})"
by fast

lemma Union_in_lemma [rule_format]:
     "n ∈ nat ⟹ ∀z. (∀y ∈ z. Ord(y)) ∧ z≈n ∧ z≠0 ⟶ ⋃(z) ∈ z"
apply (induct_tac "n")
apply (fast dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
apply (intro allI impI)
apply (erule natE)
apply (fast dest!: eqpoll_1_iff_singleton [THEN iffD1]
            intro!: Union_singleton, clarify) 
apply (elim not_emptyE)
apply (erule_tac x = "z-{xb}" in allE)
apply (erule impE)
apply (fast elim!: Diff_sing_eqpoll
                   Diff_sing_eqpoll [THEN eqpoll_succ_imp_not_empty])
apply (subgoal_tac "xb ∪ ⋃(z - {xb}) ∈ z")
apply (simp add: Union_eq_Un [symmetric])
apply (frule bspec, assumption)
apply (drule bspec) 
apply (erule Diff_subset [THEN subsetD])
apply (drule Un_Ord_disj, assumption, auto) 
done

lemma Union_in: "⟦∀x ∈ z. Ord(x); z≈n; z≠0; n ∈ nat⟧ ⟹ ⋃(z) ∈ z"
by (blast intro: Union_in_lemma)

lemma succ_Union_in_x:
     "⟦InfCard(x); z ∈ Pow(x); z≈n; n ∈ nat⟧ ⟹ succ(⋃(z)) ∈ x"
apply (rule Limit_has_succ [THEN ltE])
prefer 3 apply assumption
apply (erule InfCard_is_Limit)
apply (case_tac "z=0")
apply (simp, fast intro!: InfCard_is_Limit [THEN Limit_has_0])
apply (rule ltI [OF PowD [THEN subsetD] InfCard_is_Card [THEN Card_is_Ord]], assumption)
apply (blast intro: Union_in
                    InfCard_is_Card [THEN Card_is_Ord, THEN Ord_in_Ord])+
done

lemma succ_lepoll_succ_succ:
     "⟦InfCard(x); n ∈ nat⟧ 
      ⟹ {y ∈ Pow(x). y≈succ(n)} ≲ {y ∈ Pow(x). y≈succ(succ(n))}"
  unfolding lepoll_def
apply (rule_tac x = "λz ∈ {y∈Pow(x). y≈succ(n)}. cons(succ(⋃(z)), z)" 
       in exI)
apply (rule_tac d = "λz. z-{⋃(z) }" in lam_injective)
apply (blast intro!: succ_Union_in_x succ_Union_not_mem
             intro: cons_eqpoll_succ Ord_in_Ord
             dest!: InfCard_is_Card [THEN Card_is_Ord])
apply (simp only: Union_cons_eq_succ_Union) 
apply (rule cons_Diff_eq)
apply (fast dest!: InfCard_is_Card [THEN Card_is_Ord]
            elim: Ord_in_Ord 
            intro!: succ_Union_not_mem)
done

lemma subsets_eqpoll_X:
     "⟦InfCard(X); n ∈ nat⟧ ⟹ {Y ∈ Pow(X). Y≈succ(n)} ≈ X"
apply (induct_tac "n")
apply (rule subsets_eqpoll_1_eqpoll)
apply (rule eqpollI)
apply (rule subsets_lepoll_lemma1 [THEN lepoll_trans], assumption+)
apply (rule eqpoll_trans [THEN eqpoll_imp_lepoll]) 
 apply (erule eqpoll_refl [THEN prod_eqpoll_cong])
apply (erule InfCard_square_eqpoll)
apply (fast elim: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 
            intro!: succ_lepoll_succ_succ)
done

lemma image_vimage_eq:
     "⟦f ∈ surj(A,B); y ⊆ B⟧ ⟹ f``(converse(f)``y) = y"
  unfolding surj_def
apply (fast dest: apply_equality2 elim: apply_iff [THEN iffD2])
done

lemma vimage_image_eq: "⟦f ∈ inj(A,B); y ⊆ A⟧ ⟹ converse(f)``(f``y) = y"
by (fast elim!: inj_is_fun [THEN apply_Pair] dest: inj_equality)

lemma subsets_eqpoll:
     "A≈B ⟹ {Y ∈ Pow(A). Y≈n}≈{Y ∈ Pow(B). Y≈n}"
  unfolding eqpoll_def
apply (erule exE)
apply (rule_tac x = "λX ∈ {Y ∈ Pow (A) . ∃f. f ∈ bij (Y, n) }. f``X" in exI)
apply (rule_tac d = "λZ. converse (f) ``Z" in lam_bijective)
apply (fast intro!: bij_is_inj [THEN restrict_bij, THEN bij_converse_bij, 
                                THEN comp_bij] 
            elim!: bij_is_fun [THEN fun_is_rel, THEN image_subset])
apply (blast intro!:  bij_is_inj [THEN restrict_bij] 
                      comp_bij bij_converse_bij
                      bij_is_fun [THEN fun_is_rel, THEN image_subset])
apply (fast elim!: bij_is_inj [THEN vimage_image_eq])
apply (fast elim!: bij_is_surj [THEN image_vimage_eq])
done

lemma WO2_imp_ex_Card: "WO2 ⟹ ∃a. Card(a) ∧ X≈a"
  unfolding WO2_def
apply (drule spec [of _ X])
apply (blast intro: Card_cardinal eqpoll_trans
          well_ord_Memrel [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym])
done

lemma lepoll_infinite: "⟦X≲Y; ¬Finite(X)⟧ ⟹ ¬Finite(Y)"
by (blast intro: lepoll_Finite)

lemma infinite_Card_is_InfCard: "⟦¬Finite(X); Card(X)⟧ ⟹ InfCard(X)"
  unfolding InfCard_def
apply (fast elim!: Card_is_Ord [THEN nat_le_infinite_Ord])
done

lemma WO2_infinite_subsets_eqpoll_X: "⟦WO2; n ∈ nat; ¬Finite(X)⟧   
        ⟹ {Y ∈ Pow(X). Y≈succ(n)}≈X"
apply (drule WO2_imp_ex_Card)
apply (elim allE exE conjE)
apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
apply (drule infinite_Card_is_InfCard, assumption)
apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans) 
done

lemma well_ord_imp_ex_Card: "well_ord(X,R) ⟹ ∃a. Card(a) ∧ X≈a"
by (fast elim!: well_ord_cardinal_eqpoll [THEN eqpoll_sym] 
         intro!: Card_cardinal)

lemma well_ord_infinite_subsets_eqpoll_X:
     "⟦well_ord(X,R); n ∈ nat; ¬Finite(X)⟧ ⟹ {Y ∈ Pow(X). Y≈succ(n)}≈X"
apply (drule well_ord_imp_ex_Card)
apply (elim allE exE conjE)
apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
apply (drule infinite_Card_is_InfCard, assumption)
apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans) 
done

end