author | paulson |
Mon, 19 Oct 1998 11:25:37 +0200 | |
changeset 5668 | 9ddc4e836d3e |
parent 5637 | a06006a320a1 |
child 5701 | e57980ec351b |
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 |
(*split_all_tac causes a big blow-up*) |
|
12 |
claset_ref() := claset() delSWrapper "split_all_tac"; |
|
13 |
||
14 |
Delsimps [split_paired_All]; |
|
15 |
||
16 |
||
17 |
(*** component ***) |
|
18 |
||
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
19 |
Goalw [component_def] "component SKIP F"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
20 |
by (blast_tac (claset() addIs [Join_SKIP_left]) 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
21 |
qed "component_SKIP"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
22 |
|
5597 | 23 |
Goalw [component_def] "component F F"; |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
24 |
by (blast_tac (claset() addIs [Join_SKIP_right]) 1); |
5597 | 25 |
qed "component_refl"; |
26 |
||
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
27 |
AddIffs [component_SKIP, component_refl]; |
5597 | 28 |
|
29 |
Goalw [component_def] "[| component F G; component G H |] ==> component F H"; |
|
30 |
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); |
|
31 |
qed "component_trans"; |
|
32 |
||
33 |
Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G"; |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
34 |
by Auto_tac; |
5620 | 35 |
qed "component_Acts"; |
5597 | 36 |
|
37 |
Goalw [component_def,Join_def] "component F G ==> Init G <= Init F"; |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
38 |
by Auto_tac; |
5620 | 39 |
qed "component_Init"; |
5597 | 40 |
|
41 |
Goal "[| component F G; component G F |] ==> F=G"; |
|
42 |
by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI, |
|
5620 | 43 |
component_Acts, component_Init]) 1); |
5597 | 44 |
qed "component_anti_sym"; |
45 |
||
46 |
||
47 |
(*** existential properties ***) |
|
48 |
||
49 |
Goalw [ex_prop_def] |
|
50 |
"[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X"; |
|
51 |
by (etac finite_induct 1); |
|
52 |
by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); |
|
53 |
qed_spec_mp "ex1"; |
|
54 |
||
55 |
Goalw [ex_prop_def] |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
56 |
"ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X"; |
5597 | 57 |
by (Clarify_tac 1); |
58 |
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
|
59 |
by Auto_tac; |
5597 | 60 |
qed "ex2"; |
61 |
||
62 |
(*Chandy & Sanders take this as a definition*) |
|
63 |
Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)"; |
|
64 |
by (blast_tac (claset() addIs [ex1,ex2]) 1); |
|
65 |
qed "ex_prop_finite"; |
|
66 |
||
67 |
(*Their "equivalent definition" given at the end of section 3*) |
|
68 |
Goal "ex_prop X = (ALL G. G:X = (ALL H. component G H --> H: X))"; |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
69 |
by Auto_tac; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
70 |
by (rewrite_goals_tac [ex_prop_def, component_def]); |
5597 | 71 |
by (Blast_tac 1); |
72 |
by Safe_tac; |
|
73 |
by (stac Join_commute 2); |
|
74 |
by (ALLGOALS Blast_tac); |
|
75 |
qed "ex_prop_equiv"; |
|
76 |
||
77 |
||
78 |
(*** universal properties ***) |
|
79 |
||
80 |
Goalw [uv_prop_def] |
|
81 |
"[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X"; |
|
82 |
by (etac finite_induct 1); |
|
83 |
by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); |
|
84 |
qed_spec_mp "uv1"; |
|
85 |
||
86 |
Goalw [uv_prop_def] |
|
87 |
"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
|
88 |
by (rtac conjI 1); |
5597 | 89 |
by (Clarify_tac 2); |
90 |
by (dres_inst_tac [("x", "{F,G}")] spec 2); |
|
91 |
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
|
92 |
by Auto_tac; |
5597 | 93 |
qed "uv2"; |
94 |
||
95 |
(*Chandy & Sanders take this as a definition*) |
|
96 |
Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)"; |
|
97 |
by (blast_tac (claset() addIs [uv1,uv2]) 1); |
|
98 |
qed "uv_prop_finite"; |
|
99 |
||
100 |
||
101 |
(*** guarantees ***) |
|
102 |
||
5668 | 103 |
(*This equation is more intuitive than the official definition*) |
104 |
Goalw [guarantees_def, component_def] |
|
105 |
"(F : A guarantees B) = (ALL G. F Join G : A --> F Join G : B)"; |
|
106 |
by (Blast_tac 1); |
|
107 |
qed "guarantees_eq"; |
|
108 |
||
5597 | 109 |
Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV"; |
110 |
by (Blast_tac 1); |
|
111 |
qed "subset_imp_guarantees"; |
|
112 |
||
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
113 |
(*Remark at end of section 4.1*) |
5597 | 114 |
Goalw [guarantees_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
|
115 |
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
|
116 |
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
|
117 |
qed "ex_prop_equiv2"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
118 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
119 |
Goalw [guarantees_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
120 |
"(INT X:XX. X guarantees Y) = (UN X:XX. X) guarantees Y"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
121 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
122 |
qed "INT_guarantees_left"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
123 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
124 |
Goalw [guarantees_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
125 |
"(INT Y:YY. X guarantees Y) = X guarantees (INT Y:YY. Y)"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
126 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
127 |
qed "INT_guarantees_right"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
128 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
129 |
Goalw [guarantees_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
130 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
131 |
qed "shunting"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
132 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
133 |
Goalw [guarantees_def] "(X guarantees Y) = -Y guarantees -X"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
134 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
135 |
qed "contrapositive"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
136 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
137 |
Goalw [guarantees_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
138 |
"V guarantees X Int ((X Int Y) guarantees Z) <= (V Int Y) guarantees Z"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
139 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
140 |
qed "combining1"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
141 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
142 |
Goalw [guarantees_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
143 |
"V guarantees (X Un Y) Int (Y guarantees Z) <= V guarantees (X Un Z)"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
144 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
145 |
qed "combining2"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
146 |
|
5630 | 147 |
Goalw [guarantees_def] |
148 |
"ALL z:I. F : A guarantees (B z) ==> F : A guarantees (INT z:I. B z)"; |
|
149 |
by (Blast_tac 1); |
|
150 |
qed "all_guarantees"; |
|
151 |
||
152 |
Goalw [guarantees_def] |
|
153 |
"EX z:I. F : A guarantees (B z) ==> F : A guarantees (UN z:I. B z)"; |
|
154 |
by (Blast_tac 1); |
|
155 |
qed "ex_guarantees"; |
|
156 |
||
157 |
val prems = Goalw [guarantees_def, component_def] |
|
158 |
"(!!G. F Join G : A ==> F Join G : B) ==> F : A guarantees B"; |
|
159 |
by (blast_tac (claset() addIs prems) 1); |
|
160 |
qed "guaranteesI"; |
|
161 |
||
5637 | 162 |
Goal "[| F : A guarantees B; F Join G : A |] ==> F Join G : B"; |
163 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_eq]) 1); |
|
164 |
qed "guaranteesD"; |
|
165 |
||
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
166 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
167 |
(*** well-definedness ***) |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
168 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
169 |
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
|
170 |
by Auto_tac; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
171 |
qed "Join_welldef_D1"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
172 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
173 |
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
|
174 |
by Auto_tac; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
175 |
qed "Join_welldef_D2"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
176 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
177 |
(*** refinement ***) |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
178 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
179 |
Goalw [refines_def] "F refines F wrt X"; |
5597 | 180 |
by (Blast_tac 1); |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
181 |
qed "refines_refl"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
182 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
183 |
Goalw [refines_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
184 |
"[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
185 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
186 |
qed "refines_trans"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
187 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
188 |
Goalw [strict_ex_prop_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
189 |
"strict_ex_prop X \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
190 |
\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
191 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
192 |
qed "strict_ex_refine_lemma"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
193 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
194 |
Goalw [strict_ex_prop_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
195 |
"strict_ex_prop X \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
196 |
\ ==> (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
|
197 |
\ (F: welldef Int X --> G:X)"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
198 |
by Safe_tac; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
199 |
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
|
200 |
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
|
201 |
qed "strict_ex_refine_lemma_v"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
202 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
203 |
Goal "[| strict_ex_prop X; \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
204 |
\ 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
|
205 |
\ ==> (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
|
206 |
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
|
207 |
THEN assume_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
208 |
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
|
209 |
strict_ex_refine_lemma_v]) 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
210 |
qed "ex_refinement_thm"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
211 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
212 |
Goalw [strict_uv_prop_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
213 |
"strict_uv_prop X \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
214 |
\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
215 |
by (Blast_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
216 |
qed "strict_uv_refine_lemma"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
217 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
218 |
Goalw [strict_uv_prop_def] |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
219 |
"strict_uv_prop X \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
220 |
\ ==> (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
|
221 |
\ (F: welldef Int X --> G:X)"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
222 |
by Safe_tac; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
223 |
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
|
224 |
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
|
225 |
simpset())); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
226 |
qed "strict_uv_refine_lemma_v"; |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
227 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
228 |
Goal "[| strict_uv_prop X; \ |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
229 |
\ 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
|
230 |
\ ==> (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
|
231 |
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
|
232 |
THEN assume_tac 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
233 |
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
|
234 |
strict_uv_refine_lemma_v]) 1); |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
235 |
qed "uv_refinement_thm"; |