877   A user of our quotient package first needs to define an equivalence relation:

   877   In this section we will show, a complete interaction with the quotient package

   878 

   878   for lifting a theorem about integers. A user of our quotient package first

   879   @{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}

   879   needs to define a relation on the raw type, by which the quotienting will be

   880 

   880   performed. We give the same integer relation as the one presented in the

   881   Then the user defines a quotient type:

   881   introduction:

   882 

   882 

   883   @{text "quotient_type int = (nat \<times> nat) / \<approx>"}

   883   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   884 

   884   \isacommand{fun}~~@{text "\<approx>"}~~\isacommand{where}~~@{text "(x \<Colon> nat, y) \<approx> (u, v) = (x + v = u + y)"}

   885   Which leaves a proof obligation that the relation is an equivalence relation,

   885   \end{isabelle}

   886   that can be solved with the automatic tactic with two definitions.

   886 

   887 

   887   \noindent

   888   Next the quotient type is defined. This leaves a proof obligation that the

   889   relation is an equivalence relation which is solved automatically using the

   890   definitions:

   891 

   892   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   893   \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "\<approx>"}

   894   \end{isabelle}

   895 

   896   \noindent