--- a/prio/Paper/Paper.thy	Mon Feb 13 04:22:52 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 05:41:53 2012 +0000
@@ -509,7 +509,7 @@
   \noindent
   In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
   Note that in the initial state, that is where the list of events is empty, the set 
-  @{term threads} is empty and therefore there is no thread ready nor a running.
+  @{term threads} is empty and therefore there is neither a thread ready nor running.
   If there is one or more threads ready, then there can only be \emph{one} thread
   running, namely the one whose current precedence is equal to the maximum of all ready 
   threads. We use the set-comprehension to capture both possibilities.
@@ -582,7 +582,7 @@
 
   \noindent
   This completes our formal model of PIP. In the next section we present
-  properties that show our version of PIP is correct.
+  properties that show our model of PIP is correct.
 *}
 
 section {* Correctness Proof *}
@@ -600,7 +600,7 @@
   of the number of critical resources: if there are @{text m} critical
   resources, then a blocked job can only be blocked @{text m} times---that is
   a bounded number of times.
-  For their version of PIP, this is \emph{not} true (as pointed out by 
+  For their version of PIP, this property is \emph{not} true (as pointed out by 
   Yodaiken \cite{Yodaiken02}) as a high-priority thread can be
   blocked an unbounded number of times by creating medium-priority
   threads that block a thread locking a critical resource and having 
@@ -612,11 +612,11 @@
   we show that in every future state (denoted by @{text "s' @ s"}) in which
   @{text th} is still active, either @{text th} is running or it is blocked by a 
   thread that was active in the state @{text s}. Since in @{text s}, as in every 
-  state, the set of active threads is finite, @{text th} can only blocked a
-  finite number of time. We will actually prove a stricter bound. However,
-  this correctness criterion depends on a number of assumptions about the states
+  state, the set of active threads is finite, @{text th} can only be blocked a
+  finite number of times. We will actually prove a stricter bound. However,
+  this correctness criterion hinges on a number of assumptions about the states
   @{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening
-  in @{text s'}.
+  in @{text s'}. We list them next.
 
   \begin{quote}
   {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make 
@@ -645,10 +645,10 @@
   
   \begin{quote}
   {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot
-  be blocked indefinitely. Of course this can by violated if threads with higher priority
-  than @{text th} are created in @{text s'}. Therefore we have to assume that  
-  events in @{text s'} can only create (respectively set) threads with lower or equal 
-  priority than @{text prio} of @{text th}. We also have to assume that @{text th} does
+  be blocked indefinitely. Of course this can happen if threads with higher priority
+  than @{text th} are continously created in @{text s'}. Therefore we have to assume that  
+  events in @{text s'} can only create (respectively set) threads with equal or lower 
+  priority than @{text prio} of the thread @{text th}. We also have to assume that @{text th} does
   not get ``exited'' in @{text "s'"}.
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{l}
@@ -674,36 +674,40 @@
   precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"} 
   by a thread @{text th'} that already existed in @{text s}. As we shall see shortly,
   that means by only finitely many threads. Consequently, indefinite wait of
-  @{text th}, that is Priority Inversion, cannot occur.
+  @{text th}---whcih is Priority Inversion---cannot occur.
+
+  In what follows we will describe properties of PIP that allow us to prove 
+  Theorem~\ref{mainthm}. It is relatively easily to see that
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\
+  @{thm[mode=IfThen]  finite_threads}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  where the second property is by induction of @{term vt}. The next three
+  properties are 
 
-   The following are several very basic prioprites:
-  \begin{enumerate}
-  \item All runing threads must be ready (@{text "runing_ready"}):
-          @{thm[display] "runing_ready"}  
-  \item All ready threads must be living (@{text "readys_threads"}):
-          @{thm[display] "readys_threads"} 
-  \item There are finite many living threads at any moment (@{text "finite_threads"}):
-          @{thm[display] "finite_threads"} 
-  \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): 
-          @{thm[display] "wq_distinct"} 
-  \item All threads in waiting queues are living threads (@{text "wq_threads"}): 
-          @{thm[display] "wq_threads"} 
-  \item The event which can get a thread into waiting queue must be @{term "P"}-events
-         (@{text "block_pre"}): 
-          @{thm[display] "block_pre"}   
-  \item A thread may never wait for two different critical resources
-         (@{text "waiting_unique"}): 
-          @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}
-  \item Every resource can only be held by one thread
-         (@{text "held_unique"}): 
-          @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}
-  \item Every living thread has an unique precedence
-         (@{text "preced_unique"}): 
-          @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}
-  \end{enumerate}
-*}
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
+  @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
+  @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
+  \end{tabular}
+  \end{isabelle}
 
-text {* \noindent
+  \noindent
+  The first one states that every waiting thread can only wait for a single
+  resource (because it gets suspended after requesting that resource), and
+  the second that every resource can only be held by a single thread. The
+  third property establishes that in every given valid state, there is
+  at most one running thread.
+
+  TODO
+
+  \noindent
   The following lemmas show how RAG is changed with the execution of events:
   \begin{enumerate}
   \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):
@@ -761,8 +765,6 @@
 text {* \noindent
   Some deeper results about the system:
   \begin{enumerate}
-  \item There can only be one running thread (@{text "runing_unique"}):
-  @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
   \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
   @{thm [display] max_cp_eq}
   \item There must be one ready thread having the max @{term "cp"}-value 

--- a/prio/PrioG.thy	Mon Feb 13 04:22:52 2012 +0000
+++ b/prio/PrioG.thy	Mon Feb 13 05:41:53 2012 +0000
@@ -2,8 +2,15 @@
 imports PrioGDef 
 begin
 
-lemma runing_ready: "runing s \<subseteq> readys s"
-  by (auto simp only:runing_def readys_def)
+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:
    "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
@@ -354,22 +361,20 @@
   and "waiting s th cs1"
   and "waiting s th cs2"
   shows "cs1 = cs2"
-proof -
-  from waiting_unique_pre and prems
-  show ?thesis
-    by (auto simp add: wq_def s_waiting_def)
-qed
+using waiting_unique_pre prems
+unfolding wq_def s_waiting_def
+by auto
 
+(* not used *)
 lemma held_unique:
-  assumes "vt s"
-  and "holding s th1 cs"
+  fixes s::"state"
+  assumes "holding s th1 cs"
   and "holding s th2 cs"
   shows "th1 = th2"
-proof -
-  from prems show ?thesis
-    unfolding s_holding_def
-    by auto
-qed
+using prems
+unfolding s_holding_def
+by auto
+
 
 lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s"
   apply (induct s, auto)
@@ -2468,42 +2473,8 @@
 lemma finite_threads:
   assumes vt: "vt s"
   shows "finite (threads s)"
-proof -
-  from vt show ?thesis
-  proof(induct)
-    case (vt_cons s e)
-    assume vt: "vt s"
-    and step: "step s e"
-    and ih: "finite (threads s)"
-    from step
-    show ?case
-    proof(cases)
-      case (thread_create thread prio)
-      assume eq_e: "e = Create thread prio"
-      with ih
-      show ?thesis by (unfold eq_e, auto)
-    next
-      case (thread_exit thread)
-      assume eq_e: "e = Exit thread"
-      with ih show ?thesis 
-        by (unfold eq_e, auto)
-    next
-      case (thread_P thread cs)
-      assume eq_e: "e = P thread cs"
-      with ih show ?thesis by (unfold eq_e, auto)
-    next
-      case (thread_V thread cs)
-      assume eq_e: "e = V thread cs"
-      with ih show ?thesis by (unfold eq_e, auto)
-    next 
-      case (thread_set thread prio)
-      from vt_cons thread_set show ?thesis by simp
-    qed
-  next
-    case vt_nil
-    show ?case by (auto)
-  qed
-qed
+using vt
+by (induct) (auto elim: step.cases)
 
 lemma Max_f_mono:
   assumes seq: "A \<subseteq> B"
@@ -2785,14 +2756,6 @@
   show ?thesis by (rule max_cp_readys_threads_pre[OF vt False])
 qed
 
-lemma readys_threads:
-  shows "readys s \<subseteq> threads s"
-proof
-  fix th
-  assume "th \<in> readys s"
-  thus "th \<in> threads s"
-    by (unfold readys_def, auto)
-qed
 
 lemma eq_holding: "holding (wq s) th cs = holding s th cs"
   apply (unfold s_holding_def cs_holding_def wq_def, simp)

Binary file prio/paper.pdf has changed