src/HOL/UNITY/Union.thy
author paulson
Fri Jan 31 20:12:44 2003 +0100 (2003-01-31)
changeset 13798 4c1a53627500
parent 13792 d1811693899c
child 13805 3786b2fd6808
permissions -rw-r--r--
conversion to new-style theories and tidying
paulson@5252
     1
(*  Title:      HOL/UNITY/Union.thy
paulson@5252
     2
    ID:         $Id$
paulson@5252
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5252
     4
    Copyright   1998  University of Cambridge
paulson@5252
     5
paulson@5804
     6
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
paulson@5252
     7
*)
paulson@5252
     8
paulson@13798
     9
header{*Unions of Programs*}
paulson@13798
    10
paulson@13792
    11
theory Union = SubstAx + FP:
paulson@5252
    12
paulson@5252
    13
constdefs
paulson@10064
    14
paulson@10064
    15
  (*FIXME: conjoin Init F Int Init G ~= {} *) 
paulson@13792
    16
  ok :: "['a program, 'a program] => bool"      (infixl "ok" 65)
paulson@10064
    17
    "F ok G == Acts F <= AllowedActs G &
paulson@10064
    18
               Acts G <= AllowedActs F"
paulson@10064
    19
paulson@10064
    20
  (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) 
paulson@13792
    21
  OK  :: "['a set, 'a => 'b program] => bool"
paulson@10064
    22
    "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
paulson@10064
    23
paulson@13792
    24
  JOIN  :: "['a set, 'a => 'b program] => 'b program"
paulson@10064
    25
    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
paulson@10064
    26
			     INT i:I. AllowedActs (F i))"
paulson@5252
    27
paulson@13792
    28
  Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
paulson@10064
    29
    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
paulson@10064
    30
			     AllowedActs F Int AllowedActs G)"
paulson@5252
    31
paulson@13792
    32
  SKIP :: "'a program"
paulson@10064
    33
    "SKIP == mk_program (UNIV, {}, UNIV)"
paulson@10064
    34
paulson@10064
    35
  (*Characterizes safety properties.  Used with specifying AllowedActs*)
paulson@10064
    36
  safety_prop :: "'a program set => bool"
paulson@10064
    37
    "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
paulson@5259
    38
paulson@5313
    39
syntax
paulson@13792
    40
  "@JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
paulson@13792
    41
  "@JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
paulson@5313
    42
paulson@5313
    43
translations
paulson@5313
    44
  "JN x:A. B"   == "JOIN A (%x. B)"
paulson@7359
    45
  "JN x y. B"   == "JN x. JN y. B"
paulson@7359
    46
  "JN x. B"     == "JOIN UNIV (%x. B)"
paulson@5313
    47
wenzelm@12114
    48
syntax (xsymbols)
paulson@13792
    49
  SKIP      :: "'a program"                              ("\<bottom>")
paulson@13792
    50
  "op Join" :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
paulson@13792
    51
  "@JOIN1"  :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
paulson@13792
    52
  "@JOIN"   :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _:_./ _)" 10)
paulson@13792
    53
paulson@13792
    54
paulson@13798
    55
subsection{*SKIP*}
paulson@13792
    56
paulson@13792
    57
lemma Init_SKIP [simp]: "Init SKIP = UNIV"
paulson@13792
    58
by (simp add: SKIP_def)
paulson@13792
    59
paulson@13792
    60
lemma Acts_SKIP [simp]: "Acts SKIP = {Id}"
paulson@13792
    61
by (simp add: SKIP_def)
paulson@13792
    62
paulson@13792
    63
lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV"
paulson@13792
    64
by (auto simp add: SKIP_def)
paulson@13792
    65
paulson@13792
    66
lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
paulson@13792
    67
by (force elim: reachable.induct intro: reachable.intros)
paulson@13792
    68
paulson@13798
    69
subsection{*SKIP and safety properties*}
paulson@13792
    70
paulson@13792
    71
lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)"
paulson@13792
    72
by (unfold constrains_def, auto)
paulson@13792
    73
paulson@13792
    74
lemma SKIP_in_Constrains_iff [iff]: "(SKIP : A Co B) = (A<=B)"
paulson@13792
    75
by (unfold Constrains_def, auto)
paulson@13792
    76
paulson@13792
    77
lemma SKIP_in_stable [iff]: "SKIP : stable A"
paulson@13792
    78
by (unfold stable_def, auto)
paulson@13792
    79
paulson@13792
    80
declare SKIP_in_stable [THEN stable_imp_Stable, iff]
paulson@13792
    81
paulson@13792
    82
paulson@13798
    83
subsection{*Join*}
paulson@13792
    84
paulson@13792
    85
lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G"
paulson@13792
    86
by (simp add: Join_def)
paulson@13792
    87
paulson@13792
    88
lemma Acts_Join [simp]: "Acts (F Join G) = Acts F Un Acts G"
paulson@13792
    89
by (auto simp add: Join_def)
paulson@13792
    90
paulson@13792
    91
lemma AllowedActs_Join [simp]:
paulson@13792
    92
     "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G"
paulson@13792
    93
by (auto simp add: Join_def)
paulson@13792
    94
paulson@13792
    95
paulson@13798
    96
subsection{*JN*}
paulson@13792
    97
paulson@13792
    98
lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP"
paulson@13792
    99
by (unfold JOIN_def SKIP_def, auto)
paulson@13792
   100
paulson@13792
   101
lemma JN_insert [simp]: "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)"
paulson@13792
   102
apply (rule program_equalityI)
paulson@13792
   103
apply (auto simp add: JOIN_def Join_def)
paulson@13792
   104
done
paulson@13792
   105
paulson@13792
   106
lemma Init_JN [simp]: "Init (JN i:I. F i) = (INT i:I. Init (F i))"
paulson@13792
   107
by (simp add: JOIN_def)
paulson@13792
   108
paulson@13792
   109
lemma Acts_JN [simp]: "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"
paulson@13792
   110
by (auto simp add: JOIN_def)
paulson@13792
   111
paulson@13792
   112
lemma AllowedActs_JN [simp]:
paulson@13792
   113
     "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))"
paulson@13792
   114
by (auto simp add: JOIN_def)
paulson@13792
   115
paulson@13792
   116
paulson@13792
   117
lemma JN_cong [cong]: 
paulson@13792
   118
    "[| I=J;  !!i. i:J ==> F i = G i |] ==> (JN i:I. F i) = (JN i:J. G i)"
paulson@13792
   119
by (simp add: JOIN_def)
paulson@13792
   120
paulson@13792
   121
paulson@13798
   122
subsection{*Algebraic laws*}
paulson@13792
   123
paulson@13792
   124
lemma Join_commute: "F Join G = G Join F"
paulson@13792
   125
by (simp add: Join_def Un_commute Int_commute)
paulson@13792
   126
paulson@13792
   127
lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)"
paulson@13792
   128
by (simp add: Un_ac Join_def Int_assoc insert_absorb)
paulson@13792
   129
 
paulson@13792
   130
lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)"
paulson@13792
   131
by (simp add: Un_ac Int_ac Join_def insert_absorb)
paulson@13792
   132
paulson@13792
   133
lemma Join_SKIP_left [simp]: "SKIP Join F = F"
paulson@13792
   134
apply (unfold Join_def SKIP_def)
paulson@13792
   135
apply (rule program_equalityI)
paulson@13792
   136
apply (simp_all (no_asm) add: insert_absorb)
paulson@13792
   137
done
paulson@13792
   138
paulson@13792
   139
lemma Join_SKIP_right [simp]: "F Join SKIP = F"
paulson@13792
   140
apply (unfold Join_def SKIP_def)
paulson@13792
   141
apply (rule program_equalityI)
paulson@13792
   142
apply (simp_all (no_asm) add: insert_absorb)
paulson@13792
   143
done
paulson@13792
   144
paulson@13792
   145
lemma Join_absorb [simp]: "F Join F = F"
paulson@13792
   146
apply (unfold Join_def)
paulson@13792
   147
apply (rule program_equalityI, auto)
paulson@13792
   148
done
paulson@13792
   149
paulson@13792
   150
lemma Join_left_absorb: "F Join (F Join G) = F Join G"
paulson@13792
   151
apply (unfold Join_def)
paulson@13792
   152
apply (rule program_equalityI, auto)
paulson@13792
   153
done
paulson@13792
   154
paulson@13792
   155
(*Join is an AC-operator*)
paulson@13792
   156
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
paulson@13792
   157
paulson@13792
   158
paulson@13798
   159
subsection{*JN laws*}
paulson@13792
   160
paulson@13792
   161
(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
paulson@13792
   162
lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)"
paulson@13792
   163
by (auto intro!: program_equalityI)
paulson@13792
   164
paulson@13792
   165
lemma JN_Un: "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))"
paulson@13792
   166
by (auto intro!: program_equalityI)
paulson@13792
   167
paulson@13792
   168
lemma JN_constant: "(JN i:I. c) = (if I={} then SKIP else c)"
paulson@13792
   169
by (rule program_equalityI, auto)
paulson@13792
   170
paulson@13792
   171
lemma JN_Join_distrib:
paulson@13792
   172
     "(JN i:I. F i Join G i) = (JN i:I. F i)  Join  (JN i:I. G i)"
paulson@13792
   173
by (auto intro!: program_equalityI)
paulson@13792
   174
paulson@13792
   175
lemma JN_Join_miniscope:
paulson@13792
   176
     "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)"
paulson@13792
   177
by (auto simp add: JN_Join_distrib JN_constant)
paulson@13792
   178
paulson@13792
   179
(*Used to prove guarantees_JN_I*)
paulson@13792
   180
lemma JN_Join_diff: "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F"
paulson@13792
   181
apply (unfold JOIN_def Join_def)
paulson@13792
   182
apply (rule program_equalityI, auto)
paulson@13792
   183
done
paulson@13792
   184
paulson@13792
   185
paulson@13798
   186
subsection{*Safety: co, stable, FP*}
paulson@13792
   187
paulson@13792
   188
(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B.  So an
paulson@13792
   189
  alternative precondition is A<=B, but most proofs using this rule require
paulson@13792
   190
  I to be nonempty for other reasons anyway.*)
paulson@13792
   191
lemma JN_constrains: 
paulson@13792
   192
    "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)"
paulson@13792
   193
by (simp add: constrains_def JOIN_def, blast)
paulson@13792
   194
paulson@13792
   195
lemma Join_constrains [simp]:
paulson@13792
   196
     "(F Join G : A co B) = (F : A co B & G : A co B)"
paulson@13792
   197
by (auto simp add: constrains_def Join_def)
paulson@13792
   198
paulson@13792
   199
lemma Join_unless [simp]:
paulson@13792
   200
     "(F Join G : A unless B) = (F : A unless B & G : A unless B)"
paulson@13792
   201
by (simp add: Join_constrains unless_def)
paulson@13792
   202
paulson@13792
   203
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
paulson@13792
   204
  reachable (F Join G) could be much bigger than reachable F, reachable G
paulson@13792
   205
*)
paulson@13792
   206
paulson@13792
   207
paulson@13792
   208
lemma Join_constrains_weaken:
paulson@13792
   209
     "[| F : A co A';  G : B co B' |]  
paulson@13792
   210
      ==> F Join G : (A Int B) co (A' Un B')"
paulson@13792
   211
by (simp, blast intro: constrains_weaken)
paulson@13792
   212
paulson@13792
   213
(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
paulson@13792
   214
lemma JN_constrains_weaken:
paulson@13792
   215
     "[| ALL i:I. F i : A i co A' i;  i: I |]  
paulson@13792
   216
      ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)"
paulson@13792
   217
apply (simp (no_asm_simp) add: JN_constrains)
paulson@13792
   218
apply (blast intro: constrains_weaken)
paulson@13792
   219
done
paulson@13792
   220
paulson@13792
   221
lemma JN_stable: "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"
paulson@13792
   222
by (simp add: stable_def constrains_def JOIN_def)
paulson@13792
   223
paulson@13792
   224
lemma invariant_JN_I:
paulson@13792
   225
     "[| !!i. i:I ==> F i : invariant A;  i : I |]   
paulson@13792
   226
       ==> (JN i:I. F i) : invariant A"
paulson@13792
   227
by (simp add: invariant_def JN_stable, blast)
paulson@13792
   228
paulson@13792
   229
lemma Join_stable [simp]:
paulson@13792
   230
     "(F Join G : stable A) =  
paulson@13792
   231
      (F : stable A & G : stable A)"
paulson@13792
   232
by (simp add: stable_def)
paulson@13792
   233
paulson@13792
   234
lemma Join_increasing [simp]:
paulson@13792
   235
     "(F Join G : increasing f) =  
paulson@13792
   236
      (F : increasing f & G : increasing f)"
paulson@13792
   237
by (simp add: increasing_def Join_stable, blast)
paulson@13792
   238
paulson@13792
   239
lemma invariant_JoinI:
paulson@13792
   240
     "[| F : invariant A; G : invariant A |]   
paulson@13792
   241
      ==> F Join G : invariant A"
paulson@13792
   242
by (simp add: invariant_def, blast)
paulson@13792
   243
paulson@13792
   244
lemma FP_JN: "FP (JN i:I. F i) = (INT i:I. FP (F i))"
paulson@13792
   245
by (simp add: FP_def JN_stable INTER_def)
paulson@13792
   246
paulson@13792
   247
paulson@13798
   248
subsection{*Progress: transient, ensures*}
paulson@13792
   249
paulson@13792
   250
lemma JN_transient:
paulson@13792
   251
     "i : I ==>  
paulson@13792
   252
    (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"
paulson@13792
   253
by (auto simp add: transient_def JOIN_def)
paulson@13792
   254
paulson@13792
   255
lemma Join_transient [simp]:
paulson@13792
   256
     "F Join G : transient A =  
paulson@13792
   257
      (F : transient A | G : transient A)"
paulson@13792
   258
by (auto simp add: bex_Un transient_def Join_def)
paulson@13792
   259
paulson@13792
   260
lemma Join_transient_I1: "F : transient A ==> F Join G : transient A"
paulson@13792
   261
by (simp add: Join_transient)
paulson@13792
   262
paulson@13792
   263
lemma Join_transient_I2: "G : transient A ==> F Join G : transient A"
paulson@13792
   264
by (simp add: Join_transient)
paulson@13792
   265
paulson@13792
   266
(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
paulson@13792
   267
lemma JN_ensures:
paulson@13792
   268
     "i : I ==>  
paulson@13792
   269
      (JN i:I. F i) : A ensures B =  
paulson@13792
   270
      ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))"
paulson@13792
   271
by (auto simp add: ensures_def JN_constrains JN_transient)
paulson@13792
   272
paulson@13792
   273
lemma Join_ensures: 
paulson@13792
   274
     "F Join G : A ensures B =      
paulson@13792
   275
      (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) &  
paulson@13792
   276
       (F : transient (A-B) | G : transient (A-B)))"
paulson@13792
   277
by (auto simp add: ensures_def Join_transient)
paulson@13792
   278
paulson@13792
   279
lemma stable_Join_constrains: 
paulson@13792
   280
    "[| F : stable A;  G : A co A' |]  
paulson@13792
   281
     ==> F Join G : A co A'"
paulson@13792
   282
apply (unfold stable_def constrains_def Join_def)
paulson@13792
   283
apply (simp add: ball_Un, blast)
paulson@13792
   284
done
paulson@13792
   285
paulson@13792
   286
(*Premise for G cannot use Always because  F: Stable A  is weaker than
paulson@13792
   287
  G : stable A *)
paulson@13792
   288
lemma stable_Join_Always1:
paulson@13792
   289
     "[| F : stable A;  G : invariant A |] ==> F Join G : Always A"
paulson@13792
   290
apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
paulson@13792
   291
apply (force intro: stable_Int)
paulson@13792
   292
done
paulson@13792
   293
paulson@13792
   294
(*As above, but exchanging the roles of F and G*)
paulson@13792
   295
lemma stable_Join_Always2:
paulson@13792
   296
     "[| F : invariant A;  G : stable A |] ==> F Join G : Always A"
paulson@13792
   297
apply (subst Join_commute)
paulson@13792
   298
apply (blast intro: stable_Join_Always1)
paulson@13792
   299
done
paulson@13792
   300
paulson@13792
   301
lemma stable_Join_ensures1:
paulson@13792
   302
     "[| F : stable A;  G : A ensures B |] ==> F Join G : A ensures B"
paulson@13792
   303
apply (simp (no_asm_simp) add: Join_ensures)
paulson@13792
   304
apply (simp add: stable_def ensures_def)
paulson@13792
   305
apply (erule constrains_weaken, auto)
paulson@13792
   306
done
paulson@13792
   307
paulson@13792
   308
(*As above, but exchanging the roles of F and G*)
paulson@13792
   309
lemma stable_Join_ensures2:
paulson@13792
   310
     "[| F : A ensures B;  G : stable A |] ==> F Join G : A ensures B"
paulson@13792
   311
apply (subst Join_commute)
paulson@13792
   312
apply (blast intro: stable_Join_ensures1)
paulson@13792
   313
done
paulson@13792
   314
paulson@13792
   315
paulson@13798
   316
subsection{*the ok and OK relations*}
paulson@13792
   317
paulson@13792
   318
lemma ok_SKIP1 [iff]: "SKIP ok F"
paulson@13792
   319
by (auto simp add: ok_def)
paulson@13792
   320
paulson@13792
   321
lemma ok_SKIP2 [iff]: "F ok SKIP"
paulson@13792
   322
by (auto simp add: ok_def)
paulson@13792
   323
paulson@13792
   324
lemma ok_Join_commute:
paulson@13792
   325
     "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))"
paulson@13792
   326
by (auto simp add: ok_def)
paulson@13792
   327
paulson@13792
   328
lemma ok_commute: "(F ok G) = (G ok F)"
paulson@13792
   329
by (auto simp add: ok_def)
paulson@13792
   330
paulson@13792
   331
lemmas ok_sym = ok_commute [THEN iffD1, standard]
paulson@13792
   332
paulson@13792
   333
lemma ok_iff_OK:
paulson@13792
   334
     "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"
paulson@13792
   335
by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb all_conj_distrib eq_commute, blast)
paulson@13792
   336
paulson@13792
   337
lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)"
paulson@13792
   338
by (auto simp add: ok_def)
paulson@13792
   339
paulson@13792
   340
lemma ok_Join_iff2 [iff]: "(G Join H) ok F = (G ok F & H ok F)"
paulson@13792
   341
by (auto simp add: ok_def)
paulson@13792
   342
paulson@13792
   343
(*useful?  Not with the previous two around*)
paulson@13792
   344
lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
paulson@13792
   345
by (auto simp add: ok_def)
paulson@13792
   346
paulson@13792
   347
lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (ALL i:I. F ok G i)"
paulson@13792
   348
by (auto simp add: ok_def)
paulson@13792
   349
paulson@13792
   350
lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F =  (ALL i:I. G i ok F)"
paulson@13792
   351
by (auto simp add: ok_def)
paulson@13792
   352
paulson@13792
   353
lemma OK_iff_ok: "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"
paulson@13792
   354
by (auto simp add: ok_def OK_def)
paulson@13792
   355
paulson@13792
   356
lemma OK_imp_ok: "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"
paulson@13792
   357
by (auto simp add: OK_iff_ok)
paulson@13792
   358
paulson@13792
   359
paulson@13798
   360
subsection{*Allowed*}
paulson@13792
   361
paulson@13792
   362
lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
paulson@13792
   363
by (auto simp add: Allowed_def)
paulson@13792
   364
paulson@13792
   365
lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F Int Allowed G"
paulson@13792
   366
by (auto simp add: Allowed_def)
paulson@13792
   367
paulson@13792
   368
lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (INT i:I. Allowed (F i))"
paulson@13792
   369
by (auto simp add: Allowed_def)
paulson@13792
   370
paulson@13792
   371
lemma ok_iff_Allowed: "F ok G = (F : Allowed G & G : Allowed F)"
paulson@13792
   372
by (simp add: ok_def Allowed_def)
paulson@13792
   373
paulson@13792
   374
lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"
paulson@13792
   375
by (auto simp add: OK_iff_ok ok_iff_Allowed)
paulson@13792
   376
paulson@13798
   377
subsection{*@{text safety_prop}, for reasoning about
paulson@13798
   378
 given instances of "ok"*}
paulson@13792
   379
paulson@13792
   380
lemma safety_prop_Acts_iff:
paulson@13792
   381
     "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)"
paulson@13792
   382
by (auto simp add: safety_prop_def)
paulson@13792
   383
paulson@13792
   384
lemma safety_prop_AllowedActs_iff_Allowed:
paulson@13792
   385
     "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)"
paulson@13792
   386
by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
paulson@13792
   387
paulson@13792
   388
lemma Allowed_eq:
paulson@13792
   389
     "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"
paulson@13792
   390
by (simp add: Allowed_def safety_prop_Acts_iff)
paulson@13792
   391
paulson@13792
   392
lemma def_prg_Allowed:
paulson@13792
   393
     "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]  
paulson@13792
   394
      ==> Allowed F = X"
paulson@13792
   395
by (simp add: Allowed_eq)
paulson@13792
   396
paulson@13792
   397
(*For safety_prop to hold, the property must be satisfiable!*)
paulson@13792
   398
lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A <= B)"
paulson@13792
   399
by (simp add: safety_prop_def constrains_def, blast)
paulson@13792
   400
paulson@13792
   401
lemma safety_prop_stable [iff]: "safety_prop (stable A)"
paulson@13792
   402
by (simp add: stable_def)
paulson@13792
   403
paulson@13792
   404
lemma safety_prop_Int [simp]:
paulson@13792
   405
     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)"
paulson@13792
   406
by (simp add: safety_prop_def, blast)
paulson@13792
   407
paulson@13792
   408
lemma safety_prop_INTER1 [simp]:
paulson@13792
   409
     "(!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)"
paulson@13792
   410
by (auto simp add: safety_prop_def, blast)
paulson@13792
   411
							       
paulson@13792
   412
lemma safety_prop_INTER [simp]:
paulson@13792
   413
     "(!!i. i:I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)"
paulson@13792
   414
by (auto simp add: safety_prop_def, blast)
paulson@13792
   415
paulson@13792
   416
lemma def_UNION_ok_iff:
paulson@13792
   417
     "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]  
paulson@13792
   418
      ==> F ok G = (G : X & acts <= AllowedActs G)"
paulson@13792
   419
by (auto simp add: ok_def safety_prop_Acts_iff)
paulson@9685
   420
paulson@5252
   421
end