equal
deleted
inserted
replaced
11 |
11 |
12 header {*Extensions to Standard Theories*} |
12 header {*Extensions to Standard Theories*} |
13 |
13 |
14 theory Extensions = Event: |
14 theory Extensions = Event: |
15 |
15 |
16 declare insert_Diff_single [simp del] |
|
17 |
|
18 subsection{*Extensions to Theory @{text Set}*} |
16 subsection{*Extensions to Theory @{text Set}*} |
19 |
17 |
20 lemma eq: "[| !!x. x:A ==> x:B; !!x. x:B ==> x:A |] ==> A=B" |
18 lemma eq: "[| !!x. x:A ==> x:B; !!x. x:B ==> x:A |] ==> A=B" |
21 by auto |
19 by auto |
22 |
|
23 lemma Un_eq: "[| A=A'; B=B' |] ==> A Un B = A' Un B'" |
|
24 by auto |
|
25 |
|
26 lemma insert_absorb_substI: "[| x:A; P (insert x A) |] ==> P A" |
|
27 by (simp add: insert_absorb) |
|
28 |
|
29 lemma insert_Diff_substD: "[| x:A; P A |] ==> P (insert x (A - {x}))" |
|
30 by (simp add: insert_Diff) |
|
31 |
|
32 lemma insert_Diff_substI: "[| x:A; P (insert x (A - {x})) |] ==> P A" |
|
33 by (simp add: insert_Diff) |
|
34 |
20 |
35 lemma insert_Un: "P ({x} Un A) ==> P (insert x A)" |
21 lemma insert_Un: "P ({x} Un A) ==> P (insert x A)" |
36 by simp |
22 by simp |
37 |
23 |
38 lemma in_sub: "x:A ==> {x}<=A" |
24 lemma in_sub: "x:A ==> {x}<=A" |
199 lemma analz_eq: "A=A' ==> analz A = analz A'" |
185 lemma analz_eq: "A=A' ==> analz A = analz A'" |
200 by auto |
186 by auto |
201 |
187 |
202 lemmas insert_commute_substI = insert_commute [THEN ssubst] |
188 lemmas insert_commute_substI = insert_commute [THEN ssubst] |
203 |
189 |
204 lemma analz_insertD: "[| Crypt K Y:H; Key (invKey K):H |] |
190 lemma analz_insertD: |
205 ==> analz (insert Y H) = analz H" |
191 "[| Crypt K Y:H; Key (invKey K):H |] ==> analz (insert Y H) = analz H" |
206 apply (rule_tac x="Crypt K Y" and P="%H. analz (insert Y H) = analz H" |
192 by (blast intro: analz.Decrypt analz_insert_eq) |
207 in insert_absorb_substI, simp) |
|
208 by (rule_tac insert_commute_substI, simp) |
|
209 |
193 |
210 lemma must_decrypt [rule_format,dest]: "[| X:analz H; has_no_pair H |] ==> |
194 lemma must_decrypt [rule_format,dest]: "[| X:analz H; has_no_pair H |] ==> |
211 X ~:H --> (EX K Y. Crypt K Y:H & Key (invKey K):H)" |
195 X ~:H --> (EX K Y. Crypt K Y:H & Key (invKey K):H)" |
212 by (erule analz.induct, auto) |
196 by (erule analz.induct, auto) |
213 |
197 |
365 subsubsection{*knows without initState*} |
349 subsubsection{*knows without initState*} |
366 |
350 |
367 consts knows' :: "agent => event list => msg set" |
351 consts knows' :: "agent => event list => msg set" |
368 |
352 |
369 primrec |
353 primrec |
370 "knows' A [] = {}" |
354 knows'_Nil: |
371 "knows' A (ev # evs) = ( |
355 "knows' A [] = {}" |
372 if A = Spy then ( |
356 |
373 case ev of |
357 knows'_Cons0: |
374 Says A' B X => insert X (knows' A evs) |
358 "knows' A (ev # evs) = ( |
375 | Gets A' X => knows' A evs |
359 if A = Spy then ( |
376 | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A evs |
360 case ev of |
377 ) else ( |
361 Says A' B X => insert X (knows' A evs) |
378 case ev of |
362 | Gets A' X => knows' A evs |
379 Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs |
363 | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A evs |
380 | Gets A' X => if A=A' then insert X (knows' A evs) else knows' A evs |
364 ) else ( |
381 | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs |
365 case ev of |
382 ))" |
366 Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs |
|
367 | Gets A' X => if A=A' then insert X (knows' A evs) else knows' A evs |
|
368 | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs |
|
369 ))" |
383 |
370 |
384 translations "spies" == "knows Spy" |
371 translations "spies" == "knows Spy" |
385 |
372 |
386 syntax spies' :: "event list => msg set" |
373 syntax spies' :: "event list => msg set" |
387 |
374 |
406 |
393 |
407 lemma knows_Cons: "knows A (ev#evs) = initState A Un knows' A [ev] |
394 lemma knows_Cons: "knows A (ev#evs) = initState A Un knows' A [ev] |
408 Un knows A evs" |
395 Un knows A evs" |
409 apply (simp only: knows_decomp) |
396 apply (simp only: knows_decomp) |
410 apply (rule_tac s="(knows' A [ev] Un knows' A evs) Un initState A" in trans) |
397 apply (rule_tac s="(knows' A [ev] Un knows' A evs) Un initState A" in trans) |
411 by (rule Un_eq, rule knows'_Cons, simp, blast) |
398 apply (simp only: knows'_Cons [of A ev evs] Un_ac) |
|
399 apply blast |
|
400 done |
|
401 |
412 |
402 |
413 lemmas knows_Cons_substI = knows_Cons [THEN ssubst] |
403 lemmas knows_Cons_substI = knows_Cons [THEN ssubst] |
414 lemmas knows_Cons_substD = knows_Cons [THEN sym, THEN ssubst] |
404 lemmas knows_Cons_substD = knows_Cons [THEN sym, THEN ssubst] |
415 |
405 |
416 lemma knows'_sub_spies': "[| evs:p; has_only_Says p; one_step p |] |
406 lemma knows'_sub_spies': "[| evs:p; has_only_Says p; one_step p |] |