diff -r 973649d612f8 -r c474186439bd Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Fri Jun 11 17:52:06 2010 +0200 +++ b/Quotient-Paper/Paper.thy Fri Jun 11 21:58:25 2010 +0200 @@ -14,12 +14,12 @@ fun_map (infix "\" 51) and fun_rel (infix "\" 51) and list_eq (infix "\" 50) and (* Not sure if we want this notation...? *) - fempty ("\\<^isub>f") and - funion ("_ \\<^isub>f _") and - finsert ("{_} \\<^isub>f _") and + fempty ("\") and + funion ("_ \ _") and + finsert ("{_} \ _") and Cons ("_::_") and concat ("flat") and - fconcat ("fset'_flat") + fconcat ("\") @@ -58,7 +58,7 @@ 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 many quotient + 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 \ nat"} and the equivalence relation @@ -74,7 +74,7 @@ "add\<^bsub>nat\nat\<^esub> (n\<^isub>1, m\<^isub>1) (n\<^isub>2, m\<^isub>2) \ (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}). Similarly one can construct the type of finite sets, written @{term "\ fset"}, - by quotienting @{text "\ list"} according to the equivalence relation + by quotienting the type @{text "\ list"} according to the equivalence relation @{text [display, indent=10] "xs \ ys \ (\x. x \ xs \ x \ ys)"} @@ -82,7 +82,7 @@ which states that two lists are equivalent if every element in one list is also member in the other (@{text "\"} stands here for membership in lists). The empty finite set, written @{term "{||}"}, can then be defined as the - empty list and the union of two finite sets, written @{text "\\<^isub>f"}, as list append. + empty list and the union of two finite sets, written @{text "\"}, 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 @@ -96,8 +96,8 @@ \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 by, - for example, Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal + $\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 @@ -106,16 +106,16 @@ from the ``raw'' type @{typ "nat \ 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, but if they have to be done over and over again as in + 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 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 is the one by Homeier \cite{Homeier05} implemented in HOL4. - The fundamental construction these quotient packages perform can be - illustrated by the following picture: + 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} @@ -143,15 +143,15 @@ \end{center} \noindent - The starting point is an existing type over which a user-given equivalence - relation is defined. With this input, the package introduces a new type, - which comes with two associated abstraction and representation functions, written - @{text Abs} and @{text Rep}. They relate elements in the existing and new - type and can be uniquely identified by their type (which however we omit for - better readability). These two function represent an isomorphism between - the non-empty subset and the new type. They are necessary making definitions - over the new type. For example @{text "0"} and @{text "1"} - of type @{typ int} can be defined as + 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, which comes with two associated abstraction and representation + functions, written @{text Abs} and @{text Rep}. These functions relate + elements in the existing and new type, and can be uniquely identified by + their type (which however we often omit for better readability). They + represent 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 \ Abs (0, 0)"}\hspace{10mm}@{text "1 \ Abs (1, 0)"} @@ -168,11 +168,10 @@ add them according to @{text "add\<^bsub>nat\nat\<^esub>"} 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 more complicated definitions involving + 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 finite sets. There one would like to have a corresponding definition - for finite sets for the operator @{term "concat"} defined over lists. This - operator flattens lists of lists as follows + in case of finite sets. For example over lists one can define an operator + that flattens lists of lists as follows @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]} @@ -183,20 +182,25 @@ @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]} \noindent - The problem is that we want to quotient lists to obtain finite sets and - @{term concat} is of type @{text "(\ list) list \ \ list"}. We expect - that @{term "fconcat"} has type @{text "(\ fset) fset \ \ fset"}. But - what should its definition be? It is not possible to just take the representation - of the argument and then take the abstraction of the result of flattening - the resulting list. The problem is that a single @{text "Rep"} only gives - us lists of finite sets, not lists of lists. It turns out that we need - to be able to build aggregate representation and abstraction function, which in + The quotient package should provide us with a definition for @{text "\"} in + terms of @{text flat}, @{text Rep} and @{text Abs}. The problem is that it + is not enough to just take the representation of the argument and then + take the abstraction of the result, because in that case we obtain an operator + with type @{text "(\ list) fset \ \ fset"}, not the expected + @{text "(\ fset) fset \ \ fset"}. It turns out that we need + to build aggregate representation and abstraction functions, which in case of @{term "fconcat"} produce the following definition - @{text [display, indent=10] "fset_flat S \ Abs (concat ((map Rep \ Rep) S))"} + @{text [display, indent=10] "\ S \ Abs (concat ((map Rep \ Rep) S))"} \noindent - where @{term map} is the usual mapping function for lists. + where @{term map} is the usual mapping function for lists. In this paper we + will present a formal definition for our aggregate abstraction and + representation functions (this definition was omitted in \cite{Homeier05}). + They generate definitions like the one above for @{text add} and @{text "\"} + according to the type of the ``raw'' constant and the type + of the quotient constant. + *}