313 following the structure of the theorem being lifted and the theorem |
313 following the structure of the theorem being lifted and the theorem |
314 on the quotient level. Space constraints, unfortunately, allow us to only |
314 on the quotient level. Space constraints, unfortunately, allow us to only |
315 sketch this part of our work in Section 5 and we defer the reader to a longer |
315 sketch this part of our work in Section 5 and we defer the reader to a longer |
316 version for the details. However, we will give in Section 3 and 4 all |
316 version for the details. However, we will give in Section 3 and 4 all |
317 definitions that specify the input and output data of our three-step |
317 definitions that specify the input and output data of our three-step |
318 lifting procedure. Section 6 gives an example how our quotient package |
318 lifting procedure. |
319 works in practise. |
319 %Appendix A gives an example how our quotient package works in practise. |
320 *} |
320 *} |
321 |
321 |
322 section {* Preliminaries and General\\ Quotients\label{sec:prelims} *} |
322 section {* Preliminaries and General\\ Quotients\label{sec:prelims} *} |
323 |
323 |
324 text {* |
324 text {* |
1177 |
1177 |
1178 %Finally, we rewrite with the preservation theorems. This will result |
1178 %Finally, we rewrite with the preservation theorems. This will result |
1179 %in two equal terms that can be solved by reflexivity. |
1179 %in two equal terms that can be solved by reflexivity. |
1180 *} |
1180 *} |
1181 |
1181 |
1182 |
|
1183 section {* Examples \label{sec:examples} *} |
|
1184 |
|
1185 text {* |
|
1186 |
|
1187 %%% FIXME Reviewer 1 would like an example of regularized and injected |
|
1188 %%% statements. He asks for the examples twice, but I would still ignore |
|
1189 %%% it due to lack of space... |
|
1190 |
|
1191 \noindent |
|
1192 In this section we will show a sequence of declarations for defining the |
|
1193 type of integers by quotienting pairs of natural numbers, and |
|
1194 lifting one theorem. |
|
1195 |
|
1196 A user of our quotient package first needs to define a relation on |
|
1197 the raw type with which the quotienting will be performed. We give |
|
1198 the same integer relation as the one presented in \eqref{natpairequiv}: |
|
1199 |
|
1200 \begin{isabelle}\ \ \ \ \ % |
|
1201 \begin{tabular}{@ {}l} |
|
1202 \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\ |
|
1203 \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"} |
|
1204 \end{tabular} |
|
1205 \end{isabelle} |
|
1206 |
|
1207 \noindent |
|
1208 Next the quotient type must be defined. This generates a proof obligation that the |
|
1209 relation is an equivalence relation, which is solved automatically using the |
|
1210 definition of equivalence and extensionality: |
|
1211 |
|
1212 \begin{isabelle}\ \ \ \ \ % |
|
1213 \begin{tabular}{@ {}l} |
|
1214 \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\ |
|
1215 \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"} |
|
1216 \end{tabular} |
|
1217 \end{isabelle} |
|
1218 |
|
1219 \noindent |
|
1220 The user can then specify the constants on the quotient type: |
|
1221 |
|
1222 \begin{isabelle}\ \ \ \ \ % |
|
1223 \begin{tabular}{@ {}l} |
|
1224 \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm] |
|
1225 \isacommand{fun}~~@{text "add_pair"}\\ |
|
1226 \isacommand{where}~~% |
|
1227 @{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\ |
|
1228 \isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~% |
|
1229 \isacommand{is}~~@{text "add_pair"}\\ |
|
1230 \end{tabular} |
|
1231 \end{isabelle} |
|
1232 |
|
1233 \noindent |
|
1234 The following theorem about addition on the raw level can be proved. |
|
1235 |
|
1236 \begin{isabelle}\ \ \ \ \ % |
|
1237 \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"} |
|
1238 \end{isabelle} |
|
1239 |
|
1240 \noindent |
|
1241 If the user lifts this theorem, the quotient package performs all the lifting |
|
1242 automatically leaving the respectfulness proof for the constant @{text "add_pair"} |
|
1243 as the only remaining proof obligation. This property needs to be proved by the user: |
|
1244 |
|
1245 \begin{isabelle}\ \ \ \ \ % |
|
1246 \begin{tabular}{@ {}l} |
|
1247 \isacommand{lemma}~~@{text "[quot_respect]:"}\\ |
|
1248 @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"} |
|
1249 \end{tabular} |
|
1250 \end{isabelle} |
|
1251 |
|
1252 \noindent |
|
1253 It can be discharged automatically by Isabelle when hinting to unfold the definition |
|
1254 of @{text "\<doublearr>"}. |
|
1255 After this, the user can prove the lifted lemma as follows: |
|
1256 |
|
1257 \begin{isabelle}\ \ \ \ \ % |
|
1258 \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"} |
|
1259 \end{isabelle} |
|
1260 |
|
1261 \noindent |
|
1262 or by using the completely automated mode stating just: |
|
1263 |
|
1264 \begin{isabelle}\ \ \ \ \ % |
|
1265 \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"} |
|
1266 \end{isabelle} |
|
1267 |
|
1268 \noindent |
|
1269 Both methods give the same result, namely @{text "0 + x = x"} |
|
1270 where @{text x} is of type integer. |
|
1271 Although seemingly simple, arriving at this result without the help of a quotient |
|
1272 package requires a substantial reasoning effort (see \cite{Paulson06}). |
|
1273 *} |
|
1274 |
|
1275 section {* Conclusion and Related Work\label{sec:conc}*} |
1182 section {* Conclusion and Related Work\label{sec:conc}*} |
1276 |
1183 |
1277 text {* |
1184 text {* |
1278 |
1185 |
1279 \noindent |
1186 \noindent |
1335 {\bf Acknowledgements:} We would like to thank Peter Homeier for the many |
1242 {\bf Acknowledgements:} We would like to thank Peter Homeier for the many |
1336 discussions about his HOL4 quotient package and explaining to us |
1243 discussions about his HOL4 quotient package and explaining to us |
1337 some of its finer points in the implementation. Without his patient |
1244 some of its finer points in the implementation. Without his patient |
1338 help, this work would have been impossible. |
1245 help, this work would have been impossible. |
1339 |
1246 |
|
1247 % \appendix |
|
1248 |
1340 *} |
1249 *} |
1341 |
1250 |
|
1251 (* section {* Examples \label{sec:examples} *} |
|
1252 |
|
1253 text {* |
|
1254 |
|
1255 %%% FIXME Reviewer 1 would like an example of regularized and injected |
|
1256 %%% statements. He asks for the examples twice, but I would still ignore |
|
1257 %%% it due to lack of space... |
|
1258 |
|
1259 \noindent |
|
1260 In this appendix we will show a sequence of declarations for defining the |
|
1261 type of integers by quotienting pairs of natural numbers, and |
|
1262 lifting one theorem. |
|
1263 |
|
1264 A user of our quotient package first needs to define a relation on |
|
1265 the raw type with which the quotienting will be performed. We give |
|
1266 the same integer relation as the one presented in \eqref{natpairequiv}: |
|
1267 |
|
1268 \begin{isabelle}\ \ \ \ \ % |
|
1269 \begin{tabular}{@ {}l} |
|
1270 \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\ |
|
1271 \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"} |
|
1272 \end{tabular} |
|
1273 \end{isabelle} |
|
1274 |
|
1275 \noindent |
|
1276 Next the quotient type must be defined. This generates a proof obligation that the |
|
1277 relation is an equivalence relation, which is solved automatically using the |
|
1278 definition of equivalence and extensionality: |
|
1279 |
|
1280 \begin{isabelle}\ \ \ \ \ % |
|
1281 \begin{tabular}{@ {}l} |
|
1282 \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\ |
|
1283 \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"} |
|
1284 \end{tabular} |
|
1285 \end{isabelle} |
|
1286 |
|
1287 \noindent |
|
1288 The user can then specify the constants on the quotient type: |
|
1289 |
|
1290 \begin{isabelle}\ \ \ \ \ % |
|
1291 \begin{tabular}{@ {}l} |
|
1292 \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm] |
|
1293 \isacommand{fun}~~@{text "add_pair"}\\ |
|
1294 \isacommand{where}~~% |
|
1295 @{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\ |
|
1296 \isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~% |
|
1297 \isacommand{is}~~@{text "add_pair"}\\ |
|
1298 \end{tabular} |
|
1299 \end{isabelle} |
|
1300 |
|
1301 \noindent |
|
1302 The following theorem about addition on the raw level can be proved. |
|
1303 |
|
1304 \begin{isabelle}\ \ \ \ \ % |
|
1305 \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"} |
|
1306 \end{isabelle} |
|
1307 |
|
1308 \noindent |
|
1309 If the user lifts this theorem, the quotient package performs all the lifting |
|
1310 automatically leaving the respectfulness proof for the constant @{text "add_pair"} |
|
1311 as the only remaining proof obligation. This property needs to be proved by the user: |
|
1312 |
|
1313 \begin{isabelle}\ \ \ \ \ % |
|
1314 \begin{tabular}{@ {}l} |
|
1315 \isacommand{lemma}~~@{text "[quot_respect]:"}\\ |
|
1316 @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"} |
|
1317 \end{tabular} |
|
1318 \end{isabelle} |
|
1319 |
|
1320 \noindent |
|
1321 It can be discharged automatically by Isabelle when hinting to unfold the definition |
|
1322 of @{text "\<doublearr>"}. |
|
1323 After this, the user can prove the lifted lemma as follows: |
|
1324 |
|
1325 \begin{isabelle}\ \ \ \ \ % |
|
1326 \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"} |
|
1327 \end{isabelle} |
|
1328 |
|
1329 \noindent |
|
1330 or by using the completely automated mode stating just: |
|
1331 |
|
1332 \begin{isabelle}\ \ \ \ \ % |
|
1333 \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"} |
|
1334 \end{isabelle} |
|
1335 |
|
1336 \noindent |
|
1337 Both methods give the same result, namely @{text "0 + x = x"} |
|
1338 where @{text x} is of type integer. |
|
1339 Although seemingly simple, arriving at this result without the help of a quotient |
|
1340 package requires a substantial reasoning effort (see \cite{Paulson06}). |
|
1341 *} |
|
1342 *) |
1342 |
1343 |
1343 |
1344 |
1344 (*<*) |
1345 (*<*) |
1345 end |
1346 end |
1346 (*>*) |
1347 (*>*) |