equal
deleted
inserted
replaced
132 |
132 |
133 The procedure. |
133 The procedure. |
134 |
134 |
135 Example of non-regularizable theorem ($0 = 1$). |
135 Example of non-regularizable theorem ($0 = 1$). |
136 |
136 |
137 New regularization lemmas: |
137 Separtion of regularization from injection thanks to the following 2 lemmas: |
138 \begin{lemma} |
138 \begin{lemma} |
139 If @{term R2} is an equivalence relation, then: |
139 If @{term R2} is an equivalence relation, then: |
140 \begin{eqnarray} |
140 \begin{eqnarray} |
141 @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\ |
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]} |
142 @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]} |
157 section {* Related Work *} |
157 section {* Related Work *} |
158 |
158 |
159 text {* |
159 text {* |
160 \begin{itemize} |
160 \begin{itemize} |
161 |
161 |
162 \item Peter Homeier's package (and related work from there), John |
162 \item Peter Homeier's package~\cite{Homeier05} (and related work from there) |
163 Harrison's one. |
163 \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems |
|
164 but only first order. |
164 |
165 |
165 \item Manually defined quotients in Isabelle/HOL Library (Larry's |
166 \item PVS~\cite{PVS:Interpretations} |
166 quotients, Markus's Quotient\_Type, Dixon's FSet, \ldots) |
167 \item MetaPRL~\cite{Nogin02} |
|
168 \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type, |
|
169 Dixon's FSet, \ldots) |
167 |
170 |
168 \item Oscar Slotosch defines quotient-type automatically but no |
171 \item Oscar Slotosch defines quotient-type automatically but no |
169 lifting. |
172 lifting~\cite{Slotosch97}. |
170 |
173 |
171 \item PER. And how to avoid it. |
174 \item PER. And how to avoid it. |
172 |
175 |
173 \item Necessity of Hilbert Choice op. |
176 \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06} |
174 |
177 |
175 \item Setoids in Coq |
178 \item Setoids in Coq and \cite{ChicliPS02} |
176 |
179 |
177 \end{itemize} |
180 \end{itemize} |
178 *} |
181 *} |
179 |
182 |
180 (*<*) |
183 (*<*) |