author  paulson 
Fri, 03 Mar 2000 18:26:19 +0100  
changeset 8334  7896bcbd8641 
parent 8251  9be357df93d4 
child 8835  56187238220d 
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 

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 

5648  98 
Goalw [leadsTo_def] 
6536  99 
"[ 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

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

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

106 
qed "transient_imp_leadsTo"; 

107 

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

112 

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

116 

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

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

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

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

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

125 
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

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

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

128 

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

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

135 
(*Binary union introduction rule*) 

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

139 
qed "leadsTo_Un"; 

140 

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

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

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

145 
qed "single_leadsTo_I"; 

146 

4776  147 

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

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

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

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

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

159 

160 

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

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

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

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

165 

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

166 
bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); 
4776  167 

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

168 
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

169 

4776  170 
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); 
171 
Addsimps [empty_leadsTo]; 

172 

8041  173 
bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo); 
174 
Addsimps [leadsTo_UNIV]; 

175 

4776  176 

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

177 

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

178 
(** Variant induction rule: on the preconditions for B **) 
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 
(*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

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

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

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

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

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

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

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

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

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

190 
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

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

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

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

194 

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

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

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

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

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

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

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

201 
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

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

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

204 
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

205 
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

206 
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

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

208 

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

209 

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

4776  213 

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

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

218 
(*Distributes over binary unions*) 

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

222 

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

226 

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

230 

231 

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

4776  235 
qed "leadsTo_weaken"; 
236 

237 

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

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

242 

243 
val prems = goal thy 

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

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

249 
qed "leadsTo_UN_UN"; 

250 

251 
(*Binary union version*) 

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

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

256 
qed "leadsTo_Un_Un"; 

257 

258 

259 
(** The cancellation law **) 

260 

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

265 
qed "leadsTo_cancel2"; 

266 

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

271 
by (ALLGOALS Asm_simp_tac); 

272 
qed "leadsTo_cancel_Diff2"; 

273 

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

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

278 
qed "leadsTo_cancel1"; 

279 

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

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

284 
by (ALLGOALS Asm_simp_tac); 

285 
qed "leadsTo_cancel_Diff1"; 

286 

287 

288 

289 
(** The impossibility law **) 

290 

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

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

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

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

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

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

298 

299 

300 
(** PSP: ProgressSafetyProgress **) 

301 

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

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

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

310 
by (asm_full_simp_tac 

311 
(simpset() addsimps [ensures_def, 

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

313 
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

314 
qed "psp_stable"; 
4776  315 

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

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

319 
qed "psp_stable2"; 
4776  320 

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

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

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

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

326 
qed "psp_ensures"; 
4776  327 

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

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

334 
by (etac leadsTo_cancel_Diff1 2); 

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

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

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

339 
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

340 
qed "psp"; 
4776  341 

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

345 
qed "psp2"; 
4776  346 

347 

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

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

354 
qed "psp_unless"; 
4776  355 

356 

357 
(*** Proving the induction rules ***) 

358 

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

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

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

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

371 
val lemma = result(); 

372 

373 

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

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

381 
by (etac lemma 2); 

382 
by (REPEAT (assume_tac 2)); 

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

384 
qed "leadsTo_wf_induct"; 

385 

386 

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

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

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

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

396 
qed "bounded_induct"; 

397 

398 

6536  399 
(*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

400 
val prems = 
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8122
diff
changeset

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

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

405 
by (blast_tac (claset() addIs prems) 1); 
4776  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"*) 

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

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

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

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

470 
by (blast_tac (claset() addIs [leadsTo_Basis] addDs [ensuresD]) 1); 
4776  471 
(*Trans*) 
472 
by (Clarify_tac 1); 

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

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

475 
leadsTo_Un_duplicate]) 1); 

476 
(*Union*) 

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

477 
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1, bchoice]) 1);; 
4776  478 
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

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

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

481 
by (deepen_tac (claset() addIs [constrains_UN RS constrains_weaken]) 0 1); 
4776  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; 
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset

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

531 
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

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

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

534 
val lemma = result(); 
4776  535 

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

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

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

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

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

540 
\ ==> 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

541 
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

542 
qed "finite_completion"; 
7963  543 

544 
Goalw [stable_def] 

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

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

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

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

549 
by (REPEAT (Force_tac 1)); 

550 
qed "stable_completion"; 

551 

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

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

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

555 
\ !!i. i:I ==> F : stable (A' i) ] \ 
7963  556 
\ ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"; 
557 
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

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

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

560 
qed "finite_stable_completion"; 
7963  561 

562 