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