theory DeBruijn
  imports Syntax
begin
  
subsection‹De Bruijn indices›

text‹Functions to find the free $\lambda$ and $\mu$ variables in an expression.›

primrec flv_trm :: "trm → nat → nat set"
    and flv_cmd :: "cmd → nat → nat set"
where
    "flv_trm (`i) k = (if i≥k then {i-k} else {})"
  | "flv_trm (λ T : t) k = flv_trm t (k+1)"
  | "flv_trm (s🚫t) k = (flv_trm s k) ∪ (flv_trm t k)"
  | "flv_trm (μ T : c) k = flv_cmd c k"
  | "flv_cmd (<i> t) k = flv_trm t k"
    
primrec fmv_trm :: "trm → nat → nat set"
    and fmv_cmd :: "cmd → nat → nat set"
where
    "fmv_trm (`i) k = {}"
  | "fmv_trm (λ T : t) k = fmv_trm t k"
  | "fmv_trm (s🚫t) k = (fmv_trm s k) ∪ (fmv_trm t k)"
  | "fmv_trm (μ T : c) k = fmv_cmd c (k+1)"
  | "fmv_cmd (<i> t) k = (if i≥k then {i-k} ∪ (fmv_trm t k) else (fmv_trm t k))"
    
abbreviation lambda_closed :: "_" where
  "lambda_closed t ≡ flv_trm t 0 = {}"
  
abbreviation lambda_closedC :: "_" where
  "lambda_closedC c ≡ flv_cmd c 0 = {}"
    
text‹Free variables in a context.›
  
primrec fmv_ctxt :: "ctxt → nat → nat set" where
    "fmv_ctxt ♢ k = {}"
  | "fmv_ctxt (E ^\<bullet> t) k = (fmv_ctxt E k) ∪ (fmv_trm t k)"     

text‹Shift free $\lambda$ and $\mu$ variables in terms and commands to make substitution capture avoiding.›    
    
primrec
  liftL_trm :: "[trm, nat] → trm" and
  liftL_cmd :: "[cmd, nat] → cmd"
where
  "liftL_trm (`i) k = (if i<k then `i else `(i+1))" |
  "liftL_trm (λ T : t) k = λ T : (liftL_trm t (k+1))" | 
  "liftL_trm (s 🚫 t) k = liftL_trm s k 🚫 liftL_trm t k" |
  "liftL_trm (μ T : c) k = μ T : (liftL_cmd c k)" |
  "liftL_cmd (<i> t) k = <i> (liftL_trm t k)"

primrec
  liftM_trm :: "[trm, nat] → trm" and
  liftM_cmd :: "[cmd, nat] → cmd"
where
  "liftM_trm (`i) k = `i" |
  "liftM_trm (λ T : t) k = λ T : (liftM_trm t k)" |
  "liftM_trm (s 🚫 t) k = liftM_trm s k 🚫 liftM_trm t k" |
  "liftM_trm (μ T : c) k = μ T : (liftM_cmd c (k+1))" |
  "liftM_cmd (<i> t) k =
      (if i<k then (<i> (liftM_trm t k)) else (<i+1> (liftM_trm t k)))"
  
text‹Shift free $\lambda$ and $\mu$ variables in contexts to make structural substitution capture avoiding.›
  
primrec liftL_ctxt :: "ctxt → nat → ctxt" where
  "liftL_ctxt ♢ n = ♢" |
  "liftL_ctxt (E ^\<bullet> t) n = (liftL_ctxt E n) ^\<bullet> (liftL_trm t n)"

primrec liftM_ctxt :: "ctxt → nat → ctxt" where
  "liftM_ctxt ♢ n = ♢" |
  "liftM_ctxt (E ^\<bullet> t) n = (liftM_ctxt E n) ^\<bullet> (liftM_trm t n)"  
  
text‹A function to decrement the indices of free $\mu$-variables when a $\mu$ surrounding the
 expression disappears as a result of a reduction›

primrec
  dropM_trm :: "[trm, nat] → trm" and
  dropM_cmd :: "[cmd, nat] → cmd"
where
    "dropM_trm (`i) k = `i"
  | "dropM_trm (λ T : t) k = λ T : (dropM_trm t k)"
  | "dropM_trm (s 🚫 t) k = (dropM_trm s k) 🚫 (dropM_trm t k)"
  | "dropM_trm (μ T : c) k = μ T : (dropM_cmd c (k+1))"
  | "dropM_cmd (<i> t) k =
      (if i>k then (<i-1> (dropM_trm t k)) else (<i> (dropM_trm t k)))"
    
lemma fmv_liftL: 
  "β ∉ fmv_trm t n ==> β ∉ fmv_trm (liftL_trm t m) n"
  "β ∉ fmv_cmd c n ==> β ∉ fmv_cmd (liftL_cmd c m) n"
  by(induct t and c arbitrary: m n and m n) auto

lemma fmv_liftL_ctxt:
  "β ∉ fmv_ctxt E m ==> β ∉ fmv_ctxt (liftL_ctxt E n) m"
  by(induct E) (fastforce simp add: fmv_liftL)+
    
lemma fmv_suc:
  "β ∉ fmv_cmd c (Suc n) ==> (Suc β) ∉ fmv_cmd c n"
  "β ∉ fmv_trm t (Suc n) ==> (Suc β) ∉ fmv_trm t n"
proof (induct c and t arbitrary: n and n)
  case (MVar x1 x2)
  then show ?case
    by clarsimp (metis UnI1 UnI2 diff_Suc_1 diff_Suc_eq_diff_pred diff_commute diff_is_0_eq nat.simps(3) not_less_eq_eq singletonI)
qed (force)+

lemma flv_drop:
  "flv_trm t k = {} ⟶ flv_trm (dropM_trm t j) k = {}"
  "flv_cmd c k = {} ⟶ flv_cmd (dropM_cmd c j) k = {}"
  by (induct t and c arbitrary: j k and j k) clarsimp+
    
end