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 

   864   find_theorems readys subtree

  1146 find_theorems "subtree" "_ - _" RAG

  1623     find_theorems readys subtree s'