1 theory CpsG

     2 imports PIPDefs

     3 begin

     4 

     5 lemma Max_fg_mono:

     6   assumes "finite A"

     7   and "\<forall> a \<in> A. f a \<le> g a"

     8   shows "Max (f ` A) \<le> Max (g ` A)"

     9 proof(cases "A = {}")

    10   case True

    11   thus ?thesis by auto

    12 next

    13   case False

    14   show ?thesis

    15   proof(rule Max.boundedI)

    16     from assms show "finite (f ` A)" by auto

    17   next

    18     from False show "f ` A \<noteq> {}" by auto

    19   next

    20     fix fa

    21     assume "fa \<in> f ` A"

    22     then obtain a where h_fa: "a \<in> A" "fa = f a" by auto

    23     show "fa \<le> Max (g ` A)"

    24     proof(rule Max_ge_iff[THEN iffD2])

    25       from assms show "finite (g ` A)" by auto

    26     next

    27       from False show "g ` A \<noteq> {}" by auto

    28     next

    29       from h_fa have "g a \<in> g ` A" by auto

    30       moreover have "fa \<le> g a" using h_fa assms(2) by auto

    31       ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto

    32     qed

    33   qed

    34 qed 

    35 

    36 lemma Max_f_mono:

    37   assumes seq: "A \<subseteq> B"

    38   and np: "A \<noteq> {}"

    39   and fnt: "finite B"

    40   shows "Max (f ` A) \<le> Max (f ` B)"

    41 proof(rule Max_mono)

    42   from seq show "f ` A \<subseteq> f ` B" by auto

    43 next

    44   from np show "f ` A \<noteq> {}" by auto

    45 next

    46   from fnt and seq show "finite (f ` B)" by auto

    47 qed

    48 

    49 lemma eq_RAG: 

    50   "RAG (wq s) = RAG s"

    51   by (unfold cs_RAG_def s_RAG_def, auto)

    52 

    53 lemma waiting_holding:

    54   assumes "waiting (s::state) th cs"

    55   obtains th' where "holding s th' cs"

    56 proof -

    57   from assms[unfolded s_waiting_def, folded wq_def]

    58   obtain th' where "th' \<in> set (wq s cs)" "th' = hd (wq s cs)"

    59     by (metis empty_iff hd_in_set list.set(1))

    60   hence "holding s th' cs" 

    61     by (unfold s_holding_def, fold wq_def, auto)

    62   from that[OF this] show ?thesis .

    63 qed

    64 

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

    66 unfolding cp_def wq_def

    67 apply(induct s rule: schs.induct)

    68 apply(simp add: Let_def cpreced_initial)

    69 apply(simp add: Let_def)

    70 apply(simp add: Let_def)

    71 apply(simp add: Let_def)

    72 apply(subst (2) schs.simps)

    73 apply(simp add: Let_def)

    74 apply(subst (2) schs.simps)

    75 apply(simp add: Let_def)

    76 done

    77 

    78 lemma cp_alt_def:

    79   "cp s th =  

    80            Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"

    81 proof -

    82   have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =

    83         Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 

    84           (is "Max (_ ` ?L) = Max (_ ` ?R)")

    85   proof -

    86     have "?L = ?R" 

    87     by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)

    88     thus ?thesis by simp

    89   qed

    90   thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)

    91 qed

    92 

    93 (* ccc *)

    94 

    95 

    96 locale valid_trace = 

    97   fixes s

    98   assumes vt : "vt s"

    99 

   100 locale valid_trace_e = valid_trace +

   101   fixes e

   102   assumes vt_e: "vt (e#s)"

   103 begin

   104 

   105 lemma pip_e: "PIP s e"

   106   using vt_e by (cases, simp)  

   107 

   108 end

   109 

   110 locale valid_trace_create = valid_trace_e + 

   111   fixes th prio

   112   assumes is_create: "e = Create th prio"

   113 

   114 locale valid_trace_exit = valid_trace_e + 

   115   fixes th

   116   assumes is_exit: "e = Exit th"

   117 

   118 locale valid_trace_p = valid_trace_e + 

   119   fixes th cs

   120   assumes is_p: "e = P th cs"

   121 

   122 locale valid_trace_v = valid_trace_e + 

   123   fixes th cs

   124   assumes is_v: "e = V th cs"

   125 begin

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

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

   128 end

   129 

   130 locale valid_trace_v_n = valid_trace_v +

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

   132 

   133 locale valid_trace_v_e = valid_trace_v +

   134   assumes rest_nil: "rest = []"

   135 

   136 locale valid_trace_set= valid_trace_e + 

   137   fixes th prio

   138   assumes is_set: "e = Set th prio"

   139 

   140 context valid_trace

   141 begin

   142 

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

   144   assumes "PP []"

   145      and "(\<And>s e. valid_trace_e s e \<Longrightarrow>

   146                    PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"

   147      shows "PP s"

   148 proof(induct rule:vt.induct[OF vt, case_names Init Step])

   149   case Init

   150   from assms(1) show ?case .

   151 next

   152   case (Step s e)

   153   show ?case

   154   proof(rule assms(2))

   155     show "valid_trace_e s e" using Step by (unfold_locales, auto)

   156   next

   157     show "PP s" using Step by simp

   158   next

   159     show "PIP s e" using Step by simp

   160   qed

   161 qed

   162 

   163 lemma  vt_moment: "\<And> t. vt (moment t s)"

   164 proof(induct rule:ind)

   165   case Nil

   166   thus ?case by (simp add:vt_nil)

   167 next

   168   case (Cons s e t)

   169   show ?case

   170   proof(cases "t \<ge> length (e#s)")

   171     case True

   172     from True have "moment t (e#s) = e#s" by simp

   173     thus ?thesis using Cons

   174       by (simp add:valid_trace_def valid_trace_e_def, auto)

   175   next

   176     case False

   177     from Cons have "vt (moment t s)" by simp

   178     moreover have "moment t (e#s) = moment t s"

   179     proof -

   180       from False have "t \<le> length s" by simp

   181       from moment_app [OF this, of "[e]"] 

   182       show ?thesis by simp

   183     qed

   184     ultimately show ?thesis by simp

   185   qed

   186 qed

   187 

   188 lemma finite_threads:

   189   shows "finite (threads s)"

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

   191 

   192 end

   193 

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

   195   by (unfold s_RAG_def, auto)

   196 

   197 locale valid_moment = valid_trace + 

   198   fixes i :: nat

   199 

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

   201   by (unfold_locales, insert vt_moment, auto)

   202 

   203 lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"

   204   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)

   205 

   206 lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"

   207   by (unfold s_holding_def wq_def cs_holding_def, simp)

   208 

   209 lemma runing_ready: 

   210   shows "runing s \<subseteq> readys s"

   211   unfolding runing_def readys_def

   212   by auto 

   213 

   214 lemma readys_threads:

   215   shows "readys s \<subseteq> threads s"

   216   unfolding readys_def

   217   by auto

   218 

   219 lemma wq_v_neq [simp]:

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

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

   222 

   223 lemma runing_head:

   224   assumes "th \<in> runing s"

   225   and "th \<in> set (wq_fun (schs s) cs)"

   226   shows "th = hd (wq_fun (schs s) cs)"

   227   using assms

   228   by (simp add:runing_def readys_def s_waiting_def wq_def)

   229 

   230 context valid_trace

   231 begin

   232 

   233 lemma runing_wqE:

   234   assumes "th \<in> runing s"

   235   and "th \<in> set (wq s cs)"

   236   obtains rest where "wq s cs = th#rest"

   237 proof -

   238   from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest"

   239     by (meson list.set_cases)

   240   have "th' = th"

   241   proof(rule ccontr)

   242     assume "th' \<noteq> th"

   243     hence "th \<noteq> hd (wq s cs)" using eq_wq by auto 

   244     with assms(2)

   245     have "waiting s th cs" 

   246       by (unfold s_waiting_def, fold wq_def, auto)

   247     with assms show False 

   248       by (unfold runing_def readys_def, auto)

   249   qed

   250   with eq_wq that show ?thesis by metis

   251 qed

   252 

   253 end

   254 

   255 context valid_trace_create

   256 begin

   257 

   258 lemma wq_neq_simp [simp]:

   259   shows "wq (e#s) cs' = wq s cs'"

   260     using assms unfolding is_create wq_def

   261   by (auto simp:Let_def)

   262 

   263 lemma wq_distinct_kept:

   264   assumes "distinct (wq s cs')"

   265   shows "distinct (wq (e#s) cs')"

   266   using assms by simp

   267 end

   268 

   269 context valid_trace_exit

   270 begin

   271 

   272 lemma wq_neq_simp [simp]:

   273   shows "wq (e#s) cs' = wq s cs'"

   274     using assms unfolding is_exit wq_def

   275   by (auto simp:Let_def)

   276 

   277 lemma wq_distinct_kept:

   278   assumes "distinct (wq s cs')"

   279   shows "distinct (wq (e#s) cs')"

   280   using assms by simp

   281 end

   282 

   283 context valid_trace_p

   284 begin

   285 

   286 lemma wq_neq_simp [simp]:

   287   assumes "cs' \<noteq> cs"

   288   shows "wq (e#s) cs' = wq s cs'"

   289     using assms unfolding is_p wq_def

   290   by (auto simp:Let_def)

   291 

   292 lemma runing_th_s:

   293   shows "th \<in> runing s"

   294 proof -

   295   from pip_e[unfolded is_p]

   296   show ?thesis by (cases, simp)

   297 qed

   298 

   299 lemma ready_th_s: "th \<in> readys s"

   300   using runing_th_s

   301   by (unfold runing_def, auto)

   302 

   303 lemma live_th_s: "th \<in> threads s"

   304   using readys_threads ready_th_s by auto

   305 

   306 lemma live_th_es: "th \<in> threads (e#s)"

   307   using live_th_s 

   308   by (unfold is_p, simp)

   309 

   310 lemma th_not_waiting: 

   311   "\<not> waiting s th c"

   312 proof -

   313   have "th \<in> readys s"

   314     using runing_ready runing_th_s by blast 

   315   thus ?thesis

   316     by (unfold readys_def, auto)

   317 qed

   318 

   319 lemma waiting_neq_th: 

   320   assumes "waiting s t c"

   321   shows "t \<noteq> th"

   322   using assms using th_not_waiting by blast 

   323 

   324 lemma th_not_in_wq: 

   325   shows "th \<notin> set (wq s cs)"

   326 proof

   327   assume otherwise: "th \<in> set (wq s cs)"

   328   from runing_wqE[OF runing_th_s this]

   329   obtain rest where eq_wq: "wq s cs = th#rest" by blast

   330   with otherwise

   331   have "holding s th cs"

   332     by (unfold s_holding_def, fold wq_def, simp)

   333   hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s"

   334     by (unfold s_RAG_def, fold holding_eq, auto)

   335   from pip_e[unfolded is_p]

   336   show False

   337   proof(cases)

   338     case (thread_P)

   339     with cs_th_RAG show ?thesis by auto

   340   qed

   341 qed

   342 

   343 lemma wq_es_cs: 

   344   "wq (e#s) cs =  wq s cs @ [th]"

   345   by (unfold is_p wq_def, auto simp:Let_def)

   346 

   347 lemma wq_distinct_kept:

   348   assumes "distinct (wq s cs')"

   349   shows "distinct (wq (e#s) cs')"

   350 proof(cases "cs' = cs")

   351   case True

   352   show ?thesis using True assms th_not_in_wq

   353     by (unfold True wq_es_cs, auto)

   354 qed (insert assms, simp)

   355 

   356 end

   357 

   358 context valid_trace_v

   359 begin

   360 

   361 lemma wq_neq_simp [simp]:

   362   assumes "cs' \<noteq> cs"

   363   shows "wq (e#s) cs' = wq s cs'"

   364     using assms unfolding is_v wq_def

   365   by (auto simp:Let_def)

   366 

   367 lemma runing_th_s:

   368   shows "th \<in> runing s"

   369 proof -

   370   from pip_e[unfolded is_v]

   371   show ?thesis by (cases, simp)

   372 qed

   373 

   374 lemma th_not_waiting: 

   375   "\<not> waiting s th c"

   376 proof -

   377   have "th \<in> readys s"

   378     using runing_ready runing_th_s by blast 

   379   thus ?thesis

   380     by (unfold readys_def, auto)

   381 qed

   382 

   383 lemma waiting_neq_th: 

   384   assumes "waiting s t c"

   385   shows "t \<noteq> th"

   386   using assms using th_not_waiting by blast 

   387 

   388 lemma wq_s_cs:

   389   "wq s cs = th#rest"

   390 proof -

   391   from pip_e[unfolded is_v]

   392   show ?thesis

   393   proof(cases)

   394     case (thread_V)

   395     from this(2) show ?thesis

   396       by (unfold rest_def s_holding_def, fold wq_def,

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

   398   qed

   399 qed

   400 

   401 lemma wq_es_cs:

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

   403  using wq_s_cs[unfolded wq_def]

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

   405 

   406 lemma wq_distinct_kept:

   407   assumes "distinct (wq s cs')"

   408   shows "distinct (wq (e#s) cs')"

   409 proof(cases "cs' = cs")

   410   case True

   411   show ?thesis

   412   proof(unfold True wq_es_cs wq'_def, rule someI2)

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

   414         using assms[unfolded True wq_s_cs] by auto

   415   qed simp

   416 qed (insert assms, simp)

   417 

   418 end

   419 

   420 context valid_trace_set

   421 begin

   422 

   423 lemma wq_neq_simp [simp]:

   424   shows "wq (e#s) cs' = wq s cs'"

   425     using assms unfolding is_set wq_def

   426   by (auto simp:Let_def)

   427 

   428 lemma wq_distinct_kept:

   429   assumes "distinct (wq s cs')"

   430   shows "distinct (wq (e#s) cs')"

   431   using assms by simp

   432 end

   433 

   434 context valid_trace

   435 begin

   436 

   437 lemma actor_inv: 

   438   assumes "PIP s e"

   439   and "\<not> isCreate e"

   440   shows "actor e \<in> runing s"

   441   using assms

   442   by (induct, auto)

   443 

   444 lemma isP_E:

   445   assumes "isP e"

   446   obtains cs where "e = P (actor e) cs"

   447   using assms by (cases e, auto)

   448 

   449 lemma isV_E:

   450   assumes "isV e"

   451   obtains cs where "e = V (actor e) cs"

   452   using assms by (cases e, auto) 

   453 

   454 lemma wq_distinct: "distinct (wq s cs)"

   455 proof(induct rule:ind)

   456   case (Cons s e)

   457   interpret vt_e: valid_trace_e s e using Cons by simp

   458   show ?case 

   459   proof(cases e)

   460     case (Create th prio)

   461     interpret vt_create: valid_trace_create s e th prio 

   462       using Create by (unfold_locales, simp)

   463     show ?thesis using Cons by (simp add: vt_create.wq_distinct_kept) 

   464   next

   465     case (Exit th)

   466     interpret vt_exit: valid_trace_exit s e th  

   467         using Exit by (unfold_locales, simp)

   468     show ?thesis using Cons by (simp add: vt_exit.wq_distinct_kept) 

   469   next

   470     case (P th cs)

   471     interpret vt_p: valid_trace_p s e th cs using P by (unfold_locales, simp)

   472     show ?thesis using Cons by (simp add: vt_p.wq_distinct_kept) 

   473   next

   474     case (V th cs)

   475     interpret vt_v: valid_trace_v s e th cs using V by (unfold_locales, simp)

   476     show ?thesis using Cons by (simp add: vt_v.wq_distinct_kept) 

   477   next

   478     case (Set th prio)

   479     interpret vt_set: valid_trace_set s e th prio

   480         using Set by (unfold_locales, simp)

   481     show ?thesis using Cons by (simp add: vt_set.wq_distinct_kept) 

   482   qed

   483 qed (unfold wq_def Let_def, simp)

   484 

   485 end

   486 

   487 context valid_trace_e

   488 begin

   489 

   490 text {*

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

   492   operation can add new thread into waiting queues. 

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

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

   495 *}

   496 

   497 lemma wq_in_inv: 

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

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

   500   shows "e = P thread cs"

   501 proof(cases e)

   502   -- {* This is the only non-trivial case: *}

   503   case (V th cs1)

   504   have False

   505   proof(cases "cs1 = cs")

   506     case True

   507     show ?thesis

   508     proof(cases "(wq s cs1)")

   509       case (Cons w_hd w_tl)

   510       have "set (wq (e#s) cs) \<subseteq> set (wq s cs)"

   511       proof -

   512         have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)"

   513           using  Cons V by (auto simp:wq_def Let_def True split:if_splits)

   514         moreover have "set ... \<subseteq> set (wq s cs)"

   515         proof(rule someI2)

   516           show "distinct w_tl \<and> set w_tl = set w_tl"

   517             by (metis distinct.simps(2) local.Cons wq_distinct)

   518         qed (insert Cons True, auto)

   519         ultimately show ?thesis by simp

   520       qed

   521       with assms show ?thesis by auto

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

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

   524   thus ?thesis by auto

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

   526 

   527 lemma wq_out_inv: 

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

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

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

   531   shows "e = V thread cs"

   532 proof(cases e)

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

   534   case (V th cs1)

   535   show ?thesis

   536   proof(cases "cs1 = cs")

   537     case True

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

   539     thus ?thesis

   540     proof(cases)

   541       case (thread_V)

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

   543           by (unfold s_holding_def wq_def, simp)

   544       ultimately show ?thesis using V True by simp

   545     qed

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

   547 next

   548   case (P th cs1)

   549   show ?thesis

   550   proof(cases "cs1 = cs")

   551     case True

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

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

   554     with s_i s_hd s_in have False

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

   556     thus ?thesis by simp

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

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

   559 

   560 end

   561 

   562 

   563 context valid_trace

   564 begin

   565 

   566 

   567 text {* (* ddd *)

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

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

   570   For instance, the fact 

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

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

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

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

   575 

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

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

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

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

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

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

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

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

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

   585 

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

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

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

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

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

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

   592   and kept on blocked on them respectively ever since.

   593  

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

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

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

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

   598 *}

   599 

   600 lemma waiting_unique_pre: (* ddd *)

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

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

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

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

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

   606   shows "False"

   607 proof -

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

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

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

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

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

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

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

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

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

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

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

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

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

   621   { fix s cs

   622     assume q: "?Q cs s"

   623     have "thread \<notin> runing s"

   624     proof

   625       assume "thread \<in> runing s"

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

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

   628         by (unfold runing_def s_waiting_def readys_def, auto)

   629       from this[rule_format, of cs] q 

   630       show False by (simp add: wq_def) 

   631     qed

   632   } note q_not_runing = this

   633   { fix t1 t2 cs1 cs2

   634     assume  lt1: "t1 < length s"

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

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

   637     and lt2: "t2 < length s"

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

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

   640     and lt12: "t1 < t2"

   641     let ?t3 = "Suc t2"

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

   643     from moment_plus [OF this] 

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

   645     have "t2 < ?t3" by simp

   646     from nn2 [rule_format, OF this] and eq_m

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

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

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

   650     proof -

   651       from vt_moment 

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

   653       with eq_m show ?thesis by simp

   654     qed

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

   656         by (unfold_locales, auto, cases, simp)

   657     have ?thesis

   658     proof -

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

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

   661         case True

   662         have "e = V thread cs2"

   663         proof -

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

   665               using True and np2  by auto 

   666           from vt_e.wq_out_inv[OF True this h2]

   667           show ?thesis .

   668         qed

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

   670       next

   671         case False

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

   673         with vt_e.actor_inv[OF vt_e.pip_e]

   674         show ?thesis by auto

   675       qed

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

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

   678       ultimately show ?thesis by simp

   679     qed

   680   } note lt_case = this

   681   show ?thesis

   682   proof -

   683     { assume "t1 < t2"

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

   685       have ?thesis .

   686     } moreover {

   687       assume "t2 < t1"

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

   689       have ?thesis .

   690     } moreover {

   691       assume eq_12: "t1 = t2"

   692       let ?t3 = "Suc t2"

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

   694       from moment_plus [OF this] 

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

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

   697       from nn2 [rule_format, OF this] and eq_m

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

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

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

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

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

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

   704       proof -

   705         from vt_moment 

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

   707         with eq_m show ?thesis by simp

   708       qed

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

   710           by (unfold_locales, auto, cases, simp)

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

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

   713         case True

   714         have "e = V thread cs2"

   715         proof -

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

   717               using True and np2  by auto 

   718           from vt_e.wq_out_inv[OF True this h2]

   719           show ?thesis .

   720         qed

   721         thus ?thesis by auto

   722       next

   723         case False

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

   725         thus ?thesis by auto

   726       qed

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

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

   729         case True

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

   731               using True and np1  by auto 

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

   733         have "e = V thread cs1" .

   734         thus ?thesis by auto

   735       next

   736         case False

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

   738         thus ?thesis by auto

   739       qed

   740       ultimately have ?thesis using neq12 by auto

   741     } ultimately show ?thesis using nat_neq_iff by blast 

   742   qed

   743 qed

   744 

   745 text {*

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

   747 *}

   748 

   749 lemma waiting_unique:

   750   assumes "waiting s th cs1"

   751   and "waiting s th cs2"

   752   shows "cs1 = cs2"

   753   using waiting_unique_pre assms

   754   unfolding wq_def s_waiting_def

   755   by auto

   756 

   757 end

   758 

   759 (* not used *)

   760 text {*

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

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

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

   764 *}

   765 lemma held_unique:

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

   767   and "holding s th2 cs"

   768   shows "th1 = th2"

   769  by (insert assms, unfold s_holding_def, auto)

   770 

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

   772   apply (induct s, auto)

   773   by (case_tac a, auto split:if_splits)

   774 

   775 lemma last_set_unique: 

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

   777           \<Longrightarrow> th1 = th2"

   778   apply (induct s, auto)

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

   780 

   781 lemma preced_unique : 

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

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

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

   785   shows "th1 = th2"

   786 proof -

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

   788   from last_set_unique [OF this th_in1 th_in2]

   789   show ?thesis .

   790 qed

   791                       

   792 lemma preced_linorder: 

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

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

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

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

   797 proof -

   798   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

   800   thus ?thesis by auto

   801 qed

   802 

   803 text {*

   804   The following three lemmas show that @{text "RAG"} does not change

   805   by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"}

   806   events, respectively.

   807 *}

   808 

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

   810 apply (unfold s_RAG_def s_waiting_def wq_def)

   811 by (simp add:Let_def)

   812 

   813 lemma (in valid_trace_set)

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

   815    by (unfold is_set RAG_set_unchanged, simp)

   816 

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

   818 apply (unfold s_RAG_def s_waiting_def wq_def)

   819 by (simp add:Let_def)

   820 

   821 lemma (in valid_trace_create)

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

   823    by (unfold is_create RAG_create_unchanged, simp)

   824 

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

   826 apply (unfold s_RAG_def s_waiting_def wq_def)

   827 by (simp add:Let_def)

   828 

   829 lemma (in valid_trace_exit)

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

   831    by (unfold is_exit RAG_exit_unchanged, simp)

   832 

   833 context valid_trace_v

   834 begin

   835 

   836 lemma distinct_rest: "distinct rest"

   837   by (simp add: distinct_tl rest_def wq_distinct)

   838 

   839 lemma holding_cs_eq_th:

   840   assumes "holding s t cs"

   841   shows "t = th"

   842 proof -

   843   from pip_e[unfolded is_v]

   844   show ?thesis

   845   proof(cases)

   846     case (thread_V)

   847     from held_unique[OF this(2) assms]

   848     show ?thesis by simp

   849   qed

   850 qed

   851 

   852 lemma distinct_wq': "distinct wq'"

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

   854   

   855 lemma set_wq': "set wq' = set rest"

   856   by (metis (mono_tags, lifting) distinct_rest rest_def 

   857       some_eq_ex wq'_def)

   858     

   859 lemma th'_in_inv:

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

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

   862   using assms set_wq' by simp

   863 

   864 lemma neq_t_th: 

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

   866   shows "t \<noteq> th"

   867 proof

   868   assume otherwise: "t = th"

   869   show False

   870   proof(cases "c = cs")

   871     case True

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

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

   874      by simp 

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

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

   877     show ?thesis by simp

   878   next

   879     case False

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

   881         by (unfold is_v, simp)

   882     hence "waiting s t c" using assms 

   883         by (simp add: cs_waiting_def waiting_eq)

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

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

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

   887   qed

   888 qed

   889 

   890 lemma waiting_esI1:

   891   assumes "waiting s t c"

   892       and "c \<noteq> cs" 

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

   894 proof -

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

   896     using assms(2) is_v by auto

   897   with assms(1) show ?thesis 

   898     using cs_waiting_def waiting_eq by auto 

   899 qed

   900 

   901 lemma holding_esI2:

   902   assumes "c \<noteq> cs" 

   903   and "holding s t c"

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

   905 proof -

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

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

   908                 folded this, unfolded wq_def, folded s_holding_def]

   909   show ?thesis .

   910 qed

   911 

   912 lemma holding_esI1:

   913   assumes "holding s t c"

   914   and "t \<noteq> th"

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

   916 proof -

   917   have "c \<noteq> cs" using assms using holding_cs_eq_th by blast 

   918   from holding_esI2[OF this assms(1)]

   919   show ?thesis .

   920 qed

   921 

   922 end

   923 

   924 context valid_trace_v_n

   925 begin

   926 

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

   928 proof (unfold wq'_def, rule someI2)

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

   930     by (simp add: distinct_rest) 

   931 next

   932   fix x

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

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

   935 qed 

   936 

   937 definition "taker = hd wq'"

   938 

   939 definition "rest' = tl wq'"

   940 

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

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

   943 

   944 lemma next_th_taker: 

   945   shows "next_th s th cs taker"

   946   using rest_nnl taker_def wq'_def wq_s_cs 

   947   by (auto simp:next_th_def)

   948 

   949 lemma taker_unique: 

   950   assumes "next_th s th cs taker'"

   951   shows "taker' = taker"

   952 proof -

   953   from assms

   954   obtain rest' where 

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

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

   957           by (unfold next_th_def, auto)

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

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

   960 qed

   961 

   962 lemma waiting_set_eq:

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

   964   by (smt all_not_in_conv bot.extremum insertI1 insert_subset 

   965       mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)

   966 

   967 lemma holding_set_eq:

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

   969   using next_th_taker taker_def waiting_set_eq 

   970   by fastforce

   971    

   972 lemma holding_taker:

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

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

   975         auto simp:neq_wq' taker_def)

   976 

   977 lemma waiting_esI2:

   978   assumes "waiting s t cs"

   979       and "t \<noteq> taker"

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

   981 proof -

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

   983   proof(unfold wq'_def, rule someI2)

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

   985           by (simp add: distinct_rest)

   986   next

   987     fix x

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

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

   990         using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto 

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

   992   qed

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

   994     using assms(2) taker_def by auto 

   995   ultimately show ?thesis

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

   997 qed

   998 

   999 lemma waiting_esE:

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

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

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

  1003 proof(cases "c = cs")

  1004   case False

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

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

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

  1008 next

  1009   case True

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

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

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

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

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

  1015   ultimately have "waiting s t cs"

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

  1017                 list.set_sel(2) rest_def waiting_eq wq_s_cs)  

  1018   show ?thesis using that(2)

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

  1020 qed

  1021 

  1022 lemma holding_esI1:

  1023   assumes "c = cs"

  1024   and "t = taker"

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

  1026   by (unfold assms, simp add: holding_taker)

  1027 

  1028 lemma holding_esE:

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

  1030   obtains "c = cs" "t = taker"

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

  1032 proof(cases "c = cs")

  1033   case True

  1034   from assms[unfolded True, unfolded s_holding_def, 

  1035              folded wq_def, unfolded wq_es_cs]

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

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

  1038 next

  1039   case False

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

  1041   from assms[unfolded s_holding_def, folded wq_def, 

  1042              unfolded this, unfolded wq_def, folded s_holding_def]

  1043   have "holding s t c"  .

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

  1045 qed

  1046 

  1047 end 

  1048 

  1049 

  1050 context valid_trace_v_e

  1051 begin

  1052 

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

  1054 proof (unfold wq'_def, rule someI2)

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

  1056     by (simp add: distinct_rest) 

  1057 next

  1058   fix x

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

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

  1061 qed 

  1062 

  1063 lemma no_taker: 

  1064   assumes "next_th s th cs taker"

  1065   shows "False"

  1066 proof -

  1067   from assms[unfolded next_th_def]

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

  1069     by auto

  1070   thus ?thesis using rest_def rest_nil by auto 

  1071 qed

  1072 

  1073 lemma waiting_set_eq:

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

  1075   using no_taker by auto

  1076 

  1077 lemma holding_set_eq:

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

  1079   using no_taker by auto

  1080    

  1081 lemma no_holding:

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

  1083   shows False

  1084 proof -

  1085   from wq_es_cs[unfolded nil_wq']

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

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

  1088   show ?thesis by auto

  1089 qed

  1090 

  1091 lemma no_waiting:

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

  1093   shows False

  1094 proof -

  1095   from wq_es_cs[unfolded nil_wq']

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

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

  1098   show ?thesis by auto

  1099 qed

  1100 

  1101 lemma waiting_esI2:

  1102   assumes "waiting s t c"

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

  1104 proof -

  1105   have "c \<noteq> cs" using assms

  1106     using cs_waiting_def rest_nil waiting_eq wq_s_cs by auto 

  1107   from waiting_esI1[OF assms this]

  1108   show ?thesis .

  1109 qed

  1110 

  1111 lemma waiting_esE:

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

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

  1114 proof(cases "c = cs")

  1115   case False

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

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

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

  1119 next

  1120   case True

  1121   from no_waiting[OF assms[unfolded True]]

  1122   show ?thesis by auto

  1123 qed

  1124 

  1125 lemma holding_esE:

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

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

  1128 proof(cases "c = cs")

  1129   case True

  1130   from no_holding[OF assms[unfolded True]] 

  1131   show ?thesis by auto

  1132 next

  1133   case False

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

  1135   from assms[unfolded s_holding_def, folded wq_def,