53   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 

    53   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" ("_ \<approx> _" [50, 50] 50) 

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

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

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

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

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

   155   finite sets, etc.~one needs to establish a reasoning infrastructure

   156   needs to establish a reasoning infrastructure by transferring, or

   156   by transferring, or \emph{lifting}, definitions and theorems from

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

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

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

   158   (similarly for finite sets, $\alpha$-equated lambda-terms and

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

   159   rational numbers). This lifting usually requires a reasoning effort

   160   lifting usually requires a reasoning effort that can be repetitive

   160   that can be rather repetitive and involves explicit conversions 

   161   and involves explicit mediation between the quotient and raw level

   161   between the quotient and raw level in form of abstraction and 

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

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

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

   163   work manually if one has only a few quotient constructions at

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

   164   hand. But if they have to be done over and over again, as in Nominal

   165   then manual reasoning is not an option.

   165   Isabelle, then manual reasoning is not an option.

   166 

   166 

   167   The purpose of a \emph{quotient package} is to ease the lifting of theorems

   167   The purpose of a \emph{quotient package} is to ease the lifting of

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

   168   theorems and automate the reasoning as much as possible. Before we

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

   169   delve into the details, let us show how the user interacts with our

   170   when defining integers. We assume the definitions involving pairs 

   170   quotient package when defining integers. We assume the definitions

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

   171   involving pairs of natural numbers shown in \eqref{natpairequiv},

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

   172   \eqref{addpair} and \eqref{minuspair} have already been made. A

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

   173   quotient can then be introduced by declaring the new type (in this case

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

   174   @{typ int}), the raw type (that is @{typ "nat \<times> nat"}) and the

   175   equivalence relation (that is @{text intrel} defined in

   176   \eqref{natpairequiv}).

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

   184   indeed an equivalence relation, whereby an equivalence 

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

   185   relation is defined as one that is reflexive, symmetric and

   184   transitivity.  This proof obligation can thus be discharged by

   186   transitive.  This proof obligation can thus be discharged by

   186   tactic in Isabelle.

   188   tactic in Isabelle/HOL.

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

   199   Next we can declare the constants @{text "0"} and @{text "1"} for the 

   200   quotient type @{text int}.

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

   210   To be useful, we can also need declare two operations for adding two

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

   211   integers (written @{text plus}) and negating an integer

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

   212   (written @{text "uminus"}).

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

   216       "plus \<Colon> int \<Rightarrow> int \<Rightarrow> int"  is  add_pair 

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

   230   Isabelle/HOL can introduce some convenient short-hand notation for these

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

   231   operations allowing the user to write

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

   232   addition as infix operation, for example @{text "i + j"}, and

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

   233   negation as prefix operation, for example @{text "- i"}.  In both

   231   the automatic proving tactic in Isabelle.

   234   cases, however, the declaration requires the user to discharge a

   235   proof-obligation which ensures that the operations a

   236   \emph{respectful}. This property ensures that the operations are

   237   well-defined on the quotient level (a formal definition of

   238   respectfulness will be given later). Both proofs can be solved by

   239   the automatic proving tactic in Isabelle/HOL.

   240 

   241   Besides helping with declarations of quotient types and definitions 

   242   of constants, the point of a quotient package is to help with 

   243   proving properties about quotient types. For example we might be

   244   interested in the usual property that zero is an ???. This property 

   245   can be stated as follows:

   246 *}

   247 

   248      lemma zero_add:

   249        shows "0 + i = (i::int)"

   250      proof(descending)

   251 txt {*

   252   \noindent 

   253   The tactic @{text "descending"} automatically transfers this property of integers

   254   to a proof-obligation involving pairs of @{typ nat}s. (There is also

   255   a tactic, called @{text lifting}, which automatically transfers properties

   256   from the raw level to the quotient type.) In case of lemma @{text "zero_add"}

   257   we obtain the subgoal

   258 

   259   \begin{isabelle}\ \ \ \ \ %%%

   260   @{text "add_pair (0, 0) i \<approx> i"}

   261   \end{isabelle}

   262 

   263   \noindent

   264   which can be solved again by the automatic proving tactic @{text "auto"}, as follows

   265 *}

   266      qed(auto)

   267 

   268 text {*

   269   In this simple example the task of the user is to state the property for integers

   270   and use the quotient package and automatic proving tools of Isabelle/HOL to do

   271   the ``rest''. A more interesting example is to establish an induction principle for 

   272   integers. For this we first establish the following induction principle where the 

   273   induction proceeds over two natural numbers. 

   274 *}

   275 

   276     lemma nat_induct2:

   277       assumes "P 0 0"

   278       and     "\<And>n m. P n m \<Longrightarrow> P (Suc n) m"

   279       and     "\<And>n m. P n m \<Longrightarrow> P n (Suc m)"

   280       shows   "P n m"

   281       using assms

   282       by (induction_schema) (pat_completeness, lexicographic_order)

   283 

   284 text {*

   285   \noindent

   286   The symbol @{text "\<And>"} stands for Isabelle/HOL's universal quantifier and

   287   @{text "\<Longrightarrow>"} for its implication.

   288   As can be seen, this induction principle can be conveniently established using the

   289   reasoning infrastructure of the function package \cite{???}, which 

   290   provides the tactics @{text "induction_schema"}, @{text "pat_completeness"}

   291   and @{text "lexicographic_order"}. These tactics enable Isabelle/HOL

   292   to use well-founded induction to prove @{text "nat_induct2"}. Our 

   293   quotient package can now be used to prove the following property:

   294 *}

   295 

   296     lemma int_induct:

   297       assumes "P 0"

   298       and     "\<And>i. P i \<Longrightarrow> P (i + 1)"

   299       and     "\<And>i. P i \<Longrightarrow> P (i + (- 1))"

   300       shows   "P (j::int)"

   301       using assms 

   302       proof (descending)

   303 

   304 txt {*

   305   \noindent

   306   The @{text descending} tactic transfers it to the following proof 

   307   obligation on the raw level.

   308   

   309   @{subgoals[display]}

   310 

   311   \noindent

   312   Note that the variable @{text "j"} in this subgoal is of type

   313   @{text "nat \<times> nat"}. This subgoal cannot be proved automatically by 

   314   @{text auto}, but if we give it the hint to use @{text nat_induct2},

   315   then @{text auto} can discharge it as follows.

   316   

   317 *}

   318        qed (auto intro: nat_induct2)

   319 

   320 text {*

   321   This completes the proof of the induction principle

   322   for integers. Isabelle/HOL would allow us to inspect the 

   323   detailed reasoning steps involved which would confirm that

   324   @{text "int_induct"} has been proved from ``first-principles''

   325   by transforming the property over the quotient type @{text int}

   326   to a corresponding property one on the raw level.

   327