src/HOL/Hoare_Parallel/RG_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 Rely-Guarantee Method} 
     3 
     4 \section {Abstract Syntax}
     5 *}
     6 
     7 theory RG_Com imports Main begin
     8 
     9 text {* Semantics of assertions and boolean expressions (bexp) as sets
    10 of states.  Syntax of commands @{text com} and parallel commands
    11 @{text par_com}. *}
    12 
    13 type_synonym 'a bexp = "'a set"
    14 
    15 datatype 'a com = 
    16     Basic "'a \<Rightarrow>'a"
    17   | Seq "'a com" "'a com"
    18   | Cond "'a bexp" "'a com" "'a com"         
    19   | While "'a bexp" "'a com"       
    20   | Await "'a bexp" "'a com"                 
    21 
    22 type_synonym 'a par_com = "'a com option list"
    23 
    24 end