1 theory PIPBasics

     2 imports PIPDefs 

     3 begin

     4 

     5 locale valid_trace = 

     6   fixes s

     7   assumes vt : "vt s"

     8 

     9 locale valid_trace_e = valid_trace +

    10   fixes e

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

    12 begin

    13 

    14 lemma pip_e: "PIP s e"

    15   using vt_e by (cases, simp)  

    16 

    17 end

    18 

    19 lemma runing_ready: 

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

    21   unfolding runing_def readys_def

    22   by auto 

    23 

    24 lemma readys_threads:

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

    26   unfolding readys_def

    27   by auto

    28 

    29 lemma wq_v_neq:

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

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

    32 

    33 lemma runing_head:

    34   assumes "th \<in> runing s"

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

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

    37   using assms

    38   by (simp add:runing_def readys_def s_waiting_def wq_def)

    39 

    40 context valid_trace

    41 begin

    42 

    43 lemma actor_inv: 

    44   assumes "PIP s e"

    45   and "\<not> isCreate e"

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

    47   using assms

    48   by (induct, auto)

    49 

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

    51   assumes "PP []"

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

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

    54      shows "PP s"

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

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

    57 next

    58   fix s e

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

    60   show "PP (e # s)"

    61   proof(cases rule:assms(2))

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

    63   next

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

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

    66   qed (insert h, auto)

    67 qed

    68 

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

    70 proof(induct rule:ind)

    71   case (Cons s e)

    72   from Cons(4,3)

    73   show ?case 

    74   proof(induct)

    75     case (thread_P th s cs1)

    76     show ?case 

    77     proof(cases "cs = cs1")

    78       case True

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

    80       proof - 

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

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

    83         moreover have "distinct ..."

    84         proof -

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

    86           proof

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

    88             from runing_head[OF thread_P(1) this]

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

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

    91               by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)

    92             with thread_P(2) show False by auto

    93           qed

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

    95               using True thread_P wq_def by auto 

    96           ultimately show ?thesis by auto

    97         qed

    98         ultimately show ?thesis by simp

    99       qed

   100     next

   101       case False

   102       with thread_P(3)

   103       show ?thesis

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

   105     qed

   106   next

   107     case (thread_V th s cs1)

   108     thus ?case

   109     proof(cases "cs = cs1")

   110       case True

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

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

   113         case Nil

   114         thus ?thesis

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

   116       next

   117         case (Cons w_hd w_tl)

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

   119         proof(rule someI2)

   120           from thread_V(3)[unfolded Cons]

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

   122         qed auto

   123         ultimately show ?thesis

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

   125       qed 

   126     next

   127       case False

   128       with thread_V(3)

   129       show ?thesis

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

   131     qed

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

   133 qed (unfold wq_def Let_def, simp)

   134 

   135 end

   136 

   137 

   138 context valid_trace_e

   139 begin

   140 

   141 text {*

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

   143   operation can add new thread into waiting queues. 

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

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

   146 *}

   147 

   148 lemma block_pre: 

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

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

   151   shows "e = P thread cs"

   152 proof(cases e)

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

   154   case (V th cs1)

   155   have False

   156   proof(cases "cs1 = cs")

   157     case True

   158     show ?thesis

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

   160       case (Cons w_hd w_tl)

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

   162       proof -

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

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

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

   166         proof(rule someI2)

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

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

   169         qed (insert Cons True, auto)

   170         ultimately show ?thesis by simp

   171       qed

   172       with assms show ?thesis by auto

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

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

   175   thus ?thesis by auto

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

   177 

   178 end

   179 

   180 text {*

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

   182   that only running thread can request for a critical resource 

   183   and that the requested resource must be one which is

   184   not current held by the thread.

   185 *}

   186 

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

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

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

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

   191 by auto

   192 

   193 lemma abs1:

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

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

   196   shows "False"

   197 proof -

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

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

   200   with neq show ?thesis by auto

   201 qed

   202 

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

   204   by (cases es, auto)

   205 

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

   207 

   208 context valid_trace_e

   209 begin

   210 

   211 lemma abs2:

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

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

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

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

   216   shows "False"

   217 proof -

   218   from vt_e assms show "False"

   219     apply (cases e)

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

   221     apply (insert abs1, fast)[1]

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

   223   proof -

   224     fix th qs

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

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

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

   228     show "False"

   229     proof -

   230       from wq_distinct[of cs]

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

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

   233       proof -

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

   235         proof(rule someI2)

   236           from wq_distinct [of cs]

   237           and eq_wq [folded wq_def]

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

   239         next

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

   241           thus "set x = set qs" by auto

   242         qed

   243         with th_in show ?thesis by auto

   244       qed

   245       ultimately show ?thesis by auto

   246     qed

   247   qed

   248 qed

   249 

   250 end

   251 

   252 

   253 context valid_trace

   254 begin

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

   256 proof(induct rule:ind)

   257   case Nil

   258   thus ?case by (simp add:vt_nil)

   259 next

   260   case (Cons s e t)

   261   show ?case

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

   263     case True

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

   265     thus ?thesis using Cons

   266       by (simp add:valid_trace_def)

   267   next

   268     case False

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

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

   271     proof -

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

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

   274       show ?thesis by simp

   275     qed

   276     ultimately show ?thesis by simp

   277   qed

   278 qed

   279 end

   280 

   281 locale valid_moment = valid_trace + 

   282   fixes i :: nat

   283 

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

   285   by (unfold_locales, insert vt_moment, auto)

   286 

   287 context valid_trace

   288 begin

   289 

   290 

   291 text {* (* ddd *)

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

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

   294   For instance, the fact 

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

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

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

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

   299 

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

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

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

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

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

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

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

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

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

   309 

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

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

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

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

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

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

   316   and kept on blocked on them respectively ever since.

   317  

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

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

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

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

   322 *}

   323 

   324 lemma waiting_unique_pre: (* ccc *)

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

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

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

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

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

   330   shows "False"

   331 proof -

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

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

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

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

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

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

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

   339     and np1: "\<not>(thread \<in> set (wq (moment t1 s) cs1) \<and>

   340         thread \<noteq> hd (wq (moment t1 s) cs1))"

   341     and nn1: "(\<forall>i'>t1. thread \<in> set (wq (moment i' s) cs1) \<and>

   342              thread \<noteq> hd (wq (moment i' s) cs1))" by auto

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

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

   345     and np2: "\<not>(thread \<in> set (wq (moment t2 s) cs2) \<and>

   346         thread \<noteq> hd (wq (moment t2 s) cs2))"

   347     and nn2: "(\<forall>i'>t2. thread \<in> set (wq (moment i' s) cs2) \<and>

   348              thread \<noteq> hd (wq (moment i' s) cs2))" by auto

   349   show ?thesis

   350   proof -

   351     { 

   352       assume lt12: "t1 < t2"

   353       let ?t3 = "Suc t2"

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

   355       from moment_plus [OF this] 

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

   357       have "t2 < ?t3" by simp

   358       from nn2 [rule_format, OF this] and eq_m

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

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

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

   362       proof -

   363         from vt_moment 

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

   365         with eq_m show ?thesis by simp

   366       qed

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

   368         by (unfold_locales, auto, cases, simp)

   369       have ?thesis

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

   371         case True

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

   373           by auto 

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

   375         show ?thesis by auto

   376       next

   377         case False

   378         from vt_e.block_pre[OF False h1]

   379         have "e = P thread cs2" .

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

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

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

   383         with nn1 [rule_format, OF lt12]

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

   385       qed

   386     } moreover {

   387       assume lt12: "t2 < t1"

   388       let ?t3 = "Suc t1"

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

   390       from moment_plus [OF this] 

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

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

   393       from nn1 [rule_format, OF this] and eq_m

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

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

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

   397       proof -

   398         from vt_moment

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

   400         with eq_m show ?thesis by simp

   401       qed

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

   403         by (unfold_locales, auto, cases, auto)

   404       have ?thesis

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

   406         case True

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

   408           by auto

   409         from vt_e.abs2 True eq_th h2 h1

   410         show ?thesis by auto

   411       next

   412         case False

   413         from vt_e.block_pre [OF False h1]

   414         have "e = P thread cs1" .

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

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

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

   418         with nn2 [rule_format, OF lt12]

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

   420       qed

   421     } moreover {

   422       assume eqt12: "t1 = t2"

   423       let ?t3 = "Suc t1"

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

   425       from moment_plus [OF this] 

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

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

   428       from nn1 [rule_format, OF this] and eq_m

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

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

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

   432       proof -

   433         from vt_moment

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

   435         with eq_m show ?thesis by simp

   436       qed

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

   438         by (unfold_locales, auto, cases, auto)

   439       have ?thesis

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

   441         case True

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

   443           by auto

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

   445         show ?thesis by auto

   446       next

   447         case False

   448         from vt_e.block_pre [OF False h1]

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

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

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

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

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

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

   455         show ?thesis

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

   457           case True

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

   459             by auto

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

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

   462             by (unfold_locales, auto, cases, auto)

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

   464           show ?thesis .

   465         next

   466           case False

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

   468           proof -

   469             from vt_moment eqt12

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

   471             with eq_m eqt12 show ?thesis by simp

   472           qed

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

   474             by (unfold_locales, auto, cases, auto)

   475           from vt_e2.block_pre [OF False h1]

   476           have "e = P thread cs2" .

   477           with eq_e1 neq12 show ?thesis by auto

   478         qed

   479       qed

   480     } ultimately show ?thesis by arith

   481   qed

   482 qed

   483 

   484 text {*

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

   486 *}

   487 

   488 lemma waiting_unique:

   489   assumes "waiting s th cs1"

   490   and "waiting s th cs2"

   491   shows "cs1 = cs2"

   492 using waiting_unique_pre assms

   493 unfolding wq_def s_waiting_def

   494 by auto

   495 

   496 end

   497 

   498 (* not used *)

   499 text {*

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

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

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

   503 *}

   504 lemma held_unique:

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

   506   and "holding s th2 cs"

   507   shows "th1 = th2"

   508  by (insert assms, unfold s_holding_def, auto)

   509 

   510 

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

   512   apply (induct s, auto)

   513   by (case_tac a, auto split:if_splits)

   514 

   515 lemma last_set_unique: 

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

   517           \<Longrightarrow> th1 = th2"

   518   apply (induct s, auto)

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

   520 

   521 lemma preced_unique : 

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

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

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

   525   shows "th1 = th2"

   526 proof -

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

   528   from last_set_unique [OF this th_in1 th_in2]

   529   show ?thesis .

   530 qed

   531 

   532 lemma preced_linorder: 

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

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

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

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

   537 proof -

   538   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

   540   thus ?thesis by auto

   541 qed

   542 

   543 (* An aux lemma used later *)

   544 lemma unique_minus:

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

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

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

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

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

   550 proof -

   551  from xz and neq show ?thesis

   552  proof(induct)

   553    case (base ya)

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

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

   556    with base show ?case by auto

   557  next

   558    case (step ya z)

   559    show ?case

   560    proof(cases "y = ya")

   561      case True

   562      from step True show ?thesis by simp

   563    next

   564      case False

   565      from step False

   566      show ?thesis by auto

   567    qed

   568  qed

   569 qed

   570 

   571 lemma unique_base:

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

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

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

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

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

   577 proof -

   578   from xz neq_yz show ?thesis

   579   proof(induct)

   580     case (base ya)

   581     from xy unique base show ?case by auto

   582   next

   583     case (step ya z)

   584     show ?case

   585     proof(cases "y = ya")

   586       case True

   587       from True step show ?thesis by auto

   588     next

   589       case False

   590       from False step 

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

   592       with step show ?thesis by auto

   593     qed

   594   qed

   595 qed

   596 

   597 lemma unique_chain:

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

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

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

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

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

   603 proof -

   604   from xy xz neq_yz show ?thesis

   605   proof(induct)

   606     case (base y)

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

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

   609   next

   610     case (step y za)

   611     show ?case

   612     proof(cases "y = z")

   613       case True

   614       from True step show ?thesis by auto

   615     next

   616       case False

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

   618       thus ?thesis

   619       proof

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

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

   622         thus ?thesis by auto

   623       next

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

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

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

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

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

   629         thus ?thesis by auto

   630       qed

   631     qed

   632   qed

   633 qed

   634 

   635 text {*

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

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

   638   events, respectively.

   639 *}

   640 

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

   642 apply (unfold s_RAG_def s_waiting_def wq_def)

   643 by (simp add:Let_def)

   644 

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

   646 apply (unfold s_RAG_def s_waiting_def wq_def)

   647 by (simp add:Let_def)

   648 

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

   650 apply (unfold s_RAG_def s_waiting_def wq_def)

   651 by (simp add:Let_def)

   652 

   653 

   654 text {* 

   655   The following lemmas are used in the proof of 

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

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

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

   659   starting from the model definitions.

   660 *}

   661 lemma step_v_hold_inv[elim_format]:

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

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

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

   665 proof -

   666   fix c t

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

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

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

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

   671   proof(cases "c = cs")

   672     case False

   673     with nhd hd show ?thesis

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

   675   next

   676     case True

   677     with step_back_step [OF vt] 

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

   679     hence "next_th s th cs t"

   680     proof(cases)

   681       assume "holding s th c"

   682       with nhd hd show ?thesis

   683         apply (unfold s_holding_def cs_holding_def wq_def next_th_def,

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

   685         proof -

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

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

   688           proof(rule someI2)

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

   690           next

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

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

   693           qed

   694           ultimately show False by auto

   695         next

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

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

   698           proof(rule someI2)

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

   700           next

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

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

   703           qed

   704           ultimately show False by auto

   705         qed

   706     qed

   707     with True show ?thesis by auto

   708   qed

   709 qed

   710 

   711 text {* 

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

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

   714 *}

   715 lemma step_v_wait_inv[elim_format]:

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

   717            \<rbrakk>

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

   719 proof -

   720   fix t c 

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

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

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

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

   725     by  (cases, unfold_locales, simp)

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

   727   proof(cases "cs = c")

   728     case False

   729     with nw wt show ?thesis

   730       by (auto simp:cs_waiting_def wq_def Let_def)

   731   next

   732     case True

   733     from nw[folded True] wt[folded True]

   734     have "next_th s th cs t"

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

   736     proof -

   737       fix a list

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

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

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

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

   742       proof(rule someI2)

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

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

   745       next

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

   747           by auto

   748       qed

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

   750     next

   751       fix a list

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

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

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

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

   756       proof(rule someI2)

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

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

   759       next

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

   761           by auto

   762       qed

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

   764     next

   765       fix a list

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

   767       from step_back_step[OF vt]

   768       show "a = th"

   769       proof(cases)

   770         assume "holding s th cs"

   771         with eq_wq show ?thesis

   772           by (unfold s_holding_def wq_def, auto)

   773       qed

   774     qed

   775     with True show ?thesis by simp

   776   qed

   777 qed

   778 

   779 lemma step_v_not_wait[consumes 3]:

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

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

   782 

   783 lemma step_v_release:

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

   785 proof -

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

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

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

   789     by (cases, unfold_locales, simp+)

   790   from step_back_step [OF vt] and hd

   791   show "False"

   792   proof(cases)

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

   794     thus ?thesis

   795       apply (unfold s_holding_def wq_def cs_holding_def)

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

   797     proof -

   798       fix list

   799       assume eq_wq[folded wq_def]: 

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

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

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

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

   804       proof(rule someI2)

   805         from vt_v.wq_distinct[of cs] and eq_wq

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

   807       next

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

   809           by auto

   810       qed

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

   812       proof -

   813         from vt_v.wq_distinct[of cs] and eq_wq

   814         show ?thesis by auto

   815       qed

   816       moreover note eq_wq and hd_in

   817       ultimately show "False" by auto

   818     qed

   819   qed

   820 qed

   821 

   822 lemma step_v_get_hold:

   823   "\<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"

   824   apply (unfold cs_holding_def next_th_def wq_def,

   825          auto simp:Let_def)

   826 proof -

   827   fix rest

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

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

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

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

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

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

   834     by (cases, unfold_locales, simp+)

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

   836   proof(rule someI2)

   837     from vt_v.wq_distinct[of cs] and eq_wq

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

   839   next

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

   841     hence "set x = set rest" by auto

   842     with nrest

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

   844   qed

   845   with ni show "False" by auto

   846 qed

   847 

   848 lemma step_v_release_inv[elim_format]:

   849 "\<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> 

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

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

   852   proof -

   853     fix a list

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

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

   856     proof(cases)

   857       assume "holding s th cs" with eq_wq

   858       show ?thesis

   859         by (unfold s_holding_def wq_def, auto)

   860     qed

   861   next

   862     fix a list

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

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

   865     proof(cases)

   866       assume "holding s th cs" with eq_wq

   867       show ?thesis

   868         by (unfold s_holding_def wq_def, auto)

   869     qed

   870   qed

   871 

   872 lemma step_v_waiting_mono:

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

   874 proof -

   875   fix t c

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

   877   assume vt: "vt ?s'" 

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

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

   880     by (cases, unfold_locales, simp+)

   881   show "waiting (wq s) t c"

   882   proof(cases "c = cs")

   883     case False

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

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

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

   887     with wt show ?thesis by simp

   888   next

   889     case True

   890     with wt show ?thesis

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

   892     proof -

   893       fix a list

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

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

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

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

   898       proof(rule someI2)

   899         from vt_v.wq_distinct [of cs]

   900         and eq_wq[folded wq_def]

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

   902       next

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

   904         thus "set x = set list" by auto

   905       qed

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

   907     next

   908       fix list

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

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

   911       hence "t \<in> set list"

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

   913       proof -

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

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

   916         proof(rule someI2)

   917           from vt_v.wq_distinct [of cs]

   918             and eq_wq[folded wq_def]

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

   920         next

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

   922           thus "set x = set list" by auto

   923         qed

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

   925       qed

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

   927       show False by auto

   928     qed

   929   qed

   930 qed

   931 

   932 text {* (* ddd *) 

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

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

   935 *}

   936 lemma step_RAG_v:

   937 assumes vt:

   938   "vt (V th cs#s)"

   939 shows "

   940   RAG (V th cs # s) =

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

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

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

   944   apply (insert vt, unfold s_RAG_def) 

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

   946   apply (auto elim: step_v_waiting_mono step_v_hold_inv 

   947               step_v_release step_v_wait_inv

   948               step_v_get_hold step_v_release_inv)

   949   apply (erule_tac step_v_not_wait, auto)

   950   done

   951 

   952 text {* 

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

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

   955 *}

   956 lemma step_RAG_p:

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

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

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

   960   apply(simp only: s_RAG_def wq_def)

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

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

   963   apply(fold wq_def)

   964   apply(drule_tac step_back_step)

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

   966   apply(simp add:s_RAG_def wq_def cs_holding_def)

   967   apply(auto)

   968   done

   969 

   970 

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

   972   by (unfold s_RAG_def, auto)

   973 

   974 context valid_trace

   975 begin

   976 

   977 text {*

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

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

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

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

   982 *}

   983 lemma acyclic_RAG:

   984   shows "acyclic (RAG s)"

   985 using vt

   986 proof(induct)

   987   case (vt_cons s e)

   988   interpret vt_s: valid_trace s using vt_cons(1)

   989     by (unfold_locales, simp)

   990   assume ih: "acyclic (RAG s)"

   991     and stp: "step s e"

   992     and vt: "vt s"

   993   show ?case

   994   proof(cases e)

   995     case (Create th prio)

   996     with ih

   997     show ?thesis by (simp add:RAG_create_unchanged)

   998   next

   999     case (Exit th)

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

  1001   next

  1002     case (V th cs)

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

  1004     from step_RAG_v [OF this]

  1005     have eq_de: 

  1006       "RAG (e # s) = 

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

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

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

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

  1011     from step_back_step [OF vtt]

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

  1013     thus ?thesis

  1014     proof(cases)

  1015       assume "holding s th cs"

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

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

  1018       then obtain rest where

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

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

  1021       show ?thesis

  1022       proof(cases "rest = []")

  1023         case False

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

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

  1026           by (unfold next_th_def, auto)

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

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

  1029         proof

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

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

  1032           from tranclD [OF this]

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

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

  1035           from RAG_target_th [OF this]

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

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

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

  1039             unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp

  1040           hence "cs' = cs"

  1041           proof(rule vt_s.waiting_unique)

  1042             from eq_wq vt_s.wq_distinct[of cs]

  1043             show "waiting s ?th' cs" 

  1044               apply (unfold s_waiting_def wq_def, auto)

  1045             proof -

  1046               assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"

  1047                 and eq_wq: "wq_fun (schs s) cs = th # rest"

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

  1049               proof(rule someI2)

  1050                 from vt_s.wq_distinct[of cs] and eq_wq

  1051                 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto

  1052               next

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

  1054                 with False show "x \<noteq> []" by auto

  1055               qed

  1056               hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 

  1057                 set (SOME q. distinct q \<and> set q = set rest)" by auto

  1058               moreover have "\<dots> = set rest" 

  1059               proof(rule someI2)

  1060                 from vt_s.wq_distinct[of cs] and eq_wq

  1061                 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto

  1062               next

  1063                 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto

  1064               qed

  1065               moreover note hd_in

  1066               ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto

  1067             next

  1068               assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"

  1069                 and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"

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

  1071               proof(rule someI2)

  1072                 from vt_s.wq_distinct[of cs] and eq_wq

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

  1074               next

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

  1076                 with False show "x \<noteq> []" by auto

  1077               qed

  1078               hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> 

  1079                 set (SOME q. distinct q \<and> set q = set rest)" by auto

  1080               moreover have "\<dots> = set rest" 

  1081               proof(rule someI2)

  1082                 from vt_s.wq_distinct[of cs] and eq_wq

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

  1084               next

  1085                 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto

  1086               qed

  1087               moreover note hd_in

  1088               ultimately show False by auto

  1089             qed

  1090           qed

  1091           with th'_e eq_x have "(Th ?th', Cs cs) \<in> ?E" by simp

  1092           with False

  1093           show "False" by (auto simp: next_th_def eq_wq)

  1094         qed

  1095         with acyclic_insert[symmetric] and ac

  1096           and eq_de eq_D show ?thesis by auto

  1097       next

  1098         case True

  1099         with eq_wq

  1100         have eq_D: "?D = {}"

  1101           by (unfold next_th_def, auto)

  1102         with eq_de ac

  1103         show ?thesis by auto

  1104       qed 

  1105     qed

  1106   next

  1107     case (P th cs)

  1108     from P vt stp have vtt: "vt (P th cs#s)" by auto

  1109     from step_RAG_p [OF this] P

  1110     have "RAG (e # s) = 

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

  1112       RAG s \<union> {(Th th, Cs cs)})" (is "?L = ?R")

  1113       by simp

  1114     moreover have "acyclic ?R"

  1115     proof(cases "wq s cs = []")

  1116       case True

  1117       hence eq_r: "?R =  RAG s \<union> {(Cs cs, Th th)}" by simp

  1118       have "(Th th, Cs cs) \<notin> (RAG s)\<^sup>*"

  1119       proof

  1120         assume "(Th th, Cs cs) \<in> (RAG s)\<^sup>*"

  1121         hence "(Th th, Cs cs) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)

  1122         from tranclD2 [OF this]

  1123         obtain x where "(x, Cs cs) \<in> RAG s" by auto

  1124         with True show False by (auto simp:s_RAG_def cs_waiting_def)

  1125       qed

  1126       with acyclic_insert ih eq_r show ?thesis by auto

  1127     next

  1128       case False

  1129       hence eq_r: "?R =  RAG s \<union> {(Th th, Cs cs)}" by simp

  1130       have "(Cs cs, Th th) \<notin> (RAG s)\<^sup>*"

  1131       proof

  1132         assume "(Cs cs, Th th) \<in> (RAG s)\<^sup>*"

  1133         hence "(Cs cs, Th th) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)

  1134         moreover from step_back_step [OF vtt] have "step s (P th cs)" .

  1135         ultimately show False