--- a/Quotient-Paper/Paper.thy Fri Aug 27 13:57:00 2010 +0800
+++ b/Quotient-Paper/Paper.thy Fri Aug 27 16:00:19 2010 +0800
@@ -66,26 +66,24 @@
section {* Introduction *}
text {*
- \begin{flushright}
- {\em ``Not using a [quotient] package has its advantages: we do not have to\\
- collect all the theorems we shall ever want into one giant list;''}\\
- Larry Paulson \cite{Paulson06}
- \end{flushright}
+ \noindent
+ One might think they have been studied to death, but in the context of
+ theorem provers many questions concerning quotients are far from settled. In
+ this paper we address the question how a convenient reasoning infrastructure
+ for quotient constructions can be established in Isabelle/HOL, a popular
+ generic theorem prover. Higher-Order Logic (HOL) consists
+ of a small number of axioms and inference rules over a simply-typed
+ term-language. Safe reasoning in HOL is ensured by two very restricted
+ mechanisms for extending the logic: one is the definition of new constants
+ in terms of existing ones; the other is the introduction of new types by
+ identifying non-empty subsets in existing types. It is well understood how
+ to use both mechanisms for dealing with quotient constructions in HOL (see
+ \cite{Homeier05,Paulson06}). For example the integers in Isabelle/HOL are
+ constructed by a quotient construction over the type @{typ "nat \<times> nat"} and
+ the equivalence relation
- \noindent
- Isabelle is a popular generic theorem prover in which many logics can be
- implemented. The most widely used one, however, is Higher-Order Logic
- (HOL). This logic consists of a small number of axioms and inference rules
- over a simply-typed term-language. Safe reasoning in HOL is ensured by two
- very restricted mechanisms for extending the logic: one is the definition of
- new constants in terms of existing ones; the other is the introduction of
- new types by identifying non-empty subsets in existing types. It is well
- understood how to use both mechanisms for dealing with quotient
- constructions in HOL (see \cite{Homeier05,Paulson06}). For example the
- integers in Isabelle/HOL are constructed by a quotient construction over the
- type @{typ "nat \<times> nat"} and the equivalence relation
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{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{natpairequiv}
\end{isabelle}
@@ -100,7 +98,7 @@
Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"},
by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
\end{isabelle}
@@ -115,7 +113,7 @@
is the lambda-calculus, whose raw terms are defined as
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
\end{isabelle}
@@ -136,7 +134,7 @@
from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
(similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.
- It is feasible to do this work manually, if one has only a few quotient
+ 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.
@@ -194,7 +192,7 @@
the types of @{text Abs} and @{text Rep} are
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
\end{isabelle}
@@ -208,7 +206,7 @@
"0"} and @{text "1"} of type @{typ int} can be defined as
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}
\end{isabelle}
@@ -216,7 +214,7 @@
Slightly more complicated is the definition of @{text "add"} having type
@{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
\hfill\numbered{adddef}
\end{isabelle}
@@ -231,13 +229,19 @@
in case of quotienting lists to yield finite sets and the operator that
flattens lists of lists, defined as follows
- @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm}
+ @{thm concat.simps(2)[THEN eq_reflection, no_vars]}
+ \end{isabelle}
\noindent
We expect that the corresponding operator on finite sets, written @{term "fconcat"},
builds finite unions of finite sets:
- @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{thm fconcat_empty[THEN eq_reflection, no_vars]}\hspace{10mm}
+ @{thm fconcat_insert[THEN eq_reflection, no_vars]}
+ \end{isabelle}
\noindent
The quotient package should automatically provide us with a definition for @{text "\<Union>"} in
@@ -247,7 +251,9 @@
the abstraction of the result is \emph{not} enough. The reason is that in case
of @{text "\<Union>"} we obtain the incorrect definition
- @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
+ \end{isabelle}
\noindent
where the right-hand side is not even typable! This problem can be remedied in the
@@ -258,7 +264,9 @@
representation and abstraction functions, which in case of @{text "\<Union>"}
generate the following definition
- @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
+ \end{isabelle}
\noindent
where @{term map_list} is the usual mapping function for lists. In this paper we
@@ -281,36 +289,38 @@
implemented as a ``rough recipe'' in ML-code).
- The paper is organised as follows: Section \ref{sec:prelims} presents briefly
- some necessary preliminaries; Section \ref{sec:type} describes the definitions
- of quotient types and shows how definitions of constants can be made over
- quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
- and preservation; Section \ref{sec:lift} describes the lifting of theorems;
- Section \ref{sec:examples} presents some examples
- and Section \ref{sec:conc} concludes and compares our results to existing
- work.
+ %The paper is organised as follows: Section \ref{sec:prelims} presents briefly
+ %some necessary preliminaries; Section \ref{sec:type} describes the definitions
+ %of quotient types and shows how definitions of constants can be made over
+ %quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
+ %and preservation; Section \ref{sec:lift} describes the lifting of theorems;
+ %Section \ref{sec:examples} presents some examples
+ %and Section \ref{sec:conc} concludes and compares our results to existing
+ %work.
*}
-section {* Preliminaries and General Quotients\label{sec:prelims} *}
+section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
text {*
+ \noindent
We give in this section a crude overview of HOL and describe the main
definitions given by Homeier for quotients \cite{Homeier05}.
At its core, HOL is based on a simply-typed term language, where types are
recorded in Church-style fashion (that means, we can always infer the type of
a term and its subterms without any additional information). The grammars
- for types and terms are as follows
+ for types and terms are
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
- @{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\
- @{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} &
- (variables, constants, applications and abstractions)\\
+ \begin{isabelle}\ \ \ \ \ %%%
+ \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+ @{text "\<sigma>, \<tau> ::= \<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} &
+ @{text "t, s ::= x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"}\\
\end{tabular}
\end{isabelle}
\noindent
+ with types being either type variables or type constructors and terms
+ being variables, constants, applications or abstractions.
We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
@{text "\<sigma>s"} to stand for collections of type variables and types,
respectively. The type of a term is often made explicit by writing @{text
@@ -331,13 +341,17 @@
describes in \cite{Homeier05} map-functions for products, sums, options and
also the following map for function types
- @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{thm fun_map_def[no_vars, THEN eq_reflection]}
+ \end{isabelle}
\noindent
Using this map-function, we can give the following, equivalent, but more
uniform definition for @{text add} shown in \eqref{adddef}:
- @{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
+ \end{isabelle}
\noindent
Using extensionality and unfolding the definition of @{text "\<singlearr>"},
@@ -354,14 +368,16 @@
relations. For example given two equivalence relations @{text "R\<^isub>1"}
and @{text "R\<^isub>2"}, we can define an equivalence relations over
products as follows
- %
- @{text [display, indent=10] "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
+ \end{isabelle}
\noindent
Homeier gives also the following operator for defining equivalence
relations over function types
%
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
\hfill\numbered{relfun}
\end{isabelle}
@@ -433,9 +449,9 @@
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=2] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
-
- \vspace{-.5mm}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
+ \end{isabelle}
*}
section {* Quotient Types and Quotient Definitions\label{sec:type} *}
@@ -447,7 +463,7 @@
relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
the quotient type declaration is therefore
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
\isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
\end{isabelle}
@@ -456,7 +472,7 @@
examples are
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
\isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\
\isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}
@@ -471,7 +487,7 @@
relations is omitted). Given this data, we define for declarations shown in
\eqref{typedecl} the quotient types internally as
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
\isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
\end{isabelle}
@@ -482,7 +498,7 @@
"\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will then provide us with the following
abstraction and representation functions
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
\end{isabelle}
@@ -491,7 +507,7 @@
type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
to work with the following derived abstraction and representation functions
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
\end{isabelle}
@@ -513,7 +529,7 @@
of the raw type (remember this is the only way how to extend HOL
with new definitions). For the user the visible part of such definitions is the declaration
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
\isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
\end{isabelle}
@@ -523,7 +539,7 @@
given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ
in places where a quotient and raw type is involved). Two concrete examples are
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
\isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
\isacommand{quotient\_definition}~~@{text "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}~~%
@@ -609,8 +625,10 @@
%%% $\alpha$s$ when matching $\varrho$s $\kappa$ against $\sigma$s
%%% $\kappa$.' means, but also think that it is too vague.
- @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"}
-
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "\<lambda>a b. map_prod (map_list a) b"}
+ \end{isabelle}
+
\noindent
which is essential in order to define the corresponding aggregate
abstraction and representation functions.
@@ -621,7 +639,9 @@
fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
the abstraction function
- @{text [display, indent=10] "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
+ \end{isabelle}
\noindent
In our implementation we further
@@ -629,12 +649,16 @@
"map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
id \<circ> f = f"}. This gives us the simpler abstraction function
- @{text [display, indent=10] "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+ \end{isabelle}
\noindent
which we can use for defining @{term "fconcat"} as follows
- @{text [display, indent=10] "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
+ \end{isabelle}
\noindent
Note that by using the operator @{text "\<singlearr>"} and special clauses
@@ -643,7 +667,9 @@
Consequently, all definitions in the quotient package
are of the general form
- @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}
+ \end{isabelle}
\noindent
where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
@@ -691,7 +717,7 @@
notable is the bound variable function, that is the constant @{text bn}, defined
for raw lambda-terms as follows
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
@{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
@{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
@{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
@@ -741,7 +767,9 @@
constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
we generate the following proof obligation
- @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+ \end{isabelle}
\noindent
Homeier calls these proof obligations \emph{respectfulness
@@ -756,25 +784,31 @@
respectfulness proof obligations. In case of @{text bn}
this obligation is as follows
- @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
+ \end{isabelle}
\noindent
and the point is that 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 extensionality to obtain the false statement
- @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}
-
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}
+ \end{isabelle}
+
\noindent
In contrast, if we lift a theorem about @{text "append"} to a theorem describing
the union of finite sets, then we need to discharge the proof obligation
- @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
+ \end{isabelle}
\noindent
To do so, we have to establish
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{isabelle}\ \ \ \ \ %%%
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}
@@ -801,13 +835,17 @@
%%% Cezary: I think this would be a nice thing to do but we have not
%%% done it, the theorems need to be 'guessed' from the remaining obligations
- @{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"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "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"}
+ \end{isabelle}
\noindent
where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have
- @{text [display, indent=10] "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}
+ \end{isabelle}
\noindent
under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
@@ -1000,7 +1038,9 @@
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)"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
+ \end{isabelle}
\noindent
They decompose a bounded quantifier on the right-hand side. We can decompose a
@@ -1008,7 +1048,9 @@
if it is a relation over function types with the range being an equivalence
relation. If @{text R} is an equivalence relation we can prove that
- @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
+ \end{isabelle}
\noindent
If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
@@ -1016,7 +1058,9 @@
%%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we
%%% should include a proof sketch?
- @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+ \end{isabelle}
\noindent
The last theorem is new in comparison with Homeier's package. There the
@@ -1038,12 +1082,16 @@
@{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
can apply the theorem:
- @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{term "R x y \<longrightarrow> R x (Rep (Abs y))"}
+ \end{isabelle}
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)"}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{text "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
+ \end{isabelle}
\end{itemize}
We defined the theorem @{text "inj_thm"} in such a way that
@@ -1058,14 +1106,18 @@
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[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
+ \end{isabelle}
\noindent
Next, relations over lifted types can be rewritten to equalities
over lifted type. Rewriting is performed with the following theorem,
which has been shown by Homeier~\cite{Homeier05}:
- @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{thm (concl) Quotient_rel_rep[no_vars]}
+ \end{isabelle}
\noindent
Finally, we rewrite with the preservation theorems. This will result
@@ -1089,7 +1141,7 @@
the raw type with which the quotienting will be performed. We give
the same integer relation as the one presented in \eqref{natpairequiv}:
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+ \begin{isabelle}\ \ \ \ \ %
\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)"}
@@ -1101,7 +1153,7 @@
relation is an equivalence relation, which is solved automatically using the
definition of equivalence and extensionality:
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+ \begin{isabelle}\ \ \ \ \ %
\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)"}
@@ -1111,10 +1163,11 @@
\noindent
The user can then specify the constants on the quotient type:
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+ \begin{isabelle}\ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]
- \isacommand{fun}~~@{text "add_pair"}~~\isacommand{where}~~%
+ \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 "add_pair"}\\
@@ -1124,7 +1177,7 @@
\noindent
The following theorem about addition on the raw level can be proved.
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+ \begin{isabelle}\ \ \ \ \ %
\isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
\end{isabelle}
@@ -1133,7 +1186,7 @@
automatically leaving the respectfulness proof for the constant @{text "add_pair"}
as the only remaining proof obligation. This property needs to be proved by the user:
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+ \begin{isabelle}\ \ \ \ \ %
\begin{tabular}{@ {}l}
\isacommand{lemma}~~@{text "[quot_respect]:"}\\
@{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
@@ -1145,23 +1198,19 @@
of @{text "\<doublearr>"}.
After this, the user can prove the lifted lemma as follows:
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+ \begin{isabelle}\ \ \ \ \ %
\isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
\end{isabelle}
\noindent
or by using the completely automated mode stating just:
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+ \begin{isabelle}\ \ \ \ \ %
\isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
\end{isabelle}
\noindent
- Both methods give the same result, namely
-
- @{text [display, indent=10] "0 + x = x"}
-
- \noindent
+ Both methods give the same result, namely @{text "0 + x = x"}
where @{text x} is of type integer.
Although seemingly simple, arriving at this result without the help of a quotient
package requires a substantial reasoning effort (see \cite{Paulson06}).