--- a/Journal/Paper.thy	Thu Jun 12 10:14:50 2014 +0100
+++ b/Journal/Paper.thy	Tue Jul 15 17:25:53 2014 +0200
@@ -154,7 +154,7 @@
   error is made in the textbook \cite[Section 2.3.1]{book} which
   specifies for a process that inherited a higher priority and exits a
   critical section ``{\it it resumes the priority it had at the point
-  of entry into the critical section}''.  The same error can also be
+  of entry into the critical section}''.  This error can also be
   found in the more recent textbook \cite[Page 119]{Laplante11} where the
   authors state: ``{\it when [the task] exits the critical section that caused
   the block, it reverts to the priority it had when it entered that

--- a/PrioG.thy	Thu Jun 12 10:14:50 2014 +0100
+++ b/PrioG.thy	Tue Jul 15 17:25:53 2014 +0200
@@ -1542,8 +1542,8 @@
           with eq_e
           have eq_readys: "(th \<in> readys (e#s)) = (th \<in> readys (s))"
             apply (simp add:readys_def s_waiting_def wq_def Let_def)
-            apply (rule_tac hh, clarify)
-            apply (intro iffI allI, clarify)
+            apply (rule_tac hh)
+             apply (intro iffI allI, clarify)
             apply (erule_tac x = csa in allE, auto)
             apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto)
             apply (erule_tac x = cs in allE, auto)
@@ -2069,6 +2069,7 @@
 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
 unfolding cp_def wq_def
 apply(induct s rule: schs.induct)
+thm cpreced_initial
 apply(simp add: Let_def cpreced_initial)
 apply(simp add: Let_def)
 apply(simp add: Let_def)
@@ -2088,12 +2089,17 @@
   shows "th1 = th2"
 proof -
   from runing_1 and runing_2 have "cp s th1 = cp s th2"
-    by (unfold runing_def, simp)
+    unfolding runing_def
+    apply(simp)
+    done
   hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) =
                  Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))"
     (is "Max (?f ` ?A) = Max (?f ` ?B)")
-    by (unfold cp_eq_cpreced cpreced_def)
+    thm cp_def image_Collect
+    unfolding cp_eq_cpreced 
+    unfolding cpreced_def .
   obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"
+    thm Max_in
   proof -
     have h1: "finite (?f ` ?A)"
     proof -
@@ -2128,9 +2134,15 @@
       have "?A \<noteq> {}" by simp
       thus ?thesis by simp
     qed
+    thm Max_in
     from Max_in [OF h1 h2]
     have "Max (?f ` ?A) \<in> (?f ` ?A)" .
-    thus ?thesis by (auto intro:that)
+    thus ?thesis 
+      thm cpreced_def
+      unfolding cpreced_def[symmetric] 
+      unfolding cp_eq_cpreced[symmetric] 
+      unfolding cpreced_def 
+      using that[intro] by (auto)
   qed
   obtain th2' where th2_in: "th2' \<in> ?B" and eq_f_th2: "?f th2' = Max (?f ` ?B)"
   proof -
@@ -2273,6 +2285,8 @@
 apply(subgoal_tac "finite (runing s)")
 prefer 2
 apply (metis finite_nat_set_iff_bounded lessI runing_unique)
+apply(rule ccontr)
+apply(simp)
 apply(case_tac "Suc (Suc 0) \<le> card (runing s)")
 apply(subst (asm) card_le_Suc_iff)
 apply(simp)

--- a/Test.thy	Thu Jun 12 10:14:50 2014 +0100
+++ b/Test.thy	Tue Jul 15 17:25:53 2014 +0200
@@ -39,6 +39,9 @@
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
   where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
 
+abbreviation 
+  "preceds s ths \<equiv> {preced th s | th. th \<in> ths}"
+ 
 definition
   "holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)"
 
@@ -504,30 +507,34 @@
   ultimately show "False" by metis
 qed
 
-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
+lemma cpreced2_cpreced: "cpreced2 s th = cpreced (wq s) s th"
+unfolding cpreced2_def wq_def
+apply(induct s rule: schs.induct)
+apply(simp add: Let_def cpreced_def dependants_def RAG_def waits_def holds_def preced_def)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+done
+
+lemma cpreced_Exit:
+  shows "cpreced2 (Exit th # s) th' = cpreced2 s th'"
+by (simp add: cpreced2_cpreced cpreced_def preced_def wq_def Let_def)
 
 lemma readys_Exit:
-  shows "readys (Exit th # s) \<subseteq> readys s"
+  shows "readys (Exit th # s) = readys s - {th}"
 by (auto simp add: readys_def waits2_def Let_def)
 
 lemma readys_Create:
   shows "readys (Create th prio # s) \<subseteq> {th} \<union> readys s"
-by (auto simp add: readys_def waits2_def Let_def)
+apply (auto simp add: readys_def waits2_def Let_def waits_def)
+done
 
 lemma readys_Set:
-  shows "readys (Set th prio # s) \<subseteq> readys s"
+  shows "readys (Set th prio # s) = readys s"
 by (auto simp add: readys_def waits2_def Let_def)
 
 
@@ -549,20 +556,232 @@
 apply(auto simp add: readys_def waits2_def waits_def Let_def wq_def)
 done
 
-lemma 
+
+fun the_th :: "node \<Rightarrow> thread"
+  where "the_th (Th th) = th"
+
+lemma image_Collect2:
+  "f ` A = {f x | x. x \<in> A}"
+apply(auto)
+done
+
+lemma Collect_disj_eq2:
+  "{f x | x. x = y \<or> x \<in> A} = {f y} \<union> {f x | x. x \<in> A}"
+by (auto)
+
+lemma last_set_lt: 
+  "th \<in> threads s \<Longrightarrow> last_set th s < length s"
+  apply(induct rule: threads.induct)
+  apply(auto)
+  done
+
+lemma last_set_eq_iff: 
+  assumes "th1 \<in> threads s" "th2 \<in> threads s"
+  shows "last_set th1 s = last_set th2 s \<longleftrightarrow> th1 = th2"
+  using assms
+  apply(induct s rule: threads.induct) 
+  apply(auto split:if_splits dest:last_set_lt)
+  done
+
+lemma preced_eq_iff: 
+  assumes th_in1: "th1 \<in> threads s"
+  and th_in2: "th2 \<in> threads s"
+  shows "preced th1 s = preced th2 s \<longleftrightarrow> th1 = th2"
+using assms
+by (auto simp add: preced_def last_set_eq_iff)
+
+lemma dm_RAG_threads:
+  assumes vt: "vt s"
+  and in_dom: "(Th th) \<in> Domain (RAG2 s)"
+  shows "th \<in> threads s"
+proof -
+  from in_dom obtain n where a: "(Th th, n) \<in> RAG2 s" by auto
+  then obtain cs where "n = Cs cs" 
+    unfolding RAG2_def RAG_def
+    by auto
+  then have "(Th th, Cs cs) \<in> RAG2 s" using a by simp
+  hence "th \<in> set (wq s cs)"
+    unfolding RAG2_def wq_def RAG_def waits_def
+    by (auto)
+  then show ?thesis
+    apply(rule_tac wq_threads)
+    apply(rule assms)
+    apply(simp)
+    done
+qed
+
+lemma cpreced_eq_iff:
+  assumes "th1 \<in> readys s" "th2 \<in> readys s" "vt s"
+  shows "cpreced2 s th1 = cpreced2 s th2 \<longleftrightarrow> th1 = th2" 
+proof 
+  def S1\<equiv>"({th1} \<union> dependants (wq s) th1)"
+  def S2\<equiv>"({th2} \<union> dependants (wq s) th2)"
+  have fin: "finite ((the_th o fst) ` ((RAG (wq s))\<^sup>+))" 
+      apply(rule)
+      apply(simp add: finite_trancl)
+      apply(simp add: wq_def)
+      apply(rule finite_RAG[simplified RAG2_def])
+      apply(rule assms)
+      done
+
+  from fin have h: "finite (preceds s S1)" "finite (preceds s S2)"
+      apply(simp_all add: S2_def S1_def Collect_disj_eq2 image_Collect[symmetric])
+      apply(rule)
+      apply(simp add: dependants_def)  
+      apply(rule rev_finite_subset)
+      apply(assumption)
+      apply(auto simp add: image_def)[1]
+      apply(metis fst_conv the_th.simps)
+      apply(rule)
+      apply(simp add: dependants_def)  
+      apply(rule rev_finite_subset)
+      apply(assumption)
+      apply(auto simp add: image_def)[1]
+      apply(metis fst_conv the_th.simps)
+      done
+    moreover have "S1 \<noteq> {}" "S2 \<noteq> {}" by (simp_all add: S1_def S2_def)
+    then have "(preceds s S1) \<noteq> {}" "(preceds s S2) \<noteq> {}" by simp_all
+    ultimately have m: "Max (preceds s S1) \<in> (preceds s S1)" "Max (preceds s S2) \<in> (preceds s S2)"
+      apply(rule_tac [!] Max_in)
+      apply(simp_all)
+      done
+
+  assume q: "cpreced2 s th1 = cpreced2 s th2"
+  then have eq_max: "Max (preceds s S1) = Max (preceds s S2)"
+    unfolding cpreced2_cpreced cpreced_def
+    apply(simp only: S1_def S2_def)
+    apply(simp add: Collect_disj_eq2)
+    done
+ 
+  obtain th0 where th0_in: "th0 \<in> S1" "th0 \<in> S2" and 
+      eq_f_th1: "preced th0 s = Max (preceds s S1)"
+                "preced th0 s = Max (preceds s S2)"
+    using m 
+      apply(clarify)
+      apply(simp add: eq_max)
+      apply(subst (asm) (2)  preced_eq_iff)
+      apply(insert assms(2))[1]
+      apply(simp add: S2_def)
+      apply(auto)[1]
+      apply (metis contra_subsetD readys_threads)
+      apply(simp add: dependants_def)
+      apply(subgoal_tac "Th tha \<in> Domain ((RAG2 s)^+)")
+      apply(simp add: trancl_domain)
+      apply (metis Domain_RAG_threads assms(3))
+      apply(simp only: RAG2_def wq_def)
+      apply (metis Domain_iff)
+      apply(insert assms(1))[1]
+      apply(simp add: S1_def)
+      apply(auto)[1]
+      apply (metis contra_subsetD readys_threads)
+      apply(simp add: dependants_def)
+      apply(subgoal_tac "Th th \<in> Domain ((RAG2 s)^+)")
+      apply(simp add: trancl_domain)
+      apply (metis Domain_RAG_threads assms(3))
+      apply(simp only: RAG2_def wq_def)
+      apply (metis Domain_iff)
+      apply(simp)
+    done
+  then show "th1 = th2"
+    apply -
+    apply(insert th0_in assms(1, 2))[1]
+    apply(simp add: S1_def S2_def)
+    apply(auto)
+    --"first case"
+    prefer 2
+    apply(subgoal_tac "Th th2 \<in> Domain (RAG2 s)")
+    apply(subgoal_tac "\<exists>cs. (Th th2, Cs cs) \<in> RAG2 s")
+    apply(erule exE)
+    apply(simp add: runing_def RAG2_def RAG_def readys_def waits2_def)[1]
+    apply(auto simp add: RAG2_def RAG_def)[1]
+    apply(subgoal_tac "Th th2 \<in> Domain ((RAG2 s)^+)")
+    apply (metis trancl_domain)
+    apply(subgoal_tac "(Th th2, Th th1) \<in> (RAG2 s)^+")
+    apply (metis Domain_iff)
+    apply(simp add: dependants_def RAG2_def wq_def)
+    --"second case"
+    apply(subgoal_tac "Th th1 \<in> Domain (RAG2 s)")
+    apply(subgoal_tac "\<exists>cs. (Th th1, Cs cs) \<in> RAG2 s")
+    apply(erule exE)
+    apply(insert assms(1))[1]
+    apply(simp add: runing_def RAG2_def RAG_def readys_def waits2_def)[1]
+    apply(auto simp add: RAG2_def RAG_def)[1]
+    apply(subgoal_tac "Th th1 \<in> Domain ((RAG2 s)^+)")
+    apply (metis trancl_domain)
+    apply(subgoal_tac "(Th th1, Th th2) \<in> (RAG2 s)^+")
+    apply (metis Domain_iff)
+    apply(simp add: dependants_def RAG2_def wq_def)
+    --"third case"
+    apply(rule dchain_unique)
+    apply(rule assms(3))
+    apply(simp add: dependants_def RAG2_def wq_def)
+    apply(simp)
+    apply(simp add: dependants_def RAG2_def wq_def)
+    apply(simp)
+    done
+next
+  assume "th1 = th2"
+  then show "cpreced2 s th1 = cpreced2 s th2" by simp
+qed
+
+lemma at_most_one_running:
   assumes "vt s"
   shows "card (runing s) \<le> 1"
 proof (rule ccontr)
   assume "\<not> card (runing s) \<le> 1"
   then have "2 \<le> card (runing s)" by auto
   moreover 
-  have "finite (runing s)" sorry
-  ultimately obtain th1 th2 where "th1 \<noteq> th2" "th1 \<in> runing s" "th2 \<in> runing s"
-    by (auto simp add: numerals card_le_Suc_iff) (blast)
+  have "finite (runing s)"
+    by (metis `\<not> card (runing s) \<le> 1` card_infinite le0)
+  ultimately obtain th1 th2 where a: 
+    "th1 \<noteq> th2" "th1 \<in> runing s" "th2 \<in> runing s" 
+    "cpreced2 s th1 = cpreced2 s th2" 
+    apply(auto simp add: numerals card_le_Suc_iff runing_def) 
+    apply(blast)
+    done
+  then have "th1 = th2"
+    apply(subst (asm) cpreced_eq_iff)
+    apply(auto intro: assms a)
+    apply (metis contra_subsetD runing_ready)+
+    done
+  then show "False" using a(1) by auto
+qed
 
-  show "False"
-apply(simp)
-oops  
+
+
+
+done
 
 
+  (*
+  obtain th0 where th0_in: "th0 \<in> S1 \<and> th0 \<in> S2" 
+    and eq_f_th0: "preced th0 s = Max ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"
+  proof -
+    from fin have h1: "finite ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"
+      apply(simp only: S1_def S2_def)
+      apply(rule)
+      apply(rule)
+      apply(rule)
+      apply(simp add: dependants_def) 
+      apply(rule rev_finite_subset)
+      apply(assumption)
+      apply(auto simp add: image_def)
+      apply (metis fst_conv the_th.simps)
+      done
+    moreover 
+    have "S1 \<inter> S2 \<noteq> {}" apply (simp add: S1_def S2_def) 
+      apply(auto) 
+      
+      done
+    then have h2: "((\<lambda>th. preced th s) ` (S1 \<union> S2)) \<noteq> {}" by simp
+    ultimately have "Max ((\<lambda>th. preced th s) ` (S1 \<union> S2)) \<in> ((\<lambda>th. preced th s) ` (S1 \<union> S2))"
+      apply(rule Max_in)
+      done
+    then show ?thesis using that[intro] apply(auto) 
+      
+      apply(erule_tac preced_unique)
+      done
+  qed
+  *)
+
 end
\ No newline at end of file

Binary file journal.pdf has changed