502 with th2_r have "False" by auto |
505 with th2_r have "False" by auto |
503 } |
506 } |
504 ultimately show "False" by metis |
507 ultimately show "False" by metis |
505 qed |
508 qed |
506 |
509 |
507 lemma max_cpreceds_readys_threads: |
510 lemma cpreced2_cpreced: "cpreced2 s th = cpreced (wq s) s th" |
508 assumes vt: "vt s" |
511 unfolding cpreced2_def wq_def |
509 shows "Max (cpreceds2 s (readys s)) = Max (cpreceds2 s (threads s))" |
512 apply(induct s rule: schs.induct) |
510 apply(case_tac "threads s = {}") |
513 apply(simp add: Let_def cpreced_def dependants_def RAG_def waits_def holds_def preced_def) |
511 apply(simp add: readys_def) |
514 apply(simp add: Let_def) |
512 using vt |
515 apply(simp add: Let_def) |
513 apply(induct) |
516 apply(simp add: Let_def) |
514 apply(simp) |
517 apply(subst (2) schs.simps) |
515 apply(erule step.cases) |
518 apply(simp add: Let_def) |
516 apply(auto simp add: readys_def waits2_def waits_def Let_def holding_def runing_def holds2_def) |
519 apply(subst (2) schs.simps) |
517 defer |
520 apply(simp add: Let_def) |
518 defer |
521 done |
519 oops |
522 |
|
523 lemma cpreced_Exit: |
|
524 shows "cpreced2 (Exit th # s) th' = cpreced2 s th'" |
|
525 by (simp add: cpreced2_cpreced cpreced_def preced_def wq_def Let_def) |
520 |
526 |
521 lemma readys_Exit: |
527 lemma readys_Exit: |
522 shows "readys (Exit th # s) \<subseteq> readys s" |
528 shows "readys (Exit th # s) = readys s - {th}" |
523 by (auto simp add: readys_def waits2_def Let_def) |
529 by (auto simp add: readys_def waits2_def Let_def) |
524 |
530 |
525 lemma readys_Create: |
531 lemma readys_Create: |
526 shows "readys (Create th prio # s) \<subseteq> {th} \<union> readys s" |
532 shows "readys (Create th prio # s) \<subseteq> {th} \<union> readys s" |
527 by (auto simp add: readys_def waits2_def Let_def) |
533 apply (auto simp add: readys_def waits2_def Let_def waits_def) |
|
534 done |
528 |
535 |
529 lemma readys_Set: |
536 lemma readys_Set: |
530 shows "readys (Set th prio # s) \<subseteq> readys s" |
537 shows "readys (Set th prio # s) = readys s" |
531 by (auto simp add: readys_def waits2_def Let_def) |
538 by (auto simp add: readys_def waits2_def Let_def) |
532 |
539 |
533 |
540 |
534 lemma readys_P: |
541 lemma readys_P: |
535 shows "readys (P th cs # s) \<subseteq> readys s" |
542 shows "readys (P th cs # s) \<subseteq> readys s" |
547 lemma readys_V: |
554 lemma readys_V: |
548 shows "readys (V th cs # s) \<subseteq> readys s \<union> set (wq s cs)" |
555 shows "readys (V th cs # s) \<subseteq> readys s \<union> set (wq s cs)" |
549 apply(auto simp add: readys_def waits2_def waits_def Let_def wq_def) |
556 apply(auto simp add: readys_def waits2_def waits_def Let_def wq_def) |
550 done |
557 done |
551 |
558 |
552 lemma |
559 |
|
560 fun the_th :: "node \<Rightarrow> thread" |
|
561 where "the_th (Th th) = th" |
|
562 |
|
563 lemma image_Collect2: |
|
564 "f ` A = {f x | x. x \<in> A}" |
|
565 apply(auto) |
|
566 done |
|
567 |
|
568 lemma Collect_disj_eq2: |
|
569 "{f x | x. x = y \<or> x \<in> A} = {f y} \<union> {f x | x. x \<in> A}" |
|
570 by (auto) |
|
571 |
|
572 lemma last_set_lt: |
|
573 "th \<in> threads s \<Longrightarrow> last_set th s < length s" |
|
574 apply(induct rule: threads.induct) |
|
575 apply(auto) |
|
576 done |
|
577 |
|
578 lemma last_set_eq_iff: |
|
579 assumes "th1 \<in> threads s" "th2 \<in> threads s" |
|
580 shows "last_set th1 s = last_set th2 s \<longleftrightarrow> th1 = th2" |
|
581 using assms |
|
582 apply(induct s rule: threads.induct) |
|
583 apply(auto split:if_splits dest:last_set_lt) |
|
584 done |
|
585 |
|
586 lemma preced_eq_iff: |
|
587 assumes th_in1: "th1 \<in> threads s" |
|
588 and th_in2: "th2 \<in> threads s" |
|
589 shows "preced th1 s = preced th2 s \<longleftrightarrow> th1 = th2" |
|
590 using assms |
|
591 by (auto simp add: preced_def last_set_eq_iff) |
|
592 |
|
593 lemma dm_RAG_threads: |
|
594 assumes vt: "vt s" |
|
595 and in_dom: "(Th th) \<in> Domain (RAG2 s)" |
|
596 shows "th \<in> threads s" |
|
597 proof - |
|
598 from in_dom obtain n where a: "(Th th, n) \<in> RAG2 s" by auto |
|
599 then obtain cs where "n = Cs cs" |
|
600 unfolding RAG2_def RAG_def |
|
601 by auto |
|
602 then have "(Th th, Cs cs) \<in> RAG2 s" using a by simp |
|
603 hence "th \<in> set (wq s cs)" |
|
604 unfolding RAG2_def wq_def RAG_def waits_def |
|
605 by (auto) |
|
606 then show ?thesis |
|
607 apply(rule_tac wq_threads) |
|
608 apply(rule assms) |
|
609 apply(simp) |
|
610 done |
|
611 qed |
|
612 |
|
613 lemma cpreced_eq_iff: |
|
614 assumes "th1 \<in> readys s" "th2 \<in> readys s" "vt s" |
|
615 shows "cpreced2 s th1 = cpreced2 s th2 \<longleftrightarrow> th1 = th2" |
|
616 proof |
|
617 def S1\<equiv>"({th1} \<union> dependants (wq s) th1)" |
|
618 def S2\<equiv>"({th2} \<union> dependants (wq s) th2)" |
|
619 have fin: "finite ((the_th o fst) ` ((RAG (wq s))\<^sup>+))" |
|
620 apply(rule) |
|
621 apply(simp add: finite_trancl) |
|
622 apply(simp add: wq_def) |
|
623 apply(rule finite_RAG[simplified RAG2_def]) |
|
624 apply(rule assms) |
|
625 done |
|
626 |
|
627 from fin have h: "finite (preceds s S1)" "finite (preceds s S2)" |
|
628 apply(simp_all add: S2_def S1_def Collect_disj_eq2 image_Collect[symmetric]) |
|
629 apply(rule) |
|
630 apply(simp add: dependants_def) |
|
631 apply(rule rev_finite_subset) |
|
632 apply(assumption) |
|
633 apply(auto simp add: image_def)[1] |
|
634 apply(metis fst_conv the_th.simps) |
|
635 apply(rule) |
|
636 apply(simp add: dependants_def) |
|
637 apply(rule rev_finite_subset) |
|
638 apply(assumption) |
|
639 apply(auto simp add: image_def)[1] |
|
640 apply(metis fst_conv the_th.simps) |
|
641 done |
|
642 moreover have "S1 \<noteq> {}" "S2 \<noteq> {}" by (simp_all add: S1_def S2_def) |
|
643 then have "(preceds s S1) \<noteq> {}" "(preceds s S2) \<noteq> {}" by simp_all |
|
644 ultimately have m: "Max (preceds s S1) \<in> (preceds s S1)" "Max (preceds s S2) \<in> (preceds s S2)" |
|
645 apply(rule_tac [!] Max_in) |
|
646 apply(simp_all) |
|
647 done |
|
648 |
|
649 assume q: "cpreced2 s th1 = cpreced2 s th2" |
|
650 then have eq_max: "Max (preceds s S1) = Max (preceds s S2)" |
|
651 unfolding cpreced2_cpreced cpreced_def |
|
652 apply(simp only: S1_def S2_def) |
|
653 apply(simp add: Collect_disj_eq2) |
|
654 done |
|
655 |
|
656 obtain th0 where th0_in: "th0 \<in> S1" "th0 \<in> S2" and |
|
657 eq_f_th1: "preced th0 s = Max (preceds s S1)" |
|
658 "preced th0 s = Max (preceds s S2)" |
|
659 using m |
|
660 apply(clarify) |
|
661 apply(simp add: eq_max) |
|
662 apply(subst (asm) (2) preced_eq_iff) |
|
663 apply(insert assms(2))[1] |
|
664 apply(simp add: S2_def) |
|
665 apply(auto)[1] |
|
666 apply (metis contra_subsetD readys_threads) |
|
667 apply(simp add: dependants_def) |
|
668 apply(subgoal_tac "Th tha \<in> Domain ((RAG2 s)^+)") |
|
669 apply(simp add: trancl_domain) |
|
670 apply (metis Domain_RAG_threads assms(3)) |
|
671 apply(simp only: RAG2_def wq_def) |
|
672 apply (metis Domain_iff) |
|
673 apply(insert assms(1))[1] |
|
674 apply(simp add: S1_def) |
|
675 apply(auto)[1] |
|
676 apply (metis contra_subsetD readys_threads) |
|
677 apply(simp add: dependants_def) |
|
678 apply(subgoal_tac "Th th \<in> Domain ((RAG2 s)^+)") |
|
679 apply(simp add: trancl_domain) |
|
680 apply (metis Domain_RAG_threads assms(3)) |
|
681 apply(simp only: RAG2_def wq_def) |
|
682 apply (metis Domain_iff) |
|
683 apply(simp) |
|
684 done |
|
685 then show "th1 = th2" |
|
686 apply - |
|
687 apply(insert th0_in assms(1, 2))[1] |
|
688 apply(simp add: S1_def S2_def) |
|
689 apply(auto) |
|
690 --"first case" |
|
691 prefer 2 |
|
692 apply(subgoal_tac "Th th2 \<in> Domain (RAG2 s)") |
|
693 apply(subgoal_tac "\<exists>cs. (Th th2, Cs cs) \<in> RAG2 s") |
|
694 apply(erule exE) |
|
695 apply(simp add: runing_def RAG2_def RAG_def readys_def waits2_def)[1] |
|
696 apply(auto simp add: RAG2_def RAG_def)[1] |
|
697 apply(subgoal_tac "Th th2 \<in> Domain ((RAG2 s)^+)") |
|
698 apply (metis trancl_domain) |
|
699 apply(subgoal_tac "(Th th2, Th th1) \<in> (RAG2 s)^+") |
|
700 apply (metis Domain_iff) |
|
701 apply(simp add: dependants_def RAG2_def wq_def) |
|
702 --"second case" |
|
703 apply(subgoal_tac "Th th1 \<in> Domain (RAG2 s)") |
|
704 apply(subgoal_tac "\<exists>cs. (Th th1, Cs cs) \<in> RAG2 s") |
|
705 apply(erule exE) |
|
706 apply(insert assms(1))[1] |
|
707 apply(simp add: runing_def RAG2_def RAG_def readys_def waits2_def)[1] |
|
708 apply(auto simp add: RAG2_def RAG_def)[1] |
|
709 apply(subgoal_tac "Th th1 \<in> Domain ((RAG2 s)^+)") |
|
710 apply (metis trancl_domain) |
|
711 apply(subgoal_tac "(Th th1, Th th2) \<in> (RAG2 s)^+") |
|
712 apply (metis Domain_iff) |
|
713 apply(simp add: dependants_def RAG2_def wq_def) |
|
714 --"third case" |
|
715 apply(rule dchain_unique) |
|
716 apply(rule assms(3)) |
|
717 apply(simp add: dependants_def RAG2_def wq_def) |
|
718 apply(simp) |
|
719 apply(simp add: dependants_def RAG2_def wq_def) |
|
720 apply(simp) |
|
721 done |
|
722 next |
|
723 assume "th1 = th2" |
|
724 then show "cpreced2 s th1 = cpreced2 s th2" by simp |
|
725 qed |
|
726 |
|
727 lemma at_most_one_running: |
553 assumes "vt s" |
728 assumes "vt s" |
554 shows "card (runing s) \<le> 1" |
729 shows "card (runing s) \<le> 1" |
555 proof (rule ccontr) |
730 proof (rule ccontr) |
556 assume "\<not> card (runing s) \<le> 1" |
731 assume "\<not> card (runing s) \<le> 1" |
557 then have "2 \<le> card (runing s)" by auto |
732 then have "2 \<le> card (runing s)" by auto |
558 moreover |
733 moreover |
559 have "finite (runing s)" sorry |
734 have "finite (runing s)" |
560 ultimately obtain th1 th2 where "th1 \<noteq> th2" "th1 \<in> runing s" "th2 \<in> runing s" |
735 by (metis `\<not> card (runing s) \<le> 1` card_infinite le0) |
561 by (auto simp add: numerals card_le_Suc_iff) (blast) |
736 ultimately obtain th1 th2 where a: |
562 |
737 "th1 \<noteq> th2" "th1 \<in> runing s" "th2 \<in> runing s" |
563 show "False" |
738 "cpreced2 s th1 = cpreced2 s th2" |
564 apply(simp) |
739 apply(auto simp add: numerals card_le_Suc_iff runing_def) |
565 oops |
740 apply(blast) |
566 |
741 done |
|
742 then have "th1 = th2" |
|
743 apply(subst (asm) cpreced_eq_iff) |
|
744 apply(auto intro: assms a) |
|
745 apply (metis contra_subsetD runing_ready)+ |
|
746 done |
|
747 then show "False" using a(1) by auto |
|
748 qed |
|
749 |
|
750 |
|
751 |
|
752 |
|
753 done |
|
754 |
|
755 |
|
756 (* |
|
757 obtain th0 where th0_in: "th0 \<in> S1 \<and> th0 \<in> S2" |
|
758 and eq_f_th0: "preced th0 s = Max ((\<lambda>th. preced th s) ` (S1 \<inter> S2))" |
|
759 proof - |
|
760 from fin have h1: "finite ((\<lambda>th. preced th s) ` (S1 \<inter> S2))" |
|
761 apply(simp only: S1_def S2_def) |
|
762 apply(rule) |
|
763 apply(rule) |
|
764 apply(rule) |
|
765 apply(simp add: dependants_def) |
|
766 apply(rule rev_finite_subset) |
|
767 apply(assumption) |
|
768 apply(auto simp add: image_def) |
|
769 apply (metis fst_conv the_th.simps) |
|
770 done |
|
771 moreover |
|
772 have "S1 \<inter> S2 \<noteq> {}" apply (simp add: S1_def S2_def) |
|
773 apply(auto) |
|
774 |
|
775 done |
|
776 then have h2: "((\<lambda>th. preced th s) ` (S1 \<union> S2)) \<noteq> {}" by simp |
|
777 ultimately have "Max ((\<lambda>th. preced th s) ` (S1 \<union> S2)) \<in> ((\<lambda>th. preced th s) ` (S1 \<union> S2))" |
|
778 apply(rule Max_in) |
|
779 done |
|
780 then show ?thesis using that[intro] apply(auto) |
|
781 |
|
782 apply(erule_tac preced_unique) |
|
783 done |
|
784 qed |
|
785 *) |
567 |
786 |
568 end |
787 end |