diff --git a/thys/Forcing/Forces_Definition.thy b/thys/Forcing/Forces_Definition.thy
--- a/thys/Forcing/Forces_Definition.thy
+++ b/thys/Forcing/Forces_Definition.thy
@@ -1,1793 +1,1793 @@
 section\<open>The definition of \<^term>\<open>forces\<close>\<close>
 theory Forces_Definition imports Arities FrecR Synthetic_Definition begin
 
 text\<open>This is the core of our development.\<close>
 
 subsection\<open>The relation \<^term>\<open>frecrel\<close>\<close>
 
 definition
   frecrelP :: "[i\<Rightarrow>o,i] \<Rightarrow> o" where
   "frecrelP(M,xy) \<equiv> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,xy) \<and> is_frecR(M,x,y))"
 
 definition
   frecrelP_fm :: "i \<Rightarrow> i" where
-  "frecrelP_fm(a) \<equiv> Exists(Exists(And(pair_fm(1,0,a#+2),frecR_fm(0,1))))"
+  "frecrelP_fm(a) \<equiv> Exists(Exists(And(pair_fm(1,0,a#+2),frecR_fm(1,0))))"
 
 lemma arity_frecrelP_fm :
   "a\<in>nat \<Longrightarrow> arity(frecrelP_fm(a)) = succ(a)"
   unfolding frecrelP_fm_def
   using arity_frecR_fm arity_pair_fm pred_Un_distrib
   by simp
 
 lemma frecrelP_fm_type[TC] :
   "a\<in>nat \<Longrightarrow> frecrelP_fm(a)\<in>formula"
   unfolding frecrelP_fm_def by simp
 
 lemma sats_frecrelP_fm :
   assumes "a\<in>nat" "env\<in>list(A)"
   shows "sats(A,frecrelP_fm(a),env) \<longleftrightarrow> frecrelP(##A,nth(a, env))"
   unfolding frecrelP_def frecrelP_fm_def
   using assms by (auto simp add:frecR_fm_iff_sats[symmetric])
 
 lemma frecrelP_iff_sats:
   assumes
     "nth(a,env) = aa" "a\<in> nat"  "env \<in> list(A)"
   shows
     "frecrelP(##A,aa)  \<longleftrightarrow> sats(A, frecrelP_fm(a), env)"
   using assms
   by (simp add:sats_frecrelP_fm)
 
 definition
   is_frecrel :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
   "is_frecrel(M,A,r) \<equiv> \<exists>A2[M]. cartprod(M,A,A,A2) \<and> is_Collect(M,A2, frecrelP(M) ,r)"
 
 definition
   frecrel_fm :: "[i,i] \<Rightarrow> i" where
   "frecrel_fm(a,r) \<equiv> Exists(And(cartprod_fm(a#+1,a#+1,0),Collect_fm(0,frecrelP_fm(0),r#+1)))"
 
 lemma frecrel_fm_type[TC] :
   "\<lbrakk>a\<in>nat;b\<in>nat\<rbrakk> \<Longrightarrow> frecrel_fm(a,b)\<in>formula"
   unfolding frecrel_fm_def by simp
 
 lemma arity_frecrel_fm :
   assumes "a\<in>nat"  "b\<in>nat"
   shows "arity(frecrel_fm(a,b)) = succ(a) \<union> succ(b)"
   unfolding frecrel_fm_def
   using assms arity_Collect_fm arity_cartprod_fm arity_frecrelP_fm pred_Un_distrib
   by auto
 
 lemma sats_frecrel_fm :
   assumes
     "a\<in>nat"  "r\<in>nat" "env\<in>list(A)"
   shows
     "sats(A,frecrel_fm(a,r),env)
     \<longleftrightarrow> is_frecrel(##A,nth(a, env),nth(r, env))"
   unfolding is_frecrel_def frecrel_fm_def
   using assms
   by (simp add:sats_Collect_fm sats_frecrelP_fm)
 
 lemma is_frecrel_iff_sats:
   assumes
     "nth(a,env) = aa" "nth(r,env) = rr" "a\<in> nat"  "r\<in> nat"  "env \<in> list(A)"
   shows
     "is_frecrel(##A, aa,rr) \<longleftrightarrow> sats(A, frecrel_fm(a,r), env)"
   using assms
   by (simp add:sats_frecrel_fm)
 
 definition
   names_below :: "i \<Rightarrow> i \<Rightarrow> i" where
   "names_below(P,x) \<equiv> 2\<times>ecloseN(x)\<times>ecloseN(x)\<times>P"
 
 lemma names_belowsD:
   assumes "x \<in> names_below(P,z)"
   obtains f n1 n2 p where
     "x = \<langle>f,n1,n2,p\<rangle>" "f\<in>2" "n1\<in>ecloseN(z)" "n2\<in>ecloseN(z)" "p\<in>P"
   using assms unfolding names_below_def by auto
 
 
 definition
   is_names_below :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
   "is_names_below(M,P,x,nb) \<equiv> \<exists>p1[M]. \<exists>p0[M]. \<exists>t[M]. \<exists>ec[M].
               is_ecloseN(M,ec,x) \<and> number2(M,t) \<and> cartprod(M,ec,P,p0) \<and> cartprod(M,ec,p0,p1)
               \<and> cartprod(M,t,p1,nb)"
 
 definition
   number2_fm :: "i\<Rightarrow>i" where
   "number2_fm(a) \<equiv> Exists(And(number1_fm(0), succ_fm(0,succ(a))))"
 
 lemma number2_fm_type[TC] :
   "a\<in>nat \<Longrightarrow> number2_fm(a) \<in> formula"
   unfolding number2_fm_def by simp
 
 lemma number2arity__fm :
   "a\<in>nat \<Longrightarrow> arity(number2_fm(a)) = succ(a)"
   unfolding number2_fm_def
   using number1arity__fm arity_succ_fm nat_union_abs2 pred_Un_distrib
   by simp
 
 lemma sats_number2_fm [simp]:
   "\<lbrakk> x \<in> nat; env \<in> list(A) \<rbrakk>
     \<Longrightarrow> sats(A, number2_fm(x), env) \<longleftrightarrow> number2(##A, nth(x,env))"
   by (simp add: number2_fm_def number2_def)
 
 definition
   is_names_below_fm :: "[i,i,i] \<Rightarrow> i" where
   "is_names_below_fm(P,x,nb) \<equiv> Exists(Exists(Exists(Exists(
                     And(ecloseN_fm(0,x #+ 4),And(number2_fm(1),
                     And(cartprod_fm(0,P #+ 4,2),And(cartprod_fm(0,2,3),cartprod_fm(1,3,nb#+4)))))))))"
 
 lemma arity_is_names_below_fm :
   "\<lbrakk>P\<in>nat;x\<in>nat;nb\<in>nat\<rbrakk> \<Longrightarrow> arity(is_names_below_fm(P,x,nb)) = succ(P) \<union> succ(x) \<union> succ(nb)"
   unfolding is_names_below_fm_def
   using arity_cartprod_fm number2arity__fm arity_ecloseN_fm nat_union_abs2 pred_Un_distrib
   by auto
 
 
 lemma is_names_below_fm_type[TC]:
   "\<lbrakk>P\<in>nat;x\<in>nat;nb\<in>nat\<rbrakk> \<Longrightarrow> is_names_below_fm(P,x,nb)\<in>formula"
   unfolding is_names_below_fm_def by simp
 
 lemma sats_is_names_below_fm :
   assumes
     "P\<in>nat" "x\<in>nat" "nb\<in>nat" "env\<in>list(A)"
   shows
     "sats(A,is_names_below_fm(P,x,nb),env)
     \<longleftrightarrow> is_names_below(##A,nth(P, env),nth(x, env),nth(nb, env))"
   unfolding is_names_below_fm_def is_names_below_def using assms by simp
 
 definition
   is_tuple :: "[i\<Rightarrow>o,i,i,i,i,i] \<Rightarrow> o" where
   "is_tuple(M,z,t1,t2,p,t) \<equiv> \<exists>t1t2p[M]. \<exists>t2p[M]. pair(M,t2,p,t2p) \<and> pair(M,t1,t2p,t1t2p) \<and>
                                                   pair(M,z,t1t2p,t)"
 
 
 definition
   is_tuple_fm :: "[i,i,i,i,i] \<Rightarrow> i" where
   "is_tuple_fm(z,t1,t2,p,tup) = Exists(Exists(And(pair_fm(t2 #+ 2,p #+ 2,0),
                       And(pair_fm(t1 #+ 2,0,1),pair_fm(z #+ 2,1,tup #+ 2)))))"
 
 
 lemma arity_is_tuple_fm : "\<lbrakk> z\<in>nat ; t1\<in>nat ; t2\<in>nat ; p\<in>nat ; tup\<in>nat \<rbrakk> \<Longrightarrow>
   arity(is_tuple_fm(z,t1,t2,p,tup)) = \<Union> {succ(z),succ(t1),succ(t2),succ(p),succ(tup)}"
   unfolding is_tuple_fm_def
   using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib
   by auto
 
 lemma is_tuple_fm_type[TC] :
   "z\<in>nat \<Longrightarrow> t1\<in>nat \<Longrightarrow> t2\<in>nat \<Longrightarrow> p\<in>nat \<Longrightarrow> tup\<in>nat \<Longrightarrow> is_tuple_fm(z,t1,t2,p,tup)\<in>formula"
   unfolding is_tuple_fm_def by simp
 
 lemma sats_is_tuple_fm :
   assumes
     "z\<in>nat"  "t1\<in>nat" "t2\<in>nat" "p\<in>nat" "tup\<in>nat" "env\<in>list(A)"
   shows
     "sats(A,is_tuple_fm(z,t1,t2,p,tup),env)
     \<longleftrightarrow> is_tuple(##A,nth(z, env),nth(t1, env),nth(t2, env),nth(p, env),nth(tup, env))"
   unfolding is_tuple_def is_tuple_fm_def using assms by simp
 
 lemma is_tuple_iff_sats:
   assumes
     "nth(a,env) = aa" "nth(b,env) = bb" "nth(c,env) = cc" "nth(d,env) = dd" "nth(e,env) = ee"
     "a\<in>nat" "b\<in>nat" "c\<in>nat" "d\<in>nat" "e\<in>nat"  "env \<in> list(A)"
   shows
     "is_tuple(##A,aa,bb,cc,dd,ee)  \<longleftrightarrow> sats(A, is_tuple_fm(a,b,c,d,e), env)"
   using assms by (simp add: sats_is_tuple_fm)
 
 subsection\<open>Definition of \<^term>\<open>forces\<close> for equality and membership\<close>
 
 (* p ||- \<tau> = \<theta> \<equiv>
   \<forall>\<sigma>. \<sigma>\<in>domain(\<tau>) \<union> domain(\<theta>) \<longrightarrow> (\<forall>q\<in>P. \<langle>q,p\<rangle>\<in>leq \<longrightarrow> ((q ||- \<sigma>\<in>\<tau>) \<longleftrightarrow> (q ||- \<sigma>\<in>\<theta>)) ) *)
 definition
   eq_case :: "[i,i,i,i,i,i] \<Rightarrow> o" where
   "eq_case(t1,t2,p,P,leq,f) \<equiv> \<forall>s. s\<in>domain(t1) \<union> domain(t2) \<longrightarrow>
       (\<forall>q. q\<in>P \<and> \<langle>q,p\<rangle>\<in>leq \<longrightarrow> (f`\<langle>1,s,t1,q\<rangle>=1  \<longleftrightarrow> f`\<langle>1,s,t2,q\<rangle> =1))"
 
 
 definition
   is_eq_case :: "[i\<Rightarrow>o,i,i,i,i,i,i] \<Rightarrow> o" where
   "is_eq_case(M,t1,t2,p,P,leq,f) \<equiv>
    \<forall>s[M]. (\<exists>d[M]. is_domain(M,t1,d) \<and> s\<in>d) \<or> (\<exists>d[M]. is_domain(M,t2,d) \<and> s\<in>d)
        \<longrightarrow> (\<forall>q[M]. q\<in>P \<and> (\<exists>qp[M]. pair(M,q,p,qp) \<and> qp\<in>leq) \<longrightarrow>
             (\<exists>ost1q[M]. \<exists>ost2q[M]. \<exists>o[M].  \<exists>vf1[M]. \<exists>vf2[M].
              is_tuple(M,o,s,t1,q,ost1q) \<and>
              is_tuple(M,o,s,t2,q,ost2q) \<and> number1(M,o) \<and>
              fun_apply(M,f,ost1q,vf1) \<and> fun_apply(M,f,ost2q,vf2) \<and>
              (vf1 = o \<longleftrightarrow> vf2 = o)))"
 
 (* p ||-
    \<pi> \<in> \<tau> \<equiv> \<forall>v\<in>P. \<langle>v,p\<rangle>\<in>leq \<longrightarrow> (\<exists>q\<in>P. \<langle>q,v\<rangle>\<in>leq \<and> (\<exists>\<sigma>. \<exists>r\<in>P. \<langle>\<sigma>,r\<rangle>\<in>\<tau> \<and> \<langle>q,r\<rangle>\<in>leq \<and>  q ||- \<pi> = \<sigma>)) *)
 definition
   mem_case :: "[i,i,i,i,i,i] \<Rightarrow> o" where
   "mem_case(t1,t2,p,P,leq,f) \<equiv> \<forall>v\<in>P. \<langle>v,p\<rangle>\<in>leq \<longrightarrow>
     (\<exists>q. \<exists>s. \<exists>r. r\<in>P \<and> q\<in>P \<and> \<langle>q,v\<rangle>\<in>leq \<and> \<langle>s,r\<rangle> \<in> t2 \<and> \<langle>q,r\<rangle>\<in>leq \<and>  f`\<langle>0,t1,s,q\<rangle> = 1)"
 
 definition
   is_mem_case :: "[i\<Rightarrow>o,i,i,i,i,i,i] \<Rightarrow> o" where
   "is_mem_case(M,t1,t2,p,P,leq,f) \<equiv> \<forall>v[M]. \<forall>vp[M]. v\<in>P \<and> pair(M,v,p,vp) \<and> vp\<in>leq \<longrightarrow>
     (\<exists>q[M]. \<exists>s[M]. \<exists>r[M]. \<exists>qv[M]. \<exists>sr[M]. \<exists>qr[M]. \<exists>z[M]. \<exists>zt1sq[M]. \<exists>o[M].
      r\<in> P \<and> q\<in>P \<and> pair(M,q,v,qv) \<and> pair(M,s,r,sr) \<and> pair(M,q,r,qr) \<and>
      empty(M,z) \<and> is_tuple(M,z,t1,s,q,zt1sq) \<and>
      number1(M,o) \<and> qv\<in>leq \<and> sr\<in>t2 \<and> qr\<in>leq \<and> fun_apply(M,f,zt1sq,o))"
 
 
 schematic_goal sats_is_mem_case_fm_auto:
   assumes
     "n1\<in>nat" "n2\<in>nat" "p\<in>nat" "P\<in>nat" "leq\<in>nat" "f\<in>nat" "env\<in>list(A)"
   shows
     "is_mem_case(##A, nth(n1, env),nth(n2, env),nth(p, env),nth(P, env), nth(leq, env),nth(f,env))
     \<longleftrightarrow> sats(A,?imc_fm(n1,n2,p,P,leq,f),env)"
   unfolding is_mem_case_def
   by (insert assms ; (rule sep_rules'  is_tuple_iff_sats | simp)+)
 
 
 synthesize "mem_case_fm" from_schematic sats_is_mem_case_fm_auto
 
 lemma arity_mem_case_fm :
   assumes
     "n1\<in>nat" "n2\<in>nat" "p\<in>nat" "P\<in>nat" "leq\<in>nat" "f\<in>nat"
   shows
     "arity(mem_case_fm(n1,n2,p,P,leq,f)) =
     succ(n1) \<union> succ(n2) \<union> succ(p) \<union> succ(P) \<union> succ(leq) \<union> succ(f)"
   unfolding mem_case_fm_def
   using assms arity_pair_fm arity_is_tuple_fm number1arity__fm arity_fun_apply_fm arity_empty_fm
     pred_Un_distrib
   by auto
 
 schematic_goal sats_is_eq_case_fm_auto:
   assumes
     "n1\<in>nat" "n2\<in>nat" "p\<in>nat" "P\<in>nat" "leq\<in>nat" "f\<in>nat" "env\<in>list(A)"
   shows
     "is_eq_case(##A, nth(n1, env),nth(n2, env),nth(p, env),nth(P, env), nth(leq, env),nth(f,env))
     \<longleftrightarrow> sats(A,?iec_fm(n1,n2,p,P,leq,f),env)"
   unfolding is_eq_case_def
   by (insert assms ; (rule sep_rules'  is_tuple_iff_sats | simp)+)
 
 synthesize "eq_case_fm" from_schematic sats_is_eq_case_fm_auto
 
 lemma arity_eq_case_fm :
   assumes
     "n1\<in>nat" "n2\<in>nat" "p\<in>nat" "P\<in>nat" "leq\<in>nat" "f\<in>nat"
   shows
     "arity(eq_case_fm(n1,n2,p,P,leq,f)) =
     succ(n1) \<union> succ(n2) \<union> succ(p) \<union> succ(P) \<union> succ(leq) \<union> succ(f)"
   unfolding eq_case_fm_def
   using assms arity_pair_fm arity_is_tuple_fm number1arity__fm arity_fun_apply_fm arity_empty_fm
     arity_domain_fm pred_Un_distrib
   by auto
 
 definition
   Hfrc :: "[i,i,i,i] \<Rightarrow> o" where
   "Hfrc(P,leq,fnnc,f) \<equiv> \<exists>ft. \<exists>n1. \<exists>n2. \<exists>c. c\<in>P \<and> fnnc = \<langle>ft,n1,n2,c\<rangle> \<and>
      (  ft = 0 \<and>  eq_case(n1,n2,c,P,leq,f)
       \<or> ft = 1 \<and> mem_case(n1,n2,c,P,leq,f))"
 
 definition
   is_Hfrc :: "[i\<Rightarrow>o,i,i,i,i] \<Rightarrow> o" where
   "is_Hfrc(M,P,leq,fnnc,f) \<equiv>
      \<exists>ft[M]. \<exists>n1[M]. \<exists>n2[M]. \<exists>co[M].
       co\<in>P \<and> is_tuple(M,ft,n1,n2,co,fnnc) \<and>
       (  (empty(M,ft) \<and> is_eq_case(M,n1,n2,co,P,leq,f))
        \<or> (number1(M,ft) \<and>  is_mem_case(M,n1,n2,co,P,leq,f)))"
 
 definition
   Hfrc_fm :: "[i,i,i,i] \<Rightarrow> i" where
   "Hfrc_fm(P,leq,fnnc,f) \<equiv>
     Exists(Exists(Exists(Exists(
       And(Member(0,P #+ 4),And(is_tuple_fm(3,2,1,0,fnnc #+ 4),
-      Or(And(empty_fm(3),eq_case_fm(leq #+ 4,1,2,0,f #+ 4,P #+ 4)),
-         And(number1_fm(3),mem_case_fm(leq #+ 4,1,2,0,f #+ 4,P #+ 4)))))))))"
+      Or(And(empty_fm(3),eq_case_fm(2,1,0,P #+ 4,leq #+ 4,f #+ 4)),
+         And(number1_fm(3),mem_case_fm(2,1,0,P #+ 4,leq #+ 4,f #+ 4)))))))))"
 
 lemma Hfrc_fm_type[TC] :
   "\<lbrakk>P\<in>nat;leq\<in>nat;fnnc\<in>nat;f\<in>nat\<rbrakk> \<Longrightarrow> Hfrc_fm(P,leq,fnnc,f)\<in>formula"
   unfolding Hfrc_fm_def by simp
 
 lemma arity_Hfrc_fm :
   assumes
     "P\<in>nat" "leq\<in>nat" "fnnc\<in>nat" "f\<in>nat"
   shows
     "arity(Hfrc_fm(P,leq,fnnc,f)) = succ(P) \<union> succ(leq) \<union> succ(fnnc) \<union> succ(f)"
   unfolding Hfrc_fm_def
   using assms arity_is_tuple_fm arity_mem_case_fm arity_eq_case_fm
     arity_empty_fm number1arity__fm pred_Un_distrib
   by auto
 
 lemma sats_Hfrc_fm:
   assumes
     "P\<in>nat" "leq\<in>nat" "fnnc\<in>nat" "f\<in>nat" "env\<in>list(A)"
   shows
     "sats(A,Hfrc_fm(P,leq,fnnc,f),env)
     \<longleftrightarrow> is_Hfrc(##A,nth(P, env), nth(leq, env), nth(fnnc, env),nth(f, env))"
   unfolding is_Hfrc_def Hfrc_fm_def
   using assms  
   by (simp add: sats_is_tuple_fm eq_case_fm_iff_sats[symmetric] mem_case_fm_iff_sats[symmetric])
 
 lemma Hfrc_iff_sats:
   assumes
     "P\<in>nat" "leq\<in>nat" "fnnc\<in>nat" "f\<in>nat" "env\<in>list(A)"
     "nth(P,env) = PP"  "nth(leq,env) = lleq" "nth(fnnc,env) = ffnnc" "nth(f,env) = ff"
   shows
     "is_Hfrc(##A, PP, lleq,ffnnc,ff)
     \<longleftrightarrow> sats(A,Hfrc_fm(P,leq,fnnc,f),env)"
   using assms
   by (simp add:sats_Hfrc_fm)
 
 definition
   is_Hfrc_at :: "[i\<Rightarrow>o,i,i,i,i,i] \<Rightarrow> o" where
   "is_Hfrc_at(M,P,leq,fnnc,f,z) \<equiv>
             (empty(M,z) \<and> \<not> is_Hfrc(M,P,leq,fnnc,f))
           \<or> (number1(M,z) \<and> is_Hfrc(M,P,leq,fnnc,f))"
 
 definition
   Hfrc_at_fm :: "[i,i,i,i,i] \<Rightarrow> i" where
   "Hfrc_at_fm(P,leq,fnnc,f,z) \<equiv> Or(And(empty_fm(z),Neg(Hfrc_fm(P,leq,fnnc,f))),
                                       And(number1_fm(z),Hfrc_fm(P,leq,fnnc,f)))"
 
 lemma arity_Hfrc_at_fm :
   assumes
     "P\<in>nat" "leq\<in>nat" "fnnc\<in>nat" "f\<in>nat" "z\<in>nat"
   shows
     "arity(Hfrc_at_fm(P,leq,fnnc,f,z)) = succ(P) \<union> succ(leq) \<union> succ(fnnc) \<union> succ(f) \<union> succ(z)"
   unfolding Hfrc_at_fm_def
   using assms arity_Hfrc_fm arity_empty_fm number1arity__fm pred_Un_distrib
   by auto
 
 
 lemma Hfrc_at_fm_type[TC] :
   "\<lbrakk>P\<in>nat;leq\<in>nat;fnnc\<in>nat;f\<in>nat;z\<in>nat\<rbrakk> \<Longrightarrow> Hfrc_at_fm(P,leq,fnnc,f,z)\<in>formula"
   unfolding Hfrc_at_fm_def by simp
 
 lemma sats_Hfrc_at_fm:
   assumes
     "P\<in>nat" "leq\<in>nat" "fnnc\<in>nat" "f\<in>nat" "z\<in>nat" "env\<in>list(A)"
   shows
     "sats(A,Hfrc_at_fm(P,leq,fnnc,f,z),env)
     \<longleftrightarrow> is_Hfrc_at(##A,nth(P, env), nth(leq, env), nth(fnnc, env),nth(f, env),nth(z, env))"
   unfolding is_Hfrc_at_def Hfrc_at_fm_def using assms sats_Hfrc_fm
   by simp
 
 lemma is_Hfrc_at_iff_sats:
   assumes
     "P\<in>nat" "leq\<in>nat" "fnnc\<in>nat" "f\<in>nat" "z\<in>nat" "env\<in>list(A)"
     "nth(P,env) = PP"  "nth(leq,env) = lleq" "nth(fnnc,env) = ffnnc"
     "nth(f,env) = ff" "nth(z,env) = zz"
   shows
     "is_Hfrc_at(##A, PP, lleq,ffnnc,ff,zz)
     \<longleftrightarrow> sats(A,Hfrc_at_fm(P,leq,fnnc,f,z),env)"
   using assms by (simp add:sats_Hfrc_at_fm)
 
 lemma arity_tran_closure_fm :
   "\<lbrakk>x\<in>nat;f\<in>nat\<rbrakk> \<Longrightarrow> arity(trans_closure_fm(x,f)) = succ(x) \<union> succ(f)"
   unfolding trans_closure_fm_def
   using arity_omega_fm arity_field_fm arity_typed_function_fm arity_pair_fm arity_empty_fm arity_fun_apply_fm
     arity_composition_fm arity_succ_fm nat_union_abs2 pred_Un_distrib 
   by auto
 
 subsection\<open>The well-founded relation \<^term>\<open>forcerel\<close>\<close>
 definition
   forcerel :: "i \<Rightarrow> i \<Rightarrow> i" where
   "forcerel(P,x) \<equiv> frecrel(names_below(P,x))^+"
 
 definition
   is_forcerel :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
   "is_forcerel(M,P,x,z) \<equiv> \<exists>r[M]. \<exists>nb[M]. tran_closure(M,r,z) \<and>
                         (is_names_below(M,P,x,nb) \<and> is_frecrel(M,nb,r))"
 
 definition
   forcerel_fm :: "i\<Rightarrow> i \<Rightarrow> i \<Rightarrow> i" where
-  "forcerel_fm(p,x,z) \<equiv> Exists(Exists(And(trans_closure_fm(z#+2,1),
+  "forcerel_fm(p,x,z) \<equiv> Exists(Exists(And(trans_closure_fm(1, z#+2),
                                         And(is_names_below_fm(p#+2,x#+2,0),frecrel_fm(0,1)))))"
 
 lemma arity_forcerel_fm:
   "\<lbrakk>p\<in>nat;x\<in>nat;z\<in>nat\<rbrakk> \<Longrightarrow> arity(forcerel_fm(p,x,z)) = succ(p) \<union> succ(x) \<union> succ(z)"
   unfolding forcerel_fm_def
   using arity_frecrel_fm arity_tran_closure_fm arity_is_names_below_fm pred_Un_distrib
   by auto
 
 lemma forcerel_fm_type[TC]:
   "\<lbrakk>p\<in>nat;x\<in>nat;z\<in>nat\<rbrakk> \<Longrightarrow> forcerel_fm(p,x,z)\<in>formula"
   unfolding forcerel_fm_def by simp
 
 
 lemma sats_forcerel_fm:
   assumes
     "p\<in>nat" "x\<in>nat"  "z\<in>nat" "env\<in>list(A)"
   shows
     "sats(A,forcerel_fm(p,x,z),env) \<longleftrightarrow> is_forcerel(##A,nth(p,env),nth(x, env),nth(z, env))"
 proof -
-  have "sats(A,trans_closure_fm(z #+ 2,1),Cons(nb,Cons(r,env))) \<longleftrightarrow>
+  have "sats(A,trans_closure_fm(1,z #+ 2),Cons(nb,Cons(r,env))) \<longleftrightarrow>
         tran_closure(##A, r, nth(z, env))" if "r\<in>A" "nb\<in>A" for r nb
     using that assms trans_closure_fm_iff_sats[of 1 "[nb,r]@env" _ "z#+2",symmetric] by simp
   moreover
   have "sats(A, is_names_below_fm(succ(succ(p)), succ(succ(x)), 0), Cons(nb, Cons(r, env))) \<longleftrightarrow>
         is_names_below(##A, nth(p,env), nth(x, env), nb)"
     if "r\<in>A" "nb\<in>A" for nb r
     using assms that sats_is_names_below_fm[of "p #+ 2" "x #+ 2" 0 "[nb,r]@env"] by simp
   moreover
   have "sats(A, frecrel_fm(0, 1), Cons(nb, Cons(r, env))) \<longleftrightarrow>
         is_frecrel(##A, nb, r)"
     if "r\<in>A" "nb\<in>A" for r nb
     using assms that sats_frecrel_fm[of 0 1 "[nb,r]@env"] by simp
   ultimately
   show ?thesis using assms unfolding is_forcerel_def forcerel_fm_def by simp
 qed
 
 subsection\<open>\<^term>\<open>frc_at\<close>, forcing for atomic formulas\<close>
 definition
   frc_at :: "[i,i,i] \<Rightarrow> i" where
   "frc_at(P,leq,fnnc) \<equiv> wfrec(frecrel(names_below(P,fnnc)),fnnc,
                               \<lambda>x f. bool_of_o(Hfrc(P,leq,x,f)))"
 
 definition
   is_frc_at :: "[i\<Rightarrow>o,i,i,i,i] \<Rightarrow> o" where
   "is_frc_at(M,P,leq,x,z) \<equiv> \<exists>r[M]. is_forcerel(M,P,x,r) \<and>
                                     is_wfrec(M,is_Hfrc_at(M,P,leq),r,x,z)"
 
 definition
   frc_at_fm :: "[i,i,i,i] \<Rightarrow> i" where
   "frc_at_fm(p,l,x,z) \<equiv> Exists(And(forcerel_fm(succ(p),succ(x),0),
           is_wfrec_fm(Hfrc_at_fm(6#+p,6#+l,2,1,0),0,succ(x),succ(z))))"
 
 lemma frc_at_fm_type [TC] :
   "\<lbrakk>p\<in>nat;l\<in>nat;x\<in>nat;z\<in>nat\<rbrakk> \<Longrightarrow> frc_at_fm(p,l,x,z)\<in>formula"
   unfolding frc_at_fm_def by simp
 
 lemma arity_frc_at_fm :
   assumes "p\<in>nat" "l\<in>nat" "x\<in>nat" "z\<in>nat"
   shows "arity(frc_at_fm(p,l,x,z)) = succ(p) \<union> succ(l) \<union> succ(x) \<union> succ(z)"
 proof -
   let ?\<phi> = "Hfrc_at_fm(6 #+ p, 6 #+ l, 2, 1, 0)"
   from assms
   have  "arity(?\<phi>) = (7#+p) \<union> (7#+l)" "?\<phi> \<in> formula"
     using arity_Hfrc_at_fm nat_simp_union
     by auto
   with assms
   have W: "arity(is_wfrec_fm(?\<phi>, 0, succ(x), succ(z))) = 2#+p \<union> (2#+l) \<union> (2#+x) \<union> (2#+z)"
     using arity_is_wfrec_fm[OF \<open>?\<phi>\<in>_\<close> _ _ _ _ \<open>arity(?\<phi>) = _\<close>] pred_Un_distrib pred_succ_eq
       nat_union_abs1
     by auto
   from assms
   have "arity(forcerel_fm(succ(p),succ(x),0)) = succ(succ(p)) \<union> succ(succ(x))"
     using arity_forcerel_fm nat_simp_union
     by auto
   with W assms
   show ?thesis
     unfolding frc_at_fm_def
     using arity_forcerel_fm pred_Un_distrib
     by auto
 qed
 
 lemma sats_frc_at_fm :
   assumes
     "p\<in>nat" "l\<in>nat" "i\<in>nat" "j\<in>nat" "env\<in>list(A)" "i < length(env)" "j < length(env)"
   shows
     "sats(A,frc_at_fm(p,l,i,j),env) \<longleftrightarrow>
      is_frc_at(##A,nth(p,env),nth(l,env),nth(i,env),nth(j,env))"
 proof -
   {
     fix r pp ll
     assume "r\<in>A"
     have 0:"is_Hfrc_at(##A,nth(p,env),nth(l,env),a2, a1, a0) \<longleftrightarrow>
          sats(A, Hfrc_at_fm(6#+p,6#+l,2,1,0), [a0,a1,a2,a3,a4,r]@env)"
       if "a0\<in>A" "a1\<in>A" "a2\<in>A" "a3\<in>A" "a4\<in>A" for a0 a1 a2 a3 a4
       using  that assms \<open>r\<in>A\<close>
         is_Hfrc_at_iff_sats[of "6#+p" "6#+l" 2 1 0 "[a0,a1,a2,a3,a4,r]@env" A]  by simp
     have "sats(A,is_wfrec_fm(Hfrc_at_fm(6 #+ p, 6 #+ l, 2, 1, 0), 0, succ(i), succ(j)),[r]@env) \<longleftrightarrow>
          is_wfrec(##A, is_Hfrc_at(##A, nth(p,env), nth(l,env)), r,nth(i, env), nth(j, env))"
       using assms \<open>r\<in>A\<close>
         sats_is_wfrec_fm[OF 0[simplified]]
       by simp
   }
   moreover
   have "sats(A, forcerel_fm(succ(p), succ(i), 0), Cons(r, env)) \<longleftrightarrow>
         is_forcerel(##A,nth(p,env),nth(i,env),r)" if "r\<in>A" for r
     using assms sats_forcerel_fm that by simp
   ultimately
   show ?thesis unfolding is_frc_at_def frc_at_fm_def
     using assms by simp
 qed
 
 definition
   forces_eq' :: "[i,i,i,i,i] \<Rightarrow> o" where
   "forces_eq'(P,l,p,t1,t2) \<equiv> frc_at(P,l,\<langle>0,t1,t2,p\<rangle>) = 1"
 
 definition
   forces_mem' :: "[i,i,i,i,i] \<Rightarrow> o" where
   "forces_mem'(P,l,p,t1,t2) \<equiv> frc_at(P,l,\<langle>1,t1,t2,p\<rangle>) = 1"
 
 definition
   forces_neq' :: "[i,i,i,i,i] \<Rightarrow> o" where
   "forces_neq'(P,l,p,t1,t2) \<equiv> \<not> (\<exists>q\<in>P. \<langle>q,p\<rangle>\<in>l \<and> forces_eq'(P,l,q,t1,t2))"
 
 definition
   forces_nmem' :: "[i,i,i,i,i] \<Rightarrow> o" where
   "forces_nmem'(P,l,p,t1,t2) \<equiv> \<not> (\<exists>q\<in>P. \<langle>q,p\<rangle>\<in>l \<and> forces_mem'(P,l,q,t1,t2))"
 
 definition
   is_forces_eq' :: "[i\<Rightarrow>o,i,i,i,i,i] \<Rightarrow> o" where
   "is_forces_eq'(M,P,l,p,t1,t2) \<equiv> \<exists>o[M]. \<exists>z[M]. \<exists>t[M]. number1(M,o) \<and> empty(M,z) \<and>
                                 is_tuple(M,z,t1,t2,p,t) \<and> is_frc_at(M,P,l,t,o)"
 
 definition
   is_forces_mem' :: "[i\<Rightarrow>o,i,i,i,i,i] \<Rightarrow> o" where
   "is_forces_mem'(M,P,l,p,t1,t2) \<equiv> \<exists>o[M]. \<exists>t[M]. number1(M,o) \<and>
                                 is_tuple(M,o,t1,t2,p,t) \<and> is_frc_at(M,P,l,t,o)"
 
 definition
   is_forces_neq' :: "[i\<Rightarrow>o,i,i,i,i,i] \<Rightarrow> o" where
   "is_forces_neq'(M,P,l,p,t1,t2) \<equiv>
       \<not> (\<exists>q[M]. q\<in>P \<and> (\<exists>qp[M]. pair(M,q,p,qp) \<and> qp\<in>l \<and> is_forces_eq'(M,P,l,q,t1,t2)))"
 
 definition
   is_forces_nmem' :: "[i\<Rightarrow>o,i,i,i,i,i] \<Rightarrow> o" where
   "is_forces_nmem'(M,P,l,p,t1,t2) \<equiv>
       \<not> (\<exists>q[M]. \<exists>qp[M]. q\<in>P \<and> pair(M,q,p,qp) \<and> qp\<in>l \<and> is_forces_mem'(M,P,l,q,t1,t2))"
 
 definition
   forces_eq_fm :: "[i,i,i,i,i] \<Rightarrow> i" where
   "forces_eq_fm(p,l,q,t1,t2) \<equiv>
      Exists(Exists(Exists(And(number1_fm(2),And(empty_fm(1),
               And(is_tuple_fm(1,t1#+3,t2#+3,q#+3,0),frc_at_fm(p#+3,l#+3,0,2) ))))))"
 
 definition
   forces_mem_fm :: "[i,i,i,i,i] \<Rightarrow> i" where
   "forces_mem_fm(p,l,q,t1,t2) \<equiv> Exists(Exists(And(number1_fm(1),
                           And(is_tuple_fm(1,t1#+2,t2#+2,q#+2,0),frc_at_fm(p#+2,l#+2,0,1)))))"
 
 definition
   forces_neq_fm :: "[i,i,i,i,i] \<Rightarrow> i" where
   "forces_neq_fm(p,l,q,t1,t2) \<equiv> Neg(Exists(Exists(And(Member(1,p#+2),
      And(pair_fm(1,q#+2,0),And(Member(0,l#+2),forces_eq_fm(p#+2,l#+2,1,t1#+2,t2#+2)))))))"
 
 definition
   forces_nmem_fm :: "[i,i,i,i,i] \<Rightarrow> i" where
   "forces_nmem_fm(p,l,q,t1,t2) \<equiv> Neg(Exists(Exists(And(Member(1,p#+2),
      And(pair_fm(1,q#+2,0),And(Member(0,l#+2),forces_mem_fm(p#+2,l#+2,1,t1#+2,t2#+2)))))))"
 
 
 lemma forces_eq_fm_type [TC]:
   "\<lbrakk> p\<in>nat;l\<in>nat;q\<in>nat;t1\<in>nat;t2\<in>nat\<rbrakk> \<Longrightarrow> forces_eq_fm(p,l,q,t1,t2) \<in> formula"
   unfolding forces_eq_fm_def
   by simp
 
 lemma forces_mem_fm_type [TC]:
   "\<lbrakk> p\<in>nat;l\<in>nat;q\<in>nat;t1\<in>nat;t2\<in>nat\<rbrakk> \<Longrightarrow> forces_mem_fm(p,l,q,t1,t2) \<in> formula"
   unfolding forces_mem_fm_def
   by simp
 
 lemma forces_neq_fm_type [TC]:
   "\<lbrakk> p\<in>nat;l\<in>nat;q\<in>nat;t1\<in>nat;t2\<in>nat\<rbrakk> \<Longrightarrow> forces_neq_fm(p,l,q,t1,t2) \<in> formula"
   unfolding forces_neq_fm_def
   by simp
 
 lemma forces_nmem_fm_type [TC]:
   "\<lbrakk> p\<in>nat;l\<in>nat;q\<in>nat;t1\<in>nat;t2\<in>nat\<rbrakk> \<Longrightarrow> forces_nmem_fm(p,l,q,t1,t2) \<in> formula"
   unfolding forces_nmem_fm_def
   by simp
 
 lemma arity_forces_eq_fm :
   "p\<in>nat \<Longrightarrow> l\<in>nat \<Longrightarrow> q\<in>nat \<Longrightarrow> t1 \<in> nat \<Longrightarrow> t2 \<in> nat \<Longrightarrow>
    arity(forces_eq_fm(p,l,q,t1,t2)) = succ(t1) \<union> succ(t2) \<union> succ(q) \<union> succ(p) \<union> succ(l)"
   unfolding forces_eq_fm_def
   using number1arity__fm arity_empty_fm arity_is_tuple_fm arity_frc_at_fm
     pred_Un_distrib
   by auto
 
 lemma arity_forces_mem_fm :
   "p\<in>nat \<Longrightarrow> l\<in>nat \<Longrightarrow> q\<in>nat \<Longrightarrow> t1 \<in> nat \<Longrightarrow> t2 \<in> nat \<Longrightarrow>
    arity(forces_mem_fm(p,l,q,t1,t2)) = succ(t1) \<union> succ(t2) \<union> succ(q) \<union> succ(p) \<union> succ(l)"
   unfolding forces_mem_fm_def
   using number1arity__fm arity_empty_fm arity_is_tuple_fm arity_frc_at_fm
     pred_Un_distrib
   by auto
 
 lemma sats_forces_eq'_fm:
   assumes  "p\<in>nat" "l\<in>nat" "q\<in>nat" "t1\<in>nat" "t2\<in>nat"  "env\<in>list(M)"
   shows "sats(M,forces_eq_fm(p,l,q,t1,t2),env) \<longleftrightarrow>
          is_forces_eq'(##M,nth(p,env),nth(l,env),nth(q,env),nth(t1,env),nth(t2,env))"
   unfolding forces_eq_fm_def is_forces_eq'_def using assms sats_is_tuple_fm  sats_frc_at_fm
   by simp
 
 lemma sats_forces_mem'_fm:
   assumes  "p\<in>nat" "l\<in>nat" "q\<in>nat" "t1\<in>nat" "t2\<in>nat"  "env\<in>list(M)"
   shows "sats(M,forces_mem_fm(p,l,q,t1,t2),env) \<longleftrightarrow>
              is_forces_mem'(##M,nth(p,env),nth(l,env),nth(q,env),nth(t1,env),nth(t2,env))"
   unfolding forces_mem_fm_def is_forces_mem'_def using assms sats_is_tuple_fm sats_frc_at_fm
   by simp
 
 lemma sats_forces_neq'_fm:
   assumes  "p\<in>nat" "l\<in>nat" "q\<in>nat" "t1\<in>nat" "t2\<in>nat"  "env\<in>list(M)"
   shows "sats(M,forces_neq_fm(p,l,q,t1,t2),env) \<longleftrightarrow>
              is_forces_neq'(##M,nth(p,env),nth(l,env),nth(q,env),nth(t1,env),nth(t2,env))"
   unfolding forces_neq_fm_def is_forces_neq'_def
   using assms sats_forces_eq'_fm sats_is_tuple_fm sats_frc_at_fm
   by simp
 
 lemma sats_forces_nmem'_fm:
   assumes  "p\<in>nat" "l\<in>nat" "q\<in>nat" "t1\<in>nat" "t2\<in>nat"  "env\<in>list(M)"
   shows "sats(M,forces_nmem_fm(p,l,q,t1,t2),env) \<longleftrightarrow>
              is_forces_nmem'(##M,nth(p,env),nth(l,env),nth(q,env),nth(t1,env),nth(t2,env))"
   unfolding forces_nmem_fm_def is_forces_nmem'_def
   using assms sats_forces_mem'_fm sats_is_tuple_fm sats_frc_at_fm
   by simp
 
 context forcing_data
 begin
 
 (* Absoluteness of components *)
 lemma fst_abs [simp]:
   "\<lbrakk>x\<in>M; y\<in>M \<rbrakk> \<Longrightarrow> is_fst(##M,x,y) \<longleftrightarrow> y = fst(x)"
   unfolding fst_def is_fst_def using pair_in_M_iff zero_in_M
   by (auto;rule_tac the_0 the_0[symmetric],auto)
 
 lemma snd_abs [simp]:
   "\<lbrakk>x\<in>M; y\<in>M \<rbrakk> \<Longrightarrow> is_snd(##M,x,y) \<longleftrightarrow> y = snd(x)"
   unfolding snd_def is_snd_def using pair_in_M_iff zero_in_M
   by (auto;rule_tac the_0 the_0[symmetric],auto)
 
 lemma ftype_abs[simp] :
   "\<lbrakk>x\<in>M; y\<in>M \<rbrakk> \<Longrightarrow> is_ftype(##M,x,y) \<longleftrightarrow> y = ftype(x)" unfolding ftype_def  is_ftype_def by simp
 
 lemma name1_abs[simp] :
   "\<lbrakk>x\<in>M; y\<in>M \<rbrakk> \<Longrightarrow> is_name1(##M,x,y) \<longleftrightarrow> y = name1(x)"
   unfolding name1_def is_name1_def
   by (rule hcomp_abs[OF fst_abs];simp_all add:fst_snd_closed)
 
 lemma snd_snd_abs:
   "\<lbrakk>x\<in>M; y\<in>M \<rbrakk> \<Longrightarrow> is_snd_snd(##M,x,y) \<longleftrightarrow> y = snd(snd(x))"
   unfolding is_snd_snd_def
   by (rule hcomp_abs[OF snd_abs];simp_all add:fst_snd_closed)
 
 lemma name2_abs[simp]:
   "\<lbrakk>x\<in>M; y\<in>M \<rbrakk> \<Longrightarrow> is_name2(##M,x,y) \<longleftrightarrow> y = name2(x)"
   unfolding name2_def is_name2_def
   by (rule hcomp_abs[OF fst_abs snd_snd_abs];simp_all add:fst_snd_closed)
 
 lemma cond_of_abs[simp]:
   "\<lbrakk>x\<in>M; y\<in>M \<rbrakk> \<Longrightarrow> is_cond_of(##M,x,y) \<longleftrightarrow> y = cond_of(x)"
   unfolding cond_of_def is_cond_of_def
   by (rule hcomp_abs[OF snd_abs snd_snd_abs];simp_all add:fst_snd_closed)
 
 lemma tuple_abs[simp]:
   "\<lbrakk>z\<in>M;t1\<in>M;t2\<in>M;p\<in>M;t\<in>M\<rbrakk> \<Longrightarrow>
    is_tuple(##M,z,t1,t2,p,t) \<longleftrightarrow> t = \<langle>z,t1,t2,p\<rangle>"
   unfolding is_tuple_def using tuples_in_M by simp
 
 lemma oneN_in_M[simp]: "1\<in>M"
   by (simp flip: setclass_iff)
 
 lemma twoN_in_M : "2\<in>M"
   by (simp flip: setclass_iff)
 
 lemma comp_in_M:
   "p \<preceq> q \<Longrightarrow> p\<in>M"
   "p \<preceq> q \<Longrightarrow> q\<in>M"
   using leq_in_M transitivity[of _ leq] pair_in_M_iff by auto
 
 (* Absoluteness of Hfrc *)
 
 lemma eq_case_abs [simp]:
   assumes
     "t1\<in>M" "t2\<in>M" "p\<in>M" "f\<in>M"
   shows
     "is_eq_case(##M,t1,t2,p,P,leq,f) \<longleftrightarrow> eq_case(t1,t2,p,P,leq,f)"
 proof -
   have "q \<preceq> p \<Longrightarrow> q\<in>M" for q
     using comp_in_M by simp
   moreover
   have "\<langle>s,y\<rangle>\<in>t \<Longrightarrow> s\<in>domain(t)" if "t\<in>M" for s y t
     using that unfolding domain_def by auto
   ultimately
   have
     "(\<forall>s\<in>M. s \<in> domain(t1) \<or> s \<in> domain(t2) \<longrightarrow> (\<forall>q\<in>M. q\<in>P \<and> q \<preceq> p \<longrightarrow>
                               (f ` \<langle>1, s, t1, q\<rangle> =1 \<longleftrightarrow> f ` \<langle>1, s, t2, q\<rangle>=1))) \<longleftrightarrow>
     (\<forall>s. s \<in> domain(t1) \<or> s \<in> domain(t2) \<longrightarrow> (\<forall>q. q\<in>P \<and> q \<preceq> p \<longrightarrow>
                                   (f ` \<langle>1, s, t1, q\<rangle> =1 \<longleftrightarrow> f ` \<langle>1, s, t2, q\<rangle>=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 n_in_M[of 1] domain_closed tuples_in_M
       apply_closed leq_in_M
     by simp
 qed
 
 lemma mem_case_abs [simp]:
   assumes
     "t1\<in>M" "t2\<in>M" "p\<in>M" "f\<in>M"
   shows
     "is_mem_case(##M,t1,t2,p,P,leq,f) \<longleftrightarrow> mem_case(t1,t2,p,P,leq,f)"
 proof
   {
     fix v
     assume "v\<in>P" "v \<preceq> p" "is_mem_case(##M,t1,t2,p,P,leq,f)"
     moreover
     from this
     have "v\<in>M" "\<langle>v,p\<rangle> \<in> 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 \<in> P \<and> q \<in> P \<and> \<langle>q, v\<rangle> \<in> M \<and> \<langle>s, r\<rangle> \<in> M \<and> \<langle>q, r\<rangle> \<in> M \<and> 0 \<in> M \<and>
        \<langle>0, t1, s, q\<rangle> \<in> M \<and> q \<preceq> v \<and> \<langle>s, r\<rangle> \<in> t2 \<and> q \<preceq> r \<and> f ` \<langle>0, t1, s, q\<rangle> = 1"
       unfolding is_mem_case_def by auto
     then
     have "\<exists>q s r. r \<in> P \<and> q \<in> P \<and> q \<preceq> v \<and> \<langle>s, r\<rangle> \<in> t2 \<and> q \<preceq> r \<and> f ` \<langle>0, t1, s, q\<rangle> = 1"
       by auto
   }
   then
   show "mem_case(t1, t2, p, P, leq, f)" if "is_mem_case(##M, t1, t2, p, P, leq, f)"
     unfolding mem_case_def using that assms by auto
 next
   { fix v
     assume "v \<in> M" "v \<in> P" "\<langle>v, p\<rangle> \<in> M" "v \<preceq> p" "mem_case(t1, t2, p, P, leq, f)"
     moreover
     from this
     obtain q s r where "r \<in> P \<and> q \<in> P \<and> q \<preceq> v \<and> \<langle>s, r\<rangle> \<in> t2 \<and> q \<preceq> r \<and> f ` \<langle>0, t1, s, q\<rangle> = 1"
       unfolding mem_case_def by auto
     moreover
     from this \<open>t2\<in>M\<close>
     have "r\<in>M" "q\<in>M" "s\<in>M" "r \<in> P \<and> q \<in> P \<and> q \<preceq> v \<and> \<langle>s, r\<rangle> \<in> t2 \<and> q \<preceq> r \<and> f ` \<langle>0, t1, s, q\<rangle> = 1"
       using transitivity P_in_M domain_closed[of t2] by auto
     moreover
     note \<open>t1\<in>M\<close>
     ultimately
     have "\<exists>q\<in>M . \<exists>s\<in>M. \<exists>r\<in>M.
          r \<in> P \<and> q \<in> P \<and> \<langle>q, v\<rangle> \<in> M \<and> \<langle>s, r\<rangle> \<in> M \<and> \<langle>q, r\<rangle> \<in> M \<and> 0 \<in> M \<and>
          \<langle>0, t1, s, q\<rangle> \<in> M \<and> q \<preceq> v \<and> \<langle>s, r\<rangle> \<in> t2 \<and> q \<preceq> r \<and> f ` \<langle>0, t1, s, q\<rangle> = 1"
       using tuples_in_M zero_in_M by auto
   }
   then
   show "is_mem_case(##M, t1, t2, p, P, leq, f)" if "mem_case(t1, t2, p, P, leq, f)"
     unfolding is_mem_case_def using assms that by auto
 qed
 
 
 lemma Hfrc_abs:
   "\<lbrakk>fnnc\<in>M; f\<in>M\<rbrakk> \<Longrightarrow>
    is_Hfrc(##M,P,leq,fnnc,f) \<longleftrightarrow> Hfrc(P,leq,fnnc,f)"
   unfolding is_Hfrc_def Hfrc_def using pair_in_M_iff
   by auto
 
 lemma Hfrc_at_abs:
   "\<lbrakk>fnnc\<in>M; f\<in>M ; z\<in>M\<rbrakk> \<Longrightarrow>
    is_Hfrc_at(##M,P,leq,fnnc,f,z) \<longleftrightarrow>  z = bool_of_o(Hfrc(P,leq,fnnc,f)) "
   unfolding is_Hfrc_at_def using Hfrc_abs
   by auto
 
 lemma components_closed :
   "x\<in>M \<Longrightarrow> ftype(x)\<in>M"
   "x\<in>M \<Longrightarrow> name1(x)\<in>M"
   "x\<in>M \<Longrightarrow> name2(x)\<in>M"
   "x\<in>M \<Longrightarrow> cond_of(x)\<in>M"
   unfolding ftype_def name1_def name2_def cond_of_def using fst_snd_closed by simp_all
 
 lemma ecloseN_closed:
   "(##M)(A) \<Longrightarrow> (##M)(ecloseN(A))"
   "(##M)(A) \<Longrightarrow> (##M)(eclose_n(name1,A))"
   "(##M)(A) \<Longrightarrow> (##M)(eclose_n(name2,A))"
   unfolding ecloseN_def eclose_n_def
   using components_closed eclose_closed singletonM Un_closed by auto
 
 lemma is_eclose_n_abs :
   assumes "x\<in>M" "ec\<in>M"
   shows "is_eclose_n(##M,is_name1,ec,x) \<longleftrightarrow> ec = eclose_n(name1,x)"
     "is_eclose_n(##M,is_name2,ec,x) \<longleftrightarrow> ec = eclose_n(name2,x)"
   unfolding is_eclose_n_def eclose_n_def
   using assms name1_abs name2_abs eclose_abs singletonM components_closed
   by auto
 
 
 lemma is_ecloseN_abs :
   "\<lbrakk>x\<in>M;ec\<in>M\<rbrakk> \<Longrightarrow> is_ecloseN(##M,ec,x) \<longleftrightarrow> ec = ecloseN(x)"
   unfolding is_ecloseN_def ecloseN_def
   using is_eclose_n_abs Un_closed union_abs ecloseN_closed
   by auto
 
 lemma frecR_abs :
   "x\<in>M \<Longrightarrow> y\<in>M \<Longrightarrow> frecR(x,y) \<longleftrightarrow> is_frecR(##M,x,y)"
   unfolding frecR_def is_frecR_def using components_closed domain_closed by simp
 
 lemma frecrelP_abs :
   "z\<in>M \<Longrightarrow> frecrelP(##M,z) \<longleftrightarrow> (\<exists>x y. z = \<langle>x,y\<rangle> \<and> frecR(x,y))"
   using pair_in_M_iff frecR_abs unfolding frecrelP_def by auto
 
 lemma frecrel_abs:
   assumes
     "A\<in>M" "r\<in>M"
   shows
     "is_frecrel(##M,A,r) \<longleftrightarrow>  r = frecrel(A)"
 proof -
   from \<open>A\<in>M\<close>
   have "z\<in>M" if "z\<in>A\<times>A" for z
     using cartprod_closed transitivity that by simp
   then
   have "Collect(A\<times>A,frecrelP(##M)) = Collect(A\<times>A,\<lambda>z. (\<exists>x y. z = \<langle>x,y\<rangle> \<and> frecR(x,y)))"
     using Collect_cong[of "A\<times>A" "A\<times>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
     "x\<in>M"
   shows
     "frecrel(x)\<in>M"
 proof -
   have "Collect(x\<times>x,\<lambda>z. (\<exists>x y. z = \<langle>x,y\<rangle> \<and> frecR(x,y)))\<in>M"
     using Collect_in_M_0p[of "frecrelP_fm(0)"] arity_frecrelP_fm sats_frecrelP_fm
       frecrelP_abs \<open>x\<in>M\<close> cartprod_closed by simp
   then show ?thesis
     unfolding frecrel_def Rrel_def frecrelP_def by simp
 qed
 
 lemma field_frecrel : "field(frecrel(names_below(P,x))) \<subseteq> names_below(P,x)"
   unfolding frecrel_def
   using field_Rrel by simp
 
 lemma forcerelD : "uv \<in> forcerel(P,x) \<Longrightarrow> uv\<in> names_below(P,x) \<times> names_below(P,x)"
   unfolding forcerel_def
   using trancl_type field_frecrel by blast
 
 lemma wf_forcerel :
   "wf(forcerel(P,x))"
   unfolding forcerel_def using wf_trancl wf_frecrel .
 
 lemma restrict_trancl_forcerel:
   assumes "frecR(w,y)"
   shows "restrict(f,frecrel(names_below(P,x))-``{y})`w
        = restrict(f,forcerel(P,x)-``{y})`w"
   unfolding forcerel_def frecrel_def using assms restrict_trancl_Rrel[of frecR]
   by simp
 
 lemma names_belowI :
   assumes "frecR(\<langle>ft,n1,n2,p\<rangle>,\<langle>a,b,c,d\<rangle>)" "p\<in>P"
   shows "\<langle>ft,n1,n2,p\<rangle> \<in> names_below(P,\<langle>a,b,c,d\<rangle>)" (is "?x \<in> names_below(_,?y)")
 proof -
   from assms
   have "ft \<in> 2" "a \<in> 2"
     unfolding frecR_def by (auto simp add:components_simp)
   from assms
   consider (e) "n1 \<in> domain(b) \<union> domain(c) \<and> (n2 = b \<or> n2 =c)"
     | (m) "n1 = b \<and> n2 \<in> domain(c)"
     unfolding frecR_def by (auto simp add:components_simp)
   then show ?thesis
   proof cases
     case e
     then
     have "n1 \<in> eclose(b) \<or> n1 \<in> eclose(c)"
       using Un_iff in_dom_in_eclose by auto
     with e
     have "n1 \<in> ecloseN(?y)" "n2 \<in> ecloseN(?y)"
       using ecloseNI components_in_eclose by auto
     with \<open>ft\<in>2\<close> \<open>p\<in>P\<close>
     show ?thesis unfolding names_below_def by  auto
   next
     case m
     then
     have "n1 \<in> ecloseN(?y)" "n2 \<in> ecloseN(?y)"
       using mem_eclose_trans  ecloseNI
         in_dom_in_eclose components_in_eclose by auto
     with \<open>ft\<in>2\<close> \<open>p\<in>P\<close>
     show ?thesis unfolding names_below_def
       by auto
   qed
 qed
 
 lemma names_below_tr :
   assumes "x\<in> names_below(P,y)"
     "y\<in> names_below(P,z)"
   shows "x\<in> names_below(P,z)"
 proof -
   let ?A="\<lambda>y . names_below(P,y)"
   from assms
   obtain fx x1 x2 px where
     "x = \<langle>fx,x1,x2,px\<rangle>" "fx\<in>2" "x1\<in>ecloseN(y)" "x2\<in>ecloseN(y)" "px\<in>P"
     unfolding names_below_def by auto
   from assms
   obtain fy y1 y2 py where
     "y = \<langle>fy,y1,y2,py\<rangle>" "fy\<in>2" "y1\<in>ecloseN(z)" "y2\<in>ecloseN(z)" "py\<in>P"
     unfolding names_below_def by auto
   from \<open>x1\<in>_\<close> \<open>x2\<in>_\<close> \<open>y1\<in>_\<close> \<open>y2\<in>_\<close> \<open>x=_\<close> \<open>y=_\<close>
   have "x1\<in>ecloseN(z)" "x2\<in>ecloseN(z)"
     using ecloseN_mono names_simp by auto
   with \<open>fx\<in>2\<close> \<open>px\<in>P\<close> \<open>x=_\<close>
   have "x\<in>?A(z)"
     unfolding names_below_def by simp
   then show ?thesis using subsetI by simp
 qed
 
 lemma arg_into_names_below2 :
   assumes "\<langle>x,y\<rangle> \<in> frecrel(names_below(P,z))"
   shows  "x \<in> names_below(P,y)"
 proof -
   {
     from assms
     have "x\<in>names_below(P,z)" "y\<in>names_below(P,z)" "frecR(x,y)"
       unfolding frecrel_def Rrel_def
       by auto
     obtain f n1 n2 p where
       "x = \<langle>f,n1,n2,p\<rangle>" "f\<in>2" "n1\<in>ecloseN(z)" "n2\<in>ecloseN(z)" "p\<in>P"
       using \<open>x\<in>names_below(P,z)\<close>
       unfolding names_below_def by auto
     moreover
     obtain fy m1 m2 q where
       "q\<in>P" "y = \<langle>fy,m1,m2,q\<rangle>"
       using \<open>y\<in>names_below(P,z)\<close>
       unfolding names_below_def by auto
     moreover
     note \<open>frecR(x,y)\<close>
     ultimately
     have "x\<in>names_below(P,y)" using names_belowI by simp
   }
   then show ?thesis .
 qed
 
 lemma arg_into_names_below :
   assumes "\<langle>x,y\<rangle> \<in> frecrel(names_below(P,z))"
   shows  "x \<in> names_below(P,x)"
 proof -
   {
     from assms
     have "x\<in>names_below(P,z)"
       unfolding frecrel_def Rrel_def
       by auto
     from \<open>x\<in>names_below(P,z)\<close>
     obtain f n1 n2 p where
       "x = \<langle>f,n1,n2,p\<rangle>" "f\<in>2" "n1\<in>ecloseN(z)" "n2\<in>ecloseN(z)" "p\<in>P"
       unfolding names_below_def by auto
     then
     have "n1\<in>ecloseN(x)" "n2\<in>ecloseN(x)"
       using components_in_eclose by simp_all
     with \<open>f\<in>2\<close> \<open>p\<in>P\<close> \<open>x = \<langle>f,n1,n2,p\<rangle>\<close>
     have "x\<in>names_below(P,x)"
       unfolding names_below_def by simp
   }
   then show ?thesis .
 qed
 
 lemma forcerel_arg_into_names_below :
   assumes "\<langle>x,y\<rangle> \<in> forcerel(P,z)"
   shows  "x \<in> names_below(P,x)"
   using assms
   unfolding forcerel_def
   by(rule trancl_induct;auto simp add: arg_into_names_below)
 
 lemma names_below_mono :
   assumes "\<langle>x,y\<rangle> \<in> frecrel(names_below(P,z))"
   shows "names_below(P,x) \<subseteq> names_below(P,y)"
 proof -
   from assms
   have "x\<in>names_below(P,y)"
     using arg_into_names_below2 by simp
   then
   show ?thesis
     using names_below_tr subsetI by simp
 qed
 
 lemma frecrel_mono :
   assumes "\<langle>x,y\<rangle> \<in> frecrel(names_below(P,z))"
   shows "frecrel(names_below(P,x)) \<subseteq> frecrel(names_below(P,y))"
   unfolding frecrel_def
   using Rrel_mono names_below_mono assms by simp
 
 lemma forcerel_mono2 :
   assumes "\<langle>x,y\<rangle> \<in> frecrel(names_below(P,z))"
   shows "forcerel(P,x) \<subseteq> forcerel(P,y)"
   unfolding forcerel_def
   using trancl_mono frecrel_mono assms by simp
 
 lemma forcerel_mono_aux :
   assumes "\<langle>x,y\<rangle> \<in> frecrel(names_below(P, w))^+"
   shows "forcerel(P,x) \<subseteq> forcerel(P,y)"
   using assms
   by (rule trancl_induct,simp_all add: subset_trans forcerel_mono2)
 
 lemma forcerel_mono :
   assumes "\<langle>x,y\<rangle> \<in> forcerel(P,z)"
   shows "forcerel(P,x) \<subseteq> forcerel(P,y)"
   using forcerel_mono_aux assms unfolding forcerel_def by simp
 
 lemma aux: "x \<in> names_below(P, w) \<Longrightarrow> \<langle>x,y\<rangle> \<in> forcerel(P,z) \<Longrightarrow>
   (y \<in> names_below(P, w) \<longrightarrow> \<langle>x,y\<rangle> \<in> forcerel(P,w))"
   unfolding forcerel_def
 proof(rule_tac a=x and b=y and P="\<lambda> y . y \<in> names_below(P, w) \<longrightarrow> \<langle>x,y\<rangle> \<in> frecrel(names_below(P,w))^+" in trancl_induct,simp)
   let ?A="\<lambda> a . names_below(P, a)"
   let ?R="\<lambda> a . frecrel(?A(a))"
   let ?fR="\<lambda> a .forcerel(a)"
   show "u\<in>?A(w) \<longrightarrow> \<langle>x,u\<rangle>\<in>?R(w)^+" if "x\<in>?A(w)" "\<langle>x,y\<rangle>\<in>?R(z)^+" "\<langle>x,u\<rangle>\<in>?R(z)"  for  u
     using that frecrelD frecrelI r_into_trancl unfolding names_below_def by simp
   {
     fix u v
     assume "x \<in> ?A(w)"
       "\<langle>x, y\<rangle> \<in> ?R(z)^+"
       "\<langle>x, u\<rangle> \<in> ?R(z)^+"
       "\<langle>u, v\<rangle> \<in> ?R(z)"
       "u \<in> ?A(w) \<Longrightarrow> \<langle>x, u\<rangle> \<in> ?R(w)^+"
     then
     have "v \<in> ?A(w) \<Longrightarrow> \<langle>x, v\<rangle> \<in> ?R(w)^+"
     proof -
       assume "v \<in>?A(w)"
       from \<open>\<langle>u,v\<rangle>\<in>_\<close>
       have "u\<in>?A(v)"
         using arg_into_names_below2 by simp
       with \<open>v \<in>?A(w)\<close>
       have "u\<in>?A(w)"
         using names_below_tr by simp
       with \<open>v\<in>_\<close> \<open>\<langle>u,v\<rangle>\<in>_\<close>
       have "\<langle>u,v\<rangle>\<in> ?R(w)"
         using frecrelD frecrelI r_into_trancl unfolding names_below_def by simp
       with \<open>u \<in> ?A(w) \<Longrightarrow> \<langle>x, u\<rangle> \<in> ?R(w)^+\<close> \<open>u\<in>?A(w)\<close>
       have "\<langle>x, u\<rangle> \<in> ?R(w)^+" by simp
       with \<open>\<langle>u,v\<rangle>\<in> ?R(w)\<close>
       show "\<langle>x,v\<rangle>\<in> ?R(w)^+" using trancl_trans r_into_trancl
         by simp
     qed
   }
   then show "v \<in> ?A(w) \<longrightarrow> \<langle>x, v\<rangle> \<in> ?R(w)^+"
     if "x \<in> ?A(w)"
       "\<langle>x, y\<rangle> \<in> ?R(z)^+"
       "\<langle>x, u\<rangle> \<in> ?R(z)^+"
       "\<langle>u, v\<rangle> \<in> ?R(z)"
       "u \<in> ?A(w) \<longrightarrow> \<langle>x, u\<rangle> \<in> ?R(w)^+" for u v
     using that by simp
 qed
 
 lemma forcerel_eq :
   assumes "\<langle>z,x\<rangle> \<in> forcerel(P,x)"
   shows "forcerel(P,z) = forcerel(P,x) \<inter> names_below(P,z)\<times>names_below(P,z)"
   using assms aux forcerelD forcerel_mono[of z x x] subsetI
   by auto
 
 lemma forcerel_below_aux :
   assumes "\<langle>z,x\<rangle> \<in> forcerel(P,x)" "\<langle>u,z\<rangle> \<in> forcerel(P,x)"
   shows "u \<in> names_below(P,z)"
   using assms(2)
   unfolding forcerel_def
 proof(rule trancl_induct)
   show  "u \<in> names_below(P,y)" if " \<langle>u, y\<rangle> \<in> frecrel(names_below(P, x))" for y
     using that vimage_singleton_iff arg_into_names_below2 by simp
 next
   show "u \<in> names_below(P,z)"
     if "\<langle>u, y\<rangle> \<in> frecrel(names_below(P, x))^+"
       "\<langle>y, z\<rangle> \<in> frecrel(names_below(P, x))"
       "u \<in> names_below(P, y)"
     for y z
     using that arg_into_names_below2[of y z x] names_below_tr by simp
 qed
 
 lemma forcerel_below :
   assumes "\<langle>z,x\<rangle> \<in> forcerel(P,x)"
   shows "forcerel(P,x) -`` {z} \<subseteq> names_below(P,z)"
   using vimage_singleton_iff assms forcerel_below_aux by auto
 
 lemma relation_forcerel :
   shows "relation(forcerel(P,z))" "trans(forcerel(P,z))"
   unfolding forcerel_def using relation_trancl trans_trancl by simp_all
 
 lemma Hfrc_restrict_trancl: "bool_of_o(Hfrc(P, leq, y, restrict(f,frecrel(names_below(P,x))-``{y})))
          = bool_of_o(Hfrc(P, leq, y, restrict(f,(frecrel(names_below(P,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(P,leq,z) = wfrec(forcerel(P,z),z,\<lambda>x f. bool_of_o(Hfrc(P,leq,x,f)))"
   unfolding frc_at_def forcerel_def using wf_eq_trancl Hfrc_restrict_trancl by simp
 
 
 lemma forcerelI1 :
   assumes "n1 \<in> domain(b) \<or> n1 \<in> domain(c)" "p\<in>P" "d\<in>P"
   shows "\<langle>\<langle>1, n1, b, p\<rangle>, \<langle>0,b,c,d\<rangle>\<rangle>\<in> forcerel(P,\<langle>0,b,c,d\<rangle>)"
 proof -
   let ?x="\<langle>1, n1, b, p\<rangle>"
   let ?y="\<langle>0,b,c,d\<rangle>"
   from assms
   have "frecR(?x,?y)"
     using frecRI1 by simp
   then
   have "?x\<in>names_below(P,?y)"  "?y \<in> names_below(P,?y)"
     using names_belowI  assms components_in_eclose
     unfolding names_below_def by auto
   with \<open>frecR(?x,?y)\<close>
   show ?thesis
     unfolding forcerel_def frecrel_def
     using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
     by auto
 qed
 
 lemma forcerelI2 :
   assumes "n1 \<in> domain(b) \<or> n1 \<in> domain(c)" "p\<in>P" "d\<in>P"
   shows "\<langle>\<langle>1, n1, c, p\<rangle>, \<langle>0,b,c,d\<rangle>\<rangle>\<in> forcerel(P,\<langle>0,b,c,d\<rangle>)"
 proof -
   let ?x="\<langle>1, n1, c, p\<rangle>"
   let ?y="\<langle>0,b,c,d\<rangle>"
   from assms
   have "frecR(?x,?y)"
     using frecRI2 by simp
   then
   have "?x\<in>names_below(P,?y)"  "?y \<in> names_below(P,?y)"
     using names_belowI  assms components_in_eclose
     unfolding names_below_def by auto
   with \<open>frecR(?x,?y)\<close>
   show ?thesis
     unfolding forcerel_def frecrel_def
     using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
     by auto
 qed
 
 lemma forcerelI3 :
   assumes "\<langle>n2, r\<rangle> \<in> c" "p\<in>P" "d\<in>P" "r \<in> P"
   shows "\<langle>\<langle>0, b, n2, p\<rangle>,\<langle>1, b, c, d\<rangle>\<rangle> \<in> forcerel(P,\<langle>1,b,c,d\<rangle>)"
 proof -
   let ?x="\<langle>0, b, n2, p\<rangle>"
   let ?y="\<langle>1, b, c, d\<rangle>"
   from assms
   have "frecR(?x,?y)"
     using assms frecRI3 by simp
   then
   have "?x\<in>names_below(P,?y)"  "?y \<in> names_below(P,?y)"
     using names_belowI  assms components_in_eclose
     unfolding names_below_def by auto
   with \<open>frecR(?x,?y)\<close>
   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 \<in> forcerel(P,x) -`` {x}"
   shows "wfrec(forcerel(P,x), z, H) =  wfrec(forcerel(P,z), z, H)"
 proof -
   let ?A="names_below(P,z)"
   from assms
   have "\<langle>z,x\<rangle> \<in> forcerel(P,x)"
     using vimage_singleton_iff by simp
   then
   have "z \<in> ?A"
     using forcerel_arg_into_names_below by simp
   from \<open>\<langle>z,x\<rangle> \<in> forcerel(P,x)\<close>
   have E:"forcerel(P,z) = forcerel(P,x) \<inter> (?A\<times>?A)"
     "forcerel(P,x) -`` {z} \<subseteq> ?A"
     using forcerel_eq forcerel_below
     by auto
   with \<open>z\<in>?A\<close>
   have "wfrec(forcerel(P,x), z, H) = wfrec[?A](forcerel(P,x), z, H)"
     using wfrec_trans_restr[OF relation_forcerel(1) wf_forcerel relation_forcerel(2), of x z ?A]
     by simp
   then show ?thesis
     using E wfrec_restr_eq by simp
 qed
 
 subsection\<open>Recursive expression of \<^term>\<open>frc_at\<close>\<close>
 
 lemma def_frc_at :
   assumes "p\<in>P"
   shows
     "frc_at(P,leq,\<langle>ft,n1,n2,p\<rangle>) =
    bool_of_o( p \<in>P \<and>
   (  ft = 0 \<and>  (\<forall>s. s\<in>domain(n1) \<union> domain(n2) \<longrightarrow>
         (\<forall>q. q\<in>P \<and> q \<preceq> p \<longrightarrow> (frc_at(P,leq,\<langle>1,s,n1,q\<rangle>) =1 \<longleftrightarrow> frc_at(P,leq,\<langle>1,s,n2,q\<rangle>) =1)))
    \<or> ft = 1 \<and> ( \<forall>v\<in>P. v \<preceq> p \<longrightarrow>
     (\<exists>q. \<exists>s. \<exists>r. r\<in>P \<and> q\<in>P \<and> q \<preceq> v \<and> \<langle>s,r\<rangle> \<in> n2 \<and> q \<preceq> r \<and>  frc_at(P,leq,\<langle>0,n1,s,q\<rangle>) = 1))))"
 proof -
   let ?r="\<lambda>y. forcerel(P,y)" and ?Hf="\<lambda>x f. bool_of_o(Hfrc(P,leq,x,f))"
   let ?t="\<lambda>y. ?r(y) -`` {y}"
   let ?arg="\<langle>ft,n1,n2,p\<rangle>"
   from wf_forcerel
   have wfr: "\<forall>w . wf(?r(w))" ..
   with wfrec [of "?r(?arg)" ?arg ?Hf]
   have "frc_at(P,leq,?arg) = ?Hf( ?arg, \<lambda>x\<in>?r(?arg) -`` {?arg}. wfrec(?r(?arg), x, ?Hf))"
     using frc_at_trancl by simp
   also
   have " ... = ?Hf( ?arg, \<lambda>x\<in>?r(?arg) -`` {?arg}. frc_at(P,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
 
 
 subsection\<open>Absoluteness of \<^term>\<open>frc_at\<close>\<close>
 
 lemma trans_forcerel_t : "trans(forcerel(P,x))"
   unfolding forcerel_def using trans_trancl .
 
 lemma relation_forcerel_t : "relation(forcerel(P,x))"
   unfolding forcerel_def using relation_trancl .
 
 
 lemma forcerel_in_M :
   assumes
     "x\<in>M"
   shows
     "forcerel(P,x)\<in>M"
   unfolding forcerel_def def_frecrel names_below_def
 proof -
   let ?Q = "2 \<times> ecloseN(x) \<times> ecloseN(x) \<times> P"
   have "?Q \<times> ?Q \<in> M"
     using \<open>x\<in>M\<close> P_in_M twoN_in_M ecloseN_closed cartprod_closed by simp
   moreover
   have "separation(##M,\<lambda>z. \<exists>x y. z = \<langle>x, y\<rangle> \<and> frecR(x, y))"
   proof -
     have "arity(frecrelP_fm(0)) = 1"
       unfolding number1_fm_def frecrelP_fm_def
       by (simp del:FOL_sats_iff pair_abs empty_abs
           add: fm_defs frecR_fm_def number1_fm_def components_defs nat_simp_union)
     then
     have "separation(##M, \<lambda>z. sats(M,frecrelP_fm(0) , [z]))"
       using separation_ax by simp
     moreover
     have "frecrelP(##M,z) \<longleftrightarrow> sats(M,frecrelP_fm(0),[z])"
       if "z\<in>M" for z
       using that sats_frecrelP_fm[of 0 "[z]"] by simp
     ultimately
     have "separation(##M,frecrelP(##M))"
       unfolding separation_def by simp
     then
     show ?thesis using frecrelP_abs
         separation_cong[of "##M" "frecrelP(##M)" "\<lambda>z. \<exists>x y. z = \<langle>x, y\<rangle> \<and> frecR(x, y)"]
       by simp
   qed
   ultimately
   show "{z \<in> ?Q \<times> ?Q . \<exists>x y. z = \<langle>x, y\<rangle> \<and> frecR(x, y)}^+ \<in> M"
     using separation_closed frecrelP_abs trancl_closed by simp
 qed
 
 lemma relation2_Hfrc_at_abs:
   "relation2(##M,is_Hfrc_at(##M,P,leq),\<lambda>x f. bool_of_o(Hfrc(P,leq,x,f)))"
   unfolding relation2_def using Hfrc_at_abs
   by simp
 
 lemma Hfrc_at_closed :
   "\<forall>x\<in>M. \<forall>g\<in>M. function(g) \<longrightarrow> bool_of_o(Hfrc(P,leq,x,g))\<in>M"
   unfolding bool_of_o_def using zero_in_M n_in_M[of 1] by simp
 
 lemma wfrec_Hfrc_at :
   assumes
     "X\<in>M"
   shows
     "wfrec_replacement(##M,is_Hfrc_at(##M,P,leq),forcerel(P,X))"
 proof -
   have 0:"is_Hfrc_at(##M,P,leq,a,b,c) \<longleftrightarrow>
         sats(M,Hfrc_at_fm(8,9,2,1,0),[c,b,a,d,e,y,x,z,P,leq,forcerel(P,X)])"
     if "a\<in>M" "b\<in>M" "c\<in>M" "d\<in>M" "e\<in>M" "y\<in>M" "x\<in>M" "z\<in>M"
     for a b c d e y x z
     using that P_in_M leq_in_M \<open>X\<in>M\<close> forcerel_in_M
       is_Hfrc_at_iff_sats[of concl:M P leq a b c 8 9 2 1 0
         "[c,b,a,d,e,y,x,z,P,leq,forcerel(P,X)]"] by simp
   have 1:"sats(M,is_wfrec_fm(Hfrc_at_fm(8,9,2,1,0),5,1,0),[y,x,z,P,leq,forcerel(P,X)]) \<longleftrightarrow>
                    is_wfrec(##M, is_Hfrc_at(##M,P,leq),forcerel(P,X), x, y)"
     if "x\<in>M" "y\<in>M" "z\<in>M" for x y z
     using  that \<open>X\<in>M\<close> forcerel_in_M P_in_M leq_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,P,leq,forcerel(P,X)]) \<longleftrightarrow>
               (\<exists>y\<in>M. pair(##M,x,y,z) & is_wfrec(##M, is_Hfrc_at(##M,P,leq),forcerel(P,X), x, y))"
     if "x\<in>M" "z\<in>M" for x z
     using that 1 \<open>X\<in>M\<close> forcerel_in_M P_in_M leq_in_M by (simp del:pair_abs)
   have artyf:"arity(?f) = 5"
     unfolding is_wfrec_fm_def Hfrc_at_fm_def Hfrc_fm_def Replace_fm_def PHcheck_fm_def
       pair_fm_def upair_fm_def is_recfun_fm_def fun_apply_fm_def big_union_fm_def
       pre_image_fm_def restriction_fm_def image_fm_def fm_defs number1_fm_def
       eq_case_fm_def mem_case_fm_def is_tuple_fm_def
     by (simp add:nat_simp_union)
   moreover
   have "?f\<in>formula"
     unfolding fm_defs Hfrc_at_fm_def by simp
   ultimately
   have "strong_replacement(##M,\<lambda>x z. sats(M,?f,[x,z,P,leq,forcerel(P,X)]))"
     using replacement_ax 1 artyf \<open>X\<in>M\<close> forcerel_in_M P_in_M leq_in_M by simp
   then
   have "strong_replacement(##M,\<lambda>x z.
           \<exists>y\<in>M. pair(##M,x,y,z) & is_wfrec(##M, is_Hfrc_at(##M,P,leq),forcerel(P,X), x, y))"
     using repl_sats[of M ?f "[P,leq,forcerel(P,X)]"] satsf by (simp del:pair_abs)
   then
   show ?thesis unfolding wfrec_replacement_def by simp
 qed
 
 lemma names_below_abs :
   "\<lbrakk>Q\<in>M;x\<in>M;nb\<in>M\<rbrakk> \<Longrightarrow> is_names_below(##M,Q,x,nb) \<longleftrightarrow> nb = names_below(Q,x)"
   unfolding is_names_below_def names_below_def
   using succ_in_M_iff zero_in_M cartprod_closed is_ecloseN_abs ecloseN_closed
   by auto
 
 lemma names_below_closed:
   "\<lbrakk>Q\<in>M;x\<in>M\<rbrakk> \<Longrightarrow> names_below(Q,x) \<in> 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 \<in> M" "x \<in> M"
     "\<And>A1 A2 A3 A4. A1 \<in> M \<Longrightarrow> A2 \<in> M \<Longrightarrow> A3 \<in> M \<Longrightarrow> A4 \<in> M \<Longrightarrow> R(A1 \<times> A2 \<times> A3 \<times> A4)"
   shows "R(names_below(Q,x))"
   unfolding names_below_def using assms zero_in_M ecloseN_closed[of x] twoN_in_M by auto
 
 lemma forcerel_abs :
   "\<lbrakk>x\<in>M;z\<in>M\<rbrakk> \<Longrightarrow> is_forcerel(##M,P,x,z) \<longleftrightarrow> z = forcerel(P,x)"
   unfolding is_forcerel_def forcerel_def
   using frecrel_abs names_below_abs trancl_abs P_in_M twoN_in_M ecloseN_closed names_below_closed
     names_below_productE[of concl:"\<lambda>p. is_frecrel(##M,p,_) \<longleftrightarrow>  _ = frecrel(p)"] frecrel_closed
   by simp
 
 lemma frc_at_abs:
   assumes "fnnc\<in>M" "z\<in>M"
   shows "is_frc_at(##M,P,leq,fnnc,z) \<longleftrightarrow> z = frc_at(P,leq,fnnc)"
 proof -
   from assms
   have "(\<exists>r\<in>M. is_forcerel(##M,P,fnnc, r) \<and> is_wfrec(##M, is_Hfrc_at(##M, P, leq), r, fnnc, z))
         \<longleftrightarrow> is_wfrec(##M, is_Hfrc_at(##M, P, leq), forcerel(P,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 trans_forcerel_t relation_forcerel_t forcerel_in_M
       Hfrc_at_closed relation2_Hfrc_at_abs
       trans_wfrec_abs[of "forcerel(P,fnnc)" fnnc z "is_Hfrc_at(##M,P,leq)" "\<lambda>x f. bool_of_o(Hfrc(P,leq,x,f))"]
     by (simp flip:setclass_iff)
 qed
 
 lemma forces_eq'_abs :
   "\<lbrakk>p\<in>M ; t1\<in>M ; t2\<in>M\<rbrakk> \<Longrightarrow> is_forces_eq'(##M,P,leq,p,t1,t2) \<longleftrightarrow> forces_eq'(P,leq,p,t1,t2)"
   unfolding is_forces_eq'_def forces_eq'_def
   using frc_at_abs zero_in_M tuples_in_M by auto
 
 lemma forces_mem'_abs :
   "\<lbrakk>p\<in>M ; t1\<in>M ; t2\<in>M\<rbrakk> \<Longrightarrow> is_forces_mem'(##M,P,leq,p,t1,t2) \<longleftrightarrow> forces_mem'(P,leq,p,t1,t2)"
   unfolding is_forces_mem'_def forces_mem'_def
   using frc_at_abs zero_in_M tuples_in_M by auto
 
 lemma forces_neq'_abs :
   assumes
     "p\<in>M" "t1\<in>M" "t2\<in>M"
   shows
     "is_forces_neq'(##M,P,leq,p,t1,t2) \<longleftrightarrow> forces_neq'(P,leq,p,t1,t2)"
 proof -
   have "q\<in>M" if "q\<in>P" for q
     using that transitivity P_in_M by simp
   then show ?thesis
     unfolding is_forces_neq'_def forces_neq'_def
     using assms forces_eq'_abs pair_in_M_iff
     by (auto,blast)
 qed
 
 
 lemma forces_nmem'_abs :
   assumes
     "p\<in>M" "t1\<in>M" "t2\<in>M"
   shows
     "is_forces_nmem'(##M,P,leq,p,t1,t2) \<longleftrightarrow> forces_nmem'(P,leq,p,t1,t2)"
 proof -
   have "q\<in>M" if "q\<in>P" for q
     using that transitivity P_in_M by simp
   then show ?thesis
     unfolding is_forces_nmem'_def forces_nmem'_def
     using assms forces_mem'_abs pair_in_M_iff
     by (auto,blast)
 qed
 
 end (* forcing_data *)
 
 subsection\<open>Forcing for general formulas\<close>
 
 definition
   ren_forces_nand :: "i\<Rightarrow>i" where
   "ren_forces_nand(\<phi>) \<equiv> Exists(And(Equal(0,1),iterates(\<lambda>p. incr_bv(p)`1 , 2, \<phi>)))"
 
 lemma ren_forces_nand_type[TC] :
   "\<phi>\<in>formula \<Longrightarrow> ren_forces_nand(\<phi>) \<in>formula"
   unfolding ren_forces_nand_def
   by simp
 
 lemma arity_ren_forces_nand :
   assumes "\<phi>\<in>formula"
   shows "arity(ren_forces_nand(\<phi>)) \<le> succ(arity(\<phi>))"
 proof -
   consider (lt) "1<arity(\<phi>)" | (ge) "\<not> 1 < arity(\<phi>)"
     by auto
   then
   show ?thesis
   proof cases
     case lt
     with \<open>\<phi>\<in>_\<close>
     have "2 < succ(arity(\<phi>))" "2<arity(\<phi>)#+2"
       using succ_ltI by auto
     with \<open>\<phi>\<in>_\<close>
     have "arity(iterates(\<lambda>p. incr_bv(p)`1,2,\<phi>)) = 2#+arity(\<phi>)"
       using arity_incr_bv_lemma lt
       by auto
     with \<open>\<phi>\<in>_\<close>
     show ?thesis
       unfolding ren_forces_nand_def
       using lt pred_Un_distrib nat_union_abs1 Un_assoc[symmetric] Un_le_compat
       by simp
   next
     case ge
     with \<open>\<phi>\<in>_\<close>
     have "arity(\<phi>) \<le> 1" "pred(arity(\<phi>)) \<le> 1"
       using not_lt_iff_le le_trans[OF le_pred]
       by simp_all
     with \<open>\<phi>\<in>_\<close>
     have "arity(iterates(\<lambda>p. incr_bv(p)`1,2,\<phi>)) = (arity(\<phi>))"
       using arity_incr_bv_lemma ge
       by simp
     with \<open>arity(\<phi>) \<le> 1\<close> \<open>\<phi>\<in>_\<close> \<open>pred(_) \<le> 1\<close>
     show ?thesis
       unfolding ren_forces_nand_def
       using  pred_Un_distrib nat_union_abs1 Un_assoc[symmetric] nat_union_abs2
       by simp
   qed
 qed
 
 lemma sats_ren_forces_nand:
   "[q,P,leq,o,p] @ env \<in> list(M) \<Longrightarrow> \<phi>\<in>formula \<Longrightarrow>
    sats(M, ren_forces_nand(\<phi>),[q,p,P,leq,o] @ env) \<longleftrightarrow> sats(M, \<phi>,[q,P,leq,o] @ env)"
   unfolding ren_forces_nand_def
   using sats_incr_bv_iff [of _ _ M _ "[q]"]
   by simp
 
 
 definition
   ren_forces_forall :: "i\<Rightarrow>i" where
   "ren_forces_forall(\<phi>) \<equiv>
       Exists(Exists(Exists(Exists(Exists(
         And(Equal(0,6),And(Equal(1,7),And(Equal(2,8),And(Equal(3,9),
         And(Equal(4,5),iterates(\<lambda>p. incr_bv(p)`5 , 5, \<phi>)))))))))))"
 
 lemma arity_ren_forces_all :
   assumes "\<phi>\<in>formula"
   shows "arity(ren_forces_forall(\<phi>)) = 5 \<union> arity(\<phi>)"
 proof -
   consider (lt) "5<arity(\<phi>)" | (ge) "\<not> 5 < arity(\<phi>)"
     by auto
   then
   show ?thesis
   proof cases
     case lt
     with \<open>\<phi>\<in>_\<close>
     have "5 < succ(arity(\<phi>))" "5<arity(\<phi>)#+2"  "5<arity(\<phi>)#+3"  "5<arity(\<phi>)#+4"
       using succ_ltI by auto
     with \<open>\<phi>\<in>_\<close>
     have "arity(iterates(\<lambda>p. incr_bv(p)`5,5,\<phi>)) = 5#+arity(\<phi>)"
       using arity_incr_bv_lemma lt
       by simp
     with \<open>\<phi>\<in>_\<close>
     show ?thesis
       unfolding ren_forces_forall_def
       using pred_Un_distrib nat_union_abs1 Un_assoc[symmetric] nat_union_abs2
       by simp
   next
     case ge
     with \<open>\<phi>\<in>_\<close>
     have "arity(\<phi>) \<le> 5" "pred^5(arity(\<phi>)) \<le> 5"
       using not_lt_iff_le le_trans[OF le_pred]
       by simp_all
     with \<open>\<phi>\<in>_\<close>
     have "arity(iterates(\<lambda>p. incr_bv(p)`5,5,\<phi>)) = arity(\<phi>)"
       using arity_incr_bv_lemma ge
       by simp
     with \<open>arity(\<phi>) \<le> 5\<close> \<open>\<phi>\<in>_\<close> \<open>pred^5(_) \<le> 5\<close>
     show ?thesis
       unfolding ren_forces_forall_def
       using  pred_Un_distrib nat_union_abs1 Un_assoc[symmetric] nat_union_abs2
       by simp
   qed
 qed
 
 lemma ren_forces_forall_type[TC] :
   "\<phi>\<in>formula \<Longrightarrow> ren_forces_forall(\<phi>) \<in>formula"
   unfolding ren_forces_forall_def by simp
 
 lemma sats_ren_forces_forall :
   "[x,P,leq,o,p] @ env \<in> list(M) \<Longrightarrow> \<phi>\<in>formula \<Longrightarrow>
     sats(M, ren_forces_forall(\<phi>),[x,p,P,leq,o] @ env) \<longleftrightarrow> sats(M, \<phi>,[p,P,leq,o,x] @ env)"
   unfolding ren_forces_forall_def
   using sats_incr_bv_iff [of _ _ M _ "[p,P,leq,o,x]"]
   by simp
 
 
 definition
   is_leq :: "[i\<Rightarrow>o,i,i,i] \<Rightarrow> o" where
   "is_leq(A,l,q,p) \<equiv> \<exists>qp[A]. (pair(A,q,p,qp) \<and> qp\<in>l)"
 
 lemma (in forcing_data) leq_abs[simp]:
   "\<lbrakk> l\<in>M ; q\<in>M ; p\<in>M \<rbrakk> \<Longrightarrow> is_leq(##M,l,q,p) \<longleftrightarrow> \<langle>q,p\<rangle>\<in>l"
   unfolding is_leq_def using pair_in_M_iff by simp
 
 
 definition
   leq_fm :: "[i,i,i] \<Rightarrow> i" where
   "leq_fm(leq,q,p) \<equiv> Exists(And(pair_fm(q#+1,p#+1,0),Member(0,leq#+1)))"
 
 lemma arity_leq_fm :
   "\<lbrakk>leq\<in>nat;q\<in>nat;p\<in>nat\<rbrakk> \<Longrightarrow> arity(leq_fm(leq,q,p)) = succ(q) \<union> succ(p) \<union> succ(leq)"
   unfolding leq_fm_def
   using arity_pair_fm pred_Un_distrib nat_simp_union
   by auto
 
 lemma leq_fm_type[TC] :
   "\<lbrakk>leq\<in>nat;q\<in>nat;p\<in>nat\<rbrakk> \<Longrightarrow> leq_fm(leq,q,p)\<in>formula"
   unfolding leq_fm_def by simp
 
 lemma sats_leq_fm :
   "\<lbrakk> leq\<in>nat;q\<in>nat;p\<in>nat;env\<in>list(A) \<rbrakk> \<Longrightarrow>
      sats(A,leq_fm(leq,q,p),env) \<longleftrightarrow> is_leq(##A,nth(leq,env),nth(q,env),nth(p,env))"
   unfolding leq_fm_def is_leq_def by simp
 
 subsubsection\<open>The primitive recursion\<close>
 
 consts forces' :: "i\<Rightarrow>i"
 primrec
   "forces'(Member(x,y)) = forces_mem_fm(1,2,0,x#+4,y#+4)"
   "forces'(Equal(x,y))  = forces_eq_fm(1,2,0,x#+4,y#+4)"
   "forces'(Nand(p,q))   =
         Neg(Exists(And(Member(0,2),And(leq_fm(3,0,1),And(ren_forces_nand(forces'(p)),
                                          ren_forces_nand(forces'(q)))))))"
   "forces'(Forall(p))   = Forall(ren_forces_forall(forces'(p)))"
 
 
 definition
   forces :: "i\<Rightarrow>i" where
   "forces(\<phi>) \<equiv> And(Member(0,1),forces'(\<phi>))"
 
 lemma forces'_type [TC]:  "\<phi>\<in>formula \<Longrightarrow> forces'(\<phi>) \<in> formula"
   by (induct \<phi> set:formula; simp)
 
 lemma forces_type[TC] : "\<phi>\<in>formula \<Longrightarrow> forces(\<phi>) \<in> formula"
   unfolding forces_def by simp
 
 context forcing_data
 begin
 
 subsection\<open>Forcing for atomic formulas in context\<close>
 
 definition
   forces_eq :: "[i,i,i] \<Rightarrow> o" where
   "forces_eq \<equiv> forces_eq'(P,leq)"
 
 definition
   forces_mem :: "[i,i,i] \<Rightarrow> o" where
   "forces_mem \<equiv> forces_mem'(P,leq)"
 
 (* frc_at(P,leq,\<langle>0,t1,t2,p\<rangle>) = 1*)
 definition
   is_forces_eq :: "[i,i,i] \<Rightarrow> o" where
   "is_forces_eq \<equiv> is_forces_eq'(##M,P,leq)"
 
 (* frc_at(P,leq,\<langle>1,t1,t2,p\<rangle>) = 1*)
 definition
   is_forces_mem :: "[i,i,i] \<Rightarrow> o" where
   "is_forces_mem \<equiv> is_forces_mem'(##M,P,leq)"
 
 
 lemma def_forces_eq: "p\<in>P \<Longrightarrow> forces_eq(p,t1,t2) \<longleftrightarrow>
       (\<forall>s\<in>domain(t1) \<union> domain(t2). \<forall>q. q\<in>P \<and> q \<preceq> p \<longrightarrow>
       (forces_mem(q,s,t1) \<longleftrightarrow> forces_mem(q,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\<in>P \<Longrightarrow> forces_mem(p,t1,t2) \<longleftrightarrow>
      (\<forall>v\<in>P. v \<preceq> p \<longrightarrow>
       (\<exists>q. \<exists>s. \<exists>r. r\<in>P \<and> q\<in>P \<and> q \<preceq> v \<and> \<langle>s,r\<rangle> \<in> t2 \<and> q \<preceq> r \<and> forces_eq(q,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 :
   "\<lbrakk>p\<in>M ; t1\<in>M ; t2\<in>M\<rbrakk> \<Longrightarrow> is_forces_eq(p,t1,t2) \<longleftrightarrow> forces_eq(p,t1,t2)"
   unfolding is_forces_eq_def forces_eq_def
   using forces_eq'_abs by simp
 
 lemma forces_mem_abs :
   "\<lbrakk>p\<in>M ; t1\<in>M ; t2\<in>M\<rbrakk> \<Longrightarrow> is_forces_mem(p,t1,t2) \<longleftrightarrow> forces_mem(p,t1,t2)"
   unfolding is_forces_mem_def forces_mem_def
   using forces_mem'_abs by simp
 
 lemma sats_forces_eq_fm:
   assumes  "p\<in>nat" "l\<in>nat" "q\<in>nat" "t1\<in>nat" "t2\<in>nat"  "env\<in>list(M)"
     "nth(p,env)=P" "nth(l,env)=leq"
   shows "sats(M,forces_eq_fm(p,l,q,t1,t2),env) \<longleftrightarrow>
          is_forces_eq(nth(q,env),nth(t1,env),nth(t2,env))"
   unfolding forces_eq_fm_def is_forces_eq_def is_forces_eq'_def
   using assms sats_is_tuple_fm  sats_frc_at_fm
   by simp
 
 lemma sats_forces_mem_fm:
   assumes  "p\<in>nat" "l\<in>nat" "q\<in>nat" "t1\<in>nat" "t2\<in>nat"  "env\<in>list(M)"
     "nth(p,env)=P" "nth(l,env)=leq"
   shows "sats(M,forces_mem_fm(p,l,q,t1,t2),env) \<longleftrightarrow>
              is_forces_mem(nth(q,env),nth(t1,env),nth(t2,env))"
   unfolding forces_mem_fm_def is_forces_mem_def is_forces_mem'_def
   using assms sats_is_tuple_fm sats_frc_at_fm
   by simp
 
 
 definition
   forces_neq :: "[i,i,i] \<Rightarrow> o" where
   "forces_neq(p,t1,t2) \<equiv> \<not> (\<exists>q\<in>P. q\<preceq>p \<and> forces_eq(q,t1,t2))"
 
 definition
   forces_nmem :: "[i,i,i] \<Rightarrow> o" where
   "forces_nmem(p,t1,t2) \<equiv> \<not> (\<exists>q\<in>P. q\<preceq>p \<and> forces_mem(q,t1,t2))"
 
 
 lemma forces_neq :
   "forces_neq(p,t1,t2) \<longleftrightarrow> forces_neq'(P,leq,p,t1,t2)"
   unfolding forces_neq_def forces_neq'_def forces_eq_def by simp
 
 lemma forces_nmem :
   "forces_nmem(p,t1,t2) \<longleftrightarrow> forces_nmem'(P,leq,p,t1,t2)"
   unfolding forces_nmem_def forces_nmem'_def forces_mem_def by simp
 
 
 lemma sats_forces_Member :
   assumes  "x\<in>nat" "y\<in>nat" "env\<in>list(M)"
     "nth(x,env)=xx" "nth(y,env)=yy" "q\<in>M"
   shows "sats(M,forces(Member(x,y)),[q,P,leq,one]@env) \<longleftrightarrow>
                 (q\<in>P \<and> is_forces_mem(q,xx,yy))"
   unfolding forces_def
   using assms sats_forces_mem_fm P_in_M leq_in_M one_in_M
   by simp
 
 lemma sats_forces_Equal :
   assumes  "x\<in>nat" "y\<in>nat" "env\<in>list(M)"
     "nth(x,env)=xx" "nth(y,env)=yy" "q\<in>M"
   shows "sats(M,forces(Equal(x,y)),[q,P,leq,one]@env) \<longleftrightarrow>
                 (q\<in>P \<and> is_forces_eq(q,xx,yy))"
   unfolding forces_def
   using assms sats_forces_eq_fm P_in_M leq_in_M one_in_M
   by simp
 
 lemma sats_forces_Nand :
   assumes  "\<phi>\<in>formula" "\<psi>\<in>formula" "env\<in>list(M)" "p\<in>M"
   shows "sats(M,forces(Nand(\<phi>,\<psi>)),[p,P,leq,one]@env) \<longleftrightarrow>
          (p\<in>P \<and> \<not>(\<exists>q\<in>M. q\<in>P \<and> is_leq(##M,leq,q,p) \<and>
                (sats(M,forces'(\<phi>),[q,P,leq,one]@env) \<and> sats(M,forces'(\<psi>),[q,P,leq,one]@env))))"
   unfolding forces_def using sats_leq_fm assms sats_ren_forces_nand P_in_M leq_in_M one_in_M
   by simp
 
 lemma sats_forces_Neg :
   assumes  "\<phi>\<in>formula" "env\<in>list(M)" "p\<in>M"
   shows "sats(M,forces(Neg(\<phi>)),[p,P,leq,one]@env) \<longleftrightarrow>
          (p\<in>P \<and> \<not>(\<exists>q\<in>M. q\<in>P \<and> is_leq(##M,leq,q,p) \<and>
                (sats(M,forces'(\<phi>),[q,P,leq,one]@env))))"
   unfolding Neg_def using assms sats_forces_Nand
   by simp
 
 lemma sats_forces_Forall :
   assumes  "\<phi>\<in>formula" "env\<in>list(M)" "p\<in>M"
   shows "sats(M,forces(Forall(\<phi>)),[p,P,leq,one]@env) \<longleftrightarrow>
          p\<in>P \<and> (\<forall>x\<in>M. sats(M,forces'(\<phi>),[p,P,leq,one,x]@env))"
   unfolding forces_def using assms sats_ren_forces_forall P_in_M leq_in_M one_in_M
   by simp
 
 end (* forcing_data *)
 
 subsection\<open>The arity of \<^term>\<open>forces\<close>\<close>
 
 lemma arity_forces_at:
   assumes  "x \<in> nat" "y \<in> nat"
   shows "arity(forces(Member(x, y))) = (succ(x) \<union> succ(y)) #+ 4"
     "arity(forces(Equal(x, y))) = (succ(x) \<union> succ(y)) #+ 4"
   unfolding forces_def
   using assms arity_forces_mem_fm arity_forces_eq_fm succ_Un_distrib nat_simp_union
   by auto
 
 lemma arity_forces':
   assumes "\<phi>\<in>formula"
   shows "arity(forces'(\<phi>)) \<le> arity(\<phi>) #+ 4"
   using assms
 proof (induct set:formula)
   case (Member x y)
   then
   show ?case
     using arity_forces_mem_fm succ_Un_distrib nat_simp_union
     by simp
 next
   case (Equal x y)
   then
   show ?case
     using arity_forces_eq_fm succ_Un_distrib nat_simp_union
     by simp
 next
   case (Nand \<phi> \<psi>)
   let ?\<phi>' = "ren_forces_nand(forces'(\<phi>))"
   let ?\<psi>' = "ren_forces_nand(forces'(\<psi>))"
   have "arity(leq_fm(3, 0, 1)) = 4"
     using arity_leq_fm succ_Un_distrib nat_simp_union
     by simp
   have "3 \<le> (4#+arity(\<phi>)) \<union> (4#+arity(\<psi>))" (is "_ \<le> ?rhs")
     using nat_simp_union by simp
   from \<open>\<phi>\<in>_\<close> Nand
   have "pred(arity(?\<phi>')) \<le> ?rhs"  "pred(arity(?\<psi>')) \<le> ?rhs"
   proof -
     from \<open>\<phi>\<in>_\<close> \<open>\<psi>\<in>_\<close>
     have A:"pred(arity(?\<phi>')) \<le> arity(forces'(\<phi>))"
       "pred(arity(?\<psi>')) \<le> arity(forces'(\<psi>))"
       using pred_mono[OF _  arity_ren_forces_nand] pred_succ_eq
       by simp_all
     from Nand
     have "3 \<union> arity(forces'(\<phi>)) \<le> arity(\<phi>) #+ 4"
       "3 \<union> arity(forces'(\<psi>)) \<le> arity(\<psi>) #+ 4"
       using Un_le by simp_all
     with Nand
     show "pred(arity(?\<phi>')) \<le> ?rhs"
       "pred(arity(?\<psi>')) \<le> ?rhs"
       using le_trans[OF A(1)] le_trans[OF A(2)] le_Un_iff
       by simp_all
   qed
   with Nand \<open>_=4\<close>
   show ?case
     using pred_Un_distrib Un_assoc[symmetric] succ_Un_distrib nat_union_abs1 Un_leI3[OF \<open>3 \<le> ?rhs\<close>]
     by simp
 next
   case (Forall \<phi>)
   let ?\<phi>' = "ren_forces_forall(forces'(\<phi>))"
   show ?case
   proof (cases "arity(\<phi>) = 0")
     case True
     with Forall
     show ?thesis
     proof -
       from Forall True
       have "arity(forces'(\<phi>)) \<le> 5"
         using le_trans[of _ 4 5] by auto
       with \<open>\<phi>\<in>_\<close>
       have "arity(?\<phi>') \<le> 5"
         using arity_ren_forces_all[OF forces'_type[OF \<open>\<phi>\<in>_\<close>]] nat_union_abs2
         by auto
       with Forall True
       show ?thesis
         using pred_mono[OF _ \<open>arity(?\<phi>') \<le> 5\<close>]
         by simp
     qed
   next
     case False
     with Forall
     show ?thesis
     proof -
       from Forall False
       have "arity(?\<phi>') = 5 \<union> arity(forces'(\<phi>))"
         "arity(forces'(\<phi>)) \<le> 5 #+ arity(\<phi>)"
         "4 \<le> succ(succ(succ(arity(\<phi>))))"
         using Ord_0_lt arity_ren_forces_all
           le_trans[OF _ add_le_mono[of 4 5, OF _ le_refl]]
         by auto
       with \<open>\<phi>\<in>_\<close>
       have "5 \<union> arity(forces'(\<phi>)) \<le> 5#+arity(\<phi>)"
         using nat_simp_union by auto
       with \<open>\<phi>\<in>_\<close> \<open>arity(?\<phi>') = 5 \<union> _\<close>
       show ?thesis
         using pred_Un_distrib succ_pred_eq[OF _ \<open>arity(\<phi>)\<noteq>0\<close>]
           pred_mono[OF _ Forall(2)] Un_le[OF \<open>4\<le>succ(_)\<close>]
         by simp
     qed
   qed
 qed
 
 lemma arity_forces :
   assumes "\<phi>\<in>formula"
   shows "arity(forces(\<phi>)) \<le> 4#+arity(\<phi>)"
   unfolding forces_def
   using assms arity_forces' le_trans nat_simp_union by auto
 
 lemma arity_forces_le :
   assumes "\<phi>\<in>formula" "n\<in>nat" "arity(\<phi>) \<le> n"
   shows "arity(forces(\<phi>)) \<le> 4#+n"
   using assms le_trans[OF _ add_le_mono[OF le_refl[of 5] \<open>arity(\<phi>)\<le>_\<close>]] arity_forces
   by auto
 
 end
\ No newline at end of file
diff --git a/thys/Forcing/Internal_ZFC_Axioms.thy b/thys/Forcing/Internal_ZFC_Axioms.thy
--- a/thys/Forcing/Internal_ZFC_Axioms.thy
+++ b/thys/Forcing/Internal_ZFC_Axioms.thy
@@ -1,523 +1,523 @@
 section\<open>The ZFC axioms, internalized\<close>
 theory Internal_ZFC_Axioms
   imports 
   Forcing_Data
 
 begin
 
 schematic_goal ZF_union_auto:
     "Union_ax(##A) \<longleftrightarrow> (A, [] \<Turnstile> ?zfunion)"
   unfolding Union_ax_def 
   by ((rule sep_rules | simp)+)
 
 synthesize "ZF_union_fm" from_schematic ZF_union_auto
 
 schematic_goal ZF_power_auto:
     "power_ax(##A) \<longleftrightarrow> (A, [] \<Turnstile> ?zfpow)"
   unfolding power_ax_def powerset_def subset_def
   by ((rule sep_rules | simp)+)
 
 synthesize "ZF_power_fm" from_schematic ZF_power_auto
 
 schematic_goal ZF_pairing_auto:
     "upair_ax(##A) \<longleftrightarrow> (A, [] \<Turnstile> ?zfpair)"
   unfolding upair_ax_def 
   by ((rule sep_rules | simp)+)
 
 synthesize "ZF_pairing_fm" from_schematic ZF_pairing_auto
 
 schematic_goal ZF_foundation_auto:
     "foundation_ax(##A) \<longleftrightarrow> (A, [] \<Turnstile> ?zfpow)"
   unfolding foundation_ax_def 
   by ((rule sep_rules | simp)+)
 
 synthesize "ZF_foundation_fm" from_schematic ZF_foundation_auto
 
 schematic_goal ZF_extensionality_auto:
     "extensionality(##A) \<longleftrightarrow> (A, [] \<Turnstile> ?zfpow)"
   unfolding extensionality_def 
   by ((rule sep_rules | simp)+)
 
 synthesize "ZF_extensionality_fm" from_schematic ZF_extensionality_auto
 
 schematic_goal ZF_infinity_auto:
     "infinity_ax(##A) \<longleftrightarrow> (A, [] \<Turnstile> (?\<phi>(i,j,h)))"
   unfolding infinity_ax_def 
   by ((rule sep_rules | simp)+)
 
 synthesize "ZF_infinity_fm" from_schematic ZF_infinity_auto
 
 schematic_goal ZF_choice_auto:
     "choice_ax(##A) \<longleftrightarrow> (A, [] \<Turnstile> (?\<phi>(i,j,h)))"
   unfolding choice_ax_def 
   by ((rule sep_rules | simp)+)
 
 synthesize "ZF_choice_fm" from_schematic ZF_choice_auto
 
 syntax
   "_choice" :: "i"  ("AC")
 translations
   "AC" \<rightharpoonup> "CONST ZF_choice_fm"
 
 lemmas ZFC_fm_defs = ZF_extensionality_fm_def ZF_foundation_fm_def ZF_pairing_fm_def
               ZF_union_fm_def ZF_infinity_fm_def ZF_power_fm_def ZF_choice_fm_def
 
 lemmas ZFC_fm_sats = ZF_extensionality_auto ZF_foundation_auto ZF_pairing_auto
               ZF_union_auto ZF_infinity_auto ZF_power_auto ZF_choice_auto
 
 definition
   ZF_fin :: "i" where
   "ZF_fin \<equiv> { ZF_extensionality_fm, ZF_foundation_fm, ZF_pairing_fm,
               ZF_union_fm, ZF_infinity_fm, ZF_power_fm }"
 
 definition
   ZFC_fin :: "i" where
   "ZFC_fin \<equiv> ZF_fin \<union> {ZF_choice_fm}"
 
 lemma ZFC_fin_type : "ZFC_fin \<subseteq> formula"
   unfolding ZFC_fin_def ZF_fin_def ZFC_fm_defs by (auto)
 
 subsection\<open>The Axiom of Separation, internalized\<close>
 lemma iterates_Forall_type [TC]:
       "\<lbrakk> n \<in> nat; p \<in> formula \<rbrakk> \<Longrightarrow> Forall^n(p) \<in> formula"
   by (induct set:nat, auto)
 
 lemma last_init_eq :
   assumes "l \<in> list(A)" "length(l) = succ(n)"
   shows "\<exists> a\<in>A. \<exists>l'\<in>list(A). l = l'@[a]"
 proof-
   from \<open>l\<in>_\<close> \<open>length(_) = _\<close>
   have "rev(l) \<in> list(A)" "length(rev(l)) = succ(n)"
     by simp_all
   then
   obtain a l' where "a\<in>A" "l'\<in>list(A)" "rev(l) = Cons(a,l')"
     by (cases;simp)
   then
   have "l = rev(l') @ [a]" "rev(l') \<in> list(A)"
     using rev_rev_ident[OF \<open>l\<in>_\<close>] by auto
   with \<open>a\<in>_\<close>
   show ?thesis by blast
 qed
 
 lemma take_drop_eq :
   assumes "l\<in>list(M)"
   shows "\<And> n . n < succ(length(l)) \<Longrightarrow> l = take(n,l) @ drop(n,l)"
   using \<open>l\<in>list(M)\<close>
 proof induct
   case Nil
   then show ?case by auto
 next
   case (Cons a l)
   then show ?case
   proof -
     {
       fix i
       assume "i<succ(succ(length(l)))"
       with \<open>l\<in>list(M)\<close>
       consider (lt) "i = 0" | (eq) "\<exists>k\<in>nat. i = succ(k) \<and> k < succ(length(l))"
         using \<open>l\<in>list(M)\<close>  le_natI nat_imp_quasinat
         by (cases rule:nat_cases[of i];auto)
       then
       have "take(i,Cons(a,l)) @ drop(i,Cons(a,l)) = Cons(a,l)"
         using Cons
         by (cases;auto)
     }
     then show ?thesis using Cons by auto
   qed
 qed
 
 lemma list_split :
 assumes "n \<le> succ(length(rest))" "rest \<in> list(M)"
 shows  "\<exists>re\<in>list(M). \<exists>st\<in>list(M). rest = re @ st \<and> length(re) = pred(n)"
 proof -
   from assms
   have "pred(n) \<le> length(rest)"
     using pred_mono[OF _ \<open>n\<le>_\<close>] pred_succ_eq by auto
   with \<open>rest\<in>_\<close>
   have "pred(n)\<in>nat" "rest = take(pred(n),rest) @ drop(pred(n),rest)" (is "_ = ?re @ ?st")
     using take_drop_eq[OF \<open>rest\<in>_\<close>] le_natI by auto
   then
   have "length(?re) = pred(n)" "?re\<in>list(M)" "?st\<in>list(M)"
     using length_take[rule_format,OF _ \<open>pred(n)\<in>_\<close>] \<open>pred(n) \<le> _\<close> \<open>rest\<in>_\<close>
     unfolding min_def
     by auto
   then
   show ?thesis
     using rev_bexI[of _ _ "\<lambda> re. \<exists>st\<in>list(M). rest = re @ st \<and> length(re) = pred(n)"]
       \<open>length(?re) = _\<close> \<open>rest = _\<close>
     by auto
 qed
 
 lemma sats_nForall:
   assumes
     "\<phi> \<in> formula"
   shows
     "n\<in>nat \<Longrightarrow> ms \<in> list(M) \<Longrightarrow>
        M, ms \<Turnstile> (Forall^n(\<phi>)) \<longleftrightarrow>
        (\<forall>rest \<in> list(M). length(rest) = n \<longrightarrow> M, rest @ ms \<Turnstile> \<phi>)"
 proof (induct n arbitrary:ms set:nat)
   case 0
   with assms
   show ?case by simp
 next
   case (succ n)
   have "(\<forall>rest\<in>list(M). length(rest) = succ(n) \<longrightarrow> P(rest,n)) \<longleftrightarrow>
         (\<forall>t\<in>M. \<forall>res\<in>list(M). length(res) = n \<longrightarrow> P(res @ [t],n))"
     if "n\<in>nat" for n P
     using that last_init_eq by force
   from this[of _ "\<lambda>rest _. (M, rest @ ms \<Turnstile> \<phi>)"] \<open>n\<in>nat\<close>
   have "(\<forall>rest\<in>list(M). length(rest) = succ(n) \<longrightarrow> M, rest @ ms \<Turnstile> \<phi>) \<longleftrightarrow>
         (\<forall>t\<in>M. \<forall>res\<in>list(M). length(res) = n \<longrightarrow>  M, (res @ [t]) @ ms \<Turnstile> \<phi>)"
     by simp
     with assms succ(1,3) succ(2)[of "Cons(_,ms)"]
   show ?case
     using arity_sats_iff[of \<phi> _ M "Cons(_, ms @ _)"] app_assoc
     by (simp)
 qed
 
 definition
   sep_body_fm :: "i \<Rightarrow> i" where
   "sep_body_fm(p) \<equiv> Forall(Exists(Forall(
                            Iff(Member(0,1),And(Member(0,2),
                                     incr_bv1^2(p))))))"
 
 lemma sep_body_fm_type [TC]: "p \<in> formula \<Longrightarrow> sep_body_fm(p) \<in> formula"
   by (simp add: sep_body_fm_def)
 
 lemma sats_sep_body_fm: 
   assumes
     "\<phi> \<in> formula" "ms\<in>list(M)" "rest\<in>list(M)"
   shows
     "M, rest @ ms \<Turnstile> sep_body_fm(\<phi>) \<longleftrightarrow> 
      separation(##M,\<lambda>x. M, [x] @ rest @ ms \<Turnstile> \<phi>)"
   using assms formula_add_params1[of _ 2 _ _ "[_,_]" ]
   unfolding sep_body_fm_def separation_def by simp
 
 definition
   ZF_separation_fm :: "i \<Rightarrow> i" where
   "ZF_separation_fm(p) \<equiv> Forall^(pred(arity(p)))(sep_body_fm(p))"
 
 lemma ZF_separation_fm_type [TC]: "p \<in> formula \<Longrightarrow> ZF_separation_fm(p) \<in> formula"
   by (simp add: ZF_separation_fm_def)
 
 lemma sats_ZF_separation_fm_iff:
   assumes
     "\<phi>\<in>formula"
   shows
   "(M, [] \<Turnstile> (ZF_separation_fm(\<phi>)))
    \<longleftrightarrow>
    (\<forall>env\<in>list(M). arity(\<phi>) \<le> 1 #+ length(env) \<longrightarrow> 
       separation(##M,\<lambda>x. M, [x] @ env \<Turnstile> \<phi>))"
 proof (intro iffI ballI impI)
   let ?n="Arith.pred(arity(\<phi>))"
   fix env
   assume "M, [] \<Turnstile> ZF_separation_fm(\<phi>)" 
   assume "arity(\<phi>) \<le> 1 #+ length(env)" "env\<in>list(M)"
   moreover from this
   have "arity(\<phi>) \<le> succ(length(env))" by simp
   then
   obtain some rest where "some\<in>list(M)" "rest\<in>list(M)" 
     "env = some @ rest" "length(some) = Arith.pred(arity(\<phi>))"
     using list_split[OF \<open>arity(\<phi>) \<le> succ(_)\<close> \<open>env\<in>_\<close>] by force
   moreover from \<open>\<phi>\<in>_\<close>
   have "arity(\<phi>) \<le> succ(Arith.pred(arity(\<phi>)))"
    using succpred_leI by simp
   moreover
   note assms
   moreover 
   assume "M, [] \<Turnstile> ZF_separation_fm(\<phi>)" 
   moreover from calculation
   have "M, some \<Turnstile> sep_body_fm(\<phi>)"
     using sats_nForall[of "sep_body_fm(\<phi>)" ?n]
     unfolding ZF_separation_fm_def by simp
   ultimately
   show "separation(##M, \<lambda>x. M, [x] @ env \<Turnstile> \<phi>)"
     unfolding ZF_separation_fm_def
     using sats_sep_body_fm[of \<phi> "[]" M some]
       arity_sats_iff[of \<phi> rest M "[_] @ some"]
       separation_cong[of "##M" "\<lambda>x. M, Cons(x, some @ rest) \<Turnstile> \<phi>" _ ]
     by simp
 next \<comment> \<open>almost equal to the previous implication\<close>
   let ?n="Arith.pred(arity(\<phi>))"
   assume asm:"\<forall>env\<in>list(M). arity(\<phi>) \<le> 1 #+ length(env) \<longrightarrow> 
     separation(##M, \<lambda>x. M, [x] @ env \<Turnstile> \<phi>)"
   {
     fix some
     assume "some\<in>list(M)" "length(some) = Arith.pred(arity(\<phi>))"
     moreover
     note \<open>\<phi>\<in>_\<close>
     moreover from calculation
     have "arity(\<phi>) \<le> 1 #+ length(some)" 
       using le_trans[OF succpred_leI] succpred_leI by simp
     moreover from calculation and asm
     have "separation(##M, \<lambda>x. M, [x] @ some \<Turnstile> \<phi>)" by blast
     ultimately
     have "M, some \<Turnstile> sep_body_fm(\<phi>)" 
     using sats_sep_body_fm[of \<phi> "[]" M some]
       arity_sats_iff[of \<phi> _ M "[_,_] @ some"]
       strong_replacement_cong[of "##M" "\<lambda>x y. M, Cons(x, Cons(y, some @ _)) \<Turnstile> \<phi>" _ ]
     by simp
   }
   with \<open>\<phi>\<in>_\<close>
   show "M, [] \<Turnstile> ZF_separation_fm(\<phi>)"
     using sats_nForall[of "sep_body_fm(\<phi>)" ?n]
     unfolding ZF_separation_fm_def
     by simp
 qed
 
 subsection\<open>The Axiom of Replacement, internalized\<close>
 schematic_goal sats_univalent_fm_auto:
   assumes 
     (*    Q_iff_sats:"\<And>a b z env aa bb. nth(a,Cons(z,env)) = aa \<Longrightarrow> nth(b,Cons(z,env)) = bb \<Longrightarrow> z\<in>A 
           \<Longrightarrow> aa \<in> A \<Longrightarrow> bb \<in> A \<Longrightarrow> env\<in> list(A) \<Longrightarrow> 
                  Q(aa,bb) \<longleftrightarrow> (A, Cons(z,env) \<Turnstile> (Q_fm(a,b)))" \<comment> \<open>using only one formula\<close> *)
     Q_iff_sats:"\<And>x y z. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z\<in>A \<Longrightarrow> 
                  Q(x,z) \<longleftrightarrow> (A,Cons(z,Cons(y,Cons(x,env))) \<Turnstile> Q1_fm)"
        "\<And>x y z. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z\<in>A \<Longrightarrow> 
                  Q(x,y) \<longleftrightarrow> (A,Cons(z,Cons(y,Cons(x,env))) \<Turnstile> Q2_fm)"
     and 
     asms: "nth(i,env) = B" "i \<in> nat" "env \<in> list(A)"
   shows
     "univalent(##A,B,Q) \<longleftrightarrow> A,env \<Turnstile> ?ufm(i)"
   unfolding univalent_def 
   by (insert asms; (rule sep_rules Q_iff_sats | simp)+)
   
 synthesize_notc "univalent_fm" from_schematic sats_univalent_fm_auto
 
 lemma univalent_fm_type [TC]: "q1\<in> formula \<Longrightarrow> q2\<in>formula \<Longrightarrow> i\<in>nat \<Longrightarrow> 
   univalent_fm(q2,q1,i) \<in>formula"
   by (simp add:univalent_fm_def)
 
 lemma sats_univalent_fm :
   assumes
     Q_iff_sats:"\<And>x y z. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z\<in>A \<Longrightarrow> 
                  Q(x,z) \<longleftrightarrow> (A,Cons(z,Cons(y,Cons(x,env))) \<Turnstile> Q1_fm)"
        "\<And>x y z. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z\<in>A \<Longrightarrow> 
                  Q(x,y) \<longleftrightarrow> (A,Cons(z,Cons(y,Cons(x,env))) \<Turnstile> Q2_fm)"
     and 
     asms: "nth(i,env) = B" "i \<in> nat" "env \<in> list(A)"
   shows
-    "A,env \<Turnstile> univalent_fm(Q2_fm,Q1_fm,i) \<longleftrightarrow> univalent(##A,B,Q)"
+    "A,env \<Turnstile> univalent_fm(Q1_fm,Q2_fm,i) \<longleftrightarrow> univalent(##A,B,Q)"
   unfolding univalent_fm_def using asms sats_univalent_fm_auto[OF Q_iff_sats] by simp
 
 definition
   swap_vars :: "i\<Rightarrow>i" where
   "swap_vars(\<phi>) \<equiv> 
       Exists(Exists(And(Equal(0,3),And(Equal(1,2),iterates(\<lambda>p. incr_bv(p)`2 , 2, \<phi>)))))" 
 
 lemma swap_vars_type[TC] :
   "\<phi>\<in>formula \<Longrightarrow> swap_vars(\<phi>) \<in>formula" 
   unfolding swap_vars_def by simp
 
 lemma sats_swap_vars :
   "[x,y] @ env \<in> list(M) \<Longrightarrow> \<phi>\<in>formula \<Longrightarrow> 
     M, [x,y] @ env \<Turnstile> swap_vars(\<phi>)\<longleftrightarrow> M,[y,x] @ env \<Turnstile> \<phi>"
   unfolding swap_vars_def
   using sats_incr_bv_iff [of _ _ M _ "[y,x]"] by simp
 
 definition
   univalent_Q1 :: "i \<Rightarrow> i" where
   "univalent_Q1(\<phi>) \<equiv> incr_bv1(swap_vars(\<phi>))"
 
 definition
   univalent_Q2 :: "i \<Rightarrow> i" where
   "univalent_Q2(\<phi>) \<equiv> incr_bv(swap_vars(\<phi>))`0"
 
 lemma univalent_Qs_type [TC]: 
   assumes "\<phi>\<in>formula"
   shows "univalent_Q1(\<phi>) \<in> formula" "univalent_Q2(\<phi>) \<in> formula"
   unfolding univalent_Q1_def univalent_Q2_def using assms by simp_all
 
 lemma sats_univalent_fm_assm:
   assumes 
     "x \<in> A" "y \<in> A" "z\<in>A" "env\<in> list(A)" "\<phi> \<in> formula"
   shows 
     "(A, ([x,z] @ env) \<Turnstile> \<phi>) \<longleftrightarrow> (A, Cons(z,Cons(y,Cons(x,env))) \<Turnstile> (univalent_Q1(\<phi>)))"
     "(A, ([x,y] @ env) \<Turnstile> \<phi>) \<longleftrightarrow> (A, Cons(z,Cons(y,Cons(x,env))) \<Turnstile> (univalent_Q2(\<phi>)))"
   unfolding univalent_Q1_def univalent_Q2_def
   using 
     sats_incr_bv_iff[of _ _ A _ "[]"] \<comment> \<open>simplifies iterates of \<^term>\<open>\<lambda>x. incr_bv(x)`0\<close>\<close>
     sats_incr_bv1_iff[of _ "Cons(x,env)" A z y] 
     sats_swap_vars  assms 
    by simp_all
 
 definition
   rep_body_fm :: "i \<Rightarrow> i" where
   "rep_body_fm(p) \<equiv> Forall(Implies(
-        univalent_fm(univalent_Q2(incr_bv(p)`2),univalent_Q1(incr_bv(p)`2),0),
+        univalent_fm(univalent_Q1(incr_bv(p)`2),univalent_Q2(incr_bv(p)`2),0),
         Exists(Forall(
           Iff(Member(0,1),Exists(And(Member(0,3),incr_bv(incr_bv(p)`2)`2)))))))"
 
 lemma rep_body_fm_type [TC]: "p \<in> formula \<Longrightarrow> rep_body_fm(p) \<in> formula"
   by (simp add: rep_body_fm_def)
 
 lemmas ZF_replacement_simps = formula_add_params1[of \<phi> 2 _ M "[_,_]" ]
   sats_incr_bv_iff[of _ _ M _ "[]"] \<comment> \<open>simplifies iterates of \<^term>\<open>\<lambda>x. incr_bv(x)`0\<close>\<close>
   sats_incr_bv_iff[of _ _ M _ "[_,_]"]\<comment> \<open>simplifies \<^term>\<open>\<lambda>x. incr_bv(x)`2\<close>\<close>
   sats_incr_bv1_iff[of _ _ M] sats_swap_vars for \<phi> M
 
 lemma sats_rep_body_fm:
   assumes
     "\<phi> \<in> formula" "ms\<in>list(M)" "rest\<in>list(M)"
   shows
     "M, rest @ ms \<Turnstile> rep_body_fm(\<phi>) \<longleftrightarrow> 
      strong_replacement(##M,\<lambda>x y. M, [x,y] @ rest @ ms \<Turnstile> \<phi>)"
   using assms ZF_replacement_simps 
   unfolding rep_body_fm_def strong_replacement_def univalent_def
   unfolding univalent_fm_def univalent_Q1_def univalent_Q2_def
   by simp
 
 definition
   ZF_replacement_fm :: "i \<Rightarrow> i" where
   "ZF_replacement_fm(p) \<equiv> Forall^(pred(pred(arity(p))))(rep_body_fm(p))"
 
 lemma ZF_replacement_fm_type [TC]: "p \<in> formula \<Longrightarrow> ZF_replacement_fm(p) \<in> formula"
   by (simp add: ZF_replacement_fm_def)
 
 lemma sats_ZF_replacement_fm_iff:
   assumes
     "\<phi>\<in>formula"
   shows
   "(M, [] \<Turnstile> (ZF_replacement_fm(\<phi>)))
    \<longleftrightarrow>
    (\<forall>env\<in>list(M). arity(\<phi>) \<le> 2 #+ length(env) \<longrightarrow> 
       strong_replacement(##M,\<lambda>x y. M,[x,y] @ env \<Turnstile> \<phi>))"
 proof (intro iffI ballI impI)
   let ?n="Arith.pred(Arith.pred(arity(\<phi>)))"
   fix env
   assume "M, [] \<Turnstile> ZF_replacement_fm(\<phi>)" "arity(\<phi>) \<le> 2 #+ length(env)" "env\<in>list(M)"
   moreover from this
   have "arity(\<phi>) \<le> succ(succ(length(env)))" by (simp)
   moreover from calculation 
   have "pred(arity(\<phi>)) \<le> succ(length(env))"
     using pred_mono[OF _ \<open>arity(\<phi>)\<le>succ(_)\<close>] pred_succ_eq by simp
   moreover from calculation
   obtain some rest where "some\<in>list(M)" "rest\<in>list(M)" 
     "env = some @ rest" "length(some) = Arith.pred(Arith.pred(arity(\<phi>)))" 
     using list_split[OF \<open>pred(_) \<le> _\<close> \<open>env\<in>_\<close>] by auto
   moreover
   note \<open>\<phi>\<in>_\<close>
   moreover from this
   have "arity(\<phi>) \<le> succ(succ(Arith.pred(Arith.pred(arity(\<phi>)))))"
     using le_trans[OF succpred_leI] succpred_leI by simp
   moreover from calculation
   have "M, some \<Turnstile> rep_body_fm(\<phi>)"
     using sats_nForall[of "rep_body_fm(\<phi>)" ?n]
     unfolding ZF_replacement_fm_def
     by simp
   ultimately
   show "strong_replacement(##M, \<lambda>x y. M, [x, y] @ env \<Turnstile> \<phi>)"
     using sats_rep_body_fm[of \<phi> "[]" M some]
       arity_sats_iff[of \<phi> rest M "[_,_] @ some"]
       strong_replacement_cong[of "##M" "\<lambda>x y. M, Cons(x, Cons(y, some @ rest)) \<Turnstile> \<phi>" _ ]
     by simp
 next \<comment> \<open>almost equal to the previous implication\<close>
   let ?n="Arith.pred(Arith.pred(arity(\<phi>)))"
   assume asm:"\<forall>env\<in>list(M). arity(\<phi>) \<le> 2 #+ length(env) \<longrightarrow> 
     strong_replacement(##M, \<lambda>x y. M, [x, y] @ env \<Turnstile> \<phi>)"
   {
     fix some
     assume "some\<in>list(M)" "length(some) = Arith.pred(Arith.pred(arity(\<phi>)))"
     moreover
     note \<open>\<phi>\<in>_\<close>
     moreover from calculation
     have "arity(\<phi>) \<le> 2 #+ length(some)" 
       using le_trans[OF succpred_leI] succpred_leI by simp
     moreover from calculation and asm
     have "strong_replacement(##M, \<lambda>x y. M, [x, y] @ some \<Turnstile> \<phi>)" by blast
     ultimately
     have "M, some \<Turnstile> rep_body_fm(\<phi>)" 
     using sats_rep_body_fm[of \<phi> "[]" M some]
       arity_sats_iff[of \<phi> _ M "[_,_] @ some"]
       strong_replacement_cong[of "##M" "\<lambda>x y. M, Cons(x, Cons(y, some @ _)) \<Turnstile> \<phi>" _ ]
     by simp
   }
   with \<open>\<phi>\<in>_\<close>
   show "M, [] \<Turnstile> ZF_replacement_fm(\<phi>)"
     using sats_nForall[of "rep_body_fm(\<phi>)" ?n]
     unfolding ZF_replacement_fm_def
     by simp
 qed
 
 definition
   ZF_inf :: "i" where
   "ZF_inf \<equiv> {ZF_separation_fm(p) . p \<in> formula } \<union> {ZF_replacement_fm(p) . p \<in> formula }"
               
 lemma Un_subset_formula: "A\<subseteq>formula \<and> B\<subseteq>formula \<Longrightarrow> A\<union>B \<subseteq> formula"
   by auto
   
 lemma ZF_inf_subset_formula : "ZF_inf \<subseteq> formula"
   unfolding ZF_inf_def by auto
     
 definition
   ZFC :: "i" where
   "ZFC \<equiv> ZF_inf \<union> ZFC_fin"
 
 definition
   ZF :: "i" where
   "ZF \<equiv> ZF_inf \<union> ZF_fin"
 
 definition 
   ZF_minus_P :: "i" where
   "ZF_minus_P \<equiv> ZF - { ZF_power_fm }"
 
 lemma ZFC_subset_formula: "ZFC \<subseteq> formula"
   by (simp add:ZFC_def Un_subset_formula ZF_inf_subset_formula ZFC_fin_type)
   
 txt\<open>Satisfaction of a set of sentences\<close>
 definition
   satT :: "[i,i] \<Rightarrow> o"  ("_ \<Turnstile> _" [36,36] 60) where
   "A \<Turnstile> \<Phi>  \<equiv>  \<forall>\<phi>\<in>\<Phi>. (A,[] \<Turnstile> \<phi>)"
 
 lemma satTI [intro!]: 
   assumes "\<And>\<phi>. \<phi>\<in>\<Phi> \<Longrightarrow> A,[] \<Turnstile> \<phi>"
   shows "A \<Turnstile> \<Phi>"
   using assms unfolding satT_def by simp
 
 lemma satTD [dest] :"A \<Turnstile> \<Phi> \<Longrightarrow>  \<phi>\<in>\<Phi> \<Longrightarrow> A,[] \<Turnstile> \<phi>"
   unfolding satT_def by simp
 
 lemma sats_ZFC_iff_sats_ZF_AC: 
   "(N \<Turnstile> ZFC) \<longleftrightarrow> (N \<Turnstile> ZF) \<and> (N, [] \<Turnstile> AC)"
     unfolding ZFC_def ZFC_fin_def ZF_def by auto
 
 lemma M_ZF_iff_M_satT: "M_ZF(M) \<longleftrightarrow> (M \<Turnstile> ZF)"
 proof
   assume "M \<Turnstile> ZF"
   then
   have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)"
     "extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)"
     unfolding ZF_def ZF_fin_def ZFC_fm_defs satT_def
     using ZFC_fm_sats[of M] by simp_all
   {
     fix \<phi> env
     assume "\<phi> \<in> formula" "env\<in>list(M)" 
     moreover from \<open>M \<Turnstile> ZF\<close>
     have "\<forall>p\<in>formula. (M, [] \<Turnstile> (ZF_separation_fm(p)))" 
          "\<forall>p\<in>formula. (M, [] \<Turnstile> (ZF_replacement_fm(p)))"
       unfolding ZF_def ZF_inf_def by auto
     moreover from calculation
     have "arity(\<phi>) \<le> succ(length(env)) \<Longrightarrow> separation(##M, \<lambda>x. (M, Cons(x, env) \<Turnstile> \<phi>))"
       "arity(\<phi>) \<le> succ(succ(length(env))) \<Longrightarrow> strong_replacement(##M,\<lambda>x y. sats(M,\<phi>,Cons(x,Cons(y, env))))"
       using sats_ZF_separation_fm_iff sats_ZF_replacement_fm_iff by simp_all  
   }
   with fin
   show "M_ZF(M)"
     unfolding M_ZF_def by simp
 next
   assume \<open>M_ZF(M)\<close>
   then
   have "M \<Turnstile> ZF_fin" 
     unfolding M_ZF_def ZF_fin_def ZFC_fm_defs satT_def
     using ZFC_fm_sats[of M] by blast
   moreover from \<open>M_ZF(M)\<close>
   have "\<forall>p\<in>formula. (M, [] \<Turnstile> (ZF_separation_fm(p)))" 
        "\<forall>p\<in>formula. (M, [] \<Turnstile> (ZF_replacement_fm(p)))"
     unfolding M_ZF_def using sats_ZF_separation_fm_iff 
       sats_ZF_replacement_fm_iff by simp_all
   ultimately
   show "M \<Turnstile> ZF"
     unfolding ZF_def ZF_inf_def by blast
 qed
 
 end
diff --git a/thys/Forcing/Names.thy b/thys/Forcing/Names.thy
--- a/thys/Forcing/Names.thy
+++ b/thys/Forcing/Names.thy
@@ -1,1060 +1,1060 @@
 section\<open>Names and generic extensions\<close>
 
 theory Names
   imports
     Forcing_Data
     Interface
     Recursion_Thms
     Synthetic_Definition
 begin
 
 definition
   SepReplace :: "[i, i\<Rightarrow>i, i\<Rightarrow> o] \<Rightarrow> i" where
   "SepReplace(A,b,Q) \<equiv> {y . x\<in>A, y=b(x) \<and> Q(x)}"
 
 syntax
   "_SepReplace"  :: "[i, pttrn, i, o] \<Rightarrow> i"  ("(1{_ ../ _ \<in> _, _})")
 translations
   "{b .. x\<in>A, Q}" => "CONST SepReplace(A, \<lambda>x. b, \<lambda>x. Q)"
 
 lemma Sep_and_Replace: "{b(x) .. x\<in>A, P(x) } = {b(x) . x\<in>{y\<in>A. P(y)}}"
   by (auto simp add:SepReplace_def)
 
 lemma SepReplace_subset : "A\<subseteq>A'\<Longrightarrow> {b .. x\<in>A, Q}\<subseteq>{b .. x\<in>A', Q}"
   by (auto simp add:SepReplace_def)
 
 lemma SepReplace_iff [simp]: "y\<in>{b(x) .. x\<in>A, P(x)} \<longleftrightarrow> (\<exists>x\<in>A. y=b(x) & P(x))"
   by (auto simp add:SepReplace_def)
 
 lemma SepReplace_dom_implies :
   "(\<And> x . x \<in>A \<Longrightarrow> b(x) = b'(x))\<Longrightarrow> {b(x) .. x\<in>A, Q(x)}={b'(x) .. x\<in>A, Q(x)}"
   by  (simp add:SepReplace_def)
 
 lemma SepReplace_pred_implies :
   "\<forall>x. Q(x)\<longrightarrow> b(x) = b'(x)\<Longrightarrow> {b(x) .. x\<in>A, Q(x)}={b'(x) .. x\<in>A, Q(x)}"
   by  (force simp add:SepReplace_def)
 
 subsection\<open>The well-founded relation \<^term>\<open>ed\<close>\<close>
 
 lemma eclose_sing : "x \<in> eclose(a) \<Longrightarrow> x \<in> eclose({a})"
   by(rule subsetD[OF mem_eclose_subset],simp+)
 
 lemma ecloseE :
   assumes  "x \<in> eclose(A)"
   shows  "x \<in> A \<or> (\<exists> B \<in> A . x \<in> eclose(B))"
   using assms
 proof (induct rule:eclose_induct_down)
   case (1 y)
   then
   show ?case
     using arg_into_eclose by auto
 next
   case (2 y z)
   from \<open>y \<in> A \<or> (\<exists>B\<in>A. y \<in> eclose(B))\<close>
   consider (inA) "y \<in> A" | (exB) "(\<exists>B\<in>A. y \<in> eclose(B))"
     by auto
   then show ?case
   proof (cases)
     case inA
     then
     show ?thesis using 2 arg_into_eclose by auto
   next
     case exB
     then obtain B where "y \<in> eclose(B)" "B\<in>A"
       by auto
     then
     show ?thesis using 2 ecloseD[of y B z] by auto
   qed
 qed
 
 lemma eclose_singE : "x \<in> eclose({a}) \<Longrightarrow> x = a \<or> x \<in> eclose(a)"
   by(blast dest: ecloseE)
 
 lemma in_eclose_sing :
   assumes "x \<in> eclose({a})" "a \<in> eclose(z)"
   shows "x \<in> eclose({z})"
 proof -
   from \<open>x\<in>eclose({a})\<close>
   consider (eq) "x=a" | (lt) "x\<in>eclose(a)"
     using eclose_singE by auto
   then
   show ?thesis
     using eclose_sing mem_eclose_trans assms
     by (cases, auto)
 qed
 
 lemma in_dom_in_eclose :
   assumes "x \<in> domain(z)"
   shows "x \<in> eclose(z)"
 proof -
   from assms
   obtain y where "\<langle>x,y\<rangle> \<in> z"
     unfolding domain_def by auto
   then
   show ?thesis
     unfolding Pair_def
     using ecloseD[of "{x,x}"] ecloseD[of "{{x,x},{x,y}}"] arg_into_eclose
     by auto
 qed
 
 text\<open>term\<open>ed\<close> is the well-founded relation on which \<^term>\<open>val\<close> is defined.\<close>
 definition
   ed :: "[i,i] \<Rightarrow> o" where
   "ed(x,y) \<equiv> x \<in> domain(y)"
 
 definition
   edrel :: "i \<Rightarrow> i" where
   "edrel(A) \<equiv> Rrel(ed,A)"
 
 
 lemma edI[intro!]: "t\<in>domain(x) \<Longrightarrow> ed(t,x)"
   unfolding ed_def .
 
 lemma edD[dest!]: "ed(t,x) \<Longrightarrow> t\<in>domain(x)"
   unfolding ed_def .
 
 
 lemma rank_ed:
   assumes "ed(y,x)"
   shows "succ(rank(y)) \<le> rank(x)"
 proof
   from assms
   obtain p where "\<langle>y,p\<rangle>\<in>x" by auto
   moreover
   obtain s where "y\<in>s" "s\<in>\<langle>y,p\<rangle>" unfolding Pair_def by auto
   ultimately
   have "rank(y) < rank(s)" "rank(s) < rank(\<langle>y,p\<rangle>)" "rank(\<langle>y,p\<rangle>) < rank(x)"
     using rank_lt by blast+
   then
   show "rank(y) < rank(x)"
     using lt_trans by blast
 qed
 
 lemma edrel_dest [dest]: "x \<in> edrel(A) \<Longrightarrow> \<exists> a\<in> A. \<exists> b \<in> A. x =\<langle>a,b\<rangle>"
   by(auto simp add:ed_def edrel_def Rrel_def)
 
 lemma edrelD : "x \<in> edrel(A) \<Longrightarrow> \<exists> a\<in> A. \<exists> b \<in> A. x =\<langle>a,b\<rangle> \<and> a \<in> domain(b)"
   by(auto simp add:ed_def edrel_def Rrel_def)
 
 lemma edrelI [intro!]: "x\<in>A \<Longrightarrow> y\<in>A \<Longrightarrow> x \<in> domain(y) \<Longrightarrow> \<langle>x,y\<rangle>\<in>edrel(A)"
   by (simp add:ed_def edrel_def Rrel_def)
 
 lemma edrel_trans: "Transset(A) \<Longrightarrow> y\<in>A \<Longrightarrow> x \<in> domain(y) \<Longrightarrow> \<langle>x,y\<rangle>\<in>edrel(A)"
   by (rule edrelI, auto simp add:Transset_def domain_def Pair_def)
 
 lemma domain_trans: "Transset(A) \<Longrightarrow> y\<in>A \<Longrightarrow> x \<in> domain(y) \<Longrightarrow> x\<in>A"
   by (auto simp add: Transset_def domain_def Pair_def)
 
 lemma relation_edrel : "relation(edrel(A))"
   by(auto simp add: relation_def)
 
 lemma field_edrel : "field(edrel(A))\<subseteq>A"
   by blast
 
 lemma edrel_sub_memrel: "edrel(A) \<subseteq> trancl(Memrel(eclose(A)))"
 proof
   fix z
   assume
     "z\<in>edrel(A)"
   then obtain x y where
     Eq1:   "x\<in>A" "y\<in>A" "z=\<langle>x,y\<rangle>" "x\<in>domain(y)"
     using edrelD
     by blast
   then obtain u v where
     Eq2:   "x\<in>u" "u\<in>v" "v\<in>y"
     unfolding domain_def Pair_def by auto
   with Eq1 have
     Eq3:   "x\<in>eclose(A)" "y\<in>eclose(A)" "u\<in>eclose(A)" "v\<in>eclose(A)"
     by (auto, rule_tac [3-4] ecloseD, rule_tac [3] ecloseD, simp_all add:arg_into_eclose)
   let
     ?r="trancl(Memrel(eclose(A)))"
   from Eq2 and Eq3 have
     "\<langle>x,u\<rangle>\<in>?r" "\<langle>u,v\<rangle>\<in>?r" "\<langle>v,y\<rangle>\<in>?r"
     by (auto simp add: r_into_trancl)
   then  have
     "\<langle>x,y\<rangle>\<in>?r"
     by (rule_tac trancl_trans, rule_tac [2] trancl_trans, simp)
   with Eq1 show "z\<in>?r" by simp
 qed
 
 lemma wf_edrel : "wf(edrel(A))"
   using wf_subset [of "trancl(Memrel(eclose(A)))"] edrel_sub_memrel
     wf_trancl wf_Memrel
   by auto
 
 lemma ed_induction:
   assumes "\<And>x. \<lbrakk>\<And>y.  ed(y,x) \<Longrightarrow> Q(y) \<rbrakk> \<Longrightarrow> Q(x)"
   shows "Q(a)"
 proof(induct rule: wf_induct2[OF wf_edrel[of "eclose({a})"] ,of a "eclose({a})"])
   case 1
   then show ?case using arg_into_eclose by simp
 next
   case 2
   then show ?case using field_edrel .
 next
   case (3 x)
   then
   show ?case
     using assms[of x] edrelI domain_trans[OF Transset_eclose 3(1)] by blast
 qed
 
 lemma dom_under_edrel_eclose: "edrel(eclose({x})) -`` {x} = domain(x)"
 proof
   show "edrel(eclose({x})) -`` {x} \<subseteq> domain(x)"
     unfolding edrel_def Rrel_def ed_def
     by auto
 next
   show "domain(x) \<subseteq> edrel(eclose({x})) -`` {x}"
     unfolding edrel_def Rrel_def
     using in_dom_in_eclose eclose_sing arg_into_eclose
     by blast
 qed
 
 lemma ed_eclose : "\<langle>y,z\<rangle> \<in> edrel(A) \<Longrightarrow> y \<in> eclose(z)"
   by(drule edrelD,auto simp add:domain_def in_dom_in_eclose)
 
 lemma tr_edrel_eclose : "\<langle>y,z\<rangle> \<in> edrel(eclose({x}))^+ \<Longrightarrow> y \<in> eclose(z)"
   by(rule trancl_induct,(simp add: ed_eclose mem_eclose_trans)+)
 
 
 lemma restrict_edrel_eq :
   assumes "z \<in> domain(x)"
   shows "edrel(eclose({x})) \<inter> eclose({z})\<times>eclose({z}) = edrel(eclose({z}))"
 proof(intro equalityI subsetI)
   let ?ec="\<lambda> y . edrel(eclose({y}))"
   let ?ez="eclose({z})"
   let ?rr="?ec(x) \<inter> ?ez \<times> ?ez"
   fix y
   assume yr:"y \<in> ?rr"
   with yr obtain a b where 1:"\<langle>a,b\<rangle> \<in> ?rr" "a \<in> ?ez" "b \<in> ?ez" "\<langle>a,b\<rangle> \<in> ?ec(x)" "y=\<langle>a,b\<rangle>"
     by blast
   moreover
   from this
   have "a \<in> domain(b)" using edrelD by blast
   ultimately
   show "y \<in> edrel(eclose({z}))" by blast
 next
   let ?ec="\<lambda> y . edrel(eclose({y}))"
   let ?ez="eclose({z})"
   let ?rr="?ec(x) \<inter> ?ez \<times> ?ez"
   fix y
   assume yr:"y \<in> edrel(?ez)"
   then obtain a b where "a \<in> ?ez" "b \<in> ?ez" "y=\<langle>a,b\<rangle>" "a \<in> domain(b)"
     using edrelD by blast
   moreover
   from this assms
   have "z \<in> eclose(x)" using in_dom_in_eclose by simp
   moreover
   from assms calculation
   have "a \<in> eclose({x})" "b \<in> eclose({x})" using in_eclose_sing by simp_all
   moreover
   from this \<open>a\<in>domain(b)\<close>
   have "\<langle>a,b\<rangle> \<in> edrel(eclose({x}))" by blast
   ultimately
   show "y \<in> ?rr" by simp
 qed
 
 lemma tr_edrel_subset :
   assumes "z \<in> domain(x)"
   shows   "tr_down(edrel(eclose({x})),z) \<subseteq> eclose({z})"
 proof(intro subsetI)
   let ?r="\<lambda> x . edrel(eclose({x}))"
   fix y
   assume  "y \<in> tr_down(?r(x),z)"
   then
   have "\<langle>y,z\<rangle> \<in> ?r(x)^+" using tr_downD by simp
   with assms
   show "y \<in> eclose({z})" using tr_edrel_eclose eclose_sing by simp
 qed
 
 
 context M_ctm
 begin
 
 lemma upairM : "x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> {x,y} \<in> M"
   by (simp flip: setclass_iff)
 
 lemma singletonM : "a \<in> M \<Longrightarrow> {a} \<in> M"
   by (simp flip: setclass_iff)
 
 lemma Rep_simp : "Replace(u,\<lambda> y z . z = f(y)) = { f(y) . y \<in> u}"
   by(auto)
 
 end (* M_ctm *)
 
 subsection\<open>Values and check-names\<close>
 context forcing_data
 begin
 
 definition
   Hcheck :: "[i,i] \<Rightarrow> i" where
   "Hcheck(z,f)  \<equiv> { \<langle>f`y,one\<rangle> . y \<in> z}"
 
 definition
   check :: "i \<Rightarrow> i" where
   "check(x) \<equiv> transrec(x , Hcheck)"
 
 lemma checkD:
   "check(x) =  wfrec(Memrel(eclose({x})), x, Hcheck)"
   unfolding check_def transrec_def ..
 
 definition
   rcheck :: "i \<Rightarrow> i" where
   "rcheck(x) \<equiv> Memrel(eclose({x}))^+"
 
 
 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
 
 (* relation of check is in M *)
 lemma rcheck_in_M :
   "x \<in> M \<Longrightarrow> rcheck(x) \<in> M"
   unfolding rcheck_def by (simp flip: setclass_iff)
 
 
 lemma  aux_def_check: "x \<in> y \<Longrightarrow>
   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) = { \<langle>check(w),one\<rangle> . w \<in> y}"
 proof -
   let
     ?r="\<lambda>y. Memrel(eclose({y}))"
   have wfr:   "\<forall>w . wf(?r(w))" 
     using wf_Memrel ..
   then 
   have "check(y)= Hcheck( y, \<lambda>x\<in>?r(y) -`` {y}. wfrec(?r(y), x, Hcheck))"
     using wfrec[of "?r(y)" y "Hcheck"] checkD by simp
   also 
   have " ... = Hcheck( y, \<lambda>x\<in>y. wfrec(?r(y), x, Hcheck))"
     using under_Memrel_eclose arg_into_eclose by simp
   also 
   have " ... = Hcheck( y, \<lambda>x\<in>y. 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 \<in> nat"
   shows "check(succ(n)) = check(n) \<union> {\<langle>check(n),one\<rangle>}"
 proof -
   have "check(succ(n)) = {\<langle>check(i),one\<rangle> . i \<in> succ(n)} "
     using def_check by blast
   also have "... = {\<langle>check(i),one\<rangle> . i \<in> n} \<union> {\<langle>check(n),one\<rangle>}"
     by blast
   also have "... = check(n) \<union> {\<langle>check(n),one\<rangle>}"
     using def_check[of n,symmetric] by simp
   finally show ?thesis .
 qed
 
 lemma field_Memrel2 :
   assumes "x \<in> M"
   shows "field(Memrel(eclose({x}))) \<subseteq> M"
 proof -
   have "field(Memrel(eclose({x}))) \<subseteq> eclose({x})" "eclose({x}) \<subseteq> 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
 
 definition
   Hv :: "i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i" where
   "Hv(G,x,f) \<equiv> { f`y .. y\<in> domain(x), \<exists>p\<in>P. \<langle>y,p\<rangle> \<in> x \<and> p \<in> G }"
 
 text\<open>The funcion \<^term>\<open>val\<close> interprets a name in \<^term>\<open>M\<close>
 according to a (generic) filter \<^term>\<open>G\<close>. Note the definition
 in terms of the well-founded recursor.\<close>
 
 definition
   val :: "i\<Rightarrow>i\<Rightarrow>i" where
   "val(G,\<tau>) \<equiv> wfrec(edrel(eclose({\<tau>})), \<tau> ,Hv(G))"
 
 lemma aux_def_val:
   assumes "z \<in> domain(x)"
   shows "wfrec(edrel(eclose({x})),z,Hv(G)) = wfrec(edrel(eclose({z})),z,Hv(G))"
 proof -
   let ?r="\<lambda>x . edrel(eclose({x}))"
   have "z\<in>eclose({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) \<subseteq> 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 \<open>z\<in>domain(x)\<close>
   have "... = wfrec(?r(z),z,Hv(G))"
     using restrict_edrel_eq wfrec_restr_eq by simp
   finally show ?thesis .
 qed
 
 text\<open>The next lemma provides the usual recursive expresion for the definition of term\<open>val\<close>.\<close>
 
 lemma def_val:  "val(G,x) = {val(G,t) .. t\<in>domain(x) , \<exists>p\<in>P .  \<langle>t,p\<rangle>\<in>x \<and> p \<in> G }"
 proof -
   let
     ?r="\<lambda>\<tau> . edrel(eclose({\<tau>}))"
   let
     ?f="\<lambda>z\<in>?r(x)-``{x}. wfrec(?r(x),z,Hv(G))"
   have "\<forall>\<tau>. wf(?r(\<tau>))" 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,\<lambda>z\<in>domain(x). wfrec(?r(x),z,Hv(G)))"
     using dom_under_edrel_eclose by simp
   also
   have " ... = Hv(G,x,\<lambda>z\<in>domain(x). val(G,z))"
     using aux_def_val val_def by simp
   finally
   show ?thesis using Hv_def SepReplace_def by simp
 qed
 
 lemma val_mono : "x\<subseteq>y \<Longrightarrow> val(G,x) \<subseteq> val(G,y)"
   by (subst (1 2) def_val, force)
 
 text\<open>Check-names are the canonical names for elements of the
 ground model. Here we show that this is the case.\<close>
 
 lemma valcheck : "one \<in> G \<Longrightarrow>  one \<in> P \<Longrightarrow> val(G,check(y))  = y"
 proof (induct rule:eps_induct)
   case (1 y)
   then show ?case
   proof -    
     have "check(y) = { \<langle>check(w), one\<rangle> . w \<in> y}"  (is "_ = ?C") 
       using def_check .
     then
     have "val(G,check(y)) = val(G, {\<langle>check(w), one\<rangle> . w \<in> y})"
       by simp
     also
     have " ...  = {val(G,t) .. t\<in>domain(?C) , \<exists>p\<in>P .  \<langle>t, p\<rangle>\<in>?C \<and> p \<in> G }"
       using def_val by blast
     also
     have " ... =  {val(G,t) .. t\<in>domain(?C) , \<exists>w\<in>y. t=check(w) }"
       using 1 by simp
     also
     have " ... = {val(G,check(w)) . w\<in>y }"
       by force
     finally
     show "val(G,check(y)) = y"
       using 1 by simp
   qed
 qed
 
 lemma val_of_name :
   "val(G,{x\<in>A\<times>P. Q(x)}) = {val(G,t) .. t\<in>A , \<exists>p\<in>P .  Q(\<langle>t,p\<rangle>) \<and> p \<in> G }"
 proof -
   let
     ?n="{x\<in>A\<times>P. Q(x)}" and
     ?r="\<lambda>\<tau> . edrel(eclose({\<tau>}))"
   let
     ?f="\<lambda>z\<in>?r(?n)-``{?n}. val(G,z)"
   have
     wfR : "wf(?r(\<tau>))" for \<tau>
     by (simp add: wf_edrel)
   have "domain(?n) \<subseteq> A" by auto
   { fix t
     assume H:"t \<in> domain({x \<in> A \<times> P . Q(x)})"
     then have "?f ` t = (if t \<in> ?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 \<in> domain({x \<in> A \<times> P . Q(x)}) \<Longrightarrow> val(G,t) = ?f` t"  for t
     by simp
   have "val(G,?n) = {val(G,t) .. t\<in>domain(?n), \<exists>p \<in> P . \<langle>t,p\<rangle> \<in> ?n \<and> p \<in> G}"
     by (subst def_val,simp)
   also
   have "... = {?f`t .. t\<in>domain(?n), \<exists>p\<in>P . \<langle>t,p\<rangle>\<in>?n \<and> p\<in>G}"
     unfolding Hv_def
     by (subst SepReplace_dom_implies,auto simp add:Eq1)
   also
   have  "... = { (if t\<in>?r(?n)-``{?n} then val(G,t) else 0) .. t\<in>domain(?n), \<exists>p\<in>P . \<langle>t,p\<rangle>\<in>?n \<and> p\<in>G}"
     by (simp)
   also
   have Eq2:  "... = { val(G,t) .. t\<in>domain(?n), \<exists>p\<in>P . \<langle>t,p\<rangle>\<in>?n \<and> p\<in>G}"
   proof -
     have "domain(?n) \<subseteq> ?r(?n)-``{?n}"
       using dom_under_edrel_eclose by simp
     then
     have "\<forall>t\<in>domain(?n). (if t\<in>?r(?n)-``{?n} then val(G,t) else 0) = val(G,t)"
       by auto
     then
     show "{ (if t\<in>?r(?n)-``{?n} then val(G,t) else 0) .. t\<in>domain(?n), \<exists>p\<in>P . \<langle>t,p\<rangle>\<in>?n \<and> p\<in>G} =
           { val(G,t) .. t\<in>domain(?n), \<exists>p\<in>P . \<langle>t,p\<rangle>\<in>?n \<and> p\<in>G}"
       by auto
   qed
   also
   have " ... = { val(G,t) .. t\<in>A, \<exists>p\<in>P . \<langle>t,p\<rangle>\<in>?n \<and> p\<in>G}"
     by force
   finally
   show " val(G,?n)  = { val(G,t) .. t\<in>A, \<exists>p\<in>P . Q(\<langle>t,p\<rangle>) \<and> p\<in>G}"
     by auto
 qed
 
 lemma val_of_name_alt :
   "val(G,{x\<in>A\<times>P. Q(x)}) = {val(G,t) .. t\<in>A , \<exists>p\<in>P\<inter>G .  Q(\<langle>t,p\<rangle>) }"
   using val_of_name by force
 
 lemma val_only_names: "val(F,\<tau>) = val(F,{x\<in>\<tau>. \<exists>t\<in>domain(\<tau>). \<exists>p\<in>P. x=\<langle>t,p\<rangle>})"
   (is "_ = val(F,?name)")
 proof -
   have "val(F,?name) = {val(F, t).. t\<in>domain(?name), \<exists>p\<in>P. \<langle>t, p\<rangle> \<in> ?name \<and> p \<in> F}"
     using def_val by blast
   also
   have " ... = {val(F, t). t\<in>{y\<in>domain(?name). \<exists>p\<in>P. \<langle>y, p\<rangle> \<in> ?name \<and> p \<in> F}}"
     using Sep_and_Replace by simp
   also
   have " ... = {val(F, t). t\<in>{y\<in>domain(\<tau>). \<exists>p\<in>P. \<langle>y, p\<rangle> \<in> \<tau> \<and> p \<in> F}}"
     by blast
   also
   have " ... = {val(F, t).. t\<in>domain(\<tau>), \<exists>p\<in>P. \<langle>t, p\<rangle> \<in> \<tau> \<and> p \<in> F}"
     using Sep_and_Replace by simp
   also
   have " ... = val(F, \<tau>)"
     using def_val[symmetric] by blast
   finally
   show ?thesis ..
 qed
 
 lemma val_only_pairs: "val(F,\<tau>) = val(F,{x\<in>\<tau>. \<exists>t p. x=\<langle>t,p\<rangle>})"
 proof
   have "val(F,\<tau>) = val(F,{x\<in>\<tau>. \<exists>t\<in>domain(\<tau>). \<exists>p\<in>P. x=\<langle>t,p\<rangle>})"
     (is "_ = val(F,?name)")
     using val_only_names .
   also
   have "... \<subseteq> val(F,{x\<in>\<tau>. \<exists>t p. x=\<langle>t,p\<rangle>})"
     using val_mono[of ?name "{x\<in>\<tau>. \<exists>t p. x=\<langle>t,p\<rangle>}"] by auto
   finally
   show "val(F,\<tau>) \<subseteq> val(F,{x\<in>\<tau>. \<exists>t p. x=\<langle>t,p\<rangle>})" by simp
 next
   show "val(F,{x\<in>\<tau>. \<exists>t p. x=\<langle>t,p\<rangle>}) \<subseteq> val(F,\<tau>)"
     using val_mono[of "{x\<in>\<tau>. \<exists>t p. x=\<langle>t,p\<rangle>}"] by auto
 qed
 
 lemma val_subset_domain_times_range: "val(F,\<tau>) \<subseteq> val(F,domain(\<tau>)\<times>range(\<tau>))"
   using val_only_pairs[THEN equalityD1]
     val_mono[of "{x \<in> \<tau> . \<exists>t p. x = \<langle>t, p\<rangle>}" "domain(\<tau>)\<times>range(\<tau>)"] by blast
 
 lemma val_subset_domain_times_P: "val(F,\<tau>) \<subseteq> val(F,domain(\<tau>)\<times>P)"
   using val_only_names[of F \<tau>] val_mono[of "{x\<in>\<tau>. \<exists>t\<in>domain(\<tau>). \<exists>p\<in>P. x=\<langle>t,p\<rangle>}" "domain(\<tau>)\<times>P" F]
   by auto
 
 definition
   GenExt :: "i\<Rightarrow>i"     ("M[_]")
   where "GenExt(G)\<equiv> {val(G,\<tau>). \<tau> \<in> M}"
 
 
 lemma val_of_elem: "\<langle>\<theta>,p\<rangle> \<in> \<pi> \<Longrightarrow> p\<in>G \<Longrightarrow> p\<in>P \<Longrightarrow> val(G,\<theta>) \<in> val(G,\<pi>)"
 proof -
   assume
     "\<langle>\<theta>,p\<rangle> \<in> \<pi>"
   then
   have "\<theta>\<in>domain(\<pi>)" by auto
   assume "p\<in>G" "p\<in>P"
   with \<open>\<theta>\<in>domain(\<pi>)\<close> \<open>\<langle>\<theta>,p\<rangle> \<in> \<pi>\<close>
   have "val(G,\<theta>) \<in> {val(G,t) .. t\<in>domain(\<pi>) , \<exists>p\<in>P .  \<langle>t, p\<rangle>\<in>\<pi> \<and> p \<in> G }"
     by auto
   then
   show ?thesis by (subst def_val)
 qed
 
 lemma elem_of_val: "x\<in>val(G,\<pi>) \<Longrightarrow> \<exists>\<theta>\<in>domain(\<pi>). val(G,\<theta>) = x"
   by (subst (asm) def_val,auto)
 
 lemma elem_of_val_pair: "x\<in>val(G,\<pi>) \<Longrightarrow> \<exists>\<theta>. \<exists>p\<in>G.  \<langle>\<theta>,p\<rangle>\<in>\<pi> \<and> val(G,\<theta>) = x"
   by (subst (asm) def_val,auto)
 
 lemma elem_of_val_pair':
   assumes "\<pi>\<in>M" "x\<in>val(G,\<pi>)"
   shows "\<exists>\<theta>\<in>M. \<exists>p\<in>G.  \<langle>\<theta>,p\<rangle>\<in>\<pi> \<and> val(G,\<theta>) = x"
 proof -
   from assms
   obtain \<theta> p where "p\<in>G" "\<langle>\<theta>,p\<rangle>\<in>\<pi>" "val(G,\<theta>) = x"
     using elem_of_val_pair by blast
   moreover from this \<open>\<pi>\<in>M\<close>
   have "\<theta>\<in>M"
     using pair_in_M_iff[THEN iffD1, THEN conjunct1, simplified]
       transitivity by blast
   ultimately
   show ?thesis by blast
 qed
 
 
 lemma GenExtD:
   "x \<in> M[G] \<Longrightarrow> \<exists>\<tau>\<in>M. x = val(G,\<tau>)"
   by (simp add:GenExt_def)
 
 lemma GenExtI:
   "x \<in> M \<Longrightarrow> val(G,x) \<in> M[G]"
   by (auto simp add: GenExt_def)
 
 lemma Transset_MG : "Transset(M[G])"
 proof -
   { fix vc y
     assume "vc \<in> M[G]" and "y \<in> vc"
     then obtain c where "c\<in>M" "val(G,c)\<in>M[G]" "y \<in> val(G,c)"
       using GenExtD by auto
     from \<open>y \<in> val(G,c)\<close>
     obtain \<theta> where "\<theta>\<in>domain(c)" "val(G,\<theta>) = y"
       using elem_of_val by blast
     with trans_M \<open>c\<in>M\<close>
     have "y \<in> 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]
 
 lemma check_n_M :
   fixes n
   assumes "n \<in> nat"
   shows "check(n) \<in> M"
   using \<open>n\<in>nat\<close>
 proof (induct n)
   case 0
   then show ?case using zero_in_M by (subst def_check,simp)
 next
   case (succ x)
   have "one \<in> M" using one_in_P P_sub_M subsetD by simp
   with \<open>check(x)\<in>M\<close>
   have "\<langle>check(x),one\<rangle> \<in> M"
     using tuples_in_M by simp
   then
   have "{\<langle>check(x),one\<rangle>} \<in> M"
     using singletonM by simp
   with \<open>check(x)\<in>M\<close>
   have "check(x) \<union> {\<langle>check(x),one\<rangle>} \<in> M"
     using Un_closed by simp
   then show ?case using \<open>x\<in>nat\<close> def_checkS by simp
 qed
 
 
 definition
   PHcheck :: "[i,i,i,i] \<Rightarrow> o" where
   "PHcheck(o,f,y,p) \<equiv> p\<in>M \<and> (\<exists>fy[##M]. fun_apply(##M,f,y,fy) \<and> pair(##M,fy,o,p))"
 
 definition
   is_Hcheck :: "[i,i,i,i] \<Rightarrow> o" where
   "is_Hcheck(o,z,f,hc)  \<equiv> is_Replace(##M,z,PHcheck(o,f),hc)"
 
 lemma one_in_M: "one \<in> M"
   by (insert one_in_P P_in_M, simp add: transitivity)
 
 lemma def_PHcheck:
   assumes
     "z\<in>M" "f\<in>M"
   shows
     "Hcheck(z,f) = Replace(z,PHcheck(one,f))"
 proof -
   from assms
   have "\<langle>f`x,one\<rangle> \<in> M" "f`x\<in>M" if "x\<in>z" for x
     using tuples_in_M one_in_M transitivity that apply_closed by simp_all
   then
   have "{y . x \<in> z, y = \<langle>f ` x, one\<rangle>} =  {y . x \<in> z, y = \<langle>f ` x, one\<rangle> \<and> y\<in>M \<and> f`x\<in>M}"
     by simp
   then
   show ?thesis
     using \<open>z\<in>M\<close> \<open>f\<in>M\<close> transitivity
     unfolding Hcheck_def PHcheck_def RepFun_def
     by auto
 qed
 
 (*
   "PHcheck(o,f,y,p) \<equiv> \<exists>fy[##M]. fun_apply(##M,f,y,fy) \<and> pair(##M,fy,o,p)"
 *)
 definition
   PHcheck_fm :: "[i,i,i,i] \<Rightarrow> i" where
   "PHcheck_fm(o,f,y,p) \<equiv> Exists(And(fun_apply_fm(succ(f),succ(y),0)
                                  ,pair_fm(0,succ(o),succ(p))))"
 
 lemma PHcheck_type [TC]:
   "\<lbrakk> x \<in> nat; y \<in> nat; z \<in> nat; u \<in> nat \<rbrakk> \<Longrightarrow> PHcheck_fm(x,y,z,u) \<in> formula"
   by (simp add:PHcheck_fm_def)
 
 lemma sats_PHcheck_fm [simp]:
   "\<lbrakk> x \<in> nat; y \<in> nat; z \<in> nat; u \<in> nat ; env \<in> list(M)\<rbrakk>
     \<Longrightarrow> sats(M,PHcheck_fm(x,y,z,u),env) \<longleftrightarrow>
         PHcheck(nth(x,env),nth(y,env),nth(z,env),nth(u,env))"
   using zero_in_M Internalizations.nth_closed by (simp add: PHcheck_def PHcheck_fm_def)
 
 (*
   "is_Hcheck(o,z,f,hc)  \<equiv> is_Replace(##M,z,PHcheck(o,f),hc)"
 *)
 definition
   is_Hcheck_fm :: "[i,i,i,i] \<Rightarrow> i" where
   "is_Hcheck_fm(o,z,f,hc) \<equiv> Replace_fm(z,PHcheck_fm(succ(succ(o)),succ(succ(f)),0,1),hc)"
 
 lemma is_Hcheck_type [TC]:
   "\<lbrakk> x \<in> nat; y \<in> nat; z \<in> nat; u \<in> nat \<rbrakk> \<Longrightarrow> is_Hcheck_fm(x,y,z,u) \<in> formula"
   by (simp add:is_Hcheck_fm_def)
 
 lemma sats_is_Hcheck_fm [simp]:
   "\<lbrakk> x \<in> nat; y \<in> nat; z \<in> nat; u \<in> nat ; env \<in> list(M)\<rbrakk>
     \<Longrightarrow> sats(M,is_Hcheck_fm(x,y,z,u),env) \<longleftrightarrow>
         is_Hcheck(nth(x,env),nth(y,env),nth(z,env),nth(u,env))"
   using sats_Replace_fm unfolding is_Hcheck_def is_Hcheck_fm_def
   by simp
 
 
 (* instance of replacement for hcheck *)
 lemma wfrec_Hcheck :
   assumes
     "X\<in>M"
   shows
     "wfrec_replacement(##M,is_Hcheck(one),rcheck(X))"
 proof -
   have "is_Hcheck(one,a,b,c) \<longleftrightarrow>
         sats(M,is_Hcheck_fm(8,2,1,0),[c,b,a,d,e,y,x,z,one,rcheck(x)])"
     if "a\<in>M" "b\<in>M" "c\<in>M" "d\<in>M" "e\<in>M" "y\<in>M" "x\<in>M" "z\<in>M"
     for a b c d e y x z
     using that one_in_M \<open>X\<in>M\<close> rcheck_in_M by simp
   then have 1:"sats(M,is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0),
                     [y,x,z,one,rcheck(X)]) \<longleftrightarrow>
             is_wfrec(##M, is_Hcheck(one),rcheck(X), x, y)"
     if "x\<in>M" "y\<in>M" "z\<in>M" for x y z
     using  that sats_is_wfrec_fm \<open>X\<in>M\<close> rcheck_in_M one_in_M by simp
   let
     ?f="Exists(And(pair_fm(1,0,2),
                is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0)))"
   have satsf:"sats(M, ?f, [x,z,one,rcheck(X)]) \<longleftrightarrow>
               (\<exists>y\<in>M. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(one),rcheck(X), x, y))"
     if "x\<in>M" "z\<in>M" for x z
     using that 1 \<open>X\<in>M\<close> rcheck_in_M one_in_M by (simp del:pair_abs)
   have artyf:"arity(?f) = 4"
     unfolding is_wfrec_fm_def is_Hcheck_fm_def Replace_fm_def PHcheck_fm_def
       pair_fm_def upair_fm_def is_recfun_fm_def fun_apply_fm_def big_union_fm_def
       pre_image_fm_def restriction_fm_def image_fm_def
     by (simp add:nat_simp_union)
   then
   have "strong_replacement(##M,\<lambda>x z. sats(M,?f,[x,z,one,rcheck(X)]))"
     using replacement_ax 1 artyf \<open>X\<in>M\<close> rcheck_in_M one_in_M by simp
   then
   have "strong_replacement(##M,\<lambda>x z.
           \<exists>y\<in>M. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(one),rcheck(X), x, y))"
     using repl_sats[of M ?f "[one,rcheck(X)]"] satsf by (simp del:pair_abs)
   then
   show ?thesis unfolding wfrec_replacement_def by simp
 qed
 
 lemma repl_PHcheck :
   assumes
     "f\<in>M"
   shows
     "strong_replacement(##M,PHcheck(one,f))"
 proof -
   have "arity(PHcheck_fm(2,3,0,1)) = 4"
     unfolding PHcheck_fm_def fun_apply_fm_def big_union_fm_def pair_fm_def image_fm_def
       upair_fm_def
     by (simp add:nat_simp_union)
   with \<open>f\<in>M\<close>
   have "strong_replacement(##M,\<lambda>x y. sats(M,PHcheck_fm(2,3,0,1),[x,y,one,f]))"
     using replacement_ax one_in_M by simp
   with \<open>f\<in>M\<close>
   show ?thesis using one_in_M unfolding strong_replacement_def univalent_def by simp
 qed
 
 lemma univ_PHcheck : "\<lbrakk> z\<in>M ; f\<in>M \<rbrakk> \<Longrightarrow> univalent(##M,z,PHcheck(one,f))"
   unfolding univalent_def PHcheck_def by simp
 
 lemma relation2_Hcheck :
   "relation2(##M,is_Hcheck(one),Hcheck)"
 proof -
   have 1:"\<lbrakk>x\<in>z; PHcheck(one,f,x,y) \<rbrakk> \<Longrightarrow> (##M)(y)"
     if "z\<in>M" "f\<in>M" for z f x y
     using that unfolding PHcheck_def by simp
   have "is_Replace(##M,z,PHcheck(one,f),hc) \<longleftrightarrow> hc = Replace(z,PHcheck(one,f))"
     if "z\<in>M" "f\<in>M" "hc\<in>M" for z f hc
     using that Replace_abs[OF _ _ univ_PHcheck 1] by simp
   with def_PHcheck
   show ?thesis
     unfolding relation2_def is_Hcheck_def Hcheck_def by simp
 qed
 
 lemma PHcheck_closed :
   "\<lbrakk>z\<in>M ; f\<in>M ; x\<in>z; PHcheck(one,f,x,y) \<rbrakk> \<Longrightarrow> (##M)(y)"
   unfolding PHcheck_def by simp
 
 lemma Hcheck_closed :
   "\<forall>y\<in>M. \<forall>g\<in>M. function(g) \<longrightarrow> Hcheck(y,g)\<in>M"
 proof -
   have "Replace(y,PHcheck(one,f))\<in>M" if "f\<in>M" "y\<in>M" for f y
     using that repl_PHcheck  PHcheck_closed[of y f] univ_PHcheck
       strong_replacement_closed
     by (simp flip: setclass_iff)
   then show ?thesis using def_PHcheck by auto
 qed
 
 lemma wf_rcheck : "x\<in>M \<Longrightarrow> wf(rcheck(x))"
   unfolding rcheck_def using wf_trancl[OF wf_Memrel] .
 
 lemma trans_rcheck : "x\<in>M \<Longrightarrow> trans(rcheck(x))"
   unfolding rcheck_def using trans_trancl .
 
 lemma relation_rcheck : "x\<in>M \<Longrightarrow> relation(rcheck(x))"
   unfolding rcheck_def using relation_trancl .
 
 lemma check_in_M : "x\<in>M \<Longrightarrow> check(x) \<in> M"
   unfolding transrec_def
   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)" x "is_Hcheck(one)" Hcheck]
   by (simp flip: setclass_iff)
 
 end (* forcing_data *)
 
 (* check if this should go to Relative! *)
 definition
   is_singleton :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
   "is_singleton(A,x,z) \<equiv> \<exists>c[A]. empty(A,c) \<and> is_cons(A,x,c,z)"
 
 lemma (in M_trivial) singleton_abs[simp] : "\<lbrakk> M(x) ; M(s) \<rbrakk> \<Longrightarrow> is_singleton(M,x,s) \<longleftrightarrow> s = {x}"
   unfolding is_singleton_def using nonempty by simp
 
 definition
   singleton_fm :: "[i,i] \<Rightarrow> i" where
   "singleton_fm(i,j) \<equiv> Exists(And(empty_fm(0), cons_fm(succ(i),0,succ(j))))"
 
 lemma singleton_type[TC] : "\<lbrakk> x \<in> nat; y \<in> nat \<rbrakk> \<Longrightarrow> singleton_fm(x,y) \<in> formula"
   unfolding singleton_fm_def by simp
 
 lemma is_singleton_iff_sats:
   "\<lbrakk> nth(i,env) = x; nth(j,env) = y;
           i \<in> nat; j\<in>nat ; env \<in> list(A)\<rbrakk>
        \<Longrightarrow> is_singleton(##A,x,y) \<longleftrightarrow> sats(A, singleton_fm(i,j), env)"
   unfolding is_singleton_def singleton_fm_def by simp
 
 context forcing_data begin
 
 (* Internalization and absoluteness of rcheck *)
 definition
   is_rcheck :: "[i,i] \<Rightarrow> o" where
   "is_rcheck(x,z) \<equiv> \<exists>r\<in>M. tran_closure(##M,r,z) \<and> (\<exists>ec\<in>M. membership(##M,ec,r) \<and>
                            (\<exists>s\<in>M. is_singleton(##M,x,s) \<and>  is_eclose(##M,s,ec)))"
 
 lemma rcheck_abs :
   "\<lbrakk> x\<in>M ; r\<in>M \<rbrakk> \<Longrightarrow> is_rcheck(x,r) \<longleftrightarrow> r = rcheck(x)"
   unfolding rcheck_def is_rcheck_def
   using singletonM trancl_closed Memrel_closed eclose_closed by simp
 
 schematic_goal rcheck_fm_auto:
   assumes
     "i \<in> nat" "j \<in> nat" "env \<in> list(M)"
   shows
     "is_rcheck(nth(i,env),nth(j,env)) \<longleftrightarrow> sats(M,?rch(i,j),env)"
   unfolding is_rcheck_def
   by (insert assms ; (rule sep_rules is_singleton_iff_sats is_eclose_iff_sats
         trans_closure_fm_iff_sats | simp)+)
 
 synthesize "rcheck_fm" from_schematic rcheck_fm_auto
 
 definition
   is_check :: "[i,i] \<Rightarrow> o" where
   "is_check(x,z) \<equiv> \<exists>rch\<in>M. is_rcheck(x,rch) \<and> is_wfrec(##M,is_Hcheck(one),rch,x,z)"
 
 lemma check_abs :
   assumes
     "x\<in>M" "z\<in>M"
   shows
     "is_check(x,z) \<longleftrightarrow> z = check(x)"
 proof -
   have
     "is_check(x,z) \<longleftrightarrow> is_wfrec(##M,is_Hcheck(one),rcheck(x),x,z)"
     unfolding is_check_def using assms rcheck_abs rcheck_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(one)" Hcheck]
     by (simp flip: setclass_iff)
 qed
 
 (* \<exists>rch\<in>M. is_rcheck(x,rch) \<and> is_wfrec(##M,is_Hcheck(one),rch,x,z) *)
 definition
   check_fm :: "[i,i,i] \<Rightarrow> i" where
-  "check_fm(x,o,z) \<equiv> Exists(And(rcheck_fm(0,1#+x),
+  "check_fm(x,o,z) \<equiv> Exists(And(rcheck_fm(1#+x,0),
                       is_wfrec_fm(is_Hcheck_fm(6#+o,2,1,0),0,1#+x,1#+z)))"
 
 lemma check_fm_type[TC] :
   "\<lbrakk>x\<in>nat;o\<in>nat;z\<in>nat\<rbrakk> \<Longrightarrow> check_fm(x,o,z)\<in>formula"
   unfolding check_fm_def by simp
 
 lemma sats_check_fm :
   assumes
     "nth(o,env) = one" "x\<in>nat" "z\<in>nat" "o\<in>nat" "env\<in>list(M)" "x < length(env)" "z < length(env)"
   shows
     "sats(M, check_fm(x,o,z), env) \<longleftrightarrow> is_check(nth(x,env),nth(z,env))"
 proof -
   have sats_is_Hcheck_fm:
     "\<And>a0 a1 a2 a3 a4. \<lbrakk> a0\<in>M; a1\<in>M; a2\<in>M; a3\<in>M; a4\<in>M \<rbrakk> \<Longrightarrow>
          is_Hcheck(one,a2, a1, a0) \<longleftrightarrow>
          sats(M, is_Hcheck_fm(6#+o,2,1,0), [a0,a1,a2,a3,a4,r]@env)" if "r\<in>M" for r
     using that one_in_M assms  by simp
   then
   have "sats(M, is_wfrec_fm(is_Hcheck_fm(6#+o,2,1,0),0,1#+x,1#+z),Cons(r,env))
         \<longleftrightarrow> is_wfrec(##M,is_Hcheck(one),r,nth(x,env),nth(z,env))" if "r\<in>M" for r
     using that assms one_in_M sats_is_wfrec_fm by simp
   then
   show ?thesis unfolding is_check_def check_fm_def
     using assms rcheck_in_M one_in_M rcheck_fm_iff_sats[symmetric] by simp
 qed
 
 
 lemma check_replacement:
   "{check(x). x\<in>P} \<in> M"
 proof -
   have "arity(check_fm(0,2,1)) = 3"
     unfolding check_fm_def rcheck_fm_def trans_closure_fm_def is_eclose_fm_def mem_eclose_fm_def
       is_Hcheck_fm_def Replace_fm_def PHcheck_fm_def finite_ordinal_fm_def is_iterates_fm_def
       is_wfrec_fm_def is_recfun_fm_def restriction_fm_def pre_image_fm_def eclose_n_fm_def
       is_nat_case_fm_def quasinat_fm_def Memrel_fm_def singleton_fm_def fm_defs iterates_MH_fm_def
     by (simp add:nat_simp_union)
   moreover
   have "check(x)\<in>M" if "x\<in>P" for x
     using that Transset_intf[of M x P] trans_M check_in_M P_in_M by simp
   ultimately
   show ?thesis using sats_check_fm check_abs P_in_M check_in_M one_in_M
       Repl_in_M[of "check_fm(0,2,1)" "[one]" is_check check] by simp
 qed
 
 lemma pair_check : "\<lbrakk> p\<in>M ; y\<in>M \<rbrakk>  \<Longrightarrow> (\<exists>c\<in>M. is_check(p,c) \<and> pair(##M,c,p,y)) \<longleftrightarrow> y = \<langle>check(p),p\<rangle>"
   using check_abs check_in_M tuples_in_M by simp
 
 
 lemma M_subset_MG :  "one \<in> G \<Longrightarrow> M \<subseteq> M[G]"
   using check_in_M one_in_P GenExtI
   by (intro subsetI, subst valcheck [of G,symmetric], auto)
 
 text\<open>The name for the generic filter\<close>
 definition
   G_dot :: "i" where
   "G_dot \<equiv> {\<langle>check(p),p\<rangle> . p\<in>P}"
 
 lemma G_dot_in_M :
   "G_dot \<in> M"
 proof -
   let ?is_pcheck = "\<lambda>x y. \<exists>ch\<in>M. is_check(x,ch) \<and> pair(##M,ch,x,y)"
   let ?pcheck_fm = "Exists(And(check_fm(1,3,0),pair_fm(0,1,2)))"
   have "sats(M,?pcheck_fm,[x,y,one]) \<longleftrightarrow> ?is_pcheck(x,y)" if "x\<in>M" "y\<in>M" for x y
     using sats_check_fm that one_in_M by simp
   moreover
   have "?is_pcheck(x,y) \<longleftrightarrow> y = \<langle>check(x),x\<rangle>" if "x\<in>M" "y\<in>M" for x y
     using that check_abs check_in_M by simp
   moreover
   have "?pcheck_fm\<in>formula" by simp
   moreover
   have "arity(?pcheck_fm)=3"
     unfolding check_fm_def rcheck_fm_def trans_closure_fm_def is_eclose_fm_def mem_eclose_fm_def
       is_Hcheck_fm_def Replace_fm_def PHcheck_fm_def finite_ordinal_fm_def is_iterates_fm_def
       is_wfrec_fm_def is_recfun_fm_def restriction_fm_def pre_image_fm_def eclose_n_fm_def
       is_nat_case_fm_def quasinat_fm_def Memrel_fm_def singleton_fm_def fm_defs iterates_MH_fm_def
     by (simp add:nat_simp_union)
   moreover
   from P_in_M check_in_M tuples_in_M P_sub_M
   have "\<langle>check(p),p\<rangle> \<in> M" if "p\<in>P" for p
     using that by auto
   ultimately
   show ?thesis
     unfolding G_dot_def
     using one_in_M P_in_M Repl_in_M[of ?pcheck_fm "[one]"]
     by simp
 qed
 
 
 lemma val_G_dot :
   assumes "G \<subseteq> P"
     "one \<in> G"
   shows "val(G,G_dot) = G"
 proof (intro equalityI subsetI)
   fix x
   assume "x\<in>val(G,G_dot)"
   then obtain \<theta> p where "p\<in>G" "\<langle>\<theta>,p\<rangle> \<in> G_dot" "val(G,\<theta>) = x" "\<theta> = check(p)"
     unfolding G_dot_def using elem_of_val_pair G_dot_in_M
     by force
   with \<open>one\<in>G\<close> \<open>G\<subseteq>P\<close> show
     "x \<in> G"
     using valcheck P_sub_M by auto
 next
   fix p
   assume "p\<in>G"
   have "\<langle>check(q),q\<rangle> \<in> G_dot" if "q\<in>P" for q
     unfolding G_dot_def using that by simp
   with \<open>p\<in>G\<close> \<open>G\<subseteq>P\<close>
   have "val(G,check(p)) \<in> val(G,G_dot)"
     using val_of_elem G_dot_in_M by blast
   with \<open>p\<in>G\<close> \<open>G\<subseteq>P\<close> \<open>one\<in>G\<close>
   show "p \<in> val(G,G_dot)"
     using P_sub_M valcheck by auto
 qed
 
 
 lemma G_in_Gen_Ext :
   assumes "G \<subseteq> P" and "one \<in> G"
   shows   "G \<in> M[G]"
   using assms val_G_dot GenExtI[of _ G] G_dot_in_M
   by force
 
 (* Move this to M_trivial *)
 lemma fst_snd_closed: "p\<in>M \<Longrightarrow> fst(p) \<in> M \<and> snd(p)\<in> M"
 proof (cases "\<exists>a. \<exists>b. p = \<langle>a, b\<rangle>")
   case False
   then
   show "fst(p) \<in> M \<and> snd(p) \<in> M" unfolding fst_def snd_def using zero_in_M by auto
 next
   case True
   then
   obtain a b where "p = \<langle>a, b\<rangle>" by blast
   with True
   have "fst(p) = a" "snd(p) = b" unfolding fst_def snd_def by simp_all
   moreover
   assume "p\<in>M"
   moreover from this
   have "a\<in>M"
     unfolding \<open>p = _\<close> Pair_def by (force intro:Transset_M[OF trans_M])
   moreover from  \<open>p\<in>M\<close>
   have "b\<in>M"
     using Transset_M[OF trans_M, of "{a,b}" p] Transset_M[OF trans_M, of "b" "{a,b}"]
     unfolding \<open>p = _\<close> Pair_def by (simp)
   ultimately
   show ?thesis by simp
 qed
 
 end (* forcing_data *)
 
 locale G_generic = forcing_data +
   fixes G :: "i"
   assumes generic : "M_generic(G)"
 begin
 
 lemma zero_in_MG :
   "0 \<in> M[G]"
 proof -
   have "0 = val(G,0)"
     using zero_in_M elem_of_val by auto
   also 
   have "... \<in> M[G]"
     using GenExtI zero_in_M by simp
   finally show ?thesis .
 qed
 
 lemma G_nonempty: "G\<noteq>0"
 proof -
   have "P\<subseteq>P" ..
   with P_in_M P_dense \<open>P\<subseteq>P\<close>
   show "G \<noteq> 0"
     using generic unfolding M_generic_def by auto
 qed
 
 end (* context G_generic *)
 end
\ No newline at end of file
diff --git a/thys/Forcing/Succession_Poset.thy b/thys/Forcing/Succession_Poset.thy
--- a/thys/Forcing/Succession_Poset.thy
+++ b/thys/Forcing/Succession_Poset.thy
@@ -1,369 +1,369 @@
 section\<open>A poset of successions\<close>
 theory Succession_Poset
   imports
     Arities Proper_Extension Synthetic_Definition
     Names
 begin
 
 subsection\<open>The set of finite binary sequences\<close>
 
 text\<open>We implement the poset for adding one Cohen real, the set 
 $2^{<\omega}$ of of finite binary sequences.\<close>
 
 definition
   seqspace :: "i \<Rightarrow> i" ("_^<\<omega>" [100]100) where
   "seqspace(B) \<equiv> \<Union>n\<in>nat. (n\<rightarrow>B)"
 
 lemma seqspaceI[intro]: "n\<in>nat \<Longrightarrow> f:n\<rightarrow>B \<Longrightarrow> f\<in>seqspace(B)"
   unfolding seqspace_def by blast
 
 lemma seqspaceD[dest]: "f\<in>seqspace(B) \<Longrightarrow> \<exists>n\<in>nat. f:n\<rightarrow>B"
   unfolding seqspace_def by blast
 
 lemma seqspace_type: 
   "f \<in> B^<\<omega> \<Longrightarrow> \<exists>n\<in>nat. f:n\<rightarrow>B" 
   unfolding seqspace_def by auto
 
 schematic_goal seqspace_fm_auto:
   assumes 
     "nth(i,env) = n" "nth(j,env) = z"  "nth(h,env) = B" 
     "i \<in> nat" "j \<in> nat" "h\<in>nat" "env \<in> list(A)"
   shows 
     "(\<exists>om\<in>A. omega(##A,om) \<and> n \<in> om \<and> is_funspace(##A, n, B, z)) \<longleftrightarrow> (A, env \<Turnstile> (?sqsprp(i,j,h)))"
   unfolding is_funspace_def 
   by (insert assms ; (rule sep_rules | simp)+)
 
 synthesize "seqspace_rep_fm" from_schematic seqspace_fm_auto
  
 locale M_seqspace =  M_trancl +
   assumes 
     seqspace_replacement: "M(B) \<Longrightarrow> strong_replacement(M,\<lambda>n z. n\<in>nat \<and> is_funspace(M,n,B,z))"
 begin
 
 lemma seqspace_closed:
   "M(B) \<Longrightarrow> M(B^<\<omega>)"
   unfolding seqspace_def using seqspace_replacement[of B] RepFun_closed2 
   by simp
 
 end (* M_seqspace *)
 
 
 sublocale M_ctm \<subseteq> M_seqspace "##M"
 proof (unfold_locales, simp)
   fix B
-  have "arity(seqspace_rep_fm(1,0,2)) \<le> 3" "seqspace_rep_fm(1,0,2)\<in>formula" 
+  have "arity(seqspace_rep_fm(0,1,2)) \<le> 3" "seqspace_rep_fm(0,1,2)\<in>formula" 
     unfolding seqspace_rep_fm_def 
     using arity_pair_fm arity_omega_fm arity_typed_function_fm nat_simp_union 
     by auto
   moreover
   assume "B\<in>M"
   ultimately
-  have "strong_replacement(##M, \<lambda>x y. M, [x, y, B] \<Turnstile> seqspace_rep_fm(1, 0, 2))"
-    using replacement_ax[of "seqspace_rep_fm(1,0,2)"]
+  have "strong_replacement(##M, \<lambda>x y. M, [x, y, B] \<Turnstile> seqspace_rep_fm(0, 1, 2))"
+    using replacement_ax[of "seqspace_rep_fm(0,1,2)"]
     by simp
   moreover 
   note \<open>B\<in>M\<close>
   moreover from this
-  have "univalent(##M, A, \<lambda>x y. M, [x, y, B] \<Turnstile> seqspace_rep_fm(1, 0, 2))" 
+  have "univalent(##M, A, \<lambda>x y. M, [x, y, B] \<Turnstile> seqspace_rep_fm(0, 1, 2))" 
     if "A\<in>M" for A 
     using that unfolding univalent_def seqspace_rep_fm_def  
     by (auto, blast dest:transitivity)
   ultimately
   have "strong_replacement(##M, \<lambda>n z. \<exists>om[##M]. omega(##M,om) \<and> n \<in> om \<and> is_funspace(##M, n, B, z))"
     using seqspace_fm_auto[of 0 "[_,_,B]" _ 1 _ 2 B M] unfolding seqspace_rep_fm_def strong_replacement_def
     by simp
   with \<open>B\<in>M\<close> 
   show "strong_replacement(##M, \<lambda>n z. n \<in> nat \<and> is_funspace(##M, n, B, z))"
     using M_nat by simp
 qed
 
 definition seq_upd :: "i \<Rightarrow> i \<Rightarrow> i" where
   "seq_upd(f,a) \<equiv> \<lambda> j \<in> succ(domain(f)) . if j < domain(f) then f`j else a"
 
 lemma seq_upd_succ_type : 
   assumes "n\<in>nat" "f\<in>n\<rightarrow>A" "a\<in>A"
   shows "seq_upd(f,a)\<in> succ(n) \<rightarrow> A"
 proof -
   from assms
   have equ: "domain(f) = n" using domain_of_fun by simp
   {
     fix j
     assume "j\<in>succ(domain(f))"
     with equ \<open>n\<in>_\<close>
     have "j\<le>n" using ltI by auto
     with \<open>n\<in>_\<close>
     consider (lt) "j<n" | (eq) "j=n" using leD by auto
     then 
     have "(if j < n then f`j else a) \<in> A"
     proof cases
       case lt
       with \<open>f\<in>_\<close> 
       show ?thesis using apply_type ltD[OF lt] by simp
     next
       case eq
       with \<open>a\<in>_\<close>
       show ?thesis by auto
     qed
   }
   with equ
   show ?thesis
     unfolding seq_upd_def
     using lam_type[of "succ(domain(f))"]
     by auto
 qed
 
 lemma seq_upd_type : 
   assumes "f\<in>A^<\<omega>" "a\<in>A"
   shows "seq_upd(f,a) \<in> A^<\<omega>"
 proof -
   from \<open>f\<in>_\<close>
   obtain y where "y\<in>nat" "f\<in>y\<rightarrow>A"
     unfolding seqspace_def by blast
   with \<open>a\<in>A\<close>
   have "seq_upd(f,a)\<in>succ(y)\<rightarrow>A" 
     using seq_upd_succ_type by simp
   with \<open>y\<in>_\<close>
   show ?thesis
     unfolding seqspace_def by auto
 qed
 
 lemma seq_upd_apply_domain [simp]: 
   assumes "f:n\<rightarrow>A" "n\<in>nat"
   shows "seq_upd(f,a)`n = a"
   unfolding seq_upd_def using assms domain_of_fun by auto
 
 lemma zero_in_seqspace : 
   shows "0 \<in> A^<\<omega>"
   unfolding seqspace_def
   by force
 
 definition
   seqleR :: "i \<Rightarrow> i \<Rightarrow> o" where
   "seqleR(f,g) \<equiv> g \<subseteq> f"
 
 definition
   seqlerel :: "i \<Rightarrow> i" where
   "seqlerel(A) \<equiv> Rrel(\<lambda>x y. y \<subseteq> x,A^<\<omega>)"
 
 definition
   seqle :: "i" where
   "seqle \<equiv> seqlerel(2)"
 
 lemma seqleI[intro!]: 
   "\<langle>f,g\<rangle> \<in> 2^<\<omega>\<times>2^<\<omega> \<Longrightarrow> g \<subseteq> f  \<Longrightarrow> \<langle>f,g\<rangle> \<in> seqle"
   unfolding  seqspace_def seqle_def seqlerel_def Rrel_def 
   by blast
 
 lemma seqleD[dest!]: 
   "z \<in> seqle \<Longrightarrow> \<exists>x y. \<langle>x,y\<rangle> \<in> 2^<\<omega>\<times>2^<\<omega> \<and> y \<subseteq> x \<and> z = \<langle>x,y\<rangle>"
   unfolding seqle_def seqlerel_def Rrel_def 
   by blast
 
 lemma upd_leI : 
   assumes "f\<in>2^<\<omega>" "a\<in>2"
   shows "\<langle>seq_upd(f,a),f\<rangle>\<in>seqle"  (is "\<langle>?f,_\<rangle>\<in>_")
 proof
   show " \<langle>?f, f\<rangle> \<in> 2^<\<omega> \<times> 2^<\<omega>" 
     using assms seq_upd_type by auto
 next
   show  "f \<subseteq> seq_upd(f,a)" 
   proof 
     fix x
     assume "x \<in> f"
     moreover from \<open>f \<in> 2^<\<omega>\<close>
     obtain n where  "n\<in>nat" "f : n \<rightarrow> 2"
       using seqspace_type by blast
     moreover from calculation
     obtain y where "y\<in>n" "x=\<langle>y,f`y\<rangle>" using Pi_memberD[of f n "\<lambda>_ . 2"] 
       by blast
     moreover from \<open>f:n\<rightarrow>2\<close>
     have "domain(f) = n" using domain_of_fun by simp
     ultimately
     show "x \<in> seq_upd(f,a)"
       unfolding seq_upd_def lam_def  
       by (auto intro:ltI)
   qed
 qed
 
 lemma preorder_on_seqle: "preorder_on(2^<\<omega>,seqle)"
   unfolding preorder_on_def refl_def trans_on_def by blast
 
 lemma zero_seqle_max: "x\<in>2^<\<omega> \<Longrightarrow> \<langle>x,0\<rangle> \<in> seqle"
   using zero_in_seqspace 
   by auto
 
 interpretation forcing_notion "2^<\<omega>" "seqle" "0"
   using preorder_on_seqle zero_seqle_max zero_in_seqspace 
   by unfold_locales simp_all
 
 abbreviation SEQle :: "[i, i] \<Rightarrow> o"  (infixl "\<preceq>s" 50)
   where "x \<preceq>s y \<equiv> Leq(x,y)"
 
 abbreviation SEQIncompatible :: "[i, i] \<Rightarrow> o"  (infixl "\<bottom>s" 50)
   where "x \<bottom>s y \<equiv> Incompatible(x,y)"
 
 lemma seqspace_separative:
   assumes "f\<in>2^<\<omega>"
   shows "seq_upd(f,0) \<bottom>s seq_upd(f,1)" (is "?f \<bottom>s ?g")
 proof 
   assume "compat(?f, ?g)"
   then 
   obtain h where "h \<in> 2^<\<omega>" "?f \<subseteq> h" "?g \<subseteq> h"
     by blast
   moreover from \<open>f\<in>_\<close>
   obtain y where "y\<in>nat" "f:y\<rightarrow>2" by blast
   moreover from this
   have "?f: succ(y) \<rightarrow> 2" "?g: succ(y) \<rightarrow> 2" 
     using seq_upd_succ_type by blast+
   moreover from this
   have "\<langle>y,?f`y\<rangle> \<in> ?f" "\<langle>y,?g`y\<rangle> \<in> ?g" using apply_Pair by auto
   ultimately
   have "\<langle>y,0\<rangle> \<in> h" "\<langle>y,1\<rangle> \<in> h" by auto
   moreover from \<open>h \<in> 2^<\<omega>\<close>
   obtain n where "n\<in>nat" "h:n\<rightarrow>2" by blast
   ultimately
   show "False"
     using fun_is_function[of h n "\<lambda>_. 2"] 
     unfolding seqspace_def function_def by auto
 qed
 
 definition is_seqleR :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
   "is_seqleR(Q,f,g) \<equiv> g \<subseteq> f"
 
 definition seqleR_fm :: "i \<Rightarrow> i" where
   "seqleR_fm(fg) \<equiv> Exists(Exists(And(pair_fm(0,1,fg#+2),subset_fm(1,0))))"
 
 lemma type_seqleR_fm :
   "fg \<in> nat \<Longrightarrow> seqleR_fm(fg) \<in> formula"
   unfolding seqleR_fm_def 
   by simp
 
 lemma arity_seqleR_fm :
   "fg \<in> nat \<Longrightarrow> arity(seqleR_fm(fg)) = succ(fg)"
   unfolding seqleR_fm_def 
   using arity_pair_fm arity_subset_fm nat_simp_union by simp
 
 lemma (in M_basic) seqleR_abs: 
   assumes "M(f)" "M(g)"
   shows "seqleR(f,g) \<longleftrightarrow> is_seqleR(M,f,g)"
   unfolding seqleR_def is_seqleR_def 
   using assms apply_abs domain_abs domain_closed[OF \<open>M(f)\<close>]  domain_closed[OF \<open>M(g)\<close>]
   by auto
 
 definition
   relP :: "[i\<Rightarrow>o,[i\<Rightarrow>o,i,i]\<Rightarrow>o,i] \<Rightarrow> o" where
   "relP(M,r,xy) \<equiv> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,xy) \<and> r(M,x,y))"
 
 lemma (in M_ctm) seqleR_fm_sats : 
   assumes "fg\<in>nat" "env\<in>list(M)" 
   shows "sats(M,seqleR_fm(fg),env) \<longleftrightarrow> relP(##M,is_seqleR,nth(fg, env))"
   unfolding seqleR_fm_def is_seqleR_def relP_def
   using assms trans_M sats_subset_fm pair_iff_sats
   by auto
 
 
 lemma (in M_basic) is_related_abs :
   assumes "\<And> f g . M(f) \<Longrightarrow> M(g) \<Longrightarrow> rel(f,g) \<longleftrightarrow> is_rel(M,f,g)"
   shows "\<And>z . M(z) \<Longrightarrow> relP(M,is_rel,z) \<longleftrightarrow> (\<exists>x y. z = \<langle>x,y\<rangle> \<and> rel(x,y))"
   unfolding relP_def using pair_in_M_iff assms by auto
 
 definition
   is_RRel :: "[i\<Rightarrow>o,[i\<Rightarrow>o,i,i]\<Rightarrow>o,i,i] \<Rightarrow> o" where
   "is_RRel(M,is_r,A,r) \<equiv> \<exists>A2[M]. cartprod(M,A,A,A2) \<and> is_Collect(M,A2, relP(M,is_r),r)"
 
 lemma (in M_basic) is_Rrel_abs :
   assumes "M(A)"  "M(r)"
     "\<And> f g . M(f) \<Longrightarrow> M(g) \<Longrightarrow> rel(f,g) \<longleftrightarrow> is_rel(M,f,g)"
   shows "is_RRel(M,is_rel,A,r) \<longleftrightarrow>  r = Rrel(rel,A)"
 proof -
   from \<open>M(A)\<close> 
   have "M(z)" if "z\<in>A\<times>A" for z
     using cartprod_closed transM[of z "A\<times>A"] that by simp
   then
   have A:"relP(M, is_rel, z) \<longleftrightarrow> (\<exists>x y. z = \<langle>x, y\<rangle> \<and> rel(x, y))" "M(z)" if "z\<in>A\<times>A" for z
     using that is_related_abs[of rel is_rel,OF assms(3)] by auto
   then
   have "Collect(A\<times>A,relP(M,is_rel)) = Collect(A\<times>A,\<lambda>z. (\<exists>x y. z = \<langle>x,y\<rangle> \<and> rel(x,y)))"
     using Collect_cong[of "A\<times>A" "A\<times>A" "relP(M,is_rel)",OF _ A(1)] assms(1) assms(2)
     by auto
   with assms
   show ?thesis unfolding is_RRel_def Rrel_def using cartprod_closed
     by auto
 qed
 
 definition
   is_seqlerel :: "[i\<Rightarrow>o,i,i] \<Rightarrow> o" where
   "is_seqlerel(M,A,r) \<equiv> is_RRel(M,is_seqleR,A,r)"
 
 lemma (in M_basic) seqlerel_abs :
   assumes "M(A)"  "M(r)"
   shows "is_seqlerel(M,A,r) \<longleftrightarrow> r = Rrel(seqleR,A)"
   unfolding is_seqlerel_def
   using is_Rrel_abs[OF \<open>M(A)\<close> \<open>M(r)\<close>,of seqleR is_seqleR] seqleR_abs
   by auto
 
 definition RrelP :: "[i\<Rightarrow>i\<Rightarrow>o,i] \<Rightarrow> i" where
   "RrelP(R,A) \<equiv> {z\<in>A\<times>A. \<exists>x y. z = \<langle>x, y\<rangle> \<and> R(x,y)}"
   
 lemma Rrel_eq : "RrelP(R,A) = Rrel(R,A)"
   unfolding Rrel_def RrelP_def by auto
 
 context M_ctm
 begin
 
 lemma Rrel_closed:
   assumes "A\<in>M" 
     "\<And> a. a \<in> nat \<Longrightarrow> rel_fm(a)\<in>formula"
     "\<And> f g . (##M)(f) \<Longrightarrow> (##M)(g) \<Longrightarrow> rel(f,g) \<longleftrightarrow> is_rel(##M,f,g)"
     "arity(rel_fm(0)) = 1" 
     "\<And> a . a \<in> M \<Longrightarrow> sats(M,rel_fm(0),[a]) \<longleftrightarrow> relP(##M,is_rel,a)"
   shows "(##M)(Rrel(rel,A))" 
 proof -
   have "z\<in> M \<Longrightarrow> relP(##M, is_rel, z) \<longleftrightarrow> (\<exists>x y. z = \<langle>x, y\<rangle> \<and> rel(x, y))" for z
     using assms(3) is_related_abs[of rel is_rel]
     by auto
   with assms
   have "Collect(A\<times>A,\<lambda>z. (\<exists>x y. z = \<langle>x,y\<rangle> \<and> rel(x,y))) \<in> M"
     using Collect_in_M_0p[of "rel_fm(0)" "\<lambda> A z . relP(A,is_rel,z)" "\<lambda> z.\<exists>x y. z = \<langle>x, y\<rangle> \<and> rel(x, y)" ]
         cartprod_closed
     by simp
   then show ?thesis
   unfolding Rrel_def by simp
 qed
 
 lemma seqle_in_M: "seqle \<in> M"
   using Rrel_closed seqspace_closed 
     transitivity[OF _ nat_in_M] type_seqleR_fm[of 0] arity_seqleR_fm[of 0]
     seqleR_fm_sats[of 0] seqleR_abs seqlerel_abs 
   unfolding seqle_def seqlerel_def seqleR_def
   by auto
 
 subsection\<open>Cohen extension is proper\<close>
 
 interpretation ctm_separative "2^<\<omega>" seqle 0
 proof (unfold_locales)
   fix f
   let ?q="seq_upd(f,0)" and ?r="seq_upd(f,1)"
   assume "f \<in> 2^<\<omega>"
   then
   have "?q \<preceq>s f \<and> ?r \<preceq>s f \<and> ?q \<bottom>s ?r" 
     using upd_leI seqspace_separative by auto
   moreover from calculation
   have "?q \<in> 2^<\<omega>"  "?r \<in> 2^<\<omega>"
     using seq_upd_type[of f 2] by auto
   ultimately
   show "\<exists>q\<in>2^<\<omega>. \<exists>r\<in>2^<\<omega>. q \<preceq>s f \<and> r \<preceq>s f \<and> q \<bottom>s r"
     by (rule_tac bexI)+ \<comment> \<open>why the heck auto-tools don't solve this?\<close>
 next
   show "2^<\<omega> \<in> M" using nat_into_M seqspace_closed by simp
 next
   show "seqle \<in> M" using seqle_in_M .
 qed
 
 lemma cohen_extension_is_proper: "\<exists>G. M_generic(G) \<and> M \<noteq> GenExt(G)"
   using proper_extension generic_filter_existence zero_in_seqspace
   by force
 
 end (* M_ctm *)
 
 end
\ No newline at end of file