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