1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(*<*)
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
theory Paper
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
imports "Quotient"
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
"LaTeXsugar"
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
begin
|
1994
|
6 |
|
|
7 |
notation (latex output)
|
|
8 |
fun_rel ("_ ===> _" [51, 51] 50)
|
|
9 |
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
(*>*)
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
section {* Introduction *}
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
|
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
text {*
|
2103
|
15 |
{\hfill quote by Larry}\bigskip
|
|
16 |
|
|
17 |
\noindent
|
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
Isabelle is a generic theorem prover in which many logics can be implemented.
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
The most widely used one, however, is
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
Higher-Order Logic (HOL). This logic consists of a small number of
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
axioms and inference
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
mechanisms for extending the logic: one is the definition of new constants
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
in terms of existing ones; the other is the introduction of new types
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
by identifying non-empty subsets in existing types. It is well understood
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
to use both mechanism for dealing with quotient constructions in HOL (cite Larry).
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
For example the integers in Isabelle/HOL are constructed by a quotient construction over
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
the type @{typ "nat \<times> nat"} and the equivalence relation
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
@{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
\noindent
|
2103
|
33 |
Similarly one can construct the type of finite sets by quotienting lists
|
|
34 |
according to the equivalence relation
|
|
35 |
|
|
36 |
@{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
|
|
37 |
|
|
38 |
\noindent
|
|
39 |
where @{text "\<in>"} stands for membership in a list.
|
|
40 |
|
|
41 |
The problem is that in order to start reasoning about, for example integers,
|
|
42 |
definitions and theorems need to be transferred, or \emph{lifted},
|
|
43 |
from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}.
|
|
44 |
This lifting usually requires a lot of tedious reasoning effort.
|
|
45 |
The purpose of a \emph{quotient package} is to ease the lifting and automate
|
|
46 |
the reasoning involved as much as possible. Such a package is a central
|
|
47 |
component of the new version of Nominal Isabelle where representations
|
|
48 |
of alpha-equated terms are constructed according to specifications given by
|
|
49 |
the user.
|
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
|
2103
|
51 |
In the context of HOL, there have been several quotient packages (...). The
|
|
52 |
most notable is the one by Homeier (...) implemented in HOL4. However, what is
|
|
53 |
surprising, none of them can deal compositions of quotients, for example with
|
|
54 |
lifting theorems about @{text "concat"}:
|
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
|
2103
|
56 |
@{text [display] "concat definition"}
|
|
57 |
|
|
58 |
\noindent
|
|
59 |
One would like to lift this definition to the operation
|
|
60 |
|
|
61 |
@{text [display] "union definition"}
|
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
|
2103
|
63 |
\noindent
|
|
64 |
What is special about this operation is that we have as input
|
|
65 |
lists of lists which after lifting turn into finite sets of finite
|
|
66 |
sets.
|
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
*}
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
|
1978
|
69 |
subsection {* Contributions *}
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
|
1978
|
71 |
text {*
|
|
72 |
We present the detailed lifting procedure, which was not shown before.
|
|
73 |
|
|
74 |
The quotient package presented in this paper has the following
|
|
75 |
advantages over existing packages:
|
|
76 |
\begin{itemize}
|
|
77 |
|
|
78 |
\item We define quotient composition, function map composition and
|
|
79 |
relation map composition. This lets lifting polymorphic types with
|
|
80 |
subtypes quotiented as well. We extend the notions of
|
|
81 |
respectfullness and preservation to cope with quotient
|
|
82 |
composition.
|
|
83 |
|
|
84 |
\item We allow lifting only some occurrences of quotiented
|
|
85 |
types. Rsp/Prs extended. (used in nominal)
|
|
86 |
|
|
87 |
\item We regularize more thanks to new lemmas. (inductions in
|
|
88 |
nominal).
|
|
89 |
|
|
90 |
\item The quotient package is very modular. Definitions can be added
|
|
91 |
separately, rsp and prs can be proved separately and theorems can
|
|
92 |
be lifted on a need basis. (useful with type-classes).
|
|
93 |
|
|
94 |
\item Can be used both manually (attribute, separate tactics,
|
|
95 |
rsp/prs databases) and programatically (automated definition of
|
|
96 |
lifted constants, the rsp proof obligations and theorem statement
|
|
97 |
translation according to given quotients).
|
|
98 |
|
|
99 |
\end{itemize}
|
|
100 |
*}
|
|
101 |
|
|
102 |
section {* Quotient Type*}
|
|
103 |
|
|
104 |
text {*
|
|
105 |
Defintion of quotient,
|
|
106 |
|
|
107 |
Equivalence,
|
|
108 |
|
|
109 |
Relation map and function map
|
|
110 |
*}
|
|
111 |
|
|
112 |
section {* Constants *}
|
|
113 |
|
|
114 |
text {*
|
|
115 |
Rep and Abs, Rsp and Prs
|
|
116 |
*}
|
|
117 |
|
|
118 |
section {* Lifting Theorems *}
|
|
119 |
|
1994
|
120 |
text {* TBD *}
|
|
121 |
|
|
122 |
text {* Why providing a statement to prove is necessary is some cases *}
|
|
123 |
|
|
124 |
subsection {* Regularization *}
|
|
125 |
|
|
126 |
text {*
|
|
127 |
Transformation of the theorem statement:
|
|
128 |
\begin{itemize}
|
|
129 |
\item Quantifiers and abstractions involving raw types replaced by bounded ones.
|
|
130 |
\item Equalities involving raw types replaced by bounded ones.
|
|
131 |
\end{itemize}
|
|
132 |
|
|
133 |
The procedure.
|
|
134 |
|
|
135 |
Example of non-regularizable theorem ($0 = 1$).
|
|
136 |
|
|
137 |
New regularization lemmas:
|
|
138 |
\begin{lemma}
|
|
139 |
If @{term R2} is an equivalence relation, then:
|
|
140 |
\begin{eqnarray}
|
|
141 |
@{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
|
|
142 |
@{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
|
|
143 |
\end{eqnarray}
|
|
144 |
\end{lemma}
|
|
145 |
|
|
146 |
*}
|
|
147 |
|
|
148 |
subsection {* Injection *}
|
|
149 |
|
|
150 |
subsection {* Cleaning *}
|
|
151 |
|
|
152 |
text {* Preservation of quantifiers, abstractions, relations, quotient-constants
|
|
153 |
(definitions) and user given constant preservation lemmas *}
|
|
154 |
|
|
155 |
section {* Examples *}
|
|
156 |
|
1978
|
157 |
section {* Related Work *}
|
|
158 |
|
|
159 |
text {*
|
|
160 |
\begin{itemize}
|
|
161 |
|
|
162 |
\item Peter Homeier's package (and related work from there), John
|
|
163 |
Harrison's one.
|
|
164 |
|
|
165 |
\item Manually defined quotients in Isabelle/HOL Library (Larry's
|
|
166 |
quotients, Markus's Quotient\_Type, Dixon's FSet, \ldots)
|
|
167 |
|
|
168 |
\item Oscar Slotosch defines quotient-type automatically but no
|
|
169 |
lifting.
|
|
170 |
|
|
171 |
\item PER. And how to avoid it.
|
|
172 |
|
|
173 |
\item Necessity of Hilbert Choice op.
|
|
174 |
|
|
175 |
\item Setoids in Coq
|
|
176 |
|
|
177 |
\end{itemize}
|
|
178 |
*}
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
179 |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
180 |
(*<*)
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
181 |
end
|
1978
|
182 |
(*>*)
|