Theory SafeDAss_P1

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


header {* Derived Assertions. P1. Semantic *}

theory SafeDAss_P1 imports SafeDAssBasic
begin

text{*
Lemmas for REUSE
*}

lemma P1_REUSE:
  "[| (E1,E2) \<turnstile> h,k,td,(ReuseE x a)\<Down> hh,k,v,r |]  
   ==> ∃ p q c . E1 x = Some (Loc p)
      ∧ h p = Some c
      ∧ fresh q h
      ∧ hh = (h(p:=None))(q \<mapsto> c) 
      ∧ v = Loc q"
apply (ind_cases "(E1,E2) \<turnstile> h,k,td,(ReuseE x a)\<Down> hh,k,v,r")
by force


text{*
Lemmas for COPY
*}

lemma P1_COPY:
  "[| (E1, E2) \<turnstile> h , k , td , x @ r a \<Down> hh , k , v , rs |]  
   ==> ∃ p p' j . E1 x = Some (Loc p)
      ∧ E2 r = Some j
      ∧ j <= k
      ∧ copy (h,k) p j = ((hh,k),p') 
      ∧ def_copy p (h,k)
      ∧ v = Loc p'"
apply (ind_cases "(E1, E2) \<turnstile> h , k , td , x @ r a \<Down> hh , k , v , rs")
by force


text{*
Lemmas for LET1 and LET2
*}

lemma P1_LET:
  "[| ∀ C as r a'. e1 ≠  ConstrE C as r a'; 
     (E1,E2) \<turnstile> h, k, td, Let x1 = e1 In e2 a\<Down>  hh, k,v2, r' |]  
   ==> ∃ h' v1 r'' r'''. (E1,E2) \<turnstile> h, k, 0, e1\<Down> h', k ,v1, r''
      ∧ (E1(x1 \<mapsto>  v1),E2) \<turnstile> h', k, (td+1), e2 \<Down> hh,k,v2,r'''
      ∧ x1 ∉ dom E1"
apply (ind_cases "(E1,E2) \<turnstile> h, k, td, Let x1 = e1 In e2 a\<Down> hh, k,v2,r'")
prefer 2 
apply (erule_tac x="C" in allE)
apply (erule_tac x="as" in allE)
apply (erule_tac x="r" in allE)
apply (erule_tac x="a'" in allE)
apply simp
apply (rule_tac x="h'" in exI)
apply (rule_tac x="v1" in exI)
apply (rule_tac x="(δ1, m1, s1)" in exI)
apply (rule_tac x="(δ2, m2, s2)" in exI)
by simp


lemma P1_f_n_LET:
  "[| ∀ C as r a'. e1 ≠  ConstrE C as r a'; 
     (E1,E2) \<turnstile> h,  k , Let x1 = e1 In e2 a  \<Down>(f, n)  h'', k, v2|]  
   ==> ∃ h' v1. 
          (E1,E2) \<turnstile> h, k, e1 \<Down>(f,n) h', k, v1
       ∧ (E1(x1 \<mapsto> v1),E2) \<turnstile> h', k, e2 \<Down>(f,n) h'', k, v2
       ∧ x1 ∉ dom E1"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all) 
apply (elim conjE)
apply (rule_tac x=h' in exI)
apply (rule_tac x=v1 in exI)
apply (rule conjI)
apply (rule_tac x=n1 in exI,simp)
apply (rule_tac x=n2 in exI,simp)
done


lemma P1_LETC:
  "[|(E1,E2) \<turnstile> h,k, td, Let x1 = ConstrE C as r a' In e2 a \<Down> hh,k,v,rs |]  
   ==> ∃ rs' p j. 
       (E1(x1 \<mapsto> Val.Loc p),E2) \<turnstile> h(p \<mapsto> (j,(C,map (atom2val E1) as))),k, (td+1),e2 \<Down> hh,k,v,rs'
      ∧ x1 ∉ dom E1
      ∧ fresh p h
      ∧ E2 r = Some j
      ∧ j ≤ k
      ∧ r ≠ self"
apply (ind_cases "(E1,E2) \<turnstile> h,k, td, Let x1 = ConstrE C as r a' In e2 a \<Down> hh,k,v,rs")
by force+


lemma P1_f_n_LETC:
  "[| (E1, E2) \<turnstile> h , k , Let x1 = ConstrE C as r a' In e2 a  \<Down> (f, n)  hh , k , v|]  
   ==> ∃ rs' p j. 
          (E1(x1 \<mapsto> Loc p), E2) \<turnstile> h(p \<mapsto> (j, C, map (atom2val E1) as)) , k , e2  \<Down> (f, n)  hh , k , v
        ∧ x1 ∉ dom E1
        ∧ fresh p h
        ∧ E2 r = Some j
        ∧ j ≤ k
        ∧ r ≠ self"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all) 
apply force
apply force
done


text{*
Lemmas for CASE
*}


lemma P1_CASE:
  "[| E1 x  = Some (Val.Loc p); 
    (E1,E2) \<turnstile> h,k,td, Case (VarE x a) Of alts a \<Down> h',k,v,r |]
    ==> ∃ j C vs. h p  = Some (j,C,vs) ∧
        (∃ i < length alts. ∃ td r.
          def_extend E1 (snd (extractP (fst (alts ! i)))) vs
       ∧ (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) \<turnstile> h , k , td , snd (alts ! i) \<Down> h' , k , v , r)"
apply (ind_cases "(E1,E2) \<turnstile> h,k, td, Case (VarE x a) Of alts a \<Down> h',k,v,r",clarsimp)
apply (rule_tac x="i" in exI,force)
by (simp_all)



lemma P1_CASE_1_1:
  "[| E1 x  = Some (IntT n); 
    (E1,E2) \<turnstile> h,k,td, Case (VarE x a) Of alts a' \<Down> hh,k,v,r |]
   ==> (∃ i < length alts.
       (∃ td r. (E1,E2) \<turnstile> h,k, td, snd (alts ! i) \<Down> hh,k,v,r
                 ∧ fst (alts ! i) = ConstP (LitN n)))"
apply (ind_cases "(E1,E2) \<turnstile> h,k, td, Case (VarE x a) Of alts a' \<Down> hh,k,v,r",clarsimp)
apply (rule_tac x="i" in exI,force)
by (simp_all)


lemma P1_CASE_1_2:
  "[| E1 x  = Some (BoolT b); 
    (E1,E2) \<turnstile> h,k,td, Case (VarE x a) Of alts a' \<Down> hh,k,v,r |]
   ==> (∃ i < length alts.
        ∃  td r. (E1,E2) \<turnstile> h,k, td, snd (alts ! i) \<Down> hh,k,v,r
                ∧  fst (alts ! i) = ConstP (LitB b))"
apply (ind_cases "(E1,E2) \<turnstile> h,k, td, Case (VarE x a) Of alts a' \<Down> hh,k,v,r",clarsimp)
apply (rule_tac x="i" in exI,force)
by force


lemma P1_f_n_CASE:
  "[| E1 x  = Some (Val.Loc p); 
    (E1, E2) \<turnstile> h , k , Case VarE x a Of alts a'  \<Down> (f, n)  hh , k , v|]
    ==> ∃ j C vs. h p  = Some (j,C,vs) ∧
        (∃ i < length alts. 
          def_extend E1 (snd (extractP (fst (alts ! i)))) vs
       ∧ (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) \<turnstile> h , k , snd (alts ! i) \<Down>(f, n) hh , k , v)"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all) 
by force


lemma P1_f_n_CASE_1_1:
  "[| E1 x  = Some (IntT n'); 
    (E1, E2) \<turnstile> h , k , Case VarE x a Of alts a'  \<Down> (f, n)  hh , k , v|]
   ==> (∃ i < length alts.
       ((E1, E2) \<turnstile> h , k ,  snd (alts ! i) \<Down> (f, n)  hh , k , v 
        ∧ fst (alts ! i) = ConstP (LitN n')))"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all) 
by force


lemma P1_f_n_CASE_1_2:
  "[| E1 x  = Some (BoolT b); 
    (E1, E2) \<turnstile> h , k , Case VarE x a Of alts a'  \<Down> (f, n)  hh , k , v|]
   ==> (∃ i < length alts.
       (E1, E2) \<turnstile> h , k ,  snd (alts ! i) \<Down> (f, n)  hh , k , v 
       ∧  fst (alts ! i) = ConstP (LitB b))"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all) 
by force


text{*
Lemmas for CASED
*}


lemma P1_CASED: 
  "[|(E1,E2) \<turnstile> h,k, td,CaseD (VarE x a) Of alts a' \<Down> hh,kk,v,r |] 
    ==> ∃ p j C vs. E1 x = Some (Loc p) ∧ h p  = Some (j,C,vs) ∧
        (∃ i < length alts. ∃ td r.
          def_extend E1 (snd (extractP (fst (alts ! i)))) vs
       ∧ (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) \<turnstile>  h(p := None), k, td, snd (alts ! i) \<Down>hh,k , v, r)"
apply (ind_cases "(E1,E2) \<turnstile> h,k, td, CaseD (VarE x a) Of alts a' \<Down> hh,kk,v,r",clarsimp)
by (rule_tac x="i" in exI,force)


lemma P1_f_n_CASED: 
  "[|(E1,E2) \<turnstile> h,k,CaseD (VarE x a) Of alts a' \<Down>(f,n)  hh,kk,v |] 
    ==> ∃ p j C vs. E1 x = Some (Loc p) ∧ h p  = Some (j,C,vs) ∧
        (∃ i < length alts. 
          def_extend E1 (snd (extractP (fst (alts ! i)))) vs
       ∧ (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) \<turnstile>  h(p := None), k, snd (alts ! i) \<Down>(f,n) hh,k , v)"
apply (simp add: SafeBoundSem_def)
apply (elim conjE, elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all) 
by force


text{*
Lemmas for APP
*}

lemma P1_APP:
 "[| (E1, E2) \<turnstile> h , k , td , AppE f as rs' a \<Down> hh , k , v , r; primops f = None;
    Σf f = Some (xs, rs, ef) |] 
  ==> ∃ h' δ m s. 
      (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) \<turnstile> 
       h , Suc k , (length as + length rs) , ef \<Down> h' , Suc k , v , (δ, m, s) 
    ∧ length xs = length as
    ∧ distinct xs
    ∧ length rs = length rs'
    ∧ distinct rs
    ∧  hh =  h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}
    ∧ dom E1 ∩ set xs = {}" 
apply (ind_cases "(E1, E2) \<turnstile> h , k , td , AppE f as rs' a \<Down> hh , k , v , r",clarsimp)
apply (rule_tac x=h' in exI)
apply (rule_tac x=δ in exI)
apply (rule_tac x=m in exI)
apply (rule_tac x=s in exI)
by (rule conjI,simp,simp)



lemma P1_f_n_APP:
 "[| (E1, E2) \<turnstile> h , k , AppE f as rs' a \<Down>(f,n) hh , k , v; primops f = None;
    Σf f = Some (xs, rs, ef) |] 
  ==> ∃ h'. 
      (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) \<turnstile> 
       h , Suc k , ef \<Down>(f,n) h' , Suc k , v  
    ∧ length xs = length as
    ∧ distinct xs
    ∧ length rs = length rs'
    ∧ distinct rs
    ∧  hh =  h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}
    ∧ dom E1 ∩ set xs = {}
    ∧ n > 0" 
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
apply clarsimp
by force


lemma P1_f_n_ge_0_APP:
 "[| (E1, E2) \<turnstile> h , k , AppE f as rs' a \<Down>(f,Suc n) hh , k , v; primops f = None;
    Σf f = Some (xs, rs, ef) |] 
  ==> ∃ h'. 
      (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) \<turnstile> 
       h , Suc k , ef \<Down>(f,n) h' , Suc k , v  
    ∧ length xs = length as
    ∧ distinct xs
    ∧ length rs = length rs'
    ∧ distinct rs
    ∧  hh =  h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}
    ∧ dom E1 ∩ set xs = {}" 
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
apply clarsimp
by auto


lemma P1_f_n_APP_2:
 "[| (E1, E2) \<turnstile> h , k , AppE g as rs' a \<Down>(f,n) hh , k , v; primops g = None; f≠g;
    Σf g = Some (xs, rs, ef) |] 
  ==> ∃ h'. 
      (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) \<turnstile> 
       h , Suc k, ef \<Down>(f,n) h' , Suc k , v 
    ∧ length xs = length as
    ∧ distinct xs
    ∧ length rs = length rs'
    ∧ distinct rs
    ∧  hh =  h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}
    ∧ dom E1 ∩ set xs = {}" 
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
apply clarsimp
by force


end