author  paulson 
Mon, 24 May 1999 15:50:23 +0200  
changeset 6712  d1bebb7f1c50 
parent 6536  281d44905cab 
child 7240  a509730e424b 
permissions  rwrr 
4776  1 
(* Title: HOL/UNITY/UNITY 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6 
The basic UNITY theory (revised version, based upon the "co" operator) 

7 

8 
From Misra, "A Logic for Concurrent Programming", 1994 

9 
*) 

10 

11 
set proof_timing; 

12 
HOL_quantifiers := false; 

13 

14 

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

15 
(*** General lemmas ***) 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

16 

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

17 
Goal "UNIV Times UNIV = UNIV"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

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

19 
qed "UNIV_Times_UNIV"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

20 
Addsimps [UNIV_Times_UNIV]; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

21 

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

22 
Goal " (UNIV Times A) = UNIV Times (A)"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

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

24 
qed "Compl_Times_UNIV1"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

25 

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

26 
Goal " (A Times UNIV) = (A) Times UNIV"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

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

28 
qed "Compl_Times_UNIV2"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

29 

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

30 
Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

31 

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

32 

6535  33 
(*** The abstract type of programs ***) 
34 

35 
val rep_ss = simpset() addsimps 

36 
[Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, 

37 
Rep_Program_inverse, Abs_Program_inverse]; 

38 

39 

40 
Goal "Id : Acts F"; 

41 
by (cut_inst_tac [("x", "F")] Rep_Program 1); 

42 
by (auto_tac (claset(), rep_ss)); 

43 
qed "Id_in_Acts"; 

44 
AddIffs [Id_in_Acts]; 

45 

46 
Goal "insert Id (Acts F) = Acts F"; 

47 
by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1); 

48 
qed "insert_Id_Acts"; 

49 
AddIffs [insert_Id_Acts]; 

50 

51 
(** Inspectors for type "program" **) 

52 

53 
Goal "Init (mk_program (init,acts)) = init"; 

54 
by (auto_tac (claset(), rep_ss)); 

55 
qed "Init_eq"; 

56 

57 
Goal "Acts (mk_program (init,acts)) = insert Id acts"; 

58 
by (auto_tac (claset(), rep_ss)); 

59 
qed "Acts_eq"; 

60 

61 
Addsimps [Acts_eq, Init_eq]; 

62 

63 

64 
(** The notation of equality for type "program" **) 

65 

66 
Goal "[ Init F = Init G; Acts F = Acts G ] ==> F = G"; 

67 
by (subgoals_tac ["EX x. Rep_Program F = x", 

68 
"EX x. Rep_Program G = x"] 1); 

69 
by (REPEAT (Blast_tac 2)); 

70 
by (Clarify_tac 1); 

71 
by (auto_tac (claset(), rep_ss)); 

72 
by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1)); 

73 
by (asm_full_simp_tac rep_ss 1); 

74 
qed "program_equalityI"; 

75 

76 
val [major,minor] = 

77 
Goal "[ F = G; [ Init F = Init G; Acts F = Acts G ] ==> P ] ==> P"; 

78 
by (rtac minor 1); 

79 
by (auto_tac (claset(), simpset() addsimps [major])); 

80 
qed "program_equalityE"; 

81 

82 

83 
(*** These rules allow "lazy" definition expansion 

84 
They avoid expanding the full program, which is a large expression 

85 
***) 

86 

87 
Goal "F == mk_program (init,acts) ==> Init F = init"; 

88 
by Auto_tac; 

89 
qed "def_prg_Init"; 

90 

91 
(*The program is not expanded, but its Init and Acts are*) 

92 
val [rew] = goal thy 

93 
"[ F == mk_program (init,acts) ] \ 

94 
\ ==> Init F = init & Acts F = insert Id acts"; 

95 
by (rewtac rew); 

96 
by Auto_tac; 

97 
qed "def_prg_simps"; 

98 

99 
(*An action is expanded only if a pair of states is being tested against it*) 

100 
Goal "[ act == {(s,s'). P s s'} ] ==> ((s,s') : act) = P s s'"; 

101 
by Auto_tac; 

102 
qed "def_act_simp"; 

103 

104 
fun simp_of_act def = def RS def_act_simp; 

105 

106 
(*A set is expanded only if an element is being tested against it*) 

107 
Goal "A == B ==> (x : A) = (x : B)"; 

108 
by Auto_tac; 

109 
qed "def_set_simp"; 

110 

111 
fun simp_of_set def = def RS def_set_simp; 

112 

113 

6536  114 
(*** co ***) 
4776  115 

6536  116 
overload_1st_set "UNITY.op co"; 
5648  117 
overload_1st_set "UNITY.stable"; 
118 
overload_1st_set "UNITY.unless"; 

5340  119 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset

120 
val prems = Goalw [constrains_def] 
5648  121 
"(!!act s s'. [ act: Acts F; (s,s') : act; s: A ] ==> s': A') \ 
6536  122 
\ ==> F : A co A'"; 
4776  123 
by (blast_tac (claset() addIs prems) 1); 
124 
qed "constrainsI"; 

125 

5069  126 
Goalw [constrains_def] 
6536  127 
"[ F : A co A'; act: Acts F; (s,s'): act; s: A ] ==> s': A'"; 
4776  128 
by (Blast_tac 1); 
129 
qed "constrainsD"; 

130 

6536  131 
Goalw [constrains_def] "F : {} co B"; 
4776  132 
by (Blast_tac 1); 
133 
qed "constrains_empty"; 

134 

6536  135 
Goalw [constrains_def] "F : A co UNIV"; 
4776  136 
by (Blast_tac 1); 
137 
qed "constrains_UNIV"; 

138 
AddIffs [constrains_empty, constrains_UNIV]; 

139 

5648  140 
(*monotonic in 2nd argument*) 
5069  141 
Goalw [constrains_def] 
6536  142 
"[ F : A co A'; A'<=B' ] ==> F : A co B'"; 
4776  143 
by (Blast_tac 1); 
144 
qed "constrains_weaken_R"; 

145 

5648  146 
(*antimonotonic in 1st argument*) 
5069  147 
Goalw [constrains_def] 
6536  148 
"[ F : A co A'; B<=A ] ==> F : B co A'"; 
4776  149 
by (Blast_tac 1); 
150 
qed "constrains_weaken_L"; 

151 

5069  152 
Goalw [constrains_def] 
6536  153 
"[ F : A co A'; B<=A; A'<=B' ] ==> F : B co B'"; 
4776  154 
by (Blast_tac 1); 
155 
qed "constrains_weaken"; 

156 

157 
(** Union **) 

158 

5069  159 
Goalw [constrains_def] 
6536  160 
"[ F : A co A'; F : B co B' ] \ 
161 
\ ==> F : (A Un B) co (A' Un B')"; 

4776  162 
by (Blast_tac 1); 
163 
qed "constrains_Un"; 

164 

5069  165 
Goalw [constrains_def] 
6536  166 
"ALL i:I. F : (A i) co (A' i) \ 
167 
\ ==> F : (UN i:I. A i) co (UN i:I. A' i)"; 

4776  168 
by (Blast_tac 1); 
169 
qed "ball_constrains_UN"; 

170 

171 
(** Intersection **) 

172 

5069  173 
Goalw [constrains_def] 
6536  174 
"[ F : A co A'; F : B co B' ] \ 
175 
\ ==> F : (A Int B) co (A' Int B')"; 

4776  176 
by (Blast_tac 1); 
177 
qed "constrains_Int"; 

178 

5069  179 
Goalw [constrains_def] 
6536  180 
"ALL i:I. F : (A i) co (A' i) \ 
181 
\ ==> F : (INT i:I. A i) co (INT i:I. A' i)"; 

4776  182 
by (Blast_tac 1); 
183 
qed "ball_constrains_INT"; 

184 

6536  185 
Goalw [constrains_def] "F : A co A' ==> A <= A'"; 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

186 
by Auto_tac; 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset

187 
qed "constrains_imp_subset"; 
4776  188 

6536  189 
(*The reasoning is by subsets since "co" refers to single actions 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

190 
only. So this rule isn't that useful.*) 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

191 
Goalw [constrains_def] 
6536  192 
"[ F : A co B; F : B co C ] ==> F : A co C"; 
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

193 
by (Blast_tac 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset

194 
qed "constrains_trans"; 
4776  195 

6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

196 
Goalw [constrains_def] 
6536  197 
"[ F : A co (A' Un B); F : B co B' ] \ 
198 
\ ==> F : A co (A' Un B')"; 

6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

199 
by (Clarify_tac 1); 
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset

200 
by (Blast_tac 1); 
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

201 
qed "constrains_cancel"; 
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset

202 

4776  203 

204 
(*** stable ***) 

205 

6536  206 
Goalw [stable_def] "F : A co A ==> F : stable A"; 
4776  207 
by (assume_tac 1); 
208 
qed "stableI"; 

209 

6536  210 
Goalw [stable_def] "F : stable A ==> F : A co A"; 
4776  211 
by (assume_tac 1); 
212 
qed "stableD"; 

213 

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

214 
(** Union **) 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset

215 

5069  216 
Goalw [stable_def] 
5648  217 
"[ F : stable A; F : stable A' ] ==> F : stable (A Un A')"; 
4776  218 
by (blast_tac (claset() addIs [constrains_Un]) 1); 
219 
qed "stable_Un"; 

220 

5069  221 
Goalw [stable_def] 
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset

222 
"ALL i:I. F : stable (A i) ==> F : stable (UN i:I. A i)"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset

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

224 
qed "ball_stable_UN"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset

225 

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

226 
(** Intersection **) 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset

227 

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

228 
Goalw [stable_def] 
5648  229 
"[ F : stable A; F : stable A' ] ==> F : stable (A Int A')"; 
4776  230 
by (blast_tac (claset() addIs [constrains_Int]) 1); 
231 
qed "stable_Int"; 

232 

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

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

234 
"ALL i:I. F : stable (A i) ==> F : stable (INT i:I. A i)"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset

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

236 
qed "ball_stable_INT"; 
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset

237 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset

238 
Goalw [stable_def, constrains_def] 
6536  239 
"[ F : stable C; F : A co (C Un A') ] \ 
240 
\ ==> F : (C Un A) co (C Un A')"; 

4776  241 
by (Blast_tac 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset

242 
qed "stable_constrains_Un"; 
4776  243 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset

244 
Goalw [stable_def, constrains_def] 
6536  245 
"[ F : stable C; F : (C Int A) co A' ] \ 
246 
\ ==> F : (C Int A) co (C Int A')"; 

4776  247 
by (Blast_tac 1); 
5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset

248 
qed "stable_constrains_Int"; 
4776  249 

6536  250 
(*[ F : stable C; F : co (C Int A) A ] ==> F : stable (C Int A)*) 
5648  251 
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI); 
252 

253 

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

254 
(*** invariant ***) 
5648  255 

256 
Goal "[ Init F<=A; F: stable A ] ==> F : invariant A"; 

257 
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); 

258 
qed "invariantI"; 

259 

260 
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*) 

261 
Goal "[ F : invariant A; F : invariant B ] ==> F : invariant (A Int B)"; 

262 
by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int])); 

263 
qed "invariant_Int"; 

264 

265 

266 
(*** increasing ***) 

267 

268 
Goalw [increasing_def, stable_def, constrains_def] 

6712  269 
"mono g ==> increasing f <= increasing (g o f)"; 
5648  270 
by Auto_tac; 
6712  271 
by (blast_tac (claset() addIs [monoD, order_trans]) 1); 
272 
qed "mono_increasing_o"; 

5648  273 

274 
Goalw [increasing_def] 

275 
"increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}"; 

276 
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); 

277 
by (Blast_tac 1); 

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

278 
qed "increasing_stable_less"; 
5648  279 

280 

281 
(** The Elimination Theorem. The "free" m has become universally quantified! 

282 
Should the premise be !!m instead of ALL m ? Would make it harder to use 

283 
in forward proof. **) 

284 

5069  285 
Goalw [constrains_def] 
6536  286 
"[ ALL m:M. F : {s. s x = m} co (B m) ] \ 
287 
\ ==> F : {s. s x : M} co (UN m:M. B m)"; 

4776  288 
by (Blast_tac 1); 
289 
qed "elimination"; 

290 

291 
(*As above, but for the trivial case of a onevariable state, in which the 

292 
state is identified with its one variable.*) 

5069  293 
Goalw [constrains_def] 
6536  294 
"(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)"; 
4776  295 
by (Blast_tac 1); 
296 
qed "elimination_sing"; 

297 

298 

299 

300 
(*** Theoretical Results from Section 6 ***) 

301 

5069  302 
Goalw [constrains_def, strongest_rhs_def] 
6536  303 
"F : A co (strongest_rhs F A )"; 
4776  304 
by (Blast_tac 1); 
305 
qed "constrains_strongest_rhs"; 

306 

5069  307 
Goalw [constrains_def, strongest_rhs_def] 
6536  308 
"F : A co B ==> strongest_rhs F A <= B"; 
4776  309 
by (Blast_tac 1); 
310 
qed "strongest_rhs_is_strongest"; 