1(* Title: HOL/UNITY/SubstAx.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5Weak LeadsTo relation (restricted to the set of reachable states) 6*) 7 8section\<open>Weak Progress\<close> 9 10theory SubstAx imports WFair Constrains begin 11 12definition Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) where 13 "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}" 14 15definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where 16 "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}" 17 18notation LeadsTo (infixl "\<longmapsto>w" 60) 19 20 21text\<open>Resembles the previous definition of LeadsTo\<close> 22lemma LeadsTo_eq_leadsTo: 23 "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}" 24apply (unfold LeadsTo_def) 25apply (blast dest: psp_stable2 intro: leadsTo_weaken) 26done 27 28 29subsection\<open>Specialized laws for handling invariants\<close> 30 31(** Conjoining an Always property **) 32 33lemma Always_LeadsTo_pre: 34 "F \<in> Always INV ==> (F \<in> (INV \<inter> A) LeadsTo A') = (F \<in> A LeadsTo A')" 35by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 36 Int_assoc [symmetric]) 37 38lemma Always_LeadsTo_post: 39 "F \<in> Always INV ==> (F \<in> A LeadsTo (INV \<inter> A')) = (F \<in> A LeadsTo A')" 40by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 41 Int_assoc [symmetric]) 42 43(* [| F \<in> Always C; F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *) 44lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1] 45 46(* [| F \<in> Always INV; F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *) 47lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2] 48 49 50subsection\<open>Introduction rules: Basis, Trans, Union\<close> 51 52lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B" 53apply (simp add: LeadsTo_def) 54apply (blast intro: leadsTo_weaken_L) 55done 56 57lemma LeadsTo_Trans: 58 "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C" 59apply (simp add: LeadsTo_eq_leadsTo) 60apply (blast intro: leadsTo_Trans) 61done 62 63lemma LeadsTo_Union: 64 "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (\<Union>S) LeadsTo B" 65apply (simp add: LeadsTo_def) 66apply (subst Int_Union) 67apply (blast intro: leadsTo_UN) 68done 69 70 71subsection\<open>Derived rules\<close> 72 73lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV" 74by (simp add: LeadsTo_def) 75 76text\<open>Useful with cancellation, disjunction\<close> 77lemma LeadsTo_Un_duplicate: 78 "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'" 79by (simp add: Un_ac) 80 81lemma LeadsTo_Un_duplicate2: 82 "F \<in> A LeadsTo (A' \<union> C \<union> C) ==> F \<in> A LeadsTo (A' \<union> C)" 83by (simp add: Un_ac) 84 85lemma LeadsTo_UN: 86 "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B" 87apply (blast intro: LeadsTo_Union) 88done 89 90text\<open>Binary union introduction rule\<close> 91lemma LeadsTo_Un: 92 "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C" 93 using LeadsTo_UN [of "{A, B}" F id C] by auto 94 95text\<open>Lets us look at the starting state\<close> 96lemma single_LeadsTo_I: 97 "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B" 98by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast) 99 100lemma subset_imp_LeadsTo: "A \<subseteq> B ==> F \<in> A LeadsTo B" 101apply (simp add: LeadsTo_def) 102apply (blast intro: subset_imp_leadsTo) 103done 104 105lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, simp] 106 107lemma LeadsTo_weaken_R: 108 "[| F \<in> A LeadsTo A'; A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'" 109apply (simp add: LeadsTo_def) 110apply (blast intro: leadsTo_weaken_R) 111done 112 113lemma LeadsTo_weaken_L: 114 "[| F \<in> A LeadsTo A'; B \<subseteq> A |] 115 ==> F \<in> B LeadsTo A'" 116apply (simp add: LeadsTo_def) 117apply (blast intro: leadsTo_weaken_L) 118done 119 120lemma LeadsTo_weaken: 121 "[| F \<in> A LeadsTo A'; 122 B \<subseteq> A; A' \<subseteq> B' |] 123 ==> F \<in> B LeadsTo B'" 124by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans) 125 126lemma Always_LeadsTo_weaken: 127 "[| F \<in> Always C; F \<in> A LeadsTo A'; 128 C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |] 129 ==> F \<in> B LeadsTo B'" 130by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD) 131 132(** Two theorems for "proof lattices" **) 133 134lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F \<in> (A \<union> B) LeadsTo B" 135by (blast intro: LeadsTo_Un subset_imp_LeadsTo) 136 137lemma LeadsTo_Trans_Un: 138 "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |] 139 ==> F \<in> (A \<union> B) LeadsTo C" 140by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans) 141 142 143(** Distributive laws **) 144 145lemma LeadsTo_Un_distrib: 146 "(F \<in> (A \<union> B) LeadsTo C) = (F \<in> A LeadsTo C & F \<in> B LeadsTo C)" 147by (blast intro: LeadsTo_Un LeadsTo_weaken_L) 148 149lemma LeadsTo_UN_distrib: 150 "(F \<in> (\<Union>i \<in> I. A i) LeadsTo B) = (\<forall>i \<in> I. F \<in> (A i) LeadsTo B)" 151by (blast intro: LeadsTo_UN LeadsTo_weaken_L) 152 153lemma LeadsTo_Union_distrib: 154 "(F \<in> (\<Union>S) LeadsTo B) = (\<forall>A \<in> S. F \<in> A LeadsTo B)" 155by (blast intro: LeadsTo_Union LeadsTo_weaken_L) 156 157 158(** More rules using the premise "Always INV" **) 159 160lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B" 161by (simp add: Ensures_def LeadsTo_def leadsTo_Basis) 162 163lemma EnsuresI: 164 "[| F \<in> (A-B) Co (A \<union> B); F \<in> transient (A-B) |] 165 ==> F \<in> A Ensures B" 166apply (simp add: Ensures_def Constrains_eq_constrains) 167apply (blast intro: ensuresI constrains_weaken transient_strengthen) 168done 169 170lemma Always_LeadsTo_Basis: 171 "[| F \<in> Always INV; 172 F \<in> (INV \<inter> (A-A')) Co (A \<union> A'); 173 F \<in> transient (INV \<inter> (A-A')) |] 174 ==> F \<in> A LeadsTo A'" 175apply (rule Always_LeadsToI, assumption) 176apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen) 177done 178 179text\<open>Set difference: maybe combine with \<open>leadsTo_weaken_L\<close>?? 180 This is the most useful form of the "disjunction" rule\<close> 181lemma LeadsTo_Diff: 182 "[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |] 183 ==> F \<in> A LeadsTo C" 184by (blast intro: LeadsTo_Un LeadsTo_weaken) 185 186 187lemma LeadsTo_UN_UN: 188 "(!! i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i)) 189 ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo (\<Union>i \<in> I. A' i)" 190apply (blast intro: LeadsTo_Union LeadsTo_weaken_R) 191done 192 193 194text\<open>Version with no index set\<close> 195lemma LeadsTo_UN_UN_noindex: 196 "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" 197by (blast intro: LeadsTo_UN_UN) 198 199text\<open>Version with no index set\<close> 200lemma all_LeadsTo_UN_UN: 201 "\<forall>i. F \<in> (A i) LeadsTo (A' i) 202 ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" 203by (blast intro: LeadsTo_UN_UN) 204 205text\<open>Binary union version\<close> 206lemma LeadsTo_Un_Un: 207 "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] 208 ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')" 209by (blast intro: LeadsTo_Un LeadsTo_weaken_R) 210 211 212(** The cancellation law **) 213 214lemma LeadsTo_cancel2: 215 "[| F \<in> A LeadsTo (A' \<union> B); F \<in> B LeadsTo B' |] 216 ==> F \<in> A LeadsTo (A' \<union> B')" 217by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans) 218 219lemma LeadsTo_cancel_Diff2: 220 "[| F \<in> A LeadsTo (A' \<union> B); F \<in> (B-A') LeadsTo B' |] 221 ==> F \<in> A LeadsTo (A' \<union> B')" 222apply (rule LeadsTo_cancel2) 223prefer 2 apply assumption 224apply (simp_all (no_asm_simp)) 225done 226 227lemma LeadsTo_cancel1: 228 "[| F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' |] 229 ==> F \<in> A LeadsTo (B' \<union> A')" 230apply (simp add: Un_commute) 231apply (blast intro!: LeadsTo_cancel2) 232done 233 234lemma LeadsTo_cancel_Diff1: 235 "[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |] 236 ==> F \<in> A LeadsTo (B' \<union> A')" 237apply (rule LeadsTo_cancel1) 238prefer 2 apply assumption 239apply (simp_all (no_asm_simp)) 240done 241 242 243text\<open>The impossibility law\<close> 244 245text\<open>The set "A" may be non-empty, but it contains no reachable states\<close> 246lemma LeadsTo_empty: "[|F \<in> A LeadsTo {}; all_total F|] ==> F \<in> Always (-A)" 247apply (simp add: LeadsTo_def Always_eq_includes_reachable) 248apply (drule leadsTo_empty, auto) 249done 250 251 252subsection\<open>PSP: Progress-Safety-Progress\<close> 253 254text\<open>Special case of PSP: Misra's "stable conjunction"\<close> 255lemma PSP_Stable: 256 "[| F \<in> A LeadsTo A'; F \<in> Stable B |] 257 ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)" 258apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable) 259apply (drule psp_stable, assumption) 260apply (simp add: Int_ac) 261done 262 263lemma PSP_Stable2: 264 "[| F \<in> A LeadsTo A'; F \<in> Stable B |] 265 ==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')" 266by (simp add: PSP_Stable Int_ac) 267 268lemma PSP: 269 "[| F \<in> A LeadsTo A'; F \<in> B Co B' |] 270 ==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))" 271apply (simp add: LeadsTo_def Constrains_eq_constrains) 272apply (blast dest: psp intro: leadsTo_weaken) 273done 274 275lemma PSP2: 276 "[| F \<in> A LeadsTo A'; F \<in> B Co B' |] 277 ==> F \<in> (B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))" 278by (simp add: PSP Int_ac) 279 280lemma PSP_Unless: 281 "[| F \<in> A LeadsTo A'; F \<in> B Unless B' |] 282 ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')" 283apply (unfold Unless_def) 284apply (drule PSP, assumption) 285apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo) 286done 287 288 289lemma Stable_transient_Always_LeadsTo: 290 "[| F \<in> Stable A; F \<in> transient C; 291 F \<in> Always (-A \<union> B \<union> C) |] ==> F \<in> A LeadsTo B" 292apply (erule Always_LeadsTo_weaken) 293apply (rule LeadsTo_Diff) 294 prefer 2 295 apply (erule 296 transient_imp_leadsTo [THEN leadsTo_imp_LeadsTo, THEN PSP_Stable2]) 297 apply (blast intro: subset_imp_LeadsTo)+ 298done 299 300 301subsection\<open>Induction rules\<close> 302 303(** Meta or object quantifier ????? **) 304lemma LeadsTo_wf_induct: 305 "[| wf r; 306 \<forall>m. F \<in> (A \<inter> f-`{m}) LeadsTo 307 ((A \<inter> f-`(r\<inverse> `` {m})) \<union> B) |] 308 ==> F \<in> A LeadsTo B" 309apply (simp add: LeadsTo_eq_leadsTo) 310apply (erule leadsTo_wf_induct) 311apply (blast intro: leadsTo_weaken) 312done 313 314 315lemma Bounded_induct: 316 "[| wf r; 317 \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) LeadsTo 318 ((A \<inter> f-`(r\<inverse> `` {m})) \<union> B) |] 319 ==> F \<in> A LeadsTo ((A - (f-`I)) \<union> B)" 320apply (erule LeadsTo_wf_induct, safe) 321apply (case_tac "m \<in> I") 322apply (blast intro: LeadsTo_weaken) 323apply (blast intro: subset_imp_LeadsTo) 324done 325 326 327lemma LessThan_induct: 328 "(!!m::nat. F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B)) 329 ==> F \<in> A LeadsTo B" 330by (rule wf_less_than [THEN LeadsTo_wf_induct], auto) 331 332text\<open>Integer version. Could generalize from 0 to any lower bound\<close> 333lemma integ_0_le_induct: 334 "[| F \<in> Always {s. (0::int) \<le> f s}; 335 !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo 336 ((A \<inter> {s. f s < z}) \<union> B) |] 337 ==> F \<in> A LeadsTo B" 338apply (rule_tac f = "nat o f" in LessThan_induct) 339apply (simp add: vimage_def) 340apply (rule Always_LeadsTo_weaken, assumption+) 341apply (auto simp add: nat_eq_iff nat_less_iff) 342done 343 344lemma LessThan_bounded_induct: 345 "!!l::nat. \<forall>m \<in> greaterThan l. 346 F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B) 347 ==> F \<in> A LeadsTo ((A \<inter> (f-`(atMost l))) \<union> B)" 348apply (simp only: Diff_eq [symmetric] vimage_Compl 349 Compl_greaterThan [symmetric]) 350apply (rule wf_less_than [THEN Bounded_induct], simp) 351done 352 353lemma GreaterThan_bounded_induct: 354 "!!l::nat. \<forall>m \<in> lessThan l. 355 F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(greaterThan m)) \<union> B) 356 ==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)" 357apply (rule_tac f = f and f1 = "%k. l - k" 358 in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct]) 359apply (simp add: Image_singleton, clarify) 360apply (case_tac "m<l") 361 apply (blast intro: LeadsTo_weaken_R diff_less_mono2) 362apply (blast intro: not_le_imp_less subset_imp_LeadsTo) 363done 364 365 366subsection\<open>Completion: Binary and General Finite versions\<close> 367 368lemma Completion: 369 "[| F \<in> A LeadsTo (A' \<union> C); F \<in> A' Co (A' \<union> C); 370 F \<in> B LeadsTo (B' \<union> C); F \<in> B' Co (B' \<union> C) |] 371 ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)" 372apply (simp add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib) 373apply (blast intro: completion leadsTo_weaken) 374done 375 376lemma Finite_completion_lemma: 377 "finite I 378 ==> (\<forall>i \<in> I. F \<in> (A i) LeadsTo (A' i \<union> C)) --> 379 (\<forall>i \<in> I. F \<in> (A' i) Co (A' i \<union> C)) --> 380 F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" 381apply (erule finite_induct, auto) 382apply (rule Completion) 383 prefer 4 384 apply (simp only: INT_simps [symmetric]) 385 apply (rule Constrains_INT, auto) 386done 387 388lemma Finite_completion: 389 "[| finite I; 390 !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i \<union> C); 391 !!i. i \<in> I ==> F \<in> (A' i) Co (A' i \<union> C) |] 392 ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" 393by (blast intro: Finite_completion_lemma [THEN mp, THEN mp]) 394 395lemma Stable_completion: 396 "[| F \<in> A LeadsTo A'; F \<in> Stable A'; 397 F \<in> B LeadsTo B'; F \<in> Stable B' |] 398 ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')" 399apply (unfold Stable_def) 400apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R]) 401apply (force+) 402done 403 404lemma Finite_stable_completion: 405 "[| finite I; 406 !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i); 407 !!i. i \<in> I ==> F \<in> Stable (A' i) |] 408 ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo (\<Inter>i \<in> I. A' i)" 409apply (unfold Stable_def) 410apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R]) 411apply (simp_all, blast+) 412done 413 414end 415