Theory SafeDAss_P2

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


header {* Derived Assertions. P2. dom  $\Gamma$  $\subseteq$ dom E *}

theory SafeDAss_P2 imports SafeDAssBasic
begin


text{*
Lemmas for LET1 and LET2
*}

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

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


lemma P2_LET_e1: 
  "[|dom (pp Γ1 Γ2 L2) ⊆ dom E1|] 
  ==> dom Γ1 ⊆ dom E1 "
apply (subgoal_tac "dom Γ1 ⊆ dom (pp Γ1 Γ2 L2)")
by (blast, rule dom_Γ1_subseteq_triangle_Γ1_Γ2_L2)


lemma P2_LET_e2: 
  "[| def_disjointUnionEnv Γ2 [x1 \<mapsto> m]; 
     x1 ∉ dom E1; 
     dom (pp Γ1 Γ2 L2) ⊆ dom E1|] 
   ==> dom (Γ2 + [x1 \<mapsto> m]) ⊆ dom (E1(x1 \<mapsto> v1))"
apply (rule subsetI)
apply (case_tac "x≠x1",simp)
 apply (subgoal_tac "x ∈ dom (pp Γ1 Γ2 L2)")
  apply blast
 apply (frule union_dom_disjointUnionEnv,simp add: def_disjointUnionEnv_def)
 apply (subgoal_tac "dom Γ2 ⊆ dom (pp Γ1 Γ2 L2)")
  apply blast
 apply (rule dom_Γ2_subseteq_triangle_Γ1_Γ2_L2)
by simp


lemma P2_LET: 
  "[| def_disjointUnionEnv Γ2 (empty(x1\<mapsto>m));
     x1 ∉ dom E1;
     dom (pp Γ1 Γ2 L2) ⊆ dom E1|] 
  ==>  dom Γ1 ⊆ dom E1 ∧ dom ( Γ2 + (empty(x1 \<mapsto> m))) ⊆ dom (E1(x1 \<mapsto> r))"
apply (rule conjI)
 apply (erule P2_LET_e1)
by (erule P2_LET_e2,assumption+)



text{*
Lemmas for CASE
*}


lemma P2_CASE:
  "[| length assert > 0; i < length alts; length assert = length alts;
     def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
     dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1 |] 
  ==> dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)"
apply (frule dom_Γi_subseteq_dom_Γ_case)
apply (subgoal_tac "dom E1 ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
 apply (erule_tac x="i" in allE,simp) 
by (simp add: extend_def,blast)



lemma P2_CASE_1_1:
  "[| length assert > 0; i < length alts; length assert = length alts;
     dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1 |] 
  ==> dom (snd (assert ! i)) ⊆ dom E1"
apply (frule dom_Γi_subseteq_dom_Γ_case)
by (erule_tac x="i" in allE,simp) 


text{*
Lemmas for CASED
*}


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

lemma dom_G_dom_restrict_neg_map:
    "dom G = dom (restrict_neg_map G A) ∪  (dom G ∩  A)"
apply (subst dom_restrict_neg_map)
by blast


lemma dom_map_of_zip:
  "length xs = length ys 
   ==> dom (map_of (zip xs ys)) = set xs"
by (induct xs ys rule: list_induct2',simp_all)



lemma dom_foldl_disjointUnionEnv_monotone_generic:
  " dom (foldl op ⊗ (empty ⊗ y) ys + [x \<mapsto> d'']) = 
    dom y ∪  dom (foldl op ⊗ empty ys) ∪ dom  [x \<mapsto> d'']"
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_monotone_foldl_nonDijointUnionEnv_Gis:
 "length Gis > i ==> dom (Gis ! i) ⊆ dom (foldl op ⊗ empty Gis + [x \<mapsto> d''])"
apply (induct Gis i rule: list_induct3, simp_all)
apply (subgoal_tac " dom (foldl op ⊗ (empty ⊗ xa) xs + [x \<mapsto> d'']) = 
                     dom xa ∪  dom (foldl op ⊗ empty xs) ∪ dom [x \<mapsto> d'']",simp)
apply blast
apply (rule dom_foldl_disjointUnionEnv_monotone_generic)
apply (subgoal_tac " dom (foldl op ⊗ (empty ⊗ xa) xs + [x \<mapsto> d'']) = 
                     dom xa ∪  dom (foldl op ⊗ empty xs) ∪ dom [x \<mapsto> d'']",simp)
 apply (subgoal_tac "dom (foldl op ⊗ empty xs + [x \<mapsto> d'']) =
                     dom (foldl op ⊗ empty xs) ∪ dom [x \<mapsto> d'']",simp)
  apply blast
 apply (rule dom_disjointUnionEnv_monotone)
by (rule dom_foldl_disjointUnionEnv_monotone_generic)


lemma dom_Γ_case_subseteq_dom_Γi [rule_format]:
  "dom (foldl op ⊗ empty Gis + [x \<mapsto> d'']) ⊆ dom E1
   --> def_disjointUnionEnv (foldl op ⊗ empty Gis) [x \<mapsto> d'']
   --> length Gis > 0
   --> i < length Gis
   --> dom (Gis!i) ⊆ dom E1"
apply (rule impI)+
apply (subgoal_tac
  "dom (Gis ! i) ⊆ dom (foldl op ⊗ empty Gis + [x \<mapsto> d''])")
 apply blast
by (rule dom_monotone_foldl_nonDijointUnionEnv_Gis,assumption)

lemma P2_CASED:
  "[| length assert > 0;  length assert = length alts; x ∈ dom E1;
     length (snd (extractP (fst (alts ! i)))) = length vs;
     i < 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''];
     length (snd (extractP (fst (alts ! i)))) = length vs;
     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'']) ⊆ dom E1 |] 
  ==>  dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)"
apply (subst dom_G_dom_restrict_neg_map [where A=" (insert x (set (snd (extractP (fst (alts ! i))))))"])
apply (simp add: extend_def)
apply (rule conjI)
 apply (frule dom_Γ_case_subseteq_dom_Γi) 
 apply (assumption+,simp,simp,simp)
 apply force
apply (subst dom_map_of_zip,simp)
by blast


end