1 (* Title: HOL/UNITY/Comp.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Composition |
|
7 From Chandy and Sanders, "Reasoning About Program Composition" |
|
8 |
|
9 Revised by Sidi Ehmety on January 2001 |
|
10 |
|
11 *) |
|
12 (*** component <= ***) |
|
13 Goalw [component_def] |
|
14 "H <= F | H <= G ==> H <= (F Join G)"; |
|
15 by Auto_tac; |
|
16 by (res_inst_tac [("x", "G Join Ga")] exI 1); |
|
17 by (res_inst_tac [("x", "G Join F")] exI 2); |
|
18 by (auto_tac (claset(), simpset() addsimps Join_ac)); |
|
19 qed "componentI"; |
|
20 |
|
21 Goalw [component_def] |
|
22 "(F <= G) = \ |
|
23 \ (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)"; |
|
24 by (force_tac (claset() addSIs [exI, program_equalityI], |
|
25 simpset()) 1); |
|
26 qed "component_eq_subset"; |
|
27 |
|
28 Goalw [component_def] "SKIP <= F"; |
|
29 by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1); |
|
30 qed "component_SKIP"; |
|
31 |
|
32 Goalw [component_def] "F <= (F :: 'a program)"; |
|
33 by (blast_tac (claset() addIs [Join_SKIP_right]) 1); |
|
34 qed "component_refl"; |
|
35 |
|
36 AddIffs [component_SKIP, component_refl]; |
|
37 |
|
38 Goal "F <= SKIP ==> F = SKIP"; |
|
39 by (auto_tac (claset() addSIs [program_equalityI], |
|
40 simpset() addsimps [component_eq_subset])); |
|
41 qed "SKIP_minimal"; |
|
42 |
|
43 Goalw [component_def] "F <= (F Join G)"; |
|
44 by (Blast_tac 1); |
|
45 qed "component_Join1"; |
|
46 |
|
47 Goalw [component_def] "G <= (F Join G)"; |
|
48 by (simp_tac (simpset() addsimps [Join_commute]) 1); |
|
49 by (Blast_tac 1); |
|
50 qed "component_Join2"; |
|
51 |
|
52 Goal "F<=G ==> F Join G = G"; |
|
53 by (auto_tac (claset(), simpset() addsimps [component_def, Join_left_absorb])); |
|
54 qed "Join_absorb1"; |
|
55 |
|
56 Goal "G<=F ==> F Join G = F"; |
|
57 by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def])); |
|
58 qed "Join_absorb2"; |
|
59 |
|
60 Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)"; |
|
61 by (simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
62 by (Blast_tac 1); |
|
63 qed "JN_component_iff"; |
|
64 |
|
65 Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))"; |
|
66 by (blast_tac (claset() addIs [JN_absorb]) 1); |
|
67 qed "component_JN"; |
|
68 |
|
69 Goalw [component_def] "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"; |
|
70 by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); |
|
71 qed "component_trans"; |
|
72 |
|
73 Goal "[| F <= G; G <= F |] ==> F = (G :: 'a program)"; |
|
74 by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
75 by (blast_tac (claset() addSIs [program_equalityI]) 1); |
|
76 qed "component_antisym"; |
|
77 |
|
78 Goal "((F Join G) <= H) = (F <= H & G <= H)"; |
|
79 by (simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
80 by (Blast_tac 1); |
|
81 qed "Join_component_iff"; |
|
82 |
|
83 Goal "[| F <= G; G : A co B |] ==> F : A co B"; |
|
84 by (auto_tac (claset(), |
|
85 simpset() addsimps [constrains_def, component_eq_subset])); |
|
86 qed "component_constrains"; |
|
87 |
|
88 (*Used in Guar.thy to show that programs are partially ordered*) |
|
89 bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq); |
|
90 |
|
91 |
|
92 (*** preserves ***) |
|
93 |
|
94 val prems = |
|
95 Goalw [preserves_def] "(!!z. F : stable {s. v s = z}) ==> F : preserves v"; |
|
96 by (blast_tac (claset() addIs prems) 1); |
|
97 qed "preservesI"; |
|
98 |
|
99 Goalw [preserves_def, stable_def, constrains_def] |
|
100 "[| F : preserves v; act : Acts F; (s,s') : act |] ==> v s = v s'"; |
|
101 by (Force_tac 1); |
|
102 qed "preserves_imp_eq"; |
|
103 |
|
104 Goalw [preserves_def] |
|
105 "(F Join G : preserves v) = (F : preserves v & G : preserves v)"; |
|
106 by Auto_tac; |
|
107 qed "Join_preserves"; |
|
108 |
|
109 Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"; |
|
110 by (simp_tac (simpset() addsimps [JN_stable, preserves_def]) 1); |
|
111 by (Blast_tac 1); |
|
112 qed "JN_preserves"; |
|
113 |
|
114 Goal "SKIP : preserves v"; |
|
115 by (auto_tac (claset(), simpset() addsimps [preserves_def])); |
|
116 qed "SKIP_preserves"; |
|
117 |
|
118 AddIffs [Join_preserves, JN_preserves, SKIP_preserves]; |
|
119 |
|
120 Goalw [funPair_def] "(funPair f g) x = (f x, g x)"; |
|
121 by (Simp_tac 1); |
|
122 qed "funPair_apply"; |
|
123 Addsimps [funPair_apply]; |
|
124 |
|
125 Goal "preserves (funPair v w) = preserves v Int preserves w"; |
|
126 by (auto_tac (claset(), |
|
127 simpset() addsimps [preserves_def, stable_def, constrains_def])); |
|
128 by (Blast_tac 1); |
|
129 qed "preserves_funPair"; |
|
130 |
|
131 (* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *) |
|
132 AddIffs [preserves_funPair RS eqset_imp_iff]; |
|
133 |
|
134 |
|
135 Goal "(funPair f g) o h = funPair (f o h) (g o h)"; |
|
136 by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1); |
|
137 qed "funPair_o_distrib"; |
|
138 |
|
139 Goal "fst o (funPair f g) = f"; |
|
140 by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1); |
|
141 qed "fst_o_funPair"; |
|
142 |
|
143 Goal "snd o (funPair f g) = g"; |
|
144 by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1); |
|
145 qed "snd_o_funPair"; |
|
146 Addsimps [fst_o_funPair, snd_o_funPair]; |
|
147 |
|
148 Goal "preserves v <= preserves (w o v)"; |
|
149 by (force_tac (claset(), |
|
150 simpset() addsimps [preserves_def, stable_def, constrains_def]) 1); |
|
151 qed "subset_preserves_o"; |
|
152 |
|
153 Goal "preserves v <= stable {s. P (v s)}"; |
|
154 by (auto_tac (claset(), |
|
155 simpset() addsimps [preserves_def, stable_def, constrains_def])); |
|
156 by (rename_tac "s' s" 1); |
|
157 by (subgoal_tac "v s = v s'" 1); |
|
158 by (ALLGOALS Force_tac); |
|
159 qed "preserves_subset_stable"; |
|
160 |
|
161 Goal "preserves v <= increasing v"; |
|
162 by (auto_tac (claset(), |
|
163 simpset() addsimps [impOfSubs preserves_subset_stable, |
|
164 increasing_def])); |
|
165 qed "preserves_subset_increasing"; |
|
166 |
|
167 Goal "preserves id <= stable A"; |
|
168 by (force_tac (claset(), |
|
169 simpset() addsimps [preserves_def, stable_def, constrains_def]) 1); |
|
170 qed "preserves_id_subset_stable"; |
|
171 |
|
172 |
|
173 (** For use with def_UNION_ok_iff **) |
|
174 |
|
175 Goal "safety_prop (preserves v)"; |
|
176 by (auto_tac (claset() addIs [safety_prop_INTER1], |
|
177 simpset() addsimps [preserves_def])); |
|
178 qed "safety_prop_preserves"; |
|
179 AddIffs [safety_prop_preserves]; |
|
180 |
|
181 |
|
182 (** Some lemmas used only in Client.ML **) |
|
183 |
|
184 Goal "[| F : stable {s. P (v s) (w s)}; \ |
|
185 \ G : preserves v; G : preserves w |] \ |
|
186 \ ==> F Join G : stable {s. P (v s) (w s)}"; |
|
187 by (Asm_simp_tac 1); |
|
188 by (subgoal_tac "G: preserves (funPair v w)" 1); |
|
189 by (Asm_simp_tac 2); |
|
190 by (dres_inst_tac [("P1", "split ?Q")] |
|
191 (impOfSubs preserves_subset_stable) 1); |
|
192 by Auto_tac; |
|
193 qed "stable_localTo_stable2"; |
|
194 |
|
195 Goal "[| F : stable {s. v s <= w s}; G : preserves v; \ |
|
196 \ F Join G : Increasing w |] \ |
|
197 \ ==> F Join G : Stable {s. v s <= w s}"; |
|
198 by (auto_tac (claset(), |
|
199 simpset() addsimps [stable_def, Stable_def, Increasing_def, |
|
200 Constrains_def, all_conj_distrib])); |
|
201 by (blast_tac (claset() addIs [constrains_weaken]) 1); |
|
202 (*The G case remains*) |
|
203 by (auto_tac (claset(), |
|
204 simpset() addsimps [preserves_def, stable_def, constrains_def])); |
|
205 by (case_tac "act: Acts F" 1); |
|
206 by (Blast_tac 1); |
|
207 (*We have a G-action, so delete assumptions about F-actions*) |
|
208 by (thin_tac "ALL act:Acts F. ?P act" 1); |
|
209 by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1); |
|
210 by (subgoal_tac "v x = v xa" 1); |
|
211 by (Blast_tac 2); |
|
212 by Auto_tac; |
|
213 by (etac order_trans 1); |
|
214 by (Blast_tac 1); |
|
215 qed "Increasing_preserves_Stable"; |
|
216 |
|
217 (** component_of **) |
|
218 |
|
219 (* component_of is stronger than <= *) |
|
220 Goalw [component_def, component_of_def] |
|
221 "F component_of H ==> F <= H"; |
|
222 by (Blast_tac 1); |
|
223 qed "component_of_imp_component"; |
|
224 |
|
225 |
|
226 (* component_of satisfies many of the <='s properties *) |
|
227 Goalw [component_of_def] |
|
228 "F component_of F"; |
|
229 by (res_inst_tac [("x", "SKIP")] exI 1); |
|
230 by Auto_tac; |
|
231 qed "component_of_refl"; |
|
232 |
|
233 Goalw [component_of_def] |
|
234 "SKIP component_of F"; |
|
235 by Auto_tac; |
|
236 qed "component_of_SKIP"; |
|
237 |
|
238 Addsimps [component_of_refl, component_of_SKIP]; |
|
239 |
|
240 Goalw [component_of_def] |
|
241 "[| F component_of G; G component_of H |] ==> F component_of H"; |
|
242 by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); |
|
243 qed "component_of_trans"; |
|
244 |
|
245 bind_thm ("strict_component_of_eq", strict_component_of_def RS meta_eq_to_obj_eq); |
|
246 |
|
247 (** localize **) |
|
248 Goalw [localize_def] |
|
249 "Init (localize v F) = Init F"; |
|
250 by (Simp_tac 1); |
|
251 qed "localize_Init_eq"; |
|
252 |
|
253 Goalw [localize_def] |
|
254 "Acts (localize v F) = Acts F"; |
|
255 by (Simp_tac 1); |
|
256 qed "localize_Acts_eq"; |
|
257 |
|
258 Goalw [localize_def] |
|
259 "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"; |
|
260 by Auto_tac; |
|
261 qed "localize_AllowedActs_eq"; |
|
262 |
|
263 Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq]; |
|