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