2710 lemma Max_UNION: 

  2711   assumes "finite A"

  2712   and "A \<noteq> {}"

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

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

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

  2716   using assms[simp]

  2717 proof -

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

  2719     by (fold Union_image_eq, simp)

  2720   also have "... = ?R"

  2721     by (subst Max_Union, simp+)

  2722   finally show ?thesis .

  2723 qed

  2724 

  2725 lemma max_Max_eq:

  2726   assumes "finite A"

  2727     and "A \<noteq> {}"

  2728     and "x = y"

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

  2730 proof -

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

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

  2733       by (subst Max.insert, simp+)

  2734   finally show ?thesis by simp

  2735 qed

  2736 

  2737 lemma birth_time_lt:  

  2738   assumes "s \<noteq> []"

  2739   shows "last_set th s < length s"

  2740   using assms

  2741 proof(induct s)

  2742   case (Cons a s)

  2743   show ?case

  2744   proof(cases "s \<noteq> []")

  2745     case False

  2746     thus ?thesis

  2747       by (cases a, auto)

  2748   next

  2749     case True

  2750     show ?thesis using Cons(1)[OF True]

  2751       by (cases a, auto)

  2752   qed

  2753 qed simp

  2754 

  2755 lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"

  2756   by (induct s, auto)

  2757 

  2758 lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"

  2759   by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)

  2760 

  3903 lemma tRAG_alt_def: 

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

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

  3906  by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)

  3907 

  3908 sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"

  3909 proof -

  3910   have "fsubtree (tRAG s)"

  3911   proof -

  3912     have "fbranch (tRAG s)"

  3913     proof(unfold tRAG_def, rule fbranch_compose)

  3914         show "fbranch (wRAG s)"

  3915         proof(rule finite_fbranchI)

  3916            from finite_RAG show "finite (wRAG s)"

  3917            by (unfold RAG_split, auto)

  3918         qed

  3919     next

  3920         show "fbranch (hRAG s)"

  3921         proof(rule finite_fbranchI)

  3922            from finite_RAG 

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

  3924         qed

  3925     qed

  3926     moreover have "wf (tRAG s)"

  3927     proof(rule wf_subset)

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

  3929         by (fold wf_comp_self, simp)

  3930     next

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

  3932         by (unfold tRAG_alt_def, auto)

  3933     qed

  3934     ultimately show ?thesis

  3935       by (unfold fsubtree_def fsubtree_axioms_def,auto)

  3936   qed

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

  3938 qed

  3939 

  3940