# Theory Separation_Rename

```section‹Auxiliary renamings for Separation›
theory Separation_Rename
imports
Interface
begin

no_notation Aleph (‹ℵ_› [90] 90)

lemmas apply_fun = apply_iff[THEN iffD1]

lemma nth_concat : "[p,t] ∈ list(A) ⟹ env∈ list(A) ⟹ nth(1 +⇩ω length(env),[p]@ env @ [t]) = t"

lemma nth_concat2 : "env∈ list(A) ⟹ nth(length(env),env @ [p,t]) = p"

lemma nth_concat3 : "env∈ list(A) ⟹ u = nth(succ(length(env)), env @ [pi, u])"

definition
sep_var :: "i ⇒ i" where
"sep_var(n) ≡ {⟨0,1⟩,⟨1,3⟩,⟨2,4⟩,⟨3,5⟩,⟨4,0⟩,⟨5+⇩ωn,6⟩,⟨6+⇩ωn,2⟩}"

definition
sep_env :: "i ⇒ i" where
"sep_env(n) ≡ λ i ∈ (5+⇩ωn)-5 . i+⇩ω2"

definition weak :: "[i, i] ⇒ i" where
"weak(n,m) ≡ {i+⇩ωm . i ∈ n}"

lemma weakD :
assumes "n ∈ nat" "k∈nat" "x ∈ weak(n,k)"
shows "∃ i ∈ n . x = i+⇩ωk"
using assms unfolding weak_def by blast

lemma weak_equal :
assumes "n∈nat" "m∈nat"
shows "weak(n,m) = (m+⇩ωn) - m"
proof -
have "weak(n,m)⊆(m+⇩ωn)-m"
proof(intro subsetI)
fix x
assume "x∈weak(n,m)"
with assms
obtain i where
"i∈n" "x=i+⇩ωm"
using weakD by blast
then
have "m≤i+⇩ωm" "i<n"
using add_le_self2[of m i] ‹m∈nat› ‹n∈nat› ltI[OF ‹i∈n›] by simp_all
then
have "¬i+⇩ωm<m"
using not_lt_iff_le in_n_in_nat[OF ‹n∈nat› ‹i∈n›] ‹m∈nat› by simp
with ‹x=i+⇩ωm›
have "x∉m"
using ltI ‹m∈nat› by auto
moreover
from assms ‹x=i+⇩ωm› ‹i<n›
have "x<m+⇩ωn"
using add_lt_mono1[OF ‹i<n› ‹n∈nat›] by simp
ultimately
show "x∈(m+⇩ωn)-m"
using ltD DiffI by simp
qed
moreover
have "(m+⇩ωn)-m⊆weak(n,m)"
proof (intro subsetI)
fix x
assume "x∈(m+⇩ωn)-m"
then
have "x∈m+⇩ωn" "x∉m"
using DiffD1[of x "n+⇩ωm" m] DiffD2[of x "n+⇩ωm" m] by simp_all
then
have "x<m+⇩ωn" "x∈nat"
using ltI in_n_in_nat[OF add_type[of m n]] by simp_all
then
obtain i where
"m+⇩ωn = succ(x+⇩ωi)"
then
have "x+⇩ωi<m+⇩ωn" using succ_le_iff by simp
with ‹x∉m›
have "¬x<m" using ltD by blast
with ‹m∈nat› ‹x∈nat›
have "m≤x" using not_lt_iff_le by simp
with ‹x<m+⇩ωn›  ‹n∈nat›
have "x-⇩ωm<m+⇩ωn-⇩ωm"
using diff_mono[OF ‹x∈nat› _ ‹m∈nat›] by simp
have "m+⇩ωn-⇩ωm =  n" using diff_cancel2 ‹m∈nat› ‹n∈nat› by simp
with ‹x-⇩ωm<m+⇩ωn-⇩ωm› ‹x∈nat›
have "x-⇩ωm ∈ n" "x=x-⇩ωm+⇩ωm"
using ltD add_diff_inverse2[OF ‹m≤x›] by simp_all
then
show "x∈weak(n,m)"
unfolding weak_def by auto
qed
ultimately
show ?thesis by auto
qed

lemma weak_zero:
shows "weak(0,n) = 0"
unfolding weak_def by simp

lemma weakening_diff :
assumes "n ∈ nat"
shows "weak(n,7) - weak(n,5) ⊆ {5+⇩ωn, 6+⇩ωn}"
unfolding weak_def using assms
proof(auto)
{
fix i
assume "i∈n" "succ(succ(natify(i)))≠n" "∀w∈n. succ(succ(natify(i))) ≠ natify(w)"
then
have "i<n"
using ltI ‹n∈nat› by simp
from ‹n∈nat› ‹i∈n› ‹succ(succ(natify(i)))≠n›
have "i∈nat" "succ(succ(i))≠n" using in_n_in_nat by simp_all
from ‹i<n›
have "succ(i)≤n" using succ_leI by simp
with ‹n∈nat›
consider (a) "succ(i) = n" | (b) "succ(i) < n"
using leD by auto
then have "succ(i) = n"
proof cases
case a
then show ?thesis .
next
case b
then
have "succ(succ(i))≤n" using succ_leI by simp
with ‹n∈nat›
consider (a) "succ(succ(i)) = n" | (b) "succ(succ(i)) < n"
using leD by auto
then have "succ(i) = n"
proof cases
case a
with ‹succ(succ(i))≠n› show ?thesis by blast
next
case b
then
have "succ(succ(i))∈n" using ltD by simp
with ‹i∈nat›
have "succ(succ(natify(i))) ≠ natify(succ(succ(i)))"
using  ‹∀w∈n. succ(succ(natify(i))) ≠ natify(w)› by auto
then
have "False" using ‹i∈nat› by auto
then show ?thesis by blast
qed
then show ?thesis .
qed
with ‹i∈nat› have "succ(natify(i)) = n" by simp
}
then
show "n ∈ nat ⟹
succ(succ(natify(y))) ≠ n ⟹
∀x∈n. succ(succ(natify(y))) ≠ natify(x) ⟹
y ∈ n ⟹ succ(natify(y)) = n" for y
by blast
qed

assumes "x∈j+⇩ωn" "n∈nat" "j∈nat"
shows "x < j ∨ x ∈ weak(n,j)"
proof (cases "x<j")
case True
then show ?thesis ..
next
case False
have "x∈nat" "j+⇩ωn∈nat"
using in_n_in_nat[OF _ ‹x∈j+⇩ωn›] assms by simp_all
then
have "j ≤ x" "x < j+⇩ωn"
using not_lt_iff_le False ‹j∈nat› ‹n∈nat› ltI[OF ‹x∈j+⇩ωn›] by auto
then
have "x-⇩ωj < (j +⇩ω n) -⇩ω j" "x = j +⇩ω (x -⇩ωj)"
using diff_mono ‹x∈nat› ‹j+⇩ωn∈nat› ‹j∈nat› ‹n∈nat›
then
have "x-⇩ωj < n" "x = (x -⇩ωj ) +⇩ω j"
then
have "x-⇩ωj ∈n" using ltD by simp
then
have "x ∈ weak(n,j)"
unfolding weak_def
using ‹x= (x-⇩ωj) +⇩ωj› RepFunI[OF ‹x-⇩ωj∈n›] add_commute by force
then show ?thesis  ..
qed

lemma sep_env_action:
assumes
"[t,p,u,P,leq,o,pi] ∈ list(M)"
"env ∈ list(M)"
shows "∀ i . i ∈ weak(length(env),5) ⟶
nth(sep_env(length(env))`i,[t,p,u,P,leq,o,pi]@env) = nth(i,[p,P,leq,o,t] @ env @ [pi,u])"
proof -
from assms
have A: "5+⇩ωlength(env)∈nat" "[p, P, leq, o, t] ∈list(M)"
by simp_all
let ?f="sep_env(length(env))"
have EQ: "weak(length(env),5) = 5+⇩ωlength(env) - 5"
using weak_equal length_type[OF ‹env∈list(M)›] by simp
let ?tgt="[t,p,u,P,leq,o,pi]@env"
let ?src="[p,P,leq,o,t] @ env @ [pi,u]"
have "nth(?f`i,[t,p,u,P,leq,o,pi]@env) = nth(i,[p,P,leq,o,t] @ env @ [pi,u])"
if "i ∈ (5+⇩ωlength(env)-5)" for i
proof -
from that
have 2: "i ∈ 5+⇩ωlength(env)"  "i ∉ 5" "i ∈ nat" "i-⇩ω5∈nat" "i+⇩ω2∈nat"
using in_n_in_nat[OF ‹5+⇩ωlength(env)∈nat›] by simp_all
then
have 3: "¬ i < 5" using ltD by force
then
have "5 ≤ i" "2 ≤ 5"
using  not_lt_iff_le ‹i∈nat› by simp_all
then have "2 ≤ i" using le_trans[OF ‹2≤5›] by simp
from A ‹i ∈ 5+⇩ωlength(env)›
have "i < 5+⇩ωlength(env)" using ltI by simp
with ‹i∈nat› ‹2≤i› A
have C:"i+⇩ω2 < 7+⇩ωlength(env)"  by simp
with that
have B: "?f`i = i+⇩ω2" unfolding sep_env_def by simp
from 3 assms(1) ‹i∈nat›
have "¬ i+⇩ω2 < 7" using not_lt_iff_le add_le_mono by simp
from ‹i < 5+⇩ωlength(env)› 3 ‹i∈nat›
have "i-⇩ω5 < 5+⇩ωlength(env) -⇩ω 5"
using diff_mono[of i "5+⇩ωlength(env)" 5,OF _ _ _ ‹i < 5+⇩ωlength(env)›]
not_lt_iff_le[THEN iffD1] by force
with assms(2)
have "i-⇩ω5 < length(env)" using diff_add_inverse length_type by simp
have "nth(i,?src) =nth(i-⇩ω5,env@[pi,u])"
using nth_append[OF A(2) ‹i∈nat›] 3 by simp
also
have "... = nth(i-⇩ω5, env)"
using nth_append[OF ‹env ∈list(M)› ‹i-⇩ω5∈nat›] ‹i-⇩ω5 < length(env)› by simp
also
have "... = nth(i+⇩ω2, ?tgt)"
using nth_append[OF assms(1) ‹i+⇩ω2∈nat›] ‹¬ i+⇩ω2 <7› by simp
ultimately
have "nth(i,?src) = nth(?f`i,?tgt)"
using B by simp
then show ?thesis using that by simp
qed
then show ?thesis using EQ by force
qed

lemma sep_env_type :
assumes "n ∈ nat"
shows "sep_env(n) : (5+⇩ωn)-5 → (7+⇩ωn)-7"
proof -
let ?h="sep_env(n)"
from ‹n∈nat›
have "(5+⇩ωn)+⇩ω2 = 7+⇩ωn" "7+⇩ωn∈nat" "5+⇩ωn∈nat" by simp_all
have
D: "sep_env(n)`x ∈ (7+⇩ωn)-7" if "x ∈ (5+⇩ωn)-5" for x
proof -
from ‹x∈5+⇩ωn-5›
have "?h`x = x+⇩ω2" "x<5+⇩ωn" "x∈nat"
unfolding sep_env_def using ltI in_n_in_nat[OF ‹5+⇩ωn∈nat›] by simp_all
then
have "x+⇩ω2 < 7+⇩ωn" by simp
then
have "x+⇩ω2 ∈ 7+⇩ωn" using ltD by simp
from ‹x∈5+⇩ωn-5›
have "x∉5" by simp
then have "¬x<5" using ltD by blast
then have "5≤x" using not_lt_iff_le ‹x∈nat› by simp
then have "7≤x+⇩ω2" using add_le_mono ‹x∈nat› by simp
then have "¬x+⇩ω2<7" using not_lt_iff_le ‹x∈nat› by simp
then have "x+⇩ω2 ∉ 7" using ltI ‹x∈nat› by force
with ‹x+⇩ω2 ∈ 7+⇩ωn› show ?thesis using  ‹?h`x = x+⇩ω2› DiffI by simp
qed
then show ?thesis unfolding sep_env_def using lam_type by simp
qed

lemma sep_var_fin_type :
assumes "n ∈ nat"
shows "sep_var(n) : 7+⇩ωn  -||> 7+⇩ωn"
unfolding sep_var_def
using consI ltD emptyI by force

lemma sep_var_domain :
assumes "n ∈ nat"
shows "domain(sep_var(n)) =  7+⇩ωn - weak(n,5)"
proof -
let ?A="weak(n,5)"
have A:"domain(sep_var(n)) ⊆ (7+⇩ωn)"
unfolding sep_var_def
have C: "x=5+⇩ωn ∨ x=6+⇩ωn ∨ x ≤ 4" if "x∈domain(sep_var(n))" for x
using that unfolding sep_var_def by auto
have D : "x<n+⇩ω7" if "x∈7+⇩ωn" for x
using that ‹n∈nat› ltI by simp
have "¬ 5+⇩ωn < 5+⇩ωn" using ‹n∈nat›  lt_irrefl[of _ False] by force
have "¬ 6+⇩ωn < 5+⇩ωn" using ‹n∈nat› by force
have R: "x < 5+⇩ωn" if "x∈?A" for x
proof -
from that
obtain i where
"i<n" "x=5+⇩ωi"
unfolding weak_def
using ltI ‹n∈nat› RepFun_iff by force
with ‹n∈nat›
have "5+⇩ωi < 5+⇩ωn" using add_lt_mono2 by simp
with ‹x=5+⇩ωi›
show "x < 5+⇩ωn" by simp
qed
then
have 1:"x∉?A" if "¬x <5+⇩ωn" for x using that by blast
have "5+⇩ωn ∉ ?A" "6+⇩ωn∉?A"
proof -
show "5+⇩ωn ∉ ?A" using 1 ‹¬5+⇩ωn<5+⇩ωn› by blast
with 1 show "6+⇩ωn ∉ ?A" using  ‹¬6+⇩ωn<5+⇩ωn› by blast
qed
then
have E:"x∉?A" if "x∈domain(sep_var(n))" for x
unfolding weak_def
using C that by force
then
have F: "domain(sep_var(n)) ⊆ 7+⇩ωn - ?A" using A by auto
from assms
have "x<7 ∨ x∈weak(n,7)" if "x∈7+⇩ωn" for x
moreover
{
fix x
assume asm:"x∈7+⇩ωn"  "x∉?A"  "x∈weak(n,7)"
then
have "x∈domain(sep_var(n))"
proof -
from ‹n∈nat›
have "weak(n,7)-weak(n,5)⊆{n+⇩ω5,n+⇩ω6}"
using weakening_diff by simp
with  ‹x∉?A› asm
have "x∈{n+⇩ω5,n+⇩ω6}" using  subsetD DiffI by blast
then
show ?thesis unfolding sep_var_def by simp
qed
}
moreover
{
fix x
assume asm:"x∈7+⇩ωn"  "x∉?A" "x<7"
then have "x∈domain(sep_var(n))"
proof (cases "2 ≤ n")
case True
moreover
have "0<n" using  leD[OF ‹n∈nat› ‹2≤n›] lt_imp_0_lt by auto
ultimately
have "x<5"
using ‹x<7› ‹x∉?A› ‹n∈nat› in_n_in_nat
unfolding weak_def
then
show ?thesis unfolding sep_var_def
next
case False
then
show ?thesis
proof (cases "n=0")
case True
then show ?thesis
unfolding sep_var_def using ltD asm ‹n∈nat› by auto
next
case False
then
have "n < 2" using  ‹n∈nat› not_lt_iff_le ‹¬ 2 ≤ n›  by force
then
have "¬ n <1" using ‹n≠0› by simp
then
have "n=1" using not_lt_iff_le ‹n<2› le_iff by auto
then show ?thesis
using ‹x∉?A›
unfolding weak_def sep_var_def
using ltD asm ‹n∈nat› by force
qed
qed
}
ultimately
have "w∈domain(sep_var(n))" if "w∈ 7+⇩ωn - ?A" for w
using that by blast
then
have "7+⇩ωn - ?A ⊆ domain(sep_var(n))" by blast
with F
show ?thesis by auto
qed

lemma sep_var_type :
assumes "n ∈ nat"
shows "sep_var(n) : (7+⇩ωn)-weak(n,5) → 7+⇩ωn"
using FiniteFun_is_fun[OF sep_var_fin_type[OF ‹n∈nat›]]
sep_var_domain[OF ‹n∈nat›] by simp

lemma sep_var_action :
assumes
"[t,p,u,P,leq,o,pi] ∈ list(M)"
"env ∈ list(M)"
shows "∀ i . i ∈ (7+⇩ωlength(env)) - weak(length(env),5) ⟶
nth(sep_var(length(env))`i,[t,p,u,P,leq,o,pi]@env) = nth(i,[p,P,leq,o,t] @ env @ [pi,u])"
using assms
proof (subst sep_var_domain[OF length_type[OF ‹env∈list(M)›],symmetric],auto)
fix i y
assume "⟨i, y⟩ ∈ sep_var(length(env))"
with assms
show "nth(sep_var(length(env)) ` i,
Cons(t, Cons(p, Cons(u, Cons(P, Cons(leq, Cons(o, Cons(pi, env)))))))) =
nth(i, Cons(p, Cons(P, Cons(leq, Cons(o, Cons(t, env @ [pi, u]))))))"
using apply_fun[OF sep_var_type] assms
unfolding sep_var_def
using nth_concat2[OF ‹env∈list(M)›]  nth_concat3[OF ‹env∈list(M)›,symmetric]
by force
qed

definition
rensep :: "i ⇒ i" where
"rensep(n) ≡ union_fun(sep_var(n),sep_env(n),7+⇩ωn-weak(n,5),weak(n,5))"

lemma rensep_aux :
assumes "n∈nat"
shows "(7+⇩ωn-weak(n,5)) ∪ weak(n,5) = 7+⇩ωn" "7+⇩ωn ∪ ( 7 +⇩ω n - 7) = 7+⇩ωn"
proof -
from ‹n∈nat›
have "weak(n,5) = n+⇩ω5-5"
using weak_equal by simp
with  ‹n∈nat›
show "(7+⇩ωn-weak(n,5)) ∪ weak(n,5) = 7+⇩ωn" "7+⇩ωn ∪ ( 7 +⇩ω n - 7) = 7+⇩ωn"
using Diff_partition le_imp_subset by auto
qed

lemma rensep_type :
assumes "n∈nat"
shows "rensep(n) ∈ 7+⇩ωn → 7+⇩ωn"
proof -
from ‹n∈nat›
have "rensep(n) ∈ (7+⇩ωn-weak(n,5)) ∪ weak(n,5) → 7+⇩ωn ∪ (7+⇩ωn - 7)"
unfolding rensep_def
using union_fun_type  sep_var_type ‹n∈nat› sep_env_type weak_equal
by force
then
show ?thesis using rensep_aux ‹n∈nat› by auto
qed

lemma rensep_action :
assumes "[t,p,u,P,leq,o,pi] @ env ∈ list(M)"
shows "∀ i . i < 7+⇩ωlength(env) ⟶ nth(rensep(length(env))`i,[t,p,u,P,leq,o,pi]@env) = nth(i,[p,P,leq,o,t] @ env @ [pi,u])"
proof -
let ?tgt="[t,p,u,P,leq,o,pi]@env"
let ?src="[p,P,leq,o,t] @ env @ [pi,u]"
let ?m="7 +⇩ω length(env) - weak(length(env),5)"
let ?p="weak(length(env),5)"
let ?f="sep_var(length(env))"
let ?g="sep_env(length(env))"
let ?n="length(env)"
from assms
have 1 : "[t,p,u,P,leq,o,pi] ∈ list(M)" " env ∈ list(M)"
"?src ∈ list(M)" "?tgt ∈ list(M)"
"7+⇩ω?n = (7+⇩ω?n-weak(?n,5)) ∪ weak(?n,5)"
" length(?src) = (7+⇩ω?n-weak(?n,5)) ∪ weak(?n,5)"
using Diff_partition le_imp_subset rensep_aux by auto
then
have "nth(i, ?src) = nth(union_fun(?f, ?g, ?m, ?p) ` i, ?tgt)" if "i < 7+⇩ωlength(env)" for i
proof -
from ‹i<7+⇩ω?n›
have "i ∈ (7+⇩ω?n-weak(?n,5)) ∪ weak(?n,5)"
using ltD by simp
then show ?thesis
unfolding rensep_def using
union_fun_action[OF ‹?src∈list(M)› ‹?tgt∈list(M)› ‹length(?src) = (7+⇩ω?n-weak(?n,5)) ∪ weak(?n,5)›
sep_var_action[OF ‹[t,p,u,P,leq,o,pi] ∈ list(M)› ‹env∈list(M)›]
sep_env_action[OF ‹[t,p,u,P,leq,o,pi] ∈ list(M)› ‹env∈list(M)›]
] that
by simp
qed
then show ?thesis unfolding rensep_def by simp
qed

definition sep_ren :: "[i,i] ⇒ i" where
"sep_ren(n,φ) ≡ ren(φ)`(7+⇩ωn)`(7+⇩ωn)`rensep(n)"

lemma arity_rensep: assumes "φ∈formula" "env ∈ list(M)"
"arity(φ) ≤ 7+⇩ωlength(env)"
shows "arity(sep_ren(length(env),φ)) ≤ 7+⇩ωlength(env)"
unfolding sep_ren_def
using arity_ren rensep_type assms
by simp

lemma type_rensep [TC]:
assumes "φ∈formula" "env∈list(M)"
shows "sep_ren(length(env),φ) ∈ formula"
unfolding sep_ren_def
using ren_tc rensep_type assms
by simp

lemma sepren_action:
assumes "arity(φ) ≤ 7 +⇩ω length(env)"
"[t,p,u,P,leq,o,pi] ∈ list(M)"
"env∈list(M)"
"φ∈formula"
shows "sats(M, sep_ren(length(env),φ),[t,p,u,P,leq,o,pi] @ env) ⟷ sats(M, φ,[p,P,leq,o,t] @ env @ [pi,u])"
proof -
from assms
have 1: "[t, p, u, P, leq, o, pi] @ env ∈ list(M)"
by simp_all
then
have 2: "[p,P,leq,o,t] @ env @ [pi,u] ∈ list(M)"
using app_type by simp
show ?thesis
unfolding sep_ren_def
using sats_iff_sats_ren[OF ‹φ∈formula›