src/HOL/Induct/QuoDataType.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58310 91ea607a34d8
child 59478 1755b24e8b44
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Title:      HOL/Induct/QuoDataType.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   2004  University of Cambridge
     4 *)
     5 
     6 section{*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 definition "Msg = UNIV//msgrel"
   127 
   128 typedef msg = Msg
   129   morphisms Rep_Msg Abs_Msg
   130   unfolding Msg_def by (auto simp add: quotient_def)
   131 
   132 
   133 text{*The abstract message constructors*}
   134 definition
   135   Nonce :: "nat \<Rightarrow> msg" where
   136   "Nonce N = Abs_Msg(msgrel``{NONCE N})"
   137 
   138 definition
   139   MPair :: "[msg,msg] \<Rightarrow> msg" where
   140    "MPair X Y =
   141        Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
   142 
   143 definition
   144   Crypt :: "[nat,msg] \<Rightarrow> msg" where
   145    "Crypt K X =
   146        Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
   147 
   148 definition
   149   Decrypt :: "[nat,msg] \<Rightarrow> msg" where
   150    "Decrypt K X =
   151        Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
   152 
   153 
   154 text{*Reduces equality of equivalence classes to the @{term msgrel} relation:
   155   @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"} *}
   156 lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]
   157 
   158 declare equiv_msgrel_iff [simp]
   159 
   160 
   161 text{*All equivalence classes belong to set of representatives*}
   162 lemma [simp]: "msgrel``{U} \<in> Msg"
   163 by (auto simp add: Msg_def quotient_def intro: msgrel_refl)
   164 
   165 lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
   166 apply (rule inj_on_inverseI)
   167 apply (erule Abs_Msg_inverse)
   168 done
   169 
   170 text{*Reduces equality on abstractions to equality on representatives*}
   171 declare inj_on_Abs_Msg [THEN inj_on_iff, simp]
   172 
   173 declare Abs_Msg_inverse [simp]
   174 
   175 
   176 subsubsection{*Characteristic Equations for the Abstract Constructors*}
   177 
   178 lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) = 
   179               Abs_Msg (msgrel``{MPAIR U V})"
   180 proof -
   181   have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
   182     by (auto simp add: congruent2_def msgrel.MPAIR)
   183   thus ?thesis
   184     by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
   185 qed
   186 
   187 lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
   188 proof -
   189   have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
   190     by (auto simp add: congruent_def msgrel.CRYPT)
   191   thus ?thesis
   192     by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
   193 qed
   194 
   195 lemma Decrypt:
   196      "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
   197 proof -
   198   have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
   199     by (auto simp add: congruent_def msgrel.DECRYPT)
   200   thus ?thesis
   201     by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
   202 qed
   203 
   204 text{*Case analysis on the representation of a msg as an equivalence class.*}
   205 lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]:
   206      "(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P"
   207 apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE])
   208 apply (drule arg_cong [where f=Abs_Msg])
   209 apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl)
   210 done
   211 
   212 text{*Establishing these two equations is the point of the whole exercise*}
   213 theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
   214 by (cases X, simp add: Crypt Decrypt CD)
   215 
   216 theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
   217 by (cases X, simp add: Crypt Decrypt DC)
   218 
   219 
   220 subsection{*The Abstract Function to Return the Set of Nonces*}
   221 
   222 definition
   223   nonces :: "msg \<Rightarrow> nat set" where
   224    "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
   225 
   226 lemma nonces_congruent: "freenonces respects msgrel"
   227 by (auto simp add: congruent_def msgrel_imp_eq_freenonces) 
   228 
   229 
   230 text{*Now prove the four equations for @{term nonces}*}
   231 
   232 lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}"
   233 by (simp add: nonces_def Nonce_def 
   234               UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
   235  
   236 lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X \<union> nonces Y"
   237 apply (cases X, cases Y) 
   238 apply (simp add: nonces_def MPair 
   239                  UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
   240 done
   241 
   242 lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X"
   243 apply (cases X) 
   244 apply (simp add: nonces_def Crypt
   245                  UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
   246 done
   247 
   248 lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
   249 apply (cases X) 
   250 apply (simp add: nonces_def Decrypt
   251                  UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
   252 done
   253 
   254 
   255 subsection{*The Abstract Function to Return the Left Part*}
   256 
   257 definition
   258   left :: "msg \<Rightarrow> msg" where
   259    "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
   260 
   261 lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
   262 by (auto simp add: congruent_def msgrel_imp_eqv_freeleft) 
   263 
   264 text{*Now prove the four equations for @{term left}*}
   265 
   266 lemma left_Nonce [simp]: "left (Nonce N) = Nonce N"
   267 by (simp add: left_def Nonce_def 
   268               UN_equiv_class [OF equiv_msgrel left_congruent]) 
   269 
   270 lemma left_MPair [simp]: "left (MPair X Y) = X"
   271 apply (cases X, cases Y) 
   272 apply (simp add: left_def MPair 
   273                  UN_equiv_class [OF equiv_msgrel left_congruent]) 
   274 done
   275 
   276 lemma left_Crypt [simp]: "left (Crypt K X) = left X"
   277 apply (cases X) 
   278 apply (simp add: left_def Crypt
   279                  UN_equiv_class [OF equiv_msgrel left_congruent]) 
   280 done
   281 
   282 lemma left_Decrypt [simp]: "left (Decrypt K X) = left X"
   283 apply (cases X) 
   284 apply (simp add: left_def Decrypt
   285                  UN_equiv_class [OF equiv_msgrel left_congruent]) 
   286 done
   287 
   288 
   289 subsection{*The Abstract Function to Return the Right Part*}
   290 
   291 definition
   292   right :: "msg \<Rightarrow> msg" where
   293    "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
   294 
   295 lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
   296 by (auto simp add: congruent_def msgrel_imp_eqv_freeright) 
   297 
   298 text{*Now prove the four equations for @{term right}*}
   299 
   300 lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"
   301 by (simp add: right_def Nonce_def 
   302               UN_equiv_class [OF equiv_msgrel right_congruent]) 
   303 
   304 lemma right_MPair [simp]: "right (MPair X Y) = Y"
   305 apply (cases X, cases Y) 
   306 apply (simp add: right_def MPair 
   307                  UN_equiv_class [OF equiv_msgrel right_congruent]) 
   308 done
   309 
   310 lemma right_Crypt [simp]: "right (Crypt K X) = right X"
   311 apply (cases X) 
   312 apply (simp add: right_def Crypt
   313                  UN_equiv_class [OF equiv_msgrel right_congruent]) 
   314 done
   315 
   316 lemma right_Decrypt [simp]: "right (Decrypt K X) = right X"
   317 apply (cases X) 
   318 apply (simp add: right_def Decrypt
   319                  UN_equiv_class [OF equiv_msgrel right_congruent]) 
   320 done
   321 
   322 
   323 subsection{*Injectivity Properties of Some Constructors*}
   324 
   325 lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
   326 by (drule msgrel_imp_eq_freenonces, simp)
   327 
   328 text{*Can also be proved using the function @{term nonces}*}
   329 lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"
   330 by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)
   331 
   332 lemma MPAIR_imp_eqv_left: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
   333 by (drule msgrel_imp_eqv_freeleft, simp)
   334 
   335 lemma MPair_imp_eq_left: 
   336   assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'"
   337 proof -
   338   from eq
   339   have "left (MPair X Y) = left (MPair X' Y')" by simp
   340   thus ?thesis by simp
   341 qed
   342 
   343 lemma MPAIR_imp_eqv_right: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
   344 by (drule msgrel_imp_eqv_freeright, simp)
   345 
   346 lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'" 
   347 apply (cases X, cases X', cases Y, cases Y') 
   348 apply (simp add: MPair)
   349 apply (erule MPAIR_imp_eqv_right)  
   350 done
   351 
   352 theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" 
   353 by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
   354 
   355 lemma NONCE_neqv_MPAIR: "NONCE m \<sim> MPAIR X Y \<Longrightarrow> False"
   356 by (drule msgrel_imp_eq_freediscrim, simp)
   357 
   358 theorem Nonce_neq_MPair [iff]: "Nonce N \<noteq> MPair X Y"
   359 apply (cases X, cases Y) 
   360 apply (simp add: Nonce_def MPair) 
   361 apply (blast dest: NONCE_neqv_MPAIR) 
   362 done
   363 
   364 text{*Example suggested by a referee*}
   365 theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) \<noteq> Nonce N" 
   366 by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)  
   367 
   368 text{*...and many similar results*}
   369 theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N" 
   370 by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)  
   371 
   372 theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')" 
   373 proof
   374   assume "Crypt K X = Crypt K X'"
   375   hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
   376   thus "X = X'" by simp
   377 next
   378   assume "X = X'"
   379   thus "Crypt K X = Crypt K X'" by simp
   380 qed
   381 
   382 theorem Decrypt_Decrypt_eq [iff]: "(Decrypt K X = Decrypt K X') = (X=X')" 
   383 proof
   384   assume "Decrypt K X = Decrypt K X'"
   385   hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
   386   thus "X = X'" by simp
   387 next
   388   assume "X = X'"
   389   thus "Decrypt K X = Decrypt K X'" by simp
   390 qed
   391 
   392 lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
   393   assumes N: "\<And>N. P (Nonce N)"
   394       and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
   395       and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
   396       and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   397   shows "P msg"
   398 proof (cases msg)
   399   case (Abs_Msg U)
   400   have "P (Abs_Msg (msgrel `` {U}))"
   401   proof (induct U)
   402     case (NONCE N) 
   403     with N show ?case by (simp add: Nonce_def) 
   404   next
   405     case (MPAIR X Y)
   406     with M [of "Abs_Msg (msgrel `` {X})" "Abs_Msg (msgrel `` {Y})"]
   407     show ?case by (simp add: MPair) 
   408   next
   409     case (CRYPT K X)
   410     with C [of "Abs_Msg (msgrel `` {X})"]
   411     show ?case by (simp add: Crypt) 
   412   next
   413     case (DECRYPT K X)
   414     with D [of "Abs_Msg (msgrel `` {X})"]
   415     show ?case by (simp add: Decrypt)
   416   qed
   417   with Abs_Msg show ?thesis by (simp only:)
   418 qed
   419 
   420 
   421 subsection{*The Abstract Discriminator*}
   422 
   423 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
   424 need this function in order to prove discrimination theorems.*}
   425 
   426 definition
   427   discrim :: "msg \<Rightarrow> int" where
   428    "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
   429 
   430 lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
   431 by (auto simp add: congruent_def msgrel_imp_eq_freediscrim) 
   432 
   433 text{*Now prove the four equations for @{term discrim}*}
   434 
   435 lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0"
   436 by (simp add: discrim_def Nonce_def 
   437               UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
   438 
   439 lemma discrim_MPair [simp]: "discrim (MPair X Y) = 1"
   440 apply (cases X, cases Y) 
   441 apply (simp add: discrim_def MPair 
   442                  UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
   443 done
   444 
   445 lemma discrim_Crypt [simp]: "discrim (Crypt K X) = discrim X + 2"
   446 apply (cases X) 
   447 apply (simp add: discrim_def Crypt
   448                  UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
   449 done
   450 
   451 lemma discrim_Decrypt [simp]: "discrim (Decrypt K X) = discrim X - 2"
   452 apply (cases X) 
   453 apply (simp add: discrim_def Decrypt
   454                  UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
   455 done
   456 
   457 
   458 end
   459