1 theory CpsG

     2 imports PIPDefs

     3 begin

     4 

     5 lemma f_image_eq:

     6   assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"

     7   shows "f ` A = g ` A"

     8 proof

     9   show "f ` A \<subseteq> g ` A"

    10     by(rule image_subsetI, auto intro:h)

    11 next

    12   show "g ` A \<subseteq> f ` A"

    13    by (rule image_subsetI, auto intro:h[symmetric])

    14 qed

    15 

    16 lemma Max_fg_mono:

    17   assumes "finite A"

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

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

    20 proof(cases "A = {}")

    21   case True

    22   thus ?thesis by auto

    23 next

    24   case False

    25   show ?thesis

    26   proof(rule Max.boundedI)

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

    28   next

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

    30   next

    31     fix fa

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

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

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

    35     proof(rule Max_ge_iff[THEN iffD2])

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

    37     next

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

    39     next

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

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

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

    43     qed

    44   qed

    45 qed 

    46 

    47 lemma Max_f_mono:

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

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

    50   and fnt: "finite B"

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

    52 proof(rule Max_mono)

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

    54 next

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

    56 next

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

    58 qed

    59 

    60 lemma Max_UNION: 

    61   assumes "finite A"

    62   and "A \<noteq> {}"

    63   and "\<forall> M \<in> f ` A. finite M"

    64   and "\<forall> M \<in> f ` A. M \<noteq> {}"

    65   shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")

    66   using assms[simp]

    67 proof -

    68   have "?L = Max (\<Union>(f ` A))"

    69     by (fold Union_image_eq, simp)

    70   also have "... = ?R"

    71     by (subst Max_Union, simp+)

    72   finally show ?thesis .

    73 qed

    74 

    75 lemma max_Max_eq:

    76   assumes "finite A"

    77     and "A \<noteq> {}"

    78     and "x = y"

    79   shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")

    80 proof -

    81   have "?R = Max (insert y A)" by simp

    82   also from assms have "... = ?L"

    83       by (subst Max.insert, simp+)

    84   finally show ?thesis by simp

    85 qed

    86 

    87 lemma birth_time_lt:  

    88   assumes "s \<noteq> []"

    89   shows "last_set th s < length s"

    90   using assms

    91 proof(induct s)

    92   case (Cons a s)

    93   show ?case

    94   proof(cases "s \<noteq> []")

    95     case False

    96     thus ?thesis

    97       by (cases a, auto)

    98   next

    99     case True

   100     show ?thesis using Cons(1)[OF True]

   101       by (cases a, auto)

   102   qed

   103 qed simp

   104 

   105 lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"

   106   by (induct s, auto)

   107 

   108 lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"

   109   by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)

   110 

   111 lemma eq_RAG: 

   112   "RAG (wq s) = RAG s"

   113   by (unfold cs_RAG_def s_RAG_def, auto)

   114 

   115 lemma waiting_holding:

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

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

   118 proof -

   119   from assms[unfolded s_waiting_def, folded wq_def]

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

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

   122   hence "holding s th' cs" 

   123     by (unfold s_holding_def, fold wq_def, auto)

   124   from that[OF this] show ?thesis .

   125 qed

   126 

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

   128 unfolding cp_def wq_def

   129 apply(induct s rule: schs.induct)

   130 apply(simp add: Let_def cpreced_initial)

   131 apply(simp add: Let_def)

   132 apply(simp add: Let_def)

   133 apply(simp add: Let_def)

   134 apply(subst (2) schs.simps)

   135 apply(simp add: Let_def)

   136 apply(subst (2) schs.simps)

   137 apply(simp add: Let_def)

   138 done

   139 

   140 lemma cp_alt_def:

   141   "cp s th =  

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

   143 proof -

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

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

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

   147   proof -

   148     have "?L = ?R" 

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

   150     thus ?thesis by simp

   151   qed

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

   153 qed

   154 

   155 (* ccc *)

   156 

   157 

   158 locale valid_trace = 

   159   fixes s

   160   assumes vt : "vt s"

   161 

   162 locale valid_trace_e = valid_trace +

   163   fixes e

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

   165 begin

   166 

   167 lemma pip_e: "PIP s e"

   168   using vt_e by (cases, simp)  

   169 

   170 end

   171 

   172 locale valid_trace_create = valid_trace_e + 

   173   fixes th prio

   174   assumes is_create: "e = Create th prio"

   175 

   176 locale valid_trace_exit = valid_trace_e + 

   177   fixes th

   178   assumes is_exit: "e = Exit th"

   179 

   180 locale valid_trace_p = valid_trace_e + 

   181   fixes th cs

   182   assumes is_p: "e = P th cs"

   183 

   184 locale valid_trace_v = valid_trace_e + 

   185   fixes th cs

   186   assumes is_v: "e = V th cs"

   187 begin

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

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

   190 end

   191 

   192 locale valid_trace_v_n = valid_trace_v +

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

   194 

   195 locale valid_trace_v_e = valid_trace_v +

   196   assumes rest_nil: "rest = []"

   197 

   198 locale valid_trace_set= valid_trace_e + 

   199   fixes th prio

   200   assumes is_set: "e = Set th prio"

   201 

   202 context valid_trace

   203 begin

   204 

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

   206   assumes "PP []"

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

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

   209      shows "PP s"

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

   211   case Init

   212   from assms(1) show ?case .

   213 next

   214   case (Step s e)

   215   show ?case

   216   proof(rule assms(2))

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

   218   next

   219     show "PP s" using Step by simp

   220   next

   221     show "PIP s e" using Step by simp

   222   qed

   223 qed

   224 

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

   226 proof(induct rule:ind)

   227   case Nil

   228   thus ?case by (simp add:vt_nil)

   229 next

   230   case (Cons s e t)

   231   show ?case

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

   233     case True

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

   235     thus ?thesis using Cons

   236       by (simp add:valid_trace_def valid_trace_e_def, auto)

   237   next

   238     case False

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

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

   241     proof -

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

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

   244       show ?thesis by simp

   245     qed

   246     ultimately show ?thesis by simp

   247   qed

   248 qed

   249 

   250 lemma finite_threads:

   251   shows "finite (threads s)"

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

   253 

   254 end

   255 

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

   257   by (unfold s_RAG_def, auto)

   258 

   259 locale valid_moment = valid_trace + 

   260   fixes i :: nat

   261 

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

   263   by (unfold_locales, insert vt_moment, auto)

   264 

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

   266   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)

   267 

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

   269   by (unfold s_holding_def wq_def cs_holding_def, simp)

   270 

   271 lemma runing_ready: 

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

   273   unfolding runing_def readys_def

   274   by auto 

   275 

   276 lemma readys_threads:

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

   278   unfolding readys_def

   279   by auto

   280 

   281 lemma wq_v_neq [simp]:

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

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

   284 

   285 lemma runing_head:

   286   assumes "th \<in> runing s"

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

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

   289   using assms

   290   by (simp add:runing_def readys_def s_waiting_def wq_def)

   291 

   292 context valid_trace

   293 begin

   294 

   295 lemma runing_wqE:

   296   assumes "th \<in> runing s"

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

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

   299 proof -

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

   301     by (meson list.set_cases)

   302   have "th' = th"

   303   proof(rule ccontr)

   304     assume "th' \<noteq> th"

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

   306     with assms(2)

   307     have "waiting s th cs" 

   308       by (unfold s_waiting_def, fold wq_def, auto)

   309     with assms show False 

   310       by (unfold runing_def readys_def, auto)

   311   qed

   312   with eq_wq that show ?thesis by metis

   313 qed

   314 

   315 end

   316 

   317 context valid_trace_create

   318 begin

   319 

   320 lemma wq_neq_simp [simp]:

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

   322     using assms unfolding is_create wq_def

   323   by (auto simp:Let_def)

   324 

   325 lemma wq_distinct_kept:

   326   assumes "distinct (wq s cs')"

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

   328   using assms by simp

   329 end

   330 

   331 context valid_trace_exit

   332 begin

   333 

   334 lemma wq_neq_simp [simp]:

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

   336     using assms unfolding is_exit wq_def

   337   by (auto simp:Let_def)

   338 

   339 lemma wq_distinct_kept:

   340   assumes "distinct (wq s cs')"

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

   342   using assms by simp

   343 end

   344 

   345 context valid_trace_p

   346 begin

   347 

   348 lemma wq_neq_simp [simp]:

   349   assumes "cs' \<noteq> cs"

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

   351     using assms unfolding is_p wq_def

   352   by (auto simp:Let_def)

   353 

   354 lemma runing_th_s:

   355   shows "th \<in> runing s"

   356 proof -

   357   from pip_e[unfolded is_p]

   358   show ?thesis by (cases, simp)

   359 qed

   360 

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

   362   using runing_th_s

   363   by (unfold runing_def, auto)

   364 

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

   366   using readys_threads ready_th_s by auto

   367 

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

   369   using live_th_s 

   370   by (unfold is_p, simp)

   371 

   372 lemma th_not_waiting: 

   373   "\<not> waiting s th c"

   374 proof -

   375   have "th \<in> readys s"

   376     using runing_ready runing_th_s by blast 

   377   thus ?thesis

   378     by (unfold readys_def, auto)

   379 qed

   380 

   381 lemma waiting_neq_th: 

   382   assumes "waiting s t c"

   383   shows "t \<noteq> th"

   384   using assms using th_not_waiting by blast 

   385 

   386 lemma th_not_in_wq: 

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

   388 proof

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

   390   from runing_wqE[OF runing_th_s this]

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

   392   with otherwise

   393   have "holding s th cs"

   394     by (unfold s_holding_def, fold wq_def, simp)

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

   396     by (unfold s_RAG_def, fold holding_eq, auto)

   397   from pip_e[unfolded is_p]

   398   show False

   399   proof(cases)

   400     case (thread_P)

   401     with cs_th_RAG show ?thesis by auto

   402   qed

   403 qed

   404 

   405 lemma wq_es_cs: 

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

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

   408 

   409 lemma wq_distinct_kept:

   410   assumes "distinct (wq s cs')"

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

   412 proof(cases "cs' = cs")

   413   case True

   414   show ?thesis using True assms th_not_in_wq

   415     by (unfold True wq_es_cs, auto)

   416 qed (insert assms, simp)

   417 

   418 end

   419 

   420 context valid_trace_v

   421 begin

   422 

   423 lemma wq_neq_simp [simp]:

   424   assumes "cs' \<noteq> cs"

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

   426     using assms unfolding is_v wq_def

   427   by (auto simp:Let_def)

   428 

   429 lemma runing_th_s:

   430   shows "th \<in> runing s"

   431 proof -

   432   from pip_e[unfolded is_v]

   433   show ?thesis by (cases, simp)

   434 qed

   435 

   436 lemma th_not_waiting: 

   437   "\<not> waiting s th c"

   438 proof -

   439   have "th \<in> readys s"

   440     using runing_ready runing_th_s by blast 

   441   thus ?thesis

   442     by (unfold readys_def, auto)

   443 qed

   444 

   445 lemma waiting_neq_th: 

   446   assumes "waiting s t c"

   447   shows "t \<noteq> th"

   448   using assms using th_not_waiting by blast 

   449 

   450 lemma wq_s_cs:

   451   "wq s cs = th#rest"

   452 proof -

   453   from pip_e[unfolded is_v]

   454   show ?thesis

   455   proof(cases)

   456     case (thread_V)

   457     from this(2) show ?thesis

   458       by (unfold rest_def s_holding_def, fold wq_def,

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

   460   qed

   461 qed

   462 

   463 lemma wq_es_cs:

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

   465  using wq_s_cs[unfolded wq_def]

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

   467 

   468 lemma wq_distinct_kept:

   469   assumes "distinct (wq s cs')"

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

   471 proof(cases "cs' = cs")

   472   case True

   473   show ?thesis

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

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

   476         using assms[unfolded True wq_s_cs] by auto

   477   qed simp

   478 qed (insert assms, simp)

   479 

   480 end

   481 

   482 context valid_trace_set

   483 begin

   484 

   485 lemma wq_neq_simp [simp]:

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

   487     using assms unfolding is_set wq_def

   488   by (auto simp:Let_def)

   489 

   490 lemma wq_distinct_kept:

   491   assumes "distinct (wq s cs')"

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

   493   using assms by simp

   494 end

   495 

   496 context valid_trace

   497 begin

   498 

   499 lemma actor_inv: 

   500   assumes "PIP s e"

   501   and "\<not> isCreate e"

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

   503   using assms

   504   by (induct, auto)

   505 

   506 lemma isP_E:

   507   assumes "isP e"

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

   509   using assms by (cases e, auto)

   510 

   511 lemma isV_E:

   512   assumes "isV e"

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

   514   using assms by (cases e, auto) 

   515 

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

   517 proof(induct rule:ind)

   518   case (Cons s e)

   519   interpret vt_e: valid_trace_e s e using Cons by simp

   520   show ?case 

   521   proof(cases e)

   522     case (Create th prio)

   523     interpret vt_create: valid_trace_create s e th prio 

   524       using Create by (unfold_locales, simp)

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

   526   next

   527     case (Exit th)

   528     interpret vt_exit: valid_trace_exit s e th  

   529         using Exit by (unfold_locales, simp)

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

   531   next

   532     case (P th cs)

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

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

   535   next

   536     case (V th cs)

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

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

   539   next

   540     case (Set th prio)

   541     interpret vt_set: valid_trace_set s e th prio

   542         using Set by (unfold_locales, simp)

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

   544   qed

   545 qed (unfold wq_def Let_def, simp)

   546 

   547 end

   548 

   549 context valid_trace_e

   550 begin

   551 

   552 text {*

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

   554   operation can add new thread into waiting queues. 

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

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

   557 *}

   558 

   559 lemma wq_in_inv: 

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

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

   562   shows "e = P thread cs"

   563 proof(cases e)

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

   565   case (V th cs1)

   566   have False

   567   proof(cases "cs1 = cs")

   568     case True

   569     show ?thesis

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

   571       case (Cons w_hd w_tl)

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

   573       proof -

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

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

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

   577         proof(rule someI2)

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

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

   580         qed (insert Cons True, auto)

   581         ultimately show ?thesis by simp

   582       qed

   583       with assms show ?thesis by auto

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

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

   586   thus ?thesis by auto

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

   588 

   589 lemma wq_out_inv: 

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

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

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

   593   shows "e = V thread cs"

   594 proof(cases e)

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

   596   case (V th cs1)

   597   show ?thesis

   598   proof(cases "cs1 = cs")

   599     case True

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

   601     thus ?thesis

   602     proof(cases)

   603       case (thread_V)

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

   605           by (unfold s_holding_def wq_def, simp)

   606       ultimately show ?thesis using V True by simp

   607     qed

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

   609 next

   610   case (P th cs1)

   611   show ?thesis

   612   proof(cases "cs1 = cs")

   613     case True

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

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

   616     with s_i s_hd s_in have False

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

   618     thus ?thesis by simp

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

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

   621 

   622 end

   623 

   624 

   625 context valid_trace

   626 begin

   627 

   628 

   629 text {* (* ddd *)

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

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

   632   For instance, the fact 

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

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

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

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

   637 

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

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

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

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

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

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

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

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

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

   647 

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

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

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

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

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

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

   654   and kept on blocked on them respectively ever since.

   655  

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

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

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

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

   660 *}

   661 

   662 lemma waiting_unique_pre: (* ddd *)

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

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

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

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

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

   668   shows "False"

   669 proof -

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

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

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

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

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

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

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

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

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

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

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

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

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

   683   { fix s cs

   684     assume q: "?Q cs s"

   685     have "thread \<notin> runing s"

   686     proof

   687       assume "thread \<in> runing s"

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

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

   690         by (unfold runing_def s_waiting_def readys_def, auto)

   691       from this[rule_format, of cs] q 

   692       show False by (simp add: wq_def) 

   693     qed

   694   } note q_not_runing = this

   695   { fix t1 t2 cs1 cs2

   696     assume  lt1: "t1 < length s"

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

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

   699     and lt2: "t2 < length s"

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

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

   702     and lt12: "t1 < t2"

   703     let ?t3 = "Suc t2"

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

   705     from moment_plus [OF this] 

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

   707     have "t2 < ?t3" by simp

   708     from nn2 [rule_format, OF this] and eq_m

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

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

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

   712     proof -

   713       from vt_moment 

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

   715       with eq_m show ?thesis by simp

   716     qed

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

   718         by (unfold_locales, auto, cases, simp)

   719     have ?thesis

   720     proof -

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

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

   723         case True

   724         have "e = V thread cs2"

   725         proof -

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

   727               using True and np2  by auto 

   728           from vt_e.wq_out_inv[OF True this h2]

   729           show ?thesis .

   730         qed

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

   732       next

   733         case False

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

   735         with vt_e.actor_inv[OF vt_e.pip_e]

   736         show ?thesis by auto

   737       qed

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

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

   740       ultimately show ?thesis by simp

   741     qed

   742   } note lt_case = this

   743   show ?thesis

   744   proof -

   745     { assume "t1 < t2"

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

   747       have ?thesis .

   748     } moreover {

   749       assume "t2 < t1"

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

   751       have ?thesis .

   752     } moreover {

   753       assume eq_12: "t1 = t2"

   754       let ?t3 = "Suc t2"

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

   756       from moment_plus [OF this] 

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

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

   759       from nn2 [rule_format, OF this] and eq_m

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

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

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

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

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

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

   766       proof -

   767         from vt_moment 

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

   769         with eq_m show ?thesis by simp

   770       qed

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

   772           by (unfold_locales, auto, cases, simp)

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

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

   775         case True

   776         have "e = V thread cs2"

   777         proof -

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

   779               using True and np2  by auto 

   780           from vt_e.wq_out_inv[OF True this h2]

   781           show ?thesis .

   782         qed

   783         thus ?thesis by auto

   784       next

   785         case False

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

   787         thus ?thesis by auto

   788       qed

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

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

   791         case True

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

   793               using True and np1  by auto 

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

   795         have "e = V thread cs1" .

   796         thus ?thesis by auto

   797       next

   798         case False

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

   800         thus ?thesis by auto

   801       qed

   802       ultimately have ?thesis using neq12 by auto

   803     } ultimately show ?thesis using nat_neq_iff by blast 

   804   qed

   805 qed

   806 

   807 text {*

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

   809 *}

   810 

   811 lemma waiting_unique:

   812   assumes "waiting s th cs1"

   813   and "waiting s th cs2"

   814   shows "cs1 = cs2"

   815   using waiting_unique_pre assms

   816   unfolding wq_def s_waiting_def

   817   by auto

   818 

   819 end

   820 

   821 (* not used *)

   822 text {*

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

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

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

   826 *}

   827 lemma held_unique:

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

   829   and "holding s th2 cs"

   830   shows "th1 = th2"

   831  by (insert assms, unfold s_holding_def, auto)

   832 

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

   834   apply (induct s, auto)

   835   by (case_tac a, auto split:if_splits)

   836 

   837 lemma last_set_unique: 

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

   839           \<Longrightarrow> th1 = th2"

   840   apply (induct s, auto)

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

   842 

   843 lemma preced_unique : 

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

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

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

   847   shows "th1 = th2"

   848 proof -

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

   850   from last_set_unique [OF this th_in1 th_in2]

   851   show ?thesis .

   852 qed

   853                       

   854 lemma preced_linorder: 

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

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

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

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

   859 proof -

   860   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

   862   thus ?thesis by auto

   863 qed

   864 

   865 text {*

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

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

   868   events, respectively.

   869 *}

   870 

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

   872 apply (unfold s_RAG_def s_waiting_def wq_def)

   873 by (simp add:Let_def)

   874 

   875 lemma (in valid_trace_set)

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

   877    by (unfold is_set RAG_set_unchanged, simp)

   878 

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

   880 apply (unfold s_RAG_def s_waiting_def wq_def)

   881 by (simp add:Let_def)

   882 

   883 lemma (in valid_trace_create)

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

   885    by (unfold is_create RAG_create_unchanged, simp)

   886 

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

   888 apply (unfold s_RAG_def s_waiting_def wq_def)

   889 by (simp add:Let_def)

   890 

   891 lemma (in valid_trace_exit)

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

   893    by (unfold is_exit RAG_exit_unchanged, simp)

   894 

   895 context valid_trace_v

   896 begin

   897 

   898 lemma distinct_rest: "distinct rest"

   899   by (simp add: distinct_tl rest_def wq_distinct)

   900 

   901 lemma holding_cs_eq_th:

   902   assumes "holding s t cs"

   903   shows "t = th"

   904 proof -

   905   from pip_e[unfolded is_v]

   906   show ?thesis

   907   proof(cases)

   908     case (thread_V)

   909     from held_unique[OF this(2) assms]

   910     show ?thesis by simp

   911   qed

   912 qed

   913 

   914 lemma distinct_wq': "distinct wq'"

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

   916   

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

   918   by (metis (mono_tags, lifting) distinct_rest rest_def 

   919       some_eq_ex wq'_def)

   920     

   921 lemma th'_in_inv:

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

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

   924   using assms set_wq' by simp

   925 

   926 lemma neq_t_th: 

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

   928   shows "t \<noteq> th"

   929 proof

   930   assume otherwise: "t = th"

   931   show False

   932   proof(cases "c = cs")

   933     case True

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

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

   936      by simp 

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

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

   939     show ?thesis by simp

   940   next

   941     case False

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

   943         by (unfold is_v, simp)

   944     hence "waiting s t c" using assms 

   945         by (simp add: cs_waiting_def waiting_eq)

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

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

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

   949   qed

   950 qed

   951 

   952 lemma waiting_esI1:

   953   assumes "waiting s t c"

   954       and "c \<noteq> cs" 

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

   956 proof -

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

   958     using assms(2) is_v by auto

   959   with assms(1) show ?thesis 

   960     using cs_waiting_def waiting_eq by auto 

   961 qed

   962 

   963 lemma holding_esI2:

   964   assumes "c \<noteq> cs" 

   965   and "holding s t c"

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

   967 proof -

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

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

   970                 folded this, unfolded wq_def, folded s_holding_def]

   971   show ?thesis .

   972 qed

   973 

   974 lemma holding_esI1:

   975   assumes "holding s t c"

   976   and "t \<noteq> th"

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

   978 proof -

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

   980   from holding_esI2[OF this assms(1)]

   981   show ?thesis .

   982 qed

   983 

   984 end

   985 

   986 context valid_trace_v_n

   987 begin

   988 

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

   990 proof (unfold wq'_def, rule someI2)

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

   992     by (simp add: distinct_rest) 

   993 next

   994   fix x

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

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

   997 qed 

   998 

   999 definition "taker = hd wq'"

  1000 

  1001 definition "rest' = tl wq'"

  1002 

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

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

  1005 

  1006 lemma next_th_taker: 

  1007   shows "next_th s th cs taker"

  1008   using rest_nnl taker_def wq'_def wq_s_cs 

  1009   by (auto simp:next_th_def)

  1010 

  1011 lemma taker_unique: 

  1012   assumes "next_th s th cs taker'"

  1013   shows "taker' = taker"

  1014 proof -

  1015   from assms

  1016   obtain rest' where 

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

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

  1019           by (unfold next_th_def, auto)

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

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

  1022 qed

  1023 

  1024 lemma waiting_set_eq:

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

  1026   by (smt all_not_in_conv bot.extremum insertI1 insert_subset 

  1027       mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)

  1028 

  1029 lemma holding_set_eq:

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

  1031   using next_th_taker taker_def waiting_set_eq 

  1032   by fastforce

  1033    

  1034 lemma holding_taker:

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

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

  1037         auto simp:neq_wq' taker_def)

  1038 

  1039 lemma waiting_esI2:

  1040   assumes "waiting s t cs"

  1041       and "t \<noteq> taker"

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

  1043 proof -

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

  1045   proof(unfold wq'_def, rule someI2)

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

  1047           by (simp add: distinct_rest)

  1048   next

  1049     fix x

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

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

  1052         using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto 

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

  1054   qed

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

  1056     using assms(2) taker_def by auto 

  1057   ultimately show ?thesis

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

  1059 qed

  1060 

  1061 lemma waiting_esE:

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

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

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

  1065 proof(cases "c = cs")

  1066   case False

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

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

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

  1070 next

  1071   case True

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

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

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

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

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

  1077   ultimately have "waiting s t cs"

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

  1079                 list.set_sel(2) rest_def waiting_eq wq_s_cs)  

  1080   show ?thesis using that(2)

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

  1082 qed

  1083 

  1084 lemma holding_esI1:

  1085   assumes "c = cs"

  1086   and "t = taker"

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

  1088   by (unfold assms, simp add: holding_taker)

  1089 

  1090 lemma holding_esE:

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

  1092   obtains "c = cs" "t = taker"

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

  1094 proof(cases "c = cs")

  1095   case True

  1096   from assms[unfolded True, unfolded s_holding_def, 

  1097              folded wq_def, unfolded wq_es_cs]

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

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

  1100 next

  1101   case False

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

  1103   from assms[unfolded s_holding_def, folded wq_def, 

  1104              unfolded this, unfolded wq_def, folded s_holding_def]

  1105   have "holding s t c"  .

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

  1107 qed

  1108 

  1109 end 

  1110 

  1111 

  1112 context valid_trace_v_e

  1113 begin

  1114 

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

  1116 proof (unfold wq'_def, rule someI2)

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

  1118     by (simp add: distinct_rest) 

  1119 next

  1120   fix x

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

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

  1123 qed 

  1124 

  1125 lemma no_taker: 

  1126   assumes "next_th s th cs taker"

  1127   shows "False"

  1128 proof -

  1129   from assms[unfolded next_th_def]

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

  1131     by auto

  1132   thus ?thesis using rest_def rest_nil by auto 

  1133 qed

  1134 

  1135 lemma waiting_set_eq: