nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:d1ab5d2d6926
+:8ddf1330f2ed
 @{text "\<union>"}, as list append.
 An area where quotients are ubiquitous is reasoning about programming language
 calculi. A simple example is the lambda-calculus, whose raw terms are defined as
-@{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
+\end{isabelle}
 \noindent
 The problem with this definition arises when one attempts to
 prove formally, for example, the substitution lemma \cite{Barendregt81} by induction
 over the structure of terms. This can be fiendishly complicated (see
 It is feasible to to 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 definitions and reasoning as much as possible. In the
+and automate the reasoning as much as possible. In the
 context of HOL, there have been a few quotient packages already
 \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
 \cite{Homeier05} implemented in HOL4.  The fundamental construction these
 quotient packages perform can be illustrated by the following picture:
 \end{tikzpicture}
 \end{center}
 \noindent
-The starting point is an existing type, often referred to as the \emph{raw
+The starting point is an existing type, to which we often refer as the
-type}, over which an equivalence relation given by the user is defined. With
+\emph{raw type}, over which an equivalence relation given by the user is
-this input the package introduces a new type, to which we refer as the
+defined. With this input the package introduces a new type, to which we
-\emph{quotient type}. This type comes with an \emph{abstraction} and a
+refer as the \emph{quotient type}. This type comes with an
-\emph{representation} function, written @{text Abs} and @{text
+\emph{abstraction} and a \emph{representation} function, written @{text Abs}
-Rep}.\footnote{Actually slightly more basic functions are given; the @{text Abs}
+and @{text Rep}.\footnote{Actually slightly more basic functions are given;
-and @{text Rep} need to be derived from them. We will show the details
+the functions @{text Abs} and @{text Rep} need to be derived from them. We
-later. } These functions relate elements in the existing type to ones in the
+will show the details later. } These functions relate elements in the
-new type and vice versa; they can be uniquely identified by their type. For
+existing type to ones in the new type and vice versa; they can be uniquely
-example for the integer quotient construction the types of @{text Abs} and
+identified by their type. For example for the integer quotient construction
-@{text Rep} are
+the types of @{text Abs} and @{text Rep} are
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
 \end{isabelle}
 \noindent
-However we often leave this typing information implicit for better
+We therefore often write @{text Abs_int} and @{text Rep_int} if the
-readability, but sometimes write @{text Abs_int} and @{text Rep_int} if the
+typing information is important.
-typing information is important. Every abstraction and representation
-function stands for an isomorphism between the non-empty subset and elements
+Every abstraction and representation function stands for an isomorphism
-in the new type. They are necessary for making definitions involving the new
+between the non-empty subset and elements in the new type. They are
-type. For example @{text "0"} and @{text "1"} of type @{typ int} can be
+necessary for making definitions involving the new type. For example @{text
-defined as
+"0"} and @{text "1"} of type @{typ int} can be defined as
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-@{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"}
+\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
-@{text [display, indent=10] "add n m \<equiv> Abs (add_pair (Rep n) (Rep m))"}
+@{text [display, indent=10] "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
 \noindent
 where we take the representation of the arguments @{text n} and @{text m},
 add them according to the function @{text "add_pair"} and then take the
 abstraction of the result.  This is all straightforward and the existing
 @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 \noindent
 The quotient package should provide us with a definition for @{text "\<Union>"} in
-terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having
+terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is
-the type @{text "\<alpha> fset \<Rightarrow> \<alpha> list"} and @{text "\<alpha> list \<Rightarrow> \<alpha> fset"},
+that the method  used in the existing quotient
-respectively). The problem is that the method  used in the existing quotient
 packages of just taking the representation of the arguments and then take
 the abstraction of the result is \emph{not} enough. The reason is that case in case
 of @{text "\<Union>"} we obtain the incorrect definition
 @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
 Such maps for most common types (list, pair, sum,
 option, \ldots) are described in Homeier, and we assume that @{text "map"}
 is the function that returns a map for a given type.
+{\it say something about our use of @{text "\<sigma>s"}}
 *}
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 text {*
 The first step in a quotient constructions is to take a name for the new
-type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation defined over a
+type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
-raw type, say @{text "\<sigma>"}. The equivalence relation for the quotient
+defined over a raw type, say @{text "\<sigma>"}. The type of this equivalence
-construction, lets say @{text "R"}, must then be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
+relation must be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
-bool"}. The user-visible part of the declaration is therefore
+the declaration is therefore
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
 \end{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
-and relating the new quotient type and equivalence classes of the raw
+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}\ \ \ \ \ \ \ \ \ \ %%%
 @{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)"}
 @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
 \noindent
 holds (for the proof see \cite{Homeier05}).
-The next step is to introduce new definitions involving the quotient type,
+The next step in a quotient construction is to introduce new definitions
-which need to be defined in terms of concepts of the raw type (remember this
+involving the quotient type, which need to be defined in terms of concepts
-is the only way how toe be able to extend HOL with new definitions). For the
+of the raw type (remember this is the only way how to extend HOL
-user visible is the declaration
+with new definitions). For the user visible is the declaration
 \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 are involved). Two examples are
+in places where a quotient and raw type are involved). Two concrete examples are
 \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"}~~%
 \end{tabular}
 \end{isabelle}
 \noindent
 The first one declares zero for integers and the second the operator for
-building unions of finite sets. The problem for us is that from such
+building unions of finite sets.
-declarations we need to derive proper definitions using the @{text "Abs"}
-and @{text "Rep"} functions for the quotient types involved. The data we
+The problem for us is that from such declarations we need to derive proper
-rely on is the given quotient type @{text "\<tau>"} and the raw type @{text "\<sigma>"}.
+definitions using the @{text "Abs"} and @{text "Rep"} functions for the
-They allow us to define aggregate abstraction and representation functions
+quotient types involved. The data we rely on is the given quotient type
-using the functions @{text "ABS (\<sigma>, \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose
+@{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define aggregate
-clauses are given below. The idea behind them is to recursively descend into
+abstraction and representation functions using the functions @{text "ABS (\<sigma>,
-both types and generate the appropriate @{text "Abs"} and @{text "Rep"}
+\<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses are given below. The idea behind
-in places where the types differ. Therefore we returning just the identity
+them is to recursively descend into types @{text \<sigma>} and @{text \<tau>}, and generate the appropriate
-whenever the types are equal.
+@{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
+we returning just the identity whenever the types are equal. All clauses
+are as follows:
 \begin{center}
-\begin{longtable}{rcl}
+\begin{tabular}{rcl}
 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
-@{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
+@{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
-@{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
+@{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
 \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\
 @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
 @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
 @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
 @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
 \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
-@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s')))"}\\
+@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
-@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>q"}
+@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
-\end{longtable}
+\end{tabular}
 \end{center}
 %
 \noindent
 where in the last two clauses we have that the quotient type @{text "\<alpha>s
-\<kappa>\<^isub>q"} is a quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
+\<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
 @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
 list"}). The quotient construction ensures that the type variables in @{text
 "\<rho>s"} must be amongst the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
-matchers for the @{text "\<alpha>s"} when matching @{text "\<sigma>s \<kappa>\<^isub>q"} against
+matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
-@{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the same
+@{text "\<sigma>s \<kappa>"}.  The
-type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.  The
 function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
 type as follows:
 %
 \begin{center}
-\begin{longtable}{rcl}
+\begin{tabular}{rcl}
 @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
-@{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id"}\\
+@{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
 @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
 @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
-\end{longtable}
+\end{tabular}
 \end{center}
 %
 \noindent
 In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} as
-term variables @{text a}, and in the last clause build an abstraction over all
+term variables @{text a}. In the last clause we build an abstraction over all
-term-variables inside the aggregate map-function generated by @{text "MAP'"}.
+term-variables inside the aggregate map-function generated by the auxiliary function
-This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"},
+@{text "MAP'"}.
-out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. In this case @{text MAP}
+The need of aggregate map-functions can be appreciated if we build quotients,
-generates the aggregate map-function:
+say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types of the form @{text "(\<alpha> list) \<times> \<beta>"}.
+In this case @{text MAP} generates the aggregate map-function:
 @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
 \noindent
-Returning to our example about @{term "concat"} and @{term "fconcat"} which have the
+which we need to define the aggregate abstraction and representation functions.
-types @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. Feeding this
-into @{text ABS} gives us the abstraction function:
+To se how these definitions pan out in practise, let us return to our
+example about @{term "concat"} and @{term "fconcat"}, where we have types
+@{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
+fset"}. Feeding them into @{text ABS} gives us the abstraction function
 @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
 \noindent
-where we already performed some @{text "\<beta>"}-simplifications. In our
+after some @{text "\<beta>"}-simplifications. In our implementation we further
-implementation we further simplify this by noticing the usual laws about
+simplify this abstraction function employing the usual laws about @{text
-@{text "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f
+"map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =
-\<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function
+id \<circ> f = f"}. This gives us the abstraction function
 @{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
 \noindent
 which we can use for defining @{term "fconcat"} as follows
 @{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
 \noindent
 Note that by using the operator @{text "\<singlearr>"} we do not have to
-distinguish between arguments and results: teh representation and abstraction
+distinguish between arguments and results: the representation and abstraction
-functions are just inverses which we can combine using @{text "\<singlearr>"}.
+functions are just inverses of each other, which we can combine using
-So all our definitions are of the general form
+@{text "\<singlearr>"} to deal uniformly with arguments of functions and
+their result. As a result, all definitions in the quotient package
+are of the general form
 @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
 \noindent
-where @{text \<sigma>} is the type of @{text "t"} and @{text "\<tau>"} the type of the
+where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
-newly defined quotient constant @{text "c"}. To ensure we obtained a correct
+type of the defined quotient constant @{text "c"}. To ensure we
-definition, we can prove:
+obtained a correct definition, we can prove:
 \begin{lemma}
 If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
 and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"},
 then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
 @{text "\<tau> \<Rightarrow> \<sigma>"}.
 \end{lemma}
 \begin{proof}
-By induction of the definitions of @{text "ABS"}, @{text "REP"} and @{text "MAP"}.
+By induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
+and @{text "MAP"}. The cases of equal and function types are straightforward
+(the latter follows from @{text "\<singlearr>"} having the type
+@{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). The case of equal
+type constructors follows by observing that a map-function after applying
+the functions @{text "ABS (\<sigma>s, \<tau>s)"} produce a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.
+The interesting case is the one with unequal type constructors. Since we know the
+quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have that @{text "Abs_\<kappa>\<^isub>q"}
+is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}, that can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"}
+where the type variables @{text "\<alpha>s"} are instantiated with @{text "\<tau>s"}. The
+complete type can be calculated by observing that @{text "MAP (\<rho>s \<kappa>)"} after applying
+the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it, returns a term of type
+@{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is equivalent to  @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}
+as desired.\qed
 \end{proof}
 \noindent
-This lemma fails for the abstraction and representation functions used in,
+The reader should note that this lemma fails for the abstraction and representation
-for example, Homeier's quotient package.
+functions used, for example, in Homeier's quotient package.
 *}
-subsection {* Respectfulness *}
+section {* Respectfulness and Preservation *}
 text {*
+Before we can lift theorems involving the raw types to theorems over
-A respectfulness lemma for a constant states that the equivalence
+quotient types, we have to impose some restrictions. The reason is that not
+all theorems can be lifted. Homeier formulates these restrictions in terms
+of \emph{respectfullness} and \emph{preservation} of constants occuring in
+theorems.
+The respectfulness property for a constant states that it essentially
+respects the equivalence relation involved in the quotient. An example
+is the function returning bound variables of a lambda-term (see \eqref{lambda})
+and @{text "\<alpha>"}-equivalence. It will turn out that this function is not
+respectful.
+To state the respectfulness property we have to define \emph{aggregate equivalence
+relations}.
+@{text [display] "GIVE DEFINITION HERE"}
 class returned by this constant depends only on the equivalence
 classes of the arguments applied to the constant. To automatically
 lift a theorem that talks about a raw constant, to a theorem about
 the quotient type a respectfulness theorem is required.
 A respectfulness condition for a constant can be expressed in
 terms of an aggregate relation between the constant and itself,
-for example the respectfullness for @{term "append"}
+for example the respectfullness for @{text "append"}
 can be stated as:
-@{thm [display, indent=10] append_rsp[no_vars]}
+@{text [display, indent=10] "(R \<doublearr> R \<doublearr> R) append append"}
 \noindent
 Which after unfolding the definition of @{term "op ===>"} is equivalent to:
 @{thm [display, indent=10] append_rsp_unfolded[no_vars]}
 element of @{term b'} is in relation with the appropriate element of
 @{term b}.
 *}
-subsection {* Preservation *}
 text {*
 Sometimes a non-lifted polymorphic constant is instantiated to a
 type being lifted. For example take the @{term "op #"} which inserts
 an element in a list of pairs of natural numbers. When the theorem

changeset 2238	8ddf1330f2ed
parent 2237	d1ab5d2d6926
child 2239	ff997de1bd73