Theory Renaming

section‹Renaming of variables in internalized formulas›

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

lemma app_nm :
  assumes "nnat" "mnat" "fnm" "x  nat"
  shows "f`x  nat"
proof(cases "xn")
  case True
  then show ?thesis using assms in_n_in_nat apply_type by simp
next
  case False
  then show ?thesis using assms apply_0 domain_of_fun by simp
qed

subsection‹Renaming of free variables›

definition
  union_fun :: "[i,i,i,i]  i" where
  "union_fun(f,g,m,p)  λj  m  p  . if jm 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 xm
    have "?h`x = f`x"
      unfolding union_fun_def  beta by simp
    with f  m  n xm
    have "?h`x  n" by simp
    then show ?thesis ..
  next
    case False
    with x  m  p
    have "x  p"
      by auto
    with xm
    have "?h`x = g`x"
      unfolding union_fun_def using beta by simp
    with g  p  q xp
    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 "xm")
    case True
    with xm
    have "?h`x = f`x"
      unfolding union_fun_def  beta by simp
    with assms xm
    have "nth(x,env) = nth(?h`x,env')" by simp
    then show ?thesis .
  next
    case False
    with x  m  p
    have
      "x  p" "xm"  by auto
    then
    have "?h`x = g`x"
      unfolding union_fun_def beta by simp
    with assms xp
    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 nnat by simp

lemma id_fn_action:
  assumes "n  nat" "envlist(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 nnat ltD by simp
qed


definition
  sum :: "[i,i,i,i,i]  i" where
  "sum(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" "nnat"
    "f  mn" "x  m"
  shows "sum(f,g,m,n,p)`x = f`x"
proof -
  from mnat
  have "mm#+p"
    using add_le_self[of m] by simp
  with assms
  have "xm#+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 xm#+p
  show ?thesis unfolding sum_def by simp
qed

lemma sum_inr:
  assumes "m  nat" "nnat" "pnat"
    "gpq" "m  x" "x < m#+p"
  shows "sum(f,g,m,n,p)`x = g`(x#-m)#+n"
proof -
  from assms
  have "xnat"
    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 "xm#+p"
    using ltD by simp
  with ¬ x<m
  show ?thesis unfolding sum_def by simp
qed


lemma sum_action :
  assumes "m  nat" "nnat" "pnat" "qnat"
    "f  mn" "gpq"
    "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(sum(f,g,m,n,p)`i,env'@env2)"
proof -
  let ?h = "sum(f,g,m,n,p)"
  from mnat nnat qnat
  have "mm#+p" "nn#+q" "qn#+q"
    using add_le_self[of m]  add_le_self2[of n q] by simp_all
  from pnat
  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" "xm" "f`x  n" "xnat"
      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`xnat"
      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 envlist(M)] xnat 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 "xnat"
      using that in_n_in_nat[of "m#+p" x] ltD pnat mnat by simp
    with length(env) = m
    have "mx" "length(env)  x"
      using not_lt_iff_le mnat ¬x<m by simp_all
    with ¬x<m length(env) = m
    have 2 : "?h`x= g`(x#-m)#+n"  "¬ x <length(env)"
      unfolding sum_def
      using  sum_inr that beta ltD by simp_all
    from assms xnat p=m#+p#-m
    have "x#-m < p"
      using diff_mono[OF _ _ _ x<m#+p mx] by simp
    then have "x#-mp" using ltD by simp
    with gpq
    have "g`(x#-m)  q"  by simp
    with qnat length(env') = n
    have "g`(x#-m) < q" "g`(x#-m)nat" using ltI in_n_in_nat by simp_all
    with qnat nnat
    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 _ qnat]
        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 envlist(M) xnat] 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)] nnat ¬ 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" "nnat" "pnat" "qnat"
    "f  mn" "gpq"
  shows "sum(f,g,m,n,p)  (m#+p)  (n#+q)"
proof -
  let ?h = "sum(f,g,m,n,p)"
  from mnat nnat qnat
  have "mm#+p" "nn#+q" "qn#+q"
    using add_le_self[of m]  add_le_self2[of n q] by simp_all
  from pnat
  have "p = (m#+p)#-m" using diff_add_inverse2 by simp
  {fix x
    assume 1: "xm#+p" "x<m"
    with 1 have "?h`x= f`x" "xm"
      using assms sum_inl ltD by simp_all
    with fmn
    have "?h`x  n" by simp
    with nnat have "?h`x < n" using ltI by simp
    with nn#+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 "xm#+p" "x<m" for x using that .
  {fix x
    assume 1: "xm#+p" "mx"
    then have "x<m#+p" "xnat" 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 xnat p=m#+p#-m
    have "x#-m < p" using diff_mono[OF _ _ _ x<m#+p mx] by simp
    then have "x#-mp" using ltD by simp
    with gpq
    have "g`(x#-m)  q"  by simp
    with qnat have "g`(x#-m) < q" using ltI by simp
    with qnat
    have "(g`(x#-m))#+n <n#+q" using add_lt_mono1[of "g`(x#-m)" _ n,OF _ qnat] by simp
    with 2
    have "?h`x  n#+q"  using ltD by simp
  }
  then have 2:"?h`x  n#+q" if "xm#+p" "mx" for x using that .
  have
    D: "?h`x  n#+q" if "xm#+p" for x
    using that
  proof (cases "x<m")
    case True
    then show ?thesis using 1 that by simp
  next
    case False
    with mnat have "mx" 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 sum_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 sum_def
    by auto
  then have B:"?h  (m #+ p) × (n #+ q)" ..
  have "m #+ p  domain(?h)"
    unfolding sum_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
    "sum(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  mn"
    "m  nat" "n  nat"
    "env1  list(M)"
  shows
    "sum(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(sum(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 ?pnat env1list(M)]
  note lenv_ty = id_fn_type[OF ?pnat]
  {
    fix i
    assume "i < length(env)#+length(env1)"
    have "nth(i,env@env1) = nth(sum(f,id(length(env1)),?m,?n,?p)`i,env'@env1)"
      using sum_action[OF ?mnat ?nnat ?pnat ?pnat f?m?n
          lenv_ty envlist(M) env'list(M)
          env1list(M) env1list(M) _
          _ _  assms(5) lenv
          ] i<?m#+length(env1) by simp
  }
  then show " i . i < ?m#+length(env1) 
          nth(i,env@env1) = nth(sum(f,id(?p),?m,?n,?p)`i,env'@env1)" by simp
qed

lemma sum_action_id_aux :
  assumes
    "f  mn"
    "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(sum(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)  sum(λx1.x,f,1,1,m)"

lemma sum_id0 : "mnatsum_id(m,f)`0 = 0"
  by(unfold sum_id_def,subst sum_inl,auto)

lemma sum_idS : "pnat  qnat  fpq  x  p  sum_id(p,f)`(succ(x)) = succ(f`x)"
  by(subgoal_tac "xnat",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 :: "ii"
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  qformula arity(p)  arity(Nand(p,q))"
  by (simp,rule Un_upper1_le,simp+)
lemma nand_ar2 : "p  formula  qformula arity(q)  arity(Nand(p,q))"
  by (simp,rule Un_upper2_le,simp+)

lemma nand_ar1D : "p  formula  qformula  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  qformula  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  nm   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  nm  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 nnat by simp
  then have "j  nat" using jsucc(n) in_n_in_nat by blast
  then have "nth(j,Cons(a,ρ)) = nth(?g`j,Cons(a,ρ'))"
  proof (cases rule:natE[OF jnat])
    case 1
    then show ?thesis using assms sum_id0 by simp
  next
    case (2 i)
    with jsucc(n) have "succ(i)succ(n)" by simp
    with nnat have "i  n" using nat_succD assms by simp
    have "f`im" using fnm apply_type in by simp
    then have "f`i  nat" using in_n_in_nat mnat by simp
    have "nth(succ(i),Cons(a,ρ)) = nth(i,ρ)" using inat by simp
    also have "... = nth(f`i,ρ')" using assms in ltI by simp
    also have "... = nth(succ(f`i),Cons(a,ρ'))" using f`inat by simp
    also have "... = nth(?g`succ(i),Cons(a,ρ'))"
      using assms sum_idS[OF nnat mnat  fnm 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 :
  fixes "φ"
  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 "aM" 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 "aM" 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 aM]] by simp
    then show ?thesis .
  qed
  then show ?case using Forall 0 1 2 by simp
qed

end