Theory Names

section‹Names and generic extensions›

theory Names
  imports
    Forcing_Data
    FrecR_Arities
    ZF_Trans_Interpretations
begin

definition
  Hv :: "[i,i,i]i" where
  "Hv(G,x,f)  { z . y domain(x), (pG. y,p  x)  z=f`y}"

text‹The funcion termval interprets a name in termM
according to a (generic) filter termG. Note the definition
in terms of the well-founded recursor.›

definition
  val :: "[i,i]i" where
  "val(G,τ)  wfrec(edrel(eclose({τ})), τ ,Hv(G))"

definition
  GenExt :: "[i,i]i"     ("_[_]" [71,1])
  where "M[G]  {val(G,τ). τ  M}"

lemma map_val_in_MG:
  assumes
    "envlist(M)"
  shows
    "map(val(G),env)list(M[G])"
  unfolding GenExt_def using assms map_type2 by simp

subsection‹Values and check-names›
context forcing_data1
begin

lemma name_components_in_M:
  assumes "σ,pθ" "θ  M"
  shows   "σM" "pM"
  using assms transitivity pair_in_M_iff
  by auto

definition
  Hcheck :: "[i,i]  i" where
  "Hcheck(z,f)   { f`y,𝟭 . y  z}"

definition
  check :: "i  i" where
  "check(x)  transrec(x , Hcheck)"

lemma checkD:
  "check(x) =  wfrec(Memrel(eclose({x})), x, Hcheck)"
  unfolding check_def transrec_def ..

lemma Hcheck_trancl:"Hcheck(y, restrict(f,Memrel(eclose({x}))-``{y}))
                   = Hcheck(y, restrict(f,(Memrel(eclose({x}))^+)-``{y}))"
  unfolding Hcheck_def
  using restrict_trans_eq by simp

lemma check_trancl: "check(x) = wfrec(rcheck(x), x, Hcheck)"
  using checkD wf_eq_trancl Hcheck_trancl unfolding rcheck_def by simp

lemma rcheck_in_M : "x  M  rcheck(x)  M"
  unfolding rcheck_def by (simp flip: setclass_iff)

lemma rcheck_subset_M : "x  M  field(rcheck(x))  eclose({x})"
  unfolding rcheck_def using field_Memrel field_trancl by auto

lemma  aux_def_check: "x  y 
  wfrec(Memrel(eclose({y})), x, Hcheck) =
  wfrec(Memrel(eclose({x})), x, Hcheck)"
  by (rule wfrec_eclose_eq,auto simp add: arg_into_eclose eclose_sing)

lemma def_check : "check(y) = { check(w),𝟭 . w  y}"
proof -
  let
    ?r="λy. Memrel(eclose({y}))"
  have wfr:   "w . wf(?r(w))"
    using wf_Memrel ..
  then
  have "check(y)= Hcheck( y, λx?r(y) -`` {y}. wfrec(?r(y), x, Hcheck))"
    using wfrec[of "?r(y)" y "Hcheck"] checkD by simp
  also
  have " ... = Hcheck( y, λxy. wfrec(?r(y), x, Hcheck))"
    using under_Memrel_eclose arg_into_eclose by simp
  also
  have " ... = Hcheck( y, λxy. check(x))"
    using aux_def_check checkD by simp
  finally
  show ?thesis
    using Hcheck_def by simp
qed

lemma def_checkS :
  fixes n
  assumes "n  nat"
  shows "check(succ(n)) = check(n)  {check(n),𝟭}"
proof -
  have "check(succ(n)) = {check(i),𝟭 . i  succ(n)} "
    using def_check by blast
  also
  have "... = {check(i),𝟭 . i  n}  {check(n),𝟭}"
    by blast
  also
  have "... = check(n)  {check(n),𝟭}"
    using def_check[of n,symmetric] by simp
  finally
  show ?thesis .
qed

lemma field_Memrel2 :
  assumes "x  M"
  shows "field(Memrel(eclose({x})))  M"
proof -
  have "field(Memrel(eclose({x})))  eclose({x})" "eclose({x})  M"
    using Ordinal.Memrel_type field_rel_subset assms eclose_least[OF trans_M] by auto
  then
  show ?thesis
    using subset_trans by simp
qed

lemma aux_def_val:
  assumes "z  domain(x)"
  shows "wfrec(edrel(eclose({x})),z,Hv(G)) = wfrec(edrel(eclose({z})),z,Hv(G))"
proof -
  let ?r="λx . edrel(eclose({x}))"
  have "zeclose({z})"
    using arg_in_eclose_sing .
  moreover
  have "relation(?r(x))"
    using relation_edrel .
  moreover
  have "wf(?r(x))"
    using wf_edrel .
  moreover from assms
  have "tr_down(?r(x),z)  eclose({z})"
    using tr_edrel_subset by simp
  ultimately
  have "wfrec(?r(x),z,Hv(G)) = wfrec[eclose({z})](?r(x),z,Hv(G))"
    using wfrec_restr by simp
  also from zdomain(x)
  have "... = wfrec(?r(z),z,Hv(G))"
    using restrict_edrel_eq wfrec_restr_eq by simp
  finally
  show ?thesis .
qed

text‹The next lemma provides the usual recursive expresion for the definition of termval.›

lemma def_val:  "val(G,x) = {z . tdomain(x) , (pG .  t,px)  z=val(G,t)}"
proof -
  let
    ?r="λτ . edrel(eclose({τ}))"
  let
    ?f="λz?r(x)-``{x}. wfrec(?r(x),z,Hv(G))"
  have "τ. wf(?r(τ))"
    using wf_edrel by simp
  with wfrec [of _ x]
  have "val(G,x) = Hv(G,x,?f)"
    using val_def by simp
  also
  have " ... = Hv(G,x,λzdomain(x). wfrec(?r(x),z,Hv(G)))"
    using dom_under_edrel_eclose by simp
  also
  have " ... = Hv(G,x,λzdomain(x). val(G,z))"
    using aux_def_val val_def by simp
  finally
  show ?thesis
    using Hv_def by simp
qed

lemma val_mono : "xy  val(G,x)  val(G,y)"
  by (subst (1 2) def_val, force)

text‹Check-names are the canonical names for elements of the
ground model. Here we show that this is the case.›

lemma val_check : "𝟭  G   𝟭    val(G,check(y))  = y"
proof (induct rule:eps_induct)
  case (1 y)
  then show ?case
  proof -
    have "check(y) = { check(w), 𝟭 . w  y}"  (is "_ = ?C")
      using def_check .
    then
    have "val(G,check(y)) = val(G, {check(w), 𝟭 . w  y})"
      by simp
    also
    have " ...  = {z . tdomain(?C) , (pG .  t, p?C )  z=val(G,t) }"
      using def_val by blast
    also
    have " ... =  {z . tdomain(?C) , (wy. t=check(w))  z=val(G,t) }"
      using 1 by simp
    also
    have " ... = {val(G,check(w)) . wy }"
      by force
    finally
    show "val(G,check(y)) = y"
      using 1 by simp
  qed
qed

lemma val_of_name :
  "val(G,{xA×. Q(x)}) = {z . tA , (p .  Q(t,p)  p  G)  z=val(G,t)}"
proof -
  let
    ?n="{xA×. Q(x)}" and
    ?r="λτ . edrel(eclose({τ}))"
  let
    ?f="λz?r(?n)-``{?n}. val(G,z)"
  have
    wfR : "wf(?r(τ))" for τ
    by (simp add: wf_edrel)
  have "domain(?n)  A" by auto
  { fix t
    assume H:"t  domain({x  A ×  . Q(x)})"
    then have "?f ` t = (if t  ?r(?n)-``{?n} then val(G,t) else 0)"
      by simp
    moreover have "... = val(G,t)"
      using dom_under_edrel_eclose H if_P by auto
  }
  then
  have Eq1: "t  domain({x  A ×  . Q(x)})  val(G,t) = ?f` t"  for t
    by simp
  have "val(G,?n) = {z . tdomain(?n), (p  G . t,p  ?n)  z=val(G,t)}"
    by (subst def_val,simp)
  also
  have "... = {z . tdomain(?n), (p . t,p?n  pG)  z=?f`t}"
    unfolding Hv_def
    by (auto simp add:Eq1)
  also
  have "... = {z . tdomain(?n), (p . t,p?n  pG)  z=(if t?r(?n)-``{?n} then val(G,t) else 0)}"
    by (simp)
  also
  have "... = { z . tdomain(?n), (p . t,p?n  pG)  z=val(G,t)}"
  proof -
    have "domain(?n)  ?r(?n)-``{?n}"
      using dom_under_edrel_eclose by simp
    then
    have "tdomain(?n). (if t?r(?n)-``{?n} then val(G,t) else 0) = val(G,t)"
      by auto
    then
    show "{ z . tdomain(?n), (p . t,p?n  pG)  z=(if t?r(?n)-``{?n} then val(G,t) else 0)} =
          { z . tdomain(?n), (p . t,p?n  pG)  z=val(G,t)}"
      by auto
  qed
  also
  have " ... = { z . tA, (p . t,p?n  pG)  z=val(G,t)}"
    by force
  finally
  show " val(G,?n)  = { z . tA, (p . Q(t,p)  pG)  z=val(G,t)}"
    by auto
qed

lemma val_of_name_alt :
  "val(G,{xA×. Q(x)}) = {z . tA , (pG .  Q(t,p))  z=val(G,t) }"
  using val_of_name by force

lemma val_only_names: "val(F,τ) = val(F,{xτ. tdomain(τ). pF. x=t,p})"
  (is "_ = val(F,?name)")
proof -
  have "val(F,?name) = {z . tdomain(?name), (pF. t, p  ?name)  z=val(F, t)}"
    using def_val by blast
  also
  have " ... = {val(F, t). t{ydomain(τ). pF. y, p  τ }}"
    by blast
  also
  have " ... = {z . tdomain(τ), (pF. t, p  τ)  z=val(F, t)}"
    by blast
  also
  have " ... = val(F, τ)"
    using def_val[symmetric] by blast
  finally
  show ?thesis ..
qed

lemma val_only_pairs: "val(F,τ) = val(F,{xτ. t p. x=t,p})"
proof
  have "val(F,τ) = val(F,{xτ. tdomain(τ). pF. x=t,p})" (is "_ = val(F,?name)")
    using val_only_names .
  also
  have "...  val(F,{xτ. t p. x=t,p})"
    using val_mono[of ?name "{xτ. t p. x=t,p}"] by auto
  finally
  show "val(F,τ)  val(F,{xτ. t p. x=t,p})" by simp
next
  show "val(F,{xτ. t p. x=t,p})  val(F,τ)"
    using val_mono[of "{xτ. t p. x=t,p}"] by auto
qed

lemma val_subset_domain_times_range: "val(F,τ)  val(F,domain(τ)×range(τ))"
  using val_only_pairs[THEN equalityD1]
    val_mono[of "{x  τ . t p. x = t, p}" "domain(τ)×range(τ)"] by blast

lemma val_of_elem: "θ,p  π  pG  val(G,θ)  val(G,π)"
proof -
  assume "θ,p  π"
  then
  have "θdomain(π)"
    by auto
  assume "pG"
  with θdomain(π) θ,p  π
  have "val(G,θ)  {z . tdomain(π) , (pG .  t, pπ)  z=val(G,t) }"
    by auto
  then
  show ?thesis
    by (subst def_val)
qed

lemma elem_of_val: "xval(G,π)  θdomain(π). val(G,θ) = x"
  by (subst (asm) def_val,auto)

lemma elem_of_val_pair: "xval(G,π)  θ. pG.  θ,pπ  val(G,θ) = x"
  by (subst (asm) def_val,auto)

lemma elem_of_val_pair':
  assumes "πM" "xval(G,π)"
  shows "θM. pG.  θ,pπ  val(G,θ) = x"
proof -
  from assms
  obtain θ p where "pG" "θ,pπ" "val(G,θ) = x"
    using elem_of_val_pair by blast
  moreover from this πM
  have "θM"
    using pair_in_M_iff[THEN iffD1, THEN conjunct1, simplified]
      transitivity by blast
  ultimately
  show ?thesis
    by blast
qed

lemma GenExtD: "x  M[G]  τM. x = val(G,τ)"
  by (simp add:GenExt_def)

lemma GenExtI: "x  M  val(G,x)  M[G]"
  by (auto simp add: GenExt_def)

lemma Transset_MG : "Transset(M[G])"
proof -
  { fix vc y
    assume "vc  M[G]" and "y  vc"
    then
    obtain c where "cM" "val(G,c)M[G]" "y  val(G,c)"
      using GenExtD by auto
    from y  val(G,c)
    obtain θ where "θdomain(c)" "val(G,θ) = y"
      using elem_of_val by blast
    with trans_M cM
    have "y  M[G]"
      using domain_trans GenExtI by blast
  }
  then
  show ?thesis
    using Transset_def by auto
qed

lemmas transitivity_MG = Transset_intf[OF Transset_MG]

text‹This lemma can be proved before having termcheck_in_M. At some point Miguel naïvely
thought that the termcheck_in_M could be proved using this argument.›
lemma check_nat_M :
  assumes "n  nat"
  shows "check(n)  M"
  using assms
proof (induct n)
  case 0
  then
  show ?case
    using zero_in_M by (subst def_check,simp)
next
  case (succ x)
  have "𝟭  M"
    using one_in_P P_sub_M subsetD by simp
  with check(x)M
  have "check(x),𝟭  M"
    using pair_in_M_iff by simp
  then
  have "{check(x),𝟭}  M"
    using singleton_closed by simp
  with check(x)M
  have "check(x)  {check(x),𝟭}  M"
    using Un_closed by simp
  then
  show ?case
    using xnat def_checkS by simp
qed

lemma def_PHcheck:
  assumes
    "zM" "fM"
  shows
    "Hcheck(z,f) = Replace(z,PHcheck(##M,𝟭,f))"
proof -
  from assms
  have "f`x,𝟭  M" "f`xM" if "xz" for x
    using pair_in_M_iff transitivity that apply_closed by simp_all
  then
  have "{y . x  z, y = f ` x, 𝟭} =  {y . x  z, y = f ` x, 𝟭  yM  f`xM}"
    by simp
  then
  show ?thesis
    using zM fM transitivity
    unfolding Hcheck_def PHcheck_def RepFun_def
    by auto
qed

(* instance of replacement for hcheck *)
lemma wfrec_Hcheck :
  assumes "XM"
  shows "wfrec_replacement(##M,is_Hcheck(##M,𝟭),rcheck(X))"
proof -
  let ?f="Exists(And(pair_fm(1,0,2),
               is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0)))"
  have "is_Hcheck(##M,𝟭,a,b,c) 
        sats(M,is_Hcheck_fm(8,2,1,0),[c,b,a,d,e,y,x,z,𝟭,rcheck(x)])"
    if "aM" "bM" "cM" "dM" "eM" "yM" "xM" "zM"
    for a b c d e y x z
    using that XM rcheck_in_M is_Hcheck_iff_sats zero_in_M
    by simp
  then
  have "sats(M,is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0), [y,x,z,𝟭,rcheck(X)])
         is_wfrec(##M, is_Hcheck(##M,𝟭),rcheck(X), x, y)"
    if "xM" "yM" "zM" for x y z
    using that sats_is_wfrec_fm XM rcheck_in_M zero_in_M
    by simp
  moreover from this
  have satsf:"sats(M, ?f, [x,z,𝟭,rcheck(X)]) 
              (yM. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(##M,𝟭),rcheck(X), x, y))"
    if "xM" "zM" for x z
    using that XM rcheck_in_M
    by (simp del:pair_abs)
  moreover
  have artyf:"arity(?f) = 4"
    using arity_wfrec_replacement_fm[where p="is_Hcheck_fm(8, 2, 1, 0)" and i=9]
      arity_is_Hcheck_fm ord_simp_union
    by simp
  ultimately
  have "strong_replacement(##M,λx z. sats(M,?f,[x,z,𝟭,rcheck(X)]))"
    using ZF_ground_replacements(2) artyf XM rcheck_in_M
    unfolding replacement_assm_def wfrec_Hcheck_fm_def by simp
  then
  have "strong_replacement(##M,λx z.
          yM. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(##M,𝟭),rcheck(X), x, y))"
    using repl_sats[of M ?f "[𝟭,rcheck(X)]"] satsf by (simp del:pair_abs)
  then
  show ?thesis
    unfolding wfrec_replacement_def by simp
qed

lemma Hcheck_closed' : "fM  zM  {f ` x . x  z}  M"
  using RepFun_closed[OF lam_replacement_imp_strong_replacement]
          lam_replacement_apply apply_closed transM[of _ z]
  by simp

lemma repl_PHcheck :
  assumes "fM"
  shows "lam_replacement(##M,λx. Hcheck(x,f))"
proof -
  have "Hcheck(x,f) = {f`y . yx}×{𝟭}" for x
    unfolding Hcheck_def by auto
  moreover
  note assms
  moreover from this
  have 1:"lam_replacement(##M, λx . {f`y . yx}×{𝟭})"
    using lam_replacement_RepFun_apply
      lam_replacement_constant lam_replacement_fst lam_replacement_snd
      singleton_closed cartprod_closed fst_snd_closed Hcheck_closed'
    by (rule_tac lam_replacement_CartProd[THEN [5] lam_replacement_hcomp2],simp_all)
  ultimately
  show ?thesis
    using singleton_closed cartprod_closed Hcheck_closed'
    by(rule_tac lam_replacement_cong[OF 1],auto)
qed

lemma univ_PHcheck : " zM ; fM   univalent(##M,z,PHcheck(##M,𝟭,f))"
  unfolding univalent_def PHcheck_def
  by simp

lemma PHcheck_closed : "zM ; fM ; xz; PHcheck(##M,𝟭,f,x,y)   (##M)(y)"
  unfolding PHcheck_def by simp

lemma relation2_Hcheck : "relation2(##M,is_Hcheck(##M,𝟭),Hcheck)"
proof -
  have "is_Replace(##M,z,PHcheck(##M,𝟭,f),hc)  hc = Replace(z,PHcheck(##M,𝟭,f))"
    if "zM" "fM" "hcM" for z f hc
    using that Replace_abs[OF _ _ univ_PHcheck] PHcheck_closed[of z f]
    by simp
  with def_PHcheck
  show ?thesis
    unfolding relation2_def is_Hcheck_def Hcheck_def
    by simp
qed

lemma Hcheck_closed : "yM. gM.  Hcheck(y,g)M"
proof -
  have eq:"Hcheck(x,f) = {f`y . yx}×{𝟭}" for f x
    unfolding Hcheck_def by auto
  then
  have "Hcheck(y,g)M" if "yM" "gM" for y g
    using eq that Hcheck_closed' cartprod_closed singleton_closed
    by simp
  then
  show ?thesis
    by auto
qed

lemma wf_rcheck : "xM  wf(rcheck(x))"
  unfolding rcheck_def using wf_trancl[OF wf_Memrel] .

lemma trans_rcheck : "xM  trans(rcheck(x))"
  unfolding rcheck_def using trans_trancl .

lemma relation_rcheck : "xM  relation(rcheck(x))"
  unfolding rcheck_def using relation_trancl .

lemma check_in_M : "xM  check(x)  M"
  using wfrec_Hcheck[of x] check_trancl wf_rcheck trans_rcheck relation_rcheck rcheck_in_M
    Hcheck_closed relation2_Hcheck trans_wfrec_closed[of "rcheck(x)"]
  by simp

(* Internalization and absoluteness of rcheck› *)
lemma rcheck_abs[Rel] : " xM ; rM   is_rcheck(##M,x,r)  r = rcheck(x)"
  unfolding rcheck_def is_rcheck_def
  using singleton_closed trancl_closed Memrel_closed eclose_closed zero_in_M
  by simp

lemma check_abs[Rel] :
  assumes "xM" "zM"
  shows "is_check(##M,𝟭,x,z)  z = check(x)"
proof -
  have "is_check(##M,𝟭,x,z)  is_wfrec(##M,is_Hcheck(##M,𝟭),rcheck(x),x,z)"
    unfolding is_check_def
    using assms rcheck_abs rcheck_in_M zero_in_M
    unfolding check_trancl is_check_def
    by simp
  then
  show ?thesis
    unfolding check_trancl
    using assms wfrec_Hcheck[of x] wf_rcheck trans_rcheck relation_rcheck rcheck_in_M
      Hcheck_closed relation2_Hcheck trans_wfrec_abs[of "rcheck(x)" x z "is_Hcheck(##M,𝟭)" Hcheck]
    by (simp flip: setclass_iff)
qed

lemma check_lam_replacement: "lam_replacement(##M,check)"
proof -
  have "arity(check_fm(2,0,1)) = 3"
    by (simp add:ord_simp_union arity)
  then
  have "Lambda(A, check)  M" if "AM" for A
    using that check_in_M transitivity[of _ A]
      sats_check_fm check_abs zero_in_M
      check_fm_type ZF_ground_replacements(3)
    by(rule_tac Lambda_in_M [of "check_fm(2,0,1)" "[𝟭]"],simp_all)
  then
  show ?thesis
    using check_in_M lam_replacement_iff_lam_closed[THEN iffD2]
    by simp
qed

lemma check_replacement: "{check(x). x}  M"
  using lam_replacement_imp_strong_replacement_aux[OF check_lam_replacement]
    transitivity check_in_M RepFun_closed
    by simp_all

lemma M_subset_MG : "𝟭  G  M  M[G]"
  using check_in_M GenExtI
  by (intro subsetI, subst val_check [of G,symmetric], auto)

text‹The name for the generic filter›
definition
  G_dot :: "i" where
  "G_dot  {check(p),p . p}"

lemma G_dot_in_M : "G_dot  M"
  using lam_replacement_Pair[THEN [5] lam_replacement_hcomp2,OF
    check_lam_replacement lam_replacement_identity]
    check_in_M lam_replacement_imp_strong_replacement_aux
    transitivity check_in_M RepFun_closed pair_in_M_iff
  unfolding G_dot_def
  by simp

lemma zero_in_MG : "0  M[G]"
proof -
  have "0 = val(G,0)"
    using zero_in_M elem_of_val by auto
  also
  have "...  M[G]"
    using GenExtI zero_in_M by simp
  finally
  show ?thesis .
qed

declare check_in_M [simp,intro]

end ― ‹localeforcing_data1

context G_generic1
begin

lemma val_G_dot : "val(G,G_dot) = G"
proof (intro equalityI subsetI)
  fix x
  assume "xval(G,G_dot)"
  then obtain θ p where "pG" "θ,p  G_dot" "val(G,θ) = x" "θ = check(p)"
    unfolding G_dot_def using elem_of_val_pair G_dot_in_M
    by force
  then
  show "x  G"
    using G_subset_P one_in_G val_check P_sub_M by auto
next
  fix p
  assume "pG"
  have "check(q),q  G_dot" if "q" for q
    unfolding G_dot_def using that by simp
  with pG
  have "val(G,check(p))  val(G,G_dot)"
    using val_of_elem G_dot_in_M by blast
  with pG
  show "p  val(G,G_dot)"
    using one_in_G G_subset_P P_sub_M val_check by auto
qed

lemma G_in_Gen_Ext : "G  M[G]"
  using G_subset_P one_in_G val_G_dot GenExtI[of _ G] G_dot_in_M
  by force

lemmas generic_simps = val_check[OF one_in_G one_in_P]
  M_subset_MG[OF one_in_G, THEN subsetD]
  GenExtI P_in_M

lemmas generic_dests = M_genericD M_generic_compatD

bundle G_generic1_lemmas = generic_simps[simp] generic_dests[dest]

end  ― ‹localeG_generic1

sublocale G_generic1  ext: M_trans "##M[G]"
  using generic transitivity_MG zero_in_MG
  by unfold_locales force+

end