4 

     5 lemma f_image_eq:

     6   assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"

     7   shows "f ` A = g ` A"

     8 proof

     9   show "f ` A \<subseteq> g ` A"

    10     by(rule image_subsetI, auto intro:h)

    11 next

    12   show "g ` A \<subseteq> f ` A"

    13    by (rule image_subsetI, auto intro:h[symmetric])

    14 qed

    59 

    60 lemma Max_UNION: 

    61   assumes "finite A"

    62   and "A \<noteq> {}"

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

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

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

    66   using assms[simp]

    67 proof -

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

    69     by (fold Union_image_eq, simp)

    70   also have "... = ?R"

    71     by (subst Max_Union, simp+)

    72   finally show ?thesis .

    73 qed

    74 

    75 lemma max_Max_eq:

    76   assumes "finite A"

    77     and "A \<noteq> {}"

    78     and "x = y"

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

    80 proof -

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

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

    83       by (subst Max.insert, simp+)

    84   finally show ?thesis by simp

    85 qed

    86 

    87 lemma birth_time_lt:  

    88   assumes "s \<noteq> []"

    89   shows "last_set th s < length s"

    90   using assms

    91 proof(induct s)

    92   case (Cons a s)

    93   show ?case

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

    95     case False

    96     thus ?thesis

    97       by (cases a, auto)

    98   next

    99     case True

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

   101       by (cases a, auto)

   102   qed

   103 qed simp

   104 

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

   106   by (induct s, auto)

   107 

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

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

  1540 lemma RAG_threads:

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

  1542   shows "th \<in> threads s"

  1543   using assms

  1544   by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)

  1545 

  2170 lemma tRAG_alt_def: 

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

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

  2173  by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)

  2174 

  2175 sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"

  2176 proof -

  2177   have "fsubtree (tRAG s)"

  2178   proof -

  2179     have "fbranch (tRAG s)"

  2180     proof(unfold tRAG_def, rule fbranch_compose)

  2181         show "fbranch (wRAG s)"

  2182         proof(rule finite_fbranchI)

  2183            from finite_RAG show "finite (wRAG s)"

  2184            by (unfold RAG_split, auto)

  2185         qed

  2186     next

  2187         show "fbranch (hRAG s)"

  2188         proof(rule finite_fbranchI)

  2189            from finite_RAG 

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

  2191         qed

  2192     qed

  2193     moreover have "wf (tRAG s)"

  2194     proof(rule wf_subset)

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

  2196         by (fold wf_comp_self, simp)

  2197     next

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

  2199         by (unfold tRAG_alt_def, auto)

  2200     qed

  2201     ultimately show ?thesis

  2202       by (unfold fsubtree_def fsubtree_axioms_def,auto)

  2203   qed

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

  2205 qed

  2206 

  2207 

  3739   from rp1 rp2

  3776 lemma card_runing: "card (runing s) \<le> 1"

  3777 proof(cases "runing s = {}")

  3778   case True

  3779   thus ?thesis by auto

  3780 next

  3781   case False

  3782   then obtain th where [simp]: "th \<in> runing s" by auto

  3783   from runing_unique[OF this]

  3784   have "runing s = {th}" by auto

  3785   thus ?thesis by auto

  3786 qed

  3787 

  3788 lemma create_pre:

  3789   assumes stp: "step s e"

  3790   and not_in: "th \<notin> threads s"

  3791   and is_in: "th \<in> threads (e#s)"

  3792   obtains prio where "e = Create th prio"

  3793 proof -

  3794   from assms  

  3795   show ?thesis

  3796   proof(cases)

  3797     case (thread_create thread prio)

  3798     with is_in not_in have "e = Create th prio" by simp

  3799     from that[OF this] show ?thesis .

  3800   next

  3801     case (thread_exit thread)

  3802     with assms show ?thesis by (auto intro!:that)

  3803   next

  3804     case (thread_P thread)

  3805     with assms show ?thesis by (auto intro!:that)

  3806   next

  3807     case (thread_V thread)

  3808     with assms show ?thesis by (auto intro!:that)

  3809   next 

  3810     case (thread_set thread)

  3811     with assms show ?thesis by (auto intro!:that)

  3812   qed

  3813 qed

  3814 

  3815 lemma eq_pv_children:

  3816   assumes eq_pv: "cntP s th = cntV s th"

  3817   shows "children (RAG s) (Th th) = {}"

  3818 proof -

  3819     from cnp_cnv_cncs and eq_pv

  3820     have "cntCS s th = 0" 

  3821       by (auto split:if_splits)

  3822     from this[unfolded cntCS_def holdents_alt_def]

  3823     have card_0: "card (the_cs ` children (RAG s) (Th th)) = 0" .

  3824     have "finite (the_cs ` children (RAG s) (Th th))"

  3825       by (simp add: fsbtRAGs.finite_children)

  3826     from card_0[unfolded card_0_eq[OF this]]

  3827     show ?thesis by auto

  3828 qed

  3829 

  3830 lemma eq_pv_holdents:

  3831   assumes eq_pv: "cntP s th = cntV s th"

  3832   shows "holdents s th = {}"

  3833   by (unfold holdents_alt_def eq_pv_children[OF assms], simp)

  3834 

  3835 lemma eq_pv_subtree:

  3836   assumes eq_pv: "cntP s th = cntV s th"

  3837   shows "subtree (RAG s) (Th th) = {Th th}"

  3838   using eq_pv_children[OF assms]

  3839     by (unfold subtree_children, simp)

  3840 

  4009 lemma eq_dependants: "dependants (wq s) = dependants s"

  4010   by (simp add: s_dependants_abv wq_def)

  4011 

  4012 context valid_trace

  4013 begin

  4014 

  4015 lemma count_eq_tRAG_plus:

  4016   assumes "cntP s th = cntV s th"

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

  4018   using assms eq_pv_dependants dependants_alt_def eq_dependants by auto 

  4019 

  4020 lemma count_eq_RAG_plus_Th:

  4021   assumes "cntP s th = cntV s th"

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

  4023   using count_eq_RAG_plus[OF assms] by auto

  4024 

  4025 lemma count_eq_tRAG_plus_Th:

  4026   assumes "cntP s th = cntV s th"

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

  4028    using count_eq_tRAG_plus[OF assms] by auto

  4029 end

  4030 

  4031 lemma inj_the_preced: 

  4032   "inj_on (the_preced s) (threads s)"

  4033   by (metis inj_onI preced_unique the_preced_def)

  4034 

  4035 lemma tRAG_Field:

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

  4037   by (unfold tRAG_alt_def Field_def, auto)

  4038 

  4039 lemma tRAG_ancestorsE:

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

  4041   obtains th where "x = Th th"

  4042 proof -

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

  4044       by (unfold ancestors_def, auto)

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

  4046   then obtain th where "x = Th th"

  4047     by (unfold tRAG_alt_def, auto)

  4048   from that[OF this] show ?thesis .

  4049 qed

  4050 

  4051 lemma tRAG_mono:

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

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

  4054   using assms 

  4055   by (unfold tRAG_alt_def, auto)

  4056 

  4057 lemma holding_next_thI:

  4058   assumes "holding s th cs"

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

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

  4061 proof -

  4062   from assms(1)[folded holding_eq, unfolded cs_holding_def]

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

  4064     by (unfold s_holding_def, fold wq_def, auto)

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

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

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

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

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

  4070     by (unfold next_th_def, auto)

  4071   from that[OF this] show ?thesis .

  4072 qed

  4073 

  4074 lemma RAG_tRAG_transfer:

  4075   assumes "vt s'"

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

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

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

  4079 proof -

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

  4081     by (unfold_locales, simp)

  4082   { fix n1 n2

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

  4084     from this[unfolded tRAG_alt_def]

  4085     obtain th1 th2 cs' where 

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

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

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

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

  4090     from h(3) and assms(2) 

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

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

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

  4094     proof

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

  4096       hence eq_th1: "th1 = th" by simp

  4097       moreover have "th2 = th''"

  4098       proof -

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

  4100         from assms(3) cs_in[unfolded this]

  4101         show ?thesis using vt_s'.unique_RAG by auto 

  4102       qed

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

  4104     next

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

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

  4107         by (unfold tRAG_alt_def, auto)

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

  4109     qed

  4110   } moreover {

  4111     fix n1 n2

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

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

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

  4115     proof

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

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

  4118       proof(rule tRAG_mono)

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

  4120       qed

  4121       ultimately show ?thesis by auto

  4122     next

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

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

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

  4126       ultimately show ?thesis 

  4127         by (unfold eq_n tRAG_alt_def, auto)

  4128     qed

  4129   } ultimately show ?thesis by auto

  4130 qed

  4131 

  4132 context valid_trace

  4133 begin

  4134 

  4135 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]

  4136 

  4137 end

  4138 

  4139 lemma tRAG_subtree_eq: 

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

  4141    (is "?L = ?R")

  4142 proof -

  4143   { fix n 

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

  4145     hence "n \<in> ?R"

  4146     by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) 

  4147   } moreover {

  4148     fix n

  4149     assume "n \<in> ?R"

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

  4151       by (auto simp:subtree_def)

  4152     from rtranclD[OF this(2)]

  4153     have "n \<in> ?L"

  4154     proof

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

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

  4157       thus ?thesis using subtree_def tRAG_trancl_eq by fastforce

  4158     qed (insert h, auto simp:subtree_def)

  4159   } ultimately show ?thesis by auto

  4160 qed

  4161 

  4162 lemma threads_set_eq: 

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

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

  4165    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)

  4166 

  4167 lemma cp_alt_def1: 

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

  4169 proof -

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

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

  4172        by auto

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

  4174 qed

  4175 

  4176 lemma cp_gen_def_cond: 

  4177   assumes "x = Th th"

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

  4179 by (unfold cp_alt_def1 cp_gen_def, simp)

  4180 

  4181 lemma cp_gen_over_set:

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

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

  4184 proof(rule f_image_eq)

  4185   fix a

  4186   assume "a \<in> A"

  4187   from assms[rule_format, OF this]

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

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

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

  4191 qed

  4192 

  4193 context valid_trace

  4194 begin

  4195 

  4196 lemma subtree_tRAG_thread:

  4197   assumes "th \<in> threads s"

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

  4199 proof -

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

  4201     by (unfold tRAG_subtree_eq, simp)

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

  4203   proof

  4204     fix x

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

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

  4207     from this(2)

  4208     show "x \<in> ?R"

  4209     proof(cases rule:subtreeE)

  4210       case 1

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

  4212     next

  4213       case 2

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

  4215     qed

  4216   qed

  4217   finally show ?thesis .

  4218 qed

  4219 

  4220 lemma readys_root:

  4221   assumes "th \<in> readys s"

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

  4223 proof -

  4224   { fix x

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

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

  4227     from tranclD[OF this]

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

  4229     with assms(1) have False

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

  4231          by (fold wq_def, blast)

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

  4233 qed

  4234 

  4235 lemma readys_in_no_subtree:

  4236   assumes "th \<in> readys s"

  4237   and "th' \<noteq> th"

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

  4239 proof

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

  4241    thus False

  4242    proof(cases rule:subtreeE)

  4243       case 1

  4244       with assms show ?thesis by auto

  4245    next

  4246       case 2

  4247       with readys_root[OF assms(1)]

  4248       show ?thesis by (auto simp:root_def)

  4249    qed

  4250 qed

  4251 

  4252 lemma not_in_thread_isolated:

  4253   assumes "th \<notin> threads s"

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

  4255 proof

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

  4257   with dm_RAG_threads and rg_RAG_threads assms

  4258   show False by (unfold Field_def, blast)

  4259 qed

  4260 

  4261 end

  4262 

  4263 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"

  4264   where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"

  4265 

  4266 

  4267 lemma detached_test:

  4268   shows "detached s th = (Th th \<notin> Field (RAG s))"

  4269 apply(simp add: detached_def Field_def)

  4270 apply(simp add: s_RAG_def)

  4271 apply(simp add: s_holding_abv s_waiting_abv)

  4272 apply(simp add: Domain_iff Range_iff)

  4273 apply(simp add: wq_def)

  4274 apply(auto)

  4275 done

  4276 

  4277 context valid_trace

  4278 begin

  4279 

  4280 lemma detached_intro:

  4281   assumes eq_pv: "cntP s th = cntV s th"

  4282   shows "detached s th"

  4283 proof -

  4284   from eq_pv cnp_cnv_cncs

  4285   have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:pvD_def)

  4286   thus ?thesis

  4287   proof

  4288     assume "th \<notin> threads s"

  4289     with rg_RAG_threads dm_RAG_threads

  4290     show ?thesis

  4291       by (auto simp add: detached_def s_RAG_def s_waiting_abv 

  4292               s_holding_abv wq_def Domain_iff Range_iff)

  4293   next

  4294     assume "th \<in> readys s"

  4295     moreover have "Th th \<notin> Range (RAG s)"

  4296     proof -

  4297       from eq_pv_children[OF assms]

  4298       have "children (RAG s) (Th th) = {}" .

  4299       thus ?thesis

  4300       by (unfold children_def, auto)

  4301     qed

  4302     ultimately show ?thesis

  4303       by (auto simp add: detached_def s_RAG_def s_waiting_abv 

  4304               s_holding_abv wq_def readys_def)

  4305   qed

  4306 qed

  4307 

  4308 lemma detached_elim:

  4309   assumes dtc: "detached s th"

  4310   shows "cntP s th = cntV s th"

  4311 proof -

  4312   have cncs_z: "cntCS s th = 0"

  4313   proof -

  4314     from dtc have "holdents s th = {}"

  4315       unfolding detached_def holdents_test s_RAG_def

  4316       by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff)

  4317     thus ?thesis by (auto simp:cntCS_def)

  4318   qed

  4319   show ?thesis

  4320   proof(cases "th \<in> threads s")

  4321     case True

  4322     with dtc 

  4323     have "th \<in> readys s"

  4324       by (unfold readys_def detached_def Field_def Domain_def Range_def, 

  4325            auto simp:waiting_eq s_RAG_def)

  4326     with cncs_z  show ?thesis using cnp_cnv_cncs by (simp add:pvD_def)

  4327   next

  4328     case False

  4329     with cncs_z and cnp_cnv_cncs show ?thesis by (simp add:pvD_def)

  4330   qed

  4331 qed

  4332 

  4333 lemma detached_eq:

  4334   shows "(detached s th) = (cntP s th = cntV s th)"

  4335   by (insert vt, auto intro:detached_intro detached_elim)

  4336 

  4337 end

  4338 

  4339 context valid_trace

  4340 begin

  4341 (* ddd *)

  4342 lemma cp_gen_rec:

  4343   assumes "x = Th th"

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

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

  4346   case True

  4347   show ?thesis

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

  4349 next

  4350   case False

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

  4352   note fsbttRAGs.finite_subtree[simp]

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

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

  4355             rule children_subtree)

  4356   { fix r x

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

  4358   } note this[simp]

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

  4360   proof -

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

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

  4363     ultimately show ?thesis by blast

  4364   qed

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

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

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

  4368                      (is "?L = ?R")

  4369   proof -

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

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

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

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

  4374     proof -

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

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

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

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

  4379         by (subst Max_UNION, simp+)

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

  4381           by (unfold image_comp cp_gen_alt_def, simp)

  4382       finally show ?thesis .

  4383     qed

  4384     show ?thesis

  4385     proof -

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

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

  4388             by (subst Max_Un, simp+)

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

  4390         by (unfold eq_Max_L1, simp)

  4391       also have "... =?R"

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

  4393       finally show ?thesis .

  4394     qed

  4395   qed  thus ?thesis 

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

  4397 qed

  4398 

  4399 lemma cp_rec:

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

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

  4402 proof -

  4403   have "Th th = Th th" by simp

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

  4405   show ?thesis 

  4406   proof -

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

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

  4409     proof(rule cp_gen_over_set)

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

  4411         by (unfold tRAG_alt_def, auto simp:children_def)

  4412     qed

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

  4414   qed

  4415 qed

  4416 

  4417 lemma next_th_holding:

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

  4419   shows "holding (wq s) th cs"

  4420 proof -

  4421   from nxt[unfolded next_th_def]

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

  4423                        "rest \<noteq> []" 

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

  4425   thus ?thesis

  4426     by (unfold cs_holding_def, auto)

  4427 qed

  4428 

  4429 lemma next_th_waiting:

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

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

  4432 proof -

  4433   from nxt[unfolded next_th_def]

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

  4435                        "rest \<noteq> []" 

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

  4437   from wq_distinct[of cs, unfolded h]

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

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

  4440   proof(unfold h, rule someI2)

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

  4442   next

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

  4444     with h(2)

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

  4446   qed

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

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

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

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

  4451 qed

  4452 

  4453 lemma next_th_RAG:

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

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

  4456   using vt assms next_th_holding next_th_waiting

  4457   by (unfold s_RAG_def, simp)

  4458 

  4459 end

  4460 

  4461 lemma next_th_unique: 

  4462   assumes nt1: "next_th s th cs th1"

  4463   and nt2: "next_th s th cs th2"

  4464   shows "th1 = th2"

  4465 using assms by (unfold next_th_def, auto)

  4466 

  4467 context valid_trace

  4468 begin

  4469 

  4470 thm th_chain_to_ready

  4471 

  4472 find_theorems subtree Th RAG

  4473 

  4474 lemma "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"

  4475     (is "?L = ?R")

  4476 proof -

  4477   { fix th1

  4478     assume "th1 \<in> ?L"

  4479     from th_chain_to_ready[OF this]

  4480     have "th1 \<in> readys s \<or> (\<exists>th'a. th'a \<in> readys s \<and> (Th th1, Th th'a) \<in> (RAG s)\<^sup>+)" .

  4481     hence "th1 \<in> ?R"

  4482     proof

  4483       assume "th1 \<in> readys s"

  4484       thus ?thesis by (auto simp:subtree_def)

  4485     next

  4486       assume "\<exists>th'a. th'a \<in> readys s \<and> (Th th1, Th th'a) \<in> (RAG s)\<^sup>+"

  4487       thus ?thesis 

  4488     qed

  4489   } moreover 

  4490   { fix th'

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

  4492     have "th' \<in> ?L" sorry

  4493   } ultimately show ?thesis by auto

  4494 qed

  4495 

  4496 lemma max_cp_readys_threads_pre: (* ccc *)

  4497   assumes np: "threads s \<noteq> {}"

  4498   shows "Max (cp s ` readys s) = Max (cp s ` threads s)"

  4499 proof(unfold max_cp_eq)

  4500   show "Max (cp s ` readys s) = Max (the_preced s ` threads s)"

  4501   proof -

  4502     let ?p = "Max (the_preced s ` threads s)" 

  4503     let ?f = "the_preced s"

  4504     have "?p \<in> (?f ` threads s)"

  4505     proof(rule Max_in)

  4506       from finite_threads show "finite (?f ` threads s)" by simp

  4507     next

  4508       from np show "?f ` threads s \<noteq> {}" by simp

  4509     qed

  4510     then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \<in> threads s"

  4511       by (auto simp:Image_def)

  4512     from th_chain_to_ready [OF tm_in]

  4513     have "tm \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+)" .

  4514     thus ?thesis

  4515     proof

  4516       assume "\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+ "

  4517       then obtain th' where th'_in: "th' \<in> readys s" 

  4518         and tm_chain:"(Th tm, Th th') \<in> (RAG s)\<^sup>+" by auto

  4519       have "cp s th' = ?f tm"

  4520       proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)

  4521         from dependants_threads finite_threads

  4522         show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))" 

  4523           by (auto intro:finite_subset)

  4524       next

  4525         fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"

  4526         from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .

  4527         moreover have "p \<le> \<dots>"

  4528         proof(rule Max_ge)

  4529           from finite_threads

  4530           show "finite ((\<lambda>th. preced th s) ` threads s)" by simp

  4531         next

  4532           from p_in and th'_in and dependants_threads[of th']

  4533           show "p \<in> (\<lambda>th. preced th s) ` threads s"

  4534             by (auto simp:readys_def)

  4535         qed

  4536         ultimately show "p \<le> preced tm s" by auto

  4537       next

  4538         show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"

  4539         proof -

  4540           from tm_chain

  4541           have "tm \<in> dependants (wq s) th'"

  4542             by (unfold cs_dependants_def s_RAG_def cs_RAG_def, auto)

  4543           thus ?thesis by auto

  4544         qed

  4545       qed

  4546       with tm_max

  4547       have h: "cp s th' = Max ((\<lambda>th. preced th s) ` threads s)" by simp

  4548       show ?thesis

  4549       proof (fold h, rule Max_eqI)

  4550         fix q 

  4551         assume "q \<in> cp s ` readys s"

  4552         then obtain th1 where th1_in: "th1 \<in> readys s"

  4553           and eq_q: "q = cp s th1" by auto

  4554         show "q \<le> cp s th'"

  4555           apply (unfold h eq_q)

  4556           apply (unfold cp_eq_cpreced cpreced_def)

  4557           apply (rule Max_mono)

  4558         proof -

  4559           from dependants_threads [of th1] th1_in

  4560           show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq> 

  4561                  (\<lambda>th. preced th s) ` threads s"

  4562             by (auto simp:readys_def)

  4563         next

  4564           show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp

  4565         next

  4566           from finite_threads 

  4567           show " finite ((\<lambda>th. preced th s) ` threads s)" by simp

  4568         qed

  4569       next

  4570         from finite_threads

  4571         show "finite (cp s ` readys s)" by (auto simp:readys_def)

  4572       next

  4573         from th'_in

  4574         show "cp s th' \<in> cp s ` readys s" by simp

  4575       qed

  4576     next

  4577       assume tm_ready: "tm \<in> readys s"

  4578       show ?thesis

  4579       proof(fold tm_max)

  4580         have cp_eq_p: "cp s tm = preced tm s"

  4581         proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)

  4582           fix y 

  4583           assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"

  4584           show "y \<le> preced tm s"

  4585           proof -

  4586             { fix y'

  4587               assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"

  4588               have "y' \<le> preced tm s"

  4589               proof(unfold tm_max, rule Max_ge)

  4590                 from hy' dependants_threads[of tm]

  4591                 show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto

  4592               next

  4593                 from finite_threads

  4594                 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp

  4595               qed

  4596             } with hy show ?thesis by auto

  4597           qed

  4598         next

  4599           from dependants_threads[of tm] finite_threads

  4600           show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"

  4601             by (auto intro:finite_subset)

  4602         next

  4603           show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"

  4604             by simp

  4605         qed 

  4606         moreover have "Max (cp s ` readys s) = cp s tm"

  4607         proof(rule Max_eqI)

  4608           from tm_ready show "cp s tm \<in> cp s ` readys s" by simp

  4609         next

  4610           from finite_threads

  4611           show "finite (cp s ` readys s)" by (auto simp:readys_def)

  4612         next

  4613           fix y assume "y \<in> cp s ` readys s"

  4614           then obtain th1 where th1_readys: "th1 \<in> readys s"

  4615             and h: "y = cp s th1" by auto

  4616           show "y \<le> cp s tm"

  4617             apply(unfold cp_eq_p h)

  4618             apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono)

  4619           proof -

  4620             from finite_threads

  4621             show "finite ((\<lambda>th. preced th s) ` threads s)" by simp

  4622           next

  4623             show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"

  4624               by simp

  4625           next

  4626             from dependants_threads[of th1] th1_readys

  4627             show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) 

  4628                     \<subseteq> (\<lambda>th. preced th s) ` threads s"

  4629               by (auto simp:readys_def)

  4630           qed

  4631         qed

  4632         ultimately show " Max (cp s ` readys s) = preced tm s" by simp

  4633       qed 

  4634     qed

  4635   qed

  4636 qed

  4637 

  4638 text {* (* ccc *) \noindent

  4639   Since the current precedence of the threads in ready queue will always be boosted,

  4640   there must be one inside it has the maximum precedence of the whole system. 

  4641 *}

  4642 lemma max_cp_readys_threads:

  4643   shows "Max (cp s ` readys s) = Max (cp s ` threads s)"

  4644 proof(cases "threads s = {}")

  4645   case True

  4646   thus ?thesis 

  4647     by (auto simp:readys_def)

  4648 next

  4649   case False

  4650   show ?thesis by (rule max_cp_readys_threads_pre[OF False])

  4651 qed

  4652 

  4653 end