1 theory Prio

     2 imports Precedence_ord Moment Lsp Happen_within

     3 begin

     4 

     5 type_synonym thread = nat

     6 type_synonym priority = nat

     7 type_synonym cs = nat

     8 

     9 datatype event = 

    10   Create thread priority |

    11   Exit thread |

    12   P thread cs |

    13   V thread cs |

    14   Set thread priority

    15 

    16 datatype node = 

    17    Th "thread" |

    18    Cs "cs"

    19 

    20 type_synonym state = "event list"

    21 

    22 fun threads :: "state \<Rightarrow> thread set"

    23 where 

    24   "threads [] = {}" |

    25   "threads (Create thread prio#s) = {thread} \<union> threads s" |

    26   "threads (Exit thread # s) = (threads s) - {thread}" |

    27   "threads (e#s) = threads s"

    28 

    29 fun original_priority :: "thread \<Rightarrow> state \<Rightarrow> nat"

    30 where

    31   "original_priority thread [] = 0" |

    32   "original_priority thread (Create thread' prio#s) = 

    33      (if thread' = thread then prio else original_priority thread s)" |

    34   "original_priority thread (Set thread' prio#s) = 

    35      (if thread' = thread then prio else original_priority thread s)" |

    36   "original_priority thread (e#s) = original_priority thread s"

    37 

    38 fun birthtime :: "thread \<Rightarrow> state \<Rightarrow> nat"

    39 where

    40   "birthtime thread [] = 0" |

    41   "birthtime thread ((Create thread' prio)#s) = (if (thread = thread') then length s 

    42                                                   else birthtime thread s)" |

    43   "birthtime thread ((Set thread' prio)#s) = (if (thread = thread') then length s 

    44                                                   else birthtime thread s)" |

    45   "birthtime thread (e#s) = birthtime thread s"

    46 

    47 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"

    48   where "preced thread s = Prc (original_priority thread s) (birthtime thread s)"

    49 

    50 consts holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"

    51        waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"

    52        depend :: "'b \<Rightarrow> (node \<times> node) set"

    53        dependents :: "'b \<Rightarrow> thread \<Rightarrow> thread set"

    54 

    55 defs (overloaded) cs_holding_def: "holding wq thread cs == (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"

    56                   cs_waiting_def: "waiting wq thread cs == (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"

    57                   cs_depend_def: "depend (wq::cs \<Rightarrow> thread list) == {(Th t, Cs c) | t c. waiting wq t c} \<union> 

    58                                                {(Cs c, Th t) | c t. holding wq t c}"

    59                   cs_dependents_def: "dependents (wq::cs \<Rightarrow> thread list) th == {th' . (Th th', Th th) \<in> (depend wq)^+}"

    60 

    61 record schedule_state = 

    62     waiting_queue :: "cs \<Rightarrow> thread list"

    63     cur_preced :: "thread \<Rightarrow> precedence"

    64 

    65 

    66 definition cpreced :: "state \<Rightarrow> (cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> precedence"

    67 where "cpreced s wq = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"

    68 

    69 fun schs :: "state \<Rightarrow> schedule_state"

    70 where

    71    "schs [] = \<lparr>waiting_queue = \<lambda> cs. [], 

    72                cur_preced = cpreced [] (\<lambda> cs. [])\<rparr>" |

    73    "schs (e#s) = (let ps = schs s in

    74                   let pwq = waiting_queue ps in

    75                   let pcp = cur_preced ps in

    76                   let nwq = case e of

    77                              P thread cs \<Rightarrow>  pwq(cs:=(pwq cs @ [thread])) |

    78                              V thread cs \<Rightarrow> let nq = case (pwq cs) of

    79                                                       [] \<Rightarrow> [] | 

    80                                                       (th#pq) \<Rightarrow> case (lsp pcp pq) of

    81                                                                    (l, [], r) \<Rightarrow> []

    82                                                                  | (l, m#ms, r) \<Rightarrow> m#(l@ms@r)

    83                                             in pwq(cs:=nq)                 |

    84                               _ \<Rightarrow> pwq

    85                   in let ncp = cpreced (e#s) nwq in 

    86                      \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>

    87                  )"

    88 

    89 definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 

    90 where "wq s == waiting_queue (schs s)"

    91 

    92 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"

    93 where "cp s = cur_preced (schs s)"

    94 

    95 defs (overloaded) s_holding_def: "holding (s::state) thread cs == (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))"

    96                   s_waiting_def: "waiting (s::state) thread cs == (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"

    97                   s_depend_def: "depend (s::state) == {(Th t, Cs c) | t c. waiting (wq s) t c} \<union> 

    98                                                {(Cs c, Th t) | c t. holding (wq s) t c}"

    99                   s_dependents_def: "dependents (s::state) th == {th' . (Th th', Th th) \<in> (depend (wq s))^+}"

   100 

   101 definition readys :: "state \<Rightarrow> thread set"

   102 where

   103   "readys s = 

   104      {thread . thread \<in> threads s \<and> (\<forall> cs. \<not> waiting s thread cs)}"

   105 

   106 definition runing :: "state \<Rightarrow> thread set"

   107 where "runing s = {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"

   108 

   109 definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"

   110   where "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"

   111 

   112 inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"

   113 where

   114   thread_create: "\<lbrakk>prio \<le> max_prio; thread \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create thread prio)" |

   115   thread_exit: "\<lbrakk>thread \<in> runing s; holdents s thread = {}\<rbrakk> \<Longrightarrow> step s (Exit thread)" |

   116   thread_P: "\<lbrakk>thread \<in> runing s;  (Cs cs, Th thread)  \<notin> (depend s)^+\<rbrakk> \<Longrightarrow> step s (P thread cs)" |

   117   thread_V: "\<lbrakk>thread \<in> runing s;  holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |

   118   thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"

   119 

   120 inductive vt :: "(state \<Rightarrow> event \<Rightarrow> bool) \<Rightarrow> state \<Rightarrow> bool"

   121  for cs

   122 where

   123   vt_nil[intro]: "vt cs []" |

   124   vt_cons[intro]: "\<lbrakk>vt cs s; cs s e\<rbrakk> \<Longrightarrow> vt cs (e#s)"

   125 

   126 lemma runing_ready: "runing s \<subseteq> readys s"

   127   by (auto simp only:runing_def readys_def)

   128 

   129 lemma wq_v_eq_nil: 

   130   fixes s cs thread rest

   131   assumes eq_wq: "wq s cs = thread # rest"

   132   and eq_lsp: "lsp (cp s) rest = (l, [], r)"

   133   shows "wq (V thread cs#s) cs = []"

   134 proof -

   135   from prems show ?thesis

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

   137 qed

   138 

   139 lemma wq_v_eq: 

   140   fixes s cs thread rest

   141   assumes eq_wq: "wq s cs = thread # rest"

   142   and eq_lsp: "lsp (cp s) rest = (l, [th'], r)"

   143   shows "wq (V thread cs#s) cs = th'#l@r"

   144 proof -

   145   from prems show ?thesis

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

   147 qed

   148 

   149 lemma wq_v_neq:

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

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

   152 

   153 lemma wq_distinct: "vt step s \<Longrightarrow> distinct (wq s cs)"

   154 proof(erule_tac vt.induct, simp add:wq_def)

   155   fix s e

   156   assume h1: "step s e"

   157   and h2: "distinct (wq s cs)"

   158   thus "distinct (wq (e # s) cs)"

   159   proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)

   160     fix thread s

   161     assume h1: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"

   162       and h2: "thread \<in> set (waiting_queue (schs s) cs)"

   163       and h3: "thread \<in> runing s"

   164     show "False" 

   165     proof -

   166       from h3 have "\<And> cs. thread \<in>  set (waiting_queue (schs s) cs) \<Longrightarrow> 

   167                              thread = hd ((waiting_queue (schs s) cs))" 

   168         by (simp add:runing_def readys_def s_waiting_def wq_def)

   169       from this [OF h2] have "thread = hd (waiting_queue (schs s) cs)" .

   170       with h2

   171       have "(Cs cs, Th thread) \<in> (depend s)"

   172         by (simp add:s_depend_def s_holding_def wq_def cs_holding_def)

   173       with h1 show False by auto

   174     qed

   175   next

   176     fix thread s a list

   177     assume h1: "thread \<in> runing s" 

   178       and h2: "holding s thread cs"

   179       and h3: "waiting_queue (schs s) cs = a # list"

   180       and h4: "a \<notin> set list"

   181       and h5: "distinct list"

   182     thus "distinct

   183            ((\<lambda>(l, a, r). case a of [] \<Rightarrow> [] | m # ms \<Rightarrow> m # l @ ms @ r)

   184              (lsp (cur_preced (schs s)) list))"

   185     apply (cases "(lsp (cur_preced (schs s)) list)", simp)

   186     apply (case_tac b, simp)

   187     by (drule_tac lsp_set_eq, simp)

   188   qed

   189 qed

   190 

   191 lemma block_pre: 

   192   fixes thread cs s

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

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

   195   shows "e = P thread cs"

   196 proof -

   197   have ee: "\<And> x y. \<lbrakk>x = y\<rbrakk> \<Longrightarrow> set x = set y"

   198     by auto

   199   from s_ni s_i show ?thesis

   200   proof (cases e, auto split:if_splits simp add:Let_def wq_def)

   201     fix uu uub uuc uud uue

   202     assume h: "(uuc, thread # uu, uub) = lsp (cur_preced (schs s)) uud"

   203       and h1 [symmetric]: "uue # uud = waiting_queue (schs s) cs"

   204       and h2: "thread \<notin> set (waiting_queue (schs s) cs)"

   205     from lsp_set [OF h] have "set (uuc @ (thread # uu) @ uub) = set uud" .

   206     hence "thread \<in> set uud" by auto

   207     with h1 have "thread \<in> set (waiting_queue (schs s) cs)" by auto

   208     with h2 show False by auto

   209   next

   210     fix uu uua uub uuc uud uue

   211     assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"

   212       and h2: "uue # uud = waiting_queue (schs s) cs"

   213       and h3: "(uuc, uua # uu, uub) = lsp (cur_preced (schs s)) uud"

   214       and h4: "thread \<in> set uuc"

   215     from lsp_set [OF h3] have "set (uuc @ (uua # uu) @ uub) = set uud" .

   216     with h4 have "thread \<in> set uud" by auto

   217     with h2 have "thread \<in> set (waiting_queue (schs s) cs)" 

   218       apply (drule_tac ee) by auto

   219     with h1 show "False" by fast

   220   next

   221     fix uu uua uub uuc uud uue

   222     assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"

   223       and h2: "uue # uud = waiting_queue (schs s) cs"

   224       and h3: "(uuc, uua # uu, uub) = lsp (cur_preced (schs s)) uud"

   225       and h4: "thread \<in> set uu"

   226     from lsp_set [OF h3] have "set (uuc @ (uua # uu) @ uub) = set uud" .

   227     with h4 have "thread \<in> set uud" by auto

   228     with h2 have "thread \<in> set (waiting_queue (schs s) cs)" 

   229       apply (drule_tac ee) by auto

   230     with h1 show "False" by fast

   231   next

   232     fix uu uua uub uuc uud uue

   233     assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"

   234       and h2: "uue # uud = waiting_queue (schs s) cs"

   235       and h3: "(uuc, uua # uu, uub) = lsp (cur_preced (schs s)) uud"

   236       and h4: "thread \<in> set uub"

   237     from lsp_set [OF h3] have "set (uuc @ (uua # uu) @ uub) = set uud" .

   238     with h4 have "thread \<in> set uud" by auto

   239     with h2 have "thread \<in> set (waiting_queue (schs s) cs)" 

   240       apply (drule_tac ee) by auto

   241     with h1 show "False" by fast

   242   qed

   243 qed

   244 

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

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

   247 apply (ind_cases "vt step ((P thread cs)#s)")

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

   249 by auto

   250 

   251 lemma abs1:

   252   fixes e es

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

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

   255   shows "False"

   256 proof -

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

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

   259   with neq show ?thesis by auto

   260 qed

   261 

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

   263   by (cases es, auto)

   264 

   265 inductive_cases evt_cons: "vt cs (a#s)"

   266 

   267 lemma abs2:

   268   assumes vt: "vt step (e#s)"

   269   and inq: "thread \<in> set (wq s cs)"

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

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

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

   273   shows "False"

   274 proof -

   275   have ee: "\<And> uuc thread uu uub s list. (uuc, thread # uu, uub) = lsp (cur_preced (schs s)) list \<Longrightarrow> 

   276                  lsp (cur_preced (schs s)) list = (uuc, thread # uu, uub) 

   277                " by simp

   278   from prems show "False"

   279     apply (cases e)

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

   281     apply (insert abs1, fast)[1] 

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

   283     apply (simp split:if_splits list.splits add:Let_def wq_def) 

   284     apply (auto dest!:ee)

   285     apply (drule_tac lsp_set_eq, simp)

   286     apply (subgoal_tac "distinct (waiting_queue (schs s) cs)", simp, fold wq_def)

   287     apply (rule_tac wq_distinct, auto)

   288     apply (erule_tac evt_cons, auto)

   289     apply (drule_tac lsp_set_eq, simp)

   290     apply (subgoal_tac "distinct (wq s cs)", simp)

   291     apply (rule_tac wq_distinct, auto)

   292     apply (erule_tac evt_cons, auto)

   293     apply (drule_tac lsp_set_eq, simp)

   294     apply (subgoal_tac "distinct (wq s cs)", simp)

   295     apply (rule_tac wq_distinct, auto)

   296     apply (erule_tac evt_cons, auto)

   297     apply (auto simp:wq_def Let_def split:if_splits prod.splits)

   298     done

   299 qed

   300 

   301 lemma vt_moment: "\<And> t. \<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"

   302 proof(induct s, simp)

   303   fix a s t

   304   assume h: "\<And>t.\<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"

   305     and vt_a: "vt cs (a # s)"

   306     and le_t: "t \<le> length (a # s)"

   307   show "vt cs (moment t (a # s))"

   308   proof(cases "t = length (a#s)")

   309     case True

   310     from True have "moment t (a#s) = a#s" by simp

   311     with vt_a show ?thesis by simp

   312   next

   313     case False

   314     with le_t have le_t1: "t \<le> length s" by simp

   315     from vt_a have "vt cs s"

   316       by (erule_tac evt_cons, simp)

   317     from h [OF this le_t1] have "vt cs (moment t s)" .

   318     moreover have "moment t (a#s) = moment t s"

   319     proof -

   320       from moment_app [OF le_t1, of "[a]"] 

   321       show ?thesis by simp

   322     qed

   323     ultimately show ?thesis by auto

   324   qed

   325 qed

   326 

   327 (* Wrong:

   328     lemma \<lbrakk>thread \<in> set (waiting_queue cs1 s); thread \<in> set (waiting_queue cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"

   329 *)

   330 

   331 lemma waiting_unique_pre:

   332   fixes cs1 cs2 s thread

   333   assumes vt: "vt step s"

   334   and h11: "thread \<in> set (wq s cs1)"

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

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

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

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

   339   shows "False"

   340 proof -

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   358   show ?thesis

   359   proof -

   360     { 

   361       assume lt12: "t1 < t2"

   362       let ?t3 = "Suc t2"

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

   364       from moment_plus [OF this] 

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

   366       have "t2 < ?t3" by simp

   367       from nn2 [rule_format, OF this] and eq_m

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

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

   370       have vt_e: "vt step (e#moment t2 s)"

   371       proof -

   372         from vt_moment [OF vt le_t3]

   373         have "vt step (moment ?t3 s)" .

   374         with eq_m show ?thesis by simp

   375       qed

   376       have ?thesis

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

   378         case True

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

   380           by auto

   381         from abs2 [OF vt_e True eq_th h2 h1]

   382         show ?thesis by auto

   383       next

   384         case False

   385         from block_pre [OF False h1]

   386         have "e = P thread cs2" .

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

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

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

   390         with nn1 [rule_format, OF lt12]

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

   392       qed

   393     } moreover {

   394       assume lt12: "t2 < t1"

   395       let ?t3 = "Suc t1"

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

   397       from moment_plus [OF this] 

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

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

   400       from nn1 [rule_format, OF this] and eq_m

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

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

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

   404       proof -

   405         from vt_moment [OF vt le_t3]

   406         have "vt step (moment ?t3 s)" .

   407         with eq_m show ?thesis by simp

   408       qed

   409       have ?thesis

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

   411         case True

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

   413           by auto

   414         from abs2 [OF vt_e True eq_th h2 h1]

   415         show ?thesis by auto

   416       next

   417         case False

   418         from block_pre [OF False h1]

   419         have "e = P thread cs1" .

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

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

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

   423         with nn2 [rule_format, OF lt12]

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

   425       qed

   426     } moreover {

   427       assume eqt12: "t1 = t2"

   428       let ?t3 = "Suc t1"

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

   430       from moment_plus [OF this] 

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

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

   433       from nn1 [rule_format, OF this] and eq_m

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

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

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

   437       proof -

   438         from vt_moment [OF vt le_t3]

   439         have "vt step (moment ?t3 s)" .

   440         with eq_m show ?thesis by simp

   441       qed

   442       have ?thesis

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

   444         case True

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

   446           by auto

   447         from abs2 [OF vt_e True eq_th h2 h1]

   448         show ?thesis by auto

   449       next

   450         case False

   451         from block_pre [OF False h1]

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

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

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

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

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

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

   458         show ?thesis

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

   460           case True

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

   462             by auto

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

   464           from abs2 [OF this True eq_th h2 h1]

   465           show ?thesis .

   466         next

   467           case False

   468           from block_pre [OF False h1]

   469           have "e = P thread cs2" .

   470           with eq_e1 neq12 show ?thesis by auto

   471         qed

   472       qed

   473     } ultimately show ?thesis by arith

   474   qed

   475 qed

   476 

   477 lemma waiting_unique:

   478   assumes "vt step s"

   479   and "waiting s th cs1"

   480   and "waiting s th cs2"

   481   shows "cs1 = cs2"

   482 proof -

   483   from waiting_unique_pre and prems

   484   show ?thesis

   485     by (auto simp add:s_waiting_def)

   486 qed

   487 

   488 lemma holded_unique:

   489   assumes "vt step s"

   490   and "holding s th1 cs"

   491   and "holding s th2 cs"

   492   shows "th1 = th2"

   493 proof -

   494   from prems show ?thesis

   495     unfolding s_holding_def

   496     by auto

   497 qed

   498 

   499 lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s"

   500   apply (induct s, auto)

   501   by (case_tac a, auto split:if_splits)

   502 

   503 lemma birthtime_unique: 

   504   "\<lbrakk>birthtime th1 s = birthtime th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>

   505           \<Longrightarrow> th1 = th2"

   506   apply (induct s, auto)

   507   by (case_tac a, auto split:if_splits dest:birthtime_lt)

   508 

   509 lemma preced_unique : 

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

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

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

   513   shows "th1 = th2"

   514 proof -

   515   from pcd_eq have "birthtime th1 s = birthtime th2 s" by (simp add:preced_def)

   516   from birthtime_unique [OF this th_in1 th_in2]

   517   show ?thesis .

   518 qed

   519 

   520 lemma preced_linorder: 

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

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

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

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

   525 proof -

   526   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

   528   thus ?thesis by auto

   529 qed

   530 

   531 lemma unique_minus:

   532   fixes x y z r

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

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

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

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

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

   538 proof -

   539  from xz and neq show ?thesis

   540  proof(induct)

   541    case (base ya)

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

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

   544    with base show ?case by auto

   545  next

   546    case (step ya z)

   547    show ?case

   548    proof(cases "y = ya")

   549      case True

   550      from step True show ?thesis by simp

   551    next

   552      case False

   553      from step False

   554      show ?thesis by auto

   555    qed

   556  qed

   557 qed

   558 

   559 lemma unique_base:

   560   fixes r x y z

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

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

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

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

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

   566 proof -

   567   from xz neq_yz show ?thesis

   568   proof(induct)

   569     case (base ya)

   570     from xy unique base show ?case by auto

   571   next

   572     case (step ya z)

   573     show ?case

   574     proof(cases "y = ya")

   575       case True

   576       from True step show ?thesis by auto

   577     next

   578       case False

   579       from False step 

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

   581       with step show ?thesis by auto

   582     qed

   583   qed

   584 qed

   585 

   586 lemma unique_chain:

   587   fixes r x y z

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

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

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

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

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

   593 proof -

   594   from xy xz neq_yz show ?thesis

   595   proof(induct)

   596     case (base y)

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

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

   599   next

   600     case (step y za)

   601     show ?case

   602     proof(cases "y = z")

   603       case True

   604       from True step show ?thesis by auto

   605     next

   606       case False

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

   608       thus ?thesis

   609       proof

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

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

   612         thus ?thesis by auto

   613       next

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

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

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

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

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

   619         thus ?thesis by auto

   620       qed

   621     qed

   622   qed

   623 qed

   624 

   625 lemma depend_set_unchanged: "(depend (Set th prio # s)) = depend s"

   626 apply (unfold s_depend_def s_waiting_def wq_def)

   627 by (simp add:Let_def)

   628 

   629 lemma depend_create_unchanged: "(depend (Create th prio # s)) = depend s"

   630 apply (unfold s_depend_def s_waiting_def wq_def)

   631 by (simp add:Let_def)

   632 

   633 lemma depend_exit_unchanged: "(depend (Exit th # s)) = depend s"

   634 apply (unfold s_depend_def s_waiting_def wq_def)

   635 by (simp add:Let_def)

   636 

   637 definition head_of :: "('a \<Rightarrow> 'b::linorder) \<Rightarrow> 'a set \<Rightarrow> 'a set"

   638   where "head_of f A = {a . a \<in> A \<and> f a = Max (f ` A)}"

   639 

   640 definition wq_head :: "state \<Rightarrow> cs \<Rightarrow> thread set"

   641   where "wq_head s cs = head_of (cp s) (set (wq s cs))"

   642 

   643 lemma f_nil_simp: "\<lbrakk>f cs = []\<rbrakk> \<Longrightarrow> f(cs:=[]) = f"

   644 proof

   645   fix x

   646   assume h:"f cs = []"

   647   show "(f(cs := [])) x = f x"

   648   proof(cases "cs = x")

   649     case True

   650     with h show ?thesis by simp

   651   next

   652     case False

   653     with h show ?thesis by simp

   654   qed

   655 qed

   656 

   657 lemma step_back_vt: "vt ccs (e#s) \<Longrightarrow> vt ccs s"

   658   by(ind_cases "vt ccs (e#s)", simp)

   659 

   660 lemma step_back_step: "vt ccs (e#s) \<Longrightarrow> ccs s e"

   661   by(ind_cases "vt ccs (e#s)", simp)

   662 

   663 lemma holding_nil:

   664     "\<lbrakk>wq s cs = []; holding (wq s) th cs\<rbrakk> \<Longrightarrow> False"

   665   by (unfold cs_holding_def, auto)

   666 

   667 lemma waiting_kept_1: "

   668        \<lbrakk>vt step (V th cs#s); wq s cs = a # list; waiting ((wq s)(cs := ab # aa @ lista @ ca)) t c;

   669         lsp (cp s) list = (aa, ab # lista, ca)\<rbrakk>

   670        \<Longrightarrow> waiting (wq s) t c"

   671   apply (drule_tac step_back_vt, drule_tac wq_distinct[of _ cs])

   672   apply(drule_tac lsp_set_eq)

   673   by (unfold cs_waiting_def, auto split:if_splits)

   674  

   675 lemma waiting_kept_2: 

   676   "\<And>a list t c aa ca.

   677        \<lbrakk>wq s cs = a # list; waiting ((wq s)(cs := [])) t c; lsp (cp s) list = (aa, [], ca)\<rbrakk>

   678        \<Longrightarrow> waiting (wq s) t c"

   679   apply(drule_tac lsp_set_eq)

   680   by (unfold cs_waiting_def, auto split:if_splits)

   681   

   682 

   683 lemma holding_nil_simp: "\<lbrakk>holding ((wq s)(cs := [])) t c\<rbrakk> \<Longrightarrow> holding (wq s) t c"

   684   by(unfold cs_holding_def, auto)

   685 

   686 lemma step_wq_elim: "\<lbrakk>vt step (V th cs#s); wq s cs = a # list; a \<noteq> th\<rbrakk> \<Longrightarrow> False"

   687   apply(drule_tac step_back_step)

   688   apply(ind_cases "step s (V th cs)")

   689   by(unfold s_holding_def, auto)

   690 

   691 lemma holding_cs_neq_simp: "c \<noteq> cs \<Longrightarrow> holding ((wq s)(cs := u)) t c = holding (wq s) t c"

   692   by (unfold cs_holding_def, auto)

   693 

   694 lemma holding_th_neq_elim:

   695   "\<And>a list c t aa ca ab lista.

   696        \<lbrakk>\<not> holding (wq s) t c; holding ((wq s)(cs := ab # aa @ lista @ ca)) t c;

   697          ab \<noteq> t\<rbrakk>

   698        \<Longrightarrow> False"

   699   by (unfold cs_holding_def, auto split:if_splits)

   700 

   701 lemma holding_nil_abs:

   702   "\<not> holding ((wq s)(cs := [])) th cs"

   703   by (unfold cs_holding_def, auto split:if_splits)

   704 

   705 lemma holding_abs: "\<lbrakk>holding ((wq s)(cs := ab # aa @ lista @ c)) th cs; ab \<noteq> th\<rbrakk>

   706        \<Longrightarrow> False"

   707     by (unfold cs_holding_def, auto split:if_splits)

   708 

   709 lemma waiting_abs: "\<not> waiting ((wq s)(cs := t # l @ r)) t cs"

   710     by (unfold cs_waiting_def, auto split:if_splits)

   711 

   712 lemma waiting_abs_1: 

   713   "\<lbrakk>\<not> waiting ((wq s)(cs := [])) t c; waiting (wq s) t c; c \<noteq> cs\<rbrakk>

   714        \<Longrightarrow> False"

   715     by (unfold cs_waiting_def, auto split:if_splits)

   716 

   717 lemma waiting_abs_2: "

   718        \<lbrakk>\<not> waiting ((wq s)(cs := ab # aa @ lista @ ca)) t c; waiting (wq s) t c;

   719         c \<noteq> cs\<rbrakk>

   720        \<Longrightarrow> False"

   721   by (unfold cs_waiting_def, auto split:if_splits)

   722 

   723 lemma waiting_abs_3:

   724      "\<lbrakk>wq s cs = a # list; \<not> waiting ((wq s)(cs := [])) t c;

   725         waiting (wq s) t c; lsp (cp s) list = (aa, [], ca)\<rbrakk>

   726        \<Longrightarrow> False"

   727   apply(drule_tac lsp_mid_nil, simp)

   728   by(unfold cs_waiting_def, auto split:if_splits)

   729 

   730 lemma waiting_simp: "c \<noteq> cs \<Longrightarrow> waiting ((wq s)(cs:=z)) t c = waiting (wq s) t c"

   731    by(unfold cs_waiting_def, auto split:if_splits)

   732 

   733 lemma holding_cs_eq:

   734   "\<lbrakk>\<not> holding ((wq s)(cs := [])) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> c = cs"

   735    by(unfold cs_holding_def, auto split:if_splits)

   736 

   737 lemma holding_cs_eq_1:

   738   "\<lbrakk>\<not> holding ((wq s)(cs := ab # aa @ lista @ ca)) t c; holding (wq s) t c\<rbrakk>

   739        \<Longrightarrow> c = cs"

   740    by(unfold cs_holding_def, auto split:if_splits)

   741 

   742 lemma holding_th_eq: 

   743        "\<lbrakk>vt step (V th cs#s); wq s cs = a # list; \<not> holding ((wq s)(cs := [])) t c; holding (wq s) t c;

   744         lsp (cp s) list = (aa, [], ca)\<rbrakk>

   745        \<Longrightarrow> t = th"

   746   apply(drule_tac lsp_mid_nil, simp)

   747   apply(unfold cs_holding_def, auto split:if_splits)

   748   apply(drule_tac step_back_step)

   749   apply(ind_cases "step s (V th cs)")

   750   by (unfold s_holding_def, auto split:if_splits)

   751 

   752 lemma holding_th_eq_1:

   753   "\<lbrakk>vt step (V th cs#s); 

   754      wq s cs = a # list; \<not> holding ((wq s)(cs := ab # aa @ lista @ ca)) t c; holding (wq s) t c;

   755         lsp (cp s) list = (aa, ab # lista, ca)\<rbrakk>

   756        \<Longrightarrow> t = th"

   757   apply(drule_tac step_back_step)

   758   apply(ind_cases "step s (V th cs)")

   759   apply(unfold s_holding_def cs_holding_def)

   760   by (auto split:if_splits)

   761 

   762 lemma holding_th_eq_2: "\<lbrakk>holding ((wq s)(cs := ac # x)) th cs\<rbrakk>

   763        \<Longrightarrow> ac = th"

   764   by (unfold cs_holding_def, auto)

   765 

   766 lemma holding_th_eq_3: "

   767        \<lbrakk>\<not> holding (wq s) t c;

   768         holding ((wq s)(cs := ac # x)) t c\<rbrakk>

   769        \<Longrightarrow> ac = t"

   770   by (unfold cs_holding_def, auto)

   771 

   772 lemma holding_wq_eq: "holding ((wq s)(cs := th' # l @ r)) th' cs"

   773    by (unfold cs_holding_def, auto)

   774 

   775 lemma waiting_th_eq: "

   776        \<lbrakk>waiting (wq s) t c; wq s cs = a # list;

   777         lsp (cp s) list = (aa, ac # lista, ba); \<not> waiting ((wq s)(cs := ac # aa @ lista @ ba)) t c\<rbrakk>

   778        \<Longrightarrow> ac = t"

   779   apply(drule_tac lsp_set_eq, simp)

   780   by (unfold cs_waiting_def, auto split:if_splits)

   781 

   782 lemma step_depend_v:

   783   "vt step (V th cs#s) \<Longrightarrow>

   784   depend (V th cs # s) =

   785   depend s - {(Cs cs, Th th)} -

   786   {(Th th', Cs cs) |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))} \<union>

   787   {(Cs cs, Th th') |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))}"

   788   apply (unfold s_depend_def wq_def, 

   789          auto split:list.splits simp:Let_def f_nil_simp holding_wq_eq, fold wq_def cp_def)

   790   apply (auto split:list.splits prod.splits  

   791                simp:Let_def f_nil_simp holding_nil_simp holding_cs_neq_simp holding_nil_abs

   792                     waiting_abs waiting_simp holding_wq_eq

   793                elim:holding_nil waiting_kept_1 waiting_kept_2 step_wq_elim holding_th_neq_elim 

   794                holding_abs waiting_abs_1 waiting_abs_3 holding_cs_eq holding_cs_eq_1

   795                holding_th_eq holding_th_eq_1 holding_th_eq_2 holding_th_eq_3 waiting_th_eq

   796                dest:lsp_mid_length)

   797   done

   798 

   799 lemma step_depend_p:

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

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

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

   803   apply(unfold s_depend_def wq_def)

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

   805   apply(case_tac "c = cs", auto)

   806   apply(fold wq_def)

   807   apply(drule_tac step_back_step)

   808   by (ind_cases " step s (P (hd (wq s cs)) cs)", 

   809     auto simp:s_depend_def wq_def cs_holding_def)

   810 

   811 lemma simple_A:

   812   fixes A

   813   assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"

   814   shows "A = {} \<or> (\<exists> a. A = {a})"

   815 proof(cases "A = {}")

   816   case True thus ?thesis by simp

   817 next

   818   case False then obtain a where "a \<in> A" by auto

   819   with h have "A = {a}" by auto

   820   thus ?thesis by simp

   821 qed

   822 

   823 lemma depend_target_th: "(Th th, x) \<in> depend (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"

   824   by (unfold s_depend_def, auto)

   825 

   826 lemma acyclic_depend: 

   827   fixes s

   828   assumes vt: "vt step s"

   829   shows "acyclic (depend s)"

   830 proof -

   831   from vt show ?thesis

   832   proof(induct)

   833     case (vt_cons s e)

   834     assume ih: "acyclic (depend s)"

   835       and stp: "step s e"

   836       and vt: "vt step s"

   837     show ?case

   838     proof(cases e)

   839       case (Create th prio)

   840       with ih

   841       show ?thesis by (simp add:depend_create_unchanged)

   842     next

   843       case (Exit th)

   844       with ih show ?thesis by (simp add:depend_exit_unchanged)

   845     next

   846       case (V th cs)

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

   848       from step_depend_v [OF this]

   849       have eq_de: "depend (e # s) = 

   850         depend s - {(Cs cs, Th th)} -

   851         {(Th th', Cs cs) |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))} \<union>

   852         {(Cs cs, Th th') |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))}"

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

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

   855       have "?D = {} \<or> (\<exists> a. ?D = {a})" by (rule simple_A, auto)

   856       thus ?thesis

   857       proof(cases "wq s cs")

   858         case Nil

   859         hence "?D = {}" by simp

   860         with ac and eq_de show ?thesis by simp

   861       next

   862         case (Cons tth rest)

   863         from stp and V have "step s (V th cs)" by simp

   864         hence eq_wq: "wq s cs = th # rest"

   865         proof -

   866           show "step s (V th cs) \<Longrightarrow> wq s cs = th # rest"

   867             apply(ind_cases "step s (V th cs)")

   868             by(insert Cons, unfold s_holding_def, simp)

   869         qed

   870         show ?thesis

   871         proof(cases "lsp (cp s) rest")

   872           fix l b r

   873           assume eq_lsp: "lsp (cp s) rest = (l, b, r) "

   874           show ?thesis

   875           proof(cases "b")

   876             case Nil

   877             with eq_lsp and eq_wq have "?D = {}" by simp

   878             with ac and eq_de show ?thesis by simp

   879           next

   880             case (Cons th' m)

   881             with eq_lsp 

   882             have eq_lsp: "lsp (cp s) rest = (l, [th'], r)" 

   883               apply simp

   884               by (drule_tac lsp_mid_length, simp)

   885             from eq_wq and eq_lsp

   886             have eq_D: "?D = {(Cs cs, Th th')}" by auto

   887             from eq_wq and eq_lsp

   888             have eq_C: "?C = {(Th th', Cs cs)}" by auto

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

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

   891             proof

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

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

   894               from tranclD [OF this]

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

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

   897               from depend_target_th [OF this]

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

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

   900               hence wt_th': "waiting s th' cs'"

   901                 unfolding s_depend_def s_waiting_def cs_waiting_def by simp

   902               hence "cs' = cs"

   903               proof(rule waiting_unique [OF vt])

   904                 from eq_wq eq_lsp wq_distinct[OF vt, of cs]

   905                 show "waiting s th' cs" by(unfold s_waiting_def, auto dest:lsp_set_eq)

   906               qed

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

   908               with eq_C show "False" by simp

   909             qed

   910             with acyclic_insert[symmetric] and ac and eq_D

   911             and eq_de show ?thesis by simp

   912           qed 

   913         qed

   914       qed

   915     next

   916       case (P th cs)

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

   918       from step_depend_p [OF this] P

   919       have "depend (e # s) = 

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

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

   922         by simp

   923       moreover have "acyclic ?R"

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

   925         case True

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

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

   928         proof

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

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

   931           from tranclD2 [OF this]

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

   933           with True show False by (auto simp:s_depend_def cs_waiting_def)

   934         qed

   935         with acyclic_insert ih eq_r show ?thesis by auto

   936       next

   937         case False

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

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

   940         proof

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

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

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

   944           ultimately show False

   945           proof -

   946             show " \<lbrakk>(Cs cs, Th th) \<in> (depend s)\<^sup>+; step s (P th cs)\<rbrakk> \<Longrightarrow> False"

   947               by (ind_cases "step s (P th cs)", simp)

   948           qed

   949         qed

   950         with acyclic_insert ih eq_r show ?thesis by auto

   951       qed

   952       ultimately show ?thesis by simp

   953     next

   954       case (Set thread prio)

   955       with ih

   956       thm depend_set_unchanged

   957       show ?thesis by (simp add:depend_set_unchanged)

   958     qed

   959   next

   960     case vt_nil

   961     show "acyclic (depend ([]::state))"

   962       by (auto simp: s_depend_def cs_waiting_def 

   963                       cs_holding_def wq_def acyclic_def)

   964   qed

   965 qed

   966 

   967 lemma finite_depend: 

   968   fixes s

   969   assumes vt: "vt step s"

   970   shows "finite (depend s)"

   971 proof -

   972   from vt show ?thesis

   973   proof(induct)

   974     case (vt_cons s e)

   975     assume ih: "finite (depend s)"

   976       and stp: "step s e"

   977       and vt: "vt step s"

   978     show ?case

   979     proof(cases e)

   980       case (Create th prio)

   981       with ih

   982       show ?thesis by (simp add:depend_create_unchanged)

   983     next

   984       case (Exit th)

   985       with ih show ?thesis by (simp add:depend_exit_unchanged)

   986     next

   987       case (V th cs)

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

   989       from step_depend_v [OF this]

   990       have eq_de: "depend (e # s) = 

   991         depend s - {(Cs cs, Th th)} -

   992         {(Th th', Cs cs) |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))} \<union>

   993         {(Cs cs, Th th') |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))}"

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

   995       moreover from ih have ac: "finite (?A - ?B - ?C)" by simp

   996       moreover have "finite ?D"

   997       proof -

   998         have "?D = {} \<or> (\<exists> a. ?D = {a})" by (rule simple_A, auto)

   999         thus ?thesis

  1000         proof

  1001           assume h: "?D = {}"

  1002           show ?thesis by (unfold h, simp)

  1003         next

  1004           assume "\<exists> a. ?D = {a}"

  1005           thus ?thesis by auto

  1006         qed

  1007       qed

  1008       ultimately show ?thesis by simp

  1009     next

  1010       case (P th cs)

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

  1012       from step_depend_p [OF this] P

  1013       have "depend (e # s) = 

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

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

  1016         by simp

  1017       moreover have "finite ?R"

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

  1019         case True

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

  1021         with True and ih show ?thesis by auto

  1022       next

  1023         case False

  1024         hence "?R = depend s \<union> {(Th th, Cs cs)}" by simp

  1025         with False and ih show ?thesis by auto

  1026       qed

  1027       ultimately show ?thesis by auto

  1028     next

  1029       case (Set thread prio)

  1030       with ih

  1031       show ?thesis by (simp add:depend_set_unchanged)

  1032     qed

  1033   next

  1034     case vt_nil

  1035     show "finite (depend ([]::state))"

  1036       by (auto simp: s_depend_def cs_waiting_def 

  1037                    cs_holding_def wq_def acyclic_def)

  1038   qed

  1039 qed

  1040 

  1041 text {* Several useful lemmas *}

  1042 

  1043 thm wf_trancl

  1044 thm finite_acyclic_wf

  1045 thm finite_acyclic_wf_converse

  1046 thm wf_induct

  1047 

  1048 

  1049 lemma wf_dep_converse: 

  1050   fixes s

  1051   assumes vt: "vt step s"

  1052   shows "wf ((depend s)^-1)"

  1053 proof(rule finite_acyclic_wf_converse)

  1054   from finite_depend [OF vt]

  1055   show "finite (depend s)" .

  1056 next

  1057   from acyclic_depend[OF vt]

  1058   show "acyclic (depend s)" .

  1059 qed

  1060 

  1061 lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"

  1062 by (induct l, auto)

  1063 

  1064 lemma th_chasing: "(Th th, Cs cs) \<in> depend (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> depend s"

  1065   by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)

  1066 

  1067 lemma wq_threads: 

  1068   fixes s cs

  1069   assumes vt: "vt step s"

  1070   and h: "th \<in> set (wq s cs)"

  1071   shows "th \<in> threads s"

  1072 proof -

  1073  from vt and h show ?thesis

  1074   proof(induct arbitrary: th cs)

  1075     case (vt_cons s e)

  1076     assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"

  1077       and stp: "step s e"

  1078       and vt: "vt step s"

  1079       and h: "th \<in> set (wq (e # s) cs)"

  1080     show ?case

  1081     proof(cases e)

  1082       case (Create th' prio)

  1083       with ih h show ?thesis

  1084         by (auto simp:wq_def Let_def)

  1085     next

  1086       case (Exit th')

  1087       with stp ih h show ?thesis

  1088         apply (auto simp:wq_def Let_def)

  1089         apply (ind_cases "step s (Exit th')")

  1090         apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def

  1091                s_depend_def s_holding_def cs_holding_def)

  1092         by (fold wq_def, auto)

  1093     next

  1094       case (V th' cs')

  1095       show ?thesis

  1096       proof(cases "cs' = cs")

  1097         case False

  1098         with h

  1099         show ?thesis

  1100           apply(unfold wq_def V, auto simp:Let_def V split:prod.splits, fold wq_def)

  1101           by (drule_tac ih, simp)

  1102       next

  1103         case True

  1104         from h

  1105         show ?thesis

  1106         proof(unfold V wq_def)

  1107           assume th_in: "th \<in> set (waiting_queue (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")

  1108           show "th \<in> threads (V th' cs' # s)"

  1109           proof(cases "cs = cs'")

  1110             case False

  1111             hence "?l = waiting_queue (schs s) cs" by (simp add:Let_def)

  1112             with th_in have " th \<in> set (wq s cs)" 

  1113               by (fold wq_def, simp)

  1114             from ih [OF this] show ?thesis by simp

  1115           next

  1116             case True

  1117             show ?thesis

  1118             proof(cases "waiting_queue (schs s) cs'")

  1119               case Nil

  1120               with h V show ?thesis

  1121                 apply (auto simp:wq_def Let_def split:if_splits)

  1122                 by (fold wq_def, drule_tac ih, simp)

  1123             next

  1124               case (Cons a rest)

  1125               assume eq_wq: "waiting_queue (schs s) cs' = a # rest"

  1126               with h V show ?thesis

  1127               proof(cases "(lsp (cur_preced (schs s)) rest)", unfold V)

  1128                 fix l m r

  1129                 assume eq_lsp: "lsp (cur_preced (schs s)) rest = (l, m, r)"

  1130                   and eq_wq: "waiting_queue (schs s) cs' = a # rest"

  1131                   and th_in_set: "th \<in> set (wq (V th' cs' # s) cs)"

  1132                 show ?thesis

  1133                 proof(cases "m")

  1134                   case Nil

  1135                   with eq_lsp have "rest = []" using lsp_mid_nil by auto