1 section {*

     2   This file contains lemmas used to guide the recalculation of current precedence 

     3   after every system call (or system operation)

     4 *}

     5 theory CpsG

     6 imports PrioG Max RTree

     7 begin

     8 

     9 locale pip = 

    10   fixes s

    11   assumes vt: "vt s"

    12 

    13 context pip

    14 begin

    15 

    16 interpretation rtree_RAG: rtree "RAG s"

    17 proof

    18   show "single_valued (RAG s)"

    19     by (unfold single_valued_def, auto intro: unique_RAG[OF vt])

    20 

    21   show "acyclic (RAG s)"

    22      by (rule acyclic_RAG[OF vt])

    23 qed

    24 

    25 thm rtree_RAG.rpath_overlap_oneside

    26 

    27 end

    28 

    29 

    30 

    31 definition "the_preced s th = preced th s"

    32 

    33 lemma cp_alt_def:

    34   "cp s th =  

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

    36 proof -

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

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

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

    40   proof -

    41     have "?L = ?R" 

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

    43     thus ?thesis by simp

    44   qed

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

    46 qed

    47 

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

    49   by (simp add: s_dependants_abv wq_def)

    50   

    51 (* obvious lemma *)

    52 lemma not_thread_holdents:

    53   fixes th s

    54   assumes vt: "vt s"

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

    56   shows "holdents s th = {}"

    57 proof -

    58   from vt not_in show ?thesis

    59   proof(induct arbitrary:th)

    60     case (vt_cons s e th)

    61     assume vt: "vt s"

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

    63       and stp: "step s e"

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

    65     from stp show ?case

    66     proof(cases)

    67       case (thread_create thread prio)

    68       assume eq_e: "e = Create thread prio"

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

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

    71         apply (unfold eq_e holdents_test)

    72         by (simp add:RAG_create_unchanged)

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

    74       proof -

    75         from not_in eq_e show ?thesis by simp

    76       qed

    77       moreover note ih ultimately show ?thesis by auto

    78     next

    79       case (thread_exit thread)

    80       assume eq_e: "e = Exit thread"

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

    82       show ?thesis

    83       proof(cases "th = thread")

    84         case True

    85         with nh eq_e

    86         show ?thesis 

    87           by (auto simp:holdents_test RAG_exit_unchanged)

    88       next

    89         case False

    90         with not_in and eq_e

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

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

    93           by (auto simp:holdents_test RAG_exit_unchanged)

    94       qed

    95     next

    96       case (thread_P thread cs)

    97       assume eq_e: "e = P thread cs"

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

    99       from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto

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

   101       proof -

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

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

   104           by (simp add:runing_def readys_def)

   105         ultimately show ?thesis by auto

   106       qed

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

   108         apply (unfold cntCS_def holdents_test eq_e)

   109         by (unfold step_RAG_p[OF vtp], auto)

   110       moreover have "holdents s th = {}"

   111       proof(rule ih)

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

   113       qed

   114       ultimately show ?thesis by simp

   115     next

   116       case (thread_V thread cs)

   117       assume eq_e: "e = V thread cs"

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

   119         and hold: "holding s thread cs"

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

   121       proof -

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

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

   124           by (simp add:runing_def readys_def)

   125         ultimately show ?thesis by auto

   126       qed

   127       from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto

   128       from hold obtain rest 

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

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

   131       from not_in eq_e eq_wq

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

   133         apply (auto simp:next_th_def)

   134       proof -

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

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

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

   138         proof(rule someI2)

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

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

   141         next

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

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

   144         qed

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

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

   147         show False by auto

   148       qed

   149       moreover note neq_th eq_wq

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

   151         by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)

   152       moreover have "holdents s th = {}"

   153       proof(rule ih)

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

   155       qed

   156       ultimately show ?thesis by simp

   157     next

   158       case (thread_set thread prio)

   159       print_facts

   160       assume eq_e: "e = Set thread prio"

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

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

   163       from ih [OF this] and eq_e

   164       show ?thesis 

   165         apply (unfold eq_e cntCS_def holdents_test)

   166         by (simp add:RAG_set_unchanged)

   167     qed

   168     next

   169       case vt_nil

   170       show ?case

   171       by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)

   172   qed

   173 qed

   174 

   175 (* obvious lemma *)

   176 lemma next_th_neq: 

   177   assumes vt: "vt s"

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

   179   shows "th' \<noteq> th"

   180 proof -

   181   from nt show ?thesis

   182     apply (auto simp:next_th_def)

   183   proof -

   184     fix rest

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

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

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

   188     proof(rule someI2)

   189       from wq_distinct[OF vt, of cs] eq_wq

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

   191     next

   192       fix x

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

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

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

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

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

   198     qed

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

   200   qed

   201 qed

   202 

   203 (* obvious lemma *)

   204 lemma next_th_unique: 

   205   assumes nt1: "next_th s th cs th1"

   206   and nt2: "next_th s th cs th2"

   207   shows "th1 = th2"

   208 using assms by (unfold next_th_def, auto)

   209 

   210 lemma wf_RAG:

   211   assumes vt: "vt s"

   212   shows "wf (RAG s)"

   213 proof(rule finite_acyclic_wf)

   214   from finite_RAG[OF vt] show "finite (RAG s)" .

   215 next

   216   from acyclic_RAG[OF vt] show "acyclic (RAG s)" .

   217 qed

   218 

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

   220   where "child s \<equiv>

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

   222 

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

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

   225 

   226 lemma children_def2:

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

   228 unfolding child_def children_def by simp

   229 

   230 lemma children_dependants: 

   231   "children s th \<subseteq> dependants (wq s) th"

   232   unfolding children_def2

   233   unfolding cs_dependants_def

   234   by (auto simp add: eq_RAG)

   235 

   236 lemma child_unique:

   237   assumes vt: "vt s"

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

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

   240   shows "th1 = th2"

   241 using ch1 ch2 

   242 proof(unfold child_def, clarsimp)

   243   fix cs csa

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

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

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

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

   248   from unique_RAG[OF vt h1 h3] have "cs = csa" by simp

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

   250   from unique_RAG[OF vt h2 this]

   251   show "th1 = th2" by simp

   252 qed 

   253 

   254 lemma RAG_children:

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

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

   257 proof -

   258   from h show ?thesis

   259   proof(induct rule: tranclE)

   260     fix c th2

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

   262     and h2: "(c, Th th2) \<in> RAG s"

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

   264       by (case_tac c, auto simp:s_RAG_def)

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

   266     proof(rule tranclE[OF h1])

   267       fix ca

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

   269         and h4: "(ca, c) \<in> RAG s"

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

   271       proof -

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

   273           by (case_tac ca, auto simp:s_RAG_def)

   274         from eq_ca h4 h2 eq_c

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

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

   277         ultimately show ?thesis by auto

   278       qed

   279     next

   280       assume "(Th th1, c) \<in> RAG s"

   281       with h2 eq_c

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

   283         by (auto simp:children_def child_def)

   284       thus ?thesis by auto

   285     qed

   286   next

   287     assume "(Th th1, Th th2) \<in> RAG s"

   288     thus ?thesis

   289       by (auto simp:s_RAG_def)

   290   qed

   291 qed

   292 

   293 lemma sub_child: "child s \<subseteq> (RAG s)^+"

   294   by (unfold child_def, auto)

   295 

   296 lemma wf_child: 

   297   assumes vt: "vt s"

   298   shows "wf (child s)"

   299 apply(rule wf_subset)

   300 apply(rule wf_trancl[OF wf_RAG[OF vt]])

   301 apply(rule sub_child)

   302 done

   303 

   304 lemma RAG_child_pre:

   305   assumes vt: "vt s"

   306   shows

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

   308 proof -

   309   from wf_trancl[OF wf_RAG[OF vt]]

   310   have wf: "wf ((RAG s)^+)" .

   311   show ?thesis

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

   313     fix th'

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

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

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

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

   318     proof -

   319       from RAG_children[OF h]

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

   321       thus ?thesis

   322       proof

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

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

   325       next

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

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

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

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

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

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

   332       qed

   333     qed

   334   qed

   335 qed

   336 

   337 lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"

   338   by (insert RAG_child_pre, auto)

   339 

   340 lemma child_RAG_p:

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

   342   shows "(n1, n2) \<in> (RAG s)^+"

   343 proof -

   344   from assms show ?thesis

   345   proof(induct)

   346     case (base y)

   347     with sub_child show ?case by auto

   348   next

   349     case (step y z)

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

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

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

   353     ultimately show ?case by auto

   354   qed

   355 qed

   356 

   357 text {* (* ddd *)

   358 *}

   359 lemma child_RAG_eq: 

   360   assumes vt: "vt s"

   361   shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"

   362   by (auto intro: RAG_child[OF vt] child_RAG_p)

   363 

   364 text {* (* ddd *)

   365 *}

   366 lemma children_no_dep:

   367   fixes s th th1 th2 th3

   368   assumes vt: "vt s"

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

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

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

   372   shows "False"

   373 proof -

   374   from RAG_child[OF vt ch3]

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

   376   thus ?thesis

   377   proof(rule converse_tranclE)

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

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

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

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

   382   next

   383     fix c

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

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

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

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

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

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

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

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

   392     proof(rule wf_trancl)

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

   394     qed

   395     ultimately show False by auto

   396   qed

   397 qed

   398 

   399 text {* (* ddd *)

   400 *}

   401 lemma unique_RAG_p:

   402   assumes vt: "vt s"

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

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

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

   406   shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"

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

   408   from unique_RAG[OF vt]

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

   410 qed

   411 

   412 text {* (* ddd *)

   413 *}

   414 lemma dependants_child_unique:

   415   fixes s th th1 th2 th3

   416   assumes vt: "vt s"

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

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

   419   and dp1: "th3 \<in> dependants s th1"

   420   and dp2: "th3 \<in> dependants s th2"

   421 shows "th1 = th2"

   422 proof -

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

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

   425       by (simp add:s_dependants_def eq_RAG)

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

   427       by (simp add:s_dependants_def eq_RAG)

   428     from unique_RAG_p[OF vt dp1 dp2] and neq

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

   430     hence False

   431     proof

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

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

   434     next

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

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

   437     qed

   438   } thus ?thesis by auto

   439 qed

   440 

   441 lemma RAG_plus_elim:

   442   assumes "vt s"

   443   fixes x

   444   assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"

   445   shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"

   446   using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]

   447   apply (unfold children_def)

   448   by (metis assms(2) children_def RAG_children eq_RAG)

   449 

   450 text {* (* ddd *)

   451 *}

   452 lemma dependants_expand:

   453   assumes "vt s"

   454   shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"

   455 apply(simp add: image_def)

   456 unfolding cs_dependants_def

   457 apply(auto)

   458 apply (metis assms RAG_plus_elim mem_Collect_eq)

   459 apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')

   460 by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)

   461 

   462 lemma finite_children:

   463   assumes "vt s"

   464   shows "finite (children s th)"

   465   using children_dependants dependants_threads[OF assms] finite_threads[OF assms]

   466   by (metis rev_finite_subset)

   467   

   468 lemma finite_dependants:

   469   assumes "vt s"

   470   shows "finite (dependants (wq s) th')"

   471   using dependants_threads[OF assms] finite_threads[OF assms]

   472   by (metis rev_finite_subset)

   473 

   474 abbreviation

   475   "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"

   476 

   477 abbreviation

   478   "cpreceds s ths \<equiv> (cp s) ` ths"

   479 

   480 lemma Un_compr:

   481   "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"

   482 by auto

   483 

   484 lemma in_disj:

   485   shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"

   486 by metis

   487 

   488 lemma UN_exists:

   489   shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"

   490 by auto

   491 

   492 text {* (* ddd *)

   493   This is the recursive equation used to compute the current precedence of 

   494   a thread (the @{text "th"}) here. 

   495 *}

   496 lemma cp_rec:

   497   fixes s th

   498   assumes vt: "vt s"

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

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

   501   case True

   502   show ?thesis

   503     unfolding cp_eq_cpreced cpreced_def 

   504     by (subst dependants_expand[OF `vt s`]) (simp add: True)

   505 next

   506   case False

   507   show ?thesis (is "?LHS = ?RHS")

   508   proof -

   509     have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"

   510       by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])

   511   

   512     have not_emptyness_facts[simp]: 

   513       "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"

   514       using False dependants_expand[OF assms] by(auto simp only: Un_empty)

   515 

   516     have finiteness_facts[simp]:

   517       "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"

   518       by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])

   519 

   520     (* expanding definition *)

   521     have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"

   522       unfolding eq_cp by (simp add: Un_compr)

   523     

   524     (* moving Max in *)

   525     also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"

   526       by (simp add: Max_Un)

   527 

   528     (* expanding dependants *)

   529     also have "\<dots> = max (Max {preced th s}) 

   530       (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"

   531       by (subst dependants_expand[OF `vt s`]) (simp)

   532 

   533     (* moving out big Union *)

   534     also have "\<dots> = max (Max {preced th s})

   535       (Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"  

   536       by simp

   537 

   538     (* moving in small union *)

   539     also have "\<dots> = max (Max {preced th s})

   540       (Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"  

   541       by (simp add: in_disj)

   542 

   543     (* moving in preceds *)

   544     also have "\<dots> = max (Max {preced th s})  

   545       (Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))" 

   546       by (simp add: UN_exists)

   547 

   548     (* moving in Max *)

   549     also have "\<dots> = max (Max {preced th s})  

   550       (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))" 

   551       by (subst Max_Union) (auto simp add: image_image)

   552 

   553     (* folding cp + moving out Max *)

   554     also have "\<dots> = ?RHS" 

   555       unfolding eq_cp by (simp add: Max_insert)

   556 

   557     finally show "?LHS = ?RHS" .

   558   qed

   559 qed

   560 

   561 lemma next_waiting:

   562   assumes vt: "vt s"

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

   564   shows "waiting s th' cs"

   565 proof -

   566   from assms show ?thesis

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

   568   proof -

   569     fix rest

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

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

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

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

   574     proof(rule someI2)

   575       from wq_distinct[OF vt, of cs] eq_wq

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

   577     next

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

   579     qed

   580     with ni

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

   582       by simp

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

   584     proof(rule someI2)

   585       from wq_distinct[OF vt, of cs] eq_wq

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

   587     next

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

   589     qed

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

   591   next

   592     fix rest

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

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

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

   596     proof(rule someI2)

   597       from wq_distinct[OF vt, of cs] eq_wq

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

   599     next

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

   601     qed

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

   603       by auto

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

   605     proof(rule someI2)

   606       from wq_distinct[OF vt, of cs] eq_wq

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

   608     next

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

   610     qed

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

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

   613     show False by auto

   614   qed

   615 qed

   616 

   617 -- {* A useless definition *}

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

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

   620 

   621 

   622 text {* (* ddd *)

   623   One beauty of our modelling is that we follow the definitional extension tradition of HOL.

   624   The benefit of such a concise and miniature model is that  large number of intuitively 

   625   obvious facts are derived as lemmas, rather than asserted as axioms.

   626 *}

   627 

   628 text {*

   629   However, the lemmas in the forthcoming several locales are no longer 

   630   obvious. These lemmas show how the current precedences should be recalculated 

   631   after every execution step (in our model, every step is represented by an event, 

   632   which in turn, represents a system call, or operation). Each operation is 

   633   treated in a separate locale.

   634 

   635   The complication of current precedence recalculation comes 

   636   because the changing of RAG needs to be taken into account, 

   637   in addition to the changing of precedence. 

   638   The reason RAG changing affects current precedence is that,

   639   according to the definition, current precedence 

   640   of a thread is the maximum of the precedences of its dependants, 

   641   where the dependants are defined in terms of RAG.

   642 

   643   Therefore, each operation, lemmas concerning the change of the precedences 

   644   and RAG are derived first, so that the lemmas about

   645   current precedence recalculation can be based on.

   646 *}

   647 

   648 text {* (* ddd *)

   649   The following locale @{text "step_set_cps"} investigates the recalculation 

   650   after the @{text "Set"} operation.

   651 *}

   652 locale step_set_cps =

   653   fixes s' th prio s 

   654   -- {* @{text "s'"} is the system state before the operation *}

   655   -- {* @{text "s"} is the system state after the operation *}

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

   657   -- {* @{text "s"} is assumed to be a legitimate state, from which

   658          the legitimacy of @{text "s"} can be derived. *}

   659   assumes vt_s: "vt s"

   660 

   661 context step_set_cps 

   662 begin

   663 

   664 interpretation h: pip "s"

   665   by (unfold pip_def, insert vt_s, simp)

   666 

   667 find_theorems 

   668 

   669 (* *)

   670 

   671 text {* (* ddd *)

   672   The following lemma confirms that @{text "Set"}-operating only changes the precedence 

   673   of initiating thread.

   674 *}

   675 

   676 lemma eq_preced:

   677   fixes th'

   678   assumes "th' \<noteq> th"

   679   shows "preced th' s = preced th' s'"

   680 proof -

   681   from assms show ?thesis 

   682     by (unfold s_def, auto simp:preced_def)

   683 qed

   684 

   685 text {* (* ddd *)

   686   The following lemma assures that the resetting of priority does not change the RAG. 

   687 *}

   688 

   689 lemma eq_dep: "RAG s = RAG s'"

   690   by (unfold s_def RAG_set_unchanged, auto)

   691 

   692 text {*

   693   Th following lemma @{text "eq_cp_pre"} circumscribe a rough range of recalculation.

   694   It says, thread other than the initiating thread @{text "th"} does not need recalculation

   695   unless it lies upstream of @{text "th"} in the RAG. 

   696 

   697   The reason behind this lemma is that: 

   698   the change of precedence of one thread can only affect it's upstream threads, according to 

   699   lemma @{text "eq_preced"}. Since the only thread which might change precedence is

   700   @{text "th"}, so only @{text "th"} and its upstream threads need recalculation.

   701   (* ccc *)

   702 *}

   703 

   704 lemma eq_cp_pre:

   705   fixes th' 

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

   707   and nd: "th \<notin> dependants s th'"

   708   shows "cp s th' = cp s' th'"

   709 proof -

   710   -- {* This is what we need to prove after expanding the definition of @{text "cp"} *}

   711   have "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =

   712         Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"

   713    (is "Max (?f1 ` ({th'} \<union> ?A)) = Max (?f2 ` ({th'} \<union> ?B))") 

   714   proof -

   715       -- {* Since RAG is not changed by @{text "Set"}-operation, the dependants of 

   716             any threads are not changed, this is one of key facts underpinning this 

   717             lemma *}

   718       have eq_ab: "?A = ?B" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)

   719       have "(?f1 ` ({th'} \<union> ?A)) =  (?f2 ` ({th'} \<union> ?B))"

   720       proof(rule image_cong)

   721         show "{th'} \<union> ?A = {th'} \<union> ?B" by (simp only:eq_ab)

   722       next  

   723         fix x

   724         assume x_in: "x \<in> {th'} \<union> ?B"

   725         show "?f1 x = ?f2 x"

   726         proof(rule eq_preced) -- {* The other key fact underpinning this lemma is @{text "eq_preced"} *}

   727           from x_in[folded eq_ab, unfolded eq_dependants]

   728           have "x \<in> {th'} \<union> dependants s th'" .

   729           thus "x \<noteq> th"

   730           proof

   731             assume "x \<in> {th'}" 

   732             with `th' \<noteq> th` show ?thesis by simp

   733           next

   734             assume "x \<in> dependants s th'"

   735             with `th \<notin> dependants s th'` show ?thesis by auto

   736           qed 

   737         qed 

   738       qed

   739       thus ?thesis by simp

   740   qed 

   741   thus ?thesis by (unfold cp_eq_cpreced cpreced_def)

   742 qed

   743 

   744 text {*

   745   The following lemma shows that no thread lies upstream of the initiating thread @{text "th"}. 

   746   The reason for this is that only no-blocked thread can initiate 

   747   a system call. Since thread @{text "th"} is non-blocked, it is not waiting for any 

   748   critical resource. Therefore, there is edge leading out of @{text "th"} in the RAG.

   749   Consequently, there is no node (neither resource nor thread) upstream of @{text "th"}.

   750 *}

   751 lemma no_dependants:

   752   shows "th \<notin> dependants s th'"

   753 proof

   754   assume "th \<in> dependants s th'"

   755   from `th \<in> dependants s th'` have "(Th th, Th th') \<in> (RAG s')\<^sup>+"

   756     by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto)

   757   from tranclD[OF this]

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

   759   moreover have "th \<in> readys s'"

   760   proof -

   761     from step_back_step [OF vt_s[unfolded s_def]]

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

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

   764     thus ?thesis by (simp add:readys_def runing_def)

   765   qed

   766   ultimately show "False"

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

   768     by (fold wq_def, blast)

   769 qed

   770 

   771 (* Result improved *)

   772 text {* 

   773   A simple combination of @{text "eq_cp_pre"} and @{text "no_dependants"}

   774   gives the main lemma of this locale, which shows that

   775   only the initiating thread needs a recalculation of current precedence.

   776 *}

   777 lemma eq_cp:

   778   fixes th' 

   779   assumes "th' \<noteq> th"

   780   shows "cp s th' = cp s' th'"

   781   by (rule eq_cp_pre[OF assms no_dependants])

   782 

   783 end

   784 

   785 text {*

   786   The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.

   787 *}

   788 

   789 locale step_v_cps =

   790   -- {* @{text "th"} is the initiating thread *}

   791   -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}

   792   fixes s' th cs s    -- {* @{text "s'"} is the state before operation*}

   793   defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}

   794   -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}

   795   assumes vt_s: "vt s"

   796 

   797 text {*

   798   The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 

   799   which represents the case when there is another thread @{text "th'"}

   800   to take over the critical resource released by the initiating thread @{text "th"}.

   801 *}

   802 locale step_v_cps_nt = step_v_cps +

   803   fixes th'

   804   -- {* @{text "th'"} is assumed to take over @{text "cs"} *}

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

   806 

   807 context step_v_cps_nt

   808 begin

   809 

   810 text {*

   811   Lemma @{text "RAG_s"} confirms the change of RAG:

   812   two edges removed and one added, as shown by the following diagram.

   813 *}

   814 

   815 (*

   816   RAG before the V-operation

   817     th1 ----|

   818             |

   819     th' ----|

   820             |----> cs -----|

   821     th2 ----|              |

   822             |              |

   823     th3 ----|              |

   824                            |------> th

   825     th4 ----|              |

   826             |              |

   827     th5 ----|              |

   828             |----> cs'-----|

   829     th6 ----|

   830             |

   831     th7 ----|

   832 

   833  RAG after the V-operation

   834     th1 ----|

   835             |

   836             |----> cs ----> th'

   837     th2 ----|              

   838             |              

   839     th3 ----|              

   840                            

   841     th4 ----|              

   842             |              

   843     th5 ----|              

   844             |----> cs'----> th

   845     th6 ----|

   846             |

   847     th7 ----|

   848 *)

   849 

   850 lemma RAG_s:

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

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

   853 proof -

   854   from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]

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

   856 qed

   857 

   858 text {*

   859   Lemma @{text "dependants_kept"} shows only @{text "th"} and @{text "th'"}

   860   have their dependants changed.

   861 *}

   862 lemma dependants_kept:

   863   fixes th''

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

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

   866   shows "dependants (wq s) th'' = dependants (wq s') th''"

   867 proof(auto) (* ccc *)

   868   fix x

   869   assume "x \<in> dependants (wq s) th''"

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

   871     by (auto simp:cs_dependants_def eq_RAG)

   872   { fix n

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

   874     proof(induct rule:converse_trancl_induct)

   875       fix y 

   876       assume "(y, Th th'') \<in> RAG s"

   877       with RAG_s neq1 neq2

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

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

   880     next

   881       fix y z 

   882       assume yz: "(y, z) \<in> RAG s"

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

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

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

   886       proof

   887         show "y \<noteq> Cs cs"

   888         proof

   889           assume eq_y: "y = Cs cs"

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

   891           from RAG_s

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

   893           from unique_RAG[OF vt_s this dp_yz] 

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

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

   896           from converse_tranclE[OF this]

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

   898             by (auto simp:s_RAG_def)

   899           with RAG_s have dp': "(Th th', Cs cs') \<in> RAG s'" by auto

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

   901           moreover have "cs' = cs"

   902           proof -

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

   904             have "(Th th', Cs cs) \<in> RAG s'"

   905               by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)

   906             from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']

   907             show ?thesis by simp

   908           qed

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

   910           moreover note wf_trancl[OF wf_RAG[OF vt_s]]

   911           ultimately show False by auto

   912         qed

   913       next

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

   915         proof

   916           assume eq_y: "y = Th th'"

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

   918           with RAG_s have dps': "(Th th', z) \<in> RAG s'" by auto

   919           have "z = Cs cs"

   920           proof -

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

   922             have "(Th th', Cs cs) \<in> RAG s'"

   923               by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)

   924             from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]

   925             show ?thesis .

   926           qed

   927           with dps RAG_s show False by auto

   928         qed

   929       qed

   930       with RAG_s yz have "(y, z) \<in> RAG s'" by auto

   931       with ztp'

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

   933     qed    

   934   }

   935   from this[OF dp]

   936   show "x \<in> dependants (wq s') th''" 

   937     by (auto simp:cs_dependants_def eq_RAG)

   938 next

   939   fix x

   940   assume "x \<in> dependants (wq s') th''"

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

   942     by (auto simp:cs_dependants_def eq_RAG)

   943   { fix n

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

   945     proof(induct rule:converse_trancl_induct)

   946       fix y 

   947       assume "(y, Th th'') \<in> RAG s'"

   948       with RAG_s neq1 neq2

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

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

   951     next

   952       fix y z 

   953       assume yz: "(y, z) \<in> RAG s'"

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

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

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

   957       proof

   958         show "y \<noteq> Cs cs"

   959         proof

   960           assume eq_y: "y = Cs cs"

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

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

   963           proof -

   964             from step_back_step[OF vt_s[unfolded s_def]]

   965             have "(Cs cs, Th th) \<in> RAG s'"

   966               by(cases, auto simp: wq_def s_RAG_def cs_holding_def s_holding_def)

   967             from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]

   968             show ?thesis by simp

   969           qed

   970           from converse_tranclE[OF ztp]

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

   972           moreover 

   973           from step_back_step[OF vt_s[unfolded s_def]]

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

   975           moreover note eq_z

   976           ultimately show False 

   977             by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)

   978         qed

   979       next

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

   981         proof

   982           assume eq_y: "y = Th th'"

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

   984           have "z = Cs cs"

   985           proof -

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

   987             have "(Th th', Cs cs) \<in> RAG s'"

   988               by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)

   989             from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]

   990             show ?thesis .

   991           qed

   992           with ztp have cs_i: "(Cs cs, Th th'') \<in>  (RAG s')\<^sup>+" by simp

   993           from step_back_step[OF vt_s[unfolded s_def]]

   994           have cs_th: "(Cs cs, Th th) \<in> RAG s'"

   995             by(cases, auto simp: s_RAG_def wq_def cs_holding_def s_holding_def)

   996           have "(Cs cs, Th th'') \<notin>  RAG s'"

   997           proof

   998             assume "(Cs cs, Th th'') \<in> RAG s'"

   999             from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]

  1000             and neq1 show "False" by simp

  1001           qed

  1002           with converse_tranclE[OF cs_i]

  1003           obtain u where cu: "(Cs cs, u) \<in> RAG s'"  

  1004             and u_t: "(u, Th th'') \<in> (RAG s')\<^sup>+" by auto

  1005           have "u = Th th"

  1006           proof -

  1007             from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th]

  1008             show ?thesis .

  1009           qed

  1010           with u_t have "(Th th, Th th'') \<in> (RAG s')\<^sup>+" by simp

  1011           from converse_tranclE[OF this]

  1012           obtain v where "(Th th, v) \<in> (RAG s')" by auto

  1013           moreover from step_back_step[OF vt_s[unfolded s_def]]

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

  1015           ultimately show False 

  1016             by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)

  1017         qed

  1018       qed

  1019       with RAG_s yz have "(y, z) \<in> RAG s" by auto

  1020       with ztp'

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

  1022     qed    

  1023   }

  1024   from this[OF dp]

  1025   show "x \<in> dependants (wq s) th''"

  1026     by (auto simp:cs_dependants_def eq_RAG)

  1027 qed

  1028 

  1029 lemma cp_kept:

  1030   fixes th''

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

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

  1033   shows "cp s th'' = cp s' th''"

  1034 proof -

  1035   from dependants_kept[OF neq1 neq2]

  1036   have "dependants (wq s) th'' = dependants (wq s') th''" .

  1037   moreover {

  1038     fix th1

  1039     assume "th1 \<in> dependants (wq s) th''"

  1040     have "preced th1 s = preced th1 s'" 

  1041       by (unfold s_def, auto simp:preced_def)

  1042   }

  1043   moreover have "preced th'' s = preced th'' s'" 

  1044     by (unfold s_def, auto simp:preced_def)

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

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

  1047     by (auto simp:image_def)

  1048   thus ?thesis

  1049     by (unfold cp_eq_cpreced cpreced_def, simp)

  1050 qed

  1051 

  1052 end

  1053 

  1054 locale step_v_cps_nnt = step_v_cps +

  1055   assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"

  1056 

  1057 context step_v_cps_nnt

  1058 begin

  1059 

  1060 lemma nw_cs: "(Th th1, Cs cs) \<notin> RAG s'"

  1061 proof

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

  1063   thus "False"

  1064     apply (auto simp:s_RAG_def cs_waiting_def)

  1065   proof -

  1066     assume h1: "th1 \<in> set (wq s' cs)"

  1067       and h2: "th1 \<noteq> hd (wq s' cs)"

  1068     from step_back_step[OF vt_s[unfolded s_def]]

  1069     show "False"

  1070     proof(cases)

  1071       assume "holding s' th cs" 

  1072       then obtain rest where

  1073         eq_wq: "wq s' cs = th#rest"

  1074         apply (unfold s_holding_def wq_def[symmetric])

  1075         by (case_tac "(wq s' cs)", auto)

  1076       with h1 h2 have ne: "rest \<noteq> []" by auto

  1077       with eq_wq

  1078       have "next_th s' th cs (hd (SOME q. distinct q \<and> set q = set rest))"

  1079         by(unfold next_th_def, rule_tac x = "rest" in exI, auto)

  1080       with nnt show ?thesis by auto

  1081     qed

  1082   qed

  1083 qed

  1084 

  1085 lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"

  1086 proof -

  1087   from nnt and  step_RAG_v[OF vt_s[unfolded s_def], folded s_def]

  1088   show ?thesis by auto

  1089 qed

  1090 

  1091 lemma child_kept_left:

  1092   assumes 

  1093   "(n1, n2) \<in> (child s')^+"

  1094   shows "(n1, n2) \<in> (child s)^+"

  1095 proof -

  1096   from assms show ?thesis 

  1097   proof(induct rule: converse_trancl_induct)

  1098     case (base y)

  1099     from base obtain th1 cs1 th2

  1100       where h1: "(Th th1, Cs cs1) \<in> RAG s'"

  1101       and h2: "(Cs cs1, Th th2) \<in> RAG s'"

  1102       and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)

  1103     have "cs1 \<noteq> cs"

  1104     proof

  1105       assume eq_cs: "cs1 = cs"

  1106       with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp

  1107       with nw_cs eq_cs show False by auto

  1108     qed

  1109     with h1 h2 RAG_s have 

  1110       h1': "(Th th1, Cs cs1) \<in> RAG s" and

  1111       h2': "(Cs cs1, Th th2) \<in> RAG s" by auto

  1112     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)

  1113     with eq_y eq_n2 have "(y, n2) \<in> child s" by simp

  1114     thus ?case by auto

  1115   next

  1116     case (step y z)

  1117     have "(y, z) \<in> child s'" by fact

  1118     then obtain th1 cs1 th2

  1119       where h1: "(Th th1, Cs cs1) \<in> RAG s'"

  1120       and h2: "(Cs cs1, Th th2) \<in> RAG s'"

  1121       and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)

  1122     have "cs1 \<noteq> cs"

  1123     proof

  1124       assume eq_cs: "cs1 = cs"

  1125       with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp

  1126       with nw_cs eq_cs show False by auto

  1127     qed

  1128     with h1 h2 RAG_s have 

  1129       h1': "(Th th1, Cs cs1) \<in> RAG s" and

  1130       h2': "(Cs cs1, Th th2) \<in> RAG s" by auto

  1131     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)

  1132     with eq_y eq_z have "(y, z) \<in> child s" by simp

  1133     moreover have "(z, n2) \<in> (child s)^+" by fact

  1134     ultimately show ?case by auto

  1135   qed