equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Example of mutually recursive procedures verified with Hoare logic *} |
5 header {* Example of mutually recursive procedures verified with Hoare logic *} |
6 |
6 |
7 theory EvenOdd |
7 theory EvenOdd |
8 imports Misc |
8 imports Misc "~~/src/HOL/Parity" |
9 begin |
9 begin |
10 |
|
11 definition |
|
12 even :: "nat => bool" where |
|
13 "even n = (2 dvd n)" |
|
14 |
10 |
15 axiomatization |
11 axiomatization |
16 Even :: pname and |
12 Even :: pname and |
17 Odd :: pname |
13 Odd :: pname |
18 where |
14 where |
44 Res_ok :: "nat assn" where |
40 Res_ok :: "nat assn" where |
45 "Res_ok = (%Z s. even Z = (s<Res> = 0))" |
41 "Res_ok = (%Z s. even Z = (s<Res> = 0))" |
46 |
42 |
47 |
43 |
48 subsection "even" |
44 subsection "even" |
49 |
|
50 lemma even_0 [simp]: "even 0" |
|
51 apply (unfold even_def) |
|
52 apply simp |
|
53 done |
|
54 |
45 |
55 lemma not_even_1 [simp]: "even (Suc 0) = False" |
46 lemma not_even_1 [simp]: "even (Suc 0) = False" |
56 apply (unfold even_def) |
47 apply (unfold even_def) |
57 apply simp |
48 apply simp |
58 done |
49 done |