# HG changeset patch # User Christian Urban # Date 1334067667 -3600 # Node ID 80e2fb39332b5973764fbc3df25b6268a685e6b5 # Parent 0fb396ae137a03ba016230f10965c0827db6a0d0 slight polishing on Quotient paper diff -r 0fb396ae137a -r 80e2fb39332b Quotient-Paper-jv/Paper.thy --- a/Quotient-Paper-jv/Paper.thy Tue Apr 10 15:19:42 2012 +0100 +++ b/Quotient-Paper-jv/Paper.thy Tue Apr 10 15:21:07 2012 +0100 @@ -50,7 +50,7 @@ where "minus_pair (n, m) = (m, n)" fun - intrel :: "(nat \ nat) \ (nat \ nat) \ bool" + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" ("_ \ _" [50, 50] 50) where "intrel (x, y) (u, v) = (x + v = u + y)" @@ -94,7 +94,7 @@ \end{isabelle} \noindent - Negation on integers is defined in terms of swapping on pairs: + Negation on integers is defined in terms of swapping of pairs: \begin{isabelle}\ \ \ \ \ %%% @{thm minus_pair.simps[where ?n="n" and ?m="m", THEN eq_reflection]}% @@ -149,29 +149,31 @@ \end{isabelle} \noindent - where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not zero. + where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not allowed to be zero. 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. + finite sets, etc.~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 rather repetitive and involves explicit conversions + between the quotient and raw level in form of abstraction and + representation functions \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. 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}). + The purpose of a \emph{quotient package} is to ease the lifting of + theorems 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 then be introduced by declaring the new type (in this case + @{typ int}), the raw type (that is @{typ "nat \ nat"}) and the + equivalence relation (that is @{text intrel} defined in + \eqref{natpairequiv}). *} quotient_type int = "nat \ nat" / intrel @@ -179,11 +181,11 @@ 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 + indeed an equivalence relation, whereby an equivalence + relation is defined as one that is reflexive, symmetric and + transitive. This proof obligation can thus be discharged by unfolding the definitions and using the standard automatic proving - tactic in Isabelle. + tactic in Isabelle/HOL. *} unfolding equivp_reflp_symp_transp unfolding reflp_def symp_def transp_def @@ -194,7 +196,8 @@ (*>*) text {* \noindent - Next we can declare the constants zero and one for the quotient type @{text int}. + Next we can declare the constants @{text "0"} and @{text "1"} for the + quotient type @{text int}. *} quotient_definition "0 \ int" is "(0\nat, 0\nat)" . @@ -204,13 +207,13 @@ 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 "- _"}). + To be useful, we can also need declare two operations for adding two + integers (written @{text plus}) and negating an integer + (written @{text "uminus"}). *} quotient_definition - "(op +) \ int \ int \ int" is add_pair + "plus \ int \ int \ int" is add_pair by auto quotient_definition @@ -224,11 +227,104 @@ 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. + Isabelle/HOL can introduce some convenient short-hand notation for these + operations allowing the user to write + addition as infix operation, for example @{text "i + j"}, and + negation as prefix operation, for example @{text "- i"}. In both + cases, however, the declaration requires the user 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 of + respectfulness will be given later). Both proofs can be solved by + the automatic proving tactic in Isabelle/HOL. + + Besides helping with declarations of quotient types and definitions + of constants, the point of a quotient package is to help with + proving properties about quotient types. For example we might be + interested in the usual property that zero is an ???. This property + can be stated as follows: +*} + + lemma zero_add: + shows "0 + i = (i::int)" + proof(descending) +txt {* + \noindent + The tactic @{text "descending"} automatically transfers this property of integers + to a proof-obligation involving pairs of @{typ nat}s. (There is also + a tactic, called @{text lifting}, which automatically transfers properties + from the raw level to the quotient type.) In case of lemma @{text "zero_add"} + we obtain the subgoal + + \begin{isabelle}\ \ \ \ \ %%% + @{text "add_pair (0, 0) i \ i"} + \end{isabelle} + + \noindent + which can be solved again by the automatic proving tactic @{text "auto"}, as follows +*} + qed(auto) + +text {* + In this simple example the task of the user is to state the property for integers + and use the quotient package and automatic proving tools of Isabelle/HOL to do + the ``rest''. A more interesting example is to establish an induction principle for + integers. For this we first establish the following induction principle where the + induction proceeds over two natural numbers. +*} + + lemma nat_induct2: + assumes "P 0 0" + and "\n m. P n m \ P (Suc n) m" + and "\n m. P n m \ P n (Suc m)" + shows "P n m" + using assms + by (induction_schema) (pat_completeness, lexicographic_order) + +text {* + \noindent + The symbol @{text "\"} stands for Isabelle/HOL's universal quantifier and + @{text "\"} for its implication. + As can be seen, this induction principle can be conveniently established using the + reasoning infrastructure of the function package \cite{???}, which + provides the tactics @{text "induction_schema"}, @{text "pat_completeness"} + and @{text "lexicographic_order"}. These tactics enable Isabelle/HOL + to use well-founded induction to prove @{text "nat_induct2"}. Our + quotient package can now be used to prove the following property: +*} + + lemma int_induct: + assumes "P 0" + and "\i. P i \ P (i + 1)" + and "\i. P i \ P (i + (- 1))" + shows "P (j::int)" + using assms + proof (descending) + +txt {* + \noindent + The @{text descending} tactic transfers it to the following proof + obligation on the raw level. + + @{subgoals[display]} + + \noindent + Note that the variable @{text "j"} in this subgoal is of type + @{text "nat \ nat"}. This subgoal cannot be proved automatically by + @{text auto}, but if we give it the hint to use @{text nat_induct2}, + then @{text auto} can discharge it as follows. + +*} + qed (auto intro: nat_induct2) + +text {* + This completes the proof of the induction principle + for integers. Isabelle/HOL would allow us to inspect the + detailed reasoning steps involved which would confirm that + @{text "int_induct"} has been proved from ``first-principles'' + by transforming the property over the quotient type @{text int} + to a corresponding property one on the raw level. + In the context of HOL, there have been a few quotient packages already