3051 lemma inj_the_preced: 

  3052   "inj_on (the_preced s) (threads s)"

  3053   by (metis inj_onI preced_unique the_preced_def)

  3054 

  3055 lemma tRAG_alt_def: 

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

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

  3058  by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)

  3059 

  3060 lemma tRAG_Field:

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

  3062   by (unfold tRAG_alt_def Field_def, auto)

  3063 

  3064 lemma tRAG_ancestorsE:

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

  3066   obtains th where "x = Th th"

  3067 proof -

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

  3069       by (unfold ancestors_def, auto)

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

  3071   then obtain th where "x = Th th"

  3072     by (unfold tRAG_alt_def, auto)

  3073   from that[OF this] show ?thesis .

  3074 qed

  3075 

  3076 lemma tRAG_mono:

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

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

  3079   using assms 

  3080   by (unfold tRAG_alt_def, auto)

  3081 

  3082 lemma holding_next_thI:

  3083   assumes "holding s th cs"

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

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

  3086 proof -

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

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

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

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

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

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

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

  3094     by (unfold next_th_def, auto)

  3095   from that[OF this] show ?thesis .

  3096 qed

  3097 

  3098 lemma RAG_tRAG_transfer:

  3099   assumes "vt s'"

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

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

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

  3103 proof -

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

  3105     by (unfold_locales, simp)

  3106   interpret rtree: rtree "RAG s'"

  3107   proof

  3108   show "single_valued (RAG s')"

  3109   apply (intro_locales)

  3110     by (unfold single_valued_def, 

  3111         auto intro:vt_s'.unique_RAG)

  3112 

  3113   show "acyclic (RAG s')"

  3114      by (rule vt_s'.acyclic_RAG)

  3115   qed

  3116   { fix n1 n2

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

  3118     from this[unfolded tRAG_alt_def]

  3119     obtain th1 th2 cs' where 

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

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

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

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

  3124     from h(3) and assms(2) 

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

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

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

  3128     proof

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

  3130       hence eq_th1: "th1 = th" by simp

  3131       moreover have "th2 = th''"

  3132       proof -

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

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

  3135         show ?thesis

  3136           by (unfold single_valued_def, auto)

  3137       qed

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

  3139     next

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

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

  3142         by (unfold tRAG_alt_def, auto)

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

  3144     qed

  3145   } moreover {

  3146     fix n1 n2

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

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

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

  3150     proof

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

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

  3153       proof(rule tRAG_mono)

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

  3155       qed

  3156       ultimately show ?thesis by auto

  3157     next

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

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

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

  3161       ultimately show ?thesis 

  3162         by (unfold eq_n tRAG_alt_def, auto)

  3163     qed

  3164   } ultimately show ?thesis by auto

  3165 qed

  3166 

  3167 context valid_trace

  3168 begin

  3169 

  3170 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]

  3171 

  3173 

  3174 lemma cp_alt_def:

  3175   "cp s th =  

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

  3177 proof -

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

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

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

  3181   proof -

  3182     have "?L = ?R" 

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

  3184     thus ?thesis by simp

  3185   qed

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

  3187 qed

  3188 

  3189 lemma cp_gen_alt_def:

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

  3191     by (auto simp:cp_gen_def)

  3192 

  3193 lemma tRAG_nodeE:

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

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

  3196   using assms

  3197   by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def)

  3198 

  3199 lemma subtree_nodeE:

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

  3201   obtains th1 where "n = Th th1"

  3202 proof -

  3203   show ?thesis

  3204   proof(rule subtreeE[OF assms])

  3205     assume "n = Th th"

  3206     from that[OF this] show ?thesis .

  3207   next

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

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

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

  3211     proof(induct)

  3212       case (base y)

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

  3214     next

  3215       case (step y z)

  3216       thus ?case by auto

  3217     qed

  3218     with that show ?thesis by auto

  3219   qed

  3220 qed

  3221 

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

  3223 proof -

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

  3225     by (rule rtrancl_mono, auto simp:RAG_split)

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

  3227     by (rule rtrancl_mono, auto)

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

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

  3230 qed

  3231 

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

  3233 proof -

  3234   { fix a

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

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

  3237     with tRAG_star_RAG[of s]

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

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

  3240   } thus ?thesis by auto

  3241 qed

  3242 

  3243 lemma tRAG_trancl_eq:

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

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

  3246    (is "?L = ?R")

  3247 proof -

  3248   { fix th'

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

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

  3251     from tranclD[OF this]

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

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

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

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

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

  3257   } moreover 

  3258   { fix th'

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

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

  3261     from plus_rpath[OF this]

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

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

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

  3265       case (1 xs th' th)

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

  3267       show ?case

  3268       proof(cases "xs1")

  3269         case Nil

  3270         from 1(2)[unfolded Cons1 Nil]

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

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

  3273         then obtain cs where "x1 = Cs cs" 

  3274               by (unfold s_RAG_def, auto)

  3275         from rpath_nnl_lastE[OF rp[unfolded this]]

  3276         show ?thesis by auto

  3277       next

  3278         case (Cons x2 xs2)

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

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

  3281         from rpath_edges_on[OF this]

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

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

  3284             by (simp add: edges_on_unfold)

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

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

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

  3288             by (simp add: edges_on_unfold)

  3289         from this eds

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

  3291         from this[unfolded eq_x1] 

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

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

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

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

  3296            by  (elim rpath_ConsE, simp)

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

  3298         show ?thesis

  3299         proof(cases "xs2 = []")

  3300           case True

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

  3302           have "th1 = th" by auto

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

  3304         next

  3305           case False

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

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

  3308           with rt1 show ?thesis by auto

  3309         qed

  3310       qed

  3311     qed

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

  3313   } ultimately show ?thesis by blast

  3314 qed

  3315 

  3316 lemma tRAG_trancl_eq_Th:

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

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

  3319     using tRAG_trancl_eq by auto

  3320 

  3321 lemma dependants_alt_def:

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

  3323   by (metis eq_RAG s_dependants_def tRAG_trancl_eq)

  3324   

  3325 context valid_trace

  3326 begin

  3327 

  3328 lemma count_eq_tRAG_plus:

  3329   assumes "cntP s th = cntV s th"

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

  3331   using assms count_eq_dependants dependants_alt_def eq_dependants by auto 

  3332 

  3333 lemma count_eq_RAG_plus:

  3334   assumes "cntP s th = cntV s th"

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

  3336   using assms count_eq_dependants cs_dependants_def eq_RAG by auto

  3337 

  3338 lemma count_eq_RAG_plus_Th:

  3339   assumes "cntP s th = cntV s th"

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

  3341   using count_eq_RAG_plus[OF assms] by auto

  3342 

  3343 lemma count_eq_tRAG_plus_Th:

  3344   assumes "cntP s th = cntV s th"

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

  3346    using count_eq_tRAG_plus[OF assms] by auto

  3347 

  3348 end

  3349 

  3350 lemma tRAG_subtree_eq: 

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

  3352    (is "?L = ?R")

  3353 proof -

  3354   { fix n 

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

  3356     hence "n \<in> ?R"

  3357     by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) 

  3358   } moreover {

  3359     fix n

  3360     assume "n \<in> ?R"

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

  3362       by (auto simp:subtree_def)

  3363     from rtranclD[OF this(2)]

  3364     have "n \<in> ?L"

  3365     proof

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

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

  3368       thus ?thesis using subtree_def tRAG_trancl_eq by fastforce

  3369     qed (insert h, auto simp:subtree_def)

  3370   } ultimately show ?thesis by auto

  3371 qed

  3372 

  3373 lemma threads_set_eq: 

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

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

  3376    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)

  3377 

  3378 lemma cp_alt_def1: 

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

  3380 proof -

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

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

  3383        by auto

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

  3385 qed

  3386 

  3387 lemma cp_gen_def_cond: 

  3388   assumes "x = Th th"

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

  3390 by (unfold cp_alt_def1 cp_gen_def, simp)

  3391 

  3392 lemma cp_gen_over_set:

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

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

  3395 proof(rule f_image_eq)

  3396   fix a

  3397   assume "a \<in> A"

  3398   from assms[rule_format, OF this]

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

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

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

  3402 qed

  3403 

  3404 

  3405 context valid_trace

  3406 begin

  3407 

  3408 lemma RAG_threads:

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

  3410   shows "th \<in> threads s"

  3411   using assms

  3412   by (metis Field_def UnE dm_RAG_threads range_in vt)

  3413 

  3414 lemma subtree_tRAG_thread:

  3415   assumes "th \<in> threads s"

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

  3417 proof -

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

  3419     by (unfold tRAG_subtree_eq, simp)

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

  3421   proof

  3422     fix x

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

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

  3425     from this(2)

  3426     show "x \<in> ?R"

  3427     proof(cases rule:subtreeE)

  3428       case 1

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

  3430     next

  3431       case 2

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

  3433     qed

  3434   qed

  3435   finally show ?thesis .

  3436 qed

  3437 

  3438 lemma readys_root:

  3439   assumes "th \<in> readys s"

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

  3441 proof -

  3442   { fix x

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

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

  3445     from tranclD[OF this]

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

  3447     with assms(1) have False

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

  3449          by (fold wq_def, blast)

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

  3451 qed

  3452 

  3453 lemma readys_in_no_subtree:

  3454   assumes "th \<in> readys s"

  3455   and "th' \<noteq> th"

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

  3457 proof

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

  3459    thus False

  3460    proof(cases rule:subtreeE)

  3461       case 1

  3462       with assms show ?thesis by auto

  3463    next

  3464       case 2

  3465       with readys_root[OF assms(1)]

  3466       show ?thesis by (auto simp:root_def)

  3467    qed

  3468 qed

  3469 

  3470 lemma not_in_thread_isolated:

  3471   assumes "th \<notin> threads s"

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

  3473 proof

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

  3475   with dm_RAG_threads and range_in assms

  3476   show False by (unfold Field_def, blast)

  3477 qed

  3478 

  3479 lemma wf_RAG: "wf (RAG s)"

  3480 proof(rule finite_acyclic_wf)

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

  3482 next

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

  3484 qed

  3485 

  3486 lemma sgv_wRAG: "single_valued (wRAG s)"

  3487   using waiting_unique

  3488   by (unfold single_valued_def wRAG_def, auto)

  3489 

  3490 lemma sgv_hRAG: "single_valued (hRAG s)"

  3491   using holding_unique 

  3492   by (unfold single_valued_def hRAG_def, auto)

  3493 

  3494 lemma sgv_tRAG: "single_valued (tRAG s)"

  3495   by (unfold tRAG_def, rule single_valued_relcomp, 

  3496               insert sgv_wRAG sgv_hRAG, auto)

  3497 

  3498 lemma acyclic_tRAG: "acyclic (tRAG s)"

  3499 proof(unfold tRAG_def, rule acyclic_compose)

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

  3501 next

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

  3503 next

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

  3505 qed

  3506 

  3507 lemma sgv_RAG: "single_valued (RAG s)"

  3508   using unique_RAG by (auto simp:single_valued_def)

  3509 

  3510 lemma rtree_RAG: "rtree (RAG s)"

  3511   using sgv_RAG acyclic_RAG

  3512   by (unfold rtree_def rtree_axioms_def sgv_def, auto)

  3513 

  3514 end

  3515 

  3516 sublocale valid_trace < rtree_RAG: rtree "RAG s"

  3517 proof

  3518   show "single_valued (RAG s)"

  3519   apply (intro_locales)

  3520     by (unfold single_valued_def, 

  3521         auto intro:unique_RAG)

  3522 

  3523   show "acyclic (RAG s)"

  3524      by (rule acyclic_RAG)

  3525 qed

  3526 

  3527 sublocale valid_trace < rtree_s: rtree "tRAG s"

  3528 proof(unfold_locales)

  3529   from sgv_tRAG show "single_valued (tRAG s)" .

  3530 next

  3531   from acyclic_tRAG show "acyclic (tRAG s)" .

  3532 qed

  3533 

  3534 sublocale valid_trace < fsbtRAGs : fsubtree "RAG s"

  3535 proof -

  3536   show "fsubtree (RAG s)"

  3537   proof(intro_locales)

  3538     show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .

  3539   next

  3540     show "fsubtree_axioms (RAG s)"

  3541     proof(unfold fsubtree_axioms_def)

  3542       from wf_RAG show "wf (RAG s)" .

  3543     qed

  3544   qed

  3545 qed

  3546 

  3547 sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"

  3548 proof -

  3549   have "fsubtree (tRAG s)"

  3550   proof -

  3551     have "fbranch (tRAG s)"

  3552     proof(unfold tRAG_def, rule fbranch_compose)

  3553         show "fbranch (wRAG s)"

  3554         proof(rule finite_fbranchI)

  3555            from finite_RAG show "finite (wRAG s)"

  3556            by (unfold RAG_split, auto)

  3557         qed

  3558     next

  3559         show "fbranch (hRAG s)"

  3560         proof(rule finite_fbranchI)

  3561            from finite_RAG 

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

  3563         qed

  3564     qed

  3565     moreover have "wf (tRAG s)"

  3566     proof(rule wf_subset)

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

  3568         by (fold wf_comp_self, simp)

  3569     next

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

  3571         by (unfold tRAG_alt_def, auto)

  3572     qed

  3573     ultimately show ?thesis

  3574       by (unfold fsubtree_def fsubtree_axioms_def,auto)

  3575   qed

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

  3577 qed

  3578 

  3579 lemma Max_UNION: 

  3580   assumes "finite A"

  3581   and "A \<noteq> {}"

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

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

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

  3585   using assms[simp]

  3586 proof -

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

  3588     by (fold Union_image_eq, simp)

  3589   also have "... = ?R"

  3590     by (subst Max_Union, simp+)

  3591   finally show ?thesis .

  3592 qed

  3593 

  3594 lemma max_Max_eq:

  3595   assumes "finite A"

  3596     and "A \<noteq> {}"

  3597     and "x = y"

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

  3599 proof -

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

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

  3602       by (subst Max.insert, simp+)

  3603   finally show ?thesis by simp

  3604 qed

  3605 

  3606 context valid_trace

  3607 begin

  3608 

  3609 (* ddd *)

  3610 lemma cp_gen_rec:

  3611   assumes "x = Th th"

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

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

  3614   case True

  3615   show ?thesis

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

  3617 next

  3618   case False

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

  3620   note fsbttRAGs.finite_subtree[simp]

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

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

  3623             rule children_subtree)

  3624   { fix r x

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

  3626   } note this[simp]

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

  3628   proof -

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

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

  3631     ultimately show ?thesis by blast

  3632   qed

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

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

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

  3636                      (is "?L = ?R")

  3637   proof -

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

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

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

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

  3642     proof -

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

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

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

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

  3647         by (subst Max_UNION, simp+)

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

  3649           by (unfold image_comp cp_gen_alt_def, simp)

  3650       finally show ?thesis .

  3651     qed

  3652     show ?thesis

  3653     proof -

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

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

  3656             by (subst Max_Un, simp+)

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

  3658         by (unfold eq_Max_L1, simp)

  3659       also have "... =?R"

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

  3661       finally show ?thesis .

  3662     qed

  3663   qed  thus ?thesis 

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

  3665 qed

  3666 

  3667 lemma cp_rec:

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

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

  3670 proof -

  3671   have "Th th = Th th" by simp

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

  3673   show ?thesis 

  3674   proof -

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

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

  3677     proof(rule cp_gen_over_set)

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

  3679         by (unfold tRAG_alt_def, auto simp:children_def)

  3680     qed

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

  3682   qed

  3683 qed

  3684 

  3685 end

  3686 

  3687 (* keep *)

  3688 lemma next_th_holding:

  3689   assumes vt: "vt s"

  3690   and nxt: "next_th s th cs th'"

  3691   shows "holding (wq s) th cs"

  3692 proof -

  3693   from nxt[unfolded next_th_def]

  3694   obtain rest where h: "wq s cs = th # rest"

  3695                        "rest \<noteq> []" 

  3696                        "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto

  3697   thus ?thesis

  3698     by (unfold cs_holding_def, auto)

  3699 qed

  3700 

  3701 context valid_trace

  3702 begin

  3703 

  3704 lemma next_th_waiting:

  3705   assumes nxt: "next_th s th cs th'"

  3706   shows "waiting (wq s) th' cs"

  3707 proof -

  3708   from nxt[unfolded next_th_def]

  3709   obtain rest where h: "wq s cs = th # rest"

  3710                        "rest \<noteq> []" 

  3711                        "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto

  3712   from wq_distinct[of cs, unfolded h]

  3713   have dst: "distinct (th # rest)" .

  3714   have in_rest: "th' \<in> set rest"

  3715   proof(unfold h, rule someI2)

  3716     show "distinct rest \<and> set rest = set rest" using dst by auto

  3717   next

  3718     fix x assume "distinct x \<and> set x = set rest"

  3719     with h(2)

  3720     show "hd x \<in> set (rest)" by (cases x, auto)

  3721   qed

  3722   hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)

  3723   moreover have "th' \<noteq> hd (wq s cs)"

  3724     by (unfold h(1), insert in_rest dst, auto)

  3725   ultimately show ?thesis by (auto simp:cs_waiting_def)

  3726 qed

  3727 

  3728 lemma next_th_RAG:

  3729   assumes nxt: "next_th (s::event list) th cs th'"

  3730   shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"

  3731   using vt assms next_th_holding next_th_waiting

  3732   by (unfold s_RAG_def, simp)

  3733 

  3734 end

  3735 

  3736 -- {* A useless definition *}

  3737 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"

  3738 where "cps s = {(th, cp s th) | th . th \<in> threads s}"

  3739 

  3740 end