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.
CpsG.thy
changeset 55 b85cfbd58f59
parent 53 8142e80f5d58
child 56 0fd478e14e87
equal deleted inserted replaced
54:fee01b2858a2 55:b85cfbd58f59 
     4 *}
 
     4 *}
 
     5 theory CpsG
 
     5 theory CpsG
 
     6 imports PrioG Max
 
     6 imports PrioG Max
 
     7 begin
 
     7 begin
 
     8 
     8 
       
     9 lemma eq_dependants: "dependants (wq s) = dependants s"
 
       
    10   by (simp add: s_dependants_abv wq_def)
 
       
    11   
     9 (* obvious lemma *)
 
    12 (* obvious lemma *)
 
    10 lemma not_thread_holdents:
 
    13 lemma not_thread_holdents:
 
    11   fixes th s
 
    14   fixes th s
 
    12   assumes vt: "vt s"
 
    15   assumes vt: "vt s"
 
    13   and not_in: "th \<notin> threads s" 
    16   and not_in: "th \<notin> threads s" 
   310     moreover have "(n1, y) \<in> (RAG s)^+" by fact
 
   313     moreover have "(n1, y) \<in> (RAG s)^+" by fact
 
   311     ultimately show ?case by auto
 
   314     ultimately show ?case by auto
 
   312   qed
 
   315   qed
 
   313 qed
 
   316 qed
 
   314 
   317 
   315 text {* (* ??? *)
 
   318 text {* (* ddd *)
 
   316 *}
 
   319 *}
 
   317 lemma child_RAG_eq: 
   320 lemma child_RAG_eq: 
   318   assumes vt: "vt s"
 
   321   assumes vt: "vt s"
 
   319   shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
 
   322   shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
 
   320   by (auto intro: RAG_child[OF vt] child_RAG_p)
 
   323   by (auto intro: RAG_child[OF vt] child_RAG_p)
 
   321 
   324 
   322 text {* (* ??? *)
 
   325 text {* (* ddd *)
 
   323 *}
 
   326 *}
 
   324 lemma children_no_dep:
 
   327 lemma children_no_dep:
 
   325   fixes s th th1 th2 th3
 
   328   fixes s th th1 th2 th3
 
   326   assumes vt: "vt s"
 
   329   assumes vt: "vt s"
 
   327   and ch1: "(Th th1, Th th) \<in> child s"
 
   330   and ch1: "(Th th1, Th th) \<in> child s"
 
   352     qed
 
   355     qed
 
   353     ultimately show False by auto
 
   356     ultimately show False by auto
 
   354   qed
 
   357   qed
 
   355 qed
 
   358 qed
 
   356 
   359 
   357 text {* (* ??? *)
 
   360 text {* (* ddd *)
 
   358 *}
 
   361 *}
 
   359 lemma unique_RAG_p:
 
   362 lemma unique_RAG_p:
 
   360   assumes vt: "vt s"
 
   363   assumes vt: "vt s"
 
   361   and dp1: "(n, n1) \<in> (RAG s)^+"
 
   364   and dp1: "(n, n1) \<in> (RAG s)^+"
 
   362   and dp2: "(n, n2) \<in> (RAG s)^+"
 
   365   and dp2: "(n, n2) \<in> (RAG s)^+"
 
   365 proof(rule unique_chain [OF _ dp1 dp2 neq])
 
   368 proof(rule unique_chain [OF _ dp1 dp2 neq])
 
   366   from unique_RAG[OF vt]
 
   369   from unique_RAG[OF vt]
 
   367   show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
 
   370   show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
 
   368 qed
 
   371 qed
 
   369 
   372 
   370 text {* (* ??? *)
 
   373 text {* (* ddd *)
 
   371 *}
 
   374 *}
 
   372 lemma dependants_child_unique:
 
   375 lemma dependants_child_unique:
 
   373   fixes s th th1 th2 th3
 
   376   fixes s th th1 th2 th3
 
   374   assumes vt: "vt s"
 
   377   assumes vt: "vt s"
 
   375   and ch1: "(Th th1, Th th) \<in> child s"
 
   378   and ch1: "(Th th1, Th th) \<in> child s"
 
   403   shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"
 
   406   shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"
 
   404   using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
 
   407   using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
 
   405   apply (unfold children_def)
 
   408   apply (unfold children_def)
 
   406   by (metis assms(2) children_def RAG_children eq_RAG)
 
   409   by (metis assms(2) children_def RAG_children eq_RAG)
 
   407 
   410 
   408 text {* (* ??? *)
 
   411 text {* (* ddd *)
 
   409 *}
 
   412 *}
 
   410 lemma dependants_expand:
 
   413 lemma dependants_expand:
 
   411   assumes "vt s"
 
   414   assumes "vt s"
 
   412   shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
 
   415   shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
 
   413 apply(simp add: image_def)
 
   416 apply(simp add: image_def)
 
   445 
   448 
   446 lemma UN_exists:
 
   449 lemma UN_exists:
 
   447   shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
 
   450   shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
 
   448 by auto
 
   451 by auto
 
   449 
   452 
   450 text {* (* ??? *)
 
   453 text {* (* ddd *)
 
       
   454   This is the recursive equation used to compute the current precedence of 
       
   455   a thread (the @{text "th"}) here. 
   451 *}
 
   456 *}
 
   452 lemma cp_rec:
 
   457 lemma cp_rec:
 
   453   fixes s th
 
   458   fixes s th
 
   454   assumes vt: "vt s"
 
   459   assumes vt: "vt s"
 
   455   shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
 
   460   shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
 
   512 
   517 
   513     finally show "?LHS = ?RHS" .
 
   518     finally show "?LHS = ?RHS" .
 
   514   qed
 
   519   qed
 
   515 qed
 
   520 qed
 
   516 
   521 
       
   522 lemma next_waiting:
 
       
   523   assumes vt: "vt s"
 
       
   524   and nxt: "next_th s th cs th'"
 
       
   525   shows "waiting s th' cs"
 
       
   526 proof -
 
       
   527   from assms show ?thesis
 
       
   528     apply (auto simp:next_th_def s_waiting_def[folded wq_def])
 
       
   529   proof -
 
       
   530     fix rest
 
       
   531     assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
 
       
   532       and eq_wq: "wq s cs = th # rest"
 
       
   533       and ne: "rest \<noteq> []"
 
       
   534     have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
       
   535     proof(rule someI2)
 
       
   536       from wq_distinct[OF vt, of cs] eq_wq
 
       
   537       show "distinct rest \<and> set rest = set rest" by auto
 
       
   538     next
 
       
   539       show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 
       
   540     qed
 
       
   541     with ni
 
       
   542     have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>  set (SOME q. distinct q \<and> set q = set rest)"
 
       
   543       by simp
 
       
   544     moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 
       
   545     proof(rule someI2)
 
       
   546       from wq_distinct[OF vt, of cs] eq_wq
 
       
   547       show "distinct rest \<and> set rest = set rest" by auto
 
       
   548     next
 
       
   549       from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
 
       
   550     qed
 
       
   551     ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
 
       
   552   next
 
       
   553     fix rest
 
       
   554     assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
 
       
   555       and ne: "rest \<noteq> []"
 
       
   556     have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 
       
   557     proof(rule someI2)
 
       
   558       from wq_distinct[OF vt, of cs] eq_wq
 
       
   559       show "distinct rest \<and> set rest = set rest" by auto
 
       
   560     next
 
       
   561       from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
 
       
   562     qed
 
       
   563     hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"
 
       
   564       by auto
 
       
   565     moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
       
   566     proof(rule someI2)
 
       
   567       from wq_distinct[OF vt, of cs] eq_wq
 
       
   568       show "distinct rest \<and> set rest = set rest" by auto
 
       
   569     next
 
       
   570       show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 
       
   571     qed
 
       
   572     ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp
 
       
   573     with eq_wq and wq_distinct[OF vt, of cs]
 
       
   574     show False by auto
 
       
   575   qed
 
       
   576 qed
 
       
   577 
   517 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
 
   578 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
 
   518 where "cps s = {(th, cp s th) | th . th \<in> threads s}"
 
   579 where "cps s = {(th, cp s th) | th . th \<in> threads s}"
 
   519 
   580 
       
   581 text {* (* ddd *)
 
       
   582   One beauty of our modelling is that we follow the definitional extension tradition of HOL.
 
       
   583   The benefit of such a concise and miniature model is that  large number of intuitively 
       
   584   obvious facts are derived as lemmas, rather than asserted as axioms.
 
       
   585 *}
 
       
   586 
       
   587 text {*
 
       
   588   However, the lemmas in the forthcoming several locales are no longer 
       
   589   obvious. These lemmas show how the current precedences should be recalculated 
       
   590   after every execution step (in our model, every step is represented by an event, 
       
   591   which in turn, represents a system call, or operation). Each operation is 
       
   592   treated in a separate locale.
 
       
   593 
       
   594   The complication of current precedence recalculation comes 
       
   595   because the changing of RAG needs to be taken into account, 
       
   596   in addition to the changing of precedence. 
       
   597   The reason RAG changing affects current precedence is that,
 
       
   598   according to the definition, current precedence 
       
   599   of a thread is the maximum of the precedences of its dependants, 
       
   600   where the dependants are defined in terms of RAG.
 
       
   601 
       
   602   Therefore, each operation, lemmas concerning the change of the precedences 
       
   603   and RAG are derived first, so that the lemmas about
 
       
   604   current precedence recalculation can be based on.
 
       
   605 *}
 
       
   606 
       
   607 text {* (* ddd *)
 
       
   608   The following locale @{text "step_set_cps"} investigates the recalculation 
       
   609   after the @{text "Set"} operation.
 
       
   610 *}
 
   520 locale step_set_cps =
 
   611 locale step_set_cps =
 
   521   fixes s' th prio s 
   612   fixes s' th prio s 
   522   defines s_def : "s \<equiv> (Set th prio#s')"
 
   613   -- {* @{text "s'"} is the system state before the operation *}
 
       
   614   -- {* @{text "s"} is the system state after the operation *}
 
       
   615   defines s_def : "s \<equiv> (Set th prio#s')" 
       
   616   -- {* @{text "s"} is assumed to be a legitimate state, from which
 
       
   617          the legitimacy of @{text "s"} can be derived. *}
 
   523   assumes vt_s: "vt s"
 
   618   assumes vt_s: "vt s"
 
   524 
   619 
   525 context step_set_cps 
   620 context step_set_cps 
   526 begin
 
   621 begin
 
       
   622 
       
   623 text {* (* ddd *)
 
       
   624   The following lemma confirms that @{text "Set"}-operating only changes the precedence 
       
   625   of initiating thread.
 
       
   626 *}
 
   527 
   627 
   528 lemma eq_preced:
 
   628 lemma eq_preced:
 
   529   fixes th'
 
   629   fixes th'
 
   530   assumes "th' \<noteq> th"
 
   630   assumes "th' \<noteq> th"
 
   531   shows "preced th' s = preced th' s'"
 
   631   shows "preced th' s = preced th' s'"
 
   532 proof -
 
   632 proof -
 
   533   from assms show ?thesis 
   633   from assms show ?thesis 
   534     by (unfold s_def, auto simp:preced_def)
 
   634     by (unfold s_def, auto simp:preced_def)
 
   535 qed
 
   635 qed
 
   536 
   636 
       
   637 text {* (* ddd *)
 
       
   638   The following lemma assures that the resetting of priority does not change the RAG. 
       
   639 *}
 
       
   640 
   537 lemma eq_dep: "RAG s = RAG s'"
 
   641 lemma eq_dep: "RAG s = RAG s'"
 
   538   by (unfold s_def RAG_set_unchanged, auto)
 
   642   by (unfold s_def RAG_set_unchanged, auto)
 
       
   643 
       
   644 text {*
 
       
   645   Th following lemma @{text "eq_cp_pre"} circumscribe a rough range of recalculation.
 
       
   646   It says, thread other than the initiating thread @{text "th"} does not need recalculation
 
       
   647   unless it lies upstream of @{text "th"} in the RAG. 
       
   648 
       
   649   The reason behind this lemma is that: 
       
   650   the change of precedence of one thread can only affect it's upstream threads, according to 
       
   651   lemma @{text "eq_preced"}. Since the only thread which might change precedence is
 
       
   652   @{text "th"}, so only @{text "th"} and its upstream threads need recalculation.
 
       
   653   (* ccc *)
 
       
   654 *}
 
   539 
   655 
   540 lemma eq_cp_pre:
 
   656 lemma eq_cp_pre:
 
   541   fixes th' 
   657   fixes th' 
   542   assumes neq_th: "th' \<noteq> th"
 
   658   assumes neq_th: "th' \<noteq> th"
 
   543   and nd: "th \<notin> dependants s th'"
 
   659   and nd: "th \<notin> dependants s th'"
 
   544   shows "cp s th' = cp s' th'"
 
   660   shows "cp s th' = cp s' th'"
 
   545   apply (unfold cp_eq_cpreced cpreced_def)
 
   661 proof -
 
   546 proof -
 
   662   -- {* This is what we need to prove after expanding the definition of @{text "cp"} *}
 
   547   have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
 
   663   have "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
 
   548     by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
 
   664         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
 
   549   moreover {
 
   665    (is "Max (?f1 ` ({th'} \<union> ?A)) = Max (?f2 ` ({th'} \<union> ?B))") 
   550     fix th1 
   666   proof -
 
   551     assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
 
   667       -- {* Since RAG is not changed by @{text "Set"}-operation, the dependants of 
   552     hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
 
   668             any threads are not changed, this is one of key facts underpinning this 
   553     hence "preced th1 s = preced th1 s'"
 
   669             lemma *}
 
   554     proof
 
   670       have eq_ab: "?A = ?B" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
 
   555       assume "th1 = th'"
 
   671       have "(?f1 ` ({th'} \<union> ?A)) =  (?f2 ` ({th'} \<union> ?B))"
 
   556       with eq_preced[OF neq_th]
 
   672       proof(rule image_cong)
 
   557       show "preced th1 s = preced th1 s'" by simp
 
   673         show "{th'} \<union> ?A = {th'} \<union> ?B" by (simp only:eq_ab)
 
   558     next
 
   674       next  
   559       assume "th1 \<in> dependants (wq s') th'"
 
   675         fix x
 
   560       with nd and eq_dp have "th1 \<noteq> th"
 
   676         assume x_in: "x \<in> {th'} \<union> ?B"
 
   561         by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
 
   677         show "?f1 x = ?f2 x"
 
   562       from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
 
   678         proof(rule eq_preced) -- {* The other key fact underpinning this lemma is @{text "eq_preced"} *}
 
   563     qed
 
   679           from x_in[folded eq_ab, unfolded eq_dependants]
 
   564   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
   680           have "x \<in> {th'} \<union> dependants s th'" .
 
   565                      ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 
   681           thus "x \<noteq> th"
 
   566     by (auto simp:image_def)
 
   682           proof
 
   567   thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
 
   683             assume "x \<in> {th'}" 
   568         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
 
   684             with `th' \<noteq> th` show ?thesis by simp
 
   569 qed
 
   685           next
 
   570 
   686             assume "x \<in> dependants s th'"
 
       
   687             with `th \<notin> dependants s th'` show ?thesis by auto
 
       
   688           qed 
       
   689         qed 
       
   690       qed
 
       
   691       thus ?thesis by simp
 
       
   692   qed 
       
   693   thus ?thesis by (unfold cp_eq_cpreced cpreced_def)
 
       
   694 qed
 
       
   695 
       
   696 text {*
 
       
   697   The following lemma shows that no thread lies upstream of the initiating thread @{text "th"}. 
       
   698   The reason for this is that only no-blocked thread can initiate 
       
   699   a system call. Since thread @{text "th"} is non-blocked, it is not waiting for any 
       
   700   critical resource. Therefore, there is edge leading out of @{text "th"} in the RAG.
 
       
   701   Consequently, there is no node (neither resource nor thread) upstream of @{text "th"}.
 
       
   702 *}
 
   571 lemma no_dependants:
 
   703 lemma no_dependants:
 
   572   assumes "th' \<noteq> th"
 
       
   573   shows "th \<notin> dependants s th'"
 
   704   shows "th \<notin> dependants s th'"
 
   574 proof
 
   705 proof
 
   575   assume h: "th \<in> dependants s th'"
 
   706   assume "th \<in> dependants s th'"
 
   576   from step_back_step [OF vt_s[unfolded s_def]]
 
   707   from `th \<in> dependants s th'` have "(Th th, Th th') \<in> (RAG s')\<^sup>+"
 
   577   have "step s' (Set th prio)" .
 
       
   578   hence "th \<in> runing s'" by (cases, simp)
 
       
   579   hence rd_th: "th \<in> readys s'" 
       
   580     by (simp add:readys_def runing_def)
 
       
   581   from h have "(Th th, Th th') \<in> (RAG s')\<^sup>+"
 
       
   582     by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto)
 
   708     by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto)
 
   583   from tranclD[OF this]
 
   709   from tranclD[OF this]
 
   584   obtain z where "(Th th, z) \<in> RAG s'" by auto
 
   710   obtain z where "(Th th, z) \<in> RAG s'" by auto
 
   585   with rd_th show "False"
 
   711   moreover have "th \<in> readys s'"
 
       
   712   proof -
 
       
   713     from step_back_step [OF vt_s[unfolded s_def]]
 
       
   714     have "step s' (Set th prio)" .
 
       
   715     hence "th \<in> runing s'" by (cases, simp)
 
       
   716     thus ?thesis by (simp add:readys_def runing_def)
 
       
   717   qed
 
       
   718   ultimately show "False"
 
   586     apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
 
   719     apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
 
   587     by (fold wq_def, blast)
 
   720     by (fold wq_def, blast)
 
   588 qed
 
   721 qed
 
   589 
   722 
   590 (* Result improved *)
 
   723 (* Result improved *)
 
       
   724 text {* 
       
   725   A simple combination of @{text "eq_cp_pre"} and @{text "no_dependants"}
 
       
   726   gives the main lemma of this locale, which shows that
 
       
   727   only the initiating thread needs a recalculation of current precedence.
 
       
   728 *}
 
   591 lemma eq_cp:
 
   729 lemma eq_cp:
 
   592  fixes th' 
   730   fixes th' 
   593   assumes neq_th: "th' \<noteq> th"
 
   731   assumes "th' \<noteq> th"
 
   594   shows "cp s th' = cp s' th'"
 
   732   shows "cp s th' = cp s' th'"
 
   595 proof(rule eq_cp_pre [OF neq_th])
 
   733   by (rule eq_cp_pre[OF assms no_dependants])
 
   596   from no_dependants[OF neq_th] 
   734 
   597   show "th \<notin> dependants s th'" .
 
   735 
   598 qed
 
   736 text {* (* ddd *) \noindent
 
   599 
   737    The following @{text "eq_up"} was originally designed to save the recalculations
 
       
   738    of current precedence going upstream from thread @{text "th"} can stop earlier. 
       
   739    If at a certain point along way, the recalculation results in the same
 
       
   740    result, the recalculation can stop there. 
       
   741    This lemma is obsolete because we found that @{text "th"} is not contained in 
       
   742    any thread's dependants set. 
       
   743 
       
   744    The foregoing lemma says only those threads which 
       
   745 *}
 
   600 lemma eq_up:
 
   746 lemma eq_up:
 
   601   fixes th' th''
 
   747   fixes th' th''
 
   602   assumes dp1: "th \<in> dependants s th'"
 
   748   assumes dp1: "th \<in> dependants s th'"
 
   603   and dp2: "th' \<in> dependants s th''"
 
   749   and dp2: "th' \<in> dependants s th''"
 
   604   and eq_cps: "cp s th' = cp s' th'"
 
   750   and eq_cps: "cp s th' = cp s' th'"
 
   731     qed
 
   877     qed
 
   732   }
 
   878   }
 
   733   ultimately show ?thesis by auto
 
   879   ultimately show ?thesis by auto
 
   734 qed
 
   880 qed
 
   735 
   881 
       
   882 text {* (* ddd *)
 
       
   883   For those @{text "th''"},  @{text "th \<in> dependants s th''"} means that 
       
   884   the current precedence of such @{text "th''"} might possibly be boosted if the 
       
   885   current precedence of @{text "th"} somehow get raised. The following lemma
 
       
   886   says that if the resetting of its own priority by thread @{text "th"} does not
 
       
   887   change its current precedence, then the current precedence of such @{text "th''"}
 
       
   888   will remain unchanged. The situation such that @{text "th"}'s current 
       
   889   precedence does not change with the resetting of its priority might happen in many
 
       
   890   different cases. For example, if the current precedence of @{text "th"} is already an inherited one,
 
       
   891   the lowering of its priority will not change its current precedence, and the increasing 
       
   892   of its priority will not change its current precedence neither, if 
       
   893   incidental rising of its own precedence is not large enough to surpass the inherited precedence. 
       
   894 *}
 
       
   895 
   736 lemma eq_up_self:
 
   896 lemma eq_up_self:
 
   737   fixes th' th''
 
   897   fixes th' th''
 
   738   assumes dp: "th \<in> dependants s th''"
 
   898   assumes dp: "th \<in> dependants s th''"
 
   739   and eq_cps: "cp s th = cp s' th"
 
   899   and eq_cps: "cp s th = cp s' th"
 
   740   shows "cp s th'' = cp s' th''"
 
   900   shows "cp s th'' = cp s' th''"
 
   856     qed
 
  1016     qed
 
   857   }
 
  1017   }
 
   858   ultimately show ?thesis by auto
 
  1018   ultimately show ?thesis by auto
 
   859 qed
 
  1019 qed
 
   860 end
 
  1020 end
 
   861 
       
   862 lemma next_waiting:
 
       
   863   assumes vt: "vt s"
 
       
   864   and nxt: "next_th s th cs th'"
 
       
   865   shows "waiting s th' cs"
 
       
   866 proof -
 
       
   867   from assms show ?thesis
 
       
   868     apply (auto simp:next_th_def s_waiting_def[folded wq_def])
 
       
   869   proof -
 
       
   870     fix rest
 
       
   871     assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
 
       
   872       and eq_wq: "wq s cs = th # rest"
 
       
   873       and ne: "rest \<noteq> []"
 
       
   874     have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
       
   875     proof(rule someI2)
 
       
   876       from wq_distinct[OF vt, of cs] eq_wq
 
       
   877       show "distinct rest \<and> set rest = set rest" by auto
 
       
   878     next
 
       
   879       show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 
       
   880     qed
 
       
   881     with ni
 
       
   882     have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>  set (SOME q. distinct q \<and> set q = set rest)"
 
       
   883       by simp
 
       
   884     moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 
       
   885     proof(rule someI2)
 
       
   886       from wq_distinct[OF vt, of cs] eq_wq
 
       
   887       show "distinct rest \<and> set rest = set rest" by auto
 
       
   888     next
 
       
   889       from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
 
       
   890     qed
 
       
   891     ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
 
       
   892   next
 
       
   893     fix rest
 
       
   894     assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
 
       
   895       and ne: "rest \<noteq> []"
 
       
   896     have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 
       
   897     proof(rule someI2)
 
       
   898       from wq_distinct[OF vt, of cs] eq_wq
 
       
   899       show "distinct rest \<and> set rest = set rest" by auto
 
       
   900     next
 
       
   901       from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
 
       
   902     qed
 
       
   903     hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"
 
       
   904       by auto
 
       
   905     moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
       
   906     proof(rule someI2)
 
       
   907       from wq_distinct[OF vt, of cs] eq_wq
 
       
   908       show "distinct rest \<and> set rest = set rest" by auto
 
       
   909     next
 
       
   910       show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 
       
   911     qed
 
       
   912     ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp
 
       
   913     with eq_wq and wq_distinct[OF vt, of cs]
 
       
   914     show False by auto
 
       
   915   qed
 
       
   916 qed
 
       
   917 
       
   918 
  1021 
   919 locale step_v_cps =
 
  1022 locale step_v_cps =
 
   920   fixes s' th cs s 
  1023   fixes s' th cs s 
   921   defines s_def : "s \<equiv> (V th cs#s')"
 
  1024   defines s_def : "s \<equiv> (V th cs#s')"
 
   922   assumes vt_s: "vt s"
 
  1025   assumes vt_s: "vt s"
pip