src/HOL/Quotient_Examples/Quotient_Message.thy
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55415 05f5fdb8d093
parent 47304 a0d97d919f01
child 58305 57752a91eec4
permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
     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 "~~/src/HOL/Library/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 done
   140 
   141 quotient_definition
   142   "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
   143 is
   144   "MPAIR"
   145 by (rule MPAIR)
   146 
   147 quotient_definition
   148   "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   149 is
   150   "CRYPT"
   151 by (rule CRYPT)
   152 
   153 quotient_definition
   154   "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   155 is
   156   "DECRYPT"
   157 by (rule DECRYPT)
   158 
   159 text{*Establishing these two equations is the point of the whole exercise*}
   160 theorem CD_eq [simp]:
   161   shows "Crypt K (Decrypt K X) = X"
   162   by (lifting CD)
   163 
   164 theorem DC_eq [simp]:
   165   shows "Decrypt K (Crypt K X) = X"
   166   by (lifting DC)
   167 
   168 subsection{*The Abstract Function to Return the Set of Nonces*}
   169 
   170 quotient_definition
   171    "nonces:: msg \<Rightarrow> nat set"
   172 is
   173   "freenonces"
   174 by (rule msgrel_imp_eq_freenonces)
   175 
   176 text{*Now prove the four equations for @{term nonces}*}
   177 
   178 lemma nonces_Nonce [simp]:
   179   shows "nonces (Nonce N) = {N}"
   180   by (lifting freenonces.simps(1))
   181 
   182 lemma nonces_MPair [simp]:
   183   shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
   184   by (lifting freenonces.simps(2))
   185 
   186 lemma nonces_Crypt [simp]:
   187   shows "nonces (Crypt K X) = nonces X"
   188   by (lifting freenonces.simps(3))
   189 
   190 lemma nonces_Decrypt [simp]:
   191   shows "nonces (Decrypt K X) = nonces X"
   192   by (lifting freenonces.simps(4))
   193 
   194 subsection{*The Abstract Function to Return the Left Part*}
   195 
   196 quotient_definition
   197   "left:: msg \<Rightarrow> msg"
   198 is
   199   "freeleft"
   200 by (rule msgrel_imp_eqv_freeleft)
   201 
   202 lemma left_Nonce [simp]:
   203   shows "left (Nonce N) = Nonce N"
   204   by (lifting freeleft.simps(1))
   205 
   206 lemma left_MPair [simp]:
   207   shows "left (MPair X Y) = X"
   208   by (lifting freeleft.simps(2))
   209 
   210 lemma left_Crypt [simp]:
   211   shows "left (Crypt K X) = left X"
   212   by (lifting freeleft.simps(3))
   213 
   214 lemma left_Decrypt [simp]:
   215   shows "left (Decrypt K X) = left X"
   216   by (lifting freeleft.simps(4))
   217 
   218 subsection{*The Abstract Function to Return the Right Part*}
   219 
   220 quotient_definition
   221   "right:: msg \<Rightarrow> msg"
   222 is
   223   "freeright"
   224 by (rule msgrel_imp_eqv_freeright)
   225 
   226 text{*Now prove the four equations for @{term right}*}
   227 
   228 lemma right_Nonce [simp]:
   229   shows "right (Nonce N) = Nonce N"
   230   by (lifting freeright.simps(1))
   231 
   232 lemma right_MPair [simp]:
   233   shows "right (MPair X Y) = Y"
   234   by (lifting freeright.simps(2))
   235 
   236 lemma right_Crypt [simp]:
   237   shows "right (Crypt K X) = right X"
   238   by (lifting freeright.simps(3))
   239 
   240 lemma right_Decrypt [simp]:
   241   shows "right (Decrypt K X) = right X"
   242   by (lifting freeright.simps(4))
   243 
   244 subsection{*Injectivity Properties of Some Constructors*}
   245 
   246 text{*Can also be proved using the function @{term nonces}*}
   247 lemma Nonce_Nonce_eq [iff]:
   248   shows "(Nonce m = Nonce n) = (m = n)"
   249 proof
   250   assume "Nonce m = Nonce n"
   251   then show "m = n" 
   252     by (descending) (drule msgrel_imp_eq_freenonces, simp)
   253 next
   254   assume "m = n"
   255   then show "Nonce m = Nonce n" by simp
   256 qed
   257 
   258 lemma MPair_imp_eq_left:
   259   assumes eq: "MPair X Y = MPair X' Y'"
   260   shows "X = X'"
   261   using eq 
   262   by (descending) (drule msgrel_imp_eqv_freeleft, simp)
   263 
   264 lemma MPair_imp_eq_right:
   265   shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
   266   by (descending) (drule msgrel_imp_eqv_freeright, simp)
   267 
   268 theorem MPair_MPair_eq [iff]:
   269   shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
   270   by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
   271 
   272 theorem Nonce_neq_MPair [iff]:
   273   shows "Nonce N \<noteq> MPair X Y"
   274   by (descending) (auto dest: msgrel_imp_eq_freediscrim)
   275 
   276 text{*Example suggested by a referee*}
   277 
   278 theorem Crypt_Nonce_neq_Nonce:
   279   shows "Crypt K (Nonce M) \<noteq> Nonce N"
   280   by (descending) (auto dest: msgrel_imp_eq_freediscrim) 
   281 
   282 text{*...and many similar results*}
   283 
   284 theorem Crypt2_Nonce_neq_Nonce:
   285   shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
   286   by (descending) (auto dest: msgrel_imp_eq_freediscrim)
   287 
   288 theorem Crypt_Crypt_eq [iff]:
   289   shows "(Crypt K X = Crypt K X') = (X=X')"
   290 proof
   291   assume "Crypt K X = Crypt K X'"
   292   hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
   293   thus "X = X'" by simp
   294 next
   295   assume "X = X'"
   296   thus "Crypt K X = Crypt K X'" by simp
   297 qed
   298 
   299 theorem Decrypt_Decrypt_eq [iff]:
   300   shows "(Decrypt K X = Decrypt K X') = (X=X')"
   301 proof
   302   assume "Decrypt K X = Decrypt K X'"
   303   hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
   304   thus "X = X'" by simp
   305 next
   306   assume "X = X'"
   307   thus "Decrypt K X = Decrypt K X'" by simp
   308 qed
   309 
   310 lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
   311   assumes N: "\<And>N. P (Nonce N)"
   312       and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
   313       and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
   314       and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   315   shows "P msg"
   316   using N M C D 
   317   by (descending) (auto intro: freemsg.induct)
   318 
   319 
   320 subsection{*The Abstract Discriminator*}
   321 
   322 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
   323 need this function in order to prove discrimination theorems.*}
   324 
   325 quotient_definition
   326   "discrim:: msg \<Rightarrow> int"
   327 is
   328   "freediscrim"
   329 by (rule msgrel_imp_eq_freediscrim)
   330 
   331 text{*Now prove the four equations for @{term discrim}*}
   332 
   333 lemma discrim_Nonce [simp]:
   334   shows "discrim (Nonce N) = 0"
   335   by (lifting freediscrim.simps(1))
   336 
   337 lemma discrim_MPair [simp]:
   338   shows "discrim (MPair X Y) = 1"
   339   by (lifting freediscrim.simps(2))
   340 
   341 lemma discrim_Crypt [simp]:
   342   shows "discrim (Crypt K X) = discrim X + 2"
   343   by (lifting freediscrim.simps(3))
   344 
   345 lemma discrim_Decrypt [simp]:
   346   shows "discrim (Decrypt K X) = discrim X - 2"
   347   by (lifting freediscrim.simps(4))
   348 
   349 end
   350