78   such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in

    88   such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined 

    79   terms of operations on pairs of natural numbers:

    89   in terms of operations on pairs of natural numbers:

    80 

    90 

    81   \begin{isabelle}\ \ \ \ \ %%%

    91   \begin{isabelle}\ \ \ \ \ %%%

    82   @{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)"}

    92   @{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]}%

    93   \hfill\numbered{addpair}

    94   \end{isabelle}

    95 

    96   \noindent

    97   Negation on integers is defined in terms of swapping on pairs:

    98 

    99   \begin{isabelle}\ \ \ \ \ %%%

   100   @{thm minus_pair.simps[where ?n="n" and ?m="m", THEN eq_reflection]}%

   101   \hfill\numbered{minuspair}

   124   {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?}

   143   There is also often a need to consider quotients of parial equivalence relations. For 

   125 

   144   example the rational numbers

   126 

   145   can be constructed using pairs of integers and the partial equivalence relation

   127   The difficulty is that in order to be able to reason about integers, finite

   146 

   128   sets or $\alpha$-equated lambda-terms one needs to establish a reasoning

   147   \begin{isabelle}\ \ \ \ \ %%%

   129   infrastructure by transferring, or \emph{lifting}, definitions and theorems

   148   @{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}

   130   from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}

   149   \end{isabelle}

   131   (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting

   150 

   132   usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.

   151   \noindent

   133   In principle it is feasible to do this work manually, if one has only a few quotient

   152   where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not zero.

   134   constructions at hand. But if they have to be done over and over again, as in

   153 

   135   Nominal Isabelle, then manual reasoning is not an option.

   154   The difficulty is that in order to be able to reason about integers,

   155   finite sets, $\alpha$-equated lambda-terms and rational numbers one

   156   needs to establish a reasoning infrastructure by transferring, or

   157   \emph{lifting}, definitions and theorems from the raw type @{typ

   158   "nat \<times> nat"} to the quotient type @{typ int} (similarly for finite

   159   sets, $\alpha$-equated lambda-terms and rational numbers). This

   160   lifting usually requires a reasoning effort that can be repetitive

   161   and involves explicit mediation between the quotient and raw level

   162   \cite{Paulson06}.  In principle it is feasible to do this work

   163   manually, if one has only a few quotient constructions at hand. But

   164   if they have to be done over and over again, as in Nominal Isabelle,

   165   then manual reasoning is not an option.

   138   and automate the reasoning as much as possible. In the

   168   and automate the reasoning as much as possible. Before we delve into the 

   169   details, let us show how the user interacts with our quotient package

   170   when defining integers. We assume the definitions involving pairs 

   171   of natural numbers shown in \eqref{natpairequiv}, \eqref{addpair} and 

   172   \eqref{minuspair} have already been made. A quotient can be introduced by declaring 

   173   the new type (in this case @{typ int}), the raw type (@{typ "nat * nat"}) and the 

   174   equivalence relation (@{text intrel} defined in \eqref{natpairequiv}).

   175 *}

   176 

   177   quotient_type int = "nat \<times> nat" / intrel

   178 

   179 txt {*

   180   \noindent

   181   This declaration requires the user to prove that @{text intrel} is

   182   indeed an equivalence relation, whereby the notion of an equivalence

   183   relation is defined as usual in terms of reflexivity, symmetry and

   184   transitivity.  This proof obligation can thus be discharged by

   185   unfolding the definitions and using the standard automatic proving

   186   tactic in Isabelle.

   187 *}

   188     unfolding equivp_reflp_symp_transp

   189     unfolding reflp_def symp_def transp_def

   190     by auto

   191 (*<*)

   192     instantiation int :: "{zero, one, plus, uminus}"

   193     begin

   194 (*>*)

   195 text {*

   196   \noindent

   197   Next we can declare the constants zero and one for the quotient type @{text int}.

   198 *}

   199     quotient_definition

   200       "0 \<Colon> int"  is  "(0\<Colon>nat, 0\<Colon>nat)" .

   201 

   202     quotient_definition

   203       "1 \<Colon> int"  is  "(1\<Colon>nat, 0\<Colon>nat)" .

   204 

   205 text {*

   206   \noindent

   207   To be useful and to state some properties, we also need to declare 

   208   two operations for adding two integers (written infix as @{text "_ + _"}) and negating 

   209   an integer (written @{text "uminus _"} or @{text "- _"}). 

   210 *}

   211 

   212     quotient_definition

   213       "(op +) \<Colon> int \<Rightarrow> int \<Rightarrow> int"  is  add_pair 

   214       by auto

   215 

   216     quotient_definition

   217       "uminus \<Colon> int \<Rightarrow> int"  is  minus_pair 

   218       by auto

   219 (*<*)    

   220     instance ..

   221 

   222     end

   223 (*>*)

   224 

   225 text {*

   226   \noindent

   227   In both cases we have to discharge a proof-obligation which ensures

   228   that the operations a \emph{respectful}. This property ensures that

   229   the operations are well-defined on the quotient level (a formal

   230   definition will be given later). Both proofs can again be solved by

   231   the automatic proving tactic in Isabelle.

   232 

   233   In the