src/HOL/UNITY/UNITY.thy
author paulson
Tue Feb 04 18:12:40 2003 +0100 (2003-02-04)
changeset 13805 3786b2fd6808
parent 13798 4c1a53627500
child 13812 91713a1915ee
permissions -rw-r--r--
some x-symbols
     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 = Main:
    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   constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
    22     "A co B == {F. \<forall>act \<in> Acts F. act``A \<subseteq> B}"
    23 
    24   unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
    25     "A unless B == (A-B) co (A \<union> B)"
    26 
    27   mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
    28 		   => 'a program"
    29     "mk_program == %(init, acts, allowed).
    30                       Abs_Program (init, insert Id acts, insert Id allowed)"
    31 
    32   Init :: "'a program => 'a set"
    33     "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
    34 
    35   Acts :: "'a program => ('a * 'a)set set"
    36     "Acts F == (%(init, acts, allowed). acts) (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   (*Polymorphic in both states and the meaning of \<le> *)
    54   increasing :: "['a => 'b::{order}] => 'a program set"
    55     "increasing f == \<Inter>z. stable {s. z \<le> f s}"
    56 
    57 
    58 (*Perhaps equalities.ML shouldn't add this in the first place!*)
    59 declare image_Collect [simp del]
    60 
    61 (*** 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 Id_in_AllowedActs [iff]: "Id \<in> AllowedActs F"
    76 apply (cut_tac x = F in Rep_Program)
    77 apply (auto simp add: program_typedef) 
    78 done
    79 
    80 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
    81 by (simp add: insert_absorb Id_in_AllowedActs)
    82 
    83 (** Inspectors for type "program" **)
    84 
    85 lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
    86 by (auto simp add: program_typedef)
    87 
    88 lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
    89 by (auto simp add: program_typedef)
    90 
    91 lemma AllowedActs_eq [simp]:
    92      "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
    93 by (auto simp add: program_typedef)
    94 
    95 (** Equality for UNITY programs **)
    96 
    97 lemma surjective_mk_program [simp]:
    98      "mk_program (Init F, Acts F, AllowedActs F) = F"
    99 apply (cut_tac x = F in Rep_Program)
   100 apply (auto simp add: program_typedef)
   101 apply (drule_tac f = Abs_Program in arg_cong)+
   102 apply (simp add: program_typedef insert_absorb)
   103 done
   104 
   105 lemma program_equalityI:
   106      "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]  
   107       ==> F = G"
   108 apply (rule_tac t = F in surjective_mk_program [THEN subst])
   109 apply (rule_tac t = G in surjective_mk_program [THEN subst], simp)
   110 done
   111 
   112 lemma program_equalityE:
   113      "[| F = G;  
   114          [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] 
   115          ==> P |] ==> P"
   116 by simp 
   117 
   118 lemma program_equality_iff:
   119      "(F=G) =   
   120       (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)"
   121 by (blast intro: program_equalityI program_equalityE)
   122 
   123 
   124 (*** These rules allow "lazy" definition expansion 
   125      They avoid expanding the full program, which is a large expression
   126 ***)
   127 
   128 lemma def_prg_Init: "F == mk_program (init,acts,allowed) ==> Init F = init"
   129 by auto
   130 
   131 lemma def_prg_Acts:
   132      "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts"
   133 by auto
   134 
   135 lemma def_prg_AllowedActs:
   136      "F == mk_program (init,acts,allowed)  
   137       ==> AllowedActs F = insert Id allowed"
   138 by auto
   139 
   140 (*The program is not expanded, but its Init and Acts are*)
   141 lemma def_prg_simps:
   142     "[| F == mk_program (init,acts,allowed) |]  
   143      ==> Init F = init & Acts F = insert Id acts"
   144 by simp
   145 
   146 (*An action is expanded only if a pair of states is being tested against it*)
   147 lemma def_act_simp:
   148      "[| act == {(s,s'). P s s'} |] ==> ((s,s') \<in> act) = P s s'"
   149 by auto
   150 
   151 (*A set is expanded only if an element is being tested against it*)
   152 lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
   153 by auto
   154 
   155 
   156 (*** co ***)
   157 
   158 lemma constrainsI: 
   159     "(!!act s s'. [| act: Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s': A')  
   160      ==> F \<in> A co A'"
   161 by (simp add: constrains_def, blast)
   162 
   163 lemma constrainsD: 
   164     "[| F \<in> A co A'; act: Acts F;  (s,s'): act;  s \<in> A |] ==> s': A'"
   165 by (unfold constrains_def, blast)
   166 
   167 lemma constrains_empty [iff]: "F \<in> {} co B"
   168 by (unfold constrains_def, blast)
   169 
   170 lemma constrains_empty2 [iff]: "(F \<in> A co {}) = (A={})"
   171 by (unfold constrains_def, blast)
   172 
   173 lemma constrains_UNIV [iff]: "(F \<in> UNIV co B) = (B = UNIV)"
   174 by (unfold constrains_def, blast)
   175 
   176 lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
   177 by (unfold constrains_def, blast)
   178 
   179 (*monotonic in 2nd argument*)
   180 lemma constrains_weaken_R: 
   181     "[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
   182 by (unfold constrains_def, blast)
   183 
   184 (*anti-monotonic in 1st argument*)
   185 lemma constrains_weaken_L: 
   186     "[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
   187 by (unfold constrains_def, blast)
   188 
   189 lemma constrains_weaken: 
   190    "[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
   191 by (unfold constrains_def, blast)
   192 
   193 (** Union **)
   194 
   195 lemma constrains_Un: 
   196     "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
   197 by (unfold constrains_def, blast)
   198 
   199 lemma constrains_UN: 
   200     "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
   201      ==> F \<in> (\<Union>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
   202 by (unfold constrains_def, blast)
   203 
   204 lemma constrains_Un_distrib: "(A \<union> B) co C = (A co C) \<inter> (B co C)"
   205 by (unfold constrains_def, blast)
   206 
   207 lemma constrains_UN_distrib: "(\<Union>i \<in> I. A i) co B = (\<Inter>i \<in> I. A i co B)"
   208 by (unfold constrains_def, blast)
   209 
   210 lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
   211 by (unfold constrains_def, blast)
   212 
   213 lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
   214 by (unfold constrains_def, blast)
   215 
   216 (** Intersection **)
   217 
   218 lemma constrains_Int: 
   219     "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
   220 by (unfold constrains_def, blast)
   221 
   222 lemma constrains_INT: 
   223     "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
   224      ==> F \<in> (\<Inter>i \<in> I. A i) co (\<Inter>i \<in> I. A' i)"
   225 by (unfold constrains_def, blast)
   226 
   227 lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
   228 by (unfold constrains_def, auto)
   229 
   230 (*The reasoning is by subsets since "co" refers to single actions
   231   only.  So this rule isn't that useful.*)
   232 lemma constrains_trans: 
   233     "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
   234 by (unfold constrains_def, blast)
   235 
   236 lemma constrains_cancel: 
   237    "[| F \<in> A co (A' \<union> B); F \<in> B co B' |] ==> F \<in> A co (A' \<union> B')"
   238 by (unfold constrains_def, clarify, blast)
   239 
   240 
   241 (*** unless ***)
   242 
   243 lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
   244 by (unfold unless_def, assumption)
   245 
   246 lemma unlessD: "F \<in> A unless B ==> F \<in> (A-B) co (A \<union> B)"
   247 by (unfold unless_def, assumption)
   248 
   249 
   250 (*** stable ***)
   251 
   252 lemma stableI: "F \<in> A co A ==> F \<in> stable A"
   253 by (unfold stable_def, assumption)
   254 
   255 lemma stableD: "F \<in> stable A ==> F \<in> A co A"
   256 by (unfold stable_def, assumption)
   257 
   258 lemma stable_UNIV [simp]: "stable UNIV = UNIV"
   259 by (unfold stable_def constrains_def, auto)
   260 
   261 (** Union **)
   262 
   263 lemma stable_Un: 
   264     "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
   265 
   266 apply (unfold stable_def)
   267 apply (blast intro: constrains_Un)
   268 done
   269 
   270 lemma stable_UN: 
   271     "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Union>i \<in> I. A i)"
   272 apply (unfold stable_def)
   273 apply (blast intro: constrains_UN)
   274 done
   275 
   276 (** Intersection **)
   277 
   278 lemma stable_Int: 
   279     "[| F \<in> stable A;  F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
   280 apply (unfold stable_def)
   281 apply (blast intro: constrains_Int)
   282 done
   283 
   284 lemma stable_INT: 
   285     "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Inter>i \<in> I. A i)"
   286 apply (unfold stable_def)
   287 apply (blast intro: constrains_INT)
   288 done
   289 
   290 lemma stable_constrains_Un: 
   291     "[| F \<in> stable C; F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')"
   292 by (unfold stable_def constrains_def, blast)
   293 
   294 lemma stable_constrains_Int: 
   295   "[| F \<in> stable C; F \<in>  (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
   296 by (unfold stable_def constrains_def, blast)
   297 
   298 (*[| F \<in> stable C; F \<in>  (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
   299 lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
   300 
   301 
   302 (*** invariant ***)
   303 
   304 lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
   305 by (simp add: invariant_def)
   306 
   307 (*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*)
   308 lemma invariant_Int:
   309      "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
   310 by (auto simp add: invariant_def stable_Int)
   311 
   312 
   313 (*** increasing ***)
   314 
   315 lemma increasingD: 
   316      "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
   317 
   318 by (unfold increasing_def, blast)
   319 
   320 lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
   321 by (unfold increasing_def stable_def, auto)
   322 
   323 lemma mono_increasing_o: 
   324      "mono g ==> increasing f \<subseteq> increasing (g o f)"
   325 apply (unfold increasing_def stable_def constrains_def, auto)
   326 apply (blast intro: monoD order_trans)
   327 done
   328 
   329 (*Holds by the theorem (Suc m \<subseteq> n) = (m < n) *)
   330 lemma strict_increasingD: 
   331      "!!z::nat. F \<in> increasing f ==> F \<in> stable {s. z < f s}"
   332 by (simp add: increasing_def Suc_le_eq [symmetric])
   333 
   334 
   335 (** The Elimination Theorem.  The "free" m has become universally quantified!
   336     Should the premise be !!m instead of \<forall>m ?  Would make it harder to use
   337     in forward proof. **)
   338 
   339 lemma elimination: 
   340     "[| \<forall>m \<in> M. F \<in> {s. s x = m} co (B m) |]  
   341      ==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
   342 by (unfold constrains_def, blast)
   343 
   344 (*As above, but for the trivial case of a one-variable state, in which the
   345   state is identified with its one variable.*)
   346 lemma elimination_sing: 
   347     "(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
   348 by (unfold constrains_def, blast)
   349 
   350 
   351 
   352 (*** Theoretical Results from Section 6 ***)
   353 
   354 lemma constrains_strongest_rhs: 
   355     "F \<in> A co (strongest_rhs F A )"
   356 by (unfold constrains_def strongest_rhs_def, blast)
   357 
   358 lemma strongest_rhs_is_strongest: 
   359     "F \<in> A co B ==> strongest_rhs F A \<subseteq> B"
   360 by (unfold constrains_def strongest_rhs_def, blast)
   361 
   362 
   363 (** Ad-hoc set-theory rules **)
   364 
   365 lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
   366 by blast
   367 
   368 lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
   369 by blast
   370 
   371 (** Needed for WF reasoning in WFair.ML **)
   372 
   373 lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
   374 by blast
   375 
   376 lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
   377 by blast
   378 
   379 end