# Theory DenotSoundFSet

```section "Soundness of the declarative semantics wrt. operational"

theory DenotSoundFSet
imports SmallStepLam BigStepLam ChangeEnv
begin

subsection "Substitution preserves denotation"

lemma subst_app: "subst x v (EApp e1 e2) = EApp (subst x v e1) (subst x v e2)"
by auto

lemma subst_prim: "subst x v (EPrim f e1 e2) = EPrim f (subst x v e1) (subst x v e2)"
by auto

lemma subst_lam_eq: "subst x v (ELam x e) = ELam x e" by auto

lemma subst_lam_neq: "y ≠ x ⟹ subst x v (ELam y e) = ELam y (subst x v e)" by simp

lemma subst_if: "subst x v (EIf e1 e2 e3) = EIf (subst x v e1) (subst x v e2) (subst x v e3)"
by auto

lemma substitution:
fixes Γ::env and A::val
assumes wte: "B ∈ E e Γ'" and wtv: "A ∈ E v []"
and gp: "Γ' ≈ (x,A)#Γ" and v: "is_val v"
shows "B ∈ E (subst x v e) Γ"
using wte wtv gp v
proof (induction arbitrary: v A B Γ x rule: E.induct)
case (1 n ρ)
then show ?case by auto
next
case (2 x ρ v A B Γ x')
then show ?case
apply (simp only: env_eq_def)
apply (cases "x = x'")
apply simp apply clarify
apply (rule env_strengthen)
apply (rule e_sub)
apply auto
done
next
case (3 x e ρ v A B Γ x')
then show ?case
apply (case_tac "x' = x") apply (simp only: subst_lam_eq)
apply (rule env_strengthen) apply assumption apply (simp add: env_eq_def)
apply (simp only: subst_lam_neq) apply (erule e_lam_elim)
apply (rule e_lam_intro)
apply assumption apply clarify apply (erule_tac x=v1 in allE) apply (erule_tac x=v2 in allE)
apply clarify
apply (subgoal_tac "(x,v1)#ρ ≈ (x',A)#(x,v1)#Γ")
prefer 2 apply (simp add: env_eq_def)
apply blast
done
next
case (4 e1 e2 ρ)
then show ?case
apply (simp only: subst_app)
apply (erule e_app_elim)
apply (rule e_app_intro)
apply auto
done
next
case (5 f e1 e2 ρ)
then show ?case
apply (simp only: subst_prim) apply (erule e_prim_elim) apply simp
apply (rule_tac x=n1 in exI) apply (rule conjI)
apply force
apply (rule_tac x=n2 in exI)
apply auto
done
next
case (6 e1 e2 e3 ρ)
then show ?case
apply (simp only: subst_if) apply (erule e_if_elim) apply (rename_tac n)
apply simp
apply (case_tac "n = 0") apply (rule_tac x=0 in exI)
apply force
apply (rule_tac x=n in exI) apply simp done
qed

subsection "Reduction preserves denotation"

lemma subject_reduction: fixes e::exp assumes v: "v ∈ E e ρ" and r: "e ⟶ e'" shows "v ∈ E e' ρ"
using r v
proof (induction arbitrary: v ρ rule: reduce.induct)
case (beta v x e v' ρ)
then show ?case apply (simp only: is_val_def)
apply (erule e_app_elim) apply (erule e_lam_elim) apply clarify
apply (rename_tac f v2 v2' v3' f')
apply (erule_tac x=v2' in allE) apply (erule_tac x=v3' in allE) apply clarify
apply (subgoal_tac "v3' ∈ E (subst x v e) ρ") prefer 2 apply (rule substitution)
apply (subgoal_tac "v3' ∈ E e ((x,v2)#ρ)") prefer 2 apply (rule raise_env)
apply assumption apply (simp add: env_le_def) prefer 2 apply (rule env_strengthen)
apply assumption apply force prefer 2 apply (subgoal_tac "(x,v2)#ρ ≈ (x,v2)#ρ") prefer 2
apply (simp add: env_eq_def) apply assumption apply assumption
apply simp
apply simp
apply (rule e_sub)
apply assumption
apply (rule val_le_trans)
apply blast
apply force
done
qed force+

theorem preservation: assumes v: "v ∈ E e ρ" and rr: "e ⟶* e'" shows "v ∈ E e' ρ"
using rr v subject_reduction by (induction arbitrary: ρ v) auto

lemma canonical_nat: assumes v: "VNat n ∈ E v ρ" and vv: "isval v" shows "v = ENat n"
using v vv by (cases v) auto

lemma canonical_fun: assumes v: "VFun f ∈ E v ρ" and vv: "isval v" shows "∃ x e. v = ELam x e"
using v vv by (cases v) auto

subsection "Progress"

theorem progress: assumes v: "v ∈ E e ρ" and r: "ρ = []" and fve: "FV e = {}"
shows "is_val e ∨ (∃ e'. e ⟶ e')"
using v r fve
proof (induction arbitrary: v rule: E.induct)
case (4 e1 e2 ρ)
show ?case
apply (rule e_app_elim) using 4(3) apply assumption
apply (cases "is_val e1")
apply (cases "is_val e2")
apply (frule canonical_fun) apply force apply (erule exE)+ apply simp apply (rule disjI2)
apply (rename_tac x e)
apply (rule_tac x="subst x e2 e" in exI)
apply (rule beta) apply simp
using 4 apply simp
apply blast
using 4 apply simp
apply blast done
next
case (5 f e1 e2 ρ)
show ?case
apply (rule e_prim_elim) using 5(3) apply assumption
using 5 apply (case_tac "isval e1")
apply (case_tac "isval e2")
apply (subgoal_tac "e1 = ENat n1") prefer 2 using canonical_nat apply blast
apply (subgoal_tac "e2 = ENat n2") prefer 2 using canonical_nat apply blast
apply force
apply force
apply force done
next
case (6 e1 e2 e3 ρ)
show ?case
apply (rule e_if_elim)
using 6(4) apply assumption
apply (cases "isval e1")
apply (rename_tac n)
apply (subgoal_tac "e1 = ENat n") prefer 2 apply (rule canonical_nat) apply blast apply blast
apply (rule disjI2) apply (case_tac "n = 0") apply force apply force
apply (rule disjI2)
using 6 apply (subgoal_tac "∃ e1'. e1 ⟶ e1'") prefer 2 apply force
apply clarify apply (rename_tac e1')
apply (rule_tac x="EIf e1' e2 e3" in exI)
apply (rule if_cond) apply assumption
done
qed auto

subsection "Logical relation between values and big-step values"

fun good_entry :: "name ⇒ exp ⇒ benv ⇒ (val × bval set) × (val × bval set) ⇒ bool ⇒ bool" where
"good_entry x e ρ ((v1,g1),(v2,g2)) r = ((∀ v ∈ g1. ∃ v'. (x,v)#ρ ⊢ e ⇓ v' ∧ v' ∈ g2) ∧ r)"

primrec good :: "val ⇒ bval set" where
Gnat: "good (VNat n) = { BNat n }" |
Gfun: "good (VFun f) = { vc. ∃ x e ρ. vc = BClos x e ρ
∧ (ffold (good_entry x e ρ) True (fimage (map_prod (λv. (v,good v)) (λv. (v,good v))) f)) }"

inductive good_env :: "benv ⇒ env ⇒ bool" where
genv_nil[intro!]: "good_env [] []" |
genv_cons[intro!]: "⟦ v ∈ good v'; good_env ρ ρ' ⟧ ⟹ good_env ((x,v)#ρ) ((x,v')#ρ')"

inductive_cases
genv_any_nil_inv: "good_env ρ []" and
genv_any_cons_inv: "good_env ρ (b#ρ')"

lemma lookup_good:
assumes l: "lookup ρ' x = Some A" and EE: "good_env ρ ρ'"
shows "∃ v. lookup ρ x = Some v ∧ v ∈ good A"
using l EE
proof (induction ρ' arbitrary: x A ρ)
case Nil
show ?case apply (rule genv_any_nil_inv) using Nil by auto
next
case (Cons a ρ')
show ?case
apply (rule genv_any_cons_inv)
using Cons apply force
apply (rename_tac x') apply clarify
using Cons apply (case_tac "x = x'")
apply force
apply force
done
qed

abbreviation good_prod :: "val × val ⇒ (val × bval set) × (val × bval set)" where
"good_prod ≡ map_prod (λv. (v,good v)) (λv. (v,good v))"

lemma good_prod_inj: "inj_on good_prod (fset A)"
unfolding inj_on_def apply auto done

definition good_fun :: "func ⇒ name ⇒ exp ⇒ benv ⇒ bool" where
"good_fun f x e ρ ≡ (ffold (good_entry x e ρ) True (fimage good_prod f))"

lemma good_fun_def2:
"good_fun f x e ρ = ffold (good_entry x e ρ ∘ good_prod) True f"
proof -
interpret ge: comp_fun_commute "(good_entry x e ρ) ∘ good_prod"
unfolding comp_fun_commute_def by auto
show "good_fun f x e ρ
= ffold ((good_entry x e ρ) ∘ good_prod) True f"
using good_prod_inj[of "f"] good_fun_def
ffold_fimage[of good_prod "f" "good_entry x e ρ" True] by auto
qed

lemma gfun_elim: "w ∈ good (VFun f) ⟹ ∃ x e ρ. w = BClos x e ρ ∧ good_fun f x e ρ"
using good_fun_def by auto

lemma gfun_mem_iff: "good_fun f x e ρ = (∀ v1 v2. (v1,v2) ∈ fset f ⟶
(∀ v ∈ good v1. ∃ v'. (x,v)#ρ ⊢ e ⇓ v' ∧ v' ∈ good v2))"
proof (induction f arbitrary: x e ρ)
case empty
interpret ge: comp_fun_commute "(good_entry x e ρ)"
unfolding comp_fun_commute_def by auto
from empty show ?case using good_fun_def2
by (simp add: comp_fun_commute.ffold_empty ge.comp_comp_fun_commute)
next
case (insert p f)
interpret ge: comp_fun_commute "(good_entry x e ρ) ∘ good_prod"
unfolding comp_fun_commute_def by auto
have "good_fun (finsert p f) x e ρ
= ffold ((good_entry x e ρ) ∘ good_prod) True (finsert p f)" by (simp add: good_fun_def2)
also from insert(1) have "... = ((good_entry x e ρ) ∘ good_prod) p
(ffold ((good_entry x e ρ) ∘ good_prod) True f)" by simp
finally have 1: "good_fun (finsert p f) x e ρ
= ((good_entry x e ρ) ∘ good_prod) p (ffold ((good_entry x e ρ) ∘ good_prod) True f)" .
show ?case
proof
assume 2: "good_fun (finsert p f) x e ρ"
show "∀v1 v2. (v1, v2) ∈ fset (finsert p f) ⟶
(∀v∈good v1. ∃v'. (x, v) # ρ ⊢ e ⇓ v' ∧ v' ∈ good v2)"
proof clarify
fix v1 v2 v assume 3: "(v1, v2) ∈ fset (finsert p f)" and 4: "v ∈ good v1"
from 3 have "(v1,v2) = p ∨ (v1,v2) ∈ fset f" by auto
from this show "∃v'. (x, v) # ρ ⊢ e ⇓ v' ∧ v' ∈ good v2"
proof
assume v12_p: "(v1,v2) = p"
from 1 v12_p[THEN sym] 2 4 show ?thesis by simp
next
assume v12_f: "(v1,v2) ∈ fset f"
from 1 2 have 5: "good_fun f x e ρ" apply simp
apply (cases "(good_prod p)") by (auto simp: good_fun_def2)
from v12_f 5 4 insert(2)[of x e ρ] show ?thesis by auto
qed
qed
next
assume 2: "∀v1 v2. (v1, v2) ∈ fset (finsert p f) ⟶
(∀v∈good v1. ∃v'. (x, v) # ρ ⊢ e ⇓ v' ∧ v' ∈ good v2)"
have 3: "good_entry x e ρ (good_prod p) True"
apply (cases p) apply simp apply clarify
proof -
fix v1 v2 v
assume p: "p = (v1,v2)" and v_v1: "v ∈ good v1"
from p have "(v1,v2) ∈ fset (finsert p f)" by simp
from this 2 v_v1 show "∃v'. (x, v) # ρ ⊢ e ⇓ v' ∧ v' ∈ good v2" by blast
qed
from insert(2) 2 have 4: "good_fun f x e ρ" by auto
have "(good_entry x e ρ ∘ good_prod) p
(ffold (good_entry x e ρ ∘ good_prod) True f)"
apply simp apply (cases "good_prod p")
apply (rename_tac a b c)
apply (case_tac a) apply simp
apply (rule conjI) prefer 2 using 4 good_fun_def2 apply force
using 3 apply force done
from this 1 show "good_fun (finsert p f) x e ρ"
unfolding good_fun_def by simp
qed
qed

lemma gfun_mem: "⟦ (v1,v2) ∈ fset f; good_fun f x e ρ ⟧
⟹ ∀ v ∈ good v1. ∃ v'. (x,v)#ρ ⊢ e ⇓ v' ∧ v' ∈ good v2"
using gfun_mem_iff by blast

lemma gfun_intro: "(∀ v1 v2.(v1,v2)∈fset f⟶(∀v∈good v1.∃ v'.(x,v)#ρ ⊢ e ⇓ v'∧v'∈good v2))
⟹ good_fun f x e ρ" using gfun_mem_iff[of f x e ρ] by simp

lemma sub_good: fixes v::val assumes wv: "w ∈ good v" and vp_v: "v' ⊑ v" shows "w ∈ good v'"
proof (cases v)
case (VNat n)
from this wv vp_v show ?thesis by auto
next
case (VFun t1)
from vp_v VFun obtain t2 where b: "v' = VFun t2" and t2_t1: "fset t2 ⊆ fset t1" by auto
from wv VFun obtain x e ρ where w: "w = BClos x e ρ" by auto
from w wv VFun have gt1: "good_fun t1 x e ρ" by (simp add: good_fun_def)
have gt2: "good_fun t2 x e ρ" apply (rule gfun_intro) apply clarify
proof -
fix v1 v2 w1
assume v12: "(v1,v2) ∈ fset t2" and w1_v1: "w1 ∈ good v1"
from v12 t2_t1 have v12_t1: "(v1,v2) ∈ fset t1" by blast
from gt1 v12_t1 w1_v1 show "∃v'. (x, w1) # ρ ⊢ e ⇓ v' ∧ v' ∈ good v2"
by (simp add: gfun_mem)
qed
from gt2 b w show ?thesis by (simp add: good_fun_def)
qed

subsection "Denotational semantics sound wrt. big-step"

lemma denot_terminates: assumes vp_e: "v' ∈ E e ρ'" and ge: "good_env ρ ρ'"
shows "∃ v. ρ ⊢ e ⇓ v ∧ v ∈ good v'"
using vp_e ge
proof (induction arbitrary: v' ρ rule: E.induct)
case (1 n ρ) ― ‹ENat›
then show ?case by auto
next ― ‹EVar›
case (2 x ρ v' ρ')
from 2 obtain v1 where lx_vpp: "lookup ρ x = Some v1" and vp_v1: "v' ⊑ v1" by auto
from lx_vpp 2(2) obtain v2 where lx: "lookup ρ' x = Some v2" and v2_v1: "v2 ∈ good v1"
using lookup_good[of ρ x v1 ρ'] by blast
from lx have x_v2: "ρ' ⊢ EVar x ⇓ v2" by auto
from v2_v1 vp_v1 have v2_vp: "v2 ∈ good v'" using sub_good by blast
from x_v2 v2_vp show ?case by blast
next ― ‹ELam›
case (3 x e ρ v' ρ')
have 1: "ρ' ⊢ ELam x e ⇓ BClos x e ρ'" by auto
have 2: "BClos x e ρ' ∈ good v'"
proof -
from 3(2) obtain t where vp: "v' = VFun t" and
body: "∀v1 v2. (v1, v2) ∈ fset t ⟶ v2 ∈ E e ((x, v1) # ρ)" by blast
have gt: "good_fun t x e ρ'" apply (rule gfun_intro) apply clarify
proof -
fix v1 v2 w1 assume v12_t: "(v1,v2) ∈ fset t" and w1_v1: "w1 ∈ good v1"
from v12_t body have v2_Ee: "v2 ∈ E e ((x, v1) # ρ)" by blast
from 3(3) w1_v1 have ge: "good_env ((x,w1)#ρ') ((x,v1)#ρ)" by auto
from v12_t v2_Ee ge 3(1)[of v1 v2 t v2]
show "∃v'. (x, w1) # ρ' ⊢ e ⇓ v' ∧ v' ∈ good v2" by blast
qed
from vp gt show ?thesis unfolding good_fun_def by simp
qed
from 1 2 show ?case by blast
next ― ‹EApp›
case (4 e1 e2 ρ v' ρ')
from 4(3) show ?case
proof
fix t v2 and v2'::val and v3' assume t_Ee1: "VFun t ∈ E e1 ρ" and v2_Ee2: "v2 ∈ E e2 ρ" and
v23_t: "(v2',v3') ∈ fset t" and v2p_v2: "v2' ⊑ v2" and vp_v3p: "v' ⊑ v3'"
from 4(1) t_Ee1 4(4) obtain w1 where e1_w1: "ρ' ⊢ e1 ⇓ w1" and
w1_t: "w1 ∈ good (VFun t)" by blast
from 4(2) v2_Ee2 4(4) obtain w2 where e2_w2: "ρ' ⊢ e2 ⇓ w2" and w2_v2: "w2 ∈ good v2" by blast
from w1_t obtain x e ρ1 where w1: "w1 = BClos x e ρ1" and gt: "good_fun t x e ρ1"
by (auto simp: good_fun_def)
from w2_v2 v2p_v2 have w2_v2p: "w2 ∈ good v2'" by (rule sub_good)
from v23_t gt w2_v2p obtain w3 where e_w3: "(x,w2)#ρ1 ⊢ e ⇓ w3" and w3_v3p: "w3 ∈ good v3'"
using gfun_mem[of v2' v3' t x e ρ1] by blast
from w3_v3p vp_v3p have w3_vp: "w3 ∈ good v'" by (rule sub_good)
from e1_w1 e2_w2 w1 e_w3 w3_vp show "∃v. ρ' ⊢ EApp e1 e2 ⇓ v ∧ v ∈ good v'" by blast
qed
next ― ‹EPrim›
case (5 f e1 e2 ρ v' ρ')
from 5(3) show ?case
proof
fix n1 n2 assume n1_e1: "VNat n1 ∈ E e1 ρ" and n2_e2: "VNat n2 ∈ E e2 ρ" and
vp: "v' = VNat (f n1 n2)"
from 5(1)[of "VNat n1" ρ'] n1_e1 5(4) have e1_w1: "ρ' ⊢ e1 ⇓ BNat n1" by auto
from 5(2)[of "VNat n2" ρ'] n2_e2 5(4) have e2_w2: "ρ' ⊢ e2 ⇓ BNat n2" by auto
from e1_w1 e2_w2 have 1: "ρ' ⊢ EPrim f e1 e2 ⇓ BNat (f n1 n2)" by blast
from vp have 2: "BNat (f n1 n2) ∈ good v'" by auto
from 1 2 show "∃v. ρ' ⊢ EPrim f e1 e2 ⇓ v ∧ v ∈ good v'" by auto
qed
next ― ‹EIf›
case (6 e1 e2 e3 ρ v' ρ')
from 6(4) show ?case
proof
fix n assume n_e1: "VNat n ∈ E e1 ρ" and els: "n = 0 ⟶ v' ∈ E e3 ρ" and
thn: "n ≠ 0 ⟶ v' ∈ E e2 ρ"
from 6(1)[of "VNat n" ρ'] n_e1 6(5) have e1_w1: "ρ' ⊢ e1 ⇓ BNat n" by auto
show "∃v. ρ' ⊢ EIf e1 e2 e3 ⇓ v ∧ v ∈ good v'"
proof (cases "n = 0")
case True
from 6(2)[of n v' ρ'] True els 6(5) obtain w3 where
e3_w3: "ρ' ⊢ e3 ⇓ w3" and w3_vp: "w3 ∈ good v'" by blast
from e1_w1 True e3_w3 w3_vp show ?thesis by blast
next
case False
from 6(3)[of n v' ρ'] False thn 6(5) obtain w2 where
e2_w2: "ρ' ⊢ e2 ⇓ w2" and w2_vp: "w2 ∈ good v'" by blast
from e1_w1 False e2_w2 have "ρ' ⊢ EIf e1 e2 e3 ⇓ w2"
using eval_if1[of ρ' e1 n e2 w2 e3] by simp
from this w2_vp show ?thesis by (rule_tac x=w2 in exI) simp
qed
qed
qed

theorem sound_wrt_op_sem:
assumes E_e_n: "E e [] = E (ENat n) []" and fv_e: "FV e = {}" shows "e ⇓ ONat n"
proof -
have "VNat n ∈ E (ENat n) []" by simp
with E_e_n have 1: "VNat n ∈ E e []" by simp
have 2: "good_env [] []" by auto
from 1 2 obtain v where e_v: "[] ⊢ e ⇓ v" and v_n: "v ∈ good (VNat n)" using denot_terminates by blast
from v_n have v: "v = BNat n" by auto
from e_v fv_e obtain v' ob where e_vp: "e ⟶* v'" and
vp_ob: "observe v' ob" and v_ob: "bs_observe v ob" using sound_wrt_small_step by blast
from e_vp vp_ob v_ob v show ?thesis unfolding run_def by (case_tac ob) auto
qed

end
```