1 (*<*)

     2 theory Paper

     3 imports "Quotient"

     4         "~~/src/HOL/Library/Quotient_Syntax"

     5         "~~/src/HOL/Library/LaTeXsugar"

     6         "~~/src/HOL/Quotient_Examples/FSet"

     7 begin

     8 

     9 notation (latex output)

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

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

    12   implies (infix "\<longrightarrow>" 100) and

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

    14   map_fun ("_ \<singlearr> _" 51) and

    15   fun_rel ("_ \<doublearr> _" 51) and

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

    17   empty_fset ("\<emptyset>") and

    18   union_fset ("_ \<union> _") and

    19   insert_fset ("{_} \<union> _") and

    20   Cons ("_::_") and

    21   concat ("flat") and

    22   concat_fset ("\<Union>") and

    23   Quotient ("Quot _ _ _")

    24 

    25 declare [[show_question_marks = false]]

    26 

    27 ML {*

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

    29 

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

    31   let

    32     val concl =

    33       Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)

    34   in

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

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

    37   end);

    38 *}

    39 

    40 setup {*

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

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

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

    44 *}

    45 

    46 fun add_pair :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" 

    47 where "add_pair (n1, m1) (n2, m2) = (n1 + n2, m1 + m2)"

    48 

    49 fun minus_pair :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" 

    50 where "minus_pair (n, m) = (m, n)"

    51 

    52 fun

    53   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" ("_ \<approx> _" [50, 50] 50) 

    54 where

    55   "intrel (x, y) (u, v) = (x + v = u + y)"

    56 

    57 (*>*)

    58 

    59 section {* Introduction *}

    60 

    61 text {*

    62   \noindent

    63   One might think quotients have been studied to death, but in the

    64   context of theorem provers a number questions concerning them are

    65   far from settled. In this paper we address the question of how to

    66   establish a convenient reasoning infrastructure for quotient

    67   constructions in the Isabelle/HOL theorem prover. Higher-Order Logic

    68   (HOL) consists of a small number of axioms and inference rules over

    69   a simply-typed term-language. Safe reasoning in HOL is ensured by

    70   two very restricted mechanisms for extending the logic: one is the

    71   definition of new constants in terms of existing ones; the other is

    72   the introduction of new types by identifying non-empty subsets in

    73   existing types. Previous work has shown how to use both mechanisms

    74   for dealing with quotient constructions in HOL (see

    75   \cite{Homeier05,Paulson06}).  For example the integers in

    76   Isabelle/HOL are constructed by a quotient construction over the

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

    78 

    79 

    80   \begin{isabelle}\ \ \ \ \ %%%

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

    82   \end{isabelle}

    83 

    84   \noindent

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

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

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

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

    89   in terms of operations on pairs of natural numbers:

    90 

    91   \begin{isabelle}\ \ \ \ \ %%%

    92   @{thm add_pair.simps[where ?n1.0="n\<^isub>1" and ?n2.0="n\<^isub>2" and ?m1.0="m\<^isub>1" and ?m2.0="m\<^isub>2", THEN eq_reflection]}%

    93   \hfill\numbered{addpair}

    94   \end{isabelle}

    95 

    96   \noindent

    97   Negation on integers is defined in terms of swapping of pairs:

    98 

    99   \begin{isabelle}\ \ \ \ \ %%%

   100   @{thm minus_pair.simps[where ?n="n" and ?m="m", THEN eq_reflection]}%

   101   \hfill\numbered{minuspair}

   102   \end{isabelle}

   103 

   104   \noindent

   105   Similarly one can construct the type of finite sets, written @{term

   106   "\<alpha> fset"}, by quotienting the type @{text "\<alpha> list"} according to the

   107   equivalence relation

   108 

   109   \begin{isabelle}\ \ \ \ \ %%%

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

   111   \end{isabelle}

   112 

   113   \noindent

   114   which states that two lists are equivalent if every element in one

   115   list is also member in the other, and vice versa. The empty finite

   116   set, written @{term "{||}"}, can then be defined as the empty list

   117   and the union of two finite sets, written @{text "\<union>"}, as list

   118   append.

   119 

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

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

   122   is the lambda-calculus, whose raw, or un-quotient, terms are defined as

   123 

   124   \begin{isabelle}\ \ \ \ \ %%%

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

   126   \end{isabelle}

   127 

   128   \noindent

   129   The problem with this definition arises from the need to reason

   130   modulo $\alpha$-equivalence, for instance, when one attempts to

   131   prove formally the substitution lemma \cite{Barendregt81} by

   132   induction over the structure of terms. This can be fiendishly

   133   complicated (see \cite[Pages 94--104]{CurryFeys58} for some

   134   ``rough'' sketches of a proof about raw lambda-terms). In contrast,

   135   if we reason about $\alpha$-equated lambda-terms, that means terms

   136   quotient according to $\alpha$-equivalence, then the reasoning

   137   infrastructure provided, for example, by Nominal Isabelle

   138   \cite{UrbanKaliszyk11} makes the formal proof of the substitution

   139   lemma almost trivial. The fundamental reason is that in case of

   140   $\alpha$-equated terms, equality coincides with $\alpha$-equivalence and

   141   we can use for reasoning HOL's built-in notion of ``replacing equals by equals''.

   142 

   143   There is also often a need to consider quotients of parial equivalence relations. For 

   144   example the rational numbers

   145   can be constructed using pairs of integers and the partial equivalence relation

   146 

   147   \begin{isabelle}\ \ \ \ \ %%%

   148   @{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{ratpairequiv}

   149   \end{isabelle}

   150 

   151   \noindent

   152   where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not allowed to be zero.

   153 

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

   155   finite sets, etc.~one needs to establish a reasoning infrastructure

   156   by transferring, or \emph{lifting}, definitions and theorems from

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

   158   (similarly for finite sets, $\alpha$-equated lambda-terms and

   159   rational numbers). This lifting usually requires a reasoning effort

   160   that can be rather repetitive and involves explicit conversions 

   161   between the quotient and raw level in form of abstraction and 

   162   representation functions \cite{Paulson06}.  In principle it is feasible to do this

   163   work manually if one has only a few quotient constructions at

   164   hand. But if they have to be done over and over again, as in Nominal

   165   Isabelle, then manual reasoning is not an option.

   166 

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

   168   theorems and automate the reasoning as much as possible. Before we

   169   delve into the details, let us show how the user interacts with our

   170   quotient package when defining integers. We assume the definitions

   171   involving pairs of natural numbers shown in \eqref{natpairequiv},

   172   \eqref{addpair} and \eqref{minuspair} have already been made. A

   173   quotient can then be introduced by declaring the new type (in this case

   174   @{typ int}), the raw type (that is @{typ "nat \<times> nat"}) and the

   175   equivalence relation (that is @{text intrel} defined in

   176   \eqref{natpairequiv}).

   177 *}

   178 

   179   quotient_type int = "nat \<times> nat" / intrel

   180 

   181 txt {*

   182   \noindent

   183   This declaration requires the user to prove that @{text intrel} is

   184   indeed an equivalence relation, whereby an equivalence 

   185   relation is defined as one that is reflexive, symmetric and

   186   transitive.  This proof obligation can thus be discharged by

   187   unfolding the definitions and using the standard automatic proving

   188   tactic in Isabelle/HOL.

   189 *}

   190     unfolding equivp_reflp_symp_transp

   191     unfolding reflp_def symp_def transp_def

   192     by auto

   193 (*<*)

   194     instantiation int :: "{zero, one, plus, uminus}"

   195     begin

   196 (*>*)

   197 text {*

   198   \noindent

   199   Next we can declare the constants @{text "0"} and @{text "1"} for the 

   200   quotient type @{text int}.

   201 *}

   202     quotient_definition

   203       "0 \<Colon> int"  is  "(0\<Colon>nat, 0\<Colon>nat)" .

   204 

   205     quotient_definition

   206       "1 \<Colon> int"  is  "(1\<Colon>nat, 0\<Colon>nat)" .

   207 

   208 text {*

   209   \noindent

   210   To be useful, we can also need declare two operations for adding two

   211   integers (written @{text plus}) and negating an integer

   212   (written @{text "uminus"}).

   213 *}

   214 

   215     quotient_definition

   216       "plus \<Colon> int \<Rightarrow> int \<Rightarrow> int"  is  add_pair 

   217       by auto

   218 

   219     quotient_definition

   220       "uminus \<Colon> int \<Rightarrow> int"  is  minus_pair 

   221       by auto

   222 (*<*)    

   223     instance ..

   224 

   225     end

   226 (*>*)

   227 

   228 text {*

   229   \noindent

   230   Isabelle/HOL can introduce some convenient short-hand notation for these

   231   operations allowing the user to write

   232   addition as infix operation, for example @{text "i + j"}, and

   233   negation as prefix operation, for example @{text "- i"}.  In both

   234   cases, however, the declaration requires the user to discharge a

   235   proof-obligation which ensures that the operations a

   236   \emph{respectful}. This property ensures that the operations are

   237   well-defined on the quotient level (a formal definition of

   238   respectfulness will be given later). Both proofs can be solved by

   239   the automatic proving tactic in Isabelle/HOL.

   240 

   241   Besides helping with declarations of quotient types and definitions 

   242   of constants, the point of a quotient package is to help with 

   243   proving properties about quotient types. For example we might be

   244   interested in the usual property that zero is an ???. This property 

   245   can be stated as follows:

   246 *}

   247 

   248      lemma zero_add:

   249        shows "0 + i = (i::int)"

   250      proof(descending)

   251 txt {*

   252   \noindent 

   253   The tactic @{text "descending"} automatically transfers this property of integers

   254   to a proof-obligation involving pairs of @{typ nat}s. (There is also

   255   a tactic, called @{text lifting}, which automatically transfers properties

   256   from the raw level to the quotient type.) In case of lemma @{text "zero_add"}

   257   we obtain the subgoal

   258 

   259   \begin{isabelle}\ \ \ \ \ %%%

   260   @{text "add_pair (0, 0) i \<approx> i"}

   261   \end{isabelle}

   262 

   263   \noindent

   264   which can be solved again by the automatic proving tactic @{text "auto"}, as follows

   265 *}

   266      qed(auto)

   267 

   268 text {*

   269   In this simple example the task of the user is to state the property for integers

   270   and use the quotient package and automatic proving tools of Isabelle/HOL to do

   271   the ``rest''. A more interesting example is to establish an induction principle for 

   272   integers. For this we first establish the following induction principle where the 

   273   induction proceeds over two natural numbers. 

   274 *}

   275 

   276     lemma nat_induct2:

   277       assumes "P 0 0"

   278       and     "\<And>n m. P n m \<Longrightarrow> P (Suc n) m"

   279       and     "\<And>n m. P n m \<Longrightarrow> P n (Suc m)"

   280       shows   "P n m"

   281       using assms

   282       by (induction_schema) (pat_completeness, lexicographic_order)

   283 

   284 text {*

   285   \noindent

   286   The symbol @{text "\<And>"} stands for Isabelle/HOL's universal quantifier and

   287   @{text "\<Longrightarrow>"} for its implication.

   288   As can be seen, this induction principle can be conveniently established using the

   289   reasoning infrastructure of the function package \cite{???}, which 

   290   provides the tactics @{text "induction_schema"}, @{text "pat_completeness"}

   291   and @{text "lexicographic_order"}. These tactics enable Isabelle/HOL

   292   to use well-founded induction to prove @{text "nat_induct2"}. Our 

   293   quotient package can now be used to prove the following property:

   294 *}

   295 

   296     lemma int_induct:

   297       assumes "P 0"

   298       and     "\<And>i. P i \<Longrightarrow> P (i + 1)"

   299       and     "\<And>i. P i \<Longrightarrow> P (i + (- 1))"

   300       shows   "P (j::int)"

   301       using assms 

   302       proof (descending)

   303 

   304 txt {*

   305   \noindent

   306   The @{text descending} tactic transfers it to the following proof 

   307   obligation on the raw level.

   308   

   309   @{subgoals[display]}

   310 

   311   \noindent

   312   Note that the variable @{text "j"} in this subgoal is of type

   313   @{text "nat \<times> nat"}. This subgoal cannot be proved automatically by 

   314   @{text auto}, but if we give it the hint to use @{text nat_induct2},

   315   then @{text auto} can discharge it as follows.

   316   

   317 *}

   318        qed (auto intro: nat_induct2)

   319 

   320 text {*

   321   This completes the proof of the induction principle

   322   for integers. Isabelle/HOL would allow us to inspect the 

   323   detailed reasoning steps involved which would confirm that

   324   @{text "int_induct"} has been proved from ``first-principles''

   325   by transforming the property over the quotient type @{text int}

   326   to a corresponding property one on the raw level.

   327 

   328 

   329   In the

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

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

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

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

   334 

   335 %%% FIXME: Referee 1 says:

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

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

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

   339 

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

   341 %%% I wouldn't change it.

   342 

   343   \begin{center}

   344   \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=1.1]

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

   346 

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

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

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

   350 

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

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

   353 

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

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

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

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

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

   359 

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

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

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

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

   364   \end{tikzpicture}

   365   \end{center}

   366 

   367   \noindent

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

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

   370   With this input the package introduces a new type, to which we

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

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

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

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

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

   376   existing type to elements in the new type, % and vice versa,

   377   and can be uniquely

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

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

   380 

   381 

   382   \begin{isabelle}\ \ \ \ \ %%%

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

   384   \end{isabelle}

   385 

   386   \noindent

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

   388   typing information is important.

   389 

   390   Every abstraction and representation function stands for an isomorphism

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

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

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

   394 

   395 

   396   \begin{isabelle}\ \ \ \ \ %%%

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

   398   \end{isabelle}

   399 

   400   \noindent

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

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

   403 

   404   \begin{isabelle}\ \ \ \ \ %%%

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

   406   \hfill\numbered{adddef}

   407   \end{isabelle}

   408 

   409   \noindent

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

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

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

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

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

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

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

   417   flattens lists of lists, defined as follows

   418 

   419   \begin{isabelle}\ \ \ \ \ %%%

   420   \begin{tabular}{@ {}l}

   421   @{thm concat.simps(1)[THEN eq_reflection]}\\

   422   @{thm concat.simps(2)[THEN eq_reflection, where x1="x" and xs1="xs"]}

   423   \end{tabular}

   424   \end{isabelle}

   425 

   426   \noindent

   427   where @{text "@"} is the usual

   428   list append. We expect that the corresponding

   429   operator on finite sets, written @{term "fconcat"},

   430   builds finite unions of finite sets:

   431 

   432   \begin{isabelle}\ \ \ \ \ %%%

   433   \begin{tabular}{@ {}l}

   434   @{thm concat_empty_fset[THEN eq_reflection]}\\

   435   @{thm concat_insert_fset[THEN eq_reflection, where x1="x" and S1="S"]}

   436   \end{tabular}

   437   \end{isabelle}

   438 

   439   \noindent

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

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

   442   that the method  used in the existing quotient

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

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

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

   446 

   447   \begin{isabelle}\ \ \ \ \ %%%

   448   @{text "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}

   449   \end{isabelle}

   450 

   451   \noindent

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

   453   existing quotient packages by introducing an intermediate step and reasoning

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

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

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

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

   458   generate the %%%following

   459   definition

   460 

   461   \begin{isabelle}\ \ \ \ \ %%%

   462   @{text "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}

   463   \end{isabelle}

   464 

   465   \noindent

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

   467   will present a formal definition of our aggregate abstraction and

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

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

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

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

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

   473   from Homeier \cite{Homeier05}.

   474 

   475   {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset}}

   476 

   477 %%%TODO Update the contents.

   478 

   479   In addition we are able to clearly specify what is involved

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

   481   implemented as a ``rough recipe'' in ML-code). A pleasing side-result

   482   is that our procedure for lifting theorems is completely deterministic

   483   following the structure of the theorem being lifted and the theorem

   484   on the quotient level. {\it Space constraints, unfortunately, allow us to only

   485   sketch this part of our work in Section 5 and we defer the reader to a longer

   486   version for the details.} However, we will give in Section 3 and 4 all

   487   definitions that specify the input and output data of our three-step

   488   lifting procedure. Appendix A gives an example how our quotient

   489   package works in practise.

   490 *}

   491 

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

   493 

   494 text {*

   495   \noindent

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

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

   498 

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

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

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

   502   for types and terms are

   503 

   504   \begin{isabelle}\ \ \ \ \ %%%

   505   \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}

   506   @{text "\<sigma>, \<tau> ::= \<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} &

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

   508   \end{tabular}

   509   \end{isabelle}

   510 

   511   \noindent

   512   with types being either type variables or type constructors and terms

   513   being variables, constants, applications or abstractions.

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

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

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

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

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

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

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

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

   522 

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

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

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

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

   527   underlying the first theorem.

   528 

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

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

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

   532   also the following map for function types

   533 

   534   \begin{isabelle}\ \ \ \ \ %%%

   535   @{thm map_fun_def[THEN eq_reflection]}

   536   \end{isabelle}

   537 

   538   \noindent

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

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

   541 

   542   \begin{isabelle}\ \ \ \ \ %%%

   543   @{text "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}

   544   \end{isabelle}

   545 

   546   \noindent

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

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

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

   550   of the type-constructor @{text \<kappa>}.

   551   %% a general type for map all types is difficult to give (algebraic types are

   552   %% easy, but for example the function type is not algebraic

   553   %For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the

   554   %type of the function @{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>"}.

   555   %For example @{text "map_list"}

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

   557   In our implementation we maintain

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

   559 

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

   561   which define equivalence relations in terms of constituent equivalence

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

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

   564   products as %% follows

   565 

   566   \begin{isabelle}\ \ \ \ \ %%%

   567   @{text "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}

   568   \end{isabelle}

   569 

   570   \noindent

   571   Homeier gives also the following operator for defining equivalence

   572   relations over function types

   573   %

   574   \begin{isabelle}\ \ \ \ \ %%%

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

   576   \hfill\numbered{relfun}

   577   \end{isabelle}

   578 

   579   \noindent

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

   581   are needed later on.

   582 

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

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

   585   \end{definition}

   586 

   587   \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}

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

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

   590   \end{definition}

   591 

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

   593   relations, abstraction and representation functions:

   594 

   595   \begin{definition}[Quotient Types]

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

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

   598   holds if and only if

   599   \begin{isabelle}\ \ \ \ \ %%%%

   600   \begin{tabular}{rl}

   601   (i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R"]}\end{isa}\\

   602   (ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R"]}\end{isa}\\

   603   (iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R"]}\end{isa}\\

   604   \end{tabular}

   605   \end{isabelle}

   606   \end{definition}

   607 

   608   \noindent

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

   610   often be proved in terms of the validity of @{term "Quot"} over the constituent

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

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

   613   types:

   614 

   615   \begin{proposition}\label{funquot}

   616   \begin{isa}

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

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

   619   \end{isa}

   620   \end{proposition}

   621 

   622   \noindent

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

   624   always discharge a proof obligation involving @{text "Quot"}. Our quotient

   625   package makes heavy

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

   627   for dealing with \emph{conjugations} of equivalence relations\footnote{That are

   628   symmetric by definition.} defined as follows:

   629 

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

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

   632 

   633   \begin{definition}%%[Composition of Relations]

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

   635   composition defined by

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

   637   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

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

   639   \end{definition}

   640 

   641   \noindent

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

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

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

   645   However, we can prove specific instances of a

   646   quotient theorem for composing particular quotient relations.

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

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

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

   650 

   651   \begin{isabelle}\ \ \ \ \ %%%

   652   \begin{tabular}{r@ {\hspace{1mm}}l}

   653   @{text  "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\

   654                   & @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\

   655   \end{tabular}

   656   \end{isabelle}

   657 *}

   658 

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

   660 

   661 text {*

   662   \noindent

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

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

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

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

   667   the quotient type declaration is therefore

   668 

   669   \begin{isabelle}\ \ \ \ \ %%%

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

   671   \end{isabelle}

   672 

   673   \noindent

   674   and a proof that @{text "R"} is indeed an equivalence relation. The @{text "\<alpha>s"}

   675   indicate the arity of the new type and the type-variables of @{text "\<sigma>"} can only

   676   be contained in @{text "\<alpha>s"}. Two concrete

   677   examples are

   678 

   679 

   680   \begin{isabelle}\ \ \ \ \ %%%

   681   \begin{tabular}{@ {}l}

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

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

   684   \end{tabular}

   685   \end{isabelle}

   686 

   687   \noindent

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

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

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

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

   692   relations are omitted).  Given this data, we define for declarations shown in

   693   \eqref{typedecl} the quotient types internally as

   694 

   695   \begin{isabelle}\ \ \ \ \ %%%

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

   697   \end{isabelle}

   698 

   699   \noindent

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

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

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

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

   704   abstraction and representation functions

   705 

   706   \begin{isabelle}\ \ \ \ \ %%%

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

   708   \end{isabelle}

   709 

   710   \noindent

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

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

   713   to work with the following derived abstraction and representation functions

   714 

   715   \begin{isabelle}\ \ \ \ \ %%%

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

   717   \end{isabelle}

   718 

   719   \noindent

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

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

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

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

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

   725   following property holds  for every quotient type

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

   727 

   728   \begin{proposition}

   729   \begin{isa}@{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.\end{isa}

   730   \end{proposition}

   731 

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

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

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

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

   736 

   737   \begin{isabelle}\ \ \ \ \ %%%

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

   739   \end{isabelle}

   740 

   741   \noindent

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

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

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

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

   746 

   747   \begin{isabelle}\ \ \ \ \ %%%

   748   \begin{tabular}{@ {}l}

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

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

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

   752   \end{tabular}

   753   \end{isabelle}

   754 

   755   \noindent

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

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

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

   759 

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

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

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

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

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

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

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

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

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

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

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

   771   @{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

   772   for @{text REP}.

   773   %

   774   \begin{center}

   775   \hfill

   776   \begin{tabular}{@ {\hspace{2mm}}l@ {}}

   777   \multicolumn{1}{@ {}l}{equal types:}\\

   778   @{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\hspace{5mm}%\\

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

   780   \multicolumn{1}{@ {}l}{function types:}\\

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

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

   783   \multicolumn{1}{@ {}l}{equal type constructors:}\\

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

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

   786   \multicolumn{1}{@ {}l}{unequal type constructors:}\\

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

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

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

   790   \end{center}

   791   %

   792   \noindent

   793   In the last two clauses are subtle. We rely in them on the fact that the type @{text "\<alpha>s

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

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

   796   list"}). This data is given by declarations shown in \eqref{typedecl}.

   797   The quotient construction ensures that the type variables in @{text

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

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

   800   @{text "\<rho>s \<kappa>"}. This calculation determines what are the types in place

   801   of the type variables @{text "\<alpha>s"} in the instance of

   802   quotient type @{text "\<alpha>s \<kappa>\<^isub>q"}---namely @{text "\<tau>s"}, and the corresponding

   803   types in place of the @{text "\<alpha>s"} in the raw type @{text "\<rho>s \<kappa>"}---namely @{text "\<sigma>s'"}. The

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

   805   type as follows:

   806   %

   807   \begin{center}

   808   \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

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

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

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

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

   813   \end{tabular}

   814   \end{center}

   815   %

   816   \noindent

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

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

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

   820   @{text "MAP'"}.

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

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

   823   In this case @{text MAP} generates  the

   824   aggregate map-function:

   825 

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

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

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

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

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

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

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

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

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

   835 

   836   \begin{isabelle}\ \ \ \ \ %%%

   837   @{text "\<lambda>a b. map_prod (map_list a) b"}

   838   \end{isabelle}

   839 

   840   \noindent

   841   which is essential in order to define the corresponding aggregate

   842   abstraction and representation functions.

   843 

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

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

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

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

   848   the abstraction function

   849 

   850   \begin{isabelle}\ \ \ %%%

   851   \begin{tabular}{l}

   852   @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\

   853   \mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}

   854   \end{tabular}

   855   \end{isabelle}

   856 

   857   \noindent

   858   In our implementation we further

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

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

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

   862 

   863   \begin{isabelle}\ \ \ \ \ %%%

   864   @{text "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}

   865   \end{isabelle}

   866 

   867   \noindent

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

   869 

   870   \begin{isabelle}\ \ \ \ \ %%%

   871   @{text "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}

   872   \end{isabelle}

   873 

   874   \noindent

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

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

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

   878   Consequently, all definitions in the quotient package

   879   are of the general form

   880 

   881   \begin{isabelle}\ \ \ \ \ %%%

   882   \mbox{@{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}}

   883   \end{isabelle}

   884 

   885   \noindent

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

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

   888   generated from the declaration given by the user.

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

   890   that the terms involved are all typable.

   891 

   892   \begin{lemma}

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

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

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

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

   897   \end{lemma}

   898 

   899   \begin{proof}

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

   901   The cases of equal types and function types are

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   916   \end{proof}

   917 *}

   918 

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

   920 

   921 text {*

   922   \noindent

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

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

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

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

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

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

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

   930   defined

   931   for raw lambda-terms as follows

   932 

   933   \begin{isabelle}

   934   \begin{center}

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

   936   @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\smallskip\\

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

   938   \end{center}

   939   \end{isabelle}

   940 

   941   \noindent

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

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

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

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

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

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

   948   compositions.

   949 

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

   951 %%% with quotient composition.

   952 

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

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

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

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

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

   958   elsewhere.

   959 

   960   \begin{center}

   961   \hfill

   962   \begin{tabular}{l}

   963   \multicolumn{1}{@ {}l}{equal types:}

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

   965    \multicolumn{1}{@ {}l}{equal type constructors:}\\

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

   967   \multicolumn{1}{@ {}l}{unequal type constructors:}\\

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

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

   970   \end{center}

   971 

   972   \noindent

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

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

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

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

   977 

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

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

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

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

   982   we generate the following proof obligation

   983 

   984   \begin{isabelle}\ \ \ \ \ %%%

   985   @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}.

   986   \end{isabelle}

   987 

   988   \noindent

   989   Homeier calls these proof obligations \emph{respectfulness

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

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

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

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

   994   And for every instantiation of the types, a corresponding

   995   respectfulness theorem is necessary.

   996 

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

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

   999   this obligation is %%as follows

  1000 

  1001   \begin{isabelle}\ \ \ \ \ %%%

  1002   @{text  "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}

  1003   \end{isabelle}

  1004 

  1005   \noindent

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

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

  1008   using extensionality to obtain the false statement

  1009 

  1010   \begin{isabelle}\ \ \ \ \ %%%

  1011   @{text "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}

  1012   \end{isabelle}

  1013 

  1014   \noindent

  1015   In contrast, lifting a theorem about @{text "append"} to a theorem describing

  1016   the union of finite sets will mean to discharge the proof obligation

  1017 

  1018   \begin{isabelle}\ \ \ \ \ %%%

  1019   @{text "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}

  1020   \end{isabelle}

  1021 

  1022   \noindent

  1023   To do so, we have to establish

  1024 

  1025   \begin{isabelle}\ \ \ \ \ %%%

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

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

  1028   \end{isabelle}

  1029 

  1030   \noindent

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

  1032 

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

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

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

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

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

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

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

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

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

  1042   preservation property is as follows

  1043 

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

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

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

  1047 %%% and its corresponding lifted constant?

  1048 

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

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

  1051 

  1052   \begin{isabelle}\ \ \ \ \ %%%

  1053   @{text "Quot 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"}

  1054   \end{isabelle}

  1055 

  1056   \noindent

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

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

  1059 

  1060   \begin{isabelle}\ \ \ \ \ %%%

  1061   @{text "(Rep \<singlearr> map_list Rep \<singlearr> map_list Abs) cons = cons"}

  1062   \end{isabelle}

  1063 

  1064   \noindent

  1065   under the assumption @{term "Quotient R Abs Rep"}. The point is that if we have

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

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

  1068   then we need to show this preservation property.

  1069 

  1070   %%%@ {thm [display, indent=10] Cons_prs2}

  1071 

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

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

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

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

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

  1077   %quotients composed with the usual function composition.

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

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

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

  1081   %This becomes especially interesting

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

  1083   %intermediate step.

  1084   %

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

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

  1087   %theorem which allows quotienting inside the container:

  1088   %

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

  1090   %then

  1091   %

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

  1093   %%%

  1094   %%%\noindent

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

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

  1097   %%%proceed in an unchanged way.

  1098 *}

  1099 

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

  1101 

  1102 text {*

  1103 

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

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

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

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

  1108 %%% proposed there

  1109 

  1110 %%% TODO: This introduction is same as the introduction to the previous section.

  1111 

  1112   \noindent

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

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

  1115   three phases, called \emph{regularization},

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

  1117   Space restrictions, unfortunately, prevent us from giving anything but a sketch of these three

  1118   phases. However, we will precisely define the input and output data of these phases

  1119   (this was omitted in \cite{Homeier05}).

  1120 

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

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

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

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

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

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

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

  1128   package establishes the following three proof steps:

  1129 

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

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

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

  1133 

  1134   \begin{center}