# Theory BigStepLam

```section "Big-step semantics of CBV lambda calculus"

theory BigStepLam
imports Lambda SmallStepLam
begin

datatype bval
= BNat nat
| BClos name exp "(name × bval) list"

type_synonym benv = "(name × bval) list"

inductive eval :: "benv ⇒ exp ⇒ bval ⇒ bool" ("_ ⊢ _ ⇓ _" [50,50,50] 51) where
eval_nat[intro!]: "ρ ⊢ ENat n ⇓ BNat n" |
eval_var[intro!]: "lookup ρ x = Some v ⟹ ρ ⊢ EVar x ⇓ v" |
eval_lam[intro!]: "ρ ⊢ ELam x e ⇓ BClos x e ρ" |
eval_app[intro!]: "⟦ ρ ⊢ e1 ⇓ BClos x e ρ'; ρ ⊢ e2 ⇓ arg;
(x,arg)#ρ' ⊢ e ⇓ v ⟧ ⟹
ρ ⊢ EApp e1 e2 ⇓ v" |
eval_prim[intro!]: "⟦ ρ ⊢ e1 ⇓ BNat n1; ρ ⊢ e2 ⇓ BNat n2 ; n3 = f n1 n2⟧ ⟹
ρ ⊢ EPrim f e1 e2 ⇓ BNat n3" |
eval_if0[intro!]: "⟦ ρ ⊢ e1 ⇓ BNat 0; ρ ⊢ e3 ⇓ v3 ⟧ ⟹
ρ ⊢ EIf e1 e2 e3 ⇓ v3" |
eval_if1[intro!]: "⟦ ρ ⊢ e1 ⇓ BNat n; n ≠ 0; ρ ⊢ e2 ⇓ v2 ⟧ ⟹
ρ ⊢ EIf e1 e2 e3 ⇓ v2"

inductive_cases
eval_nat_inv[elim!]: "ρ ⊢ ENat n ⇓ v" and
eval_var_inv[elim!]: "ρ ⊢ EVar x ⇓ v" and
eval_lam_inv[elim!]: "ρ ⊢ ELam x e ⇓ v" and
eval_app_inv[elim!]: "ρ ⊢ EApp e1 e2 ⇓ v" and
eval_prim_inv[elim!]: "ρ ⊢ EPrim f e1 e2 ⇓ v" and
eval_if_inv[elim!]: "ρ ⊢ EIf e1 e2 e3 ⇓ v"

subsection "Big-step semantics is sound wrt. small-step semantics"

type_synonym env = "(name × exp) list"

fun psubst :: "env ⇒ exp ⇒ exp" where
"psubst ρ (ENat n) = ENat n" |
"psubst ρ (EVar x) =
(case lookup ρ x of
None ⇒ EVar x
| Some v ⇒ v)" |
"psubst ρ (ELam x e) = ELam x (psubst ((x,EVar x)#ρ) e)" |
"psubst ρ (EApp e1 e2) = EApp (psubst ρ e1) (psubst ρ e2)" |
"psubst ρ (EPrim f e1 e2) = EPrim f (psubst ρ e1) (psubst ρ e2)" |
"psubst ρ (EIf e1 e2 e3) = EIf (psubst ρ e1) (psubst ρ e2) (psubst ρ e3)"

inductive bs_val :: "bval ⇒ exp ⇒ bool" and
bs_env :: "benv ⇒ env ⇒ bool" where
bs_nat[intro!]: "bs_val (BNat n) (ENat n)" |
bs_clos[intro!]: "⟦ bs_env ρ ρ'; FV (ELam x (psubst ((x,EVar x)#ρ') e)) = {} ⟧ ⟹
bs_val (BClos x e ρ) (ELam x (psubst ((x,EVar x)#ρ') e))" |
bs_nil[intro!]: "bs_env [] []" |
bs_cons[intro!]: "⟦ bs_val w v; bs_env ρ ρ' ⟧ ⟹ bs_env ((x,w)#ρ) ((x,v)#ρ')"

inductive_cases bs_env_inv1[elim!]: "bs_env ((x, w) # ρ) ρ'" and
bs_clos_inv[elim!]: "bs_val (BClos x e ρ'') v1" and
bs_nat_inv[elim!]: "bs_val (BNat n) v"

lemma bs_val_is_val[intro!]: "bs_val w v ⟹ is_val v"
by (cases w) auto

lemma lookup_bs_env: "⟦ bs_env ρ ρ'; lookup ρ x = Some w ⟧ ⟹
∃ v. lookup ρ' x = Some v ∧ bs_val w v"
by (induction ρ arbitrary: ρ' x w) auto

lemma app_red_cong1: "e1 ⟶* e1' ⟹ EApp e1 e2 ⟶* EApp e1' e2"
by (induction rule: multi_step.induct) blast+

lemma app_red_cong2: "e2 ⟶* e2' ⟹ EApp e1 e2 ⟶* EApp e1 e2'"
by (induction rule: multi_step.induct) blast+

lemma prim_red_cong1: "e1 ⟶* e1' ⟹ EPrim f e1 e2 ⟶* EPrim f e1' e2"
by (induction rule: multi_step.induct) blast+

lemma prim_red_cong2: "e2 ⟶* e2' ⟹ EPrim f e1 e2 ⟶* EPrim f e1 e2'"
by (induction rule: multi_step.induct) blast+

lemma if_red_cong1: "e1 ⟶* e1' ⟹ EIf e1 e2 e3 ⟶* EIf e1' e2 e3"
by (induction rule: multi_step.induct) blast+

lemma multi_step_trans: "⟦ e1 ⟶* e2; e2 ⟶* e3 ⟧ ⟹ e1 ⟶* e3"
proof (induction arbitrary: e3 rule: multi_step.induct)
case (ms_cons e1 e2 e3 e3')
then have "e2 ⟶* e3'" by auto
with ms_cons(1) show ?case by blast
qed blast

lemma subst_id_fv: "x ∉ FV e ⟹ subst x v e = e"
by (induction e arbitrary: x v) auto

definition sdom :: "env ⇒ name set" where
"sdom ρ ≡ {x. ∃ v. lookup ρ x = Some v ∧ v ≠ EVar x }"

definition closed_env :: "env ⇒ bool" where
"closed_env ρ ≡ (∀ x v. x ∈ sdom ρ ⟶ lookup ρ x = Some v ⟶ FV v = {})"

definition equiv_env :: "env ⇒ env ⇒ bool" where
"equiv_env ρ ρ' ≡ (sdom ρ = sdom ρ' ∧ (∀ x. x ∈ sdom ρ ⟶ lookup ρ x = lookup ρ' x))"

lemma sdom_cons_xx[simp]: "sdom ((x,EVar x)#ρ) = sdom ρ - {x}"
unfolding sdom_def by auto

lemma sdom_cons_v[simp]: "FV v = {} ⟹ sdom ((x,v)#ρ) = insert x (sdom ρ)"
unfolding sdom_def by auto

lemma lookup_some_in_dom: "⟦ lookup ρ x = Some v; v ≠ EVar x ⟧ ⟹ x ∈ sdom ρ"
proof (induction ρ)
case (Cons b ρ)
show ?case
proof (cases b)
case (Pair y v')
with Cons show ?thesis unfolding sdom_def by auto
qed
qed auto

lemma lookup_none_notin_dom: "lookup ρ x = None ⟹ x ∉ sdom ρ"
proof (induction ρ)
case (Cons b ρ)
show ?case
proof (cases b)
case (Pair y v)
with Cons show ?thesis unfolding sdom_def by auto
qed
qed (auto simp: sdom_def)

lemma psubst_change: "equiv_env ρ ρ' ⟹ psubst ρ e = psubst ρ' e"
proof (induction e arbitrary: ρ ρ')
case (EVar x)
show ?case
proof (cases "lookup ρ x")
case None from None have lx: "lookup ρ x = None" by simp
show ?thesis
proof (cases "lookup ρ' x")
case None
with EVar lx show ?thesis by auto
next
case (Some v)
from EVar lx Some have "x ∉ sdom ρ'" unfolding equiv_env_def by auto
with lx Some show ?thesis unfolding sdom_def by simp
qed
next
case (Some v) from Some have lx: "lookup ρ x = Some v" by simp
show ?thesis
proof (cases "lookup ρ' x")
case None
from EVar lx None have "x ∉ sdom ρ" unfolding equiv_env_def by auto
with None Some show ?thesis unfolding sdom_def by simp
next
case (Some v')
from EVar Some lx show ?thesis by (simp add: equiv_env_def sdom_def) force
qed
qed
next
case (ELam x' e)
from ELam(2) have "equiv_env ((x',EVar x')#ρ) ((x',EVar x')#ρ')" by (simp add: equiv_env_def)
with ELam show ?case by (simp add: equiv_env_def)
qed fastforce+

lemma subst_psubst: "⟦ closed_env ρ; FV v = {} ⟧ ⟹
subst x v (psubst ((x, EVar x) # ρ) e) = psubst ((x, v) # ρ) e"
proof (induction e arbitrary: x v ρ)
case (EVar x x' v ρ)
show ?case
proof (cases "x = x'")
case True
then show ?thesis by force
next
case False from False have xxp: "x ≠ x'" by simp
show ?thesis
proof (cases "lookup ρ x")
case None
then show ?thesis by auto
next
case (Some v')
show ?thesis
proof (cases "v' = EVar x")
case True
with Some show ?thesis by auto
next
case False
from False Some have xdom: "x ∈ sdom ρ" using lookup_some_in_dom by simp
from this EVar Some have "FV v' = {}" using closed_env_def by blast
from this Some show ?thesis using subst_id_fv by auto
qed
qed
qed
next
case (ELam x' e)
show ?case
proof (cases "x = x'")
case True
then show ?thesis apply simp apply (rule psubst_change)
using equiv_env_def sdom_def by auto
next
case False
then show ?thesis apply simp
proof -
assume x_xp: "x ≠ x'"
let ?r = "(x',EVar x') # ρ"
from ELam have IHprem: "closed_env ((x', EVar x') # ρ)" using closed_env_def by auto
have "psubst ((x',EVar x')#(x, EVar x)#ρ) e = psubst ((x,EVar x)#(x',EVar x') # ρ) e"
apply (rule psubst_change) using x_xp equiv_env_def by auto
from this have "subst x v (psubst ((x', EVar x') # (x, EVar x) # ρ) e)
= subst x v (psubst ((x,EVar x)#(x',EVar x') # ρ) e)" by simp
also with ELam IHprem have "... = psubst ((x,v)#(x',EVar x')#ρ) e"
using ELam(1)[of "(x',EVar x')#ρ" v x] by simp
also have "... = psubst ((x',EVar x')#(x,v)#ρ) e"
apply (rule psubst_change) using x_xp equiv_env_def sdom_def by auto
finally show "subst x v (psubst ((x', EVar x') # (x, EVar x) # ρ) e)
= psubst ((x', EVar x') # (x,v) # ρ) e" .
qed
qed
qed fastforce+

inductive_cases bsenv_nil[elim!]: "bs_env [] ρ'"

lemma bs_env_dom: "bs_env ρ ρ' ⟹ set (map fst ρ) = sdom ρ'"
proof (induction ρ arbitrary: ρ')
case Nil
then show ?case by (force simp: sdom_def)
next
case (Cons b ρ)
then show ?case
proof (cases b)
case (Pair x v')
with Cons show ?thesis by (cases v') force+
qed
qed

lemma closed_env_cons[intro!]: "FV v = {} ⟹ closed_env ρ'' ⟹ closed_env ((a, v) # ρ'')"

lemma bs_env_closed: "bs_env ρ ρ' ⟹ closed_env ρ'"
proof (induction ρ arbitrary: ρ')
case Nil
then show ?case by (force simp: closed_env_def)
next
case (Cons b ρ)
from Cons obtain x v v' ρ'' where b: "b = (x,v)" and rp: "ρ' = (x,v')#ρ''"
and vvp: "bs_val v v'" and r_rpp: "bs_env ρ ρ''" by (cases b) blast
from vvp have "is_val v'" by blast
from this have fv_vp: "FV v' = {}" by auto
from Cons r_rpp have "closed_env ρ''" by blast
from this rp fv_vp show ?case by blast
qed

lemma psubst_fv: "closed_env ρ ⟹ FV (psubst ρ e) = FV e - sdom ρ"
proof (induction e arbitrary: ρ)
case (EVar x)
then show ?case
apply (cases "x ∈ sdom ρ")
apply (erule_tac x=x in allE)
apply (erule impE) apply blast apply (simp add: sdom_def) apply clarify
apply force
apply (cases "lookup ρ x")
apply force
apply force
done
next
case (ELam x e)
from ELam have "closed_env ((x, EVar x) # ρ)" by (simp add: closed_env_def sdom_def)
from this ELam show ?case by auto
qed fastforce+

lemma big_small_step:
assumes ev: "ρ ⊢ e ⇓ w" and r_rp: "bs_env ρ ρ'" and fv_e: "FV e ⊆ set (map fst ρ)"
shows "∃ v. psubst ρ' e ⟶* v ∧ is_val v ∧ bs_val w v"
using ev r_rp fv_e
proof (induction arbitrary: ρ' rule: eval.induct)
case (eval_nat ρ n ρ')
then show ?case by (rule_tac x="ENat n" in exI) auto
next
case (eval_var ρ x w ρ')
from eval_var obtain v where lx: "lookup ρ' x = Some v" and
vv: "is_val v" and w_v: "bs_val w v" using lookup_bs_env by blast
from lx vv w_v show ?case by (rule_tac x=v in exI) auto
next
case (eval_lam ρ x e ρ')
from eval_lam(1) have dom_eq: "set (map fst ρ) = sdom ρ'" using bs_env_dom by blast
from eval_lam(1) have "closed_env ((x,EVar x)#ρ')" using bs_env_closed closed_env_def by auto
from this psubst_fv have "FV (psubst ((x,EVar x)#ρ') e) = FV e - sdom ((x,EVar x)#ρ')" by blast
from this eval_lam(2) dom_eq
have fv_lam: "FV (ELam x (psubst ((x,EVar x)#ρ') e)) = {}" by auto
from fv_lam eval_lam have 1: "bs_val (BClos x e ρ) (ELam x (psubst ((x, EVar x) # ρ') e))" by auto
from this eval_lam fv_lam show ?case
by (rule_tac x="ELam x (psubst ((x,EVar x)#ρ') e)" in exI) auto
next
case (eval_app ρ e1 x e ρ' e2 arg v  ρ'')
from eval_app(8) have "FV e1 ⊆ set (map fst ρ)" by auto
from this eval_app(7) eval_app(4)[of ρ''] obtain v1 where e1_v1: "psubst ρ'' e1 ⟶* v1" and
vv1: "is_val v1" and clos_v1: "bs_val (BClos x e ρ') v1" by (simp, blast)
from eval_app(8) have "FV e2 ⊆ set (map fst ρ)" by auto
from this eval_app(5) eval_app(7) obtain v2 where e2_v2: "psubst ρ'' e2 ⟶* v2" and
vv2: "is_val v2" and arg_v2: "bs_val arg v2" by blast
from vv2 have fv_v2: "FV v2 = {}" by auto
from clos_v1 obtain ρ2 where rpp_r2: "bs_env ρ' ρ2" and fv_v1: "FV v1 = {}" and
v1_lam: "v1 = ELam x (psubst ((x,EVar x)#ρ2) e)" by auto
let ?r = "((x,v2) # ρ2)"
from rpp_r2 have cr2: "closed_env ρ2" using bs_env_closed by auto
from this have "closed_env ((x,EVar x)#ρ2)"  using  closed_env_def sdom_def by auto
from this have fve: "FV (psubst ((x,EVar x)#ρ2) e) = FV e - sdom ((x,EVar x)#ρ2)"
using psubst_fv[of "(x,EVar x)#ρ2"] by blast
let ?r2 = "((x, arg) # ρ')"
from rpp_r2 arg_v2 vv2 have rr: "bs_env ?r2 ?r" by auto
from rr bs_env_dom have dr2_dr: "set (map fst ?r2) = sdom ?r" by blast
from fve dr2_dr fv_v1 v1_lam fv_v2 have "FV e ⊆ set (map fst ((x, arg) # ρ'))" by auto
from this rr eval_app(6) obtain v3 where e_v3: "psubst ?r e ⟶* v3" and
vv3: "isval v3" and v_v3: "bs_val v v3" by (simp, blast)
from e1_v1 have 1: "EApp (psubst ρ'' e1) (psubst ρ'' e2) ⟶* EApp v1 (psubst ρ'' e2)"
by (rule app_red_cong1)
from e2_v2 have 2: "EApp v1 (psubst ρ'' e2) ⟶* EApp v1 v2"
by (rule app_red_cong2)
from vv2 fv_v2 have vv2b: "is_val v2" by auto
let ?body = "psubst ((x,EVar x)#ρ2) e"
from v1_lam vv2b have 3: "EApp (ELam x ?body) v2 ⟶
subst x v2 (psubst ((x,EVar x)#ρ2) e)" using beta[of v2 x "?body"] by simp
have 4: "subst x v2 (psubst ((x,EVar x)#ρ2) e) = psubst ?r e"
apply (rule subst_psubst) using fv_v2 cr2 by auto
have 4: "subst x v2 (psubst ((x,EVar x)#ρ2) e) = psubst ?r e"
apply (rule subst_psubst) using fv_v2 cr2 by auto
from 1 2 have 5: "psubst ρ'' (EApp e1 e2) ⟶* EApp v1 v2" apply simp
by (rule multi_step_trans) auto
from 5 3 4 v1_lam have 6: "psubst ρ'' (EApp e1 e2) ⟶* psubst ?r e"
apply simp apply (rule multi_step_trans) apply assumption apply blast done
from 6 e_v3 have 7: "psubst ρ'' (EApp e1 e2) ⟶* v3" by (rule multi_step_trans)
from 7 vv3 v_v3 show ?case by blast
next
case (eval_prim ρ e1 n1 e2 n2 n3 f ρ')
from eval_prim(7) have "FV e1 ⊆ set (map fst ρ)" by auto
from this eval_prim obtain v1 where e1_v1: "psubst ρ' e1 ⟶* v1" and
n1_v1: "bs_val (BNat n1) v1" by blast
from n1_v1 have v1: "v1 = ENat n1" by blast

from eval_prim(7) have "FV e2 ⊆ set (map fst ρ)" by auto
from this eval_prim obtain v2 where e2_v2: "psubst ρ' e2 ⟶* v2" and
n2_v2: "bs_val (BNat n2) v2" by blast
from n2_v2 have v2: "v2 = ENat n2" by blast

from e1_v1 have 1: "EPrim f (psubst ρ' e1) (psubst ρ' e2) ⟶* EPrim f v1 (psubst ρ' e2)"
by (rule prim_red_cong1)
from e2_v2 have 2: "EPrim f v1 (psubst ρ' e2) ⟶* EPrim f v1 v2"
by (rule prim_red_cong2)
from v1 v2 have 3: "EPrim f v1 v2 ⟶ ENat (f n1 n2)" by auto
from 1 2 have 5: "psubst ρ' (EPrim f e1 e2) ⟶* EPrim f v1 v2" apply simp
apply (rule multi_step_trans) apply auto done
from 5 3  have 6: "psubst ρ' (EPrim f e1 e2) ⟶* ENat (f n1 n2)" apply simp
apply (rule multi_step_trans) apply assumption apply blast done
from this eval_prim(3) show ?case apply (rule_tac x="ENat (f n1 n2)" in exI) by auto
next
case (eval_if0 ρ e1 e3 v3 e2 ρ')
from eval_if0(6) have "FV e1 ⊆ set (map fst ρ)" by auto
from this eval_if0 obtain v1 where e1_v1: "psubst ρ' e1 ⟶* v1" and
n1_v1: "bs_val (BNat 0) v1" by blast
from n1_v1 have v1: "v1 = ENat 0" by blast
from eval_if0(6) have "FV e3 ⊆ set (map fst ρ)" by auto
from this eval_if0 obtain v3' where e3_v3: "psubst ρ' e3 ⟶* v3'" and
v3_v3: "bs_val v3 v3'" by blast

from e1_v1 have 1: "EIf (psubst ρ' e1) (psubst ρ' e2) (psubst ρ' e3)
⟶* EIf v1 (psubst ρ' e2) (psubst ρ' e3)" by (rule if_red_cong1)
from v1 have 3: "EIf v1 (psubst ρ' e2) (psubst ρ' e3) ⟶ (psubst ρ' e3)" by auto
from 1 3 have 5: "psubst ρ' (EIf e1 e2 e3) ⟶* psubst ρ' e3" apply simp
apply (rule multi_step_trans) apply assumption apply blast done
from 5 e3_v3 have 6: "psubst ρ' (EIf e1 e2 e3) ⟶* v3'"
apply (rule multi_step_trans) done
from 6 v3_v3 show ?case by blast
next
case (eval_if1 ρ e1 n e2 v2 e3 ρ')
from eval_if1 have "FV e1 ⊆ set (map fst ρ)" by auto
from this eval_if1 obtain v1 where e1_v1: "psubst ρ' e1 ⟶* v1" and
n1_v1: "bs_val (BNat n) v1" and nz: "n ≠ 0" apply auto apply blast done
from n1_v1 have v1: "v1 = ENat n" by blast
from eval_if1 have "FV e2 ⊆ set (map fst ρ)" by auto
from this eval_if1 obtain v2' where e2_v2: "psubst ρ' e2 ⟶* v2'" and
v2_v2: "bs_val v2 v2'" by blast
from e1_v1 have 1: "EIf (psubst ρ' e1) (psubst ρ' e2) (psubst ρ' e3)
⟶* EIf v1 (psubst ρ' e2) (psubst ρ' e3)" by (rule if_red_cong1)
from v1 nz have 3: "EIf v1 (psubst ρ' e2) (psubst ρ' e3) ⟶ (psubst ρ' e2)" by auto
from 1 3 have 5: "psubst ρ' (EIf e1 e2 e3) ⟶* psubst ρ' e2" apply simp
apply (rule multi_step_trans) apply assumption apply blast done
from 5 e2_v2 have 6: "psubst ρ' (EIf e1 e2 e3) ⟶* v2'"
by (rule multi_step_trans)
from 6 v2_v2 show ?case by blast
qed

lemma psubst_id: "FV e ∩ sdom ρ = {} ⟹ psubst ρ e = e"
proof (induction e arbitrary: ρ)
case (EVar x)
then show ?case by (cases "lookup ρ x") (auto simp: sdom_def)
next
case (ENat x ρ)
from ENat have "sdom ((x,EVar x)#ρ) = sdom ρ - {x}" by simp
with ENat show ?case by auto
next
case (ELam x e)
from ELam have "FV e ∩ sdom ((x,EVar x)#ρ) = {}" by auto
with ELam show ?case by auto
qed fastforce+

fun bs_observe :: "bval ⇒ obs ⇒ bool" where
"bs_observe (BNat n) (ONat n') = (n = n')" |
"bs_observe (BClos x e ρ) OFun = True" |
"bs_observe e ob = False"

theorem sound_wrt_small_step:
assumes e_v: "[] ⊢ e ⇓ v" and fv_e: "FV e = {}"
shows "∃ v' ob. e ⟶* v' ∧ isval v' ∧ observe v' ob
∧ bs_observe v ob"
proof -
have 1: "bs_env [] []" by blast
from fv_e have 2: "FV e ⊆ set (map fst [])" by simp
from e_v 1 2 big_small_step obtain v' where 3: "psubst [] e ⟶* v'" and 4: "is_val v'" and
5: "bs_val v v'" by blast
have "psubst [] e = e" using psubst_id sdom_def apply auto done
from this 3 4 5 show ?thesis apply (rule_tac x=v' in exI) apply simp
apply (case_tac v)
apply simp apply clarify apply simp
apply (rename_tac n) apply (rule_tac x="ONat n" in exI) apply force
apply (rule_tac x=OFun in exI) apply force done
qed

subsection "Big-step semantics is deterministic"

theorem big_step_fun:
assumes ev: "ρ ⊢ e ⇓ v" and evp: "ρ ⊢ e ⇓ v'" shows "v = v'"
using ev evp
proof (induction arbitrary: v')
case (eval_app ρ e1 x e ρ' e2 arg v)
from eval_app(7) obtain x' e' ρ'' arg' where e1_cl: "ρ ⊢ e1 ⇓ BClos x' e' ρ''" and
e2_argp: "ρ ⊢ e2 ⇓ arg'" and e_vp: "(x', arg') # ρ'' ⊢ e' ⇓ v'" by blast
from eval_app(4) e1_cl have 1: "BClos x e ρ' = BClos x' e' ρ''" by simp
from eval_app(5) e2_argp have 2: "arg = arg'" by simp
from eval_app(6) e_vp 1 2 show ?case by simp
next
case (eval_if0 ρ e1 e3 v3 e2)
from eval_if0(5)
show ?case
proof (rule eval_if_inv)
assume "ρ ⊢ e3 ⇓ v'" with eval_if0(4) show ?thesis by simp
next
fix n assume "ρ ⊢ e1 ⇓ BNat n" and nz: "n > 0"
with eval_if0(3) have "False" by auto thus ?thesis ..
qed
next
case (eval_if1 ρ e1 n e2 v2 e3)
then show ?case by blast
qed fastforce+

end
```