Theory Cardinal_AC_Relative

sectionRelative, Cardinal Arithmetic Using AC

theory Cardinal_AC_Relative
  imports
    CardinalArith_Relative

begin

locale M_AC =
  fixes M
  assumes
  choice_ax: "choice_ax(M)"

locale M_cardinal_AC = M_cardinal_arith + M_AC
begin

lemma well_ord_surj_imp_lepoll_rel:
  assumes "well_ord(A,r)" "h  surj(A,B)" and
    types:"M(A)" "M(r)" "M(h)" "M(B)"
  shows "B ≲⇗MA"
proof -
  note eq=vimage_fun_sing[OF surj_is_fun[OF h_]]
  from assms
  have "(λbB. minimum(r, {aA. h`a=b}))  inj(B,A)" (is "?f_")
    using well_ord_surj_imp_inj_inverse assms(1,2) by simp
  with assms
  have "M(?f`b)" if "bB" for b
    using apply_type[OF inj_is_fun[OF ?f_]] that transM[OF _ M(A)] by simp
  with assms
  have "M(?f)"
    using lam_closed surj_imp_inj_replacement4 eq by auto
  with ?f_ assms
  have "?f  inj⇗M⇖(B,A)"
    using mem_inj_abs by simp
  with M(?f)
  show ?thesis unfolding lepoll_rel_def by auto
qed

lemma surj_imp_well_ord_M:
  assumes wos: "well_ord(A,r)" "h  surj(A,B)"
    and
    types: "M(A)" "M(r)" "M(h)" "M(B)"
  shows "s[M]. well_ord(B,s)"
  using assms lepoll_rel_well_ord
    well_ord_surj_imp_lepoll_rel by fast


lemma choice_ax_well_ord: "M(S)  r[M]. well_ord(S,r)"
  using choice_ax well_ord_Memrel[THEN surj_imp_well_ord_M]
  unfolding choice_ax_def by auto

lemma Finite_cardinal_rel_Finite:
  assumes "Finite(|i|⇗M)" "M(i)"
  shows "Finite(i)"
proof -
  note assms
  moreover from this
  obtain r where "M(r)" "well_ord(i,r)"
    using choice_ax_well_ord by auto
  moreover from calculation
  have "|i|⇗M⇖ ≈⇗Mi"
    using well_ord_cardinal_rel_eqpoll_rel
    by auto
  ultimately
  show ?thesis
    using eqpoll_rel_imp_Finite
    by auto
qed

end ― ‹localeM_cardinal_AC

locale M_Pi_assumptions_choice = M_Pi_assumptions + M_cardinal_AC +
  assumes
    B_replacement: "strong_replacement(M, λx y. y = B(x))"
    and
    ― ‹The next one should be derivable from (some variant)
        of B\_replacement. Proving both instances each time seems
        inconvenient.
    minimum_replacement: "M(r)  strong_replacement(M, λx y. y = x, minimum(r, B(x)))"
begin

lemma AC_M:
  assumes "a  A" "x. x  A  y. y  B(x)"
  shows "z[M]. z  Pi⇗M⇖(A, B)"
proof -
  have "M(xA. B(x))" using assms family_union_closed Pi_assumptions B_replacement by simp
  then
  obtain r where "well_ord(xA. B(x),r)" "M(r)"
    using choice_ax_well_ord by blast
  let ?f="λxA. minimum(r,B(x))"
  have "M(minimum(r, B(x)))" if "xA" for x
  proof -
    from well_ord(_,r) xA
    have "well_ord(B(x),r)" using well_ord_subset UN_upper by simp
    with assms xA M(r)
    show ?thesis using Pi_assumptions by blast
  qed
  with assms and M(r)
  have "M(?f)"
    using Pi_assumptions minimum_replacement lam_closed
    by simp
  moreover from assms and calculation
  have "?f  Pi⇗M⇖(A,B)"
    using lam_type[OF minimum_in, OF well_ord(xA. B(x),r), of A B]
     Pi_rel_char by auto
  ultimately
  show ?thesis by blast
qed

lemma AC_Pi_rel: assumes "x. x  A  y. y  B(x)"
  shows "z[M]. z  Pi⇗M⇖(A, B)"
proof (cases "A=0")
  interpret Pi0:M_Pi_assumptions_0
    using Pi_assumptions by unfold_locales auto
  case True
  then
  show ?thesis using assms by simp
next
  case False
  then
  obtain a where "a  A" by auto
    ― ‹It is noteworthy that without obtaining an element of
        termA, the final step won't work
  with assms
  show ?thesis by (blast intro!: AC_M)
qed

end ― ‹localeM_Pi_assumptions_choice


context M_cardinal_AC
begin

subsectionStrengthened Forms of Existing Theorems on Cardinals

lemma cardinal_rel_eqpoll_rel: "M(A)  |A|⇗M⇖ ≈⇗MA"
apply (rule choice_ax_well_ord [THEN rexE])
apply (auto intro:well_ord_cardinal_rel_eqpoll_rel)
done

lemmas cardinal_rel_idem = cardinal_rel_eqpoll_rel [THEN cardinal_rel_cong, simp]

lemma cardinal_rel_eqE: "|X|⇗M= |Y|⇗M==> M(X)  M(Y)  X ≈⇗MY"
apply (rule choice_ax_well_ord [THEN rexE], assumption)
   apply (rule choice_ax_well_ord [THEN rexE, of Y], assumption)
    apply (rule well_ord_cardinal_rel_eqE, assumption+)
done

lemma cardinal_rel_eqpoll_rel_iff: "M(X)  M(Y)  |X|⇗M= |Y|⇗M X ≈⇗MY"
by (blast intro: cardinal_rel_cong cardinal_rel_eqE)

lemma cardinal_rel_disjoint_Un:
     "[| |A|⇗M=|B|⇗M;  |C|⇗M=|D|⇗M;  A  C = 0;  B  D = 0; M(A); M(B); M(C); M(D)|]
      ==> |A  C|⇗M= |B  D|⇗M"
by (simp add: cardinal_rel_eqpoll_rel_iff eqpoll_rel_disjoint_Un)

lemma lepoll_rel_imp_cardinal_rel_le: "A ≲⇗MB ==> M(A)  M(B)  |A|⇗M |B|⇗M"
  apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
   apply (erule well_ord_lepoll_rel_imp_cardinal_rel_le, assumption+)
  done

lemma cadd_rel_assoc: "M(i); M(j); M(k)  (i ⊕⇗Mj) ⊕⇗Mk = i ⊕⇗M(j ⊕⇗Mk)"
  apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
   apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
    apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
     apply (rule well_ord_cadd_rel_assoc, assumption+)
done

lemma cmult_rel_assoc: "M(i); M(j); M(k)  (i ⊗⇗Mj) ⊗⇗Mk = i ⊗⇗M(j ⊗⇗Mk)"
  apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
   apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
    apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
     apply (rule well_ord_cmult_rel_assoc, assumption+)
  done

lemma cadd_cmult_distrib: "M(i); M(j); M(k)  (i ⊕⇗Mj) ⊗⇗Mk = (i ⊗⇗Mk) ⊕⇗M(j ⊗⇗Mk)"
  apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
   apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
    apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
     apply (rule well_ord_cadd_cmult_distrib, assumption+)
  done


lemma InfCard_rel_square_eq: "InfCard⇗M⇖(|A|⇗M)  M(A)  A×A ≈⇗MA"
apply (rule choice_ax_well_ord [THEN rexE]) prefer 2
   apply (erule well_ord_InfCard_rel_square_eq, assumption, simp_all)
done

subsection The relationship between cardinality and le-pollence

lemma Card_rel_le_imp_lepoll_rel:
  assumes "|A|⇗M |B|⇗M"
    and types: "M(A)" "M(B)"
  shows "A ≲⇗MB"
proof -
  have "A ≈⇗M|A|⇗M"
    by (rule cardinal_rel_eqpoll_rel [THEN eqpoll_rel_sym], simp_all add:types)
  also have "... ≲⇗M|B|⇗M"
    by (rule le_imp_subset [THEN subset_imp_lepoll_rel]) (rule assms, simp_all add:types)
  also have "... ≈⇗MB"
    by (rule cardinal_rel_eqpoll_rel, simp_all add:types)
  finally show ?thesis by (simp_all add:types)
qed

lemma le_Card_rel_iff: "Card⇗M⇖(K) ==> M(K)  M(A)  |A|⇗M K  A ≲⇗MK"
apply (erule Card_rel_cardinal_rel_eq [THEN subst], assumption, rule iffI,
       erule Card_rel_le_imp_lepoll_rel, assumption+)
apply (erule lepoll_rel_imp_cardinal_rel_le, assumption+)
done

lemma cardinal_rel_0_iff_0 [simp]: "M(A)  |A|⇗M= 0  A = 0"
  using cardinal_rel_0 eqpoll_rel_0_iff [THEN iffD1]
    cardinal_rel_eqpoll_rel_iff [THEN iffD1, OF _ nonempty]
  by auto

lemma cardinal_rel_lt_iff_lesspoll_rel:
  assumes i: "Ord(i)" and
    types: "M(i)" "M(A)"
  shows "i < |A|⇗M i ≺⇗MA"
proof
  assume "i < |A|⇗M"
  hence  "i ≺⇗M|A|⇗M"
    by (blast intro: lt_Card_rel_imp_lesspoll_rel types)
  also have "...  ≈⇗MA"
    by (rule cardinal_rel_eqpoll_rel) (simp_all add:types)
  finally show "i ≺⇗MA" by (simp_all add:types)
next
  assume "i ≺⇗MA"
  also have "...  ≈⇗M|A|⇗M"
    by (blast intro: cardinal_rel_eqpoll_rel eqpoll_rel_sym types)
  finally have "i ≺⇗M|A|⇗M" by (simp_all add:types)
  thus  "i < |A|⇗M" using i types
    by (force intro: cardinal_rel_lt_imp_lt lesspoll_rel_cardinal_rel_lt)
qed

lemma cardinal_rel_le_imp_lepoll_rel: " i  |A|⇗M==> M(i)  M(A) i ≲⇗MA"
  by (blast intro: lt_Ord Card_rel_le_imp_lepoll_rel Ord_cardinal_rel_le le_trans)


subsectionOther Applications of AC

textWe have an example of instantiating a locale involving higher
order variables inside a proof, by using the assumptions of the
first order, active locale.

lemma surj_rel_implies_inj_rel:
  assumes f: "f  surj⇗M⇖(X,Y)" and
    types: "M(f)" "M(X)" "M(Y)"
  shows "g[M]. g  inj⇗M⇖(Y,X)"
proof -
  from types
  interpret M_Pi_assumptions_choice _ Y "λy. f-``{y}"
    by unfold_locales (auto intro:surj_imp_inj_replacement dest:transM)
  from f AC_Pi_rel
  obtain z where z: "z  Pi⇗M⇖(Y, λy. f -`` {y})"
    ― ‹In this and the following ported result, it is not clear how
        uniformly are "\_char" theorems to be used
    using surj_rel_char
    by (auto simp add: surj_def types) (fast dest: apply_Pair)
  show ?thesis
  proof
    show "z  inj⇗M⇖(Y, X)" "M(z)"
      using z surj_is_fun[of f X Y] f Pi_rel_char
      by (auto dest: apply_type Pi_memberD
          intro: apply_equality Pi_type f_imp_injective
          simp add:types mem_surj_abs)
  qed
qed


textKunen's Lemma 10.20
lemma surj_rel_implies_cardinal_rel_le:
  assumes f: "f  surj⇗M⇖(X,Y)" and
    types:"M(f)" "M(X)" "M(Y)"
  shows "|Y|⇗M |X|⇗M"
proof (rule lepoll_rel_imp_cardinal_rel_le)
  from f [THEN surj_rel_implies_inj_rel]
  obtain g where "g  inj⇗M⇖(Y,X)"
    by (blast intro:types)
  then
  show "Y ≲⇗MX"
    using inj_rel_char
    by (auto simp add: def_lepoll_rel types)
qed (simp_all add:types)

end ― ‹localeM_cardinal_AC

textThe set-theoretic universe.

abbreviation
  Universe :: "io" (𝒱) where
  "𝒱(x)  True"

lemma separation_absolute: "separation(𝒱, P)"
  unfolding separation_def
  by (rule rallI, rule_tac x="{x_ . P(x)}" in rexI) auto

lemma univalent_absolute:
  assumes "univalent(𝒱, A, P)" "P(x, b)" "x  A"
  shows "P(x, y)  y = b"
  using assms
  unfolding univalent_def by force

lemma replacement_absolute: "strong_replacement(𝒱, P)"
  unfolding strong_replacement_def
proof (intro rallI impI)
  fix A
  assume "univalent(𝒱, A, P)"
  then
  show "Y[𝒱]. b[𝒱]. b  Y  (x[𝒱]. x  A  P(x, b))"
    by (rule_tac x="{y. xA , P(x,y)}" in rexI)
      (auto dest:univalent_absolute[of _ P])
qed

lemma Union_ax_absolute: "Union_ax(𝒱)"
    unfolding Union_ax_def big_union_def
    by (auto intro:rexI[of _ "_"])

lemma upair_ax_absolute: "upair_ax(𝒱)"
  unfolding upair_ax_def upair_def rall_def rex_def
    by (auto)

lemma power_ax_absolute:"power_ax(𝒱)"
proof -
  {
    fix x
    have "y[𝒱]. y  Pow(x)  (z[𝒱]. z  y  z  x)"
      by auto
  }
  then
  show "power_ax(𝒱)"
    unfolding power_ax_def powerset_def subset_def by blast
qed

locale M_cardinal_UN =  M_Pi_assumptions_choice _ K X for K X +
  assumes
    ― ‹The next assumption is required by @{thm Least_closed}
    X_witness_in_M: "w  X(x)  M(x)"
    and
    lam_m_replacement:"M(f)  strong_replacement(M,
      λx y. y = x, μ i. x  X(i), f ` (μ i. x  X(i)) ` x)"
    and
    inj_replacement:
    "M(x)  strong_replacement(M, λy z. y  inj⇗M⇖(X(x), K)  z = {x, y})"
    "strong_replacement(M, λx y. y = inj⇗M⇖(X(x), K))"
    "strong_replacement(M,
      λx z. z = Sigfun(x, λi. inj⇗M⇖(X(i), K)))"
    "M(r)  strong_replacement(M,
      λx y. y = x, minimum(r, inj⇗M⇖(X(x), K)))"

begin

lemma UN_closed: "M(iK. X(i))"
  using family_union_closed B_replacement Pi_assumptions by simp

textKunen's Lemma 10.21
lemma cardinal_rel_UN_le:
  assumes K: "InfCard⇗M⇖(K)"
  shows "(i. iK  |X(i)|⇗M K)  |iK. X(i)|⇗M K"
proof (simp add: K InfCard_rel_is_Card_rel le_Card_rel_iff Pi_assumptions)
  have "M(f)  M(λx(xK. X(x)). μ i. x  X(i), f ` (μ i. x  X(i)) ` x)" for f
    using lam_m_replacement X_witness_in_M Least_closed' Pi_assumptions UN_closed
    by (rule_tac lam_closed) (auto dest:transM)
  note types = this Pi_assumptions UN_closed
  have [intro]: "Ord(K)" by (blast intro: InfCard_rel_is_Card_rel
        Card_rel_is_Ord K types)
  interpret pii:M_Pi_assumptions_choice _ K "λi. inj⇗M⇖(X(i), K)"
    using inj_replacement Pi_assumptions transM[of _ K]
    by unfold_locales (simp_all del:mem_inj_abs)
  assume asm:"i. iK  X(i) ≲⇗MK"
  then
  have "i. iK  M(inj⇗M⇖(X(i), K))"
    by (auto simp add: types)
  interpret V:M_N_Perm M "𝒱"
    using separation_absolute replacement_absolute Union_ax_absolute
      power_ax_absolute upair_ax_absolute
    by unfold_locales auto
  note bad_simps[simp del] = V.N.Forall_in_M_iff V.N.Equal_in_M_iff
    V.N.nonempty
  have abs:"inj_rel(𝒱,x,y) = inj(x,y)" for x y
    using V.N.inj_rel_char by simp
  from asm
  have "i. iK  f[M]. f  inj⇗M⇖(X(i), K)"
    by (simp add: types def_lepoll_rel)
  then
  obtain f where "f  (iK. inj⇗M⇖(X(i), K))" "M(f)"
    using pii.AC_Pi_rel pii.Pi_rel_char by auto
  with abs
  have f:"f  (iK. inj(X(i), K))"
    using Pi_weaken_type[OF _ V.inj_rel_transfer, of f K X "λ_. K"]
      Pi_assumptions by simp
  { fix z
    assume z: "z  (iK. X(i))"
    then obtain i where i: "i  K" "Ord(i)" "z  X(i)"
      by (blast intro: Ord_in_Ord [of K])
    hence "(μ i. z  X(i))  i" by (fast intro: Least_le)
    hence "(μ i. z  X(i)) < K" by (best intro: lt_trans1 ltI i)
    hence "(μ i. z  X(i))  K" and "z  X(μ i. z  X(i))"
      by (auto intro: LeastI ltD i)
  } note mems = this
  have "(iK. X(i)) ≲⇗MK × K"
    proof (simp add:types def_lepoll_rel)
      show "f[M]. f  inj(xK. X(x), K × K)"
        apply (rule rexI)
        apply (rule_tac c = "λz. μ i. z  X(i), f ` (μ i. z  X(i)) ` z"
                    and d = "λi,j. converse (f`i) ` j" in lam_injective)
          apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
        apply (simp add:types M(f))
        done
    qed
    also have "... ≈⇗MK"
    by (simp add: K InfCard_rel_square_eq InfCard_rel_is_Card_rel
        Card_rel_cardinal_rel_eq types)
  finally have "(iK. X(i)) ≲⇗MK" by (simp_all add:types)
  then
  show ?thesis
    by (simp add: K InfCard_rel_is_Card_rel le_Card_rel_iff types)
qed

end ― ‹localeM_cardinal_UN

end