src/HOL/IMP/VC.thy
author oheimb
Tue Jul 04 10:54:46 2000 +0200 (2000-07-04)
changeset 9241 f961c1fdff50
parent 5183 89f162de39cf
child 12431 07ec657249e5
permissions -rw-r--r--
disambiguated := ; added Examples (factorial)
clasohm@1476
     1
(*  Title:      HOL/IMP/VC.thy
nipkow@1447
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
nipkow@1447
     4
    Copyright   1996 TUM
nipkow@1447
     5
nipkow@1447
     6
acom: annotated commands
nipkow@1447
     7
vc:   verification-conditions
nipkow@2810
     8
awp:   weakest (liberal) precondition
nipkow@1447
     9
*)
nipkow@1447
    10
nipkow@1447
    11
VC  =  Hoare +
nipkow@1447
    12
nipkow@1447
    13
datatype  acom = Askip
nipkow@1447
    14
               | Aass   loc aexp
nipkow@1447
    15
               | Asemi  acom acom
nipkow@1447
    16
               | Aif    bexp acom acom
nipkow@1447
    17
               | Awhile bexp assn acom
nipkow@1447
    18
nipkow@1447
    19
consts
nipkow@2810
    20
  vc,awp :: acom => assn => assn
nipkow@2810
    21
  vcawp :: "acom => assn => assn * assn"
nipkow@1447
    22
  astrip :: acom => com
nipkow@1447
    23
berghofe@5183
    24
primrec
nipkow@2810
    25
  "awp Askip Q = Q"
oheimb@9241
    26
  "awp (Aass x a) Q = (%s. Q(s[x::=a s]))"
nipkow@2810
    27
  "awp (Asemi c d) Q = awp c (awp d Q)"
nipkow@2810
    28
  "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
nipkow@2810
    29
  "awp (Awhile b I c) Q = I"
nipkow@1447
    30
berghofe@5183
    31
primrec
wenzelm@3842
    32
  "vc Askip Q = (%s. True)"
wenzelm@3842
    33
  "vc (Aass x a) Q = (%s. True)"
nipkow@2810
    34
  "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
berghofe@1900
    35
  "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
berghofe@1900
    36
  "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
nipkow@2810
    37
                              (I s & b s --> awp c I s) & vc c I s)"
nipkow@1447
    38
berghofe@5183
    39
primrec
berghofe@1900
    40
  "astrip Askip = SKIP"
oheimb@9241
    41
  "astrip (Aass x a) = (x:==a)"
berghofe@1900
    42
  "astrip (Asemi c d) = (astrip c;astrip d)"
berghofe@1900
    43
  "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
berghofe@1900
    44
  "astrip (Awhile b I c) = (WHILE b DO astrip c)"
nipkow@1451
    45
nipkow@2810
    46
(* simultaneous computation of vc and awp: *)
berghofe@5183
    47
primrec
wenzelm@3842
    48
  "vcawp Askip Q = (%s. True, Q)"
oheimb@9241
    49
  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x::=a s]))"
nipkow@2810
    50
  "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
nipkow@2810
    51
                              (vcc,wpc) = vcawp c wpd
nipkow@2810
    52
                          in (%s. vcc s & vcd s, wpc))"
nipkow@2810
    53
  "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
nipkow@2810
    54
                              (vcc,wpc) = vcawp c Q
nipkow@2810
    55
                          in (%s. vcc s & vcd s,
nipkow@2810
    56
                              %s.(b s --> wpc s) & (~b s --> wpd s)))"
nipkow@2810
    57
  "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
nipkow@2810
    58
                             in (%s. (I s & ~b s --> Q s) &
nipkow@2810
    59
                                     (I s & b s --> wpc s) & vcc s, I))"
nipkow@1451
    60
nipkow@1447
    61
end