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"
  by(auto simp add:nth_append)

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

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

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)"
      using less_iff_succ_add[OF ‹x∈nat›,of "m+⇩ωn"] add_type by auto
    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

lemma in_add_del :
  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›
      add_diff_inverse[OF ‹j≤x›] by simp_all
  then
  have "x-⇩ωj < n" "x = (x -⇩ωj ) +⇩ω j"
    using diff_add_inverse ‹n∈nat› add_commute by simp_all
  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
    by(auto simp add: le_natE)
  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
    using in_add_del[OF ‹x∈7+⇩ωn›] by simp
  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
        by (clarsimp simp add:not_lt_iff_le, auto simp add:lt_def)
      then
      show ?thesis unfolding sep_var_def
        by (clarsimp simp add:not_lt_iff_le, auto simp add:lt_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›
        add_type[of 7 "length(env)"]
        add_type[of 7 "length(env)"]
        2 1
        rensep_type[OF length_type[OF ‹env∈list(M)›]]
        ‹arity(φ) ≤ 7 +⇩ω length(env)›]
      rensep_action[OF 1,rule_format,symmetric]
    by simp
qed

end