Theory Fm_Definitions
section‹Concepts involved in instances of Replacement›
theory Fm_Definitions
imports
Transitive_Models.Renaming_Auto
Transitive_Models.Aleph_Relative
FrecR_Arities
begin
no_notation Aleph (‹ℵ_› [90] 90)
text‹In 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.
[|a0∈Aa; a1∈Aa; a2∈Aa|]
==> 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
lemma sats_is_wfrec_fm':
assumes MH_iff_sats:
"!!a0 a1 a2 a3 a4.
[|a0∈A; a1∈A; a2∈A; a3∈A; a4∈A|]
==> 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.
[|a0∈Aa; a1∈Aa; a2∈Aa; a3∈Aa; a4∈Aa|]
==> 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.
[|a0∈Aa; a1∈Aa; a2∈Aa; a3∈Aa; a4∈Aa|]
==> 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
text‹Formulas for particular replacement instances›
text‹Now we introduce some definitions used in the definition of check; which
is defined by well-founded recursion using replacement in the recursive call.›
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"
definition
PHcheck :: "[i⇒o,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"
definition
is_Hcheck :: "[i⇒o,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 "m∈nat" "n∈nat" "p∈nat" "o∈nat"
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
definition
is_check :: "[i⇒o,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)"
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]: "x∈nat ⟹ o∈nat ⟹ z∈nat ⟹ check_fm(x,o,z) ∈ formula"
by (simp add:check_fm_def)
lemma sats_check_fm :
assumes
"o∈nat" "x∈nat" "z∈nat" "env∈list(M)" "0∈M"
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. ⟦ a0∈M; a1∈M; a2∈M; a3∈M; a4∈M;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 "r∈M" 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 "r∈M" 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 "m∈nat" "n∈nat" "o∈nat"
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 _⋅›)
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)"
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)"
subsection‹Formulas used to prove some generic instances.›
definition ρ_repl :: "i⇒i" 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
hide_fact Internalize.sum_type
lemma ren_type :
assumes "l∈nat"
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 ⟹ len∈nat ⟹ 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 :: "i⇒i" 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 "l∈nat"
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 ⟹ len∈nat ⟹ 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
subsection‹The relation \<^term>‹frecrel››
definition
frecrelP :: "[i⇒o,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 :: "[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)"
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⟩" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈P"
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 :: "[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)"
synthesize "is_tuple" from_definition
arity_theorem for "is_tuple_fm"
subsection‹Definition of Forces›
subsubsection‹Definition of \<^term>‹forces› 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. q∈P ∧ ⟨q,p⟩∈leq ⟶ (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) ≡ ∀v∈P. ⟨v,p⟩∈leq ⟶
(∃q. ∃σ. ∃r. r∈P ∧ q∈P ∧ ⟨q,v⟩∈leq ∧ ⟨σ,r⟩ ∈ θ ∧ ⟨q,r⟩∈leq ∧ 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
"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)"
using assms arity_eq_case_fm'
by auto
arity_theorem intermediate for "mem_case_fm"
lemma arity_mem_case_fm[arity] :
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)"
using assms arity_mem_case_fm'
by auto
definition
Hfrc :: "[i,i,i,i] ⇒ o" where
"Hfrc(P,leq,fnnc,f) ≡ ∃ft. ∃τ. ∃θ. ∃p. p∈P ∧ 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 :: "[i⇒o,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
"P∈nat" "leq∈nat" "fnnc∈nat" "f∈nat"
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"
subsubsection‹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))"
synthesize "is_forcerel" from_definition
arity_theorem for "is_forcerel_fm"
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)"
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] :
"⟦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[arity] :
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)"
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
"p∈nat" "l∈nat" "i∈nat" "j∈nat" "env∈list(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 "r∈A"
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 "a0∈A" "a1∈A" "a2∈A" "a3∈A" "a4∈A" for a0 a1 a2 a3 a4
using that assms ‹r∈A›
Hfrc_at_iff_sats[of "6+⇩ωp" "6+⇩ωl" 2 1 0 "[a0,a1,a2,a3,a4,r]@env" A] by simp
with ‹r∈A›
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 "r∈A" 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" "l∈nat" "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) ≡ ¬ (∃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))"
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)"
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)))"
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))"
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
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, φ)))"
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 :: "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 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
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(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 :: "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
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 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 ‹4≤3+⇩ω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" "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
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 "n∈nat" 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 "n∈nat" 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" "n∈nat" "m∈nat" 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 :"A∈nat ⟹ r∈nat ⟹ omap_wfrec_body(A,r)∈formula"
unfolding omap_wfrec_body_def by simp
lemma arity_omap_wfrec_aux : "A∈nat ⟹ r∈nat ⟹ 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: "A∈nat ⟹ r∈nat ⟹
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: "A∈nat ⟹ r∈nat ⟹d∈nat⟹
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: "A∈nat ⟹ r∈nat ⟹d∈nat⟹
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"
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