src/ZF/UNITY/Union.thy
author wenzelm
Tue Mar 02 23:59:54 2010 +0100 (2010-03-02)
changeset 35427 ad039d29e01c
parent 35112 ff6f60e6ab85
child 45602 2a858377c3d2
permissions -rw-r--r--
proper (type_)notation;
paulson@11479
     1
(*  Title:      ZF/UNITY/Union.thy
paulson@11479
     2
    Author:     Sidi O Ehmety, Computer Laboratory
paulson@11479
     3
    Copyright   2001  University of Cambridge
paulson@11479
     4
paulson@11479
     5
Unions of programs
paulson@11479
     6
paulson@11479
     7
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
paulson@11479
     8
paulson@11479
     9
Theory ported form HOL..
paulson@11479
    10
paulson@11479
    11
*)
paulson@11479
    12
wenzelm@24893
    13
theory Union imports SubstAx FP
wenzelm@24893
    14
begin
paulson@14092
    15
wenzelm@24893
    16
definition
paulson@14092
    17
  (*FIXME: conjoin Init(F) Int Init(G) \<noteq> 0 *) 
wenzelm@24893
    18
  ok :: "[i, i] => o"     (infixl "ok" 65)  where
paulson@14092
    19
    "F ok G == Acts(F) \<subseteq> AllowedActs(G) &
paulson@14092
    20
               Acts(G) \<subseteq> AllowedActs(F)"
paulson@11479
    21
wenzelm@24893
    22
definition
paulson@14092
    23
  (*FIXME: conjoin (\<Inter>i \<in> I. Init(F(i))) \<noteq> 0 *) 
wenzelm@24893
    24
  OK  :: "[i, i=>i] => o"  where
paulson@14092
    25
    "OK(I,F) == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts(F(i)) \<subseteq> AllowedActs(F(j)))"
paulson@11479
    26
wenzelm@24893
    27
definition
wenzelm@24893
    28
  JOIN  :: "[i, i=>i] => i"  where
paulson@11479
    29
  "JOIN(I,F) == if I = 0 then SKIP else
paulson@14092
    30
                 mk_program(\<Inter>i \<in> I. Init(F(i)), \<Union>i \<in> I. Acts(F(i)),
paulson@14092
    31
                 \<Inter>i \<in> I. AllowedActs(F(i)))"
paulson@11479
    32
wenzelm@24893
    33
definition
wenzelm@24893
    34
  Join :: "[i, i] => i"    (infixl "Join" 65)  where
paulson@11479
    35
  "F Join G == mk_program (Init(F) Int Init(G), Acts(F) Un Acts(G),
wenzelm@32960
    36
                                AllowedActs(F) Int AllowedActs(G))"
wenzelm@24893
    37
definition
paulson@11479
    38
  (*Characterizes safety properties.  Used with specifying AllowedActs*)
wenzelm@24893
    39
  safety_prop :: "i => o"  where
paulson@14092
    40
  "safety_prop(X) == X\<subseteq>program &
paulson@14092
    41
      SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
paulson@11479
    42
  
wenzelm@35427
    43
notation (xsymbols)
wenzelm@35427
    44
  SKIP  ("\<bottom>") and
wenzelm@35427
    45
  Join  (infixl "\<squnion>" 65)
wenzelm@35427
    46
paulson@11479
    47
syntax
wenzelm@35112
    48
  "_JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
wenzelm@35112
    49
  "_JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
wenzelm@35427
    50
syntax (xsymbols)
wenzelm@35427
    51
  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
wenzelm@35427
    52
  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
paulson@11479
    53
paulson@11479
    54
translations
wenzelm@24893
    55
  "JN x:A. B"   == "CONST JOIN(A, (%x. B))"
paulson@11479
    56
  "JN x y. B"   == "JN x. JN y. B"
wenzelm@24893
    57
  "JN x. B"     == "CONST JOIN(CONST state,(%x. B))"
paulson@11479
    58
paulson@14092
    59
paulson@14092
    60
subsection{*SKIP*}
paulson@14092
    61
paulson@14092
    62
lemma reachable_SKIP [simp]: "reachable(SKIP) = state"
paulson@14092
    63
by (force elim: reachable.induct intro: reachable.intros)
paulson@14092
    64
paulson@14092
    65
text{*Elimination programify from ok and Join*}
paulson@14092
    66
paulson@14092
    67
lemma ok_programify_left [iff]: "programify(F) ok G <-> F ok G"
paulson@14092
    68
by (simp add: ok_def)
paulson@14092
    69
paulson@14092
    70
lemma ok_programify_right [iff]: "F ok programify(G) <-> F ok G"
paulson@14092
    71
by (simp add: ok_def)
paulson@14092
    72
paulson@14092
    73
lemma Join_programify_left [simp]: "programify(F) Join G = F Join G"
paulson@14092
    74
by (simp add: Join_def)
paulson@14092
    75
paulson@14092
    76
lemma Join_programify_right [simp]: "F Join programify(G) = F Join G"
paulson@14092
    77
by (simp add: Join_def)
paulson@14092
    78
paulson@14092
    79
subsection{*SKIP and safety properties*}
paulson@14092
    80
paulson@14092
    81
lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) <-> (A\<subseteq>B & st_set(A))"
paulson@14092
    82
by (unfold constrains_def st_set_def, auto)
paulson@14092
    83
paulson@14092
    84
lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B)<-> (state Int A\<subseteq>B)"
paulson@14092
    85
by (unfold Constrains_def, auto)
paulson@14092
    86
paulson@14092
    87
lemma SKIP_in_stable [iff]: "SKIP \<in> stable(A) <-> st_set(A)"
paulson@14092
    88
by (auto simp add: stable_def)
paulson@14092
    89
paulson@14092
    90
lemma SKIP_in_Stable [iff]: "SKIP \<in> Stable(A)"
paulson@14092
    91
by (unfold Stable_def, auto)
paulson@14092
    92
paulson@14092
    93
subsection{*Join and JOIN types*}
paulson@14092
    94
paulson@14092
    95
lemma Join_in_program [iff,TC]: "F Join G \<in> program"
paulson@14092
    96
by (unfold Join_def, auto)
paulson@14092
    97
paulson@14092
    98
lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \<in> program"
paulson@14092
    99
by (unfold JOIN_def, auto)
paulson@14092
   100
paulson@14092
   101
subsection{*Init, Acts, and AllowedActs of Join and JOIN*}
paulson@14092
   102
lemma Init_Join [simp]: "Init(F Join G) = Init(F) Int Init(G)"
paulson@14092
   103
by (simp add: Int_assoc Join_def)
paulson@14092
   104
paulson@14092
   105
lemma Acts_Join [simp]: "Acts(F Join G) = Acts(F) Un Acts(G)"
paulson@14092
   106
by (simp add: Int_Un_distrib2 cons_absorb Join_def)
paulson@14092
   107
paulson@14092
   108
lemma AllowedActs_Join [simp]: "AllowedActs(F Join G) =  
paulson@14092
   109
  AllowedActs(F) Int AllowedActs(G)"
paulson@14092
   110
apply (simp add: Int_assoc cons_absorb Join_def)
paulson@14092
   111
done
paulson@14092
   112
paulson@14092
   113
subsection{*Join's algebraic laws*}
paulson@14092
   114
paulson@14092
   115
lemma Join_commute: "F Join G = G Join F"
paulson@14092
   116
by (simp add: Join_def Un_commute Int_commute)
paulson@14092
   117
paulson@14092
   118
lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)"
paulson@14092
   119
apply (simp add: Join_def Int_Un_distrib2 cons_absorb)
paulson@14092
   120
apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb)
paulson@14092
   121
done
paulson@14092
   122
paulson@14092
   123
lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)"
paulson@14092
   124
by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2)
paulson@14092
   125
paulson@14092
   126
subsection{*Needed below*}
paulson@14092
   127
lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)"
paulson@14092
   128
by auto
paulson@14092
   129
paulson@14092
   130
lemma Join_SKIP_left [simp]: "SKIP Join F = programify(F)"
paulson@14092
   131
apply (unfold Join_def SKIP_def)
paulson@14092
   132
apply (auto simp add: Int_absorb cons_eq)
paulson@14092
   133
done
paulson@14092
   134
paulson@14092
   135
lemma Join_SKIP_right [simp]: "F Join SKIP =  programify(F)"
paulson@14092
   136
apply (subst Join_commute)
paulson@14092
   137
apply (simp add: Join_SKIP_left)
paulson@14092
   138
done
paulson@14092
   139
paulson@14092
   140
lemma Join_absorb [simp]: "F Join F = programify(F)"
paulson@14092
   141
by (rule program_equalityI, auto)
paulson@14092
   142
paulson@14092
   143
lemma Join_left_absorb: "F Join (F Join G) = F Join G"
paulson@14092
   144
by (simp add: Join_assoc [symmetric])
paulson@14092
   145
paulson@14092
   146
subsection{*Join is an AC-operator*}
paulson@14092
   147
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
paulson@14092
   148
paulson@14092
   149
subsection{*Eliminating programify form JN and OK expressions*}
paulson@14092
   150
paulson@14092
   151
lemma OK_programify [iff]: "OK(I, %x. programify(F(x))) <-> OK(I, F)"
paulson@14092
   152
by (simp add: OK_def)
paulson@14092
   153
paulson@14092
   154
lemma JN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)"
paulson@14092
   155
by (simp add: JOIN_def)
paulson@14092
   156
paulson@14092
   157
paulson@14092
   158
subsection{*JN*}
paulson@14092
   159
paulson@14092
   160
lemma JN_empty [simp]: "JOIN(0, F) = SKIP"
paulson@14092
   161
by (unfold JOIN_def, auto)
paulson@14092
   162
paulson@14092
   163
lemma Init_JN [simp]:
paulson@14092
   164
     "Init(\<Squnion>i \<in> I. F(i)) = (if I=0 then state else (\<Inter>i \<in> I. Init(F(i))))"
paulson@14095
   165
by (simp add: JOIN_def INT_extend_simps del: INT_simps)
paulson@14092
   166
paulson@14092
   167
lemma Acts_JN [simp]: 
paulson@14092
   168
     "Acts(JOIN(I,F)) = cons(id(state), \<Union>i \<in> I.  Acts(F(i)))"
paulson@14092
   169
apply (unfold JOIN_def)
paulson@14092
   170
apply (auto simp del: INT_simps UN_simps)
paulson@14092
   171
apply (rule equalityI)
paulson@14092
   172
apply (auto dest: Acts_type [THEN subsetD])
paulson@14092
   173
done
paulson@14092
   174
paulson@14092
   175
lemma AllowedActs_JN [simp]: 
paulson@14092
   176
     "AllowedActs(\<Squnion>i \<in> I. F(i)) = 
paulson@14092
   177
      (if I=0 then Pow(state*state) else (\<Inter>i \<in> I. AllowedActs(F(i))))"
paulson@14092
   178
apply (unfold JOIN_def, auto)
paulson@14092
   179
apply (rule equalityI)
paulson@14092
   180
apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD])
paulson@14092
   181
done
paulson@14092
   182
paulson@14092
   183
lemma JN_cons [simp]: "(\<Squnion>i \<in> cons(a,I). F(i)) = F(a) Join (\<Squnion>i \<in> I. F(i))"
paulson@14092
   184
by (rule program_equalityI, auto)
paulson@14092
   185
paulson@14092
   186
lemma JN_cong [cong]:
paulson@14092
   187
    "[| I=J;  !!i. i \<in> J ==> F(i) = G(i) |] ==>  
paulson@14092
   188
     (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> J. G(i))"
paulson@14092
   189
by (simp add: JOIN_def)
paulson@14092
   190
paulson@14092
   191
paulson@14092
   192
paulson@14092
   193
subsection{*JN laws*}
paulson@14092
   194
lemma JN_absorb: "k \<in> I ==>F(k) Join (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> I. F(i))"
paulson@14092
   195
apply (subst JN_cons [symmetric])
paulson@14092
   196
apply (auto simp add: cons_absorb)
paulson@14092
   197
done
paulson@14092
   198
paulson@14092
   199
lemma JN_Un: "(\<Squnion>i \<in> I Un J. F(i)) = ((\<Squnion>i \<in> I. F(i)) Join (\<Squnion>i \<in> J. F(i)))"
paulson@14092
   200
apply (rule program_equalityI)
paulson@14092
   201
apply (simp_all add: UN_Un INT_Un)
paulson@14092
   202
apply (simp_all del: INT_simps add: INT_extend_simps, blast)
paulson@14092
   203
done
paulson@14092
   204
paulson@14092
   205
lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I=0 then SKIP else programify(c))"
paulson@14092
   206
by (rule program_equalityI, auto)
paulson@14092
   207
paulson@14092
   208
lemma JN_Join_distrib:
paulson@14092
   209
     "(\<Squnion>i \<in> I. F(i) Join G(i)) = (\<Squnion>i \<in> I. F(i))  Join  (\<Squnion>i \<in> I. G(i))"
paulson@14092
   210
apply (rule program_equalityI)
paulson@14095
   211
apply (simp_all add: INT_Int_distrib, blast) 
paulson@14092
   212
done
paulson@14092
   213
paulson@14092
   214
lemma JN_Join_miniscope: "(\<Squnion>i \<in> I. F(i) Join G) = ((\<Squnion>i \<in> I. F(i) Join G))"
paulson@14092
   215
by (simp add: JN_Join_distrib JN_constant)
paulson@14092
   216
paulson@14092
   217
text{*Used to prove guarantees_JN_I*}
paulson@14092
   218
lemma JN_Join_diff: "i \<in> I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)"
paulson@14092
   219
apply (rule program_equalityI)
paulson@14092
   220
apply (auto elim!: not_emptyE)
paulson@14092
   221
done
paulson@14092
   222
paulson@14092
   223
subsection{*Safety: co, stable, FP*}
paulson@14092
   224
paulson@14092
   225
paulson@14092
   226
(*Fails if I=0 because it collapses to SKIP \<in> A co B, i.e. to A\<subseteq>B.  So an
paulson@14092
   227
  alternative precondition is A\<subseteq>B, but most proofs using this rule require
paulson@14092
   228
  I to be nonempty for other reasons anyway.*)
paulson@14092
   229
paulson@14092
   230
lemma JN_constrains: 
paulson@14092
   231
 "i \<in> I==>(\<Squnion>i \<in> I. F(i)) \<in> A co B <-> (\<forall>i \<in> I. programify(F(i)) \<in> A co B)"
paulson@14092
   232
paulson@14092
   233
apply (unfold constrains_def JOIN_def st_set_def, auto)
paulson@14092
   234
prefer 2 apply blast
paulson@14092
   235
apply (rename_tac j act y z)
paulson@14092
   236
apply (cut_tac F = "F (j) " in Acts_type)
paulson@14092
   237
apply (drule_tac x = act in bspec, auto)
paulson@14092
   238
done
paulson@14092
   239
paulson@14092
   240
lemma Join_constrains [iff]:
paulson@14092
   241
     "(F Join G \<in> A co B) <-> (programify(F) \<in> A co B & programify(G) \<in> A co B)"
paulson@14092
   242
by (auto simp add: constrains_def)
paulson@14092
   243
paulson@14092
   244
lemma Join_unless [iff]:
paulson@14092
   245
     "(F Join G \<in> A unless B) <->  
paulson@14092
   246
    (programify(F) \<in> A unless B & programify(G) \<in> A unless B)"
paulson@14092
   247
by (simp add: Join_constrains unless_def)
paulson@14092
   248
paulson@14092
   249
paulson@14092
   250
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
paulson@14092
   251
  reachable (F Join G) could be much bigger than reachable F, reachable G
paulson@14092
   252
*)
paulson@14092
   253
paulson@14092
   254
lemma Join_constrains_weaken:
paulson@14092
   255
     "[| F \<in> A co A';  G \<in> B co B' |]  
paulson@14092
   256
      ==> F Join G \<in> (A Int B) co (A' Un B')"
paulson@14092
   257
apply (subgoal_tac "st_set (A) & st_set (B) & F \<in> program & G \<in> program")
paulson@14092
   258
prefer 2 apply (blast dest: constrainsD2, simp)
paulson@14092
   259
apply (blast intro: constrains_weaken)
paulson@14092
   260
done
paulson@14092
   261
paulson@14092
   262
(*If I=0, it degenerates to SKIP \<in> state co 0, which is false.*)
paulson@14092
   263
lemma JN_constrains_weaken:
paulson@14092
   264
  assumes major: "(!!i. i \<in> I ==> F(i) \<in> A(i) co A'(i))"
paulson@14092
   265
      and minor: "i \<in> I"
paulson@14092
   266
  shows "(\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))"
paulson@14092
   267
apply (cut_tac minor)
paulson@14092
   268
apply (simp (no_asm_simp) add: JN_constrains)
paulson@14092
   269
apply clarify
paulson@14092
   270
apply (rename_tac "j")
paulson@14092
   271
apply (frule_tac i = j in major)
paulson@14092
   272
apply (frule constrainsD2, simp)
paulson@14092
   273
apply (blast intro: constrains_weaken)
paulson@14092
   274
done
paulson@14092
   275
paulson@14092
   276
lemma JN_stable:
paulson@14092
   277
     "(\<Squnion>i \<in> I. F(i)) \<in>  stable(A) <-> ((\<forall>i \<in> I. programify(F(i)) \<in> stable(A)) & st_set(A))"
paulson@14092
   278
apply (auto simp add: stable_def constrains_def JOIN_def)
paulson@14092
   279
apply (cut_tac F = "F (i) " in Acts_type)
paulson@14092
   280
apply (drule_tac x = act in bspec, auto)
paulson@14092
   281
done
paulson@14092
   282
paulson@14092
   283
lemma initially_JN_I: 
paulson@14092
   284
  assumes major: "(!!i. i \<in> I ==>F(i) \<in> initially(A))"
paulson@14092
   285
      and minor: "i \<in> I"
paulson@14092
   286
  shows  "(\<Squnion>i \<in> I. F(i)) \<in> initially(A)"
paulson@14092
   287
apply (cut_tac minor)
paulson@14092
   288
apply (auto elim!: not_emptyE simp add: Inter_iff initially_def) 
paulson@14092
   289
apply (frule_tac i = x in major)
paulson@14092
   290
apply (auto simp add: initially_def) 
paulson@14092
   291
done
paulson@14092
   292
paulson@14092
   293
lemma invariant_JN_I: 
paulson@14092
   294
  assumes major: "(!!i. i \<in> I ==> F(i) \<in> invariant(A))"
paulson@14092
   295
      and minor: "i \<in> I"
paulson@14092
   296
  shows "(\<Squnion>i \<in> I. F(i)) \<in> invariant(A)"
paulson@14092
   297
apply (cut_tac minor)
paulson@14092
   298
apply (auto intro!: initially_JN_I dest: major simp add: invariant_def JN_stable)
paulson@14092
   299
apply (erule_tac V = "i \<in> I" in thin_rl)
paulson@14092
   300
apply (frule major)
paulson@14092
   301
apply (drule_tac [2] major)
paulson@14092
   302
apply (auto simp add: invariant_def)
paulson@14092
   303
apply (frule stableD2, force)+
paulson@14092
   304
done
paulson@14092
   305
paulson@14092
   306
lemma Join_stable [iff]:
paulson@14092
   307
     " (F Join G \<in> stable(A)) <->   
paulson@14092
   308
      (programify(F) \<in> stable(A) & programify(G) \<in>  stable(A))"
paulson@14092
   309
by (simp add: stable_def)
paulson@14092
   310
paulson@14092
   311
lemma initially_JoinI [intro!]:
paulson@14092
   312
     "[| F \<in> initially(A); G \<in> initially(A) |] ==> F Join G \<in> initially(A)"
paulson@14092
   313
by (unfold initially_def, auto)
paulson@14092
   314
paulson@14092
   315
lemma invariant_JoinI:
paulson@14092
   316
     "[| F \<in> invariant(A); G \<in> invariant(A) |]   
paulson@14092
   317
      ==> F Join G \<in> invariant(A)"
paulson@14092
   318
apply (subgoal_tac "F \<in> program&G \<in> program")
paulson@14092
   319
prefer 2 apply (blast dest: invariantD2)
paulson@14092
   320
apply (simp add: invariant_def)
paulson@14092
   321
apply (auto intro: Join_in_program)
paulson@14092
   322
done
paulson@14092
   323
paulson@14092
   324
paulson@14092
   325
(* Fails if I=0 because \<Inter>i \<in> 0. A(i) = 0 *)
paulson@14092
   326
lemma FP_JN: "i \<in> I ==> FP(\<Squnion>i \<in> I. F(i)) = (\<Inter>i \<in> I. FP (programify(F(i))))"
paulson@14092
   327
by (auto simp add: FP_def Inter_def st_set_def JN_stable)
paulson@14092
   328
paulson@14092
   329
subsection{*Progress: transient, ensures*}
paulson@14092
   330
paulson@14092
   331
lemma JN_transient:
paulson@14092
   332
     "i \<in> I ==> 
paulson@14092
   333
      (\<Squnion>i \<in> I. F(i)) \<in> transient(A) <-> (\<exists>i \<in> I. programify(F(i)) \<in> transient(A))"
paulson@14092
   334
apply (auto simp add: transient_def JOIN_def)
paulson@14092
   335
apply (unfold st_set_def)
paulson@14092
   336
apply (drule_tac [2] x = act in bspec)
paulson@14092
   337
apply (auto dest: Acts_type [THEN subsetD])
paulson@14092
   338
done
paulson@14092
   339
paulson@14092
   340
lemma Join_transient [iff]:
paulson@14092
   341
     "F Join G \<in> transient(A) <->  
paulson@14092
   342
      (programify(F) \<in> transient(A) | programify(G) \<in> transient(A))"
paulson@14092
   343
apply (auto simp add: transient_def Join_def Int_Un_distrib2)
paulson@14092
   344
done
paulson@14092
   345
paulson@14092
   346
lemma Join_transient_I1: "F \<in> transient(A) ==> F Join G \<in> transient(A)"
paulson@14092
   347
by (simp add: Join_transient transientD2)
paulson@14092
   348
paulson@14092
   349
paulson@14092
   350
lemma Join_transient_I2: "G \<in> transient(A) ==> F Join G \<in> transient(A)"
paulson@14092
   351
by (simp add: Join_transient transientD2)
paulson@14092
   352
paulson@14092
   353
(*If I=0 it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A\<subseteq>B) *)
paulson@14092
   354
lemma JN_ensures:
paulson@14092
   355
     "i \<in> I ==>  
paulson@14092
   356
      (\<Squnion>i \<in> I. F(i)) \<in> A ensures B <->  
paulson@14092
   357
      ((\<forall>i \<in> I. programify(F(i)) \<in> (A-B) co (A Un B)) &   
paulson@14092
   358
      (\<exists>i \<in> I. programify(F(i)) \<in> A ensures B))"
paulson@14092
   359
by (auto simp add: ensures_def JN_constrains JN_transient)
paulson@14092
   360
paulson@14092
   361
paulson@14092
   362
lemma Join_ensures: 
paulson@14092
   363
     "F Join G \<in> A ensures B  <->      
paulson@14092
   364
      (programify(F) \<in> (A-B) co (A Un B) & programify(G) \<in> (A-B) co (A Un B) &  
paulson@14092
   365
       (programify(F) \<in>  transient (A-B) | programify(G) \<in> transient (A-B)))"
paulson@14092
   366
paulson@14092
   367
apply (unfold ensures_def)
paulson@14092
   368
apply (auto simp add: Join_transient)
paulson@14092
   369
done
paulson@14092
   370
paulson@14092
   371
lemma stable_Join_constrains: 
paulson@14092
   372
    "[| F \<in> stable(A);  G \<in> A co A' |]  
paulson@14092
   373
     ==> F Join G \<in> A co A'"
paulson@14092
   374
apply (unfold stable_def constrains_def Join_def st_set_def)
paulson@14092
   375
apply (cut_tac F = F in Acts_type)
paulson@14092
   376
apply (cut_tac F = G in Acts_type, force) 
paulson@14092
   377
done
paulson@14092
   378
paulson@14092
   379
(*Premise for G cannot use Always because  F \<in> Stable A  is
paulson@14092
   380
   weaker than G \<in> stable A *)
paulson@14092
   381
lemma stable_Join_Always1:
paulson@14092
   382
     "[| F \<in> stable(A);  G \<in> invariant(A) |] ==> F Join G \<in> Always(A)"
paulson@14092
   383
apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ")
paulson@14092
   384
prefer 2 apply (blast dest: invariantD2 stableD2)
paulson@14092
   385
apply (simp add: Always_def invariant_def initially_def Stable_eq_stable)
paulson@14092
   386
apply (force intro: stable_Int)
paulson@14092
   387
done
paulson@14092
   388
paulson@14092
   389
(*As above, but exchanging the roles of F and G*)
paulson@14092
   390
lemma stable_Join_Always2:
paulson@14092
   391
     "[| F \<in> invariant(A);  G \<in> stable(A) |] ==> F Join G \<in> Always(A)"
paulson@14092
   392
apply (subst Join_commute)
paulson@14092
   393
apply (blast intro: stable_Join_Always1)
paulson@14092
   394
done
paulson@14092
   395
paulson@14092
   396
paulson@14092
   397
paulson@14092
   398
lemma stable_Join_ensures1:
paulson@14092
   399
     "[| F \<in> stable(A);  G \<in> A ensures B |] ==> F Join G \<in> A ensures B"
paulson@14092
   400
apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ")
paulson@14092
   401
prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD])
paulson@14092
   402
apply (simp (no_asm_simp) add: Join_ensures)
paulson@14092
   403
apply (simp add: stable_def ensures_def)
paulson@14092
   404
apply (erule constrains_weaken, auto)
paulson@14092
   405
done
paulson@14092
   406
paulson@14092
   407
paulson@14092
   408
(*As above, but exchanging the roles of F and G*)
paulson@14092
   409
lemma stable_Join_ensures2:
paulson@14092
   410
     "[| F \<in> A ensures B;  G \<in> stable(A) |] ==> F Join G \<in> A ensures B"
paulson@14092
   411
apply (subst Join_commute)
paulson@14092
   412
apply (blast intro: stable_Join_ensures1)
paulson@14092
   413
done
paulson@14092
   414
paulson@14092
   415
subsection{*The ok and OK relations*}
paulson@14092
   416
paulson@14092
   417
lemma ok_SKIP1 [iff]: "SKIP ok F"
paulson@14092
   418
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)
paulson@14092
   419
paulson@14092
   420
lemma ok_SKIP2 [iff]: "F ok SKIP"
paulson@14092
   421
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)
paulson@14092
   422
paulson@14092
   423
lemma ok_Join_commute:
paulson@14092
   424
     "(F ok G & (F Join G) ok H) <-> (G ok H & F ok (G Join H))"
paulson@14092
   425
by (auto simp add: ok_def)
paulson@14092
   426
paulson@14092
   427
lemma ok_commute: "(F ok G) <->(G ok F)"
paulson@14092
   428
by (auto simp add: ok_def)
paulson@14092
   429
paulson@14092
   430
lemmas ok_sym = ok_commute [THEN iffD1, standard]
paulson@14092
   431
paulson@14092
   432
lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)"
paulson@14092
   433
by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb
paulson@14092
   434
                 Int_Un_distrib2 Ball_def,  safe, force+)
paulson@14092
   435
paulson@14092
   436
lemma ok_Join_iff1 [iff]: "F ok (G Join H) <-> (F ok G & F ok H)"
paulson@14092
   437
by (auto simp add: ok_def)
paulson@14092
   438
paulson@14092
   439
lemma ok_Join_iff2 [iff]: "(G Join H) ok F <-> (G ok F & H ok F)"
paulson@14092
   440
by (auto simp add: ok_def)
paulson@14092
   441
paulson@14092
   442
(*useful?  Not with the previous two around*)
paulson@14092
   443
lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
paulson@14092
   444
by (auto simp add: ok_def)
paulson@14092
   445
paulson@14092
   446
lemma ok_JN_iff1 [iff]: "F ok JOIN(I,G) <-> (\<forall>i \<in> I. F ok G(i))"
paulson@14092
   447
by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def)
paulson@14092
   448
paulson@14092
   449
lemma ok_JN_iff2 [iff]: "JOIN(I,G) ok F   <->  (\<forall>i \<in> I. G(i) ok F)"
paulson@14092
   450
apply (auto elim!: not_emptyE simp add: ok_def)
paulson@14092
   451
apply (blast dest: Acts_type [THEN subsetD])
paulson@14092
   452
done
paulson@14092
   453
paulson@14092
   454
lemma OK_iff_ok: "OK(I,F) <-> (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F(i) ok (F(j)))"
paulson@14092
   455
by (auto simp add: ok_def OK_def)
paulson@14092
   456
paulson@14092
   457
lemma OK_imp_ok: "[| OK(I,F); i \<in> I; j \<in> I; i\<noteq>j|] ==> F(i) ok F(j)"
paulson@14092
   458
by (auto simp add: OK_iff_ok)
paulson@14092
   459
paulson@14092
   460
paulson@14093
   461
lemma OK_0 [iff]: "OK(0,F)"
paulson@14093
   462
by (simp add: OK_def)
paulson@14093
   463
paulson@14093
   464
lemma OK_cons_iff:
paulson@14093
   465
     "OK(cons(i, I), F) <->  
paulson@14093
   466
      (i \<in> I & OK(I, F)) | (i\<notin>I & OK(I, F) & F(i) ok JOIN(I,F))"
paulson@14093
   467
apply (simp add: OK_iff_ok)
paulson@14093
   468
apply (blast intro: ok_sym) 
paulson@14093
   469
done
paulson@14093
   470
paulson@14093
   471
paulson@14092
   472
subsection{*Allowed*}
paulson@14092
   473
paulson@14092
   474
lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program"
paulson@14092
   475
by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def)
paulson@14092
   476
paulson@14092
   477
lemma Allowed_Join [simp]:
paulson@14092
   478
     "Allowed(F Join G) =  
paulson@14092
   479
   Allowed(programify(F)) Int Allowed(programify(G))"
paulson@14092
   480
apply (auto simp add: Allowed_def)
paulson@14092
   481
done
paulson@14092
   482
paulson@14092
   483
lemma Allowed_JN [simp]:
paulson@14092
   484
     "i \<in> I ==>  
paulson@14092
   485
   Allowed(JOIN(I,F)) = (\<Inter>i \<in> I. Allowed(programify(F(i))))"
paulson@14092
   486
apply (auto simp add: Allowed_def, blast)
paulson@14092
   487
done
paulson@14092
   488
paulson@14092
   489
lemma ok_iff_Allowed:
paulson@14092
   490
     "F ok G <-> (programify(F) \<in> Allowed(programify(G)) &  
paulson@14092
   491
   programify(G) \<in> Allowed(programify(F)))"
paulson@14092
   492
by (simp add: ok_def Allowed_def)
paulson@14092
   493
paulson@14092
   494
paulson@14092
   495
lemma OK_iff_Allowed:
paulson@14092
   496
     "OK(I,F) <->  
paulson@14092
   497
  (\<forall>i \<in> I. \<forall>j \<in> I-{i}. programify(F(i)) \<in> Allowed(programify(F(j))))"
paulson@14092
   498
apply (auto simp add: OK_iff_ok ok_iff_Allowed)
paulson@14092
   499
done
paulson@14092
   500
paulson@14092
   501
subsection{*safety_prop, for reasoning about given instances of "ok"*}
paulson@14092
   502
paulson@14092
   503
lemma safety_prop_Acts_iff:
paulson@14092
   504
     "safety_prop(X) ==> (Acts(G) \<subseteq> cons(id(state), (\<Union>F \<in> X. Acts(F)))) <-> (programify(G) \<in> X)"
paulson@14092
   505
apply (simp (no_asm_use) add: safety_prop_def)
paulson@14092
   506
apply clarify
paulson@14092
   507
apply (case_tac "G \<in> program", simp_all, blast, safe)
paulson@14092
   508
prefer 2 apply force
paulson@14092
   509
apply (force simp add: programify_def)
paulson@14092
   510
done
paulson@14092
   511
paulson@14092
   512
lemma safety_prop_AllowedActs_iff_Allowed:
paulson@14092
   513
     "safety_prop(X) ==>  
paulson@14092
   514
  (\<Union>G \<in> X. Acts(G)) \<subseteq> AllowedActs(F) <-> (X \<subseteq> Allowed(programify(F)))"
paulson@14092
   515
apply (simp add: Allowed_def safety_prop_Acts_iff [THEN iff_sym] 
paulson@14092
   516
                 safety_prop_def, blast) 
paulson@14092
   517
done
paulson@14092
   518
paulson@14092
   519
paulson@14092
   520
lemma Allowed_eq:
paulson@14092
   521
     "safety_prop(X) ==> Allowed(mk_program(init, acts, \<Union>F \<in> X. Acts(F))) = X"
paulson@14092
   522
apply (subgoal_tac "cons (id (state), Union (RepFun (X, Acts)) Int Pow (state * state)) = Union (RepFun (X, Acts))")
paulson@14092
   523
apply (rule_tac [2] equalityI)
paulson@14092
   524
  apply (simp del: UN_simps add: Allowed_def safety_prop_Acts_iff safety_prop_def, auto)
paulson@14092
   525
apply (force dest: Acts_type [THEN subsetD] simp add: safety_prop_def)+
paulson@14092
   526
done
paulson@14092
   527
paulson@14092
   528
lemma def_prg_Allowed:
paulson@14092
   529
     "[| F == mk_program (init, acts, \<Union>F \<in> X. Acts(F)); safety_prop(X) |]  
paulson@14092
   530
      ==> Allowed(F) = X"
paulson@14092
   531
by (simp add: Allowed_eq)
paulson@14092
   532
paulson@14092
   533
(*For safety_prop to hold, the property must be satisfiable!*)
paulson@14092
   534
lemma safety_prop_constrains [iff]:
paulson@14092
   535
     "safety_prop(A co B) <-> (A \<subseteq> B & st_set(A))"
paulson@14092
   536
by (simp add: safety_prop_def constrains_def st_set_def, blast)
paulson@14092
   537
paulson@14092
   538
(* To be used with resolution *)
paulson@14092
   539
lemma safety_prop_constrainsI [iff]:
paulson@14092
   540
     "[| A\<subseteq>B; st_set(A) |] ==>safety_prop(A co B)"
paulson@14092
   541
by auto
paulson@14092
   542
paulson@14092
   543
lemma safety_prop_stable [iff]: "safety_prop(stable(A)) <-> st_set(A)"
paulson@14092
   544
by (simp add: stable_def)
paulson@14092
   545
paulson@14092
   546
lemma safety_prop_stableI: "st_set(A) ==> safety_prop(stable(A))"
paulson@14092
   547
by auto
paulson@14092
   548
paulson@14092
   549
lemma safety_prop_Int [simp]:
paulson@14092
   550
     "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X Int Y)"
paulson@14092
   551
apply (simp add: safety_prop_def, safe, blast)
paulson@14092
   552
apply (drule_tac [2] B = "Union (RepFun (X Int Y, Acts))" and C = "Union (RepFun (Y, Acts))" in subset_trans)
paulson@14092
   553
apply (drule_tac B = "Union (RepFun (X Int Y, Acts))" and C = "Union (RepFun (X, Acts))" in subset_trans)
paulson@14092
   554
apply blast+
paulson@14092
   555
done
paulson@14092
   556
paulson@14092
   557
(* If I=0 the conclusion becomes safety_prop(0) which is false *)
paulson@14092
   558
lemma safety_prop_Inter:
paulson@14092
   559
  assumes major: "(!!i. i \<in> I ==>safety_prop(X(i)))"
paulson@14092
   560
      and minor: "i \<in> I"
paulson@14092
   561
  shows "safety_prop(\<Inter>i \<in> I. X(i))"
paulson@14092
   562
apply (simp add: safety_prop_def)
paulson@14092
   563
apply (cut_tac minor, safe)
paulson@14092
   564
apply (simp (no_asm_use) add: Inter_iff)
paulson@14092
   565
apply clarify
paulson@14092
   566
apply (frule major)
paulson@14092
   567
apply (drule_tac [2] i = xa in major)
paulson@14092
   568
apply (frule_tac [4] i = xa in major)
paulson@14092
   569
apply (auto simp add: safety_prop_def)
paulson@14092
   570
apply (drule_tac B = "Union (RepFun (Inter (RepFun (I, X)), Acts))" and C = "Union (RepFun (X (xa), Acts))" in subset_trans)
paulson@14092
   571
apply blast+
paulson@14092
   572
done
paulson@14092
   573
paulson@14092
   574
lemma def_UNION_ok_iff: 
paulson@14092
   575
"[| F == mk_program(init,acts, \<Union>G \<in> X. Acts(G)); safety_prop(X) |]  
paulson@14092
   576
      ==> F ok G <-> (programify(G) \<in> X & acts Int Pow(state*state) \<subseteq> AllowedActs(G))"
paulson@14092
   577
apply (unfold ok_def)
paulson@14092
   578
apply (drule_tac G = G in safety_prop_Acts_iff)
paulson@14092
   579
apply (cut_tac F = G in AllowedActs_type)
paulson@14092
   580
apply (cut_tac F = G in Acts_type, auto)
paulson@14092
   581
done
paulson@14092
   582
paulson@11479
   583
end