Theory Separation_Rename

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

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)" 
    "[P,leq,o,p,t]  list(M)"
    "[pi,u]  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(1) 
        rensep_type[OF length_type[OF envlist(M)]] 
        arity(φ)  7 #+ length(env)]
      rensep_action[OF 1(1),rule_format,symmetric]
    by simp
qed

end