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