src/HOL/Hoare_Parallel/OG_Com.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 62390 842917225d56
permissions -rw-r--r--
more robust sorted_entries;
     1 chapter \<open>The Owicki-Gries Method\<close>
     2 
     3 section \<open>Abstract Syntax\<close>
     4 
     5 theory OG_Com imports Main begin
     6 
     7 text \<open>Type abbreviations for boolean expressions and assertions:\<close>
     8 
     9 type_synonym 'a bexp = "'a set"
    10 type_synonym 'a assn = "'a set"
    11 
    12 text \<open>The syntax of commands is defined by two mutually recursive
    13 datatypes: \<open>'a ann_com\<close> for annotated commands and \<open>'a
    14 com\<close> for non-annotated commands.\<close>
    15 
    16 datatype 'a ann_com =
    17      AnnBasic "('a assn)"  "('a \<Rightarrow> 'a)"
    18    | AnnSeq "('a ann_com)"  "('a ann_com)"
    19    | AnnCond1 "('a assn)"  "('a bexp)"  "('a ann_com)"  "('a ann_com)"
    20    | AnnCond2 "('a assn)"  "('a bexp)"  "('a ann_com)"
    21    | AnnWhile "('a assn)"  "('a bexp)"  "('a assn)"  "('a ann_com)"
    22    | AnnAwait "('a assn)"  "('a bexp)"  "('a com)"
    23 and 'a com =
    24      Parallel "('a ann_com option \<times> 'a assn) list"
    25    | Basic "('a \<Rightarrow> 'a)"
    26    | Seq "('a com)"  "('a com)"
    27    | Cond "('a bexp)"  "('a com)"  "('a com)"
    28    | While "('a bexp)"  "('a assn)"  "('a com)"
    29 
    30 text \<open>The function \<open>pre\<close> extracts the precondition of an
    31 annotated command:\<close>
    32 
    33 primrec pre ::"'a ann_com \<Rightarrow> 'a assn"  where
    34   "pre (AnnBasic r f) = r"
    35 | "pre (AnnSeq c1 c2) = pre c1"
    36 | "pre (AnnCond1 r b c1 c2) = r"
    37 | "pre (AnnCond2 r b c) = r"
    38 | "pre (AnnWhile r b i c) = r"
    39 | "pre (AnnAwait r b c) = r"
    40 
    41 text \<open>Well-formedness predicate for atomic programs:\<close>
    42 
    43 primrec atom_com :: "'a com \<Rightarrow> bool" where
    44   "atom_com (Parallel Ts) = False"
    45 | "atom_com (Basic f) = True"
    46 | "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
    47 | "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
    48 | "atom_com (While b i c) = atom_com c"
    49 
    50 end