37936

1 
(* Title: ZF/UNITY/WFair.thy

11479

2 
Author: Sidi Ehmety, Computer Laboratory


3 
Copyright 1998 University of Cambridge


4 
*)


5 

15634

6 
header{*Progress under Weak Fairness*}


7 


8 
theory WFair


9 
imports UNITY Main_ZFC


10 
begin


11 


12 
text{*This theory defines the operators transient, ensures and leadsTo,


13 
assuming weak fairness. From Misra, "A Logic for Concurrent Programming",


14 
1994.*}


15 

24893

16 
definition

12195

17 
(* This definition specifies weak fairness. The rest of the theory

46953

18 
is generic to all forms of fairness.*)

24893

19 
transient :: "i=>i" where

46953

20 
"transient(A) =={F \<in> program. (\<exists>act\<in>Acts(F). A<=domain(act) &

46823

21 
act``A \<subseteq> stateA) & st_set(A)}"

11479

22 

24893

23 
definition


24 
ensures :: "[i,i] => i" (infixl "ensures" 60) where

46823

25 
"A ensures B == ((AB) co (A \<union> B)) \<inter> transient(AB)"

46953

26 

11479

27 
consts


28 


29 
(*LEADSTO constant for the inductive definition*)

12195

30 
leads :: "[i, i]=>i"

11479

31 

46953

32 
inductive

11479

33 
domains

46823

34 
"leads(D, F)" \<subseteq> "Pow(D)*Pow(D)"

46953

35 
intros


36 
Basis: "[ F \<in> A ensures B; A \<in> Pow(D); B \<in> Pow(D) ] ==> <A,B>:leads(D, F)"

46823

37 
Trans: "[ <A,B> \<in> leads(D, F); <B,C> \<in> leads(D, F) ] ==> <A,C>:leads(D, F)"

46953

38 
Union: "[ S \<in> Pow({A \<in> S. <A, B>:leads(D, F)}); B \<in> Pow(D); S \<in> Pow(Pow(D)) ] ==>

46823

39 
<\<Union>(S),B>:leads(D, F)"

11479

40 


41 
monos Pow_mono

15634

42 
type_intros Union_Pow_iff [THEN iffD2] UnionI PowI

46953

43 

24893

44 
definition

12195

45 
(* The Visible version of the LEADSTO relation*)

24893

46 
leadsTo :: "[i, i] => i" (infixl "leadsTo" 60) where

46953

47 
"A leadsTo B == {F \<in> program. <A,B>:leads(state, F)}"


48 

24893

49 
definition

12195

50 
(* wlt(F, B) is the largest set that leads to B*)

24893

51 
wlt :: "[i, i] => i" where

46953

52 
"wlt(F, B) == \<Union>({A \<in> Pow(state). F \<in> A leadsTo B})"

11479

53 

24893

54 
notation (xsymbols)


55 
leadsTo (infixl "\<longmapsto>" 60)

15634

56 


57 
(** Adhoc settheory rules **)


58 

46823

59 
lemma Int_Union_Union: "\<Union>(B) \<inter> A = (\<Union>b \<in> B. b \<inter> A)"

15634

60 
by auto


61 

46823

62 
lemma Int_Union_Union2: "A \<inter> \<Union>(B) = (\<Union>b \<in> B. A \<inter> b)"

15634

63 
by auto


64 


65 
(*** transient ***)


66 


67 
lemma transient_type: "transient(A)<=program"


68 
by (unfold transient_def, auto)


69 

46953

70 
lemma transientD2:

15634

71 
"F \<in> transient(A) ==> F \<in> program & st_set(A)"


72 
apply (unfold transient_def, auto)


73 
done


74 


75 
lemma stable_transient_empty: "[ F \<in> stable(A); F \<in> transient(A) ] ==> A = 0"


76 
by (simp add: stable_def constrains_def transient_def, fast)


77 


78 
lemma transient_strengthen: "[F \<in> transient(A); B<=A] ==> F \<in> transient(B)"


79 
apply (simp add: transient_def st_set_def, clarify)


80 
apply (blast intro!: rev_bexI)


81 
done


82 

46953

83 
lemma transientI:


84 
"[act \<in> Acts(F); A \<subseteq> domain(act); act``A \<subseteq> stateA;

15634

85 
F \<in> program; st_set(A)] ==> F \<in> transient(A)"


86 
by (simp add: transient_def, blast)


87 

46953

88 
lemma transientE:


89 
"[ F \<in> transient(A);

46823

90 
!!act. [ act \<in> Acts(F); A \<subseteq> domain(act); act``A \<subseteq> stateA]==>P]

15634

91 
==>P"


92 
by (simp add: transient_def, blast)


93 


94 
lemma transient_state: "transient(state) = 0"


95 
apply (simp add: transient_def)

46953

96 
apply (rule equalityI, auto)

15634

97 
apply (cut_tac F = x in Acts_type)


98 
apply (simp add: Diff_cancel)


99 
apply (auto intro: st0_in_state)


100 
done


101 


102 
lemma transient_state2: "state<=B ==> transient(B) = 0"


103 
apply (simp add: transient_def st_set_def)


104 
apply (rule equalityI, auto)


105 
apply (cut_tac F = x in Acts_type)


106 
apply (subgoal_tac "B=state")


107 
apply (auto intro: st0_in_state)


108 
done


109 


110 
lemma transient_empty: "transient(0) = program"


111 
by (auto simp add: transient_def)


112 


113 
declare transient_empty [simp] transient_state [simp] transient_state2 [simp]


114 


115 
(*** ensures ***)


116 


117 
lemma ensures_type: "A ensures B <=program"


118 
by (simp add: ensures_def constrains_def, auto)


119 

46953

120 
lemma ensuresI:

46823

121 
"[F:(AB) co (A \<union> B); F \<in> transient(AB)]==>F \<in> A ensures B"

15634

122 
apply (unfold ensures_def)


123 
apply (auto simp add: transient_type [THEN subsetD])


124 
done


125 


126 
(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *)

46823

127 
lemma ensuresI2: "[ F \<in> A co A \<union> B; F \<in> transient(A) ] ==> F \<in> A ensures B"

15634

128 
apply (drule_tac B = "AB" in constrains_weaken_L)


129 
apply (drule_tac [2] B = "AB" in transient_strengthen)


130 
apply (auto simp add: ensures_def transient_type [THEN subsetD])


131 
done


132 

46823

133 
lemma ensuresD: "F \<in> A ensures B ==> F:(AB) co (A \<union> B) & F \<in> transient (AB)"

15634

134 
by (unfold ensures_def, auto)


135 


136 
lemma ensures_weaken_R: "[F \<in> A ensures A'; A'<=B' ] ==> F \<in> A ensures B'"


137 
apply (unfold ensures_def)


138 
apply (blast intro: transient_strengthen constrains_weaken)


139 
done


140 

46953

141 
(*The Lversion (precondition strengthening) fails, but we have this*)


142 
lemma stable_ensures_Int:

46823

143 
"[ F \<in> stable(C); F \<in> A ensures B ] ==> F:(C \<inter> A) ensures (C \<inter> B)"

46953

144 

15634

145 
apply (unfold ensures_def)


146 
apply (simp (no_asm) add: Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])


147 
apply (blast intro: transient_strengthen stable_constrains_Int constrains_weaken)


148 
done


149 

46823

150 
lemma stable_transient_ensures: "[F \<in> stable(A); F \<in> transient(C); A<=B \<union> C] ==> F \<in> A ensures B"

15634

151 
apply (frule stable_type [THEN subsetD])


152 
apply (simp add: ensures_def stable_def)


153 
apply (blast intro: transient_strengthen constrains_weaken)


154 
done


155 

46823

156 
lemma ensures_eq: "(A ensures B) = (A unless B) \<inter> transient (AB)"

15634

157 
by (auto simp add: ensures_def unless_def)


158 


159 
lemma subset_imp_ensures: "[ F \<in> program; A<=B ] ==> F \<in> A ensures B"


160 
by (auto simp add: ensures_def constrains_def transient_def st_set_def)


161 


162 
(*** leadsTo ***)


163 
lemmas leads_left = leads.dom_subset [THEN subsetD, THEN SigmaD1]


164 
lemmas leads_right = leads.dom_subset [THEN subsetD, THEN SigmaD2]


165 

46823

166 
lemma leadsTo_type: "A leadsTo B \<subseteq> program"

15634

167 
by (unfold leadsTo_def, auto)


168 

46953

169 
lemma leadsToD2:

15634

170 
"F \<in> A leadsTo B ==> F \<in> program & st_set(A) & st_set(B)"


171 
apply (unfold leadsTo_def st_set_def)


172 
apply (blast dest: leads_left leads_right)


173 
done


174 

46953

175 
lemma leadsTo_Basis:

15634

176 
"[F \<in> A ensures B; st_set(A); st_set(B)] ==> F \<in> A leadsTo B"


177 
apply (unfold leadsTo_def st_set_def)


178 
apply (cut_tac ensures_type)


179 
apply (auto intro: leads.Basis)


180 
done


181 
declare leadsTo_Basis [intro]


182 


183 
(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)


184 
(* [ F \<in> program; A<=B; st_set(A); st_set(B) ] ==> A leadsTo B *)

45602

185 
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]

15634

186 


187 
lemma leadsTo_Trans: "[F \<in> A leadsTo B; F \<in> B leadsTo C ]==>F \<in> A leadsTo C"


188 
apply (unfold leadsTo_def)


189 
apply (auto intro: leads.Trans)


190 
done


191 


192 
(* Better when used in association with leadsTo_weaken_R *)


193 
lemma transient_imp_leadsTo: "F \<in> transient(A) ==> F \<in> A leadsTo (stateA)"


194 
apply (unfold transient_def)


195 
apply (blast intro: ensuresI [THEN leadsTo_Basis] constrains_weaken transientI)


196 
done


197 


198 
(*Useful with cancellation, disjunction*)

46823

199 
lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"

15634

200 
by simp


201 


202 
lemma leadsTo_Un_duplicate2:

46823

203 
"F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"

15634

204 
by (simp add: Un_ac)


205 


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

46953

207 
lemma leadsTo_Union:

15634

208 
"[!!A. A \<in> S ==> F \<in> A leadsTo B; F \<in> program; st_set(B)]

46823

209 
==> F \<in> \<Union>(S) leadsTo B"

15634

210 
apply (unfold leadsTo_def st_set_def)


211 
apply (blast intro: leads.Union dest: leads_left)


212 
done


213 

46953

214 
lemma leadsTo_Union_Int:


215 
"[!!A. A \<in> S ==>F \<in> (A \<inter> C) leadsTo B; F \<in> program; st_set(B)]

46823

216 
==> F \<in> (\<Union>(S)Int C)leadsTo B"

15634

217 
apply (unfold leadsTo_def st_set_def)


218 
apply (simp only: Int_Union_Union)


219 
apply (blast dest: leads_left intro: leads.Union)


220 
done


221 

46953

222 
lemma leadsTo_UN:

15634

223 
"[ !!i. i \<in> I ==> F \<in> A(i) leadsTo B; F \<in> program; st_set(B)]


224 
==> F:(\<Union>i \<in> I. A(i)) leadsTo B"


225 
apply (simp add: Int_Union_Union leadsTo_def st_set_def)


226 
apply (blast dest: leads_left intro: leads.Union)


227 
done


228 


229 
(* Binary union introduction rule *)


230 
lemma leadsTo_Un:

46823

231 
"[ F \<in> A leadsTo C; F \<in> B leadsTo C ] ==> F \<in> (A \<union> B) leadsTo C"

15634

232 
apply (subst Un_eq_Union)


233 
apply (blast intro: leadsTo_Union dest: leadsToD2)


234 
done


235 


236 
lemma single_leadsTo_I:

46953

237 
"[!!x. x \<in> A==> F:{x} leadsTo B; F \<in> program; st_set(B) ]

15634

238 
==> F \<in> A leadsTo B"


239 
apply (rule_tac b = A in UN_singleton [THEN subst])

46953

240 
apply (rule leadsTo_UN, auto)

15634

241 
done


242 


243 
lemma leadsTo_refl: "[ F \<in> program; st_set(A) ] ==> F \<in> A leadsTo A"


244 
by (blast intro: subset_imp_leadsTo)


245 

46823

246 
lemma leadsTo_refl_iff: "F \<in> A leadsTo A \<longleftrightarrow> F \<in> program & st_set(A)"

15634

247 
by (auto intro: leadsTo_refl dest: leadsToD2)


248 

46823

249 
lemma empty_leadsTo: "F \<in> 0 leadsTo B \<longleftrightarrow> (F \<in> program & st_set(B))"

15634

250 
by (auto intro: subset_imp_leadsTo dest: leadsToD2)


251 
declare empty_leadsTo [iff]


252 

46823

253 
lemma leadsTo_state: "F \<in> A leadsTo state \<longleftrightarrow> (F \<in> program & st_set(A))"

15634

254 
by (auto intro: subset_imp_leadsTo dest: leadsToD2 st_setD)


255 
declare leadsTo_state [iff]


256 


257 
lemma leadsTo_weaken_R: "[ F \<in> A leadsTo A'; A'<=B'; st_set(B') ] ==> F \<in> A leadsTo B'"


258 
by (blast dest: leadsToD2 intro: subset_imp_leadsTo leadsTo_Trans)


259 


260 
lemma leadsTo_weaken_L: "[ F \<in> A leadsTo A'; B<=A ] ==> F \<in> B leadsTo A'"


261 
apply (frule leadsToD2)


262 
apply (blast intro: leadsTo_Trans subset_imp_leadsTo st_set_subset)


263 
done


264 


265 
lemma leadsTo_weaken: "[ F \<in> A leadsTo A'; B<=A; A'<=B'; st_set(B')]==> F \<in> B leadsTo B'"


266 
apply (frule leadsToD2)


267 
apply (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans leadsTo_refl)


268 
done


269 


270 
(* This rule has a nicer conclusion *)


271 
lemma transient_imp_leadsTo2: "[ F \<in> transient(A); stateA<=B; st_set(B)] ==> F \<in> A leadsTo B"


272 
apply (frule transientD2)


273 
apply (rule leadsTo_weaken_R)


274 
apply (auto simp add: transient_imp_leadsTo)


275 
done


276 


277 
(*Distributes over binary unions*)

46823

278 
lemma leadsTo_Un_distrib: "F:(A \<union> B) leadsTo C \<longleftrightarrow> (F \<in> A leadsTo C & F \<in> B leadsTo C)"

15634

279 
by (blast intro: leadsTo_Un leadsTo_weaken_L)


280 

46953

281 
lemma leadsTo_UN_distrib:

46823

282 
"(F:(\<Union>i \<in> I. A(i)) leadsTo B)\<longleftrightarrow> ((\<forall>i \<in> I. F \<in> A(i) leadsTo B) & F \<in> program & st_set(B))"

15634

283 
apply (blast dest: leadsToD2 intro: leadsTo_UN leadsTo_weaken_L)


284 
done


285 

46823

286 
lemma leadsTo_Union_distrib: "(F \<in> \<Union>(S) leadsTo B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A leadsTo B) & F \<in> program & st_set(B)"

15634

287 
by (blast dest: leadsToD2 intro: leadsTo_Union leadsTo_weaken_L)


288 


289 
text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}


290 
lemma leadsTo_Diff:


291 
"[ F: (AB) leadsTo C; F \<in> B leadsTo C; st_set(C) ]


292 
==> F \<in> A leadsTo C"


293 
by (blast intro: leadsTo_Un leadsTo_weaken dest: leadsToD2)


294 


295 
lemma leadsTo_UN_UN:

46953

296 
"[!!i. i \<in> I ==> F \<in> A(i) leadsTo A'(i); F \<in> program ]

15634

297 
==> F: (\<Union>i \<in> I. A(i)) leadsTo (\<Union>i \<in> I. A'(i))"


298 
apply (rule leadsTo_Union)

46953

299 
apply (auto intro: leadsTo_weaken_R dest: leadsToD2)

15634

300 
done


301 


302 
(*Binary union version*)

46823

303 
lemma leadsTo_Un_Un: "[ F \<in> A leadsTo A'; F \<in> B leadsTo B' ] ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"

15634

304 
apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') ")


305 
prefer 2 apply (blast dest: leadsToD2)


306 
apply (blast intro: leadsTo_Un leadsTo_weaken_R)


307 
done


308 


309 
(** The cancellation law **)

46823

310 
lemma leadsTo_cancel2: "[F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B'] ==> F \<in> A leadsTo (A' \<union> B')"

15634

311 
apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') &F \<in> program")


312 
prefer 2 apply (blast dest: leadsToD2)


313 
apply (blast intro: leadsTo_Trans leadsTo_Un_Un leadsTo_refl)


314 
done


315 

46823

316 
lemma leadsTo_cancel_Diff2: "[F \<in> A leadsTo (A' \<union> B); F \<in> (BA') leadsTo B']==> F \<in> A leadsTo (A' \<union> B')"

15634

317 
apply (rule leadsTo_cancel2)


318 
prefer 2 apply assumption


319 
apply (blast dest: leadsToD2 intro: leadsTo_weaken_R)


320 
done


321 


322 

46823

323 
lemma leadsTo_cancel1: "[ F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' ] ==> F \<in> A leadsTo (B' \<union> A')"

15634

324 
apply (simp add: Un_commute)


325 
apply (blast intro!: leadsTo_cancel2)


326 
done


327 


328 
lemma leadsTo_cancel_Diff1:

46823

329 
"[F \<in> A leadsTo (B \<union> A'); F: (BA') leadsTo B']==> F \<in> A leadsTo (B' \<union> A')"

15634

330 
apply (rule leadsTo_cancel1)


331 
prefer 2 apply assumption


332 
apply (blast intro: leadsTo_weaken_R dest: leadsToD2)


333 
done


334 


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


336 
lemma leadsTo_induct:


337 
assumes major: "F \<in> za leadsTo zb"


338 
and basis: "!!A B. [F \<in> A ensures B; st_set(A); st_set(B)] ==> P(A,B)"

46953

339 
and trans: "!!A B C. [ F \<in> A leadsTo B; P(A, B);

15634

340 
F \<in> B leadsTo C; P(B, C) ] ==> P(A,C)"

46953

341 
and union: "!!B S. [ \<forall>A \<in> S. F \<in> A leadsTo B; \<forall>A \<in> S. P(A,B);

46823

342 
st_set(B); \<forall>A \<in> S. st_set(A)] ==> P(\<Union>(S), B)"

15634

343 
shows "P(za, zb)"


344 
apply (cut_tac major)

46953

345 
apply (unfold leadsTo_def, clarify)


346 
apply (erule leads.induct)

15634

347 
apply (blast intro: basis [unfolded st_set_def])

46953

348 
apply (blast intro: trans [unfolded leadsTo_def])


349 
apply (force intro: union [unfolded st_set_def leadsTo_def])

15634

350 
done


351 


352 


353 
(* Added by Sidi, an induction rule without ensures *)


354 
lemma leadsTo_induct2:


355 
assumes major: "F \<in> za leadsTo zb"


356 
and basis1: "!!A B. [ A<=B; st_set(B) ] ==> P(A, B)"

46953

357 
and basis2: "!!A B. [ F \<in> A co A \<union> B; F \<in> transient(A); st_set(B) ]

15634

358 
==> P(A, B)"

46953

359 
and trans: "!!A B C. [ F \<in> A leadsTo B; P(A, B);

15634

360 
F \<in> B leadsTo C; P(B, C) ] ==> P(A,C)"

46953

361 
and union: "!!B S. [ \<forall>A \<in> S. F \<in> A leadsTo B; \<forall>A \<in> S. P(A,B);

46823

362 
st_set(B); \<forall>A \<in> S. st_set(A)] ==> P(\<Union>(S), B)"

15634

363 
shows "P(za, zb)"


364 
apply (cut_tac major)


365 
apply (erule leadsTo_induct)


366 
apply (auto intro: trans union)


367 
apply (simp add: ensures_def, clarify)


368 
apply (frule constrainsD2)

46823

369 
apply (drule_tac B' = " (AB) \<union> B" in constrains_weaken_R)

15634

370 
apply blast


371 
apply (frule ensuresI2 [THEN leadsTo_Basis])


372 
apply (drule_tac [4] basis2, simp_all)


373 
apply (frule_tac A1 = A and B = B in Int_lower2 [THEN basis1])

46823

374 
apply (subgoal_tac "A=\<Union>({A  B, A \<inter> B}) ")

15634

375 
prefer 2 apply blast


376 
apply (erule ssubst)


377 
apply (rule union)


378 
apply (auto intro: subset_imp_leadsTo)


379 
done


380 


381 


382 
(** Variant induction rule: on the preconditions for B **)


383 
(*Lemma is the weak version: can't see how to do it in one step*)

46953

384 
lemma leadsTo_induct_pre_aux:


385 
"[ F \<in> za leadsTo zb;


386 
P(zb);


387 
!!A B. [ F \<in> A ensures B; P(B); st_set(A); st_set(B) ] ==> P(A);


388 
!!S. [ \<forall>A \<in> S. P(A); \<forall>A \<in> S. st_set(A) ] ==> P(\<Union>(S))

15634

389 
] ==> P(za)"


390 
txt{*by induction on this formula*}

46823

391 
apply (subgoal_tac "P (zb) \<longrightarrow> P (za) ")

15634

392 
txt{*now solve first subgoal: this formula is sufficient*}


393 
apply (blast intro: leadsTo_refl)


394 
apply (erule leadsTo_induct)


395 
apply (blast+)


396 
done


397 


398 

46953

399 
lemma leadsTo_induct_pre:


400 
"[ F \<in> za leadsTo zb;


401 
P(zb);


402 
!!A B. [ F \<in> A ensures B; F \<in> B leadsTo zb; P(B); st_set(A) ] ==> P(A);


403 
!!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P(A) & st_set(A) ==> P(\<Union>(S))

15634

404 
] ==> P(za)"


405 
apply (subgoal_tac " (F \<in> za leadsTo zb) & P (za) ")


406 
apply (erule conjunct2)

46953

407 
apply (frule leadsToD2)

15634

408 
apply (erule leadsTo_induct_pre_aux)


409 
prefer 3 apply (blast dest: leadsToD2 intro: leadsTo_Union)


410 
prefer 2 apply (blast intro: leadsTo_Trans leadsTo_Basis)


411 
apply (blast intro: leadsTo_refl)


412 
done


413 


414 
(** The impossibility law **)

46953

415 
lemma leadsTo_empty:

15634

416 
"F \<in> A leadsTo 0 ==> A=0"


417 
apply (erule leadsTo_induct_pre)


418 
apply (auto simp add: ensures_def constrains_def transient_def st_set_def)


419 
apply (drule bspec, assumption)+


420 
apply blast


421 
done


422 
declare leadsTo_empty [simp]


423 


424 
subsection{*PSP: ProgressSafetyProgress*}


425 


426 
text{*Special case of PSP: Misra's "stable conjunction"*}


427 

46953

428 
lemma psp_stable:

46823

429 
"[ F \<in> A leadsTo A'; F \<in> stable(B) ] ==> F:(A \<inter> B) leadsTo (A' \<inter> B)"

15634

430 
apply (unfold stable_def)

46953

431 
apply (frule leadsToD2)

15634

432 
apply (erule leadsTo_induct)


433 
prefer 3 apply (blast intro: leadsTo_Union_Int)


434 
prefer 2 apply (blast intro: leadsTo_Trans)


435 
apply (rule leadsTo_Basis)


436 
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])


437 
apply (auto intro: transient_strengthen constrains_Int)


438 
done


439 


440 

46823

441 
lemma psp_stable2: "[F \<in> A leadsTo A'; F \<in> stable(B) ]==>F: (B \<inter> A) leadsTo (B \<inter> A')"

15634

442 
apply (simp (no_asm_simp) add: psp_stable Int_ac)


443 
done


444 

46953

445 
lemma psp_ensures:

46823

446 
"[ F \<in> A ensures A'; F \<in> B co B' ]==> F: (A \<inter> B') ensures ((A' \<inter> B) \<union> (B'  B))"

15634

447 
apply (unfold ensures_def constrains_def st_set_def)


448 
(*speeds up the proof*)


449 
apply clarify


450 
apply (blast intro: transient_strengthen)


451 
done


452 

46953

453 
lemma psp:

46823

454 
"[F \<in> A leadsTo A'; F \<in> B co B'; st_set(B')]==> F:(A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B'  B))"

15634

455 
apply (subgoal_tac "F \<in> program & st_set (A) & st_set (A') & st_set (B) ")


456 
prefer 2 apply (blast dest!: constrainsD2 leadsToD2)


457 
apply (erule leadsTo_induct)


458 
prefer 3 apply (blast intro: leadsTo_Union_Int)


459 
txt{*Basis case*}


460 
apply (blast intro: psp_ensures leadsTo_Basis)


461 
txt{*Transitivity case has a delicate argument involving "cancellation"*}


462 
apply (rule leadsTo_Un_duplicate2)


463 
apply (erule leadsTo_cancel_Diff1)


464 
apply (simp add: Int_Diff Diff_triv)


465 
apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)


466 
done


467 


468 

46953

469 
lemma psp2: "[ F \<in> A leadsTo A'; F \<in> B co B'; st_set(B') ]

46823

470 
==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B'  B))"

15634

471 
by (simp (no_asm_simp) add: psp Int_ac)


472 

46953

473 
lemma psp_unless:


474 
"[ F \<in> A leadsTo A'; F \<in> B unless B'; st_set(B); st_set(B') ]

46823

475 
==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')"

15634

476 
apply (unfold unless_def)


477 
apply (subgoal_tac "st_set (A) &st_set (A') ")


478 
prefer 2 apply (blast dest: leadsToD2)


479 
apply (drule psp, assumption, blast)


480 
apply (blast intro: leadsTo_weaken)


481 
done


482 


483 


484 
subsection{*Proving the induction rules*}


485 


486 
(** The most general rule \<in> r is any wf relation; f is any variant function **)

46953

487 
lemma leadsTo_wf_induct_aux: "[ wf(r);


488 
m \<in> I;


489 
field(r)<=I;


490 
F \<in> program; st_set(B);


491 
\<forall>m \<in> I. F \<in> (A \<inter> f``{m}) leadsTo


492 
((A \<inter> f``(converse(r)``{m})) \<union> B) ]

46823

493 
==> F \<in> (A \<inter> f``{m}) leadsTo B"

15634

494 
apply (erule_tac a = m in wf_induct2, simp_all)

46823

495 
apply (subgoal_tac "F \<in> (A \<inter> (f`` (converse (r) ``{x}))) leadsTo B")

15634

496 
apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)


497 
apply (subst vimage_eq_UN)


498 
apply (simp del: UN_simps add: Int_UN_distrib)


499 
apply (auto intro: leadsTo_UN simp del: UN_simps simp add: Int_UN_distrib)


500 
done


501 


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

46953

503 
lemma leadsTo_wf_induct: "[ wf(r);


504 
field(r)<=I;


505 
A<=f``I;


506 
F \<in> program; st_set(A); st_set(B);


507 
\<forall>m \<in> I. F \<in> (A \<inter> f``{m}) leadsTo


508 
((A \<inter> f``(converse(r)``{m})) \<union> B) ]

15634

509 
==> F \<in> A leadsTo B"


510 
apply (rule_tac b = A in subst)


511 
defer 1


512 
apply (rule_tac I = I in leadsTo_UN)

46953

513 
apply (erule_tac I = I in leadsTo_wf_induct_aux, assumption+, best)

15634

514 
done


515 


516 
lemma nat_measure_field: "field(measure(nat, %x. x)) = nat"


517 
apply (unfold field_def)


518 
apply (simp add: measure_def)


519 
apply (rule equalityI, force, clarify)


520 
apply (erule_tac V = "x\<notin>range (?y) " in thin_rl)


521 
apply (erule nat_induct)


522 
apply (rule_tac [2] b = "succ (succ (xa))" in domainI)


523 
apply (rule_tac b = "succ (0) " in domainI)


524 
apply simp_all


525 
done


526 


527 


528 
lemma Image_inverse_lessThan: "k<A ==> measure(A, %x. x) `` {k} = k"


529 
apply (rule equalityI)


530 
apply (auto simp add: measure_def)


531 
apply (blast intro: ltD)


532 
apply (rule vimageI)


533 
prefer 2 apply blast


534 
apply (simp add: lt_Ord lt_Ord2 Ord_mem_iff_lt)


535 
apply (blast intro: lt_trans)


536 
done


537 

46823

538 
(*Alternative proof is via the lemma F \<in> (A \<inter> f`(lessThan m)) leadsTo B*)

46953

539 
lemma lessThan_induct:


540 
"[ A<=f``nat;


541 
F \<in> program; st_set(A); st_set(B);


542 
\<forall>m \<in> nat. F:(A \<inter> f``{m}) leadsTo ((A \<inter> f `` m) \<union> B) ]

15634

543 
==> F \<in> A leadsTo B"

46953

544 
apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN leadsTo_wf_induct])

15634

545 
apply (simp_all add: nat_measure_field)


546 
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])


547 
done


548 


549 


550 
(*** wlt ****)


551 


552 
(*Misra's property W3*)


553 
lemma wlt_type: "wlt(F,B) <=state"


554 
by (unfold wlt_def, auto)


555 


556 
lemma wlt_st_set: "st_set(wlt(F, B))"


557 
apply (unfold st_set_def)


558 
apply (rule wlt_type)


559 
done


560 
declare wlt_st_set [iff]


561 

46823

562 
lemma wlt_leadsTo_iff: "F \<in> wlt(F, B) leadsTo B \<longleftrightarrow> (F \<in> program & st_set(B))"

15634

563 
apply (unfold wlt_def)


564 
apply (blast dest: leadsToD2 intro!: leadsTo_Union)


565 
done


566 


567 
(* [ F \<in> program; st_set(B) ] ==> F \<in> wlt(F, B) leadsTo B *)

45602

568 
lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]]

15634

569 

46823

570 
lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt(F, B)"

15634

571 
apply (unfold wlt_def)


572 
apply (frule leadsToD2)


573 
apply (auto simp add: st_set_def)


574 
done


575 


576 
(*Misra's property W2*)

46823

577 
lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B \<longleftrightarrow> (A \<subseteq> wlt(F,B) & F \<in> program & st_set(B))"

15634

578 
apply auto


579 
apply (blast dest: leadsToD2 leadsTo_subset intro: leadsTo_weaken_L wlt_leadsTo)+


580 
done


581 


582 
(*Misra's property W4*)

46823

583 
lemma wlt_increasing: "[ F \<in> program; st_set(B) ] ==> B \<subseteq> wlt(F,B)"

15634

584 
apply (rule leadsTo_subset)


585 
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [THEN iff_sym] subset_imp_leadsTo)


586 
done


587 


588 
(*Used in the Trans case below*)

46953

589 
lemma leadsTo_123_aux:


590 
"[ B \<subseteq> A2;


591 
F \<in> (A1  B) co (A1 \<union> B);


592 
F \<in> (A2  C) co (A2 \<union> C) ]

46823

593 
==> F \<in> (A1 \<union> A2  C) co (A1 \<union> A2 \<union> C)"

15634

594 
apply (unfold constrains_def st_set_def, blast)


595 
done


596 


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


598 
(* slightly different from the HOL one \<in> B here is bounded *)

46953

599 
lemma leadsTo_123: "F \<in> A leadsTo A'

46823

600 
==> \<exists>B \<in> Pow(state). A<=B & F \<in> B leadsTo A' & F \<in> (BA') co (B \<union> A')"

15634

601 
apply (frule leadsToD2)


602 
apply (erule leadsTo_induct)


603 
txt{*Basis*}


604 
apply (blast dest: ensuresD constrainsD2 st_setD)


605 
txt{*Trans*}


606 
apply clarify

46823

607 
apply (rule_tac x = "Ba \<union> Bb" in bexI)

15634

608 
apply (blast intro: leadsTo_123_aux leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate, blast)


609 
txt{*Union*}


610 
apply (clarify dest!: ball_conj_distrib [THEN iffD1])

46823

611 
apply (subgoal_tac "\<exists>y. y \<in> Pi (S, %A. {Ba \<in> Pow (state) . A<=Ba & F \<in> Ba leadsTo B & F \<in> Ba  B co Ba \<union> B}) ")

15634

612 
defer 1


613 
apply (rule AC_ball_Pi, safe)


614 
apply (rotate_tac 1)

46953

615 
apply (drule_tac x = x in bspec, blast, blast)

15634

616 
apply (rule_tac x = "\<Union>A \<in> S. y`A" in bexI, safe)


617 
apply (rule_tac [3] I1 = S in constrains_UN [THEN constrains_weaken])


618 
apply (rule_tac [2] leadsTo_Union)


619 
prefer 5 apply (blast dest!: apply_type, simp_all)


620 
apply (force dest!: apply_type)+


621 
done


622 


623 


624 
(*Misra's property W5*)


625 
lemma wlt_constrains_wlt: "[ F \<in> program; st_set(B) ] ==>F \<in> (wlt(F, B)  B) co (wlt(F,B))"


626 
apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], assumption, blast)


627 
apply clarify


628 
apply (subgoal_tac "Ba = wlt (F,B) ")


629 
prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify)


630 
apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]])


631 
done


632 


633 


634 
subsection{*Completion: Binary and General Finite versions*}


635 

46953

636 
lemma completion_aux: "[ W = wlt(F, (B' \<union> C));


637 
F \<in> A leadsTo (A' \<union> C); F \<in> A' co (A' \<union> C);


638 
F \<in> B leadsTo (B' \<union> C); F \<in> B' co (B' \<union> C) ]

46823

639 
==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)"

15634

640 
apply (subgoal_tac "st_set (C) &st_set (W) &st_set (WC) &st_set (A') &st_set (A) & st_set (B) & st_set (B') & F \<in> program")

46953

641 
prefer 2


642 
apply simp

15634

643 
apply (blast dest!: leadsToD2)

46823

644 
apply (subgoal_tac "F \<in> (WC) co (W \<union> B' \<union> C) ")

15634

645 
prefer 2


646 
apply (blast intro!: constrains_weaken [OF constrains_Un [OF _ wlt_constrains_wlt]])


647 
apply (subgoal_tac "F \<in> (WC) co W")


648 
prefer 2


649 
apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]] Un_assoc)

46823

650 
apply (subgoal_tac "F \<in> (A \<inter> W  C) leadsTo (A' \<inter> W \<union> C) ")

15634

651 
prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])


652 
(** step 13 **)

46823

653 
apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ")

15634

654 
apply (drule leadsTo_Diff)


655 
apply (blast intro: subset_imp_leadsTo dest: leadsToD2 constrainsD2)


656 
apply (force simp add: st_set_def)

46823

657 
apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W")

15634

658 
prefer 2 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])


659 
apply (blast intro: leadsTo_Trans subset_imp_leadsTo)


660 
txt{*last subgoal*}


661 
apply (rule_tac leadsTo_Un_duplicate2)


662 
apply (rule_tac leadsTo_Un_Un)


663 
prefer 2 apply (blast intro: leadsTo_refl)

46823

664 
apply (rule_tac A'1 = "B' \<union> C" in wlt_leadsTo[THEN psp2, THEN leadsTo_weaken])

15634

665 
apply blast+


666 
done


667 

45602

668 
lemmas completion = refl [THEN completion_aux]

15634

669 


670 
lemma finite_completion_aux:

46953

671 
"[ I \<in> Fin(X); F \<in> program; st_set(C) ] ==>


672 
(\<forall>i \<in> I. F \<in> (A(i)) leadsTo (A'(i) \<union> C)) \<longrightarrow>


673 
(\<forall>i \<in> I. F \<in> (A'(i)) co (A'(i) \<union> C)) \<longrightarrow>

46823

674 
F \<in> (\<Inter>i \<in> I. A(i)) leadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"

15634

675 
apply (erule Fin_induct)


676 
apply (auto simp add: Inter_0)


677 
apply (rule completion)


678 
apply (auto simp del: INT_simps simp add: INT_extend_simps)


679 
apply (blast intro: constrains_INT)


680 
done


681 

46953

682 
lemma finite_completion:


683 
"[ I \<in> Fin(X);


684 
!!i. i \<in> I ==> F \<in> A(i) leadsTo (A'(i) \<union> C);


685 
!!i. i \<in> I ==> F \<in> A'(i) co (A'(i) \<union> C); F \<in> program; st_set(C)]

46823

686 
==> F \<in> (\<Inter>i \<in> I. A(i)) leadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"

15634

687 
by (blast intro: finite_completion_aux [THEN mp, THEN mp])


688 

46953

689 
lemma stable_completion:


690 
"[ F \<in> A leadsTo A'; F \<in> stable(A');


691 
F \<in> B leadsTo B'; F \<in> stable(B') ]

46823

692 
==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')"

15634

693 
apply (unfold stable_def)


694 
apply (rule_tac C1 = 0 in completion [THEN leadsTo_weaken_R], simp+)


695 
apply (blast dest: leadsToD2)


696 
done


697 


698 

46953

699 
lemma finite_stable_completion:


700 
"[ I \<in> Fin(X);


701 
(!!i. i \<in> I ==> F \<in> A(i) leadsTo A'(i));


702 
(!!i. i \<in> I ==> F \<in> stable(A'(i))); F \<in> program ]

15634

703 
==> F \<in> (\<Inter>i \<in> I. A(i)) leadsTo (\<Inter>i \<in> I. A'(i))"


704 
apply (unfold stable_def)


705 
apply (subgoal_tac "st_set (\<Inter>i \<in> I. A' (i))")


706 
prefer 2 apply (blast dest: leadsToD2)

46953

707 
apply (rule_tac C1 = 0 in finite_completion [THEN leadsTo_weaken_R], auto)

15634

708 
done


709 

11479

710 
end
