1 theory Ext

     2 imports Prio

     3 begin

     4 

     5 locale highest_create =

     6   fixes s' th prio fixes s 

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

     8   assumes vt_s: "vt step s"

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

    10 

    11 context highest_create

    12 begin

    13 

    14 lemma threads_s: "threads s = threads s' \<union> {th}"

    15   by (unfold s_def, simp)

    16 

    17 lemma vt_s': "vt step s'"

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

    19 

    20 lemma step_create: "step s' (Create th prio)"

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

    22 

    23 lemma step_create_elim: 

    24   "\<lbrakk>\<And>max_prio. \<lbrakk>prio \<le> max_prio; th \<notin> threads s'\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"

    25   by (insert step_create, ind_cases "step s' (Create th prio)", auto)

    26 

    27 lemma eq_cp_s: 

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

    29   shows "cp s th' = cp s' th'"

    30 proof(unfold cp_eq_cpreced cpreced_def cs_dependents_def s_def 

    31     eq_depend depend_create_unchanged)

    32   show "Max ((\<lambda>tha. preced tha (Create th prio # s')) `

    33          ({th'} \<union> {th'a. (Th th'a, Th th') \<in> (depend s')\<^sup>+})) =

    34         Max ((\<lambda>th. preced th s') ` ({th'} \<union> {th'a. (Th th'a, Th th') \<in> (depend s')\<^sup>+}))"

    35     (is "Max (?f ` ?A) = Max (?g ` ?A)")

    36   proof -

    37     have "?f ` ?A = ?g ` ?A"

    38     proof(rule f_image_eq)

    39       fix a

    40       assume a_in: "a \<in> ?A"

    41       thus "?f a = ?g a" 

    42       proof -

    43         from a_in

    44         have "a = th' \<or> (Th a, Th th') \<in> (depend s')\<^sup>+" by auto 

    45         hence "a \<noteq> th"

    46         proof

    47           assume "a = th'"

    48           moreover have "th' \<noteq> th"

    49           proof(rule step_create_elim)

    50             assume th_not_in: "th \<notin> threads s'" with th'_in

    51             show ?thesis by auto

    52           qed

    53           ultimately show ?thesis by auto

    54         next

    55           assume "(Th a, Th th') \<in> (depend s')\<^sup>+"

    56           hence "Th a \<in> Domain \<dots>"

    57             by (auto simp:Domain_def)

    58           hence "Th a \<in> Domain (depend s')"

    59             by (simp add:trancl_domain)

    60           from dm_depend_threads[OF vt_s' this]

    61           have h: "a \<in> threads s'" .

    62           show ?thesis

    63           proof(rule step_create_elim)

    64             assume "th \<notin> threads s'" with h

    65             show ?thesis by auto

    66           qed

    67         qed

    68         thus ?thesis 

    69           by (unfold preced_def, auto)

    70       qed

    71     qed

    72     thus ?thesis by auto

    73   qed

    74 qed

    75 

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

    77   by (insert depend_create_unchanged, unfold s_def, simp)

    78 

    79 lemma same_dependents:

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

    81   apply (unfold cs_dependents_def)

    82   by (unfold eq_depend same_depend, simp)

    83 

    84 lemma nil_dependents_s': "dependents (wq s') th = {}"

    85 proof -

    86   { assume ne: "dependents (wq s') th \<noteq> {}"

    87     then obtain th' where "th' \<in>  dependents (wq s') th"

    88       by (unfold cs_dependents_def, auto)

    89     hence "(Th th', Th th) \<in> (depend (wq s'))^+"

    90       by (unfold cs_dependents_def, auto)

    91     hence "(Th th', Th th) \<in> (depend s')^+"

    92       by (simp add:eq_depend)

    93     hence "Th th \<in> Range ((depend s')^+)" by (auto simp:Range_def Domain_def)

    94     hence "Th th \<in> Range (depend s')" by (simp add:trancl_range)

    95     from range_in [OF vt_s' this]

    96     have h: "th \<in> threads s'" .

    97     have "False"

    98     proof(rule step_create_elim)

    99       assume "th \<notin> threads s'" with h show ?thesis by auto

   100     qed

   101   } thus ?thesis by auto

   102 qed

   103 

   104 lemma nil_dependents: "dependents (wq s) th = {}"

   105 proof -

   106   have "wq s' = wq s"

   107     by (unfold wq_def s_def, auto simp:Let_def)

   108   with nil_dependents_s' show ?thesis by auto

   109 qed

   110 

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

   112   by (unfold cp_eq_cpreced cpreced_def nil_dependents, auto)

   113 

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

   115   by (fold max_cp_eq[OF vt_s], unfold highest, simp)

   116 

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

   118   by (fold eq_cp_s_th, unfold highest_cp_preced, simp)

   119 

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

   121 proof -

   122   { assume "th \<notin> readys s"

   123     with threads_s obtain cs where 

   124       "waiting s th cs"

   125       by (unfold readys_def, auto)

   126     hence "(Th th, Cs cs) \<in> depend s"

   127       by (unfold s_depend_def, unfold eq_waiting, simp)

   128     hence "Th th \<in> Domain (depend s')"

   129       by (unfold same_depend, auto simp:Domain_def)

   130     from dm_depend_threads [OF vt_s' this] 

   131     have h: "th \<in> threads s'" .

   132     have "False"

   133     proof (rule_tac step_create_elim)

   134       assume "th \<notin> threads s'" with h show ?thesis by simp

   135     qed

   136   } thus ?thesis by auto

   137 qed

   138 

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

   140 proof -

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

   142   proof -

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

   144     proof(rule Max_eqI)

   145       from finite_threads[OF vt_s] readys_threads finite_subset

   146       have "finite (readys s)" by blast

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

   148     next

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

   150     next

   151       fix y

   152       assume h: "y \<in> cp s ` readys s"

   153       have "y \<le> Max (cp s ` readys s)"

   154       proof(rule Max_ge [OF _ h])

   155         from finite_threads[OF vt_s] readys_threads finite_subset

   156         have "finite (readys s)" by blast

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

   158       qed

   159       moreover have "\<dots> \<le> Max (cp s ` threads s)"

   160       proof(rule Max_mono)

   161         from readys_threads 

   162         show "cp s ` readys s \<subseteq> cp s ` threads s" by auto

   163       next

   164         from is_ready show "cp s ` readys s \<noteq> {}" by auto

   165       next

   166         from finite_threads [OF vt_s]

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

   168       qed

   169       moreover note highest

   170       ultimately show "y \<le> cp s th" by auto

   171     qed

   172     with highest show ?thesis by auto

   173   qed

   174   thus ?thesis

   175     by (unfold runing_def, insert highest is_ready, auto)

   176 qed

   177 

   178 end

   179 

   180 locale extend_highest = highest_create + 

   181   fixes t 

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

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

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

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

   186 

   187 lemma step_back_vt_app: 

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

   189   shows "vt cs s"

   190 proof -

   191   from vt_ts show ?thesis

   192   proof(induct t)

   193     case Nil

   194     from Nil show ?case by auto

   195   next

   196     case (Cons e t)

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

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

   199     show ?case

   200     proof(rule ih)

   201       show "vt cs (t @ s)"

   202       proof(rule step_back_vt)

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

   204       qed

   205     qed

   206   qed

   207 qed

   208 

   209 context extend_highest

   210 begin

   211 

   212 lemma red_moment:

   213   "extend_highest s' th prio (moment i t)"

   214   apply (insert extend_highest_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])

   215   apply (unfold extend_highest_def extend_highest_axioms_def, clarsimp)

   216   by (unfold highest_create_def, auto dest:step_back_vt_app)

   217 

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

   219   assumes 

   220     h0: "R []"

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

   222                     extend_highest s' th prio t; 

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

   224   shows "R t"

   225 proof -

   226   from vt_t extend_highest_axioms show ?thesis

   227   proof(induct t)

   228     from h0 show "R []" .

   229   next

   230     case (Cons e t')

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

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

   233       and et: "extend_highest s' th prio (e # t')"

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

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

   236     show ?case

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

   238       show "R t'"

   239       proof(rule ih)

   240         from et show ext': "extend_highest s' th prio t'"

   241           by (unfold extend_highest_def extend_highest_axioms_def, auto dest:step_back_vt)

   242       next

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

   244       qed

   245     next

   246       from et show "extend_highest s' th prio (e # t')" .

   247     next

   248       from et show ext': "extend_highest s' th prio t'"

   249           by (unfold extend_highest_def extend_highest_axioms_def, auto dest:step_back_vt)

   250     qed

   251   qed

   252 qed

   253 

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

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

   256 proof -

   257   show ?thesis

   258   proof(induct rule:ind)

   259     case Nil

   260     from threads_s

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

   262       by auto

   263   next

   264     case (Cons e t)

   265     show ?case

   266     proof(cases e)

   267       case (Create thread prio)

   268       assume eq_e: " e = Create thread prio"

   269       show ?thesis

   270       proof -

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

   272         hence "th \<noteq> thread"

   273         proof(cases)

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

   275           with Cons show ?thesis by auto

   276         qed

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

   278           by (unfold eq_e, auto simp:preced_def)

   279         moreover note Cons

   280         ultimately show ?thesis

   281           by (auto simp:eq_e)

   282       qed

   283     next

   284       case (Exit thread)

   285       assume eq_e: "e = Exit thread"

   286       from Cons have "extend_highest s' th prio (e # t)" by auto

   287       from extend_highest.exit_diff [OF this] and eq_e

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

   289       with Cons

   290       show ?thesis

   291         by (unfold eq_e, auto simp:preced_def)

   292     next

   293       case (P thread cs)

   294       assume eq_e: "e = P thread cs"

   295       with Cons

   296       show ?thesis 

   297         by (auto simp:eq_e preced_def)

   298     next

   299       case (V thread cs)

   300       assume eq_e: "e = V thread cs"

   301       with Cons

   302       show ?thesis 

   303         by (auto simp:eq_e preced_def)

   304     next

   305       case (Set thread prio')

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

   307       show ?thesis

   308       proof -

   309         from Cons have "extend_highest s' th prio (e # t)" by auto

   310         from extend_highest.set_diff_low[OF this] and eq_e

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

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

   313           by (unfold eq_e, auto simp:preced_def)

   314         moreover note Cons

   315         ultimately show ?thesis

   316           by (auto simp:eq_e)

   317       qed

   318     qed

   319   qed

   320 qed

   321 

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

   323 proof(induct rule:ind)

   324   case Nil

   325   from highest_preced_thread

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

   327     by simp

   328 next

   329   case (Cons e t)

   330   show ?case

   331   proof(cases e)

   332     case (Create thread prio')

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

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

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

   336     proof(cases)

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

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

   339       proof -

   340         from Cons have "extend_highest s' th prio t" by auto

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

   342       qed

   343       ultimately show ?thesis by auto

   344     qed

   345     from Cons have "extend_highest s' th prio t" by auto

   346     from extend_highest.th_kept[OF this]

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

   348       by (auto simp:s_def)

   349     from stp

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

   351       by (cases, auto)

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

   353     proof -

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

   355         by (unfold eq_e, simp)

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

   357       proof(rule Max_insert)

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

   359         from finite_threads[OF this]

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

   361       next

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

   363       qed

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

   365       proof -

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

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

   368         proof -

   369           { fix th' 

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

   371             with thread_ts eq_e

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

   373           } thus ?thesis 

   374             apply (auto simp:Image_def)

   375           proof -

   376             fix th'

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

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

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

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

   381             proof -

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

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

   384               ultimately show ?thesis by simp

   385             qed

   386           qed

   387         qed

   388         with Cons show ?thesis by auto

   389       qed

   390       moreover have "?f thread < ?t"

   391       proof -

   392         from Cons have " extend_highest s' th prio (e # t)" by auto

   393         from extend_highest.create_low[OF this] and eq_e

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

   395         thus ?thesis

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

   397     qed

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

   399   qed

   400 next

   401     case (Exit thread)

   402     assume eq_e: "e = Exit thread"

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

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

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

   406       by(cases, unfold runing_def readys_def, auto)

   407     from Cons have "extend_highest s' th prio (e # t)" by auto

   408     from extend_highest.exit_diff[OF this] and eq_e

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

   410     from Cons have "extend_highest s' th prio t" by auto

   411     from extend_highest.th_kept[OF this, folded s_def]

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

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

   414     proof -

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

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

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

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

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

   420       proof(rule Max_insert)

   421         from finite_threads [OF vt_e]

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

   423       next

   424         from Cons have "extend_highest s' th prio (e # t)" by auto

   425         from extend_highest.th_kept[OF this]

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

   427       qed

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

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

   430       proof -

   431         from Cons show ?thesis

   432           by (unfold eq_e, auto simp:preced_def)

   433       qed

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

   435       moreover have "?f thread < ?t"

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

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

   438         proof -

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

   440           proof -

   441             from Cons

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

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

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

   445             proof(rule Max_ge)

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

   447               from finite_threads [OF this]

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

   449             next

   450               from thread_ts

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

   452             qed

   453             ultimately show ?thesis by auto

   454           qed

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

   456           proof

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

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

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

   460             proof

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

   462             next

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

   464             qed(simp)

   465             with neq_thread show "False" by simp

   466           qed

   467           ultimately show ?thesis by auto

   468         qed

   469       qed

   470       ultimately show ?thesis 

   471         by (auto simp:max_def split:if_splits)

   472     qed

   473   next

   474     case (P thread cs)

   475     with Cons

   476     show ?thesis by (auto simp:preced_def)

   477   next

   478     case (V thread cs)

   479     with Cons

   480     show ?thesis by (auto simp:preced_def)

   481   next

   482     case (Set thread prio')

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

   484     proof -

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

   486       from Cons have "extend_highest s' th prio (e # t)" by auto

   487       from extend_highest.set_diff_low[OF this] and Set

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

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

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

   491       proof(rule Max_eqI)

   492         fix y

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

   494         then obtain th1 where 

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

   496         show "y \<le> ?t"

   497         proof(cases "th1 = thread")

   498           case True

   499           with neq_thread le_p eq_y s_def Set

   500           show ?thesis

   501             by (auto simp:preced_def precedence_le_def)

   502         next

   503           case False

   504           with Set eq_y

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

   506             by (simp add:preced_def)

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

   508           proof -

   509             from Cons

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

   511               by auto

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

   513             proof(rule Max_ge)

   514               from th1_in 

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

   516                 by simp

   517             next

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

   519               proof -

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

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

   522               qed

   523             qed

   524             ultimately show ?thesis by auto

   525           qed

   526           ultimately show ?thesis by auto

   527         qed

   528       next

   529         from Cons and finite_threads

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

   531       next

   532         from Cons have "extend_highest s' th prio t" by auto

   533         from extend_highest.th_kept [OF this, folded s_def]

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

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

   536         proof -

   537           from neq_thread Set h

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

   539           with h show ?thesis by auto

   540         qed

   541       qed

   542       finally show ?thesis .

   543     qed

   544   qed

   545 qed

   546 

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

   548   by (insert th_kept max_kept, auto)

   549 

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

   551   (is "?L = ?R")

   552 proof -

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

   554     by (unfold cp_eq_cpreced, simp)

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

   556   proof(unfold cpreced_def)

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

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

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

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

   561       case False

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

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

   564       proof(rule Max_insert)

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

   566         proof -

   567           from dependents_threads[OF vt_t]

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

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

   570           ultimately show ?thesis 

   571             by (auto simp:finite_subset)

   572         qed

   573       next

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

   575       qed

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

   577       proof -

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

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

   580         proof(rule Max_mono)

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

   582         next

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

   584           proof -

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

   586             thus ?thesis by auto

   587           qed

   588         next

   589           from finite_threads[OF vt_t] 

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

   591         qed

   592         ultimately show ?thesis

   593           by (auto simp:max_def)

   594       qed

   595       ultimately show ?thesis by auto

   596     next

   597       case True

   598       with max_preced show ?thesis by auto

   599     qed

   600   qed

   601   finally show ?thesis .

   602 qed

   603 

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

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

   606 

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

   608   by (fold max_kept, unfold th_cp_max_preced, simp)

   609 

   610 lemma preced_less':

   611   fixes th'

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

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

   614   shows "preced th' s < preced th s"

   615 proof -

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

   617   proof(rule Max_ge)

   618     from finite_threads [OF vt_s]

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

   620   next

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

   622       by simp

   623   qed

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

   625   proof

   626     assume "preced th' s = preced th s"

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

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

   629   qed

   630   ultimately show ?thesis using highest_preced_thread

   631     by auto

   632 qed

   633 

   634 lemma pv_blocked:

   635   fixes th'

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

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

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

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

   640 proof

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

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

   643     by (auto simp:runing_def)

   644   with max_cp_readys_threads [OF vt_t]

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

   646     by auto

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

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

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

   650     by simp

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

   652   show False

   653   proof -

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

   655       by (rule count_eq_dependents [OF vt_t eq_pv])

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

   657     proof

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

   659       hence "th' = th"

   660       proof(rule preced_unique)

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

   662       next

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

   664       qed

   665       with assms show False by simp

   666     qed

   667     ultimately show ?thesis

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

   669   qed

   670 qed

   671 

   672 lemma runing_precond_pre:

   673   fixes th'

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

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

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

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

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

   679 proof -

   680   show ?thesis

   681   proof(induct rule:ind)

   682     case (Cons e t)

   683     from Cons

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

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

   686     have "extend_highest s' th prio t" by fact

   687     from extend_highest.pv_blocked 

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

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

   690     show ?case

   691     proof(cases e)

   692       case (V thread cs)

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

   694 

   695       show ?thesis

   696       proof -

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

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

   699         proof(cases)

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

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

   702           ultimately show ?thesis by auto

   703         qed

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

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

   706         moreover from in_thread

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

   708         ultimately show ?thesis by auto

   709       qed

   710     next

   711       case (P thread cs)

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

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

   714       proof(cases)

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

   716         moreover note not_runing

   717         ultimately show ?thesis by auto

   718       qed

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

   720         by (auto simp:cntP_def cntV_def count_def)

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

   722         by auto

   723       ultimately show ?thesis by auto

   724     next

   725       case (Create thread prio')

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

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

   728       proof(cases)

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

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

   731         ultimately show ?thesis by auto

   732       qed

   733       with Cons and Create 

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

   735         by (auto simp:cntP_def cntV_def count_def)

   736       moreover from Cons and Create 

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

   738       ultimately show ?thesis by auto

   739     next

   740       case (Exit thread)

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

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

   743       proof(cases)

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

   745         moreover note not_runing

   746         ultimately show ?thesis by auto

   747       qed

   748       with Cons and Exit 

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

   750         by (auto simp:cntP_def cntV_def count_def)

   751       moreover from Cons and Exit and neq_th' 

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

   753         by auto

   754       ultimately show ?thesis by auto

   755     next

   756       case (Set thread prio')

   757       with Cons

   758       show ?thesis 

   759         by (auto simp:cntP_def cntV_def count_def)

   760     qed

   761   next

   762     case Nil

   763     with assms

   764     show ?case by auto

   765   qed

   766 qed

   767 

   768 (*

   769 lemma runing_precond:

   770   fixes th'

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

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

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

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

   775 proof -

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

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

   778   from pv_blocked[OF h1 neq_th' h2] 

   779   show ?thesis .

   780 qed

   781 *)

   782 

   783 lemma runing_precond:

   784   fixes th'

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

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

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

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

   789 proof -

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

   791   proof

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

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

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

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

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

   797     with is_runing show "False" by simp

   798   qed

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

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

   801   ultimately show ?thesis by auto

   802 qed

   803 

   804 lemma moment_blocked_pre:

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

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

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

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

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

   810 proof(induct j)

   811   case (Suc k)

   812   show ?case

   813   proof -

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

   815       from moment_head [OF this] 

   816       obtain e where

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

   818         by blast

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

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

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

   822         by (unfold extend_highest_def extend_highest_axioms_def 

   823           highest_create_def s_def, auto)

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

   825       proof(unfold s_def)

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

   827         proof(rule extend_highest.pv_blocked)

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

   829             by (simp add:s_def)

   830         next

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

   832         next

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

   834         next

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

   836             cntV (moment (i + k) t @ Create th prio # s') th'"

   837             by (auto simp:s_def)

   838         qed

   839       qed

   840       from step_back_step[OF vt_e]

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

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

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

   844         "

   845       proof(cases)

   846         case (thread_create thread prio)

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

   848       next

   849         case (thread_exit thread)

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

   851         proof -

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

   853           moreover note not_runing'

   854           ultimately show ?thesis by auto

   855         qed

   856         moreover note Suc 

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

   858       next

   859         case (thread_P thread cs)

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

   861         proof -

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

   863           moreover note not_runing'

   864           ultimately show ?thesis by auto

   865         qed

   866         moreover note Suc 

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

   868       next

   869         case (thread_V thread cs)

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

   871         proof -

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

   873           moreover note not_runing'

   874           ultimately show ?thesis by auto

   875         qed

   876         moreover note Suc 

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

   878       next

   879         case (thread_set thread prio')

   880         with Suc show ?thesis

   881           by (auto simp:cntP_def cntV_def count_def)

   882       qed

   883       with eq_me have ?thesis using eq_me by auto 

   884     } note h = this

   885     show ?thesis

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

   887       case True

   888       from h [OF this] show ?thesis .

   889     next

   890       case False

   891       with moment_ge

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

   893       with Suc show ?thesis by auto

   894     qed

   895   qed

   896 next

   897   case 0

   898   from assms show ?case by auto

   899 qed

   900 

   901 lemma moment_blocked:

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

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

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

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

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

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

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

   909 proof -

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

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

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

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

   914   show ?thesis by auto

   915 qed

   916 

   917 lemma runing_inversion_1:

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

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

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

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

   922   case True

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

   924 next

   925   case False

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

   927   let ?q = "moment 0 t"

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

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

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

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

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

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

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

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

   936   from moment_head[OF this] obtain e where 

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

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

   939   have "extend_highest s' th prio (e # moment i t)" by simp

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

   941     by (unfold extend_highest_def extend_highest_axioms_def 

   942       highest_create_def s_def, auto)

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

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

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

   946   from create_pre[OF stp_i pre this] 

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

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

   949   proof(rule cnp_cnv_eq)

   950     from step_back_vt [OF vt_e] 

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

   952   next

   953     from eq_e and stp_i 

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

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

   956   qed

   957   with eq_e

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

   959     by (simp add:cntP_def cntV_def count_def)

   960   with eq_me[symmetric]

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

   962     by simp

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

   964   with eq_me [symmetric]

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

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

   967   and moment_ge

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

   969   with runing'

   970   show ?thesis by auto

   971 qed

   972 

   973 lemma runing_inversion_2:

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

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

   976 proof -

   977   from runing_inversion_1[OF _ runing']

   978   show ?thesis by auto

   979 qed

   980 

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

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

   983   case True thus ?thesis by auto

   984 next

   985   case False

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

   987     apply (unfold runing_def, 

   988             insert th_cp_max max_cp_readys_threads[OF vt_t, symmetric])

   989     by auto

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

   991   from th_chain_to_ready[OF vt_t this] and not_ready

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

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

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

   995   proof -

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

   997     proof -

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

   999                preced th (t@s)"

  1000       proof(rule Max_eqI)

  1001         fix y

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

  1003         then obtain th1 where

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

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

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

  1007         proof -

  1008           from max_preced

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

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

  1011           proof(rule Max_ge)

  1012             from h1

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

  1014             proof

  1015               assume "th1 = th'"

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

  1017             next

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

  1019               with dependents_threads [OF vt_t]

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

  1021             qed

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

  1023           next

  1024             from finite_threads[OF vt_t]

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

  1026           qed

  1027           ultimately show ?thesis by auto

  1028         qed

  1029       next

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

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

  1032           by (auto intro:finite_subset)

  1033       next

  1034         from dp

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

  1036           by (unfold cs_dependents_def, auto simp:eq_depend)

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

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

  1039           by auto

  1040       qed

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

  1042       proof -

  1043         from max_preced and max_cp_eq[OF vt_t, symmetric]

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

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

  1046       qed

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

  1048     qed

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

  1050   qed

  1051   thus ?thesis by auto

  1052 qed

  1053 

  1054 end

  1055 

  1056 end

  1057