Theory SafeDAss_P8

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


header {* Derived Assertions. P8. closed E L h *}

theory SafeDAss_P8 imports SafeDAssBasic 
                           BasicFacts
begin


text{*
Lemmas for LET
*}

lemma P8_LET_e1: 
  "closed (E1, E2) (L1 ∪ (L2 - {x1})) (h, k) 
  ==> closed (E1, E2) L1 (h, k)"
by (simp add: closed_def add: live_def add: closureLS_def)

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

lemma P8_dem3: 
  "[| closed_f v1 (h', k'); y ∈ closure (E1(x1 \<mapsto> v1), E2) x1 (h', k')|]  
  ==> y ∈ domHeap (h', k')"
apply (simp add: closure_def add: closed_f_def)
apply (case_tac "v1",simp_all)
by blast

lemma P8_dem4: 
  "[| (\<Union>x∈L2 - {x1}. closure (E1, E2) x (h, k)) ⊆ dom h; x≠x1; x∈L2; p ∈ closure (E1, E2) x (h, k) |] 
  ==> p ∈ dom h"
by auto

lemma P8_LET_e2: 
  "[| def_pp Γ1 Γ2 L2;
     L2 ⊆ dom (disjointUnionEnv Γ2  (empty(x1 \<mapsto> m)));
     dom ( Γ2 + (empty(x1 \<mapsto> m))) ⊆ dom (E1(x1 \<mapsto> v1));
     shareRec L1 Γ1 (E1, E2) (h, k) (h',k);
     closed_f v1 (h', k);
     closed (E1, E2) (L1 ∪ (L2 - {x1})) (h, k) |] 
   ==> closed (E1(x1 \<mapsto> v1), E2) L2 (h', k)"
apply (simp add: closed_def add: live_def add: closureLS_def add: domHeap_def)
apply (erule conjE)
apply safe apply (rename_tac y x)
apply (case_tac "x≠x1")
 apply (subgoal_tac "x∈ dom E1",simp)
  prefer 2 apply blast
 apply (case_tac "¬  (identityClosure (E1, E2) x (h, k) (h', k))")
  apply (simp add: shareRec_def)
  apply (elim conjE)
  apply (erule_tac x="x" in ballE)+
   prefer 2 apply simp
   prefer 2 apply simp
  apply simp
  apply (elim conjE)
   apply (subgoal_tac "x∉ L2",simp)
   apply (rule P8_dem2,assumption+)
 apply (simp add: identityClosure_def)
  apply (erule conjE)
  apply (erule_tac x="y" in ballE)
   apply (subgoal_tac "closure (E1(x1 \<mapsto> v1), E2) x (h', k) = closure (E1, E2) x (h', k)",simp)
    prefer 2 apply (simp add: closure_def)
   apply (frule P8_dem4) apply assumption apply assumption+ apply simp apply (simp add: dom_def)
  apply (subgoal_tac "closure (E1(x1 \<mapsto> v1), E2) x (h', k) = closure (E1, E2) x (h', k)",simp)
  apply (simp add: closure_def)
 apply simp
apply (subgoal_tac "y ∈ domHeap (h', k)")
prefer 2 apply (rule P8_dem3, assumption+)
by (simp add: domHeap_def add: dom_def)


lemma P8_LET: 
  " [| def_pp Γ1 Γ2 L2;
      L2 ⊆ dom (disjointUnionEnv Γ2  (empty(x1 \<mapsto> m)));
      dom ( Γ2 + (empty(x1 \<mapsto> m))) ⊆ dom (E1(x1 \<mapsto> v1));
      shareRec L1 Γ1 (E1, E2) (h, k) (h',k);
      closed_f v1 (h', k);
      closed (E1, E2) (L1 ∪ (L2 - {x1})) (h, k) |] 
  ==> closed (E1, E2) L1 (h, k) ∧  closed (E1(x1 \<mapsto> v1), E2) L2 (h', k)"
apply (rule conjI)
 apply (erule P8_LET_e1)
by (erule P8_LET_e2)






text{*
Lemmas for CASE
*}

lemma vs_defined:
  "[| set xs ∩ dom E1  = {};
    length xs = length vs;
     y ∈ set xs;
     extend E1 xs vs y = Some (Loc q) |] 
   ==>∃ j < length vs. vs!j = Loc q"
apply (simp add: extend_def)
apply (induct xs vs rule: list_induct2',simp_all)
by (split split_if_asm,force,force)


lemma closure_Loc_subseteq_closureV_Loc:
 "[| vs ! i = Loc q; 
    i < length vs |] 
  ==> closureL q (h,k) ⊆ (\<Union>i < length vs closureV (vs ! i) (h, k))"
apply (rule subsetI)
apply clarsimp
apply (rule_tac x="i" in bexI)
 apply (simp add: closureV_def)
by simp

lemma closureV_subseteq_closureL:
  "h p = Some (j,C,vs)
   ==> (\<Union> i < length vs. closureV (vs!i) (h,k)) ⊆ closureL p (h,k)"
apply (frule closureV_equals_closureL)
by blast


lemma patrones:
  "[| E1 x = Some (Loc p); h p = Some (j,C,vs); 
     i < length alts; length alts > 0; length assert = length alts;
     set (snd (extractP (fst (alts ! i)))) ∩ dom E1  = {};
     length (snd (extractP (fst (alts ! i)))) = length vs;
     y ∈ set (snd (extractP (fst (alts ! i)))) |]
   ==> closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h, k) ⊆ 
       closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k)"
apply (rule subsetI)
apply (subst (asm) closure_def)
apply (case_tac 
 "extend E1 (snd (extractP (fst (alts ! i)))) vs y",simp_all)
apply (case_tac a,simp_all)
apply (subgoal_tac "x ∉ set (snd (extractP (fst (alts ! i))))")
 prefer 2 apply blast
apply (frule_tac x="x" and E="E1" and vs="vs" in extend_monotone_i)
apply (simp,simp,simp)
apply (rename_tac q)
apply (frule_tac y="y" in vs_defined,force,assumption+)
apply (simp add: closure_def)
apply (frule_tac k="k" in closureV_subseteq_closureL)
apply (elim exE,elim conjE)
apply (frule closure_Loc_subseteq_closureV_Loc,assumption+)
by force



lemma closure_monotone_extend_4: 
  "[| def_extend E  (snd (extractP (fst (alts ! i)))) vs;
     x∈ dom E; 
    length alts > 0;
    i < length alts |] 
  ==> closure (E, E') x (h, k) =  closure (extend E (snd (extractP (fst (alts ! i))))  vs, E') x (h, k)"
apply (subgoal_tac " x ∉ set (snd (extractP (fst (alts ! i))))")
 apply (subgoal_tac 
   "E x = extend E  (snd (extractP (fst (alts ! i)))) vs x")
  apply (simp add:closure_def)
 apply (rule extend_monotone_i) 
 apply (simp,simp,simp)
apply (simp add: def_extend_def)
by blast


lemma P8_CASE_closureLS:
  "[| def_extend E1  (snd (extractP (fst (alts ! i)))) vs;
     ∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
     (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪ {x}
        ⊆ dom (nonDisjointUnionEnvList (map snd assert));
     dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
     E1 x = Some (Loc p);
     h p = Some (j,C,vs);
     i < length assert; length assert = length alts; 0 < length assert|]
   ==> closureLS (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (fst (assert ! i)) (h, k) ⊆ 
       closureLS (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k)"
apply (simp add: closureLS_def)
apply (rule subsetI,simp)
apply (erule bexE)
apply (rule disjI2)
apply (rule_tac x="i" in bexI)
prefer 2 apply simp
apply (case_tac "xaa ∈ set (snd (extractP (fst (alts ! i))))")
 apply (rule_tac x="x" in bexI)
  prefer 2 apply simp
 apply (simp add: def_extend_def)
 apply (elim conjE)
 apply (frule_tac y="xaa" and vs="vs" and j="j" and 
                  C="C" and k="k" and ?E2.0="E2" and h="h" in patrones)
 apply (assumption+,simp,assumption+)
 apply (subgoal_tac 
   "closure (E1, E2) x (h, k) = 
    closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k)")
  apply blast
 apply (rule closure_monotone_extend_4) 
 apply (simp add: def_extend_def)
 apply (simp add: dom_def,simp,simp)
apply (rule_tac x="xaa" in bexI)
prefer 2 apply simp
apply (subgoal_tac 
  "xaa ∈ (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))")
 prefer 2 apply blast
apply (subgoal_tac 
  "closure (E1, E2) xaa (h, k) = 
   closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) xaa (h, k)")
 apply simp
apply (rule closure_monotone_extend_4) 
by (simp,blast,simp,simp)


lemma P8_CASE:
  "[| def_extend E1  (snd (extractP (fst (alts ! i)))) vs;
     ∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
     (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪ {x}
        ⊆ dom (nonDisjointUnionEnvList (map snd assert));
     dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
     E1 x = Some (Loc p);
     h p = Some (j,C,vs);
     i < length assert; length assert = length alts; 0 < length assert;
     closed (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k) |] 
==>  closed (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (fst (assert ! i)) (h, k)"
apply (simp add: closed_def)
apply (simp add: live_def)
apply (subgoal_tac 
  "closureLS (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (fst (assert ! i)) (h, k) ⊆
   closureLS (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k)")
apply blast
by (rule P8_CASE_closureLS,simp_all)


lemma P8_CASE_1_1_closureLS:
  "[| fst (alts ! i) = ConstP (LitN n);
     i < length assert; length assert = length alts; 0 < length assert|]
   ==> closureLS (E1, E2) (fst (assert ! i)) (h, k) ⊆ 
       closureLS (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k)"
apply (simp add: closureLS_def)
apply (rule subsetI,simp)
apply (erule bexE)
apply (rule disjI2)
apply (rule_tac x="i" in bexI)
prefer 2 apply simp
by (rule_tac x="xa" in bexI,simp,simp)


lemma P8_CASE_1_1:
  "[| fst (alts ! i) = ConstP (LitN n);
     i < length assert; length assert = length alts; 0 < length assert;
     closed (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k) |] 
==>  closed (E1, E2) (fst (assert ! i)) (h, k)"
apply (simp add: closed_def)
apply (simp add: live_def)
apply (subgoal_tac 
  "closureLS (E1, E2) (fst (assert ! i)) (h, k) ⊆
   closureLS (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k)")
apply blast
by (rule P8_CASE_1_1_closureLS,simp_all)


lemma P8_CASE_1_2_closureLS:
  "[| fst (alts ! i) = ConstP (LitB b);
     i < length assert; length assert = length alts; 0 < length assert|]
   ==> closureLS (E1, E2) (fst (assert ! i)) (h, k) ⊆ 
       closureLS (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k)"
apply (simp add: closureLS_def)
apply (rule subsetI,simp)
apply (erule bexE)
apply (rule disjI2)
apply (rule_tac x="i" in bexI)
prefer 2 apply simp
by (rule_tac x="xa" in bexI,simp,simp)


lemma P8_CASE_1_2:
  "[| fst (alts ! i) = ConstP (LitB b);
     i < length assert; length assert = length alts; 0 < length assert;
     closed (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k) |] 
==>  closed (E1, E2) (fst (assert ! i)) (h, k)"
apply (simp add: closed_def)
apply (simp add: live_def)
apply (subgoal_tac 
  "closureLS (E1, E2) (fst (assert ! i)) (h, k) ⊆
   closureLS (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k)")
apply blast
by (rule P8_CASE_1_2_closureLS,simp_all)


text{*
Lemmas for CASED
*}


lemma closureL_p_None_p:
  "closureL p (h(p := None), k) = {p}"
apply (rule equalityI)
 apply (rule subsetI)
 apply (erule closureL.induct,simp)
 apply (simp add: descendants_def)
apply (rule subsetI,simp)
by (rule closureL_basic)

lemma closure_extend_p_None_subseteq_closure:
  "[| E1 x = Some (Loc p); 
     E1 x = (extend E1 (snd (extractP (fst (alts ! i)))) vs) x |] 
    ==> closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h(p := None), k) ⊆ 
        closure (E1, E2) x (h, k)"
apply (simp add: closure_def)
apply (subst closureL_p_None_p,simp)
by (rule closureL_basic)


lemma descendants_p_None_q:
  "[| d ∈ descendants q (h(p:=None),k); q≠p |] 
  ==> d ∈ descendants q (h,k)"
by (simp add: descendants_def)


lemma closureL_p_None_subseteq_closureL:
  "p ≠ q
   ==> closureL q (h(p := None), k) ⊆ closureL q (h, k)"
apply (rule subsetI)
apply (erule closureL.induct)
 apply (rule closureL_basic)
apply clarsimp
apply (subgoal_tac "d ∈ descendants qa (h,k)")
 apply (rule closureL_step,simp,simp)
apply (rule descendants_p_None_q,assumption+)
apply (simp add: descendants_def)
by (case_tac "qa = p",simp_all)


lemma dom_foldl_monotone_list:
  " 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_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 x_notin_Γ_cased:
  "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))))"
apply (induct_tac assert alts rule: list_induct2',simp_all)
apply (subgoal_tac
  " dom (foldl op ⊗ (empty ⊗ restrict_neg_map (snd xa) (insert x (set (snd (extractP (fst y))))))
                 (map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li))) (zip (map (λa. snd (extractP (fst a))) ys) (map snd xs)))) = 
    dom (restrict_neg_map (snd xa) (insert x (set (snd (extractP (fst y)))))) ∪  
    dom (foldl op ⊗ empty (map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li))) 
                                (zip (map (λa. snd (extractP (fst a))) ys) (map snd xs))))",simp)
 apply (subst dom_restrict_neg_map,blast)
by (rule dom_foldl_monotone_list)



lemma Γ_case_x_is_d:
  "[|  Γ = 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''] |] 
   ==> Γ x = Some d''"
apply (simp add: disjointUnionEnv_def)
apply (simp add: unionEnv_def)
apply (rule impI)
apply (insert x_notin_Γ_cased)
by force


lemma P8_CASED:
  "[| E1 x = Some (Loc p); h p = Some (j,C,vs); 
     length assert > 0; length assert = length alts;
     length (snd (extractP (fst (alts ! i)))) = length vs;
      set (snd (extractP (fst (alts ! i)))) ∩ dom E1  = {};
     Γ = disjointUnionEnv
             (nonDisjointUnionEnvList ((map (λ(Li,Γi). restrict_neg_map Γi (set Li∪{x}))) 
             (zip (map (snd o extractP o fst) alts) (map snd assert))))
           (empty(x\<mapsto>d''));
     ∀ z ∈ dom Γ. Γ z ≠ Some s'' --> (∀i<length alts. z ∉ fst (assert ! i));
      shareRec (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
          Γ (E1, E2) (h, k) (hh, k);
     closed (E1, E2) (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))) (h, k);
     i < length alts |] 
  ==>  closed (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (fst (assert ! i)) (h(p := None), k)"
apply (subgoal_tac "Γ x = Some d''")
 prefer 2 apply (rule Γ_case_x_is_d,force)
apply (simp add: closed_def)
apply (simp add: live_def)
apply (simp add: closureLS_def)
apply (simp add: domHeap_def)
apply (elim conjE)
apply (rule subsetI)
apply (rename_tac q,simp)
apply (elim bexE)
apply (rename_tac y)
apply (case_tac "y ∈ set (snd (extractP (fst (alts ! i))))")
 (* y ∈ set {xij} *)
 apply (rule conjI)
 (* q ∈ dom h *)
  apply (frule_tac ?E2.0="E2" and  k="k" in patrones) 
  apply (assumption+,simp,assumption+)
  apply (subgoal_tac "x ∉ set (snd (extractP (fst (alts ! i)))) ")
   prefer 2 apply blast
  apply (frule_tac E="E1" and vs="vs" in extend_monotone_i,simp,assumption+)
  apply (frule_tac alts="alts" and vs="vs" and i="i" and ?E2.0="E2" and k="k" and h="h" in 
                   closure_extend_p_None_subseteq_closure,simp) 
  apply (simp add: closure_def)
  apply (case_tac "extend E1 (snd (extractP (fst (alts ! i)))) vs y",simp_all)
  apply (case_tac a, simp_all)
  apply (case_tac "p = nat",simp_all)
  (* p = E+ y *)
   apply (subst (asm) closureL_p_None_p,blast)
  (* p ≠ E+ y *)
  apply (frule_tac h="h" and k="k" in closureL_p_None_subseteq_closureL)
  apply blast
 (* p ≠ q *)
 apply (simp add: closure_def)
 apply (case_tac "extend E1 (snd (extractP (fst (alts ! i)))) vs y",simp_all)
 apply (case_tac a,simp_all)
 apply (frule vs_defined,simp,simp,simp)
 apply (elim exE,elim conjE)
 apply (frule_tac k="k" in no_cycles)
 apply (erule_tac x="ja" in allE,simp)
 apply (simp add: closureV_def)
 apply (case_tac "p = nat",simp_all)
  (* p = E+ y *)
  apply (subgoal_tac " nat ∈ closureL nat (h, k)",simp)
  apply (rule closureL_basic)
 (* p ≠ E+ y *)
 apply (frule_tac h="h" and k="k" in closureL_p_None_subseteq_closureL)
 apply blast

(* y ∉ set {xij} *)
apply (simp add: closure_def)
apply (case_tac "extend E1 (snd (extractP (fst (alts ! i)))) vs y",simp_all)
apply (case_tac a,simp_all)
apply (subgoal_tac "y ∈ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
 prefer 2 apply force
apply (frule extend_prop1,simp,simp)
apply (simp only: shareRec_def)
apply (elim conjE)
apply (rotate_tac 20)
apply (erule thin_rl)
apply (rotate_tac 19)
apply (erule_tac x="y" in ballE)
 prefer 2 apply simp
apply (rotate_tac 19)
apply (erule_tac x="x" in ballE)
 prefer 2 apply force
apply (case_tac 
  "closure (E1, E2) y (h, k) ∩ recReach (E1, E2) x (h, k) ≠ {}")
 apply simp
(* closure (E1, E2) y (h, k) ∩ recReach (E1, E2) x (h, k) = {} *)
apply (simp add: recReach_def)
apply (subgoal_tac "p ∈ recReachL p (h,k)")
 prefer 2 apply (rule recReachL_basic)
apply (frule_tac E="E1" and vs="vs" 
  in extend_monotone_i,simp,simp)
apply (simp add: closure_def)
apply (case_tac "p=nat",simp)
 (* p = E+ y *)
 apply (subgoal_tac "nat ∈ closureL nat (h,k)")
  apply (subgoal_tac "nat ∈ recReachL nat (h,k)")
   apply blast
  apply (rule recReachL_basic)
 apply (rule closureL_basic)
(* p ≠ E+ y *)
apply (frule_tac h="h" and k="k" in closureL_p_None_subseteq_closureL)
apply (subgoal_tac
  "∀ x ∈ (\<Union>x < length alts
       \<Union>x∈fst (assert ! x) - set (snd (extractP (fst (alts ! x)))).
           case E1 x of None => {} | Some (Loc p) => closureL p (h, k) | Some _ => {}).
    x ∈ dom h")
 prefer 2 apply blast
apply (erule_tac x="q" in ballE)
 apply force
apply simp
apply (erule_tac x="i" in ballE)
 prefer 2 apply simp
apply (rotate_tac 24)
apply (erule_tac x="y" in ballE)
 prefer 2 apply simp
apply simp
apply (frule_tac h="h" and k="k" in closureL_p_None_subseteq_closureL)
by blast




(** P8_APP **)


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_map_of_xs_atom2val:
  "[| length xs = length as; 
     distinct xs |] 
   ==> ∀ i < length xs. 
        map_of (zip xs (map (atom2val E1) as)) (xs!i) = 
        Some (atom2val E1 (as!i))"
apply clarsimp
apply (induct xs as rule: list_induct2',simp_all)
by (case_tac i,simp,clarsimp)


lemma closureL_k_equals_closureL_Suc_k:
  "closureL p (h, Suc k) = closureL p (h,k)" 
apply (rule equalityI)
 apply (rule subsetI)
 apply (erule_tac closureL.induct)
  apply (rule closureL_basic)
 apply (rule closureL_step,simp)
 apply (simp add: descendants_def)
apply (rule subsetI)
apply (erule_tac closureL.induct)
 apply (rule closureL_basic)
 apply (rule closureL_step,simp)
by (simp add: descendants_def)



lemma fvs_as_in_dom_E1:
 "[| fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1;
    i < length as; as ! i = VarE x a |] 
  ==> x ∈ dom E1"
apply (induct as i rule:list_induct3,simp_all)
by blast

lemma closure_APP_equals_closure_ef:
  "[| length xs = length as; distinct xs;  
     fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1;
     distinct xs;
     i < length as; as ! i = VarE xa a |]
   ==> closure (E1, E2) xa (h, k) = 
       closure (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (xs ! i) (h, Suc k)"
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val,assumption+)
apply (erule_tac x="i" in allE,simp)
apply (rule equalityI)
 (* closure App ⊆ closure ef *)
 apply (rule subsetI) 
 apply (simp add: closure_def)
 apply (case_tac "E1 xa",simp_all)
 apply (case_tac aa, simp_all)
 apply (subst closureL_k_equals_closureL_Suc_k,assumption)
(* closure ef ⊆ closure App *)
apply (rule subsetI) 
apply (simp add: closure_def)
apply (case_tac "E1 xa",simp_all)
 apply (frule fvs_as_in_dom_E1,assumption+)
 apply (simp add: dom_def)
apply (case_tac aa, simp_all)
apply (insert closureL_k_equals_closureL_Suc_k)
by simp



lemma nth_set_distinct:
  "[| x ∈ set xs; distinct xs |] 
  ==> ∃ i < length xs. xs!i = x"
by (induct xs,simp,force)

lemma  nth_map_add_map_of:
  "[|  i < length xs; length xs = length ms; distinct xs |] 
   ==> (Γ ++ map_of (zip xs ms)) (xs!i) = Some (ms!i)"
apply (subst map_add_Some_iff,simp)
apply (subgoal_tac
  "set (zip xs ms) = 
   {(xs!i, ms!i) | i. i < min (length xs) (length ms)}")
 apply force
by (rule set_zip)



lemma map_add_map_of:
 "[| x ∈ set xs; dom E1 ∩ set xs = {}; length xs = length ys|] 
  ==> (E1 ++ map_of (zip xs ys)) x = map_of (zip xs ys) x"  
apply (subgoal_tac "E1 x = None") 
 apply (simp only: map_add_def)
apply (case_tac "map_of (zip xs ys) x",simp_all)
by blast


lemma var_in_fvs:
 "[| i < length as; as ! i = VarE x a|] 
  ==>  x ∈ fvs' as"
apply (induct as arbitrary: i, simp_all)
apply clarsimp
apply (case_tac i,simp_all)
apply (case_tac aa, simp_all)
by auto


declare atom.simps [simp del]

lemma live_APP_equals_live_ef:
  "[| (∀ a ∈ set as. atom a); length xs = length as;
     length xs = length ms;
     fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1;
     dom E1 ∩ set xs = {}; distinct xs|] 
  ==> live (E1, E2) (fvs' as) (h, k) = 
      live (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (set xs) (h, Suc k)"
apply (rule equalityI)
 (* live App ⊆ live ef *) 
 apply (rule subsetI) 
 apply (simp add: live_def)
 apply (simp add: closureLS_def)
 apply (erule bexE)
 apply (frule atom_fvs_VarE,assumption+)
 apply (elim exE)
 apply (elim conjE, elim exE)
 apply (rule_tac x="xs!i" in bexI)
  prefer 2 apply simp
 apply (frule closure_APP_equals_closure_ef)
 apply (assumption+,force)
(* live ef ⊆ live App *) 
apply (rule subsetI) 
apply (simp add: live_def)
apply (simp add: closureLS_def)
apply (elim bexE)
apply (frule nth_set_distinct,assumption+)
apply (elim exE,elim conjE)
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val, assumption+)
apply (rotate_tac 11)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="as!i" in ballE)
 prefer 2 apply simp
apply (subgoal_tac 
  "length xs = length (map (atom2val E1) as)")
apply (frule map_add_map_of,assumption+) 
 prefer 2 apply simp
apply (simp add: atom.simps)
apply (case_tac "(as ! i)",simp_all)
 apply (simp add: closure_def)
apply (rule_tac x="list" in bexI)
 apply (case_tac "E1 list",simp_all) 
  apply (frule fvs_as_in_dom_E1,assumption+)
  apply (simp add: dom_def)
 apply (case_tac aa, simp_all)
 apply (subst (asm) closureL_k_equals_closureL_Suc_k)
 apply simp
by (frule var_in_fvs,assumption+)



lemma P8_APP_ef:
  "[| (∀ a ∈ set as. atom a); length xs = length as;
    length xs = length ms;
    dom E1 ∩ set xs = {}; distinct xs;
    fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1;
     closed (E1, E2) (fvs' as) (h, k) |] 
  ==> closed (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (set xs) (h, Suc k)"
apply (simp add: closed_def)
apply (frule live_APP_equals_live_ef) 
apply (assumption+) 
apply (subgoal_tac "domHeap (h, k) = domHeap (h, Suc k)")
 apply force
by (simp add: domHeap_def)



end