1 section {*

     1 theory CpsG

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

     2 imports PIPDefs 

     3   after every system call (or system operation)

     3 begin

     4 

     5 (* I am going to use this file as a start point to retrofiting 

     6    PIPBasics.thy, which is originally called CpsG.ghy *)

     7 

     8 locale valid_trace = 

     9   fixes s

    10   assumes vt : "vt s"

    11 

    12 locale valid_trace_e = valid_trace +

    13   fixes e

    14   assumes vt_e: "vt (e#s)"

    15 begin

    16 

    17 lemma pip_e: "PIP s e"

    18   using vt_e by (cases, simp)  

    19 

    20 end

    21 

    22 lemma runing_ready: 

    23   shows "runing s \<subseteq> readys s"

    24   unfolding runing_def readys_def

    25   by auto 

    26 

    27 lemma readys_threads:

    28   shows "readys s \<subseteq> threads s"

    29   unfolding readys_def

    30   by auto

    31 

    32 lemma wq_v_neq [simp]:

    33    "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"

    34   by (auto simp:wq_def Let_def cp_def split:list.splits)

    35 

    36 lemma runing_head:

    37   assumes "th \<in> runing s"

    38   and "th \<in> set (wq_fun (schs s) cs)"

    39   shows "th = hd (wq_fun (schs s) cs)"

    40   using assms

    41   by (simp add:runing_def readys_def s_waiting_def wq_def)

    42 

    43 context valid_trace

    44 begin

    45 

    46 lemma actor_inv: 

    47   assumes "PIP s e"

    48   and "\<not> isCreate e"

    49   shows "actor e \<in> runing s"

    50   using assms

    51   by (induct, auto)

    52 

    53 

    54 lemma isP_E:

    55   assumes "isP e"

    56   obtains cs where "e = P (actor e) cs"

    57   using assms by (cases e, auto)

    58 

    59 lemma isV_E:

    60   assumes "isV e"

    61   obtains cs where "e = V (actor e) cs"

    62   using assms by (cases e, auto) 

    63 

    64 

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

    66   assumes "PP []"

    67      and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow>

    68                    PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"

    69      shows "PP s"

    70 proof(rule vt.induct[OF vt])

    71   from assms(1) show "PP []" .

    72 next

    73   fix s e

    74   assume h: "vt s" "PP s" "PIP s e"

    75   show "PP (e # s)"

    76   proof(cases rule:assms(2))

    77     from h(1) show v1: "valid_trace s" by (unfold_locales, simp)

    78   next

    79     from h(1,3) have "vt (e#s)" by auto

    80     thus "valid_trace (e # s)" by (unfold_locales, simp)

    81   qed (insert h, auto)

    82 qed

    83 

    84 lemma wq_distinct: "distinct (wq s cs)"

    85 proof(induct rule:ind)

    86   case (Cons s e)

    87   from Cons(4,3)

    88   show ?case 

    89   proof(induct)

    90     case (thread_P th s cs1)

    91     show ?case 

    92     proof(cases "cs = cs1")

    93       case True

    94       thus ?thesis (is "distinct ?L")

    95       proof - 

    96         have "?L = wq_fun (schs s) cs1 @ [th]" using True

    97           by (simp add:wq_def wf_def Let_def split:list.splits)

    98         moreover have "distinct ..."

    99         proof -

   100           have "th \<notin> set (wq_fun (schs s) cs1)"

   101           proof

   102             assume otherwise: "th \<in> set (wq_fun (schs s) cs1)"

   103             from runing_head[OF thread_P(1) this]

   104             have "th = hd (wq_fun (schs s) cs1)" .

   105             hence "(Cs cs1, Th th) \<in> (RAG s)" using otherwise

   106               by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)

   107             with thread_P(2) show False by auto

   108           qed

   109           moreover have "distinct (wq_fun (schs s) cs1)"

   110               using True thread_P wq_def by auto 

   111           ultimately show ?thesis by auto

   112         qed

   113         ultimately show ?thesis by simp

   114       qed

   115     next

   116       case False

   117       with thread_P(3)

   118       show ?thesis

   119         by (auto simp:wq_def wf_def Let_def split:list.splits)

   120     qed

   121   next

   122     case (thread_V th s cs1)

   123     thus ?case

   124     proof(cases "cs = cs1")

   125       case True

   126       show ?thesis (is "distinct ?L")

   127       proof(cases "(wq s cs)")

   128         case Nil

   129         thus ?thesis

   130           by (auto simp:wq_def wf_def Let_def split:list.splits)

   131       next

   132         case (Cons w_hd w_tl)

   133         moreover have "distinct (SOME q. distinct q \<and> set q = set w_tl)"

   134         proof(rule someI2)

   135           from thread_V(3)[unfolded Cons]

   136           show  "distinct w_tl \<and> set w_tl = set w_tl" by auto

   137         qed auto

   138         ultimately show ?thesis

   139           by (auto simp:wq_def wf_def Let_def True split:list.splits)

   140       qed 

   141     next

   142       case False

   143       with thread_V(3)

   144       show ?thesis

   145         by (auto simp:wq_def wf_def Let_def split:list.splits)

   146     qed

   147   qed (insert Cons, auto simp: wq_def Let_def split:list.splits)

   148 qed (unfold wq_def Let_def, simp)

   149 

   150 end

   151 

   152 context valid_trace_e

   153 begin

   154 

   155 text {*

   156   The following lemma shows that only the @{text "P"}

   157   operation can add new thread into waiting queues. 

   158   Such kind of lemmas are very obvious, but need to be checked formally.

   159   This is a kind of confirmation that our modelling is correct.

     5 theory CpsG

   161 

     6 imports PrioG Max RTree

   162 lemma wq_in_inv: 

   163   assumes s_ni: "thread \<notin> set (wq s cs)"

   164   and s_i: "thread \<in> set (wq (e#s) cs)"

   165   shows "e = P thread cs"

   166 proof(cases e)

   167   -- {* This is the only non-trivial case: *}

   168   case (V th cs1)

   169   have False

   170   proof(cases "cs1 = cs")

   171     case True

   172     show ?thesis

   173     proof(cases "(wq s cs1)")

   174       case (Cons w_hd w_tl)

   175       have "set (wq (e#s) cs) \<subseteq> set (wq s cs)"

   176       proof -

   177         have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)"

   178           using  Cons V by (auto simp:wq_def Let_def True split:if_splits)

   179         moreover have "set ... \<subseteq> set (wq s cs)"

   180         proof(rule someI2)

   181           show "distinct w_tl \<and> set w_tl = set w_tl"

   182             by (metis distinct.simps(2) local.Cons wq_distinct)

   183         qed (insert Cons True, auto)

   184         ultimately show ?thesis by simp

   185       qed

   186       with assms show ?thesis by auto

   187     qed (insert assms V True, auto simp:wq_def Let_def split:if_splits)

   188   qed (insert assms V, auto simp:wq_def Let_def split:if_splits)

   189   thus ?thesis by auto

   190 qed (insert assms, auto simp:wq_def Let_def split:if_splits)

   191 

   192 lemma wq_out_inv: 

   193   assumes s_in: "thread \<in> set (wq s cs)"

   194   and s_hd: "thread = hd (wq s cs)"

   195   and s_i: "thread \<noteq> hd (wq (e#s) cs)"

   196   shows "e = V thread cs"

   197 proof(cases e)

   198 -- {* There are only two non-trivial cases: *}

   199   case (V th cs1)

   200   show ?thesis

   201   proof(cases "cs1 = cs")

   202     case True

   203     have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] .

   204     thus ?thesis

   205     proof(cases)

   206       case (thread_V)

   207       moreover have "th = thread" using thread_V(2) s_hd

   208           by (unfold s_holding_def wq_def, simp)

   209       ultimately show ?thesis using V True by simp

   210     qed

   211   qed (insert assms V, auto simp:wq_def Let_def split:if_splits)

   212 next

   213   case (P th cs1)

   214   show ?thesis

   215   proof(cases "cs1 = cs")

   216     case True

   217     with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]"

   218       by (auto simp:wq_def Let_def split:if_splits)

   219     with s_i s_hd s_in have False

   220       by (metis empty_iff hd_append2 list.set(1) wq_def) 

   221     thus ?thesis by simp

   222   qed (insert assms P, auto simp:wq_def Let_def split:if_splits)

   223 qed (insert assms, auto simp:wq_def Let_def split:if_splits)

   224 

   225 end

   226 

   227 text {*

   228   The following lemmas is also obvious and shallow. It says

   229   that only running thread can request for a critical resource 

   230   and that the requested resource must be one which is

   231   not current held by the thread.

   232 *}

   233 

   234 lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow> 

   235   thread \<in> runing s \<and> (Cs cs, Th thread)  \<notin> (RAG s)^+"

   236 apply (ind_cases "vt ((P thread cs)#s)")

   237 apply (ind_cases "step s (P thread cs)")

   238 by auto

   239 

   240 lemma abs1:

   241   assumes ein: "e \<in> set es"

   242   and neq: "hd es \<noteq> hd (es @ [x])"

   243   shows "False"

   244 proof -

   245   from ein have "es \<noteq> []" by auto

   246   then obtain e ess where "es = e # ess" by (cases es, auto)

   247   with neq show ?thesis by auto

   248 qed

   249 

   250 lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"

   251   by (cases es, auto)

   252 

   253 inductive_cases evt_cons: "vt (a#s)"

   254 

   255 context valid_trace_e

     9 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only

   258 lemma abs2:

    10        difference is the order of arguemts. *}

   259   assumes inq: "thread \<in> set (wq s cs)"

    11 definition "the_preced s th = preced th s"

   260   and nh: "thread = hd (wq s cs)"

   261   and qt: "thread \<noteq> hd (wq (e#s) cs)"

   262   and inq': "thread \<in> set (wq (e#s) cs)"

   263   shows "False"

   264 proof -

   265   from vt_e assms show "False"

   266     apply (cases e)

   267     apply ((simp split:if_splits add:Let_def wq_def)[1])+

   268     apply (insert abs1, fast)[1]

   269     apply (auto simp:wq_def simp:Let_def split:if_splits list.splits)

   270   proof -

   271     fix th qs

   272     assume vt: "vt (V th cs # s)"

   273       and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"

   274       and eq_wq: "wq_fun (schs s) cs = thread # qs"

   275     show "False"

   276     proof -

   277       from wq_distinct[of cs]

   278         and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp

   279       moreover have "thread \<in> set qs"

   280       proof -

   281         have "set (SOME q. distinct q \<and> set q = set qs) = set qs"

   282         proof(rule someI2)

   283           from wq_distinct [of cs]

   284           and eq_wq [folded wq_def]

   285           show "distinct qs \<and> set qs = set qs" by auto

   286         next

   287           fix x assume "distinct x \<and> set x = set qs"

   288           thus "set x = set qs" by auto

   289         qed

   290         with th_in show ?thesis by auto

   291       qed

   292       ultimately show ?thesis by auto

   293     qed

   294   qed

   295 qed

   296 

   297 end

   298 

   299 

   300 context valid_trace

   301 begin

   302 lemma  vt_moment: "\<And> t. vt (moment t s)"

   303 proof(induct rule:ind)

   304   case Nil

   305   thus ?case by (simp add:vt_nil)

   306 next

   307   case (Cons s e t)

   308   show ?case

   309   proof(cases "t \<ge> length (e#s)")

   310     case True

   311     from True have "moment t (e#s) = e#s" by simp

   312     thus ?thesis using Cons

   313       by (simp add:valid_trace_def)

   314   next

   315     case False

   316     from Cons have "vt (moment t s)" by simp

   317     moreover have "moment t (e#s) = moment t s"

   318     proof -

   319       from False have "t \<le> length s" by simp

   320       from moment_app [OF this, of "[e]"] 

   321       show ?thesis by simp

   322     qed

   323     ultimately show ?thesis by simp

   324   qed

   325 qed

   326 end

   327 

   328 

   329 locale valid_moment = valid_trace + 

   330   fixes i :: nat

   331 

   332 sublocale valid_moment < vat_moment: valid_trace "(moment i s)"

   333   by (unfold_locales, insert vt_moment, auto)

   334 

   335 context valid_trace

   336 begin

   337 

   338 

   339 text {* (* ddd *)

   340   The nature of the work is like this: since it starts from a very simple and basic 

   341   model, even intuitively very `basic` and `obvious` properties need to derived from scratch.

   342   For instance, the fact 

   343   that one thread can not be blocked by two critical resources at the same time

   344   is obvious, because only running threads can make new requests, if one is waiting for 

   345   a critical resource and get blocked, it can not make another resource request and get 

   346   blocked the second time (because it is not running). 

   347 

   348   To derive this fact, one needs to prove by contraction and 

   349   reason about time (or @{text "moement"}). The reasoning is based on a generic theorem

   350   named @{text "p_split"}, which is about status changing along the time axis. It says if 

   351   a condition @{text "Q"} is @{text "True"} at a state @{text "s"},

   352   but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"} 

   353   in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history 

   354   of events leading to it), such that @{text "Q"} switched 

   355   from being @{text "False"} to @{text "True"} and kept being @{text "True"}

   356   till the last moment of @{text "s"}.

   357 

   358   Suppose a thread @{text "th"} is blocked

   359   on @{text "cs1"} and @{text "cs2"} in some state @{text "s"}, 

   360   since no thread is blocked at the very beginning, by applying 

   361   @{text "p_split"} to these two blocking facts, there exist 

   362   two moments @{text "t1"} and @{text "t2"}  in @{text "s"}, such that 

   363   @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} 

   364   and kept on blocked on them respectively ever since.

   365  

   366   Without lost of generality, we assume @{text "t1"} is earlier than @{text "t2"}.

   367   However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still

   368   in blocked state at moment @{text "t2"} and could not

   369   make any request and get blocked the second time: Contradiction.

   370 *}

   371 

   372 lemma waiting_unique_pre: (* ccc *)

   373   assumes h11: "thread \<in> set (wq s cs1)"

   374   and h12: "thread \<noteq> hd (wq s cs1)"

   375   assumes h21: "thread \<in> set (wq s cs2)"

   376   and h22: "thread \<noteq> hd (wq s cs2)"

   377   and neq12: "cs1 \<noteq> cs2"

   378   shows "False"

   379 proof -

   380   let "?Q" = "\<lambda> cs s. thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs)"

   381   from h11 and h12 have q1: "?Q cs1 s" by simp

   382   from h21 and h22 have q2: "?Q cs2 s" by simp

   383   have nq1: "\<not> ?Q cs1 []" by (simp add:wq_def)

   384   have nq2: "\<not> ?Q cs2 []" by (simp add:wq_def)

   385   from p_split [of "?Q cs1", OF q1 nq1]

   386   obtain t1 where lt1: "t1 < length s"

   387     and np1: "\<not> ?Q cs1 (moment t1 s)"

   388     and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" by auto

   389   from p_split [of "?Q cs2", OF q2 nq2]

   390   obtain t2 where lt2: "t2 < length s"

   391     and np2: "\<not> ?Q cs2 (moment t2 s)"

   392     and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" by auto

   393   { fix s cs

   394     assume q: "?Q cs s"

   395     have "thread \<notin> runing s"

   396     proof

   397       assume "thread \<in> runing s"

   398       hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and> 

   399                  thread \<noteq> hd (wq_fun (schs s) cs))"

   400         by (unfold runing_def s_waiting_def readys_def, auto)

   401       from this[rule_format, of cs] q 

   402       show False by (simp add: wq_def) 

   403     qed

   404   } note q_not_runing = this

   405   { fix i1 i2

   406     let ?i3 = "Suc i2"

   407     assume lt12: "i1 < i2"

   408     and "i1 < length s" "i2 < length s"

   409     hence le_i3: "?i3 \<le> length s" by auto

   410     from moment_plus [OF this]

   411     obtain e where eq_m: "moment ?i3 s = e#moment i2 s" by auto

   412     have "i2 < ?i3" by simp

   413     from nn2 [rule_format, OF this] and eq_m

   414       have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and

   415            h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto

   416       have "vt (e#moment t2 s)"

   417       proof -

   418         from vt_moment 

   419         have "vt (moment ?t3 s)" .

   420         with eq_m show ?thesis by simp

   421       qed

   422       then interpret vt_e: valid_trace_e "moment t2 s" "e"

   423         by (unfold_locales, auto, cases, simp)

   424       have ?thesis

   425       proof(cases "thread \<in> set (wq (moment t2 s) cs2)")

   426         case True

   427         from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"

   428           by auto 

   429         from vt_e.abs2 [OF True eq_th h2 h1]

   430         show ?thesis by auto

   431       next

   432         case False

   433         from vt_e.block_pre[OF False h1]

   434         have "e = P thread cs2" .

   435         with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp

   436         from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp

   437         with runing_ready have "thread \<in> readys (moment t2 s)" by auto

   438         with nn1 [rule_format, OF lt12]

   439         show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)

   440       qed

   441   }

   442   show ?thesis

   443   proof -

   444     { 

   445       assume lt12: "t1 < t2"

   446       let ?t3 = "Suc t2"

   447       from lt2 have le_t3: "?t3 \<le> length s" by auto

   448       from moment_plus [OF this] 

   449       obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto

   450       have "t2 < ?t3" by simp

   451       from nn2 [rule_format, OF this] and eq_m

   452       have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and

   453            h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto

   454       have "vt (e#moment t2 s)"

   455       proof -

   456         from vt_moment 

   457         have "vt (moment ?t3 s)" .

   458         with eq_m show ?thesis by simp

   459       qed

   460       then interpret vt_e: valid_trace_e "moment t2 s" "e"

   461         by (unfold_locales, auto, cases, simp)

   462       have ?thesis

   463       proof(cases "thread \<in> set (wq (moment t2 s) cs2)")

   464         case True

   465         from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"

   466           by auto 

   467         from vt_e.abs2 [OF True eq_th h2 h1]

   468         show ?thesis by auto

   469       next

   470         case False

   471         from vt_e.block_pre[OF False h1]

   472         have "e = P thread cs2" .

   473         with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp

   474         from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp

   475         with runing_ready have "thread \<in> readys (moment t2 s)" by auto

   476         with nn1 [rule_format, OF lt12]

   477         show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)

   478       qed

   479     } moreover {

   480       assume lt12: "t2 < t1"

   481       let ?t3 = "Suc t1"

   482       from lt1 have le_t3: "?t3 \<le> length s" by auto

   483       from moment_plus [OF this] 

   484       obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto

   485       have lt_t3: "t1 < ?t3" by simp

   486       from nn1 [rule_format, OF this] and eq_m

   487       have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and

   488         h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto

   489       have "vt  (e#moment t1 s)"

   490       proof -

   491         from vt_moment

   492         have "vt (moment ?t3 s)" .

   493         with eq_m show ?thesis by simp

   494       qed

   495       then interpret vt_e: valid_trace_e "moment t1 s" e

   496         by (unfold_locales, auto, cases, auto)

   497       have ?thesis

   498       proof(cases "thread \<in> set (wq (moment t1 s) cs1)")

   499         case True

   500         from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"

   501           by auto

   502         from vt_e.abs2 True eq_th h2 h1

   503         show ?thesis by auto

   504       next

   505         case False

   506         from vt_e.block_pre [OF False h1]

   507         have "e = P thread cs1" .

   508         with vt_e.vt_e have "vt ((P thread cs1)# moment t1 s)" by simp

   509         from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp

   510         with runing_ready have "thread \<in> readys (moment t1 s)" by auto

   511         with nn2 [rule_format, OF lt12]

   512         show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)

   513       qed

   514     } moreover {

   515       assume eqt12: "t1 = t2"

   516       let ?t3 = "Suc t1"

   517       from lt1 have le_t3: "?t3 \<le> length s" by auto

   518       from moment_plus [OF this] 

   519       obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto

   520       have lt_t3: "t1 < ?t3" by simp

   521       from nn1 [rule_format, OF this] and eq_m

   522       have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and

   523         h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto

   524       have vt_e: "vt (e#moment t1 s)"

   525       proof -

   526         from vt_moment

   527         have "vt (moment ?t3 s)" .

   528         with eq_m show ?thesis by simp

   529       qed

   530       then interpret vt_e: valid_trace_e "moment t1 s" e

   531         by (unfold_locales, auto, cases, auto)

   532       have ?thesis

   533       proof(cases "thread \<in> set (wq (moment t1 s) cs1)")

   534         case True

   535         from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"

   536           by auto

   537         from vt_e.abs2 [OF True eq_th h2 h1]

   538         show ?thesis by auto

   539       next

   540         case False

   541         from vt_e.block_pre [OF False h1]

   542         have eq_e1: "e = P thread cs1" .

   543         have lt_t3: "t1 < ?t3" by simp

   544         with eqt12 have "t2 < ?t3" by simp

   545         from nn2 [rule_format, OF this] and eq_m and eqt12

   546         have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and

   547           h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto

   548         show ?thesis

   549         proof(cases "thread \<in> set (wq (moment t2 s) cs2)")

   550           case True

   551           from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"

   552             by auto

   553           from vt_e and eqt12 have "vt (e#moment t2 s)" by simp 

   554           then interpret vt_e2: valid_trace_e "moment t2 s" e

   555             by (unfold_locales, auto, cases, auto)

   556           from vt_e2.abs2 [OF True eq_th h2 h1]

   557           show ?thesis .

   558         next

   559           case False

   560           have "vt (e#moment t2 s)"

   561           proof -

   562             from vt_moment eqt12

   563             have "vt (moment (Suc t2) s)" by auto

   564             with eq_m eqt12 show ?thesis by simp

   565           qed

   566           then interpret vt_e2: valid_trace_e "moment t2 s" e

   567             by (unfold_locales, auto, cases, auto)

   568           from vt_e2.block_pre [OF False h1]

   569           have "e = P thread cs2" .

   570           with eq_e1 neq12 show ?thesis by auto

   571         qed

   572       qed

   573     } ultimately show ?thesis by arith

   574   qed

   575 qed

   576 

   577 text {*

   578   This lemma is a simple corrolary of @{text "waiting_unique_pre"}.

   579 *}

   580 

   581 lemma waiting_unique:

   582   assumes "waiting s th cs1"

   583   and "waiting s th cs2"

   584   shows "cs1 = cs2"

   585 using waiting_unique_pre assms

   586 unfolding wq_def s_waiting_def

   587 by auto

   588 

   589 end

   590 

   591 (* not used *)

   592 text {*

   593   Every thread can only be blocked on one critical resource, 

   594   symmetrically, every critical resource can only be held by one thread. 

   595   This fact is much more easier according to our definition. 

   596 *}

   597 lemma held_unique:

   598   assumes "holding (s::event list) th1 cs"

   599   and "holding s th2 cs"

   600   shows "th1 = th2"

   601  by (insert assms, unfold s_holding_def, auto)

   602 

   603 

   604 lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"

   605   apply (induct s, auto)

   606   by (case_tac a, auto split:if_splits)

   607 

   608 lemma last_set_unique: 

   609   "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>

   610           \<Longrightarrow> th1 = th2"

   611   apply (induct s, auto)

   612   by (case_tac a, auto split:if_splits dest:last_set_lt)

   613 

   614 lemma preced_unique : 

   615   assumes pcd_eq: "preced th1 s = preced th2 s"

   616   and th_in1: "th1 \<in> threads s"

   617   and th_in2: " th2 \<in> threads s"

   618   shows "th1 = th2"

   619 proof -

   620   from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)

   621   from last_set_unique [OF this th_in1 th_in2]

   622   show ?thesis .

   623 qed

   624 

   625 lemma preced_linorder: 

   626   assumes neq_12: "th1 \<noteq> th2"

   627   and th_in1: "th1 \<in> threads s"

   628   and th_in2: " th2 \<in> threads s"

   629   shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"

   630 proof -

   631   from preced_unique [OF _ th_in1 th_in2] and neq_12 

   632   have "preced th1 s \<noteq> preced th2 s" by auto

   633   thus ?thesis by auto

   634 qed

   635 

   636 (* An aux lemma used later *)

   637 lemma unique_minus:

   638   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

   639   and xy: "(x, y) \<in> r"

   640   and xz: "(x, z) \<in> r^+"

   641   and neq: "y \<noteq> z"

   642   shows "(y, z) \<in> r^+"

   643 proof -

   644  from xz and neq show ?thesis

   645  proof(induct)

   646    case (base ya)

   647    have "(x, ya) \<in> r" by fact

   648    from unique [OF xy this] have "y = ya" .

   649    with base show ?case by auto

   650  next

   651    case (step ya z)

   652    show ?case

   653    proof(cases "y = ya")

   654      case True

   655      from step True show ?thesis by simp

   656    next

   657      case False

   658      from step False

   659      show ?thesis by auto

   660    qed

   661  qed

   662 qed

   663 

   664 lemma unique_base:

   665   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

   666   and xy: "(x, y) \<in> r"

   667   and xz: "(x, z) \<in> r^+"

   668   and neq_yz: "y \<noteq> z"

   669   shows "(y, z) \<in> r^+"

   670 proof -

   671   from xz neq_yz show ?thesis

   672   proof(induct)

   673     case (base ya)

   674     from xy unique base show ?case by auto

   675   next

   676     case (step ya z)

   677     show ?case

   678     proof(cases "y = ya")

   679       case True

   680       from True step show ?thesis by auto

   681     next

   682       case False

   683       from False step 

   684       have "(y, ya) \<in> r\<^sup>+" by auto

   685       with step show ?thesis by auto

   686     qed

   687   qed

   688 qed

   689 

   690 lemma unique_chain:

   691   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

   692   and xy: "(x, y) \<in> r^+"

   693   and xz: "(x, z) \<in> r^+"

   694   and neq_yz: "y \<noteq> z"

   695   shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+"

   696 proof -

   697   from xy xz neq_yz show ?thesis

   698   proof(induct)

   699     case (base y)

   700     have h1: "(x, y) \<in> r" and h2: "(x, z) \<in> r\<^sup>+" and h3: "y \<noteq> z" using base by auto

   701     from unique_base [OF _ h1 h2 h3] and unique show ?case by auto

   702   next

   703     case (step y za)

   704     show ?case

   705     proof(cases "y = z")

   706       case True

   707       from True step show ?thesis by auto

   708     next

   709       case False

   710       from False step have "(y, z) \<in> r\<^sup>+ \<or> (z, y) \<in> r\<^sup>+" by auto

   711       thus ?thesis

   712       proof

   713         assume "(z, y) \<in> r\<^sup>+"

   714         with step have "(z, za) \<in> r\<^sup>+" by auto

   715         thus ?thesis by auto

   716       next

   717         assume h: "(y, z) \<in> r\<^sup>+"

   718         from step have yza: "(y, za) \<in> r" by simp

   719         from step have "za \<noteq> z" by simp

   720         from unique_minus [OF _ yza h this] and unique

   721         have "(za, z) \<in> r\<^sup>+" by auto

   722         thus ?thesis by auto

   723       qed

   724     qed

   725   qed

   726 qed

   727 

   728 text {*

   729   The following three lemmas show that @{text "RAG"} does not change

   730   by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"}

   731   events, respectively.

   732 *}

   733 

   734 lemma RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s"

   735 apply (unfold s_RAG_def s_waiting_def wq_def)

   736 by (simp add:Let_def)

   737 

   738 lemma RAG_create_unchanged: "(RAG (Create th prio # s)) = RAG s"

   739 apply (unfold s_RAG_def s_waiting_def wq_def)

   740 by (simp add:Let_def)

   741 

   742 lemma RAG_exit_unchanged: "(RAG (Exit th # s)) = RAG s"

   743 apply (unfold s_RAG_def s_waiting_def wq_def)

   744 by (simp add:Let_def)

   745 

   746 

   747 text {* 

   748   The following lemmas are used in the proof of 

   749   lemma @{text "step_RAG_v"}, which characterizes how the @{text "RAG"} is changed

   750   by @{text "V"}-events. 

   751   However, since our model is very concise, such  seemingly obvious lemmas need to be derived from scratch,

   752   starting from the model definitions.

   753 *}

   754 lemma step_v_hold_inv[elim_format]:

   755   "\<And>c t. \<lbrakk>vt (V th cs # s); 

   756           \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> 

   757             next_th s th cs t \<and> c = cs"

   758 proof -

   759   fix c t

   760   assume vt: "vt (V th cs # s)"

   761     and nhd: "\<not> holding (wq s) t c"

   762     and hd: "holding (wq (V th cs # s)) t c"

   763   show "next_th s th cs t \<and> c = cs"

   764   proof(cases "c = cs")

   765     case False

   766     with nhd hd show ?thesis

   767       by (unfold cs_holding_def wq_def, auto simp:Let_def)

   768   next

   769     case True

   770     with step_back_step [OF vt] 

   771     have "step s (V th c)" by simp

   772     hence "next_th s th cs t"

   773     proof(cases)

   774       assume "holding s th c"

   775       with nhd hd show ?thesis

   776         apply (unfold s_holding_def cs_holding_def wq_def next_th_def,

   777                auto simp:Let_def split:list.splits if_splits)

   778         proof -

   779           assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])"

   780           moreover have "\<dots> = set []"

   781           proof(rule someI2)

   782             show "distinct [] \<and> [] = []" by auto

   783           next

   784             fix x assume "distinct x \<and> x = []"

   785             thus "set x = set []" by auto

   786           qed

   787           ultimately show False by auto

   788         next

   789           assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])"

   790           moreover have "\<dots> = set []"

   791           proof(rule someI2)

   792             show "distinct [] \<and> [] = []" by auto

   793           next

   794             fix x assume "distinct x \<and> x = []"

   795             thus "set x = set []" by auto

   796           qed

   797           ultimately show False by auto

   798         qed

   799     qed

   800     with True show ?thesis by auto

   801   qed

   802 qed

   803 

   804 text {* 

   805   The following @{text "step_v_wait_inv"} is also an obvious lemma, which, however, needs to be

   806   derived from scratch, which confirms the correctness of the definition of @{text "next_th"}.

   807 *}

   808 lemma step_v_wait_inv[elim_format]:

   809     "\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c

   810            \<rbrakk>

   811           \<Longrightarrow> (next_th s th cs t \<and> cs = c)"

   812 proof -

   813   fix t c 

   814   assume vt: "vt (V th cs # s)"

   815     and nw: "\<not> waiting (wq (V th cs # s)) t c"

   816     and wt: "waiting (wq s) t c"

   817   from vt interpret vt_v: valid_trace_e s "V th cs" 

   818     by  (cases, unfold_locales, simp)

   819   show "next_th s th cs t \<and> cs = c"

   820   proof(cases "cs = c")

   821     case False

   822     with nw wt show ?thesis

   823       by (auto simp:cs_waiting_def wq_def Let_def)

   824   next

   825     case True

   826     from nw[folded True] wt[folded True]

   827     have "next_th s th cs t"

   828       apply (unfold next_th_def, auto simp:cs_waiting_def wq_def Let_def split:list.splits)

   829     proof -

   830       fix a list

   831       assume t_in: "t \<in> set list"

   832         and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"

   833         and eq_wq: "wq_fun (schs s) cs = a # list"

   834       have " set (SOME q. distinct q \<and> set q = set list) = set list"

   835       proof(rule someI2)

   836         from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]

   837         show "distinct list \<and> set list = set list" by auto

   838       next

   839         show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"

   840           by auto

   841       qed

   842       with t_ni and t_in show "a = th" by auto

   843     next

   844       fix a list

   845       assume t_in: "t \<in> set list"

   846         and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"

   847         and eq_wq: "wq_fun (schs s) cs = a # list"

   848       have " set (SOME q. distinct q \<and> set q = set list) = set list"

   849       proof(rule someI2)

   850         from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]

   851         show "distinct list \<and> set list = set list" by auto

   852       next

   853         show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"

   854           by auto

   855       qed

   856       with t_ni and t_in show "t = hd (SOME q. distinct q \<and> set q = set list)" by auto

   857     next

   858       fix a list

   859       assume eq_wq: "wq_fun (schs s) cs = a # list"

   860       from step_back_step[OF vt]

   861       show "a = th"

   862       proof(cases)

   863         assume "holding s th cs"

   864         with eq_wq show ?thesis

   865           by (unfold s_holding_def wq_def, auto)

   866       qed

   867     qed

   868     with True show ?thesis by simp

   869   qed

   870 qed

   871 

   872 lemma step_v_not_wait[consumes 3]:

   873   "\<lbrakk>vt (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"

   874   by (unfold next_th_def cs_waiting_def wq_def, auto simp:Let_def)

   875 

   876 lemma step_v_release:

   877   "\<lbrakk>vt (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"

   878 proof -

   879   assume vt: "vt (V th cs # s)"

   880     and hd: "holding (wq (V th cs # s)) th cs"

   881   from vt interpret vt_v: valid_trace_e s "V th cs"

   882     by (cases, unfold_locales, simp+)

   883   from step_back_step [OF vt] and hd

   884   show "False"

   885   proof(cases)

   886     assume "holding (wq (V th cs # s)) th cs" and "holding s th cs"

   887     thus ?thesis

   888       apply (unfold s_holding_def wq_def cs_holding_def)

   889       apply (auto simp:Let_def split:list.splits)

   890     proof -

   891       fix list

   892       assume eq_wq[folded wq_def]: 

   893         "wq_fun (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list"

   894       and hd_in: "hd (SOME q. distinct q \<and> set q = set list)

   895             \<in> set (SOME q. distinct q \<and> set q = set list)"

   896       have "set (SOME q. distinct q \<and> set q = set list) = set list"

   897       proof(rule someI2)

   898         from vt_v.wq_distinct[of cs] and eq_wq

   899         show "distinct list \<and> set list = set list" by auto

   900       next

   901         show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"

   902           by auto

   903       qed

   904       moreover have "distinct  (hd (SOME q. distinct q \<and> set q = set list) # list)"

   905       proof -

   906         from vt_v.wq_distinct[of cs] and eq_wq

   907         show ?thesis by auto

   908       qed

   909       moreover note eq_wq and hd_in

   910       ultimately show "False" by auto

   911     qed

   912   qed

   913 qed

   914 

   915 lemma step_v_get_hold:

   916   "\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"

   917   apply (unfold cs_holding_def next_th_def wq_def,

   918          auto simp:Let_def)

   919 proof -

   920   fix rest

   921   assume vt: "vt (V th cs # s)"

   922     and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest"

   923     and nrest: "rest \<noteq> []"

   924     and ni: "hd (SOME q. distinct q \<and> set q = set rest)

   925             \<notin> set (SOME q. distinct q \<and> set q = set rest)"

   926   from vt interpret vt_v: valid_trace_e s "V th cs"

   927     by (cases, unfold_locales, simp+)

   928   have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"

   929   proof(rule someI2)

   930     from vt_v.wq_distinct[of cs] and eq_wq

   931     show "distinct rest \<and> set rest = set rest" by auto

   932   next

   933     fix x assume "distinct x \<and> set x = set rest"

   934     hence "set x = set rest" by auto

   935     with nrest

   936     show "x \<noteq> []" by (case_tac x, auto)

   937   qed

   938   with ni show "False" by auto

   939 qed

   940 

   941 lemma step_v_release_inv[elim_format]:

   942 "\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> 

   943   c = cs \<and> t = th"

   944   apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits)

   945   proof -

   946     fix a list

   947     assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"

   948     from step_back_step [OF vt] show "a = th"

   949     proof(cases)

   950       assume "holding s th cs" with eq_wq

   951       show ?thesis

   952         by (unfold s_holding_def wq_def, auto)

   953     qed

   954   next

   955     fix a list

   956     assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"

   957     from step_back_step [OF vt] show "a = th"

   958     proof(cases)

   959       assume "holding s th cs" with eq_wq

   960       show ?thesis

   961         by (unfold s_holding_def wq_def, auto)

   962     qed

   963   qed

   964 

   965 lemma step_v_waiting_mono:

   966   "\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"

   967 proof -

   968   fix t c

   969   let ?s' = "(V th cs # s)"

   970   assume vt: "vt ?s'" 

   971     and wt: "waiting (wq ?s') t c"

   972   from vt interpret vt_v: valid_trace_e s "V th cs"

   973     by (cases, unfold_locales, simp+)

   974   show "waiting (wq s) t c"

   975   proof(cases "c = cs")

   976     case False

   977     assume neq_cs: "c \<noteq> cs"

   978     hence "waiting (wq ?s') t c = waiting (wq s) t c"

   979       by (unfold cs_waiting_def wq_def, auto simp:Let_def)

   980     with wt show ?thesis by simp

   981   next

   982     case True

   983     with wt show ?thesis

   984       apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits)

   985     proof -

   986       fix a list

   987       assume not_in: "t \<notin> set list"

   988         and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)"

   989         and eq_wq: "wq_fun (schs s) cs = a # list"

   990       have "set (SOME q. distinct q \<and> set q = set list) = set list"

   991       proof(rule someI2)

   992         from vt_v.wq_distinct [of cs]

   993         and eq_wq[folded wq_def]

   994         show "distinct list \<and> set list = set list" by auto

   995       next

   996         fix x assume "distinct x \<and> set x = set list"

   997         thus "set x = set list" by auto

   998       qed

   999       with not_in is_in show "t = a" by auto

  1000     next

  1001       fix list

  1002       assume is_waiting: "waiting (wq (V th cs # s)) t cs"

  1003       and eq_wq: "wq_fun (schs s) cs = t # list"

  1004       hence "t \<in> set list"

  1005         apply (unfold wq_def, auto simp:Let_def cs_waiting_def)

  1006       proof -

  1007         assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"

  1008         moreover have "\<dots> = set list" 

  1009         proof(rule someI2)

  1010           from vt_v.wq_distinct [of cs]

  1011             and eq_wq[folded wq_def]

  1012           show "distinct list \<and> set list = set list" by auto

  1013         next

  1014           fix x assume "distinct x \<and> set x = set list" 

  1015           thus "set x = set list" by auto

  1016         qed

  1017         ultimately show "t \<in> set list" by simp

  1018       qed

  1019       with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def]

  1020       show False by auto

  1021     qed

  1022   qed

  1023 qed

  1024 

  1025 text {* (* ddd *) 

  1026   The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed

  1027   with the happening of @{text "V"}-events:

  1028 *}

  1029 lemma step_RAG_v:

  1030 assumes vt:

  1031   "vt (V th cs#s)"

  1032 shows "

  1033   RAG (V th cs # s) =

  1034   RAG s - {(Cs cs, Th th)} -

  1035   {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>

  1036   {(Cs cs, Th th') |th'.  next_th s th cs th'}"

  1037   apply (insert vt, unfold s_RAG_def) 

  1038   apply (auto split:if_splits list.splits simp:Let_def)

  1039   apply (auto elim: step_v_waiting_mono step_v_hold_inv 

  1040               step_v_release step_v_wait_inv

  1041               step_v_get_hold step_v_release_inv)

  1042   apply (erule_tac step_v_not_wait, auto)

  1043   done

  1044 

  1045 text {* 

  1046   The following @{text "step_RAG_p"} lemma charaterizes how @{text "RAG"} is changed

  1047   with the happening of @{text "P"}-events:

  1048 *}

  1049 lemma step_RAG_p:

  1050   "vt (P th cs#s) \<Longrightarrow>

  1051   RAG (P th cs # s) =  (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}

  1052                                              else RAG s \<union> {(Th th, Cs cs)})"

  1053   apply(simp only: s_RAG_def wq_def)

  1054   apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def)

  1055   apply(case_tac "csa = cs", auto)

  1056   apply(fold wq_def)

  1057   apply(drule_tac step_back_step)

  1058   apply(ind_cases " step s (P (hd (wq s cs)) cs)")

  1059   apply(simp add:s_RAG_def wq_def cs_holding_def)

  1060   apply(auto)

  1061   done

  1062 

  1063 

  1064 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"

  1065   by (unfold s_RAG_def, auto)

  1066 

  1067 context valid_trace

  1068 begin

  1069 

  1070 text {*

  1071   The following lemma shows that @{text "RAG"} is acyclic.

  1072   The overall structure is by induction on the formation of @{text "vt s"}

  1073   and then case analysis on event @{text "e"}, where the non-trivial cases 

  1074   for those for @{text "V"} and @{text "P"} events.

  1075 *}

  1076 lemma acyclic_RAG:

  1077   shows "acyclic (RAG s)"

  1078 using vt

  1079 proof(induct)

  1080   case (vt_cons s e)

  1081   interpret vt_s: valid_trace s using vt_cons(1)

  1082     by (unfold_locales, simp)

  1083   assume ih: "acyclic (RAG s)"

  1084     and stp: "step s e"

  1085     and vt: "vt s"

  1086   show ?case

  1087   proof(cases e)

  1088     case (Create th prio)

  1089     with ih

  1090     show ?thesis by (simp add:RAG_create_unchanged)

  1091   next

  1092     case (Exit th)

  1093     with ih show ?thesis by (simp add:RAG_exit_unchanged)

  1094   next

  1095     case (V th cs)

  1096     from V vt stp have vtt: "vt (V th cs#s)" by auto

  1097     from step_RAG_v [OF this]

  1098     have eq_de: 

  1099       "RAG (e # s) = 

  1100       RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>

  1101       {(Cs cs, Th th') |th'. next_th s th cs th'}"

  1102       (is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V)

  1103     from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset)

  1104     from step_back_step [OF vtt]

  1105     have "step s (V th cs)" .

  1106     thus ?thesis

  1107     proof(cases)

  1108       assume "holding s th cs"

  1109       hence th_in: "th \<in> set (wq s cs)" and

  1110         eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto

  1111       then obtain rest where

  1112         eq_wq: "wq s cs = th#rest"

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

  1114       show ?thesis

  1115       proof(cases "rest = []")

  1116         case False

  1117         let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"

  1118         from eq_wq False have eq_D: "?D = {(Cs cs, Th ?th')}"

  1119           by (unfold next_th_def, auto)

  1120         let ?E = "(?A - ?B - ?C)"

  1121         have "(Th ?th', Cs cs) \<notin> ?E\<^sup>*"

  1122         proof

  1123           assume "(Th ?th', Cs cs) \<in> ?E\<^sup>*"

  1124           hence " (Th ?th', Cs cs) \<in> ?E\<^sup>+" by (simp add: rtrancl_eq_or_trancl)

  1125           from tranclD [OF this]

  1126           obtain x where th'_e: "(Th ?th', x) \<in> ?E" by blast

  1127           hence th_d: "(Th ?th', x) \<in> ?A" by simp

  1128           from RAG_target_th [OF this]

  1129           obtain cs' where eq_x: "x = Cs cs'" by auto

  1130           with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp

  1131           hence wt_th': "waiting s ?th' cs'"

  1132             unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp

  1133           hence "cs' = cs"

  1134           proof(rule vt_s.waiting_unique)