2   Generic Separation Logic

     2   Generic Separation Logic

     3 *}

     3 *}

     4 

     4 

     5 theory Hoare_gen

     5 theory Hoare_gen

     6 imports Main  

     6 imports Main  

     8   "../Separation_Algebra/Sep_Tactics"

     7   "../Separation_Algebra/Sep_Tactics"

     9 begin

     8 begin

    12 

     9 

    13 definition pasrt :: "bool \<Rightarrow> (('a::sep_algebra) \<Rightarrow> bool)" ("<_>" [72] 71)

    10 definition pasrt :: "bool \<Rightarrow> (('a::sep_algebra) \<Rightarrow> bool)" ("<_>" [72] 71)

    14 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"

    11 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"

    15 

    12 

    16 lemma sep_conj_cond1: "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"

    13 lemma sep_conj_cond1: "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"