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