src/HOL/Hoare_Parallel/RG_Com.thy
author wenzelm
Mon, 12 Sep 2022 22:52:15 +0200
changeset 76122 b8f26c20d3b1
parent 62390 842917225d56
permissions -rw-r--r--
ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration); tuned signature;

chapter \<open>The Rely-Guarantee Method\<close>

section \<open>Abstract Syntax\<close>

theory RG_Com imports Main begin

text \<open>Semantics of assertions and boolean expressions (bexp) as sets
of states.  Syntax of commands \<open>com\<close> and parallel commands
\<open>par_com\<close>.\<close>

type_synonym 'a bexp = "'a set"

datatype 'a com =
    Basic "'a \<Rightarrow>'a"
  | Seq "'a com" "'a com"
  | Cond "'a bexp" "'a com" "'a com"
  | While "'a bexp" "'a com"
  | Await "'a bexp" "'a com"

type_synonym 'a par_com = "'a com option list"

end