3026 lemma birth_time_lt:  "s \<noteq> [] \<Longrightarrow> last_set th s < length s"

  3027   apply (induct s, simp)

  3028 proof -

  3029   fix a s

  3030   assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"

  3031     and eq_as: "a # s \<noteq> []"

  3032   show "last_set th (a # s) < length (a # s)"

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

  3034     case False

  3035     from False show ?thesis

  3036       by (cases a, auto simp:last_set.simps)

  3037   next

  3038     case True

  3039     from ih [OF True] show ?thesis

  3040       by (cases a, auto simp:last_set.simps)

  3041   qed

  3042 qed

  3043 

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

  3045   by (induct s, auto simp:threads.simps)

  3046 

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

  3048   apply (drule_tac th_in_ne)

  3049   by (unfold preced_def, auto intro: birth_time_lt)

  3050 

  3051 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only

  3052        difference is the order of arguemts. *}

  3053 definition "the_preced s th = preced th s"

  3054 

  3055 lemma inj_the_preced: 

  3056   "inj_on (the_preced s) (threads s)"

  3057   by (metis inj_onI preced_unique the_preced_def)

  3058 

  3059 text {* @{term "the_thread"} extracts thread out of RAG node. *}

  3060 fun the_thread :: "node \<Rightarrow> thread" where

  3061    "the_thread (Th th) = th"

  3062 

  3063 text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}

  3064 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"

  3065 

  3066 text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}

  3067 definition "hRAG (s::state) =  {(Cs cs, Th th) | th cs. holding s th cs}"

  3068 

  3069 text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}

  3070 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"

  3071   by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 

  3072              s_holding_abv cs_RAG_def, auto)

  3073 

  3074 text {* 

  3075   The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.

  3076   It characterizes the dependency between threads when calculating current

  3077   precedences. It is defined as the composition of the above two sub-graphs, 

  3078   names @{term "wRAG"} and @{term "hRAG"}.

  3079  *}

  3080 definition "tRAG s = wRAG s O hRAG s"

  3081 

  3082 (* ccc *)

  3083 

  3084 definition "cp_gen s x =

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

  3086 

  3087 lemma tRAG_alt_def: 

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

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

  3090  by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)

  3091 

  3092 lemma tRAG_Field:

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

  3094   by (unfold tRAG_alt_def Field_def, auto)

  3095 

  3096 lemma tRAG_ancestorsE:

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

  3098   obtains th where "x = Th th"

  3099 proof -

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

  3101       by (unfold ancestors_def, auto)

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

  3103   then obtain th where "x = Th th"

  3104     by (unfold tRAG_alt_def, auto)

  3105   from that[OF this] show ?thesis .

  3106 qed

  3107 

  3108 lemma tRAG_mono:

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

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

  3111   using assms 

  3112   by (unfold tRAG_alt_def, auto)

  3113 

  3114 lemma holding_next_thI:

  3115   assumes "holding s th cs"

  3116   and "length (wq s cs) > 1"

  3117   obtains th' where "next_th s th cs th'"

  3118 proof -

  3119   from assms(1)[folded eq_holding, unfolded cs_holding_def]

  3120   have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" .

  3121   then obtain rest where h1: "wq s cs = th#rest" 

  3122     by (cases "wq s cs", auto)

  3123   with assms(2) have h2: "rest \<noteq> []" by auto

  3124   let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"

  3125   have "next_th s th cs ?th'" using  h1(1) h2 

  3126     by (unfold next_th_def, auto)

  3127   from that[OF this] show ?thesis .

  3128 qed

  3129 

  3130 lemma RAG_tRAG_transfer:

  3131   assumes "vt s'"

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

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

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

  3135 proof -

  3136   interpret vt_s': valid_trace "s'" using assms(1)

  3137     by (unfold_locales, simp)

  3138   interpret rtree: rtree "RAG s'"

  3139   proof

  3140   show "single_valued (RAG s')"

  3141   apply (intro_locales)

  3142     by (unfold single_valued_def, 

  3143         auto intro:vt_s'.unique_RAG)

  3144 

  3145   show "acyclic (RAG s')"

  3146      by (rule vt_s'.acyclic_RAG)

  3147   qed

  3148   { fix n1 n2

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

  3150     from this[unfolded tRAG_alt_def]

  3151     obtain th1 th2 cs' where 

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

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

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

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

  3156     from h(3) and assms(2) 

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

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

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

  3160     proof

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

  3162       hence eq_th1: "th1 = th" by simp

  3163       moreover have "th2 = th''"

  3164       proof -

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

  3166         from assms(3) cs_in[unfolded this] rtree.sgv

  3167         show ?thesis

  3168           by (unfold single_valued_def, auto)

  3169       qed

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

  3171     next

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

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

  3174         by (unfold tRAG_alt_def, auto)

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

  3176     qed

  3177   } moreover {

  3178     fix n1 n2

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

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

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

  3182     proof

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

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

  3185       proof(rule tRAG_mono)

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

  3187       qed

  3188       ultimately show ?thesis by auto

  3189     next

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

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

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

  3193       ultimately show ?thesis 

  3194         by (unfold eq_n tRAG_alt_def, auto)

  3195     qed

  3196   } ultimately show ?thesis by auto

  3197 qed

  3198 

  3199 context valid_trace

  3200 begin

  3201 

  3202 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]

  3203 

  3205 

  3206 lemma cp_alt_def:

  3207   "cp s th =  

  3208            Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"

  3209 proof -

  3210   have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =

  3211         Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 

  3212           (is "Max (_ ` ?L) = Max (_ ` ?R)")

  3213   proof -

  3214     have "?L = ?R" 

  3215     by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)

  3216     thus ?thesis by simp

  3217   qed

  3218   thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)

  3219 qed

  3220 

  3221 lemma cp_gen_alt_def:

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

  3223     by (auto simp:cp_gen_def)

  3224 

  3225 lemma tRAG_nodeE:

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

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

  3228   using assms

  3229   by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def)

  3230 

  3231 lemma subtree_nodeE:

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

  3233   obtains th1 where "n = Th th1"

  3234 proof -

  3235   show ?thesis

  3236   proof(rule subtreeE[OF assms])

  3237     assume "n = Th th"

  3238     from that[OF this] show ?thesis .

  3239   next

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

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

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

  3243     proof(induct)

  3244       case (base y)

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

  3246     next

  3247       case (step y z)

  3248       thus ?case by auto

  3249     qed

  3250     with that show ?thesis by auto

  3251   qed

  3252 qed

  3253 

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

  3255 proof -

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

  3257     by (rule rtrancl_mono, auto simp:RAG_split)

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

  3259     by (rule rtrancl_mono, auto)

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

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

  3262 qed

  3263 

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

  3265 proof -

  3266   { fix a

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

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

  3269     with tRAG_star_RAG[of s]

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

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

  3272   } thus ?thesis by auto

  3273 qed

  3274 

  3275 lemma tRAG_trancl_eq:

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

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

  3278    (is "?L = ?R")

  3279 proof -

  3280   { fix th'

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

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

  3283     from tranclD[OF this]

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

  3285     from tRAG_subtree_RAG[of s] and this(2)

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

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

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

  3289   } moreover 

  3290   { fix th'

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

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

  3293     from plus_rpath[OF this]

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

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

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

  3297       case (1 xs th' th)

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

  3299       show ?case

  3300       proof(cases "xs1")

  3301         case Nil

  3302         from 1(2)[unfolded Cons1 Nil]

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

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

  3305         then obtain cs where "x1 = Cs cs" 

  3306               by (unfold s_RAG_def, auto)

  3307         from rpath_nnl_lastE[OF rp[unfolded this]]

  3308         show ?thesis by auto

  3309       next

  3310         case (Cons x2 xs2)

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

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

  3313         from rpath_edges_on[OF this]

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

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

  3316             by (simp add: edges_on_unfold)

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

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

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

  3320             by (simp add: edges_on_unfold)

  3321         from this eds

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

  3323         from this[unfolded eq_x1] 

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

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

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

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

  3328            by  (elim rpath_ConsE, simp)

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

  3330         show ?thesis

  3331         proof(cases "xs2 = []")

  3332           case True

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

  3334           have "th1 = th" by auto

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

  3336         next

  3337           case False

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

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

  3340           with rt1 show ?thesis by auto

  3341         qed

  3342       qed

  3343     qed

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

  3345   } ultimately show ?thesis by blast

  3346 qed

  3347 

  3348 lemma tRAG_trancl_eq_Th:

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

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

  3351     using tRAG_trancl_eq by auto

  3352 

  3353 lemma dependants_alt_def:

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

  3355   by (metis eq_RAG s_dependants_def tRAG_trancl_eq)

  3356   

  3357 context valid_trace

  3358 begin

  3359 

  3360 lemma count_eq_tRAG_plus:

  3361   assumes "cntP s th = cntV s th"

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

  3363   using assms count_eq_dependants dependants_alt_def eq_dependants by auto 

  3364 

  3365 lemma count_eq_RAG_plus:

  3366   assumes "cntP s th = cntV s th"

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

  3368   using assms count_eq_dependants cs_dependants_def eq_RAG by auto

  3369 

  3370 lemma count_eq_RAG_plus_Th:

  3371   assumes "cntP s th = cntV s th"

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

  3373   using count_eq_RAG_plus[OF assms] by auto

  3374 

  3375 lemma count_eq_tRAG_plus_Th:

  3376   assumes "cntP s th = cntV s th"

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

  3378    using count_eq_tRAG_plus[OF assms] by auto

  3379 

  3380 end

  3381 

  3382 lemma tRAG_subtree_eq: 

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

  3384    (is "?L = ?R")

  3385 proof -

  3386   { fix n 

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

  3388     hence "n \<in> ?R"

  3389     by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) 

  3390   } moreover {

  3391     fix n

  3392     assume "n \<in> ?R"

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

  3394       by (auto simp:subtree_def)

  3395     from rtranclD[OF this(2)]

  3396     have "n \<in> ?L"

  3397     proof

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

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

  3400       thus ?thesis using subtree_def tRAG_trancl_eq by fastforce

  3401     qed (insert h, auto simp:subtree_def)

  3402   } ultimately show ?thesis by auto

  3403 qed

  3404 

  3405 lemma threads_set_eq: 

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

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

  3408    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)

  3409 

  3410 lemma cp_alt_def1: 

  3411   "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"

  3412 proof -

  3413   have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =

  3414        ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"

  3415        by auto

  3416   thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)

  3417 qed

  3418 

  3419 lemma cp_gen_def_cond: 

  3420   assumes "x = Th th"

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

  3422 by (unfold cp_alt_def1 cp_gen_def, simp)

  3423 

  3424 lemma cp_gen_over_set:

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

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

  3427 proof(rule f_image_eq)

  3428   fix a

  3429   assume "a \<in> A"

  3430   from assms[rule_format, OF this]

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

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

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

  3434 qed

  3435 

  3436 

  3437 context valid_trace

  3438 begin

  3439 

  3440 lemma RAG_threads:

  3441   assumes "(Th th) \<in> Field (RAG s)"

  3442   shows "th \<in> threads s"

  3443   using assms

  3444   by (metis Field_def UnE dm_RAG_threads range_in vt)

  3445 

  3446 lemma subtree_tRAG_thread:

  3447   assumes "th \<in> threads s"

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

  3449 proof -

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

  3451     by (unfold tRAG_subtree_eq, simp)

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

  3453   proof

  3454     fix x

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

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

  3457     from this(2)

  3458     show "x \<in> ?R"

  3459     proof(cases rule:subtreeE)

  3460       case 1

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

  3462     next

  3463       case 2

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

  3465     qed

  3466   qed

  3467   finally show ?thesis .

  3468 qed

  3469 

  3470 lemma readys_root:

  3471   assumes "th \<in> readys s"

  3472   shows "root (RAG s) (Th th)"

  3473 proof -

  3474   { fix x

  3475     assume "x \<in> ancestors (RAG s) (Th th)"

  3476     hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)

  3477     from tranclD[OF this]

  3478     obtain z where "(Th th, z) \<in> RAG s" by auto

  3479     with assms(1) have False

  3480          apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)

  3481          by (fold wq_def, blast)

  3482   } thus ?thesis by (unfold root_def, auto)

  3483 qed

  3484 

  3485 lemma readys_in_no_subtree:

  3486   assumes "th \<in> readys s"

  3487   and "th' \<noteq> th"

  3488   shows "Th th \<notin> subtree (RAG s) (Th th')" 

  3489 proof

  3490    assume "Th th \<in> subtree (RAG s) (Th th')"

  3491    thus False

  3492    proof(cases rule:subtreeE)

  3493       case 1

  3494       with assms show ?thesis by auto

  3495    next

  3496       case 2

  3497       with readys_root[OF assms(1)]

  3498       show ?thesis by (auto simp:root_def)

  3499    qed

  3500 qed

  3501 

  3502 lemma not_in_thread_isolated:

  3503   assumes "th \<notin> threads s"

  3504   shows "(Th th) \<notin> Field (RAG s)"

  3505 proof

  3506   assume "(Th th) \<in> Field (RAG s)"

  3507   with dm_RAG_threads and range_in assms

  3508   show False by (unfold Field_def, blast)

  3509 qed

  3510 

  3511 lemma wf_RAG: "wf (RAG s)"

  3512 proof(rule finite_acyclic_wf)

  3513   from finite_RAG show "finite (RAG s)" .

  3514 next

  3515   from acyclic_RAG show "acyclic (RAG s)" .

  3516 qed

  3517 

  3518 lemma sgv_wRAG: "single_valued (wRAG s)"

  3519   using waiting_unique

  3520   by (unfold single_valued_def wRAG_def, auto)

  3521 

  3522 lemma sgv_hRAG: "single_valued (hRAG s)"

  3523   using holding_unique 

  3524   by (unfold single_valued_def hRAG_def, auto)

  3525 

  3526 lemma sgv_tRAG: "single_valued (tRAG s)"

  3527   by (unfold tRAG_def, rule single_valued_relcomp, 

  3528               insert sgv_wRAG sgv_hRAG, auto)

  3529 

  3530 lemma acyclic_tRAG: "acyclic (tRAG s)"

  3531 proof(unfold tRAG_def, rule acyclic_compose)

  3532   show "acyclic (RAG s)" using acyclic_RAG .

  3533 next

  3534   show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto

  3535 next

  3536   show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto

  3537 qed

  3538 

  3539 lemma sgv_RAG: "single_valued (RAG s)"

  3540   using unique_RAG by (auto simp:single_valued_def)

  3541 

  3542 lemma rtree_RAG: "rtree (RAG s)"

  3543   using sgv_RAG acyclic_RAG

  3544   by (unfold rtree_def rtree_axioms_def sgv_def, auto)

  3545 

  3546 end

  3547 context valid_trace

  3548 begin

  3549 

  3550 (* ddd *)

  3551 lemma cp_gen_rec:

  3552   assumes "x = Th th"

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

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

  3555   case True

  3556   show ?thesis

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

  3558 next

  3559   case False

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

  3561   note fsbttRAGs.finite_subtree[simp]

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

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

  3564             rule children_subtree)

  3565   { fix r x

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

  3567   } note this[simp]

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

  3569   proof -

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

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

  3572     ultimately show ?thesis by blast

  3573   qed

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

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

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

  3577                      (is "?L = ?R")

  3578   proof -

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

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

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

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

  3583     proof -

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

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

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

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

  3588         by (subst Max_UNION, simp+)

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

  3590           by (unfold image_comp cp_gen_alt_def, simp)

  3591       finally show ?thesis .

  3592     qed

  3593     show ?thesis

  3594     proof -

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

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

  3597             by (subst Max_Un, simp+)

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

  3599         by (unfold eq_Max_L1, simp)

  3600       also have "... =?R"

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

  3602       finally show ?thesis .

  3603     qed

  3604   qed  thus ?thesis 

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

  3606 qed

  3607 

  3608 lemma cp_rec:

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

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

  3611 proof -

  3612   have "Th th = Th th" by simp

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

  3614   show ?thesis 

  3615   proof -

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

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

  3618     proof(rule cp_gen_over_set)

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

  3620         by (unfold tRAG_alt_def, auto simp:children_def)

  3621     qed

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

  3623   qed

  3624 qed

  3625 

  3626 end

  3627 

  3628 end