1(* Title: HOL/UNITY/Constrains.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5Weak safety relations: restricted to the set of reachable states. 6*) 7 8section\<open>Weak Safety\<close> 9 10theory Constrains imports UNITY begin 11 12 (*Initial states and program => (final state, reversed trace to it)... 13 Arguments MUST be curried in an inductive definition*) 14 15inductive_set 16 traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" 17 for init :: "'a set" and acts :: "('a * 'a)set set" 18 where 19 (*Initial trace is empty*) 20 Init: "s \<in> init ==> (s,[]) \<in> traces init acts" 21 22 | Acts: "[| act \<in> acts; (s,evs) \<in> traces init acts; (s,s') \<in> act |] 23 ==> (s', s#evs) \<in> traces init acts" 24 25 26inductive_set 27 reachable :: "'a program => 'a set" 28 for F :: "'a program" 29 where 30 Init: "s \<in> Init F ==> s \<in> reachable F" 31 32 | Acts: "[| act \<in> Acts F; s \<in> reachable F; (s,s') \<in> act |] 33 ==> s' \<in> reachable F" 34 35definition Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) where 36 "A Co B == {F. F \<in> (reachable F \<inter> A) co B}" 37 38definition Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) where 39 "A Unless B == (A-B) Co (A \<union> B)" 40 41definition Stable :: "'a set => 'a program set" where 42 "Stable A == A Co A" 43 44 (*Always is the weak form of "invariant"*) 45definition Always :: "'a set => 'a program set" where 46 "Always A == {F. Init F \<subseteq> A} \<inter> Stable A" 47 48 (*Polymorphic in both states and the meaning of \<le> *) 49definition Increasing :: "['a => 'b::{order}] => 'a program set" where 50 "Increasing f == \<Inter>z. Stable {s. z \<le> f s}" 51 52 53subsection\<open>traces and reachable\<close> 54 55lemma reachable_equiv_traces: 56 "reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}" 57apply safe 58apply (erule_tac [2] traces.induct) 59apply (erule reachable.induct) 60apply (blast intro: reachable.intros traces.intros)+ 61done 62 63lemma Init_subset_reachable: "Init F \<subseteq> reachable F" 64by (blast intro: reachable.intros) 65 66lemma stable_reachable [intro!,simp]: 67 "Acts G \<subseteq> Acts F ==> G \<in> stable (reachable F)" 68by (blast intro: stableI constrainsI reachable.intros) 69 70(*The set of all reachable states is an invariant...*) 71lemma invariant_reachable: "F \<in> invariant (reachable F)" 72apply (simp add: invariant_def) 73apply (blast intro: reachable.intros) 74done 75 76(*...in fact the strongest invariant!*) 77lemma invariant_includes_reachable: "F \<in> invariant A ==> reachable F \<subseteq> A" 78apply (simp add: stable_def constrains_def invariant_def) 79apply (rule subsetI) 80apply (erule reachable.induct) 81apply (blast intro: reachable.intros)+ 82done 83 84 85subsection\<open>Co\<close> 86 87(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*) 88lemmas constrains_reachable_Int = 89 subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int] 90 91(*Resembles the previous definition of Constrains*) 92lemma Constrains_eq_constrains: 93 "A Co B = {F. F \<in> (reachable F \<inter> A) co (reachable F \<inter> B)}" 94apply (unfold Constrains_def) 95apply (blast dest: constrains_reachable_Int intro: constrains_weaken) 96done 97 98lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'" 99apply (unfold Constrains_def) 100apply (blast intro: constrains_weaken_L) 101done 102 103lemma stable_imp_Stable: "F \<in> stable A ==> F \<in> Stable A" 104apply (unfold stable_def Stable_def) 105apply (erule constrains_imp_Constrains) 106done 107 108lemma ConstrainsI: 109 "(!!act s s'. [| act \<in> Acts F; (s,s') \<in> act; s \<in> A |] ==> s' \<in> A') 110 ==> F \<in> A Co A'" 111apply (rule constrains_imp_Constrains) 112apply (blast intro: constrainsI) 113done 114 115lemma Constrains_empty [iff]: "F \<in> {} Co B" 116by (unfold Constrains_def constrains_def, blast) 117 118lemma Constrains_UNIV [iff]: "F \<in> A Co UNIV" 119by (blast intro: ConstrainsI) 120 121lemma Constrains_weaken_R: 122 "[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'" 123apply (unfold Constrains_def) 124apply (blast intro: constrains_weaken_R) 125done 126 127lemma Constrains_weaken_L: 128 "[| F \<in> A Co A'; B \<subseteq> A |] ==> F \<in> B Co A'" 129apply (unfold Constrains_def) 130apply (blast intro: constrains_weaken_L) 131done 132 133lemma Constrains_weaken: 134 "[| F \<in> A Co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B Co B'" 135apply (unfold Constrains_def) 136apply (blast intro: constrains_weaken) 137done 138 139(** Union **) 140 141lemma Constrains_Un: 142 "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<union> B) Co (A' \<union> B')" 143apply (unfold Constrains_def) 144apply (blast intro: constrains_Un [THEN constrains_weaken]) 145done 146 147lemma Constrains_UN: 148 assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)" 149 shows "F \<in> (\<Union>i \<in> I. A i) Co (\<Union>i \<in> I. A' i)" 150apply (unfold Constrains_def) 151apply (rule CollectI) 152apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, 153 THEN constrains_weaken], auto) 154done 155 156(** Intersection **) 157 158lemma Constrains_Int: 159 "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<inter> B) Co (A' \<inter> B')" 160apply (unfold Constrains_def) 161apply (blast intro: constrains_Int [THEN constrains_weaken]) 162done 163 164lemma Constrains_INT: 165 assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)" 166 shows "F \<in> (\<Inter>i \<in> I. A i) Co (\<Inter>i \<in> I. A' i)" 167apply (unfold Constrains_def) 168apply (rule CollectI) 169apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, 170 THEN constrains_weaken], auto) 171done 172 173lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable F \<inter> A \<subseteq> A'" 174by (simp add: constrains_imp_subset Constrains_def) 175 176lemma Constrains_trans: "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C" 177apply (simp add: Constrains_eq_constrains) 178apply (blast intro: constrains_trans constrains_weaken) 179done 180 181lemma Constrains_cancel: 182 "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')" 183apply (simp add: Constrains_eq_constrains constrains_def) 184apply best 185done 186 187 188subsection\<open>Stable\<close> 189 190(*Useful because there's no Stable_weaken. [Tanja Vos]*) 191lemma Stable_eq: "[| F \<in> Stable A; A = B |] ==> F \<in> Stable B" 192by blast 193 194lemma Stable_eq_stable: "(F \<in> Stable A) = (F \<in> stable (reachable F \<inter> A))" 195by (simp add: Stable_def Constrains_eq_constrains stable_def) 196 197lemma StableI: "F \<in> A Co A ==> F \<in> Stable A" 198by (unfold Stable_def, assumption) 199 200lemma StableD: "F \<in> Stable A ==> F \<in> A Co A" 201by (unfold Stable_def, assumption) 202 203lemma Stable_Un: 204 "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<union> A')" 205apply (unfold Stable_def) 206apply (blast intro: Constrains_Un) 207done 208 209lemma Stable_Int: 210 "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<inter> A')" 211apply (unfold Stable_def) 212apply (blast intro: Constrains_Int) 213done 214 215lemma Stable_Constrains_Un: 216 "[| F \<in> Stable C; F \<in> A Co (C \<union> A') |] 217 ==> F \<in> (C \<union> A) Co (C \<union> A')" 218apply (unfold Stable_def) 219apply (blast intro: Constrains_Un [THEN Constrains_weaken]) 220done 221 222lemma Stable_Constrains_Int: 223 "[| F \<in> Stable C; F \<in> (C \<inter> A) Co A' |] 224 ==> F \<in> (C \<inter> A) Co (C \<inter> A')" 225apply (unfold Stable_def) 226apply (blast intro: Constrains_Int [THEN Constrains_weaken]) 227done 228 229lemma Stable_UN: 230 "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Union>i \<in> I. A i)" 231by (simp add: Stable_def Constrains_UN) 232 233lemma Stable_INT: 234 "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Inter>i \<in> I. A i)" 235by (simp add: Stable_def Constrains_INT) 236 237lemma Stable_reachable: "F \<in> Stable (reachable F)" 238by (simp add: Stable_eq_stable) 239 240 241 242subsection\<open>Increasing\<close> 243 244lemma IncreasingD: 245 "F \<in> Increasing f ==> F \<in> Stable {s. x \<le> f s}" 246by (unfold Increasing_def, blast) 247 248lemma mono_Increasing_o: 249 "mono g ==> Increasing f \<subseteq> Increasing (g o f)" 250apply (simp add: Increasing_def Stable_def Constrains_def stable_def 251 constrains_def) 252apply (blast intro: monoD order_trans) 253done 254 255lemma strict_IncreasingD: 256 "!!z::nat. F \<in> Increasing f ==> F \<in> Stable {s. z < f s}" 257by (simp add: Increasing_def Suc_le_eq [symmetric]) 258 259lemma increasing_imp_Increasing: 260 "F \<in> increasing f ==> F \<in> Increasing f" 261apply (unfold increasing_def Increasing_def) 262apply (blast intro: stable_imp_Stable) 263done 264 265lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff] 266 267 268subsection\<open>The Elimination Theorem\<close> 269 270(*The "free" m has become universally quantified! Should the premise be !!m 271instead of \<forall>m ? Would make it harder to use in forward proof.*) 272 273lemma Elimination: 274 "[| \<forall>m. F \<in> {s. s x = m} Co (B m) |] 275 ==> F \<in> {s. s x \<in> M} Co (\<Union>m \<in> M. B m)" 276by (unfold Constrains_def constrains_def, blast) 277 278(*As above, but for the trivial case of a one-variable state, in which the 279 state is identified with its one variable.*) 280lemma Elimination_sing: 281 "(\<forall>m. F \<in> {m} Co (B m)) ==> F \<in> M Co (\<Union>m \<in> M. B m)" 282by (unfold Constrains_def constrains_def, blast) 283 284 285subsection\<open>Specialized laws for handling Always\<close> 286 287(** Natural deduction rules for "Always A" **) 288 289lemma AlwaysI: "[| Init F \<subseteq> A; F \<in> Stable A |] ==> F \<in> Always A" 290by (simp add: Always_def) 291 292lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A" 293by (simp add: Always_def) 294 295lemmas AlwaysE = AlwaysD [THEN conjE] 296lemmas Always_imp_Stable = AlwaysD [THEN conjunct2] 297 298 299(*The set of all reachable states is Always*) 300lemma Always_includes_reachable: "F \<in> Always A ==> reachable F \<subseteq> A" 301apply (simp add: Stable_def Constrains_def constrains_def Always_def) 302apply (rule subsetI) 303apply (erule reachable.induct) 304apply (blast intro: reachable.intros)+ 305done 306 307lemma invariant_imp_Always: 308 "F \<in> invariant A ==> F \<in> Always A" 309apply (unfold Always_def invariant_def Stable_def stable_def) 310apply (blast intro: constrains_imp_Constrains) 311done 312 313lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always] 314 315lemma Always_eq_invariant_reachable: 316 "Always A = {F. F \<in> invariant (reachable F \<inter> A)}" 317apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains 318 stable_def) 319apply (blast intro: reachable.intros) 320done 321 322(*the RHS is the traditional definition of the "always" operator*) 323lemma Always_eq_includes_reachable: "Always A = {F. reachable F \<subseteq> A}" 324by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable) 325 326lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV" 327by (auto simp add: Always_eq_includes_reachable) 328 329lemma UNIV_AlwaysI: "UNIV \<subseteq> A ==> F \<in> Always A" 330by (auto simp add: Always_eq_includes_reachable) 331 332lemma Always_eq_UN_invariant: "Always A = (\<Union>I \<in> Pow A. invariant I)" 333apply (simp add: Always_eq_includes_reachable) 334apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] 335 invariant_includes_reachable [THEN subsetD]) 336done 337 338lemma Always_weaken: "[| F \<in> Always A; A \<subseteq> B |] ==> F \<in> Always B" 339by (auto simp add: Always_eq_includes_reachable) 340 341 342subsection\<open>"Co" rules involving Always\<close> 343 344lemma Always_Constrains_pre: 345 "F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')" 346by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def 347 Int_assoc [symmetric]) 348 349lemma Always_Constrains_post: 350 "F \<in> Always INV ==> (F \<in> A Co (INV \<inter> A')) = (F \<in> A Co A')" 351by (simp add: Always_includes_reachable [THEN Int_absorb2] 352 Constrains_eq_constrains Int_assoc [symmetric]) 353 354(* [| F \<in> Always INV; F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *) 355lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1] 356 357(* [| F \<in> Always INV; F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *) 358lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2] 359 360(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) 361lemma Always_Constrains_weaken: 362 "[| F \<in> Always C; F \<in> A Co A'; 363 C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |] 364 ==> F \<in> B Co B'" 365apply (rule Always_ConstrainsI, assumption) 366apply (drule Always_ConstrainsD, assumption) 367apply (blast intro: Constrains_weaken) 368done 369 370 371(** Conjoining Always properties **) 372 373lemma Always_Int_distrib: "Always (A \<inter> B) = Always A \<inter> Always B" 374by (auto simp add: Always_eq_includes_reachable) 375 376lemma Always_INT_distrib: "Always (\<Inter>(A ` I)) = (\<Inter>i \<in> I. Always (A i))" 377by (auto simp add: Always_eq_includes_reachable) 378 379lemma Always_Int_I: 380 "[| F \<in> Always A; F \<in> Always B |] ==> F \<in> Always (A \<inter> B)" 381by (simp add: Always_Int_distrib) 382 383(*Allows a kind of "implication introduction"*) 384lemma Always_Compl_Un_eq: 385 "F \<in> Always A ==> (F \<in> Always (-A \<union> B)) = (F \<in> Always B)" 386by (auto simp add: Always_eq_includes_reachable) 387 388(*Delete the nearest invariance assumption (which will be the second one 389 used by Always_Int_I) *) 390lemmas Always_thin = thin_rl [of "F \<in> Always A"] for F A 391 392 393subsection\<open>Totalize\<close> 394 395lemma reachable_imp_reachable_tot: 396 "s \<in> reachable F ==> s \<in> reachable (totalize F)" 397apply (erule reachable.induct) 398 apply (rule reachable.Init) 399 apply simp 400apply (rule_tac act = "totalize_act act" in reachable.Acts) 401apply (auto simp add: totalize_act_def) 402done 403 404lemma reachable_tot_imp_reachable: 405 "s \<in> reachable (totalize F) ==> s \<in> reachable F" 406apply (erule reachable.induct) 407 apply (rule reachable.Init, simp) 408apply (force simp add: totalize_act_def intro: reachable.Acts) 409done 410 411lemma reachable_tot_eq [simp]: "reachable (totalize F) = reachable F" 412by (blast intro: reachable_imp_reachable_tot reachable_tot_imp_reachable) 413 414lemma totalize_Constrains_iff [simp]: "(totalize F \<in> A Co B) = (F \<in> A Co B)" 415by (simp add: Constrains_def) 416 417lemma totalize_Stable_iff [simp]: "(totalize F \<in> Stable A) = (F \<in> Stable A)" 418by (simp add: Stable_def) 419 420lemma totalize_Always_iff [simp]: "(totalize F \<in> Always A) = (F \<in> Always A)" 421by (simp add: Always_def) 422 423end 424