src/HOL/UNITY/Constrains.thy
 author wenzelm Sat Jun 14 23:19:51 2008 +0200 (2008-06-14) changeset 27208 5fe899199f85 parent 23767 7272a839ccd9 child 32960 69916a850301 permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
```     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   (*Initial states and program => (final state, reversed trace to it)...
```
```    14     Arguments MUST be curried in an inductive definition*)
```
```    15
```
```    16 inductive_set
```
```    17   traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
```
```    18   for init :: "'a set" and acts :: "('a * 'a)set set"
```
```    19   where
```
```    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 inductive_set
```
```    28   reachable :: "'a program => 'a set"
```
```    29   for F :: "'a program"
```
```    30   where
```
```    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
```