# Theory HH

Up to index of Isabelle/ZF/AC

theory HH
imports AC_Equiv Hartog
begin

    (*  Title:      ZF/AC/HH.thy
        ID:         $Id: HH.thy,v 1.13 2005/06/17 14:15:10 haftmann Exp $
        Author:     Krzysztof Grabczewski

    Some properties of the recursive definition of HH used in the proofs of
      AC17 ==> AC1
      AC1 ==> WO2
      AC15 ==> WO6
    *)

    theory HH imports AC_Equiv Hartog begin

    constdefs

      HH :: "[i, i, i] => i"
        "HH(f,x,a) == transrec(a, %b r. let z = x - (\<Union>c ∈ b. r`c)
                                        in  if f`z ∈ Pow(z)-{0} then f`z else {x})"

    subsection{*Lemmas useful in each of the three proofs*}

    lemma HH_def_satisfies_eq:
         "HH(f,x,a) = (let z = x - (\<Union>b ∈ a. HH(f,x,b))
                       in  if f`z ∈ Pow(z)-{0} then f`z else {x})"
    by (rule HH_def [THEN def_transrec, THEN trans], simp)

    lemma HH_values: "HH(f,x,a) ∈ Pow(x)-{0} | HH(f,x,a)={x}"
    apply (rule HH_def_satisfies_eq [THEN ssubst])
    apply (simp add: Let_def Diff_subset [THEN PowI], fast)
    done

    lemma subset_imp_Diff_eq:
         "B ⊆ A ==> X-(\<Union>a ∈ A. P(a)) = X-(\<Union>a ∈ A-B. P(a))-(\<Union>b ∈ B. P(b))"
    by fast

    lemma Ord_DiffE: "[| c ∈ a-b; b<a |] ==> c=b | b<c & c<a"
    apply (erule ltE)
    apply (drule Ord_linear [of _ c])
    apply (fast elim: Ord_in_Ord)
    apply (fast intro!: ltI intro: Ord_in_Ord)
    done

    lemma Diff_UN_eq_self: "(!!y. y∈A ==> P(y) = {x}) ==> x - (\<Union>y ∈ A. P(y)) = x"
    by (simp, fast elim!: mem_irrefl)

    lemma HH_eq: "x - (\<Union>b ∈ a. HH(f,x,b)) = x - (\<Union>b ∈ a1. HH(f,x,b))
                  ==> HH(f,x,a) = HH(f,x,a1)"
    apply (subst HH_def_satisfies_eq [of _ _ a1])
    apply (rule HH_def_satisfies_eq [THEN trans], simp)
    done

    lemma HH_is_x_gt_too: "[| HH(f,x,b)={x}; b<a |] ==> HH(f,x,a)={x}"
    apply (rule_tac P = "b<a" in impE)
    prefer 2 apply assumption+
    apply (erule lt_Ord2 [THEN trans_induct])
    apply (rule impI)
    apply (rule HH_eq [THEN trans])
    prefer 2 apply assumption+
    apply (rule leI [THEN le_imp_subset, THEN subset_imp_Diff_eq, THEN ssubst],
           assumption)
    apply (rule_tac t = "%z. z-?X" in subst_context)
    apply (rule Diff_UN_eq_self)
    apply (drule Ord_DiffE, assumption)
    apply (fast elim: ltE, auto)
    done

    lemma HH_subset_x_lt_too:
         "[| HH(f,x,a) ∈ Pow(x)-{0}; b<a |] ==> HH(f,x,b) ∈ Pow(x)-{0}"
    apply (rule HH_values [THEN disjE], assumption)
    apply (drule HH_is_x_gt_too, assumption)
    apply (drule subst, assumption)
    apply (fast elim!: mem_irrefl)
    done

    lemma HH_subset_x_imp_subset_Diff_UN:
        "HH(f,x,a) ∈ Pow(x)-{0} ==> HH(f,x,a) ∈ Pow(x - (\<Union>b ∈ a. HH(f,x,b)))-{0}"
    apply (drule HH_def_satisfies_eq [THEN subst])
    apply (rule HH_def_satisfies_eq [THEN ssubst])
    apply (simp add: Let_def Diff_subset [THEN PowI])
    apply (drule split_if [THEN iffD1])
    apply (fast elim!: mem_irrefl)
    done

    lemma HH_eq_arg_lt:
         "[| HH(f,x,v)=HH(f,x,w); HH(f,x,v) ∈ Pow(x)-{0}; v ∈ w |] ==> P"
    apply (frule_tac P = "%y. y ∈ Pow (x) -{0}" in subst, assumption)
    apply (drule_tac a = w in HH_subset_x_imp_subset_Diff_UN)
    apply (drule subst_elem, assumption)
    apply (fast intro!: singleton_iff [THEN iffD2] equals0I)
    done

    lemma HH_eq_imp_arg_eq:
      "[| HH(f,x,v)=HH(f,x,w); HH(f,x,w) ∈ Pow(x)-{0}; Ord(v); Ord(w) |] ==> v=w"
    apply (rule_tac j = w in Ord_linear_lt)
    apply (simp_all (no_asm_simp))
     apply (drule subst_elem, assumption)
     apply (blast dest: ltD HH_eq_arg_lt)
    apply (blast dest: HH_eq_arg_lt [OF sym] ltD)
    done

    lemma HH_subset_x_imp_lepoll:
         "[| HH(f, x, i) ∈ Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}"
    apply (unfold lepoll_def inj_def)
    apply (rule_tac x = "λj ∈ i. HH (f, x, j) " in exI)
    apply (simp (no_asm_simp))
    apply (fast del: DiffE
                elim!: HH_eq_imp_arg_eq Ord_in_Ord HH_subset_x_lt_too
                intro!: lam_type ballI ltI intro: bexI)
    done

    lemma HH_Hartog_is_x: "HH(f, x, Hartog(Pow(x)-{0})) = {x}"
    apply (rule HH_values [THEN disjE])
    prefer 2 apply assumption
    apply (fast del: DiffE
                intro!: Ord_Hartog
                dest!: HH_subset_x_imp_lepoll
                elim!: Hartog_lepoll_selfE)
    done

    lemma HH_Least_eq_x: "HH(f, x, LEAST i. HH(f, x, i) = {x}) = {x}"
    by (fast intro!: Ord_Hartog HH_Hartog_is_x LeastI)

    lemma less_Least_subset_x:
         "a ∈ (LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) ∈ Pow(x)-{0}"
    apply (rule HH_values [THEN disjE], assumption)
    apply (rule less_LeastE)
    apply (erule_tac [2] ltI [OF _ Ord_Least], assumption)
    done

    subsection{*Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1*}

    lemma lam_Least_HH_inj_Pow:
            "(λa ∈ (LEAST i. HH(f,x,i)={x}). HH(f,x,a))
             ∈ inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})"
    apply (unfold inj_def, simp)
    apply (fast intro!: lam_type dest: less_Least_subset_x
                elim!: HH_eq_imp_arg_eq Ord_Least [THEN Ord_in_Ord])
    done

    lemma lam_Least_HH_inj:
         "∀a ∈ (LEAST i. HH(f,x,i)={x}). ∃z ∈ x. HH(f,x,a) = {z}
          ==> (λa ∈ (LEAST i. HH(f,x,i)={x}). HH(f,x,a))
              ∈ inj(LEAST i. HH(f,x,i)={x}, {{y}. y ∈ x})"
    by (rule lam_Least_HH_inj_Pow [THEN inj_strengthen_type], simp)

    lemma lam_surj_sing:
            "[| x - (\<Union>a ∈ A. F(a)) = 0;  ∀a ∈ A. ∃z ∈ x. F(a) = {z} |]
             ==> (λa ∈ A. F(a)) ∈ surj(A, {{y}. y ∈ x})"
    apply (simp add: surj_def lam_type Diff_eq_0_iff)
    apply (blast elim: equalityE)
    done

    lemma not_emptyI2: "y ∈ Pow(x)-{0} ==> x ≠ 0"
    by auto

    lemma f_subset_imp_HH_subset:
         "f`(x - (\<Union>j ∈ i. HH(f,x,j))) ∈ Pow(x - (\<Union>j ∈ i. HH(f,x,j)))-{0}
          ==> HH(f, x, i) ∈ Pow(x) - {0}"
    apply (rule HH_def_satisfies_eq [THEN ssubst])
    apply (simp add: Let_def Diff_subset [THEN PowI] not_emptyI2 [THEN if_P], fast)
    done

    lemma f_subsets_imp_UN_HH_eq_x:
         "∀z ∈ Pow(x)-{0}. f`z ∈ Pow(z)-{0}
          ==> x - (\<Union>j ∈ (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"
    apply (case_tac "?P ∈ {0}", fast)
    apply (drule Diff_subset [THEN PowI, THEN DiffI])
    apply (drule bspec, assumption)
    apply (drule f_subset_imp_HH_subset)
    apply (blast dest!: subst_elem [OF _ HH_Least_eq_x [symmetric]]
                 elim!: mem_irrefl)
    done

    lemma HH_values2: "HH(f,x,i) = f`(x - (\<Union>j ∈ i. HH(f,x,j))) | HH(f,x,i)={x}"
    apply (rule HH_def_satisfies_eq [THEN ssubst])
    apply (simp add: Let_def Diff_subset [THEN PowI])
    done

    lemma HH_subset_imp_eq:
         "HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (\<Union>j ∈ i. HH(f,x,j)))"
    apply (rule HH_values2 [THEN disjE], assumption)
    apply (fast elim!: equalityE mem_irrefl dest!: singleton_subsetD)
    done

    lemma f_sing_imp_HH_sing:
         "[| f ∈ (Pow(x)-{0}) -> {{z}. z ∈ x};
             a ∈ (LEAST i. HH(f,x,i)={x}) |] ==> ∃z ∈ x. HH(f,x,a) = {z}"
    apply (drule less_Least_subset_x)
    apply (frule HH_subset_imp_eq)
    apply (drule apply_type)
    apply (rule Diff_subset [THEN PowI, THEN DiffI])
    apply (fast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2], force)
    done

    lemma f_sing_lam_bij:
         "[| x - (\<Union>j ∈ (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0;
             f ∈ (Pow(x)-{0}) -> {{z}. z ∈ x} |]
          ==> (λa ∈ (LEAST i. HH(f,x,i)={x}). HH(f,x,a))
              ∈ bij(LEAST i. HH(f,x,i)={x}, {{y}. y ∈ x})"
    apply (unfold bij_def)
    apply (fast intro!: lam_Least_HH_inj lam_surj_sing f_sing_imp_HH_sing)
    done

    lemma lam_singI:
         "f ∈ (Π X ∈ Pow(x)-{0}. F(X))
          ==> (λX ∈ Pow(x)-{0}. {f`X}) ∈ (Π X ∈ Pow(x)-{0}. {{z}. z ∈ F(X)})"
    by (fast del: DiffI DiffE
                intro!: lam_type singleton_eq_iff [THEN iffD2] dest: apply_type)

    (*FIXME: both uses have the form ...[THEN bij_converse_bij], so
      simplification is needed!*)
    lemmas bij_Least_HH_x =
        comp_bij [OF f_sing_lam_bij [OF _ lam_singI]
                  lam_sing_bij [THEN bij_converse_bij], standard]

    subsection{*The proof of AC1 ==> WO2*}

    (*Establishing the existence of a bijection, namely
    converse
     (converse(λx∈x. {x}) O
      Lambda
       (LEAST i. HH(λX∈Pow(x) - {0}. {f ` X}, x, i) = {x},
        HH(λX∈Pow(x) - {0}. {f ` X}, x)))
    Perhaps it could be simplified. *)

    lemma bijection:
         "f ∈ (Π X ∈ Pow(x) - {0}. X)
          ==> ∃g. g ∈ bij(x, LEAST i. HH(λX ∈ Pow(x)-{0}. {f`X}, x, i) = {x})"
    apply (rule exI)
    apply (rule bij_Least_HH_x [THEN bij_converse_bij])
    apply (rule f_subsets_imp_UN_HH_eq_x)
    apply (intro ballI apply_type)
    apply (fast intro: lam_type apply_type del: DiffE, assumption)
    apply (fast intro: Pi_weaken_type)
    done

    lemma AC1_WO2: "AC1 ==> WO2"
    apply (unfold AC1_def WO2_def eqpoll_def)
    apply (intro allI)
    apply (drule_tac x = "Pow(A) - {0}" in spec)
    apply (blast dest: bijection)
    done

    end

### Lemmas useful in each of the three proofs

lemma HH_def_satisfies_eq:

      HH(f, x, a) =
      (let z = x - (\<Union>b∈a. HH(f, x, b))
       in if f ` z ∈ Pow(z) - {0} then f ` z else {x})

lemma HH_values:

      HH(f, x, a) ∈ Pow(x) - {0} ∨ HH(f, x, a) = {x}

lemma subset_imp_Diff_eq:

      B ⊆ A
      ==> X - (\<Union>a∈A. P(a)) = X - (\<Union>a∈A - B. P(a)) - (\<Union>b∈B. P(b))

lemma Ord_DiffE:

      [| c ∈ a - b; b < a |] ==> c = b ∨ b < c ∧ c < a

lemma Diff_UN_eq_self:

      (!!y. y ∈ A ==> P(y) = {x}) ==> x - (\<Union>y∈A. P(y)) = x

lemma HH_eq:

      x - (\<Union>b∈a. HH(f, x, b)) = x - (\<Union>b∈a1.0. HH(f, x, b))
      ==> HH(f, x, a) = HH(f, x, a1.0)

lemma HH_is_x_gt_too:

      [| HH(f, x, b) = {x}; b < a |] ==> HH(f, x, a) = {x}

lemma HH_subset_x_lt_too:

      [| HH(f, x, a) ∈ Pow(x) - {0}; b < a |] ==> HH(f, x, b) ∈ Pow(x) - {0}

lemma HH_subset_x_imp_subset_Diff_UN:

      HH(f, x, a) ∈ Pow(x) - {0}
      ==> HH(f, x, a) ∈ Pow(x - (\<Union>b∈a. HH(f, x, b))) - {0}

lemma HH_eq_arg_lt:

      [| HH(f, x, v) = HH(f, x, w); HH(f, x, v) ∈ Pow(x) - {0}; v ∈ w |] ==> P

lemma HH_eq_imp_arg_eq:

      [| HH(f, x, v) = HH(f, x, w); HH(f, x, w) ∈ Pow(x) - {0}; Ord(v); Ord(w) |]
      ==> v = w

lemma HH_subset_x_imp_lepoll:

      [| HH(f, x, i) ∈ Pow(x) - {0}; Ord(i) |] ==> i lepoll Pow(x) - {0}

lemma HH_Hartog_is_x:

      HH(f, x, Hartog(Pow(x) - {0})) = {x}

lemma HH_Least_eq_x:

      HH(f, x, μi. HH(f, x, i) = {x}) = {x}

lemma less_Least_subset_x:

      a ∈ (μi. HH(f, x, i) = {x}) ==> HH(f, x, a) ∈ Pow(x) - {0}

### Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1

lemma lam_Least_HH_inj_Pow:

      (λa∈μi. HH(f, x, i) = {x}. HH(f, x, a)) ∈
      inj(μi. HH(f, x, i) = {x}, Pow(x) - {0})

lemma lam_Least_HH_inj:

      ∀a∈μi. HH(f, x, i) = {x}. ∃z∈x. HH(f, x, a) = {z}
      ==> (λa∈μi. HH(f, x, i) = {x}. HH(f, x, a)) ∈
          inj(μi. HH(f, x, i) = {x}, {{y} . y ∈ x})

lemma lam_surj_sing:

      [| x - (\<Union>a∈A. F(a)) = 0; ∀a∈A. ∃z∈x. F(a) = {z} |]
      ==> (λa∈A. F(a)) ∈ surj(A, {{y} . y ∈ x})

lemma not_emptyI2:

      y ∈ Pow(x) - {0} ==> x ≠ 0

lemma f_subset_imp_HH_subset:

      f ` (x - (\<Union>j∈i. HH(f, x, j))) ∈ Pow(x - (\<Union>j∈i. HH(f, x, j))) - {0}
      ==> HH(f, x, i) ∈ Pow(x) - {0}

lemma f_subsets_imp_UN_HH_eq_x:

      ∀z∈Pow(x) - {0}. f ` z ∈ Pow(z) - {0}
      ==> x - (\<Union>j∈μi. HH(f, x, i) = {x}. HH(f, x, j)) = 0

lemma HH_values2:

      HH(f, x, i) = f ` (x - (\<Union>j∈i. HH(f, x, j))) ∨ HH(f, x, i) = {x}

lemma HH_subset_imp_eq:

      HH(f, x, i) ∈ Pow(x) - {0}
      ==> HH(f, x, i) = f ` (x - (\<Union>j∈i. HH(f, x, j)))

lemma f_sing_imp_HH_sing:

      [| f ∈ Pow(x) - {0} -> {{z} . z ∈ x}; a ∈ (μi. HH(f, x, i) = {x}) |]
      ==> ∃z∈x. HH(f, x, a) = {z}

lemma f_sing_lam_bij:

      [| x - (\<Union>j∈μi. HH(f, x, i) = {x}. HH(f, x, j)) = 0;
         f ∈ Pow(x) - {0} -> {{z} . z ∈ x} |]
      ==> (λa∈μi. HH(f, x, i) = {x}. HH(f, x, a)) ∈
          bij(μi. HH(f, x, i) = {x}, {{y} . y ∈ x})

lemma lam_singI:

      f ∈ (ΠX∈Pow(x) - {0}. F(X))
      ==> (λX∈Pow(x) - {0}. {f ` X}) ∈ (ΠX∈Pow(x) - {0}. {{z} . z ∈ F(X)})

lemmas bij_Least_HH_x:

      [| C - (\<Union>j∈μi. HH(λX∈Pow(C) - {0}. {f ` X}, C, i) = {C}.
                 HH(λX∈Pow(C) - {0}. {f ` X}, C, j)) =
         0;
         f ∈ Pow(C) - {0} -> C |]
      ==> converse(λx∈C. {x}) O
          (λa∈μi. HH(λX∈Pow(C) - {0}. {f ` X}, C, i) = {C}.
              HH(λX∈Pow(C) - {0}. {f ` X}, C, a)) ∈
          bij(μi. HH(λX∈Pow(C) - {0}. {f ` X}, C, i) = {C}, C)

lemmas bij_Least_HH_x:

      [| C - (\<Union>j∈μi. HH(λX∈Pow(C) - {0}. {f ` X}, C, i) = {C}.
                 HH(λX∈Pow(C) - {0}. {f ` X}, C, j)) =
         0;
         f ∈ Pow(C) - {0} -> C |]
      ==> converse(λx∈C. {x}) O
          (λa∈μi. HH(λX∈Pow(C) - {0}. {f ` X}, C, i) = {C}.
              HH(λX∈Pow(C) - {0}. {f ` X}, C, a)) ∈
          bij(μi. HH(λX∈Pow(C) - {0}. {f ` X}, C, i) = {C}, C)

### The proof of AC1 ==> WO2

lemma bijection:

      f ∈ (ΠX∈Pow(x) - {0}. X)
      ==> ∃g. g ∈ bij(x, μi. HH(λX∈Pow(x) - {0}. {f ` X}, x, i) = {x})

lemma AC1_WO2:

      AC1 ==> WO2