author | Christian Urban <urbanc@in.tum.de> |
Mon, 07 Jun 2010 11:33:00 +0200 | |
changeset 2213 | 231a20534950 |
parent 2212 | 79cebcc230d6 |
child 2214 | 02e03d4287ec |
permissions | -rw-r--r-- |
2208 | 1 |
(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *) |
2195
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
2 |
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
(*<*) |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
theory Paper |
2183 | 5 |
imports "Quotient" |
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
"LaTeXsugar" |
2186
762a739c9eb4
added FSet to the correct paper
Christian Urban <urbanc@in.tum.de>
parents:
2183
diff
changeset
|
7 |
"../Nominal/FSet" |
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
begin |
1994 | 9 |
|
2208 | 10 |
print_syntax |
11 |
||
1994 | 12 |
notation (latex output) |
2182 | 13 |
rel_conj ("_ OOO _" [53, 53] 52) |
14 |
and |
|
2208 | 15 |
"op -->" (infix "\<rightarrow>" 100) |
16 |
and |
|
17 |
"==>" (infix "\<Rightarrow>" 100) |
|
2182 | 18 |
and |
2208 | 19 |
fun_map (infix "\<longrightarrow>" 51) |
20 |
and |
|
21 |
fun_rel (infix "\<Longrightarrow>" 51) |
|
2188 | 22 |
and |
23 |
list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *) |
|
1994 | 24 |
|
2182 | 25 |
ML {* |
26 |
fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
|
27 |
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
|
28 |
let |
|
29 |
val concl = |
|
30 |
Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t) |
|
31 |
in |
|
32 |
case concl of (_ $ l $ r) => proj (l, r) |
|
33 |
| _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl) |
|
34 |
end); |
|
35 |
*} |
|
36 |
setup {* |
|
37 |
Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #> |
|
38 |
Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #> |
|
39 |
Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2)) |
|
40 |
*} |
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
(*>*) |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
section {* Introduction *} |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
|
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1994
diff
changeset
|
45 |
text {* |
2205 | 46 |
\begin{flushright} |
47 |
{\em ``Not using a [quotient] package has its advantages: we do not have to\\ |
|
48 |
collect all the theorems we shall ever want into one giant list;''}\\ |
|
2213
231a20534950
improved abstract, some tuning
Christian Urban <urbanc@in.tum.de>
parents:
2212
diff
changeset
|
49 |
Larry Paulson \cite{Paulson06} |
2205 | 50 |
\end{flushright}\smallskip |
2103
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
51 |
|
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
52 |
\noindent |
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1994
diff
changeset
|
53 |
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>
parents:
1994
diff
changeset
|
54 |
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>
parents:
1994
diff
changeset
|
55 |
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>
parents:
1994
diff
changeset
|
56 |
axioms and inference |
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1994
diff
changeset
|
57 |
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>
parents:
1994
diff
changeset
|
58 |
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>
parents:
1994
diff
changeset
|
59 |
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>
parents:
1994
diff
changeset
|
60 |
by identifying non-empty subsets in existing types. It is well understood |
2213
231a20534950
improved abstract, some tuning
Christian Urban <urbanc@in.tum.de>
parents:
2212
diff
changeset
|
61 |
to use both mechanisms for dealing with quotient constructions in HOL (see for example |
231a20534950
improved abstract, some tuning
Christian Urban <urbanc@in.tum.de>
parents:
2212
diff
changeset
|
62 |
\cite{Paulson06}). |
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1994
diff
changeset
|
63 |
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>
parents:
1994
diff
changeset
|
64 |
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>
parents:
1994
diff
changeset
|
65 |
|
2182 | 66 |
% I would avoid substraction for natural numbers. |
67 |
||
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1994
diff
changeset
|
68 |
@{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>
parents:
1994
diff
changeset
|
69 |
|
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1994
diff
changeset
|
70 |
\noindent |
2103
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
71 |
Similarly one can construct the type of finite sets by quotienting lists |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
72 |
according to the equivalence relation |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
73 |
|
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
74 |
@{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
75 |
|
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
76 |
\noindent |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
77 |
where @{text "\<in>"} stands for membership in a list. |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
78 |
|
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
79 |
The problem is that in order to start reasoning about, for example integers, |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
80 |
definitions and theorems need to be transferred, or \emph{lifted}, |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
81 |
from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
82 |
This lifting usually requires a lot of tedious reasoning effort. |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
83 |
The purpose of a \emph{quotient package} is to ease the lifting and automate |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
84 |
the reasoning involved as much as possible. Such a package is a central |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
85 |
component of the new version of Nominal Isabelle where representations |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
86 |
of alpha-equated terms are constructed according to specifications given by |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
87 |
the user. |
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1994
diff
changeset
|
88 |
|
2103
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
89 |
In the context of HOL, there have been several quotient packages (...). The |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
90 |
most notable is the one by Homeier (...) implemented in HOL4. However, what is |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
91 |
surprising, none of them can deal compositions of quotients, for example with |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
92 |
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>
parents:
1994
diff
changeset
|
93 |
|
2190 | 94 |
@{thm [display] concat.simps(1)} |
95 |
@{thm [display] concat.simps(2)[no_vars]} |
|
2183 | 96 |
|
2103
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
97 |
\noindent |
2188 | 98 |
One would like to lift this definition to the operation: |
99 |
||
2190 | 100 |
@{thm [display] fconcat_empty[no_vars]} |
101 |
@{thm [display] fconcat_insert[no_vars]} |
|
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1994
diff
changeset
|
102 |
|
2103
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
103 |
\noindent |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
104 |
What is special about this operation is that we have as input |
e08e3c29dbc0
a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents:
2102
diff
changeset
|
105 |
lists of lists which after lifting turn into finite sets of finite |
2190 | 106 |
sets. |
2102
200954544cae
added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1994
diff
changeset
|
107 |
*} |
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
108 |
|
1978 | 109 |
subsection {* Contributions *} |
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
110 |
|
1978 | 111 |
text {* |
112 |
We present the detailed lifting procedure, which was not shown before. |
|
113 |
||
114 |
The quotient package presented in this paper has the following |
|
115 |
advantages over existing packages: |
|
116 |
\begin{itemize} |
|
117 |
||
118 |
\item We define quotient composition, function map composition and |
|
119 |
relation map composition. This lets lifting polymorphic types with |
|
120 |
subtypes quotiented as well. We extend the notions of |
|
2188 | 121 |
respectfulness and preservation to cope with quotient |
1978 | 122 |
composition. |
123 |
||
124 |
\item We allow lifting only some occurrences of quotiented |
|
125 |
types. Rsp/Prs extended. (used in nominal) |
|
126 |
||
127 |
\item The quotient package is very modular. Definitions can be added |
|
2206 | 128 |
separately, rsp and prs can be proved separately, Quotients and maps |
129 |
can be defined separately and theorems can |
|
130 |
be lifted on a need basis. (useful with type-classes). |
|
1978 | 131 |
|
132 |
\item Can be used both manually (attribute, separate tactics, |
|
133 |
rsp/prs databases) and programatically (automated definition of |
|
134 |
lifted constants, the rsp proof obligations and theorem statement |
|
135 |
translation according to given quotients). |
|
136 |
||
137 |
\end{itemize} |
|
138 |
*} |
|
139 |
||
140 |
section {* Quotient Type*} |
|
141 |
||
2182 | 142 |
|
143 |
||
1978 | 144 |
text {* |
2182 | 145 |
In this section we present the definitions of a quotient that follow |
146 |
those by Homeier, the proofs can be found there. |
|
147 |
||
148 |
\begin{definition}[Quotient] |
|
149 |
A relation $R$ with an abstraction function $Abs$ |
|
150 |
and a representation function $Rep$ is a \emph{quotient} |
|
151 |
if and only if: |
|
1978 | 152 |
|
2182 | 153 |
\begin{enumerate} |
154 |
\item @{thm (rhs1) Quotient_def[of "R", no_vars]} |
|
155 |
\item @{thm (rhs2) Quotient_def[of "R", no_vars]} |
|
156 |
\item @{thm (rhs3) Quotient_def[of "R", no_vars]} |
|
157 |
\end{enumerate} |
|
158 |
||
159 |
\end{definition} |
|
1978 | 160 |
|
2188 | 161 |
\begin{definition}[Relation map and function map]\\ |
2190 | 162 |
@{thm fun_rel_def[of "R1" "R2", no_vars]}\\ |
2182 | 163 |
@{thm fun_map_def[no_vars]} |
164 |
\end{definition} |
|
165 |
||
166 |
The main theorems for building higher order quotients is: |
|
167 |
\begin{lemma}[Function Quotient] |
|
168 |
If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]} |
|
169 |
then @{thm (concl) fun_quotient[no_vars]} |
|
170 |
\end{lemma} |
|
171 |
||
1978 | 172 |
*} |
173 |
||
2195
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
174 |
subsection {* Higher Order Logic *} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
175 |
|
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
176 |
text {* |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
177 |
|
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
178 |
Types: |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
179 |
\begin{eqnarray}\nonumber |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
180 |
@{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
181 |
@{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
182 |
\end{eqnarray} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
183 |
|
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
184 |
Terms: |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
185 |
\begin{eqnarray}\nonumber |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
186 |
@{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
187 |
@{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
188 |
@{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
189 |
@{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
190 |
\end{eqnarray} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
191 |
|
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
192 |
*} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
193 |
|
1978 | 194 |
section {* Constants *} |
195 |
||
2188 | 196 |
(* Say more about containers? *) |
2182 | 197 |
|
1978 | 198 |
text {* |
2182 | 199 |
|
2188 | 200 |
To define a constant on the lifted type, an aggregate abstraction |
201 |
function is applied to the raw constant. Below we describe the operation |
|
202 |
that generates |
|
203 |
an aggregate @{term "Abs"} or @{term "Rep"} function given the |
|
204 |
compound raw type and the compound quotient type. |
|
205 |
This operation will also be used in translations of theorem statements |
|
206 |
and in the lifting procedure. |
|
207 |
||
208 |
The operation is additionally able to descend into types for which |
|
209 |
maps are known. Such maps for most common types (list, pair, sum, |
|
2195
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
210 |
option, \ldots) are described in Homeier, and we assume that @{text "map"} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
211 |
is the function that returns a map for a given type. Then REP/ABS is defined |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
212 |
as follows: |
2182 | 213 |
|
214 |
\begin{itemize} |
|
2195
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
215 |
\item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
216 |
\item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
217 |
\item @{text "ABS(\<sigma>, \<sigma>)"} = @{text "id"} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
218 |
\item @{text "REP(\<sigma>, \<sigma>)"} = @{text "id"} |
2208 | 219 |
\item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"} = @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"} |
220 |
\item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"} = @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"} |
|
2195
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
221 |
\item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
222 |
\item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
223 |
\item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"} |
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
224 |
\item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"} |
2182 | 225 |
\end{itemize} |
226 |
||
2195
0c1dcdefb515
Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2194
diff
changeset
|
227 |
Apart from the last 2 points the definition is same as the one implemented in |
2208 | 228 |
in Homeier's HOL package. Adding composition in last two cases is necessary |
229 |
for compositional quotients. We ilustrate the different behaviour of the |
|
230 |
definition by showing the derived definition of @{term fconcat}: |
|
2182 | 231 |
|
2188 | 232 |
@{thm fconcat_def[no_vars]} |
233 |
||
234 |
The aggregate @{term Abs} function takes a finite set of finite sets |
|
235 |
and applies @{term "map rep_fset"} composed with @{term rep_fset} to |
|
236 |
its input, obtaining a list of lists, passes the result to @{term concat} |
|
237 |
obtaining a list and applies @{term abs_fset} obtaining the composed |
|
238 |
finite set. |
|
239 |
*} |
|
240 |
||
241 |
subsection {* Respectfulness *} |
|
242 |
||
243 |
text {* |
|
244 |
||
245 |
A respectfulness lemma for a constant states that the equivalence |
|
246 |
class returned by this constant depends only on the equivalence |
|
2207 | 247 |
classes of the arguments applied to the constant. To automatically |
248 |
lift a theorem that talks about a raw constant, to a theorem about |
|
249 |
the quotient type a respectfulness theorem is required. |
|
250 |
||
251 |
A respectfulness condition for a constant can be expressed in |
|
252 |
terms of an aggregate relation between the constant and itself, |
|
253 |
for example the respectfullness for @{term "append"} |
|
2188 | 254 |
can be stated as: |
255 |
||
2190 | 256 |
@{thm [display] append_rsp[no_vars]} |
2182 | 257 |
|
2190 | 258 |
\noindent |
2208 | 259 |
Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to: |
2188 | 260 |
|
2190 | 261 |
@{thm [display] append_rsp_unfolded[no_vars]} |
2188 | 262 |
|
2207 | 263 |
An aggregate relation is defined in terms of relation composition, |
264 |
so we define it first: |
|
2188 | 265 |
|
266 |
\begin{definition}[Composition of Relations] |
|
2190 | 267 |
@{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate |
268 |
composition @{thm pred_compI[no_vars]} |
|
2188 | 269 |
\end{definition} |
270 |
||
2207 | 271 |
The aggregate relation for an aggregate raw type and quotient type |
272 |
is defined as: |
|
2188 | 273 |
|
274 |
\begin{itemize} |
|
2207 | 275 |
\item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="} |
276 |
\item @{text "REL(\<sigma>, \<sigma>)"} = @{text "op ="} |
|
277 |
\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"} |
|
278 |
\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"} |
|
2189 | 279 |
|
2188 | 280 |
\end{itemize} |
281 |
||
2207 | 282 |
Again, the last case is novel, so lets look at the example of |
283 |
respectfullness for @{term concat}. The statement according to |
|
284 |
the definition above is: |
|
2190 | 285 |
|
286 |
@{thm [display] concat_rsp[no_vars]} |
|
2189 | 287 |
|
2190 | 288 |
\noindent |
289 |
By unfolding the definition of relation composition and relation map |
|
290 |
we can see the equivalent statement just using the primitive list |
|
291 |
equivalence relation: |
|
292 |
||
293 |
@{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]} |
|
2189 | 294 |
|
2190 | 295 |
The statement reads that, for any lists of lists @{term a} and @{term b} |
296 |
if there exist intermediate lists of lists @{term "a'"} and @{term "b'"} |
|
297 |
such that each element of @{term a} is in the relation with an appropriate |
|
298 |
element of @{term a'}, @{term a'} is in relation with @{term b'} and each |
|
299 |
element of @{term b'} is in relation with the appropriate element of |
|
300 |
@{term b}. |
|
2189 | 301 |
|
302 |
*} |
|
303 |
||
304 |
subsection {* Preservation *} |
|
305 |
||
2190 | 306 |
text {* |
307 |
To be able to lift theorems that talk about constants that are not |
|
308 |
lifted but whose type changes when lifting is performed additionally |
|
309 |
preservation theorems are needed. |
|
2196
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
310 |
|
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
311 |
To lift theorems that talk about insertion in lists of lifted types |
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
312 |
we need to know that for any quotient type with the abstraction and |
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
313 |
representation functions @{text "Abs"} and @{text Rep} we have: |
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
314 |
|
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
315 |
@{thm [display] (concl) cons_prs[no_vars]} |
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
316 |
|
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
317 |
This is not enough to lift theorems that talk about quotient compositions. |
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
318 |
For some constants (for example empty list) it is possible to show a |
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
319 |
general compositional theorem, but for @{term "op #"} it is necessary |
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
320 |
to show that it respects the particular quotient type: |
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
321 |
|
74637f186af7
qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2195
diff
changeset
|
322 |
@{thm [display] insert_preserve2[no_vars]} |
2190 | 323 |
*} |
324 |
||
2191
8fdfbec54229
qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2190
diff
changeset
|
325 |
subsection {* Composition of Quotient theorems *} |
2189 | 326 |
|
2191
8fdfbec54229
qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2190
diff
changeset
|
327 |
text {* |
8fdfbec54229
qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2190
diff
changeset
|
328 |
Given two quotients, one of which quotients a container, and the |
8fdfbec54229
qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2190
diff
changeset
|
329 |
other quotients the type in the container, we can write the |
2193 | 330 |
composition of those quotients. To compose two quotient theorems |
2207 | 331 |
we compose the relations with relation composition as defined above |
332 |
and the abstraction and relation functions are the ones of the sub |
|
333 |
quotients composed with the usual function composition. |
|
334 |
The @{term "Rep"} and @{term "Abs"} functions that we obtain agree |
|
335 |
with the definition of aggregate Abs/Rep functions and the |
|
2193 | 336 |
relation is the same as the one given by aggregate relations. |
337 |
This becomes especially interesting |
|
2191
8fdfbec54229
qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2190
diff
changeset
|
338 |
when we compose the quotient with itself, as there is no simple |
8fdfbec54229
qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2190
diff
changeset
|
339 |
intermediate step. |
8fdfbec54229
qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2190
diff
changeset
|
340 |
|
2193 | 341 |
Lets take again the example of @{term concat}. To be able to lift |
2207 | 342 |
theorems that talk about it we provide the composition quotient |
343 |
theorems, which then lets us perform the lifting procedure in an |
|
344 |
unchanged way: |
|
2188 | 345 |
|
2190 | 346 |
@{thm [display] quotient_compose_list[no_vars]} |
2192 | 347 |
*} |
348 |
||
2191
8fdfbec54229
qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2190
diff
changeset
|
349 |
|
8fdfbec54229
qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2190
diff
changeset
|
350 |
section {* Lifting Theorems *} |
1978 | 351 |
|
2194
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
352 |
text {* |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
353 |
The core of the quotient package takes an original theorem that |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
354 |
talks about the raw types, and the statement of the theorem that |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
355 |
it is supposed to produce. This is different from other existing |
2207 | 356 |
quotient packages, where only the raw theorems were necessary. |
2194
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
357 |
We notice that in some cases only some occurrences of the raw |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
358 |
types need to be lifted. This is for example the case in the |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
359 |
new Nominal package, where a raw datatype that talks about |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
360 |
pairs of natural numbers or strings (being lists of characters) |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
361 |
should not be changed to a quotient datatype with constructors |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
362 |
taking integers or finite sets of characters. To simplify the |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
363 |
use of the quotient package we additionally provide an automated |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
364 |
statement translation mechanism that replaces occurrences of |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
365 |
types that match given quotients by appropriate lifted types. |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
366 |
|
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
367 |
Lifting the theorems is performed in three steps. In the following |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
368 |
we call these steps \emph{regularization}, \emph{injection} and |
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
369 |
\emph{cleaning} following the names used in Homeier's HOL |
2197 | 370 |
implementation. |
2193 | 371 |
|
2197 | 372 |
We first define the statement of the regularized theorem based |
373 |
on the original theorem and the goal theorem. Then we define |
|
374 |
the statement of the injected theorem, based on the regularized |
|
2208 | 375 |
theorem and the goal. We then show the 3 proofs, as all three |
2197 | 376 |
can be performed independently from each other. |
2193 | 377 |
|
2194
a52499e125ce
qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2193
diff
changeset
|
378 |
*} |
1994 | 379 |
|
2197 | 380 |
subsection {* Regularization and Injection statements *} |
1994 | 381 |
|
382 |
text {* |
|
2197 | 383 |
|
2207 | 384 |
We first define the function @{text REG}, which takes the statements |
385 |
of the raw theorem and the lifted theorem (both as terms) and |
|
386 |
returns the statement of the regularized version. The intuition |
|
387 |
behind this function is that it replaces quantifiers and |
|
388 |
abstractions involving raw types by bounded ones, and equalities |
|
389 |
involving raw types are replaced by appropriate aggregate |
|
390 |
relations. It is defined as follows: |
|
1994 | 391 |
|
2197 | 392 |
\begin{itemize} |
2198
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
393 |
\item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
394 |
\item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
395 |
\item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
396 |
\item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
2197 | 397 |
\item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"} |
398 |
\item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"} |
|
399 |
\item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"} |
|
2198
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
400 |
\item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
401 |
\item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"} |
2197 | 402 |
\end{itemize} |
1994 | 403 |
|
2207 | 404 |
In the above definition we ommited the cases for existential quantifiers |
405 |
and unique existential quantifiers, as they are very similar to the cases |
|
406 |
for the universal quantifier. |
|
2197 | 407 |
|
2207 | 408 |
Next we define the function @{text INJ} which takes the statement of |
409 |
the regularized theorems and the statement of the lifted theorem both as |
|
410 |
terms and returns the statment of the injected theorem: |
|
2198
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
411 |
|
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
412 |
\begin{itemize} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
413 |
\item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
414 |
\item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
415 |
\item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
416 |
\item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
417 |
\item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
418 |
\item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
419 |
\item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
420 |
\item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
421 |
\item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
422 |
\item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
423 |
\end{itemize} |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
424 |
|
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
425 |
For existential quantifiers and unique existential quantifiers it is |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
426 |
defined similarily to the universal one. |
8fe1a706ade7
qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2197
diff
changeset
|
427 |
|
2197 | 428 |
*} |
429 |
||
2208 | 430 |
subsection {* Proof procedure *} |
431 |
||
432 |
(* In the below the type-guiding 'QuotTrue' assumption is removed; since we |
|
433 |
present in a paper a version with typed-variables it is not necessary *) |
|
2197 | 434 |
|
435 |
text {* |
|
2208 | 436 |
|
437 |
With the above definitions of @{text "REG"} and @{text "INJ"} we can show |
|
438 |
how the proof is performed. The first step is always the application of |
|
439 |
of the following lemma: |
|
440 |
||
441 |
@{term "[|A; A --> B; B = C; C = D|] ==> D"} |
|
442 |
||
443 |
With @{text A} instantiated to the original raw theorem, |
|
444 |
@{text B} instantiated to @{text "REG(A)"}, |
|
445 |
@{text C} instantiated to @{text "INJ(REG(A))"}, |
|
446 |
and @{text D} instantiated to the statement of the lifted theorem. |
|
447 |
The first assumption can be immediately discharged using the original |
|
448 |
theorem and the three left subgoals are exactly the subgoals of regularization, |
|
449 |
injection and cleaning. The three can be proved independently by the |
|
450 |
framework and in case there are non-solved subgoals they can be left |
|
451 |
to the user. |
|
452 |
||
453 |
The injection and cleaning subgoals are always solved if the appropriate |
|
454 |
respectfulness and preservation theorems are given. It is not the case |
|
455 |
with regularization; sometimes a theorem given by the user does not |
|
456 |
imply a regularized version and a stronger one needs to be proved. This |
|
457 |
is outside of the scope of the quotient package, so the user is then left |
|
458 |
with such obligations. As an example lets see the simplest possible |
|
459 |
non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"} |
|
460 |
on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It |
|
461 |
only shows that particular items in the equivalence classes are not equal, |
|
462 |
a more general statement saying that the classes are not equal is necessary. |
|
463 |
*} |
|
464 |
||
465 |
subsection {* Proving Regularization *} |
|
466 |
||
467 |
text {* |
|
1994 | 468 |
|
2209
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
469 |
Isabelle provides a set of \emph{mono} rules, that are used to split implications |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
470 |
of similar statements into simpler implication subgoals. These are enchanced |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
471 |
with special quotient theorem in the regularization goal. Below we only show |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
472 |
the versions for the universal quantifier. For the existential quantifier |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
473 |
and abstraction they are analoguous with some symmetry. |
2199
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
474 |
|
2209
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
475 |
First, bounded universal quantifiers can be removed on the right: |
2199
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
476 |
|
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
477 |
@{thm [display] ball_reg_right[no_vars]} |
2206 | 478 |
|
2209
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
479 |
They can be removed anywhere if the relation is an equivalence relation: |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
480 |
|
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
481 |
@{thm [display] ball_reg_eqv[no_vars]} |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
482 |
|
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
483 |
And finally it can be removed anywhere if @{term R2} is an equivalence relation, then: |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
484 |
\[ |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
485 |
@{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]} |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
486 |
\] |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
487 |
|
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
488 |
The last theorem is new in comparison with Homeier's package; it allows separating |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
489 |
regularization from injection. |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
490 |
|
2206 | 491 |
*} |
492 |
||
493 |
(* |
|
2209
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
494 |
@{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) bex_reg_eqv_range[no_vars]} |
2199
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
495 |
@{thm [display] bex_reg_left[no_vars]} |
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
496 |
@{thm [display] bex1_bexeq_reg[no_vars]} |
2206 | 497 |
@{thm [display] bex_reg_eqv[no_vars]} |
2209
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
498 |
@{thm [display] babs_reg_eqv[no_vars]} |
5952b0f28261
Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2208
diff
changeset
|
499 |
@{thm [display] babs_simp[no_vars]} |
2206 | 500 |
*) |
1994 | 501 |
|
502 |
subsection {* Injection *} |
|
503 |
||
2199
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
504 |
text {* |
2211
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
505 |
The injection proof starts with an equality between the regularized theorem |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
506 |
and the injected version. The proof again follows by the structure of the |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
507 |
two term, and is defined for a goal being a relation between the two terms. |
2199
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
508 |
|
2211
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
509 |
\begin{itemize} |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
510 |
\item For two constants, an appropriate constant respectfullness assumption is used. |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
511 |
\item For two variables, the regularization assumptions state that they are related. |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
512 |
\item For two abstractions, they are eta-expanded and beta-reduced. |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
513 |
\end{itemize} |
2199
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
514 |
|
2211
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
515 |
Otherwise the two terms are applications. There are two cases: If there is a REP/ABS |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
516 |
in the injected theorem we can use the theorem: |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
517 |
|
2199
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
518 |
@{thm [display] rep_abs_rsp[no_vars]} |
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
519 |
|
2211
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
520 |
and continue the proof. |
2199
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
521 |
|
2211
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
522 |
Otherwise we introduce an appropriate relation between the subterms and continue with |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
523 |
two subgoals using the lemma: |
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
524 |
|
9d0673c319d1
qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2210
diff
changeset
|
525 |
@{thm [display] apply_rsp[no_vars]} |
2199
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
526 |
|
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
527 |
*} |
6ce64fb5cbd9
qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2198
diff
changeset
|
528 |
|
1994 | 529 |
subsection {* Cleaning *} |
530 |
||
2212
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
531 |
text {* |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
532 |
The @{text REG} and @{text INJ} functions have been defined in such a way |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
533 |
that establishing the goal theorem now consists only on rewriting the |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
534 |
injected theorem with the preservation theorems. |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
535 |
|
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
536 |
\begin{itemize} |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
537 |
\item First for lifted constants, their definitions are the preservation rules for |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
538 |
them. |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
539 |
\item For lambda abstractions lambda preservation establishes |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
540 |
the equality between the injected theorem and the goal. This allows both |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
541 |
abstraction and quantification over lifted types. |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
542 |
@{thm [display] lambda_prs[no_vars]} |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
543 |
\item Relations over lifted types are folded with: |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
544 |
@{thm [display] Quotient_rel_rep[no_vars]} |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
545 |
\item User given preservation theorems, that allow using higher level operations |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
546 |
and containers of types being lifted. An example may be |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
547 |
@{thm [display] map_prs(1)[no_vars]} |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
548 |
\end{itemize} |
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
549 |
|
79cebcc230d6
Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2211
diff
changeset
|
550 |
Preservation of relations and user given constant preservation lemmas *} |
1994 | 551 |
|
552 |
section {* Examples *} |
|
553 |
||
2210
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
554 |
(* Mention why equivalence *) |
2206 | 555 |
|
2210
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
556 |
text {* |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
557 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
558 |
A user of our quotient package first needs to define an equivalence relation: |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
559 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
560 |
@{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
561 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
562 |
Then the user defines a quotient type: |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
563 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
564 |
@{text "quotient_type int = (nat \<times> nat) / \<approx>"} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
565 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
566 |
Which leaves a proof obligation that the relation is an equivalence relation, |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
567 |
that can be solved with the automatic tactic with two definitions. |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
568 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
569 |
The user can then specify the constants on the quotient type: |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
570 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
571 |
@{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
572 |
@{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
573 |
@{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
574 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
575 |
Lets first take a simple theorem about addition on the raw level: |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
576 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
577 |
@{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
578 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
579 |
When the user tries to lift a theorem about integer addition, the respectfulness |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
580 |
proof obligation is left, so let us prove it first: |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
581 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
582 |
@{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
583 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
584 |
Can be proved automatically by the system just by unfolding the definition |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
585 |
of @{term "op \<Longrightarrow>"}. |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
586 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
587 |
Now the user can either prove a lifted lemma explicitely: |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
588 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
589 |
@{text "lemma 0 + i = i by lifting plus_zero_raw"} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
590 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
591 |
Or in this simple case use the automated translation mechanism: |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
592 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
593 |
@{text "thm plus_zero_raw[quot_lifted]"} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
594 |
|
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
595 |
obtaining the same result. |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
596 |
*} |
2206 | 597 |
|
1978 | 598 |
section {* Related Work *} |
599 |
||
600 |
text {* |
|
601 |
\begin{itemize} |
|
602 |
||
2152
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
603 |
\item Peter Homeier's package~\cite{Homeier05} (and related work from there) |
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
604 |
\item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems |
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
605 |
but only first order. |
1978 | 606 |
|
2152
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
607 |
\item PVS~\cite{PVS:Interpretations} |
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
608 |
\item MetaPRL~\cite{Nogin02} |
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
609 |
\item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type, |
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
610 |
Dixon's FSet, \ldots) |
1978 | 611 |
|
612 |
\item Oscar Slotosch defines quotient-type automatically but no |
|
2152
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
613 |
lifting~\cite{Slotosch97}. |
1978 | 614 |
|
615 |
\item PER. And how to avoid it. |
|
616 |
||
2152
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
617 |
\item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06} |
1978 | 618 |
|
2152
d7d4491535a9
starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2103
diff
changeset
|
619 |
\item Setoids in Coq and \cite{ChicliPS02} |
1978 | 620 |
|
621 |
\end{itemize} |
|
622 |
*} |
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
623 |
|
2210
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
624 |
section {* Conclusion *} |
6aaec9dd0c62
qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2209
diff
changeset
|
625 |
|
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
626 |
(*<*) |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
627 |
end |
1978 | 628 |
(*>*) |