10 (*>*) |
10 (*>*) |
11 |
11 |
12 section {* Introduction *} |
12 section {* Introduction *} |
13 |
13 |
14 text {* |
14 text {* |
|
15 {\hfill quote by Larry}\bigskip |
|
16 |
|
17 \noindent |
15 Isabelle is a generic theorem prover in which many logics can be implemented. |
18 Isabelle is a generic theorem prover in which many logics can be implemented. |
16 The most widely used one, however, is |
19 The most widely used one, however, is |
17 Higher-Order Logic (HOL). This logic consists of a small number of |
20 Higher-Order Logic (HOL). This logic consists of a small number of |
18 axioms and inference |
21 axioms and inference |
19 rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted |
22 rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted |
25 the type @{typ "nat \<times> nat"} and the equivalence relation |
28 the type @{typ "nat \<times> nat"} and the equivalence relation |
26 |
29 |
27 @{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"} |
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"} |
28 |
31 |
29 \noindent |
32 \noindent |
30 The problem is that one |
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. |
31 |
50 |
|
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"}: |
32 |
55 |
|
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"} |
33 |
62 |
|
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. |
34 *} |
67 *} |
35 |
68 |
36 subsection {* Contributions *} |
69 subsection {* Contributions *} |
37 |
70 |
38 text {* |
71 text {* |