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