author | wenzelm |
Tue, 17 Nov 1998 14:07:25 +0100 | |
changeset 5906 | 1f58694fc3e2 |
parent 5782 | 7559f116cb10 |
child 6055 | fdf4638bf726 |
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 |
||
5782
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
25 |
val TR2 = thm "TR2"; |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
26 |
val TR3 = thm "TR3"; |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
27 |
val TR4 = thm "TR4"; |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
28 |
val TR5 = thm "TR5"; |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
29 |
val TR6 = thm "TR6"; |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
30 |
val TR7 = thm "TR7"; |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
31 |
val nodeOrder_def = thm "nodeOrder_def"; |
7559f116cb10
locales now implicitly quantify over free variables
paulson
parents:
5648
diff
changeset
|
32 |
val next_def = thm "next_def"; |
5420 | 33 |
|
5648 | 34 |
AddIffs [thm "N_positive"]; |
5420 | 35 |
|
5648 | 36 |
Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))"; |
4776 | 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 |
||
5069 | 46 |
Goalw [nodeOrder_def] "wf(nodeOrder j)"; |
4776 | 47 |
by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1); |
48 |
by (Blast_tac 1); |
|
49 |
qed"wf_nodeOrder"; |
|
50 |
||
5069 | 51 |
Goalw [nodeOrder_def, next_def, inv_image_def] |
5111 | 52 |
"[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"; |
4776 | 53 |
by (auto_tac (claset(), |
54 |
simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq])); |
|
55 |
by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1); |
|
5596 | 56 |
by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, less_imp_le, |
4776 | 57 |
diff_add_assoc]) 2); |
5625 | 58 |
by (full_simp_tac (simpset() addsimps [linorder_neq_iff]) 1); |
4776 | 59 |
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1); |
5420 | 60 |
by (auto_tac (claset(), |
5625 | 61 |
simpset() addsimps [diff_add_assoc2, linorder_neq_iff, |
5420 | 62 |
Suc_le_eq, Suc_diff_Suc, less_imp_diff_less, |
63 |
add_diff_less, mod_less, mod_geq])); |
|
4776 | 64 |
by (etac subst 1); |
65 |
by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1); |
|
66 |
qed "nodeOrder_eq"; |
|
67 |
||
68 |
||
69 |
(*From "A Logic for Concurrent Programming", but not used in Chapter 4. |
|
70 |
Note the use of case_tac. Reasoning about leadsTo takes practice!*) |
|
5232 | 71 |
Goal "[| i<N; j<N |] ==> \ |
5648 | 72 |
\ F : leadsTo (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)"; |
4776 | 73 |
by (case_tac "i=j" 1); |
74 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
75 |
by (rtac (TR7 RS leadsTo_weaken_R) 1); |
|
76 |
by (Clarify_tac 1); |
|
77 |
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
|
78 |
qed "TR7_nodeOrder"; |
|
79 |
||
80 |
||
81 |
(*Chapter 4 variant, the one actually used below.*) |
|
5232 | 82 |
Goal "[| i<N; j<N; i~=j |] \ |
5648 | 83 |
\ ==> F : leadsTo (HasTok i) {s. (token s, i) : nodeOrder j}"; |
4776 | 84 |
by (rtac (TR7 RS leadsTo_weaken_R) 1); |
85 |
by (Clarify_tac 1); |
|
86 |
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); |
|
87 |
qed "TR7_aux"; |
|
88 |
||
5232 | 89 |
Goal "({s. token s < N} Int token -`` {m}) = \ |
90 |
\ (if m<N then token -`` {m} else {})"; |
|
4776 | 91 |
by Auto_tac; |
5232 | 92 |
val token_lemma = result(); |
4776 | 93 |
|
94 |
||
95 |
(*Misra's TR9: the token reaches an arbitrary node*) |
|
5648 | 96 |
Goal "j<N ==> F : leadsTo {s. token s < N} (HasTok j)"; |
4776 | 97 |
by (rtac leadsTo_weaken_R 1); |
5490 | 98 |
by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")] |
4776 | 99 |
(wf_nodeOrder RS bounded_induct) 1); |
5232 | 100 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff, |
4776 | 101 |
HasTok_def]))); |
102 |
by (Blast_tac 2); |
|
103 |
by (Clarify_tac 1); |
|
104 |
by (rtac (TR7_aux RS leadsTo_weaken) 1); |
|
105 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def]))); |
|
106 |
by (ALLGOALS Blast_tac); |
|
107 |
qed "leadsTo_j"; |
|
108 |
||
109 |
(*Misra's TR8: a hungry process eventually eats*) |
|
5648 | 110 |
Goal "j<N ==> F : leadsTo ({s. token s < N} Int H j) (E j)"; |
4776 | 111 |
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); |
112 |
by (rtac TR6 2); |
|
113 |
by (rtac leadsTo_weaken_R 1); |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
114 |
by (rtac ([leadsTo_j, TR3] MRS psp) 1); |
4776 | 115 |
by (ALLGOALS Blast_tac); |
5232 | 116 |
qed "token_progress"; |