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