src/HOL/Hoare_Parallel/RG_Com.thy
author wenzelm
Wed Apr 10 21:20:35 2013 +0200 (2013-04-10)
changeset 51692 ecd34f863242
parent 42174 d0be2722ce9f
child 58249 180f1b3508ed
permissions -rw-r--r--
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;
     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