1 theory CpsG

     2 imports PIPDefs 

     3 begin

     4 

     5 lemma Max_f_mono:

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

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

     8   and fnt: "finite B"

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

    10 proof(rule Max_mono)

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

    12 next

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

    14 next

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

    16 qed

    17 

    18 

    19 locale valid_trace = 

    20   fixes s

    21   assumes vt : "vt s"

    22 

    23 locale valid_trace_e = valid_trace +

    24   fixes e

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

    26 begin

    27 

    28 lemma pip_e: "PIP s e"

    29   using vt_e by (cases, simp)  

    30 

    31 end

    32 

    33 locale valid_trace_create = valid_trace_e + 

    34   fixes th prio

    35   assumes is_create: "e = Create th prio"

    36 

    37 locale valid_trace_exit = valid_trace_e + 

    38   fixes th

    39   assumes is_exit: "e = Exit th"

    40 

    41 locale valid_trace_p = valid_trace_e + 

    42   fixes th cs

    43   assumes is_p: "e = P th cs"

    44 

    45 locale valid_trace_v = valid_trace_e + 

    46   fixes th cs

    47   assumes is_v: "e = V th cs"

    48 begin

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

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

    51 end

    52 

    53 locale valid_trace_v_n = valid_trace_v +

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

    55 

    56 locale valid_trace_v_e = valid_trace_v +

    57   assumes rest_nil: "rest = []"

    58 

    59 locale valid_trace_set= valid_trace_e + 

    60   fixes th prio

    61   assumes is_set: "e = Set th prio"

    62 

    63 context valid_trace

    64 begin

    65 

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

    67   assumes "PP []"

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

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

    70      shows "PP s"

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

    72   case Init

    73   from assms(1) show ?case .

    74 next

    75   case (Step s e)

    76   show ?case

    77   proof(rule assms(2))

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

    79   next

    80     show "PP s" using Step by simp

    81   next

    82     show "PIP s e" using Step by simp

    83   qed

    84 qed

    85 

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

    87 proof(induct rule:ind)

    88   case Nil

    89   thus ?case by (simp add:vt_nil)

    90 next

    91   case (Cons s e t)

    92   show ?case

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

    94     case True

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

    96     thus ?thesis using Cons

    97       by (simp add:valid_trace_def valid_trace_e_def, auto)

    98   next

    99     case False

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

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

   102     proof -

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

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

   105       show ?thesis by simp

   106     qed

   107     ultimately show ?thesis by simp

   108   qed

   109 qed

   110 

   111 lemma finite_threads:

   112   shows "finite (threads s)"

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

   114 

   115 end

   116 

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

   118 unfolding cp_def wq_def

   119 apply(induct s rule: schs.induct)

   120 apply(simp add: Let_def cpreced_initial)

   121 apply(simp add: Let_def)

   122 apply(simp add: Let_def)

   123 apply(simp add: Let_def)

   124 apply(subst (2) schs.simps)

   125 apply(simp add: Let_def)

   126 apply(subst (2) schs.simps)

   127 apply(simp add: Let_def)

   128 done

   129 

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

   131   by (unfold s_RAG_def, auto)

   132 

   133 locale valid_moment = valid_trace + 

   134   fixes i :: nat

   135 

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

   137   by (unfold_locales, insert vt_moment, auto)

   138 

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

   140   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)

   141 

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

   143   by (unfold s_holding_def wq_def cs_holding_def, simp)

   144 

   145 lemma runing_ready: 

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

   147   unfolding runing_def readys_def

   148   by auto 

   149 

   150 lemma readys_threads:

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

   152   unfolding readys_def

   153   by auto

   154 

   155 lemma wq_v_neq [simp]:

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

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

   158 

   159 lemma runing_head:

   160   assumes "th \<in> runing s"

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

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

   163   using assms

   164   by (simp add:runing_def readys_def s_waiting_def wq_def)

   165 

   166 context valid_trace

   167 begin

   168 

   169 lemma runing_wqE:

   170   assumes "th \<in> runing s"

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

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

   173 proof -

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

   175     by (meson list.set_cases)

   176   have "th' = th"

   177   proof(rule ccontr)

   178     assume "th' \<noteq> th"

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

   180     with assms(2)

   181     have "waiting s th cs" 

   182       by (unfold s_waiting_def, fold wq_def, auto)

   183     with assms show False 

   184       by (unfold runing_def readys_def, auto)

   185   qed

   186   with eq_wq that show ?thesis by metis

   187 qed

   188 

   189 end

   190 

   191 context valid_trace_create

   192 begin

   193 

   194 lemma wq_neq_simp [simp]:

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

   196     using assms unfolding is_create wq_def

   197   by (auto simp:Let_def)

   198 

   199 lemma wq_distinct_kept:

   200   assumes "distinct (wq s cs')"

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

   202   using assms by simp

   203 end

   204 

   205 context valid_trace_exit

   206 begin

   207 

   208 lemma wq_neq_simp [simp]:

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

   210     using assms unfolding is_exit wq_def

   211   by (auto simp:Let_def)

   212 

   213 lemma wq_distinct_kept:

   214   assumes "distinct (wq s cs')"

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

   216   using assms by simp

   217 end

   218 

   219 context valid_trace_p

   220 begin

   221 

   222 lemma wq_neq_simp [simp]:

   223   assumes "cs' \<noteq> cs"

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

   225     using assms unfolding is_p wq_def

   226   by (auto simp:Let_def)

   227 

   228 lemma runing_th_s:

   229   shows "th \<in> runing s"

   230 proof -

   231   from pip_e[unfolded is_p]

   232   show ?thesis by (cases, simp)

   233 qed

   234 

   235 lemma th_not_waiting: 

   236   "\<not> waiting s th c"

   237 proof -

   238   have "th \<in> readys s"

   239     using runing_ready runing_th_s by blast 

   240   thus ?thesis

   241     by (unfold readys_def, auto)

   242 qed

   243 

   244 lemma waiting_neq_th: 

   245   assumes "waiting s t c"

   246   shows "t \<noteq> th"

   247   using assms using th_not_waiting by blast 

   248 

   249 lemma th_not_in_wq: 

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

   251 proof

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

   253   from runing_wqE[OF runing_th_s this]

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

   255   with otherwise

   256   have "holding s th cs"

   257     by (unfold s_holding_def, fold wq_def, simp)

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

   259     by (unfold s_RAG_def, fold holding_eq, auto)

   260   from pip_e[unfolded is_p]

   261   show False

   262   proof(cases)

   263     case (thread_P)

   264     with cs_th_RAG show ?thesis by auto

   265   qed

   266 qed

   267 

   268 lemma wq_es_cs: 

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

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

   271 

   272 lemma wq_distinct_kept:

   273   assumes "distinct (wq s cs')"

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

   275 proof(cases "cs' = cs")

   276   case True

   277   show ?thesis using True assms th_not_in_wq

   278     by (unfold True wq_es_cs, auto)

   279 qed (insert assms, simp)

   280 

   281 end

   282 

   283 context valid_trace_v

   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_v 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_v]

   296   show ?thesis by (cases, simp)

   297 qed

   298 

   299 lemma th_not_waiting: 

   300   "\<not> waiting s th c"

   301 proof -

   302   have "th \<in> readys s"

   303     using runing_ready runing_th_s by blast 

   304   thus ?thesis

   305     by (unfold readys_def, auto)

   306 qed

   307 

   308 lemma waiting_neq_th: 

   309   assumes "waiting s t c"

   310   shows "t \<noteq> th"

   311   using assms using th_not_waiting by blast 

   312 

   313 lemma wq_s_cs:

   314   "wq s cs = th#rest"

   315 proof -

   316   from pip_e[unfolded is_v]

   317   show ?thesis

   318   proof(cases)

   319     case (thread_V)

   320     from this(2) show ?thesis

   321       by (unfold rest_def s_holding_def, fold wq_def,

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

   323   qed

   324 qed

   325 

   326 lemma wq_es_cs:

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

   328  using wq_s_cs[unfolded wq_def]

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

   330 

   331 lemma wq_distinct_kept:

   332   assumes "distinct (wq s cs')"

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

   334 proof(cases "cs' = cs")

   335   case True

   336   show ?thesis

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

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

   339         using assms[unfolded True wq_s_cs] by auto

   340   qed simp

   341 qed (insert assms, simp)

   342 

   343 end

   344 

   345 context valid_trace_set

   346 begin

   347 

   348 lemma wq_neq_simp [simp]:

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

   350     using assms unfolding is_set wq_def

   351   by (auto simp:Let_def)

   352 

   353 lemma wq_distinct_kept:

   354   assumes "distinct (wq s cs')"

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

   356   using assms by simp

   357 end

   358 

   359 context valid_trace

   360 begin

   361 

   362 lemma actor_inv: 

   363   assumes "PIP s e"

   364   and "\<not> isCreate e"

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

   366   using assms

   367   by (induct, auto)

   368 

   369 lemma isP_E:

   370   assumes "isP e"

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

   372   using assms by (cases e, auto)

   373 

   374 lemma isV_E:

   375   assumes "isV e"

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

   377   using assms by (cases e, auto) 

   378 

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

   380 proof(induct rule:ind)

   381   case (Cons s e)

   382   interpret vt_e: valid_trace_e s e using Cons by simp

   383   show ?case 

   384   proof(cases e)

   385     case (Create th prio)

   386     interpret vt_create: valid_trace_create s e th prio 

   387       using Create by (unfold_locales, simp)

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

   389   next

   390     case (Exit th)

   391     interpret vt_exit: valid_trace_exit s e th  

   392         using Exit by (unfold_locales, simp)

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

   394   next

   395     case (P th cs)

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

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

   398   next

   399     case (V th cs)

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

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

   402   next

   403     case (Set th prio)

   404     interpret vt_set: valid_trace_set s e th prio

   405         using Set by (unfold_locales, simp)

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

   407   qed

   408 qed (unfold wq_def Let_def, simp)

   409 

   410 end

   411 

   412 context valid_trace_e

   413 begin

   414 

   415 text {*

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

   417   operation can add new thread into waiting queues. 

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

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

   420 *}

   421 

   422 lemma wq_in_inv: 

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

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

   425   shows "e = P thread cs"

   426 proof(cases e)

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

   428   case (V th cs1)

   429   have False

   430   proof(cases "cs1 = cs")

   431     case True

   432     show ?thesis

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

   434       case (Cons w_hd w_tl)

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

   436       proof -

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

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

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

   440         proof(rule someI2)

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

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

   443         qed (insert Cons True, auto)

   444         ultimately show ?thesis by simp

   445       qed

   446       with assms show ?thesis by auto

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

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

   449   thus ?thesis by auto

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

   451 

   452 lemma wq_out_inv: 

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

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

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

   456   shows "e = V thread cs"

   457 proof(cases e)

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

   459   case (V th cs1)

   460   show ?thesis

   461   proof(cases "cs1 = cs")

   462     case True

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

   464     thus ?thesis

   465     proof(cases)

   466       case (thread_V)

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

   468           by (unfold s_holding_def wq_def, simp)

   469       ultimately show ?thesis using V True by simp

   470     qed

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

   472 next

   473   case (P th cs1)

   474   show ?thesis

   475   proof(cases "cs1 = cs")

   476     case True

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

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

   479     with s_i s_hd s_in have False

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

   481     thus ?thesis by simp

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

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

   484 

   485 end

   486 

   487 

   488 context valid_trace

   489 begin

   490 

   491 

   492 text {* (* ddd *)

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

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

   495   For instance, the fact 

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

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

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

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

   500 

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

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

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

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

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

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

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

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

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

   510 

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

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

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

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

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

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

   517   and kept on blocked on them respectively ever since.

   518  

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

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

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

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

   523 *}

   524 

   525 lemma waiting_unique_pre: (* ddd *)

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

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

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

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

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

   531   shows "False"

   532 proof -

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

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

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

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

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

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

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

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

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

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

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

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

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

   546   { fix s cs

   547     assume q: "?Q cs s"

   548     have "thread \<notin> runing s"

   549     proof

   550       assume "thread \<in> runing s"

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

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

   553         by (unfold runing_def s_waiting_def readys_def, auto)

   554       from this[rule_format, of cs] q 

   555       show False by (simp add: wq_def) 

   556     qed

   557   } note q_not_runing = this

   558   { fix t1 t2 cs1 cs2

   559     assume  lt1: "t1 < length s"

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

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

   562     and lt2: "t2 < length s"

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

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

   565     and lt12: "t1 < t2"

   566     let ?t3 = "Suc t2"

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

   568     from moment_plus [OF this] 

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

   570     have "t2 < ?t3" by simp

   571     from nn2 [rule_format, OF this] and eq_m

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

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

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

   575     proof -

   576       from vt_moment 

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

   578       with eq_m show ?thesis by simp

   579     qed

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

   581         by (unfold_locales, auto, cases, simp)

   582     have ?thesis

   583     proof -

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

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

   586         case True

   587         have "e = V thread cs2"

   588         proof -

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

   590               using True and np2  by auto 

   591           from vt_e.wq_out_inv[OF True this h2]

   592           show ?thesis .

   593         qed

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

   595       next

   596         case False

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

   598         with vt_e.actor_inv[OF vt_e.pip_e]

   599         show ?thesis by auto

   600       qed

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

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

   603       ultimately show ?thesis by simp

   604     qed

   605   } note lt_case = this

   606   show ?thesis

   607   proof -

   608     { assume "t1 < t2"

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

   610       have ?thesis .

   611     } moreover {

   612       assume "t2 < t1"

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

   614       have ?thesis .

   615     } moreover {

   616       assume eq_12: "t1 = t2"

   617       let ?t3 = "Suc t2"

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

   619       from moment_plus [OF this] 

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

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

   622       from nn2 [rule_format, OF this] and eq_m

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

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

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

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

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

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

   629       proof -

   630         from vt_moment 

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

   632         with eq_m show ?thesis by simp

   633       qed

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

   635           by (unfold_locales, auto, cases, simp)

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

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

   638         case True

   639         have "e = V thread cs2"

   640         proof -

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

   642               using True and np2  by auto 

   643           from vt_e.wq_out_inv[OF True this h2]

   644           show ?thesis .

   645         qed

   646         thus ?thesis by auto

   647       next

   648         case False

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

   650         thus ?thesis by auto

   651       qed

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

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

   654         case True

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

   656               using True and np1  by auto 

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

   658         have "e = V thread cs1" .

   659         thus ?thesis by auto

   660       next

   661         case False

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

   663         thus ?thesis by auto

   664       qed

   665       ultimately have ?thesis using neq12 by auto

   666     } ultimately show ?thesis using nat_neq_iff by blast 

   667   qed

   668 qed

   669 

   670 text {*

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

   672 *}

   673 

   674 lemma waiting_unique:

   675   assumes "waiting s th cs1"

   676   and "waiting s th cs2"

   677   shows "cs1 = cs2"

   678   using waiting_unique_pre assms

   679   unfolding wq_def s_waiting_def

   680   by auto

   681 

   682 end

   683 

   684 (* not used *)

   685 text {*

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

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

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

   689 *}

   690 lemma held_unique:

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

   692   and "holding s th2 cs"

   693   shows "th1 = th2"

   694  by (insert assms, unfold s_holding_def, auto)

   695 

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

   697   apply (induct s, auto)

   698   by (case_tac a, auto split:if_splits)

   699 

   700 lemma last_set_unique: 

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

   702           \<Longrightarrow> th1 = th2"

   703   apply (induct s, auto)

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

   705 

   706 lemma preced_unique : 

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

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

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

   710   shows "th1 = th2"

   711 proof -

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

   713   from last_set_unique [OF this th_in1 th_in2]

   714   show ?thesis .

   715 qed

   716                       

   717 lemma preced_linorder: 

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

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

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

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

   722 proof -

   723   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

   725   thus ?thesis by auto

   726 qed

   727 

   728 text {*

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

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

   731   events, respectively.

   732 *}

   733 

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

   735 apply (unfold s_RAG_def s_waiting_def wq_def)

   736 by (simp add:Let_def)

   737 

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

   739 apply (unfold s_RAG_def s_waiting_def wq_def)

   740 by (simp add:Let_def)

   741 

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

   743 apply (unfold s_RAG_def s_waiting_def wq_def)

   744 by (simp add:Let_def)

   745 

   746 

   747 context valid_trace_v

   748 begin

   749 

   750 lemma distinct_rest: "distinct rest"

   751   by (simp add: distinct_tl rest_def wq_distinct)

   752 

   753 lemma holding_cs_eq_th:

   754   assumes "holding s t cs"

   755   shows "t = th"

   756 proof -

   757   from pip_e[unfolded is_v]

   758   show ?thesis

   759   proof(cases)

   760     case (thread_V)

   761     from held_unique[OF this(2) assms]

   762     show ?thesis by simp

   763   qed

   764 qed

   765 

   766 lemma distinct_wq': "distinct wq'"

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

   768   

   769 lemma th'_in_inv:

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

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

   772   using assms

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

   774         rest_def some_eq_ex wq'_def wq_distinct wq_s_cs) 

   775 

   776 lemma neq_t_th: 

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

   778   shows "t \<noteq> th"

   779 proof

   780   assume otherwise: "t = th"

   781   show False

   782   proof(cases "c = cs")

   783     case True

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

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

   786      by simp 

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

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

   789     show ?thesis by simp

   790   next

   791     case False

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

   793         by (unfold is_v, simp)

   794     hence "waiting s t c" using assms 

   795         by (simp add: cs_waiting_def waiting_eq)

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

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

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

   799   qed

   800 qed

   801 

   802 lemma waiting_esI1:

   803   assumes "waiting s t c"

   804       and "c \<noteq> cs" 

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

   806 proof -

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

   808     using assms(2) is_v by auto

   809   with assms(1) show ?thesis 

   810     using cs_waiting_def waiting_eq by auto 

   811 qed

   812 

   813 lemma holding_esI2:

   814   assumes "c \<noteq> cs" 

   815   and "holding s t c"

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

   817 proof -

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

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

   820                 folded this, unfolded wq_def, folded s_holding_def]

   821   show ?thesis .

   822 qed

   823 

   824 lemma holding_esI1:

   825   assumes "holding s t c"

   826   and "t \<noteq> th"

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

   828 proof -

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

   830   from holding_esI2[OF this assms(1)]

   831   show ?thesis .

   832 qed

   833 

   834 end

   835 

   836 context valid_trace_v_n

   837 begin

   838 

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

   840 proof (unfold wq'_def, rule someI2)

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

   842     by (simp add: distinct_rest) 

   843 next

   844   fix x

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

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

   847 qed 

   848 

   849 definition "taker = hd wq'"

   850 

   851 definition "rest' = tl wq'"

   852 

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

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

   855 

   856 lemma next_th_taker: 

   857   shows "next_th s th cs taker"

   858   using rest_nnl taker_def wq'_def wq_s_cs 

   859   by (auto simp:next_th_def)

   860 

   861 lemma taker_unique: 

   862   assumes "next_th s th cs taker'"

   863   shows "taker' = taker"

   864 proof -

   865   from assms

   866   obtain rest' where 

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

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

   869           by (unfold next_th_def, auto)

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

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

   872 qed

   873 

   874 lemma waiting_set_eq:

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

   876   by (smt all_not_in_conv bot.extremum insertI1 insert_subset 

   877       mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)

   878 

   879 lemma holding_set_eq:

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

   881   using next_th_taker taker_def waiting_set_eq 

   882   by fastforce

   883    

   884 lemma holding_taker:

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

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

   887         auto simp:neq_wq' taker_def)

   888 

   889 lemma waiting_esI2:

   890   assumes "waiting s t cs"

   891       and "t \<noteq> taker"

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

   893 proof -

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

   895   proof(unfold wq'_def, rule someI2)

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

   897           by (simp add: distinct_rest)

   898   next

   899     fix x

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

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

   902         using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto 

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

   904   qed

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

   906     using assms(2) taker_def by auto 

   907   ultimately show ?thesis

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

   909 qed

   910 

   911 lemma waiting_esE:

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

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

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

   915 proof(cases "c = cs")

   916   case False

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

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

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

   920 next

   921   case True

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

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

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

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

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

   927   ultimately have "waiting s t cs"

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

   929                 list.set_sel(2) rest_def waiting_eq wq_s_cs)  

   930   show ?thesis using that(2)

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

   932 qed

   933 

   934 lemma holding_esI1:

   935   assumes "c = cs"

   936   and "t = taker"

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

   938   by (unfold assms, simp add: holding_taker)

   939 

   940 lemma holding_esE:

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

   942   obtains "c = cs" "t = taker"

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

   944 proof(cases "c = cs")

   945   case True

   946   from assms[unfolded True, unfolded s_holding_def, 

   947              folded wq_def, unfolded wq_es_cs]

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

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

   950 next

   951   case False

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

   953   from assms[unfolded s_holding_def, folded wq_def, 

   954              unfolded this, unfolded wq_def, folded s_holding_def]

   955   have "holding s t c"  .

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

   957 qed

   958 

   959 end 

   960 

   961 

   962 context valid_trace_v_e

   963 begin

   964 

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

   966 proof (unfold wq'_def, rule someI2)

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

   968     by (simp add: distinct_rest) 

   969 next

   970   fix x

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

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

   973 qed 

   974 

   975 lemma no_taker: 

   976   assumes "next_th s th cs taker"

   977   shows "False"

   978 proof -

   979   from assms[unfolded next_th_def]

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

   981     by auto

   982   thus ?thesis using rest_def rest_nil by auto 

   983 qed

   984 

   985 lemma waiting_set_eq:

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

   987   using no_taker by auto

   988 

   989 lemma holding_set_eq:

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

   991   using no_taker by auto

   992    

   993 lemma no_holding:

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

   995   shows False

   996 proof -

   997   from wq_es_cs[unfolded nil_wq']

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

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

  1000   show ?thesis by auto

  1001 qed

  1002 

  1003 lemma no_waiting:

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

  1005   shows False

  1006 proof -

  1007   from wq_es_cs[unfolded nil_wq']

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

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

  1010   show ?thesis by auto

  1011 qed

  1012 

  1013 lemma waiting_esI2:

  1014   assumes "waiting s t c"

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

  1016 proof -

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

  1018     using cs_waiting_def rest_nil waiting_eq wq_s_cs by auto 

  1019   from waiting_esI1[OF assms this]

  1020   show ?thesis .

  1021 qed

  1022 

  1023 lemma waiting_esE:

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

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

  1026 proof(cases "c = cs")

  1027   case False

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

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

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

  1031 next

  1032   case True

  1033   from no_waiting[OF assms[unfolded True]]

  1034   show ?thesis by auto

  1035 qed

  1036 

  1037 lemma holding_esE:

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

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

  1040 proof(cases "c = cs")

  1041   case True

  1042   from no_holding[OF assms[unfolded True]] 

  1043   show ?thesis by auto

  1044 next

  1045   case False

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

  1047   from assms[unfolded s_holding_def, folded wq_def, 

  1048              unfolded this, unfolded wq_def, folded s_holding_def]

  1049   have "holding s t c"  .

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

  1051 qed

  1052 

  1053 end 

  1054 

  1055 lemma rel_eqI:

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

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

  1058   shows "A = B"

  1059   using assms by auto

  1060 

  1061 lemma in_RAG_E:

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

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

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

  1065   using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]

  1066   by auto

  1067   

  1068 context valid_trace_v

  1069 begin

  1070 

  1071 lemma RAG_es:

  1072   "RAG (e # s) =

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

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

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

  1076 proof(rule rel_eqI)

  1077   fix n1 n2

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

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

  1080   proof(cases rule:in_RAG_E)

  1081     case (waiting th' cs')

  1082     show ?thesis

  1083     proof(cases "rest = []")

  1084       case False

  1085       interpret h_n: valid_trace_v_n s e th cs

  1086         by (unfold_locales, insert False, simp)

  1087       from waiting(3)

  1088       show ?thesis

  1089       proof(cases rule:h_n.waiting_esE)

  1090         case 1

  1091         with waiting(1,2)

  1092         show ?thesis

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

  1094              fold waiting_eq, auto)

  1095       next

  1096         case 2

  1097         with waiting(1,2)

  1098         show ?thesis

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

  1100              fold waiting_eq, auto)

  1101       qed

  1102     next

  1103       case True

  1104       interpret h_e: valid_trace_v_e s e th cs

  1105         by (unfold_locales, insert True, simp)

  1106       from waiting(3)

  1107       show ?thesis

  1108       proof(cases rule:h_e.waiting_esE)

  1109         case 1

  1110         with waiting(1,2)

  1111         show ?thesis

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

  1113              fold waiting_eq, auto)

  1114       qed

  1115     qed

  1116   next

  1117     case (holding th' cs')

  1118     show ?thesis

  1119     proof(cases "rest = []")

  1120       case False

  1121       interpret h_n: valid_trace_v_n s e th cs

  1122         by (unfold_locales, insert False, simp)

  1123       from holding(3)

  1124       show ?thesis

  1125       proof(cases rule:h_n.holding_esE)

  1126         case 1

  1127         with holding(1,2)

  1128         show ?thesis

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

  1130              fold waiting_eq, auto)

  1131       next

  1132         case 2

  1133         with holding(1,2)

  1134         show ?thesis

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