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