Theory Fm_Definitions

sectionConcepts involved in instances of Replacement
theory Fm_Definitions
  imports
    Transitive_Models.Renaming_Auto
    Transitive_Models.Aleph_Relative
    FrecR_Arities
begin

(* Really, I have no idea why is this needed again. At the end of the
   imported theories, notation works just fine. *)
no_notation Aleph (_ [90] 90)

textIn this theory we put every concept that should be synthesized in a formula
to have an instance of replacement.

The automatic synthesis of a concept /foo/ requires that every concept used to
define /foo/ is already synthesized. We try to use our meta-programs to synthesize
concepts: given the absolute concept /foo/ we relativize in relational form
obtaining /is\_foo/ and the we synthesize the formula /is\_foo\_fm/.
The meta-program that synthesizes formulas also produce satisfactions lemmas.

Having one file to collect every formula needed for replacements breaks
the reading flow: we need to introduce the concept in this theory in order
to use the meta-programs; moreover there are some concepts for which we prove
here the satisfaction lemmas manually, while for others we prove them
on its theory.


declare arity_subset_fm [simp del] arity_ordinal_fm[simp del, arity] arity_transset_fm[simp del]
  FOL_arities[simp del]

synthesize "setdiff" from_definition "setdiff" assuming "nonempty"
arity_theorem for "setdiff_fm"

synthesize "is_converse" from_definition assuming "nonempty"
arity_theorem for "is_converse_fm"

relationalize "first_rel" "is_first" external
synthesize "first_fm" from_definition "is_first" assuming "nonempty"

relationalize "minimum_rel" "is_minimum" external
definition is_minimum' where
  "is_minimum'(M,R,X,u)  (M(u)  u  X  (v[M]. a[M]. (v  X  v  u  a  R)  pair(M, u, v, a))) 
    (x[M].
        (M(x)  x  X  (v[M]. a[M]. (v  X  v  x  a  R)  pair(M, x, v, a))) 
        (y[M]. M(y)  y  X  (v[M]. a[M]. (v  X  v  y  a  R)  pair(M, y, v, a))  y = x)) 
    ¬ (x[M]. (M(x)  x  X  (v[M]. a[M]. (v  X  v  x  a  R)  pair(M, x, v, a))) 
               (y[M]. M(y)  y  X  (v[M]. a[M]. (v  X  v  y  a  R)  pair(M, y, v, a))  y = x)) 
    empty(M, u)"

synthesize "minimum" from_definition "is_minimum'" assuming "nonempty"
arity_theorem for "minimum_fm"

lemma is_lambda_iff_sats[iff_sats]:
  assumes is_F_iff_sats:
    "!!a0 a1 a2.
        [|a0Aa; a1Aa; a2Aa|]
        ==> is_F(a1, a0)  sats(Aa, is_F_fm, Cons(a0,Cons(a1,Cons(a2,env))))"
  shows
    "nth(A, env) = Ab 
    nth(r, env) = ra 
    A  nat 
    r  nat 
    env  list(Aa) 
    is_lambda(##Aa, Ab, is_F, ra)  Aa, env  lambda_fm(is_F_fm,A, r)"
  using sats_lambda_fm[OF assms, of A r] by simp

― ‹same as @{thm [source] sats_is_wfrec_fm}, but changing length assumptions to
    term0 being in the model
lemma sats_is_wfrec_fm':
  assumes MH_iff_sats:
    "!!a0 a1 a2 a3 a4.
        [|a0A; a1A; a2A; a3A; a4A|]
        ==> MH(a2, a1, a0)  sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
  shows
    "[|x  nat; y  nat; z  nat; env  list(A); 0  A|]
       ==> sats(A, is_wfrec_fm(p,x,y,z), env) 
           is_wfrec(##A, MH, nth(x,env), nth(y,env), nth(z,env))"
  using MH_iff_sats [THEN iff_sym] nth_closed sats_is_recfun_fm
  by (simp add: is_wfrec_fm_def is_wfrec_def) blast

lemma is_wfrec_iff_sats'[iff_sats]:
  assumes MH_iff_sats:
    "!!a0 a1 a2 a3 a4.
        [|a0Aa; a1Aa; a2Aa; a3Aa; a4Aa|]
        ==> MH(a2, a1, a0)  sats(Aa, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
    "nth(x, env) = xx" "nth(y, env) = yy" "nth(z, env) = zz"
    "x  nat" "y  nat" "z  nat" "env  list(Aa)" "0  Aa"
  shows
    "is_wfrec(##Aa, MH, xx, yy, zz)  Aa, env  is_wfrec_fm(p,x,y,z)"
  using assms(2-4) sats_is_wfrec_fm'[OF assms(1,5-9)] by simp

lemma is_wfrec_on_iff_sats[iff_sats]:
  assumes MH_iff_sats:
    "!!a0 a1 a2 a3 a4.
        [|a0Aa; a1Aa; a2Aa; a3Aa; a4Aa|]
        ==> MH(a2, a1, a0)  sats(Aa, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
  shows
    "nth(x, env) = xx 
    nth(y, env) = yy 
    nth(z, env) = zz 
    x  nat 
    y  nat 
    z  nat 
    env  list(Aa) 
    0  Aa  is_wfrec_on(##Aa, MH, aa,xx, yy, zz)  Aa, env  is_wfrec_fm(p,x,y,z)"
  using assms sats_is_wfrec_fm'[OF assms] unfolding is_wfrec_on_def by simp

textFormulas for particular replacement instances

textNow we introduce some definitions used in the definition of check; which
is defined by well-founded recursion using replacement in the recursive call.

― ‹The well-founded relation for defining check.›
definition
  rcheck :: "i  i" where
  "rcheck(x)  Memrel(eclose({x}))^+"

relativize "rcheck" "is_rcheck"
synthesize "is_rcheck" from_definition
arity_theorem for "is_rcheck_fm"

― ‹The function used for the replacement.
definition
  PHcheck :: "[io,i,i,i,i]  o" where
  "PHcheck(M,o,f,y,p)  M(p)  (fy[M]. fun_apply(M,f,y,fy)  pair(M,fy,o,p))"

synthesize "PHcheck" from_definition assuming "nonempty"
arity_theorem for "PHcheck_fm"

― ‹The recursive call for check. We could use the meta-program relationalize for
this; but it makes some proofs more involved.
definition
  is_Hcheck :: "[io,i,i,i,i]  o" where
  "is_Hcheck(M,o,z,f,hc)   is_Replace(M,z,PHcheck(M,o,f),hc)"

synthesize "is_Hcheck" from_definition assuming "nonempty"

lemma arity_is_Hcheck_fm:
  assumes "mnat" "nnat" "pnat" "onat"
  shows "arity(is_Hcheck_fm(m,n,p,o)) = succ(o)  succ(n)  succ(p)  succ(m) "
  unfolding is_Hcheck_fm_def
  using assms arity_Replace_fm[rule_format,OF PHcheck_fm_type _ _ _ arity_PHcheck_fm]
    pred_Un_distrib Un_assoc Un_nat_type
  by simp

― ‹The relational version of check is hand-made because our automatic tool
does not handle termwfrec.
definition
  is_check :: "[io,i,i,i]  o" where
  "is_check(M,o,x,z)  rch[M]. is_rcheck(M,x,rch) 
      is_wfrec(M,is_Hcheck(M,o),rch,x,z)"

― ‹Finally, we internalize the formula.
definition
  check_fm :: "[i,i,i]  i" where
  "check_fm(o,x,z)  Exists(And(is_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]: "xnat  onat  znat  check_fm(x,o,z)  formula"
  by (simp add:check_fm_def)

lemma sats_check_fm :
  assumes
    "onat" "xnat" "znat" "envlist(M)" "0M"
  shows
    "(M , env  check_fm(o,x,z))  is_check(##M,nth(o,env),nth(x,env),nth(z,env))"
proof -
  have sats_is_Hcheck_fm:
    "a0 a1 a2 a3 a4 a6.  a0M; a1M; a2M; a3M; a4M;a6 M 
         is_Hcheck(##M,a6,a2, a1, a0) 
         (M , [a0,a1,a2,a3,a4,r,a6]@env  is_Hcheck_fm(6,2,1,0))" if "rM" for r
    using that assms
    by simp
  then
  have "(M , [r]@env  is_wfrec_fm(is_Hcheck_fm(6+ωo,2,1,0),0,1+ωx,1+ωz))
         is_wfrec(##M,is_Hcheck(##M,nth(o,env)),r,nth(x,env),nth(z,env))"
    if "rM" for r
    using that assms is_wfrec_iff_sats'[symmetric]
    by simp
  then
  show ?thesis
    unfolding is_check_def check_fm_def
    using assms is_rcheck_iff_sats[symmetric]
    by simp
qed

lemma iff_sats_check_fm[iff_sats] :
  assumes
    "nth(o, env) = oa" "nth(x, env) = xa" "nth(z, env) = za" "o  nat" "x  nat" "z  nat" "env  list(A)" "0  A"
  shows "is_check(##A, oa,xa, za)  A, env  check_fm(o,x,z)"
  using assms sats_check_fm[symmetric]
  by auto

lemma arity_check_fm[arity]:
  assumes "mnat" "nnat" "onat"
  shows "arity(check_fm(m,n,o)) = succ(o)  succ(n)  succ(m) "
  unfolding check_fm_def
  using assms arity_is_wfrec_fm[rule_format,OF _ _ _ _ _ arity_is_Hcheck_fm]
    pred_Un_distrib Un_assoc arity_tran_closure_fm
  by (auto simp add:arity)

notation check_fm (_v_ is _)

― ‹The pair of elements belongs to some set. The intended set is the preorder.
definition
  is_leq :: "[io,i,i,i]  o" where
  "is_leq(A,l,q,p)  qp[A]. (pair(A,q,p,qp)  qpl)"

synthesize "is_leq" from_definition assuming "nonempty"
arity_theorem for "is_leq_fm"

abbreviation
  fm_leq :: "[i,i,i]  i" (_≼⇗__) where
  "fm_leq(A,l,B)  is_leq_fm(l,A,B)"

subsectionFormulas used to prove some generic instances.

definition ρ_repl :: "ii" where
  "ρ_repl(l)  rsum({0, 1, 1, 0}, id(l), 2, 3, l)"

lemma f_type : "{0, 1, 1, 0}  2  3"
  using Pi_iff unfolding function_def by auto

― ‹thmInternalize.sum_type› clashes with thmRenaming.sum_type›.
hide_fact Internalize.sum_type

lemma ren_type :
  assumes "lnat"
  shows "ρ_repl(l) : 2+ωl  3+ωl"
  using sum_type[of 2 3 l l "{0, 1, 1, 0}" "id(l)"] f_type assms id_type
  unfolding ρ_repl_def by auto

definition Lambda_in_M_fm where [simp]:"Lambda_in_M_fm(φ,len) 
  (⋅∃pair_fm(1, 0, 2) 
   ren(φ) ` (2 +ω len) ` (3 +ω len) ` ρ_repl(len) ⋅)  0  len +ω 2"

lemma Lambda_in_M_fm_type[TC]: "φformula  lennat  Lambda_in_M_fm(φ,len) formula"
  using ren_tc[of φ "2+ωlen" "3+ωlen" "ρ_repl(len)"] ren_type
  unfolding Lambda_in_M_fm_def
  by simp

definition ρ_pair_repl :: "ii" where
  "ρ_pair_repl(l)  rsum({0, 0, 1, 1, 2, 3}, id(l), 3, 4, l)"

definition LambdaPair_in_M_fm where "LambdaPair_in_M_fm(φ,len) 
  (⋅∃pair_fm(1, 0, 2) 
             ren((⋅∃(⋅∃⋅fst(2) is 0  ⋅snd(2) is 1  ren(φ) ` (3 +ω len) ` (4 +ω len) ` ρ_pair_repl(len) ⋅)⋅)) ` (2 +ω len) `
             (3 +ω len) `
             ρ_repl(len) ⋅) 
          0  len +ω 2 "

lemma f_type' : "{0,0 , 1, 1, 2, 3}  3  4"
  using Pi_iff unfolding function_def by auto

lemma ren_type' :
  assumes "lnat"
  shows "ρ_pair_repl(l) : 3+ωl  4+ωl"
  using sum_type[of 3 4 l l "{0, 0, 1, 1, 2, 3}" "id(l)"] f_type' assms id_type
  unfolding ρ_pair_repl_def by auto

lemma LambdaPair_in_M_fm_type[TC]: "φformula  lennat  LambdaPair_in_M_fm(φ,len) formula"
  using ren_tc[OF _ _ _ ren_type',of φ "len"] Lambda_in_M_fm_type
  unfolding LambdaPair_in_M_fm_def
  by simp

subsectionThe relation termfrecrel

definition
  frecrelP :: "[io,i]  o" where
  "frecrelP(M,xy)  (x[M]. y[M]. pair(M,x,y,xy)  is_frecR(M,x,y))"

synthesize "frecrelP" from_definition
arity_theorem for "frecrelP_fm"

definition
  is_frecrel :: "[io,i,i]  o" where
  "is_frecrel(M,A,r)  A2[M]. cartprod(M,A,A,A2)  is_Collect(M,A2, frecrelP(M) ,r)"

synthesize "frecrel" from_definition "is_frecrel"
arity_theorem for "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" "f2" "n1ecloseN(z)" "n2ecloseN(z)" "pP"
  using assms unfolding names_below_def by auto

synthesize "number2" from_definition

lemma number2_iff :
  "(A)(c)  number2(A,c)  (b[A]. a[A]. successor(A, b, c)  successor(A, a, b)  empty(A, a))"
  unfolding number2_def number1_def by auto
arity_theorem for "number2_fm"

reldb_add "ecloseN" "is_ecloseN"
relativize "names_below" "is_names_below"
synthesize "is_names_below" from_definition
arity_theorem for "is_names_below_fm"

definition
  is_tuple :: "[io,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)"

synthesize "is_tuple" from_definition
arity_theorem for "is_tuple_fm"

subsectionDefinition of Forces

subsubsectionDefinition of termforces for equality and membership
text$p\forces \tau = \theta$ if for every $q\leqslant p$ both $q\forces \sigma \in \tau$
and $q\forces \sigma \in \theta$ hold for all $\sigma \in \dom(\tau)\cup \dom(\theta)$.
definition
  eq_case :: "[i,i,i,i,i,i]  o" where
  "eq_case(τ,θ,p,P,leq,f)  σ. σ  domain(τ)  domain(θ) 
      (q. qP  q,pleq  (f`1,σ,τ,q=1   f`1,σ,θ,q =1))"

relativize "eq_case" "is_eq_case"
synthesize "eq_case" from_definition "is_eq_case"

text$p\forces \tau \in \theta$ if for every $v\leqslant p$
  there exist $q$, $r$, and $\sigma$ such that
  $v\leqslant q$, $q\leqslant r$, $\langle \sigma,r\rangle \in \tau$, and
  $q\forces \pi = \sigma$.
definition
  mem_case :: "[i,i,i,i,i,i]  o" where
  "mem_case(τ,θ,p,P,leq,f)  vP. v,pleq 
    (q. σ. r. rP  qP  q,vleq  σ,r  θ  q,rleq   f`0,τ,σ,q = 1)"

relativize "mem_case" "is_mem_case"
synthesize "mem_case" from_definition "is_mem_case"
arity_theorem intermediate for "eq_case_fm"
lemma arity_eq_case_fm[arity]:
  assumes
    "n1nat" "n2nat" "pnat" "Pnat" "leqnat" "fnat"
  shows
    "arity(eq_case_fm(n1,n2,p,P,leq,f)) =
    succ(n1)  succ(n2)  succ(p)  succ(P)  succ(leq)  succ(f)"
  using assms arity_eq_case_fm'
  by auto

arity_theorem intermediate for "mem_case_fm"
lemma arity_mem_case_fm[arity] :
  assumes
    "n1nat" "n2nat" "pnat" "Pnat" "leqnat" "fnat"
  shows
    "arity(mem_case_fm(n1,n2,p,P,leq,f)) =
    succ(n1)  succ(n2)  succ(p)  succ(P)  succ(leq)  succ(f)"
  using assms arity_mem_case_fm'
  by auto

definition
  Hfrc :: "[i,i,i,i]  o" where
  "Hfrc(P,leq,fnnc,f)  ft. τ. θ. p. pP  fnnc = ft,τ,θ,p 
     (  ft = 0   eq_case(τ,θ,p,P,leq,f)
       ft = 1  mem_case(τ,θ,p,P,leq,f))"

relativize "Hfrc" "is_Hfrc"
synthesize "Hfrc" from_definition "is_Hfrc"

definition
  is_Hfrc_at :: "[io,i,i,i,i,i]  o" where
  "is_Hfrc_at(M,P,leq,fnnc,f,b) 
            (empty(M,b)  ¬ is_Hfrc(M,P,leq,fnnc,f))
           (number1(M,b)  is_Hfrc(M,P,leq,fnnc,f))"

synthesize "Hfrc_at" from_definition "is_Hfrc_at"
arity_theorem intermediate for "Hfrc_fm"

lemma arity_Hfrc_fm[arity] :
  assumes
    "Pnat" "leqnat" "fnncnat" "fnat"
  shows
    "arity(Hfrc_fm(P,leq,fnnc,f)) = succ(P)  succ(leq)  succ(fnnc)  succ(f)"
  using assms arity_Hfrc_fm'
  by auto

arity_theorem for "Hfrc_at_fm"

subsubsectionThe well-founded relation termforcerel
definition
  forcerel :: "i  i  i" where
  "forcerel(P,x)  frecrel(names_below(P,x))^+"

definition
  is_forcerel :: "[io,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))"
synthesize "is_forcerel" from_definition
arity_theorem for "is_forcerel_fm"

subsectiontermfrc_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)))"

― ‹The relational form is defined manually because it uses termwfrec.
definition
  is_frc_at :: "[io,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)"

definition
  frc_at_fm :: "[i,i,i,i]  i" where
  "frc_at_fm(p,l,x,z)  Exists(And(is_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] :
  "pnat;lnat;xnat;znat  frc_at_fm(p,l,x,z)formula"
  unfolding frc_at_fm_def by simp

lemma arity_frc_at_fm[arity] :
  assumes "pnat" "lnat" "xnat" "znat"
  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)"
  note assms
  moreover from this
  have  "arity() = (7+ωp)  (7+ωl)" "  formula"
    using arity_Hfrc_at_fm ord_simp_union
    by auto
  moreover from calculation
  have "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
      union_abs1
    by auto
  moreover from assms
  have "arity(is_forcerel_fm(succ(p),succ(x),0)) = 2+ωp  (2+ωx)"
    using arity_is_forcerel_fm ord_simp_union
    by auto
  ultimately
  show ?thesis
    unfolding frc_at_fm_def
    using arity_is_forcerel_fm pred_Un_distrib
    by (auto simp:FOL_arities)
qed

lemma sats_frc_at_fm :
  assumes
    "pnat" "lnat" "inat" "jnat" "envlist(A)" "i < length(env)" "j < length(env)"
  shows
    "(A , env  frc_at_fm(p,l,i,j)) 
     is_frc_at(##A,nth(p,env),nth(l,env),nth(i,env),nth(j,env))"
proof -
  {
    fix r pp ll
    assume "rA"
    have "is_Hfrc_at(##A,nth(p,env),nth(l,env),a2, a1, a0) 
         (A, [a0,a1,a2,a3,a4,r]@env  Hfrc_at_fm(6+ωp,6+ωl,2,1,0))"
      if "a0A" "a1A" "a2A" "a3A" "a4A" for a0 a1 a2 a3 a4
      using  that assms rA
        Hfrc_at_iff_sats[of "6+ωp" "6+ωl" 2 1 0 "[a0,a1,a2,a3,a4,r]@env" A]  by simp
    with rA
    have "(A,[r]@env  is_wfrec_fm(Hfrc_at_fm(6+ωp, 6+ωl,2,1,0),0, i+ω1, j+ω1)) 
         is_wfrec(##A, is_Hfrc_at(##A, nth(p,env), nth(l,env)), r,nth(i, env), nth(j, env))"
      using assms sats_is_wfrec_fm
      by simp
  }
  moreover
  have "(A, Cons(r, env)  is_forcerel_fm(succ(p), succ(i), 0)) 
        is_forcerel(##A,nth(p,env),nth(i,env),r)" if "rA" for r
    using assms sats_is_forcerel_fm that
    by simp
  ultimately
  show ?thesis
    unfolding is_frc_at_def frc_at_fm_def
    using assms
    by simp
qed

lemma frc_at_fm_iff_sats:
  assumes "nth(i,env) = w" "nth(j,env) = x" "nth(k,env) = y" "nth(l,env) = z"
    "i  nat" "j  nat" "k  nat" "lnat" "env  list(A)" "k<length(env)" "l<length(env)"
  shows "is_frc_at(##A, w, x, y,z)  (A , env  frc_at_fm(i,j,k,l))"
  using assms sats_frc_at_fm
  by simp

declare frc_at_fm_iff_sats [iff_sats]

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)  ¬ (qP. q,pl  forces_eq'(P,l,q,t1,t2))"

definition
  forces_nmem' :: "[i,i,i,i,i]  o" where
  "forces_nmem'(P,l,p,t1,t2)  ¬ (qP. q,pl  forces_mem'(P,l,q,t1,t2))"

― ‹The following definitions are explicitly defined to avoid the expansion
of concepts.
definition
  is_forces_eq' :: "[io,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)"

definition
  is_forces_mem' :: "[io,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' :: "[io,i,i,i,i,i]  o" where
  "is_forces_neq'(M,P,l,p,t1,t2) 
      ¬ (q[M]. qP  (qp[M]. pair(M,q,p,qp)  qpl  is_forces_eq'(M,P,l,q,t1,t2)))"

definition
  is_forces_nmem' :: "[io,i,i,i,i,i]  o" where
  "is_forces_nmem'(M,P,l,p,t1,t2) 
      ¬ (q[M]. qp[M]. qP  pair(M,q,p,qp)  qpl  is_forces_mem'(M,P,l,q,t1,t2))"

synthesize "forces_eq" from_definition "is_forces_eq'"
synthesize "forces_mem" from_definition "is_forces_mem'"
synthesize "forces_neq" from_definition "is_forces_neq'" assuming "nonempty"
synthesize "forces_nmem" from_definition "is_forces_nmem'" assuming "nonempty"

context
  notes Un_assoc[simp] Un_trasposition_aux2[simp]
begin
arity_theorem for "forces_eq_fm"
arity_theorem for "forces_mem_fm"
arity_theorem for "forces_neq_fm"
arity_theorem for "forces_nmem_fm"
end

subsectionForcing for general formulas

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

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 union_abs1 Un_assoc[symmetric] Un_le_compat
      by (simp add:FOL_arities)
  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 union_abs1 Un_assoc[symmetric] union_abs2
      by (simp add:FOL_arities)
  qed
qed

lemma sats_ren_forces_nand:
  "[q,P,leq,o,p] @ env  list(M)  φformula 
   (M, [q,p,P,leq,o] @ env  ren_forces_nand(φ))  (M, [q,P,leq,o] @ env  φ)"
  unfolding ren_forces_nand_def
  using sats_incr_bv_iff [of _ _ M _ "[q]"]
  by simp


definition
  ren_forces_forall :: "ii" 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 union_abs1 Un_assoc[symmetric] union_abs2
      by (simp add:FOL_arities)
  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 union_abs1 Un_assoc[symmetric] union_abs2
      by (simp add:FOL_arities)
  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 
    (M, [x,p,P,leq,o] @ env  ren_forces_forall(φ))  (M, [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

subsubsectionThe primitive recursion

consts forces' :: "ii"
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(is_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 :: "ii" 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

subsectionThe arity of termforces

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 ord_simp_union
  by (auto simp:FOL_arities,(rule_tac le_anti_sym,simp_all,(rule_tac not_le_anti_sym,simp_all))+)

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 ord_simp_union leI not_le_iff_lt
    by simp
next
  case (Equal x y)
  then
  show ?case
    using arity_forces_eq_fm succ_Un_distrib ord_simp_union leI not_le_iff_lt
    by simp
next
  case (Nand φ ψ)
  let ?φ' = "ren_forces_nand(forces'(φ))"
  let ?ψ' = "ren_forces_nand(forces'(ψ))"
  have "arity(is_leq_fm(3, 0, 1)) = 4"
    using arity_is_leq_fm succ_Un_distrib ord_simp_union
    by simp
  have "3  (4+ωarity(φ))  (4+ωarity(ψ))" (is "_  ?rhs")
    using ord_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 union_abs1 Un_leI3[OF 3  ?rhs]
    by (simp add:FOL_arities)
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 φ_]] 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  3+ω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 ord_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 43+ωarity(φ)]
        by simp
    qed
  qed
qed

lemma arity_forces :
  assumes "φformula"
  shows "arity(forces(φ))  4+ωarity(φ)"
  unfolding forces_def
  using assms arity_forces' le_trans ord_simp_union FOL_arities by auto

lemma arity_forces_le :
  assumes "φformula" "nnat" "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

definition rename_split_fm where
  "rename_split_fm(φ)  (⋅∃(⋅∃(⋅∃(⋅∃(⋅∃(⋅∃⋅snd(9) is 0  ⋅fst(9) is 4  1=11 
    2=12  3=13  5=7 
    (λp. incr_bv(p)`6)^8(forces(φ)) ⋅)⋅)⋅)⋅)⋅)⋅)"

lemma rename_split_fm_type[TC]: "φformula  rename_split_fm(φ)formula"
  unfolding rename_split_fm_def by simp

schematic_goal arity_rename_split_fm: "φformula  arity(rename_split_fm(φ)) = ?m"
  using arity_forces[of φ] forces_type unfolding rename_split_fm_def
  by (simp add:arity Un_assoc[symmetric] union_abs1)

lemma arity_rename_split_fm_le:
  assumes "φformula"
  shows "arity(rename_split_fm(φ))  8  (6 +ω arity(φ))"
proof -
  from assms
  have arity_forces_6: "¬ 1 < arity(φ)  6  n  arity(forces(φ))  n" for n
    using le_trans lt_trans[of _ 5 n] not_lt_iff_le[of 1 "arity(φ)"]
    by (auto intro!:le_trans[OF arity_forces])
  have pred1_arity_forces: "¬ 1 < arity(φ)  pred^n(arity(forces(φ)))  8" if "nnat" for n
    using that pred_le[of 7] le_succ[THEN [2] le_trans] arity_forces_6
    by (induct rule:nat_induct) auto
  have arity_forces_le_succ6: "pred^n(arity(forces(φ)))  succ(succ(succ(succ(succ(succ(arity(φ)))))))"
    if "nnat" for n
    using that assms arity_forces[of φ, THEN le_trans,
        OF _ le_succ, THEN le_trans, OF _ _ le_succ] le_trans[OF pred_le[OF _ le_succ]]
    by (induct rule:nat_induct) auto
  note trivial_arities = arity_forces_6
    arity_forces_le_succ6[of 1, simplified] arity_forces_le_succ6[of 2, simplified]
    arity_forces_le_succ6[of 3, simplified] arity_forces_le_succ6[of 4, simplified]
    arity_forces_le_succ6[of 5, simplified] arity_forces_le_succ6[of 6, simplified]
    pred1_arity_forces[of 1, simplified] pred1_arity_forces[of 2, simplified]
    pred1_arity_forces[of 3, simplified] pred1_arity_forces[of 4, simplified]
    pred1_arity_forces[of 5, simplified] pred1_arity_forces[of 6, simplified]
  show ?thesis
    using assms arity_forces[of φ] arity_forces[of φ, THEN le_trans, OF _ le_succ]
      arity_forces[of φ, THEN le_trans, OF _ le_succ, THEN le_trans, OF _ _ le_succ]
    unfolding rename_split_fm_def
    by (simp add:arity Un_assoc[symmetric] union_abs1 arity_forces[of φ] forces_type)
      ((subst arity_incr_bv_lemma; auto simp: arity ord_simp_union forces_type trivial_arities)+)
qed

definition body_ground_repl_fm where
  "body_ground_repl_fm(φ)  (⋅∃(⋅∃is_Vset_fm(2, 0)  1  0  rename_split_fm(φ) ⋅)⋅)"

lemma body_ground_repl_fm_type[TC]: "φformula  body_ground_repl_fm(φ)formula"
  unfolding body_ground_repl_fm_def by simp

lemma arity_body_ground_repl_fm_le:
  notes le_trans[trans]
  assumes "φformula"
  shows "arity(body_ground_repl_fm(φ))  6  (arity(φ) +ω 4)"
proof -
  from φformula
  have ineq: "n  pred(pred(arity(rename_split_fm(φ))))
     m  pred(pred(8  (arity(φ) +ω6 )))" if "n  m" "nnat" "mnat" for n m
    using that arity_rename_split_fm_le[of φ, THEN [2] pred_mono, THEN [2] pred_mono,
        THEN [2] Un_mono[THEN subset_imp_le, OF _ le_imp_subset]] le_imp_subset
    by auto
  moreover
  have eq1: "pred(pred(pred(4  2  pred(pred(pred(
    pred(pred(pred(pred(pred(9  1  3  2))))))))))) = 1"
    by (auto simp:pred_Un_distrib)
  ultimately
  have "pred(pred(pred(4  2  pred(pred(pred(
    pred(pred(pred(pred(pred(9  1  3  2))))))))))) 
    pred(pred(arity(rename_split_fm(φ)))) 
    1  pred(pred(8  (arity(φ) +ω6 )))"
    by auto
  also from φformula
  have "1  pred(pred(8  (arity(φ) +ω6 )))  6  (4+ωarity(φ))"
    by (auto simp:pred_Un_distrib Un_assoc[symmetric] ord_simp_union)
  finally
  show ?thesis
    using  φformula unfolding body_ground_repl_fm_def
    by (simp add:arity pred_Un_distrib, subst arity_transrec_fm[of "is_HVfrom_fm(8,2,1,0)" 3 1])
      (simp add:arity pred_Un_distrib,simp_all,
        auto simp add:eq1 arity_is_HVfrom_fm[of 8 2 1 0])
qed

definition ground_repl_fm where
  "ground_repl_fm(φ)  least_fm(body_ground_repl_fm(φ), 1)"

lemma ground_repl_fm_type[TC]:
  "φformula  ground_repl_fm(φ)  formula"
  unfolding ground_repl_fm_def by simp

lemma arity_ground_repl_fm:
  assumes "φformula"
  shows "arity(ground_repl_fm(φ))  5  (3 +ω arity(φ))"
proof -
  from assms
  have "pred(arity(body_ground_repl_fm(φ)))  5  (3 +ω arity(φ))"
    using arity_body_ground_repl_fm_le pred_mono succ_Un_distrib
    by (rule_tac pred_le) auto
  with assms
  have "2  pred(arity(body_ground_repl_fm(φ)))  5  (3 +ω arity(φ))"
    using Un_le le_Un_iff by auto
  then
  show ?thesis
    using assms arity_forces arity_body_ground_repl_fm_le
    unfolding least_fm_def ground_repl_fm_def
    apply (auto simp add:arity Un_assoc[symmetric])
    apply (simp add: pred_Un Un_assoc, simp add: Un_assoc[symmetric] union_abs1 pred_Un)
    by(simp only: Un_commute, subst Un_commute, simp add:ord_simp_union,force)
qed

synthesize "is_ordermap" from_definition assuming "nonempty"

synthesize "is_ordertype" from_definition assuming "nonempty"

synthesize "is_order_body" from_definition assuming "nonempty"
arity_theorem for "is_order_body_fm"

definition omap_wfrec_body where
  "omap_wfrec_body(A,r)  (⋅∃image_fm(2, 0, 1)  pred_set_fm(9+ωA, 3,9+ωr, 0) ⋅)"

lemma type_omap_wfrec_body_fm :"Anat  rnat  omap_wfrec_body(A,r)formula"
  unfolding omap_wfrec_body_def by simp

lemma arity_omap_wfrec_aux : "Anat  rnat  arity(omap_wfrec_body(A,r)) = (9+ωA)  (9+ωr)"
  unfolding omap_wfrec_body_def
  using arity_image_fm arity_pred_set_fm pred_Un_distrib union_abs2[of 3] union_abs1
  by (simp add:FOL_arities, auto simp add:Un_assoc[symmetric] union_abs1)

lemma arity_omap_wfrec: "Anat  rnat 
  arity(is_wfrec_fm(omap_wfrec_body(A,r),r+ω3, 1, 0)) = (4+ωA)  (4+ωr)"
  using Arities.arity_is_wfrec_fm[OF _ _ _ _ _ arity_omap_wfrec_aux,of A r "3+ωr" 1 0]
    pred_Un_distrib union_abs1 union_abs2 type_omap_wfrec_body_fm
  by auto

lemma arity_isordermap: "Anat  rnat dnat
   arity(is_ordermap_fm(A,r,d)) = succ(d)  (succ(A)  succ(r))"
  unfolding is_ordermap_fm_def
  using arity_lambda_fm[where i="(4+ωA)  (4+ωr)",OF _ _ _ _ arity_omap_wfrec,
      unfolded omap_wfrec_body_def] pred_Un_distrib union_abs1
  by auto

lemma arity_is_ordertype: "Anat  rnat dnat
   arity(is_ordertype_fm(A,r,d)) = succ(d)  (succ(A)  succ(r))"
  unfolding is_ordertype_fm_def
  using arity_isordermap arity_image_fm pred_Un_distrib FOL_arities
  by auto

lemma arity_is_order_body: "arity(is_order_body_fm(0,1)) = 2"
  using arity_is_order_body_fm arity_is_ordertype ord_simp_union
  by (simp add:FOL_arities)

definition H_order_pred where
  "H_order_pred(A,r)   λx f . f `` Order.pred(A, x, r)"

relationalize "H_order_pred" "is_H_order_pred"

synthesize "is_H_order_pred" from_definition assuming "nonempty"

definition order_pred_wfrec_body where
  "order_pred_wfrec_body(M,A,r,z,x)  y[M].
                pair(M, x, y, z) 
                (f[M].
                    (z[M].
                        z  f 
                        (xa[M].
                            y[M].
                               xaa[M].
                                  sx[M].
                                     r_sx[M].
                                        f_r_sx[M].
                                           pair(M, xa, y, z) 
                                           pair(M, xa, x, xaa) 
                                           upair(M, xa, xa, sx) 
                                           pre_image(M, r, sx, r_sx) 
                                           restriction(M, f, r_sx, f_r_sx) 
                                           xaa  r  (a[M]. image(M, f_r_sx, a, y)  pred_set(M, A, xa, r, a)))) 
                    (a[M]. image(M, f, a, y)  pred_set(M, A, x, r, a)))"


synthesize "order_pred_wfrec_body" from_definition
arity_theorem for "order_pred_wfrec_body_fm"

definition ordtype_replacement_fm where "ordtype_replacement_fm   (⋅∃is_order_body_fm(1, 0)  ⋅⟨1,0 is 2 ⋅)"
definition wfrec_ordertype_fm where "wfrec_ordertype_fm  order_pred_wfrec_body_fm(3,2,1,0)"
definition replacement_is_aleph_fm where "replacement_is_aleph_fm  0 is ordinal⋅  ⋅ℵ(0) is 1"

definition
  funspace_succ_rep_intf where
  "funspace_succ_rep_intf  λp z n. f b. p = <f,b> & z = {cons(<n,b>, f)}"

relativize functional "funspace_succ_rep_intf" "funspace_succ_rep_intf_rel"

― ‹The definition obtained next uses termis_cons instead of termupair
  as in Paulson's 🗏‹~~/src/ZF/Constructible/Relative.thy›.
relationalize "funspace_succ_rep_intf_rel" "is_funspace_succ_rep_intf"

synthesize "is_funspace_succ_rep_intf" from_definition

arity_theorem for "is_funspace_succ_rep_intf_fm"

definition wfrec_Hfrc_at_fm where "wfrec_Hfrc_at_fm  (⋅∃pair_fm(1, 0, 2)  is_wfrec_fm(Hfrc_at_fm(8, 9, 2, 1, 0), 5, 1, 0) ⋅)"
definition list_repl1_intf_fm where "list_repl1_intf_fm  (⋅∃pair_fm(1, 0, 2)  is_wfrec_fm(iterates_MH_fm(list_functor_fm(13, 1, 0), 10, 2, 1, 0), 3, 1, 0) ⋅)"
definition list_repl2_intf_fm where "list_repl2_intf_fm  0  4  is_iterates_fm(list_functor_fm(13, 1, 0), 3, 0, 1) "
definition formula_repl2_intf_fm where "formula_repl2_intf_fm  0  3  is_iterates_fm(formula_functor_fm(1, 0), 2, 0, 1) "
definition eclose_abs_fm where "eclose_abs_fm  0  3  is_iterates_fm(⋅⋃1 is 0, 2, 0, 1) "
definition powapply_repl_fm where "powapply_repl_fm  is_Powapply_fm(2,0,1)"
definition wfrec_rank_fm where "wfrec_rank_fm  (⋅∃pair_fm(1, 0, 2)  is_wfrec_fm(is_Hrank_fm(2, 1, 0), 3, 1, 0) ⋅)"
definition transrec_VFrom_fm where "transrec_VFrom_fm  (⋅∃pair_fm(1, 0, 2)  is_wfrec_fm(is_HVfrom_fm(8, 2, 1, 0), 4, 1, 0) ⋅)"
definition wfrec_Hcheck_fm where "wfrec_Hcheck_fm  (⋅∃pair_fm(1, 0, 2)  is_wfrec_fm(is_Hcheck_fm(8, 2, 1, 0), 4, 1, 0) ⋅) "
definition repl_PHcheck_fm where "repl_PHcheck_fm  PHcheck_fm(2,3,0,1)"
definition tl_repl_intf_fm where "tl_repl_intf_fm  (⋅∃pair_fm(1, 0, 2)  is_wfrec_fm(iterates_MH_fm(tl_fm(1,0), 9, 2, 1, 0), 3, 1, 0) ⋅)"
definition formula_repl1_intf_fm where "formula_repl1_intf_fm  (⋅∃pair_fm(1, 0, 2)  is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0), 9, 2, 1, 0), 3, 1, 0) ⋅)"
definition eclose_closed_fm where "eclose_closed_fm  (⋅∃pair_fm(1, 0, 2)  is_wfrec_fm(iterates_MH_fm(⋅⋃1 is 0, 9, 2, 1, 0), 3, 1, 0) ⋅)"

definition replacement_assm where
  "replacement_assm(M,env,φ)  φ  formula  env  list(M) 
  arity(φ)  2 +ω length(env) 
    strong_replacement(##M,λx y. (M , [x,y]@env  φ))"

definition ground_replacement_assm where
  "ground_replacement_assm(M,env,φ)  replacement_assm(M,env,ground_repl_fm(φ))"

end