src/HOL/Induct/QuoDataType.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 58310 91ea607a34d8 child 59478 1755b24e8b44 permissions -rw-r--r--
```     1 (*  Title:      HOL/Induct/QuoDataType.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   2004  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 section{*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 definition "Msg = UNIV//msgrel"
```
```   127
```
```   128 typedef msg = Msg
```
```   129   morphisms Rep_Msg Abs_Msg
```
```   130   unfolding Msg_def by (auto simp add: quotient_def)
```
```   131
```
```   132
```
```   133 text{*The abstract message constructors*}
```
```   134 definition
```
```   135   Nonce :: "nat \<Rightarrow> msg" where
```
```   136   "Nonce N = Abs_Msg(msgrel``{NONCE N})"
```
```   137
```
```   138 definition
```
```   139   MPair :: "[msg,msg] \<Rightarrow> msg" where
```
```   140    "MPair X Y =
```
```   141        Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
```
```   142
```
```   143 definition
```
```   144   Crypt :: "[nat,msg] \<Rightarrow> msg" where
```
```   145    "Crypt K X =
```
```   146        Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
```
```   147
```
```   148 definition
```
```   149   Decrypt :: "[nat,msg] \<Rightarrow> msg" where
```
```   150    "Decrypt K X =
```
```   151        Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
```
```   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*}
```
```   162 lemma [simp]: "msgrel``{U} \<in> Msg"
```
```   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 -
```
```   181   have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
```
```   182     by (auto simp add: congruent2_def msgrel.MPAIR)
```
```   183   thus ?thesis
```
```   184     by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
```
```   185 qed
```
```   186
```
```   187 lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
```
```   188 proof -
```
```   189   have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
```
```   190     by (auto simp add: congruent_def msgrel.CRYPT)
```
```   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 -
```
```   198   have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
```
```   199     by (auto simp add: congruent_def msgrel.DECRYPT)
```
```   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*}
```
```   213 theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
```
```   214 by (cases X, simp add: Crypt Decrypt CD)
```
```   215
```
```   216 theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
```
```   217 by (cases X, simp add: Crypt Decrypt DC)
```
```   218
```
```   219
```
```   220 subsection{*The Abstract Function to Return the Set of Nonces*}
```
```   221
```
```   222 definition
```
```   223   nonces :: "msg \<Rightarrow> nat set" where
```
```   224    "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
```
```   225
```
```   226 lemma nonces_congruent: "freenonces respects msgrel"
```
```   227 by (auto simp add: congruent_def msgrel_imp_eq_freenonces)
```
```   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
```
```   257 definition
```
```   258   left :: "msg \<Rightarrow> msg" where
```
```   259    "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
```
```   260
```
```   261 lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
```
```   262 by (auto simp add: congruent_def msgrel_imp_eqv_freeleft)
```
```   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
```
```   291 definition
```
```   292   right :: "msg \<Rightarrow> msg" where
```
```   293    "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
```
```   294
```
```   295 lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
```
```   296 by (auto simp add: congruent_def msgrel_imp_eqv_freeright)
```
```   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'"
```
```   333 by (drule msgrel_imp_eqv_freeleft, simp)
```
```   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'"
```
```   344 by (drule msgrel_imp_eqv_freeright, simp)
```
```   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')"
```
```   353 by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
```
```   354
```
```   355 lemma NONCE_neqv_MPAIR: "NONCE m \<sim> MPAIR X Y \<Longrightarrow> False"
```
```   356 by (drule msgrel_imp_eq_freediscrim, simp)
```
```   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
```
```   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*}
```
```   369 theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
```
```   370 by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)
```
```   371
```
```   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"
```
```   398 proof (cases msg)
```
```   399   case (Abs_Msg U)
```
```   400   have "P (Abs_Msg (msgrel `` {U}))"
```
```   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
```
```   417   with Abs_Msg show ?thesis by (simp only:)
```
```   418 qed
```
```   419
```
```   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
```
```   426 definition
```
```   427   discrim :: "msg \<Rightarrow> int" where
```
```   428    "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
```
```   429
```
```   430 lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
```
```   431 by (auto simp add: congruent_def msgrel_imp_eq_freediscrim)
```
```   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
```
```   458 end
```
```   459
```