equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 header{*The Message Theory, Modified for SET*} |
7 header{*The Message Theory, Modified for SET*} |
8 |
8 |
9 theory Message_SET |
9 theory Message_SET |
10 imports Main Nat_Int_Bij |
10 imports Main Nat_Bijection |
11 begin |
11 begin |
12 |
12 |
13 subsection{*General Lemmas*} |
13 subsection{*General Lemmas*} |
14 |
14 |
15 text{*Needed occasionally with @{text spy_analz_tac}, e.g. in |
15 text{*Needed occasionally with @{text spy_analz_tac}, e.g. in |
79 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
79 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
80 "{|x, y|}" == "CONST MPair x y" |
80 "{|x, y|}" == "CONST MPair x y" |
81 |
81 |
82 |
82 |
83 definition nat_of_agent :: "agent => nat" where |
83 definition nat_of_agent :: "agent => nat" where |
84 "nat_of_agent == agent_case (curry nat2_to_nat 0) |
84 "nat_of_agent == agent_case (curry prod_encode 0) |
85 (curry nat2_to_nat 1) |
85 (curry prod_encode 1) |
86 (curry nat2_to_nat 2) |
86 (curry prod_encode 2) |
87 (curry nat2_to_nat 3) |
87 (curry prod_encode 3) |
88 (nat2_to_nat (4,0))" |
88 (prod_encode (4,0))" |
89 --{*maps each agent to a unique natural number, for specifications*} |
89 --{*maps each agent to a unique natural number, for specifications*} |
90 |
90 |
91 text{*The function is indeed injective*} |
91 text{*The function is indeed injective*} |
92 lemma inj_nat_of_agent: "inj nat_of_agent" |
92 lemma inj_nat_of_agent: "inj nat_of_agent" |
93 by (simp add: nat_of_agent_def inj_on_def curry_def |
93 by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split) |
94 nat2_to_nat_inj [THEN inj_eq] split: agent.split) |
|
95 |
94 |
96 |
95 |
97 constdefs |
96 constdefs |
98 (*Keys useful to decrypt elements of a message set*) |
97 (*Keys useful to decrypt elements of a message set*) |
99 keysFor :: "msg set => key set" |
98 keysFor :: "msg set => key set" |