Theory TypeEnvironment

(*  Title:      TypeEnvironment
    Author:     Javier de Dios and Ricardo Peña
    Copyright:  June 2008, Universidad Complutense de Madrid
*)

header {* Type Environment and operators *}

(*<*)
theory TypeEnvironment
imports Main 
begin
(*>*)

text{*
Non-functional algebraic types may be safe types s'', condemned types d'' or indanger
types r''.
*}

datatype Mark = s'' | d'' | r''

text{*
A type environment is a partial mapping from program variables to marks.
*}

types TypeEnvironment = "string \<rightharpoonup> Mark"

text{*
Some auxiliary predicates: 'unsafe' is true for condemned and in-danger types,
'safe' is true for safe types.
*}

constdefs unsafe :: "Mark option => bool"
"unsafe x ≡  (x = Some d'')  ∨ (x = Some r'')"

constdefs safe :: "Mark option => bool"
"safe x ≡  (x = Some s'')"

subsection {* Operators on type environments  *}

constdefs
unionEnv ::  "TypeEnvironment => TypeEnvironment => TypeEnvironment" 
"unionEnv Γ1 Γ2 ≡ (%x. if x: dom Γ1 then Γ1 x else Γ2 x)"

text{*
Operator +: Disjoint union of environments
*}

constdefs def_disjointUnionEnv ::  "TypeEnvironment => TypeEnvironment => bool"
"def_disjointUnionEnv Γ1 Γ2 ≡  dom Γ1 ∩ dom Γ2 = {}"

constdefs disjointUnionEnv ::  "TypeEnvironment => TypeEnvironment => TypeEnvironment" (infix "+" 100)
"Γ1 + Γ2 ≡ unionEnv Γ1 Γ2"

text{*
Operator $\otimes$ : It allows to join two non-disjoint environments provided they
map the common variables to the same types. 
*}

constdefs
def_nonDisjointUnionEnv :: "TypeEnvironment =>  TypeEnvironment => bool"
"def_nonDisjointUnionEnv Γ1 Γ2 ≡ (∀x ∈ dom Γ1 ∩ dom Γ2. Γ1 x = Γ2 x)"

constdefs
nonDisjointUnionEnv :: "TypeEnvironment => TypeEnvironment => TypeEnvironment" (infixl "⊗" 60)
"Γ1 ⊗ Γ2 ≡ unionEnv Γ1 Γ2"


text{*
Operator $\otimes$ : It allows to join n-non-disjoint environments provided they
map the common variables to the same types. 
*}

fun nonDisjointUnionEnvList :: "TypeEnvironment list => TypeEnvironment" where
  "nonDisjointUnionEnvList Γs = foldl nonDisjointUnionEnv empty Γs"

fun def_nonDisjointUnionEnvList :: "TypeEnvironment list => bool" where
  "def_nonDisjointUnionEnvList []         = True"

| "def_nonDisjointUnionEnvList (G#Gs) = (let Gs' = nonDisjointUnionEnvList Gs;
                                             def_Gs' = def_nonDisjointUnionEnvList Gs in 
                                             def_nonDisjointUnionEnv G Gs' ∧ def_Gs' )"


text{*
Operator $\oplus$ : It allows to join two non-disjoint environments provided they
map the common variables to the same safe types.
*}

constdefs 
def_nonDisjointUnionSafeEnv :: "TypeEnvironment => TypeEnvironment => bool"
"def_nonDisjointUnionSafeEnv Γ1 Γ2 ≡ (∀x ∈ dom Γ1 ∩ dom Γ2. safe (Γ1 x) ∧ safe (Γ2 x))"

constdefs
nonDisjointUnionSafeEnv :: "TypeEnvironment => TypeEnvironment => TypeEnvironment" (infixl "⊕" 60)
"Γ1 ⊕ Γ2 ≡ unionEnv Γ1 Γ2"

fun nonDisjointUnionSafeEnvList :: "TypeEnvironment list => TypeEnvironment" where
  "nonDisjointUnionSafeEnvList Γs = foldl nonDisjointUnionSafeEnv empty Γs"

fun def_nonDisjointUnionSafeEnvList :: "TypeEnvironment list => bool" where
  "def_nonDisjointUnionSafeEnvList []         = True"

| "def_nonDisjointUnionSafeEnvList (G#Gs) = (let Gs' = nonDisjointUnionSafeEnvList Gs;
                                             def_Gs' = def_nonDisjointUnionSafeEnvList Gs in 
                                             def_nonDisjointUnionSafeEnv G Gs' ∧ def_Gs' )"


text{*
Operator $\triangleright$ : This is used in rules for let. In the union $\Gamma$1 $\triangleright$ $\Gamma$2
not allowed that variables in L may have unsafe type in $\Gamma$1 . Also, variables
common to $\Gamma$2 and L may not have unsafe type in $\Gamma$2. Once well defined, in
environment  $\Gamma$1 $\triangleright$ $\Gamma$2 the types assigned in $\Gamma$2 to common 
variables, will prevail.
*}


constdefs
def_pp :: "TypeEnvironment => TypeEnvironment => string set => bool"
"def_pp Γ1 Γ2 L ≡
 (∀x. x ∈ dom Γ1 --> unsafe (Γ1 x) --> x ∉ L ∧ (x ∉ dom Γ2 ∨ (Γ2 x ≠ Some s'' ∧ Γ2 x ≠  Some d''))) ∧
 (∀x. x ∈ dom Γ2 ∧ 
          (Γ2 x = Some s'' ∨ Γ2 x =  Some d'') 
       --> x ∈ L)"

constdefs
pp :: "TypeEnvironment => TypeEnvironment => string set => TypeEnvironment"  ("_\<triangleright>_ _")
"Γ1 \<triangleright> Γ2 L ≡  (%x. (if x ∉ dom Γ1 ∨ (x ∈ dom Γ1 ∩ dom Γ2 ∧ safe (Γ1 x))
                     then Γ2 x else Γ1 x))"



text{*
Lemmas for unionEnv operator
*}

lemma empty_unionEnv: "unionEnv m empty = m"
apply (rule ext) 
by (simp add: unionEnv_def split: option.split add: dom_def)

lemma dom_empty_unionEnv: "dom (unionEnv m1 empty) = dom m1"
apply (subgoal_tac "unionEnv m1 empty = m1")
by (simp, rule empty_unionEnv)


text{*
Lemmas for disjointUnionEnv operator
*}

lemma empty_disjointUnionEnv: "disjointUnionEnv m empty = m"
by (simp add: disjointUnionEnv_def, rule empty_unionEnv)

lemma dom_empty_disjointUnionEnv: "dom (disjointUnionEnv m1 empty) = dom m1"
by (simp add: disjointUnionEnv_def, rule dom_empty_unionEnv)

lemma union_dom_disjointUnionEnv: 
 "def_disjointUnionEnv Γ1 Γ2 ==> dom (disjointUnionEnv Γ1 Γ2) = dom Γ1 ∪ dom Γ2"
apply (simp add: def_disjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def, auto)
by (split split_if_asm,simp,simp)

lemma dom_disjointUnionEnv_monotone:
  "dom (G + G') = dom G ∪  dom G'"
apply (simp add: disjointUnionEnv_def add: unionEnv_def, auto)
by (split split_if_asm, simp, simp)

text{*
Lemmas for nonDisjointUnionEnv operator
*}

lemma empty_nonDisjointUnionEnv :
  "empty ⊗ A = A"
by (simp add: nonDisjointUnionEnv_def add: unionEnv_def)

lemma refl_nonDisjointUnionEnv :
  "A ⊗ A = A"
by (simp add: nonDisjointUnionEnv_def add: unionEnv_def)


lemma list_induct3: 
  "[| P [] 0;
  !!x xs. P (x#xs) 0;
  !!i. P [] (Suc i);
   !!x xs i. P xs i  ==> P (x#xs) (Suc i) |]
 ==> P xs i"
by (induct xs arbitrary: i) (case_tac x, auto)+

lemma nonDisjointUnionEnv_conmutative: 
  "def_nonDisjointUnionEnv G G' ==> (G ⊗ G') = (G' ⊗ G)"
apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def)
apply (rule ext)
by (simp add: def_nonDisjointUnionEnv_def,clarsimp)

lemma nonDisjointUnionEnv_assoc: 
  "(G1 ⊗ G2) ⊗  G3 = G1 ⊗ (G2 ⊗  G3)"
apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def)
apply (rule ext, auto)
 apply (split split_if_asm, simp, simp)
 apply (split split_if_asm, simp,simp)
by (split split_if_asm, simp, simp add: dom_def)

lemma nonDisjointUnionEnv_disjointUnionEnv_assoc: 
  "(G1 ⊗ G2) +  G3 = G1 ⊗ (G2 +  G3)"
apply (simp add: nonDisjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
apply (rule ext, auto)
 apply (split split_if_asm, simp, simp)
 apply (split split_if_asm, simp,simp)
by (split split_if_asm, simp, simp add: dom_def)

lemma foldl_prop1: 
  "foldl op ⊗ (G' ⊗ G) Gs = G' ⊗ foldl op ⊗ G Gs"
apply (induct Gs arbitrary: G)
 apply simp
by (simp_all add: nonDisjointUnionEnv_assoc)

lemma foldl_prop2: 
  "foldl op ⊗ (G' ⊗ G) Gs + G'' = G' ⊗ foldl op ⊗ G Gs + G''"
apply (induct Gs arbitrary: G)
apply (simp_all add: nonDisjointUnionEnv_assoc)
by (rule nonDisjointUnionEnv_disjointUnionEnv_assoc)

lemma union_dom_nonDisjointUnionEnv:
" dom (A ⊗ B) = dom A ∪ dom B"
apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def,auto)
by (split split_if_asm,simp_all)

lemma union_dom_nonDisjointUnionEnv_disjointUnionEnv:
" dom (A ⊗ B +  [x \<mapsto> m]) = dom A ∪ dom (B +  [x \<mapsto> m])"
apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def, auto)
apply (split split_if_asm,simp)
by simp

lemma def_nonDisjointUnionEnvList_prop1:
"def_nonDisjointUnionEnvList (x # xs) --> def_nonDisjointUnionEnv x (foldl op ⊗ empty xs)"
by (simp add: Let_def)

lemma dom_foldl_monotone:
  " dom (foldl op ⊗ (empty ⊗ snd a) (map snd assert)) = 
    dom (snd a) ∪  dom (foldl op ⊗ empty (map snd assert))"
apply (subgoal_tac "empty ⊗ snd a = snd a ⊗ empty",simp)
 apply (subgoal_tac "foldl op ⊗ (snd a ⊗ empty) (map snd assert) = 
                     (snd a) ⊗ foldl op ⊗ empty (map snd assert)",simp)
  apply (rule union_dom_nonDisjointUnionEnv)
 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd a)")
 apply (erule nonDisjointUnionEnv_conmutative)
by (simp add: def_nonDisjointUnionEnv_def)

lemma dom_foldl_disjointUnionEnv_monotone:
  " dom (foldl op ⊗ (empty ⊗ snd a) (map snd assert) + [x \<mapsto> d'']) = 
    dom (snd a) ∪  dom (foldl op ⊗ empty (map snd assert)) ∪ dom  [x \<mapsto> d'']"
apply (subgoal_tac "empty ⊗ snd a = snd a ⊗ empty",simp)
 apply (subgoal_tac "foldl op ⊗ (snd a ⊗ empty) (map snd assert) = 
                     (snd a) ⊗ foldl op ⊗ empty (map snd assert)",simp)
  apply (subst dom_disjointUnionEnv_monotone)
  apply (subst union_dom_nonDisjointUnionEnv)
  apply simp
 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd a)")
 apply (erule nonDisjointUnionEnv_conmutative)
by (simp add: def_nonDisjointUnionEnv_def)


lemma dom_monotone:
" length assert > i ==> dom (snd (assert ! i)) ⊆ dom (foldl op ⊗ empty (map snd assert))"
apply (induct assert i rule: list_induct3, simp_all)
apply (subgoal_tac " dom (foldl op ⊗ (empty ⊗ snd x) (map snd xs)) = 
                     dom (snd x) ∪  dom (foldl op ⊗ empty (map snd xs))",simp)
apply blast
apply (rule dom_foldl_monotone)
apply (subgoal_tac " dom (foldl op ⊗ (empty ⊗ snd x) (map snd xs)) = 
                     dom (snd x) ∪  dom (foldl op ⊗ empty (map snd xs))",simp)
apply blast
by (rule dom_foldl_monotone)

lemma dom_monotone_foldl_nonDijointUnionEnv:
 "length assert > i ==> dom (snd (assert ! i)) ⊆ dom (foldl op ⊗ empty (map snd assert) + [x \<mapsto> d''])"
apply (induct assert i rule: list_induct3, simp_all)
apply (subgoal_tac " dom (foldl op ⊗ (empty ⊗ snd xa) (map snd xs) + [x \<mapsto> d'']) = 
                     dom (snd xa) ∪  dom (foldl op ⊗ empty (map snd xs)) ∪ dom [x \<mapsto> d'']",simp)
apply blast
apply (rule dom_foldl_disjointUnionEnv_monotone)
apply (subgoal_tac " dom (foldl op ⊗ (empty ⊗ snd xa) (map snd xs) + [x \<mapsto> d'']) = 
                     dom (snd xa) ∪  dom (foldl op ⊗ empty (map snd xs)) ∪ dom [x \<mapsto> d'']",simp)
 apply (subgoal_tac "dom (foldl op ⊗ empty (map snd xs) + [x \<mapsto> d'']) =
                     dom (foldl op ⊗ empty (map snd xs)) ∪ dom [x \<mapsto> d'']",simp)
  apply blast
 apply (rule dom_disjointUnionEnv_monotone)
by (rule dom_foldl_disjointUnionEnv_monotone)



lemma dom_Γi_subseteq_dom_Γ_case:
" length assert > 0 ==> 
  (∀i< length assert. dom (snd (assert ! i)) ⊆ 
                      dom (foldl op ⊗ empty (map snd assert)))"
apply (induct assert)
 apply simp
apply (case_tac "assert = []")
 apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def,simp)
apply (rule allI)
apply (subgoal_tac " dom (foldl op ⊗ (empty ⊗ snd a) (map snd assert)) = 
                     dom (snd a) ∪  dom (foldl op ⊗ empty (map snd assert))",simp)
 apply (case_tac i)
  apply (simp,blast)
 apply simp
 apply (erule_tac x="nat" in allE)
apply (blast,simp)
apply (subgoal_tac "empty ⊗ snd a = snd a ⊗ empty",simp)
 apply (subgoal_tac "foldl op ⊗ (snd a ⊗ empty) (map snd assert) = 
                     (snd a) ⊗ foldl op ⊗ empty (map snd assert)",simp)
  apply (rule union_dom_nonDisjointUnionEnv)
 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd a)")
 apply (erule nonDisjointUnionEnv_conmutative)
by (simp add: def_nonDisjointUnionEnv_def)


lemma dom_Γi_subseteq_dom_Γ_cased:
" length assert > 0 ==> 
  (∀i< length assert. dom (snd (assert ! i)) ⊆ dom (foldl op ⊗ empty (map snd assert) + [x \<mapsto> d'']))"
apply (induct assert)
 apply simp
apply (case_tac "assert = []")
 apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def)
 apply (simp add: disjointUnionEnv_def add: unionEnv_def, clarsimp)
apply (rule allI)
apply (subgoal_tac " dom (foldl op ⊗ (empty ⊗ snd a) (map snd assert) + [x \<mapsto> d'']) = 
                     dom (snd a) ∪  dom (foldl op ⊗ empty (map snd assert) + [x \<mapsto> d''])",simp)
 apply (case_tac i)
  apply (simp,blast)
 apply simp
 apply (erule_tac x="nat" in allE)
apply (blast,simp)  
apply (subgoal_tac "empty ⊗ snd a = snd a ⊗ empty",simp)
 apply (subgoal_tac "foldl op ⊗ (snd a ⊗ empty) (map snd assert) + [x \<mapsto> d''] = 
                     (snd a) ⊗ foldl op ⊗ empty (map snd assert) + [x \<mapsto> d'']",simp)
  apply (rule union_dom_nonDisjointUnionEnv_disjointUnionEnv)
 apply (rule foldl_prop2)
apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd a)")
 apply (erule nonDisjointUnionEnv_conmutative)
by (simp add: def_nonDisjointUnionEnv_def)


lemma nonDisjointUnionEnv_prop1: 
  "(G ⊗ G') z = Some m ==> G z = Some m ∨ (z ∉ dom G ∧ G' z = Some m)"
apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def)
by (split split_if_asm,simp_all)


lemma nonDisjointUnionEnv_prop2: 
  "[| def_nonDisjointUnionEnv G G'; (G ⊗ G') z = Some m |] 
  ==> G' z = Some m ∨ (z ∉ dom G' ∧ G z = Some m)"
apply (frule nonDisjointUnionEnv_conmutative,simp) 
by (erule nonDisjointUnionEnv_prop1)

lemma nonDisjointUnionEnv_prop5: 
  "[| x ∈ dom G; G x ≠ Some m |] ==> (G ⊗ G') x ≠ Some m"
by (simp add: nonDisjointUnionEnv_def add: unionEnv_def)

lemma nonDisjointUnionEnv_prop6: 
  "[| def_nonDisjointUnionEnv G G'; z ∈ dom G'; G' z ≠ Some m |] ==> (G ⊗ G') z ≠ Some m"
apply (simp add: def_nonDisjointUnionEnv_def)
apply (erule_tac x="z" in ballE)
 apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def)
by (simp add: nonDisjointUnionEnv_def add: unionEnv_def)

lemma nonDisjointUnionEnv_prop6_1: 
  "[| x ∈ dom G; G x = Some m |] ==> (G ⊗ G') x = Some m"
by (simp add: nonDisjointUnionEnv_def add: unionEnv_def)

lemma nonDisjointUnionEnv_prop6_2: 
  "[| def_nonDisjointUnionEnv G G'; G' z = Some m |] ==> (G ⊗ G') z = Some m"
apply (simp add: def_nonDisjointUnionEnv_def)
apply (erule_tac x="z" in ballE)
 apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def)
apply (simp add: nonDisjointUnionEnv_def add: unionEnv_def)
by (rule impI, simp, simp add: dom_def)


lemma Otimes_prop1:
  "i < length (map snd assert) --> 
   length (map snd assert) > 0 --> 
   def_nonDisjointUnionEnvList (map snd assert) -->  
   foldl op ⊗ empty (map snd assert) z = Some d'' -->
   z ∈ dom (snd (assert ! i)) -->
   (snd (assert ! i)) z = Some d''"
apply (induct assert i rule: list_induct3, simp_all)
 apply (intro impI)
 apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd x)") 
  prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
 apply (subgoal_tac "(empty ⊗ (snd x)) = ((snd x) ⊗ empty)" ,simp) 
  prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
 apply (subgoal_tac "foldl op ⊗ (snd x ⊗ empty) (map snd xs) = 
                     (snd x) ⊗ foldl op ⊗ empty (map snd xs)",simp)
  prefer 2 apply (rule foldl_prop1)
 apply (frule nonDisjointUnionEnv_prop1)
 apply (erule disjE) 
  apply (simp add: dom_def)
apply (simp,intro impI,simp)
apply (case_tac "xs=[]",simp)
apply (simp add: Let_def)
apply (elim conjE)
apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd x)")
 prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
apply (subgoal_tac "(empty ⊗ snd x) = (snd x ⊗ empty)",simp)
 prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
apply (subgoal_tac "foldl op ⊗ (snd x ⊗ empty) (map snd xs) = 
                    snd x ⊗ foldl op ⊗ empty (map snd xs)",simp)
 prefer 2 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnvList (snd x # (map snd xs)) --> 
                    def_nonDisjointUnionEnv (snd x) (foldl op ⊗ empty (map snd xs))",simp)
 prefer 2 apply (rule def_nonDisjointUnionEnvList_prop1)
apply (frule_tac G="snd x" and G'="foldl op ⊗ empty (map snd xs)" in nonDisjointUnionEnv_prop2,simp)
apply (erule disjE) 
 apply simp
apply (elim conjE)
apply (subgoal_tac " dom (snd (xs ! i)) ⊆ dom (foldl op ⊗ empty (map snd xs))")
 prefer 2 apply (rule dom_monotone,blast)
by blast

lemma Otimes_prop2 [rule_format]:
"  i < length (map snd assert) --> 
   length (map snd assert) > 0 --> 
   def_nonDisjointUnionEnvList (map snd assert) -->  
   x ∈ dom (snd (assert ! i)) -->
   snd (assert ! i) x ≠ Some s'' -->
   foldl op ⊗ empty (map snd assert) x ≠ Some s''"
apply (induct assert i rule: list_induct3, simp_all)
 apply (intro impI)
 apply (simp add: Let_def)
 apply (elim conjE)
 apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd xa)") 
  prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
 apply (subgoal_tac "(empty ⊗ (snd xa)) = ((snd xa) ⊗ empty)",simp)
  prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
 apply (subgoal_tac "foldl op ⊗ (snd xa ⊗ empty) (map snd xs) = 
                     (snd xa) ⊗ foldl op ⊗ empty (map snd xs)",simp)
  prefer 2 apply (rule foldl_prop1)
 apply (rule nonDisjointUnionEnv_prop5,assumption+)
apply (intro impI,simp)
apply (case_tac "xs=[]",simp)
apply (simp add: Let_def)
apply (elim conjE)
apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd xa)") 
 prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
apply (subgoal_tac "(empty ⊗ snd xa) = (snd xa ⊗ empty)",simp)
 prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
apply (subgoal_tac "foldl op ⊗ (snd xa ⊗ empty) (map snd xs) = 
                    snd xa ⊗ foldl op ⊗ empty (map snd xs)",simp)
 prefer 2 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnvList (snd xa # (map snd xs)) --> 
                    def_nonDisjointUnionEnv (snd xa) (foldl op ⊗ empty (map snd xs))",simp)
 prefer 2 apply (rule def_nonDisjointUnionEnvList_prop1)
apply (subgoal_tac " dom (snd (xs ! i)) ⊆ dom (foldl op ⊗ empty (map snd xs))")
 prefer 2 apply (rule dom_monotone,simp)
apply (subgoal_tac "x ∈ dom (foldl op ⊗ empty (map snd xs))")
 prefer 2 apply blast
by (rule nonDisjointUnionEnv_prop6,assumption+)


lemma Otimes_prop3:
"  i < length (map snd assert) --> 
   length (map snd assert) > 0 --> 
   def_nonDisjointUnionEnvList (map snd assert) -->  
   snd (assert ! i) x = Some m -->
   foldl op ⊗ empty (map snd assert) x = Some m"
apply (induct assert i rule: list_induct3, simp_all)
 apply (intro impI)
 apply (simp add: Let_def)
 apply (elim conjE)
 apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd xa)") 
  prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
 apply (subgoal_tac "(empty ⊗ (snd xa)) = ((snd xa) ⊗ empty)",simp) 
  prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
 apply (subgoal_tac "foldl op ⊗ (snd xa ⊗ empty) (map snd xs) = 
                     (snd xa) ⊗ foldl op ⊗ empty (map snd xs)",simp)
  prefer 2 apply (rule foldl_prop1)
 apply (rule nonDisjointUnionEnv_prop6_1, simp add: dom_def, assumption+)
apply (intro impI,simp)
apply (case_tac "xs=[]",simp)
apply (simp add: Let_def)
apply (elim conjE)
apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd xa)") 
 prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
apply (subgoal_tac "(empty ⊗ snd xa) = (snd xa ⊗ empty)",simp) 
 prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
apply (subgoal_tac "foldl op ⊗ (snd xa ⊗ empty) (map snd xs) = 
                    snd xa ⊗ foldl op ⊗ empty (map snd xs)",simp)
 prefer 2 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnvList (snd xa # (map snd xs)) --> 
                    def_nonDisjointUnionEnv (snd xa) (foldl op ⊗ empty (map snd xs))",simp)
 prefer 2 apply (rule def_nonDisjointUnionEnvList_prop1)
apply (subgoal_tac " dom (snd (xs ! i)) ⊆ dom (foldl op ⊗ empty (map snd xs))")
 prefer 2 apply (rule dom_monotone,simp)
apply (subgoal_tac "x ∈ dom (foldl op ⊗ empty (map snd xs))")
 prefer 2 apply blast
by (rule nonDisjointUnionEnv_prop6_2,assumption+)


lemma nonDisjointUnionEnv_disjointUnionEnv_prop1: 
  "[| x ∈ dom G; G x ≠ Some m |] ==> ((G ⊗ G') + G'') x ≠ Some m"
apply (simp add: nonDisjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
apply (rule impI, auto)
apply (split split_if_asm, simp add: dom_def)
by (simp add: dom_def)


lemma nonDisjointUnionEnv_disjointUnionEnv_prop2:
  "[| def_nonDisjointUnionEnv G G'; z ∈ dom G'; G' z ≠ Some m |] ==> ((G ⊗ G') + G'') z ≠ Some m"
apply (simp add: def_nonDisjointUnionEnv_def)
apply (erule_tac x="z" in ballE)
 apply (simp add: nonDisjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def) 
 apply (rule impI, auto)
apply (simp add: nonDisjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def) 
by (split split_if_asm, simp add: dom_def,auto)

lemma nonDisjointUnionEnv_disjointUnionEnv_prop3: 
  "[| x ∈ dom G; G x = Some m |] ==> ((G ⊗ G') + G'') x = Some m"
apply (simp add: nonDisjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
by (rule impI,auto)

lemma nonDisjointUnionEnv_disjointUnionEnv_prop4: 
  "[| def_nonDisjointUnionEnv G G'; G' z = Some m |] ==> ((G ⊗ G') + G'') z = Some m"
apply (simp add: def_nonDisjointUnionEnv_def)
apply (erule_tac x="z" in ballE)
 apply (simp add: nonDisjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
 apply (rule impI,auto)
apply (simp add: nonDisjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
apply (split split_if_asm,auto)
by (split split_if_asm,auto) 


lemma Otimes_prop2_not_s [rule_format]:
"  i < length (map snd assert) --> 
   length (map snd assert) > 0 --> 
   def_nonDisjointUnionEnvList (map snd assert) -->  
   y ∈ dom (snd (assert ! i)) -->
   snd (assert ! i) y ≠ Some s'' -->
   (foldl op ⊗ empty (map snd assert) + [x \<mapsto> d'']) y ≠ Some s''"
apply (induct assert i rule: list_induct3, simp_all)
 apply (intro impI)
 apply (simp add: Let_def)
 apply (elim conjE)
 apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd xa)") 
  prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
 apply (subgoal_tac "(empty ⊗ (snd xa)) = ((snd xa) ⊗ empty)",simp)
  prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
 apply (subgoal_tac "foldl op ⊗ (snd xa ⊗ empty) (map snd xs) = 
                     (snd xa) ⊗ foldl op ⊗ empty (map snd xs)",simp)
  prefer 2 apply (rule foldl_prop1)
 apply (rule nonDisjointUnionEnv_disjointUnionEnv_prop1,assumption+)
apply (intro impI,simp)
apply (case_tac "xs=[]",simp)
apply (simp add: Let_def)
apply (elim conjE)
apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd xa)") 
 prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
apply (subgoal_tac "(empty ⊗ snd xa) = (snd xa ⊗ empty)",simp)
 prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
apply (subgoal_tac "foldl op ⊗ (snd xa ⊗ empty) (map snd xs) = 
                    snd xa ⊗ foldl op ⊗ empty (map snd xs)",simp)
 prefer 2 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnvList (snd xa # (map snd xs)) --> 
                    def_nonDisjointUnionEnv (snd xa) (foldl op ⊗ empty (map snd xs))",simp)
 prefer 2 apply (rule def_nonDisjointUnionEnvList_prop1)
apply (subgoal_tac " dom (snd (xs ! i)) ⊆ dom (foldl op ⊗ empty (map snd xs))")
 prefer 2 apply (rule dom_monotone,simp)
apply (subgoal_tac "y ∈ dom (foldl op ⊗ empty (map snd xs))")
 prefer 2 apply blast
apply (rule nonDisjointUnionEnv_disjointUnionEnv_prop2,assumption+)
by (simp add: disjointUnionEnv_def add: unionEnv_def)


lemma Otimes_prop4 [rule_format]:
"  i < length (map snd assert) --> 
   length (map snd assert) > 0 --> 
   def_nonDisjointUnionEnvList (map snd assert) -->  
   snd (assert ! i) xa = Some m -->
   (foldl op ⊗ empty (map snd assert) + [x \<mapsto> d'']) xa = Some m"
apply (induct assert i rule: list_induct3, simp_all)
 apply (intro impI)
 apply (simp add: Let_def)
 apply (elim conjE)
 apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd xb)") 
  prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
 apply (subgoal_tac "(empty ⊗ (snd xb)) = ((snd xb) ⊗ empty)",simp) 
  prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
 apply (subgoal_tac "foldl op ⊗ (snd xb ⊗ empty) (map snd xs) = 
                     (snd xb) ⊗ foldl op ⊗ empty (map snd xs)",simp)
  prefer 2 apply (rule foldl_prop1)
 apply (rule nonDisjointUnionEnv_disjointUnionEnv_prop3, simp add: dom_def, assumption+)
apply (intro impI,simp)
apply (case_tac "xs=[]",simp)
apply (simp add: Let_def)
apply (elim conjE)
apply (subgoal_tac "def_nonDisjointUnionEnv empty (snd xb)") 
 prefer 2 apply (simp add: def_nonDisjointUnionEnv_def)
apply (subgoal_tac "(empty ⊗ snd xb) = (snd xb ⊗ empty)",simp) 
 prefer 2 apply (rule nonDisjointUnionEnv_conmutative,simp)
apply (subgoal_tac "foldl op ⊗ (snd xb ⊗ empty) (map snd xs) = 
                    snd xb ⊗ foldl op ⊗ empty (map snd xs)",simp)
 prefer 2 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnvList (snd xb # (map snd xs)) --> 
                    def_nonDisjointUnionEnv (snd xb) (foldl op ⊗ empty (map snd xs))",simp)
 prefer 2 apply (rule def_nonDisjointUnionEnvList_prop1)
apply (subgoal_tac " dom (snd (xs ! i)) ⊆ dom (foldl op ⊗ empty (map snd xs))")
 prefer 2 apply (rule dom_monotone,simp)
apply (subgoal_tac "xa ∈ dom (foldl op ⊗ empty (map snd xs))")
 prefer 2 apply blast
apply (rule nonDisjointUnionEnv_disjointUnionEnv_prop4,assumption)
by (simp add: disjointUnionEnv_def add: unionEnv_def)

text{*
Lemmas for nonDisjointUnionSafeEnv operator
*}

lemma empty_nonDisjointUnionSafeEnv :
  "empty ⊕ A = A"
by (simp add: nonDisjointUnionSafeEnv_def add: unionEnv_def)



text{*
Lemmas for triangle operator
*}

lemma safe_triangle:  
  "[| (def_pp Γ1 Γ2 L2); Γ2 x = Some s''|]  ==> (pp Γ1 Γ2 L2) x =  Some s''"
apply (simp add: pp_def add: def_pp_def add: safe_def add: unsafe_def)
apply (erule conjE)
apply (erule_tac x="x" in allE)+
apply auto
by (case_tac "y", simp+)

lemma safe_Gamma2_triangle: 
  "[|def_pp Γ1 Γ2 L2; Γ2 x = Some s''; x ∈ L2|] ==> Γ1 x = Some s'' ∨ x ∉ dom Γ1"
apply (simp add: def_pp_def)
apply (erule conjE)+
apply (erule_tac x="x" in allE)+
apply (simp add: unsafe_def,auto)
by (case_tac "y", simp_all)

lemma unsafe_triangle: 
  "[|def_pp Γ1 Γ2 L2; 
    def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
    L2 ⊆ dom (disjointUnionEnv Γ2  (empty(x1 \<mapsto> m)));
    x ≠ x1;
    Γ2 x ≠ Some s''; x ∈ L2|]  ==> (pp Γ1 Γ2 L2) x ≠  Some s''"
apply (simp add: def_pp_def)
apply (elim conjE)
apply (erule_tac x="x" in allE,clarsimp)+
apply (simp add: unsafe_def add: pp_def)
apply (split split_if_asm,clarsimp)
apply (simp add: safe_def)
apply (erule conjE)
apply (subgoal_tac "[| x ≠ x1; x ∈ L2; L2 ⊆ dom (Γ2 + [x1 \<mapsto> m])|]  ==> x ∈ dom Γ2",clarsimp)
apply (subgoal_tac "dom (disjointUnionEnv Γ2 [x1 \<mapsto> m]) = dom Γ2  ∪ dom [x1 \<mapsto> m]",simp)
 apply blast
by (rule union_dom_disjointUnionEnv,assumption)

lemma safe_Gamma_triangle_3: 
 "[|def_pp Γ1 Γ2 L2;  
   def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
   L2 ⊆ dom (disjointUnionEnv Γ2  (empty(x1 \<mapsto> m)));
   x ≠ x1;
   Γ2  x ≠  Some s''; 
   x∈ L2|] 
  ==> Γ1 x = Some s'' ∨ x ∉ dom Γ1"
apply (frule unsafe_triangle,assumption+)
apply (simp add: pp_def)
apply (split split_if_asm,clarsimp)
 apply (simp add: safe_def,clarsimp)
apply (simp add: safe_def add: def_pp_def)
apply (erule conjE)
apply (erule_tac x="x" in allE, simp)
apply (simp add: unsafe_def, clarsimp)
by (case_tac "y",simp_all)

lemma unsafe_Gamma2_triangle: 
  "[| def_pp  Γ1 Γ2 L2; (Γ2 + [x1 \<mapsto> m]) y ≠ Some s''; y ≠ x1 |] ==> Γ2 y ≠ Some  s''"
apply (simp add: disjointUnionEnv_def add: unionEnv_def)
apply (split split_if_asm)
 apply simp
apply (simp add: def_pp_def)
by auto

lemma condemned_Gamma2_triangle: 
  "[|def_pp  Γ1 Γ2 L2; (Γ2 + [x1 \<mapsto> s'']) x = Some d''|]  ==> (pp Γ1 Γ2 L2) x = Some d''"
apply (simp add: disjointUnionEnv_def add: unionEnv_def)
apply (split split_if_asm)
 apply (simp add: pp_def add: def_pp_def, clarsimp)
 apply (simp add: safe_def add: unsafe_def)
 apply (erule_tac x="x" in allE)+ apply (simp add: dom_def)
 apply (case_tac "ya", simp_all) 
apply (split split_if_asm)
 apply simp
by simp

lemma unsafe_triangle_unsafe_2: 
  "[| def_pp Γ1 Γ2 L2; (pp Γ1 Γ2 L2) x = Some d'' |] ==> Γ2 x ≠ Some s''"
apply (simp add: pp_def)
apply (split split_if_asm)
 apply (simp add: safe_def)
apply (simp add: safe_def)
apply (simp add: def_pp_def)
apply (simp add: unsafe_def)
by auto

lemma triangle_d_Gamma1_s_or_not_dom_Gamma1: 
  "[|def_disjointUnionEnv Γ2  (empty(x1 \<mapsto> m));
    L1 ⊆ dom Γ1; 
    L2 ⊆ dom (disjointUnionEnv Γ2  (empty(x1 \<mapsto> m))); 
    z ≠ x1;
    def_pp Γ1 Γ2 L2 ;(pp Γ1 Γ2 L2) z = Some d''; z ∈ L2 |]  
   ==> (Γ1 z = Some s'' ∨ z ∉ dom Γ1)"
apply (subgoal_tac "Γ2 z = Some d''");
 apply (subgoal_tac "z ∈ dom Γ2")
  prefer 2 apply blast
 apply (simp add: pp_def)
 apply (case_tac "z∈ L1")
  apply (rule disjI1)
  apply (subgoal_tac "z ∈ dom Γ1")
   prefer 2 apply blast
  apply (simp add: safe_def)
  apply (split split_if_asm, simp, simp)
  apply (simp add: def_pp_def)
  apply auto
  apply (erule_tac x="z" in allE)+
  apply simp
  apply (simp add: unsafe_def, auto)
 apply (simp add: safe_def)
 apply (split split_if_asm, simp)
  apply (simp add: def_pp_def, auto)
 apply (simp add: def_pp_def, auto)
 apply (simp add: unsafe_def, auto)
apply (simp add: def_pp_def)
apply (subgoal_tac "z ∈ dom Γ2")
 apply (erule conjE)
 apply (erule_tac x="z" in allE)+
 apply simp
 apply (simp add: unsafe_def add: pp_def)
 apply (split split_if_asm, simp, simp)
apply (subgoal_tac "dom (Γ2 + [x1 \<mapsto> m]) = dom Γ2 ∪ dom [x1 \<mapsto> m]") 
 prefer 2 apply (rule union_dom_disjointUnionEnv) apply simp
apply (subgoal_tac "dom [x1 \<mapsto> m] = {x1}",simp) 
 apply blast
by simp

lemma triangle_d_Gamma1_s_Gamma2_d: 
  "[|(pp Γ1 Γ2 L2) z = Some d'';  Γ1 z = Some s''|] ==> Γ2 z = Some d''"
apply (simp add: pp_def)
apply (split split_if_asm)
 apply simp
by simp

lemma triangle_prop: 
  "[|x ∈ dom Γ1; Γ1 x ≠ Some  s''|] 
   ==>  x ∈ dom (pp Γ1 Γ2 L2) ∧ (pp Γ1 Γ2 L2) x ≠ Some  s''"
by (simp add: pp_def, simp add: dom_def add: safe_def)

lemma triangle_d_Gamma1_d_or_Gamma2_d: 
  "[|(pp Γ1 Γ2 L2) z = Some d''|] ==> Γ1 z  = Some d'' ∨ Γ2 z = Some d''"
apply (simp add: pp_def add: safe_def)
apply (split split_if_asm)
 apply simp
by simp


lemma triangle_d_Gamma2_d_Gamma1_s: 
  "[|L1 ⊆ dom Γ1;
    def_pp Γ1 Γ2 L2; 
    (pp Γ1 Γ2 L2) z = Some d''; 
    Γ2 z = Some d''; z ∈ L1|] 
   ==> Γ1 z  = Some s'' ∧ z ∈ L2"
apply (subgoal_tac "z ∈ dom Γ1")
 prefer 2 apply (erule set_mp, assumption)
apply (rule conjI)
 apply (simp add: pp_def)
 apply (split split_if_asm)
  apply (simp_all add: safe_def)
 apply (simp add: def_pp_def)
 apply (erule conjE)
 apply (erule_tac x="z" in allE)+
 apply (simp add: unsafe_def)
 apply (erule conjE)
 apply (simp add: dom_def)
apply (simp add: def_pp_def)
apply (erule conjE)+
apply (erule_tac x="z" in allE,simp)+
by (simp add: unsafe_def add: pp_def add: safe_def,clarsimp)



lemma Gamma2_d_disjointUnionEnv_m_d: 
  "[|def_disjointUnionEnv  Γ2  (empty(x1 \<mapsto> m)); 
    Γ2 z = Some d''|]
   ==>  (disjointUnionEnv Γ2  (empty(x1 \<mapsto> m))) z = Some d''"
by (simp add: disjointUnionEnv_def unionEnv_def def_disjointUnionEnv_def, auto)


lemma dom_Gamma1_dom_triangle: 
  "x∈ dom Γ1 ==> x ∈  dom (pp Γ1 Γ2 L2)"
by (simp add: pp_def,auto)


lemma safe_triangle_safe_Gamma1: 
  "[| (pp Γ1 Γ2 L2) x = Some s'';  x ∈ dom Γ1 |] ==> Γ1 x = Some s''"
apply (simp add: pp_def)
apply (split split_if_asm)
 apply (simp add: safe_def)
by simp


lemma dom_Gamma2_dom_triangle: 
  "[| x ≠ x1; x ∈ dom (Γ2 + [x1 \<mapsto> m]) |]  ==> x ∈  dom (pp Γ1 Γ2 L2)"
apply (simp add: pp_def add: disjointUnionEnv_def add: unionEnv_def,clarsimp)
apply (split split_if_asm)
 apply (simp add: safe_def add: dom_def)
by simp

lemma usafe_Gamma2_unsafe_triangle: 
  "[|x≠x1;  
    x ∈ dom (Γ2 + [x1 \<mapsto> m]); 
    (Γ2 + [x1 \<mapsto> m]) x ≠ Some s''|]  
   ==> (pp Γ1 Γ2 L2) x ≠ Some s''"
apply (simp add: pp_def add: disjointUnionEnv_def add: unionEnv_def,clarsimp)
apply (split split_if_asm)
 apply (simp add: safe_def add: dom_def)
by simp


lemma def_disjointUnionEnv_monotone: 
  "def_disjointUnionEnv Γ2 [x1 \<mapsto> d''] ==> (Γ2 + [x1 \<mapsto> d'']) x1 = Some d''"
by (simp add: def_disjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)


lemma disjointUnionEnv_d_Gamma2_d: 
  "[|def_disjointUnionEnv Γ2 [x1 \<mapsto> d'']; 
    (Γ2 + [x1 \<mapsto> d'']) z = Some d''; 
    z≠ x1|]
   ==> Γ2 z = Some d''"
apply (simp add: disjointUnionEnv_def add: unionEnv_def)
apply (split split_if_asm,clarsimp)
by (simp add: def_disjointUnionEnv_def)


lemma Gamma2_d_disjointUnionEnv_d: 
  "[|def_disjointUnionEnv Γ2 [x1 \<mapsto> d'']; 
    Γ2 z = Some d''|]
  ==>  (Γ2 + [x1 \<mapsto> d'']) z = Some d''"
by (simp add: disjointUnionEnv_def unionEnv_def def_disjointUnionEnv_def, auto)


lemma dom_disjointUnionEnv_subset_dom_extend: 
  "[|def_disjointUnionEnv Γ2 [x1 \<mapsto> d'']; 
    dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) ⊆ dom (E1(x1 \<mapsto> v1)); 
   (Γ2 + [x1 \<mapsto> d'']) x = Some s''|]  
   ==> x ∈ dom E1"
apply (simp add: disjointUnionEnv_def add: unionEnv_def)
apply (subgoal_tac "x≠x1")
 apply blast
apply (simp add: def_disjointUnionEnv_def)
apply (split split_if_asm,clarsimp,simp)
by (split split_if_asm,clarsimp, simp)

lemma Gamma2_d_triangle_d: 
  "[|def_pp  Γ1 Γ2 L2; Γ2 x = Some d''|] ==> (pp Γ1 Γ2 L2) x = Some d''"
apply (simp add: pp_def add: def_pp_def, clarsimp)
 apply (simp add: safe_def add: unsafe_def)
 apply (erule_tac x="x" in allE)+ apply (simp add: dom_def)
apply (elim conjE)
 apply (case_tac "y", simp_all) 
done

lemma disjounitUnionEnv_d_triangle_d: 
  "[|x≠x1;def_pp  Γ1 Γ2 L2; (Γ2 + [x1 \<mapsto> d'']) x = Some d''|]  ==> (pp Γ1 Γ2 L2) x = Some d''"
apply (simp add: disjointUnionEnv_def add: unionEnv_def)
apply (split split_if_asm)
 apply (simp add: pp_def add: def_pp_def, clarsimp)
 apply (simp add: safe_def add: unsafe_def)
 apply (erule_tac x="x" in allE)+ apply (simp add: dom_def)
 apply (case_tac "ya", simp_all) 
done


(********** CASE **************)
(*declare dom_fun_upd [simp del]*)





end