|
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 |
|
12 open Token; |
|
13 |
|
14 |
|
15 val Token_defs = [WellTyped_def, Token_def, HasTok_def, H_def, E_def, T_def]; |
|
16 |
|
17 AddIffs [N_positive, skip]; |
|
18 |
|
19 goalw thy [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j"; |
|
20 by Auto_tac; |
|
21 qed "HasToK_partition"; |
|
22 |
|
23 goalw thy Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)"; |
|
24 by (Simp_tac 1); |
|
25 by (exhaust_tac "s (Suc i)" 1); |
|
26 by Auto_tac; |
|
27 qed "not_E_eq"; |
|
28 |
|
29 (** We should be able to prove WellTyped as a separate Invariant. Then |
|
30 the Invariant rule should let us assume that the initial |
|
31 state is reachable, and therefore contained in any Invariant. Then |
|
32 we'd not have to mention WellTyped in the statement of this theorem. |
|
33 **) |
|
34 |
|
35 goalw thy [stable_def] |
|
36 "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})"; |
|
37 by (rtac (stable_WT RS stable_constrains_Int) 1); |
|
38 by (cut_facts_tac [TR2,TR4,TR5] 1); |
|
39 by (asm_full_simp_tac (simpset() addsimps [constrains_def]) 1); |
|
40 by (REPEAT_FIRST (rtac ballI ORELSE' (dtac bspec THEN' assume_tac))); |
|
41 by (auto_tac (claset(), simpset() addsimps [not_E_eq])); |
|
42 by (case_tac "xa : HasTok i" 1); |
|
43 by (auto_tac (claset(), simpset() addsimps [H_def, E_def, T_def])); |
|
44 qed "token_stable"; |
|
45 |
|
46 (*This proof is in the "massaging" style and is much faster! *) |
|
47 goalw thy [stable_def] |
|
48 "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))"; |
|
49 by (rtac (stable_WT RS stable_constrains_Int) 1); |
|
50 by (rtac constrains_weaken 1); |
|
51 by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1); |
|
52 by (auto_tac (claset(), simpset() addsimps [not_E_eq])); |
|
53 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def]))); |
|
54 qed "token_stable"; |
|
55 |
|
56 |
|
57 (*** Progress under weak fairness ***) |
|
58 |
|
59 goalw thy [nodeOrder_def] "wf(nodeOrder j)"; |
|
60 by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1); |
|
61 by (Blast_tac 1); |
|
62 qed"wf_nodeOrder"; |
|
63 |
|
64 goal thy "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n"; |
|
65 by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1); |
|
66 by (blast_tac (claset() addEs [less_asym, less_SucE]) 1); |
|
67 qed "Suc_lessI"; |
|
68 |
|
69 goalw thy [nodeOrder_def, next_def, inv_image_def] |
|
70 "!!x. [| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"; |
|
71 by (auto_tac (claset(), |
|
72 simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq])); |
|
73 by (dtac sym 1); |
|
74 (*The next two lines...**) |
|
75 by (REPEAT (eres_inst_tac [("P", "?a<N")] rev_mp 1)); |
|
76 by (etac ssubst 1); |
|
77 (*were with the previous version of asm_full_simp_tac... |
|
78 by (rotate_tac ~1 1); |
|
79 *) |
|
80 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv, mod_Suc, mod_less]) 1); |
|
81 by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1); |
|
82 by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, less_imp_le, Suc_leI, |
|
83 diff_add_assoc]) 2); |
|
84 by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1); |
|
85 by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1); |
|
86 (*including less_asym here would slow things down*) |
|
87 by (auto_tac (claset() delrules [notI], |
|
88 simpset() addsimps [diff_add_assoc2, Suc_leI, |
|
89 less_imp_diff_less, |
|
90 mod_less, mod_geq, nat_neq_iff])); |
|
91 by (REPEAT (blast_tac (claset() addEs [less_asym]) 3)); |
|
92 by (asm_simp_tac (simpset() addsimps [less_imp_diff_less, |
|
93 Suc_diff_n RS sym]) 1); |
|
94 by (asm_simp_tac (simpset() addsimps [add_diff_less, mod_less]) 1); |
|
95 by (etac subst 1); |
|
96 by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1); |
|
97 qed "nodeOrder_eq"; |
|
98 |
|
99 |
|
100 (*From "A Logic for Concurrent Programming", but not used in Chapter 4. |
|
101 Note the use of case_tac. Reasoning about leadsTo takes practice!*) |
|
102 goal thy |
|
103 "!!i. [| i<N; j<N |] ==> \ |
|
104 \ leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)"; |
|
105 by (case_tac "i=j" 1); |
|
106 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
107 by (rtac (TR7 RS leadsTo_weaken_R) 1); |
|
108 by (Clarify_tac 1); |
|
109 by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
|
110 qed "TR7_nodeOrder"; |
|
111 |
|
112 |
|
113 (*Chapter 4 variant, the one actually used below.*) |
|
114 goal thy |
|
115 "!!i. [| i<N; j<N; i~=j |] ==> \ |
|
116 \ leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}"; |
|
117 by (rtac (TR7 RS leadsTo_weaken_R) 1); |
|
118 by (Clarify_tac 1); |
|
119 by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
|
120 qed "TR7_aux"; |
|
121 |
|
122 goal thy "({s. Token s < N} Int Token -`` {m}) = \ |
|
123 \ (if m<N then Token -`` {m} else {})"; |
|
124 by Auto_tac; |
|
125 val Token_lemma = result(); |
|
126 |
|
127 |
|
128 (*Misra's TR9: the token reaches an arbitrary node*) |
|
129 goal thy |
|
130 "!!i. j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)"; |
|
131 by (rtac leadsTo_weaken_R 1); |
|
132 by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")] |
|
133 (wf_nodeOrder RS bounded_induct) 1); |
|
134 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff, |
|
135 HasTok_def]))); |
|
136 by (Blast_tac 2); |
|
137 by (Clarify_tac 1); |
|
138 by (rtac (TR7_aux RS leadsTo_weaken) 1); |
|
139 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def]))); |
|
140 by (ALLGOALS Blast_tac); |
|
141 qed "leadsTo_j"; |
|
142 |
|
143 (*Misra's TR8: a hungry process eventually eats*) |
|
144 goal thy "!!i. j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)"; |
|
145 by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); |
|
146 by (rtac TR6 2); |
|
147 by (rtac leadsTo_weaken_R 1); |
|
148 by (rtac ([leadsTo_j, TR3] MRS PSP) 1); |
|
149 by (ALLGOALS Blast_tac); |
|
150 qed "Token_progress"; |