author  paulson 
Mon, 19 Oct 1998 11:25:37 +0200  
changeset 5668  9ddc4e836d3e 
parent 5637  a06006a320a1 
child 5701  e57980ec351b 
permissions  rwrr 
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 blowup*) 

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 
(*** welldefinedness ***) 
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"; 