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