# HG changeset patch
# User zhangx
# Date 1455355131 -28800
# Node ID 8a6125caead2f9b0e6e9428808d6a7aac6804a4b
# Parent  a7441db6f4e1c08431b02c676e9c040d3a82a6c8
Slight changes in commenting.

diff -r a7441db6f4e1 -r 8a6125caead2 Implementation.thy
--- a/Implementation.thy	Fri Feb 12 17:50:24 2016 +0800
+++ b/Implementation.thy	Sat Feb 13 17:18:51 2016 +0800
@@ -2,6 +2,19 @@
 imports PIPBasics
 begin
 
+section {*
+  This file contains lemmas used to guide the recalculation of current precedence 
+  after every step of execution (or system operation, or event), 
+  which is the most tricky part in the implementation of PIP.
+
+  Following convention, lemmas are grouped into locales corresponding to 
+  system operations, each explained in a separate section.
+*}
+
+text {*
+  The following two lemmas are general about any valid system state, 
+  but are used in the derivation in more specific system operations. 
+*}
 
 context valid_trace
 begin
@@ -40,38 +53,6 @@
 
 end
 
-section {*
-  This file contains lemmas used to guide the recalculation of current precedence 
-  after every system call (or system operation)
-*}
-
-text {* (* ddd *)
-  One beauty of our modelling is that we follow the definitional extension tradition of HOL.
-  The benefit of such a concise and miniature model is that  large number of intuitively 
-  obvious facts are derived as lemmas, rather than asserted as axioms.
-*}
-
-text {*
-  However, the lemmas in the forthcoming several locales are no longer 
-  obvious. These lemmas show how the current precedences should be recalculated 
-  after every execution step (in our model, every step is represented by an event, 
-  which in turn, represents a system call, or operation). Each operation is 
-  treated in a separate locale.
-
-  The complication of current precedence recalculation comes 
-  because the changing of RAG needs to be taken into account, 
-  in addition to the changing of precedence. 
-
-  The reason RAG changing affects current precedence is that,
-  according to the definition, current precedence 
-  of a thread is the maximum of the precedences of every threads in its subtree, 
-  where the notion of sub-tree in RAG is defined in RTree.thy.
-
-  Therefore, for each operation, lemmas about the change of precedences 
-  and RAG are derived first, on which lemmas about current precedence 
-  recalculation are based on.
-*}
-
 section {* The @{term Set} operation *}
 
 context valid_trace_set
diff -r a7441db6f4e1 -r 8a6125caead2 PIPBasics.thy
--- a/PIPBasics.thy	Fri Feb 12 17:50:24 2016 +0800
+++ b/PIPBasics.thy	Sat Feb 13 17:18:51 2016 +0800
@@ -2,6 +2,18 @@
 imports PIPDefs
 begin
 
+text {* (* ddd *)
+  Following the HOL convention of {\em definitional extension}, we have
+  given a concise and miniature model of PIP. To assure ourselves of 
+  the correctness of this model, we are going to derive a series of 
+  expected properties out of it. 
+
+  This file contains the very basic properties, useful for self-assurance, 
+  as well as for deriving more advance properties concerning 
+  the correctness and implementation of PIP.
+*}
+
+
 section {* Generic aulxiliary lemmas *}
 
 lemma rel_eqI: