diff -r 5d8ec128518b -r e3cf792db636 PIPBasics.thy --- a/PIPBasics.thy Tue Jun 14 13:56:51 2016 +0100 +++ b/PIPBasics.thy Tue Jun 14 15:06:16 2016 +0100 @@ -511,10 +511,12 @@ } ultimately show ?thesis by blast qed +(* lemma image_eq: assumes "A = B" shows "f ` A = f ` B" using assms by auto +*) lemma tRAG_trancl_eq_Th: "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = @@ -907,40 +909,6 @@ qed qed -text {* - The following lemma says that if @{text "s"} is a valid state, so - is its any postfix. Where @{term "monent t s"} is the postfix of - @{term "s"} with length @{term "t"}. -*} -lemma vt_moment: "\<And> t. vt (moment t s)" -proof(induct rule:ind) - case Nil - thus ?case by (simp add:vt_nil) -next - case (Cons s e t) - show ?case - proof(cases "t \<ge> length (e#s)") - case True - from True have "moment t (e#s) = e#s" by simp - thus ?thesis using Cons - by (simp add:valid_trace_def valid_trace_e_def, auto) - next - case False - from Cons have "vt (moment t s)" by simp - moreover have "moment t (e#s) = moment t s" - proof - - from False have "t \<le> length s" by simp - from moment_app [OF this, of "[e]"] - show ?thesis by simp - qed - ultimately show ?thesis by simp - qed -qed - -text {* - The following two lemmas are fundamental, because they assure - that the numbers of both living and ready threads are finite. -*} lemma finite_threads: shows "finite (threads s)" @@ -951,34 +919,6 @@ end -text {* - The following locale @{text "valid_moment"} is to inherit the properties - derived on any valid state to the prefix of it, with length @{text "i"}. -*} -locale valid_moment = valid_trace + - fixes i :: nat - -sublocale valid_moment < vat_moment: valid_trace "(moment i s)" - by (unfold_locales, insert vt_moment, auto) - -locale valid_moment_e = valid_moment + - assumes less_i: "i < length s" -begin - definition "next_e = hd (moment (Suc i) s)" - - lemma trace_e: - "moment (Suc i) s = next_e#moment i s" - proof - - from less_i have "Suc i \<le> length s" by auto - from moment_plus[OF this, folded next_e_def] - show ?thesis . - qed - -end - -sublocale valid_moment_e < vat_moment_e: valid_trace_e "moment i s" "next_e" - using vt_moment[of "Suc i", unfolded trace_e] - by (unfold_locales, simp) section {* Waiting queues are distinct *} @@ -1385,13 +1325,16 @@ end +context valid_trace +begin + text {* The is the main lemma of this section, which is derived by induction, case analysis on event @{text e} and assembling the @{text "wq_threads_kept"}-results of all possible cases of @{text "e"}. *} -lemma (in valid_trace) wq_threads: +lemma wq_threads: assumes "th \<in> set (wq s cs)" shows "th \<in> threads s" using assms @@ -1432,8 +1375,6 @@ subsection {* RAG and threads *} -context valid_trace -begin text {* As corollaries of @{thm wq_threads}, it is shown in this subsection @@ -1869,7 +1810,7 @@ "RAG (e # s) = RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> - {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R") + {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R") proof(rule rel_eqI) fix n1 n2 assume "(n1, n2) \<in> ?L" @@ -3208,14 +3149,15 @@ qed qed -lemma card_running: "card (running s) \<le> 1" +lemma card_running: + shows "card (running s) \<le> 1" proof(cases "running s = {}") case True thus ?thesis by auto next case False - then obtain th where [simp]: "th \<in> running s" by auto - from running_unique[OF this] + then obtain th where "th \<in> running s" by auto + with running_unique have "running s = {th}" by auto thus ?thesis by auto qed