133 |
133 |
134 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
134 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
135 where |
135 where |
136 "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')" |
136 "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')" |
137 |
137 |
|
138 definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
|
139 where |
|
140 "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')" |
|
141 |
138 |
142 |
139 (* |
143 (* |
140 lemma POSIX_SEQ: |
144 lemma POSIX_SEQ: |
141 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
145 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
142 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
146 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
208 apply(auto) |
211 apply(auto) |
209 apply(erule ValOrd.cases) |
212 apply(erule ValOrd.cases) |
210 apply(simp_all) |
213 apply(simp_all) |
211 done |
214 done |
212 |
215 |
|
216 lemma POSIX2_ALT: |
|
217 assumes "POSIX2 (Left v1) (ALT r1 r2)" |
|
218 shows "POSIX2 v1 r1" |
|
219 using assms |
|
220 apply(simp add: POSIX2_def) |
|
221 apply(auto) |
|
222 apply(erule Prf.cases) |
|
223 apply(simp_all)[5] |
|
224 apply(drule_tac x="Left v'" in spec) |
|
225 apply(drule mp) |
|
226 apply(rule Prf.intros) |
|
227 apply(auto) |
|
228 apply(erule ValOrd.cases) |
|
229 apply(simp_all) |
|
230 done |
|
231 |
|
232 |
213 lemma POSIX_ALT1a: |
233 lemma POSIX_ALT1a: |
214 assumes "POSIX (Right v2) (ALT r1 r2)" |
234 assumes "POSIX (Right v2) (ALT r1 r2)" |
215 shows "POSIX v2 r2" |
235 shows "POSIX v2 r2" |
216 using assms |
236 using assms |
217 unfolding POSIX_def |
237 unfolding POSIX_def |
223 apply(auto) |
243 apply(auto) |
224 apply(erule ValOrd.cases) |
244 apply(erule ValOrd.cases) |
225 apply(simp_all) |
245 apply(simp_all) |
226 done |
246 done |
227 |
247 |
|
248 lemma POSIX2_ALT1a: |
|
249 assumes "POSIX2 (Right v2) (ALT r1 r2)" |
|
250 shows "POSIX2 v2 r2" |
|
251 using assms |
|
252 unfolding POSIX2_def |
|
253 apply(auto) |
|
254 apply(erule Prf.cases) |
|
255 apply(simp_all)[5] |
|
256 apply(drule_tac x="Right v'" in spec) |
|
257 apply(drule mp) |
|
258 apply(rule Prf.intros) |
|
259 apply(auto) |
|
260 apply(erule ValOrd.cases) |
|
261 apply(simp_all) |
|
262 done |
|
263 |
228 |
264 |
229 lemma POSIX_ALT1b: |
265 lemma POSIX_ALT1b: |
230 assumes "POSIX (Right v2) (ALT r1 r2)" |
266 assumes "POSIX (Right v2) (ALT r1 r2)" |
231 shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')" |
267 shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')" |
232 using assms |
268 using assms |
247 apply(auto) |
283 apply(auto) |
248 apply(rule ValOrd.intros) |
284 apply(rule ValOrd.intros) |
249 apply(auto) |
285 apply(auto) |
250 apply(rule ValOrd.intros) |
286 apply(rule ValOrd.intros) |
251 by simp |
287 by simp |
|
288 |
|
289 lemma POSIX2_ALT_I1: |
|
290 assumes "POSIX2 v1 r1" |
|
291 shows "POSIX2 (Left v1) (ALT r1 r2)" |
|
292 using assms |
|
293 unfolding POSIX2_def |
|
294 apply(auto) |
|
295 apply(rule Prf.intros) |
|
296 apply(simp) |
|
297 apply(rotate_tac 2) |
|
298 apply(erule Prf.cases) |
|
299 apply(simp_all)[5] |
|
300 apply(auto) |
|
301 apply(rule ValOrd.intros) |
|
302 apply(auto) |
|
303 apply(rule ValOrd.intros) |
|
304 oops |
252 |
305 |
253 lemma POSIX_ALT_I2: |
306 lemma POSIX_ALT_I2: |
254 assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')" |
307 assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')" |
255 shows "POSIX (Right v2) (ALT r1 r2)" |
308 shows "POSIX (Right v2) (ALT r1 r2)" |
256 using assms |
309 using assms |
364 apply(erule Prf.cases) |
418 apply(erule Prf.cases) |
365 apply(simp_all)[5] |
419 apply(simp_all)[5] |
366 apply(auto) |
420 apply(auto) |
367 apply (metis Prf_flat_L mkeps_flat nullable_correctness) |
421 apply (metis Prf_flat_L mkeps_flat nullable_correctness) |
368 by (simp add: ValOrd.intros(5)) |
422 by (simp add: ValOrd.intros(5)) |
|
423 |
|
424 |
|
425 lemma mkeps_POSIX2: |
|
426 assumes "nullable r" |
|
427 shows "POSIX2 (mkeps r) r" |
|
428 using assms |
|
429 apply(induct r) |
|
430 apply(simp) |
|
431 apply(simp) |
|
432 apply(simp add: POSIX2_def) |
|
433 apply(rule conjI) |
|
434 apply(rule Prf.intros) |
|
435 apply(auto)[1] |
|
436 apply(erule Prf.cases) |
|
437 apply(simp_all)[5] |
|
438 apply(rule ValOrd.intros) |
|
439 apply(simp) |
|
440 apply(simp) |
|
441 apply(simp add: POSIX2_def) |
|
442 apply(rule conjI) |
|
443 apply(rule Prf.intros) |
|
444 apply(simp add: mkeps_nullable) |
|
445 apply(simp add: mkeps_nullable) |
|
446 apply(auto)[1] |
|
447 apply(rotate_tac 6) |
|
448 apply(erule Prf.cases) |
|
449 apply(simp_all)[5] |
|
450 apply(rule ValOrd.intros(2)) |
|
451 apply(simp) |
|
452 apply(simp only: nullable.simps) |
|
453 apply(erule disjE) |
|
454 apply(simp) |
|
455 thm POSIX2_ALT1a |
|
456 apply(rule POSIX2_ALT) |
|
457 apply(simp add: POSIX2_def) |
|
458 apply(rule conjI) |
|
459 apply(rule Prf.intros) |
|
460 apply(simp add: mkeps_nullable) |
|
461 oops |
369 |
462 |
370 |
463 |
371 section {* Derivatives *} |
464 section {* Derivatives *} |
372 |
465 |
373 fun |
466 fun |
559 defer |
652 defer |
560 apply(auto) |
653 apply(auto) |
561 apply (metis POSIX_ALT_I1) |
654 apply (metis POSIX_ALT_I1) |
562 (* maybe it is too early to instantiate this existential quantifier *) |
655 (* maybe it is too early to instantiate this existential quantifier *) |
563 (* potentially this is the wrong POSIX value *) |
656 (* potentially this is the wrong POSIX value *) |
564 apply(rule_tac x = "Seq v va" in exI ) |
657 apply(case_tac "r1 = NULL") |
|
658 apply(simp add: POSIX_def) |
|
659 apply(auto)[1] |
|
660 apply (metis L.simps(1) L.simps(4) Prf_flat_L mkeps_flat nullable.simps(1) nullable.simps(2) nullable_correctness seq_null(2)) |
|
661 apply(case_tac "r1 = EMPTY") |
|
662 apply(rule_tac x = "Seq Void va" in exI ) |
565 apply(simp (no_asm) add: POSIX_def) |
663 apply(simp (no_asm) add: POSIX_def) |
566 apply(auto) |
664 apply(auto) |
567 apply(erule Prf.cases) |
665 apply(erule Prf.cases) |
568 apply(simp_all) |
666 apply(simp_all) |
|
667 apply(auto)[1] |
|
668 apply(erule Prf.cases) |
|
669 apply(simp_all) |
|
670 apply(rule ValOrd.intros(2)) |
|
671 apply(rule ValOrd.intros) |
|
672 apply(case_tac "\<exists>c. r1 = CHAR c") |
|
673 apply(auto) |
|
674 apply(rule_tac x = "Seq (Char c) va" in exI ) |
|
675 apply(simp (no_asm) add: POSIX_def) |
|
676 apply(auto) |
|
677 apply(erule Prf.cases) |
|
678 apply(simp_all) |
|
679 apply(auto)[1] |
|
680 apply(erule Prf.cases) |
|
681 apply(simp_all) |
|
682 apply(auto)[1] |
|
683 apply(rule ValOrd.intros(2)) |
|
684 apply(rule ValOrd.intros) |
|
685 apply(case_tac "\<exists>r1a r1b. r1 = ALT r1a r1b") |
|
686 apply(auto) |
|
687 apply(rule_tac x = "Seq () va" in exI ) |
|
688 apply(simp (no_asm) add: POSIX_def) |
|
689 apply(auto) |
|
690 apply(erule Prf.cases) |
|
691 apply(simp_all) |
|
692 apply(auto)[1] |
|
693 apply(erule Prf.cases) |
|
694 apply(simp_all) |
|
695 apply(auto)[1] |
|
696 apply(rule ValOrd.intros(2)) |
|
697 apply(rule ValOrd.intros) |
|
698 |
569 apply(case_tac "v \<succ>r1a v1") |
699 apply(case_tac "v \<succ>r1a v1") |
570 apply (metis ValOrd.intros(2)) |
700 apply (metis ValOrd.intros(2)) |
571 apply(simp add: POSIX_def) |
701 apply(simp add: POSIX_def) |
572 apply(case_tac "flat v = flat v1") |
702 apply(case_tac "flat v = flat v1") |
573 apply(auto)[1] |
703 apply(auto)[1] |