equal
deleted
inserted
replaced
|
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 |
|
12 "even n == 2 dvd n" |
|
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) |
|
30 ELSE(Loc Res:=CALL Even (%s. s<Arg> -1))" |
|
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 |