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