author | paulson |
Tue, 23 Sep 2003 15:41:33 +0200 | |
changeset 14200 | d8598e24f8fa |
parent 14133 | 4cd1a7e7edac |
child 14207 | f20fbb141673 |
permissions | -rw-r--r-- |
2318 | 1 |
(* Title: HOL/Auth/Public |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3478
diff
changeset
|
6 |
Theory of Public Keys (common to all public-key protocols) |
2318 | 7 |
|
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3478
diff
changeset
|
8 |
Private and public keys; initial states of agents |
2318 | 9 |
*) |
10 |
||
13922 | 11 |
theory Public = Event: |
12 |
||
13 |
subsection{*Asymmetric Keys*} |
|
2318 | 14 |
|
15 |
consts |
|
13922 | 16 |
(*the bool is TRUE if a signing key*) |
17 |
publicKey :: "[bool,agent] => key" |
|
2318 | 18 |
|
19 |
syntax |
|
13922 | 20 |
pubEK :: "agent => key" |
21 |
pubSK :: "agent => key" |
|
22 |
||
23 |
privateKey :: "[bool,agent] => key" |
|
24 |
priEK :: "agent => key" |
|
25 |
priSK :: "agent => key" |
|
26 |
||
27 |
translations |
|
28 |
"pubEK" == "publicKey False" |
|
29 |
"pubSK" == "publicKey True" |
|
30 |
||
31 |
(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) |
|
32 |
"privateKey b A" == "invKey (publicKey b A)" |
|
33 |
"priEK A" == "privateKey False A" |
|
34 |
"priSK A" == "privateKey True A" |
|
35 |
||
36 |
||
37 |
text{*These translations give backward compatibility. They represent the |
|
38 |
simple situation where the signature and encryption keys are the same.*} |
|
39 |
syntax |
|
40 |
pubK :: "agent => key" |
|
41 |
priK :: "agent => key" |
|
42 |
||
43 |
translations |
|
44 |
"pubK A" == "pubEK A" |
|
45 |
"priK A" == "invKey (pubEK A)" |
|
46 |
||
47 |
||
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
48 |
text{*By freeness of agents, no two agents have the same key. Since |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
49 |
@{term "True\<noteq>False"}, no agent has identical signing and encryption keys*} |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
50 |
specification (publicKey) |
13922 | 51 |
injective_publicKey: |
52 |
"publicKey b A = publicKey c A' ==> b=c & A=A'" |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
53 |
apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"]) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
54 |
apply (auto simp add: inj_on_def split: agent.split) |
14133 | 55 |
apply presburger+ |
56 |
(*faster would be this: |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
57 |
apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+ |
14133 | 58 |
*) |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
59 |
done |
13922 | 60 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
61 |
|
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
62 |
axioms |
13922 | 63 |
(*No private key equals any public key (essential to ensure that private |
64 |
keys are private!) *) |
|
65 |
privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'" |
|
66 |
||
13926 | 67 |
declare privateKey_neq_publicKey [THEN not_sym, iff] |
13922 | 68 |
|
69 |
||
13926 | 70 |
subsection{*Basic properties of @{term pubK} and @{term priK}*} |
13922 | 71 |
|
72 |
lemma [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')" |
|
73 |
by (blast dest!: injective_publicKey) |
|
74 |
||
75 |
lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys" |
|
13926 | 76 |
by (simp add: symKeys_def) |
13922 | 77 |
|
78 |
lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys" |
|
13926 | 79 |
by (simp add: symKeys_def) |
13922 | 80 |
|
81 |
lemma symKey_neq_priEK: "K \<in> symKeys ==> K \<noteq> priEK A" |
|
82 |
by auto |
|
83 |
||
84 |
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'" |
|
13926 | 85 |
by blast |
13922 | 86 |
|
87 |
lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)" |
|
13926 | 88 |
by (unfold symKeys_def, auto) |
2318 | 89 |
|
13922 | 90 |
lemma analz_symKeys_Decrypt: |
91 |
"[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] |
|
92 |
==> X \<in> analz H" |
|
93 |
by (auto simp add: symKeys_def) |
|
94 |
||
95 |
||
96 |
||
97 |
subsection{*"Image" equations that hold for injective functions*} |
|
98 |
||
99 |
lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)" |
|
13926 | 100 |
by auto |
13922 | 101 |
|
102 |
(*holds because invKey is injective*) |
|
103 |
lemma publicKey_image_eq [simp]: |
|
104 |
"(publicKey b x \<in> publicKey c ` AA) = (b=c & x \<in> AA)" |
|
105 |
by auto |
|
106 |
||
107 |
lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA" |
|
13926 | 108 |
by auto |
13922 | 109 |
|
110 |
lemma privateKey_image_eq [simp]: |
|
111 |
"(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)" |
|
112 |
by auto |
|
113 |
||
114 |
lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> invKey ` publicKey c ` AS" |
|
13926 | 115 |
by auto |
13922 | 116 |
|
117 |
||
118 |
subsection{*Symmetric Keys*} |
|
119 |
||
120 |
text{*For some protocols, it is convenient to equip agents with symmetric as |
|
121 |
well as asymmetric keys. The theory @{text Shared} assumes that all keys |
|
122 |
are symmetric.*} |
|
123 |
||
124 |
consts |
|
125 |
shrK :: "agent => key" --{*long-term shared keys*} |
|
126 |
||
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
127 |
specification (shrK) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
128 |
inj_shrK: "inj shrK" |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
129 |
--{*No two agents have the same long-term key*} |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
130 |
apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
131 |
apply (simp add: inj_on_def split: agent.split) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
132 |
done |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
133 |
|
13922 | 134 |
axioms |
135 |
sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*} |
|
136 |
||
137 |
(*Injectiveness: Agents' long-term keys are distinct.*) |
|
138 |
declare inj_shrK [THEN inj_eq, iff] |
|
139 |
||
140 |
lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C" |
|
13926 | 141 |
by (simp add: symKeys_neq_imp_neq) |
13922 | 142 |
|
143 |
declare priK_neq_shrK [THEN not_sym, simp] |
|
144 |
||
145 |
lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C" |
|
13926 | 146 |
by (simp add: symKeys_neq_imp_neq) |
13922 | 147 |
|
148 |
declare pubK_neq_shrK [THEN not_sym, simp] |
|
149 |
||
150 |
lemma priEK_noteq_shrK [simp]: "priEK A \<noteq> shrK B" |
|
151 |
by auto |
|
152 |
||
153 |
lemma publicKey_notin_image_shrK [simp]: "publicKey b x \<notin> shrK ` AA" |
|
154 |
by auto |
|
155 |
||
156 |
lemma privateKey_notin_image_shrK [simp]: "privateKey b x \<notin> shrK ` AA" |
|
157 |
by auto |
|
158 |
||
159 |
lemma shrK_notin_image_publicKey [simp]: "shrK x \<notin> publicKey b ` AA" |
|
160 |
by auto |
|
161 |
||
162 |
lemma shrK_notin_image_privateKey [simp]: "shrK x \<notin> invKey ` publicKey b ` AA" |
|
163 |
by auto |
|
164 |
||
165 |
lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)" |
|
166 |
by auto |
|
167 |
||
168 |
||
169 |
subsection{*Initial States of Agents*} |
|
170 |
||
171 |
text{*Note: for all practical purposes, all that matters is the initial |
|
172 |
knowledge of the Spy. All other agents are automata, merely following the |
|
173 |
protocol.*} |
|
2318 | 174 |
|
5183 | 175 |
primrec |
2318 | 176 |
(*Agents know their private key and all public keys*) |
13922 | 177 |
initState_Server: |
178 |
"initState Server = |
|
179 |
{Key (priEK Server), Key (priSK Server)} \<union> |
|
180 |
(Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)" |
|
181 |
||
182 |
initState_Friend: |
|
183 |
"initState (Friend i) = |
|
184 |
{Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union> |
|
185 |
(Key ` range pubEK) \<union> (Key ` range pubSK)" |
|
186 |
||
187 |
initState_Spy: |
|
188 |
"initState Spy = |
|
189 |
(Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union> |
|
190 |
(Key ` shrK ` bad) \<union> |
|
191 |
(Key ` range pubEK) \<union> (Key ` range pubSK)" |
|
192 |
||
193 |
||
194 |
text{*These lemmas allow reasoning about @{term "used evs"} rather than |
|
13935 | 195 |
@{term "knows Spy evs"}, which is useful when there are private Notes. |
196 |
Because they depend upon the definition of @{term initState}, they cannot |
|
197 |
be moved up.*} |
|
13922 | 198 |
|
199 |
lemma used_parts_subset_parts [rule_format]: |
|
200 |
"\<forall>X \<in> used evs. parts {X} \<subseteq> used evs" |
|
201 |
apply (induct evs) |
|
202 |
prefer 2 |
|
203 |
apply (simp add: used_Cons) |
|
204 |
apply (rule ballI) |
|
13935 | 205 |
apply (case_tac a, auto) |
206 |
apply (auto dest!: parts_cut) |
|
13922 | 207 |
txt{*Base case*} |
13935 | 208 |
apply (simp add: used_Nil) |
13922 | 209 |
done |
210 |
||
211 |
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H" |
|
212 |
by (drule used_parts_subset_parts, simp, blast) |
|
213 |
||
214 |
lemma MPair_used [elim!]: |
|
215 |
"[| {|X,Y|} \<in> used H; |
|
216 |
[| X \<in> used H; Y \<in> used H |] ==> P |] |
|
217 |
==> P" |
|
218 |
by (blast dest: MPair_used_D) |
|
219 |
||
220 |
||
221 |
text{*Rewrites should not refer to @{term "initState(Friend i)"} because |
|
222 |
that expression is not in normal form.*} |
|
223 |
||
224 |
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" |
|
225 |
apply (unfold keysFor_def) |
|
226 |
apply (induct_tac "C") |
|
227 |
apply (auto intro: range_eqI) |
|
228 |
done |
|
229 |
||
230 |
lemma Crypt_notin_initState: "Crypt K X \<notin> parts (initState B)" |
|
231 |
by (induct B, auto) |
|
232 |
||
13935 | 233 |
lemma Crypt_notin_used_empty [simp]: "Crypt K X \<notin> used []" |
234 |
by (simp add: Crypt_notin_initState used_Nil) |
|
235 |
||
13922 | 236 |
|
237 |
(*** Basic properties of shrK ***) |
|
238 |
||
239 |
(*Agents see their own shared keys!*) |
|
240 |
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A" |
|
13926 | 241 |
by (induct_tac "A", auto) |
13922 | 242 |
|
243 |
lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs" |
|
244 |
by (simp add: initState_subset_knows [THEN subsetD]) |
|
245 |
||
246 |
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs" |
|
13926 | 247 |
by (rule initState_into_used, blast) |
13922 | 248 |
|
249 |
(** Fresh keys never clash with long-term shared keys **) |
|
250 |
||
251 |
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys |
|
252 |
from long-term shared keys*) |
|
253 |
lemma Key_not_used: "Key K \<notin> used evs ==> K \<notin> range shrK" |
|
13926 | 254 |
by blast |
13922 | 255 |
|
256 |
lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K" |
|
13926 | 257 |
by blast |
13922 | 258 |
|
2318 | 259 |
|
260 |
||
13922 | 261 |
subsection{*Function @{term spies} *} |
262 |
||
263 |
text{*Agents see their own private keys!*} |
|
264 |
lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A" |
|
13926 | 265 |
by (induct_tac "A", auto) |
13922 | 266 |
|
267 |
text{*Agents see all public keys!*} |
|
268 |
lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B" |
|
13926 | 269 |
by (case_tac "B", auto) |
13922 | 270 |
|
271 |
text{*All public keys are visible*} |
|
272 |
lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs" |
|
273 |
apply (induct_tac "evs") |
|
274 |
apply (simp_all add: imageI knows_Cons split add: event.split) |
|
275 |
done |
|
276 |
||
277 |
declare spies_pubK [THEN analz.Inj, iff] |
|
278 |
||
279 |
text{*Spy sees private keys of bad agents!*} |
|
280 |
lemma Spy_spies_bad_privateKey [intro!]: |
|
281 |
"A \<in> bad ==> Key (privateKey b A) \<in> spies evs" |
|
282 |
apply (induct_tac "evs") |
|
283 |
apply (simp_all add: imageI knows_Cons split add: event.split) |
|
284 |
done |
|
285 |
||
286 |
text{*Spy sees long-term shared keys of bad agents!*} |
|
287 |
lemma Spy_spies_bad_shrK [intro!]: |
|
288 |
"A \<in> bad ==> Key (shrK A) \<in> spies evs" |
|
289 |
apply (induct_tac "evs") |
|
290 |
apply (simp_all add: imageI knows_Cons split add: event.split) |
|
291 |
done |
|
292 |
||
293 |
lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs" |
|
294 |
apply (rule initState_into_used) |
|
295 |
apply (rule publicKey_in_initState [THEN parts.Inj]) |
|
296 |
done |
|
297 |
||
298 |
lemma privateKey_into_used [iff]: "Key (privateKey b A) \<in> used evs" |
|
299 |
apply(rule initState_into_used) |
|
300 |
apply(rule priK_in_initState [THEN parts.Inj]) |
|
301 |
done |
|
302 |
||
303 |
||
304 |
subsection{*Fresh Nonces*} |
|
305 |
||
306 |
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)" |
|
13926 | 307 |
by (induct_tac "B", auto) |
13922 | 308 |
|
309 |
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []" |
|
13926 | 310 |
by (simp add: used_Nil) |
13922 | 311 |
|
11104 | 312 |
|
13922 | 313 |
subsection{*Supply fresh nonces for possibility theorems*} |
314 |
||
315 |
text{*In any trace, there is an upper bound N on the greatest nonce in use*} |
|
316 |
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs" |
|
317 |
apply (induct_tac "evs") |
|
13926 | 318 |
apply (rule_tac x = 0 in exI) |
13922 | 319 |
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split) |
320 |
apply safe |
|
321 |
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ |
|
322 |
done |
|
323 |
||
324 |
lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs" |
|
13926 | 325 |
by (rule Nonce_supply_lemma [THEN exE], blast) |
13922 | 326 |
|
327 |
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs" |
|
328 |
apply (rule Nonce_supply_lemma [THEN exE]) |
|
13926 | 329 |
apply (rule someI, fast) |
13922 | 330 |
done |
331 |
||
13956 | 332 |
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} |
13922 | 333 |
|
334 |
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H" |
|
13926 | 335 |
by blast |
11104 | 336 |
|
13922 | 337 |
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C" |
13926 | 338 |
by blast |
13922 | 339 |
|
340 |
ML |
|
341 |
{* |
|
342 |
val Key_not_used = thm "Key_not_used"; |
|
343 |
val insert_Key_singleton = thm "insert_Key_singleton"; |
|
344 |
val insert_Key_image = thm "insert_Key_image"; |
|
345 |
*} |
|
346 |
||
347 |
(* |
|
348 |
val not_symKeys_pubK = thm "not_symKeys_pubK"; |
|
349 |
val not_symKeys_priK = thm "not_symKeys_priK"; |
|
350 |
val symKeys_neq_imp_neq = thm "symKeys_neq_imp_neq"; |
|
351 |
val analz_symKeys_Decrypt = thm "analz_symKeys_Decrypt"; |
|
352 |
val invKey_image_eq = thm "invKey_image_eq"; |
|
353 |
val pubK_image_eq = thm "pubK_image_eq"; |
|
354 |
val priK_pubK_image_eq = thm "priK_pubK_image_eq"; |
|
355 |
val keysFor_parts_initState = thm "keysFor_parts_initState"; |
|
356 |
val priK_in_initState = thm "priK_in_initState"; |
|
357 |
val spies_pubK = thm "spies_pubK"; |
|
358 |
val Spy_spies_bad = thm "Spy_spies_bad"; |
|
359 |
val Nonce_notin_initState = thm "Nonce_notin_initState"; |
|
360 |
val Nonce_notin_used_empty = thm "Nonce_notin_used_empty"; |
|
361 |
||
362 |
*) |
|
363 |
||
364 |
||
365 |
lemma invKey_K [simp]: "K \<in> symKeys ==> invKey K = K" |
|
11287 | 366 |
by (simp add: symKeys_def) |
367 |
||
13922 | 368 |
lemma Crypt_imp_keysFor :"[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H" |
13926 | 369 |
by (drule Crypt_imp_invKey_keysFor, simp) |
13922 | 370 |
|
371 |
||
372 |
subsection{*Specialized Methods for Possibility Theorems*} |
|
373 |
||
374 |
ML |
|
375 |
{* |
|
376 |
val Nonce_supply1 = thm "Nonce_supply1"; |
|
377 |
val Nonce_supply = thm "Nonce_supply"; |
|
378 |
||
379 |
(*Tactic for possibility theorems (Isar interface)*) |
|
380 |
fun gen_possibility_tac ss state = state |> |
|
381 |
REPEAT (*omit used_Says so that Nonces start from different traces!*) |
|
382 |
(ALLGOALS (simp_tac (ss delsimps [used_Says])) |
|
383 |
THEN |
|
384 |
REPEAT_FIRST (eq_assume_tac ORELSE' |
|
385 |
resolve_tac [refl, conjI, Nonce_supply])) |
|
386 |
||
387 |
(*Tactic for possibility theorems (ML script version)*) |
|
388 |
fun possibility_tac state = gen_possibility_tac (simpset()) state |
|
389 |
*} |
|
11104 | 390 |
|
391 |
method_setup possibility = {* |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11104
diff
changeset
|
392 |
Method.ctxt_args (fn ctxt => |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11104
diff
changeset
|
393 |
Method.METHOD (fn facts => |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11104
diff
changeset
|
394 |
gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} |
11104 | 395 |
"for proving possibility theorems" |
2318 | 396 |
|
13922 | 397 |
|
398 |
||
13926 | 399 |
lemmas analz_image_freshK_simps = |
400 |
simp_thms mem_simps --{*these two allow its use with @{text "only:"}*} |
|
401 |
disj_comms |
|
402 |
image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14133
diff
changeset
|
403 |
analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD] |
13926 | 404 |
insert_Key_singleton |
405 |
Key_not_used insert_Key_image Un_assoc [THEN sym] |
|
406 |
||
13922 | 407 |
ML |
408 |
{* |
|
409 |
val analz_image_freshK_ss = |
|
410 |
simpset() delsimps [image_insert, image_Un] |
|
411 |
delsimps [imp_disjL] (*reduces blow-up*) |
|
13926 | 412 |
addsimps thms"analz_image_freshK_simps" |
13922 | 413 |
*} |
414 |
||
2318 | 415 |
end |