nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:1f9360daf6e1
+:5606de1e5034
 section {* Introduction *}
 text {*
-\begin{flushright}
+\noindent
-{\em ``Not using a [quotient] package has its advantages: we do not have to\\
+One might think they have been studied to death, but in the context of
-collect all the theorems we shall ever want into one giant list;''}\\
+theorem provers many questions concerning quotients are far from settled. In
-Larry Paulson \cite{Paulson06}
+this paper we address the question how a convenient reasoning infrastructure
-\end{flushright}
+for quotient constructions can be established in Isabelle/HOL, a popular
+generic theorem prover. Higher-Order Logic (HOL) consists
-\noindent
+of a small number of axioms and inference rules over a simply-typed
-Isabelle is a popular generic theorem prover in which many logics can be
+term-language. Safe reasoning in HOL is ensured by two very restricted
-implemented. The most widely used one, however, is Higher-Order Logic
+mechanisms for extending the logic: one is the definition of new constants
-(HOL). This logic consists of a small number of axioms and inference rules
+in terms of existing ones; the other is the introduction of new types by
-over a simply-typed term-language. Safe reasoning in HOL is ensured by two
+identifying non-empty subsets in existing types. It is well understood how
-very restricted mechanisms for extending the logic: one is the definition of
+to use both mechanisms for dealing with quotient constructions in HOL (see
-new constants in terms of existing ones; the other is the introduction of
+\cite{Homeier05,Paulson06}).  For example the integers in Isabelle/HOL are
-new types by identifying non-empty subsets in existing types. It is well
+constructed by a quotient construction over the type @{typ "nat \<times> nat"} and
-understood how to use both mechanisms for dealing with quotient
+the equivalence relation
-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}
 \noindent
 This constructions yields the new type @{typ int} and definitions for @{text
 "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
 m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
 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}
 \noindent
 which states that two lists are equivalent if every element in one list is
 Quotients are important in a variety of areas, but they are really ubiquitous in
 the area of reasoning about programming language calculi. A simple example
 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}
 \noindent
 The problem with this definition arises, for instance, when one attempts to
 sets or $\alpha$-equated lambda-terms 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 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.
 The purpose of a \emph{quotient package} is to ease the lifting of theorems
 and automate the reasoning as much as possible. In the
 existing type to elements in the new type and vice versa, and can be uniquely
 identified by their quotient type. For example for the integer quotient construction
 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}
 \noindent
 We therefore often write @{text Abs_int} and @{text Rep_int} if the
 between the non-empty subset and elements in the new type. They are
 necessary for making definitions involving the new type. For example @{text
 "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}
 \noindent
 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}
 \noindent
 that none of them can deal with slightly more complicated definitions involving
 \emph{compositions} of quotients. Such compositions are needed for example
 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
 terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is
 that the method  used in the existing quotient
 packages of just taking the representation of the arguments and then taking
 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
 existing quotient packages by introducing an intermediate step and reasoning
 about flattening of lists of finite sets. However, this remedy is rather
 cumbersome and inelegant in light of our work, which can deal with such
 definitions directly. The solution is that we need to build aggregate
 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
 will present a formal definition of our aggregate abstraction and
 representation functions (this definition was omitted in \cite{Homeier05}).
 the modularity is that we are able to clearly specify what is involved
 in the lifting process (this was only hinted at in \cite{Homeier05} and
 implemented as a ``rough recipe'' in ML-code).
-The paper is organised as follows: Section \ref{sec:prelims} presents briefly
+%The paper is organised as follows: Section \ref{sec:prelims} presents briefly
-some necessary preliminaries; Section \ref{sec:type} describes the definitions
+%some necessary preliminaries; Section \ref{sec:type} describes the definitions
-of quotient types and shows how definitions of constants can be made over
+%of quotient types and shows how definitions of constants can be made over
-quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
+%quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
-and preservation; Section \ref{sec:lift} describes the lifting of theorems;
+%and preservation; Section \ref{sec:lift} describes the lifting of theorems;
-Section \ref{sec:examples} presents some examples
+%Section \ref{sec:examples} presents some examples
-and Section \ref{sec:conc} concludes and compares our results to existing
+%and Section \ref{sec:conc} concludes and compares our results to existing
-work.
+%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{isabelle}\ \ \ \ \ %%%
-\begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
+\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
-@{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\
+@{text "\<sigma>, \<tau> ::= \<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} &
-@{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} &
+@{text "t, s ::= x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"}\\
-(variables, constants, applications and abstractions)\\
 \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
 "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
 Like Homeier's, our work relies on map-functions defined for every type
 constructor taking some arguments, for example @{text map_list} for lists. Homeier
 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>"},
 we can get back to \eqref{adddef}.
 In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function
 It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
 which define equivalence relations in terms of constituent equivalence
 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}
 \noindent
 quotient theorem for composing particular quotient relations.
 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=2] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
+\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)"}
-\vspace{-.5mm}
+\end{isabelle}
 *}
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 text {*
 type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
 defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
 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}
 \noindent
 and a proof that @{text "R"} is indeed an equivalence relation. Two concrete
 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>"}
 \end{tabular}
 \end{isabelle}
 "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
 \eqref{listequiv}, respectively (the proofs about being equivalence
 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}
 \noindent
 where the right-hand side is the (non-empty) set of equivalence classes of
 @{text "R"}. The constraint in this declaration is that the type variables
 in the raw type @{text "\<sigma>"} must be included in the type variables @{text
 "\<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}
 \noindent
 As can be seen from the type, they relate the new quotient type and equivalence classes of the raw
 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}
 \noindent
 on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
 The next step in a quotient construction is to introduce definitions of new constants
 involving the quotient type. These definitions need to be given in terms of concepts
 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}
 \noindent
 where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)
 and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be
 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"}~~%
 \isacommand{is}~~@{text "flat"}
 \end{tabular}
 %%% in this paragraph. I can imagine roughly what the following
 %%% sentence `The $\sigma$s' are given by the matchers for the
 %%% $\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.
 To see how these definitions pan out in practise, let us return to our
 example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
 @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
 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
 simplify this function by rewriting with the usual laws about @{text
 "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
 for function types in \eqref{ABSREP}, we do not have to
 distinguish between arguments and results, but can deal with them uniformly.
 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
 type of the defined quotient constant @{text "c"}. This data can be easily
 generated from the declaration given by the user.
 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
 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)"}
 \end{isabelle}
 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 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
 theorems}. However, unlike his quotient package, we might have several
 respectfulness theorems for one constant---he has at most one.
 Before lifting a theorem, we require the user to discharge
 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}
 \noindent
 %%% and its corresponding lifted constant?
 %%% 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
 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,
 the implications into simpler implicational subgoals. This succeeds for every
 monotone connective, except in places where the function @{text REG} replaced,
 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
 bounded quantifier anywhere if R is an equivalence relation or
 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}
 %%% 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
 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,
 \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"} 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
 establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
 achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
 variables that include raw types with respects by quantifiers
 over variables that include quotient types. We show here only
 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
 in two equal terms that can be solved by reflexivity.
 *}
 A user of our quotient package first needs to define a relation on
 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)"}
 \end{tabular}
 \end{isabelle}
 \noindent
 Next the quotient type must be defined. This generates a proof obligation that the
 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)"}
 \end{tabular}
 \end{isabelle}
 \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"}\\
 \end{tabular}
 \end{isabelle}
 \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}
 \noindent
 If the user lifts this theorem, the quotient package performs all the lifting
 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"}
 \end{tabular}
 \end{isabelle}
 \noindent
 It can be discharged automatically by Isabelle when hinting to unfold the definition
 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
+Both methods give the same result, namely @{text "0 + x = x"}
-@{text [display, indent=10] "0 + x = x"}
-\noindent
 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}).
 *}

changeset 2443	5606de1e5034
parent 2437	319f469b8b67
child 2444	d769c24094cf