src/HOL/IMP/Hoare.thy
author nipkow
Wed Feb 07 12:22:32 1996 +0100 (1996-02-07)
changeset 1481 03f096efa26d
parent 1476 608483c2122a
child 1486 7b95d7b49f7a
permissions -rw-r--r--
Modified datatype com.
Added (part of) relative completeness proof for Hoare logic.
clasohm@1476
     1
(*  Title:      HOL/IMP/Hoare.thy
nipkow@938
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
nipkow@936
     4
    Copyright   1995 TUM
nipkow@936
     5
nipkow@1447
     6
Inductive definition of Hoare logic
nipkow@936
     7
*)
nipkow@936
     8
nipkow@936
     9
Hoare = Denotation +
nipkow@1447
    10
nipkow@1447
    11
types assn = state => bool
nipkow@1447
    12
nipkow@936
    13
consts
nipkow@1447
    14
  hoare :: "(assn * com * assn) set"
nipkow@1481
    15
  hoare_valid :: [assn,com,assn] => bool ("|= {{_}}_{{_}}")
nipkow@936
    16
defs
nipkow@1481
    17
  hoare_valid_def "|= {{P}}c{{Q}} == !s t. (s,t) : C(c) --> P s --> Q t"
nipkow@939
    18
nipkow@1447
    19
syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
nipkow@1447
    20
translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare"
nipkow@939
    21
nipkow@1447
    22
inductive "hoare"
nipkow@1447
    23
intrs
nipkow@1481
    24
  skip "{{P}}Skip{{P}}"
nipkow@1481
    25
  ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
nipkow@1481
    26
  semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
nipkow@1481
    27
  If "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
nipkow@1481
    28
        {{P}} IF b THEN c ELSE d {{Q}}"
nipkow@1481
    29
  While "[| {{%s. P s & B b s}} c {{P}} |] ==>
nipkow@1481
    30
         {{P}} WHILE b DO c {{%s. P s & ~B b s}}"
nipkow@1481
    31
  conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
nipkow@1481
    32
          {{P'}}c{{Q'}}"
nipkow@1481
    33
nipkow@1481
    34
consts swp :: com => assn => assn
nipkow@1481
    35
defs swp_def "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
nipkow@939
    36
nipkow@939
    37
end