Theory ChangeEnv

section "Subsumption and change of environment"

theory ChangeEnv
  imports Main Lambda DeclSemAsDenotFSet ValuesFSetProps
begin

lemma e_prim_intro[intro]: "⟦ VNat n1 ∈ E e1 ρ; VNat n2 ∈ E e2 ρ; v = VNat (f n1 n2) ⟧
    ⟹ v ∈ E (EPrim f e1 e2) ρ" by auto

lemma e_prim_elim[elim]: "⟦ v ∈ E (EPrim f e1 e2) ρ;
   ⋀ n1 n2. ⟦ VNat n1 ∈ E e1 ρ; VNat n2 ∈ E e2 ρ; v = VNat (f n1 n2) ⟧ ⟹ P ⟧ ⟹ P"
  by auto 
 
lemma e_app_elim[elim]: "⟦ v3 ∈ E (EApp e1 e2) ρ;
  ⋀ f v2 v2' v3'. ⟦ VFun f ∈ E e1 ρ; v2 ∈ E e2 ρ; (v2',v3') ∈ fset f; v2' ⊑ v2; v3 ⊑ v3' ⟧ ⟹ P
 ⟧ ⟹ P"
  by auto

lemma e_app_intro[intro]: "⟦ VFun f ∈ E e1 ρ; v2 ∈ E e2 ρ; (v2',v3') ∈ fset f; v2' ⊑ v2; v3 ⊑ v3'⟧
     ⟹ v3 ∈ E (EApp e1 e2) ρ" by auto 

lemma e_lam_intro[intro]: "⟦ v = VFun f;
      ∀ v1 v2. (v1,v2) ∈ fset f ⟶ v2 ∈ E e ((x,v1)#ρ) ⟧
    ⟹ v ∈ E (ELam x e) ρ"
  by auto 

lemma e_lam_intro2[intro]: 
  "⟦ VFun f ∈ E (ELam x e) ρ; v2 ∈ E e ((x,v1)#ρ) ⟧ 
  ⟹ VFun (finsert (v1,v2) f) ∈ E (ELam x e) ρ"    
  by auto 

lemma e_lam_intro3[intro]: "VFun {||} ∈ E (ELam x e) ρ"
  by auto

lemma e_if_intro[intro]: "⟦ VNat n ∈ E e1 ρ; n = 0 ⟶ v ∈ E e3 ρ; n ≠ 0 ⟶ v ∈ E e2 ρ ⟧
    ⟹ v ∈ E (EIf e1 e2 e3) ρ"
  by auto 

lemma e_var_intro[elim]: "⟦ lookup ρ x = Some v'; v ⊑ v' ⟧ ⟹ v ∈ E (EVar x) ρ"
  by auto

lemma e_var_elim[elim]: "⟦ v ∈ E (EVar x) ρ;
   ⋀ v'. ⟦ lookup ρ x = Some v'; v ⊑ v' ⟧ ⟹ P ⟧ ⟹ P"
  by auto 

lemma e_lam_elim[elim]: "⟦ v ∈ E (ELam x e) ρ;
   ⋀ f. ⟦ v = VFun f; ∀ v1 v2. (v1,v2) ∈ fset f ⟶ v2 ∈ E e ((x,v1)#ρ) ⟧
    ⟹ P ⟧ ⟹ P"
  by auto 

lemma e_lam_elim2[elim]: "⟦ VFun (finsert (v1,v2) f) ∈ E (ELam x e) ρ;
   ⟦ v2 ∈ E e ((x,v1)#ρ) ⟧ ⟹ P ⟧ ⟹ P"
  by auto 

lemma e_if_elim[elim]: "⟦ v ∈ E (EIf e1 e2 e3) ρ;
   ⋀ n. ⟦ VNat n ∈ E e1 ρ; n = 0 ⟶ v ∈ E e3 ρ; n ≠ 0 ⟶ v ∈ E e2 ρ ⟧ ⟹ P ⟧ ⟹ P" 
  by auto 
    
definition xenv_le :: "name set ⇒ env ⇒ env ⇒ bool" ("_ ⊢ _ ⊑ _" [51,51,51] 52) where 
  "X ⊢ ρ ⊑ ρ' ≡ ∀ x v. x ∈ X ∧ lookup ρ x = Some v ⟶ (∃ v'. lookup ρ' x = Some v' ∧ v ⊑ v')" 
declare xenv_le_def[simp]
    
proposition change_env_le: fixes v::val and ρ::env
  assumes de: "v ∈ E e ρ" and vp_v: "v' ⊑ v" and rr: "FV e ⊢ ρ ⊑ ρ'"
  shows "v' ∈ E e ρ'"
  using de rr vp_v
proof (induction e arbitrary: v v' ρ ρ' rule: exp.induct)
  case (EVar x v v' ρ ρ')
  from EVar obtain v2 where lx: "lookup ρ x = Some v2" and v_v2: "v ⊑ v2" by auto 
  from lx EVar obtain v3 where 
    lx2: "lookup ρ' x = Some v3" and v2_v3: "v2 ⊑ v3" by force
  from v_v2 v2_v3 have v_v3: "v ⊑ v3" by (rule val_le_trans)
  from EVar v_v3 have vp_v3: "v' ⊑ v3" using val_le_trans by blast 
  from lx2 vp_v3 show ?case by (rule e_var_intro)
next
  case (ENat n) then show ?case by simp
next
  case (ELam x e)
  from ELam(2) obtain f where v: "v = VFun f" and 
    body: "∀ v1 v2. (v1,v2) ∈ fset f ⟶ v2 ∈ E e ((x,v1)#ρ)" by auto
  from v ELam(4) obtain f' where vp: "v' = VFun f'" and fp_f: "fset f' ⊆ fset f" 
    by (case_tac v') auto 
  from vp show ?case 
  proof (simp,clarify)
    fix v1 v2 assume v12: "(v1,v2)∈ fset f'" 
    from v12 fp_f have v34: "(v1,v2) ∈ fset f" by blast
    from v34 body have v4_E: "v2 ∈ E e ((x,v1)#ρ)" by blast
    from ELam(3) have rr2: "FV e ⊢ ((x,v1)#ρ) ⊑ ((x,v1)#ρ')" by auto
    from ELam(1) v4_E rr2 show "v2 ∈ E e ((x,v1)#ρ')" by auto
  qed
next
  case (EApp e1 e2)
  from EApp(3) obtain f and v2::val and v2' v3' where 
    f_e1: "VFun f ∈ E e1 ρ" and v2_e2: "v2 ∈ E e2 ρ" and
    v23p_f: "(v2',v3') ∈ fset f" and v2p_v2: "v2' ⊑ v2" and v_v3: "v ⊑ v3'" by blast
  from EApp(4) have 1: "FV e1 ⊢ ρ ⊑ ρ'" by auto
  have f_f: "VFun f ⊑ VFun f" by auto 
  from EApp(1) f_e1 1 f_f have f_e1b: "VFun f ∈ E e1 ρ'" by blast
  from EApp(4) have 2: "FV e2 ⊢ ρ ⊑ ρ'" by auto
  from EApp(2) v2_e2 2 have v2_e2b: "v2 ∈ E e2 ρ'" by auto 
  from EApp(5) v_v3 have vp_v3p: "v' ⊑ v3'" by (rule val_le_trans)
  from f_e1b v2_e2b v23p_f v2p_v2 vp_v3p
  show ?case by auto
next
  case (EPrim f e1 e2)
  from EPrim(3) obtain n1 n2 where n1_e1: "VNat n1 ∈ E e1 ρ" and 
    n2_e2: "VNat n2 ∈ E e2 ρ" and v: "v = VNat (f n1 n2)" by blast
  from EPrim(4) have 1: "FV e1 ⊢ ρ ⊑ ρ'" by auto
  from EPrim(1) n1_e1 1 have n1_e1b: "VNat n1 ∈ E e1 ρ'" by blast
  from EPrim(4) have 2: "FV e2 ⊢ ρ ⊑ ρ'" by auto
  from EPrim(2) n2_e2 2 have n2_e2b: "VNat n2 ∈ E e2 ρ'" by blast
  from v EPrim(5) have vp: "v' = VNat (f n1 n2)" by auto
  from n1_e1b n2_e2b vp show ?case by auto 
next
  case (EIf e1 e2 e3)
  then show ?case apply simp apply clarify apply (rule_tac x=n in exI) apply (rule conjI)
      apply force apply force done
qed
  
― ‹Subsumption is admissible› 
proposition e_sub: "⟦ v ∈ E e ρ; v' ⊑ v ⟧ ⟹ v' ∈ E e ρ"
  apply (subgoal_tac "FV e ⊢ ρ ⊑ ρ") using change_env_le apply blast apply auto done

lemma env_le_ext: fixes ρ::env assumes rr: "ρ ⊑ ρ'" shows "((x,v)#ρ) ⊑ ((x,v)#ρ')"  
  using rr apply (simp add: env_le_def) done

lemma change_env: fixes ρ::env assumes de: "v ∈ E e ρ" and rr: "FV e ⊢ ρ ⊑ ρ'" shows "v ∈ E e ρ'"
proof -
  have vv: "v ⊑ v" by auto
  from de rr vv show ?thesis using change_env_le by blast
qed

lemma raise_env: fixes ρ::env assumes de: "v ∈ E e ρ" and rr: "ρ ⊑ ρ'" shows "v ∈ E e ρ'"
  using de rr change_env env_le_def by auto 

lemma env_eq_refl[simp]: fixes ρ::env shows "ρ ≈ ρ" by (simp add: env_eq_def) 

lemma env_eq_ext: fixes ρ::env assumes rr: "ρ ≈ ρ'" shows "((x,v)#ρ) ≈ ((x,v)#ρ')"  
  using rr by (simp add: env_eq_def) 

lemma eq_implies_le: fixes ρ::env shows "ρ ≈ ρ' ⟹ ρ ⊑ ρ'" 
  by (simp add: env_le_def env_eq_def) 

lemma env_swap: fixes ρ::env assumes rr: "ρ ≈ ρ'" and ve: "v ∈ E e ρ" shows "v ∈ E e ρ'"
  using rr ve apply (subgoal_tac "ρ ⊑ ρ'") prefer 2 apply (rule eq_implies_le) apply blast
  apply (rule raise_env) apply auto done

lemma env_strengthen: "⟦ v ∈ E e ρ; ∀ x. x ∈ FV e ⟶ lookup ρ' x = lookup ρ x ⟧ ⟹ v ∈ E e ρ'"
  using change_env by auto    

end