author | paulson |
Wed, 07 Oct 1998 10:32:00 +0200 | |
changeset 5620 | 3ac11c4af76a |
parent 5596 | b29d18d8c4d2 |
child 5648 | fe887910e32e |
permissions | -rw-r--r-- |
5111 | 1 |
(* Title: HOL/UNITY/Mutex |
4776 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra |
|
7 |
*) |
|
8 |
||
5232 | 9 |
(*split_all_tac causes a big blow-up*) |
10 |
claset_ref() := claset() delSWrapper "split_all_tac"; |
|
4776 | 11 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
12 |
Addsimps [Mprg_def RS def_prg_simps]; |
4776 | 13 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
14 |
Addsimps (map simp_of_act |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
15 |
[cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
16 |
cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def]); |
4776 | 17 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
18 |
Addsimps (map simp_of_set |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
19 |
[invariantU_def, invariantV_def, bad_invariantU_def]); |
4776 | 20 |
|
5232 | 21 |
(*Simplification for records*) |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
22 |
Addsimps (thms"state.update_defs"); |
5232 | 23 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
24 |
Goal "Invariant Mprg invariantU"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
25 |
by (rtac InvariantI 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
26 |
by (constrains_tac 2); |
5232 | 27 |
by Auto_tac; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
28 |
qed "invariantU"; |
4776 | 29 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
30 |
Goal "Invariant Mprg invariantV"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
31 |
by (rtac InvariantI 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
32 |
by (constrains_tac 2); |
4776 | 33 |
by Auto_tac; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
34 |
qed "invariantV"; |
4776 | 35 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
36 |
val invariantUV = Invariant_Int_rule [invariantU, invariantV]; |
4776 | 37 |
|
38 |
||
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
39 |
(*The safety property: mutual exclusion*) |
5596 | 40 |
Goal "(reachable Mprg) Int {s. MM s = #3 & NN s = #3} = {}"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
41 |
by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1); |
4776 | 42 |
by Auto_tac; |
43 |
qed "mutual_exclusion"; |
|
44 |
||
45 |
||
5232 | 46 |
(*The bad invariant FAILS in cmd1V*) |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
47 |
Goal "Invariant Mprg bad_invariantU"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
48 |
by (rtac InvariantI 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
49 |
by (constrains_tac 2); |
5596 | 50 |
by (Force_tac 1); |
51 |
(*Needs a decision procedure to simplify the resulting state*) |
|
52 |
by (auto_tac (claset(), |
|
53 |
simpset_of Int.thy addsimps |
|
54 |
[zadd_int, integ_of_Pls, integ_of_Min, |
|
55 |
integ_of_BIT, le_int_Suc_eq])); |
|
56 |
by (dtac zle_trans 1 THEN assume_tac 1); |
|
57 |
by (full_simp_tac (simpset_of Int.thy) 1); |
|
58 |
by (asm_full_simp_tac (simpset() addsimps int_simps) 1); |
|
4776 | 59 |
(*Resulting state: n=1, p=false, m=4, u=false. |
5232 | 60 |
Execution of cmd1V (the command of process v guarded by n=1) sets p:=true, |
4776 | 61 |
violating the invariant!*) |
62 |
(*Check that subgoals remain: proof failed.*) |
|
63 |
getgoal 1; |
|
64 |
||
65 |
||
5596 | 66 |
Goal "(#1 <= m & m <= #3) = (m = #1 | m = #2 | m = #3)"; |
67 |
by (auto_tac (claset(), |
|
68 |
simpset_of Int.thy addsimps |
|
69 |
[zle_iff_zadd, zadd_int, integ_of_Pls, integ_of_Min, |
|
70 |
integ_of_BIT])); |
|
71 |
by (exhaust_tac "na" 1); |
|
72 |
by (exhaust_tac "nat" 2); |
|
73 |
by (exhaust_tac "n" 3); |
|
5620 | 74 |
by Auto_tac; |
5596 | 75 |
qed "eq_123"; |
76 |
||
77 |
||
4776 | 78 |
(*** Progress for U ***) |
79 |
||
5596 | 80 |
Goalw [Unless_def] "Unless Mprg {s. MM s=#2} {s. MM s=#3}"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
81 |
by (constrains_tac 1); |
4776 | 82 |
qed "U_F0"; |
83 |
||
5596 | 84 |
Goal "LeadsTo Mprg {s. MM s=#1} {s. PP s = VV s & MM s = #2}"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
85 |
by (ensures_tac "cmd1U" 1); |
4776 | 86 |
qed "U_F1"; |
87 |
||
5596 | 88 |
Goal "LeadsTo Mprg {s. ~ PP s & MM s = #2} {s. MM s = #3}"; |
5340 | 89 |
by (cut_facts_tac [invariantU] 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
90 |
by (ensures_tac "cmd2U" 1); |
4776 | 91 |
qed "U_F2"; |
92 |
||
5596 | 93 |
Goal "LeadsTo Mprg {s. MM s = #3} {s. PP s}"; |
94 |
by (res_inst_tac [("B", "{s. MM s = #4}")] LeadsTo_Trans 1); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
95 |
by (ensures_tac "cmd4U" 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
96 |
by (ensures_tac "cmd3U" 1); |
4776 | 97 |
qed "U_F3"; |
98 |
||
5596 | 99 |
Goal "LeadsTo Mprg {s. MM s = #2} {s. PP s}"; |
5340 | 100 |
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
4776 | 101 |
MRS LeadsTo_Diff) 1); |
102 |
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1); |
|
103 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
104 |
val U_lemma2 = result(); |
4776 | 105 |
|
5596 | 106 |
Goal "LeadsTo Mprg {s. MM s = #1} {s. PP s}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
107 |
by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1); |
4776 | 108 |
by (Blast_tac 1); |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
109 |
val U_lemma1 = result(); |
4776 | 110 |
|
5596 | 111 |
Goal "LeadsTo Mprg {s. #1 <= MM s & MM s <= #3} {s. PP s}"; |
112 |
by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
113 |
U_lemma1, U_lemma2, U_F3] ) 1); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
114 |
val U_lemma123 = result(); |
4776 | 115 |
|
116 |
(*Misra's F4*) |
|
5253 | 117 |
Goal "LeadsTo Mprg {s. UU s} {s. PP s}"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
118 |
by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1); |
4776 | 119 |
by Auto_tac; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
120 |
qed "u_Leadsto_p"; |
4776 | 121 |
|
122 |
||
123 |
(*** Progress for V ***) |
|
124 |
||
125 |
||
5596 | 126 |
Goalw [Unless_def] "Unless Mprg {s. NN s=#2} {s. NN s=#3}"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
127 |
by (constrains_tac 1); |
4776 | 128 |
qed "V_F0"; |
129 |
||
5596 | 130 |
Goal "LeadsTo Mprg {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
131 |
by (ensures_tac "cmd1V" 1); |
4776 | 132 |
qed "V_F1"; |
133 |
||
5596 | 134 |
Goal "LeadsTo Mprg {s. PP s & NN s = #2} {s. NN s = #3}"; |
5340 | 135 |
by (cut_facts_tac [invariantV] 1); |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
136 |
by (ensures_tac "cmd2V" 1); |
4776 | 137 |
qed "V_F2"; |
138 |
||
5596 | 139 |
Goal "LeadsTo Mprg {s. NN s = #3} {s. ~ PP s}"; |
140 |
by (res_inst_tac [("B", "{s. NN s = #4}")] LeadsTo_Trans 1); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
141 |
by (ensures_tac "cmd4V" 2); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
142 |
by (ensures_tac "cmd3V" 1); |
4776 | 143 |
qed "V_F3"; |
144 |
||
5596 | 145 |
Goal "LeadsTo Mprg {s. NN s = #2} {s. ~ PP s}"; |
5340 | 146 |
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
4776 | 147 |
MRS LeadsTo_Diff) 1); |
148 |
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1); |
|
149 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
150 |
val V_lemma2 = result(); |
4776 | 151 |
|
5596 | 152 |
Goal "LeadsTo Mprg {s. NN s = #1} {s. ~ PP s}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
153 |
by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1); |
4776 | 154 |
by (Blast_tac 1); |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
155 |
val V_lemma1 = result(); |
4776 | 156 |
|
5596 | 157 |
Goal "LeadsTo Mprg {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}"; |
158 |
by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
159 |
V_lemma1, V_lemma2, V_F3] ) 1); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
160 |
val V_lemma123 = result(); |
4776 | 161 |
|
162 |
||
163 |
(*Misra's F4*) |
|
5253 | 164 |
Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
165 |
by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1); |
4776 | 166 |
by Auto_tac; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
167 |
qed "v_Leadsto_not_p"; |
4776 | 168 |
|
169 |
||
170 |
(** Absence of starvation **) |
|
171 |
||
172 |
(*Misra's F6*) |
|
5596 | 173 |
Goal "LeadsTo Mprg {s. MM s = #1} {s. MM s = #3}"; |
4776 | 174 |
by (rtac LeadsTo_Un_duplicate 1); |
175 |
by (rtac LeadsTo_cancel2 1); |
|
176 |
by (rtac U_F2 2); |
|
177 |
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); |
|
178 |
by (stac Un_commute 1); |
|
179 |
by (rtac LeadsTo_Un_duplicate 1); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
180 |
by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1); |
4776 | 181 |
by (rtac (U_F1 RS LeadsTo_weaken_R) 1); |
182 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
183 |
qed "m1_Leadsto_3"; |
4776 | 184 |
|
185 |
||
186 |
(*The same for V*) |
|
5596 | 187 |
Goal "LeadsTo Mprg {s. NN s = #1} {s. NN s = #3}"; |
4776 | 188 |
by (rtac LeadsTo_Un_duplicate 1); |
189 |
by (rtac LeadsTo_cancel2 1); |
|
190 |
by (rtac V_F2 2); |
|
191 |
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); |
|
192 |
by (stac Un_commute 1); |
|
193 |
by (rtac LeadsTo_Un_duplicate 1); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
194 |
by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1); |
4776 | 195 |
by (rtac (V_F1 RS LeadsTo_weaken_R) 1); |
196 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
197 |
qed "n1_Leadsto_3"; |