diff -r 1fd6809f5a44 -r c0c5bc4ee8cb Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Tue Jun 15 10:08:12 2010 +0200 +++ b/Quotient-Paper/Paper.thy Tue Jun 15 11:59:16 2010 +0200 @@ -1,5 +1,3 @@ -(* How to change the notation for \ \ meta-level implications? *) - (*<*) theory Paper imports "Quotient" @@ -353,7 +351,7 @@ and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]} \end{proposition} - \begin{definition}[Respects] + \begin{definition}[Respects]\label{def:respects} An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}. \end{definition} @@ -748,35 +746,39 @@ *} - section {* Lifting of Theorems\label{sec:lift} *} text {* - The core of our quotient package takes an original theorem - involving raw types and a statement of the theorem that - it is supposed to produce. This is different from existing - quotient packages, where only the raw theorems are necessary. - 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. - Lifting the theorems is performed in three steps. In the following - we call these steps \emph{regularization}, \emph{injection} and - \emph{cleaning} following the names used in Homeier's HOL4 - implementation. + + The core of a quotient package lifts an original theorem to a lifted + version. We will perform this operation in three phases. In the + following we call these phases \emph{regularization}, + \emph{injection} and \emph{cleaning} following the names used in + Homeier's HOL4 implementation. + + Regularization is supposed to change the quantifications and abstractions + in the theorem to quantification over variables that respect the relation + (definition \ref{def:respects}). Injection is supposed 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. - We 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, as all three - can be performed independently from each other. + 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. -*} -text {* \textit{Regularization and Injection statements} *} -text {* + 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. We define the function @{text REG}, which takes the statements of the raw theorem and the lifted theorem (both as terms) and @@ -829,32 +831,15 @@ \end{tabular} \end{center} - For existential quantifiers and unique existential quantifiers it is - defined similarly to the universal one. - -*} -text {*\textit{Proof Procedure}*} - -(* In the below the type-guiding 'QuotTrue' assumption is removed. We need it - only for bound variables without types, while in the paper presentation - variables are typed *) - -text {* + \noindent where the cases for existential quantifiers and unique existential + quantifiers have been omitted for clarity; are similar to universal quantifier. - When lifting a theorem we first apply the following rule - - @{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"} - - \noindent - with @{text A} instantiated to the original raw theorem, - @{text B} instantiated to @{text "REG(A)"}, - @{text C} instantiated to @{text "INJ(REG(A))"}, - and @{text D} instantiated to the statement of the lifted theorem. - The first assumption can be immediately discharged using the original - theorem and the three left subgoals are exactly the subgoals of regularization, - injection and cleaning. The three can be proved independently by the - framework and in case there are non-solved subgoals they can be left - to the user. + 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. The injection and cleaning subgoals are always solved if the appropriate respectfulness and preservation theorems are given. It is not the case @@ -867,10 +852,7 @@ equivalence classes are not equal. A more general statement saying that the classes are not equal is necessary. -*} -text {* \textit{Proving Regularization} *} -text {* - + 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 @@ -894,19 +876,7 @@ 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. -*} -text {* \textit{Proving Rep/Abs Injection} *} -(* - @{thm bex_reg_eqv_range[no_vars]} - @{thm [display] bex_reg_left[no_vars]} - @{thm [display] bex1_bexeq_reg[no_vars]} - @{thm [display] bex_reg_eqv[no_vars]} - @{thm [display] babs_reg_eqv[no_vars]} - @{thm [display] babs_simp[no_vars]} -*) - -text {* 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. @@ -915,42 +885,48 @@ \item For two constants, an appropriate constant respectfullness 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: + + @{term [display, indent=10] "R x y \ R x (Rep (Abs y))"} + + otherwise we introduce an appropriate relation between the subterms + and continue with two subgoals using the lemma: + + @{term [display, indent=10] "(R1 ===> R2) f g \ R1 x 1 \ R2 (f x) (g y)"} + \end{itemize} - Otherwise the two terms are applications. There are two cases: If there is a REP/ABS - in the injected theorem we can use the theorem: + 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 + are used to fold the @{term Rep} with the raw constant. Next for + all lambda abstractions and quantifications the lambda and + quantifier preservation theorems are used to replace the + variables that include raw types with respects by quantification + over variables that include quotient types. We show here only + the lambda preservation theorem; assuming + @{term "Quotient R1 Abs1 Rep1"} and @{term "Quotient R2 Abs2 Rep2"} + we have: - @{thm [display, indent=10] rep_abs_rsp[no_vars]} + @{thm [display, indent=10] (concl) lambda_prs[no_vars]} \noindent - and continue the proof. - - Otherwise we introduce an appropriate relation between the subterms and continue with - two subgoals using the lemma: + holds. Next relations over lifted types are folded to equality. + The following theorem has been shown in Homeier~\cite{Homeier05}: - @{thm [display, indent=10] apply_rsp[no_vars]} - -*} -text {* \textit{Cleaning} *} -text {* + @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]} - The @{text REG} and @{text INJ} functions have been defined in such a way - that establishing the goal theorem now consists only on rewriting the - injected theorem with the preservation theorems. + \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 R1 Abs1 Rep1"} and @{term "Quotient R2 Abs2 Rep2"} + we have: - \begin{itemize} - \item First for lifted constants, their definitions are the preservation rules for - them. - \item For lambda abstractions lambda preservation establishes - the equality between the injected theorem and the goal. This allows both - abstraction and quantification over lifted types. - @{thm [display] (concl) lambda_prs[no_vars]} - \item Relations over lifted types are folded with: - @{thm [display] (concl) Quotient_rel_rep[no_vars]} - \item User given preservation theorems, that allow using higher level operations - and containers of types being lifted. An example may be - @{thm [display] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]} - \end{itemize} + @{thm [display, indent=10] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]} *}