12 "op -->" (infix "\<rightarrow>" 100) and |
12 "op -->" (infix "\<rightarrow>" 100) and |
13 "==>" (infix "\<Rightarrow>" 100) and |
13 "==>" (infix "\<Rightarrow>" 100) and |
14 fun_map (infix "\<longrightarrow>" 51) and |
14 fun_map (infix "\<longrightarrow>" 51) and |
15 fun_rel (infix "\<Longrightarrow>" 51) and |
15 fun_rel (infix "\<Longrightarrow>" 51) and |
16 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) |
16 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) |
17 fempty ("\<emptyset>\<^isub>f") and |
17 fempty ("\<emptyset>") and |
18 funion ("_ \<union>\<^isub>f _") and |
18 funion ("_ \<union> _") and |
19 finsert ("{_} \<union>\<^isub>f _") and |
19 finsert ("{_} \<union> _") and |
20 Cons ("_::_") and |
20 Cons ("_::_") and |
21 concat ("flat") and |
21 concat ("flat") and |
22 fconcat ("fset'_flat") |
22 fconcat ("\<Union>") |
23 |
23 |
24 |
24 |
25 |
25 |
26 ML {* |
26 ML {* |
27 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
27 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
56 (HOL). This logic consists of a small number of axioms and inference rules |
56 (HOL). This logic consists of a small number of axioms and inference rules |
57 over a simply-typed term-language. Safe reasoning in HOL is ensured by two |
57 over a simply-typed term-language. Safe reasoning in HOL is ensured by two |
58 very restricted mechanisms for extending the logic: one is the definition of |
58 very restricted mechanisms for extending the logic: one is the definition of |
59 new constants in terms of existing ones; the other is the introduction of |
59 new constants in terms of existing ones; the other is the introduction of |
60 new types by identifying non-empty subsets in existing types. It is well |
60 new types by identifying non-empty subsets in existing types. It is well |
61 understood how to use both mechanisms for dealing with many quotient |
61 understood how to use both mechanisms for dealing with quotient |
62 constructions in HOL (see \cite{Homeier05,Paulson06}). For example the |
62 constructions in HOL (see \cite{Homeier05,Paulson06}). For example the |
63 integers in Isabelle/HOL are constructed by a quotient construction over the |
63 integers in Isabelle/HOL are constructed by a quotient construction over the |
64 type @{typ "nat \<times> nat"} and the equivalence relation |
64 type @{typ "nat \<times> nat"} and the equivalence relation |
65 |
65 |
66 @{text [display, indent=10] "(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"} |
66 @{text [display, indent=10] "(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"} |
72 such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in |
72 such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in |
73 terms of operations on pairs of natural numbers (namely @{text |
73 terms of operations on pairs of natural numbers (namely @{text |
74 "add\<^bsub>nat\<times>nat\<^esub> (n\<^isub>1, m\<^isub>1) (n\<^isub>2, |
74 "add\<^bsub>nat\<times>nat\<^esub> (n\<^isub>1, m\<^isub>1) (n\<^isub>2, |
75 m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}). |
75 m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}). |
76 Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"}, |
76 Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"}, |
77 by quotienting @{text "\<alpha> list"} according to the equivalence relation |
77 by quotienting the type @{text "\<alpha> list"} according to the equivalence relation |
78 |
78 |
79 @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
79 @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} |
80 |
80 |
81 \noindent |
81 \noindent |
82 which states that two lists are equivalent if every element in one list is also |
82 which states that two lists are equivalent if every element in one list is also |
83 member in the other (@{text "\<in>"} stands here for membership in lists). The |
83 member in the other (@{text "\<in>"} stands here for membership in lists). The |
84 empty finite set, written @{term "{||}"}, can then be defined as the |
84 empty finite set, written @{term "{||}"}, can then be defined as the |
85 empty list and the union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append. |
85 empty list and the union of two finite sets, written @{text "\<union>"}, as list append. |
86 |
86 |
87 An area where quotients are ubiquitous is reasoning about programming language |
87 An area where quotients are ubiquitous is reasoning about programming language |
88 calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as |
88 calculi. A simple example is the lambda-calculus, whose ``raw'' terms are defined as |
89 |
89 |
90 @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"} |
90 @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"} |
94 prove formally, for example, the substitution lemma \cite{Barendregt81} by induction |
94 prove formally, for example, the substitution lemma \cite{Barendregt81} by induction |
95 over the structure of terms. This can be fiendishly complicated (see |
95 over the structure of terms. This can be fiendishly complicated (see |
96 \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof |
96 \cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof |
97 about ``raw'' lambda-terms). In contrast, if we reason about |
97 about ``raw'' lambda-terms). In contrast, if we reason about |
98 $\alpha$-equated lambda-terms, that means terms quotient according to |
98 $\alpha$-equated lambda-terms, that means terms quotient according to |
99 $\alpha$-equivalence, then the reasoning infrastructure provided by, |
99 $\alpha$-equivalence, then the reasoning infrastructure provided, |
100 for example, Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal |
100 for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal |
101 proof of the substitution lemma almost trivial. |
101 proof of the substitution lemma almost trivial. |
102 |
102 |
103 The difficulty is that in order to be able to reason about integers, finite |
103 The difficulty is that in order to be able to reason about integers, finite |
104 sets or $\alpha$-equated lambda-terms one needs to establish a reasoning |
104 sets or $\alpha$-equated lambda-terms one needs to establish a reasoning |
105 infrastructure by transferring, or \emph{lifting}, definitions and theorems |
105 infrastructure by transferring, or \emph{lifting}, definitions and theorems |
106 from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int} |
106 from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int} |
107 (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting |
107 (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting |
108 usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}. |
108 usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}. |
109 It is feasible to to this work manually if one has only a few quotient |
109 It is feasible to to this work manually, if one has only a few quotient |
110 constructions, but if they have to be done over and over again as in |
110 constructions at hand. But if they have to be done over and over again as in |
111 Nominal Isabelle, then manual reasoning is not an option. |
111 Nominal Isabelle, then manual reasoning is not an option. |
112 |
112 |
113 The purpose of a \emph{quotient package} is to ease the lifting and automate |
113 The purpose of a \emph{quotient package} is to ease the lifting of theorems |
114 the reasoning as much as possible. In the context of HOL, there have been |
114 and automate the definitions and reasoning as much as possible. In the |
115 a few quotient packages already \cite{harrison-thesis,Slotosch97}. The |
115 context of HOL, there have been a few quotient packages already |
116 most notable is the one by Homeier \cite{Homeier05} implemented in HOL4. |
116 \cite{harrison-thesis,Slotosch97}. The most notable is the one by Homeier |
117 The fundamental construction these quotient packages perform can be |
117 \cite{Homeier05} implemented in HOL4. The fundamental construction these |
118 illustrated by the following picture: |
118 quotient packages perform can be illustrated by the following picture: |
119 |
119 |
120 \begin{center} |
120 \begin{center} |
121 \mbox{}\hspace{20mm}\begin{tikzpicture} |
121 \mbox{}\hspace{20mm}\begin{tikzpicture} |
122 %%\draw[step=2mm] (-4,-1) grid (4,1); |
122 %%\draw[step=2mm] (-4,-1) grid (4,1); |
123 |
123 |
141 |
141 |
142 \end{tikzpicture} |
142 \end{tikzpicture} |
143 \end{center} |
143 \end{center} |
144 |
144 |
145 \noindent |
145 \noindent |
146 The starting point is an existing type over which a user-given equivalence |
146 The starting point is an existing type over which an equivalence relation |
147 relation is defined. With this input, the package introduces a new type, |
147 given by the user is defined. With this input the package introduces a new |
148 which comes with two associated abstraction and representation functions, written |
148 type, which comes with two associated abstraction and representation |
149 @{text Abs} and @{text Rep}. They relate elements in the existing and new |
149 functions, written @{text Abs} and @{text Rep}. These functions relate |
150 type and can be uniquely identified by their type (which however we omit for |
150 elements in the existing and new type, and can be uniquely identified by |
151 better readability). These two function represent an isomorphism between |
151 their type (which however we often omit for better readability). They |
152 the non-empty subset and the new type. They are necessary making definitions |
152 represent an isomorphism between the non-empty subset and elements in the |
153 over the new type. For example @{text "0"} and @{text "1"} |
153 new type. They are necessary for making definitions involving the new type. For |
154 of type @{typ int} can be defined as |
154 example @{text "0"} and @{text "1"} of type @{typ int} can be defined as |
155 |
155 |
156 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
156 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
157 @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"} |
157 @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"} |
158 \end{isabelle} |
158 \end{isabelle} |
159 |
159 |
166 \noindent |
166 \noindent |
167 where we have to take first the representation of @{text n} and @{text m}, |
167 where we have to take first the representation of @{text n} and @{text m}, |
168 add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the |
168 add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the |
169 abstraction of the result. This is all straightforward and the existing |
169 abstraction of the result. This is all straightforward and the existing |
170 quotient packages can deal with such definitions. But what is surprising |
170 quotient packages can deal with such definitions. But what is surprising |
171 that none of them can deal with more complicated definitions involving |
171 that none of them can deal with slightly more complicated definitions involving |
172 \emph{compositions} of quotients. Such compositions are needed for example |
172 \emph{compositions} of quotients. Such compositions are needed for example |
173 in case of finite sets. There one would like to have a corresponding definition |
173 in case of finite sets. For example over lists one can define an operator |
174 for finite sets for the operator @{term "concat"} defined over lists. This |
174 that flattens lists of lists as follows |
175 operator flattens lists of lists as follows |
|
176 |
175 |
177 @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]} |
176 @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]} |
178 |
177 |
179 \noindent |
178 \noindent |
180 We expect that the corresponding operator on finite sets, written @{term "fconcat"}, |
179 We expect that the corresponding operator on finite sets, written @{term "fconcat"}, |
181 behaves as follows: |
180 behaves as follows: |
182 |
181 |
183 @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]} |
182 @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]} |
184 |
183 |
185 \noindent |
184 \noindent |
186 The problem is that we want to quotient lists to obtain finite sets and |
185 The quotient package should provide us with a definition for @{text "\<Union>"} in |
187 @{term concat} is of type @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}. We expect |
186 terms of @{text flat}, @{text Rep} and @{text Abs}. The problem is that it |
188 that @{term "fconcat"} has type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. But |
187 is not enough to just take the representation of the argument and then |
189 what should its definition be? It is not possible to just take the representation |
188 take the abstraction of the result, because in that case we obtain an operator |
190 of the argument and then take the abstraction of the result of flattening |
189 with type @{text "(\<alpha> list) fset \<Rightarrow> \<alpha> fset"}, not the expected |
191 the resulting list. The problem is that a single @{text "Rep"} only gives |
190 @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. It turns out that we need |
192 us lists of finite sets, not lists of lists. It turns out that we need |
191 to build aggregate representation and abstraction functions, which in |
193 to be able to build aggregate representation and abstraction function, which in |
|
194 case of @{term "fconcat"} produce the following definition |
192 case of @{term "fconcat"} produce the following definition |
195 |
193 |
196 @{text [display, indent=10] "fset_flat S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"} |
194 @{text [display, indent=10] "\<Union> S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"} |
197 |
195 |
198 \noindent |
196 \noindent |
199 where @{term map} is the usual mapping function for lists. |
197 where @{term map} is the usual mapping function for lists. In this paper we |
|
198 will present a formal definition for our aggregate abstraction and |
|
199 representation functions (this definition was omitted in \cite{Homeier05}). |
|
200 They generate definitions like the one above for @{text add} and @{text "\<Union>"} |
|
201 according to the type of the ``raw'' constant and the type |
|
202 of the quotient constant. |
|
203 |
200 |
204 |
201 *} |
205 *} |
202 |
206 |
203 subsection {* Contributions *} |
207 subsection {* Contributions *} |
204 |
208 |