--- 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