Theory ClosureHeap

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

header {* Closure Heap *}


theory ClosureHeap
imports SafeHeap "../CoreSafe/SafeRASemantics"
begin


(* Closure Definitions *)

inductive_set
  closureL :: "Location => Heap => Location set"
  for p :: Location and h :: Heap
where
  closureL_basic: "p ∈ closureL p h"
| closureL_step:  " [|q ∈ closureL p h; d ∈ descendants q h|] ==> d ∈ closureL p h"

constdefs closure :: "Environment => string => Heap => Location set"
"closure E x h ≡ (case ((fst E) x) of Some (Loc p) => closureL p h
                                    | _ => {})"

constdefs closureV :: "Val => Heap => Location set"
"closureV v h ≡  (case v of IntT i => {}
                         | BoolT b => {}
                         | Loc p => closureL p h)"


constdefs closureLS :: "Environment => string set => Heap => Location set"
"closureLS E L h ≡ (\<Union>x∈L. closure E x h)"

constdefs identityClosure :: "Environment => string => Heap => Heap => bool"
"identityClosure E x h hh ≡ closure E x h = closure E x hh ∧
                            (∀p ∈ closure E x h. (fst h) p = (fst hh) p)"

constdefs identityClosureL :: "Location => Heap => Heap => bool"
"identityClosureL q h hh ≡ closureL q h = closureL q hh ∧
                            (∀p ∈ closureL q h. (fst h) p = (fst hh) p)"


defs def_copy:
 "def_copy p h == (∀ q ∈ closureL p h. q ∈ dom (fst h))"

(* Scope Definition *)
constdefs scope :: "Environment => Heap => Location set"
"scope E h ≡ closureLS E (dom (fst E)) h"

constdefs live :: "Environment => string set => Heap => Location set"
"live E L h ≡ closureLS E L h"



(* Closed Definitions *)


constdefs closed :: "Environment => string set => Heap => bool"
"closed E L h ≡ (live E L h) ⊆ domHeap h"

lemma closed_Empty : "closed E {} h"
by (simp add: closed_def add: live_def add: closureLS_def)

lemma closed_monotone: "closed E (L1 ∪ (L2 - {x1})) h ==>  closed E L1 h"
by (simp add: closed_def add: live_def add: closureLS_def)

constdefs closed_f :: "Val => Heap => bool"
"closed_f v h ≡ (case v of IntT i => True
                         | BoolT b => True
                         | Loc p => closureL p h ⊆ domHeap h)"


(* RecReach Definitions *)

inductive_set
   recReachL :: "Location => Heap => Location set"
   for p :: Location and h :: Heap
where
  recReachL_basic: "p ∈ recReachL p h"
| recReachL_step:  "[| q ∈ recReachL p h; d ∈ recDescendants q h|] ==>  d ∈ recReachL p h"


constdefs recReach :: "Environment => string => Heap => Location set"
"recReach E x h ≡ (case ((fst E) x) of Some (Loc p) => recReachL p h
                                    | _ => {})"


lemma transit_aux: "[| r ∈ closureL d h |] ==>  d ∈ descendants qa h --> r ∈ closureL qa h"
apply (erule closureL.induct)
 apply (rule impI)
 apply (subgoal_tac "qa ∈ closureL qa h")
  apply (erule closureL_step, assumption)
 apply (rule closureL_basic)
apply (rule impI)
apply (drule mp)
 apply assumption
by (erule closureL_step, assumption)

lemma transit_aux2: "[| r ∈  closureL d h;  d ∈ descendants qa h |] ==> r ∈ closureL qa h"
apply (subgoal_tac "[| r ∈ closureL d h |] ==>  d ∈ descendants qa h --> r ∈ closureL qa h", simp)
by (rule transit_aux,assumption)

lemma transit: "[|p ∈ closureL q h|] ==> ∀r. r ∈ closureL p h
                --> r ∈ closureL q h"
apply (erule closureL.induct)
 apply simp
apply clarsimp
apply(erule allE, erule mp)
apply (erule thin_rl)
by (erule transit_aux2,assumption)

lemma closureL_transit: "[|p ∈ closureL q h; r ∈ closureL p h|] ==>  r ∈ closureL q h"
by (frule transit,simp)


lemma closure_transit:  "[|p ∈ closure E x h; q ∈ closureL p h|] ==> q ∈ closure E x h"
apply (simp add: closure_def)
apply (case_tac "fst E x")
 apply simp
apply simp
apply (case_tac "a")
 apply simp_all
apply (erule closureL_transit)
by assumption

lemma closureL_monotone: "p ∈ closureL q (h1', h2') ==>  closureL p (h1', h2') ⊆  closureL q (h1', h2')"
apply (erule closureL.induct)
 apply simp
apply (subgoal_tac "closureL d (h1', h2') ⊆  closureL qa (h1', h2')")
 apply blast
apply (rule subsetI, rule transit_aux2)
 apply simp
by simp

lemma closure_recReach_monotone: 
  "[| p ∈ closure (E1(x1 \<mapsto> r), E2) y (h1', h2');
     closureL p (h1', h2') ∩ recReach (E1(x1 \<mapsto> r), E2) x (h1', h2') ≠ {} |] 
    ==>  closure (E1(x1 \<mapsto> r), E2) y (h1', h2') ∩ recReach (E1(x1 \<mapsto> r), E2) x (h1', h2') ≠ {}"
apply (case_tac "y≠x1")
 apply (simp add: closure_def)
 apply (case_tac "E1 y")
  apply simp
 apply simp
 apply (case_tac "a", simp_all,clarsimp)
 apply (subgoal_tac " p ∈ closureL nat (h1', h2') ==>  closureL p (h1', h2') ⊆  closureL nat (h1', h2')")
  apply blast
 apply (erule closureL_monotone)
apply (simp add: closure_def)
apply (case_tac "r",simp_all,clarsimp)
apply (subgoal_tac " p ∈ closureL nat (h1', h2') ==>  closureL p (h1', h2') ⊆  closureL nat (h1', h2')")
 apply blast
by (erule closureL_monotone)

lemma closure_monotone: "[|y ≠ x1;p ∈ closure (E1(x1 \<mapsto> r), E2) y (h1', h2')|]
        ==>  closureL p (h1', h2') ⊆ closure (E1(x1 \<mapsto> r), E2) y (h1', h2')"
apply (simp add: closure_def)
apply (case_tac "E1 y",simp_all)
apply (case_tac "a", simp_all)
by (erule closureL_monotone)

lemma identityClosureL_monotone_h: 
  " [|x ∈ closureL q h|] ==> q ∈ closureL p h --> identityClosureL p h hh --> x ∈ closureL q hh"
apply (erule closureL.induct)
 apply (intro impI, rule closureL_basic)
apply (intro impI)
apply simp
apply (subgoal_tac "d ∈ descendants qa hh")
 apply (erule closureL_step,simp)
apply (simp add: identityClosureL_def)
apply (erule conjE)
apply (erule_tac x="qa" in ballE)
apply (subgoal_tac "qa ∈ closureL q h")
 apply (subgoal_tac "d ∈ closureL q h")
  apply (simp add: descendants_def)
 apply (erule closureL_step,simp)
apply simp
apply (subgoal_tac "q ∈ closureL p h")
 prefer 2 apply simp
apply (subgoal_tac "[| qa ∈ closureL q h;  q ∈ closureL p h|]  ==> qa ∈  closureL p h",simp)
by (rule closureL_transit)

lemma identityClosureL_monotone_hh: 
  "[|x ∈ closureL q hh|] ==> q ∈ closureL p h --> identityClosureL p h hh --> x ∈ closureL q h"
apply (erule closureL.induct)
 apply (intro impI, rule closureL_basic)
apply (intro impI)
apply simp
apply (subgoal_tac "d ∈ descendants qa h")
 apply (erule closureL_step,simp)
apply (simp add: identityClosureL_def)
apply (erule conjE)
apply (erule_tac x="qa" in ballE)
apply (subgoal_tac "qa ∈ closureL q hh")
 apply (subgoal_tac "d ∈ closureL q hh")
  apply (simp add: descendants_def)
 apply (erule closureL_step,simp)
apply simp
apply (subgoal_tac "q ∈ closureL p hh")
 prefer 2 apply simp
apply (subgoal_tac "[| qa ∈ closureL q hh;  q ∈ closureL p hh|]  ==> qa ∈  closureL p hh",simp)
by (rule closureL_transit)

lemma identityClosureL_monotone: 
  " [|identityClosureL p h hh; q ∈ closureL p h|] ==> identityClosureL q h hh"
apply (simp (no_asm) add: identityClosureL_def)
apply (rule conjI)
 apply (rule equalityI)
  apply (rule subsetI)
  apply (subgoal_tac "[|x ∈ closureL q h|] ==> q ∈ closureL p h --> identityClosureL p h hh --> x ∈ closureL q hh",simp)
  apply (rule identityClosureL_monotone_h,simp)
 apply (rule subsetI)
 apply (subgoal_tac "[|x ∈ closureL q hh|] ==> q ∈ closureL p h --> identityClosureL p h hh --> x ∈ closureL q h",simp)
 apply (rule identityClosureL_monotone_hh,simp)
apply (simp add: identityClosureL_def)
apply (rule ballI)
apply (erule conjE)
apply (subgoal_tac "q ∈ closureL p h")
 apply (frule_tac r="pa" and h="h" in closureL_transit)
  apply (rule closureL_basic)
 apply (erule_tac x="pa" in ballE,clarsimp)
apply (frule_tac r="pa" and h ="h" and p="q" in closureL_transit,clarsimp) 
 apply simp 
by simp


lemma identityClosure_closureL_monotone:
  "[| identityClosure E x h hh; q ∈ closure E x h|] ==> identityClosureL q h hh"
apply (simp add: identityClosure_def)
apply (simp add: closure_def)
apply (case_tac "fst E x",simp_all)
apply (case_tac "a",simp_all)
apply (subgoal_tac "closureL nat h = closureL nat hh ∧ (∀p∈closureL nat h. fst h p = fst hh p) --> identityClosureL nat h hh",simp)
 apply (erule identityClosureL_monotone,simp)
by (simp add: identityClosureL_def)

lemma recReachL_subseteq_closureL: 
  "recReachL p h ⊆ closureL p h"
apply clarify
apply (erule recReachL.induct)
apply (simp add: closure_def)
apply (rule closureL_basic)
apply (simp add: closure_def)
apply (subgoal_tac "recDescendants q h ⊆ descendants q h")
apply (erule closureL_step, blast)
apply (simp add: recDescendants_def add: descendants_def)
apply (case_tac "fst h q", simp, simp)
apply (subgoal_tac "getRecursiveValuesCell (snd a) ⊆ getNonBasicValuesCell (snd a)", simp)
apply (simp add: getRecursiveValuesCell_def add: getNonBasicValuesCell_def)
apply (simp add: isRecursive_def add: isNonBasicValue_def)
apply auto
done


lemma recReach_subseteq_closure: 
  "recReach E z h ⊆ closure E z h"
apply (simp add: recReach_def)
apply (case_tac "fst E z",simp_all)
apply (case_tac "a",simp_all)
apply (simp add: closure_def)
by (rule recReachL_subseteq_closureL)

lemma identityClosure_equals_recReach_hh: 
  "p∈ recReachL q hh ==> closureL q h = closureL q hh --> (∀p ∈ closureL q h. (fst h) p = (fst hh) p) --> p ∈ recReachL q h"
apply (erule recReachL.induct)
 apply (intro impI)
 apply (rule recReachL_basic)
apply clarsimp
apply (erule_tac c="qa" in equalityCE)
 apply (subgoal_tac " d ∈ recDescendants qa hh ==>  d ∈ recDescendants qa h",simp)
  apply (erule recReachL_step,simp)
 apply (simp add: recDescendants_def)
apply (subgoal_tac " recReachL q h ⊆  closureL q h")
 apply blast
by (rule recReachL_subseteq_closureL) 

lemma identityClosure_equals_recReach_h: 
  "p∈ recReachL q h ==> closureL q h = closureL q hh --> (∀p ∈ closureL q h. (fst h) p = (fst hh) p) --> p ∈ recReachL q hh"
apply (erule recReachL.induct)
 apply (intro impI)
 apply (rule recReachL_basic)
apply clarsimp
apply (erule_tac c="qa" in equalityCE)
 apply (subgoal_tac " d ∈ recDescendants qa h ==>  d ∈ recDescendants qa hh",simp)
  apply (erule recReachL_step,simp)
 apply (simp add: recDescendants_def)
apply (subgoal_tac " recReachL q hh ⊆  closureL q hh")
 apply blast
by (rule recReachL_subseteq_closureL) 


lemma identityClosure_equals_recReach: 
  "identityClosure E x h hh ==> recReach E x h = recReach E x hh"
apply (simp add: identityClosure_def)
apply (simp add: closure_def)
apply (case_tac "fst E x",simp_all)
apply (simp add: recReach_def)
apply (case_tac "a",simp_all)
apply (elim conjE)
apply (simp_all add: recReach_def)
apply (rule equalityI)
 apply (rule subsetI)
 apply (subgoal_tac "xa∈ recReachL nat h ==> 
                     closureL nat h = closureL nat hh --> (∀p ∈ closureL nat h. (fst h) p = (fst hh) p) --> xa ∈ recReachL nat hh",simp)
 apply (rule identityClosure_equals_recReach_h,simp)
apply (rule subsetI)
apply (subgoal_tac "xa∈ recReachL nat hh ==> 
                    closureL nat h = closureL nat hh --> (∀p ∈ closureL nat h. (fst h) p = (fst hh) p) --> xa ∈ recReachL nat h",simp)
by (rule identityClosure_equals_recReach_hh,simp)

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

lemma closure_monotone_extend: 
  "[| ∀i<length alts. set (snd (extractP (fst (alts ! i)))) ∩ dom E = {}  ∧ 
                     length (snd (extractP (fst (alts ! i)))) = length 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 (erule_tac x="i" in allE)
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)
by blast


lemma closure_monotone_extend_2: 
  "[| set (snd (extractP (fst (alts ! i)))) ∩ dom E = {};
     length (snd (extractP (fst (alts ! i)))) = length 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)
by blast

lemma closure_monotone_extend_3: 
  "[| set (snd (extractP (fst (alts ! i)))) ∩ dom E = {};
     length (snd (extractP (fst (alts ! i)))) = length vs; 
     x∈ dom E; 
    length alts > 0;
    i < length alts;
    xa ∈ closure (extend E (snd (extractP (fst (alts ! i))))  vs, E') x (h, k) |] 
  ==> xa ∈ closure (E, 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)
by blast

lemma recReach_monotone_extend: 
  "[| ∀i<length alts. set (snd (extractP (fst (alts ! i)))) ∩ dom E = {} ∧ 
                     length (snd (extractP (fst (alts ! i)))) = length vs;
    x ∈ dom E;
    length alts > 0; i < length alts|] 
  ==> recReach (E, E') x (h, k) =  recReach (extend E (snd (extractP (fst (alts ! i))))  vs, E') x (h, k)"
apply (erule_tac x="i" in allE)
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:recReach_def)
 apply (rule extend_monotone_i) 
 apply (simp,simp,simp)
by blast

lemma recReach_monotone_extend_2: 
  "[| set (snd (extractP (fst (alts ! i)))) ∩ dom E = {};
    length (snd (extractP (fst (alts ! i)))) = length vs;
    x ∈ dom E;
    length alts > 0; i < length alts|] 
  ==> recReach (E, E') x (h, k) =  recReach (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:recReach_def)
 apply (rule extend_monotone_i) 
 apply (simp,simp,simp)
by blast



lemma monotone_extend_closures:
"[|∀ i < length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
  ∀ i < length alts. set (snd (extractP (fst (alts ! i)))) ∩ dom E1  = {} ∧ 
                     length (snd (extractP (fst (alts ! i)))) = length vs;
  ∀ i < length assert. dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
   z∈fst (assert ! i); z ∉ set (snd (extractP (fst (alts ! i))));
   length alts = length assert;
   closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {};
   x∈ dom E1; 
   length assert > 0;
   i < length alts |] 
 ==>
  closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k) ∩
  recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) z (h, k) ≠ {}"
apply (subgoal_tac "closure (E1, E2) x (h, k) = 
                    closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k)")
 prefer 2 apply (simp,rule closure_monotone_extend,simp,simp,simp,simp)
apply (subgoal_tac "z ∈ dom E1")
 apply (subgoal_tac "recReach (E1, E2) z (h, k) = 
                     recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) z (h, k)")
 prefer 2 apply (rule recReach_monotone_extend,assumption+,simp,simp)
 apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="i" in allE,simp)
apply (subgoal_tac "z ∈ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
 prefer 2 apply blast
apply (elim conjE)
by (rule extend_prop1,assumption+)


lemma monotone_extend_closures_i:
"[| set (snd (extractP (fst (alts ! i)))) ∩ dom E1  = {} ∧ length (snd (extractP (fst (alts ! i)))) = length vs;
   fst (assert ! i) ⊆ dom (snd (assert ! i));
   z∈fst (assert ! i);  z ∉ set (snd (extractP (fst (alts ! i))));
   length alts = length assert;
   length alts > 0;
   closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {};
   dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
   x∈ dom E1; 
   i < length alts |] 
 ==>
  closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k) ∩
  recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) z (h, k) ≠ {}"
apply (elim conjE)
apply (subgoal_tac "closure (E1, E2) x (h, k) = 
                    closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k)")
 prefer 2 apply (simp, rule closure_monotone_extend_2,simp,assumption+,simp,simp)    
apply (subgoal_tac "z ∈ dom E1")
apply (subgoal_tac "recReach (E1, E2) z (h, k) = 
                    recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) z (h, k)")
 prefer 2 apply (rule recReach_monotone_extend_2,simp,assumption+,simp) 
apply (subgoal_tac "z ∈ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
 prefer 2 apply blast
by (rule extend_prop1,assumption+)

end