Mercurial Mercurial > hg > pip / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PrioG.thy
changeset 53 8142e80f5d58
parent 44 f676a68935a0
child 55 b85cfbd58f59
equal deleted inserted replaced
49:8679d75b1d76 53:8142e80f5d58 
    49       thus "distinct q" by auto
 
    49       thus "distinct q" by auto
 
    50     qed
 
    50     qed
 
    51   qed
 
    51   qed
 
    52 qed
 
    52 qed
 
    53 
    53 
    54 lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"
 
    54 text {*
 
    55   by(ind_cases "vt (e#s)", simp)
 
    55   The following lemma shows that only the @{text "P"}
 
    56 
    56   operation can add new thread into waiting queues. 
    57 lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"
 
    57   Such kind of lemmas are very obvious, but need to be checked formally.
 
    58   by(ind_cases "vt (e#s)", simp)
 
    58   This is a kind of confirmation that our modelling is correct.
 
       
    59 *}
 
    59 
    60 
    60 lemma block_pre: 
    61 lemma block_pre: 
    61   fixes thread cs s
 
    62   fixes thread cs s
 
    62   assumes vt_e: "vt (e#s)"
 
    63   assumes vt_e: "vt (e#s)"
 
    63   and s_ni: "thread \<notin>  set (wq s cs)"
 
    64   and s_ni: "thread \<notin>  set (wq s cs)"
 
   108       qed
 
   109       qed
 
   109       ultimately show "False" by auto
 
   110       ultimately show "False" by auto
 
   110       qed
 
   111       qed
 
   111   qed
 
   112   qed
 
   112 qed
 
   113 qed
 
       
   114 
       
   115 text {*
 
       
   116   The following lemmas is also obvious and shallow. It says
 
       
   117   that only running thread can request for a critical resource 
       
   118   and that the requested resource must be one which is
 
       
   119   not current held by the thread.
 
       
   120 *}
 
   113 
   121 
   114 lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow> 
   122 lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow> 
   115   thread \<in> runing s \<and> (Cs cs, Th thread)  \<notin> (RAG s)^+"
 
   123   thread \<in> runing s \<and> (Cs cs, Th thread)  \<notin> (RAG s)^+"
 
   116 apply (ind_cases "vt ((P thread cs)#s)")
 
   124 apply (ind_cases "vt ((P thread cs)#s)")
 
   117 apply (ind_cases "step s (P thread cs)")
 
   125 apply (ind_cases "step s (P thread cs)")
 
   199 qed
 
   207 qed
 
   200 
   208 
   201 (* Wrong:
 
   209 (* Wrong:
 
   202     lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
 
   210     lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
 
   203 *)
 
   211 *)
 
       
   212 
       
   213 text {* (* ??? *)
 
       
   214   The nature of the work is like this: since it starts from a very simple and basic 
       
   215   model, even intuitively very `basic` and `obvious` properties need to derived from scratch.
 
       
   216   For instance, the fact 
       
   217   that one thread can not be blocked by two critical resources at the same time
 
       
   218   is obvious, because only running threads can make new requests, if one is waiting for 
       
   219   a critical resource and get blocked, it can not make another resource request and get 
       
   220   blocked the second time (because it is not running). 
       
   221 
       
   222   To derive this fact, one needs to prove by contraction and 
       
   223   reason about time (or @{text "moement"}). The reasoning is based on a generic theorem
 
       
   224   named @{text "p_split"}, which is about status changing along the time axis. It says if 
       
   225   a condition @{text "Q"} is @{text "True"} at a state @{text "s"},
 
       
   226   but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"} 
       
   227   in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history 
       
   228   of events leading to it), such that @{text "Q"} switched 
       
   229   from being @{text "False"} to @{text "True"} and kept being @{text "True"}
 
       
   230   till the last moment of @{text "s"}.
 
       
   231 
       
   232   Suppose a thread @{text "th"} is blocked
 
       
   233   on @{text "cs1"} and @{text "cs2"} in some state @{text "s"}, 
       
   234   since no thread is blocked at the very beginning, by applying 
       
   235   @{text "p_split"} to these two blocking facts, there exist 
       
   236   two moments @{text "t1"} and @{text "t2"}  in @{text "s"}, such that 
       
   237   @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} 
       
   238   and kept on blocked on them respectively ever since.
 
       
   239  
       
   240   Without lose of generality, we assume @{text "t1"} is earlier than @{text "t2"}.
 
       
   241   However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still
 
       
   242   in blocked state at moment @{text "t2"} and could not
 
       
   243   make any request and get blocked the second time: Contradiction.
 
       
   244 *}
 
   204 
   245 
   205 lemma waiting_unique_pre:
 
   246 lemma waiting_unique_pre:
 
   206   fixes cs1 cs2 s thread
 
   247   fixes cs1 cs2 s thread
 
   207   assumes vt: "vt s"
 
   248   assumes vt: "vt s"
 
   208   and h11: "thread \<in> set (wq s cs1)"
 
   249   and h11: "thread \<in> set (wq s cs1)"
 
   250       have ?thesis
 
   291       have ?thesis
 
   251       proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
 
   292       proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
 
   252         case True
 
   293         case True
 
   253         from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
 
   294         from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
 
   254           by auto
 
   295           by auto
 
       
   296           thm abs2
 
   255         from abs2 [OF vt_e True eq_th h2 h1]
 
   297         from abs2 [OF vt_e True eq_th h2 h1]
 
   256         show ?thesis by auto
 
   298         show ?thesis by auto
 
   257       next
 
   299       next
 
   258         case False
 
   300         case False
 
   259         from block_pre [OF vt_e False h1]
 
   301         from block_pre [OF vt_e False h1]
 
   352       qed
 
   394       qed
 
   353     } ultimately show ?thesis by arith
 
   395     } ultimately show ?thesis by arith
 
   354   qed
 
   396   qed
 
   355 qed
 
   397 qed
 
   356 
   398 
       
   399 text {*
 
       
   400   This lemma is a simple corrolary of @{text "waiting_unique_pre"}.
 
       
   401 *}
 
       
   402 
   357 lemma waiting_unique:
 
   403 lemma waiting_unique:
 
   358   fixes s cs1 cs2
 
   404   fixes s cs1 cs2
 
   359   assumes "vt s"
 
   405   assumes "vt s"
 
   360   and "waiting s th cs1"
 
   406   and "waiting s th cs1"
 
   361   and "waiting s th cs2"
 
   407   and "waiting s th cs2"
 
   363 using waiting_unique_pre assms
 
   409 using waiting_unique_pre assms
 
   364 unfolding wq_def s_waiting_def
 
   410 unfolding wq_def s_waiting_def
 
   365 by auto
 
   411 by auto
 
   366 
   412 
   367 (* not used *)
 
   413 (* not used *)
 
       
   414 text {*
 
       
   415   Every thread can only be blocked on one critical resource, 
       
   416   symmetrically, every critical resource can only be held by one thread. 
       
   417   This fact is much more easier according to our definition. 
       
   418 *}
 
   368 lemma held_unique:
 
   419 lemma held_unique:
 
   369   fixes s::"state"
 
   420   fixes s::"state"
 
   370   assumes "holding s th1 cs"
 
   421   assumes "holding s th1 cs"
 
   371   and "holding s th2 cs"
 
   422   and "holding s th2 cs"
 
   372   shows "th1 = th2"
 
   423   shows "th1 = th2"
 
   405   from preced_unique [OF _ th_in1 th_in2] and neq_12 
   456   from preced_unique [OF _ th_in1 th_in2] and neq_12 
   406   have "preced th1 s \<noteq> preced th2 s" by auto
 
   457   have "preced th1 s \<noteq> preced th2 s" by auto
 
   407   thus ?thesis by auto
 
   458   thus ?thesis by auto
 
   408 qed
 
   459 qed
 
   409 
   460 
       
   461 (* An aux lemma used later *)
 
   410 lemma unique_minus:
 
   462 lemma unique_minus:
 
   411   fixes x y z r
 
   463   fixes x y z r
 
   412   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
 
   464   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
 
   413   and xy: "(x, y) \<in> r"
 
   465   and xy: "(x, y) \<in> r"
 
   414   and xz: "(x, z) \<in> r^+"
 
   466   and xz: "(x, z) \<in> r^+"
 
   499       qed
 
   551       qed
 
   500     qed
 
   552     qed
 
   501   qed
 
   553   qed
 
   502 qed
 
   554 qed
 
   503 
   555 
       
   556 text {*
 
       
   557   The following three lemmas show that @{text "RAG"} does not change
 
       
   558   by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"}
 
       
   559   events, respectively.
 
       
   560 *}
 
       
   561 
   504 lemma RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s"
 
   562 lemma RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s"
 
   505 apply (unfold s_RAG_def s_waiting_def wq_def)
 
   563 apply (unfold s_RAG_def s_waiting_def wq_def)
 
   506 by (simp add:Let_def)
 
   564 by (simp add:Let_def)
 
   507 
   565 
   508 lemma RAG_create_unchanged: "(RAG (Create th prio # s)) = RAG s"
 
   566 lemma RAG_create_unchanged: "(RAG (Create th prio # s)) = RAG s"
 
   512 lemma RAG_exit_unchanged: "(RAG (Exit th # s)) = RAG s"
 
   570 lemma RAG_exit_unchanged: "(RAG (Exit th # s)) = RAG s"
 
   513 apply (unfold s_RAG_def s_waiting_def wq_def)
 
   571 apply (unfold s_RAG_def s_waiting_def wq_def)
 
   514 by (simp add:Let_def)
 
   572 by (simp add:Let_def)
 
   515 
   573 
   516 
   574 
   517 
   575 text {* 
       
   576   The following lemmas are used in the proof of 
       
   577   lemma @{text "step_RAG_v"}, which characterizes how the @{text "RAG"} is changed
 
       
   578   by @{text "V"}-events. 
       
   579   However, since our model is very concise, such  seemingly obvious lemmas need to be derived from scratch,
 
       
   580   starting from the model definitions.
 
       
   581 *}
 
   518 lemma step_v_hold_inv[elim_format]:
 
   582 lemma step_v_hold_inv[elim_format]:
 
   519   "\<And>c t. \<lbrakk>vt (V th cs # s); 
   583   "\<And>c t. \<lbrakk>vt (V th cs # s); 
   520   \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> next_th s th cs t \<and> c = cs"
 
   584           \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> 
       
   585             next_th s th cs t \<and> c = cs"
 
   521 proof -
 
   586 proof -
 
   522   fix c t
 
   587   fix c t
 
   523   assume vt: "vt (V th cs # s)"
 
   588   assume vt: "vt (V th cs # s)"
 
   524     and nhd: "\<not> holding (wq s) t c"
 
   589     and nhd: "\<not> holding (wq s) t c"
 
   525     and hd: "holding (wq (V th cs # s)) t c"
 
   590     and hd: "holding (wq (V th cs # s)) t c"
 
   562     qed
 
   627     qed
 
   563     with True show ?thesis by auto
 
   628     with True show ?thesis by auto
 
   564   qed
 
   629   qed
 
   565 qed
 
   630 qed
 
   566 
   631 
       
   632 text {* 
       
   633   The following @{text "step_v_wait_inv"} is also an obvious lemma, which, however, needs to be
 
       
   634   derived from scratch, which confirms the correctness of the definition of @{text "next_th"}.
 
       
   635 *}
 
   567 lemma step_v_wait_inv[elim_format]:
 
   636 lemma step_v_wait_inv[elim_format]:
 
   568     "\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
 
   637     "\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
 
   569            \<rbrakk>
 
   638            \<rbrakk>
 
   570           \<Longrightarrow> (next_th s th cs t \<and> cs = c)"
 
   639           \<Longrightarrow> (next_th s th cs t \<and> cs = c)"
 
   571 proof -
 
   640 proof -
 
   771       show False by auto
 
   840       show False by auto
 
   772     qed
 
   841     qed
 
   773   qed
 
   842   qed
 
   774 qed
 
   843 qed
 
   775 
   844 
       
   845 text {* (* ??? *) 
       
   846   The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed
 
       
   847   with the happening of @{text "V"}-events:
 
       
   848 *}
 
   776 lemma step_RAG_v:
 
   849 lemma step_RAG_v:
 
   777 fixes th::thread
 
   850 fixes th::thread
 
   778 assumes vt:
 
   851 assumes vt:
 
   779   "vt (V th cs#s)"
 
   852   "vt (V th cs#s)"
 
   780 shows "
 
   853 shows "
 
   788               step_v_release step_v_wait_inv
 
   861               step_v_release step_v_wait_inv
 
   789               step_v_get_hold step_v_release_inv)
 
   862               step_v_get_hold step_v_release_inv)
 
   790   apply (erule_tac step_v_not_wait, auto)
 
   863   apply (erule_tac step_v_not_wait, auto)
 
   791   done
 
   864   done
 
   792 
   865 
       
   866 text {* 
       
   867   The following @{text "step_RAG_p"} lemma charaterizes how @{text "RAG"} is changed
 
       
   868   with the happening of @{text "P"}-events:
 
       
   869 *}
 
   793 lemma step_RAG_p:
 
   870 lemma step_RAG_p:
 
   794   "vt (P th cs#s) \<Longrightarrow>
 
   871   "vt (P th cs#s) \<Longrightarrow>
 
   795   RAG (P th cs # s) =  (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}
 
   872   RAG (P th cs # s) =  (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}
 
   796                                              else RAG s \<union> {(Th th, Cs cs)})"
 
   873                                              else RAG s \<union> {(Th th, Cs cs)})"
 
   797   apply(simp only: s_RAG_def wq_def)
 
   874   apply(simp only: s_RAG_def wq_def)
 
   806 
   883 
   807 
   884 
   808 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
 
   885 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
 
   809   by (unfold s_RAG_def, auto)
 
   886   by (unfold s_RAG_def, auto)
 
   810 
   887 
       
   888 text {*
 
       
   889   The following lemma shows that @{text "RAG"} is acyclic.
 
       
   890   The overall structure is by induction on the formation of @{text "vt s"}
 
       
   891   and then case analysis on event @{text "e"}, where the non-trivial cases 
       
   892   for those for @{text "V"} and @{text "P"} events.
 
       
   893 *}
 
   811 lemma acyclic_RAG: 
   894 lemma acyclic_RAG: 
   812   fixes s
 
   895   fixes s
 
   813   assumes vt: "vt s"
 
   896   assumes vt: "vt s"
 
   814   shows "acyclic (RAG s)"
 
   897   shows "acyclic (RAG s)"
 
   815 using assms
 
   898 using assms
 
  1216       qed
 
  1299       qed
 
  1217       with th_nin th_in show False by auto
 
  1300       with th_nin th_in show False by auto
 
  1218     qed
 
  1301     qed
 
  1219 qed
 
  1302 qed
 
  1220 
  1303 
       
  1304 text {* \noindent
 
       
  1305   The following lemmas shows that: starting from any node in @{text "RAG"}, 
       
  1306   by chasing out-going edges, it is always possible to reach a node representing a ready
 
       
  1307   thread. In this lemma, it is the @{text "th'"}.
 
       
  1308 *}
 
       
  1309 
  1221 lemma chain_building:
 
  1310 lemma chain_building:
 
  1222   assumes vt: "vt s"
 
  1311   assumes vt: "vt s"
 
  1223   shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
 
  1312   shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
 
  1224 proof -
 
  1313 proof -
 
  1225   from wf_dep_converse [OF vt]
 
  1314   from wf_dep_converse [OF vt]
 
  1267       qed
 
  1356       qed
 
  1268     qed
 
  1357     qed
 
  1269   qed
 
  1358   qed
 
  1270 qed
 
  1359 qed
 
  1271 
  1360 
       
  1361 text {* \noindent
 
       
  1362   The following is just an instance of @{text "chain_building"}.
 
       
  1363 *}
 
  1272 lemma th_chain_to_ready:
 
  1364 lemma th_chain_to_ready:
 
  1273   fixes s th
 
  1365   fixes s th
 
  1274   assumes vt: "vt s"
 
  1366   assumes vt: "vt s"
 
  1275   and th_in: "th \<in> threads s"
 
  1367   and th_in: "th \<in> threads s"
 
  1276   shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
 
  1368   shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
 
  1449   qed
 
  1541   qed
 
  1450   moreover from cs_not_in 
  1542   moreover from cs_not_in 
  1451   have "cs \<notin> (holdents (V thread cs#s) thread)" by auto
 
  1543   have "cs \<notin> (holdents (V thread cs#s) thread)" by auto
 
  1452   ultimately show ?thesis by (simp add:cntCS_def)
 
  1544   ultimately show ?thesis by (simp add:cntCS_def)
 
  1453 qed 
  1545 qed 
       
  1546 
       
  1547 text {* (* ??? *) \noindent
 
       
  1548   The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} 
       
  1549   of one particular thread. 
       
  1550 *} 
  1454 
  1551 
  1455 lemma cnp_cnv_cncs:
 
  1552 lemma cnp_cnv_cncs:
 
  1456   fixes s th
 
  1553   fixes s th
 
  1457   assumes vt: "vt s"
 
  1554   assumes vt: "vt s"
 
  1458   shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s) 
  1555   shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s) 
  2292 apply(simp)
 
  2389 apply(simp)
 
  2293 apply(auto)[1]
 
  2390 apply(auto)[1]
 
  2294 apply (metis insertCI runing_unique)
 
  2391 apply (metis insertCI runing_unique)
 
  2295 apply(auto) 
  2392 apply(auto) 
  2296 done
 
  2393 done
 
  2297   
       
  2298 
       
  2299 
  2394 
  2300 lemma create_pre:
 
  2395 lemma create_pre:
 
  2301   assumes stp: "step s e"
 
  2396   assumes stp: "step s e"
 
  2302   and not_in: "th \<notin> threads s"
 
  2397   and not_in: "th \<notin> threads s"
 
  2303   and is_in: "th \<in> threads (e#s)"
 
  2398   and is_in: "th \<in> threads (e#s)"
 
  2358 lemma cnp_cnv_eq:
 
  2453 lemma cnp_cnv_eq:
 
  2359   fixes th s
 
  2454   fixes th s
 
  2360   assumes "vt s"
 
  2455   assumes "vt s"
 
  2361   and "th \<notin> threads s"
 
  2456   and "th \<notin> threads s"
 
  2362   shows "cntP s th = cntV s th"
 
  2457   shows "cntP s th = cntV s th"
 
  2363 proof -
 
  2458  by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
 
  2364   from assms show ?thesis
 
       
  2365   proof(induct)
 
       
  2366     case (vt_cons s e)
 
       
  2367     have ih: "th \<notin> threads s \<Longrightarrow> cntP s th = cntV s th" by fact
 
       
  2368     have not_in: "th \<notin> threads (e # s)" by fact
 
       
  2369     have "step s e" by fact
 
       
  2370     thus ?case proof(cases)
 
       
  2371       case (thread_create thread prio)
 
       
  2372       assume eq_e: "e = Create thread prio"
 
       
  2373       hence "thread \<in> threads (e#s)" by simp
 
       
  2374       with not_in and eq_e have "th \<notin> threads s" by auto
 
       
  2375       from ih [OF this] show ?thesis using eq_e
 
       
  2376         by (auto simp:cntP_def cntV_def count_def)
 
       
  2377     next
 
       
  2378       case (thread_exit thread)
 
       
  2379       assume eq_e: "e = Exit thread"
 
       
  2380         and not_holding: "holdents s thread = {}"
 
       
  2381       have vt_s: "vt s" by fact
 
       
  2382       from finite_holding[OF vt_s] have "finite (holdents s thread)" .
 
       
  2383       with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto)
 
       
  2384       moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def)
 
       
  2385       moreover note cnp_cnv_cncs[OF vt_s, of thread]
 
       
  2386       ultimately have eq_thread: "cntP s thread = cntV s thread" by auto
 
       
  2387       show ?thesis
 
       
  2388       proof(cases "th = thread")
 
       
  2389         case True
 
       
  2390         with eq_thread eq_e show ?thesis 
       
  2391           by (auto simp:cntP_def cntV_def count_def)
 
       
  2392       next
 
       
  2393         case False
 
       
  2394         with not_in and eq_e have "th \<notin> threads s" by simp
 
       
  2395         from ih[OF this] and eq_e show ?thesis 
       
  2396            by (auto simp:cntP_def cntV_def count_def)
 
       
  2397       qed
 
       
  2398     next
 
       
  2399       case (thread_P thread cs)
 
       
  2400       assume eq_e: "e = P thread cs"
 
       
  2401       have "thread \<in> runing s" by fact
 
       
  2402       with not_in eq_e have neq_th: "thread \<noteq> th" 
       
  2403         by (auto simp:runing_def readys_def)
 
       
  2404       from not_in eq_e have "th \<notin> threads s" by simp
 
       
  2405       from ih[OF this] and neq_th and eq_e show ?thesis
 
       
  2406         by (auto simp:cntP_def cntV_def count_def)
 
       
  2407     next
 
       
  2408       case (thread_V thread cs)
 
       
  2409       assume eq_e: "e = V thread cs"
 
       
  2410       have "thread \<in> runing s" by fact
 
       
  2411       with not_in eq_e have neq_th: "thread \<noteq> th" 
       
  2412         by (auto simp:runing_def readys_def)
 
       
  2413       from not_in eq_e have "th \<notin> threads s" by simp
 
       
  2414       from ih[OF this] and neq_th and eq_e show ?thesis
 
       
  2415         by (auto simp:cntP_def cntV_def count_def)
 
       
  2416     next
 
       
  2417       case (thread_set thread prio)
 
       
  2418       assume eq_e: "e = Set thread prio"
 
       
  2419         and "thread \<in> runing s"
 
       
  2420       hence "thread \<in> threads (e#s)" 
       
  2421         by (simp add:runing_def readys_def)
 
       
  2422       with not_in and eq_e have "th \<notin> threads s" by auto
 
       
  2423       from ih [OF this] show ?thesis using eq_e
 
       
  2424         by (auto simp:cntP_def cntV_def count_def)  
       
  2425     qed
 
       
  2426   next
 
       
  2427     case vt_nil
 
       
  2428     show ?case by (auto simp:cntP_def cntV_def count_def)
 
       
  2429   qed
 
       
  2430 qed
 
       
  2431 
  2459 
  2432 lemma eq_RAG: 
  2460 lemma eq_RAG: 
  2433   "RAG (wq s) = RAG s"
 
  2461   "RAG (wq s) = RAG s"
 
  2434 by (unfold cs_RAG_def s_RAG_def, auto)
 
  2462 by (unfold cs_RAG_def s_RAG_def, auto)
 
  2435 
  2463 
  2762       qed 
  2790       qed 
  2763     qed
 
  2791     qed
 
  2764   qed
 
  2792   qed
 
  2765 qed
 
  2793 qed
 
  2766 
  2794 
       
  2795 text {* (* ccc *) \noindent
 
       
  2796   Since the current precedence of the threads in ready queue will always be boosted,
 
       
  2797   there must be one inside it has the maximum precedence of the whole system. 
       
  2798 *}
 
  2767 lemma max_cp_readys_threads:
 
  2799 lemma max_cp_readys_threads:
 
  2768   assumes vt: "vt s"
 
  2800   assumes vt: "vt s"
 
  2769   shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
 
  2801   shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
 
  2770 proof(cases "threads s = {}")
 
  2802 proof(cases "threads s = {}")
 
  2771   case True
 
  2803   case True
 
  2878   fixes s th
 
  2910   fixes s th
 
  2879   assumes vt: "vt s"
 
  2911   assumes vt: "vt s"
 
  2880   shows "(detached s th) = (cntP s th = cntV s th)"
 
  2912   shows "(detached s th) = (cntP s th = cntV s th)"
 
  2881   by (insert vt, auto intro:detached_intro detached_elim)
 
  2913   by (insert vt, auto intro:detached_intro detached_elim)
 
  2882 
  2914 
       
  2915 text {* 
       
  2916   The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived
 
       
  2917   from the concise and miniature model of PIP given in PrioGDef.thy.
 
       
  2918 *}
 
       
  2919 
  2883 end
 
  2920 end
pip