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