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 (****

    10 

    11 ** things to do for the next version

    12 *

    13 * - what are quot_thms?

    14 * - what do all preservation theorems look like,

    15     in particular preservation for quotient

    16     compositions

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

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

    19 

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

    21 

    22 *)

    23 

    24 notation (latex output)

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

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

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

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

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

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

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

    32   empty_fset ("\<emptyset>") and

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

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

    35   Cons ("_::_") and

    36   concat ("flat") and

    37   concat_fset ("\<Union>") and

    38   Quotient ("Quot _ _ _")

    39 

    40   

    41 

    42 ML {*

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

    44 

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

    46   let

    47     val concl =

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

    49   in

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

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

    52   end);

    53 *}

    54 

    55 setup {*

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

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

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

    59 *}

    60 

    61 lemma insert_preserve2:

    62   shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =

    63          (id ---> rep_fset ---> abs_fset) op #"

    64   by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])

    65 

    66 lemma list_all2_symp:

    67   assumes a: "equivp R"

    68   and b: "list_all2 R xs ys"

    69   shows "list_all2 R ys xs"

    70 using list_all2_lengthD[OF b] b

    71 apply(induct xs ys rule: list_induct2)

    72 apply(auto intro: equivp_symp[OF a])

    73 done

    74 

    75 lemma concat_rsp_unfolded:

    76   "\<lbrakk>list_all2 list_eq a ba; list_eq ba bb; list_all2 list_eq bb b\<rbrakk> \<Longrightarrow> list_eq (concat a) (concat b)"

    77 proof -

    78   fix a b ba bb

    79   assume a: "list_all2 list_eq a ba"

    80   assume b: "list_eq ba bb"

    81   assume c: "list_all2 list_eq bb b"

    82   have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof

    83     fix x

    84     show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof

    85       assume d: "\<exists>xa\<in>set a. x \<in> set xa"

    86       show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])

    87     next

    88       assume e: "\<exists>xa\<in>set b. x \<in> set xa"

    89       have a': "list_all2 list_eq ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])

    90       have b': "list_eq bb ba" by (rule equivp_symp[OF list_eq_equivp, OF b])

    91       have c': "list_all2 list_eq b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])

    92       show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])

    93     qed

    94   qed

    95   then show "list_eq (concat a) (concat b)" by auto

    96 qed

    97 

    98 (*>*)

    99 

   100 

   101 section {* Introduction *}

   102 

   103 text {* 

   104   \noindent

   105   One might think quotients have been studied to death, but in the context of

   106   theorem provers many questions concerning them are far from settled. In

   107   this paper we address the question of how to establish a convenient reasoning 

   108   infrastructure

   109   for quotient constructions in the Isabelle/HOL 

   110   theorem prover. Higher-Order Logic (HOL) consists

   111   of a small number of axioms and inference rules over a simply-typed

   112   term-language. Safe reasoning in HOL is ensured by two very restricted

   113   mechanisms for extending the logic: one is the definition of new constants

   114   in terms of existing ones; the other is the introduction of new types by

   115   identifying non-empty subsets in existing types. Previous work has shown how

   116   to use both mechanisms for dealing with quotient constructions in HOL (see

   117   \cite{Homeier05,Paulson06}).  For example the integers in Isabelle/HOL are

   118   constructed by a quotient construction over the type @{typ "nat \<times> nat"} and

   119   the equivalence relation

   120 

   121 

   122   \begin{isabelle}\ \ \ \ \ %%%

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

   124   \end{isabelle}

   125 

   126   \noindent

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

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

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

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

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

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

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

   134   Similarly one can construct %%the type of 

   135   finite sets, written @{term "\<alpha> fset"}, 

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

   137 

   138   \begin{isabelle}\ \ \ \ \ %%%

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

   140   \end{isabelle}

   141 

   142   \noindent

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

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

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

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

   147 

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

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

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

   151   

   152   \begin{isabelle}\ \ \ \ \ %%%

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

   154   \end{isabelle}

   155   

   156   \noindent

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

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

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

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

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

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

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

   164   for example, by Nominal Isabelle %%\cite{UrbanKaliszyk11}

   165   makes the formal 

   166   proof of the substitution lemma almost trivial. 

   167 

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

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

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

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

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

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

   174   In principle it is feasible to do this work manually, if one has only a few quotient

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

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

   177 

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

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

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

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

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

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

   184 

   185 %%% FIXME: Referee 1 says:

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

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

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

   189 

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

   191 %%% I wouldn't change it.

   192 

   193   \begin{center}

   194   \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=0.9]

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

   196   

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

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

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

   200   

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

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

   203 

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

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

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

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

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

   209   

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

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

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

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

   214   \end{tikzpicture}

   215   \end{center}

   216 

   217   \noindent

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

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

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

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

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

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

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

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

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

   227   and can be uniquely

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

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

   230 

   231 

   232   \begin{isabelle}\ \ \ \ \ %%%

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

   234   \end{isabelle}

   235 

   236   \noindent

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

   238   typing information is important. 

   239 

   240   Every abstraction and representation function stands for an isomorphism

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

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

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

   244 

   245 

   246   \begin{isabelle}\ \ \ \ \ %%%

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

   248   \end{isabelle}

   249 

   250   \noindent

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

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

   253 

   254   \begin{isabelle}\ \ \ \ \ %%%

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

   256   \hfill\numbered{adddef}

   257   \end{isabelle}

   258 

   259   \noindent

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

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

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

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

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

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

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

   267   flattens lists of lists, defined as follows

   268 

   269   \begin{isabelle}\ \ \ \ \ %%%

   270   @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm} 

   271   @{thm concat.simps(2)[THEN eq_reflection, no_vars]}

   272   \end{isabelle}

   273 

   274   \noindent

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

   276   list append. We expect that the corresponding 

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

   278   builds finite unions of finite sets:

   279 

   280   \begin{isabelle}\ \ \ \ \ %%%

   281   @{thm concat_empty_fset[THEN eq_reflection, no_vars]}\hspace{10mm} 

   282   @{thm concat_insert_fset[THEN eq_reflection, no_vars]}

   283   \end{isabelle}

   284 

   285   \noindent

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

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

   288   that the method  used in the existing quotient

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

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

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

   292 

   293   \begin{isabelle}\ \ \ \ \ %%%

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

   295   \end{isabelle}

   296 

   297   \noindent

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

   299   existing quotient packages by introducing an intermediate step and reasoning

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

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

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

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

   304   generate the %%%following 

   305   definition

   306 

   307   \begin{isabelle}\ \ \ \ \ %%%

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

   309   \end{isabelle}

   310 

   311   \noindent

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

   313   will present a formal definition of our aggregate abstraction and

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

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

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

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

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

   319   from Homeier \cite{Homeier05}.

   320 

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

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

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

   324   is that our procedure for lifting theorems is completely deterministic

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

   326   on the quotient level. Space constraints, unfortunately, allow us to only 

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

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

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

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

   331   package works in practise.

   332 *}

   333 

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

   335 

   336 text {*

   337   \noindent

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

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

   340 

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

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

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

   344   for types and terms are

   345 

   346   \begin{isabelle}\ \ \ \ \ %%%

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

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

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

   350   \end{tabular}

   351   \end{isabelle}

   352 

   353   \noindent

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

   355   being variables, constants, applications or abstractions.

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

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

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

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

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

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

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

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

   364 

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

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

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

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

   369   underlying the first theorem.

   370 

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

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

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

   374   also the following map for function types

   375 

   376   \begin{isabelle}\ \ \ \ \ %%%

   377   @{thm map_fun_def[no_vars, THEN eq_reflection]}

   378   \end{isabelle}

   379 

   380   \noindent

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

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

   383 

   384   \begin{isabelle}\ \ \ \ \ %%%

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

   386   \end{isabelle}

   387 

   388   \noindent

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

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

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

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

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

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

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

   396   %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>"}. 

   397   %For example @{text "map_list"}

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

   399   In our implementation we maintain

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

   401 

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

   403   which define equivalence relations in terms of constituent equivalence

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

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

   406   products as %% follows

   407   

   408   \begin{isabelle}\ \ \ \ \ %%%

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

   410   \end{isabelle}

   411 

   412   \noindent

   413   Homeier gives also the following operator for defining equivalence 

   414   relations over function types

   415   %

   416   \begin{isabelle}\ \ \ \ \ %%%

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

   418   \hfill\numbered{relfun}

   419   \end{isabelle}

   420   

   421   \noindent

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

   423   are needed later on.

   424 

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

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

   427   \end{definition}

   428 

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

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

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

   432   \end{definition}

   433 

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

   435   relations, abstraction and representation functions:

   436 

   437   \begin{definition}[Quotient Types]

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

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

   440   holds if and only if

   441   \begin{isabelle}\ \ \ \ \ %%%%

   442   \begin{tabular}{rl}

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

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

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

   446   \end{tabular}

   447   \end{isabelle}

   448   \end{definition}

   449 

   450   \noindent

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

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

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

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

   455   types:

   456  

   457   \begin{proposition}\label{funquot}

   458   \begin{isa}

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

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

   461   \end{isa}

   462   \end{proposition}

   463 

   464   \noindent

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

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

   467   package makes heavy 

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

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

   470   symmetric by definition.} defined as follows:

   471 

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

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

   474 

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

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

   477   composition defined by 

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

   479   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

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

   481   \end{definition}

   482 

   483   \noindent

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

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

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

   487   However, we can prove specific instances of a

   488   quotient theorem for composing particular quotient relations.

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

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

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

   492 

   493   \begin{isabelle}\ \ \ \ \ %%%

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

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

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

   497   \end{tabular}

   498   \end{isabelle}

   499 *}

   500 

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

   502 

   503 text {*

   504   \noindent

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

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

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

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

   509   the quotient type declaration is therefore

   510 

   511   \begin{isabelle}\ \ \ \ \ %%%

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

   513   \end{isabelle}

   514 

   515   \noindent

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

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

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

   519   examples are

   520 

   521   

   522   \begin{isabelle}\ \ \ \ \ %%%

   523   \begin{tabular}{@ {}l}

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

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

   526   \end{tabular}

   527   \end{isabelle}

   528 

   529   \noindent

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

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

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

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

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

   535   \eqref{typedecl} the quotient types internally as

   536   

   537   \begin{isabelle}\ \ \ \ \ %%%

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

   539   \end{isabelle}

   540 

   541   \noindent

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

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

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

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

   546   abstraction and representation functions 

   547 

   548   \begin{isabelle}\ \ \ \ \ %%%

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

   550   \end{isabelle}

   551 

   552   \noindent 

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

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

   555   to work with the following derived abstraction and representation functions

   556 

   557   \begin{isabelle}\ \ \ \ \ %%%

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

   559   \end{isabelle}

   560   

   561   \noindent

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

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

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

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

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

   567   following property holds  for every quotient type 

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

   569 

   570   \begin{proposition}

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

   572   \end{proposition}

   573 

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

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

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

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

   578 

   579   \begin{isabelle}\ \ \ \ \ %%%

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

   581   \end{isabelle}

   582 

   583   \noindent

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

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

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

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

   588 

   589   \begin{isabelle}\ \ \ \ \ %%%

   590   \begin{tabular}{@ {}l}

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

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

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

   594   \end{tabular}

   595   \end{isabelle}

   596   

   597   \noindent

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

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

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

   601 

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

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

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

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

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

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

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

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

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

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

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

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

   614   for @{text REP}.

   615   %

   616   \begin{center}

   617   \hfill

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   632   \end{center}

   633   %

   634   \noindent

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

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

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

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

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

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

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

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

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

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

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

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

   647   type as follows:

   648   %

   649   \begin{center}

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

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

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

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

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

   655   \end{tabular}

   656   \end{center}

   657   %

   658   \noindent

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

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

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

   662   @{text "MAP'"}.

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

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

   665   In this case @{text MAP} generates  the 

   666   aggregate map-function:

   667 

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

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

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

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

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

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

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

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

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

   677 

   678   \begin{isabelle}\ \ \ \ \ %%%

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

   680   \end{isabelle}

   681 

   682   \noindent

   683   which is essential in order to define the corresponding aggregate 

   684   abstraction and representation functions.

   685   

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

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

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

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

   690   the abstraction function

   691 

   692   \begin{isabelle}\ \ \ %%%

   693   \begin{tabular}{l}

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

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

   696   \end{tabular}

   697   \end{isabelle}

   698 

   699   \noindent

   700   In our implementation we further

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

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

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

   704 

   705   \begin{isabelle}\ \ \ \ \ %%%

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

   707   \end{isabelle}

   708 

   709   \noindent

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

   711 

   712   \begin{isabelle}\ \ \ \ \ %%%

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

   714   \end{isabelle}

   715 

   716   \noindent

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

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

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

   720   Consequently, all definitions in the quotient package 

   721   are of the general form

   722   

   723   \begin{isabelle}\ \ \ \ \ %%%

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

   725   \end{isabelle}

   726   

   727   \noindent

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

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

   730   generated from the declaration given by the user.

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

   732   that the terms involved are all typable.

   733 

   734   \begin{lemma}

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

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

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

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

   739   \end{lemma}

   740 

   741   \begin{proof}

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

   743   The cases of equal types and function types are

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   758   \end{proof}

   759 *}

   760 

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

   762 

   763 text {*

   764   \noindent

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

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

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

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

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

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

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

   772   defined 

   773   for raw lambda-terms as follows

   774 

   775   \begin{isabelle}

   776   \begin{center}

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

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

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

   780   \end{center}

   781   \end{isabelle}

   782 

   783   \noindent

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

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

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

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

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

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

   790   compositions. 

   791 

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

   793 %%% with quotient composition.

   794 

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

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

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

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

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

   800   elsewhere.

   801 

   802   \begin{center}

   803   \hfill

   804   \begin{tabular}{l}

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

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

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

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

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

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

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

   812   \end{center}

   813 

   814   \noindent

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

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

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

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

   819 

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

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

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

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

   824   we generate the following proof obligation

   825   

   826   \begin{isabelle}\ \ \ \ \ %%%

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

   828   \end{isabelle}

   829   

   830   \noindent

   831   Homeier calls these proof obligations \emph{respectfulness

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

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

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

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

   836   And for every instantiation of the types, a corresponding

   837   respectfulness theorem is necessary.

   838 

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

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

   841   this obligation is %%as follows

   842    

   843   \begin{isabelle}\ \ \ \ \ %%%

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

   845   \end{isabelle}

   846   

   847   \noindent

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

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

   850   using extensionality to obtain the false statement

   851 

   852   \begin{isabelle}\ \ \ \ \ %%%

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

   854   \end{isabelle}

   855 

   856   \noindent

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

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

   859 

   860   \begin{isabelle}\ \ \ \ \ %%%

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

   862   \end{isabelle}

   863 

   864   \noindent

   865   To do so, we have to establish

   866   

   867   \begin{isabelle}\ \ \ \ \ %%%

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

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

   870   \end{isabelle}

   871 

   872   \noindent

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

   874 

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

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

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

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

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

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

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

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

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

   884   preservation property is as follows

   885 

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

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

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

   889 %%% and its corresponding lifted constant?

   890 

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

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

   893 

   894   \begin{isabelle}\ \ \ \ \ %%%

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

   896   \end{isabelle}

   897 

   898   \noindent

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

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

   901 

   902   \begin{isabelle}\ \ \ \ \ %%%

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

   904   \end{isabelle}

   905 

   906   \noindent

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

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

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

   910   then we need to show this preservation property.

   911 

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

   913 

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

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

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

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

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

   919   %quotients composed with the usual function composition.

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

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

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

   923   %This becomes especially interesting

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

   925   %intermediate step.

   926   %

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

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

   929   %theorem which allows quotienting inside the container:

   930   %

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

   932   %then

   933   % 

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

   935   %%%

   936   %%%\noindent

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

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

   939   %%%proceed in an unchanged way.

   940 *}

   941 

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

   943 

   944 text {*

   945 

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

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

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

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

   950 %%% proposed there

   951 

   952   \noindent

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

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

   955   three phases, called \emph{regularization},

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

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

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

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

   960 

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

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

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

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

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

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

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

   968   package establishes the following three proof steps:

   969 

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

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

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

   973 

   974   \begin{center}

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

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

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

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

   979   \end{tabular}

   980   \end{center}

   981 

   982   \noindent

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

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

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

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

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

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

   989 

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

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

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

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

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

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

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

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

   998   more general statement stipulating that the equivalence classes are not 

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

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

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

  1002   for the first proof step. Homeier gives more details about this issue

  1003   in the long version of \cite{Homeier05}.

  1004 

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

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

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

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

  1009   which can all be performed independently from each other.

  1010 

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

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

  1013   @{text "reg_thm"}. The idea

  1014   behind this function is that it replaces quantifiers and

  1015   abstractions involving raw types by bounded ones, and equalities

  1016   involving raw types by appropriate aggregate

  1017   equivalence relations. It is defined by simultaneous recursion on 

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

  1019   %

  1020   \begin{center}

  1021   \begin{tabular}{@ {}l@ {}}

  1022   \multicolumn{1}{@ {}l@ {}}{abstractions:}\\%%\smallskip\\

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

  1024   $\begin{cases}

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

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

  1027   \end{cases}$\\%%\smallskip\\

  1028   \multicolumn{1}{@ {}l@ {}}{universal quantifiers:}\\

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

  1030   $\begin{cases}

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

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

  1033   \end{cases}$\\%%\smallskip\\

  1034   \multicolumn{1}{@ {}l@ {}}{equality:  \hspace{3mm}%%}\smallskip\\

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

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

  1037   \multicolumn{1}{@ {}l@ {}}{applications, variables and constants:}\\

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

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

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

  1041   \end{tabular}

  1042   \end{center}

  1043   %

  1044   \noindent

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

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

  1047   for the universal quantifier. 

  1048 

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

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

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

  1052 

  1053   \begin{center}

  1054   \begin{tabular}{l}

  1055   \multicolumn{1}{@ {}l}{abstractions:}\\

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

  1057   \hspace{18mm}$\begin{cases}

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

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

  1060   \end{cases}$\smallskip\\

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

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

  1063   \multicolumn{1}{@ {}l}{universal quantifiers:}\\

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

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

  1066   \multicolumn{1}{@ {}l}{applications, variables and constants:}\smallskip\\

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

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

  1069   $\begin{cases}

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

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

  1072   \end{cases}$\\

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

  1074   $\begin{cases}

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

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

  1077   \end{cases}$\\

  1078   \end{tabular}

  1079   \end{center}

  1080 

  1081   \noindent 

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

  1083   quantifiers. 

  1084 

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

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

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

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

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

  1090 %%% being proved here.

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

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

  1093 

  1094   In the first phase, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 

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

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

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

  1098   for instance, a quantifier by a bounded quantifier. To decompose them, we have 

  1099   to prove that the relations involved are aggregate equivalence relations.

  1100 

  1101   

  1102   %In this case we have 

  1103   %rules of the form

  1104   %

  1105   % \begin{isabelle}\ \ \ \ \ %%%

  1106   %@{text "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}

  1107   %\end{isabelle}

  1108 

  1109   %\noindent

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

  1111   %bounded quantifier anywhere if R is an equivalence relation or

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

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

  1114 

  1115   %\begin{isabelle}\ \ \ \ \ %%%

  1116   %@{text "\<forall>x \<in> Resp R. P x = \<forall>x. P x"}    

  1117   %\end{isabelle}

  1118 

  1119   %\noindent

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

  1121 

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

  1123 %%% should include a proof sketch?

  1124 

  1125   %\begin{isabelle}\ \ \ \ \ %%%

  1126   %@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}

  1127   %\end{isabelle}

  1128 

  1129   %\noindent

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

  1131   %injection procedure would be used to prove such goals and 

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

  1133   %because this allows us to completely separate the first and the second

  1134   %proof step into two independent ``units''.