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.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 -*)
```