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
```