# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1458569751 0
# Node ID 8d8ed7b9680f85c1aa0e4de30aad4c65b34e4123
# Parent  a4bb5525b7b62e8dd01cf6d4e73025a19a53fa25
updated partially

diff -r a4bb5525b7b6 -r 8d8ed7b9680f PIPBasics.thy
--- a/PIPBasics.thy	Mon Mar 21 14:07:37 2016 +0000
+++ b/PIPBasics.thy	Mon Mar 21 14:15:51 2016 +0000
@@ -156,13 +156,13 @@
   @{term dependants} and @{term cp}.
 *}
 
-lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
-  by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
-
-lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
-  by (unfold s_holding_def wq_def cs_holding_def, simp)
-
-lemma eq_dependants: "dependants (wq s) = dependants s"
+lemma waiting_eq: "waiting s th cs = waiting_raw (wq s) th cs"
+  by  (unfold s_waiting_def cs_waiting_raw wq_def, auto)
+
+lemma holding_eq: "holding (s::state) th cs = holding_raw (wq s) th cs"
+  by (unfold s_holding_def wq_def cs_holding_raw, simp)
+
+lemma eq_dependants: "dependants_raw (wq s) = dependants s"
   by (simp add: s_dependants_abv wq_def)
 
 lemma cp_eq: "cp s th = cpreced (wq s) s th"
@@ -392,8 +392,8 @@
 qed (insert assms, auto simp:cntV_def)
 
 lemma eq_RAG: 
-  "RAG (wq s) = RAG s"
-  by (unfold cs_RAG_def s_RAG_def, auto)
+  "RAG_raw (wq s) = RAG s"
+  by (unfold cs_RAG_raw s_RAG_def, auto)
 
 text {* 
   The following three lemmas shows the shape
@@ -594,12 +594,12 @@
   "cp s th =  
            Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
 proof -
-  have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
+  have "Max (the_preced s ` ({th} \<union> dependants_raw (wq s) th)) =
         Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 
           (is "Max (_ ` ?L) = Max (_ ` ?R)")
   proof -
     have "?L = ?R" 
-    by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
+    by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_raw s_RAG_def subtree_def)
     thus ?thesis by simp
   qed
   thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp)