Theory SmallStepLam

section ‹Small-step semantics of CBV lambda calculus›

theory SmallStepLam
  imports Lambda
begin
  
text‹
  The following substitution function is not capture avoiding, so it has a precondition
  that $v$ is closed. With hindsight, we should have used DeBruijn indices instead
  because we also use substitution in the optimizing compiler.
›
fun subst :: "name ⇒ exp ⇒ exp ⇒ exp" where
  "subst x v (EVar y) = (if x = y then v else EVar y)" |
  "subst x v (ENat n) = ENat n" |
  "subst x v (ELam y e) = (if x = y then ELam y e else ELam y (subst x v e))" |
  "subst x v (EApp e1 e2) = EApp (subst x v e1) (subst x v e2)" |
  "subst x v (EPrim f e1 e2) = EPrim f (subst x v e1) (subst x v e2)" |
  "subst x v (EIf e1 e2 e3) = EIf (subst x v e1) (subst x v e2) (subst x v e3)"

inductive isval :: "exp ⇒ bool" where
  valnat[intro!]: "isval (ENat n)" |
  vallam[intro!]: "isval (ELam x e)"

inductive_cases
  isval_var_inv[elim!]: "isval (EVar x)" and
  isval_app_inv[elim!]: "isval (EApp e1 e2)" and
  isval_prim_inv[elim!]: "isval (EPrim f e1 e2)" and
  isval_if_inv[elim!]: "isval (EIf e1 e2 e3)" 

definition is_val :: "exp ⇒ bool" where
  "is_val v ≡ isval v ∧ FV v = {}"
declare is_val_def[simp]

inductive reduce :: "exp ⇒ exp ⇒ bool" (infix ‹⟶› 55) where
  beta[intro!]: "⟦ is_val v ⟧ ⟹ EApp (ELam x e) v ⟶ (subst x v e)" |
  app_left[intro!]: "⟦ e1 ⟶ e1' ⟧ ⟹ EApp e1 e2 ⟶ EApp e1' e2" |
  app_right[intro!]: "⟦ e2 ⟶ e2' ⟧ ⟹ EApp e1 e2 ⟶ EApp e1 e2'" |
  delta[intro!]: "EPrim f (ENat n1) (ENat n2) ⟶ ENat (f n1 n2)" |
  prim_left[intro!]: "⟦ e1 ⟶ e1' ⟧ ⟹ EPrim f e1 e2 ⟶ EPrim f e1' e2" |
  prim_right[intro!]: "⟦ e2 ⟶ e2' ⟧ ⟹ EPrim f e1 e2 ⟶ EPrim f e1 e2'" |
  if_zero[intro!]: "EIf (ENat 0) thn els ⟶ els" |
  if_nz[intro!]: "n ≠ 0 ⟹ EIf (ENat n) thn els ⟶ thn" |
  if_cond[intro!]: "⟦ cond ⟶ cond' ⟧ ⟹ 
    EIf cond thn els ⟶ EIf cond' thn els" 

inductive_cases
  red_var_inv[elim!]: "EVar x ⟶ e" and
  red_int_inv[elim!]: "ENat n ⟶ e" and
  red_lam_inv[elim!]: "ELam x e ⟶ e'" and
  red_app_inv[elim!]: "EApp e1 e2 ⟶ e'"
  
inductive multi_step :: "exp ⇒ exp ⇒ bool" (infix ‹⟶*› 55) where
  ms_nil[intro!]: "e ⟶* e" |
  ms_cons[intro!]: "⟦ e1 ⟶ e2; e2 ⟶* e3 ⟧ ⟹ e1 ⟶* e3"

definition diverge :: "exp ⇒ bool" where
  "diverge e ≡ (∀ e'. e ⟶* e' ⟶ (∃ e''. e' ⟶ e''))"
  
definition stuck :: "exp ⇒ bool" where
  "stuck e ≡ ¬ (∃ e'. e ⟶ e')" 
declare stuck_def[simp]

definition goes_wrong :: "exp ⇒ bool" where
  "goes_wrong e ≡ ∃ e'. e ⟶* e' ∧ stuck e' ∧ ¬ isval e'"
declare goes_wrong_def[simp]

datatype obs = ONat nat | OFun | OBad

fun observe :: "exp ⇒ obs ⇒ bool" where
  "observe (ENat n) (ONat n') = (n = n')" |
  "observe (ELam x e) OFun = True" |
  "observe e ob = False" 

definition run :: "exp ⇒ obs ⇒ bool" (infix ‹⇓› 52) where
  "run e ob ≡ ((∃ v. e ⟶* v ∧ observe v ob)
              ∨ ((diverge e ∨ goes_wrong e) ∧ ob = OBad))"

lemma val_stuck: fixes e::exp assumes val_e: "isval e" shows "stuck e"
proof (rule classical)
  assume "¬ stuck e"
  from this obtain e' where red: "e ⟶ e'" by auto 
  from val_e red have "False" by (case_tac e) auto
  from this show ?thesis ..
qed

lemma subst_fv_aux: assumes fvv: "FV v = {}" shows "FV (subst x v e) ⊆ FV e - {x}"
  using fvv
proof (induction e arbitrary: x v rule: exp.induct)
  case (EVar x)
  then show ?case by auto
next
  case (ENat x)
  then show ?case by auto
next
  case (ELam y e)
  then show ?case by (cases "x = y") auto
qed (simp,blast)+
    
lemma subst_fv:  assumes fv_e: "FV e ⊆ {x}" and fv_v: "FV v = {}" 
  shows "FV (subst x v e) = {}"
  using fv_e fv_v subst_fv_aux by blast
    
lemma red_pres_fv:  fixes e::exp assumes red: "e ⟶ e'" and fv: "FV e = {}" shows "FV e' = {}"
  using red fv
proof (induction rule: reduce.induct)
  case (beta v x e)
  then show ?case using subst_fv by auto
qed fastforce+
    
lemma reduction_pres_fv: fixes e::exp assumes r: "e ⟶* e'" and fv: "FV e = {}" shows "FV e' = {}"
  using r fv
proof (induction)
  case (ms_nil e)
  then show ?case by blast
next
  case (ms_cons e1 e2 e3)
  then show ?case using red_pres_fv by auto
qed

end