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 (* I am going to use this file as a start point to retrofiting 

    19    PIPBasics.thy, which is originally called CpsG.ghy *)

    20 

    21 locale valid_trace = 

    22   fixes s

    23   assumes vt : "vt s"

    24 

    25 locale valid_trace_e = valid_trace +

    26   fixes e

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

    28 begin

    29 

    30 lemma pip_e: "PIP s e"

    31   using vt_e by (cases, simp)  

    32 

    33 end

    34 

    35 locale valid_trace_create = valid_trace_e + 

    36   fixes th prio

    37   assumes is_create: "e = Create th prio"

    38 

    39 locale valid_trace_exit = valid_trace_e + 

    40   fixes th

    41   assumes is_exit: "e = Exit th"

    42 

    43 locale valid_trace_p = valid_trace_e + 

    44   fixes th cs

    45   assumes is_p: "e = P th cs"

    46 

    47 locale valid_trace_v = valid_trace_e + 

    48   fixes th cs

    49   assumes is_v: "e = V th cs"

    50 begin

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

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

    53 end

    54 

    55 locale valid_trace_v_n = valid_trace_v +

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

    57 

    58 locale valid_trace_v_e = valid_trace_v +

    59   assumes rest_nil: "rest = []"

    60 

    61 locale valid_trace_set= valid_trace_e + 

    62   fixes th prio

    63   assumes is_set: "e = Set th prio"

    64 

    65 context valid_trace

    66 begin

    67 

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

    69   assumes "PP []"

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

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

    72      shows "PP s"

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

    74   case Init

    75   from assms(1) show ?case .

    76 next

    77   case (Step s e)

    78   show ?case

    79   proof(rule assms(2))

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

    81   next

    82     show "PP s" using Step by simp

    83   next

    84     show "PIP s e" using Step by simp

    85   qed

    86 qed

    87 

    88 end

    89 

    90 

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

    92   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)

    93 

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

    95   by (unfold s_holding_def wq_def cs_holding_def, simp)

    96 

    97 lemma runing_ready: 

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

    99   unfolding runing_def readys_def

   100   by auto 

   101 

   102 lemma readys_threads:

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

   104   unfolding readys_def

   105   by auto

   106 

   107 lemma wq_v_neq [simp]:

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

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

   110 

   111 lemma runing_head:

   112   assumes "th \<in> runing s"

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

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

   115   using assms

   116   by (simp add:runing_def readys_def s_waiting_def wq_def)

   117 

   118 context valid_trace

   119 begin

   120 

   121 lemma runing_wqE:

   122   assumes "th \<in> runing s"

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

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

   125 proof -

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

   127     by (meson list.set_cases)

   128   have "th' = th"

   129   proof(rule ccontr)

   130     assume "th' \<noteq> th"

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

   132     with assms(2)

   133     have "waiting s th cs" 

   134       by (unfold s_waiting_def, fold wq_def, auto)

   135     with assms show False 

   136       by (unfold runing_def readys_def, auto)

   137   qed

   138   with eq_wq that show ?thesis by metis

   139 qed

   140 

   141 end

   142 

   143 context valid_trace_p

   144 begin

   145 

   146 lemma wq_neq_simp [simp]:

   147   assumes "cs' \<noteq> cs"

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

   149     using assms unfolding is_p wq_def

   150   by (auto simp:Let_def)

   151 

   152 lemma runing_th_s:

   153   shows "th \<in> runing s"

   154 proof -

   155   from pip_e[unfolded is_p]

   156   show ?thesis by (cases, simp)

   157 qed

   158 

   159 lemma th_not_waiting: 

   160   "\<not> waiting s th c"

   161 proof -

   162   have "th \<in> readys s"

   163     using runing_ready runing_th_s by blast 

   164   thus ?thesis

   165     by (unfold readys_def, auto)

   166 qed

   167 

   168 lemma waiting_neq_th: 

   169   assumes "waiting s t c"

   170   shows "t \<noteq> th"

   171   using assms using th_not_waiting by blast 

   172 

   173 lemma th_not_in_wq: 

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

   175 proof

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

   177   from runing_wqE[OF runing_th_s this]

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

   179   with otherwise

   180   have "holding s th cs"

   181     by (unfold s_holding_def, fold wq_def, simp)

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

   183     by (unfold s_RAG_def, fold holding_eq, auto)

   184   from pip_e[unfolded is_p]

   185   show False

   186   proof(cases)

   187     case (thread_P)

   188     with cs_th_RAG show ?thesis by auto

   189   qed

   190 qed

   191 

   192 lemma wq_es_cs: 

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

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

   195 

   196 lemma wq_distinct_kept:

   197   assumes "distinct (wq s cs')"

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

   199 proof(cases "cs' = cs")

   200   case True

   201   show ?thesis using True assms th_not_in_wq

   202     by (unfold True wq_es_cs, auto)

   203 qed (insert assms, simp)

   204 

   205 end

   206 

   207 

   208 context valid_trace_v

   209 begin

   210 

   211 lemma wq_neq_simp [simp]:

   212   assumes "cs' \<noteq> cs"

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

   214     using assms unfolding is_v wq_def

   215   by (auto simp:Let_def)

   216 

   217 lemma runing_th_s:

   218   shows "th \<in> runing s"

   219 proof -

   220   from pip_e[unfolded is_v]

   221   show ?thesis by (cases, simp)

   222 qed

   223 

   224 lemma th_not_waiting: 

   225   "\<not> waiting s th c"

   226 proof -

   227   have "th \<in> readys s"

   228     using runing_ready runing_th_s by blast 

   229   thus ?thesis

   230     by (unfold readys_def, auto)

   231 qed

   232 

   233 lemma waiting_neq_th: 

   234   assumes "waiting s t c"

   235   shows "t \<noteq> th"

   236   using assms using th_not_waiting by blast 

   237 

   238 lemma wq_s_cs:

   239   "wq s cs = th#rest"

   240 proof -

   241   from pip_e[unfolded is_v]

   242   show ?thesis

   243   proof(cases)

   244     case (thread_V)

   245     from this(2) show ?thesis

   246       by (unfold rest_def s_holding_def, fold wq_def,

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

   248   qed

   249 qed

   250 

   251 lemma wq_es_cs:

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

   253  using wq_s_cs[unfolded wq_def]

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

   255 

   256 lemma wq_distinct_kept:

   257   assumes "distinct (wq s cs')"

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

   259 proof(cases "cs' = cs")

   260   case True

   261   show ?thesis

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

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

   264         using assms[unfolded True wq_s_cs] by auto

   265   qed simp

   266 qed (insert assms, simp)

   267 

   268 end

   269 

   270 context valid_trace

   271 begin

   272 

   273 lemma actor_inv: 

   274   assumes "PIP s e"

   275   and "\<not> isCreate e"

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

   277   using assms

   278   by (induct, auto)

   279 

   280 lemma isP_E:

   281   assumes "isP e"

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

   283   using assms by (cases e, auto)

   284 

   285 lemma isV_E:

   286   assumes "isV e"

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

   288   using assms by (cases e, auto) 

   289 

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

   291 proof(induct rule:ind)

   292   case (Cons s e)

   293   interpret vt_e: valid_trace_e s e using Cons by simp

   294   show ?case 

   295   proof(cases e)

   296     case (V th cs)

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

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

   299   qed

   300 qed (unfold wq_def Let_def, simp)

   301 

   302 end

   303 

   304 context valid_trace_e

   305 begin

   306 

   307 text {*

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

   309   operation can add new thread into waiting queues. 

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

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

   312 *}

   313 

   314 lemma wq_in_inv: 

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

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

   317   shows "e = P thread cs"

   318 proof(cases e)

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

   320   case (V th cs1)

   321   have False

   322   proof(cases "cs1 = cs")

   323     case True

   324     show ?thesis

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

   326       case (Cons w_hd w_tl)

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

   328       proof -

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

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

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

   332         proof(rule someI2)

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

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

   335         qed (insert Cons True, auto)

   336         ultimately show ?thesis by simp

   337       qed

   338       with assms show ?thesis by auto

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

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

   341   thus ?thesis by auto

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

   343 

   344 lemma wq_out_inv: 

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

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

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

   348   shows "e = V thread cs"

   349 proof(cases e)

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

   351   case (V th cs1)

   352   show ?thesis

   353   proof(cases "cs1 = cs")

   354     case True

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

   356     thus ?thesis

   357     proof(cases)

   358       case (thread_V)

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

   360           by (unfold s_holding_def wq_def, simp)

   361       ultimately show ?thesis using V True by simp

   362     qed

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

   364 next

   365   case (P th cs1)

   366   show ?thesis

   367   proof(cases "cs1 = cs")

   368     case True

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

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

   371     with s_i s_hd s_in have False

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

   373     thus ?thesis by simp

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

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

   376 

   377 end

   378 

   379 

   380 context valid_trace

   381 begin

   382 

   383 end

   384 

   385 

   386 

   387 context valid_trace

   388 begin

   389 

   390 

   391 text {* (* ddd *)

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

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

   394   For instance, the fact 

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

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

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

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

   399 

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

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

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

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

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

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

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

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

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

   409 

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

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

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

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

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

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

   416   and kept on blocked on them respectively ever since.

   417  

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

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

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

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

   422 *}

   423 

   424 lemma waiting_unique_pre: (* ddd *)

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

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

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

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

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

   430   shows "False"

   431 proof -

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

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

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

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

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

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

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

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

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

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

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

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

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

   445   { fix s cs

   446     assume q: "?Q cs s"

   447     have "thread \<notin> runing s"

   448     proof

   449       assume "thread \<in> runing s"

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

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

   452         by (unfold runing_def s_waiting_def readys_def, auto)

   453       from this[rule_format, of cs] q 

   454       show False by (simp add: wq_def) 

   455     qed

   456   } note q_not_runing = this

   457   { fix t1 t2 cs1 cs2

   458     assume  lt1: "t1 < length s"

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

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

   461     and lt2: "t2 < length s"

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

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

   464     and lt12: "t1 < t2"

   465     let ?t3 = "Suc t2"

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

   467     from moment_plus [OF this] 

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

   469     have "t2 < ?t3" by simp

   470     from nn2 [rule_format, OF this] and eq_m

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

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

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

   474     proof -

   475       from vt_moment 

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

   477       with eq_m show ?thesis by simp

   478     qed

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

   480         by (unfold_locales, auto, cases, simp)

   481     have ?thesis

   482     proof -

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

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

   485         case True

   486         have "e = V thread cs2"

   487         proof -

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

   489               using True and np2  by auto 

   490           from vt_e.wq_out_inv[OF True this h2]

   491           show ?thesis .

   492         qed

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

   494       next

   495         case False

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

   497         with vt_e.actor_inv[OF vt_e.pip_e]

   498         show ?thesis by auto

   499       qed

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

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

   502       ultimately show ?thesis by simp

   503     qed

   504   } note lt_case = this

   505   show ?thesis

   506   proof -

   507     { assume "t1 < t2"

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

   509       have ?thesis .

   510     } moreover {

   511       assume "t2 < t1"

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

   513       have ?thesis .

   514     } moreover {

   515       assume eq_12: "t1 = t2"

   516       let ?t3 = "Suc t2"

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

   518       from moment_plus [OF this] 

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

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

   521       from nn2 [rule_format, OF this] and eq_m

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

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

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

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

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

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

   528       proof -

   529         from vt_moment 

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

   531         with eq_m show ?thesis by simp

   532       qed

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

   534           by (unfold_locales, auto, cases, simp)

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

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

   537         case True

   538         have "e = V thread cs2"

   539         proof -

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

   541               using True and np2  by auto 

   542           from vt_e.wq_out_inv[OF True this h2]

   543           show ?thesis .

   544         qed

   545         thus ?thesis by auto

   546       next

   547         case False

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

   549         thus ?thesis by auto

   550       qed

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

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

   553         case True

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

   555               using True and np1  by auto 

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

   557         have "e = V thread cs1" .

   558         thus ?thesis by auto

   559       next

   560         case False

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

   562         thus ?thesis by auto

   563       qed

   564       ultimately have ?thesis using neq12 by auto

   565     } ultimately show ?thesis using nat_neq_iff by blast 

   566   qed

   567 qed

   568 

   569 text {*

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

   571 *}

   572 

   573 lemma waiting_unique:

   574   assumes "waiting s th cs1"

   575   and "waiting s th cs2"

   576   shows "cs1 = cs2"

   577   using waiting_unique_pre assms

   578   unfolding wq_def s_waiting_def

   579   by auto

   580 

   581 end

   582 

   583 (* not used *)

   584 text {*

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

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

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

   588 *}

   589 lemma held_unique:

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

   591   and "holding s th2 cs"

   592   shows "th1 = th2"

   593  by (insert assms, unfold s_holding_def, auto)

   594 

   595 

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

   597   apply (induct s, auto)

   598   by (case_tac a, auto split:if_splits)

   599 

   600 lemma last_set_unique: 

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

   602           \<Longrightarrow> th1 = th2"

   603   apply (induct s, auto)

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

   605 

   606 lemma preced_unique : 

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

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

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

   610   shows "th1 = th2"

   611 proof -

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

   613   from last_set_unique [OF this th_in1 th_in2]

   614   show ?thesis .

   615 qed

   616                       

   617 lemma preced_linorder: 

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

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

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

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

   622 proof -

   623   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

   625   thus ?thesis by auto

   626 qed

   627 

   628 (* An aux lemma used later *) 

   629 lemma unique_minus:

   630   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

   631   and xy: "(x, y) \<in> r"

   632   and xz: "(x, z) \<in> r^+"

   633   and neq: "y \<noteq> z"

   634   shows "(y, z) \<in> r^+"

   635 proof -

   636  from xz and neq show ?thesis

   637  proof(induct)

   638    case (base ya)

   639    have "(x, ya) \<in> r" by fact

   640    from unique [OF xy this] have "y = ya" .

   641    with base show ?case by auto

   642  next

   643    case (step ya z)

   644    show ?case

   645    proof(cases "y = ya")

   646      case True

   647      from step True show ?thesis by simp

   648    next

   649      case False

   650      from step False

   651      show ?thesis by auto

   652    qed

   653  qed

   654 qed

   655 

   656 lemma unique_base:

   657   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

   658   and xy: "(x, y) \<in> r"

   659   and xz: "(x, z) \<in> r^+"

   660   and neq_yz: "y \<noteq> z"

   661   shows "(y, z) \<in> r^+"

   662 proof -

   663   from xz neq_yz show ?thesis

   664   proof(induct)

   665     case (base ya)

   666     from xy unique base show ?case by auto

   667   next

   668     case (step ya z)

   669     show ?case

   670     proof(cases "y = ya")

   671       case True

   672       from True step show ?thesis by auto

   673     next

   674       case False

   675       from False step 

   676       have "(y, ya) \<in> r\<^sup>+" by auto

   677       with step show ?thesis by auto

   678     qed

   679   qed

   680 qed

   681 

   682 lemma unique_chain:

   683   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

   684   and xy: "(x, y) \<in> r^+"

   685   and xz: "(x, z) \<in> r^+"

   686   and neq_yz: "y \<noteq> z"

   687   shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+"

   688 proof -

   689   from xy xz neq_yz show ?thesis

   690   proof(induct)

   691     case (base y)

   692     have h1: "(x, y) \<in> r" and h2: "(x, z) \<in> r\<^sup>+" and h3: "y \<noteq> z" using base by auto

   693     from unique_base [OF _ h1 h2 h3] and unique show ?case by auto

   694   next

   695     case (step y za)

   696     show ?case

   697     proof(cases "y = z")

   698       case True

   699       from True step show ?thesis by auto

   700     next

   701       case False

   702       from False step have "(y, z) \<in> r\<^sup>+ \<or> (z, y) \<in> r\<^sup>+" by auto

   703       thus ?thesis

   704       proof

   705         assume "(z, y) \<in> r\<^sup>+"

   706         with step have "(z, za) \<in> r\<^sup>+" by auto

   707         thus ?thesis by auto

   708       next

   709         assume h: "(y, z) \<in> r\<^sup>+"

   710         from step have yza: "(y, za) \<in> r" by simp

   711         from step have "za \<noteq> z" by simp

   712         from unique_minus [OF _ yza h this] and unique

   713         have "(za, z) \<in> r\<^sup>+" by auto

   714         thus ?thesis by auto

   715       qed

   716     qed

   717   qed

   718 qed

   719 

   720 text {*

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

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

   723   events, respectively.

   724 *}

   725 

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

   727 apply (unfold s_RAG_def s_waiting_def wq_def)

   728 by (simp add:Let_def)

   729 

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

   731 apply (unfold s_RAG_def s_waiting_def wq_def)

   732 by (simp add:Let_def)

   733 

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

   735 apply (unfold s_RAG_def s_waiting_def wq_def)

   736 by (simp add:Let_def)

   737 

   738 

   739 

   740 context valid_trace_v

   741 begin

   742 

   743 

   744 lemma distinct_rest: "distinct rest"

   745   by (simp add: distinct_tl rest_def wq_distinct)

   746 

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

   748 

   749 lemma runing_th_s:

   750   shows "th \<in> runing s"

   751 proof -

   752   from pip_e[unfolded is_v]

   753   show ?thesis by (cases, simp)

   754 qed

   755 

   756 lemma holding_cs_eq_th:

   757   assumes "holding s t cs"

   758   shows "t = th"

   759 proof -

   760   from pip_e[unfolded is_v]

   761   show ?thesis

   762   proof(cases)

   763     case (thread_V)

   764     from held_unique[OF this(2) assms]

   765     show ?thesis by simp

   766   qed

   767 qed

   768 

   769 lemma th_not_waiting: 

   770   "\<not> waiting s th c"

   771 proof -

   772   have "th \<in> readys s"

   773     using runing_ready runing_th_s by blast 

   774   thus ?thesis

   775     by (unfold readys_def, auto)

   776 qed

   777 

   778 lemma waiting_neq_th: 

   779   assumes "waiting s t c"

   780   shows "t \<noteq> th"

   781   using assms using th_not_waiting by blast 

   782 

   783 lemma wq_s_cs:

   784   "wq s cs = th#rest"

   785 proof -

   786   from pip_e[unfolded is_v]

   787   show ?thesis

   788   proof(cases)

   789     case (thread_V)

   790     from this(2) show ?thesis

   791       by (unfold rest_def s_holding_def, fold wq_def,

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

   793   qed

   794 qed

   795 

   796 lemma wq_es_cs:

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

   798  using wq_s_cs[unfolded wq_def]

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

   800 

   801 lemma distinct_wq': "distinct wq'"

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

   803   

   804 lemma th'_in_inv:

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

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

   807   using assms

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

   809         rest_def some_eq_ex wq'_def wq_distinct wq_s_cs) 

   810 

   811 lemma neq_t_th: 

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

   813   shows "t \<noteq> th"

   814 proof

   815   assume otherwise: "t = th"

   816   show False

   817   proof(cases "c = cs")

   818     case True

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

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

   821      by simp 

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

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

   824     show ?thesis by simp

   825   next

   826     case False

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

   828         by (unfold is_v, simp)

   829     hence "waiting s t c" using assms 

   830         by (simp add: cs_waiting_def waiting_eq)

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

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

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

   834   qed

   835 qed

   836 

   837 lemma waiting_esI1:

   838   assumes "waiting s t c"

   839       and "c \<noteq> cs" 

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

   841 proof -

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

   843     using assms(2) is_v by auto

   844   with assms(1) show ?thesis 

   845     using cs_waiting_def waiting_eq by auto 

   846 qed

   847 

   848 lemma holding_esI2:

   849   assumes "c \<noteq> cs" 

   850   and "holding s t c"

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

   852 proof -

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

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

   855                 folded this, unfolded wq_def, folded s_holding_def]

   856   show ?thesis .

   857 qed

   858 

   859 lemma holding_esI1:

   860   assumes "holding s t c"

   861   and "t \<noteq> th"

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

   863 proof -

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

   865   from holding_esI2[OF this assms(1)]

   866   show ?thesis .

   867 qed

   868 

   869 end

   870 

   871 context valid_trace_v_n

   872 begin

   873 

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

   875 proof (unfold wq'_def, rule someI2)

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

   877     by (simp add: distinct_rest) 

   878 next

   879   fix x

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

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

   882 qed 

   883 

   884 definition "taker = hd wq'"

   885 

   886 definition "rest' = tl wq'"

   887 

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

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

   890 

   891 lemma next_th_taker: 

   892   shows "next_th s th cs taker"

   893   using rest_nnl taker_def wq'_def wq_s_cs 

   894   by (auto simp:next_th_def)

   895 

   896 lemma taker_unique: 

   897   assumes "next_th s th cs taker'"

   898   shows "taker' = taker"

   899 proof -

   900   from assms

   901   obtain rest' where 

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

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

   904           by (unfold next_th_def, auto)

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

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

   907 qed

   908 

   909 lemma waiting_set_eq:

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

   911   by (smt all_not_in_conv bot.extremum insertI1 insert_subset 

   912       mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)

   913 

   914 lemma holding_set_eq:

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

   916   using next_th_taker taker_def waiting_set_eq 

   917   by fastforce

   918    

   919 lemma holding_taker:

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

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

   922         auto simp:neq_wq' taker_def)

   923 

   924 lemma waiting_esI2:

   925   assumes "waiting s t cs"

   926       and "t \<noteq> taker"

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

   928 proof -

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

   930   proof(unfold wq'_def, rule someI2)

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

   932           by (simp add: distinct_rest)

   933   next

   934     fix x

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

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

   937         using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto 

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

   939   qed

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

   941     using assms(2) taker_def by auto 

   942   ultimately show ?thesis

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

   944 qed

   945 

   946 lemma waiting_esE:

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

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

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

   950 proof(cases "c = cs")

   951   case False

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

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

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

   955 next

   956   case True

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

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

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

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

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

   962   ultimately have "waiting s t cs"

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

   964                 list.set_sel(2) rest_def waiting_eq wq_s_cs)  

   965   show ?thesis using that(2)

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

   967 qed

   968 

   969 lemma holding_esI1:

   970   assumes "c = cs"

   971   and "t = taker"

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

   973   by (unfold assms, simp add: holding_taker)

   974 

   975 lemma holding_esE:

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

   977   obtains "c = cs" "t = taker"

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

   979 proof(cases "c = cs")

   980   case True

   981   from assms[unfolded True, unfolded s_holding_def, 

   982              folded wq_def, unfolded wq_es_cs]

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

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

   985 next

   986   case False

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

   988   from assms[unfolded s_holding_def, folded wq_def, 

   989              unfolded this, unfolded wq_def, folded s_holding_def]

   990   have "holding s t c"  .

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

   992 qed

   993 

   994 end 

   995 

   996 

   997 context valid_trace_v_n

   998 begin

   999 

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

  1001 proof (unfold wq'_def, rule someI2)

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

  1003     by (simp add: distinct_rest) 

  1004 next

  1005   fix x

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

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

  1008 qed 

  1009 

  1010 lemma no_taker: 

  1011   assumes "next_th s th cs taker"

  1012   shows "False"

  1013 proof -

  1014   from assms[unfolded next_th_def]

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

  1016     by auto

  1017   thus ?thesis using rest_def rest_nil by auto 

  1018 qed

  1019 

  1020 lemma waiting_set_eq:

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

  1022   using no_taker by auto

  1023 

  1024 lemma holding_set_eq:

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

  1026   using no_taker by auto

  1027    

  1028 lemma no_holding:

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

  1030   shows False

  1031 proof -

  1032   from wq_es_cs[unfolded nil_wq']

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

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

  1035   show ?thesis by auto

  1036 qed

  1037 

  1038 lemma no_waiting:

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

  1040   shows False

  1041 proof -

  1042   from wq_es_cs[unfolded nil_wq']

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

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

  1045   show ?thesis by auto

  1046 qed

  1047 

  1048 lemma waiting_esI2:

  1049   assumes "waiting s t c"

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

  1051 proof -

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

  1053     using cs_waiting_def rest_nil waiting_eq wq_s_cs by auto 

  1054   from waiting_esI1[OF assms this]

  1055   show ?thesis .

  1056 qed

  1057 

  1058 lemma waiting_esE:

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

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

  1061 proof(cases "c = cs")

  1062   case False

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

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

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

  1066 next

  1067   case True

  1068   from no_waiting[OF assms[unfolded True]]

  1069   show ?thesis by auto

  1070 qed

  1071 

  1072 lemma holding_esE:

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

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

  1075 proof(cases "c = cs")

  1076   case True

  1077   from no_holding[OF assms[unfolded True]] 

  1078   show ?thesis by auto

  1079 next

  1080   case False

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

  1082   from assms[unfolded s_holding_def, folded wq_def, 

  1083              unfolded this, unfolded wq_def, folded s_holding_def]

  1084   have "holding s t c"  .

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

  1086 qed

  1087 

  1088 end (* ccc *)

  1089 

  1090 lemma rel_eqI:

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

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

  1093   shows "A = B"

  1094   using assms by auto

  1095 

  1096 lemma in_RAG_E:

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

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

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

  1100   using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]

  1101   by auto

  1102   

  1103 context valid_trace_v

  1104 begin

  1105 

  1106 lemma RAG_es:

  1107   "RAG (e # s) =

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

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

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

  1111 proof(rule rel_eqI)

  1112   fix n1 n2

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

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

  1115   proof(cases rule:in_RAG_E)

  1116     case (waiting th' cs')

  1117     show ?thesis

  1118     proof(cases "rest = []")

  1119       case False

  1120       interpret h_n: valid_trace_v_n s e th cs

  1121         by (unfold_locales, insert False, simp)

  1122       from waiting(3)

  1123       show ?thesis

  1124       proof(cases rule:h_n.waiting_esE)

  1125         case 1

  1126         with waiting(1,2)

  1127         show ?thesis

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

  1129              fold waiting_eq, auto)

  1130       next

  1131         case 2

  1132         with waiting(1,2)

  1133         show ?thesis

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

  1135              fold waiting_eq, auto)