(*<*)

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))

*}

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

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

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

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

fun

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

where

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

(*>*)

section {* Introduction *}

text {*

  \noindent

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

  context of theorem provers a number questions concerning them are

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

  establish a convenient reasoning infrastructure for quotient

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

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

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

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

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

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

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

  for dealing with quotient constructions in HOL (see

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

  Isabelle/HOL are constructed by a quotient construction over the

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

  \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}\ \ \ \ \ %%%

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

  \hfill\numbered{addpair}

  \end{isabelle}

  \noindent

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

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

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

  \hfill\numbered{minuspair}

  \end{isabelle}

  \noindent

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

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

  equivalence relation

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

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

  \end{isabelle}

  \noindent

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

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

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

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

  append.

  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

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

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

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

  \end{isabelle}

  \noindent

  The problem with this definition arises from the need to reason

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

  prove formally the substitution lemma \cite{Barendregt81} by

  induction over the structure of terms. This can be fiendishly

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

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

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

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

  infrastructure provided, for example, by Nominal Isabelle

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

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

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

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

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

  example the rational numbers

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

  \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{ratpairequiv}

  \end{isabelle}

  \noindent

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

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

  finite sets, etc.~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, $\alpha$-equated lambda-terms and

  rational numbers). This lifting usually requires a reasoning effort

  that can be rather repetitive and involves explicit conversions 

  between the quotient and raw level in form of abstraction and 

  representation functions \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. Before we

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

  quotient package when defining integers. We assume the definitions

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

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

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

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

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

  \eqref{natpairequiv}).

*}

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

txt {*

  \noindent

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

  indeed an equivalence relation, whereby an equivalence 

  relation is defined as one that is reflexive, symmetric and

  transitive.  This proof obligation can thus be discharged by

  unfolding the definitions and using the standard automatic proving

  tactic in Isabelle/HOL.

*}

    unfolding equivp_reflp_symp_transp

    unfolding reflp_def symp_def transp_def

    by auto

(*<*)

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

    begin

(*>*)

text {*

  \noindent

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

  quotient type @{text int}.

*}

    quotient_definition

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

    quotient_definition

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

text {*

  \noindent

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

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

  (written @{text "uminus"}).

*}

    quotient_definition

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

      by auto

    quotient_definition

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

      by auto

(*<*)    

    instance ..

    end

(*>*)

text {*

  \noindent

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

  operations allowing the user to write

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

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

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

  proof-obligation which ensures that the operations a

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

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

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

  the automatic proving tactic in Isabelle/HOL.

  Besides helping with declarations of quotient types and definitions 

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

  proving properties about quotient types. For example we might be

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

  can be stated as follows:

*}

     lemma zero_add:

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

     proof(descending)

txt {*

  \noindent 

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

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

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

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

  we obtain the subgoal

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

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

  \end{isabelle}

  \noindent

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

*}

     qed(auto)

text {*

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

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

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

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

  induction proceeds over two natural numbers. 

*}

    lemma nat_induct2:

      assumes "P 0 0"

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

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

      shows   "P n m"

      using assms

      by (induction_schema) (pat_completeness, lexicographic_order)

text {*

  \noindent

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

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

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

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

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

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

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

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

*}

    lemma int_induct:

      assumes "P 0"

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

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

      shows   "P (j::int)"

      using assms 

      proof (descending)

txt {*

  \noindent

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

  obligation on the raw level.

  @{subgoals[display]}

  \noindent

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

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

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

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

*}

       qed (auto intro: nat_induct2)

text {*

  This completes the proof of the induction principle

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

  detailed reasoning steps involved which would confirm that

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

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

  to a corresponding property one on the raw level.

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

%%%TODO Update the contents.

  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"}\\