author | paulson |
Thu, 03 Dec 1998 10:45:06 +0100 | |
changeset 6012 | 1894bfc4aee9 |
parent 5804 | 8e0a4c4fd67b |
child 6295 | 351b3c2b0d83 |
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 |
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 "Pow UNIV = UNIV"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
18 |
by (Blast_tac 1); |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
19 |
qed "Pow_UNIV"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
20 |
Addsimps [Pow_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 UNIV = UNIV"; |
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 "UNIV_Times_UNIV"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
25 |
Addsimps [UNIV_Times_UNIV]; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
26 |
|
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
27 |
Goal "- (UNIV Times A) = UNIV Times (-A)"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
28 |
by Auto_tac; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
29 |
qed "Compl_Times_UNIV1"; |
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 |
Goal "- (A Times UNIV) = (-A) Times UNIV"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
32 |
by Auto_tac; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
33 |
qed "Compl_Times_UNIV2"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
34 |
|
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
35 |
Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
36 |
|
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
37 |
|
4776 | 38 |
(*** constrains ***) |
39 |
||
5648 | 40 |
overload_1st_set "UNITY.constrains"; |
41 |
overload_1st_set "UNITY.stable"; |
|
42 |
overload_1st_set "UNITY.unless"; |
|
5340 | 43 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
44 |
val prems = Goalw [constrains_def] |
5648 | 45 |
"(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \ |
46 |
\ ==> F : constrains A A'"; |
|
4776 | 47 |
by (blast_tac (claset() addIs prems) 1); |
48 |
qed "constrainsI"; |
|
49 |
||
5069 | 50 |
Goalw [constrains_def] |
5648 | 51 |
"[| F : constrains A A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'"; |
4776 | 52 |
by (Blast_tac 1); |
53 |
qed "constrainsD"; |
|
54 |
||
5648 | 55 |
Goalw [constrains_def] "F : constrains {} B"; |
4776 | 56 |
by (Blast_tac 1); |
57 |
qed "constrains_empty"; |
|
58 |
||
5648 | 59 |
Goalw [constrains_def] "F : constrains A UNIV"; |
4776 | 60 |
by (Blast_tac 1); |
61 |
qed "constrains_UNIV"; |
|
62 |
AddIffs [constrains_empty, constrains_UNIV]; |
|
63 |
||
5648 | 64 |
(*monotonic in 2nd argument*) |
5069 | 65 |
Goalw [constrains_def] |
5648 | 66 |
"[| F : constrains A A'; A'<=B' |] ==> F : constrains A B'"; |
4776 | 67 |
by (Blast_tac 1); |
68 |
qed "constrains_weaken_R"; |
|
69 |
||
5648 | 70 |
(*anti-monotonic in 1st argument*) |
5069 | 71 |
Goalw [constrains_def] |
5648 | 72 |
"[| F : constrains A A'; B<=A |] ==> F : constrains B A'"; |
4776 | 73 |
by (Blast_tac 1); |
74 |
qed "constrains_weaken_L"; |
|
75 |
||
5069 | 76 |
Goalw [constrains_def] |
5648 | 77 |
"[| F : constrains A A'; B<=A; A'<=B' |] ==> F : constrains B B'"; |
4776 | 78 |
by (Blast_tac 1); |
79 |
qed "constrains_weaken"; |
|
80 |
||
81 |
(** Union **) |
|
82 |
||
5069 | 83 |
Goalw [constrains_def] |
5648 | 84 |
"[| F : constrains A A'; F : constrains B B' |] \ |
85 |
\ ==> F : constrains (A Un B) (A' Un B')"; |
|
4776 | 86 |
by (Blast_tac 1); |
87 |
qed "constrains_Un"; |
|
88 |
||
5069 | 89 |
Goalw [constrains_def] |
5648 | 90 |
"ALL i:I. F : constrains (A i) (A' i) \ |
91 |
\ ==> F : constrains (UN i:I. A i) (UN i:I. A' i)"; |
|
4776 | 92 |
by (Blast_tac 1); |
93 |
qed "ball_constrains_UN"; |
|
94 |
||
95 |
(** Intersection **) |
|
96 |
||
5069 | 97 |
Goalw [constrains_def] |
5648 | 98 |
"[| F : constrains A A'; F : constrains B B' |] \ |
99 |
\ ==> F : constrains (A Int B) (A' Int B')"; |
|
4776 | 100 |
by (Blast_tac 1); |
101 |
qed "constrains_Int"; |
|
102 |
||
5069 | 103 |
Goalw [constrains_def] |
5648 | 104 |
"ALL i:I. F : constrains (A i) (A' i) \ |
105 |
\ ==> F : constrains (INT i:I. A i) (INT i:I. A' i)"; |
|
4776 | 106 |
by (Blast_tac 1); |
107 |
qed "ball_constrains_INT"; |
|
108 |
||
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
109 |
Goalw [constrains_def] "[| F : constrains A A'; A <= States F |] ==> A <= A'"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
110 |
by (Force_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
111 |
qed "constrains_imp_subset"; |
4776 | 112 |
|
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
113 |
(*The reasoning is by subsets since "constrains" refers to single actions |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
114 |
only. So this rule isn't that useful.*) |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
115 |
Goal "[| F : constrains A B; F : constrains B C; B <= States F |] \ |
5648 | 116 |
\ ==> F : constrains A C"; |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
117 |
by (etac constrains_weaken_R 1); |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
118 |
by (etac constrains_imp_subset 1); |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
119 |
by (assume_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
120 |
qed "constrains_trans"; |
4776 | 121 |
|
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
122 |
Goal "[| F : constrains A (A' Un B); F : constrains B B'; B <= States F|] \ |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
123 |
\ ==> F : constrains A (A' Un B')"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
124 |
by (etac constrains_weaken_R 1); |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
125 |
by (blast_tac (claset() addDs [impOfSubs constrains_imp_subset]) 1); |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
126 |
qed "constrains_cancel"; |
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5804
diff
changeset
|
127 |
|
4776 | 128 |
|
129 |
(*** stable ***) |
|
130 |
||
5648 | 131 |
Goalw [stable_def] "F : constrains A A ==> F : stable A"; |
4776 | 132 |
by (assume_tac 1); |
133 |
qed "stableI"; |
|
134 |
||
5648 | 135 |
Goalw [stable_def] "F : stable A ==> F : constrains A A"; |
4776 | 136 |
by (assume_tac 1); |
137 |
qed "stableD"; |
|
138 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
139 |
(** Union **) |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
140 |
|
5069 | 141 |
Goalw [stable_def] |
5648 | 142 |
"[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"; |
4776 | 143 |
by (blast_tac (claset() addIs [constrains_Un]) 1); |
144 |
qed "stable_Un"; |
|
145 |
||
5069 | 146 |
Goalw [stable_def] |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
147 |
"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
|
148 |
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
|
149 |
qed "ball_stable_UN"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
150 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
151 |
(** Intersection **) |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
152 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
153 |
Goalw [stable_def] |
5648 | 154 |
"[| F : stable A; F : stable A' |] ==> F : stable (A Int A')"; |
4776 | 155 |
by (blast_tac (claset() addIs [constrains_Int]) 1); |
156 |
qed "stable_Int"; |
|
157 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
158 |
Goalw [stable_def] |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
159 |
"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
|
160 |
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
|
161 |
qed "ball_stable_INT"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
162 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
163 |
Goalw [stable_def, constrains_def] |
5648 | 164 |
"[| F : stable C; F : constrains A (C Un A') |] \ |
165 |
\ ==> F : constrains (C Un A) (C Un A')"; |
|
4776 | 166 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
167 |
qed "stable_constrains_Un"; |
4776 | 168 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
169 |
Goalw [stable_def, constrains_def] |
5648 | 170 |
"[| F : stable C; F : constrains (C Int A) A' |] \ |
171 |
\ ==> F : constrains (C Int A) (C Int A')"; |
|
4776 | 172 |
by (Blast_tac 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset
|
173 |
qed "stable_constrains_Int"; |
4776 | 174 |
|
5648 | 175 |
Goal "Init F <= reachable F"; |
176 |
by (blast_tac (claset() addIs reachable.intrs) 1); |
|
177 |
qed "Init_subset_reachable"; |
|
4776 | 178 |
|
5648 | 179 |
Goal "Acts G <= Acts F ==> G : stable (reachable F)"; |
180 |
by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1); |
|
181 |
qed "stable_reachable"; |
|
182 |
||
183 |
(*[| F : stable C; F : constrains (C Int A) A |] ==> F : stable (C Int A)*) |
|
184 |
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI); |
|
185 |
||
186 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
187 |
(*** invariant ***) |
5648 | 188 |
|
189 |
Goal "[| Init F<=A; F: stable A |] ==> F : invariant A"; |
|
190 |
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1); |
|
191 |
qed "invariantI"; |
|
192 |
||
193 |
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*) |
|
194 |
Goal "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)"; |
|
195 |
by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int])); |
|
196 |
qed "invariant_Int"; |
|
197 |
||
198 |
(*The set of all reachable states is an invariant...*) |
|
199 |
Goal "F : invariant (reachable F)"; |
|
200 |
by (simp_tac (simpset() addsimps [invariant_def]) 1); |
|
201 |
by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1); |
|
202 |
qed "invariant_reachable"; |
|
203 |
||
204 |
(*...in fact the strongest invariant!*) |
|
205 |
Goal "F : invariant A ==> reachable F <= A"; |
|
206 |
by (full_simp_tac |
|
207 |
(simpset() addsimps [stable_def, constrains_def, invariant_def]) 1); |
|
208 |
by (rtac subsetI 1); |
|
209 |
by (etac reachable.induct 1); |
|
210 |
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
|
211 |
qed "invariant_includes_reachable"; |
|
212 |
||
213 |
||
214 |
(*** increasing ***) |
|
215 |
||
216 |
Goalw [increasing_def, stable_def, constrains_def] |
|
217 |
"increasing f <= increasing (length o f)"; |
|
218 |
by Auto_tac; |
|
219 |
by (blast_tac (claset() addIs [prefix_length_le, le_trans]) 1); |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
220 |
qed "increasing_size"; |
5648 | 221 |
|
222 |
Goalw [increasing_def] |
|
223 |
"increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}"; |
|
224 |
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); |
|
225 |
by (Blast_tac 1); |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5669
diff
changeset
|
226 |
qed "increasing_stable_less"; |
5648 | 227 |
|
228 |
||
229 |
(** The Elimination Theorem. The "free" m has become universally quantified! |
|
230 |
Should the premise be !!m instead of ALL m ? Would make it harder to use |
|
231 |
in forward proof. **) |
|
232 |
||
5069 | 233 |
Goalw [constrains_def] |
5648 | 234 |
"[| ALL m. F : constrains {s. s x = m} (B m) |] \ |
235 |
\ ==> F : constrains {s. s x : M} (UN m:M. B m)"; |
|
4776 | 236 |
by (Blast_tac 1); |
237 |
qed "elimination"; |
|
238 |
||
239 |
(*As above, but for the trivial case of a one-variable state, in which the |
|
240 |
state is identified with its one variable.*) |
|
5069 | 241 |
Goalw [constrains_def] |
5648 | 242 |
"(ALL m. F : constrains {m} (B m)) ==> F : constrains M (UN m:M. B m)"; |
4776 | 243 |
by (Blast_tac 1); |
244 |
qed "elimination_sing"; |
|
245 |
||
246 |
||
247 |
||
248 |
(*** Theoretical Results from Section 6 ***) |
|
249 |
||
5069 | 250 |
Goalw [constrains_def, strongest_rhs_def] |
5648 | 251 |
"F : constrains A (strongest_rhs F A )"; |
4776 | 252 |
by (Blast_tac 1); |
253 |
qed "constrains_strongest_rhs"; |
|
254 |
||
5069 | 255 |
Goalw [constrains_def, strongest_rhs_def] |
5648 | 256 |
"F : constrains A B ==> strongest_rhs F A <= B"; |
4776 | 257 |
by (Blast_tac 1); |
258 |
qed "strongest_rhs_is_strongest"; |