# Theory QuoDataType

(*  Title:      HOL/Induct/QuoDataType.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section‹Defining an Initial Algebra by Quotienting a Free Algebra›

text ‹For Lawrence Paulson's paper Defining functions on equivalence classes''
\emph{ACM Transactions on Computational Logic} \textbf{7}:40 (2006), 658--675,
illustrating bare-bones quotient constructions. Any comparison using lifting and transfer
should be done in a separate theory.›

theory QuoDataType imports Main begin

subsection‹Defining the Free Algebra›

text‹Messages with encryption and decryption as free constructors.›
datatype
freemsg = NONCE  nat
| MPAIR  freemsg freemsg
| CRYPT  nat freemsg
| DECRYPT  nat freemsg

text‹The equivalence relation, which makes encryption and decryption inverses
provided the keys are the same.

The first two rules are the desired equations. The next four rules
make the equations applicable to subterms. The last two rules are symmetry
and transitivity.›

inductive_set
msgrel :: "(freemsg * freemsg) set"
and msg_rel :: "[freemsg, freemsg] => bool"  (infixl "∼" 50)
where
"X ∼ Y == (X,Y) ∈ msgrel"
| 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"

text‹Proving that it is an equivalence relation›

lemma msgrel_refl: "X ∼ X"
by (induct X) (blast intro: msgrel.intros)+

theorem equiv_msgrel: "equiv UNIV msgrel"
proof (rule equivI)
show "refl msgrel" by (simp add: refl_on_def msgrel_refl)
show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
qed

subsection‹Some Functions on the Free Algebra›

subsubsection‹The Set of Nonces›

text‹A function to return the set of nonces present in a message.  It will
be lifted to the initial algebra, to serve as an example of that process.›
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"

text‹This theorem lets us prove that the nonces function respects the
equivalence relation.  It also helps us prove that Nonce
(the abstract constructor) is injective›
theorem msgrel_imp_eq_freenonces: "U ∼ V ⟹ freenonces U = freenonces V"
by (induct set: msgrel) 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›
theorem msgrel_imp_eqv_freeleft:
"U ∼ V ⟹ freeleft U ∼ freeleft V"
by (induct set: msgrel) (auto intro: msgrel.intros)

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›
theorem msgrel_imp_eqv_freeright:
"U ∼ V ⟹ freeright U ∼ freeright V"
by (induct set: msgrel) (auto intro: msgrel.intros)

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:
"U ∼ V ⟹ freediscrim U = freediscrim V"
by (induct set: msgrel) auto

subsection‹The Initial Algebra: A Quotiented Message Type›

definition "Msg = UNIV//msgrel"

typedef msg = Msg
morphisms Rep_Msg Abs_Msg
unfolding Msg_def by (auto simp add: quotient_def)

text‹The abstract message constructors›
definition
Nonce :: "nat ⇒ msg" where
"Nonce N = Abs_Msg(msgrel{NONCE N})"

definition
MPair :: "[msg,msg] ⇒ msg" where
"MPair X Y =
Abs_Msg (⋃U ∈ Rep_Msg X. ⋃V ∈ Rep_Msg Y. msgrel{MPAIR U V})"

definition
Crypt :: "[nat,msg] ⇒ msg" where
"Crypt K X =
Abs_Msg (⋃U ∈ Rep_Msg X. msgrel{CRYPT K U})"

definition
Decrypt :: "[nat,msg] ⇒ msg" where
"Decrypt K X =
Abs_Msg (⋃U ∈ Rep_Msg X. msgrel{DECRYPT K U})"

text‹Reduces equality of equivalence classes to the \<^term>‹msgrel› relation:
\<^term>‹(msgrel  {x} = msgrel  {y}) = ((x,y) ∈ msgrel)››
lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]

declare equiv_msgrel_iff [simp]

text‹All equivalence classes belong to set of representatives›
lemma [simp]: "msgrel{U} ∈ Msg"
by (auto simp add: Msg_def quotient_def intro: msgrel_refl)

lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
by (meson Abs_Msg_inject inj_onI)

text‹Reduces equality on abstractions to equality on representatives›
declare inj_on_Abs_Msg [THEN inj_on_eq_iff, simp]

declare Abs_Msg_inverse [simp]

subsubsection‹Characteristic Equations for the Abstract Constructors›

lemma MPair: "MPair (Abs_Msg(msgrel{U})) (Abs_Msg(msgrel{V})) =
Abs_Msg (msgrel{MPAIR U V})"
proof -
have "(λU V. msgrel  {MPAIR U V}) respects2 msgrel"
by (auto simp add: congruent2_def msgrel.MPAIR)
thus ?thesis
by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
qed

lemma Crypt: "Crypt K (Abs_Msg(msgrel{U})) = Abs_Msg (msgrel{CRYPT K U})"
proof -
have "(λU. msgrel  {CRYPT K U}) respects msgrel"
by (auto simp add: congruent_def msgrel.CRYPT)
thus ?thesis
by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
qed

lemma Decrypt:
"Decrypt K (Abs_Msg(msgrel{U})) = Abs_Msg (msgrel{DECRYPT K U})"
proof -
have "(λU. msgrel  {DECRYPT K U}) respects msgrel"
by (auto simp add: congruent_def msgrel.DECRYPT)
thus ?thesis
by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
qed

text‹Case analysis on the representation of a msg as an equivalence class.›
lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]:
"(⋀U. z = Abs_Msg (msgrel  {U}) ⟹ P) ⟹ P"
by (metis Abs_Msg_cases Msg_def quotientE)

text‹Establishing these two equations is the point of the whole exercise›
theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
by (cases X, simp add: Crypt Decrypt CD)

theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
by (cases X, simp add: Crypt Decrypt DC)

subsection‹The Abstract Function to Return the Set of Nonces›

definition
nonces :: "msg ⇒ nat set" where
"nonces X = (⋃U ∈ Rep_Msg X. freenonces U)"

lemma nonces_congruent: "freenonces respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eq_freenonces)

text‹Now prove the four equations for \<^term>‹nonces››

lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}"
UN_equiv_class [OF equiv_msgrel nonces_congruent])

lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X ∪ nonces Y"
proof -
have "⋀U V. ⟦X = Abs_Msg (msgrel  {U}); Y = Abs_Msg (msgrel  {V})⟧
⟹ nonces (MPair X Y) = nonces X ∪ nonces Y"
UN_equiv_class [OF equiv_msgrel nonces_congruent])
then show ?thesis
by (meson eq_Abs_Msg)
qed

lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X"
proof -
have "⋀U. X = Abs_Msg (msgrel  {U}) ⟹ nonces (Crypt K X) = nonces X"
by (simp add: nonces_def Crypt UN_equiv_class [OF equiv_msgrel nonces_congruent])
then show ?thesis
by (meson eq_Abs_Msg)
qed

lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
proof -
have "⋀U. X = Abs_Msg (msgrel  {U}) ⟹ nonces (Decrypt K X) = nonces X"
by (simp add: nonces_def Decrypt UN_equiv_class [OF equiv_msgrel nonces_congruent])
then show ?thesis
by (meson eq_Abs_Msg)
qed

subsection‹The Abstract Function to Return the Left Part›

definition
left :: "msg ⇒ msg"
where "left X = Abs_Msg (⋃U ∈ Rep_Msg X. msgrel{freeleft U})"

lemma left_congruent: "(λU. msgrel  {freeleft U}) respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eqv_freeleft)

text‹Now prove the four equations for \<^term>‹left››

lemma left_Nonce [simp]: "left (Nonce N) = Nonce N"
UN_equiv_class [OF equiv_msgrel left_congruent])

lemma left_MPair [simp]: "left (MPair X Y) = X"
by (cases X, cases Y) (simp add: left_def MPair UN_equiv_class [OF equiv_msgrel left_congruent])

lemma left_Crypt [simp]: "left (Crypt K X) = left X"
by (cases X) (simp add: left_def Crypt UN_equiv_class [OF equiv_msgrel left_congruent])

lemma left_Decrypt [simp]: "left (Decrypt K X) = left X"
by (metis CD_eq left_Crypt)

subsection‹The Abstract Function to Return the Right Part›

definition
right :: "msg ⇒ msg"
where "right X = Abs_Msg (⋃U ∈ Rep_Msg X. msgrel{freeright U})"

lemma right_congruent: "(λU. msgrel  {freeright U}) respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eqv_freeright)

text‹Now prove the four equations for \<^term>‹right››

lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"
UN_equiv_class [OF equiv_msgrel right_congruent])

lemma right_MPair [simp]: "right (MPair X Y) = Y"
by (cases X, cases Y) (simp add: right_def MPair UN_equiv_class [OF equiv_msgrel right_congruent])

lemma right_Crypt [simp]: "right (Crypt K X) = right X"
by (cases X) (simp add: right_def Crypt UN_equiv_class [OF equiv_msgrel right_congruent])

lemma right_Decrypt [simp]: "right (Decrypt K X) = right X"
by (metis CD_eq right_Crypt)

subsection‹Injectivity Properties of Some Constructors›

lemma NONCE_imp_eq: "NONCE m ∼ NONCE n ⟹ m = n"
by (drule msgrel_imp_eq_freenonces, simp)

text‹Can also be proved using the function \<^term>‹nonces››
lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"
by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)

lemma MPAIR_imp_eqv_left: "MPAIR X Y ∼ MPAIR X' Y' ⟹ X ∼ X'"
by (drule msgrel_imp_eqv_freeleft, simp)

lemma MPair_imp_eq_left:
assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'"
proof -
from eq
have "left (MPair X Y) = left (MPair X' Y')" by simp
thus ?thesis by simp
qed

lemma MPAIR_imp_eqv_right: "MPAIR X Y ∼ MPAIR X' Y' ⟹ Y ∼ Y'"
by (drule msgrel_imp_eqv_freeright, simp)

lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' ⟹ Y = Y'"
by (metis right_MPair)

theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)

lemma NONCE_neqv_MPAIR: "NONCE m ∼ MPAIR X Y ⟹ False"
by (drule msgrel_imp_eq_freediscrim, simp)

theorem Nonce_neq_MPair [iff]: "Nonce N ≠ MPair X Y"
by (cases X, cases Y) (use MPair NONCE_neqv_MPAIR Nonce_def in fastforce)

text‹Example suggested by a referee›
theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) ≠ Nonce N"
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)

text‹...and many similar results›
theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) ≠ Nonce N"
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)

theorem Crypt_Crypt_eq [iff]: "(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]: "(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"
proof (cases msg)
case (Abs_Msg U)
have "P (Abs_Msg (msgrel  {U}))"
proof (induct U)
case (NONCE N)
with N show ?case by (simp add: Nonce_def)
next
case (MPAIR X Y)
with M [of "Abs_Msg (msgrel  {X})" "Abs_Msg (msgrel  {Y})"]
show ?case by (simp add: MPair)
next
case (CRYPT K X)
with C [of "Abs_Msg (msgrel  {X})"]
show ?case by (simp add: Crypt)
next
case (DECRYPT K X)
with D [of "Abs_Msg (msgrel  {X})"]
show ?case by (simp add: Decrypt)
qed
with Abs_Msg show ?thesis by (simp only:)
qed

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.›

definition
discrim :: "msg ⇒ int" where
"discrim X = the_elem (⋃U ∈ Rep_Msg X. {freediscrim U})"

lemma discrim_congruent: "(λU. {freediscrim U}) respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eq_freediscrim)

text‹Now prove the four equations for \<^term>‹discrim››

lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0"
UN_equiv_class [OF equiv_msgrel discrim_congruent])

lemma discrim_MPair [simp]: "discrim (MPair X Y) = 1"
proof -
have "⋀U V. discrim (MPair (Abs_Msg (msgrel  {U})) (Abs_Msg (msgrel  {V}))) = 1"
by (simp add: discrim_def MPair  UN_equiv_class [OF equiv_msgrel discrim_congruent])
then show ?thesis
by (metis eq_Abs_Msg)
qed

lemma discrim_Crypt [simp]: "discrim (Crypt K X) = discrim X + 2"
by (cases X) (use Crypt UN_equiv_class discrim_congruent discrim_def equiv_msgrel in fastforce)

lemma discrim_Decrypt [simp]: "discrim (Decrypt K X) = discrim X - 2"
by (cases X) (use Decrypt UN_equiv_class discrim_congruent discrim_def equiv_msgrel in fastforce)

end