--- a/PrioG.thy	Fri May 30 07:56:39 2014 +0100
+++ b/PrioG.thy	Mon Jun 02 14:58:42 2014 +0100
@@ -804,19 +804,6 @@
   apply(auto)
   done
 
-(* FIXME: Unused
-lemma simple_A:
-  fixes A
-  assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"
-  shows "A = {} \<or> (\<exists> a. A = {a})"
-proof(cases "A = {}")
-  case True thus ?thesis by simp
-next
-  case False then obtain a where "a \<in> A" by auto
-  with h have "A = {a}" by auto
-  thus ?thesis by simp
-qed
-*)
 
 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
   by (unfold s_RAG_def, auto)
@@ -2092,7 +2079,7 @@
 apply(simp add: Let_def)
 done
 
-
+(* FIXME: NOT NEEDED *)
 lemma runing_unique:
   fixes th1 th2 s
   assumes vt: "vt s"
@@ -2281,6 +2268,7 @@
   qed
 qed
 
+
 lemma create_pre:
   assumes stp: "step s e"
   and not_in: "th \<notin> threads s"

--- a/ROOT	Fri May 30 07:56:39 2014 +0100
+++ b/ROOT	Mon Jun 02 14:58:42 2014 +0100
@@ -1,7 +1,8 @@
 session "PIP" = HOL +
   theories [document = false]
 	"CpsG" 
-	"ExtGG" 
+	"ExtGG"
+        "Test" 
 
 session "Slides2" in "Slides" = PIP +
   options [document_variants="slides2"]

--- a/Test.thy	Fri May 30 07:56:39 2014 +0100
+++ b/Test.thy	Mon Jun 02 14:58:42 2014 +0100
@@ -350,7 +350,70 @@
 qed (simp_all)
 
 
+lemma finite_RAG:
+  assumes "vt s"
+  shows "finite (RAG2 s)"
+using assms
+apply(induct)
+apply(simp add: RAG2_def RAG_def waits_def holds_def)
+apply(erule step.cases)
+apply(auto)
+apply(case_tac "wq sa cs = []")
+apply(rule finite_subset)
+apply(rule RAG_p1)
+apply(simp)
+apply(simp)
+apply(rule finite_subset)
+apply(rule RAG_p2)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(subgoal_tac "\<exists>wts. wq sa cs = th # wts")
+apply(erule exE)
+apply(case_tac "wts = []")
+apply(rule finite_subset)
+apply(rule RAG_v1)
+apply(simp)
+apply(simp)
+apply(rule finite_subset)
+apply(rule RAG_v2)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(subgoal_tac "th \<in> set (wq sa cs) \<and> th = hd (wq sa cs)") 
+apply(case_tac "wq sa cs") 
+apply(auto)[2]
+apply(auto simp add: holds2_def holds_def wq_def)
+done
+
+lemma wq_threads: 
+  assumes vt: "vt s"
+  and h: "th \<in> set (wq s cs)"
+  shows "th \<in> threads s"
+using assms
+apply(induct)
+apply(simp add: wq_def)
+apply(erule step.cases)
+apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def)
+apply(simp add: waits_def)
+apply(auto simp add: waits_def split: if_splits)[1]
+apply(auto split: if_splits)
+apply(simp only: waits_def)
+by (metis insert_iff set_simps(2))
+
+lemma max_cpreceds_readys_threads:
+  assumes vt: "vt s"
+  shows "Max (cpreceds2 s (readys s)) = Max (cpreceds2 s (threads s))"
+apply(case_tac "threads s = {}")
+apply(simp add: readys_def)
+using vt
+apply(induct)
+apply(simp)
+apply(erule step.cases)
+apply(auto simp add: readys_def waits2_def waits_def Let_def holding_def runing_def holds2_def)
+defer
+defer
+oops
 
 
-
-
+end
\ No newline at end of file

Binary file journal.pdf has changed