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 ExtGG

     6 imports CpsG

     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 context valid_trace_set

    39 begin

    40 

    41 text {* (* ddd *)

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

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

    44   of the operation (or event).

    45 *}

    46 

    47 

    48 lemma eq_preced:

    49   assumes "th' \<noteq> th"

    50   shows "preced th' (e#s) = preced th' s"

    51 proof -

    52   from assms show ?thesis 

    53     by (unfold is_set, auto simp:preced_def)

    54 qed

    55 

    56 lemma eq_the_preced: 

    57   assumes "th' \<noteq> th"

    58   shows "the_preced (e#s) th' = the_preced s th'"

    59   using assms

    60   by (unfold the_preced_def, intro eq_preced, simp)

    61 

    62 

    63 text {* (* ddd *)

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

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

    66   

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

    68   of @{text "cp"}. 

    69 *}

    70 

    71 lemma eq_cp_pre:

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

    73   shows "cp (e#s) th' = cp s th'"

    74 proof -

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

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

    77         We only need to prove the following: *}

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

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

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

    81   proof -

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

    83     have "?S1 = ?S2" using RAG_unchanged by simp

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

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

    86     proof

    87       fix th1

    88       assume "th1 \<in> ?S2"

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

    90       from eq_the_preced[OF this]

    91       show "the_preced (e#s) th1 = the_preced s th1" .

    92     qed

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

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

    95     thus ?thesis by simp

    96   qed

    97   thus ?thesis by (simp add:cp_alt_def)

    98 qed

    99 

   100 text {*

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

   102   sub-tree of any other thread. 

   103 *}

   104 lemma th_in_no_subtree:

   105   assumes "th' \<noteq> th"

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

   107 proof -

   108   from readys_in_no_subtree[OF th_ready_s assms(1)]

   109   show ?thesis by blast

   110 qed

   111 

   112 text {* 

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

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

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

   116 *}

   117 lemma eq_cp:

   118   assumes "th' \<noteq> th"

   119   shows "cp (e#s) th' = cp s th'"

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

   121 

   122 end

   123 

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

   125 

   126 text {*

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

   128 *}

   129 

   130 

   131 context valid_trace_v

   132 begin

   133 

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

   135 proof -

   136   from readys_root[OF th_ready_s]

   137   show ?thesis

   138   by (unfold root_def, simp)

   139 qed

   140 

   141 lemma edge_of_th:

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

   143 proof -

   144  from holding_th_cs_s

   145  show ?thesis 

   146     by (unfold s_RAG_def holding_eq, auto)

   147 qed

   148 

   149 lemma ancestors_cs: 

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

   151 proof -

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

   153    by (rule rtree_RAG.ancestors_accum[OF edge_of_th])

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

   155 qed

   156 

   157 end

   158 

   159 text {*

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

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

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

   163 *}

   164 

   165 context valid_trace_v_n

   166 begin

   167 

   168 lemma sub_RAGs': 

   169   "{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s"

   170      using next_th_RAG[OF next_th_taker]  .

   171 

   172 lemma ancestors_th': 

   173   "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" 

   174 proof -

   175   have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}"

   176   proof(rule  rtree_RAG.ancestors_accum)

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

   178   qed

   179   thus ?thesis using ancestors_th ancestors_cs by auto

   180 qed

   181 

   182 lemma RAG_s:

   183   "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \<union>

   184                                          {(Cs cs, Th taker)}"

   185  by (unfold RAG_es waiting_set_eq holding_set_eq, auto)

   186 

   187 lemma subtree_kept: (* ddd *)

   188   assumes "th1 \<notin> {th, taker}"

   189   shows "subtree (RAG (e#s)) (Th th1) = 

   190                      subtree (RAG s) (Th th1)" (is "_ = ?R")

   191 proof -

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

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

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

   195   proof(rule subset_del_subtree_outside)

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

   197     proof -

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

   199       proof(rule subtree_refute)

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

   201           by (unfold ancestors_th, simp)

   202       next

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

   204       qed

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

   206       proof(rule subtree_refute)

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

   208           by (unfold ancestors_cs, insert assms, auto)

   209       qed simp

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

   211       thus ?thesis by simp

   212      qed

   213   qed

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

   215   proof(rule subtree_insert_next)

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

   217     proof(rule subtree_refute)

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

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

   220       proof -

   221           have "?R \<subseteq> ancestors (RAG s) (Th taker)" by (rule ancestors_mono, auto)

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

   223           ultimately show ?thesis by auto

   224       qed

   225     next

   226       from assms show "Th th1 \<noteq> Th taker" by simp

   227     qed

   228   qed

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

   230 qed

   231 

   232 lemma cp_kept:

   233   assumes "th1 \<notin> {th, taker}"

   234   shows "cp (e#s) th1 = cp s th1"

   235     by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)

   236 

   237 end

   238 

   239 

   240 context valid_trace_v_e

   241 begin

   242 

   243 find_theorems RAG s e

   244 

   245 lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}"

   246   by (unfold RAG_es waiting_set_eq holding_set_eq, simp)

   247 

   248 lemma subtree_kept:

   249   assumes "th1 \<noteq> th"

   250   shows "subtree (RAG (e#s)) (Th th1) = subtree (RAG s) (Th th1)"

   251 proof(unfold RAG_s, rule subset_del_subtree_outside)

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

   253   proof -

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

   255     proof(rule subtree_refute)

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

   257           by (unfold ancestors_th, simp)

   258     next

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

   260     qed

   261     thus ?thesis by auto

   262   qed

   263 qed

   264 

   265 lemma cp_kept_1:

   266   assumes "th1 \<noteq> th"

   267   shows "cp (e#s) th1 = cp s th1"

   268     by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)

   269 

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

   271 proof -

   272   { fix n

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

   274     proof

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

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

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

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

   279         by (unfold s_RAG_def, auto)

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

   281       from this[unfolded s_RAG_def]

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

   283       from this[unfolded cs_waiting_def]

   284       have "1 < length (wq s cs)"

   285           by (cases "wq s cs", auto)

   286       from holding_next_thI[OF holding_th_cs_s this]

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

   288       thus False using no_taker by blast

   289     qed

   290   } note h = this

   291   {  fix n

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

   293      hence "n = (Cs cs)"

   294      by (elim subtreeE, insert h, auto)

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

   296       by (auto simp:subtree_def)

   297   ultimately show ?thesis by auto 

   298 qed

   299 

   300 lemma subtree_th: 

   301   "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"

   302 proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside)

   303   from edge_of_th

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

   305     by (unfold edges_in_def, auto simp:subtree_def)

   306 qed

   307 

   308 lemma cp_kept_2: 

   309   shows "cp (e#s) th = cp s th" 

   310  by (unfold cp_alt_def subtree_th the_preced_es, auto)

   311 

   312 lemma eq_cp:

   313   shows "cp (e#s) th' = cp s th'"

   314   using cp_kept_1 cp_kept_2

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

   316 

   317 end

   318 

   319 

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

   321 

   322 context valid_trace_p

   323 begin

   324 

   325 lemma root_th: "root (RAG s) (Th th)"

   326   by (simp add: ready_th_s readys_root)

   327 

   328 lemma in_no_others_subtree:

   329   assumes "th' \<noteq> th"

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

   331 proof

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

   333   thus False

   334   proof(cases rule:subtreeE)

   335     case 1

   336     with assms show ?thesis by auto

   337   next

   338     case 2

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

   340   qed

   341 qed

   342 

   343 lemma preced_kept: "the_preced (e#s) = the_preced s"

   344 proof

   345   fix th'

   346   show "the_preced (e # s) th' = the_preced s th'"

   347     by (unfold the_preced_def is_p preced_def, simp)

   348 qed

   349 

   350 end

   351 

   352 

   353 context valid_trace_p_h

   354 begin

   355 

   356 lemma subtree_kept:

   357   assumes "th' \<noteq> th"

   358   shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')"

   359 proof(unfold RAG_es, rule subtree_insert_next)

   360   from in_no_others_subtree[OF assms] 

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

   362 qed

   363 

   364 lemma cp_kept: 

   365   assumes "th' \<noteq> th"

   366   shows "cp (e#s) th' = cp s th'"

   367 proof -

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

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

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

   371   thus ?thesis by (unfold cp_alt_def, simp)

   372 qed

   373 

   374 end

   375 

   376 context valid_trace_p_w

   377 begin

   378 

   379 interpretation vat_e: valid_trace "e#s"

   380   by (unfold_locales, insert vt_e, simp)

   381 

   382 lemma cs_held: "(Cs cs, Th holder) \<in> RAG s"

   383   using holding_s_holder

   384   by (unfold s_RAG_def, fold holding_eq, auto)

   385 

   386 lemma tRAG_s: 

   387   "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"

   388   using local.RAG_tRAG_transfer[OF RAG_es cs_held] .

   389 

   390 lemma cp_kept:

   391   assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"

   392   shows "cp (e#s) th'' = cp s th''"

   393 proof -

   394   have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')"

   395   proof -

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

   397     proof

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

   399       thus False

   400       proof(rule subtreeE)

   401          assume "Th holder = Th th''"

   402          from assms[unfolded tRAG_s ancestors_def, folded this]

   403          show ?thesis by auto

   404       next

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

   406          moreover have "... \<subseteq> ancestors (tRAG (e#s)) (Th holder)"

   407          proof(rule ancestors_mono)

   408             show "tRAG s \<subseteq> tRAG (e#s)" by (unfold tRAG_s, auto)

   409          qed 

   410          ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th holder)" by auto

   411          moreover have "Th holder \<in> ancestors (tRAG (e#s)) (Th th)"

   412            by (unfold tRAG_s, auto simp:ancestors_def)

   413          ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th th)"

   414                        by (auto simp:ancestors_def)

   415          with assms show ?thesis by auto

   416       qed

   417     qed

   418     from subtree_insert_next[OF this]

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

   420     from this[folded tRAG_s] show ?thesis .

   421   qed

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

   423 qed

   424 

   425 lemma cp_gen_update_stop: (* ddd *)

   426   assumes "u \<in> ancestors (tRAG (e#s)) (Th th)"

   427   and "cp_gen (e#s) u = cp_gen s u"

   428   and "y \<in> ancestors (tRAG (e#s)) u"

   429   shows "cp_gen (e#s) y = cp_gen s y"

   430   using assms(3)

   431 proof(induct rule:wf_induct[OF vat_e.fsbttRAGs.wf])

   432   case (1 x)

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

   434   proof -

   435     from tRAG_ancestorsE[OF 1(2)]

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

   437     from vat_e.cp_gen_rec[OF this]

   438     have "?L = 

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

   440     also have "... = 

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

   442     proof -

   443       from preced_kept have "the_preced (e#s) th2 = the_preced s th2" by simp

   444       moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x =

   445                      cp_gen s ` RTree.children (tRAG s) x"

   446       proof -

   447         have "RTree.children (tRAG (e#s)) x =  RTree.children (tRAG s) x"

   448         proof(unfold tRAG_s, rule children_union_kept)

   449           have start: "(Th th, Th holder) \<in> tRAG (e#s)"

   450             by (unfold tRAG_s, auto)

   451           note x_u = 1(2)

   452           show "x \<notin> Range {(Th th, Th holder)}"

   453           proof

   454             assume "x \<in> Range {(Th th, Th holder)}"

   455             hence eq_x: "x = Th holder" using RangeE by auto

   456             show False

   457             proof(cases rule:vat_e.ancestors_headE[OF assms(1) start])

   458               case 1

   459               from x_u[folded this, unfolded eq_x] vat_e.acyclic_tRAG

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

   461             next

   462               case 2

   463               with x_u[unfolded eq_x]

   464               have "(Th holder, Th holder) \<in> (tRAG (e#s))^+" by (auto simp:ancestors_def)

   465               with vat_e.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)

   466             qed

   467           qed

   468         qed

   469         moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x =

   470                        cp_gen s ` RTree.children (tRAG (e#s)) x" (is "?f ` ?A = ?g ` ?A")

   471         proof(rule f_image_eq)

   472           fix a

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

   474           from 1(2)

   475           show "?f a = ?g a"

   476           proof(cases rule:vat_e.rtree_s.ancestors_childrenE[case_names in_ch out_ch])

   477              case in_ch

   478              show ?thesis

   479              proof(cases "a = u")

   480                 case True

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

   482              next

   483                 case False

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

   485                 proof

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

   487                   have "a = u"

   488                   proof(rule vat_e.rtree_s.ancestors_children_unique)

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

   490                                           RTree.children (tRAG (e#s)) x" by auto

   491                   next 

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

   493                                       RTree.children (tRAG (e#s)) x" by auto

   494                   qed

   495                   with False show False by simp

   496                 qed

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

   498                     by (unfold RTree.children_def tRAG_alt_def, auto)

   499                 from cp_kept[OF a_not_in[unfolded eq_a]]

   500                 have "cp (e#s) th_a = cp s th_a" .

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

   502                 show ?thesis .

   503              qed

   504           next

   505             case (out_ch z)

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

   507             show ?thesis

   508             proof(cases "a = z")

   509               case True

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

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

   512               have eq_cp_gen: "cp_gen (e#s) z = cp_gen s z" .

   513               with True show ?thesis by metis

   514             next

   515               case False

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

   517                 by (auto simp:RTree.children_def tRAG_alt_def)

   518               have "a \<notin> ancestors (tRAG (e#s)) (Th th)"

   519               proof

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

   521                 have "a = z"

   522                 proof(rule vat_e.rtree_s.ancestors_children_unique)

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

   524                       by (auto simp:ancestors_def)

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

   526                                        RTree.children (tRAG (e#s)) x" by auto

   527                 next

   528                   from a_in a_in'

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

   530                     by auto

   531                 qed

   532                 with False show False by auto

   533               qed

   534               from cp_kept[OF this[unfolded eq_a]]

   535               have "cp (e#s) th_a = cp s th_a" .

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

   537               show ?thesis .

   538             qed

   539           qed

   540         qed

   541         ultimately show ?thesis by metis

   542       qed

   543       ultimately show ?thesis by simp

   544     qed

   545     also have "... = ?R"

   546       by (fold cp_gen_rec[OF eq_x], simp)

   547     finally show ?thesis .

   548   qed

   549 qed

   550 

   551 lemma cp_up:

   552   assumes "(Th th') \<in> ancestors (tRAG (e#s)) (Th th)"

   553   and "cp (e#s) th' = cp s th'"

   554   and "(Th th'') \<in> ancestors (tRAG (e#s)) (Th th')"

   555   shows "cp (e#s) th'' = cp s th''"

   556 proof -

   557   have "cp_gen (e#s) (Th th'') = cp_gen s (Th th'')"

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

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

   560     show "cp_gen (e#s) (Th th') = cp_gen s (Th th')" by metis

   561   qed

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

   563   show ?thesis by metis

   564 qed

   565 

   566 end

   567 

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

   569 

   570 context valid_trace_create

   571 begin 

   572 

   573 interpretation vat_e: valid_trace "e#s"

   574   by (unfold_locales, insert vt_e, simp)

   575 

   576 lemma tRAG_kept: "tRAG (e#s) = tRAG s"

   577   by (unfold tRAG_alt_def RAG_unchanged, auto)

   578 

   579 lemma preced_kept:

   580   assumes "th' \<noteq> th"

   581   shows "the_preced (e#s) th' = the_preced s th'"

   582   by (unfold the_preced_def preced_def is_create, insert assms, auto)

   583 

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

   585   by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s)

   586 

   587 lemma eq_cp:

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

   589   shows "cp (e#s) th' = cp s th'"

   590 proof -

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

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

   593   proof(unfold tRAG_kept, rule f_image_eq)

   594     fix a

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

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

   597     proof(cases rule:subtreeE)

   598       case 2

   599       from ancestors_Field[OF 2(2)]

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

   601     qed auto

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

   603     proof -

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

   605       proof

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

   607         thus False

   608         proof(cases rule:subtreeE)

   609           case 2

   610           from ancestors_Field[OF this(2)]

   611           and th_not_in[unfolded Field_def]

   612           show ?thesis by auto

   613         qed (insert assms, auto)

   614       qed

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

   616     qed

   617     from preced_kept[OF this]

   618     show "(the_preced (e#s) \<circ> the_thread) a = (the_preced s \<circ> the_thread) a"

   619       by (unfold eq_a, simp)

   620   qed

   621   thus ?thesis by (unfold cp_alt_def1, simp)

   622 qed

   623 

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

   625 proof -

   626   { fix a

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

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

   629     with th_not_in have False 

   630      by (unfold Field_def tRAG_kept, auto)

   631   } thus ?thesis by auto

   632 qed

   633 

   634 lemma eq_cp_th: "cp (e#s) th = preced th (e#s)"

   635  by (unfold vat_e.cp_rec children_of_th, simp add:the_preced_def)

   636 

   637 end

   638 

   639 

   640 context valid_trace_exit

   641 begin

   642 

   643 lemma preced_kept:

   644   assumes "th' \<noteq> th"

   645   shows "the_preced (e#s) th' = the_preced s th'"

   646   using assms

   647   by (unfold the_preced_def is_exit preced_def, simp)

   648 

   649 lemma tRAG_kept: "tRAG (e#s) = tRAG s"

   650   by (unfold tRAG_alt_def RAG_unchanged, auto)

   651 

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

   653 proof -

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

   655   proof

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

   657     then obtain cs where "holding (wq s) th cs"

   658       by (unfold Range_iff s_RAG_def, auto)

   659     with holdents_th_s[unfolded holdents_def]

   660     show False by (unfold holding_eq, auto)

   661   qed

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

   663   proof

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

   665     then obtain cs where "waiting (wq s) th cs"

   666       by (unfold Domain_iff s_RAG_def, auto)

   667     with th_ready_s show False by (unfold readys_def waiting_eq, auto)

   668   qed

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

   670 qed

   671 

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

   673   using th_RAG tRAG_Field by auto

   674 

   675 lemma eq_cp:

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

   677   shows "cp (e#s) th' = cp s th'"

   678 proof -

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

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

   681   proof(unfold tRAG_kept, rule f_image_eq)

   682     fix a

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

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

   685     proof(cases rule:subtreeE)

   686       case 2

   687       from ancestors_Field[OF 2(2)]

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

   689     qed auto

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

   691     proof -

   692       from readys_in_no_subtree[OF th_ready_s assms]

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

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

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

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

   697     qed

   698     from preced_kept[OF this]

   699     show "(the_preced (e#s) \<circ> the_thread) a = (the_preced s \<circ> the_thread) a"

   700       by (unfold eq_a, simp)

   701   qed

   702   thus ?thesis by (unfold cp_alt_def1, simp)

   703 qed

   704 

   705 end

   706 

   707 end

   708