218 alpha-equivalence classes according to our alpha-equivalence relation and |
218 alpha-equivalence classes according to our alpha-equivalence relation and |
219 then define the new type as these alpha-equivalence classes. The construction we |
219 then define the new type as these alpha-equivalence classes. The construction we |
220 can perform in HOL is illustrated by the following picture: |
220 can perform in HOL is illustrated by the following picture: |
221 |
221 |
222 \begin{center} |
222 \begin{center} |
223 figure |
223 \begin{tikzpicture} |
224 %\begin{pspicture}(0.5,0.0)(8,2.5) |
224 %\draw[step=2mm] (-4,-1) grid (4,1); |
|
225 |
|
226 \draw[very thick] (0.7,0.4) circle (4.25mm); |
|
227 \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9); |
|
228 \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05); |
|
229 |
|
230 \draw (-2.0, 0.845) -- (0.7,0.845); |
|
231 \draw (-2.0,-0.045) -- (0.7,-0.045); |
|
232 |
|
233 \draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}}; |
|
234 \draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}}; |
|
235 \draw (1.8, 0.48) node[right=-0.1mm] |
|
236 {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}}; |
|
237 \draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}}; |
|
238 \draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}}; |
|
239 |
|
240 \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3); |
|
241 \draw (-0.95, 0.3) node[above=0mm] {isomorphism}; |
|
242 |
|
243 %\rput(3.7,1.75){isomorphism} |
|
244 \end{tikzpicture} |
|
245 |
|
246 %%\begin{pspicture}(0.5,0.0)(8,2.5) |
225 %%\showgrid |
247 %%\showgrid |
226 %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5) |
248 %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5) |
227 %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6} |
249 %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6} |
228 %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9) |
250 %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9) |
229 |
251 |
253 {\bf Contributions:} We provide new definitions for when terms |
275 {\bf Contributions:} We provide new definitions for when terms |
254 involving multiple binders are alpha-equivalent. These definitions are |
276 involving multiple binders are alpha-equivalent. These definitions are |
255 inspired by earlier work of Pitts \cite{}. By means of automatic |
277 inspired by earlier work of Pitts \cite{}. By means of automatic |
256 proofs, we establish a reasoning infrastructure for alpha-equated |
278 proofs, we establish a reasoning infrastructure for alpha-equated |
257 terms, including properties about support, freshness and equality |
279 terms, including properties about support, freshness and equality |
258 conditions for alpha-equated terms. We will also derive for these |
280 conditions for alpha-equated terms. We re also able to derive, at the moment |
259 terms a strong induction principle that has the variable convention |
281 only manually, for these terms a strong induction principle that |
260 already built in. |
282 has the variable convention already built in. |
261 *} |
283 *} |
262 |
284 |
263 section {* A Short Review of the Nominal Logic Work *} |
285 section {* A Short Review of the Nominal Logic Work *} |
264 |
286 |
265 text {* |
287 text {* |