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