1 (* Title: HOL/IMPP/EvenOdd.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1999 TUM |
|
5 *) |
|
6 |
|
7 section "even"; |
|
8 |
|
9 Goalw [even_def] "even 0"; |
|
10 by (Simp_tac 1); |
|
11 qed "even_0"; |
|
12 Addsimps [even_0]; |
|
13 |
|
14 Goalw [even_def] "even (Suc 0) = False"; |
|
15 by (Simp_tac 1); |
|
16 qed "not_even_1"; |
|
17 Addsimps [not_even_1]; |
|
18 |
|
19 Goalw [even_def] "even (Suc (Suc n)) = even n"; |
|
20 by (subgoal_tac "Suc (Suc n) = n+2" 1); |
|
21 by (Simp_tac 2); |
|
22 by (etac ssubst 1); |
|
23 by (rtac dvd_reduce 1); |
|
24 qed "even_step"; |
|
25 Addsimps[even_step]; |
|
26 |
|
27 |
|
28 section "Arg, Res"; |
|
29 |
|
30 Addsimps[Arg_neq_Res,Arg_neq_Res RS not_sym]; |
|
31 Addsimps[Even_neq_Odd, Even_neq_Odd RS not_sym]; |
|
32 |
|
33 Goalw [Z_eq_Arg_plus_def] "(Z=Arg+n) Z s = (Z = s<Arg>+n)"; |
|
34 by (rtac refl 1); |
|
35 qed "Z_eq_Arg_plus_def2"; |
|
36 |
|
37 Goalw [Res_ok_def] "Res_ok Z s = (even Z = (s<Res> = 0))"; |
|
38 by (rtac refl 1); |
|
39 qed "Res_ok_def2"; |
|
40 |
|
41 val Arg_Res_css = (claset(),simpset()addsimps[Z_eq_Arg_plus_def2,Res_ok_def2]); |
|
42 |
|
43 Goalw [body_def, bodies_def] "body Odd = Some odd"; |
|
44 by Auto_tac; |
|
45 qed "body_Odd"; |
|
46 Goalw [body_def, bodies_def] "body Even = Some evn"; |
|
47 by Auto_tac; |
|
48 qed "body_Even"; |
|
49 Addsimps[body_Odd, body_Even]; |
|
50 |
|
51 section "verification"; |
|
52 |
|
53 Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}"; |
|
54 by (rtac hoare_derivs.If 1); |
|
55 by (rtac (hoare_derivs.Ass RS conseq1) 1); |
|
56 by (clarsimp_tac Arg_Res_css 1); |
|
57 by (rtac export_s 1); |
|
58 by (rtac (hoare_derivs.Call RS conseq1) 1); |
|
59 by (res_inst_tac [("P","Z=Arg+Suc (Suc 0)")] conseq12 1); |
|
60 by (rtac single_asm 1); |
|
61 by (auto_tac Arg_Res_css); |
|
62 qed "Odd_lemma"; |
|
63 |
|
64 Goalw [evn_def] "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}"; |
|
65 by (rtac hoare_derivs.If 1); |
|
66 by (rtac (hoare_derivs.Ass RS conseq1) 1); |
|
67 by (clarsimp_tac Arg_Res_css 1); |
|
68 by (rtac hoare_derivs.Comp 1); |
|
69 by (rtac hoare_derivs.Ass 2); |
|
70 by (Clarsimp_tac 1); |
|
71 by (res_inst_tac [("Q","%Z s. ?P Z s & Res_ok Z s")] hoare_derivs.Comp 1); |
|
72 by (rtac export_s 1); |
|
73 by (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"), |
|
74 ("Q1","Res_ok")] (Call_invariant RS conseq12) 1); |
|
75 by (rtac (single_asm RS conseq2) 1); |
|
76 by (clarsimp_tac Arg_Res_css 1); |
|
77 by (force_tac Arg_Res_css 1); |
|
78 by (rtac export_s 1); |
|
79 by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"), |
|
80 ("Q1","%Z s. even Z = (s<Arg> = 0)")] |
|
81 (Call_invariant RS conseq12) 1); |
|
82 by (rtac (single_asm RS conseq2) 1); |
|
83 by (clarsimp_tac Arg_Res_css 1); |
|
84 by (force_tac Arg_Res_css 1); |
|
85 qed "Even_lemma"; |
|
86 |
|
87 |
|
88 Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"; |
|
89 by (rtac BodyN 1); |
|
90 by (Simp_tac 1); |
|
91 by (rtac (Even_lemma RS hoare_derivs.cut) 1); |
|
92 by (rtac BodyN 1); |
|
93 by (Simp_tac 1); |
|
94 by (rtac (Odd_lemma RS thin) 1); |
|
95 by (Simp_tac 1); |
|
96 qed "Even_ok_N"; |
|
97 |
|
98 Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"; |
|
99 by (rtac conseq1 1); |
|
100 by (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"), |
|
101 ("P","%pn. Z=Arg+(if pn = Odd then 1 else 0)"), |
|
102 ("Q","%pn. Res_ok")] Body1 1); |
|
103 by Auto_tac; |
|
104 by (rtac hoare_derivs.insert 1); |
|
105 by (rtac (Odd_lemma RS thin) 1); |
|
106 by (Simp_tac 1); |
|
107 by (rtac (Even_lemma RS thin) 1); |
|
108 by (Simp_tac 1); |
|
109 qed "Even_ok_S"; |
|