--- a/PrioGDef.thy	Wed Mar 12 10:08:20 2014 +0000
+++ b/PrioGDef.thy	Tue May 06 14:36:40 2014 +0100
@@ -68,38 +68,38 @@
   Functions such as @{text "threads"}, which extract information out of system states, are called
   {\em observing functions}. A series of observing functions will be defined in the sequel in order to 
   model the protocol. 
-  Observing function @{text "original_priority"} calculates 
+  Observing function @{text "priority"} calculates 
   the {\em original priority} of thread @{text "th"} in state @{text "s"}, expressed as
-  : @{text "original_priority th s" }. The {\em original priority} is the priority 
+  : @{text "priority th s" }. The {\em original priority} is the priority 
   assigned to a thread when it is created or when it is reset by system call 
   @{text "Set thread priority"}.
 *}
 
-fun original_priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
+fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
   where
   -- {* @{text "0"} is assigned to threads which have never been created: *}
-  "original_priority thread [] = 0" |
-  "original_priority thread (Create thread' prio#s) = 
-     (if thread' = thread then prio else original_priority thread s)" |
-  "original_priority thread (Set thread' prio#s) = 
-     (if thread' = thread then prio else original_priority thread s)" |
-  "original_priority thread (e#s) = original_priority thread s"
+  "priority thread [] = 0" |
+  "priority thread (Create thread' prio#s) = 
+     (if thread' = thread then prio else priority thread s)" |
+  "priority thread (Set thread' prio#s) = 
+     (if thread' = thread then prio else priority thread s)" |
+  "priority thread (e#s) = priority thread s"
 
 text {*
   \noindent
   In the following,
-  @{text "birthtime th s"} is the time when thread @{text "th"} is created, 
+  @{text "last_set th s"} is the time when thread @{text "th"} is created, 
   observed from state @{text "s"}.
   The time in the system is measured by the number of events happened so far since the very beginning.
 *}
-fun birthtime :: "thread \<Rightarrow> state \<Rightarrow> nat"
+fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
   where
-  "birthtime thread [] = 0" |
-  "birthtime thread ((Create thread' prio)#s) = 
-       (if (thread = thread') then length s else birthtime thread s)" |
-  "birthtime thread ((Set thread' prio)#s) = 
-       (if (thread = thread') then length s else birthtime thread s)" |
-  "birthtime thread (e#s) = birthtime thread s"
+  "last_set thread [] = 0" |
+  "last_set thread ((Create thread' prio)#s) = 
+       (if (thread = thread') then length s else last_set thread s)" |
+  "last_set thread ((Set thread' prio)#s) = 
+       (if (thread = thread') then length s else last_set thread s)" |
+  "last_set thread (_#s) = last_set thread s"
 
 text {*
   \noindent 
@@ -110,7 +110,7 @@
   This explains the following definition:
   *}
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
-  where "preced thread s \<equiv> Prc (original_priority thread s) (birthtime thread s)"
+  where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)"
 
 
 text {*
@@ -122,7 +122,7 @@
   holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool" 
   waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
   depend :: "'b \<Rightarrow> (node \<times> node) set"
-  dependents :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
+  dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
 
 text {*
   \noindent
@@ -162,12 +162,12 @@
       {(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}"
   -- {* 
   \begin{minipage}{0.9\textwidth}
-  The following @{text "dependents wq th"} represents the set of threads which are depending on
+  The following @{text "dependants wq th"} represents the set of threads which are depending on
   thread @{text "th"} in Resource Allocation Graph @{text "depend wq"}:
   \end{minipage}
   *}
-  cs_dependents_def: 
-  "dependents (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"
+  cs_dependants_def: 
+  "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"
 
 
 text {*
@@ -185,18 +185,18 @@
   @{text "cpreced s th"} gives the {\em current precedence} of thread @{text "th"} under
   state @{text "s"}. The definition of @{text "cpreced"} reflects the basic idea of 
   Priority Inheritance that the {\em current precedence} of a thread is the precedence 
-  inherited from the maximum of all its dependents, i.e. the threads which are waiting 
+  inherited from the maximum of all its dependants, i.e. the threads which are waiting 
   directly or indirectly waiting for some resources from it. If no such thread exits, 
   @{text "th"}'s {\em current precedence} equals its original precedence, i.e. 
   @{text "preced th s"}.
   *}
 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
-  where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"
+  where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependants wq th)))"
 
 (*<*)
 lemma 
   cpreced_def2:
-  "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
+  "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"
   unfolding cpreced_def image_def
   apply(rule eq_reflection)
   apply(rule_tac f="Max" in arg_cong)
@@ -268,7 +268,7 @@
 lemma cpreced_initial: 
   "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
 apply(simp add: cpreced_def)
-apply(simp add: cs_dependents_def cs_depend_def cs_waiting_def cs_holding_def)
+apply(simp add: cs_dependants_def cs_depend_def cs_waiting_def cs_holding_def)
 apply(simp add: preced_def)
 done
 
@@ -305,7 +305,7 @@
 
 text {* \noindent
   Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and 
-  @{text "dependents"} still have the 
+  @{text "dependants"} still have the 
   same meaning, but redefined so that they no longer depend on the 
   fictitious {\em waiting queue function}
   @{text "wq"}, but on system state @{text "s"}.
@@ -317,8 +317,8 @@
   "waiting (s::state) \<equiv> waiting (wq_fun (schs s))"
   s_depend_abv: 
   "depend (s::state) \<equiv> depend (wq_fun (schs s))"
-  s_dependents_abv: 
-  "dependents (s::state) \<equiv> dependents (wq_fun (schs s))"
+  s_dependants_abv: 
+  "dependants (s::state) \<equiv> dependants (wq_fun (schs s))"
 
 
 text {* 
@@ -339,9 +339,9 @@
   by (auto simp:s_depend_abv wq_def cs_depend_def)
 
 lemma
-  s_dependents_def: 
-  "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
-  by (auto simp:s_dependents_abv wq_def cs_dependents_def)
+  s_dependants_def: 
+  "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
+  by (auto simp:s_dependants_abv wq_def cs_dependants_def)
 
 text {*
   The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready}