equal
deleted
inserted
replaced
210 "\<turnstile> v : ALT r1 r2" |
210 "\<turnstile> v : ALT r1 r2" |
211 "\<turnstile> v : ONE" |
211 "\<turnstile> v : ONE" |
212 "\<turnstile> v : CHAR c" |
212 "\<turnstile> v : CHAR c" |
213 (* "\<turnstile> vs : STAR r"*) |
213 (* "\<turnstile> vs : STAR r"*) |
214 |
214 |
215 |
|
216 |
|
217 lemma Prf_flat_L: |
215 lemma Prf_flat_L: |
218 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
216 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
219 using assms |
217 using assms |
220 apply(induct v r rule: Prf.induct) |
218 apply(induct v r rule: Prf.induct) |
221 apply(auto simp add: Sequ_def) |
219 apply(auto simp add: Sequ_def) |
248 using assms |
246 using assms |
249 apply(induct ss) |
247 apply(induct ss) |
250 apply(auto) |
248 apply(auto) |
251 apply (metis empty_iff list.set(1)) |
249 apply (metis empty_iff list.set(1)) |
252 by (metis concat.simps(2) list.simps(9) set_ConsD) |
250 by (metis concat.simps(2) list.simps(9) set_ConsD) |
253 |
|
254 |
251 |
255 lemma L_flat_Prf: |
252 lemma L_flat_Prf: |
256 "L(r) = {flat v | v. \<turnstile> v : r}" |
253 "L(r) = {flat v | v. \<turnstile> v : r}" |
257 apply(induct r) |
254 apply(induct r) |
258 apply(auto dest: Prf_flat_L simp add: Sequ_def) |
255 apply(auto dest: Prf_flat_L simp add: Sequ_def) |
340 lemma Prf_injval_flat: |
337 lemma Prf_injval_flat: |
341 assumes "\<turnstile> v : der c r" |
338 assumes "\<turnstile> v : der c r" |
342 shows "flat (injval r c v) = c # (flat v)" |
339 shows "flat (injval r c v) = c # (flat v)" |
343 using assms |
340 using assms |
344 apply(induct arbitrary: v rule: der.induct) |
341 apply(induct arbitrary: v rule: der.induct) |
345 apply(simp) |
342 apply(auto elim!: Prf_elims split: if_splits) |
346 apply(erule Prf.cases) |
343 apply(metis mkeps_flat) |
347 apply(simp_all)[7] |
|
348 apply(simp) |
|
349 apply(erule Prf.cases) |
|
350 apply(simp_all)[7] |
|
351 apply(simp) |
|
352 apply(case_tac "c = d") |
|
353 apply(simp) |
|
354 apply(auto)[1] |
|
355 apply(erule Prf.cases) |
|
356 apply(simp_all)[7] |
|
357 apply(simp) |
|
358 apply(erule Prf.cases) |
|
359 apply(simp_all)[7] |
|
360 apply(simp) |
|
361 apply(erule Prf.cases) |
|
362 apply(simp_all)[7] |
|
363 apply(simp) |
|
364 apply(case_tac "nullable r1") |
|
365 apply(simp) |
|
366 apply(erule Prf.cases) |
|
367 apply(simp_all (no_asm_use))[7] |
|
368 apply(auto)[1] |
|
369 apply(erule Prf.cases) |
|
370 apply(simp_all)[7] |
|
371 apply(clarify) |
|
372 apply(simp only: injval.simps flat.simps) |
|
373 apply(auto)[1] |
|
374 apply (metis mkeps_flat) |
|
375 apply(simp) |
|
376 apply(erule Prf.cases) |
|
377 apply(simp_all)[7] |
|
378 apply(simp) |
|
379 apply(erule Prf.cases) |
|
380 apply(simp_all)[7] |
|
381 apply(auto) |
|
382 apply(rotate_tac 2) |
344 apply(rotate_tac 2) |
383 apply(erule Prf.cases) |
345 apply(erule Prf.cases) |
384 apply(simp_all)[7] |
346 apply(simp_all)[7] |
385 done |
347 done |
386 |
348 |
431 shows "[] \<in> r \<rightarrow> mkeps r" |
393 shows "[] \<in> r \<rightarrow> mkeps r" |
432 using assms |
394 using assms |
433 apply(induct r) |
395 apply(induct r) |
434 apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def) |
396 apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def) |
435 apply(subst append.simps(1)[symmetric]) |
397 apply(subst append.simps(1)[symmetric]) |
436 apply (rule PMatch.intros) |
398 apply(rule PMatch.intros) |
437 apply(auto) |
399 apply(auto) |
438 done |
400 done |
439 |
401 |
440 |
402 |
441 lemma PMatch_determ: |
403 lemma PMatch_determ: |