--- a/Quotient-Paper/Paper.thy Wed Jun 16 22:29:42 2010 +0100
+++ b/Quotient-Paper/Paper.thy Thu Jun 17 00:27:57 2010 +0100
@@ -768,7 +768,7 @@
with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
then we need to show the corresponding preservation lemma.
- @{thm [display, indent=10] insert_preserve2[no_vars]}
+ %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
%Given two quotients, one of which quotients a container, and the
%other quotients the type in the container, we can write the
@@ -809,31 +809,46 @@
The purpose of regularization is to change the quantifiers and abstractions
in a ``raw'' theorem to quantifiers over variables that respect the relation
- (Definition \ref{def:respects} states what respects means). The purpose of injection is supposed to add @{term Rep}
+ (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
and @{term Abs} of appropriate types in front of constants and variables
of the raw type so that they can be replaced by the ones that include the
- quotient type. Cleaning rewrites the obtained injected theorem with
- preservation rules obtaining the desired goal theorem.
+ quotient type. The purpose of cleaning is to bring the theorem derived in the
+ first two phases into the form the user has specified. Abstractly, our
+ package establishes the following three proof steps:
+
+ \begin{center}
+ \begin{tabular}{r@ {\hspace{4mm}}l}
+ 1.) & @{text "raw_thm \<longrightarrow> reg_thm"}\\
+ 2.) & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
+ 3.) & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
+ \end{tabular}
+ \end{center}
- Most quotient packages take only an original theorem involving raw
- types and lift it. The procedure in our package takes both an
- original theorem involving raw types and a statement of the theorem
- that it is supposed to produce. To simplify the use of the quotient
- package we additionally provide an automated statement translation
- mechanism which can produce the latter automatically given a list of
- quotient types. It is possible that a user wants to lift only some
- occurrences of a raw type. In this case the user specifies the
- complete lifted goal instead of using the automated mechanism.
+ \noindent
+ 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.
+
+ 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.
In the following we will first define the statement of the
- regularized theorem based on the original theorem and the goal
- theorem. Then we define the statement of the injected theorem, based
- on the regularized theorem and the goal. We then show the 3 proofs,
- all three can be performed independently from each other.
+ regularized theorem based on @{text "raw_thm"} and the
+ @{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,
+ which can all be performed independently from each other.
- We define the function @{text REG}, which takes the statements
- of the raw theorem and the lifted theorem (both as terms) and
- returns the statement of the regularized version. The intuition
+ We 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
@@ -847,6 +862,7 @@
@{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
@{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
\end{cases}$\smallskip\\
+ \\
\multicolumn{3}{@ {}l}{universal quantifiers:}\\
@{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ &
$\begin{cases}
@@ -870,9 +886,10 @@
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.
- Next we define the function @{text INJ} which takes the statement of
- the regularized theorems and the statement of the lifted theorem both as
- terms and returns the statement of the injected theorem:
+
+ Next we define the function @{text INJ} which takes as argument
+ @{text "reg_thm"} and @{text "quot_thm"} (both as
+ terms) and returns @{text "inj_thm"}:
\begin{center}
\begin{tabular}{rcl}
@@ -902,103 +919,81 @@
\end{tabular}
\end{center}
- \noindent where the cases for existential quantifiers and unique existential
- quantifiers have been omitted for clarity; are similar to universal quantifier.
+ \noindent
+ where again the cases for existential quantifiers and unique existential
+ quantifiers have been omitted.
- We can now define the subgoals that will imply the lifted theorem. Given
- the statement of the original theorem @{term t} and the statement of the
- goal @{term g} the regularization subgoal is @{term "t \<longrightarrow> REG(t, g)"},
- the injection subgoal is @{term "REG(t, g) = INJ(REG(t, g), g)"} and the
- cleaning subgoal is @{term "INJ(REG(t, g), g) = g"}. We will now describe
- the three tactics provided for these three subgoals.
+ In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
+ start with an implication. Isabelle provides \emph{mono} rules that can split up
+ the implications into simpler implication subgoals. This succeeds for every
+ monotone connectives, except in places wher the function @{text REG} inserted,
+ for example, a quantifier by a bounded quantifier. In this case we have
+ rules of the form
- The injection and cleaning subgoals are always solved if the appropriate
- respectfulness and preservation theorems are given. It is not the case
- with regularization; sometimes a theorem given by the user does not
- imply a regularized version and a stronger one needs to be proved. This
- is outside of the scope of the quotient package, so such obligations are
- left to the user. Take a simple statement for integers @{text "0 \<noteq> 1"}.
- It does not follow from the fact that @{text "(0, 0) \<noteq> (1, 0)"} because
- of regularization. The raw theorem only shows that particular items in the
- equivalence classes are not equal. A more general statement saying that
- the classes are not equal is necessary.
+ @{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)"}
+
+ \noindent
+ They decompose a bounded quantifier on the right-hand side, but are only applicable
+ if we can prove that
- In the proof of the regularization subgoal we always start with an implication.
- Isabelle provides a set of \emph{mono} rules, that are used to split implications
- of similar statements into simpler implication subgoals. These are enhanced
- with special quotient theorem in the regularization proof. Below we only show
- the versions for the universal quantifier. For the existential quantifier
- and abstraction they are analogous.
+ @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
- First, bounded universal quantifiers can be removed on the right:
-
- @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]}
-
- They can be removed anywhere if the relation is an equivalence relation:
-
- @{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]}
-
- And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation:
+ \noindent
+ And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation
+ and we can prove
@{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+ \noindent
The last theorem is new in comparison with Homeier's package. There the
- injection procedure would be used to prove goals with such shape, and there
- the equivalence assumption would be used. We use the above theorem directly
- also for composed relations where the range type is a type for which we know an
- equivalence theorem. This allows separating regularization from injection.
+ injection procedure would be used to prove such goals, and there
+ 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''.
- The injection proof starts with an equality between the regularized theorem
- and the injected version. The proof again follows by the structure of the
- two terms, and is defined for a goal being a relation between these two terms.
+ The secon proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"}, starts with an equality.
+ The proof again follows the structure of the
+ two underlying terms, and is defined for a goal being a relation between these two terms.
\begin{itemize}
- \item For two constants, an appropriate constant respectfulness assumption is used.
- \item For two variables, we use the assumptions proved in regularization.
- \item For two abstractions, they are eta-expanded and beta-reduced.
- \item For two applications, if the right side is an application of
- @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} we
- can reduce the injected pair using the theorem:
+ \item For two constants an appropriate constant respectfulness lemma is applied.
+ \item For two variables, we use the assumptions proved in the regularization step.
+ \item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
+ \item For two applications, we check that the right-hand side is an application of
+ @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"}. If yes then we
+ can apply the theorem:
@{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
- otherwise we introduce an appropriate relation between the subterms
+ Otherwise we introduce an appropriate relation between the subterms
and continue with two subgoals using the lemma:
@{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
-
\end{itemize}
- The cleaning subgoal has been defined in such a way that
- establishing the goal theorem now consists only on rewriting the
- injected theorem with the preservation theorems and quotient
- definitions. First for all lifted constants, their definitions
+ 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
are used to fold the @{term Rep} with the raw constant. Next for
- all lambda abstractions and quantifications the lambda and
+ all abstractions and quantifiers the lambda and
quantifier preservation theorems are used to replace the
- variables that include raw types with respects by quantification
+ variables that include raw types with respects by quantifiers
over variables that include quotient types. We show here only
- the lambda preservation theorem; assuming
- @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}
- hold, we have:
+ the lambda preservation theorem. Given
+ @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
- @{thm [display, indent=10] (concl) lambda_prs[no_vars]}
+ @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
\noindent
- holds. Next relations over lifted types are folded to equality.
- The following theorem has been shown in Homeier~\cite{Homeier05}:
+ Next, relations over lifted types are folded to equalities.
+ For this the following theorem has been shown in Homeier~\cite{Homeier05}:
@{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
\noindent
- Finally the user given preservation theorems, that allow using
- higher level operations and containers of types being lifted.
- We show the preservation theorem for @{term map}. Again assuming
- that @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"} hold,
- we have:
-
- @{thm [display, indent=10] (concl) map_prs(1)[of R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1 R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2]}
-
+ Finally, we rewrite with the preservation theorems. This will result
+ in two equal terms that can be solved by reflexivity.
*}
section {* Examples \label{sec:examples} *}
@@ -1009,27 +1004,32 @@
In this section we will show, a complete interaction with the quotient package
for defining the type of integers by quotienting pairs of natural numbers and
- lifting theorems to integers. Our quotient package is fully compatible with
+ lifting theorems to integers. Oeur quotient package is fully compatible with
Isabelle type classes, but for clarity we will not use them in this example.
In a larger formalization of integers using the type class mechanism would
provide many algebraic properties ``for free''.
A user of our quotient package first needs to define a relation on
the raw type, by which the quotienting will be performed. We give
- the same integer relation as the one presented in the introduction:
+ the same integer relation as the one presented in \eqref{natpairequiv}:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
- \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~%
- @{text "(m :: nat, n) int_rel (p, q) = (m + q = n + p)"}
+ \begin{tabular}{@ {}l}
+ \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\
+ \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
+ \end{tabular}
\end{isabelle}
\noindent
- Next the quotient type is defined. This leaves a proof obligation that the
- relation is an equivalence relation which is solved automatically using the
- definitions:
+ Next the quotient type is defined. This generates a proof obligation that the
+ relation is an equivalence relation, which is solved automatically using the
+ definition and extensionality:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
- \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}
+ \begin{tabular}{@ {}l}
+ \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\
+ \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}
+ \end{tabular}
\end{isabelle}
\noindent
@@ -1037,7 +1037,7 @@
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\begin{tabular}{@ {}l}
- \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\
+ \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{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
@@ -1046,39 +1046,48 @@
\end{isabelle}
\noindent
- Lets first take a simple theorem about addition on the raw level:
+ 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"}
\end{isabelle}
\noindent
- When the user tries to lift a theorem about integer addition, the respectfulness
- proof obligation is left, so let us prove it first:
+ If the user attempts to lift this theorem, all proof obligations are
+ automatically discharged, except the respectfulness
+ proof for @{text "plus_raw"}:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
- \isacommand{lemma}~~@{text "[quot_respect]:
+ \begin{tabular}{@ {}l}
+ \isacommand{lemma}~~@{text "[quot_respect]:\\
(int_rel \<doublearr> int_rel \<doublearr> int_rel) plus_raw plus_raw"}
+ \end{tabular}
\end{isabelle}
\noindent
- Can be proved automatically by the system just by unfolding the definition
+ This can be dischaged automatically by Isabelle when telling it to unfold the definition
of @{text "\<doublearr>"}.
- Now the user can either prove a lifted lemma explicitly:
+ 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"}
\end{isabelle}
\noindent
- Or in this simple case use the automated translation mechanism:
+ or by the completely automated mode by stating:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"}
\end{isabelle}
\noindent
- obtaining the same result.
+ Both methods give the same result, namely
+
+ @{text [display, indent=10] "0 + x = x"}
+
+ \noindent
+ Although seemingly simple, arriving at this result without the help of a quotient
+ package requires substantial reasoning effort.
*}
section {* Conclusion and Related Work\label{sec:conc}*}