1 theory ExtS

     2 imports Prio

     3 begin

     4 

     5 locale highest_set =

     6   fixes s' th prio fixes s 

     7   defines s_def : "s \<equiv> (Set th prio#s')"

     8   assumes vt_s: "vt step s"

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

    10 

    11 context highest_set

    12 begin

    13 

    14 

    15 lemma vt_s': "vt step s'"

    16   by (insert vt_s, unfold s_def, drule_tac step_back_vt, simp)

    17 

    18 lemma step_set: "step s' (Set th prio)"

    19   by (insert vt_s, unfold s_def, drule_tac step_back_step, simp)

    20 

    21 lemma step_set_elim: 

    22   "\<lbrakk>\<lbrakk>th \<in> runing s'\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"

    23   by (insert step_set, ind_cases "step s' (Set th prio)", auto)

    24 

    25 

    26 lemma threads_s: "th \<in> threads s"

    27   by (rule step_set_elim, unfold runing_def readys_def, auto simp:s_def)

    28 

    29 lemma same_depend: "depend s = depend s'"

    30   by (insert depend_set_unchanged, unfold s_def, simp)

    31 

    32 lemma same_dependents:

    33   "dependents (wq s) th = dependents (wq s') th"

    34   apply (unfold cs_dependents_def)

    35   by (unfold eq_depend same_depend, simp)

    36 

    37 lemma eq_cp_s_th: "cp s th = preced th s"

    38 proof -

    39   from highest and max_cp_eq[OF vt_s]

    40   have is_max: "preced th s = Max ((\<lambda>th. preced th s) ` threads s)" by simp

    41   have sbs: "({th} \<union> dependents (wq s) th) \<subseteq> threads s"

    42   proof -

    43     from threads_s and dependents_threads[OF vt_s, of th]

    44     show ?thesis by auto

    45   qed

    46   show ?thesis

    47   proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)

    48     show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)" by simp

    49   next

    50     fix y 

    51     assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)"

    52     then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependents (wq s) th)"

    53       and eq_y: "y = preced th1 s" by auto

    54     show "y \<le> preced th s"

    55     proof(unfold is_max, rule Max_ge)

    56       from finite_threads[OF vt_s] 

    57       show "finite ((\<lambda>th. preced th s) ` threads s)" by simp

    58     next

    59       from sbs th1_in and eq_y 

    60       show "y \<in> (\<lambda>th. preced th s) ` threads s" by auto

    61     qed

    62   next

    63     from sbs and finite_threads[OF vt_s]

    64     show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))"

    65       by (auto intro:finite_subset)

    66   qed

    67 qed

    68 

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

    70   by (fold max_cp_eq[OF vt_s], unfold eq_cp_s_th, insert highest, simp)

    71 

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

    73   by (fold eq_cp_s_th, unfold highest_cp_preced, simp)

    74 

    75 lemma is_ready: "th \<in> readys s"

    76 proof -

    77   have "\<forall>cs. \<not> waiting s th cs"

    78     apply (rule step_set_elim, unfold s_def, insert depend_set_unchanged[of th prio s'])

    79     apply (unfold s_depend_def, unfold runing_def readys_def)

    80     apply (auto, fold s_def)

    81     apply (erule_tac x = cs in allE, auto simp:waiting_eq)

    82   proof -

    83     fix cs

    84     assume h: 

    85       "{(Th t, Cs c) |t c. waiting (wq s) t c} \<union> {(Cs c, Th t) |c t. holding (wq s) t c} =

    86           {(Th t, Cs c) |t c. waiting (wq s') t c} \<union> {(Cs c, Th t) |c t. holding (wq s') t c}"

    87             (is "?L = ?R")

    88     and wt: "waiting (wq s) th cs" and nwt: "\<not> waiting (wq s') th cs"

    89     from wt have "(Th th, Cs cs) \<in> ?L" by auto

    90     with h have "(Th th, Cs cs) \<in> ?R" by simp

    91     hence "waiting (wq s') th cs" by auto with nwt

    92     show False by auto

    93   qed    

    94   with threads_s show ?thesis 

    95     by (unfold readys_def, auto)

    96 qed

    97 

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

    99 proof -

   100   from highest_cp_preced max_cp_eq[OF vt_s, symmetric]

   101   show ?thesis by simp

   102 qed

   103 

   104 lemma is_runing: "th \<in> runing s"

   105 proof -

   106   have "Max (cp s ` threads s) = Max (cp s ` readys s)"

   107   proof -

   108     have " Max (cp s ` readys s) = cp s th"

   109     proof(rule Max_eqI)

   110       from finite_threads[OF vt_s] readys_threads finite_subset

   111       have "finite (readys s)" by blast

   112       thus "finite (cp s ` readys s)" by auto

   113     next

   114       from is_ready show "cp s th \<in> cp s ` readys s" by auto

   115     next

   116       fix y

   117       assume "y \<in> cp s ` readys s"

   118       then obtain th1 where 

   119         eq_y: "y = cp s th1" and th1_in: "th1 \<in> readys s" by auto

   120       show  "y \<le> cp s th" 

   121       proof -

   122         have "y \<le> Max (cp s ` threads s)"

   123         proof(rule Max_ge)

   124           from eq_y and th1_in

   125           show "y \<in> cp s ` threads s"

   126             by (auto simp:readys_def)

   127         next

   128           from finite_threads[OF vt_s]

   129           show "finite (cp s ` threads s)" by auto

   130         qed

   131         with highest' show ?thesis by auto

   132       qed

   133     qed

   134     with highest' show ?thesis by auto

   135   qed

   136   thus ?thesis

   137     by (unfold runing_def, insert highest' is_ready, auto)

   138 qed

   139 

   140 end

   141 

   142 locale extend_highest_set = highest_set + 

   143   fixes t 

   144   assumes vt_t: "vt step (t@s)"

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

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

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

   148 

   149 lemma step_back_vt_app: 

   150   assumes vt_ts: "vt cs (t@s)" 

   151   shows "vt cs s"

   152 proof -

   153   from vt_ts show ?thesis

   154   proof(induct t)

   155     case Nil

   156     from Nil show ?case by auto

   157   next

   158     case (Cons e t)

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

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

   161     show ?case

   162     proof(rule ih)

   163       show "vt cs (t @ s)"

   164       proof(rule step_back_vt)

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

   166       qed

   167     qed

   168   qed

   169 qed

   170 

   171 context extend_highest_set

   172 begin

   173 

   174 lemma red_moment:

   175   "extend_highest_set s' th prio (moment i t)"

   176   apply (insert extend_highest_set_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])

   177   apply (unfold extend_highest_set_def extend_highest_set_axioms_def, clarsimp)

   178   by (unfold highest_set_def, auto dest:step_back_vt_app)

   179 

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

   181   assumes 

   182     h0: "R []"

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

   184                     extend_highest_set s' th prio t; 

   185                     extend_highest_set s' th prio (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"

   186   shows "R t"

   187 proof -

   188   from vt_t extend_highest_set_axioms show ?thesis

   189   proof(induct t)

   190     from h0 show "R []" .

   191   next

   192     case (Cons e t')

   193     assume ih: "\<lbrakk>vt step (t' @ s); extend_highest_set s' th prio t'\<rbrakk> \<Longrightarrow> R t'"

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

   195       and et: "extend_highest_set s' th prio (e # t')"

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

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

   198     show ?case

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

   200       show "R t'"

   201       proof(rule ih)

   202         from et show ext': "extend_highest_set s' th prio t'"

   203           by (unfold extend_highest_set_def extend_highest_set_axioms_def, auto dest:step_back_vt)

   204       next

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

   206       qed

   207     next

   208       from et show "extend_highest_set s' th prio (e # t')" .

   209     next

   210       from et show ext': "extend_highest_set s' th prio t'"

   211           by (unfold extend_highest_set_def extend_highest_set_axioms_def, auto dest:step_back_vt)

   212     qed

   213   qed

   214 qed

   215 

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

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

   218 proof -

   219   show ?thesis

   220   proof(induct rule:ind)

   221     case Nil

   222     from threads_s

   223     show "th \<in> threads ([] @ s) \<and> preced th ([] @ s) = preced th s"

   224       by auto

   225   next

   226     case (Cons e t)

   227     show ?case

   228     proof(cases e)

   229       case (Create thread prio)

   230       assume eq_e: " e = Create thread prio"

   231       show ?thesis

   232       proof -

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

   234         hence "th \<noteq> thread"

   235         proof(cases)

   236           assume "thread \<notin> threads (t @ s)"

   237           with Cons show ?thesis by auto

   238         qed

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

   240           by (unfold eq_e, auto simp:preced_def)

   241         moreover note Cons

   242         ultimately show ?thesis

   243           by (auto simp:eq_e)

   244       qed

   245     next

   246       case (Exit thread)

   247       assume eq_e: "e = Exit thread"

   248       from Cons have "extend_highest_set s' th prio (e # t)" by auto

   249       from extend_highest_set.exit_diff [OF this] and eq_e

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

   251       with Cons

   252       show ?thesis

   253         by (unfold eq_e, auto simp:preced_def)

   254     next

   255       case (P thread cs)

   256       assume eq_e: "e = P thread cs"

   257       with Cons

   258       show ?thesis 

   259         by (auto simp:eq_e preced_def)

   260     next

   261       case (V thread cs)

   262       assume eq_e: "e = V thread cs"

   263       with Cons

   264       show ?thesis 

   265         by (auto simp:eq_e preced_def)

   266     next

   267       case (Set thread prio')

   268       assume eq_e: " e = Set thread prio'"

   269       show ?thesis

   270       proof -

   271         from Cons have "extend_highest_set s' th prio (e # t)" by auto

   272         from extend_highest_set.set_diff_low[OF this] and eq_e

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

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

   275           by (unfold eq_e, auto simp:preced_def)

   276         moreover note Cons

   277         ultimately show ?thesis

   278           by (auto simp:eq_e)

   279       qed

   280     qed

   281   qed

   282 qed

   283 

   284 lemma max_kept: "Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s))) = preced th s"

   285 proof(induct rule:ind)

   286   case Nil

   287   from highest_preced_thread

   288   show "Max ((\<lambda>th'. preced th' ([] @ s)) ` threads ([] @ s)) = preced th s"

   289     by simp

   290 next

   291   case (Cons e t)

   292   show ?case

   293   proof(cases e)

   294     case (Create thread prio')

   295     assume eq_e: " e = Create thread prio'"

   296     from Cons and eq_e have stp: "step (t@s) (Create thread prio')" by auto

   297     hence neq_thread: "thread \<noteq> th"

   298     proof(cases)

   299       assume "thread \<notin> threads (t @ s)"

   300       moreover have "th \<in> threads (t@s)"

   301       proof -

   302         from Cons have "extend_highest_set s' th prio t" by auto

   303         from extend_highest_set.th_kept[OF this] show ?thesis by (simp add:s_def)

   304       qed

   305       ultimately show ?thesis by auto

   306     qed

   307     from Cons have "extend_highest_set s' th prio t" by auto

   308     from extend_highest_set.th_kept[OF this]

   309     have h': " th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" 

   310       by (auto simp:s_def)

   311     from stp

   312     have thread_ts: "thread \<notin> threads (t @ s)"

   313       by (cases, auto)

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

   315     proof -

   316       have "Max (?f ` ?A) = Max(insert (?f thread) (?f ` (threads (t@s))))"

   317         by (unfold eq_e, simp)

   318       moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))"

   319       proof(rule Max_insert)

   320         from Cons have "vt step (t @ s)" by auto

   321         from finite_threads[OF this]

   322         show "finite (?f ` (threads (t@s)))" by simp

   323       next

   324         from h' show "(?f ` (threads (t@s))) \<noteq> {}" by auto

   325       qed

   326       moreover have "(Max (?f ` (threads (t@s)))) = ?t"

   327       proof -

   328         have "(\<lambda>th'. preced th' ((e # t) @ s)) ` threads (t @ s) = 

   329           (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" (is "?f1 ` ?B = ?f2 ` ?B")

   330         proof -

   331           { fix th' 

   332             assume "th' \<in> ?B"

   333             with thread_ts eq_e

   334             have "?f1 th' = ?f2 th'" by (auto simp:preced_def)

   335           } thus ?thesis 

   336             apply (auto simp:Image_def)

   337           proof -

   338             fix th'

   339             assume h: "\<And>th'. th' \<in> threads (t @ s) \<Longrightarrow> 

   340               preced th' (e # t @ s) = preced th' (t @ s)"

   341               and h1: "th' \<in> threads (t @ s)"

   342             show "preced th' (t @ s) \<in> (\<lambda>th'. preced th' (e # t @ s)) ` threads (t @ s)"

   343             proof -

   344               from h1 have "?f1 th' \<in> ?f1 ` ?B" by auto

   345               moreover from h[OF h1] have "?f1 th' = ?f2 th'" by simp

   346               ultimately show ?thesis by simp

   347             qed

   348           qed

   349         qed

   350         with Cons show ?thesis by auto

   351       qed

   352       moreover have "?f thread < ?t"

   353       proof -

   354         from Cons have " extend_highest_set s' th prio (e # t)" by auto

   355         from extend_highest_set.create_low[OF this] and eq_e

   356         have "prio' \<le> prio" by auto

   357         thus ?thesis

   358         by (unfold eq_e, auto simp:preced_def s_def precedence_less_def)

   359     qed

   360     ultimately show ?thesis by (auto simp:max_def)

   361   qed

   362 next

   363     case (Exit thread)

   364     assume eq_e: "e = Exit thread"

   365     from Cons have vt_e: "vt step (e#(t @ s))" by auto

   366     from Cons and eq_e have stp: "step (t@s) (Exit thread)" by auto

   367     from stp have thread_ts: "thread \<in> threads (t @ s)"

   368       by(cases, unfold runing_def readys_def, auto)

   369     from Cons have "extend_highest_set s' th prio (e # t)" by auto

   370     from extend_highest_set.exit_diff[OF this] and eq_e

   371     have neq_thread: "thread \<noteq> th" by auto

   372     from Cons have "extend_highest_set s' th prio t" by auto

   373     from extend_highest_set.th_kept[OF this, folded s_def]

   374     have h': "th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" .

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

   376     proof -

   377       have "threads (t@s) = insert thread ?A"

   378         by (insert stp thread_ts, unfold eq_e, auto)

   379       hence "Max (?f ` (threads (t@s))) = Max (?f ` \<dots>)" by simp

   380       also from this have "\<dots> = Max (insert (?f thread) (?f ` ?A))" by simp

   381       also have "\<dots> = max (?f thread) (Max (?f ` ?A))"

   382       proof(rule Max_insert)

   383         from finite_threads [OF vt_e]

   384         show "finite (?f ` ?A)" by simp

   385       next

   386         from Cons have "extend_highest_set s' th prio (e # t)" by auto

   387         from extend_highest_set.th_kept[OF this]

   388         show "?f ` ?A \<noteq> {}" by  (auto simp:s_def)

   389       qed

   390       finally have "Max (?f ` (threads (t@s))) = max (?f thread) (Max (?f ` ?A))" .

   391       moreover have "Max (?f ` (threads (t@s))) = ?t"

   392       proof -

   393         from Cons show ?thesis

   394           by (unfold eq_e, auto simp:preced_def)

   395       qed

   396       ultimately have "max (?f thread) (Max (?f ` ?A)) = ?t" by simp

   397       moreover have "?f thread < ?t"

   398       proof(unfold eq_e, simp add:preced_def, fold preced_def)

   399         show "preced thread (t @ s) < ?t"

   400         proof -

   401           have "preced thread (t @ s) \<le> ?t" 

   402           proof -

   403             from Cons

   404             have "?t = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" 

   405               (is "?t = Max (?g ` ?B)") by simp

   406             moreover have "?g thread \<le> \<dots>"

   407             proof(rule Max_ge)

   408               have "vt step (t@s)" by fact

   409               from finite_threads [OF this]

   410               show "finite (?g ` ?B)" by simp

   411             next

   412               from thread_ts

   413               show "?g thread \<in> (?g ` ?B)" by auto

   414             qed

   415             ultimately show ?thesis by auto

   416           qed

   417           moreover have "preced thread (t @ s) \<noteq> ?t"

   418           proof

   419             assume "preced thread (t @ s) = preced th s"

   420             with h' have "preced thread (t @ s) = preced th (t@s)" by simp

   421             from preced_unique [OF this] have "thread = th"

   422             proof

   423               from h' show "th \<in> threads (t @ s)" by simp

   424             next

   425               from thread_ts show "thread \<in> threads (t @ s)" .

   426             qed(simp)

   427             with neq_thread show "False" by simp

   428           qed

   429           ultimately show ?thesis by auto

   430         qed

   431       qed

   432       ultimately show ?thesis 

   433         by (auto simp:max_def split:if_splits)

   434     qed

   435   next

   436     case (P thread cs)

   437     with Cons

   438     show ?thesis by (auto simp:preced_def)

   439   next

   440     case (V thread cs)

   441     with Cons

   442     show ?thesis by (auto simp:preced_def)

   443   next

   444     case (Set thread prio')

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

   446     proof -

   447       let ?B = "threads (t@s)"

   448       from Cons have "extend_highest_set s' th prio (e # t)" by auto

   449       from extend_highest_set.set_diff_low[OF this] and Set

   450       have neq_thread: "thread \<noteq> th" and le_p: "prio' \<le> prio" by auto

   451       from Set have "Max (?f ` ?A) = Max (?f ` ?B)" by simp

   452       also have "\<dots> = ?t"

   453       proof(rule Max_eqI)

   454         fix y

   455         assume y_in: "y \<in> ?f ` ?B"

   456         then obtain th1 where 

   457           th1_in: "th1 \<in> ?B" and eq_y: "y = ?f th1" by auto

   458         show "y \<le> ?t"

   459         proof(cases "th1 = thread")

   460           case True

   461           with neq_thread le_p eq_y s_def Set

   462           show ?thesis

   463             by (auto simp:preced_def precedence_le_def)

   464         next

   465           case False

   466           with Set eq_y

   467           have "y  = preced th1 (t@s)"

   468             by (simp add:preced_def)

   469           moreover have "\<dots> \<le> ?t"

   470           proof -

   471             from Cons

   472             have "?t = Max ((\<lambda> th'. preced th' (t@s)) ` (threads (t@s)))"

   473               by auto

   474             moreover have "preced th1 (t@s) \<le> \<dots>"

   475             proof(rule Max_ge)

   476               from th1_in 

   477               show "preced th1 (t @ s) \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)"

   478                 by simp

   479             next

   480               show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"

   481               proof -

   482                 from Cons have "vt step (t @ s)" by auto

   483                 from finite_threads[OF this] show ?thesis by auto

   484               qed

   485             qed

   486             ultimately show ?thesis by auto

   487           qed

   488           ultimately show ?thesis by auto

   489         qed

   490       next

   491         from Cons and finite_threads

   492         show "finite (?f ` ?B)" by auto

   493       next

   494         from Cons have "extend_highest_set s' th prio t" by auto

   495         from extend_highest_set.th_kept [OF this, folded s_def]

   496         have h: "th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" .

   497         show "?t \<in> (?f ` ?B)" 

   498         proof -

   499           from neq_thread Set h

   500           have "?t = ?f th" by (auto simp:preced_def)

   501           with h show ?thesis by auto

   502         qed

   503       qed

   504       finally show ?thesis .

   505     qed

   506   qed

   507 qed

   508 

   509 lemma max_preced: "preced th (t@s) = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))"

   510   by (insert th_kept max_kept, auto)

   511 

   512 lemma th_cp_max_preced: "cp (t@s) th = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))" 

   513   (is "?L = ?R")

   514 proof -

   515   have "?L = cpreced (t@s) (wq (t@s)) th" 

   516     by (unfold cp_eq_cpreced, simp)

   517   also have "\<dots> = ?R"

   518   proof(unfold cpreced_def)

   519     show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependents (wq (t @ s)) th)) =

   520           Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"

   521       (is "Max (?f ` ({th} \<union> ?A)) = Max (?f ` ?B)")

   522     proof(cases "?A = {}")

   523       case False

   524       have "Max (?f ` ({th} \<union> ?A)) = Max (insert (?f th) (?f ` ?A))" by simp

   525       moreover have "\<dots> = max (?f th) (Max (?f ` ?A))"

   526       proof(rule Max_insert)

   527         show "finite (?f ` ?A)"

   528         proof -

   529           from dependents_threads[OF vt_t]

   530           have "?A \<subseteq> threads (t@s)" .

   531           moreover from finite_threads[OF vt_t] have "finite \<dots>" .

   532           ultimately show ?thesis 

   533             by (auto simp:finite_subset)

   534         qed

   535       next

   536         from False show "(?f ` ?A) \<noteq> {}" by simp

   537       qed

   538       moreover have "\<dots> = Max (?f ` ?B)"

   539       proof -

   540         from max_preced have "?f th = Max (?f ` ?B)" .

   541         moreover have "Max (?f ` ?A) \<le> \<dots>" 

   542         proof(rule Max_mono)

   543           from False show "(?f ` ?A) \<noteq> {}" by simp

   544         next

   545           show "?f ` ?A \<subseteq> ?f ` ?B" 

   546           proof -

   547             have "?A \<subseteq> ?B" by (rule dependents_threads[OF vt_t])

   548             thus ?thesis by auto

   549           qed

   550         next

   551           from finite_threads[OF vt_t] 

   552           show "finite (?f ` ?B)" by simp

   553         qed

   554         ultimately show ?thesis

   555           by (auto simp:max_def)

   556       qed

   557       ultimately show ?thesis by auto

   558     next

   559       case True

   560       with max_preced show ?thesis by auto

   561     qed

   562   qed

   563   finally show ?thesis .

   564 qed

   565 

   566 lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))"

   567   by (unfold max_cp_eq[OF vt_t] th_cp_max_preced, simp)

   568 

   569 lemma th_cp_preced: "cp (t@s) th = preced th s"

   570   by (fold max_kept, unfold th_cp_max_preced, simp)

   571 

   572 lemma preced_less':

   573   fixes th'

   574   assumes th'_in: "th' \<in> threads s"

   575   and neq_th': "th' \<noteq> th"

   576   shows "preced th' s < preced th s"

   577 proof -

   578   have "preced th' s \<le> Max ((\<lambda>th'. preced th' s) ` threads s)"

   579   proof(rule Max_ge)

   580     from finite_threads [OF vt_s]

   581     show "finite ((\<lambda>th'. preced th' s) ` threads s)" by simp

   582   next

   583     from th'_in show "preced th' s \<in> (\<lambda>th'. preced th' s) ` threads s"

   584       by simp

   585   qed

   586   moreover have "preced th' s \<noteq> preced th s"

   587   proof

   588     assume "preced th' s = preced th s"

   589     from preced_unique[OF this th'_in] neq_th' is_ready

   590     show "False" by  (auto simp:readys_def)

   591   qed

   592   ultimately show ?thesis using highest_preced_thread

   593     by auto

   594 qed

   595 

   596 lemma pv_blocked:

   597   fixes th'

   598   assumes th'_in: "th' \<in> threads (t@s)"

   599   and neq_th': "th' \<noteq> th"

   600   and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"

   601   shows "th' \<notin> runing (t@s)"

   602 proof

   603   assume "th' \<in> runing (t@s)"

   604   hence "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" 

   605     by (auto simp:runing_def)

   606   with max_cp_readys_threads [OF vt_t]

   607   have "cp (t @ s) th' = Max (cp (t@s) ` threads (t@s))"

   608     by auto

   609   moreover from th_cp_max have "cp (t @ s) th = \<dots>" by simp

   610   ultimately have "cp (t @ s) th' = cp (t @ s) th" by simp

   611   moreover from th_cp_preced and th_kept have "\<dots> = preced th (t @ s)"

   612     by simp

   613   finally have h: "cp (t @ s) th' = preced th (t @ s)" .

   614   show False

   615   proof -

   616     have "dependents (wq (t @ s)) th' = {}" 

   617       by (rule count_eq_dependents [OF vt_t eq_pv])

   618     moreover have "preced th' (t @ s) \<noteq> preced th (t @ s)"

   619     proof

   620       assume "preced th' (t @ s) = preced th (t @ s)"

   621       hence "th' = th"

   622       proof(rule preced_unique)

   623         from th_kept show "th \<in> threads (t @ s)" by simp

   624       next

   625         from th'_in show "th' \<in> threads (t @ s)" by simp

   626       qed

   627       with assms show False by simp

   628     qed

   629     ultimately show ?thesis

   630       by (insert h, unfold cp_eq_cpreced cpreced_def, simp)

   631   qed

   632 qed

   633 

   634 lemma runing_precond_pre:

   635   fixes th'

   636   assumes th'_in: "th' \<in> threads s"

   637   and eq_pv: "cntP s th' = cntV s th'"

   638   and neq_th': "th' \<noteq> th"

   639   shows "th' \<in> threads (t@s) \<and>

   640          cntP (t@s) th' = cntV (t@s) th'"

   641 proof -

   642   show ?thesis

   643   proof(induct rule:ind)

   644     case (Cons e t)

   645     from Cons

   646     have in_thread: "th' \<in> threads (t @ s)"

   647       and not_holding: "cntP (t @ s) th' = cntV (t @ s) th'" by auto

   648     have "extend_highest_set s' th prio t" by fact

   649     from extend_highest_set.pv_blocked 

   650     [OF this, folded s_def, OF in_thread neq_th' not_holding]

   651     have not_runing: "th' \<notin> runing (t @ s)" .

   652     show ?case

   653     proof(cases e)

   654       case (V thread cs)

   655       from Cons and V have vt_v: "vt step (V thread cs#(t@s))" by auto

   656 

   657       show ?thesis

   658       proof -

   659         from Cons and V have "step (t@s) (V thread cs)" by auto

   660         hence neq_th': "thread \<noteq> th'"

   661         proof(cases)

   662           assume "thread \<in> runing (t@s)"

   663           moreover have "th' \<notin> runing (t@s)" by fact

   664           ultimately show ?thesis by auto

   665         qed

   666         with not_holding have cnt_eq: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" 

   667           by (unfold V, simp add:cntP_def cntV_def count_def)

   668         moreover from in_thread

   669         have in_thread': "th' \<in> threads ((e # t) @ s)" by (unfold V, simp)

   670         ultimately show ?thesis by auto

   671       qed

   672     next

   673       case (P thread cs)

   674       from Cons and P have "step (t@s) (P thread cs)" by auto

   675       hence neq_th': "thread \<noteq> th'"

   676       proof(cases)

   677         assume "thread \<in> runing (t@s)"

   678         moreover note not_runing

   679         ultimately show ?thesis by auto

   680       qed

   681       with Cons and P have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"

   682         by (auto simp:cntP_def cntV_def count_def)

   683       moreover from Cons and P have in_thread': "th' \<in> threads ((e # t) @ s)"

   684         by auto

   685       ultimately show ?thesis by auto

   686     next

   687       case (Create thread prio')

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

   689       hence neq_th': "thread \<noteq> th'"

   690       proof(cases)

   691         assume "thread \<notin> threads (t @ s)"

   692         moreover have "th' \<in> threads (t@s)" by fact

   693         ultimately show ?thesis by auto

   694       qed

   695       with Cons and Create 

   696       have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"

   697         by (auto simp:cntP_def cntV_def count_def)

   698       moreover from Cons and Create 

   699       have in_thread': "th' \<in> threads ((e # t) @ s)" by auto

   700       ultimately show ?thesis by auto

   701     next

   702       case (Exit thread)

   703       from Cons and Exit have "step (t@s) (Exit thread)" by auto

   704       hence neq_th': "thread \<noteq> th'"

   705       proof(cases)

   706         assume "thread \<in> runing (t @ s)"

   707         moreover note not_runing

   708         ultimately show ?thesis by auto

   709       qed

   710       with Cons and Exit 

   711       have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"

   712         by (auto simp:cntP_def cntV_def count_def)

   713       moreover from Cons and Exit and neq_th' 

   714       have in_thread': "th' \<in> threads ((e # t) @ s)"

   715         by auto

   716       ultimately show ?thesis by auto

   717     next

   718       case (Set thread prio')

   719       with Cons

   720       show ?thesis 

   721         by (auto simp:cntP_def cntV_def count_def)

   722     qed

   723   next

   724     case Nil

   725     with assms

   726     show ?case by auto

   727   qed

   728 qed

   729 

   730 (*

   731 lemma runing_precond:

   732   fixes th'

   733   assumes th'_in: "th' \<in> threads s"

   734   and eq_pv: "cntP s th' = cntV s th'"

   735   and neq_th': "th' \<noteq> th"

   736   shows "th' \<notin> runing (t@s)"

   737 proof -

   738   from runing_precond_pre[OF th'_in eq_pv neq_th']

   739   have h1: "th' \<in> threads (t @ s)"  and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto

   740   from pv_blocked[OF h1 neq_th' h2] 

   741   show ?thesis .

   742 qed

   743 *)

   744 

   745 lemma runing_precond:

   746   fixes th'

   747   assumes th'_in: "th' \<in> threads s"

   748   and neq_th': "th' \<noteq> th"

   749   and is_runing: "th' \<in> runing (t@s)"

   750   shows "cntP s th' > cntV s th'"

   751 proof -

   752   have "cntP s th' \<noteq> cntV s th'"

   753   proof

   754     assume eq_pv: "cntP s th' = cntV s th'"

   755     from runing_precond_pre[OF th'_in eq_pv neq_th']

   756     have h1: "th' \<in> threads (t @ s)"  

   757       and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto

   758     from pv_blocked[OF h1 neq_th' h2] have " th' \<notin> runing (t @ s)" .

   759     with is_runing show "False" by simp

   760   qed

   761   moreover from cnp_cnv_cncs[OF vt_s, of th'] 

   762   have "cntV s th' \<le> cntP s th'" by auto

   763   ultimately show ?thesis by auto

   764 qed

   765 

   766 lemma moment_blocked_pre:

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

   768   and th'_in: "th' \<in> threads ((moment i t)@s)"

   769   and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"

   770   shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \<and>

   771          th' \<in> threads ((moment (i+j) t)@s)"

   772 proof(induct j)

   773   case (Suc k)

   774   show ?case

   775   proof -

   776     { assume True: "Suc (i+k) \<le> length t"

   777       from moment_head [OF this] 

   778       obtain e where

   779         eq_me: "moment (Suc(i+k)) t = e#(moment (i+k) t)"

   780         by blast

   781       from red_moment[of "Suc(i+k)"]

   782       and eq_me have "extend_highest_set s' th prio (e # moment (i + k) t)" by simp

   783       hence vt_e: "vt step (e#(moment (i + k) t)@s)"

   784         by (unfold extend_highest_set_def extend_highest_set_axioms_def 

   785           highest_set_def s_def, auto)

   786       have not_runing': "th' \<notin>  runing (moment (i + k) t @ s)"

   787       proof(unfold s_def)

   788         show "th' \<notin> runing (moment (i + k) t @ Set th prio # s')"

   789         proof(rule extend_highest_set.pv_blocked)

   790           from Suc show "th' \<in> threads (moment (i + k) t @ Set th prio # s')"

   791             by (simp add:s_def)

   792         next

   793           from neq_th' show "th' \<noteq> th" .

   794         next

   795           from red_moment show "extend_highest_set s' th prio (moment (i + k) t)" .

   796         next

   797           from Suc show "cntP (moment (i + k) t @ Set th prio # s') th' =

   798             cntV (moment (i + k) t @ Set th prio # s') th'"

   799             by (auto simp:s_def)

   800         qed

   801       qed

   802       from step_back_step[OF vt_e]

   803       have "step ((moment (i + k) t)@s) e" .

   804       hence "cntP (e#(moment (i + k) t)@s) th' = cntV (e#(moment (i + k) t)@s) th' \<and>

   805         th' \<in> threads (e#(moment (i + k) t)@s)

   806         "

   807       proof(cases)

   808         case (thread_create thread prio)

   809         with Suc show ?thesis by (auto simp:cntP_def cntV_def count_def)

   810       next

   811         case (thread_exit thread)

   812         moreover have "thread \<noteq> th'"

   813         proof -

   814           have "thread \<in> runing (moment (i + k) t @ s)" by fact

   815           moreover note not_runing'

   816           ultimately show ?thesis by auto

   817         qed

   818         moreover note Suc 

   819         ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def)

   820       next

   821         case (thread_P thread cs)

   822         moreover have "thread \<noteq> th'"

   823         proof -

   824           have "thread \<in> runing (moment (i + k) t @ s)" by fact

   825           moreover note not_runing'

   826           ultimately show ?thesis by auto

   827         qed

   828         moreover note Suc 

   829         ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def)

   830       next

   831         case (thread_V thread cs)

   832         moreover have "thread \<noteq> th'"

   833         proof -

   834           have "thread \<in> runing (moment (i + k) t @ s)" by fact

   835           moreover note not_runing'

   836           ultimately show ?thesis by auto

   837         qed

   838         moreover note Suc 

   839         ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def)

   840       next

   841         case (thread_set thread prio')

   842         with Suc show ?thesis

   843           by (auto simp:cntP_def cntV_def count_def)

   844       qed

   845       with eq_me have ?thesis using eq_me by auto 

   846     } note h = this

   847     show ?thesis

   848     proof(cases "Suc (i+k) \<le> length t")

   849       case True

   850       from h [OF this] show ?thesis .

   851     next

   852       case False

   853       with moment_ge

   854       have eq_m: "moment (i + Suc k) t = moment (i+k) t" by auto

   855       with Suc show ?thesis by auto

   856     qed

   857   qed

   858 next

   859   case 0

   860   from assms show ?case by auto

   861 qed

   862 

   863 lemma moment_blocked:

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

   865   and th'_in: "th' \<in> threads ((moment i t)@s)"

   866   and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"

   867   and le_ij: "i \<le> j"

   868   shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and>

   869          th' \<in> threads ((moment j t)@s) \<and>

   870          th' \<notin> runing ((moment j t)@s)"

   871 proof -

   872   from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij

   873   have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'"

   874     and h2: "th' \<in> threads ((moment j t)@s)" by auto

   875   with extend_highest_set.pv_blocked [OF  red_moment [of j], folded s_def, OF h2 neq_th' h1]

   876   show ?thesis by auto

   877 qed

   878 

   879 lemma runing_inversion_1:

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

   881   and runing': "th' \<in> runing (t@s)"

   882   shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"

   883 proof(cases "th' \<in> threads s")

   884   case True

   885   with runing_precond [OF this neq_th' runing'] show ?thesis by simp

   886 next

   887   case False

   888   let ?Q = "\<lambda> t. th' \<in> threads (t@s)"

   889   let ?q = "moment 0 t"

   890   from moment_eq and False have not_thread: "\<not> ?Q ?q" by simp

   891   from runing' have "th' \<in> threads (t@s)" by (simp add:runing_def readys_def)

   892   from p_split_gen [of ?Q, OF this not_thread]

   893   obtain i where lt_its: "i < length t"

   894     and le_i: "0 \<le> i"

   895     and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre")

   896     and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by auto

   897   from lt_its have "Suc i \<le> length t" by auto

   898   from moment_head[OF this] obtain e where 

   899    eq_me: "moment (Suc i) t = e # moment i t" by blast

   900   from red_moment[of "Suc i"] and eq_me

   901   have "extend_highest_set s' th prio (e # moment i t)" by simp

   902   hence vt_e: "vt step (e#(moment i t)@s)"

   903     by (unfold extend_highest_set_def extend_highest_set_axioms_def 

   904       highest_set_def s_def, auto)

   905   from step_back_step[OF this] have stp_i: "step (moment i t @ s) e" .

   906   from post[rule_format, of "Suc i"] and eq_me 

   907   have not_in': "th' \<in> threads (e # moment i t@s)" by auto

   908   from create_pre[OF stp_i pre this] 

   909   obtain prio where eq_e: "e = Create th' prio" .

   910   have "cntP (moment i t@s) th' = cntV (moment i t@s) th'"

   911   proof(rule cnp_cnv_eq)

   912     from step_back_vt [OF vt_e] 

   913     show "vt step (moment i t @ s)" .

   914   next

   915     from eq_e and stp_i 

   916     have "step (moment i t @ s) (Create th' prio)" by simp

   917     thus "th' \<notin> threads (moment i t @ s)" by (cases, simp)

   918   qed

   919   with eq_e

   920   have "cntP ((e#moment i t)@s) th' = cntV ((e#moment i t)@s) th'" 

   921     by (simp add:cntP_def cntV_def count_def)

   922   with eq_me[symmetric]

   923   have h1: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'"

   924     by simp

   925   from eq_e have "th' \<in> threads ((e#moment i t)@s)" by simp

   926   with eq_me [symmetric]

   927   have h2: "th' \<in> threads (moment (Suc i) t @ s)" by simp

   928   from moment_blocked [OF neq_th' h2 h1, of "length t"] and lt_its

   929   and moment_ge

   930   have "th' \<notin> runing (t @ s)" by auto

   931   with runing'

   932   show ?thesis by auto

   933 qed

   934 

   935 lemma runing_inversion_2:

   936   assumes runing': "th' \<in> runing (t@s)"

   937   shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"

   938 proof -

   939   from runing_inversion_1[OF _ runing']

   940   show ?thesis by auto

   941 qed

   942 

   943 lemma live: "runing (t@s) \<noteq> {}"

   944 proof(cases "th \<in> runing (t@s)")

   945   case True thus ?thesis by auto

   946 next

   947   case False

   948   then have not_ready: "th \<notin> readys (t@s)"

   949     apply (unfold runing_def, 

   950             insert th_cp_max max_cp_readys_threads[OF vt_t, symmetric])

   951     by auto

   952   from th_kept have "th \<in> threads (t@s)" by auto

   953   from th_chain_to_ready[OF vt_t this] and not_ready

   954   obtain th' where th'_in: "th' \<in> readys (t@s)"

   955     and dp: "(Th th, Th th') \<in> (depend (t @ s))\<^sup>+" by auto

   956   have "th' \<in> runing (t@s)"

   957   proof -

   958     have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"

   959     proof -

   960       have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')) = 

   961                preced th (t@s)"

   962       proof(rule Max_eqI)

   963         fix y

   964         assume "y \<in> (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')"

   965         then obtain th1 where

   966           h1: "th1 = th' \<or> th1 \<in>  dependents (wq (t @ s)) th'"

   967           and eq_y: "y = preced th1 (t@s)" by auto

   968         show "y \<le> preced th (t @ s)"

   969         proof -

   970           from max_preced

   971           have "preced th (t @ s) = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" .

   972           moreover have "y \<le> \<dots>"

   973           proof(rule Max_ge)

   974             from h1

   975             have "th1 \<in> threads (t@s)"

   976             proof

   977               assume "th1 = th'"

   978               with th'_in show ?thesis by (simp add:readys_def)

   979             next

   980               assume "th1 \<in> dependents (wq (t @ s)) th'"

   981               with dependents_threads [OF vt_t]

   982               show "th1 \<in> threads (t @ s)" by auto

   983             qed

   984             with eq_y show " y \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" by simp

   985           next

   986             from finite_threads[OF vt_t]

   987             show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" by simp

   988           qed

   989           ultimately show ?thesis by auto

   990         qed

   991       next

   992         from finite_threads[OF vt_t] dependents_threads [OF vt_t, of th']

   993         show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th'))"

   994           by (auto intro:finite_subset)

   995       next

   996         from dp

   997         have "th \<in> dependents (wq (t @ s)) th'" 

   998           by (unfold cs_dependents_def, auto simp:eq_depend)

   999         thus "preced th (t @ s) \<in> 

  1000                 (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')"

  1001           by auto

  1002       qed

  1003       moreover have "\<dots> = Max (cp (t @ s) ` readys (t @ s))"

  1004       proof -

  1005         from max_preced and max_cp_eq[OF vt_t, symmetric]

  1006         have "preced th (t @ s) = Max (cp (t @ s) ` threads (t @ s))" by simp

  1007         with max_cp_readys_threads[OF vt_t] show ?thesis by simp

  1008       qed

  1009       ultimately show ?thesis by (unfold cp_eq_cpreced cpreced_def, simp)

  1010     qed

  1011     with th'_in show ?thesis by (auto simp:runing_def)

  1012   qed

  1013   thus ?thesis by auto

  1014 qed

  1015 

  1016 end

  1017 

  1018 end

  1019