(* Title: HOL/Quotient_Examples/Quotient_Message.thy Author: Christian Urban Message datatype, based on an older version by Larry Paulson. *) theory Quotient_Message imports Main "~~/src/HOL/Library/Quotient_Syntax" begin subsection‹Defining the Free Algebra› datatype freemsg = NONCE nat | MPAIR freemsg freemsg | CRYPT nat freemsg | DECRYPT nat freemsg inductive msgrel::"freemsg ⇒ freemsg ⇒ bool" (infixl "∼" 50) where CD: "CRYPT K (DECRYPT K X) ∼ X" | DC: "DECRYPT K (CRYPT K X) ∼ X" | NONCE: "NONCE N ∼ NONCE N" | MPAIR: "⟦X ∼ X'; Y ∼ Y'⟧ ⟹ MPAIR X Y ∼ MPAIR X' Y'" | CRYPT: "X ∼ X' ⟹ CRYPT K X ∼ CRYPT K X'" | DECRYPT: "X ∼ X' ⟹ DECRYPT K X ∼ DECRYPT K X'" | SYM: "X ∼ Y ⟹ Y ∼ X" | TRANS: "⟦X ∼ Y; Y ∼ Z⟧ ⟹ X ∼ Z" lemmas msgrel.intros[intro] text‹Proving that it is an equivalence relation› lemma msgrel_refl: "X ∼ X" by (induct X) (auto intro: msgrel.intros) theorem equiv_msgrel: "equivp msgrel" proof (rule equivpI) show "reflp msgrel" by (rule reflpI) (simp add: msgrel_refl) show "symp msgrel" by (rule sympI) (blast intro: msgrel.SYM) show "transp msgrel" by (rule transpI) (blast intro: msgrel.TRANS) qed subsection‹Some Functions on the Free Algebra› subsubsection‹The Set of Nonces› primrec freenonces :: "freemsg ⇒ nat set" where "freenonces (NONCE N) = {N}" | "freenonces (MPAIR X Y) = freenonces X ∪ freenonces Y" | "freenonces (CRYPT K X) = freenonces X" | "freenonces (DECRYPT K X) = freenonces X" theorem msgrel_imp_eq_freenonces: assumes a: "U ∼ V" shows "freenonces U = freenonces V" using a by (induct) (auto) subsubsection‹The Left Projection› text‹A function to return the left part of the top pair in a message. It will be lifted to the initial algebra, to serve as an example of that process.› primrec freeleft :: "freemsg ⇒ freemsg" where "freeleft (NONCE N) = NONCE N" | "freeleft (MPAIR X Y) = X" | "freeleft (CRYPT K X) = freeleft X" | "freeleft (DECRYPT K X) = freeleft X" text‹This theorem lets us prove that the left function respects the equivalence relation. It also helps us prove that MPair (the abstract constructor) is injective› lemma msgrel_imp_eqv_freeleft_aux: shows "freeleft U ∼ freeleft U" by (fact msgrel_refl) theorem msgrel_imp_eqv_freeleft: assumes a: "U ∼ V" shows "freeleft U ∼ freeleft V" using a by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux) subsubsection‹The Right Projection› text‹A function to return the right part of the top pair in a message.› primrec freeright :: "freemsg ⇒ freemsg" where "freeright (NONCE N) = NONCE N" | "freeright (MPAIR X Y) = Y" | "freeright (CRYPT K X) = freeright X" | "freeright (DECRYPT K X) = freeright X" text‹This theorem lets us prove that the right function respects the equivalence relation. It also helps us prove that MPair (the abstract constructor) is injective› lemma msgrel_imp_eqv_freeright_aux: shows "freeright U ∼ freeright U" by (fact msgrel_refl) theorem msgrel_imp_eqv_freeright: assumes a: "U ∼ V" shows "freeright U ∼ freeright V" using a by (induct) (auto intro: msgrel_imp_eqv_freeright_aux) subsubsection‹The Discriminator for Constructors› text‹A function to distinguish nonces, mpairs and encryptions› primrec freediscrim :: "freemsg ⇒ int" where "freediscrim (NONCE N) = 0" | "freediscrim (MPAIR X Y) = 1" | "freediscrim (CRYPT K X) = freediscrim X + 2" | "freediscrim (DECRYPT K X) = freediscrim X - 2" text‹This theorem helps us prove @{term "Nonce N ≠ MPair X Y"}› theorem msgrel_imp_eq_freediscrim: assumes a: "U ∼ V" shows "freediscrim U = freediscrim V" using a by (induct) (auto) subsection‹The Initial Algebra: A Quotiented Message Type› quotient_type msg = freemsg / msgrel by (rule equiv_msgrel) text‹The abstract message constructors› quotient_definition "Nonce :: nat ⇒ msg" is "NONCE" done quotient_definition "MPair :: msg ⇒ msg ⇒ msg" is "MPAIR" by (rule MPAIR) quotient_definition "Crypt :: nat ⇒ msg ⇒ msg" is "CRYPT" by (rule CRYPT) quotient_definition "Decrypt :: nat ⇒ msg ⇒ msg" is "DECRYPT" by (rule DECRYPT) text‹Establishing these two equations is the point of the whole exercise› theorem CD_eq [simp]: shows "Crypt K (Decrypt K X) = X" by (lifting CD) theorem DC_eq [simp]: shows "Decrypt K (Crypt K X) = X" by (lifting DC) subsection‹The Abstract Function to Return the Set of Nonces› quotient_definition "nonces:: msg ⇒ nat set" is "freenonces" by (rule msgrel_imp_eq_freenonces) text‹Now prove the four equations for @{term nonces}› lemma nonces_Nonce [simp]: shows "nonces (Nonce N) = {N}" by (lifting freenonces.simps(1)) lemma nonces_MPair [simp]: shows "nonces (MPair X Y) = nonces X ∪ nonces Y" by (lifting freenonces.simps(2)) lemma nonces_Crypt [simp]: shows "nonces (Crypt K X) = nonces X" by (lifting freenonces.simps(3)) lemma nonces_Decrypt [simp]: shows "nonces (Decrypt K X) = nonces X" by (lifting freenonces.simps(4)) subsection‹The Abstract Function to Return the Left Part› quotient_definition "left:: msg ⇒ msg" is "freeleft" by (rule msgrel_imp_eqv_freeleft) lemma left_Nonce [simp]: shows "left (Nonce N) = Nonce N" by (lifting freeleft.simps(1)) lemma left_MPair [simp]: shows "left (MPair X Y) = X" by (lifting freeleft.simps(2)) lemma left_Crypt [simp]: shows "left (Crypt K X) = left X" by (lifting freeleft.simps(3)) lemma left_Decrypt [simp]: shows "left (Decrypt K X) = left X" by (lifting freeleft.simps(4)) subsection‹The Abstract Function to Return the Right Part› quotient_definition "right:: msg ⇒ msg" is "freeright" by (rule msgrel_imp_eqv_freeright) text‹Now prove the four equations for @{term right}› lemma right_Nonce [simp]: shows "right (Nonce N) = Nonce N" by (lifting freeright.simps(1)) lemma right_MPair [simp]: shows "right (MPair X Y) = Y" by (lifting freeright.simps(2)) lemma right_Crypt [simp]: shows "right (Crypt K X) = right X" by (lifting freeright.simps(3)) lemma right_Decrypt [simp]: shows "right (Decrypt K X) = right X" by (lifting freeright.simps(4)) subsection‹Injectivity Properties of Some Constructors› text‹Can also be proved using the function @{term nonces}› lemma Nonce_Nonce_eq [iff]: shows "(Nonce m = Nonce n) = (m = n)" proof assume "Nonce m = Nonce n" then show "m = n" by (descending) (drule msgrel_imp_eq_freenonces, simp) next assume "m = n" then show "Nonce m = Nonce n" by simp qed lemma MPair_imp_eq_left: assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'" using eq by (descending) (drule msgrel_imp_eqv_freeleft, simp) lemma MPair_imp_eq_right: shows "MPair X Y = MPair X' Y' ⟹ Y = Y'" by (descending) (drule msgrel_imp_eqv_freeright, simp) theorem MPair_MPair_eq [iff]: shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" by (blast dest: MPair_imp_eq_left MPair_imp_eq_right) theorem Nonce_neq_MPair [iff]: shows "Nonce N ≠ MPair X Y" by (descending) (auto dest: msgrel_imp_eq_freediscrim) text‹Example suggested by a referee› theorem Crypt_Nonce_neq_Nonce: shows "Crypt K (Nonce M) ≠ Nonce N" by (descending) (auto dest: msgrel_imp_eq_freediscrim) text‹...and many similar results› theorem Crypt2_Nonce_neq_Nonce: shows "Crypt K (Crypt K' (Nonce M)) ≠ Nonce N" by (descending) (auto dest: msgrel_imp_eq_freediscrim) theorem Crypt_Crypt_eq [iff]: shows "(Crypt K X = Crypt K X') = (X=X')" proof assume "Crypt K X = Crypt K X'" hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp thus "X = X'" by simp next assume "X = X'" thus "Crypt K X = Crypt K X'" by simp qed theorem Decrypt_Decrypt_eq [iff]: shows "(Decrypt K X = Decrypt K X') = (X=X')" proof assume "Decrypt K X = Decrypt K X'" hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp thus "X = X'" by simp next assume "X = X'" thus "Decrypt K X = Decrypt K X'" by simp qed lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]: assumes N: "⋀N. P (Nonce N)" and M: "⋀X Y. ⟦P X; P Y⟧ ⟹ P (MPair X Y)" and C: "⋀K X. P X ⟹ P (Crypt K X)" and D: "⋀K X. P X ⟹ P (Decrypt K X)" shows "P msg" using N M C D by (descending) (auto intro: freemsg.induct) subsection‹The Abstract Discriminator› text‹However, as ‹Crypt_Nonce_neq_Nonce› above illustrates, we don't need this function in order to prove discrimination theorems.› quotient_definition "discrim:: msg ⇒ int" is "freediscrim" by (rule msgrel_imp_eq_freediscrim) text‹Now prove the four equations for @{term discrim}› lemma discrim_Nonce [simp]: shows "discrim (Nonce N) = 0" by (lifting freediscrim.simps(1)) lemma discrim_MPair [simp]: shows "discrim (MPair X Y) = 1" by (lifting freediscrim.simps(2)) lemma discrim_Crypt [simp]: shows "discrim (Crypt K X) = discrim X + 2" by (lifting freediscrim.simps(3)) lemma discrim_Decrypt [simp]: shows "discrim (Decrypt K X) = discrim X - 2" by (lifting freediscrim.simps(4)) end