Quelle  Substitution.thy

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]<sup>T</sup> =
          (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 ^\<bullet> 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]<sup>T</sup> = (`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,
  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