|
1 (* Title: HOL/UNITY/Token |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 The Token Ring. |
|
7 |
|
8 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2. |
|
9 *) |
|
10 |
|
11 val Token_defs = [HasTok_def, H_def, E_def, T_def]; |
|
12 |
|
13 Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j"; |
|
14 by Auto_tac; |
|
15 qed "HasToK_partition"; |
|
16 |
|
17 Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)"; |
|
18 by (Simp_tac 1); |
|
19 by (case_tac "proc s i" 1); |
|
20 by Auto_tac; |
|
21 qed "not_E_eq"; |
|
22 |
|
23 Open_locale "Token"; |
|
24 |
|
25 val TR2 = thm "TR2"; |
|
26 val TR3 = thm "TR3"; |
|
27 val TR4 = thm "TR4"; |
|
28 val TR5 = thm "TR5"; |
|
29 val TR6 = thm "TR6"; |
|
30 val TR7 = thm "TR7"; |
|
31 val nodeOrder_def = thm "nodeOrder_def"; |
|
32 val next_def = thm "next_def"; |
|
33 |
|
34 AddIffs [thm "N_positive"]; |
|
35 |
|
36 Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))"; |
|
37 by (rtac constrains_weaken 1); |
|
38 by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1); |
|
39 by (auto_tac (claset(), simpset() addsimps [not_E_eq])); |
|
40 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def]))); |
|
41 qed "token_stable"; |
|
42 |
|
43 |
|
44 (*** Progress under weak fairness ***) |
|
45 |
|
46 Goalw [nodeOrder_def] "wf(nodeOrder j)"; |
|
47 by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1); |
|
48 by (Blast_tac 1); |
|
49 qed"wf_nodeOrder"; |
|
50 |
|
51 Goalw [nodeOrder_def, next_def, inv_image_def] |
|
52 "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"; |
|
53 by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq])); |
|
54 by (auto_tac (claset(), |
|
55 simpset() addsplits [nat_diff_split] |
|
56 addsimps [linorder_neq_iff, mod_geq])); |
|
57 qed "nodeOrder_eq"; |
|
58 |
|
59 (*From "A Logic for Concurrent Programming", but not used in Chapter 4. |
|
60 Note the use of case_tac. Reasoning about leadsTo takes practice!*) |
|
61 Goal "[| i<N; j<N |] ==> \ |
|
62 \ F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)"; |
|
63 by (case_tac "i=j" 1); |
|
64 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
65 by (rtac (TR7 RS leadsTo_weaken_R) 1); |
|
66 by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq])); |
|
67 qed "TR7_nodeOrder"; |
|
68 |
|
69 |
|
70 (*Chapter 4 variant, the one actually used below.*) |
|
71 Goal "[| i<N; j<N; i~=j |] \ |
|
72 \ ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}"; |
|
73 by (rtac (TR7 RS leadsTo_weaken_R) 1); |
|
74 by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq])); |
|
75 qed "TR7_aux"; |
|
76 |
|
77 Goal "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})"; |
|
78 by Auto_tac; |
|
79 val token_lemma = result(); |
|
80 |
|
81 |
|
82 (*Misra's TR9: the token reaches an arbitrary node*) |
|
83 Goal "j<N ==> F : {s. token s < N} leadsTo (HasTok j)"; |
|
84 by (rtac leadsTo_weaken_R 1); |
|
85 by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")] |
|
86 (wf_nodeOrder RS bounded_induct) 1); |
|
87 by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff, |
|
88 HasTok_def]))); |
|
89 by (Blast_tac 2); |
|
90 by (Clarify_tac 1); |
|
91 by (rtac (TR7_aux RS leadsTo_weaken) 1); |
|
92 by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def])); |
|
93 qed "leadsTo_j"; |
|
94 |
|
95 (*Misra's TR8: a hungry process eventually eats*) |
|
96 Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)"; |
|
97 by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); |
|
98 by (rtac TR6 2); |
|
99 by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1); |
|
100 by (ALLGOALS Blast_tac); |
|
101 qed "token_progress"; |