equal
deleted
inserted
replaced
31 goalw thy [isSymKey_def] "~ isSymKey (priK A)"; |
31 goalw thy [isSymKey_def] "~ isSymKey (priK A)"; |
32 by (Simp_tac 1); |
32 by (Simp_tac 1); |
33 qed "not_isSymKey_priK"; |
33 qed "not_isSymKey_priK"; |
34 |
34 |
35 AddIffs [not_isSymKey_pubK, not_isSymKey_priK]; |
35 AddIffs [not_isSymKey_pubK, not_isSymKey_priK]; |
|
36 |
|
37 |
|
38 (** "Image" equations that hold for injective functions **) |
|
39 |
|
40 goal thy "(invKey x : invKey``A) = (x:A)"; |
|
41 by (Auto_tac()); |
|
42 qed "invKey_image_eq"; |
|
43 |
|
44 (*holds because invKey is injective*) |
|
45 goal thy "(pubK x : pubK``A) = (x:A)"; |
|
46 by (Auto_tac()); |
|
47 qed "pubK_image_eq"; |
|
48 |
|
49 goal thy "(priK x ~: pubK``A)"; |
|
50 by (Auto_tac()); |
|
51 qed "priK_pubK_image_eq"; |
|
52 Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq]; |
|
53 |
36 |
54 |
37 (** Rewrites should not refer to initState(Friend i) |
55 (** Rewrites should not refer to initState(Friend i) |
38 -- not in normal form! **) |
56 -- not in normal form! **) |
39 |
57 |
40 goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}"; |
58 goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}"; |