Theory Quotient_Message

(*  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 "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