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`