# HG changeset patch # User Christian Urban # Date 1477057621 -3600 # Node ID f70344294e9932e28ee93419a1c8e14ab18ff2f8 # Parent 389ef8b1959c26bda2df0fbec7464dadf73e11f2 updated diff -r 389ef8b1959c -r f70344294e99 Correctness.thy --- 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' \ running (t @ s)" shows "cp (t @ s) th' = preced th s" proof - + have "th' \ 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))" diff -r 389ef8b1959c -r f70344294e99 Journal/Paper.thy --- 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} diff -r 389ef8b1959c -r f70344294e99 Max.thy --- 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 "\ a \ A. f a \ g a" + shows "Max (f ` A) \ 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 \ {}" by auto + next + fix fa + assume "fa \ f ` A" + then obtain a where h_fa: "a \ A" "fa = f a" by auto + show "fa \ Max (g ` A)" + proof(rule Max_ge_iff[THEN iffD2]) + from assms show "finite (g ` A)" by auto + next + from False show "g ` A \ {}" by auto + next + from h_fa have "g a \ g ` A" by auto + moreover have "fa \ g a" using h_fa assms(2) by auto + ultimately show "\a\g ` A. fa \ a" by auto + qed + qed +qed + +lemma Max_f_mono: + assumes seq: "A \ B" + and np: "A \ {}" + and fnt: "finite B" + shows "Max (f ` A) \ Max (f ` B)" +proof(rule Max_mono) + from seq show "f ` A \ f ` B" by auto +next + from np show "f ` A \ {}" by auto +next + from fnt and seq show "finite (f ` B)" by auto +qed + +lemma Max_UNION: + assumes "finite A" + and "A \ {}" + and "\ M \ f ` A. finite M" + and "\ M \ f ` A. M \ {}" + shows "Max (\x\ A. f x) = Max (Max ` f ` A)" (is "?L = ?R") + using assms[simp] +proof - + have "?L = Max (\(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 \ {}" + and "x = y" + shows "max x (Max A) = Max ({y} \ 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 diff -r 389ef8b1959c -r f70344294e99 PIPBasics.thy --- 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 "\ a \ A. f a \ g a" - shows "Max (f ` A) \ 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 \ {}" by auto - next - fix fa - assume "fa \ f ` A" - then obtain a where h_fa: "a \ A" "fa = f a" by auto - show "fa \ Max (g ` A)" - proof(rule Max_ge_iff[THEN iffD2]) - from assms show "finite (g ` A)" by auto - next - from False show "g ` A \ {}" by auto - next - from h_fa have "g a \ g ` A" by auto - moreover have "fa \ g a" using h_fa assms(2) by auto - ultimately show "\a\g ` A. fa \ a" by auto - qed - qed -qed - -lemma Max_f_mono: - assumes seq: "A \ B" - and np: "A \ {}" - and fnt: "finite B" - shows "Max (f ` A) \ Max (f ` B)" -proof(rule Max_mono) - from seq show "f ` A \ f ` B" by auto -next - from np show "f ` A \ {}" by auto -next - from fnt and seq show "finite (f ` B)" by auto -qed - -lemma Max_UNION: - assumes "finite A" - and "A \ {}" - and "\ M \ f ` A. finite M" - and "\ M \ f ` A. M \ {}" - shows "Max (\x\ A. f x) = Max (Max ` f ` A)" (is "?L = ?R") - using assms[simp] -proof - - have "?L = Max (\(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 \ {}" - and "x = y" - shows "max x (Max A) = Max ({y} \ 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 "(\x\C. B x) = (\ {B x |x. x \ C})" +(* and "\" *) +by (simp_all add: Setcompr_eq_image) + +lemma Max_Segments: + assumes "finite C" "\x\ C. finite (B x)" "\x\ C. B x \ {}" "{B x |x. x \ C} \ {}" + shows "Max (\x \ C. B x) = Max {Max (B x) | x. x \ 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 ` (\th\readys s. subtree (tG s) th))" - by (simp add: threads_alt_def1) - also have "... = Max (\x\readys s. the_preced s ` subtree (tG s) x) " - by (unfold image_UN, simp) - also have "... = Max (Max ` (\x. the_preced s ` subtree (tG s) x) ` readys s)" - proof(rule Max_UNION) - show "\M\(\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 \ (\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 \ ?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 (\th\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 \ 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 \ 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 diff -r 389ef8b1959c -r f70344294e99 journal.pdf Binary file journal.pdf has changed