src/HOL/Quotient_Examples/Quotient_Message.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Thu Apr 29 09:06:35 2010 +0200 (2010-04-29)
changeset 36524 3909002beca5
parent 35222 src/HOL/Quotient_Examples/LarryDatatype.thy@4f1fba00f66d
child 37594 32ad67684ee7
permissions -rw-r--r--
Tuning the quotient examples
kaliszyk@36524
     1
(*  Title:      HOL/Quotient_Examples/Quotient_Message.thy
kaliszyk@36524
     2
    Author:     Christian Urban
kaliszyk@36524
     3
kaliszyk@36524
     4
Message datatype, based on an older version by Larry Paulson.
kaliszyk@36524
     5
*)
kaliszyk@36524
     6
theory Quotient_Message
kaliszyk@35222
     7
imports Main Quotient_Syntax
kaliszyk@35222
     8
begin
kaliszyk@35222
     9
kaliszyk@35222
    10
subsection{*Defining the Free Algebra*}
kaliszyk@35222
    11
kaliszyk@35222
    12
datatype
kaliszyk@35222
    13
  freemsg = NONCE  nat
kaliszyk@35222
    14
        | MPAIR  freemsg freemsg
kaliszyk@36524
    15
        | CRYPT  nat freemsg
kaliszyk@35222
    16
        | DECRYPT  nat freemsg
kaliszyk@35222
    17
kaliszyk@36524
    18
inductive
kaliszyk@35222
    19
  msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
kaliszyk@36524
    20
where
kaliszyk@35222
    21
  CD:    "CRYPT K (DECRYPT K X) \<sim> X"
kaliszyk@35222
    22
| DC:    "DECRYPT K (CRYPT K X) \<sim> X"
kaliszyk@35222
    23
| NONCE: "NONCE N \<sim> NONCE N"
kaliszyk@35222
    24
| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
kaliszyk@35222
    25
| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
kaliszyk@35222
    26
| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
kaliszyk@35222
    27
| SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
kaliszyk@35222
    28
| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
kaliszyk@35222
    29
kaliszyk@35222
    30
lemmas msgrel.intros[intro]
kaliszyk@35222
    31
kaliszyk@35222
    32
text{*Proving that it is an equivalence relation*}
kaliszyk@35222
    33
kaliszyk@35222
    34
lemma msgrel_refl: "X \<sim> X"
kaliszyk@35222
    35
by (induct X, (blast intro: msgrel.intros)+)
kaliszyk@35222
    36
kaliszyk@35222
    37
theorem equiv_msgrel: "equivp msgrel"
kaliszyk@35222
    38
proof (rule equivpI)
kaliszyk@35222
    39
  show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
kaliszyk@35222
    40
  show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
kaliszyk@35222
    41
  show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
kaliszyk@35222
    42
qed
kaliszyk@35222
    43
kaliszyk@35222
    44
subsection{*Some Functions on the Free Algebra*}
kaliszyk@35222
    45
kaliszyk@35222
    46
subsubsection{*The Set of Nonces*}
kaliszyk@35222
    47
kaliszyk@35222
    48
fun
kaliszyk@35222
    49
  freenonces :: "freemsg \<Rightarrow> nat set"
kaliszyk@35222
    50
where
kaliszyk@35222
    51
  "freenonces (NONCE N) = {N}"
kaliszyk@35222
    52
| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
kaliszyk@35222
    53
| "freenonces (CRYPT K X) = freenonces X"
kaliszyk@35222
    54
| "freenonces (DECRYPT K X) = freenonces X"
kaliszyk@35222
    55
kaliszyk@36524
    56
theorem msgrel_imp_eq_freenonces:
kaliszyk@35222
    57
  assumes a: "U \<sim> V"
kaliszyk@35222
    58
  shows "freenonces U = freenonces V"
kaliszyk@36524
    59
  using a by (induct) (auto)
kaliszyk@35222
    60
kaliszyk@35222
    61
subsubsection{*The Left Projection*}
kaliszyk@35222
    62
kaliszyk@35222
    63
text{*A function to return the left part of the top pair in a message.  It will
kaliszyk@35222
    64
be lifted to the initial algrebra, to serve as an example of that process.*}
kaliszyk@35222
    65
fun
kaliszyk@35222
    66
  freeleft :: "freemsg \<Rightarrow> freemsg"
kaliszyk@35222
    67
where
kaliszyk@35222
    68
  "freeleft (NONCE N) = NONCE N"
kaliszyk@35222
    69
| "freeleft (MPAIR X Y) = X"
kaliszyk@35222
    70
| "freeleft (CRYPT K X) = freeleft X"
kaliszyk@35222
    71
| "freeleft (DECRYPT K X) = freeleft X"
kaliszyk@35222
    72
kaliszyk@35222
    73
text{*This theorem lets us prove that the left function respects the
kaliszyk@35222
    74
equivalence relation.  It also helps us prove that MPair
kaliszyk@35222
    75
  (the abstract constructor) is injective*}
kaliszyk@35222
    76
lemma msgrel_imp_eqv_freeleft_aux:
kaliszyk@35222
    77
  shows "freeleft U \<sim> freeleft U"
kaliszyk@35222
    78
  by (induct rule: freeleft.induct) (auto)
kaliszyk@35222
    79
kaliszyk@35222
    80
theorem msgrel_imp_eqv_freeleft:
kaliszyk@36524
    81
  assumes a: "U \<sim> V"
kaliszyk@35222
    82
  shows "freeleft U \<sim> freeleft V"
kaliszyk@35222
    83
  using a
kaliszyk@35222
    84
  by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
kaliszyk@35222
    85
kaliszyk@35222
    86
subsubsection{*The Right Projection*}
kaliszyk@35222
    87
kaliszyk@35222
    88
text{*A function to return the right part of the top pair in a message.*}
kaliszyk@35222
    89
fun
kaliszyk@35222
    90
  freeright :: "freemsg \<Rightarrow> freemsg"
kaliszyk@35222
    91
where
kaliszyk@35222
    92
  "freeright (NONCE N) = NONCE N"
kaliszyk@35222
    93
| "freeright (MPAIR X Y) = Y"
kaliszyk@35222
    94
| "freeright (CRYPT K X) = freeright X"
kaliszyk@35222
    95
| "freeright (DECRYPT K X) = freeright X"
kaliszyk@35222
    96
kaliszyk@35222
    97
text{*This theorem lets us prove that the right function respects the
kaliszyk@35222
    98
equivalence relation.  It also helps us prove that MPair
kaliszyk@35222
    99
  (the abstract constructor) is injective*}
kaliszyk@35222
   100
lemma msgrel_imp_eqv_freeright_aux:
kaliszyk@35222
   101
  shows "freeright U \<sim> freeright U"
kaliszyk@35222
   102
  by (induct rule: freeright.induct) (auto)
kaliszyk@35222
   103
kaliszyk@35222
   104
theorem msgrel_imp_eqv_freeright:
kaliszyk@36524
   105
  assumes a: "U \<sim> V"
kaliszyk@35222
   106
  shows "freeright U \<sim> freeright V"
kaliszyk@35222
   107
  using a
kaliszyk@35222
   108
  by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
kaliszyk@35222
   109
kaliszyk@35222
   110
subsubsection{*The Discriminator for Constructors*}
kaliszyk@35222
   111
kaliszyk@35222
   112
text{*A function to distinguish nonces, mpairs and encryptions*}
kaliszyk@36524
   113
fun
kaliszyk@35222
   114
  freediscrim :: "freemsg \<Rightarrow> int"
kaliszyk@35222
   115
where
kaliszyk@35222
   116
   "freediscrim (NONCE N) = 0"
kaliszyk@35222
   117
 | "freediscrim (MPAIR X Y) = 1"
kaliszyk@35222
   118
 | "freediscrim (CRYPT K X) = freediscrim X + 2"
kaliszyk@35222
   119
 | "freediscrim (DECRYPT K X) = freediscrim X - 2"
kaliszyk@35222
   120
kaliszyk@35222
   121
text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
kaliszyk@35222
   122
theorem msgrel_imp_eq_freediscrim:
kaliszyk@35222
   123
  assumes a: "U \<sim> V"
kaliszyk@35222
   124
  shows "freediscrim U = freediscrim V"
kaliszyk@35222
   125
  using a by (induct) (auto)
kaliszyk@35222
   126
kaliszyk@35222
   127
subsection{*The Initial Algebra: A Quotiented Message Type*}
kaliszyk@35222
   128
kaliszyk@35222
   129
quotient_type msg = freemsg / msgrel
kaliszyk@35222
   130
  by (rule equiv_msgrel)
kaliszyk@35222
   131
kaliszyk@35222
   132
text{*The abstract message constructors*}
kaliszyk@35222
   133
kaliszyk@35222
   134
quotient_definition
kaliszyk@35222
   135
  "Nonce :: nat \<Rightarrow> msg"
kaliszyk@35222
   136
is
kaliszyk@35222
   137
  "NONCE"
kaliszyk@35222
   138
kaliszyk@35222
   139
quotient_definition
kaliszyk@35222
   140
  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
kaliszyk@35222
   141
is
kaliszyk@35222
   142
  "MPAIR"
kaliszyk@35222
   143
kaliszyk@35222
   144
quotient_definition
kaliszyk@35222
   145
  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
kaliszyk@35222
   146
is
kaliszyk@35222
   147
  "CRYPT"
kaliszyk@35222
   148
kaliszyk@35222
   149
quotient_definition
kaliszyk@35222
   150
  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
kaliszyk@35222
   151
is
kaliszyk@35222
   152
  "DECRYPT"
kaliszyk@35222
   153
kaliszyk@35222
   154
lemma [quot_respect]:
kaliszyk@35222
   155
  shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
kaliszyk@35222
   156
by (auto intro: CRYPT)
kaliszyk@35222
   157
kaliszyk@35222
   158
lemma [quot_respect]:
kaliszyk@35222
   159
  shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
kaliszyk@35222
   160
by (auto intro: DECRYPT)
kaliszyk@35222
   161
kaliszyk@35222
   162
text{*Establishing these two equations is the point of the whole exercise*}
kaliszyk@36524
   163
theorem CD_eq [simp]:
kaliszyk@35222
   164
  shows "Crypt K (Decrypt K X) = X"
kaliszyk@35222
   165
  by (lifting CD)
kaliszyk@35222
   166
kaliszyk@36524
   167
theorem DC_eq [simp]:
kaliszyk@35222
   168
  shows "Decrypt K (Crypt K X) = X"
kaliszyk@35222
   169
  by (lifting DC)
kaliszyk@35222
   170
kaliszyk@35222
   171
subsection{*The Abstract Function to Return the Set of Nonces*}
kaliszyk@35222
   172
kaliszyk@35222
   173
quotient_definition
kaliszyk@35222
   174
   "nonces:: msg \<Rightarrow> nat set"
kaliszyk@35222
   175
is
kaliszyk@35222
   176
  "freenonces"
kaliszyk@35222
   177
kaliszyk@35222
   178
text{*Now prove the four equations for @{term nonces}*}
kaliszyk@35222
   179
kaliszyk@35222
   180
lemma [quot_respect]:
kaliszyk@35222
   181
  shows "(op \<sim> ===> op =) freenonces freenonces"
kaliszyk@35222
   182
  by (simp add: msgrel_imp_eq_freenonces)
kaliszyk@35222
   183
kaliszyk@35222
   184
lemma [quot_respect]:
kaliszyk@35222
   185
  shows "(op = ===> op \<sim>) NONCE NONCE"
kaliszyk@35222
   186
  by (simp add: NONCE)
kaliszyk@35222
   187
kaliszyk@36524
   188
lemma nonces_Nonce [simp]:
kaliszyk@35222
   189
  shows "nonces (Nonce N) = {N}"
kaliszyk@35222
   190
  by (lifting freenonces.simps(1))
kaliszyk@36524
   191
kaliszyk@35222
   192
lemma [quot_respect]:
kaliszyk@35222
   193
  shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
kaliszyk@35222
   194
  by (simp add: MPAIR)
kaliszyk@35222
   195
kaliszyk@36524
   196
lemma nonces_MPair [simp]:
kaliszyk@35222
   197
  shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
kaliszyk@35222
   198
  by (lifting freenonces.simps(2))
kaliszyk@35222
   199
kaliszyk@36524
   200
lemma nonces_Crypt [simp]:
kaliszyk@35222
   201
  shows "nonces (Crypt K X) = nonces X"
kaliszyk@35222
   202
  by (lifting freenonces.simps(3))
kaliszyk@35222
   203
kaliszyk@36524
   204
lemma nonces_Decrypt [simp]:
kaliszyk@35222
   205
  shows "nonces (Decrypt K X) = nonces X"
kaliszyk@35222
   206
  by (lifting freenonces.simps(4))
kaliszyk@35222
   207
kaliszyk@35222
   208
subsection{*The Abstract Function to Return the Left Part*}
kaliszyk@35222
   209
kaliszyk@35222
   210
quotient_definition
kaliszyk@35222
   211
  "left:: msg \<Rightarrow> msg"
kaliszyk@35222
   212
is
kaliszyk@35222
   213
  "freeleft"
kaliszyk@35222
   214
kaliszyk@35222
   215
lemma [quot_respect]:
kaliszyk@35222
   216
  shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
kaliszyk@35222
   217
  by (simp add: msgrel_imp_eqv_freeleft)
kaliszyk@35222
   218
kaliszyk@36524
   219
lemma left_Nonce [simp]:
kaliszyk@35222
   220
  shows "left (Nonce N) = Nonce N"
kaliszyk@35222
   221
  by (lifting freeleft.simps(1))
kaliszyk@35222
   222
kaliszyk@36524
   223
lemma left_MPair [simp]:
kaliszyk@35222
   224
  shows "left (MPair X Y) = X"
kaliszyk@35222
   225
  by (lifting freeleft.simps(2))
kaliszyk@35222
   226
kaliszyk@36524
   227
lemma left_Crypt [simp]:
kaliszyk@35222
   228
  shows "left (Crypt K X) = left X"
kaliszyk@35222
   229
  by (lifting freeleft.simps(3))
kaliszyk@35222
   230
kaliszyk@36524
   231
lemma left_Decrypt [simp]:
kaliszyk@35222
   232
  shows "left (Decrypt K X) = left X"
kaliszyk@35222
   233
  by (lifting freeleft.simps(4))
kaliszyk@35222
   234
kaliszyk@35222
   235
subsection{*The Abstract Function to Return the Right Part*}
kaliszyk@35222
   236
kaliszyk@35222
   237
quotient_definition
kaliszyk@35222
   238
  "right:: msg \<Rightarrow> msg"
kaliszyk@35222
   239
is
kaliszyk@35222
   240
  "freeright"
kaliszyk@35222
   241
kaliszyk@35222
   242
text{*Now prove the four equations for @{term right}*}
kaliszyk@35222
   243
kaliszyk@35222
   244
lemma [quot_respect]:
kaliszyk@35222
   245
  shows "(op \<sim> ===> op \<sim>) freeright freeright"
kaliszyk@35222
   246
  by (simp add: msgrel_imp_eqv_freeright)
kaliszyk@35222
   247
kaliszyk@36524
   248
lemma right_Nonce [simp]:
kaliszyk@35222
   249
  shows "right (Nonce N) = Nonce N"
kaliszyk@35222
   250
  by (lifting freeright.simps(1))
kaliszyk@35222
   251
kaliszyk@36524
   252
lemma right_MPair [simp]:
kaliszyk@35222
   253
  shows "right (MPair X Y) = Y"
kaliszyk@35222
   254
  by (lifting freeright.simps(2))
kaliszyk@35222
   255
kaliszyk@36524
   256
lemma right_Crypt [simp]:
kaliszyk@35222
   257
  shows "right (Crypt K X) = right X"
kaliszyk@35222
   258
  by (lifting freeright.simps(3))
kaliszyk@35222
   259
kaliszyk@36524
   260
lemma right_Decrypt [simp]:
kaliszyk@35222
   261
  shows "right (Decrypt K X) = right X"
kaliszyk@35222
   262
  by (lifting freeright.simps(4))
kaliszyk@35222
   263
kaliszyk@35222
   264
subsection{*Injectivity Properties of Some Constructors*}
kaliszyk@35222
   265
kaliszyk@36524
   266
lemma NONCE_imp_eq:
kaliszyk@35222
   267
  shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
kaliszyk@35222
   268
  by (drule msgrel_imp_eq_freenonces, simp)
kaliszyk@35222
   269
kaliszyk@35222
   270
text{*Can also be proved using the function @{term nonces}*}
kaliszyk@36524
   271
lemma Nonce_Nonce_eq [iff]:
kaliszyk@35222
   272
  shows "(Nonce m = Nonce n) = (m = n)"
kaliszyk@35222
   273
proof
kaliszyk@35222
   274
  assume "Nonce m = Nonce n"
kaliszyk@35222
   275
  then show "m = n" by (lifting NONCE_imp_eq)
kaliszyk@35222
   276
next
kaliszyk@36524
   277
  assume "m = n"
kaliszyk@35222
   278
  then show "Nonce m = Nonce n" by simp
kaliszyk@35222
   279
qed
kaliszyk@35222
   280
kaliszyk@36524
   281
lemma MPAIR_imp_eqv_left:
kaliszyk@35222
   282
  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
kaliszyk@35222
   283
  by (drule msgrel_imp_eqv_freeleft) (simp)
kaliszyk@35222
   284
kaliszyk@36524
   285
lemma MPair_imp_eq_left:
kaliszyk@36524
   286
  assumes eq: "MPair X Y = MPair X' Y'"
kaliszyk@35222
   287
  shows "X = X'"
kaliszyk@35222
   288
  using eq by (lifting MPAIR_imp_eqv_left)
kaliszyk@35222
   289
kaliszyk@36524
   290
lemma MPAIR_imp_eqv_right:
kaliszyk@35222
   291
  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
kaliszyk@35222
   292
  by (drule msgrel_imp_eqv_freeright) (simp)
kaliszyk@35222
   293
kaliszyk@36524
   294
lemma MPair_imp_eq_right:
kaliszyk@35222
   295
  shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
kaliszyk@35222
   296
  by (lifting  MPAIR_imp_eqv_right)
kaliszyk@35222
   297
kaliszyk@36524
   298
theorem MPair_MPair_eq [iff]:
kaliszyk@36524
   299
  shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
kaliszyk@35222
   300
  by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
kaliszyk@35222
   301
kaliszyk@36524
   302
lemma NONCE_neqv_MPAIR:
kaliszyk@35222
   303
  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
kaliszyk@35222
   304
  by (auto dest: msgrel_imp_eq_freediscrim)
kaliszyk@35222
   305
kaliszyk@36524
   306
theorem Nonce_neq_MPair [iff]:
kaliszyk@35222
   307
  shows "Nonce N \<noteq> MPair X Y"
kaliszyk@35222
   308
  by (lifting NONCE_neqv_MPAIR)
kaliszyk@35222
   309
kaliszyk@35222
   310
text{*Example suggested by a referee*}
kaliszyk@35222
   311
kaliszyk@35222
   312
lemma CRYPT_NONCE_neq_NONCE:
kaliszyk@35222
   313
  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
kaliszyk@35222
   314
  by (auto dest: msgrel_imp_eq_freediscrim)
kaliszyk@35222
   315
kaliszyk@36524
   316
theorem Crypt_Nonce_neq_Nonce:
kaliszyk@35222
   317
  shows "Crypt K (Nonce M) \<noteq> Nonce N"
kaliszyk@35222
   318
  by (lifting CRYPT_NONCE_neq_NONCE)
kaliszyk@35222
   319
kaliszyk@35222
   320
text{*...and many similar results*}
kaliszyk@36524
   321
lemma CRYPT2_NONCE_neq_NONCE:
kaliszyk@35222
   322
  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
kaliszyk@36524
   323
  by (auto dest: msgrel_imp_eq_freediscrim)
kaliszyk@35222
   324
kaliszyk@36524
   325
theorem Crypt2_Nonce_neq_Nonce:
kaliszyk@35222
   326
  shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
kaliszyk@36524
   327
  by (lifting CRYPT2_NONCE_neq_NONCE)
kaliszyk@35222
   328
kaliszyk@36524
   329
theorem Crypt_Crypt_eq [iff]:
kaliszyk@36524
   330
  shows "(Crypt K X = Crypt K X') = (X=X')"
kaliszyk@35222
   331
proof
kaliszyk@35222
   332
  assume "Crypt K X = Crypt K X'"
kaliszyk@35222
   333
  hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
kaliszyk@35222
   334
  thus "X = X'" by simp
kaliszyk@35222
   335
next
kaliszyk@35222
   336
  assume "X = X'"
kaliszyk@35222
   337
  thus "Crypt K X = Crypt K X'" by simp
kaliszyk@35222
   338
qed
kaliszyk@35222
   339
kaliszyk@36524
   340
theorem Decrypt_Decrypt_eq [iff]:
kaliszyk@36524
   341
  shows "(Decrypt K X = Decrypt K X') = (X=X')"
kaliszyk@35222
   342
proof
kaliszyk@35222
   343
  assume "Decrypt K X = Decrypt K X'"
kaliszyk@35222
   344
  hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
kaliszyk@35222
   345
  thus "X = X'" by simp
kaliszyk@35222
   346
next
kaliszyk@35222
   347
  assume "X = X'"
kaliszyk@35222
   348
  thus "Decrypt K X = Decrypt K X'" by simp
kaliszyk@35222
   349
qed
kaliszyk@35222
   350
kaliszyk@35222
   351
lemma msg_induct_aux:
kaliszyk@35222
   352
  shows "\<lbrakk>\<And>N. P (Nonce N);
kaliszyk@35222
   353
          \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
kaliszyk@35222
   354
          \<And>K X. P X \<Longrightarrow> P (Crypt K X);
kaliszyk@35222
   355
          \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
kaliszyk@35222
   356
  by (lifting freemsg.induct)
kaliszyk@35222
   357
kaliszyk@35222
   358
lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
kaliszyk@35222
   359
  assumes N: "\<And>N. P (Nonce N)"
kaliszyk@35222
   360
      and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
kaliszyk@35222
   361
      and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
kaliszyk@35222
   362
      and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
kaliszyk@35222
   363
  shows "P msg"
kaliszyk@35222
   364
  using N M C D by (rule msg_induct_aux)
kaliszyk@35222
   365
kaliszyk@35222
   366
subsection{*The Abstract Discriminator*}
kaliszyk@35222
   367
kaliszyk@35222
   368
text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
kaliszyk@35222
   369
need this function in order to prove discrimination theorems.*}
kaliszyk@35222
   370
kaliszyk@35222
   371
quotient_definition
kaliszyk@35222
   372
  "discrim:: msg \<Rightarrow> int"
kaliszyk@35222
   373
is
kaliszyk@35222
   374
  "freediscrim"
kaliszyk@35222
   375
kaliszyk@35222
   376
text{*Now prove the four equations for @{term discrim}*}
kaliszyk@35222
   377
kaliszyk@35222
   378
lemma [quot_respect]:
kaliszyk@35222
   379
  shows "(op \<sim> ===> op =) freediscrim freediscrim"
kaliszyk@35222
   380
  by (auto simp add: msgrel_imp_eq_freediscrim)
kaliszyk@35222
   381
kaliszyk@36524
   382
lemma discrim_Nonce [simp]:
kaliszyk@35222
   383
  shows "discrim (Nonce N) = 0"
kaliszyk@35222
   384
  by (lifting freediscrim.simps(1))
kaliszyk@35222
   385
kaliszyk@36524
   386
lemma discrim_MPair [simp]:
kaliszyk@35222
   387
  shows "discrim (MPair X Y) = 1"
kaliszyk@35222
   388
  by (lifting freediscrim.simps(2))
kaliszyk@35222
   389
kaliszyk@36524
   390
lemma discrim_Crypt [simp]:
kaliszyk@35222
   391
  shows "discrim (Crypt K X) = discrim X + 2"
kaliszyk@35222
   392
  by (lifting freediscrim.simps(3))
kaliszyk@35222
   393
kaliszyk@36524
   394
lemma discrim_Decrypt [simp]:
kaliszyk@35222
   395
  shows "discrim (Decrypt K X) = discrim X - 2"
kaliszyk@35222
   396
  by (lifting freediscrim.simps(4))
kaliszyk@35222
   397
kaliszyk@35222
   398
end
kaliszyk@35222
   399