Theory Aleph_Relative

theory Aleph_Relative
  imports
    Univ_Relative
    CardinalArith_Relative
    Cardinal_Relative
begin

definition
  HAleph :: "[i,i]  i" where
  "HAleph(i,r)  if(¬(Ord(i)),i,if(i=0, nat, if(¬Limit(i)  i0,
                            csucc(r`(  i )),
                                   ji. r`j)))"

reldb_add functional "Limit" "Limit"
relationalize "Limit" "is_Limit" external
synthesize "is_Limit" from_definition
arity_theorem for "is_Limit_fm"

relativize functional "HAleph" "HAleph_rel"
relationalize "HAleph_rel" "is_HAleph"

synthesize "is_HAleph" from_definition assuming "nonempty"
arity_theorem for "is_HAleph_fm"

definition
  Aleph' :: "i => i"  where
  "Aleph'(a) == transrec(a,λi r. HAleph(i,r))"

relativize functional "Aleph'" "Aleph_rel"
relationalize "Aleph_rel" "is_Aleph"

txtThe extra assumptions terma < length(env) and termc < length(env)
    in this schematic goal (and the following results on synthesis that
    depend on it) are imposed by @{thm is_transrec_iff_sats}.
schematic_goal sats_is_Aleph_fm_auto:
  "a  nat  c  nat  env  list(A) 
  a < length(env)  c < length(env)  0  A 
  is_Aleph(##A, nth(a, env), nth(c, env))  A, env  ?fm(a, c)"
  unfolding is_Aleph_def
proof (rule is_transrec_iff_sats, rule_tac [1] is_HAleph_iff_sats)
  fix a0 a1 a2 a3 a4 a5 a6 a7
  let ?env' = "Cons(a0, Cons(a1, Cons(a2, Cons(a3, Cons(a4, Cons(a5, Cons(a6, Cons(a7, env))))))))"
  show "nth(2, ?env') = a2"
    "nth(1, ?env') = a1"
    "nth(0, ?env') = a0"
    "nth(c, env) = nth(c, env)"
    by simp_all
qed simp_all

synthesize_notc "is_Aleph" from_schematic

notation is_Aleph_fm (⋅ℵ'(_') is _)

lemma is_Aleph_fm_type [TC]: "a  nat  c  nat  is_Aleph_fm(a, c)  formula"
  unfolding is_Aleph_fm_def by simp

lemma sats_is_Aleph_fm:
  assumes "fnat" "rnat" "env  list(A)" "0A" "f < length(env)" "r< length(env)"
  shows "is_Aleph(##A, nth(f, env), nth(r, env))  A, env  is_Aleph_fm(f,r)"
  using assms sats_is_Aleph_fm_auto unfolding is_Aleph_def is_Aleph_fm_def by simp

lemma is_Aleph_iff_sats [iff_sats]:
  assumes
    "nth(f, env) = fa" "nth(r, env) = ra" "f < length(env)" "r< length(env)"
    "f  nat" "r  nat" "env  list(A)" "0A"
  shows "is_Aleph(##A,fa,ra)  A, env  is_Aleph_fm(f,r)"
  using assms sats_is_Aleph_fm[of f r env A] by simp

arity_theorem for "is_Aleph_fm"

lemma (in M_cardinal_arith_jump) is_Limit_iff:
  assumes "M(a)"
  shows "is_Limit(M,a)  Limit(a)"
  unfolding is_Limit_def Limit_def using lt_abs transM[OF ltD M(a)] assms
  by auto

lemma HAleph_eq_Aleph_recursive:
  "Ord(i)  HAleph(i,r) = (if i = 0 then nat
                else if j. i = succ(j) then csucc(r ` (THE j. i = succ(j))) else j<i. r ` j)"
proof -
  assume "Ord(i)"
  moreover from this
  have "i = succ(j)  (succ(j)) = j" for j
    using Ord_Union_succ_eq by simp
  moreover from Ord(i)
  have "(j. i = succ(j))  ¬Limit(i)  i  0"
    using Ord_cases_disj by auto
  ultimately
  show ?thesis
    unfolding HAleph_def OUnion_def
    by auto
qed

lemma Aleph'_eq_Aleph: "Ord(a)  Aleph'(a) = Aleph(a)"
  unfolding Aleph'_def Aleph_def transrec2_def
  using HAleph_eq_Aleph_recursive
  by (intro transrec_equal_on_Ord) auto

reldb_rem functional "Aleph'"
reldb_rem relational "is_Aleph"
reldb_add functional "Aleph" "Aleph_rel"
reldb_add relational "Aleph" "is_Aleph"

abbreviation
  Aleph_r :: "[i,io]  i" (ℵ⇘_⇙⇗_) where
  "Aleph_r(a,M)  Aleph_rel(M,a)"

abbreviation
  Aleph_r_set :: "[i,i]  i" (ℵ⇘_⇙⇗_) where
  "Aleph_r_set(a,M)  Aleph_rel(##M,a)"

lemma Aleph_rel_def': "Aleph_rel(M,a)  transrec(a, λi r. HAleph_rel(M, i, r))"
  unfolding Aleph_rel_def .

lemma succ_mem_Limit: "Limit(j)  i  j  succ(i)  j"
  using Limit_has_succ[THEN ltD] ltI Limit_is_Ord by auto

locale M_pre_aleph = M_eclose + M_cardinal_arith_jump +
  assumes
    haleph_transrec_replacement: "M(a)  transrec_replacement(M,is_HAleph(M),a)"

begin

lemma aux_ex_Replace_funapply:
  assumes "M(a)" "M(f)"
  shows "x[M]. is_Replace(M, a, λj y. f ` j = y, x)"
proof -
  have "{f`j . ja} = {y . ja , f ` j=y}"
    "{y . ja , f ` j=y} = {y . ja , y =f ` j}"
    by auto
  moreover
  note assms
  moreover from calculation
  have "x  a  y = f `x  M(y)" for x y
    using transM[OF _ M(a)] by auto
  moreover from assms
  have "M({f`j . ja})"
    using transM[OF _ M(a)] RepFun_closed[OF apply_replacement] by simp
  ultimately
  have 2:"is_Replace(M, a, λj y. y = f ` j, {f`j . ja})"
    using Replace_abs[of _ _ "λj y. y = f ` j",OF M(a),THEN iffD2]
    by auto
  with M({f`j . ja})
  show ?thesis
    using
      is_Replace_cong[of _ _ M "λj y. y = f ` j" "λj y. f ` j = y", THEN iffD1,OF _ _ _ 2]
    by auto
qed

lemma is_HAleph_zero:
  assumes "M(f)"
  shows "is_HAleph(M,0,f,res)  res = nat"
  unfolding is_HAleph_def
  using Ord_0 If_abs is_Limit_iff is_csucc_iff assms aux_ex_Replace_funapply
  by auto

lemma is_HAleph_succ:
  assumes "M(f)" "M(x)" "Ord(x)" "M(res)"
  shows "is_HAleph(M,succ(x),f,res)  res = csucc_rel(M,f`x)"
  unfolding is_HAleph_def
  using assms is_Limit_iff is_csucc_iff aux_ex_Replace_funapply If_abs Ord_Union_succ_eq
  by simp

lemma is_HAleph_limit:
  assumes "M(f)" "M(x)" "Limit(x)" "M(res)"
  shows "is_HAleph(M,x,f,res)  res = ({y . ix ,M(i)  M(y)  y = f`i})"
proof -
  from assms
  have "univalent(M, x, λj y. y = f ` j  )"
    "(xa y. xa  x  f ` xa = y  M(y))"
    "{y . x  x, f ` x = y} = {y . ix ,M(i)  M(y)  y = f`i}"
    using univalent_triv[of M x "λj .f ` j"] transM[OF _ M(x)]
    by auto
  moreover
  from this
  have "univalent(M, x, λj y. f ` j = y )"
    by (rule_tac univalent_cong[of x x M " λj y. y = f ` j" " λj y. f ` j=y",THEN iffD1], auto)
  moreover
  from this
  have "univalent(M, x, λj y. M(j)  M(y)  f ` j = y )"
    by auto
  ultimately
  show ?thesis
    unfolding is_HAleph_def
    using assms is_Limit_iff Limit_is_Ord zero_not_Limit If_abs is_csucc_iff
      Replace_abs apply_replacement
    by auto
qed

lemma is_HAleph_iff:
  assumes "M(a)" "M(f)" "M(res)"
  shows "is_HAleph(M, a, f, res)  res = HAleph_rel(M, a, f)"
proof(cases "Ord(a)")
  case True
  note Ord_cases[OF Ord(a)]
  then
  show ?thesis
  proof(cases )
    case 1
    with True assms
    show ?thesis
      using is_HAleph_zero unfolding HAleph_rel_def
      by simp
  next
    case (2 j)
    with True assms
    show ?thesis
      using is_HAleph_succ Ord_Union_succ_eq
      unfolding HAleph_rel_def
      by simp
  next
    case 3
    with assms
    show ?thesis
      using is_HAleph_limit zero_not_Limit Limit_is_Ord
      unfolding HAleph_rel_def
      by auto
  qed
next
  case False
  then
  have "¬Limit(a)" "a0" " x . Ord(x)  asucc(x)"
    using Limit_is_Ord by auto
  with False
  show ?thesis
    unfolding is_HAleph_def HAleph_rel_def
    using assms is_Limit_iff If_abs is_csucc_iff aux_ex_Replace_funapply
    by auto
qed

lemma HAleph_rel_closed [intro,simp]:
  assumes "function(f)" "M(a)" "M(f)"
  shows "M(HAleph_rel(M,a,f))"
  unfolding HAleph_rel_def
  using assms apply_replacement
  by simp

lemma Aleph_rel_closed[intro, simp]:
  assumes "Ord(a)" "M(a)"
  shows "M(Aleph_rel(M,a))"
proof -
  have "relation2(M, is_HAleph(M), HAleph_rel(M))"
    unfolding relation2_def using is_HAleph_iff assms by simp
  moreover
  have "x[M]. g[M]. function(g)  M(HAleph_rel(M, x, g))"
    using HAleph_rel_closed by simp
  moreover
  note assms
  ultimately
  show ?thesis
    unfolding Aleph_rel_def
    using transrec_closed[of "is_HAleph(M)" a "HAleph_rel(M)"]
      haleph_transrec_replacement  by simp
qed

lemma Aleph_rel_zero: "ℵ⇘0⇙⇗M= nat"
  using def_transrec [OF Aleph_rel_def',of _ 0]
  unfolding HAleph_rel_def by simp

lemma Aleph_rel_succ: "Ord(α)  M(α)  ℵ⇘succ(α)⇙⇗M= (ℵ⇘α⇙⇗M+)⇗M"
  using Ord_Union_succ_eq
  by (subst def_transrec [OF Aleph_rel_def'])
    (simp add:HAleph_rel_def)

lemma Aleph_rel_limit:
  assumes "Limit(α)" "M(α)"
  shows "ℵ⇘α⇙⇗M= {ℵ⇘j⇙⇗M. j  α}"
proof -
  note trans=transM[OF _ M(α)]
  from M(α)
  have "ℵ⇘α⇙⇗M= HAleph_rel(M, α, λxα. ℵ⇘x⇙⇗M)"
    using def_transrec [OF Aleph_rel_def',of M α] by simp
  also
  have "... = {a . j  α, M(a)  a = ℵ⇘j⇙⇗M}"
    unfolding HAleph_rel_def
    using assms zero_not_Limit Limit_is_Ord trans by auto
  also
  have "... = {ℵ⇘j⇙⇗M. j  α}"
    using Aleph_rel_closed[OF _ trans] Ord_in_Ord Limit_is_Ord[OF Limit(α)] by auto
  finally
  show ?thesis .
qed

lemma is_Aleph_iff:
  assumes "Ord(a)" "M(a)" "M(res)"
  shows "is_Aleph(M, a, res)  res = ℵ⇘a⇙⇗M"
proof -
  have "relation2(M, is_HAleph(M), HAleph_rel(M))"
    unfolding relation2_def using is_HAleph_iff assms by simp
  moreover
  have "x[M]. g[M]. function(g)  M(HAleph_rel(M, x, g))"
    using HAleph_rel_closed by simp
  ultimately
  show ?thesis
    using assms transrec_abs haleph_transrec_replacement
    unfolding is_Aleph_def Aleph_rel_def
    by simp
qed

end ― ‹localeM_pre_aleph

locale M_aleph = M_pre_aleph +
  assumes
    aleph_rel_replacement: "strong_replacement(M, λx y. Ord(x)  y = ℵ⇘x⇙⇗M)"
begin

lemma Aleph_rel_cont: "Limit(l)  M(l)  ℵ⇘l⇙⇗M= (i<l. ℵ⇘i⇙⇗M)"
  using Limit_is_Ord Aleph_rel_limit
  by (simp add:OUnion_def)

lemma Ord_Aleph_rel:
  assumes "Ord(a)"
  shows "M(a)  Ord(ℵ⇘a⇙⇗M)"
  using Ord(a)
proof(induct a rule:trans_induct3)
  case 0
  show ?case using Aleph_rel_zero by simp
next
  case (succ x)
  with Ord(x)
  have "M(x)" "Ord(ℵ⇘x⇙⇗M)" by simp_all
  with Ord(x)
  have "Ord(csucc_rel(M,ℵ⇘x⇙⇗M))"
    using Card_rel_is_Ord Card_rel_csucc_rel
    by simp
  with Ord(x) M(x)
  show ?case using Aleph_rel_succ by simp
next
  case (limit x)
  note trans=transM[OF _ M(x)]
  from limit
  have "ℵ⇘x⇙⇗M= (ix. ℵ⇘i⇙⇗M)"
    using Aleph_rel_cont OUnion_def Limit_is_Ord
    by auto
  with limit
  show ?case using Ord_UN trans by auto
qed

lemma Card_rel_Aleph_rel [simp, intro]:
  assumes "Ord(a)" and types: "M(a)" shows "Card⇗M⇖(ℵ⇘a⇙⇗M)"
  using assms
proof (induct rule:trans_induct3)
  case 0
  then
  show ?case
    using Aleph_rel_zero Card_rel_nat by simp
next
  case (succ x)
  then
  show ?case
    using Card_rel_csucc_rel Ord_Aleph_rel Aleph_rel_succ
    by simp
next
  case (limit x)
  moreover
  from this
  have "M({y . z  x, M(y)  M(z)  Ord(z)  y = ℵ⇘z⇙⇗M})"
    using aleph_rel_replacement
    by auto
  moreover
  have "{y . z  x, M(y)  M(z)  y = ℵ⇘z⇙⇗M} = {y . z  x, M(y)  M(z)  Ord(z)  y = ℵ⇘z⇙⇗M}"
    using Ord_in_Ord Limit_is_Ord[OF limit(1)] by simp
  ultimately
  show ?case
    using Ord_Aleph_rel Card_nat Limit_is_Ord Card_relI
    by (subst def_transrec [OF Aleph_rel_def'])
      (auto simp add:HAleph_rel_def)
qed

lemma Aleph_rel_increasing:
  assumes "a < b" and types: "M(a)" "M(b)"
  shows "ℵ⇘a⇙⇗M< ℵ⇘b⇙⇗M"
proof -
  { fix x
    from assms
    have "Ord(b)"
      by (blast intro: lt_Ord2)
    moreover
    assume "M(x)"
    moreover
    note M(b)
    ultimately
    have "x < b  ℵ⇘x⇙⇗M< ℵ⇘b⇙⇗M"
    proof (induct b arbitrary: x rule: trans_induct3)
      case 0 thus ?case by simp
    next
      case (succ b)
      then
      show ?case
        using Card_rel_csucc_rel Ord_Aleph_rel Ord_Union_succ_eq lt_csucc_rel
          lt_trans[of _ "ℵ⇘b⇙⇗M" "csucc⇗M⇖(ℵ⇘b⇙⇗M)"]
        by (subst (2) def_transrec[OF Aleph_rel_def'])
          (auto simp add: le_iff HAleph_rel_def)
    next
      case (limit l)
      then
      have sc: "succ(x) < l"
        by (blast intro: Limit_has_succ)
      then
      have "ℵ⇘x⇙⇗M< (j<l. ℵ⇘j⇙⇗M)"
        using limit Ord_Aleph_rel Ord_OUN
      proof(rule_tac OUN_upper_lt,blast intro: Card_rel_is_Ord ltD lt_Ord)
        from x<l Limit(l)
        have "Ord(x)"
          using Limit_is_Ord Ord_in_Ord
          by (auto dest!:ltD)
        with M(x)
        show "ℵ⇘x⇙⇗M< ℵ⇘succ(x)⇙⇗M"
          using Card_rel_csucc_rel Ord_Aleph_rel lt_csucc_rel
            ltD[THEN [2] Ord_in_Ord] succ_in_MI[OF M(x)]
            Aleph_rel_succ[of x]
          by (simp)
      next
        from M(l) Limit(l)
        show "Ord(j<l. ℵ⇘j⇙⇗M)"
          using Ord_Aleph_rel lt_Ord Limit_is_Ord Ord_in_Ord
          by (rule_tac Ord_OUN)
            (auto dest:transM ltD intro!:Ord_Aleph_rel)
      qed
      then
      show ?case using limit Aleph_rel_cont by simp
    qed
  }
  with types assms
  show ?thesis by simp
qed


end ― ‹localeM_aleph

end