1 theory CpsG

     2 imports PrioG 

     3 begin

     4 

     5 lemma not_thread_holdents:

     6   fixes th s

     7   assumes vt: "vt step s"

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

     9   shows "holdents s th = {}"

    10 proof -

    11   from vt not_in show ?thesis

    12   proof(induct arbitrary:th)

    13     case (vt_cons s e th)

    14     assume vt: "vt step s"

    15       and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"

    16       and stp: "step s e"

    17       and not_in: "th \<notin> threads (e # s)"

    18     from stp show ?case

    19     proof(cases)

    20       case (thread_create thread prio)

    21       assume eq_e: "e = Create thread prio"

    22         and not_in': "thread \<notin> threads s"

    23       have "holdents (e # s) th = holdents s th"

    24         apply (unfold eq_e holdents_def)

    25         by (simp add:depend_create_unchanged)

    26       moreover have "th \<notin> threads s" 

    27       proof -

    28         from not_in eq_e show ?thesis by simp

    29       qed

    30       moreover note ih ultimately show ?thesis by auto

    31     next

    32       case (thread_exit thread)

    33       assume eq_e: "e = Exit thread"

    34       and nh: "holdents s thread = {}"

    35       show ?thesis

    36       proof(cases "th = thread")

    37         case True

    38         with nh eq_e

    39         show ?thesis 

    40           by (auto simp:holdents_def depend_exit_unchanged)

    41       next

    42         case False

    43         with not_in and eq_e

    44         have "th \<notin> threads s" by simp

    45         from ih[OF this] False eq_e show ?thesis 

    46           by (auto simp:holdents_def depend_exit_unchanged)

    47       qed

    48     next

    49       case (thread_P thread cs)

    50       assume eq_e: "e = P thread cs"

    51       and is_runing: "thread \<in> runing s"

    52       from prems have vtp: "vt step (P thread cs#s)" by auto

    53       have neq_th: "th \<noteq> thread" 

    54       proof -

    55         from not_in eq_e have "th \<notin> threads s" by simp

    56         moreover from is_runing have "thread \<in> threads s"

    57           by (simp add:runing_def readys_def)

    58         ultimately show ?thesis by auto

    59       qed

    60       hence "holdents (e # s) th  = holdents s th "

    61         apply (unfold cntCS_def holdents_def eq_e)

    62         by (unfold step_depend_p[OF vtp], auto)

    63       moreover have "holdents s th = {}"

    64       proof(rule ih)

    65         from not_in eq_e show "th \<notin> threads s" by simp

    66       qed

    67       ultimately show ?thesis by simp

    68     next

    69       case (thread_V thread cs)

    70       assume eq_e: "e = V thread cs"

    71         and is_runing: "thread \<in> runing s"

    72         and hold: "holding s thread cs"

    73       have neq_th: "th \<noteq> thread" 

    74       proof -

    75         from not_in eq_e have "th \<notin> threads s" by simp

    76         moreover from is_runing have "thread \<in> threads s"

    77           by (simp add:runing_def readys_def)

    78         ultimately show ?thesis by auto

    79       qed

    80       from prems have vtv: "vt step (V thread cs#s)" by auto

    81       from hold obtain rest 

    82         where eq_wq: "wq s cs = thread # rest"

    83         by (case_tac "wq s cs", auto simp:s_holding_def)

    84       from not_in eq_e eq_wq

    85       have "\<not> next_th s thread cs th"

    86         apply (auto simp:next_th_def)

    87       proof -

    88         assume ne: "rest \<noteq> []"

    89           and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")

    90         have "?t \<in> set rest"

    91         proof(rule someI2)

    92           from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq

    93           show "distinct rest \<and> set rest = set rest" by auto

    94         next

    95           fix x assume "distinct x \<and> set x = set rest" with ne

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

    97         qed

    98         with eq_wq have "?t \<in> set (wq s cs)" by simp

    99         from wq_threads[OF step_back_vt[OF vtv], OF this] and ni

   100         show False by auto

   101       qed

   102       moreover note neq_th eq_wq

   103       ultimately have "holdents (e # s) th  = holdents s th"

   104         by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)

   105       moreover have "holdents s th = {}"

   106       proof(rule ih)

   107         from not_in eq_e show "th \<notin> threads s" by simp

   108       qed

   109       ultimately show ?thesis by simp

   110     next

   111       case (thread_set thread prio)

   112       print_facts

   113       assume eq_e: "e = Set thread prio"

   114         and is_runing: "thread \<in> runing s"

   115       from not_in and eq_e have "th \<notin> threads s" by auto

   116       from ih [OF this] and eq_e

   117       show ?thesis 

   118         apply (unfold eq_e cntCS_def holdents_def)

   119         by (simp add:depend_set_unchanged)

   120     qed

   121     next

   122       case vt_nil

   123       show ?case

   124       by (auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)

   125   qed

   126 qed

   127 

   128 

   129 

   130 lemma next_th_neq: 

   131   assumes vt: "vt step s"

   132   and nt: "next_th s th cs th'"

   133   shows "th' \<noteq> th"

   134 proof -

   135   from nt show ?thesis

   136     apply (auto simp:next_th_def)

   137   proof -

   138     fix rest

   139     assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"

   140       and ne: "rest \<noteq> []"

   141     have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" 

   142     proof(rule someI2)

   143       from wq_distinct[OF vt, of cs] eq_wq

   144       show "distinct rest \<and> set rest = set rest" by auto

   145     next

   146       fix x

   147       assume "distinct x \<and> set x = set rest"

   148       hence eq_set: "set x = set rest" by auto

   149       with ne have "x \<noteq> []" by auto

   150       hence "hd x \<in> set x" by auto

   151       with eq_set show "hd x \<in> set rest" by auto

   152     qed

   153     with wq_distinct[OF vt, of cs] eq_wq show False by auto

   154   qed

   155 qed

   156 

   157 lemma next_th_unique: 

   158   assumes nt1: "next_th s th cs th1"

   159   and nt2: "next_th s th cs th2"

   160   shows "th1 = th2"

   161 proof -

   162   from assms show ?thesis

   163     by (unfold next_th_def, auto)

   164 qed

   165 

   166 lemma pp_sub: "(r^+)^+ \<subseteq> r^+"

   167   by auto

   168 

   169 lemma wf_depend:

   170   assumes vt: "vt step s"

   171   shows "wf (depend s)"

   172 proof(rule finite_acyclic_wf)

   173   from finite_depend[OF vt] show "finite (depend s)" .

   174 next

   175   from acyclic_depend[OF vt] show "acyclic (depend s)" .

   176 qed

   177 

   178 lemma Max_Union:

   179   assumes fc: "finite C"

   180   and ne: "C \<noteq> {}"

   181   and fa: "\<And> A. A \<in> C \<Longrightarrow> finite A \<and> A \<noteq> {}"

   182   shows "Max (\<Union> C) = Max (Max ` C)"

   183 proof -

   184   from fc ne fa show ?thesis

   185   proof(induct)

   186     case (insert x F)

   187     assume ih: "\<lbrakk>F \<noteq> {}; \<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}\<rbrakk> \<Longrightarrow> Max (\<Union>F) = Max (Max ` F)"

   188     and h: "\<And> A. A \<in> insert x F \<Longrightarrow> finite A \<and> A \<noteq> {}"

   189     show ?case (is "?L = ?R")

   190     proof(cases "F = {}")

   191       case False

   192       from Union_insert have "?L = Max (x \<union> (\<Union> F))" by simp

   193       also have "\<dots> = max (Max x) (Max(\<Union> F))"

   194       proof(rule Max_Un)

   195         from h[of x] show "finite x" by auto

   196       next

   197         from h[of x] show "x \<noteq> {}" by auto

   198       next

   199         show "finite (\<Union>F)"

   200         proof(rule finite_Union)

   201           show "finite F" by fact

   202         next

   203           from h show "\<And>M. M \<in> F \<Longrightarrow> finite M" by auto

   204         qed

   205       next

   206         from False and h show "\<Union>F \<noteq> {}" by auto

   207       qed

   208       also have "\<dots> = ?R"

   209       proof -

   210         have "?R = Max (Max ` ({x} \<union> F))" by simp

   211         also have "\<dots> = Max ({Max x} \<union> (Max ` F))" by simp

   212         also have "\<dots> = max (Max x) (Max (\<Union>F))"

   213         proof -

   214           have "Max ({Max x} \<union> Max ` F) = max (Max {Max x}) (Max (Max ` F))"

   215           proof(rule Max_Un)

   216             show "finite {Max x}" by simp

   217           next

   218             show "{Max x} \<noteq> {}" by simp

   219           next

   220             from insert show "finite (Max ` F)" by auto

   221           next

   222             from False show "Max ` F \<noteq> {}" by auto

   223           qed

   224           moreover have "Max {Max x} = Max x" by simp

   225           moreover have "Max (\<Union>F) = Max (Max ` F)"

   226           proof(rule ih)

   227             show "F \<noteq> {}" by fact

   228           next

   229             from h show "\<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}"

   230               by auto

   231           qed

   232           ultimately show ?thesis by auto

   233         qed

   234         finally show ?thesis by simp

   235       qed

   236       finally show ?thesis by simp

   237     next

   238       case True

   239       thus ?thesis by auto

   240     qed

   241   next

   242     case empty

   243     assume "{} \<noteq> {}" show ?case by auto

   244   qed

   245 qed

   246 

   247 definition child :: "state \<Rightarrow> (node \<times> node) set"

   248   where "child s =

   249             {(Th th', Th th) | th th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"

   250 

   251 definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"

   252   where "children s th = {th'. (Th th', Th th) \<in> child s}"

   253 

   254 

   255 lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"

   256   by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)

   257 

   258 lemma child_unique:

   259   assumes vt: "vt step s"

   260   and ch1: "(Th th, Th th1) \<in> child s"

   261   and ch2: "(Th th, Th th2) \<in> child s"

   262   shows "th1 = th2"

   263 proof -

   264   from ch1 ch2 show ?thesis

   265   proof(unfold child_def, clarsimp)

   266     fix cs csa

   267     assume h1: "(Th th, Cs cs) \<in> depend s"

   268       and h2: "(Cs cs, Th th1) \<in> depend s"

   269       and h3: "(Th th, Cs csa) \<in> depend s"

   270       and h4: "(Cs csa, Th th2) \<in> depend s"

   271     from unique_depend[OF vt h1 h3] have "cs = csa" by simp

   272     with h4 have "(Cs cs, Th th2) \<in> depend s" by simp

   273     from unique_depend[OF vt h2 this]

   274     show "th1 = th2" by simp

   275   qed 

   276 qed

   277 

   278 

   279 lemma cp_eq_cpreced_f: "cp s = cpreced s (wq s)"

   280 proof -

   281   from fun_eq_iff 

   282   have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto

   283   show ?thesis

   284   proof(rule h)

   285     from cp_eq_cpreced show "\<forall>x. cp s x = cpreced s (wq s) x" by auto

   286   qed

   287 qed

   288 

   289 lemma depend_children:

   290   assumes h: "(Th th1, Th th2) \<in> (depend s)^+"

   291   shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)^+)"

   292 proof -

   293   from h show ?thesis

   294   proof(induct rule: tranclE)

   295     fix c th2

   296     assume h1: "(Th th1, c) \<in> (depend s)\<^sup>+"

   297     and h2: "(c, Th th2) \<in> depend s"

   298     from h2 obtain cs where eq_c: "c = Cs cs"

   299       by (case_tac c, auto simp:s_depend_def)

   300     show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"

   301     proof(rule tranclE[OF h1])

   302       fix ca

   303       assume h3: "(Th th1, ca) \<in> (depend s)\<^sup>+"

   304         and h4: "(ca, c) \<in> depend s"

   305       show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"

   306       proof -

   307         from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"

   308           by (case_tac ca, auto simp:s_depend_def)

   309         from eq_ca h4 h2 eq_c

   310         have "th3 \<in> children s th2" by (auto simp:children_def child_def)

   311         moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (depend s)\<^sup>+" by simp

   312         ultimately show ?thesis by auto

   313       qed

   314     next

   315       assume "(Th th1, c) \<in> depend s"

   316       with h2 eq_c

   317       have "th1 \<in> children s th2"

   318         by (auto simp:children_def child_def)

   319       thus ?thesis by auto

   320     qed

   321   next

   322     assume "(Th th1, Th th2) \<in> depend s"

   323     thus ?thesis

   324       by (auto simp:s_depend_def)

   325   qed

   326 qed

   327 

   328 lemma sub_child: "child s \<subseteq> (depend s)^+"

   329   by (unfold child_def, auto)

   330 

   331 lemma wf_child: 

   332   assumes vt: "vt step s"

   333   shows "wf (child s)"

   334 proof(rule wf_subset)

   335   from wf_trancl[OF wf_depend[OF vt]]

   336   show "wf ((depend s)\<^sup>+)" .

   337 next

   338   from sub_child show "child s \<subseteq> (depend s)\<^sup>+" .

   339 qed

   340 

   341 lemma depend_child_pre:

   342   assumes vt: "vt step s"

   343   shows

   344   "(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")

   345 proof -

   346   from wf_trancl[OF wf_depend[OF vt]]

   347   have wf: "wf ((depend s)^+)" .

   348   show ?thesis

   349   proof(rule wf_induct[OF wf, of ?P], clarsimp)

   350     fix th'

   351     assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (depend s)\<^sup>+ \<longrightarrow>

   352                (Th th, y) \<in> (depend s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"

   353     and h: "(Th th, Th th') \<in> (depend s)\<^sup>+"

   354     show "(Th th, Th th') \<in> (child s)\<^sup>+"

   355     proof -

   356       from depend_children[OF h]

   357       have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend s)\<^sup>+)" .

   358       thus ?thesis

   359       proof

   360         assume "th \<in> children s th'"

   361         thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)

   362       next

   363         assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend s)\<^sup>+"

   364         then obtain th3 where th3_in: "th3 \<in> children s th'" 

   365           and th_dp: "(Th th, Th th3) \<in> (depend s)\<^sup>+" by auto

   366         from th3_in have "(Th th3, Th th') \<in> (depend s)^+" by (auto simp:children_def child_def)

   367         from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp

   368         with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)

   369       qed

   370     qed

   371   qed

   372 qed

   373 

   374 lemma depend_child: "\<lbrakk>vt step s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"

   375   by (insert depend_child_pre, auto)

   376 

   377 lemma child_depend_p:

   378   assumes "(n1, n2) \<in> (child s)^+"

   379   shows "(n1, n2) \<in> (depend s)^+"

   380 proof -

   381   from assms show ?thesis

   382   proof(induct)

   383     case (base y)

   384     with sub_child show ?case by auto

   385   next

   386     case (step y z)

   387     assume "(y, z) \<in> child s"

   388     with sub_child have "(y, z) \<in> (depend s)^+" by auto

   389     moreover have "(n1, y) \<in> (depend s)^+" by fact

   390     ultimately show ?case by auto

   391   qed

   392 qed

   393 

   394 lemma child_depend_eq: 

   395   assumes vt: "vt step s"

   396   shows 

   397   "((Th th1, Th th2) \<in> (child s)^+) = 

   398    ((Th th1, Th th2) \<in> (depend s)^+)"

   399   by (auto intro: depend_child[OF vt] child_depend_p)

   400 

   401 lemma children_no_dep:

   402   fixes s th th1 th2 th3

   403   assumes vt: "vt step s"

   404   and ch1: "(Th th1, Th th) \<in> child s"

   405   and ch2: "(Th th2, Th th) \<in> child s"

   406   and ch3: "(Th th1, Th th2) \<in> (depend s)^+"

   407   shows "False"

   408 proof -

   409   from depend_child[OF vt ch3]

   410   have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .

   411   thus ?thesis

   412   proof(rule converse_tranclE)

   413     thm tranclD

   414     assume "(Th th1, Th th2) \<in> child s"

   415     from child_unique[OF vt ch1 this] have "th = th2" by simp

   416     with ch2 have "(Th th2, Th th2) \<in> child s" by simp

   417     with wf_child[OF vt] show ?thesis by auto

   418   next

   419     fix c

   420     assume h1: "(Th th1, c) \<in> child s"

   421       and h2: "(c, Th th2) \<in> (child s)\<^sup>+"

   422     from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)

   423     with h1 have "(Th th1, Th th3) \<in> child s" by simp

   424     from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp

   425     with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp

   426     with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto

   427     moreover have "wf ((child s)\<^sup>+)"

   428     proof(rule wf_trancl)

   429       from wf_child[OF vt] show "wf (child s)" .

   430     qed

   431     ultimately show False by auto

   432   qed

   433 qed

   434 

   435 lemma unique_depend_p:

   436   assumes vt: "vt step s"

   437   and dp1: "(n, n1) \<in> (depend s)^+"

   438   and dp2: "(n, n2) \<in> (depend s)^+"

   439   and neq: "n1 \<noteq> n2"

   440   shows "(n1, n2) \<in> (depend s)^+ \<or> (n2, n1) \<in> (depend s)^+"

   441 proof(rule unique_chain [OF _ dp1 dp2 neq])

   442   from unique_depend[OF vt]

   443   show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by auto

   444 qed

   445 

   446 lemma dependents_child_unique:

   447   fixes s th th1 th2 th3

   448   assumes vt: "vt step s"

   449   and ch1: "(Th th1, Th th) \<in> child s"

   450   and ch2: "(Th th2, Th th) \<in> child s"

   451   and dp1: "th3 \<in> dependents s th1"

   452   and dp2: "th3 \<in> dependents s th2"

   453 shows "th1 = th2"

   454 proof -

   455   { assume neq: "th1 \<noteq> th2"

   456     from dp1 have dp1: "(Th th3, Th th1) \<in> (depend s)^+" 

   457       by (simp add:s_dependents_def eq_depend)

   458     from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+" 

   459       by (simp add:s_dependents_def eq_depend)

   460     from unique_depend_p[OF vt dp1 dp2] and neq

   461     have "(Th th1, Th th2) \<in> (depend s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (depend s)\<^sup>+" by auto

   462     hence False

   463     proof

   464       assume "(Th th1, Th th2) \<in> (depend s)\<^sup>+ "

   465       from children_no_dep[OF vt ch1 ch2 this] show ?thesis .

   466     next

   467       assume " (Th th2, Th th1) \<in> (depend s)\<^sup>+"

   468       from children_no_dep[OF vt ch2 ch1 this] show ?thesis .

   469     qed

   470   } thus ?thesis by auto

   471 qed

   472 

   473 lemma cp_rec:

   474   fixes s th

   475   assumes vt: "vt step s"

   476   shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"

   477 proof(unfold cp_eq_cpreced_f cpreced_def)

   478   let ?f = "(\<lambda>th. preced th s)"

   479   show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =

   480         Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th)"

   481   proof(cases " children s th = {}")

   482     case False

   483     have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th = 

   484           {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"

   485       (is "?L = ?R")

   486       by auto

   487     also have "\<dots> = 

   488       Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"

   489       (is "_ = Max ` ?C")

   490       by auto

   491     finally have "Max ?L = Max (Max ` ?C)" by auto

   492     also have "\<dots> = Max (\<Union> ?C)"

   493     proof(rule Max_Union[symmetric])

   494       from children_dependents[of s th] finite_threads[OF vt] and dependents_threads[OF vt, of th]

   495       show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"

   496         by (auto simp:finite_subset)

   497     next

   498       from False

   499       show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"

   500         by simp

   501     next

   502       show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>

   503         finite A \<and> A \<noteq> {}"

   504         apply (auto simp:finite_subset)

   505       proof -

   506         fix th'

   507         from finite_threads[OF vt] and dependents_threads[OF vt, of th']

   508         show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th')" by (auto simp:finite_subset)

   509       qed

   510     qed

   511     also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependents (wq s) th)"

   512       (is "Max ?A = Max ?B")

   513     proof -

   514       have "?A = ?B"

   515       proof

   516         show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}

   517                     \<subseteq> (\<lambda>th. preced th s) ` dependents (wq s) th"

   518         proof

   519           fix x 

   520           assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"

   521           then obtain th' where 

   522              th'_in: "th' \<in> children s th"

   523             and x_in: "x \<in> ?f ` ({th'} \<union> dependents (wq s) th')" by auto

   524           hence "x = ?f th' \<or> x \<in> (?f ` dependents (wq s) th')" by auto

   525           thus "x \<in> ?f ` dependents (wq s) th"

   526           proof

   527             assume "x = preced th' s"

   528             with th'_in and children_dependents

   529             show "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" by auto

   530           next

   531             assume "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th'"

   532             moreover note th'_in

   533             ultimately show " x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"

   534               by (unfold cs_dependents_def children_def child_def, auto simp:eq_depend)

   535           qed

   536         qed

   537       next

   538         show "?f ` dependents (wq s) th

   539            \<subseteq> \<Union>{?f ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"

   540         proof

   541           fix x 

   542           assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"

   543           then obtain th' where

   544             eq_x: "x = ?f th'" and dp: "(Th th', Th th) \<in> (depend s)^+" 

   545             by (auto simp:cs_dependents_def eq_depend)

   546           from depend_children[OF dp]

   547           have "th' \<in> children s th \<or> (\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+)" .

   548           thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"

   549           proof

   550             assume "th' \<in> children s th"

   551             with eq_x

   552             show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"

   553               by auto

   554           next

   555             assume "\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+"

   556             then obtain th3 where th3_in: "th3 \<in> children s th"

   557               and dp3: "(Th th', Th th3) \<in> (depend s)\<^sup>+" by auto

   558             show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"

   559             proof -

   560               from dp3

   561               have "th' \<in> dependents (wq s) th3"

   562                 by (auto simp:cs_dependents_def eq_depend)

   563               with eq_x th3_in show ?thesis by auto

   564             qed

   565           qed          

   566         qed

   567       qed

   568       thus ?thesis by simp

   569     qed

   570     finally have "Max ((\<lambda>th. preced th s) ` dependents (wq s) th) = Max (?L)" 

   571       (is "?X = ?Y") by auto

   572     moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) = 

   573                    max (?f th) ?X" 

   574     proof -

   575       have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) = 

   576             Max ({?f th} \<union> ?f ` (dependents (wq s) th))" by simp

   577       also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependents (wq s) th)))"

   578       proof(rule Max_Un, auto)

   579         from finite_threads[OF vt] and dependents_threads[OF vt, of th]

   580         show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th)" by (auto simp:finite_subset)

   581       next

   582         assume "dependents (wq s) th = {}"

   583         with False and children_dependents show False by auto

   584       qed

   585       also have "\<dots> = max (?f th) ?X" by simp

   586       finally show ?thesis .

   587     qed

   588     moreover have "Max ({preced th s} \<union> 

   589                      (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) = 

   590                    max (?f th) ?Y"

   591     proof -

   592       have "Max ({preced th s} \<union> 

   593                      (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) = 

   594             max (Max {preced th s}) ?Y"

   595       proof(rule Max_Un, auto)

   596         from finite_threads[OF vt] dependents_threads[OF vt, of th] children_dependents [of s th]

   597         show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependents (wq s) th))) ` 

   598                        children s th)" 

   599           by (auto simp:finite_subset)

   600       next

   601         assume "children s th = {}"

   602         with False show False by auto

   603       qed

   604       thus ?thesis by simp

   605     qed

   606     ultimately show ?thesis by auto

   607   next

   608     case True

   609     moreover have "dependents (wq s) th = {}"

   610     proof -

   611       { fix th'

   612         assume "th' \<in> dependents (wq s) th"

   613         hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependents_def eq_depend)

   614         from depend_children[OF this] and True

   615         have "False" by auto

   616       } thus ?thesis by auto

   617     qed

   618     ultimately show ?thesis by auto

   619   qed

   620 qed

   621 

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

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

   624 

   625 locale step_set_cps =

   626   fixes s' th prio s 

   627   defines s_def : "s \<equiv> (Set th prio#s')"

   628   assumes vt_s: "vt step s"

   629 

   630 context step_set_cps 

   631 begin

   632 

   633 lemma eq_preced:

   634   fixes th'

   635   assumes "th' \<noteq> th"

   636   shows "preced th' s = preced th' s'"

   637 proof -

   638   from assms show ?thesis 

   639     by (unfold s_def, auto simp:preced_def)

   640 qed

   641 

   642 lemma eq_dep: "depend s = depend s'"

   643   by (unfold s_def depend_set_unchanged, auto)

   644 

   645 lemma eq_cp:

   646   fixes th' 

   647   assumes neq_th: "th' \<noteq> th"

   648   and nd: "th \<notin> dependents s th'"

   649   shows "cp s th' = cp s' th'"

   650   apply (unfold cp_eq_cpreced cpreced_def)

   651 proof -

   652   have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"

   653     by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)

   654   moreover {

   655     fix th1 

   656     assume "th1 \<in> {th'} \<union> dependents (wq s') th'"

   657     hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto

   658     hence "preced th1 s = preced th1 s'"

   659     proof

   660       assume "th1 = th'"

   661       with eq_preced[OF neq_th]

   662       show "preced th1 s = preced th1 s'" by simp

   663     next

   664       assume "th1 \<in> dependents (wq s') th'"

   665       with nd and eq_dp have "th1 \<noteq> th"

   666         by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)

   667       from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp

   668     qed

   669   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = 

   670                      ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" 

   671     by (auto simp:image_def)

   672   thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =

   673         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp

   674 qed

   675 

   676 lemma eq_up:

   677   fixes th' th''

   678   assumes dp1: "th \<in> dependents s th'"

   679   and dp2: "th' \<in> dependents s th''"

   680   and eq_cps: "cp s th' = cp s' th'"

   681   shows "cp s th'' = cp s' th''"

   682 proof -

   683   from dp2

   684   have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)

   685   from depend_child[OF vt_s this[unfolded eq_depend]]

   686   have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .

   687   moreover { fix n th''

   688     have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>

   689                    (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"

   690     proof(erule trancl_induct, auto)

   691       fix y th''

   692       assume y_ch: "(y, Th th'') \<in> child s"

   693         and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"

   694         and ch': "(Th th', y) \<in> (child s)\<^sup>+"

   695       from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)

   696       with ih have eq_cpy:"cp s thy = cp s' thy" by blast

   697       from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)

   698       moreover from child_depend_p[OF ch'] and eq_y

   699       have "(Th th', Th thy) \<in> (depend s)^+" by simp

   700       ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto

   701       show "cp s th'' = cp s' th''"

   702         apply (subst cp_rec[OF vt_s])

   703       proof -

   704         have "preced th'' s = preced th'' s'"

   705         proof(rule eq_preced)

   706           show "th'' \<noteq> th"

   707           proof

   708             assume "th'' = th"

   709             with dp_thy y_ch[unfolded eq_y] 

   710             have "(Th th, Th th) \<in> (depend s)^+"

   711               by (auto simp:child_def)

   712             with wf_trancl[OF wf_depend[OF vt_s]] 

   713             show False by auto

   714           qed

   715         qed

   716         moreover { 

   717           fix th1

   718           assume th1_in: "th1 \<in> children s th''"

   719           have "cp s th1 = cp s' th1"

   720           proof(cases "th1 = thy")

   721             case True

   722             with eq_cpy show ?thesis by simp

   723           next

   724             case False

   725             have neq_th1: "th1 \<noteq> th"

   726             proof

   727               assume eq_th1: "th1 = th"

   728               with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp

   729               from children_no_dep[OF vt_s _ _ this] and 

   730               th1_in y_ch eq_y show False by (auto simp:children_def)

   731             qed

   732             have "th \<notin> dependents s th1"

   733             proof

   734               assume h:"th \<in> dependents s th1"

   735               from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)

   736               from dependents_child_unique[OF vt_s _ _ h this]

   737               th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)

   738               with False show False by auto

   739             qed

   740             from eq_cp[OF neq_th1 this]

   741             show ?thesis .

   742           qed

   743         }

   744         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 

   745           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)

   746         moreover have "children s th'' = children s' th''"

   747           by (unfold children_def child_def s_def depend_set_unchanged, simp)

   748         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"

   749           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])

   750       qed

   751     next

   752       fix th''

   753       assume dp': "(Th th', Th th'') \<in> child s"

   754       show "cp s th'' = cp s' th''"

   755         apply (subst cp_rec[OF vt_s])

   756       proof -

   757         have "preced th'' s = preced th'' s'"

   758         proof(rule eq_preced)

   759           show "th'' \<noteq> th"

   760           proof

   761             assume "th'' = th"

   762             with dp1 dp'

   763             have "(Th th, Th th) \<in> (depend s)^+"

   764               by (auto simp:child_def s_dependents_def eq_depend)

   765             with wf_trancl[OF wf_depend[OF vt_s]] 

   766             show False by auto

   767           qed

   768         qed

   769         moreover { 

   770           fix th1

   771           assume th1_in: "th1 \<in> children s th''"

   772           have "cp s th1 = cp s' th1"

   773           proof(cases "th1 = th'")

   774             case True

   775             with eq_cps show ?thesis by simp

   776           next

   777             case False

   778             have neq_th1: "th1 \<noteq> th"

   779             proof

   780               assume eq_th1: "th1 = th"

   781               with dp1 have "(Th th1, Th th') \<in> (depend s)^+" 

   782                 by (auto simp:s_dependents_def eq_depend)

   783               from children_no_dep[OF vt_s _ _ this]

   784               th1_in dp'

   785               show False by (auto simp:children_def)

   786             qed

   787             thus ?thesis

   788             proof(rule eq_cp)

   789               show "th \<notin> dependents s th1"

   790               proof

   791                 assume "th \<in> dependents s th1"

   792                 from dependents_child_unique[OF vt_s _ _ this dp1]

   793                 th1_in dp' have "th1 = th'"

   794                   by (auto simp:children_def)

   795                 with False show False by auto

   796               qed

   797             qed

   798           qed

   799         }

   800         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 

   801           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)

   802         moreover have "children s th'' = children s' th''"

   803           by (unfold children_def child_def s_def depend_set_unchanged, simp)

   804         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"

   805           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])

   806       qed     

   807     qed

   808   }

   809   ultimately show ?thesis by auto

   810 qed

   811 

   812 lemma eq_up_self:

   813   fixes th' th''

   814   assumes dp: "th \<in> dependents s th''"

   815   and eq_cps: "cp s th = cp s' th"

   816   shows "cp s th'' = cp s' th''"

   817 proof -

   818   from dp

   819   have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)

   820   from depend_child[OF vt_s this[unfolded eq_depend]]

   821   have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .

   822   moreover { fix n th''

   823     have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>

   824                    (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"

   825     proof(erule trancl_induct, auto)

   826       fix y th''

   827       assume y_ch: "(y, Th th'') \<in> child s"

   828         and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"

   829         and ch': "(Th th, y) \<in> (child s)\<^sup>+"

   830       from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)

   831       with ih have eq_cpy:"cp s thy = cp s' thy" by blast

   832       from child_depend_p[OF ch'] and eq_y

   833       have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by simp

   834       show "cp s th'' = cp s' th''"

   835         apply (subst cp_rec[OF vt_s])

   836       proof -

   837         have "preced th'' s = preced th'' s'"

   838         proof(rule eq_preced)

   839           show "th'' \<noteq> th"

   840           proof

   841             assume "th'' = th"

   842             with dp_thy y_ch[unfolded eq_y] 

   843             have "(Th th, Th th) \<in> (depend s)^+"

   844               by (auto simp:child_def)

   845             with wf_trancl[OF wf_depend[OF vt_s]] 

   846             show False by auto

   847           qed

   848         qed

   849         moreover { 

   850           fix th1

   851           assume th1_in: "th1 \<in> children s th''"

   852           have "cp s th1 = cp s' th1"

   853           proof(cases "th1 = thy")

   854             case True

   855             with eq_cpy show ?thesis by simp

   856           next

   857             case False

   858             have neq_th1: "th1 \<noteq> th"

   859             proof

   860               assume eq_th1: "th1 = th"

   861               with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp

   862               from children_no_dep[OF vt_s _ _ this] and 

   863               th1_in y_ch eq_y show False by (auto simp:children_def)

   864             qed

   865             have "th \<notin> dependents s th1"

   866             proof

   867               assume h:"th \<in> dependents s th1"

   868               from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)

   869               from dependents_child_unique[OF vt_s _ _ h this]

   870               th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)

   871               with False show False by auto

   872             qed

   873             from eq_cp[OF neq_th1 this]

   874             show ?thesis .

   875           qed

   876         }

   877         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 

   878           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)

   879         moreover have "children s th'' = children s' th''"

   880           by (unfold children_def child_def s_def depend_set_unchanged, simp)

   881         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"

   882           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])

   883       qed

   884     next

   885       fix th''

   886       assume dp': "(Th th, Th th'') \<in> child s"

   887       show "cp s th'' = cp s' th''"

   888         apply (subst cp_rec[OF vt_s])

   889       proof -

   890         have "preced th'' s = preced th'' s'"

   891         proof(rule eq_preced)

   892           show "th'' \<noteq> th"

   893           proof

   894             assume "th'' = th"

   895             with dp dp'

   896             have "(Th th, Th th) \<in> (depend s)^+"

   897               by (auto simp:child_def s_dependents_def eq_depend)

   898             with wf_trancl[OF wf_depend[OF vt_s]] 

   899             show False by auto

   900           qed

   901         qed

   902         moreover { 

   903           fix th1

   904           assume th1_in: "th1 \<in> children s th''"

   905           have "cp s th1 = cp s' th1"

   906           proof(cases "th1 = th")

   907             case True

   908             with eq_cps show ?thesis by simp

   909           next

   910             case False

   911             assume neq_th1: "th1 \<noteq> th"

   912             thus ?thesis

   913             proof(rule eq_cp)

   914               show "th \<notin> dependents s th1"

   915               proof

   916                 assume "th \<in> dependents s th1"

   917                 hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)

   918                 from children_no_dep[OF vt_s _ _ this]

   919                 and th1_in dp' show False

   920                   by (auto simp:children_def)

   921               qed

   922             qed

   923           qed

   924         }

   925         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 

   926           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)

   927         moreover have "children s th'' = children s' th''"

   928           by (unfold children_def child_def s_def depend_set_unchanged, simp)

   929         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"

   930           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])

   931       qed     

   932     qed

   933   }

   934   ultimately show ?thesis by auto

   935 qed

   936 end

   937 

   938 lemma next_waiting:

   939   assumes vt: "vt step s"

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

   941   shows "waiting s th' cs"

   942 proof -

   943   from assms show ?thesis

   944     apply (auto simp:next_th_def s_waiting_def)

   945   proof -

   946     fix rest

   947     assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"

   948       and eq_wq: "wq s cs = th # rest"

   949       and ne: "rest \<noteq> []"

   950     have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 

   951     proof(rule someI2)

   952       from wq_distinct[OF vt, of cs] eq_wq

   953       show "distinct rest \<and> set rest = set rest" by auto

   954     next

   955       show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto

   956     qed

   957     with ni

   958     have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>  set (SOME q. distinct q \<and> set q = set rest)"

   959       by simp

   960     moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"

   961     proof(rule someI2)

   962       from wq_distinct[OF vt, of cs] eq_wq

   963       show "distinct rest \<and> set rest = set rest" by auto

   964     next

   965       from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto

   966     qed

   967     ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto

   968   next

   969     fix rest

   970     assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"

   971       and ne: "rest \<noteq> []"

   972     have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"

   973     proof(rule someI2)

   974       from wq_distinct[OF vt, of cs] eq_wq

   975       show "distinct rest \<and> set rest = set rest" by auto

   976     next

   977       from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto

   978     qed

   979     hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"

   980       by auto

   981     moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 

   982     proof(rule someI2)

   983       from wq_distinct[OF vt, of cs] eq_wq

   984       show "distinct rest \<and> set rest = set rest" by auto

   985     next

   986       show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto

   987     qed

   988     ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp

   989     with eq_wq and wq_distinct[OF vt, of cs]

   990     show False by auto

   991   qed

   992 qed

   993 

   994 locale step_v_cps =

   995   fixes s' th cs s 

   996   defines s_def : "s \<equiv> (V th cs#s')"

   997   assumes vt_s: "vt step s"

   998 

   999 locale step_v_cps_nt = step_v_cps +

  1000   fixes th'

  1001   assumes nt: "next_th s' th cs th'"

  1002 

  1003 context step_v_cps_nt

  1004 begin

  1005 

  1006 lemma depend_s:

  1007   "depend s = (depend s' - {(Cs cs, Th th)} - {(Th th', Cs cs)}) \<union>

  1008                                          {(Cs cs, Th th')}"

  1009 proof -

  1010   from step_depend_v[OF vt_s[unfolded s_def], folded s_def]

  1011     and nt show ?thesis  by (auto intro:next_th_unique)

  1012 qed

  1013 

  1014 lemma dependents_kept:

  1015   fixes th''

  1016   assumes neq1: "th'' \<noteq> th"

  1017   and neq2: "th'' \<noteq> th'"

  1018   shows "dependents (wq s) th'' = dependents (wq s') th''"

  1019 proof(auto)

  1020   fix x

  1021   assume "x \<in> dependents (wq s) th''"

  1022   hence dp: "(Th x, Th th'') \<in> (depend s)^+"

  1023     by (auto simp:cs_dependents_def eq_depend)

  1024   { fix n

  1025     have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow>  (n, Th th'') \<in> (depend s')^+"

  1026     proof(induct rule:converse_trancl_induct)

  1027       fix y 

  1028       assume "(y, Th th'') \<in> depend s"

  1029       with depend_s neq1 neq2

  1030       have "(y, Th th'') \<in> depend s'" by auto

  1031       thus "(y, Th th'') \<in> (depend s')\<^sup>+" by auto

  1032     next

  1033       fix y z 

  1034       assume yz: "(y, z) \<in> depend s"

  1035         and ztp: "(z, Th th'') \<in> (depend s)\<^sup>+"

  1036         and ztp': "(z, Th th'') \<in> (depend s')\<^sup>+"

  1037       have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"

  1038       proof

  1039         show "y \<noteq> Cs cs"

  1040         proof

  1041           assume eq_y: "y = Cs cs"

  1042           with yz have dp_yz: "(Cs cs, z) \<in> depend s" by simp

  1043           from depend_s

  1044           have cst': "(Cs cs, Th th') \<in> depend s" by simp

  1045           from unique_depend[OF vt_s this dp_yz] 

  1046           have eq_z: "z = Th th'" by simp

  1047           with ztp have "(Th th', Th th'') \<in> (depend s)^+" by simp

  1048           from converse_tranclE[OF this]

  1049           obtain cs' where dp'': "(Th th', Cs cs') \<in> depend s"

  1050             by (auto simp:s_depend_def)

  1051           with depend_s have dp': "(Th th', Cs cs') \<in> depend s'" by auto

  1052           from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (depend s)^+" by auto

  1053           moreover have "cs' = cs"

  1054           proof -

  1055             from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]

  1056             have "(Th th', Cs cs) \<in> depend s'"

  1057               by (auto simp:s_waiting_def s_depend_def cs_waiting_def)

  1058             from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']

  1059             show ?thesis by simp

  1060           qed

  1061           ultimately have "(Cs cs, Cs cs) \<in> (depend s)^+" by simp

  1062           moreover note wf_trancl[OF wf_depend[OF vt_s]]

  1063           ultimately show False by auto

  1064         qed

  1065       next

  1066         show "y \<noteq> Th th'"

  1067         proof

  1068           assume eq_y: "y = Th th'"

  1069           with yz have dps: "(Th th', z) \<in> depend s" by simp

  1070           with depend_s have dps': "(Th th', z) \<in> depend s'" by auto

  1071           have "z = Cs cs"

  1072           proof -

  1073             from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]

  1074             have "(Th th', Cs cs) \<in> depend s'"

  1075               by (auto simp:s_waiting_def s_depend_def cs_waiting_def)

  1076             from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]

  1077             show ?thesis .

  1078           qed

  1079           with dps depend_s show False by auto

  1080         qed

  1081       qed

  1082       with depend_s yz have "(y, z) \<in> depend s'" by auto

  1083       with ztp'

  1084       show "(y, Th th'') \<in> (depend s')\<^sup>+" by auto

  1085     qed    

  1086   }

  1087   from this[OF dp]

  1088   show "x \<in> dependents (wq s') th''" 

  1089     by (auto simp:cs_dependents_def eq_depend)

  1090 next

  1091   fix x

  1092   assume "x \<in> dependents (wq s') th''"

  1093   hence dp: "(Th x, Th th'') \<in> (depend s')^+"

  1094     by (auto simp:cs_dependents_def eq_depend)

  1095   { fix n

  1096     have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow>  (n, Th th'') \<in> (depend s)^+"

  1097     proof(induct rule:converse_trancl_induct)

  1098       fix y 

  1099       assume "(y, Th th'') \<in> depend s'"

  1100       with depend_s neq1 neq2

  1101       have "(y, Th th'') \<in> depend s" by auto

  1102       thus "(y, Th th'') \<in> (depend s)\<^sup>+" by auto

  1103     next

  1104       fix y z 

  1105       assume yz: "(y, z) \<in> depend s'"

  1106         and ztp: "(z, Th th'') \<in> (depend s')\<^sup>+"

  1107         and ztp': "(z, Th th'') \<in> (depend s)\<^sup>+"

  1108       have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"

  1109       proof

  1110         show "y \<noteq> Cs cs"

  1111         proof

  1112           assume eq_y: "y = Cs cs"

  1113           with yz have dp_yz: "(Cs cs, z) \<in> depend s'" by simp

  1114           from this have eq_z: "z = Th th"

  1115           proof -

  1116             from step_back_step[OF vt_s[unfolded s_def]]

  1117             have "(Cs cs, Th th) \<in> depend s'"

  1118               by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)

  1119             from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]

  1120             show ?thesis by simp

  1121           qed

  1122           from converse_tranclE[OF ztp]

  1123           obtain u where "(z, u) \<in> depend s'" by auto

  1124           moreover 

  1125           from step_back_step[OF vt_s[unfolded s_def]]

  1126           have "th \<in> readys s'" by (cases, simp add:runing_def)

  1127           moreover note eq_z

  1128           ultimately show False 

  1129             by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)

  1130         qed

  1131       next

  1132         show "y \<noteq> Th th'"

  1133         proof

  1134           assume eq_y: "y = Th th'"

  1135           with yz have dps: "(Th th', z) \<in> depend s'" by simp