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