432 apply(simp_all)[8] |
432 apply(simp_all)[8] |
433 apply(erule ValOrd.cases) |
433 apply(erule ValOrd.cases) |
434 apply(simp_all)[8] |
434 apply(simp_all)[8] |
435 done |
435 done |
436 |
436 |
437 lemma ValOrd_max: |
437 lemma |
438 shows "\<exists>v. \<forall>v'. (v' \<succ>r v \<longrightarrow> v = v')" |
438 "s \<in> L r \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r \<and> flat v = s}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v = s}. vmax 2\<succ> v)" |
439 apply(induct r) |
439 apply(induct s arbitrary: r rule: length_induct) |
440 apply(auto) |
440 apply(induct_tac r rule: rexp.induct) |
441 apply(rule exI) |
|
442 apply(rule allI) |
|
443 apply(rule impI) |
441 apply(rule impI) |
444 apply(erule ValOrd.cases) |
442 apply(simp) |
445 apply(simp_all)[8] |
443 apply(simp) |
446 apply(rule exI) |
|
447 apply(rule allI) |
|
448 apply(rule impI) |
444 apply(rule impI) |
449 apply(erule ValOrd.cases) |
445 apply(simp) |
450 apply(simp_all)[8] |
446 apply(rule_tac x="Void" in exI) |
451 apply(rule exI) |
447 apply(simp) |
452 apply(rule allI) |
|
453 apply(rule impI) |
|
454 apply(erule ValOrd.cases) |
|
455 apply(simp_all)[8] |
|
456 apply(rule exI) |
|
457 apply(rule allI) |
|
458 apply(rule impI) |
|
459 apply(erule ValOrd.cases) |
|
460 apply(simp_all)[8] |
|
461 apply(rule exI) |
|
462 apply(rule allI) |
|
463 apply(rule impI) |
|
464 apply(erule ValOrd.cases) |
|
465 apply(simp_all)[8] |
|
466 done |
|
467 |
|
468 lemma ValOrd_max: |
|
469 assumes "L r \<noteq> {}" |
|
470 shows "\<exists>v. \<turnstile> v : r \<and> (\<forall>v'. ((\<turnstile> v' : r \<and> v' \<succ>r v) \<longrightarrow> v = v'))" |
|
471 using assms |
|
472 apply(induct r) |
|
473 apply(auto) |
|
474 apply(rule exI) |
|
475 apply(rule conjI) |
448 apply(rule conjI) |
476 apply(rule Prf.intros) |
449 apply (metis Prf.intros(4)) |
477 apply(rule allI) |
450 apply(rule allI) |
478 apply(rule impI) |
451 apply(rule impI) |
479 apply(erule conjE) |
452 apply(erule conjE) |
480 apply(erule ValOrd.cases) |
453 apply(erule Prf.cases) |
481 apply(simp_all)[8] |
454 apply(simp_all)[5] |
482 apply(rule exI) |
455 apply (metis ValOrd2.intros(7)) |
|
456 apply(simp) |
|
457 apply(rule impI) |
|
458 apply(rule_tac x="Char char" in exI) |
|
459 apply(simp) |
483 apply(rule conjI) |
460 apply(rule conjI) |
484 apply(rule Prf.intros) |
461 apply (metis Prf.intros) |
485 apply(rule allI) |
462 apply(rule allI) |
486 apply(rule impI) |
463 apply(rule impI) |
487 apply(erule conjE) |
464 apply(erule conjE) |
488 apply(erule ValOrd.cases) |
465 apply(erule Prf.cases) |
489 apply(simp_all)[8] |
466 apply(simp_all)[5] |
490 apply(auto simp add: Sequ_def)[1] |
467 apply (metis ValOrd2.intros(8)) |
|
468 apply(simp) |
|
469 apply(rule impI) |
|
470 apply(simp add: Sequ_def)[1] |
|
471 apply(erule exE)+ |
|
472 apply(erule conjE)+ |
|
473 apply(clarify) |
|
474 defer |
|
475 apply(simp) |
|
476 apply(rule conjI) |
|
477 apply(rule impI) |
|
478 apply(simp) |
|
479 apply(erule exE) |
|
480 apply(clarify) |
|
481 apply(rule_tac x="Left vmax" in exI) |
|
482 apply(rule conjI) |
|
483 apply (metis Prf.intros(2)) |
|
484 apply(simp) |
|
485 apply(rule allI) |
|
486 apply(rule impI) |
|
487 apply(erule conjE) |
|
488 apply(rotate_tac 5) |
|
489 apply(erule Prf.cases) |
|
490 apply(simp_all)[5] |
|
491 apply (metis ValOrd2.intros(6)) |
|
492 apply(clarify) |
|
493 apply (metis ValOrd2.intros(3) order_refl) |
|
494 apply(rule impI) |
|
495 apply(simp) |
|
496 apply(erule exE) |
|
497 apply(clarify) |
|
498 apply(rule_tac x="Right vmax" in exI) |
|
499 apply(simp) |
|
500 apply(rule conjI) |
|
501 apply (metis Prf.intros(3)) |
|
502 apply(rule allI) |
|
503 apply(rule impI) |
|
504 apply(erule conjE)+ |
|
505 apply(rotate_tac 5) |
|
506 apply(erule Prf.cases) |
|
507 apply(simp_all)[5] |
|
508 apply (metis ValOrd2.intros(8)) |
|
509 apply(simp) |
|
510 apply(rule impI) |
|
511 apply(simp add: Sequ_def)[1] |
|
512 apply(erule exE)+ |
|
513 apply(erule conjE)+ |
|
514 apply(clarify) |
|
515 |
|
516 |
|
517 inductive ValOrd3 :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ 3\<succ>_ _" [100, 100, 100] 100) |
|
518 where |
|
519 "\<lbrakk>v2 3\<succ>r2 v2'; \<turnstile> v1 : r1\<rbrakk> \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1 v2')" |
|
520 | "\<lbrakk>v1 3\<succ>r1 v1'; v1 \<noteq> v1'; flat v2 = flat v2'; \<turnstile> v2 : r2; \<turnstile> v2' : r2\<rbrakk> |
|
521 \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1' v2')" |
|
522 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 3\<succ>(ALT r1 r2) (Right v2)" |
|
523 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Left v1)" |
|
524 | "v2 3\<succ>r2 v2' \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Right v2')" |
|
525 | "v1 3\<succ>r1 v1' \<Longrightarrow> (Left v1) 3\<succ>(ALT r1 r2) (Left v1')" |
|
526 | "Void 3\<succ>EMPTY Void" |
|
527 | "(Char c) 3\<succ>(CHAR c) (Char c)" |
|
528 |
|
529 |
|
530 lemma "v1 3\<succ>r v2 \<Longrightarrow> v1 \<succ>r v2 \<and> \<turnstile> v1 : r \<and> \<turnstile> v2 : r \<and> flat v1 = flat v2" |
|
531 apply(induct rule: ValOrd3.induct) |
|
532 prefer 8 |
|
533 apply(simp) |
|
534 apply (metis Prf.intros(5) ValOrd.intros(8)) |
|
535 prefer 7 |
|
536 apply(simp) |
|
537 apply (metis Prf.intros(4) ValOrd.intros(7)) |
|
538 apply(simp) |
|
539 apply (metis Prf.intros(1) ValOrd.intros(1)) |
|
540 apply(simp) |
|
541 |
|
542 |
|
543 |
|
544 |
|
545 lemma ValOrd_trans: |
|
546 assumes "v1 \<succ>r v2" "v2 \<succ>r v3" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r" |
|
547 "flat v1 = flat v2" "flat v2 = flat v3" |
|
548 shows "v1 \<succ>r v3" |
|
549 using assms |
|
550 apply(induct r arbitrary: v1 v2 v3 s1 s2 s3) |
|
551 apply(erule Prf.cases) |
|
552 apply(simp_all)[5] |
|
553 apply(erule Prf.cases) |
|
554 apply(simp_all)[5] |
|
555 apply(erule Prf.cases) |
|
556 apply(simp_all)[5] |
|
557 apply(erule Prf.cases) |
|
558 apply(simp_all)[5] |
|
559 apply(erule Prf.cases) |
|
560 apply(simp_all)[5] |
|
561 apply(erule Prf.cases) |
|
562 apply(simp_all)[5] |
|
563 apply(erule Prf.cases) |
|
564 apply(simp_all)[5] |
|
565 apply(erule Prf.cases) |
|
566 apply(simp_all)[5] |
|
567 apply(clarify) |
|
568 apply(erule ValOrd.cases) |
|
569 apply(simp_all)[8] |
|
570 apply(erule ValOrd.cases) |
|
571 apply(simp_all)[8] |
|
572 apply(clarify) |
|
573 apply (metis ValOrd.intros(1)) |
|
574 apply(clarify) |
|
575 apply (metis ValOrd.intros(2)) |
|
576 apply(erule ValOrd.cases) |
|
577 apply(simp_all)[8] |
|
578 apply (metis ValOrd.intros(2)) |
|
579 apply(clarify) |
|
580 apply(case_tac "v1d = v1'a") |
|
581 apply(simp) |
|
582 apply (metis ValOrd_anti) |
|
583 apply (rule ValOrd.intros(2)) |
|
584 prefer 2 |
|
585 apply(auto)[1] |
|
586 apply metis |
|
587 apply(erule Prf.cases) |
|
588 apply(simp_all)[5] |
|
589 apply(erule Prf.cases) |
|
590 apply(simp_all)[5] |
|
591 apply(erule Prf.cases) |
|
592 apply(simp_all)[5] |
|
593 apply(erule ValOrd.cases) |
|
594 apply(simp_all)[8] |
|
595 apply(erule ValOrd.cases) |
|
596 apply(simp_all)[8] |
|
597 apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6)) |
|
598 apply(erule ValOrd.cases) |
|
599 apply(simp_all)[8] |
|
600 apply(erule ValOrd.cases) |
|
601 apply(simp_all)[8] |
|
602 apply (rule ValOrd.intros) |
|
603 apply(clarify) |
|
604 oops |
|
605 |
|
606 |
|
607 lemma ValOrd_max: |
|
608 shows "L r \<noteq> {} \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<longrightarrow> v' \<succ>r v \<longrightarrow> v = v'))" |
|
609 using assms |
|
610 apply(induct r) |
|
611 apply(auto)[3] |
|
612 apply(rule_tac x="Void" in exI) |
|
613 apply(rule conjI) |
|
614 apply (metis Prf.intros(4)) |
|
615 apply(rule allI) |
|
616 apply(rule impI)+ |
|
617 apply(erule ValOrd.cases) |
|
618 apply(simp_all)[8] |
|
619 apply(rule_tac x="Char char" in exI) |
|
620 apply(rule conjI) |
|
621 apply (metis Prf.intros(5)) |
|
622 apply(rule allI) |
|
623 apply(rule impI)+ |
|
624 apply(erule ValOrd.cases) |
|
625 apply(simp_all)[8] |
|
626 apply(simp add: L.simps) |
|
627 apply(auto simp: Sequ_def)[1] |
491 apply(drule meta_mp) |
628 apply(drule meta_mp) |
492 apply (metis empty_iff) |
629 apply (metis empty_iff) |
493 apply(drule meta_mp) |
630 apply(drule meta_mp) |
494 apply (metis empty_iff) |
631 apply (metis empty_iff) |
495 apply(auto)[1] |
632 apply(erule exE)+ |
496 apply(drule_tac x="Seq v va" in spec) |
633 apply(rule_tac x="Seq v va" in exI) |
497 apply(drule mp) |
634 apply(rule conjI) |
498 apply (metis Prf.intros(1)) |
635 apply (metis Prf.intros(1)) |
499 apply(auto)[1] |
636 apply(rule allI) |
500 apply(erule ValOrd.cases) |
637 apply(rule impI)+ |
501 apply(simp_all)[8] |
638 apply(rotate_tac 4) |
502 apply(rotate_tac 6) |
639 apply(erule Prf.cases) |
503 apply(erule Prf.cases) |
640 apply(simp_all)[5] |
504 apply(simp_all)[5] |
641 apply(erule ValOrd.cases) |
505 apply(rotate_tac 6) |
642 apply(simp_all)[8] |
506 apply(erule Prf.cases) |
|
507 apply(simp_all)[5] |
|
508 apply(clarify) |
|
509 apply metis |
643 apply metis |
|
644 apply(simp only: L.simps Lattices.bounded_lattice_bot_class.sup_eq_bot_iff HOL.de_Morgan_conj) |
|
645 apply(erule disjE) |
510 apply(drule meta_mp) |
646 apply(drule meta_mp) |
511 apply (metis empty_iff) |
647 apply (metis empty_iff) |
512 apply(auto)[1] |
648 apply(erule exE)+ |
513 apply(drule_tac x="Left v" in spec) |
649 apply(rule exI) |
514 apply(drule mp) |
650 apply(rule conjI) |
515 apply (metis Prf.intros) |
651 apply(rule Prf.intros) |
516 apply(auto)[1] |
652 apply(erule conjE)+ |
517 apply(rotate_tac 4) |
653 apply(assumption) |
518 apply(erule Prf.cases) |
654 apply(rule allI) |
519 apply(simp_all)[5] |
655 apply(rule impI)+ |
520 apply(erule ValOrd.cases) |
656 apply(erule Prf.cases) |
521 apply(simp_all)[8] |
657 apply(simp_all)[5] |
522 apply(erule ValOrd.cases) |
658 apply(clarify) |
523 apply(simp_all)[8] |
659 apply(erule ValOrd.cases) |
524 apply(clarify) |
660 apply(simp_all)[8] |
525 apply(auto)[1] |
661 apply(clarify) |
|
662 apply(drule meta_mp) |
|
663 apply (metis Prf_flat_L empty_iff) |
|
664 apply(auto)[1] |
|
665 apply(erule ValOrd.cases) |
|
666 apply(simp_all)[8] |
|
667 apply(clarify) |
526 oops |
668 oops |
527 |
|
528 lemma ValOrd_max2: |
|
529 shows "\<exists>v. \<turnstile> v : r \<and> (\<forall>v'. v \<succ>r v')" |
|
530 using ValOrd_max[where r="r"] |
|
531 apply - |
|
532 apply(auto) |
|
533 apply(rule_tac x="v" in exI) |
|
534 apply(auto) |
|
535 oops |
|
536 |
|
537 lemma ValOrd_trans: |
|
538 assumes "v1 \<succ>r v2" "v2 \<succ>r v3" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r" "flat v1 = flat v2" "flat v2 = flat v3" |
|
539 shows "v1 \<succ>r v3" |
|
540 using assms |
|
541 apply(induct r arbitrary: v1 v2 v3) |
|
542 apply(erule Prf.cases) |
|
543 apply(simp_all)[5] |
|
544 apply(erule Prf.cases) |
|
545 apply(simp_all)[5] |
|
546 apply(erule Prf.cases) |
|
547 apply(simp_all)[5] |
|
548 apply(erule Prf.cases) |
|
549 apply(simp_all)[5] |
|
550 apply(erule Prf.cases) |
|
551 apply(simp_all)[5] |
|
552 apply(erule Prf.cases) |
|
553 apply(simp_all)[5] |
|
554 apply(erule Prf.cases) |
|
555 apply(simp_all)[5] |
|
556 apply(erule Prf.cases) |
|
557 apply(simp_all)[5] |
|
558 apply(clarify) |
|
559 apply(erule ValOrd.cases) |
|
560 apply(simp_all)[8] |
|
561 apply(erule ValOrd.cases) |
|
562 apply(simp_all)[8] |
|
563 apply(clarify) |
|
564 apply (metis ValOrd.intros(1)) |
|
565 apply(clarify) |
|
566 apply (metis ValOrd.intros(2)) |
|
567 apply(erule ValOrd.cases) |
|
568 apply(simp_all)[8] |
|
569 apply (metis ValOrd.intros(2)) |
|
570 apply(clarify) |
|
571 apply(case_tac "v1d = v1'a") |
|
572 apply(simp) |
|
573 apply (metis ValOrd_anti) |
|
574 apply (rule ValOrd.intros(2)) |
|
575 prefer 2 |
|
576 apply(auto)[1] |
|
577 prefer 2 |
|
578 oops |
|
579 |
|
580 |
|
581 |
669 |
582 section {* Posix definition *} |
670 section {* Posix definition *} |
583 |
671 |
584 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
672 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
585 where |
673 where |
1531 apply (metis POSIXs_ALT1a) |
1620 apply (metis POSIXs_ALT1a) |
1532 apply(frule POSIXs_ALT1b) |
1621 apply(frule POSIXs_ALT1b) |
1533 apply(auto) |
1622 apply(auto) |
1534 apply(frule POSIXs_ALT1a) |
1623 apply(frule POSIXs_ALT1a) |
1535 (* HERE *) |
1624 (* HERE *) |
1536 apply(auto) |
1625 oops |
1537 apply(rule ccontr) |
|
1538 apply(simp) |
|
1539 apply(auto)[1] |
|
1540 apply(drule POSIXs_ALT1a) |
|
1541 thm ValOrd2.intros |
|
1542 |
|
1543 apply(simp (no_asm) add: POSIXs_def) |
|
1544 apply(auto)[1] |
|
1545 apply (metis POSIXs_def |
|
1546 der.simps(4) v3s) |
|
1547 apply(subst (asm) (5) POSIXs_def) |
|
1548 apply(auto)[1] |
|
1549 apply(erule Prfs.cases) |
|
1550 apply(simp_all)[5] |
|
1551 apply(erule Prfs.cases) |
|
1552 apply(simp_all)[5] |
|
1553 apply(auto)[1] |
|
1554 apply(rule ValOrd2.intros) |
|
1555 apply(drule_tac x="v1a" in meta_spec) |
|
1556 apply(drule_tac x="sb" in meta_spec) |
|
1557 apply(drule_tac meta_mp) |
|
1558 defer |
|
1559 apply (metis POSIXs_def) |
|
1560 apply(auto)[1] |
|
1561 apply(rule ValOrd2.intros) |
|
1562 apply(subst v4) |
|
1563 apply (metis Prfs_Prf) |
|
1564 apply(simp) |
|
1565 apply(drule_tac x="Left (injval r1a c v1)" in spec) |
|
1566 apply(drule mp) |
|
1567 apply(rule Prfs.intros) |
|
1568 defer |
|
1569 apply(erule ValOrd2.cases) |
|
1570 apply(simp_all)[8] |
|
1571 apply(clarify) |
|
1572 thm v4s |
|
1573 apply(subst (asm) v4s[of "sb"]) |
|
1574 apply(assumption) |
|
1575 apply(simp) |
|
1576 apply(clarify) |
|
1577 apply(erule Prfs.cases) |
|
1578 apply(simp_all)[5] |
|
1579 apply(auto)[1] |
|
1580 apply(rule ValOrd2.intros) |
|
1581 apply(subst v4) |
|
1582 apply (metis Prfs_Prf) |
|
1583 apply(simp) |
|
1584 apply(drule_tac x="Right (injval r2a c v2)" in spec) |
|
1585 apply(drule mp) |
|
1586 apply(rule Prfs.intros) |
|
1587 defer |
|
1588 apply(erule ValOrd2.cases) |
|
1589 apply(simp_all)[8] |
|
1590 apply(clarify) |
|
1591 apply(subst (asm) v4) |
|
1592 defer |
|
1593 apply(simp) |
|
1594 apply(rule ValOrd2.intros) |
|
1595 apply (metis POSIXs_ALT1a POSIXs_def Prfs.intros(3)) |
|
1596 apply(case_tac "nullable r1") |
|
1597 apply(simp (no_asm) add: POSIXs_def) |
|
1598 apply(auto)[1] |
|
1599 apply(subst (asm) (6) POSIXs_def) |
|
1600 apply(auto)[1] |
|
1601 apply(erule Prfs.cases) |
|
1602 apply(simp_all)[5] |
|
1603 apply(clarify) |
|
1604 defer |
|
1605 apply (metis Prfs.intros(3) der.simps(5) injval.simps(6) v3s) |
|
1606 apply(erule Prfs.cases) |
|
1607 apply(simp_all)[5] |
|
1608 apply(clarify) |
|
1609 apply(subst (asm) (6) POSIXs_def) |
|
1610 apply(auto)[1] |
|
1611 apply(rotate_tac 7) |
|
1612 apply(erule Prfs.cases) |
|
1613 apply(simp_all)[5] |
|
1614 apply(clarify) |
|
1615 apply(simp) |
|
1616 apply(rotate_tac 8) |
|
1617 apply(erule Prfs.cases) |
|
1618 apply(simp_all)[5] |
|
1619 apply(clarify) |
|
1620 apply(rule ValOrd2.intros(2)) |
|
1621 apply(drule_tac x="v1b" in meta_spec) |
|
1622 apply(drule_tac x="s1a" in meta_spec) |
|
1623 apply(drule meta_mp) |
|
1624 defer |
|
1625 apply(subst (asm) Cons_eq_append_conv) |
|
1626 apply(auto) |
|
1627 defer |
|
1628 defer |
|
1629 |
|
1630 |
|
1631 thm v4 |
|
1632 |
1626 |
1633 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys" |
1627 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys" |
1634 by (metis list.sel(3)) |
1628 by (metis list.sel(3)) |
1635 |
1629 |
1636 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)" |
1630 lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)" |
1759 apply(rule v3s_proj) |
1753 apply(rule v3s_proj) |
1760 apply(simp) |
1754 apply(simp) |
1761 thm v3s_proj |
1755 thm v3s_proj |
1762 apply(drule v3s_proj) |
1756 apply(drule v3s_proj) |
1763 oops |
1757 oops |
|
1758 |
|
1759 lemma Prf_inj_test: |
|
1760 assumes "v1 2\<succ> v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" |
|
1761 "length (flat v1) = length (flat v2)" |
|
1762 shows "(injval r c v1) 2\<succ> (injval r c v2)" |
|
1763 using assms |
|
1764 apply(induct c r arbitrary: v1 v2 rule: der.induct) |
|
1765 (* NULL case *) |
|
1766 apply(simp) |
|
1767 apply(erule Prf.cases) |
|
1768 apply(simp_all)[5] |
|
1769 (* EMPTY case *) |
|
1770 apply(simp) |
|
1771 apply(erule Prf.cases) |
|
1772 apply(simp_all)[5] |
|
1773 (* CHAR case *) |
|
1774 apply(case_tac "c = c'") |
|
1775 apply(simp) |
|
1776 apply(erule Prf.cases) |
|
1777 apply(simp_all)[5] |
|
1778 apply(erule Prf.cases) |
|
1779 apply(simp_all)[5] |
|
1780 apply(erule ValOrd2.cases) |
|
1781 apply(simp_all)[8] |
|
1782 apply(rule ValOrd2.intros) |
|
1783 apply(simp) |
|
1784 apply(erule Prf.cases) |
|
1785 apply(simp_all)[5] |
|
1786 (* ALT case *) |
|
1787 apply(simp) |
|
1788 apply(erule Prf.cases) |
|
1789 apply(simp_all)[5] |
|
1790 apply(auto)[2] |
|
1791 apply(erule Prf.cases) |
|
1792 apply(simp_all)[5] |
|
1793 apply(auto)[2] |
|
1794 apply(erule ValOrd2.cases) |
|
1795 apply(simp_all)[8] |
|
1796 apply(rule ValOrd2.intros) |
|
1797 apply(auto)[1] |
|
1798 apply(erule ValOrd2.cases) |
|
1799 apply(simp_all)[8] |
|
1800 apply(rule ValOrd2.intros) |
|
1801 apply(subst v4) |
|
1802 apply metis |
|
1803 apply(subst v4) |
|
1804 apply (metis) |
|
1805 apply(simp) |
|
1806 apply(erule Prf.cases) |
|
1807 apply(simp_all)[5] |
|
1808 apply(auto)[2] |
|
1809 apply(erule ValOrd2.cases) |
|
1810 apply(simp_all)[8] |
|
1811 apply(rule ValOrd2.intros) |
|
1812 apply(erule ValOrd2.cases) |
|
1813 apply(simp_all)[8] |
|
1814 (* SEQ case*) |
|
1815 apply(simp) |
|
1816 apply(case_tac "nullable r1") |
|
1817 apply(simp) |
|
1818 defer |
|
1819 apply(simp) |
|
1820 apply(erule Prf.cases) |
|
1821 apply(simp_all)[5] |
|
1822 apply(erule Prf.cases) |
|
1823 apply(simp_all)[5] |
|
1824 apply(clarify) |
|
1825 apply(erule ValOrd2.cases) |
|
1826 apply(simp_all)[8] |
|
1827 apply(clarify) |
|
1828 apply(rule ValOrd2.intros) |
|
1829 apply(simp) |
|
1830 apply(rule ValOrd2.intros) |
|
1831 apply(auto)[1] |
|
1832 |
|
1833 using injval_inj |
|
1834 apply(simp add: inj_on_def) |
|
1835 apply metis |
|
1836 apply(erule Prf.cases) |
|
1837 apply(simp_all)[5] |
|
1838 apply(erule Prf.cases) |
|
1839 apply(simp_all)[5] |
|
1840 apply(clarify) |
|
1841 apply(erule Prf.cases) |
|
1842 apply(simp_all)[5] |
|
1843 apply(erule Prf.cases) |
|
1844 apply(simp_all)[5] |
|
1845 apply(clarify) |
|
1846 apply(erule ValOrd2.cases) |
|
1847 apply(simp_all)[8] |
|
1848 apply(clarify) |
|
1849 apply(erule ValOrd2.cases) |
|
1850 apply(simp_all)[8] |
|
1851 apply(clarify) |
|
1852 apply (metis ValOrd2.intros(1)) |
|
1853 apply(rule ValOrd2.intros) |
|
1854 apply metis |
|
1855 using injval_inj |
|
1856 apply(simp add: inj_on_def) |
|
1857 apply metis |
|
1858 apply(clarify) |
|
1859 apply(simp) |
|
1860 apply(erule Prf.cases) |
|
1861 apply(simp_all)[5] |
|
1862 apply(clarify) |
|
1863 apply(rule ValOrd2.intros) |
|
1864 apply(rule Ord1) |
|
1865 apply(rule h) |
|
1866 apply(simp) |
|
1867 apply(simp) |
|
1868 apply (metis list.distinct(1) mkeps_flat v4) |
|
1869 apply(clarify) |
|
1870 apply(erule Prf.cases) |
|
1871 apply(simp_all)[5] |
|
1872 apply(clarify) |
|
1873 apply(rotate_tac 7) |
|
1874 apply(erule Prf.cases) |
|
1875 apply(simp_all)[5] |
|
1876 apply(clarify) |
|
1877 defer |
|
1878 apply(clarify) |
|
1879 apply(erule ValOrd2.cases) |
|
1880 apply(simp_all)[8] |
|
1881 apply(clarify) |
|
1882 apply (metis ValOrd2.intros(1)) |
|
1883 apply(erule ValOrd2.cases) |
|
1884 apply(simp_all)[8] |
|
1885 apply(clarify) |
|
1886 apply(simp) |
|
1887 apply (rule_tac ValOrd2.intros(2)) |
|
1888 prefer 2 |
|
1889 apply (metis list.distinct(1) mkeps_flat v4) |
|
1890 |
1764 |
1891 |
1765 lemma Prf_inj_test: |
1892 lemma Prf_inj_test: |
1766 assumes "v1 2\<succ> v2" "\<Turnstile>s1 v1 : der c r" "\<Turnstile>s2 v2 : der c r" |
1893 assumes "v1 2\<succ> v2" "\<Turnstile>s1 v1 : der c r" "\<Turnstile>s2 v2 : der c r" |
1767 shows "(injval r c v1) 2\<succ> (injval r c v2)" |
1894 shows "(injval r c v1) 2\<succ> (injval r c v2)" |
1768 using assms |
1895 using assms |