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
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