src/HOL/IMP/Hoare.thy
 author clasohm Fri Mar 24 12:30:35 1995 +0100 (1995-03-24) changeset 972 e61b058d58d2 parent 939 534955033ed2 child 1374 5e407f2a3323 permissions -rw-r--r--
changed syntax of tuples from <..., ...> to (..., ...)
1 (*  Title: 	HOL/IMP/Hoare.thy
2     ID:         \$Id\$
3     Author: 	Tobias Nipkow
6 Semantic embedding of Hoare logic
7 *)
9 Hoare = Denotation +
10 consts
11   spec :: "[state=>bool,com,state=>bool] => bool"
12 (* syntax "@spec" :: "[bool,com,bool] => bool" *)
13           ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
14 defs
15   spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
16 end
17 (* Pretty-printing of assertions.
18    Not very helpful as long as programs are not pretty-printed.
19 ML
21 local open Syntax
23 fun is_loc a = let val ch = hd(explode a)
24                in ord "A" <= ord ch andalso ord ch <= ord "Z" end;
26 fun tr(s\$t,i) = tr(s,i)\$tr(t,i)
27   | tr(Abs(x,T,u),i) = Abs(x,T,tr(u,i+1))
28   | tr(t as Free(a,T),i) = if is_loc a then Bound(i) \$ free(a) else t
29   | tr(t,_) = t;
31 fun cond_tr(p) = Abs("",dummyT,tr(p,0))
33 fun spec_tr[p,c,q] = const"spec" \$ cond_tr p \$ c \$ cond_tr q;
35 fun tr'(t as (Bound j \$ (u as Free(a,_))),i) = if i=j then u else t
36   | tr'(s\$t,i) = tr'(s,i)\$tr'(t,i)
37   | tr'(Abs(x,T,u),i) = Abs(x,T,tr'(u,i+1))
38   | tr'(t,_) = t;
40 fun spec_tr'[Abs(_,_,p),c,Abs(_,_,q)] =
41   const"@spec" \$ tr'(p,0) \$ c \$ tr'(q,0);
43 in
45 val parse_translation = [("@spec", spec_tr)];
46 val print_translation = [("spec", spec_tr')];
48 end
49 *)