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" "knat" "x  weak(n,k)"
  shows " i  n . x = i+ωk"
  using assms unfolding weak_def by blast

lemma weak_equal :
  assumes "nnat" "mnat"
  shows "weak(n,m) = (m+ωn) - m"
proof -
  have "weak(n,m)(m+ωn)-m"
  proof(intro subsetI)
    fix x
    assume "xweak(n,m)"
    with assms
    obtain i where
      "in" "x=i+ωm"
      using weakD by blast
    then
    have "mi+ωm" "i<n"
      using add_le_self2[of m i] mnat nnat ltI[OF in] by simp_all
    then
    have "¬i+ωm<m"
      using not_lt_iff_le in_n_in_nat[OF nnat in] mnat by simp
    with x=i+ωm
    have "xm"
      using ltI mnat by auto
    moreover
    from assms x=i+ωm i<n
    have "x<m+ωn"
      using add_lt_mono1[OF i<n nnat] by simp
    ultimately
    show "x(m+ωn)-m"
      using ltD DiffI by simp
  qed
  moreover
  have "(m+ωn)-mweak(n,m)"
  proof (intro subsetI)
    fix x
    assume "x(m+ωn)-m"
    then
    have "xm+ωn" "xm"
      using DiffD1[of x "n+ωm" m] DiffD2[of x "n+ωm" m] by simp_all
    then
    have "x<m+ωn" "xnat"
      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 xnat,of "m+ωn"] add_type by auto
    then
    have "x+ωi<m+ωn" using succ_le_iff by simp
    with xm
    have "¬x<m" using ltD by blast
    with mnat xnat
    have "mx" using not_lt_iff_le by simp
    with x<m+ωn  nnat
    have "x-ωm<m+ωn-ωm"
      using diff_mono[OF xnat _ mnat] by simp
    have "m+ωn-ωm =  n" using diff_cancel2 mnat nnat by simp
    with x-ωm<m+ωn-ωm xnat
    have "x-ωm  n" "x=x-ωm+ωm"
      using ltD add_diff_inverse2[OF mx] by simp_all
    then
    show "xweak(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 "in" "succ(succ(natify(i)))n" "wn. succ(succ(natify(i)))  natify(w)"
    then
    have "i<n"
      using ltI nnat by simp
    from nnat in succ(succ(natify(i)))n
    have "inat" "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 nnat
    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 nnat
      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 inat
        have "succ(succ(natify(i)))  natify(succ(succ(i)))"
          using  wn. succ(succ(natify(i)))  natify(w) by auto
        then
        have "False" using inat by auto
        then show ?thesis by blast
      qed
      then show ?thesis .
    qed
    with inat have "succ(natify(i)) = n" by simp
  }
  then
  show "n  nat 
    succ(succ(natify(y)))  n 
    xn. succ(succ(natify(y)))  natify(x) 
    y  n  succ(natify(y)) = n" for y
    by blast
qed

lemma in_add_del :
  assumes "xj+ωn" "nnat" "jnat"
  shows "x < j  x  weak(n,j)"
proof (cases "x<j")
  case True
  then show ?thesis ..
next
  case False
  have "xnat" "j+ωnnat"
    using in_n_in_nat[OF _ xj+ωn] assms by simp_all
  then
  have "j  x" "x < j+ωn"
    using not_lt_iff_le False jnat nnat ltI[OF xj+ωn] by auto
  then
  have "x-ωj < (j +ω n) -ω j" "x = j +ω (x -ωj)"
    using diff_mono xnat j+ωnnat jnat nnat
      add_diff_inverse[OF jx] by simp_all
  then
  have "x-ωj < n" "x = (x -ωj ) +ω j"
    using diff_add_inverse nnat 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-ωjn] 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 envlist(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-ω5nat" "i+ω2nat"
      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 inat by simp_all
    then have "2  i" using le_trans[OF 25] by simp
    from A i  5+ωlength(env)
    have "i < 5+ωlength(env)" using ltI by simp
    with inat 2i 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) inat
    have "¬ i+ω2 < 7" using not_lt_iff_le add_le_mono by simp
    from i < 5+ωlength(env) 3 inat
    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) inat] 3 by simp
    also
    have "... = nth(i-ω5, env)"
      using nth_append[OF env list(M) i-ω5nat] i-ω5 < length(env) by simp
    also
    have "... = nth(i+ω2, ?tgt)"
      using nth_append[OF assms(1) i+ω2nat] ¬ 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 nnat
  have "(5+ωn)+ω2 = 7+ωn" "7+ωnnat" "5+ωnnat" by simp_all
  have
    D: "sep_env(n)`x  (7+ωn)-7" if "x  (5+ωn)-5" for x
  proof -
    from x5+ωn-5
    have "?h`x = x+ω2" "x<5+ωn" "xnat"
      unfolding sep_env_def using ltI in_n_in_nat[OF 5+ωnnat] by simp_all
    then
    have "x+ω2 < 7+ωn" by simp
    then
    have "x+ω2  7+ωn" using ltD by simp
    from x5+ωn-5
    have "x5" by simp
    then have "¬x<5" using ltD by blast
    then have "5x" using not_lt_iff_le xnat by simp
    then have "7x+ω2" using add_le_mono xnat by simp
    then have "¬x+ω2<7" using not_lt_iff_le xnat by simp
    then have "x+ω2  7" using ltI xnat 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 "xdomain(sep_var(n))" for x
    using that unfolding sep_var_def by auto
  have D : "x<n+ω7" if "x7+ωn" for x
    using that nnat ltI by simp
  have "¬ 5+ωn < 5+ωn" using nnat  lt_irrefl[of _ False] by force
  have "¬ 6+ωn < 5+ωn" using nnat 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 nnat RepFun_iff by force
    with nnat
    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 "xdomain(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  xweak(n,7)" if "x7+ωn" for x
    using in_add_del[OF x7+ωn] by simp
  moreover
  {
    fix x
    assume asm:"x7+ωn"  "x?A"  "xweak(n,7)"
    then
    have "xdomain(sep_var(n))"
    proof -
      from nnat
      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:"x7+ωn"  "x?A" "x<7"
    then have "xdomain(sep_var(n))"
    proof (cases "2  n")
      case True
      moreover
      have "0<n" using  leD[OF nnat 2n] lt_imp_0_lt by auto
      ultimately
      have "x<5"
        using x<7 x?A nnat 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 nnat by auto
      next
        case False
        then
        have "n < 2" using  nnat not_lt_iff_le ¬ 2  n  by force
        then
        have "¬ n <1" using n0 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 nnat by force
      qed
    qed
  }
  ultimately
  have "wdomain(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 nnat]]
    sep_var_domain[OF nnat] 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 envlist(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 envlist(M)]  nth_concat3[OF envlist(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 "nnat"
  shows "(7+ωn-weak(n,5))  weak(n,5) = 7+ωn" "7+ωn  ( 7 +ω n - 7) = 7+ωn"
proof -
  from nnat
  have "weak(n,5) = n+ω5-5"
    using weak_equal by simp
  with  nnat
  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 "nnat"
  shows "rensep(n)  7+ωn  7+ωn"
proof -
  from nnat
  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 nnat sep_env_type weak_equal
    by force
  then
  show ?thesis using rensep_aux nnat 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 ?srclist(M) ?tgtlist(M) length(?src) = (7+ω?n-weak(?n,5))  weak(?n,5)
          sep_var_action[OF [t,p,u,P,leq,o,pi]  list(M) envlist(M)]
          sep_env_action[OF [t,p,u,P,leq,o,pi]  list(M) envlist(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" "envlist(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)"
    "envlist(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 envlist(M)]]
        arity(φ)  7 +ω length(env)]
      rensep_action[OF 1,rule_format,symmetric]
    by simp
qed

end