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 

   381 context valid_trace

   382 begin

   383 

   384 

   385 text {* (* ddd *)

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

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

   388   For instance, the fact 

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

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

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

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

   393 

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

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

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

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

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

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

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

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

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

   403 

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

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

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

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

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

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

   410   and kept on blocked on them respectively ever since.

   411  

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

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

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

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

   416 *}

   417 

   418 lemma waiting_unique_pre: (* ddd *)

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

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

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

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

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

   424   shows "False"

   425 proof -

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

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

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

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

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

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

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

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

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

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

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

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

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

   439   { fix s cs

   440     assume q: "?Q cs s"

   441     have "thread \<notin> runing s"

   442     proof

   443       assume "thread \<in> runing s"

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

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

   446         by (unfold runing_def s_waiting_def readys_def, auto)

   447       from this[rule_format, of cs] q 

   448       show False by (simp add: wq_def) 

   449     qed

   450   } note q_not_runing = this

   451   { fix t1 t2 cs1 cs2

   452     assume  lt1: "t1 < length s"

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

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

   455     and lt2: "t2 < length s"

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

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

   458     and lt12: "t1 < t2"

   459     let ?t3 = "Suc t2"

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

   461     from moment_plus [OF this] 

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

   463     have "t2 < ?t3" by simp

   464     from nn2 [rule_format, OF this] and eq_m

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

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

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

   468     proof -

   469       from vt_moment 

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

   471       with eq_m show ?thesis by simp

   472     qed

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

   474         by (unfold_locales, auto, cases, simp)

   475     have ?thesis

   476     proof -

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

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

   479         case True

   480         have "e = V thread cs2"

   481         proof -

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

   483               using True and np2  by auto 

   484           from vt_e.wq_out_inv[OF True this h2]

   485           show ?thesis .

   486         qed

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

   488       next

   489         case False

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

   491         with vt_e.actor_inv[OF vt_e.pip_e]

   492         show ?thesis by auto

   493       qed

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

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

   496       ultimately show ?thesis by simp

   497     qed

   498   } note lt_case = this

   499   show ?thesis

   500   proof -

   501     { assume "t1 < t2"

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

   503       have ?thesis .

   504     } moreover {

   505       assume "t2 < t1"

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

   507       have ?thesis .

   508     } moreover {

   509       assume eq_12: "t1 = t2"

   510       let ?t3 = "Suc t2"

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

   512       from moment_plus [OF this] 

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

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

   515       from nn2 [rule_format, OF this] and eq_m

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

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

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

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

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

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

   522       proof -

   523         from vt_moment 

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

   525         with eq_m show ?thesis by simp

   526       qed

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

   528           by (unfold_locales, auto, cases, simp)

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

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

   531         case True

   532         have "e = V thread cs2"

   533         proof -

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

   535               using True and np2  by auto 

   536           from vt_e.wq_out_inv[OF True this h2]

   537           show ?thesis .

   538         qed

   539         thus ?thesis by auto

   540       next

   541         case False

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

   543         thus ?thesis by auto

   544       qed

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

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

   547         case True

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

   549               using True and np1  by auto 

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

   551         have "e = V thread cs1" .

   552         thus ?thesis by auto

   553       next

   554         case False

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

   556         thus ?thesis by auto

   557       qed

   558       ultimately have ?thesis using neq12 by auto

   559     } ultimately show ?thesis using nat_neq_iff by blast 

   560   qed

   561 qed

   562 

   563 text {*

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

   565 *}

   566 

   567 lemma waiting_unique:

   568   assumes "waiting s th cs1"

   569   and "waiting s th cs2"

   570   shows "cs1 = cs2"

   571   using waiting_unique_pre assms

   572   unfolding wq_def s_waiting_def

   573   by auto

   574 

   575 end

   576 

   577 (* not used *)

   578 text {*

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

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

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

   582 *}

   583 lemma held_unique:

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

   585   and "holding s th2 cs"

   586   shows "th1 = th2"

   587  by (insert assms, unfold s_holding_def, auto)

   588 

   589 

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

   591   apply (induct s, auto)

   592   by (case_tac a, auto split:if_splits)

   593 

   594 lemma last_set_unique: 

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

   596           \<Longrightarrow> th1 = th2"

   597   apply (induct s, auto)

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

   599 

   600 lemma preced_unique : 

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

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

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

   604   shows "th1 = th2"

   605 proof -

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

   607   from last_set_unique [OF this th_in1 th_in2]

   608   show ?thesis .

   609 qed

   610                       

   611 lemma preced_linorder: 

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

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

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

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

   616 proof -

   617   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

   619   thus ?thesis by auto

   620 qed

   621 

   622 (* An aux lemma used later *) 

   623 lemma unique_minus:

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

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

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

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

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

   629 proof -

   630  from xz and neq show ?thesis

   631  proof(induct)

   632    case (base ya)

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

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

   635    with base show ?case by auto

   636  next

   637    case (step ya z)

   638    show ?case

   639    proof(cases "y = ya")

   640      case True

   641      from step True show ?thesis by simp

   642    next

   643      case False

   644      from step False

   645      show ?thesis by auto

   646    qed

   647  qed

   648 qed

   649 

   650 lemma unique_base:

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

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

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

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

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

   656 proof -

   657   from xz neq_yz show ?thesis

   658   proof(induct)

   659     case (base ya)

   660     from xy unique base show ?case by auto

   661   next

   662     case (step ya z)

   663     show ?case

   664     proof(cases "y = ya")

   665       case True

   666       from True step show ?thesis by auto

   667     next

   668       case False

   669       from False step 

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

   671       with step show ?thesis by auto

   672     qed

   673   qed

   674 qed

   675 

   676 lemma unique_chain:

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

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

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

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

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

   682 proof -

   683   from xy xz neq_yz show ?thesis

   684   proof(induct)

   685     case (base y)

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

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

   688   next

   689     case (step y za)

   690     show ?case

   691     proof(cases "y = z")

   692       case True

   693       from True step show ?thesis by auto

   694     next

   695       case False

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

   697       thus ?thesis

   698       proof

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

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

   701         thus ?thesis by auto

   702       next

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

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

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

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

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

   708         thus ?thesis by auto

   709       qed

   710     qed

   711   qed

   712 qed

   713 

   714 text {*

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

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

   717   events, respectively.

   718 *}

   719 

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

   721 apply (unfold s_RAG_def s_waiting_def wq_def)

   722 by (simp add:Let_def)

   723 

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

   725 apply (unfold s_RAG_def s_waiting_def wq_def)

   726 by (simp add:Let_def)

   727 

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

   729 apply (unfold s_RAG_def s_waiting_def wq_def)

   730 by (simp add:Let_def)

   731 

   732 

   733 context valid_trace_v

   734 begin

   735 

   736 

   737 lemma distinct_rest: "distinct rest"

   738   by (simp add: distinct_tl rest_def wq_distinct)

   739 

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

   741 

   742 lemma runing_th_s:

   743   shows "th \<in> runing s"

   744 proof -

   745   from pip_e[unfolded is_v]

   746   show ?thesis by (cases, simp)

   747 qed

   748 

   749 lemma holding_cs_eq_th:

   750   assumes "holding s t cs"

   751   shows "t = th"

   752 proof -

   753   from pip_e[unfolded is_v]

   754   show ?thesis

   755   proof(cases)

   756     case (thread_V)

   757     from held_unique[OF this(2) assms]

   758     show ?thesis by simp

   759   qed

   760 qed

   761 

   762 lemma th_not_waiting: 

   763   "\<not> waiting s th c"

   764 proof -

   765   have "th \<in> readys s"

   766     using runing_ready runing_th_s by blast 

   767   thus ?thesis

   768     by (unfold readys_def, auto)

   769 qed

   770 

   771 lemma waiting_neq_th: 

   772   assumes "waiting s t c"

   773   shows "t \<noteq> th"

   774   using assms using th_not_waiting by blast 

   775 

   776 lemma wq_s_cs:

   777   "wq s cs = th#rest"

   778 proof -

   779   from pip_e[unfolded is_v]

   780   show ?thesis

   781   proof(cases)

   782     case (thread_V)

   783     from this(2) show ?thesis

   784       by (unfold rest_def s_holding_def, fold wq_def,

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

   786   qed

   787 qed

   788 

   789 lemma wq_es_cs:

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

   791  using wq_s_cs[unfolded wq_def]

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

   793 

   794 lemma distinct_wq': "distinct wq'"

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

   796   

   797 lemma th'_in_inv:

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

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

   800   using assms

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

   802         rest_def some_eq_ex wq'_def wq_distinct wq_s_cs) 

   803 

   804 lemma neq_t_th: 

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

   806   shows "t \<noteq> th"

   807 proof

   808   assume otherwise: "t = th"

   809   show False

   810   proof(cases "c = cs")

   811     case True

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

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

   814      by simp 

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

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

   817     show ?thesis by simp

   818   next

   819     case False

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

   821         by (unfold is_v, simp)

   822     hence "waiting s t c" using assms 

   823         by (simp add: cs_waiting_def waiting_eq)

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

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

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

   827   qed

   828 qed

   829 

   830 lemma waiting_esI1:

   831   assumes "waiting s t c"

   832       and "c \<noteq> cs" 

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

   834 proof -

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

   836     using assms(2) is_v by auto

   837   with assms(1) show ?thesis 

   838     using cs_waiting_def waiting_eq by auto 

   839 qed

   840 

   841 lemma holding_esI2:

   842   assumes "c \<noteq> cs" 

   843   and "holding s t c"

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

   845 proof -

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

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

   848                 folded this, unfolded wq_def, folded s_holding_def]

   849   show ?thesis .

   850 qed

   851 

   852 lemma holding_esI1:

   853   assumes "holding s t c"

   854   and "t \<noteq> th"

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

   856 proof -

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

   858   from holding_esI2[OF this assms(1)]

   859   show ?thesis .

   860 qed

   861 

   862 end

   863 

   864 context valid_trace_v_n

   865 begin

   866 

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

   868 proof (unfold wq'_def, rule someI2)

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

   870     by (simp add: distinct_rest) 

   871 next

   872   fix x

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

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

   875 qed 

   876 

   877 definition "taker = hd wq'"

   878 

   879 definition "rest' = tl wq'"

   880 

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

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

   883 

   884 lemma next_th_taker: 

   885   shows "next_th s th cs taker"

   886   using rest_nnl taker_def wq'_def wq_s_cs 

   887   by (auto simp:next_th_def)

   888 

   889 lemma taker_unique: 

   890   assumes "next_th s th cs taker'"

   891   shows "taker' = taker"

   892 proof -

   893   from assms

   894   obtain rest' where 

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

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

   897           by (unfold next_th_def, auto)

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

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

   900 qed

   901 

   902 lemma waiting_set_eq:

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

   904   by (smt all_not_in_conv bot.extremum insertI1 insert_subset 

   905       mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)

   906 

   907 lemma holding_set_eq:

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

   909   using next_th_taker taker_def waiting_set_eq 

   910   by fastforce

   911    

   912 lemma holding_taker:

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

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

   915         auto simp:neq_wq' taker_def)

   916 

   917 lemma waiting_esI2:

   918   assumes "waiting s t cs"

   919       and "t \<noteq> taker"

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

   921 proof -

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

   923   proof(unfold wq'_def, rule someI2)

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

   925           by (simp add: distinct_rest)

   926   next

   927     fix x

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

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

   930         using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto 

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

   932   qed

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

   934     using assms(2) taker_def by auto 

   935   ultimately show ?thesis

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

   937 qed

   938 

   939 lemma waiting_esE:

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

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

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

   943 proof(cases "c = cs")

   944   case False

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

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

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

   948 next

   949   case True

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

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

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

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

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

   955   ultimately have "waiting s t cs"

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

   957                 list.set_sel(2) rest_def waiting_eq wq_s_cs)  

   958   show ?thesis using that(2)

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

   960 qed

   961 

   962 lemma holding_esI1:

   963   assumes "c = cs"

   964   and "t = taker"

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

   966   by (unfold assms, simp add: holding_taker)

   967 

   968 lemma holding_esE:

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

   970   obtains "c = cs" "t = taker"

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

   972 proof(cases "c = cs")

   973   case True

   974   from assms[unfolded True, unfolded s_holding_def, 

   975              folded wq_def, unfolded wq_es_cs]

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

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

   978 next

   979   case False

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

   981   from assms[unfolded s_holding_def, folded wq_def, 

   982              unfolded this, unfolded wq_def, folded s_holding_def]

   983   have "holding s t c"  .

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

   985 qed

   986 

   987 end 

   988 

   989 

   990 context valid_trace_v_n

   991 begin

   992 

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

   994 proof (unfold wq'_def, rule someI2)

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

   996     by (simp add: distinct_rest) 

   997 next

   998   fix x

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

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

  1001 qed 

  1002 

  1003 lemma no_taker: 

  1004   assumes "next_th s th cs taker"

  1005   shows "False"

  1006 proof -

  1007   from assms[unfolded next_th_def]

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

  1009     by auto

  1010   thus ?thesis using rest_def rest_nil by auto 

  1011 qed

  1012 

  1013 lemma waiting_set_eq:

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

  1015   using no_taker by auto

  1016 

  1017 lemma holding_set_eq:

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

  1019   using no_taker by auto

  1020    

  1021 lemma no_holding:

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

  1023   shows False

  1024 proof -

  1025   from wq_es_cs[unfolded nil_wq']

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

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

  1028   show ?thesis by auto

  1029 qed

  1030 

  1031 lemma no_waiting:

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

  1033   shows False

  1034 proof -

  1035   from wq_es_cs[unfolded nil_wq']

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

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

  1038   show ?thesis by auto

  1039 qed

  1040 

  1041 lemma waiting_esI2:

  1042   assumes "waiting s t c"

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

  1044 proof -

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

  1046     using cs_waiting_def rest_nil waiting_eq wq_s_cs by auto 

  1047   from waiting_esI1[OF assms this]

  1048   show ?thesis .

  1049 qed

  1050 

  1051 lemma waiting_esE:

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

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

  1054 proof(cases "c = cs")

  1055   case False

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

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

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

  1059 next

  1060   case True

  1061   from no_waiting[OF assms[unfolded True]]

  1062   show ?thesis by auto

  1063 qed

  1064 

  1065 lemma holding_esE:

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

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

  1068 proof(cases "c = cs")

  1069   case True

  1070   from no_holding[OF assms[unfolded True]] 

  1071   show ?thesis by auto

  1072 next

  1073   case False

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

  1075   from assms[unfolded s_holding_def, folded wq_def, 

  1076              unfolded this, unfolded wq_def, folded s_holding_def]

  1077   have "holding s t c"  .

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

  1079 qed

  1080 

  1081 end (* ccc *)

  1082 

  1083 lemma rel_eqI:

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

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

  1086   shows "A = B"

  1087   using assms by auto

  1088 

  1089 lemma in_RAG_E:

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

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

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

  1093   using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]

  1094   by auto

  1095   

  1096 context valid_trace_v

  1097 begin

  1098 

  1099 lemma RAG_es:

  1100   "RAG (e # s) =

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

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

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

  1104 proof(rule rel_eqI)

  1105   fix n1 n2

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

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

  1108   proof(cases rule:in_RAG_E)

  1109     case (waiting th' cs')

  1110     show ?thesis

  1111     proof(cases "rest = []")

  1112       case False

  1113       interpret h_n: valid_trace_v_n s e th cs

  1114         by (unfold_locales, insert False, simp)

  1115       from waiting(3)

  1116       show ?thesis

  1117       proof(cases rule:h_n.waiting_esE)

  1118         case 1

  1119         with waiting(1,2)

  1120         show ?thesis

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

  1122              fold waiting_eq, auto)

  1123       next

  1124         case 2

  1125         with waiting(1,2)

  1126         show ?thesis

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

  1128              fold waiting_eq, auto)

  1129       qed

  1130     next

  1131       case True

  1132       interpret h_e: valid_trace_v_e s e th cs

  1133         by (unfold_locales, insert True, simp)

  1134       from waiting(3)

  1135       show ?thesis