1 section {*

     2   This file contains lemmas used to guide the recalculation of current precedence 

     3   after every system call (or system operation)

     4 *}

     5 theory Implementation

     6 imports PIPBasics

     7 begin

     8 

     9 text {* (* ddd *)

    10   One beauty of our modelling is that we follow the definitional extension tradition of HOL.

    11   The benefit of such a concise and miniature model is that  large number of intuitively 

    12   obvious facts are derived as lemmas, rather than asserted as axioms.

    13 *}

    14 

    15 text {*

    16   However, the lemmas in the forthcoming several locales are no longer 

    17   obvious. These lemmas show how the current precedences should be recalculated 

    18   after every execution step (in our model, every step is represented by an event, 

    19   which in turn, represents a system call, or operation). Each operation is 

    20   treated in a separate locale.

    21 

    22   The complication of current precedence recalculation comes 

    23   because the changing of RAG needs to be taken into account, 

    24   in addition to the changing of precedence. 

    25   The reason RAG changing affects current precedence is that,

    26   according to the definition, current precedence 

    27   of a thread is the maximum of the precedences of its dependants, 

    28   where the dependants are defined in terms of RAG.

    29 

    30   Therefore, each operation, lemmas concerning the change of the precedences 

    31   and RAG are derived first, so that the lemmas about

    32   current precedence recalculation can be based on.

    33 *}

    34 

    35 text {* (* ddd *)

    36   The following locale @{text "step_set_cps"} investigates the recalculation 

    37   after the @{text "Set"} operation.

    38 *}

    39 locale step_set_cps =

    40   fixes s' th prio s 

    41   -- {* @{text "s'"} is the system state before the operation *}

    42   -- {* @{text "s"} is the system state after the operation *}

    43   defines s_def : "s \<equiv> (Set th prio#s')" 

    44   -- {* @{text "s"} is assumed to be a legitimate state, from which

    45          the legitimacy of @{text "s"} can be derived. *}

    46   assumes vt_s: "vt s"

    47 

    48 sublocale step_set_cps < vat_s : valid_trace "s"

    49 proof

    50   from vt_s show "vt s" .

    51 qed

    52 

    53 sublocale step_set_cps < vat_s' : valid_trace "s'"

    54 proof

    55   from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .

    56 qed

    57 

    58 context step_set_cps 

    59 begin

    60 

    61 text {* (* ddd *)

    62   The following two lemmas confirm that @{text "Set"}-operating only changes the precedence 

    63   of the initiating thread.

    64 *}

    65 

    66 lemma eq_preced:

    67   assumes "th' \<noteq> th"

    68   shows "preced th' s = preced th' s'"

    69 proof -

    70   from assms show ?thesis 

    71     by (unfold s_def, auto simp:preced_def)

    72 qed

    73 

    74 lemma eq_the_preced: 

    75   fixes th'

    76   assumes "th' \<noteq> th"

    77   shows "the_preced s th' = the_preced s' th'"

    78   using assms

    79   by (unfold the_preced_def, intro eq_preced, simp)

    80 

    81 text {*

    82   The following lemma assures that the resetting of priority does not change the RAG. 

    83 *}

    84 

    85 lemma eq_dep: "RAG s = RAG s'"

    86   by (unfold s_def RAG_set_unchanged, auto)

    87 

    88 text {* (* ddd *)

    89   Th following lemma @{text "eq_cp_pre"} says the priority change of @{text "th"}

    90   only affects those threads, which as @{text "Th th"} in their sub-trees.

    91   

    92   The proof of this lemma is simplified by using the alternative definition of @{text "cp"}. 

    93 *}

    94 

    95 lemma eq_cp_pre:

    96   fixes th' 

    97   assumes nd: "Th th \<notin> subtree (RAG s') (Th th')"

    98   shows "cp s th' = cp s' th'"

    99 proof -

   100   -- {* After unfolding using the alternative definition, elements 

   101         affecting the @{term "cp"}-value of threads become explicit. 

   102         We only need to prove the following: *}

   103   have "Max (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) =

   104         Max (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})"

   105         (is "Max (?f ` ?S1) = Max (?g ` ?S2)")

   106   proof -

   107     -- {* The base sets are equal. *}

   108     have "?S1 = ?S2" using eq_dep by simp

   109     -- {* The function values on the base set are equal as well. *}

   110     moreover have "\<forall> e \<in> ?S2. ?f e = ?g e"

   111     proof

   112       fix th1

   113       assume "th1 \<in> ?S2"

   114       with nd have "th1 \<noteq> th" by (auto)

   115       from eq_the_preced[OF this]

   116       show "the_preced s th1 = the_preced s' th1" .

   117     qed

   118     -- {* Therefore, the image of the functions are equal. *}

   119     ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq)

   120     thus ?thesis by simp

   121   qed

   122   thus ?thesis by (simp add:cp_alt_def)

   123 qed

   124 

   125 text {*

   126   The following lemma shows that @{term "th"} is not in the 

   127   sub-tree of any other thread. 

   128 *}

   129 lemma th_in_no_subtree:

   130   assumes "th' \<noteq> th"

   131   shows "Th th \<notin> subtree (RAG s') (Th th')"

   132 proof -

   133   have "th \<in> readys s'"

   134   proof -

   135     from step_back_step [OF vt_s[unfolded s_def]]

   136     have "step s' (Set th prio)" .

   137     hence "th \<in> runing s'" by (cases, simp)

   138     thus ?thesis by (simp add:readys_def runing_def)

   139   qed

   140   from vat_s'.readys_in_no_subtree[OF this assms(1)]

   141   show ?thesis by blast

   142 qed

   143 

   144 text {* 

   145   By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, 

   146   it is obvious that the change of priority only affects the @{text "cp"}-value 

   147   of the initiating thread @{text "th"}.

   148 *}

   149 lemma eq_cp:

   150   fixes th' 

   151   assumes "th' \<noteq> th"

   152   shows "cp s th' = cp s' th'"

   153   by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])

   154 

   155 end

   156 

   157 text {*

   158   The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.

   159 *}

   160 

   161 locale step_v_cps =

   162   -- {* @{text "th"} is the initiating thread *}

   163   -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}

   164   fixes s' th cs s    -- {* @{text "s'"} is the state before operation*}

   165   defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}

   166   -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}

   167   assumes vt_s: "vt s"

   168 

   169 sublocale step_v_cps < vat_s : valid_trace "s"

   170 proof

   171   from vt_s show "vt s" .

   172 qed

   173 

   174 sublocale step_v_cps < vat_s' : valid_trace "s'"

   175 proof

   176   from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .

   177 qed

   178 

   179 context step_v_cps

   180 begin

   181 

   182 lemma ready_th_s': "th \<in> readys s'"

   183   using step_back_step[OF vt_s[unfolded s_def]]

   184   by (cases, simp add:runing_def)

   185 

   186 lemma ancestors_th: "ancestors (RAG s') (Th th) = {}"

   187 proof -

   188   from vat_s'.readys_root[OF ready_th_s']

   189   show ?thesis

   190   by (unfold root_def, simp)

   191 qed

   192 

   193 lemma holding_th: "holding s' th cs"

   194 proof -

   195   from vt_s[unfolded s_def]

   196   have " PIP s' (V th cs)" by (cases, simp)

   197   thus ?thesis by (cases, auto)

   198 qed

   199 

   200 lemma edge_of_th:

   201     "(Cs cs, Th th) \<in> RAG s'" 

   202 proof -

   203  from holding_th

   204  show ?thesis 

   205     by (unfold s_RAG_def holding_eq, auto)

   206 qed

   207 

   208 lemma ancestors_cs: 

   209   "ancestors (RAG s') (Cs cs) = {Th th}"

   210 proof -

   211   have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th)  \<union>  {Th th}"

   212   proof(rule vat_s'.rtree_RAG.ancestors_accum)

   213     from vt_s[unfolded s_def]

   214     have " PIP s' (V th cs)" by (cases, simp)

   215     thus "(Cs cs, Th th) \<in> RAG s'" 

   216     proof(cases)

   217       assume "holding s' th cs"

   218       from this[unfolded holding_eq]

   219       show ?thesis by (unfold s_RAG_def, auto)

   220     qed

   221   qed

   222   from this[unfolded ancestors_th] show ?thesis by simp

   223 qed

   224 

   225 lemma preced_kept: "the_preced s = the_preced s'"

   226   by (auto simp: s_def the_preced_def preced_def)

   227 

   228 end

   229 

   230 text {*

   231   The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 

   232   which represents the case when there is another thread @{text "th'"}

   233   to take over the critical resource released by the initiating thread @{text "th"}.

   234 *}

   235 locale step_v_cps_nt = step_v_cps +

   236   fixes th'

   237   -- {* @{text "th'"} is assumed to take over @{text "cs"} *}

   238   assumes nt: "next_th s' th cs th'" 

   239 

   240 context step_v_cps_nt

   241 begin

   242 

   243 text {*

   244   Lemma @{text "RAG_s"} confirms the change of RAG:

   245   two edges removed and one added, as shown by the following diagram.

   246 *}

   247 

   248 (*

   249   RAG before the V-operation

   250     th1 ----|

   251             |

   252     th' ----|

   253             |----> cs -----|

   254     th2 ----|              |

   255             |              |

   256     th3 ----|              |

   257                            |------> th

   258     th4 ----|              |

   259             |              |

   260     th5 ----|              |

   261             |----> cs'-----|

   262     th6 ----|

   263             |

   264     th7 ----|

   265 

   266  RAG after the V-operation

   267     th1 ----|

   268             |

   269             |----> cs ----> th'

   270     th2 ----|              

   271             |              

   272     th3 ----|              

   273                            

   274     th4 ----|              

   275             |              

   276     th5 ----|              

   277             |----> cs'----> th

   278     th6 ----|

   279             |

   280     th7 ----|

   281 *)

   282 

   283 lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"

   284                 using next_th_RAG[OF nt]  .

   285 

   286 lemma ancestors_th': 

   287   "ancestors (RAG s') (Th th') = {Th th, Cs cs}" 

   288 proof -

   289   have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}"

   290   proof(rule  vat_s'.rtree_RAG.ancestors_accum)

   291     from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto

   292   qed

   293   thus ?thesis using ancestors_th ancestors_cs by auto

   294 qed

   295 

   296 lemma RAG_s:

   297   "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>

   298                                          {(Cs cs, Th th')}"

   299 proof -

   300   from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]

   301     and nt show ?thesis  by (auto intro:next_th_unique)

   302 qed

   303 

   304 lemma subtree_kept:

   305   assumes "th1 \<notin> {th, th'}"

   306   shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R")

   307 proof -

   308   let ?RAG' = "(RAG s' - {(Cs cs, Th th), (Th th', Cs cs)})"

   309   let ?RAG'' = "?RAG' \<union> {(Cs cs, Th th')}"

   310   have "subtree ?RAG' (Th th1) = ?R" 

   311   proof(rule subset_del_subtree_outside)

   312     show "Range {(Cs cs, Th th), (Th th', Cs cs)} \<inter> subtree (RAG s') (Th th1) = {}"

   313     proof -

   314       have "(Th th) \<notin> subtree (RAG s') (Th th1)"

   315       proof(rule subtree_refute)

   316         show "Th th1 \<notin> ancestors (RAG s') (Th th)"

   317           by (unfold ancestors_th, simp)

   318       next

   319         from assms show "Th th1 \<noteq> Th th" by simp

   320       qed

   321       moreover have "(Cs cs) \<notin>  subtree (RAG s') (Th th1)"

   322       proof(rule subtree_refute)

   323         show "Th th1 \<notin> ancestors (RAG s') (Cs cs)"

   324           by (unfold ancestors_cs, insert assms, auto)

   325       qed simp

   326       ultimately have "{Th th, Cs cs} \<inter> subtree (RAG s') (Th th1) = {}" by auto

   327       thus ?thesis by simp

   328      qed

   329   qed

   330   moreover have "subtree ?RAG'' (Th th1) =  subtree ?RAG' (Th th1)"

   331   proof(rule subtree_insert_next)

   332     show "Th th' \<notin> subtree (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th1)"

   333     proof(rule subtree_refute)

   334       show "Th th1 \<notin> ancestors (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th')"

   335             (is "_ \<notin> ?R")

   336       proof -

   337           have "?R \<subseteq> ancestors (RAG s') (Th th')" by (rule ancestors_mono, auto)

   338           moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp

   339           ultimately show ?thesis by auto

   340       qed

   341     next

   342       from assms show "Th th1 \<noteq> Th th'" by simp

   343     qed

   344   qed

   345   ultimately show ?thesis by (unfold RAG_s, simp)

   346 qed

   347 

   348 lemma cp_kept:

   349   assumes "th1 \<notin> {th, th'}"

   350   shows "cp s th1 = cp s' th1"

   351     by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp)

   352 

   353 end

   354 

   355 locale step_v_cps_nnt = step_v_cps +

   356   assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"

   357 

   358 context step_v_cps_nnt

   359 begin

   360 

   361 lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"

   362 proof -

   363   from nnt and  step_RAG_v[OF vt_s[unfolded s_def], folded s_def]

   364   show ?thesis by auto

   365 qed

   366 

   367 lemma subtree_kept:

   368   assumes "th1 \<noteq> th"

   369   shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)"

   370 proof(unfold RAG_s, rule subset_del_subtree_outside)

   371   show "Range {(Cs cs, Th th)} \<inter> subtree (RAG s') (Th th1) = {}"

   372   proof -

   373     have "(Th th) \<notin> subtree (RAG s') (Th th1)"

   374     proof(rule subtree_refute)

   375       show "Th th1 \<notin> ancestors (RAG s') (Th th)"

   376           by (unfold ancestors_th, simp)

   377     next

   378       from assms show "Th th1 \<noteq> Th th" by simp

   379     qed

   380     thus ?thesis by auto

   381   qed

   382 qed

   383 

   384 lemma cp_kept_1:

   385   assumes "th1 \<noteq> th"

   386   shows "cp s th1 = cp s' th1"

   387     by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp)

   388 

   389 lemma subtree_cs: "subtree (RAG s') (Cs cs) = {Cs cs}"

   390 proof -

   391   { fix n

   392     have "(Cs cs) \<notin> ancestors (RAG s') n"

   393     proof

   394       assume "Cs cs \<in> ancestors (RAG s') n"

   395       hence "(n, Cs cs) \<in> (RAG s')^+" by (auto simp:ancestors_def)

   396       from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> RAG s'" by auto

   397       then obtain th' where "nn = Th th'"

   398         by (unfold s_RAG_def, auto)

   399       from h[unfolded this] have "(Th th', Cs cs) \<in> RAG s'" .

   400       from this[unfolded s_RAG_def]

   401       have "waiting (wq s') th' cs" by auto

   402       from this[unfolded cs_waiting_def]

   403       have "1 < length (wq s' cs)"

   404           by (cases "wq s' cs", auto)

   405       from holding_next_thI[OF holding_th this]

   406       obtain th' where "next_th s' th cs th'" by auto

   407       with nnt show False by auto

   408     qed

   409   } note h = this

   410   {  fix n

   411      assume "n \<in> subtree (RAG s') (Cs cs)"

   412      hence "n = (Cs cs)"

   413      by (elim subtreeE, insert h, auto)

   414   } moreover have "(Cs cs) \<in> subtree (RAG s') (Cs cs)"

   415       by (auto simp:subtree_def)

   416   ultimately show ?thesis by auto 

   417 qed

   418 

   419 lemma subtree_th: 

   420   "subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}"

   421 proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside)

   422   from edge_of_th

   423   show "(Cs cs, Th th) \<in> edges_in (RAG s') (Th th)"

   424     by (unfold edges_in_def, auto simp:subtree_def)

   425 qed

   426 

   427 lemma cp_kept_2: 

   428   shows "cp s th = cp s' th" 

   429  by (unfold cp_alt_def subtree_th preced_kept, auto)

   430 

   431 lemma eq_cp:

   432   fixes th' 

   433   shows "cp s th' = cp s' th'"

   434   using cp_kept_1 cp_kept_2

   435   by (cases "th' = th", auto)

   436 end

   437 

   438 

   439 locale step_P_cps =

   440   fixes s' th cs s 

   441   defines s_def : "s \<equiv> (P th cs#s')"

   442   assumes vt_s: "vt s"

   443 

   444 sublocale step_P_cps < vat_s : valid_trace "s"

   445 proof

   446   from vt_s show "vt s" .

   447 qed

   448 

   449 sublocale step_P_cps < vat_s' : valid_trace "s'"

   450 proof

   451   from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .

   452 qed

   453 

   454 context step_P_cps

   455 begin

   456 

   457 lemma readys_th: "th \<in> readys s'"

   458 proof -

   459     from step_back_step [OF vt_s[unfolded s_def]]

   460     have "PIP s' (P th cs)" .

   461     hence "th \<in> runing s'" by (cases, simp)

   462     thus ?thesis by (simp add:readys_def runing_def)

   463 qed

   464 

   465 lemma root_th: "root (RAG s') (Th th)"

   466   using readys_root[OF readys_th] .

   467 

   468 lemma in_no_others_subtree:

   469   assumes "th' \<noteq> th"

   470   shows "Th th \<notin> subtree (RAG s') (Th th')"

   471 proof

   472   assume "Th th \<in> subtree (RAG s') (Th th')"

   473   thus False

   474   proof(cases rule:subtreeE)

   475     case 1

   476     with assms show ?thesis by auto

   477   next

   478     case 2

   479     with root_th show ?thesis by (auto simp:root_def)

   480   qed

   481 qed

   482 

   483 lemma preced_kept: "the_preced s = the_preced s'"

   484   by (auto simp: s_def the_preced_def preced_def)

   485 

   486 end

   487 

   488 locale step_P_cps_ne =step_P_cps +

   489   fixes th'

   490   assumes ne: "wq s' cs \<noteq> []"

   491   defines th'_def: "th' \<equiv> hd (wq s' cs)"

   492 

   493 locale step_P_cps_e =step_P_cps +

   494   assumes ee: "wq s' cs = []"

   495 

   496 context step_P_cps_e

   497 begin

   498 

   499 lemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}"

   500 proof -

   501   from ee and  step_RAG_p[OF vt_s[unfolded s_def], folded s_def]

   502   show ?thesis by auto

   503 qed

   504 

   505 lemma subtree_kept:

   506   assumes "th' \<noteq> th"

   507   shows "subtree (RAG s) (Th th') = subtree (RAG s') (Th th')"

   508 proof(unfold RAG_s, rule subtree_insert_next)

   509   from in_no_others_subtree[OF assms] 

   510   show "Th th \<notin> subtree (RAG s') (Th th')" .

   511 qed

   512 

   513 lemma cp_kept: 

   514   assumes "th' \<noteq> th"

   515   shows "cp s th' = cp s' th'"

   516 proof -

   517   have "(the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) =

   518         (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})"

   519         by (unfold preced_kept subtree_kept[OF assms], simp)

   520   thus ?thesis by (unfold cp_alt_def, simp)

   521 qed

   522 

   523 end

   524 

   525 context step_P_cps_ne 

   526 begin

   527 

   528 lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"

   529 proof -

   530   from step_RAG_p[OF vt_s[unfolded s_def]] and ne

   531   show ?thesis by (simp add:s_def)

   532 qed

   533 

   534 lemma cs_held: "(Cs cs, Th th') \<in> RAG s'"

   535 proof -

   536   have "(Cs cs, Th th') \<in> hRAG s'"

   537   proof -

   538     from ne

   539     have " holding s' th' cs"

   540       by (unfold th'_def holding_eq cs_holding_def, auto)

   541     thus ?thesis 

   542       by (unfold hRAG_def, auto)

   543   qed

   544   thus ?thesis by (unfold RAG_split, auto)

   545 qed

   546 

   547 lemma tRAG_s: 

   548   "tRAG s = tRAG s' \<union> {(Th th, Th th')}"

   549   using RAG_tRAG_transfer[OF RAG_s cs_held] .

   550 

   551 lemma cp_kept:

   552   assumes "Th th'' \<notin> ancestors (tRAG s) (Th th)"

   553   shows "cp s th'' = cp s' th''"

   554 proof -

   555   have h: "subtree (tRAG s) (Th th'') = subtree (tRAG s') (Th th'')"

   556   proof -

   557     have "Th th' \<notin> subtree (tRAG s') (Th th'')"

   558     proof

   559       assume "Th th' \<in> subtree (tRAG s') (Th th'')"

   560       thus False

   561       proof(rule subtreeE)

   562          assume "Th th' = Th th''"

   563          from assms[unfolded tRAG_s ancestors_def, folded this]

   564          show ?thesis by auto

   565       next

   566          assume "Th th'' \<in> ancestors (tRAG s') (Th th')"

   567          moreover have "... \<subseteq> ancestors (tRAG s) (Th th')"

   568          proof(rule ancestors_mono)

   569             show "tRAG s' \<subseteq> tRAG s" by (unfold tRAG_s, auto)

   570          qed 

   571          ultimately have "Th th'' \<in> ancestors (tRAG s) (Th th')" by auto

   572          moreover have "Th th' \<in> ancestors (tRAG s) (Th th)"

   573            by (unfold tRAG_s, auto simp:ancestors_def)

   574          ultimately have "Th th'' \<in> ancestors (tRAG s) (Th th)"

   575                        by (auto simp:ancestors_def)

   576          with assms show ?thesis by auto

   577       qed

   578     qed

   579     from subtree_insert_next[OF this]

   580     have "subtree (tRAG s' \<union> {(Th th, Th th')}) (Th th'') = subtree (tRAG s') (Th th'')" .

   581     from this[folded tRAG_s] show ?thesis .

   582   qed

   583   show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)

   584 qed

   585 

   586 lemma cp_gen_update_stop: (* ddd *)

   587   assumes "u \<in> ancestors (tRAG s) (Th th)"

   588   and "cp_gen s u = cp_gen s' u"

   589   and "y \<in> ancestors (tRAG s) u"

   590   shows "cp_gen s y = cp_gen s' y"

   591   using assms(3)

   592 proof(induct rule:wf_induct[OF vat_s.fsbttRAGs.wf])

   593   case (1 x)

   594   show ?case (is "?L = ?R")

   595   proof -

   596     from tRAG_ancestorsE[OF 1(2)]

   597     obtain th2 where eq_x: "x = Th th2" by blast

   598     from vat_s.cp_gen_rec[OF this]

   599     have "?L = 

   600           Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" .

   601     also have "... = 

   602           Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)"

   603   

   604     proof -

   605       from preced_kept have "the_preced s th2 = the_preced s' th2" by simp

   606       moreover have "cp_gen s ` RTree.children (tRAG s) x =

   607                      cp_gen s' ` RTree.children (tRAG s') x"

   608       proof -

   609         have "RTree.children (tRAG s) x =  RTree.children (tRAG s') x"

   610         proof(unfold tRAG_s, rule children_union_kept)

   611           have start: "(Th th, Th th') \<in> tRAG s"

   612             by (unfold tRAG_s, auto)

   613           note x_u = 1(2)

   614           show "x \<notin> Range {(Th th, Th th')}"

   615           proof

   616             assume "x \<in> Range {(Th th, Th th')}"

   617             hence eq_x: "x = Th th'" using RangeE by auto

   618             show False

   619             proof(cases rule:vat_s.rtree_s.ancestors_headE[OF assms(1) start])

   620               case 1

   621               from x_u[folded this, unfolded eq_x] vat_s.acyclic_tRAG

   622               show ?thesis by (auto simp:ancestors_def acyclic_def)

   623             next

   624               case 2

   625               with x_u[unfolded eq_x]

   626               have "(Th th', Th th') \<in> (tRAG s)^+" by (auto simp:ancestors_def)

   627               with vat_s.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)

   628             qed

   629           qed

   630         qed

   631         moreover have "cp_gen s ` RTree.children (tRAG s) x =

   632                        cp_gen s' ` RTree.children (tRAG s) x" (is "?f ` ?A = ?g ` ?A")

   633         proof(rule f_image_eq)

   634           fix a

   635           assume a_in: "a \<in> ?A"

   636           from 1(2)

   637           show "?f a = ?g a"

   638           proof(cases rule:vat_s.rtree_s.ancestors_childrenE[case_names in_ch out_ch])

   639              case in_ch

   640              show ?thesis

   641              proof(cases "a = u")

   642                 case True

   643                 from assms(2)[folded this] show ?thesis .

   644              next

   645                 case False

   646                 have a_not_in: "a \<notin> ancestors (tRAG s) (Th th)"

   647                 proof

   648                   assume a_in': "a \<in> ancestors (tRAG s) (Th th)"

   649                   have "a = u"

   650                   proof(rule vat_s.rtree_s.ancestors_children_unique)

   651                     from a_in' a_in show "a \<in> ancestors (tRAG s) (Th th) \<inter> 

   652                                           RTree.children (tRAG s) x" by auto

   653                   next 

   654                     from assms(1) in_ch show "u \<in> ancestors (tRAG s) (Th th) \<inter> 

   655                                       RTree.children (tRAG s) x" by auto

   656                   qed

   657                   with False show False by simp

   658                 qed

   659                 from a_in obtain th_a where eq_a: "a = Th th_a" 

   660                     by (unfold RTree.children_def tRAG_alt_def, auto)

   661                 from cp_kept[OF a_not_in[unfolded eq_a]]

   662                 have "cp s th_a = cp s' th_a" .

   663                 from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a]

   664                 show ?thesis .

   665              qed

   666           next

   667             case (out_ch z)

   668             hence h: "z \<in> ancestors (tRAG s) u" "z \<in> RTree.children (tRAG s) x" by auto

   669             show ?thesis

   670             proof(cases "a = z")

   671               case True

   672               from h(2) have zx_in: "(z, x) \<in> (tRAG s)" by (auto simp:RTree.children_def)

   673               from 1(1)[rule_format, OF this h(1)]

   674               have eq_cp_gen: "cp_gen s z = cp_gen s' z" .

   675               with True show ?thesis by metis

   676             next

   677               case False

   678               from a_in obtain th_a where eq_a: "a = Th th_a"

   679                 by (auto simp:RTree.children_def tRAG_alt_def)

   680               have "a \<notin> ancestors (tRAG s) (Th th)"

   681               proof

   682                 assume a_in': "a \<in> ancestors (tRAG s) (Th th)"

   683                 have "a = z"

   684                 proof(rule vat_s.rtree_s.ancestors_children_unique)

   685                   from assms(1) h(1) have "z \<in> ancestors (tRAG s) (Th th)"

   686                       by (auto simp:ancestors_def)

   687                   with h(2) show " z \<in> ancestors (tRAG s) (Th th) \<inter> 

   688                                        RTree.children (tRAG s) x" by auto

   689                 next

   690                   from a_in a_in'

   691                   show "a \<in> ancestors (tRAG s) (Th th) \<inter> RTree.children (tRAG s) x"

   692                     by auto

   693                 qed

   694                 with False show False by auto

   695               qed

   696               from cp_kept[OF this[unfolded eq_a]]

   697               have "cp s th_a = cp s' th_a" .

   698               from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a]

   699               show ?thesis .

   700             qed

   701           qed

   702         qed

   703         ultimately show ?thesis by metis

   704       qed

   705       ultimately show ?thesis by simp

   706     qed

   707     also have "... = ?R"

   708       by (fold vat_s'.cp_gen_rec[OF eq_x], simp)

   709     finally show ?thesis .

   710   qed

   711 qed

   712 

   713 lemma cp_up:

   714   assumes "(Th th') \<in> ancestors (tRAG s) (Th th)"

   715   and "cp s th' = cp s' th'"

   716   and "(Th th'') \<in> ancestors (tRAG s) (Th th')"

   717   shows "cp s th'' = cp s' th''"

   718 proof -

   719   have "cp_gen s (Th th'') = cp_gen s' (Th th'')"

   720   proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)])

   721     from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]]

   722     show "cp_gen s (Th th') = cp_gen s' (Th th')" by metis

   723   qed

   724   with cp_gen_def_cond[OF refl[of "Th th''"]]

   725   show ?thesis by metis

   726 qed

   727 

   728 end

   729 

   730 locale step_create_cps =

   731   fixes s' th prio s 

   732   defines s_def : "s \<equiv> (Create th prio#s')"

   733   assumes vt_s: "vt s"

   734 

   735 sublocale step_create_cps < vat_s: valid_trace "s"

   736   by (unfold_locales, insert vt_s, simp)

   737 

   738 sublocale step_create_cps < vat_s': valid_trace "s'"

   739   by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp)

   740 

   741 context step_create_cps

   742 begin

   743 

   744 lemma RAG_kept: "RAG s = RAG s'"

   745   by (unfold s_def RAG_create_unchanged, auto)

   746 

   747 lemma tRAG_kept: "tRAG s = tRAG s'"

   748   by (unfold tRAG_alt_def RAG_kept, auto)

   749 

   750 lemma preced_kept:

   751   assumes "th' \<noteq> th"

   752   shows "the_preced s th' = the_preced s' th'"

   753   by (unfold s_def the_preced_def preced_def, insert assms, auto)

   754 

   755 lemma th_not_in: "Th th \<notin> Field (tRAG s')"

   756 proof -

   757   from vt_s[unfolded s_def]

   758   have "PIP s' (Create th prio)" by (cases, simp)

   759   hence "th \<notin> threads s'" by(cases, simp)

   760   from vat_s'.not_in_thread_isolated[OF this]

   761   have "Th th \<notin> Field (RAG s')" .

   762   with tRAG_Field show ?thesis by auto

   763 qed

   764 

   765 lemma eq_cp:

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

   767   shows "cp s th' = cp s' th'"

   768 proof -

   769   have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =

   770         (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"

   771   proof(unfold tRAG_kept, rule f_image_eq)

   772     fix a

   773     assume a_in: "a \<in> subtree (tRAG s') (Th th')"

   774     then obtain th_a where eq_a: "a = Th th_a" 

   775     proof(cases rule:subtreeE)

   776       case 2

   777       from ancestors_Field[OF 2(2)]

   778       and that show ?thesis by (unfold tRAG_alt_def, auto)

   779     qed auto

   780     have neq_th_a: "th_a \<noteq> th"

   781     proof -

   782       have "(Th th) \<notin> subtree (tRAG s') (Th th')"

   783       proof

   784         assume "Th th \<in> subtree (tRAG s') (Th th')"

   785         thus False

   786         proof(cases rule:subtreeE)

   787           case 2

   788           from ancestors_Field[OF this(2)]

   789           and th_not_in[unfolded Field_def]

   790           show ?thesis by auto

   791         qed (insert assms, auto)

   792       qed

   793       with a_in[unfolded eq_a] show ?thesis by auto

   794     qed

   795     from preced_kept[OF this]

   796     show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"

   797       by (unfold eq_a, simp)

   798   qed

   799   thus ?thesis by (unfold cp_alt_def1, simp)

   800 qed

   801 

   802 lemma children_of_th: "RTree.children (tRAG s) (Th th) = {}"

   803 proof -

   804   { fix a

   805     assume "a \<in> RTree.children (tRAG s) (Th th)"

   806     hence "(a, Th th) \<in> tRAG s" by (auto simp:RTree.children_def)

   807     with th_not_in have False 

   808      by (unfold Field_def tRAG_kept, auto)

   809   } thus ?thesis by auto

   810 qed

   811 

   812 lemma eq_cp_th: "cp s th = preced th s"

   813  by (unfold vat_s.cp_rec children_of_th, simp add:the_preced_def)

   814 

   815 end

   816 

   817 locale step_exit_cps =

   818   fixes s' th prio s 

   819   defines s_def : "s \<equiv> Exit th # s'"

   820   assumes vt_s: "vt s"

   821 

   822 sublocale step_exit_cps < vat_s: valid_trace "s"

   823   by (unfold_locales, insert vt_s, simp)

   824 

   825 sublocale step_exit_cps < vat_s': valid_trace "s'"

   826   by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp)

   827 

   828 context step_exit_cps

   829 begin

   830 

   831 lemma preced_kept:

   832   assumes "th' \<noteq> th"

   833   shows "the_preced s th' = the_preced s' th'"

   834   by (unfold s_def the_preced_def preced_def, insert assms, auto)

   835 

   836 lemma RAG_kept: "RAG s = RAG s'"

   837   by (unfold s_def RAG_exit_unchanged, auto)

   838 

   839 lemma tRAG_kept: "tRAG s = tRAG s'"

   840   by (unfold tRAG_alt_def RAG_kept, auto)

   841 

   842 lemma th_ready: "th \<in> readys s'"

   843 proof -

   844   from vt_s[unfolded s_def]

   845   have "PIP s' (Exit th)" by (cases, simp)

   846   hence h: "th \<in> runing s' \<and> holdents s' th = {}" by (cases, metis)

   847   thus ?thesis by (unfold runing_def, auto)

   848 qed

   849 

   850 lemma th_holdents: "holdents s' th = {}"

   851 proof -

   852  from vt_s[unfolded s_def]

   853   have "PIP s' (Exit th)" by (cases, simp)

   854   thus ?thesis by (cases, metis)

   855 qed

   856 

   857 lemma th_RAG: "Th th \<notin> Field (RAG s')"

   858 proof -

   859   have "Th th \<notin> Range (RAG s')"

   860   proof

   861     assume "Th th \<in> Range (RAG s')"

   862     then obtain cs where "holding (wq s') th cs"

   863       by (unfold Range_iff s_RAG_def, auto)

   864     with th_holdents[unfolded holdents_def]

   865     show False by (unfold eq_holding, auto)

   866   qed

   867   moreover have "Th th \<notin> Domain (RAG s')"

   868   proof

   869     assume "Th th \<in> Domain (RAG s')"

   870     then obtain cs where "waiting (wq s') th cs"

   871       by (unfold Domain_iff s_RAG_def, auto)

   872     with th_ready show False by (unfold readys_def eq_waiting, auto)

   873   qed

   874   ultimately show ?thesis by (auto simp:Field_def)

   875 qed

   876 

   877 lemma th_tRAG: "(Th th) \<notin> Field (tRAG s')"

   878   using th_RAG tRAG_Field[of s'] by auto

   879 

   880 lemma eq_cp:

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

   882   shows "cp s th' = cp s' th'"

   883 proof -

   884   have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =

   885         (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"

   886   proof(unfold tRAG_kept, rule f_image_eq)

   887     fix a

   888     assume a_in: "a \<in> subtree (tRAG s') (Th th')"

   889     then obtain th_a where eq_a: "a = Th th_a" 

   890     proof(cases rule:subtreeE)

   891       case 2

   892       from ancestors_Field[OF 2(2)]

   893       and that show ?thesis by (unfold tRAG_alt_def, auto)

   894     qed auto

   895     have neq_th_a: "th_a \<noteq> th"

   896     proof -

   897       from vat_s'.readys_in_no_subtree[OF th_ready assms]

   898       have "(Th th) \<notin> subtree (RAG s') (Th th')" .

   899       with tRAG_subtree_RAG[of s' "Th th'"]

   900       have "(Th th) \<notin> subtree (tRAG s') (Th th')" by auto

   901       with a_in[unfolded eq_a] show ?thesis by auto

   902     qed

   903     from preced_kept[OF this]

   904     show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"

   905       by (unfold eq_a, simp)

   906   qed

   907   thus ?thesis by (unfold cp_alt_def1, simp)

   908 qed

   909 

   910 end

   911 

   912 end

   913