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