# HG changeset patch # User Christian Urban # Date 1277329276 -3600 # Node ID 9a560e489c648e7231d746d3dbb04b6a7ec0ee9c # Parent f170ee51eed2f6a7273f7f21aa375287b0f8a5a5 polished paper again (and took out some claims about Homeier's package) diff -r f170ee51eed2 -r 9a560e489c64 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Wed Jun 23 15:59:43 2010 +0100 +++ b/Quotient-Paper/Paper.thy Wed Jun 23 22:41:16 2010 +0100 @@ -255,9 +255,9 @@ In addition we are able to 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 into one giant list. Our - quotient package is the first one that is modular so that it allows to lift - single higher-order theorems separately. This has the advantage for the user of being able to develop a + lifted from the raw level to the quotient level into one giant list. Homeier's and + also our quotient package are modular so that they allow lifting + theorems separately. This has the advantage for the user of being able to develop a formal theory interactively as a natural progression. A pleasing side-result of the modularity is that we are able to clearly specify what is involved in the lifting process (this was only hinted at in \cite{Homeier05} and @@ -299,9 +299,9 @@ respectively. The type of a term is often made explicit by writing @{text "t :: \"}. HOL includes a type @{typ bool} for booleans and the function type, written @{text "\ \ \"}. HOL also contains many primitive and defined - constants; a primitive constant is equality, with type @{text "= :: \ \ \ \ + constants; for example, a primitive constant is equality, with type @{text "= :: \ \ \ \ bool"}, and the identity function with type @{text "id :: \ \ \"} is - defined as @{text "\x\<^sup>\. x\<^sup>\"}). + defined as @{text "\x\<^sup>\. x\<^sup>\"}. An important point to note is that theorems in HOL can be seen as a subset of terms that are constructed specially (namely through axioms and proof @@ -318,7 +318,7 @@ \noindent Using this map-function, we can give the following, equivalent, but more - uniform, definition for @{text add} shown in \eqref{adddef}: + uniform definition for @{text add} shown in \eqref{adddef}: @{text [display, indent=10] "add \ (Rep_int \ Rep_int \ Abs_int) add_pair"} @@ -374,7 +374,7 @@ \end{definition} \noindent - The value of this definition is that validity of @{text "Quotient R Abs Rep"} can + The value of this definition lies in the fact that validity of @{text "Quotient R Abs Rep"} can often be proved in terms of the validity of @{text "Quotient"} over the constituent types of @{text "R"}, @{text Abs} and @{text Rep}. For example Homeier proves the following property for higher-order quotient @@ -403,7 +403,7 @@ \noindent Unfortunately, there are two predicaments with compositions of relations. First, a general quotient theorem, like the one given in Proposition \ref{funquot}, - cannot be stated inside HOL, because of the restriction on types. + cannot be stated inside HOL, because of restrictions on types. Second, even if we were able to state such a quotient theorem, it would not be true in general. However, we can prove specific instances of a quotient theorem for composing particular quotient relations. @@ -515,18 +515,17 @@ @{text "(\ list) list \ \ list"}). The problem for us is that from such declarations we need to derive proper - definitions using the @{text "Abs"} and @{text "Rep"} functions for the - quotient types involved. The data we rely on is the given quotient type + definitions using @{text "Abs"} and @{text "Rep"}. The data we rely on is the given quotient type @{text "\"} and the raw type @{text "\"}. They allow us to define \emph{aggregate abstraction} and \emph{representation functions} using the functions @{text "ABS (\, - \)"} and @{text "REP (\, \)"} whose clauses we give below. The idea behind + \)"} and @{text "REP (\, \)"} whose clauses we shall give below. The idea behind these two functions is to simultaneously descend into the raw types @{text \} and quotient types @{text \}, and generate the appropriate @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore we generate just the identity whenever the types are equal. On the ``way'' down, however we might have to use map-functions to let @{text Abs} and @{text Rep} act over the appropriate types. In what follows we use the short-hand notation - @{text "ABS (\s, \s)"} to mean @{text "ABS (\\<^isub>1, \\<^isub>1)\ABS (\\<^isub>i, \\<^isub>i)"}; similarly + @{text "ABS (\s, \s)"} to mean @{text "ABS (\\<^isub>1, \\<^isub>1)\ABS (\\<^isub>n, \\<^isub>n)"}; similarly for @{text REP}. % \begin{center} @@ -657,7 +656,7 @@ The main point of the quotient package is to automatically ``lift'' theorems involving constants over the raw type to theorems involving constants over the quotient type. Before we can describe this lifting process, we need to impose - two restrictions in the form of proof obligations that arise during the + two restrictions in form of proof obligations that arise during the lifting. The reason is that even if definitions for all raw constants can be given, \emph{not} all theorems can be lifted to the quotient type. Most notable is the bound variable function, that is the constant @{text bn}, defined @@ -699,7 +698,7 @@ @{text "\s \"}. The @{text "\s'"} are determined by matching @{text "\s \"} and @{text "\s \"}. - Lets return to the lifting procedure of theorems. Assume we have a theorem + Let us return to the lifting procedure of theorems. Assume we have a theorem that contains the raw constant @{text "c\<^isub>r :: \"} and which we want to lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding constant @{text "c\<^isub>q :: \"} defined over a quotient type. In this situation @@ -717,15 +716,15 @@ corresponding respectfulness theorem. Before lifting a theorem, we require the user to discharge - respectfulness proof obligations. And the point with @{text bn} is that the respectfulness theorem - looks as follows + respectfulness proof obligations. In case of @{text bn} + this obligation is as follows @{text [display, indent=10] "(\\<^isub>\ \ =) bn bn"} \noindent - and the user cannot discharge it: because it is not true. To see this, + and the point is that the user cannot discharge it: because it is not true. To see this, we can just unfold the definition of @{text "\"} \eqref{relfun} - using extensionally to obtain + using extensionally to obtain the false statement @{text [display, indent=10] "\t\<^isub>1 t\<^isub>2. if t\<^isub>1 \\<^isub>\ t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"} @@ -749,8 +748,8 @@ The second restriction we have to impose arises from non-lifted polymorphic constants, which are instantiated to a type being quotient. For example, take the @{term "cons"}-constructor to - add a pair of natural numbers to a list, whereby teh pair of natural numbers - is to become an integer in te quotient construction. The point is that we + add a pair of natural numbers to a list, whereby the pair of natural numbers + turns into an integer in the quotient construction. The point is that we still want to use @{text cons} for adding integers to lists---just with a different type. To be able to lift such theorems, we need a \emph{preservation property} @@ -815,7 +814,7 @@ in a ``raw'' theorem to quantifiers over variables that respect the relation (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep} and @{term Abs} of appropriate types in front of constants and variables - of the raw type so that they can be replaced by the ones that include the + of the raw type so that they can be replaced by the corresponding constants from the quotient type. The purpose of cleaning is to bring the theorem derived in the first two phases into the form the user has specified. Abstractly, our package establishes the following three proof steps: @@ -932,7 +931,7 @@ In the first proof step, establishing @{text "raw_thm \ reg_thm"}, we always start with an implication. Isabelle provides \emph{mono} rules that can split up the implications into simpler implicational subgoals. This succeeds for every - monotone connective, except in places where the function @{text REG} inserted, + monotone connective, except in places where the function @{text REG} replaced, for instance, a quantifier by a bounded quantifier. In this case we have rules of the form @@ -947,27 +946,27 @@ @{text [display, indent=10] "\x \ Respects R. P x = \x. P x"} \noindent - And when @{term R\<^isub>2} is an equivalence relation and we can prove + If @{term R\<^isub>2} is an equivalence relation, we can prove @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]} \noindent The last theorem is new in comparison with Homeier's package. There the - injection procedure would be used to prove such goals, and + injection procedure would be used to prove such goals and the assumption about the equivalence relation would be used. We use the above theorem directly, because this allows us to completely separate the first and the second proof step into two independent ``units''. The second proof step, establishing @{text "reg_thm \ inj_thm"}, starts with an equality. The proof again follows the structure of the - two underlying terms, and is defined for a goal being a relation between these two terms. + two underlying terms and is defined for a goal being a relation between these two terms. \begin{itemize} - \item For two constants an appropriate constant respectfulness lemma is applied. + \item For two constants an appropriate respectfulness theorem is applied. \item For two variables, we use the assumptions proved in the regularization step. \item For two abstractions, we @{text "\"}-expand and @{text "\"}-reduce them. \item For two applications, we check that the right-hand side is an application of - @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"}. If yes then we + @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we can apply the theorem: @{term [display, indent=10] "R x y \ R x (Rep (Abs y))"} @@ -994,7 +993,7 @@ \noindent Next, relations over lifted types are folded to equalities. - For this the following theorem has been shown in Homeier~\cite{Homeier05}: + For this the following theorem has been shown by Homeier~\cite{Homeier05}: @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]} @@ -1009,15 +1008,12 @@ text {* - In this section we will show, a complete interaction with the quotient package - for defining the type of integers by quotienting pairs of natural numbers and - lifting theorems to integers. Our quotient package is fully compatible with - Isabelle type classes, but for clarity we will not use them in this example. - In a larger formalization of integers using the type class mechanism would - provide many algebraic properties ``for free''. + In this section we will show a sequence of declarations for defining the + type of integers by quotienting pairs of natural numbers, and + lifting one theorem. A user of our quotient package first needs to define a relation on - the raw type, by which the quotienting will be performed. We give + the raw type with which the quotienting will be performed. We give the same integer relation as the one presented in \eqref{natpairequiv}: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % @@ -1028,9 +1024,9 @@ \end{isabelle} \noindent - Next the quotient type is defined. This generates a proof obligation that the + Next the quotient type must be defined. This generates a proof obligation that the relation is an equivalence relation, which is solved automatically using the - definition and extensionality: + definition of equivalence and extensionality: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % \begin{tabular}{@ {}l} @@ -1060,7 +1056,7 @@ \end{isabelle} \noindent - If the user attempts to lift this theorem, all proof obligations are + If the user lifts this theorem, all proof obligations are automatically discharged, except the respectfulness proof for @{text "add_pair"}: @@ -1072,16 +1068,17 @@ \end{isabelle} \noindent - This can be discharged automatically by Isabelle when telling it to unfold the definition + This property needs to beproved by the user. It + can be discharged automatically by Isabelle when hinting to unfold the definition of @{text "\"}. - After this, the user can prove the lifted lemma explicitly: + After this, the user can prove the lifted lemma as follows: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"} \end{isabelle} \noindent - or by the completely automated mode by stating: + or by using the completely automated stating just: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"} @@ -1130,22 +1127,17 @@ Paulson showed a construction of quotients that does not require the Hilbert Choice operator, but also only first-order theorems can be lifted~\cite{Paulson06}. The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}. - He introduced most of the abstract notions about quotients and also deals with the + He introduced most of the abstract notions about quotients and also deals with lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed for lifting theorems about @{text flat}). Also, a number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc only exist in \cite{Homeier05} as ML-code, not included in the paper. - One advantage of our package is that it is modular---in the sense that every step - in the quotient construction can be done independently (see the criticism of Paulson - about other quotient packages). This modularity is essential in the context of - Isabelle, which supports type-classes and locales. - - Another feature of our quotient package is that when lifting theorems, teh user can + One feature of our quotient package is that when lifting theorems, the user can precisely specify what the lifted theorem should look like. This feature is necessary, for example, when lifting an induction principle for two lists. - This principle has as the conclusion a predicate of the form @{text "P xs ys"}, - and we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"}, + Assuming this principle has as the conclusion a predicate of the form @{text "P xs ys"}, + then we can precisely specify whether we want to quotient @{text "xs"} or @{text "ys"}, or both. We found this feature very useful in the new version of Nominal Isabelle, where such a choice is required to generate a resoning infrastructure for alpha-equated terms. diff -r f170ee51eed2 -r 9a560e489c64 Quotient-Paper/document/root.tex --- a/Quotient-Paper/document/root.tex Wed Jun 23 15:59:43 2010 +0100 +++ b/Quotient-Paper/document/root.tex Wed Jun 23 22:41:16 2010 +0100 @@ -45,8 +45,8 @@ non-empty types. Both extensions are often performed in quotient constructions. To ease the work involved with such quotient constructions, we re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we -extended his work in order to deal with compositions of quotients. We also -designed our quotient package so that every step in a quotient construction +extended his work in order to deal with compositions of quotients. Like his +package, we designed our quotient package so that every step in a quotient construction can be performed separately and as a result we are able to specify completely the procedure of lifting theorems from the raw level to the quotient level. The importance for programming language research is that many properties of