equal
deleted
inserted
replaced
58 section {* Introduction *} |
58 section {* Introduction *} |
59 |
59 |
60 text {* |
60 text {* |
61 |
61 |
62 So far, Nominal Isabelle provided a mechanism for constructing |
62 So far, Nominal Isabelle provided a mechanism for constructing |
63 $\alpha$-equated terms, for example lambda-terms |
63 $\alpha$-equated terms, for example lambda-terms, |
64 % |
64 @{text "t ::= x | t t | \<lambda>x. t"}, |
65 \begin{center} |
|
66 @{text "t ::= x | t t | \<lambda>x. t"} |
|
67 \end{center} |
|
68 % |
|
69 \noindent |
|
70 where free and bound variables have names. For such $\alpha$-equated terms, |
65 where free and bound variables have names. For such $\alpha$-equated terms, |
71 Nominal Isabelle derives automatically a reasoning infrastructure that has |
66 Nominal Isabelle derives automatically a reasoning infrastructure that has |
72 been used successfully in formalisations of an equivalence checking |
67 been used successfully in formalisations of an equivalence checking |
73 algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed |
68 algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed |
74 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
69 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
81 the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are, |
76 the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are, |
82 respectively, of the form |
77 respectively, of the form |
83 % |
78 % |
84 \begin{equation}\label{tysch} |
79 \begin{equation}\label{tysch} |
85 \begin{array}{l} |
80 \begin{array}{l} |
86 @{text "T ::= x | T \<rightarrow> T"}\hspace{5mm} |
81 @{text "T ::= x | T \<rightarrow> T"}\hspace{9mm} |
87 @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"} |
82 @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"} |
88 \end{array} |
83 \end{array} |
89 \end{equation} |
84 \end{equation} |
90 % |
85 % |
91 \noindent |
86 \noindent |
237 %binders matters. Consequently, type-schemes with binding sets |
232 %binders matters. Consequently, type-schemes with binding sets |
238 %of names cannot be modelled in Ott. |
233 %of names cannot be modelled in Ott. |
239 |
234 |
240 However, we will not be able to cope with all specifications that are |
235 However, we will not be able to cope with all specifications that are |
241 allowed by Ott. One reason is that Ott lets the user specify ``empty'' |
236 allowed by Ott. One reason is that Ott lets the user specify ``empty'' |
242 types like |
237 types like @{text "t ::= t t | \<lambda>x. t"} |
243 % |
|
244 \begin{center} |
|
245 @{text "t ::= t t | \<lambda>x. t"} |
|
246 \end{center} |
|
247 % |
|
248 \noindent |
|
249 where no clause for variables is given. Arguably, such specifications make |
238 where no clause for variables is given. Arguably, such specifications make |
250 some sense in the context of Coq's type theory (which Ott supports), but not |
239 some sense in the context of Coq's type theory (which Ott supports), but not |
251 at all in a HOL-based environment where every datatype must have a non-empty |
240 at all in a HOL-based environment where every datatype must have a non-empty |
252 set-theoretic model \cite{Berghofer99}. |
241 set-theoretic model \cite{Berghofer99}. |
253 |
242 |
286 $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining |
275 $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining |
287 a new type by identifying a non-empty subset of an existing type. The |
276 a new type by identifying a non-empty subset of an existing type. The |
288 construction we perform in Isabelle/HOL can be illustrated by the following picture: |
277 construction we perform in Isabelle/HOL can be illustrated by the following picture: |
289 % |
278 % |
290 \begin{center} |
279 \begin{center} |
291 \begin{tikzpicture} |
280 \begin{tikzpicture}[scale=0.9] |
292 %\draw[step=2mm] (-4,-1) grid (4,1); |
281 %\draw[step=2mm] (-4,-1) grid (4,1); |
293 |
282 |
294 \draw[very thick] (0.7,0.4) circle (4.25mm); |
283 \draw[very thick] (0.7,0.4) circle (4.25mm); |
295 \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9); |
284 \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9); |
296 \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05); |
285 \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05); |