1(* Title: ZF/UNITY/Constrains.thy 2 Author: Sidi O Ehmety, Computer Laboratory 3 Copyright 2001 University of Cambridge 4*) 5 6section\<open>Weak Safety Properties\<close> 7 8theory Constrains 9imports UNITY 10begin 11 12consts traces :: "[i, i] => i" 13 (* Initial states and program => (final state, reversed trace to it)... 14 the domain may also be state*list(state) *) 15inductive 16 domains 17 "traces(init, acts)" <= 18 "(init \<union> (\<Union>act\<in>acts. field(act)))*list(\<Union>act\<in>acts. field(act))" 19 intros 20 (*Initial trace is empty*) 21 Init: "s: init ==> <s,[]> \<in> traces(init,acts)" 22 23 Acts: "[| act:acts; <s,evs> \<in> traces(init,acts); <s,s'>: act |] 24 ==> <s', Cons(s,evs)> \<in> traces(init, acts)" 25 26 type_intros list.intros UnI1 UnI2 UN_I fieldI2 fieldI1 27 28 29consts reachable :: "i=>i" 30inductive 31 domains 32 "reachable(F)" \<subseteq> "Init(F) \<union> (\<Union>act\<in>Acts(F). field(act))" 33 intros 34 Init: "s:Init(F) ==> s:reachable(F)" 35 36 Acts: "[| act: Acts(F); s:reachable(F); <s,s'>: act |] 37 ==> s':reachable(F)" 38 39 type_intros UnI1 UnI2 fieldI2 UN_I 40 41 42definition 43 Constrains :: "[i,i] => i" (infixl "Co" 60) where 44 "A Co B == {F:program. F:(reachable(F) \<inter> A) co B}" 45 46definition 47 op_Unless :: "[i, i] => i" (infixl "Unless" 60) where 48 "A Unless B == (A-B) Co (A \<union> B)" 49 50definition 51 Stable :: "i => i" where 52 "Stable(A) == A Co A" 53 54definition 55 (*Always is the weak form of "invariant"*) 56 Always :: "i => i" where 57 "Always(A) == initially(A) \<inter> Stable(A)" 58 59 60(*** traces and reachable ***) 61 62lemma reachable_type: "reachable(F) \<subseteq> state" 63apply (cut_tac F = F in Init_type) 64apply (cut_tac F = F in Acts_type) 65apply (cut_tac F = F in reachable.dom_subset, blast) 66done 67 68lemma st_set_reachable: "st_set(reachable(F))" 69apply (unfold st_set_def) 70apply (rule reachable_type) 71done 72declare st_set_reachable [iff] 73 74lemma reachable_Int_state: "reachable(F) \<inter> state = reachable(F)" 75by (cut_tac reachable_type, auto) 76declare reachable_Int_state [iff] 77 78lemma state_Int_reachable: "state \<inter> reachable(F) = reachable(F)" 79by (cut_tac reachable_type, auto) 80declare state_Int_reachable [iff] 81 82lemma reachable_equiv_traces: 83"F \<in> program ==> reachable(F)={s \<in> state. \<exists>evs. <s,evs>:traces(Init(F), Acts(F))}" 84apply (rule equalityI, safe) 85apply (blast dest: reachable_type [THEN subsetD]) 86apply (erule_tac [2] traces.induct) 87apply (erule reachable.induct) 88apply (blast intro: reachable.intros traces.intros)+ 89done 90 91lemma Init_into_reachable: "Init(F) \<subseteq> reachable(F)" 92by (blast intro: reachable.intros) 93 94lemma stable_reachable: "[| F \<in> program; G \<in> program; 95 Acts(G) \<subseteq> Acts(F) |] ==> G \<in> stable(reachable(F))" 96apply (blast intro: stableI constrainsI st_setI 97 reachable_type [THEN subsetD] reachable.intros) 98done 99 100declare stable_reachable [intro!] 101declare stable_reachable [simp] 102 103(*The set of all reachable states is an invariant...*) 104lemma invariant_reachable: 105 "F \<in> program ==> F \<in> invariant(reachable(F))" 106apply (unfold invariant_def initially_def) 107apply (blast intro: reachable_type [THEN subsetD] reachable.intros) 108done 109 110(*...in fact the strongest invariant!*) 111lemma invariant_includes_reachable: "F \<in> invariant(A) ==> reachable(F) \<subseteq> A" 112apply (cut_tac F = F in Acts_type) 113apply (cut_tac F = F in Init_type) 114apply (cut_tac F = F in reachable_type) 115apply (simp (no_asm_use) add: stable_def constrains_def invariant_def initially_def) 116apply (rule subsetI) 117apply (erule reachable.induct) 118apply (blast intro: reachable.intros)+ 119done 120 121(*** Co ***) 122 123lemma constrains_reachable_Int: "F \<in> B co B'==>F:(reachable(F) \<inter> B) co (reachable(F) \<inter> B')" 124apply (frule constrains_type [THEN subsetD]) 125apply (frule stable_reachable [OF _ _ subset_refl]) 126apply (simp_all add: stable_def constrains_Int) 127done 128 129(*Resembles the previous definition of Constrains*) 130lemma Constrains_eq_constrains: 131"A Co B = {F \<in> program. F:(reachable(F) \<inter> A) co (reachable(F) \<inter> B)}" 132apply (unfold Constrains_def) 133apply (blast dest: constrains_reachable_Int constrains_type [THEN subsetD] 134 intro: constrains_weaken) 135done 136 137lemmas Constrains_def2 = Constrains_eq_constrains [THEN eq_reflection] 138 139lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'" 140apply (unfold Constrains_def) 141apply (blast intro: constrains_weaken_L dest: constrainsD2) 142done 143 144lemma ConstrainsI: 145 "[|!!act s s'. [| act \<in> Acts(F); <s,s'>:act; s \<in> A |] ==> s':A'; 146 F \<in> program|] 147 ==> F \<in> A Co A'" 148apply (auto simp add: Constrains_def constrains_def st_set_def) 149apply (blast dest: reachable_type [THEN subsetD]) 150done 151 152lemma Constrains_type: 153 "A Co B \<subseteq> program" 154apply (unfold Constrains_def, blast) 155done 156 157lemma Constrains_empty: "F \<in> 0 Co B \<longleftrightarrow> F \<in> program" 158by (auto dest: Constrains_type [THEN subsetD] 159 intro: constrains_imp_Constrains) 160declare Constrains_empty [iff] 161 162lemma Constrains_state: "F \<in> A Co state \<longleftrightarrow> F \<in> program" 163apply (unfold Constrains_def) 164apply (auto dest: Constrains_type [THEN subsetD] intro: constrains_imp_Constrains) 165done 166declare Constrains_state [iff] 167 168lemma Constrains_weaken_R: 169 "[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'" 170apply (unfold Constrains_def2) 171apply (blast intro: constrains_weaken_R) 172done 173 174lemma Constrains_weaken_L: 175 "[| F \<in> A Co A'; B<=A |] ==> F \<in> B Co A'" 176apply (unfold Constrains_def2) 177apply (blast intro: constrains_weaken_L st_set_subset) 178done 179 180lemma Constrains_weaken: 181 "[| F \<in> A Co A'; B<=A; A'<=B' |] ==> F \<in> B Co B'" 182apply (unfold Constrains_def2) 183apply (blast intro: constrains_weaken st_set_subset) 184done 185 186(** Union **) 187lemma Constrains_Un: 188 "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<union> B) Co (A' \<union> B')" 189apply (unfold Constrains_def2, auto) 190apply (simp add: Int_Un_distrib) 191apply (blast intro: constrains_Un) 192done 193 194lemma Constrains_UN: 195 "[|(!!i. i \<in> I==>F \<in> A(i) Co A'(i)); F \<in> program|] 196 ==> F:(\<Union>i \<in> I. A(i)) Co (\<Union>i \<in> I. A'(i))" 197by (auto intro: constrains_UN simp del: UN_simps 198 simp add: Constrains_def2 Int_UN_distrib) 199 200 201(** Intersection **) 202 203lemma Constrains_Int: 204 "[| F \<in> A Co A'; F \<in> B Co B'|]==> F:(A \<inter> B) Co (A' \<inter> B')" 205apply (unfold Constrains_def) 206apply (subgoal_tac "reachable (F) \<inter> (A \<inter> B) = (reachable (F) \<inter> A) \<inter> (reachable (F) \<inter> B) ") 207apply (auto intro: constrains_Int) 208done 209 210lemma Constrains_INT: 211 "[| (!!i. i \<in> I ==>F \<in> A(i) Co A'(i)); F \<in> program |] 212 ==> F:(\<Inter>i \<in> I. A(i)) Co (\<Inter>i \<in> I. A'(i))" 213apply (simp (no_asm_simp) del: INT_simps add: Constrains_def INT_extend_simps) 214apply (rule constrains_INT) 215apply (auto simp add: Constrains_def) 216done 217 218lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable(F) \<inter> A \<subseteq> A'" 219apply (unfold Constrains_def) 220apply (blast dest: constrains_imp_subset) 221done 222 223lemma Constrains_trans: 224 "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C" 225apply (unfold Constrains_def2) 226apply (blast intro: constrains_trans constrains_weaken) 227done 228 229lemma Constrains_cancel: 230"[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')" 231apply (unfold Constrains_def2) 232apply (simp (no_asm_use) add: Int_Un_distrib) 233apply (blast intro: constrains_cancel) 234done 235 236(*** Stable ***) 237(* Useful because there's no Stable_weaken. [Tanja Vos] *) 238 239lemma stable_imp_Stable: 240"F \<in> stable(A) ==> F \<in> Stable(A)" 241 242apply (unfold stable_def Stable_def) 243apply (erule constrains_imp_Constrains) 244done 245 246lemma Stable_eq: "[| F \<in> Stable(A); A = B |] ==> F \<in> Stable(B)" 247by blast 248 249lemma Stable_eq_stable: 250"F \<in> Stable(A) \<longleftrightarrow> (F \<in> stable(reachable(F) \<inter> A))" 251apply (auto dest: constrainsD2 simp add: Stable_def stable_def Constrains_def2) 252done 253 254lemma StableI: "F \<in> A Co A ==> F \<in> Stable(A)" 255by (unfold Stable_def, assumption) 256 257lemma StableD: "F \<in> Stable(A) ==> F \<in> A Co A" 258by (unfold Stable_def, assumption) 259 260lemma Stable_Un: 261 "[| F \<in> Stable(A); F \<in> Stable(A') |] ==> F \<in> Stable(A \<union> A')" 262apply (unfold Stable_def) 263apply (blast intro: Constrains_Un) 264done 265 266lemma Stable_Int: 267 "[| F \<in> Stable(A); F \<in> Stable(A') |] ==> F \<in> Stable (A \<inter> A')" 268apply (unfold Stable_def) 269apply (blast intro: Constrains_Int) 270done 271 272lemma Stable_Constrains_Un: 273 "[| F \<in> Stable(C); F \<in> A Co (C \<union> A') |] 274 ==> F \<in> (C \<union> A) Co (C \<union> A')" 275apply (unfold Stable_def) 276apply (blast intro: Constrains_Un [THEN Constrains_weaken_R]) 277done 278 279lemma Stable_Constrains_Int: 280 "[| F \<in> Stable(C); F \<in> (C \<inter> A) Co A' |] 281 ==> F \<in> (C \<inter> A) Co (C \<inter> A')" 282apply (unfold Stable_def) 283apply (blast intro: Constrains_Int [THEN Constrains_weaken]) 284done 285 286lemma Stable_UN: 287 "[| (!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program |] 288 ==> F \<in> Stable (\<Union>i \<in> I. A(i))" 289apply (simp add: Stable_def) 290apply (blast intro: Constrains_UN) 291done 292 293lemma Stable_INT: 294 "[|(!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program |] 295 ==> F \<in> Stable (\<Inter>i \<in> I. A(i))" 296apply (simp add: Stable_def) 297apply (blast intro: Constrains_INT) 298done 299 300lemma Stable_reachable: "F \<in> program ==>F \<in> Stable (reachable(F))" 301apply (simp (no_asm_simp) add: Stable_eq_stable Int_absorb) 302done 303 304lemma Stable_type: "Stable(A) \<subseteq> program" 305apply (unfold Stable_def) 306apply (rule Constrains_type) 307done 308 309(*** The Elimination Theorem. The "free" m has become universally quantified! 310 Should the premise be !!m instead of \<forall>m ? Would make it harder to use 311 in forward proof. ***) 312 313lemma Elimination: 314 "[| \<forall>m \<in> M. F \<in> ({s \<in> A. x(s) = m}) Co (B(m)); F \<in> program |] 315 ==> F \<in> ({s \<in> A. x(s):M}) Co (\<Union>m \<in> M. B(m))" 316apply (unfold Constrains_def, auto) 317apply (rule_tac A1 = "reachable (F) \<inter> A" 318 in UNITY.elimination [THEN constrains_weaken_L]) 319apply (auto intro: constrains_weaken_L) 320done 321 322(* As above, but for the special case of A=state *) 323lemma Elimination2: 324 "[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} Co B(m); F \<in> program |] 325 ==> F \<in> {s \<in> state. x(s):M} Co (\<Union>m \<in> M. B(m))" 326apply (blast intro: Elimination) 327done 328 329(** Unless **) 330 331lemma Unless_type: "A Unless B <=program" 332apply (unfold op_Unless_def) 333apply (rule Constrains_type) 334done 335 336(*** Specialized laws for handling Always ***) 337 338(** Natural deduction rules for "Always A" **) 339 340lemma AlwaysI: 341"[| Init(F)<=A; F \<in> Stable(A) |] ==> F \<in> Always(A)" 342 343apply (unfold Always_def initially_def) 344apply (frule Stable_type [THEN subsetD], auto) 345done 346 347lemma AlwaysD: "F \<in> Always(A) ==> Init(F)<=A & F \<in> Stable(A)" 348by (simp add: Always_def initially_def) 349 350lemmas AlwaysE = AlwaysD [THEN conjE] 351lemmas Always_imp_Stable = AlwaysD [THEN conjunct2] 352 353(*The set of all reachable states is Always*) 354lemma Always_includes_reachable: "F \<in> Always(A) ==> reachable(F) \<subseteq> A" 355apply (simp (no_asm_use) add: Stable_def Constrains_def constrains_def Always_def initially_def) 356apply (rule subsetI) 357apply (erule reachable.induct) 358apply (blast intro: reachable.intros)+ 359done 360 361lemma invariant_imp_Always: 362 "F \<in> invariant(A) ==> F \<in> Always(A)" 363apply (unfold Always_def invariant_def Stable_def stable_def) 364apply (blast intro: constrains_imp_Constrains) 365done 366 367lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always] 368 369lemma Always_eq_invariant_reachable: "Always(A) = {F \<in> program. F \<in> invariant(reachable(F) \<inter> A)}" 370apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def) 371apply (rule equalityI, auto) 372apply (blast intro: reachable.intros reachable_type) 373done 374 375(*the RHS is the traditional definition of the "always" operator*) 376lemma Always_eq_includes_reachable: "Always(A) = {F \<in> program. reachable(F) \<subseteq> A}" 377apply (rule equalityI, safe) 378apply (auto dest: invariant_includes_reachable 379 simp add: subset_Int_iff invariant_reachable Always_eq_invariant_reachable) 380done 381 382lemma Always_type: "Always(A) \<subseteq> program" 383by (unfold Always_def initially_def, auto) 384 385lemma Always_state_eq: "Always(state) = program" 386apply (rule equalityI) 387apply (auto dest: Always_type [THEN subsetD] reachable_type [THEN subsetD] 388 simp add: Always_eq_includes_reachable) 389done 390declare Always_state_eq [simp] 391 392lemma state_AlwaysI: "F \<in> program ==> F \<in> Always(state)" 393by (auto dest: reachable_type [THEN subsetD] 394 simp add: Always_eq_includes_reachable) 395 396lemma Always_eq_UN_invariant: "st_set(A) ==> Always(A) = (\<Union>I \<in> Pow(A). invariant(I))" 397apply (simp (no_asm) add: Always_eq_includes_reachable) 398apply (rule equalityI, auto) 399apply (blast intro: invariantI rev_subsetD [OF _ Init_into_reachable] 400 rev_subsetD [OF _ invariant_includes_reachable] 401 dest: invariant_type [THEN subsetD])+ 402done 403 404lemma Always_weaken: "[| F \<in> Always(A); A \<subseteq> B |] ==> F \<in> Always(B)" 405by (auto simp add: Always_eq_includes_reachable) 406 407 408(*** "Co" rules involving Always ***) 409lemmas Int_absorb2 = subset_Int_iff [unfolded iff_def, THEN conjunct1, THEN mp] 410 411lemma Always_Constrains_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) Co A') \<longleftrightarrow> (F \<in> A Co A')" 412apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_def Int_assoc [symmetric]) 413done 414 415lemma Always_Constrains_post: "F \<in> Always(I) ==> (F \<in> A Co (I \<inter> A')) \<longleftrightarrow>(F \<in> A Co A')" 416apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_eq_constrains Int_assoc [symmetric]) 417done 418 419lemma Always_ConstrainsI: "[| F \<in> Always(I); F \<in> (I \<inter> A) Co A' |] ==> F \<in> A Co A'" 420by (blast intro: Always_Constrains_pre [THEN iffD1]) 421 422(* [| F \<in> Always(I); F \<in> A Co A' |] ==> F \<in> A Co (I \<inter> A') *) 423lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2] 424 425(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) 426lemma Always_Constrains_weaken: 427"[|F \<in> Always(C); F \<in> A Co A'; C \<inter> B<=A; C \<inter> A'<=B'|]==>F \<in> B Co B'" 428apply (rule Always_ConstrainsI) 429apply (drule_tac [2] Always_ConstrainsD, simp_all) 430apply (blast intro: Constrains_weaken) 431done 432 433(** Conjoining Always properties **) 434lemma Always_Int_distrib: "Always(A \<inter> B) = Always(A) \<inter> Always(B)" 435by (auto simp add: Always_eq_includes_reachable) 436 437(* the premise i \<in> I is need since \<Inter>is formally not defined for I=0 *) 438lemma Always_INT_distrib: "i \<in> I==>Always(\<Inter>i \<in> I. A(i)) = (\<Inter>i \<in> I. Always(A(i)))" 439apply (rule equalityI) 440apply (auto simp add: Inter_iff Always_eq_includes_reachable) 441done 442 443 444lemma Always_Int_I: "[| F \<in> Always(A); F \<in> Always(B) |] ==> F \<in> Always(A \<inter> B)" 445apply (simp (no_asm_simp) add: Always_Int_distrib) 446done 447 448(*Allows a kind of "implication introduction"*) 449lemma Always_Diff_Un_eq: "[| F \<in> Always(A) |] ==> (F \<in> Always(C-A \<union> B)) \<longleftrightarrow> (F \<in> Always(B))" 450by (auto simp add: Always_eq_includes_reachable) 451 452(*Delete the nearest invariance assumption (which will be the second one 453 used by Always_Int_I) *) 454lemmas Always_thin = thin_rl [of "F \<in> Always(A)"] for F A 455 456(*To allow expansion of the program's definition when appropriate*) 457named_theorems program "program definitions" 458 459ML 460\<open> 461(*Combines two invariance ASSUMPTIONS into one. USEFUL??*) 462fun Always_Int_tac ctxt = 463 dresolve_tac ctxt @{thms Always_Int_I} THEN' 464 assume_tac ctxt THEN' 465 eresolve_tac ctxt @{thms Always_thin}; 466 467(*Combines a list of invariance THEOREMS into one.*) 468val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}); 469 470(*proves "co" properties when the program is specified*) 471 472fun constrains_tac ctxt = 473 SELECT_GOAL 474 (EVERY [REPEAT (Always_Int_tac ctxt 1), 475 REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1 476 ORELSE 477 resolve_tac ctxt [@{thm StableI}, @{thm stableI}, 478 @{thm constrains_imp_Constrains}] 1), 479 resolve_tac ctxt @{thms constrainsI} 1, 480 (* Three subgoals *) 481 rewrite_goal_tac ctxt [@{thm st_set_def}] 3, 482 REPEAT (force_tac ctxt 2), 483 full_simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 1, 484 ALLGOALS (clarify_tac ctxt), 485 REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})), 486 ALLGOALS (clarify_tac ctxt), 487 REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})), 488 ALLGOALS (clarify_tac ctxt), 489 ALLGOALS (asm_full_simp_tac ctxt), 490 ALLGOALS (clarify_tac ctxt)]); 491 492(*For proving invariants*) 493fun always_tac ctxt i = 494 resolve_tac ctxt @{thms AlwaysI} i THEN 495 force_tac ctxt i 496 THEN constrains_tac ctxt i; 497\<close> 498 499method_setup safety = \<open> 500 Scan.succeed (SIMPLE_METHOD' o constrains_tac)\<close> 501 "for proving safety properties" 502 503method_setup always = \<open> 504 Scan.succeed (SIMPLE_METHOD' o always_tac)\<close> 505 "for proving invariants" 506 507end 508