403 

   404 lemma eq_RAG: 

   405   "RAG (wq s) = RAG s"

   406   by (unfold cs_RAG_def s_RAG_def, auto)

   407 

   408 text {* 

   409   The following three lemmas shows the shape

   410   of nodes in @{term tRAG}.

   411 *}

   412 lemma tRAG_nodeE:

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

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

   415   using assms

   416   by (auto simp: tRAG_def wRAG_def hRAG_def)

   417 

   418 lemma tRAG_ancestorsE:

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

   420   obtains th where "x = Th th"

   421 proof -

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

   423       by (unfold ancestors_def, auto)

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

   425   then obtain th where "x = Th th"

   426     by (unfold tRAG_alt_def, auto)

   427   from that[OF this] show ?thesis .

   428 qed

   429 

   430 lemma subtree_nodeE:

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

   432   obtains th1 where "n = Th th1"

   433 proof -

   434   show ?thesis

   435   proof(rule subtreeE[OF assms])

   436     assume "n = Th th"

   437     from that[OF this] show ?thesis .

   438   next

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

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

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

   442     proof(induct)

   443       case (base y)

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

   445     next

   446       case (step y z)

   447       thus ?case by auto

   448     qed

   449     with that show ?thesis by auto

   450   qed

   451 qed

   452 

   453 text {*

   454   The following lemmas relate @{term tRAG} with 

   455   @{term RAG} from different perspectives. 

   456 *}

   457 

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

   459 proof -

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

   461     by (rule rtrancl_mono, auto simp:RAG_split)

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

   463     by (rule rtrancl_mono, auto)

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

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

   466 qed

   467 

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

   469 proof -

   470   { fix a

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

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

   473     with tRAG_star_RAG

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

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

   476   } thus ?thesis by auto

   477 qed

   478 

   479 lemma tRAG_trancl_eq:

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

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

   482    (is "?L = ?R")

   483 proof -

   484   { fix th'

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

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

   487     from tranclD[OF this]

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

   489     from tRAG_subtree_RAG and this(2)

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

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

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

   493   } moreover 

   494   { fix th'

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

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

   497     from plus_rpath[OF this]

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

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

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

   501       case (1 xs th' th)

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

   503       show ?case

   504       proof(cases "xs1")

   505         case Nil

   506         from 1(2)[unfolded Cons1 Nil]

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

   508         hence "(Th th', x1) \<in> (RAG s)" 

   509           by (cases, auto)

   510         then obtain cs where "x1 = Cs cs" 

   511               by (unfold s_RAG_def, auto)

   512         from rpath_nnl_lastE[OF rp[unfolded this]]

   513         show ?thesis by auto

   514       next

   515         case (Cons x2 xs2)

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

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

   518         from rpath_edges_on[OF this]

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

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

   521             by (simp add: edges_on_unfold)

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

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

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

   525             by (simp add: edges_on_unfold)

   526         from this eds

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

   528         from this[unfolded eq_x1] 

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

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

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

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

   533            by  (elim rpath_ConsE, simp)

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

   535         show ?thesis

   536         proof(cases "xs2 = []")

   537           case True

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

   539           have "th1 = th" by auto

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

   541         next

   542           case False

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

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

   545           with rt1 show ?thesis by auto

   546         qed

   547       qed

   548     qed

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

   550   } ultimately show ?thesis by blast

   551 qed

   552 

   553 lemma tRAG_trancl_eq_Th:

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

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

   556     using tRAG_trancl_eq by auto

   557 

   558 lemma tRAG_Field:

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

   560   by (unfold tRAG_alt_def Field_def, auto)

   561 

   562 lemma tRAG_mono:

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

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

   565   using assms 

   566   by (unfold tRAG_alt_def, auto)

   567 

   568 lemma tRAG_subtree_eq: 

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

   570    (is "?L = ?R")

   571 proof -

   572   { fix n 

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

   574     hence "n \<in> ?R"

   575     by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) 

   576   } moreover {

   577     fix n

   578     assume "n \<in> ?R"

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

   580       by (auto simp:subtree_def)

   581     from rtranclD[OF this(2)]

   582     have "n \<in> ?L"

   583     proof

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

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

   586       thus ?thesis using subtree_def tRAG_trancl_eq by fastforce

   587     qed (insert h, auto simp:subtree_def)

   588   } ultimately show ?thesis by auto

   589 qed

   590 

   591 lemma threads_set_eq: 

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

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

   594    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)

   595 

   596 lemma RAG_tRAG_transfer:

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

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

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

   600 proof -

   601   { fix n1 n2

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

   603     from this[unfolded tRAG_alt_def]

   604     obtain th1 th2 cs' where 

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

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

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

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

   609     from h(3) and assms(1) 

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

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

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

   613     proof

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

   615       with assms(1) have "(Th th1, Cs cs) \<in> RAG s'" by auto

   616       moreover have "th2 = th''"

   617       proof -

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

   619         from assms(2) cs_in[unfolded this]

   620         have "holding s th'' cs" "holding s th2 cs"

   621           by (unfold s_RAG_def, fold holding_eq, auto)

   622         from held_unique[OF this]

   623         show ?thesis by simp 

   624       qed

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

   626     next

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

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

   629         by (unfold tRAG_alt_def, auto)

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

   631     qed

   632   } moreover {

   633     fix n1 n2

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

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

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

   637     proof

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

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

   640       proof(rule tRAG_mono)

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

   642       qed

   643       ultimately show ?thesis by auto

   644     next

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

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

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

   648       ultimately show ?thesis 

   649         by (unfold eq_n tRAG_alt_def, auto)

   650     qed

   651   } ultimately show ?thesis by auto

   652 qed

   653 

   654 text {* 

   655   The following lemmas gives an alternative definition @{term dependants}

   656   in terms of @{term tRAG}.

   657 *}

   658 

   659 lemma dependants_alt_def:

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

   661   by (metis eq_RAG s_dependants_def tRAG_trancl_eq)

   662 

   663 text {* 

   664   The following lemmas gives another alternative definition @{term dependants}

   665   in terms of @{term RAG}.

   666 *}

   667 

   668 lemma dependants_alt_def1:

   669   "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"

   670   using dependants_alt_def tRAG_trancl_eq by auto

  1450 

  1451 text {*

  1452   As a corollary, this lemma shows that @{term tRAG}

  1453   is also covered by the @{term threads}-set.

  1454 *}

  1455 lemma subtree_tRAG_thread:

  1456   assumes "th \<in> threads s"

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

  1458 proof -

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

  1460     by (unfold tRAG_subtree_eq, simp)

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

  1462   proof

  1463     fix x

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

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

  1466     from this(2)

  1467     show "x \<in> ?R"

  1468     proof(cases rule:subtreeE)

  1469       case 1

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

  1471     next

  1472       case 2

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

  1474     qed

  1475   qed

  1476   finally show ?thesis .

  1477 qed

  2818 text {*

  2819   In this section, it is proved that both @{term RAG} and 

  2820   its converse @{term "(RAG s)^-1"} are well-founded.

  2821   The proof is very simple with the help of

  2822   already proved fact that @{term RAG} is finite.

  2823 *}

  2824 

  2907 

  2908 text {*

  2909   It can be shown that @{term tRAG} is also a 

  2910   finite-branch relational tree (or forest):  

  2911 *}