4312 lemma tRAG_nodeE:

  4317 end

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

  4318 

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

  4319 context valid_trace

  4315   using assms

  4320 begin

  4316   by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def)

  4317 

  4318 lemma subtree_nodeE:

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

  4320   obtains th1 where "n = Th th1"

  4321 proof -

  4322   show ?thesis

  4323   proof(rule subtreeE[OF assms])

  4324     assume "n = Th th"

  4325     from that[OF this] show ?thesis .

  4326   next

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

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

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

  4330     proof(induct)

  4331       case (base y)

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

  4333     next

  4334       case (step y z)

  4335       thus ?case by auto

  4336     qed

  4337     with that show ?thesis by auto

  4338   qed

  4339 qed

  4340 

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

  4342 proof -

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

  4344     by (rule rtrancl_mono, auto simp:RAG_split)

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

  4346     by (rule rtrancl_mono, auto)

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

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

  4349 qed

  4350 

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

  4352 proof -

  4353   { fix a

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

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

  4356     with tRAG_star_RAG

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

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

  4359   } thus ?thesis by auto

  4360 qed

  4361 

  4362 lemma tRAG_trancl_eq:

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

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

  4365    (is "?L = ?R")

  4366 proof -

  4367   { fix th'

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

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

  4370     from tranclD[OF this]

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

  4372     from tRAG_subtree_RAG and this(2)

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

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

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

  4376   } moreover 

  4377   { fix th'

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

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

  4380     from plus_rpath[OF this]

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

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

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

  4384       case (1 xs th' th)

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

  4386       show ?case

  4387       proof(cases "xs1")

  4388         case Nil

  4389         from 1(2)[unfolded Cons1 Nil]

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

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

  4392         then obtain cs where "x1 = Cs cs" 

  4393               by (unfold s_RAG_def, auto)

  4394         from rpath_nnl_lastE[OF rp[unfolded this]]

  4395         show ?thesis by auto

  4396       next

  4397         case (Cons x2 xs2)

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

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

  4400         from rpath_edges_on[OF this]

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

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

  4403             by (simp add: edges_on_unfold)

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

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

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

  4407             by (simp add: edges_on_unfold)

  4408         from this eds

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

  4410         from this[unfolded eq_x1] 

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

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

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

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

  4415            by  (elim rpath_ConsE, simp)

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

  4417         show ?thesis

  4418         proof(cases "xs2 = []")

  4419           case True

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

  4421           have "th1 = th" by auto

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

  4423         next

  4424           case False

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

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

  4427           with rt1 show ?thesis by auto

  4428         qed

  4429       qed

  4430     qed

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

  4432   } ultimately show ?thesis by blast

  4433 qed

  4434 

  4435 lemma tRAG_trancl_eq_Th:

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

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

  4438     using tRAG_trancl_eq by auto

  4439 

  4440 lemma dependants_alt_def:

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

  4442   by (metis eq_RAG s_dependants_def tRAG_trancl_eq)

  4443