Theory Cofinality

section‹Cofinality\label{sec:cofinality}›

theory Cofinality
  imports
    ZF_Library
begin


subsection‹Basic results and definitions›

text‹A set termX is ‹cofinal› in termA (with respect to the relation
    termr) if every element of termA is ``bounded
    above'' by some element of termX. Note that termX does not need 
    to be a subset of termA.›
definition
  cofinal :: "[i,i,i]  o" where
  "cofinal(X,A,r)  aA. xX. a,xr  a = x"

(*
(* Alternative definitions *)
definition
  cofinal_predic :: "[i,i,[i,i]⇒o] ⇒ o" where
  "cofinal_predic(X,A,r) ≡ ∀a∈A. ∃x∈X. r(a,x) ∨ a = x"

definition
  f_cofinal :: "[i⇒i,i,i,i] ⇒ o" where
  "f_cofinal(f,C,A,r) ≡ ∀a∈A. ∃x∈C. ⟨a,f(x)⟩∈r ∨ a = f(x)"

(* The next definition doesn't work if 0 is the top element of A.
   But it works for limit ordinals. *)
definition
  cofinal_fun' :: "[i,i,i] ⇒ o" where
  "cofinal_fun'(f,A,r) == f_cofinal(λx. f`x,domain(f),A, r)"
*)

text‹A function is cofinal if it range is.›
definition
  cofinal_fun :: "[i,i,i]  o" where
  "cofinal_fun(f,A,r)  aA. xdomain(f). a,f`xr  a = f`x"

lemma cofinal_funI:
  assumes "a. aA  xdomain(f). a,f`xr  a = f`x"
  shows "cofinal_fun(f,A,r)"
  using assms unfolding cofinal_fun_def by simp

lemma cofinal_funD:
  assumes "cofinal_fun(f,A,r)" "aA"
  shows "xdomain(f). a,f`xr  a = f`x"
  using assms unfolding cofinal_fun_def by simp

lemma cofinal_in_cofinal:
  assumes
    "trans(r)" "cofinal(Y,X,r)" "cofinal(X,A,r)"
  shows
    "cofinal(Y,A,r)"
  unfolding cofinal_def
proof
  fix a
  assume "aA"
  moreover from cofinal(X,A,r)
  have "bAxX. b,xr  b=x" for b
    unfolding cofinal_def by simp
  ultimately
  obtain y where "yX" "a,yr  a=y" by auto
  moreover from cofinal(Y,X,r)
  have "cXyY. c,yr  c=y" for c
    unfolding cofinal_def by simp
  ultimately
  obtain x where "xY" "y,xr  y=x" by auto
  with aA yX a,yr  a=y trans(r)
  show "xY. a,xr  a=x" unfolding trans_def by auto
qed

lemma codomain_is_cofinal:
  assumes "cofinal_fun(f,A,r)" "f:C  D"
  shows "cofinal(D,A,r)"
  unfolding cofinal_def
proof
  fix b
  assume "b  A"
  moreover from assms
  have "aA  xdomain(f). a, f ` x  r  a = f`x" for a
    unfolding cofinal_fun_def by simp
  ultimately
  obtain x where "xdomain(f)" "b, f ` x  r  b = f`x"
    by blast
  moreover from f:C  D  xdomain(f)
  have "f`xD"
    using domain_of_fun apply_rangeI by simp
  ultimately
  show  "yD. b, y  r  b = y" by auto
qed

lemma cofinal_range_iff_cofinal_fun:
  assumes "function(f)"
  shows "cofinal(range(f),A,r)  cofinal_fun(f,A,r)"
  unfolding cofinal_fun_def
proof (intro iffI ballI)
  fix a
  assume "aA" cofinal(range(f),A,r)
  then
  obtain y where "yrange(f)" "a,y  r  a = y"
    unfolding cofinal_def by blast
  moreover from this
  obtain x where "x,yf"
    unfolding range_def domain_def converse_def by blast
  moreover
  note function(f)
  ultimately
  have "a, f ` x  r  a = f ` x"
    using function_apply_equality by blast
  with x,yf
  show "xdomain(f). a, f ` x  r  a = f ` x"  by blast
next
  assume "aA. xdomain(f). a, f ` x  r  a = f ` x"
  with assms
  show "cofinal(range(f), A, r)"
    using function_apply_Pair[of f] unfolding cofinal_def by fast
qed

lemma cofinal_comp:
  assumes
    "f mono_map(C,s,D,r)" "cofinal_fun(f,D,r)" "h:B  C"  "cofinal_fun(h,C,s)"
    "trans(r)"
  shows "cofinal_fun(f O h,D,r)"
  unfolding cofinal_fun_def
proof
  fix a
  from f mono_map(C,s,D,r)
  have "f:C  D"
    using mono_map_is_fun by simp
  with h:B  C
  have "domain(f) = C" "domain(h) = B"
    using domain_of_fun by simp_all
  moreover
  assume "a  D"
  moreover
  note cofinal_fun(f,D,r)
  ultimately
  obtain c where "cC"  "a, f ` c  r  a = f ` c"
    unfolding cofinal_fun_def by blast
  with cofinal_fun(h,C,s) domain(h) = B
  obtain b where "b  B"  "c, h ` b  s  c = h ` b"
    unfolding cofinal_fun_def by blast
  moreover from this and h:B  C
  have "h`b  C" by simp
  moreover
  note f  mono_map(C,s,D,r)  cC
  ultimately
  have "f`c, f` (h ` b)  r  f`c = f` (h ` b)"
    unfolding mono_map_def by blast
  with a, f ` c  r  a = f ` c trans(r) h:B  C bB
  have "a, (f O h) ` b  r  a = (f O h) ` b"
    using transD by auto
  moreover from h:B  C domain(f) = C domain(h) = B
  have "domain(f O h) = B"
    using range_fun_subset_codomain by blast
  moreover
  note bB
  ultimately
  show "xdomain(f O h). a, (f O h) ` x  r  a = (f O h) ` x"  by blast
qed

definition
  cf_fun :: "[i,i]  o" where
  "cf_fun(f,α)  cofinal_fun(f,α,Memrel(α))"

lemma cf_funI[intro!]: "cofinal_fun(f,α,Memrel(α))  cf_fun(f,α)"
  unfolding cf_fun_def by simp

lemma cf_funD[dest!]: "cf_fun(f,α)  cofinal_fun(f,α,Memrel(α))"
  unfolding cf_fun_def by simp

lemma cf_fun_comp:
  assumes
    "Ord(α)" "f mono_map(C,s,α,Memrel(α))" "cf_fun(f,α)"
    "h:B  C" "cofinal_fun(h,C,s)"
  shows "cf_fun(f O h,α)"
  using assms cofinal_comp[OF _ _ _ _ trans_Memrel] by auto

definition
  cf :: "ii" where
  "cf(γ)  μ β.  A. Aγ  cofinal(A,γ,Memrel(γ))  β = ordertype(A,Memrel(γ))"

lemma Ord_cf [TC]: "Ord(cf(β))"
  unfolding cf_def using Ord_Least by simp

lemma gamma_cofinal_gamma:
  assumes "Ord(γ)"
  shows "cofinal(γ,γ,Memrel(γ))"
  unfolding cofinal_def by auto

lemma cf_is_ordertype:
  assumes "Ord(γ)"
  shows "A. Aγ  cofinal(A,γ,Memrel(γ))  cf(γ) = ordertype(A,Memrel(γ))"
    (is "?P(cf(γ))")
  using gamma_cofinal_gamma LeastI[of ?P γ] ordertype_Memrel[symmetric] assms
  unfolding cf_def by blast

lemma cf_fun_succ':
  assumes "Ord(β)" "Ord(α)" "f:αsucc(β)"
  shows "(xα. f`x=β)  cf_fun(f,succ(β))"
proof (intro iffI)
  assume "(xα. f`x=β)"
  with assms
  show "cf_fun(f,succ(β))"
    using domain_of_fun[OF f:αsucc(β)]
    unfolding cf_fun_def cofinal_fun_def by auto
next
  assume "cf_fun(f,succ(β))"
  with assms
  obtain x where "xα" "β,f`x  Memrel(succ(β))  β = f ` x"
    using domain_of_fun[OF f:αsucc(β)]
    unfolding cf_fun_def cofinal_fun_def by auto
  moreover from Ord(β)
  have "β,y  Memrel(succ(β))" for y
    using foundation unfolding Memrel_def by blast
  ultimately
  show "xα. f ` x = β" by blast
qed

lemma cf_fun_succ:
  "Ord(β)  f:1succ(β)  f`0=β  cf_fun(f,succ(β))"
  using cf_fun_succ' by blast

lemma ordertype_0_not_cofinal_succ:
  assumes "ordertype(A,Memrel(succ(i))) = 0"  "Asucc(i)" "Ord(i)"
  shows "¬cofinal(A,succ(i),Memrel(succ(i)))"
proof
  have 1:"ordertype(A,Memrel(succ(i))) = ordertype(0,Memrel(0))"
    using ordertype(A,Memrel(succ(i))) = 0 ordertype_0 by simp
  from  Asucc(i) Ord(i)
  have "f. f  A, Memrel(succ(i))  0, Memrel(0)"
    using   well_ord_Memrel well_ord_subset
      ordertype_eq_imp_ord_iso[OF 1] Ord_0  by blast
  then
  have "A=0"
    using  ord_iso_is_bij bij_imp_eqpoll eqpoll_0_is_0 by blast
  moreover
  assume "cofinal(A, succ(i), Memrel(succ(i)))"
  moreover
  note Ord(i)
  ultimately
  show "False"
    using not_mem_empty unfolding cofinal_def by auto
qed

text‹I thank Edwin Pacheco Rodríguez for the following lemma.›
lemma cf_succ:
  assumes "Ord(α)"
  shows "cf(succ(α)) = 1"
proof -
  define f where "f  {0,α}"
  then
  have  "f : 1succ(α)" "f`0 = α"
    using fun_extend3[of 0 0 "succ(α)" 0 α] singleton_0 by auto
  with assms
  have "cf_fun(f,succ(α))"
    using cf_fun_succ unfolding cofinal_fun_def by simp
  from f:1succ(α)
  have "0domain(f)" using domain_of_fun by simp
  define A where "A={f`0}"
  with cf_fun(f,succ(α)) 0domain(f) f`0=α
  have "cofinal(A,succ(α),Memrel(succ(α)))"
    unfolding cofinal_def cofinal_fun_def by simp
  moreover from  f`0=α A={f`0}
  have "A  succ(α)" unfolding succ_def  by auto
  moreover from Ord(α) A succ(α)
  have "well_ord(A,Memrel(succ(α)))"
    using Ord_succ well_ord_Memrel  well_ord_subset relation_Memrel by blast
  moreover from Ord(α)
  have "¬(A. A  succ(α)  cofinal(A, succ(α), Memrel(succ(α)))  0 = ordertype(A, Memrel(succ(α))))"
    (is "¬?P(0)")
    using ordertype_0_not_cofinal_succ  unfolding cf_def  by auto
  moreover
  have "1 = ordertype(A,Memrel(succ(α)))"
  proof -
    from A={f`0}
    have "A1" using singleton_eqpoll_1 by simp
    with well_ord(A,Memrel(succ(α)))
    show ?thesis using nat_1I ordertype_eq_n by simp
  qed
  ultimately
  show "cf(succ(α)) = 1" using Ord_1  Least_equality[of ?P 1]
    unfolding cf_def by blast
qed

lemma cf_zero [simp]:
  "cf(0) = 0"
  unfolding cf_def cofinal_def using
    ordertype_0 subset_empty_iff Least_le[of _ 0] by auto

lemma surj_is_cofinal: "f  surj(δ,γ)  cf_fun(f,γ)"
  unfolding surj_def cofinal_fun_def cf_fun_def
  using domain_of_fun by force

lemma cf_zero_iff: "Ord(α)  cf(α) = 0  α = 0"
proof (intro iffI)
  assume "α = 0" "Ord(α)"
  then
  show "cf(α) = 0" using cf_zero by simp
next
  assume "cf(α) = 0" "Ord(α)"
  moreover from this
  obtain A where "Aα" "cf(α) = ordertype(A,Memrel(α))"
    "cofinal(A,α,Memrel(α))"
    using cf_is_ordertype by blast
  ultimately
  have "cofinal(0,α,Memrel(α))"
    using ordertype_zero_imp_zero[of A "Memrel(α)"] by simp
  then
  show "α=0"
    unfolding cofinal_def by blast
qed

― ‹TODO: define Succ (predicate for successor ordinals)›
lemma cf_eq_one_iff:
  assumes "Ord(γ)"
  shows "cf(γ) = 1  (α. Ord(α)  γ  = succ(α))"
proof (intro iffI)
  assume "α. Ord(α)  γ  = succ(α)"
  then
  show "cf(γ) = 1" using cf_succ by auto
next
  assume "cf(γ) = 1"
  moreover from assms
  obtain A where "A  γ" "cf(γ) = ordertype(A,Memrel(γ))"
    "cofinal(A,γ,Memrel(γ))"
    using cf_is_ordertype by blast
  ultimately
  have "ordertype(A,Memrel(γ)) = 1" by simp
  moreover
  define f where "fconverse(ordermap(A,Memrel(γ)))"
  moreover from this ordertype(A,Memrel(γ)) = 1 A  γ assms
  have "f  surj(1,A)"
    using well_ord_subset[OF well_ord_Memrel, THEN ordermap_bij,
        THEN bij_converse_bij, of γ A] bij_is_surj
    by simp
  with cofinal(A,γ,Memrel(γ))
  have "aγ. a, f`0  Memrel(γ)  a = f`0"
    unfolding cofinal_def surj_def
    by auto
  with assms A  γ f  surj(1,A)
  show "α. Ord(α)  γ  = succ(α)"
    using Ord_has_max_imp_succ[of γ "f`0"]
      surj_is_fun[of f 1 A] apply_type[of f 1 "λ_.A" 0]
    unfolding lt_def
    by (auto intro:Ord_in_Ord)
qed

lemma ordertype_in_cf_imp_not_cofinal:
  assumes
    "ordertype(A,Memrel(γ))  cf(γ)"
    "A  γ"
  shows
    "¬ cofinal(A,γ,Memrel(γ))"
proof
  note A  γ
  moreover
  assume "cofinal(A,γ,Memrel(γ))"
  ultimately
  have "B. B  γ  cofinal(B, γ, Memrel(γ))   ordertype(A,Memrel(γ)) = ordertype(B, Memrel(γ))"
    (is "?P(ordertype(A,_))")
    by blast
  moreover from assms
  have "ordertype(A,Memrel(γ)) < cf(γ)"
    using Ord_cf ltI by blast
  ultimately
  show "False"
    unfolding cf_def using less_LeastE[of ?P  "ordertype(A,Memrel(γ))"]
    by auto
qed

lemma cofinal_mono_map_cf:
  assumes "Ord(γ)"
  shows "j  mono_map(cf(γ), Memrel(cf(γ)), γ, Memrel(γ)) . cf_fun(j,γ)"
proof -
  note assms
  moreover from this
  obtain A where "A  γ" "cf(γ) = ordertype(A,Memrel(γ))"
    "cofinal(A,γ,Memrel(γ))"
    using cf_is_ordertype by blast
  moreover
  define j where "j  converse(ordermap(A,Memrel(γ)))"
  moreover from calculation
  have "j :cf(γ) < γ"
    using ordertype_ord_iso[THEN ord_iso_sym,
        THEN ord_iso_is_mono_map, THEN mono_map_mono,
        of A "Memrel(γ)" γ] well_ord_Memrel[THEN well_ord_subset]
    by simp
  moreover from calculation
  have "j  surj(cf(γ),A)"
    using well_ord_Memrel[THEN well_ord_subset, THEN ordertype_ord_iso,
        THEN ord_iso_sym, of γ A, THEN ord_iso_is_bij,
        THEN bij_is_surj]
    by simp
  with cofinal(A,γ,Memrel(γ))
  have "cf_fun(j,γ)"
    using cofinal_range_iff_cofinal_fun[of j γ "Memrel(γ)"]
      surj_range[of j "cf(γ)" A] surj_is_fun fun_is_function
    by fastforce
  with j  mono_map(_,_,_,_)
  show ?thesis by auto
qed


subsection‹The factorization lemma›

text‹In this subsection we prove a factorization lemma for cofinal functions
into ordinals, which shows that any cofinal function between ordinals can be
``decomposed'' in such a way that a commutative triangle of strictly increasing
maps arises.

The factorization lemma has a kind of
fundamental character, in that the rest of the basic results on cofinality
(for, instance, idempotence) follow easily from it, in a more algebraic way.

This is a consequence that the proof encapsulates uses of transfinite
recursion in the basic theory of cofinality; indeed, only one use is needed.
In the setting of Isabelle/ZF, this is convenient since the machinery of
recursion is pretty clumsy. On the downside, this way of presenting things 
results in a longer proof of the factorization lemma. This approach was
taken by the author in the notes cite"apunte_st" for an introductory course
in Set Theory.

To organize the use of the hypotheses of the factorization lemma,
we set up a locale containing all the relevant ingredients.
›
locale cofinal_factor =
  fixes j δ ξ γ f
  assumes j_mono: "j :ξ < γ"
    and     ords: "Ord(δ)" "Ord(ξ)" "Limit(γ)"
    and   f_type: "f: δ  γ"
begin

text‹Here, termf is cofinal function from termδ to termγ, and the
ordinal termξ is meant to be the cofinality of termγ. Hence, there exists
an increasing map termj from  termξ to  termγ by the last lemma.

The main goal is to construct an increasing function termg:ξδ such that
the composition termf O g is still cofinal but also increasing.›

definition
  factor_body :: "[i,i,i]  o" where
  "factor_body(β,h,x)  (xδ  j`β  f`x  (α<β . f`(h`α) < f`x))  x=δ"

definition
  factor_rec :: "[i,i]  i" where
  "factor_rec(β,h)   μ x. factor_body(β,h,x)"

texttermfactor_rec is the inductive step for the definition by transfinite
recursion of the ‹factor› function (called termg above), which in
turn is obtained by minimizing the predicate termfactor_body. Next we show
that this predicate is monotonous.›

lemma factor_body_mono:
  assumes
    "βξ" "α<β"
    "factor_body(β,λxβ. G(x),x)"
  shows
    "factor_body(α,λxα. G(x),x)"
proof -
  from α<β
  have "αβ" using ltD by simp
  moreover
  note βξ
  moreover from calculation
  have "αξ" using ords ltD Ord_cf Ord_trans by blast
  ultimately
  have "j`α  j`β" using j_mono mono_map_increasing by blast
  moreover from βξ
  have "j`βγ"
    using j_mono domain_of_fun apply_rangeI mono_map_is_fun by force
  moreover from this
  have "Ord(j`β)"
    using Ord_in_Ord ords Limit_is_Ord by auto
  ultimately
  have "j`α  j`β"  unfolding lt_def by blast
  then
  have "j`β  f`θ  j`α  f`θ" for θ using le_trans by blast
  moreover
  have "f`((λwα. G(w))`y) < f`z" if "zδ" "x<β. f`((λwβ. G(w))`x) < f`z" "y<α" for y z
  proof -
    note y<α
    also
    note α<β
    finally
    have "y<β" by simp
    with x<β. f`((λwβ. G(w))`x) < f`z
    have "f ` ((λwβ. G(w)) ` y) < f ` z" by simp
    moreover from y<α y<β
    have "(λwβ. G(w)) ` y = (λwα. G(w)) ` y"
      using beta_if  by (auto dest:ltD)
    ultimately show ?thesis by simp
  qed
  moreover
  note factor_body(β,λxβ. G(x),x)
  ultimately
  show ?thesis
    unfolding factor_body_def by blast
qed

lemma factor_body_simp[simp]: "factor_body(α,g,δ)"
  unfolding factor_body_def by simp

lemma factor_rec_mono:
  assumes
    "βξ" "α<β"
  shows
    "factor_rec(α,λxα. G(x))  factor_rec(β,λxβ. G(x))"
  unfolding factor_rec_def
  using assms ords factor_body_mono Least_antitone by simp

text‹We now define the factor as higher-order function.
Later it will be restricted to a set to obtain a bona fide function of
type @{typ i}.›
definition
  factor :: "i  i" where
  "factor(β)  transrec(β,factor_rec)"

lemma factor_unfold:
  "factor(α) = factor_rec(α,λxα. factor(x))"
  using def_transrec[OF factor_def] .

lemma factor_mono:
  assumes "βξ" "α<β" "factor(α)δ" "factor(β)δ"
  shows "factor(α)  factor(β)"
proof -
  have "factor(α) = factor_rec(α, λxα. factor(x))"
    using factor_unfold .
  also from assms and factor_rec_mono
  have "...  factor_rec(β, λxβ. factor(x))"
    by simp
  also
  have "factor_rec(β, λxβ. factor(x)) = factor(β)"
    using def_transrec[OF factor_def, symmetric] .
  finally show ?thesis .
qed

text‹The factor satisfies the predicate body of the minimization.›

lemma factor_body_factor:
  "factor_body(α,λxα. factor(x),factor(α))"
  using ords factor_unfold[of α]
    LeastI[of "factor_body(_,_)" δ]
  unfolding factor_rec_def by simp

lemma factor_type [TC]: "Ord(factor(α))"
  using ords factor_unfold[of α]
  unfolding factor_rec_def by simp

text‹The value termδ in termfactor_body (and therefore, in
termfactor) is meant to be a ``default value''. Whenever it is not 
attained, the factor function behaves as expected: It is increasing
and its composition with termf also is.›

lemma f_factor_increasing:
  assumes "βξ" "α<β" "factor(β)δ"
  shows "f`factor(α) < f`factor(β)"
proof -
  from assms
  have "f ` ((λxβ. factor(x)) ` α) < f ` factor(β)"
    using factor_unfold[of β] ords LeastI[of "factor_body(β,λxβ. factor(x))"]
    unfolding factor_rec_def factor_body_def
    by (auto simp del:beta_if)
  with α<β
  show ?thesis using ltD by auto
qed

lemma factor_increasing:
  assumes "βξ" "α<β" "factor(α)δ" "factor(β)δ"
  shows "factor(α)<factor(β)"
  using assms f_factor_increasing factor_mono by (force intro:le_neq_imp_lt)

lemma factor_in_delta:
  assumes "factor(β)  δ"
  shows "factor(β)  δ"
  using assms factor_body_factor ords
  unfolding factor_body_def by auto

text‹Finally, we define the (set) factor function as the restriction of
factor to the ordinal  termξ.›

definition
  fun_factor :: "i" where
  "fun_factor  λβξ. factor(β)"

lemma fun_factor_is_mono_map:
  assumes "β. β  ξ  factor(β)  δ"
  shows "fun_factor  mono_map(ξ, Memrel(ξ), δ, Memrel(δ))"
  unfolding mono_map_def
proof (intro CollectI ballI impI)
  text‹Proof that termfun_factor respects membership:›
  fix α β
  assume "αξ" "βξ"
  moreover
  note assms
  moreover from calculation
  have "factor(α)δ" "factor(β)δ" "Ord(β)"
    using factor_in_delta Ord_in_Ord ords by auto
  moreover
  assume "α, β  Memrel(ξ)"
  ultimately
  show "fun_factor ` α, fun_factor ` β  Memrel(δ)"
    unfolding fun_factor_def
    using ltI factor_increasing[THEN ltD] factor_in_delta
    by simp
next
  text‹Proof that it has the appropriate type:›
  from assms
  show "fun_factor : ξ  δ"
    unfolding fun_factor_def
    using ltI lam_type factor_in_delta by simp
qed

lemma f_fun_factor_is_mono_map:
  assumes "β. β  ξ  factor(β)  δ"
  shows "f O fun_factor  mono_map(ξ, Memrel(ξ), γ, Memrel(γ))"
  unfolding mono_map_def
  using f_type
proof (intro CollectI ballI impI comp_fun[of _ _ δ])
  from assms
  show "fun_factor : ξ  δ"
    using fun_factor_is_mono_map mono_map_is_fun by simp
  text‹Proof that termf O fun_factor respects membership›
  fix α β
  assume "α, β  Memrel(ξ)"
  then
  have "α<β"
    using Ord_in_Ord[of "ξ"] ltI ords by blast
  assume "αξ" "βξ"
  moreover from this and assms
  have "factor(α)δ" "factor(β)δ" by auto
  moreover
  have "Ord(γ)" "γ0" using ords Limit_is_Ord by auto
  moreover
  note α<β fun_factor : ξ  δ
  ultimately
  show "(f O fun_factor) ` α, (f O fun_factor) ` β  Memrel(γ)"
    using ltD[of "f ` factor(α)" "f ` factor(β)"]
      f_factor_increasing apply_in_codomain_Ord f_type
    unfolding fun_factor_def by auto
qed

end ― ‹localecofinal_factor

text‹We state next the factorization lemma.›

lemma cofinal_fun_factorization:
  notes le_imp_subset [dest] lt_trans2 [trans]
  assumes
    "Ord(δ)" "Limit(γ)" "f: δ  γ" "cf_fun(f,γ)"
  shows
    "g  cf(γ) < δ.  f O g : cf(γ) < γ 
           cofinal_fun(f O g,γ,Memrel(γ))"
proof -
  from Limit(γ)
  have "Ord(γ)" using Limit_is_Ord by simp
  then
  obtain j where "j :cf(γ) < γ" "cf_fun(j,γ)"
    using cofinal_mono_map_cf by blast
  then
  have "domain(j) = cf(γ)"
    using domain_of_fun mono_map_is_fun by force
  from j  _ assms
  interpret cofinal_factor j δ "cf(γ)"
    by (unfold_locales) (simp_all)
  text‹The core of the argument is to show that the factor function
  indeed maps into termδ, therefore its values satisfy the first
  disjunct of termfactor_body. This holds in turn because no
  restriction of the factor composed with termf to a proper initial
  segment of termcf(γ) can be cofinal in termγ by definition of
  cofinality. Hence there must be a witness that satisfies the first
  disjunct.›
  have factor_not_delta: "factor(β)δ" if "β  cf(γ)" for β
    text‹For this, we induct on termβ ranging over termcf(γ).›
  proof (induct β rule:Ord_induct[OF _ Ord_cf[of γ]])
    case 1 with that show ?case .
  next
    case (2 β)
    then
    have IH: "zβ  factor(z)δ" for z by simp
    define h where "h  λxβ. f`factor(x)"
    from IH
    have "zβ  factor(z)  δ" for z
      using factor_in_delta by blast
    with f:δγ
    have "h : β  γ" unfolding h_def using apply_funtype lam_type by auto
    then
    have "h : β < γ"
      unfolding mono_map_def
    proof (intro CollectI ballI impI)
      fix x y
      assume "xβ" "yβ"
      moreover from this and IH
      have "factor(y)  δ" by simp
      moreover from calculation and h  β  γ
      have "h`x  γ" "h`y  γ" by simp_all
      moreover from βcf(γ) and yβ
      have "y  cf(γ)"
        using Ord_trans Ord_cf by blast
      moreover from this
      have "Ord(y)"
        using Ord_cf Ord_in_Ord by blast
      moreover
      assume "x,y  Memrel(β)"
      moreover from calculation
      have "x<y" by (blast intro:ltI)
      ultimately
      show "h ` x, h ` y  Memrel(γ)"
        unfolding h_def using f_factor_increasing ltD by (auto)
    qed
    with βcf(γ) Ord(γ)
    have "ordertype(h``β,Memrel(γ)) = β" (* Maybe should use range(h) *)
      using mono_map_ordertype_image[of β] Ord_cf Ord_in_Ord by blast
    also
    note β cf(γ)
    finally
    have "ordertype(h``β,Memrel(γ))  cf(γ)" by simp
    moreover from h  β  γ
    have "h``β  γ"
      using mono_map_is_fun Image_sub_codomain by blast
    ultimately
    have "¬ cofinal(h``β,γ,Memrel(γ))"
      using ordertype_in_cf_imp_not_cofinal by simp
    then
    obtain α_0 where "α_0γ" "xh `` β. ¬ α_0, x  Memrel(γ)  α_0  x"
      unfolding cofinal_def by auto
    with Ord(γ) h``β  γ
    have "xh `` β. x  α_0"
      using well_ord_Memrel[of γ] well_ord_is_linear[of γ "Memrel(γ)"]
      unfolding linear_def by blast
    from α_0  γ j  mono_map(_,_,γ,_) Ord(γ)
    have "j`β  γ"
      using mono_map_is_fun apply_in_codomain_Ord by force
    with α_0  γ Ord(γ)
    have "α_0  j`β  γ"
      using Un_least_mem_iff Ord_in_Ord by auto
    with cf_fun(f,γ)
    obtain θ where "θdomain(f)" "α_0  j`β, f ` θ  Memrel(γ)   α_0  j`β = f ` θ"
      by (auto simp add:cofinal_fun_def) blast
    moreover from this and f:δγ
    have "θ  δ" using domain_of_fun by auto
    moreover
    note Ord(γ)
    moreover from this and f:δγ  α_0  γ
    have "Ord(f`θ)"
      using apply_in_codomain_Ord Ord_in_Ord by blast
    moreover from calculation and α_0  γ and Ord(δ) and j`β  γ
    have "Ord(α_0)" "Ord(j`β)" "Ord(θ)"
      using Ord_in_Ord by auto
    moreover from xh `` β. x  α_0 Ord(α_0) h:βγ
    have "xβ  h`x < α_0" for x
      using fun_is_function[of h β "λ_. γ"]
        Image_subset_Ord_imp_lt domain_of_fun[of h β "λ_. γ"]
      by blast
    moreover
    have "xβ  h`x < f`θ" for x
    proof -
      fix x
      assume "xβ"
      with xh `` β. x  α_0 Ord(α_0) h:βγ
      have "h`x < α_0"
        using fun_is_function[of h β "λ_. γ"]
          Image_subset_Ord_imp_lt domain_of_fun[of h β "λ_. γ"]
        by blast
      also from α_0  _, f ` θ  Memrel(γ)  α_0  _= f ` θ
        Ord(f`θ) Ord(α_0) Ord(j`β)
      have "α_0  f`θ"
        using Un_leD1[OF leI [OF ltI]] Un_leD1[OF le_eqI] by blast
      finally
      show "h`x < f`θ" .
    qed
    ultimately
    have "factor_body(β,λxβ. factor(x),θ)"
      unfolding h_def factor_body_def using ltD
      by (auto dest:Un_memD2 Un_leD2[OF le_eqI])
    with Ord(θ)
    have "factor(β)  θ"
      using factor_unfold[of β] Least_le unfolding factor_rec_def by auto
    with θδ Ord(δ)
    have "factor(β)  δ"
      using leI[of θ] ltI[of θ]  by (auto dest:ltD)
    then
    show ?case by (auto elim:mem_irrefl)
  qed
  moreover
  have "cofinal_fun(f O fun_factor, γ, Memrel(γ))"
  proof (intro cofinal_funI)
    fix a
    assume "a  γ"
    with cf_fun(j,γ) domain(j) = cf(γ)
    obtain x where "xcf(γ)" "a  j`x  a = j`x"
      by (auto simp add:cofinal_fun_def) blast
    with factor_not_delta
    have "x  domain(f O fun_factor)"
      using f_fun_factor_is_mono_map mono_map_is_fun domain_of_fun by force
    moreover
    have "a  (f O fun_factor) `x  a = (f O fun_factor) `x"
    proof -
      from xcf(γ) factor_not_delta
      have "j ` x  f ` factor(x)"
        using mem_not_refl factor_body_factor factor_in_delta
        unfolding factor_body_def by auto
      with a  j`x  a = j`x
      have "a  f ` factor(x)  a = f ` factor(x)"
        using ltD by blast
      with xcf(γ)
      show ?thesis using lam_funtype[of "cf(γ)" factor]
        unfolding fun_factor_def by auto
    qed
    moreover
    note a  γ
    moreover from calculation and Ord(γ) and factor_not_delta
    have "(f O fun_factor) `x  γ"
      using Limit_nonzero apply_in_codomain_Ord mono_map_is_fun[of "f O fun_factor"]
        f_fun_factor_is_mono_map by blast
    ultimately
    show "x  domain(f O fun_factor). a, (f O fun_factor) ` x  Memrel(γ)
                                        a = (f O fun_factor) `x"
      by blast
  qed
  ultimately
  show ?thesis
    using fun_factor_is_mono_map f_fun_factor_is_mono_map by blast
qed

text‹As a final observation in this part, we note that if the original
cofinal map was increasing, then the factor function is also cofinal.›
lemma factor_is_cofinal:
  assumes
    "Ord(δ)" "Ord(γ)"
    "f :δ < γ"  "f O g  mono_map(α,r,γ,Memrel(γ))"
    "cofinal_fun(f O g,γ,Memrel(γ))" "g: α  δ"
  shows
    "cf_fun(g,δ)"
  unfolding cf_fun_def cofinal_fun_def
proof
  fix a
  assume "a  δ"
  with f  mono_map(δ,_,γ,_)
  have "f`a  γ"
    using mono_map_is_fun by force
  with cofinal_fun(f O g,γ,_)
  obtain y where "yα"  "f`a, (f O g) ` y  Memrel(γ)  f`a = (f O g) ` y"
    unfolding cofinal_fun_def using domain_of_fun[OF g:α  δ] by blast
  with g:α  δ
  have "f`a, f ` (g ` y)  Memrel(γ)  f`a = f ` (g ` y)" "g`y  δ"
    using comp_fun_apply[of g α δ y f] by auto
  with assms(1-3) and aδ
  have "a, g ` y  Memrel(δ)  a = g ` y"
    using Memrel_mono_map_reflects Memrel_mono_map_is_inj[of δ f γ γ]
      inj_apply_equality[of f δ γ]  by blast
  with yα
  show "xdomain(g). a, g ` x  Memrel(δ)  a = g ` x"
    using domain_of_fun[OF g:α  δ] by blast
qed


subsection‹Classical results on cofinalities›

text‹Now the rest of the results follow in a more algebraic way. The
next proof one invokes a case analysis on whether the argument is zero,
a successor ordinal or a limit one; the last case being the most
relevant one and is immediate from the factorization lemma.›

lemma cf_le_domain_cofinal_fun:
  assumes
    "Ord(γ)" "Ord(δ)" "f:δ  γ" "cf_fun(f,γ)"
  shows
    "cf(γ)δ"
  using assms
proof (cases rule:Ord_cases)
  case 0
  with Ord(δ)
  show ?thesis using Ord_0_le by simp
next
  case (succ γ)
  with assms
  obtain x where "xδ" "f`x=γ" using cf_fun_succ' by blast
  then
  have "δ0" by blast
  let ?f="{0,f`x}"
  from f`x=γ
  have "?f:1succ(γ)"
    using singleton_0 singleton_fun[of 0 γ] singleton_subsetI fun_weaken_type by simp
  with Ord(γ)  f`x=γ
  have "cf(succ(γ)) = 1" using cf_succ by simp
  with δ0 succ
  show ?thesis using Ord_0_lt_iff succ_leI Ord(δ) by simp
next
  case (limit)
  with assms
  obtain g where "g :cf(γ) < δ"
    using cofinal_fun_factorization by blast
  with assms
  show ?thesis using mono_map_imp_le by simp
qed

lemma cf_ordertype_cofinal:
  assumes
    "Limit(γ)" "Aγ" "cofinal(A,γ,Memrel(γ))"
  shows
    "cf(γ) = cf(ordertype(A,Memrel(γ)))"
proof (intro le_anti_sym)
  text‹We show the result by proving the two inequalities.›
  from Limit(γ)
  have "Ord(γ)"
    using Limit_is_Ord by simp
  with A  γ
  have "well_ord(A,Memrel(γ))"
    using well_ord_Memrel well_ord_subset by blast
  then
  obtain f α where "f:α, Memrel(α)  A,Memrel(γ)" "Ord(α)" "α = ordertype(A,Memrel(γ))"
    using ordertype_ord_iso Ord_ordertype ord_iso_sym by blast
  moreover from this
  have "f: α  A"
    using ord_iso_is_mono_map mono_map_is_fun[of f _ "Memrel(α)"] by blast
  moreover from this
  have "function(f)"
    using fun_is_function by simp
  moreover from f:α, Memrel(α)  A,Memrel(γ)
  have "range(f) = A"
    using ord_iso_is_bij bij_is_surj surj_range by blast
  moreover note cofinal(A,γ,_)
  ultimately
  have "cf_fun(f,γ)"
    using cofinal_range_iff_cofinal_fun by blast
  moreover from Ord(α)
  obtain h where "h :cf(α) < α" "cf_fun(h,α)"
    using cofinal_mono_map_cf by blast
  moreover from Ord(γ)
  have "trans(Memrel(γ))"
    using trans_Memrel by simp
  moreover
  note Aγ
  ultimately
  have "cofinal_fun(f O h,γ,Memrel(γ))"
    using cofinal_comp ord_iso_is_mono_map[OF f:α,_  A,_] mono_map_is_fun
      mono_map_mono by blast
  moreover from f:αA Aγ hmono_map(cf(α),_,α,_)
  have "f O h : cf(α)  γ"
    using Pi_mono[of A γ] comp_fun  mono_map_is_fun by blast
  moreover
  note Ord(γ) Ord(α) α = ordertype(A,Memrel(γ))
  ultimately
  show "cf(γ)  cf(ordertype(A,Memrel(γ)))"
    using cf_le_domain_cofinal_fun[of _ _ "f O h"]
    by (auto simp add:cf_fun_def)
  text‹That finishes the first inequality. Now we go the other side.›
  from f:α, _  A,_ Aγ
  have "f :α < γ"
    using mono_map_mono[OF ord_iso_is_mono_map] by simp
  then
  have "f: α  γ"
    using mono_map_is_fun by simp
  with cf_fun(f,γ) Limit(γ) Ord(α)
  obtain g where "g :cf(γ) < α"
    "f O g :cf(γ) < γ"
    "cofinal_fun(f O g,γ,Memrel(γ))"
    using cofinal_fun_factorization by blast
  moreover from this
  have "g:cf(γ)α"
    using mono_map_is_fun by simp
  moreover
  note Ord(α)
  moreover from calculation and f :α < γ Ord(γ)
  have "cf_fun(g,α)"
    using factor_is_cofinal by blast
  moreover
  note α = ordertype(A,Memrel(γ))
  ultimately
  show "cf(ordertype(A,Memrel(γ)))  cf(γ)"
    using cf_le_domain_cofinal_fun[OF _ Ord_cf mono_map_is_fun] by simp
qed

lemma cf_idemp:
  assumes "Limit(γ)"
  shows "cf(γ) = cf(cf(γ))"
proof -
  from assms
  obtain A where "Aγ" "cofinal(A,γ,Memrel(γ))" "cf(γ) = ordertype(A,Memrel(γ))"
    using Limit_is_Ord cf_is_ordertype by blast
  with assms
  have "cf(γ) = cf(ordertype(A,Memrel(γ)))" using cf_ordertype_cofinal by simp
  also
  have "... = cf(cf(γ))"
    using cf(γ) = ordertype(A,Memrel(γ)) by simp
  finally
  show "cf(γ) = cf(cf(γ))"  .
qed

lemma cf_le_cardinal:
  assumes "Limit(γ)"
  shows "cf(γ)  |γ|"
proof -
  from assms
  have Ord(γ) using Limit_is_Ord by simp
  then
  obtain f where "f  surj(|γ|,γ)"
    using Ord_cardinal_eqpoll unfolding eqpoll_def bij_def by blast
  with Ord(γ)
  show ?thesis
    using Card_is_Ord[OF Card_cardinal] surj_is_cofinal
      cf_le_domain_cofinal_fun[of γ] surj_is_fun by blast
qed

lemma regular_is_Card:
  notes le_imp_subset [dest]
  assumes "Limit(γ)" "γ = cf(γ)"
  shows "Card(γ)"
proof -
  from assms
  have "|γ|  γ"
    using Limit_is_Ord Ord_cardinal_le by blast
  also from γ = cf(γ)
  have "γ  cf(γ)" by simp
  finally
  have "|γ|  cf(γ)" .
  with assms
  show ?thesis unfolding Card_def using cf_le_cardinal by force
qed

lemma Limit_cf: assumes "Limit(κ)" shows "Limit(cf(κ))"
  using Ord_cf[of κ, THEN Ord_cases]
    ― ‹termcf(κ) being $0$ or successor leads to contradiction›
proof (cases)
  case 1
  with Limit(κ)
  show ?thesis using cf_zero_iff Limit_is_Ord by simp
next
  case (2 α)
  moreover
  note Limit(κ)
  moreover from calculation
  have "cf(κ) = 1"
    using cf_idemp cf_succ by fastforce
  ultimately
  show ?thesis
    using succ_LimitE cf_eq_one_iff Limit_is_Ord
    by auto
qed

lemma InfCard_cf: "Limit(κ)  InfCard(cf(κ))"
  using regular_is_Card cf_idemp Limit_cf nat_le_Limit Limit_cf
  unfolding InfCard_def by simp

lemma cf_le_cf_fun:
  notes [dest] = Limit_is_Ord
  assumes "cf(κ)  ν" "Limit(κ)"
  shows "f.  f:ν  κ    cf_fun(f, κ)"
proof -
  note assms
  moreover from this
  obtain h where h_cofinal_mono: "cf_fun(h,κ)"
    "h :cf(κ) < κ"
    "h : cf(κ)  κ"
    using cofinal_mono_map_cf mono_map_is_fun by force
  moreover from calculation
  obtain g where "g  inj(cf(κ), ν)"
    using le_imp_lepoll by blast
  from this and calculation(2,3,5)
  obtain f where "f  surj(ν, cf(κ))" "f: ν  cf(κ)"
    using inj_imp_surj[OF _ Limit_has_0[THEN ltD]]
      surj_is_fun Limit_cf by blast
  moreover from this
  have "cf_fun(f,cf(κ))"
    using surj_is_cofinal by simp
  moreover
  note h_cofinal_mono Limit(κ)
  moreover from calculation
  have "cf_fun(h O f,κ)"
    using cf_fun_comp by blast
  moreover from calculation
  have "h O f  ν -> κ"
    using comp_fun by simp
  ultimately
  show ?thesis by blast
qed

lemma Limit_cofinal_fun_lt:
  notes [dest] = Limit_is_Ord
  assumes "Limit(κ)" "f: ν  κ" "cf_fun(f,κ)" "nκ"
  shows "αν. n < f`α"
proof -
  from Limit(κ) nκ
  have "succ(n)  κ"
    using Limit_has_succ[OF _ ltI, THEN ltD] by auto
  moreover
  note f: ν  _
  moreover from this
  have "domain(f) = ν"
    using domain_of_fun by simp
  moreover
  note cf_fun(f,κ)
  ultimately
  obtain α where "α  ν" "succ(n)  f`α  succ(n) = f `α"
    using cf_funD[THEN cofinal_funD] by blast
  moreover from this
  consider (1) "succ(n)  f`α" | (2) "succ(n) = f `α"
    by blast
  then
  have "n < f`α"
  proof (cases)
    case 1
    moreover
    have "n  succ(n)" by simp
    moreover
    note Limit(κ) f: ν  _ α  ν
    moreover from this
    have "Ord(f ` α)"
      using apply_type[of f ν "λ_. κ", THEN [2] Ord_in_Ord]
      by blast
    ultimately
    show ?thesis
      using Ord_trans[of n "succ(n)" "f ` α"] ltI  by blast
  next
    case 2
    have "n  f ` α" by (simp add:2[symmetric])
    with Limit(κ) f: ν  _ α  ν
    show ?thesis
      using ltI
        apply_type[of f ν "λ_. κ", THEN [2] Ord_in_Ord]
      by blast
  qed
  ultimately
  show ?thesis by blast
qed

context
  includes Ord_dests Aleph_dests Aleph_intros Aleph_mem_dests mono_map_rules
begin

text‹We end this section by calculating the cofinality of Alephs, for
the zero and limit case. The successor case depends on $\AC$.›

lemma cf_nat: "cf(ω) = ω"
  using Limit_nat[THEN InfCard_cf] cf_le_cardinal[of ω]
    Card_nat[THEN Card_cardinal_eq] le_anti_sym
  unfolding InfCard_def by auto

lemma cf_Aleph_zero: "cf(ℵ⇘0) = ℵ⇘0⇙" 
  using cf_nat unfolding Aleph_def by simp

lemma cf_Aleph_Limit:
  assumes "Limit(γ)"
  shows "cf(ℵ⇘γ) = cf(γ)" 
proof -
  note Limit(γ)
  moreover from this
  have "(λxγ. ℵ⇘x) : γ  ℵ⇘γ⇙" (is "?f : _  _")
    using lam_funtype[of _ Aleph] fun_weaken_type[of _ _ _ "ℵ⇘γ⇙"] by blast
  moreover from Limit(γ)
  have "x  y  ℵ⇘x ℵ⇘y⇙" if "x  γ" "y  γ" for x y
    using that Ord_in_Ord[of γ] Ord_trans[of _ _ γ] by blast
  ultimately
  have "?f  mono_map(γ,Memrel(γ),ℵ⇘γ, Memrel(ℵ⇘γ))"
    by auto
  with  Limit(γ) 
  have "?f  γ, Memrel(γ)  ?f``γ, Memrel(ℵ⇘γ)"
    using mono_map_imp_ord_iso_Memrel[of γ "ℵ⇘γ⇙" ?f] 
      Card_Aleph (* Already an intro rule, but need it explicitly *)
    by blast
  then
  have "converse(?f)  ?f``γ, Memrel(ℵ⇘γ)  γ, Memrel(γ)"
    using ord_iso_sym by simp
  with Limit(γ)
  have "ordertype(?f``γ, Memrel(ℵ⇘γ)) = γ"
    using ordertype_eq[OF _ well_ord_Memrel]
    ordertype_Memrel by auto
  moreover from Limit(γ)
  have "cofinal(?f``γ, ℵ⇘γ, Memrel(ℵ⇘γ))" 
    unfolding cofinal_def 
  proof (standard, intro ballI)
    fix a
    assume "aℵ⇘γ⇙" "ℵ⇘γ= (i<γ. ℵ⇘i)"
    moreover from this
    obtain i where "i<γ" "aℵ⇘i⇙"
      by auto
    moreover from this and Limit(γ)
    have "Ord(i)" using ltD Ord_in_Ord by blast
    moreover from Limit(γ) and calculation
    have "succ(i)  γ" using ltD by auto
    moreover from this and Ord(i)
    have "ℵ⇘i< ℵ⇘succ(i)⇙" 
      by (auto) 
    ultimately
    have "a,ℵ⇘i  Memrel(ℵ⇘γ)"
      using ltD by (auto dest:Aleph_increasing)
    moreover from i<γ
    have "ℵ⇘i ?f``γ" 
      using ltD apply_in_image[OF ?f : _  _] by auto
    ultimately
    show "x?f `` γ. a, x  Memrel(ℵ⇘γ)  a = x" by blast
  qed
  moreover
  note ?f: γ  ℵ⇘γ⇙› Limit(γ)
  ultimately
  show "cf(ℵ⇘γ) =  cf(γ)"
    using cf_ordertype_cofinal[OF Limit_Aleph Image_sub_codomain, of γ ?f γ γ ] 
      Limit_is_Ord by simp 
qed

end ― ‹includes›

end