src/HOL/UNITY/UNITY.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 30198 922f944f03b2
child 32960 69916a850301
permissions -rw-r--r--
simplified method setup;
     1 (*  Title:      HOL/UNITY/UNITY
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The basic UNITY theory (revised version, based upon the "co" operator)
     7 
     8 From Misra, "A Logic for Concurrent Programming", 1994
     9 *)
    10 
    11 header {*The Basic UNITY Theory*}
    12 
    13 theory UNITY imports Main begin
    14 
    15 typedef (Program)
    16   'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
    17 		   allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}" 
    18   by blast
    19 
    20 constdefs
    21   Acts :: "'a program => ('a * 'a)set set"
    22     "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
    23 
    24   "constrains" :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
    25     "A co B == {F. \<forall>act \<in> Acts F. act``A \<subseteq> B}"
    26 
    27   unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
    28     "A unless B == (A-B) co (A \<union> B)"
    29 
    30   mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
    31 		   => 'a program"
    32     "mk_program == %(init, acts, allowed).
    33                       Abs_Program (init, insert Id acts, insert Id allowed)"
    34 
    35   Init :: "'a program => 'a set"
    36     "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
    37 
    38   AllowedActs :: "'a program => ('a * 'a)set set"
    39     "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
    40 
    41   Allowed :: "'a program => 'a program set"
    42     "Allowed F == {G. Acts G \<subseteq> AllowedActs F}"
    43 
    44   stable     :: "'a set => 'a program set"
    45     "stable A == A co A"
    46 
    47   strongest_rhs :: "['a program, 'a set] => 'a set"
    48     "strongest_rhs F A == Inter {B. F \<in> A co B}"
    49 
    50   invariant :: "'a set => 'a program set"
    51     "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
    52 
    53   increasing :: "['a => 'b::{order}] => 'a program set"
    54     --{*Polymorphic in both states and the meaning of @{text "\<le>"}*}
    55     "increasing f == \<Inter>z. stable {s. z \<le> f s}"
    56 
    57 
    58 text{*Perhaps HOL shouldn't add this in the first place!*}
    59 declare image_Collect [simp del]
    60 
    61 subsubsection{*The abstract type of programs*}
    62 
    63 lemmas program_typedef =
    64      Rep_Program Rep_Program_inverse Abs_Program_inverse 
    65      Program_def Init_def Acts_def AllowedActs_def mk_program_def
    66 
    67 lemma Id_in_Acts [iff]: "Id \<in> Acts F"
    68 apply (cut_tac x = F in Rep_Program)
    69 apply (auto simp add: program_typedef) 
    70 done
    71 
    72 lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
    73 by (simp add: insert_absorb Id_in_Acts)
    74 
    75 lemma Acts_nonempty [simp]: "Acts F \<noteq> {}"
    76 by auto
    77 
    78 lemma Id_in_AllowedActs [iff]: "Id \<in> AllowedActs F"
    79 apply (cut_tac x = F in Rep_Program)
    80 apply (auto simp add: program_typedef) 
    81 done
    82 
    83 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
    84 by (simp add: insert_absorb Id_in_AllowedActs)
    85 
    86 subsubsection{*Inspectors for type "program"*}
    87 
    88 lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
    89 by (simp add: program_typedef)
    90 
    91 lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
    92 by (simp add: program_typedef)
    93 
    94 lemma AllowedActs_eq [simp]:
    95      "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
    96 by (simp add: program_typedef)
    97 
    98 subsubsection{*Equality for UNITY programs*}
    99 
   100 lemma surjective_mk_program [simp]:
   101      "mk_program (Init F, Acts F, AllowedActs F) = F"
   102 apply (cut_tac x = F in Rep_Program)
   103 apply (auto simp add: program_typedef)
   104 apply (drule_tac f = Abs_Program in arg_cong)+
   105 apply (simp add: program_typedef insert_absorb)
   106 done
   107 
   108 lemma program_equalityI:
   109      "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]  
   110       ==> F = G"
   111 apply (rule_tac t = F in surjective_mk_program [THEN subst])
   112 apply (rule_tac t = G in surjective_mk_program [THEN subst], simp)
   113 done
   114 
   115 lemma program_equalityE:
   116      "[| F = G;  
   117          [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] 
   118          ==> P |] ==> P"
   119 by simp 
   120 
   121 lemma program_equality_iff:
   122      "(F=G) =   
   123       (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)"
   124 by (blast intro: program_equalityI program_equalityE)
   125 
   126 
   127 subsubsection{*co*}
   128 
   129 lemma constrainsI: 
   130     "(!!act s s'. [| act: Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s': A')  
   131      ==> F \<in> A co A'"
   132 by (simp add: constrains_def, blast)
   133 
   134 lemma constrainsD: 
   135     "[| F \<in> A co A'; act: Acts F;  (s,s'): act;  s \<in> A |] ==> s': A'"
   136 by (unfold constrains_def, blast)
   137 
   138 lemma constrains_empty [iff]: "F \<in> {} co B"
   139 by (unfold constrains_def, blast)
   140 
   141 lemma constrains_empty2 [iff]: "(F \<in> A co {}) = (A={})"
   142 by (unfold constrains_def, blast)
   143 
   144 lemma constrains_UNIV [iff]: "(F \<in> UNIV co B) = (B = UNIV)"
   145 by (unfold constrains_def, blast)
   146 
   147 lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
   148 by (unfold constrains_def, blast)
   149 
   150 text{*monotonic in 2nd argument*}
   151 lemma constrains_weaken_R: 
   152     "[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
   153 by (unfold constrains_def, blast)
   154 
   155 text{*anti-monotonic in 1st argument*}
   156 lemma constrains_weaken_L: 
   157     "[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
   158 by (unfold constrains_def, blast)
   159 
   160 lemma constrains_weaken: 
   161    "[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
   162 by (unfold constrains_def, blast)
   163 
   164 subsubsection{*Union*}
   165 
   166 lemma constrains_Un: 
   167     "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
   168 by (unfold constrains_def, blast)
   169 
   170 lemma constrains_UN: 
   171     "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
   172      ==> F \<in> (\<Union>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
   173 by (unfold constrains_def, blast)
   174 
   175 lemma constrains_Un_distrib: "(A \<union> B) co C = (A co C) \<inter> (B co C)"
   176 by (unfold constrains_def, blast)
   177 
   178 lemma constrains_UN_distrib: "(\<Union>i \<in> I. A i) co B = (\<Inter>i \<in> I. A i co B)"
   179 by (unfold constrains_def, blast)
   180 
   181 lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
   182 by (unfold constrains_def, blast)
   183 
   184 lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
   185 by (unfold constrains_def, blast)
   186 
   187 subsubsection{*Intersection*}
   188 
   189 lemma constrains_Int: 
   190     "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
   191 by (unfold constrains_def, blast)
   192 
   193 lemma constrains_INT: 
   194     "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
   195      ==> F \<in> (\<Inter>i \<in> I. A i) co (\<Inter>i \<in> I. A' i)"
   196 by (unfold constrains_def, blast)
   197 
   198 lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
   199 by (unfold constrains_def, auto)
   200 
   201 text{*The reasoning is by subsets since "co" refers to single actions
   202   only.  So this rule isn't that useful.*}
   203 lemma constrains_trans: 
   204     "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
   205 by (unfold constrains_def, blast)
   206 
   207 lemma constrains_cancel: 
   208    "[| F \<in> A co (A' \<union> B); F \<in> B co B' |] ==> F \<in> A co (A' \<union> B')"
   209 by (unfold constrains_def, clarify, blast)
   210 
   211 
   212 subsubsection{*unless*}
   213 
   214 lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
   215 by (unfold unless_def, assumption)
   216 
   217 lemma unlessD: "F \<in> A unless B ==> F \<in> (A-B) co (A \<union> B)"
   218 by (unfold unless_def, assumption)
   219 
   220 
   221 subsubsection{*stable*}
   222 
   223 lemma stableI: "F \<in> A co A ==> F \<in> stable A"
   224 by (unfold stable_def, assumption)
   225 
   226 lemma stableD: "F \<in> stable A ==> F \<in> A co A"
   227 by (unfold stable_def, assumption)
   228 
   229 lemma stable_UNIV [simp]: "stable UNIV = UNIV"
   230 by (unfold stable_def constrains_def, auto)
   231 
   232 subsubsection{*Union*}
   233 
   234 lemma stable_Un: 
   235     "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
   236 
   237 apply (unfold stable_def)
   238 apply (blast intro: constrains_Un)
   239 done
   240 
   241 lemma stable_UN: 
   242     "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Union>i \<in> I. A i)"
   243 apply (unfold stable_def)
   244 apply (blast intro: constrains_UN)
   245 done
   246 
   247 lemma stable_Union: 
   248     "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Union>X)"
   249 by (unfold stable_def constrains_def, blast)
   250 
   251 subsubsection{*Intersection*}
   252 
   253 lemma stable_Int: 
   254     "[| F \<in> stable A;  F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
   255 apply (unfold stable_def)
   256 apply (blast intro: constrains_Int)
   257 done
   258 
   259 lemma stable_INT: 
   260     "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Inter>i \<in> I. A i)"
   261 apply (unfold stable_def)
   262 apply (blast intro: constrains_INT)
   263 done
   264 
   265 lemma stable_Inter: 
   266     "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Inter>X)"
   267 by (unfold stable_def constrains_def, blast)
   268 
   269 lemma stable_constrains_Un: 
   270     "[| F \<in> stable C; F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')"
   271 by (unfold stable_def constrains_def, blast)
   272 
   273 lemma stable_constrains_Int: 
   274   "[| F \<in> stable C; F \<in>  (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
   275 by (unfold stable_def constrains_def, blast)
   276 
   277 (*[| F \<in> stable C; F \<in>  (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
   278 lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI, standard]
   279 
   280 
   281 subsubsection{*invariant*}
   282 
   283 lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
   284 by (simp add: invariant_def)
   285 
   286 text{*Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}*}
   287 lemma invariant_Int:
   288      "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
   289 by (auto simp add: invariant_def stable_Int)
   290 
   291 
   292 subsubsection{*increasing*}
   293 
   294 lemma increasingD: 
   295      "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
   296 by (unfold increasing_def, blast)
   297 
   298 lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
   299 by (unfold increasing_def stable_def, auto)
   300 
   301 lemma mono_increasing_o: 
   302      "mono g ==> increasing f \<subseteq> increasing (g o f)"
   303 apply (unfold increasing_def stable_def constrains_def, auto)
   304 apply (blast intro: monoD order_trans)
   305 done
   306 
   307 (*Holds by the theorem (Suc m \<subseteq> n) = (m < n) *)
   308 lemma strict_increasingD: 
   309      "!!z::nat. F \<in> increasing f ==> F \<in> stable {s. z < f s}"
   310 by (simp add: increasing_def Suc_le_eq [symmetric])
   311 
   312 
   313 (** The Elimination Theorem.  The "free" m has become universally quantified!
   314     Should the premise be !!m instead of \<forall>m ?  Would make it harder to use
   315     in forward proof. **)
   316 
   317 lemma elimination: 
   318     "[| \<forall>m \<in> M. F \<in> {s. s x = m} co (B m) |]  
   319      ==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
   320 by (unfold constrains_def, blast)
   321 
   322 text{*As above, but for the trivial case of a one-variable state, in which the
   323   state is identified with its one variable.*}
   324 lemma elimination_sing: 
   325     "(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
   326 by (unfold constrains_def, blast)
   327 
   328 
   329 
   330 subsubsection{*Theoretical Results from Section 6*}
   331 
   332 lemma constrains_strongest_rhs: 
   333     "F \<in> A co (strongest_rhs F A )"
   334 by (unfold constrains_def strongest_rhs_def, blast)
   335 
   336 lemma strongest_rhs_is_strongest: 
   337     "F \<in> A co B ==> strongest_rhs F A \<subseteq> B"
   338 by (unfold constrains_def strongest_rhs_def, blast)
   339 
   340 
   341 subsubsection{*Ad-hoc set-theory rules*}
   342 
   343 lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
   344 by blast
   345 
   346 lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
   347 by blast
   348 
   349 text{*Needed for WF reasoning in WFair.thy*}
   350 
   351 lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
   352 by blast
   353 
   354 lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
   355 by blast
   356 
   357 
   358 subsection{*Partial versus Total Transitions*}
   359 
   360 constdefs
   361   totalize_act :: "('a * 'a)set => ('a * 'a)set"
   362     "totalize_act act == act \<union> Id_on (-(Domain act))"
   363 
   364   totalize :: "'a program => 'a program"
   365     "totalize F == mk_program (Init F,
   366 			       totalize_act ` Acts F,
   367 			       AllowedActs F)"
   368 
   369   mk_total_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
   370 		   => 'a program"
   371     "mk_total_program args == totalize (mk_program args)"
   372 
   373   all_total :: "'a program => bool"
   374     "all_total F == \<forall>act \<in> Acts F. Domain act = UNIV"
   375   
   376 lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
   377 by (blast intro: sym [THEN image_eqI])
   378 
   379 
   380 subsubsection{*Basic properties*}
   381 
   382 lemma totalize_act_Id [simp]: "totalize_act Id = Id"
   383 by (simp add: totalize_act_def) 
   384 
   385 lemma Domain_totalize_act [simp]: "Domain (totalize_act act) = UNIV"
   386 by (auto simp add: totalize_act_def)
   387 
   388 lemma Init_totalize [simp]: "Init (totalize F) = Init F"
   389 by (unfold totalize_def, auto)
   390 
   391 lemma Acts_totalize [simp]: "Acts (totalize F) = (totalize_act ` Acts F)"
   392 by (simp add: totalize_def insert_Id_image_Acts) 
   393 
   394 lemma AllowedActs_totalize [simp]: "AllowedActs (totalize F) = AllowedActs F"
   395 by (simp add: totalize_def)
   396 
   397 lemma totalize_constrains_iff [simp]: "(totalize F \<in> A co B) = (F \<in> A co B)"
   398 by (simp add: totalize_def totalize_act_def constrains_def, blast)
   399 
   400 lemma totalize_stable_iff [simp]: "(totalize F \<in> stable A) = (F \<in> stable A)"
   401 by (simp add: stable_def)
   402 
   403 lemma totalize_invariant_iff [simp]:
   404      "(totalize F \<in> invariant A) = (F \<in> invariant A)"
   405 by (simp add: invariant_def)
   406 
   407 lemma all_total_totalize: "all_total (totalize F)"
   408 by (simp add: totalize_def all_total_def)
   409 
   410 lemma Domain_iff_totalize_act: "(Domain act = UNIV) = (totalize_act act = act)"
   411 by (force simp add: totalize_act_def)
   412 
   413 lemma all_total_imp_totalize: "all_total F ==> (totalize F = F)"
   414 apply (simp add: all_total_def totalize_def) 
   415 apply (rule program_equalityI)
   416   apply (simp_all add: Domain_iff_totalize_act image_def)
   417 done
   418 
   419 lemma all_total_iff_totalize: "all_total F = (totalize F = F)"
   420 apply (rule iffI) 
   421  apply (erule all_total_imp_totalize) 
   422 apply (erule subst) 
   423 apply (rule all_total_totalize) 
   424 done
   425 
   426 lemma mk_total_program_constrains_iff [simp]:
   427      "(mk_total_program args \<in> A co B) = (mk_program args \<in> A co B)"
   428 by (simp add: mk_total_program_def)
   429 
   430 
   431 subsection{*Rules for Lazy Definition Expansion*}
   432 
   433 text{*They avoid expanding the full program, which is a large expression*}
   434 
   435 lemma def_prg_Init:
   436      "F == mk_total_program (init,acts,allowed) ==> Init F = init"
   437 by (simp add: mk_total_program_def)
   438 
   439 lemma def_prg_Acts:
   440      "F == mk_total_program (init,acts,allowed) 
   441       ==> Acts F = insert Id (totalize_act ` acts)"
   442 by (simp add: mk_total_program_def)
   443 
   444 lemma def_prg_AllowedActs:
   445      "F == mk_total_program (init,acts,allowed)  
   446       ==> AllowedActs F = insert Id allowed"
   447 by (simp add: mk_total_program_def)
   448 
   449 text{*An action is expanded if a pair of states is being tested against it*}
   450 lemma def_act_simp:
   451      "act == {(s,s'). P s s'} ==> ((s,s') \<in> act) = P s s'"
   452 by (simp add: mk_total_program_def)
   453 
   454 text{*A set is expanded only if an element is being tested against it*}
   455 lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
   456 by (simp add: mk_total_program_def)
   457 
   458 subsubsection{*Inspectors for type "program"*}
   459 
   460 lemma Init_total_eq [simp]:
   461      "Init (mk_total_program (init,acts,allowed)) = init"
   462 by (simp add: mk_total_program_def)
   463 
   464 lemma Acts_total_eq [simp]:
   465     "Acts(mk_total_program(init,acts,allowed)) = insert Id (totalize_act`acts)"
   466 by (simp add: mk_total_program_def)
   467 
   468 lemma AllowedActs_total_eq [simp]:
   469      "AllowedActs (mk_total_program (init,acts,allowed)) = insert Id allowed"
   470 by (auto simp add: mk_total_program_def)
   471 
   472 end