
diff -r d62c082cb56b -r 99cf23602d36 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 22:25:03 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed Jun 16 02:55:52 2010 +0100
@@ -24,6 +24,7 @@
 
 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 =
@@ -33,11 +34,13 @@
     | _ => 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))
 *}
+
 (*>*)
 
 
@@ -255,7 +258,8 @@
   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.
 *}
@@ -263,10 +267,10 @@
 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 
-  the important definitions given by Homeier for quotients \cite{Homeier05}.
+  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 
+  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
@@ -283,12 +287,11 @@
   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 constants; this includes equality, with type @{text "= :: \<sigma> \<Rightarrow>
-  \<sigma> \<Rightarrow> bool"}, and the identity function, with type @{text "id :: \<sigma> => \<sigma>"} (the former
-  being primitive and the latter being defined as @{text
-  "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
+  "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
+  constants; a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
+  bool"}, and the identity function with type @{text "id :: \<sigma> => \<sigma>"} is
+  defined as @{text "\<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
@@ -296,10 +299,10 @@
   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 @{text map} for lists. Homeier describes in \cite{Homeier05} map-functions
-  for products, sums,
-  options and also the following map for function types
+  Like Homeier, our work relies on map-functions defined for every type
+  constructor taking some arguments, for example @{text map} 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]}
 
@@ -310,10 +313,11 @@
   @{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}. 
-  In what follows we shall use the terminology @{text "map_\<kappa>"} for a map-function 
-  defined for the type-constructor @{text \<kappa>}. In our implementation we have 
-  a database of map-functions that can be dynamically extended.
+  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 
+  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
@@ -327,7 +331,23 @@
   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:
@@ -355,30 +375,28 @@
       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}
-  An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.
-  \end{definition}
-
   \noindent
-  As a result, Homeier was able to build an automatic prover that can nearly
+  As a result, Homeier is 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
-  %
-  @{thm [mode=Rule, display, indent=10] pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
+  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 (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
-  the composition of any two quotients in not true (it is not even typable in
-  the HOL type system). However, we can prove useful instances for compatible
-  containers. We will show such example in Section \ref{sec:resp}.
-
+  Unfortunately, there are two predicaments with compositions of relations.
+  First, a general quotient theorem, like the one given in Proposition \ref{funquot},
+  cannot be stated inside HOL, because of the restriction on types.
+  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}.
 
 *}
 
@@ -412,8 +430,8 @@
   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 
-  the quotient types as
+  relations is omitted).  Given this data, we define for declarations shown in
+  \eqref{typedecl} the quotient types internally as
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
@@ -421,9 +439,9 @@
 
   \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}\ \ \ \ \ \ \ \ \ \ %%%
@@ -445,16 +463,13 @@
   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
@@ -480,7 +495,8 @@
   
   \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
@@ -488,15 +504,15 @@
   @{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} 
-  are as follows (where we use the short-hand notation @{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 for @{text REP}):
-
+  over the appropriate types. In what follows we use the short-hand notation 
+  @{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 
+  for @{text REP}.
+  %
   \begin{center}
   \hfill
   \begin{tabular}{rcl}
@@ -516,7 +532,7 @@
   \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
@@ -538,9 +554,9 @@
   \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:
@@ -548,13 +564,13 @@
   @{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 
-  functions.
+  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 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"}
@@ -563,7 +579,7 @@
   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"}
 
@@ -596,8 +612,8 @@
   \end{lemma}
 
   \begin{proof}
-  By mutual induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
-  and @{text "MAP"}. The cases of equal types and function types are
+  By mutual induction and analysing the definitions of @{text "ABS"} and @{text "REP"}. 
+  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
@@ -616,7 +632,7 @@
   
   \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} *}
@@ -624,11 +640,12 @@
 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 
-  some restrictions. The reason is that even if definitions for all raw constants 
-  can be given, \emph{not} all theorems can be actually be lifted. Most notably is
-  the bound variable function, that is the constant @{text bn}, defined for 
-  raw lambda-terms as follows
+  the quotient type. Before we can describe this lifting process, we need to impose 
+  some restrictions in the form of proof obligations that arise during the
+  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 
+  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}
@@ -637,7 +654,8 @@
   \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
@@ -645,16 +663,65 @@
   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}:
+
+  \begin{center}
+  \hfill
+  \begin{tabular}{rcl}
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
+  @{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
+   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 
+  @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
+  \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}
 
-  TBD
+  \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"}
 
-  \begin{itemize}
-  \item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
-  \item @{text "REL(\<sigma>, \<sigma>)"}  =  @{text "op ="}
-  \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))"}
-  \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"}
-  \end{itemize}
+  \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
@@ -961,7 +1028,7 @@
 
   *}
 
-section {* Examples *}
+section {* Examples \label{sec:examples} *}
 
 (* Mention why equivalence *)
 




