author  paulson 
Fri, 16 Jun 2000 13:41:44 +0200  
changeset 9084  090d450af656 
parent 8948  b797cfa3548d 
child 10064  1a77667b21ef 
permissions  rwrr 
4776  1 
(* Title: HOL/UNITY/WFair 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6 
Weak Fairness versions of transient, ensures, leadsTo. 

7 

8 
From Misra, "A Logic for Concurrent Programming", 1994 

9 
*) 

10 

11 

5648  12 
overload_1st_set "WFair.transient"; 
13 
overload_1st_set "WFair.ensures"; 

6536  14 
overload_1st_set "WFair.op leadsTo"; 
5340  15 

4776  16 
(*** transient ***) 
17 

5069  18 
Goalw [stable_def, constrains_def, transient_def] 
5648  19 
"[ F : stable A; F : transient A ] ==> A = {}"; 
4776  20 
by (Blast_tac 1); 
21 
qed "stable_transient_empty"; 

22 

5069  23 
Goalw [transient_def] 
5648  24 
"[ F : transient A; B<=A ] ==> F : transient B"; 
4776  25 
by (Clarify_tac 1); 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5971
diff
changeset

26 
by (blast_tac (claset() addSIs [rev_bexI]) 1); 
4776  27 
qed "transient_strengthen"; 
28 

5069  29 
Goalw [transient_def] 
5648  30 
"[ act: Acts F; A <= Domain act; act^^A <= A ] ==> F : transient A"; 
4776  31 
by (Blast_tac 1); 
8041  32 
qed "transientI"; 
33 

34 
val major::prems = 

35 
Goalw [transient_def] 

36 
"[ F : transient A; \ 

37 
\ !!act. [ act: Acts F; A <= Domain act; act^^A <= A ] ==> P ] \ 

38 
\ ==> P"; 

39 
by (rtac (major RS CollectD RS bexE) 1); 

40 
by (blast_tac (claset() addIs prems) 1); 

41 
qed "transientE"; 

4776  42 

7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset

43 
Goalw [transient_def] "transient UNIV = {}"; 
9084  44 
by (Blast_tac 1); 
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset

45 
qed "transient_UNIV"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset

46 

c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset

47 
Goalw [transient_def] "transient {} = UNIV"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset

48 
by Auto_tac; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset

49 
qed "transient_empty"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset

50 
Addsimps [transient_UNIV, transient_empty]; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset

51 

4776  52 

53 
(*** ensures ***) 

54 

5069  55 
Goalw [ensures_def] 
7524  56 
"[ F : (AB) co (A Un B); F : transient (AB) ] ==> F : A ensures B"; 
4776  57 
by (Blast_tac 1); 
58 
qed "ensuresI"; 

59 

5069  60 
Goalw [ensures_def] 
6536  61 
"F : A ensures B ==> F : (AB) co (A Un B) & F : transient (AB)"; 
4776  62 
by (Blast_tac 1); 
63 
qed "ensuresD"; 

64 

5069  65 
Goalw [ensures_def] 
6536  66 
"[ F : A ensures A'; A'<=B' ] ==> F : A ensures B'"; 
4776  67 
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); 
68 
qed "ensures_weaken_R"; 

69 

8041  70 
(*The Lversion (precondition strengthening) fails, but we have this*) 
5069  71 
Goalw [ensures_def] 
8041  72 
"[ F : stable C; F : A ensures B ] \ 
73 
\ ==> F : (C Int A) ensures (C Int B)"; 

74 
by (auto_tac (claset(), 

75 
simpset() addsimps [ensures_def, 

76 
Int_Un_distrib RS sym, 

77 
Diff_Int_distrib RS sym])); 

78 
by (blast_tac (claset() addIs [transient_strengthen]) 2); 

79 
by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1); 

4776  80 
qed "stable_ensures_Int"; 
81 

6536  82 
Goal "[ F : stable A; F : transient C; A <= B Un C ] ==> F : A ensures B"; 
5640  83 
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); 
84 
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); 

85 
qed "stable_transient_ensures"; 

86 

8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8112
diff
changeset

87 
Goal "(A ensures B) = (A unless B) Int transient (AB)"; 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8112
diff
changeset

88 
by (simp_tac (simpset() addsimps [ensures_def, unless_def]) 1); 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8112
diff
changeset

89 
qed "ensures_eq"; 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8112
diff
changeset

90 

4776  91 

92 
(*** leadsTo ***) 

93 

6536  94 
Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B"; 
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset

95 
by (blast_tac (claset() addIs [leads.Basis]) 1); 
5648  96 
qed "leadsTo_Basis"; 
4776  97 

8835  98 
AddIs [leadsTo_Basis]; 
99 

5648  100 
Goalw [leadsTo_def] 
6536  101 
"[ F : A leadsTo B; F : B leadsTo C ] ==> F : A leadsTo C"; 
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset

102 
by (blast_tac (claset() addIs [leads.Trans]) 1); 
5648  103 
qed "leadsTo_Trans"; 
104 

6536  105 
Goal "F : transient A ==> F : A leadsTo (A)"; 
5640  106 
by (asm_simp_tac 
107 
(simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1); 

108 
qed "transient_imp_leadsTo"; 

109 

4776  110 
(*Useful with cancellation, disjunction*) 
6536  111 
Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; 
4776  112 
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); 
113 
qed "leadsTo_Un_duplicate"; 

114 

6536  115 
Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"; 
4776  116 
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); 
117 
qed "leadsTo_Un_duplicate2"; 

118 

119 
(*The Union introduction rule as we should have liked to state it*) 

5648  120 
val prems = Goalw [leadsTo_def] 
6536  121 
"(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"; 
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset

122 
by (blast_tac (claset() addIs [leads.Union] addDs prems) 1); 
4776  123 
qed "leadsTo_Union"; 
124 

6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

125 
val prems = Goalw [leadsTo_def] 
7524  126 
"(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B"; 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

127 
by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1); 
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset

128 
by (blast_tac (claset() addIs [leads.Union] addDs prems) 1); 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

129 
qed "leadsTo_Union_Int"; 
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

130 

5648  131 
val prems = Goal 
6536  132 
"(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"; 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

133 
by (stac (Union_image_eq RS sym) 1); 
5648  134 
by (blast_tac (claset() addIs leadsTo_Union::prems) 1); 
4776  135 
qed "leadsTo_UN"; 
136 

137 
(*Binary union introduction rule*) 

6536  138 
Goal "[ F : A leadsTo C; F : B leadsTo C ] ==> F : (A Un B) leadsTo C"; 
4776  139 
by (stac Un_eq_Union 1); 
140 
by (blast_tac (claset() addIs [leadsTo_Union]) 1); 

141 
qed "leadsTo_Un"; 

142 

6714  143 
val prems = 
144 
Goal "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B"; 

145 
by (stac (UN_singleton RS sym) 1 THEN rtac leadsTo_UN 1); 

146 
by (blast_tac (claset() addIs prems) 1); 

147 
qed "single_leadsTo_I"; 

148 

4776  149 

150 
(*The INDUCTION rule as we should have liked to state it*) 

5648  151 
val major::prems = Goalw [leadsTo_def] 
6536  152 
"[ F : za leadsTo zb; \ 
153 
\ !!A B. F : A ensures B ==> P A B; \ 

154 
\ !!A B C. [ F : A leadsTo B; P A B; F : B leadsTo C; P B C ] \ 

4776  155 
\ ==> P A C; \ 
6536  156 
\ !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \ 
4776  157 
\ ] ==> P za zb"; 
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset

158 
by (rtac (major RS CollectD RS leads.induct) 1); 
4776  159 
by (REPEAT (blast_tac (claset() addIs prems) 1)); 
160 
qed "leadsTo_induct"; 

161 

162 

7594
8a188ef6545e
working version with coguaranteesleadsto results
paulson
parents:
7524
diff
changeset

163 
Goal "A<=B ==> F : A ensures B"; 
4776  164 
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); 
165 
by (Blast_tac 1); 

7594
8a188ef6545e
working version with coguaranteesleadsto results
paulson
parents:
7524
diff
changeset

166 
qed "subset_imp_ensures"; 
8a188ef6545e
working version with coguaranteesleadsto results
paulson
parents:
7524
diff
changeset

167 

8a188ef6545e
working version with coguaranteesleadsto results
paulson
parents:
7524
diff
changeset

168 
bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); 
4776  169 

8112
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

170 
bind_thm ("leadsTo_refl", subset_refl RS subset_imp_leadsTo); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

171 

4776  172 
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); 
173 
Addsimps [empty_leadsTo]; 

174 

8041  175 
bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo); 
176 
Addsimps [leadsTo_UNIV]; 

177 

4776  178 

8112
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

179 

efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

180 
(** Variant induction rule: on the preconditions for B **) 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

181 

efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

182 
(*Lemma is the weak version: can't see how to do it in one step*) 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

183 
val major::prems = Goal 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

184 
"[ F : za leadsTo zb; \ 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

185 
\ P zb; \ 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

186 
\ !!A B. [ F : A ensures B; P B ] ==> P A; \ 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

187 
\ !!S. ALL A:S. P A ==> P (Union S) \ 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

188 
\ ] ==> P za"; 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

189 
(*by induction on this formula*) 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

190 
by (subgoal_tac "P zb > P za" 1); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

191 
(*now solve first subgoal: this formula is sufficient*) 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

192 
by (blast_tac (claset() addIs leadsTo_refl::prems) 1); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

193 
by (rtac (major RS leadsTo_induct) 1); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

194 
by (REPEAT (blast_tac (claset() addIs prems) 1)); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

195 
val lemma = result(); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

196 

efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

197 
val major::prems = Goal 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

198 
"[ F : za leadsTo zb; \ 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

199 
\ P zb; \ 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

200 
\ !!A B. [ F : A ensures B; F : B leadsTo zb; P B ] ==> P A; \ 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

201 
\ !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S) \ 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

202 
\ ] ==> P za"; 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

203 
by (subgoal_tac "F : za leadsTo zb & P za" 1); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

204 
by (etac conjunct2 1); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

205 
by (rtac (major RS lemma) 1); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

206 
by (blast_tac (claset() addIs [leadsTo_Union]@prems) 3); 
8835  207 
by (blast_tac (claset() addIs [leadsTo_Trans]@prems) 2); 
8112
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

208 
by (blast_tac (claset() addIs [leadsTo_refl]@prems) 1); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

209 
qed "leadsTo_induct_pre"; 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

210 

efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

211 

6536  212 
Goal "[ F : A leadsTo A'; A'<=B' ] ==> F : A leadsTo B'"; 
5648  213 
by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1); 
214 
qed "leadsTo_weaken_R"; 

4776  215 

6536  216 
Goal "[ F : A leadsTo A'; B<=A ] ==> F : B leadsTo A'"; 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

217 
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); 
4776  218 
qed_spec_mp "leadsTo_weaken_L"; 
219 

220 
(*Distributes over binary unions*) 

6536  221 
Goal "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)"; 
4776  222 
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); 
223 
qed "leadsTo_Un_distrib"; 

224 

6536  225 
Goal "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)"; 
4776  226 
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1); 
227 
qed "leadsTo_UN_distrib"; 

228 

6536  229 
Goal "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)"; 
4776  230 
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1); 
231 
qed "leadsTo_Union_distrib"; 

232 

233 

6536  234 
Goal "[ F : A leadsTo A'; B<=A; A'<=B' ] ==> F : B leadsTo B'"; 
5340  235 
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, 
236 
leadsTo_Trans]) 1); 

4776  237 
qed "leadsTo_weaken"; 
238 

239 

240 
(*Set difference: maybe combine with leadsTo_weaken_L??*) 

6536  241 
Goal "[ F : (AB) leadsTo C; F : B leadsTo C ] ==> F : A leadsTo C"; 
4776  242 
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1); 
243 
qed "leadsTo_Diff"; 

244 

245 
val prems = goal thy 

6536  246 
"(!! i. i:I ==> F : (A i) leadsTo (A' i)) \ 
247 
\ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"; 

6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

248 
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); 
4776  249 
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] 
250 
addIs prems) 1); 

251 
qed "leadsTo_UN_UN"; 

252 

253 
(*Binary union version*) 

6714  254 
Goal "[ F : A leadsTo A'; F : B leadsTo B' ] \ 
255 
\ ==> F : (A Un B) leadsTo (A' Un B')"; 

4776  256 
by (blast_tac (claset() addIs [leadsTo_Un, 
257 
leadsTo_weaken_R]) 1); 

258 
qed "leadsTo_Un_Un"; 

259 

260 

261 
(** The cancellation law **) 

262 

6536  263 
Goal "[ F : A leadsTo (A' Un B); F : B leadsTo B' ] \ 
6714  264 
\ ==> F : A leadsTo (A' Un B')"; 
4776  265 
by (blast_tac (claset() addIs [leadsTo_Un_Un, 
266 
subset_imp_leadsTo, leadsTo_Trans]) 1); 

267 
qed "leadsTo_cancel2"; 

268 

6536  269 
Goal "[ F : A leadsTo (A' Un B); F : (BA') leadsTo B' ] \ 
6714  270 
\ ==> F : A leadsTo (A' Un B')"; 
4776  271 
by (rtac leadsTo_cancel2 1); 
272 
by (assume_tac 2); 

273 
by (ALLGOALS Asm_simp_tac); 

274 
qed "leadsTo_cancel_Diff2"; 

275 

6536  276 
Goal "[ F : A leadsTo (B Un A'); F : B leadsTo B' ] \ 
277 
\ ==> F : A leadsTo (B' Un A')"; 

4776  278 
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); 
279 
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); 

280 
qed "leadsTo_cancel1"; 

281 

6536  282 
Goal "[ F : A leadsTo (B Un A'); F : (BA') leadsTo B' ] \ 
283 
\ ==> F : A leadsTo (B' Un A')"; 

4776  284 
by (rtac leadsTo_cancel1 1); 
285 
by (assume_tac 2); 

286 
by (ALLGOALS Asm_simp_tac); 

287 
qed "leadsTo_cancel_Diff1"; 

288 

289 

290 

291 
(** The impossibility law **) 

292 

8112
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

293 
Goal "F : A leadsTo {} ==> A={}"; 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

294 
by (etac leadsTo_induct_pre 1); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

295 
by (ALLGOALS 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

296 
(asm_full_simp_tac 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

297 
(simpset() addsimps [ensures_def, constrains_def, transient_def]))); 
4776  298 
by (Blast_tac 1); 
299 
qed "leadsTo_empty"; 

300 

301 

302 
(** PSP: ProgressSafetyProgress **) 

303 

5640  304 
(*Special case of PSP: Misra's "stable conjunction"*) 
5069  305 
Goalw [stable_def] 
6536  306 
"[ F : A leadsTo A'; F : stable B ] \ 
307 
\ ==> F : (A Int B) leadsTo (A' Int B)"; 

4776  308 
by (etac leadsTo_induct 1); 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

309 
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); 
4776  310 
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); 
311 
by (rtac leadsTo_Basis 1); 

312 
by (asm_full_simp_tac 

313 
(simpset() addsimps [ensures_def, 

314 
Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1); 

315 
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1); 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

316 
qed "psp_stable"; 
4776  317 

7524  318 
Goal 
319 
"[ F : A leadsTo A'; F : stable B ] ==> F : (B Int A) leadsTo (B Int A')"; 

5536  320 
by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

321 
qed "psp_stable2"; 
4776  322 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

323 
Goalw [ensures_def, constrains_def] 
6536  324 
"[ F : A ensures A'; F : B co B' ] \ 
6714  325 
\ ==> F : (A Int B') ensures ((A' Int B) Un (B'  B))"; 
326 
by (Clarify_tac 1); (*speeds up the proof*) 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

327 
by (blast_tac (claset() addIs [transient_strengthen]) 1); 
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

328 
qed "psp_ensures"; 
4776  329 

6536  330 
Goal "[ F : A leadsTo A'; F : B co B' ] \ 
6714  331 
\ ==> F : (A Int B') leadsTo ((A' Int B) Un (B'  B))"; 
4776  332 
by (etac leadsTo_induct 1); 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

333 
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); 
4776  334 
(*Transitivity case has a delicate argument involving "cancellation"*) 
335 
by (rtac leadsTo_Un_duplicate2 2); 

336 
by (etac leadsTo_cancel_Diff1 2); 

337 
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2); 

6714  338 
by (blast_tac (claset() addIs [leadsTo_weaken_L] 
339 
addDs [constrains_imp_subset]) 2); 

4776  340 
(*Basis case*) 
8835  341 
by (blast_tac (claset() addIs [psp_ensures]) 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

342 
qed "psp"; 
4776  343 

6536  344 
Goal "[ F : A leadsTo A'; F : B co B' ] \ 
6714  345 
\ ==> F : (B' Int A) leadsTo ((B Int A') Un (B'  B))"; 
5536  346 
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

347 
qed "psp2"; 
4776  348 

349 

5069  350 
Goalw [unless_def] 
6536  351 
"[ F : A leadsTo A'; F : B unless B' ] \ 
352 
\ ==> F : (A Int B) leadsTo ((A' Int B) Un B')"; 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

353 
by (dtac psp 1); 
4776  354 
by (assume_tac 1); 
6714  355 
by (blast_tac (claset() addIs [leadsTo_weaken]) 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

356 
qed "psp_unless"; 
4776  357 

358 

359 
(*** Proving the induction rules ***) 

360 

5257  361 
(** The most general rule: r is any wf relation; f is any variant function **) 
362 

5239  363 
Goal "[ wf r; \ 
6536  364 
\ ALL m. F : (A Int f``{m}) leadsTo \ 
7524  365 
\ ((A Int f``(r^1 ^^ {m})) Un B) ] \ 
6536  366 
\ ==> F : (A Int f``{m}) leadsTo B"; 
4776  367 
by (eres_inst_tac [("a","m")] wf_induct 1); 
6536  368 
by (subgoal_tac "F : (A Int (f `` (r^1 ^^ {x}))) leadsTo B" 1); 
4776  369 
by (stac vimage_eq_UN 2); 
370 
by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2); 

371 
by (blast_tac (claset() addIs [leadsTo_UN]) 2); 

372 
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); 

373 
val lemma = result(); 

374 

375 

376 
(** Meta or object quantifier ????? **) 

5239  377 
Goal "[ wf r; \ 
6536  378 
\ ALL m. F : (A Int f``{m}) leadsTo \ 
7524  379 
\ ((A Int f``(r^1 ^^ {m})) Un B) ] \ 
6536  380 
\ ==> F : A leadsTo B"; 
4776  381 
by (res_inst_tac [("t", "A")] subst 1); 
382 
by (rtac leadsTo_UN 2); 

383 
by (etac lemma 2); 

384 
by (REPEAT (assume_tac 2)); 

385 
by (Fast_tac 1); (*Blast_tac: Function unknown's argument not a parameter*) 

386 
qed "leadsTo_wf_induct"; 

387 

388 

5239  389 
Goal "[ wf r; \ 
6536  390 
\ ALL m:I. F : (A Int f``{m}) leadsTo \ 
7524  391 
\ ((A Int f``(r^1 ^^ {m})) Un B) ] \ 
6536  392 
\ ==> F : A leadsTo ((A  (f``I)) Un B)"; 
4776  393 
by (etac leadsTo_wf_induct 1); 
394 
by Safe_tac; 

395 
by (case_tac "m:I" 1); 

396 
by (blast_tac (claset() addIs [leadsTo_weaken]) 1); 

397 
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); 

398 
qed "bounded_induct"; 

399 

400 

6536  401 
(*Alternative proof is via the lemma F : (A Int f``(lessThan m)) leadsTo B*) 
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8122
diff
changeset

402 
val prems = 
8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8835
diff
changeset

403 
Goal "[ !!m::nat. F : (A Int f``{m}) leadsTo ((A Int f``{..m(}) Un B) ] \ 
6536  404 
\ ==> F : A leadsTo B"; 
4776  405 
by (rtac (wf_less_than RS leadsTo_wf_induct) 1); 
406 
by (Asm_simp_tac 1); 

8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8122
diff
changeset

407 
by (blast_tac (claset() addIs prems) 1); 
4776  408 
qed "lessThan_induct"; 
409 

8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8835
diff
changeset

410 
Goal "!!l::nat. [ ALL m:(greaterThan l). \ 
7524  411 
\ F : (A Int f``{m}) leadsTo ((A Int f``(lessThan m)) Un B) ] \ 
6536  412 
\ ==> F : A leadsTo ((A Int (f``(atMost l))) Un B)"; 
5648  413 
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
414 
Compl_greaterThan RS sym]) 1); 

4776  415 
by (rtac (wf_less_than RS bounded_induct) 1); 
416 
by (Asm_simp_tac 1); 

417 
qed "lessThan_bounded_induct"; 

418 

8948
b797cfa3548d
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
paulson
parents:
8835
diff
changeset

419 
Goal "!!l::nat. [ ALL m:(lessThan l). \ 
7524  420 
\ F : (A Int f``{m}) leadsTo ((A Int f``(greaterThan m)) Un B) ] \ 
6536  421 
\ ==> F : A leadsTo ((A Int (f``(atLeast l))) Un B)"; 
4776  422 
by (res_inst_tac [("f","f"),("f1", "%k. l  k")] 
423 
(wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1); 

424 
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1); 

425 
by (Clarify_tac 1); 

426 
by (case_tac "m<l" 1); 

427 
by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2); 

428 
by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1); 

429 
qed "greaterThan_bounded_induct"; 

430 

431 

432 
(*** wlt ****) 

433 

434 
(*Misra's property W3*) 

6536  435 
Goalw [wlt_def] "F : (wlt F B) leadsTo B"; 
4776  436 
by (blast_tac (claset() addSIs [leadsTo_Union]) 1); 
437 
qed "wlt_leadsTo"; 

438 

6536  439 
Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt F B"; 
4776  440 
by (blast_tac (claset() addSIs [leadsTo_Union]) 1); 
441 
qed "leadsTo_subset"; 

442 

443 
(*Misra's property W2*) 

6536  444 
Goal "F : A leadsTo B = (A <= wlt F B)"; 
4776  445 
by (blast_tac (claset() addSIs [leadsTo_subset, 
446 
wlt_leadsTo RS leadsTo_weaken_L]) 1); 

447 
qed "leadsTo_eq_subset_wlt"; 

448 

449 
(*Misra's property W4*) 

5648  450 
Goal "B <= wlt F B"; 
4776  451 
by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym, 
452 
subset_imp_leadsTo]) 1); 

453 
qed "wlt_increasing"; 

454 

455 

456 
(*Used in the Trans case below*) 

5069  457 
Goalw [constrains_def] 
5111  458 
"[ B <= A2; \ 
6536  459 
\ F : (A1  B) co (A1 Un B); \ 
460 
\ F : (A2  C) co (A2 Un C) ] \ 

461 
\ ==> F : (A1 Un A2  C) co (A1 Un A2 Un C)"; 

5669  462 
by (Clarify_tac 1); 
5620  463 
by (Blast_tac 1); 
4776  464 
val lemma1 = result(); 
465 

466 

467 
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) 

8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

468 
Goal "F : A leadsTo A' \ 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

469 
\ ==> EX B. A<=B & F : B leadsTo A' & F : (BA') co (B Un A')"; 
4776  470 
by (etac leadsTo_induct 1); 
471 
(*Basis*) 

8835  472 
by (blast_tac (claset() addDs [ensuresD]) 1); 
4776  473 
(*Trans*) 
474 
by (Clarify_tac 1); 

475 
by (res_inst_tac [("x", "Ba Un Bb")] exI 1); 

476 
by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1, 

477 
leadsTo_Un_duplicate]) 1); 

478 
(*Union*) 

8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

479 
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1, bchoice]) 1);; 
4776  480 
by (res_inst_tac [("x", "UN A:S. f A")] exI 1); 
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

481 
by (auto_tac (claset() addIs [leadsTo_UN], simpset())); 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

482 
(*Blast_tac says PROOF FAILED*) 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

483 
by (deepen_tac (claset() addIs [constrains_UN RS constrains_weaken]) 0 1); 
4776  484 
qed "leadsTo_123"; 
485 

486 

487 
(*Misra's property W5*) 

6536  488 
Goal "F : (wlt F B  B) co (wlt F B)"; 
5648  489 
by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1); 
4776  490 
by (Clarify_tac 1); 
5648  491 
by (subgoal_tac "Ba = wlt F B" 1); 
492 
by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2); 

4776  493 
by (Clarify_tac 1); 
494 
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1); 

495 
qed "wlt_constrains_wlt"; 

496 

497 

498 
(*** Completion: Binary and General Finite versions ***) 

499 

5648  500 
Goal "[ W = wlt F (B' Un C); \ 
6536  501 
\ F : A leadsTo (A' Un C); F : A' co (A' Un C); \ 
502 
\ F : B leadsTo (B' Un C); F : B' co (B' Un C) ] \ 

503 
\ ==> F : (A Int B) leadsTo ((A' Int B') Un C)"; 

504 
by (subgoal_tac "F : (WC) co (W Un B' Un C)" 1); 

4776  505 
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
506 
MRS constrains_Un RS constrains_weaken]) 2); 

6536  507 
by (subgoal_tac "F : (WC) co W" 1); 
4776  508 
by (asm_full_simp_tac 
509 
(simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2); 

6536  510 
by (subgoal_tac "F : (A Int W  C) leadsTo (A' Int W Un C)" 1); 
6714  511 
by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2); 
7963  512 
(** LEVEL 6 **) 
6536  513 
by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1); 
6714  514 
by (rtac leadsTo_Un_duplicate2 2); 
515 
by (blast_tac (claset() addIs [leadsTo_Un_Un, 

516 
wlt_leadsTo RS psp2 RS leadsTo_weaken, 

8112
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

517 
leadsTo_refl]) 2); 
4776  518 
by (dtac leadsTo_Diff 1); 
519 
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); 

520 
by (subgoal_tac "A Int B <= A Int W" 1); 

5456  521 
by (blast_tac (claset() addSDs [leadsTo_subset] 
522 
addSIs [subset_refl RS Int_mono]) 2); 

4776  523 
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); 
524 
bind_thm("completion", refl RS result()); 

525 

526 

6536  527 
Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) > \ 
528 
\ (ALL i:I. F : (A' i) co (A' i Un C)) > \ 

529 
\ F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"; 

4776  530 
by (etac finite_induct 1); 
7963  531 
by Auto_tac; 
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

532 
by (rtac completion 1); 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

533 
by (simp_tac (HOL_ss addsimps (INT_simps RL [sym])) 4); 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

534 
by (rtac constrains_INT 4); 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

535 
by Auto_tac; 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

536 
val lemma = result(); 
4776  537 

8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

538 
val prems = Goal 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

539 
"[ finite I; \ 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

540 
\ !!i. i:I ==> F : (A i) leadsTo (A' i Un C); \ 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

541 
\ !!i. i:I ==> F : (A' i) co (A' i Un C) ] \ 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

542 
\ ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"; 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

543 
by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1); 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

544 
qed "finite_completion"; 
7963  545 

546 
Goalw [stable_def] 

547 
"[ F : A leadsTo A'; F : stable A'; \ 

548 
\ F : B leadsTo B'; F : stable B' ] \ 

549 
\ ==> F : (A Int B) leadsTo (A' Int B')"; 

550 
by (res_inst_tac [("C1", "{}")] (completion RS leadsTo_weaken_R) 1); 

551 
by (REPEAT (Force_tac 1)); 

552 
qed "stable_completion"; 

553 

8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

554 
val prems = Goalw [stable_def] 
7963  555 
"[ finite I; \ 
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

556 
\ !!i. i:I ==> F : (A i) leadsTo (A' i); \ 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

557 
\ !!i. i:I ==> F : stable (A' i) ] \ 
7963  558 
\ ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"; 
559 
by (res_inst_tac [("C1", "{}")] (finite_completion RS leadsTo_weaken_R) 1); 

8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

560 
by (ALLGOALS Asm_simp_tac); 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

561 
by (ALLGOALS (blast_tac (claset() addIs prems))); 
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

562 
qed "finite_stable_completion"; 
7963  563 

564 