--- a/Quotient-Paper-jv/Paper.thy Tue Apr 10 15:19:42 2012 +0100
+++ b/Quotient-Paper-jv/Paper.thy Tue Apr 10 15:21:07 2012 +0100
@@ -50,7 +50,7 @@
where "minus_pair (n, m) = (m, n)"
fun
- intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+ intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" ("_ \<approx> _" [50, 50] 50)
where
"intrel (x, y) (u, v) = (x + v = u + y)"
@@ -94,7 +94,7 @@
\end{isabelle}
\noindent
- Negation on integers is defined in terms of swapping on pairs:
+ Negation on integers is defined in terms of swapping of pairs:
\begin{isabelle}\ \ \ \ \ %%%
@{thm minus_pair.simps[where ?n="n" and ?m="m", THEN eq_reflection]}%
@@ -149,29 +149,31 @@
\end{isabelle}
\noindent
- where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not zero.
+ where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not allowed to be zero.
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.
+ finite sets, etc.~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 rather repetitive and involves explicit conversions
+ between the quotient and raw level in form of abstraction and
+ representation functions \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. 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}).
+ The purpose of a \emph{quotient package} is to ease the lifting of
+ theorems 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 then be introduced by declaring the new type (in this case
+ @{typ int}), the raw type (that is @{typ "nat \<times> nat"}) and the
+ equivalence relation (that is @{text intrel} defined in
+ \eqref{natpairequiv}).
*}
quotient_type int = "nat \<times> nat" / intrel
@@ -179,11 +181,11 @@
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
+ indeed an equivalence relation, whereby an equivalence
+ relation is defined as one that is reflexive, symmetric and
+ transitive. This proof obligation can thus be discharged by
unfolding the definitions and using the standard automatic proving
- tactic in Isabelle.
+ tactic in Isabelle/HOL.
*}
unfolding equivp_reflp_symp_transp
unfolding reflp_def symp_def transp_def
@@ -194,7 +196,8 @@
(*>*)
text {*
\noindent
- Next we can declare the constants zero and one for the quotient type @{text int}.
+ Next we can declare the constants @{text "0"} and @{text "1"} for the
+ quotient type @{text int}.
*}
quotient_definition
"0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" .
@@ -204,13 +207,13 @@
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 "- _"}).
+ To be useful, we can also need declare two operations for adding two
+ integers (written @{text plus}) and negating an integer
+ (written @{text "uminus"}).
*}
quotient_definition
- "(op +) \<Colon> int \<Rightarrow> int \<Rightarrow> int" is add_pair
+ "plus \<Colon> int \<Rightarrow> int \<Rightarrow> int" is add_pair
by auto
quotient_definition
@@ -224,11 +227,104 @@
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.
+ Isabelle/HOL can introduce some convenient short-hand notation for these
+ operations allowing the user to write
+ addition as infix operation, for example @{text "i + j"}, and
+ negation as prefix operation, for example @{text "- i"}. In both
+ cases, however, the declaration requires the user 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 of
+ respectfulness will be given later). Both proofs can be solved by
+ the automatic proving tactic in Isabelle/HOL.
+
+ Besides helping with declarations of quotient types and definitions
+ of constants, the point of a quotient package is to help with
+ proving properties about quotient types. For example we might be
+ interested in the usual property that zero is an ???. This property
+ can be stated as follows:
+*}
+
+ lemma zero_add:
+ shows "0 + i = (i::int)"
+ proof(descending)
+txt {*
+ \noindent
+ The tactic @{text "descending"} automatically transfers this property of integers
+ to a proof-obligation involving pairs of @{typ nat}s. (There is also
+ a tactic, called @{text lifting}, which automatically transfers properties
+ from the raw level to the quotient type.) In case of lemma @{text "zero_add"}
+ we obtain the subgoal
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "add_pair (0, 0) i \<approx> i"}
+ \end{isabelle}
+
+ \noindent
+ which can be solved again by the automatic proving tactic @{text "auto"}, as follows
+*}
+ qed(auto)
+
+text {*
+ In this simple example the task of the user is to state the property for integers
+ and use the quotient package and automatic proving tools of Isabelle/HOL to do
+ the ``rest''. A more interesting example is to establish an induction principle for
+ integers. For this we first establish the following induction principle where the
+ induction proceeds over two natural numbers.
+*}
+
+ lemma nat_induct2:
+ assumes "P 0 0"
+ and "\<And>n m. P n m \<Longrightarrow> P (Suc n) m"
+ and "\<And>n m. P n m \<Longrightarrow> P n (Suc m)"
+ shows "P n m"
+ using assms
+ by (induction_schema) (pat_completeness, lexicographic_order)
+
+text {*
+ \noindent
+ The symbol @{text "\<And>"} stands for Isabelle/HOL's universal quantifier and
+ @{text "\<Longrightarrow>"} for its implication.
+ As can be seen, this induction principle can be conveniently established using the
+ reasoning infrastructure of the function package \cite{???}, which
+ provides the tactics @{text "induction_schema"}, @{text "pat_completeness"}
+ and @{text "lexicographic_order"}. These tactics enable Isabelle/HOL
+ to use well-founded induction to prove @{text "nat_induct2"}. Our
+ quotient package can now be used to prove the following property:
+*}
+
+ lemma int_induct:
+ assumes "P 0"
+ and "\<And>i. P i \<Longrightarrow> P (i + 1)"
+ and "\<And>i. P i \<Longrightarrow> P (i + (- 1))"
+ shows "P (j::int)"
+ using assms
+ proof (descending)
+
+txt {*
+ \noindent
+ The @{text descending} tactic transfers it to the following proof
+ obligation on the raw level.
+
+ @{subgoals[display]}
+
+ \noindent
+ Note that the variable @{text "j"} in this subgoal is of type
+ @{text "nat \<times> nat"}. This subgoal cannot be proved automatically by
+ @{text auto}, but if we give it the hint to use @{text nat_induct2},
+ then @{text auto} can discharge it as follows.
+
+*}
+ qed (auto intro: nat_induct2)
+
+text {*
+ This completes the proof of the induction principle
+ for integers. Isabelle/HOL would allow us to inspect the
+ detailed reasoning steps involved which would confirm that
+ @{text "int_induct"} has been proved from ``first-principles''
+ by transforming the property over the quotient type @{text int}
+ to a corresponding property one on the raw level.
+
In the
context of HOL, there have been a few quotient packages already