11479
|
1 |
(* Title: ZF/UNITY/Comp.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Sidi O Ehmety, Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
Composition
|
|
6 |
From Chandy and Sanders, "Reasoning About Program Composition"
|
|
7 |
|
|
8 |
Revised by Sidi Ehmety on January 2001
|
|
9 |
|
|
10 |
*)
|
|
11 |
|
|
12 |
(*** component and strict_component relations ***)
|
|
13 |
|
|
14 |
Goalw [component_def]
|
|
15 |
"H component F | H component G ==> H component (F Join G)";
|
|
16 |
by Auto_tac;
|
|
17 |
by (res_inst_tac [("x", "Ga Join G")] exI 1);
|
|
18 |
by (res_inst_tac [("x", "G Join F")] exI 2);
|
|
19 |
by (auto_tac (claset(), simpset() addsimps Join_ac));
|
|
20 |
qed "componentI";
|
|
21 |
|
|
22 |
Goalw [component_def]
|
|
23 |
"G:program ==> (F component G) <-> \
|
|
24 |
\ (Init(G) <= Init(F) & Acts(F) <= Acts(G) & AllowedActs(G) <= AllowedActs(F))";
|
|
25 |
by Auto_tac;
|
|
26 |
by (rtac exI 1);
|
|
27 |
by (rtac program_equalityI 1);
|
|
28 |
by Auto_tac;
|
|
29 |
qed "component_eq_subset";
|
|
30 |
|
|
31 |
|
|
32 |
Goalw [component_def]
|
|
33 |
"F:program ==> SKIP component F";
|
|
34 |
by (res_inst_tac [("x", "F")] exI 1);
|
|
35 |
by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
|
|
36 |
qed "component_SKIP";
|
|
37 |
|
|
38 |
|
|
39 |
Goalw [component_def]
|
|
40 |
"F:program ==> F component F";
|
|
41 |
by (res_inst_tac [("x", "F")] exI 1);
|
|
42 |
by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 1);
|
|
43 |
qed "component_refl";
|
|
44 |
|
|
45 |
Addsimps [component_SKIP, component_refl];
|
|
46 |
|
|
47 |
Goal "F component SKIP ==> programify(F) = SKIP";
|
|
48 |
by (rtac program_equalityI 1);
|
|
49 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_eq_subset])));
|
|
50 |
by (Blast_tac 1);
|
|
51 |
qed "SKIP_minimal";
|
|
52 |
|
|
53 |
|
|
54 |
Goalw [component_def] "F component (F Join G)";
|
|
55 |
by (Blast_tac 1);
|
|
56 |
qed "component_Join1";
|
|
57 |
|
|
58 |
|
|
59 |
Goalw [component_def] "G component (F Join G)";
|
|
60 |
by (simp_tac (simpset() addsimps [Join_commute]) 1);
|
|
61 |
by (Blast_tac 1);
|
|
62 |
qed "component_Join2";
|
|
63 |
|
|
64 |
Goal "F component G ==> F Join G = G";
|
|
65 |
by (auto_tac (claset(), simpset()
|
|
66 |
addsimps [component_def, Join_left_absorb]));
|
|
67 |
qed "Join_absorb1";
|
|
68 |
|
|
69 |
Goal "G component F ==> F Join G = F";
|
|
70 |
by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
|
|
71 |
qed "Join_absorb2";
|
|
72 |
|
|
73 |
|
|
74 |
|
|
75 |
Goal "H:program ==> \
|
|
76 |
\ (JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)";
|
|
77 |
by (case_tac "I=0" 1);
|
|
78 |
by (Force_tac 1);
|
|
79 |
by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
|
|
80 |
by Auto_tac;
|
|
81 |
by (dres_inst_tac [("c", "xb"), ("A", "AllowedActs(H)")] subsetD 2);
|
|
82 |
by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1));
|
|
83 |
qed "JN_component_iff";
|
|
84 |
|
|
85 |
|
|
86 |
Goalw [component_def] "i : I ==> F(i) component (JN i:I. (F(i)))";
|
|
87 |
by (blast_tac (claset() addIs [JN_absorb]) 1);
|
|
88 |
qed "component_JN";
|
|
89 |
|
|
90 |
|
|
91 |
Goalw [component_def] "[| F component G; G component H |] ==> F component H";
|
|
92 |
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
|
|
93 |
qed "component_trans";
|
|
94 |
|
|
95 |
Goal "[| F:program; G:program |] ==> \
|
|
96 |
\ (F component G & G component F) --> F = G";
|
|
97 |
by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
|
|
98 |
by (Clarify_tac 1);
|
|
99 |
by (rtac program_equalityI 1);
|
|
100 |
by Auto_tac;
|
|
101 |
qed "component_antisym";
|
|
102 |
|
|
103 |
Goal "H:program ==> ((F Join G) component H) <-> (F component H & G component H)";
|
|
104 |
by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
|
|
105 |
by (Blast_tac 1);
|
|
106 |
qed "Join_component_iff";
|
|
107 |
|
|
108 |
|
|
109 |
Goal "[| F component G; G:A co B; F:program |] ==> F : A co B";
|
|
110 |
by (forward_tac [constrainsD2] 1);
|
|
111 |
by (rotate_tac ~1 1);
|
|
112 |
by (auto_tac (claset(),
|
|
113 |
simpset() addsimps [constrains_def, component_eq_subset]));
|
|
114 |
qed "component_constrains";
|
|
115 |
|
|
116 |
(*Used in Guar.thy to show that programs are partially ordered*)
|
|
117 |
(* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*)
|
|
118 |
|
|
119 |
|
|
120 |
(*** preserves ***)
|
|
121 |
|
|
122 |
val prems =
|
|
123 |
Goalw [preserves_def]
|
|
124 |
"ALL z. F:stable({s:state. f(s) = z}) ==> F:preserves(f)";
|
|
125 |
by Auto_tac;
|
|
126 |
by (blast_tac (claset() addDs [stableD2]) 1);
|
|
127 |
bind_thm("preservesI", allI RS result());
|
|
128 |
|
|
129 |
Goalw [preserves_def, stable_def, constrains_def]
|
|
130 |
"[| F:preserves(f); act : Acts(F); <s,t> : act |] ==> f(s) = f(t)";
|
|
131 |
by (subgoal_tac "s:state & t:state" 1);
|
|
132 |
by (blast_tac (claset() addSDs [ActsD]) 2);
|
|
133 |
by Auto_tac;
|
|
134 |
by (dres_inst_tac [("x", "f(s)")] spec 1);
|
|
135 |
by (dres_inst_tac [("x", "act")] bspec 1);
|
|
136 |
by Auto_tac;
|
|
137 |
qed "preserves_imp_eq";
|
|
138 |
|
|
139 |
Goalw [preserves_def]
|
|
140 |
"(F Join G : preserves(v)) <-> \
|
|
141 |
\ (programify(F) : preserves(v) & programify(G) : preserves(v))";
|
|
142 |
by (auto_tac (claset(), simpset() addsimps [INT_iff]));
|
|
143 |
qed "Join_preserves";
|
|
144 |
|
|
145 |
|
|
146 |
Goal "(JOIN(I,F): preserves(v)) <-> (ALL i:I. programify(F(i)):preserves(v))";
|
|
147 |
by (auto_tac (claset(), simpset() addsimps
|
|
148 |
[JN_stable, preserves_def, INT_iff]@state_simps));
|
|
149 |
qed "JN_preserves";
|
|
150 |
|
|
151 |
Goal "SKIP : preserves(v)";
|
|
152 |
by (auto_tac (claset(), simpset()
|
|
153 |
addsimps [preserves_def, INT_iff]@state_simps));
|
|
154 |
qed "SKIP_preserves";
|
|
155 |
|
|
156 |
AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
|
|
157 |
|
|
158 |
|
|
159 |
|
|
160 |
|
|
161 |
(** component_of **)
|
|
162 |
|
|
163 |
(* component_of is stronger than component *)
|
|
164 |
Goalw [component_def, component_of_def]
|
|
165 |
"F component_of H ==> F component H";
|
|
166 |
by (Blast_tac 1);
|
|
167 |
qed "component_of_imp_component";
|
|
168 |
|
|
169 |
|
|
170 |
|
|
171 |
(* component_of satisfies many of the <='s properties *)
|
|
172 |
Goalw [component_of_def]
|
|
173 |
"F:program ==> F component_of F";
|
|
174 |
by (res_inst_tac [("x", "SKIP")] exI 1);
|
|
175 |
by Auto_tac;
|
|
176 |
qed "component_of_refl";
|
|
177 |
|
|
178 |
|
|
179 |
|
|
180 |
Goalw [component_of_def]
|
|
181 |
"F:program ==>SKIP component_of F";
|
|
182 |
by Auto_tac;
|
|
183 |
by (res_inst_tac [("x", "F")] exI 1);
|
|
184 |
by Auto_tac;
|
|
185 |
qed "component_of_SKIP";
|
|
186 |
|
|
187 |
Addsimps [component_of_refl, component_of_SKIP];
|
|
188 |
|
|
189 |
|
|
190 |
|
|
191 |
Goalw [component_of_def]
|
|
192 |
"[| F component_of G; G component_of H |] ==> F component_of H";
|
|
193 |
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
|
|
194 |
qed "component_of_trans";
|
|
195 |
|
|
196 |
|
|
197 |
(** localize **)
|
|
198 |
Goalw [localize_def]
|
|
199 |
"Init(localize(v,F)) = Init(F)";
|
|
200 |
by (Simp_tac 1);
|
|
201 |
qed "localize_Init_eq";
|
|
202 |
|
|
203 |
|
|
204 |
Goalw [localize_def]
|
|
205 |
"Acts(localize(v,F)) = Acts(F)";
|
|
206 |
by (Simp_tac 1);
|
|
207 |
qed "localize_Acts_eq";
|
|
208 |
|
|
209 |
Goalw [localize_def]
|
|
210 |
"AllowedActs(localize(v,F)) = AllowedActs(F Int (UN G:preserves(v). Acts(G)))";
|
|
211 |
by Auto_tac;
|
|
212 |
qed "localize_AllowedActs_eq";
|
|
213 |
|
|
214 |
Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];
|