Theory CZH_EX_Replacement

(* Copyright 2021 (C) Mihails Milehins *)

section‹Example I: absence of replacement in ‹Vω+ω››
theory CZH_EX_Replacement
  imports CZH_Sets_ZQR
begin


text‹
The statement of the main result presented in this subsection
can be found in cite‹"noauthor_wikipedia_2001"›\footnote{
\url{https://en.wikipedia.org/wiki/Zermelo_set_theory}
}
›

definition repl_ex_fun :: V
  where "repl_ex_fun = (λi∈∘ω. Vfrom ω i)"

mk_VLambda repl_ex_fun_def
  |vsv repl_ex_fun_vsv|
  |vdomain repl_ex_fun_vdomain|
  |app repl_ex_fun_app|

lemma repl_ex_fun_vrange: "ℛ∘ repl_ex_fun ⊆∘ Vset (ω + ω)"
proof(intro vsv.vsv_vrange_vsubset, unfold repl_ex_fun_vdomain)
  fix x assume prems: "x ∈∘ ω"
  then show "repl_ex_fun⦇x⦈ ∈∘ Vset (ω + ω)"
  proof(induction rule: omega_induct)
    case 0 then show ?case 
      by 
        (
          auto 
            simp: repl_ex_fun_app intro!: vreal_in_Vset_ω2 omega_vsubset_vreal
        )
  next
    case (succ n)
    then have Ord_n: "Ord n" by auto
    have Limit_ωω: "Limit (ω + ω)" by auto
    from succ show ?case 
      by
        (
          auto 
            simp: Vfrom_succ_Ord[OF Ord_n, of ω] repl_ex_fun_app 
            intro: Limit_ωω 
            intro!: omega_vsubset_vreal vreal_in_Vset_ω2
        )
  qed
qed (unfold repl_ex_fun_def, auto)

lemma Limit_vsv_not_in_Vset_if_vrange_not_in_Vset:
  assumes "Limit α" and "ℛ∘ f ∉∘ Vset α"
  shows "f ∉∘ Vset α"
proof(rule ccontr, unfold not_not)
  assume "f ∈∘ Vset α"
  with assms(1) have "ℛ∘ f ∈∘ Vset α" by (simp add: vrange_in_VsetI)
  with assms(2) show False by simp
qed

lemma Ord_not_in_Vset:
  assumes "Ord α"
  shows "α ∉∘ Vset α"
  using assms
proof(induction rule: Ord_induct3')
  case (succ α)
  then have succα: "Vset (succ α) = VPow (Vset α)" by (simp add: Vset_succ)
  show ?case 
  proof(rule ccontr, unfold not_not)
    assume "succ α ∈∘ Vset (succ α)"
    then have "vinsert α α ∈∘ VPow (Vset α)" 
      unfolding succα by (simp add: succ_def)
    with succ(2) show False by auto
  qed
next
  case (Limit α) show ?case 
  proof(rule ccontr, unfold not_not)
    assume "(⋃∘ξ∈∘α. ξ) ∈∘ Vset (⋃∘ξ∈∘α. ξ)"
    with Limit(1) have "α ∈∘ Vset α" by auto
    with Limit(1) obtain i where i: "i ∈∘ α" and "(⋃∘ξ∈∘α. ξ) ∈∘ Vset i" 
      by (metis Limit_Vfrom_eq Limit_vifunion_def vifunion_iff)
    moreover with Limit(1) have "α ∈∘ Vset i" by auto
    ultimately have "i ∈∘ Vset i" by auto
    with Limit(2)[OF i] show False by auto
  qed
qed simp

lemma Ord_succ_vsusbset_Vfrom_succ: 
  assumes "Transset A" and "Ord a" and "a ∈∘ Vfrom A i" 
  shows "succ a ⊆∘ Vfrom A (succ i)"
proof(intro vsubsetI)
  from Vfrom_in_mono[OF vsubset_reflexive] have i_succi: 
    "Vfrom A i ∈∘ Vfrom A (succ i)"
    by simp
  fix x assume prems: "x ∈∘ succ a"
  then consider ‹x ∈∘ a› | ‹x = a› unfolding succ_def by auto
  then show "x ∈∘ Vfrom A (succ i)"
  proof cases
    case 1
    have "x ∈∘ Vfrom A i" by (rule Vfrom_trans[OF assms(1) 1 assms(3)])
    then show "x ∈∘ Vfrom A (succ i)" by (rule Vfrom_trans[OF assms(1) _ i_succi])
  next
    case 2 from assms(3) show ?thesis
      unfolding 2 by (intro Vfrom_trans[OF assms(1) _ i_succi])
  qed
qed

lemma Ord_succ_in_Vfrom_succ: 
  assumes "Transset A" and "Ord a" and "a ∈∘ Vfrom A i" 
  shows "succ a ∈∘ Vfrom A (succ (succ i))"
  using Ord_succ_vsusbset_Vfrom_succ[OF assms] by (simp add: Vfrom_succ)

lemma ω_vplus_in_Vfrom_ω:
  assumes "j ∈∘ ω"
  shows "ω + j ∈∘ Vfrom ω (succ (2ℕ * j))"
  using assms
proof(induction rule: omega_induct)
  case 0
  have "ω ∈∘ Vfrom ω (succ 0)" 
    unfolding Vfrom_succ_Ord[where i=0, simplified] by auto
  then show ?case by simp
next
  case (succ n)
  from succ(1) obtain m where n_def: "n = mℕ" by (auto elim: nat_of_omega)
  from succ(1) have ω_succn: "ω + succ n = succ (ω + n)" by (simp add: plus_V_succ_right)
  from succ(1) have succ_2succn: "succ (2ℕ * succ n) = succ (succ (succ (2ℕ * n)))" 
    unfolding n_def by (cs_concl_step nat_omega_simps)+ auto    
  show ?case 
    unfolding ω_succn succ_2succn
    by (intro Ord_succ_in_Vfrom_succ succ) 
      (auto simp: succ(1) intro: Ord_is_Transset)
qed

lemma repl_ex_fun_vrange_not_in_Vset: "ℛ∘ repl_ex_fun ∉∘ Vset (ω + ω)"
proof(rule ccontr, unfold not_not)
  assume prems: "ℛ∘ repl_ex_fun ∈∘ Vset (ω + ω)"
  then have "⋃∘(ℛ∘ repl_ex_fun) ∈∘ Vset (ω + ω)" by (simp add: VUnion_in_VsetI)
  moreover have "ω + ω ⊆∘ ⋃∘(ℛ∘ repl_ex_fun)"
  proof(intro vsubsetI)
    fix x assume prems: "x ∈∘ ω + ω"
    from prems consider ‹x ∈∘ ω› | ‹x ∉∘ ω› by auto
    then show "x ∈∘ ⋃∘(ℛ∘ repl_ex_fun)"
    proof cases
      case 1 
      show ?thesis 
      proof(rule VUnionI)
        show "Vfrom ω 0 ∈∘ ℛ∘ repl_ex_fun"
          unfolding repl_ex_fun_def by blast
        from 1 show "x ∈∘ Vfrom ω 0" by auto
      qed
    next
      case 2
      with prems obtain j where x_def: "x = ω + j" and j: "j ∈∘ ω" 
        by (auto elim: mem_plus_V_E)
      show ?thesis
      proof(rule VUnionI)
        from j show "Vfrom ω (succ (2ℕ * j)) ∈∘ ℛ∘ repl_ex_fun"
          unfolding repl_ex_fun_def by blast
        show "x ∈∘ Vfrom ω (succ (2ℕ * j))"
          by (rule ω_vplus_in_Vfrom_ω[OF j, folded x_def])
      qed
    qed
  qed
  ultimately have "ω + ω ∈∘ Vset (ω + ω)" by auto
  with Ord_not_in_Vset show False by auto
qed

lemma repl_ex_fun_not_in_Vset: "repl_ex_fun ∉∘ Vset (ω + ω)"
  by (rule Limit_vsv_not_in_Vset_if_vrange_not_in_Vset) 
    (auto simp: repl_ex_fun_vrange_not_in_Vset)

text‹\newpage›

end