Theory BasicFacts

(*  Title:      BasicFacts
    Author:     Javier de Dios and Ricardo Peña
    Copyright:  February 2010, Universidad Complutense de Madrid
*)


header {* Basic Facts *}


theory BasicFacts imports SafeRegion_definitions

begin

(** Axioms **)

(* If μ maps range(ϑ) to some other region type, and polymorphic
   type variables of the types in ϑ to arbitrary type, and  e \<turnstile> ϑ \<leadsto> t
   holds, then  e \<turnstile> μ(ϑ) \<leadsto> μ(t) also holds  *)
axioms Regions_Lemma_5:
  "[| e : \<lbrace> (ϑ1,ϑ2),  t \<rbrace> |] 
   ==> e : \<lbrace> ((mu_ext (μ1,μ2)) of ϑ1, (μ2 om ϑ2)), (mu_ext (μ1,μ2) t) \<rbrace> "

axioms Regions_Lemma_5_Depth:
  "[| e  :f , n  \<lbrace> (ϑ1,ϑ2),  t \<rbrace> |] 
   ==> e  :f , n  \<lbrace> ((mu_ext (μ1,μ2)) of ϑ1, (μ2 om ϑ2)), (mu_ext (μ1,μ2) t) \<rbrace> "



axioms ρfake_not_in_dom_η:
  "ρfake ∉ dom η"


axioms no_cycles:
  "h p = Some (j, C, vn) 
  ==> ∀ i < length vn. p ∉ closureV (vn!i) (h,k)"

axioms fresh_notin_closureL:
  "fresh p h
   ==> ∀ q ∈ dom h. p ∉ closureL q (h,k)"


axioms semantic_extend_pointers:
 "(E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r 
  ==> (∀p∈dom h. p ∉ dom h' ∨ h p = h' p)"

axioms semantic_no_capture_h:
  "[| (E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r ; 
      v' ∈ rangeHeap h - domLoc h |] 
  ==> v' ∉ domLoc h'"

axioms semantic_no_capture_E1:
  "[| (E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r ; 
      E1  x = Some (Loc p); 
      p ∉ dom h |] 
  ==> p ∉ dom h'"

axioms semantic_no_capture_E1_fresh:
  "[| (E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r ; 
      fresh p h |] 
  ==> ∀ x ∈ dom E1. ∀ q. E1 x = Some (Loc q) --> p ≠ q"

axioms semantic_no_capture_E1_fresh_2:
  "[| (E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r ; 
      fresh p h |] 
  ==> ∀ x ∈ dom E1. ∀ q. E1 x = Some (Loc q) --> p ∉ closureL q (h,k)"

axioms semantic_no_capture_E1_fresh_2_semDepth:
  "[| (E1, E2) \<turnstile> h , k , e \<Down>(f,n)  h' , k , v; 
      fresh p h |] 
  ==> ∀ x ∈ dom E1. ∀ q. E1 x = Some (Loc q) --> p ∉ closureL q (h,k)"



axioms closureV_equals_closureL:
  "h p = Some (j,C,vs)
   ==> closureL p (h,k) = (\<Union> i < length vs. closureV (vs!i) (h,k)) ∪ {p}"

axioms closureV_subseteq_closureL_None:
  "h p = Some (j,C,vs)
   ==> (\<Union> i < length vs. closureV (vs!i) (h(p:=None),k)) ⊆ closureL p (h(p:=None),k)"


(* Pendiente demostrar *)
axioms SafeDARegion_Var2_2:
  "∀i<length tn'. consistent_v (mu_ext (μ1, μ2) (tn' ! i)) η' (vn ! i) h
   ==> ∀i<length (snd (mapAccumL (copy' j) h (zip vn (recursiveArgs C)))).
       consistent_v (map (mu_ext (μ1, μ2(ρ \<mapsto> ρ'))) tn' ! i) η' 
                    (snd (mapAccumL (copy' j) h (zip vn (recursiveArgs C))) ! i) h'"


(* Este axioma quiza habria que incluirlo como premisa 
   en la semantica *)
axioms dom_copy':
 "copy (h, k) p j = ((h', k), p')
  ==> copy'_dom (j, h, Loc p, True)"




end