1 theory ExtGG |
1 theory ExtGG |
2 imports PrioG |
2 imports PrioG |
3 begin |
3 begin |
4 |
4 |
5 lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> birthtime th s < length s" |
5 lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s" |
6 apply (induct s, simp) |
6 apply (induct s, simp) |
7 proof - |
7 proof - |
8 fix a s |
8 fix a s |
9 assume ih: "s \<noteq> [] \<Longrightarrow> birthtime th s < length s" |
9 assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s" |
10 and eq_as: "a # s \<noteq> []" |
10 and eq_as: "a # s \<noteq> []" |
11 show "birthtime th (a # s) < length (a # s)" |
11 show "last_set th (a # s) < length (a # s)" |
12 proof(cases "s \<noteq> []") |
12 proof(cases "s \<noteq> []") |
13 case False |
13 case False |
14 from False show ?thesis |
14 from False show ?thesis |
15 by (cases a, auto simp:birthtime.simps) |
15 by (cases a, auto simp:last_set.simps) |
16 next |
16 next |
17 case True |
17 case True |
18 from ih [OF True] show ?thesis |
18 from ih [OF True] show ?thesis |
19 by (cases a, auto simp:birthtime.simps) |
19 by (cases a, auto simp:last_set.simps) |
20 qed |
20 qed |
21 qed |
21 qed |
22 |
22 |
23 lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []" |
23 lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []" |
24 by (induct s, auto simp:threads.simps) |
24 by (induct s, auto simp:threads.simps) |
44 |
44 |
45 lemma eq_cp_s_th: "cp s th = preced th s" |
45 lemma eq_cp_s_th: "cp s th = preced th s" |
46 proof - |
46 proof - |
47 from highest and max_cp_eq[OF vt_s] |
47 from highest and max_cp_eq[OF vt_s] |
48 have is_max: "preced th s = Max ((\<lambda>th. preced th s) ` threads s)" by simp |
48 have is_max: "preced th s = Max ((\<lambda>th. preced th s) ` threads s)" by simp |
49 have sbs: "({th} \<union> dependents (wq s) th) \<subseteq> threads s" |
49 have sbs: "({th} \<union> dependants (wq s) th) \<subseteq> threads s" |
50 proof - |
50 proof - |
51 from threads_s and dependents_threads[OF vt_s, of th] |
51 from threads_s and dependants_threads[OF vt_s, of th] |
52 show ?thesis by auto |
52 show ?thesis by auto |
53 qed |
53 qed |
54 show ?thesis |
54 show ?thesis |
55 proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI) |
55 proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI) |
56 show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)" by simp |
56 show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)" by simp |
57 next |
57 next |
58 fix y |
58 fix y |
59 assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)" |
59 assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)" |
60 then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependents (wq s) th)" |
60 then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependants (wq s) th)" |
61 and eq_y: "y = preced th1 s" by auto |
61 and eq_y: "y = preced th1 s" by auto |
62 show "y \<le> preced th s" |
62 show "y \<le> preced th s" |
63 proof(unfold is_max, rule Max_ge) |
63 proof(unfold is_max, rule Max_ge) |
64 from finite_threads[OF vt_s] |
64 from finite_threads[OF vt_s] |
65 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp |
65 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp |
67 from sbs th1_in and eq_y |
67 from sbs th1_in and eq_y |
68 show "y \<in> (\<lambda>th. preced th s) ` threads s" by auto |
68 show "y \<in> (\<lambda>th. preced th s) ` threads s" by auto |
69 qed |
69 qed |
70 next |
70 next |
71 from sbs and finite_threads[OF vt_s] |
71 from sbs and finite_threads[OF vt_s] |
72 show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))" |
72 show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))" |
73 by (auto intro:finite_subset) |
73 by (auto intro:finite_subset) |
74 qed |
74 qed |
75 qed |
75 qed |
76 |
76 |
77 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)" |
77 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)" |
467 proof - |
467 proof - |
468 have "?L = cpreced (wq (t@s)) (t@s) th" |
468 have "?L = cpreced (wq (t@s)) (t@s) th" |
469 by (unfold cp_eq_cpreced, simp) |
469 by (unfold cp_eq_cpreced, simp) |
470 also have "\<dots> = ?R" |
470 also have "\<dots> = ?R" |
471 proof(unfold cpreced_def) |
471 proof(unfold cpreced_def) |
472 show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependents (wq (t @ s)) th)) = |
472 show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependants (wq (t @ s)) th)) = |
473 Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" |
473 Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" |
474 (is "Max (?f ` ({th} \<union> ?A)) = Max (?f ` ?B)") |
474 (is "Max (?f ` ({th} \<union> ?A)) = Max (?f ` ?B)") |
475 proof(cases "?A = {}") |
475 proof(cases "?A = {}") |
476 case False |
476 case False |
477 have "Max (?f ` ({th} \<union> ?A)) = Max (insert (?f th) (?f ` ?A))" by simp |
477 have "Max (?f ` ({th} \<union> ?A)) = Max (insert (?f th) (?f ` ?A))" by simp |
478 moreover have "\<dots> = max (?f th) (Max (?f ` ?A))" |
478 moreover have "\<dots> = max (?f th) (Max (?f ` ?A))" |
479 proof(rule Max_insert) |
479 proof(rule Max_insert) |
480 show "finite (?f ` ?A)" |
480 show "finite (?f ` ?A)" |
481 proof - |
481 proof - |
482 from dependents_threads[OF vt_t] |
482 from dependants_threads[OF vt_t] |
483 have "?A \<subseteq> threads (t@s)" . |
483 have "?A \<subseteq> threads (t@s)" . |
484 moreover from finite_threads[OF vt_t] have "finite \<dots>" . |
484 moreover from finite_threads[OF vt_t] have "finite \<dots>" . |
485 ultimately show ?thesis |
485 ultimately show ?thesis |
486 by (auto simp:finite_subset) |
486 by (auto simp:finite_subset) |
487 qed |
487 qed |
495 proof(rule Max_mono) |
495 proof(rule Max_mono) |
496 from False show "(?f ` ?A) \<noteq> {}" by simp |
496 from False show "(?f ` ?A) \<noteq> {}" by simp |
497 next |
497 next |
498 show "?f ` ?A \<subseteq> ?f ` ?B" |
498 show "?f ` ?A \<subseteq> ?f ` ?B" |
499 proof - |
499 proof - |
500 have "?A \<subseteq> ?B" by (rule dependents_threads[OF vt_t]) |
500 have "?A \<subseteq> ?B" by (rule dependants_threads[OF vt_t]) |
501 thus ?thesis by auto |
501 thus ?thesis by auto |
502 qed |
502 qed |
503 next |
503 next |
504 from finite_threads[OF vt_t] |
504 from finite_threads[OF vt_t] |
505 show "finite (?f ` ?B)" by simp |
505 show "finite (?f ` ?B)" by simp |
564 moreover from th_cp_preced and th_kept have "\<dots> = preced th (t @ s)" |
564 moreover from th_cp_preced and th_kept have "\<dots> = preced th (t @ s)" |
565 by simp |
565 by simp |
566 finally have h: "cp (t @ s) th' = preced th (t @ s)" . |
566 finally have h: "cp (t @ s) th' = preced th (t @ s)" . |
567 show False |
567 show False |
568 proof - |
568 proof - |
569 have "dependents (wq (t @ s)) th' = {}" |
569 have "dependants (wq (t @ s)) th' = {}" |
570 by (rule count_eq_dependents [OF vt_t eq_pv]) |
570 by (rule count_eq_dependants [OF vt_t eq_pv]) |
571 moreover have "preced th' (t @ s) \<noteq> preced th (t @ s)" |
571 moreover have "preced th' (t @ s) \<noteq> preced th (t @ s)" |
572 proof |
572 proof |
573 assume "preced th' (t @ s) = preced th (t @ s)" |
573 assume "preced th' (t @ s) = preced th (t @ s)" |
574 hence "th' = th" |
574 hence "th' = th" |
575 proof(rule preced_unique) |
575 proof(rule preced_unique) |
981 and dp: "(Th th, Th th') \<in> (depend (t @ s))\<^sup>+" by auto |
981 and dp: "(Th th, Th th') \<in> (depend (t @ s))\<^sup>+" by auto |
982 have "th' \<in> runing (t@s)" |
982 have "th' \<in> runing (t@s)" |
983 proof - |
983 proof - |
984 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" |
984 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" |
985 proof - |
985 proof - |
986 have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')) = |
986 have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')) = |
987 preced th (t@s)" |
987 preced th (t@s)" |
988 proof(rule Max_eqI) |
988 proof(rule Max_eqI) |
989 fix y |
989 fix y |
990 assume "y \<in> (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')" |
990 assume "y \<in> (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')" |
991 then obtain th1 where |
991 then obtain th1 where |
992 h1: "th1 = th' \<or> th1 \<in> dependents (wq (t @ s)) th'" |
992 h1: "th1 = th' \<or> th1 \<in> dependants (wq (t @ s)) th'" |
993 and eq_y: "y = preced th1 (t@s)" by auto |
993 and eq_y: "y = preced th1 (t@s)" by auto |
994 show "y \<le> preced th (t @ s)" |
994 show "y \<le> preced th (t @ s)" |
995 proof - |
995 proof - |
996 from max_preced |
996 from max_preced |
997 have "preced th (t @ s) = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" . |
997 have "preced th (t @ s) = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" . |
1001 have "th1 \<in> threads (t@s)" |
1001 have "th1 \<in> threads (t@s)" |
1002 proof |
1002 proof |
1003 assume "th1 = th'" |
1003 assume "th1 = th'" |
1004 with th'_in show ?thesis by (simp add:readys_def) |
1004 with th'_in show ?thesis by (simp add:readys_def) |
1005 next |
1005 next |
1006 assume "th1 \<in> dependents (wq (t @ s)) th'" |
1006 assume "th1 \<in> dependants (wq (t @ s)) th'" |
1007 with dependents_threads [OF vt_t] |
1007 with dependants_threads [OF vt_t] |
1008 show "th1 \<in> threads (t @ s)" by auto |
1008 show "th1 \<in> threads (t @ s)" by auto |
1009 qed |
1009 qed |
1010 with eq_y show " y \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" by simp |
1010 with eq_y show " y \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" by simp |
1011 next |
1011 next |
1012 from finite_threads[OF vt_t] |
1012 from finite_threads[OF vt_t] |
1013 show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" by simp |
1013 show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" by simp |
1014 qed |
1014 qed |
1015 ultimately show ?thesis by auto |
1015 ultimately show ?thesis by auto |
1016 qed |
1016 qed |
1017 next |
1017 next |
1018 from finite_threads[OF vt_t] dependents_threads [OF vt_t, of th'] |
1018 from finite_threads[OF vt_t] dependants_threads [OF vt_t, of th'] |
1019 show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th'))" |
1019 show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th'))" |
1020 by (auto intro:finite_subset) |
1020 by (auto intro:finite_subset) |
1021 next |
1021 next |
1022 from dp |
1022 from dp |
1023 have "th \<in> dependents (wq (t @ s)) th'" |
1023 have "th \<in> dependants (wq (t @ s)) th'" |
1024 by (unfold cs_dependents_def, auto simp:eq_depend) |
1024 by (unfold cs_dependants_def, auto simp:eq_depend) |
1025 thus "preced th (t @ s) \<in> |
1025 thus "preced th (t @ s) \<in> |
1026 (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')" |
1026 (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')" |
1027 by auto |
1027 by auto |
1028 qed |
1028 qed |
1029 moreover have "\<dots> = Max (cp (t @ s) ` readys (t @ s))" |
1029 moreover have "\<dots> = Max (cp (t @ s) ` readys (t @ s))" |
1030 proof - |
1030 proof - |
1031 from max_preced and max_cp_eq[OF vt_t, symmetric] |
1031 from max_preced and max_cp_eq[OF vt_t, symmetric] |