1(*  Title:      HOL/UNITY/Simple/Token.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4*)
5
6
7section \<open>The Token Ring\<close>
8
9theory Token
10imports "../WFair"
11
12begin
13
14text\<open>From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.\<close>
15
16subsection\<open>Definitions\<close>
17
18datatype pstate = Hungry | Eating | Thinking
19    \<comment> \<open>process states\<close>
20
21record state =
22  token :: "nat"
23  proc  :: "nat => pstate"
24
25
26definition HasTok :: "nat => state set" where
27    "HasTok i == {s. token s = i}"
28
29definition H :: "nat => state set" where
30    "H i == {s. proc s i = Hungry}"
31
32definition E :: "nat => state set" where
33    "E i == {s. proc s i = Eating}"
34
35definition T :: "nat => state set" where
36    "T i == {s. proc s i = Thinking}"
37
38
39locale Token =
40  fixes N and F and nodeOrder and "next"   
41  defines nodeOrder_def:
42       "nodeOrder j == measure(%i. ((j+N)-i) mod N) \<inter> {..<N} \<times> {..<N}"
43      and next_def:
44       "next i == (Suc i) mod N"
45  assumes N_positive [iff]: "0<N"
46      and TR2:  "F \<in> (T i) co (T i \<union> H i)"
47      and TR3:  "F \<in> (H i) co (H i \<union> E i)"
48      and TR4:  "F \<in> (H i - HasTok i) co (H i)"
49      and TR5:  "F \<in> (HasTok i) co (HasTok i \<union> -(E i))"
50      and TR6:  "F \<in> (H i \<inter> HasTok i) leadsTo (E i)"
51      and TR7:  "F \<in> (HasTok i) leadsTo (HasTok (next i))"
52
53
54lemma HasToK_partition: "[| s \<in> HasTok i; s \<in> HasTok j |] ==> i=j"
55by (unfold HasTok_def, auto)
56
57lemma not_E_eq: "(s \<notin> E i) = (s \<in> H i | s \<in> T i)"
58apply (simp add: H_def E_def T_def)
59apply (cases "proc s i", auto)
60done
61
62context Token
63begin
64
65lemma token_stable: "F \<in> stable (-(E i) \<union> (HasTok i))"
66apply (unfold stable_def)
67apply (rule constrains_weaken)
68apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
69apply (auto simp add: not_E_eq)
70apply (simp_all add: H_def E_def T_def)
71done
72
73
74subsection\<open>Progress under Weak Fairness\<close>
75
76lemma wf_nodeOrder: "wf(nodeOrder j)"
77apply (unfold nodeOrder_def)
78apply (rule wf_measure [THEN wf_subset], blast)
79done
80
81lemma nodeOrder_eq: 
82     "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
83apply (unfold nodeOrder_def next_def)
84apply (auto simp add: mod_Suc mod_geq)
85apply (auto split: nat_diff_split simp add: linorder_neq_iff mod_geq)
86done
87
88text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4.
89  Note the use of \<open>cases\<close>.  Reasoning about leadsTo takes practice!\<close>
90lemma TR7_nodeOrder:
91     "[| i<N; j<N |] ==>    
92      F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
93apply (cases "i=j")
94apply (blast intro: subset_imp_leadsTo)
95apply (rule TR7 [THEN leadsTo_weaken_R])
96apply (auto simp add: HasTok_def nodeOrder_eq)
97done
98
99
100text\<open>Chapter 4 variant, the one actually used below.\<close>
101lemma TR7_aux: "[| i<N; j<N; i\<noteq>j |]     
102      ==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
103apply (rule TR7 [THEN leadsTo_weaken_R])
104apply (auto simp add: HasTok_def nodeOrder_eq)
105done
106
107lemma token_lemma:
108     "({s. token s < N} \<inter> token -` {m}) = (if m<N then token -` {m} else {})"
109by auto
110
111
112text\<open>Misra's TR9: the token reaches an arbitrary node\<close>
113lemma leadsTo_j: "j<N ==> F \<in> {s. token s < N} leadsTo (HasTok j)"
114apply (rule leadsTo_weaken_R)
115apply (rule_tac I = "-{j}" and f = token and B = "{}" 
116       in wf_nodeOrder [THEN bounded_induct])
117apply (simp_all (no_asm_simp) add: token_lemma vimage_Diff HasTok_def)
118 prefer 2 apply blast
119apply clarify
120apply (rule TR7_aux [THEN leadsTo_weaken])
121apply (auto simp add: HasTok_def nodeOrder_def)
122done
123
124text\<open>Misra's TR8: a hungry process eventually eats\<close>
125lemma token_progress:
126     "j<N ==> F \<in> ({s. token s < N} \<inter> H j) leadsTo (E j)"
127apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
128apply (rule_tac [2] TR6)
129apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+)
130done
131
132end
133
134end
135