106 apply(simp add: image_UN) |
106 apply(simp add: image_UN) |
107 apply(subst star5[OF assms]) |
107 apply(subst star5[OF assms]) |
108 apply(simp) |
108 apply(simp) |
109 done |
109 done |
110 |
110 |
111 |
|
112 lemma star_decomp: |
111 lemma star_decomp: |
113 assumes a: "c # x \<in> A\<star>" |
112 assumes a: "c # x \<in> A\<star>" |
114 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
113 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
115 using a |
114 using a |
116 by (induct x\<equiv>"c # x" rule: Star.induct) |
115 by (induct x\<equiv>"c # x" rule: Star.induct) |
117 (auto simp add: append_eq_Cons_conv) |
116 (auto simp add: append_eq_Cons_conv) |
|
117 |
|
118 (* |
|
119 lemma star_induct[consumes 1, case_names Nil append, induct set: Star]: |
|
120 assumes "w \<in> A\<star>" |
|
121 and "P []" |
|
122 and step: "\<And>u v. u \<in> A \<Longrightarrow> v \<in> A\<star> \<Longrightarrow> P v \<Longrightarrow> P (u @ v)" |
|
123 shows "P w" |
|
124 proof - |
|
125 { fix n have "w \<in> A \<up> n \<Longrightarrow> P w" |
|
126 apply(induct n arbitrary: w) |
|
127 apply(auto intro: `P []` step star2 simp add: Sequ_def) |
|
128 done |
|
129 } |
|
130 with `w \<in> A\<star>` show "P w" by (auto simp: star3) |
|
131 qed |
|
132 *) |
118 |
133 |
119 section {* Regular Expressions *} |
134 section {* Regular Expressions *} |
120 |
135 |
121 datatype rexp = |
136 datatype rexp = |
122 NULL |
137 NULL |
203 using assms |
224 using assms |
204 apply(induct v r rule: Prf.induct) |
225 apply(induct v r rule: Prf.induct) |
205 apply(auto simp add: Sequ_def) |
226 apply(auto simp add: Sequ_def) |
206 done |
227 done |
207 |
228 |
208 |
229 lemma Prf_Star: |
209 lemma Prf_Star_flat_L: |
230 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
210 assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>" |
231 shows "\<turnstile> Star vs : STAR r" |
211 using assms |
232 using assms |
212 apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct) |
233 apply(induct vs) |
213 apply(auto) |
234 apply (metis Prf.intros(6)) |
214 apply(simp add: star3) |
235 by (metis Prf.intros(7) insert_iff set_simps(2)) |
215 apply(auto) |
236 |
216 apply(rule_tac x="Suc x" in exI) |
237 lemma Star_string: |
217 apply(auto simp add: Sequ_def) |
238 assumes "s \<in> A\<star>" |
218 apply(rule_tac x="flat v" in exI) |
239 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
219 apply(rule_tac x="flat (Star vs)" in exI) |
240 using assms |
220 apply(auto) |
241 apply(induct rule: Star.induct) |
221 by (metis Prf_flat_L) |
242 apply(auto) |
|
243 apply(rule_tac x="[]" in exI) |
|
244 apply(simp) |
|
245 apply(rule_tac x="s1#ss" in exI) |
|
246 apply(simp) |
|
247 done |
|
248 |
|
249 lemma Star_val: |
|
250 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
|
251 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
|
252 using assms |
|
253 apply(induct ss) |
|
254 apply(auto) |
|
255 apply (metis empty_iff list.set(1)) |
|
256 by (metis concat.simps(2) list.simps(9) set_ConsD) |
222 |
257 |
223 lemma L_flat_Prf: |
258 lemma L_flat_Prf: |
224 "L(r) = {flat v | v. \<turnstile> v : r}" |
259 "L(r) = {flat v | v. \<turnstile> v : r}" |
225 apply(induct r) |
260 apply(induct r) |
226 apply(auto dest: Prf_flat_L simp add: Sequ_def) |
261 apply(auto dest: Prf_flat_L simp add: Sequ_def) |
229 apply (metis Prf.intros(1) flat.simps(5)) |
264 apply (metis Prf.intros(1) flat.simps(5)) |
230 apply (metis Prf.intros(2) flat.simps(3)) |
265 apply (metis Prf.intros(2) flat.simps(3)) |
231 apply (metis Prf.intros(3) flat.simps(4)) |
266 apply (metis Prf.intros(3) flat.simps(4)) |
232 apply(erule Prf.cases) |
267 apply(erule Prf.cases) |
233 apply(auto) |
268 apply(auto) |
234 apply(simp add: star3) |
269 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)") |
235 apply(auto) |
270 apply(auto)[1] |
236 sorry |
271 apply(rule_tac x="Star vs" in exI) |
237 |
272 apply(simp) |
238 section {* Greedy Ordering according to Frisch/Cardelli *} |
273 apply(rule Prf_Star) |
239 |
274 apply(simp) |
240 inductive |
275 apply(drule Star_string) |
241 GrOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ gr\<succ> _") |
276 apply(auto) |
242 where |
277 apply(rule Star_val) |
243 "v1 gr\<succ> v1' \<Longrightarrow> (Seq v1 v2) gr\<succ> (Seq v1' v2')" |
278 apply(simp) |
244 | "v2 gr\<succ> v2' \<Longrightarrow> (Seq v1 v2) gr\<succ> (Seq v1 v2')" |
279 done |
245 | "v1 gr\<succ> v2 \<Longrightarrow> (Left v1) gr\<succ> (Left v2)" |
|
246 | "v1 gr\<succ> v2 \<Longrightarrow> (Right v1) gr\<succ> (Right v2)" |
|
247 | "(Left v2) gr\<succ>(Right v1)" |
|
248 | "(Char c) gr\<succ> (Char c)" |
|
249 | "(Void) gr\<succ> (Void)" |
|
250 |
|
251 lemma Gr_refl: |
|
252 assumes "\<turnstile> v : r" |
|
253 shows "v gr\<succ> v" |
|
254 using assms |
|
255 apply(induct) |
|
256 apply(auto intro: GrOrd.intros) |
|
257 done |
|
258 |
|
259 lemma Gr_total: |
|
260 assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" |
|
261 shows "v1 gr\<succ> v2 \<or> v2 gr\<succ> v1" |
|
262 using assms |
|
263 apply(induct v1 r arbitrary: v2 rule: Prf.induct) |
|
264 apply(rotate_tac 4) |
|
265 apply(erule Prf.cases) |
|
266 apply(simp_all)[5] |
|
267 apply(clarify) |
|
268 apply (metis GrOrd.intros(1) GrOrd.intros(2)) |
|
269 apply(rotate_tac 2) |
|
270 apply(erule Prf.cases) |
|
271 apply(simp_all) |
|
272 apply(clarify) |
|
273 apply (metis GrOrd.intros(3)) |
|
274 apply(clarify) |
|
275 apply (metis GrOrd.intros(5)) |
|
276 apply(rotate_tac 2) |
|
277 apply(erule Prf.cases) |
|
278 apply(simp_all) |
|
279 apply(clarify) |
|
280 apply (metis GrOrd.intros(5)) |
|
281 apply(clarify) |
|
282 apply (metis GrOrd.intros(4)) |
|
283 apply(erule Prf.cases) |
|
284 apply(simp_all) |
|
285 apply (metis GrOrd.intros(7)) |
|
286 apply(erule Prf.cases) |
|
287 apply(simp_all) |
|
288 apply (metis GrOrd.intros(6)) |
|
289 done |
|
290 |
|
291 lemma Gr_trans: |
|
292 assumes "v1 gr\<succ> v2" "v2 gr\<succ> v3" |
|
293 and "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r" |
|
294 shows "v1 gr\<succ> v3" |
|
295 using assms |
|
296 apply(induct r arbitrary: v1 v2 v3) |
|
297 apply(erule Prf.cases) |
|
298 apply(simp_all)[5] |
|
299 apply(erule Prf.cases) |
|
300 apply(simp_all)[5] |
|
301 apply(erule Prf.cases) |
|
302 apply(simp_all)[5] |
|
303 apply(erule Prf.cases) |
|
304 apply(simp_all)[5] |
|
305 apply(erule Prf.cases) |
|
306 apply(simp_all)[5] |
|
307 defer |
|
308 (* ALT case *) |
|
309 apply(erule Prf.cases) |
|
310 apply(simp_all (no_asm_use))[5] |
|
311 apply(erule Prf.cases) |
|
312 apply(simp_all (no_asm_use))[5] |
|
313 apply(erule Prf.cases) |
|
314 apply(simp_all (no_asm_use))[5] |
|
315 apply(clarify) |
|
316 apply(erule GrOrd.cases) |
|
317 apply(simp_all (no_asm_use))[7] |
|
318 apply(erule GrOrd.cases) |
|
319 apply(simp_all (no_asm_use))[7] |
|
320 apply (metis GrOrd.intros(3)) |
|
321 apply(clarify) |
|
322 apply(erule GrOrd.cases) |
|
323 apply(simp_all (no_asm_use))[7] |
|
324 apply(erule GrOrd.cases) |
|
325 apply(simp_all (no_asm_use))[7] |
|
326 apply (metis GrOrd.intros(5)) |
|
327 apply(erule Prf.cases) |
|
328 apply(simp_all (no_asm_use))[5] |
|
329 apply(clarify) |
|
330 apply(erule GrOrd.cases) |
|
331 apply(simp_all (no_asm_use))[7] |
|
332 apply(erule GrOrd.cases) |
|
333 apply(simp_all (no_asm_use))[7] |
|
334 apply (metis GrOrd.intros(5)) |
|
335 apply(erule Prf.cases) |
|
336 apply(simp_all (no_asm_use))[5] |
|
337 apply(erule Prf.cases) |
|
338 apply(simp_all (no_asm_use))[5] |
|
339 apply(clarify) |
|
340 apply(erule GrOrd.cases) |
|
341 apply(simp_all (no_asm_use))[7] |
|
342 apply(clarify) |
|
343 apply(erule GrOrd.cases) |
|
344 apply(simp_all (no_asm_use))[7] |
|
345 apply(erule Prf.cases) |
|
346 apply(simp_all (no_asm_use))[5] |
|
347 apply(clarify) |
|
348 apply(erule GrOrd.cases) |
|
349 apply(simp_all (no_asm_use))[7] |
|
350 apply(erule GrOrd.cases) |
|
351 apply(simp_all (no_asm_use))[7] |
|
352 apply(clarify) |
|
353 apply(erule GrOrd.cases) |
|
354 apply(simp_all (no_asm_use))[7] |
|
355 apply(erule GrOrd.cases) |
|
356 apply(simp_all (no_asm_use))[7] |
|
357 apply (metis GrOrd.intros(4)) |
|
358 (* SEQ case *) |
|
359 apply(erule Prf.cases) |
|
360 apply(simp_all (no_asm_use))[5] |
|
361 apply(erule Prf.cases) |
|
362 apply(simp_all (no_asm_use))[5] |
|
363 apply(erule Prf.cases) |
|
364 apply(simp_all (no_asm_use))[5] |
|
365 apply(clarify) |
|
366 apply(erule GrOrd.cases) |
|
367 apply(simp_all (no_asm_use))[7] |
|
368 apply(erule GrOrd.cases) |
|
369 apply(simp_all (no_asm_use))[7] |
|
370 apply(clarify) |
|
371 apply (metis GrOrd.intros(1)) |
|
372 apply (metis GrOrd.intros(1)) |
|
373 apply(erule GrOrd.cases) |
|
374 apply(simp_all (no_asm_use))[7] |
|
375 apply (metis GrOrd.intros(1)) |
|
376 by (metis GrOrd.intros(1) Gr_refl) |
|
377 |
280 |
378 |
281 |
379 section {* Values Sets *} |
282 section {* Values Sets *} |
380 |
283 |
381 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100) |
284 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100) |
456 "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}" |
359 "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}" |
457 unfolding Values_def |
360 unfolding Values_def |
458 apply(auto) |
361 apply(auto) |
459 (*NULL*) |
362 (*NULL*) |
460 apply(erule Prf.cases) |
363 apply(erule Prf.cases) |
461 apply(simp_all)[5] |
364 apply(simp_all)[7] |
462 (*EMPTY*) |
365 (*EMPTY*) |
463 apply(erule Prf.cases) |
366 apply(erule Prf.cases) |
464 apply(simp_all)[5] |
367 apply(simp_all)[7] |
465 apply(rule Prf.intros) |
368 apply(rule Prf.intros) |
466 apply (metis append_Nil prefix_def) |
369 apply (metis append_Nil prefix_def) |
467 (*CHAR*) |
370 (*CHAR*) |
468 apply(erule Prf.cases) |
371 apply(erule Prf.cases) |
469 apply(simp_all)[5] |
372 apply(simp_all)[7] |
470 apply(rule Prf.intros) |
373 apply(rule Prf.intros) |
471 apply(erule Prf.cases) |
374 apply(erule Prf.cases) |
472 apply(simp_all)[5] |
375 apply(simp_all)[7] |
473 (*ALT*) |
376 (*ALT*) |
474 apply(erule Prf.cases) |
377 apply(erule Prf.cases) |
475 apply(simp_all)[5] |
378 apply(simp_all)[7] |
476 apply (metis Prf.intros(2)) |
379 apply (metis Prf.intros(2)) |
477 apply (metis Prf.intros(3)) |
380 apply (metis Prf.intros(3)) |
478 (*SEQ*) |
381 (*SEQ*) |
479 apply(erule Prf.cases) |
382 apply(erule Prf.cases) |
480 apply(simp_all)[5] |
383 apply(simp_all)[7] |
481 apply (simp add: append_eq_conv_conj prefix_def rest_def) |
384 apply (simp add: append_eq_conv_conj prefix_def rest_def) |
482 apply (metis Prf.intros(1)) |
385 apply (metis Prf.intros(1)) |
483 apply (simp add: append_eq_conv_conj prefix_def rest_def) |
386 apply (simp add: append_eq_conv_conj prefix_def rest_def) |
484 done |
387 done |
485 |
388 |
|
389 (* This lemma needs to be adapted to Star |
486 lemma Values_finite: |
390 lemma Values_finite: |
487 "finite (Values r s)" |
391 "finite (Values r s)" |
488 apply(induct r arbitrary: s) |
392 apply(induct r arbitrary: s) |
489 apply(simp_all add: Values_recs) |
393 apply(simp_all add: Values_recs) |
490 thm finite_surj |
394 thm finite_surj |