src/HOL/Quotient_Examples/Quotient_Message.thy
changeset 36524 3909002beca5
parent 35222 4f1fba00f66d
child 37594 32ad67684ee7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Thu Apr 29 09:06:35 2010 +0200
     1.3 @@ -0,0 +1,399 @@
     1.4 +(*  Title:      HOL/Quotient_Examples/Quotient_Message.thy
     1.5 +    Author:     Christian Urban
     1.6 +
     1.7 +Message datatype, based on an older version by Larry Paulson.
     1.8 +*)
     1.9 +theory Quotient_Message
    1.10 +imports Main Quotient_Syntax
    1.11 +begin
    1.12 +
    1.13 +subsection{*Defining the Free Algebra*}
    1.14 +
    1.15 +datatype
    1.16 +  freemsg = NONCE  nat
    1.17 +        | MPAIR  freemsg freemsg
    1.18 +        | CRYPT  nat freemsg
    1.19 +        | DECRYPT  nat freemsg
    1.20 +
    1.21 +inductive
    1.22 +  msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
    1.23 +where
    1.24 +  CD:    "CRYPT K (DECRYPT K X) \<sim> X"
    1.25 +| DC:    "DECRYPT K (CRYPT K X) \<sim> X"
    1.26 +| NONCE: "NONCE N \<sim> NONCE N"
    1.27 +| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
    1.28 +| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
    1.29 +| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
    1.30 +| SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
    1.31 +| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
    1.32 +
    1.33 +lemmas msgrel.intros[intro]
    1.34 +
    1.35 +text{*Proving that it is an equivalence relation*}
    1.36 +
    1.37 +lemma msgrel_refl: "X \<sim> X"
    1.38 +by (induct X, (blast intro: msgrel.intros)+)
    1.39 +
    1.40 +theorem equiv_msgrel: "equivp msgrel"
    1.41 +proof (rule equivpI)
    1.42 +  show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
    1.43 +  show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
    1.44 +  show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
    1.45 +qed
    1.46 +
    1.47 +subsection{*Some Functions on the Free Algebra*}
    1.48 +
    1.49 +subsubsection{*The Set of Nonces*}
    1.50 +
    1.51 +fun
    1.52 +  freenonces :: "freemsg \<Rightarrow> nat set"
    1.53 +where
    1.54 +  "freenonces (NONCE N) = {N}"
    1.55 +| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
    1.56 +| "freenonces (CRYPT K X) = freenonces X"
    1.57 +| "freenonces (DECRYPT K X) = freenonces X"
    1.58 +
    1.59 +theorem msgrel_imp_eq_freenonces:
    1.60 +  assumes a: "U \<sim> V"
    1.61 +  shows "freenonces U = freenonces V"
    1.62 +  using a by (induct) (auto)
    1.63 +
    1.64 +subsubsection{*The Left Projection*}
    1.65 +
    1.66 +text{*A function to return the left part of the top pair in a message.  It will
    1.67 +be lifted to the initial algrebra, to serve as an example of that process.*}
    1.68 +fun
    1.69 +  freeleft :: "freemsg \<Rightarrow> freemsg"
    1.70 +where
    1.71 +  "freeleft (NONCE N) = NONCE N"
    1.72 +| "freeleft (MPAIR X Y) = X"
    1.73 +| "freeleft (CRYPT K X) = freeleft X"
    1.74 +| "freeleft (DECRYPT K X) = freeleft X"
    1.75 +
    1.76 +text{*This theorem lets us prove that the left function respects the
    1.77 +equivalence relation.  It also helps us prove that MPair
    1.78 +  (the abstract constructor) is injective*}
    1.79 +lemma msgrel_imp_eqv_freeleft_aux:
    1.80 +  shows "freeleft U \<sim> freeleft U"
    1.81 +  by (induct rule: freeleft.induct) (auto)
    1.82 +
    1.83 +theorem msgrel_imp_eqv_freeleft:
    1.84 +  assumes a: "U \<sim> V"
    1.85 +  shows "freeleft U \<sim> freeleft V"
    1.86 +  using a
    1.87 +  by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
    1.88 +
    1.89 +subsubsection{*The Right Projection*}
    1.90 +
    1.91 +text{*A function to return the right part of the top pair in a message.*}
    1.92 +fun
    1.93 +  freeright :: "freemsg \<Rightarrow> freemsg"
    1.94 +where
    1.95 +  "freeright (NONCE N) = NONCE N"
    1.96 +| "freeright (MPAIR X Y) = Y"
    1.97 +| "freeright (CRYPT K X) = freeright X"
    1.98 +| "freeright (DECRYPT K X) = freeright X"
    1.99 +
   1.100 +text{*This theorem lets us prove that the right function respects the
   1.101 +equivalence relation.  It also helps us prove that MPair
   1.102 +  (the abstract constructor) is injective*}
   1.103 +lemma msgrel_imp_eqv_freeright_aux:
   1.104 +  shows "freeright U \<sim> freeright U"
   1.105 +  by (induct rule: freeright.induct) (auto)
   1.106 +
   1.107 +theorem msgrel_imp_eqv_freeright:
   1.108 +  assumes a: "U \<sim> V"
   1.109 +  shows "freeright U \<sim> freeright V"
   1.110 +  using a
   1.111 +  by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
   1.112 +
   1.113 +subsubsection{*The Discriminator for Constructors*}
   1.114 +
   1.115 +text{*A function to distinguish nonces, mpairs and encryptions*}
   1.116 +fun
   1.117 +  freediscrim :: "freemsg \<Rightarrow> int"
   1.118 +where
   1.119 +   "freediscrim (NONCE N) = 0"
   1.120 + | "freediscrim (MPAIR X Y) = 1"
   1.121 + | "freediscrim (CRYPT K X) = freediscrim X + 2"
   1.122 + | "freediscrim (DECRYPT K X) = freediscrim X - 2"
   1.123 +
   1.124 +text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
   1.125 +theorem msgrel_imp_eq_freediscrim:
   1.126 +  assumes a: "U \<sim> V"
   1.127 +  shows "freediscrim U = freediscrim V"
   1.128 +  using a by (induct) (auto)
   1.129 +
   1.130 +subsection{*The Initial Algebra: A Quotiented Message Type*}
   1.131 +
   1.132 +quotient_type msg = freemsg / msgrel
   1.133 +  by (rule equiv_msgrel)
   1.134 +
   1.135 +text{*The abstract message constructors*}
   1.136 +
   1.137 +quotient_definition
   1.138 +  "Nonce :: nat \<Rightarrow> msg"
   1.139 +is
   1.140 +  "NONCE"
   1.141 +
   1.142 +quotient_definition
   1.143 +  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
   1.144 +is
   1.145 +  "MPAIR"
   1.146 +
   1.147 +quotient_definition
   1.148 +  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   1.149 +is
   1.150 +  "CRYPT"
   1.151 +
   1.152 +quotient_definition
   1.153 +  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   1.154 +is
   1.155 +  "DECRYPT"
   1.156 +
   1.157 +lemma [quot_respect]:
   1.158 +  shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
   1.159 +by (auto intro: CRYPT)
   1.160 +
   1.161 +lemma [quot_respect]:
   1.162 +  shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
   1.163 +by (auto intro: DECRYPT)
   1.164 +
   1.165 +text{*Establishing these two equations is the point of the whole exercise*}
   1.166 +theorem CD_eq [simp]:
   1.167 +  shows "Crypt K (Decrypt K X) = X"
   1.168 +  by (lifting CD)
   1.169 +
   1.170 +theorem DC_eq [simp]:
   1.171 +  shows "Decrypt K (Crypt K X) = X"
   1.172 +  by (lifting DC)
   1.173 +
   1.174 +subsection{*The Abstract Function to Return the Set of Nonces*}
   1.175 +
   1.176 +quotient_definition
   1.177 +   "nonces:: msg \<Rightarrow> nat set"
   1.178 +is
   1.179 +  "freenonces"
   1.180 +
   1.181 +text{*Now prove the four equations for @{term nonces}*}
   1.182 +
   1.183 +lemma [quot_respect]:
   1.184 +  shows "(op \<sim> ===> op =) freenonces freenonces"
   1.185 +  by (simp add: msgrel_imp_eq_freenonces)
   1.186 +
   1.187 +lemma [quot_respect]:
   1.188 +  shows "(op = ===> op \<sim>) NONCE NONCE"
   1.189 +  by (simp add: NONCE)
   1.190 +
   1.191 +lemma nonces_Nonce [simp]:
   1.192 +  shows "nonces (Nonce N) = {N}"
   1.193 +  by (lifting freenonces.simps(1))
   1.194 +
   1.195 +lemma [quot_respect]:
   1.196 +  shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
   1.197 +  by (simp add: MPAIR)
   1.198 +
   1.199 +lemma nonces_MPair [simp]:
   1.200 +  shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
   1.201 +  by (lifting freenonces.simps(2))
   1.202 +
   1.203 +lemma nonces_Crypt [simp]:
   1.204 +  shows "nonces (Crypt K X) = nonces X"
   1.205 +  by (lifting freenonces.simps(3))
   1.206 +
   1.207 +lemma nonces_Decrypt [simp]:
   1.208 +  shows "nonces (Decrypt K X) = nonces X"
   1.209 +  by (lifting freenonces.simps(4))
   1.210 +
   1.211 +subsection{*The Abstract Function to Return the Left Part*}
   1.212 +
   1.213 +quotient_definition
   1.214 +  "left:: msg \<Rightarrow> msg"
   1.215 +is
   1.216 +  "freeleft"
   1.217 +
   1.218 +lemma [quot_respect]:
   1.219 +  shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
   1.220 +  by (simp add: msgrel_imp_eqv_freeleft)
   1.221 +
   1.222 +lemma left_Nonce [simp]:
   1.223 +  shows "left (Nonce N) = Nonce N"
   1.224 +  by (lifting freeleft.simps(1))
   1.225 +
   1.226 +lemma left_MPair [simp]:
   1.227 +  shows "left (MPair X Y) = X"
   1.228 +  by (lifting freeleft.simps(2))
   1.229 +
   1.230 +lemma left_Crypt [simp]:
   1.231 +  shows "left (Crypt K X) = left X"
   1.232 +  by (lifting freeleft.simps(3))
   1.233 +
   1.234 +lemma left_Decrypt [simp]:
   1.235 +  shows "left (Decrypt K X) = left X"
   1.236 +  by (lifting freeleft.simps(4))
   1.237 +
   1.238 +subsection{*The Abstract Function to Return the Right Part*}
   1.239 +
   1.240 +quotient_definition
   1.241 +  "right:: msg \<Rightarrow> msg"
   1.242 +is
   1.243 +  "freeright"
   1.244 +
   1.245 +text{*Now prove the four equations for @{term right}*}
   1.246 +
   1.247 +lemma [quot_respect]:
   1.248 +  shows "(op \<sim> ===> op \<sim>) freeright freeright"
   1.249 +  by (simp add: msgrel_imp_eqv_freeright)
   1.250 +
   1.251 +lemma right_Nonce [simp]:
   1.252 +  shows "right (Nonce N) = Nonce N"
   1.253 +  by (lifting freeright.simps(1))
   1.254 +
   1.255 +lemma right_MPair [simp]:
   1.256 +  shows "right (MPair X Y) = Y"
   1.257 +  by (lifting freeright.simps(2))
   1.258 +
   1.259 +lemma right_Crypt [simp]:
   1.260 +  shows "right (Crypt K X) = right X"
   1.261 +  by (lifting freeright.simps(3))
   1.262 +
   1.263 +lemma right_Decrypt [simp]:
   1.264 +  shows "right (Decrypt K X) = right X"
   1.265 +  by (lifting freeright.simps(4))
   1.266 +
   1.267 +subsection{*Injectivity Properties of Some Constructors*}
   1.268 +
   1.269 +lemma NONCE_imp_eq:
   1.270 +  shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
   1.271 +  by (drule msgrel_imp_eq_freenonces, simp)
   1.272 +
   1.273 +text{*Can also be proved using the function @{term nonces}*}
   1.274 +lemma Nonce_Nonce_eq [iff]:
   1.275 +  shows "(Nonce m = Nonce n) = (m = n)"
   1.276 +proof
   1.277 +  assume "Nonce m = Nonce n"
   1.278 +  then show "m = n" by (lifting NONCE_imp_eq)
   1.279 +next
   1.280 +  assume "m = n"
   1.281 +  then show "Nonce m = Nonce n" by simp
   1.282 +qed
   1.283 +
   1.284 +lemma MPAIR_imp_eqv_left:
   1.285 +  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
   1.286 +  by (drule msgrel_imp_eqv_freeleft) (simp)
   1.287 +
   1.288 +lemma MPair_imp_eq_left:
   1.289 +  assumes eq: "MPair X Y = MPair X' Y'"
   1.290 +  shows "X = X'"
   1.291 +  using eq by (lifting MPAIR_imp_eqv_left)
   1.292 +
   1.293 +lemma MPAIR_imp_eqv_right:
   1.294 +  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
   1.295 +  by (drule msgrel_imp_eqv_freeright) (simp)
   1.296 +
   1.297 +lemma MPair_imp_eq_right:
   1.298 +  shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
   1.299 +  by (lifting  MPAIR_imp_eqv_right)
   1.300 +
   1.301 +theorem MPair_MPair_eq [iff]:
   1.302 +  shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
   1.303 +  by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
   1.304 +
   1.305 +lemma NONCE_neqv_MPAIR:
   1.306 +  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
   1.307 +  by (auto dest: msgrel_imp_eq_freediscrim)
   1.308 +
   1.309 +theorem Nonce_neq_MPair [iff]:
   1.310 +  shows "Nonce N \<noteq> MPair X Y"
   1.311 +  by (lifting NONCE_neqv_MPAIR)
   1.312 +
   1.313 +text{*Example suggested by a referee*}
   1.314 +
   1.315 +lemma CRYPT_NONCE_neq_NONCE:
   1.316 +  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
   1.317 +  by (auto dest: msgrel_imp_eq_freediscrim)
   1.318 +
   1.319 +theorem Crypt_Nonce_neq_Nonce:
   1.320 +  shows "Crypt K (Nonce M) \<noteq> Nonce N"
   1.321 +  by (lifting CRYPT_NONCE_neq_NONCE)
   1.322 +
   1.323 +text{*...and many similar results*}
   1.324 +lemma CRYPT2_NONCE_neq_NONCE:
   1.325 +  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
   1.326 +  by (auto dest: msgrel_imp_eq_freediscrim)
   1.327 +
   1.328 +theorem Crypt2_Nonce_neq_Nonce:
   1.329 +  shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
   1.330 +  by (lifting CRYPT2_NONCE_neq_NONCE)
   1.331 +
   1.332 +theorem Crypt_Crypt_eq [iff]:
   1.333 +  shows "(Crypt K X = Crypt K X') = (X=X')"
   1.334 +proof
   1.335 +  assume "Crypt K X = Crypt K X'"
   1.336 +  hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
   1.337 +  thus "X = X'" by simp
   1.338 +next
   1.339 +  assume "X = X'"
   1.340 +  thus "Crypt K X = Crypt K X'" by simp
   1.341 +qed
   1.342 +
   1.343 +theorem Decrypt_Decrypt_eq [iff]:
   1.344 +  shows "(Decrypt K X = Decrypt K X') = (X=X')"
   1.345 +proof
   1.346 +  assume "Decrypt K X = Decrypt K X'"
   1.347 +  hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
   1.348 +  thus "X = X'" by simp
   1.349 +next
   1.350 +  assume "X = X'"
   1.351 +  thus "Decrypt K X = Decrypt K X'" by simp
   1.352 +qed
   1.353 +
   1.354 +lemma msg_induct_aux:
   1.355 +  shows "\<lbrakk>\<And>N. P (Nonce N);
   1.356 +          \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
   1.357 +          \<And>K X. P X \<Longrightarrow> P (Crypt K X);
   1.358 +          \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
   1.359 +  by (lifting freemsg.induct)
   1.360 +
   1.361 +lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
   1.362 +  assumes N: "\<And>N. P (Nonce N)"
   1.363 +      and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
   1.364 +      and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
   1.365 +      and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   1.366 +  shows "P msg"
   1.367 +  using N M C D by (rule msg_induct_aux)
   1.368 +
   1.369 +subsection{*The Abstract Discriminator*}
   1.370 +
   1.371 +text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
   1.372 +need this function in order to prove discrimination theorems.*}
   1.373 +
   1.374 +quotient_definition
   1.375 +  "discrim:: msg \<Rightarrow> int"
   1.376 +is
   1.377 +  "freediscrim"
   1.378 +
   1.379 +text{*Now prove the four equations for @{term discrim}*}
   1.380 +
   1.381 +lemma [quot_respect]:
   1.382 +  shows "(op \<sim> ===> op =) freediscrim freediscrim"
   1.383 +  by (auto simp add: msgrel_imp_eq_freediscrim)
   1.384 +
   1.385 +lemma discrim_Nonce [simp]:
   1.386 +  shows "discrim (Nonce N) = 0"
   1.387 +  by (lifting freediscrim.simps(1))
   1.388 +
   1.389 +lemma discrim_MPair [simp]:
   1.390 +  shows "discrim (MPair X Y) = 1"
   1.391 +  by (lifting freediscrim.simps(2))
   1.392 +
   1.393 +lemma discrim_Crypt [simp]:
   1.394 +  shows "discrim (Crypt K X) = discrim X + 2"
   1.395 +  by (lifting freediscrim.simps(3))
   1.396 +
   1.397 +lemma discrim_Decrypt [simp]:
   1.398 +  shows "discrim (Decrypt K X) = discrim X - 2"
   1.399 +  by (lifting freediscrim.simps(4))
   1.400 +
   1.401 +end
   1.402 +