(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)

(*<*)

theory Paper

imports "Quotient"

        "LaTeXsugar"

        "../Nominal/FSet"

begin

notation (latex output)

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

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

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

  fun_map ("_ \<^raw:\mbox{\tt{---\textgreater}}> _" 51) and

  fun_rel ("_ \<^raw:\mbox{\tt{===\textgreater}}> _" 51) and

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

  fempty ("\<emptyset>") and

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

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

  Cons ("_::_") and

  concat ("flat") and

  fconcat ("\<Union>")

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 (ProofContext.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 {* 

   \begin{flushright}

  {\em ``Not using a [quotient] package has its advantages: we do not have to\\ 

    collect all the theorems we shall ever want into one giant list;''}\\

    Larry Paulson \cite{Paulson06}

  \end{flushright}\smallskip

  \noindent

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

  implemented. The most widely used one, however, is Higher-Order Logic

  (HOL). This logic 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. It is well

  understood 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

  \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 (namely @{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)"}).

  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

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

  \noindent

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

  also member in the other. 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.

  An area where quotients are ubiquitous is reasoning about programming language

  calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as

  @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}

  \noindent

  The problem with this definition arises when one attempts to

  prove formally, for example, 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 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}.  

  It is feasible to to 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 definitions and 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 is the one by Homeier

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

  quotient packages perform can be illustrated by the following picture:

  \begin{center}

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

  %%\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 over which an equivalence relation

  given by the user is defined. With this input the package introduces a new

  type that comes with associated \emph{abstraction} and \emph{representation}

  functions, written @{text Abs} and @{text Rep}. These functions relate

  elements in the existing type to ones in the new type and vice versa; they

  can be uniquely identified by their 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

  However we often leave this typing information implicit for better

  readability. Every abstraction and representation function represents 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 (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (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

  @{text [display, indent=10] "add n m \<equiv> Abs (add_pair (Rep n) (Rep m))"}

  \noindent

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

  add them according to @{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

  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 and the operator that flattens lists of lists, defined 

  as follows

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

  \noindent

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

  behaves as follows:

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

  \noindent

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

  terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having

  the type @{text "\<alpha> fset \<Rightarrow> \<alpha> list"} and @{text "\<alpha> list \<Rightarrow> \<alpha> fset"},

  respectively). The problem is that the method is used in the existing quotient

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

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

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

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

  \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 faltening 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

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

  \noindent

  where @{term map} 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{respectfulness} and \emph{preservation} from Homeier 

  \cite{Homeier05}.

  We will also address the criticism by Paulson \cite{Paulson06} cited at the

  beginning of this section about having to collect theorems that are lifted from the raw

  level to the quotient level. Our quotient package is modular so that it

  allows to lift single theorems separately. This has the advantage for the

  user to develop a formal theory interactively an a natural progression. A

  pleasing result of the modularity is also that we are able to clearly

  specify what needs to be done in the lifting process (this was only hinted at in

  \cite{Homeier05} and implemented as a ``rough recipe'' in ML-code).

  The paper is organised as follows \ldots

*}

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

text {*

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

  those by Homeier, the proofs can be found there.

  \begin{definition}[Quotient]

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

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

  if and only if:

  \begin{enumerate}

  \item @{thm (rhs1) Quotient_def[of "R", no_vars]}

  \item @{thm (rhs2) Quotient_def[of "R", no_vars]}

  \item @{thm (rhs3) Quotient_def[of "R", no_vars]}

  \end{enumerate}

  \end{definition}

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

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

  @{thm fun_map_def[no_vars]}

  \end{definition}

  The main theorems for building higher order quotients is:

  \begin{lemma}[Function Quotient]

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

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

  \end{lemma}

*}

subsection {* Higher Order Logic *}

text {*

  Types:

  \begin{eqnarray}\nonumber

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

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

  \end{eqnarray}

  Terms:

  \begin{eqnarray}\nonumber

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

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

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

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

  \end{eqnarray}

*}

section {* Lifting of Definitions *}

(* Say more about containers? *)

text {*

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

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

  that generates

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

  compound raw type and the compound quotient type.

  This operation will also be used in translations of theorem statements

  and in the lifting procedure.

  The operation is additionally able to descend into types for which

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

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

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

  as follows:

  \begin{itemize}

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

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

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

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

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

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

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

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

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

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

  \end{itemize}

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

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

  for compositional quotients. We ilustrate the different behaviour of the

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

  @{thm fconcat_def[no_vars]}

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

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

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

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

  finite set.

*}

subsection {* Respectfulness *}

text {*

  A respectfulness lemma for a constant states that the equivalence

  class returned by this constant depends only on the equivalence

  classes of the arguments applied to the constant. To automatically

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

  the quotient type a respectfulness theorem is required.

  A respectfulness condition for a constant can be expressed in

  terms of an aggregate relation between the constant and itself,

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

  can be stated as:

  @{thm [display] append_rsp[no_vars]}

  \noindent

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

  @{thm [display] append_rsp_unfolded[no_vars]}

  An aggregate relation is defined in terms of relation composition,

  so we define it first:

  \begin{definition}[Composition of Relations]

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

  composition @{thm pred_compI[no_vars]}

  \end{definition}

  The aggregate relation for an aggregate raw type and quotient type

  is defined as:

  \begin{itemize}

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

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

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

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

  \end{itemize}

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

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

  the definition above is:

  @{thm [display] concat_rsp[no_vars]}

  \noindent

  By unfolding the definition of relation composition and relation map