src/HOL/IMP/Hoare.thy
author nipkow
Tue Jan 23 10:59:35 1996 +0100 (1996-01-23)
changeset 1447 bc2c0acbbf29
parent 1374 5e407f2a3323
child 1476 608483c2122a
permissions -rw-r--r--
Added a verified verification-condition generator.
nipkow@936
     1
(*  Title: 	HOL/IMP/Hoare.thy
nipkow@938
     2
    ID:         $Id$
nipkow@936
     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"
clasohm@1374
    15
  spec :: [state=>bool,com,state=>bool] => bool
nipkow@936
    16
defs
clasohm@972
    17
  spec_def "spec 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@1447
    24
  hoare_skip "{{P}}skip{{P}}"
nipkow@1447
    25
  hoare_ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
nipkow@1447
    26
  hoare_semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
nipkow@1447
    27
  hoare_if   "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
nipkow@1447
    28
              {{P}} ifc b then c else d {{Q}}"
nipkow@1447
    29
  hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
nipkow@1447
    30
	       {{P}} while b do c {{%s. P s & ~B b s}}"
nipkow@1447
    31
  hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
nipkow@1447
    32
		{{P'}}c{{Q'}}"
nipkow@939
    33
nipkow@939
    34
end