src/HOL/Quotient_Examples/Quotient_Message.thy
author haftmann
Tue Nov 30 17:19:11 2010 +0100 (2010-11-30)
changeset 40823 37b25a87d7ef
parent 40468 d4aac200199e
child 41467 8fc17c5e11c0
permissions -rw-r--r--
adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
     1 (*  Title:      HOL/Quotient_Examples/Quotient_Message.thy
     2     Author:     Christian Urban
     3 
     4 Message datatype, based on an older version by Larry Paulson.
     5 *)
     6 theory Quotient_Message
     7 imports Main Quotient_Syntax
     8 begin
     9 
    10 subsection{*Defining the Free Algebra*}
    11 
    12 datatype
    13   freemsg = NONCE  nat
    14         | MPAIR  freemsg freemsg
    15         | CRYPT  nat freemsg
    16         | DECRYPT  nat freemsg
    17 
    18 inductive
    19   msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
    20 where
    21   CD:    "CRYPT K (DECRYPT K X) \<sim> X"
    22 | DC:    "DECRYPT K (CRYPT K X) \<sim> X"
    23 | NONCE: "NONCE N \<sim> NONCE N"
    24 | MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
    25 | CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
    26 | DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
    27 | SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
    28 | TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
    29 
    30 lemmas msgrel.intros[intro]
    31 
    32 text{*Proving that it is an equivalence relation*}
    33 
    34 lemma msgrel_refl: "X \<sim> X"
    35 by (induct X) (auto intro: msgrel.intros)
    36 
    37 theorem equiv_msgrel: "equivp msgrel"
    38 proof (rule equivpI)
    39   show "reflp msgrel" by (rule reflpI) (simp add: msgrel_refl)
    40   show "symp msgrel" by (rule sympI) (blast intro: msgrel.SYM)
    41   show "transp msgrel" by (rule transpI) (blast intro: msgrel.TRANS)
    42 qed
    43 
    44 subsection{*Some Functions on the Free Algebra*}
    45 
    46 subsubsection{*The Set of Nonces*}
    47 
    48 primrec
    49   freenonces :: "freemsg \<Rightarrow> nat set"
    50 where
    51   "freenonces (NONCE N) = {N}"
    52 | "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
    53 | "freenonces (CRYPT K X) = freenonces X"
    54 | "freenonces (DECRYPT K X) = freenonces X"
    55 
    56 theorem msgrel_imp_eq_freenonces:
    57   assumes a: "U \<sim> V"
    58   shows "freenonces U = freenonces V"
    59   using a by (induct) (auto)
    60 
    61 subsubsection{*The Left Projection*}
    62 
    63 text{*A function to return the left part of the top pair in a message.  It will
    64 be lifted to the initial algrebra, to serve as an example of that process.*}
    65 primrec
    66   freeleft :: "freemsg \<Rightarrow> freemsg"
    67 where
    68   "freeleft (NONCE N) = NONCE N"
    69 | "freeleft (MPAIR X Y) = X"
    70 | "freeleft (CRYPT K X) = freeleft X"
    71 | "freeleft (DECRYPT K X) = freeleft X"
    72 
    73 text{*This theorem lets us prove that the left function respects the
    74 equivalence relation.  It also helps us prove that MPair
    75   (the abstract constructor) is injective*}
    76 lemma msgrel_imp_eqv_freeleft_aux:
    77   shows "freeleft U \<sim> freeleft U"
    78   by (fact msgrel_refl)
    79 
    80 theorem msgrel_imp_eqv_freeleft:
    81   assumes a: "U \<sim> V"
    82   shows "freeleft U \<sim> freeleft V"
    83   using a
    84   by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
    85 
    86 subsubsection{*The Right Projection*}
    87 
    88 text{*A function to return the right part of the top pair in a message.*}
    89 primrec
    90   freeright :: "freemsg \<Rightarrow> freemsg"
    91 where
    92   "freeright (NONCE N) = NONCE N"
    93 | "freeright (MPAIR X Y) = Y"
    94 | "freeright (CRYPT K X) = freeright X"
    95 | "freeright (DECRYPT K X) = freeright X"
    96 
    97 text{*This theorem lets us prove that the right function respects the
    98 equivalence relation.  It also helps us prove that MPair
    99   (the abstract constructor) is injective*}
   100 lemma msgrel_imp_eqv_freeright_aux:
   101   shows "freeright U \<sim> freeright U"
   102   by (fact msgrel_refl)
   103 
   104 theorem msgrel_imp_eqv_freeright:
   105   assumes a: "U \<sim> V"
   106   shows "freeright U \<sim> freeright V"
   107   using a
   108   by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
   109 
   110 subsubsection{*The Discriminator for Constructors*}
   111 
   112 text{*A function to distinguish nonces, mpairs and encryptions*}
   113 primrec
   114   freediscrim :: "freemsg \<Rightarrow> int"
   115 where
   116    "freediscrim (NONCE N) = 0"
   117  | "freediscrim (MPAIR X Y) = 1"
   118  | "freediscrim (CRYPT K X) = freediscrim X + 2"
   119  | "freediscrim (DECRYPT K X) = freediscrim X - 2"
   120 
   121 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
   122 theorem msgrel_imp_eq_freediscrim:
   123   assumes a: "U \<sim> V"
   124   shows "freediscrim U = freediscrim V"
   125   using a by (induct) (auto)
   126 
   127 subsection{*The Initial Algebra: A Quotiented Message Type*}
   128 
   129 quotient_type msg = freemsg / msgrel
   130   by (rule equiv_msgrel)
   131 
   132 text{*The abstract message constructors*}
   133 
   134 quotient_definition
   135   "Nonce :: nat \<Rightarrow> msg"
   136 is
   137   "NONCE"
   138 
   139 quotient_definition
   140   "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
   141 is
   142   "MPAIR"
   143 
   144 quotient_definition
   145   "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   146 is
   147   "CRYPT"
   148 
   149 quotient_definition
   150   "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   151 is
   152   "DECRYPT"
   153 
   154 lemma [quot_respect]:
   155   shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
   156 by (auto intro: CRYPT)
   157 
   158 lemma [quot_respect]:
   159   shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
   160 by (auto intro: DECRYPT)
   161 
   162 text{*Establishing these two equations is the point of the whole exercise*}
   163 theorem CD_eq [simp]:
   164   shows "Crypt K (Decrypt K X) = X"
   165   by (lifting CD)
   166 
   167 theorem DC_eq [simp]:
   168   shows "Decrypt K (Crypt K X) = X"
   169   by (lifting DC)
   170 
   171 subsection{*The Abstract Function to Return the Set of Nonces*}
   172 
   173 quotient_definition
   174    "nonces:: msg \<Rightarrow> nat set"
   175 is
   176   "freenonces"
   177 
   178 text{*Now prove the four equations for @{term nonces}*}
   179 
   180 lemma [quot_respect]:
   181   shows "(op \<sim> ===> op =) freenonces freenonces"
   182   by (auto simp add: msgrel_imp_eq_freenonces)
   183 
   184 lemma [quot_respect]:
   185   shows "(op = ===> op \<sim>) NONCE NONCE"
   186   by (auto simp add: NONCE)
   187 
   188 lemma nonces_Nonce [simp]:
   189   shows "nonces (Nonce N) = {N}"
   190   by (lifting freenonces.simps(1))
   191 
   192 lemma [quot_respect]:
   193   shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
   194   by (auto simp add: MPAIR)
   195 
   196 lemma nonces_MPair [simp]:
   197   shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
   198   by (lifting freenonces.simps(2))
   199 
   200 lemma nonces_Crypt [simp]:
   201   shows "nonces (Crypt K X) = nonces X"
   202   by (lifting freenonces.simps(3))
   203 
   204 lemma nonces_Decrypt [simp]:
   205   shows "nonces (Decrypt K X) = nonces X"
   206   by (lifting freenonces.simps(4))
   207 
   208 subsection{*The Abstract Function to Return the Left Part*}
   209 
   210 quotient_definition
   211   "left:: msg \<Rightarrow> msg"
   212 is
   213   "freeleft"
   214 
   215 lemma [quot_respect]:
   216   shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
   217   by (auto simp add: msgrel_imp_eqv_freeleft)
   218 
   219 lemma left_Nonce [simp]:
   220   shows "left (Nonce N) = Nonce N"
   221   by (lifting freeleft.simps(1))
   222 
   223 lemma left_MPair [simp]:
   224   shows "left (MPair X Y) = X"
   225   by (lifting freeleft.simps(2))
   226 
   227 lemma left_Crypt [simp]:
   228   shows "left (Crypt K X) = left X"
   229   by (lifting freeleft.simps(3))
   230 
   231 lemma left_Decrypt [simp]:
   232   shows "left (Decrypt K X) = left X"
   233   by (lifting freeleft.simps(4))
   234 
   235 subsection{*The Abstract Function to Return the Right Part*}
   236 
   237 quotient_definition
   238   "right:: msg \<Rightarrow> msg"
   239 is
   240   "freeright"
   241 
   242 text{*Now prove the four equations for @{term right}*}
   243 
   244 lemma [quot_respect]:
   245   shows "(op \<sim> ===> op \<sim>) freeright freeright"
   246   by (auto simp add: msgrel_imp_eqv_freeright)
   247 
   248 lemma right_Nonce [simp]:
   249   shows "right (Nonce N) = Nonce N"
   250   by (lifting freeright.simps(1))
   251 
   252 lemma right_MPair [simp]:
   253   shows "right (MPair X Y) = Y"
   254   by (lifting freeright.simps(2))
   255 
   256 lemma right_Crypt [simp]:
   257   shows "right (Crypt K X) = right X"
   258   by (lifting freeright.simps(3))
   259 
   260 lemma right_Decrypt [simp]:
   261   shows "right (Decrypt K X) = right X"
   262   by (lifting freeright.simps(4))
   263 
   264 subsection{*Injectivity Properties of Some Constructors*}
   265 
   266 text{*Can also be proved using the function @{term nonces}*}
   267 lemma Nonce_Nonce_eq [iff]:
   268   shows "(Nonce m = Nonce n) = (m = n)"
   269 proof
   270   assume "Nonce m = Nonce n"
   271   then show "m = n" 
   272     by (descending) (drule msgrel_imp_eq_freenonces, simp)
   273 next
   274   assume "m = n"
   275   then show "Nonce m = Nonce n" by simp
   276 qed
   277 
   278 lemma MPair_imp_eq_left:
   279   assumes eq: "MPair X Y = MPair X' Y'"
   280   shows "X = X'"
   281   using eq 
   282   by (descending) (drule msgrel_imp_eqv_freeleft, simp)
   283 
   284 lemma MPair_imp_eq_right:
   285   shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
   286   by (descending) (drule msgrel_imp_eqv_freeright, simp)
   287 
   288 theorem MPair_MPair_eq [iff]:
   289   shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
   290   by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
   291 
   292 theorem Nonce_neq_MPair [iff]:
   293   shows "Nonce N \<noteq> MPair X Y"
   294   by (descending) (auto dest: msgrel_imp_eq_freediscrim)
   295 
   296 text{*Example suggested by a referee*}
   297 
   298 theorem Crypt_Nonce_neq_Nonce:
   299   shows "Crypt K (Nonce M) \<noteq> Nonce N"
   300   by (descending) (auto dest: msgrel_imp_eq_freediscrim) 
   301 
   302 text{*...and many similar results*}
   303 
   304 theorem Crypt2_Nonce_neq_Nonce:
   305   shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
   306   by (descending) (auto dest: msgrel_imp_eq_freediscrim)
   307 
   308 theorem Crypt_Crypt_eq [iff]:
   309   shows "(Crypt K X = Crypt K X') = (X=X')"
   310 proof
   311   assume "Crypt K X = Crypt K X'"
   312   hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
   313   thus "X = X'" by simp
   314 next
   315   assume "X = X'"
   316   thus "Crypt K X = Crypt K X'" by simp
   317 qed
   318 
   319 theorem Decrypt_Decrypt_eq [iff]:
   320   shows "(Decrypt K X = Decrypt K X') = (X=X')"
   321 proof
   322   assume "Decrypt K X = Decrypt K X'"
   323   hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
   324   thus "X = X'" by simp
   325 next
   326   assume "X = X'"
   327   thus "Decrypt K X = Decrypt K X'" by simp
   328 qed
   329 
   330 lemma msg_induct_aux:
   331   shows "\<lbrakk>\<And>N. P (Nonce N);
   332           \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
   333           \<And>K X. P X \<Longrightarrow> P (Crypt K X);
   334           \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
   335   by (lifting freemsg.induct)
   336 
   337 lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
   338   assumes N: "\<And>N. P (Nonce N)"
   339       and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
   340       and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
   341       and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   342   shows "P msg"
   343   using N M C D by (rule msg_induct_aux)
   344 
   345 subsection{*The Abstract Discriminator*}
   346 
   347 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
   348 need this function in order to prove discrimination theorems.*}
   349 
   350 quotient_definition
   351   "discrim:: msg \<Rightarrow> int"
   352 is
   353   "freediscrim"
   354 
   355 text{*Now prove the four equations for @{term discrim}*}
   356 
   357 lemma [quot_respect]:
   358   shows "(op \<sim> ===> op =) freediscrim freediscrim"
   359   by (auto simp add: msgrel_imp_eq_freediscrim)
   360 
   361 lemma discrim_Nonce [simp]:
   362   shows "discrim (Nonce N) = 0"
   363   by (lifting freediscrim.simps(1))
   364 
   365 lemma discrim_MPair [simp]:
   366   shows "discrim (MPair X Y) = 1"
   367   by (lifting freediscrim.simps(2))
   368 
   369 lemma discrim_Crypt [simp]:
   370   shows "discrim (Crypt K X) = discrim X + 2"
   371   by (lifting freediscrim.simps(3))
   372 
   373 lemma discrim_Decrypt [simp]:
   374   shows "discrim (Decrypt K X) = discrim X - 2"
   375   by (lifting freediscrim.simps(4))
   376 
   377 end
   378