Theory CardinalArith_Relative

section‹Relative, Choice-less Cardinal Arithmetic›

theory CardinalArith_Relative
  imports
    Cardinal_Relative

begin

relativize functional "rvimage" "rvimage_rel" external
relationalize "rvimage_rel" "is_rvimage"

definition
  csquare_lam :: "ii" where
  "csquare_lam(K)  λx,yK×K. x  y, x, y"

― ‹Can't do the next thing because split is a missing HOC›
(* relativize functional "csquare_lam" "csquare_lam_rel" *)
relativize_tm "⟨fst(x) ∪ snd(x), fst(x), snd(x)⟩" "is_csquare_lam_body"

definition
  is_csquare_lam :: "[io,i,i]o" where
  "is_csquare_lam(M,K,l)  K2[M]. cartprod(M,K,K,K2) 
        is_lambda(M,K2,is_csquare_lam_body(M),l)"

definition jump_cardinal_body :: "[i,i]  i" where
  "jump_cardinal_body(U,X) 
    {z . r  U, well_ord(X, r)  z = ordertype(X, r)}"

lemma jump_cardinal_body_char :
  "jump_cardinal_body(U,X) = {ordertype(X, r) . r  {rU . well_ord(X, r)}}"
  unfolding jump_cardinal_body_def
  by auto

― ‹We internalize the relativized version of this particular instance.›
definition jump_cardinal_body'  where
  "jump_cardinal_body'(x)  jump_cardinal_body(Pow(x×x),x)"

lemma (in M_cardinals) csquare_lam_closed[intro,simp]: "M(K)  M(csquare_lam(K))"
  using csquare_lam_replacement  unfolding csquare_lam_def
  by (rule lam_closed) (auto dest:transM)

locale M_pre_cardinal_arith = M_cardinals +
  assumes
    wfrec_pred_replacement:"M(A)  M(r) 
      wfrec_replacement(M, λx f z. z = f `` Order.pred(A, x, r), r)"

relativize_tm "∃x' y' x y. z = ⟨⟨x', y'⟩, x, y⟩ ∧ (⟨x', x⟩ ∈ r ∨ x' = x ∧ ⟨y', y⟩ ∈ s)"
  "is_rmultP"

relativize functional "rmult" "rmult_rel" external
relationalize "rmult_rel" "is_rmult"

lemma (in M_trivial) rmultP_abs [absolut]: " M(r); M(s); M(z)   is_rmultP(M,s,r,z) 
    (x' y' x y. z = x', y', x, y  (x', x  r  x' = x  y', y  s))"
  unfolding is_rmultP_def by (auto dest:transM)

definition
  is_csquare_rel :: "[io,i,i]o"  where
  "is_csquare_rel(M,K,cs)  K2[M]. la[M]. memK[M].
      rmKK[M]. rmKK2[M].
        cartprod(M,K,K,K2)  is_csquare_lam(M,K,la) 
        membership(M,K,memK)  is_rmult(M,K,memK,K,memK,rmKK) 
        is_rmult(M,K,memK,K2,rmKK,rmKK2)  is_rvimage(M,K2,la,rmKK2,cs)"

context M_basic
begin

lemma rvimage_abs[absolut]:
  assumes "M(A)" "M(f)" "M(r)" "M(z)"
  shows "is_rvimage(M,A,f,r,z)  z = rvimage(A,f,r)"
  using assms transM[OF _ M(A)]
  unfolding is_rvimage_def rvimage_def
  by auto

lemma rmult_abs [absolut]: " M(A); M(r); M(B); M(s); M(z)  
    is_rmult(M,A,r,B,s,z)  z=rmult(A,r,B,s)"
  using rmultP_abs transM[of _ "(A × B) × A × B"]
  unfolding is_rmultP_def is_rmult_def rmult_def
  by (auto del: iffI)

lemma csquare_lam_body_abs[absolut]: "M(x)  M(z) 
  is_csquare_lam_body(M,x,z)  z = <fst(x)  snd(x), fst(x), snd(x)>"
  unfolding is_csquare_lam_body_def by (simp add:absolut)

lemma csquare_lam_abs[absolut]: "M(K)  M(l) 
  is_csquare_lam(M,K,l)  l = (λxK×K. fst(x)  snd(x), fst(x), snd(x))"
  unfolding is_csquare_lam_def
  using lambda_abs2[of "K×K" "is_csquare_lam_body(M)"
      "λx. fst(x)  snd(x), fst(x), snd(x)"]
  unfolding Relation1_def by (simp add:absolut)

lemma csquare_lam_eq_lam:"csquare_lam(K) = (λzK×K. <fst(z)  snd(z), fst(z), snd(z)>)"
proof -
  have "(λx,yK × K. x  y, x, y)`z =
      (λzK×K. <fst(z)  snd(z), fst(z), snd(z)>)`z" if "zK×K" for z
    using that by auto
  then
  show ?thesis
    unfolding csquare_lam_def
    by simp
qed

end ― ‹localeM_basic

context M_pre_cardinal_arith
begin

lemma csquare_rel_closed[intro,simp]: "M(K)  M(csquare_rel(K))"
  using csquare_lam_replacement unfolding csquare_rel_def
  by (intro rvimage_closed lam_closed) (auto dest:transM)

lemma csquare_rel_abs[absolut]: " M(K); M(cs) 
     is_csquare_rel(M,K,cs)  cs = csquare_rel(K)"
  using csquare_lam_closed[unfolded csquare_lam_eq_lam]
  unfolding is_csquare_rel_def csquare_rel_def
  by (simp add:absolut csquare_lam_eq_lam[unfolded csquare_lam_def])

end ― ‹localeM_pre_cardinal_arith

subsection‹Discipline for termcsucc

relativize functional "csucc" "csucc_rel" external
relationalize "csucc_rel" "is_csucc"
synthesize "is_csucc" from_definition assuming "nonempty"
arity_theorem for "is_csucc_fm"

abbreviation
  csucc_r :: "[i,io]  i"  ('(_+')⇗_) where
  "csucc_r(x,M)  csucc_rel(M,x)"

abbreviation
  csucc_r_set :: "[i,i]  i"  ('(_+')⇗_) where
  "csucc_r_set(x,M)  csucc_rel(##M,x)"

context M_Perm
begin

rel_closed for "csucc"
  using Least_closed'[of "λ L. M(L)  Card⇗M⇖(L)  K < L"]
  unfolding csucc_rel_def
  by simp

is_iff_rel for "csucc"
  using least_abs'[of "λ L. M(L)  Card⇗M⇖(L)  K < L" res]
    is_Card_iff
  unfolding is_csucc_def csucc_rel_def
  by (simp add:absolut)

end ― ‹localeM_Perm

notation csucc_rel (csucc⇗_⇖'(_'))

context M_cardinals
begin

lemma Card_rel_Union [simp,intro,TC]:
  assumes A: "x. xA  Card⇗M⇖(x)" and
    types:"M(A)"
  shows "Card⇗M⇖((A))"
proof (rule Card_relI)
  show "Ord(A)" using A
    by (simp add: Card_rel_is_Ord types transM)
next
  fix j
  assume j: "j < A"
  moreover from this
  have "M(j)" unfolding lt_def by (auto simp add:types dest:transM)
  from j
  have "cA. j  c  Card⇗M⇖(c)" using A types
    unfolding lt_def
    by (simp)
  then
  obtain c where c: "cA" "j < c" "Card⇗M⇖(c)" "M(c)"
    using Card_rel_is_Ord types unfolding lt_def
    by (auto dest:transM)
  with M(j)
  have jls: "j ≺⇗Mc"
    by (simp add: lt_Card_rel_imp_lesspoll_rel types)
  { assume eqp: "j ≈⇗MA"
    have  "c ≲⇗MA" using c
      by (blast intro: subset_imp_lepoll_rel types)
    also from types M(j)
    have "... ≈⇗Mj"  by (rule_tac eqpoll_rel_sym [OF eqp]) (simp_all add:types)
    also have "... ≺⇗Mc"  by (rule jls)
    finally have "c ≺⇗Mc" by (simp_all add:M(c) M(j) types)
    with M(c)
    have False
      by (auto dest:lesspoll_rel_irrefl)
  } thus "¬ j ≈⇗MA" by blast
qed (simp_all add:types)

text‹We are not relativizing directly the results involving unions of
(ordinal) indexed families (namely, @{thm [source] Card_UN} and
@{thm [source] Card_OUN}, respectively) because of their higher order nature.›

lemma in_Card_imp_lesspoll: "[| Card⇗M⇖(K); b  K; M(K); M(b) |] ==> b ≺⇗MK"
  apply (unfold lesspoll_rel_def)
  apply (simp add: Card_rel_iff_initial)
  apply (fast intro!: le_imp_lepoll_rel ltI leI)
  done


subsection‹Cardinal addition›

text‹Note (Paulson): Could omit proving the algebraic laws for cardinal addition and
multiplication.  On finite cardinals these operations coincide with
addition and multiplication of natural numbers; on infinite cardinals they
coincide with union (maximum).  Either way we get most laws for free.›

subsubsection‹Cardinal addition is commutative›

lemma sum_commute_eqpoll_rel: "M(A)  M(B)  A+B ≈⇗MB+A"
proof (simp add: def_eqpoll_rel, rule rexI)
  show "(λzA+B. case(Inr,Inl,z))  bij(A+B, B+A)"
    by (auto intro: lam_bijective [where d = "case(Inr,Inl)"])
  assume "M(A)" "M(B)"
  then
  show "M(λzA + B. case(Inr, Inl, z))"
    using case_replacement1
    by (rule_tac lam_closed) (auto dest:transM)
qed

lemma cadd_rel_commute: "M(i)  M(j)  i ⊕⇗Mj = j ⊕⇗Mi"
  apply (unfold cadd_rel_def)
  apply (auto intro: sum_commute_eqpoll_rel [THEN cardinal_rel_cong])
  done

subsubsection‹Cardinal addition is associative›

lemma sum_assoc_eqpoll_rel: "M(A)  M(B)  M(C)  (A+B)+C ≈⇗MA+(B+C)"
  apply (simp add: def_eqpoll_rel)
  apply (rule rexI)
   apply (rule sum_assoc_bij)
  using case_replacement2
  by (rule_tac lam_closed) (auto dest:transM)

text‹Unconditional version requires AC›
lemma well_ord_cadd_rel_assoc:
  assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
    and
    types: "M(i)" "M(ri)" "M(j)" "M(rj)" "M(k)" "M(rk)"
  shows "(i ⊕⇗Mj) ⊕⇗Mk = i ⊕⇗M(j ⊕⇗Mk)"
proof (simp add: assms cadd_rel_def, rule cardinal_rel_cong)
  from types
  have "|i + j|⇗M+ k ≈⇗M(i + j) + k"
    by (auto intro!: sum_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel eqpoll_rel_refl well_ord_radd i j)
  also have "...  ≈⇗Mi + (j + k)"
    by (rule sum_assoc_eqpoll_rel) (simp_all add:types)
  also
  have "...  ≈⇗Mi + |j + k|⇗M⇖"
  proof (auto intro!: sum_eqpoll_rel_cong intro:eqpoll_rel_refl simp add:types)
    from types
    have "|j + k|⇗M⇖ ≈⇗Mj + k"
      using well_ord_cardinal_rel_eqpoll_rel[OF well_ord_radd, OF j k]
      by (simp)
    with types
    show "j + k ≈⇗M|j + k|⇗M⇖"
      using eqpoll_rel_sym by simp
  qed
  finally show "|i + j|⇗M+ k ≈⇗Mi + |j + k|⇗M⇖" by (simp_all add:types)
qed (simp_all add:types)


subsubsection‹0 is the identity for addition›

lemma case_id_eq: "xsum(A,B)  case(λz . z, λz. z ,x) = snd(x)"
  unfolding case_def cond_def by (auto simp:Inl_def Inr_def)

lemma lam_case_id: "(λz0 + A. case(λx. x, λy. y, z)) = (λz0 + A . snd(z))"
  using case_id_eq by simp

lemma sum_0_eqpoll_rel: "M(A)  0+A ≈⇗MA"
  apply (simp add:def_eqpoll_rel)
  apply (rule rexI)
   apply (rule bij_0_sum,subst lam_case_id)
  using lam_replacement_snd[unfolded lam_replacement_def]
  by (rule lam_closed)
    (auto simp add:case_def cond_def Inr_def dest:transM)

lemma cadd_rel_0 [simp]: "Card⇗M⇖(K)  M(K)  0 ⊕⇗MK = K"
  apply (simp add: cadd_rel_def)
  apply (simp add: sum_0_eqpoll_rel [THEN cardinal_rel_cong] Card_rel_cardinal_rel_eq)
  done

subsubsection‹Addition by another cardinal›

lemma sum_lepoll_rel_self: "M(A)  M(B)  A ≲⇗MA+B"
proof (simp add: def_lepoll_rel, rule rexI)
  show "(λxA. Inl (x))  inj(A, A + B)"
    by (simp add: inj_def)
  assume "M(A)" "M(B)"
  then
  show "M(λxA. Inl(x))"
    using Inl_replacement1 transM[OF _ M(A)]
    by (rule_tac lam_closed) (auto simp add: Inl_def)
qed

lemma cadd_rel_le_self:
  assumes K: "Card⇗M⇖(K)" and L: "Ord(L)" and
    types:"M(K)" "M(L)"
  shows "K  (K ⊕⇗ML)"
proof (simp add:types cadd_rel_def)
  have "K  |K|⇗M⇖"
    by (rule Card_rel_cardinal_rel_le [OF K]) (simp add:types)
  moreover have "|K|⇗M |K + L|⇗M⇖" using K L
    by (blast intro: well_ord_lepoll_rel_imp_cardinal_rel_le sum_lepoll_rel_self
        well_ord_radd well_ord_Memrel Card_rel_is_Ord types)
  ultimately show "K  |K + L|⇗M⇖"
    by (blast intro: le_trans)
qed

subsubsection‹Monotonicity of addition›

lemma sum_lepoll_rel_mono:
  "[| A ≲⇗MC;  B ≲⇗MD; M(A); M(B); M(C); M(D) |] ==> A + B ≲⇗MC + D"
  apply (simp add: def_lepoll_rel)
  apply (elim rexE)
  apply (rule_tac x = "λzA+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in rexI)
   apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) ` y))"
      in lam_injective)
    apply (typecheck add: inj_is_fun, auto)
  apply (rule_tac lam_closed, auto dest:transM intro:case_replacement4)
  done

lemma cadd_rel_le_mono:
  "[| K'  K;  L'  L;M(K');M(K);M(L');M(L) |] ==> (K' ⊕⇗ML')  (K ⊕⇗ML)"
  apply (unfold cadd_rel_def)
  apply (safe dest!: le_subset_iff [THEN iffD1])
  apply (rule well_ord_lepoll_rel_imp_cardinal_rel_le)
      apply (blast intro: well_ord_radd well_ord_Memrel)
     apply (auto intro: sum_lepoll_rel_mono subset_imp_lepoll_rel)
  done

subsubsection‹Addition of finite cardinals is "ordinary" addition›

lemma sum_succ_eqpoll_rel: "M(A)  M(B)  succ(A)+B ≈⇗Msucc(A+B)"
  apply (simp add:def_eqpoll_rel)
  apply (rule rexI)
   apply (rule_tac c = "%z. if z=Inl (A) then A+B else z"
      and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective)
      apply simp_all
      apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+
  apply(rule_tac lam_closed, auto dest:transM intro:if_then_range_replacement2)
  done

lemma cadd_succ_lemma:
  assumes "Ord(m)" "Ord(n)" and
    types: "M(m)" "M(n)"
  shows "succ(m) ⊕⇗Mn = |succ(m ⊕⇗Mn)|⇗M⇖"
  using types
proof (simp add: cadd_rel_def)
  have [intro]: "m + n ≈⇗M|m + n|⇗M⇖" using assms
    by (blast intro: eqpoll_rel_sym well_ord_cardinal_rel_eqpoll_rel well_ord_radd well_ord_Memrel)

  have "|succ(m) + n|⇗M= |succ(m + n)|⇗M⇖"
    by (rule sum_succ_eqpoll_rel [THEN cardinal_rel_cong]) (simp_all add:types)
  also have "... = |succ(|m + n|⇗M)|⇗M⇖"
    by (blast intro: succ_eqpoll_rel_cong cardinal_rel_cong types)
  finally show "|succ(m) + n|⇗M= |succ(|m + n|⇗M)|⇗M⇖" .
qed

lemma nat_cadd_rel_eq_add:
  assumes m: "m  nat" and [simp]: "n  nat" shows"m ⊕⇗Mn = m +ω n"
  using m
proof (induct m)
  case 0 thus ?case
    using transM[OF _ M_nat]
    by (auto simp add: nat_into_Card_rel)
next
  case (succ m) thus ?case
    using transM[OF _ M_nat]
    by (simp add: cadd_succ_lemma nat_into_Card_rel Card_rel_cardinal_rel_eq)
qed


subsection‹Cardinal multiplication›

subsubsection‹Cardinal multiplication is commutative›

lemma prod_commute_eqpoll_rel: "M(A)  M(B)  A*B ≈⇗MB*A"
  apply (simp add: def_eqpoll_rel)
  apply (rule rexI)
   apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective,
      auto)
  apply(rule_tac lam_closed, auto intro:swap_replacement dest:transM)
  done

lemma cmult_rel_commute: "M(i)  M(j)  i ⊗⇗Mj = j ⊗⇗Mi"
  apply (unfold cmult_rel_def)
  apply (rule prod_commute_eqpoll_rel [THEN cardinal_rel_cong], simp_all)
  done

subsubsection‹Cardinal multiplication is associative›

lemma prod_assoc_eqpoll_rel: "M(A)  M(B)  M(C)  (A*B)*C ≈⇗MA*(B*C)"
  apply (simp add: def_eqpoll_rel)
  apply (rule rexI)
   apply (rule prod_assoc_bij)
  apply(rule_tac lam_closed, auto intro:assoc_replacement dest:transM)
  done

text‹Unconditional version requires AC›
lemma well_ord_cmult_rel_assoc:
  assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
    and
    types: "M(i)" "M(ri)" "M(j)" "M(rj)" "M(k)" "M(rk)"
  shows "(i ⊗⇗Mj) ⊗⇗Mk = i ⊗⇗M(j ⊗⇗Mk)"
proof (simp add: assms cmult_rel_def, rule cardinal_rel_cong)
  have "|i * j|⇗M* k ≈⇗M(i * j) * k"
    by (auto intro!: prod_eqpoll_rel_cong
        well_ord_cardinal_rel_eqpoll_rel eqpoll_rel_refl
        well_ord_rmult i j simp add:types)
  also have "...  ≈⇗Mi * (j * k)"
    by (rule prod_assoc_eqpoll_rel, simp_all add:types)
  also have "...  ≈⇗Mi * |j * k|⇗M⇖"
    by (blast intro: prod_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel
        eqpoll_rel_refl well_ord_rmult j k eqpoll_rel_sym types)
  finally show "|i * j|⇗M* k ≈⇗Mi * |j * k|⇗M⇖" by (simp add:types)
qed (simp_all add:types)


subsubsection‹Cardinal multiplication distributes over addition›

lemma sum_prod_distrib_eqpoll_rel: "M(A)  M(B)  M(C)  (A+B)*C ≈⇗M(A*C)+(B*C)"
  apply (simp add: def_eqpoll_rel)
  apply (rule rexI)
   apply (rule sum_prod_distrib_bij)
  apply(rule_tac lam_closed, auto intro:case_replacement5 dest:transM)
  done

lemma well_ord_cadd_cmult_distrib:
  assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
    and
    types: "M(i)" "M(ri)" "M(j)" "M(rj)" "M(k)" "M(rk)"
  shows "(i ⊕⇗Mj) ⊗⇗Mk = (i ⊗⇗Mk) ⊕⇗M(j ⊗⇗Mk)"
proof (simp add: assms cadd_rel_def cmult_rel_def, rule cardinal_rel_cong)
  have "|i + j|⇗M* k ≈⇗M(i + j) * k"
    by (blast intro: prod_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel
        eqpoll_rel_refl well_ord_radd i j types)
  also have "...  ≈⇗Mi * k + j * k"
    by (rule sum_prod_distrib_eqpoll_rel) (simp_all add:types)
  also have "...  ≈⇗M|i * k|⇗M+ |j * k|⇗M⇖"
    by (blast intro: sum_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel
        well_ord_rmult i j k eqpoll_rel_sym types)
  finally show "|i + j|⇗M* k ≈⇗M|i * k|⇗M+ |j * k|⇗M⇖" by (simp add:types)
qed (simp_all add:types)


subsubsection‹Multiplication by 0 yields 0›

lemma prod_0_eqpoll_rel: "M(A)  0*A ≈⇗M0"
  apply (simp add: def_eqpoll_rel)
  apply (rule rexI)
   apply (rule lam_bijective, auto)
  done

lemma cmult_rel_0 [simp]: "M(i)  0 ⊗⇗Mi = 0"
  by (simp add: cmult_rel_def prod_0_eqpoll_rel [THEN cardinal_rel_cong])

subsubsection‹1 is the identity for multiplication›

lemma prod_singleton_eqpoll_rel: "M(x)  M(A)  {x}*A ≈⇗MA"
  apply (simp add: def_eqpoll_rel)
  apply (rule rexI)
   apply (rule singleton_prod_bij [THEN bij_converse_bij])
  apply (rule converse_closed)
  apply(rule_tac lam_closed, auto intro:prepend_replacement dest:transM)
  done

lemma cmult_rel_1 [simp]: "Card⇗M⇖(K)  M(K)  1 ⊗⇗MK = K"
  apply (simp add: cmult_rel_def succ_def)
  apply (simp add: prod_singleton_eqpoll_rel[THEN cardinal_rel_cong] Card_rel_cardinal_rel_eq)
  done

subsection‹Some inequalities for multiplication›

lemma prod_square_lepoll_rel: "M(A)  A ≲⇗MA*A"
  apply (simp add:def_lepoll_rel inj_def)
  apply (rule_tac x = "λxA. <x,x>" in rexI, simp)
  apply(rule_tac lam_closed, auto intro:id_replacement dest:transM)
  done

lemma cmult_rel_square_le: "Card⇗M⇖(K)  M(K)  K  K ⊗⇗MK"
  apply (unfold cmult_rel_def)
  apply (rule le_trans)
   apply (rule_tac [2] well_ord_lepoll_rel_imp_cardinal_rel_le)
       apply (rule_tac [3] prod_square_lepoll_rel)
       apply (simp add: le_refl Card_rel_is_Ord Card_rel_cardinal_rel_eq)
      apply (blast intro: well_ord_rmult well_ord_Memrel Card_rel_is_Ord)
     apply simp_all
  done

subsubsection‹Multiplication by a non-zero cardinal›

lemma prod_lepoll_rel_self: "b  B  M(b)  M(B)  M(A)  A ≲⇗MA*B"
  apply (simp add: def_lepoll_rel inj_def)
  apply (rule_tac x = "λxA. <x,b>" in rexI, simp)
  apply(rule_tac lam_closed, auto intro:pospend_replacement dest:transM)
  done

lemma cmult_rel_le_self:
  "[| Card⇗M⇖(K);  Ord(L);  0<L; M(K);M(L) |] ==> K  (K ⊗⇗ML)"
  apply (unfold cmult_rel_def)
  apply (rule le_trans [OF Card_rel_cardinal_rel_le well_ord_lepoll_rel_imp_cardinal_rel_le])
        apply assumption apply simp
      apply (blast intro: well_ord_rmult well_ord_Memrel Card_rel_is_Ord)
     apply (auto intro: prod_lepoll_rel_self ltD)
  done

subsubsection‹Monotonicity of multiplication›

lemma prod_lepoll_rel_mono:
  "[| A ≲⇗MC;  B ≲⇗MD; M(A); M(B); M(C); M(D)|] ==> A * B  ≲⇗MC * D"
  apply (simp add:def_lepoll_rel)
  apply (elim rexE)
  apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in rexI)
   apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>"
      in lam_injective)
    apply (typecheck add: inj_is_fun, auto)
  apply(rule_tac lam_closed, auto intro:prod_fun_replacement dest:transM)
  done

lemma cmult_rel_le_mono:
  "[| K'  K;  L'  L;M(K');M(K);M(L');M(L) |] ==> (K' ⊗⇗ML')  (K ⊗⇗ML)"
  apply (unfold cmult_rel_def)
  apply (safe dest!: le_subset_iff [THEN iffD1])
  apply (rule well_ord_lepoll_rel_imp_cardinal_rel_le)
      apply (blast intro: well_ord_rmult well_ord_Memrel)
     apply (auto intro: prod_lepoll_rel_mono subset_imp_lepoll_rel)
  done

subsection‹Multiplication of finite cardinals is "ordinary" multiplication›

lemma prod_succ_eqpoll_rel: "M(A)  M(B)  succ(A)*B ≈⇗MB + A*B"
  apply (simp add: def_eqpoll_rel)
  apply (rule rexI)
   apply (rule_tac c = "λp. if fst(p)=A then Inl (snd(p)) else Inr (p)"
      and d = "case (%y. <A,y>, %z. z)" in lam_bijective)
      apply safe
          apply (simp_all add: succI2 if_type mem_imp_not_eq)
  apply(rule_tac lam_closed, auto intro:Inl_replacement2 dest:transM)
  done

lemma cmult_rel_succ_lemma:
  "[| Ord(m);  Ord(n) ; M(m); M(n) |] ==> succ(m) ⊗⇗Mn = n ⊕⇗M(m ⊗⇗Mn)"
  apply (simp add: cmult_rel_def cadd_rel_def)
  apply (rule prod_succ_eqpoll_rel [THEN cardinal_rel_cong, THEN trans], simp_all)
  apply (rule cardinal_rel_cong [symmetric], simp_all)
  apply (rule sum_eqpoll_rel_cong [OF eqpoll_rel_refl well_ord_cardinal_rel_eqpoll_rel], assumption)
        apply (blast intro: well_ord_rmult well_ord_Memrel)
       apply simp_all
  done

lemma nat_cmult_rel_eq_mult: "[| m  nat;  n  nat |] ==> m ⊗⇗Mn = m#*n"
  using transM[OF _ M_nat]
  apply (induct_tac m)
   apply (simp_all add: cmult_rel_succ_lemma nat_cadd_rel_eq_add)
  done

lemma cmult_rel_2: "Card⇗M⇖(n)  M(n)  2 ⊗⇗Mn = n ⊕⇗Mn"
  by (simp add: cmult_rel_succ_lemma Card_rel_is_Ord cadd_rel_commute [of _ 0])

lemma sum_lepoll_rel_prod:
  assumes C: "2 ≲⇗MC" and
    types:"M(C)" "M(B)"
  shows "B+B ≲⇗MC*B"
proof -
  have "B+B ≲⇗M2*B"
    by (simp add: sum_eq_2_times types)
  also have "... ≲⇗MC*B"
    by (blast intro: prod_lepoll_rel_mono lepoll_rel_refl C types)
  finally show "B+B ≲⇗MC*B" by (simp_all add:types)
qed

lemma lepoll_imp_sum_lepoll_prod: "[| A ≲⇗MB; 2 ≲⇗MA; M(A) ;M(B) |] ==> A+B ≲⇗MA*B"
  by (blast intro: sum_lepoll_rel_mono sum_lepoll_rel_prod lepoll_rel_trans lepoll_rel_refl)

end ― ‹localeM_cardinals

subsection‹Infinite Cardinals are Limit Ordinals›

context M_pre_cardinal_arith
begin

lemma nat_cons_lepoll_rel: "nat ≲⇗MA  M(A)  M(u) ==> cons(u,A) ≲⇗MA"
  apply (simp add: def_lepoll_rel)
  apply (erule rexE)
  apply (rule_tac x =
      "λzcons (u,A).
             if z=u then f`0
             else if z  range (f) then f`succ (converse (f) `z) else z"
      in rexI)
   apply (rule_tac d =
      "%y. if y  range(f) then nat_case (u, %z. f`z, converse(f) `y)
                              else y"
      in lam_injective)
    apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun)
   apply (simp add: inj_is_fun [THEN apply_rangeI]
      inj_converse_fun [THEN apply_rangeI]
      inj_converse_fun [THEN apply_funtype])
proof -
  fix f
  assume "M(A)" "M(f)" "M(u)"
  then
  show "M(λzcons(u, A). if z = u then f ` 0 else if z  range(f) then f ` succ(converse(f) ` z) else z)"
    using if_then_range_replacement transM[OF _ M(A)]
    by (rule_tac lam_closed, auto)
qed

lemma nat_cons_eqpoll_rel: "nat ≲⇗MA ==> M(A)  M(u)  cons(u,A) ≈⇗MA"
  apply (erule nat_cons_lepoll_rel [THEN eqpoll_relI], assumption+)
    apply (rule subset_consI [THEN subset_imp_lepoll_rel], simp_all)
  done

lemma nat_succ_eqpoll_rel: "nat  A ==> M(A)  succ(A) ≈⇗MA"
  apply (unfold succ_def)
  apply (erule subset_imp_lepoll_rel [THEN nat_cons_eqpoll_rel], simp_all)
  done

lemma InfCard_rel_nat: "InfCard⇗M⇖(nat)"
  apply (simp add: InfCard_rel_def)
  apply (blast intro: Card_rel_nat Card_rel_is_Ord)
  done

lemma InfCard_rel_is_Card_rel: "M(K)  InfCard⇗M⇖(K)  Card⇗M⇖(K)"
  apply (simp add: InfCard_rel_def)
  done

lemma InfCard_rel_Un:
  "[| InfCard⇗M⇖(K);  Card⇗M⇖(L); M(K); M(L) |] ==> InfCard⇗M⇖(K  L)"
  apply (simp add: InfCard_rel_def)
  apply (simp add: Card_rel_Un Un_upper1_le [THEN [2] le_trans]  Card_rel_is_Ord)
  done

lemma InfCard_rel_is_Limit: "InfCard⇗M⇖(K) ==> M(K)  Limit(K)"
  apply (simp add: InfCard_rel_def)
  apply (erule conjE)
  apply (frule Card_rel_is_Ord, assumption)
  apply (rule ltI [THEN non_succ_LimitI])
    apply (erule le_imp_subset [THEN subsetD])
    apply (safe dest!: Limit_nat [THEN Limit_le_succD])
  apply (unfold Card_rel_def)
  apply (drule trans)
   apply (erule le_imp_subset [THEN nat_succ_eqpoll_rel, THEN cardinal_rel_cong], simp_all)
  apply (erule Ord_cardinal_rel_le [THEN lt_trans2, THEN lt_irrefl], assumption)
  apply (rule le_eqI) prefer 2
   apply (rule Ord_cardinal_rel, assumption+)
  done

end ― ‹localeM_pre_cardinal_arith

lemma (in M_ordertype) ordertype_abs[absolut]:
  assumes "wellordered(M,A,r)" "M(A)" "M(r)" "M(i)"
  shows "otype(M,A,r,i)  i = ordertype(A,r)"
proof -
  have eq:"j = k" if
    "g  A, r  j, Memrel(j)" "Ord(j)"
    "h  A, r  k, Memrel(k)" "Ord(k)"
  for j k g h
  proof -
    from that
    have "h O converse(g)  j, Memrel(j)  k, Memrel(k)"
      using ord_iso_sym ord_iso_trans by blast
    with Ord(j) Ord(k)
    show "j=k"
      using Ord_iso_implies_eq[of j k "h O converse(g)"]
      by simp
  qed
  have otypeE: " h . h  A, r  k, Memrel(k)" if "otype(M, A, r, k)" "M(k)" for k
  proof -
    note that assms
    moreover from this
    obtain h where "omap(M, A, r, h)" "M(h)"
      using that omap_exists[of A r] by auto
    moreover from calculation
    have "h  A, r  k, Memrel(k)"
      using that omap_ord_iso obase_equals by simp
    then
    show ?thesis ..
  qed
  show ?thesis
  proof(intro iffI)
    note assms
    moreover
    assume "otype(M, A, r, i)"
    moreover from calculation
    obtain f j where "M(f)" "Ord(j)" "f  A, r  j, Memrel(j)"
      using ordertype_exists[of A r] by auto
    ultimately
    show "i = ordertype(A, r)"
      using Ord_otype[OF _ well_ord_is_trans_on] eq[of f j _ i] ordertypes_are_absolute
        otypeE[of i]
      by auto
  next
    note assms
    moreover
    assume "i = ordertype(A, r)"
    moreover from calculation
    obtain j where "otype(M,A,r,j)" "M(j)"
      using otype_exists by auto
    ultimately
    show "otype(M, A, r, i)"
      using Ord_ordertype eq[of _ i _ j] Ord_otype[OF _ well_ord_is_trans_on]
        otypeE[of j] ordertype_ord_iso[of A r]
      by auto
  qed
qed

lemma (in M_ordertype) ordertype_closed[intro,simp]: " wellordered(M,A,r);M(A);M(r)  M(ordertype(A,r))"
  using ordertype_exists ordertypes_are_absolute by blast

― ‹This apparent duplication of definitions is needed because in sessionZF-Constructible
pairs are in their absolute version and this breaks the synthesis of formulas.›

relationalize "transitive_rel" "is_transitive" external
synthesize "is_transitive" from_definition assuming "nonempty"
arity_theorem for "is_transitive_fm"

lemma (in M_trivial) is_transitive_iff_transitive_rel:
  "M(A) M(r)  transitive_rel(M, A, r)  is_transitive(M,A, r)"
  unfolding transitive_rel_def is_transitive_def by simp

relationalize "linear_rel" "is_linear" external
synthesize "is_linear" from_definition assuming "nonempty"
arity_theorem for "is_linear_fm"
reldb_add relational "transitive_on" "transitive_rel"
reldb_add relational "linear_on" "linear_rel"
reldb_add functional "transitive_on" "transitive_rel"
reldb_add functional "linear_on" "linear_rel"

lemma (in M_trivial) is_linear_iff_linear_rel:
  "M(A) M(r)  is_linear(M,A, r)  linear_rel(M, A, r)"
  unfolding linear_rel_def is_linear_def by simp

relationalize "wellfounded_on" "is_wellfounded_on" external
synthesize "is_wellfounded_on" from_definition assuming "nonempty"
arity_theorem for "is_wellfounded_on_fm"

lemma (in M_trivial) is_wellfounded_on_iff_wellfounded_on:
  "M(A) M(r)  is_wellfounded_on(M,A, r)  wellfounded_on(M, A, r)"
  unfolding wellfounded_on_def is_wellfounded_on_def by simp

definition
  is_well_ord :: "[i=>o,i,i]=>o" where
  ― ‹linear and wellfounded on A›
  "is_well_ord(M,A,r) ==
        is_transitive(M,A,r)  is_linear(M,A,r)  is_wellfounded_on(M,A,r)"

lemma (in M_trivial) is_well_ord_iff_wellordered:
  "M(A) M(r)   is_well_ord(M,A, r)  wellordered(M, A, r)"
  using is_wellfounded_on_iff_wellfounded_on is_linear_iff_linear_rel
    is_transitive_iff_transitive_rel
  unfolding wellordered_def is_well_ord_def by simp

synthesize "is_well_ord" from_definition assuming "nonempty"
arity_theorem for "is_well_ord_fm"
reldb_add relational "well_ord" "is_well_ord"
reldb_add functional "well_ord" "well_ord"

― ‹One keyword (functional or relational) means going
    from an absolute term to that kind of term›
reldb_add relational "Order.pred" "pred_set"

― ‹The following form (twice the same argument) is only correct
    when an "\_abs" theorem is available›
reldb_add functional "Order.pred" "Order.pred"


― ‹Two keywords denote origin and destination, respectively›
(*
reldb_add functional relational "Ord" "ordinal"
*)

relativize functional "ord_iso" "ord_iso_rel" external
― ‹The following corresponds to "relativize functional relational"›
relationalize "ord_iso_rel" "is_ord_iso"

context M_pre_cardinal_arith
begin

is_iff_rel for "ord_iso"
  using bij_rel_iff
  unfolding is_ord_iso_def ord_iso_rel_def
  by simp

rel_closed for "ord_iso"
  using ord_iso_separation unfolding ord_iso_rel_def
  by simp

end ― ‹localeM_pre_cardinal_arith

synthesize "is_ord_iso" from_definition assuming "nonempty"

lemma trans_on_iff_trans: "trans[A](r)  trans(r  A×A)"
  unfolding trans_on_def trans_def by auto

lemma trans_on_subset: "trans[A](r)  B  A  trans[B](r)"
  unfolding trans_on_def
  by auto

lemma relation_Int: "relation(r  B×B)"
  unfolding relation_def
  by auto

text‹Discipline for termordermap
relativize functional "ordermap" "ordermap_rel" external
relationalize "ordermap_rel" "is_ordermap"

lemma wfrec_on_pred_eq:
  assumes "r  Pow(A×A)"
  shows "wfrec[A](r, x, λx f. f `` Order.pred(A, x, r)) = wfrec(r, x, λx f. f `` Order.pred(A, x, r))"
proof -
  from r  Pow(A×A)
  have "r  A×A = r" by auto
  then
  show ?thesis
    unfolding wfrec_on_def by simp
qed

context M_pre_cardinal_arith
begin

lemma wfrec_on_pred_closed:
  assumes "wf[A](r)" "trans[A](r)" "r  Pow⇗M⇖(A×A)" "M(A)" "x  A"
  shows "M(wfrec(r, x, λx f. f `` Order.pred(A, x, r)))"
proof -
  note assms
  moreover from this
  have "M(r)" "M(x)"
    using transM[of _ "Pow⇗M⇖(A×A)"] transM[of _ A]
    by simp_all
  moreover from calculation
  have "wfrec[A](r, x, λx f. f `` Order.pred(A, x, r)) = wfrec(r, x, λx f. f `` Order.pred(A, x, r))"
    using wfrec_on_pred_eq Pow_rel_char
    by simp
  moreover from calculation
  have "M(wfrec(r, x, λx f. f `` Order.pred(A, x, r)))"
    using wfrec_pred_replacement wf_on_imp_wf trans_on_imp_trans subset_Sigma_imp_relation
      Pow_rel_char
    by (rule_tac MH="λx f b. a[M]. image(M, f, a, b)  pred_set(M, A, x, r, a)" in trans_wfrec_closed)
      (auto dest:transM simp:relation2_def)
  ultimately
  show ?thesis
    by simp
qed

lemma wfrec_on_pred_closed':
  assumes "wf[A](r)" "trans[A](r)" "r  Pow⇗M⇖(A×A)" "M(A)" "x  A"
  shows "M(wfrec[A](r, x, λx f. f `` Order.pred(A, x, r)))"
  using assms wfrec_on_pred_closed wfrec_on_pred_eq Pow_rel_char
  by simp

lemma ordermap_rel_closed[intro,simp]:
  assumes "wf[A](r)" "trans[A](r)" "r  Pow⇗M⇖(A×A)" "M(A)"
  shows "M(ordermap_rel(M, A, r))"
proof -
  from assms
  have "r  A×A = r" "rPow(A×A)" "M(r)"
    using Pow_rel_char
    by auto
  with assms
  have "wf(r)" "trans(r)" "relation(r)"
    unfolding wf_on_def
    using trans_on_iff_trans relation_def by auto
  with M(A) M(r)
  have 1:"
    (y[M]. pair(M, x, y, z)  is_wfrec(M, λx f z. z = f `` Order.pred(A, x, r), r, x, y))
      
    z = x,wfrec(r,x,λx f. f `` Order.pred(A, x, r))" if "M(x)" "M(z)" for x z
    using that trans_wfrec_abs[of r,where
        H="λx f. f `` Order.pred(A, x, r)" and
        MH="λx f z . z= f `` Order.pred(A, x, r)",simplified]
      wfrec_pred_replacement
    unfolding relation2_def
    by auto
  with M(A) M(r)
  have "strong_replacement(M,λx z. z = x,wfrec(r,x,λx f. f `` Order.pred(A, x, r)))"
    using strong_replacement_cong[of M,OF 1,THEN iffD1,OF _ _
        wfrec_pred_replacement[unfolded wfrec_replacement_def]]
    by simp
  with M(A) M(r) r  Pow(A×A) assms
  show ?thesis
    unfolding ordermap_rel_def
    using lam_cong[OF refl wfrec_on_pred_eq] wfrec_on_pred_closed lam_closed
    by auto
qed

lemma is_ordermap_iff:
  assumes "r  Pow⇗M⇖(A×A)" "wf[A](r)" "trans[A](r)"
    "M(A)" "M(res)"
  shows "is_ordermap(M, A, r, res)  res = ordermap_rel(M, A, r)"
proof -
  from r  _ M(A)
  have "r  A×A = r" "M(r)" "r  Pow(A×A)" " x y . x,yr  xA"
    using Pow_rel_char
    by auto
  with assms
  have "wf(r)" "trans(r)" "relation(r)"
    unfolding wf_on_def
    using trans_on_iff_trans relation_def by auto
  with rPow(A×A)
  show ?thesis
    using ordermap_rel_closed[of r A] assms wfrec_on_pred_closed wfrec_pred_replacement
    unfolding is_ordermap_def ordermap_rel_def
    apply (rule_tac lambda_abs2,simp_all add:Relation1_def,clarify)
     apply (rule trans_wfrec_on_abs)
               apply (auto dest:transM simp add: relation_Int relation2_def)
    by(rule_tac wfrec_on_pred_closed'[of A r],auto)
qed

end ― ‹localeM_pre_cardinal_arith

text‹Discipline for termordertype
relativize functional "ordertype" "ordertype_rel" external
relationalize "ordertype_rel" "is_ordertype"

definition is_order_body
  where "is_order_body(M,p,z)  X[M].r[M].A[M]. is_fst(M,p,X)  is_snd(M,p,r) 
      cartprod(M,X,X,A)  subset(M,r,A)  M(z)  M(r)  is_well_ord(M,X,r)  is_ordertype(M,X,r,z)"

context M_pre_cardinal_arith
begin

lemma is_ordertype_iff:
  assumes "r  Pow⇗M⇖(A×A)" "well_ord(A,r)"
  shows "M(A)  M(res)  is_ordertype(M, A, r, res)  res = ordertype_rel(M, A, r)"
  using assms is_ordermap_iff[of r A] trans_on_iff_trans
    ordermap_rel_closed[of A r]
  unfolding is_ordertype_def ordertype_rel_def wf_on_def well_ord_def part_ord_def tot_ord_def
  by simp

lemma ordertype_rel_abs:
  assumes "wellordered(M,X,r)" "M(X)" "M(r)"
  shows "ordertype_rel(M,X,r) = ordertype(X,r)"
  using assms ordertypes_are_absolute[of X r]
  unfolding ordertype_def ordertype_rel_def ordermap_rel_def ordermap_def
  by simp

lemma (in M_pre_cardinal_arith) is_order_body_abs :
  "M(Xr)  M(z)  is_order_body(M, Xr, z) 
    snd(Xr)Pow⇗M⇖(fst(Xr)×fst(Xr))  well_ord(fst(Xr), snd(Xr))  z = ordertype(fst(Xr), snd(Xr))"
  using is_ordertype_iff ordertype_rel_abs well_ord_is_linear Pow_rel_char
    is_well_ord_iff_wellordered snd_abs fst_abs
  unfolding is_order_body_def
  by simp

lemma well_ord_restr: "well_ord(X, r)  well_ord(X, r  X×X)"
proof -
  have "r  X×X  X×X = r  X×X" by auto
  moreover
  assume "well_ord(X, r)"
  ultimately
  show ?thesis
    unfolding well_ord_def tot_ord_def part_ord_def linear_def
      irrefl_def wf_on_def
    by simp_all (simp only: trans_on_def, blast)
qed

lemma ordertype_restr_eq :
  assumes "well_ord(X,r)"
  shows "ordertype(X, r) = ordertype(X, r  X×X)"
  using ordermap_restr_eq assms unfolding ordertype_def
  by simp

lemma ordertype_rel_closed[intro,simp]:
  assumes "well_ord(A,r)" "r  Pow⇗M⇖(A×A)" "M(A)"
  shows "M(ordertype_rel(M,A,r))"
  using assms Pow_rel_char
  unfolding well_ord_def tot_ord_def part_ord_def ordertype_rel_def
  by simp

end ― ‹localeM_pre_cardinal_arith

relativize functional "jump_cardinal_body" "jump_cardinal_body_rel"
relationalize "jump_cardinal_body_rel" "is_jump_cardinal_body_rel"

relativize functional "jump_cardinal_body'" "jump_cardinal_body'_rel"
relationalize "jump_cardinal_body'_rel" "is_jump_cardinal_body'_rel"

text‹Notice that this is not quite the same as termjump_cardinal:
observe termPow(X*X).›

definition
  jump_cardinal' :: "ii"  where
  "jump_cardinal'(K) 
         XPow(K). {z. r  Pow(X*X), z = jump_cardinal_body(Pow(X*X),X)}"

relativize functional "jump_cardinal" "jump_cardinal_rel" external
relativize functional "trans_on" "transitivie_rel" external
relationalize "jump_cardinal_rel" "is_jump_cardinal"


lemma (in M_ordertype) ordermap_closed[intro,simp]:
  assumes "wellordered(M,A,r)" and types:"M(A)" "M(r)"
  shows "M(ordermap(A,r))"
proof -
  note assms
  moreover from this
  obtain i f where "Ord(i)" "f  ord_iso(A, r, i, Memrel(i))"
    "M(i)" "M(f)" using ordertype_exists by blast
  moreover from calculation
  have "i = ordertype(A,r)" using ordertypes_are_absolute by force
  moreover from calculation
  have "ordermap(A,r)  ord_iso(A, r, i, Memrel(i))"
    using ordertype_ord_iso by simp
  ultimately
  have "f = ordermap(A,r)" using well_ord_iso_unique by fastforce
  with M(f)
  show ?thesis by simp
qed

context M_pre_cardinal_arith
begin

lemma def_jump_cardinal_body:
  "M(X)  M(U) 
  jump_cardinal_body(U,X) = {z . r  U, M(z)  well_ord(X, r)  z = ordertype(X, r)}"
  unfolding jump_cardinal_body_def
  using ordertype_closed
  by(rule_tac Replace_cong,auto dest:transM)

lemma jump_cardinal_body_abs:
  shows "M(A)  jump_cardinal_body_rel(M,Pow⇗M⇖(A×A),A) = jump_cardinal_body(Pow⇗M⇖(A×A),A)"
  unfolding jump_cardinal_body_rel_def
  using def_jump_cardinal_body ordertype_rel_abs transM[of _ "Pow⇗M⇖(A×A)"]
  by simp

end ― ‹localeM_pre_cardinal_arith

locale M_cardinal_arith = M_pre_cardinal_arith +
  assumes
    is_ordertype_replacement :
    "strong_replacement(M,λ x z . y[M]. is_order_body(M,x,y)  z=x,y)"
    and
    pow_rel_separation : "A[M]. separation(M, λy. x[M]. x  A  y = x, Pow⇗M⇖(x))"
    and
    separation_is_well_ord : "separation(M, λx . is_well_ord(M,fst(x),snd(x)))"
begin

lemmas Pow_rel_replacement = lam_replacement_Pow_rel[OF pow_rel_separation]

lemma ordtype_replacement :
  "strong_replacement(M , λx z . (snd(x)  Pow⇗M⇖(fst(x)×fst(x))  well_ord(fst(x),snd(x))) 
      z =x, ordertype(fst(x),snd(x)))"
  using strong_replacement_cong[THEN iffD1,OF _ is_ordertype_replacement] is_order_body_abs
  by simp

lemma separation_well_ord : "separation(M, λx . well_ord(fst(x),snd(x)))"
  using separation_cong[THEN iffD1] separation_is_well_ord is_well_ord_iff_wellordered well_ord_abs
  by simp

lemma jump_cardinal_body_lam_replacement :
  shows "lam_replacement(M, λX .jump_cardinal_body(Pow⇗M⇖(X × X),X))" and
    "M(X)  M(jump_cardinal_body(Pow⇗M⇖(X × X), X))"
proof -
  define WO where "WO  λX . {rPow⇗M⇖(X×X) . well_ord(X,r)}"
  define lam_jump_cardinal_body where
     "lam_jump_cardinal_body  λX . λrWO(X) . ordertype(X,r)"
  have "lam_jump_cardinal_body(X) = {r,ordertype(X,r) . r  WO(X)}" for X
    unfolding lam_jump_cardinal_body_def WO_def lam_def
    by simp
  then
  have "jump_cardinal_body(Pow⇗M⇖(X × X),X) = {snd(p) . p  lam_jump_cardinal_body(X)}" if "M(X)" for X
    unfolding jump_cardinal_body_def WO_def lam_def
    by force
  moreover
  have "lam_replacement(M, λx. {y . r  Pow⇗M⇖(x × x), (r  Pow⇗M⇖(x × x)  well_ord(x, r))  y = ordertype(x, r)})"
    (is "lam_replacement(M,?q)")
  using Pow_rel_replacement[THEN [2] lam_replacement_hcomp]
      lam_replacement_CartProd lam_replacement_identity lam_replacement_fst lam_replacement_snd
      fst_closed[OF transM] snd_closed[OF transM]
      separation_well_ord separation_in separation_conj transM[of _ "Pow⇗M⇖(_×_)"]
      strong_lam_replacement_imp_lam_replacement_RepFun[OF ordtype_replacement, where g="λX. Pow⇗M⇖(X × X)"]
  by force
  moreover
  have "M(?q(x))" if "M(x)" for x
    using that Pow_rel_replacement[THEN [2] lam_replacement_hcomp]
      lam_replacement_CartProd lam_replacement_identity
      ordertype_closed transM[of _ "Pow⇗M⇖(_×_)"]
      fst_closed[OF transM] snd_closed[OF transM]
    by(rule_tac strong_lam_replacement_imp_strong_replacement[OF ordtype_replacement,THEN strong_replacement_closed],
        auto)
  moreover
  have "?q(x)={snd(p) . p  (λrWO(x). ordertype(x, r))}" if "M(x)" for x
    using that
    unfolding lam_def WO_def
    by force
  moreover from calculation
  have "?q(X) = jump_cardinal_body(Pow⇗M⇖(X × X), X)" if "M(X)" for X
    using that
    unfolding lam_jump_cardinal_body_def
    by simp
  moreover from calculation
  have "M(jump_cardinal_body(Pow⇗M⇖(X × X), X))" if "M(X)" for X
    using that by simp
  moreover from calculation
  have 1:"lam_replacement(M, λx . {snd(p) . p  lam_jump_cardinal_body(x)})"
    using lam_replacement_cong
    by auto
  ultimately
  show "lam_replacement(M, λX .jump_cardinal_body(Pow⇗M⇖(X × X),X))" and
    "M(X)  M(jump_cardinal_body(Pow⇗M⇖(X × X), X))"
    using lam_replacement_imp_strong_replacement[OF lam_replacement_snd]
      lam_replacement_cong[OF 1,unfolded lam_jump_cardinal_body_def]
    by simp_all
qed

lemmas jump_cardinal_body_closed = jump_cardinal_body_lam_replacement(2)

lemma jump_cardinal_closed:
  assumes "M(K)"
  shows "M({jump_cardinal_body(Pow⇗M⇖(X × X),X) . X  Pow⇗M⇖(K)})"
  using assms jump_cardinal_body_lam_replacement lam_replacement_imp_strong_replacement
    transM[of _ "Pow⇗M⇖(K)"] RepFun_closed
  by auto

end ― ‹localeM_cardinal_arith

context M_pre_cardinal_arith
begin

(*A general fact about ordermap*)
lemma ordermap_eqpoll_pred:
  "[| well_ord(A,r);  x  A ; M(A);M(r);M(x)|] ==> ordermap(A,r)`x ≈⇗MOrder.pred(A,x,r)"
  apply (simp add: def_eqpoll_rel)
  apply (rule rexI)
   apply (simp add: ordermap_eq_image well_ord_is_wf)
   apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij,
        THEN bij_converse_bij])
   apply (rule pred_subset, simp)
  done

text‹Kunen: "each termx,y  K × K has no more than termz × z predecessors..." (page 29)›
lemma ordermap_csquare_le:
  assumes K: "Limit(K)" and x: "x<K" and y: " y<K"
    and types: "M(K)" "M(x)" "M(y)"
  shows "|ordermap(K × K, csquare_rel(K)) ` x,y|⇗M |succ(succ(x  y))|⇗M⇖ ⊗⇗M|succ(succ(x  y))|⇗M⇖"
  using types
proof (simp add: cmult_rel_def, rule_tac well_ord_lepoll_rel_imp_cardinal_rel_le)
  let ?z="succ(x  y)"
  show "well_ord(|succ(?z)|⇗M× |succ(?z)|⇗M,
                 rmult(|succ(?z)|⇗M, Memrel(|succ(?z)|⇗M), |succ(?z)|⇗M, Memrel(|succ(?z)|⇗M)))"
    by (blast intro: well_ord_Memrel well_ord_rmult types)
next
  let ?z="succ(x  y)"
  have zK: "?z<K" using x y K
    by (blast intro: Un_least_lt Limit_has_succ)
  hence oz: "Ord(?z)" by (elim ltE)
  from assms
  have Mom:"M(ordermap(K × K, csquare_rel(K)))"
    using well_ord_csquare Limit_is_Ord by fastforce
  then
  have "ordermap(K × K, csquare_rel(K)) ` x,y ≲⇗Mordermap(K × K, csquare_rel(K)) ` ?z,?z"
    by (blast intro: ordermap_z_lt leI le_imp_lepoll_rel K x y types)
  also have "... ≈⇗MOrder.pred(K × K, ?z,?z, csquare_rel(K))"
  proof (rule ordermap_eqpoll_pred)
    show "well_ord(K × K, csquare_rel(K))" using K
      by (rule Limit_is_Ord [THEN well_ord_csquare])
  next
    show "?z, ?z  K × K" using zK
      by (blast intro: ltD)
  qed (simp_all add:types)
  also have "...  ≲⇗Msucc(?z) × succ(?z)" using zK
    by (rule_tac pred_csquare_subset [THEN subset_imp_lepoll_rel]) (simp_all add:types)
  also have "... ≈⇗M|succ(?z)|⇗M× |succ(?z)|⇗M⇖" using oz
    by (blast intro: prod_eqpoll_rel_cong Ord_cardinal_rel_eqpoll_rel eqpoll_rel_sym types)
  finally show "ordermap(K × K, csquare_rel(K)) ` x,y ≲⇗M|succ(?z)|⇗M× |succ(?z)|⇗M⇖"
    by (simp_all add:types Mom)
  from Mom
  show "M(ordermap(K × K, csquare_rel(K)) ` x, y)" by (simp_all add:types)
qed (simp_all add:types)

text‹Kunen: "... so the order type is ≤› K"›
lemma ordertype_csquare_le_M:
  assumes IK: "InfCard⇗M⇖(K)" and eq: "y. yK  InfCard⇗M⇖(y)  M(y)  y ⊗⇗My = y"
    ― ‹Note the weakened hypothesis @{thm [source] eq}
    and types: "M(K)"
  shows "ordertype(K*K, csquare_rel(K))  K"
proof -
  have  CK: "Card⇗M⇖(K)" using IK by (rule_tac InfCard_rel_is_Card_rel) (simp_all add:types)
  hence OK: "Ord(K)"  by (rule Card_rel_is_Ord) (simp_all add:types)
  moreover have "Ord(ordertype(K × K, csquare_rel(K)))" using OK
    by (rule well_ord_csquare [THEN Ord_ordertype])
  ultimately show ?thesis
  proof (rule all_lt_imp_le)
    fix i
    assume i:"i < ordertype(K × K, csquare_rel(K))"
    hence Oi: "Ord(i)" by (elim ltE)
    obtain x y where x: "x  K" and y: "y  K"
      and ieq: "i = ordermap(K × K, csquare_rel(K)) ` x,y"
      using i by (auto simp add: ordertype_unfold elim: ltE)
    hence xy: "Ord(x)" "Ord(y)" "x < K" "y < K" using OK
      by (blast intro: Ord_in_Ord ltI)+
    hence ou: "Ord(x  y)"
      by (simp)
    from OK types
    have "M(ordertype(K × K, csquare_rel(K)))"
      using well_ord_csquare by fastforce
    with i x y types
    have types': "M(K)" "M(i)" "M(x)" "M(y)"
      using types by (auto dest:transM ltD)
    show "i < K"
    proof (rule Card_rel_lt_imp_lt [OF _ Oi CK])
      have "|i|⇗M |succ(succ(x  y))|⇗M⇖ ⊗⇗M|succ(succ(x  y))|⇗M⇖" using IK xy
        by (auto simp add: ieq types intro: InfCard_rel_is_Limit [THEN ordermap_csquare_le] types')
      moreover have "|succ(succ(x  y))|⇗M⇖ ⊗⇗M|succ(succ(x  y))|⇗M< K"
      proof (cases rule: Ord_linear2 [OF ou Ord_nat])
        assume "x  y < nat"
        hence "|succ(succ(x  y))|⇗M⇖ ⊗⇗M|succ(succ(x  y))|⇗M nat"
          by (simp add: lt_def nat_cmult_rel_eq_mult nat_succI
              nat_into_Card_rel [THEN Card_rel_cardinal_rel_eq] types')
        also have "...  K" using IK
          by (simp add: InfCard_rel_def le_imp_subset types)
        finally show "|succ(succ(x  y))|⇗M⇖ ⊗⇗M|succ(succ(x  y))|⇗M< K"
          by (simp add: ltI OK)
      next
        assume natxy: "nat  x  y"
        hence seq: "|succ(succ(x  y))|⇗M= |x  y|⇗M⇖" using xy
          by (simp add: le_imp_subset nat_succ_eqpoll_rel [THEN cardinal_rel_cong] le_succ_iff types')
        also have "... < K" using xy
          by (simp add: Un_least_lt Ord_cardinal_rel_le [THEN lt_trans1] types')
        finally have "|succ(succ(x  y))|⇗M< K" .
        moreover have "InfCard⇗M⇖(|succ(succ(x  y))|⇗M)" using xy natxy
          by (simp add: seq InfCard_rel_def nat_le_cardinal_rel types')
        ultimately show ?thesis by (simp add: eq ltD types')
      qed
      ultimately show "|i|⇗M< K" by (blast intro: lt_trans1)
    qed (simp_all add:types')
  qed
qed

(*Main result: Kunen's Theorem 10.12*)
lemma InfCard_rel_csquare_eq:
  assumes IK: "InfCard⇗M⇖(K)" and
    types: "M(K)"
  shows "K ⊗⇗MK = K"
proof -
  have  OK: "Ord(K)" using IK by (simp add: Card_rel_is_Ord InfCard_rel_is_Card_rel types)
  from OK assms
  show "K ⊗⇗MK = K"
  proof (induct rule: trans_induct)
    case (step i)
    note types = M(K) M(i)
    show "i ⊗⇗Mi = i"
    proof (rule le_anti_sym)
      from step types
      have Mot:"M(ordertype(i × i, csquare_rel(i)))" "M(ordermap(i × i, csquare_rel(i)))"
        using well_ord_csquare Limit_is_Ord by simp_all
      then
      have "|i × i|⇗M= |ordertype(i × i, csquare_rel(i))|⇗M⇖"
        by (rule_tac cardinal_rel_cong,
            simp_all add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll_rel] types)
      with Mot
      have "i ⊗⇗Mi  ordertype(i × i, csquare_rel(i))"
        by (simp add: step.hyps cmult_rel_def Ord_cardinal_rel_le well_ord_csquare [THEN Ord_ordertype] types)
      moreover
      have "ordertype(i × i, csquare_rel(i))  i" using step
        by (rule_tac ordertype_csquare_le_M) (simp add: types)
      ultimately show "i ⊗⇗Mi  i" by (rule le_trans)
    next
      show "i  i ⊗⇗Mi" using step
        by (blast intro: cmult_rel_square_le InfCard_rel_is_Card_rel)
    qed
  qed
qed


(*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
lemma well_ord_InfCard_rel_square_eq:
  assumes r: "well_ord(A,r)" and I: "InfCard⇗M⇖(|A|⇗M)" and
    types: "M(A)" "M(r)"
  shows "A × A ≈⇗MA"
proof -
  have "A × A ≈⇗M|A|⇗M× |A|⇗M⇖"
    by (blast intro: prod_eqpoll_rel_cong well_ord_cardinal_rel_eqpoll_rel eqpoll_rel_sym r types)
  also have "... ≈⇗MA"
  proof (rule well_ord_cardinal_rel_eqE [OF _ r])
    show "well_ord(|A|⇗M× |A|⇗M, rmult(|A|⇗M, Memrel(|A|⇗M), |A|⇗M, Memrel(|A|⇗M)))"
      by (blast intro: well_ord_rmult well_ord_Memrel r types)
  next
    show "||A|⇗M× |A|⇗M⇖|⇗M= |A|⇗M⇖" using InfCard_rel_csquare_eq I
      by (simp add: cmult_rel_def types)
  qed (simp_all add:types)
  finally show ?thesis by (simp_all add:types)
qed

lemma InfCard_rel_square_eqpoll:
  assumes "InfCard⇗M⇖(K)" and types:"M(K)" shows "K × K ≈⇗MK"
  using assms
  apply (rule_tac well_ord_InfCard_rel_square_eq)
     apply (erule InfCard_rel_is_Card_rel [THEN Card_rel_is_Ord, THEN well_ord_Memrel])
      apply (simp_all add: InfCard_rel_is_Card_rel [THEN Card_rel_cardinal_rel_eq] types)
  done

lemma Inf_Card_rel_is_InfCard_rel: "[| Card⇗M⇖(i); ~ Finite_rel(M,i) ; M(i) |] ==> InfCard⇗M⇖(i)"
  by (simp add: InfCard_rel_def Card_rel_is_Ord [THEN nat_le_infinite_Ord])

subsubsection‹Toward's Kunen's Corollary 10.13 (1)›

lemma InfCard_rel_le_cmult_rel_eq: "[| InfCard⇗M⇖(K);  L  K;  0<L; M(K) ; M(L) |] ==> K ⊗⇗ML = K"
  apply (rule le_anti_sym)
   prefer 2
   apply (erule ltE, blast intro: cmult_rel_le_self InfCard_rel_is_Card_rel)
  apply (frule InfCard_rel_is_Card_rel [THEN Card_rel_is_Ord, THEN le_refl]) prefer 3
    apply (rule cmult_rel_le_mono [THEN le_trans], assumption+)
    apply (simp_all add: InfCard_rel_csquare_eq)
  done

(*Corollary 10.13 (1), for cardinal multiplication*)
lemma InfCard_rel_cmult_rel_eq: "[| InfCard⇗M⇖(K);  InfCard⇗M⇖(L); M(K) ; M(L) |] ==> K ⊗⇗ML = K  L"
  apply (rule_tac i = K and j = L in Ord_linear_le)
     apply (typecheck add: InfCard_rel_is_Card_rel Card_rel_is_Ord)
   apply (rule cmult_rel_commute [THEN ssubst]) prefer 3
     apply (rule Un_commute [THEN ssubst])
     apply (simp_all add: InfCard_rel_is_Limit [THEN Limit_has_0] InfCard_rel_le_cmult_rel_eq
      subset_Un_iff2 [THEN iffD1] le_imp_subset)
  done

lemma InfCard_rel_cdouble_eq: "InfCard⇗M⇖(K)  M(K)   K ⊕⇗MK = K"
  apply (simp add: cmult_rel_2 [symmetric] InfCard_rel_is_Card_rel cmult_rel_commute)
  apply (simp add: InfCard_rel_le_cmult_rel_eq InfCard_rel_is_Limit Limit_has_0 Limit_has_succ)
  done

(*Corollary 10.13 (1), for cardinal addition*)
lemma InfCard_rel_le_cadd_rel_eq: "[| InfCard⇗M⇖(K);  L  K ; M(K) ; M(L)|] ==> K ⊕⇗ML = K"
  apply (rule le_anti_sym)
   prefer 2
   apply (erule ltE, blast intro: cadd_rel_le_self InfCard_rel_is_Card_rel)
  apply (frule InfCard_rel_is_Card_rel [THEN Card_rel_is_Ord, THEN le_refl]) prefer 3
    apply (rule cadd_rel_le_mono [THEN le_trans], assumption+)
    apply (simp_all add: InfCard_rel_cdouble_eq)
  done

lemma InfCard_rel_cadd_rel_eq: "[| InfCard⇗M⇖(K);  InfCard⇗M⇖(L); M(K) ; M(L) |] ==> K ⊕⇗ML = K  L"
  apply (rule_tac i = K and j = L in Ord_linear_le)
     apply (typecheck add: InfCard_rel_is_Card_rel Card_rel_is_Ord)
   apply (rule cadd_rel_commute [THEN ssubst]) prefer 3
     apply (rule Un_commute [THEN ssubst])
     apply (simp_all add: InfCard_rel_le_cadd_rel_eq subset_Un_iff2 [THEN iffD1] le_imp_subset)
  done

(*The other part, Corollary 10.13 (2), refers to the cardinality of the set
  of all n-tuples of elements of K.  A better version for the Isabelle theory
  might be  InfCard(K) ==> |list(K)| = K.
*)

end ― ‹localeM_pre_cardinal_arith

subsection‹For Every Cardinal Number There Exists A Greater One›

text‹This result is Kunen's Theorem 10.16, which would be trivial using AC›

locale M_cardinal_arith_jump = M_cardinal_arith + M_ordertype
begin

lemma def_jump_cardinal_rel_aux:
  "X  Pow⇗M⇖(K)  M(K) 
  {z . r  Pow⇗M⇖(X × X), M(z)  well_ord(X, r)  z = ordertype(X, r)} =
  {z . r  Pow⇗M⇖(K × K), M(z)  well_ord(X, r)  z = ordertype(X, r)}"
proof(rule,auto simp:Pow_rel_char dest:transM)
  let ?L="{z . r  Pow⇗M⇖(X × X), M(z)  well_ord(X, r)  z = ordertype(X, r)}"
  let ?R="{z . r  Pow⇗M⇖(K × K), M(z)  well_ord(X, r)  z = ordertype(X, r)}"
  show "ordertype(X, r)  {y . x  {x  Pow(X × X) . M(x)}, M(y)  well_ord(X, x)  y = ordertype(X, x)}"
    if "M(K)" "M(r)" "rK×K" "XK" "M(X)" "well_ord(X,r)" for r
  proof -
    from that
    have "ordertype(X,r) = ordertype(X,rX×X)" "(rX×X)X×X" "M(rX×X)"
      "well_ord(X,rX×X)" "wellordered(M,X,rX×X)"
      using well_ord_restr ordertype_restr_eq by auto
    moreover from this
    have "ordertype(X,rX×X)  ?L"
      using that Pow_rel_char
        ReplaceI[of "λ z r . M(z)  well_ord(X, r)  z = ordertype(X, r)" "ordertype(X,rX×X)"]
      by auto
    ultimately
    show ?thesis
      using Pow_rel_char by auto
  qed
qed

lemma def_jump_cardinal_rel_aux2:
  assumes "X  Pow⇗M⇖(K)" "M(K)"
  shows "jump_cardinal_body(Pow⇗M⇖(K×K),X) = jump_cardinal_body(Pow⇗M⇖(X×X),X)"
proof -
  from assms
  have "jump_cardinal_body(Pow⇗M⇖(K×K),X) = {z . r Pow⇗M⇖(K×K), M(z)  well_ord(X, r)  z = ordertype(X, r)}"
    using def_jump_cardinal_body transM[of _ "Pow⇗M⇖(K)"]
    by simp
  also from assms
  have "... = {z . r Pow⇗M⇖(X×X), M(z)  well_ord(X, r)  z = ordertype(X, r)}"
    using def_jump_cardinal_rel_aux  transM[of _ "Pow⇗M⇖(K)"]
    by simp
  also from assms
  have "... = jump_cardinal_body(Pow⇗M⇖(X×X),X)"
    using def_jump_cardinal_body transM[of _ "Pow⇗M⇖(K)"] by auto
  finally
  show ?thesis .
qed

lemma def_jump_cardinal_rel:
  assumes "M(K)"
  shows "jump_cardinal_rel(M,K) =
         ({jump_cardinal_body(Pow⇗M⇖(K*K),X) . X Pow⇗M⇖(K)})"
proof -
  have "jump_cardinal_body(Pow⇗M⇖(X × X),X) = {z . r  Pow⇗M⇖(X × X), M(z)  well_ord(X, r)  z=ordertype(X, r)}"
    if "M(X)" for X
    using that ordertype_closed transM[of _ "Pow⇗M⇖(X×X)"]
    unfolding jump_cardinal_body_def
    by(intro equalityI subsetI,auto)
  then
  have "M({z . r  Pow⇗M⇖(X × X), M(z)  well_ord(X, r)  z = ordertype(X, r)})"
    if "M(Y)" "X  Pow⇗M⇖(Y)" for Y X
    using jump_cardinal_body_closed[of X] that transM[of _ "Pow⇗M⇖(Y)"]
      ordertype_closed transM[of _ "Pow⇗M⇖(X×X)"]
    unfolding jump_cardinal_body_def
    by auto
  moreover from M(K)
  have "R  Pow⇗M⇖(X × X)  X  Pow⇗M⇖(K)  R  Pow⇗M⇖(K × K)" for X R
    using mem_Pow_rel_abs transM[OF _ Pow_rel_closed, of R "X×X"]
      transM[OF _ Pow_rel_closed, of X K] by auto
  ultimately
  show ?thesis
    using assms is_ordertype_iff
      ordertype_rel_abs transM[of _ "Pow⇗M⇖(K)"] transM[of _ "Pow⇗M⇖(K×K)"]
      def_jump_cardinal_rel_aux jump_cardinal_body_closed ordertype_closed
    unfolding jump_cardinal_rel_def jump_cardinal_body_def
    apply(intro equalityI subsetI,auto dest:transM[of _ "Pow⇗M⇖(K)"],rename_tac y r)
    by(rule_tac x="{z . xa  Pow⇗M⇖(K × K), M(z)  well_ord(y, xa)  z = ordertype(y, xa)}" in bexI,auto)
qed

lemma Ord_jump_cardinal_rel: "M(K)  Ord(jump_cardinal_rel(M,K))"
  apply (unfold def_jump_cardinal_rel jump_cardinal_body_def )
  apply (rule Ord_is_Transset [THEN [2] OrdI])
   prefer 2 apply (blast intro!: Ord_ordertype)
  apply (unfold Transset_def)
  apply (safe del: subsetI)
  apply (subst ordertype_pred_unfold, simp, safe)
  apply (rule UN_I)
   apply (rule_tac [2] ReplaceI)
     prefer 4 apply (blast intro: well_ord_subset elim!: predE, simp_all)
   prefer 2 apply (blast intro: well_ord_subset elim!: predE)
proof -
  fix X r xb
  assume "M(K)" "X  Pow⇗M⇖(K)" "r  Pow⇗M⇖(K × K)" "well_ord(X, r)" "xb  X"
  moreover from this
  have "M(X)" "M(r)"
    using cartprod_closed trans_Pow_rel_closed by auto
  moreover from this
  have "M(xb)" using transM[OF xbX] by simp
  ultimately
  show "Order.pred(X, xb, r)  Pow⇗M⇖(K)"
    using def_Pow_rel by (auto dest:predE)
qed

declare conj_cong [cong del]
  ― ‹incompatible with some of the proofs of the original theory›

lemma jump_cardinal_rel_iff_old:
  "M(i)  M(K)  i  jump_cardinal_rel(M,K) 
      (r[M]. X[M]. r  K*K & X  K & well_ord(X,r) & i = ordertype(X,r))"
  apply (unfold def_jump_cardinal_rel jump_cardinal_body_def)
  apply (auto del: subsetI)
   apply (rename_tac y r)
   apply (rule_tac x=r in rexI, intro conjI) prefer 2
     apply (rule_tac x=y in rexI, intro conjI)
        apply (auto dest:mem_Pow_rel transM)
   apply (rule_tac A=r in rev_subsetD, assumption)
   defer
   apply (rename_tac r y)
   apply (rule_tac x=y in bexI)
    apply (rule_tac x=r in ReplaceI, auto)
  using def_Pow_rel
    apply (force+)[2]
  apply (rule_tac A=r in rev_subsetD, assumption)
  using mem_Pow_rel[THEN conjunct1]
  apply auto
  done

(*The easy part of Theorem 10.16: jump_cardinal_rel(K) exceeds K*)
lemma K_lt_jump_cardinal_rel: "Ord(K) ==> M(K)  K < jump_cardinal_rel(M,K)"
  apply (rule Ord_jump_cardinal_rel [THEN [2] ltI])
   apply (rule jump_cardinal_rel_iff_old [THEN iffD2], assumption+)
   apply (rule_tac x="Memrel(K)" in rexI)
    apply (rule_tac x=K in rexI)
     apply (simp add: ordertype_Memrel well_ord_Memrel)
  using Memrel_closed
     apply (simp_all add: Memrel_def subset_iff)
  done

lemma def_jump_cardinal_rel':
  assumes "M(K)"
  shows "jump_cardinal_rel(M,K) =
         (XPow⇗M⇖(K). {z. r  Pow⇗M⇖(X×X), well_ord(X,r)  z = ordertype(X,r)})"
proof -
  from assms
  have "jump_cardinal_rel(M, K) = (XPow⇗M⇖(K). jump_cardinal_body(Pow⇗M⇖(K × K), X))"
    using def_jump_cardinal_rel
    by simp
  also from M(K)
  have " ... = (XPow⇗M⇖(K). jump_cardinal_body(Pow⇗M⇖(X × X), X))"
    using def_jump_cardinal_rel_aux2
    by simp
  finally
  show ?thesis
    unfolding jump_cardinal_body_def by simp
qed

rel_closed for "jump_cardinal"
proof -
  fix K
  assume "M(K)"
  moreover from this
  have "jump_cardinal_rel(M, K) =
    {jump_cardinal_body(Pow⇗M⇖(X × X), X) . XPow⇗M⇖(K)}"
    using def_jump_cardinal_rel'
    unfolding jump_cardinal_body_def[symmetric]
    by simp
  moreover from calculation
  have "M(({jump_cardinal_body(Pow⇗M⇖(X × X), X) . XPow⇗M⇖(K)}))"
    using def_jump_cardinal_rel_aux jump_cardinal_closed
    by simp
  ultimately
  show "M(jump_cardinal_rel(M,K))"
    by simp
qed

(*The proof by contradiction: the bijection f yields a wellordering of X
  whose ordertype is jump_cardinal_rel(K).  *)
lemma Card_rel_jump_cardinal_rel_lemma:
  "[| well_ord(X,r);  r  K * K;  X  K;
         f  bij(ordertype(X,r), jump_cardinal_rel(M,K));
         M(X); M(r); M(K); M(f) |]
      ==> jump_cardinal_rel(M,K)  jump_cardinal_rel(M,K)"
  apply (subgoal_tac "f O ordermap (X,r)  bij (X, jump_cardinal_rel (M,K))")
   prefer 2 apply (blast intro: comp_bij ordermap_bij)
  apply (rule jump_cardinal_rel_iff_old [THEN iffD2],simp+)
  apply (intro rexI conjI)
       apply (rule subset_trans [OF rvimage_type Sigma_mono], assumption+)
     apply (erule bij_is_inj [THEN well_ord_rvimage])
     apply (rule Ord_jump_cardinal_rel [THEN well_ord_Memrel])
     apply (simp_all add: well_ord_Memrel [THEN [2] bij_ordertype_vimage]
      ordertype_Memrel Ord_jump_cardinal_rel)
  done

(*The hard part of Theorem 10.16: jump_cardinal_rel(K) is itself a cardinal*)
lemma Card_rel_jump_cardinal_rel: "M(K)  Card_rel(M,jump_cardinal_rel(M,K))"
  apply (rule Ord_jump_cardinal_rel [THEN Card_relI])
    apply (simp_all add: def_eqpoll_rel)
  apply (drule_tac i1=j in jump_cardinal_rel_iff_old [THEN iffD1, OF _ _ ltD, of _ K], safe)
  apply (blast intro: Card_rel_jump_cardinal_rel_lemma [THEN mem_irrefl])
  done

subsection‹Basic Properties of Successor Cardinals›

lemma csucc_rel_basic: "Ord(K) ==> M(K)  Card_rel(M,csucc_rel(M,K)) & K < csucc_rel(M,K)"
  apply (unfold csucc_rel_def)
  apply (rule LeastI[of "λi. M(i)  Card_rel(M,i)  K < i", THEN conjunct2])
   apply (blast intro: Card_rel_jump_cardinal_rel K_lt_jump_cardinal_rel Ord_jump_cardinal_rel)+
  done

lemmas Card_rel_csucc_rel = csucc_rel_basic [THEN conjunct1]

lemmas lt_csucc_rel = csucc_rel_basic [THEN conjunct2]

lemma Ord_0_lt_csucc_rel: "Ord(K) ==> M(K)  0 < csucc_rel(M,K)"
  by (blast intro: Ord_0_le lt_csucc_rel lt_trans1)

lemma csucc_rel_le: "[| Card_rel(M,L);  K<L; M(K); M(L) |] ==> csucc_rel(M,K)  L"
  apply (unfold csucc_rel_def)
  apply (rule Least_le)
   apply (blast intro: Card_rel_is_Ord)+
  done

lemma lt_csucc_rel_iff: "[| Ord(i); Card_rel(M,K); M(K); M(i)|] ==> i < csucc_rel(M,K)  |i|⇗M K"
  apply (rule iffI)
   apply (rule_tac [2] Card_rel_lt_imp_lt)
       apply (erule_tac [2] lt_trans1)
       apply (simp_all add: lt_csucc_rel Card_rel_csucc_rel Card_rel_is_Ord)
  apply (rule notI [THEN not_lt_imp_le])
    apply (rule Card_rel_cardinal_rel [THEN csucc_rel_le, THEN lt_trans1, THEN lt_irrefl], simp_all+)
   apply (rule Ord_cardinal_rel_le [THEN lt_trans1])
     apply (simp_all add: Card_rel_is_Ord)
  done

lemma Card_rel_lt_csucc_rel_iff:
  "[| Card_rel(M,K'); Card_rel(M,K); M(K'); M(K) |] ==> K' < csucc_rel(M,K)  K'  K"
  by (simp add: lt_csucc_rel_iff Card_rel_cardinal_rel_eq Card_rel_is_Ord)

lemma InfCard_rel_csucc_rel: "InfCard_rel(M,K)  M(K) ==> InfCard_rel(M,csucc_rel(M,K))"
  by (simp add: InfCard_rel_def Card_rel_csucc_rel Card_rel_is_Ord
      lt_csucc_rel [THEN leI, THEN [2] le_trans])


subsubsection‹Theorems by Krzysztof Grabczewski, proofs by lcp›

lemma nat_sum_eqpoll_rel_sum:
  assumes m: "m  nat" and n: "n  nat" shows "m + n ≈⇗Mm +ω n"
proof -
  have "m + n ≈⇗M|m+n|⇗M⇖" using m n
    by (blast intro: nat_implies_well_ord well_ord_radd well_ord_cardinal_rel_eqpoll_rel eqpoll_rel_sym)
  also have "... = m +ω n" using m