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