9 

    10 section {* Recursive calculation of @{term "cp"} *}

    11 

    12 definition "cp_gen s x =

    13                   Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"

    14 

    15 lemma cp_gen_alt_def:

    16   "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"

    17     by (auto simp:cp_gen_def)

    18 

    19 lemma cp_gen_def_cond: 

    20   assumes "x = Th th"

    21   shows "cp s th = cp_gen s (Th th)"

    22 by (unfold cp_alt_def1 cp_gen_def, simp)

    23 

    24 lemma cp_gen_over_set:

    25   assumes "\<forall> x \<in> A. \<exists> th. x = Th th"

    26   shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"

    27 proof(rule f_image_eq)

    28   fix a

    29   assume "a \<in> A"

    30   from assms[rule_format, OF this]

    31   obtain th where eq_a: "a = Th th" by auto

    32   show "cp_gen s a = (cp s \<circ> the_thread) a"

    33     by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)

    34 qed

    35 

    36 

    37 context valid_trace

    38 begin

    39 (* ddd *)

    40 lemma cp_gen_rec:

    41   assumes "x = Th th"

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

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

    44   case True

    45   show ?thesis

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

    47 next

    48   case False

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

    50   note fsbttRAGs.finite_subtree[simp]

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

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

    53             rule children_subtree)

    54   { fix r x

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

    56   } note this[simp]

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

    58   proof -

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

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

    61     ultimately show ?thesis by blast

    62   qed

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

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

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

    66                      (is "?L = ?R")

    67   proof -

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

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

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

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

    72     proof -

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

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

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

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

    77         by (subst Max_UNION, simp+)

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

    79           by (unfold image_comp cp_gen_alt_def, simp)

    80       finally show ?thesis .

    81     qed

    82     show ?thesis

    83     proof -

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

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

    86             by (subst Max_Un, simp+)

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

    88         by (unfold eq_Max_L1, simp)

    89       also have "... =?R"

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

    91       finally show ?thesis .

    92     qed

    93   qed  thus ?thesis 

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

    95 qed

    96 

    97 lemma cp_rec:

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

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

   100 proof -

   101   have "Th th = Th th" by simp

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

   103   show ?thesis 

   104   proof -

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

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

   107     proof(rule cp_gen_over_set)

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

   109         by (unfold tRAG_alt_def, auto simp:children_def)

   110     qed

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

   112   qed

   113 qed

   114 

   115 end