--- a/Correctness.thy Wed Aug 24 16:13:20 2016 +0200
+++ b/Correctness.thy Sun Oct 02 14:32:05 2016 +0100
@@ -5,6 +5,17 @@
text {*
The following two auxiliary lemmas are used to reason about @{term Max}.
*}
+
+lemma subset_Max:
+ assumes "finite A"
+ and "B \<subseteq> A"
+ and "c \<in> B"
+ and "Max A = c"
+shows "Max B = c"
+using Max.subset assms
+by (metis Max.coboundedI Max_eqI rev_finite_subset subset_eq)
+
+
lemma image_Max_eqI:
assumes "finite B"
and "b \<in> B"
@@ -101,7 +112,7 @@
locale extend_highest_gen = highest_gen +
fixes t
- assumes vt_t: "vt (t@s)"
+ assumes vt_t: "vt (t @ s)"
and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"
and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
@@ -131,16 +142,6 @@
qed
qed
-(* locale red_extend_highest_gen = extend_highest_gen +
- fixes i::nat
-*)
-
-(*
-sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"
- apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
- apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
- by (unfold highest_gen_def, auto dest:step_back_vt_app)
-*)
context extend_highest_gen
begin
@@ -183,7 +184,7 @@
lemma th_kept: "th \<in> threads (t @ s) \<and>
- preced th (t@s) = preced th s" (is "?Q t")
+ preced th (t @ s) = preced th s" (is "?Q t")
proof -
show ?thesis
proof(induct rule:ind)
@@ -246,7 +247,7 @@
qed
text {*
- According to @{thm th_kept}, thread @{text "th"} has its living status
+ According to @{thm th_kept}, thread @{text "th"} has its liveness status
and precedence kept along the way of @{text "t"}. The following lemma
shows that this preserved precedence of @{text "th"} remains as the highest
along the way of @{text "t"}.
@@ -260,7 +261,8 @@
are newly introduced or modified, are always lower than the one held
by @{term "th"}, which by @{thm th_kept} is preserved along the way.
*}
-lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
+lemma max_kept:
+ shows "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
proof(induct rule:ind)
case Nil
from highest_preced_thread
@@ -723,9 +725,11 @@
Now, since @{term readys}-set is non-empty, there must be
one in it which holds the highest @{term cp}-value, which, by definition,
- is the @{term running}-thread. However, we are going to show more: this running thread
- is exactly @{term "th'"}.
- *}
+ is the @{term running}-thread. However, we are going to show more: this
+ running thread is exactly @{term "th'"}. *}
+
+
+(*
lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
assumes "th \<notin> running (t @ s)"
obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
@@ -744,9 +748,14 @@
-- {* So, there must be a path from @{term th} to another thread @{text "th'"} in
term @{term readys}: *}
- ultimately obtain th' where th'_in: "th' \<in> readys (t @ s)"
+ ultimately obtain th' where th'_readys: "th' \<in> readys (t @ s)"
and dp: "(th, th') \<in> (tG (t @ s))\<^sup>+" by auto
+ -- {* @{text "th'"} is an ancestor of @{term "th"} *}
+ have "th' \<in> ancestors (tG (t @ s)) th" using dp
+ unfolding ancestors_def by simp
+
+ moreover
-- {* We are going to show that this @{term th'} is running. *}
have "th' \<in> running (t @ s)"
proof -
@@ -756,6 +765,72 @@
-- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
the @{term cp}-value of @{term th'} is the maximum of
all precedences of all thread nodes in its @{term tRAG}-subtree: *}
+
+ have "?L = Max (preceds (subtree (tG (t @ s)) th') (t @ s))"
+ unfolding cp_alt_def2 image_def the_preced_def by meson
+ also have "... = (preced th (t @ s))"
+ thm subset_Max
+ thm preced_unique
+ proof(rule subset_Max[where ?A="preceds (threads (t @ s)) (t @ s)"])
+ show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
+ next
+ have "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"
+ using readys_def th'_readys vat_t.subtree_tG_thread by auto
+ then show "preceds (subtree (tG (t @ s)) th') (t @ s) \<subseteq> preceds (threads (t @ s)) (t @ s)"
+ by auto
+ next
+ have "th \<in> subtree (tG (t @ s)) th'"
+ by (simp add: dp subtree_def trancl_into_rtrancl)
+ then show " preced th (t @ s) \<in> preceds (subtree (tG (t @ s)) th') (t @ s)"
+ by blast
+ next
+ have "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
+ apply(simp only: the_preced_def)
+ by simp
+ show "Max (preceds (threads (t @ s)) (t @ s)) = preced th (t @ s)"
+ thm th_kept max_kept
+ apply(simp del: th_kept)
+ apply(simp only: the_preced_def image_def)
+ apply(simp add: Bex_def_raw)
+
+ qed
+ also have "... = ?R"
+ using th_cp_max th_cp_preced th_kept
+ the_preced_def vat_t.max_cp_readys_threads by auto
+ finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
+ qed
+
+ -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys,
+ it is @{term running} by definition. *}
+ then show "th' \<in> running (t @ s)" using th'_readys
+ unfolding running_def by simp
+ qed
+
+ ultimately show ?thesis using that by metis
+qed
+*)
+
+lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
+ obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
+ "th' \<in> running (t @ s)"
+proof -
+ -- {* According to @{thm vat_t.th_chain_to_ready}, there is a
+ ready ancestor of @{term th}. *}
+ have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)"
+ using th_kept vat_t.th_chain_to_ready_tG by auto
+ then obtain th' where th'_in: "th' \<in> readys (t@s)"
+ and dp: "th' \<in> nancestors (tG (t @ s)) th"
+ by blast
+
+ -- {* We are going to first show that this @{term th'} is running. *}
+ have "th' \<in> running (t @ s)"
+ proof -
+ -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}
+ have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
+ proof -
+ -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
+ the @{term cp}-value of @{term th'} is the maximum of
+ all precedences of all thread nodes in its @{term tRAG}-subtree: *}
have "?L = Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))"
by (unfold cp_alt_def2, simp)
also have "... = (the_preced (t @ s) th)"
@@ -765,80 +840,10 @@
show "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"
using readys_def th'_in vat_t.subtree_tG_thread by auto
next
- show "th \<in> subtree (tG (t @ s)) th'"
- by (simp add: dp subtree_def trancl_into_rtrancl)
+ show "th \<in> subtree (tG (t @ s)) th'"
+ using dp unfolding subtree_def nancestors_def2 by simp
next
- show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
- by simp
- qed
- also have "... = ?R"
- using th_cp_max th_cp_preced th_kept
- the_preced_def vat_t.max_cp_readys_threads by auto
- finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
- qed
-
- -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys,
- it is @{term running} by definition. *}
- with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_def)
- qed
-
- -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
- moreover have "th' \<in> ancestors (tG (t @ s)) th"
- by (simp add: ancestors_def dp)
- ultimately show ?thesis using that by metis
-qed
-
-lemma (* new proof of th_blockedE *)
- assumes "th \<notin> running (t @ s)"
- obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> running (t @ s)"
-proof -
-
- -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is
- in @{term "readys"} or there is path in the @{term RAG} leading from
- it to a thread that is in @{term "readys"}. However, @{term th} cannot
- be in @{term readys}, because otherwise, since @{term th} holds the
- highest @{term cp}-value, it must be @{term "running"}. This would
- violate our assumption. *}
- have "th \<notin> readys (t @ s)"
- using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto
- then have "\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+"
- using th_kept vat_t.th_chain_to_ready by auto
- then obtain th' where th'_in: "th' \<in> readys (t@s)"
- and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
-
- -- {* We are going to first show that this @{term th'} is running. *}
- have "th' \<in> running (t @ s)"
- proof -
- -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}
- have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
- proof -
- -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
- the @{term cp}-value of @{term th'} is the maximum of
- all precedences of all thread nodes in its @{term tRAG}-subtree: *}
- have "?L = Max (the_preced (t @ s) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))"
- proof -
- have "(the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th') =
- the_preced (t @ s) ` the_thread ` subtree (tRAG (t @ s)) (Th th')"
- by fastforce
- thus ?thesis by (unfold cp_alt_def1, simp)
- qed
- also have "... = (the_preced (t @ s) th)"
- proof(rule image_Max_subset)
- show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
- next
- show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)"
- by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in
- the_thread.simps vat_t.subtree_tRAG_thread)
- next
- show "th \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')"
- proof -
- have "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
- by (unfold tRAG_subtree_eq, auto simp:subtree_def)
- thus ?thesis by force
- qed
- next
- show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
+ show " Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
by simp
qed
also have "... = ?R"
@@ -849,24 +854,22 @@
-- {* Now, since @{term th'} holds the highest @{term cp}-value in readys,
it is @{term running} by definition. *}
- with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_def)
+ with `th' \<in> readys (t @ s)`
+ show "th' \<in> running (t @ s)" by (simp add: running_def)
qed
-- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
- moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
+ moreover have "th' \<in> nancestors (tG (t @ s)) th"
+ using dp unfolding nancestors_def2 by simp
ultimately show ?thesis using that by metis
qed
lemma th_blockedE_pretty:
- assumes "th \<notin> running (t @ s)"
- shows "\<exists>th'. th' \<in> ancestors (tG (t @ s)) th \<and> th' \<in> running (t @ s)"
+ shows "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> running (t @ s)"
using th_blockedE assms
by blast
-
-
text {*
Now it is easy to see there is always a thread to run by case analysis
on whether thread @{term th} is running: if the answer is yes, the
@@ -874,14 +877,35 @@
thread is the @{text th'} given by lemma @{thm th_blockedE}.
*}
lemma live: "running (t @ s) \<noteq> {}"
-proof(cases "th \<in> running (t @ s)")
- case True thus ?thesis by auto
-next
- case False
- thus ?thesis using th_blockedE by auto
+using th_blockedE by auto
+
+lemma blockedE:
+ assumes "th \<notin> running (t @ s)"
+ obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
+ "th' \<in> running (t @ s)"
+ "th' \<in> threads s"
+ "\<not>detached s th'"
+ "cp (t @ s) th' = preced th s"
+ "th' \<noteq> th"
+proof -
+ obtain th' where a: "th' \<in> nancestors (tG (t @ s)) th" "th' \<in> running (t @ s)"
+ using th_blockedE by blast
+ moreover
+ from a(2) have b: "th' \<in> threads s"
+ using running_threads_inv assms by metis
+ moreover
+ from a(2) have "\<not>detached s th'"
+ using running_inversion(2) assms by metis
+ moreover
+ from a(2) have "cp (t @ s) th' = preced th s"
+ using running_preced_inversion by blast
+ moreover
+ from a(2) have "th' \<noteq> th" using assms a(2) by blast
+ ultimately show ?thesis using that by metis
qed
-lemma blockedE:
+
+lemma nblockedE:
assumes "th \<notin> running (t @ s)"
obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
"th' \<in> running (t @ s)"
@@ -889,8 +913,9 @@
"\<not>detached s th'"
"cp (t @ s) th' = preced th s"
"th' \<noteq> th"
-using assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE
-by metis
+using blockedE unfolding nancestors_def
+using assms nancestors3 by auto
+
lemma detached_not_running:
assumes "detached (t @ s) th'"