30 fun simp_ALT where |
30 fun simp_ALT where |
31 "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" |
31 "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" |
32 | "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" |
32 | "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" |
33 | "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)" |
33 | "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)" |
34 |
34 |
35 (* where is ZERO *) |
35 |
36 fun simp_SEQ where |
36 fun simp_SEQ where |
37 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
37 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
38 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
38 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
|
39 | "simp_SEQ (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ZERO, undefined)" |
|
40 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (ZERO, undefined)" |
39 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
41 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
40 |
42 |
41 lemma simp_SEQ_simps[simp]: |
43 lemma simp_SEQ_simps[simp]: |
42 "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2)) |
44 "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2)) |
43 else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2)) |
45 else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2)) |
44 else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))" |
46 else (if (fst p1 = ZERO) then (ZERO, undefined) |
|
47 else (if (fst p2 = ZERO) then (ZERO, undefined) |
|
48 else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))))" |
45 by (induct p1 p2 rule: simp_SEQ.induct) (auto) |
49 by (induct p1 p2 rule: simp_SEQ.induct) (auto) |
46 |
50 |
47 lemma simp_ALT_simps[simp]: |
51 lemma simp_ALT_simps[simp]: |
48 "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2)) |
52 "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2)) |
49 else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1)) |
53 else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1)) |
139 have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact |
143 have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact |
140 have as: "s \<in> fst (simp (SEQ r1 r2)) \<rightarrow> v" by fact |
144 have as: "s \<in> fst (simp (SEQ r1 r2)) \<rightarrow> v" by fact |
141 consider (ONE_ONE) "fst (simp r1) = ONE" "fst (simp r2) = ONE" |
145 consider (ONE_ONE) "fst (simp r1) = ONE" "fst (simp r2) = ONE" |
142 | (ONE_NONE) "fst (simp r1) = ONE" "fst (simp r2) \<noteq> ONE" |
146 | (ONE_NONE) "fst (simp r1) = ONE" "fst (simp r2) \<noteq> ONE" |
143 | (NONE_ONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) = ONE" |
147 | (NONE_ONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) = ONE" |
144 | (NONE_NONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) \<noteq> ONE" by auto |
148 | (NONE_NONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) \<noteq> ONE" |
|
149 by auto |
145 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" |
150 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" |
146 proof(cases) |
151 proof(cases) |
147 case (ONE_ONE) |
152 case (ONE_ONE) |
148 with as have b: "s \<in> ONE \<rightarrow> v" by simp |
153 with as have b: "s \<in> ONE \<rightarrow> v" by simp |
149 from b have "s \<in> r1 \<rightarrow> snd (simp r1) v" using IH1 ONE_ONE by simp |
154 from b have "s \<in> r1 \<rightarrow> snd (simp r1) v" using IH1 ONE_ONE by simp |
181 ultimately have "(s @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) v) (snd (simp r2) Void)" |
186 ultimately have "(s @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) v) (snd (simp r2) Void)" |
182 by(rule_tac Posix_SEQ) auto |
187 by(rule_tac Posix_SEQ) auto |
183 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using NONE_ONE by simp |
188 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using NONE_ONE by simp |
184 next |
189 next |
185 case (NONE_NONE) |
190 case (NONE_NONE) |
186 with as have "s \<in> SEQ (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp |
191 from as have 00: "fst (simp r1) \<noteq> ZERO" "fst (simp r2) \<noteq> ZERO" |
|
192 apply(auto) |
|
193 apply(smt Posix_elims(1) fst_conv) |
|
194 by (smt NONE_NONE(2) Posix_elims(1) fstI) |
|
195 with NONE_NONE as have "s \<in> SEQ (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp |
187 then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2" |
196 then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2" |
188 "s1 \<in> (fst (simp r1)) \<rightarrow> v1" "s2 \<in> (fst (simp r2)) \<rightarrow> v2" |
197 "s1 \<in> (fst (simp r1)) \<rightarrow> v1" "s2 \<in> (fst (simp r2)) \<rightarrow> v2" |
189 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" |
198 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" |
190 by (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric]) |
199 by (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric]) |
191 then have "s1 \<in> r1 \<rightarrow> (snd (simp r1) v1)" "s2 \<in> r2 \<rightarrow> (snd (simp r2) v2)" |
200 then have "s1 \<in> r1 \<rightarrow> (snd (simp r1) v1)" "s2 \<in> r2 \<rightarrow> (snd (simp r2) v2)" |
192 using IH1 IH2 by auto |
201 using IH1 IH2 by auto |
193 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using eqs NONE_NONE |
202 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using eqs NONE_NONE 00 |
194 by(auto intro: Posix_SEQ) |
203 by(auto intro: Posix_SEQ) |
195 qed |
204 qed |
196 qed (simp_all) |
205 qed (simp_all) |
197 |
206 |
198 |
207 |
228 ultimately show "slexer r (c # s) = lexer r (c # s)" |
237 ultimately show "slexer r (c # s) = lexer r (c # s)" |
229 by (simp del: slexer.simps add: slexer_better_simp) |
238 by (simp del: slexer.simps add: slexer_better_simp) |
230 qed |
239 qed |
231 qed |
240 qed |
232 |
241 |
233 (* |
|
234 fun simp2_ALT where |
|
235 "simp2_ALT ZERO r2 seen = (r2, seen)" |
|
236 | "simp2_ALT r1 ZERO seen = (r1, seen)" |
|
237 | "simp2_ALT r1 r2 seen = (ALT r1 r2, seen)" |
|
238 |
|
239 fun simp2_SEQ where |
|
240 "simp2_SEQ ZERO r2 seen = (ZERO, seen)" |
|
241 | "simp2_SEQ r1 ZERO seen = (ZERO, seen)" |
|
242 | "simp2_SEQ ONE r2 seen = (r2, seen \<union> {r2})" |
|
243 | "simp2_SEQ r1 ONE seen = (r1, seen \<union> {r1})" |
|
244 | "simp2_SEQ r1 r2 seen = (SEQ r1 r2, seen \<union> {SEQ r1 r2})" |
|
245 |
|
246 |
|
247 |
|
248 |
|
249 fun |
|
250 simp2 :: "rexp \<Rightarrow> rexp set \<Rightarrow> rexp * rexp set" |
|
251 where |
|
252 "simp2 (ALT r1 r2) seen = |
|
253 (let (r1s, seen1) = simp2 r1 seen in |
|
254 let (r2s, seen2) = simp2 r2 seen1 |
|
255 in simp2_ALT r1s r2s seen2)" |
|
256 | "simp2 (SEQ r1 r2) seen = |
|
257 (let (r1s, _) = simp2 r1 {} in |
|
258 let (r2s, _) = simp2 r2 {} |
|
259 in if (SEQ r1s r2s \<in> seen) then (ZERO, seen) |
|
260 else simp2_SEQ r1s r2s seen)" |
|
261 | "simp2 r seen = (if r \<in> seen then (ZERO, seen) else (r, seen \<union> {r}))" |
|
262 |
|
263 |
|
264 lemma simp2_ALT[simp]: |
|
265 shows "L (fst (simp2_ALT r1 r2 seen)) = L r1 \<union> L r2" |
|
266 apply(induct r1 r2 seen rule: simp2_ALT.induct) |
|
267 apply(simp_all) |
|
268 done |
|
269 |
|
270 lemma test1: |
|
271 shows "snd (simp2_ALT r1 r2 rs) = rs" |
|
272 apply(induct r1 r2 rs rule: simp2_ALT.induct) |
|
273 apply(auto) |
|
274 done |
|
275 |
|
276 lemma test2: |
|
277 shows "rs \<subseteq> snd (simp2_SEQ r1 r2 rs)" |
|
278 apply(induct r1 r2 rs rule: simp2_SEQ.induct) |
|
279 apply(auto) |
|
280 done |
|
281 |
|
282 lemma test3: |
|
283 shows "rs \<subseteq> snd (simp2 r rs)" |
|
284 apply(induct r rs rule: simp2.induct) |
|
285 apply(auto split: prod.split) |
|
286 apply (metis set_mp test1) |
|
287 by (meson set_mp test2) |
|
288 |
|
289 lemma test3a: |
|
290 shows "\<Union>(L ` snd (simp2 r rs)) \<subseteq> L(r) \<union> (\<Union> (L ` rs))" |
|
291 apply(induct r rs rule: simp2.induct) |
|
292 apply(auto split: prod.split simp add: Sequ_def) |
|
293 apply (smt UN_iff Un_iff set_mp test1) |
|
294 |
|
295 |
|
296 lemma test: |
|
297 assumes "(\<Union>r' \<in> rs. L r') \<subseteq> L r" |
|
298 shows "L(fst (simp2 r rs)) \<subseteq> L(r)" |
|
299 using assms |
|
300 apply(induct r arbitrary: rs) |
|
301 apply(simp only: simp2.simps) |
|
302 apply(simp) |
|
303 apply(simp only: simp2.simps) |
|
304 apply(simp) |
|
305 apply(simp only: simp2.simps) |
|
306 apply(simp) |
|
307 prefer 3 |
|
308 apply(simp only: simp2.simps) |
|
309 apply(simp) |
|
310 prefer 2 |
|
311 apply(simp only: simp2.simps) |
|
312 apply(simp) |
|
313 apply(subst prod.split) |
|
314 apply(rule allI)+ |
|
315 apply(rule impI) |
|
316 apply(subst prod.split) |
|
317 apply(rule allI)+ |
|
318 apply(rule impI) |
|
319 apply(simp) |
|
320 apply(drule_tac x="rs" in meta_spec) |
|
321 apply(simp) |
|
322 apply(drule_tac x="x2" in meta_spec) |
|
323 apply(simp) |
|
324 apply(auto)[1] |
|
325 apply(subgoal_tac "rs \<subseteq> x2a") |
|
326 prefer 2 |
|
327 apply (metis order_trans prod.sel(2) test3) |
|
328 |
|
329 |
|
330 apply(rule antisym) |
|
331 prefer 2 |
|
332 apply(simp) |
|
333 apply(rule conjI) |
|
334 apply(drule meta_mp) |
|
335 prefer 2 |
|
336 apply(simp) |
|
337 apply(auto)[1] |
|
338 apply(auto)[1] |
|
339 |
|
340 thm prod.split |
|
341 apply(auto split: prod.split)[1] |
|
342 apply(drule_tac x="rs" in meta_spec) |
|
343 apply(drule_tac x="rs" in meta_spec) |
|
344 apply(simp) |
|
345 apply(rule_tac x="SEQ x1 x1a" in bexI) |
|
346 apply(simp add: Sequ_def) |
|
347 |
|
348 apply(auto)[1] |
|
349 apply(simp) |
|
350 apply(subgoal_tac "L (fst (simp2_SEQ x1 x1a rs)) \<subseteq> L x1 \<union> L x1a") |
|
351 apply(frule_tac x="{}" in meta_spec) |
|
352 apply(rotate_tac 1) |
|
353 apply(frule_tac x="{}" in meta_spec) |
|
354 apply(simp) |
|
355 |
|
356 |
|
357 apply(rule_tac x="SEQ x1 x1a" in bexI) |
|
358 apply(simp add: Sequ_def) |
|
359 apply(auto)[1] |
|
360 apply(simp) |
|
361 using L.simps(2) apply blast |
|
362 prefer 3 |
|
363 apply(simp only: simp2.simps) |
|
364 apply(simp) |
|
365 using L.simps(3) apply blast |
|
366 prefer 2 |
|
367 apply(simp add: Sequ_def) |
|
368 apply(auto)[1] |
|
369 oops |
|
370 *) |
|
371 end |
242 end |