# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272524795 -7200
# Node ID 3909002beca5afb8b2fb6dffe1052f43739c6fc4
# Parent  a294e4ebe0a3ef7dc3dc9c0d547c0a980fe48252
Tuning the quotient examples

diff -r a294e4ebe0a3 -r 3909002beca5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Apr 28 17:42:37 2010 +0200
+++ b/src/HOL/IsaMakefile	Thu Apr 29 09:06:35 2010 +0200
@@ -1295,8 +1295,8 @@
 HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
 
 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL				\
-  Quotient_Examples/FSet.thy                                            \
-  Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy
+  Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy         \
+  Quotient_Examples/Quotient_Message.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
 
 
diff -r a294e4ebe0a3 -r 3909002beca5 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Wed Apr 28 17:42:37 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Apr 29 09:06:35 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Quotient_Examples/Quotient.thy
+(*  Title:      HOL/Quotient_Examples/FSet.thy
     Author:     Cezary Kaliszyk, TU Munich
     Author:     Christian Urban, TU Munich
 
diff -r a294e4ebe0a3 -r 3909002beca5 src/HOL/Quotient_Examples/LarryDatatype.thy
--- a/src/HOL/Quotient_Examples/LarryDatatype.thy	Wed Apr 28 17:42:37 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,394 +0,0 @@
-theory LarryDatatype
-imports Main Quotient_Syntax
-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_type msg = freemsg / msgrel
-  by (rule equiv_msgrel)
-
-text{*The abstract message constructors*}
-
-quotient_definition
-  "Nonce :: nat \<Rightarrow> msg"
-is
-  "NONCE"
-
-quotient_definition
-  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-is
-  "MPAIR"
-
-quotient_definition
-  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
-  "CRYPT"
-
-quotient_definition
-  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
-  "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]: 
-  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 \<Rightarrow> nat set"
-is
-  "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]: 
-  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 \<Rightarrow> msg"
-is
-  "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_definition
-  "right:: msg \<Rightarrow> msg"
-is
-  "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_definition
-  "discrim:: msg \<Rightarrow> int"
-is
-  "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
-
diff -r a294e4ebe0a3 -r 3909002beca5 src/HOL/Quotient_Examples/LarryInt.thy
--- a/src/HOL/Quotient_Examples/LarryInt.thy	Wed Apr 28 17:42:37 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,395 +0,0 @@
-
-header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
-
-theory LarryInt
-imports Main Quotient_Product
-begin
-
-fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
-where
-  "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type int = "nat \<times> nat" / intrel
-  by (auto simp add: equivp_def expand_fun_eq)
-
-instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
-begin
-
-quotient_definition
-  Zero_int_def: "0::int" is "(0::nat, 0::nat)"
-
-quotient_definition
-  One_int_def: "1::int" is "(1::nat, 0::nat)"
-
-definition
-  "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
-
-quotient_definition
-  "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
-is
-  "add_raw"
-
-definition
-  "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
-
-quotient_definition
-  "uminus :: int \<Rightarrow> int" 
-is
-  "uminus_raw"
-
-fun
-  mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
-where
-  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
-
-quotient_definition
-  "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
-is
-  "mult_raw"
-
-definition
-  "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
-
-quotient_definition 
-  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
-is
-  "le_raw"
-
-definition
-  less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
-
-definition
-  diff_int_def:  "z - (w::int) \<equiv> z + (-w)"
-
-instance ..
-
-end
-
-subsection{*Construction of the Integers*}
-
-lemma zminus_zminus_raw:
-  "uminus_raw (uminus_raw z) = z"
-  by (cases z) (simp add: uminus_raw_def)
-
-lemma [quot_respect]:
-  shows "(intrel ===> intrel) uminus_raw uminus_raw"
-  by (simp add: uminus_raw_def)
-  
-lemma zminus_zminus:
-  fixes z::"int"
-  shows "- (- z) = z"
-  by(lifting zminus_zminus_raw)
-
-lemma zminus_0_raw:
-  shows "uminus_raw (0, 0) = (0, 0::nat)"
-  by (simp add: uminus_raw_def)
-
-lemma zminus_0: 
-  shows "- 0 = (0::int)"
-  by (lifting zminus_0_raw)
-
-subsection{*Integer Addition*}
-
-lemma zminus_zadd_distrib_raw:
-  shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
-by (cases z, cases w)
-   (auto simp add: add_raw_def uminus_raw_def)
-
-lemma [quot_respect]:
-  shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
-by (simp add: add_raw_def)
-
-lemma zminus_zadd_distrib: 
-  fixes z w::"int"
-  shows "- (z + w) = (- z) + (- w)"
-  by(lifting zminus_zadd_distrib_raw)
-
-lemma zadd_commute_raw:
-  shows "add_raw z w = add_raw w z"
-by (cases z, cases w)
-   (simp add: add_raw_def)
-
-lemma zadd_commute:
-  fixes z w::"int"
-  shows "(z::int) + w = w + z"
-  by (lifting zadd_commute_raw)
-
-lemma zadd_assoc_raw:
-  shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
-  by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
-
-lemma zadd_assoc: 
-  fixes z1 z2 z3::"int"
-  shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
-  by (lifting zadd_assoc_raw)
-
-lemma zadd_0_raw:
-  shows "add_raw (0, 0) z = z"
-  by (simp add: add_raw_def)
-
-
-text {*also for the instance declaration int :: plus_ac0*}
-lemma zadd_0: 
-  fixes z::"int"
-  shows "0 + z = z"
-  by (lifting zadd_0_raw)
-
-lemma zadd_zminus_inverse_raw:
-  shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
-  by (cases z) (simp add: add_raw_def uminus_raw_def)
-
-lemma zadd_zminus_inverse2: 
-  fixes z::"int"
-  shows "(- z) + z = 0"
-  by (lifting zadd_zminus_inverse_raw)
-
-subsection{*Integer Multiplication*}
-
-lemma zmult_zminus_raw:
-  shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
-apply(cases z, cases w)
-apply(simp add: uminus_raw_def)
-done
-
-lemma mult_raw_fst:
-  assumes a: "intrel x z"
-  shows "intrel (mult_raw x y) (mult_raw z y)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma mult_raw_snd:
-  assumes a: "intrel x z"
-  shows "intrel (mult_raw y x) (mult_raw y z)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma [quot_respect]:
-  shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule equivp_transp[OF int_equivp])
-apply(rule mult_raw_fst)
-apply(assumption)
-apply(rule mult_raw_snd)
-apply(assumption)
-done
-
-lemma zmult_zminus: 
-  fixes z w::"int"
-  shows "(- z) * w = - (z * w)"
-  by (lifting zmult_zminus_raw)
-
-lemma zmult_commute_raw: 
-  shows "mult_raw z w = mult_raw w z"
-apply(cases z, cases w)
-apply(simp add: add_ac mult_ac)
-done
-
-lemma zmult_commute: 
-  fixes z w::"int"
-  shows "z * w = w * z"
-  by (lifting zmult_commute_raw)
-
-lemma zmult_assoc_raw:
-  shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
-apply(cases z1, cases z2, cases z3)
-apply(simp add: add_mult_distrib2 mult_ac)
-done
-
-lemma zmult_assoc: 
-  fixes z1 z2 z3::"int"
-  shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
-  by (lifting zmult_assoc_raw)
-
-lemma zadd_mult_distrib_raw:
-  shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
-apply(cases z1, cases z2, cases w)
-apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
-done
-
-lemma zadd_zmult_distrib: 
-  fixes z1 z2 w::"int"
-  shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
-  by(lifting zadd_mult_distrib_raw)
-
-lemma zadd_zmult_distrib2: 
-  fixes w z1 z2::"int"
-  shows "w * (z1 + z2) = (w * z1) + (w * z2)"
-  by (simp add: zmult_commute [of w] zadd_zmult_distrib)
-
-lemma zdiff_zmult_distrib: 
-  fixes w z1 z2::"int"
-  shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
-  by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
-
-lemma zdiff_zmult_distrib2: 
-  fixes w z1 z2::"int"
-  shows "w * (z1 - z2) = (w * z1) - (w * z2)"
-  by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
-
-lemmas int_distrib =
-  zadd_zmult_distrib zadd_zmult_distrib2
-  zdiff_zmult_distrib zdiff_zmult_distrib2
-
-lemma zmult_1_raw:
-  shows "mult_raw (1, 0) z = z"
-  by (cases z) (auto)
-
-lemma zmult_1:
-  fixes z::"int"
-  shows "1 * z = z"
-  by (lifting zmult_1_raw)
-
-lemma zmult_1_right: 
-  fixes z::"int"
-  shows "z * 1 = z"
-  by (rule trans [OF zmult_commute zmult_1])
-
-lemma zero_not_one:
-  shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
-  by auto
-
-text{*The Integers Form A Ring*}
-instance int :: comm_ring_1
-proof
-  fix i j k :: int
-  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
-  show "i + j = j + i" by (simp add: zadd_commute)
-  show "0 + i = i" by (rule zadd_0)
-  show "- i + i = 0" by (rule zadd_zminus_inverse2)
-  show "i - j = i + (-j)" by (simp add: diff_int_def)
-  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
-  show "i * j = j * i" by (rule zmult_commute)
-  show "1 * i = i" by (rule zmult_1) 
-  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
-  show "0 \<noteq> (1::int)" by (lifting zero_not_one)
-qed
-
-
-subsection{*The @{text "\<le>"} Ordering*}
-
-lemma zle_refl_raw:
-  shows "le_raw w w"
-  by (cases w) (simp add: le_raw_def)
-
-lemma [quot_respect]:
-  shows "(intrel ===> intrel ===> op =) le_raw le_raw"
-  by (auto) (simp_all add: le_raw_def)
-
-lemma zle_refl: 
-  fixes w::"int"
-  shows "w \<le> w"
-  by (lifting zle_refl_raw)
-
-
-lemma zle_trans_raw:
-  shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
-apply(cases i, cases j, cases k)
-apply(auto simp add: le_raw_def)
-done
-
-lemma zle_trans: 
-  fixes i j k::"int"
-  shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
-  by (lifting zle_trans_raw)
-
-lemma zle_anti_sym_raw:
-  shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
-apply(cases z, cases w)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_anti_sym: 
-  fixes z w::"int"
-  shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
-  by (lifting zle_anti_sym_raw)
-
-
-(* Axiom 'order_less_le' of class 'order': *)
-lemma zless_le: 
-  fixes w z::"int"
-  shows "(w < z) = (w \<le> z & w \<noteq> z)"
-  by (simp add: less_int_def)
-
-instance int :: order
-apply (default)
-apply(auto simp add: zless_le zle_anti_sym)[1]
-apply(rule zle_refl)
-apply(erule zle_trans, assumption)
-apply(erule zle_anti_sym, assumption)
-done
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-
-lemma zle_linear_raw:
-  shows "le_raw z w \<or> le_raw w z"
-apply(cases w, cases z)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_linear: 
-  fixes z w::"int"
-  shows "z \<le> w \<or> w \<le> z"
-  by (lifting zle_linear_raw)
-
-instance int :: linorder
-apply(default)
-apply(rule zle_linear)
-done
-
-lemma zadd_left_mono_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
-apply(cases k)
-apply(auto simp add: add_raw_def le_raw_def)
-done
-
-lemma zadd_left_mono: 
-  fixes i j::"int"
-  shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
-  by (lifting zadd_left_mono_raw)
-
-
-subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
-
-definition
-  "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
-
-quotient_definition
-  "nat2::int \<Rightarrow> nat"
-is
-  "nat_raw"
-
-abbreviation
-  "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
-
-lemma nat_le_eq_zle_raw:
-  shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
-  apply (cases w)
-  apply (cases z)
-  apply (simp add: nat_raw_def le_raw_def)
-  by auto
-
-lemma [quot_respect]:
-  shows "(intrel ===> op =) nat_raw nat_raw"
-  by (auto iff: nat_raw_def)
-
-lemma nat_le_eq_zle: 
-  fixes w z::"int"
-  shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
-  unfolding less_int_def
-  by (lifting nat_le_eq_zle_raw)
-
-end
diff -r a294e4ebe0a3 -r 3909002beca5 src/HOL/Quotient_Examples/Quotient_Int.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Thu Apr 29 09:06:35 2010 +0200
@@ -0,0 +1,380 @@
+(*  Title:      HOL/Quotient_Examples/Quotient_Int.thy
+    Author:     Cezary Kaliszyk
+    Author:     Christian Urban
+
+Integers based on Quotients, based on an older version by Larry Paulson.
+*)
+theory Quotient_Int
+imports Quotient_Product Nat
+begin
+
+fun
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+  "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type int = "nat \<times> nat" / intrel
+  by (auto simp add: equivp_def expand_fun_eq)
+
+instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
+begin
+
+quotient_definition
+  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
+
+quotient_definition
+  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
+
+fun
+  plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
+
+quotient_definition
+  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
+
+fun
+  uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "uminus_int_raw (x, y) = (y, x)"
+
+quotient_definition
+  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
+
+definition
+  minus_int_def [code del]:  "z - w = z + (-w\<Colon>int)"
+
+fun
+  times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_definition
+  "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+
+fun
+  le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+  "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
+
+quotient_definition
+  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
+
+definition
+  less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
+
+definition
+  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
+definition
+  zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
+
+instance ..
+
+end
+
+lemma [quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
+  and   "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
+  and   "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
+  by auto
+
+lemma times_int_raw_fst:
+  assumes a: "x \<approx> z"
+  shows "times_int_raw x y \<approx> times_int_raw z y"
+  using a
+  apply(cases x, cases y, cases z)
+  apply(auto simp add: times_int_raw.simps intrel.simps)
+  apply(rename_tac u v w x y z)
+  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+  apply(simp add: mult_ac)
+  apply(simp add: add_mult_distrib [symmetric])
+  done
+
+lemma times_int_raw_snd:
+  assumes a: "x \<approx> z"
+  shows "times_int_raw y x \<approx> times_int_raw y z"
+  using a
+  apply(cases x, cases y, cases z)
+  apply(auto simp add: times_int_raw.simps intrel.simps)
+  apply(rename_tac u v w x y z)
+  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
+  apply(simp add: mult_ac)
+  apply(simp add: add_mult_distrib [symmetric])
+  done
+
+lemma [quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
+  apply(simp only: fun_rel_def)
+  apply(rule allI | rule impI)+
+  apply(rule equivp_transp[OF int_equivp])
+  apply(rule times_int_raw_fst)
+  apply(assumption)
+  apply(rule times_int_raw_snd)
+  apply(assumption)
+  done
+
+lemma plus_assoc_raw:
+  shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
+  by (cases i, cases j, cases k) (simp)
+
+lemma plus_sym_raw:
+  shows "plus_int_raw i j \<approx> plus_int_raw j i"
+  by (cases i, cases j) (simp)
+
+lemma plus_zero_raw:
+  shows "plus_int_raw (0, 0) i \<approx> i"
+  by (cases i) (simp)
+
+lemma plus_minus_zero_raw:
+  shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
+  by (cases i) (simp)
+
+lemma times_assoc_raw:
+  shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
+  by (cases i, cases j, cases k)
+     (simp add: algebra_simps)
+
+lemma times_sym_raw:
+  shows "times_int_raw i j \<approx> times_int_raw j i"
+  by (cases i, cases j) (simp add: algebra_simps)
+
+lemma times_one_raw:
+  shows "times_int_raw  (1, 0) i \<approx> i"
+  by (cases i) (simp)
+
+lemma times_plus_comm_raw:
+  shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
+by (cases i, cases j, cases k)
+   (simp add: algebra_simps)
+
+lemma one_zero_distinct:
+  shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
+  by simp
+
+text{* The integers form a @{text comm_ring_1}*}
+
+instance int :: comm_ring_1
+proof
+  fix i j k :: int
+  show "(i + j) + k = i + (j + k)"
+    by (lifting plus_assoc_raw)
+  show "i + j = j + i"
+    by (lifting plus_sym_raw)
+  show "0 + i = (i::int)"
+    by (lifting plus_zero_raw)
+  show "- i + i = 0"
+    by (lifting plus_minus_zero_raw)
+  show "i - j = i + - j"
+    by (simp add: minus_int_def)
+  show "(i * j) * k = i * (j * k)"
+    by (lifting times_assoc_raw)
+  show "i * j = j * i"
+    by (lifting times_sym_raw)
+  show "1 * i = i"
+    by (lifting times_one_raw)
+  show "(i + j) * k = i * k + j * k"
+    by (lifting times_plus_comm_raw)
+  show "0 \<noteq> (1::int)"
+    by (lifting one_zero_distinct)
+qed
+
+lemma plus_int_raw_rsp_aux:
+  assumes a: "a \<approx> b" "c \<approx> d"
+  shows "plus_int_raw a c \<approx> plus_int_raw b d"
+  using a
+  by (cases a, cases b, cases c, cases d)
+     (simp)
+
+lemma add_abs_int:
+  "(abs_int (x,y)) + (abs_int (u,v)) =
+   (abs_int (x + u, y + v))"
+  apply(simp add: plus_int_def id_simps)
+  apply(fold plus_int_raw.simps)
+  apply(rule Quotient_rel_abs[OF Quotient_int])
+  apply(rule plus_int_raw_rsp_aux)
+  apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
+  done
+
+definition int_of_nat_raw:
+  "int_of_nat_raw m = (m :: nat, 0 :: nat)"
+
+quotient_definition
+  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
+
+lemma[quot_respect]:
+  shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
+  by (simp add: equivp_reflp[OF int_equivp])
+
+lemma int_of_nat:
+  shows "of_nat m = int_of_nat m"
+  by (induct m)
+     (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
+
+lemma le_antisym_raw:
+  shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
+  by (cases i, cases j) (simp)
+
+lemma le_refl_raw:
+  shows "le_int_raw i i"
+  by (cases i) (simp)
+
+lemma le_trans_raw:
+  shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
+  by (cases i, cases j, cases k) (simp)
+
+lemma le_cases_raw:
+  shows "le_int_raw i j \<or> le_int_raw j i"
+  by (cases i, cases j)
+     (simp add: linorder_linear)
+
+instance int :: linorder
+proof
+  fix i j k :: int
+  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
+    by (lifting le_antisym_raw)
+  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
+    by (auto simp add: less_int_def dest: antisym)
+  show "i \<le> i"
+    by (lifting le_refl_raw)
+  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
+    by (lifting le_trans_raw)
+  show "i \<le> j \<or> j \<le> i"
+    by (lifting le_cases_raw)
+qed
+
+instantiation int :: distrib_lattice
+begin
+
+definition
+  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
+  by default
+     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+
+end
+
+lemma le_plus_int_raw:
+  shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
+  by (cases i, cases j, cases k) (simp)
+
+instance int :: ordered_cancel_ab_semigroup_add
+proof
+  fix i j k :: int
+  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+    by (lifting le_plus_int_raw)
+qed
+
+abbreviation
+  "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
+
+lemma zmult_zless_mono2_lemma:
+  fixes i j::int
+  and   k::nat
+  shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
+  apply(induct "k")
+  apply(simp)
+  apply(case_tac "k = 0")
+  apply(simp_all add: left_distrib add_strict_mono)
+  done
+
+lemma zero_le_imp_eq_int_raw:
+  fixes k::"(nat \<times> nat)"
+  shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
+  apply(cases k)
+  apply(simp add:int_of_nat_raw)
+  apply(auto)
+  apply(rule_tac i="b" and j="a" in less_Suc_induct)
+  apply(auto)
+  done
+
+lemma zero_le_imp_eq_int:
+  fixes k::int
+  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
+  unfolding less_int_def int_of_nat
+  by (lifting zero_le_imp_eq_int_raw)
+
+lemma zmult_zless_mono2:
+  fixes i j k::int
+  assumes a: "i < j" "0 < k"
+  shows "k * i < k * j"
+  using a
+  by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
+
+text{*The integers form an ordered integral domain*}
+
+instance int :: linordered_idom
+proof
+  fix i j k :: int
+  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
+    by (rule zmult_zless_mono2)
+  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
+    by (simp only: zabs_def)
+  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+    by (simp only: zsgn_def)
+qed
+
+lemmas int_distrib =
+  left_distrib [of "z1::int" "z2" "w", standard]
+  right_distrib [of "w::int" "z1" "z2", standard]
+  left_diff_distrib [of "z1::int" "z2" "w", standard]
+  right_diff_distrib [of "w::int" "z1" "z2", standard]
+  minus_add_distrib[of "z1::int" "z2", standard]
+
+lemma int_induct_raw:
+  assumes a: "P (0::nat, 0)"
+  and     b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))"
+  and     c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))"
+  shows      "P x"
+proof (cases x, clarify)
+  fix a b
+  show "P (a, b)"
+  proof (induct a arbitrary: b rule: Nat.induct)
+    case zero
+    show "P (0, b)" using assms by (induct b) auto
+  next
+    case (Suc n)
+    then show ?case using assms by auto
+  qed
+qed
+
+lemma int_induct:
+  fixes x :: int
+  assumes a: "P 0"
+  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
+  and     c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
+  shows      "P x"
+  using a b c unfolding minus_int_def
+  by (lifting int_induct_raw)
+
+text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
+
+definition
+  "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
+
+quotient_definition
+  "int_to_nat::int \<Rightarrow> nat"
+is
+  "int_to_nat_raw"
+
+lemma [quot_respect]:
+  shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
+  by (auto iff: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle_raw:
+  assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
+  shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
+  using a
+  by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle:
+  fixes w z::"int"
+  shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
+  unfolding less_int_def
+  by (lifting nat_le_eq_zle_raw)
+
+end
diff -r a294e4ebe0a3 -r 3909002beca5 src/HOL/Quotient_Examples/Quotient_Message.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Thu Apr 29 09:06:35 2010 +0200
@@ -0,0 +1,399 @@
+(*  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 Quotient_Syntax
+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_type msg = freemsg / msgrel
+  by (rule equiv_msgrel)
+
+text{*The abstract message constructors*}
+
+quotient_definition
+  "Nonce :: nat \<Rightarrow> msg"
+is
+  "NONCE"
+
+quotient_definition
+  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+is
+  "MPAIR"
+
+quotient_definition
+  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+  "CRYPT"
+
+quotient_definition
+  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+  "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]:
+  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 \<Rightarrow> nat set"
+is
+  "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]:
+  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 \<Rightarrow> msg"
+is
+  "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_definition
+  "right:: msg \<Rightarrow> msg"
+is
+  "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_definition
+  "discrim:: msg \<Rightarrow> int"
+is
+  "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
+
diff -r a294e4ebe0a3 -r 3909002beca5 src/HOL/Quotient_Examples/ROOT.ML
--- a/src/HOL/Quotient_Examples/ROOT.ML	Wed Apr 28 17:42:37 2010 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML	Thu Apr 29 09:06:35 2010 +0200
@@ -4,5 +4,5 @@
 Testing the quotient package.
 *)
 
-use_thys ["FSet", "LarryInt", "LarryDatatype"];
+use_thys ["FSet", "Quotient_Int", "Quotient_Message"];