author | paulson |
Mon, 06 Sep 1999 10:52:26 +0200 | |
changeset 7482 | 7badd511844d |
parent 7399 | cf780c2bcccf |
child 7537 | 875754b599df |
permissions | -rw-r--r-- |
6828 | 1 |
(* Title: HOL/UNITY/Alloc |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Specification of Chandy and Charpentier's Allocator |
|
7 |
*) |
|
8 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
9 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
10 |
Goal "~ f #2 ==> ~ (!t::nat. (#0 <= t & t <= #10) --> f t)"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
11 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
12 |
(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
13 |
Goal "[| b:A; a=b |] ==> a:A"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
14 |
by (etac ssubst 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
15 |
by (assume_tac 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
16 |
qed "subst_elem"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
17 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
18 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
19 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
20 |
|
6840 | 21 |
(*Generalized version allowing different clients*) |
22 |
Goal "[| Alloc : alloc_spec; \ |
|
23 |
\ Client : (lessThan Nclients) funcset client_spec; \ |
|
24 |
\ Network : network_spec |] \ |
|
25 |
\ ==> (extend sysOfAlloc Alloc) \ |
|
26 |
\ Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \ |
|
27 |
\ Join Network : system_spec"; |
|
28 |
||
29 |
Goal "System : system_spec"; |
|
30 |
||
31 |
||
6828 | 32 |
Goalw [sysOfAlloc_def] "inj sysOfAlloc"; |
33 |
by (rtac injI 1); |
|
7347 | 34 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
6828 | 35 |
qed "inj_sysOfAlloc"; |
36 |
||
37 |
Goalw [sysOfAlloc_def] "surj sysOfAlloc"; |
|
38 |
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s, \ |
|
39 |
\ allocAsk = allocAsk s, \ |
|
40 |
\ allocRel = allocRel s |), \ |
|
41 |
\ client s)")] surjI 1); |
|
7347 | 42 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
6828 | 43 |
qed "surj_sysOfAlloc"; |
44 |
||
45 |
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc]; |
|
46 |
||
7482 | 47 |
Goalw [good_map_def] "good_map sysOfAlloc"; |
48 |
by Auto_tac; |
|
49 |
qed "good_map_sysOfAlloc"; |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
50 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
51 |
(*MUST BE AUTOMATED: even the statement of such results*) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
52 |
Goal "!!s. inv sysOfAlloc s = \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
53 |
\ ((| allocGiv = allocGiv s, \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
54 |
\ allocAsk = allocAsk s, \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
55 |
\ allocRel = allocRel s|), \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
56 |
\ client s)"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
57 |
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
58 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
59 |
simpset() addsimps [sysOfAlloc_def])); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
60 |
qed "inv_sysOfAlloc_eq"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
61 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
62 |
|
7365 | 63 |
(**SHOULD NOT BE NECESSARY: The various injections into the system |
64 |
state need to be treated symmetrically or done automatically*) |
|
7347 | 65 |
Goalw [sysOfClient_def] "inj sysOfClient"; |
66 |
by (rtac injI 1); |
|
67 |
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD] |
|
68 |
addSWrapper record_split_wrapper, simpset())); |
|
69 |
qed "inj_sysOfClient"; |
|
70 |
||
71 |
Goalw [sysOfClient_def] "surj sysOfClient"; |
|
72 |
by (cut_facts_tac [surj_sysOfAlloc] 1); |
|
73 |
by (rewtac surj_def); |
|
74 |
by Auto_tac; |
|
75 |
by (Blast_tac 1); |
|
76 |
qed "surj_sysOfClient"; |
|
77 |
||
78 |
AddIffs [inj_sysOfClient, surj_sysOfClient]; |
|
79 |
||
7482 | 80 |
Goalw [good_map_def] "good_map sysOfClient"; |
81 |
by Auto_tac; |
|
82 |
qed "good_map_sysOfClient"; |
|
6828 | 83 |
|
7347 | 84 |
(*MUST BE AUTOMATED: even the statement of such results*) |
85 |
Goal "!!s. inv sysOfClient s = \ |
|
86 |
\ (client s, \ |
|
87 |
\ (| allocGiv = allocGiv s, \ |
|
88 |
\ allocAsk = allocAsk s, \ |
|
89 |
\ allocRel = allocRel s|) )"; |
|
90 |
by (rtac (inj_sysOfClient RS inv_f_eq) 1); |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
91 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
92 |
simpset() addsimps [sysOfAlloc_def, sysOfClient_def])); |
7365 | 93 |
qed "inv_sysOfClient_eq"; |
6837 | 94 |
|
95 |
||
7365 | 96 |
Open_locale "System"; |
97 |
||
98 |
val Alloc = thm "Alloc"; |
|
99 |
val Client = thm "Client"; |
|
100 |
val Network = thm "Network"; |
|
101 |
val System_def = thm "System_def"; |
|
102 |
||
103 |
AddIffs [finite_lessThan]; |
|
104 |
||
105 |
(*Client : <unfolded specification> *) |
|
106 |
val Client_Spec = |
|
107 |
rewrite_rule [client_spec_def, client_increasing_def, |
|
108 |
client_bounded_def, client_progress_def] Client; |
|
109 |
||
110 |
Goal "Client : UNIV guarantees Increasing ask"; |
|
111 |
by (cut_facts_tac [Client_Spec] 1); |
|
112 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
|
113 |
qed "Client_Increasing_ask"; |
|
114 |
||
115 |
Goal "Client : UNIV guarantees Increasing rel"; |
|
116 |
by (cut_facts_tac [Client_Spec] 1); |
|
117 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
|
118 |
qed "Client_Increasing_rel"; |
|
119 |
||
120 |
AddIffs [Client_Increasing_ask, Client_Increasing_rel]; |
|
121 |
||
122 |
Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"; |
|
123 |
by (cut_facts_tac [Client_Spec] 1); |
|
124 |
by Auto_tac; |
|
125 |
qed "Client_Bounded"; |
|
126 |
||
127 |
(*Client_Progress is cumbersome to state*) |
|
128 |
val Client_Progress = Client_Spec RS IntD2; |
|
6828 | 129 |
|
130 |
||
7365 | 131 |
(*Network : <unfolded specification> *) |
132 |
val Network_Spec = |
|
133 |
rewrite_rule [network_spec_def, network_ask_def, |
|
134 |
network_giv_def, network_rel_def] Network; |
|
135 |
||
136 |
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect |
|
137 |
exporting it from the locale*) |
|
138 |
val Network_Ask = Network_Spec RS IntD1 RS IntD1; |
|
139 |
val Network_Giv = Network_Spec RS IntD1 RS IntD2; |
|
140 |
val Network_Rel = Network_Spec RS IntD2 RS INT_D; |
|
141 |
||
142 |
||
143 |
(*Alloc : <unfolded specification> *) |
|
144 |
val Alloc_Spec = |
|
145 |
rewrite_rule [alloc_spec_def, alloc_increasing_def, |
|
146 |
alloc_safety_def, alloc_progress_def] Alloc; |
|
147 |
||
148 |
Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocAsk)"; |
|
149 |
by (cut_facts_tac [Alloc_Spec] 1); |
|
150 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1); |
|
151 |
qed "Alloc_Increasing"; |
|
152 |
||
153 |
val Alloc_Safety = Alloc_Spec RS IntD1 RS IntD2; |
|
154 |
val Alloc_Progress = (Alloc_Spec RS IntD2 |
|
155 |
|> simplify (simpset() addsimps [guarantees_INT_right])) |
|
156 |
RS bspec RS spec; |
|
157 |
||
158 |
||
7347 | 159 |
|
7365 | 160 |
(*Not sure what to say about the other components because they involve |
161 |
extend*) |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
162 |
Goalw [System_def] "Network <= System"; |
7365 | 163 |
by (blast_tac (claset() addIs [componentI]) 1); |
164 |
qed "Network_component_System"; |
|
165 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
166 |
Goalw [System_def] "(extend sysOfAlloc Alloc) <= System"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
167 |
by (blast_tac (claset() addIs [componentI]) 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
168 |
qed "Alloc_component_System"; |
7365 | 169 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
170 |
AddIffs [Network_component_System, Alloc_component_System]; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
171 |
|
7365 | 172 |
|
173 |
(* F : UNIV guarantees Increasing func |
|
174 |
==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *) |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
175 |
val extend_Client_guar_Increasing = |
7482 | 176 |
good_map_sysOfClient RS export extend_guar_Increasing |
7365 | 177 |
|> simplify (simpset() addsimps [inv_sysOfClient_eq]); |
178 |
||
179 |
||
180 |
(** Proof of property (1) **) |
|
181 |
||
182 |
(*step 1*) |
|
183 |
Goalw [System_def] |
|
184 |
"i < Nclients ==> System : Increasing (rel o sub i o client)"; |
|
185 |
by (rtac ([guaranteesI RS disjI2 RS guarantees_Join_I, UNIV_I] |
|
186 |
MRS guaranteesD) 1); |
|
187 |
by (asm_simp_tac |
|
188 |
(simpset() addsimps [guarantees_PLam_I, |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
189 |
extend_Client_guar_Increasing RS guaranteesD, |
7365 | 190 |
lift_prog_guar_Increasing]) 1); |
7347 | 191 |
qed "System_Increasing_rel"; |
6828 | 192 |
|
7365 | 193 |
(*Note: the first step above performs simple quantifier reasoning. It could |
194 |
be replaced by a proof mentioning no guarantees primitives*) |
|
6828 | 195 |
|
196 |
||
7365 | 197 |
(*step 2*) |
198 |
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)"; |
|
199 |
by (rtac Follows_Increasing1 1); |
|
200 |
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD, |
|
201 |
System_Increasing_rel, Network]) 1); |
|
202 |
qed "System_Increasing_allocRel"; |
|
6828 | 203 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
204 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
205 |
(*NEED TO PROVE something like this (maybe without premise)*) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
206 |
Goal "i < Nclients ==> System : (sub i o allocRel) localTo Network"; |
7347 | 207 |
|
7482 | 208 |
fun alloc_export th = good_map_sysOfAlloc RS export th; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
209 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
210 |
val extend_Alloc_guar_Increasing = |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
211 |
alloc_export extend_guar_Increasing |
7365 | 212 |
|> simplify (simpset() addsimps [inv_sysOfAlloc_eq]); |
6828 | 213 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
214 |
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
215 |
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
216 |
by (res_inst_tac |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
217 |
[("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
218 |
\ Int Increasing (sub i o allocRel))")] |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
219 |
component_guaranteesD 1);; |
7482 | 220 |
by (rtac Alloc_component_System 3); |
221 |
by (rtac project_guarantees 1); |
|
222 |
by (rtac Alloc_Safety 1); |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
223 |
by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2 |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
224 |
THEN |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
225 |
full_simp_tac |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
226 |
(simpset() addsimps [inv_sysOfAlloc_eq, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
227 |
alloc_export Collect_eq_extend_set RS sym]) 2); |
7482 | 228 |
by Auto_tac; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
229 |
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 3); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
230 |
|
7482 | 231 |
by (dtac bspec 1); |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
232 |
by (Blast_tac 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
233 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
234 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
235 |
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
236 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
237 |
[| i < Nclients; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
238 |
extend sysOfAlloc Alloc Join G |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
239 |
: (sub i o allocRel) localTo Network & |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
240 |
extend sysOfAlloc Alloc Join G : Increasing (sub i o allocRel) |] |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
241 |
==> Alloc Join project sysOfAlloc G : Increasing (sub i o allocRel) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
242 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
243 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
244 |
[| i < Nclients; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
245 |
H : (sub i o allocRel) localTo Network & |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
246 |
H : Increasing (sub i o allocRel) |] |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
247 |
==> project sysOfAlloc H : Increasing (sub i o allocRel) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
248 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
249 |
Open_locale"Extend"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
250 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
251 |
Goal "(H : (func o f) localTo G) ==> (project h H : func localTo (project h G))"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
252 |
by (asm_full_simp_tac |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
253 |
(simpset() addsimps [localTo_def, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
254 |
project_extend_Join RS sym, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
255 |
Diff_project_stable, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
256 |
Collect_eq_extend_set RS sym]) 1); |
7482 | 257 |
by Auto_tac; |
258 |
by (rtac Diff_project_stable 1); |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
259 |
PROBABLY FALSE; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
260 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
261 |
by (Clarify_tac 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
262 |
by (dres_inst_tac [("x","z")] spec 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
263 |
|
7482 | 264 |
by (rtac (alloc_export project_Always_D) 2); |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
265 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
266 |
by (rtac (alloc_export extend_Always RS iffD2) 2); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
267 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
268 |
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
269 |
|
7482 | 270 |
by (rtac guaranteesI 1); |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
271 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
272 |
by (res_inst_tac |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
273 |
[("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
274 |
component_guaranteesD 1);; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
275 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
276 |
|
7365 | 277 |
by (rtac (Alloc_Safety RS component_guaranteesD) 1); |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
278 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
279 |
|
7482 | 280 |
by (rtac (alloc_export guarantees_imp_extend_guarantees RS guarantees_weaken) 1); |
281 |
by (rtac Alloc_Safety 1); |