src/HOL/UNITY/Comp.thy
 author paulson Sat Feb 08 16:05:33 2003 +0100 (2003-02-08) changeset 13812 91713a1915ee parent 13805 3786b2fd6808 child 13819 78f5885b76a9 permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
1 (*  Title:      HOL/UNITY/Comp.thy
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   1998  University of Cambridge
6 Composition
7 From Chandy and Sanders, "Reasoning About Program Composition",
8 Technical Report 2000-003, University of Florida, 2000.
10 Revised by Sidi Ehmety on January  2001
12 Added: a strong form of the \<subseteq> relation (component_of) and localize
14 *)
18 theory Comp = Union:
20 instance program :: (type) ord ..
22 defs
23   component_def:          "F \<le> H == \<exists>G. F Join G = H"
24   strict_component_def:   "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
27 constdefs
28   component_of :: "'a program =>'a program=> bool"
29                                     (infixl "component'_of" 50)
30   "F component_of H == \<exists>G. F ok G & F Join G = H"
32   strict_component_of :: "'a program\<Rightarrow>'a program=> bool"
33                                     (infixl "strict'_component'_of" 50)
34   "F strict_component_of H == F component_of H & F\<noteq>H"
36   preserves :: "('a=>'b) => 'a program set"
37     "preserves v == \<Inter>z. stable {s. v s = z}"
39   localize  :: "('a=>'b) => 'a program => 'a program"
40   "localize v F == mk_program(Init F, Acts F,
41 			      AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))"
43   funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
44   "funPair f g == %x. (f x, g x)"
47 subsection{*The component relation*}
48 lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F Join G)"
49 apply (unfold component_def, auto)
50 apply (rule_tac x = "G Join Ga" in exI)
51 apply (rule_tac [2] x = "G Join F" in exI)
52 apply (auto simp add: Join_ac)
53 done
55 lemma component_eq_subset:
56      "(F \<le> G) =
57       (Init G \<subseteq> Init F & Acts F \<subseteq> Acts G & AllowedActs G \<subseteq> AllowedActs F)"
58 apply (unfold component_def)
59 apply (force intro!: exI program_equalityI)
60 done
62 lemma component_SKIP [iff]: "SKIP \<le> F"
63 apply (unfold component_def)
64 apply (force intro: Join_SKIP_left)
65 done
67 lemma component_refl [iff]: "F \<le> (F :: 'a program)"
68 apply (unfold component_def)
69 apply (blast intro: Join_SKIP_right)
70 done
72 lemma SKIP_minimal: "F \<le> SKIP ==> F = SKIP"
73 by (auto intro!: program_equalityI simp add: component_eq_subset)
75 lemma component_Join1: "F \<le> (F Join G)"
76 by (unfold component_def, blast)
78 lemma component_Join2: "G \<le> (F Join G)"
79 apply (unfold component_def)
80 apply (simp add: Join_commute, blast)
81 done
83 lemma Join_absorb1: "F \<le> G ==> F Join G = G"
84 by (auto simp add: component_def Join_left_absorb)
86 lemma Join_absorb2: "G \<le> F ==> F Join G = F"
87 by (auto simp add: Join_ac component_def)
89 lemma JN_component_iff: "((JOIN I F) \<le> H) = (\<forall>i \<in> I. F i \<le> H)"
90 by (simp add: component_eq_subset, blast)
92 lemma component_JN: "i \<in> I ==> (F i) \<le> (\<Squnion>i \<in> I. (F i))"
93 apply (unfold component_def)
94 apply (blast intro: JN_absorb)
95 done
97 lemma component_trans: "[| F \<le> G; G \<le> H |] ==> F \<le> (H :: 'a program)"
98 apply (unfold component_def)
99 apply (blast intro: Join_assoc [symmetric])
100 done
102 lemma component_antisym: "[| F \<le> G; G \<le> F |] ==> F = (G :: 'a program)"
103 apply (simp (no_asm_use) add: component_eq_subset)
104 apply (blast intro!: program_equalityI)
105 done
107 lemma Join_component_iff: "((F Join G) \<le> H) = (F \<le> H & G \<le> H)"
108 by (simp add: component_eq_subset, blast)
110 lemma component_constrains: "[| F \<le> G; G \<in> A co B |] ==> F \<in> A co B"
111 by (auto simp add: constrains_def component_eq_subset)
113 (*Used in Guar.thy to show that programs are partially ordered*)
114 lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
117 subsection{*The preserves property*}
119 lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
120 by (unfold preserves_def, blast)
122 lemma preserves_imp_eq:
123      "[| F \<in> preserves v;  act \<in> Acts F;  (s,s') \<in> act |] ==> v s = v s'"
124 apply (unfold preserves_def stable_def constrains_def, force)
125 done
127 lemma Join_preserves [iff]:
128      "(F Join G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
129 apply (unfold preserves_def, auto)
130 done
132 lemma JN_preserves [iff]:
133      "(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)"
134 apply (simp add: JN_stable preserves_def, blast)
135 done
137 lemma SKIP_preserves [iff]: "SKIP \<in> preserves v"
138 by (auto simp add: preserves_def)
140 lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)"
143 lemma preserves_funPair: "preserves (funPair v w) = preserves v \<inter> preserves w"
144 by (auto simp add: preserves_def stable_def constrains_def, blast)
146 (* (F \<in> preserves (funPair v w)) = (F \<in> preserves v \<inter> preserves w) *)
147 declare preserves_funPair [THEN eqset_imp_iff, iff]
150 lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)"
151 by (simp add: funPair_def o_def)
153 lemma fst_o_funPair [simp]: "fst o (funPair f g) = f"
154 by (simp add: funPair_def o_def)
156 lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
157 by (simp add: funPair_def o_def)
159 lemma subset_preserves_o: "preserves v \<subseteq> preserves (w o v)"
160 by (force simp add: preserves_def stable_def constrains_def)
162 lemma preserves_subset_stable: "preserves v \<subseteq> stable {s. P (v s)}"
163 apply (auto simp add: preserves_def stable_def constrains_def)
164 apply (rename_tac s' s)
165 apply (subgoal_tac "v s = v s'")
166 apply (force+)
167 done
169 lemma preserves_subset_increasing: "preserves v \<subseteq> increasing v"
170 by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def)
172 lemma preserves_id_subset_stable: "preserves id \<subseteq> stable A"
173 by (force simp add: preserves_def stable_def constrains_def)
176 (** For use with def_UNION_ok_iff **)
178 lemma safety_prop_preserves [iff]: "safety_prop (preserves v)"
179 by (auto intro: safety_prop_INTER1 simp add: preserves_def)
182 (** Some lemmas used only in Client.ML **)
184 lemma stable_localTo_stable2:
185      "[| F \<in> stable {s. P (v s) (w s)};
186          G \<in> preserves v;  G \<in> preserves w |]
187       ==> F Join G \<in> stable {s. P (v s) (w s)}"
188 apply simp
189 apply (subgoal_tac "G \<in> preserves (funPair v w) ")
190  prefer 2 apply simp
191 apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
192 done
194 lemma Increasing_preserves_Stable:
195      "[| F \<in> stable {s. v s \<le> w s};  G \<in> preserves v;
196          F Join G \<in> Increasing w |]
197       ==> F Join G \<in> Stable {s. v s \<le> w s}"
198 apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
199 apply (blast intro: constrains_weaken)
200 (*The G case remains*)
201 apply (auto simp add: preserves_def stable_def constrains_def)
202 apply (case_tac "act: Acts F", blast)
203 (*We have a G-action, so delete assumptions about F-actions*)
204 apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
205 apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)
206 apply (subgoal_tac "v x = v xa")
207 prefer 2 apply blast
208 apply auto
209 apply (erule order_trans, blast)
210 done
212 (** component_of **)
214 (*  component_of is stronger than \<le> *)
215 lemma component_of_imp_component: "F component_of H ==> F \<le> H"
216 by (unfold component_def component_of_def, blast)
219 (* component_of satisfies many of the same properties as \<le> *)
220 lemma component_of_refl [simp]: "F component_of F"
221 apply (unfold component_of_def)
222 apply (rule_tac x = SKIP in exI, auto)
223 done
225 lemma component_of_SKIP [simp]: "SKIP component_of F"
226 by (unfold component_of_def, auto)
228 lemma component_of_trans:
229      "[| F component_of G; G component_of H |] ==> F component_of H"
230 apply (unfold component_of_def)
231 apply (blast intro: Join_assoc [symmetric])
232 done
234 lemmas strict_component_of_eq =
235     strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
237 (** localize **)
238 lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"