src/HOL/HoareParallel/OG_Com.thy
author haftmann
Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417 9bc16273c2d4
parent 13020 791e3b4c4039
permissions -rw-r--r--
migrated theory headers to new format
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     1
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
header {* \chapter{The Owicki-Gries Method} 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     3
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     4
\section{Abstract Syntax} *} 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     5
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13020
diff changeset
     6
theory OG_Com imports Main begin
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     7
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     8
text {* Type abbreviations for boolean expressions and assertions: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     9
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    10
types
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    11
    'a bexp = "'a set"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    12
    'a assn = "'a set"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    13
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    14
text {* The syntax of commands is defined by two mutually recursive
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    15
datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    16
com"} for non-annotated commands. *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    17
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    18
datatype 'a ann_com = 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    19
     AnnBasic "('a assn)"  "('a \<Rightarrow> 'a)"         
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    20
   | AnnSeq "('a ann_com)"  "('a ann_com)"   
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    21
   | AnnCond1 "('a assn)"  "('a bexp)"  "('a ann_com)"  "('a ann_com)" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    22
   | AnnCond2 "('a assn)"  "('a bexp)"  "('a ann_com)" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    23
   | AnnWhile "('a assn)"  "('a bexp)"  "('a assn)"  "('a ann_com)" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    24
   | AnnAwait "('a assn)"  "('a bexp)"  "('a com)" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    25
and 'a com = 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    26
     Parallel "('a ann_com option \<times> 'a assn) list"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    27
   | Basic "('a \<Rightarrow> 'a)" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    28
   | Seq "('a com)"  "('a com)" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    29
   | Cond "('a bexp)"  "('a com)"  "('a com)" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    30
   | While "('a bexp)"  "('a assn)"  "('a com)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    31
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    32
text {* The function @{text pre} extracts the precondition of an
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    33
annotated command: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    34
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    35
consts
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    36
  pre ::"'a ann_com \<Rightarrow> 'a assn" 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    37
primrec 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    38
  "pre (AnnBasic r f) = r"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    39
  "pre (AnnSeq c1 c2) = pre c1"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    40
  "pre (AnnCond1 r b c1 c2) = r"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    41
  "pre (AnnCond2 r b c) = r"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    42
  "pre (AnnWhile r b i c) = r"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    43
  "pre (AnnAwait r b c) = r"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    44
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    45
text {* Well-formedness predicate for atomic programs: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    46
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    47
consts atom_com :: "'a com \<Rightarrow> bool"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    48
primrec  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    49
  "atom_com (Parallel Ts) = False"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    50
  "atom_com (Basic f) = True"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    51
  "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    52
  "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    53
  "atom_com (While b i c) = atom_com c"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    54
  
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    55
end