| author | wenzelm |
| Mon, 04 Mar 2002 19:06:52 +0100 | |
| changeset 13012 | f8bfc61ee1b5 |
| parent 11704 | 3c50a2cd6f00 |
| child 15354 | 9234f5765d9c |
| permissions | -rw-r--r-- |
| 8177 | 1 |
(* Title: HOL/IMPP/EvenOdd.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 TUM |
|
5 |
||
6 |
Example of mutually recursive procedures verified with Hoare logic |
|
7 |
*) |
|
8 |
||
9 |
EvenOdd = Misc + |
|
10 |
||
11 |
constdefs even :: nat => bool |
|
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
12 |
"even n == 2 dvd n" |
| 8177 | 13 |
|
14 |
consts |
|
15 |
Even, Odd :: pname |
|
16 |
rules |
|
17 |
Even_neq_Odd "Even ~= Odd" |
|
18 |
Arg_neq_Res "Arg ~= Res" |
|
19 |
||
20 |
constdefs |
|
21 |
evn :: com |
|
22 |
"evn == IF (%s. s<Arg>=0) |
|
23 |
THEN Loc Res:==(%s. 0) |
|
24 |
ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);; |
|
25 |
Loc Arg:=CALL Odd(%s. s<Arg> - 1);; |
|
26 |
Loc Res:==(%s. s<Res> * s<Arg>))" |
|
27 |
odd :: com |
|
28 |
"odd == IF (%s. s<Arg>=0) |
|
29 |
THEN Loc Res:==(%s. 1) |
|
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
8791
diff
changeset
|
30 |
ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))" |
| 8177 | 31 |
|
32 |
defs |
|
33 |
bodies_def "bodies == [(Even,evn),(Odd,odd)]" |
|
34 |
||
35 |
consts |
|
36 |
Z_eq_Arg_plus :: nat => nat assn ("Z=Arg+_" [50]50)
|
|
37 |
"even_Z=(Res=0)" :: nat assn ("Res'_ok")
|
|
38 |
defs |
|
39 |
Z_eq_Arg_plus_def "Z=Arg+n == %Z s. Z = s<Arg>+n" |
|
40 |
Res_ok_def "Res_ok == %Z s. even Z = (s<Res>=0)" |
|
41 |
||
42 |
end |