src/HOL/IMP/VC.thy
author clasohm
Mon, 05 Feb 1996 21:29:06 +0100
changeset 1476 608483c2122a
parent 1451 6803ecb9b198
child 1481 03f096efa26d
permissions -rw-r--r--
expanded tabs; incorporated Konrad's changes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1451
diff changeset
     1
(*  Title:      HOL/IMP/VC.thy
1447
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1451
diff changeset
     3
    Author:     Tobias Nipkow
1447
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
     4
    Copyright   1996 TUM
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
     5
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
     6
acom: annotated commands
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
     7
vc:   verification-conditions
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
     8
wp:   weakest (liberal) precondition
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
     9
*)
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    10
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    11
VC  =  Hoare +
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    12
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    13
datatype  acom = Askip
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    14
               | Aass   loc aexp
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    15
               | Asemi  acom acom
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    16
               | Aif    bexp acom acom
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    17
               | Awhile bexp assn acom
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    18
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    19
consts
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    20
  vc,wp :: acom => assn => assn
1451
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    21
  vcwp :: "acom => assn => assn * assn"
1447
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    22
  astrip :: acom => com
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    23
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    24
primrec wp acom
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    25
  wp_Askip  "wp Askip Q = Q"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    26
  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[A a s/x]))"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    27
  wp_Asemi  "wp (Asemi c d) Q = wp c (wp d Q)"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    28
  wp_Aif    "wp (Aif b c d) Q = (%s. (B b s-->wp c Q s)&(~B b s-->wp d Q s))" 
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    29
  wp_Awhile "wp (Awhile b I c) Q = I"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    30
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    31
primrec vc acom
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    32
  vc_Askip  "vc Askip Q = (%s.True)"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    33
  vc_Aass   "vc (Aass x a) Q = (%s.True)"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    34
  vc_Asemi  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    35
  vc_Aif    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    36
  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~B b s --> Q s) &
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    37
                              (I s & B b s --> wp c I s) & vc c I s)"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    38
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    39
primrec astrip acom
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    40
  astrip_Askip  "astrip Askip = skip"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    41
  astrip_Aass   "astrip (Aass x a) = (x:=a)"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    42
  astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    43
  astrip_Aif    "astrip (Aif b c d) = ifC b (astrip c) (astrip d)"
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    44
  astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"
1451
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    45
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    46
(* simultaneous computation of vc and wp: *)
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    47
primrec vcwp acom
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    48
  vcwp_Askip
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    49
  "vcwp Askip Q = (%s.True, Q)"
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    50
  vcwp_Aass
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    51
  "vcwp (Aass x a) Q = (%s.True, %s.Q(s[A a s/x]))"
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    52
  vcwp_Asemi
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    53
  "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    54
                            (vcc,wpc) = vcwp c wpd
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    55
                         in (%s. vcc s & vcd s, wpc))"
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    56
  vcwp_Aif
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    57
  "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    58
                            (vcc,wpc) = vcwp c Q
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    59
                         in (%s. vcc s & vcd s,
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    60
                             %s.(B b s-->wpc s) & (~B b s-->wpd s)))"
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    61
  vcwp_Awhile
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    62
  "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    63
                            in (%s. (I s & ~B b s --> Q s) &
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    64
                                    (I s & B b s --> wpc s) & vcc s, I))"
6803ecb9b198 Added vcwp
nipkow
parents: 1447
diff changeset
    65
1447
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents:
diff changeset
    66
end