Theory SmallStepLam

section ‹Small-step semantics of CBV lambda calculus›

theory SmallStepLam
  imports Lambda
  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)"

  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" 

  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 ..

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
  case (ENat x)
  then show ?case by auto
  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
  case (ms_cons e1 e2 e3)
  then show ?case using red_pres_fv by auto