pip: comparison PIPBasics.thy

equal deleted inserted replaced

-:30ed212f268a
+:b769f43deb30
 theory PIPBasics
 imports PIPDefs
 begin
 section {* Generic aulxiliary lemmas *}
+lemma rel_eqI:
+assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
+and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"
+shows "A = B"
+using assms by auto
 lemma f_image_eq:
 assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"
 shows "f ` A = g ` A"
 proof
 also from assms have "... = ?L"
 by (subst Max.insert, simp+)
 finally show ?thesis by simp
 qed
-lemma rel_eqI:
-assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
-and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"
-shows "A = B"
-using assms by auto
 section {* Lemmas do not depend on trace validity *}
+text {* The following lemma serves to proof @{text "preced_tm_lt"} *}
 lemma birth_time_lt:
 assumes "s \<noteq> []"
 shows "last_set th s < length s"
 using assms
 show ?thesis using Cons(1)[OF True]
 by (cases a, auto)
 qed
 qed simp
+text {* The following lemma also serves to proof @{text "preced_tm_lt"} *}
 lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
 by (induct s, auto)
+text {* The following lemma is used in Correctness.thy *}
 lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
 by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)
-lemma eq_RAG:
+text {*
-"RAG (wq s) = RAG s"
+The follow lemma says if a resource is waited for, it must be held
-by (unfold cs_RAG_def s_RAG_def, auto)
+by someone else.
+*}
 lemma waiting_holding:
 assumes "waiting (s::state) th cs"
 obtains th' where "holding s th' cs"
 proof -
 from assms[unfolded s_waiting_def, folded wq_def]
 hence "holding s th' cs"
 by (unfold s_holding_def, fold wq_def, auto)
 from that[OF this] show ?thesis .
 qed
-lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
+text {*
+The following four lemmas relate the @{term wq}
+and non-@{term wq} versions of @{term waiting}, @{term holding},
+@{term dependants} and @{term cp}.
+*}
+lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
+by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
+lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
+by (unfold s_holding_def wq_def cs_holding_def, simp)
+lemma eq_dependants: "dependants (wq s) = dependants s"
+by (simp add: s_dependants_abv wq_def)
+lemma cp_eq: "cp s th = cpreced (wq s) s th"
 unfolding cp_def wq_def
 apply(induct s rule: schs.induct)
 apply(simp add: Let_def cpreced_initial)
 apply(simp add: Let_def)
 apply(simp add: Let_def)
 apply(simp add: Let_def)
 apply(subst (2) schs.simps)
 apply(simp add: Let_def)
 done
+text {*
+The following lemmas is an alternative definition of @{term cp},
+which is based on the notion of subtrees in @{term RAG} and
+is handy to use once the abstract theory of {\em relational graph}
+(and specifically {\em relational tree} and {\em relational forest})
+are in place.
+*}
 lemma cp_alt_def:
 "cp s th =
 Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
 proof -
 have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
 proof -
 have "?L = ?R"
 by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
 thus ?thesis by simp
 qed
-thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
+thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp)
 qed
-lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
+text {*
-by (unfold s_RAG_def, auto)
+The following @{text "children_RAG_alt_def"} relates
+@{term children} in @{term RAG} to the notion of @{term holding}.
-lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
+It is a technical lemmas used to prove the two following lemmas.
-by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
+*}
-lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
-by (unfold s_holding_def wq_def cs_holding_def, simp)
 lemma children_RAG_alt_def:
 "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"
 by (unfold s_RAG_def, auto simp:children_def holding_eq)
+text {*
+The following two lemmas relate @{term holdents} and @{term cntCS}
+to @{term children} in @{term RAG}, so that proofs about
+@{term holdents} and @{term cntCS} can be carried out under
+the support of the abstract theory of {\em relational graph}
+(and specifically {\em relational tree} and {\em relational forest}).
+*}
 lemma holdents_alt_def:
 "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))"
 by (unfold children_RAG_alt_def holdents_def, simp add: image_image)
 lemma cntCS_alt_def:
 "cntCS s th = card (children (RAG s) (Th th))"
 apply (unfold children_RAG_alt_def cntCS_def holdents_def)
 by (rule card_image[symmetric], auto simp:inj_on_def)
+text {*
+The following two lemmas show the inclusion relations
+among three key sets, namely @{term runing}, @{term readys}
+and @{term threads}.
+*}
 lemma runing_ready:
 shows "runing s \<subseteq> readys s"
 unfolding runing_def readys_def
 by auto
 lemma readys_threads:
 shows "readys s \<subseteq> threads s"
 unfolding readys_def
 by auto
-lemma wq_v_neq [simp]:
+text {*
-"cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
+The following lemma says that if a thread is running,
-by (auto simp:wq_def Let_def cp_def split:list.splits)
+it must be the head of every waiting queue it is in.
+In other words, a running thread must have got every
-lemma runing_head:
+resource it has requested.
-assumes "th \<in> runing s"
+*}
-and "th \<in> set (wq_fun (schs s) cs)"
-shows "th = hd (wq_fun (schs s) cs)"
-using assms
-by (simp add:runing_def readys_def s_waiting_def wq_def)
 lemma runing_wqE:
 assumes "th \<in> runing s"
 and "th \<in> set (wq s cs)"
 obtains rest where "wq s cs = th#rest"
 proof -
 by (unfold runing_def readys_def, auto)
 qed
 with eq_wq that show ?thesis by metis
 qed
-lemma isP_E:
-assumes "isP e"
-obtains cs where "e = P (actor e) cs"
-using assms by (cases e, auto)
-lemma isV_E:
-assumes "isV e"
-obtains cs where "e = V (actor e) cs"
-using assms by (cases e, auto)
 text {*
 Every thread can only be blocked on one critical resource,
 symmetrically, every critical resource can only be held by one thread.
 This fact is much more easier according to our definition.
 *}
 assumes "holding (s::event list) th1 cs"
 and "holding s th2 cs"
 shows "th1 = th2"
 by (insert assms, unfold s_holding_def, auto)
+text {*
+The following three lemmas establishes the uniqueness of
+precedence, a key property about precedence.
+The first two are just technical lemmas to assist the proof
+of the third.
+*}
 lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
 apply (induct s, auto)
 by (case_tac a, auto split:if_splits)
 lemma last_set_unique:
 proof -
 from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)
 from last_set_unique [OF this th_in1 th_in2]
 show ?thesis .
 qed
+text {*
+The following lemma shows that there exits a linear order
+on precedences, which is crucial for the notion of
+@{term Max} to be applicable.
+*}
 lemma preced_linorder:
 assumes neq_12: "th1 \<noteq> th2"
 and th_in1: "th1 \<in> threads s"
 and th_in2: " th2 \<in> threads s"
 shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"
 from preced_unique [OF _ th_in1 th_in2] and neq_12
 have "preced th1 s \<noteq> preced th2 s" by auto
 thus ?thesis by auto
 qed
+text {*
+The following lemma case analysis the situations when
+two nodes are in @{term RAG}.
+*}
 lemma in_RAG_E:
 assumes "(n1, n2) \<in> RAG (s::state)"
 obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
 | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
 using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
 by auto
+text {*
+The following lemmas are the simplification rules
+for @{term count}, @{term cntP}, @{term cntV}.
+It is a major technical in this development to use
+the counter of @{term "P"} and @{term "V"} (* ccc *)
+*}
 lemma count_rec1 [simp]:
 assumes "Q e"
 shows "count Q (e#es) = Suc (count Q es)"
 using assms
 case (V th' pty)
 show ?thesis
 by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)",
 insert assms V, auto simp:cntV_def)
 qed (insert assms, auto simp:cntV_def)
-lemma eq_dependants: "dependants (wq s) = dependants s"
-by (simp add: s_dependants_abv wq_def)
-lemma inj_the_preced:
-"inj_on (the_preced s) (threads s)"
-by (metis inj_onI preced_unique the_preced_def)
-lemma holding_next_thI:
-assumes "holding s th cs"
-and "length (wq s cs) > 1"
-obtains th' where "next_th s th cs th'"
-proof -
-from assms(1)[folded holding_eq, unfolded cs_holding_def]
-have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)"
-by (unfold s_holding_def, fold wq_def, auto)
-then obtain rest where h1: "wq s cs = th#rest"
-by (cases "wq s cs", auto)
-with assms(2) have h2: "rest \<noteq> []" by auto
-let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
-have "next_th s th cs ?th'" using  h1(1) h2
-by (unfold next_th_def, auto)
-from that[OF this] show ?thesis .
-qed
 (* ccc *)
 section {* Locales used to investigate the execution of PIP *}
 using vt_moment[of "Suc i", unfolded trace_e]
 by (unfold_locales, simp)
 section {* Distinctiveness of waiting queues *}
+lemma (in valid_trace) finite_threads:
+shows "finite (threads s)"
+using vt by (induct) (auto elim: step.cases)
+lemma (in valid_trace) finite_readys [simp]: "finite (readys s)"
+using finite_threads readys_threads rev_finite_subset by blast
 context valid_trace_create
 begin
 lemma wq_kept [simp]:
 shows "wq (e#s) cs' = wq s cs'"
 using assms by simp
 end
 context valid_trace
 begin
-lemma  finite_threads:
-shows "finite (threads s)"
-using vt by (induct) (auto elim: step.cases)
-lemma finite_readys [simp]: "finite (readys s)"
-using finite_threads readys_threads rev_finite_subset by blast
 lemma wq_distinct: "distinct (wq s cs)"
 proof(induct rule:ind)
 case (Cons s e)
 interpret vt_e: valid_trace_e s e using Cons by simp
 lemma  dm_RAG_threads:
 assumes in_dom: "(Th th) \<in> Domain (RAG s)"
 shows "th \<in> threads s"
 proof -
 from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
-moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto
+moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto)
 ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
 hence "th \<in> set (wq s cs)"
 by (unfold s_RAG_def, auto simp:cs_waiting_def)
 from wq_threads [OF this] show ?thesis .
 qed
 with wq_s_cs[folded otherwise] wq_distinct[of cs]
 show ?thesis by simp
 next
 case False
 have "wq (e#s) c = wq s c" using False
-by (unfold is_v, simp)
+by simp
 hence "waiting s t c" using assms
 by (simp add: cs_waiting_def waiting_eq)
 hence "t \<notin> readys s" by (unfold readys_def, auto)
 hence "t \<notin> runing s" using runing_ready by auto
 with runing_th_s[folded otherwise] show ?thesis by auto
 assumes "waiting s t c"
 and "c \<noteq> cs"
 shows "waiting (e#s) t c"
 proof -
 have "wq (e#s) c = wq s c"
-using assms(2) is_v by auto
+using assms(2) by auto
 with assms(1) show ?thesis
 using cs_waiting_def waiting_eq by auto
 qed
 lemma holding_esI2:
 assumes "c \<noteq> cs"
 and "holding s t c"
 shows "holding (e#s) t c"
 proof -
-from assms(1) have "wq (e#s) c = wq s c" using is_v by auto
+from assms(1) have "wq (e#s) c = wq s c"  by auto
 from assms(2)[unfolded s_holding_def, folded wq_def,
 folded this, unfolded wq_def, folded s_holding_def]
 show ?thesis .
 qed
 assumes "waiting (e#s) t c"
 obtains "c \<noteq> cs" "waiting s t c"
 |    "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'"
 proof(cases "c = cs")
 case False
-hence "wq (e#s) c = wq s c" using is_v by auto
+hence "wq (e#s) c = wq s c" by auto
 with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto
 from that(1)[OF False this] show ?thesis .
 next
 case True
 from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs]
 folded wq_def, unfolded wq_es_cs]
 have "t = taker" by (simp add: taker_def)
 from that(1)[OF True this] show ?thesis .
 next
 case False
-hence "wq (e#s) c = wq s c" using is_v by auto
+hence "wq (e#s) c = wq s c" by auto
 from assms[unfolded s_holding_def, folded wq_def,
 unfolded this, unfolded wq_def, folded s_holding_def]
 have "holding s t c"  .
 from that(2)[OF False this] show ?thesis .
 qed
 have " wq (e # s) cs = []" .
 from assms[unfolded s_holding_def, folded wq_def, unfolded this]
 show ?thesis by auto
 qed
-lemma no_waiting:
+lemma no_waiter_before: "\<not> waiting s t cs"
+proof
+assume otherwise: "waiting s t cs"
+from this[unfolded s_waiting_def, folded wq_def,
+unfolded wq_s_cs rest_nil]
+show False by simp
+qed
+lemma no_waiter_after:
 assumes "waiting (e#s) t cs"
 shows False
 proof -
 from wq_es_cs[unfolded nil_wq']
 have " wq (e # s) cs = []" .
 lemma waiting_esE:
 assumes "waiting (e#s) t c"
 obtains "c \<noteq> cs" "waiting s t c"
 proof(cases "c = cs")
 case False
-hence "wq (e#s) c = wq s c" using is_v by auto
+hence "wq (e#s) c = wq s c"  by auto
 with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto
 from that(1)[OF False this] show ?thesis .
 next
 case True
-from no_waiting[OF assms[unfolded True]]
+from no_waiter_after[OF assms[unfolded True]]
 show ?thesis by auto
 qed
 lemma holding_esE:
 assumes "holding (e#s) t c"
 case True
 from no_holding[OF assms[unfolded True]]
 show ?thesis by auto
 next
 case False
-hence "wq (e#s) c = wq s c" using is_v by auto
+hence "wq (e#s) c = wq s c" by auto
 from assms[unfolded s_holding_def, folded wq_def,
 unfolded this, unfolded wq_def, folded s_holding_def]
 have "holding s t c"  .
 from that[OF False this] show ?thesis .
 qed
 qed
 qed
 finally show ?thesis .
 qed
+lemma eq_RAG:
+"RAG (wq s) = RAG s"
+by (unfold cs_RAG_def s_RAG_def, auto)
 lemma dependants_alt_def:
 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
 by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
 lemma dependants_alt_def1:

changeset 108	b769f43deb30
parent 107	30ed212f268a
child 109	4e59c0ce1511