--- a/Paper/Paper.thy Tue Oct 05 08:43:49 2010 +0100
+++ b/Paper/Paper.thy Tue Oct 05 21:48:31 2010 +0100
@@ -88,8 +88,10 @@
type-variables. While it is possible to implement this kind of more general
binders by iterating single binders, this leads to a rather clumsy
formalisation of W. The need of iterating single binders is also one reason
- why Nominal Isabelle and similar theorem provers that only provide
- mechanisms for binding single variables have not fared extremely well with the
+ why Nominal Isabelle
+ % and similar theorem provers that only provide
+ %mechanisms for binding single variables
+ has not fared extremely well with the
more advanced tasks in the POPLmark challenge \cite{challenge05}, because
also there one would like to bind multiple variables at once.
@@ -202,7 +204,7 @@
\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}cl}
@{text trm} & @{text "::="} & @{text "\<dots>"}
& @{text "|"} @{text "\<LET> as::assn s::trm"}\hspace{2mm}
- \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
+ \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\%%%[1mm]
@{text assn} & @{text "::="} & @{text "\<ANIL>"}
& @{text "|"} @{text "\<ACONS> name trm assn"}
\end{tabular}
@@ -277,7 +279,7 @@
construction we perform in Isabelle/HOL can be illustrated by the following picture:
%
\begin{center}
- \begin{tikzpicture}[scale=0.9]
+ \begin{tikzpicture}[scale=0.89]
%\draw[step=2mm] (-4,-1) grid (4,1);
\draw[very thick] (0.7,0.4) circle (4.25mm);
@@ -506,30 +508,30 @@
@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
\end{property}
- While often the support of an object can be relatively easily
- described, for example for atoms, products, lists, function applications,
- booleans and permutations as follows
+ %While often the support of an object can be relatively easily
+ %described, for example for atoms, products, lists, function applications,
+ %booleans and permutations as follows
+ %%
+ %\begin{center}
+ %\begin{tabular}{c@ {\hspace{10mm}}c}
+ %\begin{tabular}{rcl}
+ %@{term "supp a"} & $=$ & @{term "{a}"}\\
+ %@{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
+ %@{term "supp []"} & $=$ & @{term "{}"}\\
+ %@{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
+ %\end{tabular}
+ %&
+ %\begin{tabular}{rcl}
+ %@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
+ %@{term "supp b"} & $=$ & @{term "{}"}\\
+ %@{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
+ %\end{tabular}
+ %\end{tabular}
+ %\end{center}
%
- \begin{center}
- \begin{tabular}{c@ {\hspace{10mm}}c}
- \begin{tabular}{rcl}
- @{term "supp a"} & $=$ & @{term "{a}"}\\
- @{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
- @{term "supp []"} & $=$ & @{term "{}"}\\
- @{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
- \end{tabular}
- &
- \begin{tabular}{rcl}
- @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
- @{term "supp b"} & $=$ & @{term "{}"}\\
- @{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
- \end{tabular}
- \end{tabular}
- \end{center}
-
- \noindent
- in some cases it can be difficult to characterise the support precisely, and
- only an approximation can be established (as for functions above).
+ %\noindent
+ %in some cases it can be difficult to characterise the support precisely, and
+ %only an approximation can be established (as for functions above).
%Reasoning about
%such approximations can be simplified with the notion \emph{supports}, defined
@@ -576,10 +578,14 @@
%\begin{center}
%@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
%\end{center}
-
- Using support and freshness, the nominal logic work provides us with general means for renaming
- binders. While in the older version of Nominal Isabelle, we used extensively
- Property~\ref{swapfreshfresh} to rename single binders, this property
+ %
+ %Using freshness, the nominal logic work provides us with general means for renaming
+ %binders.
+ %
+ \noindent
+ While in the older version of Nominal Isabelle, we used extensively
+ %Property~\ref{swapfreshfresh}
+ this property to rename single binders, it %%this property
proved too unwieldy for dealing with multiple binders. For such binders the
following generalisations turned out to be easier to use.
@@ -880,7 +886,7 @@
\mbox{\begin{tabular}{@ {}p{2.5cm}l}
type \mbox{declaration part} &
$\begin{cases}
- \mbox{\begin{tabular}{l}
+ \mbox{\small\begin{tabular}{l}
\isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
\isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
\raisebox{2mm}{$\ldots$}\\[-2mm]
@@ -889,7 +895,7 @@
\end{cases}$\\
binding \mbox{function part} &
$\begin{cases}
- \mbox{\begin{tabular}{l}
+ \mbox{\small\begin{tabular}{l}
\isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
\isacommand{where}\\
\raisebox{2mm}{$\ldots$}\\[-2mm]
@@ -979,8 +985,7 @@
single name is bound, and type-schemes, where a finite set of names is
bound:
-
- \begin{center}
+ \begin{center}\small
\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
\begin{tabular}{@ {}l}
\isacommand{nominal\_datatype} @{text lam} $=$\\
@@ -1020,7 +1025,7 @@
tuple patterns might be specified as:
%
\begin{equation}\label{letpat}
- \mbox{%
+ \mbox{\small%
\begin{tabular}{l}
\isacommand{nominal\_datatype} @{text trm} =\\
\hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
@@ -1063,7 +1068,7 @@
specification:
%
\begin{equation}\label{letrecs}
- \mbox{%
+ \mbox{\small%
\begin{tabular}{@ {}l@ {}}
\isacommand{nominal\_datatype}~@{text "trm ="}\ldots\\
\hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
@@ -1132,7 +1137,7 @@
clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
of the lambda-terms, the completion produces
- \begin{center}
+ \begin{center}\small
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
\isacommand{nominal\_datatype} @{text lam} =\\
\hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
@@ -1172,13 +1177,7 @@
But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate
that a notion is given for $\alpha$-equivalence classes and leave it out
for the corresponding notion given on the ``raw'' level. So for example
- we have
-
- \begin{center}
- @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
- \end{center}
-
- \noindent
+ we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
where @{term ty} is the type used in the quotient construction for
@{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}.
@@ -2233,12 +2232,13 @@
\medskip
\noindent
- {\bf Acknowledgements:} We are very grateful to Andrew Pitts for
- many discussions about Nominal Isabelle. We also thank Peter Sewell for
+ {\bf Acknowledgements:} %We are very grateful to Andrew Pitts for
+ %many discussions about Nominal Isabelle.
+ We thank Peter Sewell for
making the informal notes \cite{SewellBestiary} available to us and
also for patiently explaining some of the finer points of the work on the Ott-tool.
- Stephanie Weirich suggested to separate the subgrammars
- of kinds and types in our Core-Haskell example.
+ %Stephanie Weirich suggested to separate the subgrammars
+ %of kinds and types in our Core-Haskell example.
*}