1 theory CpsG

     2 imports PIPDefs

     3 begin

     4 

     5 section {* Generic aulxiliary lemmas *}

     6 

     7 lemma f_image_eq:

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

     9   shows "f ` A = g ` A"

    10 proof

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

    12     by(rule image_subsetI, auto intro:h)

    13 next

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

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

    16 qed

    17 

    18 lemma Max_fg_mono:

    19   assumes "finite A"

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

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

    22 proof(cases "A = {}")

    23   case True

    24   thus ?thesis by auto

    25 next

    26   case False

    27   show ?thesis

    28   proof(rule Max.boundedI)

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

    30   next

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

    32   next

    33     fix fa

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

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

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

    37     proof(rule Max_ge_iff[THEN iffD2])

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

    39     next

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

    41     next

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

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

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

    45     qed

    46   qed

    47 qed 

    48 

    49 lemma Max_f_mono:

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

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

    52   and fnt: "finite B"

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

    54 proof(rule Max_mono)

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

    56 next

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

    58 next

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

    60 qed

    61 

    62 lemma Max_UNION: 

    63   assumes "finite A"

    64   and "A \<noteq> {}"

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

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

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

    68   using assms[simp]

    69 proof -

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

    71     by (fold Union_image_eq, simp)

    72   also have "... = ?R"

    73     by (subst Max_Union, simp+)

    74   finally show ?thesis .

    75 qed

    76 

    77 lemma max_Max_eq:

    78   assumes "finite A"

    79     and "A \<noteq> {}"

    80     and "x = y"

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

    82 proof -

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

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

    85       by (subst Max.insert, simp+)

    86   finally show ?thesis by simp

    87 qed

    88 

    89 lemma rel_eqI:

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

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

    92   shows "A = B"

    93   using assms by auto

    94 

    95 section {* Lemmas do not depend on trace validity *}

    96 

    97 lemma birth_time_lt:  

    98   assumes "s \<noteq> []"

    99   shows "last_set th s < length s"

   100   using assms

   101 proof(induct s)

   102   case (Cons a s)

   103   show ?case

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

   105     case False

   106     thus ?thesis

   107       by (cases a, auto)

   108   next

   109     case True

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

   111       by (cases a, auto)

   112   qed

   113 qed simp

   114 

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

   116   by (induct s, auto)

   117 

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

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

   120 

   121 lemma eq_RAG: 

   122   "RAG (wq s) = RAG s"

   123   by (unfold cs_RAG_def s_RAG_def, auto)

   124 

   125 lemma waiting_holding:

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

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

   128 proof -

   129   from assms[unfolded s_waiting_def, folded wq_def]

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

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

   132   hence "holding s th' cs" 

   133     by (unfold s_holding_def, fold wq_def, auto)

   134   from that[OF this] show ?thesis .

   135 qed

   136 

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

   138 unfolding cp_def wq_def

   139 apply(induct s rule: schs.induct)

   140 apply(simp add: Let_def cpreced_initial)

   141 apply(simp add: Let_def)

   142 apply(simp add: Let_def)

   143 apply(simp add: Let_def)

   144 apply(subst (2) schs.simps)

   145 apply(simp add: Let_def)

   146 apply(subst (2) schs.simps)

   147 apply(simp add: Let_def)

   148 done

   149 

   150 lemma cp_alt_def:

   151   "cp s th =  

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

   153 proof -

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

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

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

   157   proof -

   158     have "?L = ?R" 

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

   160     thus ?thesis by simp

   161   qed

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

   163 qed

   164 

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

   166   by (unfold s_RAG_def, auto)

   167 

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

   169   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)

   170 

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

   172   by (unfold s_holding_def wq_def cs_holding_def, simp)

   173 

   174 lemma children_RAG_alt_def:

   175   "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"

   176   by (unfold s_RAG_def, auto simp:children_def holding_eq)

   177 

   178 lemma holdents_alt_def:

   179   "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))"

   180   by (unfold children_RAG_alt_def holdents_def, simp add: image_image)

   181 

   182 lemma cntCS_alt_def:

   183   "cntCS s th = card (children (RAG s) (Th th))"

   184   apply (unfold children_RAG_alt_def cntCS_def holdents_def)

   185   by (rule card_image[symmetric], auto simp:inj_on_def)

   186 

   187 lemma runing_ready: 

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

   189   unfolding runing_def readys_def

   190   by auto 

   191 

   192 lemma readys_threads:

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

   194   unfolding readys_def

   195   by auto

   196 

   197 lemma wq_v_neq [simp]:

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

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

   200 

   201 lemma runing_head:

   202   assumes "th \<in> runing s"

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

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

   205   using assms

   206   by (simp add:runing_def readys_def s_waiting_def wq_def)

   207 

   208 lemma runing_wqE:

   209   assumes "th \<in> runing s"

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

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

   212 proof -

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

   214     by (meson list.set_cases)

   215   have "th' = th"

   216   proof(rule ccontr)

   217     assume "th' \<noteq> th"

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

   219     with assms(2)

   220     have "waiting s th cs" 

   221       by (unfold s_waiting_def, fold wq_def, auto)

   222     with assms show False 

   223       by (unfold runing_def readys_def, auto)

   224   qed

   225   with eq_wq that show ?thesis by metis

   226 qed

   227 

   228 lemma isP_E:

   229   assumes "isP e"

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

   231   using assms by (cases e, auto)

   232 

   233 lemma isV_E:

   234   assumes "isV e"

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

   236   using assms by (cases e, auto) 

   237 

   238 

   239 text {*

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

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

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

   243 *}

   244 lemma held_unique:

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

   246   and "holding s th2 cs"

   247   shows "th1 = th2"

   248  by (insert assms, unfold s_holding_def, auto)

   249 

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

   251   apply (induct s, auto)

   252   by (case_tac a, auto split:if_splits)

   253 

   254 lemma last_set_unique: 

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

   256           \<Longrightarrow> th1 = th2"

   257   apply (induct s, auto)

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

   259 

   260 lemma preced_unique : 

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

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

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

   264   shows "th1 = th2"

   265 proof -

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

   267   from last_set_unique [OF this th_in1 th_in2]

   268   show ?thesis .

   269 qed

   270                       

   271 lemma preced_linorder: 

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

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

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

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

   276 proof -

   277   from preced_unique [OF _ th_in1 th_in2] and neq_12 

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

   279   thus ?thesis by auto

   280 qed

   281 

   282 lemma in_RAG_E:

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

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

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

   286   using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]

   287   by auto

   288 

   289 lemma count_rec1 [simp]: 

   290   assumes "Q e"

   291   shows "count Q (e#es) = Suc (count Q es)"

   292   using assms

   293   by (unfold count_def, auto)

   294 

   295 lemma count_rec2 [simp]: 

   296   assumes "\<not>Q e"

   297   shows "count Q (e#es) = (count Q es)"

   298   using assms

   299   by (unfold count_def, auto)

   300 

   301 lemma count_rec3 [simp]: 

   302   shows "count Q [] =  0"

   303   by (unfold count_def, auto)

   304 

   305 lemma cntP_simp1[simp]:

   306   "cntP (P th cs'#s) th = cntP s th + 1"

   307   by (unfold cntP_def, simp)

   308 

   309 lemma cntP_simp2[simp]:

   310   assumes "th' \<noteq> th"

   311   shows "cntP (P th cs'#s) th' = cntP s th'"

   312   using assms

   313   by (unfold cntP_def, simp)

   314 

   315 lemma cntP_simp3[simp]:

   316   assumes "\<not> isP e"

   317   shows "cntP (e#s) th' = cntP s th'"

   318   using assms

   319   by (unfold cntP_def, cases e, simp+)

   320 

   321 lemma cntV_simp1[simp]:

   322   "cntV (V th cs'#s) th = cntV s th + 1"

   323   by (unfold cntV_def, simp)

   324 

   325 lemma cntV_simp2[simp]:

   326   assumes "th' \<noteq> th"

   327   shows "cntV (V th cs'#s) th' = cntV s th'"

   328   using assms

   329   by (unfold cntV_def, simp)

   330 

   331 lemma cntV_simp3[simp]:

   332   assumes "\<not> isV e"

   333   shows "cntV (e#s) th' = cntV s th'"

   334   using assms

   335   by (unfold cntV_def, cases e, simp+)

   336 

   337 lemma cntP_diff_inv:

   338   assumes "cntP (e#s) th \<noteq> cntP s th"

   339   shows "isP e \<and> actor e = th"

   340 proof(cases e)

   341   case (P th' pty)

   342   show ?thesis

   343   by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", 

   344         insert assms P, auto simp:cntP_def)

   345 qed (insert assms, auto simp:cntP_def)

   346   

   347 lemma cntV_diff_inv:

   348   assumes "cntV (e#s) th \<noteq> cntV s th"

   349   shows "isV e \<and> actor e = th"

   350 proof(cases e)

   351   case (V th' pty)

   352   show ?thesis

   353   by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", 

   354         insert assms V, auto simp:cntV_def)

   355 qed (insert assms, auto simp:cntV_def)

   356 

   357 lemma eq_dependants: "dependants (wq s) = dependants s"

   358   by (simp add: s_dependants_abv wq_def)

   359 

   360 lemma inj_the_preced: 

   361   "inj_on (the_preced s) (threads s)"

   362   by (metis inj_onI preced_unique the_preced_def)

   363 

   364 lemma holding_next_thI:

   365   assumes "holding s th cs"

   366   and "length (wq s cs) > 1"

   367   obtains th' where "next_th s th cs th'"

   368 proof -

   369   from assms(1)[folded holding_eq, unfolded cs_holding_def]

   370   have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" 

   371     by (unfold s_holding_def, fold wq_def, auto)

   372   then obtain rest where h1: "wq s cs = th#rest" 

   373     by (cases "wq s cs", auto)

   374   with assms(2) have h2: "rest \<noteq> []" by auto

   375   let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"

   376   have "next_th s th cs ?th'" using  h1(1) h2 

   377     by (unfold next_th_def, auto)

   378   from that[OF this] show ?thesis .

   379 qed

   380 

   381 (* ccc *)

   382 

   383 section {* Locales used to investigate the execution of PIP *}

   384 

   385 text {* 

   386   The following locale @{text valid_trace} is used to constrain the 

   387   trace to be valid. All properties hold for valid traces are 

   388   derived under this locale. 

   389 *}

   390 locale valid_trace = 

   391   fixes s

   392   assumes vt : "vt s"

   393 

   394 text {* 

   395   The following locale @{text valid_trace_e} describes 

   396   the valid extension of a valid trace. The event @{text "e"}

   397   represents an event in the system, which corresponds 

   398   to a one step operation of the PIP protocol. 

   399   It is required that @{text "e"} is an event eligible to happen

   400   under state @{text "s"}, which is already required to be valid

   401   by the parent locale @{text "valid_trace"}.

   402 

   403   This locale is used to investigate one step execution of PIP, 

   404   properties concerning the effects of @{text "e"}'s execution, 

   405   for example, how the values of observation functions are changed, 

   406   or how desirable properties are kept invariant, are derived

   407   under this locale. The state before execution is @{text "s"}, while

   408   the state after execution is @{text "e#s"}. Therefore, the lemmas 

   409   derived usually relate observations on @{text "e#s"} to those 

   410   on @{text "s"}.

   411 *}

   412 

   413 locale valid_trace_e = valid_trace +

   414   fixes e

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

   416 begin

   417 

   418 text {*

   419   The following lemma shows that @{text "e"} must be a 

   420   eligible event (or a valid step) to be taken under

   421   the state represented by @{text "s"}.

   422 *}

   423 lemma pip_e: "PIP s e"

   424   using vt_e by (cases, simp)  

   425 

   426 end

   427 

   428 text {*

   429   Because @{term "e#s"} is also a valid trace, properties 

   430   derived for valid trace @{term s} also hold on @{term "e#s"}.

   431 *}

   432 sublocale valid_trace_e < vat_es!: valid_trace "e#s" 

   433   using vt_e

   434   by (unfold_locales, simp)

   435 

   436 text {*

   437   For each specific event (or operation), there is a sublocale

   438   further constraining that the event @{text e} to be that 

   439   particular event. 

   440 

   441   For example, the following 

   442   locale @{text "valid_trace_create"} is the sublocale for 

   443   event @{term "Create"}:

   444 *}

   445 locale valid_trace_create = valid_trace_e + 

   446   fixes th prio

   447   assumes is_create: "e = Create th prio"

   448 

   449 locale valid_trace_exit = valid_trace_e + 

   450   fixes th

   451   assumes is_exit: "e = Exit th"

   452 

   453 locale valid_trace_p = valid_trace_e + 

   454   fixes th cs

   455   assumes is_p: "e = P th cs"

   456 

   457 text {*

   458   locale @{text "valid_trace_p"} is divided further into two 

   459   sublocales, namely, @{text "valid_trace_p_h"} 

   460   and @{text "valid_trace_p_w"}.

   461 *}

   462 

   463 text {*

   464   The following two sublocales @{text "valid_trace_p_h"}

   465   and @{text "valid_trace_p_w"} represent two complementary 

   466   cases under @{text "valid_trace_p"}, where

   467   @{text "valid_trace_p_h"} further constraints that

   468   @{text "wq s cs = []"}, which means the waiting queue of 

   469   the requested resource @{text "cs"} is empty, in which

   470   case,  the requesting thread @{text "th"} 

   471   will take hold of @{text "cs"}. 

   472 

   473   Opposite to @{text "valid_trace_p_h"},

   474   @{text "valid_trace_p_w"} constraints that

   475   @{text "wq s cs \<noteq> []"}, which means the waiting queue of 

   476   the requested resource @{text "cs"} is nonempty, in which

   477   case,  the requesting thread @{text "th"} will be blocked

   478   on @{text "cs"}: 

   479 

   480   Peculiar properties will be derived under respective 

   481   locales.

   482 *}

   483 

   484 locale valid_trace_p_h = valid_trace_p +

   485   assumes we: "wq s cs = []"

   486 

   487 locale valid_trace_p_w = valid_trace_p +

   488   assumes wne: "wq s cs \<noteq> []"

   489 begin

   490 

   491 text {*

   492   The following @{text "holder"} designates

   493   the holder of @{text "cs"} before the @{text "P"}-operation.

   494 *}

   495 definition "holder = hd (wq s cs)"

   496 

   497 text {*

   498   The following @{text "waiters"} designates

   499   the list of threads waiting for @{text "cs"} 

   500   before the @{text "P"}-operation.

   501 *}

   502 definition "waiters = tl (wq s cs)"

   503 end

   504 

   505 text {* 

   506   @{text "valid_trace_v"} is set for the @{term V}-operation.

   507 *}

   508 locale valid_trace_v = valid_trace_e + 

   509   fixes th cs

   510   assumes is_v: "e = V th cs"

   511 begin

   512   -- {* The following @{text "rest"} is the tail of 

   513         waiting queue of the resource @{text "cs"}

   514         to be released by this @{text "V"}-operation.

   515      *}

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

   517 

   518   text {*

   519     The following @{text "wq'"} is the waiting

   520     queue of @{term "cs"}

   521     after the @{text "V"}-operation, which

   522     is simply a reordering of @{term "rest"}. 

   523 

   524     The effect of this reordering needs to be 

   525     understood by two cases:

   526     \begin{enumerate}

   527     \item When @{text "rest = []"},

   528     the reordering gives rise to an empty list as well, 

   529     which means there is no thread holding or waiting 

   530     for resource @{term "cs"}, therefore, it is free.

   531 

   532     \item When @{text "rest \<noteq> []"}, the effect of 

   533     this reordering is to arbitrarily 

   534     switch one thread in @{term "rest"} to the 

   535     head, which, by definition take over the hold

   536     of @{term "cs"} and is designated by @{text "taker"}

   537     in the following sublocale @{text "valid_trace_v_n"}.

   538   *}

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

   540 

   541   text {* 

   542   The following @{text "rest'"} is the tail of the 

   543   waiting queue after the @{text "V"}-operation. 

   544   It plays only auxiliary role to ease reasoning. 

   545   *}

   546   definition "rest' = tl wq'"

   547 

   548 end

   549 

   550 text {* 

   551   In the following, @{text "valid_trace_v"} is also 

   552   divided into two 

   553   sublocales: when @{text "rest"} is empty (represented

   554   by @{text "valid_trace_v_e"}), which means, there is no thread waiting 

   555   for @{text "cs"}, therefore, after the @{text "V"}-operation, 

   556   it will become free; otherwise (represented 

   557   by @{text "valid_trace_v_n"}), one thread 

   558   will be picked from those in @{text "rest"} to take 

   559   over @{text "cs"}.

   560 *}

   561 

   562 locale valid_trace_v_e = valid_trace_v +

   563   assumes rest_nil: "rest = []"

   564 

   565 locale valid_trace_v_n = valid_trace_v +

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

   567 begin

   568 

   569 text {* 

   570   The following @{text "taker"} is the thread to 

   571   take over @{text "cs"}. 

   572 *}

   573   definition "taker = hd wq'"

   574 

   575 end

   576 

   577 

   578 locale valid_trace_set = valid_trace_e + 

   579   fixes th prio

   580   assumes is_set: "e = Set th prio"

   581 

   582 context valid_trace

   583 begin

   584 

   585 text {*

   586   Induction rule introduced to easy the 

   587   derivation of properties for valid trace @{term "s"}.

   588   One more premises, namely @{term "valid_trace_e s e"}

   589   is added, so that an interpretation of 

   590   @{text "valid_trace_e"} can be instantiated 

   591   so that all properties derived so far becomes 

   592   available in the proof of induction step.

   593 

   594   You will see its use in the proofs that follows.

   595 *}

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

   597   assumes "PP []"

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

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

   600      shows "PP s"

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

   602   case Init

   603   from assms(1) show ?case .

   604 next

   605   case (Step s e)

   606   show ?case

   607   proof(rule assms(2))

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

   609   next

   610     show "PP s" using Step by simp

   611   next

   612     show "PIP s e" using Step by simp

   613   qed

   614 qed

   615 

   616 text {*

   617   The following lemma says that if @{text "s"} is a valid state, so 

   618   is its any postfix. Where @{term "monent t s"} is the postfix of 

   619   @{term "s"} with length @{term "t"}.

   620 *}

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

   622 proof(induct rule:ind)

   623   case Nil

   624   thus ?case by (simp add:vt_nil)

   625 next

   626   case (Cons s e t)

   627   show ?case

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

   629     case True

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

   631     thus ?thesis using Cons

   632       by (simp add:valid_trace_def valid_trace_e_def, auto)

   633   next

   634     case False

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

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

   637     proof -

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

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

   640       show ?thesis by simp

   641     qed

   642     ultimately show ?thesis by simp

   643   qed

   644 qed

   645 end

   646 

   647 text {*

   648   The following locale @{text "valid_moment"} is to inherit the properties 

   649   derived on any valid state to the prefix of it, with length @{text "i"}.

   650 *}

   651 locale valid_moment = valid_trace + 

   652   fixes i :: nat

   653 

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

   655   by (unfold_locales, insert vt_moment, auto)

   656 

   657 locale valid_moment_e = valid_moment +

   658   assumes less_i: "i < length s"

   659 begin

   660   definition "next_e  = hd (moment (Suc i) s)"

   661 

   662   lemma trace_e: 

   663     "moment (Suc i) s = next_e#moment i s"

   664    proof -

   665     from less_i have "Suc i \<le> length s" by auto

   666     from moment_plus[OF this, folded next_e_def]

   667     show ?thesis .

   668    qed

   669 

   670 end

   671 

   672 sublocale valid_moment_e < vat_moment_e!: valid_trace_e "moment i s" "next_e"

   673   using vt_moment[of "Suc i", unfolded trace_e]

   674   by (unfold_locales, simp)

   675 

   676 section {* Distinctiveness of waiting queues *}

   677 

   678 context valid_trace_create

   679 begin

   680 

   681 lemma wq_kept [simp]:

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

   683     using assms unfolding is_create wq_def

   684   by (auto simp:Let_def)

   685 

   686 lemma wq_distinct_kept:

   687   assumes "distinct (wq s cs')"

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

   689   using assms by simp

   690 end

   691 

   692 context valid_trace_exit

   693 begin

   694 

   695 lemma wq_kept [simp]:

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

   697     using assms unfolding is_exit wq_def

   698   by (auto simp:Let_def)

   699 

   700 lemma wq_distinct_kept:

   701   assumes "distinct (wq s cs')"

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

   703   using assms by simp

   704 end

   705 

   706 context valid_trace_p 

   707 begin

   708 

   709 lemma wq_neq_simp [simp]:

   710   assumes "cs' \<noteq> cs"

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

   712     using assms unfolding is_p wq_def

   713   by (auto simp:Let_def)

   714 

   715 lemma runing_th_s:

   716   shows "th \<in> runing s"

   717 proof -

   718   from pip_e[unfolded is_p]

   719   show ?thesis by (cases, simp)

   720 qed

   721 

   722 lemma th_not_in_wq: 

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

   724 proof

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

   726   from runing_wqE[OF runing_th_s this]

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

   728   with otherwise

   729   have "holding s th cs"

   730     by (unfold s_holding_def, fold wq_def, simp)

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

   732     by (unfold s_RAG_def, fold holding_eq, auto)

   733   from pip_e[unfolded is_p]

   734   show False

   735   proof(cases)

   736     case (thread_P)

   737     with cs_th_RAG show ?thesis by auto

   738   qed

   739 qed

   740 

   741 lemma wq_es_cs: 

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

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

   744 

   745 lemma wq_distinct_kept:

   746   assumes "distinct (wq s cs')"

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

   748 proof(cases "cs' = cs")

   749   case True

   750   show ?thesis using True assms th_not_in_wq

   751     by (unfold True wq_es_cs, auto)

   752 qed (insert assms, simp)

   753 

   754 end

   755 

   756 context valid_trace_v

   757 begin

   758 

   759 lemma wq_neq_simp [simp]:

   760   assumes "cs' \<noteq> cs"

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

   762     using assms unfolding is_v wq_def

   763   by (auto simp:Let_def)

   764 

   765 lemma wq_s_cs:

   766   "wq s cs = th#rest"

   767 proof -

   768   from pip_e[unfolded is_v]

   769   show ?thesis

   770   proof(cases)

   771     case (thread_V)

   772     from this(2) show ?thesis

   773       by (unfold rest_def s_holding_def, fold wq_def,

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

   775   qed

   776 qed

   777 

   778 lemma wq_es_cs:

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

   780  using wq_s_cs[unfolded wq_def]

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

   782 

   783 lemma wq_distinct_kept:

   784   assumes "distinct (wq s cs')"

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

   786 proof(cases "cs' = cs")

   787   case True

   788   show ?thesis

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

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

   791         using assms[unfolded True wq_s_cs] by auto

   792   qed simp

   793 qed (insert assms, simp)

   794 

   795 end

   796 

   797 context valid_trace_set

   798 begin

   799 

   800 lemma wq_kept [simp]:

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

   802     using assms unfolding is_set wq_def

   803   by (auto simp:Let_def)

   804 

   805 lemma wq_distinct_kept:

   806   assumes "distinct (wq s cs')"

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

   808   using assms by simp

   809 end

   810 

   811 context valid_trace

   812 begin

   813 

   814 lemma  finite_threads:

   815   shows "finite (threads s)"

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

   817 

   818 lemma finite_readys [simp]: "finite (readys s)"

   819   using finite_threads readys_threads rev_finite_subset by blast

   820 

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

   822 proof(induct rule:ind)

   823   case (Cons s e)

   824   interpret vt_e: valid_trace_e s e using Cons by simp

   825   show ?case 

   826   proof(cases e)

   827     case (Create th prio)

   828     interpret vt_create: valid_trace_create s e th prio 

   829       using Create by (unfold_locales, simp)

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

   831   next

   832     case (Exit th)

   833     interpret vt_exit: valid_trace_exit s e th  

   834         using Exit by (unfold_locales, simp)

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

   836   next

   837     case (P th cs)

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

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

   840   next

   841     case (V th cs)

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

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

   844   next

   845     case (Set th prio)

   846     interpret vt_set: valid_trace_set s e th prio

   847         using Set by (unfold_locales, simp)

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

   849   qed

   850 qed (unfold wq_def Let_def, simp)

   851 

   852 end

   853 

   854 section {* Waiting queues and threads *}

   855 

   856 context valid_trace_e

   857 begin

   858 

   859 lemma wq_out_inv: 

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

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

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

   863   shows "e = V thread cs"

   864 proof(cases e)

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

   866   case (V th cs1)

   867   show ?thesis

   868   proof(cases "cs1 = cs")

   869     case True

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

   871     thus ?thesis

   872     proof(cases)

   873       case (thread_V)

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

   875           by (unfold s_holding_def wq_def, simp)

   876       ultimately show ?thesis using V True by simp

   877     qed

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

   879 next

   880   case (P th cs1)

   881   show ?thesis

   882   proof(cases "cs1 = cs")

   883     case True

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

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

   886     with s_i s_hd s_in have False

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

   888     thus ?thesis by simp

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

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

   891 

   892 lemma wq_in_inv: 

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

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

   895   shows "e = P thread cs"

   896 proof(cases e)

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

   898   case (V th cs1)

   899   have False

   900   proof(cases "cs1 = cs")

   901     case True

   902     show ?thesis

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

   904       case (Cons w_hd w_tl)

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

   906       proof -

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

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

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

   910         proof(rule someI2)

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

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

   913         qed (insert Cons True, auto)

   914         ultimately show ?thesis by simp

   915       qed

   916       with assms show ?thesis by auto

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

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

   919   thus ?thesis by auto

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

   921 

   922 end

   923 

   924 lemma (in valid_trace_create)

   925   th_not_in_threads: "th \<notin> threads s"

   926 proof -

   927   from pip_e[unfolded is_create]

   928   show ?thesis by (cases, simp)

   929 qed

   930 

   931 lemma (in valid_trace_create)

   932   threads_es [simp]: "threads (e#s) = threads s \<union> {th}"

   933   by (unfold is_create, simp)

   934 

   935 lemma (in valid_trace_exit)

   936   threads_es [simp]: "threads (e#s) = threads s - {th}"

   937   by (unfold is_exit, simp)

   938 

   939 lemma (in valid_trace_p)

   940   threads_es [simp]: "threads (e#s) = threads s"

   941   by (unfold is_p, simp)

   942 

   943 lemma (in valid_trace_v)

   944   threads_es [simp]: "threads (e#s) = threads s"

   945   by (unfold is_v, simp)

   946 

   947 lemma (in valid_trace_v)

   948   th_not_in_rest[simp]: "th \<notin> set rest"

   949 proof

   950   assume otherwise: "th \<in> set rest"

   951   have "distinct (wq s cs)" by (simp add: wq_distinct)

   952   from this[unfolded wq_s_cs] and otherwise

   953   show False by auto

   954 qed

   955 

   956 lemma (in valid_trace_v) distinct_rest: "distinct rest"

   957   by (simp add: distinct_tl rest_def wq_distinct)

   958 

   959 lemma (in valid_trace_v)

   960   set_wq_es_cs [simp]: "set (wq (e#s) cs) = set (wq s cs) - {th}"

   961 proof(unfold wq_es_cs wq'_def, rule someI2)

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

   963     by (simp add: distinct_rest) 

   964 next

   965   fix x

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

   967   thus "set x = set (wq s cs) - {th}" 

   968       by (unfold wq_s_cs, simp)

   969 qed

   970 

   971 lemma (in valid_trace_exit)

   972   th_not_in_wq: "th \<notin> set (wq s cs)"

   973 proof -

   974   from pip_e[unfolded is_exit]

   975   show ?thesis

   976   by (cases, unfold holdents_def s_holding_def, fold wq_def, 

   977              auto elim!:runing_wqE)

   978 qed

   979 

   980 lemma (in valid_trace) wq_threads: 

   981   assumes "th \<in> set (wq s cs)"

   982   shows "th \<in> threads s"

   983   using assms

   984 proof(induct rule:ind)

   985   case (Nil)

   986   thus ?case by (auto simp:wq_def)

   987 next

   988   case (Cons s e)

   989   interpret vt_e: valid_trace_e s e using Cons by simp

   990   show ?case

   991   proof(cases e)

   992     case (Create th' prio')

   993     interpret vt: valid_trace_create s e th' prio'

   994       using Create by (unfold_locales, simp)

   995     show ?thesis

   996       using Cons.hyps(2) Cons.prems by auto

   997   next

   998     case (Exit th')

   999     interpret vt: valid_trace_exit s e th'

  1000       using Exit by (unfold_locales, simp)

  1001     show ?thesis

  1002       using Cons.hyps(2) Cons.prems vt.th_not_in_wq by auto 

  1003   next

  1004     case (P th' cs')

  1005     interpret vt: valid_trace_p s e th' cs'

  1006       using P by (unfold_locales, simp)

  1007     show ?thesis

  1008       using Cons.hyps(2) Cons.prems readys_threads 

  1009         runing_ready vt.is_p vt.runing_th_s vt_e.wq_in_inv 

  1010         by fastforce 

  1011   next

  1012     case (V th' cs')

  1013     interpret vt: valid_trace_v s e th' cs'

  1014       using V by (unfold_locales, simp)

  1015     show ?thesis using Cons

  1016       using vt.is_v vt.threads_es vt_e.wq_in_inv by blast

  1017   next

  1018     case (Set th' prio)

  1019     interpret vt: valid_trace_set s e th' prio

  1020       using Set by (unfold_locales, simp)

  1021     show ?thesis using Cons.hyps(2) Cons.prems vt.is_set 

  1022         by (auto simp:wq_def Let_def)

  1023   qed

  1024 qed 

  1025 

  1026 section {* RAG and threads *}

  1027 

  1028 context valid_trace

  1029 begin

  1030 

  1031 lemma  dm_RAG_threads:

  1032   assumes in_dom: "(Th th) \<in> Domain (RAG s)"

  1033   shows "th \<in> threads s"

  1034 proof -

  1035   from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto

  1036   moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto

  1037   ultimately have "(Th th, Cs cs) \<in> RAG s" by simp

  1038   hence "th \<in> set (wq s cs)"

  1039     by (unfold s_RAG_def, auto simp:cs_waiting_def)

  1040   from wq_threads [OF this] show ?thesis .

  1041 qed

  1042 

  1043 lemma rg_RAG_threads: 

  1044   assumes "(Th th) \<in> Range (RAG s)"

  1045   shows "th \<in> threads s"

  1046   using assms

  1047   by (unfold s_RAG_def cs_waiting_def cs_holding_def, 

  1048        auto intro:wq_threads)

  1049 

  1050 lemma RAG_threads:

  1051   assumes "(Th th) \<in> Field (RAG s)"

  1052   shows "th \<in> threads s"

  1053   using assms

  1054   by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)

  1055 

  1056 end

  1057 

  1058 section {* The change of @{term RAG} *}

  1059 

  1060 text {*

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

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

  1063   events, respectively.

  1064 *}

  1065 

  1066 lemma (in valid_trace_set) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"

  1067    by (unfold is_set s_RAG_def s_waiting_def wq_def, simp add:Let_def)

  1068 

  1069 lemma (in valid_trace_create) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"

  1070  by (unfold is_create s_RAG_def s_waiting_def wq_def, simp add:Let_def)

  1071 

  1072 lemma (in valid_trace_exit) RAG_unchanged[simp]: "(RAG (e # s)) = RAG s"

  1073   by (unfold is_exit s_RAG_def s_waiting_def wq_def, simp add:Let_def)

  1074 

  1075 context valid_trace_v

  1076 begin

  1077 

  1078 lemma holding_cs_eq_th:

  1079   assumes "holding s t cs"

  1080   shows "t = th"

  1081 proof -

  1082   from pip_e[unfolded is_v]

  1083   show ?thesis

  1084   proof(cases)

  1085     case (thread_V)

  1086     from held_unique[OF this(2) assms]

  1087     show ?thesis by simp

  1088   qed

  1089 qed

  1090 

  1091 lemma distinct_wq': "distinct wq'"

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

  1093   

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

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

  1096     

  1097 lemma th'_in_inv:

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

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

  1100   using assms set_wq' by simp

  1101 

  1102 lemma runing_th_s:

  1103   shows "th \<in> runing s"

  1104 proof -

  1105   from pip_e[unfolded is_v]

  1106   show ?thesis by (cases, simp)

  1107 qed

  1108 

  1109 lemma neq_t_th: 

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

  1111   shows "t \<noteq> th"

  1112 proof

  1113   assume otherwise: "t = th"

  1114   show False

  1115   proof(cases "c = cs")

  1116     case True

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

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

  1119      by simp 

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

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

  1122     show ?thesis by simp

  1123   next

  1124     case False

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

  1126         by (unfold is_v, simp)

  1127     hence "waiting s t c" using assms 

  1128         by (simp add: cs_waiting_def waiting_eq)

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

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

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

  1132   qed

  1133 qed

  1134 

  1135 lemma waiting_esI1: