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

    52   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

    59   understood how to use both mechanisms for dealing with quotient

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

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

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

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

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

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

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

    68   "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 

    69   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 

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

    71   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 +

    72   "add\<^bsub>nat\<times>nat\<^esub> (x\<^isub>1, y\<^isub>1) (x\<^isub>2,

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

    73   y\<^isub>2) \<equiv> (x\<^isub>1 + x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}).

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

    74   Similarly one can construct the type of finite sets by quotienting lists

    75   relation

    75   according to the equivalence relation

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

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

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

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

    84 

    84 

    85   Another important area of quotients is reasoning about programming language

    85   An area where quotients are ubiquitous is reasoning about programming language

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

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

    87 

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

    89 

    90   \noindent

    91   The problem with this definition arises when one, for example, attempts to

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

    93   ove the structure of terms. This can be fiendishly complicated (see

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

    95   about ``raw'' lambda-terms). In contrast, if we reason about

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

    97   $\alpha$-equivalence, then the reasoning infrastructure provided by, 

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

    99   proof of the substitution lemma almost trivial.

   100 

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

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

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

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

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

   106   usually requires a \emph{lot} of tedious reasoning effort.  The purpose of a

   107   \emph{quotient package} is to ease the lifting and automate the reasoning as

   108   much as possible. 

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

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

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

   113   

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

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

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

   117   

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

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

   120 

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

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

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

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

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

   126   

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

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

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

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

   131 

   132   \end{tikzpicture}

    92   \noindent

   135 

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

    94   example, proving formally the substitution lemma ...

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

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

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

    98   almost trivial. 

    99 

   100 

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

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

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

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

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

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

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

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

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

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

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

   112   again.

   113 

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

   115   Nominal Isabelle where representations of alpha-equated terms are

   116   constructed according to specifications given by the user.

   117 

   118   

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

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

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

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

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

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