author | paulson |
Wed, 01 Sep 1999 11:16:02 +0200 | |
changeset 7403 | c318acb88251 |
parent 7345 | 59bc887290df |
child 7594 | 8a188ef6545e |
permissions | -rw-r--r-- |
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 |
||
13 |
||
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
14 |
(*** General lemmas ***) |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
15 |
|
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
16 |
Goal "UNIV Times UNIV = UNIV"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
17 |
by Auto_tac; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
18 |
qed "UNIV_Times_UNIV"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
19 |
Addsimps [UNIV_Times_UNIV]; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
20 |
|
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
21 |
Goal "- (UNIV Times A) = UNIV Times (-A)"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
22 |
by Auto_tac; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
23 |
qed "Compl_Times_UNIV1"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
24 |
|
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
25 |
Goal "- (A Times UNIV) = (-A) Times UNIV"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
26 |
by Auto_tac; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
27 |
qed "Compl_Times_UNIV2"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
28 |
|
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
29 |
Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
30 |
|
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
31 |
|
6535 | 32 |
(*** The abstract type of programs ***) |
33 |
||
34 |
val rep_ss = simpset() addsimps |
|
35 |
[Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, |
|
36 |
Rep_Program_inverse, Abs_Program_inverse]; |
|
37 |
||
38 |
||
39 |
Goal "Id : Acts F"; |
|
40 |
by (cut_inst_tac [("x", "F")] Rep_Program 1); |
|
41 |
by (auto_tac (claset(), rep_ss)); |
|
42 |
qed "Id_in_Acts"; |
|
43 |
AddIffs [Id_in_Acts]; |
|
44 |
||
45 |
Goal "insert Id (Acts F) = Acts F"; |
|
46 |
by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1); |
|
47 |
qed "insert_Id_Acts"; |
|
48 |
AddIffs [insert_Id_Acts]; |
|
49 |
||
50 |
(** Inspectors for type "program" **) |
|
51 |
||
52 |
Goal "Init (mk_program (init,acts)) = init"; |
|
53 |
by (auto_tac (claset(), rep_ss)); |
|
54 |
qed "Init_eq"; |
|
55 |
||
56 |
Goal "Acts (mk_program (init,acts)) = insert Id acts"; |
|
57 |
by (auto_tac (claset(), rep_ss)); |
|
58 |
qed "Acts_eq"; |
|
59 |
||
60 |
Addsimps [Acts_eq, Init_eq]; |
|
61 |
||
62 |
||
63 |
(** The notation of equality for type "program" **) |
|
64 |
||
65 |
Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G"; |
|
66 |
by (subgoals_tac ["EX x. Rep_Program F = x", |
|
67 |
"EX x. Rep_Program G = x"] 1); |
|
68 |
by (REPEAT (Blast_tac 2)); |
|
69 |
by (Clarify_tac 1); |
|
70 |
by (auto_tac (claset(), rep_ss)); |
|
71 |
by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1)); |
|
72 |
by (asm_full_simp_tac rep_ss 1); |
|
73 |
qed "program_equalityI"; |
|
74 |
||
75 |
val [major,minor] = |
|
76 |
Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P"; |
|
77 |
by (rtac minor 1); |
|
78 |
by (auto_tac (claset(), simpset() addsimps [major])); |
|
79 |
qed "program_equalityE"; |
|
80 |
||
81 |
||
82 |
(*** These rules allow "lazy" definition expansion |
|
83 |
They avoid expanding the full program, which is a large expression |
|
84 |
***) |
|
85 |
||
86 |
Goal "F == mk_program (init,acts) ==> Init F = init"; |
|
87 |
by Auto_tac; |
|
88 |
qed "def_prg_Init"; |
|
89 |
||
90 |
(*The program is not expanded, but its Init and Acts are*) |
|
91 |
val [rew] = goal thy |
|
92 |
"[| F == mk_program (init,acts) |] \ |
|
93 |
\ ==> Init F = init & Acts F = insert Id acts"; |
|
94 |
by (rewtac rew); |
|
95 |
by Auto_tac; |
|
96 |
qed "def_prg_simps"; |
|
97 |
||
98 |
(*An action is expanded only if a pair of states is being tested against it*) |
|
99 |
Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"; |
|
100 |
by Auto_tac; |
|
101 |
qed "def_act_simp"; |
|
102 |
||
103 |
fun simp_of_act def = def RS def_act_simp; |
|
104 |
||
105 |
(*A set is expanded only if an element is being tested against it*) |
|
106 |
Goal "A == B ==> (x : A) = (x : B)"; |
|
107 |
by Auto_tac; |
|
108 |
qed "def_set_simp"; |
|
109 |
||
110 |
fun simp_of_set def = def RS def_set_simp; |
|
111 |
||
112 |
||
6536 | 113 |
(*** co ***) |
4776 | 114 |
|
7403 | 115 |
(*These operators are not overloaded, but their operands are sets, and |
116 |
ultimately there's a risk of reaching equality, which IS overloaded*) |
|
117 |
overload_1st_set "UNITY.constrains"; |
|
5648 | 118 |
overload_1st_set "UNITY.stable"; |
119 |
overload_1st_set "UNITY.unless"; |
|
5340 | 120 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
121 |
val prems = Goalw [constrains_def] |
5648 | 122 |
"(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \ |
6536 | 123 |
\ ==> F : A co A'"; |
4776 | 124 |
by (blast_tac (claset() addIs prems) 1); |
125 |
qed "constrainsI"; |
|
126 |
||
5069 | 127 |
Goalw [constrains_def] |
6536 | 128 |
"[| F : A co A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'"; |
4776 | 129 |
by (Blast_tac 1); |
130 |
qed "constrainsD"; |
|
131 |
||
6536 | 132 |
Goalw [constrains_def] "F : {} co B"; |
4776 | 133 |
by (Blast_tac 1); |
134 |
qed "constrains_empty"; |
|
135 |
||
6536 | 136 |
Goalw [constrains_def] "F : A co UNIV"; |
4776 | 137 |
by (Blast_tac 1); |
138 |
qed "constrains_UNIV"; |
|
139 |
AddIffs [constrains_empty, constrains_UNIV]; |
|
140 |
||
5648 | 141 |
(*monotonic in 2nd argument*) |
5069 | 142 |
Goalw [constrains_def] |
6536 | 143 |
"[| F : A co A'; A'<=B' |] ==> F : A co B'"; |
4776 | 144 |
by (Blast_tac 1); |
145 |
qed "constrains_weaken_R"; |
|
146 |
||
5648 | 147 |
(*anti-monotonic in 1st argument*) |
5069 | 148 |
Goalw [constrains_def] |
6536 | 149 |
"[| F : A co A'; B<=A |] ==> F : B co A'"; |
4776 | 150 |
by (Blast_tac 1); |
151 |
qed "constrains_weaken_L"; |
|
152 |
||
5069 | 153 |
Goalw [constrains_def] |
6536 | 154 |
"[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'"; |
4776 | 155 |
by (Blast_tac 1); |
156 |
qed "constrains_weaken"; |
|
157 |
||
158 |
(** Union **) |
|
159 |
||
5069 | 160 |
Goalw [constrains_def] |
7345 | 161 |
"[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')"; |
4776 | 162 |
by (Blast_tac 1); |
163 |
qed "constrains_Un"; |
|
164 |
||
5069 | 165 |
Goalw [constrains_def] |
7345 | 166 |
"ALL i:I. F : (A i) co (A' i) ==> F : (UN i:I. A i) co (UN i:I. A' i)"; |
4776 | 167 |
by (Blast_tac 1); |
168 |
qed "ball_constrains_UN"; |
|
169 |
||
170 |
(** Intersection **) |
|
171 |
||
5069 | 172 |
Goalw [constrains_def] |
7345 | 173 |
"[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"; |
4776 | 174 |
by (Blast_tac 1); |
175 |
qed "constrains_Int"; |
|
176 |
||
5069 | 177 |
Goalw [constrains_def] |
7345 | 178 |
"ALL i:I. F : (A i) co (A' i) ==> F : (INT i:I. A i) co (INT i:I. A' i)"; |
4776 | 179 |
by (Blast_tac 1); |
180 |
qed "ball_constrains_INT"; |
|
181 |
||
6536 | 182 |
Goalw [constrains_def] "F : A co A' ==> A <= A'"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
183 |
by Auto_tac; |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
184 |
qed "constrains_imp_subset"; |
4776 | 185 |
|
6536 | 186 |
(*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
|
187 |
only. So this rule isn't that useful.*) |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
188 |
Goalw [constrains_def] |
6536 | 189 |
"[| 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
|
190 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
191 |
qed "constrains_trans"; |
4776 | 192 |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
193 |
Goalw [constrains_def] |
7345 | 194 |
"[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
195 |
by (Clarify_tac 1); |
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
196 |
by (Blast_tac 1); |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
197 |
qed "constrains_cancel"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
198 |
|
4776 | 199 |
|
200 |
(*** stable ***) |
|
201 |
||
6536 | 202 |
Goalw [stable_def] "F : A co A ==> F : stable A"; |
4776 | 203 |
by (assume_tac 1); |
204 |
qed "stableI"; |
|
205 |
||
6536 | 206 |
Goalw [stable_def] "F : stable A ==> F : A co A"; |
4776 | 207 |
by (assume_tac 1); |
208 |
qed "stableD"; |
|
209 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
210 |
(** Union **) |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
211 |
|
5069 | 212 |
Goalw [stable_def] |
5648 | 213 |
"[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"; |
4776 | 214 |
by (blast_tac (claset() addIs [constrains_Un]) 1); |
215 |
qed "stable_Un"; |
|
216 |
||
5069 | 217 |
Goalw [stable_def] |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
218 |
"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
|
219 |
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
|
220 |
qed "ball_stable_UN"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
221 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
222 |
(** Intersection **) |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
223 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
224 |
Goalw [stable_def] |
5648 | 225 |
"[| F : stable A; F : stable A' |] ==> F : stable (A Int A')"; |
4776 | 226 |
by (blast_tac (claset() addIs [constrains_Int]) 1); |
227 |
qed "stable_Int"; |
|
228 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
229 |
Goalw [stable_def] |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
230 |
"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
|
231 |
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
|
232 |
qed "ball_stable_INT"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
233 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
234 |
Goalw [stable_def, constrains_def] |
7345 | 235 |
"[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"; |
4776 | 236 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
237 |
qed "stable_constrains_Un"; |
4776 | 238 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
239 |
Goalw [stable_def, constrains_def] |
7345 | 240 |
"[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"; |
4776 | 241 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
242 |
qed "stable_constrains_Int"; |
4776 | 243 |
|
6536 | 244 |
(*[| F : stable C; F : co (C Int A) A |] ==> F : stable (C Int A)*) |
5648 | 245 |
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI); |
246 |
||
247 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
248 |
(*** invariant ***) |
5648 | 249 |
|
250 |
Goal "[| Init F<=A; F: stable A |] ==> F : invariant A"; |
|
251 |
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); |
|
252 |
qed "invariantI"; |
|
253 |
||
254 |
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*) |
|
255 |
Goal "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)"; |
|
256 |
by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int])); |
|
257 |
qed "invariant_Int"; |
|
258 |
||
259 |
||
260 |
(*** increasing ***) |
|
261 |
||
262 |
Goalw [increasing_def, stable_def, constrains_def] |
|
6712 | 263 |
"mono g ==> increasing f <= increasing (g o f)"; |
5648 | 264 |
by Auto_tac; |
6712 | 265 |
by (blast_tac (claset() addIs [monoD, order_trans]) 1); |
266 |
qed "mono_increasing_o"; |
|
5648 | 267 |
|
268 |
Goalw [increasing_def] |
|
269 |
"increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}"; |
|
270 |
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); |
|
271 |
by (Blast_tac 1); |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
272 |
qed "increasing_stable_less"; |
5648 | 273 |
|
274 |
||
275 |
(** The Elimination Theorem. The "free" m has become universally quantified! |
|
276 |
Should the premise be !!m instead of ALL m ? Would make it harder to use |
|
277 |
in forward proof. **) |
|
278 |
||
5069 | 279 |
Goalw [constrains_def] |
6536 | 280 |
"[| ALL m:M. F : {s. s x = m} co (B m) |] \ |
281 |
\ ==> F : {s. s x : M} co (UN m:M. B m)"; |
|
4776 | 282 |
by (Blast_tac 1); |
283 |
qed "elimination"; |
|
284 |
||
285 |
(*As above, but for the trivial case of a one-variable state, in which the |
|
286 |
state is identified with its one variable.*) |
|
5069 | 287 |
Goalw [constrains_def] |
6536 | 288 |
"(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)"; |
4776 | 289 |
by (Blast_tac 1); |
290 |
qed "elimination_sing"; |
|
291 |
||
292 |
||
293 |
||
294 |
(*** Theoretical Results from Section 6 ***) |
|
295 |
||
5069 | 296 |
Goalw [constrains_def, strongest_rhs_def] |
6536 | 297 |
"F : A co (strongest_rhs F A )"; |
4776 | 298 |
by (Blast_tac 1); |
299 |
qed "constrains_strongest_rhs"; |
|
300 |
||
5069 | 301 |
Goalw [constrains_def, strongest_rhs_def] |
6536 | 302 |
"F : A co B ==> strongest_rhs F A <= B"; |
4776 | 303 |
by (Blast_tac 1); |
304 |
qed "strongest_rhs_is_strongest"; |