# HG changeset patch # User Christian Urban # Date 1275916419 -7200 # Node ID 02e03d4287ec66ccc4423a7f0b3f0cb973c7be40 # Parent 231a20534950fc3d49057160204dabd0d67cd57f a bit more in the introduction and abstract diff -r 231a20534950 -r 02e03d4287ec Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Mon Jun 07 11:33:00 2010 +0200 +++ b/Quotient-Paper/Paper.thy Mon Jun 07 15:13:39 2010 +0200 @@ -50,31 +50,33 @@ \end{flushright}\smallskip \noindent - Isabelle is a 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 - to use both mechanisms for dealing with quotient constructions in HOL (see for example - \cite{Paulson06}). - For example the integers in Isabelle/HOL are constructed by a quotient construction over - the type @{typ "nat \ nat"} and the equivalence relation + Isabelle is a 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 to use both mechanisms for dealing with quotient constructions in + HOL (see for example \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 -% I would avoid substraction for natural numbers. - - @{text [display] "(n\<^isub>1, n\<^isub>2) \ (m\<^isub>1, m\<^isub>2) \ n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"} + @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \ (m\<^isub>1, m\<^isub>2) \ n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"} \noindent - Similarly one can construct the type of finite sets by quotienting lists - according to the equivalence relation + This produces the type @{typ int} and definitions for @{text "0::int"} and + @{text "1::int"} in terms of pairs of natural numbers can be given (namely + @{text "(0, 0)"} and @{text "(1, 0)"}). Operations such as @{text "add::int + \ int \ int"} can be defined in terms of operations on pairs of natural + numbers. Similarly one can construct the type of finite sets by quotienting + lists according to the equivalence relation - @{text [display] "xs \ ys \ (\x. x \ xs \ x \ ys)"} + @{text [display, indent=10] "xs \ ys \ (\x. x \ xs \ x \ ys)"} \noindent - where @{text "\"} stands for membership in a list. + which means two lists are equivalent if every element in one list is also + member in the other (@{text "\"} stands here for membership in lists). The problem is that in order to start reasoning about, for example integers, definitions and theorems need to be transferred, or \emph{lifted}, diff -r 231a20534950 -r 02e03d4287ec Quotient-Paper/document/root.tex --- a/Quotient-Paper/document/root.tex Mon Jun 07 11:33:00 2010 +0200 +++ b/Quotient-Paper/document/root.tex Mon Jun 07 15:13:39 2010 +0200 @@ -24,18 +24,19 @@ \maketitle \begin{abstract} -Higher-order logic (HOL), used in several theorem provers, is based on a -small logic kernel, whose only mechanism for extension is the introduction -of safe definitions and non-empty types. Both extensions are often performed by +Higher-order logic (HOL), used in several theorem provers, is based on a small +logic kernel, whose only mechanism for extension is the introduction of safe +definitions and non-empty types. Both extensions are often performed by quotient constructions; for example finite sets are constructed by quotienting -lists, or integers by quotienting pairs of natural numbers. To ease the work -involved with 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. Also, we designed -our quotient package so that every step in a quotient construction -can be performed separately. The importance to programming language research -is that many properties of programming languages are more convenient to verify -over $\alpha$-quotient terms, than over raw terms. +lists, or integers by quotienting pairs of natural numbers. To ease the work +involved with 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. Also, we designed our quotient package so that +every step in a quotient construction can be performed separately and as a +result were able to specify completely the procedure of lifting theorems from +the raw level to the quotient level. The importance to programming language +research is that many properties of programming languages are more convenient +to verify over $\alpha$-quotient terms, than over raw terms. \end{abstract} % generated text of all theories