section‹Relativization of the cumulative hierarchy›
theory Relative_Univ
imports
"ZF-Constructible.Rank"
Internalizations
Recursion_Thms
begin
declare (in M_trivial) powerset_abs[simp]
lemma Collect_inter_Transset:
assumes
"Transset(M)" "b ∈ M"
shows
"{x∈b . P(x)} = {x∈b . P(x)} ∩ M"
using assms unfolding Transset_def
by (auto)
lemma (in M_trivial) family_union_closed: "⟦strong_replacement(M, λx y. y = f(x)); M(A); ∀x∈A. M(f(x))⟧
⟹ M(⋃x∈A. f(x))"
using RepFun_closed ..
definition
HVfrom :: "[i⇒o,i,i,i] ⇒ i" where
"HVfrom(M,A,x,f) ≡ A ∪ (⋃y∈x. {a∈Pow(f`y). M(a)})"
definition
is_powapply :: "[i⇒o,i,i,i] ⇒ o" where
"is_powapply(M,f,y,z) ≡ M(z) ∧ (∃fy[M]. fun_apply(M,f,y,fy) ∧ powerset(M,fy,z))"
lemma is_powapply_closed: "is_powapply(M,f,y,z) ⟹ M(z)"
unfolding is_powapply_def by simp
definition
is_HVfrom :: "[i⇒o,i,i,i,i] ⇒ o" where
"is_HVfrom(M,A,x,f,h) ≡ ∃U[M]. ∃R[M]. union(M,A,U,h)
∧ big_union(M,R,U) ∧ is_Replace(M,x,is_powapply(M,f),R)"
definition
is_Vfrom :: "[i⇒o,i,i,i] ⇒ o" where
"is_Vfrom(M,A,i,V) ≡ is_transrec(M,is_HVfrom(M,A),i,V)"
definition
is_Vset :: "[i⇒o,i,i] ⇒ o" where
"is_Vset(M,i,V) ≡ ∃z[M]. empty(M,z) ∧ is_Vfrom(M,z,i,V)"
subsection‹Formula synthesis›
schematic_goal sats_is_powapply_fm_auto:
assumes
"f∈nat" "y∈nat" "z∈nat" "env∈list(A)" "0∈A"
shows
"is_powapply(##A,nth(f, env),nth(y, env),nth(z, env))
⟷ sats(A,?ipa_fm(f,y,z),env)"
unfolding is_powapply_def powerset_def subset_def
using nth_closed assms
by (simp) (rule sep_rules | simp)+
schematic_goal is_powapply_iff_sats:
assumes
"nth(f,env) = ff" "nth(y,env) = yy" "nth(z,env) = zz" "0∈A"
"f ∈ nat" "y ∈ nat" "z ∈ nat" "env ∈ list(A)"
shows
"is_powapply(##A,ff,yy,zz) ⟷ sats(A, ?is_one_fm(a,r), env)"
unfolding ‹nth(f,env) = ff›[symmetric] ‹nth(y,env) = yy›[symmetric]
‹nth(z,env) = zz›[symmetric]
by (rule sats_is_powapply_fm_auto(1); simp add:assms)
definition
Hrank :: "[i,i] ⇒ i" where
"Hrank(x,f) = (⋃y∈x. succ(f`y))"
definition
PHrank :: "[i⇒o,i,i,i] ⇒ o" where
"PHrank(M,f,y,z) ≡ M(z) ∧ (∃fy[M]. fun_apply(M,f,y,fy) ∧ successor(M,fy,z))"
definition
is_Hrank :: "[i⇒o,i,i,i] ⇒ o" where
"is_Hrank(M,x,f,hc) ≡ (∃R[M]. big_union(M,R,hc) ∧is_Replace(M,x,PHrank(M,f),R)) "
definition
rrank :: "i ⇒ i" where
"rrank(a) ≡ Memrel(eclose({a}))^+"
lemma (in M_eclose) wf_rrank : "M(x) ⟹ wf(rrank(x))"
unfolding rrank_def using wf_trancl[OF wf_Memrel] .
lemma (in M_eclose) trans_rrank : "M(x) ⟹ trans(rrank(x))"
unfolding rrank_def using trans_trancl .
lemma (in M_eclose) relation_rrank : "M(x) ⟹ relation(rrank(x))"
unfolding rrank_def using relation_trancl .
lemma (in M_eclose) rrank_in_M : "M(x) ⟹ M(rrank(x))"
unfolding rrank_def by simp
subsection‹Absoluteness results›
locale M_eclose_pow = M_eclose +
assumes
power_ax : "power_ax(M)" and
powapply_replacement : "M(f) ⟹ strong_replacement(M,is_powapply(M,f))" and
HVfrom_replacement : "⟦ M(i) ; M(A) ⟧ ⟹
transrec_replacement(M,is_HVfrom(M,A),i)" and
PHrank_replacement : "M(f) ⟹ strong_replacement(M,PHrank(M,f))" and
is_Hrank_replacement : "M(x) ⟹ wfrec_replacement(M,is_Hrank(M),rrank(x))"
begin
lemma is_powapply_abs: "⟦M(f); M(y)⟧ ⟹ is_powapply(M,f,y,z) ⟷ M(z) ∧ z = {x∈Pow(f`y). M(x)}"
unfolding is_powapply_def by simp
lemma "⟦M(A); M(x); M(f); M(h) ⟧ ⟹
is_HVfrom(M,A,x,f,h) ⟷
(∃R[M]. h = A ∪ ⋃R ∧ is_Replace(M, x,λx y. y = {x ∈ Pow(f ` x) . M(x)}, R))"
using is_powapply_abs unfolding is_HVfrom_def by auto
lemma Replace_is_powapply:
assumes
"M(R)" "M(A)" "M(f)"
shows
"is_Replace(M, A, is_powapply(M, f), R) ⟷ R = Replace(A,is_powapply(M,f))"
proof -
have "univalent(M,A,is_powapply(M,f))"
using ‹M(A)› ‹M(f)› unfolding univalent_def is_powapply_def by simp
moreover
have "⋀x y. ⟦ x∈A; is_powapply(M,f,x,y) ⟧ ⟹ M(y)"
using ‹M(A)› ‹M(f)› unfolding is_powapply_def by simp
ultimately
show ?thesis using ‹M(A)› ‹M(R)› Replace_abs by simp
qed
lemma powapply_closed:
"⟦ M(y) ; M(f) ⟧ ⟹ M({x ∈ Pow(f ` y) . M(x)})"
using apply_closed power_ax unfolding power_ax_def by simp
lemma RepFun_is_powapply:
assumes
"M(R)" "M(A)" "M(f)"
shows
"Replace(A,is_powapply(M,f)) = RepFun(A,λy.{x∈Pow(f`y). M(x)})"
proof -
have "{y . x ∈ A, M(y) ∧ y = {x ∈ Pow(f ` x) . M(x)}} = {y . x ∈ A, y = {x ∈ Pow(f ` x) . M(x)}}"
using assms powapply_closed transM[of _ A] by blast
also
have " ... = {{x ∈ Pow(f ` y) . M(x)} . y ∈ A}" by auto
finally
show ?thesis using assms is_powapply_abs transM[of _ A] by simp
qed
lemma RepFun_powapply_closed:
assumes
"M(f)" "M(A)"
shows
"M(Replace(A,is_powapply(M,f)))"
proof -
have "univalent(M,A,is_powapply(M,f))"
using ‹M(A)› ‹M(f)› unfolding univalent_def is_powapply_def by simp
moreover
have "⟦ x∈A ; is_powapply(M,f,x,y) ⟧ ⟹ M(y)" for x y
using assms unfolding is_powapply_def by simp
ultimately
show ?thesis using assms powapply_replacement by simp
qed
lemma Union_powapply_closed:
assumes
"M(x)" "M(f)"
shows
"M(⋃y∈x. {a∈Pow(f`y). M(a)})"
proof -
have "M({a∈Pow(f`y). M(a)})" if "y∈x" for y
using that assms transM[of _ x] powapply_closed by simp
then
have "M({{a∈Pow(f`y). M(a)}. y∈x})"
using assms transM[of _ x] RepFun_powapply_closed RepFun_is_powapply by simp
then show ?thesis using assms by simp
qed
lemma relation2_HVfrom: "M(A) ⟹ relation2(M,is_HVfrom(M,A),HVfrom(M,A))"
unfolding is_HVfrom_def HVfrom_def relation2_def
using Replace_is_powapply RepFun_is_powapply
Union_powapply_closed RepFun_powapply_closed by auto
lemma HVfrom_closed :
"M(A) ⟹ ∀x[M]. ∀g[M]. function(g) ⟶ M(HVfrom(M,A,x,g))"
unfolding HVfrom_def using Union_powapply_closed by simp
lemma transrec_HVfrom:
assumes "M(A)"
shows "Ord(i) ⟹ {x∈Vfrom(A,i). M(x)} = transrec(i,HVfrom(M,A))"
proof (induct rule:trans_induct)
case (step i)
have "Vfrom(A,i) = A ∪ (⋃y∈i. Pow((λx∈i. Vfrom(A, x)) ` y))"
using def_transrec[OF Vfrom_def, of A i] by simp
then
have "Vfrom(A,i) = A ∪ (⋃y∈i. Pow(Vfrom(A, y)))"
by simp
then
have "{x∈Vfrom(A,i). M(x)} = {x∈A. M(x)} ∪ (⋃y∈i. {x∈Pow(Vfrom(A, y)). M(x)})"
by auto
with ‹M(A)›
have "{x∈Vfrom(A,i). M(x)} = A ∪ (⋃y∈i. {x∈Pow(Vfrom(A, y)). M(x)})"
by (auto intro:transM)
also
have "... = A ∪ (⋃y∈i. {x∈Pow({z∈Vfrom(A,y). M(z)}). M(x)})"
proof -
have "{x∈Pow(Vfrom(A, y)). M(x)} = {x∈Pow({z∈Vfrom(A,y). M(z)}). M(x)}"
if "y∈i" for y by (auto intro:transM)
then
show ?thesis by simp
qed
also from step
have " ... = A ∪ (⋃y∈i. {x∈Pow(transrec(y, HVfrom(M, A))). M(x)})" by auto
also
have " ... = transrec(i, HVfrom(M, A))"
using def_transrec[of "λy. transrec(y, HVfrom(M, A))" "HVfrom(M, A)" i,symmetric]
unfolding HVfrom_def by simp
finally
show ?case .
qed
lemma Vfrom_abs: "⟦ M(A); M(i); M(V); Ord(i) ⟧ ⟹ is_Vfrom(M,A,i,V) ⟷ V = {x∈Vfrom(A,i). M(x)}"
unfolding is_Vfrom_def
using relation2_HVfrom HVfrom_closed HVfrom_replacement
transrec_abs[of "is_HVfrom(M,A)" i "HVfrom(M,A)"] transrec_HVfrom by simp
lemma Vfrom_closed: "⟦ M(A); M(i); Ord(i) ⟧ ⟹ M({x∈Vfrom(A,i). M(x)})"
unfolding is_Vfrom_def
using relation2_HVfrom HVfrom_closed HVfrom_replacement
transrec_closed[of "is_HVfrom(M,A)" i "HVfrom(M,A)"] transrec_HVfrom by simp
lemma Vset_abs: "⟦ M(i); M(V); Ord(i) ⟧ ⟹ is_Vset(M,i,V) ⟷ V = {x∈Vset(i). M(x)}"
using Vfrom_abs unfolding is_Vset_def by simp
lemma Vset_closed: "⟦ M(i); Ord(i) ⟧ ⟹ M({x∈Vset(i). M(x)})"
using Vfrom_closed unfolding is_Vset_def by simp
lemma Hrank_trancl:"Hrank(y, restrict(f,Memrel(eclose({x}))-``{y}))
= Hrank(y, restrict(f,(Memrel(eclose({x}))^+)-``{y}))"
unfolding Hrank_def
using restrict_trans_eq by simp
lemma rank_trancl: "rank(x) = wfrec(rrank(x), x, Hrank)"
proof -
have "rank(x) = wfrec(Memrel(eclose({x})), x, Hrank)"
(is "_ = wfrec(?r,_,_)")
unfolding rank_def transrec_def Hrank_def by simp
also
have " ... = wftrec(?r^+, x, λy f. Hrank(y, restrict(f,?r-``{y})))"
unfolding wfrec_def ..
also
have " ... = wftrec(?r^+, x, λy f. Hrank(y, restrict(f,(?r^+)-``{y})))"
using Hrank_trancl by simp
also
have " ... = wfrec(?r^+, x, Hrank)"
unfolding wfrec_def using trancl_eq_r[OF relation_trancl trans_trancl] by simp
finally
show ?thesis unfolding rrank_def .
qed
lemma univ_PHrank : "⟦ M(z) ; M(f) ⟧ ⟹ univalent(M,z,PHrank(M,f))"
unfolding univalent_def PHrank_def by simp
lemma PHrank_abs :
"⟦ M(f) ; M(y) ⟧ ⟹ PHrank(M,f,y,z) ⟷ M(z) ∧ z = succ(f`y)"
unfolding PHrank_def by simp
lemma PHrank_closed : "PHrank(M,f,y,z) ⟹ M(z)"
unfolding PHrank_def by simp
lemma Replace_PHrank_abs:
assumes
"M(z)" "M(f)" "M(hr)"
shows
"is_Replace(M,z,PHrank(M,f),hr) ⟷ hr = Replace(z,PHrank(M,f))"
proof -
have "⋀x y. ⟦x∈z; PHrank(M,f,x,y) ⟧ ⟹ M(y)"
using ‹M(z)› ‹M(f)› unfolding PHrank_def by simp
then
show ?thesis using ‹M(z)› ‹M(hr)› ‹M(f)› univ_PHrank Replace_abs by simp
qed
lemma RepFun_PHrank:
assumes
"M(R)" "M(A)" "M(f)"
shows
"Replace(A,PHrank(M,f)) = RepFun(A,λy. succ(f`y))"
proof -
have "{z . y ∈ A, M(z) ∧ z = succ(f`y)} = {z . y ∈ A, z = succ(f`y)}"
using assms PHrank_closed transM[of _ A] by blast
also
have " ... = {succ(f`y) . y ∈ A}" by auto
finally
show ?thesis using assms PHrank_abs transM[of _ A] by simp
qed
lemma RepFun_PHrank_closed :
assumes
"M(f)" "M(A)"
shows
"M(Replace(A,PHrank(M,f)))"
proof -
have "⟦ x∈A ; PHrank(M,f,x,y) ⟧ ⟹ M(y)" for x y
using assms unfolding PHrank_def by simp
with univ_PHrank
show ?thesis using assms PHrank_replacement by simp
qed
lemma relation2_Hrank :
"relation2(M,is_Hrank(M),Hrank)"
unfolding is_Hrank_def Hrank_def relation2_def
using Replace_PHrank_abs RepFun_PHrank RepFun_PHrank_closed by auto
lemma Union_PHrank_closed:
assumes
"M(x)" "M(f)"
shows
"M(⋃y∈x. succ(f`y))"
proof -
have "M(succ(f`y))" if "y∈x" for y
using that assms transM[of _ x] by simp
then
have "M({succ(f`y). y∈x})"
using assms transM[of _ x] RepFun_PHrank_closed RepFun_PHrank by simp
then show ?thesis using assms by simp
qed
lemma is_Hrank_closed :
"M(A) ⟹ ∀x[M]. ∀g[M]. function(g) ⟶ M(Hrank(x,g))"
unfolding Hrank_def using RepFun_PHrank_closed Union_PHrank_closed by simp
lemma rank_closed: "M(a) ⟹ M(rank(a))"
unfolding rank_trancl
using relation2_Hrank is_Hrank_closed is_Hrank_replacement
wf_rrank relation_rrank trans_rrank rrank_in_M
trans_wfrec_closed[of "rrank(a)" a "is_Hrank(M)"] by simp
lemma M_into_Vset:
assumes "M(a)"
shows "∃i[M]. ∃V[M]. ordinal(M,i) ∧ is_Vfrom(M,0,i,V) ∧ a∈V"
proof -
let ?i="succ(rank(a))"
from assms
have "a∈{x∈Vfrom(0,?i). M(x)}" (is "a∈?V")
using Vset_Ord_rank_iff by simp
moreover from assms
have "M(?i)"
using rank_closed by simp
moreover
note ‹M(a)›
moreover from calculation
have "M(?V)"
using Vfrom_closed by simp
moreover from calculation
have "ordinal(M,?i) ∧ is_Vfrom(M, 0, ?i, ?V) ∧ a ∈ ?V"
using Ord_rank Vfrom_abs by simp
ultimately
show ?thesis by blast
qed
end
end