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