1 <<<<<<< local

   710 =======

   711 theory ExtGG

   712 imports PrioG CpsG

   713 begin

   714 

   715 text {* 

   716   The following two auxiliary lemmas are used to reason about @{term Max}.

   717 *}

   718 lemma image_Max_eqI: 

   719   assumes "finite B"

   720   and "b \<in> B"

   721   and "\<forall> x \<in> B. f x \<le> f b"

   722   shows "Max (f ` B) = f b"

   723   using assms

   724   using Max_eqI by blast 

   725 

   726 lemma image_Max_subset:

   727   assumes "finite A"

   728   and "B \<subseteq> A"

   729   and "a \<in> B"

   730   and "Max (f ` A) = f a"

   731   shows "Max (f ` B) = f a"

   732 proof(rule image_Max_eqI)

   733   show "finite B"

   734     using assms(1) assms(2) finite_subset by auto 

   735 next

   736   show "a \<in> B" using assms by simp

   737 next

   738   show "\<forall>x\<in>B. f x \<le> f a"

   739     by (metis Max_ge assms(1) assms(2) assms(4) 

   740             finite_imageI image_eqI subsetCE) 

   741 qed

   742 

   743 text {*

   744   The following locale @{text "highest_gen"} sets the basic context for our

   745   investigation: supposing thread @{text th} holds the highest @{term cp}-value

   746   in state @{text s}, which means the task for @{text th} is the 

   747   most urgent. We want to show that  

   748   @{text th} is treated correctly by PIP, which means

   749   @{text th} will not be blocked unreasonably by other less urgent

   750   threads. 

   751 *}

   752 locale highest_gen =

   753   fixes s th prio tm

   754   assumes vt_s: "vt s"

   755   and threads_s: "th \<in> threads s"

   756   and highest: "preced th s = Max ((cp s)`threads s)"

   757   -- {* The internal structure of @{term th}'s precedence is exposed:*}

   758   and preced_th: "preced th s = Prc prio tm" 

   759 

   760 -- {* @{term s} is a valid trace, so it will inherit all results derived for

   761       a valid trace: *}

   762 sublocale highest_gen < vat_s: valid_trace "s"

   763   by (unfold_locales, insert vt_s, simp)

   764 

   765 context highest_gen

   766 begin

   767 

   768 text {*

   769   @{term tm} is the time when the precedence of @{term th} is set, so 

   770   @{term tm} must be a valid moment index into @{term s}.

   771 *}

   772 lemma lt_tm: "tm < length s"

   773   by (insert preced_tm_lt[OF threads_s preced_th], simp)

   774 

   775 text {*

   776   Since @{term th} holds the highest precedence and @{text "cp"}

   777   is the highest precedence of all threads in the sub-tree of 

   778   @{text "th"} and @{text th} is among these threads, 

   779   its @{term cp} must equal to its precedence:

   780 *}

   781 lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")

   782 proof -

   783   have "?L \<le> ?R"

   784   by (unfold highest, rule Max_ge, 

   785         auto simp:threads_s finite_threads)

   786   moreover have "?R \<le> ?L"

   787     by (unfold vat_s.cp_rec, rule Max_ge, 

   788         auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)

   789   ultimately show ?thesis by auto

   790 qed

   791 

   792 (* ccc *)

   793 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"

   794   by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp)

   795 

   796 lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)"

   797   by (fold eq_cp_s_th, unfold highest_cp_preced, simp)

   798 

   799 lemma highest': "cp s th = Max (cp s ` threads s)"

   800 proof -

   801   from highest_cp_preced max_cp_eq[symmetric]

   802   show ?thesis by simp

   803 qed

   804 

   805 end

   806 

   807 locale extend_highest_gen = highest_gen + 

   808   fixes t 

   809   assumes vt_t: "vt (t@s)"

   810   and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"

   811   and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"

   812   and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"

   813 

   814 sublocale extend_highest_gen < vat_t: valid_trace "t@s"

   815   by (unfold_locales, insert vt_t, simp)

   816 

   817 lemma step_back_vt_app: 

   818   assumes vt_ts: "vt (t@s)" 

   819   shows "vt s"

   820 proof -

   821   from vt_ts show ?thesis

   822   proof(induct t)

   823     case Nil

   824     from Nil show ?case by auto

   825   next

   826     case (Cons e t)

   827     assume ih: " vt (t @ s) \<Longrightarrow> vt s"

   828       and vt_et: "vt ((e # t) @ s)"

   829     show ?case

   830     proof(rule ih)

   831       show "vt (t @ s)"

   832       proof(rule step_back_vt)

   833         from vt_et show "vt (e # t @ s)" by simp

   834       qed

   835     qed

   836   qed

   837 qed

   838 

   839 

   840 locale red_extend_highest_gen = extend_highest_gen +

   841    fixes i::nat

   842 

   843 sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"

   844   apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])

   845   apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)

   846   by (unfold highest_gen_def, auto dest:step_back_vt_app)

   847 

   848 

   849 context extend_highest_gen

   850 begin

   851 

   852  lemma ind [consumes 0, case_names Nil Cons, induct type]:

   853   assumes 

   854     h0: "R []"

   855   and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e; 

   856                     extend_highest_gen s th prio tm t; 

   857                     extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"

   858   shows "R t"

   859 proof -

   860   from vt_t extend_highest_gen_axioms show ?thesis

   861   proof(induct t)

   862     from h0 show "R []" .

   863   next

   864     case (Cons e t')

   865     assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"

   866       and vt_e: "vt ((e # t') @ s)"

   867       and et: "extend_highest_gen s th prio tm (e # t')"

   868     from vt_e and step_back_step have stp: "step (t'@s) e" by auto

   869     from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto

   870     show ?case

   871     proof(rule h2 [OF vt_ts stp _ _ _ ])

   872       show "R t'"

   873       proof(rule ih)

   874         from et show ext': "extend_highest_gen s th prio tm t'"

   875           by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

   876       next

   877         from vt_ts show "vt (t' @ s)" .

   878       qed

   879     next

   880       from et show "extend_highest_gen s th prio tm (e # t')" .

   881     next

   882       from et show ext': "extend_highest_gen s th prio tm t'"

   883           by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

   884     qed

   885   qed

   886 qed

   887 

   888 

   889 lemma th_kept: "th \<in> threads (t @ s) \<and> 

   890                  preced th (t@s) = preced th s" (is "?Q t") 

   891 proof -

   892   show ?thesis

   893   proof(induct rule:ind)

   894     case Nil

   895     from threads_s

   896     show ?case

   897       by auto

   898   next

   899     case (Cons e t)

   900     interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto

   901     interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto

   902     show ?case

   903     proof(cases e)

   904       case (Create thread prio)

   905       show ?thesis

   906       proof -

   907         from Cons and Create have "step (t@s) (Create thread prio)" by auto

   908         hence "th \<noteq> thread"

   909         proof(cases)

   910           case thread_create

   911           with Cons show ?thesis by auto

   912         qed

   913         hence "preced th ((e # t) @ s)  = preced th (t @ s)"

   914           by (unfold Create, auto simp:preced_def)

   915         moreover note Cons

   916         ultimately show ?thesis

   917           by (auto simp:Create)

   918       qed

   919     next

   920       case (Exit thread)

   921       from h_e.exit_diff and Exit

   922       have neq_th: "thread \<noteq> th" by auto

   923       with Cons

   924       show ?thesis

   925         by (unfold Exit, auto simp:preced_def)

   926     next

   927       case (P thread cs)

   928       with Cons

   929       show ?thesis 

   930         by (auto simp:P preced_def)

   931     next

   932       case (V thread cs)

   933       with Cons

   934       show ?thesis 

   935         by (auto simp:V preced_def)

   936     next

   937       case (Set thread prio')

   938       show ?thesis

   939       proof -

   940         from h_e.set_diff_low and Set

   941         have "th \<noteq> thread" by auto

   942         hence "preced th ((e # t) @ s)  = preced th (t @ s)"

   943           by (unfold Set, auto simp:preced_def)

   944         moreover note Cons

   945         ultimately show ?thesis

   946           by (auto simp:Set)

   947       qed

   948     qed

   949   qed

   950 qed

   951 

   952 text {*

   953   According to @{thm th_kept}, thread @{text "th"} has its living status

   954   and precedence kept along the way of @{text "t"}. The following lemma

   955   shows that this preserved precedence of @{text "th"} remains as the highest

   956   along the way of @{text "t"}.

   957 

   958   The proof goes by induction over @{text "t"} using the specialized

   959   induction rule @{thm ind}, followed by case analysis of each possible 

   960   operations of PIP. All cases follow the same pattern rendered by the 

   961   generalized introduction rule @{thm "image_Max_eqI"}. 

   962 

   963   The very essence is to show that precedences, no matter whether they are newly introduced 

   964   or modified, are always lower than the one held by @{term "th"},

   965   which by @{thm th_kept} is preserved along the way.

   966 *}

   967 lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"

   968 proof(induct rule:ind)

   969   case Nil

   970   from highest_preced_thread

   971   show ?case

   972     by (unfold the_preced_def, simp)

   973 next

   974   case (Cons e t)

   975     interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto

   976     interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto

   977   show ?case

   978   proof(cases e)

   979     case (Create thread prio')

   980     show ?thesis (is "Max (?f ` ?A) = ?t")

   981     proof -

   982       -- {* The following is the common pattern of each branch of the case analysis. *}

   983       -- {* The major part is to show that @{text "th"} holds the highest precedence: *}

   984       have "Max (?f ` ?A) = ?f th"

   985       proof(rule image_Max_eqI)

   986         show "finite ?A" using h_e.finite_threads by auto 

   987       next

   988         show "th \<in> ?A" using h_e.th_kept by auto 

   989       next

   990         show "\<forall>x\<in>?A. ?f x \<le> ?f th"

   991         proof 

   992           fix x

   993           assume "x \<in> ?A"

   994           hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create)

   995           thus "?f x \<le> ?f th"

   996           proof

   997             assume "x = thread"

   998             thus ?thesis 

   999               apply (simp add:Create the_preced_def preced_def, fold preced_def)

  1000               using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force

  1001           next

  1002             assume h: "x \<in> threads (t @ s)"

  1003             from Cons(2)[unfolded Create] 

  1004             have "x \<noteq> thread" using h by (cases, auto)

  1005             hence "?f x = the_preced (t@s) x" 

  1006               by (simp add:Create the_preced_def preced_def)

  1007             hence "?f x \<le> Max (the_preced (t@s) ` threads (t@s))"

  1008               by (simp add: h_t.finite_threads h)

  1009             also have "... = ?f th"

  1010               by (metis Cons.hyps(5) h_e.th_kept the_preced_def) 

  1011             finally show ?thesis .

  1012           qed

  1013         qed

  1014       qed

  1015      -- {* The minor part is to show that the precedence of @{text "th"} 

  1016            equals to preserved one, given by the foregoing lemma @{thm th_kept} *}

  1017       also have "... = ?t" using h_e.th_kept the_preced_def by auto

  1018       -- {* Then it follows trivially that the precedence preserved

  1019             for @{term "th"} remains the maximum of all living threads along the way. *}

  1020       finally show ?thesis .

  1021     qed 

  1022   next 

  1023     case (Exit thread)

  1024     show ?thesis (is "Max (?f ` ?A) = ?t")

  1025     proof -

  1026       have "Max (?f ` ?A) = ?f th"

  1027       proof(rule image_Max_eqI)

  1028         show "finite ?A" using h_e.finite_threads by auto 

  1029       next

  1030         show "th \<in> ?A" using h_e.th_kept by auto 

  1031       next

  1032         show "\<forall>x\<in>?A. ?f x \<le> ?f th"

  1033         proof 

  1034           fix x

  1035           assume "x \<in> ?A"

  1036           hence "x \<in> threads (t@s)" by (simp add: Exit) 

  1037           hence "?f x \<le> Max (?f ` threads (t@s))" 

  1038             by (simp add: h_t.finite_threads) 

  1039           also have "... \<le> ?f th" 

  1040             apply (simp add:Exit the_preced_def preced_def, fold preced_def)

  1041             using Cons.hyps(5) h_t.th_kept the_preced_def by auto

  1042           finally show "?f x \<le> ?f th" .

  1043         qed

  1044       qed

  1045       also have "... = ?t" using h_e.th_kept the_preced_def by auto

  1046       finally show ?thesis .

  1047     qed 

  1048   next

  1049     case (P thread cs)

  1050     with Cons

  1051     show ?thesis by (auto simp:preced_def the_preced_def)

  1052   next

  1053     case (V thread cs)

  1054     with Cons

  1055     show ?thesis by (auto simp:preced_def the_preced_def)

  1056   next 

  1057     case (Set thread prio')

  1058     show ?thesis (is "Max (?f ` ?A) = ?t")

  1059     proof -

  1060       have "Max (?f ` ?A) = ?f th"

  1061       proof(rule image_Max_eqI)

  1062         show "finite ?A" using h_e.finite_threads by auto 

  1063       next

  1064         show "th \<in> ?A" using h_e.th_kept by auto 

  1065       next

  1066         show "\<forall>x\<in>?A. ?f x \<le> ?f th"

  1067         proof 

  1068           fix x

  1069           assume h: "x \<in> ?A"

  1070           show "?f x \<le> ?f th"

  1071           proof(cases "x = thread")

  1072             case True

  1073             moreover have "the_preced (Set thread prio' # t @ s) thread \<le> the_preced (t @ s) th"

  1074             proof -

  1075               have "the_preced (t @ s) th = Prc prio tm"  

  1076                 using h_t.th_kept preced_th by (simp add:the_preced_def)

  1077               moreover have "prio' \<le> prio" using Set h_e.set_diff_low by auto

  1078               ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def)

  1079             qed

  1080             ultimately show ?thesis

  1081               by (unfold Set, simp add:the_preced_def preced_def)

  1082           next

  1083             case False

  1084             then have "?f x  = the_preced (t@s) x"

  1085               by (simp add:the_preced_def preced_def Set)

  1086             also have "... \<le> Max (the_preced (t@s) ` threads (t@s))"

  1087               using Set h h_t.finite_threads by auto 

  1088             also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) 

  1089             finally show ?thesis .

  1090           qed

  1091         qed

  1092       qed

  1093       also have "... = ?t" using h_e.th_kept the_preced_def by auto

  1094       finally show ?thesis .

  1095     qed 

  1096   qed

  1097 qed

  1098 

  1099 lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))"

  1100   by (insert th_kept max_kept, auto)

  1101 

  1102 text {*

  1103   The reason behind the following lemma is that:

  1104   Since @{term "cp"} is defined as the maximum precedence 

  1105   of those threads contained in the sub-tree of node @{term "Th th"} 

  1106   in @{term "RAG (t@s)"}, and all these threads are living threads, and 

  1107   @{term "th"} is also among them, the maximum precedence of 

  1108   them all must be the one for @{text "th"}.

  1109 *}

  1110 lemma th_cp_max_preced: 

  1111   "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") 

  1112 proof -

  1113   let ?f = "the_preced (t@s)"

  1114   have "?L = ?f th"

  1115   proof(unfold cp_alt_def, rule image_Max_eqI)

  1116     show "finite {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

  1117     proof -

  1118       have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = 

  1119             the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and>

  1120                             (\<exists> th'. n = Th th')}"

  1121       by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps)

  1122       moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) 

  1123       ultimately show ?thesis by simp

  1124     qed

  1125   next

  1126     show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

  1127       by (auto simp:subtree_def)

  1128   next

  1129     show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}.

  1130                the_preced (t @ s) x \<le> the_preced (t @ s) th"

  1131     proof

  1132       fix th'

  1133       assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

  1134       hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto

  1135       moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}"

  1136         by (meson subtree_Field)

  1137       ultimately have "Th th' \<in> ..." by auto

  1138       hence "th' \<in> threads (t@s)" 

  1139       proof

  1140         assume "Th th' \<in> {Th th}"

  1141         thus ?thesis using th_kept by auto 

  1142       next

  1143         assume "Th th' \<in> Field (RAG (t @ s))"

  1144         thus ?thesis using vat_t.not_in_thread_isolated by blast 

  1145       qed

  1146       thus "the_preced (t @ s) th' \<le> the_preced (t @ s) th"

  1147         by (metis Max_ge finite_imageI finite_threads image_eqI 

  1148                max_kept th_kept the_preced_def)

  1149     qed

  1150   qed

  1151   also have "... = ?R" by (simp add: max_preced the_preced_def) 

  1152   finally show ?thesis .

  1153 qed

  1154 

  1155 lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))"

  1156   using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger

  1157 

  1158 lemma th_cp_preced: "cp (t@s) th = preced th s"

  1159   by (fold max_kept, unfold th_cp_max_preced, simp)

  1160 

  1161 lemma preced_less:

  1162   assumes th'_in: "th' \<in> threads s"

  1163   and neq_th': "th' \<noteq> th"

  1164   shows "preced th' s < preced th s"

  1165   using assms

  1166 by (metis Max.coboundedI finite_imageI highest not_le order.trans 

  1167     preced_linorder rev_image_eqI threads_s vat_s.finite_threads 

  1168     vat_s.le_cp)

  1169 

  1170 text {*

  1171   Counting of the number of @{term "P"} and @{term "V"} operations 

  1172   is the cornerstone of a large number of the following proofs. 

  1173   The reason is that this counting is quite easy to calculate and 

  1174   convenient to use in the reasoning. 

  1175 

  1176   The following lemma shows that the counting controls whether 

  1177   a thread is running or not.

  1178 *}

  1179 

  1180 lemma pv_blocked_pre:

  1181   assumes th'_in: "th' \<in> threads (t@s)"

  1182   and neq_th': "th' \<noteq> th"

  1183   and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"

  1184   shows "th' \<notin> runing (t@s)"

  1185 proof

  1186   assume otherwise: "th' \<in> runing (t@s)"

  1187   show False

  1188   proof -

  1189     have "th' = th"

  1190     proof(rule preced_unique)

  1191       show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")

  1192       proof -

  1193         have "?L = cp (t@s) th'"

  1194           by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)

  1195         also have "... = cp (t @ s) th" using otherwise 

  1196           by (metis (mono_tags, lifting) mem_Collect_eq 

  1197                     runing_def th_cp_max vat_t.max_cp_readys_threads)

  1198         also have "... = ?R" by (metis th_cp_preced th_kept) 

  1199         finally show ?thesis .

  1200       qed

  1201     qed (auto simp: th'_in th_kept)

  1202     moreover have "th' \<noteq> th" using neq_th' .

  1203     ultimately show ?thesis by simp

  1204  qed

  1205 qed

  1206 

  1207 lemmas pv_blocked = pv_blocked_pre[folded detached_eq]

  1208 

  1209 lemma runing_precond_pre:

  1210   fixes th'

  1211   assumes th'_in: "th' \<in> threads s"

  1212   and eq_pv: "cntP s th' = cntV s th'"

  1213   and neq_th': "th' \<noteq> th"

  1214   shows "th' \<in> threads (t@s) \<and>

  1215          cntP (t@s) th' = cntV (t@s) th'"

  1216 proof(induct rule:ind)

  1217   case (Cons e t)

  1218     interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp

  1219     interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp

  1220     show ?case

  1221     proof(cases e)

  1222       case (P thread cs)

  1223       show ?thesis

  1224       proof -

  1225         have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"

  1226         proof -

  1227           have "thread \<noteq> th'"

  1228           proof -

  1229             have "step (t@s) (P thread cs)" using Cons P by auto

  1230             thus ?thesis

  1231             proof(cases)

  1232               assume "thread \<in> runing (t@s)"

  1233               moreover have "th' \<notin> runing (t@s)" using Cons(5)

  1234                 by (metis neq_th' vat_t.pv_blocked_pre) 

  1235               ultimately show ?thesis by auto

  1236             qed

  1237           qed with Cons show ?thesis

  1238             by (unfold P, simp add:cntP_def cntV_def count_def)

  1239         qed

  1240         moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold P, simp)

  1241         ultimately show ?thesis by auto

  1242       qed

  1243     next

  1244       case (V thread cs)

  1245       show ?thesis

  1246       proof -

  1247         have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"

  1248         proof -

  1249           have "thread \<noteq> th'"

  1250           proof -

  1251             have "step (t@s) (V thread cs)" using Cons V by auto

  1252             thus ?thesis

  1253             proof(cases)

  1254               assume "thread \<in> runing (t@s)"

  1255               moreover have "th' \<notin> runing (t@s)" using Cons(5)

  1256                 by (metis neq_th' vat_t.pv_blocked_pre) 

  1257               ultimately show ?thesis by auto

  1258             qed

  1259           qed with Cons show ?thesis

  1260             by (unfold V, simp add:cntP_def cntV_def count_def)

  1261         qed

  1262         moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold V, simp)

  1263         ultimately show ?thesis by auto

  1264       qed

  1265     next

  1266       case (Create thread prio')

  1267       show ?thesis

  1268       proof -

  1269         have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"

  1270         proof -

  1271           have "thread \<noteq> th'"

  1272           proof -

  1273             have "step (t@s) (Create thread prio')" using Cons Create by auto

  1274             thus ?thesis using Cons(5) by (cases, auto)

  1275           qed with Cons show ?thesis

  1276             by (unfold Create, simp add:cntP_def cntV_def count_def)

  1277         qed

  1278         moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold Create, simp)

  1279         ultimately show ?thesis by auto

  1280       qed

  1281     next

  1282       case (Exit thread)

  1283       show ?thesis

  1284       proof -

  1285         have neq_thread: "thread \<noteq> th'"

  1286         proof -

  1287           have "step (t@s) (Exit thread)" using Cons Exit by auto

  1288           thus ?thesis apply (cases) using Cons(5)

  1289                 by (metis neq_th' vat_t.pv_blocked_pre) 

  1290         qed 

  1291         hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons

  1292             by (unfold Exit, simp add:cntP_def cntV_def count_def)

  1293         moreover have "th' \<in> threads ((e # t) @ s)" using Cons neq_thread 

  1294           by (unfold Exit, simp) 

  1295         ultimately show ?thesis by auto

  1296       qed

  1297     next

  1298       case (Set thread prio')

  1299       with Cons

  1300       show ?thesis 

  1301         by (auto simp:cntP_def cntV_def count_def)

  1302     qed

  1303 next

  1304   case Nil

  1305   with assms

  1306   show ?case by auto

  1307 qed

  1308 

  1309 text {* Changing counting balance to detachedness *}

  1310 lemmas runing_precond_pre_dtc = runing_precond_pre

  1311          [folded vat_t.detached_eq vat_s.detached_eq]

  1312 

  1313 lemma runing_precond:

  1314   fixes th'

  1315   assumes th'_in: "th' \<in> threads s"

  1316   and neq_th': "th' \<noteq> th"

  1317   and is_runing: "th' \<in> runing (t@s)"

  1318   shows "cntP s th' > cntV s th'"

  1319   using assms

  1320 proof -

  1321   have "cntP s th' \<noteq> cntV s th'"

  1322     by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in)

  1323   moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto

  1324   ultimately show ?thesis by auto

  1325 qed

  1326 

  1327 lemma moment_blocked_pre:

  1328   assumes neq_th': "th' \<noteq> th"

  1329   and th'_in: "th' \<in> threads ((moment i t)@s)"

  1330   and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"

  1331   shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \<and>

  1332          th' \<in> threads ((moment (i+j) t)@s)"

  1333 proof -

  1334   interpret h_i: red_extend_highest_gen _ _ _ _ _ i

  1335       by (unfold_locales)

  1336   interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j"

  1337       by (unfold_locales)

  1338   interpret h:  extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)"

  1339   proof(unfold_locales)

  1340     show "vt (moment i t @ s)" by (metis h_i.vt_t) 

  1341   next

  1342     show "th \<in> threads (moment i t @ s)" by (metis h_i.th_kept)

  1343   next

  1344     show "preced th (moment i t @ s) = 

  1345             Max (cp (moment i t @ s) ` threads (moment i t @ s))"

  1346               by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept)

  1347   next

  1348     show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) 

  1349   next

  1350     show "vt (moment j (restm i t) @ moment i t @ s)"

  1351       using moment_plus_split by (metis add.commute append_assoc h_j.vt_t)

  1352   next

  1353     fix th' prio'

  1354     assume "Create th' prio' \<in> set (moment j (restm i t))"

  1355     thus "prio' \<le> prio" using assms

  1356        by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append)

  1357   next

  1358     fix th' prio'

  1359     assume "Set th' prio' \<in> set (moment j (restm i t))"

  1360     thus "th' \<noteq> th \<and> prio' \<le> prio"

  1361     by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append)

  1362   next

  1363     fix th'

  1364     assume "Exit th' \<in> set (moment j (restm i t))"

  1365     thus "th' \<noteq> th"

  1366       by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append)

  1367   qed

  1368   show ?thesis 

  1369     by (metis add.commute append_assoc eq_pv h.runing_precond_pre

  1370           moment_plus_split neq_th' th'_in)

  1371 qed

  1372 

  1373 lemma moment_blocked_eqpv:

  1374   assumes neq_th': "th' \<noteq> th"

  1375   and th'_in: "th' \<in> threads ((moment i t)@s)"

  1376   and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"

  1377   and le_ij: "i \<le> j"

  1378   shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and>

  1379          th' \<in> threads ((moment j t)@s) \<and>

  1380          th' \<notin> runing ((moment j t)@s)"

  1381 proof -

  1382   from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij

  1383   have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'"

  1384    and h2: "th' \<in> threads ((moment j t)@s)" by auto

  1385   moreover have "th' \<notin> runing ((moment j t)@s)"

  1386   proof -

  1387     interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales)

  1388     show ?thesis

  1389       using h.pv_blocked_pre h1 h2 neq_th' by auto 

  1390   qed

  1391   ultimately show ?thesis by auto

  1392 qed

  1393 

  1394 (* The foregoing two lemmas are preparation for this one, but

  1395    in long run can be combined. Maybe I am wrong.

  1396 *)

  1397 lemma moment_blocked:

  1398   assumes neq_th': "th' \<noteq> th"

  1399   and th'_in: "th' \<in> threads ((moment i t)@s)"

  1400   and dtc: "detached (moment i t @ s) th'"

  1401   and le_ij: "i \<le> j"

  1402   shows "detached (moment j t @ s) th' \<and>

  1403          th' \<in> threads ((moment j t)@s) \<and>

  1404          th' \<notin> runing ((moment j t)@s)"

  1405 proof -

  1406   interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales)

  1407   interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) 

  1408   have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'"

  1409                 by (metis dtc h_i.detached_elim)

  1410   from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij]

  1411   show ?thesis by (metis h_j.detached_intro) 

  1412 qed

  1413 

  1414 lemma runing_preced_inversion:

  1415   assumes runing': "th' \<in> runing (t@s)"

  1416   shows "cp (t@s) th' = preced th s" (is "?L = ?R")

  1417 proof -

  1418   have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms

  1419       by (unfold runing_def, auto)

  1420   also have "\<dots> = ?R"

  1421       by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 

  1422   finally show ?thesis .

  1423 qed

  1424 

  1425 text {*

  1426   The situation when @{term "th"} is blocked is analyzed by the following lemmas.

  1427 *}

  1428 

  1429 text {*

  1430   The following lemmas shows the running thread @{text "th'"}, if it is different from

  1431   @{term th}, must be live at the very beginning. By the term {\em the very beginning},

  1432   we mean the moment where the formal investigation starts, i.e. the moment (or state)

  1433   @{term s}. 

  1434 *}

  1435 

  1436 lemma runing_inversion_0:

  1437   assumes neq_th': "th' \<noteq> th"

  1438   and runing': "th' \<in> runing (t@s)"

  1439   shows "th' \<in> threads s"

  1440 proof -

  1441     -- {* The proof is by contradiction: *}

  1442     { assume otherwise: "\<not> ?thesis"

  1443       have "th' \<notin> runing (t @ s)"

  1444       proof -

  1445         -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *}

  1446         have th'_in: "th' \<in> threads (t@s)" using runing' by (simp add:runing_def readys_def)

  1447         -- {* However, @{text "th'"} does not exist at very beginning. *}

  1448         have th'_notin: "th' \<notin> threads (moment 0 t @ s)" using otherwise

  1449           by (metis append.simps(1) moment_zero)

  1450         -- {* Therefore, there must be a moment during @{text "t"}, when 

  1451               @{text "th'"} came into being. *}

  1452         -- {* Let us suppose the moment being @{text "i"}: *}

  1453         from p_split_gen[OF th'_in th'_notin]

  1454         obtain i where lt_its: "i < length t"

  1455                  and le_i: "0 \<le> i"

  1456                  and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre")

  1457                  and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by (auto)

  1458         interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales)

  1459         interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales)

  1460         from lt_its have "Suc i \<le> length t" by auto

  1461         -- {* Let us also suppose the event which makes this change is @{text e}: *}

  1462         from moment_head[OF this] obtain e where 

  1463           eq_me: "moment (Suc i) t = e # moment i t" by blast

  1464         hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) 

  1465         hence "PIP (moment i t @ s) e" by (cases, simp)

  1466         -- {* It can be derived that this event @{text "e"}, which 

  1467               gives birth to @{term "th'"} must be a @{term "Create"}: *}

  1468         from create_pre[OF this, of th']

  1469         obtain prio where eq_e: "e = Create th' prio"

  1470             by (metis append_Cons eq_me lessI post pre) 

  1471         have h1: "th' \<in> threads (moment (Suc i) t @ s)" using post by auto 

  1472         have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'"

  1473         proof -

  1474           have "cntP (moment i t@s) th' = cntV (moment i t@s) th'"

  1475             by (metis h_i.cnp_cnv_eq pre)

  1476           thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def)

  1477         qed

  1478         show ?thesis 

  1479           using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge

  1480             by auto

  1481       qed

  1482       with `th' \<in> runing (t@s)`

  1483       have False by simp

  1484     } thus ?thesis by auto

  1485 qed

  1486 

  1487 text {* 

  1488   The second lemma says, if the running thread @{text th'} is different from 

  1489   @{term th}, then this @{text th'} must in the possession of some resources

  1490   at the very beginning. 

  1491 

  1492   To ease the reasoning of resource possession of one particular thread, 

  1493   we used two auxiliary functions @{term cntV} and @{term cntP}, 

  1494   which are the counters of @{term P}-operations and 

  1495   @{term V}-operations respectively. 

  1496   If the number of @{term V}-operation is less than the number of 

  1497   @{term "P"}-operations, the thread must have some unreleased resource. 

  1498 *}

  1499 

  1500 lemma runing_inversion_1: (* ddd *)

  1501   assumes neq_th': "th' \<noteq> th"

  1502   and runing': "th' \<in> runing (t@s)"

  1503   -- {* thread @{term "th'"} is a live on in state @{term "s"} and 

  1504         it has some unreleased resource. *}

  1505   shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"

  1506 proof -

  1507   -- {* The proof is a simple composition of @{thm runing_inversion_0} and 

  1508         @{thm runing_precond}: *}

  1509   -- {* By applying @{thm runing_inversion_0} to assumptions,

  1510         it can be shown that @{term th'} is live in state @{term s}: *}

  1511   have "th' \<in> threads s"  using runing_inversion_0[OF assms(1,2)] .

  1512   -- {* Then the thesis is derived easily by applying @{thm runing_precond}: *}

  1513   with runing_precond [OF this neq_th' runing'] show ?thesis by simp

  1514 qed

  1515 

  1516 text {* 

  1517   The following lemma is just a rephrasing of @{thm runing_inversion_1}:

  1518 *}

  1519 lemma runing_inversion_2:

  1520   assumes runing': "th' \<in> runing (t@s)"

  1521   shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"

  1522 proof -

  1523   from runing_inversion_1[OF _ runing']

  1524   show ?thesis by auto

  1525 qed

  1526 

  1527 lemma runing_inversion_3:

  1528   assumes runing': "th' \<in> runing (t@s)"

  1529   and neq_th: "th' \<noteq> th"

  1530   shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)"

  1531   by (metis neq_th runing' runing_inversion_2 runing_preced_inversion)

  1532 

  1533 lemma runing_inversion_4:

  1534   assumes runing': "th' \<in> runing (t@s)"

  1535   and neq_th: "th' \<noteq> th"

  1536   shows "th' \<in> threads s"

  1537   and    "\<not>detached s th'"

  1538   and    "cp (t@s) th' = preced th s"

  1539   apply (metis neq_th runing' runing_inversion_2)

  1540   apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc)

  1541   by (metis neq_th runing' runing_inversion_3)

  1542 

  1543 

  1544 text {* 

  1545   Suppose @{term th} is not running, it is first shown that

  1546   there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 

  1547   in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).

  1548 

  1549   Now, since @{term readys}-set is non-empty, there must be

  1550   one in it which holds the highest @{term cp}-value, which, by definition, 

  1551   is the @{term runing}-thread. However, we are going to show more: this running thread

  1552   is exactly @{term "th'"}.

  1553      *}

  1554 lemma th_blockedE: (* ddd *)

  1555   assumes "th \<notin> runing (t@s)"

  1556   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"

  1557                     "th' \<in> runing (t@s)"

  1558 proof -

  1559   -- {* According to @{thm vat_t.th_chain_to_ready}, either 

  1560         @{term "th"} is in @{term "readys"} or there is path leading from it to 

  1561         one thread in @{term "readys"}. *}

  1562   have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" 

  1563     using th_kept vat_t.th_chain_to_ready by auto

  1564   -- {* However, @{term th} can not be in @{term readys}, because otherwise, since 

  1565        @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}

  1566   moreover have "th \<notin> readys (t@s)" 

  1567     using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto 

  1568   -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in 

  1569         term @{term readys}: *}

  1570   ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"

  1571                           and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto

  1572   -- {* We are going to show that this @{term th'} is running. *}

  1573   have "th' \<in> runing (t@s)"

  1574   proof -

  1575     -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}

  1576     have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")

  1577     proof -

  1578       have "?L =  Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"

  1579         by (unfold cp_alt_def1, simp)

  1580       also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"

  1581       proof(rule image_Max_subset)

  1582         show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)

  1583       next

  1584         show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)"

  1585           by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) 

  1586       next

  1587         show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp

  1588                     by (unfold tRAG_subtree_eq, auto simp:subtree_def)

  1589       next

  1590         show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =

  1591                       (the_preced (t @ s) \<circ> the_thread) (Th th)" (is "Max ?L = _")

  1592         proof -

  1593           have "?L = the_preced (t @ s) `  threads (t @ s)" 

  1594                      by (unfold image_comp, rule image_cong, auto)

  1595           thus ?thesis using max_preced the_preced_def by auto

  1596         qed

  1597       qed

  1598       also have "... = ?R"

  1599         using th_cp_max th_cp_preced th_kept 

  1600               the_preced_def vat_t.max_cp_readys_threads by auto

  1601       finally show ?thesis .

  1602     qed 

  1603     -- {* Now, since @{term th'} holds the highest @{term cp} 

  1604           and we have already show it is in @{term readys},

  1605           it is @{term runing} by definition. *}

  1606     with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def) 

  1607   qed

  1608   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}

  1609   moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 

  1610     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)

  1611   ultimately show ?thesis using that by metis

  1612 qed

  1613 

  1614 text {*

  1615   Now it is easy to see there is always a thread to run by case analysis

  1616   on whether thread @{term th} is running: if the answer is Yes, the 

  1617   the running thread is obviously @{term th} itself; otherwise, the running

  1618   thread is the @{text th'} given by lemma @{thm th_blockedE}.

  1619 *}

  1620 lemma live: "runing (t@s) \<noteq> {}"

  1621 proof(cases "th \<in> runing (t@s)") 

  1622   case True thus ?thesis by auto

  1623 next

  1624   case False

  1625   thus ?thesis using th_blockedE by auto

  1626 qed

  1627 

  1628 end

  1629 end

  1630 

  1631 

  1632 

  1633 >>>>>>> other