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) # ρ'')"
  by (simp add: closed_env_def sdom_def)   

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 (simp add: closed_env_def)
    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 (simp add: sdom_def)
    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