Theory SafeDAss_P3

(*  Title:      Safe DAss P3
    Author:     Javier de Dios and Ricardo Peña
    Copyright:  March 2008, Universidad Complutense de Madrid
*)


header {* Derived Assertions. P3. L   dom G  *}

theory SafeDAss_P3 imports SafeDAssBasic
begin

(* Demostracion de  L ⊆ dom Γ *)

text{*
Lemmas for LET
*}

lemma dom_Γ2_subseteq_triangle_Γ1_Γ2_L2: 
  "dom Γ2  ⊆ dom (pp Γ1 Γ2 L2)"
by (simp add: pp_def, clarsimp)

lemma set_atom2var_as_subeteq_Γ1:
  "∀a∈set as. atom a
   ==> set (map atom2var as) ⊆  
       dom (map_of (zip (map atom2var as) (replicate (length as) s'')))"
apply (induct as,simp,clarsimp)
apply (case_tac a,simp_all)
by force

lemma P3_LET_e1: 
  "[|L1 ⊆ dom Γ1|] 
  ==> L1 ⊆ dom (pp Γ1 Γ2 L2)"
by (simp add: pp_def, auto)

lemma P3_LET_e2: 
  "[|def_disjointUnionEnv  Γ2  (empty(x1 \<mapsto> m));
    L2 ⊆  dom (disjointUnionEnv Γ2  (empty(x1 \<mapsto> m)))|] 
  ==> L2 - {x1} ⊆ dom (pp Γ1 Γ2 L2)"
apply (rule subsetI)
apply (frule union_dom_disjointUnionEnv)
apply (simp add: def_disjointUnionEnv_def)
apply (subgoal_tac "dom Γ2  ⊆ dom (pp Γ1 Γ2 L2)",blast)
by (rule dom_Γ2_subseteq_triangle_Γ1_Γ2_L2)

lemma P3_LET: 
  "[| def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
     L1 ⊆ dom Γ1;  
     L2 ⊆ dom (disjointUnionEnv Γ2  (empty(x1 \<mapsto> m)))|] 
    ==> L1 ∪ (L2 - {x1}) ⊆ dom (pp Γ1 Γ2 L2)"
apply clarsimp
apply (rule conjI)
 apply (erule P3_LET_e1)
by (erule P3_LET_e2,assumption)




text{*
Lemmas for CASE
*}

(***************** CASE *****************)

lemma P3_CASE:
"[| length assert > 0; 
   length alts = length assert; 
   (∀i < length alts. fst (assert ! i) ⊆ dom (snd (assert ! i)));
    x ∈ dom (nonDisjointUnionEnvList (map snd assert)) |] 
==> (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪ {x} ⊆ 
     dom (nonDisjointUnionEnvList (map snd assert))"
apply (frule dom_Γi_subseteq_dom_Γ_case)
by (clarsimp,blast)


text{*
Lemmas for CASED
*}


lemma P3_1_CASED:
  "[| length assert > 0; 
     length assert = length alts; 
     (∀i < length alts. fst (assert ! i) ⊆ dom (snd (assert ! i))) |] 
  ==> x ∈ dom (foldl op ⊗ empty
                 (map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li))) 
                 (zip (map (snd o extractP o fst) alts) (map snd assert))) +
                [x \<mapsto> d''])"
apply (subst dom_disjointUnionEnv_monotone)
by (simp add: dom_def)


lemma dom_restrict_neg_map:
  "dom (restrict_neg_map m A) = dom m - (dom m ∩ A)"
apply (simp add: restrict_neg_map_def)
apply auto
by (split split_if_asm,simp_all)

lemma dom_foldl_monotone_generic:
  " dom (foldl op ⊗ (empty ⊗ x) xs) = 
    dom x ∪  dom (foldl op ⊗ empty xs)"
apply (subgoal_tac "empty ⊗ x = x ⊗ empty",simp)
 apply (subgoal_tac "foldl op ⊗ (x ⊗ empty) xs = 
                     x ⊗ foldl op ⊗ empty xs",simp)
  apply (rule union_dom_nonDisjointUnionEnv)
 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnv empty x")
 apply (erule nonDisjointUnionEnv_conmutative)
by (simp add: def_nonDisjointUnionEnv_def)

lemma dom_foldl_disjointUnionEnv_monotone_generic_2:
  " dom (foldl op ⊗ (empty ⊗ y) ys + A) = 
    dom y ∪  dom (foldl op ⊗ empty ys) ∪ dom  A"
apply (subgoal_tac "empty ⊗ y = y ⊗ empty",simp)
 apply (subgoal_tac "foldl op ⊗ (y ⊗ empty) ys = 
                     y ⊗ foldl op ⊗ empty ys",simp)
  apply (subst dom_disjointUnionEnv_monotone)
  apply (subst union_dom_nonDisjointUnionEnv)
  apply simp
 apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnv empty y")
 apply (erule nonDisjointUnionEnv_conmutative)
by (simp add: def_nonDisjointUnionEnv_def)

lemma dom_Γi_in_Γcased [rule_format]:
  "length assert > 0
   --> length assert = length alts
   -->  def_disjointUnionEnv 
             (foldl op ⊗ empty
                       (map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
                         (zip (map (snd o extractP o fst) alts) (map snd assert))))
             [x \<mapsto> d'']
   --> (∀ i < length alts. y ∈ dom (snd (assert ! i)) 
   --> y ∉ set (snd (extractP (fst (alts ! i))))
   --> y ∈ dom (foldl op ⊗ empty
                       (map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
                         (zip (map (snd o extractP o fst) alts) (map snd assert))) +
                      [x \<mapsto> d'']))"
apply (induct assert alts rule:list_induct2',simp_all)
apply (rule impI)+
apply (case_tac "xs = []",simp)
 apply (rule impI)
 apply (subst empty_nonDisjointUnionEnv)
 apply (subst union_dom_disjointUnionEnv)
  apply (subst (asm) empty_nonDisjointUnionEnv)
  apply simp
 apply (subst dom_restrict_neg_map)
 apply force
apply simp
apply (drule mp)
 apply (simp add: def_disjointUnionEnv_def)
 apply (subst (asm) dom_foldl_monotone_generic)
 apply blast
apply (rule allI, rule impI)
apply (case_tac i,simp_all)
 apply (rule impI)
 apply (subst dom_foldl_disjointUnionEnv_monotone_generic_2)
 apply (subst dom_restrict_neg_map)
 apply force
apply (rule impI)
apply (rotate_tac 3)
apply (erule_tac x="nat" in allE,simp)
apply (subst dom_foldl_disjointUnionEnv_monotone_generic_2)
apply (subst (asm) union_dom_disjointUnionEnv) 
 apply (simp add: def_disjointUnionEnv_def)
 apply (subst (asm) dom_foldl_monotone_generic)
 apply blast
by blast



lemma P3_2_CASED:
  "[| length assert > 0; 
     length assert = length alts;
     def_disjointUnionEnv 
             (foldl op ⊗ empty
                       (map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
                         (zip (map (snd o extractP o fst) alts) (map snd assert))))
             [x \<mapsto> d''];
      ∀ i < length alts. ∀ j < length alts. i ≠ j --> (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j))))) = {}; 
     (∀i < length alts. fst (assert ! i) ⊆ dom (snd (assert ! i))) |] 
==> (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
       ⊆ dom (foldl op ⊗ empty
               (map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li))) 
               (zip (map (snd o extractP o fst) alts) (map snd assert))) +
              [x \<mapsto> d''])"
apply (rule subsetI,simp)
apply (rename_tac y)
apply (elim bexE, elim conjE)
apply (erule_tac x="i" in allE,simp)
apply (subgoal_tac "y ∈ dom (snd (assert ! i))")
 prefer 2 apply blast
apply (rule dom_Γi_in_Γcased) 
by (simp,assumption+)



(** APP **)

lemma union_dom_nonDisjointUnionSafeEnv:
" dom (nonDisjointUnionSafeEnv A  B) = dom A ∪ dom B"
apply (simp add: nonDisjointUnionSafeEnv_def add: unionEnv_def,auto)
by (split split_if_asm,simp_all)


lemma nonDisjointUnionSafeEnv_assoc: 
  "nonDisjointUnionSafeEnv (nonDisjointUnionSafeEnv G1 G2)  G3 = 
   nonDisjointUnionSafeEnv G1 (nonDisjointUnionSafeEnv G2  G3)"
apply (simp add: nonDisjointUnionSafeEnv_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_nonDisjointUnionSafeEnv_prop: 
  "foldl nonDisjointUnionSafeEnv (G' ⊕ G) Gs = G' ⊕ foldl op ⊕ G Gs"
apply (induct Gs arbitrary: G)
 apply simp
by (simp_all add: nonDisjointUnionSafeEnv_assoc)


lemma nonDisjointUnionSafeEnv_conmutative: 
  "def_nonDisjointUnionSafeEnv G G' ==> (G ⊕ G') = (G' ⊕ G)"
apply (simp add: nonDisjointUnionSafeEnv_def add: unionEnv_def)
apply (rule ext)
apply (simp add: def_nonDisjointUnionSafeEnv_def)
apply (simp add: safe_def)
by clarsimp


lemma dom_foldl_nonDisjointUnionSafeEnv_monotone:
  " dom (foldl nonDisjointUnionSafeEnv (empty ⊕ x) xs) = 
    dom x ∪  dom (foldl op ⊕ empty xs)"
apply (subgoal_tac "empty ⊕ x = x ⊕ empty",simp)
 apply (subgoal_tac "foldl op ⊕ (x ⊕ empty) xs = 
                     x ⊕ foldl op ⊕ empty xs",simp)
  apply (rule union_dom_nonDisjointUnionSafeEnv)
  apply (rule foldl_nonDisjointUnionSafeEnv_prop)
apply (rule nonDisjointUnionSafeEnv_conmutative)
by (simp add: def_nonDisjointUnionSafeEnv_def)

lemma nonDisjointUnionSafeEnv_empty:
  "nonDisjointUnionSafeEnv empty  x = x"
apply (simp add: nonDisjointUnionSafeEnv_def)
by (simp add: unionEnv_def)


declare dom_fun_upd [simp del]

lemma dom_atom2var_fv:
  "(∃y. x = VarE y unit)
   ==> dom [atom2var x \<mapsto> y] = fv x"
apply (case_tac x)
apply (simp_all add: atom2var.simps) 
by (simp add: dom_def)


declare nonDisjointUnionSafeEnvList.simps [simp del]


lemma atom_fvs_VarE:
  "[| (∀ a ∈ set as. atom a); xa ∈ fvs' as |] 
   ==> (∃ i < length as. ∃ a. as!i = VarE xa a)"
apply (induct as,simp_all)
 apply (case_tac a, simp_all)
by force



lemma nth_nonDisjointUnionSafeEnvList:
  "[| length xs = length ms; def_nonDisjointUnionSafeEnvList (maps_of (zip xs ms)) |] 
   ==> (∀ i < length xs . nonDisjointUnionSafeEnvList (maps_of (zip xs ms)) (xs!i) = Some (ms!i))"
apply (induct xs ms rule: list_induct2',simp_all)
apply clarsimp
apply (case_tac i)
 apply simp
 apply (simp add: nonDisjointUnionSafeEnvList.simps)
 apply (subgoal_tac "empty ⊕ [x \<mapsto> y] = [x \<mapsto> y] ⊕ empty",simp)
  apply (subgoal_tac "foldl op ⊕ ([x \<mapsto> y] ⊕ empty) (maps_of (zip xs ys)) = 
                      [x \<mapsto> y] ⊕ foldl op ⊕ empty (maps_of (zip xs ys))",simp)
   apply (simp add: nonDisjointUnionSafeEnv_def)
   apply (simp add: unionEnv_def)
   apply (simp add: dom_def)
  apply (rule foldl_nonDisjointUnionSafeEnv_prop)
 apply (subst nonDisjointUnionSafeEnv_empty)
 apply (subst nonDisjointUnionSafeEnv_conmutative)
  apply (simp add: def_nonDisjointUnionSafeEnv_def)
 apply (subst nonDisjointUnionSafeEnv_empty)
 apply simp
apply clarsimp
apply (simp add: nonDisjointUnionSafeEnvList.simps)
apply (subgoal_tac "empty ⊕ [x \<mapsto> y] = [x \<mapsto> y] ⊕ empty",simp)
 apply (subgoal_tac "foldl op ⊕ ([x \<mapsto> y] ⊕ empty) (maps_of (zip xs ys)) = 
                     [x \<mapsto> y] ⊕ foldl op ⊕ empty (maps_of (zip xs ys))",simp)
  apply (simp add: Let_def)
  apply (erule_tac x="nat" in allE,simp)
  apply (simp add: nonDisjointUnionSafeEnv_def)
  apply (simp add: unionEnv_def)
  apply (rule conjI)
   apply (rule impI)+
   apply (elim conjE)
   apply (simp add:  def_nonDisjointUnionSafeEnv_def)
   apply (erule_tac x="x" in ballE)
    apply (simp add: safe_def)
   apply (simp add: dom_def)
  apply clarsimp
 apply (rule foldl_nonDisjointUnionSafeEnv_prop) 
apply (rule nonDisjointUnionSafeEnv_conmutative) 
by (simp add: def_nonDisjointUnionSafeEnv_def)


lemma dom_nonDisjointUnionSafeEnvList_fvs:
  "[| ∀ a ∈ set xs. atom a; length xs = length ys |] 
   ==> fvs' xs ⊆  dom (nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var xs) ys)))"
apply (induct xs ys rule: list_induct2',simp_all)
apply (simp add: nonDisjointUnionSafeEnvList.simps)
apply (subst dom_foldl_nonDisjointUnionSafeEnv_monotone)
apply (rule conjI)
 apply (case_tac x, simp_all)
 apply (simp add: dom_def)
apply (subst dom_foldl_nonDisjointUnionSafeEnv_monotone)
by blast 

declare nonDisjointUnionSafeEnvList.simps [simp add]
declare def_nonDisjointUnionSafeEnvList.simps [simp add] thm dom_map_add
declare atom.simps [simp del]

lemma nonDisjointUnionSafeEnvList_prop1:
  "[| nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ; 
     xa ∈ fvs' as; Γ xa = Some y;
     def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
    (∀ a ∈ set as. atom a); length as = length ms |] 
   ==> ∃ i < length as. ∃ a. as!i = VarE xa a ∧ ms!i = y"
apply (frule atom_fvs_VarE,assumption+)
apply (elim exE, elim conjE, elim exE)
apply (rule_tac x="i" in exI,simp)
apply (simp add: map_le_def)
apply (erule_tac x="xa" in ballE,simp)
 apply (subgoal_tac "length (map atom2var as) = length ms")
  prefer 2 apply simp
 apply (frule nth_nonDisjointUnionSafeEnvList,assumption+)
 apply (erule_tac x="i" in allE,simp)
apply (frule dom_nonDisjointUnionSafeEnvList_fvs,assumption+,simp)
by blast


lemma P3_APP:
  "[| length as = length ms; ∀ a ∈ set as. atom a;
     nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ |] 
  ==> fvs' as ⊆ dom Γ"
apply (induct as ms rule: list_induct2',simp_all)
apply (elim conjE)
apply (frule map_le_implies_dom_le)
apply (frule dom_nonDisjointUnionSafeEnvList_fvs,assumption+)
apply (subgoal_tac 
  " dom (nonDisjointUnionSafeEnvList ([atom2var x \<mapsto> y] # maps_of (zip (map atom2var xs) ys))) = 
    dom [atom2var x \<mapsto> y] ∪ dom (nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var xs) ys)))")
 apply simp
 apply (rule conjI)
  apply (case_tac x,simp_all add: atom.simps) 
  apply force 
 apply force
by (rule dom_foldl_nonDisjointUnionSafeEnv_monotone)


(* APP PRIMOP *)

lemma P3_APP_PRIMOP:
  "[| Γ0 = [atom2var a1 \<mapsto> s'', atom2var a2 \<mapsto> s''];
     [atom2var a1 \<mapsto> s'', atom2var a2 \<mapsto> s''] ⊆m Γ|]
    ==> {atom2var a1, atom2var a2} ⊆ dom Γ"
apply (simp add: map_le_def)
apply (rule conjI)
 apply (erule_tac x="atom2var a1" in ballE)
  apply (split split_if_asm) 
   apply (drule_tac t="Γ (atom2var a1)" in sym,force)
  apply (drule_tac t="Γ (atom2var a1)" in sym, simp add: dom_def) 
 apply (simp add: dom_def) 
 apply (split split_if_asm,simp,simp) 
apply (erule_tac x="atom2var a2" in ballE)
 apply (split split_if_asm) 
  apply (drule_tac t="Γ (atom2var a2)" in sym,force)
 apply (drule_tac t="Γ (atom2var a2)" in sym, simp add: dom_def) 
by (simp add: dom_def) 



end