Mercurial Mercurial > hg > pip / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Correctness.thy
changeset 138 20c1d3a14143
parent 137 785c0f6b8184
child 140 389ef8b1959c
equal deleted inserted replaced
137:785c0f6b8184 138:20c1d3a14143 
     3 begin
 
     3 begin
 
     4 
     4 
     5 text {* 
     5 text {* 
     6   The following two auxiliary lemmas are used to reason about @{term Max}.
 
     6   The following two auxiliary lemmas are used to reason about @{term Max}.
 
     7 *}
 
     7 *}
 
       
     8 
       
     9 lemma subset_Max:
 
       
    10   assumes "finite A"
 
       
    11   and "B \<subseteq> A"
 
       
    12   and "c \<in> B"
 
       
    13   and "Max A = c"
 
       
    14 shows "Max B = c"
 
       
    15 using Max.subset assms
 
       
    16 by (metis Max.coboundedI Max_eqI rev_finite_subset subset_eq)
 
       
    17 
       
    18 
     8 lemma image_Max_eqI: 
    19 lemma image_Max_eqI: 
     9   assumes "finite B"
 
    20   assumes "finite B"
 
    10   and "b \<in> B"
 
    21   and "b \<in> B"
 
    11   and "\<forall> x \<in> B. f x \<le> f b"
 
    22   and "\<forall> x \<in> B. f x \<le> f b"
 
    12   shows "Max (f ` B) = f b"
 
    23   shows "Max (f ` B) = f b"
 
    99 
   110 
   100 end
 
   111 end
 
   101 
   112 
   102 locale extend_highest_gen = highest_gen + 
   113 locale extend_highest_gen = highest_gen + 
   103   fixes t 
   114   fixes t 
   104   assumes vt_t: "vt (t@s)"
 
   115   assumes vt_t: "vt (t @ s)"
 
   105   and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"
 
   116   and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"
 
   106   and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
 
   117   and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
 
   107   and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
 
   118   and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
 
   108 
   119 
   109 sublocale extend_highest_gen < vat_t?: valid_trace "t@s"
 
   120 sublocale extend_highest_gen < vat_t?: valid_trace "t@s"
 
   129       qed
 
   140       qed
 
   130     qed
 
   141     qed
 
   131   qed
 
   142   qed
 
   132 qed
 
   143 qed
 
   133 
   144 
   134 (* locale red_extend_highest_gen = extend_highest_gen +
 
       
   135    fixes i::nat
 
       
   136 *)
 
       
   137 
       
   138 (*
 
       
   139 sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"
 
       
   140   apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
 
       
   141   apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
 
       
   142   by (unfold highest_gen_def, auto dest:step_back_vt_app)
 
       
   143 *)
 
       
   144 
   145 
   145 context extend_highest_gen
 
   146 context extend_highest_gen
 
   146 begin
 
   147 begin
 
   147 
   148 
   148  lemma ind [consumes 0, case_names Nil Cons, induct type]:
 
   149  lemma ind [consumes 0, case_names Nil Cons, induct type]:
 
   181   qed
 
   182   qed
 
   182 qed
 
   183 qed
 
   183 
   184 
   184 
   185 
   185 lemma th_kept: "th \<in> threads (t @ s) \<and> 
   186 lemma th_kept: "th \<in> threads (t @ s) \<and> 
   186                  preced th (t@s) = preced th s" (is "?Q t") 
   187                 preced th (t @ s) = preced th s" (is "?Q t") 
   187 proof -
 
   188 proof -
 
   188   show ?thesis
 
   189   show ?thesis
 
   189   proof(induct rule:ind)
 
   190   proof(induct rule:ind)
 
   190     case Nil
 
   191     case Nil
 
   191     from threads_s
 
   192     from threads_s
 
   244     qed
 
   245     qed
 
   245   qed
 
   246   qed
 
   246 qed
 
   247 qed
 
   247 
   248 
   248 text {*
 
   249 text {*
 
   249   According to @{thm th_kept}, thread @{text "th"} has its living status
 
   250   According to @{thm th_kept}, thread @{text "th"} has its liveness status
 
   250   and precedence kept along the way of @{text "t"}. The following lemma
 
   251   and precedence kept along the way of @{text "t"}. The following lemma
 
   251   shows that this preserved precedence of @{text "th"} remains as the highest
 
   252   shows that this preserved precedence of @{text "th"} remains as the highest
 
   252   along the way of @{text "t"}.
 
   253   along the way of @{text "t"}.
 
   253 
   254 
   254   The proof goes by induction over @{text "t"} using the specialized
 
   255   The proof goes by induction over @{text "t"} using the specialized
 
   258 
   259 
   259   The very essence is to show that precedences, no matter whether they 
   260   The very essence is to show that precedences, no matter whether they 
   260   are newly introduced or modified, are always lower than the one held 
   261   are newly introduced or modified, are always lower than the one held 
   261   by @{term "th"}, which by @{thm th_kept} is preserved along the way.
 
   262   by @{term "th"}, which by @{thm th_kept} is preserved along the way.
 
   262 *}
 
   263 *}
 
   263 lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
 
   264 lemma max_kept: 
       
   265   shows "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
 
   264 proof(induct rule:ind)
 
   266 proof(induct rule:ind)
 
   265   case Nil
 
   267   case Nil
 
   266   from highest_preced_thread
 
   268   from highest_preced_thread
 
   267   show ?case by simp
 
   269   show ?case by simp
 
   268 next
 
   270 next
 
   721   there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 
   723   there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 
   722   in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
 
   724   in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
 
   723 
   725 
   724   Now, since @{term readys}-set is non-empty, there must be
 
   726   Now, since @{term readys}-set is non-empty, there must be
 
   725   one in it which holds the highest @{term cp}-value, which, by definition, 
   727   one in it which holds the highest @{term cp}-value, which, by definition, 
   726   is the @{term running}-thread. However, we are going to show more: this running thread
 
   728   is the @{term running}-thread. However, we are going to show more: this 
   727   is exactly @{term "th'"}.
 
   729   running thread is exactly @{term "th'"}. *}
 
   728      *}
 
   730 
       
   731 
       
   732 (*
 
   729 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
 
   733 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
 
   730   assumes "th \<notin> running (t @ s)"
 
   734   assumes "th \<notin> running (t @ s)"
 
   731   obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
 
   735   obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
 
   732                     "th' \<in> running (t @ s)"
 
   736                     "th' \<in> running (t @ s)"
 
   733 proof -
 
   737 proof -
 
   742   moreover have "th \<notin> readys (t @ s)" 
   746   moreover have "th \<notin> readys (t @ s)" 
   743     using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto 
   747     using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto 
   744   
   748   
   745   -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in 
   749   -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in 
   746         term @{term readys}: *}
 
   750         term @{term readys}: *}
 
   747   ultimately obtain th' where th'_in: "th' \<in> readys (t @ s)"
 
   751   ultimately obtain th' where th'_readys: "th' \<in> readys (t @ s)"
 
   748                           and dp: "(th, th') \<in> (tG (t @ s))\<^sup>+" by auto
 
   752                           and dp: "(th, th') \<in> (tG (t @ s))\<^sup>+" by auto
 
   749 
   753 
       
   754   -- {* @{text "th'"} is an ancestor of @{term "th"} *}
 
       
   755   have "th' \<in> ancestors (tG (t @ s)) th" using dp
 
       
   756     unfolding ancestors_def by simp
 
       
   757 
       
   758   moreover
 
   750   -- {* We are going to show that this @{term th'} is running. *}
 
   759   -- {* We are going to show that this @{term th'} is running. *}
 
   751   have "th' \<in> running (t @ s)"
 
   760   have "th' \<in> running (t @ s)"
 
   752   proof -
 
   761   proof -
 
   753     -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
 
   762     -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
 
   754     have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t@s))" (is "?L = ?R")
 
   763     have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t@s))" (is "?L = ?R")
 
       
   764     proof -
 
       
   765       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
 
       
   766             the  @{term cp}-value of @{term th'} is the maximum of 
       
   767             all precedences of all thread nodes in its @{term tRAG}-subtree: *}
 
       
   768       
       
   769       have "?L =  Max (preceds (subtree (tG (t @ s)) th') (t @ s))"
 
       
   770             unfolding cp_alt_def2 image_def the_preced_def by meson 
       
   771       also have "... = (preced th (t @ s))"
 
       
   772       thm subset_Max
 
       
   773       thm preced_unique
 
       
   774       proof(rule subset_Max[where ?A="preceds (threads (t @ s)) (t @ s)"])
 
       
   775         show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
 
       
   776       next
 
       
   777         have "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"
 
       
   778           using readys_def th'_readys vat_t.subtree_tG_thread by auto 
       
   779         then show "preceds (subtree (tG (t @ s)) th') (t @ s) \<subseteq> preceds (threads (t @ s)) (t @ s)"
 
       
   780           by auto
 
       
   781       next
 
       
   782         have "th \<in> subtree (tG (t @ s)) th'"
 
       
   783           by (simp add: dp subtree_def trancl_into_rtrancl)   
       
   784         then show " preced th (t @ s) \<in> preceds (subtree (tG (t @ s)) th') (t @ s)"
 
       
   785           by blast
 
       
   786       next
 
       
   787         have "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
 
       
   788           apply(simp only: the_preced_def)
 
       
   789           by simp 
       
   790         show "Max (preceds (threads (t @ s)) (t @ s)) = preced th (t @ s)"
 
       
   791           thm th_kept max_kept
 
       
   792           apply(simp del: th_kept)
 
       
   793           apply(simp only: the_preced_def image_def)
 
       
   794           apply(simp add: Bex_def_raw)
 
       
   795           
       
   796       qed
 
       
   797       also have "... = ?R"
 
       
   798         using th_cp_max th_cp_preced th_kept 
       
   799               the_preced_def vat_t.max_cp_readys_threads by auto
 
       
   800       finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
 
       
   801     qed 
       
   802 
       
   803     -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
       
   804           it is @{term running} by definition. *}
 
       
   805     then show "th' \<in> running (t @ s)" using th'_readys 
       
   806       unfolding running_def by simp
 
       
   807   qed
 
       
   808 
       
   809   ultimately show ?thesis using that by metis
 
       
   810 qed
 
       
   811 *)
 
       
   812 
       
   813 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
 
       
   814   obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
 
       
   815                     "th' \<in> running (t @ s)"
 
       
   816 proof -
 
       
   817     -- {* According to @{thm vat_t.th_chain_to_ready}, there is a
 
       
   818        ready ancestor of @{term th}. *}
 
       
   819   have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)" 
       
   820     using th_kept vat_t.th_chain_to_ready_tG by auto
 
       
   821   then obtain th' where th'_in: "th' \<in> readys (t@s)"
 
       
   822                     and dp: "th' \<in> nancestors (tG (t @ s)) th"
 
       
   823     by blast
 
       
   824 
       
   825   -- {* We are going to first show that this @{term th'} is running. *}
 
       
   826   have "th' \<in> running (t @ s)"
 
       
   827   proof -
 
       
   828     -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}
 
       
   829     have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
 
   755     proof -
 
   830     proof -
 
   756       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
 
   831       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
 
   757             the  @{term cp}-value of @{term th'} is the maximum of 
   832             the  @{term cp}-value of @{term th'} is the maximum of 
   758             all precedences of all thread nodes in its @{term tRAG}-subtree: *}
 
   833             all precedences of all thread nodes in its @{term tRAG}-subtree: *}
 
   759       have "?L =  Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))"
 
   834       have "?L =  Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))"
 
   763         show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
 
   838         show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
 
   764       next
 
   839       next
 
   765         show "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"
 
   840         show "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"
 
   766           using readys_def th'_in vat_t.subtree_tG_thread by auto 
   841           using readys_def th'_in vat_t.subtree_tG_thread by auto 
   767       next
 
   842       next
 
   768         show "th \<in> subtree (tG (t @ s)) th'"
 
   843         show "th \<in> subtree (tG (t @ s)) th'" 
   769         by (simp add: dp subtree_def trancl_into_rtrancl)   
   844         using dp unfolding subtree_def nancestors_def2 by simp  
   770       next
 
   845       next
 
   771         show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
 
   846         show " Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
 
   772           by simp 
   847           by simp
 
   773       qed
 
   848       qed
 
   774       also have "... = ?R"
 
   849       also have "... = ?R"
 
   775         using th_cp_max th_cp_preced th_kept 
   850         using th_cp_max th_cp_preced th_kept 
   776               the_preced_def vat_t.max_cp_readys_threads by auto
 
   851               the_preced_def vat_t.max_cp_readys_threads by auto
 
   777       finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
 
   852       finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
 
   778     qed 
   853     qed 
   779 
   854 
   780     -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
   855     -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
   781           it is @{term running} by definition. *}
 
   856           it is @{term running} by definition. *}
 
   782     with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_def) 
   857     with `th' \<in> readys (t @ s)` 
       
   858     show "th' \<in> running (t @ s)" by (simp add: running_def) 
   783   qed
 
   859   qed
 
   784 
   860 
   785   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
 
   861   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
 
   786   moreover have "th' \<in> ancestors (tG (t @ s)) th"
 
   862   moreover have "th' \<in> nancestors (tG (t @ s)) th"
 
   787     by (simp add: ancestors_def dp)
 
   863     using dp unfolding nancestors_def2 by simp
 
   788   ultimately show ?thesis using that by metis
 
   864   ultimately show ?thesis using that by metis
 
   789 qed
 
   865 qed
 
   790 
   866 
   791 lemma (* new proof of th_blockedE *)
 
       
   792   assumes "th \<notin> running (t @ s)"
 
       
   793   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
 
       
   794                     "th' \<in> running (t @ s)"
 
       
   795 proof -
 
       
   796   
       
   797   -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is 
       
   798         in @{term "readys"} or there is path in the @{term RAG} leading from 
       
   799         it to a thread that is in @{term "readys"}. However, @{term th} cannot 
       
   800         be in @{term readys}, because otherwise, since @{term th} holds the 
       
   801         highest @{term cp}-value, it must be @{term "running"}. This would
 
       
   802         violate our assumption. *}
 
       
   803   have "th \<notin> readys (t @ s)" 
       
   804     using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto 
       
   805   then have "\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" 
       
   806     using th_kept vat_t.th_chain_to_ready by auto
 
       
   807   then obtain th' where th'_in: "th' \<in> readys (t@s)"
 
       
   808                     and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
 
       
   809   
       
   810   -- {* We are going to first show that this @{term th'} is running. *}
 
       
   811   have "th' \<in> running (t @ s)"
 
       
   812   proof -
 
       
   813     -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}
 
       
   814     have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
 
       
   815     proof -
 
       
   816       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
 
       
   817             the  @{term cp}-value of @{term th'} is the maximum of 
       
   818             all precedences of all thread nodes in its @{term tRAG}-subtree: *}
 
       
   819       have "?L =  Max (the_preced (t @ s) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))"
 
       
   820       proof -
 
       
   821         have "(the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th') =
 
       
   822               the_preced (t @ s) ` the_thread ` subtree (tRAG (t @ s)) (Th th')"
 
       
   823                 by fastforce
 
       
   824         thus ?thesis by (unfold cp_alt_def1, simp)
 
       
   825       qed
 
       
   826       also have "... = (the_preced (t @ s) th)"
 
       
   827       proof(rule image_Max_subset)
 
       
   828         show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
 
       
   829       next
 
       
   830         show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)"
 
       
   831           by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in 
       
   832                 the_thread.simps vat_t.subtree_tRAG_thread)
 
       
   833       next
 
       
   834         show "th \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')"
 
       
   835         proof -
 
       
   836           have "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
 
       
   837                     by (unfold tRAG_subtree_eq, auto simp:subtree_def)
 
       
   838           thus ?thesis by force
 
       
   839         qed
 
       
   840       next
 
       
   841         show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
 
       
   842           by simp
 
       
   843       qed
 
       
   844       also have "... = ?R"
 
       
   845         using th_cp_max th_cp_preced th_kept 
       
   846               the_preced_def vat_t.max_cp_readys_threads by auto
 
       
   847       finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
 
       
   848     qed 
       
   849 
       
   850     -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
       
   851           it is @{term running} by definition. *}
 
       
   852     with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_def) 
       
   853   qed
 
       
   854 
       
   855   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
 
       
   856   moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 
       
   857     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
 
       
   858   ultimately show ?thesis using that by metis
 
       
   859 qed
 
       
   860 
       
   861 lemma th_blockedE_pretty:
 
   867 lemma th_blockedE_pretty:
 
   862   assumes "th \<notin> running (t @ s)"
 
   868   shows "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> running (t @ s)"
 
   863   shows "\<exists>th'. th' \<in> ancestors (tG (t @ s)) th \<and> th' \<in> running (t @ s)"
 
       
   864 using th_blockedE assms 
   869 using th_blockedE assms 
   865 by blast
 
   870 by blast
 
   866 
       
   867 
       
   868 
   871 
   869 
   872 
   870 text {*
 
   873 text {*
 
   871   Now it is easy to see there is always a thread to run by case analysis
 
   874   Now it is easy to see there is always a thread to run by case analysis
 
   872   on whether thread @{term th} is running: if the answer is yes, the 
   875   on whether thread @{term th} is running: if the answer is yes, the 
   873   the running thread is obviously @{term th} itself; otherwise, the running
 
   876   the running thread is obviously @{term th} itself; otherwise, the running
 
   874   thread is the @{text th'} given by lemma @{thm th_blockedE}.
 
   877   thread is the @{text th'} given by lemma @{thm th_blockedE}.
 
   875 *}
 
   878 *}
 
   876 lemma live: "running (t @ s) \<noteq> {}"
 
   879 lemma live: "running (t @ s) \<noteq> {}"
 
   877 proof(cases "th \<in> running (t @ s)") 
   880 using th_blockedE by auto
 
   878   case True thus ?thesis by auto
 
       
   879 next
 
       
   880   case False
 
       
   881   thus ?thesis using th_blockedE by auto
 
       
   882 qed
 
       
   883 
   881 
   884 lemma blockedE:
 
   882 lemma blockedE:
 
       
   883   assumes "th \<notin> running (t @ s)"
 
       
   884   obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
 
       
   885                     "th' \<in> running (t @ s)"
 
       
   886                     "th' \<in> threads s"
 
       
   887                     "\<not>detached s th'"
 
       
   888                     "cp (t @ s) th' = preced th s"
 
       
   889                     "th' \<noteq> th"
 
       
   890 proof -
 
       
   891   obtain th' where a: "th' \<in> nancestors (tG (t @ s)) th" "th' \<in> running (t @ s)"
 
       
   892     using th_blockedE by blast
 
       
   893   moreover
 
       
   894     from a(2) have b: "th' \<in> threads s" 
       
   895     using running_threads_inv assms by metis
 
       
   896   moreover
 
       
   897     from a(2) have "\<not>detached s th'" 
       
   898     using running_inversion(2) assms by metis
 
       
   899   moreover
 
       
   900     from a(2) have "cp (t @ s) th' = preced th s" 
       
   901     using running_preced_inversion by blast 
       
   902   moreover
 
       
   903     from a(2) have "th' \<noteq> th" using assms a(2) by blast 
       
   904   ultimately show ?thesis using that by metis
 
       
   905 qed
 
       
   906 
       
   907 
       
   908 lemma nblockedE:
 
   885   assumes "th \<notin> running (t @ s)"
 
   909   assumes "th \<notin> running (t @ s)"
 
   886   obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
 
   910   obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
 
   887                     "th' \<in> running (t @ s)"
 
   911                     "th' \<in> running (t @ s)"
 
   888                     "th' \<in> threads s"
 
   912                     "th' \<in> threads s"
 
   889                     "\<not>detached s th'"
 
   913                     "\<not>detached s th'"
 
   890                     "cp (t @ s) th' = preced th s"
 
   914                     "cp (t @ s) th' = preced th s"
 
   891                     "th' \<noteq> th"
 
   915                     "th' \<noteq> th"
 
   892 using assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE
 
   916 using blockedE unfolding nancestors_def
 
   893 by metis
 
   917 using assms nancestors3 by auto
 
       
   918 
   894 
   919 
   895 lemma detached_not_running:
 
   920 lemma detached_not_running:
 
   896   assumes "detached (t @ s) th'"
 
   921   assumes "detached (t @ s) th'"
 
   897   and "th' \<noteq> th"
 
   922   and "th' \<noteq> th"
 
   898   shows "th' \<notin> running (t @ s)"
 
   923   shows "th' \<notin> running (t @ s)"
pip