author  paulson 
Mon, 16 Nov 1998 10:39:30 +0100  
changeset 5867  1c4806b4bf43 
parent 5804  8e0a4c4fd67b 
child 5898  3e34e7aa7479 
permissions  rwrr 
5252  1 
(* Title: HOL/UNITY/Union.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6 
Unions of programs 

7 

8 
From Misra's Chapter 5: Asynchronous Compositions of Programs 

9 
*) 

10 

11 

5867  12 
(** SKIP **) 
13 

5648  14 
Goal "Init SKIP = UNIV"; 
15 
by (simp_tac (simpset() addsimps [SKIP_def]) 1); 

5611  16 
qed "Init_SKIP"; 
17 

5648  18 
Goal "Acts SKIP = {Id}"; 
19 
by (simp_tac (simpset() addsimps [SKIP_def]) 1); 

20 
qed "Acts_SKIP"; 

21 

22 
Addsimps [Init_SKIP, Acts_SKIP]; 

23 

5867  24 
Goal "reachable SKIP = UNIV"; 
25 
by (force_tac (claset() addIs reachable.intrs, simpset()) 1); 

26 
qed "reachable_SKIP"; 

27 

28 
Addsimps [reachable_SKIP]; 

29 

30 

31 
(** Join and JN **) 

32 

5611  33 
Goal "Init (F Join G) = Init F Int Init G"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

34 
by (simp_tac (simpset() addsimps [Join_def]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

35 
qed "Init_Join"; 
5252  36 

5611  37 
Goal "Acts (F Join G) = Acts F Un Acts G"; 
5596  38 
by (auto_tac (claset(), simpset() addsimps [Join_def])); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

39 
qed "Acts_Join"; 
5252  40 

5611  41 
Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

42 
by (simp_tac (simpset() addsimps [JOIN_def]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

43 
qed "Init_JN"; 
5252  44 

5611  45 
Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"; 
5596  46 
by (auto_tac (claset(), simpset() addsimps [JOIN_def])); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

47 
qed "Acts_JN"; 
5252  48 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

49 
Addsimps [Init_Join, Init_JN]; 
5259  50 

5867  51 
Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP"; 
52 
by Auto_tac; 

53 
qed "JN_empty"; 

54 

5611  55 
Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)"; 
56 
by (rtac program_equalityI 1); 

5596  57 
by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def]))); 
5584  58 
qed "JN_insert"; 
5867  59 
Addsimps[JN_empty, JN_insert]; 
5584  60 

61 

5611  62 
(** Algebraic laws **) 
5259  63 

5611  64 
Goal "F Join G = G Join F"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

65 
by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1); 
5259  66 
qed "Join_commute"; 
67 

5611  68 
Goal "(F Join G) Join H = F Join (G Join H)"; 
5596  69 
by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1); 
5259  70 
qed "Join_assoc"; 
5596  71 

5611  72 
Goalw [Join_def, SKIP_def] "SKIP Join F = F"; 
73 
by (rtac program_equalityI 1); 

5596  74 
by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); 
5611  75 
qed "Join_SKIP_left"; 
5584  76 

5611  77 
Goalw [Join_def, SKIP_def] "F Join SKIP = F"; 
78 
by (rtac program_equalityI 1); 

79 
by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); 

80 
qed "Join_SKIP_right"; 

81 

82 
Addsimps [Join_SKIP_left, Join_SKIP_right]; 

83 

84 
Goalw [Join_def] "F Join F = F"; 

85 
by (rtac program_equalityI 1); 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

86 
by Auto_tac; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

87 
qed "Join_absorb"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

88 

5611  89 
Addsimps [Join_absorb]; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

90 

5584  91 

92 

93 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

94 
(*** Safety: constrains, stable, FP ***) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

95 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

96 
Goalw [constrains_def, JOIN_def] 
5584  97 
"I ~= {} ==> \ 
5648  98 
\ (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)"; 
5596  99 
by (Simp_tac 1); 
100 
by (Blast_tac 1); 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

101 
qed "constrains_JN"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

102 

5648  103 
Goal "F Join G : constrains A B = \ 
104 
\ (F : constrains A B & G : constrains A B)"; 

5620  105 
by (auto_tac 
106 
(claset(), 

107 
simpset() addsimps [constrains_def, Join_def])); 

108 
qed "constrains_Join"; 

109 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

110 
(**FAILS, I think; see 5.4.1, Substitution Axiom. 
5620  111 
The problem is to relate reachable (F Join G) with 
112 
reachable F and reachable G 

113 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

114 
Goalw [Constrains_def] 
5648  115 
"(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

116 
by (simp_tac (simpset() addsimps [constrains_JN]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

117 
by (Blast_tac 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

118 
qed "Constrains_JN"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

119 

5648  120 
Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)"; 
5584  121 
by (auto_tac 
122 
(claset(), 

5620  123 
simpset() addsimps [Constrains_def, constrains_Join])); 
124 
qed "Constrains_Join"; 

125 
**) 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

126 

5648  127 
Goal "[ F : constrains A A'; G : constrains B B' ] \ 
128 
\ ==> F Join G : constrains (A Int B) (A' Un B')"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

129 
by (simp_tac (simpset() addsimps [constrains_Join]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

130 
by (blast_tac (claset() addIs [constrains_weaken]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

131 
qed "constrains_Join_weaken"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

132 

5584  133 
Goal "I ~= {} ==> \ 
5648  134 
\ (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"; 
5584  135 
by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

136 
qed "stable_JN"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

137 

5648  138 
Goal "F Join G : stable A = \ 
139 
\ (F : stable A & G : stable A)"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

140 
by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

141 
qed "stable_Join"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

142 

5648  143 
Goal "I ~= {} ==> FP (JN i:I. F i) = (INT i:I. FP (F i))"; 
5584  144 
by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

145 
qed "FP_JN"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

146 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

147 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

148 
(*** Progress: transient, ensures ***) 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

149 

5584  150 
Goal "I ~= {} ==> \ 
5648  151 
\ (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"; 
5584  152 
by (auto_tac (claset(), 
153 
simpset() addsimps [transient_def, JOIN_def])); 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

154 
qed "transient_JN"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

155 

5648  156 
Goal "F Join G : transient A = \ 
157 
\ (F : transient A  G : transient A)"; 

5584  158 
by (auto_tac (claset(), 
5596  159 
simpset() addsimps [bex_Un, transient_def, 
5584  160 
Join_def])); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

161 
qed "transient_Join"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

162 

5584  163 
Goal "I ~= {} ==> \ 
5648  164 
\ (JN i:I. F i) : ensures A B = \ 
165 
\ ((ALL i:I. F i : constrains (AB) (A Un B)) & \ 

166 
\ (EX i:I. F i : ensures A B))"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

167 
by (auto_tac (claset(), 
5584  168 
simpset() addsimps [ensures_def, constrains_JN, transient_JN])); 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

169 
qed "ensures_JN"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

170 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

171 
Goalw [ensures_def] 
5648  172 
"F Join G : ensures A B = \ 
173 
\ (F : constrains (AB) (A Un B) & \ 

174 
\ G : constrains (AB) (A Un B) & \ 

175 
\ (F : ensures A B  G : ensures A B))"; 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

176 
by (auto_tac (claset(), 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

177 
simpset() addsimps [constrains_Join, transient_Join])); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

178 
qed "ensures_Join"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

179 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

180 
Goalw [stable_def, constrains_def, Join_def] 
5648  181 
"[ F : stable A; G : constrains A A' ] \ 
182 
\ ==> F Join G : constrains A A'"; 

183 
by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1); 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

184 
by (Blast_tac 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

185 
qed "stable_constrains_Join"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

186 

5648  187 
(*Premise for G cannot use Invariant because Stable F A is weaker than 
188 
G : stable A *) 

189 
Goal "[ F : stable A; G : invariant A ] ==> F Join G : Invariant A"; 

190 
by (full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, 

191 
Stable_eq_stable, stable_Join]) 1); 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

192 
by (force_tac(claset() addIs [stable_reachable, stable_Int], 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

193 
simpset() addsimps [Acts_Join]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

194 
qed "stable_Join_Invariant"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

195 

5648  196 
Goal "[ F : stable A; G : ensures A B ] ==> F Join G : ensures A B"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

197 
by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

198 
by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

199 
by (etac constrains_weaken 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

200 
by Auto_tac; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

201 
qed "ensures_stable_Join1"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

202 

1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

203 
(*As above, but exchanging the roles of F and G*) 
5648  204 
Goal "[ F : ensures A B; G : stable A ] ==> F Join G : ensures A B"; 
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

205 
by (stac Join_commute 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

206 
by (blast_tac (claset() addIs [ensures_stable_Join1]) 1); 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

207 
qed "ensures_stable_Join2"; 
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset

208 

5648  209 

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

210 
(** Diff and localTo **) 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

211 

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

212 
Goalw [Join_def, Diff_def] "F Join (Diff G (Acts F)) = F Join G"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

213 
by (rtac program_equalityI 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

214 
by Auto_tac; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

215 
qed "Join_Diff2"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

216 

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

217 
Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

218 
by Auto_tac; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

219 
qed "Diff_Disjoint"; 
5648  220 

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

221 
Goal "[ F Join G : v localTo F; Disjoint F G ] \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

222 
\ ==> G : (INT z. stable {s. v s = z})"; 
5648  223 
by (asm_full_simp_tac 
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

224 
(simpset() addsimps [localTo_def, Diff_def, Disjoint_def, 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

225 
Acts_Join, stable_def, constrains_def]) 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

226 
by (Blast_tac 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

227 
qed "localTo_imp_stable"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

228 

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

229 
Goal "[ F Join G : v localTo F; (s,s') : act; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

230 
\ act : Acts G; Disjoint F G ] ==> v s' = v s"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

231 
by (asm_full_simp_tac 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

232 
(simpset() addsimps [localTo_def, Diff_def, Disjoint_def, 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

233 
Acts_Join, stable_def, constrains_def]) 1); 
5648  234 
by (Blast_tac 1); 
235 
qed "localTo_imp_equals"; 

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

236 

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

237 
Goalw [localTo_def, stable_def, constrains_def] 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

238 
"v localTo F <= (f o v) localTo F"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

239 
by (Clarify_tac 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

240 
by (auto_tac (claset() addSEs [allE, ballE], simpset())); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

241 
qed "localTo_imp_o_localTo"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

242 

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

243 

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

244 
(*** Higherlevel rules involving localTo and Join ***) 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

245 

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

246 
Goal "[ F : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

247 
\ F Join G : v localTo F; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

248 
\ F Join G : w localTo F; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

249 
\ Disjoint F G ] \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

250 
\ ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

251 
by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join])); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

252 
by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac)); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

253 
by Auto_tac; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

254 
qed "constrains_localTo_constrains2"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

255 

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

256 
Goalw [stable_def] 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

257 
"[ F : stable {s. P (v s) (w s)}; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

258 
\ F Join G : v localTo F; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

259 
\ F Join G : w localTo F; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

260 
\ Disjoint F G ] \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

261 
\ ==> F Join G : stable {s. P (v s) (w s)}"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

262 
by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

263 
qed "stable_localTo_stable2"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

264 

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

265 

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

266 
Goal "(UN k. {s. f s = k}) = UNIV"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

267 
by (Blast_tac 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

268 
qed "UN_eq_UNIV"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

269 

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

270 
Goal "[ F : stable {s. v s <= w s}; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

271 
\ F Join G : v localTo F; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

272 
\ F Join G : Increasing w; \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

273 
\ Disjoint F G ] \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

274 
\ ==> F Join G : Stable {s. v s <= w s}"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

275 
by (safe_tac (claset() addSDs [localTo_imp_stable])); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

276 
by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

277 
by (subgoal_tac "ALL k: UNIV. ?H : Constrains ({s. v s = k} Int ?AA) ?AA" 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

278 
by (dtac ball_Constrains_UN 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

279 
by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

280 
by (rtac ballI 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

281 
by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \ 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

282 
\ ({s. v s = k} Un {s. v s <= w s})" 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

283 
by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

284 
by (blast_tac (claset() addIs [constrains_weaken]) 2); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

285 
by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

286 
by (etac Constrains_weaken 2); 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

287 
by Auto_tac; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5785
diff
changeset

288 
qed "Increasing_localTo_Stable"; 