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