src/HOL/Hoare_Parallel/OG_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
 prensani@13020 1 prensani@13020 2 header {* \chapter{The Owicki-Gries Method} prensani@13020 3 prensani@13020 4 \section{Abstract Syntax} *} prensani@13020 5 haftmann@16417 6 theory OG_Com imports Main begin prensani@13020 7 prensani@13020 8 text {* Type abbreviations for boolean expressions and assertions: *} prensani@13020 9 wenzelm@42174 10 type_synonym 'a bexp = "'a set" wenzelm@42174 11 type_synonym 'a assn = "'a set" prensani@13020 12 prensani@13020 13 text {* The syntax of commands is defined by two mutually recursive prensani@13020 14 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a prensani@13020 15 com"} for non-annotated commands. *} prensani@13020 16 prensani@13020 17 datatype 'a ann_com = prensani@13020 18 AnnBasic "('a assn)" "('a \ 'a)" prensani@13020 19 | AnnSeq "('a ann_com)" "('a ann_com)" prensani@13020 20 | AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)" prensani@13020 21 | AnnCond2 "('a assn)" "('a bexp)" "('a ann_com)" prensani@13020 22 | AnnWhile "('a assn)" "('a bexp)" "('a assn)" "('a ann_com)" prensani@13020 23 | AnnAwait "('a assn)" "('a bexp)" "('a com)" prensani@13020 24 and 'a com = prensani@13020 25 Parallel "('a ann_com option \ 'a assn) list" prensani@13020 26 | Basic "('a \ 'a)" prensani@13020 27 | Seq "('a com)" "('a com)" prensani@13020 28 | Cond "('a bexp)" "('a com)" "('a com)" prensani@13020 29 | While "('a bexp)" "('a assn)" "('a com)" prensani@13020 30 prensani@13020 31 text {* The function @{text pre} extracts the precondition of an prensani@13020 32 annotated command: *} prensani@13020 33 haftmann@39246 34 primrec pre ::"'a ann_com \ 'a assn" where prensani@13020 35 "pre (AnnBasic r f) = r" haftmann@39246 36 | "pre (AnnSeq c1 c2) = pre c1" haftmann@39246 37 | "pre (AnnCond1 r b c1 c2) = r" haftmann@39246 38 | "pre (AnnCond2 r b c) = r" haftmann@39246 39 | "pre (AnnWhile r b i c) = r" haftmann@39246 40 | "pre (AnnAwait r b c) = r" prensani@13020 41 prensani@13020 42 text {* Well-formedness predicate for atomic programs: *} prensani@13020 43 haftmann@39246 44 primrec atom_com :: "'a com \ bool" where prensani@13020 45 "atom_com (Parallel Ts) = False" haftmann@39246 46 | "atom_com (Basic f) = True" haftmann@39246 47 | "atom_com (Seq c1 c2) = (atom_com c1 \ atom_com c2)" haftmann@39246 48 | "atom_com (Cond b c1 c2) = (atom_com c1 \ atom_com c2)" haftmann@39246 49 | "atom_com (While b i c) = atom_com c" prensani@13020 50 prensani@13020 51 end