author  paulson 
Mon, 07 Dec 1998 18:23:39 +0100  
changeset 6018  8131f37f4ba3 
parent 6012  1894bfc4aee9 
child 6295  351b3c2b0d83 
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*) 

5706  12 
claset_ref() := claset() delSWrapper record_split_name; 
5597  13 

14 
Delsimps [split_paired_All]; 

15 

16 

17 
(*** component ***) 

18 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

19 
Goalw [component_def] "component (SKIP (States F)) F"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

20 
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

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"; 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

24 
by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 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 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

29 
Goalw [component_def] "States F = States G ==> component F (F Join G)"; 
5968  30 
by (Blast_tac 1); 
31 
qed "component_Join1"; 

32 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

33 
Goalw [component_def] "States F = States G ==> component G (F Join G)"; 
5968  34 
by (simp_tac (simpset() addsimps [Join_commute]) 1); 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

35 
by (dtac sym 1); 
5968  36 
by (Blast_tac 1); 
37 
qed "component_Join2"; 

38 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

39 
Goalw [component_def, eqStates_def] 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

40 
"[ i : I; eqStates I F ] ==> component (F i) (JN i:I. (F i))"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

41 
by (force_tac (claset() addIs [JN_absorb], simpset()) 1); 
5968  42 
qed "component_JN"; 
43 

5597  44 
Goalw [component_def] "[ component F G; component G H ] ==> component F H"; 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

45 
by (force_tac (claset() addIs [Join_assoc RS sym], simpset()) 1); 
5597  46 
qed "component_trans"; 
47 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

48 
Goalw [component_def] "component F G ==> Acts F <= Acts G"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

49 
by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); 
5620  50 
qed "component_Acts"; 
5597  51 

52 
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

53 
by Auto_tac; 
5620  54 
qed "component_Init"; 
5597  55 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

56 
Goalw [component_def] "component F G ==> States F = States G"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

57 
by Auto_tac; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

58 
qed "component_States"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

59 

5597  60 
Goal "[ component F G; component G F ] ==> F=G"; 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

61 
by (blast_tac (claset() addSIs [program_equalityI, component_States, 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

62 
component_Init, component_Acts]) 1); 
5597  63 
qed "component_anti_sym"; 
64 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset

65 
Goalw [component_def] 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset

66 
"component F H = (EX G. F Join G = H & Disjoint F G)"; 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

67 
by (blast_tac (claset() addSIs [Disjoint_States_eq, 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

68 
Diff_Disjoint, Join_Diff2]) 1); 
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset

69 
qed "component_eq"; 
5597  70 

71 
(*** existential properties ***) 

72 

73 
Goalw [ex_prop_def] 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

74 
"[ ex_prop X; finite GG ] \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

75 
\ ==> eqStates GG (%x. x) > GG Int X ~= {} > (JN G:GG. G) : X"; 
5597  76 
by (etac finite_induct 1); 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

77 
by (Simp_tac 1); 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

78 
by (rename_tac "GG J" 1); 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

79 
by (full_simp_tac (simpset() addsimps [Int_insert_left]) 1); 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

80 
by (dres_inst_tac [("x","J")] spec 1); 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

81 
by (Force_tac 1); 
5597  82 
qed_spec_mp "ex1"; 
83 

84 
Goalw [ex_prop_def] 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

85 
"ALL GG. finite GG & eqStates GG (%x. x) & GG Int X ~= {} \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

86 
\ > (JN G:GG. G) : X ==> ex_prop X"; 
5597  87 
by (Clarify_tac 1); 
88 
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

89 
by Auto_tac; 
5597  90 
qed "ex2"; 
91 

92 
(*Chandy & Sanders take this as a definition*) 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

93 
Goal "ex_prop X = \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

94 
\ (ALL GG. finite GG & eqStates GG (%x. x) & GG Int X ~= {} \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

95 
\ > (JN G:GG. G) : X)"; 
5597  96 
by (blast_tac (claset() addIs [ex1,ex2]) 1); 
97 
qed "ex_prop_finite"; 

98 

99 
(*Their "equivalent definition" given at the end of section 3*) 

100 
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

101 
by Auto_tac; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

102 
by (rewrite_goals_tac [ex_prop_def, component_def]); 
5597  103 
by (Blast_tac 1); 
104 
by Safe_tac; 

105 
by (stac Join_commute 2); 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

106 
by (dtac sym 2); 
5597  107 
by (ALLGOALS Blast_tac); 
108 
qed "ex_prop_equiv"; 

109 

110 

111 
(*** universal properties ***) 

112 

113 
Goalw [uv_prop_def] 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

114 
"[ uv_prop X; finite GG ] \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

115 
\ ==> eqStates GG (%x. x) > GG <= X > (JN G:GG. G) : X"; 
5597  116 
by (etac finite_induct 1); 
117 
by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); 

118 
qed_spec_mp "uv1"; 

119 

120 
Goalw [uv_prop_def] 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

121 
"ALL GG. finite GG & eqStates GG (%x. x) & GG <= X \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

122 
\ > (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

123 
by (rtac conjI 1); 
5597  124 
by (Clarify_tac 2); 
125 
by (dres_inst_tac [("x", "{F,G}")] spec 2); 

126 
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

127 
by Auto_tac; 
5597  128 
qed "uv2"; 
129 

130 
(*Chandy & Sanders take this as a definition*) 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

131 
Goal "uv_prop X = (ALL GG. finite GG & eqStates GG (%x. x) & GG <= X \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

132 
\ > (JN G:GG. G) : X)"; 
5597  133 
by (blast_tac (claset() addIs [uv1,uv2]) 1); 
134 
qed "uv_prop_finite"; 

135 

136 

137 
(*** guarantees ***) 

138 

5668  139 
(*This equation is more intuitive than the official definition*) 
5968  140 
Goal "(F : X guarantees Y) = \ 
141 
\ (ALL G. F Join G : X & Disjoint F G > F Join G : Y)"; 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset

142 
by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1); 
5668  143 
by (Blast_tac 1); 
144 
qed "guarantees_eq"; 

145 

5597  146 
Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV"; 
147 
by (Blast_tac 1); 

148 
qed "subset_imp_guarantees"; 

149 

5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

150 
(*Remark at end of section 4.1*) 
5597  151 
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

152 
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

153 
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

154 
qed "ex_prop_equiv2"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

155 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

156 
Goalw [guarantees_def] 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

157 
"(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

158 
by (Blast_tac 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

159 
qed "INT_guarantees_left"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

160 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

161 
Goalw [guarantees_def] 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

162 
"(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

163 
by (Blast_tac 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

164 
qed "INT_guarantees_right"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

165 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

166 
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

167 
by (Blast_tac 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

168 
qed "shunting"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

169 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

170 
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

171 
by (Blast_tac 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

172 
qed "contrapositive"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

173 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

174 
Goalw [guarantees_def] 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

175 
"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

176 
by (Blast_tac 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

177 
qed "combining1"; 
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 [guarantees_def] 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

180 
"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

181 
by (Blast_tac 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

182 
qed "combining2"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

183 

5630  184 
Goalw [guarantees_def] 
5968  185 
"ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"; 
5630  186 
by (Blast_tac 1); 
187 
qed "all_guarantees"; 

188 

189 
Goalw [guarantees_def] 

5968  190 
"EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"; 
5630  191 
by (Blast_tac 1); 
192 
qed "ex_guarantees"; 

193 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset

194 
val prems = Goal 
5968  195 
"(!!G. [ F Join G : X; Disjoint F G ] ==> F Join G : Y) \ 
196 
\ ==> F : X guarantees Y"; 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset

197 
by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1); 
5630  198 
by (blast_tac (claset() addIs prems) 1); 
199 
qed "guaranteesI"; 

200 

5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset

201 
Goalw [guarantees_def, component_def] 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

202 
"[ F : X guarantees Y; F Join G : X; States F = States G ] \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

203 
\ ==> F Join G : Y"; 
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5706
diff
changeset

204 
by (Blast_tac 1); 
5637  205 
qed "guaranteesD"; 
206 

5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

207 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

208 
(*** welldefinedness ***) 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

209 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

210 
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

211 
by Auto_tac; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

212 
qed "Join_welldef_D1"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

213 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

214 
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

215 
by Auto_tac; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

216 
qed "Join_welldef_D2"; 
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 
(*** refinement ***) 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

219 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

220 
Goalw [refines_def] "F refines F wrt X"; 
5597  221 
by (Blast_tac 1); 
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

222 
qed "refines_refl"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

223 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

224 
Goalw [refines_def] 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

225 
"[ 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

226 
by Auto_tac; 
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

227 
qed "refines_trans"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

228 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

229 
Goalw [strict_ex_prop_def] 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

230 
"[ strict_ex_prop X; States F = States G ] \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

231 
\ ==> (ALL H. States F = States H & F Join H : X > G Join H : X) = \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

232 
\ (F:X > G:X)"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

233 
by Safe_tac; 
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

234 
by (Blast_tac 1); 
6018  235 
by Auto_tac; 
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

236 
qed "strict_ex_refine_lemma"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

237 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

238 
Goalw [strict_ex_prop_def] 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

239 
"[ strict_ex_prop X; States F = States G ] \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

240 
\ ==> (ALL H. States F = States H & F Join H : welldef & F Join H : X \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

241 
\ > G Join H : X) = \ 
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

242 
\ (F: welldef Int X > G:X)"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

243 
by Safe_tac; 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

244 
by (eres_inst_tac [("x","SKIP ?A"), ("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

245 
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

246 
qed "strict_ex_refine_lemma_v"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

247 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

248 
Goal "[ strict_ex_prop X; States F = States G; \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

249 
\ ALL H. States F = States H & F Join H : welldef Int X \ 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

250 
\ > G Join H : welldef ] \ 
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

251 
\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; 
6018  252 
by (dtac sym 1); 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

253 
by (res_inst_tac [("x","SKIP (States G)")] allE 1 
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

254 
THEN assume_tac 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

255 
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

256 
strict_ex_refine_lemma_v]) 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

257 
qed "ex_refinement_thm"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

258 

6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

259 

1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

260 
(*** 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

261 

1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

262 

5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

263 
Goalw [strict_uv_prop_def] 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

264 
"strict_uv_prop X \ 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

265 
\ ==> (ALL H. States F = States 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

266 
by (Blast_tac 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

267 
qed "strict_uv_refine_lemma"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

268 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

269 
Goalw [strict_uv_prop_def] 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

270 
"strict_uv_prop X \ 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

271 
\ ==> (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

272 
\ (F: welldef Int X > G:X)"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

273 
by Safe_tac; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

274 
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

275 
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

276 
simpset())); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

277 
qed "strict_uv_refine_lemma_v"; 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

278 

e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

279 
Goal "[ strict_uv_prop X; \ 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

280 
\ 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

281 
\ ==> (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

282 
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

283 
THEN assume_tac 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

284 
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

285 
strict_uv_refine_lemma_v]) 1); 
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset

286 
qed "uv_refinement_thm"; 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5968
diff
changeset

287 
***) 