author | oheimb |
Fri, 23 Oct 1998 20:35:19 +0200 | |
changeset 5755 | 22081de41254 |
parent 5525 | 896f8234b864 |
child 6255 | db63752140c7 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: TLA/ex/inc/Inc.ML |
|
3 |
Author: Stephan Merz |
|
4 |
Copyright: 1997 University of Munich |
|
5 |
||
6 |
Proofs for the "increment" example from SRC79. |
|
7 |
*) |
|
8 |
||
9 |
val PsiInv_defs = [PsiInv_def,PsiInv1_def,PsiInv2_def,PsiInv3_def]; |
|
10 |
val Psi_defs = [Psi_def,InitPsi_def,N1_def,N2_def,alpha1_def,alpha2_def, |
|
11 |
beta1_def,beta2_def,gamma1_def,gamma2_def]; |
|
12 |
||
4089 | 13 |
val Inc_css = (claset(), simpset()); |
3807 | 14 |
|
15 |
(*** Invariant proof for Psi: "manual" proof proves individual lemmas ***) |
|
16 |
||
17 |
qed_goal "PsiInv_Init" Inc.thy "InitPsi .-> PsiInv" |
|
18 |
(fn _ => [ auto_tac (Inc_css addsimps2 InitPsi_def::PsiInv_defs) ]); |
|
19 |
||
20 |
qed_goal "PsiInv_alpha1" Inc.thy "alpha1 .& PsiInv .-> PsiInv`" |
|
21 |
(fn _ => [ auto_tac (Inc_css addsimps2 alpha1_def::PsiInv_defs) ]); |
|
22 |
||
23 |
qed_goal "PsiInv_alpha2" Inc.thy "alpha2 .& PsiInv .-> PsiInv`" |
|
24 |
(fn _ => [ auto_tac (Inc_css addsimps2 alpha2_def::PsiInv_defs) ]); |
|
25 |
||
26 |
qed_goal "PsiInv_beta1" Inc.thy "beta1 .& PsiInv .-> PsiInv`" |
|
27 |
(fn _ => [ auto_tac (Inc_css addsimps2 beta1_def::PsiInv_defs) ]); |
|
28 |
||
29 |
qed_goal "PsiInv_beta2" Inc.thy "beta2 .& PsiInv .-> PsiInv`" |
|
30 |
(fn _ => [ auto_tac (Inc_css addsimps2 beta2_def::PsiInv_defs) ]); |
|
31 |
||
32 |
qed_goal "PsiInv_gamma1" Inc.thy "gamma1 .& PsiInv .-> PsiInv`" |
|
33 |
(fn _ => [ auto_tac (Inc_css addsimps2 gamma1_def::PsiInv_defs) ]); |
|
34 |
||
35 |
qed_goal "PsiInv_gamma2" Inc.thy "gamma2 .& PsiInv .-> PsiInv`" |
|
36 |
(fn _ => [ auto_tac (Inc_css addsimps2 gamma2_def::PsiInv_defs) ]); |
|
37 |
||
38 |
qed_goal "PsiInv_stutter" Inc.thy "unchanged <x,y,sem,pc1,pc2> .& PsiInv .-> PsiInv`" |
|
39 |
(fn _ => [ auto_tac (Inc_css addsimps2 PsiInv_defs) ]); |
|
40 |
||
5755
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
41 |
qed_goal "PsiInv" Inc.thy "Psi .-> []PsiInv" (K [ |
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
42 |
inv_tac (Inc_css addsimps2 [Psi_def]) 1, |
3807 | 43 |
SELECT_GOAL (auto_tac (Inc_css addSIs2 [action_mp PsiInv_Init] |
44 |
addsimps2 [Init_def])) 1, |
|
5755
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
45 |
force_tac (Inc_css addSEs2 (map action_conjimpE |
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
46 |
[PsiInv_alpha1,PsiInv_alpha2,PsiInv_beta1, |
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
47 |
PsiInv_beta2,PsiInv_gamma1,PsiInv_gamma2]) |
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
48 |
addIs2 [action_mp PsiInv_stutter] |
22081de41254
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5525
diff
changeset
|
49 |
addsimps2 [square_def,N1_def, N2_def]) 1]); |
3807 | 50 |
|
51 |
||
52 |
||
53 |
(* Automatic proof works too, but it make take a while on a slow machine. |
|
54 |
More substantial examples require manual guidance anyway. |
|
55 |
||
5069 | 56 |
Goal "Psi .-> []PsiInv"; |
4089 | 57 |
by (auto_inv_tac (simpset() addsimps PsiInv_defs @ Psi_defs @ pcount.simps) 1); |
3807 | 58 |
|
59 |
*) |
|
60 |
||
61 |
(**** Step simulation ****) |
|
62 |
||
63 |
qed_goal "Init_sim" Inc.thy "Psi .-> Init(InitPhi)" |
|
64 |
(fn _ => [ auto_tac (Inc_css addsimps2 [InitPhi_def,Psi_def,InitPsi_def,Init_def]) ]); |
|
65 |
||
66 |
qed_goal "Step_sim" Inc.thy "Psi .-> [][M1 .| M2]_<x,y>" |
|
67 |
(fn _ => [auto_tac (Inc_css addsimps2 [square_def,M1_def,M2_def] @ Psi_defs |
|
68 |
addSEs2 [STL4E]) |
|
69 |
]); |
|
70 |
||
71 |
(**** Proof of fairness ****) |
|
72 |
||
73 |
(* |
|
74 |
The goal is to prove Fair_M1 far below, which asserts |
|
75 |
Psi .-> WF(M1)_<x,y> |
|
76 |
(the other fairness condition is symmetrical). |
|
77 |
||
78 |
The strategy is to use WF2 (with beta1 as the helpful action). Proving its |
|
79 |
temporal premise needs two auxiliary lemmas: |
|
80 |
1. Stuck_at_b: control can only proceed at pc1 = b by executing beta1 |
|
81 |
2. N1_live: the first component will eventually reach b |
|
82 |
||
83 |
Lemma 1 is easy, lemma 2 relies on the invariant, the strong fairness |
|
84 |
of the semaphore, and needs auxiliary lemmas that ensure that the second |
|
85 |
component will eventually release the semaphore. Most of the proofs of |
|
86 |
the auxiliary lemmas are very similar. |
|
87 |
*) |
|
88 |
||
89 |
qed_goal "Stuck_at_b" Inc.thy |
|
90 |
"[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .-> stable($pc1 .= #b)" |
|
91 |
(fn _ => [rtac StableL 1, |
|
92 |
auto_tac (Inc_css addsimps2 square_def::Psi_defs) |
|
93 |
]); |
|
94 |
||
95 |
qed_goal "N1_enabled_at_g" Inc.thy |
|
96 |
"($pc1 .= #g) .-> $(Enabled (<N1>_<x,y,sem,pc1,pc2>))" |
|
97 |
(fn _ => [Action_simp_tac 1, |
|
98 |
res_inst_tac [("F","gamma1")] enabled_mono 1, |
|
99 |
enabled_tac Inc_base 1, |
|
100 |
auto_tac (Inc_css addsimps2 [angle_def,gamma1_def,N1_def]) |
|
101 |
]); |
|
102 |
||
103 |
qed_goal "g1_leadsto_a1" Inc.thy |
|
104 |
"[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N1)_<x,y,sem,pc1,pc2> .& []#True \ |
|
105 |
\ .-> ($pc1 .= #g ~> $pc1 .= #a)" |
|
106 |
(fn _ => [rtac SF1 1, |
|
107 |
(* the first two subgoals are simple action formulas and succumb to the |
|
108 |
auto_tac; don't expand N1 in the third subgoal *) |
|
109 |
SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1, |
|
110 |
SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1, |
|
111 |
(* reduce []A .-> <>Enabled B to A .-> Enabled B *) |
|
112 |
auto_tac (Inc_css addSIs2 [InitDmdD, action_mp N1_enabled_at_g] |
|
113 |
addSDs2 [STL2bD] |
|
114 |
addsimps2 [Init_def]) |
|
115 |
]); |
|
116 |
||
117 |
(* symmetrical for N2, and similar for beta2 *) |
|
118 |
qed_goal "N2_enabled_at_g" Inc.thy |
|
119 |
"($pc2 .= #g) .-> $(Enabled (<N2>_<x,y,sem,pc1,pc2>))" |
|
120 |
(fn _ => [Action_simp_tac 1, |
|
121 |
res_inst_tac [("F","gamma2")] enabled_mono 1, |
|
122 |
enabled_tac Inc_base 1, |
|
123 |
auto_tac (Inc_css addsimps2 [angle_def,gamma2_def,N2_def]) |
|
124 |
]); |
|
125 |
||
126 |
qed_goal "g2_leadsto_a2" Inc.thy |
|
127 |
"[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N2)_<x,y,sem,pc1,pc2> .& []#True \ |
|
128 |
\ .-> ($pc2 .= #g ~> $pc2 .= #a)" |
|
129 |
(fn _ => [rtac SF1 1, |
|
130 |
SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1, |
|
131 |
SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1, |
|
132 |
auto_tac (Inc_css addSIs2 [InitDmdD, action_mp N2_enabled_at_g] |
|
133 |
addSDs2 [STL2bD] |
|
134 |
addsimps2 [Init_def]) |
|
135 |
]); |
|
136 |
||
137 |
qed_goal "N2_enabled_at_b" Inc.thy |
|
138 |
"($pc2 .= #b) .-> $(Enabled (<N2>_<x,y,sem,pc1,pc2>))" |
|
139 |
(fn _ => [Action_simp_tac 1, |
|
140 |
res_inst_tac [("F","beta2")] enabled_mono 1, |
|
141 |
enabled_tac Inc_base 1, |
|
142 |
auto_tac (Inc_css addsimps2 [angle_def,beta2_def,N2_def]) |
|
143 |
]); |
|
144 |
||
145 |
qed_goal "b2_leadsto_g2" Inc.thy |
|
146 |
"[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N2)_<x,y,sem,pc1,pc2> .& []#True \ |
|
147 |
\ .-> ($pc2 .= #b ~> $pc2 .= #g)" |
|
148 |
(fn _ => [rtac SF1 1, |
|
149 |
SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1, |
|
150 |
SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1, |
|
151 |
auto_tac (Inc_css addSIs2 [InitDmdD, action_mp N2_enabled_at_b] |
|
152 |
addSDs2 [STL2bD] |
|
153 |
addsimps2 [Init_def]) |
|
154 |
]); |
|
155 |
||
156 |
(* Combine above lemmas: the second component will eventually reach pc2 = a *) |
|
157 |
qed_goal "N2_leadsto_a" Inc.thy |
|
158 |
"[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N2)_<x,y,sem,pc1,pc2> .& []#True \ |
|
159 |
\ .-> (($pc2 .= #a .| $pc2 .= #b .| $pc2 .= #g) ~> $pc2 .= #a)" |
|
160 |
(fn _ => [auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]), |
|
161 |
rtac (LatticeReflexivity RS tempD) 1, |
|
162 |
rtac LatticeTransitivity 1, |
|
163 |
auto_tac (Inc_css addSIs2 (map temp_mp [b2_leadsto_g2,g2_leadsto_a2])) |
|
164 |
]); |
|
165 |
||
166 |
(* A variant that gets rid of the disjunction, thanks to induction over data types *) |
|
167 |
qed_goal "N2_live" Inc.thy |
|
168 |
"[][(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2> .& SF(N2)_<x,y,sem,pc1,pc2> \ |
|
169 |
\ .-> <>($pc2 .= #a)" |
|
170 |
(fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N2_leadsto_a) RSN(2,leadsto_init)]), |
|
171 |
rewrite_goals_tac (Init_def::action_rews), |
|
5176 | 172 |
exhaust_tac "pc2 (fst_st sigma)" 1, |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4089
diff
changeset
|
173 |
Auto_tac |
3807 | 174 |
]); |
175 |
||
176 |
(* Now prove that the first component will eventually reach pc1 = b from pc1 = a *) |
|
177 |
||
178 |
qed_goal "N1_enabled_at_both_a" Inc.thy |
|
179 |
"$pc2 .= #a .& (PsiInv .& $pc1 .= #a) .-> $(Enabled (<N1>_<x,y,sem,pc1,pc2>))" |
|
180 |
(fn _ => [Action_simp_tac 1, |
|
181 |
res_inst_tac [("F","alpha1")] enabled_mono 1, |
|
182 |
enabled_tac Inc_base 1, |
|
183 |
auto_tac (Inc_css addIs2 [sym] |
|
184 |
addsimps2 [angle_def,alpha1_def,N1_def] @ PsiInv_defs) |
|
185 |
]); |
|
186 |
||
187 |
qed_goal "a1_leadsto_b1" Inc.thy |
|
188 |
"[](PsiInv .& [(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2>) \ |
|
189 |
\ .& SF(N1)_<x,y,sem,pc1,pc2> .& [] SF(N2)_<x,y,sem,pc1,pc2> \ |
|
190 |
\ .-> ($pc1 .= #a ~> $pc1 .= #b)" |
|
191 |
(fn _ => [rtac SF1 1, |
|
192 |
SELECT_GOAL (auto_tac (Inc_css addsimps2 [square_def] @ Psi_defs)) 1, |
|
193 |
SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def] @ Psi_defs)) 1, |
|
194 |
auto_tac (Inc_css addSIs2 [N1_enabled_at_both_a RS (temp_mp DmdImpl)]), |
|
195 |
auto_tac (Inc_css addSIs2 [temp_mp BoxDmdT2, temp_mp N2_live] |
|
196 |
addsimps2 split_box_conj::more_temp_simps) |
|
197 |
]); |
|
198 |
||
199 |
(* Combine the leadsto properties for N1: it will arrive at pc1 = b *) |
|
200 |
||
201 |
qed_goal "N1_leadsto_b" Inc.thy |
|
202 |
"[](PsiInv .& [(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2>) \ |
|
203 |
\ .& SF(N1)_<x,y,sem,pc1,pc2> .& [] SF(N2)_<x,y,sem,pc1,pc2> \ |
|
204 |
\ .-> (($pc1 .= #b .| $pc1 .= #g .| $pc1 .= #a) ~> $pc1 .= #b)" |
|
205 |
(fn _ => [auto_tac (Inc_css addSIs2 [LatticeDisjunctionIntro]), |
|
206 |
rtac (LatticeReflexivity RS tempD) 1, |
|
207 |
rtac LatticeTransitivity 1, |
|
208 |
auto_tac (Inc_css addSIs2 (map temp_mp [a1_leadsto_b1,g1_leadsto_a1]) |
|
209 |
addsimps2 [split_box_conj]) |
|
210 |
]); |
|
211 |
||
212 |
qed_goal "N1_live" Inc.thy |
|
213 |
"[](PsiInv .& [(N1 .| N2) .& .~ beta1]_<x,y,sem,pc1,pc2>) \ |
|
214 |
\ .& SF(N1)_<x,y,sem,pc1,pc2> .& [] SF(N2)_<x,y,sem,pc1,pc2> \ |
|
215 |
\ .-> <>($pc1 .= #b)" |
|
216 |
(fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N1_leadsto_b) RSN(2,leadsto_init)]), |
|
217 |
rewrite_goals_tac (Init_def::action_rews), |
|
5176 | 218 |
exhaust_tac "pc1 (fst_st sigma)" 1, |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4089
diff
changeset
|
219 |
Auto_tac |
3807 | 220 |
]); |
221 |
||
222 |
qed_goal "N1_enabled_at_b" Inc.thy |
|
223 |
"($pc1 .= #b) .-> $(Enabled (<N1>_<x,y,sem,pc1,pc2>))" |
|
224 |
(fn _ => [Action_simp_tac 1, |
|
225 |
res_inst_tac [("F","beta1")] enabled_mono 1, |
|
226 |
enabled_tac Inc_base 1, |
|
227 |
auto_tac (Inc_css addsimps2 [angle_def,beta1_def,N1_def]) |
|
228 |
]); |
|
229 |
||
230 |
(* Now assemble the bits and pieces to prove that Psi is fair. *) |
|
231 |
||
5525 | 232 |
goal Inc.thy "[](PsiInv .& [(N1 .| N2)]_<x,y,sem,pc1,pc2>) \ |
3807 | 233 |
\ .& SF(N1)_<x,y,sem,pc1,pc2> .& [] SF(N2)_<x,y,sem,pc1,pc2> \ |
5525 | 234 |
\ .-> SF(M1)_<x,y>"; |
235 |
by (res_inst_tac [("B","beta1"),("P","$pc1 .= #b")] SF2 1); |
|
236 |
||
237 |
(* the action premises are simple *) |
|
238 |
by (force_tac (Inc_css addsimps2 [angle_def,M1_def,beta1_def]) 1); |
|
239 |
by (force_tac (Inc_css addsimps2 angle_def::Psi_defs) 1); |
|
240 |
by (force_tac (Inc_css addSEs2 [action_mp N1_enabled_at_b]) 1); |
|
241 |
(* temporal premise: use previous lemmas and simple TL *) |
|
242 |
by (force_tac (Inc_css addSIs2 DmdStable::(map temp_mp [N1_live,Stuck_at_b]) |
|
243 |
addEs2 [STL4E] addsimps2 [square_def]) 1); |
|
244 |
qed "Fair_M1_lemma"; |
|
3807 | 245 |
|
246 |
qed_goal "Fair_M1" Inc.thy "Psi .-> WF(M1)_<x,y>" |
|
247 |
(fn _ => [auto_tac (Inc_css addSIs2 SFImplWF::(map temp_mp [Fair_M1_lemma, PsiInv]) |
|
248 |
addsimps2 [split_box_conj]), |
|
249 |
auto_tac (Inc_css addsimps2 Psi_def::more_temp_simps) |
|
250 |
]); |
|
251 |