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 

   709 =======

   710 theory ExtGG

   711 imports PrioG CpsG

   712 begin

   713 

   714 text {* 

   715   The following two auxiliary lemmas are used to reason about @{term Max}.

   716 *}

   717 lemma image_Max_eqI: 

   718   assumes "finite B"

   719   and "b \<in> B"

   720   and "\<forall> x \<in> B. f x \<le> f b"

   721   shows "Max (f ` B) = f b"

   722   using assms

   723   using Max_eqI by blast 

   724 

   725 lemma image_Max_subset:

   726   assumes "finite A"

   727   and "B \<subseteq> A"

   728   and "a \<in> B"

   729   and "Max (f ` A) = f a"

   730   shows "Max (f ` B) = f a"

   731 proof(rule image_Max_eqI)

   732   show "finite B"

   733     using assms(1) assms(2) finite_subset by auto 

   734 next

   735   show "a \<in> B" using assms by simp

   736 next

   737   show "\<forall>x\<in>B. f x \<le> f a"

   738     by (metis Max_ge assms(1) assms(2) assms(4) 

   739             finite_imageI image_eqI subsetCE) 

   740 qed

   741 

   742 text {*

   743   The following locale @{text "highest_gen"} sets the basic context for our

   744   investigation: supposing thread @{text th} holds the highest @{term cp}-value

   745   in state @{text s}, which means the task for @{text th} is the 

   746   most urgent. We want to show that  

   747   @{text th} is treated correctly by PIP, which means

   748   @{text th} will not be blocked unreasonably by other less urgent

   749   threads. 

   750 *}

   751 locale highest_gen =

   752   fixes s th prio tm

   753   assumes vt_s: "vt s"

   754   and threads_s: "th \<in> threads s"

   755   and highest: "preced th s = Max ((cp s)`threads s)"

   756   -- {* The internal structure of @{term th}'s precedence is exposed:*}

   757   and preced_th: "preced th s = Prc prio tm" 

   758 

   759 -- {* @{term s} is a valid trace, so it will inherit all results derived for

   760       a valid trace: *}

   761 sublocale highest_gen < vat_s: valid_trace "s"

   762   by (unfold_locales, insert vt_s, simp)

   763 

   764 context highest_gen

   765 begin

   766 

   767 text {*

   768   @{term tm} is the time when the precedence of @{term th} is set, so 

   769   @{term tm} must be a valid moment index into @{term s}.

   770 *}

   771 lemma lt_tm: "tm < length s"

   772   by (insert preced_tm_lt[OF threads_s preced_th], simp)

   773 

   774 text {*

   775   Since @{term th} holds the highest precedence and @{text "cp"}

   776   is the highest precedence of all threads in the sub-tree of 

   777   @{text "th"} and @{text th} is among these threads, 

   778   its @{term cp} must equal to its precedence:

   779 *}

   780 lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")

   781 proof -

   782   have "?L \<le> ?R"

   783   by (unfold highest, rule Max_ge, 

   784         auto simp:threads_s finite_threads)

   785   moreover have "?R \<le> ?L"

   786     by (unfold vat_s.cp_rec, rule Max_ge, 

   787         auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)

   788   ultimately show ?thesis by auto

   789 qed

   790 

   791 (* ccc *)

   792 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"

   793   by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp)

   794 

   795 lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)"

   796   by (fold eq_cp_s_th, unfold highest_cp_preced, simp)

   797 

   798 lemma highest': "cp s th = Max (cp s ` threads s)"

   799 proof -

   800   from highest_cp_preced max_cp_eq[symmetric]

   801   show ?thesis by simp

   802 qed

   803 

   804 end

   805 

   806 locale extend_highest_gen = highest_gen + 

   807   fixes t 

   808   assumes vt_t: "vt (t@s)"

   809   and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"

   810   and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"

   811   and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"

   812 

   813 sublocale extend_highest_gen < vat_t: valid_trace "t@s"

   814   by (unfold_locales, insert vt_t, simp)

   815 

   816 lemma step_back_vt_app: 

   817   assumes vt_ts: "vt (t@s)" 

   818   shows "vt s"

   819 proof -

   820   from vt_ts show ?thesis

   821   proof(induct t)

   822     case Nil

   823     from Nil show ?case by auto

   824   next

   825     case (Cons e t)

   826     assume ih: " vt (t @ s) \<Longrightarrow> vt s"

   827       and vt_et: "vt ((e # t) @ s)"

   828     show ?case

   829     proof(rule ih)

   830       show "vt (t @ s)"

   831       proof(rule step_back_vt)

   832         from vt_et show "vt (e # t @ s)" by simp

   833       qed

   834     qed

   835   qed

   836 qed

   837 

   838 

   839 locale red_extend_highest_gen = extend_highest_gen +

   840    fixes i::nat

   841 

   842 sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"

   843   apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])

   844   apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)

   845   by (unfold highest_gen_def, auto dest:step_back_vt_app)

   846 

   847 

   848 context extend_highest_gen

   849 begin

   850 

   851  lemma ind [consumes 0, case_names Nil Cons, induct type]:

   852   assumes 

   853     h0: "R []"

   854   and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e; 

   855                     extend_highest_gen s th prio tm t; 

   856                     extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"

   857   shows "R t"

   858 proof -

   859   from vt_t extend_highest_gen_axioms show ?thesis

   860   proof(induct t)

   861     from h0 show "R []" .

   862   next

   863     case (Cons e t')

   864     assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"

   865       and vt_e: "vt ((e # t') @ s)"

   866       and et: "extend_highest_gen s th prio tm (e # t')"

   867     from vt_e and step_back_step have stp: "step (t'@s) e" by auto

   868     from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto

   869     show ?case

   870     proof(rule h2 [OF vt_ts stp _ _ _ ])

   871       show "R t'"

   872       proof(rule ih)

   873         from et show ext': "extend_highest_gen s th prio tm t'"

   874           by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

   875       next

   876         from vt_ts show "vt (t' @ s)" .

   877       qed

   878     next

   879       from et show "extend_highest_gen s th prio tm (e # t')" .

   880     next

   881       from et show ext': "extend_highest_gen s th prio tm t'"

   882           by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

   883     qed

   884   qed

   885 qed

   886 

   887 

   888 lemma th_kept: "th \<in> threads (t @ s) \<and> 

   889                  preced th (t@s) = preced th s" (is "?Q t") 

   890 proof -

   891   show ?thesis

   892   proof(induct rule:ind)

   893     case Nil

   894     from threads_s

   895     show ?case

   896       by auto

   897   next

   898     case (Cons e t)

   899     interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto

   900     interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto

   901     show ?case

   902     proof(cases e)

   903       case (Create thread prio)

   904       show ?thesis

   905       proof -

   906         from Cons and Create have "step (t@s) (Create thread prio)" by auto

   907         hence "th \<noteq> thread"

   908         proof(cases)

   909           case thread_create

   910           with Cons show ?thesis by auto

   911         qed

   912         hence "preced th ((e # t) @ s)  = preced th (t @ s)"

   913           by (unfold Create, auto simp:preced_def)

   914         moreover note Cons

   915         ultimately show ?thesis

   916           by (auto simp:Create)

   917       qed

   918     next

   919       case (Exit thread)

   920       from h_e.exit_diff and Exit

   921       have neq_th: "thread \<noteq> th" by auto

   922       with Cons

   923       show ?thesis

   924         by (unfold Exit, auto simp:preced_def)

   925     next

   926       case (P thread cs)

   927       with Cons

   928       show ?thesis 

   929         by (auto simp:P preced_def)

   930     next

   931       case (V thread cs)

   932       with Cons

   933       show ?thesis 

   934         by (auto simp:V preced_def)

   935     next

   936       case (Set thread prio')

   937       show ?thesis

   938       proof -

   939         from h_e.set_diff_low and Set

   940         have "th \<noteq> thread" by auto

   941         hence "preced th ((e # t) @ s)  = preced th (t @ s)"

   942           by (unfold Set, auto simp:preced_def)

   943         moreover note Cons

   944         ultimately show ?thesis

   945           by (auto simp:Set)

   946       qed

   947     qed

   948   qed

   949 qed

   950 

   951 text {*

   952   According to @{thm th_kept}, thread @{text "th"} has its living status

   953   and precedence kept along the way of @{text "t"}. The following lemma

   954   shows that this preserved precedence of @{text "th"} remains as the highest

   955   along the way of @{text "t"}.

   956 

   957   The proof goes by induction over @{text "t"} using the specialized

   958   induction rule @{thm ind}, followed by case analysis of each possible 

   959   operations of PIP. All cases follow the same pattern rendered by the 

   960   generalized introduction rule @{thm "image_Max_eqI"}. 

   961 

   962   The very essence is to show that precedences, no matter whether they are newly introduced 

   963   or modified, are always lower than the one held by @{term "th"},

   964   which by @{thm th_kept} is preserved along the way.

   965 *}

   966 lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"

   967 proof(induct rule:ind)

   968   case Nil

   969   from highest_preced_thread

   970   show ?case

   971     by (unfold the_preced_def, simp)

   972 next

   973   case (Cons e t)

   974     interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto

   975     interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto

   976   show ?case

   977   proof(cases e)

   978     case (Create thread prio')

   979     show ?thesis (is "Max (?f ` ?A) = ?t")

   980     proof -

   981       -- {* The following is the common pattern of each branch of the case analysis. *}

   982       -- {* The major part is to show that @{text "th"} holds the highest precedence: *}

   983       have "Max (?f ` ?A) = ?f th"

   984       proof(rule image_Max_eqI)

   985         show "finite ?A" using h_e.finite_threads by auto 

   986       next

   987         show "th \<in> ?A" using h_e.th_kept by auto 

   988       next

   989         show "\<forall>x\<in>?A. ?f x \<le> ?f th"

   990         proof 

   991           fix x

   992           assume "x \<in> ?A"

   993           hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create)

   994           thus "?f x \<le> ?f th"

   995           proof

   996             assume "x = thread"

   997             thus ?thesis 

   998               apply (simp add:Create the_preced_def preced_def, fold preced_def)

   999               using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force

  1000           next

  1001             assume h: "x \<in> threads (t @ s)"

  1002             from Cons(2)[unfolded Create] 

  1003             have "x \<noteq> thread" using h by (cases, auto)

  1004             hence "?f x = the_preced (t@s) x" 

  1005               by (simp add:Create the_preced_def preced_def)

  1006             hence "?f x \<le> Max (the_preced (t@s) ` threads (t@s))"

  1007               by (simp add: h_t.finite_threads h)

  1008             also have "... = ?f th"

  1009               by (metis Cons.hyps(5) h_e.th_kept the_preced_def) 

  1010             finally show ?thesis .

  1011           qed

  1012         qed

  1013       qed

  1014      -- {* The minor part is to show that the precedence of @{text "th"} 

  1015            equals to preserved one, given by the foregoing lemma @{thm th_kept} *}

  1016       also have "... = ?t" using h_e.th_kept the_preced_def by auto

  1017       -- {* Then it follows trivially that the precedence preserved

  1018             for @{term "th"} remains the maximum of all living threads along the way. *}

  1019       finally show ?thesis .

  1020     qed 

  1021   next 

  1022     case (Exit thread)

  1023     show ?thesis (is "Max (?f ` ?A) = ?t")

  1024     proof -

  1025       have "Max (?f ` ?A) = ?f th"

  1026       proof(rule image_Max_eqI)

  1027         show "finite ?A" using h_e.finite_threads by auto 

  1028       next

  1029         show "th \<in> ?A" using h_e.th_kept by auto 

  1030       next

  1031         show "\<forall>x\<in>?A. ?f x \<le> ?f th"

  1032         proof 

  1033           fix x

  1034           assume "x \<in> ?A"

  1035           hence "x \<in> threads (t@s)" by (simp add: Exit) 

  1036           hence "?f x \<le> Max (?f ` threads (t@s))" 

  1037             by (simp add: h_t.finite_threads) 

  1038           also have "... \<le> ?f th" 

  1039             apply (simp add:Exit the_preced_def preced_def, fold preced_def)

  1040             using Cons.hyps(5) h_t.th_kept the_preced_def by auto

  1041           finally show "?f x \<le> ?f th" .

  1042         qed

  1043       qed

  1044       also have "... = ?t" using h_e.th_kept the_preced_def by auto

  1045       finally show ?thesis .

  1046     qed 

  1047   next

  1048     case (P thread cs)

  1049     with Cons

  1050     show ?thesis by (auto simp:preced_def the_preced_def)

  1051   next

  1052     case (V thread cs)

  1053     with Cons

  1054     show ?thesis by (auto simp:preced_def the_preced_def)

  1055   next 

  1056     case (Set thread prio')

  1057     show ?thesis (is "Max (?f ` ?A) = ?t")

  1058     proof -

  1059       have "Max (?f ` ?A) = ?f th"

  1060       proof(rule image_Max_eqI)

  1061         show "finite ?A" using h_e.finite_threads by auto 

  1062       next

  1063         show "th \<in> ?A" using h_e.th_kept by auto 

  1064       next

  1065         show "\<forall>x\<in>?A. ?f x \<le> ?f th"

  1066         proof 

  1067           fix x

  1068           assume h: "x \<in> ?A"

  1069           show "?f x \<le> ?f th"

  1070           proof(cases "x = thread")

  1071             case True

  1072             moreover have "the_preced (Set thread prio' # t @ s) thread \<le> the_preced (t @ s) th"

  1073             proof -

  1074               have "the_preced (t @ s) th = Prc prio tm"  

  1075                 using h_t.th_kept preced_th by (simp add:the_preced_def)

  1076               moreover have "prio' \<le> prio" using Set h_e.set_diff_low by auto

  1077               ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def)

  1078             qed

  1079             ultimately show ?thesis

  1080               by (unfold Set, simp add:the_preced_def preced_def)

  1081           next

  1082             case False

  1083             then have "?f x  = the_preced (t@s) x"

  1084               by (simp add:the_preced_def preced_def Set)

  1085             also have "... \<le> Max (the_preced (t@s) ` threads (t@s))"

  1086               using Set h h_t.finite_threads by auto 

  1087             also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) 

  1088             finally show ?thesis .

  1089           qed

  1090         qed

  1091       qed

  1092       also have "... = ?t" using h_e.th_kept the_preced_def by auto

  1093       finally show ?thesis .

  1094     qed 

  1095   qed

  1096 qed

  1097 

  1098 lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))"

  1099   by (insert th_kept max_kept, auto)

  1100 

  1101 text {*

  1102   The reason behind the following lemma is that:

  1103   Since @{term "cp"} is defined as the maximum precedence 

  1104   of those threads contained in the sub-tree of node @{term "Th th"} 

  1105   in @{term "RAG (t@s)"}, and all these threads are living threads, and 

  1106   @{term "th"} is also among them, the maximum precedence of 

  1107   them all must be the one for @{text "th"}.

  1108 *}

  1109 lemma th_cp_max_preced: 

  1110   "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") 

  1111 proof -

  1112   let ?f = "the_preced (t@s)"

  1113   have "?L = ?f th"

  1114   proof(unfold cp_alt_def, rule image_Max_eqI)

  1115     show "finite {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

  1116     proof -

  1117       have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = 

  1118             the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and>

  1119                             (\<exists> th'. n = Th th')}"

  1120       by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps)

  1121       moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) 

  1122       ultimately show ?thesis by simp

  1123     qed

  1124   next

  1125     show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

  1126       by (auto simp:subtree_def)

  1127   next

  1128     show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}.

  1129                the_preced (t @ s) x \<le> the_preced (t @ s) th"

  1130     proof

  1131       fix th'

  1132       assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

  1133       hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto

  1134       moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}"