Theory Relative_Univ

section‹Relativization of the cumulative hierarchy›
theory Relative_Univ
  imports
    "ZF-Constructible.Rank"
    Internalizations
    Recursion_Thms

begin

lemma (in M_trivial) powerset_abs' [simp]: 
  assumes
    "M(x)" "M(y)"
  shows
    "powerset(M,x,y) ⟷ y = {a∈Pow(x) . M(a)}"
  using powerset_abs assms by 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 ..

(* "Vfrom(A,i) ≡ transrec(i, %x f. A ∪ (⋃y∈x. Pow(f`y)))" *)
(* HVfrom is *not* the recursive step for Vfrom. It is the
   relativized version *)
definition
  HVfrom :: "[i⇒o,i,i,i] ⇒ i" where
  "HVfrom(M,A,x,f) ≡ A ∪ (⋃y∈x. {a∈Pow(f`y). M(a)})"

(* z = Pow(f`y) *)
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))"

(* Trivial lemma *)
lemma is_powapply_closed: "is_powapply(M,f,y,z) ⟹ M(z)"
  unfolding is_powapply_def by simp

(* is_Replace(M,A,P,z) ≡ ∀u[M]. u ∈ z ⟷ (∃x[M]. x∈A & P(x,u)) *)
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 is_Collect_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)

(* rank *)
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