--- a/Quotient-Paper/Paper.thy Tue Jun 15 12:00:03 2010 +0200
+++ b/Quotient-Paper/Paper.thy Tue Jun 15 22:25:03 2010 +0200
@@ -800,23 +800,33 @@
equivalence relations. It is defined as follows:
\begin{center}
- \begin{tabular}{rcl}
- \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
- @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\
- @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
- @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\
- @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\
- @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\
- @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\
+ \begin{longtable}{rcl}
+ \multicolumn{3}{@ {}l}{abstractions:}\smallskip\\
+ @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ &
+ $\begin{cases}
+ @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ @{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+ \end{cases}$\smallskip\\
+ \multicolumn{3}{@ {}l}{universal quantifiers:}\\
+ @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ &
+ $\begin{cases}
+ @{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ @{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+ \end{cases}$\smallskip\\
+ \multicolumn{3}{@ {}l}{equality:}\smallskip\\
+ @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ &
+ $\begin{cases}
+ @{text "="} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ @{text "REL (\<sigma>, \<tau>)"}\\
+ \end{cases}$\\
+ \multicolumn{3}{@ {}l}{applications, variables and constants:}\\
@{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
- @{text "REG (v\<^isub>1, v\<^isub>2)"} & $\dn$ & @{text "v\<^isub>1"}\\
- @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\
- \end{tabular}
+ @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
+ @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\[-5mm]
+ \end{longtable}
\end{center}
-
+ %
+ \noindent
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.
@@ -826,19 +836,29 @@
\begin{center}
\begin{tabular}{rcl}
- \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
- @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) "} & $\dn$ & @{text "\<lambda>x. INJ (t, s)"}\\
- @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}\\
- @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
- @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> (INJ (t, s))"}\\
- @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\\
- \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\
+ @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ &
+ $\begin{cases}
+ @{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
+ \end{cases}$\\
+ @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$
+ & @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{universal quantifiers:}\\
+ @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s)"}\\
+ @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
+ \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables and constants:}\smallskip\\
@{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
- @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "v\<^isub>1"}\\
- @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}\\
- @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "c\<^isub>1"}\\
- @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}\\
+ @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
+ $\begin{cases}
+ @{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
+ \end{cases}$\\
+ @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
+ $\begin{cases}
+ @{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+ @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\
+ \end{cases}$\\
\end{tabular}
\end{center}
@@ -857,8 +877,8 @@
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 @{term "0 \<noteq> 1"}.
- It does not follow from the fact that @{term "\<not> (0, 0) = (1, 0)"} because
+ left to the user. Take a simple statement for integers @{text "0 \<noteq> 1"}.
+ It does not follow from the fact that @{text "(0, 0) \<noteq> (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.
@@ -878,9 +898,9 @@
@{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]}
- And finally it can be removed anywhere if @{term R2} is an equivalence relation:
+ And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation:
- @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]}
+ @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
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
@@ -905,7 +925,7 @@
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)"}
+ @{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
\end{itemize}
@@ -919,8 +939,8 @@
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:
+ @{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) lambda_prs[no_vars]}
@@ -934,10 +954,10 @@
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"}
+ 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 R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
+ @{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]}
*}
@@ -959,7 +979,8 @@
the same integer relation as the one presented in the introduction:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
- \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~@{text "(m \<Colon> nat, n) int_rel (p, q) = (m + q = n + p)"}
+ \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~%
+ @{text "(m :: nat, n) int_rel (p, q) = (m + q = n + p)"}
\end{isabelle}
\noindent
@@ -976,9 +997,11 @@
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
\begin{tabular}{@ {}l}
- \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
- \isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~@{text "plus_raw (m :: nat, n) (p, q) = (m + p, n + q)"}\\
- \isacommand{quotient\_definition}~~@{text "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)"}~~\isacommand{is}~~@{text "plus_raw"}\\
+ \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\
+ \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 \<Rightarrow> int \<Rightarrow> int"}~~%
+ \isacommand{is}~~@{text "plus_raw"}\\
\end{tabular}
\end{isabelle}
@@ -994,12 +1017,13 @@
proof obligation is left, so let us prove it first:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
- \isacommand{lemma}~~@{text "[quot_respect]: (int_rel \<Longrightarrow> int_rel \<Longrightarrow> int_rel) plus_raw plus_raw"}
+ \isacommand{lemma}~~@{text "[quot_respect]:
+ (int_rel \<doublearr> int_rel \<doublearr> int_rel) plus_raw plus_raw"}
\end{isabelle}
\noindent
Can be proved automatically by the system just by unfolding the definition
- of @{text "op \<Longrightarrow>"}.
+ of @{text "\<doublearr>"}.
Now the user can either prove a lifted lemma explicitly:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
@@ -1033,16 +1057,16 @@
concurrency \cite{BengtsonParow09} and a strong normalisation result for
cut-elimination in classical logic \cite{UrbanZhu08}.
- Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
+ Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
defines quotient types for Isabelle/HOL. It did not include theorem lifting.
- John Harrison's quotient package~\cite{harrison-thesis} is the first one to
+ Harrison's quotient package~\cite{harrison-thesis} is the first one to
lift theorems, however only first order. There is work on quotient types in
non-HOL based systems and logical frameworks, namely theory interpretations
in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or
the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.
- Larry Paulson shows a construction of quotients that does not require the
+ Paulson shows a construction of quotients that does not require the
Hilbert Choice operator, again only first order~\cite{Paulson06}.
- The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05},
+ The closest to our package is the package for HOL4 by Homeier~\cite{Homeier05},
which is the first one to support lifting of higher order theorems.
@@ -1063,7 +1087,7 @@
a theory progressively.
We allow lifting only some occurrences of quotiented types, which
- is useful in Nominal. The package can be used automatically with
+ is useful in Nominal Isabelle. The package can be used automatically with
an attribute, manually with separate tactics for parts of the lifting
procedure, and programatically. Automated definitions of constants
and respectfulness proof obligations are used in Nominal. Finally
@@ -1073,8 +1097,8 @@
\medskip
\noindent
{\bf Acknowledgements:} We would like to thank Peter Homeier for the
- discussions about the HOL4 quotient package and explaining us its
- implementation details.
+ discussions about his HOL4 quotient package and explaining to us
+ some its finer points in the implementation.
*}