644 qed |
644 qed |
645 |
645 |
646 lemma eq_dep: "depend s = depend s'" |
646 lemma eq_dep: "depend s = depend s'" |
647 by (unfold s_def depend_set_unchanged, auto) |
647 by (unfold s_def depend_set_unchanged, auto) |
648 |
648 |
649 lemma eq_cp: |
649 lemma eq_cp_pre: |
650 fixes th' |
650 fixes th' |
651 assumes neq_th: "th' \<noteq> th" |
651 assumes neq_th: "th' \<noteq> th" |
652 and nd: "th \<notin> dependents s th'" |
652 and nd: "th \<notin> dependents s th'" |
653 shows "cp s th' = cp s' th'" |
653 shows "cp s th' = cp s' th'" |
654 apply (unfold cp_eq_cpreced cpreced_def) |
654 apply (unfold cp_eq_cpreced cpreced_def) |
673 } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = |
673 } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = |
674 ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" |
674 ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" |
675 by (auto simp:image_def) |
675 by (auto simp:image_def) |
676 thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = |
676 thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = |
677 Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp |
677 Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp |
|
678 qed |
|
679 |
|
680 lemma no_dependents: |
|
681 assumes "th' \<noteq> th" |
|
682 shows "th \<notin> dependents s th'" |
|
683 proof |
|
684 assume h: "th \<in> dependents s th'" |
|
685 from step_back_step [OF vt_s[unfolded s_def]] |
|
686 have "step s' (Set th prio)" . |
|
687 hence "th \<in> runing s'" by (cases, simp) |
|
688 hence rd_th: "th \<in> readys s'" |
|
689 by (simp add:readys_def runing_def) |
|
690 from h have "(Th th, Th th') \<in> (depend s')\<^sup>+" |
|
691 by (unfold s_dependents_def, unfold eq_depend, unfold eq_dep, auto) |
|
692 from tranclD[OF this] |
|
693 obtain z where "(Th th, z) \<in> depend s'" by auto |
|
694 with rd_th show "False" |
|
695 apply (case_tac z, auto simp:readys_def s_waiting_def s_depend_def s_waiting_def cs_waiting_def) |
|
696 by (fold wq_def, blast) |
|
697 qed |
|
698 |
|
699 (* Result improved *) |
|
700 lemma eq_cp: |
|
701 fixes th' |
|
702 assumes neq_th: "th' \<noteq> th" |
|
703 shows "cp s th' = cp s' th'" |
|
704 proof(rule eq_cp_pre [OF neq_th]) |
|
705 from no_dependents[OF neq_th] |
|
706 show "th \<notin> dependents s th'" . |
678 qed |
707 qed |
679 |
708 |
680 lemma eq_up: |
709 lemma eq_up: |
681 fixes th' th'' |
710 fixes th' th'' |
682 assumes dp1: "th \<in> dependents s th'" |
711 assumes dp1: "th \<in> dependents s th'" |
739 from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend) |
768 from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend) |
740 from dependents_child_unique[OF vt_s _ _ h this] |
769 from dependents_child_unique[OF vt_s _ _ h this] |
741 th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) |
770 th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) |
742 with False show False by auto |
771 with False show False by auto |
743 qed |
772 qed |
744 from eq_cp[OF neq_th1 this] |
773 from eq_cp_pre[OF neq_th1 this] |
745 show ?thesis . |
774 show ?thesis . |
746 qed |
775 qed |
747 } |
776 } |
748 ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = |
777 ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = |
749 {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) |
778 {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) |
787 from children_no_dep[OF vt_s _ _ this] |
816 from children_no_dep[OF vt_s _ _ this] |
788 th1_in dp' |
817 th1_in dp' |
789 show False by (auto simp:children_def) |
818 show False by (auto simp:children_def) |
790 qed |
819 qed |
791 thus ?thesis |
820 thus ?thesis |
792 proof(rule eq_cp) |
821 proof(rule eq_cp_pre) |
793 show "th \<notin> dependents s th1" |
822 show "th \<notin> dependents s th1" |
794 proof |
823 proof |
795 assume "th \<in> dependents s th1" |
824 assume "th \<in> dependents s th1" |
796 from dependents_child_unique[OF vt_s _ _ this dp1] |
825 from dependents_child_unique[OF vt_s _ _ this dp1] |
797 th1_in dp' have "th1 = th'" |
826 th1_in dp' have "th1 = th'" |
872 from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend) |
901 from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend) |
873 from dependents_child_unique[OF vt_s _ _ h this] |
902 from dependents_child_unique[OF vt_s _ _ h this] |
874 th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) |
903 th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def) |
875 with False show False by auto |
904 with False show False by auto |
876 qed |
905 qed |
877 from eq_cp[OF neq_th1 this] |
906 from eq_cp_pre[OF neq_th1 this] |
878 show ?thesis . |
907 show ?thesis . |
879 qed |
908 qed |
880 } |
909 } |
881 ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = |
910 ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = |
882 {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) |
911 {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def) |
912 with eq_cps show ?thesis by simp |
941 with eq_cps show ?thesis by simp |
913 next |
942 next |
914 case False |
943 case False |
915 assume neq_th1: "th1 \<noteq> th" |
944 assume neq_th1: "th1 \<noteq> th" |
916 thus ?thesis |
945 thus ?thesis |
917 proof(rule eq_cp) |
946 proof(rule eq_cp_pre) |
918 show "th \<notin> dependents s th1" |
947 show "th \<notin> dependents s th1" |
919 proof |
948 proof |
920 assume "th \<in> dependents s th1" |
949 assume "th \<in> dependents s th1" |
921 hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend) |
950 hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend) |
922 from children_no_dep[OF vt_s _ _ this] |
951 from children_no_dep[OF vt_s _ _ this] |