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 intermediate for "is_HAleph_fm"
lemma arity_is_HAleph_fm_aux:
assumes
"i ∈ nat" "r ∈ nat"
shows
"arity(Replace_fm(8 +⇩ω i, ⋅10 +⇩ω r`0 is 1⋅, 3)) = 9 +⇩ω i ∪ pred(pred(11 +⇩ω r))"
using arity_Replace_fm[of "⋅ (10+⇩ωr)`0 is 1⋅" "8+⇩ωi" 3 "(11+⇩ωr) ∪ 1 ∪ 2"]
ord_simp_union
by (auto simp:arity)
lemma arity_is_HAleph_fm[arity]:
assumes
"i ∈ nat" "r ∈ nat" "l ∈ nat"
shows
"arity(is_HAleph_fm(i, r, l)) = succ(i) ∪ succ(l) ∪ succ(r)"
using assms pred_Un arity_is_HAleph_fm_aux arity_is_HAleph_fm'
by auto
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 [source] 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 "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"
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,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_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 . 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 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 . j∈a})"
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 . j∈a})"
using Replace_abs[of _ _ "λj y. y = f ` j",OF ‹M(a)›,THEN iffD2]
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_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 . 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 "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)" "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_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
locale M_aleph = M_pre_aleph +
assumes
aleph_rel_separation: "Ord(x) ⟹ M(x) ⟹ separation(M, λy. ∃z∈x. y = ℵ⇘z⇙⇗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 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
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 "Ord(x)"
using Limit_is_Ord by simp
from this
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 by simp
moreover from ‹Ord(x)›
have "{y . z ∈ x, M(y) ∧ M(z) ∧ Ord(z) ∧ y = ℵ⇘z⇙⇗M⇖} = {y . z ∈ x, M(z) ∧ y = ℵ⇘z⇙⇗M⇖}"
using Ord_in_Ord by blast
moreover from ‹Ord(x)› ‹M(x)›
have "{y . z ∈ x, M(z) ∧ y = ℵ⇘z⇙⇗M⇖} ⊆ ℵ⇘x⇙⇗M⇖"
using Aleph_rel_increasing
by (auto dest:ltD transM intro:ltI)
with calculation
have "{y . z ∈ x, M(z) ∧ y = ℵ⇘z⇙⇗M⇖} = {y ∈ ℵ⇘x⇙⇗M⇖ . (∃z ∈ x. y = ℵ⇘z⇙⇗M⇖)}"
by (blast dest:transM)
with calculation
have "{y . z ∈ x, M(y) ∧ M(z) ∧ y = ℵ⇘z⇙⇗M⇖} = {y ∈ ℵ⇘x⇙⇗M⇖ . (∃z ∈ x. y = ℵ⇘z⇙⇗M⇖)}"
by simp
moreover from ‹Ord(x)› ‹M(x)›
have "M({y ∈ ℵ⇘x⇙⇗M⇖ . (∃z ∈ x. y = ℵ⇘z⇙⇗M⇖)})"
using aleph_rel_separation
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
lemmas nat_subset_Aleph_rel_1 =
Ord_lt_subset[OF Ord_Aleph_rel[of 1] Aleph_rel_increasing[of 0 1,simplified],simplified]
end
end