nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:d62c082cb56b
+:99cf23602d36
 ML {*
 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
 let
 val concl =
 Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
 in
 case concl of (_ $ l $ r) => proj (l, r)
 | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
 end);
 *}
 setup {*
 Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
 Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
 Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
 *}
 (*>*)
 section {* Introduction *}
 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 respectfullness
-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
 and Section \ref{sec:conc} concludes and compares our results to existing
 work.
 *}
 section {* Preliminaries and General Quotients\label{sec:prelims} *}
 text {*
-We describe in this section briefly the most basic notions of HOL we rely on, and
+We give in this section a crude overview of HOL and describe the main
-the important definitions given by Homeier for quotients \cite{Homeier05}.
+definitions given by Homeier for quotients \cite{Homeier05}.
-At its core HOL is based on a simply-typed term language, where types are
+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
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \noindent
 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
+type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined
-many primitive and defined constants; this includes equality, with type @{text "= :: \<sigma> \<Rightarrow>
+constants; a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
-\<sigma> \<Rightarrow> bool"}, and the identity function, with type @{text "id :: \<sigma> => \<sigma>"} (the former
+bool"}, and the identity function with type @{text "id :: \<sigma> => \<sigma>"} is
-being primitive and the latter being defined as @{text
+defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
-"\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
 An important point to note is that theorems in HOL can be seen as a subset
 of terms that are constructed specially (namely through axioms and prove
 rules). As a result we are able to define automatic proof
 procedures showing that one theorem implies another by decomposing the term
 underlying the first theorem.
-Like Homeier, our work relies on map-functions defined for every type constructor,
+Like Homeier, our work relies on map-functions defined for every type
-like @{text map} for lists. Homeier describes in \cite{Homeier05} map-functions
+constructor taking some arguments, for example @{text map} for lists. Homeier
-for products, sums,
+describes in \cite{Homeier05} map-functions for products, sums, options and
-options and also the following map for function types
+also the following map for function types
 @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
 \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"}
 \noindent
-Using extensionality and unfolding the definition, we can get back to \eqref{adddef}.
+Using extensionality and unfolding the definition of @{text "\<singlearr>"},
-In what follows we shall use the terminology @{text "map_\<kappa>"} for a map-function
+we can get back to \eqref{adddef}.
-defined for the type-constructor @{text \<kappa>}. In our implementation we have
+In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function
-a database of map-functions that can be dynamically extended.
+of the type-constructor @{text \<kappa>}. In our implementation we maintain
+a database of these map-functions that can be dynamically extended.
 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
 \noindent
 Homeier gives also the following operator for defining equivalence
 relations over function types
 %
-@{thm [display, indent=10] fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
+\hfill\numbered{relfun}
+\end{isabelle}
+\noindent
+In the context of quotients, the following two notions from are \cite{Homeier05}
+needed later on.
+\begin{definition}[Respects]\label{def:respects}
+An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
+\end{definition}
+\begin{definition}[Bounded Quantification and Bounded Abstractions]\label{def:babs}
+@{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
+and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
+\end{definition}
 The central definition in Homeier's work \cite{Homeier05} relates equivalence
 relations, abstraction and representation functions:
 \begin{definition}[Quotient Types]
 \begin{proposition}\label{funquot}
 @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"
 and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
 \end{proposition}
-\begin{definition}[Respects]\label{def:respects}
+\noindent
-An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.
+As a result, Homeier is able to build an automatic prover that can nearly
-\end{definition}
-\noindent
-As a result, Homeier was able to build an automatic prover that can nearly
 always discharge a proof obligation involving @{text "Quotient"}. Our quotient
 package makes heavy
 use of this part of Homeier's work including an extension
-to deal with compositions of equivalence relations defined as follows
+to deal with compositions of equivalence relations defined as follows:
 \begin{definition}[Composition of Relations]
 @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
-composition defined by the rule
+composition defined by @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
-%
+holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
-@{thm [mode=Rule, display, indent=10] pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
+@{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
 \end{definition}
 \noindent
-Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for
+Unfortunately, there are two predicaments with compositions of relations.
-the composition of any two quotients in not true (it is not even typable in
+First, a general quotient theorem, like the one given in Proposition \ref{funquot},
-the HOL type system). However, we can prove useful instances for compatible
+cannot be stated inside HOL, because of the restriction on types.
-containers. We will show such example in Section \ref{sec:resp}.
+Second, even if we were able to state such a quotient theorem, it
+would not be true in general. However, we can prove specific and useful
+instances of the quotient theorem. We will
+show an example in Section \ref{sec:resp}.
 *}
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 \noindent
 which introduce the type of integers and of finite sets using the
 equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
 "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
 \eqref{listequiv}, respectively (the proofs about being equivalence
-relations is omitted).  Given this data, we declare for \eqref{typedecl} internally
+relations is omitted).  Given this data, we define for declarations shown in
-the quotient types as
+\eqref{typedecl} the quotient types internally as
 \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 restriction in this declaration is that the type variables
+@{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 provide us with the following
+"\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will then provide us with the following
 abstraction and representation functions
 \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}
 on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
 definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the
 quotient type and the raw type directly, as can be seen from their type,
 namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
 respectively.  Given that @{text "R"} is an equivalence relation, the
-following property
+following property holds  for every quotient type
+(for the proof see \cite{Homeier05}).
 \begin{proposition}
 @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
 \end{proposition}
-\noindent
-holds  for every quotient type defined
-as above (for the proof see \cite{Homeier05}).
 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
 \end{tabular}
 \end{isabelle}
 \noindent
 The first one declares zero for integers and the second the operator for
-building unions of finite sets.
+building unions of finite sets (@{text "flat"} having the type
+@{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}).
 The problem for us is that from such declarations we need to derive proper
 definitions using the @{text "Abs"} and @{text "Rep"} functions for the
 quotient types involved. The data we rely on is the given quotient type
 @{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define \emph{aggregate
 abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
 \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we give below. The idea behind
-these two functions is to recursively descend into the raw types @{text \<sigma>} and
+these two functions is to simultaneously descend into the raw types @{text \<sigma>} and
 quotient types @{text \<tau>}, and generate the appropriate
 @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
 we generate just the identity whenever the types are equal. On the ``way'' down,
 however we might have to use map-functions to let @{text Abs} and @{text Rep} act
-over the appropriate types. The clauses of @{text ABS} and @{text REP}
+over the appropriate types. In what follows we use the short-hand notation
-are as follows (where we use the short-hand notation @{text "ABS (\<sigma>s, \<tau>s)"} to mean
+@{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>i, \<tau>\<^isub>i)"}; similarly
-@{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>i, \<tau>\<^isub>i)"}; similarly for @{text REP}):
+for @{text REP}.
+%
 \begin{center}
 \hfill
 \begin{tabular}{rcl}
 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
 @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
 @{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{tabular}\hfill\numbered{ABSREP}
 \end{center}
 %
 \noindent
-where in the last two clauses we have that the type @{text "\<alpha>s
+In the last two clauses we have that the type @{text "\<alpha>s
 \<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 among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
 matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
 \end{center}
 %
 \noindent
 In this definition we rely on the fact that we can interpret type-variables @{text \<alpha>} as
 term variables @{text a}. In the last clause we build an abstraction over all
-term-variables inside map-function generated by the auxiliary function
+term-variables of the map-function generated by the auxiliary function
 @{text "MAP'"}.
-The need of aggregate map-functions can be seen in cases where we build quotients,
+The need for aggregate map-functions can be seen in cases where we build quotients,
 say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{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
-which we need in order to define the aggregate abstraction and representation
+which is essential in order to define the corresponding aggregate
-functions.
+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 them into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
+fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
 the abstraction function
 @{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
 \noindent
 In our implementation we further
 simplify this function by rewriting with the usual laws about @{text
 "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =
-id \<circ> f = f"}. This gives us the abstraction function
+id \<circ> f = f"}. This gives us the simpler 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
 then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
 @{text "\<tau> \<Rightarrow> \<sigma>"}.
 \end{lemma}
 \begin{proof}
-By mutual induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
+By mutual induction and analysing the definitions of @{text "ABS"} and @{text "REP"}.
-and @{text "MAP"}. The cases of equal types and function types are
+The cases of equal types 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>)"}). In case of equal type
 constructors we can observe that a map-function after applying the functions
 @{text "ABS (\<sigma>s, \<tau>s)"} produces 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
 @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
 \end{proof}
 \noindent
 The reader should note that this lemma fails for the abstraction and representation
-functions used, for example, in Homeier's quotient package.
+functions used in Homeier's quotient package.
 *}
 section {* Respectfulness and Preservation \label{sec:resp} *}
 text {*
 The main point of the quotient package is to automatically ``lift'' theorems
 involving constants over the raw type to theorems involving constants over
-the quotient type. Before we can describe this lift process, we need to impose
+the quotient type. Before we can describe this lifting process, we need to impose
-some restrictions. The reason is that even if definitions for all raw constants
+some restrictions in the form of proof obligations that arise during the
-can be given, \emph{not} all theorems can be actually be lifted. Most notably is
+lifting. The reason is that even if definitions for all raw constants
-the bound variable function, that is the constant @{text bn}, defined for
+can be given, \emph{not} all theorems can be lifted to the quotient type. Most
-raw lambda-terms as follows
+notably is the bound variable function, that is the constant @{text bn}, defined
+for raw lambda-terms as follows
 \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}
 \noindent
-This constant just does not respect @{text "\<alpha>"}-equivalence and as
+We can generate a definition for this constant using @{text ABS} and @{text REP}.
+But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and
 consequently no theorem involving this constant can be lifted to @{text
 "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
 the properties of \emph{respectfullness} and \emph{preservation}. We have
 to slightly extend Homeier's definitions in order to deal with quotient
 compositions.
 To formally define what respectfulness is, we have to first define
-the notion of \emph{aggregate equivalence relations}.
+the notion of \emph{aggregate equivalence relations} using @{text REL}:
-TBD
+\begin{center}
+\hfill
-\begin{itemize}
+\begin{tabular}{rcl}
-\item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
+\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
-\item @{text "REL(\<sigma>, \<sigma>)"}  =  @{text "op ="}
+@{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
-\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
-\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
+@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
-\end{itemize}
+\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\smallskip\\
+@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
+\end{tabular}\hfill\numbered{REL}
+\end{center}
+\noindent
+The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
+we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
+@{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are determined by matching
+@{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
+Lets return to the lifting procedure of theorems. Assume we have a theorem
+that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
+lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
+constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
+we throw the following proof obligation
+@{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+\noindent
+if @{text \<sigma>} and @{text \<tau>} have no type variables. In case they have, then
+the proof obligation is of the form
+@{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+\noindent
+where @{text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
+Homeier calls these proof obligations \emph{respectfullness
+theorems}. Before lifting a theorem, we require the user to discharge
+them. And the point with @{text bn} is that the respectfullness theorem
+looks as follows
+@{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
+\noindent
+and the user cannot discharge it---because it is not true. To see this,
+we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun}
+using extensionality to obtain
+@{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"}
+\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] "(rel_list R \<doublearr> rel_list R \<doublearr> rel_listR) append append"}
+\noindent
+under the assumption @{text "Quotient R Abs Rep"}.
 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.
 @{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]}
 *}
-section {* Examples *}
+section {* Examples \label{sec:examples} *}
 (* Mention why equivalence *)
 text {*

changeset 2274	99cf23602d36
parent 2273	d62c082cb56b
child 2275	69b80ad616c5