author | paulson |
Thu, 26 Aug 1999 11:36:04 +0200 | |
changeset 7361 | 477e1bdf230f |
parent 7340 | a22efb7a522b |
child 7386 | 1048bc161c05 |
permissions | -rw-r--r-- |
5597 | 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 |
||
8 |
From Chandy and Sanders, "Reasoning About Program Composition" |
|
9 |
*) |
|
10 |
||
11 |
(*** component ***) |
|
12 |
||
6738
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
13 |
Goalw [component_def] |
7361 | 14 |
"H component F | H component G ==> H component (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] |
|
6738
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
22 |
"(F component G) = (Init G <= Init F & Acts F <= Acts G)"; |
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
23 |
by (force_tac (claset() addSIs [exI, program_equalityI], |
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
24 |
simpset() addsimps [Acts_Join]) 1); |
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
25 |
qed "component_eq_subset"; |
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
26 |
|
6646 | 27 |
Goalw [component_def] "SKIP component F"; |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset
|
28 |
by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1); |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
29 |
qed "component_SKIP"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
30 |
|
6646 | 31 |
Goalw [component_def] "F component F"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
32 |
by (blast_tac (claset() addIs [Join_SKIP_right]) 1); |
5597 | 33 |
qed "component_refl"; |
34 |
||
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
35 |
AddIffs [component_SKIP, component_refl]; |
5597 | 36 |
|
6833 | 37 |
Goal "F component SKIP ==> F = SKIP"; |
38 |
by (auto_tac (claset() addSIs [program_equalityI], |
|
39 |
simpset() addsimps [component_eq_subset])); |
|
40 |
qed "SKIP_minimal"; |
|
41 |
||
6646 | 42 |
Goalw [component_def] "F component (F Join G)"; |
5968 | 43 |
by (Blast_tac 1); |
44 |
qed "component_Join1"; |
|
45 |
||
6646 | 46 |
Goalw [component_def] "G component (F Join G)"; |
5968 | 47 |
by (simp_tac (simpset() addsimps [Join_commute]) 1); |
48 |
by (Blast_tac 1); |
|
49 |
qed "component_Join2"; |
|
50 |
||
6646 | 51 |
Goalw [component_def] "i : I ==> (F i) component (JN i:I. (F i))"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
52 |
by (blast_tac (claset() addIs [JN_absorb]) 1); |
5968 | 53 |
qed "component_JN"; |
54 |
||
6646 | 55 |
Goalw [component_def] "[| F component G; G component H |] ==> F component H"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
56 |
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); |
5597 | 57 |
qed "component_trans"; |
58 |
||
6646 | 59 |
Goal "[| F component G; G component F |] ==> F=G"; |
6738
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
60 |
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
06189132c67b
component_eq_subset: a neat characterization of "component"
paulson
parents:
6703
diff
changeset
|
61 |
by (blast_tac (claset() addSIs [program_equalityI]) 1); |
6703 | 62 |
qed "component_antisym"; |
5597 | 63 |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset
|
64 |
Goalw [component_def] |
6646 | 65 |
"F component H = (EX G. F Join G = H & Disjoint F G)"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
66 |
by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset
|
67 |
qed "component_eq"; |
5597 | 68 |
|
6833 | 69 |
Goal "((F Join G) component H) = (F component H & G component H)"; |
70 |
by (simp_tac (simpset() addsimps [component_eq_subset, Acts_Join]) 1); |
|
71 |
by (Blast_tac 1); |
|
72 |
qed "Join_component_iff"; |
|
73 |
||
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
74 |
|
5597 | 75 |
(*** existential properties ***) |
76 |
||
77 |
Goalw [ex_prop_def] |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
78 |
"[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X"; |
5597 | 79 |
by (etac finite_induct 1); |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
80 |
by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); |
5597 | 81 |
qed_spec_mp "ex1"; |
82 |
||
83 |
Goalw [ex_prop_def] |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
84 |
"ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X"; |
5597 | 85 |
by (Clarify_tac 1); |
86 |
by (dres_inst_tac [("x", "{F,G}")] spec 1); |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
87 |
by Auto_tac; |
5597 | 88 |
qed "ex2"; |
89 |
||
90 |
(*Chandy & Sanders take this as a definition*) |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
91 |
Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)"; |
5597 | 92 |
by (blast_tac (claset() addIs [ex1,ex2]) 1); |
93 |
qed "ex_prop_finite"; |
|
94 |
||
95 |
(*Their "equivalent definition" given at the end of section 3*) |
|
6646 | 96 |
Goal "ex_prop X = (ALL G. G:X = (ALL H. G component H --> H: X))"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
97 |
by Auto_tac; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
98 |
by (rewrite_goals_tac [ex_prop_def, component_def]); |
5597 | 99 |
by (Blast_tac 1); |
100 |
by Safe_tac; |
|
101 |
by (stac Join_commute 2); |
|
102 |
by (ALLGOALS Blast_tac); |
|
103 |
qed "ex_prop_equiv"; |
|
104 |
||
105 |
||
106 |
(*** universal properties ***) |
|
107 |
||
108 |
Goalw [uv_prop_def] |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
109 |
"[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X"; |
5597 | 110 |
by (etac finite_induct 1); |
111 |
by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); |
|
112 |
qed_spec_mp "uv1"; |
|
113 |
||
114 |
Goalw [uv_prop_def] |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
115 |
"ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X ==> uv_prop X"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
116 |
by (rtac conjI 1); |
5597 | 117 |
by (Clarify_tac 2); |
118 |
by (dres_inst_tac [("x", "{F,G}")] spec 2); |
|
119 |
by (dres_inst_tac [("x", "{}")] spec 1); |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
120 |
by Auto_tac; |
5597 | 121 |
qed "uv2"; |
122 |
||
123 |
(*Chandy & Sanders take this as a definition*) |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
124 |
Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)"; |
5597 | 125 |
by (blast_tac (claset() addIs [uv1,uv2]) 1); |
126 |
qed "uv_prop_finite"; |
|
127 |
||
128 |
||
129 |
(*** guarantees ***) |
|
130 |
||
6833 | 131 |
val prems = Goal |
132 |
"(!!G. [| F Join G : X; Disjoint F G |] ==> F Join G : Y) \ |
|
7361 | 133 |
\ ==> F : X guarantees Y"; |
134 |
by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1); |
|
6833 | 135 |
by (blast_tac (claset() addIs prems) 1); |
136 |
qed "guaranteesI"; |
|
137 |
||
7361 | 138 |
Goalw [guar_def, component_def] |
139 |
"[| F : X guarantees Y; F Join G : X |] ==> F Join G : Y"; |
|
6833 | 140 |
by (Blast_tac 1); |
141 |
qed "guaranteesD"; |
|
142 |
||
7361 | 143 |
(*This version of guaranteesD matches more easily in the conclusion*) |
144 |
Goalw [guar_def] |
|
145 |
"[| F : X guarantees Y; H : X; F component H |] ==> H : Y"; |
|
146 |
by (Blast_tac 1); |
|
147 |
qed "component_guaranteesD"; |
|
148 |
||
5668 | 149 |
(*This equation is more intuitive than the official definition*) |
7361 | 150 |
Goal "(F : X guarantees Y) = \ |
5968 | 151 |
\ (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)"; |
7361 | 152 |
by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1); |
5668 | 153 |
by (Blast_tac 1); |
154 |
qed "guarantees_eq"; |
|
155 |
||
7361 | 156 |
Goalw [guar_def] |
157 |
"[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"; |
|
6833 | 158 |
by (Blast_tac 1); |
159 |
qed "guarantees_weaken"; |
|
160 |
||
7361 | 161 |
Goalw [guar_def] |
162 |
"[| F: X guarantees Y; F component F' |] ==> F': X guarantees Y"; |
|
6833 | 163 |
by (blast_tac (claset() addIs [component_trans]) 1); |
164 |
qed "guarantees_weaken_prog"; |
|
165 |
||
7361 | 166 |
Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV"; |
5597 | 167 |
by (Blast_tac 1); |
6646 | 168 |
qed "subset_imp_guarantees_UNIV"; |
169 |
||
170 |
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) |
|
7361 | 171 |
Goalw [guar_def] "X <= Y ==> F : X guarantees Y"; |
6646 | 172 |
by (Blast_tac 1); |
5597 | 173 |
qed "subset_imp_guarantees"; |
174 |
||
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
175 |
(*Remark at end of section 4.1*) |
7361 | 176 |
Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
177 |
by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
178 |
by (blast_tac (claset() addEs [equalityE]) 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
179 |
qed "ex_prop_equiv2"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
180 |
|
6822 | 181 |
(** Distributive laws. Re-orient to perform miniscoping **) |
182 |
||
7361 | 183 |
Goalw [guar_def] |
184 |
"(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"; |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
185 |
by (Blast_tac 1); |
6822 | 186 |
qed "guarantees_UN_left"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
187 |
|
7361 | 188 |
Goalw [guar_def] |
189 |
"(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"; |
|
6822 | 190 |
by (Blast_tac 1); |
191 |
qed "guarantees_Un_left"; |
|
192 |
||
7361 | 193 |
Goalw [guar_def] |
194 |
"X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"; |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
195 |
by (Blast_tac 1); |
6822 | 196 |
qed "guarantees_INT_right"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
197 |
|
7361 | 198 |
Goalw [guar_def] |
199 |
"Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"; |
|
6822 | 200 |
by (Blast_tac 1); |
201 |
qed "guarantees_Int_right"; |
|
202 |
||
7361 | 203 |
Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
204 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
205 |
qed "shunting"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
206 |
|
7361 | 207 |
Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
208 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
209 |
qed "contrapositive"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
210 |
|
6646 | 211 |
(** The following two can be expressed using intersection and subset, which |
212 |
is more faithful to the text but looks cryptic. |
|
213 |
**) |
|
214 |
||
7361 | 215 |
Goalw [guar_def] |
216 |
"[| F : V guarantees X; F : (X Int Y) guarantees Z |]\ |
|
217 |
\ ==> F : (V Int Y) guarantees Z"; |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
218 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
219 |
qed "combining1"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
220 |
|
7361 | 221 |
Goalw [guar_def] |
222 |
"[| F : V guarantees (X Un Y); F : Y guarantees Z |]\ |
|
223 |
\ ==> F : V guarantees (X Un Z)"; |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
224 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
225 |
qed "combining2"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
226 |
|
6646 | 227 |
(** The following two follow Chandy-Sanders, but the use of object-quantifiers |
228 |
does not suit Isabelle... **) |
|
229 |
||
7361 | 230 |
(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) |
231 |
Goalw [guar_def] |
|
232 |
"ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"; |
|
5630 | 233 |
by (Blast_tac 1); |
234 |
qed "all_guarantees"; |
|
235 |
||
7361 | 236 |
(*Premises should be [| F: X guarantees Y i; i: I |] *) |
237 |
Goalw [guar_def] |
|
238 |
"EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"; |
|
5630 | 239 |
by (Blast_tac 1); |
240 |
qed "ex_guarantees"; |
|
241 |
||
6833 | 242 |
(*** Additional guarantees laws, by lcp ***) |
243 |
||
7361 | 244 |
Goalw [guar_def] |
245 |
"[| F: U guarantees V; G: X guarantees Y |] \ |
|
246 |
\ ==> F Join G: (U Int X) guarantees (V Int Y)"; |
|
6833 | 247 |
by (simp_tac (simpset() addsimps [Join_component_iff]) 1); |
248 |
by (Blast_tac 1); |
|
249 |
qed "guarantees_Join_Int"; |
|
250 |
||
7361 | 251 |
Goalw [guar_def] |
252 |
"[| F: U guarantees V; G: X guarantees Y |] \ |
|
253 |
\ ==> F Join G: (U Un X) guarantees (V Un Y)"; |
|
6833 | 254 |
by (simp_tac (simpset() addsimps [Join_component_iff]) 1); |
255 |
by (Blast_tac 1); |
|
256 |
qed "guarantees_Join_Un"; |
|
5630 | 257 |
|
6833 | 258 |
Goal "((JOIN I F) component H) = (ALL i: I. F i component H)"; |
259 |
by (simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1); |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset
|
260 |
by (Blast_tac 1); |
6833 | 261 |
qed "JN_component_iff"; |
262 |
||
7361 | 263 |
Goalw [guar_def] |
264 |
"[| ALL i:I. F i : X i guarantees Y i |] \ |
|
265 |
\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"; |
|
6833 | 266 |
by (simp_tac (simpset() addsimps [JN_component_iff]) 1); |
267 |
by (Blast_tac 1); |
|
7340
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
268 |
bind_thm ("guarantees_JN_INT", ballI RS result()); |
6833 | 269 |
|
7361 | 270 |
Goalw [guar_def] |
271 |
"[| ALL i:I. F i : X i guarantees Y i |] \ |
|
272 |
\ ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"; |
|
6833 | 273 |
by (simp_tac (simpset() addsimps [JN_component_iff]) 1); |
274 |
by (Blast_tac 1); |
|
7340
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
275 |
bind_thm ("guarantees_JN_UN", ballI RS result()); |
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
276 |
|
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
277 |
|
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
278 |
(*** guarantees laws for breaking down the program, by lcp ***) |
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
279 |
|
7361 | 280 |
Goalw [guar_def] |
281 |
"F: X guarantees Y | G: X guarantees Y ==> F Join G: X guarantees Y"; |
|
7340
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
282 |
by (simp_tac (simpset() addsimps [Join_component_iff]) 1); |
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
283 |
by (Blast_tac 1); |
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
284 |
qed "guarantees_Join_I"; |
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
285 |
|
7361 | 286 |
Goalw [guar_def] |
287 |
"[| i : I; F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y"; |
|
7340
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
288 |
by (simp_tac (simpset() addsimps [JN_component_iff]) 1); |
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
289 |
by (Blast_tac 1); |
a22efb7a522b
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
6833
diff
changeset
|
290 |
qed "guarantees_JN_I"; |
5637 | 291 |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
292 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
293 |
(*** well-definedness ***) |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
294 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
295 |
Goalw [welldef_def] "F Join G: welldef ==> F: welldef"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
296 |
by Auto_tac; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
297 |
qed "Join_welldef_D1"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
298 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
299 |
Goalw [welldef_def] "F Join G: welldef ==> G: welldef"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
300 |
by Auto_tac; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
301 |
qed "Join_welldef_D2"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
302 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
303 |
(*** refinement ***) |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
304 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
305 |
Goalw [refines_def] "F refines F wrt X"; |
5597 | 306 |
by (Blast_tac 1); |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
307 |
qed "refines_refl"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
308 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
309 |
Goalw [refines_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
310 |
"[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X"; |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset
|
311 |
by Auto_tac; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
312 |
qed "refines_trans"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
313 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
314 |
Goalw [strict_ex_prop_def] |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
315 |
"strict_ex_prop X \ |
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
316 |
\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
317 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
318 |
qed "strict_ex_refine_lemma"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
319 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
320 |
Goalw [strict_ex_prop_def] |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
321 |
"strict_ex_prop X \ |
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
322 |
\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \ |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
323 |
\ (F: welldef Int X --> G:X)"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
324 |
by Safe_tac; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
325 |
by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
326 |
by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset())); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
327 |
qed "strict_ex_refine_lemma_v"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
328 |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
329 |
Goal "[| strict_ex_prop X; \ |
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
330 |
\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \ |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
331 |
\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
332 |
by (res_inst_tac [("x","SKIP")] allE 1 |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
333 |
THEN assume_tac 1); |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
334 |
by (asm_full_simp_tac |
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
335 |
(simpset() addsimps [refines_def, iso_refines_def, |
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
336 |
strict_ex_refine_lemma_v]) 1); |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
337 |
qed "ex_refinement_thm"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
338 |
|
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset
|
339 |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
340 |
Goalw [strict_uv_prop_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
341 |
"strict_uv_prop X \ |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
342 |
\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
343 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
344 |
qed "strict_uv_refine_lemma"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
345 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
346 |
Goalw [strict_uv_prop_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
347 |
"strict_uv_prop X \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
348 |
\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
349 |
\ (F: welldef Int X --> G:X)"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
350 |
by Safe_tac; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
351 |
by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
352 |
by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
353 |
simpset())); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
354 |
qed "strict_uv_refine_lemma_v"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
355 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
356 |
Goal "[| strict_uv_prop X; \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
357 |
\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
358 |
\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
359 |
by (res_inst_tac [("x","SKIP")] allE 1 |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
360 |
THEN assume_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
361 |
by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def, |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
362 |
strict_uv_refine_lemma_v]) 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
363 |
qed "uv_refinement_thm"; |