--- a/CpsG.thy	Tue Oct 06 18:52:04 2015 +0800
+++ b/CpsG.thy	Sat Oct 17 16:10:33 2015 +0800
@@ -1,8 +1,12 @@
-
+section {*
+  This file contains lemmas used to guide the recalculation of current precedence 
+  after every system call (or system operation)
+*}
 theory CpsG
 imports PrioG Max
 begin
 
+(* obvious lemma *)
 lemma not_thread_holdents:
   fixes th s
   assumes vt: "vt s"
@@ -126,8 +130,7 @@
   qed
 qed
 
-
-
+(* obvious lemma *)
 lemma next_th_neq: 
   assumes vt: "vt s"
   and nt: "next_th s th cs th'"
@@ -155,6 +158,7 @@
   qed
 qed
 
+(* obvious lemma *)
 lemma next_th_unique: 
   assumes nt1: "next_th s th cs th1"
   and nt2: "next_th s th cs th2"
@@ -170,8 +174,6 @@
   from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
 qed
 
-
-
 definition child :: "state \<Rightarrow> (node \<times> node) set"
   where "child s \<equiv>
             {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
@@ -310,11 +312,15 @@
   qed
 qed
 
+text {* (* ??? *)
+*}
 lemma child_RAG_eq: 
   assumes vt: "vt s"
   shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
   by (auto intro: RAG_child[OF vt] child_RAG_p)
 
+text {* (* ??? *)
+*}
 lemma children_no_dep:
   fixes s th th1 th2 th3
   assumes vt: "vt s"
@@ -348,6 +354,8 @@
   qed
 qed
 
+text {* (* ??? *)
+*}
 lemma unique_RAG_p:
   assumes vt: "vt s"
   and dp1: "(n, n1) \<in> (RAG s)^+"
@@ -359,6 +367,8 @@
   show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
 qed
 
+text {* (* ??? *)
+*}
 lemma dependants_child_unique:
   fixes s th th1 th2 th3
   assumes vt: "vt s"
@@ -395,6 +405,8 @@
   apply (unfold children_def)
   by (metis assms(2) children_def RAG_children eq_RAG)
 
+text {* (* ??? *)
+*}
 lemma dependants_expand:
   assumes "vt s"
   shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
@@ -435,6 +447,8 @@
   shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
 by auto
 
+text {* (* ??? *)
+*}
 lemma cp_rec:
   fixes s th
   assumes vt: "vt s"
@@ -902,8 +916,6 @@
 qed
 
 
-
-
 locale step_v_cps =
   fixes s' th cs s 
   defines s_def : "s \<equiv> (V th cs#s')"