1(* Title: HOL/UNITY/Transformers.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 2003 University of Cambridge 4 5Predicate Transformers. From 6 7 David Meier and Beverly Sanders, 8 Composing Leads-to Properties 9 Theoretical Computer Science 243:1-2 (2000), 339-361. 10 11 David Meier, 12 Progress Properties in Program Refinement and Parallel Composition 13 Swiss Federal Institute of Technology Zurich (1997) 14*) 15 16section\<open>Predicate Transformers\<close> 17 18theory Transformers imports Comp begin 19 20subsection\<open>Defining the Predicate Transformers @{term wp}, 21 @{term awp} and @{term wens}\<close> 22 23definition wp :: "[('a*'a) set, 'a set] => 'a set" where 24 \<comment> \<open>Dijkstra's weakest-precondition operator (for an individual command)\<close> 25 "wp act B == - (act\<inverse> `` (-B))" 26 27definition awp :: "['a program, 'a set] => 'a set" where 28 \<comment> \<open>Dijkstra's weakest-precondition operator (for a program)\<close> 29 "awp F B == (\<Inter>act \<in> Acts F. wp act B)" 30 31definition wens :: "['a program, ('a*'a) set, 'a set] => 'a set" where 32 \<comment> \<open>The weakest-ensures transformer\<close> 33 "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)" 34 35text\<open>The fundamental theorem for wp\<close> 36theorem wp_iff: "(A <= wp act B) = (act `` A <= B)" 37by (force simp add: wp_def) 38 39text\<open>This lemma is a good deal more intuitive than the definition!\<close> 40lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act --> x \<in> B)" 41by (simp add: wp_def, blast) 42 43lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B" 44by (force simp add: wp_def) 45 46lemma wp_empty [simp]: "wp act {} = - (Domain act)" 47by (force simp add: wp_def) 48 49text\<open>The identity relation is the skip action\<close> 50lemma wp_Id [simp]: "wp Id B = B" 51by (simp add: wp_def) 52 53lemma wp_totalize_act: 54 "wp (totalize_act act) B = (wp act B \<inter> Domain act) \<union> (B - Domain act)" 55by (simp add: wp_def totalize_act_def, blast) 56 57lemma awp_subset: "(awp F A \<subseteq> A)" 58by (force simp add: awp_def wp_def) 59 60lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B" 61by (simp add: awp_def wp_def, blast) 62 63text\<open>The fundamental theorem for awp\<close> 64theorem awp_iff_constrains: "(A <= awp F B) = (F \<in> A co B)" 65by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 66 67lemma awp_iff_stable: "(A \<subseteq> awp F A) = (F \<in> stable A)" 68by (simp add: awp_iff_constrains stable_def) 69 70lemma stable_imp_awp_ident: "F \<in> stable A ==> awp F A = A" 71apply (rule equalityI [OF awp_subset]) 72apply (simp add: awp_iff_stable) 73done 74 75lemma wp_mono: "(A \<subseteq> B) ==> wp act A \<subseteq> wp act B" 76by (simp add: wp_def, blast) 77 78lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B" 79by (simp add: awp_def wp_def, blast) 80 81lemma wens_unfold: 82 "wens F act B = (wp act B \<inter> awp F (B \<union> wens F act B)) \<union> B" 83apply (simp add: wens_def) 84apply (rule gfp_unfold) 85apply (simp add: mono_def wp_def awp_def, blast) 86done 87 88lemma wens_Id [simp]: "wens F Id B = B" 89by (simp add: wens_def gfp_def wp_def awp_def, blast) 90 91text\<open>These two theorems justify the claim that @{term wens} returns the 92weakest assertion satisfying the ensures property\<close> 93lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B" 94apply (simp add: wens_def ensures_def transient_def, clarify) 95apply (rule rev_bexI, assumption) 96apply (rule gfp_upperbound) 97apply (simp add: constrains_def awp_def wp_def, blast) 98done 99 100lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B" 101by (simp add: wens_def gfp_def constrains_def awp_def wp_def 102 ensures_def transient_def, blast) 103 104text\<open>These two results constitute assertion (4.13) of the thesis\<close> 105lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B" 106apply (simp add: wens_def wp_def awp_def) 107apply (rule gfp_mono, blast) 108done 109 110lemma wens_weakening: "B \<subseteq> wens F act B" 111by (simp add: wens_def gfp_def, blast) 112 113text\<open>Assertion (6), or 4.16 in the thesis\<close> 114lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 115apply (simp add: wens_def wp_def awp_def) 116apply (rule gfp_upperbound, blast) 117done 118 119text\<open>Assertion 4.17 in the thesis\<close> 120lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 121by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast) 122 \<comment> \<open>Proved instantly, yet remarkably fragile. If \<open>Un_subset_iff\<close> 123 is declared as an iff-rule, then it's almost impossible to prove. 124 One proof is via \<open>meson\<close> after expanding all definitions, but it's 125 slow!\<close> 126 127text\<open>Assertion (7): 4.18 in the thesis. NOTE that many of these results 128hold for an arbitrary action. We often do not require @{term "act \<in> Acts F"}\<close> 129lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)" 130apply (simp add: stable_def) 131apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 132apply (simp add: Un_Int_distrib2 Compl_partition2) 133apply (erule constrains_weaken, blast) 134apply (simp add: wens_weakening) 135done 136 137text\<open>Assertion 4.20 in the thesis.\<close> 138lemma wens_Int_eq_lemma: 139 "[|T-B \<subseteq> awp F T; act \<in> Acts F|] 140 ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)" 141apply (rule subset_wens) 142apply (rule_tac P="\<lambda>x. f x \<subseteq> b" for f b in ssubst [OF wens_unfold]) 143apply (simp add: wp_def awp_def, blast) 144done 145 146text\<open>Assertion (8): 4.21 in the thesis. Here we indeed require 147 @{term "act \<in> Acts F"}\<close> 148lemma wens_Int_eq: 149 "[|T-B \<subseteq> awp F T; act \<in> Acts F|] 150 ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)" 151apply (rule equalityI) 152 apply (simp_all add: Int_lower1) 153 apply (rule wens_Int_eq_lemma, assumption+) 154apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 155done 156 157 158subsection\<open>Defining the Weakest Ensures Set\<close> 159 160inductive_set 161 wens_set :: "['a program, 'a set] => 'a set set" 162 for F :: "'a program" and B :: "'a set" 163where 164 165 Basis: "B \<in> wens_set F B" 166 167| Wens: "[|X \<in> wens_set F B; act \<in> Acts F|] ==> wens F act X \<in> wens_set F B" 168 169| Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B" 170 171lemma wens_set_imp_co: "A \<in> wens_set F B ==> F \<in> (A-B) co A" 172apply (erule wens_set.induct) 173 apply (simp add: constrains_def) 174 apply (drule_tac act1=act and A1=X 175 in constrains_Un [OF Diff_wens_constrains]) 176 apply (erule constrains_weaken, blast) 177 apply (simp add: wens_weakening) 178apply (rule constrains_weaken) 179apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+) 180done 181 182lemma wens_set_imp_leadsTo: "A \<in> wens_set F B ==> F \<in> A leadsTo B" 183apply (erule wens_set.induct) 184 apply (rule leadsTo_refl) 185 apply (blast intro: wens_ensures leadsTo_Trans) 186apply (blast intro: leadsTo_Union) 187done 188 189lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C" 190apply (erule leadsTo_induct_pre) 191 apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens) 192 apply (clarify, drule ensures_weaken_R, assumption) 193 apply (blast dest!: ensures_imp_wens intro: wens_set.Wens) 194apply (case_tac "S={}") 195 apply (simp, blast intro: wens_set.Basis) 196apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def) 197apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>S. Z = f U}" in exI) 198apply (blast intro: wens_set.Union) 199done 200 201text\<open>Assertion (9): 4.27 in the thesis.\<close> 202lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)" 203by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 204 205text\<open>This is the result that requires the definition of @{term wens_set} to 206 require @{term W} to be non-empty in the Unio case, for otherwise we should 207 always have @{term "{} \<in> wens_set F B"}.\<close> 208lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A" 209apply (erule wens_set.induct) 210 apply (blast intro: wens_weakening [THEN subsetD])+ 211done 212 213 214subsection\<open>Properties Involving Program Union\<close> 215 216text\<open>Assertion (4.30) of thesis, reoriented\<close> 217lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B" 218by (simp add: awp_def wp_def, blast) 219 220lemma wens_subset: "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)" 221by (subst wens_unfold, fast) 222 223text\<open>Assertion (4.31)\<close> 224lemma subset_wens_Join: 225 "[|A = T \<inter> wens F act B; T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|] 226 ==> A \<subseteq> wens (F\<squnion>G) act B" 227apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 228 wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 229 apply (rule subset_wens) 230 apply (simp add: awp_Join_eq awp_Int_eq Un_commute) 231 apply (simp add: awp_def wp_def, blast) 232apply (insert wens_subset [of F act B], blast) 233done 234 235text\<open>Assertion (4.32)\<close> 236lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B" 237apply (simp add: wens_def) 238apply (rule gfp_mono) 239apply (auto simp add: awp_Join_eq) 240done 241 242text\<open>Lemma, because the inductive step is just too messy.\<close> 243lemma wens_Union_inductive_step: 244 assumes awpF: "T-B \<subseteq> awp F T" 245 and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)" 246 shows "[|X \<in> wens_set F B; act \<in> Acts F; Y \<subseteq> X; T\<inter>X = T\<inter>Y|] 247 ==> wens (F\<squnion>G) act Y \<subseteq> wens F act X \<and> 248 T \<inter> wens F act X = T \<inter> wens (F\<squnion>G) act Y" 249apply (subgoal_tac "wens (F\<squnion>G) act Y \<subseteq> wens F act X") 250 prefer 2 251 apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp) 252apply (rule equalityI) 253 prefer 2 apply blast 254apply (simp add: Int_lower1) 255apply (frule wens_set_imp_subset) 256apply (subgoal_tac "T-X \<subseteq> awp F T") 257 prefer 2 apply (blast intro: awpF [THEN subsetD]) 258apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans) 259 prefer 2 apply (blast intro!: wens_mono) 260apply (subst wens_Int_eq, assumption+) 261apply (rule subset_wens_Join [of _ T], simp, blast) 262apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X") 263 prefer 2 264 apply (subst wens_Int_eq [symmetric], assumption+) 265 apply (blast intro: wens_weakening [THEN subsetD], simp) 266apply (blast intro: awpG [THEN subsetD] wens_set.Wens) 267done 268 269theorem wens_Union: 270 assumes awpF: "T-B \<subseteq> awp F T" 271 and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)" 272 and major: "X \<in> wens_set F B" 273 shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y" 274apply (rule wens_set.induct [OF major]) 275 txt\<open>Basis: trivial\<close> 276 apply (blast intro: wens_set.Basis) 277 txt\<open>Inductive step\<close> 278 apply clarify 279 apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI) 280 apply (force intro: wens_set.Wens) 281 apply (simp add: wens_Union_inductive_step [OF awpF awpG]) 282txt\<open>Union: by Axiom of Choice\<close> 283apply (simp add: ball_conj_distrib Bex_def) 284apply (clarify dest!: bchoice) 285apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI) 286apply (blast intro: wens_set.Union) 287done 288 289theorem leadsTo_Join: 290 assumes leadsTo: "F \<in> A leadsTo B" 291 and awpF: "T-B \<subseteq> awp F T" 292 and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)" 293 shows "F\<squnion>G \<in> T\<inter>A leadsTo B" 294apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) 295apply (rule wens_Union [THEN bexE]) 296 apply (rule awpF) 297 apply (erule awpG, assumption) 298apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L]) 299done 300 301 302subsection \<open>The Set @{term "wens_set F B"} for a Single-Assignment Program\<close> 303text\<open>Thesis Section 4.3.3\<close> 304 305text\<open>We start by proving laws about single-assignment programs\<close> 306lemma awp_single_eq [simp]: 307 "awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B" 308by (force simp add: awp_def wp_def) 309 310lemma wp_Un_subset: "wp act A \<union> wp act B \<subseteq> wp act (A \<union> B)" 311by (force simp add: wp_def) 312 313lemma wp_Un_eq: "single_valued act ==> wp act (A \<union> B) = wp act A \<union> wp act B" 314apply (rule equalityI) 315 apply (force simp add: wp_def single_valued_def) 316apply (rule wp_Un_subset) 317done 318 319lemma wp_UN_subset: "(\<Union>i\<in>I. wp act (A i)) \<subseteq> wp act (\<Union>i\<in>I. A i)" 320by (force simp add: wp_def) 321 322lemma wp_UN_eq: 323 "[|single_valued act; I\<noteq>{}|] 324 ==> wp act (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. wp act (A i))" 325apply (rule equalityI) 326 prefer 2 apply (rule wp_UN_subset) 327 apply (simp add: wp_def Image_INT_eq) 328done 329 330lemma wens_single_eq: 331 "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B" 332by (simp add: wens_def gfp_def wp_def, blast) 333 334 335text\<open>Next, we express the @{term "wens_set"} for single-assignment programs\<close> 336 337definition wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set" where 338 "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ i) B" 339 340definition wens_single :: "[('a*'a) set, 'a set] => 'a set" where 341 "wens_single act B == \<Union>i. (wp act ^^ i) B" 342 343lemma wens_single_Un_eq: 344 "single_valued act 345 ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B" 346apply (rule equalityI) 347 apply (simp_all add: Un_upper1) 348apply (simp add: wens_single_def wp_UN_eq, clarify) 349apply (rule_tac a="Suc xa" in UN_I, auto) 350done 351 352lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}" 353by force 354 355lemma wens_single_finite_0 [simp]: "wens_single_finite act B 0 = B" 356by (simp add: wens_single_finite_def) 357 358lemma wens_single_finite_Suc: 359 "single_valued act 360 ==> wens_single_finite act B (Suc k) = 361 wens_single_finite act B k \<union> wp act (wens_single_finite act B k)" 362apply (simp add: wens_single_finite_def image_def 363 wp_UN_eq [OF _ atMost_nat_nonempty]) 364apply (force elim!: le_SucE) 365done 366 367lemma wens_single_finite_Suc_eq_wens: 368 "single_valued act 369 ==> wens_single_finite act B (Suc k) = 370 wens (mk_program (init, {act}, allowed)) act 371 (wens_single_finite act B k)" 372by (simp add: wens_single_finite_Suc wens_single_eq) 373 374lemma def_wens_single_finite_Suc_eq_wens: 375 "[|F = mk_program (init, {act}, allowed); single_valued act|] 376 ==> wens_single_finite act B (Suc k) = 377 wens F act (wens_single_finite act B k)" 378by (simp add: wens_single_finite_Suc_eq_wens) 379 380lemma wens_single_finite_Un_eq: 381 "single_valued act 382 ==> wens_single_finite act B k \<union> wp act (wens_single_finite act B k) 383 \<in> range (wens_single_finite act B)" 384by (simp add: wens_single_finite_Suc [symmetric]) 385 386lemma wens_single_eq_Union: 387 "wens_single act B = \<Union>range (wens_single_finite act B)" 388by (simp add: wens_single_finite_def wens_single_def, blast) 389 390lemma wens_single_finite_eq_Union: 391 "wens_single_finite act B n = (\<Union>k\<in>atMost n. wens_single_finite act B k)" 392apply (auto simp add: wens_single_finite_def) 393apply (blast intro: le_trans) 394done 395 396lemma wens_single_finite_mono: 397 "m \<le> n ==> wens_single_finite act B m \<subseteq> wens_single_finite act B n" 398by (force simp add: wens_single_finite_eq_Union [of act B n]) 399 400lemma wens_single_finite_subset_wens_single: 401 "wens_single_finite act B k \<subseteq> wens_single act B" 402by (simp add: wens_single_eq_Union, blast) 403 404lemma subset_wens_single_finite: 405 "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|] 406 ==> \<exists>m. \<Union>W = wens_single_finite act B m" 407apply (induct k) 408 apply (rule_tac x=0 in exI, simp, blast) 409apply (auto simp add: atMost_Suc) 410apply (case_tac "wens_single_finite act B (Suc k) \<in> W") 411 prefer 2 apply blast 412apply (drule_tac x="Suc k" in spec) 413apply (erule notE, rule equalityI) 414 prefer 2 apply blast 415apply (subst wens_single_finite_eq_Union) 416apply (simp add: atMost_Suc, blast) 417done 418 419text\<open>lemma for Union case\<close> 420lemma Union_eq_wens_single: 421 "\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k}; 422 W \<subseteq> insert (wens_single act B) 423 (range (wens_single_finite act B))\<rbrakk> 424 \<Longrightarrow> \<Union>W = wens_single act B" 425apply (cases "wens_single act B \<in> W") 426 apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 427apply (simp add: wens_single_eq_Union) 428apply (rule equalityI, blast) 429apply (simp add: UN_subset_iff, clarify) 430apply (subgoal_tac "\<exists>y\<in>W. \<exists>n. y = wens_single_finite act B n & i\<le>n") 431 apply (blast intro: wens_single_finite_mono [THEN subsetD]) 432apply (drule_tac x=i in spec) 433apply (force simp add: atMost_def) 434done 435 436lemma wens_set_subset_single: 437 "single_valued act 438 ==> wens_set (mk_program (init, {act}, allowed)) B \<subseteq> 439 insert (wens_single act B) (range (wens_single_finite act B))" 440apply (rule subsetI) 441apply (erule wens_set.induct) 442 txt\<open>Basis\<close> 443 apply (fastforce simp add: wens_single_finite_def) 444 txt\<open>Wens inductive step\<close> 445 apply (case_tac "acta = Id", simp) 446 apply (simp add: wens_single_eq) 447 apply (elim disjE) 448 apply (simp add: wens_single_Un_eq) 449 apply (force simp add: wens_single_finite_Un_eq) 450txt\<open>Union inductive step\<close> 451apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)") 452 apply (blast dest!: subset_wens_single_finite, simp) 453apply (rule disjI1 [OF Union_eq_wens_single], blast+) 454done 455 456lemma wens_single_finite_in_wens_set: 457 "single_valued act \<Longrightarrow> 458 wens_single_finite act B k 459 \<in> wens_set (mk_program (init, {act}, allowed)) B" 460apply (induct_tac k) 461 apply (simp add: wens_single_finite_def wens_set.Basis) 462apply (simp add: wens_set.Wens 463 wens_single_finite_Suc_eq_wens [of act B _ init allowed]) 464done 465 466lemma single_subset_wens_set: 467 "single_valued act 468 ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 469 wens_set (mk_program (init, {act}, allowed)) B" 470apply (simp add: image_def wens_single_eq_Union) 471apply (blast intro: wens_set.Union wens_single_finite_in_wens_set) 472done 473 474text\<open>Theorem (4.29)\<close> 475theorem wens_set_single_eq: 476 "[|F = mk_program (init, {act}, allowed); single_valued act|] 477 ==> wens_set F B = 478 insert (wens_single act B) (range (wens_single_finite act B))" 479apply (rule equalityI) 480 apply (simp add: wens_set_subset_single) 481apply (erule ssubst, erule single_subset_wens_set) 482done 483 484text\<open>Generalizing Misra's Fixed Point Union Theorem (4.41)\<close> 485 486lemma fp_leadsTo_Join: 487 "[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B" 488apply (rule leadsTo_Join, assumption, blast) 489apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast) 490done 491 492end 493