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