# 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
```