Theory SafeDAssBasic

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

header {* SafeDAssBasic *}

(*<*)
theory SafeDAssBasic
imports TypeEnvironment SafeDepthSemantics "../SafeImp/ClosureHeap"
begin
(*>*)

constdefs SSet :: "string set => TypeEnvironment => Environment => Heap => Location set"
"SSet L Γ E h ≡ let LS = {z∈L. Γ z = Some s''} 
                 in (\<Union>x∈LS. closure E x h)"

constdefs SSet1 :: "string set => TypeEnvironment => TypeEnvironment => Mark => Environment => Heap => Location set"
"SSet1 L Γ1 Γ m E h ≡ (\<Union>x∈{z∈L. Γ z = (Some m) ∧ Γ1 z = (Some s'')}. closure E x h)"


constdefs RSet :: "string set => TypeEnvironment => Environment => Heap => Location set"
"RSet L Γ E h ≡  {p ∈ live E L h. ∃z∈ L. Γ z =  Some d'' ∧ 
                                          closureL p h ∩ recReach E z h ≠ {}}"


constdefs RSet1 :: "string set => TypeEnvironment => TypeEnvironment => Mark => Environment => Heap => Heap => Location set"
"RSet1 L Γ1 Γ m E h hh ≡  {p ∈ live E L h. ∃z∈ L. Γ z = Some m ∧ Γ1 z =  Some d'' ∧ 
                                          closureL p h ∩ recReach E z h ≠ {}} ∪ 
                           {p ∈ scope E h.  ¬identityClosureL p h hh }"

constdefs RSet2 :: "string set => string set => TypeEnvironment => Environment => Heap => Location set"
"RSet2 L L' Γ E h ≡  {p ∈ live E L' h. ∃z∈ L. Γ z =  Some d'' ∧ 
                                          closureL p h ∩ recReach E z h ≠ {}}"


constdefs shareRec :: "string set => TypeEnvironment => Environment => Heap => Heap => bool"
"shareRec L Γ E h hh ≡ (∀x∈ dom (fst E). ∀  z ∈ L. Γ z = Some d'' ∧ 
                             closure E x h ∩ recReach E z h ≠ {} 
                             --> x ∈ dom Γ ∧ Γ x ≠ Some s'') 
                        ∧
                        (∀x∈ dom (fst E). ¬ identityClosure E x h hh 
                           --> x ∈ dom Γ ∧ Γ x ≠ Some s'')" 



constdefs wellFormed :: "string set => TypeEnvironment => unit Exp => bool"
"wellFormed L Γ e ≡ (∀ E1 E2 h k td hh v r.
                        (E1,E2) \<turnstile> h,k,td, e \<Down> hh,k,v,r 
                      ∧ dom Γ ⊆ dom E1
                      ∧ L ⊆ dom Γ
                      ∧ fv e ⊆ L 
                      --> (∀x∈ dom E1. ∀  z ∈ L. Γ z = Some d'' ∧ 
                           closure (E1,E2) x (h,k) ∩ recReach (E1,E2) z (h,k) ≠ {} 
                           --> x ∈ dom Γ ∧ Γ x ≠ Some s''))" 

constdefs wellFormedDepth :: "string => nat => string set => TypeEnvironment => unit Exp => bool"
"wellFormedDepth f n L Γ e ≡ (∀ E1 E2 h k hh v.
                             (E1,E2) \<turnstile> h,k, e \<Down>(f,n) hh,k,v
                           ∧ dom Γ ⊆ dom E1
                           ∧ L ⊆ dom Γ
                           ∧ fv e ⊆ L 
                          --> (∀x∈ dom E1. ∀  z ∈ L. Γ z = Some d'' ∧ 
                               closure (E1,E2) x (h,k) ∩ recReach (E1,E2) z (h,k) ≠ {} 
                              --> x ∈ dom Γ ∧ Γ x ≠ Some s''))" 


lemma imp_wellFormed_wellFormedDepth:
  "wellFormed L Γ e ==> wellFormedDepth f n L Γ e"
apply (simp only: wellFormed_def)
apply (simp only: wellFormedDepth_def)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="td" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="r" in allE)
apply (drule mp,simp)
by (frule impSemBoundRA,simp)


constdefs SR :: "string set => TypeEnvironment => Environment => Heap => Heap => string set"
"SR L Γ E h hh ≡ {x∈ dom (fst E). ∃ z ∈ L. Γ z = Some d'' ∧ closure E x h ∩ recReach E z h ≠ {}}"

(* for CASED *)
definition
  restrict_neg_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)"  where
  "restrict_neg_map m A = (λx. if x : A then None else m x)"


(* For APP *)
consts
  maps_of :: "('a * 'b) list => ('a ~=> 'b) list"

primrec
  "maps_of [] = [empty]"
  "maps_of (p#ps) = [fst p \<mapsto> snd p] # maps_of ps"


axioms z_in_SR:
  "¬ identityClosure (E1, E2) z (h, k) (h', k') ==> z ∈ SR L Γ (E1,E2) (h,k) (h',k')"


types MarkEnv   = "string \<rightharpoonup> Mark list"

(* Definition 3. e satisfies the static assertion \<lbrace>L,Γ\<rbrace> *)
constdefs SafeDAss ::
  "unit Exp => string set => TypeEnvironment => bool"  ("_ : \<lbrace> _ , _ \<rbrace>" 1000)
  " SafeDAss e L Γ ≡ 
       fv e ⊆ L ∧ L ⊆ dom Γ ∧ 
       (∀ E1 E2 h k td hh v r. 
         (E1,E2) \<turnstile> h,k,td, e \<Down> hh,k,v,r 
       ∧ dom Γ ⊆ dom E1
        --> shareRec L Γ (E1,E2) (h,k) (hh,k) 
           ∧  (closed (E1,E2) L (h,k) 
               ∧ SSet L Γ (E1,E2) (h,k) ∩  RSet L Γ (E1,E2) (h,k) = {}
     --> closed_f v (hh,k)))"

(* Definition 4. A mark environment ΣM is valid. \<Turnstile> ΣM *)
inductive 
    ValidGlobalMarkEnv :: "MarkEnv => bool" ("\<Turnstile>  _ " 1000) 

where
   base:  "  \<Turnstile>  empty"
|  step:  "[| \<Turnstile>  Σm; f ∉ dom Σm;
             Lf = set (varsAPP Σf f); Γf = empty ((varsAPP Σf f) [\<mapsto>] ms);
             (bodyAPP Σf f) : \<lbrace> Lf , Γf \<rbrace>|] ==> \<Turnstile>  Σm(f\<mapsto>ms)"


(* Definition 5. e satisfies the static assertion \<lbrace>L,Γ\<rbrace> in the context of ΣM *)
constdefs SafeDAssCntxt ::
  "unit Exp => MarkEnv => string set => TypeEnvironment => bool"  ("_ , _ :  \<lbrace> _ , _ \<rbrace>" 1000)
  "SafeDAssCntxt e Σm L Γ ≡  (\<Turnstile>  Σm --> e : \<lbrace> L , Γ \<rbrace>)"


(* Definition 7. the subexpresion e of f's body satisfies the static assertion \<lbrace>L,Γ\<rbrace> 
   up to depth n *)
constdefs SafeDAssDepth ::
  "unit Exp => string => nat => string set => TypeEnvironment => bool"   ("_ :_ , _ \<lbrace> _ , _ \<rbrace>" 1000)
  " SafeDAssDepth e f n L Γ ≡ 
       fv e ⊆ L ∧ L ⊆ dom Γ ∧ 
       (∀ E1 E2 h k hh v. 
         (E1,E2) \<turnstile> h, k, e \<Down>(f,n) hh, k, v
       ∧ dom Γ ⊆ dom E1
        --> shareRec L Γ (E1,E2) (h,k) (hh,k) 
           ∧  (closed (E1,E2) L (h,k) 
               ∧ SSet L Γ (E1,E2) (h,k) ∩  RSet L Γ (E1,E2) (h,k) = {}
     --> closed_f v (hh,k)))"


(* Definition 8. A mark environment ΣM is valid up to depth n for function f. \<Turnstile>f,n ΣM *)
inductive ValidGlobalMarkEnvDepth :: "string => nat => MarkEnv => bool"
                                     ("\<Turnstile>_ , _  _ " 1000)
where
   base   :  "[| \<Turnstile> Σm; f ∉ dom Σm|] ==> \<Turnstile>f,n Σm"
| depth0  :  "[| \<Turnstile> Σm; f ∉ dom Σm|] ==> \<Turnstile>f,0 Σm(f\<mapsto>ms)"
|  step   :  "[| \<Turnstile> Σm; f ∉ dom Σm;
                Lf = set (varsAPP Σf f); Γf = empty ((varsAPP Σf f) [\<mapsto>] ms);
                (bodyAPP Σf f) :f,n \<lbrace> Lf , Γf \<rbrace> |] ==>  \<Turnstile>f,Suc n Σm(f\<mapsto>ms)"
|  g      :  "[| \<Turnstile>f,n Σm; g ∉ dom Σm; g≠f; 
               Lg = set (varsAPP Σf g); Γg = empty ((varsAPP Σf g) [\<mapsto>] ms);
               (bodyAPP Σf g) : \<lbrace> Lg , Γg \<rbrace> |] ==>  \<Turnstile>f, n Σm(g\<mapsto>ms)"


(* Definition 9. the subexpresion e of f's body satisfies the static assertion \<lbrace>L,Γ\<rbrace> 
   up to depth n in the context of ΣM *)
constdefs SafeDAssDepthCntxt ::
  "unit Exp => MarkEnv => string => nat => string set => TypeEnvironment => bool"  ("_ , _ :_ , _ \<lbrace> _ , _ \<rbrace>" 1000)
  "SafeDAssDepthCntxt e Σm f n L Γ ≡  ( \<Turnstile>f,n Σm -->  e :f,n \<lbrace> L , Γ \<rbrace>)"



text{*
Lemmas
*}

(*********** LEMMAS *************)

lemma equals_recReach: 
  "[|z ≠ x1; z∈ L; Γ z = Some s''; identityClosure (E1,E2) z h hh|]
   ==> recReach (E1,E2) z h = recReach (E1(x1 \<mapsto> r), E2) z hh"
apply (subgoal_tac "z ≠ x1 ==> recReach (E1(x1 \<mapsto> r), E2) z hh = recReach (E1, E2) z hh",simp)
apply (erule identityClosure_equals_recReach)
 apply simp
by (simp add: recReach_def)


lemma monotone_identityClosure:
" [|x≠x1; identityClosure (E1, E2) x (h, k) (h', k');
   identityClosure (E1(x1 \<mapsto> r), E2) x (h', k') (hh, kk)|]
==> identityClosure (E1, E2) x (h, k) (hh, kk)"
apply (simp add: identityClosure_def)
apply (elim conjE)
apply (rule conjI)
 apply (simp add: closure_def)
apply (rule ballI)
apply (erule_tac x="p" in ballE)+
  apply simp
 apply (simp add: closure_def)
by simp

lemma unsafe_Gamma2_identityClosure:
  "[| L2 ⊆ dom (disjointUnionEnv Γ2  (empty(x1 \<mapsto> m)));
    def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
    dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m))) ⊆ insert x1 (dom E1); y ≠ x1;
    ∀x∈dom E1. (∃z∈L1. Γ1 z = Some d'' ∧ closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {}) --> x ∈ dom Γ1 ∧ Γ1 x ≠ Some s'';
    ∀x∈dom E1. ¬ identityClosure (E1, E2) x (h, k) (h', k') --> x ∈ dom Γ1 ∧ Γ1 x ≠ Some s'';
    def_pp Γ1 Γ2 L2;
    Γ2 y ≠ Some s''; y ∈ L2|] 
   ==> identityClosure (E1, E2) y (h, k) (h', k')"
apply (erule_tac x="y" in ballE)+
 prefer 2 apply blast
 prefer 2 apply blast
apply (frule_tac x="y" in safe_Gamma_triangle_3, assumption+)
apply (case_tac " ¬ identityClosure (E1, E2) y (h, k) (h', k')")
 apply simp
apply simp
done



lemma closure_subset_live:
"[|y ≠ x1; y ∈ L2|] ==> closure (E1,E2) y (h, k) ⊆ live (E1, E2) (L1 ∪ (L2 - {x1})) (h, k)"
apply (simp add: live_def add: closureLS_def)
apply blast
done

lemma closure_live_monotone:
"[|  p ∈ closure (E1(x1 \<mapsto> r), E2) y (h', k');
   closure (E1(x1 \<mapsto> r), E2) y (h', k') ⊆ live (E1, E2) (L1 ∪ (L2 - {x1})) (h, k) |] 
 ==>  p ∈ live (E1, E2) (L1 ∪ (L2 - {x1})) (h, k)"
apply blast
done


end