9791
|
1 |
(* Title: HOL/BCV/Kildall.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2000 TUM
|
|
5 |
*)
|
|
6 |
|
|
7 |
Addsimps [Let_def];
|
|
8 |
Addsimps [le_iff_plus_unchanged RS sym];
|
|
9 |
|
|
10 |
Goalw [pres_type_def]
|
|
11 |
"[| pres_type step n A; s:A; p<n |] ==> step p s : A";
|
|
12 |
by (Blast_tac 1);
|
|
13 |
qed "pres_typeD";
|
|
14 |
|
|
15 |
Goalw [bounded_def]
|
|
16 |
"[| bounded succs n; p < n; q : set(succs p) |] ==> q < n";
|
|
17 |
by (Blast_tac 1);
|
|
18 |
qed "boundedD";
|
|
19 |
|
|
20 |
Goalw [mono_def]
|
|
21 |
"[| mono r step n A; p < n; s:A; s <=_r t |] ==> step p s <=_r step p t";
|
|
22 |
by (Blast_tac 1);
|
|
23 |
qed "monoD";
|
|
24 |
|
|
25 |
(** merges **)
|
|
26 |
|
|
27 |
Goal "!ss. size(merges f t ps ss) = size ss";
|
|
28 |
by (induct_tac "ps" 1);
|
|
29 |
by (Auto_tac);
|
|
30 |
qed_spec_mp "length_merges";
|
|
31 |
Addsimps [length_merges];
|
|
32 |
|
|
33 |
Goalw [closed_def]
|
|
34 |
"[| semilat(A,r,f) |] ==> \
|
|
35 |
\ !xs. xs : list n A --> x : A --> (!p : set ps. p<n) \
|
|
36 |
\ --> merges f x ps xs : list n A";
|
|
37 |
by(ftac semilatDclosedI 1);
|
|
38 |
by(rewtac closed_def);
|
|
39 |
by (induct_tac "ps" 1);
|
|
40 |
by (Auto_tac);
|
|
41 |
qed_spec_mp "merges_preserves_type";
|
|
42 |
Addsimps [merges_preserves_type];
|
|
43 |
|
|
44 |
Goal
|
|
45 |
"[| semilat(A,r,f) |] ==> \
|
|
46 |
\ !xs. xs : list n A --> x : A --> (!p:set ps. p<size xs) --> xs <=[r] merges f x ps xs";
|
|
47 |
by (induct_tac "ps" 1);
|
|
48 |
by (Asm_simp_tac 1);
|
|
49 |
by (Asm_full_simp_tac 1);
|
|
50 |
by (Clarify_tac 1);
|
|
51 |
by (rtac order_trans 1);
|
|
52 |
by(Asm_simp_tac 1);
|
|
53 |
by (etac list_update_incr 1);
|
|
54 |
ba 1;
|
|
55 |
by (Asm_simp_tac 1);
|
|
56 |
by (Asm_simp_tac 1);
|
|
57 |
by (blast_tac (claset() addSIs [listE_set]
|
|
58 |
addIs [closedD,listE_length RS nth_in]) 1);
|
|
59 |
qed_spec_mp "merges_incr";
|
|
60 |
|
|
61 |
Goal
|
|
62 |
"[| semilat(A,r,f) |] ==> \
|
|
63 |
\ (!xs. xs : list n A --> x:A --> (!p:set ps. p<size xs) --> \
|
|
64 |
\ (merges f x ps xs = xs) = (!p:set ps. x <=_r xs!p))";
|
|
65 |
by (induct_tac "ps" 1);
|
|
66 |
by (Asm_simp_tac 1);
|
|
67 |
by (Clarsimp_tac 1);
|
|
68 |
by (rename_tac "p ps xs" 1);
|
|
69 |
by (rtac iffI 1);
|
|
70 |
by (rtac context_conjI 1);
|
|
71 |
by (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs" 1);
|
|
72 |
by (EVERY[etac subst 2, rtac merges_incr 2]);
|
|
73 |
by(force_tac (claset() addSDs [le_listD],
|
|
74 |
simpset() addsimps [nth_list_update]) 1);
|
|
75 |
by (assume_tac 1);
|
|
76 |
by (blast_tac (claset() addSIs [listE_set]
|
|
77 |
addIs [closedD,listE_length RS nth_in]) 1);
|
|
78 |
ba 1;
|
|
79 |
by(Asm_simp_tac 1);
|
|
80 |
by (Clarify_tac 1);
|
|
81 |
by (rotate_tac ~2 1);
|
|
82 |
by (asm_full_simp_tac (simpset() addsimps
|
|
83 |
[le_iff_plus_unchanged RS iffD1,
|
|
84 |
list_update_same_conv RS iffD2]) 1);
|
|
85 |
by (Clarify_tac 1);
|
|
86 |
by (asm_simp_tac (simpset() addsimps
|
|
87 |
[le_iff_plus_unchanged RS iffD1,
|
|
88 |
list_update_same_conv RS iffD2]) 1);
|
|
89 |
qed_spec_mp "merges_same_conv";
|
|
90 |
|
|
91 |
|
|
92 |
Goalw [Listn.le_def,lesub_def,semilat_def]
|
|
93 |
"set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs --> \
|
|
94 |
\ x <=_r ys!p --> semilat(A,r,f) --> x:A --> \
|
|
95 |
\ xs[p := x +_f xs!p] <=[r] ys";
|
|
96 |
by (simp_tac (simpset() addsimps [list_all2_conv_all_nth,nth_list_update]) 1);
|
|
97 |
qed_spec_mp "list_update_le_listI";
|
|
98 |
|
|
99 |
Goalw [closed_def]
|
|
100 |
"[| semilat(A,r,f); set ts <= A; t:A; \
|
|
101 |
\ !p. p:set ps --> t <=_r ts!p; \
|
|
102 |
\ !p. p:set ps --> p<size ts |] ==> \
|
|
103 |
\ set qs <= set ps --> \
|
|
104 |
\ (!ss. set ss <= A --> ss <=[r] ts --> merges f t qs ss <=[r] ts)";
|
|
105 |
by (induct_tac "qs" 1);
|
|
106 |
by (Asm_simp_tac 1);
|
|
107 |
by (Asm_simp_tac 1);
|
|
108 |
by (Clarify_tac 1);
|
|
109 |
by (rotate_tac ~2 1);
|
|
110 |
by (Asm_full_simp_tac 1);
|
|
111 |
by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
|
|
112 |
by (asm_simp_tac (simpset() addsimps [closedD]) 1);
|
|
113 |
by (asm_full_simp_tac (simpset() addsimps [list_update_le_listI]) 1);
|
|
114 |
val lemma = result();
|
|
115 |
|
|
116 |
Goal
|
|
117 |
"[| semilat(A,r,f); t:A; set ts <= A; set ss <= A; \
|
|
118 |
\ !p. p:set ps --> t <=_r ts!p; \
|
|
119 |
\ !p. p:set ps --> p<size ts; \
|
|
120 |
\ ss <=[r] ts |] \
|
|
121 |
\ ==> merges f t ps ss <=[r] ts";
|
|
122 |
by (blast_tac (claset() addDs [lemma]) 1);
|
|
123 |
qed "merges_pres_le_ub";
|
|
124 |
|
|
125 |
Goal "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A --> \
|
|
126 |
\ (!p:set ps. p<n) --> \
|
|
127 |
\ (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)";
|
|
128 |
by(induct_tac "ps" 1);
|
|
129 |
by (Simp_tac 1);
|
|
130 |
by(asm_simp_tac (simpset() addsimps [nth_list_update,closedD,listE_nth_in]) 1);
|
|
131 |
qed_spec_mp "nth_merges";
|
|
132 |
|
|
133 |
|
|
134 |
(** propa **)
|
|
135 |
|
|
136 |
Goal "!ss w. (!q:set qs. q < size ss) --> \
|
|
137 |
\ propa f qs t ss w = \
|
|
138 |
\ (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)";
|
|
139 |
by (induct_tac "qs" 1);
|
|
140 |
by(Simp_tac 1);
|
|
141 |
by (Simp_tac 1);
|
|
142 |
by(Clarify_tac 1);
|
|
143 |
br conjI 1;
|
|
144 |
by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
|
|
145 |
by(Blast_tac 1);
|
|
146 |
by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
|
|
147 |
by(Blast_tac 1);
|
|
148 |
qed_spec_mp "decomp_propa";
|
|
149 |
|
|
150 |
(** iter **)
|
|
151 |
|
|
152 |
val [iter_wf,iter_tc] = iter.tcs;
|
|
153 |
|
|
154 |
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
|
|
155 |
by(REPEAT(rtac wf_same_fstI 1));
|
|
156 |
by(split_all_tac 1);
|
|
157 |
by(asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1);
|
|
158 |
by(REPEAT(rtac wf_same_fstI 1));
|
|
159 |
br wf_lex_prod 1;
|
|
160 |
br wf_finite_psubset 2; (* FIXME *)
|
|
161 |
by(Clarify_tac 1);
|
|
162 |
bd (semilatDorderI RS acc_le_listI) 1;
|
|
163 |
ba 1;
|
|
164 |
by(rewrite_goals_tac [acc_def,lesssub_def]);
|
|
165 |
ba 1;
|
|
166 |
qed "iter_wf";
|
|
167 |
|
|
168 |
Goalw [lesssub_def]
|
|
169 |
"[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==> \
|
|
170 |
\ ss <[r] merges f t qs ss | \
|
|
171 |
\ merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w";
|
|
172 |
by (asm_simp_tac (simpset() addsimps [merges_incr]) 1);
|
|
173 |
br impI 1;
|
|
174 |
bd (sym RS (rotate_prems 4 (merges_same_conv RS iffD1))) 1;
|
|
175 |
ba 1;
|
|
176 |
ba 1;
|
|
177 |
ba 1;
|
|
178 |
by(Asm_simp_tac 1);
|
|
179 |
by (asm_simp_tac (simpset() addcongs [conj_cong]
|
|
180 |
addsimps [le_iff_plus_unchanged RS sym]) 1);
|
|
181 |
by (blast_tac (claset() addSIs [psubsetI] addEs [equalityE]) 1);
|
|
182 |
qed "inter_tc_lemma";
|
|
183 |
|
|
184 |
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc));
|
|
185 |
by(asm_simp_tac (simpset() addsimps [same_fst_def,pres_type_def]) 1);
|
|
186 |
by(clarify_tac (claset() delrules [disjCI]) 1);
|
|
187 |
by(subgoal_tac "(@p. p:w) : w" 1);
|
9970
|
188 |
by (fast_tac (claset() addIs [someI]) 2);
|
9791
|
189 |
by(subgoal_tac "ss : list (size ss) A" 1);
|
|
190 |
by (blast_tac (claset() addSIs [listI]) 2);
|
|
191 |
by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
|
|
192 |
by (blast_tac (claset() addDs [boundedD]) 2);
|
|
193 |
by(rotate_tac 1 1);
|
|
194 |
by(asm_full_simp_tac (simpset() delsimps [listE_length]
|
|
195 |
addsimps [decomp_propa,finite_psubset_def,inter_tc_lemma,
|
|
196 |
bounded_nat_set_is_finite]) 1);
|
|
197 |
qed "iter_tc";
|
|
198 |
|
|
199 |
val prems = goal thy
|
|
200 |
"(!!A r f step succs ss w. \
|
|
201 |
\ (!p. p = (@ p. p : w) & w ~= {} & semilat(A,r,f) & acc r & \
|
|
202 |
\ (!p:w. p < length ss) & bounded succs (length ss) & \
|
|
203 |
\ set ss <= A & pres_type step (length ss) A \
|
|
204 |
\ --> P A r f step succs (merges f (step p (ss!p)) (succs p) ss) \
|
|
205 |
\ ({q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))\
|
|
206 |
\ ==> P A r f step succs ss w) ==> P A r f step succs ss w";
|
|
207 |
by(res_inst_tac [("P","P")] (iter_tc RS (iter_wf RS iter.induct)) 1);
|
|
208 |
by(rename_tac "w" 1);
|
|
209 |
brs prems 1;
|
|
210 |
by(Clarify_tac 1);
|
|
211 |
by(asm_full_simp_tac (simpset()) 1);
|
|
212 |
by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
|
|
213 |
by(rotate_tac ~1 1);
|
|
214 |
by(asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1);
|
|
215 |
by(subgoal_tac "(@p. p:w) : w" 1);
|
9970
|
216 |
by (fast_tac (claset() addIs [someI]) 2);
|
9791
|
217 |
by (blast_tac (claset() addDs [boundedD]) 1);
|
|
218 |
qed "iter_induct";
|
|
219 |
|
|
220 |
Goal
|
|
221 |
"[| semilat(A,r,f); acc r; set ss <= A; pres_type step (length ss) A; \
|
|
222 |
\ bounded succs (size ss); !p:w. p<size ss |] ==> \
|
|
223 |
\ iter(((A,r,f),step,succs),ss,w) = \
|
|
224 |
\ (if w={} then ss \
|
|
225 |
\ else let p = SOME p. p : w \
|
|
226 |
\ in iter(((A,r,f),step,succs),merges f (step p (ss!p)) (succs p) ss, \
|
|
227 |
\ {q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))";
|
|
228 |
by (rtac ((iter_tc RS (iter_wf RS (hd iter.simps))) RS trans) 1);
|
|
229 |
by (Asm_simp_tac 1);
|
|
230 |
br impI 1;
|
|
231 |
by(stac decomp_propa 1);
|
|
232 |
by(subgoal_tac "(@p. p:w) : w" 1);
|
9970
|
233 |
by (fast_tac (claset() addIs [someI]) 2);
|
9791
|
234 |
by (blast_tac (claset() addDs [boundedD]) 1);
|
|
235 |
by (Simp_tac 1);
|
|
236 |
qed "iter_unfold";
|
|
237 |
|
|
238 |
Goalw [stable_def]
|
|
239 |
"[| semilat (A,r,f); pres_type step n A; bounded succs n; \
|
|
240 |
\ ss : list n A; p : w; ! q:w. q < n; \
|
|
241 |
\ ! q. q < n --> q ~: w --> stable r step succs ss q; q < n; \
|
|
242 |
\ q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q; \
|
|
243 |
\ q ~: w | q = p |] ==> \
|
|
244 |
\ stable r step succs (merges f (step p (ss!p)) (succs p) ss) q";
|
|
245 |
by(subgoal_tac "step p (ss!p) : A" 1);
|
|
246 |
by (blast_tac (claset() addIs [listE_nth_in,pres_typeD]) 2);
|
|
247 |
by (Simp_tac 1);
|
|
248 |
by(Clarify_tac 1);
|
|
249 |
by(stac nth_merges 1);
|
|
250 |
ba 1;
|
|
251 |
ba 1;
|
|
252 |
ba 2;
|
|
253 |
by (blast_tac (claset() addDs [boundedD]) 1);
|
|
254 |
by (blast_tac (claset() addDs [boundedD]) 1);
|
|
255 |
by(stac nth_merges 1);
|
|
256 |
ba 1;
|
|
257 |
ba 1;
|
|
258 |
ba 2;
|
|
259 |
by (blast_tac (claset() addDs [boundedD]) 1);
|
|
260 |
by (blast_tac (claset() addDs [boundedD]) 1);
|
|
261 |
by (Simp_tac 1);
|
|
262 |
br conjI 1;
|
|
263 |
by(Clarify_tac 1);
|
|
264 |
by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
|
|
265 |
by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1);
|
|
266 |
by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1);
|
|
267 |
qed "stable_pres_lemma";
|
|
268 |
|
|
269 |
Goalw [stable_def]
|
|
270 |
"[| semilat (A,r,f); mono r step n A; bounded succs n; \
|
|
271 |
\ step p (ss!p) : A; ss : list n A; ts : list n A; p < n; \
|
|
272 |
\ ss <=[r] ts; ! p. p < n --> stable r step succs ts p |] \
|
|
273 |
\ ==> merges f (step p (ss!p)) (succs p) ss <=[r] ts";
|
|
274 |
by (blast_tac (claset()
|
|
275 |
addSIs [listE_set,monoD,listE_nth_in,le_listD,less_lengthI]
|
|
276 |
addIs [merges_pres_le_ub,order_trans]
|
|
277 |
addDs [pres_typeD,boundedD]) 1);
|
|
278 |
qed_spec_mp "merges_bounded_lemma";
|
|
279 |
|
|
280 |
Unify.trace_bound := 80;
|
|
281 |
Unify.search_bound := 90;
|
|
282 |
Goalw [stables_def]
|
|
283 |
"semilat(A,r,f) & acc r & pres_type step n A & mono r step n A & \
|
|
284 |
\ bounded succs n & (! p:w. p < n) & ss:list n A & \
|
|
285 |
\ (!p<n. p~:w --> stable r step succs ss p) \
|
|
286 |
\ --> iter(((A,r,f),step,succs),ss,w) : list n A & \
|
|
287 |
\ stables r step succs (iter(((A,r,f),step,succs),ss,w)) & \
|
|
288 |
\ ss <=[r] iter(((A,r,f),step,succs),ss,w) & \
|
|
289 |
\ (! ts:list n A. \
|
|
290 |
\ ss <=[r] ts & stables r step succs ts --> \
|
|
291 |
\ iter(((A,r,f),step,succs),ss,w) <=[r] ts)";
|
|
292 |
by(res_inst_tac [("A","A"),("r","r"),("f","f"),("step","step"),("ss","ss"),("w","w")]iter_induct 1);
|
|
293 |
by(Clarify_tac 1);
|
|
294 |
by(ftac listE_length 1);
|
|
295 |
by(hyp_subst_tac 1);
|
|
296 |
by(stac iter_unfold 1);
|
|
297 |
ba 1;
|
|
298 |
ba 1;
|
|
299 |
by (Asm_simp_tac 1);
|
|
300 |
ba 1;
|
|
301 |
ba 1;
|
|
302 |
ba 1;
|
|
303 |
by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
|
|
304 |
br impI 1;
|
|
305 |
be allE 1;
|
|
306 |
be impE 1;
|
|
307 |
by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
|
|
308 |
by(subgoal_tac "(@p. p:w) : w" 1);
|
9970
|
309 |
by (fast_tac (claset() addIs [someI]) 2);
|
9791
|
310 |
by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
|
|
311 |
by (blast_tac (claset() addIs [pres_typeD,listE_nth_in]) 2);
|
|
312 |
be impE 1;
|
|
313 |
by(asm_simp_tac (simpset() delsimps [listE_length,le_iff_plus_unchanged RS sym]) 1);
|
|
314 |
br conjI 1;
|
|
315 |
by (blast_tac (claset() addDs [boundedD]) 1);
|
|
316 |
br conjI 1;
|
|
317 |
by(blast_tac (claset() addIs[merges_preserves_type]addDs[boundedD]) 1);
|
|
318 |
by (blast_tac (claset() addSIs [stable_pres_lemma]) 1);
|
|
319 |
by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
|
|
320 |
by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
|
|
321 |
by (blast_tac (claset() addDs [boundedD]) 2);
|
|
322 |
by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
|
|
323 |
by (blast_tac (claset() addIs [pres_typeD]) 2);
|
|
324 |
br conjI 1;
|
|
325 |
by (blast_tac (claset() addSIs [merges_incr] addIs [le_list_trans]) 1);
|
|
326 |
by(Clarify_tac 1);
|
|
327 |
by(EVERY1[dtac bspec, atac, etac mp]);
|
|
328 |
by(asm_full_simp_tac (simpset() delsimps [listE_length]) 1);
|
|
329 |
by (blast_tac (claset() addIs [merges_bounded_lemma]) 1);
|
|
330 |
qed_spec_mp "iter_properties";
|
|
331 |
|
|
332 |
|
|
333 |
Goalw [is_dfa_def,kildall_def]
|
|
334 |
"[| semilat(A,r,f); acc r; pres_type step n A; \
|
|
335 |
\ mono r step n A; bounded succs n|] ==> \
|
|
336 |
\ is_dfa r (kildall (A,r,f) step succs) step succs n A";
|
|
337 |
by(Clarify_tac 1);
|
|
338 |
by(Simp_tac 1);
|
|
339 |
br iter_properties 1;
|
|
340 |
by(asm_simp_tac (simpset() addsimps [unstables_def,stable_def]) 1);
|
|
341 |
by(blast_tac (claset() addSIs [le_iff_plus_unchanged RS iffD2,listE_nth_in]
|
|
342 |
addDs [boundedD,pres_typeD]) 1);
|
|
343 |
qed "is_dfa_kildall";
|
|
344 |
|
|
345 |
Goal
|
|
346 |
"[| semilat(A,r,f); acc r; top r T; \
|
|
347 |
\ pres_type step n A; bounded succs n; \
|
|
348 |
\ mono r step n A; wti_is_stable_topless r T step wti succs n A |] \
|
|
349 |
\ ==> is_bcv r T wti n A (kildall (A,r,f) step succs)";
|
|
350 |
by (REPEAT(ares_tac [is_bcv_dfa,is_dfa_kildall,semilatDorderI] 1));
|
|
351 |
qed "is_bcv_kildall";
|