1 theory CpsG

     2 imports PrioG 

     3 begin

     4 

     5 lemma not_thread_holdents:

     6   fixes th s

     7   assumes vt: "vt 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 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_test)

    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_test 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_test 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 assms thread_exit ih stp not_in vt eq_e have vtp: "vt (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_test 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 assms thread_V eq_e ih stp not_in vt have vtv: "vt (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: wq_def 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_test 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_test)

   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_test s_depend_def wq_def cs_holding_def)

   125   qed

   126 qed

   127 

   128 

   129 

   130 lemma next_th_neq: 

   131   assumes vt: "vt 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 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 \<equiv>

   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 \<equiv> {th'. (Th th', Th th) \<in> child s}"

   253 

   254 lemma children_def2:

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

   256 unfolding child_def children_def by simp

   257 

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

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

   260 

   261 lemma child_unique:

   262   assumes vt: "vt s"

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

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

   265   shows "th1 = th2"

   266 proof -

   267   from ch1 ch2 show ?thesis

   268   proof(unfold child_def, clarsimp)

   269     fix cs csa

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

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

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

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

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

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

   276     from unique_depend[OF vt h2 this]

   277     show "th1 = th2" by simp

   278   qed 

   279 qed

   280 

   281 

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

   283 proof -

   284   from fun_eq_iff 

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

   286   show ?thesis

   287   proof(rule h)

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

   289   qed

   290 qed

   291 

   292 lemma depend_children:

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

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

   295 proof -

   296   from h show ?thesis

   297   proof(induct rule: tranclE)

   298     fix c th2

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

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

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

   302       by (case_tac c, auto simp:s_depend_def)

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

   304     proof(rule tranclE[OF h1])

   305       fix ca

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

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

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

   309       proof -

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

   311           by (case_tac ca, auto simp:s_depend_def)

   312         from eq_ca h4 h2 eq_c

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

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

   315         ultimately show ?thesis by auto

   316       qed

   317     next

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

   319       with h2 eq_c

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

   321         by (auto simp:children_def child_def)

   322       thus ?thesis by auto

   323     qed

   324   next

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

   326     thus ?thesis

   327       by (auto simp:s_depend_def)

   328   qed

   329 qed

   330 

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

   332   by (unfold child_def, auto)

   333 

   334 lemma wf_child: 

   335   assumes vt: "vt s"

   336   shows "wf (child s)"

   337 proof(rule wf_subset)

   338   from wf_trancl[OF wf_depend[OF vt]]

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

   340 next

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

   342 qed

   343 

   344 lemma depend_child_pre:

   345   assumes vt: "vt s"

   346   shows

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

   348 proof -

   349   from wf_trancl[OF wf_depend[OF vt]]

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

   351   show ?thesis

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

   353     fix th'

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

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

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

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

   358     proof -

   359       from depend_children[OF h]

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

   361       thus ?thesis

   362       proof

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

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

   365       next

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

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

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

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

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

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

   372       qed

   373     qed

   374   qed

   375 qed

   376 

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

   378   by (insert depend_child_pre, auto)

   379 

   380 lemma child_depend_p:

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

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

   383 proof -

   384   from assms show ?thesis

   385   proof(induct)

   386     case (base y)

   387     with sub_child show ?case by auto

   388   next

   389     case (step y z)

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

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

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

   393     ultimately show ?case by auto

   394   qed

   395 qed

   396 

   397 lemma child_depend_eq: 

   398   assumes vt: "vt s"

   399   shows 

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

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

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

   403 

   404 lemma children_no_dep:

   405   fixes s th th1 th2 th3

   406   assumes vt: "vt s"

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

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

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

   410   shows "False"

   411 proof -

   412   from depend_child[OF vt ch3]

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

   414   thus ?thesis

   415   proof(rule converse_tranclE)

   416     thm tranclD

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

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

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

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

   421   next

   422     fix c

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

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

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

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

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

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

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

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

   431     proof(rule wf_trancl)

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

   433     qed

   434     ultimately show False by auto

   435   qed

   436 qed

   437 

   438 lemma unique_depend_p:

   439   assumes vt: "vt s"

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

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

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

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

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

   445   from unique_depend[OF vt]

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

   447 qed

   448 

   449 lemma dependents_child_unique:

   450   fixes s th th1 th2 th3

   451   assumes vt: "vt s"

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

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

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

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

   456 shows "th1 = th2"

   457 proof -

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

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

   460       by (simp add:s_dependents_def eq_depend)

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

   462       by (simp add:s_dependents_def eq_depend)

   463     from unique_depend_p[OF vt dp1 dp2] and neq

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

   465     hence False

   466     proof

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

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

   469     next

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

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

   472     qed

   473   } thus ?thesis by auto

   474 qed

   475 

   476 lemma cp_rec:

   477   fixes s th

   478   assumes vt: "vt s"

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

   480 proof(unfold cp_eq_cpreced_f cpreced_def)

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

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

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

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

   485     case False

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

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

   488       (is "?L = ?R")

   489       by auto

   490     also have "\<dots> = 

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

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

   493       by auto

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

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

   496     proof(rule Max_Union[symmetric])

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

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

   499         by (auto simp:finite_subset)

   500     next

   501       from False

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

   503         by simp

   504     next

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

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

   507         apply (auto simp:finite_subset)

   508       proof -

   509         fix th'

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

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

   512       qed

   513     qed

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

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

   516     proof -

   517       have "?A = ?B"

   518       proof

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

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

   521         proof

   522           fix x 

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

   524           then obtain th' where 

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

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

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

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

   529           proof

   530             assume "x = preced th' s"

   531             with th'_in and children_dependents

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

   533           next

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

   535             moreover note th'_in

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

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

   538           qed

   539         qed

   540       next

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

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

   543         proof

   544           fix x 

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

   546           then obtain th' where

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

   548             by (auto simp:cs_dependents_def eq_depend)

   549           from depend_children[OF dp]

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

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

   552           proof

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

   554             with eq_x

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

   556               by auto

   557           next

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

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

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

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

   562             proof -

   563               from dp3

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

   565                 by (auto simp:cs_dependents_def eq_depend)

   566               with eq_x th3_in show ?thesis by auto

   567             qed

   568           qed          

   569         qed

   570       qed

   571       thus ?thesis by simp

   572     qed

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

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

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

   576                    max (?f th) ?X" 

   577     proof -

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

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

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

   581       proof(rule Max_Un, auto)

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

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

   584       next

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

   586         with False and children_dependents show False by auto

   587       qed

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

   589       finally show ?thesis .

   590     qed

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

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

   593                    max (?f th) ?Y"

   594     proof -

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

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

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

   598       proof(rule Max_Un, auto)

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

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

   601                        children s th)" 

   602           by (auto simp:finite_subset)

   603       next

   604         assume "children s th = {}"

   605         with False show False by auto

   606       qed

   607       thus ?thesis by simp

   608     qed

   609     ultimately show ?thesis by auto

   610   next

   611     case True

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

   613     proof -

   614       { fix th'

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

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

   617         from depend_children[OF this] and True

   618         have "False" by auto

   619       } thus ?thesis by auto

   620     qed

   621     ultimately show ?thesis by auto

   622   qed

   623 qed

   624 

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

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

   627 

   628 locale step_set_cps =

   629   fixes s' th prio s 

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

   631   assumes vt_s: "vt s"

   632 

   633 context step_set_cps 

   634 begin

   635 

   636 lemma eq_preced:

   637   fixes th'

   638   assumes "th' \<noteq> th"

   639   shows "preced th' s = preced th' s'"

   640 proof -

   641   from assms show ?thesis 

   642     by (unfold s_def, auto simp:preced_def)

   643 qed

   644 

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

   646   by (unfold s_def depend_set_unchanged, auto)

   647 

   648 lemma eq_cp_pre:

   649   fixes th' 

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

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

   652   shows "cp s th' = cp s' th'"

   653   apply (unfold cp_eq_cpreced cpreced_def)

   654 proof -

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

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

   657   moreover {

   658     fix th1 

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

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

   661     hence "preced th1 s = preced th1 s'"

   662     proof

   663       assume "th1 = th'"

   664       with eq_preced[OF neq_th]

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

   666     next

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

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

   669         by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)

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

   671     qed

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

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

   674     by (auto simp:image_def)

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

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

   677 qed

   678 

   679 lemma no_dependents:

   680   assumes "th' \<noteq> th"

   681   shows "th \<notin> dependents s th'"

   682 proof

   683   assume h: "th \<in> dependents s th'"

   684   from step_back_step [OF vt_s[unfolded s_def]]

   685   have "step s' (Set th prio)" .

   686   hence "th \<in> runing s'" by (cases, simp)

   687   hence rd_th: "th \<in> readys s'" 

   688     by (simp add:readys_def runing_def)

   689   from h have "(Th th, Th th') \<in> (depend s')\<^sup>+"

   690     by (unfold s_dependents_def, unfold eq_depend, unfold eq_dep, auto)

   691   from tranclD[OF this]

   692   obtain z where "(Th th, z) \<in> depend s'" by auto

   693   with rd_th show "False"

   694     apply (case_tac z, auto simp:readys_def s_waiting_def s_depend_def s_waiting_def cs_waiting_def)

   695     by (fold wq_def, blast)

   696 qed

   697 

   698 (* Result improved *)

   699 lemma eq_cp:

   700  fixes th' 

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

   702   shows "cp s th' = cp s' th'"

   703 proof(rule eq_cp_pre [OF neq_th])

   704   from no_dependents[OF neq_th] 

   705   show "th \<notin> dependents s th'" .

   706 qed

   707 

   708 lemma eq_up:

   709   fixes th' th''

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

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

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

   713   shows "cp s th'' = cp s' th''"

   714 proof -

   715   from dp2

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

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

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

   719   moreover { fix n th''

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

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

   722     proof(erule trancl_induct, auto)

   723       fix y th''

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

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

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

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

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

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

   730       moreover from child_depend_p[OF ch'] and eq_y

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

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

   733       show "cp s th'' = cp s' th''"

   734         apply (subst cp_rec[OF vt_s])

   735       proof -

   736         have "preced th'' s = preced th'' s'"

   737         proof(rule eq_preced)

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

   739           proof

   740             assume "th'' = th"

   741             with dp_thy y_ch[unfolded eq_y] 

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

   743               by (auto simp:child_def)

   744             with wf_trancl[OF wf_depend[OF vt_s]] 

   745             show False by auto

   746           qed

   747         qed

   748         moreover { 

   749           fix th1

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

   751           have "cp s th1 = cp s' th1"

   752           proof(cases "th1 = thy")

   753             case True

   754             with eq_cpy show ?thesis by simp

   755           next

   756             case False

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

   758             proof

   759               assume eq_th1: "th1 = th"

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

   761               from children_no_dep[OF vt_s _ _ this] and 

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

   763             qed

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

   765             proof

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

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

   768               from dependents_child_unique[OF vt_s _ _ h this]

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

   770               with False show False by auto

   771             qed

   772             from eq_cp_pre[OF neq_th1 this]

   773             show ?thesis .

   774           qed

   775         }

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

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

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

   779           by (unfold children_def child_def s_def depend_set_unchanged, simp)

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

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

   782       qed

   783     next

   784       fix th''

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

   786       show "cp s th'' = cp s' th''"

   787         apply (subst cp_rec[OF vt_s])

   788       proof -

   789         have "preced th'' s = preced th'' s'"

   790         proof(rule eq_preced)

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

   792           proof

   793             assume "th'' = th"

   794             with dp1 dp'

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

   796               by (auto simp:child_def s_dependents_def eq_depend)

   797             with wf_trancl[OF wf_depend[OF vt_s]] 

   798             show False by auto

   799           qed

   800         qed

   801         moreover { 

   802           fix th1

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

   804           have "cp s th1 = cp s' th1"

   805           proof(cases "th1 = th'")

   806             case True

   807             with eq_cps show ?thesis by simp

   808           next

   809             case False

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

   811             proof

   812               assume eq_th1: "th1 = th"

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

   814                 by (auto simp:s_dependents_def eq_depend)

   815               from children_no_dep[OF vt_s _ _ this]

   816               th1_in dp'

   817               show False by (auto simp:children_def)

   818             qed

   819             thus ?thesis

   820             proof(rule eq_cp_pre)

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

   822               proof

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

   824                 from dependents_child_unique[OF vt_s _ _ this dp1]

   825                 th1_in dp' have "th1 = th'"

   826                   by (auto simp:children_def)

   827                 with False show False by auto

   828               qed

   829             qed

   830           qed

   831         }

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

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

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

   835           by (unfold children_def child_def s_def depend_set_unchanged, simp)

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

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

   838       qed     

   839     qed

   840   }

   841   ultimately show ?thesis by auto

   842 qed

   843 

   844 lemma eq_up_self:

   845   fixes th' th''

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

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

   848   shows "cp s th'' = cp s' th''"

   849 proof -

   850   from dp

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

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

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

   854   moreover { fix n th''

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

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

   857     proof(erule trancl_induct, auto)

   858       fix y th''

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

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

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

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

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

   864       from child_depend_p[OF ch'] and eq_y

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

   866       show "cp s th'' = cp s' th''"

   867         apply (subst cp_rec[OF vt_s])

   868       proof -

   869         have "preced th'' s = preced th'' s'"

   870         proof(rule eq_preced)

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

   872           proof

   873             assume "th'' = th"

   874             with dp_thy y_ch[unfolded eq_y] 

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

   876               by (auto simp:child_def)

   877             with wf_trancl[OF wf_depend[OF vt_s]] 

   878             show False by auto

   879           qed

   880         qed

   881         moreover { 

   882           fix th1

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

   884           have "cp s th1 = cp s' th1"

   885           proof(cases "th1 = thy")

   886             case True

   887             with eq_cpy show ?thesis by simp

   888           next

   889             case False

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

   891             proof

   892               assume eq_th1: "th1 = th"

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

   894               from children_no_dep[OF vt_s _ _ this] and 

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

   896             qed

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

   898             proof

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

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

   901               from dependents_child_unique[OF vt_s _ _ h this]

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

   903               with False show False by auto

   904             qed

   905             from eq_cp_pre[OF neq_th1 this]

   906             show ?thesis .

   907           qed

   908         }

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

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

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

   912           by (unfold children_def child_def s_def depend_set_unchanged, simp)

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

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

   915       qed

   916     next

   917       fix th''

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

   919       show "cp s th'' = cp s' th''"

   920         apply (subst cp_rec[OF vt_s])

   921       proof -

   922         have "preced th'' s = preced th'' s'"

   923         proof(rule eq_preced)

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

   925           proof

   926             assume "th'' = th"

   927             with dp dp'

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

   929               by (auto simp:child_def s_dependents_def eq_depend)

   930             with wf_trancl[OF wf_depend[OF vt_s]] 

   931             show False by auto

   932           qed

   933         qed

   934         moreover { 

   935           fix th1

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

   937           have "cp s th1 = cp s' th1"

   938           proof(cases "th1 = th")

   939             case True

   940             with eq_cps show ?thesis by simp

   941           next

   942             case False

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

   944             thus ?thesis

   945             proof(rule eq_cp_pre)

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

   947               proof

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

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

   950                 from children_no_dep[OF vt_s _ _ this]

   951                 and th1_in dp' show False

   952                   by (auto simp:children_def)

   953               qed

   954             qed

   955           qed

   956         }

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

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

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

   960           by (unfold children_def child_def s_def depend_set_unchanged, simp)

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

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

   963       qed     

   964     qed

   965   }

   966   ultimately show ?thesis by auto

   967 qed

   968 end

   969 

   970 lemma next_waiting:

   971   assumes vt: "vt s"

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

   973   shows "waiting s th' cs"

   974 proof -

   975   from assms show ?thesis

   976     apply (auto simp:next_th_def s_waiting_def[folded wq_def])

   977   proof -

   978     fix rest

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

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

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

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

   983     proof(rule someI2)

   984       from wq_distinct[OF vt, of cs] eq_wq

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

   986     next

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

   988     qed

   989     with ni

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

   991       by simp

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

   993     proof(rule someI2)

   994       from wq_distinct[OF vt, of cs] eq_wq

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

   996     next

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

   998     qed

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

  1000   next

  1001     fix rest

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

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

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

  1005     proof(rule someI2)

  1006       from wq_distinct[OF vt, of cs] eq_wq

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

  1008     next

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

  1010     qed

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

  1012       by auto

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

  1014     proof(rule someI2)

  1015       from wq_distinct[OF vt, of cs] eq_wq

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

  1017     next

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

  1019     qed

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

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

  1022     show False by auto

  1023   qed

  1024 qed

  1025 

  1026 

  1027 

  1028 

  1029 locale step_v_cps =

  1030   fixes s' th cs s 

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

  1032   assumes vt_s: "vt s"

  1033 

  1034 locale step_v_cps_nt = step_v_cps +

  1035   fixes th'

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

  1037 

  1038 context step_v_cps_nt

  1039 begin

  1040 

  1041 lemma depend_s:

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

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

  1044 proof -

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

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

  1047 qed

  1048 

  1049 lemma dependents_kept:

  1050   fixes th''

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

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

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

  1054 proof(auto)

  1055   fix x

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

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

  1058     by (auto simp:cs_dependents_def eq_depend)

  1059   { fix n

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

  1061     proof(induct rule:converse_trancl_induct)

  1062       fix y 

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

  1064       with depend_s neq1 neq2

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

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

  1067     next

  1068       fix y z 

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

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

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

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

  1073       proof

  1074         show "y \<noteq> Cs cs"

  1075         proof

  1076           assume eq_y: "y = Cs cs"

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

  1078           from depend_s

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

  1080           from unique_depend[OF vt_s this dp_yz] 

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

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

  1083           from converse_tranclE[OF this]

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

  1085             by (auto simp:s_depend_def)

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

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

  1088           moreover have "cs' = cs"

  1089           proof -

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

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

  1092               by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)

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

  1094             show ?thesis by simp

  1095           qed

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

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

  1098           ultimately show False by auto

  1099         qed

  1100       next

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

  1102         proof

  1103           assume eq_y: "y = Th th'"

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

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

  1106           have "z = Cs cs"

  1107           proof -

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

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

  1110               by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)

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

  1112             show ?thesis .

  1113           qed

  1114           with dps depend_s show False by auto

  1115         qed

  1116       qed

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

  1118       with ztp'

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

  1120     qed    

  1121   }

  1122   from this[OF dp]

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

  1124     by (auto simp:cs_dependents_def eq_depend)

  1125 next

  1126   fix x

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

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

  1129     by (auto simp:cs_dependents_def eq_depend)

  1130   { fix n

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

  1132     proof(induct rule:converse_trancl_induct)

  1133       fix y 

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

  1135       with depend_s neq1 neq2