src/HOL/Hoare_Parallel/OG_Com.thy
author haftmann
Wed Sep 08 19:21:46 2010 +0200 (2010-09-08)
changeset 39246 9e58f0499f57
parent 32621 a073cb249a06
child 42174 d0be2722ce9f
permissions -rw-r--r--
modernized primrec
     1 
     2 header {* \chapter{The Owicki-Gries Method} 
     3 
     4 \section{Abstract Syntax} *} 
     5 
     6 theory OG_Com imports Main begin
     7 
     8 text {* Type abbreviations for boolean expressions and assertions: *}
     9 
    10 types
    11     'a bexp = "'a set"
    12     'a assn = "'a set"
    13 
    14 text {* The syntax of commands is defined by two mutually recursive
    15 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
    16 com"} for non-annotated commands. *}
    17 
    18 datatype 'a ann_com = 
    19      AnnBasic "('a assn)"  "('a \<Rightarrow> 'a)"         
    20    | AnnSeq "('a ann_com)"  "('a ann_com)"   
    21    | AnnCond1 "('a assn)"  "('a bexp)"  "('a ann_com)"  "('a ann_com)" 
    22    | AnnCond2 "('a assn)"  "('a bexp)"  "('a ann_com)" 
    23    | AnnWhile "('a assn)"  "('a bexp)"  "('a assn)"  "('a ann_com)" 
    24    | AnnAwait "('a assn)"  "('a bexp)"  "('a com)" 
    25 and 'a com = 
    26      Parallel "('a ann_com option \<times> 'a assn) list"
    27    | Basic "('a \<Rightarrow> 'a)" 
    28    | Seq "('a com)"  "('a com)" 
    29    | Cond "('a bexp)"  "('a com)"  "('a com)" 
    30    | While "('a bexp)"  "('a assn)"  "('a com)"
    31 
    32 text {* The function @{text pre} extracts the precondition of an
    33 annotated command: *}
    34 
    35 primrec pre ::"'a ann_com \<Rightarrow> 'a assn"  where
    36   "pre (AnnBasic r f) = r"
    37 | "pre (AnnSeq c1 c2) = pre c1"
    38 | "pre (AnnCond1 r b c1 c2) = r"
    39 | "pre (AnnCond2 r b c) = r"
    40 | "pre (AnnWhile r b i c) = r"
    41 | "pre (AnnAwait r b c) = r"
    42 
    43 text {* Well-formedness predicate for atomic programs: *}
    44 
    45 primrec atom_com :: "'a com \<Rightarrow> bool" where
    46   "atom_com (Parallel Ts) = False"
    47 | "atom_com (Basic f) = True"
    48 | "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
    49 | "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
    50 | "atom_com (While b i c) = atom_com c"
    51   
    52 end