equal
deleted
inserted
replaced
7 Inductive relations "parts", "analz" and "synth" |
7 Inductive relations "parts", "analz" and "synth" |
8 *) |
8 *) |
9 |
9 |
10 theory Message = Main |
10 theory Message = Main |
11 files ("Message_lemmas.ML"): |
11 files ("Message_lemmas.ML"): |
12 |
|
13 (*Eliminates a commonly-occurring expression*) |
|
14 lemma [simp] : "~ (\<forall> x. x\<noteq>y)" |
|
15 by blast |
|
16 |
12 |
17 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
13 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) |
18 lemma [simp] : "A Un (B Un A) = B Un A" |
14 lemma [simp] : "A Un (B Un A) = B Un A" |
19 by blast |
15 by blast |
20 |
16 |
29 |
25 |
30 (*The inverse of a symmetric key is itself; |
26 (*The inverse of a symmetric key is itself; |
31 that of a public key is the private key and vice versa*) |
27 that of a public key is the private key and vice versa*) |
32 |
28 |
33 constdefs |
29 constdefs |
34 isSymKey :: "key=>bool" |
30 symKeys :: "key set" |
35 "isSymKey K == (invKey K = K)" |
31 "symKeys == {K. invKey K = K}" |
36 |
32 |
37 datatype (*We allow any number of friendly agents*) |
33 datatype (*We allow any number of friendly agents*) |
38 agent = Server | Friend nat | Spy |
34 agent = Server | Friend nat | Spy |
39 |
35 |
40 datatype |
36 datatype |