author | paulson |
Thu, 26 Aug 1999 11:36:04 +0200 | |
changeset 7361 | 477e1bdf230f |
parent 7344 | d54e871d77e0 |
child 7399 | cf780c2bcccf |
permissions | -rw-r--r-- |
5899 | 1 |
(* Title: HOL/UNITY/PPROD.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
5 |
|
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
6 |
Abstraction over replicated components (PLam) |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
7 |
General products of programs (Pi operation) |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
8 |
|
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
9 |
It is not clear that any of this is good for anything. |
5899 | 10 |
*) |
11 |
||
6020 | 12 |
|
13 |
val rinst = read_instantiate_sg (sign_of thy); |
|
14 |
||
5899 | 15 |
|
16 |
(*** Basic properties ***) |
|
17 |
||
6842 | 18 |
Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))"; |
5972 | 19 |
by Auto_tac; |
6842 | 20 |
qed "Init_PLam"; |
21 |
Addsimps [Init_PLam]; |
|
5972 | 22 |
|
6842 | 23 |
Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))"; |
5899 | 24 |
by (auto_tac (claset(), |
6842 | 25 |
simpset() addsimps [PLam_def, Acts_JN])); |
26 |
qed "Acts_PLam"; |
|
5899 | 27 |
|
6842 | 28 |
Goal "PLam {} F = SKIP"; |
29 |
by (simp_tac (simpset() addsimps [PLam_def]) 1); |
|
30 |
qed "PLam_empty"; |
|
5899 | 31 |
|
6842 | 32 |
Goal "(plam i: I. SKIP) = SKIP"; |
33 |
by (simp_tac (simpset() addsimps [PLam_def,lift_prog_SKIP,JN_constant]) 1); |
|
34 |
qed "PLam_SKIP"; |
|
6299 | 35 |
|
6842 | 36 |
Addsimps [PLam_SKIP, PLam_empty]; |
5899 | 37 |
|
6842 | 38 |
Goalw [PLam_def] |
39 |
"PLam (insert i I) F = (lift_prog i (F i)) Join (PLam I F)"; |
|
5899 | 40 |
by Auto_tac; |
6842 | 41 |
qed "PLam_insert"; |
5899 | 42 |
|
6842 | 43 |
Goalw [PLam_def] "i : I ==> (lift_prog i (F i)) component (PLam I F)"; |
5972 | 44 |
(*blast_tac doesn't use HO unification*) |
45 |
by (fast_tac (claset() addIs [component_JN]) 1); |
|
6842 | 46 |
qed "component_PLam"; |
5899 | 47 |
|
5972 | 48 |
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
49 |
(** Safety **) |
6835
588f791ee737
addition of drop_... operators with new results and simplification of old ones
paulson
parents:
6826
diff
changeset
|
50 |
|
5899 | 51 |
Goal "i : I ==> \ |
6842 | 52 |
\ (PLam I F : (lift_set i A) co (lift_set i B)) = \ |
6536 | 53 |
\ (F i : A co B)"; |
6842 | 54 |
by (asm_simp_tac (simpset() addsimps [PLam_def, constrains_JN]) 1); |
7344
d54e871d77e0
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
7188
diff
changeset
|
55 |
by (blast_tac (claset() addIs [lift_prog_constrains RS iffD1, |
5972 | 56 |
constrains_imp_lift_prog_constrains]) 1); |
6842 | 57 |
qed "PLam_constrains"; |
5899 | 58 |
|
6842 | 59 |
Goal "i : I ==> (PLam I F : stable (lift_set i A)) = (F i : stable A)"; |
60 |
by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1); |
|
61 |
qed "PLam_stable"; |
|
5972 | 62 |
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
63 |
(*Possibly useful in Lift_set.ML?*) |
6536 | 64 |
Goal "[| lift_prog i F : AA co BB |] \ |
6835
588f791ee737
addition of drop_... operators with new results and simplification of old ones
paulson
parents:
6826
diff
changeset
|
65 |
\ ==> F : (drop_set i AA) co (drop_set i BB)"; |
5899 | 66 |
by (auto_tac (claset(), |
6835
588f791ee737
addition of drop_... operators with new results and simplification of old ones
paulson
parents:
6826
diff
changeset
|
67 |
simpset() addsimps [constrains_def, drop_set_def])); |
5972 | 68 |
by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
5899 | 69 |
simpset()) 1); |
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
70 |
qed "lift_prog_constrains_drop_set"; |
5972 | 71 |
|
6842 | 72 |
Goal "[| PLam I F : AA co BB; i: I |] \ |
6835
588f791ee737
addition of drop_... operators with new results and simplification of old ones
paulson
parents:
6826
diff
changeset
|
73 |
\ ==> F i : (drop_set i AA) co (drop_set i BB)"; |
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
74 |
by (rtac lift_prog_constrains_drop_set 1); |
5972 | 75 |
(*rotate this assumption to be last*) |
6842 | 76 |
by (dres_inst_tac [("psi", "PLam I F : ?C")] asm_rl 1); |
77 |
by (asm_full_simp_tac (simpset() addsimps [PLam_def, constrains_JN]) 1); |
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
78 |
qed "PLam_constrains_drop_set"; |
5899 | 79 |
|
80 |
||
5972 | 81 |
(** invariant **) |
82 |
||
6299 | 83 |
Goal "[| F i : invariant A; i : I |] \ |
6842 | 84 |
\ ==> PLam I F : invariant (lift_set i A)"; |
5972 | 85 |
by (auto_tac (claset(), |
6842 | 86 |
simpset() addsimps [invariant_def, PLam_stable])); |
87 |
qed "invariant_imp_PLam_invariant"; |
|
5972 | 88 |
|
89 |
(*The f0 premise ensures that the product is well-defined.*) |
|
6842 | 90 |
Goal "[| PLam I F : invariant (lift_set i A); i : I; \ |
91 |
\ f0: Init (PLam I F) |] ==> F i : invariant A"; |
|
5899 | 92 |
by (auto_tac (claset(), |
6842 | 93 |
simpset() addsimps [invariant_def, PLam_stable])); |
5972 | 94 |
by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1); |
95 |
by Auto_tac; |
|
6842 | 96 |
qed "PLam_invariant_imp_invariant"; |
5972 | 97 |
|
6842 | 98 |
Goal "[| i : I; f0: Init (PLam I F) |] \ |
99 |
\ ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"; |
|
100 |
by (blast_tac (claset() addIs [invariant_imp_PLam_invariant, |
|
101 |
PLam_invariant_imp_invariant]) 1); |
|
102 |
qed "PLam_invariant"; |
|
5899 | 103 |
|
5972 | 104 |
(*The f0 premise isn't needed if F is a constant program because then |
105 |
we get an initial state by replicating that of F*) |
|
106 |
Goal "i : I \ |
|
6842 | 107 |
\ ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"; |
5972 | 108 |
by (auto_tac (claset(), |
6842 | 109 |
simpset() addsimps [invariant_def, PLam_stable])); |
110 |
qed "const_PLam_invariant"; |
|
5972 | 111 |
|
5899 | 112 |
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
113 |
(** Reachability **) |
5972 | 114 |
|
6842 | 115 |
Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)"; |
5899 | 116 |
by (etac reachable.induct 1); |
117 |
by (auto_tac |
|
118 |
(claset() addIs reachable.intrs, |
|
6842 | 119 |
simpset() addsimps [Acts_PLam])); |
120 |
qed "reachable_PLam"; |
|
5899 | 121 |
|
6842 | 122 |
(*Result to justify a re-organization of this file*) |
123 |
Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"; |
|
6867 | 124 |
by Auto_tac; |
6842 | 125 |
result(); |
126 |
||
127 |
Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"; |
|
128 |
by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1); |
|
129 |
qed "reachable_PLam_subset1"; |
|
5899 | 130 |
|
6826 | 131 |
(*simplify using reachable_lift_prog??*) |
5972 | 132 |
Goal "[| i ~: I; A : reachable (F i) |] \ |
6842 | 133 |
\ ==> ALL f. f : reachable (PLam I F) \ |
134 |
\ --> f(i:=A) : reachable (lift_prog i (F i) Join PLam I F)"; |
|
5899 | 135 |
by (etac reachable.induct 1); |
136 |
by (ALLGOALS Clarify_tac); |
|
137 |
by (etac reachable.induct 1); |
|
138 |
(*Init, Init case*) |
|
6826 | 139 |
by (force_tac (claset() addIs reachable.intrs, simpset()) 1); |
6842 | 140 |
(*Init of F, action of PLam F case*) |
5972 | 141 |
by (rtac reachable.Acts 1); |
5899 | 142 |
by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
5972 | 143 |
by (assume_tac 1); |
6842 | 144 |
by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1); |
5899 | 145 |
(*induction over the 2nd "reachable" assumption*) |
146 |
by (eres_inst_tac [("xa","f")] reachable.induct 1); |
|
6842 | 147 |
(*Init of PLam F, action of F case*) |
5899 | 148 |
by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
6835
588f791ee737
addition of drop_... operators with new results and simplification of old ones
paulson
parents:
6826
diff
changeset
|
149 |
by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
5899 | 150 |
by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
151 |
by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
|
6842 | 152 |
(*last case: an action of PLam I F*) |
5972 | 153 |
by (rtac reachable.Acts 1); |
5899 | 154 |
by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
5972 | 155 |
by (assume_tac 1); |
6842 | 156 |
by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1); |
157 |
qed_spec_mp "reachable_lift_Join_PLam"; |
|
5899 | 158 |
|
159 |
||
160 |
(*The index set must be finite: otherwise infinitely many copies of F can |
|
6842 | 161 |
perform actions, and PLam can never catch up in finite time.*) |
5972 | 162 |
Goal "finite I \ |
6842 | 163 |
\ ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"; |
5899 | 164 |
by (etac finite_induct 1); |
165 |
by (Simp_tac 1); |
|
6842 | 166 |
by (force_tac (claset() addDs [reachable_lift_Join_PLam], |
167 |
simpset() addsimps [PLam_insert]) 1); |
|
168 |
qed "reachable_PLam_subset2"; |
|
5899 | 169 |
|
5972 | 170 |
Goal "finite I ==> \ |
6842 | 171 |
\ reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"; |
5899 | 172 |
by (REPEAT_FIRST (ares_tac [equalityI, |
6842 | 173 |
reachable_PLam_subset1, |
174 |
reachable_PLam_subset2])); |
|
175 |
qed "reachable_PLam_eq"; |
|
5899 | 176 |
|
177 |
||
6536 | 178 |
(** Co **) |
5899 | 179 |
|
6536 | 180 |
Goal "[| F i : A Co B; i: I; finite I |] \ |
6842 | 181 |
\ ==> PLam I F : (lift_set i A) Co (lift_set i B)"; |
5899 | 182 |
by (auto_tac |
183 |
(claset(), |
|
184 |
simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
|
6842 | 185 |
reachable_PLam_eq])); |
5899 | 186 |
by (auto_tac (claset(), |
6842 | 187 |
simpset() addsimps [constrains_def, PLam_def, Acts_JN])); |
5899 | 188 |
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
6842 | 189 |
qed "Constrains_imp_PLam_Constrains"; |
5972 | 190 |
|
6842 | 191 |
Goal "[| ALL j:I. f0 j : A j; i: I |] \ |
192 |
\ ==> drop_set i (INT j:I. lift_set j (A j)) = A i"; |
|
6299 | 193 |
by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
6842 | 194 |
simpset() addsimps [drop_set_def]) 1); |
195 |
qed "drop_set_INT_lift_set"; |
|
5972 | 196 |
|
6842 | 197 |
(*Again, we need the f0 premise so that PLam I F has an initial state; |
6575 | 198 |
otherwise its Co-property is vacuous.*) |
6842 | 199 |
Goal "[| PLam I F : (lift_set i A) Co (lift_set i B); \ |
200 |
\ i: I; finite I; f0: Init (PLam I F) |] \ |
|
6536 | 201 |
\ ==> F i : A Co B"; |
6575 | 202 |
by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1); |
5972 | 203 |
by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1); |
204 |
by (blast_tac (claset() addIs [reachable.Init]) 2); |
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
205 |
by (dtac PLam_constrains_drop_set 1); |
5972 | 206 |
by (assume_tac 1); |
207 |
by (asm_full_simp_tac |
|
6842 | 208 |
(simpset() addsimps [drop_set_lift_set_Int2, |
209 |
drop_set_INT_lift_set, reachable_PLam_eq]) 1); |
|
210 |
qed "PLam_Constrains_imp_Constrains"; |
|
5899 | 211 |
|
212 |
||
6842 | 213 |
Goal "[| i: I; finite I; f0: Init (PLam I F) |] \ |
214 |
\ ==> (PLam I F : (lift_set i A) Co (lift_set i B)) = \ |
|
6536 | 215 |
\ (F i : A Co B)"; |
6842 | 216 |
by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, |
217 |
PLam_Constrains_imp_Constrains]) 1); |
|
218 |
qed "PLam_Constrains"; |
|
5972 | 219 |
|
6842 | 220 |
Goal "[| i: I; finite I; f0: Init (PLam I F) |] \ |
221 |
\ ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"; |
|
222 |
by (asm_simp_tac (simpset() delsimps [Init_PLam] |
|
223 |
addsimps [Stable_def, PLam_Constrains]) 1); |
|
224 |
qed "PLam_Stable"; |
|
5899 | 225 |
|
226 |
||
6842 | 227 |
(** const_PLam (no dependence on i) doesn't require the f0 premise **) |
5899 | 228 |
|
6842 | 229 |
Goal "[| (plam x:I. F) : (lift_set i A) Co (lift_set i B); \ |
5972 | 230 |
\ i: I; finite I |] \ |
6536 | 231 |
\ ==> F : A Co B"; |
6575 | 232 |
by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1); |
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
233 |
by (dtac PLam_constrains_drop_set 1); |
5972 | 234 |
by (assume_tac 1); |
235 |
by (asm_full_simp_tac |
|
6842 | 236 |
(simpset() addsimps [drop_set_INT, |
237 |
drop_set_lift_set_Int2, Collect_conj_eq RS sym, |
|
238 |
reachable_PLam_eq]) 1); |
|
239 |
qed "const_PLam_Constrains_imp_Constrains"; |
|
5972 | 240 |
|
241 |
Goal "[| i: I; finite I |] \ |
|
6842 | 242 |
\ ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) = \ |
6536 | 243 |
\ (F : A Co B)"; |
6842 | 244 |
by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, |
245 |
const_PLam_Constrains_imp_Constrains]) 1); |
|
246 |
qed "const_PLam_Constrains"; |
|
5972 | 247 |
|
248 |
Goal "[| i: I; finite I |] \ |
|
6842 | 249 |
\ ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"; |
250 |
by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1); |
|
251 |
qed "const_PLam_Stable"; |
|
5972 | 252 |
|
7188
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
253 |
Goalw [Increasing_def] |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
254 |
"[| i: I; finite I |] \ |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
255 |
\ ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)"; |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
256 |
by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1); |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
257 |
by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2); |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
258 |
by (asm_full_simp_tac |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
259 |
(simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1); |
2bc63a44721b
re-organization of theorems from Alloc and PPROD, partly into new theory
paulson
parents:
6867
diff
changeset
|
260 |
qed "const_PLam_Increasing"; |
5972 | 261 |
|
262 |
||
263 |
(*** guarantees properties ***) |
|
264 |
||
6842 | 265 |
Goalw [PLam_def] |
7361 | 266 |
"[| i : I; lift_prog i (F i): X guarantees Y |] \ |
267 |
\ ==> (PLam I F) : X guarantees Y"; |
|
7344
d54e871d77e0
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
7188
diff
changeset
|
268 |
by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1); |
d54e871d77e0
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
7188
diff
changeset
|
269 |
qed "guarantees_PLam_I"; |
d54e871d77e0
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
7188
diff
changeset
|
270 |
|
d54e871d77e0
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
7188
diff
changeset
|
271 |
Goalw [PLam_def] |
7361 | 272 |
"[| ALL i:I. F i : X guarantees Y |] \ |
6842 | 273 |
\ ==> (PLam I F) : (INT i: I. lift_prog i `` X) \ |
7361 | 274 |
\ guarantees (INT i: I. lift_prog i `` Y)"; |
6835
588f791ee737
addition of drop_... operators with new results and simplification of old ones
paulson
parents:
6826
diff
changeset
|
275 |
by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1); |
7344
d54e871d77e0
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
7188
diff
changeset
|
276 |
bind_thm ("guarantees_PLam_INT", ballI RS result()); |
5972 | 277 |
|
6842 | 278 |
Goalw [PLam_def] |
7361 | 279 |
"[| ALL i:I. F i : X guarantees Y |] \ |
6842 | 280 |
\ ==> (PLam I F) : (UN i: I. lift_prog i `` X) \ |
7361 | 281 |
\ guarantees (UN i: I. lift_prog i `` Y)"; |
6835
588f791ee737
addition of drop_... operators with new results and simplification of old ones
paulson
parents:
6826
diff
changeset
|
282 |
by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1); |
7344
d54e871d77e0
new guarantees laws; also better natural deduction style for old ones
paulson
parents:
7188
diff
changeset
|
283 |
bind_thm ("guarantees_PLam_UN", ballI RS result()); |