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 eq_RAG: 

    88   "RAG (wq s) = RAG s"

    89   by (unfold cs_RAG_def s_RAG_def, auto)

    90 

    91 lemma waiting_holding:

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

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

    94 proof -

    95   from assms[unfolded s_waiting_def, folded wq_def]

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

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

    98   hence "holding s th' cs" 

    99     by (unfold s_holding_def, fold wq_def, auto)

   100   from that[OF this] show ?thesis .

   101 qed

   102 

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

   104 unfolding cp_def wq_def

   105 apply(induct s rule: schs.induct)

   106 apply(simp add: Let_def cpreced_initial)

   107 apply(simp add: Let_def)

   108 apply(simp add: Let_def)

   109 apply(simp add: Let_def)

   110 apply(subst (2) schs.simps)

   111 apply(simp add: Let_def)

   112 apply(subst (2) schs.simps)

   113 apply(simp add: Let_def)

   114 done

   115 

   116 lemma cp_alt_def:

   117   "cp s th =  

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

   119 proof -

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

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

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

   123   proof -

   124     have "?L = ?R" 

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

   126     thus ?thesis by simp

   127   qed

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

   129 qed

   130 

   131 (* ccc *)

   132 

   133 

   134 locale valid_trace = 

   135   fixes s

   136   assumes vt : "vt s"

   137 

   138 locale valid_trace_e = valid_trace +

   139   fixes e

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

   141 begin

   142 

   143 lemma pip_e: "PIP s e"

   144   using vt_e by (cases, simp)  

   145 

   146 end

   147 

   148 locale valid_trace_create = valid_trace_e + 

   149   fixes th prio

   150   assumes is_create: "e = Create th prio"

   151 

   152 locale valid_trace_exit = valid_trace_e + 

   153   fixes th

   154   assumes is_exit: "e = Exit th"

   155 

   156 locale valid_trace_p = valid_trace_e + 

   157   fixes th cs

   158   assumes is_p: "e = P th cs"

   159 

   160 locale valid_trace_v = valid_trace_e + 

   161   fixes th cs

   162   assumes is_v: "e = V th cs"

   163 begin

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

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

   166 end

   167 

   168 locale valid_trace_v_n = valid_trace_v +

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

   170 

   171 locale valid_trace_v_e = valid_trace_v +

   172   assumes rest_nil: "rest = []"

   173 

   174 locale valid_trace_set= valid_trace_e + 

   175   fixes th prio

   176   assumes is_set: "e = Set th prio"

   177 

   178 context valid_trace

   179 begin

   180 

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

   182   assumes "PP []"

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

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

   185      shows "PP s"

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

   187   case Init

   188   from assms(1) show ?case .

   189 next

   190   case (Step s e)

   191   show ?case

   192   proof(rule assms(2))

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

   194   next

   195     show "PP s" using Step by simp

   196   next

   197     show "PIP s e" using Step by simp

   198   qed

   199 qed

   200 

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

   202 proof(induct rule:ind)

   203   case Nil

   204   thus ?case by (simp add:vt_nil)

   205 next

   206   case (Cons s e t)

   207   show ?case

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

   209     case True

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

   211     thus ?thesis using Cons

   212       by (simp add:valid_trace_def valid_trace_e_def, auto)

   213   next

   214     case False

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

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

   217     proof -

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

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

   220       show ?thesis by simp

   221     qed

   222     ultimately show ?thesis by simp

   223   qed

   224 qed

   225 

   226 lemma finite_threads:

   227   shows "finite (threads s)"

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

   229 

   230 end

   231 

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

   233   by (unfold s_RAG_def, auto)

   234 

   235 locale valid_moment = valid_trace + 

   236   fixes i :: nat

   237 

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

   239   by (unfold_locales, insert vt_moment, auto)

   240 

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

   242   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)

   243 

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

   245   by (unfold s_holding_def wq_def cs_holding_def, simp)

   246 

   247 lemma runing_ready: 

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

   249   unfolding runing_def readys_def

   250   by auto 

   251 

   252 lemma readys_threads:

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

   254   unfolding readys_def

   255   by auto

   256 

   257 lemma wq_v_neq [simp]:

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

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

   260 

   261 lemma runing_head:

   262   assumes "th \<in> runing s"

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

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

   265   using assms

   266   by (simp add:runing_def readys_def s_waiting_def wq_def)

   267 

   268 context valid_trace

   269 begin

   270 

   271 lemma runing_wqE:

   272   assumes "th \<in> runing s"

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

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

   275 proof -

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

   277     by (meson list.set_cases)

   278   have "th' = th"

   279   proof(rule ccontr)

   280     assume "th' \<noteq> th"

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

   282     with assms(2)

   283     have "waiting s th cs" 

   284       by (unfold s_waiting_def, fold wq_def, auto)

   285     with assms show False 

   286       by (unfold runing_def readys_def, auto)

   287   qed

   288   with eq_wq that show ?thesis by metis

   289 qed

   290 

   291 end

   292 

   293 context valid_trace_create

   294 begin

   295 

   296 lemma wq_neq_simp [simp]:

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

   298     using assms unfolding is_create wq_def

   299   by (auto simp:Let_def)

   300 

   301 lemma wq_distinct_kept:

   302   assumes "distinct (wq s cs')"

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

   304   using assms by simp

   305 end

   306 

   307 context valid_trace_exit

   308 begin

   309 

   310 lemma wq_neq_simp [simp]:

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

   312     using assms unfolding is_exit wq_def

   313   by (auto simp:Let_def)

   314 

   315 lemma wq_distinct_kept:

   316   assumes "distinct (wq s cs')"

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

   318   using assms by simp

   319 end

   320 

   321 context valid_trace_p

   322 begin

   323 

   324 lemma wq_neq_simp [simp]:

   325   assumes "cs' \<noteq> cs"

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

   327     using assms unfolding is_p wq_def

   328   by (auto simp:Let_def)

   329 

   330 lemma runing_th_s:

   331   shows "th \<in> runing s"

   332 proof -

   333   from pip_e[unfolded is_p]

   334   show ?thesis by (cases, simp)

   335 qed

   336 

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

   338   using runing_th_s

   339   by (unfold runing_def, auto)

   340 

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

   342   using readys_threads ready_th_s by auto

   343 

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

   345   using live_th_s 

   346   by (unfold is_p, simp)

   347 

   348 lemma th_not_waiting: 

   349   "\<not> waiting s th c"

   350 proof -

   351   have "th \<in> readys s"

   352     using runing_ready runing_th_s by blast 

   353   thus ?thesis

   354     by (unfold readys_def, auto)

   355 qed

   356 

   357 lemma waiting_neq_th: 

   358   assumes "waiting s t c"

   359   shows "t \<noteq> th"

   360   using assms using th_not_waiting by blast 

   361 

   362 lemma th_not_in_wq: 

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

   364 proof

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

   366   from runing_wqE[OF runing_th_s this]

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

   368   with otherwise

   369   have "holding s th cs"

   370     by (unfold s_holding_def, fold wq_def, simp)

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

   372     by (unfold s_RAG_def, fold holding_eq, auto)

   373   from pip_e[unfolded is_p]

   374   show False

   375   proof(cases)

   376     case (thread_P)

   377     with cs_th_RAG show ?thesis by auto

   378   qed

   379 qed

   380 

   381 lemma wq_es_cs: 

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

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

   384 

   385 lemma wq_distinct_kept:

   386   assumes "distinct (wq s cs')"

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

   388 proof(cases "cs' = cs")

   389   case True

   390   show ?thesis using True assms th_not_in_wq

   391     by (unfold True wq_es_cs, auto)

   392 qed (insert assms, simp)

   393 

   394 end

   395 

   396 context valid_trace_v

   397 begin

   398 

   399 lemma wq_neq_simp [simp]:

   400   assumes "cs' \<noteq> cs"

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

   402     using assms unfolding is_v wq_def

   403   by (auto simp:Let_def)

   404 

   405 lemma runing_th_s:

   406   shows "th \<in> runing s"

   407 proof -

   408   from pip_e[unfolded is_v]

   409   show ?thesis by (cases, simp)

   410 qed

   411 

   412 lemma th_not_waiting: 

   413   "\<not> waiting s th c"

   414 proof -

   415   have "th \<in> readys s"

   416     using runing_ready runing_th_s by blast 

   417   thus ?thesis

   418     by (unfold readys_def, auto)

   419 qed

   420 

   421 lemma waiting_neq_th: 

   422   assumes "waiting s t c"

   423   shows "t \<noteq> th"

   424   using assms using th_not_waiting by blast 

   425 

   426 lemma wq_s_cs:

   427   "wq s cs = th#rest"

   428 proof -

   429   from pip_e[unfolded is_v]

   430   show ?thesis

   431   proof(cases)

   432     case (thread_V)

   433     from this(2) show ?thesis

   434       by (unfold rest_def s_holding_def, fold wq_def,

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

   436   qed

   437 qed

   438 

   439 lemma wq_es_cs:

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

   441  using wq_s_cs[unfolded wq_def]

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

   443 

   444 lemma wq_distinct_kept:

   445   assumes "distinct (wq s cs')"

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

   447 proof(cases "cs' = cs")

   448   case True

   449   show ?thesis

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

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

   452         using assms[unfolded True wq_s_cs] by auto

   453   qed simp

   454 qed (insert assms, simp)

   455 

   456 end

   457 

   458 context valid_trace_set

   459 begin

   460 

   461 lemma wq_neq_simp [simp]:

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

   463     using assms unfolding is_set wq_def

   464   by (auto simp:Let_def)

   465 

   466 lemma wq_distinct_kept:

   467   assumes "distinct (wq s cs')"

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

   469   using assms by simp

   470 end

   471 

   472 context valid_trace

   473 begin

   474 

   475 lemma actor_inv: 

   476   assumes "PIP s e"

   477   and "\<not> isCreate e"

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

   479   using assms

   480   by (induct, auto)

   481 

   482 lemma isP_E:

   483   assumes "isP e"

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

   485   using assms by (cases e, auto)

   486 

   487 lemma isV_E:

   488   assumes "isV e"

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

   490   using assms by (cases e, auto) 

   491 

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

   493 proof(induct rule:ind)

   494   case (Cons s e)

   495   interpret vt_e: valid_trace_e s e using Cons by simp

   496   show ?case 

   497   proof(cases e)

   498     case (Create th prio)

   499     interpret vt_create: valid_trace_create s e th prio 

   500       using Create by (unfold_locales, simp)

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

   502   next

   503     case (Exit th)

   504     interpret vt_exit: valid_trace_exit s e th  

   505         using Exit by (unfold_locales, simp)

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

   507   next

   508     case (P th cs)

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

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

   511   next

   512     case (V th cs)

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

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

   515   next

   516     case (Set th prio)

   517     interpret vt_set: valid_trace_set s e th prio

   518         using Set by (unfold_locales, simp)

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

   520   qed

   521 qed (unfold wq_def Let_def, simp)

   522 

   523 end

   524 

   525 context valid_trace_e

   526 begin

   527 

   528 text {*

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

   530   operation can add new thread into waiting queues. 

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

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

   533 *}

   534 

   535 lemma wq_in_inv: 

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

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

   538   shows "e = P thread cs"

   539 proof(cases e)

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

   541   case (V th cs1)

   542   have False

   543   proof(cases "cs1 = cs")

   544     case True

   545     show ?thesis

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

   547       case (Cons w_hd w_tl)

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

   549       proof -

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

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

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

   553         proof(rule someI2)

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

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

   556         qed (insert Cons True, auto)

   557         ultimately show ?thesis by simp

   558       qed

   559       with assms show ?thesis by auto

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

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

   562   thus ?thesis by auto

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

   564 

   565 lemma wq_out_inv: 

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

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

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

   569   shows "e = V thread cs"

   570 proof(cases e)

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

   572   case (V th cs1)

   573   show ?thesis

   574   proof(cases "cs1 = cs")

   575     case True

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

   577     thus ?thesis

   578     proof(cases)

   579       case (thread_V)

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

   581           by (unfold s_holding_def wq_def, simp)

   582       ultimately show ?thesis using V True by simp

   583     qed

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

   585 next

   586   case (P th cs1)

   587   show ?thesis

   588   proof(cases "cs1 = cs")

   589     case True

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

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

   592     with s_i s_hd s_in have False

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

   594     thus ?thesis by simp

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

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

   597 

   598 end

   599 

   600 

   601 context valid_trace

   602 begin

   603 

   604 

   605 text {* (* ddd *)

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

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

   608   For instance, the fact 

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

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

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

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

   613 

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

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

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

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

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

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

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

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

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

   623 

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

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

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

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

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

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

   630   and kept on blocked on them respectively ever since.

   631  

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

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

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

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

   636 *}

   637 

   638 lemma waiting_unique_pre: (* ddd *)

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

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

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

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

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

   644   shows "False"

   645 proof -

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

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

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

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

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

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

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

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

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

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

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

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

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

   659   { fix s cs

   660     assume q: "?Q cs s"

   661     have "thread \<notin> runing s"

   662     proof

   663       assume "thread \<in> runing s"

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

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

   666         by (unfold runing_def s_waiting_def readys_def, auto)

   667       from this[rule_format, of cs] q 

   668       show False by (simp add: wq_def) 

   669     qed

   670   } note q_not_runing = this

   671   { fix t1 t2 cs1 cs2

   672     assume  lt1: "t1 < length s"

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

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

   675     and lt2: "t2 < length s"

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

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

   678     and lt12: "t1 < t2"

   679     let ?t3 = "Suc t2"

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

   681     from moment_plus [OF this] 

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

   683     have "t2 < ?t3" by simp

   684     from nn2 [rule_format, OF this] and eq_m

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

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

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

   688     proof -

   689       from vt_moment 

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

   691       with eq_m show ?thesis by simp

   692     qed

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

   694         by (unfold_locales, auto, cases, simp)

   695     have ?thesis

   696     proof -

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

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

   699         case True

   700         have "e = V thread cs2"

   701         proof -

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

   703               using True and np2  by auto 

   704           from vt_e.wq_out_inv[OF True this h2]

   705           show ?thesis .

   706         qed

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

   708       next

   709         case False

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

   711         with vt_e.actor_inv[OF vt_e.pip_e]

   712         show ?thesis by auto

   713       qed

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

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

   716       ultimately show ?thesis by simp

   717     qed

   718   } note lt_case = this

   719   show ?thesis

   720   proof -

   721     { assume "t1 < t2"

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

   723       have ?thesis .

   724     } moreover {

   725       assume "t2 < t1"

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

   727       have ?thesis .

   728     } moreover {

   729       assume eq_12: "t1 = t2"

   730       let ?t3 = "Suc t2"

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

   732       from moment_plus [OF this] 

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

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

   735       from nn2 [rule_format, OF this] and eq_m

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

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

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

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

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

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

   742       proof -

   743         from vt_moment 

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

   745         with eq_m show ?thesis by simp

   746       qed

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

   748           by (unfold_locales, auto, cases, simp)

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

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

   751         case True

   752         have "e = V thread cs2"

   753         proof -

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

   755               using True and np2  by auto 

   756           from vt_e.wq_out_inv[OF True this h2]

   757           show ?thesis .

   758         qed

   759         thus ?thesis by auto

   760       next

   761         case False

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

   763         thus ?thesis by auto

   764       qed

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

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

   767         case True

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

   769               using True and np1  by auto 

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

   771         have "e = V thread cs1" .

   772         thus ?thesis by auto

   773       next

   774         case False

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

   776         thus ?thesis by auto

   777       qed

   778       ultimately have ?thesis using neq12 by auto

   779     } ultimately show ?thesis using nat_neq_iff by blast 

   780   qed

   781 qed

   782 

   783 text {*

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

   785 *}

   786 

   787 lemma waiting_unique:

   788   assumes "waiting s th cs1"

   789   and "waiting s th cs2"

   790   shows "cs1 = cs2"

   791   using waiting_unique_pre assms

   792   unfolding wq_def s_waiting_def

   793   by auto

   794 

   795 end

   796 

   797 (* not used *)

   798 text {*

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

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

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

   802 *}

   803 lemma held_unique:

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

   805   and "holding s th2 cs"

   806   shows "th1 = th2"

   807  by (insert assms, unfold s_holding_def, auto)

   808 

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

   810   apply (induct s, auto)

   811   by (case_tac a, auto split:if_splits)

   812 

   813 lemma last_set_unique: 

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

   815           \<Longrightarrow> th1 = th2"

   816   apply (induct s, auto)

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

   818 

   819 lemma preced_unique : 

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

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

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

   823   shows "th1 = th2"

   824 proof -

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

   826   from last_set_unique [OF this th_in1 th_in2]

   827   show ?thesis .

   828 qed

   829                       

   830 lemma preced_linorder: 

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

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

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

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

   835 proof -

   836   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

   838   thus ?thesis by auto

   839 qed

   840 

   841 text {*

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

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

   844   events, respectively.

   845 *}

   846 

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

   848 apply (unfold s_RAG_def s_waiting_def wq_def)

   849 by (simp add:Let_def)

   850 

   851 lemma (in valid_trace_set)

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

   853    by (unfold is_set RAG_set_unchanged, simp)

   854 

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

   856 apply (unfold s_RAG_def s_waiting_def wq_def)

   857 by (simp add:Let_def)

   858 

   859 lemma (in valid_trace_create)

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

   861    by (unfold is_create RAG_create_unchanged, simp)

   862 

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

   864 apply (unfold s_RAG_def s_waiting_def wq_def)

   865 by (simp add:Let_def)

   866 

   867 lemma (in valid_trace_exit)

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

   869    by (unfold is_exit RAG_exit_unchanged, simp)

   870 

   871 context valid_trace_v

   872 begin

   873 

   874 lemma distinct_rest: "distinct rest"

   875   by (simp add: distinct_tl rest_def wq_distinct)

   876 

   877 lemma holding_cs_eq_th:

   878   assumes "holding s t cs"

   879   shows "t = th"

   880 proof -

   881   from pip_e[unfolded is_v]

   882   show ?thesis

   883   proof(cases)

   884     case (thread_V)

   885     from held_unique[OF this(2) assms]

   886     show ?thesis by simp

   887   qed

   888 qed

   889 

   890 lemma distinct_wq': "distinct wq'"

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

   892   

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

   894   by (metis (mono_tags, lifting) distinct_rest rest_def 

   895       some_eq_ex wq'_def)

   896     

   897 lemma th'_in_inv:

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

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

   900   using assms set_wq' by simp

   901 

   902 lemma neq_t_th: 

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

   904   shows "t \<noteq> th"

   905 proof

   906   assume otherwise: "t = th"

   907   show False

   908   proof(cases "c = cs")

   909     case True

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

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

   912      by simp 

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

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

   915     show ?thesis by simp

   916   next

   917     case False

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

   919         by (unfold is_v, simp)

   920     hence "waiting s t c" using assms 

   921         by (simp add: cs_waiting_def waiting_eq)

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

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

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

   925   qed

   926 qed

   927 

   928 lemma waiting_esI1:

   929   assumes "waiting s t c"

   930       and "c \<noteq> cs" 

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

   932 proof -

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

   934     using assms(2) is_v by auto

   935   with assms(1) show ?thesis 

   936     using cs_waiting_def waiting_eq by auto 

   937 qed

   938 

   939 lemma holding_esI2:

   940   assumes "c \<noteq> cs" 

   941   and "holding s t c"

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

   943 proof -

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

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

   946                 folded this, unfolded wq_def, folded s_holding_def]

   947   show ?thesis .

   948 qed

   949 

   950 lemma holding_esI1:

   951   assumes "holding s t c"

   952   and "t \<noteq> th"

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

   954 proof -

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

   956   from holding_esI2[OF this assms(1)]

   957   show ?thesis .

   958 qed

   959 

   960 end

   961 

   962 context valid_trace_v_n

   963 begin

   964 

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

   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 \<noteq> []" using rest_nnl by auto

   973 qed 

   974 

   975 definition "taker = hd wq'"

   976 

   977 definition "rest' = tl wq'"

   978 

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

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

   981 

   982 lemma next_th_taker: 

   983   shows "next_th s th cs taker"

   984   using rest_nnl taker_def wq'_def wq_s_cs 

   985   by (auto simp:next_th_def)

   986 

   987 lemma taker_unique: 

   988   assumes "next_th s th cs taker'"

   989   shows "taker' = taker"

   990 proof -

   991   from assms

   992   obtain rest' where 

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

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

   995           by (unfold next_th_def, auto)

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

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

   998 qed

   999 

  1000 lemma waiting_set_eq:

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

  1002   by (smt all_not_in_conv bot.extremum insertI1 insert_subset 

  1003       mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)

  1004 

  1005 lemma holding_set_eq:

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

  1007   using next_th_taker taker_def waiting_set_eq 

  1008   by fastforce

  1009    

  1010 lemma holding_taker:

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

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

  1013         auto simp:neq_wq' taker_def)

  1014 

  1015 lemma waiting_esI2:

  1016   assumes "waiting s t cs"

  1017       and "t \<noteq> taker"

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

  1019 proof -

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

  1021   proof(unfold wq'_def, rule someI2)

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

  1023           by (simp add: distinct_rest)

  1024   next

  1025     fix x

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

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

  1028         using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto 

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

  1030   qed

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

  1032     using assms(2) taker_def by auto 

  1033   ultimately show ?thesis

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

  1035 qed

  1036 

  1037 lemma waiting_esE:

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

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

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

  1041 proof(cases "c = cs")

  1042   case False

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

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

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

  1046 next

  1047   case True

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

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

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

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

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

  1053   ultimately have "waiting s t cs"

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

  1055                 list.set_sel(2) rest_def waiting_eq wq_s_cs)  

  1056   show ?thesis using that(2)

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

  1058 qed

  1059 

  1060 lemma holding_esI1:

  1061   assumes "c = cs"

  1062   and "t = taker"

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

  1064   by (unfold assms, simp add: holding_taker)

  1065 

  1066 lemma holding_esE:

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

  1068   obtains "c = cs" "t = taker"

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

  1070 proof(cases "c = cs")

  1071   case True

  1072   from assms[unfolded True, unfolded s_holding_def, 

  1073              folded wq_def, unfolded wq_es_cs]

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

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

  1076 next

  1077   case False

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

  1079   from assms[unfolded s_holding_def, folded wq_def, 

  1080              unfolded this, unfolded wq_def, folded s_holding_def]

  1081   have "holding s t c"  .

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

  1083 qed

  1084 

  1085 end 

  1086 

  1087 

  1088 context valid_trace_v_e

  1089 begin

  1090 

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

  1092 proof (unfold wq'_def, rule someI2)

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

  1094     by (simp add: distinct_rest) 

  1095 next

  1096   fix x

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

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

  1099 qed 

  1100 

  1101 lemma no_taker: 

  1102   assumes "next_th s th cs taker"

  1103   shows "False"

  1104 proof -

  1105   from assms[unfolded next_th_def]

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

  1107     by auto

  1108   thus ?thesis using rest_def rest_nil by auto 

  1109 qed

  1110 

  1111 lemma waiting_set_eq:

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

  1113   using no_taker by auto

  1114 

  1115 lemma holding_set_eq:

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

  1117   using no_taker by auto

  1118    

  1119 lemma no_holding:

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

  1121   shows False

  1122 proof -

  1123   from wq_es_cs[unfolded nil_wq']

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

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

  1126   show ?thesis by auto

  1127 qed

  1128 

  1129 lemma no_waiting:

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

  1131   shows False

  1132 proof -

  1133   from wq_es_cs[unfolded nil_wq']

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

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