1 section {*

     2   This file contains lemmas used to guide the recalculation of current precedence 

     3   after every system call (or system operation)

     4 *}

     5 theory Implementation

     6 imports PIPBasics Max RTree

     7 begin

     8 

     9 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only

    10        difference is the order of arguemts. *}

    11 definition "the_preced s th = preced th s"

    12 

    13 lemma inj_the_preced: 

    14   "inj_on (the_preced s) (threads s)"

    15   by (metis inj_onI preced_unique the_preced_def)

    16 

    17 text {* @{term "the_thread"} extracts thread out of RAG node. *}

    18 fun the_thread :: "node \<Rightarrow> thread" where

    19    "the_thread (Th th) = th"

    20 

    21 text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}

    22 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"

    23 

    24 text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}

    25 definition "hRAG (s::state) =  {(Cs cs, Th th) | th cs. holding s th cs}"

    26 

    27 text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}

    28 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"

    29   by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 

    30              s_holding_abv cs_RAG_def, auto)

    31 

    32 text {* 

    33   The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.

    34   It characterizes the dependency between threads when calculating current

    35   precedences. It is defined as the composition of the above two sub-graphs, 

    36   names @{term "wRAG"} and @{term "hRAG"}.

    37  *}

    38 definition "tRAG s = wRAG s O hRAG s"

    39 

    40 (* ccc *)

    41 

    42 definition "cp_gen s x =

    43                   Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"

    44 

    45 lemma tRAG_alt_def: 

    46   "tRAG s = {(Th th1, Th th2) | th1 th2. 

    47                   \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"

    48  by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)

    49 

    50 lemma tRAG_Field:

    51   "Field (tRAG s) \<subseteq> Field (RAG s)"

    52   by (unfold tRAG_alt_def Field_def, auto)

    53 

    54 lemma tRAG_ancestorsE:

    55   assumes "x \<in> ancestors (tRAG s) u"

    56   obtains th where "x = Th th"

    57 proof -

    58   from assms have "(u, x) \<in> (tRAG s)^+" 

    59       by (unfold ancestors_def, auto)

    60   from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto

    61   then obtain th where "x = Th th"

    62     by (unfold tRAG_alt_def, auto)

    63   from that[OF this] show ?thesis .

    64 qed

    65 

    66 lemma tRAG_mono:

    67   assumes "RAG s' \<subseteq> RAG s"

    68   shows "tRAG s' \<subseteq> tRAG s"

    69   using assms 

    70   by (unfold tRAG_alt_def, auto)

    71 

    72 lemma holding_next_thI:

    73   assumes "holding s th cs"

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

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

    76 proof -

    77   from assms(1)[folded eq_holding, unfolded cs_holding_def]

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

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

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

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

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

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

    84     by (unfold next_th_def, auto)

    85   from that[OF this] show ?thesis .

    86 qed

    87 

    88 lemma RAG_tRAG_transfer:

    89   assumes "vt s'"

    90   assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}"

    91   and "(Cs cs, Th th'') \<in> RAG s'"

    92   shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R")

    93 proof -

    94   interpret vt_s': valid_trace "s'" using assms(1)

    95     by (unfold_locales, simp)

    96   interpret rtree: rtree "RAG s'"

    97   proof

    98   show "single_valued (RAG s')"

    99   apply (intro_locales)

   100     by (unfold single_valued_def, 

   101         auto intro:vt_s'.unique_RAG)

   102 

   103   show "acyclic (RAG s')"

   104      by (rule vt_s'.acyclic_RAG)

   105   qed

   106   { fix n1 n2

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

   108     from this[unfolded tRAG_alt_def]

   109     obtain th1 th2 cs' where 

   110       h: "n1 = Th th1" "n2 = Th th2" 

   111          "(Th th1, Cs cs') \<in> RAG s"

   112          "(Cs cs', Th th2) \<in> RAG s" by auto

   113     from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto

   114     from h(3) and assms(2) 

   115     have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> 

   116           (Th th1, Cs cs') \<in> RAG s'" by auto

   117     hence "(n1, n2) \<in> ?R"

   118     proof

   119       assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)"

   120       hence eq_th1: "th1 = th" by simp

   121       moreover have "th2 = th''"

   122       proof -

   123         from h1 have "cs' = cs" by simp

   124         from assms(3) cs_in[unfolded this] rtree.sgv

   125         show ?thesis

   126           by (unfold single_valued_def, auto)

   127       qed

   128       ultimately show ?thesis using h(1,2) by auto

   129     next

   130       assume "(Th th1, Cs cs') \<in> RAG s'"

   131       with cs_in have "(Th th1, Th th2) \<in> tRAG s'"

   132         by (unfold tRAG_alt_def, auto)

   133       from this[folded h(1, 2)] show ?thesis by auto

   134     qed

   135   } moreover {

   136     fix n1 n2

   137     assume "(n1, n2) \<in> ?R"

   138     hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto

   139     hence "(n1, n2) \<in> ?L" 

   140     proof

   141       assume "(n1, n2) \<in> tRAG s'"

   142       moreover have "... \<subseteq> ?L"

   143       proof(rule tRAG_mono)

   144         show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto)

   145       qed

   146       ultimately show ?thesis by auto

   147     next

   148       assume eq_n: "(n1, n2) = (Th th, Th th'')"

   149       from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto

   150       moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto

   151       ultimately show ?thesis 

   152         by (unfold eq_n tRAG_alt_def, auto)

   153     qed

   154   } ultimately show ?thesis by auto

   155 qed

   156 

   157 context valid_trace

   158 begin

   159 

   160 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]

   161 

   162 end

   163 

   164 lemma cp_alt_def:

   165   "cp s th =  

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

   167 proof -

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

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

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

   171   proof -

   172     have "?L = ?R" 

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

   174     thus ?thesis by simp

   175   qed

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

   177 qed

   178 

   179 lemma cp_gen_alt_def:

   180   "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"

   181     by (auto simp:cp_gen_def)

   182 

   183 lemma tRAG_nodeE:

   184   assumes "(n1, n2) \<in> tRAG s"

   185   obtains th1 th2 where "n1 = Th th1" "n2 = Th th2"

   186   using assms

   187   by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def)

   188 

   189 lemma subtree_nodeE:

   190   assumes "n \<in> subtree (tRAG s) (Th th)"

   191   obtains th1 where "n = Th th1"

   192 proof -

   193   show ?thesis

   194   proof(rule subtreeE[OF assms])

   195     assume "n = Th th"

   196     from that[OF this] show ?thesis .

   197   next

   198     assume "Th th \<in> ancestors (tRAG s) n"

   199     hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)

   200     hence "\<exists> th1. n = Th th1"

   201     proof(induct)

   202       case (base y)

   203       from tRAG_nodeE[OF this] show ?case by metis

   204     next

   205       case (step y z)

   206       thus ?case by auto

   207     qed

   208     with that show ?thesis by auto

   209   qed

   210 qed

   211 

   212 lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"

   213 proof -

   214   have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*" 

   215     by (rule rtrancl_mono, auto simp:RAG_split)

   216   also have "... \<subseteq> ((RAG s)^*)^*"

   217     by (rule rtrancl_mono, auto)

   218   also have "... = (RAG s)^*" by simp

   219   finally show ?thesis by (unfold tRAG_def, simp)

   220 qed

   221 

   222 lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"

   223 proof -

   224   { fix a

   225     assume "a \<in> subtree (tRAG s) x"

   226     hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)

   227     with tRAG_star_RAG[of s]

   228     have "(a, x) \<in> (RAG s)^*" by auto

   229     hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def)

   230   } thus ?thesis by auto

   231 qed

   232 

   233 lemma tRAG_trancl_eq:

   234    "{th'. (Th th', Th th)  \<in> (tRAG s)^+} = 

   235     {th'. (Th th', Th th)  \<in> (RAG s)^+}"

   236    (is "?L = ?R")

   237 proof -

   238   { fix th'

   239     assume "th' \<in> ?L"

   240     hence "(Th th', Th th) \<in> (tRAG s)^+" by auto

   241     from tranclD[OF this]

   242     obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto

   243     from tRAG_subtree_RAG[of s] and this(2)

   244     have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG) 

   245     moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto 

   246     ultimately have "th' \<in> ?R"  by auto 

   247   } moreover 

   248   { fix th'

   249     assume "th' \<in> ?R"

   250     hence "(Th th', Th th) \<in> (RAG s)^+" by (auto)

   251     from plus_rpath[OF this]

   252     obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto

   253     hence "(Th th', Th th) \<in> (tRAG s)^+"

   254     proof(induct xs arbitrary:th' th rule:length_induct)

   255       case (1 xs th' th)

   256       then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto)

   257       show ?case

   258       proof(cases "xs1")

   259         case Nil

   260         from 1(2)[unfolded Cons1 Nil]

   261         have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .

   262         hence "(Th th', x1) \<in> (RAG s)" by (cases, simp)

   263         then obtain cs where "x1 = Cs cs" 

   264               by (unfold s_RAG_def, auto)

   265         from rpath_nnl_lastE[OF rp[unfolded this]]

   266         show ?thesis by auto

   267       next

   268         case (Cons x2 xs2)

   269         from 1(2)[unfolded Cons1[unfolded this]]

   270         have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" .

   271         from rpath_edges_on[OF this]

   272         have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" .

   273         have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)"

   274             by (simp add: edges_on_unfold)

   275         with eds have rg1: "(Th th', x1) \<in> RAG s" by auto

   276         then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto)

   277         have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)"

   278             by (simp add: edges_on_unfold)

   279         from this eds

   280         have rg2: "(x1, x2) \<in> RAG s" by auto

   281         from this[unfolded eq_x1] 

   282         obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto)

   283         from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]

   284         have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto)

   285         from rp have "rpath (RAG s) x2 xs2 (Th th)"

   286            by  (elim rpath_ConsE, simp)

   287         from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" .

   288         show ?thesis

   289         proof(cases "xs2 = []")

   290           case True

   291           from rpath_nilE[OF rp'[unfolded this]]

   292           have "th1 = th" by auto

   293           from rt1[unfolded this] show ?thesis by auto

   294         next

   295           case False

   296           from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons]

   297           have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp

   298           with rt1 show ?thesis by auto

   299         qed

   300       qed

   301     qed

   302     hence "th' \<in> ?L" by auto

   303   } ultimately show ?thesis by blast

   304 qed

   305 

   306 lemma tRAG_trancl_eq_Th:

   307    "{Th th' | th'. (Th th', Th th)  \<in> (tRAG s)^+} = 

   308     {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}"

   309     using tRAG_trancl_eq by auto

   310 

   311 lemma dependants_alt_def:

   312   "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"

   313   by (metis eq_RAG s_dependants_def tRAG_trancl_eq)

   314   

   315 context valid_trace

   316 begin

   317 

   318 lemma count_eq_tRAG_plus:

   319   assumes "cntP s th = cntV s th"

   320   shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"

   321   using assms count_eq_dependants dependants_alt_def eq_dependants by auto 

   322 

   323 lemma count_eq_RAG_plus:

   324   assumes "cntP s th = cntV s th"

   325   shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}"

   326   using assms count_eq_dependants cs_dependants_def eq_RAG by auto

   327 

   328 lemma count_eq_RAG_plus_Th:

   329   assumes "cntP s th = cntV s th"

   330   shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"

   331   using count_eq_RAG_plus[OF assms] by auto

   332 

   333 lemma count_eq_tRAG_plus_Th:

   334   assumes "cntP s th = cntV s th"

   335   shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"

   336    using count_eq_tRAG_plus[OF assms] by auto

   337 

   338 end

   339 

   340 lemma tRAG_subtree_eq: 

   341    "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th'  \<in> (subtree (RAG s) (Th th))}"

   342    (is "?L = ?R")

   343 proof -

   344   { fix n 

   345     assume h: "n \<in> ?L"

   346     hence "n \<in> ?R"

   347     by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) 

   348   } moreover {

   349     fix n

   350     assume "n \<in> ?R"

   351     then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*"

   352       by (auto simp:subtree_def)

   353     from rtranclD[OF this(2)]

   354     have "n \<in> ?L"

   355     proof

   356       assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+"

   357       with h have "n \<in> {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}" by auto

   358       thus ?thesis using subtree_def tRAG_trancl_eq by fastforce

   359     qed (insert h, auto simp:subtree_def)

   360   } ultimately show ?thesis by auto

   361 qed

   362 

   363 lemma threads_set_eq: 

   364    "the_thread ` (subtree (tRAG s) (Th th)) = 

   365                   {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")

   366    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)

   367 

   368 lemma cp_alt_def1: 

   369   "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"

   370 proof -

   371   have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =

   372        ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"

   373        by auto

   374   thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)

   375 qed

   376 

   377 lemma cp_gen_def_cond: 

   378   assumes "x = Th th"

   379   shows "cp s th = cp_gen s (Th th)"

   380 by (unfold cp_alt_def1 cp_gen_def, simp)

   381 

   382 lemma cp_gen_over_set:

   383   assumes "\<forall> x \<in> A. \<exists> th. x = Th th"

   384   shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"

   385 proof(rule f_image_eq)

   386   fix a

   387   assume "a \<in> A"

   388   from assms[rule_format, OF this]

   389   obtain th where eq_a: "a = Th th" by auto

   390   show "cp_gen s a = (cp s \<circ> the_thread) a"

   391     by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)

   392 qed

   393 

   394 

   395 context valid_trace

   396 begin

   397 

   398 lemma RAG_threads:

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

   400   shows "th \<in> threads s"

   401   using assms

   402   by (metis Field_def UnE dm_RAG_threads range_in vt)

   403 

   404 lemma subtree_tRAG_thread:

   405   assumes "th \<in> threads s"

   406   shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")

   407 proof -

   408   have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"

   409     by (unfold tRAG_subtree_eq, simp)

   410   also have "... \<subseteq> ?R"

   411   proof

   412     fix x

   413     assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"

   414     then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto

   415     from this(2)

   416     show "x \<in> ?R"

   417     proof(cases rule:subtreeE)

   418       case 1

   419       thus ?thesis by (simp add: assms h(1)) 

   420     next

   421       case 2

   422       thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 

   423     qed

   424   qed

   425   finally show ?thesis .

   426 qed

   427 

   428 lemma readys_root:

   429   assumes "th \<in> readys s"

   430   shows "root (RAG s) (Th th)"

   431 proof -

   432   { fix x

   433     assume "x \<in> ancestors (RAG s) (Th th)"

   434     hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)

   435     from tranclD[OF this]

   436     obtain z where "(Th th, z) \<in> RAG s" by auto

   437     with assms(1) have False

   438          apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)

   439          by (fold wq_def, blast)

   440   } thus ?thesis by (unfold root_def, auto)

   441 qed

   442 

   443 lemma readys_in_no_subtree:

   444   assumes "th \<in> readys s"

   445   and "th' \<noteq> th"

   446   shows "Th th \<notin> subtree (RAG s) (Th th')" 

   447 proof

   448    assume "Th th \<in> subtree (RAG s) (Th th')"

   449    thus False

   450    proof(cases rule:subtreeE)

   451       case 1

   452       with assms show ?thesis by auto

   453    next

   454       case 2

   455       with readys_root[OF assms(1)]

   456       show ?thesis by (auto simp:root_def)

   457    qed

   458 qed

   459 

   460 lemma not_in_thread_isolated:

   461   assumes "th \<notin> threads s"

   462   shows "(Th th) \<notin> Field (RAG s)"

   463 proof

   464   assume "(Th th) \<in> Field (RAG s)"

   465   with dm_RAG_threads and range_in assms

   466   show False by (unfold Field_def, blast)

   467 qed

   468 

   469 lemma wf_RAG: "wf (RAG s)"

   470 proof(rule finite_acyclic_wf)

   471   from finite_RAG show "finite (RAG s)" .

   472 next

   473   from acyclic_RAG show "acyclic (RAG s)" .

   474 qed

   475 

   476 lemma sgv_wRAG: "single_valued (wRAG s)"

   477   using waiting_unique

   478   by (unfold single_valued_def wRAG_def, auto)

   479 

   480 lemma sgv_hRAG: "single_valued (hRAG s)"

   481   using holding_unique 

   482   by (unfold single_valued_def hRAG_def, auto)

   483 

   484 lemma sgv_tRAG: "single_valued (tRAG s)"

   485   by (unfold tRAG_def, rule single_valued_relcomp, 

   486               insert sgv_wRAG sgv_hRAG, auto)

   487 

   488 lemma acyclic_tRAG: "acyclic (tRAG s)"

   489 proof(unfold tRAG_def, rule acyclic_compose)

   490   show "acyclic (RAG s)" using acyclic_RAG .

   491 next

   492   show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto

   493 next

   494   show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto

   495 qed

   496 

   497 lemma sgv_RAG: "single_valued (RAG s)"

   498   using unique_RAG by (auto simp:single_valued_def)

   499 

   500 lemma rtree_RAG: "rtree (RAG s)"

   501   using sgv_RAG acyclic_RAG

   502   by (unfold rtree_def rtree_axioms_def sgv_def, auto)

   503 

   504 end

   505 

   506 

   507 sublocale valid_trace < rtree_RAG: rtree "RAG s"

   508 proof

   509   show "single_valued (RAG s)"

   510   apply (intro_locales)

   511     by (unfold single_valued_def, 

   512         auto intro:unique_RAG)

   513 

   514   show "acyclic (RAG s)"

   515      by (rule acyclic_RAG)

   516 qed

   517 

   518 sublocale valid_trace < rtree_s: rtree "tRAG s"

   519 proof(unfold_locales)

   520   from sgv_tRAG show "single_valued (tRAG s)" .

   521 next

   522   from acyclic_tRAG show "acyclic (tRAG s)" .

   523 qed

   524 

   525 sublocale valid_trace < fsbtRAGs : fsubtree "RAG s"

   526 proof -

   527   show "fsubtree (RAG s)"

   528   proof(intro_locales)

   529     show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .

   530   next

   531     show "fsubtree_axioms (RAG s)"

   532     proof(unfold fsubtree_axioms_def)

   533     find_theorems wf RAG

   534       from wf_RAG show "wf (RAG s)" .

   535     qed

   536   qed

   537 qed

   538 

   539 sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"

   540 proof -

   541   have "fsubtree (tRAG s)"

   542   proof -

   543     have "fbranch (tRAG s)"

   544     proof(unfold tRAG_def, rule fbranch_compose)

   545         show "fbranch (wRAG s)"

   546         proof(rule finite_fbranchI)

   547            from finite_RAG show "finite (wRAG s)"

   548            by (unfold RAG_split, auto)

   549         qed

   550     next

   551         show "fbranch (hRAG s)"

   552         proof(rule finite_fbranchI)

   553            from finite_RAG 

   554            show "finite (hRAG s)" by (unfold RAG_split, auto)

   555         qed

   556     qed

   557     moreover have "wf (tRAG s)"

   558     proof(rule wf_subset)

   559       show "wf (RAG s O RAG s)" using wf_RAG

   560         by (fold wf_comp_self, simp)

   561     next

   562       show "tRAG s \<subseteq> (RAG s O RAG s)"

   563         by (unfold tRAG_alt_def, auto)

   564     qed

   565     ultimately show ?thesis

   566       by (unfold fsubtree_def fsubtree_axioms_def,auto)

   567   qed

   568   from this[folded tRAG_def] show "fsubtree (tRAG s)" .

   569 qed

   570 

   571 lemma Max_UNION: 

   572   assumes "finite A"

   573   and "A \<noteq> {}"

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

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

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

   577   using assms[simp]

   578 proof -

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

   580     by (fold Union_image_eq, simp)

   581   also have "... = ?R"

   582     by (subst Max_Union, simp+)

   583   finally show ?thesis .

   584 qed

   585 

   586 lemma max_Max_eq:

   587   assumes "finite A"

   588     and "A \<noteq> {}"

   589     and "x = y"

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

   591 proof -

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

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

   594       by (subst Max.insert, simp+)

   595   finally show ?thesis by simp

   596 qed

   597 

   598 context valid_trace

   599 begin

   600 

   601 (* ddd *)

   602 lemma cp_gen_rec:

   603   assumes "x = Th th"

   604   shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"

   605 proof(cases "children (tRAG s) x = {}")

   606   case True

   607   show ?thesis

   608     by (unfold True cp_gen_def subtree_children, simp add:assms)

   609 next

   610   case False

   611   hence [simp]: "children (tRAG s) x \<noteq> {}" by auto

   612   note fsbttRAGs.finite_subtree[simp]

   613   have [simp]: "finite (children (tRAG s) x)"

   614      by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], 

   615             rule children_subtree)

   616   { fix r x

   617     have "subtree r x \<noteq> {}" by (auto simp:subtree_def)

   618   } note this[simp]

   619   have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}"

   620   proof -

   621     from False obtain q where "q \<in> children (tRAG s) x" by blast

   622     moreover have "subtree (tRAG s) q \<noteq> {}" by simp

   623     ultimately show ?thesis by blast

   624   qed

   625   have h: "Max ((the_preced s \<circ> the_thread) `

   626                 ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) =

   627         Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)"

   628                      (is "?L = ?R")

   629   proof -

   630     let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L

   631     let "Max (_ \<union> (?h ` ?B))" = ?R

   632     let ?L1 = "?f ` \<Union>(?g ` ?B)"

   633     have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)"

   634     proof -

   635       have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp

   636       also have "... =  (\<Union> x \<in> ?B. ?f ` (?g x))" by auto

   637       finally have "Max ?L1 = Max ..." by simp

   638       also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"

   639         by (subst Max_UNION, simp+)

   640       also have "... = Max (cp_gen s ` children (tRAG s) x)"

   641           by (unfold image_comp cp_gen_alt_def, simp)

   642       finally show ?thesis .

   643     qed

   644     show ?thesis

   645     proof -

   646       have "?L = Max (?f ` ?A \<union> ?L1)" by simp

   647       also have "... = max (the_preced s (the_thread x)) (Max ?L1)"

   648             by (subst Max_Un, simp+)

   649       also have "... = max (?f x) (Max (?h ` ?B))"

   650         by (unfold eq_Max_L1, simp)

   651       also have "... =?R"

   652         by (rule max_Max_eq, (simp)+, unfold assms, simp)

   653       finally show ?thesis .

   654     qed

   655   qed  thus ?thesis 

   656           by (fold h subtree_children, unfold cp_gen_def, simp) 

   657 qed

   658 

   659 lemma cp_rec:

   660   "cp s th = Max ({the_preced s th} \<union> 

   661                      (cp s o the_thread) ` children (tRAG s) (Th th))"

   662 proof -

   663   have "Th th = Th th" by simp

   664   note h =  cp_gen_def_cond[OF this] cp_gen_rec[OF this]

   665   show ?thesis 

   666   proof -

   667     have "cp_gen s ` children (tRAG s) (Th th) = 

   668                 (cp s \<circ> the_thread) ` children (tRAG s) (Th th)"

   669     proof(rule cp_gen_over_set)

   670       show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th"

   671         by (unfold tRAG_alt_def, auto simp:children_def)

   672     qed

   673     thus ?thesis by (subst (1) h(1), unfold h(2), simp)

   674   qed

   675 qed

   676 

   677 end

   678 

   679 (* keep *)

   680 lemma next_th_holding:

   681   assumes vt: "vt s"

   682   and nxt: "next_th s th cs th'"

   683   shows "holding (wq s) th cs"

   684 proof -

   685   from nxt[unfolded next_th_def]

   686   obtain rest where h: "wq s cs = th # rest"

   687                        "rest \<noteq> []" 

   688                        "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto

   689   thus ?thesis

   690     by (unfold cs_holding_def, auto)

   691 qed

   692 

   693 context valid_trace

   694 begin

   695 

   696 lemma next_th_waiting:

   697   assumes nxt: "next_th s th cs th'"

   698   shows "waiting (wq s) th' cs"

   699 proof -

   700   from nxt[unfolded next_th_def]

   701   obtain rest where h: "wq s cs = th # rest"

   702                        "rest \<noteq> []" 

   703                        "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto

   704   from wq_distinct[of cs, unfolded h]

   705   have dst: "distinct (th # rest)" .

   706   have in_rest: "th' \<in> set rest"

   707   proof(unfold h, rule someI2)

   708     show "distinct rest \<and> set rest = set rest" using dst by auto

   709   next

   710     fix x assume "distinct x \<and> set x = set rest"

   711     with h(2)

   712     show "hd x \<in> set (rest)" by (cases x, auto)

   713   qed

   714   hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)

   715   moreover have "th' \<noteq> hd (wq s cs)"

   716     by (unfold h(1), insert in_rest dst, auto)

   717   ultimately show ?thesis by (auto simp:cs_waiting_def)

   718 qed

   719 

   720 lemma next_th_RAG:

   721   assumes nxt: "next_th (s::event list) th cs th'"

   722   shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"

   723   using vt assms next_th_holding next_th_waiting

   724   by (unfold s_RAG_def, simp)

   725 

   726 end

   727 

   728 -- {* A useless definition *}

   729 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"

   730 where "cps s = {(th, cp s th) | th . th \<in> threads s}"

   731 

   732 

   733 text {* (* ddd *)

   734   One beauty of our modelling is that we follow the definitional extension tradition of HOL.

   735   The benefit of such a concise and miniature model is that  large number of intuitively 

   736   obvious facts are derived as lemmas, rather than asserted as axioms.

   737 *}

   738 

   739 text {*

   740   However, the lemmas in the forthcoming several locales are no longer 

   741   obvious. These lemmas show how the current precedences should be recalculated 

   742   after every execution step (in our model, every step is represented by an event, 

   743   which in turn, represents a system call, or operation). Each operation is 

   744   treated in a separate locale.

   745 

   746   The complication of current precedence recalculation comes 

   747   because the changing of RAG needs to be taken into account, 

   748   in addition to the changing of precedence. 

   749   The reason RAG changing affects current precedence is that,

   750   according to the definition, current precedence 

   751   of a thread is the maximum of the precedences of its dependants, 

   752   where the dependants are defined in terms of RAG.

   753 

   754   Therefore, each operation, lemmas concerning the change of the precedences 

   755   and RAG are derived first, so that the lemmas about

   756   current precedence recalculation can be based on.

   757 *}

   758 

   759 text {* (* ddd *)

   760   The following locale @{text "step_set_cps"} investigates the recalculation 

   761   after the @{text "Set"} operation.

   762 *}

   763 locale step_set_cps =

   764   fixes s' th prio s 

   765   -- {* @{text "s'"} is the system state before the operation *}

   766   -- {* @{text "s"} is the system state after the operation *}

   767   defines s_def : "s \<equiv> (Set th prio#s')" 

   768   -- {* @{text "s"} is assumed to be a legitimate state, from which

   769          the legitimacy of @{text "s"} can be derived. *}

   770   assumes vt_s: "vt s"

   771 

   772 sublocale step_set_cps < vat_s : valid_trace "s"

   773 proof

   774   from vt_s show "vt s" .

   775 qed

   776 

   777 sublocale step_set_cps < vat_s' : valid_trace "s'"

   778 proof

   779   from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .

   780 qed

   781 

   782 context step_set_cps 

   783 begin

   784 

   785 text {* (* ddd *)

   786   The following two lemmas confirm that @{text "Set"}-operating only changes the precedence 

   787   of the initiating thread.

   788 *}

   789 

   790 lemma eq_preced:

   791   assumes "th' \<noteq> th"

   792   shows "preced th' s = preced th' s'"

   793 proof -

   794   from assms show ?thesis 

   795     by (unfold s_def, auto simp:preced_def)

   796 qed

   797 

   798 lemma eq_the_preced: 

   799   fixes th'

   800   assumes "th' \<noteq> th"

   801   shows "the_preced s th' = the_preced s' th'"

   802   using assms

   803   by (unfold the_preced_def, intro eq_preced, simp)

   804 

   805 text {*

   806   The following lemma assures that the resetting of priority does not change the RAG. 

   807 *}

   808 

   809 lemma eq_dep: "RAG s = RAG s'"

   810   by (unfold s_def RAG_set_unchanged, auto)

   811 

   812 text {* (* ddd *)

   813   Th following lemma @{text "eq_cp_pre"} says the priority change of @{text "th"}

   814   only affects those threads, which as @{text "Th th"} in their sub-trees.

   815   

   816   The proof of this lemma is simplified by using the alternative definition of @{text "cp"}. 

   817 *}

   818 

   819 lemma eq_cp_pre:

   820   fixes th' 

   821   assumes nd: "Th th \<notin> subtree (RAG s') (Th th')"

   822   shows "cp s th' = cp s' th'"

   823 proof -

   824   -- {* After unfolding using the alternative definition, elements 

   825         affecting the @{term "cp"}-value of threads become explicit. 

   826         We only need to prove the following: *}

   827   have "Max (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) =

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

   829         (is "Max (?f ` ?S1) = Max (?g ` ?S2)")

   830   proof -

   831     -- {* The base sets are equal. *}

   832     have "?S1 = ?S2" using eq_dep by simp

   833     -- {* The function values on the base set are equal as well. *}

   834     moreover have "\<forall> e \<in> ?S2. ?f e = ?g e"

   835     proof

   836       fix th1

   837       assume "th1 \<in> ?S2"

   838       with nd have "th1 \<noteq> th" by (auto)

   839       from eq_the_preced[OF this]

   840       show "the_preced s th1 = the_preced s' th1" .

   841     qed

   842     -- {* Therefore, the image of the functions are equal. *}

   843     ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq)

   844     thus ?thesis by simp

   845   qed

   846   thus ?thesis by (simp add:cp_alt_def)

   847 qed

   848 

   849 text {*

   850   The following lemma shows that @{term "th"} is not in the 

   851   sub-tree of any other thread. 

   852 *}

   853 lemma th_in_no_subtree:

   854   assumes "th' \<noteq> th"

   855   shows "Th th \<notin> subtree (RAG s') (Th th')"

   856 proof -

   857   have "th \<in> readys s'"

   858   proof -

   859     from step_back_step [OF vt_s[unfolded s_def]]

   860     have "step s' (Set th prio)" .

   861     hence "th \<in> runing s'" by (cases, simp)

   862     thus ?thesis by (simp add:readys_def runing_def)

   863   qed

   864   find_theorems readys subtree

   865   from vat_s'.readys_in_no_subtree[OF this assms(1)]

   866   show ?thesis by blast

   867 qed

   868 

   869 text {* 

   870   By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, 

   871   it is obvious that the change of priority only affects the @{text "cp"}-value 

   872   of the initiating thread @{text "th"}.

   873 *}

   874 lemma eq_cp:

   875   fixes th' 

   876   assumes "th' \<noteq> th"

   877   shows "cp s th' = cp s' th'"

   878   by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])

   879 

   880 end

   881 

   882 text {*

   883   The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.

   884 *}

   885 

   886 locale step_v_cps =

   887   -- {* @{text "th"} is the initiating thread *}

   888   -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}

   889   fixes s' th cs s    -- {* @{text "s'"} is the state before operation*}

   890   defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}

   891   -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}

   892   assumes vt_s: "vt s"

   893 

   894 sublocale step_v_cps < vat_s : valid_trace "s"

   895 proof

   896   from vt_s show "vt s" .

   897 qed

   898 

   899 sublocale step_v_cps < vat_s' : valid_trace "s'"

   900 proof

   901   from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .

   902 qed

   903 

   904 context step_v_cps

   905 begin

   906 

   907 lemma ready_th_s': "th \<in> readys s'"

   908   using step_back_step[OF vt_s[unfolded s_def]]

   909   by (cases, simp add:runing_def)

   910 

   911 lemma ancestors_th: "ancestors (RAG s') (Th th) = {}"

   912 proof -

   913   from vat_s'.readys_root[OF ready_th_s']

   914   show ?thesis

   915   by (unfold root_def, simp)

   916 qed

   917 

   918 lemma holding_th: "holding s' th cs"

   919 proof -

   920   from vt_s[unfolded s_def]

   921   have " PIP s' (V th cs)" by (cases, simp)

   922   thus ?thesis by (cases, auto)

   923 qed

   924 

   925 lemma edge_of_th:

   926     "(Cs cs, Th th) \<in> RAG s'" 

   927 proof -

   928  from holding_th

   929  show ?thesis 

   930     by (unfold s_RAG_def holding_eq, auto)

   931 qed

   932 

   933 lemma ancestors_cs: 

   934   "ancestors (RAG s') (Cs cs) = {Th th}"

   935 proof -

   936   have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th)  \<union>  {Th th}"

   937   proof(rule vat_s'.rtree_RAG.ancestors_accum)

   938     from vt_s[unfolded s_def]

   939     have " PIP s' (V th cs)" by (cases, simp)

   940     thus "(Cs cs, Th th) \<in> RAG s'" 

   941     proof(cases)

   942       assume "holding s' th cs"

   943       from this[unfolded holding_eq]

   944       show ?thesis by (unfold s_RAG_def, auto)

   945     qed

   946   qed

   947   from this[unfolded ancestors_th] show ?thesis by simp

   948 qed

   949 

   950 lemma preced_kept: "the_preced s = the_preced s'"

   951   by (auto simp: s_def the_preced_def preced_def)

   952 

   953 end

   954 

   955 text {*

   956   The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 

   957   which represents the case when there is another thread @{text "th'"}

   958   to take over the critical resource released by the initiating thread @{text "th"}.

   959 *}

   960 locale step_v_cps_nt = step_v_cps +

   961   fixes th'

   962   -- {* @{text "th'"} is assumed to take over @{text "cs"} *}

   963   assumes nt: "next_th s' th cs th'" 

   964 

   965 context step_v_cps_nt

   966 begin

   967 

   968 text {*

   969   Lemma @{text "RAG_s"} confirms the change of RAG:

   970   two edges removed and one added, as shown by the following diagram.

   971 *}

   972 

   973 (*

   974   RAG before the V-operation

   975     th1 ----|

   976             |

   977     th' ----|

   978             |----> cs -----|

   979     th2 ----|              |

   980             |              |

   981     th3 ----|              |

   982                            |------> th

   983     th4 ----|              |

   984             |              |

   985     th5 ----|              |

   986             |----> cs'-----|

   987     th6 ----|

   988             |

   989     th7 ----|

   990 

   991  RAG after the V-operation

   992     th1 ----|

   993             |

   994             |----> cs ----> th'

   995     th2 ----|              

   996             |              

   997     th3 ----|              

   998                            

   999     th4 ----|              

  1000             |              

  1001     th5 ----|              

  1002             |----> cs'----> th

  1003     th6 ----|

  1004             |

  1005     th7 ----|

  1006 *)

  1007 

  1008 lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"

  1009                 using next_th_RAG[OF nt]  .

  1010 

  1011 lemma ancestors_th': 

  1012   "ancestors (RAG s') (Th th') = {Th th, Cs cs}" 

  1013 proof -

  1014   have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}"

  1015   proof(rule  vat_s'.rtree_RAG.ancestors_accum)

  1016     from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto

  1017   qed

  1018   thus ?thesis using ancestors_th ancestors_cs by auto

  1019 qed

  1020 

  1021 lemma RAG_s:

  1022   "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>

  1023                                          {(Cs cs, Th th')}"

  1024 proof -

  1025   from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]

  1026     and nt show ?thesis  by (auto intro:next_th_unique)

  1027 qed

  1028 

  1029 lemma subtree_kept:

  1030   assumes "th1 \<notin> {th, th'}"

  1031   shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R")

  1032 proof -

  1033   let ?RAG' = "(RAG s' - {(Cs cs, Th th), (Th th', Cs cs)})"

  1034   let ?RAG'' = "?RAG' \<union> {(Cs cs, Th th')}"

  1035   have "subtree ?RAG' (Th th1) = ?R" 

  1036   proof(rule subset_del_subtree_outside)

  1037     show "Range {(Cs cs, Th th), (Th th', Cs cs)} \<inter> subtree (RAG s') (Th th1) = {}"

  1038     proof -

  1039       have "(Th th) \<notin> subtree (RAG s') (Th th1)"

  1040       proof(rule subtree_refute)

  1041         show "Th th1 \<notin> ancestors (RAG s') (Th th)"

  1042           by (unfold ancestors_th, simp)

  1043       next

  1044         from assms show "Th th1 \<noteq> Th th" by simp

  1045       qed

  1046       moreover have "(Cs cs) \<notin>  subtree (RAG s') (Th th1)"

  1047       proof(rule subtree_refute)

  1048         show "Th th1 \<notin> ancestors (RAG s') (Cs cs)"

  1049           by (unfold ancestors_cs, insert assms, auto)

  1050       qed simp

  1051       ultimately have "{Th th, Cs cs} \<inter> subtree (RAG s') (Th th1) = {}" by auto

  1052       thus ?thesis by simp

  1053      qed

  1054   qed

  1055   moreover have "subtree ?RAG'' (Th th1) =  subtree ?RAG' (Th th1)"

  1056   proof(rule subtree_insert_next)

  1057     show "Th th' \<notin> subtree (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th1)"

  1058     proof(rule subtree_refute)

  1059       show "Th th1 \<notin> ancestors (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th')"

  1060             (is "_ \<notin> ?R")

  1061       proof -

  1062           have "?R \<subseteq> ancestors (RAG s') (Th th')" by (rule ancestors_mono, auto)

  1063           moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp

  1064           ultimately show ?thesis by auto

  1065       qed

  1066     next

  1067       from assms show "Th th1 \<noteq> Th th'" by simp

  1068     qed

  1069   qed

  1070   ultimately show ?thesis by (unfold RAG_s, simp)

  1071 qed

  1072 

  1073 lemma cp_kept:

  1074   assumes "th1 \<notin> {th, th'}"

  1075   shows "cp s th1 = cp s' th1"

  1076     by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp)

  1077 

  1078 end

  1079 

  1080 locale step_v_cps_nnt = step_v_cps +

  1081   assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"

  1082 

  1083 context step_v_cps_nnt

  1084 begin

  1085 

  1086 lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"

  1087 proof -

  1088   from nnt and  step_RAG_v[OF vt_s[unfolded s_def], folded s_def]

  1089   show ?thesis by auto

  1090 qed

  1091 

  1092 lemma subtree_kept:

  1093   assumes "th1 \<noteq> th"

  1094   shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)"

  1095 proof(unfold RAG_s, rule subset_del_subtree_outside)

  1096   show "Range {(Cs cs, Th th)} \<inter> subtree (RAG s') (Th th1) = {}"

  1097   proof -

  1098     have "(Th th) \<notin> subtree (RAG s') (Th th1)"

  1099     proof(rule subtree_refute)

  1100       show "Th th1 \<notin> ancestors (RAG s') (Th th)"

  1101           by (unfold ancestors_th, simp)

  1102     next

  1103       from assms show "Th th1 \<noteq> Th th" by simp

  1104     qed

  1105     thus ?thesis by auto

  1106   qed

  1107 qed

  1108 

  1109 lemma cp_kept_1:

  1110   assumes "th1 \<noteq> th"

  1111   shows "cp s th1 = cp s' th1"

  1112     by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp)

  1113 

  1114 lemma subtree_cs: "subtree (RAG s') (Cs cs) = {Cs cs}"

  1115 proof -

  1116   { fix n

  1117     have "(Cs cs) \<notin> ancestors (RAG s') n"

  1118     proof

  1119       assume "Cs cs \<in> ancestors (RAG s') n"

  1120       hence "(n, Cs cs) \<in> (RAG s')^+" by (auto simp:ancestors_def)

  1121       from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> RAG s'" by auto

  1122       then obtain th' where "nn = Th th'"

  1123         by (unfold s_RAG_def, auto)

  1124       from h[unfolded this] have "(Th th', Cs cs) \<in> RAG s'" .

  1125       from this[unfolded s_RAG_def]

  1126       have "waiting (wq s') th' cs" by auto

  1127       from this[unfolded cs_waiting_def]

  1128       have "1 < length (wq s' cs)"

  1129           by (cases "wq s' cs", auto)

  1130       from holding_next_thI[OF holding_th this]

  1131       obtain th' where "next_th s' th cs th'" by auto

  1132       with nnt show False by auto

  1133     qed

  1134   } note h = this