diff -r 337569f85398 -r 2cbcdaba795a Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Wed Jun 16 22:29:42 2010 +0100 +++ b/Quotient-Paper/Paper.thy Thu Jun 17 00:27:57 2010 +0100 @@ -768,7 +768,7 @@ with @{text "nat \ nat"} and we also quotient this type to yield integers, then we need to show the corresponding preservation lemma. - @{thm [display, indent=10] insert_preserve2[no_vars]} + %%%@ {thm [display, indent=10] insert_preserve2[no_vars]} %Given two quotients, one of which quotients a container, and the %other quotients the type in the container, we can write the @@ -809,31 +809,46 @@ The purpose of regularization is to change the quantifiers and abstractions 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 supposed to add @{term Rep} + (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 - quotient type. Cleaning rewrites the obtained injected theorem with - preservation rules obtaining the desired goal theorem. + 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: + + \begin{center} + \begin{tabular}{r@ {\hspace{4mm}}l} + 1.) & @{text "raw_thm \ reg_thm"}\\ + 2.) & @{text "reg_thm \ inj_thm"}\\ + 3.) & @{text "inj_thm \ quot_thm"}\\ + \end{tabular} + \end{center} - Most quotient packages take only an original theorem involving raw - types and lift it. The procedure in our package takes both an - original theorem involving raw types and a statement of the theorem - that it is supposed to produce. To simplify the use of the quotient - package we additionally provide an automated statement translation - mechanism which can produce the latter automatically given a list of - quotient types. It is possible that a user wants to lift only some - occurrences of a raw type. In this case the user specifies the - complete lifted goal instead of using the automated mechanism. + \noindent + In contrast to other quotient packages, our package requires + the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we + also provide a fully automated mode, where the @{text "quot_thm"} is guessed + from @{text "raw_thm"}.} As a result, it is possible that a user can lift only some + occurrences of a raw type. + + The second and third proof step will always succeed if the appropriate + respectfulness and preservation theorems are given. In contrast, the first + proof step can fail: a theorem given by the user does not always + imply a regularized version and a stronger one needs to be proved. This + is outside of the scope where the quotient package can help. An example + for the failure is the simple statement for integers @{text "0 \ 1"}. + It does not follow by lifting from the fact that @{text "(0, 0) \ (1, 0)"}. + The raw theorem only shows that particular element in the + equivalence classes are not equal. A more general statement saying that + the equivalence classes are not equal is necessary. In the following we will first define the statement of the - regularized theorem based on the original theorem and the goal - theorem. Then we define the statement of the injected theorem, based - on the regularized theorem and the goal. We then show the 3 proofs, - all three can be performed independently from each other. + regularized theorem based on @{text "raw_thm"} and the + @{text "quot_thm"}. Then we define the statement of the injected theorem, based + on @{text "reg_thm"} theorem and @{text "quot_thm"}. We then show the 3 proofs, + which can all be performed independently from each other. - We define the function @{text REG}, which takes the statements - of the raw theorem and the lifted theorem (both as terms) and - returns the statement of the regularized version. The intuition + We define the function @{text REG}. The intuition behind this function is that it replaces quantifiers and abstractions involving raw types by bounded ones, and equalities involving raw types are replaced by appropriate aggregate @@ -847,6 +862,7 @@ @{text "\x\<^sup>\. REG (t, s)"} \quad\mbox{provided @{text "\ = \"}}\\ @{text "\x\<^sup>\ \ Respects (REL (\, \)). REG (t, s)"} \end{cases}$\smallskip\\ + \\ \multicolumn{3}{@ {}l}{universal quantifiers:}\\ @{text "REG (\x\<^sup>\. t, \x\<^sup>\. s)"} & $\dn$ & $\begin{cases} @@ -870,9 +886,10 @@ In the above definition we omitted the cases for existential quantifiers and unique existential quantifiers, as they are very similar to the cases for the universal quantifier. - Next we define the function @{text INJ} which takes the statement of - the regularized theorems and the statement of the lifted theorem both as - terms and returns the statement of the injected theorem: + + Next we define the function @{text INJ} which takes as argument + @{text "reg_thm"} and @{text "quot_thm"} (both as + terms) and returns @{text "inj_thm"}: \begin{center} \begin{tabular}{rcl} @@ -902,103 +919,81 @@ \end{tabular} \end{center} - \noindent where the cases for existential quantifiers and unique existential - quantifiers have been omitted for clarity; are similar to universal quantifier. + \noindent + where again the cases for existential quantifiers and unique existential + quantifiers have been omitted. - We can now define the subgoals that will imply the lifted theorem. Given - the statement of the original theorem @{term t} and the statement of the - goal @{term g} the regularization subgoal is @{term "t \ REG(t, g)"}, - the injection subgoal is @{term "REG(t, g) = INJ(REG(t, g), g)"} and the - cleaning subgoal is @{term "INJ(REG(t, g), g) = g"}. We will now describe - the three tactics provided for these three subgoals. + 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 implication subgoals. This succeeds for every + monotone connectives, except in places wher the function @{text REG} inserted, + for example, a quantifier by a bounded quantifier. In this case we have + rules of the form - The injection and cleaning subgoals are always solved if the appropriate - respectfulness and preservation theorems are given. It is not the case - with regularization; sometimes a theorem given by the user does not - imply a regularized version and a stronger one needs to be proved. This - is outside of the scope of the quotient package, so such obligations are - left to the user. Take a simple statement for integers @{text "0 \ 1"}. - It does not follow from the fact that @{text "(0, 0) \ (1, 0)"} because - of regularization. The raw theorem only shows that particular items in the - equivalence classes are not equal. A more general statement saying that - the classes are not equal is necessary. + @{text [display, indent=10] "(\x. R x \ (P x \ Q x)) \ (\x. P x \ \x \ R. Q x)"} + + \noindent + They decompose a bounded quantifier on the right-hand side, but are only applicable + if we can prove that - In the proof of the regularization subgoal we always start with an implication. - Isabelle provides a set of \emph{mono} rules, that are used to split implications - of similar statements into simpler implication subgoals. These are enhanced - with special quotient theorem in the regularization proof. Below we only show - the versions for the universal quantifier. For the existential quantifier - and abstraction they are analogous. + @{text [display, indent=10] "\x \ Respects R. P x = \x. P x"} - First, bounded universal quantifiers can be removed on the right: - - @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]} - - They can be removed anywhere if the relation is an equivalence relation: - - @{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]} - - And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation: + \noindent + And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation + and 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 goals with such shape, and there - the equivalence assumption would be used. We use the above theorem directly - also for composed relations where the range type is a type for which we know an - equivalence theorem. This allows separating regularization from injection. + injection procedure would be used to prove such goals, and there + 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 independent ``units''. - The injection proof starts with an equality between the regularized theorem - and the injected version. The proof again follows by the structure of the - two terms, and is defined for a goal being a relation between these two terms. + The secon 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. \begin{itemize} - \item For two constants, an appropriate constant respectfulness assumption is used. - \item For two variables, we use the assumptions proved in regularization. - \item For two abstractions, they are eta-expanded and beta-reduced. - \item For two applications, if the right side is an application of - @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} we - can reduce the injected pair using the theorem: + \item For two constants an appropriate constant respectfulness lemma 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 + can apply the theorem: @{term [display, indent=10] "R x y \ R x (Rep (Abs y))"} - otherwise we introduce an appropriate relation between the subterms + Otherwise we introduce an appropriate relation between the subterms and continue with two subgoals using the lemma: @{text [display, indent=10] "(R\<^isub>1 \ R\<^isub>2) f g \ R\<^isub>1 x y \ R\<^isub>2 (f x) (g y)"} - \end{itemize} - The cleaning subgoal has been defined in such a way that - establishing the goal theorem now consists only on rewriting the - injected theorem with the preservation theorems and quotient - definitions. First for all lifted constants, their definitions + We defined the theorem @{text "inj_thm"} in such a way that + establishing the equivalence @{text "inj_thm \ quot_thm"} can be + achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient + definitions. Then all lifted constants, their definitions are used to fold the @{term Rep} with the raw constant. Next for - all lambda abstractions and quantifications the lambda and + all abstractions and quantifiers the lambda and quantifier preservation theorems are used to replace the - variables that include raw types with respects by quantification + variables that include raw types with respects by quantifiers over variables that include quotient types. We show here only - the lambda preservation theorem; assuming - @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"} - hold, we have: + the lambda preservation theorem. Given + @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have: - @{thm [display, indent=10] (concl) lambda_prs[no_vars]} + @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]} \noindent - holds. Next relations over lifted types are folded to equality. - The following theorem has been shown in Homeier~\cite{Homeier05}: + Next, relations over lifted types are folded to equalities. + For this the following theorem has been shown in Homeier~\cite{Homeier05}: @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]} \noindent - Finally the user given preservation theorems, that allow using - higher level operations and containers of types being lifted. - We show the preservation theorem for @{term map}. Again assuming - that @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"} hold, - we have: - - @{thm [display, indent=10] (concl) map_prs(1)[of R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1 R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2]} - + Finally, we rewrite with the preservation theorems. This will result + in two equal terms that can be solved by reflexivity. *} section {* Examples \label{sec:examples} *} @@ -1009,27 +1004,32 @@ 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 + lifting theorems to integers. Oeur 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''. 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 same integer relation as the one presented in the introduction: + the same integer relation as the one presented in \eqref{natpairequiv}: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % - \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~% - @{text "(m :: nat, n) int_rel (p, q) = (m + q = n + p)"} + \begin{tabular}{@ {}l} + \isacommand{fun}~~@{text "int_rel :: (nat \ nat) \ (nat \ nat) \ (nat \ nat)"}\\ + \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"} + \end{tabular} \end{isabelle} \noindent - Next the quotient type is defined. This leaves a proof obligation that the - relation is an equivalence relation which is solved automatically using the - definitions: + Next the quotient type is defined. This generates a proof obligation that the + relation is an equivalence relation, which is solved automatically using the + definition and extensionality: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % - \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \ nat)"}~~\isacommand{/}~~@{text "int_rel"} + \begin{tabular}{@ {}l} + \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \ nat)"}~~\isacommand{/}~~@{text "int_rel"}\\ + \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"} + \end{tabular} \end{isabelle} \noindent @@ -1037,7 +1037,7 @@ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % \begin{tabular}{@ {}l} - \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\ + \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm] \isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~% @{text "plus_raw (m, n) (p, q) = (m + p :: nat, n + q :: nat)"}\\ \isacommand{quotient\_definition}~~@{text "+ :: int \ int \ int"}~~% @@ -1046,39 +1046,48 @@ \end{isabelle} \noindent - Lets first take a simple theorem about addition on the raw level: + The following theorem about addition on the raw level can be proved. \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % \isacommand{lemma}~~@{text "plus_zero_raw: int_rel (plus_raw (0, 0) x) x"} \end{isabelle} \noindent - When the user tries to lift a theorem about integer addition, the respectfulness - proof obligation is left, so let us prove it first: + If the user attempts to lift this theorem, all proof obligations are + automatically discharged, except the respectfulness + proof for @{text "plus_raw"}: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % - \isacommand{lemma}~~@{text "[quot_respect]: + \begin{tabular}{@ {}l} + \isacommand{lemma}~~@{text "[quot_respect]:\\ (int_rel \ int_rel \ int_rel) plus_raw plus_raw"} + \end{tabular} \end{isabelle} \noindent - Can be proved automatically by the system just by unfolding the definition + This can be dischaged automatically by Isabelle when telling it to unfold the definition of @{text "\"}. - Now the user can either prove a lifted lemma explicitly: + After this, the user can prove the lifted lemma explicitly: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"} \end{isabelle} \noindent - Or in this simple case use the automated translation mechanism: + or by the completely automated mode by stating: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % \isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"} \end{isabelle} \noindent - obtaining the same result. + Both methods give the same result, namely + + @{text [display, indent=10] "0 + x = x"} + + \noindent + Although seemingly simple, arriving at this result without the help of a quotient + package requires substantial reasoning effort. *} section {* Conclusion and Related Work\label{sec:conc}*}