Theory SafeDAss_P9 (Isabelle2007: November 2007)

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


header {* Derived Assertions. P9. closed v h' *}

theory SafeDAss_P9 imports SafeDAssBasic
                           SafeRegion_definitions
                           BasicFacts
begin



text{*
Lemma for REUSE
*}


lemma closureV_equals_reuse:
  "[| p ∉ closureV v (h, k); 
     q ∉ closureV v (h, k)|]
  ==> closureV v (h, k) = closureV v (h(p := None)(q \<mapsto> (j, C, vn)), k)"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add: closureV_def)
 apply (case_tac v,simp_all)
 apply (rename_tac q)
 apply (erule closureL.induct)
  apply (rule closureL_basic)
 apply (rule closureL_step,simp)
 apply (simp add: descendants_def)
 apply (subgoal_tac "qa ≠ q",simp)
  prefer 2 apply blast
 apply (subgoal_tac "qa ≠ p",simp)
 apply blast
apply (rule subsetI)
apply (simp add: closureV_def)
apply (case_tac v,simp_all)
apply (rename_tac q)
apply (erule closureL.induct)
 apply (rule closureL_basic)
apply (rule closureL_step,simp)
apply (simp add: descendants_def)
apply (subgoal_tac "qa ≠ q",simp)
 prefer 2 apply blast
apply (subgoal_tac "qa ≠ p",simp)
by blast


lemma closureL_reuse_closureV:
  "[| E1 x = Some (Loc p); h p = Some (j, C, vn); 
     fresh q h|]
  ==> closureL q (h(p := None)(q \<mapsto> (j, C, vn)), k) = 
      (\<Union>_{i < length vn} closureV (vn ! i) (h, k)) - {p} ∪ {q}"
apply (frule_tac k=k in fresh_notin_closureL)
apply (frule_tac k=k in no_cycles)
apply (rule equalityI)
 apply (rule subsetI)
 apply (subst (asm) closureV_equals_closureL,force)
 apply (erule_tac x="p" in ballE)
  prefer 2 apply force
 apply (subst (asm) closureV_equals_closureL,force,simp)
 apply (erule disjE,simp)
 apply (rule disjI2)
 apply (elim bexE)
 apply (rule_tac x="i" in bexI)
  prefer 2 apply simp
 apply (elim conjE)
 apply (erule_tac x="i" in ballE)
  prefer 2 apply simp
 apply (erule_tac x="i" in allE,simp)
 apply (subst closureV_equals_reuse [where p=p],assumption+)
apply simp
apply (rule conjI)
 apply (rule closureL_basic)
apply (rule subsetI)
apply (subst closureV_equals_closureL,force)
apply (erule_tac x="p" in ballE)
 prefer 2 apply force
apply (subst (asm) closureV_equals_closureL,force,simp)
apply (rule disjI2)
apply (elim bexE)
apply (rule_tac x="i" in bexI)
 prefer 2 apply simp
apply (elim conjE)
apply (erule_tac x="i" in ballE)
 prefer 2 apply simp
apply (erule_tac x="i" in allE,simp)
by (subst (asm) closureV_equals_reuse [where p=p],assumption+)


lemma P9_REUSE:
  "[| E1 x = Some (Loc p); h p = Some c; fresh q h;
    closed (E1, E2) {x} (h, k)|]
  ==> closed_f (Loc q) (h(p := None)(q \<mapsto> c), k)"
apply (case_tac c)
apply (case_tac b)
apply simp
apply (rename_tac j b C vn)
apply (simp add: closed_def)
apply (simp add: live_def)
apply (simp add: closureLS_def)
apply (simp add: closure_def)
apply (simp add: closed_f_def)
apply (simp add: domHeap_def)
apply (subst closureL_reuse_closureV,assumption+)
apply (subst (asm) closureV_equals_closureL,force)
by blast


text{*
Lemma for COPY
*}

axioms P9_COPY:
  "[| E1 x = Some (Loc p);
     copy (h, k) p j = ((h', k), p'); def_copy p (h, k);
     closed (E1, E2) {x} (h, k) |]
  ==> closed_f (Loc p') (h', k)"



text{*
Lemmas for LET1 and LET2
*}

lemma P9_LET: 
  "[|closed_f v1 (h', k'); closed_f v (hh, kk)|]  
  ==> closed_f v (hh, kk)"
by simp



text{*
Lemmas for LET1C and LET2C
*}


axioms none_notequal_p:
 "the None ≠ Loc p"


lemma closed_e1_closureV_subseteq_dom_h:
  "[| closed (E1, E2) (set (map atom2var as)) (h, k); 
     ∀a∈set as. atom a |] 
   ==> (\<Union>_{i < length as} closureV (map (atom2val E1) as ! i) (h, k)) ⊆ 
       dom h"
apply (simp add: closed_def)
apply (simp add: live_def)
apply (simp add: closureLS_def)
apply (simp add: closure_def)
apply (simp add: closureV_def)
apply (rule subsetI)
apply (erule UN_E)
apply (erule_tac x="as!i" in ballE)
 prefer 2 apply simp
apply (case_tac "as!i",simp_all)
apply (case_tac "atom2val E1 (as!i)",simp_all)
apply (subgoal_tac "as!i ∈ set as")
 prefer 2 apply (subst set_conv_nth,force)
apply (subgoal_tac
  "(case E1 (atom2var (as!i)) of None => {} | Some (Loc p) => closureL p (h, k) | Some _ => {}) ⊆ 
   domHeap (h, k)")
 prefer 2 apply blast
apply (simp add: domHeap_def)
apply (subgoal_tac 
  "x ∈ (case E1 list of None => {} | Some (Loc p) => closureL p (h, k) | Some _ => {})")
 apply blast
apply (case_tac "E1 list",simp_all)
by (insert none_notequal_p,force)


lemma closureV_upt_subset_closureV:
  "fresh p h
   ==>  (\<Union>_{i < length (map (atom2val E1) as)} closureV (map (atom2val E1) as ! i) 
                                       (h(p \<mapsto> (j, C, map (atom2val E1) as)), k)) ⊆ 
        (\<Union>_{i < length (map (atom2val E1) as)} closureV (map (atom2val E1) as ! i) 
                                       (h, k)) ∪ {p}"
apply (rule subsetI)
apply (erule UN_E)
apply (subgoal_tac 
  "(h(p \<mapsto> (j, C, map (atom2val E1) as))) p = 
   Some (j,C, map (atom2val E1) as)")
 prefer 2 apply force
apply (frule_tac k=k  and h="(h(p \<mapsto> (j, C, map (atom2val E1) as)))" in no_cycles)
apply (simp add: closureV_def)
apply (erule_tac x="i" in allE,simp)
apply (case_tac "atom2val E1 (as ! i)",simp_all)
apply (rule disjI2)
apply (rule_tac x="i" in bexI,simp)
 prefer 2 apply simp
apply (erule closureL.induct)
 apply (rule closureL_basic)
apply (rule closureL_step,simp)
apply (simp add: descendants_def)
by (case_tac "q = p",simp_all)



lemma P9_LETC_e1:
  "[| ∀a∈set as. atom a; fresh p h;
     closed (E1, E2) (set (map atom2var as)) (h, k) |] 
   ==> closed_f (Loc p) (h(p \<mapsto> (j, C, map (atom2val E1) as)), k)"
apply (drule closed_e1_closureV_subseteq_dom_h,assumption+)
apply (simp add: closed_f_def)
apply (subst closureV_equals_closureL) 
 apply force
apply (subgoal_tac
  "(\<Union>_{i < length (map (atom2val E1) as)} closureV (map (atom2val E1) as ! i) (h(p \<mapsto> (j, C, map (atom2val E1) as)), k)) ⊆
        (\<Union>_{i < length (map (atom2val E1) as)} closureV (map (atom2val E1) as ! i) (h, k)) ∪ {p}")
 apply (simp add: domHeap_def)
 apply blast
by (rule closureV_upt_subset_closureV,assumption)



text{*
Lemmas for APP
*}




axioms extend_heaps_P9:
 "(h', Suc k) \<sqsubseteq>  (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k)"

lemma P9_APP_1:
  "[| x ∈ domHeap (h', Suc k); h x = h' x |] 
   ==> x ∈ domHeap (h,k)"
apply (simp only: domHeap_def)
by (simp add: dom_def)



axioms Lemma4_consistent_v:
 "(h,k) \<sqsubseteq> (h',k')
  ==> ∀ t η p.  
        consistent_v t η (Loc p) h 
    --> consistent_v t η (Loc p) h'"

axioms consistent_v_identityClosure:
  "consistent_v t η (Loc p) h 
  --> consistent_v t η (Loc p) h'
   ==> closureL p (h,k) = closureL p (h',k') ∧ (∀ x ∈ closureL p (h,k). h x = h' x)"


lemma P9_APP:
  "[| hh = h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k};
     closed_f v (h', Suc k) |] 
  ==> closed_f v (hh, k)"
apply (simp add: closed_f_def)
apply (case_tac v, simp_all)
apply (rename_tac q) 
apply (subgoal_tac 
  "(h', Suc k) \<sqsubseteq>  
   (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k)")
prefer 2 apply (rule extend_heaps_P9) 
apply (frule Lemma4_consistent_v)
apply (erule_tac x="t" in allE)
apply (erule_tac x="η" in allE)
apply (erule_tac x="q" in allE)
apply (drule consistent_v_identityClosure [where k="Suc k" and k'="k"])
apply (elim conjE)
apply (rule subsetI)
apply (subgoal_tac "x ∈ domHeap (h',Suc k)")
 prefer 2 apply blast
apply (erule_tac x="x" in ballE)
apply (frule P9_APP_1 [where h="h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}"]) 
apply (rule sym, assumption+)
by blast

axioms P9_APP:
  "[| hh = h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}|] 
  ==> closed_f v (hh, k)"


text{*
Lemmas for APP-PRIMOP
*}

lemma P9_APP_PRIMOP:
  "closed_f (execOp oper (atom2val E1 a1) (atom2val E1 a2)) (h, k)"
apply (simp only: closed_f_def)
by (case_tac oper,simp_all)

end

lemma closureV_equals_reuse:

  [| p ∉ closureV v (h, k); q ∉ closureV v (h, k) |]
  ==> closureV v (h, k) = closureV v (h(p := None)(q |-> (j, C, vn)), k)

lemma closureL_reuse_closureV:

  [| E1.0 x = Some (Loc p); h p = Some (j, C, vn); fresh q h |]
  ==> closureL q (h(p := None)(q |-> (j, C, vn)), k) =
      (UN i<length vn. closureV (vn ! i) (h, k)) - {p} ∪ {q}

lemma P9_REUSE:

  [| E1.0 x = Some (Loc p); h p = Some c; fresh q h;
     closed (E1.0, E2.0) {x} (h, k) |]
  ==> closed_f (Loc q) (h(p := None)(q |-> c), k)

lemma P9_LET:

  [| closed_f v1.0 (h', k'); closed_f v (hh, kk) |] ==> closed_f v (hh, kk)

lemma closed_e1_closureV_subseteq_dom_h:

  [| closed (E1.0, E2.0) (set (map atom2var as)) (h, k); ∀a∈set as. atom a |]
  ==> (UN i<length as. closureV (map (atom2val E1.0) as ! i) (h, k)) ⊆ dom h

lemma closureV_upt_subset_closureV:

  fresh p h
  ==> (UN i<length (map (atom2val E1.0) as).
          closureV (map (atom2val E1.0) as ! i)
           (h(p |-> (j, C, map (atom2val E1.0) as)), k))
      ⊆ (UN i<length (map (atom2val E1.0) as).
            closureV (map (atom2val E1.0) as ! i) (h, k)) ∪
        {p}

lemma P9_LETC_e1:

  [| ∀a∈set as. atom a; fresh p h;
     closed (E1.0, E2.0) (set (map atom2var as)) (h, k) |]
  ==> closed_f (Loc p) (h(p |-> (j, C, map (atom2val E1.0) as)), k)

lemma P9_APP_1:

  [| x ∈ domHeap (h', Suc k); h x = h' x |] ==> x ∈ domHeap (h, k)

lemma P9_APP:

  [| hh = h' |` {p : dom h'. fst (the (h' p)) ≤ k}; closed_f v (h', Suc k) |]
  ==> closed_f v (hh, k)

lemma P9_APP_PRIMOP:

  closed_f (execOp oper (atom2val E1.0 a1.0) (atom2val E1.0 a2.0)) (h, k)