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