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