src/HOL/Hoare_Parallel/RG_Com.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 42174 d0be2722ce9f
child 58249 180f1b3508ed
permissions -rw-r--r--
tuned proofs;
prensani@13020
     1
prensani@13020
     2
header {* \chapter{The Rely-Guarantee Method} 
prensani@13020
     3
prensani@13020
     4
\section {Abstract Syntax}
prensani@13020
     5
*}
prensani@13020
     6
haftmann@16417
     7
theory RG_Com imports Main begin
prensani@13020
     8
prensani@13020
     9
text {* Semantics of assertions and boolean expressions (bexp) as sets
prensani@13020
    10
of states.  Syntax of commands @{text com} and parallel commands
prensani@13020
    11
@{text par_com}. *}
prensani@13020
    12
wenzelm@42174
    13
type_synonym 'a bexp = "'a set"
prensani@13020
    14
prensani@13020
    15
datatype 'a com = 
prensani@13020
    16
    Basic "'a \<Rightarrow>'a"
prensani@13020
    17
  | Seq "'a com" "'a com"
prensani@13020
    18
  | Cond "'a bexp" "'a com" "'a com"         
prensani@13020
    19
  | While "'a bexp" "'a com"       
prensani@13020
    20
  | Await "'a bexp" "'a com"                 
prensani@13020
    21
wenzelm@42174
    22
type_synonym 'a par_com = "'a com option list"
prensani@13020
    23
prensani@13020
    24
end