8 |
8 |
9 theory EvenOdd |
9 theory EvenOdd |
10 imports Misc |
10 imports Misc |
11 begin |
11 begin |
12 |
12 |
13 constdefs |
13 definition |
14 even :: "nat => bool" |
14 even :: "nat => bool" where |
15 "even n == 2 dvd n" |
15 "even n = (2 dvd n)" |
16 |
16 |
17 consts |
17 axiomatization |
18 Even :: pname |
18 Even :: pname and |
19 Odd :: pname |
19 Odd :: pname |
20 axioms |
20 where |
21 Even_neq_Odd: "Even ~= Odd" |
21 Even_neq_Odd: "Even ~= Odd" and |
22 Arg_neq_Res: "Arg ~= Res" |
22 Arg_neq_Res: "Arg ~= Res" |
23 |
23 |
24 constdefs |
24 definition |
25 evn :: com |
25 evn :: com where |
26 "evn == IF (%s. s<Arg> = 0) |
26 "evn = (IF (%s. s<Arg> = 0) |
27 THEN Loc Res:==(%s. 0) |
27 THEN Loc Res:==(%s. 0) |
28 ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);; |
28 ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);; |
29 Loc Arg:=CALL Odd(%s. s<Arg> - 1);; |
29 Loc Arg:=CALL Odd(%s. s<Arg> - 1);; |
30 Loc Res:==(%s. s<Res> * s<Arg>))" |
30 Loc Res:==(%s. s<Res> * s<Arg>)))" |
31 odd :: com |
31 |
32 "odd == IF (%s. s<Arg> = 0) |
32 definition |
|
33 odd :: com where |
|
34 "odd = (IF (%s. s<Arg> = 0) |
33 THEN Loc Res:==(%s. 1) |
35 THEN Loc Res:==(%s. 1) |
34 ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))" |
36 ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))" |
35 |
37 |
36 defs |
38 defs |
37 bodies_def: "bodies == [(Even,evn),(Odd,odd)]" |
39 bodies_def: "bodies == [(Even,evn),(Odd,odd)]" |
38 |
40 |
39 consts |
41 definition |
40 Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) |
42 Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where |
41 "even_Z=(Res=0)" :: "nat assn" ("Res'_ok") |
43 "Z=Arg+n = (%Z s. Z = s<Arg>+n)" |
42 defs |
44 |
43 Z_eq_Arg_plus_def: "Z=Arg+n == %Z s. Z = s<Arg>+n" |
45 definition |
44 Res_ok_def: "Res_ok == %Z s. even Z = (s<Res> = 0)" |
46 Res_ok :: "nat assn" where |
|
47 "Res_ok = (%Z s. even Z = (s<Res> = 0))" |
45 |
48 |
46 |
49 |
47 subsection "even" |
50 subsection "even" |
48 |
51 |
49 lemma even_0 [simp]: "even 0" |
52 lemma even_0 [simp]: "even 0" |