author | obua |
Thu, 07 Jun 2007 17:21:43 +0200 | |
changeset 23293 | 77577fc2f141 |
parent 19803 | aa2581752afb |
child 27362 | a6dc1769fdda |
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 |
||
17477 | 7 |
header {* Example of mutually recursive procedures verified with Hoare logic *} |
8177 | 8 |
|
17477 | 9 |
theory EvenOdd |
10 |
imports Misc |
|
11 |
begin |
|
12 |
||
13 |
constdefs |
|
14 |
even :: "nat => bool" |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
15 |
"even n == 2 dvd n" |
8177 | 16 |
|
17 |
consts |
|
17477 | 18 |
Even :: pname |
19 |
Odd :: pname |
|
20 |
axioms |
|
21 |
Even_neq_Odd: "Even ~= Odd" |
|
22 |
Arg_neq_Res: "Arg ~= Res" |
|
8177 | 23 |
|
24 |
constdefs |
|
25 |
evn :: com |
|
15354 | 26 |
"evn == IF (%s. s<Arg> = 0) |
8177 | 27 |
THEN Loc Res:==(%s. 0) |
28 |
ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);; |
|
29 |
Loc Arg:=CALL Odd(%s. s<Arg> - 1);; |
|
30 |
Loc Res:==(%s. s<Res> * s<Arg>))" |
|
31 |
odd :: com |
|
15354 | 32 |
"odd == IF (%s. s<Arg> = 0) |
8177 | 33 |
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
|
34 |
ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))" |
8177 | 35 |
|
36 |
defs |
|
17477 | 37 |
bodies_def: "bodies == [(Even,evn),(Odd,odd)]" |
38 |
||
8177 | 39 |
consts |
17477 | 40 |
Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) |
41 |
"even_Z=(Res=0)" :: "nat assn" ("Res'_ok") |
|
8177 | 42 |
defs |
17477 | 43 |
Z_eq_Arg_plus_def: "Z=Arg+n == %Z s. Z = s<Arg>+n" |
44 |
Res_ok_def: "Res_ok == %Z s. even Z = (s<Res> = 0)" |
|
45 |
||
19803 | 46 |
|
47 |
subsection "even" |
|
48 |
||
49 |
lemma even_0 [simp]: "even 0" |
|
50 |
apply (unfold even_def) |
|
51 |
apply simp |
|
52 |
done |
|
53 |
||
54 |
lemma not_even_1 [simp]: "even (Suc 0) = False" |
|
55 |
apply (unfold even_def) |
|
56 |
apply simp |
|
57 |
done |
|
58 |
||
59 |
lemma even_step [simp]: "even (Suc (Suc n)) = even n" |
|
60 |
apply (unfold even_def) |
|
61 |
apply (subgoal_tac "Suc (Suc n) = n+2") |
|
62 |
prefer 2 |
|
63 |
apply simp |
|
64 |
apply (erule ssubst) |
|
65 |
apply (rule dvd_reduce) |
|
66 |
done |
|
67 |
||
68 |
||
69 |
subsection "Arg, Res" |
|
70 |
||
71 |
declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp] |
|
72 |
declare Even_neq_Odd [simp] Even_neq_Odd [THEN not_sym, simp] |
|
73 |
||
74 |
lemma Z_eq_Arg_plus_def2: "(Z=Arg+n) Z s = (Z = s<Arg>+n)" |
|
75 |
apply (unfold Z_eq_Arg_plus_def) |
|
76 |
apply (rule refl) |
|
77 |
done |
|
78 |
||
79 |
lemma Res_ok_def2: "Res_ok Z s = (even Z = (s<Res> = 0))" |
|
80 |
apply (unfold Res_ok_def) |
|
81 |
apply (rule refl) |
|
82 |
done |
|
83 |
||
84 |
lemmas Arg_Res_simps = Z_eq_Arg_plus_def2 Res_ok_def2 |
|
85 |
||
86 |
lemma body_Odd [simp]: "body Odd = Some odd" |
|
87 |
apply (unfold body_def bodies_def) |
|
88 |
apply auto |
|
89 |
done |
|
90 |
||
91 |
lemma body_Even [simp]: "body Even = Some evn" |
|
92 |
apply (unfold body_def bodies_def) |
|
93 |
apply auto |
|
94 |
done |
|
95 |
||
96 |
||
97 |
subsection "verification" |
|
98 |
||
99 |
lemma Odd_lemma: "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}" |
|
100 |
apply (unfold odd_def) |
|
101 |
apply (rule hoare_derivs.If) |
|
102 |
apply (rule hoare_derivs.Ass [THEN conseq1]) |
|
103 |
apply (clarsimp simp: Arg_Res_simps) |
|
104 |
apply (rule export_s) |
|
105 |
apply (rule hoare_derivs.Call [THEN conseq1]) |
|
106 |
apply (rule_tac P = "Z=Arg+Suc (Suc 0) " in conseq12) |
|
107 |
apply (rule single_asm) |
|
108 |
apply (auto simp: Arg_Res_simps) |
|
109 |
done |
|
110 |
||
111 |
lemma Even_lemma: "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}" |
|
112 |
apply (unfold evn_def) |
|
113 |
apply (rule hoare_derivs.If) |
|
114 |
apply (rule hoare_derivs.Ass [THEN conseq1]) |
|
115 |
apply (clarsimp simp: Arg_Res_simps) |
|
116 |
apply (rule hoare_derivs.Comp) |
|
117 |
apply (rule_tac [2] hoare_derivs.Ass) |
|
118 |
apply clarsimp |
|
119 |
apply (rule_tac Q = "%Z s. ?P Z s & Res_ok Z s" in hoare_derivs.Comp) |
|
120 |
apply (rule export_s) |
|
121 |
apply (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12]) |
|
122 |
apply (rule single_asm [THEN conseq2]) |
|
123 |
apply (clarsimp simp: Arg_Res_simps) |
|
124 |
apply (force simp: Arg_Res_simps) |
|
125 |
apply (rule export_s) |
|
126 |
apply (rule_tac I1 = "%Z l. even Z = (l Res = 0) " and Q1 = "%Z s. even Z = (s<Arg> = 0) " in Call_invariant [THEN conseq12]) |
|
127 |
apply (rule single_asm [THEN conseq2]) |
|
128 |
apply (clarsimp simp: Arg_Res_simps) |
|
129 |
apply (force simp: Arg_Res_simps) |
|
130 |
done |
|
131 |
||
132 |
||
133 |
lemma Even_ok_N: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}" |
|
134 |
apply (rule BodyN) |
|
135 |
apply (simp (no_asm)) |
|
136 |
apply (rule Even_lemma [THEN hoare_derivs.cut]) |
|
137 |
apply (rule BodyN) |
|
138 |
apply (simp (no_asm)) |
|
139 |
apply (rule Odd_lemma [THEN thin]) |
|
140 |
apply (simp (no_asm)) |
|
141 |
done |
|
142 |
||
143 |
lemma Even_ok_S: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}" |
|
144 |
apply (rule conseq1) |
|
145 |
apply (rule_tac Procs = "{Odd, Even}" and pn = "Even" and P = "%pn. Z=Arg+ (if pn = Odd then 1 else 0) " and Q = "%pn. Res_ok" in Body1) |
|
146 |
apply auto |
|
147 |
apply (rule hoare_derivs.insert) |
|
148 |
apply (rule Odd_lemma [THEN thin]) |
|
149 |
apply (simp (no_asm)) |
|
150 |
apply (rule Even_lemma [THEN thin]) |
|
151 |
apply (simp (no_asm)) |
|
152 |
done |
|
8177 | 153 |
|
154 |
end |