src/HOL/Hoare_Parallel/OG_Com.thy
changeset 39246 9e58f0499f57
parent 32621 a073cb249a06
child 42174 d0be2722ce9f
     1.1 --- a/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Sep 08 13:25:22 2010 +0200
     1.2 +++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Sep 08 19:21:46 2010 +0200
     1.3 @@ -32,24 +32,21 @@
     1.4  text {* The function @{text pre} extracts the precondition of an
     1.5  annotated command: *}
     1.6  
     1.7 -consts
     1.8 -  pre ::"'a ann_com \<Rightarrow> 'a assn" 
     1.9 -primrec 
    1.10 +primrec pre ::"'a ann_com \<Rightarrow> 'a assn"  where
    1.11    "pre (AnnBasic r f) = r"
    1.12 -  "pre (AnnSeq c1 c2) = pre c1"
    1.13 -  "pre (AnnCond1 r b c1 c2) = r"
    1.14 -  "pre (AnnCond2 r b c) = r"
    1.15 -  "pre (AnnWhile r b i c) = r"
    1.16 -  "pre (AnnAwait r b c) = r"
    1.17 +| "pre (AnnSeq c1 c2) = pre c1"
    1.18 +| "pre (AnnCond1 r b c1 c2) = r"
    1.19 +| "pre (AnnCond2 r b c) = r"
    1.20 +| "pre (AnnWhile r b i c) = r"
    1.21 +| "pre (AnnAwait r b c) = r"
    1.22  
    1.23  text {* Well-formedness predicate for atomic programs: *}
    1.24  
    1.25 -consts atom_com :: "'a com \<Rightarrow> bool"
    1.26 -primrec  
    1.27 +primrec atom_com :: "'a com \<Rightarrow> bool" where
    1.28    "atom_com (Parallel Ts) = False"
    1.29 -  "atom_com (Basic f) = True"
    1.30 -  "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
    1.31 -  "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
    1.32 -  "atom_com (While b i c) = atom_com c"
    1.33 +| "atom_com (Basic f) = True"
    1.34 +| "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
    1.35 +| "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
    1.36 +| "atom_com (While b i c) = atom_com c"
    1.37    
    1.38  end
    1.39 \ No newline at end of file