Theory Renaming

section‹Renaming of variables in internalized formulas›

theory Renaming
  imports
    "ZF-Constructible.Formula"
    ZF_Miscellanea
begin

subsection‹Renaming of free variables›

definition
  union_fun :: "[i,i,i,i] ⇒ i" where
  "union_fun(f,g,m,p) ≡ λj ∈ m ∪ p  . if j∈m then f`j else g`j"

lemma union_fun_type:
  assumes "f ∈ m → n"
    "g ∈ p → q"
  shows "union_fun(f,g,m,p) ∈ m ∪ p → n ∪ q"
proof -
  let ?h="union_fun(f,g,m,p)"
  have
    D: "?h`x ∈ n ∪ q" if "x ∈ m ∪ p" for x
  proof (cases "x ∈ m")
    case True
    then have
      "x ∈ m ∪ p" by simp
    with ‹x∈m›
    have "?h`x = f`x"
      unfolding union_fun_def  beta by simp
    with ‹f ∈ m → n› ‹x∈m›
    have "?h`x ∈ n" by simp
    then show ?thesis ..
  next
    case False
    with ‹x ∈ m ∪ p›
    have "x ∈ p"
      by auto
    with ‹x∉m›
    have "?h`x = g`x"
      unfolding union_fun_def using beta by simp
    with ‹g ∈ p → q› ‹x∈p›
    have "?h`x ∈ q" by simp
    then show ?thesis ..
  qed
  have A:"function(?h)" unfolding union_fun_def using function_lam by simp
  have " x∈ (m ∪ p) × (n ∪ q)" if "x∈ ?h" for x
    using that lamE[of x "m ∪ p" _ "x ∈ (m ∪ p) × (n ∪ q)"] D unfolding union_fun_def
    by auto
  then have B:"?h ⊆ (m ∪ p) × (n ∪ q)" ..
  have "m ∪ p ⊆ domain(?h)"
    unfolding union_fun_def using domain_lam by simp
  with A B
  show ?thesis using  Pi_iff [THEN iffD2] by simp
qed

lemma union_fun_action :
  assumes
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "length(env) = m ∪ p"
    "∀ i . i ∈ m ⟶  nth(f`i,env') = nth(i,env)"
    "∀ j . j ∈ p ⟶ nth(g`j,env') = nth(j,env)"
  shows "∀ i . i ∈ m ∪ p ⟶
          nth(i,env) = nth(union_fun(f,g,m,p)`i,env')"
proof -
  let ?h = "union_fun(f,g,m,p)"
  have "nth(x, env) = nth(?h`x,env')" if "x ∈ m ∪ p" for x
    using that
  proof (cases "x∈m")
    case True
    with ‹x∈m›
    have "?h`x = f`x"
      unfolding union_fun_def  beta by simp
    with assms ‹x∈m›
    have "nth(x,env) = nth(?h`x,env')" by simp
    then show ?thesis .
  next
    case False
    with ‹x ∈ m ∪ p›
    have
      "x ∈ p" "x∉m"  by auto
    then
    have "?h`x = g`x"
      unfolding union_fun_def beta by simp
    with assms ‹x∈p›
    have "nth(x,env) = nth(?h`x,env')" by simp
    then show ?thesis .
  qed
  then show ?thesis by simp
qed


lemma id_fn_type :
  assumes "n ∈ nat"
  shows "id(n) ∈ n → n"
  unfolding id_def using ‹n∈nat› by simp

lemma id_fn_action:
  assumes "n ∈ nat" "env∈list(M)"
  shows "⋀ j . j < n ⟹ nth(j,env) = nth(id(n)`j,env)"
proof -
  show "nth(j,env) = nth(id(n)`j,env)" if "j < n" for j using that ‹n∈nat› ltD by simp
qed


definition
  rsum :: "[i,i,i,i,i] ⇒ i" where
  "rsum(f,g,m,n,p) ≡ λj ∈ m+⇩ωp  . if j<m then f`j else (g`(j#-m))+⇩ωn"

lemma sum_inl:
  assumes "m ∈ nat" "n∈nat"
    "f ∈ m→n" "x ∈ m"
  shows "rsum(f,g,m,n,p)`x = f`x"
proof -
  from ‹m∈nat›
  have "m≤m+⇩ωp"
    using add_le_self[of m] by simp
  with assms
  have "x∈m+⇩ωp"
    using ltI[of x m] lt_trans2[of x m "m+⇩ωp"] ltD by simp
  from assms
  have "x<m"
    using ltI by simp
  with ‹x∈m+⇩ωp›
  show ?thesis unfolding rsum_def by simp
qed

lemma sum_inr:
  assumes "m ∈ nat" "n∈nat" "p∈nat"
    "g∈p→q" "m ≤ x" "x < m+⇩ωp"
  shows "rsum(f,g,m,n,p)`x = g`(x#-m)+⇩ωn"
proof -
  from assms
  have "x∈nat"
    using in_n_in_nat[of "m+⇩ωp"] ltD
    by simp
  with assms
  have "¬ x<m"
    using not_lt_iff_le[THEN iffD2] by simp
  from assms
  have "x∈m+⇩ωp"
    using ltD by simp
  with ‹¬ x<m›
  show ?thesis unfolding rsum_def by simp
qed


lemma sum_action :
  assumes "m ∈ nat" "n∈nat" "p∈nat" "q∈nat"
    "f ∈ m→n" "g∈p→q"
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "env1 ∈ list(M)"
    "env2 ∈ list(M)"
    "length(env) = m"
    "length(env1) = p"
    "length(env') = n"
    "⋀ i . i < m ⟹ nth(i,env) = nth(f`i,env')"
    "⋀ j. j < p ⟹ nth(j,env1) = nth(g`j,env2)"
  shows "∀ i . i < m+⇩ωp ⟶
          nth(i,env@env1) = nth(rsum(f,g,m,n,p)`i,env'@env2)"
proof -
  let ?h = "rsum(f,g,m,n,p)"
  from ‹m∈nat› ‹n∈nat› ‹q∈nat›
  have "m≤m+⇩ωp" "n≤n+⇩ωq" "q≤n+⇩ωq"
    using add_le_self[of m]  add_le_self2[of n q] by simp_all
  from ‹p∈nat›
  have "p = (m+⇩ωp)#-m" using diff_add_inverse2 by simp
  have "nth(x, env @ env1) = nth(?h`x,env'@env2)" if "x<m+⇩ωp" for x
  proof (cases "x<m")
    case True
    then
    have 2: "?h`x= f`x" "x∈m" "f`x ∈ n" "x∈nat"
      using assms sum_inl ltD apply_type[of f m _ x] in_n_in_nat by simp_all
    with ‹x<m› assms
    have "f`x < n" "f`x<length(env')"  "f`x∈nat"
      using ltI in_n_in_nat by simp_all
    with 2 ‹x<m› assms
    have "nth(x,env@env1) = nth(x,env)"
      using nth_append[OF ‹env∈list(M)›] ‹x∈nat› by simp
    also
    have
      "... = nth(f`x,env')"
      using 2 ‹x<m› assms by simp
    also
    have "... = nth(f`x,env'@env2)"
      using nth_append[OF ‹env'∈list(M)›] ‹f`x<length(env')› ‹f`x ∈nat› by simp
    also
    have "... = nth(?h`x,env'@env2)"
      using 2 by simp
    finally
    have "nth(x, env @ env1) = nth(?h`x,env'@env2)" .
    then show ?thesis .
  next
    case False
    have "x∈nat"
      using that in_n_in_nat[of "m+⇩ωp" x] ltD ‹p∈nat› ‹m∈nat› by simp
    with ‹length(env) = m›
    have "m≤x" "length(env) ≤ x"
      using not_lt_iff_le ‹m∈nat› ‹¬x<m› by simp_all
    with ‹¬x<m› ‹length(env) = m›
    have 2 : "?h`x= g`(x#-m)+⇩ωn"  "¬ x <length(env)"
      unfolding rsum_def
      using  sum_inr that beta ltD by simp_all
    from assms ‹x∈nat› ‹p=m+⇩ωp#-m›
    have "x#-m < p"
      using diff_mono[OF _ _ _ ‹x<m+⇩ωp› ‹m≤x›] by simp
    then have "x#-m∈p" using ltD by simp
    with ‹g∈p→q›
    have "g`(x#-m) ∈ q"  by simp
    with ‹q∈nat› ‹length(env') = n›
    have "g`(x#-m) < q" "g`(x#-m)∈nat" using ltI in_n_in_nat by simp_all
    with ‹q∈nat› ‹n∈nat›
    have "(g`(x#-m))+⇩ωn <n+⇩ωq" "n ≤ g`(x#-m)+⇩ωn" "¬ g`(x#-m)+⇩ωn < length(env')"
      using add_lt_mono1[of "g`(x#-m)" _ n,OF _ ‹q∈nat›]
        add_le_self2[of n] ‹length(env') = n›
      by simp_all
    from assms ‹¬ x < length(env)› ‹length(env) = m›
    have "nth(x,env @ env1) = nth(x#-m,env1)"
      using nth_append[OF ‹env∈list(M)› ‹x∈nat›] by simp
    also
    have "... = nth(g`(x#-m),env2)"
      using assms ‹x#-m < p› by simp
    also
    have "... = nth((g`(x#-m)+⇩ωn)#-length(env'),env2)"
      using  ‹length(env') = n›
        diff_add_inverse2 ‹g`(x#-m)∈nat›
      by simp
    also
    have "... = nth((g`(x#-m)+⇩ωn),env'@env2)"
      using  nth_append[OF ‹env'∈list(M)›] ‹n∈nat› ‹¬ g`(x#-m)+⇩ωn < length(env')›
      by simp
    also
    have "... = nth(?h`x,env'@env2)"
      using 2 by simp
    finally
    have "nth(x, env @ env1) = nth(?h`x,env'@env2)" .
    then show ?thesis .
  qed
  then show ?thesis by simp
qed

lemma sum_type  :
  assumes "m ∈ nat" "n∈nat" "p∈nat" "q∈nat"
    "f ∈ m→n" "g∈p→q"
  shows "rsum(f,g,m,n,p) ∈ (m+⇩ωp) → (n+⇩ωq)"
proof -
  let ?h = "rsum(f,g,m,n,p)"
  from ‹m∈nat› ‹n∈nat› ‹q∈nat›
  have "m≤m+⇩ωp" "n≤n+⇩ωq" "q≤n+⇩ωq"
    using add_le_self[of m]  add_le_self2[of n q] by simp_all
  from ‹p∈nat›
  have "p = (m+⇩ωp)#-m" using diff_add_inverse2 by simp
  {fix x
    assume 1: "x∈m+⇩ωp" "x<m"
    with 1 have "?h`x= f`x" "x∈m"
      using assms sum_inl ltD by simp_all
    with ‹f∈m→n›
    have "?h`x ∈ n" by simp
    with ‹n∈nat› have "?h`x < n" using ltI by simp
    with ‹n≤n+⇩ωq›
    have "?h`x < n+⇩ωq" using lt_trans2 by simp
    then
    have "?h`x ∈ n+⇩ωq"  using ltD by simp
  }
  then have 1:"?h`x ∈ n+⇩ωq" if "x∈m+⇩ωp" "x<m" for x using that .
  {fix x
    assume 1: "x∈m+⇩ωp" "m≤x"
    then have "x<m+⇩ωp" "x∈nat" using ltI in_n_in_nat[of "m+⇩ωp"] ltD by simp_all
    with 1
    have 2 : "?h`x= g`(x#-m)+⇩ωn"
      using assms sum_inr ltD by simp_all
    from assms ‹x∈nat› ‹p=m+⇩ωp#-m›
    have "x#-m < p" using diff_mono[OF _ _ _ ‹x<m+⇩ωp› ‹m≤x›] by simp
    then have "x#-m∈p" using ltD by simp
    with ‹g∈p→q›
    have "g`(x#-m) ∈ q"  by simp
    with ‹q∈nat› have "g`(x#-m) < q" using ltI by simp
    with ‹q∈nat›
    have "(g`(x#-m))+⇩ωn <n+⇩ωq" using add_lt_mono1[of "g`(x#-m)" _ n,OF _ ‹q∈nat›] by simp
    with 2
    have "?h`x ∈ n+⇩ωq"  using ltD by simp
  }
  then have 2:"?h`x ∈ n+⇩ωq" if "x∈m+⇩ωp" "m≤x" for x using that .
  have
    D: "?h`x ∈ n+⇩ωq" if "x∈m+⇩ωp" for x
    using that
  proof (cases "x<m")
    case True
    then show ?thesis using 1 that by simp
  next
    case False
    with ‹m∈nat› have "m≤x" using not_lt_iff_le that in_n_in_nat[of "m+⇩ωp"] by simp
    then show ?thesis using 2 that by simp
  qed
  have A:"function(?h)" unfolding rsum_def using function_lam by simp
  have " x∈ (m +⇩ω p) × (n +⇩ω q)" if "x∈ ?h" for x
    using that lamE[of x "m+⇩ωp" _ "x ∈ (m +⇩ω p) × (n +⇩ω q)"] D unfolding rsum_def
    by auto
  then have B:"?h ⊆ (m +⇩ω p) × (n +⇩ω q)" ..
  have "m +⇩ω p ⊆ domain(?h)"
    unfolding rsum_def using domain_lam by simp
  with A B
  show ?thesis using  Pi_iff [THEN iffD2] by simp
qed

lemma sum_type_id :
  assumes
    "f ∈ length(env)→length(env')"
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "env1 ∈ list(M)"
  shows
    "rsum(f,id(length(env1)),length(env),length(env'),length(env1)) ∈
        (length(env)+⇩ωlength(env1)) → (length(env')+⇩ωlength(env1))"
  using assms length_type id_fn_type sum_type
  by simp

lemma sum_type_id_aux2 :
  assumes
    "f ∈ m→n"
    "m ∈ nat" "n ∈ nat"
    "env1 ∈ list(M)"
  shows
    "rsum(f,id(length(env1)),m,n,length(env1)) ∈
        (m+⇩ωlength(env1)) → (n+⇩ωlength(env1))"
  using assms id_fn_type sum_type
  by auto

lemma sum_action_id :
  assumes
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "f ∈ length(env)→length(env')"
    "env1 ∈ list(M)"
    "⋀ i . i < length(env) ⟹ nth(i,env) = nth(f`i,env')"
  shows "⋀ i . i < length(env)+⇩ωlength(env1) ⟹
          nth(i,env@env1) = nth(rsum(f,id(length(env1)),length(env),length(env'),length(env1))`i,env'@env1)"
proof -
  from assms
  have "length(env)∈nat" (is "?m ∈ _") by simp
  from assms have "length(env')∈nat" (is "?n ∈ _") by simp
  from assms have "length(env1)∈nat" (is "?p ∈ _") by simp
  note lenv = id_fn_action[OF ‹?p∈nat› ‹env1∈list(M)›]
  note lenv_ty = id_fn_type[OF ‹?p∈nat›]
  {
    fix i
    assume "i < length(env)+⇩ωlength(env1)"
    have "nth(i,env@env1) = nth(rsum(f,id(length(env1)),?m,?n,?p)`i,env'@env1)"
      using sum_action[OF ‹?m∈nat› ‹?n∈nat› ‹?p∈nat› ‹?p∈nat› ‹f∈?m→?n›
          lenv_ty ‹env∈list(M)› ‹env'∈list(M)›
          ‹env1∈list(M)› ‹env1∈list(M)› _
          _ _  assms(5) lenv
          ] ‹i<?m+⇩ωlength(env1)› by simp
  }
  then show "⋀ i . i < ?m+⇩ωlength(env1) ⟹
          nth(i,env@env1) = nth(rsum(f,id(?p),?m,?n,?p)`i,env'@env1)" by simp
qed

lemma sum_action_id_aux :
  assumes
    "f ∈ m→n"
    "env ∈ list(M)"
    "env' ∈ list(M)"
    "env1 ∈ list(M)"
    "length(env) = m"
    "length(env') = n"
    "length(env1) = p"
    "⋀ i . i < m ⟹ nth(i,env) = nth(f`i,env')"
  shows "⋀ i . i < m+⇩ωlength(env1) ⟹
          nth(i,env@env1) = nth(rsum(f,id(length(env1)),m,n,length(env1))`i,env'@env1)"
  using assms length_type id_fn_type sum_action_id
  by auto


definition
  sum_id :: "[i,i] ⇒ i" where
  "sum_id(m,f) ≡ rsum(λx∈1.x,f,1,1,m)"

lemma sum_id0 : "m∈nat⟹sum_id(m,f)`0 = 0"
  by(unfold sum_id_def,subst sum_inl,auto)

lemma sum_idS : "p∈nat ⟹ q∈nat ⟹ f∈p→q ⟹ x ∈ p ⟹ sum_id(p,f)`(succ(x)) = succ(f`x)"
  by(subgoal_tac "x∈nat",unfold sum_id_def,subst sum_inr,
      simp_all add:ltI,simp_all add: app_nm in_n_in_nat)

lemma sum_id_tc_aux :
  "p ∈ nat ⟹  q ∈ nat ⟹ f ∈ p → q ⟹ sum_id(p,f) ∈ 1+⇩ωp → 1+⇩ωq"
  by (unfold sum_id_def,rule sum_type,simp_all)

lemma sum_id_tc :
  "n ∈ nat ⟹ m ∈ nat ⟹ f ∈ n → m ⟹ sum_id(n,f) ∈ succ(n) → succ(m)"
  by(rule ssubst[of  "succ(n) → succ(m)" "1+⇩ωn → 1+⇩ωm"],
      simp,rule sum_id_tc_aux,simp_all)

subsection‹Renaming of formulas›

consts   ren :: "i⇒i"
primrec
  "ren(Member(x,y)) =
      (λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Member (f`x, f`y))"

"ren(Equal(x,y)) =
      (λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Equal (f`x, f`y))"

"ren(Nand(p,q)) =
      (λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Nand (ren(p)`n`m`f, ren(q)`n`m`f))"

"ren(Forall(p)) =
      (λ n ∈ nat . λ m ∈ nat. λf ∈ n → m. Forall (ren(p)`succ(n)`succ(m)`sum_id(n,f)))"

lemma arity_meml : "l ∈ nat ⟹ Member(x,y) ∈ formula ⟹ arity(Member(x,y)) ≤ l ⟹ x ∈ l"
  by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma arity_memr : "l ∈ nat ⟹ Member(x,y) ∈ formula ⟹ arity(Member(x,y)) ≤ l ⟹ y ∈ l"
  by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma arity_eql : "l ∈ nat ⟹ Equal(x,y) ∈ formula ⟹ arity(Equal(x,y)) ≤ l ⟹ x ∈ l"
  by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma arity_eqr : "l ∈ nat ⟹ Equal(x,y) ∈ formula ⟹ arity(Equal(x,y)) ≤ l ⟹ y ∈ l"
  by(simp,rule subsetD,rule le_imp_subset,assumption,simp)
lemma  nand_ar1 : "p ∈ formula ⟹ q∈formula ⟹arity(p) ≤ arity(Nand(p,q))"
  by (simp,rule Un_upper1_le,simp+)
lemma nand_ar2 : "p ∈ formula ⟹ q∈formula ⟹arity(q) ≤ arity(Nand(p,q))"
  by (simp,rule Un_upper2_le,simp+)

lemma nand_ar1D : "p ∈ formula ⟹ q∈formula ⟹ arity(Nand(p,q)) ≤ n ⟹ arity(p) ≤ n"
  by(auto simp add:  le_trans[OF Un_upper1_le[of "arity(p)" "arity(q)"]])
lemma nand_ar2D : "p ∈ formula ⟹ q∈formula ⟹ arity(Nand(p,q)) ≤ n ⟹ arity(q) ≤ n"
  by(auto simp add:  le_trans[OF Un_upper2_le[of "arity(p)" "arity(q)"]])


lemma ren_tc : "p ∈ formula ⟹
  (⋀ n m f . n ∈ nat ⟹ m ∈ nat ⟹ f ∈ n→m ⟹  ren(p)`n`m`f ∈ formula)"
  by (induct set:formula,auto simp add: app_nm sum_id_tc)


lemma arity_ren :
  fixes "p"
  assumes "p ∈ formula"
  shows "⋀ n m f . n ∈ nat ⟹ m ∈ nat ⟹ f ∈ n→m ⟹ arity(p) ≤ n ⟹ arity(ren(p)`n`m`f)≤m"
  using assms
proof (induct set:formula)
  case (Member x y)
  then have "f`x ∈ m" "f`y ∈ m"
    using Member assms by (simp add: arity_meml apply_funtype,simp add:arity_memr apply_funtype)
  then show ?case using Member by (simp add: Un_least_lt ltI)
next
  case (Equal x y)
  then have "f`x ∈ m" "f`y ∈ m"
    using Equal assms by (simp add: arity_eql apply_funtype,simp add:arity_eqr apply_funtype)
  then show ?case using Equal by (simp add: Un_least_lt ltI)
next
  case (Nand p q)
  then have "arity(p)≤arity(Nand(p,q))"
    "arity(q)≤arity(Nand(p,q))"
    by (subst  nand_ar1,simp,simp,simp,subst nand_ar2,simp+)
  then have "arity(p)≤n"
    and "arity(q)≤n" using Nand
    by (rule_tac j="arity(Nand(p,q))" in le_trans,simp,simp)+
  then have "arity(ren(p)`n`m`f) ≤ m" and  "arity(ren(q)`n`m`f) ≤ m"
    using Nand by auto
  then show ?case using Nand by (simp add:Un_least_lt)
next
  case (Forall p)
  from Forall have "succ(n)∈nat"  "succ(m)∈nat" by auto
  from Forall have 2: "sum_id(n,f) ∈ succ(n)→succ(m)" by (simp add:sum_id_tc)
  from Forall have 3:"arity(p) ≤ succ(n)" by (rule_tac n="arity(p)" in natE,simp+)
  then have "arity(ren(p)`succ(n)`succ(m)`sum_id(n,f))≤succ(m)" using
      Forall ‹succ(n)∈nat› ‹succ(m)∈nat› 2 by force
  then show ?case using Forall 2 3 ren_tc arity_type pred_le by auto
qed

lemma arity_forallE : "p ∈ formula ⟹ m ∈ nat ⟹ arity(Forall(p)) ≤ m ⟹ arity(p) ≤ succ(m)"
  by(rule_tac n="arity(p)" in natE,erule arity_type,simp+)

lemma env_coincidence_sum_id :
  assumes "m ∈ nat" "n ∈ nat"
    "ρ ∈ list(A)" "ρ' ∈ list(A)"
    "f ∈ n → m"
    "⋀ i . i < n ⟹ nth(i,ρ) = nth(f`i,ρ')"
    "a ∈ A" "j ∈ succ(n)"
  shows "nth(j,Cons(a,ρ)) = nth(sum_id(n,f)`j,Cons(a,ρ'))"
proof -
  let ?g="sum_id(n,f)"
  have "succ(n) ∈ nat" using ‹n∈nat› by simp
  then have "j ∈ nat" using ‹j∈succ(n)› in_n_in_nat by blast
  then have "nth(j,Cons(a,ρ)) = nth(?g`j,Cons(a,ρ'))"
  proof (cases rule:natE[OF ‹j∈nat›])
    case 1
    then show ?thesis using assms sum_id0 by simp
  next
    case (2 i)
    with ‹j∈succ(n)› have "succ(i)∈succ(n)" by simp
    with ‹n∈nat› have "i ∈ n" using nat_succD assms by simp
    have "f`i∈m" using ‹f∈n→m› apply_type ‹i∈n› by simp
    then have "f`i ∈ nat" using in_n_in_nat ‹m∈nat› by simp
    have "nth(succ(i),Cons(a,ρ)) = nth(i,ρ)" using ‹i∈nat› by simp
    also have "... = nth(f`i,ρ')" using assms ‹i∈n› ltI by simp
    also have "... = nth(succ(f`i),Cons(a,ρ'))" using ‹f`i∈nat› by simp
    also have "... = nth(?g`succ(i),Cons(a,ρ'))"
      using assms sum_idS[OF ‹n∈nat› ‹m∈nat›  ‹f∈n→m› ‹i ∈ n›] cases by simp
    finally have "nth(succ(i),Cons(a,ρ)) = nth(?g`succ(i),Cons(a,ρ'))" .
    then show ?thesis using ‹j=succ(i)› by simp
  qed
  then show ?thesis .
qed

lemma sats_iff_sats_ren :
  assumes "φ ∈ formula"
  shows  "⟦  n ∈ nat ; m ∈ nat ; ρ ∈ list(M) ; ρ' ∈ list(M) ; f ∈ n → m ;
            arity(φ) ≤ n ;
            ⋀ i . i < n ⟹ nth(i,ρ) = nth(f`i,ρ') ⟧ ⟹
         sats(M,φ,ρ) ⟷ sats(M,ren(φ)`n`m`f,ρ')"
  using ‹φ ∈ formula›
proof(induct φ arbitrary:n m ρ ρ' f)
  case (Member x y)
  have "ren(Member(x,y))`n`m`f = Member(f`x,f`y)" using Member assms arity_type by force
  moreover
  have "x ∈ n" using Member arity_meml by simp
  moreover
  have "y ∈ n" using Member arity_memr by simp
  ultimately
  show ?case using Member ltI by simp
next
  case (Equal x y)
  have "ren(Equal(x,y))`n`m`f = Equal(f`x,f`y)" using Equal assms arity_type by force
  moreover
  have "x ∈ n" using Equal arity_eql by simp
  moreover
  have "y ∈ n" using Equal arity_eqr by simp
  ultimately show ?case using Equal ltI by simp
next
  case (Nand p q)
  have "ren(Nand(p,q))`n`m`f = Nand(ren(p)`n`m`f,ren(q)`n`m`f)" using Nand by simp
  moreover
  have "arity(p) ≤ n" using Nand nand_ar1D by simp
  moreover from this
  have "i ∈ arity(p) ⟹ i ∈ n" for i using subsetD[OF le_imp_subset[OF ‹arity(p) ≤ n›]] by simp
  moreover from this
  have "i ∈ arity(p) ⟹ nth(i,ρ) = nth(f`i,ρ')" for i using Nand ltI by simp
  moreover from this
  have "sats(M,p,ρ) ⟷ sats(M,ren(p)`n`m`f,ρ')" using ‹arity(p)≤n› Nand by simp
  have "arity(q) ≤ n" using Nand nand_ar2D by simp
  moreover from this
  have "i ∈ arity(q) ⟹ i ∈ n" for i using subsetD[OF le_imp_subset[OF ‹arity(q) ≤ n›]] by simp
  moreover from this
  have "i ∈ arity(q) ⟹ nth(i,ρ) = nth(f`i,ρ')" for i using Nand ltI by simp
  moreover from this
  have "sats(M,q,ρ) ⟷ sats(M,ren(q)`n`m`f,ρ')" using assms ‹arity(q)≤n› Nand by simp
  ultimately
  show ?case using Nand by simp
next
  case (Forall p)
  have 0:"ren(Forall(p))`n`m`f = Forall(ren(p)`succ(n)`succ(m)`sum_id(n,f))"
    using Forall by simp
  have 1:"sum_id(n,f) ∈ succ(n) → succ(m)" (is "?g ∈ _") using sum_id_tc Forall by simp
  then have 2: "arity(p) ≤ succ(n)"
    using Forall le_trans[of _ "succ(pred(arity(p)))"] succpred_leI by simp
  have "succ(n)∈nat" "succ(m)∈nat" using Forall by auto
  then have A:"⋀ j .j < succ(n) ⟹ nth(j, Cons(a, ρ)) = nth(?g`j, Cons(a, ρ'))" if "a∈M" for a
    using that env_coincidence_sum_id Forall ltD by force
  have
    "sats(M,p,Cons(a,ρ)) ⟷ sats(M,ren(p)`succ(n)`succ(m)`?g,Cons(a,ρ'))" if "a∈M" for a
  proof -
    have C:"Cons(a,ρ) ∈ list(M)" "Cons(a,ρ')∈list(M)" using Forall that by auto
    have "sats(M,p,Cons(a,ρ)) ⟷ sats(M,ren(p)`succ(n)`succ(m)`?g,Cons(a,ρ'))"
      using Forall(2)[OF ‹succ(n)∈nat› ‹succ(m)∈nat› C(1) C(2) 1 2 A[OF ‹a∈M›]] by simp
    then show ?thesis .
  qed
  then show ?case using Forall 0 1 2 by simp
qed

end