
diff -r 3a801bbd2687 -r d5e9653fbf19 PIPBasics.thy
--- a/PIPBasics.thy	Wed Feb 03 21:05:15 2016 +0800
+++ b/PIPBasics.thy	Wed Feb 03 21:41:42 2016 +0800
@@ -361,6 +361,23 @@
   "inj_on (the_preced s) (threads s)"
   by (metis inj_onI preced_unique the_preced_def)
 
+lemma holding_next_thI:
+  assumes "holding s th cs"
+  and "length (wq s cs) > 1"
+  obtains th' where "next_th s th cs th'"
+proof -
+  from assms(1)[folded holding_eq, unfolded cs_holding_def]
+  have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" 
+    by (unfold s_holding_def, fold wq_def, auto)
+  then obtain rest where h1: "wq s cs = th#rest" 
+    by (cases "wq s cs", auto)
+  with assms(2) have h2: "rest \<noteq> []" by auto
+  let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
+  have "next_th s th cs ?th'" using  h1(1) h2 
+    by (unfold next_th_def, auto)
+  from that[OF this] show ?thesis .
+qed
+
 (* ccc *)
 
 section {* Locales used to investigate the execution of PIP *}
@@ -2648,6 +2665,30 @@
   } ultimately show ?thesis by auto
 qed
 
+lemma subtree_tRAG_thread:
+  assumes "th \<in> threads s"
+  shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
+proof -
+  have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+    by (unfold tRAG_subtree_eq, simp)
+  also have "... \<subseteq> ?R"
+  proof
+    fix x
+    assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+    then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
+    from this(2)
+    show "x \<in> ?R"
+    proof(cases rule:subtreeE)
+      case 1
+      thus ?thesis by (simp add: assms h(1)) 
+    next
+      case 2
+      thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 
+    qed
+  qed
+  finally show ?thesis .
+qed
+
 lemma dependants_alt_def:
   "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
   by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
@@ -2918,6 +2959,75 @@
   ultimately show ?thesis by auto
 qed
 
+lemma threads_alt_def:
+  "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
+    (is "?L = ?R")
+proof -
+  { fix th1
+    assume "th1 \<in> ?L"
+    from th_chain_to_ready[OF this]
+    have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" .
+    hence "th1 \<in> ?R" by (auto simp:subtree_def)
+  } moreover 
+  { fix th'
+    assume "th' \<in> ?R"
+    then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)"
+      by auto
+    from this(2)
+    have "th' \<in> ?L" 
+    proof(cases rule:subtreeE)
+      case 1
+      with h(1) show ?thesis by (auto simp:readys_def)
+    next
+      case 2
+      from tranclD[OF this(2)[unfolded ancestors_def, simplified]]
+      have "Th th' \<in> Domain (RAG s)" by auto
+      from dm_RAG_threads[OF this]
+      show ?thesis .
+    qed
+  } ultimately show ?thesis by auto
+qed
+
+
+text {* (* ccc *) \noindent
+  Since the current precedence of the threads in ready queue will always be boosted,
+  there must be one inside it has the maximum precedence of the whole system. 
+*}
+lemma max_cp_readys_threads:
+  shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R")
+proof(cases "readys s = {}")
+  case False
+  have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp)
+  also have "... = 
+    Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))" 
+         by (unfold threads_alt_def, simp)
+  also have "... = 
+    Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
+          by (unfold image_UN, simp)
+  also have "... = 
+    Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" 
+  proof(rule Max_UNION)
+    show "\<forall>M\<in>(\<lambda>x. the_preced s ` 
+                    {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
+                        using finite_subtree_threads by auto
+  qed (auto simp:False subtree_def)
+  also have "... =  
+    Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)" 
+      by (unfold image_comp, simp)
+  also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
+  proof -
+    have "(?f ` ?A) = (?g ` ?A)"
+    proof(rule f_image_eq)
+      fix th1 
+      assume "th1 \<in> ?A"
+      thus "?f th1 = ?g th1"
+        by (unfold cp_alt_def, simp)
+    qed
+    thus ?thesis by simp
+  qed
+  finally show ?thesis by simp
+qed (auto simp:threads_alt_def)
+
 end
 
 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *}
@@ -4341,7 +4451,7 @@
 
 end
 
-section {* hhh *}
+section {* Recursive definition of @{term "cp"} *}
 
 lemma cp_alt_def1: 
   "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
@@ -4447,104 +4557,9 @@
     thus ?thesis by (subst (1) h(1), unfold h(2), simp)
   qed
 qed
-
-section {* Relating @{term cp}-values of @{term threads} and @{term readys }*}
-
-lemma threads_alt_def:
-  "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
-    (is "?L = ?R")
-proof -
-  { fix th1
-    assume "th1 \<in> ?L"
-    from th_chain_to_ready[OF this]
-    have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" .
-    hence "th1 \<in> ?R" by (auto simp:subtree_def)
-  } moreover 
-  { fix th'
-    assume "th' \<in> ?R"
-    then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)"
-      by auto
-    from this(2)
-    have "th' \<in> ?L" 
-    proof(cases rule:subtreeE)
-      case 1
-      with h(1) show ?thesis by (auto simp:readys_def)
-    next
-      case 2
-      from tranclD[OF this(2)[unfolded ancestors_def, simplified]]
-      have "Th th' \<in> Domain (RAG s)" by auto
-      from dm_RAG_threads[OF this]
-      show ?thesis .
-    qed
-  } ultimately show ?thesis by auto
-qed
-
-
-text {* (* ccc *) \noindent
-  Since the current precedence of the threads in ready queue will always be boosted,
-  there must be one inside it has the maximum precedence of the whole system. 
-*}
-lemma max_cp_readys_threads:
-  shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R")
-proof(cases "readys s = {}")
-  case False
-  have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp)
-  also have "... = 
-    Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))" 
-         by (unfold threads_alt_def, simp)
-  also have "... = 
-    Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
-          by (unfold image_UN, simp)
-  also have "... = 
-    Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" 
-  proof(rule Max_UNION)
-    show "\<forall>M\<in>(\<lambda>x. the_preced s ` 
-                    {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
-                        using finite_subtree_threads by auto
-  qed (auto simp:False subtree_def)
-  also have "... =  
-    Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)" 
-      by (unfold image_comp, simp)
-  also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
-  proof -
-    have "(?f ` ?A) = (?g ` ?A)"
-    proof(rule f_image_eq)
-      fix th1 
-      assume "th1 \<in> ?A"
-      thus "?f th1 = ?g th1"
-        by (unfold cp_alt_def, simp)
-    qed
-    thus ?thesis by simp
-  qed
-  finally show ?thesis by simp
-qed (auto simp:threads_alt_def)
-
 end
 
-section {* Pending properties *}
-
-lemma next_th_unique: 
-  assumes nt1: "next_th s th cs th1"
-  and nt2: "next_th s th cs th2"
-  shows "th1 = th2"
-using assms by (unfold next_th_def, auto)
-
-lemma holding_next_thI:
-  assumes "holding s th cs"
-  and "length (wq s cs) > 1"
-  obtains th' where "next_th s th cs th'"
-proof -
-  from assms(1)[folded holding_eq, unfolded cs_holding_def]
-  have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" 
-    by (unfold s_holding_def, fold wq_def, auto)
-  then obtain rest where h1: "wq s cs = th#rest" 
-    by (cases "wq s cs", auto)
-  with assms(2) have h2: "rest \<noteq> []" by auto
-  let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
-  have "next_th s th cs ?th'" using  h1(1) h2 
-    by (unfold next_th_def, auto)
-  from that[OF this] show ?thesis .
-qed
+section {* Other properties useful in Implementation.thy or Correctness.thy *}
 
 context valid_trace_e 
 begin
@@ -4554,63 +4569,11 @@
   shows "actor e \<in> runing s"
   using pip_e assms 
   by (induct, auto)
-
 end
 
 context valid_trace
 begin
 
-lemma create_pre:
-  assumes stp: "step s e"
-  and not_in: "th \<notin> threads s"
-  and is_in: "th \<in> threads (e#s)"
-  obtains prio where "e = Create th prio"
-proof -
-  from assms  
-  show ?thesis
-  proof(cases)
-    case (thread_create thread prio)
-    with is_in not_in have "e = Create th prio" by simp
-    from that[OF this] show ?thesis .
-  next
-    case (thread_exit thread)
-    with assms show ?thesis by (auto intro!:that)
-  next
-    case (thread_P thread)
-    with assms show ?thesis by (auto intro!:that)
-  next
-    case (thread_V thread)
-    with assms show ?thesis by (auto intro!:that)
-  next 
-    case (thread_set thread)
-    with assms show ?thesis by (auto intro!:that)
-  qed
-qed
-
-lemma subtree_tRAG_thread:
-  assumes "th \<in> threads s"
-  shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
-proof -
-  have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
-    by (unfold tRAG_subtree_eq, simp)
-  also have "... \<subseteq> ?R"
-  proof
-    fix x
-    assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
-    then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
-    from this(2)
-    show "x \<in> ?R"
-    proof(cases rule:subtreeE)
-      case 1
-      thus ?thesis by (simp add: assms h(1)) 
-    next
-      case 2
-      thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 
-    qed
-  qed
-  finally show ?thesis .
-qed
-
 lemma readys_root:
   assumes "th \<in> readys s"
   shows "root (RAG s) (Th th)"




