--- a/Correctness.thy Fri Oct 07 21:15:35 2016 +0100
+++ b/Correctness.thy Fri Oct 21 14:47:01 2016 +0100
@@ -504,6 +504,9 @@
assumes running': "th' \<in> running (t @ s)"
shows "cp (t @ s) th' = preced th s"
proof -
+ have "th' \<in> readys (t @ s)" using assms
+ using running_ready subsetCE by blast
+
have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" using assms
unfolding running_def by simp
also have "... = Max (cp (t @ s) ` threads (t @ s))"
--- a/Journal/Paper.thy Fri Oct 07 21:15:35 2016 +0100
+++ b/Journal/Paper.thy Fri Oct 21 14:47:01 2016 +0100
@@ -1081,7 +1081,7 @@
\end{lemma}
\begin{proof}
- By definition the running thread has as precedence the maximum of
+ By definition the running thread has as current precedence the maximum of
all ready threads, that is
\begin{center}
--- a/Max.thy Fri Oct 07 21:15:35 2016 +0100
+++ b/Max.thy Fri Oct 21 14:47:01 2016 +0100
@@ -75,4 +75,76 @@
qed
+lemma Max_fg_mono:
+ assumes "finite A"
+ and "\<forall> a \<in> A. f a \<le> g a"
+ shows "Max (f ` A) \<le> Max (g ` A)"
+proof(cases "A = {}")
+ case True
+ thus ?thesis by auto
+next
+ case False
+ show ?thesis
+ proof(rule Max.boundedI)
+ from assms show "finite (f ` A)" by auto
+ next
+ from False show "f ` A \<noteq> {}" by auto
+ next
+ fix fa
+ assume "fa \<in> f ` A"
+ then obtain a where h_fa: "a \<in> A" "fa = f a" by auto
+ show "fa \<le> Max (g ` A)"
+ proof(rule Max_ge_iff[THEN iffD2])
+ from assms show "finite (g ` A)" by auto
+ next
+ from False show "g ` A \<noteq> {}" by auto
+ next
+ from h_fa have "g a \<in> g ` A" by auto
+ moreover have "fa \<le> g a" using h_fa assms(2) by auto
+ ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto
+ qed
+ qed
+qed
+
+lemma Max_f_mono:
+ assumes seq: "A \<subseteq> B"
+ and np: "A \<noteq> {}"
+ and fnt: "finite B"
+ shows "Max (f ` A) \<le> Max (f ` B)"
+proof(rule Max_mono)
+ from seq show "f ` A \<subseteq> f ` B" by auto
+next
+ from np show "f ` A \<noteq> {}" by auto
+next
+ from fnt and seq show "finite (f ` B)" by auto
+qed
+
+lemma Max_UNION:
+ assumes "finite A"
+ and "A \<noteq> {}"
+ and "\<forall> M \<in> f ` A. finite M"
+ and "\<forall> M \<in> f ` A. M \<noteq> {}"
+ shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")
+ using assms[simp]
+proof -
+ have "?L = Max (\<Union>(f ` A))"
+ by (fold Union_image_eq, simp)
+ also have "... = ?R"
+ by (subst Max_Union, simp+)
+ finally show ?thesis .
+qed
+
+lemma max_Max_eq:
+ assumes "finite A"
+ and "A \<noteq> {}"
+ and "x = y"
+ shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")
+proof -
+ have "?R = Max (insert y A)" by simp
+ also from assms have "... = ?L"
+ by (subst Max.insert, simp+)
+ finally show ?thesis by simp
+qed
+
+
end
--- a/PIPBasics.thy Fri Oct 07 21:15:35 2016 +0100
+++ b/PIPBasics.thy Fri Oct 21 14:47:01 2016 +0100
@@ -33,76 +33,7 @@
by (rule image_subsetI, auto intro:h[symmetric])
qed
-lemma Max_fg_mono:
- assumes "finite A"
- and "\<forall> a \<in> A. f a \<le> g a"
- shows "Max (f ` A) \<le> Max (g ` A)"
-proof(cases "A = {}")
- case True
- thus ?thesis by auto
-next
- case False
- show ?thesis
- proof(rule Max.boundedI)
- from assms show "finite (f ` A)" by auto
- next
- from False show "f ` A \<noteq> {}" by auto
- next
- fix fa
- assume "fa \<in> f ` A"
- then obtain a where h_fa: "a \<in> A" "fa = f a" by auto
- show "fa \<le> Max (g ` A)"
- proof(rule Max_ge_iff[THEN iffD2])
- from assms show "finite (g ` A)" by auto
- next
- from False show "g ` A \<noteq> {}" by auto
- next
- from h_fa have "g a \<in> g ` A" by auto
- moreover have "fa \<le> g a" using h_fa assms(2) by auto
- ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto
- qed
- qed
-qed
-
-lemma Max_f_mono:
- assumes seq: "A \<subseteq> B"
- and np: "A \<noteq> {}"
- and fnt: "finite B"
- shows "Max (f ` A) \<le> Max (f ` B)"
-proof(rule Max_mono)
- from seq show "f ` A \<subseteq> f ` B" by auto
-next
- from np show "f ` A \<noteq> {}" by auto
-next
- from fnt and seq show "finite (f ` B)" by auto
-qed
-
-lemma Max_UNION:
- assumes "finite A"
- and "A \<noteq> {}"
- and "\<forall> M \<in> f ` A. finite M"
- and "\<forall> M \<in> f ` A. M \<noteq> {}"
- shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")
- using assms[simp]
-proof -
- have "?L = Max (\<Union>(f ` A))"
- by (fold Union_image_eq, simp)
- also have "... = ?R"
- by (subst Max_Union, simp+)
- finally show ?thesis .
-qed
-
-lemma max_Max_eq:
- assumes "finite A"
- and "A \<noteq> {}"
- and "x = y"
- shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")
-proof -
- have "?R = Max (insert y A)" by simp
- also from assms have "... = ?L"
- by (subst Max.insert, simp+)
- finally show ?thesis by simp
-qed
+
section {* Lemmas do not depend on trace validity *}
@@ -3821,46 +3752,68 @@
over the union of subtrees, the following equation can be derived:
*}
-thm the_preced_def cpreceds_def
+
+lemma cp_alt_def3:
+ shows "cp s th = Max (preceds (subtree (tG s) th) s)"
+unfolding cp_alt_def2
+unfolding image_def
+unfolding the_preced_def
+by meson
+
+lemma KK:
+ shows "(\<Union>x\<in>C. B x) = (\<Union> {B x |x. x \<in> C})"
+(* and "\<Union>" *)
+by (simp_all add: Setcompr_eq_image)
+
+lemma Max_Segments:
+ assumes "finite C" "\<forall>x\<in> C. finite (B x)" "\<forall>x\<in> C. B x \<noteq> {}" "{B x |x. x \<in> C} \<noteq> {}"
+ shows "Max (\<Union>x \<in> C. B x) = Max {Max (B x) | x. x \<in> C}"
+using assms
+apply(subst KK(1))
+apply(subst Max_Union)
+apply(auto)[3]
+apply(simp add: Setcompr_eq_image)
+apply(simp add: image_eq_UN)
+done
lemma max_cp_readys_max_preced_tG:
- shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R")
+ shows "Max (cp s ` readys s) = Max (preceds (threads s) s)" (is "?L = ?R")
proof(cases "readys s = {}")
case False
- have "?R =
- Max (the_preced s ` (\<Union>th\<in>readys s. subtree (tG s) th))"
- by (simp add: threads_alt_def1)
- also have "... = Max (\<Union>x\<in>readys s. the_preced s ` subtree (tG s) x) "
- by (unfold image_UN, simp)
- also have "... = Max (Max ` (\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s)"
- proof(rule Max_UNION)
- show "\<forall>M\<in>(\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s. finite M"
- using fsbttGs.finite_subtree by auto
- qed (auto simp:False subtree_def finite_readys)
- also have "... = Max ((Max \<circ> (\<lambda>x. the_preced s ` subtree (tG s) x)) ` readys s)"
- by (simp add: image_comp)
- also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
- proof -
- have "(?f ` ?A) = (?g ` ?A)"
- proof(rule f_image_eq)
- fix th1
- assume "th1 \<in> ?A"
- thus "?f th1 = ?g th1"
- by (unfold cp_alt_def2, simp)
- qed
- thus ?thesis by simp
- qed
- finally show ?thesis by simp
+ have "Max (preceds (threads s) s) = Max (preceds (\<Union>th\<in>readys s. subtree (tG s) th) s)"
+ unfolding threads_alt_def1 by simp
+ also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \<in> readys s}"
+ apply(subst Max_Segments[symmetric])
+ prefer 5
+ apply(rule arg_cong)
+ back
+ apply(blast)
+ apply (simp add: finite_readys)
+ apply (simp add: fsbttGs.finite_subtree)
+ apply blast
+ using False by blast
+ also have "... = Max {cp s th | th. th \<in> readys s}"
+ unfolding cp_alt_def3 ..
+ finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)"
+ by (simp add: Setcompr_eq_image image_def)
qed (auto simp:threads_alt_def)
+lemma LL:
+shows "the_preced s ` threads s = preceds (threads s) s"
+using the_preced_def by auto
+
+
text {*
The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG}
and @{thm max_cp_eq}:
*}
lemma max_cp_readys_threads:
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
- using max_cp_readys_max_preced_tG max_cp_eq by auto
+ apply(simp add: max_cp_readys_max_preced_tG)
+ apply(simp add: max_cp_eq)
+ apply(simp add: LL)
+ done
end
Binary file journal.pdf has changed