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

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

    14 and

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

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

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

    16 and

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

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

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

    18 and

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

    19   fun_map (infix "\<longrightarrow>" 51)

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

    20 and

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

    21   fun_rel (infix "\<Longrightarrow>" 51)

    21   Cons ("_::_") 

    22 and

    22   

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

    53   Isabelle is a generic theorem prover in which many logics can be implemented. 

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

    54   The most widely used one, however, is

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

    55   Higher-Order Logic (HOL). This logic consists of a small number of 

    54   (HOL). This logic consists of a small number of axioms and inference rules

    56   axioms and inference

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

    57   rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted 

    56   very restricted mechanisms for extending the logic: one is the definition of

    58   mechanisms for extending the logic: one is the definition of new constants

    57   new constants in terms of existing ones; the other is the introduction of

    59   in terms of existing ones; the other is the introduction of new types

    58   new types by identifying non-empty subsets in existing types. It is well

    60   by identifying non-empty subsets in existing types. It is well understood 

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

    61   to use both mechanisms for dealing with quotient constructions in HOL (see for example 

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

    62   \cite{Paulson06}).

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

    63   For example the integers in Isabelle/HOL are constructed by a quotient construction over 

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

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

    63 

    65 

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

    66 % I would avoid substraction for natural numbers.

    65 

    67 

    66   \noindent

    68   @{text [display] "(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"}

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

    69 

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

    70   \noindent

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

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

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

    72   according to the equivalence relation

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

    73 

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

    74   @{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}

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

    75 

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

    76   \noindent

    75   relation

    77   where @{text "\<in>"} stands for membership in a list.

    76 

    78 

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

    79   The problem is that in order to start reasoning about, for example integers, 

    78 

    80   definitions and theorems need to be transferred, or \emph{lifted}, 

    79   \noindent

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

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

    82   This lifting usually requires a lot of tedious reasoning effort.

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

    83   The purpose of a \emph{quotient package} is to ease the lifting and automate

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

    84   the reasoning involved as much as possible. Such a package is a central

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

    85   component of the new version of Nominal Isabelle where representations 

    84 

    86   of alpha-equated terms are constructed according to specifications given by

    85   Another important area of quotients is reasoning about programming language

    87   the user. 

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

    87 

    88   \begin{center}

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

    90   \end{center}

    91 

    92   \noindent

    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