--- a/Quotient-Paper/Paper.thy Wed Jun 23 08:48:38 2010 +0200
+++ b/Quotient-Paper/Paper.thy Wed Jun 23 08:49:33 2010 +0200
@@ -5,6 +5,16 @@
"../Nominal/FSet"
begin
+(****
+
+** things to do for the next version
+*
+* - what are quot_thms?
+* - what do all preservation theorems look like,
+ in particular preservation for quotient
+ compositions
+*)
+
notation (latex output)
rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
@@ -290,11 +300,11 @@
"t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function
type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined
constants; a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
- bool"}, and the identity function with type @{text "id :: \<sigma> => \<sigma>"} is
+ bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is
defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
An important point to note is that theorems in HOL can be seen as a subset
- of terms that are constructed specially (namely through axioms and prove
+ of terms that are constructed specially (namely through axioms and proof
rules). As a result we are able to define automatic proof
procedures showing that one theorem implies another by decomposing the term
underlying the first theorem.
@@ -396,17 +406,13 @@
Second, even if we were able to state such a quotient theorem, it
would not be true in general. However, we can prove specific instances of a
quotient theorem for composing particular quotient relations.
- To lift @{term flat} the quotient theorem for composing @{text "\<approx>\<^bsub>list\<^esub>"}
- is necessary:
-% It says when lists are being quotiented to finite sets,
-% the contents of the lists can be quotiented as well
- If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"} then
+ For example, to lift theorems involving @{term flat} the quotient theorem for
+ composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
+ with @{text R} being an equivalence relation, then
- @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
+ @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep \<circ> rep_fset)"}
\vspace{-.5mm}
-
-
*}
section {* Quotient Types and Quotient Definitions\label{sec:type} *}
@@ -476,7 +482,7 @@
(for the proof see \cite{Homeier05}).
\begin{proposition}
- @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+ @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
\end{proposition}
The next step in a quotient construction is to introduce definitions of new constants
@@ -653,7 +659,7 @@
two restrictions in the form of proof obligations that arise during the
lifting. The reason is that even if definitions for all raw constants
can be given, \emph{not} all theorems can be lifted to the quotient type. Most
- notably is the bound variable function, that is the constant @{text bn}, defined
+ notable is the bound variable function, that is the constant @{text bn}, defined
for raw lambda-terms as follows
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -672,7 +678,7 @@
compositions.
To formally define what respectfulness is, we have to first define
- the notion of \emph{aggregate equivalence relations} using @{text REL}:
+ the notion of \emph{aggregate equivalence relations} using the function @{text REL}:
\begin{center}
\hfill
@@ -696,23 +702,11 @@
that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
- we throw the following proof obligation
+ we generate the following proof obligation
@{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
- %%% PROBLEM I do not yet completely understand the
- %%% form of respectfulness theorems
- %%%\noindent
- %%%if @ {text \<sigma>} and @ {text \<tau>} have no type variables. In case they have, then
- %%%the proof obligation is of the form
- %%%
- %%%@ {text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
-
- %%% ANSWER: The respectfulness theorems never have any quotient assumptions,
- %%% So the commited version is ok.
-
\noindent
- %%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
Homeier calls these proof obligations \emph{respectfulness
theorems}. However, unlike his quotient package, we might have several
respectfulness theorems for one constant---he has at most one.
@@ -722,13 +716,13 @@
corresponding respectfulness theorem.
Before lifting a theorem, we require the user to discharge
- them. And the point with @{text bn} is that the respectfulness theorem
+ respectfulness proof obligations. And the point with @{text bn} is that the respectfulness theorem
looks as follows
@{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
\noindent
- and the user cannot discharge it---because it is not true. To see this,
+ and the user cannot discharge it: because it is not true. To see this,
we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun}
using extensionally to obtain
@@ -744,9 +738,8 @@
To do so, we have to establish
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- if @{thm (prem1) append_rsp_unfolded[of xs ys us vs, no_vars]} and
- @{thm (prem2) append_rsp_unfolded[of xs ys us vs, no_vars]}
- then @{thm (concl) append_rsp_unfolded[of xs ys us vs, no_vars]}
+ if @{text "xs \<approx>\<^bsub>list\<^esub> ys"} and @{text "us \<approx>\<^bsub>list\<^esub> vs"}
+ then @{text "xs @ us \<approx>\<^bsub>list\<^esub> ys @ vs"}
\end{isabelle}
\noindent
@@ -754,14 +747,15 @@
The second restriction we have to impose arises from
non-lifted polymorphic constants, which are instantiated to a
- type being quotient. For example, take the @{term "cons"} to
- add a pair of natural numbers to a list. The pair of natural numbers
- is to become an integer. But we still want to use @{text cons} for
+ type being quotient. For example, take the @{term "cons"}-constructor to
+ add a pair of natural numbers to a list, whereby teh pair of natural numbers
+ is to become an integer in te quotient construction. The point is that we
+ still want to use @{text cons} for
adding integers to lists---just with a different type.
- To be able to lift such theorems, we need a \emph{preservation theorem}
+ To be able to lift such theorems, we need a \emph{preservation property}
for @{text cons}. Assuming we have a polymorphic raw constant
@{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"},
- then a preservation theorem is as follows
+ then a preservation property is as follows
@{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
@@ -775,7 +769,7 @@
under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
- then we need to show the corresponding preservation lemma.
+ then we need to show the corresponding preservation property.
%%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
@@ -814,7 +808,7 @@
The main benefit of a quotient package is to lift automatically theorems over raw
types to theorems over quotient types. We will perform this lifting in
three phases, called \emph{regularization},
- \emph{injection} and \emph{cleaning}.
+ \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
The purpose of regularization is to change the quantifiers and abstractions
in a ``raw'' theorem to quantifiers over variables that respect the relation
@@ -834,30 +828,32 @@
\end{center}
\noindent
+ which means the raw theorem implies the quotient theorem.
In contrast to other quotient packages, our package requires
the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we
also provide a fully automated mode, where the @{text "quot_thm"} is guessed
- from @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
- occurrences of a raw type.
+ from the form of @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
+ occurrences of a raw type, but not others.
The second and third proof step will always succeed if the appropriate
respectfulness and preservation theorems are given. In contrast, the first
proof step can fail: a theorem given by the user does not always
imply a regularized version and a stronger one needs to be proved. This
is outside of the scope where the quotient package can help. An example
- for the failure is the simple statement for integers @{text "0 \<noteq> 1"}.
- It does not follow by lifting from the fact that @{text "(0, 0) \<noteq> (1, 0)"}.
- The raw theorem only shows that particular element in the
- equivalence classes are not equal. A more general statement saying that
- the equivalence classes are not equal is necessary.
+ for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
+ One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},
+ but the raw theorem only shows that particular element in the
+ equivalence classes are not equal. A more general statement stipulating that
+ the equivalence classes are not equal is necessary, and then leads to the
+ theorem @{text "0 \<noteq> 1"}.
In the following we will first define the statement of the
regularized theorem based on @{text "raw_thm"} and
@{text "quot_thm"}. Then we define the statement of the injected theorem, based
- on @{text "reg_thm"} theorem and @{text "quot_thm"}. We then show the 3 proofs,
+ on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
which can all be performed independently from each other.
- We define the function @{text REG}. The intuition
+ We first define the function @{text REG}. The intuition
behind this function is that it replaces quantifiers and
abstractions involving raw types by bounded ones, and equalities
involving raw types are replaced by appropriate aggregate
@@ -891,7 +887,8 @@
\noindent
In the above definition we omitted the cases for existential quantifiers
and unique existential quantifiers, as they are very similar to the cases
- for the universal quantifier.
+ for the universal quantifier. For the third and fourt clause, note that
+ @{text "\<forall>x. P"} is defined as @{text "\<forall> (\<lambda>x. P)"}.
Next we define the function @{text INJ} which takes as argument
@{text "reg_thm"} and @{text "quot_thm"} (both as
@@ -933,7 +930,7 @@
start with an implication. Isabelle provides \emph{mono} rules that can split up
the implications into simpler implication subgoals. This succeeds for every
monotone connective, except in places where the function @{text REG} inserted,
- for example, a quantifier by a bounded quantifier. In this case we have
+ for instance, a quantifier by a bounded quantifier. In this case we have
rules of the form
@{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
@@ -953,10 +950,10 @@
\noindent
The last theorem is new in comparison with Homeier's package. There the
- injection procedure would be used to prove such goals, and there
+ injection procedure would be used to prove such goals, and
the assumption about the equivalence relation would be used. We use the above theorem directly,
because this allows us to completely separate the first and the second
- proof step into independent ``units''.
+ proof step into two independent ``units''.
The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"}, starts with an equality.
The proof again follows the structure of the
@@ -981,7 +978,7 @@
We defined the theorem @{text "inj_thm"} in such a way that
establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
- definitions. Then all lifted constants, their definitions
+ definitions. Then for all lifted constants, their definitions
are used to fold the @{term Rep} with the raw constant. Next for
all abstractions and quantifiers the lambda and
quantifier preservation theorems are used to replace the
@@ -1045,10 +1042,10 @@
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]
- \isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~%
- @{text "plus_raw (m, n) (p, q) = (m + p :: nat, n + q :: nat)"}\\
+ \isacommand{fun}~~@{text "add_pair"}~~\isacommand{where}~~%
+ @{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\
\isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
- \isacommand{is}~~@{text "plus_raw"}\\
+ \isacommand{is}~~@{text "add_pair"}\\
\end{tabular}
\end{isabelle}
@@ -1056,18 +1053,18 @@
The following theorem about addition on the raw level can be proved.
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
- \isacommand{lemma}~~@{text "plus_zero_raw: int_rel (plus_raw (0, 0) x) x"}
+ \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
\end{isabelle}
\noindent
If the user attempts to lift this theorem, all proof obligations are
automatically discharged, except the respectfulness
- proof for @{text "plus_raw"}:
+ proof for @{text "add_pair"}:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\begin{tabular}{@ {}l}
- \isacommand{lemma}~~@{text "[quot_respect]:\\
- (int_rel \<doublearr> int_rel \<doublearr> int_rel) plus_raw plus_raw"}
+ \isacommand{lemma}~~@{text "[quot_respect]:"}\\
+ @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
\end{tabular}
\end{isabelle}
@@ -1077,14 +1074,14 @@
After this, the user can prove the lifted lemma explicitly:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
- \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}
+ \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
\end{isabelle}
\noindent
or by the completely automated mode by stating:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
- \isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"}
+ \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
\end{isabelle}
\noindent
@@ -1094,7 +1091,7 @@
\noindent
Although seemingly simple, arriving at this result without the help of a quotient
- package requires substantial reasoning effort.
+ package requires a substantial reasoning effort.
*}
section {* Conclusion and Related Work\label{sec:conc}*}
@@ -1106,7 +1103,7 @@
standard distribution of Isabelle.\footnote{Available from
\href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
heavily used in the new version of Nominal Isabelle, which provides a convenient reasoning
- infrastructure for programming language calculi involving binders.
+ infrastructure for programming language calculi involving general binders.
To achieve this, it builds types representing @{text \<alpha>}-equivalent terms.
Earlier
versions of Nominal Isabelle have been used successfully in formalisations
@@ -1132,28 +1129,33 @@
The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}.
He introduced most of the abstract notions about quotients and also deals with the
lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed
- for lifting theorems about @{text flat}. Also, a number of his definitions, like @{text ABS},
- @{text REP} and @{text INJ} etc only exist in ML-code. On the other hand, Homeier
- is able to deal with partial quotient constructions, which we have not implemented.
+ for lifting theorems about @{text flat}). Also, a number of his definitions, like @{text ABS},
+ @{text REP} and @{text INJ} etc only exist in \cite{Homeier05} as ML-code, not included
+ in the paper.
One advantage of our package is that it is modular---in the sense that every step
in the quotient construction can be done independently (see the criticism of Paulson
about other quotient packages). This modularity is essential in the context of
Isabelle, which supports type-classes and locales.
- Another feature of our quotient package is that when lifting theorems, we can
+ Another feature of our quotient package is that when lifting theorems, teh user can
precisely specify what the lifted theorem should look like. This feature is
- necessary, for example, when lifting an inductive principle about two lists.
+ necessary, for example, when lifting an induction principle for two lists.
This principle has as the conclusion a predicate of the form @{text "P xs ys"},
and we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"},
or both. We found this feature very useful in the new version of Nominal
- Isabelle.
+ Isabelle, where such a choice is required to generate a resoning infrastructure
+ for alpha-equated terms.
+%%
+%% give an example for this
+%%
\medskip
\noindent
- {\bf Acknowledgements:} We would like to thank Peter Homeier for the
+ {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
discussions about his HOL4 quotient package and explaining to us
- some of its finer points in the implementation.
+ some of its finer points in the implementation. Without his patient
+ help, this work would have been impossible.
*}