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