372 lemma waiting_unique_pre: (* ccc *)

   321 lemma waiting_unique_pre: (* ddd *)

   405   { fix i1 i2

   354   { fix t1 t2 cs1 cs2

   406     let ?i3 = "Suc i2"

   355     assume  lt1: "t1 < length s"

   407     assume lt12: "i1 < i2"

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

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

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

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

   358     and lt2: "t2 < length s"

   410     from moment_plus [OF this]

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

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

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

   412     have "i2 < ?i3" by simp

   361     and 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

   423         by (unfold_locales, auto, cases, simp)

   431           by (unfold_locales, auto, cases, simp)

   424       have ?thesis

   432       have "e = V thread cs2 \<or> e = P thread cs2"

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

   435         have "e = V thread cs2"

   428           by auto 

   436         proof -

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

   437           have eq_th: "thread = hd (wq (moment t2 s) cs2)" 

   430         show ?thesis by auto

   438               using True and np2  by auto 

   439           from vt_e.wq_out_inv[OF True this h2]

   440           show ?thesis .

   441         qed

   442         thus ?thesis by auto

   433         from vt_e.block_pre[OF False h1]

   445         have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .

   434         have "e = P thread cs2" .

   446         thus ?thesis by auto

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

   447       qed

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

   448       moreover have "e = V thread cs1 \<or> e = P thread cs1"

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

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

   438         with nn1 [rule_format, OF lt12]

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

   440       qed

   441   }

   442   show ?thesis

   443   proof -

   444     { 

   445       assume lt12: "t1 < t2"

   446       let ?t3 = "Suc t2"

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

   448       from moment_plus [OF this] 

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

   450       have "t2 < ?t3" by simp

   451       from nn2 [rule_format, OF this] and eq_m

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

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

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

   455       proof -

   456         from vt_moment 

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

   458         with eq_m show ?thesis by simp

   459       qed

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

   461         by (unfold_locales, auto, cases, simp)

   462       have ?thesis

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

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

   451         have eq_th: "thread = hd (wq (moment t1 s) cs1)" 

   466           by auto 

   452               using True and np1  by auto 

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

   453         from vt_e.wq_out_inv[folded eq_12, OF True this g2]

   468         show ?thesis by auto

   454         have "e = V thread cs1" .

   455         thus ?thesis by auto

   471         from vt_e.block_pre[OF False h1]

   458         have "e = P thread cs1" using vt_e.wq_in_inv[folded eq_12, OF False g1] .

   472         have "e = P thread cs2" .

   459         thus ?thesis by auto

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

   460       qed

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

   461       ultimately have ?thesis using neq12 by auto

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

   462     } ultimately show ?thesis using nat_neq_iff by blast 

   476         with nn1 [rule_format, OF lt12]

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

   478       qed

   479     } moreover {

   480       assume lt12: "t2 < t1"

   481       let ?t3 = "Suc t1"

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

   483       from moment_plus [OF this] 

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

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

   486       from nn1 [rule_format, OF this] and eq_m

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

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

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

   490       proof -

   491         from vt_moment

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

   493         with eq_m show ?thesis by simp

   494       qed

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

   496         by (unfold_locales, auto, cases, auto)

   497       have ?thesis

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

   499         case True

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

   501           by auto

   502         from vt_e.abs2 True eq_th h2 h1

   503         show ?thesis by auto

   504       next

   505         case False

   506         from vt_e.block_pre [OF False h1]

   507         have "e = P thread cs1" .

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

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

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

   511         with nn2 [rule_format, OF lt12]

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

   513       qed

   514     } moreover {

   515       assume eqt12: "t1 = t2"

   516       let ?t3 = "Suc t1"

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

   518       from moment_plus [OF this] 

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

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

   521       from nn1 [rule_format, OF this] and eq_m

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

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

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

   525       proof -

   526         from vt_moment

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

   528         with eq_m show ?thesis by simp

   529       qed

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

   531         by (unfold_locales, auto, cases, auto)

   532       have ?thesis

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

   534         case True

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

   536           by auto

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

   538         show ?thesis by auto

   539       next

   540         case False

   541         from vt_e.block_pre [OF False h1]

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

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

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

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

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

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

   548         show ?thesis

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

   550           case True

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

   552             by auto

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

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

   555             by (unfold_locales, auto, cases, auto)

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

   557           show ?thesis .

   558         next

   559           case False

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

   561           proof -

   562             from vt_moment eqt12

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

   564             with eq_m eqt12 show ?thesis by simp

   565           qed

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

   567             by (unfold_locales, auto, cases, auto)

   568           from vt_e2.block_pre [OF False h1]

   569           have "e = P thread cs2" .

   570           with eq_e1 neq12 show ?thesis by auto

   571         qed

   572       qed

   573     } ultimately show ?thesis by arith

   585 using waiting_unique_pre assms

   474   using waiting_unique_pre assms

   586 unfolding wq_def s_waiting_def

   475   unfolding wq_def s_waiting_def

   587 by auto

   476   by auto

   624 

   513                       

   636 (* An aux lemma used later *)

   525 (* An aux lemma used later *) 

   746 

   635 context valid_trace

   747 text {* 

   636 begin

   748   The following lemmas are used in the proof of 

   637 

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

   638 lemma finite_threads:

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

   639   shows "finite (threads s)"

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

   640 using vt by (induct) (auto elim: step.cases)

   752   starting from the model definitions.

   641 

   753 *}

   642 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"

   754 lemma step_v_hold_inv[elim_format]:

   643 unfolding cp_def wq_def

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

   644 apply(induct s rule: schs.induct)

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

   645 thm cpreced_initial

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

   646 apply(simp add: Let_def cpreced_initial)

   758 proof -

   647 apply(simp add: Let_def)

   759   fix c t

   648 apply(simp add: Let_def)

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

   649 apply(simp add: Let_def)

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

   650 apply(subst (2) schs.simps)

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

   651 apply(simp add: Let_def)

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

   652 apply(subst (2) schs.simps)

   764   proof(cases "c = cs")

   653 apply(simp add: Let_def)

   654 done

   655 

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

   657   by (unfold s_RAG_def, auto)

   658 

   659 lemma wq_threads: 

   660   assumes h: "th \<in> set (wq s cs)"

   661   shows "th \<in> threads s"

   662 proof -

   663  from vt and h show ?thesis

   664   proof(induct arbitrary: th cs)

   665     case (vt_cons s e)

   666     interpret vt_s: valid_trace s

   667       using vt_cons(1) by (unfold_locales, auto)

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

   669       and stp: "step s e"

   670       and vt: "vt s"

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

   672     show ?case

   673     proof(cases e)

   674       case (Create th' prio)

   675       with ih h show ?thesis

   676         by (auto simp:wq_def Let_def)

   677     next

   678       case (Exit th')

   679       with stp ih h show ?thesis

   680         apply (auto simp:wq_def Let_def)

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

   682         apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def

   683                s_RAG_def s_holding_def cs_holding_def)

   684         done

   685     next

   686       case (V th' cs')

   687       show ?thesis

   688       proof(cases "cs' = cs")

   689         case False

   690         with h

   691         show ?thesis

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

   693           by (drule_tac ih, simp)

   694       next

   695         case True

   696         from h

   697         show ?thesis

   698         proof(unfold V wq_def)

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

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

   701           proof(cases "cs = cs'")

   702             case False

   703             hence "?l = wq_fun (schs s) cs" by (simp add:Let_def)

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

   705               by (fold wq_def, simp)

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

   707           next

   708             case True

   709             show ?thesis

   710             proof(cases "wq_fun (schs s) cs'")

   711               case Nil

   712               with h V show ?thesis

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

   714                 by (fold wq_def, drule_tac ih, simp)

   715             next

   716               case (Cons a rest)

   717               assume eq_wq: "wq_fun (schs s) cs' = a # rest"

   718               with h V show ?thesis

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

   720               proof -

   721                 assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"

   722                 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 

   723                 proof(rule someI2)

   724                   from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def]

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

   726                 next

   727                   show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"

   728                     by auto

   729                 qed

   730                 with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto

   731                 from ih[OF this[folded wq_def]] show "th \<in> threads s" .

   732               next

   733                 assume th_in: "th \<in> set (wq_fun (schs s) cs)"

   734                 from ih[OF this[folded wq_def]]

   735                 show "th \<in> threads s" .

   736               qed

   737             qed

   738           qed

   739         qed

   740       qed

   741     next

   742       case (P th' cs')

   743       from h stp

   744       show ?thesis

   745         apply (unfold P wq_def)

   746         apply (auto simp:Let_def split:if_splits, fold wq_def)

   747         apply (auto intro:ih)

   748         apply(ind_cases "step s (P th' cs')")

   749         by (unfold runing_def readys_def, auto)

   750     next

   751       case (Set thread prio)

   752       with ih h show ?thesis

   753         by (auto simp:wq_def Let_def)

   754     qed

   755   next

   756     case vt_nil

   757     thus ?case by (auto simp:wq_def)

   758   qed

   759 qed

   760 

   761 lemma dm_RAG_threads:

   762   assumes in_dom: "(Th th) \<in> Domain (RAG s)"

   763   shows "th \<in> threads s"

   764 proof -

   765   from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto

   766   moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto

   767   ultimately have "(Th th, Cs cs) \<in> RAG s" by simp

   768   hence "th \<in> set (wq s cs)"

   769     by (unfold s_RAG_def, auto simp:cs_waiting_def)

   770   from wq_threads [OF this] show ?thesis .

   771 qed

   772 

   773 

   774 lemma cp_le:

   775   assumes th_in: "th \<in> threads s"

   776   shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"

   777 proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)

   778   show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))

   779          \<le> Max ((\<lambda>th. preced th s) ` threads s)"

   780     (is "Max (?f ` ?A) \<le> Max (?f ` ?B)")

   781   proof(rule Max_f_mono)

   782     show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp

   783   next

   784     from finite_threads

   785     show "finite (threads s)" .

   786   next

   787     from th_in

   788     show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"

   789       apply (auto simp:Domain_def)

   790       apply (rule_tac dm_RAG_threads)

   791       apply (unfold trancl_domain [of "RAG s", symmetric])

   792       by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)

   793   qed

   794 qed

   795 

   796 lemma le_cp:

   797   shows "preced th s \<le> cp s th"

   798 proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)

   799   show "Prc (priority th s) (last_set th s)

   800     \<le> Max (insert (Prc (priority th s) (last_set th s))

   801             ((\<lambda>th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))"

   802     (is "?l \<le> Max (insert ?l ?A)")

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

   766     with nhd hd show ?thesis

   805     have "finite ?A" (is "finite (?f ` ?B)")

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

   806     proof -

   807       have "finite ?B" 

   808       proof-

   809         have "finite {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}"

   810         proof -

   811           let ?F = "\<lambda> (x, y). the_th x"

   812           have "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)"

   813             apply (auto simp:image_def)

   814             by (rule_tac x = "(Th x, Th th)" in bexI, auto)

   815           moreover have "finite \<dots>"

   816           proof -

   817             from finite_RAG have "finite (RAG s)" .

   818             hence "finite ((RAG (wq s))\<^sup>+)"

   819               apply (unfold finite_trancl)

   820               by (auto simp: s_RAG_def cs_RAG_def wq_def)

   821             thus ?thesis by auto

   822           qed

   823           ultimately show ?thesis by (auto intro:finite_subset)

   824         qed

   825         thus ?thesis by (simp add:cs_dependants_def)

   826       qed

   827       thus ?thesis by simp

   828     qed

   829     from Max_insert [OF this False, of ?l] show ?thesis by auto

   770     with step_back_step [OF vt] 

   832     thus ?thesis by auto

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

   833   qed

   772     hence "next_th s th cs t"

   834 qed

   773     proof(cases)

   835 

   774       assume "holding s th c"

   836 lemma max_cp_eq: 

   775       with nhd hd show ?thesis

   837   shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"

   776         apply (unfold s_holding_def cs_holding_def wq_def next_th_def,

   838   (is "?l = ?r")

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

   839 proof(cases "threads s = {}")

   778         proof -

   840   case True

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

   841   thus ?thesis by auto

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

   842 next

   781           proof(rule someI2)

   843   case False

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

   844   have "?l \<in> ((cp s) ` threads s)"

   783           next

   845   proof(rule Max_in)

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

   846     from finite_threads

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

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

   786           qed

   848   next

   787           ultimately show False by auto

   849     from False show "cp s ` threads s \<noteq> {}" by auto

   788         next

   850   qed

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

   851   then obtain th 

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

   852     where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto

   791           proof(rule someI2)

   853   have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])

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

   854   moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")

   793           next

   855   proof -

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

   856     have "?r \<in> (?f ` ?A)"

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

   857     proof(rule Max_in)

   796           qed

   858       from finite_threads

   797           ultimately show False by auto

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

   798         qed

   860     next

   799     qed

   861       from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto

   800     with True show ?thesis by auto

   862     qed

   801   qed

   863     then obtain th' where 

   802 qed

   864       th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto

   803 

   865     from le_cp [of th']  eq_r

   804 text {* 

   866     have "?r \<le> cp s th'" by auto

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

   867     moreover have "\<dots> \<le> cp s th"

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

   868     proof(fold eq_l)

   807 *}

   869       show " cp s th' \<le> Max (cp s ` threads s)"

   808 lemma step_v_wait_inv[elim_format]:

   870       proof(rule Max_ge)

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

   871         from th_in' show "cp s th' \<in> cp s ` threads s"

   810            \<rbrakk>

   872           by auto

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

   873       next

   812 proof -

   874         from finite_threads

   813   fix t c 

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

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

   876       qed

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

   877     qed

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

   878     ultimately show ?thesis by auto

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

   879   qed

   818     by  (cases, unfold_locales, simp)

   880   ultimately show ?thesis using eq_l by auto

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

   881 qed

   820   proof(cases "cs = c")

   882 

   883 lemma max_cp_eq_the_preced:

   884   shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"

   885   using max_cp_eq using the_preced_def by presburger 

   886 

   887 end

   888 

   889 lemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s"

   890   by (unfold preced_def, simp)

   891 

   892 lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s"

   893 proof

   894   fix th'

   895   show "the_preced (V th cs # s) th' = the_preced s th'"

   896     by (unfold the_preced_def preced_def, simp)

   897 qed

   898 

   899 locale valid_trace_v = valid_trace_e + 

   900   fixes th cs

   901   assumes is_v: "e = V th cs"

   902 

   903 context valid_trace_v

   904 begin

   905 

   906 definition "rest = tl (wq s cs)"

   907 

   908 definition "wq' = (SOME q. distinct q \<and> set q = set rest)"

   909 

   910 lemma distinct_rest: "distinct rest"

   911   by (simp add: distinct_tl rest_def wq_distinct)

   912 

   913 lemma runing_th_s:

   914   shows "th \<in> runing s"

   915 proof -

   916   from pip_e[unfolded is_v]

   917   show ?thesis by (cases, simp)

   918 qed

   919 

   920 lemma holding_cs_eq_th:

   921   assumes "holding s t cs"

   922   shows "t = th"

   923 proof -

   924   from pip_e[unfolded is_v]

   925   show ?thesis

   926   proof(cases)

   927     case (thread_V)

   928     from held_unique[OF this(2) assms]

   929     show ?thesis by simp

   930   qed

   931 qed

   932 

   933 lemma th_not_waiting: 

   934   "\<not> waiting s th c"

   935 proof -

   936   have "th \<in> readys s"

   937     using runing_ready runing_th_s by blast 

   938   thus ?thesis

   939     by (unfold readys_def, auto)

   940 qed

   941 

   942 lemma waiting_neq_th: 

   943   assumes "waiting s t c"

   944   shows "t \<noteq> th"

   945   using assms using th_not_waiting by blast 

   946 

   947 lemma wq_s_cs:

   948   "wq s cs = th#rest"

   949 proof -

   950   from pip_e[unfolded is_v]

   951   show ?thesis

   952   proof(cases)

   953     case (thread_V)

   954     from this(2) show ?thesis

   955       by (unfold rest_def s_holding_def, fold wq_def,

   956                  metis empty_iff list.collapse list.set(1))

   957   qed

   958 qed

   959 

   960 lemma wq_es_cs:

   961   "wq (e#s) cs = wq'"

   962  using wq_s_cs[unfolded wq_def]

   963  by (auto simp:Let_def wq_def rest_def wq'_def is_v, simp) 

   964 

   965 lemma distinct_wq': "distinct wq'"

   966   by (metis (mono_tags, lifting) distinct_rest  some_eq_ex wq'_def)

   967   

   968 lemma th'_in_inv:

   969   assumes "th' \<in> set wq'"

   970   shows "th' \<in> set rest"

   971   using assms

   972   by (metis (mono_tags, lifting) distinct.simps(2) 

   973         rest_def some_eq_ex wq'_def wq_distinct wq_s_cs) 

   974 

   975 lemma neq_t_th: 

   976   assumes "waiting (e#s) t c"

   977   shows "t \<noteq> th"

   978 proof

   979   assume otherwise: "t = th"

   980   show False

   981   proof(cases "c = cs")

   982     case True

   983     have "t \<in> set wq'" 

   984      using assms[unfolded True s_waiting_def, folded wq_def, unfolded wq_es_cs]

   985      by simp 

   986     from th'_in_inv[OF this] have "t \<in> set rest" .

   987     with wq_s_cs[folded otherwise] wq_distinct[of cs]

   988     show ?thesis by simp

   989   next

   822     with nw wt show ?thesis

   991     have "wq (e#s) c = wq s c" using False

   823       by (auto simp:cs_waiting_def wq_def Let_def)

   992         by (unfold is_v, simp)

   993     hence "waiting s t c" using assms 

   994         by (simp add: cs_waiting_def waiting_eq)

   995     hence "t \<notin> readys s" by (unfold readys_def, auto)

   996     hence "t \<notin> runing s" using runing_ready by auto 

   997     with runing_th_s[folded otherwise] show ?thesis by auto

   998   qed

   999 qed

  1000 

  1001 lemma waiting_esI1:

  1002   assumes "waiting s t c"

  1003       and "c \<noteq> cs" 

  1004   shows "waiting (e#s) t c" 

  1005 proof -

  1006   have "wq (e#s) c = wq s c" 

  1007     using assms(2) is_v by auto

  1008   with assms(1) show ?thesis 

  1009     using cs_waiting_def waiting_eq by auto 

  1010 qed

  1011 

  1012 lemma holding_esI2:

  1013   assumes "c \<noteq> cs" 

  1014   and "holding s t c"

  1015   shows "holding (e#s) t c"

  1016 proof -

  1017   from assms(1) have "wq (e#s) c = wq s c" using is_v by auto

  1018   from assms(2)[unfolded s_holding_def, folded wq_def, 

  1019                 folded this, unfolded wq_def, folded s_holding_def]

  1020   show ?thesis .

  1021 qed

  1022 

  1023 end

  1024 

  1025 locale valid_trace_v_n = valid_trace_v +

  1026   assumes rest_nnl: "rest \<noteq> []"

  1027 begin

  1028 

  1029 lemma neq_wq': "wq' \<noteq> []" 

  1030 proof (unfold wq'_def, rule someI2)

  1031   show "distinct rest \<and> set rest = set rest"

  1032     by (simp add: distinct_rest) 

  1033 next

  1034   fix x

  1035   assume " distinct x \<and> set x = set rest" 

  1036   thus "x \<noteq> []" using rest_nnl by auto

  1037 qed 

  1038 

  1039 definition "taker = hd wq'"

  1040 

  1041 definition "rest' = tl wq'"

  1042 

  1043 lemma eq_wq': "wq' = taker # rest'"

  1044   by (simp add: neq_wq' rest'_def taker_def)

  1045 

  1046 lemma next_th_taker: 

  1047   shows "next_th s th cs taker"

  1048   using rest_nnl taker_def wq'_def wq_s_cs 

  1049   by (auto simp:next_th_def)

  1050 

  1051 lemma taker_unique: 

  1052   assumes "next_th s th cs taker'"

  1053   shows "taker' = taker"

  1054 proof -

  1055   from assms

  1056   obtain rest' where 

  1057     h: "wq s cs = th # rest'" 

  1058        "taker' = hd (SOME q. distinct q \<and> set q = set rest')"

  1059           by (unfold next_th_def, auto)

  1060   with wq_s_cs have "rest' = rest" by auto

  1061   thus ?thesis using h(2) taker_def wq'_def by auto 

  1062 qed

  1063 

  1064 lemma waiting_set_eq:

  1065   "{(Th th', Cs cs) |th'. next_th s th cs th'} = {(Th taker, Cs cs)}"

  1066   by (smt all_not_in_conv bot.extremum insertI1 insert_subset 

  1067       mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)

  1068 

  1069 lemma holding_set_eq:

  1070   "{(Cs cs, Th th') |th'.  next_th s th cs th'} = {(Cs cs, Th taker)}"

  1071   using next_th_taker taker_def waiting_set_eq 

  1072   by fastforce

  1073    

  1074 lemma holding_taker:

  1075   shows "holding (e#s) taker cs"

  1076     by (unfold s_holding_def, fold wq_def, unfold wq_es_cs, 

  1077         auto simp:neq_wq' taker_def)

  1078 

  1079 lemma waiting_esI2:

  1080   assumes "waiting s t cs"

  1081       and "t \<noteq> taker"

  1082   shows "waiting (e#s) t cs" 

  1083 proof -

  1084   have "t \<in> set wq'" 

  1085   proof(unfold wq'_def, rule someI2)

  1086     show "distinct rest \<and> set rest = set rest"

  1087           by (simp add: distinct_rest)

   825     case True

  1089     fix x

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

  1090     assume "distinct x \<and> set x = set rest"

   827     have "next_th s th cs t"

  1091     moreover have "t \<in> set rest"

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

  1092         using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto 

   829     proof -

  1093     ultimately show "t \<in> set x" by simp

   830       fix a list

  1094   qed

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

  1095   moreover have "t \<noteq> hd wq'"

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

  1096     using assms(2) taker_def by auto 

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

  1097   ultimately show ?thesis

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

  1098     by (unfold s_waiting_def, fold wq_def, unfold wq_es_cs, simp)

   835       proof(rule someI2)

  1099 qed

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

  1100 

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

  1101 lemma waiting_esE:

  1102   assumes "waiting (e#s) t c" 

  1103   obtains "c \<noteq> cs" "waiting s t c"

  1104      |    "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'"

  1105 proof(cases "c = cs")

  1106   case False

  1107   hence "wq (e#s) c = wq s c" using is_v by auto

  1108   with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto 

  1109   from that(1)[OF False this] show ?thesis .

  1110 next

  1111   case True

  1112   from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs]

  1113   have "t \<noteq> hd wq'" "t \<in> set wq'" by auto

  1114   hence "t \<noteq> taker" by (simp add: taker_def) 

  1115   moreover hence "t \<noteq> th" using assms neq_t_th by blast 

  1116   moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) 

  1117   ultimately have "waiting s t cs"

  1118     by (metis cs_waiting_def list.distinct(2) list.sel(1) 

  1119                 list.set_sel(2) rest_def waiting_eq wq_s_cs)  

  1120   show ?thesis using that(2)

  1121   using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto   

  1122 qed

  1123 

  1124 lemma holding_esI1:

  1125   assumes "c = cs"

  1126   and "t = taker"

  1127   shows "holding (e#s) t c"

  1128   by (unfold assms, simp add: holding_taker)

  1129 

  1130 lemma holding_esE:

  1131   assumes "holding (e#s) t c" 

  1132   obtains "c = cs" "t = taker"

  1133       | "c \<noteq> cs" "holding s t c"

  1134 proof(cases "c = cs")

  1135   case True

  1136   from assms[unfolded True, unfolded s_holding_def, 

  1137              folded wq_def, unfolded wq_es_cs]

  1138   have "t = taker" by (simp add: taker_def) 

  1139   from that(1)[OF True this] show ?thesis .

  1140 next

  1141   case False

  1142   hence "wq (e#s) c = wq s c" using is_v by auto

  1143   from assms[unfolded s_holding_def, folded wq_def, 

  1144              unfolded this, unfolded wq_def, folded s_holding_def]

  1145   have "holding s t c"  .

  1146   from that(2)[OF False this] show ?thesis .

  1147 qed

  1148 

  1149 end 

  1150 

  1151 locale valid_trace_v_e = valid_trace_v +

  1152   assumes rest_nil: "rest = []"

  1153 begin

  1154 

  1155 lemma nil_wq': "wq' = []" 

  1156 proof (unfold wq'_def, rule someI2)

  1157   show "distinct rest \<and> set rest = set rest"

  1158     by (simp add: distinct_rest) 

  1159 next

  1160   fix x

  1161   assume " distinct x \<and> set x = set rest" 

  1162   thus "x = []" using rest_nil by auto

  1163 qed 

  1164 

  1165 lemma no_taker: 

  1166   assumes "next_th s th cs taker"

  1167   shows "False"

  1168 proof -

  1169   from assms[unfolded next_th_def]

  1170   obtain rest' where "wq s cs = th # rest'" "rest' \<noteq> []"

  1171     by auto

  1172   thus ?thesis using rest_def rest_nil by auto 

  1173 qed

  1174 

  1175 lemma waiting_set_eq:

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

  1177   using no_taker by auto

  1178 

  1179 lemma holding_set_eq:

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

  1181   using no_taker by auto

  1182    

  1183 lemma no_holding:

  1184   assumes "holding (e#s) taker cs"

  1185   shows False

  1186 proof -

  1187   from wq_es_cs[unfolded nil_wq']

  1188   have " wq (e # s) cs = []" .

  1189   from assms[unfolded s_holding_def, folded wq_def, unfolded this]

  1190   show ?thesis by auto

  1191 qed

  1192 

  1193 lemma no_waiting:

  1194   assumes "waiting (e#s) t cs"

  1195   shows False

  1196 proof -

  1197   from wq_es_cs[unfolded nil_wq']

  1198   have " wq (e # s) cs = []" .

  1199   from assms[unfolded s_waiting_def, folded wq_def, unfolded this]

  1200   show ?thesis by auto

  1201 qed

  1202 

  1203 lemma waiting_esE:

  1204   assumes "waiting (e#s) t c" 

  1205   obtains "c \<noteq> cs" "waiting s t c"

  1206 proof(cases "c = cs")

  1207   case False

  1208   hence "wq (e#s) c = wq s c" using is_v by auto

  1209   with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto 

  1210   from that(1)[OF False this] show ?thesis .

  1211 next

  1212   case True

  1213   from no_waiting[OF assms[unfolded True]]

  1214   show ?thesis by auto

  1215 qed

  1216 

  1217 lemma holding_esE:

  1218   assumes "holding (e#s) t c" 

  1219   obtains "c \<noteq> cs" "holding s t c"

  1220 proof(cases "c = cs")

  1221   case True

  1222   from no_holding[OF assms[unfolded True]] 

  1223   show ?thesis by auto

  1224 next

  1225   case False

  1226   hence "wq (e#s) c = wq s c" using is_v by auto

  1227   from assms[unfolded s_holding_def, folded wq_def, 

  1228              unfolded this, unfolded wq_def, folded s_holding_def]

  1229   have "holding s t c"  .

  1230   from that[OF False this] show ?thesis .

  1231 qed

  1232 

  1233 end (* ccc *)

  1234 

  1235 lemma rel_eqI:

  1236   assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"

  1237   and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"

  1238   shows "A = B"

  1239   using assms by auto

  1240 

  1241 lemma in_RAG_E:

  1242   assumes "(n1, n2) \<in> RAG (s::state)"

  1243   obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"

  1244       | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"

  1245   using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]

  1246   by auto

  1247   

  1248 context valid_trace_v

  1249 begin

  1250 

  1251 lemma

  1252   "RAG (e # s) =

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

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

  1255      {(Cs cs, Th th') |th'.  next_th s th cs th'}" (is "?L = ?R")

  1256 proof(rule rel_eqI)

  1257   fix n1 n2

  1258   assume "(n1, n2) \<in> ?L"

  1259   thus "(n1, n2) \<in> ?R"

  1260   proof(cases rule:in_RAG_E)

  1261     case (waiting th' cs')

  1262     show ?thesis

  1263     proof(cases "rest = []")

  1264       case False

  1265       interpret h_n: valid_trace_v_n s e th cs

  1266         by (unfold_locales, insert False, simp)

  1267       from waiting(3)

  1268       show ?thesis

  1269       proof(cases rule:h_n.waiting_esE)

  1270         case 1

  1271         with waiting(1,2)

  1272         show ?thesis

  1273         by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 

  1274              fold waiting_eq, auto)

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

  1276         case 2

   840           by auto

  1277         with waiting(1,2)

   841       qed

  1278         show ?thesis

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

  1279          by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 

   843     next

  1280              fold waiting_eq, auto)

   844       fix a list

  1281       qed

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

  1282     next

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

  1283       case True

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

  1284       interpret h_e: valid_trace_v_e s e th cs

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

  1285         by (unfold_locales, insert True, simp)

   849       proof(rule someI2)

  1286       from waiting(3)

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

  1287       show ?thesis

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

  1288       proof(cases rule:h_e.waiting_esE)

  1289         case 1

  1290         with waiting(1,2)

  1291         show ?thesis

  1292         by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, 

  1293              fold waiting_eq, auto)

  1294       qed

  1295     qed

  1296   next

  1297     case (holding th' cs')

  1298     show ?thesis

  1299     proof(cases "rest = []")

  1300       case False

  1301       interpret h_n: valid_trace_v_n s e th cs

  1302         by (unfold_locales, insert False, simp)

  1303       from holding(3)

  1304       show ?thesis

  1305       proof(cases rule:h_n.holding_esE)

  1306         case 1

  1307         with holding(1,2)

  1308         show ?thesis

  1309         by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 

  1310              fold waiting_eq, auto)

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

  1312         case 2

   854           by auto

  1313         with holding(1,2)

   855       qed

  1314         show ?thesis

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

  1315          by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 

   857     next

  1316              fold holding_eq, auto)

   858       fix a list

  1317       qed

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

  1318     next

   860       from step_back_step[OF vt]

  1319       case True

   861       show "a = th"

  1320       interpret h_e: valid_trace_v_e s e th cs

   862       proof(cases)

  1321         by (unfold_locales, insert True, simp)

   863         assume "holding s th cs"

  1322       from holding(3)

   864         with eq_wq show ?thesis

  1323       show ?thesis

   865           by (unfold s_holding_def wq_def, auto)

  1324       proof(cases rule:h_e.holding_esE)

   866       qed

  1325         case 1

   867     qed

  1326         with holding(1,2)

   868     with True show ?thesis by simp

  1327         show ?thesis

   869   qed

  1328         by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, 

   870 qed

  1329              fold holding_eq, auto)

   871 

  1330       qed

   872 lemma step_v_not_wait[consumes 3]:

  1331     qed

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

  1332   qed

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

  1333 next

   875 

  1334   fix n1 n2

   876 lemma step_v_release:

  1335   assume h: "(n1, n2) \<in> ?R"

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

  1336   show "(n1, n2) \<in> ?L"

   878 proof -

  1337   proof(cases "rest = []")

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

  1338     case False

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

  1339     interpret h_n: valid_trace_v_n s e th cs

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

  1340         by (unfold_locales, insert False, simp)

   882     by (cases, unfold_locales, simp+)

  1341     from h[unfolded h_n.waiting_set_eq h_n.holding_set_eq]

   883   from step_back_step [OF vt] and hd

  1342     have "((n1, n2) \<in> RAG s \<and> (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th)

   884   show "False"

  1343                             \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)) \<or> 

   885   proof(cases)

  1344           (n2 = Th h_n.taker \<and> n1 = Cs cs)" 

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

  1345       by auto

  1346    thus ?thesis

  1347    proof

  1348       assume "n2 = Th h_n.taker \<and> n1 = Cs cs"

  1349       with h_n.holding_taker

  1350       show ?thesis 

  1351         by (unfold s_RAG_def, fold holding_eq, auto)

  1352    next

  1353     assume h: "(n1, n2) \<in> RAG s \<and>

  1354         (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)"

  1355     hence "(n1, n2) \<in> RAG s" by simp