wneuper/isa: src/HOL/Induct/QuoDataType.thy@bc9e5587d05a

     1 (*  Title:      HOL/Induct/QuoDataType

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   2004  University of Cambridge

     6 *)

     8 header{*Defining an Initial Algebra by Quotienting a Free Algebra*}

    10 theory QuoDataType = Main:

    12 subsection{*Defining the Free Algebra*}

    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

    21 text{*The equivalence relation, which makes encryption and decryption inverses

    22 provided the keys are the same.*}

    23 consts  msgrel :: "(freemsg * freemsg) set"

    25 syntax

    26   "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "~~" 50)

    27 syntax (xsymbols)

    28   "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "\<sim>" 50)

    29 translations

    30   "X \<sim> Y" == "(X,Y) \<in> msgrel"

    32 text{*The first two rules are the desired equations. The next four rules

    33 make the equations applicable to subterms. The last two rules are symmetry

    34 and transitivity.*}

    35 inductive "msgrel"

    36   intros

    37     CD:    "CRYPT K (DECRYPT K X) \<sim> X"

    38     DC:    "DECRYPT K (CRYPT K X) \<sim> X"

    39     NONCE: "NONCE N \<sim> NONCE N"

    40     MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"

    41     CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"

    42     DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"

    43     SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"

    44     TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"

    47 text{*Proving that it is an equivalence relation*}

    49 lemma msgrel_refl: "X \<sim> X"

    50 by (induct X, (blast intro: msgrel.intros)+)

    52 theorem equiv_msgrel: "equiv UNIV msgrel"

    53 proof (simp add: equiv_def, intro conjI)

    54   show "reflexive msgrel" by (simp add: refl_def msgrel_refl)

    55   show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)

    56   show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)

    57 qed

    60 subsection{*Some Functions on the Free Algebra*}

    62 subsubsection{*The Set of Nonces*}

    64 text{*A function to return the set of nonces present in a message.  It will

    65 be lifted to the initial algrebra, to serve as an example of that process.*}

    66 consts

    67   freenonces :: "freemsg \<Rightarrow> nat set"

    69 primrec

    70    "freenonces (NONCE N) = {N}"

    71    "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"

    72    "freenonces (CRYPT K X) = freenonces X"

    73    "freenonces (DECRYPT K X) = freenonces X"

    75 text{*This theorem lets us prove that the nonces function respects the

    76 equivalence relation.  It also helps us prove that Nonce

    77   (the abstract constructor) is injective*}

    78 theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V"

    79 by (erule msgrel.induct, auto)

    82 subsubsection{*The Left Projection*}

    84 text{*A function to return the left part of the top pair in a message.  It will

    85 be lifted to the initial algrebra, to serve as an example of that process.*}

    86 consts free_left :: "freemsg \<Rightarrow> freemsg"

    87 primrec

    88    "free_left (NONCE N) = NONCE N"

    89    "free_left (MPAIR X Y) = X"

    90    "free_left (CRYPT K X) = free_left X"

    91    "free_left (DECRYPT K X) = free_left X"

    93 text{*This theorem lets us prove that the left function respects the

    94 equivalence relation.  It also helps us prove that MPair

    95   (the abstract constructor) is injective*}

    96 theorem msgrel_imp_eqv_free_left:

    97      "U \<sim> V \<Longrightarrow> free_left U \<sim> free_left V"

    98 by (erule msgrel.induct, auto intro: msgrel.intros)

   101 subsubsection{*The Right Projection*}

   103 text{*A function to return the right part of the top pair in a message.*}

   104 consts free_right :: "freemsg \<Rightarrow> freemsg"

   105 primrec

   106    "free_right (NONCE N) = NONCE N"

   107    "free_right (MPAIR X Y) = Y"

   108    "free_right (CRYPT K X) = free_right X"

   109    "free_right (DECRYPT K X) = free_right X"

   111 text{*This theorem lets us prove that the right function respects the

   112 equivalence relation.  It also helps us prove that MPair

   113   (the abstract constructor) is injective*}

   114 theorem msgrel_imp_eqv_free_right:

   115      "U \<sim> V \<Longrightarrow> free_right U \<sim> free_right V"

   116 by (erule msgrel.induct, auto intro: msgrel.intros)

   119 subsubsection{*The Discriminator for Nonces*}

   121 text{*A function to identify nonces*}

   122 consts isNONCE :: "freemsg \<Rightarrow> bool"

   123 primrec

   124    "isNONCE (NONCE N) = True"

   125    "isNONCE (MPAIR X Y) = False"

   126    "isNONCE (CRYPT K X) = isNONCE X"

   127    "isNONCE (DECRYPT K X) = isNONCE X"

   129 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}

   130 theorem msgrel_imp_eq_isNONCE:

   131      "U \<sim> V \<Longrightarrow> isNONCE U = isNONCE V"

   132 by (erule msgrel.induct, auto)

   135 subsection{*The Initial Algebra: A Quotiented Message Type*}

   137 typedef (Msg)  msg = "UNIV//msgrel"

   138     by (auto simp add: quotient_def)

   141 text{*The abstract message constructors*}

   142 constdefs

   143   Nonce :: "nat \<Rightarrow> msg"

   144   "Nonce N == Abs_Msg(msgrel``{NONCE N})"

   146   MPair :: "[msg,msg] \<Rightarrow> msg"

   147    "MPair X Y ==

   148        Abs_Msg (\<Union>U \<in> Rep_Msg(X). \<Union>V \<in> Rep_Msg(Y). msgrel``{MPAIR U V})"

   150   Crypt :: "[nat,msg] \<Rightarrow> msg"

   151    "Crypt K X ==

   152        Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{CRYPT K U})"

   154   Decrypt :: "[nat,msg] \<Rightarrow> msg"

   155    "Decrypt K X ==

   156        Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{DECRYPT K U})"

   159 text{*Reduces equality of equivalence classes to the @{term msgrel} relation:

   160   @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"} *}

   161 lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]

   163 declare equiv_msgrel_iff [simp]

   166 text{*All equivalence classes belong to set of representatives*}

   167 lemma msgrel_in_integ [simp]: "msgrel``{U} \<in> Msg"

   168 by (auto simp add: Msg_def quotient_def intro: msgrel_refl)

   170 lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"

   171 apply (rule inj_on_inverseI)

   172 apply (erule Abs_Msg_inverse)

   173 done

   175 text{*Reduces equality on abstractions to equality on representatives*}

   176 declare inj_on_Abs_Msg [THEN inj_on_iff, simp]

   178 declare Abs_Msg_inverse [simp]

   181 subsubsection{*Characteristic Equations for the Abstract Constructors*}

   183 lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) =

   184               Abs_Msg (msgrel``{MPAIR U V})"

   185 proof -

   186   have "congruent2 msgrel (\<lambda>U V. msgrel `` {MPAIR U V})"

   187     by (simp add: congruent2_def msgrel.MPAIR)

   188   thus ?thesis

   189     by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel])

   190 qed

   192 lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"

   193 proof -

   194   have "congruent msgrel (\<lambda>U. msgrel `` {CRYPT K U})"

   195     by (simp add: congruent_def msgrel.CRYPT)

   196   thus ?thesis

   197     by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])

   198 qed

   200 lemma Decrypt:

   201      "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"

   202 proof -

   203   have "congruent msgrel (\<lambda>U. msgrel `` {DECRYPT K U})"

   204     by (simp add: congruent_def msgrel.DECRYPT)

   205   thus ?thesis

   206     by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])

   207 qed

   209 text{*Case analysis on the representation of a msg as an equivalence class.*}

   210 lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]:

   211      "(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P"

   212 apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE])

   213 apply (drule arg_cong [where f=Abs_Msg])

   214 apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl)

   215 done

   217 text{*Establishing these two equations is the point of the whole exercise*}

   218 theorem CD_eq: "Crypt K (Decrypt K X) = X"

   219 by (cases X, simp add: Crypt Decrypt CD)

   221 theorem DC_eq: "Decrypt K (Crypt K X) = X"

   222 by (cases X, simp add: Crypt Decrypt DC)

   225 subsection{*The Abstract Function to Return the Set of Nonces*}

   227 constdefs

   228   nonces :: "msg \<Rightarrow> nat set"

   229    "nonces X == \<Union>U \<in> Rep_Msg(X). freenonces U"

   231 lemma nonces_congruent: "congruent msgrel (\<lambda>x. freenonces x)"

   232 by (simp add: congruent_def msgrel_imp_eq_freenonces)

   235 text{*Now prove the four equations for @{term nonces}*}

   237 lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}"

   238 by (simp add: nonces_def Nonce_def

   239               UN_equiv_class [OF equiv_msgrel nonces_congruent])

   241 lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X \<union> nonces Y"

   242 apply (cases X, cases Y)

   243 apply (simp add: nonces_def MPair

   244                  UN_equiv_class [OF equiv_msgrel nonces_congruent])

   245 done

   247 lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X"

   248 apply (cases X)

   249 apply (simp add: nonces_def Crypt

   250                  UN_equiv_class [OF equiv_msgrel nonces_congruent])

   251 done

   253 lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"

   254 apply (cases X)

   255 apply (simp add: nonces_def Decrypt

   256                  UN_equiv_class [OF equiv_msgrel nonces_congruent])

   257 done

   260 subsection{*The Abstract Function to Return the Left Part*}

   262 constdefs

   263   left :: "msg \<Rightarrow> msg"

   264    "left X == Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{free_left U})"

   266 lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {free_left U})"

   267 by (simp add: congruent_def msgrel_imp_eqv_free_left)

   269 text{*Now prove the four equations for @{term left}*}

   271 lemma left_Nonce [simp]: "left (Nonce N) = Nonce N"

   272 by (simp add: left_def Nonce_def

   273               UN_equiv_class [OF equiv_msgrel left_congruent])

   275 lemma left_MPair [simp]: "left (MPair X Y) = X"

   276 apply (cases X, cases Y)

   277 apply (simp add: left_def MPair

   278                  UN_equiv_class [OF equiv_msgrel left_congruent])

   279 done

   281 lemma left_Crypt [simp]: "left (Crypt K X) = left X"

   282 apply (cases X)

   283 apply (simp add: left_def Crypt

   284                  UN_equiv_class [OF equiv_msgrel left_congruent])

   285 done

   287 lemma left_Decrypt [simp]: "left (Decrypt K X) = left X"

   288 apply (cases X)

   289 apply (simp add: left_def Decrypt

   290                  UN_equiv_class [OF equiv_msgrel left_congruent])

   291 done

   294 subsection{*The Abstract Function to Return the Right Part*}

   296 constdefs

   297   right :: "msg \<Rightarrow> msg"

   298    "right X == Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{free_right U})"

   300 lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {free_right U})"

   301 by (simp add: congruent_def msgrel_imp_eqv_free_right)

   303 text{*Now prove the four equations for @{term right}*}

   305 lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"

   306 by (simp add: right_def Nonce_def

   307               UN_equiv_class [OF equiv_msgrel right_congruent])

   309 lemma right_MPair [simp]: "right (MPair X Y) = Y"

   310 apply (cases X, cases Y)

   311 apply (simp add: right_def MPair

   312                  UN_equiv_class [OF equiv_msgrel right_congruent])

   313 done

   315 lemma right_Crypt [simp]: "right (Crypt K X) = right X"

   316 apply (cases X)

   317 apply (simp add: right_def Crypt

   318                  UN_equiv_class [OF equiv_msgrel right_congruent])

   319 done

   321 lemma right_Decrypt [simp]: "right (Decrypt K X) = right X"

   322 apply (cases X)

   323 apply (simp add: right_def Decrypt

   324                  UN_equiv_class [OF equiv_msgrel right_congruent])

   325 done

   328 subsection{*Injectivity Properties of Some Constructors*}

   330 lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"

   331 by (drule msgrel_imp_eq_freenonces, simp)

   333 text{*Can also be proved using the function @{term nonces}*}

   334 lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"

   335 by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)

   337 lemma MPAIR_imp_eqv_left: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"

   338 apply (drule msgrel_imp_eqv_free_left)

   339 apply (simp add: );

   340 done

   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

   350 lemma MPAIR_imp_eqv_right: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"

   351 apply (drule msgrel_imp_eqv_free_right)

   352 apply (simp add: );

   353 done

   355 lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"

   356 apply (cases X, cases X', cases Y, cases Y')

   357 apply (simp add: MPair)

   358 apply (erule MPAIR_imp_eqv_right)

   359 done

   361 theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"

   362 apply (blast dest: MPair_imp_eq_left MPair_imp_eq_right)

   363 done

   365 lemma NONCE_neqv_MPAIR: "NONCE m \<sim> MPAIR X Y \<Longrightarrow> False"

   366 by (drule msgrel_imp_eq_isNONCE, simp)

   368 theorem Nonce_neq_MPair [iff]: "Nonce N \<noteq> MPair X Y"

   369 apply (cases X, cases Y)

   370 apply (simp add: Nonce_def MPair)

   371 apply (blast dest: NONCE_neqv_MPAIR)

   372 done

   374 end

author	paulson
	Wed, 07 Apr 2004 14:25:48 +0200
changeset 14527	bc9e5587d05a
child 14533	32806c0afebf
permissions	-rw-r--r--