97 $\alpha$-equivalence, then the reasoning infrastructure provided by, |
99 $\alpha$-equivalence, then the reasoning infrastructure provided by, |
98 for example, Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal |
100 for example, Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal |
99 proof of the substitution lemma almost trivial. |
101 proof of the substitution lemma almost trivial. |
100 |
102 |
101 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 |
102 sets and $\alpha$-equated lambda-terms one needs to establish a reasoning |
104 sets or $\alpha$-equated lambda-terms one needs to establish a reasoning |
103 infrastructure by transferring, or \emph{lifting}, definitions and theorems |
105 infrastructure by transferring, or \emph{lifting}, definitions and theorems |
104 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} |
105 (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting |
107 (similarly for finite sets and $\alpha$-equated lambda-terms). This lifting |
106 usually requires a \emph{lot} of tedious reasoning effort. The purpose of a |
108 usually requires a \emph{lot} of tedious reasoning effort. |
107 \emph{quotient package} is to ease the lifting and automate the reasoning as |
109 |
108 much as possible. |
110 The purpose of a \emph{quotient package} is to ease the lifting and automate |
|
111 the reasoning as much as possible. In the context of HOL, there have been |
|
112 several quotient packages (...). The most notable is the one by Homeier |
|
113 (...) implemented in HOL4. The fundamental construction the quotient |
|
114 package performs can be illustrated by the following picture: |
109 |
115 |
110 \begin{center} |
116 \begin{center} |
111 \mbox{}\hspace{20mm}\begin{tikzpicture} |
117 \mbox{}\hspace{20mm}\begin{tikzpicture} |
112 %%\draw[step=2mm] (-4,-1) grid (4,1); |
118 %%\draw[step=2mm] (-4,-1) grid (4,1); |
113 |
119 |
124 {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}}; |
130 {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}}; |
125 \draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}}; |
131 \draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}}; |
126 |
132 |
127 \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36); |
133 \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36); |
128 \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16); |
134 \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16); |
129 \draw (-0.95, 0.26) node[above=0.4mm] {Rep}; |
135 \draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}}; |
130 \draw (-0.95, 0.26) node[below=0.4mm] {Abs}; |
136 \draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}}; |
131 |
137 |
132 \end{tikzpicture} |
138 \end{tikzpicture} |
133 \end{center} |
139 \end{center} |
134 |
140 |
135 |
141 \noindent |
136 In the context of HOL, there have been several quotient packages (...). The |
142 The starting point is an existing type over which a user-given equivalence |
137 most notable is the one by Homeier (...) implemented in HOL4. However, what is |
143 relation is defined. With this input, the package introduces a new type, |
138 surprising, none of them can deal compositions of quotients, for example with |
144 which comes with two associated abstraction and representation functions, |
139 lifting theorems about @{text "concat"}: |
145 @{text Abs} and @{text Rep}, that relate elements in the existing and new |
|
146 type. These two function represent an isomorphism between the non-empty |
|
147 subset and the new type. |
|
148 |
|
149 The abstractions and representation functions are important for defining |
|
150 concepts involving the new type. For example @{text "0"} and @{text "1"} |
|
151 of type @{typ int} can be defined as |
|
152 |
|
153 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
154 @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"} |
|
155 \end{isabelle} |
|
156 |
|
157 \noindent |
|
158 Slightly more complicated is the definition of @{text "add"} with type |
|
159 @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition looks as follows |
|
160 |
|
161 @{text [display, indent=10] "add x y \<equiv> Abs (add\<^bsub>nat\<times>nat\<^esub> (Rep x) (Rep y))"} |
|
162 |
|
163 \noindent |
|
164 where we have to take first the representation of @{text x} and @{text y}, |
|
165 add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the |
|
166 abstraction of the result. This is all straightforward and the existing |
|
167 quotient packages can deal with such definitions. But what is surprising |
|
168 that none of them can deal with more complicated definitions involving |
|
169 \emph{compositions} of quotients. Such compositions are needed for example |
|
170 when quotienting finite lists (@{text "\<alpha> list"}) to yield finite sets |
|
171 (@{text "\<alpha> fset"}). There one would like to have a corresponding definition |
|
172 for the operator @{term "concat"}, which flattens lists of lists as follows |
140 |
173 |
141 @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]} |
174 @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]} |
142 |
175 |
143 \noindent |
176 \noindent |
144 One would like to lift this definition to the operation: |
177 We expect that the corresponding operator on finite sets, written @{term "fconcat"}, |
|
178 behaves as follows: |
145 |
179 |
146 @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]} |
180 @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]} |
147 |
181 |
148 \noindent |
182 \noindent |
149 What is special about this operation is that we have as input |
183 The problem is that we want to quotient lists to obtain finite sets and |
150 lists of lists which after lifting turn into finite sets of finite |
184 @{term concat} is of type @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}. We expect |
151 sets. |
185 that @{term "fconcat"} has type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. But |
|
186 what should its definition be? It is not possible to just take the representation |
|
187 of the argument and then take the abstraction of the result of flattening |
|
188 the resulting list. The problem is that a single @{text "Rep"} only gives |
|
189 us lists of finite sets, not lists of lists. It turns out that we need |
|
190 to be able to build aggregate representation and abstraction function, which in |
|
191 case of @{term "fconcat"} produce the following definition |
|
192 |
|
193 @{text [display, indent=10] "fset_flat S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"} |
|
194 |
|
195 \noindent |
|
196 where @{term map} is the usual mapping function for lists. |
|
197 |
152 *} |
198 *} |
153 |
199 |
154 subsection {* Contributions *} |
200 subsection {* Contributions *} |
155 |
201 |
156 text {* |
202 text {* |