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       from wf_RAG show "wf (RAG s)" .

   534     qed

   535   qed

   536 qed

   537 

   538 sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"

   539 proof -

   540   have "fsubtree (tRAG s)"

   541   proof -

   542     have "fbranch (tRAG s)"

   543     proof(unfold tRAG_def, rule fbranch_compose)

   544         show "fbranch (wRAG s)"

   545         proof(rule finite_fbranchI)

   546            from finite_RAG show "finite (wRAG s)"

   547            by (unfold RAG_split, auto)

   548         qed

   549     next

   550         show "fbranch (hRAG s)"

   551         proof(rule finite_fbranchI)

   552            from finite_RAG 

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

   554         qed

   555     qed

   556     moreover have "wf (tRAG s)"

   557     proof(rule wf_subset)

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

   559         by (fold wf_comp_self, simp)

   560     next

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

   562         by (unfold tRAG_alt_def, auto)

   563     qed

   564     ultimately show ?thesis

   565       by (unfold fsubtree_def fsubtree_axioms_def,auto)

   566   qed

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

   568 qed

   569 

   570 lemma Max_UNION: 

   571   assumes "finite A"

   572   and "A \<noteq> {}"

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

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

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

   576   using assms[simp]

   577 proof -

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

   579     by (fold Union_image_eq, simp)

   580   also have "... = ?R"

   581     by (subst Max_Union, simp+)

   582   finally show ?thesis .

   583 qed

   584 

   585 lemma max_Max_eq:

   586   assumes "finite A"

   587     and "A \<noteq> {}"

   588     and "x = y"

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

   590 proof -

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

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

   593       by (subst Max.insert, simp+)

   594   finally show ?thesis by simp

   595 qed

   596 

   597 context valid_trace

   598 begin

   599 

   600 (* ddd *)

   601 lemma cp_gen_rec:

   602   assumes "x = Th th"

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

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

   605   case True

   606   show ?thesis

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

   608 next

   609   case False

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

   611   note fsbttRAGs.finite_subtree[simp]

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

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

   614             rule children_subtree)

   615   { fix r x

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

   617   } note this[simp]

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

   619   proof -

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

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

   622     ultimately show ?thesis by blast

   623   qed

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

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

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

   627                      (is "?L = ?R")

   628   proof -

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

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

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

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

   633     proof -

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

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

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

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

   638         by (subst Max_UNION, simp+)

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

   640           by (unfold image_comp cp_gen_alt_def, simp)

   641       finally show ?thesis .

   642     qed

   643     show ?thesis

   644     proof -

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

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

   647             by (subst Max_Un, simp+)

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

   649         by (unfold eq_Max_L1, simp)

   650       also have "... =?R"

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

   652       finally show ?thesis .

   653     qed

   654   qed  thus ?thesis 

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

   656 qed

   657 

   658 lemma cp_rec:

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

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

   661 proof -

   662   have "Th th = Th th" by simp

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

   664   show ?thesis 

   665   proof -

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

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

   668     proof(rule cp_gen_over_set)

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

   670         by (unfold tRAG_alt_def, auto simp:children_def)

   671     qed

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

   673   qed

   674 qed

   675 

   676 end

   677 

   678 (* keep *)

   679 lemma next_th_holding:

   680   assumes vt: "vt s"

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

   682   shows "holding (wq s) th cs"

   683 proof -

   684   from nxt[unfolded next_th_def]

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

   686                        "rest \<noteq> []" 

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

   688   thus ?thesis

   689     by (unfold cs_holding_def, auto)

   690 qed

   691 

   692 context valid_trace

   693 begin

   694 

   695 lemma next_th_waiting:

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

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

   698 proof -

   699   from nxt[unfolded next_th_def]

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

   701                        "rest \<noteq> []" 

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

   703   from wq_distinct[of cs, unfolded h]

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

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

   706   proof(unfold h, rule someI2)

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

   708   next

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

   710     with h(2)

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

   712   qed

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

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

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

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

   717 qed

   718 

   719 lemma next_th_RAG:

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

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

   722   using vt assms next_th_holding next_th_waiting

   723   by (unfold s_RAG_def, simp)

   724 

   725 end

   726 

   727 -- {* A useless definition *}

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

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

   730 

   731 

   732 text {* (* ddd *)

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

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

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

   736 *}

   737 

   738 text {*

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

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

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

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

   743   treated in a separate locale.

   744 

   745   The complication of current precedence recalculation comes 

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

   747   in addition to the changing of precedence. 

   748   The reason RAG changing affects current precedence is that,

   749   according to the definition, current precedence 

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

   751   where the dependants are defined in terms of RAG.

   752 

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

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

   755   current precedence recalculation can be based on.

   756 *}

   757 

   758 text {* (* ddd *)

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

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

   761 *}

   762 locale step_set_cps =

   763   fixes s' th prio s 

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

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

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

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

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

   769   assumes vt_s: "vt s"

   770 

   771 sublocale step_set_cps < vat_s : valid_trace "s"

   772 proof

   773   from vt_s show "vt s" .

   774 qed

   775 

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

   777 proof

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

   779 qed

   780 

   781 context step_set_cps 

   782 begin

   783 

   784 text {* (* ddd *)

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

   786   of the initiating thread.

   787 *}

   788 

   789 lemma eq_preced:

   790   assumes "th' \<noteq> th"

   791   shows "preced th' s = preced th' s'"

   792 proof -

   793   from assms show ?thesis 

   794     by (unfold s_def, auto simp:preced_def)

   795 qed

   796 

   797 lemma eq_the_preced: 

   798   fixes th'

   799   assumes "th' \<noteq> th"

   800   shows "the_preced s th' = the_preced s' th'"

   801   using assms

   802   by (unfold the_preced_def, intro eq_preced, simp)

   803 

   804 text {*

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

   806 *}

   807 

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

   809   by (unfold s_def RAG_set_unchanged, auto)

   810 

   811 text {* (* ddd *)

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

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

   814   

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

   816 *}

   817 

   818 lemma eq_cp_pre:

   819   fixes th' 

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

   821   shows "cp s th' = cp s' th'"

   822 proof -

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

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

   825         We only need to prove the following: *}

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

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

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

   829   proof -

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

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

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

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

   834     proof

   835       fix th1

   836       assume "th1 \<in> ?S2"

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

   838       from eq_the_preced[OF this]

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

   840     qed

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

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

   843     thus ?thesis by simp

   844   qed

   845   thus ?thesis by (simp add:cp_alt_def)

   846 qed

   847 

   848 text {*

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

   850   sub-tree of any other thread. 

   851 *}

   852 lemma th_in_no_subtree:

   853   assumes "th' \<noteq> th"

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

   855 proof -

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

   857   proof -

   858     from step_back_step [OF vt_s[unfolded s_def]]

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

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

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

   862   qed

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

   864   show ?thesis by blast

   865 qed

   866 

   867 text {* 

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

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

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

   871 *}

   872 lemma eq_cp:

   873   fixes th' 

   874   assumes "th' \<noteq> th"

   875   shows "cp s th' = cp s' th'"

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

   877 

   878 end

   879 

   880 text {*

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

   882 *}

   883 

   884 locale step_v_cps =

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

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

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

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

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

   890   assumes vt_s: "vt s"

   891 

   892 sublocale step_v_cps < vat_s : valid_trace "s"

   893 proof

   894   from vt_s show "vt s" .

   895 qed

   896 

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

   898 proof

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

   900 qed

   901 

   902 context step_v_cps

   903 begin

   904 

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

   906   using step_back_step[OF vt_s[unfolded s_def]]

   907   by (cases, simp add:runing_def)

   908 

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

   910 proof -

   911   from vat_s'.readys_root[OF ready_th_s']

   912   show ?thesis

   913   by (unfold root_def, simp)

   914 qed

   915 

   916 lemma holding_th: "holding s' th cs"

   917 proof -

   918   from vt_s[unfolded s_def]

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

   920   thus ?thesis by (cases, auto)

   921 qed

   922 

   923 lemma edge_of_th:

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

   925 proof -

   926  from holding_th

   927  show ?thesis 

   928     by (unfold s_RAG_def holding_eq, auto)

   929 qed

   930 

   931 lemma ancestors_cs: 

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

   933 proof -

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

   935   proof(rule vat_s'.rtree_RAG.ancestors_accum)

   936     from vt_s[unfolded s_def]

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

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

   939     proof(cases)

   940       assume "holding s' th cs"

   941       from this[unfolded holding_eq]

   942       show ?thesis by (unfold s_RAG_def, auto)

   943     qed

   944   qed

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

   946 qed

   947 

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

   949   by (auto simp: s_def the_preced_def preced_def)

   950 

   951 end

   952 

   953 text {*

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

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

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

   957 *}

   958 locale step_v_cps_nt = step_v_cps +

   959   fixes th'

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

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

   962 

   963 context step_v_cps_nt

   964 begin

   965 

   966 text {*

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

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

   969 *}

   970 

   971 (*

   972   RAG before the V-operation

   973     th1 ----|

   974             |

   975     th' ----|

   976             |----> cs -----|

   977     th2 ----|              |

   978             |              |

   979     th3 ----|              |

   980                            |------> th

   981     th4 ----|              |

   982             |              |

   983     th5 ----|              |

   984             |----> cs'-----|

   985     th6 ----|

   986             |

   987     th7 ----|

   988 

   989  RAG after the V-operation

   990     th1 ----|

   991             |

   992             |----> cs ----> th'

   993     th2 ----|              

   994             |              

   995     th3 ----|              

   996                            

   997     th4 ----|              

   998             |              

   999     th5 ----|              

  1000             |----> cs'----> th

  1001     th6 ----|

  1002             |

  1003     th7 ----|

  1004 *)

  1005 

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

  1007                 using next_th_RAG[OF nt]  .

  1008 

  1009 lemma ancestors_th': 

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

  1011 proof -

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

  1013   proof(rule  vat_s'.rtree_RAG.ancestors_accum)

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

  1015   qed

  1016   thus ?thesis using ancestors_th ancestors_cs by auto

  1017 qed

  1018 

  1019 lemma RAG_s:

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

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

  1022 proof -

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

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

  1025 qed

  1026 

  1027 lemma subtree_kept:

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

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

  1030 proof -

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

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

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

  1034   proof(rule subset_del_subtree_outside)

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

  1036     proof -

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

  1038       proof(rule subtree_refute)

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

  1040           by (unfold ancestors_th, simp)

  1041       next

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

  1043       qed

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

  1045       proof(rule subtree_refute)

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

  1047           by (unfold ancestors_cs, insert assms, auto)

  1048       qed simp

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

  1050       thus ?thesis by simp

  1051      qed

  1052   qed

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

  1054   proof(rule subtree_insert_next)

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

  1056     proof(rule subtree_refute)

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

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

  1059       proof -

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

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

  1062           ultimately show ?thesis by auto

  1063       qed

  1064     next

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

  1066     qed

  1067   qed

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

  1069 qed

  1070 

  1071 lemma cp_kept:

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

  1073   shows "cp s th1 = cp s' th1"

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

  1075 

  1076 end

  1077 

  1078 locale step_v_cps_nnt = step_v_cps +

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

  1080 

  1081 context step_v_cps_nnt

  1082 begin

  1083 

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

  1085 proof -

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

  1087   show ?thesis by auto

  1088 qed

  1089 

  1090 lemma subtree_kept:

  1091   assumes "th1 \<noteq> th"

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

  1093 proof(unfold RAG_s, rule subset_del_subtree_outside)

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

  1095   proof -

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

  1097     proof(rule subtree_refute)

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

  1099           by (unfold ancestors_th, simp)

  1100     next

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

  1102     qed

  1103     thus ?thesis by auto

  1104   qed

  1105 qed

  1106 

  1107 lemma cp_kept_1:

  1108   assumes "th1 \<noteq> th"

  1109   shows "cp s th1 = cp s' th1"

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

  1111 

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

  1113 proof -

  1114   { fix n

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

  1116     proof

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

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

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

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

  1121         by (unfold s_RAG_def, auto)

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

  1123       from this[unfolded s_RAG_def]

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

  1125       from this[unfolded cs_waiting_def]

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

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

  1128       from holding_next_thI[OF holding_th this]

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

  1130       with nnt show False by auto

  1131     qed

  1132   } note h = this

  1133   {  fix n

  1134      assume "n \<in> subtree (RAG s') (Cs cs)"

  1135      hence "n = (Cs cs)"