author  paulson 
Fri, 07 Jan 2000 11:00:56 +0100  
changeset 8112  efbe50e2bef9 
parent 8041  e3237d8c18d6 
child 8122  b43ad07660b9 
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 = {}"; 
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset

44 
by Auto_tac; 
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 

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

86 
qed "stable_transient_ensures"; 

87 

4776  88 

89 
(*** leadsTo ***) 

90 

6536  91 
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

92 
by (blast_tac (claset() addIs [leads.Basis]) 1); 
5648  93 
qed "leadsTo_Basis"; 
4776  94 

5648  95 
Goalw [leadsTo_def] 
6536  96 
"[ 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

97 
by (blast_tac (claset() addIs [leads.Trans]) 1); 
5648  98 
qed "leadsTo_Trans"; 
99 

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

103 
qed "transient_imp_leadsTo"; 

104 

4776  105 
(*Useful with cancellation, disjunction*) 
6536  106 
Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; 
4776  107 
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); 
108 
qed "leadsTo_Un_duplicate"; 

109 

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

113 

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

5648  115 
val prems = Goalw [leadsTo_def] 
6536  116 
"(!!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

117 
by (blast_tac (claset() addIs [leads.Union] addDs prems) 1); 
4776  118 
qed "leadsTo_Union"; 
119 

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

120 
val prems = Goalw [leadsTo_def] 
7524  121 
"(!!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

122 
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

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

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

125 

5648  126 
val prems = Goal 
6536  127 
"(!!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

128 
by (stac (Union_image_eq RS sym) 1); 
5648  129 
by (blast_tac (claset() addIs leadsTo_Union::prems) 1); 
4776  130 
qed "leadsTo_UN"; 
131 

132 
(*Binary union introduction rule*) 

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

136 
qed "leadsTo_Un"; 

137 

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

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

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

142 
qed "single_leadsTo_I"; 

143 

4776  144 

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

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

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

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

153 
by (rtac (major RS CollectD RS leads.induct) 1); 
4776  154 
by (REPEAT (blast_tac (claset() addIs prems) 1)); 
155 
qed "leadsTo_induct"; 

156 

157 

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

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

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

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

162 

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

163 
bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); 
4776  164 

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

165 
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

166 

4776  167 
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); 
168 
Addsimps [empty_leadsTo]; 

169 

8041  170 
bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo); 
171 
Addsimps [leadsTo_UNIV]; 

172 

4776  173 

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

174 

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

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

176 

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

177 
(*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

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

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

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

181 
\ !!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

182 
\ !!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

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

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

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

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

187 
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

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

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

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

191 

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

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

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

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

195 
\ !!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

196 
\ !!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

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

198 
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

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

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

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

202 
by (blast_tac (claset() addIs [leadsTo_Basis,leadsTo_Trans]@prems) 2); 
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset

203 
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

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

205 

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

206 

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

4776  210 

6536  211 
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

212 
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); 
4776  213 
qed_spec_mp "leadsTo_weaken_L"; 
214 

215 
(*Distributes over binary unions*) 

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

219 

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

223 

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

227 

228 

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

4776  232 
qed "leadsTo_weaken"; 
233 

234 

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

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

239 

240 

241 
(** Meta or object quantifier ??? 

242 
see ball_constrains_UN in UNITY.ML***) 

243 

244 
val prems = goal thy 

6536  245 
"(!! i. i:I ==> F : (A i) leadsTo (A' i)) \ 
246 
\ ==> 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

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

250 
qed "leadsTo_UN_UN"; 

251 

252 
(*Binary union version*) 

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

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

257 
qed "leadsTo_Un_Un"; 

258 

259 

260 
(** The cancellation law **) 

261 

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

266 
qed "leadsTo_cancel2"; 

267 

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

272 
by (ALLGOALS Asm_simp_tac); 

273 
qed "leadsTo_cancel_Diff2"; 

274 

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

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

279 
qed "leadsTo_cancel1"; 

280 

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

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

285 
by (ALLGOALS Asm_simp_tac); 

286 
qed "leadsTo_cancel_Diff1"; 

287 

288 

289 

290 
(** The impossibility law **) 

291 

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

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

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

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

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

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

299 

300 

301 
(** PSP: ProgressSafetyProgress **) 

302 

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

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

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

311 
by (asm_full_simp_tac 

312 
(simpset() addsimps [ensures_def, 

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

314 
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

315 
qed "psp_stable"; 
4776  316 

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

5536  319 
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

320 
qed "psp_stable2"; 
4776  321 

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

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

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

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

327 
qed "psp_ensures"; 
4776  328 

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

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

335 
by (etac leadsTo_cancel_Diff1 2); 

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

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

4776  339 
(*Basis case*) 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset

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

341 
qed "psp"; 
4776  342 

6536  343 
Goal "[ F : A leadsTo A'; F : B co B' ] \ 
6714  344 
\ ==> F : (B' Int A) leadsTo ((B Int A') Un (B'  B))"; 
5536  345 
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

346 
qed "psp2"; 
4776  347 

348 

5069  349 
Goalw [unless_def] 
6536  350 
"[ F : A leadsTo A'; F : B unless B' ] \ 
351 
\ ==> 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

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

355 
qed "psp_unless"; 
4776  356 

357 

358 
(*** Proving the induction rules ***) 

359 

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

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

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

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

372 
val lemma = result(); 

373 

374 

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

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

382 
by (etac lemma 2); 

383 
by (REPEAT (assume_tac 2)); 

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

385 
qed "leadsTo_wf_induct"; 

386 

387 

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

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

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

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

397 
qed "bounded_induct"; 

398 

399 

6536  400 
(*Alternative proof is via the lemma F : (A Int f``(lessThan m)) leadsTo B*) 
401 
Goal "[ ALL m. F : (A Int f``{m}) leadsTo \ 

7524  402 
\ ((A Int f``(lessThan m)) Un B) ] \ 
6536  403 
\ ==> F : A leadsTo B"; 
4776  404 
by (rtac (wf_less_than RS leadsTo_wf_induct) 1); 
405 
by (Asm_simp_tac 1); 

406 
qed "lessThan_induct"; 

407 

7524  408 
Goal "[ ALL m:(greaterThan l). \ 
409 
\ F : (A Int f``{m}) leadsTo ((A Int f``(lessThan m)) Un B) ] \ 

6536  410 
\ ==> F : A leadsTo ((A Int (f``(atMost l))) Un B)"; 
5648  411 
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
412 
Compl_greaterThan RS sym]) 1); 

4776  413 
by (rtac (wf_less_than RS bounded_induct) 1); 
414 
by (Asm_simp_tac 1); 

415 
qed "lessThan_bounded_induct"; 

416 

7524  417 
Goal "[ ALL m:(lessThan l). \ 
418 
\ F : (A Int f``{m}) leadsTo ((A Int f``(greaterThan m)) Un B) ] \ 

6536  419 
\ ==> F : A leadsTo ((A Int (f``(atLeast l))) Un B)"; 
4776  420 
by (res_inst_tac [("f","f"),("f1", "%k. l  k")] 
421 
(wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1); 

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

423 
by (Clarify_tac 1); 

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

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

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

427 
qed "greaterThan_bounded_induct"; 

428 

429 

430 
(*** wlt ****) 

431 

432 
(*Misra's property W3*) 

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

436 

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

440 

441 
(*Misra's property W2*) 

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

445 
qed "leadsTo_eq_subset_wlt"; 

446 

447 
(*Misra's property W4*) 

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

451 
qed "wlt_increasing"; 

452 

453 

454 
(*Used in the Trans case below*) 

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

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

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

464 

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

6536  466 
Goal "F : A leadsTo A' ==> \ 
467 
\ EX B. A<=B & F : B leadsTo A' & F : (BA') co (B Un A')"; 

4776  468 
by (etac leadsTo_induct 1); 
469 
(*Basis*) 

470 
by (blast_tac (claset() addIs [leadsTo_Basis] 

471 
addDs [ensuresD]) 1); 

472 
(*Trans*) 

473 
by (Clarify_tac 1); 

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

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

476 
leadsTo_Un_duplicate]) 1); 

477 
(*Union*) 

478 
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1, 

479 
bchoice, ball_constrains_UN]) 1);; 

480 
by (res_inst_tac [("x", "UN A:S. f A")] exI 1); 

481 
by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1); 

482 
qed "leadsTo_123"; 

483 

484 

485 
(*Misra's property W5*) 

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

4776  491 
by (Clarify_tac 1); 
492 
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1); 

493 
qed "wlt_constrains_wlt"; 

494 

495 

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

497 

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

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

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

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

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

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

514 
wlt_leadsTo RS psp2 RS leadsTo_weaken, 

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

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

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

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

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

523 

524 

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

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

4776  528 
by (etac finite_induct 1); 
7963  529 
by Auto_tac; 
4776  530 
by (dtac ball_constrains_INT 1); 
531 
by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 

6564  532 
qed_spec_mp "finite_completion"; 
4776  533 

7963  534 

535 
Goalw [stable_def] 

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

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

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

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

540 
by (REPEAT (Force_tac 1)); 

541 
qed "stable_completion"; 

542 

543 
Goalw [stable_def] 

544 
"[ finite I; \ 

545 
\ ALL i:I. F : (A i) leadsTo (A' i); \ 

546 
\ ALL i:I. F : stable (A' i) ] \ 

547 
\ ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"; 

548 
by (res_inst_tac [("C1", "{}")] (finite_completion RS leadsTo_weaken_R) 1); 

549 
by (REPEAT (Force_tac 1)); 

550 
qed_spec_mp "finite_stable_completion"; 

551 

552 