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