src/HOL/Hoare_Parallel/OG_Com.thy
changeset 39246 9e58f0499f57
parent 32621 a073cb249a06
child 42174 d0be2722ce9f
equal deleted inserted replaced
39215:7b2631c91a95 39246:9e58f0499f57
    30    | While "('a bexp)"  "('a assn)"  "('a com)"
    30    | While "('a bexp)"  "('a assn)"  "('a com)"
    31 
    31 
    32 text {* The function @{text pre} extracts the precondition of an
    32 text {* The function @{text pre} extracts the precondition of an
    33 annotated command: *}
    33 annotated command: *}
    34 
    34 
    35 consts
    35 primrec pre ::"'a ann_com \<Rightarrow> 'a assn"  where
    36   pre ::"'a ann_com \<Rightarrow> 'a assn" 
       
    37 primrec 
       
    38   "pre (AnnBasic r f) = r"
    36   "pre (AnnBasic r f) = r"
    39   "pre (AnnSeq c1 c2) = pre c1"
    37 | "pre (AnnSeq c1 c2) = pre c1"
    40   "pre (AnnCond1 r b c1 c2) = r"
    38 | "pre (AnnCond1 r b c1 c2) = r"
    41   "pre (AnnCond2 r b c) = r"
    39 | "pre (AnnCond2 r b c) = r"
    42   "pre (AnnWhile r b i c) = r"
    40 | "pre (AnnWhile r b i c) = r"
    43   "pre (AnnAwait r b c) = r"
    41 | "pre (AnnAwait r b c) = r"
    44 
    42 
    45 text {* Well-formedness predicate for atomic programs: *}
    43 text {* Well-formedness predicate for atomic programs: *}
    46 
    44 
    47 consts atom_com :: "'a com \<Rightarrow> bool"
    45 primrec atom_com :: "'a com \<Rightarrow> bool" where
    48 primrec  
       
    49   "atom_com (Parallel Ts) = False"
    46   "atom_com (Parallel Ts) = False"
    50   "atom_com (Basic f) = True"
    47 | "atom_com (Basic f) = True"
    51   "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
    48 | "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
    52   "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
    49 | "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
    53   "atom_com (While b i c) = atom_com c"
    50 | "atom_com (While b i c) = atom_com c"
    54   
    51   
    55 end
    52 end