pip: comparison PIPBasics.thy

equal deleted inserted replaced

-:4b416723a616
+:b3795b1f030b
 section {* RAG is acyclic *}
 subsection {* Uniqueness of waiting *}
 text {*
-Uniqueness of waiting is expressed by the following
+{\em Uniqueness of waiting} means that
-predicate over system state (or event trace).
+a thread can only be blocked on one resource.
-It says a thread can only be blocked on one resource.
+This property is needed in order to prove that @{term RAG}
+is acyclic. Therefore, we need to prove it first in the following
+lemma @{text "waiting_unqiue"}, all lemmas before it are auxiliary.
+The property is expressed by the following predicate over system
+state (or event trace), which is also named @{text "waiting_unqiue"}.
 *}
 definition
 "waiting_unique (ss::state) =
 (\<forall> th cs1 cs2. waiting ss th cs1 \<longrightarrow>
 lemma named @{text waiting_unique}) that
 this property holds on any valid trace (or system state).
 *}
 text {*
-As a first step, we need to understand how
+As a first step to prove lemma @{text "waiting_unqiue"},
+we need to understand how
 a thread is get blocked.
 We show in the following lemmas
 (all named @{text "waiting_inv"}) that
 @{term P}-operation is the only cause.
 *}
 and "waiting (e#s) th' cs'"
 shows "e = P th' cs'"
 proof -
 from assms(2)
 show ?thesis
-by (cases rule:waiting_esE, insert assms, auto)
+by (cases rule:waiting_esE, insert assms, auto) (* ccc *)
 qed
 end
 context valid_trace_v_e
 show ?thesis
 by (cases rule:waiting_esE, insert assms, auto)
 qed
 end
 context valid_trace_e
 begin
 lemma waiting_inv:
 by (unfold_locales, simp)
 show ?thesis using vt.waiting_inv[OF assms] by simp
 qed
 qed
+text {*
+Now, with @{thm waiting_inv} in place, the following lemma
+shows the uniqueness of waiting is kept by every operation
+in the PIP protocol. This lemma constitutes the main part
+in the proof of lemma @{text "waiting_unique"}.
+*}
 lemma waiting_unique_kept:
 assumes "waiting_unique s"
 shows "waiting_unique (e#s)"
 proof -
 note h = assms[unfolded waiting_unique_def, rule_format]
 end
 context valid_trace
 begin
+text {*
+With @{thm valid_trace_e.waiting_unique_kept} in place,
+the proof of the following lemma @{text "waiting_unique"}
+needs only a very simple induction.
+*}
 lemma waiting_unique
 [unfolded waiting_unique_def, rule_format]:
 shows "waiting_unique s"
 proof(induct rule:ind)
 case Nil
 by simp
 qed
 end
 subsection {* Acyclic keeping *}
+text {*
+To prove that @{term RAG} is acyclic, we need to show the acyclic property
+is preserved by all system operations. There are only two non-trivial cases,
+the @{term P} and @{term V} operation, where are treated in the following
+locales, under the name @{text "acylic_RAG_kept"}:
+*}
 context valid_trace_v_e
 begin
 lemma
 end
 context valid_trace
 begin
+text {*
+With these @{text "acylic_RAG_kept"}-lemmas proved,
+the proof of the following @{text "acyclic_RAG"} is
+straight forward.
+*}
 lemma acyclic_RAG:
 shows "acyclic (RAG s)"
 proof(induct rule:ind)
 case Nil
 qed
 end
 section {* RAG is single-valued *}
+text {*
+The proof that @{term RAG} is single-valued makes use of
+@{text "unique_waiting"} and @{thm held_unique} and the
+proof itself is very simple:
+*}
 context valid_trace
 begin
 lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"

changeset 112	b3795b1f030b
parent 111	4b416723a616
child 113	ce85c3c4e5bf