10 print_syntax

     8 (****

     9 

    10 ** things to do for the next version

    11 *

    12 * - what are quot_thms?

    13 * - what do all preservation theorems look like,

    14     in particular preservation for quotient

    15     compositions

    16 *)

    13   rel_conj ("_ OOO _" [53, 53] 52) and

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

    14   "op -->" (infix "\<rightarrow>" 100) and

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

    15   "==>" (infix "\<Rightarrow>" 100) and

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

    16   fun_map (infix "\<longrightarrow>" 51) and

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

    17   fun_rel (infix "\<Longrightarrow>" 51) and

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

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

    19   fempty ("\<emptyset>\<^isub>f") and

    26   fempty ("\<emptyset>") and

    20   funion ("_ \<union>\<^isub>f _") and

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

    21   Cons ("_::_") 

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

    29   Cons ("_::_") and

    30   concat ("flat") and

    31   fconcat ("\<Union>")

    32  

    49   \end{flushright}\smallskip

    64   \end{flushright}

    50 

    65 

    51   \noindent

    66   \noindent

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

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

    59   understood how to use both mechanisms for dealing with quotient constructions in

    74   understood how to use both mechanisms for dealing with quotient

    60   HOL (see \cite{Homeier05,Paulson06}).  For example the integers

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

    61   in Isabelle/HOL are constructed by a quotient construction over the type

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

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

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

    63 

    78 

    64   @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"}

    79   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

    81   \end{isabelle}

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

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

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

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

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

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

    71   in terms of operations on pairs of natural numbers (namely @{text "add\<^bsub>nat\<times>nat\<^esub>

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

    72   (x\<^isub>1, y\<^isub>1) (x\<^isub>2, y\<^isub>2) \<equiv> (x\<^isub>1 +

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

    73   x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}).  Similarly one can construct the

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

    74   type of finite sets by quotienting lists according to the equivalence

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

    75   relation

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

    76 

    93 

    77   @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}

    94   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

    78 

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

    79   \noindent

    96   \end{isabelle}

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

    97 

    81   member in the other (@{text "\<in>"} stands here for membership in lists). The

    98   \noindent

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

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

    83   empty list and union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append. 

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

    84 

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

    85   Another important area of quotients is reasoning about programming language

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

    86   calculi. A simple example are lambda-terms defined as

   103 

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

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

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

   107 

   108 

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

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

   111   \end{isabelle}

   112 

   113   \noindent

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

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

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

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

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

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

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

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

   122   proof of the substitution lemma almost trivial. 

   123 

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

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

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

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

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

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

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

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

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

   133 

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

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

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

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

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

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

    89   @{text "t ::= x | t t | \<lambda>x.t"}

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

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

   144   

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

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

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

   148   

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

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

   151 

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

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

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

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

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

   157   

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

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

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

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

   162 

   163   \end{tikzpicture}

    93   The difficulty with this definition of lambda-terms arises when, for 

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

    94   example, proving formally the substitution lemma ...

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

    95   On the other hand if we reason about alpha-equated lambda-terms, that means

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

    96   terms quotient according to alpha-equivalence, then reasoning infrastructure

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

    97   can be introduced that make the formal proof of the substitution lemma

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

    98   almost trivial. 

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

    99 

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

   100 

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

   101   The problem is that in order to be able to reason about integers, finite sets

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

   102   and alpha-equated lambda-terms one needs to establish a reasoning infrastructure by

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

   103   transferring, or \emph{lifting}, definitions and theorems from the ``raw''

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

   104   type @{typ "nat \<times> nat"} to the quotient type @{typ int} (similarly for

   178 

   105   @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}, and also for raw lambda-terms

   179 

   106   and alpha-equated lambda-terms). This lifting usually

   180   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   107   requires a \emph{lot} of tedious reasoning effort.  The purpose of a \emph{quotient

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

   108   package} is to ease the lifting and automate the reasoning as much as

   182   \end{isabelle}

   109   possible. While for integers and finite sets teh tedious reasoning needs

   183 

   110   to be done only once, Nominal Isabelle providing a reasoning infrastructure 

   184   \noindent

   111   for binders and @{text "\<alpha>"}-equated terms it needs to be done over and over 

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

   112   again.

   186   typing information is important. 

   113 

   187 

   114   Such a package is a central component of the new version of

   188   Every abstraction and representation function stands for an isomorphism

   115   Nominal Isabelle where representations of alpha-equated terms are

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

   116   constructed according to specifications given by the user.

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

   117 

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

   118   

   192 

   119   In the context of HOL, there have been several quotient packages (...). The

   193 

   120   most notable is the one by Homeier (...) implemented in HOL4. However, what is

   194   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   121   surprising, none of them can deal compositions of quotients, for example with 

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

   122   lifting theorems about @{text "concat"}:

   196   \end{isabelle}

   123 

   197 

   124   @{thm [display] concat.simps(1)}

   198   \noindent

   125   @{thm [display] concat.simps(2)[no_vars]}

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

   126 

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

   127   \noindent

   201 

   128   One would like to lift this definition to the operation:

   202    \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   129 

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

   130   @{thm [display] fconcat_empty[no_vars]}

   204   \hfill\numbered{adddef}

   131   @{thm [display] fconcat_insert[no_vars]}

   205   \end{isabelle}

   132 

   206 

   133   \noindent

   207   \noindent

   134   What is special about this operation is that we have as input

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

   135   lists of lists which after lifting turn into finite sets of finite

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

   136   sets.

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

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

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

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

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

   215   flattens lists of lists, defined as follows

   216 

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

   218 

   219   \noindent

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

   221   builds finite unions of finite sets:

   222 

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

   224 

   225   \noindent

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

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

   228   that the method  used in the existing quotient

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

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

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

   232 

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

   234 

   235   \noindent

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

   237   existing quotient packages by introducing an intermediate step and reasoning

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

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

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

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

   242   generate the following definition

   243 

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

   245 

   246   \noindent

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

   248   will present a formal definition of our aggregate abstraction and

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

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

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

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

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

   254   from Homeier \cite{Homeier05}.

   255 

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

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

   258   lifted from the raw level to the quotient level into one giant list. Our

   259   quotient package is the first one that is modular so that it allows to lift

   260   single higher-order theorems separately. This has the advantage for the user of being able to develop a

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

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

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

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

   265 

   266 

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

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

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

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

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

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

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

   274   work.

   139 subsection {* Contributions *}

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

   142   We present the detailed lifting procedure, which was not shown before.

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

   143 

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

   144   The quotient package presented in this paper has the following

   282 

   145   advantages over existing packages:

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

   146   \begin{itemize}

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

   147 

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

   148   \item We define quotient composition, function map composition and

   286   for types and terms are as follows

   149     relation map composition. This lets lifting polymorphic types with

   287 

   150     subtypes quotiented as well. We extend the notions of

   288   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   151     respectfulness and preservation to cope with quotient

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

   152     composition.

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

   153 

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

   154   \item We allow lifting only some occurrences of quotiented

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

   155     types. Rsp/Prs extended. (used in nominal)

   293   \end{tabular}

   156 

   294   \end{isabelle}

   157   \item The quotient package is very modular. Definitions can be added

   295 

   158     separately, rsp and prs can be proved separately, Quotients and maps

   296   \noindent

   159     can be defined separately and theorems can

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

   160     be lifted on a need basis. (useful with type-classes).

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

   161 

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

   162   \item Can be used both manually (attribute, separate tactics,

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

   163     rsp/prs databases) and programatically (automated definition of

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

   164     lifted constants, the rsp proof obligations and theorem statement

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

   165     translation according to given quotients).

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

   166 

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

   167   \end{itemize}

   305 

   168 *}

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

   169 

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

   170 section {* Quotient Type*}

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

   171 

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

   172 

   310   underlying the first theorem.

   173 

   311 

   174 text {*

   312   Like Homeier, our work relies on map-functions defined for every type

   175   In this section we present the definitions of a quotient that follow

   313   constructor taking some arguments, for example @{text map} for lists. Homeier

   176   those by Homeier, the proofs can be found there.

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

   177 

   315   also the following map for function types

   178   \begin{definition}[Quotient]

   316 

   179   A relation $R$ with an abstraction function $Abs$

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

   180   and a representation function $Rep$ is a \emph{quotient}

   318 

   181   if and only if:

   319   \noindent

   182 

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

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

   322 

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

   324 

   325   \noindent

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

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

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

   329   of the type-constructor @{text \<kappa>}. In our implementation we maintain 

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

   331 

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

   333   which define equivalence relations in terms of constituent equivalence

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

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

   336   products as follows

   337   %

   338   @{text [display, indent=10] "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}

   339 

   340   \noindent

   341   Homeier gives also the following operator for defining equivalence 

   342   relations over function types

   343   %

   344   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   346   \hfill\numbered{relfun}

   347   \end{isabelle}

   348   

   349   \noindent

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

   351   needed later on.

   352 

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

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

   355   \end{definition}

   356 

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

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

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

   360   \end{definition}

   361 

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

   363   relations, abstraction and representation functions:

   364 

   365   \begin{definition}[Quotient Types]

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

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

   368   means

   191   \begin{definition}[Relation map and function map]\\

   376   \noindent

   192   @{thm fun_rel_def[of "R1" "R2", no_vars]}\\

   377   The value of this definition is that validity of @{text "Quotient R Abs Rep"} can 

   193   @{thm fun_map_def[no_vars]}

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

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

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

   381   types:

   382  

   383   \begin{proposition}\label{funquot}

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

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

   386   \end{proposition}

   387 

   388   \noindent

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

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

   391   package makes heavy 

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

   393   to deal with compositions of equivalence relations defined as follows:

   394 

   395   \begin{definition}[Composition of Relations]

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

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

   398   holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and

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

   196   The main theorems for building higher order quotients is:

   402   \noindent

   197   \begin{lemma}[Function Quotient]

   403   Unfortunately, there are two predicaments with compositions of relations.

   198   If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}

   404   First, a general quotient theorem, like the one given in Proposition \ref{funquot},

   199   then @{thm (concl) fun_quotient[no_vars]}

   405   cannot be stated inside HOL, because of the restriction on types.

   406   Second, even if we were able to state such a quotient theorem, it

   407   would not be true in general. However, we can prove specific instances of a

   408   quotient theorem for composing particular quotient relations.

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

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

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

   412 

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

   414 

   415   \vspace{-.5mm}

   416 *}

   417 

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

   419 

   420 text {*

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

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

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

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

   425   the quotient type declaration is therefore

   426 

   427   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   429   \end{isabelle}

   430 

   431   \noindent

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

   433   examples are

   434 

   435   

   436   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   437   \begin{tabular}{@ {}l}

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

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

   440   \end{tabular}

   441   \end{isabelle}

   442 

   443   \noindent

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

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

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

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

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

   449   \eqref{typedecl} the quotient types internally as

   450   

   451   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   453   \end{isabelle}

   454 

   455   \noindent

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

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

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

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

   460   abstraction and representation functions 

   461 

   462   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   464   \end{isabelle}

   465 

   466   \noindent 

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

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

   469   to work with the following derived abstraction and representation functions

   470 

   471   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   473   \end{isabelle}

   474   

   475   \noindent

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

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

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

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

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

   481   following property holds  for every quotient type 

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

   483 

   484   \begin{proposition}

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

   486   \end{proposition}

   487 

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

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

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

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

   492 

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

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

   495   \end{isabelle}

   496 

   497   \noindent

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

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

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

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

   502 

   503   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   504   \begin{tabular}{@ {}l}

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

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

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

   508   \end{tabular}

   509   \end{isabelle}

   510   

   511   \noindent

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

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

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

   515 

   516   The problem for us is that from such declarations we need to derive proper

   517   definitions using the @{text "Abs"} and @{text "Rep"} functions for the

   518   quotient types involved. The data we rely on is the given quotient type

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

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

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

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

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

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

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

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

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

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

   529   for @{text REP}.

   530   %

   531   \begin{center}

   532   \hfill

   533   \begin{tabular}{rcl}

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

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

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

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

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

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

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

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

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

   543   \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\

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

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

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

   547   \end{center}

   548   %

   549   \noindent

   550   In the last two clauses we have that the type @{text "\<alpha>s

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

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

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

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

   555   matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against

   556   @{text "\<sigma>s \<kappa>"}.  The

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

   558   type as follows:

   559   %

   560   \begin{center}

   561   \begin{tabular}{rcl}

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

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

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

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

   566   \end{tabular}

   567   \end{center}

   568   %

   569   \noindent

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

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

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

   573   @{text "MAP'"}.

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

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

   576   In this case @{text MAP} generates  the 

   577   aggregate map-function:

   578 

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

   580   

   581   \noindent

   582   which is essential in order to define the corresponding aggregate 

   583   abstraction and representation functions.

   584   

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

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

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

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

   589   the abstraction function

   590 

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

   592 

   593   \noindent

   594   In our implementation we further

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

   596   "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f \<circ> id =

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

   598 

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

   600 

   601   \noindent

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

   603 

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

   605 

   606   \noindent

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

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

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

   610   Consequently, all definitions in the quotient package 

   611   are of the general form

   612 

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

   614 

   615   \noindent

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

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

   618   generated from the declaration given by the user.

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

   620   that the terms involved are all typable.

   621 

   622   \begin{lemma}

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

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

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

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

   204 subsection {* Higher Order Logic *}

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

   207 

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

   208   Types:

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

   209   \begin{eqnarray}\nonumber

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

   210   @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber

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

   211       @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}

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

   212   \end{eqnarray}

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

   213 

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

   214   Terms:

   663   for raw lambda-terms as follows

   215   \begin{eqnarray}\nonumber

   664 

   216   @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber

   665   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   217       @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber

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

   218       @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber

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

   219       @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber

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

   220   \end{eqnarray}

   669   \end{isabelle}

   221 

   670 

   671   \noindent

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

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

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

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

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

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

   678   compositions. 

   679 

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

   681   the notion of \emph{aggregate equivalence relations} using the function @{text REL}:

   682 

   683   \begin{center}

   684   \hfill

   685   \begin{tabular}{rcl}

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

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

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

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

   690   \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\smallskip\\

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

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

   693   \end{center}

   694 

   695   \noindent

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

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

   698   @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are determined by matching 

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

   700 

   701   Lets return to the lifting procedure of theorems. Assume we have a theorem

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

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

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

   705   we generate the following proof obligation

   706 

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

   708 

   709   \noindent

   710   Homeier calls these proof obligations \emph{respectfulness

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

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

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

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

   715   And for every instantiation of the types, we might end up with a 

   716   corresponding respectfulness theorem.

   717 

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

   719   respectfulness proof obligations. And the point with @{text bn} is that the respectfulness theorem

   720   looks as follows

   721 

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

   723 

   724   \noindent

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

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

   727   using extensionally to obtain

   728 

   729   @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"}

   730  

   731   \noindent

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

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

   734 

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

   736 

   737   \noindent

   738   To do so, we have to establish

   739   

   740   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

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

   743   \end{isabelle}

   744 

   745   \noindent

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

   747 

   748   The second restriction we have to impose arises from

   749   non-lifted polymorphic constants, which are instantiated to a

   750   type being quotient. For example, take the @{term "cons"}-constructor to 

   751   add a pair of natural numbers to a list, whereby teh pair of natural numbers 

   752   is to become an integer in te quotient construction. The point is that we 

   753   still want to use @{text cons} for

   754   adding integers to lists---just with a different type. 

   755   To be able to lift such theorems, we need a \emph{preservation property} 

   756   for @{text cons}. Assuming we have a polymorphic raw constant 

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

   758   then a preservation property is as follows

   759 

   760   @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}

   761 

   762   \noindent

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

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

   765 

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

   767 

   768   \noindent

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

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

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

   772   then we need to show the corresponding preservation property.

   773 

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

   775 

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

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

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

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

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

   781   %quotients composed with the usual function composition.

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

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

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

   785   %This becomes especially interesting

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

   787   %intermediate step.

   788   %

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

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

   791   %theorem which allows quotienting inside the container:

   792   %

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

   794   %then

   795   % 

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

   797   %%%

   798   %%%\noindent

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

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

   801   %%%proceed in an unchanged way.

   224 section {* Constants *}

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

   225 

   226 (* Say more about containers? *)

   230   To define a constant on the lifted type, an aggregate abstraction

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

   231   function is applied to the raw constant. Below we describe the operation

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

   232   that generates

   810   three phases, called \emph{regularization},

   233   an aggregate @{term "Abs"} or @{term "Rep"} function given the

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

   234   compound raw type and the compound quotient type.

   812 

   235   This operation will also be used in translations of theorem statements

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

   236   and in the lifting procedure.

   814   in a ``raw'' theorem to quantifiers over variables that respect the relation

   237 

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

   238   The operation is additionally able to descend into types for which

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

   239   maps are known. Such maps for most common types (list, pair, sum,

   817   of the raw type so that they can be replaced by the ones that include the

   240   option, \ldots) are described in Homeier, and we assume that @{text "map"}

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

   241   is the function that returns a map for a given type. Then REP/ABS is defined

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

   242   as follows:

   820   package establishes the following three proof steps:

   243 

   821 

   244   \begin{itemize}

   822   \begin{center}

   245   \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}

   823   \begin{tabular}{r@ {\hspace{4mm}}l}

   246   \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}

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

   247   \item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}

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

   248   \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}

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

   249   \item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}

   827   \end{tabular}

   250   \item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}

   828   \end{center}

   251   \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}

   829 

   252   \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}

   830   \noindent

   253   \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}

   831   which means the raw theorem implies the quotient theorem.

   254   \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}

   832   In contrast to other quotient packages, our package requires

   255   \end{itemize}

   833   the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we

   256 

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

   257   Apart from the last 2 points the definition is same as the one implemented in

   835   from the form of @{text "raw_thm"}.} As a result, it is possible that a user can lift only some

   258   in Homeier's HOL package. Adding composition in last two cases is necessary

   836   occurrences of a raw type, but not others. 

   259   for compositional quotients. We ilustrate the different behaviour of the

   837 

   260   definition by showing the derived definition of @{term fconcat}:

   838   The second and third proof step will always succeed if the appropriate

   261 

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

   262   @{thm fconcat_def[no_vars]}

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

   263 

   841   imply a regularized version and a stronger one needs to be proved. This

   264   The aggregate @{term Abs} function takes a finite set of finite sets

   842   is outside of the scope where the quotient package can help. An example

   265   and applies @{term "map rep_fset"} composed with @{term rep_fset} to

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

   266   its input, obtaining a list of lists, passes the result to @{term concat}

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

   267   obtaining a list and applies @{term abs_fset} obtaining the composed

   845   but the raw theorem only shows that particular element in the

   268   finite set.

   846   equivalence classes are not equal. A more general statement stipulating that

   269 *}

   847   the equivalence classes are not equal is necessary, and then leads to the

   270 

   848   theorem  @{text "0 \<noteq> 1"}.

   271 subsection {* Respectfulness *}

   849 

   272 

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

   273 text {*

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

   274 

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

   275   A respectfulness lemma for a constant states that the equivalence

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

   276   class returned by this constant depends only on the equivalence

   854   which can all be performed independently from each other.

   277   classes of the arguments applied to the constant. To automatically

   855 

   278   lift a theorem that talks about a raw constant, to a theorem about

   856   We first define the function @{text REG}. The intuition

   279   the quotient type a respectfulness theorem is required.

   280 

   281   A respectfulness condition for a constant can be expressed in

   282   terms of an aggregate relation between the constant and itself,

   283   for example the respectfullness for @{term "append"}

   284   can be stated as:

   285 

   286   @{thm [display] append_rsp[no_vars]}

   287 

   288   \noindent

   289   Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to:

   290 

   291   @{thm [display] append_rsp_unfolded[no_vars]}

   292 

   293   An aggregate relation is defined in terms of relation composition,

   294   so we define it first:

   295 

   296   \begin{definition}[Composition of Relations]

   297   @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate

   298   composition @{thm pred_compI[no_vars]}

   299   \end{definition}

   300 

   301   The aggregate relation for an aggregate raw type and quotient type

   302   is defined as:

   303 

   304   \begin{itemize}

   305   \item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}

   306   \item @{text "REL(\<sigma>, \<sigma>)"}  =  @{text "op ="}

   307   \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}

   308   \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}

   309 

   310   \end{itemize}

   311 

   312   Again, the last case is novel, so lets look at the example of

   313   respectfullness for @{term concat}. The statement according to

   314   the definition above is:

   315 

   316   @{thm [display] concat_rsp[no_vars]}

   317 

   318   \noindent

   319   By unfolding the definition of relation composition and relation map

   320   we can see the equivalent statement just using the primitive list

   321   equivalence relation:

   322 

   323   @{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}

   324 

   325   The statement reads that, for any lists of lists @{term a} and @{term b}

   326   if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}

   327   such that each element of @{term a} is in the relation with an appropriate

   328   element of @{term a'}, @{term a'} is in relation with @{term b'} and each

   329   element of @{term b'} is in relation with the appropriate element of

   330   @{term b}.

   331 

   332 *}

   333 

   334 subsection {* Preservation *}

   335 

   336 text {*

   337   To be able to lift theorems that talk about constants that are not

   338   lifted but whose type changes when lifting is performed additionally

   339   preservation theorems are needed.

   340 

   341   To lift theorems that talk about insertion in lists of lifted types

   342   we need to know that for any quotient type with the abstraction and

   343   representation functions @{text "Abs"} and @{text Rep} we have:

   344 

   345   @{thm [display] (concl) cons_prs[no_vars]}

   346 

   347   This is not enough to lift theorems that talk about quotient compositions.

   348   For some constants (for example empty list) it is possible to show a

   349   general compositional theorem, but for @{term "op #"} it is necessary

   350   to show that it respects the particular quotient type:

   351 

   352   @{thm [display] insert_preserve2[no_vars]}

   353 *}

   354 

   355 subsection {* Composition of Quotient theorems *}

   356 

   357 text {*

   358   Given two quotients, one of which quotients a container, and the

   359   other quotients the type in the container, we can write the

   360   composition of those quotients. To compose two quotient theorems

   361   we compose the relations with relation composition as defined above

   362   and the abstraction and relation functions are the ones of the sub

   363   quotients composed with the usual function composition.

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

   365   with the definition of aggregate Abs/Rep functions and the

   366   relation is the same as the one given by aggregate relations.

   367   This becomes especially interesting

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

   369   intermediate step.

   370 

   371   Lets take again the example of @{term concat}. To be able to lift

   372   theorems that talk about it we provide the composition quotient

   373   theorems, which then lets us perform the lifting procedure in an

   374   unchanged way:

   375 

   376   @{thm [display] quotient_compose_list[no_vars]}

   377 *}

   378 

   379 

   380 section {* Lifting Theorems *}

   381 

   382 text {*

   383   The core of the quotient package takes an original theorem that

   384   talks about the raw types, and the statement of the theorem that

   385   it is supposed to produce. This is different from other existing

   386   quotient packages, where only the raw theorems were necessary.

   387   We notice that in some cases only some occurrences of the raw

   388   types need to be lifted. This is for example the case in the

   389   new Nominal package, where a raw datatype that talks about

   390   pairs of natural numbers or strings (being lists of characters)

   391   should not be changed to a quotient datatype with constructors

   392   taking integers or finite sets of characters. To simplify the

   393   use of the quotient package we additionally provide an automated

   394   statement translation mechanism that replaces occurrences of

   395   types that match given quotients by appropriate lifted types.

   396 

   397   Lifting the theorems is performed in three steps. In the following

   398   we call these steps \emph{regularization}, \emph{injection} and

   399   \emph{cleaning} following the names used in Homeier's HOL

   400   implementation.

   401 

   402   We first define the statement of the regularized theorem based

   403   on the original theorem and the goal theorem. Then we define

   404   the statement of the injected theorem, based on the regularized

   405   theorem and the goal. We then show the 3 proofs, as all three

   406   can be performed independently from each other.

   407 

   408 *}

   409 

   410 subsection {* Regularization and Injection statements *}

   411 

   412 text {*

   413 

   414   We first define the function @{text REG}, which takes the statements

   415   of the raw theorem and the lifted theorem (both as terms) and

   416   returns the statement of the regularized version. The intuition

   420   relations. It is defined as follows:

   860   equivalence relations. It is defined as follows:

   861 

   862   \begin{center}

   863   \begin{longtable}{rcl}

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

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

   866   $\begin{cases}

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

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

   869   \end{cases}$\smallskip\\

   870   \\

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

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

   873   $\begin{cases}

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

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

   876   \end{cases}$\smallskip\\

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

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

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

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

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

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

   883   @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\[-5mm]

   884   \end{longtable}

   885   \end{center}

   886   %

   887   \noindent

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

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

   890   for the universal quantifier. For the third and fourt clause, note that 

   891   @{text "\<forall>x. P"} is defined as @{text "\<forall> (\<lambda>x. P)"}.

   892 

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

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

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

   896 

   897   \begin{center}

   898   \begin{tabular}{rcl}

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

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

   901   $\begin{cases}

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

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

   904   \end{cases}$\\

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

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

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

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

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

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

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

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

   913   $\begin{cases}

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

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

   916   \end{cases}$\\

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

   918   $\begin{cases}

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

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

   921   \end{cases}$\\

   922   \end{tabular}

   923   \end{center}

   924 

   925   \noindent 

   926   where again the cases for existential quantifiers and unique existential

   927   quantifiers have been omitted.

   928 

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

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

   931   the implications into simpler implication subgoals. This succeeds for every

   932   monotone connective, except in places where the function @{text REG} inserted,

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

   934   rules of the form

   935 

   936   @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}

   937 

   938   \noindent

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

   940   bounded quantifier anywhere if R is an equivalence relation or

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

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

   943 

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

   945 

   946   \noindent

   947   And when @{term R\<^isub>2} is an equivalence relation and we can prove

   948 

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

   950 

   951   \noindent

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

   953   injection procedure would be used to prove such goals, and 

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

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

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

   957 

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

   959   The proof again follows the structure of the

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

   423   \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}

   963   \item For two constants an appropriate constant respectfulness lemma is applied.

   424   \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}

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

   425   \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}

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

   426   \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}

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

   427   \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}

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

   428   \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}

   968     can apply the theorem:

   429   \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}

   969 

   430   \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}

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

   431   \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}

   971 

   972     Otherwise we introduce an appropriate relation between the subterms

   973     and continue with two subgoals using the lemma:

   974 

   975     @{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}

   434   In the above definition we ommited the cases for existential quantifiers

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

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

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

   436   for the universal quantifier.

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

   437 

   981   definitions. Then for all lifted constants, their definitions

   438   Next we define the function @{text INJ} which takes the statement of

   982   are used to fold the @{term Rep} with the raw constant. Next for

   439   the regularized theorems and the statement of the lifted theorem both as

   983   all abstractions and quantifiers the lambda and

   440   terms and returns the statment of the injected theorem:

   984   quantifier preservation theorems are used to replace the

   441 

   985   variables that include raw types with respects by quantifiers

   442   \begin{itemize}

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

   443   \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}

   987   the lambda preservation theorem. Given

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

   988   @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:

   445   \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}

   989 

   446   \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}

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

   447   \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}

   991 

   448   \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}