# HG changeset patch # User Christian Urban # Date 1333490953 -3600 # Node ID 16e6140225afc930ca4a9c4b1362d99451ae128a # Parent 8a3352cff8d0a27f78903df1ca2336c3359517f2 a bit more on the qpaper diff -r 8a3352cff8d0 -r 16e6140225af Quotient-Paper-jv/Paper.thy --- a/Quotient-Paper-jv/Paper.thy Fri Mar 30 16:08:00 2012 +0200 +++ b/Quotient-Paper-jv/Paper.thy Tue Apr 03 23:09:13 2012 +0100 @@ -43,9 +43,19 @@ Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2)) *} +fun add_pair :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" +where "add_pair (n1, m1) (n2, m2) = (n1 + n2, m1 + m2)" + +fun minus_pair :: "(nat \ nat) \ (nat \ nat)" +where "minus_pair (n, m) = (m, n)" + +fun + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" +where + "intrel (x, y) (u, v) = (x + v = u + y)" + (*>*) - section {* Introduction *} text {* @@ -75,11 +85,20 @@ This constructions yields the new type @{typ int}, and definitions for @{text "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations - such as @{text "add"} with type @{typ "int \ int \ int"} can be defined in - terms of operations on pairs of natural numbers: + such as @{text "add"} with type @{typ "int \ int \ int"} can be defined + in terms of operations on pairs of natural numbers: \begin{isabelle}\ \ \ \ \ %%% - @{text "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2, m\<^isub>2) \ (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"} + @{thm add_pair.simps[where ?n1.0="n\<^isub>1" and ?n2.0="n\<^isub>2" and ?m1.0="m\<^isub>1" and ?m2.0="m\<^isub>2", THEN eq_reflection]}% + \hfill\numbered{addpair} + \end{isabelle} + + \noindent + Negation on integers is defined in terms of swapping on pairs: + + \begin{isabelle}\ \ \ \ \ %%% + @{thm minus_pair.simps[where ?n="n" and ?m="m", THEN eq_reflection]}% + \hfill\numbered{minuspair} \end{isabelle} \noindent @@ -121,21 +140,97 @@ $\alpha$-equated terms, equality coincides with $\alpha$-equivalence and we can use for reasoning HOL's built-in notion of ``replacing equals by equals''. - {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?} + There is also often a need to consider quotients of parial equivalence relations. For + example the rational numbers + can be constructed using pairs of integers and the partial equivalence relation + \begin{isabelle}\ \ \ \ \ %%% + @{text "(n\<^isub>1, n\<^isub>2) \ (m\<^isub>1, m\<^isub>2) \ n\<^isub>1 * m\<^isub>2 = m\<^isub>1 * n\<^isub>2"}\hfill\numbered{ratpairequiv} + \end{isabelle} + + \noindent + where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not zero. - The difficulty is that in order to be able to reason about integers, finite - sets or $\alpha$-equated lambda-terms one needs to establish a reasoning - infrastructure by transferring, or \emph{lifting}, definitions and theorems - 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}. - In principle it is feasible to do 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 difficulty is that in order to be able to reason about integers, + finite sets, $\alpha$-equated lambda-terms and rational numbers one + needs to establish a reasoning infrastructure by transferring, or + \emph{lifting}, definitions and theorems from the raw type @{typ + "nat \ nat"} to the quotient type @{typ int} (similarly for finite + sets, $\alpha$-equated lambda-terms and rational numbers). This + lifting usually requires a reasoning effort that can be repetitive + and involves explicit mediation between the quotient and raw level + \cite{Paulson06}. In principle it is feasible to do 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 of theorems - and automate the reasoning as much as possible. In the + and automate the reasoning as much as possible. Before we delve into the + details, let us show how the user interacts with our quotient package + when defining integers. We assume the definitions involving pairs + of natural numbers shown in \eqref{natpairequiv}, \eqref{addpair} and + \eqref{minuspair} have already been made. A quotient can be introduced by declaring + the new type (in this case @{typ int}), the raw type (@{typ "nat * nat"}) and the + equivalence relation (@{text intrel} defined in \eqref{natpairequiv}). +*} + + quotient_type int = "nat \ nat" / intrel + +txt {* + \noindent + This declaration requires the user to prove that @{text intrel} is + indeed an equivalence relation, whereby the notion of an equivalence + relation is defined as usual in terms of reflexivity, symmetry and + transitivity. This proof obligation can thus be discharged by + unfolding the definitions and using the standard automatic proving + tactic in Isabelle. +*} + unfolding equivp_reflp_symp_transp + unfolding reflp_def symp_def transp_def + by auto +(*<*) + instantiation int :: "{zero, one, plus, uminus}" + begin +(*>*) +text {* + \noindent + Next we can declare the constants zero and one for the quotient type @{text int}. +*} + quotient_definition + "0 \ int" is "(0\nat, 0\nat)" . + + quotient_definition + "1 \ int" is "(1\nat, 0\nat)" . + +text {* + \noindent + To be useful and to state some properties, we also need to declare + two operations for adding two integers (written infix as @{text "_ + _"}) and negating + an integer (written @{text "uminus _"} or @{text "- _"}). +*} + + quotient_definition + "(op +) \ int \ int \ int" is add_pair + by auto + + quotient_definition + "uminus \ int \ int" is minus_pair + by auto +(*<*) + instance .. + + end +(*>*) + +text {* + \noindent + In both cases we have to discharge a proof-obligation which ensures + that the operations a \emph{respectful}. This property ensures that + the operations are well-defined on the quotient level (a formal + definition will be given later). Both proofs can again be solved by + the automatic proving tactic in Isabelle. + + In the context of HOL, there have been a few quotient packages already \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier \cite{Homeier05} implemented in HOL4. The fundamental construction these diff -r 8a3352cff8d0 -r 16e6140225af Quotient-Paper-jv/document/root.tex --- a/Quotient-Paper-jv/document/root.tex Fri Mar 30 16:08:00 2012 +0200 +++ b/Quotient-Paper-jv/document/root.tex Tue Apr 03 23:09:13 2012 +0100 @@ -9,9 +9,6 @@ \usepackage{pdfsetup} \usepackage{times} \usepackage{stmaryrd} -%\newtheorem{definition}{Definition} -%\newtheorem{proposition}{Proposition} -%\newtheorem{lemma}{Lemma} \urlstyle{rm} \isabellestyle{it} @@ -25,7 +22,6 @@ \renewcommand{\isasymequiv}{$\triangleq$} \renewcommand{\isasymemptyset}{$\varnothing$} -%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} \renewcommand{\isasymUnion}{$\bigcup$} \renewcommand{\isacharunderscore}{\text{$\_\!\_$}} @@ -40,7 +36,7 @@ \title{Quotients Revisited for Isabelle/HOL} \author{Cezary Kaliszyk \and Christian Urban} \institute{C.~Kaliszyk \at University of Innsbruck, Austria - \and C.~Urban \at King's College London, UK} + \and C.~Urban \at King's College London, UK} \date{Received: date / Accepted: date} \maketitle @@ -49,15 +45,14 @@ Higher-Order Logic (HOL) is based on a small logic kernel, whose only mechanism for extension is the introduction of safe definitions and of non-empty types. Both extensions are often performed in quotient -constructions. To ease the work involved with such quotient constructions, we -re-implemented in the %popular -Isabelle/HOL theorem prover the quotient -package by Homeier. In doing so we extended his work in order to deal with -compositions of quotients and also specified completely the procedure -of lifting theorems from the raw level to the quotient level. -The importance for theorem proving is that many formal -verifications, in order to be feasible, require a convenient reasoning infrastructure -for quotient constructions. +constructions. To ease the work involved with such quotient +constructions, we re-implemented in the Isabelle/HOL theorem prover +the quotient package by Homeier. In doing so we extended his work in +order to deal with compositions of quotients and also specified +completely the procedure of lifting theorems from the raw level to the +quotient level. The importance for theorem proving is that many +formal verifications, in order to be feasible, require a convenient +reasoning infrastructure for quotient constructions. \end{abstract} %\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}