equal
deleted
inserted
replaced
126 by (rule equiv_msgrel) |
126 by (rule equiv_msgrel) |
127 |
127 |
128 text{*The abstract message constructors*} |
128 text{*The abstract message constructors*} |
129 |
129 |
130 quotient_def |
130 quotient_def |
131 Nonce::"Nonce :: nat \<Rightarrow> msg" |
131 "Nonce :: nat \<Rightarrow> msg" |
132 where |
132 as |
133 "NONCE" |
133 "NONCE" |
134 |
134 |
135 quotient_def |
135 quotient_def |
136 MPair::"MPair :: msg \<Rightarrow> msg \<Rightarrow> msg" |
136 "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg" |
137 where |
137 as |
138 "MPAIR" |
138 "MPAIR" |
139 |
139 |
140 quotient_def |
140 quotient_def |
141 Crypt::"Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
141 "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
142 where |
142 as |
143 "CRYPT" |
143 "CRYPT" |
144 |
144 |
145 quotient_def |
145 quotient_def |
146 Decrypt::"Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
146 "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
147 where |
147 as |
148 "DECRYPT" |
148 "DECRYPT" |
149 |
149 |
150 lemma [quot_respect]: |
150 lemma [quot_respect]: |
151 shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT" |
151 shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT" |
152 by (auto intro: CRYPT) |
152 by (auto intro: CRYPT) |
163 by (lifting DC) |
163 by (lifting DC) |
164 |
164 |
165 subsection{*The Abstract Function to Return the Set of Nonces*} |
165 subsection{*The Abstract Function to Return the Set of Nonces*} |
166 |
166 |
167 quotient_def |
167 quotient_def |
168 nonces :: "nonces:: msg \<Rightarrow> nat set" |
168 "nonces:: msg \<Rightarrow> nat set" |
169 where |
169 as |
170 "freenonces" |
170 "freenonces" |
171 |
171 |
172 text{*Now prove the four equations for @{term nonces}*} |
172 text{*Now prove the four equations for @{term nonces}*} |
173 |
173 |
174 lemma [quot_respect]: |
174 lemma [quot_respect]: |
199 by (lifting freenonces.simps(4)) |
199 by (lifting freenonces.simps(4)) |
200 |
200 |
201 subsection{*The Abstract Function to Return the Left Part*} |
201 subsection{*The Abstract Function to Return the Left Part*} |
202 |
202 |
203 quotient_def |
203 quotient_def |
204 left :: "left:: msg \<Rightarrow> msg" |
204 "left:: msg \<Rightarrow> msg" |
205 where |
205 as |
206 "freeleft" |
206 "freeleft" |
207 |
207 |
208 lemma [quot_respect]: |
208 lemma [quot_respect]: |
209 shows "(op \<sim> ===> op \<sim>) freeleft freeleft" |
209 shows "(op \<sim> ===> op \<sim>) freeleft freeleft" |
210 by (simp add: msgrel_imp_eqv_freeleft) |
210 by (simp add: msgrel_imp_eqv_freeleft) |
226 by (lifting freeleft.simps(4)) |
226 by (lifting freeleft.simps(4)) |
227 |
227 |
228 subsection{*The Abstract Function to Return the Right Part*} |
228 subsection{*The Abstract Function to Return the Right Part*} |
229 |
229 |
230 quotient_def |
230 quotient_def |
231 right :: "right:: msg \<Rightarrow> msg" |
231 "right:: msg \<Rightarrow> msg" |
232 where |
232 as |
233 "freeright" |
233 "freeright" |
234 |
234 |
235 text{*Now prove the four equations for @{term right}*} |
235 text{*Now prove the four equations for @{term right}*} |
236 |
236 |
237 lemma [quot_respect]: |
237 lemma [quot_respect]: |
360 |
360 |
361 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't |
361 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't |
362 need this function in order to prove discrimination theorems.*} |
362 need this function in order to prove discrimination theorems.*} |
363 |
363 |
364 quotient_def |
364 quotient_def |
365 discrim :: "discrim:: msg \<Rightarrow> int" |
365 "discrim:: msg \<Rightarrow> int" |
366 where |
366 as |
367 "freediscrim" |
367 "freediscrim" |
368 |
368 |
369 text{*Now prove the four equations for @{term discrim}*} |
369 text{*Now prove the four equations for @{term discrim}*} |
370 |
370 |
371 lemma [quot_respect]: |
371 lemma [quot_respect]: |