--- a/Quotient-Paper-jv/Paper.thy	Fri Mar 30 16:08:00 2012 +0200
+++ b/Quotient-Paper-jv/Paper.thy	Tue Apr 03 23:09:13 2012 +0100
@@ -43,9 +43,19 @@
   Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
 *}
 
+fun add_pair :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" 
+where "add_pair (n1, m1) (n2, m2) = (n1 + n2, m1 + m2)"
+
+fun minus_pair :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" 
+where "minus_pair (n, m) = (m, n)"
+
+fun
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
+where
+  "intrel (x, y) (u, v) = (x + v = u + y)"
+
 (*>*)
 
-
 section {* Introduction *}
 
 text {*
@@ -75,11 +85,20 @@
   This constructions yields the new type @{typ int}, and definitions for @{text
   "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
   natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
-  such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
-  terms of operations on pairs of natural numbers:
+  such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined 
+  in terms of operations on pairs of natural numbers:
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{text "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2, m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}
+  @{thm add_pair.simps[where ?n1.0="n\<^isub>1" and ?n2.0="n\<^isub>2" and ?m1.0="m\<^isub>1" and ?m2.0="m\<^isub>2", THEN eq_reflection]}%
+  \hfill\numbered{addpair}
+  \end{isabelle}
+
+  \noindent
+  Negation on integers is defined in terms of swapping on pairs:
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm minus_pair.simps[where ?n="n" and ?m="m", THEN eq_reflection]}%
+  \hfill\numbered{minuspair}
   \end{isabelle}
 
   \noindent
@@ -121,21 +140,97 @@
   $\alpha$-equated terms, equality coincides with $\alpha$-equivalence and
   we can use for reasoning HOL's built-in notion of ``replacing equals by equals''.
 
-  {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?}
+  There is also often a need to consider quotients of parial equivalence relations. For 
+  example the rational numbers
+  can be constructed using pairs of integers and the partial equivalence relation
 
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 * m\<^isub>2 = m\<^isub>1 * n\<^isub>2"}\hfill\numbered{ratpairequiv}
+  \end{isabelle}
+
+  \noindent
+  where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not zero.
 
-  The difficulty is that in order to be able to reason about integers, finite
-  sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
-  infrastructure by transferring, or \emph{lifting}, definitions and theorems
-  from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
-  (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
-  usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.
-  In principle it is feasible to do this work manually, if one has only a few quotient
-  constructions at hand. But if they have to be done over and over again, as in
-  Nominal Isabelle, then manual reasoning is not an option.
+  The difficulty is that in order to be able to reason about integers,
+  finite sets, $\alpha$-equated lambda-terms and rational numbers one
+  needs to establish a reasoning infrastructure by transferring, or
+  \emph{lifting}, definitions and theorems from the raw type @{typ
+  "nat \<times> nat"} to the quotient type @{typ int} (similarly for finite
+  sets, $\alpha$-equated lambda-terms and rational numbers). This
+  lifting usually requires a reasoning effort that can be repetitive
+  and involves explicit mediation between the quotient and raw level
+  \cite{Paulson06}.  In principle it is feasible to do this work
+  manually, if one has only a few quotient constructions at hand. But
+  if they have to be done over and over again, as in Nominal Isabelle,
+  then manual reasoning is not an option.
 
   The purpose of a \emph{quotient package} is to ease the lifting of theorems
-  and automate the reasoning as much as possible. In the
+  and automate the reasoning as much as possible. Before we delve into the 
+  details, let us show how the user interacts with our quotient package
+  when defining integers. We assume the definitions involving pairs 
+  of natural numbers shown in \eqref{natpairequiv}, \eqref{addpair} and 
+  \eqref{minuspair} have already been made. A quotient can be introduced by declaring 
+  the new type (in this case @{typ int}), the raw type (@{typ "nat * nat"}) and the 
+  equivalence relation (@{text intrel} defined in \eqref{natpairequiv}).
+*}
+
+  quotient_type int = "nat \<times> nat" / intrel
+
+txt {*
+  \noindent
+  This declaration requires the user to prove that @{text intrel} is
+  indeed an equivalence relation, whereby the notion of an equivalence
+  relation is defined as usual in terms of reflexivity, symmetry and
+  transitivity.  This proof obligation can thus be discharged by
+  unfolding the definitions and using the standard automatic proving
+  tactic in Isabelle.
+*}
+    unfolding equivp_reflp_symp_transp
+    unfolding reflp_def symp_def transp_def
+    by auto
+(*<*)
+    instantiation int :: "{zero, one, plus, uminus}"
+    begin
+(*>*)
+text {*
+  \noindent
+  Next we can declare the constants zero and one for the quotient type @{text int}.
+*}
+    quotient_definition
+      "0 \<Colon> int"  is  "(0\<Colon>nat, 0\<Colon>nat)" .
+
+    quotient_definition
+      "1 \<Colon> int"  is  "(1\<Colon>nat, 0\<Colon>nat)" .
+
+text {*
+  \noindent
+  To be useful and to state some properties, we also need to declare 
+  two operations for adding two integers (written infix as @{text "_ + _"}) and negating 
+  an integer (written @{text "uminus _"} or @{text "- _"}). 
+*}
+
+    quotient_definition
+      "(op +) \<Colon> int \<Rightarrow> int \<Rightarrow> int"  is  add_pair 
+      by auto
+
+    quotient_definition
+      "uminus \<Colon> int \<Rightarrow> int"  is  minus_pair 
+      by auto
+(*<*)    
+    instance ..
+
+    end
+(*>*)
+
+text {*
+  \noindent
+  In both cases we have to discharge a proof-obligation which ensures
+  that the operations a \emph{respectful}. This property ensures that
+  the operations are well-defined on the quotient level (a formal
+  definition will be given later). Both proofs can again be solved by
+  the automatic proving tactic in Isabelle.
+
+  In the
   context of HOL, there have been a few quotient packages already
   \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
   \cite{Homeier05} implemented in HOL4.  The fundamental construction these

--- a/Quotient-Paper-jv/document/root.tex	Fri Mar 30 16:08:00 2012 +0200
+++ b/Quotient-Paper-jv/document/root.tex	Tue Apr 03 23:09:13 2012 +0100
@@ -9,9 +9,6 @@
 \usepackage{pdfsetup}
 \usepackage{times}
 \usepackage{stmaryrd}
-%\newtheorem{definition}{Definition}
-%\newtheorem{proposition}{Proposition}
-%\newtheorem{lemma}{Lemma}
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -25,7 +22,6 @@
 
 \renewcommand{\isasymequiv}{$\triangleq$}
 \renewcommand{\isasymemptyset}{$\varnothing$}
-%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymUnion}{$\bigcup$}
 \renewcommand{\isacharunderscore}{\text{$\_\!\_$}}
 
@@ -40,7 +36,7 @@
 \title{Quotients Revisited for Isabelle/HOL}
 \author{Cezary Kaliszyk \and Christian Urban}
 \institute{C.~Kaliszyk \at University of Innsbruck, Austria
-     \and C.~Urban \at King's College London, UK}
+      \and C.~Urban \at King's College London, UK}
 \date{Received: date / Accepted: date}
 
 \maketitle
@@ -49,15 +45,14 @@
 Higher-Order Logic (HOL) is based on a small logic kernel, whose only
 mechanism for extension is the introduction of safe definitions and of
 non-empty types. Both extensions are often performed in quotient
-constructions. To ease the work involved with such quotient constructions, we
-re-implemented in the %popular
-Isabelle/HOL theorem prover the quotient
-package by Homeier. In doing so we extended his work in order to deal with
-compositions of quotients and also specified completely the procedure
-of lifting theorems from the raw level to the quotient level.
-The importance for theorem proving is that many formal
-verifications, in order to be feasible, require a convenient reasoning infrastructure
-for quotient constructions.
+constructions. To ease the work involved with such quotient
+constructions, we re-implemented in the Isabelle/HOL theorem prover
+the quotient package by Homeier. In doing so we extended his work in
+order to deal with compositions of quotients and also specified
+completely the procedure of lifting theorems from the raw level to the
+quotient level.  The importance for theorem proving is that many
+formal verifications, in order to be feasible, require a convenient
+reasoning infrastructure for quotient constructions.
 \end{abstract}
 
 %\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}