1 theory Test 

     2 imports Precedence_ord Graphs

     3 begin

     4 

     5 type_synonym thread = nat -- {* Type for thread identifiers. *}

     6 type_synonym priority = nat  -- {* Type for priorities. *}

     7 type_synonym cs = nat -- {* Type for critical sections (or resources). *}

     8 

     9 -- {* Schedulling Events *}

    10 

    11 datatype event = 

    12   Create thread priority 

    13 | Exit thread 

    14 | P thread cs 

    15 | V thread cs 

    16 | Set thread priority 

    17 

    18 type_synonym state = "event list"

    19 

    20 fun threads :: "state \<Rightarrow> thread set"

    21   where 

    22   "threads [] = {}" 

    23 | "threads (Create th prio#s) = {th} \<union> threads s" 

    24 | "threads (Exit th # s) = (threads s) - {th}" 

    25 | "threads (_#s) = threads s" 

    26 

    27 fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"

    28   where

    29   "priority th [] = 0" 

    30 | "priority th (Create th' prio#s) = (if th' = th then prio else priority th s)" 

    31 | "priority th (Set th' prio#s) = (if th' = th then prio else priority th s)" 

    32 | "priority th (_#s) = priority th s"

    33 

    34 fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"

    35   where

    36   "last_set th [] = 0" 

    37 | "last_set th ((Create th' prio)#s) = (if (th = th') then length s else last_set th s)" 

    38 | "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" 

    39 | "last_set th (_#s) = last_set th s"

    40 

    41 

    42 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"

    43   where "preced th s \<equiv> Prc (priority th s) (last_set th s)"

    44 

    45 abbreviation 

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

    47  

    48 definition

    49   "holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)"

    50 

    51 definition

    52   "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)"

    53 

    54 --{* Nodes in Resource Graph *}

    55 datatype node = 

    56   Th "thread" 

    57 | Cs "cs" 

    58 

    59 definition

    60   "RAG wq \<equiv> {(Th th, Cs cs) | th cs. waits wq th cs} \<union> {(Cs cs, Th th) | cs th. holds wq th cs}"

    61 

    62 definition

    63   "dependants wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"

    64 

    65 record schedule_state = 

    66   wq_fun :: "cs \<Rightarrow> thread list" 

    67   cprec_fun :: "thread \<Rightarrow> precedence" 

    68 

    69 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"

    70   where 

    71   "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"

    72 

    73 abbreviation

    74   "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"

    75 

    76 abbreviation 

    77   "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"

    78  

    79 abbreviation

    80   "release qs \<equiv> case qs of

    81              [] => [] 

    82           |  (_ # qs) => SOME q. distinct q \<and> set q = set qs"

    83 

    84 lemma [simp]: 

    85   "(SOME q. distinct q \<and> q = []) = []"

    86 by auto

    87 

    88 lemma [simp]: 

    89   "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)"

    90 apply(rule iffI)

    91 apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)+

    92 done

    93 

    94 abbreviation

    95   "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"

    96 

    97 

    98 fun schs :: "state \<Rightarrow> schedule_state"

    99   where 

   100   "schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" 

   101 | "schs (Create th prio # s) = 

   102        (let wq = wq_fun (schs s) in

   103           (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"

   104 |  "schs (Exit th # s) = 

   105        (let wq = wq_fun (schs s) in

   106           (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"

   107 |  "schs (Set th prio # s) = 

   108        (let wq = wq_fun (schs s) in

   109           (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"

   110 |  "schs (P th cs # s) = 

   111        (let wq = wq_fun (schs s) in

   112         let new_wq = wq(cs := (wq cs @ [th])) in

   113           (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"

   114 |  "schs (V th cs # s) = 

   115        (let wq = wq_fun (schs s) in

   116         let new_wq = wq(cs := release (wq cs)) in

   117           (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"

   118 

   119 definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 

   120   where "wq s = wq_fun (schs s)"

   121 

   122 definition cpreced2 :: "state \<Rightarrow> thread \<Rightarrow> precedence"

   123   where "cpreced2 s \<equiv> cprec_fun (schs s)"

   124 

   125 abbreviation

   126   "cpreceds2 s ths \<equiv> {cpreced2 s th | th. th \<in> ths}"

   127 

   128 definition

   129   "holds2 s \<equiv> holds (wq_fun (schs s))"

   130 

   131 definition

   132   "waits2 s \<equiv> waits (wq_fun (schs s))"

   133 

   134 definition

   135   "RAG2 s \<equiv> RAG (wq_fun (schs s))"

   136   

   137 definition

   138   "dependants2 s \<equiv> dependants (wq_fun (schs s))"

   139 

   140 (* ready -> is a thread that is not waiting for any resource *) 

   141 definition readys :: "state \<Rightarrow> thread set"

   142   where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waits2 s th cs)}"

   143 

   144 definition runing :: "state \<Rightarrow> thread set"

   145   where "runing s \<equiv> {th . th \<in> readys s \<and> cpreced2 s th = Max (cpreceds2 s (readys s))}"

   146 

   147 (* all resources a thread hols in a state *)

   148 definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set"

   149   where "holding s th \<equiv> {cs . holds2 s th cs}"

   150 

   151 

   152 lemma exists_distinct:

   153   obtains ys where "distinct ys" "set ys = set xs"

   154 by (metis List.finite_set finite_distinct_list)

   155 

   156 lemma next_to_run_set [simp]:

   157   "wts \<noteq> [] \<Longrightarrow> next_to_run wts \<in> set wts"

   158 apply(rule exists_distinct[of wts])

   159 by (metis (mono_tags, lifting) hd_in_set set_empty some_eq_ex)

   160 

   161 lemma holding_RAG: 

   162   "holding s th = {cs . (Cs cs, Th th) \<in> RAG2 s}"

   163 unfolding holding_def RAG2_def RAG_def

   164 unfolding holds2_def holds_def waits_def

   165 by auto

   166 

   167 inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"

   168   where

   169   step_Create: "\<lbrakk>th \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create th prio)" 

   170 | step_Exit: "\<lbrakk>th \<in> runing s; holding s th = {}\<rbrakk> \<Longrightarrow> step s (Exit th)" 

   171 | step_P: "\<lbrakk>th \<in> runing s;  (Cs cs, Th th)  \<notin> (RAG2 s)^+\<rbrakk> \<Longrightarrow> step s (P th cs)" 

   172 | step_V: "\<lbrakk>th \<in> runing s;  holds2 s th cs\<rbrakk> \<Longrightarrow> step s (V th cs)" 

   173 | step_Set: "\<lbrakk>th \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set th prio)"

   174 

   175 (* valid states *)

   176 inductive vt :: "state \<Rightarrow> bool"

   177   where

   178   vt_nil[intro]: "vt []" 

   179 | vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"

   180 

   181 lemma runing_ready: 

   182   shows "runing s \<subseteq> readys s"

   183   unfolding runing_def readys_def

   184   by auto 

   185 

   186 lemma readys_threads:

   187   shows "readys s \<subseteq> threads s"

   188   unfolding readys_def

   189   by auto

   190 

   191 lemma wq_threads: 

   192   assumes vt: "vt s"

   193   and h: "th \<in> set (wq s cs)"

   194   shows "th \<in> threads s"

   195 using assms

   196 apply(induct)

   197 apply(simp add: wq_def)

   198 apply(erule step.cases)

   199 apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def)

   200 apply(simp add: waits_def)

   201 apply(auto simp add: waits_def split: if_splits)[1]

   202 apply(auto split: if_splits)

   203 apply(simp only: waits_def)

   204 by (metis insert_iff set_simps(2))

   205 

   206 

   207 

   208 lemma Domain_RAG_threads:

   209   assumes vt: "vt s"

   210   and in_dom: "(Th th) \<in> Domain (RAG2 s)"

   211   shows "th \<in> threads s"

   212 proof -

   213   from in_dom obtain n where "(Th th, n) \<in> RAG2 s" by auto

   214   then obtain cs where "n = Cs cs" "(Th th, Cs cs) \<in> RAG2 s"  

   215     unfolding RAG2_def RAG_def by auto

   216   then have "th \<in> set (wq s cs)"

   217     unfolding wq_def RAG_def RAG2_def waits_def by auto

   218   with wq_threads [OF vt] show ?thesis .

   219 qed

   220 

   221 lemma dependants_threads:

   222   assumes vt: "vt s"

   223   shows "dependants2 s th \<subseteq> threads s"

   224 proof

   225   fix th1 

   226   assume "th1 \<in> dependants2 s th"

   227   then have h: "(Th th1, Th th) \<in> (RAG2 s)\<^sup>+"

   228     unfolding dependants2_def dependants_def RAG2_def by simp

   229   then have "Th th1 \<in> Domain ((RAG2 s)\<^sup>+)" unfolding Domain_def by auto

   230   then have "Th th1 \<in> Domain (RAG2 s)" using trancl_domain by simp

   231   then show "th1 \<in> threads s" using vt by (rule_tac Domain_RAG_threads)

   232 qed

   233 

   234 lemma finite_threads:

   235   assumes vt: "vt s"

   236   shows "finite (threads s)"

   237 using vt by (induct) (auto elim: step.cases)

   238 

   239 

   240 section {* Distinctness of @{const wq} *}

   241 

   242 lemma wq_distinct_step: 

   243   assumes "step s e" "distinct (wq s cs)" 

   244   shows "distinct (wq (e # s) cs)"

   245 using assms

   246 unfolding wq_def

   247 apply(erule_tac step.cases)

   248 apply(auto simp add: RAG2_def RAG_def Let_def)[1]

   249 apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def)

   250 apply(auto split: list.split)

   251 apply(rule someI2)

   252 apply(auto)

   253 done

   254 

   255 lemma wq_distinct: 

   256   assumes "vt s" 

   257   shows "distinct (wq s cs)"

   258 using assms

   259 apply(induct)

   260 apply(simp add: wq_def)

   261 apply(simp add: wq_distinct_step)

   262 done

   263 

   264 

   265 section {* Single_Valuedness of @{const waits2}, @{const holds2}, @{const RAG2} *}

   266 

   267 lemma waits2_unique:

   268   assumes "vt s"

   269   and "waits2 s th cs1"

   270   and "waits2 s th cs2"

   271   shows "cs1 = cs2"

   272 using assms

   273 apply(induct)

   274 apply(simp add: waits2_def waits_def)

   275 apply(erule step.cases)

   276 apply(auto simp add: Let_def waits2_def waits_def holds_def RAG2_def RAG_def 

   277  readys_def runing_def split: if_splits)

   278 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list)

   279 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list)

   280 apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)

   281 by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)

   282 

   283 lemma single_valued_waits2:

   284   assumes "vt s"

   285   shows "single_valuedP (waits2 s)"

   286 using assms

   287 unfolding single_valued_def

   288 by (simp add: Product_Type.Collect_case_prodD waits2_unique)

   289 

   290 lemma single_valued_holds2:

   291   assumes "vt s"

   292   shows "single_valuedP (\<lambda>cs th. holds2 s th cs)"

   293 unfolding single_valued_def holds2_def holds_def by simp

   294 

   295 lemma single_valued_RAG2:

   296   assumes "vt s"

   297   shows "single_valued (RAG2 s)"

   298 using single_valued_waits2[OF assms] single_valued_holds2[OF assms] 

   299 unfolding RAG2_def RAG_def

   300 apply(rule_tac single_valued_union)

   301 unfolding holds2_def[symmetric] waits2_def[symmetric]

   302 apply(rule single_valued_Collect)

   303 apply(simp)

   304 apply(simp add: inj_on_def)

   305 apply(rule single_valued_Collect)

   306 apply(simp)

   307 apply(simp add: inj_on_def)

   308 apply(auto)

   309 done

   310 

   311 

   312 section {* Properties of @{const RAG2} under events *}

   313 

   314 lemma RAG_Set [simp]: 

   315   shows "RAG2 (Set th prio # s) = RAG2 s"

   316 unfolding RAG2_def

   317 by (simp add: Let_def)

   318 

   319 lemma RAG_Create [simp]: 

   320   "RAG2 (Create th prio # s) = RAG2 s"

   321 unfolding RAG2_def

   322 by (simp add: Let_def)

   323 

   324 lemma RAG_Exit [simp]: 

   325   shows "RAG2 (Exit th # s) = RAG2 s"

   326 unfolding RAG2_def

   327 by (simp add: Let_def)

   328 

   329 lemma RAG_P1:

   330   assumes "wq s cs = []"

   331   shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Cs cs, Th th)}"

   332 using assms

   333 unfolding  RAG2_def RAG_def wq_def Let_def waits_def holds_def

   334 by (auto simp add: Let_def)

   335 

   336 lemma RAG_P2:

   337   assumes "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []"

   338   shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Th th, Cs cs)}"

   339 using assms

   340 unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def

   341 by (auto simp add: Let_def)

   342 

   343 

   344 lemma RAG_V1:

   345 assumes vt: "wq s cs = [th]"

   346 shows "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}"

   347 using assms

   348 unfolding RAG2_def RAG_def waits_def holds_def wq_def

   349 by (auto simp add: Let_def)

   350 

   351 lemma RAG_V2:

   352 assumes vt:"vt s" "wq s cs = th # wts \<and> wts \<noteq> []"

   353 shows "RAG2 (V th cs # s) \<subseteq>

   354   RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}"

   355 unfolding RAG2_def RAG_def waits_def holds_def

   356 using assms wq_distinct[OF vt(1), of"cs"]

   357 by (auto simp add: Let_def wq_def)

   358 

   359 

   360 

   361 section {* Acyclicity of @{const RAG2} *}

   362 

   363 lemma acyclic_RAG_step: 

   364   assumes vt: "vt s"

   365   and     stp: "step s e"

   366   and     ac: "acyclic (RAG2 s)"

   367   shows "acyclic (RAG2 (e # s))"

   368 using stp vt ac

   369 proof (induct)

   370   case (step_P th s cs)

   371   have ac: "acyclic (RAG2 s)" by fact

   372   have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact

   373   { assume wq_empty: "wq s cs = []" -- "case waiting queue is empty"

   374     then have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>+"

   375     proof (rule_tac notI)

   376       assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+"

   377       then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis 

   378       with wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def)

   379     qed

   380     with ac have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp

   381     then have "acyclic (RAG2 (P th cs # s))" using RAG_P1[OF wq_empty] 

   382       by (rule acyclic_subset)

   383   }

   384   moreover

   385   { assume wq_not_empty: "wq s cs \<noteq> []" -- "case waiting queue is not empty"

   386     from ac ds

   387     have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by simp

   388     then have "acyclic (RAG2 (P th cs # s))" using RAG_P2[OF ds wq_not_empty] 

   389       by (rule acyclic_subset)

   390   }

   391   ultimately show "acyclic (RAG2 (P th cs # s))" by metis

   392 next    

   393   case (step_V th s cs) -- "case for release of a lock" 

   394   have vt: "vt s" by fact

   395   have ac: "acyclic (RAG2 s)" by fact

   396   have hd: "holds2 s th cs" by fact

   397   from vt have wq_distinct:"distinct (wq s cs)" by (rule wq_distinct)

   398   from hd have "th \<in> set (wq s cs)" "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto

   399   then obtain wts where eq_wq: "wq s cs = th # wts"  by (cases "wq s cs") (auto)

   400   -- "case no thread present in the waiting queue to take over"

   401   { assume "wts = []" 

   402     with eq_wq have "wq s cs = [th]" by simp

   403     then have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" by (rule RAG_V1)

   404     moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset)

   405     ultimately 

   406     have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)

   407   }

   408   moreover

   409   -- "at least one thread present to take over"

   410   { def nth \<equiv> "next_to_run wts"

   411     assume wq_not_empty: "wts \<noteq> []" 

   412     have "waits2 s nth cs" 

   413       using eq_wq wq_not_empty wq_distinct

   414       unfolding nth_def waits2_def waits_def wq_def[symmetric] by auto

   415     then have cs_in_RAG: "(Th nth, Cs cs) \<in> RAG2 s" 

   416       unfolding RAG2_def RAG_def waits2_def by auto

   417     have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}" 

   418       unfolding nth_def using  vt wq_not_empty eq_wq by (rule_tac RAG_V2) (auto)

   419     moreover 

   420     have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)})" 

   421     proof -

   422       have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset)

   423       moreover 

   424       have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+" 

   425       proof (rule notI)

   426         assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+"

   427         then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})"

   428           by (metis converse_tranclE)

   429         then have "(Th nth, z) \<in> RAG2 s" by simp

   430         then have "z = Cs cs" using cs_in_RAG single_valued_RAG2[OF vt]

   431           by (simp add: single_valued_def)

   432         then show "False" using a by simp

   433       qed

   434       ultimately 

   435       show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth) })" by simp

   436     qed

   437     ultimately have "acyclic (RAG2 (V th cs # s))" 

   438       by (rule_tac acyclic_subset)

   439   }

   440   ultimately show "acyclic (RAG2 (V th cs # s))" by metis

   441 qed (simp_all)

   442 

   443 

   444 lemma finite_RAG:

   445   assumes "vt s"

   446   shows "finite (RAG2 s)"

   447 using assms

   448 apply(induct)

   449 apply(simp add: RAG2_def RAG_def waits_def holds_def)

   450 apply(erule step.cases)

   451 apply(auto)

   452 apply(case_tac "wq sa cs = []")

   453 apply(rule finite_subset)

   454 apply(rule RAG_P1)

   455 apply(simp)

   456 apply(simp)

   457 apply(rule finite_subset)

   458 apply(rule RAG_P2)

   459 apply(simp)

   460 apply(simp)

   461 apply(simp)

   462 apply(subgoal_tac "\<exists>wts. wq sa cs = th # wts")

   463 apply(erule exE)

   464 apply(case_tac "wts = []")

   465 apply(rule finite_subset)

   466 apply(rule RAG_V1)

   467 apply(simp)

   468 apply(simp)

   469 apply(rule finite_subset)

   470 apply(rule RAG_V2)

   471 apply(simp)

   472 apply(simp)

   473 apply(simp)

   474 apply(subgoal_tac "th \<in> set (wq sa cs) \<and> th = hd (wq sa cs)") 

   475 apply(case_tac "wq sa cs") 

   476 apply(auto)[2]

   477 apply(auto simp add: holds2_def holds_def wq_def)

   478 done

   479 

   480 

   481 

   482 lemma dchain_unique:

   483   assumes vt: "vt s"

   484   and th1_d: "(n, Th th1) \<in> (RAG2 s)^+"

   485   and th1_r: "th1 \<in> readys s"

   486   and th2_d: "(n, Th th2) \<in> (RAG2 s)^+"

   487   and th2_r: "th2 \<in> readys s"

   488   shows "th1 = th2"

   489 proof(rule ccontr)

   490   assume neq: "th1 \<noteq> th2"

   491    with single_valued_confluent2 [OF single_valued_RAG2 [OF vt]] th1_d th2_d

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

   493   moreover

   494   { assume "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+"      

   495     then obtain n where dd: "(Th th1, n) \<in> RAG2 s" by (metis converse_tranclE)

   496     then obtain cs where eq_n: "n = Cs cs"

   497       unfolding RAG2_def RAG_def by (case_tac n) (auto)

   498     from dd eq_n have "th1 \<notin> readys s"

   499       unfolding RAG2_def RAG_def waits2_def readys_def by (auto)

   500     with th1_r have "False" by auto

   501   }

   502   moreover

   503   { assume "(Th th2, Th th1) \<in> (RAG2 s)\<^sup>+"

   504     then obtain n where dd: "(Th th2, n) \<in> RAG2 s" by (metis converse_tranclE)

   505     then obtain cs where eq_n: "n = Cs cs"

   506       unfolding RAG2_def RAG_def by (case_tac n) (auto)

   507     from dd eq_n have "th2 \<notin> readys s"

   508       unfolding RAG2_def RAG_def waits2_def readys_def by (auto)

   509     with th2_r have "False" by auto

   510   }

   511   ultimately show "False" by metis

   512 qed

   513 

   514 lemma cpreced2_cpreced: "cpreced2 s th = cpreced (wq s) s th"

   515 unfolding cpreced2_def wq_def

   516 apply(induct s rule: schs.induct)

   517 apply(simp add: Let_def cpreced_def dependants_def RAG_def waits_def holds_def preced_def)

   518 apply(simp add: Let_def)

   519 apply(simp add: Let_def)

   520 apply(simp add: Let_def)

   521 apply(subst (2) schs.simps)

   522 apply(simp add: Let_def)

   523 apply(subst (2) schs.simps)

   524 apply(simp add: Let_def)

   525 done

   526 

   527 lemma cpreced_Exit:

   528   shows "cpreced2 (Exit th # s) th' = cpreced2 s th'"

   529 by (simp add: cpreced2_cpreced cpreced_def preced_def wq_def Let_def)

   530 

   531 lemma readys_Exit:

   532   shows "readys (Exit th # s) = readys s - {th}"

   533 by (auto simp add: readys_def waits2_def Let_def)

   534 

   535 lemma readys_Create:

   536   shows "readys (Create th prio # s) \<subseteq> {th} \<union> readys s"

   537 apply (auto simp add: readys_def waits2_def Let_def waits_def)

   538 done

   539 

   540 lemma readys_Set:

   541   shows "readys (Set th prio # s) = readys s"

   542 by (auto simp add: readys_def waits2_def Let_def)

   543 

   544 

   545 lemma readys_P:

   546   shows "readys (P th cs # s) \<subseteq> readys s"

   547 apply(auto simp add: readys_def waits2_def Let_def)

   548 apply(simp add: waits_def)

   549 apply(case_tac "csa = cs")

   550 apply(simp)

   551 apply(drule_tac x="cs" in spec)

   552 apply(simp)

   553 apply (metis hd_append2 in_set_insert insert_Nil list.sel(1))

   554 apply(drule_tac x="csa" in spec)

   555 apply(simp)

   556 done

   557 

   558 lemma readys_V:

   559   shows "readys (V th cs # s) \<subseteq> readys s \<union> set (wq s cs)"

   560 apply(auto simp add: readys_def waits2_def waits_def Let_def wq_def)

   561 done

   562 

   563 

   564 fun the_th :: "node \<Rightarrow> thread"

   565   where "the_th (Th th) = th"

   566 

   567 lemma image_Collect2:

   568   "f ` A = {f x | x. x \<in> A}"

   569 apply(auto)

   570 done

   571 

   572 lemma Collect_disj_eq2:

   573   "{f x | x. x = y \<or> x \<in> A} = {f y} \<union> {f x | x. x \<in> A}"

   574 by (auto)

   575 

   576 lemma last_set_lt: 

   577   "th \<in> threads s \<Longrightarrow> last_set th s < length s"

   578   apply(induct rule: threads.induct)

   579   apply(auto)

   580   done

   581 

   582 lemma last_set_eq_iff: 

   583   assumes "th1 \<in> threads s" "th2 \<in> threads s"

   584   shows "last_set th1 s = last_set th2 s \<longleftrightarrow> th1 = th2"

   585   using assms

   586   apply(induct s rule: threads.induct) 

   587   apply(auto split:if_splits dest:last_set_lt)

   588   done

   589 

   590 lemma preced_eq_iff: 

   591   assumes th_in1: "th1 \<in> threads s"

   592   and th_in2: "th2 \<in> threads s"

   593   shows "preced th1 s = preced th2 s \<longleftrightarrow> th1 = th2"

   594 using assms

   595 by (auto simp add: preced_def last_set_eq_iff)

   596 

   597 lemma dm_RAG_threads:

   598   assumes vt: "vt s"

   599   and in_dom: "(Th th) \<in> Domain (RAG2 s)"

   600   shows "th \<in> threads s"

   601 proof -

   602   from in_dom obtain n where a: "(Th th, n) \<in> RAG2 s" by auto

   603   then obtain cs where "n = Cs cs" 

   604     unfolding RAG2_def RAG_def

   605     by auto

   606   then have "(Th th, Cs cs) \<in> RAG2 s" using a by simp

   607   hence "th \<in> set (wq s cs)"

   608     unfolding RAG2_def wq_def RAG_def waits_def

   609     by (auto)

   610   then show ?thesis

   611     apply(rule_tac wq_threads)

   612     apply(rule assms)

   613     apply(simp)

   614     done

   615 qed

   616 

   617 lemma cpreced_eq_iff:

   618   assumes "th1 \<in> readys s" "th2 \<in> readys s" "vt s"

   619   shows "cpreced2 s th1 = cpreced2 s th2 \<longleftrightarrow> th1 = th2" 

   620 proof 

   621   def S1\<equiv>"({th1} \<union> dependants (wq s) th1)"

   622   def S2\<equiv>"({th2} \<union> dependants (wq s) th2)"

   623   have fin: "finite ((the_th o fst) ` ((RAG (wq s))\<^sup>+))" 

   624       apply(rule)

   625       apply(simp add: finite_trancl)

   626       apply(simp add: wq_def)

   627       apply(rule finite_RAG[simplified RAG2_def])

   628       apply(rule assms)

   629       done

   630 

   631   from fin have h: "finite (preceds s S1)" "finite (preceds s S2)"

   632       apply(simp_all add: S2_def S1_def Collect_disj_eq2 image_Collect[symmetric])

   633       apply(rule)

   634       apply(simp add: dependants_def)  

   635       apply(rule rev_finite_subset)

   636       apply(assumption)

   637       apply(auto simp add: image_def)[1]

   638       apply(metis fst_conv the_th.simps)

   639       apply(rule)

   640       apply(simp add: dependants_def)  

   641       apply(rule rev_finite_subset)

   642       apply(assumption)

   643       apply(auto simp add: image_def)[1]

   644       apply(metis fst_conv the_th.simps)

   645       done

   646     moreover have "S1 \<noteq> {}" "S2 \<noteq> {}" by (simp_all add: S1_def S2_def)

   647     then have "(preceds s S1) \<noteq> {}" "(preceds s S2) \<noteq> {}" by simp_all

   648     ultimately have m: "Max (preceds s S1) \<in> (preceds s S1)" "Max (preceds s S2) \<in> (preceds s S2)"

   649       apply(rule_tac [!] Max_in)

   650       apply(simp_all)

   651       done

   652 

   653   assume q: "cpreced2 s th1 = cpreced2 s th2"

   654   then have eq_max: "Max (preceds s S1) = Max (preceds s S2)"

   655     unfolding cpreced2_cpreced cpreced_def

   656     apply(simp only: S1_def S2_def)

   657     apply(simp add: Collect_disj_eq2)

   658     done

   659  

   660   obtain th0 where th0_in: "th0 \<in> S1" "th0 \<in> S2" and 

   661       eq_f_th1: "preced th0 s = Max (preceds s S1)"

   662                 "preced th0 s = Max (preceds s S2)"

   663     using m 

   664       apply(clarify)

   665       apply(simp add: eq_max)

   666       apply(subst (asm) (2)  preced_eq_iff)

   667       apply(insert assms(2))[1]

   668       apply(simp add: S2_def)

   669       apply(auto)[1]

   670       apply (metis contra_subsetD readys_threads)

   671       apply(simp add: dependants_def)

   672       apply(subgoal_tac "Th tha \<in> Domain ((RAG2 s)^+)")

   673       apply(simp add: trancl_domain)

   674       apply (metis Domain_RAG_threads assms(3))

   675       apply(simp only: RAG2_def wq_def)

   676       apply (metis Domain_iff)

   677       apply(insert assms(1))[1]

   678       apply(simp add: S1_def)

   679       apply(auto)[1]

   680       apply (metis contra_subsetD readys_threads)

   681       apply(simp add: dependants_def)

   682       apply(subgoal_tac "Th th \<in> Domain ((RAG2 s)^+)")

   683       apply(simp add: trancl_domain)

   684       apply (metis Domain_RAG_threads assms(3))

   685       apply(simp only: RAG2_def wq_def)

   686       apply (metis Domain_iff)

   687       apply(simp)

   688     done

   689   then show "th1 = th2"

   690     apply -

   691     apply(insert th0_in assms(1, 2))[1]

   692     apply(simp add: S1_def S2_def)

   693     apply(auto)

   694     --"first case"

   695     prefer 2

   696     apply(subgoal_tac "Th th2 \<in> Domain (RAG2 s)")

   697     apply(subgoal_tac "\<exists>cs. (Th th2, Cs cs) \<in> RAG2 s")

   698     apply(erule exE)

   699     apply(simp add: runing_def RAG2_def RAG_def readys_def waits2_def)[1]

   700     apply(auto simp add: RAG2_def RAG_def)[1]

   701     apply(subgoal_tac "Th th2 \<in> Domain ((RAG2 s)^+)")

   702     apply (metis trancl_domain)

   703     apply(subgoal_tac "(Th th2, Th th1) \<in> (RAG2 s)^+")

   704     apply (metis Domain_iff)

   705     apply(simp add: dependants_def RAG2_def wq_def)

   706     --"second case"

   707     apply(subgoal_tac "Th th1 \<in> Domain (RAG2 s)")

   708     apply(subgoal_tac "\<exists>cs. (Th th1, Cs cs) \<in> RAG2 s")

   709     apply(erule exE)

   710     apply(insert assms(1))[1]

   711     apply(simp add: runing_def RAG2_def RAG_def readys_def waits2_def)[1]

   712     apply(auto simp add: RAG2_def RAG_def)[1]

   713     apply(subgoal_tac "Th th1 \<in> Domain ((RAG2 s)^+)")

   714     apply (metis trancl_domain)

   715     apply(subgoal_tac "(Th th1, Th th2) \<in> (RAG2 s)^+")

   716     apply (metis Domain_iff)

   717     apply(simp add: dependants_def RAG2_def wq_def)

   718     --"third case"

   719     apply(rule dchain_unique)

   720     apply(rule assms(3))

   721     apply(simp add: dependants_def RAG2_def wq_def)

   722     apply(simp)

   723     apply(simp add: dependants_def RAG2_def wq_def)

   724     apply(simp)

   725     done

   726 next

   727   assume "th1 = th2"

   728   then show "cpreced2 s th1 = cpreced2 s th2" by simp

   729 qed

   730 

   731 lemma at_most_one_running:

   732   assumes "vt s"

   733   shows "card (runing s) \<le> 1"

   734 proof (rule ccontr)

   735   assume "\<not> card (runing s) \<le> 1"

   736   then have "2 \<le> card (runing s)" by auto

   737   moreover 

   738   have "finite (runing s)"

   739     by (metis `\<not> card (runing s) \<le> 1` card_infinite le0)

   740   ultimately obtain th1 th2 where a: 

   741     "th1 \<noteq> th2" "th1 \<in> runing s" "th2 \<in> runing s" 

   742     "cpreced2 s th1 = cpreced2 s th2" 

   743     apply(auto simp add: numerals card_le_Suc_iff runing_def) 

   744     apply(blast)

   745     done

   746   then have "th1 = th2"

   747     apply(subst (asm) cpreced_eq_iff)

   748     apply(auto intro: assms a)

   749     apply (metis contra_subsetD runing_ready)+

   750     done

   751   then show "False" using a(1) by auto

   752 qed

   753 

   754 

   755 

   756   (*

   757   obtain th0 where th0_in: "th0 \<in> S1 \<and> th0 \<in> S2" 

   758     and eq_f_th0: "preced th0 s = Max ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"

   759   proof -

   760     from fin have h1: "finite ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"

   761       apply(simp only: S1_def S2_def)

   762       apply(rule)

   763       apply(rule)

   764       apply(rule)

   765       apply(simp add: dependants_def) 

   766       apply(rule rev_finite_subset)

   767       apply(assumption)

   768       apply(auto simp add: image_def)

   769       apply (metis fst_conv the_th.simps)

   770       done

   771     moreover 

   772     have "S1 \<inter> S2 \<noteq> {}" apply (simp add: S1_def S2_def) 

   773       apply(auto) 

   774       

   775       done

   776     then have h2: "((\<lambda>th. preced th s) ` (S1 \<union> S2)) \<noteq> {}" by simp

   777     ultimately have "Max ((\<lambda>th. preced th s) ` (S1 \<union> S2)) \<in> ((\<lambda>th. preced th s) ` (S1 \<union> S2))"

   778       apply(rule Max_in)

   779       done

   780     then show ?thesis using that[intro] apply(auto) 

   781       

   782       apply(erule_tac preced_unique)

   783       done

   784   qed

   785   *)

   786 

   787 thm waits_def waits2_def

   788 

   789 end