--- a/Quot/Examples/Larry.thy Fri Dec 11 08:28:41 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,392 +0,0 @@
-theory Larry
-imports Main "../QuotMain"
-begin
-
-subsection{*Defining the Free Algebra*}
-
-datatype
- freemsg = NONCE nat
- | MPAIR freemsg freemsg
- | CRYPT nat freemsg
- | DECRYPT nat freemsg
-
-inductive
- msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
-where
- CD: "CRYPT K (DECRYPT K X) \<sim> X"
-| DC: "DECRYPT K (CRYPT K X) \<sim> X"
-| NONCE: "NONCE N \<sim> NONCE N"
-| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
-| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
-| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
-| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
-| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
-
-lemmas msgrel.intros[intro]
-
-text{*Proving that it is an equivalence relation*}
-
-lemma msgrel_refl: "X \<sim> X"
-by (induct X, (blast intro: msgrel.intros)+)
-
-theorem equiv_msgrel: "equivp msgrel"
-proof (rule equivpI)
- show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
- show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
- show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
-qed
-
-subsection{*Some Functions on the Free Algebra*}
-
-subsubsection{*The Set of Nonces*}
-
-fun
- freenonces :: "freemsg \<Rightarrow> nat set"
-where
- "freenonces (NONCE N) = {N}"
-| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
-| "freenonces (CRYPT K X) = freenonces X"
-| "freenonces (DECRYPT K X) = freenonces X"
-
-theorem msgrel_imp_eq_freenonces:
- assumes a: "U \<sim> 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 algrebra, to serve as an example of that process.*}
-fun
- freeleft :: "freemsg \<Rightarrow> 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 \<sim> freeleft U"
-by (induct rule: freeleft.induct) (auto)
-
-theorem msgrel_imp_eqv_freeleft:
- assumes a: "U \<sim> V"
- shows "freeleft U \<sim> 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.*}
-fun
- freeright :: "freemsg \<Rightarrow> 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 \<sim> freeright U"
-by (induct rule: freeright.induct) (auto)
-
-theorem msgrel_imp_eqv_freeright:
- assumes a: "U \<sim> V"
- shows "freeright U \<sim> 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*}
-fun
- freediscrim :: "freemsg \<Rightarrow> 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 \<noteq> MPair X Y"}*}
-theorem msgrel_imp_eq_freediscrim:
- assumes a: "U \<sim> V"
- shows "freediscrim U = freediscrim V"
-using a by (induct, auto)
-
-
-subsection{*The Initial Algebra: A Quotiented Message Type*}
-
-quotient msg = freemsg / msgrel
- by (rule equiv_msgrel)
-
-text{*The abstract message constructors*}
-
-quotient_def
- Nonce::"Nonce :: nat \<Rightarrow> msg"
-where
- "NONCE"
-
-quotient_def
- MPair::"MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-where
- "MPAIR"
-
-quotient_def
- Crypt::"Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-where
- "CRYPT"
-
-quotient_def
- Decrypt::"Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-where
- "DECRYPT"
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
-by (auto intro: CRYPT)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
-by (auto intro: DECRYPT)
-
-text{*Establishing these two equations is the point of the whole exercise*}
-theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
-by (lifting CD)
-
-theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
-by (lifting DC)
-
-subsection{*The Abstract Function to Return the Set of Nonces*}
-
-quotient_def
- nonces :: "nounces:: msg \<Rightarrow> nat set"
-where
- "freenonces"
-
-text{*Now prove the four equations for @{term nonces}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freenonces freenonces"
-by (simp add: msgrel_imp_eq_freenonces)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim>) NONCE NONCE"
-by (simp add: NONCE)
-
-lemma nonces_Nonce [simp]:
- shows "nonces (Nonce N) = {N}"
-by (lifting freenonces.simps(1))
-
-lemma [quot_respect]:
- shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
-by (simp add: MPAIR)
-
-lemma nonces_MPair [simp]:
- shows "nonces (MPair X Y) = nonces X \<union> 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]: "nonces (Decrypt K X) = nonces X"
-by (lifting freenonces.simps(4))
-
-subsection{*The Abstract Function to Return the Left Part*}
-
-quotient_def
- left :: "left:: msg \<Rightarrow> msg"
-where
- "freeleft"
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
-by (simp add: 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_def
- right :: "right:: msg \<Rightarrow> msg"
-where
- "freeright"
-
-text{*Now prove the four equations for @{term right}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeright freeright"
-by (simp add: msgrel_imp_eqv_freeright)
-
-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*}
-
-lemma NONCE_imp_eq:
- shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
-by (drule msgrel_imp_eq_freenonces, simp)
-
-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 (lifting NONCE_imp_eq)
-next
- assume "m = n"
- then show "Nonce m = Nonce n" by simp
-qed
-
-lemma MPAIR_imp_eqv_left:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
-by (drule msgrel_imp_eqv_freeleft) (simp)
-
-lemma MPair_imp_eq_left:
- assumes eq: "MPair X Y = MPair X' Y'"
- shows "X = X'"
-using eq by (lifting MPAIR_imp_eqv_left)
-
-lemma MPAIR_imp_eqv_right:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
-by (drule msgrel_imp_eqv_freeright) (simp)
-
-lemma MPair_imp_eq_right:
- shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
-by (lifting MPAIR_imp_eqv_right)
-
-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)
-
-lemma NONCE_neqv_MPAIR:
- shows "\<not>(NONCE m \<sim> MPAIR X Y)"
-by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Nonce_neq_MPair [iff]:
- shows "Nonce N \<noteq> MPair X Y"
-by (lifting NONCE_neqv_MPAIR)
-
-text{*Example suggested by a referee*}
-
-lemma CRYPT_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
-by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Crypt_Nonce_neq_Nonce:
- shows "Crypt K (Nonce M) \<noteq> Nonce N"
-by (lifting CRYPT_NONCE_neq_NONCE)
-
-text{*...and many similar results*}
-lemma CRYPT2_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
-by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Crypt2_Nonce_neq_Nonce:
- shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
-by (lifting CRYPT2_NONCE_neq_NONCE)
-
-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_aux:
- shows "\<lbrakk>\<And>N. P (Nonce N);
- \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
- \<And>K X. P X \<Longrightarrow> P (Crypt K X);
- \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
-by (lifting freemsg.induct)
-
-lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
- assumes N: "\<And>N. P (Nonce N)"
- and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
- and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
- and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
- shows "P msg"
-using N M C D by (rule msg_induct_aux)
-
-subsection{*The Abstract Discriminator*}
-
-text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
-need this function in order to prove discrimination theorems.*}
-
-quotient_def
- discrim :: "discrim:: msg \<Rightarrow> int"
-where
- "freediscrim"
-
-text{*Now prove the four equations for @{term discrim}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freediscrim freediscrim"
-by (auto simp add: msgrel_imp_eq_freediscrim)
-
-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
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Examples/LarryDatatype.thy Fri Dec 11 10:57:46 2009 +0100
@@ -0,0 +1,392 @@
+theory LarryDataType
+imports Main "../QuotMain"
+begin
+
+subsection{*Defining the Free Algebra*}
+
+datatype
+ freemsg = NONCE nat
+ | MPAIR freemsg freemsg
+ | CRYPT nat freemsg
+ | DECRYPT nat freemsg
+
+inductive
+ msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
+where
+ CD: "CRYPT K (DECRYPT K X) \<sim> X"
+| DC: "DECRYPT K (CRYPT K X) \<sim> X"
+| NONCE: "NONCE N \<sim> NONCE N"
+| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
+| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
+| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
+| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
+| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
+
+lemmas msgrel.intros[intro]
+
+text{*Proving that it is an equivalence relation*}
+
+lemma msgrel_refl: "X \<sim> X"
+by (induct X, (blast intro: msgrel.intros)+)
+
+theorem equiv_msgrel: "equivp msgrel"
+proof (rule equivpI)
+ show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
+ show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
+ show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
+qed
+
+subsection{*Some Functions on the Free Algebra*}
+
+subsubsection{*The Set of Nonces*}
+
+fun
+ freenonces :: "freemsg \<Rightarrow> nat set"
+where
+ "freenonces (NONCE N) = {N}"
+| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
+| "freenonces (CRYPT K X) = freenonces X"
+| "freenonces (DECRYPT K X) = freenonces X"
+
+theorem msgrel_imp_eq_freenonces:
+ assumes a: "U \<sim> 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 algrebra, to serve as an example of that process.*}
+fun
+ freeleft :: "freemsg \<Rightarrow> 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 \<sim> freeleft U"
+by (induct rule: freeleft.induct) (auto)
+
+theorem msgrel_imp_eqv_freeleft:
+ assumes a: "U \<sim> V"
+ shows "freeleft U \<sim> 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.*}
+fun
+ freeright :: "freemsg \<Rightarrow> 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 \<sim> freeright U"
+by (induct rule: freeright.induct) (auto)
+
+theorem msgrel_imp_eqv_freeright:
+ assumes a: "U \<sim> V"
+ shows "freeright U \<sim> 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*}
+fun
+ freediscrim :: "freemsg \<Rightarrow> 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 \<noteq> MPair X Y"}*}
+theorem msgrel_imp_eq_freediscrim:
+ assumes a: "U \<sim> V"
+ shows "freediscrim U = freediscrim V"
+using a by (induct, auto)
+
+
+subsection{*The Initial Algebra: A Quotiented Message Type*}
+
+quotient msg = freemsg / msgrel
+ by (rule equiv_msgrel)
+
+text{*The abstract message constructors*}
+
+quotient_def
+ Nonce::"Nonce :: nat \<Rightarrow> msg"
+where
+ "NONCE"
+
+quotient_def
+ MPair::"MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+where
+ "MPAIR"
+
+quotient_def
+ Crypt::"Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+where
+ "CRYPT"
+
+quotient_def
+ Decrypt::"Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+where
+ "DECRYPT"
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
+by (auto intro: CRYPT)
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
+by (auto intro: DECRYPT)
+
+text{*Establishing these two equations is the point of the whole exercise*}
+theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
+by (lifting CD)
+
+theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
+by (lifting DC)
+
+subsection{*The Abstract Function to Return the Set of Nonces*}
+
+quotient_def
+ nonces :: "nounces:: msg \<Rightarrow> nat set"
+where
+ "freenonces"
+
+text{*Now prove the four equations for @{term nonces}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op =) freenonces freenonces"
+by (simp add: msgrel_imp_eq_freenonces)
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim>) NONCE NONCE"
+by (simp add: NONCE)
+
+lemma nonces_Nonce [simp]:
+ shows "nonces (Nonce N) = {N}"
+by (lifting freenonces.simps(1))
+
+lemma [quot_respect]:
+ shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
+by (simp add: MPAIR)
+
+lemma nonces_MPair [simp]:
+ shows "nonces (MPair X Y) = nonces X \<union> 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]: "nonces (Decrypt K X) = nonces X"
+by (lifting freenonces.simps(4))
+
+subsection{*The Abstract Function to Return the Left Part*}
+
+quotient_def
+ left :: "left:: msg \<Rightarrow> msg"
+where
+ "freeleft"
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
+by (simp add: 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_def
+ right :: "right:: msg \<Rightarrow> msg"
+where
+ "freeright"
+
+text{*Now prove the four equations for @{term right}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op \<sim>) freeright freeright"
+by (simp add: msgrel_imp_eqv_freeright)
+
+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*}
+
+lemma NONCE_imp_eq:
+ shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
+by (drule msgrel_imp_eq_freenonces, simp)
+
+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 (lifting NONCE_imp_eq)
+next
+ assume "m = n"
+ then show "Nonce m = Nonce n" by simp
+qed
+
+lemma MPAIR_imp_eqv_left:
+ shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
+by (drule msgrel_imp_eqv_freeleft) (simp)
+
+lemma MPair_imp_eq_left:
+ assumes eq: "MPair X Y = MPair X' Y'"
+ shows "X = X'"
+using eq by (lifting MPAIR_imp_eqv_left)
+
+lemma MPAIR_imp_eqv_right:
+ shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
+by (drule msgrel_imp_eqv_freeright) (simp)
+
+lemma MPair_imp_eq_right:
+ shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
+by (lifting MPAIR_imp_eqv_right)
+
+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)
+
+lemma NONCE_neqv_MPAIR:
+ shows "\<not>(NONCE m \<sim> MPAIR X Y)"
+by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Nonce_neq_MPair [iff]:
+ shows "Nonce N \<noteq> MPair X Y"
+by (lifting NONCE_neqv_MPAIR)
+
+text{*Example suggested by a referee*}
+
+lemma CRYPT_NONCE_neq_NONCE:
+ shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
+by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Crypt_Nonce_neq_Nonce:
+ shows "Crypt K (Nonce M) \<noteq> Nonce N"
+by (lifting CRYPT_NONCE_neq_NONCE)
+
+text{*...and many similar results*}
+lemma CRYPT2_NONCE_neq_NONCE:
+ shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
+by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Crypt2_Nonce_neq_Nonce:
+ shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
+by (lifting CRYPT2_NONCE_neq_NONCE)
+
+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_aux:
+ shows "\<lbrakk>\<And>N. P (Nonce N);
+ \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
+ \<And>K X. P X \<Longrightarrow> P (Crypt K X);
+ \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
+by (lifting freemsg.induct)
+
+lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
+ assumes N: "\<And>N. P (Nonce N)"
+ and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
+ and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
+ and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
+ shows "P msg"
+using N M C D by (rule msg_induct_aux)
+
+subsection{*The Abstract Discriminator*}
+
+text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
+need this function in order to prove discrimination theorems.*}
+
+quotient_def
+ discrim :: "discrim:: msg \<Rightarrow> int"
+where
+ "freediscrim"
+
+text{*Now prove the four equations for @{term discrim}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op =) freediscrim freediscrim"
+by (auto simp add: msgrel_imp_eq_freediscrim)
+
+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
+