src/HOL/Induct/QuoDataType.thy
 author haftmann Tue Nov 30 17:22:59 2010 +0100 (2010-11-30) changeset 40825 c55ee3793712 parent 39910 10097e0a9dbd child 41959 b460124855b8 permissions -rw-r--r--
```     1 (*  Title:      HOL/Induct/QuoDataType
```
```     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
```
```     8 theory QuoDataType imports Main begin
```
```     9
```
```    10 subsection{*Defining the Free Algebra*}
```
```    11
```
```    12 text{*Messages with encryption and decryption as free constructors.*}
```
```    13 datatype
```
```    14      freemsg = NONCE  nat
```
```    15              | MPAIR  freemsg freemsg
```
```    16              | CRYPT  nat freemsg
```
```    17              | DECRYPT  nat freemsg
```
```    18
```
```    19 text{*The equivalence relation, which makes encryption and decryption inverses
```
```    20 provided the keys are the same.
```
```    21
```
```    22 The first two rules are the desired equations. The next four rules
```
```    23 make the equations applicable to subterms. The last two rules are symmetry
```
```    24 and transitivity.*}
```
```    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"
```
```    39
```
```    40
```
```    41 text{*Proving that it is an equivalence relation*}
```
```    42
```
```    43 lemma msgrel_refl: "X \<sim> X"
```
```    44   by (induct X) (blast intro: msgrel.intros)+
```
```    45
```
```    46 theorem equiv_msgrel: "equiv UNIV msgrel"
```
```    47 proof -
```
```    48   have "refl msgrel" by (simp add: refl_on_def msgrel_refl)
```
```    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)
```
```    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.*}
```
```    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"
```
```    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"
```
```    71   by (induct set: msgrel) auto
```
```    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.*}
```
```    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"
```
```    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*}
```
```    87 theorem msgrel_imp_eqv_freeleft:
```
```    88      "U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"
```
```    89   by (induct set: msgrel) (auto intro: msgrel.intros)
```
```    90
```
```    91
```
```    92 subsubsection{*The Right Projection*}
```
```    93
```
```    94 text{*A function to return the right part of the top pair in a message.*}
```
```    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"
```
```   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*}
```
```   104 theorem msgrel_imp_eqv_freeright:
```
```   105      "U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"
```
```   106   by (induct set: msgrel) (auto intro: msgrel.intros)
```
```   107
```
```   108
```
```   109 subsubsection{*The Discriminator for Constructors*}
```
```   110
```
```   111 text{*A function to distinguish nonces, mpairs and encryptions*}
```
```   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"
```
```   117
```
```   118 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
```
```   119 theorem msgrel_imp_eq_freediscrim:
```
```   120      "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
```
```   121   by (induct set: msgrel) auto
```
```   122
```
```   123
```
```   124 subsection{*The Initial Algebra: A Quotiented Message Type*}
```
```   125
```
```   126 typedef (Msg)  msg = "UNIV//msgrel"
```
```   127   by (auto simp add: quotient_def)
```
```   128
```
```   129
```
```   130 text{*The abstract message constructors*}
```
```   131 definition
```
```   132   Nonce :: "nat \<Rightarrow> msg" where
```
```   133   "Nonce N = Abs_Msg(msgrel``{NONCE N})"
```
```   134
```
```   135 definition
```
```   136   MPair :: "[msg,msg] \<Rightarrow> msg" where
```
```   137    "MPair X Y =
```
```   138        Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
```
```   139
```
```   140 definition
```
```   141   Crypt :: "[nat,msg] \<Rightarrow> msg" where
```
```   142    "Crypt K X =
```
```   143        Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
```
```   144
```
```   145 definition
```
```   146   Decrypt :: "[nat,msg] \<Rightarrow> msg" where
```
```   147    "Decrypt K X =
```
```   148        Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
```
```   149
```
```   150
```
```   151 text{*Reduces equality of equivalence classes to the @{term msgrel} relation:
```
```   152   @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"} *}
```
```   153 lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]
```
```   154
```
```   155 declare equiv_msgrel_iff [simp]
```
```   156
```
```   157
```
```   158 text{*All equivalence classes belong to set of representatives*}
```
```   159 lemma [simp]: "msgrel``{U} \<in> Msg"
```
```   160 by (auto simp add: Msg_def quotient_def intro: msgrel_refl)
```
```   161
```
```   162 lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
```
```   163 apply (rule inj_on_inverseI)
```
```   164 apply (erule Abs_Msg_inverse)
```
```   165 done
```
```   166
```
```   167 text{*Reduces equality on abstractions to equality on representatives*}
```
```   168 declare inj_on_Abs_Msg [THEN inj_on_iff, simp]
```
```   169
```
```   170 declare Abs_Msg_inverse [simp]
```
```   171
```
```   172
```
```   173 subsubsection{*Characteristic Equations for the Abstract Constructors*}
```
```   174
```
```   175 lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) =
```
```   176               Abs_Msg (msgrel``{MPAIR U V})"
```
```   177 proof -
```
```   178   have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
```
```   179     by (auto simp add: congruent2_def msgrel.MPAIR)
```
```   180   thus ?thesis
```
```   181     by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
```
```   182 qed
```
```   183
```
```   184 lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
```
```   185 proof -
```
```   186   have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
```
```   187     by (auto simp add: congruent_def msgrel.CRYPT)
```
```   188   thus ?thesis
```
```   189     by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
```
```   190 qed
```
```   191
```
```   192 lemma Decrypt:
```
```   193      "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
```
```   194 proof -
```
```   195   have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
```
```   196     by (auto simp add: congruent_def msgrel.DECRYPT)
```
```   197   thus ?thesis
```
```   198     by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
```
```   199 qed
```
```   200
```
```   201 text{*Case analysis on the representation of a msg as an equivalence class.*}
```
```   202 lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]:
```
```   203      "(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P"
```
```   204 apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE])
```
```   205 apply (drule arg_cong [where f=Abs_Msg])
```
```   206 apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl)
```
```   207 done
```
```   208
```
```   209 text{*Establishing these two equations is the point of the whole exercise*}
```
```   210 theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
```
```   211 by (cases X, simp add: Crypt Decrypt CD)
```
```   212
```
```   213 theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
```
```   214 by (cases X, simp add: Crypt Decrypt DC)
```
```   215
```
```   216
```
```   217 subsection{*The Abstract Function to Return the Set of Nonces*}
```
```   218
```
```   219 definition
```
```   220   nonces :: "msg \<Rightarrow> nat set" where
```
```   221    "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
```
```   222
```
```   223 lemma nonces_congruent: "freenonces respects msgrel"
```
```   224 by (auto simp add: congruent_def msgrel_imp_eq_freenonces)
```
```   225
```
```   226
```
```   227 text{*Now prove the four equations for @{term nonces}*}
```
```   228
```
```   229 lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}"
```
```   230 by (simp add: nonces_def Nonce_def
```
```   231               UN_equiv_class [OF equiv_msgrel nonces_congruent])
```
```   232
```
```   233 lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X \<union> nonces Y"
```
```   234 apply (cases X, cases Y)
```
```   235 apply (simp add: nonces_def MPair
```
```   236                  UN_equiv_class [OF equiv_msgrel nonces_congruent])
```
```   237 done
```
```   238
```
```   239 lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X"
```
```   240 apply (cases X)
```
```   241 apply (simp add: nonces_def Crypt
```
```   242                  UN_equiv_class [OF equiv_msgrel nonces_congruent])
```
```   243 done
```
```   244
```
```   245 lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
```
```   246 apply (cases X)
```
```   247 apply (simp add: nonces_def Decrypt
```
```   248                  UN_equiv_class [OF equiv_msgrel nonces_congruent])
```
```   249 done
```
```   250
```
```   251
```
```   252 subsection{*The Abstract Function to Return the Left Part*}
```
```   253
```
```   254 definition
```
```   255   left :: "msg \<Rightarrow> msg" where
```
```   256    "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
```
```   257
```
```   258 lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
```
```   259 by (auto simp add: congruent_def msgrel_imp_eqv_freeleft)
```
```   260
```
```   261 text{*Now prove the four equations for @{term left}*}
```
```   262
```
```   263 lemma left_Nonce [simp]: "left (Nonce N) = Nonce N"
```
```   264 by (simp add: left_def Nonce_def
```
```   265               UN_equiv_class [OF equiv_msgrel left_congruent])
```
```   266
```
```   267 lemma left_MPair [simp]: "left (MPair X Y) = X"
```
```   268 apply (cases X, cases Y)
```
```   269 apply (simp add: left_def MPair
```
```   270                  UN_equiv_class [OF equiv_msgrel left_congruent])
```
```   271 done
```
```   272
```
```   273 lemma left_Crypt [simp]: "left (Crypt K X) = left X"
```
```   274 apply (cases X)
```
```   275 apply (simp add: left_def Crypt
```
```   276                  UN_equiv_class [OF equiv_msgrel left_congruent])
```
```   277 done
```
```   278
```
```   279 lemma left_Decrypt [simp]: "left (Decrypt K X) = left X"
```
```   280 apply (cases X)
```
```   281 apply (simp add: left_def Decrypt
```
```   282                  UN_equiv_class [OF equiv_msgrel left_congruent])
```
```   283 done
```
```   284
```
```   285
```
```   286 subsection{*The Abstract Function to Return the Right Part*}
```
```   287
```
```   288 definition
```
```   289   right :: "msg \<Rightarrow> msg" where
```
```   290    "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
```
```   291
```
```   292 lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
```
```   293 by (auto simp add: congruent_def msgrel_imp_eqv_freeright)
```
```   294
```
```   295 text{*Now prove the four equations for @{term right}*}
```
```   296
```
```   297 lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"
```
```   298 by (simp add: right_def Nonce_def
```
```   299               UN_equiv_class [OF equiv_msgrel right_congruent])
```
```   300
```
```   301 lemma right_MPair [simp]: "right (MPair X Y) = Y"
```
```   302 apply (cases X, cases Y)
```
```   303 apply (simp add: right_def MPair
```
```   304                  UN_equiv_class [OF equiv_msgrel right_congruent])
```
```   305 done
```
```   306
```
```   307 lemma right_Crypt [simp]: "right (Crypt K X) = right X"
```
```   308 apply (cases X)
```
```   309 apply (simp add: right_def Crypt
```
```   310                  UN_equiv_class [OF equiv_msgrel right_congruent])
```
```   311 done
```
```   312
```
```   313 lemma right_Decrypt [simp]: "right (Decrypt K X) = right X"
```
```   314 apply (cases X)
```
```   315 apply (simp add: right_def Decrypt
```
```   316                  UN_equiv_class [OF equiv_msgrel right_congruent])
```
```   317 done
```
```   318
```
```   319
```
```   320 subsection{*Injectivity Properties of Some Constructors*}
```
```   321
```
```   322 lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
```
```   323 by (drule msgrel_imp_eq_freenonces, simp)
```
```   324
```
```   325 text{*Can also be proved using the function @{term nonces}*}
```
```   326 lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"
```
```   327 by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)
```
```   328
```
```   329 lemma MPAIR_imp_eqv_left: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
```
```   330 by (drule msgrel_imp_eqv_freeleft, simp)
```
```   331
```
```   332 lemma MPair_imp_eq_left:
```
```   333   assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'"
```
```   334 proof -
```
```   335   from eq
```
```   336   have "left (MPair X Y) = left (MPair X' Y')" by simp
```
```   337   thus ?thesis by simp
```
```   338 qed
```
```   339
```
```   340 lemma MPAIR_imp_eqv_right: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
```
```   341 by (drule msgrel_imp_eqv_freeright, simp)
```
```   342
```
```   343 lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
```
```   344 apply (cases X, cases X', cases Y, cases Y')
```
```   345 apply (simp add: MPair)
```
```   346 apply (erule MPAIR_imp_eqv_right)
```
```   347 done
```
```   348
```
```   349 theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
```
```   350 by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
```
```   351
```
```   352 lemma NONCE_neqv_MPAIR: "NONCE m \<sim> MPAIR X Y \<Longrightarrow> False"
```
```   353 by (drule msgrel_imp_eq_freediscrim, simp)
```
```   354
```
```   355 theorem Nonce_neq_MPair [iff]: "Nonce N \<noteq> MPair X Y"
```
```   356 apply (cases X, cases Y)
```
```   357 apply (simp add: Nonce_def MPair)
```
```   358 apply (blast dest: NONCE_neqv_MPAIR)
```
```   359 done
```
```   360
```
```   361 text{*Example suggested by a referee*}
```
```   362 theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) \<noteq> Nonce N"
```
```   363 by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)
```
```   364
```
```   365 text{*...and many similar results*}
```
```   366 theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
```
```   367 by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)
```
```   368
```
```   369 theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')"
```
```   370 proof
```
```   371   assume "Crypt K X = Crypt K X'"
```
```   372   hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
```
```   373   thus "X = X'" by simp
```
```   374 next
```
```   375   assume "X = X'"
```
```   376   thus "Crypt K X = Crypt K X'" by simp
```
```   377 qed
```
```   378
```
```   379 theorem Decrypt_Decrypt_eq [iff]: "(Decrypt K X = Decrypt K X') = (X=X')"
```
```   380 proof
```
```   381   assume "Decrypt K X = Decrypt K X'"
```
```   382   hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
```
```   383   thus "X = X'" by simp
```
```   384 next
```
```   385   assume "X = X'"
```
```   386   thus "Decrypt K X = Decrypt K X'" by simp
```
```   387 qed
```
```   388
```
```   389 lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
```
```   390   assumes N: "\<And>N. P (Nonce N)"
```
```   391       and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
```
```   392       and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
```
```   393       and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
```
```   394   shows "P msg"
```
```   395 proof (cases msg)
```
```   396   case (Abs_Msg U)
```
```   397   have "P (Abs_Msg (msgrel `` {U}))"
```
```   398   proof (induct U)
```
```   399     case (NONCE N)
```
```   400     with N show ?case by (simp add: Nonce_def)
```
```   401   next
```
```   402     case (MPAIR X Y)
```
```   403     with M [of "Abs_Msg (msgrel `` {X})" "Abs_Msg (msgrel `` {Y})"]
```
```   404     show ?case by (simp add: MPair)
```
```   405   next
```
```   406     case (CRYPT K X)
```
```   407     with C [of "Abs_Msg (msgrel `` {X})"]
```
```   408     show ?case by (simp add: Crypt)
```
```   409   next
```
```   410     case (DECRYPT K X)
```
```   411     with D [of "Abs_Msg (msgrel `` {X})"]
```
```   412     show ?case by (simp add: Decrypt)
```
```   413   qed
```
```   414   with Abs_Msg show ?thesis by (simp only:)
```
```   415 qed
```
```   416
```
```   417
```
```   418 subsection{*The Abstract Discriminator*}
```
```   419
```
```   420 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
```
```   421 need this function in order to prove discrimination theorems.*}
```
```   422
```
```   423 definition
```
```   424   discrim :: "msg \<Rightarrow> int" where
```
```   425    "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
```
```   426
```
```   427 lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
```
```   428 by (auto simp add: congruent_def msgrel_imp_eq_freediscrim)
```
```   429
```
```   430 text{*Now prove the four equations for @{term discrim}*}
```
```   431
```
```   432 lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0"
```
```   433 by (simp add: discrim_def Nonce_def
```
```   434               UN_equiv_class [OF equiv_msgrel discrim_congruent])
```
```   435
```
```   436 lemma discrim_MPair [simp]: "discrim (MPair X Y) = 1"
```
```   437 apply (cases X, cases Y)
```
```   438 apply (simp add: discrim_def MPair
```
```   439                  UN_equiv_class [OF equiv_msgrel discrim_congruent])
```
```   440 done
```
```   441
```
```   442 lemma discrim_Crypt [simp]: "discrim (Crypt K X) = discrim X + 2"
```
```   443 apply (cases X)
```
```   444 apply (simp add: discrim_def Crypt
```
```   445                  UN_equiv_class [OF equiv_msgrel discrim_congruent])
```
```   446 done
```
```   447
```
```   448 lemma discrim_Decrypt [simp]: "discrim (Decrypt K X) = discrim X - 2"
```
```   449 apply (cases X)
```
```   450 apply (simp add: discrim_def Decrypt
```
```   451                  UN_equiv_class [OF equiv_msgrel discrim_congruent])
```
```   452 done
```
```   453
```
```   454
```
```   455 end
```
```   456
```