14527

1 
(* Title: HOL/Induct/QuoDataType


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 2004 University of Cambridge


5 


6 
*)


7 


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


9 

16417

10 
theory QuoDataType imports Main begin

14527

11 


12 
subsection{*Defining the Free Algebra*}


13 


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


15 
datatype


16 
freemsg = NONCE nat


17 
 MPAIR freemsg freemsg


18 
 CRYPT nat freemsg


19 
 DECRYPT nat freemsg


20 


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


22 
provided the keys are the same.*}


23 
consts msgrel :: "(freemsg * freemsg) set"


24 

19736

25 
abbreviation


26 
msg_rel :: "[freemsg, freemsg] => bool" (infixl "~~" 50)


27 
"X ~~ Y == (X,Y) \<in> msgrel"


28 


29 
const_syntax (xsymbols)


30 
msg_rel (infixl "\<sim>" 50)


31 
const_syntax (HTML output)


32 
msg_rel (infixl "\<sim>" 50)

14527

33 


34 
text{*The first two rules are the desired equations. The next four rules


35 
make the equations applicable to subterms. The last two rules are symmetry


36 
and transitivity.*}


37 
inductive "msgrel"


38 
intros


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


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


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


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


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


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


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


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


47 


48 


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


50 


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

18460

52 
by (induct X) (blast intro: msgrel.intros)+

14527

53 


54 
theorem equiv_msgrel: "equiv UNIV msgrel"

18460

55 
proof 


56 
have "reflexive msgrel" by (simp add: refl_def msgrel_refl)


57 
moreover have "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)


58 
moreover have "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)


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

14527

60 
qed


61 


62 


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


64 


65 
subsubsection{*The Set of Nonces*}


66 


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


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


69 
consts


70 
freenonces :: "freemsg \<Rightarrow> nat set"


71 


72 
primrec


73 
"freenonces (NONCE N) = {N}"


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


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


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


77 


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


79 
equivalence relation. It also helps us prove that Nonce


80 
(the abstract constructor) is injective*}


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

18460

82 
by (induct set: msgrel) auto

14527

83 


84 


85 
subsubsection{*The Left Projection*}


86 


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


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

14658

89 
consts freeleft :: "freemsg \<Rightarrow> freemsg"

14527

90 
primrec

14658

91 
"freeleft (NONCE N) = NONCE N"


92 
"freeleft (MPAIR X Y) = X"


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


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

14527

95 


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


97 
equivalence relation. It also helps us prove that MPair


98 
(the abstract constructor) is injective*}

14658

99 
theorem msgrel_imp_eqv_freeleft:


100 
"U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"

18460

101 
by (induct set: msgrel) (auto intro: msgrel.intros)

14527

102 


103 


104 
subsubsection{*The Right Projection*}


105 


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

14658

107 
consts freeright :: "freemsg \<Rightarrow> freemsg"

14527

108 
primrec

14658

109 
"freeright (NONCE N) = NONCE N"


110 
"freeright (MPAIR X Y) = Y"


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


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

14527

113 


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


115 
equivalence relation. It also helps us prove that MPair


116 
(the abstract constructor) is injective*}

14658

117 
theorem msgrel_imp_eqv_freeright:


118 
"U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"

18460

119 
by (induct set: msgrel) (auto intro: msgrel.intros)

14527

120 


121 

15152

122 
subsubsection{*The Discriminator for Constructors*}

14527

123 

15152

124 
text{*A function to distinguish nonces, mpairs and encryptions*}


125 
consts freediscrim :: "freemsg \<Rightarrow> int"

14527

126 
primrec

15152

127 
"freediscrim (NONCE N) = 0"


128 
"freediscrim (MPAIR X Y) = 1"


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


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

14527

131 


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

15152

133 
theorem msgrel_imp_eq_freediscrim:


134 
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"

18460

135 
by (induct set: msgrel) auto

14527

136 


137 


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


139 


140 
typedef (Msg) msg = "UNIV//msgrel"

18460

141 
by (auto simp add: quotient_def)

14527

142 


143 


144 
text{*The abstract message constructors*}

19736

145 
definition

14527

146 
Nonce :: "nat \<Rightarrow> msg"

19736

147 
"Nonce N = Abs_Msg(msgrel``{NONCE N})"

14527

148 


149 
MPair :: "[msg,msg] \<Rightarrow> msg"

19736

150 
"MPair X Y =

15120

151 
Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"

14527

152 


153 
Crypt :: "[nat,msg] \<Rightarrow> msg"

19736

154 
"Crypt K X =

15120

155 
Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"

14527

156 


157 
Decrypt :: "[nat,msg] \<Rightarrow> msg"

19736

158 
"Decrypt K X =

15120

159 
Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"

14527

160 


161 


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


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


164 
lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]


165 


166 
declare equiv_msgrel_iff [simp]


167 


168 


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

15169

170 
lemma [simp]: "msgrel``{U} \<in> Msg"

14527

171 
by (auto simp add: Msg_def quotient_def intro: msgrel_refl)


172 


173 
lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"


174 
apply (rule inj_on_inverseI)


175 
apply (erule Abs_Msg_inverse)


176 
done


177 


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


179 
declare inj_on_Abs_Msg [THEN inj_on_iff, simp]


180 


181 
declare Abs_Msg_inverse [simp]


182 


183 


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


185 


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


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


188 
proof 

15169

189 
have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"

14527

190 
by (simp add: congruent2_def msgrel.MPAIR)


191 
thus ?thesis

14658

192 
by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])

14527

193 
qed


194 


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


196 
proof 

15169

197 
have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"

14527

198 
by (simp add: congruent_def msgrel.CRYPT)


199 
thus ?thesis


200 
by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])


201 
qed


202 


203 
lemma Decrypt:


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


205 
proof 

15169

206 
have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"

14527

207 
by (simp add: congruent_def msgrel.DECRYPT)


208 
thus ?thesis


209 
by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])


210 
qed


211 


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


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


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


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


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


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


218 
done


219 


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

14533

221 
theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"

14527

222 
by (cases X, simp add: Crypt Decrypt CD)


223 

14533

224 
theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"

14527

225 
by (cases X, simp add: Crypt Decrypt DC)


226 


227 


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


229 

19736

230 
definition

14527

231 
nonces :: "msg \<Rightarrow> nat set"

19736

232 
"nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"

14527

233 

15169

234 
lemma nonces_congruent: "freenonces respects msgrel"

14527

235 
by (simp add: congruent_def msgrel_imp_eq_freenonces)


236 


237 


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


239 


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


241 
by (simp add: nonces_def Nonce_def


242 
UN_equiv_class [OF equiv_msgrel nonces_congruent])


243 


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


245 
apply (cases X, cases Y)


246 
apply (simp add: nonces_def MPair


247 
UN_equiv_class [OF equiv_msgrel nonces_congruent])


248 
done


249 


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


251 
apply (cases X)


252 
apply (simp add: nonces_def Crypt


253 
UN_equiv_class [OF equiv_msgrel nonces_congruent])


254 
done


255 


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


257 
apply (cases X)


258 
apply (simp add: nonces_def Decrypt


259 
UN_equiv_class [OF equiv_msgrel nonces_congruent])


260 
done


261 


262 


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


264 

19736

265 
definition

14527

266 
left :: "msg \<Rightarrow> msg"

19736

267 
"left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"

14527

268 

15169

269 
lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"

14658

270 
by (simp add: congruent_def msgrel_imp_eqv_freeleft)

14527

271 


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


273 


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


275 
by (simp add: left_def Nonce_def


276 
UN_equiv_class [OF equiv_msgrel left_congruent])


277 


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


279 
apply (cases X, cases Y)


280 
apply (simp add: left_def MPair


281 
UN_equiv_class [OF equiv_msgrel left_congruent])


282 
done


283 


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


285 
apply (cases X)


286 
apply (simp add: left_def Crypt


287 
UN_equiv_class [OF equiv_msgrel left_congruent])


288 
done


289 


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


291 
apply (cases X)


292 
apply (simp add: left_def Decrypt


293 
UN_equiv_class [OF equiv_msgrel left_congruent])


294 
done


295 


296 


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


298 

19736

299 
definition

14527

300 
right :: "msg \<Rightarrow> msg"

19736

301 
"right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"

14527

302 

15169

303 
lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"

14658

304 
by (simp add: congruent_def msgrel_imp_eqv_freeright)

14527

305 


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


307 


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


309 
by (simp add: right_def Nonce_def


310 
UN_equiv_class [OF equiv_msgrel right_congruent])


311 


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


313 
apply (cases X, cases Y)


314 
apply (simp add: right_def MPair


315 
UN_equiv_class [OF equiv_msgrel right_congruent])


316 
done


317 


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


319 
apply (cases X)


320 
apply (simp add: right_def Crypt


321 
UN_equiv_class [OF equiv_msgrel right_congruent])


322 
done


323 


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


325 
apply (cases X)


326 
apply (simp add: right_def Decrypt


327 
UN_equiv_class [OF equiv_msgrel right_congruent])


328 
done


329 


330 


331 
subsection{*Injectivity Properties of Some Constructors*}


332 


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


334 
by (drule msgrel_imp_eq_freenonces, simp)


335 


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


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


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


339 


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

14658

341 
by (drule msgrel_imp_eqv_freeleft, simp)

14527

342 


343 
lemma MPair_imp_eq_left:


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


345 
proof 


346 
from eq


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


348 
thus ?thesis by simp


349 
qed


350 


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

14658

352 
by (drule msgrel_imp_eqv_freeright, simp)

14527

353 


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


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


356 
apply (simp add: MPair)


357 
apply (erule MPAIR_imp_eqv_right)


358 
done


359 


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

14533

361 
by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)

14527

362 


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

15152

364 
by (drule msgrel_imp_eq_freediscrim, simp)

14527

365 


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


367 
apply (cases X, cases Y)


368 
apply (simp add: Nonce_def MPair)


369 
apply (blast dest: NONCE_neqv_MPAIR)


370 
done


371 

15152

372 
text{*Example suggested by a referee*}


373 
theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) \<noteq> Nonce N"


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


375 


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

15172

377 
theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"

15152

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


379 

14533

380 
theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')"


381 
proof


382 
assume "Crypt K X = Crypt K X'"


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


384 
thus "X = X'" by simp


385 
next


386 
assume "X = X'"


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


388 
qed


389 


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


391 
proof


392 
assume "Decrypt K X = Decrypt K X'"


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


394 
thus "X = X'" by simp


395 
next


396 
assume "X = X'"


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


398 
qed


399 


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


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


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


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


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


405 
shows "P msg"

18460

406 
proof (cases msg)


407 
case (Abs_Msg U)


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

14533

409 
proof (induct U)


410 
case (NONCE N)


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


412 
next


413 
case (MPAIR X Y)


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


415 
show ?case by (simp add: MPair)


416 
next


417 
case (CRYPT K X)


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


419 
show ?case by (simp add: Crypt)


420 
next


421 
case (DECRYPT K X)


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


423 
show ?case by (simp add: Decrypt)


424 
qed

18460

425 
with Abs_Msg show ?thesis by (simp only:)

14533

426 
qed


427 

15152

428 


429 
subsection{*The Abstract Discriminator*}


430 


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


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


433 

19736

434 
definition

15152

435 
discrim :: "msg \<Rightarrow> int"

19736

436 
"discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"

15152

437 

15169

438 
lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"

15152

439 
by (simp add: congruent_def msgrel_imp_eq_freediscrim)


440 


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


442 


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


444 
by (simp add: discrim_def Nonce_def


445 
UN_equiv_class [OF equiv_msgrel discrim_congruent])


446 


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


448 
apply (cases X, cases Y)


449 
apply (simp add: discrim_def MPair


450 
UN_equiv_class [OF equiv_msgrel discrim_congruent])


451 
done


452 


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


454 
apply (cases X)


455 
apply (simp add: discrim_def Crypt


456 
UN_equiv_class [OF equiv_msgrel discrim_congruent])


457 
done


458 


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


460 
apply (cases X)


461 
apply (simp add: discrim_def Decrypt


462 
UN_equiv_class [OF equiv_msgrel discrim_congruent])


463 
done


464 


465 

14527

466 
end


467 
