author | paulson |
Tue, 01 Sep 1998 15:07:11 +0200 | |
changeset 5420 | b48ab3281944 |
parent 5277 | e4297d03e5d2 |
child 5490 | 85855f65d0c6 |
permissions | -rw-r--r-- |
4776 | 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 |
||
5232 | 11 |
val Token_defs = [HasTok_def, H_def, E_def, T_def]; |
4776 | 12 |
|
5111 | 13 |
Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j"; |
4776 | 14 |
by Auto_tac; |
15 |
qed "HasToK_partition"; |
|
16 |
||
5232 | 17 |
Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)"; |
4776 | 18 |
by (Simp_tac 1); |
5232 | 19 |
by (exhaust_tac "proc s i" 1); |
4776 | 20 |
by Auto_tac; |
21 |
qed "not_E_eq"; |
|
22 |
||
5420 | 23 |
Open_locale "Token"; |
24 |
||
25 |
(*Strip meta-quantifiers: perhaps the locale should do this?*) |
|
26 |
val TR2 = forall_elim_vars 0 (thm "TR2"); |
|
27 |
val TR3 = forall_elim_vars 0 (thm "TR3"); |
|
28 |
val TR4 = forall_elim_vars 0 (thm "TR4"); |
|
29 |
val TR5 = forall_elim_vars 0 (thm "TR5"); |
|
30 |
val TR6 = forall_elim_vars 0 (thm "TR6"); |
|
31 |
val TR7 = forall_elim_vars 0 (thm "TR7"); |
|
32 |
val nodeOrder_def = (thm "nodeOrder_def"); |
|
33 |
val next_def = (thm "next_def"); |
|
34 |
||
35 |
AddIffs [thm "N_positive", thm"skip"]; |
|
36 |
||
5253 | 37 |
Goalw [stable_def] "stable acts (Compl(E i) Un (HasTok i))"; |
4776 | 38 |
by (rtac constrains_weaken 1); |
39 |
by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1); |
|
40 |
by (auto_tac (claset(), simpset() addsimps [not_E_eq])); |
|
41 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def]))); |
|
42 |
qed "token_stable"; |
|
43 |
||
44 |
||
45 |
(*** Progress under weak fairness ***) |
|
46 |
||
5069 | 47 |
Goalw [nodeOrder_def] "wf(nodeOrder j)"; |
4776 | 48 |
by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1); |
49 |
by (Blast_tac 1); |
|
50 |
qed"wf_nodeOrder"; |
|
51 |
||
5069 | 52 |
Goalw [nodeOrder_def, next_def, inv_image_def] |
5111 | 53 |
"[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"; |
4776 | 54 |
by (auto_tac (claset(), |
55 |
simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq])); |
|
56 |
by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1); |
|
5420 | 57 |
by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, |
4776 | 58 |
diff_add_assoc]) 2); |
59 |
by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1); |
|
60 |
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1); |
|
5420 | 61 |
by (auto_tac (claset(), |
62 |
simpset() addsimps [diff_add_assoc2, nat_neq_iff, |
|
63 |
Suc_le_eq, Suc_diff_Suc, less_imp_diff_less, |
|
64 |
add_diff_less, mod_less, mod_geq])); |
|
4776 | 65 |
by (etac subst 1); |
66 |
by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1); |
|
67 |
qed "nodeOrder_eq"; |
|
68 |
||
69 |
||
70 |
(*From "A Logic for Concurrent Programming", but not used in Chapter 4. |
|
71 |
Note the use of case_tac. Reasoning about leadsTo takes practice!*) |
|
5232 | 72 |
Goal "[| i<N; j<N |] ==> \ |
5253 | 73 |
\ leadsTo acts (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)"; |
4776 | 74 |
by (case_tac "i=j" 1); |
75 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
76 |
by (rtac (TR7 RS leadsTo_weaken_R) 1); |
|
77 |
by (Clarify_tac 1); |
|
78 |
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
|
79 |
qed "TR7_nodeOrder"; |
|
80 |
||
81 |
||
82 |
(*Chapter 4 variant, the one actually used below.*) |
|
5232 | 83 |
Goal "[| i<N; j<N; i~=j |] \ |
5253 | 84 |
\ ==> leadsTo acts (HasTok i) {s. (token s, i) : nodeOrder j}"; |
4776 | 85 |
by (rtac (TR7 RS leadsTo_weaken_R) 1); |
86 |
by (Clarify_tac 1); |
|
87 |
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
|
88 |
qed "TR7_aux"; |
|
89 |
||
5232 | 90 |
Goal "({s. token s < N} Int token -`` {m}) = \ |
91 |
\ (if m<N then token -`` {m} else {})"; |
|
4776 | 92 |
by Auto_tac; |
5232 | 93 |
val token_lemma = result(); |
4776 | 94 |
|
95 |
||
96 |
(*Misra's TR9: the token reaches an arbitrary node*) |
|
5253 | 97 |
Goal "j<N ==> leadsTo acts {s. token s < N} (HasTok j)"; |
4776 | 98 |
by (rtac leadsTo_weaken_R 1); |
5232 | 99 |
by (res_inst_tac [("I", "Compl{j}"), ("f", "token"), ("B", "{}")] |
4776 | 100 |
(wf_nodeOrder RS bounded_induct) 1); |
5232 | 101 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff, |
4776 | 102 |
HasTok_def]))); |
103 |
by (Blast_tac 2); |
|
104 |
by (Clarify_tac 1); |
|
105 |
by (rtac (TR7_aux RS leadsTo_weaken) 1); |
|
106 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def]))); |
|
107 |
by (ALLGOALS Blast_tac); |
|
108 |
qed "leadsTo_j"; |
|
109 |
||
110 |
(*Misra's TR8: a hungry process eventually eats*) |
|
5253 | 111 |
Goal "j<N ==> leadsTo acts ({s. token s < N} Int H j) (E j)"; |
4776 | 112 |
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); |
113 |
by (rtac TR6 2); |
|
114 |
by (rtac leadsTo_weaken_R 1); |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
115 |
by (rtac ([leadsTo_j, TR3] MRS psp) 1); |
4776 | 116 |
by (ALLGOALS Blast_tac); |
5232 | 117 |
qed "token_progress"; |