--- 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 \<lbrakk> \<rbrakk> 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 \<longrightarrow> 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 \<longrightarrow> 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 \<longrightarrow> R1 x 1 \<longrightarrow> 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]}
*}