|
1 (* Title: HOL/BCV/DFAimpl.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1999 TUM |
|
5 *) |
|
6 |
|
7 (** merges **) |
|
8 |
|
9 Goal "!sos. size(merges t ps sos) = size sos"; |
|
10 by(induct_tac "ps" 1); |
|
11 by(Auto_tac); |
|
12 qed_spec_mp "length_merges"; |
|
13 Addsimps [length_merges]; |
|
14 |
|
15 Goal |
|
16 "!xs. xs : listsn n (option A) --> x : A --> (!p : set ps. p<n) --> \ |
|
17 \ semilat A --> merges x ps xs : listsn n (option A)"; |
|
18 by(induct_tac "ps" 1); |
|
19 by(Auto_tac); |
|
20 qed_spec_mp "merges_preserves_type"; |
|
21 Addsimps [merges_preserves_type]; |
|
22 (*AddSIs [merges_preserves_type];*) |
|
23 |
|
24 Goal "semilat A ==> !xs. xs : listsn n (option A) --> x:A --> (!p:set ps. p<n) \ |
|
25 \ --> xs <= merges x ps xs"; |
|
26 by(induct_tac "ps" 1); |
|
27 by(Simp_tac 1); |
|
28 by(Simp_tac 1); |
|
29 by(Clarify_tac 1); |
|
30 br order_trans 1; |
|
31 be list_update_incr 1; |
|
32 by(Blast_tac 2); |
|
33 ba 2; |
|
34 be (Some_in_option RS iffD2) 1; |
|
35 by(blast_tac (claset() addSIs [listsnE_set] |
|
36 addIs [semilat_plus,listsnE_length RS nth_in]) 1); |
|
37 qed_spec_mp "merges_incr"; |
|
38 |
|
39 (* is redundant but useful *) |
|
40 Goal "[| xs!i = Some x; xs : listsn n (option A); i < n |] ==> x:A"; |
|
41 bd listsnE_nth_in 1; |
|
42 ba 1; |
|
43 by(Asm_full_simp_tac 1); |
|
44 qed "listsn_optionE_in"; |
|
45 (*Addsimps [listsn_optionE_in];*) |
|
46 |
|
47 Goal |
|
48 "[| semilat L |] ==> \ |
|
49 \ (!xs. xs : listsn n (option L) --> x:L --> (!p:set ps. p<n) --> \ |
|
50 \ (merges x ps xs = xs) = (!p:set ps. Some x <= xs!p))"; |
|
51 by(induct_tac "ps" 1); |
|
52 by(Asm_simp_tac 1); |
|
53 by(Clarsimp_tac 1); |
|
54 by(rename_tac "p ps xs" 1); |
|
55 br iffI 1; |
|
56 br context_conjI 1; |
|
57 by(subgoal_tac "xs[p := Some x + xs!p] <= xs" 1); |
|
58 by(EVERY[etac subst 2, rtac merges_incr 2]); |
|
59 ba 2; |
|
60 by(Force_tac 2); |
|
61 ba 2; |
|
62 ba 2; |
|
63 by(exhaust_tac "xs!p" 1); |
|
64 by(asm_full_simp_tac (simpset() addsimps [list_update_le_conv]) 1); |
|
65 by(asm_full_simp_tac (simpset() addsimps |
|
66 [list_update_le_conv,listsn_optionE_in]) 1); |
|
67 by(Clarify_tac 1); |
|
68 by(rotate_tac ~3 1); |
|
69 by(asm_full_simp_tac (simpset() addsimps |
|
70 [le_iff_plus_unchanged RS iffD1,listsn_optionE_in, |
|
71 list_update_same_conv RS iffD2]) 1); |
|
72 by(Clarify_tac 1); |
|
73 by(asm_simp_tac (simpset() addsimps |
|
74 [le_iff_plus_unchanged RS iffD1,listsn_optionE_in, |
|
75 list_update_same_conv RS iffD2]) 1); |
|
76 qed_spec_mp "merges_same_conv"; |
|
77 |
|
78 |
|
79 Goalw [le_list,plus_option] |
|
80 "xs <= ys --> xs : listsn n (option L) --> ys : listsn n (option L) --> \ |
|
81 \ p < n --> ys!p = Some y --> x <= y --> x : L --> semilat L --> \ |
|
82 \ xs[p := Some x + xs!p] <= ys"; |
|
83 by(simp_tac (simpset() addsimps [nth_list_update] |
|
84 addsplits [option.split]) 1); |
|
85 by(Clarify_tac 1); |
|
86 by(rotate_tac 3 1); |
|
87 by(force_tac (claset() addEs [listsn_optionE_in] addIs [semilat_lub], |
|
88 simpset()) 1); |
|
89 qed_spec_mp "list_update_le_listI"; |
|
90 |
|
91 Goal |
|
92 "[| semilat(L); t:L; tos : listsn n (option L); \ |
|
93 \ !p. p:set ps --> Some t <= tos!p; \ |
|
94 \ !p. p:set ps --> p<n |] ==> \ |
|
95 \ set qs <= set ps --> \ |
|
96 \ (!sos. sos : listsn n (option L) & sos <= tos --> merges t qs sos <= tos)"; |
|
97 by(induct_tac "qs" 1); |
|
98 by(Asm_simp_tac 1); |
|
99 by(force_tac (claset(),simpset() addsimps [list_update_le_listI]) 1); |
|
100 val lemma = result(); |
|
101 |
|
102 Goal |
|
103 "[| semilat(L); t:L; \ |
|
104 \ !p. p:set ps --> Some t <= tos!p; \ |
|
105 \ !p. p:set ps --> p<n; \ |
|
106 \ sos <= tos; sos : listsn n (option L); tos : listsn n (option L) |] \ |
|
107 \ ==> merges t ps sos <= tos"; |
|
108 by(blast_tac (claset() addDs [lemma]) 1); |
|
109 qed "merges_pres_le_ub"; |
|
110 |
|
111 |
|
112 (** next **) |
|
113 |
|
114 Goalw [is_next_def] |
|
115 "[| is_next next; next step succs sos = None; succs_bounded succs n; \ |
|
116 \ sos : listsn n S |] ==> \ |
|
117 \ ? p<n. ? s. sos!p = Some s & step p s = None"; |
|
118 by(subgoal_tac "n=size sos" 1); |
|
119 by(Blast_tac 1); |
|
120 by(Asm_simp_tac 1); |
|
121 qed "next_None"; |
|
122 |
|
123 Goalw [is_next_def] |
|
124 "[| is_next next; succs_bounded succs n; sos : listsn n S |] ==> \ |
|
125 \ next step succs sos = Some sos --> \ |
|
126 \ (!p<n. !s. sos!p = Some s --> (? t. \ |
|
127 \ step p s = Some(t) & merges t (succs p) sos = sos))"; |
|
128 by(subgoal_tac "n=size sos" 1); |
|
129 by(Blast_tac 1); |
|
130 by(Asm_simp_tac 1); |
|
131 qed "next_Some1"; |
|
132 |
|
133 Goalw [is_next_def] |
|
134 "[| is_next next; next step succs sos = Some sos'; sos' ~= sos; \ |
|
135 \ succs_bounded succs n; sos : listsn n S |] ==> \ |
|
136 \ ? p<n. ? s. sos!p = Some s & (? t. \ |
|
137 \ step p s = Some(t) & merges t (succs p) sos = sos')"; |
|
138 by(subgoal_tac "n=size sos" 1); |
|
139 by(Blast_tac 1); |
|
140 by(Asm_simp_tac 1); |
|
141 qed "next_Some2"; |
|
142 |
|
143 Goal |
|
144 "[| is_next next; succs_bounded succs n; sos : listsn n S |] ==> \ |
|
145 \ (next step succs sos = Some sos) = \ |
|
146 \ (!p<n. !s. sos!p = Some s --> (? t. \ |
|
147 \ step p s = Some(t) & merges t (succs p) sos = sos))"; |
|
148 br iffI 1; |
|
149 by(asm_simp_tac (simpset() addsimps [next_Some1]) 1); |
|
150 by(exhaust_tac "next step succs sos" 1); |
|
151 by(best_tac (claset() addSDs [next_None] addss simpset()) 1); |
|
152 by(rename_tac "sos'" 1); |
|
153 by(case_tac "sos' = sos" 1); |
|
154 by(Blast_tac 1); |
|
155 by(best_tac (claset() addSDs [next_Some2] addss simpset()) 1); |
|
156 qed "next_Some1_eq"; |
|
157 |
|
158 Addsimps [next_Some1_eq]; |
|
159 |
|
160 Goalw [step_pres_type_def] |
|
161 "[| step_pres_type step n L; s:L; p<n; step p s = Some(t) |] ==> t:L"; |
|
162 by(Blast_tac 1); |
|
163 qed "step_pres_typeD"; |
|
164 |
|
165 Goalw [succs_bounded_def] |
|
166 "[| succs_bounded succs n; p < n; q : set(succs p) |] ==> q < n"; |
|
167 by(Blast_tac 1); |
|
168 qed "succs_boundedD"; |
|
169 |
|
170 Goal |
|
171 "[| is_next next; semilat A; \ |
|
172 \ step_pres_type step n A; succs_bounded succs n;\ |
|
173 \ sos : listsn n (option A) |] ==> \ |
|
174 \ next step succs sos : option (listsn n (option A))"; |
|
175 by(exhaust_tac "next step succs sos" 1); |
|
176 by(ALLGOALS Asm_simp_tac); |
|
177 by(rename_tac "sos'" 1); |
|
178 by(case_tac "sos' = sos" 1); |
|
179 by(Asm_simp_tac 1); |
|
180 by(blast_tac (claset() addIs [step_pres_typeD,succs_boundedD,listsn_optionE_in] addSIs [merges_preserves_type] addDs [next_Some2]) 1); |
|
181 qed_spec_mp "next_preserves_type"; |
|
182 |
|
183 Goal |
|
184 "[| is_next next; semilat A; \ |
|
185 \ step_pres_type step n A; succs_bounded succs n; \ |
|
186 \ next step succs xs = Some ys; xs : listsn n (option A) |] ==> xs <= ys"; |
|
187 by(case_tac "ys = xs" 1); |
|
188 by(Asm_full_simp_tac 1); |
|
189 by(blast_tac (claset() addSIs [merges_incr] addIs [listsn_optionE_in] |
|
190 addDs [step_pres_typeD,succs_boundedD,next_Some2]) 1); |
|
191 qed_spec_mp "next_incr"; |
|
192 |
|
193 val lemma = (Unify.trace_bound, Unify.search_bound); |
|
194 Unify.trace_bound := 50; |
|
195 Unify.search_bound := 50; |
|
196 |
|
197 Goalw [is_next_def] |
|
198 "is_next (%step succs sos. itnext (size sos) step succs sos)"; |
|
199 by(Clarify_tac 1); |
|
200 by(etac thin_rl 1); |
|
201 by(res_inst_tac [("n","length sos")] nat_induct 1); |
|
202 by(Asm_full_simp_tac 1); |
|
203 by(asm_full_simp_tac (simpset() addsimps [less_Suc_eq,Let_def] |
|
204 addsplits [option.split])1); |
|
205 by(Blast_tac 1); |
|
206 qed "is_next_itnext"; |
|
207 |
|
208 Unify.trace_bound := !(fst lemma); |
|
209 Unify.search_bound := !(snd lemma); |
|
210 |
|
211 (** fix step **) |
|
212 |
|
213 Goalw [step_mono_None_def] |
|
214 "[| step_mono_None step n L; s : L; p < n; s <= t; step p s = None |] ==> \ |
|
215 \ step p t = None"; |
|
216 by(Blast_tac 1); |
|
217 qed "step_mono_NoneD"; |
|
218 |
|
219 Goalw [step_mono_def] |
|
220 "[| step_mono step n L; s : L; p < n; s <= t; step p s = Some(u) |] ==> \ |
|
221 \ !v. step p t = Some(v) --> u <= v"; |
|
222 by(Blast_tac 1); |
|
223 qed "step_monoD"; |
|
224 |
|
225 Goalw [stable_def] |
|
226 "[| is_next next; semilat L; sos : listsn n (option L); \ |
|
227 \ step_pres_type step n L; succs_bounded succs n |] \ |
|
228 \ ==> (next step succs sos = Some sos) = (!p<n. stable step succs p sos)"; |
|
229 by(Asm_simp_tac 1); |
|
230 br iffI 1; |
|
231 by(Clarify_tac 1); |
|
232 by(etac allE 1 THEN mp_tac 1); |
|
233 by(etac allE 1 THEN mp_tac 1); |
|
234 by(Clarify_tac 1); |
|
235 bd(merges_same_conv RS iffD1)1; |
|
236 ba 4; |
|
237 ba 1; |
|
238 by(blast_tac (claset() addIs [step_pres_typeD,listsn_optionE_in]) 1); |
|
239 by(blast_tac (claset() addIs [succs_boundedD,listsn_optionE_in]) 1); |
|
240 by(Blast_tac 1); |
|
241 by(Clarify_tac 1); |
|
242 by(etac allE 1 THEN mp_tac 1); |
|
243 by(Asm_full_simp_tac 1); |
|
244 by(Clarify_tac 1); |
|
245 by(Asm_simp_tac 1); |
|
246 by(blast_tac (claset() addSIs [merges_same_conv RS iffD2] |
|
247 addIs [step_pres_typeD,succs_boundedD,listsn_optionE_in]) 1); |
|
248 qed "fixpoint_next_iff_stable"; |
|
249 |
|
250 Goal |
|
251 "[| semilat L; is_next next; succs_bounded succs n; \ |
|
252 \ step_pres_type step n L; step_mono_None step n L; step_mono step n L; \ |
|
253 \ tos:listsn n (option L); next step succs tos = Some tos; \ |
|
254 \ sos:listsn n (option L); sos <= tos |] \ |
|
255 \ ==> ? sos'. next step succs sos = Some sos' & sos' <= tos"; |
|
256 by(subgoal_tac |
|
257 "!p<n. !s. sos!p = Some s --> (? u. \ |
|
258 \ step p s = Some(u) & (!q:set(succs p). Some u<=tos!q))" 1); |
|
259 by(exhaust_tac "next step succs sos" 1); |
|
260 bd next_None 1; |
|
261 ba 1; |
|
262 ba 1; |
|
263 ba 1; |
|
264 by(Force_tac 1); |
|
265 by(rename_tac "sos'" 1); |
|
266 by(case_tac "sos' = sos" 1); |
|
267 by(Blast_tac 1); |
|
268 bd next_Some2 1; |
|
269 by(EVERY1[atac, atac, atac, atac]); |
|
270 by(Clarify_tac 1); |
|
271 by(etac allE 1 THEN mp_tac 1); |
|
272 by(etac allE 1 THEN mp_tac 1); |
|
273 by(Clarify_tac 1); |
|
274 by(EVERY1[rtac exI, rtac conjI, atac]); |
|
275 br merges_pres_le_ub 1; |
|
276 ba 1; |
|
277 by(blast_tac (claset() addIs [step_pres_typeD,listsn_optionE_in]) 1); |
|
278 by(Asm_full_simp_tac 1); |
|
279 by(blast_tac (claset() addIs [succs_boundedD,listsn_optionE_in]) 1); |
|
280 by(REPEAT(atac 1)); |
|
281 by(Clarify_tac 1); |
|
282 by(exhaust_tac "tos!p" 1); |
|
283 by(force_tac (claset() addDs [le_listD],simpset()) 1); |
|
284 by(rename_tac "t" 1); |
|
285 by(subgoal_tac "s <= t" 1); |
|
286 by(force_tac (claset() addDs [le_listD],simpset()) 2); |
|
287 by(exhaust_tac "step p s" 1); |
|
288 bd step_mono_NoneD 1; |
|
289 ba 4; |
|
290 by(blast_tac (claset() addIs [listsn_optionE_in]) 1); |
|
291 ba 1; |
|
292 ba 1; |
|
293 by(Force_tac 1); |
|
294 bd step_monoD 1; |
|
295 ba 4; |
|
296 by(blast_tac (claset() addIs [listsn_optionE_in]) 1); |
|
297 ba 1; |
|
298 ba 1; |
|
299 by(Asm_full_simp_tac 1); |
|
300 by(etac allE 1 THEN mp_tac 1); |
|
301 by(etac allE 1 THEN mp_tac 1); |
|
302 by(Clarify_tac 1); |
|
303 by(Asm_full_simp_tac 1); |
|
304 by(forward_tac[merges_same_conv RS iffD1]1); |
|
305 ba 4; |
|
306 ba 1; |
|
307 by(blast_tac (claset() addIs [step_pres_typeD,listsn_optionE_in]) 1); |
|
308 by(blast_tac (claset() addIs [succs_boundedD,listsn_optionE_in]) 1); |
|
309 by(blast_tac (claset() addIs [order_trans]) 1); |
|
310 val lemma = result(); |
|
311 |
|
312 Goalw [is_dfa_def] |
|
313 "[| semilat L; acc L; is_next next; \ |
|
314 \ step_pres_type step n L; succs_bounded succs n; \ |
|
315 \ step_mono_None step n L; step_mono step n L |] ==> \ |
|
316 \ is_dfa (%sos. fix(next step succs, sos)) step succs n L"; |
|
317 by(Clarify_tac 1); |
|
318 by(stac fix_iff_has_fixpoint 1); |
|
319 by(etac (acc_option RS acc_listsn) 1); |
|
320 by(blast_tac (claset() addIs [lemma]) 1); |
|
321 by(blast_tac (claset() addIs [next_preserves_type]) 1); |
|
322 by(blast_tac (claset() addIs [next_incr]) 1); |
|
323 ba 1; |
|
324 by(asm_simp_tac (simpset() delsimps [next_Some1_eq] addsimps [fixpoint_next_iff_stable]) 1); |
|
325 qed "is_dfa_fix_next"; |
|
326 |
|
327 Goal |
|
328 "[| semilat L; acc L; is_next next; \ |
|
329 \ step_pres_type step n L; succs_bounded succs n; \ |
|
330 \ step_mono_None step n L; step_mono step n L; \ |
|
331 \ wti_is_fix_step step wti succs n L; \ |
|
332 \ sos : listsn n (option L) |] ==> \ |
|
333 \ fix(next step succs, sos) = \ |
|
334 \ (? tos:listsn n (option L). sos<=tos & welltyping wti tos)"; |
|
335 by(blast_tac (claset() addSDs [dfa_iff_welltyping] addSIs [is_dfa_fix_next]) 1); |
|
336 qed "fix_next_iff_welltyping"; |