equal
deleted
inserted
replaced
30 lemma disjoint_image_iff: "(A <= - (f`I)) = (\<forall>i\<in>I. f i \<notin> A)" |
30 lemma disjoint_image_iff: "(A <= - (f`I)) = (\<forall>i\<in>I. f i \<notin> A)" |
31 by blast |
31 by blast |
32 |
32 |
33 |
33 |
34 |
34 |
35 types |
35 type_synonym key = nat |
36 key = nat |
|
37 |
36 |
38 consts |
37 consts |
39 all_symmetric :: bool --{*true if all keys are symmetric*} |
38 all_symmetric :: bool --{*true if all keys are symmetric*} |
40 invKey :: "key=>key" --{*inverse of a symmetric key*} |
39 invKey :: "key=>key" --{*inverse of a symmetric key*} |
41 |
40 |