# HG changeset patch
# User paulson
# Date 1111576107 -3600
# Node ID 05bad476e0f0f159482b1f6f8ff8e6c149474aea
# Parent  4c7bba41483afde238b33a2749d4811c0b6d878b
tidied

diff -r 4c7bba41483a -r 05bad476e0f0 src/HOL/UNITY/Simple/Token.thy
--- a/src/HOL/UNITY/Simple/Token.thy	Tue Mar 22 16:32:25 2005 +0100
+++ b/src/HOL/UNITY/Simple/Token.thy	Wed Mar 23 12:08:27 2005 +0100
@@ -2,17 +2,22 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
-
-The Token Ring.
-
-From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
 *)
 
 
-theory Token = WFair:
+header {*The Token Ring*}
+
+theory Token
+imports "../WFair"
+
+begin
 
-(*process states*)
+text{*From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.*}
+
+subsection{*Definitions*}
+
 datatype pstate = Hungry | Eating | Thinking
+    --{*process states*}
 
 record state =
   token :: "nat"
@@ -36,8 +41,7 @@
 locale Token =
   fixes N and F and nodeOrder and "next"   
   defines nodeOrder_def:
-       "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
-	 	       (lessThan N <*> lessThan N)"
+       "nodeOrder j == measure(%i. ((j+N)-i) mod N) \<inter> {..<N} \<times> {..<N}"
       and next_def:
        "next i == (Suc i) mod N"
   assumes N_positive [iff]: "0<N"
@@ -66,22 +70,22 @@
 done
 
 
-(*** Progress under weak fairness ***)
+subsection{*Progress under Weak Fairness*}
 
 lemma (in Token) wf_nodeOrder: "wf(nodeOrder j)"
 apply (unfold nodeOrder_def)
-apply (rule wf_less_than [THEN wf_inv_image, THEN wf_subset], blast)
+apply (rule wf_measure [THEN wf_subset], blast)
 done
 
 lemma (in Token) nodeOrder_eq: 
      "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
-apply (unfold nodeOrder_def next_def inv_image_def)
+apply (unfold nodeOrder_def next_def measure_def inv_image_def)
 apply (auto simp add: mod_Suc mod_geq)
 apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
 done
 
-(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
-  Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
+text{*From "A Logic for Concurrent Programming", but not used in Chapter 4.
+  Note the use of @{text case_tac}.  Reasoning about leadsTo takes practice!*}
 lemma (in Token) TR7_nodeOrder:
      "[| i<N; j<N |] ==>    
       F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
@@ -92,7 +96,7 @@
 done
 
 
-(*Chapter 4 variant, the one actually used below.*)
+text{*Chapter 4 variant, the one actually used below.*}
 lemma (in Token) TR7_aux: "[| i<N; j<N; i\<noteq>j |]     
       ==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
 apply (rule TR7 [THEN leadsTo_weaken_R])
@@ -104,7 +108,7 @@
 by auto
 
 
-(*Misra's TR9: the token reaches an arbitrary node*)
+text{*Misra's TR9: the token reaches an arbitrary node*}
 lemma  (in Token) leadsTo_j: "j<N ==> F \<in> {s. token s < N} leadsTo (HasTok j)"
 apply (rule leadsTo_weaken_R)
 apply (rule_tac I = "-{j}" and f = token and B = "{}" 
@@ -116,7 +120,7 @@
 apply (auto simp add: HasTok_def nodeOrder_def)
 done
 
-(*Misra's TR8: a hungry process eventually eats*)
+text{*Misra's TR8: a hungry process eventually eats*}
 lemma (in Token) token_progress:
      "j<N ==> F \<in> ({s. token s < N} \<inter> H j) leadsTo (E j)"
 apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])