src/HOL/Hoare_Parallel/OG_Com.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 42174 d0be2722ce9f
child 58249 180f1b3508ed
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
     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 type_synonym 'a bexp = "'a set"
    11 type_synonym 'a assn = "'a set"
    12 
    13 text {* The syntax of commands is defined by two mutually recursive
    14 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
    15 com"} for non-annotated commands. *}
    16 
    17 datatype 'a ann_com = 
    18      AnnBasic "('a assn)"  "('a \<Rightarrow> 'a)"         
    19    | AnnSeq "('a ann_com)"  "('a ann_com)"   
    20    | AnnCond1 "('a assn)"  "('a bexp)"  "('a ann_com)"  "('a ann_com)" 
    21    | AnnCond2 "('a assn)"  "('a bexp)"  "('a ann_com)" 
    22    | AnnWhile "('a assn)"  "('a bexp)"  "('a assn)"  "('a ann_com)" 
    23    | AnnAwait "('a assn)"  "('a bexp)"  "('a com)" 
    24 and 'a com = 
    25      Parallel "('a ann_com option \<times> 'a assn) list"
    26    | Basic "('a \<Rightarrow> 'a)" 
    27    | Seq "('a com)"  "('a com)" 
    28    | Cond "('a bexp)"  "('a com)"  "('a com)" 
    29    | While "('a bexp)"  "('a assn)"  "('a com)"
    30 
    31 text {* The function @{text pre} extracts the precondition of an
    32 annotated command: *}
    33 
    34 primrec pre ::"'a ann_com \<Rightarrow> 'a assn"  where
    35   "pre (AnnBasic r f) = r"
    36 | "pre (AnnSeq c1 c2) = pre c1"
    37 | "pre (AnnCond1 r b c1 c2) = r"
    38 | "pre (AnnCond2 r b c) = r"
    39 | "pre (AnnWhile r b i c) = r"
    40 | "pre (AnnAwait r b c) = r"
    41 
    42 text {* Well-formedness predicate for atomic programs: *}
    43 
    44 primrec atom_com :: "'a com \<Rightarrow> bool" where
    45   "atom_com (Parallel Ts) = False"
    46 | "atom_com (Basic f) = True"
    47 | "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
    48 | "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
    49 | "atom_com (While b i c) = atom_com c"
    50   
    51 end