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