|
1 (* Title: HOLCF/ex/loop.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for theory loop.thy |
|
7 *) |
|
8 |
|
9 open Loop; |
|
10 |
|
11 (* --------------------------------------------------------------------------- *) |
|
12 (* access to definitions *) |
|
13 (* --------------------------------------------------------------------------- *) |
|
14 |
|
15 val step_def2 = prove_goalw Loop.thy [step_def] |
|
16 "step[b][g][x] = If b[x] then g[x] else x fi" |
|
17 (fn prems => |
|
18 [ |
|
19 (simp_tac Cfun_ss 1) |
|
20 ]); |
|
21 |
|
22 val while_def2 = prove_goalw Loop.thy [while_def] |
|
23 "while[b][g] = fix[LAM f x. If b[x] then f[g[x]] else x fi]" |
|
24 (fn prems => |
|
25 [ |
|
26 (simp_tac Cfun_ss 1) |
|
27 ]); |
|
28 |
|
29 |
|
30 (* ------------------------------------------------------------------------- *) |
|
31 (* rekursive properties of while *) |
|
32 (* ------------------------------------------------------------------------- *) |
|
33 |
|
34 val while_unfold = prove_goal Loop.thy |
|
35 "while[b][g][x] = If b[x] then while[b][g][g[x]] else x fi" |
|
36 (fn prems => |
|
37 [ |
|
38 (fix_tac5 while_def2 1), |
|
39 (simp_tac Cfun_ss 1) |
|
40 ]); |
|
41 |
|
42 val while_unfold2 = prove_goal Loop.thy |
|
43 "!x.while[b][g][x] = while[b][g][iterate(k,step[b][g],x)]" |
|
44 (fn prems => |
|
45 [ |
|
46 (nat_ind_tac "k" 1), |
|
47 (simp_tac (HOLCF_ss addsimps [iterate_0,iterate_Suc]) 1), |
|
48 (rtac allI 1), |
|
49 (rtac trans 1), |
|
50 (rtac (while_unfold RS ssubst) 1), |
|
51 (rtac refl 2), |
|
52 (rtac (iterate_Suc2 RS ssubst) 1), |
|
53 (rtac trans 1), |
|
54 (etac spec 2), |
|
55 (rtac (step_def2 RS ssubst) 1), |
|
56 (res_inst_tac [("p","b[x]")] trE 1), |
|
57 (asm_simp_tac HOLCF_ss 1), |
|
58 (rtac (while_unfold RS ssubst) 1), |
|
59 (res_inst_tac [("s","UU"),("t","b[UU]")] ssubst 1), |
|
60 (etac (flat_tr RS flat_codom RS disjE) 1), |
|
61 (atac 1), |
|
62 (etac spec 1), |
|
63 (simp_tac HOLCF_ss 1), |
|
64 (asm_simp_tac HOLCF_ss 1), |
|
65 (asm_simp_tac HOLCF_ss 1), |
|
66 (rtac (while_unfold RS ssubst) 1), |
|
67 (asm_simp_tac HOLCF_ss 1) |
|
68 ]); |
|
69 |
|
70 val while_unfold3 = prove_goal Loop.thy |
|
71 "while[b][g][x] = while[b][g][step[b][g][x]]" |
|
72 (fn prems => |
|
73 [ |
|
74 (res_inst_tac [("s","while[b][g][iterate(Suc(0),step[b][g],x)]")] trans 1), |
|
75 (rtac (while_unfold2 RS spec) 1), |
|
76 (simp_tac iterate_ss 1) |
|
77 ]); |
|
78 |
|
79 |
|
80 (* --------------------------------------------------------------------------- *) |
|
81 (* properties of while and iterations *) |
|
82 (* --------------------------------------------------------------------------- *) |
|
83 |
|
84 val loop_lemma1 = prove_goal Loop.thy |
|
85 "[|? y.b[y]=FF; iterate(k,step[b][g],x)=UU|]==>iterate(Suc(k),step[b][g],x)=UU" |
|
86 (fn prems => |
|
87 [ |
|
88 (cut_facts_tac prems 1), |
|
89 (simp_tac iterate_ss 1), |
|
90 (rtac trans 1), |
|
91 (rtac step_def2 1), |
|
92 (asm_simp_tac HOLCF_ss 1), |
|
93 (etac exE 1), |
|
94 (etac (flat_tr RS flat_codom RS disjE) 1), |
|
95 (asm_simp_tac HOLCF_ss 1), |
|
96 (asm_simp_tac HOLCF_ss 1) |
|
97 ]); |
|
98 |
|
99 val loop_lemma2 = prove_goal Loop.thy |
|
100 "[|? y.b[y]=FF;~iterate(Suc(k),step[b][g],x)=UU |]==>\ |
|
101 \~iterate(k,step[b][g],x)=UU" |
|
102 (fn prems => |
|
103 [ |
|
104 (cut_facts_tac prems 1), |
|
105 (rtac contrapos 1), |
|
106 (etac loop_lemma1 2), |
|
107 (atac 1), |
|
108 (atac 1) |
|
109 ]); |
|
110 |
|
111 val loop_lemma3 = prove_goal Loop.thy |
|
112 "[|!x. INV(x) & b[x]=TT & ~g[x]=UU --> INV(g[x]);\ |
|
113 \? y.b[y]=FF; INV(x)|] ==>\ |
|
114 \~iterate(k,step[b][g],x)=UU --> INV(iterate(k,step[b][g],x))" |
|
115 (fn prems => |
|
116 [ |
|
117 (cut_facts_tac prems 1), |
|
118 (nat_ind_tac "k" 1), |
|
119 (asm_simp_tac iterate_ss 1), |
|
120 (strip_tac 1), |
|
121 (simp_tac (iterate_ss addsimps [step_def2]) 1), |
|
122 (res_inst_tac [("p","b[iterate(k1, step[b][g], x)]")] trE 1), |
|
123 (etac notE 1), |
|
124 (asm_simp_tac (HOLCF_ss addsimps [step_def2,iterate_Suc] ) 1), |
|
125 (asm_simp_tac HOLCF_ss 1), |
|
126 (rtac mp 1), |
|
127 (etac spec 1), |
|
128 (asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1), |
|
129 (res_inst_tac [("s","iterate(Suc(k1), step[b][g], x)"), |
|
130 ("t","g[iterate(k1, step[b][g], x)]")] ssubst 1), |
|
131 (atac 2), |
|
132 (asm_simp_tac (HOLCF_ss addsimps [iterate_Suc,step_def2] ) 1), |
|
133 (asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1) |
|
134 ]); |
|
135 |
|
136 |
|
137 val loop_lemma4 = prove_goal Loop.thy |
|
138 "!x. b[iterate(k,step[b][g],x)]=FF --> while[b][g][x]=iterate(k,step[b][g],x)" |
|
139 (fn prems => |
|
140 [ |
|
141 (nat_ind_tac "k" 1), |
|
142 (simp_tac iterate_ss 1), |
|
143 (strip_tac 1), |
|
144 (rtac (while_unfold RS ssubst) 1), |
|
145 (asm_simp_tac HOLCF_ss 1), |
|
146 (rtac allI 1), |
|
147 (rtac (iterate_Suc2 RS ssubst) 1), |
|
148 (strip_tac 1), |
|
149 (rtac trans 1), |
|
150 (rtac while_unfold3 1), |
|
151 (asm_simp_tac HOLCF_ss 1) |
|
152 ]); |
|
153 |
|
154 val loop_lemma5 = prove_goal Loop.thy |
|
155 "!k. ~b[iterate(k,step[b][g],x)]=FF ==>\ |
|
156 \ !m. while[b][g][iterate(m,step[b][g],x)]=UU" |
|
157 (fn prems => |
|
158 [ |
|
159 (cut_facts_tac prems 1), |
|
160 (rtac (while_def2 RS ssubst) 1), |
|
161 (rtac fix_ind 1), |
|
162 (rtac (allI RS adm_all) 1), |
|
163 (rtac adm_eq 1), |
|
164 (contX_tacR 1), |
|
165 (simp_tac HOLCF_ss 1), |
|
166 (rtac allI 1), |
|
167 (simp_tac HOLCF_ss 1), |
|
168 (res_inst_tac [("p","b[iterate(m, step[b][g],x)]")] trE 1), |
|
169 (asm_simp_tac HOLCF_ss 1), |
|
170 (asm_simp_tac HOLCF_ss 1), |
|
171 (res_inst_tac [("s","xa[iterate(Suc(m), step[b][g], x)]")] trans 1), |
|
172 (etac spec 2), |
|
173 (rtac cfun_arg_cong 1), |
|
174 (rtac trans 1), |
|
175 (rtac (iterate_Suc RS sym) 2), |
|
176 (asm_simp_tac (HOLCF_ss addsimps [step_def2]) 1), |
|
177 (dtac spec 1), |
|
178 (contr_tac 1) |
|
179 ]); |
|
180 |
|
181 |
|
182 val loop_lemma6 = prove_goal Loop.thy |
|
183 "!k. ~b[iterate(k,step[b][g],x)]=FF ==> while[b][g][x]=UU" |
|
184 (fn prems => |
|
185 [ |
|
186 (res_inst_tac [("t","x")] (iterate_0 RS subst) 1), |
|
187 (rtac (loop_lemma5 RS spec) 1), |
|
188 (resolve_tac prems 1) |
|
189 ]); |
|
190 |
|
191 val loop_lemma7 = prove_goal Loop.thy |
|
192 "~while[b][g][x]=UU ==> ? k. b[iterate(k,step[b][g],x)]=FF" |
|
193 (fn prems => |
|
194 [ |
|
195 (cut_facts_tac prems 1), |
|
196 (etac swap 1), |
|
197 (rtac loop_lemma6 1), |
|
198 (fast_tac HOL_cs 1) |
|
199 ]); |
|
200 |
|
201 val loop_lemma8 = prove_goal Loop.thy |
|
202 "~while[b][g][x]=UU ==> ? y. b[y]=FF" |
|
203 (fn prems => |
|
204 [ |
|
205 (cut_facts_tac prems 1), |
|
206 (dtac loop_lemma7 1), |
|
207 (fast_tac HOL_cs 1) |
|
208 ]); |
|
209 |
|
210 |
|
211 (* --------------------------------------------------------------------------- *) |
|
212 (* an invariant rule for loops *) |
|
213 (* --------------------------------------------------------------------------- *) |
|
214 |
|
215 val loop_inv2 = prove_goal Loop.thy |
|
216 "[| (!y. INV(y) & b[y]=TT & ~g[y]=UU --> INV(g[y]));\ |
|
217 \ (!y. INV(y) & b[y]=FF --> Q(y));\ |
|
218 \ INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])" |
|
219 (fn prems => |
|
220 [ |
|
221 (res_inst_tac [("P","%k.b[iterate(k,step[b][g],x)]=FF")] exE 1), |
|
222 (rtac loop_lemma7 1), |
|
223 (resolve_tac prems 1), |
|
224 (rtac ((loop_lemma4 RS spec RS mp) RS ssubst) 1), |
|
225 (atac 1), |
|
226 (rtac (nth_elem (1,prems) RS spec RS mp) 1), |
|
227 (rtac conjI 1), |
|
228 (atac 2), |
|
229 (rtac (loop_lemma3 RS mp) 1), |
|
230 (resolve_tac prems 1), |
|
231 (rtac loop_lemma8 1), |
|
232 (resolve_tac prems 1), |
|
233 (resolve_tac prems 1), |
|
234 (rtac classical3 1), |
|
235 (resolve_tac prems 1), |
|
236 (etac box_equals 1), |
|
237 (rtac (loop_lemma4 RS spec RS mp RS sym) 1), |
|
238 (atac 1), |
|
239 (rtac refl 1) |
|
240 ]); |
|
241 |
|
242 val loop_inv3 = prove_goal Loop.thy |
|
243 "[| !!y.[| INV(y); b[y]=TT; ~g[y]=UU|] ==> INV(g[y]);\ |
|
244 \ !!y.[| INV(y); b[y]=FF|]==> Q(y);\ |
|
245 \ INV(x); ~while[b][g][x]=UU |] ==> Q(while[b][g][x])" |
|
246 (fn prems => |
|
247 [ |
|
248 (rtac loop_inv2 1), |
|
249 (rtac allI 1), |
|
250 (rtac impI 1), |
|
251 (resolve_tac prems 1), |
|
252 (fast_tac HOL_cs 1), |
|
253 (fast_tac HOL_cs 1), |
|
254 (fast_tac HOL_cs 1), |
|
255 (rtac allI 1), |
|
256 (rtac impI 1), |
|
257 (resolve_tac prems 1), |
|
258 (fast_tac HOL_cs 1), |
|
259 (fast_tac HOL_cs 1), |
|
260 (resolve_tac prems 1), |
|
261 (resolve_tac prems 1) |
|
262 ]); |
|
263 |
|
264 val loop_inv = prove_goal Loop.thy |
|
265 "[| P(x);\ |
|
266 \ !!y.P(y) ==> INV(y);\ |
|
267 \ !!y.[| INV(y); b[y]=TT; ~g[y]=UU|] ==> INV(g[y]);\ |
|
268 \ !!y.[| INV(y); b[y]=FF|]==> Q(y);\ |
|
269 \ ~while[b][g][x]=UU |] ==> Q(while[b][g][x])" |
|
270 (fn prems => |
|
271 [ |
|
272 (rtac loop_inv3 1), |
|
273 (eresolve_tac prems 1), |
|
274 (atac 1), |
|
275 (atac 1), |
|
276 (resolve_tac prems 1), |
|
277 (atac 1), |
|
278 (atac 1), |
|
279 (resolve_tac prems 1), |
|
280 (resolve_tac prems 1), |
|
281 (resolve_tac prems 1) |
|
282 ]); |