(*<*)

theory Paper

imports "Quotient"

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

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

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

begin

notation (latex output)

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

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

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

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

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

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

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

  empty_fset ("\<emptyset>") and

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

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

  Cons ("_::_") and

  concat ("flat") and

  concat_fset ("\<Union>") and

  Quotient ("Quot _ _ _")

declare [[show_question_marks = false]]

ML {*

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

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

  let

    val concl =

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

  in

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

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

  end);

*}

setup {*

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

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

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

*}

(*>*)

section {* Introduction *}

text {*

  \noindent

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

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

  \end{isabelle}

  \noindent

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

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

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

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

  terms of operations on pairs of natural numbers:

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

  @{text "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2, m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}

  \end{isabelle}

  \noindent

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

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

  \end{isabelle}

  \noindent

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

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

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

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

  \end{isabelle}

  \noindent

  {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?}

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

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

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

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

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

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

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

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

  Nominal Isabelle, then manual reasoning is not an option.

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

  and automate the reasoning as much as possible. In the

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

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

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

  quotient packages perform can be illustrated by the following picture:

%%% FIXME: Referee 1 says:

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

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

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

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

%%% I wouldn't change it.

  \begin{center}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  \end{tikzpicture}

  \end{center}

  \noindent

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

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

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

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

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

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

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

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

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

  and can be uniquely

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

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

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

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

  \end{isabelle}

  \noindent

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

  typing information is important.

  Every abstraction and representation function stands for an isomorphism

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

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

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

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

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

  \end{isabelle}

  \noindent

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

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

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

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

  \hfill\numbered{adddef}

  \end{isabelle}

  \noindent

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

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

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

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

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

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

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

  flattens lists of lists, defined as follows

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

  \begin{tabular}{@ {}l}

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

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

  \end{tabular}

  \end{isabelle}

  \noindent

  where @{text "@"} is the usual

  list append. We expect that the corresponding

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

  builds finite unions of finite sets:

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

  \begin{tabular}{@ {}l}

  @{thm concat_empty_fset[THEN eq_reflection]}\\

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

  \end{tabular}

  \end{isabelle}

  \noindent

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

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

  that the method  used in the existing quotient

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

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

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

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

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

  \end{isabelle}

  \noindent

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

  existing quotient packages by introducing an intermediate step and reasoning

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

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

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

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

  generate the %%%following

  definition

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

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

  \end{isabelle}

  \noindent

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

  will present a formal definition of our aggregate abstraction and

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

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

  according to the type of the raw constant and the type

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

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

  from Homeier \cite{Homeier05}.

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

  In addition we are able to clearly specify what is involved

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

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

  is that our procedure for lifting theorems is completely deterministic

  following the structure of the theorem being lifted and the theorem

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

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

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

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

  lifting procedure. Appendix A gives an example how our quotient

  package works in practise.

*}

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

text {*

  \noindent

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

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

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

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

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

  for types and terms are

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

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

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

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

  \end{tabular}

  \end{isabelle}

  \noindent

  with types being either type variables or type constructors and terms

  being variables, constants, applications or abstractions.

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

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

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

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

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

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

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

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

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

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

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

  procedures showing that one theorem implies another by decomposing the term

  underlying the first theorem.

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

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

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

  also the following map for function types

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

  @{thm map_fun_def[THEN eq_reflection]}

  \end{isabelle}

  \noindent

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

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

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

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

  \end{isabelle}

  \noindent

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

  we can get back to \eqref{adddef}.

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

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

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

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

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

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

  %For example @{text "map_list"}

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

  In our implementation we maintain

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

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

  which define equivalence relations in terms of constituent equivalence

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

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

  products as %% follows

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

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

  \end{isabelle}

  \noindent

  Homeier gives also the following operator for defining equivalence

  relations over function types

  %

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

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

  \hfill\numbered{relfun}

  \end{isabelle}

  \noindent

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

  are needed later on.

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

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

  \end{definition}

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

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

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

  \end{definition}

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

  relations, abstraction and representation functions:

  \begin{definition}[Quotient Types]

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

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

  holds if and only if

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

  \begin{tabular}{rl}

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

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

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

  \end{tabular}

  \end{isabelle}

  \end{definition}

  \noindent

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

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

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

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

  types:

  \begin{proposition}\label{funquot}

  \begin{isa}

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

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

  \end{isa}

  \end{proposition}

  \noindent

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

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

  package makes heavy

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

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

  symmetric by definition.} defined as follows:

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

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

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

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

  composition defined by

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

  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

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

  \end{definition}

  \noindent

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

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

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

  However, we can prove specific instances of a

  quotient theorem for composing particular quotient relations.

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

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

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

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

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

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

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

  \end{tabular}

  \end{isabelle}

*}

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

text {*

  \noindent

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

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

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

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

  the quotient type declaration is therefore

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

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

  \end{isabelle}

  \noindent

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

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

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

  examples are

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

  \begin{tabular}{@ {}l}

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

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

  \end{tabular}

  \end{isabelle}

  \noindent

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

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

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

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

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

  \eqref{typedecl} the quotient types internally as

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

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

  \end{isabelle}

  \noindent

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

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

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

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

  abstraction and representation functions

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

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

  \end{isabelle}

  \noindent

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

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

  to work with the following derived abstraction and representation functions