# Theory Univ_Relative

```section‹Relativization of the cumulative hierarchy›
theory Univ_Relative
imports
"ZF-Constructible.Rank"
"ZF.Univ"
Discipline_Cardinal

begin

declare arity_ordinal_fm[arity]

context M_trivial
begin
declare powerset_abs[simp]

lemma 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 ..

lemma family_union_closed': "⟦strong_replacement(M, λx y. x∈A ∧ y = f(x)); M(A); ∀x∈A. M(f(x))⟧
⟹ M(⋃x∈A. f(x))"
using RepFun_closed2
by simp

end ― ‹\<^locale>‹M_trivial››

definition
HVfrom :: "[i,i,i] ⇒ i" where
"HVfrom(A,x,f) ≡ A ∪ (⋃y∈x. Powapply(f,y))"

relativize functional "HVfrom" "HVfrom_rel"
relationalize "HVfrom_rel" "is_HVfrom"
synthesize "is_HVfrom" from_definition assuming "nonempty"
arity_theorem intermediate for "is_HVfrom_fm"

lemma arity_is_HVfrom_fm:
"A ∈ nat ⟹
x ∈ nat ⟹
f ∈ nat ⟹
d ∈ nat ⟹
arity(is_HVfrom_fm(A, x, f, d)) = succ(A) ∪ succ(d) ∪ (succ(x) ∪ succ(f))"
using arity_is_HVfrom_fm' arity_is_Powapply_fm
by(simp,subst arity_Replace_fm[of "is_Powapply_fm(succ(succ(succ(succ(f)))), 0, 1)" "succ(succ(x))" 1])

notation HVfrom_rel (‹HVfrom⇗_⇖'(_,_,_')›)

locale M_HVfrom = M_eclose +
assumes
Powapply_replacement:
"M(f) ⟹ strong_replacement(M,λy z. z = Powapply⇗M⇖(f,y))"
begin

is_iff_rel for "HVfrom"
proof -
assume assms:"M(A)" "M(x)" "M(f)" "M(res)"
then
have "is_Replace(M,x,λy z. z = Powapply⇗M⇖(f,y),r) ⟷ r = {z . y∈x, z = Powapply⇗M⇖(f,y)}"
if "M(r)" for r
using that Powapply_rel_closed
Replace_abs[of x r "λy z. z = Powapply⇗M⇖(f,y)"] transM[of _ x]
by simp
moreover
have "is_Replace(M,x,is_Powapply(M,f),r) ⟷
is_Replace(M,x,λy z. z = Powapply⇗M⇖(f,y),r)" if "M(r)" for r
using assms that is_Powapply_iff is_Replace_cong
by simp
ultimately
have "is_Replace(M,x,is_Powapply(M,f),r) ⟷ r = {z . y∈x, z = Powapply⇗M⇖(f,y)}"
if "M(r)" for r
using that assms
by simp
moreover
have "M({z . y ∈ x, z = Powapply⇗M⇖(f,y)})"
using assms strong_replacement_closed[OF Powapply_replacement]
Powapply_rel_closed transM[of _ x]
by simp
moreover from assms
― ‹intermediate step for body of Replace›
have "{z . y ∈ x, z = Powapply⇗M⇖(f,y)} = {y . w ∈ x, M(y) ∧ M(w) ∧ y = Powapply⇗M⇖(f,w)}"
by (auto dest:transM)
ultimately
show ?thesis
using assms
unfolding is_HVfrom_def HVfrom_rel_def
by (auto dest:transM)
qed

rel_closed for "HVfrom"
proof -
assume assms:"M(A)" "M(x)" "M(f)"
have "M({z . y ∈ x, z = Powapply⇗M⇖(f,y)})"
using assms strong_replacement_closed[OF Powapply_replacement]
Powapply_rel_closed transM[of _ x]
by simp
then
have "M(A ∪ ⋃({z . y∈x, z = Powapply⇗M⇖(f,y)}))"
using assms
by simp
moreover from assms
― ‹intermediate step for body of Replace›
have "{z . y ∈ x, z = Powapply⇗M⇖(f,y)} = {y . w ∈ x, M(y) ∧ M(w) ∧ y = Powapply⇗M⇖(f,w)}"
by (auto dest:transM)
ultimately
show ?thesis
using assms
unfolding HVfrom_rel_def
by simp
qed

end ― ‹\<^locale>‹M_HVfrom››

definition
Vfrom_rel :: "[i⇒o,i,i] ⇒ i" (‹Vfrom⇗_⇖'(_,_')›) where
"Vfrom⇗M⇖(A,i) = transrec(i, HVfrom_rel(M,A))"

definition
is_Vfrom :: "[i⇒o,i,i,i] ⇒ o" where
"is_Vfrom(M,A,i,z) ≡ is_transrec(M,is_HVfrom(M,A),i,z)"

definition
Hrank :: "[i,i] ⇒ i" where
"Hrank(x,f) ≡ (⋃y∈x. succ(f`y))"

definition
rrank :: "i ⇒ i" where
"rrank(a) ≡ Memrel(eclose({a}))^+"

relativize functional "Hrank" "Hrank_rel"
relationalize "Hrank_rel" "is_Hrank"
synthesize "is_Hrank" from_definition assuming "nonempty"

lemma arity_is_Hrank_fm : "x ∈ nat ⟹
f ∈ nat ⟹
d ∈ nat ⟹
arity(is_Hrank_fm(x, f, d)) =
succ(d) ∪ succ(x) ∪ succ(f)"
unfolding is_Hrank_fm_def
using  arity_fun_apply_fm arity_big_union_fm
arity_fun_apply_fm arity_succ_fm arity_And arity_Exists
arity_Replace_fm[of
"(⋅∃⋅⋅succ(0) is 2⋅ ∧ ⋅ succ(succ(succ(succ(f))))`1 is 0⋅⋅⋅)"
"succ(x)" 0 "4+⇩ωf"]

locale M_Vfrom = M_HVfrom +
assumes
trepl_HVfrom : "⟦ M(A);M(i) ⟧ ⟹ transrec_replacement(M,is_HVfrom(M,A),i)"
and
Hrank_replacement : "M(f) ⟹ strong_replacement(M,λx y . y = succ(f`x))"
and
is_Hrank_replacement : "M(x) ⟹ wfrec_replacement(M,is_Hrank(M),rrank(x))"
and
HVfrom_replacement : "⟦ M(i) ; M(A) ⟧ ⟹
transrec_replacement(M,is_HVfrom(M,A),i)"

begin

lemma Vfrom_rel_iff :
assumes "M(A)" "M(i)" "M(z)" "Ord(i)"
shows "is_Vfrom(M,A,i,z) ⟷ z = Vfrom⇗M⇖(A,i)"
proof -
have "relation2(M, is_HVfrom(M, A), HVfrom_rel(M, A))"
using assms is_HVfrom_iff
unfolding relation2_def
by simp
then
show ?thesis
using assms HVfrom_rel_closed trepl_HVfrom
transrec_abs[of "is_HVfrom(M,A)" i "HVfrom_rel(M,A)" z]
unfolding is_Vfrom_def Vfrom_rel_def
by simp
qed

lemma relation2_HVfrom: "M(A) ⟹ relation2(M,is_HVfrom(M,A),HVfrom_rel(M,A))"
using is_HVfrom_iff
unfolding relation2_def
by auto

lemma HVfrom_closed :
"M(A) ⟹ ∀x[M]. ∀g[M]. function(g) ⟶ M(HVfrom_rel(M,A,x,g))"
using HVfrom_rel_closed by simp

lemma Vfrom_rel_closed:
assumes "M(A)" "M(i)" "Ord(i)"
shows "M(transrec(i, HVfrom_rel(M, A)))"
using is_HVfrom_iff HVfrom_closed HVfrom_replacement assms trepl_HVfrom relation2_HVfrom
transrec_closed[of "is_HVfrom(M,A)" i "HVfrom_rel(M,A)"]
by simp

lemma transrec_HVfrom:
assumes "M(A)"
shows "Ord(i) ⟹ M(i) ⟹ {x∈Vfrom(A,i). M(x)} = transrec(i,HVfrom_rel(M,A))"
proof (induct rule:trans_induct)
have eq:"(⋃x∈i. {x ∈ Pow(transrec(x, HVfrom_rel(M, A))) . M(x)}) =  ⋃{y . x ∈ i, y = Pow⇗M⇖(transrec(x, HVfrom_rel(M, A)))}"
if "Ord(i)" "M(i)" for i
using assms Pow_rel_char[OF Vfrom_rel_closed[OF ‹M(A)› transM[of _ i]]] Ord_in_Ord' that
by auto
case (step i)
then
have 0: "M(Pow⇗M⇖(transrec(x, HVfrom_rel(M, A))))" if "x∈i" for x
using assms that transM[of _ i] Ord_in_Ord
transrec_closed[of "is_HVfrom(M,A)" _ "HVfrom_rel(M,A)"] trepl_HVfrom relation2_HVfrom
by auto
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_rel(M, A))). M(x)})"
using transM[of _ i]
by auto
also
have " ... = transrec(i, HVfrom_rel(M, A))"
using 0 step assms transM[of _ i] eq
def_transrec[of "λy. transrec(y, HVfrom_rel(M, A))" "HVfrom_rel(M, A)" i]
unfolding Powapply_rel_def HVfrom_rel_def
by auto
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 is_HVfrom_iff
transrec_abs[of "is_HVfrom(M,A)" i "HVfrom_rel(M,A)"] trepl_HVfrom relation2_HVfrom
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 is_HVfrom_iff HVfrom_closed HVfrom_replacement
transrec_closed[of "is_HVfrom(M,A)" i "HVfrom_rel(M,A)"] trepl_HVfrom relation2_HVfrom
transrec_HVfrom
by simp

end ― ‹\<^locale>‹M_Vfrom››

subsection‹Formula synthesis›

context M_Vfrom
begin

rel_closed for "Hrank"
unfolding Hrank_rel_def
using Hrank_replacement
by simp

is_iff_rel for "Hrank"
proof -
assume "M(f)" "M(x)" "M(res)"
moreover from this
have "{a . y ∈ x, M(a) ∧ M(y) ∧ a = succ(f ` y)} = {a . y ∈ x,  a = succ(f ` y)}"
using transM[of _ x]
by auto
ultimately
show ?thesis
unfolding is_Hrank_def Hrank_rel_def
using Replace_abs transM[of _ x] Hrank_replacement
by auto
qed

lemma relation2_Hrank :
"relation2(M,is_Hrank(M),Hrank)"
unfolding  relation2_def
proof(clarify)
fix x f res
assume "M(x)" "M(f)" "M(res)"
moreover from this
have "{a . y ∈ x, M(a) ∧ M(y) ∧ a = succ(f ` y)} = {a . y ∈ x,  a = succ(f ` y)}"
using transM[of _ x]
by auto
ultimately
show "is_Hrank(M, x, f, res) ⟷ res = Hrank(x, f)"
unfolding  Hrank_def relation2_def
using is_Hrank_iff[unfolded Hrank_rel_def]
by auto
qed

lemma Hrank_closed :
"∀x[M]. ∀g[M]. function(g) ⟶ M(Hrank(x,g))"
proof(clarify)
fix x g
assume "M(x)" "M(g)"
then
show "M(Hrank(x,g))"
using RepFun_closed[OF Hrank_replacement] transM[of _ x]
unfolding Hrank_def
by auto
qed

end ―‹\<^locale>‹M_basic››

context M_eclose
begin

lemma wf_rrank : "M(x) ⟹ wf(rrank(x))"
unfolding rrank_def using wf_trancl[OF wf_Memrel] .

lemma trans_rrank : "M(x) ⟹ trans(rrank(x))"
unfolding rrank_def using trans_trancl .

lemma relation_rrank : "M(x) ⟹ relation(rrank(x))"
unfolding rrank_def using relation_trancl .

lemma rrank_in_M : "M(x) ⟹ M(rrank(x))"
unfolding rrank_def by simp

end ― ‹\<^locale>‹M_eclose››

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

definition
Vset' :: "[i] ⇒ i" where
"Vset'(A) ≡ Vfrom(0,A)"

relativize functional "Vset'" "Vset_rel"
relationalize "Vset_rel" "is_Vset"
reldb_rem relational "Vset"
reldb_rem functional "Vset_rel"

schematic_goal sats_is_Vset_fm_auto:
assumes
"i∈nat" "v∈nat" "env∈list(A)" "0∈A"
"i < length(env)" "v < length(env)"
shows
"is_Vset(##A,nth(i, env),nth(v, env)) ⟷ sats(A,?ivs_fm(i,v),env)"
unfolding is_Vset_def is_Vfrom_def
by (insert assms; (rule sep_rules is_HVfrom_iff_sats is_transrec_iff_sats | simp)+)

synthesize "is_Vset" from_schematic "sats_is_Vset_fm_auto"
arity_theorem for "is_Vset_fm"
context M_Vfrom
begin

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 rank_closed: "M(a) ⟹ M(rank(a))"
unfolding rank_trancl
using Hrank_closed is_Hrank_replacement relation2_Hrank
wf_rrank relation_rrank trans_rrank rrank_in_M
trans_wfrec_closed[of "rrank(a)" a "is_Hrank(M)"]
transM[of _ a]
by auto

lemma M_into_Vset:
assumes "M(a)"
shows "∃i[M]. ∃V[M]. ordinal(M,i) ∧ is_Vset(M,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
using nonempty empty_abs
unfolding is_Vset_def
by blast
qed

end ― ‹\<^locale>‹M_HVfrom››

end```