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 

    26   The reason RAG changing affects current precedence is that,

    27   according to the definition, current precedence 

    28   of a thread is the maximum of the precedences of every threads in its subtree, 

    29   where the notion of sub-tree in RAG is defined in RTree.thy.

    30 

    31   Therefore, for each operation, lemmas about the change of precedences 

    32   and RAG are derived first, on which lemmas about current precedence 

    33   recalculation are based on.

    34 *}

    35 

    36 section {* The @{term Set} operation *}

    37 

    38 text {* (* ddd *)

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

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

    41 *}

    42 locale step_set_cps =

    43   fixes s' th prio s 

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

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

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

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

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

    49   assumes vt_s: "vt s"

    50 

    51 sublocale step_set_cps < vat_s : valid_trace "s"

    52 proof

    53   from vt_s show "vt s" .

    54 qed

    55 

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

    57 proof

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

    59 qed

    60 

    61 context step_set_cps 

    62 begin

    63 

    64 text {* (* ddd *)

    65   The following two lemmas confirm that @{text "Set"}-operation

    66   only changes the precedence of the initiating thread (or actor)

    67   of the operation (or event).

    68 *}

    69 

    70 lemma eq_preced:

    71   assumes "th' \<noteq> th"

    72   shows "preced th' s = preced th' s'"

    73 proof -

    74   from assms show ?thesis 

    75     by (unfold s_def, auto simp:preced_def)

    76 qed

    77 

    78 lemma eq_the_preced: 

    79   assumes "th' \<noteq> th"

    80   shows "the_preced s th' = the_preced s' th'"

    81   using assms

    82   by (unfold the_preced_def, intro eq_preced, simp)

    83 

    84 text {*

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

    86 *}

    87 

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

    89   by (unfold s_def RAG_set_unchanged, auto)

    90 

    91 text {* (* ddd *)

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

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

    94   

    95   The proof of this lemma is simplified by using the alternative definition 

    96   of @{text "cp"}. 

    97 *}

    98 

    99 lemma eq_cp_pre:

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

   101   shows "cp s th' = cp s' th'"

   102 proof -

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

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

   105         We only need to prove the following: *}

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

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

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

   109   proof -

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

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

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

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

   114     proof

   115       fix th1

   116       assume "th1 \<in> ?S2"

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

   118       from eq_the_preced[OF this]

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

   120     qed

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

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

   123     thus ?thesis by simp

   124   qed

   125   thus ?thesis by (simp add:cp_alt_def)

   126 qed

   127 

   128 text {*

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

   130   sub-tree of any other thread. 

   131 *}

   132 lemma th_in_no_subtree:

   133   assumes "th' \<noteq> th"

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

   135 proof -

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

   137   proof -

   138     from step_back_step [OF vt_s[unfolded s_def]]

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

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

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

   142   qed

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

   144   show ?thesis by blast

   145 qed

   146 

   147 text {* 

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

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

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

   151 *}

   152 lemma eq_cp:

   153   assumes "th' \<noteq> th"

   154   shows "cp s th' = cp s' th'"

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

   156 

   157 end

   158 

   159 section {* The @{term V} operation *}

   160 

   161 text {*

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

   163 *}

   164 

   165 locale step_v_cps =

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

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

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

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

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

   171   assumes vt_s: "vt s"

   172 

   173 sublocale step_v_cps < vat_s : valid_trace "s"

   174 proof

   175   from vt_s show "vt s" .

   176 qed

   177 

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

   179 proof

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

   181 qed

   182 

   183 context step_v_cps

   184 begin

   185 

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

   187   using step_back_step[OF vt_s[unfolded s_def]]

   188   by (cases, simp add:runing_def)

   189 

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

   191 proof -

   192   from vat_s'.readys_root[OF ready_th_s']

   193   show ?thesis

   194   by (unfold root_def, simp)

   195 qed

   196 

   197 lemma holding_th: "holding s' th cs"

   198 proof -

   199   from vt_s[unfolded s_def]

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

   201   thus ?thesis by (cases, auto)

   202 qed

   203 

   204 lemma edge_of_th:

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

   206 proof -

   207  from holding_th

   208  show ?thesis 

   209     by (unfold s_RAG_def holding_eq, auto)

   210 qed

   211 

   212 lemma ancestors_cs: 

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

   214 proof -

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

   216   proof(rule vat_s'.rtree_RAG.ancestors_accum)

   217     from vt_s[unfolded s_def]

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

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

   220     proof(cases)

   221       assume "holding s' th cs"

   222       from this[unfolded holding_eq]

   223       show ?thesis by (unfold s_RAG_def, auto)

   224     qed

   225   qed

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

   227 qed

   228 

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

   230   by (auto simp: s_def the_preced_def preced_def)

   231 

   232 end

   233 

   234 text {*

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

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

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

   238 *}

   239 locale step_v_cps_nt = step_v_cps +

   240   fixes th'

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

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

   243 

   244 context step_v_cps_nt

   245 begin

   246 

   247 text {*

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

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

   250 *}

   251 

   252 (*

   253   RAG before the V-operation

   254     th1 ----|

   255             |

   256     th' ----|

   257             |----> cs -----|

   258     th2 ----|              |

   259             |              |

   260     th3 ----|              |

   261                            |------> th

   262     th4 ----|              |

   263             |              |

   264     th5 ----|              |

   265             |----> cs'-----|

   266     th6 ----|

   267             |

   268     th7 ----|

   269 

   270  RAG after the V-operation

   271     th1 ----|

   272             |

   273             |----> cs ----> th'

   274     th2 ----|              

   275             |              

   276     th3 ----|              

   277                            

   278     th4 ----|              

   279             |              

   280     th5 ----|              

   281             |----> cs'----> th

   282     th6 ----|

   283             |

   284     th7 ----|

   285 *)

   286 

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

   288                 using next_th_RAG[OF nt]  .

   289 

   290 lemma ancestors_th': 

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

   292 proof -

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

   294   proof(rule  vat_s'.rtree_RAG.ancestors_accum)

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

   296   qed

   297   thus ?thesis using ancestors_th ancestors_cs by auto

   298 qed

   299 

   300 lemma RAG_s:

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

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

   303 proof -

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

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

   306 qed

   307 

   308 lemma subtree_kept: (* ddd *)

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

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

   311 proof -

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

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

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

   315   proof(rule subset_del_subtree_outside)

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

   317     proof -

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

   319       proof(rule subtree_refute)

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

   321           by (unfold ancestors_th, simp)

   322       next

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

   324       qed

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

   326       proof(rule subtree_refute)

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

   328           by (unfold ancestors_cs, insert assms, auto)

   329       qed simp

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

   331       thus ?thesis by simp

   332      qed

   333   qed

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

   335   proof(rule subtree_insert_next)

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

   337     proof(rule subtree_refute)

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

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

   340       proof -

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

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

   343           ultimately show ?thesis by auto

   344       qed

   345     next

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

   347     qed

   348   qed

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

   350 qed

   351 

   352 lemma cp_kept:

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

   354   shows "cp s th1 = cp s' th1"

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

   356 

   357 end

   358 

   359 locale step_v_cps_nnt = step_v_cps +

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

   361 

   362 context step_v_cps_nnt

   363 begin

   364 

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

   366 proof -

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

   368   show ?thesis by auto

   369 qed

   370 

   371 lemma subtree_kept:

   372   assumes "th1 \<noteq> th"

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

   374 proof(unfold RAG_s, rule subset_del_subtree_outside)

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

   376   proof -

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

   378     proof(rule subtree_refute)

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

   380           by (unfold ancestors_th, simp)

   381     next

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

   383     qed

   384     thus ?thesis by auto

   385   qed

   386 qed

   387 

   388 lemma cp_kept_1:

   389   assumes "th1 \<noteq> th"

   390   shows "cp s th1 = cp s' th1"

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

   392 

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

   394 proof -

   395   { fix n

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

   397     proof

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

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

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

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

   402         by (unfold s_RAG_def, auto)

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

   404       from this[unfolded s_RAG_def]

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

   406       from this[unfolded cs_waiting_def]

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

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

   409       from holding_next_thI[OF holding_th this]

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

   411       with nnt show False by auto

   412     qed

   413   } note h = this

   414   {  fix n

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

   416      hence "n = (Cs cs)"

   417      by (elim subtreeE, insert h, auto)

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

   419       by (auto simp:subtree_def)

   420   ultimately show ?thesis by auto 

   421 qed

   422 

   423 lemma subtree_th: 

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

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

   426   from edge_of_th

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

   428     by (unfold edges_in_def, auto simp:subtree_def)

   429 qed

   430 

   431 lemma cp_kept_2: 

   432   shows "cp s th = cp s' th" 

   433  by (unfold cp_alt_def subtree_th preced_kept, auto)

   434 

   435 lemma eq_cp:

   436   shows "cp s th' = cp s' th'"

   437   using cp_kept_1 cp_kept_2

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

   439 end

   440 

   441 

   442 locale step_P_cps =

   443   fixes s' th cs s 

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

   445   assumes vt_s: "vt s"

   446 

   447 sublocale step_P_cps < vat_s : valid_trace "s"

   448 proof

   449   from vt_s show "vt s" .

   450 qed

   451 

   452 section {* The @{term P} operation *}

   453 

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

   455 proof

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

   457 qed

   458 

   459 context step_P_cps

   460 begin

   461 

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

   463 proof -

   464     from step_back_step [OF vt_s[unfolded s_def]]

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

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

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

   468 qed

   469 

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

   471   using readys_root[OF readys_th] .

   472 

   473 lemma in_no_others_subtree:

   474   assumes "th' \<noteq> th"

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

   476 proof

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

   478   thus False

   479   proof(cases rule:subtreeE)

   480     case 1

   481     with assms show ?thesis by auto

   482   next

   483     case 2

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

   485   qed

   486 qed

   487 

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

   489   by (auto simp: s_def the_preced_def preced_def)

   490 

   491 end

   492 

   493 locale step_P_cps_ne =step_P_cps +

   494   fixes th'

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

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

   497 

   498 locale step_P_cps_e =step_P_cps +

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

   500 

   501 context step_P_cps_e

   502 begin

   503 

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

   505 proof -

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

   507   show ?thesis by auto

   508 qed

   509 

   510 lemma subtree_kept:

   511   assumes "th' \<noteq> th"

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

   513 proof(unfold RAG_s, rule subtree_insert_next)

   514   from in_no_others_subtree[OF assms] 

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

   516 qed

   517 

   518 lemma cp_kept: 

   519   assumes "th' \<noteq> th"

   520   shows "cp s th' = cp s' th'"

   521 proof -

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

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

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

   525   thus ?thesis by (unfold cp_alt_def, simp)

   526 qed

   527 

   528 end

   529 

   530 context step_P_cps_ne 

   531 begin

   532 

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

   534 proof -

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

   536   show ?thesis by (simp add:s_def)

   537 qed

   538 

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

   540 proof -

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

   542   proof -

   543     from ne

   544     have " holding s' th' cs"

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

   546     thus ?thesis 

   547       by (unfold hRAG_def, auto)

   548   qed

   549   thus ?thesis by (unfold RAG_split, auto)

   550 qed

   551 

   552 lemma tRAG_s: 

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

   554   using RAG_tRAG_transfer[OF RAG_s cs_held] .

   555 

   556 lemma cp_kept:

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

   558   shows "cp s th'' = cp s' th''"

   559 proof -

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

   561   proof -

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

   563     proof

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

   565       thus False

   566       proof(rule subtreeE)

   567          assume "Th th' = Th th''"

   568          from assms[unfolded tRAG_s ancestors_def, folded this]

   569          show ?thesis by auto

   570       next

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

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

   573          proof(rule ancestors_mono)

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

   575          qed 

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

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

   578            by (unfold tRAG_s, auto simp:ancestors_def)

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

   580                        by (auto simp:ancestors_def)

   581          with assms show ?thesis by auto

   582       qed

   583     qed

   584     from subtree_insert_next[OF this]

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

   586     from this[folded tRAG_s] show ?thesis .

   587   qed

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

   589 qed

   590 

   591 lemma cp_gen_update_stop: (* ddd *)

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

   593   and "cp_gen s u = cp_gen s' u"

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

   595   shows "cp_gen s y = cp_gen s' y"

   596   using assms(3)

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

   598   case (1 x)

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

   600   proof -

   601     from tRAG_ancestorsE[OF 1(2)]

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

   603     from vat_s.cp_gen_rec[OF this]

   604     have "?L = 

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

   606     also have "... = 

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

   608   

   609     proof -

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

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

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

   613       proof -

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

   615         proof(unfold tRAG_s, rule children_union_kept)

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

   617             by (unfold tRAG_s, auto)

   618           note x_u = 1(2)

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

   620           proof

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

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

   623             show False

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

   625               case 1

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

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

   628             next

   629               case 2

   630               with x_u[unfolded eq_x]

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

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

   633             qed

   634           qed

   635         qed

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

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

   638         proof(rule f_image_eq)

   639           fix a

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

   641           from 1(2)

   642           show "?f a = ?g a"

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

   644              case in_ch

   645              show ?thesis

   646              proof(cases "a = u")

   647                 case True

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

   649              next

   650                 case False

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

   652                 proof

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

   654                   have "a = u"

   655                   proof(rule vat_s.rtree_s.ancestors_children_unique)

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

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

   658                   next 

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

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

   661                   qed

   662                   with False show False by simp

   663                 qed

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

   665                     by (unfold RTree.children_def tRAG_alt_def, auto)

   666                 from cp_kept[OF a_not_in[unfolded eq_a]]

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

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

   669                 show ?thesis .

   670              qed

   671           next

   672             case (out_ch z)

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

   674             show ?thesis

   675             proof(cases "a = z")

   676               case True

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

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

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

   680               with True show ?thesis by metis

   681             next

   682               case False

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

   684                 by (auto simp:RTree.children_def tRAG_alt_def)

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

   686               proof

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

   688                 have "a = z"

   689                 proof(rule vat_s.rtree_s.ancestors_children_unique)

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

   691                       by (auto simp:ancestors_def)

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

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

   694                 next

   695                   from a_in a_in'

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

   697                     by auto

   698                 qed

   699                 with False show False by auto

   700               qed

   701               from cp_kept[OF this[unfolded eq_a]]

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

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

   704               show ?thesis .

   705             qed

   706           qed

   707         qed

   708         ultimately show ?thesis by metis

   709       qed

   710       ultimately show ?thesis by simp

   711     qed

   712     also have "... = ?R"

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

   714     finally show ?thesis .

   715   qed

   716 qed

   717 

   718 lemma cp_up:

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

   720   and "cp s th' = cp s' th'"

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

   722   shows "cp s th'' = cp s' th''"

   723 proof -

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

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

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

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

   728   qed

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

   730   show ?thesis by metis

   731 qed

   732 

   733 end

   734 

   735 section {* The @{term Create} operation *}

   736 

   737 locale step_create_cps =

   738   fixes s' th prio s 

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

   740   assumes vt_s: "vt s"

   741 

   742 sublocale step_create_cps < vat_s: valid_trace "s"

   743   by (unfold_locales, insert vt_s, simp)

   744 

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

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

   747 

   748 context step_create_cps

   749 begin

   750 

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

   752   by (unfold s_def RAG_create_unchanged, auto)

   753 

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

   755   by (unfold tRAG_alt_def RAG_kept, auto)

   756 

   757 lemma preced_kept:

   758   assumes "th' \<noteq> th"

   759   shows "the_preced s th' = the_preced s' th'"

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

   761 

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

   763 proof -

   764   from vt_s[unfolded s_def]

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

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

   767   from vat_s'.not_in_thread_isolated[OF this]

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

   769   with tRAG_Field show ?thesis by auto

   770 qed

   771 

   772 lemma eq_cp:

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

   774   shows "cp s th' = cp s' th'"

   775 proof -

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

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

   778   proof(unfold tRAG_kept, rule f_image_eq)

   779     fix a

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

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

   782     proof(cases rule:subtreeE)

   783       case 2

   784       from ancestors_Field[OF 2(2)]

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

   786     qed auto

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

   788     proof -

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

   790       proof

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

   792         thus False

   793         proof(cases rule:subtreeE)

   794           case 2

   795           from ancestors_Field[OF this(2)]

   796           and th_not_in[unfolded Field_def]

   797           show ?thesis by auto

   798         qed (insert assms, auto)

   799       qed

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

   801     qed

   802     from preced_kept[OF this]

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

   804       by (unfold eq_a, simp)

   805   qed

   806   thus ?thesis by (unfold cp_alt_def1, simp)

   807 qed

   808 

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

   810 proof -

   811   { fix a

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

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

   814     with th_not_in have False 

   815      by (unfold Field_def tRAG_kept, auto)

   816   } thus ?thesis by auto

   817 qed

   818 

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

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

   821 

   822 end

   823 

   824 locale step_exit_cps =

   825   fixes s' th prio s 

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

   827   assumes vt_s: "vt s"

   828 

   829 sublocale step_exit_cps < vat_s: valid_trace "s"

   830   by (unfold_locales, insert vt_s, simp)

   831 

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

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

   834 

   835 context step_exit_cps

   836 begin

   837 

   838 lemma preced_kept:

   839   assumes "th' \<noteq> th"

   840   shows "the_preced s th' = the_preced s' th'"

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

   842 

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

   844   by (unfold s_def RAG_exit_unchanged, auto)

   845 

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

   847   by (unfold tRAG_alt_def RAG_kept, auto)

   848 

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

   850 proof -

   851   from vt_s[unfolded s_def]

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

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

   854   thus ?thesis by (unfold runing_def, auto)

   855 qed

   856 

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

   858 proof -

   859  from vt_s[unfolded s_def]

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

   861   thus ?thesis by (cases, metis)

   862 qed

   863 

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

   865 proof -

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

   867   proof

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

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

   870       by (unfold Range_iff s_RAG_def, auto)

   871     with th_holdents[unfolded holdents_def]

   872     show False by (unfold eq_holding, auto)

   873   qed

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

   875   proof

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

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

   878       by (unfold Domain_iff s_RAG_def, auto)

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

   880   qed

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

   882 qed

   883 

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

   885   using th_RAG tRAG_Field[of s'] by auto

   886 

   887 lemma eq_cp:

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

   889   shows "cp s th' = cp s' th'"

   890 proof -

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

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

   893   proof(unfold tRAG_kept, rule f_image_eq)

   894     fix a

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

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

   897     proof(cases rule:subtreeE)

   898       case 2

   899       from ancestors_Field[OF 2(2)]

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

   901     qed auto

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

   903     proof -

   904       from vat_s'.readys_in_no_subtree[OF th_ready assms]

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

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

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

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

   909     qed

   910     from preced_kept[OF this]

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

   912       by (unfold eq_a, simp)

   913   qed

   914   thus ?thesis by (unfold cp_alt_def1, simp)

   915 qed

   916 

   917 end

   918 

   919 end

   920