
diff -r a88af0e4731f -r 38c6acf03f68 Correctness.thy
--- a/Correctness.thy	Tue Jun 07 13:51:39 2016 +0100
+++ b/Correctness.thy	Thu Jun 09 23:01:36 2016 +0100
@@ -498,12 +498,12 @@
   of the blocking thread @{text th'} equals to the highest
   precedence in the whole system.
 *}
-lemma runing_preced_inversion:
-  assumes runing': "th' \<in> runing (t@s)"
+lemma running_preced_inversion:
+  assumes running': "th' \<in> running (t@s)"
   shows "cp (t@s) th' = preced th s" (is "?L = ?R")
 proof -
   have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
-      by (unfold runing_def, auto)
+      by (unfold running_def, auto)
   also have "\<dots> = ?R"
       by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 
   finally show ?thesis .
@@ -525,7 +525,7 @@
   @{text th'}s @{term cp}-value equals to its own precedence.
 
   On the other hand, since @{text th'} is running, by @{thm
-  runing_preced_inversion}, its @{term cp}-value equals to the
+  running_preced_inversion}, its @{term cp}-value equals to the
   precedence of @{term th}.
 
   Combining the above two resukts we have that @{text th'} and @{term
@@ -538,13 +538,13 @@
 lemma eq_pv_blocked: (* ddd *)
   assumes neq_th': "th' \<noteq> th"
   and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
-  shows "th' \<notin> runing (t@s)"
+  shows "th' \<notin> running (t@s)"
 proof
-  assume otherwise: "th' \<in> runing (t@s)"
+  assume otherwise: "th' \<in> running (t@s)"
   show False
   proof -
     have th'_in: "th' \<in> threads (t@s)"
-        using otherwise readys_threads runing_def by auto 
+        using otherwise readys_threads running_def by auto 
     have "th' = th"
     proof(rule preced_unique)
       -- {* The proof goes like this: 
@@ -559,12 +559,12 @@
               equals its @{term preced}-value: *}
         have "?L = cp (t@s) th'"
          by (unfold cp_eq cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp)
-        -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
+        -- {* Since @{term "th'"} is running, by @{thm running_preced_inversion},
               its @{term cp}-value equals @{term "preced th s"}, 
               which equals to @{term "?R"} by simplification: *}
         also have "... = ?R" 
-        thm runing_preced_inversion
-            using runing_preced_inversion[OF otherwise] by simp
+        thm running_preced_inversion
+            using running_preced_inversion[OF otherwise] by simp
         finally show ?thesis .
       qed
     qed (auto simp: th'_in th_kept)
@@ -600,11 +600,11 @@
       from cntP_diff_inv[OF this[simplified]]
       obtain cs' where "e = P th' cs'" by auto
       from vat_es.pip_e[unfolded this]
-      have "th' \<in> runing (t@s)" 
+      have "th' \<in> running (t@s)" 
         by (cases, simp)
       -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis
             shows @{term th'} can not be running at moment  @{term "t@s"}: *}
-      moreover have "th' \<notin> runing (t@s)" 
+      moreover have "th' \<notin> running (t@s)" 
                using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
       -- {* Contradiction is finally derived: *}
       ultimately show False by simp
@@ -618,8 +618,8 @@
       from cntV_diff_inv[OF this[simplified]]
       obtain cs' where "e = V th' cs'" by auto
       from vat_es.pip_e[unfolded this]
-      have "th' \<in> runing (t@s)" by (cases, auto)
-      moreover have "th' \<notin> runing (t@s)"
+      have "th' \<in> running (t@s)" by (cases, auto)
+      moreover have "th' \<notin> running (t@s)"
           using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
       ultimately show False by simp
     qed
@@ -637,7 +637,7 @@
 lemma eq_pv_blocked_persist:
   assumes neq_th': "th' \<noteq> th"
   and eq_pv: "cntP s th' = cntV s th'"
-  shows "th' \<notin> runing (t@s)"
+  shows "th' \<notin> running (t@s)"
   using assms
   by (simp add: eq_pv_blocked eq_pv_persist) 
 
@@ -645,8 +645,8 @@
   The following lemma shows the blocking thread @{term th'}
   must hold some resource in the very beginning. 
 *}
-lemma runing_cntP_cntV_inv: (* ddd *)
-  assumes is_runing: "th' \<in> runing (t@s)"
+lemma running_cntP_cntV_inv: (* ddd *)
+  assumes is_running: "th' \<in> running (t@s)"
   and neq_th': "th' \<noteq> th"
   shows "cntP s th' > cntV s th'"
   using assms
@@ -660,9 +660,9 @@
     -- {* By applying @{thm  eq_pv_blocked_persist} to this: *}
     from eq_pv_blocked_persist[OF neq_th' otherwise] 
     -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *}
-    have "th' \<notin> runing (t@s)" .
-    -- {* This is obvious in contradiction with assumption @{thm is_runing}  *}
-    thus False using is_runing by simp
+    have "th' \<notin> running (t@s)" .
+    -- {* This is obvious in contradiction with assumption @{thm is_running}  *}
+    thus False using is_running by simp
   qed
   -- {* However, the number of @{term V} is always less or equal to @{term P}: *}
   moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto
@@ -677,40 +677,40 @@
 
   The proof is a  simple combination of the results above:
 *}
-lemma runing_threads_inv: 
-  assumes runing': "th' \<in> runing (t@s)"
+lemma running_threads_inv: 
+  assumes running': "th' \<in> running (t@s)"
   and neq_th': "th' \<noteq> th"
   shows "th' \<in> threads s"
 proof(rule ccontr) -- {* Proof by contradiction: *}
   assume otherwise: "th' \<notin> threads s" 
-  have "th' \<notin> runing (t @ s)"
+  have "th' \<notin> running (t @ s)"
   proof -
     from vat_s.cnp_cnv_eq[OF otherwise]
     have "cntP s th' = cntV s th'" .
     from eq_pv_blocked_persist[OF neq_th' this]
     show ?thesis .
   qed
-  with runing' show False by simp
+  with running' show False by simp
 qed
 
 text {*
   The following lemma summarizes several foregoing 
   lemmas to give an overall picture of the blocking thread @{text "th'"}:
 *}
-lemma runing_inversion: (* ddd, one of the main lemmas to present *)
-  assumes runing': "th' \<in> runing (t@s)"
+lemma running_inversion: (* ddd, one of the main lemmas to present *)
+  assumes running': "th' \<in> running (t@s)"
   and neq_th: "th' \<noteq> th"
   shows "th' \<in> threads s"
   and    "\<not>detached s th'"
   and    "cp (t@s) th' = preced th s"
 proof -
-  from runing_threads_inv[OF assms]
+  from running_threads_inv[OF assms]
   show "th' \<in> threads s" .
 next
-  from runing_cntP_cntV_inv[OF runing' neq_th]
+  from running_cntP_cntV_inv[OF running' neq_th]
   show "\<not>detached s th'" using vat_s.detached_eq by simp
 next
-  from runing_preced_inversion[OF runing']
+  from running_preced_inversion[OF running']
   show "cp (t@s) th' = preced th s" .
 qed
 
@@ -723,13 +723,13 @@
 
   Now, since @{term readys}-set is non-empty, there must be
   one in it which holds the highest @{term cp}-value, which, by definition, 
-  is the @{term runing}-thread. However, we are going to show more: this running thread
+  is the @{term running}-thread. However, we are going to show more: this running thread
   is exactly @{term "th'"}.
      *}
 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
-  assumes "th \<notin> runing (t@s)"
+  assumes "th \<notin> running (t@s)"
   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
-                    "th' \<in> runing (t@s)"
+                    "th' \<in> running (t@s)"
 proof -
   -- {* According to @{thm vat_t.th_chain_to_ready}, either 
         @{term "th"} is in @{term "readys"} or there is path leading from it to 
@@ -737,15 +737,15 @@
   have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" 
     using th_kept vat_t.th_chain_to_ready by auto
   -- {* However, @{term th} can not be in @{term readys}, because otherwise, since 
-       @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}
+       @{term th} holds the highest @{term cp}-value, it must be @{term "running"}. *}
   moreover have "th \<notin> readys (t@s)" 
-    using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto 
+    using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto 
   -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in 
         term @{term readys}: *}
   ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
                           and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
   -- {* We are going to show that this @{term th'} is running. *}
-  have "th' \<in> runing (t@s)"
+  have "th' \<in> running (t@s)"
   proof -
     -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
     have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
@@ -783,8 +783,8 @@
     qed 
     -- {* Now, since @{term th'} holds the highest @{term cp} 
           and we have already show it is in @{term readys},
-          it is @{term runing} by definition. *}
-    with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def) 
+          it is @{term running} by definition. *}
+    with `th' \<in> readys (t@s)` show ?thesis by (simp add: running_def) 
   qed
   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
   moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 
@@ -793,26 +793,26 @@
 qed
 
 lemma (* new proof of th_blockedE *)
-  assumes "th \<notin> runing (t @ s)"
+  assumes "th \<notin> running (t @ s)"
   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
-                    "th' \<in> runing (t @ s)"
+                    "th' \<in> running (t @ s)"
 proof -
   
   -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is 
         in @{term "readys"} or there is path in the @{term RAG} leading from 
         it to a thread that is in @{term "readys"}. However, @{term th} cannot 
         be in @{term readys}, because otherwise, since @{term th} holds the 
-        highest @{term cp}-value, it must be @{term "runing"}. This would
+        highest @{term cp}-value, it must be @{term "running"}. This would
         violate our assumption. *}
   have "th \<notin> readys (t @ s)" 
-    using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto 
+    using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto 
   then have "\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" 
     using th_kept vat_t.th_chain_to_ready by auto
   then obtain th' where th'_in: "th' \<in> readys (t@s)"
                     and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
   
   -- {* We are going to first show that this @{term th'} is running. *}
-  have "th' \<in> runing (t @ s)"
+  have "th' \<in> running (t @ s)"
   proof -
     -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}
     have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
@@ -852,8 +852,8 @@
     qed 
 
     -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
-          it is @{term runing} by definition. *}
-    with `th' \<in> readys (t @ s)` show "th' \<in> runing (t @ s)" by (simp add: runing_def) 
+          it is @{term running} by definition. *}
+    with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_def) 
   qed
 
   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
@@ -863,8 +863,8 @@
 qed
 
 lemma th_blockedE_pretty:
-  assumes "th \<notin> runing (t@s)"
-  shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> runing (t@s)"
+  assumes "th \<notin> running (t@s)"
+  shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> running (t@s)"
 using th_blockedE assms by blast
 
 text {*
@@ -873,8 +873,8 @@
   the running thread is obviously @{term th} itself; otherwise, the running
   thread is the @{text th'} given by lemma @{thm th_blockedE}.
 *}
-lemma live: "runing (t@s) \<noteq> {}"
-proof(cases "th \<in> runing (t@s)") 
+lemma live: "running (t@s) \<noteq> {}"
+proof(cases "th \<in> running (t@s)") 
   case True thus ?thesis by auto
 next
   case False
@@ -882,25 +882,25 @@
 qed
 
 lemma blockedE:
-  assumes "th \<notin> runing (t@s)"
+  assumes "th \<notin> running (t@s)"
   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
-                    "th' \<in> runing (t@s)"
+                    "th' \<in> running (t@s)"
                     "th' \<in> threads s"
                     "\<not>detached s th'"
                     "cp (t@s) th' = preced th s"
                     "th' \<noteq> th"
-by (metis assms runing_inversion(2) runing_preced_inversion runing_threads_inv th_blockedE)
+by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE)
 
-lemma detached_not_runing:
+lemma detached_not_running:
   assumes "detached (t@s) th'"
   and "th' \<noteq> th"
-  shows "th' \<notin> runing (t@s)"
+  shows "th' \<notin> running (t@s)"
 proof
-    assume otherwise: "th' \<in> runing (t @ s)"
+    assume otherwise: "th' \<in> running (t @ s)"
     have "cp (t@s) th' = cp (t@s) th"
     proof -
       have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" using otherwise
-          by (simp add:runing_def)
+          by (simp add:running_def)
       moreover have "cp (t@s) th = ..." by (simp add: vat_t.max_cp_readys_threads)
       ultimately show ?thesis by simp
     qed
@@ -911,7 +911,7 @@
     from preced_unique[OF this] 
     have "th' \<in> threads (t @ s) \<Longrightarrow> th \<in> threads (t @ s) \<Longrightarrow> th' = th" .
     moreover have "th' \<in> threads (t@s)" 
-      using otherwise by (unfold runing_def readys_def, auto)
+      using otherwise by (unfold running_def readys_def, auto)
     moreover have "th \<in> threads (t@s)" by (simp add: th_kept) 
     ultimately have "th' = th" by metis
     with assms(2) show False by simp
@@ -945,11 +945,11 @@
   The following lemma shows that the definition of @{term "blockers"} is correct, 
   i.e. blockers do block @{term "th"}. It is a very simple corollary of @{thm blockedE}.
 *}
-lemma runingE:
-  assumes "th' \<in> runing (t@s)"
+lemma runningE:
+  assumes "th' \<in> running (t@s)"
   obtains (is_th) "th' = th"
         | (is_other) "th' \<in> blockers"
-  using assms blockers_def runing_inversion(2) by auto
+  using assms blockers_def running_inversion(2) by auto
 
 text {*
   The following lemma shows that the number of blockers are finite.
@@ -1009,11 +1009,11 @@
       have False
       proof(cases)
         case h: (thread_exit)
-        hence "th' \<in> readys (t@s)" by (auto simp:runing_def)
+        hence "th' \<in> readys (t@s)" by (auto simp:running_def)
         from readys_holdents_detached[OF this h(2)]
         have "detached (t @ s) th'" .
-        from et.detached_not_runing[OF this] assms[unfolded blockers_def]
-        have "th' \<notin> runing (t @ s)" by auto
+        from et.detached_not_running[OF this] assms[unfolded blockers_def]
+        have "th' \<notin> running (t @ s)" by auto
         with h(1) show ?thesis by simp
       qed
     } thus ?thesis by auto
@@ -1094,7 +1094,7 @@
 *}
 lemma actions_th_occs_pre:
   assumes "t = e'#t'"
-  shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t'"
+  shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t'"
   using assms
 proof(induct arbitrary: e' t' rule:ind)
   case h: (Cons e t e' t')
@@ -1111,7 +1111,7 @@
       from ve'.th_no_create[OF _ this]
       have "\<not> isCreate e" by auto
       from PIP_actorE[OF h(2) True this] Nil
-      have "th \<in> runing s" by simp
+      have "th \<in> running s" by simp
       hence "?R = 1" using Nil h by simp
       moreover have "?L = 1" using True Nil by (simp add:actions_of_def)
       ultimately show ?thesis by simp
@@ -1124,7 +1124,7 @@
     case h1: (Cons e1 t1)
     hence eq_t': "t' = e1#t1" using h by simp
     from h(5)[OF h1]
-    have le: "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t1" 
+    have le: "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> running (t' @ s)) t1" 
       (is "?F t \<le> ?G t1") .
     show ?thesis 
     proof(cases "actor e = th")
@@ -1132,7 +1132,7 @@
       from ve'.th_no_create[OF _ this]
       have "\<not> isCreate e" by auto
       from PIP_actorE[OF h(2) True this]
-      have "th \<in> runing (t@s)" by simp
+      have "th \<in> running (t@s)" by simp
       hence "?R = 1 + ?G t1" by (unfold h1 eq_t', simp)
       moreover have "?L = 1 + ?F t" using True by (simp add:actions_of_def)
       ultimately show ?thesis using le by simp
@@ -1149,12 +1149,12 @@
   lemma really needed in later proofs.
 *}
 lemma actions_th_occs:
-  shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t"
+  shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t"
 proof(cases t)
   case (Cons e' t')
   from actions_th_occs_pre[OF this]
-  have "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t'" .
-  moreover have "... \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t" 
+  have "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> running (t' @ s)) t'" .
+  moreover have "... \<le> occs (\<lambda>t'. th \<in> running (t' @ s)) t" 
     by (unfold Cons, auto)
   ultimately show ?thesis by simp
 qed (auto simp:actions_of_def)
@@ -1187,10 +1187,10 @@
   interpret ve :  extend_highest_gen s th prio tm t using h by simp
   interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp
   show ?case (is "?L (e#t) = ?T (e#t) + ?O (e#t) + ?C (e#t)")
-  proof(cases "actor e \<in> runing (t@s)")
+  proof(cases "actor e \<in> running (t@s)")
     case True
     thus ?thesis
-    proof(rule ve.runingE)
+    proof(rule ve.runningE)
       assume 1: "actor e = th"
       have "?T (e#t) = 1 + ?T (t)" using 1 by (simp add:actions_of_def)
       moreover have "?O (e#t) = ?O t" 
@@ -1273,17 +1273,17 @@
 *}
 
 theorem bound_priority_inversion:
-  "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le> 
+  "occs (\<lambda> t'. th \<notin> running (t'@s)) t \<le> 
           1 + (length (actions_of blockers t) + length (filter (isCreate) t))"
    (is "?L \<le> ?R")
 proof - 
-  let ?Q = "(\<lambda> t'. th \<in> runing (t'@s))"
+  let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"
   from occs_le[of ?Q t] 
   have "?L \<le> (1 + length t) - occs ?Q t" by simp
   also have "... \<le> ?R"
   proof -
     have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))
-              \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t" (is "?L1 \<le> ?R1")
+              \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")
     proof -
       have "?L1 = length (actions_of {th} t)" using actions_split by arith
       also have "... \<le> ?R1" using actions_th_occs by simp
@@ -1400,12 +1400,12 @@
           from ve'.blockers_no_create [OF assms _ this]
           have "\<not> isCreate e" by auto
           from PIP_actorE[OF h(2) otherwise this]
-          have "th' \<in> runing (t @ s)" .
-          moreover have "th' \<notin> runing (t @ s)"
+          have "th' \<in> running (t @ s)" .
+          moreover have "th' \<notin> running (t @ s)"
           proof -
             from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp
             from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" .
-            from extend_highest_gen.detached_not_runing[OF h(3) this] assms
+            from extend_highest_gen.detached_not_running[OF h(3) this] assms
             show ?thesis by (auto simp:blockers_def)
           qed
           ultimately show False by simp
@@ -1441,7 +1441,7 @@
   blocked occurrences of the most urgent thread @{term th} is finitely bounded:
 *}
 theorem priority_inversion_is_finite:
-  "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le> 
+  "occs (\<lambda> t'. th \<notin> running (t'@s)) t \<le> 
           1 + ((\<Sum> th' \<in> blockers . span th') + BC)" (is "?L \<le> ?R" is "_ \<le> 1 + (?A + ?B)" )
 proof -
   from bound_priority_inversion




