# Theory DenotCongruenceFSet

```section "Soundness wrt. contextual equivalence"

subsection "Denotational semantics is a congruence"

theory DenotCongruenceFSet
imports ChangeEnv DenotSoundFSet DenotCompleteFSet
begin

lemma e_lam_cong[cong]: "E e  = E e' ⟹ E (ELam x e) = E (ELam x e')"
by (rule ext) simp

lemma e_app_cong[cong]: "⟦ E e1 = E e1'; E e2 = E e2' ⟧ ⟹ E (EApp e1 e2) = E (EApp e1' e2')"
by (rule ext) simp

lemma e_prim_cong[cong]: "⟦ E e1 = E e1'; E e2 = E e2' ⟧ ⟹ E(EPrim f e1 e2) = E(EPrim f e1' e2')"
by (rule ext) simp

lemma e_if_cong[cong]: "⟦ E e1 = E e1'; E e2 = E e2'; E e3 = E e3' ⟧
⟹ E (EIf e1 e2 e3) = E (EIf e1' e2' e3')"
by (rule ext) simp

datatype ctx = CHole | CLam name ctx | CAppL ctx exp | CAppR exp ctx
| CPrimL "nat ⇒ nat ⇒ nat"  ctx exp | CPrimR "nat ⇒ nat ⇒ nat"  exp ctx
| CIf1 ctx exp exp | CIf2 exp ctx exp | CIf3 exp exp ctx

fun plug :: "ctx ⇒ exp ⇒ exp" where
"plug CHole e = e" |
"plug (CLam x C) e = ELam x (plug C e)" |
"plug (CAppL C e2) e = EApp (plug C e) e2" |
"plug (CAppR e1 C) e = EApp e1 (plug C e)" |
"plug (CPrimL f C e2) e = EPrim f (plug C e) e2" |
"plug (CPrimR f e1 C) e = EPrim f e1 (plug C e)" |
"plug (CIf1 C e2 e3) e = EIf (plug C e) e2 e3" |
"plug (CIf2 e1 C e3) e = EIf e1 (plug C e) e3" |
"plug (CIf3 e1 e2 C) e = EIf e1 e2 (plug C e)"

lemma congruence: "E e = E e' ⟹ E (plug C e) = E (plug C e')"
proof (induction C arbitrary: e e')
case (CIf1 C e2 e3)
have "E (EIf (plug C e) e2 e3) = E (EIf (plug C e') e2 e3)"
apply (rule e_if_cong) using CIf1 apply blast+ done
then show ?case by simp
next
case (CIf2 e1 C e3)
have "E (EIf e1 (plug C e) e3) = E (EIf e1 (plug C e') e3)"
apply (rule e_if_cong) using CIf2 apply blast+ done
then show ?case by simp
next
case (CIf3 e1 e2 C)
have "E (EIf e1 e2 (plug C e)) = E (EIf e1 e2 (plug C e'))"
apply (rule e_if_cong) using CIf3 apply blast+ done
then show ?case by simp
qed force+

subsection "Auxiliary lemmas"

lemma diverge_denot_empty: assumes d: "diverge e" and fve: "FV e = {}" shows "E e [] = {}"
proof (rule classical)
assume "E e [] ≠ {}"
from this obtain A where wte: "A ∈ E e []" by auto
have ge: "good_env [] []" by blast
from wte ge obtain v where e_v: "[] ⊢ e ⇓ v" and gv: "v ∈ good A"
using denot_terminates by blast
from e_v fve obtain v' where e_vp: "e ⟶* v'" and val_vp: "isval v'"
using sound_wrt_small_step by blast
from d e_vp have "∃ e'. v' ⟶ e'" by (simp add: diverge_def)
with val_vp have "False" using val_stuck by force
from this show ?thesis ..
qed

lemma goes_wrong_denot_empty:
assumes gw: "goes_wrong e" and fv_e: "FV e = {}" shows "E e [] = {}"
proof (rule classical)
assume "E e [] ≠ {}"
from this obtain A where wte: "A ∈ E e []" by auto
have ge: "good_env [] []" by blast
from gw obtain e' where e_ep: "e ⟶* e'" and s_ep: "stuck e'" and nv_ep: "¬ isval e'"
by auto
from wte e_ep have wtep: "A ∈ E e' []" using preservation by blast
from fv_e e_ep have fv_ep: "FV e' = {}" using reduction_pres_fv by auto
from wtep fv_ep have "is_val e' ∨ (∃ e''. e' ⟶ e'')" using progress[of A e' "[]" ] by simp
from this s_ep nv_ep have "False" by simp
from this show ?thesis ..
qed

lemma denot_empty_diverge: assumes E_e: "E e [] = {}" and fv_e: "FV e = {}"
shows "diverge e ∨ goes_wrong e"
proof (rule classical)
assume nd_gw: "¬ (diverge e ∨ goes_wrong e)"
from this have nd: "¬ diverge e" by blast
from nd_gw have gw: "¬ goes_wrong e" by blast
from nd obtain v::exp where e_v: "e ⟶* v" and stuck: "¬ (∃ e'. v ⟶ e')"
by (simp only: diverge_def) blast
from gw e_v stuck have val_v: "isval v" by (simp only: goes_wrong_def stuck_def) blast
from fv_e e_v have fv_v: "FV v = {}" using reduction_pres_fv by auto
from val_v fv_v have val_v2: "is_val v" by simp
from e_v val_v2 obtain A where wte: "A ∈ E e []" and wtv: "A ∈ E v []"
using completeness[of e v] by blast
from this E_e have "False" by auto
from this show ?thesis ..
qed

lemma val_ty_observe:
"⟦ A ∈ E v []; A ∈ E v' [];
observe v ob; isval v'; isval v ⟧ ⟹ observe v' ob"
apply (cases v) apply auto apply (cases v') apply auto
apply (cases v') apply auto
apply (cases ob) apply auto
done

subsection "Soundness wrt. contextual equivalence"

lemma soundness_wrt_ctx_equiv_aux[rule_format]:
assumes e12: "E e1 = E e2"
and fv_e1: "FV (plug C e1) = {}" and fv_e2: "FV (plug C e2) = {}"
shows "run (plug C e1) ob ⟶ run (plug C e2) ob"
proof
assume run_Ce1: "run (plug C e1) ob"
from e12 have pe12: "E (plug C e1) = E (plug C e2)" by (rule congruence)
from run_Ce1 have "((∃ v. (plug C e1) ⟶* v ∧ observe v ob)
∨ ((diverge (plug C e1) ∨ goes_wrong (plug C e1)) ∧ ob = OBad))"
by (simp only: run_def)
from this show "run (plug C e2) ob"
proof
assume "∃v. plug C e1 ⟶* v ∧ observe v ob"
from this obtain v where r_v: "plug C e1 ⟶* v"
and ob_v: "observe v ob" by blast
from r_v fv_e1 have fv_v: "FV v = {}" by (rule reduction_pres_fv)
from ob_v fv_v have val_v: "is_val v" by (cases v) auto
from r_v val_v obtain A  where ce1a: "A ∈ E (plug C e1) []"
and wt_v_ap: "A ∈ E v []" using completeness[of "plug C e1" v] by auto
from ce1a pe12 have ce2a: "A ∈ E (plug C e2) []" by force
have ge: "good_env [] []" by blast
from ce2a ge obtain v' where Ce2_vp: "[] ⊢ plug C e2 ⇓ v'" and vpa: "v' ∈ good A"
using denot_terminates by blast
from Ce2_vp fv_e2 obtain v'' ob' where Ce2_vpp: "plug C e2 ⟶* v''" and vvpp: "isval v''"
and ovpp: "observe v'' ob'" and vp_ob: "bs_observe v' ob'"
using sound_wrt_small_step[of "plug C e2" v'] by blast
from ovpp have vpp_ob: "observe v'' ob"
proof -
from ce2a Ce2_vpp have vpp_app: "A ∈ E v'' []" using preservation by blast
from vpp_app wt_v_ap ob_v vvpp val_v
show ?thesis apply simp apply (rule val_ty_observe) prefer 3 apply assumption apply auto done
qed
from Ce2_vpp vpp_ob show ?thesis by (simp add: run_def) blast
next
assume d_e1: "(diverge (plug C e1) ∨ goes_wrong (plug C e1)) ∧ ob = OBad"
from d_e1 fv_e1 have E_Ce1: "E (plug C e1) [] = {}"
using diverge_denot_empty goes_wrong_denot_empty by blast
from E_Ce1 pe12 have E_Ce2: "E (plug C e2) [] = {}" by simp
from E_Ce2 fv_e2 have "diverge (plug C e2) ∨ goes_wrong (plug C e2)"
using denot_empty_diverge by blast
from this d_e1 show ?thesis  by (simp add: run_def)
qed
qed

definition ctx_equiv :: "exp ⇒ exp ⇒ bool" (infix "≃" 51) where
"e ≃ e' ≡ ∀ C ob. FV (plug C e) = {} ∧ FV (plug C e') = {} ⟶
run (plug C e) ob = run (plug C e') ob"

theorem denot_sound_wrt_ctx_equiv: assumes e12: "E e1 = E e2" shows "e1 ≃ e2"
using e12
apply (simp only: ctx_equiv_def) apply clarify apply (rule iffI)
apply (rule soundness_wrt_ctx_equiv_aux) apply assumption+
apply (rule soundness_wrt_ctx_equiv_aux) apply auto
done

end
```