Theory Forces_Definition

sectionThe definition of termforces

theory Forces_Definition
  imports
    Forcing_Data
begin

textThis is the core of our development.

subsectionThe relation termfrecrel

lemma names_belowsD:
  assumes "x  names_below(P,z)"
  obtains f n1 n2 p where
    "x = f,n1,n2,p" "f2" "n1ecloseN(z)" "n2ecloseN(z)" "pP"
  using assms unfolding names_below_def by auto

context forcing_data1
begin

(* Absoluteness of components *)
lemma ftype_abs:
  "xM; yM   is_ftype(##M,x,y)  y = ftype(x)"
  unfolding ftype_def is_ftype_def by (simp add:absolut)

lemma name1_abs:
  "xM; yM   is_name1(##M,x,y)  y = name1(x)"
  unfolding name1_def is_name1_def
  by (rule is_hcomp_abs[OF fst_abs],simp_all add: fst_snd_closed[simplified] absolut)

lemma snd_snd_abs:
  "xM; yM   is_snd_snd(##M,x,y)  y = snd(snd(x))"
  unfolding is_snd_snd_def
  by (rule is_hcomp_abs[OF snd_abs],
      simp_all add: conjunct2[OF fst_snd_closed,simplified] absolut)

lemma name2_abs:
  "xM; yM   is_name2(##M,x,y)  y = name2(x)"
  unfolding name2_def is_name2_def
  by (rule is_hcomp_abs[OF fst_abs snd_snd_abs],simp_all add:absolut conjunct2[OF fst_snd_closed,simplified])

lemma cond_of_abs:
  "xM; yM   is_cond_of(##M,x,y)  y = cond_of(x)"
  unfolding cond_of_def is_cond_of_def
  by (rule is_hcomp_abs[OF snd_abs snd_snd_abs];simp_all add:fst_snd_closed[simplified])

lemma tuple_abs:
  "zM;t1M;t2M;pM;tM 
   is_tuple(##M,z,t1,t2,p,t)  t = z,t1,t2,p"
  unfolding is_tuple_def using pair_in_M_iff by simp

lemmas components_abs = ftype_abs name1_abs name2_abs cond_of_abs
  tuple_abs

lemma comp_in_M:
  "p  q  pM"
  "p  q  qM"
  using transitivity[of _ leq] pair_in_M_iff by auto

(* Absoluteness of Hfrc *)

lemma eq_case_abs [simp]:
  assumes "t1M" "t2M" "pM" "fM"
  shows "is_eq_case(##M,t1,t2,p,,leq,f)  eq_case(t1,t2,p,,leq,f)"
proof -
  have "q  p  qM" for q
    using comp_in_M by simp
  moreover
  have "s,yt  sdomain(t)" if "tM" for s y t
    using that unfolding domain_def by auto
  ultimately
  have
    "(sM. s  domain(t1)  s  domain(t2)  (qM. q  q  p 
                              (f ` 1, s, t1, q =1  f ` 1, s, t2, q=1))) 
    (s. s  domain(t1)  s  domain(t2)  (q. q  q  p 
                                  (f ` 1, s, t1, q =1  f ` 1, s, t2, q=1)))"
    using assms domain_trans[OF trans_M,of t1] domain_trans[OF trans_M,of t2]
    by auto
  then
  show ?thesis
    unfolding eq_case_def is_eq_case_def
    using assms pair_in_M_iff nat_into_M domain_closed apply_closed zero_in_M Un_closed
    by (simp add:components_abs)
qed

lemma mem_case_abs [simp]:
  assumes "t1M" "t2M" "pM" "fM"
  shows "is_mem_case(##M,t1,t2,p,,leq,f)  mem_case(t1,t2,p,,leq,f)"
proof
  {
    fix v
    assume "v" "v  p" "is_mem_case(##M,t1,t2,p,,leq,f)"
    moreover
    from this
    have "vM" "v,p  M" "(##M)(v)"
      using transitivity[OF _ P_in_M,of v] transitivity[OF _ leq_in_M]
      by simp_all
    moreover
    from calculation assms
    obtain q r s where
      "r    q    q, v  M  s, r  M  q, r  M  0  M 
       0, t1, s, q  M  q  v  s, r  t2  q  r  f ` 0, t1, s, q = 1"
      unfolding is_mem_case_def by (auto simp add:components_abs)
    then
    have "q s r. r    q    q  v  s, r  t2  q  r  f ` 0, t1, s, q = 1"
      by auto
  }
  then
  show "mem_case(t1, t2, p, , leq, f)" if "is_mem_case(##M, t1, t2, p, , leq, f)"
    unfolding mem_case_def using that assms by auto
next
  { fix v
    assume "v  M" "v  " "v, p  M" "v  p" "mem_case(t1, t2, p, , leq, f)"
    moreover
    from this
    obtain q s r where "r    q    q  v  s, r  t2  q  r  f ` 0, t1, s, q = 1"
      unfolding mem_case_def by auto
    moreover
    from this t2M
    have "rM" "qM" "sM" "r    q    q  v  s, r  t2  q  r  f ` 0, t1, s, q = 1"
      using transitivity domainI[of s r] domain_closed
      by auto
    moreover
    note t1M
    ultimately
    have "qM . sM. rM.
         r    q    q, v  M  s, r  M  q, r  M  0  M 
         0, t1, s, q  M  q  v  s, r  t2  q  r  f ` 0, t1, s, q = 1"
      using pair_in_M_iff zero_in_M by auto
  }
  then
  show "is_mem_case(##M, t1, t2, p, , leq, f)" if "mem_case(t1, t2, p, , leq, f)"
    unfolding is_mem_case_def
    using assms that zero_in_M pair_in_M_iff apply_closed nat_into_M
    by (auto simp add:components_abs)
qed

lemma Hfrc_abs:
  "fnncM; fM 
   is_Hfrc(##M,,leq,fnnc,f)  Hfrc(,leq,fnnc,f)"
  unfolding is_Hfrc_def Hfrc_def using pair_in_M_iff zero_in_M
  by (auto simp add:components_abs)

lemma Hfrc_at_abs:
  "fnncM; fM ; zM 
   is_Hfrc_at(##M,,leq,fnnc,f,z)   z = bool_of_o(Hfrc(,leq,fnnc,f)) "
  unfolding is_Hfrc_at_def using Hfrc_abs
  by auto

lemma components_closed :
  "xM  (##M)(ftype(x))"
  "xM  (##M)(name1(x))"
  "xM  (##M)(name2(x))"
  "xM  (##M)(cond_of(x))"
  unfolding ftype_def name1_def name2_def cond_of_def using fst_snd_closed by simp_all

lemma ecloseN_closed:
  "(##M)(A)  (##M)(ecloseN(A))"
  "(##M)(A)  (##M)(eclose_n(name1,A))"
  "(##M)(A)  (##M)(eclose_n(name2,A))"
  unfolding ecloseN_def eclose_n_def
  using components_closed eclose_closed singleton_closed Un_closed by auto

lemma eclose_n_abs :
  assumes "xM" "ecM"
  shows "is_eclose_n(##M,is_name1,ec,x)  ec = eclose_n(name1,x)"
    "is_eclose_n(##M,is_name2,ec,x)  ec = eclose_n(name2,x)"
  unfolding is_eclose_n_def eclose_n_def
  using assms name1_abs name2_abs eclose_abs singleton_closed components_closed
  by auto


lemma ecloseN_abs :
  "xM;ecM  is_ecloseN(##M,x,ec)  ec = ecloseN(x)"
  unfolding is_ecloseN_def ecloseN_def
  using eclose_n_abs Un_closed union_abs ecloseN_closed
  by auto

lemma frecR_abs :
  "xM  yM  frecR(x,y)  is_frecR(##M,x,y)"
  unfolding frecR_def is_frecR_def
  using zero_in_M domain_closed Un_closed components_closed nat_into_M
  by (auto simp add: components_abs)

lemma frecrelP_abs :
  "zM  frecrelP(##M,z)  (x y. z = x,y  frecR(x,y))"
  using pair_in_M_iff frecR_abs unfolding frecrelP_def by auto

lemma frecrel_abs:
  assumes "AM" "rM"
  shows "is_frecrel(##M,A,r)   r = frecrel(A)"
proof -
  from AM
  have "zM" if "zA×A" for z
    using cartprod_closed transitivity that by simp
  then
  have "Collect(A×A,frecrelP(##M)) = Collect(A×A,λz. (x y. z = x,y  frecR(x,y)))"
    using Collect_cong[of "A×A" "A×A" "frecrelP(##M)"] assms frecrelP_abs by simp
  with assms
  show ?thesis
    unfolding is_frecrel_def def_frecrel using cartprod_closed
    by simp
qed

lemma frecrel_closed:
  assumes "xM"
  shows "frecrel(x)M"
proof -
  have "Collect(x×x,λz. (x y. z = x,y  frecR(x,y)))M"
    using Collect_in_M[of "frecrelP_fm(0)" "[]"] arity_frecrelP_fm sats_frecrelP_fm
      frecrelP_abs xM cartprod_closed
    by simp
  then
  show ?thesis
    unfolding frecrel_def Rrel_def frecrelP_def by simp
qed

lemma field_frecrel : "field(frecrel(names_below(,x)))  names_below(,x)"
  unfolding frecrel_def
  using field_Rrel by simp

lemma forcerelD : "uv  forcerel(,x)  uv names_below(,x) × names_below(,x)"
  unfolding forcerel_def
  using trancl_type field_frecrel by blast

lemma wf_forcerel :
  "wf(forcerel(,x))"
  unfolding forcerel_def using wf_trancl wf_frecrel .

lemma restrict_trancl_forcerel:
  assumes "frecR(w,y)"
  shows "restrict(f,frecrel(names_below(,x))-``{y})`w
       = restrict(f,forcerel(,x)-``{y})`w"
  unfolding forcerel_def frecrel_def using assms restrict_trancl_Rrel[of frecR]
  by simp

lemma names_belowI :
  assumes "frecR(ft,n1,n2,p,a,b,c,d)" "p"
  shows "ft,n1,n2,p  names_below(,a,b,c,d)" (is "?x  names_below(_,?y)")
proof -
  from assms
  have "ft  2" "a  2"
    unfolding frecR_def by (auto simp add:components_simp)
  from assms
  consider (eq) "n1  domain(b)  domain(c)  (n2 = b  n2 =c)"
    | (mem) "n1 = b  n2  domain(c)"
    unfolding frecR_def by (auto simp add:components_simp)
  then show ?thesis
  proof cases
    case eq
    then
    have "n1  eclose(b)  n1  eclose(c)"
      using Un_iff in_dom_in_eclose by auto
    with eq
    have "n1  ecloseN(?y)" "n2  ecloseN(?y)"
      using ecloseNI components_in_eclose by auto
    with ft2 p
    show ?thesis
      unfolding names_below_def by  auto
  next
    case mem
    then
    have "n1  ecloseN(?y)" "n2  ecloseN(?y)"
      using mem_eclose_trans ecloseNI in_dom_in_eclose components_in_eclose
      by auto
    with ft2 p
    show ?thesis
      unfolding names_below_def
      by auto
  qed
qed

lemma names_below_tr :
  assumes "x names_below(,y)" "y names_below(,z)"
  shows "x names_below(,z)"
proof -
  let ?A="λy . names_below(,y)"
  note assms
  moreover from this
  obtain fx x1 x2 px where "x = fx,x1,x2,px" "fx2" "x1ecloseN(y)" "x2ecloseN(y)" "px"
    unfolding names_below_def by auto
  moreover from calculation
  obtain fy y1 y2 py where "y = fy,y1,y2,py" "fy2" "y1ecloseN(z)" "y2ecloseN(z)" "py"
    unfolding names_below_def by auto
  moreover from calculation
  have "x1ecloseN(z)" "x2ecloseN(z)"
    using ecloseN_mono names_simp by auto
  ultimately
  have "x?A(z)"
    unfolding names_below_def by simp
  then
  show ?thesis using subsetI by simp
qed

lemma arg_into_names_below2 :
  assumes "x,y  frecrel(names_below(,z))"
  shows  "x  names_below(,y)"
proof -
  from assms
  have "xnames_below(,z)" "ynames_below(,z)" "frecR(x,y)"
    unfolding frecrel_def Rrel_def
    by auto
  obtain f n1 n2 p where "x = f,n1,n2,p" "f2" "n1ecloseN(z)" "n2ecloseN(z)" "p"
    using xnames_below(,z)
    unfolding names_below_def by auto
  moreover
  obtain fy m1 m2 q where "q" "y = fy,m1,m2,q"
    using ynames_below(,z)
    unfolding names_below_def by auto
  moreover
  note frecR(x,y)
  ultimately
  show ?thesis
    using names_belowI by simp
qed

lemma arg_into_names_below :
  assumes "x,y  frecrel(names_below(,z))"
  shows  "x  names_below(,x)"
proof -
  from assms
  have "xnames_below(,z)"
    unfolding frecrel_def Rrel_def
    by auto
  from xnames_below(,z)
  obtain f n1 n2 p where
    "x = f,n1,n2,p" "f2" "n1ecloseN(z)" "n2ecloseN(z)" "p"
    unfolding names_below_def by auto
  then
  have "n1ecloseN(x)" "n2ecloseN(x)"
    using components_in_eclose by simp_all
  with f2 p x = f,n1,n2,p
  show ?thesis
    unfolding names_below_def by simp
qed

lemma forcerel_arg_into_names_below :
  assumes "x,y  forcerel(,z)"
  shows  "x  names_below(,x)"
  using assms
  unfolding forcerel_def
  by(rule trancl_induct;auto simp add: arg_into_names_below)

lemma names_below_mono :
  assumes "x,y  frecrel(names_below(,z))"
  shows "names_below(,x)  names_below(,y)"
proof -
  from assms
  have "xnames_below(,y)"
    using arg_into_names_below2 by simp
  then
  show ?thesis
    using names_below_tr subsetI by simp
qed

lemma frecrel_mono :
  assumes "x,y  frecrel(names_below(,z))"
  shows "frecrel(names_below(,x))  frecrel(names_below(,y))"
  unfolding frecrel_def
  using Rrel_mono names_below_mono assms by simp

lemma forcerel_mono2 :
  assumes "x,y  frecrel(names_below(,z))"
  shows "forcerel(,x)  forcerel(,y)"
  unfolding forcerel_def
  using trancl_mono frecrel_mono assms by simp

lemma forcerel_mono_aux :
  assumes "x,y  frecrel(names_below(, w))^+"
  shows "forcerel(,x)  forcerel(,y)"
  using assms
  by (rule trancl_induct,simp_all add: subset_trans forcerel_mono2)

lemma forcerel_mono :
  assumes "x,y  forcerel(,z)"
  shows "forcerel(,x)  forcerel(,y)"
  using forcerel_mono_aux assms unfolding forcerel_def by simp

lemma forcerel_eq_aux: "x  names_below(, w)  x,y  forcerel(,z) 
  (y  names_below(, w)  x,y  forcerel(,w))"
  unfolding forcerel_def
proof (rule_tac a=x and b=y and
    P="λ y . y  names_below(, w)  x,y  frecrel(names_below(,w))^+" in trancl_induct,simp)
  let ?A="λ a . names_below(, a)"
  let ?R="λ a . frecrel(?A(a))"
  let ?fR="λ a .forcerel(a)"
  show "u?A(w)  x,u?R(w)^+" if "x?A(w)" "x,y?R(z)^+" "x,u?R(z)"  for  u
    using that frecrelD frecrelI r_into_trancl
    unfolding names_below_def by simp
  {
    fix u v
    assume "x  ?A(w)"
      "x, y  ?R(z)^+"
      "x, u  ?R(z)^+"
      "u, v  ?R(z)"
      "u  ?A(w)  x, u  ?R(w)^+"
    then
    have "v  ?A(w)  x, v  ?R(w)^+"
    proof -
      assume "v ?A(w)"
      from u,v_
      have "u?A(v)"
        using arg_into_names_below2 by simp
      with v ?A(w)
      have "u?A(w)"
        using names_below_tr by simp
      with v_ u,v_
      have "u,v ?R(w)"
        using frecrelD frecrelI r_into_trancl unfolding names_below_def by simp
      with u  ?A(w)  x, u  ?R(w)^+ u?A(w)
      have "x, u  ?R(w)^+"
        by simp
      with u,v ?R(w)
      show "x,v ?R(w)^+" using trancl_trans r_into_trancl
        by simp
    qed
  }
  then
  show "v  ?A(w)  x, v  ?R(w)^+"
    if "x  ?A(w)"
      "x, y  ?R(z)^+"
      "x, u  ?R(z)^+"
      "u, v  ?R(z)"
      "u  ?A(w)  x, u  ?R(w)^+" for u v
    using that
    by simp
qed

lemma forcerel_eq :
  assumes "z,x  forcerel(,x)"
  shows "forcerel(,z) = forcerel(,x)  names_below(,z)×names_below(,z)"
  using assms forcerel_eq_aux forcerelD forcerel_mono[of z x x] subsetI
  by auto

lemma forcerel_below_aux :
  assumes "z,x  forcerel(,x)" "u,z  forcerel(,x)"
  shows "u  names_below(,z)"
  using assms(2)
  unfolding forcerel_def
proof(rule trancl_induct)
  show  "u  names_below(,y)" if " u, y  frecrel(names_below(, x))" for y
    using that vimage_singleton_iff arg_into_names_below2 by simp
next
  show "u  names_below(,z)"
    if "u, y  frecrel(names_below(, x))^+"
      "y, z  frecrel(names_below(, x))"
      "u  names_below(, y)"
    for y z
    using that arg_into_names_below2[of y z x] names_below_tr by simp
qed

lemma forcerel_below :
  assumes "z,x  forcerel(,x)"
  shows "forcerel(,x) -`` {z}  names_below(,z)"
  using vimage_singleton_iff assms forcerel_below_aux by auto

lemma relation_forcerel :
  shows "relation(forcerel(,z))" "trans(forcerel(,z))"
  unfolding forcerel_def using relation_trancl trans_trancl by simp_all

lemma Hfrc_restrict_trancl: "bool_of_o(Hfrc(, leq, y, restrict(f,frecrel(names_below(,x))-``{y})))
         = bool_of_o(Hfrc(, leq, y, restrict(f,(frecrel(names_below(,x))^+)-``{y})))"
  unfolding Hfrc_def bool_of_o_def eq_case_def mem_case_def
  using restrict_trancl_forcerel frecRI1 frecRI2 frecRI3
  unfolding forcerel_def
  by simp

(* Recursive definition of forces for atomic formulas using a transitive relation *)
lemma frc_at_trancl: "frc_at(,leq,z) = wfrec(forcerel(,z),z,λx f. bool_of_o(Hfrc(,leq,x,f)))"
  unfolding frc_at_def forcerel_def using wf_eq_trancl Hfrc_restrict_trancl by simp

lemma forcerelI1 :
  assumes "n1  domain(b)  n1  domain(c)" "p" "d"
  shows "1, n1, b, p, 0,b,c,d forcerel(,0,b,c,d)"
proof -
  let ?x="1, n1, b, p"
  let ?y="0,b,c,d"
  from assms
  have "frecR(?x,?y)"
    using frecRI1 by simp
  then
  have "?xnames_below(,?y)" "?y  names_below(,?y)"
    using names_belowI  assms components_in_eclose
    unfolding names_below_def by auto
  with frecR(?x,?y)
  show ?thesis
    unfolding forcerel_def frecrel_def
    using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
    by auto
qed

lemma forcerelI2 :
  assumes "n1  domain(b)  n1  domain(c)" "p" "d"
  shows "1, n1, c, p, 0,b,c,d forcerel(,0,b,c,d)"
proof -
  let ?x="1, n1, c, p"
  let ?y="0,b,c,d"
  note assms
  moreover from this
  have "frecR(?x,?y)"
    using frecRI2 by simp
  moreover from calculation
  have "?xnames_below(,?y)" "?y  names_below(,?y)"
    using names_belowI components_in_eclose
    unfolding names_below_def by auto
  ultimately
  show ?thesis
    unfolding forcerel_def frecrel_def
    using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
    by auto
qed

lemma forcerelI3 :
  assumes "n2, r  c" "p" "d" "r  "
  shows "0, b, n2, p,1, b, c, d  forcerel(,1,b,c,d)"
proof -
  let ?x="0, b, n2, p"
  let ?y="1, b, c, d"
  note assms
  moreover from this
  have "frecR(?x,?y)"
    using frecRI3 by simp
  moreover from calculation
  have "?xnames_below(,?y)"  "?y  names_below(,?y)"
    using names_belowI components_in_eclose
    unfolding names_below_def by auto
  ultimately
  show ?thesis
    unfolding forcerel_def frecrel_def
    using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
    by auto
qed

lemmas forcerelI = forcerelI1[THEN vimage_singleton_iff[THEN iffD2]]
  forcerelI2[THEN vimage_singleton_iff[THEN iffD2]]
  forcerelI3[THEN vimage_singleton_iff[THEN iffD2]]

lemma  aux_def_frc_at:
  assumes "z  forcerel(,x) -`` {x}"
  shows "wfrec(forcerel(,x), z, H) =  wfrec(forcerel(,z), z, H)"
proof -
  let ?A="names_below(,z)"
  from assms
  have "z,x  forcerel(,x)"
    using vimage_singleton_iff by simp
  moreover from this
  have "z  ?A"
    using forcerel_arg_into_names_below by simp
  moreover from calculation
  have "forcerel(,z) = forcerel(,x)  (?A×?A)"
    "forcerel(,x) -`` {z}  ?A"
    using forcerel_eq forcerel_below
    by auto
  moreover from calculation
  have "wfrec(forcerel(,x), z, H) = wfrec[?A](forcerel(,x), z, H)"
    using wfrec_trans_restr[OF relation_forcerel(1) wf_forcerel relation_forcerel(2), of x z ?A]
    by simp
  ultimately
  show ?thesis
    using wfrec_restr_eq by simp
qed

subsectionRecursive expression of termfrc_at

lemma def_frc_at :
  assumes "p"
  shows
    "frc_at(,leq,ft,n1,n2,p) =
   bool_of_o( p  
  (  ft = 0   (s. sdomain(n1)  domain(n2) 
        (q. q  q  p  (frc_at(,leq,1,s,n1,q) =1  frc_at(,leq,1,s,n2,q) =1)))
    ft = 1  ( v. v  p 
    (q. s. r. r  q  q  v  s,r  n2  q  r   frc_at(,leq,0,n1,s,q) = 1))))"
proof -
  let ?r="λy. forcerel(,y)" and ?Hf="λx f. bool_of_o(Hfrc(,leq,x,f))"
  let ?t="λy. ?r(y) -`` {y}"
  let ?arg="ft,n1,n2,p"
  from wf_forcerel
  have wfr: "w . wf(?r(w))" ..
  with wfrec [of "?r(?arg)" ?arg ?Hf]
  have "frc_at(,leq,?arg) = ?Hf( ?arg, λx?r(?arg) -`` {?arg}. wfrec(?r(?arg), x, ?Hf))"
    using frc_at_trancl by simp
  also
  have " ... = ?Hf( ?arg, λx?r(?arg) -`` {?arg}. frc_at(,leq,x))"
    using aux_def_frc_at frc_at_trancl by simp
  finally
  show ?thesis
    unfolding Hfrc_def mem_case_def eq_case_def
    using forcerelI  assms
    by auto
qed


subsectionAbsoluteness of termfrc_at

lemma forcerel_in_M :
  assumes "xM"
  shows "forcerel(,x)M"
  unfolding forcerel_def def_frecrel names_below_def
proof -
  let ?Q = "2 × ecloseN(x) × ecloseN(x) × "
  have "?Q × ?Q  M"
    using xM nat_into_M ecloseN_closed cartprod_closed by simp
  moreover
  have "separation(##M,λz. frecrelP(##M,z))"
    using separation_in_ctm[of "frecrelP_fm(0)",OF _ _ _ sats_frecrelP_fm]
      arity_frecrelP_fm frecrelP_fm_type
    by auto
  moreover from this
  have "separation(##M,λz. x y. z = x, y  frecR(x, y))"
    using separation_cong[OF frecrelP_abs]
    by force
  ultimately
  show "{z  ?Q × ?Q . x y. z = x, y  frecR(x, y)}^+  M"
    using separation_closed frecrelP_abs trancl_closed
    by simp
qed

lemma relation2_Hfrc_at_abs:
  "relation2(##M,is_Hfrc_at(##M,,leq),λx f. bool_of_o(Hfrc(,leq,x,f)))"
  unfolding relation2_def using Hfrc_at_abs
  by simp

lemma Hfrc_at_closed :
  "xM. gM. function(g)  bool_of_o(Hfrc(,leq,x,g))M"
  unfolding bool_of_o_def using zero_in_M nat_into_M[of 1] by simp

lemma wfrec_Hfrc_at :
  assumes "XM"
  shows "wfrec_replacement(##M,is_Hfrc_at(##M,,leq),forcerel(,X))"
proof -
  have 0:"is_Hfrc_at(##M,,leq,a,b,c) 
        sats(M,Hfrc_at_fm(8,9,2,1,0),[c,b,a,d,e,y,x,z,,leq,forcerel(,X)])"
    if "aM" "bM" "cM" "dM" "eM" "yM" "xM" "zM"
    for a b c d e y x z
    using that XM forcerel_in_M
      Hfrc_at_iff_sats[of concl:M  leq a b c 8 9 2 1 0]
    by simp
  have 1:"sats(M,is_wfrec_fm(Hfrc_at_fm(8,9,2,1,0),5,1,0),[y,x,z,,leq,forcerel(,X)]) 
                   is_wfrec(##M, is_Hfrc_at(##M,,leq),forcerel(,X), x, y)"
    if "xM" "yM" "zM" for x y z
    using that XM forcerel_in_M sats_is_wfrec_fm[OF 0]
    by simp
  let
    ?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(Hfrc_at_fm(8,9,2,1,0),5,1,0)))"
  have satsf:"sats(M, ?f, [x,z,,leq,forcerel(,X)]) 
              (yM. pair(##M,x,y,z) & is_wfrec(##M, is_Hfrc_at(##M,,leq),forcerel(,X), x, y))"
    if "xM" "zM" for x z
    using that 1 XM forcerel_in_M by (simp del:pair_abs)
  have artyf:"arity(?f) = 5"
    using arity_wfrec_replacement_fm[where p="Hfrc_at_fm(8,9,2,1,0)" and i=10]
      arity_Hfrc_at_fm ord_simp_union
    by simp
  moreover
  have "?fformula" by simp
  ultimately
  have "strong_replacement(##M,λx z. sats(M,?f,[x,z,,leq,forcerel(,X)]))"
    using ZF_ground_replacements(1) 1 artyf XM forcerel_in_M
    unfolding replacement_assm_def wfrec_Hfrc_at_fm_def by simp
  then
  have "strong_replacement(##M,λx z.
          yM. pair(##M,x,y,z) & is_wfrec(##M, is_Hfrc_at(##M,,leq),forcerel(,X), x, y))"
    using repl_sats[of M ?f "[,leq,forcerel(,X)]"] satsf by (simp del:pair_abs)
  then
  show ?thesis unfolding wfrec_replacement_def by simp
qed

lemma names_below_abs :
  "QM;xM;nbM  is_names_below(##M,Q,x,nb)  nb = names_below(Q,x)"
  unfolding is_names_below_def names_below_def
  using succ_in_M_iff zero_in_M cartprod_closed ecloseN_abs ecloseN_closed
  by auto

lemma names_below_closed:
  "QM;xM  names_below(Q,x)  M"
  unfolding names_below_def
  using zero_in_M cartprod_closed ecloseN_closed succ_in_M_iff
  by simp

lemma "names_below_productE" :
  assumes "Q  M" "x  M"
    "A1 A2 A3 A4. A1  M  A2  M  A3  M  A4  M  R(A1 × A2 × A3 × A4)"
  shows "R(names_below(Q,x))"
  unfolding names_below_def using assms nat_into_M ecloseN_closed[of x] by auto

lemma forcerel_abs :
  "xM;zM  is_forcerel(##M,,x,z)  z = forcerel(,x)"
  unfolding is_forcerel_def forcerel_def
  using frecrel_abs names_below_abs trancl_abs ecloseN_closed names_below_closed
    names_below_productE[of concl:"λp. is_frecrel(##M,p,_)   _ = frecrel(p)"] frecrel_closed
  by simp

lemma frc_at_abs:
  assumes "fnncM" "zM"
  shows "is_frc_at(##M,,leq,fnnc,z)  z = frc_at(,leq,fnnc)"
proof -
  from assms
  have "(rM. is_forcerel(##M,,fnnc, r)  is_wfrec(##M, is_Hfrc_at(##M, , leq), r, fnnc, z))
         is_wfrec(##M, is_Hfrc_at(##M, , leq), forcerel(,fnnc), fnnc, z)"
    using forcerel_abs forcerel_in_M by simp
  then
  show ?thesis
    unfolding frc_at_trancl is_frc_at_def
    using assms wfrec_Hfrc_at[of fnnc] wf_forcerel relation_forcerel forcerel_in_M
      Hfrc_at_closed relation2_Hfrc_at_abs
      trans_wfrec_abs[of "forcerel(,fnnc)" fnnc z "is_Hfrc_at(##M,,leq)" "λx f. bool_of_o(Hfrc(,leq,x,f))"]
    by (simp flip:setclass_iff)
qed

lemma forces_eq'_abs :
  "pM ; t1M ; t2M  is_forces_eq'(##M,,leq,p,t1,t2)  forces_eq'(,leq,p,t1,t2)"
  unfolding is_forces_eq'_def forces_eq'_def
  using frc_at_abs nat_into_M pair_in_M_iff by (auto simp add:components_abs)

lemma forces_mem'_abs :
  "pM ; t1M ; t2M  is_forces_mem'(##M,,leq,p,t1,t2)  forces_mem'(,leq,p,t1,t2)"
  unfolding is_forces_mem'_def forces_mem'_def
  using frc_at_abs nat_into_M pair_in_M_iff by (auto simp add:components_abs)

lemma forces_neq'_abs :
  assumes "pM" "t1M" "t2M"
  shows "is_forces_neq'(##M,,leq,p,t1,t2)  forces_neq'(,leq,p,t1,t2)"
proof -
  have "qM" if "q" for q
    using that transitivity by simp
  with assms
  show ?thesis
    unfolding is_forces_neq'_def forces_neq'_def
    using forces_eq'_abs pair_in_M_iff
    by (auto simp add:components_abs,blast)
qed

lemma forces_nmem'_abs :
  assumes "pM" "t1M" "t2M"
  shows "is_forces_nmem'(##M,,leq,p,t1,t2)  forces_nmem'(,leq,p,t1,t2)"
proof -
  have "qM" if "q" for q
    using that transitivity by simp
  with assms
  show ?thesis
    unfolding is_forces_nmem'_def forces_nmem'_def
    using forces_mem'_abs pair_in_M_iff
    by (auto simp add:components_abs,blast)
qed

lemma leq_abs:
  " lM ; qM ; pM   is_leq(##M,l,q,p)  q,pl"
  unfolding is_leq_def using pair_in_M_iff by simp

subsectionForcing for atomic formulas in context

definition
  forces_eq :: "[i,i,i]  o" (_ forcesa '(_ = _') [36,1,1] 60) where
  "forces_eq  forces_eq'(,leq)"

definition
  forces_mem :: "[i,i,i]  o" (_ forcesa '(_  _') [36,1,1] 60) where
  "forces_mem  forces_mem'(,leq)"

(* frc_at(ℙ,leq,⟨0,t1,t2,p⟩) = 1*)
abbreviation is_forces_eq
  where "is_forces_eq  is_forces_eq'(##M,,leq)"

(* frc_at(ℙ,leq,⟨1,t1,t2,p⟩) = 1*)
abbreviation
  is_forces_mem :: "[i,i,i]  o" where
  "is_forces_mem  is_forces_mem'(##M,,leq)"

lemma def_forces_eq: "p  p forcesa (t1 = t2) 
      (sdomain(t1)  domain(t2). q. q  q  p 
      (q forcesa (s  t1)  q forcesa (s  t2)))"
  unfolding forces_eq_def forces_mem_def forces_eq'_def forces_mem'_def
  using def_frc_at[of p 0 t1 t2 ]
  unfolding bool_of_o_def
  by auto

lemma def_forces_mem: "p  p forcesa (t1  t2) 
     (v. v  p 
      (q. s. r. r  q  q  v  s,r  t2  q  r  q forcesa (t1 = s)))"
  unfolding forces_eq'_def forces_mem'_def forces_eq_def forces_mem_def
  using def_frc_at[of p 1 t1 t2]
  unfolding bool_of_o_def
  by auto

lemma forces_eq_abs :
  "pM ; t1M ; t2M  is_forces_eq(p,t1,t2)  p forcesa (t1 = t2)"
  unfolding forces_eq_def
  using forces_eq'_abs by simp

lemma forces_mem_abs :
  "pM ; t1M ; t2M  is_forces_mem(p,t1,t2)  p forcesa (t1  t2)"
  unfolding forces_mem_def
  using forces_mem'_abs
  by simp

definition
  forces_neq :: "[i,i,i]  o" (_ forcesa '(_  _') [36,1,1] 60) where
  "p forcesa (t1  t2)  ¬ (q. qp  q forcesa (t1 = t2))"

definition
  forces_nmem :: "[i,i,i]  o" (_ forcesa '(_  _') [36,1,1] 60) where
  "p forcesa (t1  t2)  ¬ (q. qp  q forcesa (t1  t2))"

lemma forces_neq :
  "p forcesa (t1  t2)  forces_neq'(,leq,p,t1,t2)"
  unfolding forces_neq_def forces_neq'_def forces_eq_def by simp

lemma forces_nmem :
  "p forcesa (t1  t2)  forces_nmem'(,leq,p,t1,t2)"
  unfolding forces_nmem_def forces_nmem'_def forces_mem_def by simp

abbreviation Forces :: "[i, i, i]  o"  ("_  _ _" [36,36,36] 60) where
  "p  φ env      M, ([p,,leq,𝟭] @ env)  forces(φ)"

lemma sats_forces_Member :
  assumes  "xnat" "ynat" "envlist(M)"
    "nth(x,env)=xx" "nth(y,env)=yy" "qM"
  shows "q  x  y env  q    is_forces_mem(q, xx, yy)"
  unfolding forces_def
  using assms
  by simp

lemma sats_forces_Equal :
  assumes "anat" "bnat" "envlist(M)" "nth(a,env)=x" "nth(b,env)=y" "qM"
  shows "q  a = b env  q    is_forces_eq(q, x, y)"
  unfolding forces_def
  using assms
  by simp

lemma sats_forces_Nand :
  assumes "φformula" "ψformula" "envlist(M)" "pM"
  shows "p  ⋅¬(φ  ψ)⋅ env 
    p  ¬(qM. q  is_leq(##M,leq,q,p)  (q  φ env)  (q  ψ env))"
  unfolding forces_def
  using sats_is_leq_fm_auto assms sats_ren_forces_nand zero_in_M
  by simp

lemma sats_forces_Neg :
  assumes "φformula" "envlist(M)" "pM"
  shows "p  ⋅¬φ env 
         (p  ¬(qM. q  is_leq(##M,leq,q,p)  (q  φ env)))"
  unfolding Neg_def using assms sats_forces_Nand
  by simp

lemma sats_forces_Forall :
  assumes "φformula" "envlist(M)" "pM"
  shows "p  (⋅∀φ⋅) env  p    (xM. p  φ ([x] @ env))"
  unfolding forces_def using assms sats_ren_forces_forall
  by simp

end ― ‹localeforcing_data1

end