Theory Substitution

subsection‹Logical and structural substitution›
  
theory Substitution
  imports DeBruijn
begin 

primrec
  subst_trm :: "[trm, trm, nat] ⇒ trm"  (‹_[_'/_]⇧T› [300, 0, 0] 300) and
  subst_cmd ::  "[cmd, trm, nat] ⇒ cmd" (‹_[_'/_]⇧C› [300, 0, 0] 300)
where
    subst_LVar: "(`i)[s/k]⇧T = 
          (if k < i then `(i-1) else if k = i then s else (`i))"
    | subst_Lbd: "(λ T : t)[s/k]⇧T = λ T : (t[(liftL_trm s 0) / k+1]⇧T)"
    | subst_App: "(t ° u)[s/k]⇧T = t[s/k]⇧T ° u[s/k]⇧T"
    | subst_Mu: "(μ T : c)[s/k]⇧T  = μ T : (c[(liftM_trm s 0) / k]⇧C)"
    | subst_MVar: "(<i> t)[s/k]⇧C = <i> (t[s/k]⇧T)"

text‹Substituting a term for the hole in a context.›
  
primrec ctxt_subst :: "ctxt ⇒ trm ⇒ trm" where
  "ctxt_subst ◇ s = s" |
  "ctxt_subst (E ⇧∙ t) s = (ctxt_subst E s)° t"

lemma ctxt_app_subst:
  shows "ctxt_subst E (ctxt_subst F t) = ctxt_subst (E . F) t"
  by (induction E, auto)
    
text‹The structural substitution is based on Geuvers and al.~\<^cite>‹"DBLP:journals/apal/GeuversKM13"›.›

primrec
  struct_subst_trm :: "[trm, nat, nat, ctxt] ⇒ trm"  (‹_[_=_ _]⇧T› [300, 0, 0, 0] 300) and
  struct_subst_cmd ::  "[cmd, nat, nat, ctxt] ⇒ cmd" (‹_[_=_ _]⇧C› [300, 0, 0, 0] 300)
where
  struct_LVar: "(`i)[j=k E]⇧T = (`i)" |
  struct_Lbd: "(λ T : t)[j=k E]⇧T = (λ T : (t[j=k (liftL_ctxt E 0)]⇧T))" |
  struct_App: "(t°s)[j=k E]⇧T = (t[j=k E]⇧T)°(s[j=k E]⇧T)" |
  struct_Mu: "(μ T : c)[j=k E]⇧T = μ T : (c[(j+1)=(k+1) (liftM_ctxt E 0)]⇧C)" |
  struct_MVar: "(<i> t)[j=k E]⇧C = 
      (if i=j then (<k> (ctxt_subst E (t[j=k E]⇧T))) 
       else (if j<i ∧ i≤k then (<i-1> (t[j=k E]⇧T))
             else (if k≤i ∧ i<j then (<i+1> (t[j=k E]⇧T))
                   else (<i> (t[j=k E]⇧T)))))"

text‹Lifting of lambda and mu variables commute with each other›

lemma liftLM_comm: 
  "liftL_trm (liftM_trm t n) m = liftM_trm (liftL_trm t m) n"
  "liftL_cmd (liftM_cmd c n) m = liftM_cmd (liftL_cmd c m) n"
  by(induct t and c arbitrary: n m and n m) auto

lemma liftLM_comm_ctxt:
  "liftL_ctxt (liftM_ctxt E n) m = liftM_ctxt (liftL_ctxt E m) n"
  by(induct E arbitrary: n m, auto simp add: liftLM_comm)

text‹Lifting of $\mu$-variables (almost) commutes.›

lemma liftMM_comm:
  "n≥m ⟹ liftM_trm (liftM_trm t n) m = liftM_trm (liftM_trm t m) (Suc n)"
  "n≥m ⟹ liftM_cmd (liftM_cmd c n) m = liftM_cmd (liftM_cmd c m) (Suc n)"
  by(induct t and c arbitrary: n m and n m) auto

lemma liftMM_comm_ctxt:
  "liftM_ctxt (liftM_ctxt E n) 0 = liftM_ctxt (liftM_ctxt E 0) (n+1)"
  by(induct E arbitrary: n, auto simp add: liftMM_comm)

text‹If a $\mu$ variable $i$ doesn't occur in a term or a context, 
then these remain the same after structural substitution of variable $i$.›

lemma liftM_struct_subst: 
  "liftM_trm t i[i=i F]⇧T = liftM_trm t i"
  "liftM_cmd c i[i=i F]⇧C = liftM_cmd c i"
  by(induct t and c arbitrary: i F and i F) auto

lemma liftM_ctxt_struct_subst:
  "(ctxt_subst (liftM_ctxt E i) t)[i=i F]⇧T = ctxt_subst (liftM_ctxt E i) (t[i=i F]⇧T)"
  by(induct E arbitrary: i t F; force simp add: liftM_struct_subst)

end