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