src/HOL/IMP/Hoare.thy
changeset 1447 bc2c0acbbf29
parent 1374 5e407f2a3323
child 1476 608483c2122a
     1.1 --- a/src/HOL/IMP/Hoare.thy	Sat Jan 20 02:00:11 1996 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Tue Jan 23 10:59:35 1996 +0100
     1.3 @@ -3,47 +3,32 @@
     1.4      Author: 	Tobias Nipkow
     1.5      Copyright   1995 TUM
     1.6  
     1.7 -Semantic embedding of Hoare logic
     1.8 +Inductive definition of Hoare logic
     1.9  *)
    1.10  
    1.11  Hoare = Denotation +
    1.12 +
    1.13 +types assn = state => bool
    1.14 +
    1.15  consts
    1.16 +  hoare :: "(assn * com * assn) set"
    1.17    spec :: [state=>bool,com,state=>bool] => bool
    1.18 -(* syntax "@spec" :: [bool,com,bool] => bool *)
    1.19 -          ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
    1.20  defs
    1.21    spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
    1.22 -end
    1.23 -(* Pretty-printing of assertions.
    1.24 -   Not very helpful as long as programs are not pretty-printed.
    1.25 -ML
    1.26  
    1.27 -local open Syntax
    1.28 -
    1.29 -fun is_loc a = let val ch = hd(explode a)
    1.30 -               in ord "A" <= ord ch andalso ord ch <= ord "Z" end;
    1.31 -
    1.32 -fun tr(s$t,i) = tr(s,i)$tr(t,i)
    1.33 -  | tr(Abs(x,T,u),i) = Abs(x,T,tr(u,i+1))
    1.34 -  | tr(t as Free(a,T),i) = if is_loc a then Bound(i) $ free(a) else t
    1.35 -  | tr(t,_) = t;
    1.36 +syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
    1.37 +translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare"
    1.38  
    1.39 -fun cond_tr(p) = Abs("",dummyT,tr(p,0))
    1.40 -
    1.41 -fun spec_tr[p,c,q] = const"spec" $ cond_tr p $ c $ cond_tr q;
    1.42 -
    1.43 -fun tr'(t as (Bound j $ (u as Free(a,_))),i) = if i=j then u else t
    1.44 -  | tr'(s$t,i) = tr'(s,i)$tr'(t,i)
    1.45 -  | tr'(Abs(x,T,u),i) = Abs(x,T,tr'(u,i+1))
    1.46 -  | tr'(t,_) = t;
    1.47 -
    1.48 -fun spec_tr'[Abs(_,_,p),c,Abs(_,_,q)] =
    1.49 -  const"@spec" $ tr'(p,0) $ c $ tr'(q,0);
    1.50 -
    1.51 -in
    1.52 -
    1.53 -val parse_translation = [("@spec", spec_tr)];
    1.54 -val print_translation = [("spec", spec_tr')];
    1.55 +inductive "hoare"
    1.56 +intrs
    1.57 +  hoare_skip "{{P}}skip{{P}}"
    1.58 +  hoare_ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
    1.59 +  hoare_semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
    1.60 +  hoare_if   "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
    1.61 +              {{P}} ifc b then c else d {{Q}}"
    1.62 +  hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
    1.63 +	       {{P}} while b do c {{%s. P s & ~B b s}}"
    1.64 +  hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
    1.65 +		{{P'}}c{{Q'}}"
    1.66  
    1.67  end
    1.68 -*)