Theory Aleph_Relative
theory Aleph_Relative
imports
CardinalArith_Relative
begin
definition
HAleph :: "[i,i] ⇒ i" where
"HAleph(i,r) ≡ if(¬(Ord(i)),i,if(i=0, nat, if(¬Limit(i) ∧ i≠0,
csucc(r`( ⋃ i )),
⋃j∈i. 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"
txt‹The extra assumptions \<^term>‹a < length(env)› and \<^term>‹c < 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
show "nth(2, Cons(a0, Cons(a1, Cons(a2, Cons(a3, Cons(a4, Cons(a5, Cons(a6, Cons(a7, env))))))))) = a2"
"nth(1, Cons(a0, Cons(a1, Cons(a2, Cons(a3, Cons(a4, Cons(a5, Cons(a6, Cons(a7, env))))))))) = a1"
"nth(0, Cons(a0, Cons(a1, Cons(a2, Cons(a3, Cons(a4, Cons(a5, Cons(a6, Cons(a7, 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 "f∈nat" "r∈nat" "env ∈ list(A)" "0∈A" "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)" "0∈A"
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"
context M_cardinal_arith_jump
begin
lemma 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
end
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,i⇒o] ⇒ 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 :
assumes "M(a)" "M(f)"
shows "∃x[M]. is_Replace(M, a, λj y. f ` j = y, x)"
proof -
have "{f`j . j∈a} = {y . j∈a , f ` j=y}"
"{y . j∈a , f ` j=y} = {y . j∈a , y =f ` j}"
by auto
moreover
note assms
moreover
have 1:"univalent(M, a, λj y. y = f ` j)"
using univalent_triv[of M a "λj .f ` j"] by auto
moreover from calculation
have "x ∈ a ⟹ y = f `x ⟹ M(y)" for x y
using transM[OF _ ‹M(a)›] by auto
moreover from this assms
have "M({f`j . j∈a})"
using RepFun_closed[OF apply_replacement] by simp
ultimately
have 2:"is_Replace(M, a, λj y. y = f ` j, {f`j . j∈a})"
using Replace_abs[of _ _ "λj y. y = f ` j",OF ‹M(a)› _ 1,THEN iffD2, simplified]
by auto
with ‹M({f`j . j∈a})›
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
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`( ⋃ succ(x) ))"
unfolding is_HAleph_def
using assms is_Limit_iff is_csucc_iff aux If_abs
by simp
lemma is_HAleph_limit :
assumes "M(f)" "M(x)" "Limit(x)" "M(res)"
shows "is_HAleph(M,x,f,res) ⟷ res = (⋃{y . i∈x ,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 . i∈x ,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 A:"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[OF ‹M(x)› _ A] 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 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)" "a≠0" "⋀ x . Ord(x) ⟹ a≠succ(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
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 SepReplace_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
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⇖ = (⋃i∈x. ℵ⇘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 ab: "a < b" and types: "M(a)" "M(b)"
shows "ℵ⇘a⇙⇗M⇖ < ℵ⇘b⇙⇗M⇖"
proof -
{ fix x
have "Ord(b)" using ab 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
apply (rule_tac OUN_upper_lt)
apply (blast intro: Card_rel_is_Ord ltD lt_Ord)
proof -
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
show ?thesis using ab by simp
qed
end
end