# Theory DenotCompleteFSet

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

theory DenotCompleteFSet
imports ChangeEnv SmallStepLam DenotSoundFSet
begin

subsection "Reverse substitution preserves denotation"

fun join :: "val ⇒ val ⇒ val option" (infix "⊔" 60) where
"(VNat n) ⊔ (VNat n') = (if n = n' then Some (VNat n) else None)" |
"(VFun f) ⊔ (VFun f') = Some (VFun (f |∪| f'))" |
"v ⊔ v' = None"

lemma combine_values:
assumes vv: "isval v" and v1v: "v1 ∈ E v ρ" and v2v: "v2 ∈ E v ρ"
shows " ∃ v3. v3 ∈ E v ρ ∧ (v1 ⊔ v2 = Some v3)"
using vv v1v v2v by (induction v arbitrary: v1 v2 ρ) auto

lemma le_union1: fixes v1::val assumes v12: "v1 ⊔ v2 = Some v12" shows "v1 ⊑ v12"
proof (cases v1)
case (VNat n1) hence v1: "v1=VNat n1" by simp
show ?thesis
proof (cases v2)
case (VNat n2) with v1 v12 show ?thesis by (cases "n1=n2") auto
next
case (VFun x2) with v1 v12 show ?thesis by auto
qed
next
case (VFun t2) from VFun have v1: "v1=VFun t2" by simp
show ?thesis
proof (cases v2)
case (VNat n1) with v1 v12 show ?thesis by auto
next
case (VFun n2) with v1 v12 show ?thesis by auto
qed
qed

lemma le_union2: "v1 ⊔ v2 = Some v12 ⟹ v2 ⊑ v12"
apply (cases v1)
apply (cases v2)
apply auto
apply (rename_tac x1 x1')
apply (case_tac "x1 = x1'")
apply auto
apply (cases v2)
apply auto
done

lemma le_union_left: "⟦ v1 ⊔ v2 = Some v12; v1 ⊑ v3; v2 ⊑ v3 ⟧ ⟹ v12 ⊑ v3"
apply (cases v1) apply (cases v2) apply force+ done

lemma e_val: "isval v ⟹ ∃ v'. v' ∈ E v ρ"
by (cases v) auto

lemma reverse_subst_lam:
assumes fl: "VFun f ∈ E (ELam x e) ρ"
and vv: "is_val v" and ls: "ELam x e = ELam x (subst y v e')" and xy: "x ≠ y"
and IH: "∀ v1 v2. v2 ∈ E (subst y v e') ((x,v1)#ρ)
⟶ (∃ ρ' v'. v' ∈ E v [] ∧ v2 ∈ E e' ρ' ∧ ρ' ≈ (y,v')#(x,v1)#ρ)"
shows "∃ ρ' v''. v'' ∈ E v [] ∧ VFun f ∈ E (ELam x e') ρ' ∧ ρ' ≈ ((y,v'')#ρ)"
using fl vv ls IH xy
proof (induction f arbitrary: x e e' ρ v y)
case empty
from empty(2) is_val_def obtain v' where vp_v: "v' ∈ E v []" using e_val[of v "[]"] by blast
let ?R = "(y,v')#ρ"
have 1: "VFun {||} ∈ E (ELam x e') ?R" by simp
have 2: "?R ≈ (y, v') # ρ" by auto
from vp_v 1 2 show ?case by blast
next
case (insert a f x e e' ρ v y)
from insert(3) have 1: "VFun f ∈ E (ELam x e) ρ" by auto
obtain v1 v2 where a: "a = (v1,v2)" by (cases a) simp
from insert 1 have "∃ ρ' v''. v'' ∈ E v [] ∧ VFun f ∈ E (ELam x e') ρ' ∧ ρ' ≈ ((y,v'')#ρ)"
by metis
from this obtain ρ'' v'' where vpp_v: "v'' ∈ E v []" and f_l: "VFun f ∈ E (ELam x e') ρ''"
and rpp_r: "ρ'' ≈ ((y,v'')#ρ)" by blast
from insert(3) a have v2_e: "v2 ∈ E e ((x,v1)#ρ)" using e_lam_elim2 by blast
from insert v2_e have "∃ρ'' v'. v' ∈ E v [] ∧ v2 ∈ E e' ρ'' ∧ ρ'' ≈ (y, v')#(x, v1)#ρ" by auto
from this obtain ρ3 v' where vp_v: "v' ∈ E v []" and v2_ep: "v2 ∈ E e' ρ3"
and r3: "ρ3 ≈ (y,v') # (x,v1) # ρ" by blast
from insert(4) have "isval v" by auto
from this vp_v vpp_v obtain v3 where v3_v: "v3 ∈ E v []" and vp_vpp: "v' ⊔ v'' = Some v3"
using combine_values by blast
have 4: "VFun (finsert a f) ∈ E (ELam x e') ((y, v3) # ρ)"
proof -
from vp_vpp have v3_vpp: "v'' ⊑ v3" using le_union2 by simp
from rpp_r v3_vpp have "ρ'' ⊑ (y,v3)#ρ" by (simp add: env_eq_def env_le_def)
from f_l this have 2: "VFun f ∈ E (ELam x e') ((y, v3) # ρ)" by (rule raise_env)
from vp_vpp have vp_v3: "v' ⊑ v3" using le_union1 by simp
from vp_v3 r3 insert have "ρ3 ⊑ (x,v1)#(y,v3)#ρ" by (simp add: env_eq_def env_le_def)
from v2_ep this have 3: "v2 ∈ E e' ((x,v1)#(y,v3)#ρ)" by (rule raise_env)
from 2 3 a show "?thesis" using e_lam_intro2 by blast
qed
have 5: "(y, v3) # ρ ≈ (y, v3) # ρ" by auto
from v3_v 4 5 show ?case by blast
qed

lemma lookup_ext_none: "⟦ lookup ρ y = None; x ≠ y ⟧ ⟹ lookup ((x,v)#ρ) y = None"
by auto

― ‹For reverse subst lemma, the variable case shows up over and over, so we prove it as a lemma›
lemma rev_subst_var:
assumes ev: "e = EVar y ∧ v = e'" and vv: "is_val v" and vp_E: "v' ∈ E e' ρ"
shows "∃ ρ' v''. v'' ∈ E v [] ∧ v' ∈ E e ρ' ∧ ρ' ≈ ((y,v'')#ρ)"
proof -
from vv have lx: "∀ x. x ∈ FV v ⟶ lookup [] x = lookup ρ x" by auto
from ev vp_E lx env_strengthen[of v' v ρ "[]"] have n_Ev: "v' ∈ E v []" by blast
have ly: "lookup ((y,v')#ρ) y = Some v'" by simp
from env_eq_def have rr: "((y,v')#ρ) ≈ ((y,v')#ρ)" by simp
from ev ly have n_Ee: "v' ∈ E e ((y,v')#ρ)" by simp
from n_Ev rr n_Ee show ?thesis by blast
qed

lemma reverse_subst_pres_denot:
assumes vep: "v' ∈ E e' ρ" and vv: "is_val v" and ep: "e' = subst y v e"
shows "∃ ρ' v''. v'' ∈ E v [] ∧ v' ∈ E e ρ' ∧ ρ' ≈ ((y,v'')#ρ)"
using vep vv ep
proof  (induction arbitrary: v' y v e rule: E.induct)
case (1 n ρ) ― ‹e' = ENat n›
from 1(1) have vp: "v' = VNat n" by auto
from 1(3) have "e = ENat n ∨ (e = EVar y ∧ v = ENat n)" by (cases e, auto)
then show ?case
proof
assume e: "e = ENat n"
from 1(2) e_val is_val_def obtain v'' where vpp_E: "v'' ∈ E v []" by force
from env_eq_def have rr: "((y,v'')#ρ) ≈ ((y,v'')#ρ)" by simp
from vp e have vp_E: "v' ∈ E e ((y,v'')#ρ)" by simp
from vpp_E vp_E rr show ?thesis by blast
next
assume ev: "e = EVar y ∧ v = ENat n"
from ev 1(2) 1(1) rev_subst_var show ?thesis by blast
qed
next
case (2 x ρ) ― ‹e' = EVar x›
from 2 have e: "e = EVar x" by (cases e, auto)
from 2 e have xy: "x ≠ y" by force
from 2(2) e_val is_val_def obtain v'' where vpp_E: "v'' ∈ E v []" by force
from env_eq_def have rr: "((y,v'')#ρ) ≈ ((y,v'')#ρ)" by simp
from 2(1) obtain vx where lx: "lookup ρ x = Some vx" and vp_vx: "v' ⊑ vx" by auto
from e lx vp_vx xy have vp_E: "v' ∈ E e ((y,v'')#ρ)" by simp
from vpp_E rr vp_E show ?case by blast
next
case (3 x eb ρ)
{ assume ev: "e = EVar y ∧ v = ELam x eb"
from ev 3(3) 3(2) rev_subst_var have ?case by metis
} also { assume ex: "e = ELam x eb ∧ x = y"
from 3(3) e_val is_val_def obtain v'' where vpp_E: "v'' ∈ E v []" by force
from env_eq_def have rr: "((y,v'')#ρ) ≈ ((y,v'')#ρ)" by simp
from ex have lz: "∀ z. z ∈ FV (ELam x eb) ⟶ lookup ((y,v'')#ρ) z = lookup ρ z" by auto
from ex 3(2) lz env_strengthen[of v' "ELam x eb" ρ "(y,v'')#ρ"]
have vp_E: "v' ∈ E e ((y,v'')#ρ)" by blast
from vpp_E vp_E rr have ?case by blast
} moreover { assume exb: "∃ e'. e = ELam x e' ∧ x ≠ y ∧ eb = subst y v e'"
from exb obtain e'' where e: "e = ELam x e''" and xy: "x ≠ y"
and eb: "eb = subst y v e''" by blast
from 3(2) obtain f where vp: "v' = VFun f" by auto
from 3(2) vp have f_E: "VFun f ∈ E (ELam x eb) ρ" by simp
from 3(4) e xy have ls: "ELam x eb = ELam x (subst y v e'')" by simp
from 3(3) eb have IH: "∀ v1 v2. v2 ∈ E (subst y v e'') ((x,v1)#ρ)
⟶ (∃ ρ' v'. v' ∈ E v [] ∧ v2 ∈ E e'' ρ' ∧ ρ' ≈ (y,v')#(x,v1)#ρ)"
apply clarify apply (subgoal_tac "(v1,v2) ∈ fset {|(v1,v2)|}") prefer 2 apply simp
apply (rule 3(1)) apply assumption apply simp+ done
from f_E 3(3) ls xy IH e vp have ?case apply clarify apply (rule reverse_subst_lam)
apply blast+ done
} moreover from 3(4) have "(e = EVar y ∧ v = ELam x eb)
∨ (e = ELam x eb ∧ x = y)
∨ (∃ e'. e = ELam x e' ∧ x ≠ y ∧ eb = subst y v e')" by (cases e) auto
ultimately show ?case by blast
next
case (4 e1 e2 ρ) ― ‹e' = EApp e1 e2›
from 4(4) 4(5) obtain e1' e2' where
e: "e = EApp e1' e2'" and e1:"e1 = subst y v e1'" and e2: "e2 = subst y v e2'"
apply (cases e) apply (rename_tac x) apply auto apply (case_tac "y = x") apply auto
apply (rename_tac x1 x2) apply (case_tac "y = x1") apply auto done
from 4(3) obtain f v2 and v2'::val and v3' where
f_E: "VFun f ∈ E e1 ρ" and v2_E: "v2 ∈ E e2 ρ" and v23: "(v2',v3') ∈ fset f"
and v2p_v2: "v2' ⊑ v2" and vp_v3: "v' ⊑ v3'" by blast
from 4(1) f_E 4(4) e1 obtain ρ1 w1 where v1_Ev: "w1 ∈ E v []" and f_E1: "VFun f ∈ E e1' ρ1"
and r1: "ρ1 ≈ (y,w1)#ρ" by blast
from 4(2) v2_E 4(4) e2 obtain ρ2 w2 where v2_Ev: "w2 ∈ E v []" and v2_E2: "v2 ∈ E e2' ρ2"
and r2: "ρ2 ≈ (y,w2)#ρ" by blast
from 4(4) v1_Ev v2_Ev combine_values obtain w3 where
w3_Ev: "w3 ∈ E v []" and w123: "w1 ⊔ w2 = Some w3" by (simp only: is_val_def) blast
from w123 le_union1 have w13: "w1 ⊑ w3" by blast
from w123 le_union2 have w23: "w2 ⊑ w3" by blast
from w13 have r13: "((y,w1)#ρ) ⊑ ((y,w3)#ρ)" by (simp add: env_le_def)
from w23 have r23: "((y,w2)#ρ) ⊑ ((y,w3)#ρ)" by (simp add: env_le_def)
from r1 f_E1 have f_E1b: "VFun f ∈ E e1' ((y,w1)#ρ)" by (rule env_swap)
from f_E1b r13 have f_E1c: "VFun f ∈ E e1' ((y,w3)#ρ)" by (rule raise_env)
from r2 v2_E2 have v2_E2b: "v2 ∈ E e2' ((y,w2)#ρ)" by (rule env_swap)
from v2_E2b r23 have v2_E2c: "v2 ∈ E e2' ((y,w3)#ρ)" by (rule raise_env)
from f_E1c v2_E2c v23 v2p_v2 vp_v3 have vp_E2: "v' ∈ E (EApp e1' e2') ((y,w3)#ρ)" by blast
have rr3: "((y,w3)#ρ) ≈ ((y,w3)#ρ)" by (simp add: env_eq_def)
from w3_Ev vp_E2 rr3 e show ?case by blast
next
case (5 f e1 e2 ρ) ― ‹e' = EPrim f e1 e2, very similar to case for EApp›
from 5(4) 5(5) obtain e1' e2' where
e: "e = EPrim f e1' e2'" and e1:"e1 = subst y v e1'" and e2: "e2 = subst y v e2'"
apply (cases e) apply auto apply (rename_tac x) apply (case_tac "y = x") apply auto
apply (rename_tac x1 x2) apply (case_tac "y = x1") apply auto done
from 5(3) obtain n1 n2 where
n1_E: "VNat n1 ∈ E e1 ρ" and n2_E: "VNat n2 ∈ E e2 ρ" and vp: "v' = VNat (f n1 n2)" by blast
from 5(1) n1_E 5(4) e1 obtain ρ1 w1 where v1_Ev: "w1 ∈ E v []" and n1_E1: "VNat n1 ∈ E e1' ρ1"
and r1: "ρ1 ≈ (y,w1)#ρ" by blast
from 5(2) n2_E 5(4) e2 obtain ρ2 w2 where v2_Ev: "w2 ∈ E v []" and n2_E2: "VNat n2 ∈ E e2' ρ2"
and r2: "ρ2 ≈ (y,w2)#ρ" by blast
from 5(4) v1_Ev v2_Ev combine_values obtain w3 where
w3_Ev: "w3 ∈ E v []" and w123: "w1 ⊔ w2 = Some w3" by (simp only: is_val_def) blast
from w123 le_union1 have w13: "w1 ⊑ w3" by blast
from w123 le_union2 have w23: "w2 ⊑ w3" by blast
from w13 have r13: "((y,w1)#ρ) ⊑ ((y,w3)#ρ)" by (simp add: env_le_def)
from w23 have r23: "((y,w2)#ρ) ⊑ ((y,w3)#ρ)" by (simp add: env_le_def)
from r1 n1_E1 have n1_E1b: "VNat n1 ∈ E e1' ((y,w1)#ρ)" by (rule env_swap)
from n1_E1b r13 have n1_E1c: "VNat n1 ∈ E e1' ((y,w3)#ρ)" by (rule raise_env)
from r2 n2_E2 have n2_E2b: "VNat n2 ∈ E e2' ((y,w2)#ρ)" by (rule env_swap)
from n2_E2b r23 have v2_E2c: "VNat n2 ∈ E e2' ((y,w3)#ρ)" by (rule raise_env)
from n1_E1c v2_E2c vp have vp_E2: "v' ∈ E (EPrim f e1' e2') ((y,w3)#ρ)" by blast
have rr3: "((y,w3)#ρ) ≈ ((y,w3)#ρ)" by (simp add: env_eq_def)
from w3_Ev vp_E2 rr3 e show ?case by blast
next
case (6 e1 e2 e3 ρ) ― ‹e' = EIf e1 e2 e3›
from 6(5) 6(6) obtain e1' e2' e3' where
e: "e = EIf e1' e2' e3'" and e1:"e1 = subst y v e1'" and e2: "e2 = subst y v e2'"
and e3: "e3 = subst y v e3'"
apply (cases e) apply auto apply (case_tac "y=x1") apply auto apply (case_tac "y=x31") by auto
from 6(4) e_if_elim obtain n where n_E: "VNat n ∈ E e1 ρ" and
els: "n = 0 ⟶ v' ∈ E e3 ρ" and thn: "n ≠ 0 ⟶ v' ∈ E e2 ρ" by blast
from 6 n_E e1 obtain ρ1 w1 where w1_Ev: "w1 ∈ E v []" and n_E2: "VNat n ∈ E e1' ρ1"
and r1: "ρ1 ≈ (y,w1)#ρ" by blast
show ?case
proof (cases "n = 0")
case True with els have vp_E2: "v' ∈ E e3 ρ" by simp
from 6 vp_E2 e3 obtain ρ2 w2 where w2_Ev: "w2 ∈ E v []" and vp_E2: "v' ∈ E e3' ρ2"
and r2: "ρ2 ≈ (y,w2)#ρ" by blast
from 6(5) w1_Ev w2_Ev combine_values obtain w3 where
w3_Ev: "w3 ∈ E v []" and w123: "w1 ⊔ w2 = Some w3" by (simp only: is_val_def) blast
from w123 le_union1 have w13: "w1 ⊑ w3" by blast
from w123 le_union2 have w23: "w2 ⊑ w3" by blast
from w13 have r13: "((y,w1)#ρ) ⊑ ((y,w3)#ρ)" by (simp add: env_le_def)
from w23 have r23: "((y,w2)#ρ) ⊑ ((y,w3)#ρ)" by (simp add: env_le_def)
from r1 n_E2 have n_E1b: "VNat n ∈ E e1' ((y,w1)#ρ)" by (rule env_swap)
from n_E1b r13 have n_E1c: "VNat n ∈ E e1' ((y,w3)#ρ)" by (rule raise_env)
from r2 vp_E2 have vp_E2b: "v' ∈ E e3' ((y,w2)#ρ)" by (rule env_swap)
from vp_E2b r23 have vp_E2c: "v' ∈ E e3' ((y,w3)#ρ)" by (rule raise_env)
have rr3: "((y,w3)#ρ) ≈ ((y,w3)#ρ)" by (simp add: env_eq_def)
from True n_E1c vp_E2c e have vp_E3: "v' ∈ E e ((y,w3)#ρ)" by auto
from w3_Ev rr3 vp_E3 show ?thesis by blast
next
case False with thn have vp_E2: "v' ∈ E e2 ρ" by simp
from 6 vp_E2 e2 obtain ρ2 w2 where w2_Ev: "w2 ∈ E v []" and vp_E2: "v' ∈ E e2' ρ2"
and r2: "ρ2 ≈ (y,w2)#ρ" by blast
from 6(5) w1_Ev w2_Ev combine_values obtain w3 where
w3_Ev: "w3 ∈ E v []" and w123: "w1 ⊔ w2 = Some w3" by (simp only: is_val_def) blast
from w123 le_union1 have w13: "w1 ⊑ w3" by blast
from w123 le_union2 have w23: "w2 ⊑ w3" by blast
from w13 have r13: "((y,w1)#ρ) ⊑ ((y,w3)#ρ)" by (simp add: env_le_def)
from w23 have r23: "((y,w2)#ρ) ⊑ ((y,w3)#ρ)" by (simp add: env_le_def)
from r1 n_E2 have n_E1b: "VNat n ∈ E e1' ((y,w1)#ρ)" by (rule env_swap)
from n_E1b r13 have n_E1c: "VNat n ∈ E e1' ((y,w3)#ρ)" by (rule raise_env)
from r2 vp_E2 have vp_E2b: "v' ∈ E e2' ((y,w2)#ρ)" by (rule env_swap)
from vp_E2b r23 have vp_E2c: "v' ∈ E e2' ((y,w3)#ρ)" by (rule raise_env)
have rr3: "((y,w3)#ρ) ≈ ((y,w3)#ρ)" by (simp add: env_eq_def)
from False n_E1c vp_E2c e have vp_E3: "v' ∈ E e ((y,w3)#ρ)" by auto
from w3_Ev rr3 vp_E3 show ?thesis by blast
qed
qed

subsection "Reverse reduction preserves denotation"

lemma reverse_step_pres_denot:
fixes e::exp assumes e_ep: "e ⟶ e'" and v_ep: "v ∈ E e' ρ"
shows "v ∈ E e ρ"
using e_ep v_ep
proof (induction arbitrary: v ρ rule: reduce.induct)
case (beta v x e v' ρ)
from beta obtain ρ' v'' where 1: "v'' ∈ E v []" and 2: "v' ∈ E e ρ'" and 3: "ρ' ≈ (x, v'') # ρ"
using reverse_subst_pres_denot[of v' "subst x v e" ρ v x e] by blast
from beta 1 2 3 show ?case
apply simp apply (rule_tac x="{|(v'',v')|}" in exI) apply (rule conjI)
apply clarify apply simp apply (rule env_swap) apply blast apply blast
apply (rule_tac x=v'' in exI) apply (rule conjI) apply (rule env_strengthen)
apply assumption apply force apply force done
qed auto

lemma reverse_multi_step_pres_denot:
fixes e::exp assumes e_ep: "e ⟶* e'" and v_ep: "v ∈ E e' ρ" shows "v ∈ E e ρ"
using e_ep v_ep reverse_step_pres_denot
by (induction arbitrary: v ρ rule: multi_step.induct) auto

subsection "Completeness"

theorem completeness:
assumes ev: "e ⟶* v"and vv: "is_val v"
shows "∃ v'. v' ∈ E e ρ ∧ v' ∈ E v []"
proof -
from vv have "∃ v'. v' ∈ E v []" using e_val by auto
from this obtain v' where vp_v: "v' ∈ E v []" by blast
from vp_v vv have vp_v2: "v' ∈ E v ρ" using env_strengthen by force
from ev vp_v2 reverse_multi_step_pres_denot[of e v v' ρ]
have "v' ∈ E e ρ" by simp
from this vp_v show ?thesis by blast
qed

theorem reduce_pres_denot: fixes e::exp assumes r: "e ⟶ e'" shows "E e = E e'"
apply (rule ext) apply (rule equalityI) apply (rule subsetI)
apply (rule subject_reduction) apply assumption using r apply assumption
apply (rule subsetI)
using r apply (rule reverse_step_pres_denot) apply assumption
done

theorem multi_reduce_pres_denot: fixes e::exp assumes r: "e ⟶* e'" shows "E e = E e'"
using r reduce_pres_denot by induction auto

theorem complete_wrt_op_sem:
assumes e_n: "e ⇓ ONat n" shows "E e [] = E (ENat n) []"
proof -
from e_n have 1: "e ⟶* ENat n"
unfolding run_def apply simp apply (erule exE)
apply (rename_tac v) apply (case_tac v) apply auto done
from 1 show ?thesis using multi_reduce_pres_denot by simp
qed

end
```