1 (*<*)

     2 theory Paper

     3 imports "Quotient"

     4         "LaTeXsugar"

     5         "../Nominal/FSet"

     6 begin

     7 

     8 (****

     9 

    10 ** things to do for the next version

    11 *

    12 * - what are quot_thms?

    13 * - what do all preservation theorems look like,

    14     in particular preservation for quotient

    15     compositions

    16   - explain how Quotient R Abs Rep is proved (j-version)

    17   - give an example where precise specification helps (core Haskell in nominal?)

    18 

    19   - Quote from Peter:

    20 

    21     One might think quotient have been studied to death, but

    22 

    23   - Mention Andreas Lochbiler in Acknowledgements and 'desceding'.

    24 

    25 *)

    26 

    27 notation (latex output)

    28   rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and

    29   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and

    30   "op -->" (infix "\<longrightarrow>" 100) and

    31   "==>" (infix "\<Longrightarrow>" 100) and

    32   fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and

    33   fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and

    34   list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)

    35   fempty ("\<emptyset>") and

    36   funion ("_ \<union> _") and

    37   finsert ("{_} \<union> _") and 

    38   Cons ("_::_") and

    39   concat ("flat") and

    40   fconcat ("\<Union>")

    41  

    42   

    43 

    44 ML {*

    45 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;

    46 

    47 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>

    48   let

    49     val concl =

    50       Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)

    51   in

    52     case concl of (_ $ l $ r) => proj (l, r)

    53     | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)

    54   end);

    55 *}

    56 

    57 setup {*

    58   Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>

    59   Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>

    60   Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))

    61 *}

    62 

    63 (*>*)

    64 

    65 

    66 section {* Introduction *}

    67 

    68 text {* 

    69    \begin{flushright}

    70   {\em ``Not using a [quotient] package has its advantages: we do not have to\\ 

    71     collect all the theorems we shall ever want into one giant list;''}\\

    72     Larry Paulson \cite{Paulson06}

    73   \end{flushright}

    74 

    75   \noindent

    76   Isabelle is a popular generic theorem prover in which many logics can be

    77   implemented. The most widely used one, however, is Higher-Order Logic

    78   (HOL). This logic consists of a small number of axioms and inference rules

    79   over a simply-typed term-language. Safe reasoning in HOL is ensured by two

    80   very restricted mechanisms for extending the logic: one is the definition of

    81   new constants in terms of existing ones; the other is the introduction of

    82   new types by identifying non-empty subsets in existing types. It is well

    83   understood how to use both mechanisms for dealing with quotient

    84   constructions in HOL (see \cite{Homeier05,Paulson06}).  For example the

    85   integers in Isabelle/HOL are constructed by a quotient construction over the

    86   type @{typ "nat \<times> nat"} and the equivalence relation

    87 

    88   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

    89   @{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}

    90   \end{isabelle}

    91 

    92   \noindent

    93   This constructions yields the new type @{typ int} and definitions for @{text

    94   "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of

    95   natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations

    96   such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in

    97   terms of operations on pairs of natural numbers (namely @{text

    98   "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,

    99   m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).

   100   Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"}, 

   101   by quotienting the type @{text "\<alpha> list"} according to the equivalence relation

   102 

   103   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   104   @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}

   105   \end{isabelle}

   106 

   107   \noindent

   108   which states that two lists are equivalent if every element in one list is

   109   also member in the other. The empty finite set, written @{term "{||}"}, can

   110   then be defined as the empty list and the union of two finite sets, written

   111   @{text "\<union>"}, as list append.

   112 

   113   Quotients are important in a variety of areas, but they are really ubiquitous in

   114   the area of reasoning about programming language calculi. A simple example

   115   is the lambda-calculus, whose raw terms are defined as

   116 

   117 

   118   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   119   @{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}

   120   \end{isabelle}

   121 

   122   \noindent

   123   The problem with this definition arises, for instance, when one attempts to

   124   prove formally the substitution lemma \cite{Barendregt81} by induction

   125   over the structure of terms. This can be fiendishly complicated (see

   126   \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof

   127   about raw lambda-terms). In contrast, if we reason about

   128   $\alpha$-equated lambda-terms, that means terms quotient according to

   129   $\alpha$-equivalence, then the reasoning infrastructure provided, 

   130   for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal 

   131   proof of the substitution lemma almost trivial. 

   132 

   133   The difficulty is that in order to be able to reason about integers, finite

   134   sets or $\alpha$-equated lambda-terms one needs to establish a reasoning

   135   infrastructure by transferring, or \emph{lifting}, definitions and theorems

   136   from the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}

   137   (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting

   138   usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.  

   139   It is feasible to do this work manually, if one has only a few quotient

   140   constructions at hand. But if they have to be done over and over again, as in 

   141   Nominal Isabelle, then manual reasoning is not an option.

   142 

   143   The purpose of a \emph{quotient package} is to ease the lifting of theorems

   144   and automate the reasoning as much as possible. In the

   145   context of HOL, there have been a few quotient packages already

   146   \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier

   147   \cite{Homeier05} implemented in HOL4.  The fundamental construction these

   148   quotient packages perform can be illustrated by the following picture:

   149 

   150 %%% FIXME: Referee 1 says:

   151 %%% Diagram is unclear.  Firstly, isn't an existing type a "set (not sets) of raw elements"?

   152 %%% Secondly, isn't the _set of_ equivalence classes mapped to and from the new type?

   153 %%% Thirdly, what do the words "non-empty subset" refer to ?

   154 

   155 %%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise

   156 %%% I wouldn't change it.

   157 

   158   \begin{center}

   159   \mbox{}\hspace{20mm}\begin{tikzpicture}

   160   %%\draw[step=2mm] (-4,-1) grid (4,1);

   161   

   162   \draw[very thick] (0.7,0.3) circle (4.85mm);

   163   \draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);

   164   \draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);

   165   

   166   \draw (-2.0, 0.8) --  (0.7,0.8);

   167   \draw (-2.0,-0.195)  -- (0.7,-0.195);

   168 

   169   \draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};

   170   \draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};

   171   \draw (1.8, 0.35) node[right=-0.1mm]

   172     {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw elements)\end{tabular}};

   173   \draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};

   174   

   175   \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);

   176   \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);

   177   \draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};

   178   \draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};

   179 

   180   \end{tikzpicture}

   181   \end{center}

   182 

   183   \noindent

   184   The starting point is an existing type, to which we refer as the

   185   \emph{raw type} and over which an equivalence relation given by the user is

   186   defined. With this input the package introduces a new type, to which we

   187   refer as the \emph{quotient type}. This type comes with an

   188   \emph{abstraction} and a \emph{representation} function, written @{text Abs}

   189   and @{text Rep}.\footnote{Actually slightly more basic functions are given;

   190   the functions @{text Abs} and @{text Rep} need to be derived from them. We

   191   will show the details later. } They relate elements in the

   192   existing type to elements in the new type and vice versa, and can be uniquely

   193   identified by their quotient type. For example for the integer quotient construction

   194   the types of @{text Abs} and @{text Rep} are

   195 

   196 

   197   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   198   @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}

   199   \end{isabelle}

   200 

   201   \noindent

   202   We therefore often write @{text Abs_int} and @{text Rep_int} if the

   203   typing information is important. 

   204 

   205   Every abstraction and representation function stands for an isomorphism

   206   between the non-empty subset and elements in the new type. They are

   207   necessary for making definitions involving the new type. For example @{text

   208   "0"} and @{text "1"} of type @{typ int} can be defined as

   209 

   210 

   211   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   212   @{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}

   213   \end{isabelle}

   214 

   215   \noindent

   216   Slightly more complicated is the definition of @{text "add"} having type 

   217   @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows

   218 

   219    \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   220   @{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}

   221   \hfill\numbered{adddef}

   222   \end{isabelle}

   223 

   224   \noindent

   225   where we take the representation of the arguments @{text n} and @{text m},

   226   add them according to the function @{text "add_pair"} and then take the

   227   abstraction of the result.  This is all straightforward and the existing

   228   quotient packages can deal with such definitions. But what is surprising is

   229   that none of them can deal with slightly more complicated definitions involving

   230   \emph{compositions} of quotients. Such compositions are needed for example

   231   in case of quotienting lists to yield finite sets and the operator that 

   232   flattens lists of lists, defined as follows

   233 

   234   @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}

   235 

   236   \noindent

   237   We expect that the corresponding operator on finite sets, written @{term "fconcat"},

   238   builds finite unions of finite sets:

   239 

   240   @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}

   241 

   242   \noindent

   243   The quotient package should automatically provide us with a definition for @{text "\<Union>"} in

   244   terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is 

   245   that the method  used in the existing quotient

   246   packages of just taking the representation of the arguments and then taking

   247   the abstraction of the result is \emph{not} enough. The reason is that in case

   248   of @{text "\<Union>"} we obtain the incorrect definition

   249 

   250   @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}

   251 

   252   \noindent

   253   where the right-hand side is not even typable! This problem can be remedied in the

   254   existing quotient packages by introducing an intermediate step and reasoning

   255   about flattening of lists of finite sets. However, this remedy is rather

   256   cumbersome and inelegant in light of our work, which can deal with such

   257   definitions directly. The solution is that we need to build aggregate

   258   representation and abstraction functions, which in case of @{text "\<Union>"}

   259   generate the following definition

   260 

   261   @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}

   262 

   263   \noindent

   264   where @{term map_list} is the usual mapping function for lists. In this paper we

   265   will present a formal definition of our aggregate abstraction and

   266   representation functions (this definition was omitted in \cite{Homeier05}). 

   267   They generate definitions, like the one above for @{text "\<Union>"}, 

   268   according to the type of the raw constant and the type

   269   of the quotient constant. This means we also have to extend the notions

   270   of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}

   271   from Homeier \cite{Homeier05}.

   272 

   273   In addition we are able to address the criticism by Paulson \cite{Paulson06} cited

   274   at the beginning of this section about having to collect theorems that are

   275   lifted from the raw level to the quotient level into one giant list. Homeier's and

   276   also our quotient package are modular so that they allow lifting

   277   theorems separately. This has the advantage for the user of being able to develop a

   278   formal theory interactively as a natural progression. A pleasing side-result of

   279   the modularity is that we are able to clearly specify what is involved

   280   in the lifting process (this was only hinted at in \cite{Homeier05} and

   281   implemented as a ``rough recipe'' in ML-code).

   282 

   283 

   284   The paper is organised as follows: Section \ref{sec:prelims} presents briefly

   285   some necessary preliminaries; Section \ref{sec:type} describes the definitions 

   286   of quotient types and shows how definitions of constants can be made over 

   287   quotient types. Section \ref{sec:resp} introduces the notions of respectfulness

   288   and preservation; Section \ref{sec:lift} describes the lifting of theorems;

   289   Section \ref{sec:examples} presents some examples

   290   and Section \ref{sec:conc} concludes and compares our results to existing 

   291   work.

   292 *}

   293 

   294 section {* Preliminaries and General Quotients\label{sec:prelims} *}

   295 

   296 text {*

   297   We give in this section a crude overview of HOL and describe the main

   298   definitions given by Homeier for quotients \cite{Homeier05}.

   299 

   300   At its core, HOL is based on a simply-typed term language, where types are 

   301   recorded in Church-style fashion (that means, we can always infer the type of 

   302   a term and its subterms without any additional information). The grammars

   303   for types and terms are as follows

   304 

   305   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   306   \begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}

   307   @{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\

   308   @{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} & 

   309   (variables, constants, applications and abstractions)\\

   310   \end{tabular}

   311   \end{isabelle}

   312 

   313   \noindent

   314   We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and

   315   @{text "\<sigma>s"} to stand for collections of type variables and types,

   316   respectively.  The type of a term is often made explicit by writing @{text

   317   "t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function

   318   type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined

   319   constants; for example, a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>

   320   bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is

   321   defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}.

   322 

   323   An important point to note is that theorems in HOL can be seen as a subset

   324   of terms that are constructed specially (namely through axioms and proof

   325   rules). As a result we are able to define automatic proof

   326   procedures showing that one theorem implies another by decomposing the term

   327   underlying the first theorem.

   328 

   329   Like Homeier's, our work relies on map-functions defined for every type

   330   constructor taking some arguments, for example @{text map_list} for lists. Homeier

   331   describes in \cite{Homeier05} map-functions for products, sums, options and

   332   also the following map for function types

   333 

   334   @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}

   335 

   336   \noindent

   337   Using this map-function, we can give the following, equivalent, but more 

   338   uniform definition for @{text add} shown in \eqref{adddef}:

   339 

   340   @{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}

   341 

   342   \noindent

   343   Using extensionality and unfolding the definition of @{text "\<singlearr>"}, 

   344   we can get back to \eqref{adddef}. 

   345   In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function 

   346   of the type-constructor @{text \<kappa>}. For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the

   347   type of @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. For example @{text "map_list"}

   348   has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.

   349   In our implementation we maintain

   350   a database of these map-functions that can be dynamically extended.

   351 

   352   It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},

   353   which define equivalence relations in terms of constituent equivalence

   354   relations. For example given two equivalence relations @{text "R\<^isub>1"}

   355   and @{text "R\<^isub>2"}, we can define an equivalence relations over 

   356   products as follows

   357   %

   358   @{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"}

   359 

   360   \noindent

   361   Homeier gives also the following operator for defining equivalence 

   362   relations over function types

   363   %

   364   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   365   @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}

   366   \hfill\numbered{relfun}

   367   \end{isabelle}

   368   

   369   \noindent

   370   In the context of quotients, the following two notions from \cite{Homeier05} 

   371   are needed later on.

   372 

   373   \begin{definition}[Respects]\label{def:respects}

   374   An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.

   375   \end{definition}

   376 

   377   \begin{definition}[Bounded Quantification and Bounded Abstractions]\label{def:babs}

   378   @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};

   379   and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.

   380   \end{definition}

   381 

   382   The central definition in Homeier's work \cite{Homeier05} relates equivalence 

   383   relations, abstraction and representation functions:

   384 

   385   \begin{definition}[Quotient Types]

   386   Given a relation $R$, an abstraction function $Abs$

   387   and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}

   388   holds if and only if

   389   \begin{enumerate}

   390   \item @{thm (rhs1) Quotient_def[of "R", no_vars]}

   391   \item @{thm (rhs2) Quotient_def[of "R", no_vars]}

   392   \item @{thm (rhs3) Quotient_def[of "R", no_vars]}

   393   \end{enumerate}

   394   \end{definition}

   395 

   396   \noindent

   397   The value of this definition lies in the fact that validity of @{text "Quotient R Abs Rep"} can 

   398   often be proved in terms of the validity of @{text "Quotient"} over the constituent 

   399   types of @{text "R"}, @{text Abs} and @{text Rep}. 

   400   For example Homeier proves the following property for higher-order quotient

   401   types:

   402  

   403   \begin{proposition}\label{funquot}

   404   @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2" 

   405       and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}

   406   \end{proposition}

   407 

   408   \noindent

   409   As a result, Homeier is able to build an automatic prover that can nearly

   410   always discharge a proof obligation involving @{text "Quotient"}. Our quotient

   411   package makes heavy 

   412   use of this part of Homeier's work including an extension 

   413   for dealing with compositions of equivalence relations defined as follows:

   414 

   415 %%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also

   416 %%% what wikipedia says. Any idea for a different name? Conjugation of Relations?

   417 

   418   \begin{definition}[Composition of Relations]

   419   @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate

   420   composition defined by 

   421   @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}

   422   holds if and only if there exists a @{text y} such that @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and

   423   @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.

   424   \end{definition}

   425 

   426   \noindent

   427   Unfortunately a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, analogous to the one

   428   for @{text "\<singlearr>"} given in Proposition \ref{funquot}, would not be true

   429   in general. It cannot even be stated inside HOL, because of restrictions on types.

   430   However, we can prove specific instances of a

   431   quotient theorem for composing particular quotient relations.

   432   For example, to lift theorems involving @{term flat} the quotient theorem for 

   433   composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"} 

   434   with @{text R} being an equivalence relation, then

   435 

   436   @{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)"}

   437 

   438   \vspace{-.5mm}

   439 *}

   440 

   441 section {* Quotient Types and Quotient Definitions\label{sec:type} *}

   442 

   443 text {*

   444   The first step in a quotient construction is to take a name for the new

   445   type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},

   446   defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence

   447   relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of

   448   the quotient type declaration is therefore

   449 

   450   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   451   \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}

   452   \end{isabelle}

   453 

   454   \noindent

   455   and a proof that @{text "R"} is indeed an equivalence relation. Two concrete

   456   examples are

   457 

   458   

   459   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   460   \begin{tabular}{@ {}l}

   461   \isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\

   462   \isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}

   463   \end{tabular}

   464   \end{isabelle}

   465 

   466   \noindent

   467   which introduce the type of integers and of finite sets using the

   468   equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text

   469   "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and

   470   \eqref{listequiv}, respectively (the proofs about being equivalence

   471   relations is omitted).  Given this data, we define for declarations shown in

   472   \eqref{typedecl} the quotient types internally as

   473   

   474   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   475   \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}

   476   \end{isabelle}

   477 

   478   \noindent

   479   where the right-hand side is the (non-empty) set of equivalence classes of

   480   @{text "R"}. The constraint in this declaration is that the type variables

   481   in the raw type @{text "\<sigma>"} must be included in the type variables @{text

   482   "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will then provide us with the following

   483   abstraction and representation functions 

   484 

   485   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   486   @{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"}

   487   \end{isabelle}

   488 

   489   \noindent 

   490   As can be seen from the type, they relate the new quotient type and equivalence classes of the raw

   491   type. However, as Homeier \cite{Homeier05} noted, it is much more convenient

   492   to work with the following derived abstraction and representation functions

   493 

   494   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   495   @{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)"}

   496   \end{isabelle}

   497   

   498   \noindent

   499   on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the

   500   definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the

   501   quotient type and the raw type directly, as can be seen from their type,

   502   namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},

   503   respectively.  Given that @{text "R"} is an equivalence relation, the

   504   following property holds  for every quotient type 

   505   (for the proof see \cite{Homeier05}).

   506 

   507   \begin{proposition}

   508   @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.

   509   \end{proposition}

   510 

   511   The next step in a quotient construction is to introduce definitions of new constants

   512   involving the quotient type. These definitions need to be given in terms of concepts

   513   of the raw type (remember this is the only way how to extend HOL

   514   with new definitions). For the user the visible part of such definitions is the declaration

   515 

   516   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   517   \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}

   518   \end{isabelle}

   519 

   520   \noindent

   521   where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)

   522   and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be

   523   given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ 

   524   in places where a quotient and raw type is involved). Two concrete examples are

   525 

   526   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   527   \begin{tabular}{@ {}l}

   528   \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\

   529   \isacommand{quotient\_definition}~~@{text "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}~~%

   530   \isacommand{is}~~@{text "flat"} 

   531   \end{tabular}

   532   \end{isabelle}

   533   

   534   \noindent

   535   The first one declares zero for integers and the second the operator for

   536   building unions of finite sets (@{text "flat"} having the type 

   537   @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}). 

   538 

   539   From such declarations given by the user, the quotient package needs to derive proper

   540   definitions using @{text "Abs"} and @{text "Rep"}. The data we rely on is the given quotient type

   541   @{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define \emph{aggregate

   542   abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,

   543   \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we shall give below. The idea behind

   544   these two functions is to simultaneously descend into the raw types @{text \<sigma>} and 

   545   quotient types @{text \<tau>}, and generate the appropriate

   546   @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore

   547   we generate just the identity whenever the types are equal. On the ``way'' down,

   548   however we might have to use map-functions to let @{text Abs} and @{text Rep} act

   549   over the appropriate types. In what follows we use the short-hand notation 

   550   @{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>n, \<tau>\<^isub>n)"}; similarly 

   551   for @{text REP}.

   552   %

   553   \begin{center}

   554   \hfill

   555   \begin{tabular}{rcl}

   556   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 

   557   @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\

   558   @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\

   559   \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ 

   560   @{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)"}\\

   561   @{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\\

   562   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 

   563   @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\

   564   @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\

   565   \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s

   566   \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\\

   567   @{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)))"}\\

   568   @{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"}

   569   \end{tabular}\hfill\numbered{ABSREP}

   570   \end{center}

   571   %

   572   \noindent

   573   In the last two clauses we rely on the fact that the type @{text "\<alpha>s

   574   \<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example

   575   @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>

   576   list"}). The quotient construction ensures that the type variables in @{text

   577   "\<rho>s \<kappa>"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the

   578   substitutions for the @{text "\<alpha>s"} when matching  @{text "\<sigma>s \<kappa>"} against

   579   @{text "\<rho>s \<kappa>"}.  The

   580   function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw

   581   type as follows:

   582   %

   583   \begin{center}

   584   \begin{tabular}{rcl}

   585   @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\

   586   @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\

   587   @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\

   588   @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}  

   589   \end{tabular}

   590   \end{center}

   591   %

   592   \noindent

   593   In this definition we rely on the fact that in the first clause we can interpret type-variables @{text \<alpha>} as 

   594   term variables @{text a}. In the last clause we build an abstraction over all

   595   term-variables of the map-function generated by the auxiliary function 

   596   @{text "MAP'"}.

   597   The need for aggregate map-functions can be seen in cases where we build quotients, 

   598   say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. 

   599   In this case @{text MAP} generates  the 

   600   aggregate map-function:

   601 

   602 %%% FIXME: Reviewer 2 asks: last two lines defining ABS and REP for

   603 %%% unequal type constructors: How are the $\varrho$s defined? The

   604 %%% following paragraph mentions them, but this paragraph is unclear,

   605 %%% since it then mentions $\alpha$s, which do not seem to be defined

   606 %%% either. As a result, I do not understand the first two sentences

   607 %%% in this paragraph. I can imagine roughly what the following

   608 %%% sentence `The $\sigma$s' are given by the matchers for the

   609 %%% $\alpha$s$ when matching $\varrho$s $\kappa$ against $\sigma$s

   610 %%% $\kappa$.' means, but also think that it is too vague.

   611 

   612   @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"}

   613   

   614   \noindent

   615   which is essential in order to define the corresponding aggregate 

   616   abstraction and representation functions.

   617   

   618   To see how these definitions pan out in practise, let us return to our

   619   example about @{term "concat"} and @{term "fconcat"}, where we have the raw type

   620   @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>

   621   fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)

   622   the abstraction function

   623 

   624   @{text [display, indent=10] "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}

   625 

   626   \noindent

   627   In our implementation we further

   628   simplify this function by rewriting with the usual laws about @{text

   629   "map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =

   630   id \<circ> f = f"}. This gives us the simpler abstraction function

   631 

   632   @{text [display, indent=10] "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}

   633 

   634   \noindent

   635   which we can use for defining @{term "fconcat"} as follows

   636 

   637   @{text [display, indent=10] "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}

   638 

   639   \noindent

   640   Note that by using the operator @{text "\<singlearr>"} and special clauses

   641   for function types in \eqref{ABSREP}, we do not have to 

   642   distinguish between arguments and results, but can deal with them uniformly.

   643   Consequently, all definitions in the quotient package 

   644   are of the general form

   645 

   646   @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}

   647 

   648   \noindent

   649   where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the

   650   type of the defined quotient constant @{text "c"}. This data can be easily

   651   generated from the declaration given by the user.

   652   To increase the confidence in this way of making definitions, we can prove 

   653   that the terms involved are all typable.

   654 

   655   \begin{lemma}

   656   If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"} 

   657   and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"}, 

   658   then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type

   659   @{text "\<tau> \<Rightarrow> \<sigma>"}.

   660   \end{lemma}

   661 

   662   \begin{proof}

   663   By mutual induction and analysing the definitions of @{text "ABS"} and @{text "REP"}. 

   664   The cases of equal types and function types are

   665   straightforward (the latter follows from @{text "\<singlearr>"} having the

   666   type @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). In case of equal type

   667   constructors we can observe that a map-function after applying the functions

   668   @{text "ABS (\<sigma>s, \<tau>s)"} produces a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.  The

   669   interesting case is the one with unequal type constructors. Since we know

   670   the quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have

   671   that @{text "Abs_\<kappa>\<^isub>q"} is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s

   672   \<kappa>\<^isub>q"}. This type can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s

   673   \<kappa>\<^isub>q"} where the type variables @{text "\<alpha>s"} are instantiated with the

   674   @{text "\<tau>s"}. The complete type can be calculated by observing that @{text

   675   "MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it,

   676   returns a term of type @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is

   677   equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with

   678   @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed

   679   \end{proof}

   680 *}

   681 

   682 section {* Respectfulness and Preservation \label{sec:resp} *}

   683 

   684 text {*

   685   The main point of the quotient package is to automatically ``lift'' theorems

   686   involving constants over the raw type to theorems involving constants over

   687   the quotient type. Before we can describe this lifting process, we need to impose 

   688   two restrictions in form of proof obligations that arise during the

   689   lifting. The reason is that even if definitions for all raw constants 

   690   can be given, \emph{not} all theorems can be lifted to the quotient type. Most 

   691   notable is the bound variable function, that is the constant @{text bn}, defined 

   692   for raw lambda-terms as follows

   693 

   694   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   695   @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}

   696   @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}

   697   @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}

   698   \end{isabelle}

   699 

   700   \noindent

   701   We can generate a definition for this constant using @{text ABS} and @{text REP}.

   702   But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and 

   703   consequently no theorem involving this constant can be lifted to @{text

   704   "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of

   705   the properties of \emph{respectfulness} and \emph{preservation}. We have

   706   to slightly extend Homeier's definitions in order to deal with quotient

   707   compositions. 

   708 

   709 %%% FIXME: Reviewer 3 asks why are the definitions that follow enough to deal

   710 %%% with quotient composition.

   711 

   712   To formally define what respectfulness is, we have to first define 

   713   the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"}

   714   The idea behind this function is to simultaneously descend into the raw types

   715   @{text \<sigma>} and quotient types @{text \<tau>}, and generate the appropriate

   716   quotient equivalence relations in places where the types differ and equalities

   717   elsewhere.

   718 

   719   \begin{center}

   720   \hfill

   721   \begin{tabular}{rcl}

   722   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 

   723   @{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\

   724    \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 

   725   @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\

   726   \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s

   727   \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\smallskip\\

   728   @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\

   729   \end{tabular}\hfill\numbered{REL}

   730   \end{center}

   731 

   732   \noindent

   733   The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:

   734   we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type 

   735   @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are the substitutions for @{text "\<alpha>s"} obtained by matching 

   736   @{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.

   737 

   738   Let us return to the lifting procedure of theorems. Assume we have a theorem

   739   that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to

   740   lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding

   741   constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation 

   742   we generate the following proof obligation

   743 

   744   @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}

   745 

   746   \noindent

   747   Homeier calls these proof obligations \emph{respectfulness

   748   theorems}. However, unlike his quotient package, we might have several

   749   respectfulness theorems for one constant---he has at most one.

   750   The reason is that because of our quotient compositions, the types

   751   @{text \<sigma>} and @{text \<tau>} are not completely determined by @{text "c\<^bsub>r\<^esub>"}.

   752   And for every instantiation of the types, a corresponding

   753   respectfulness theorem is necessary.

   754 

   755   Before lifting a theorem, we require the user to discharge

   756   respectfulness proof obligations. In case of @{text bn}

   757   this obligation is as follows

   758 

   759   @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}

   760 

   761   \noindent

   762   and the point is that the user cannot discharge it: because it is not true. To see this,

   763   we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun} 

   764   using extensionality to obtain the false statement

   765 

   766   @{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)"}

   767  

   768   \noindent

   769   In contrast, if we lift a theorem about @{text "append"} to a theorem describing 

   770   the union of finite sets, then we need to discharge the proof obligation

   771 

   772   @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}

   773 

   774   \noindent

   775   To do so, we have to establish

   776   

   777   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   778   if @{text "xs \<approx>\<^bsub>list\<^esub> ys"} and  @{text "us \<approx>\<^bsub>list\<^esub> vs"}

   779   then @{text "xs @ us \<approx>\<^bsub>list\<^esub> ys @ vs"}

   780   \end{isabelle}

   781 

   782   \noindent

   783   which is straightforward given the definition shown in \eqref{listequiv}.

   784 

   785   The second restriction we have to impose arises from non-lifted polymorphic

   786   constants, which are instantiated to a type being quotient. For example,

   787   take the @{term "cons"}-constructor to add a pair of natural numbers to a

   788   list, whereby we assume the pair of natural numbers turns into an integer in

   789   the quotient construction. The point is that we still want to use @{text

   790   cons} for adding integers to lists---just with a different type. To be able

   791   to lift such theorems, we need a \emph{preservation property} for @{text

   792   cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"}

   793   and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a

   794   preservation property is as follows

   795 

   796 %%% FIXME: Reviewer 2 asks: You say what a preservation theorem is,

   797 %%% but not which preservation theorems you assume. Do you generate a

   798 %%% proof obligation for a preservation theorem for each raw constant

   799 %%% and its corresponding lifted constant?

   800 

   801 %%% Cezary: I think this would be a nice thing to do but we have not

   802 %%% done it, the theorems need to be 'guessed' from the remaining obligations

   803 

   804   @{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"}

   805 

   806   \noindent

   807   where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.

   808   In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have 

   809 

   810   @{text [display, indent=10] "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}

   811 

   812   \noindent

   813   under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have

   814   an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated

   815   with @{text "nat \<times> nat"} and we also quotient this type to yield integers,

   816   then we need to show the corresponding preservation property.

   817 

   818   %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}

   819 

   820   %Given two quotients, one of which quotients a container, and the

   821   %other quotients the type in the container, we can write the

   822   %composition of those quotients. To compose two quotient theorems

   823   %we compose the relations with relation composition as defined above

   824   %and the abstraction and relation functions are the ones of the sub

   825   %quotients composed with the usual function composition.

   826   %The @ {term "Rep"} and @ {term "Abs"} functions that we obtain agree

   827   %with the definition of aggregate Abs/Rep functions and the

   828   %relation is the same as the one given by aggregate relations.

   829   %This becomes especially interesting

   830   %when we compose the quotient with itself, as there is no simple

   831   %intermediate step.

   832   %

   833   %Lets take again the example of @ {term flat}. To be able to lift

   834   %theorems that talk about it we provide the composition quotient

   835   %theorem which allows quotienting inside the container:

   836   %

   837   %If @ {term R} is an equivalence relation and @ {term "Quotient R Abs Rep"}

   838   %then

   839   % 

   840   %@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map_list Abs) (map_list Rep o rep_fset)"}

   841   %%%

   842   %%%\noindent

   843   %%%this theorem will then instantiate the quotients needed in the

   844   %%%injection and cleaning proofs allowing the lifting procedure to

   845   %%%proceed in an unchanged way.

   846 *}

   847 

   848 section {* Lifting of Theorems\label{sec:lift} *}

   849 

   850 text {*

   851 

   852 %%% FIXME Reviewer 3 asks: Section 5 shows the technicalities of

   853 %%% lifting theorems. But there is no clarification about the

   854 %%% correctness. A reader would also be interested in seeing some

   855 %%% discussions about the generality and limitation of the approach

   856 %%% proposed there

   857 

   858   The main benefit of a quotient package is to lift automatically theorems over raw

   859   types to theorems over quotient types. We will perform this lifting in

   860   three phases, called \emph{regularization},

   861   \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.

   862 

   863   The purpose of regularization is to change the quantifiers and abstractions

   864   in a ``raw'' theorem to quantifiers over variables that respect their respective relations

   865   (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}

   866   and @{term Abs} of appropriate types in front of constants and variables

   867   of the raw type so that they can be replaced by the corresponding constants from the

   868   quotient type. The purpose of cleaning is to bring the theorem derived in the

   869   first two phases into the form the user has specified. Abstractly, our

   870   package establishes the following three proof steps:

   871 

   872 %%% FIXME: Reviewer 1 complains that the reader needs to guess the

   873 %%% meaning of reg_thm and inj_thm, as well as the arguments of REG

   874 %%% which are given above. I wouldn't change it.

   875 

   876   \begin{center}

   877   \begin{tabular}{l@ {\hspace{4mm}}l}

   878   1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\

   879   2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\

   880   3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\

   881   \end{tabular}

   882   \end{center}

   883 

   884   \noindent

   885   which means, stringed together, the raw theorem implies the quotient theorem.

   886   In contrast to other quotient packages, our package requires that the user specifies 

   887   both, the @{text "raw_thm"} (as theorem) and the \emph{term} of the @{text "quot_thm"}.\footnote{Though we

   888   also provide a fully automated mode, where the @{text "quot_thm"} is guessed

   889   from the form of @{text "raw_thm"}.} As a result, the user has fine control

   890   over which parts of a raw theorem should be lifted. 

   891 

   892   The second and third proof step performed in package will always succeed if the appropriate

   893   respectfulness and preservation theorems are given. In contrast, the first

   894   proof step can fail: a theorem given by the user does not always

   895   imply a regularized version and a stronger one needs to be proved. An example

   896   for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.

   897   One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},  

   898   but this raw theorem only shows that two particular elements in the

   899   equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a  

   900   more general statement stipulating that the equivalence classes are not 

   901   equal is necessary.  This kind of failure is beyond the scope where the 

   902   quotient package can help: the user has to provide a raw theorem that

   903   can be regularized automatically, or has to provide an explicit proof

   904   for the first proof step.

   905 

   906   In the following we will first define the statement of the

   907   regularized theorem based on @{text "raw_thm"} and

   908   @{text "quot_thm"}. Then we define the statement of the injected theorem, based

   909   on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,

   910   which can all be performed independently from each other.

   911 

   912   We first define the function @{text REG}, which takes the terms of the 

   913   @{text "raw_thm"} and @{text "quot_thm"} as input and returns

   914   @{text "reg_thm"}. The idea

   915   behind this function is that it replaces quantifiers and

   916   abstractions involving raw types by bounded ones, and equalities

   917   involving raw types by appropriate aggregate

   918   equivalence relations. It is defined by simultaneously recursing on 

   919   the structure of  @{text "raw_thm"} and @{text "quot_thm"} as follows:

   920 

   921   \begin{center}

   922   \begin{tabular}{rcl}

   923   \multicolumn{3}{@ {}l}{abstractions:}\smallskip\\

   924   @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ & 

   925   $\begin{cases}

   926   @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\

   927   @{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}

   928   \end{cases}$\smallskip\\

   929   \\

   930   \multicolumn{3}{@ {}l}{universal quantifiers:}\\

   931   @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ & 

   932   $\begin{cases}

   933   @{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\

   934   @{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}

   935   \end{cases}$\smallskip\\

   936   \multicolumn{3}{@ {}l}{equality:}\smallskip\\

   937   %% REL of two equal types is the equality so we do not need a separate case

   938   @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\

   939   \multicolumn{3}{@ {}l}{applications, variables and constants:}\\

   940   @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\

   941   @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\

   942   @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\

   943   \end{tabular}

   944   \end{center}

   945   %

   946   \noindent

   947   In the above definition we omitted the cases for existential quantifiers

   948   and unique existential quantifiers, as they are very similar to the cases

   949   for the universal quantifier. 

   950 

   951   Next we define the function @{text INJ} which takes as argument

   952   @{text "reg_thm"} and @{text "quot_thm"} (both as

   953   terms) and returns @{text "inj_thm"}:

   954 

   955   \begin{center}

   956   \begin{tabular}{rcl}

   957   \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\

   958   @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ & 

   959   $\begin{cases}

   960   @{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\

   961   @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}

   962   \end{cases}$\\

   963   @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ 

   964   & @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\

   965   \multicolumn{3}{@ {\hspace{-4mm}}l}{universal quantifiers:}\\

   966   @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s)"}\\

   967   @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\

   968   \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables and constants:}\smallskip\\

   969   @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\

   970   @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} & $\dn$ & 

   971   $\begin{cases}

   972   @{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\

   973   @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\

   974   \end{cases}$\\

   975   @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} & $\dn$ & 

   976   $\begin{cases}

   977   @{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\

   978   @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\

   979   \end{cases}$\\

   980   \end{tabular}

   981   \end{center}

   982 

   983   \noindent 

   984   In this definition we again omitted the cases for existential and unique existential

   985   quantifiers. 

   986 

   987 %%% FIXME: Reviewer2 citing following sentence: You mention earlier

   988 %%% that this implication may fail to be true. Does that meant that

   989 %%% the `first proof step' is a heuristic that proves the implication

   990 %%% raw_thm \implies reg_thm in some instances, but fails in others?

   991 %%% You should clarify under which circumstances the implication is

   992 %%% being proved here.

   993 %%% Cezary: It would be nice to cite Homeiers discussions in the

   994 %%% Quotient Package manual from HOL (the longer paper), do you agree?

   995 

   996   In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 

   997   start with an implication. Isabelle provides \emph{mono} rules that can split up 

   998   the implications into simpler implicational subgoals. This succeeds for every

   999   monotone connective, except in places where the function @{text REG} replaced,

  1000   for instance, a quantifier by a bounded quantifier. In this case we have 

  1001   rules of the form

  1002 

  1003   @{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)"}

  1004 

  1005   \noindent

  1006   They decompose a bounded quantifier on the right-hand side. We can decompose a

  1007   bounded quantifier anywhere if R is an equivalence relation or

  1008   if it is a relation over function types with the range being an equivalence

  1009   relation. If @{text R} is an equivalence relation we can prove that

  1010 

  1011   @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}    

  1012 

  1013   \noindent

  1014   If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}

  1015 

  1016 %%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we

  1017 %%% should include a proof sketch?

  1018 

  1019   @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}

  1020 

  1021   \noindent

  1022   The last theorem is new in comparison with Homeier's package. There the

  1023   injection procedure would be used to prove such goals and 

  1024   the assumption about the equivalence relation would be used. We use the above theorem directly,

  1025   because this allows us to completely separate the first and the second

  1026   proof step into two independent ``units''.

  1027 

  1028   The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality

  1029   between the terms of the regularized theorem and the injected theorem.

  1030   The proof again follows the structure of the

  1031   two underlying terms and is defined for a goal being a relation between these two terms.

  1032 

  1033   \begin{itemize}

  1034   \item For two constants an appropriate respectfulness theorem is applied.

  1035   \item For two variables, we use the assumptions proved in the regularization step.

  1036   \item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.

  1037   \item For two applications, we check that the right-hand side is an application of

  1038     @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we

  1039     can apply the theorem:

  1040 

  1041     @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}

  1042 

  1043     Otherwise we introduce an appropriate relation between the subterms

  1044     and continue with two subgoals using the lemma:

  1045 

  1046     @{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)"}

  1047   \end{itemize}

  1048 

  1049   We defined the theorem @{text "inj_thm"} in such a way that

  1050   establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be

  1051   achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient

  1052   definitions. First the definitions of all lifted constants

  1053   are used to fold the @{term Rep} with the raw constants. Next for

  1054   all abstractions and quantifiers the lambda and

  1055   quantifier preservation theorems are used to replace the

  1056   variables that include raw types with respects by quantifiers

  1057   over variables that include quotient types. We show here only

  1058   the lambda preservation theorem. Given

  1059   @{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:

  1060 

  1061   @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}

  1062 

  1063   \noindent

  1064   Next, relations over lifted types can be rewritten to equalities

  1065   over lifted type. Rewriting is performed with the following theorem,

  1066   which has been shown by Homeier~\cite{Homeier05}:

  1067 

  1068   @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}

  1069 

  1070   \noindent

  1071   Finally, we rewrite with the preservation theorems. This will result

  1072   in two equal terms that can be solved by reflexivity.

  1073   *}

  1074 

  1075 

  1076 section {* Examples \label{sec:examples} *}

  1077 

  1078 text {*

  1079 

  1080 %%% FIXME Reviewer 1 would like an example of regularized and injected

  1081 %%% statements. He asks for the examples twice, but I would still ignore

  1082 %%% it due to lack of space...

  1083 

  1084   In this section we will show a sequence of declarations for defining the 

  1085   type of integers by quotienting pairs of natural numbers, and

  1086   lifting one theorem. 

  1087 

  1088   A user of our quotient package first needs to define a relation on

  1089   the raw type with which the quotienting will be performed. We give

  1090   the same integer relation as the one presented in \eqref{natpairequiv}:

  1091 

  1092   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1093   \begin{tabular}{@ {}l}

  1094   \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\

  1095   \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}

  1096   \end{tabular}

  1097   \end{isabelle}

  1098 

  1099   \noindent

  1100   Next the quotient type must be defined. This generates a proof obligation that the

  1101   relation is an equivalence relation, which is solved automatically using the

  1102   definition of equivalence and extensionality:

  1103 

  1104   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1105   \begin{tabular}{@ {}l}

  1106   \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\

  1107   \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}

  1108   \end{tabular}

  1109   \end{isabelle}

  1110 

  1111   \noindent

  1112   The user can then specify the constants on the quotient type:

  1113 

  1114   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1115   \begin{tabular}{@ {}l}

  1116   \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]

  1117   \isacommand{fun}~~@{text "add_pair"}~~\isacommand{where}~~%

  1118   @{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\

  1119   \isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%

  1120   \isacommand{is}~~@{text "add_pair"}\\

  1121   \end{tabular}

  1122   \end{isabelle}

  1123 

  1124   \noindent

  1125   The following theorem about addition on the raw level can be proved.

  1126 

  1127   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1128   \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}

  1129   \end{isabelle}

  1130 

  1131   \noindent

  1132   If the user lifts this theorem, the quotient package performs all the lifting

  1133   automatically leaving the respectfulness proof for the constant @{text "add_pair"}

  1134   as the only remaining proof obligation. This property needs to be proved by the user:

  1135