Theory Forces_Definition

theory Forces_Definition
imports Arities
section‹The definition of \<^term>‹forces››
theory Forces_Definition imports Arities FrecR Synthetic_Definition begin

text‹This is the core of our development.›

subsection‹The relation \<^term>‹frecrel››

(* ∃x y. z = ⟨x, y⟩ ∧ frecR(x,y) *)
definition
  frecrelP :: "[i⇒o,i] ⇒ o" where
  "frecrelP(M,xy) ≡ (∃x[M]. ∃y[M]. pair(M,x,y,xy) ∧ is_frecR(M,x,y))"

definition
  frecrelP_fm :: "i ⇒ i" where
  "frecrelP_fm(a) == Exists(Exists(And(pair_fm(1,0,a#+2),frecR_fm(1,0))))"

lemma arity_frecrelP_fm :
  "a∈nat ⟹ 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∈nat ⟹ frecrelP_fm(a)∈formula" 
  unfolding frecrelP_fm_def by simp

lemma sats_frecrelP_fm :
  assumes "a∈nat" "env∈list(A)"
  shows "sats(A,frecrelP_fm(a),env) ⟷ frecrelP(##A,nth(a, env))"
  unfolding frecrelP_def frecrelP_fm_def
  using assms by (simp add: sats_frecR_fm)

lemma frecrelP_iff_sats:
  assumes
    "nth(a,env) = aa" "a∈ nat"  "env ∈ list(A)"
  shows
       "frecrelP(##A,aa)  ⟷ sats(A, frecrelP_fm(a), env)"
  using assms
  by (simp add:sats_frecrelP_fm)

(* {z∈A×A. ∃x y. z = ⟨x, y⟩ ∧ frecR(x,y)} *)
definition
  is_frecrel :: "[i⇒o,i,i] ⇒ o" where
  "is_frecrel(M,A,r) ≡ ∃A2[M]. cartprod(M,A,A,A2) ∧ is_Collect(M,A2, frecrelP(M) ,r)"

definition
  frecrel_fm :: "[i,i] ⇒ i" where
  "frecrel_fm(a,r) ≡ Exists(And(cartprod_fm(a#+1,a#+1,0),Collect_fm(0,frecrelP_fm(0),r#+1)))" 

lemma frecrel_fm_type[TC] :
  "⟦a∈nat;b∈nat⟧ ⟹ frecrel_fm(a,b)∈formula"
  unfolding frecrel_fm_def by simp

lemma arity_frecrel_fm :
  assumes "a∈nat"  "b∈nat" 
  shows "arity(frecrel_fm(a,b)) = succ(a) ∪ 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∈nat"  "r∈nat" "env∈list(A)"
  shows
    "sats(A,frecrel_fm(a,r),env)
    ⟷ 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∈ nat"  "r∈ nat"  "env ∈ list(A)"
  shows
       "is_frecrel(##A, aa,rr) ⟷ sats(A, frecrel_fm(a,r), env)"
  using assms
  by (simp add:sats_frecrel_fm)

definition
  names_below :: "i ⇒ i ⇒ i" where
  "names_below(P,x) ≡ 2×ecloseN(x)×ecloseN(x)×P"

lemma names_belowsD:
  assumes "x ∈ names_below(P,z)"
  obtains f n1 n2 p where
    "x = <f,n1,n2,p>" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈P"
  using assms unfolding names_below_def by auto


definition
  is_names_below :: "[i⇒o,i,i,i] ⇒ o" where
  "is_names_below(M,P,x,nb) == ∃p1[M]. ∃p0[M]. ∃t[M]. ∃ec[M]. 
              is_ecloseN(M,ec,x) ∧ number2(M,t) ∧ cartprod(M,ec,P,p0) ∧ cartprod(M,ec,p0,p1)
              ∧ cartprod(M,t,p1,nb)"

definition
  number2_fm :: "i⇒i" where
  "number2_fm(a) == Exists(And(number1_fm(0), succ_fm(0,succ(a))))"

lemma number2_fm_type[TC] :
  "a∈nat ⟹ number2_fm(a) ∈ formula"
  unfolding number2_fm_def by simp

lemma number2arity__fm : 
  "a∈nat ⟹ 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]:
   "[| x ∈ nat; env ∈ list(A)|]
    ==> sats(A, number2_fm(x), env) ⟷ number2(##A, nth(x,env))"
by (simp add: number2_fm_def number2_def)

definition 
  is_names_below_fm :: "[i,i,i] ⇒ i" where
  "is_names_below_fm(P,x,nb) == 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 : 
  "⟦P∈nat;x∈nat;nb∈nat⟧ ⟹ arity(is_names_below_fm(P,x,nb)) = succ(P) ∪ succ(x) ∪ 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]:
  "⟦P∈nat;x∈nat;nb∈nat⟧ ⟹ is_names_below_fm(P,x,nb)∈formula" 
  unfolding is_names_below_fm_def by simp

lemma sats_is_names_below_fm :
  assumes
    "P∈nat" "x∈nat" "nb∈nat" "env∈list(A)" 
  shows
    "sats(A,is_names_below_fm(P,x,nb),env)
    ⟷ 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⇒o,i,i,i,i,i] ⇒ o" where
  "is_tuple(M,z,t1,t2,p,t) == ∃t1t2p[M]. ∃t2p[M]. pair(M,t2,p,t2p) ∧ pair(M,t1,t2p,t1t2p) ∧
                                                  pair(M,z,t1t2p,t)" 


definition
  is_tuple_fm :: "[i,i,i,i,i] ⇒ 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 : "⟦ z∈nat ; t1∈nat ; t2∈nat ; p∈nat ; tup∈nat ⟧ ⟹ 
  arity(is_tuple_fm(z,t1,t2,p,tup)) = ⋃ {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∈nat ⟹ t1∈nat ⟹ t2∈nat ⟹ p∈nat ⟹ tup∈nat ⟹ is_tuple_fm(z,t1,t2,p,tup)∈formula" 
  unfolding is_tuple_fm_def by simp

lemma sats_is_tuple_fm :
  assumes
    "z∈nat"  "t1∈nat" "t2∈nat" "p∈nat" "tup∈nat" "env∈list(A)"
  shows
    "sats(A,is_tuple_fm(z,t1,t2,p,tup),env)
    ⟷ 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∈nat" "b∈nat" "c∈nat" "d∈nat" "e∈nat"  "env ∈ list(A)"
  shows
       "is_tuple(##A,aa,bb,cc,dd,ee)  ⟷ sats(A, is_tuple_fm(a,b,c,d,e), env)"
  using assms by (simp add: sats_is_tuple_fm)

subsection‹Definition of \<^term>‹forces› for equality and membership›

(* p ||- τ = θ ≡
  ∀σ. σ∈domain(τ) ∪ domain(θ) ⟶ (∀q∈P. <q,p>∈leq ⟶ ((q ||- σ∈τ) ⟷ (q ||- σ∈θ)) ) *)
definition
  eq_case :: "[i,i,i,i,i,i] ⇒ o" where
  "eq_case(t1,t2,p,P,leq,f) ≡ ∀s. s∈domain(t1) ∪ domain(t2) ⟶
      (∀q. q∈P ∧ <q,p>∈leq ⟶ (f`<1,s,t1,q>=1  ⟷ f`<1,s,t2,q> =1))"


definition
  is_eq_case :: "[i⇒o,i,i,i,i,i,i] ⇒ o" where
  "is_eq_case(M,t1,t2,p,P,leq,f) ≡
   ∀s[M]. (∃d[M]. is_domain(M,t1,d) ∧ s∈d) ∨ (∃d[M]. is_domain(M,t2,d) ∧ s∈d)
       ⟶ (∀q[M]. q∈P ∧ (∃qp[M]. pair(M,q,p,qp) ∧ qp∈leq) ⟶
            (∃ost1q[M]. ∃ost2q[M]. ∃o[M].  ∃vf1[M]. ∃vf2[M].
             is_tuple(M,o,s,t1,q,ost1q) ∧
             is_tuple(M,o,s,t2,q,ost2q) ∧ number1(M,o) ∧ 
             fun_apply(M,f,ost1q,vf1) ∧ fun_apply(M,f,ost2q,vf2) ∧
             (vf1 = o ⟷ vf2 = o)))"

(* p ||-
   π ∈ τ ≡ ∀v∈P. <v,p>∈leq ⟶ (∃q∈P. <q,v>∈leq ∧ (∃σ. ∃r∈P. <σ,r>∈τ ∧ <q,r>∈leq ∧  q ||- π = σ)) *)
definition
  mem_case :: "[i,i,i,i,i,i] ⇒ o" where
  "mem_case(t1,t2,p,P,leq,f) ≡ ∀v∈P. <v,p>∈leq ⟶
    (∃q. ∃s. ∃r. r∈P ∧ q∈P ∧ <q,v>∈leq ∧ <s,r> ∈ t2 ∧ <q,r>∈leq ∧  f`<0,t1,s,q> = 1)"

definition
  is_mem_case :: "[i⇒o,i,i,i,i,i,i] ⇒ o" where
  "is_mem_case(M,t1,t2,p,P,leq,f) ≡ ∀v[M]. ∀vp[M]. v∈P ∧ pair(M,v,p,vp) ∧ vp∈leq ⟶
    (∃q[M]. ∃s[M]. ∃r[M]. ∃qv[M]. ∃sr[M]. ∃qr[M]. ∃z[M]. ∃zt1sq[M]. ∃o[M].
     r∈ P ∧ q∈P ∧ pair(M,q,v,qv) ∧ pair(M,s,r,sr) ∧ pair(M,q,r,qr) ∧ 
     empty(M,z) ∧ is_tuple(M,z,t1,s,q,zt1sq) ∧
     number1(M,o) ∧ qv∈leq ∧ sr∈t2 ∧ qr∈leq ∧ fun_apply(M,f,zt1sq,o))"


schematic_goal sats_is_mem_case_fm_auto:
  assumes 
    "n1∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat" "env∈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))
    ⟷ 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∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat"
  shows
    "arity(mem_case_fm(n1,n2,p,P,leq,f)) = 
    succ(n1) ∪ succ(n2) ∪ succ(p) ∪ succ(P) ∪ succ(leq) ∪ 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∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat" "env∈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))
    ⟷ 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∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat"
  shows
    "arity(eq_case_fm(n1,n2,p,P,leq,f)) = 
    succ(n1) ∪ succ(n2) ∪ succ(p) ∪ succ(P) ∪ succ(leq) ∪ 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

lemma mem_case_fm_type[TC] :
  "⟦n1∈nat;n2∈nat;p∈nat;P∈nat;leq∈nat;f∈nat⟧ ⟹ mem_case_fm(n1,n2,p,P,leq,f)∈formula"
  unfolding mem_case_fm_def by simp

lemma eq_case_fm_type[TC] :
  "⟦n1∈nat;n2∈nat;p∈nat;P∈nat;leq∈nat;f∈nat⟧ ⟹ eq_case_fm(n1,n2,p,P,leq,f)∈formula"
  unfolding eq_case_fm_def by simp

lemma sats_eq_case_fm :
  assumes 
    "n1∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat" "env∈list(A)"
  shows
    "sats(A,eq_case_fm(n1,n2,p,P,leq,f),env) ⟷ 
    is_eq_case(##A, nth(n1, env),nth(n2, env),nth(p, env),nth(P, env), nth(leq, env),nth(f,env))"
  unfolding eq_case_fm_def is_eq_case_def using assms by (simp add: sats_is_tuple_fm)

lemma sats_mem_case_fm :
  assumes 
    "n1∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat" "env∈list(A)"
  shows
    "sats(A,mem_case_fm(n1,n2,p,P,leq,f),env) ⟷ 
    is_mem_case(##A, nth(n1, env),nth(n2, env),nth(p, env),nth(P, env), nth(leq, env),nth(f,env))"
  unfolding mem_case_fm_def is_mem_case_def using assms by (simp add: sats_is_tuple_fm)

lemma mem_case_iff_sats:
  assumes
    "n1∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat" "env∈list(A)"    
    "nth(n1,env) = nn1" "nth(n2,env) = nn2" "nth(p,env) = pp" "nth(P,env) = PP" 
    "nth(leq,env) = lleq" "nth(f,env) = ff"  
  shows
    "is_mem_case(##A, nn1,nn2,pp,PP, lleq,ff)
    ⟷ sats(A,mem_case_fm(n1,n2,p,P,leq,f),env)"
  using assms
  by (simp add:sats_mem_case_fm)

lemma eq_case_iff_sats :
  assumes
    "n1∈nat" "n2∈nat" "p∈nat" "P∈nat" "leq∈nat" "f∈nat" "env∈list(A)"    
    "nth(n1,env) = nn1" "nth(n2,env) = nn2" "nth(p,env) = pp" "nth(P,env) = PP" 
    "nth(leq,env) = lleq" "nth(f,env) = ff"  
  shows
    "is_eq_case(##A, nn1,nn2,pp,PP, lleq,ff)
    ⟷ sats(A,eq_case_fm(n1,n2,p,P,leq,f),env)"
  using assms
  by (simp add:sats_eq_case_fm)

definition
  Hfrc :: "[i,i,i,i] ⇒ o" where
  "Hfrc(P,leq,fnnc,f) ≡ ∃ft. ∃n1. ∃n2. ∃c. c∈P ∧ fnnc = <ft,n1,n2,c> ∧
     (  ft = 0 ∧  eq_case(n1,n2,c,P,leq,f)
      ∨ ft = 1 ∧ mem_case(n1,n2,c,P,leq,f))"

definition
  is_Hfrc :: "[i⇒o,i,i,i,i] ⇒ o" where
  "is_Hfrc(M,P,leq,fnnc,f) ≡
     ∃ft[M]. ∃n1[M]. ∃n2[M]. ∃co[M]. 
      co∈P ∧ is_tuple(M,ft,n1,n2,co,fnnc) ∧
      (  (empty(M,ft) ∧ is_eq_case(M,n1,n2,co,P,leq,f))
       ∨ (number1(M,ft) ∧  is_mem_case(M,n1,n2,co,P,leq,f)))"

definition 
  Hfrc_fm :: "[i,i,i,i] ⇒ i" where
  "Hfrc_fm(P,leq,fnnc,f) ≡ 
    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(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] :
  "⟦P∈nat;leq∈nat;fnnc∈nat;f∈nat⟧ ⟹ Hfrc_fm(P,leq,fnnc,f)∈formula"
  unfolding Hfrc_fm_def by simp

lemma arity_Hfrc_fm : 
  assumes 
    "P∈nat" "leq∈nat" "fnnc∈nat" "f∈nat"
  shows
    "arity(Hfrc_fm(P,leq,fnnc,f)) = succ(P) ∪ succ(leq) ∪ succ(fnnc) ∪ 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∈nat" "leq∈nat" "fnnc∈nat" "f∈nat" "env∈list(A)"
  shows
    "sats(A,Hfrc_fm(P,leq,fnnc,f),env)
    ⟷ 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_eq_case_fm sats_is_tuple_fm sats_mem_case_fm)

lemma Hfrc_iff_sats:
  assumes
    "P∈nat" "leq∈nat" "fnnc∈nat" "f∈nat" "env∈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)
    ⟷ sats(A,Hfrc_fm(P,leq,fnnc,f),env)"
  using assms
  by (simp add:sats_Hfrc_fm)
                              
definition
  is_Hfrc_at :: "[i⇒o,i,i,i,i,i] ⇒ o" where
  "is_Hfrc_at(M,P,leq,fnnc,f,z) ≡ 
            (empty(M,z) ∧ ¬ is_Hfrc(M,P,leq,fnnc,f))
          ∨ (number1(M,z) ∧ is_Hfrc(M,P,leq,fnnc,f))"

definition
  Hfrc_at_fm :: "[i,i,i,i,i] ⇒ i" where
  "Hfrc_at_fm(P,leq,fnnc,f,z) ≡ 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∈nat" "leq∈nat" "fnnc∈nat" "f∈nat" "z∈nat"
  shows
    "arity(Hfrc_at_fm(P,leq,fnnc,f,z)) = succ(P) ∪ succ(leq) ∪ succ(fnnc) ∪ succ(f) ∪ 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] :
  "⟦P∈nat;leq∈nat;fnnc∈nat;f∈nat;z∈nat⟧ ⟹ Hfrc_at_fm(P,leq,fnnc,f,z)∈formula"
  unfolding Hfrc_at_fm_def by simp

lemma sats_Hfrc_at_fm:
  assumes 
    "P∈nat" "leq∈nat" "fnnc∈nat" "f∈nat" "z∈nat" "env∈list(A)"
  shows
    "sats(A,Hfrc_at_fm(P,leq,fnnc,f,z),env)
    ⟷ 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∈nat" "leq∈nat" "fnnc∈nat" "f∈nat" "z∈nat" "env∈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)
    ⟷ 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 :
  "⟦x∈nat;f∈nat⟧ ⟹ arity(tran_closure_fm(x,f)) = succ(x) ∪ succ(f)"
  unfolding tran_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‹The well-founded relation \<^term>‹forcerel››
definition
  forcerel :: "i ⇒ i ⇒ i" where
  "forcerel(P,x) ≡ frecrel(names_below(P,x))^+"

definition
  is_forcerel :: "[i⇒o,i,i,i] ⇒ o" where
  "is_forcerel(M,P,x,z) == ∃r[M]. ∃nb[M]. tran_closure(M,r,z) ∧ 
                        (is_names_below(M,P,x,nb) ∧ is_frecrel(M,nb,r))"

definition
  forcerel_fm :: "i⇒ i ⇒ i ⇒ i" where
  "forcerel_fm(p,x,z) == Exists(Exists(And(tran_closure_fm(1, z#+2),
                                        And(is_names_below_fm(p#+2,x#+2,0),frecrel_fm(0,1)))))"

lemma arity_forcerel_fm: 
  "⟦p∈nat;x∈nat;z∈nat⟧ ⟹ arity(forcerel_fm(p,x,z)) = succ(p) ∪ succ(x) ∪ 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]: 
  "⟦p∈nat;x∈nat;z∈nat⟧ ⟹ forcerel_fm(p,x,z)∈formula" 
  unfolding forcerel_fm_def by simp


lemma sats_forcerel_fm:
  assumes
    "p∈nat" "x∈nat"  "z∈nat" "env∈list(A)" 
  shows
    "sats(A,forcerel_fm(p,x,z),env) ⟷ is_forcerel(##A,nth(p,env),nth(x, env),nth(z, env))"
proof -
  have "sats(A,tran_closure_fm(1,z #+ 2),Cons(nb,Cons(r,env))) ⟷
        tran_closure(##A, r, nth(z, env))" if "r∈A" "nb∈A" for r nb
    using that assms sats_tran_closure_fm[of 1 "z #+ 2" "[nb,r]@env"] by simp
  moreover
  have "sats(A, is_names_below_fm(succ(succ(p)), succ(succ(x)), 0), Cons(nb, Cons(r, env))) ⟷
        is_names_below(##A, nth(p,env), nth(x, env), nb)"
    if "r∈A" "nb∈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))) ⟷ 
        is_frecrel(##A, nb, r)"
    if "r∈A" "nb∈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‹\<^term>‹frc_at›, forcing for atomic formulas›
definition
  frc_at :: "[i,i,i] ⇒ i" where
  "frc_at(P,leq,fnnc) ≡ wfrec(frecrel(names_below(P,fnnc)),fnnc,
                              λx f. bool_of_o(Hfrc(P,leq,x,f)))"

definition
  is_frc_at :: "[i⇒o,i,i,i,i] ⇒ o" where
  "is_frc_at(M,P,leq,x,z) ≡ ∃r[M]. is_forcerel(M,P,x,r) ∧ 
                                    is_wfrec(M,is_Hfrc_at(M,P,leq),r,x,z)"


(* is_frc_at(x,z) ≡ is_wfrec(##M,is_Hfrc_at(##M,P,leq),forcerel(x),x,z) *)
definition
  frc_at_fm :: "[i,i,i,i] ⇒ i" where
  "frc_at_fm(p,l,x,z) == 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] :
  "⟦p∈nat;l∈nat;x∈nat;z∈nat⟧ ⟹ frc_at_fm(p,l,x,z)∈formula"
  unfolding frc_at_fm_def by simp

lemma arity_frc_at_fm :
  assumes "p∈nat" "l∈nat" "x∈nat" "z∈nat"
  shows "arity(frc_at_fm(p,l,x,z)) = succ(p) ∪ succ(l) ∪ succ(x) ∪ succ(z)" 
proof -
  let  = "Hfrc_at_fm(6 #+ p, 6 #+ l, 2, 1, 0)"
  from assms
  have  "arity(?φ) = (7#+p) ∪ (7#+l)" "?φ ∈ formula"
    using arity_Hfrc_at_fm nat_simp_union
    by auto
  with assms 
  have W: "arity(is_wfrec_fm(?φ, 0, succ(x), succ(z))) = 2#+p ∪ (2#+l) ∪ (2#+x) ∪ (2#+z)"
    using arity_is_wfrec_fm[OF ‹?φ∈_› _ _ _ _ ‹arity(?φ) = _›] 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)) ∪ 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∈nat" "l∈nat" "i∈nat" "j∈nat" "env∈list(A)" "i < length(env)" "j < length(env)"
  shows
    "sats(A,frc_at_fm(p,l,i,j),env) ⟷ 
     is_frc_at(##A,nth(p,env),nth(l,env),nth(i,env),nth(j,env))" 
proof -
  {
    fix r pp ll
    assume "r∈A" 
  have 0:"is_Hfrc_at(##A,nth(p,env),nth(l,env),a2, a1, a0) ⟷ 
         sats(A, Hfrc_at_fm(6#+p,6#+l,2,1,0), [a0,a1,a2,a3,a4,r]@env)" 
        if "a0∈A" "a1∈A" "a2∈A" "a3∈A" "a4∈A" for a0 a1 a2 a3 a4
    using  that assms ‹r∈A› 
          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) ⟷
         is_wfrec(##A, is_Hfrc_at(##A, nth(p,env), nth(l,env)), r,nth(i, env), nth(j, env))"
    using assms ‹r∈A› 
          sats_is_wfrec_fm[OF 0[simplified]]  
    by simp
}
  moreover
  have "sats(A, forcerel_fm(succ(p), succ(i), 0), Cons(r, env)) ⟷
        is_forcerel(##A,nth(p,env),nth(i,env),r)" if "r∈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] ⇒ o" where
  "forces_eq'(P,l,p,t1,t2) ≡ frc_at(P,l,<0,t1,t2,p>) = 1"

definition
  forces_mem' :: "[i,i,i,i,i] ⇒ o" where
  "forces_mem'(P,l,p,t1,t2) ≡ frc_at(P,l,<1,t1,t2,p>) = 1"

definition
  forces_neq' :: "[i,i,i,i,i] ⇒ o" where
  "forces_neq'(P,l,p,t1,t2) ≡ ¬ (∃q∈P. <q,p>∈l ∧ forces_eq'(P,l,q,t1,t2))"

definition
  forces_nmem' :: "[i,i,i,i,i] ⇒ o" where
  "forces_nmem'(P,l,p,t1,t2) ≡ ¬ (∃q∈P. <q,p>∈l ∧ forces_mem'(P,l,q,t1,t2))"

(* frc_at(P,leq,<0,t1,t2,p>) = 1*) 
definition
  is_forces_eq' :: "[i⇒o,i,i,i,i,i] ⇒ o" where
  "is_forces_eq'(M,P,l,p,t1,t2) == ∃o[M]. ∃z[M]. ∃t[M]. number1(M,o) ∧ empty(M,z) ∧ 
                                is_tuple(M,z,t1,t2,p,t) ∧ is_frc_at(M,P,l,t,o)"

(* frc_at(P,leq,<1,t1,t2,p>) = 1*) 
definition
  is_forces_mem' :: "[i⇒o,i,i,i,i,i] ⇒ o" where
  "is_forces_mem'(M,P,l,p,t1,t2) == ∃o[M]. ∃t[M]. number1(M,o) ∧  
                                is_tuple(M,o,t1,t2,p,t) ∧ is_frc_at(M,P,l,t,o)"


definition
  is_forces_neq' :: "[i⇒o,i,i,i,i,i] ⇒ o" where
  "is_forces_neq'(M,P,l,p,t1,t2) ≡
      ¬ (∃q[M]. q∈P ∧ (∃qp[M]. pair(M,q,p,qp) ∧ qp∈l ∧ is_forces_eq'(M,P,l,q,t1,t2)))"


(*¬ (∃q∈P. <q,p>∈l ∧ forces_eq'(P,l,q,t1,t2))*)
definition
  is_forces_nmem' :: "[i⇒o,i,i,i,i,i] ⇒ o" where
  "is_forces_nmem'(M,P,l,p,t1,t2) ≡
      ¬ (∃q[M]. ∃qp[M]. q∈P ∧ pair(M,q,p,qp) ∧ qp∈l ∧ is_forces_mem'(M,P,l,q,t1,t2))"


(* ∃o∈M. ∃z∈M. ∃t∈M. number1(##M,o) ∧ empty(##M,z) ∧
                                is_tuple(##M,z,t1,t2,p,t) ∧ is_frc_at(t,o) *)
definition
  forces_eq_fm :: "[i,i,i,i,i] ⇒ i" where
  "forces_eq_fm(p,l,q,t1,t2) ≡ 
     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) ))))))"

(* ∃o∈M. ∃t∈M. number1(##M,o) ∧  
                                is_tuple(##M,o,t1,t2,p,t) ∧ is_frc_at(t,o)*)
definition
  forces_mem_fm :: "[i,i,i,i,i] ⇒ i" where
  "forces_mem_fm(p,l,q,t1,t2) ≡ 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] ⇒ i" where
  "forces_neq_fm(p,l,q,t1,t2) ≡ 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] ⇒ i" where
  "forces_nmem_fm(p,l,q,t1,t2) ≡ 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]:
  "⟦ p∈nat;l∈nat;q∈nat;t1∈nat;t2∈nat⟧ ⟹ forces_eq_fm(p,l,q,t1,t2) ∈ formula"
  unfolding forces_eq_fm_def 
  by simp

lemma forces_mem_fm_type [TC]:
  "⟦ p∈nat;l∈nat;q∈nat;t1∈nat;t2∈nat⟧ ⟹ forces_mem_fm(p,l,q,t1,t2) ∈ formula"
  unfolding forces_mem_fm_def
  by simp

lemma forces_neq_fm_type [TC]:
  "⟦ p∈nat;l∈nat;q∈nat;t1∈nat;t2∈nat⟧ ⟹ forces_neq_fm(p,l,q,t1,t2) ∈ formula"
  unfolding forces_neq_fm_def 
  by simp

lemma forces_nmem_fm_type [TC]:
  "⟦ p∈nat;l∈nat;q∈nat;t1∈nat;t2∈nat⟧ ⟹ forces_nmem_fm(p,l,q,t1,t2) ∈ formula"
  unfolding forces_nmem_fm_def 
  by simp

lemma arity_forces_eq_fm :
  "p∈nat ⟹ l∈nat ⟹ q∈nat ⟹ t1 ∈ nat ⟹ t2 ∈ nat ⟹ 
   arity(forces_eq_fm(p,l,q,t1,t2)) = succ(t1) ∪ succ(t2) ∪ succ(q) ∪ succ(p) ∪ 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∈nat ⟹ l∈nat ⟹ q∈nat ⟹ t1 ∈ nat ⟹ t2 ∈ nat ⟹ 
   arity(forces_mem_fm(p,l,q,t1,t2)) = succ(t1) ∪ succ(t2) ∪ succ(q) ∪ succ(p) ∪ 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∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat"  "env∈list(M)" 
  shows "sats(M,forces_eq_fm(p,l,q,t1,t2),env) ⟷ 
         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∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat"  "env∈list(M)"
  shows "sats(M,forces_mem_fm(p,l,q,t1,t2),env) ⟷ 
             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∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat"  "env∈list(M)"
  shows "sats(M,forces_neq_fm(p,l,q,t1,t2),env) ⟷ 
             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∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat"  "env∈list(M)"
  shows "sats(M,forces_nmem_fm(p,l,q,t1,t2),env) ⟷ 
             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]:
  "⟦x∈M; y∈M ⟧ ⟹ is_fst(##M,x,y) ⟷ 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]:
  "⟦x∈M; y∈M ⟧ ⟹ is_snd(##M,x,y) ⟷ 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] :
  "⟦x∈M; y∈M ⟧ ⟹ is_ftype(##M,x,y) ⟷ y = ftype(x)" unfolding ftype_def  is_ftype_def by simp

lemma name1_abs[simp] :
  "⟦x∈M; y∈M ⟧ ⟹ is_name1(##M,x,y) ⟷ 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:
  "⟦x∈M; y∈M ⟧ ⟹ is_snd_snd(##M,x,y) ⟷ 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]:
  "⟦x∈M; y∈M ⟧ ⟹ is_name2(##M,x,y) ⟷ 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]:
  "⟦x∈M; y∈M ⟧ ⟹ is_cond_of(##M,x,y) ⟷ 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]:
  "⟦z∈M;t1∈M;t2∈M;p∈M;t∈M⟧ ⟹ 
   is_tuple(##M,z,t1,t2,p,t) ⟷ t = <z,t1,t2,p>" 
  unfolding is_tuple_def using tuples_in_M by simp

lemma oneN_in_M[simp]: "1∈M"
  by (simp flip: setclass_iff)

lemma twoN_in_M : "2∈M" 
  by (simp flip: setclass_iff)

lemma comp_in_M:
  "p ≼ q ⟹ p∈M"
  "p ≼ q ⟹ q∈M"
  using leq_in_M transitivity[of _ leq] pair_in_M_iff by auto

(* Absoluteness of Hfrc *)

lemma eq_case_abs [simp]:
  assumes
    "t1∈M" "t2∈M" "p∈M" "f∈M" 
  shows
    "is_eq_case(##M,t1,t2,p,P,leq,f) ⟷ eq_case(t1,t2,p,P,leq,f)"
proof -
  have "q ≼ p ⟹ q∈M" for q
    using comp_in_M by simp
  moreover
  have "⟨s,y⟩∈t ⟹ s∈domain(t)" if "t∈M" for s y t
    using that unfolding domain_def by auto
  ultimately
  have 
    "(∀s∈M. s ∈ domain(t1) ∨ s ∈ domain(t2) ⟶ (∀q∈M. q∈P ∧ q ≼ p ⟶ 
                              (f ` ⟨1, s, t1, q⟩ =1 ⟷ f ` ⟨1, s, t2, q⟩=1))) ⟷
    (∀s. s ∈ domain(t1) ∨ s ∈ domain(t2) ⟶ (∀q. q∈P ∧ q ≼ p ⟶ 
                                  (f ` ⟨1, s, t1, q⟩ =1 ⟷ f ` ⟨1, s, t2, q⟩=1)))" 
    using assms domain_trans[OF trans_M,of t1] 
                domain_trans[OF trans_M,of t2] by auto
  then show ?thesis
    unfolding eq_case_def is_eq_case_def 
    using assms pair_in_M_iff 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∈M" "t2∈M" "p∈M" "f∈M" 
  shows
    "is_mem_case(##M,t1,t2,p,P,leq,f) ⟷ mem_case(t1,t2,p,P,leq,f)"
  unfolding is_mem_case_def mem_case_def using assms zero_in_M pair_in_M_iff
    comp_in_M 
  apply auto 
   apply blast
  apply (drule bspec,auto)
  apply (rule bexI)+
     defer 1 prefer 2
  apply (rule domain_trans[OF trans_M,of t2],auto)
  done

lemma Hfrc_abs:
  "⟦fnnc∈M; f∈M⟧ ⟹
   is_Hfrc(##M,P,leq,fnnc,f) ⟷ Hfrc(P,leq,fnnc,f)"
  unfolding is_Hfrc_def Hfrc_def using pair_in_M_iff
  by auto

lemma Hfrc_at_abs:
  "⟦fnnc∈M; f∈M ; z∈M⟧ ⟹
   is_Hfrc_at(##M,P,leq,fnnc,f,z) ⟷  z = bool_of_o(Hfrc(P,leq,fnnc,f)) "
  unfolding is_Hfrc_at_def using Hfrc_abs
  by auto

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

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

lemma is_eclose_n_abs :
  assumes "x∈M" "ec∈M"
  shows "is_eclose_n(##M,is_name1,ec,x) ⟷ ec = eclose_n(name1,x)"
        "is_eclose_n(##M,is_name2,ec,x) ⟷ ec = eclose_n(name2,x)"
  unfolding is_eclose_n_def eclose_n_def
  using assms name1_abs name2_abs eclose_abs singletonM components_closed
  by auto


lemma is_ecloseN_abs :
  "⟦x∈M;ec∈M⟧ ⟹ is_ecloseN(##M,ec,x) ⟷ 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∈M ⟹ y∈M ⟹ frecR(x,y) ⟷ is_frecR(##M,x,y)" 
  unfolding frecR_def is_frecR_def using components_closed domain_closed by simp

lemma frecrelP_abs :
    "z∈M ⟹ frecrelP(##M,z) ⟷ (∃x y. z = <x,y> ∧ frecR(x,y))"
  using pair_in_M_iff frecR_abs unfolding frecrelP_def by auto

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

lemma frecrel_closed:
  assumes 
   "x∈M" 
 shows
   "frecrel(x)∈M" 
proof -
  have "Collect(x×x,λz. (∃x y. z = <x,y> ∧ frecR(x,y)))∈M"
    using Collect_in_M_0p[of "frecrelP_fm(0)"] arity_frecrelP_fm sats_frecrelP_fm
          frecrelP_abs ‹x∈M› 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))) ⊆ names_below(P,x)"
  unfolding frecrel_def
  using field_Rrel by simp

lemma forcerelD : "uv ∈ forcerel(P,x) ⟹ uv∈ names_below(P,x) × 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(<ft,n1,n2,p>,<a,b,c,d>)" "p∈P"
  shows "<ft,n1,n2,p> ∈ names_below(P,<a,b,c,d>)" (is "?x ∈ names_below(_,?y)")
proof -
  from assms
  have "ft ∈ 2" "a ∈ 2" 
    unfolding frecR_def by (auto simp add:components_simp)
  from assms
  consider (e) "n1 ∈ domain(b) ∪ domain(c) ∧ (n2 = b ∨ n2 =c)" 
    | (m) "n1 = b ∧ n2 ∈ domain(c)"
    unfolding frecR_def by (auto simp add:components_simp)
  then show ?thesis 
  proof cases
    case e
    then 
    have "n1 ∈ eclose(b) ∨ n1 ∈ eclose(c)"  
      using Un_iff in_dom_in_eclose by auto
    with e
    have "n1 ∈ ecloseN(?y)" "n2 ∈ ecloseN(?y)"
      using ecloseNI components_in_eclose by auto
    with ‹ft∈2› ‹p∈P› 
    show ?thesis unfolding names_below_def by  auto
  next
    case m
    then
    have "n1 ∈ ecloseN(?y)" "n2 ∈ ecloseN(?y)"
      using mem_eclose_trans  ecloseNI
            in_dom_in_eclose components_in_eclose by auto
    with ‹ft∈2› ‹p∈P› 
    show ?thesis unfolding names_below_def
      by auto    
  qed
qed

lemma names_below_tr : 
  assumes "x∈ names_below(P,y)" 
    "y∈ names_below(P,z)"
  shows "x∈ names_below(P,z)"
proof -
  let ?A="λy . names_below(P,y)"
  from assms
  obtain fx x1 x2 px where
    "x = <fx,x1,x2,px>" "fx∈2" "x1∈ecloseN(y)" "x2∈ecloseN(y)" "px∈P"
    unfolding names_below_def by auto
  from assms
  obtain fy y1 y2 py where
    "y = <fy,y1,y2,py>" "fy∈2" "y1∈ecloseN(z)" "y2∈ecloseN(z)" "py∈P"
    unfolding names_below_def by auto
    from ‹x1∈_› ‹x2∈_› ‹y1∈_› ‹y2∈_› ‹x=_› ‹y=_›
    have "x1∈ecloseN(z)" "x2∈ecloseN(z)"
      using ecloseN_mono names_simp by auto
    with ‹fx∈2› ‹px∈P› ‹x=_›
    have "x∈?A(z)" 
      unfolding names_below_def by simp
    then show ?thesis using subsetI by simp
qed

lemma arg_into_names_below2 :
  assumes "<x,y> ∈ frecrel(names_below(P,z))"
  shows  "x ∈ names_below(P,y)"
proof -
  {
  from assms
  have "x∈names_below(P,z)" "y∈names_below(P,z)" "frecR(x,y)"
    unfolding frecrel_def Rrel_def
    by auto
  obtain f n1 n2 p where
    A: "x = <f,n1,n2,p>" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈P" 
    using ‹x∈names_below(P,z)›
    unfolding names_below_def by auto
  obtain fy m1 m2 q where
      B: "q∈P" "y = <fy,m1,m2,q>"
    using ‹y∈names_below(P,z)›
    unfolding names_below_def by auto
  from A B ‹frecR(x,y)›
  have "x∈names_below(P,y)" using names_belowI by simp
  }
  then show ?thesis .
qed

lemma arg_into_names_below :
  assumes "<x,y> ∈ frecrel(names_below(P,z))"
  shows  "x ∈ names_below(P,x)"
proof -
  {
  from assms
  have "x∈names_below(P,z)"
    unfolding frecrel_def Rrel_def
    by auto
  from ‹x∈names_below(P,z)› 
  obtain f n1 n2 p where
    "x = <f,n1,n2,p>" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈P"
    unfolding names_below_def by auto
  then
  have "n1∈ecloseN(x)" "n2∈ecloseN(x)" 
    using components_in_eclose by simp_all
  with ‹f∈2› ‹p∈P› ‹x = <f,n1,n2,p>›
  have "x∈names_below(P,x)" 
    unfolding names_below_def by simp
  }
  then show ?thesis .
qed

lemma forcerel_arg_into_names_below :
  assumes "<x,y> ∈ forcerel(P,z)"
  shows  "x ∈ 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 "⟨x,y⟩ ∈ frecrel(names_below(P,z))"
  shows "names_below(P,x) ⊆ names_below(P,y)"
proof -
  from assms
  have "x∈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 "⟨x,y⟩ ∈ frecrel(names_below(P,z))"
  shows "frecrel(names_below(P,x)) ⊆ frecrel(names_below(P,y))"
  unfolding frecrel_def
  using Rrel_mono names_below_mono assms by simp

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

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

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

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

lemma forcerel_eq : 
  assumes "⟨z,x⟩ ∈ forcerel(P,x)"
  shows "forcerel(P,z) = forcerel(P,x) ∩ names_below(P,z)×names_below(P,z)"
  using assms aux forcerelD forcerel_mono[of z x x] subsetI 
  by auto

lemma forcerel_below_aux :
  assumes "<z,x> ∈ forcerel(P,x)" "<u,z> ∈ forcerel(P,x)"
  shows "u ∈ names_below(P,z)" 
  using assms(2)
  unfolding forcerel_def
proof(rule trancl_induct)
  show  "u ∈ names_below(P,y)" if " ⟨u, y⟩ ∈ frecrel(names_below(P, x))" for y
    using that vimage_singleton_iff arg_into_names_below2 by simp
next
  show "u ∈ names_below(P,z)" 
    if "⟨u, y⟩ ∈ frecrel(names_below(P, x))^+"
      "⟨y, z⟩ ∈ frecrel(names_below(P, x))"
      "u ∈ 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 "<z,x> ∈ forcerel(P,x)" 
  shows "forcerel(P,x) -`` {z} ⊆ 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,λ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 ∈ domain(b) ∨ n1 ∈ domain(c)" "p∈P" "d∈P"
  shows "⟨⟨1, n1, b, p⟩, ⟨0,b,c,d⟩⟩∈ forcerel(P,⟨0,b,c,d⟩)"
proof -
  let ?x="⟨1, n1, b, p⟩"
  let ?y="⟨0,b,c,d⟩"
  from assms
  have "frecR(?x,?y)"
    using frecRI1 by simp
  then
  have "?x∈names_below(P,?y)"  "?y ∈ names_below(P,?y)"
    using names_belowI  assms components_in_eclose 
    unfolding names_below_def by auto
  with ‹frecR(?x,?y)›
  show ?thesis
    unfolding forcerel_def frecrel_def
    using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
    by auto
qed

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

lemma forcerelI3 : 
  assumes "⟨n2, r⟩ ∈ c" "p∈P" "d∈P" "r ∈ P"
  shows "⟨⟨0, b, n2, p⟩,⟨1, b, c, d⟩⟩ ∈ forcerel(P,<1,b,c,d>)"
proof -
  let ?x="⟨0, b, n2, p⟩"
  let ?y="⟨1, b, c, d⟩"
  from assms
  have "frecR(?x,?y)"
    using assms frecRI3 by simp
  then
  have "?x∈names_below(P,?y)"  "?y ∈ names_below(P,?y)"
    using names_belowI  assms components_in_eclose 
    unfolding names_below_def by auto
  with ‹frecR(?x,?y)›
  show ?thesis
    unfolding forcerel_def frecrel_def 
      using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
    by auto
qed

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

lemma  aux_def_frc_at:
  assumes "z ∈ forcerel(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 "<z,x> ∈ forcerel(P,x)" 
    using vimage_singleton_iff by simp
  then 
  have "z ∈ ?A" 
    using forcerel_arg_into_names_below by simp
  from ‹<z,x> ∈ forcerel(P,x)›
  have E:"forcerel(P,z) = forcerel(P,x) ∩ (?A×?A)"
      "forcerel(P,x) -`` {z} ⊆ ?A" 
    using forcerel_eq forcerel_below
    by auto
  with ‹z∈?A›
  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‹Recursive expression of \<^term>‹frc_at››

lemma def_frc_at : 
  assumes "p∈P"
  shows
  "frc_at(P,leq,<ft,n1,n2,p>) =
   bool_of_o( p ∈P ∧ 
  (  ft = 0 ∧  (∀s. s∈domain(n1) ∪ domain(n2) ⟶
        (∀q. q∈P ∧ q ≼ p ⟶ (frc_at(P,leq,<1,s,n1,q>) =1 ⟷ frc_at(P,leq,<1,s,n2,q>) =1)))
   ∨ ft = 1 ∧ ( ∀v∈P. v ≼ p ⟶
    (∃q. ∃s. ∃r. r∈P ∧ q∈P ∧ q ≼ v ∧ <s,r> ∈ n2 ∧ q ≼ r ∧  frc_at(P,leq,<0,n1,s,q>) = 1))))"
proof -
  let ?r="λy. forcerel(P,y)" and ?Hf="λx f. bool_of_o(Hfrc(P,leq,x,f))"
  let ?t="λy. ?r(y) -`` {y}" 
  let ?arg="<ft,n1,n2,p>"
  from wf_forcerel 
  have wfr: "∀w . wf(?r(w))" ..
  with wfrec [of "?r(?arg)" ?arg ?Hf] 
  have "frc_at(P,leq,?arg) = ?Hf( ?arg, λx∈?r(?arg) -`` {?arg}. wfrec(?r(?arg), x, ?Hf))"
    using frc_at_trancl by simp 
  also
  have " ... = ?Hf( ?arg, λx∈?r(?arg) -`` {?arg}. frc_at(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‹Absoluteness of \<^term>‹frc_at››

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∈M" 
  shows 
    "forcerel(P,x)∈M" 
  unfolding forcerel_def def_frecrel names_below_def
proof -
  let ?Q = "2 × ecloseN(x) × ecloseN(x) × P"
  have "?Q × ?Q ∈ M"
    using ‹x∈M› P_in_M twoN_in_M ecloseN_closed cartprod_closed by simp
  moreover
  have "separation(##M,λz. ∃x y. z = ⟨x, y⟩ ∧ 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, λz. sats(M,frecrelP_fm(0) , [z]))"
      using separation_ax by simp
    moreover
    have "frecrelP(##M,z) ⟷ sats(M,frecrelP_fm(0),[z])" 
      if "z∈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)" "λz. ∃x y. z = ⟨x, y⟩ ∧ frecR(x, y)"]
      by simp
  qed
  ultimately
  show "{z ∈ ?Q × ?Q . ∃x y. z = ⟨x, y⟩ ∧ frecR(x, y)}^+ ∈ M" 
    using separation_closed frecrelP_abs trancl_closed by simp
qed
  
lemma relation2_Hfrc_at_abs:
  "relation2(##M,is_Hfrc_at(##M,P,leq),λx f. bool_of_o(Hfrc(P,leq,x,f)))"
  unfolding relation2_def using Hfrc_at_abs
  by simp

lemma Hfrc_at_closed :
  "∀x∈M. ∀g∈M. function(g) ⟶ bool_of_o(Hfrc(P,leq,x,g))∈M" 
  unfolding bool_of_o_def using zero_in_M n_in_M[of 1] by simp

lemma wfrec_Hfrc_at :
    assumes
      "X∈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) ⟷ 
        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∈M" "b∈M" "c∈M" "d∈M" "e∈M" "y∈M" "x∈M" "z∈M" 
    for a b c d e y x z
    using that P_in_M leq_in_M ‹X∈M› 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)]) ⟷
                   is_wfrec(##M, is_Hfrc_at(##M,P,leq),forcerel(P,X), x, y)"
    if "x∈M" "y∈M" "z∈M" for x y z
    using  that ‹X∈M› 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)]) ⟷
              (∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hfrc_at(##M,P,leq),forcerel(P,X), x, y))" 
    if "x∈M" "z∈M" for x z
    using that 1 ‹X∈M› 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∈formula"
      unfolding fm_defs Hfrc_at_fm_def by simp
    ultimately
  have "strong_replacement(##M,λx z. sats(M,?f,[x,z,P,leq,forcerel(P,X)]))"
    using replacement_ax 1 artyf ‹X∈M› forcerel_in_M P_in_M leq_in_M by simp
  then
  have "strong_replacement(##M,λx z.
          ∃y∈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 :
  "⟦Q∈M;x∈M;nb∈M⟧ ⟹ is_names_below(##M,Q,x,nb) ⟷ nb = names_below(Q,x)" 
  unfolding is_names_below_def names_below_def 
  using succ_in_M_iff zero_in_M cartprod_closed is_ecloseN_abs ecloseN_closed 
  by auto

lemma names_below_closed:
  "⟦Q∈M;x∈M⟧ ⟹ names_below(Q,x) ∈ M"
  unfolding names_below_def 
  using zero_in_M cartprod_closed ecloseN_closed succ_in_M_iff 
  by simp

lemma "names_below_productE" :
  " Q ∈ M ⟹
 x ∈ M ⟹ (⋀A1 A2 A3 A4. A1 ∈ M ⟹ A2 ∈ M ⟹ A3 ∈ M ⟹ A4 ∈ M ⟹ R(A1 × A2 × A3 × A4)) 
       ⟹ R(names_below(Q,x))" 
  unfolding names_below_def using zero_in_M ecloseN_closed[of x] twoN_in_M by auto

lemma forcerel_abs :
  "⟦x∈M;z∈M⟧ ⟹ is_forcerel(##M,P,x,z) ⟷ 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:"λp. is_frecrel(##M,p,_) ⟷  _ = frecrel(p)"] frecrel_closed
  by simp

lemma frc_at_abs:
  assumes "fnnc∈M" "z∈M" 
  shows "is_frc_at(##M,P,leq,fnnc,z) ⟷ z = frc_at(P,leq,fnnc)"
proof -
  from assms
  have "(∃r∈M. is_forcerel(##M,P,fnnc, r) ∧ is_wfrec(##M, is_Hfrc_at(##M, P, leq), r, fnnc, z))
        ⟷ 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)" "λx f. bool_of_o(Hfrc(P,leq,x,f))"]
  by (simp flip:setclass_iff)
qed

lemma forces_eq'_abs :
  "⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_eq'(##M,P,leq,p,t1,t2) ⟷ 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 :
  "⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_mem'(##M,P,leq,p,t1,t2) ⟷ 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∈M" "t1∈M" "t2∈M"
  shows 
    "is_forces_neq'(##M,P,leq,p,t1,t2) ⟷ forces_neq'(P,leq,p,t1,t2)"
proof -
  have "q∈M" if "q∈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∈M" "t1∈M" "t2∈M"
  shows 
    "is_forces_nmem'(##M,P,leq,p,t1,t2) ⟷ forces_nmem'(P,leq,p,t1,t2)"
proof -
  have "q∈M" if "q∈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‹Forcing for general formulas›

definition 
  ren_forces_nand :: "i⇒i" where
  "ren_forces_nand(φ) ≡ Exists(And(Equal(0,1),iterates(λp. incr_bv(p)`1 , 2, φ)))"

(*
sats(M, ren_forces_nand(φ),[q,p,P,leq,o] @ env) ⟷ sats(M, φ,[q,P,leq,o] @ env)"

Exists(Exists(Exists(Exists(
          And(Equal(3,4),And(Equal(0,5),And(Equal(1,6),
          And(Equal(2,7),iterates(λp. incr_bv(p)`4 , 5, φ)))))))))" 

sats(M, ren_forces_nand(φ),[q,P,leq,o,p] @ env) ⟷ sats(M, φ,[P,leq,o,q] @ env)"

  *) 

lemma ren_forces_nand_type[TC] :
  "φ∈formula ⟹ ren_forces_nand(φ) ∈formula" 
  unfolding ren_forces_nand_def
  by simp

lemma arity_ren_forces_nand : 
  assumes "φ∈formula" 
  shows "arity(ren_forces_nand(φ)) ≤ succ(arity(φ))"
proof -
  consider (lt) "1<arity(φ)" | (ge) "¬ 1 < arity(φ)"
    by auto
  then
  show ?thesis
  proof cases
    case lt
    with ‹φ∈_›
    have "2 < succ(arity(φ))" "2<arity(φ)#+2"
      using succ_ltI by auto
    with ‹φ∈_›
    have "arity(iterates(λp. incr_bv(p)`1,2,φ)) = 2#+arity(φ)"
      using arity_incr_bv_lemma lt
      by auto
    with ‹φ∈_›
    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 ‹φ∈_›
    have "arity(φ) ≤ 1" "pred(arity(φ)) ≤ 1"
      using not_lt_iff_le le_trans[OF le_pred]
      by simp_all
    with ‹φ∈_›
    have "arity(iterates(λp. incr_bv(p)`1,2,φ)) = (arity(φ))"
      using arity_incr_bv_lemma ge
      by simp
    with ‹arity(φ) ≤ 1› ‹φ∈_› ‹pred(_) ≤ 1›
    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 ∈ list(M) ⟹ φ∈formula ⟹ 
   sats(M, ren_forces_nand(φ),[q,p,P,leq,o] @ env) ⟷ sats(M, φ,[q,P,leq,o] @ env)"
  unfolding ren_forces_nand_def
  apply (insert sats_incr_bv_iff [of _ _ M _ "[q]"])
  apply simp
  done


definition
  ren_forces_forall :: "i⇒i" where
  "ren_forces_forall(φ) ≡ 
      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(λp. incr_bv(p)`5 , 5, φ)))))))))))" 

lemma arity_ren_forces_all : 
  assumes "φ∈formula"
  shows "arity(ren_forces_forall(φ)) = 5 ∪ arity(φ)"
proof -
  consider (lt) "5<arity(φ)" | (ge) "¬ 5 < arity(φ)"
    by auto
  then
  show ?thesis
  proof cases
    case lt
    with ‹φ∈_›
    have "5 < succ(arity(φ))" "5<arity(φ)#+2"  "5<arity(φ)#+3"  "5<arity(φ)#+4"
      using succ_ltI by auto
    with ‹φ∈_›
    have "arity(iterates(λp. incr_bv(p)`5,5,φ)) = 5#+arity(φ)"
      using arity_incr_bv_lemma lt
      by simp
    with ‹φ∈_›
    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 ‹φ∈_›
    have "arity(φ) ≤ 5" "pred^5(arity(φ)) ≤ 5"
      using not_lt_iff_le le_trans[OF le_pred]
      by simp_all
    with ‹φ∈_›
    have "arity(iterates(λp. incr_bv(p)`5,5,φ)) = arity(φ)"
      using arity_incr_bv_lemma ge
      by simp
    with ‹arity(φ) ≤ 5› ‹φ∈_› ‹pred^5(_) ≤ 5›
    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] :
  "φ∈formula ⟹ ren_forces_forall(φ) ∈formula" 
  unfolding ren_forces_forall_def by simp

lemma sats_ren_forces_forall :
  "[x,P,leq,o,p] @ env ∈ list(M) ⟹ φ∈formula ⟹ 
    sats(M, ren_forces_forall(φ),[x,p,P,leq,o] @ env) ⟷ sats(M, φ,[p,P,leq,o,x] @ env)"
  unfolding ren_forces_forall_def
  apply (insert sats_incr_bv_iff [of _ _ M _ "[p,P,leq,o,x]"])
  apply simp
  done

definition
  is_leq :: "[i⇒o,i,i,i] ⇒ o" where
  "is_leq(A,l,q,p) ≡ ∃qp[A]. (pair(A,q,p,qp) ∧ qp∈l)" 

lemma (in forcing_data) leq_abs[simp]:
  "⟦ l∈M ; q∈M ; p∈M ⟧ ⟹ is_leq(##M,l,q,p) ⟷ <q,p>∈l" 
  unfolding is_leq_def using pair_in_M_iff by simp


definition 
  leq_fm :: "[i,i,i] ⇒ i" where
  "leq_fm(leq,q,p) ≡ Exists(And(pair_fm(q#+1,p#+1,0),Member(0,leq#+1)))" 

lemma arity_leq_fm :
  "⟦leq∈nat;q∈nat;p∈nat⟧ ⟹ arity(leq_fm(leq,q,p)) = succ(q) ∪ succ(p) ∪ succ(leq)"
  unfolding leq_fm_def
  using arity_pair_fm pred_Un_distrib nat_simp_union
  by auto

lemma leq_fm_type[TC] :
  "⟦leq∈nat;q∈nat;p∈nat⟧ ⟹ leq_fm(leq,q,p)∈formula" 
  unfolding leq_fm_def by simp

lemma sats_leq_fm :
  "⟦ leq∈nat;q∈nat;p∈nat;env∈list(A) ⟧ ⟹ 
     sats(A,leq_fm(leq,q,p),env) ⟷ is_leq(##A,nth(leq,env),nth(q,env),nth(p,env))" 
  unfolding leq_fm_def is_leq_def by simp

subsubsection‹The primitive recursion›

consts forces' :: "i⇒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⇒i" where
  "forces(φ) ≡ And(Member(0,1),forces'(φ))"

lemma forces'_type [TC]:  "φ∈formula ⟹ forces'(φ) ∈ formula" 
  by (induct φ set:formula; simp)

lemma forces_type[TC] : "φ∈formula ⟹ forces(φ) ∈ formula"
  unfolding forces_def by simp

context forcing_data
begin

subsection‹Forcing for atomic formulas in context›

definition
  forces_eq :: "[i,i,i] ⇒ o" where
  "forces_eq ≡ forces_eq'(P,leq)"

definition
  forces_mem :: "[i,i,i] ⇒ o" where
  "forces_mem ≡ forces_mem'(P,leq)"

(* frc_at(P,leq,<0,t1,t2,p>) = 1*) 
definition
  is_forces_eq :: "[i,i,i] ⇒ o" where
  "is_forces_eq ≡ is_forces_eq'(##M,P,leq)"

(* frc_at(P,leq,<1,t1,t2,p>) = 1*) 
definition
  is_forces_mem :: "[i,i,i] ⇒ o" where
  "is_forces_mem ≡ is_forces_mem'(##M,P,leq)"


lemma def_forces_eq: "p∈P ⟹ forces_eq(p,t1,t2) ⟷ 
      (∀s∈domain(t1) ∪ domain(t2). ∀q. q∈P ∧ q ≼ p ⟶ 
      (forces_mem(q,s,t1) ⟷ 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∈P ⟹ forces_mem(p,t1,t2) ⟷ 
     (∀v∈P. v ≼ p ⟶
      (∃q. ∃s. ∃r. r∈P ∧ q∈P ∧ q ≼ v ∧ <s,r> ∈ t2 ∧ q ≼ r ∧ 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 :
  "⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_eq(p,t1,t2) ⟷ forces_eq(p,t1,t2)"
  unfolding is_forces_eq_def forces_eq_def
  using forces_eq'_abs by simp

lemma forces_mem_abs :
  "⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_mem(p,t1,t2) ⟷ 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∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat"  "env∈list(M)" 
           "nth(p,env)=P" "nth(l,env)=leq" 
  shows "sats(M,forces_eq_fm(p,l,q,t1,t2),env) ⟷ 
         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∈nat" "l∈nat" "q∈nat" "t1∈nat" "t2∈nat"  "env∈list(M)"
           "nth(p,env)=P" "nth(l,env)=leq"
  shows "sats(M,forces_mem_fm(p,l,q,t1,t2),env) ⟷ 
             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] ⇒ o" where
  "forces_neq(p,t1,t2) ≡ ¬ (∃q∈P. q≼p ∧ forces_eq(q,t1,t2))"

definition
  forces_nmem :: "[i,i,i] ⇒ o" where
  "forces_nmem(p,t1,t2) ≡ ¬ (∃q∈P. q≼p ∧ forces_mem(q,t1,t2))"


lemma forces_neq :
  "forces_neq(p,t1,t2) ⟷ 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) ⟷ 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∈nat" "y∈nat" "env∈list(M)"
           "nth(x,env)=xx" "nth(y,env)=yy" "q∈M" 
         shows "sats(M,forces(Member(x,y)),[q,P,leq,one]@env) ⟷ 
                (q∈P ∧ 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∈nat" "y∈nat" "env∈list(M)"
           "nth(x,env)=xx" "nth(y,env)=yy" "q∈M" 
         shows "sats(M,forces(Equal(x,y)),[q,P,leq,one]@env) ⟷ 
                (q∈P ∧ 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  "φ∈formula" "ψ∈formula" "env∈list(M)" "p∈M" 
  shows "sats(M,forces(Nand(φ,ψ)),[p,P,leq,one]@env) ⟷ 
         (p∈P ∧ ¬(∃q∈M. q∈P ∧ is_leq(##M,leq,q,p) ∧ 
               (sats(M,forces'(φ),[q,P,leq,one]@env) ∧ sats(M,forces'(ψ),[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  "φ∈formula" "env∈list(M)" "p∈M" 
  shows "sats(M,forces(Neg(φ)),[p,P,leq,one]@env) ⟷ 
         (p∈P ∧ ¬(∃q∈M. q∈P ∧ is_leq(##M,leq,q,p) ∧ 
               (sats(M,forces'(φ),[q,P,leq,one]@env))))"
  unfolding Neg_def using assms sats_forces_Nand
  by simp

lemma sats_forces_Forall :
  assumes  "φ∈formula" "env∈list(M)" "p∈M" 
  shows "sats(M,forces(Forall(φ)),[p,P,leq,one]@env) ⟷ 
         p∈P ∧ (∀x∈M. sats(M,forces'(φ),[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‹The arity of \<^term>‹forces››

lemma arity_forces_at:
  assumes  "x ∈ nat" "y ∈ nat"
  shows "arity(forces(Member(x, y))) = (succ(x) ∪ succ(y)) #+ 4"
        "arity(forces(Equal(x, y))) = (succ(x) ∪ 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 "φ∈formula"
  shows "arity(forces'(φ)) ≤ arity(φ) #+ 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 φ ψ)
  let ?φ' = "ren_forces_nand(forces'(φ))"
  let ?ψ' = "ren_forces_nand(forces'(ψ))"
  have "arity(leq_fm(3, 0, 1)) = 4"
    using arity_leq_fm succ_Un_distrib nat_simp_union
    by simp
  have "3 ≤ (4#+arity(φ)) ∪ (4#+arity(ψ))" (is "_ ≤ ?rhs")
    using nat_simp_union by simp
  from ‹φ∈_› Nand
  have "pred(arity(?φ')) ≤ ?rhs"  "pred(arity(?ψ')) ≤ ?rhs"
  proof -
    from ‹φ∈_› ‹ψ∈_›
    have A:"pred(arity(?φ')) ≤ arity(forces'(φ))"
           "pred(arity(?ψ')) ≤ arity(forces'(ψ))"
      using pred_mono[OF _  arity_ren_forces_nand] pred_succ_eq 
      by simp_all
    from Nand
    have "3 ∪ arity(forces'(φ)) ≤ arity(φ) #+ 4"
         "3 ∪ arity(forces'(ψ)) ≤ arity(ψ) #+ 4"
      using Un_le by simp_all
    with Nand
    show "pred(arity(?φ')) ≤ ?rhs"
         "pred(arity(?ψ')) ≤ ?rhs"
      using le_trans[OF A(1)] le_trans[OF A(2)] le_Un_iff
      by simp_all
  qed
  with Nand ‹_=4›
  show ?case 
    using pred_Un_distrib Un_assoc[symmetric] succ_Un_distrib nat_union_abs1 Un_leI3[OF ‹3 ≤ ?rhs›]
    by simp
next
  case (Forall φ)
  let ?φ' = "ren_forces_forall(forces'(φ))"
  show ?case
  proof (cases "arity(φ) = 0")
    case True
    with Forall
    show ?thesis
    proof -
      from Forall True
      have "arity(forces'(φ)) ≤ 5"
        using le_trans[of _ 4 5] by auto
      with ‹φ∈_›
      have "arity(?φ') ≤ 5"
        using arity_ren_forces_all[OF forces'_type[OF ‹φ∈_›]] nat_union_abs2
        by auto
      with Forall True
      show ?thesis
        using pred_mono[OF _ ‹arity(?φ') ≤ 5›]
        by simp
    qed
  next
    case False
    with Forall
    show ?thesis
    proof -
      from Forall False
      have "arity(?φ') = 5 ∪ arity(forces'(φ))"
           "arity(forces'(φ)) ≤ 5 #+ arity(φ)"
           "4 ≤ succ(succ(succ(arity(φ))))"
        using Ord_0_lt arity_ren_forces_all
          le_trans[OF _ add_le_mono[of 4 5, OF _ le_refl]]
        by auto
      with ‹φ∈_›
      have "5 ∪ arity(forces'(φ)) ≤ 5#+arity(φ)"
        using nat_simp_union by auto
      with ‹φ∈_› ‹arity(?φ') = 5 ∪ _›
      show ?thesis
        using pred_Un_distrib succ_pred_eq[OF _ ‹arity(φ)≠0›]
          pred_mono[OF _ Forall(2)] Un_le[OF ‹4≤succ(_)›]
      by simp
  qed
qed
qed

lemma arity_forces : 
  assumes "φ∈formula"
  shows "arity(forces(φ)) ≤ 4#+arity(φ)" 
  unfolding forces_def
  using assms arity_forces' le_trans nat_simp_union by auto

lemma arity_forces_le :
  assumes "φ∈formula" "n∈nat" "arity(φ) ≤ n"
  shows "arity(forces(φ)) ≤ 4#+n"
  using assms le_trans[OF _ add_le_mono[OF le_refl[of 5] ‹arity(φ)≤_›]] arity_forces
  by auto

end