src/HOL/Hoare_Parallel/OG_Com.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (20 months ago) changeset 67022 49309fe530fd parent 62390 842917225d56 permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
```     1 chapter \<open>The Owicki-Gries Method\<close>
```
```     2
```
```     3 section \<open>Abstract Syntax\<close>
```
```     4
```
```     5 theory OG_Com imports Main begin
```
```     6
```
```     7 text \<open>Type abbreviations for boolean expressions and assertions:\<close>
```
```     8
```
```     9 type_synonym 'a bexp = "'a set"
```
```    10 type_synonym 'a assn = "'a set"
```
```    11
```
```    12 text \<open>The syntax of commands is defined by two mutually recursive
```
```    13 datatypes: \<open>'a ann_com\<close> for annotated commands and \<open>'a
```
```    14 com\<close> for non-annotated commands.\<close>
```
```    15
```
```    16 datatype 'a ann_com =
```
```    17      AnnBasic "('a assn)"  "('a \<Rightarrow> 'a)"
```
```    18    | AnnSeq "('a ann_com)"  "('a ann_com)"
```
```    19    | AnnCond1 "('a assn)"  "('a bexp)"  "('a ann_com)"  "('a ann_com)"
```
```    20    | AnnCond2 "('a assn)"  "('a bexp)"  "('a ann_com)"
```
```    21    | AnnWhile "('a assn)"  "('a bexp)"  "('a assn)"  "('a ann_com)"
```
```    22    | AnnAwait "('a assn)"  "('a bexp)"  "('a com)"
```
```    23 and 'a com =
```
```    24      Parallel "('a ann_com option \<times> 'a assn) list"
```
```    25    | Basic "('a \<Rightarrow> 'a)"
```
```    26    | Seq "('a com)"  "('a com)"
```
```    27    | Cond "('a bexp)"  "('a com)"  "('a com)"
```
```    28    | While "('a bexp)"  "('a assn)"  "('a com)"
```
```    29
```
```    30 text \<open>The function \<open>pre\<close> extracts the precondition of an
```
```    31 annotated command:\<close>
```
```    32
```
```    33 primrec pre ::"'a ann_com \<Rightarrow> 'a assn"  where
```
```    34   "pre (AnnBasic r f) = r"
```
```    35 | "pre (AnnSeq c1 c2) = pre c1"
```
```    36 | "pre (AnnCond1 r b c1 c2) = r"
```
```    37 | "pre (AnnCond2 r b c) = r"
```
```    38 | "pre (AnnWhile r b i c) = r"
```
```    39 | "pre (AnnAwait r b c) = r"
```
```    40
```
```    41 text \<open>Well-formedness predicate for atomic programs:\<close>
```
```    42
```
```    43 primrec atom_com :: "'a com \<Rightarrow> bool" where
```
```    44   "atom_com (Parallel Ts) = False"
```
```    45 | "atom_com (Basic f) = True"
```
```    46 | "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
```
```    47 | "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
```
```    48 | "atom_com (While b i c) = atom_com c"
```
```    49
```
```    50 end
```