author | paulson |
Fri, 12 May 2000 15:18:55 +0200 | |
changeset 8868 | 851693e780d6 |
parent 8707 | 5de763446504 |
child 10834 | a7897aebbffc |
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); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
19 |
by (case_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)"; |
8707 | 53 |
by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq])); |
5420 | 54 |
by (auto_tac (claset(), |
8868 | 55 |
simpset() addsplits [nat_diff_split] |
8707 | 56 |
addsimps [linorder_neq_iff, mod_geq])); |
4776 | 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!*) |
|
5232 | 61 |
Goal "[| i<N; j<N |] ==> \ |
6536 | 62 |
\ F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)"; |
4776 | 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); |
|
7403 | 66 |
by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq])); |
4776 | 67 |
qed "TR7_nodeOrder"; |
68 |
||
69 |
||
70 |
(*Chapter 4 variant, the one actually used below.*) |
|
5232 | 71 |
Goal "[| i<N; j<N; i~=j |] \ |
6536 | 72 |
\ ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}"; |
4776 | 73 |
by (rtac (TR7 RS leadsTo_weaken_R) 1); |
7403 | 74 |
by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq])); |
4776 | 75 |
qed "TR7_aux"; |
76 |
||
5232 | 77 |
Goal "({s. token s < N} Int token -`` {m}) = \ |
78 |
\ (if m<N then token -`` {m} else {})"; |
|
4776 | 79 |
by Auto_tac; |
5232 | 80 |
val token_lemma = result(); |
4776 | 81 |
|
82 |
||
83 |
(*Misra's TR9: the token reaches an arbitrary node*) |
|
6536 | 84 |
Goal "j<N ==> F : {s. token s < N} leadsTo (HasTok j)"; |
4776 | 85 |
by (rtac leadsTo_weaken_R 1); |
5490 | 86 |
by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")] |
4776 | 87 |
(wf_nodeOrder RS bounded_induct) 1); |
5232 | 88 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff, |
4776 | 89 |
HasTok_def]))); |
90 |
by (Blast_tac 2); |
|
91 |
by (Clarify_tac 1); |
|
92 |
by (rtac (TR7_aux RS leadsTo_weaken) 1); |
|
7403 | 93 |
by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def])); |
4776 | 94 |
qed "leadsTo_j"; |
95 |
||
96 |
(*Misra's TR8: a hungry process eventually eats*) |
|
6536 | 97 |
Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)"; |
4776 | 98 |
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); |
99 |
by (rtac TR6 2); |
|
7403 | 100 |
by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1); |
4776 | 101 |
by (ALLGOALS Blast_tac); |
5232 | 102 |
qed "token_progress"; |