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