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