src/HOL/IMP/Hoare.thy
author wenzelm
Mon, 01 Dec 1997 18:27:43 +0100
changeset 4336 7fb8a0c4578a
parent 3842 b55686a7b22c
child 4897 be11be0b6ea1
permissions -rw-r--r--
open;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1447
diff changeset
     1
(*  Title:      HOL/IMP/Hoare.thy
938
621be7ec81d7 *** empty log message ***
nipkow
parents: 937
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1447
diff changeset
     3
    Author:     Tobias Nipkow
936
a6d7b4084761 Hoare logic
nipkow
parents:
diff changeset
     4
    Copyright   1995 TUM
a6d7b4084761 Hoare logic
nipkow
parents:
diff changeset
     5
1447
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents: 1374
diff changeset
     6
Inductive definition of Hoare logic
936
a6d7b4084761 Hoare logic
nipkow
parents:
diff changeset
     7
*)
a6d7b4084761 Hoare logic
nipkow
parents:
diff changeset
     8
2810
c4e16b36bc57 Added wp_while.
nipkow
parents: 1789
diff changeset
     9
Hoare = Denotation + Gfp +
1447
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents: 1374
diff changeset
    10
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents: 1374
diff changeset
    11
types assn = state => bool
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents: 1374
diff changeset
    12
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1486
diff changeset
    13
constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1486
diff changeset
    14
          "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
939
534955033ed2 Added pretty-printing coments
nipkow
parents: 938
diff changeset
    15
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1486
diff changeset
    16
consts hoare :: "(assn * com * assn) set"
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1486
diff changeset
    17
syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1481
diff changeset
    18
translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
939
534955033ed2 Added pretty-printing coments
nipkow
parents: 938
diff changeset
    19
1789
aade046ec6d5 Quotes now optional around inductive set
paulson
parents: 1696
diff changeset
    20
inductive hoare
1447
bc2c0acbbf29 Added a verified verification-condition generator.
nipkow
parents: 1374
diff changeset
    21
intrs
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1486
diff changeset
    22
  skip "|- {P}SKIP{P}"
3842
b55686a7b22c fixed dots;
wenzelm
parents: 2810
diff changeset
    23
  ass  "|- {%s. P(s[a s/x])} x:=a {P}"
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1481
diff changeset
    24
  semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1486
diff changeset
    25
  If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1481
diff changeset
    26
      |- {P} IF b THEN c ELSE d {Q}"
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1486
diff changeset
    27
  While "|- {%s. P s & b s} c {P} ==>
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1486
diff changeset
    28
         |- {P} WHILE b DO c {%s. P s & ~b s}"
1486
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1481
diff changeset
    29
  conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
7b95d7b49f7a Introduced qed_spec_mp.
nipkow
parents: 1481
diff changeset
    30
          |- {P'}c{Q'}"
1481
03f096efa26d Modified datatype com.
nipkow
parents: 1476
diff changeset
    31
2810
c4e16b36bc57 Added wp_while.
nipkow
parents: 1789
diff changeset
    32
constdefs wp :: com => assn => assn
c4e16b36bc57 Added wp_while.
nipkow
parents: 1789
diff changeset
    33
          "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
939
534955033ed2 Added pretty-printing coments
nipkow
parents: 938
diff changeset
    34
534955033ed2 Added pretty-printing coments
nipkow
parents: 938
diff changeset
    35
end