src/HOL/UNITY/UNITY.thy
 author haftmann Fri Jun 11 17:14:02 2010 +0200 (2010-06-11) changeset 37407 61dd8c145da7 parent 36866 426d5781bb25 child 45605 a89b4bc311a5 permissions -rw-r--r--
declare lex_prod_def [code del]
1 (*  Title:      HOL/UNITY/UNITY.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1998  University of Cambridge
5 The basic UNITY theory (revised version, based upon the "co"
6 operator).
8 From Misra, "A Logic for Concurrent Programming", 1994.
9 *)
11 header {*The Basic UNITY Theory*}
13 theory UNITY imports Main begin
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 definition Acts :: "'a program => ('a * 'a)set set" where
21     "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
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}"
26 definition unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)  where
27     "A unless B == (A-B) co (A \<union> B)"
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)"
34 definition Init :: "'a program => 'a set" where
35     "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
37 definition AllowedActs :: "'a program => ('a * 'a)set set" where
38     "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
40 definition Allowed :: "'a program => 'a program set" where
41     "Allowed F == {G. Acts G \<subseteq> AllowedActs F}"
43 definition stable     :: "'a set => 'a program set" where
44     "stable A == A co A"
46 definition strongest_rhs :: "['a program, 'a set] => 'a set" where
47     "strongest_rhs F A == Inter {B. F \<in> A co B}"
49 definition invariant :: "'a set => 'a program set" where
50     "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
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}"
57 text{*Perhaps HOL shouldn't add this in the first place!*}
58 declare image_Collect [simp del]
60 subsubsection{*The abstract type of programs*}
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
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
71 lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
72 by (simp add: insert_absorb Id_in_Acts)
74 lemma Acts_nonempty [simp]: "Acts F \<noteq> {}"
75 by auto
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
82 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
83 by (simp add: insert_absorb Id_in_AllowedActs)
85 subsubsection{*Inspectors for type "program"*}
87 lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
90 lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
93 lemma AllowedActs_eq [simp]:
94      "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
97 subsubsection{*Equality for UNITY programs*}
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
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
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
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)
126 subsubsection{*co*}
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)
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)
137 lemma constrains_empty [iff]: "F \<in> {} co B"
138 by (unfold constrains_def, blast)
140 lemma constrains_empty2 [iff]: "(F \<in> A co {}) = (A={})"
141 by (unfold constrains_def, blast)
143 lemma constrains_UNIV [iff]: "(F \<in> UNIV co B) = (B = UNIV)"
144 by (unfold constrains_def, blast)
146 lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
147 by (unfold constrains_def, blast)
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)
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)
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)
163 subsubsection{*Union*}
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)
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)
174 lemma constrains_Un_distrib: "(A \<union> B) co C = (A co C) \<inter> (B co C)"
175 by (unfold constrains_def, blast)
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)
180 lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
181 by (unfold constrains_def, blast)
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)
186 subsubsection{*Intersection*}
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)
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)
197 lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
198 by (unfold constrains_def, auto)
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)
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)
211 subsubsection{*unless*}
213 lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
214 by (unfold unless_def, assumption)
216 lemma unlessD: "F \<in> A unless B ==> F \<in> (A-B) co (A \<union> B)"
217 by (unfold unless_def, assumption)
220 subsubsection{*stable*}
222 lemma stableI: "F \<in> A co A ==> F \<in> stable A"
223 by (unfold stable_def, assumption)
225 lemma stableD: "F \<in> stable A ==> F \<in> A co A"
226 by (unfold stable_def, assumption)
228 lemma stable_UNIV [simp]: "stable UNIV = UNIV"
229 by (unfold stable_def constrains_def, auto)
231 subsubsection{*Union*}
233 lemma stable_Un:
234     "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
236 apply (unfold stable_def)
237 apply (blast intro: constrains_Un)
238 done
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
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)
250 subsubsection{*Intersection*}
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
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
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)
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)
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)
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]
280 subsubsection{*invariant*}
282 lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
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)
291 subsubsection{*increasing*}
293 lemma increasingD:
294      "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
295 by (unfold increasing_def, blast)
297 lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
298 by (unfold increasing_def stable_def, auto)
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
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])
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. **)
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)
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)
329 subsubsection{*Theoretical Results from Section 6*}
331 lemma constrains_strongest_rhs:
332     "F \<in> A co (strongest_rhs F A )"
333 by (unfold constrains_def strongest_rhs_def, blast)
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)
342 lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
343 by blast
345 lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
346 by blast
348 text{*Needed for WF reasoning in WFair.thy*}
350 lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
351 by blast
353 lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
354 by blast
357 subsection{*Partial versus Total Transitions*}
359 definition totalize_act :: "('a * 'a)set => ('a * 'a)set" where
360     "totalize_act act == act \<union> Id_on (-(Domain act))"
362 definition totalize :: "'a program => 'a program" where
363     "totalize F == mk_program (Init F,
364                                totalize_act ` Acts F,
365                                AllowedActs F)"
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)"
371 definition all_total :: "'a program => bool" where
372     "all_total F == \<forall>act \<in> Acts F. Domain act = UNIV"
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])
378 subsubsection{*Basic properties*}
380 lemma totalize_act_Id [simp]: "totalize_act Id = Id"
383 lemma Domain_totalize_act [simp]: "Domain (totalize_act act) = UNIV"
384 by (auto simp add: totalize_act_def)
386 lemma Init_totalize [simp]: "Init (totalize F) = Init F"
387 by (unfold totalize_def, auto)
389 lemma Acts_totalize [simp]: "Acts (totalize F) = (totalize_act ` Acts F)"
390 by (simp add: totalize_def insert_Id_image_Acts)
392 lemma AllowedActs_totalize [simp]: "AllowedActs (totalize F) = AllowedActs F"
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)
398 lemma totalize_stable_iff [simp]: "(totalize F \<in> stable A) = (F \<in> stable A)"
401 lemma totalize_invariant_iff [simp]:
402      "(totalize F \<in> invariant A) = (F \<in> invariant A)"
405 lemma all_total_totalize: "all_total (totalize F)"
406 by (simp add: totalize_def all_total_def)
408 lemma Domain_iff_totalize_act: "(Domain act = UNIV) = (totalize_act act = act)"
409 by (force simp add: totalize_act_def)
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
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
424 lemma mk_total_program_constrains_iff [simp]:
425      "(mk_total_program args \<in> A co B) = (mk_program args \<in> A co B)"
429 subsection{*Rules for Lazy Definition Expansion*}
431 text{*They avoid expanding the full program, which is a large expression*}
433 lemma def_prg_Init:
434      "F = mk_total_program (init,acts,allowed) ==> Init F = init"
437 lemma def_prg_Acts:
438      "F = mk_total_program (init,acts,allowed)
439       ==> Acts F = insert Id (totalize_act ` acts)"
442 lemma def_prg_AllowedActs:
443      "F = mk_total_program (init,acts,allowed)
444       ==> AllowedActs F = insert Id allowed"
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'"
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)"