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