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
6 The basic UNITY theory (revised version, based upon the "co" operator)
8 From Misra, "A Logic for Concurrent Programming", 1994
9 *)
11 header {*The Basic UNITY Theory*}
13 theory UNITY = Main:
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
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}"
24   unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
25     "A unless B == (A-B) co (A \<union> B)"
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)"
32   Init :: "'a program => 'a set"
33     "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
35   Acts :: "'a program => ('a * 'a)set set"
36     "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
38   AllowedActs :: "'a program => ('a * 'a)set set"
39     "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
41   Allowed :: "'a program => 'a program set"
42     "Allowed F == {G. Acts G \<subseteq> AllowedActs F}"
44   stable     :: "'a set => 'a program set"
45     "stable A == A co A"
47   strongest_rhs :: "['a program, 'a set] => 'a set"
48     "strongest_rhs F A == Inter {B. F \<in> A co B}"
50   invariant :: "'a set => 'a program set"
51     "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
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}"
58 (*Perhaps equalities.ML shouldn't add this in the first place!*)
59 declare image_Collect [simp del]
61 (*** The abstract type of programs ***)
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
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
72 lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
73 by (simp add: insert_absorb Id_in_Acts)
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
80 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
81 by (simp add: insert_absorb Id_in_AllowedActs)
83 (** Inspectors for type "program" **)
85 lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
86 by (auto simp add: program_typedef)
88 lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
89 by (auto simp add: program_typedef)
91 lemma AllowedActs_eq [simp]:
92      "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
93 by (auto simp add: program_typedef)
95 (** Equality for UNITY programs **)
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
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
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
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)
124 (*** These rules allow "lazy" definition expansion
125      They avoid expanding the full program, which is a large expression
126 ***)
128 lemma def_prg_Init: "F == mk_program (init,acts,allowed) ==> Init F = init"
129 by auto
131 lemma def_prg_Acts:
132      "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts"
133 by auto
135 lemma def_prg_AllowedActs:
136      "F == mk_program (init,acts,allowed)
137       ==> AllowedActs F = insert Id allowed"
138 by auto
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
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
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
156 (*** co ***)
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)
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)
167 lemma constrains_empty [iff]: "F \<in> {} co B"
168 by (unfold constrains_def, blast)
170 lemma constrains_empty2 [iff]: "(F \<in> A co {}) = (A={})"
171 by (unfold constrains_def, blast)
173 lemma constrains_UNIV [iff]: "(F \<in> UNIV co B) = (B = UNIV)"
174 by (unfold constrains_def, blast)
176 lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
177 by (unfold constrains_def, blast)
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)
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)
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)
193 (** Union **)
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)
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)
204 lemma constrains_Un_distrib: "(A \<union> B) co C = (A co C) \<inter> (B co C)"
205 by (unfold constrains_def, blast)
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)
210 lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
211 by (unfold constrains_def, blast)
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)
216 (** Intersection **)
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)
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)
227 lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
228 by (unfold constrains_def, auto)
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)
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)
241 (*** unless ***)
243 lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
244 by (unfold unless_def, assumption)
246 lemma unlessD: "F \<in> A unless B ==> F \<in> (A-B) co (A \<union> B)"
247 by (unfold unless_def, assumption)
250 (*** stable ***)
252 lemma stableI: "F \<in> A co A ==> F \<in> stable A"
253 by (unfold stable_def, assumption)
255 lemma stableD: "F \<in> stable A ==> F \<in> A co A"
256 by (unfold stable_def, assumption)
258 lemma stable_UNIV [simp]: "stable UNIV = UNIV"
259 by (unfold stable_def constrains_def, auto)
261 (** Union **)
263 lemma stable_Un:
264     "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
266 apply (unfold stable_def)
267 apply (blast intro: constrains_Un)
268 done
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
276 (** Intersection **)
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
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
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)
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)
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]
302 (*** invariant ***)
304 lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
305 by (simp add: invariant_def)
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)
313 (*** increasing ***)
315 lemma increasingD:
316      "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
318 by (unfold increasing_def, blast)
320 lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
321 by (unfold increasing_def stable_def, auto)
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
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])
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. **)
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)
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)
352 (*** Theoretical Results from Section 6 ***)
354 lemma constrains_strongest_rhs:
355     "F \<in> A co (strongest_rhs F A )"
356 by (unfold constrains_def strongest_rhs_def, blast)
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)
363 (** Ad-hoc set-theory rules **)
365 lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
366 by blast
368 lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
369 by blast
371 (** Needed for WF reasoning in WFair.ML **)
373 lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
374 by blast
376 lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
377 by blast
379 end