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

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

   514 context valid_trace_p (* ccc *)

   601 context valid_trace_p 

   721 text {*

   747 lemma wq_out_inv: 

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

   748   assumes s_in: "thread \<in> set (wq s cs)"

   723   operation can add new thread into waiting queues. 

   749   and s_hd: "thread = hd (wq s cs)"

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

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

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

   751   shows "e = V thread cs"

   726 *}

   752 proof(cases e)

   753 -- {* There are only two non-trivial cases: *}

   754   case (V th cs1)

   755   show ?thesis

   756   proof(cases "cs1 = cs")

   757     case True

   758     have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] .

   759     thus ?thesis

   760     proof(cases)

   761       case (thread_V)

   762       moreover have "th = thread" using thread_V(2) s_hd

   763           by (unfold s_holding_def wq_def, simp)

   764       ultimately show ?thesis using V True by simp

   765     qed

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

   767 next

   768   case (P th cs1)

   769   show ?thesis

   770   proof(cases "cs1 = cs")

   771     case True

   772     with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]"

   773       by (auto simp:wq_def Let_def split:if_splits)

   774     with s_i s_hd s_in have False

   775       by (metis empty_iff hd_append2 list.set(1) wq_def) 

   776     thus ?thesis by simp

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

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

   758 lemma wq_out_inv: (* ccc *)

   810 end

   759   assumes s_in: "thread \<in> set (wq s cs)"

   811 

   760   and s_hd: "thread = hd (wq s cs)"

   812 lemma (in valid_trace_create)

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

   813   th_not_in_threads: "th \<notin> threads s"

   762   shows "e = V thread cs"

   814 proof -

   763 proof(cases e)

   815   from pip_e[unfolded is_create]

   764 -- {* There are only two non-trivial cases: *}

   816   show ?thesis by (cases, simp)

   765   case (V th cs1)

   817 qed

   818 

   819 lemma (in valid_trace_create)

   820   threads_es [simp]: "threads (e#s) = threads s \<union> {th}"

   821   by (unfold is_create, simp)

   822 

   823 lemma (in valid_trace_exit)

   824   threads_es [simp]: "threads (e#s) = threads s - {th}"

   825   by (unfold is_exit, simp)

   826 

   827 lemma (in valid_trace_p)

   828   threads_es [simp]: "threads (e#s) = threads s"

   829   by (unfold is_p, simp)

   830 

   831 lemma (in valid_trace_v)

   832   threads_es [simp]: "threads (e#s) = threads s"

   833   by (unfold is_v, simp)

   834 

   835 lemma (in valid_trace_v)

   836   th_not_in_rest[simp]: "th \<notin> set rest"

   837 proof

   838   assume otherwise: "th \<in> set rest"

   839   have "distinct (wq s cs)" by (simp add: wq_distinct)

   840   from this[unfolded wq_s_cs] and otherwise

   841   show False by auto

   842 qed

   843 

   844 lemma (in valid_trace_v) distinct_rest: "distinct rest"

   845   by (simp add: distinct_tl rest_def wq_distinct)

   846 

   847 lemma (in valid_trace_v)

   848   set_wq_es_cs [simp]: "set (wq (e#s) cs) = set (wq s cs) - {th}"

   849 proof(unfold wq_es_cs wq'_def, rule someI2)

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

   851     by (simp add: distinct_rest) 

   852 next

   853   fix x

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

   855   thus "set x = set (wq s cs) - {th}" 

   856       by (unfold wq_s_cs, simp)

   857 qed

   858 

   859 lemma (in valid_trace_exit)

   860   th_not_in_wq: "th \<notin> set (wq s cs)"

   861 proof -

   862   from pip_e[unfolded is_exit]

   767   proof(cases "cs1 = cs")

   864   by (cases, unfold holdents_def s_holding_def, fold wq_def, 

   768     case True

   865              auto elim!:runing_wqE)

   769     have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] .

   866 qed

   770     thus ?thesis

   867 

   771     proof(cases)

   868 lemma (in valid_trace) wq_threads: 

   772       case (thread_V)

   869   assumes "th \<in> set (wq s cs)"

   773       moreover have "th = thread" using thread_V(2) s_hd

   870   shows "th \<in> threads s"

   774           by (unfold s_holding_def wq_def, simp)

   871   using assms

   775       ultimately show ?thesis using V True by simp

   872 proof(induct rule:ind)

   776     qed

   873   case (Nil)

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

   874   thus ?case by (auto simp:wq_def)

   779   case (P th cs1)

   876   case (Cons s e)

   780   show ?thesis

   877   interpret vt_e: valid_trace_e s e using Cons by simp

   781   proof(cases "cs1 = cs")

   878   show ?case

   782     case True

   879   proof(cases e)

   783     with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]"

   880     case (Create th' prio')

   784       by (auto simp:wq_def Let_def split:if_splits)

   881     interpret vt: valid_trace_create s e th' prio'

   785     with s_i s_hd s_in have False

   882       using Create by (unfold_locales, simp)

   786       by (metis empty_iff hd_append2 list.set(1) wq_def) 

   883     show ?thesis

   787     thus ?thesis by simp

   884       using Cons.hyps(2) Cons.prems by auto

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

   885   next

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

   886     case (Exit th')

   790 

   887     interpret vt: valid_trace_exit s e th'

   791 end

   888       using Exit by (unfold_locales, simp)

   792 

   889     show ?thesis

   890       using Cons.hyps(2) Cons.prems vt.th_not_in_wq by auto 

   891   next

   892     case (P th' cs')

   893     interpret vt: valid_trace_p s e th' cs'

   894       using P by (unfold_locales, simp)

   895     show ?thesis

   896       using Cons.hyps(2) Cons.prems readys_threads 

   897         runing_ready vt.is_p vt.runing_th_s vt_e.wq_in_inv 

   898         by fastforce 

   899   next

   900     case (V th' cs')

   901     interpret vt: valid_trace_v s e th' cs'

   902       using V by (unfold_locales, simp)

   903     show ?thesis using Cons

   904       using vt.is_v vt.threads_es vt_e.wq_in_inv by blast

   905   next

   906     case (Set th' prio)

   907     interpret vt: valid_trace_set s e th' prio

   908       using Set by (unfold_locales, simp)

   909     show ?thesis using Cons.hyps(2) Cons.prems vt.is_set 

   910         by (auto simp:wq_def Let_def)

   911   qed

   912 qed 

   913 

   914 section {* RAG and threads *}

   797 

   919 lemma  dm_RAG_threads:

   798 text {* (* ddd *)

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

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

   921   shows "th \<in> threads s"

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

   922 proof -

   801   For instance, the fact 

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

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

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

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

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

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

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

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

   927     by (unfold s_RAG_def, auto simp:cs_waiting_def)

   806 

   928   from wq_threads [OF this] show ?thesis .

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

   929 qed

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

   930 

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

   931 lemma rg_RAG_threads: 

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

   932   assumes "(Th th) \<in> Range (RAG s)"

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

   933   shows "th \<in> threads s"

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

   934   using assms

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

   935   by (unfold s_RAG_def cs_waiting_def cs_holding_def, 

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

   936        auto intro:wq_threads)

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

   937 

   816 

   938 lemma RAG_threads:

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

   939   assumes "(Th th) \<in> Field (RAG s)"

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

   940   shows "th \<in> threads s"

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

   941   using assms

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

   942   by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)

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

   943 

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

   944 end

   823   and kept on blocked on them respectively ever since.

   945 

   824  

   946 section {* The change of @{term RAG} *}

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

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

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

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

   829 *}

   830 

   831 lemma waiting_unique_pre: (* ddd *)

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

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

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

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

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

   837   shows "False"

   838 proof -

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

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

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

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

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

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

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

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

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

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

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

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

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

   852   { fix s cs

   853     assume q: "?Q cs s"

   854     have "thread \<notin> runing s"

   855     proof

   856       assume "thread \<in> runing s"

   857       hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and> 

   858                  thread \<noteq> hd (wq_fun (schs s) cs))"

   859         by (unfold runing_def s_waiting_def readys_def, auto)

   860       from this[rule_format, of cs] q 

   861       show False by (simp add: wq_def) 

   862     qed

   863   } note q_not_runing = this

   864   { fix t1 t2 cs1 cs2

   865     assume  lt1: "t1 < length s"

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

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

   868     and lt2: "t2 < length s"

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

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

   871     and lt12: "t1 < t2"

   872     let ?t3 = "Suc t2"

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

   874     from moment_plus [OF this] 

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

   876     have "t2 < ?t3" by simp

   877     from nn2 [rule_format, OF this] and eq_m

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

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

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

   881     proof -

   882       from vt_moment 

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

   884       with eq_m show ?thesis by simp

   885     qed

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

   887         by (unfold_locales, auto, cases, simp)

   888     have ?thesis

   889     proof -

   890       have "thread \<in> runing (moment t2 s)"

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

   892         case True

   893         have "e = V thread cs2"

   894         proof -

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

   896               using True and np2  by auto 

   897           from vt_e.wq_out_inv[OF True this h2]

   898           show ?thesis .

   899         qed

   900         thus ?thesis using vt_e.actor_inv[OF vt_e.pip_e] by auto

   901       next

   902         case False

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

   904         with vt_e.actor_inv[OF vt_e.pip_e]

   905         show ?thesis by auto

   906       qed

   907       moreover have "thread \<notin> runing (moment t2 s)"

   908         by (rule q_not_runing[OF nn1[rule_format, OF lt12]])

   909       ultimately show ?thesis by simp

   910     qed

   911   } note lt_case = this

   912   show ?thesis

   913   proof -

   914     { assume "t1 < t2"

   915       from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this]

   916       have ?thesis .

   917     } moreover {

   918       assume "t2 < t1"

   919       from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this]

   920       have ?thesis .

   921     } moreover {

   922       assume eq_12: "t1 = t2"

   923       let ?t3 = "Suc t2"

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

   925       from moment_plus [OF this] 

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

   927       have lt_2: "t2 < ?t3" by simp

   928       from nn2 [rule_format, OF this] and eq_m

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

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

   931       from nn1[rule_format, OF lt_2[folded eq_12]] eq_m[folded eq_12]

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

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

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

   935       proof -

   936         from vt_moment 

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

   938         with eq_m show ?thesis by simp

   939       qed

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

   941           by (unfold_locales, auto, cases, simp)

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

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

   944         case True

   945         have "e = V thread cs2"

   946         proof -

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

   948               using True and np2  by auto 

   949           from vt_e.wq_out_inv[OF True this h2]

   950           show ?thesis .

   951         qed

   952         thus ?thesis by auto

   953       next

   954         case False

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

   956         thus ?thesis by auto

   957       qed

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

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

   960         case True

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

   962               using True and np1  by auto 

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

   964         have "e = V thread cs1" .

   965         thus ?thesis by auto

   966       next

   967         case False

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

   969         thus ?thesis by auto

   970       qed

   971       ultimately have ?thesis using neq12 by auto

   972     } ultimately show ?thesis using nat_neq_iff by blast 

   973   qed

   974 qed

   975 

   976 text {*

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

   978 *}

   979 

   980 lemma waiting_unique:

   981   assumes "waiting s th cs1"

   982   and "waiting s th cs2"

   983   shows "cs1 = cs2"

   984   using waiting_unique_pre assms

   985   unfolding wq_def s_waiting_def

   986   by auto

   987 

   988 end

   989 

   990 (* not used *)

   991 text {*

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

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

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

   995 *}

   996 lemma held_unique:

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

   998   and "holding s th2 cs"

   999   shows "th1 = th2"

  1000  by (insert assms, unfold s_holding_def, auto)

  1001 

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

  1003   apply (induct s, auto)

  1004   by (case_tac a, auto split:if_splits)

  1005 

  1006 lemma last_set_unique: 

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

  1008           \<Longrightarrow> th1 = th2"

  1009   apply (induct s, auto)

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

  1011 

  1012 lemma preced_unique : 

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

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

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

  1016   shows "th1 = th2"

  1017 proof -

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

  1019   from last_set_unique [OF this th_in1 th_in2]

  1020   show ?thesis .

  1021 qed

  1022                       

  1023 lemma preced_linorder: 

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

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

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

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

  1028 proof -

  1029   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

  1031   thus ?thesis by auto

  1032 qed

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

   954 lemma (in valid_trace_set) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"

  1041 apply (unfold s_RAG_def s_waiting_def wq_def)

   955    by (unfold is_set s_RAG_def s_waiting_def wq_def, simp add:Let_def)

  1042 by (simp add:Let_def)

   956 

  1043 

   957 lemma (in valid_trace_create) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"

  1044 lemma (in valid_trace_set)

   958  by (unfold is_create s_RAG_def s_waiting_def wq_def, simp add:Let_def)

  1045    RAG_unchanged: "(RAG (e # s)) = RAG s"

   959 

  1046    by (unfold is_set RAG_set_unchanged, simp)

   960 lemma (in valid_trace_exit) RAG_unchanged[simp]: "(RAG (e # s)) = RAG s"

  1047 

   961   by (unfold is_exit s_RAG_def s_waiting_def wq_def, simp add:Let_def)

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

  1049 apply (unfold s_RAG_def s_waiting_def wq_def)

  1050 by (simp add:Let_def)

  1051 

  1052 lemma (in valid_trace_create)

  1053    RAG_unchanged: "(RAG (e # s)) = RAG s"

  1054    by (unfold is_create RAG_create_unchanged, simp)

  1055 

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

  1057 apply (unfold s_RAG_def s_waiting_def wq_def)

  1058 by (simp add:Let_def)

  1059 

  1060 lemma (in valid_trace_exit)

  1061    RAG_unchanged: "(RAG (e # s)) = RAG s"

  1062    by (unfold is_exit RAG_exit_unchanged, simp)

  1087   by (metis (mono_tags, lifting) distinct_rest rest_def 

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

  1088       some_eq_ex wq'_def)

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

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

  1568 end

  1458 lemma 

  1569 

  1459   finite_RAG_kept:

  1570 lemma step_RAG_v: 

  1460   assumes "finite (RAG s)"

  1571 assumes vt:

  1461   shows "finite (RAG (e#s))"

  1572   "vt (V th cs#s)"

  1462 proof(cases "rest = []")

  1573 shows "

  1463   case True

  1574   RAG (V th cs # s) =

  1464   interpret vt: valid_trace_v_e using True

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

  1465     by (unfold_locales, simp)

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

  1466   show ?thesis using assms

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

  1467     by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)

  1578 proof -

  1579   interpret vt_v: valid_trace_v s "V th cs"

  1580     using assms step_back_vt by (unfold_locales, auto) 

  1581   show ?thesis using vt_v.RAG_es .

  1582 qed

  1583 

  1584 lemma (in valid_trace_create)

  1585   th_not_in_threads: "th \<notin> threads s"

  1586 proof -

  1587   from pip_e[unfolded is_create]

  1588   show ?thesis by (cases, simp)

  1589 qed

  1590 

  1591 lemma (in valid_trace_create)

  1592   threads_es [simp]: "threads (e#s) = threads s \<union> {th}"

  1593   by (unfold is_create, simp)

  1594 

  1595 lemma (in valid_trace_exit)

  1596   threads_es [simp]: "threads (e#s) = threads s - {th}"

  1597   by (unfold is_exit, simp)

  1598 

  1599 lemma (in valid_trace_p)

  1600   threads_es [simp]: "threads (e#s) = threads s"

  1601   by (unfold is_p, simp)

  1602 

  1603 lemma (in valid_trace_v)

  1604   threads_es [simp]: "threads (e#s) = threads s"

  1605   by (unfold is_v, simp)

  1606 

  1607 lemma (in valid_trace_v)

  1608   th_not_in_rest[simp]: "th \<notin> set rest"

  1609 proof

  1610   assume otherwise: "th \<in> set rest"

  1611   have "distinct (wq s cs)" by (simp add: wq_distinct)

  1612   from this[unfolded wq_s_cs] and otherwise

  1613   show False by auto

  1614 qed

  1615 

  1616 lemma (in valid_trace_v)

  1617   set_wq_es_cs [simp]: "set (wq (e#s) cs) = set (wq s cs) - {th}"

  1618 proof(unfold wq_es_cs wq'_def, rule someI2)

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

  1620     by (simp add: distinct_rest)

  1622   fix x

  1469   case False

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

  1470   interpret vt: valid_trace_v_n using False

  1624   thus "set x = set (wq s cs) - {th}" 

  1471     by (unfold_locales, simp)

  1625       by (unfold wq_s_cs, simp)

  1472   show ?thesis using assms

  1626 qed

  1473     by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)

  1627 

  1474 qed

  1628 lemma (in valid_trace_exit)

  1475 

  1629   th_not_in_wq: "th \<notin> set (wq s cs)"

  1476 end

  1630 proof -

  1631   from pip_e[unfolded is_exit]

  1632   show ?thesis

  1633   by (cases, unfold holdents_def s_holding_def, fold wq_def, 

  1634              auto elim!:runing_wqE)

  1635 qed

  1636 

  1637 lemma (in valid_trace) wq_threads: 

  1638   assumes "th \<in> set (wq s cs)"

  1639   shows "th \<in> threads s"

  1640   using assms

  1641 proof(induct rule:ind)

  1642   case (Nil)

  1643   thus ?case by (auto simp:wq_def)

  1644 next

  1645   case (Cons s e)

  1646   interpret vt_e: valid_trace_e s e using Cons by simp

  1647   show ?case

  1648   proof(cases e)

  1649     case (Create th' prio')

  1650     interpret vt: valid_trace_create s e th' prio'

  1651       using Create by (unfold_locales, simp)

  1652     show ?thesis

  1653       using Cons.hyps(2) Cons.prems by auto

  1654   next

  1655     case (Exit th')

  1656     interpret vt: valid_trace_exit s e th'

  1657       using Exit by (unfold_locales, simp)

  1658     show ?thesis

  1659       using Cons.hyps(2) Cons.prems vt.th_not_in_wq by auto 

  1660   next

  1661     case (P th' cs')

  1662     interpret vt: valid_trace_p s e th' cs'

  1663       using P by (unfold_locales, simp)

  1664     show ?thesis

  1665       using Cons.hyps(2) Cons.prems readys_threads 

  1666         runing_ready vt.is_p vt.runing_th_s vt_e.wq_in_inv 

  1667         by fastforce 

  1668   next

  1669     case (V th' cs')

  1670     interpret vt: valid_trace_v s e th' cs'

  1671       using V by (unfold_locales, simp)

  1672     show ?thesis using Cons

  1673       using vt.is_v vt.threads_es vt_e.wq_in_inv by blast

  1674   next

  1675     case (Set th' prio)

  1676     interpret vt: valid_trace_set s e th' prio

  1677       using Set by (unfold_locales, simp)

  1678     show ?thesis using Cons.hyps(2) Cons.prems vt.is_set 

  1679         by (auto simp:wq_def Let_def)

  1680   qed

  1681 qed 

  1682 

  1683 context valid_trace

  1684 begin

  1685 

  1686 lemma  dm_RAG_threads:

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

  1688   shows "th \<in> threads s"

  1689 proof -

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

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

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

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

  1694     by (unfold s_RAG_def, auto simp:cs_waiting_def)

  1695   from wq_threads [OF this] show ?thesis .

  1696 qed

  1697 

  1698 lemma rg_RAG_threads: 

  1699   assumes "(Th th) \<in> Range (RAG s)"

  1700   shows "th \<in> threads s"

  1701   using assms

  1702   by (unfold s_RAG_def cs_waiting_def cs_holding_def, 

  1703        auto intro:wq_threads)

  1704 

  1705 lemma RAG_threads:

  1706   assumes "(Th th) \<in> Field (RAG s)"

  1707   shows "th \<in> threads s"

  1708   using assms

  1709   by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)

  1710 

  1711 end

  1712 

  1713 lemma (in valid_trace_v)

  1714   preced_es [simp]: "preced th (e#s) = preced th s"

  1715   by (unfold is_v preced_def, simp)

  1716 

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

  1718 proof

  1719   fix th'

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

  1721     by (unfold the_preced_def preced_def, simp)

  1722 qed

  1723 

  1724 lemma (in valid_trace_v)

  1725   the_preced_es: "the_preced (e#s) = the_preced s"

  1726   by (unfold is_v preced_def, simp)

  1752   

  1488 

  1770 

  1506 end 

  1771 end

  1507 

  1772 

  1508 lemma (in valid_trace_p) th_not_waiting: "\<not> waiting s th c"

  1773 

  1509 proof -

  1774 context valid_trace_p_w

  1510   have "th \<in> readys s"

  1775 begin

  1511     using runing_ready runing_th_s by blast 

  1776 

  1512   thus ?thesis

  1777 lemma wq_s_cs: "wq s cs = holder#waiters"

  1513     by (unfold readys_def, auto)

  1778     by (simp add: holder_def waiters_def wne)

  1514 qed

  1779     

  1780 lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]"

  1781   by (simp add: wq_es_cs wq_s_cs)

  1782 

  1783 lemma waiting_es_th_cs: "waiting (e#s) th cs"

  1784   using cs_waiting_def th_not_in_wq waiting_eq wq_es_cs' wq_s_cs by auto

  1785 

  1786 lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"

  1787    by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto)

  1788 

  1789 lemma holding_esE:

  1790   assumes "holding (e#s) th' cs'"

  1791   obtains "holding s th' cs'"

  1792   using assms 

  1793 proof(cases "cs' = cs")

  1794   case False

  1795   hence "wq (e#s) cs' = wq s cs'" by simp

  1796   with assms show ?thesis

  1797     using cs_holding_def holding_eq that by auto 

  1798 next

  1799   case True

  1800   with assms show ?thesis

  1801   by (metis cs_holding_def holding_eq list.sel(1) list.set_intros(1) that 

  1802         wq_es_cs' wq_s_cs) 

  1803 qed

  1804 

  1805 lemma waiting_esE:

  1806   assumes "waiting (e#s) th' cs'"

  1807   obtains "th' \<noteq> th" "waiting s th' cs'"

  1808      |  "th' = th" "cs' = cs"

  1809 proof(cases "waiting s th' cs'")

  1810   case True

  1811   have "th' \<noteq> th"

  1812   proof

  1813     assume otherwise: "th' = th"

  1814     from True[unfolded this]

  1815     show False by (simp add: th_not_waiting) 

  1816   qed

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

  1818 next

  1819   case False

  1820   hence "th' = th \<and> cs' = cs"

  1821       by (metis assms cs_waiting_def holder_def list.sel(1) rotate1.simps(2) 

  1822         set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp)

  1823   with that(2) show ?thesis by metis

  1824 qed

  1825 

  1826 lemma RAG_es: "RAG (e # s) =  RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R")

  1827 proof(rule rel_eqI)

  1828   fix n1 n2

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

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

  1831   proof(cases rule:in_RAG_E)

  1832     case (waiting th' cs')

  1833     from this(3)

  1834     show ?thesis

  1835     proof(cases rule:waiting_esE)

  1836       case 1

  1837       thus ?thesis using waiting(1,2)

  1838         by (unfold s_RAG_def, fold waiting_eq, auto)

  1839     next

  1840       case 2

  1841       thus ?thesis using waiting(1,2) by auto

  1842     qed

  1843   next

  1844     case (holding th' cs')

  1845     from this(3)

  1846     show ?thesis

  1847     proof(cases rule:holding_esE)

  1848       case 1

  1849       with holding(1,2)

  1850       show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)

  1851     qed

  1852   qed

  1853 next

  1854   fix n1 n2

  1855   assume "(n1, n2) \<in> ?R"

  1856   hence "(n1, n2) \<in> RAG s \<or> (n1 = Th th \<and> n2 = Cs cs)" by auto

  1857   thus "(n1, n2) \<in> ?L"

  1858   proof

  1859     assume "(n1, n2) \<in> RAG s"

  1860     thus ?thesis

  1861     proof(cases rule:in_RAG_E)

  1862       case (waiting th' cs')

  1863       from waiting_kept[OF this(3)]

  1864       show ?thesis using waiting(1,2)

  1865          by (unfold s_RAG_def, fold waiting_eq, auto)

  1866     next

  1867       case (holding th' cs')

  1868       from holding_kept[OF this(3)]

  1869       show ?thesis using holding(1,2)

  1870          by (unfold s_RAG_def, fold holding_eq, auto)

  1871     qed

  1872   next

  1873     assume "n1 = Th th \<and> n2 = Cs cs"

  1874     thus ?thesis using RAG_edge by auto

  1875   qed

  1876 qed

  1877 

  1878 end