Theory Separation_Rename

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

lemma apply_fun: "f ∈ Pi(A,B) ==> <a,b>: f ⟹ f`a = b"
  by(auto simp add: apply_iff)

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 -
  {
    fix x
    assume "x∈weak(n,m)"
    with assms 
    obtain i where
      a:  "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 N: "x∉m" 
      using ltI ‹m∈nat› by auto
    from assms ‹x=i#+m› ‹i<n›
    have "x<m#+n"
      using add_lt_mono1[OF ‹i<n› ‹n∈nat›] by simp
    then 
    have "x∈(m#+n)-m" using ltD DiffI N by simp
  }
  then have A: "weak(n,m)⊆(m#+n)-m" using subsetI by simp
  {
    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 
    have "x∈weak(n,m)" 
      unfolding weak_def by auto
  }
  then have "(m#+n)-m⊆weak(n,m)" using subsetI by simp
  with A 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 "⋀xa. n ∈ nat ⟹ succ(succ(natify(xa))) ≠ n ⟹ ∀x∈n. succ(succ(natify(xa))) ≠ natify(x) ⟹ xa ∈ n ⟹ succ(natify(xa)) = n"
    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
  {fix x
    assume "x∈?A" 
    then 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› have "x < 5#+n" by simp
  }
  then 
  have R: "x < 5#+n" if "x∈?A" for x using that by simp
  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
      then 
      have "x<5"
        using ‹x<7› ‹x∉?A› ‹n∈nat› in_n_in_nat
        unfolding weak_def
        apply (clarsimp simp add:not_lt_iff_le,auto simp add:lt_def)
        apply(subgoal_tac "0∈n", auto, rule succ_In, simp_all)
        done
      then show ?thesis unfolding sep_var_def using ‹n∈nat› 
        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
  apply (subst sep_var_domain[OF length_type[OF ‹env∈list(M)›],symmetric],subst (1) sep_var_def,auto)
  apply (subst apply_fun[OF sep_var_type],simp add: length_type[OF ‹env∈list(M)›],simp add: sep_var_def,simp)+
  apply (simp add: nth_concat2[OF ‹env∈list(M)›])
  apply (subst apply_fun[OF sep_var_type],simp add: length_type[OF ‹env∈list(M)›],simp add: sep_var_def,simp)
  apply ( simp add: nth_concat3[OF ‹env∈list(M)›,symmetric])
  done

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)" 
    "[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 ‹env∈list(M)›]] 
        ‹arity(φ) ≤ 7 #+ length(env)›]
      rensep_action[OF 1(1),rule_format,symmetric]
    by simp
qed

end