author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45694  4a8743618257 
child 49834  b27bbb021df1 
permissions  rwrr 
41959  1 
(* Title: HOL/Induct/QuoDataType.thy 
14527  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 2004 University of Cambridge 

4 
*) 

5 

6 
header{*Defining an Initial Algebra by Quotienting a Free Algebra*} 

7 

16417  8 
theory QuoDataType imports Main begin 
14527  9 

10 
subsection{*Defining the Free Algebra*} 

11 

12 
text{*Messages with encryption and decryption as free constructors.*} 

13 
datatype 

14 
freemsg = NONCE nat 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30198
diff
changeset

15 
 MPAIR freemsg freemsg 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30198
diff
changeset

16 
 CRYPT nat freemsg 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30198
diff
changeset

17 
 DECRYPT nat freemsg 
14527  18 

19 
text{*The equivalence relation, which makes encryption and decryption inverses 

23746  20 
provided the keys are the same. 
19736  21 

23746  22 
The first two rules are the desired equations. The next four rules 
14527  23 
make the equations applicable to subterms. The last two rules are symmetry 
24 
and transitivity.*} 

23746  25 

26 
inductive_set 

27 
msgrel :: "(freemsg * freemsg) set" 

28 
and msg_rel :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50) 

29 
where 

30 
"X \<sim> Y == (X,Y) \<in> msgrel" 

31 
 CD: "CRYPT K (DECRYPT K X) \<sim> X" 

32 
 DC: "DECRYPT K (CRYPT K X) \<sim> X" 

33 
 NONCE: "NONCE N \<sim> NONCE N" 

34 
 MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'" 

35 
 CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'" 

36 
 DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'" 

37 
 SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X" 

38 
 TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z" 

14527  39 

40 

41 
text{*Proving that it is an equivalence relation*} 

42 

43 
lemma msgrel_refl: "X \<sim> X" 

18460  44 
by (induct X) (blast intro: msgrel.intros)+ 
14527  45 

46 
theorem equiv_msgrel: "equiv UNIV msgrel" 

18460  47 
proof  
30198  48 
have "refl msgrel" by (simp add: refl_on_def msgrel_refl) 
18460  49 
moreover have "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM) 
50 
moreover have "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS) 

51 
ultimately show ?thesis by (simp add: equiv_def) 

14527  52 
qed 
53 

54 

55 
subsection{*Some Functions on the Free Algebra*} 

56 

57 
subsubsection{*The Set of Nonces*} 

58 

59 
text{*A function to return the set of nonces present in a message. It will 

60 
be lifted to the initial algrebra, to serve as an example of that process.*} 

39246  61 
primrec freenonces :: "freemsg \<Rightarrow> nat set" where 
62 
"freenonces (NONCE N) = {N}" 

63 
 "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y" 

64 
 "freenonces (CRYPT K X) = freenonces X" 

65 
 "freenonces (DECRYPT K X) = freenonces X" 

14527  66 

67 
text{*This theorem lets us prove that the nonces function respects the 

68 
equivalence relation. It also helps us prove that Nonce 

69 
(the abstract constructor) is injective*} 

70 
theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V" 

18460  71 
by (induct set: msgrel) auto 
14527  72 

73 

74 
subsubsection{*The Left Projection*} 

75 

76 
text{*A function to return the left part of the top pair in a message. It will 

77 
be lifted to the initial algrebra, to serve as an example of that process.*} 

39246  78 
primrec freeleft :: "freemsg \<Rightarrow> freemsg" where 
79 
"freeleft (NONCE N) = NONCE N" 

80 
 "freeleft (MPAIR X Y) = X" 

81 
 "freeleft (CRYPT K X) = freeleft X" 

82 
 "freeleft (DECRYPT K X) = freeleft X" 

14527  83 

84 
text{*This theorem lets us prove that the left function respects the 

85 
equivalence relation. It also helps us prove that MPair 

86 
(the abstract constructor) is injective*} 

14658  87 
theorem msgrel_imp_eqv_freeleft: 
88 
"U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V" 

18460  89 
by (induct set: msgrel) (auto intro: msgrel.intros) 
14527  90 

91 

92 
subsubsection{*The Right Projection*} 

93 

94 
text{*A function to return the right part of the top pair in a message.*} 

39246  95 
primrec freeright :: "freemsg \<Rightarrow> freemsg" where 
96 
"freeright (NONCE N) = NONCE N" 

97 
 "freeright (MPAIR X Y) = Y" 

98 
 "freeright (CRYPT K X) = freeright X" 

99 
 "freeright (DECRYPT K X) = freeright X" 

14527  100 

101 
text{*This theorem lets us prove that the right function respects the 

102 
equivalence relation. It also helps us prove that MPair 

103 
(the abstract constructor) is injective*} 

14658  104 
theorem msgrel_imp_eqv_freeright: 
105 
"U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V" 

18460  106 
by (induct set: msgrel) (auto intro: msgrel.intros) 
14527  107 

108 

15152  109 
subsubsection{*The Discriminator for Constructors*} 
14527  110 

15152  111 
text{*A function to distinguish nonces, mpairs and encryptions*} 
39246  112 
primrec freediscrim :: "freemsg \<Rightarrow> int" where 
113 
"freediscrim (NONCE N) = 0" 

114 
 "freediscrim (MPAIR X Y) = 1" 

115 
 "freediscrim (CRYPT K X) = freediscrim X + 2" 

116 
 "freediscrim (DECRYPT K X) = freediscrim X  2" 

14527  117 

118 
text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*} 

15152  119 
theorem msgrel_imp_eq_freediscrim: 
120 
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V" 

18460  121 
by (induct set: msgrel) auto 
14527  122 

123 

124 
subsection{*The Initial Algebra: A Quotiented Message Type*} 

125 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
41959
diff
changeset

126 
definition "Msg = UNIV//msgrel" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
41959
diff
changeset

127 

4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
41959
diff
changeset

128 
typedef (open) msg = Msg 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
41959
diff
changeset

129 
morphisms Rep_Msg Abs_Msg 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
41959
diff
changeset

130 
unfolding Msg_def by (auto simp add: quotient_def) 
14527  131 

132 

133 
text{*The abstract message constructors*} 

19736  134 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

135 
Nonce :: "nat \<Rightarrow> msg" where 
19736  136 
"Nonce N = Abs_Msg(msgrel``{NONCE N})" 
14527  137 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

138 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

139 
MPair :: "[msg,msg] \<Rightarrow> msg" where 
19736  140 
"MPair X Y = 
15120  141 
Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})" 
14527  142 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

143 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

144 
Crypt :: "[nat,msg] \<Rightarrow> msg" where 
19736  145 
"Crypt K X = 
15120  146 
Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})" 
14527  147 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

148 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

149 
Decrypt :: "[nat,msg] \<Rightarrow> msg" where 
19736  150 
"Decrypt K X = 
15120  151 
Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})" 
14527  152 

153 

154 
text{*Reduces equality of equivalence classes to the @{term msgrel} relation: 

155 
@{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"} *} 

156 
lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I] 

157 

158 
declare equiv_msgrel_iff [simp] 

159 

160 

161 
text{*All equivalence classes belong to set of representatives*} 

15169  162 
lemma [simp]: "msgrel``{U} \<in> Msg" 
14527  163 
by (auto simp add: Msg_def quotient_def intro: msgrel_refl) 
164 

165 
lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg" 

166 
apply (rule inj_on_inverseI) 

167 
apply (erule Abs_Msg_inverse) 

168 
done 

169 

170 
text{*Reduces equality on abstractions to equality on representatives*} 

171 
declare inj_on_Abs_Msg [THEN inj_on_iff, simp] 

172 

173 
declare Abs_Msg_inverse [simp] 

174 

175 

176 
subsubsection{*Characteristic Equations for the Abstract Constructors*} 

177 

178 
lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) = 

179 
Abs_Msg (msgrel``{MPAIR U V})" 

180 
proof  

15169  181 
have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel" 
40825  182 
by (auto simp add: congruent2_def msgrel.MPAIR) 
14527  183 
thus ?thesis 
14658  184 
by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel]) 
14527  185 
qed 
186 

187 
lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})" 

188 
proof  

15169  189 
have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel" 
40825  190 
by (auto simp add: congruent_def msgrel.CRYPT) 
14527  191 
thus ?thesis 
192 
by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel]) 

193 
qed 

194 

195 
lemma Decrypt: 

196 
"Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})" 

197 
proof  

15169  198 
have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel" 
40825  199 
by (auto simp add: congruent_def msgrel.DECRYPT) 
14527  200 
thus ?thesis 
201 
by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel]) 

202 
qed 

203 

204 
text{*Case analysis on the representation of a msg as an equivalence class.*} 

205 
lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]: 

206 
"(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P" 

207 
apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE]) 

208 
apply (drule arg_cong [where f=Abs_Msg]) 

209 
apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl) 

210 
done 

211 

212 
text{*Establishing these two equations is the point of the whole exercise*} 

14533  213 
theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X" 
14527  214 
by (cases X, simp add: Crypt Decrypt CD) 
215 

14533  216 
theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X" 
14527  217 
by (cases X, simp add: Crypt Decrypt DC) 
218 

219 

220 
subsection{*The Abstract Function to Return the Set of Nonces*} 

221 

19736  222 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

223 
nonces :: "msg \<Rightarrow> nat set" where 
19736  224 
"nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)" 
14527  225 

15169  226 
lemma nonces_congruent: "freenonces respects msgrel" 
40825  227 
by (auto simp add: congruent_def msgrel_imp_eq_freenonces) 
14527  228 

229 

230 
text{*Now prove the four equations for @{term nonces}*} 

231 

232 
lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}" 

233 
by (simp add: nonces_def Nonce_def 

234 
UN_equiv_class [OF equiv_msgrel nonces_congruent]) 

235 

236 
lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X \<union> nonces Y" 

237 
apply (cases X, cases Y) 

238 
apply (simp add: nonces_def MPair 

239 
UN_equiv_class [OF equiv_msgrel nonces_congruent]) 

240 
done 

241 

242 
lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X" 

243 
apply (cases X) 

244 
apply (simp add: nonces_def Crypt 

245 
UN_equiv_class [OF equiv_msgrel nonces_congruent]) 

246 
done 

247 

248 
lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X" 

249 
apply (cases X) 

250 
apply (simp add: nonces_def Decrypt 

251 
UN_equiv_class [OF equiv_msgrel nonces_congruent]) 

252 
done 

253 

254 

255 
subsection{*The Abstract Function to Return the Left Part*} 

256 

19736  257 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

258 
left :: "msg \<Rightarrow> msg" where 
19736  259 
"left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})" 
14527  260 

15169  261 
lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel" 
40825  262 
by (auto simp add: congruent_def msgrel_imp_eqv_freeleft) 
14527  263 

264 
text{*Now prove the four equations for @{term left}*} 

265 

266 
lemma left_Nonce [simp]: "left (Nonce N) = Nonce N" 

267 
by (simp add: left_def Nonce_def 

268 
UN_equiv_class [OF equiv_msgrel left_congruent]) 

269 

270 
lemma left_MPair [simp]: "left (MPair X Y) = X" 

271 
apply (cases X, cases Y) 

272 
apply (simp add: left_def MPair 

273 
UN_equiv_class [OF equiv_msgrel left_congruent]) 

274 
done 

275 

276 
lemma left_Crypt [simp]: "left (Crypt K X) = left X" 

277 
apply (cases X) 

278 
apply (simp add: left_def Crypt 

279 
UN_equiv_class [OF equiv_msgrel left_congruent]) 

280 
done 

281 

282 
lemma left_Decrypt [simp]: "left (Decrypt K X) = left X" 

283 
apply (cases X) 

284 
apply (simp add: left_def Decrypt 

285 
UN_equiv_class [OF equiv_msgrel left_congruent]) 

286 
done 

287 

288 

289 
subsection{*The Abstract Function to Return the Right Part*} 

290 

19736  291 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

292 
right :: "msg \<Rightarrow> msg" where 
19736  293 
"right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})" 
14527  294 

15169  295 
lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel" 
40825  296 
by (auto simp add: congruent_def msgrel_imp_eqv_freeright) 
14527  297 

298 
text{*Now prove the four equations for @{term right}*} 

299 

300 
lemma right_Nonce [simp]: "right (Nonce N) = Nonce N" 

301 
by (simp add: right_def Nonce_def 

302 
UN_equiv_class [OF equiv_msgrel right_congruent]) 

303 

304 
lemma right_MPair [simp]: "right (MPair X Y) = Y" 

305 
apply (cases X, cases Y) 

306 
apply (simp add: right_def MPair 

307 
UN_equiv_class [OF equiv_msgrel right_congruent]) 

308 
done 

309 

310 
lemma right_Crypt [simp]: "right (Crypt K X) = right X" 

311 
apply (cases X) 

312 
apply (simp add: right_def Crypt 

313 
UN_equiv_class [OF equiv_msgrel right_congruent]) 

314 
done 

315 

316 
lemma right_Decrypt [simp]: "right (Decrypt K X) = right X" 

317 
apply (cases X) 

318 
apply (simp add: right_def Decrypt 

319 
UN_equiv_class [OF equiv_msgrel right_congruent]) 

320 
done 

321 

322 

323 
subsection{*Injectivity Properties of Some Constructors*} 

324 

325 
lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n" 

326 
by (drule msgrel_imp_eq_freenonces, simp) 

327 

328 
text{*Can also be proved using the function @{term nonces}*} 

329 
lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)" 

330 
by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq) 

331 

332 
lemma MPAIR_imp_eqv_left: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'" 

14658  333 
by (drule msgrel_imp_eqv_freeleft, simp) 
14527  334 

335 
lemma MPair_imp_eq_left: 

336 
assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'" 

337 
proof  

338 
from eq 

339 
have "left (MPair X Y) = left (MPair X' Y')" by simp 

340 
thus ?thesis by simp 

341 
qed 

342 

343 
lemma MPAIR_imp_eqv_right: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'" 

14658  344 
by (drule msgrel_imp_eqv_freeright, simp) 
14527  345 

346 
lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'" 

347 
apply (cases X, cases X', cases Y, cases Y') 

348 
apply (simp add: MPair) 

349 
apply (erule MPAIR_imp_eqv_right) 

350 
done 

351 

352 
theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" 

14533  353 
by (blast dest: MPair_imp_eq_left MPair_imp_eq_right) 
14527  354 

355 
lemma NONCE_neqv_MPAIR: "NONCE m \<sim> MPAIR X Y \<Longrightarrow> False" 

15152  356 
by (drule msgrel_imp_eq_freediscrim, simp) 
14527  357 

358 
theorem Nonce_neq_MPair [iff]: "Nonce N \<noteq> MPair X Y" 

359 
apply (cases X, cases Y) 

360 
apply (simp add: Nonce_def MPair) 

361 
apply (blast dest: NONCE_neqv_MPAIR) 

362 
done 

363 

15152  364 
text{*Example suggested by a referee*} 
365 
theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) \<noteq> Nonce N" 

366 
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim) 

367 

368 
text{*...and many similar results*} 

15172  369 
theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N" 
15152  370 
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim) 
371 

14533  372 
theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')" 
373 
proof 

374 
assume "Crypt K X = Crypt K X'" 

375 
hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp 

376 
thus "X = X'" by simp 

377 
next 

378 
assume "X = X'" 

379 
thus "Crypt K X = Crypt K X'" by simp 

380 
qed 

381 

382 
theorem Decrypt_Decrypt_eq [iff]: "(Decrypt K X = Decrypt K X') = (X=X')" 

383 
proof 

384 
assume "Decrypt K X = Decrypt K X'" 

385 
hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp 

386 
thus "X = X'" by simp 

387 
next 

388 
assume "X = X'" 

389 
thus "Decrypt K X = Decrypt K X'" by simp 

390 
qed 

391 

392 
lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]: 

393 
assumes N: "\<And>N. P (Nonce N)" 

394 
and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)" 

395 
and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)" 

396 
and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)" 

397 
shows "P msg" 

18460  398 
proof (cases msg) 
399 
case (Abs_Msg U) 

400 
have "P (Abs_Msg (msgrel `` {U}))" 

14533  401 
proof (induct U) 
402 
case (NONCE N) 

403 
with N show ?case by (simp add: Nonce_def) 

404 
next 

405 
case (MPAIR X Y) 

406 
with M [of "Abs_Msg (msgrel `` {X})" "Abs_Msg (msgrel `` {Y})"] 

407 
show ?case by (simp add: MPair) 

408 
next 

409 
case (CRYPT K X) 

410 
with C [of "Abs_Msg (msgrel `` {X})"] 

411 
show ?case by (simp add: Crypt) 

412 
next 

413 
case (DECRYPT K X) 

414 
with D [of "Abs_Msg (msgrel `` {X})"] 

415 
show ?case by (simp add: Decrypt) 

416 
qed 

18460  417 
with Abs_Msg show ?thesis by (simp only:) 
14533  418 
qed 
419 

15152  420 

421 
subsection{*The Abstract Discriminator*} 

422 

423 
text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't 

424 
need this function in order to prove discrimination theorems.*} 

425 

19736  426 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

427 
discrim :: "msg \<Rightarrow> int" where 
39910  428 
"discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})" 
15152  429 

15169  430 
lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel" 
40825  431 
by (auto simp add: congruent_def msgrel_imp_eq_freediscrim) 
15152  432 

433 
text{*Now prove the four equations for @{term discrim}*} 

434 

435 
lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0" 

436 
by (simp add: discrim_def Nonce_def 

437 
UN_equiv_class [OF equiv_msgrel discrim_congruent]) 

438 

439 
lemma discrim_MPair [simp]: "discrim (MPair X Y) = 1" 

440 
apply (cases X, cases Y) 

441 
apply (simp add: discrim_def MPair 

442 
UN_equiv_class [OF equiv_msgrel discrim_congruent]) 

443 
done 

444 

445 
lemma discrim_Crypt [simp]: "discrim (Crypt K X) = discrim X + 2" 

446 
apply (cases X) 

447 
apply (simp add: discrim_def Crypt 

448 
UN_equiv_class [OF equiv_msgrel discrim_congruent]) 

449 
done 

450 

451 
lemma discrim_Decrypt [simp]: "discrim (Decrypt K X) = discrim X  2" 

452 
apply (cases X) 

453 
apply (simp add: discrim_def Decrypt 

454 
UN_equiv_class [OF equiv_msgrel discrim_congruent]) 

455 
done 

456 

457 

14527  458 
end 
459 