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