nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:734341a79028
+:2ccf3086142b
 \noindent
 and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
 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
+why Nominal Isabelle
-mechanisms for binding single variables have not fared extremely well with the
+% 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.
 Binding multiple variables has interesting properties that cannot be captured
 easily by iterating single binders. For example in the case of type-schemes we do not
 %
 \begin{center}
 \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}
 \end{center}
 %
 $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
 a new type by identifying a non-empty subset of an existing type.  The
 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);
 \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);
 \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);
 \begin{property}\label{swapfreshfresh}
 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
 \end{property}
-While often the support of an object can be relatively easily
+%While often the support of an object can be relatively easily
-described, for example for atoms, products, lists, function applications,
+%described, for example for atoms, products, lists, function applications,
-booleans and permutations as follows
+%booleans and permutations as follows
-%
+%%
-\begin{center}
+%\begin{center}
-\begin{tabular}{c@ {\hspace{10mm}}c}
+%\begin{tabular}{c@ {\hspace{10mm}}c}
-\begin{tabular}{rcl}
+%\begin{tabular}{rcl}
-@{term "supp a"} & $=$ & @{term "{a}"}\\
+%@{term "supp a"} & $=$ & @{term "{a}"}\\
-@{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
+%@{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
-@{term "supp []"} & $=$ & @{term "{}"}\\
+%@{term "supp []"} & $=$ & @{term "{}"}\\
-@{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
+%@{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
-\end{tabular}
+%\end{tabular}
-&
+%&
-\begin{tabular}{rcl}
+%\begin{tabular}{rcl}
-@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
+%@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
-@{term "supp b"} & $=$ & @{term "{}"}\\
+%@{term "supp b"} & $=$ & @{term "{}"}\\
-@{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
+%@{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
-\end{tabular}
+%\end{tabular}
-\end{tabular}
+%\end{tabular}
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
-in some cases it can be difficult to characterise the support precisely, and
+%in some cases it can be difficult to characterise the support precisely, and
-only an approximation can be established (as for functions above).
+%only an approximation can be established (as for functions above).
 %Reasoning about
 %such approximations can be simplified with the notion \emph{supports}, defined
 %as follows:
 %
 %that
 %%
 %\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
+%Using freshness, the nominal logic work provides us with general means for renaming
-binders. While in the older version of Nominal Isabelle, we used extensively
+%binders.
-Property~\ref{swapfreshfresh} to rename single binders, this property
+%
+\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.
 \begin{property}\label{supppermeq}
 @{thm[mode=IfThen] supp_perm_eq[no_vars]}
 %
 \begin{equation}\label{scheme}
 \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]
 \isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\
 \end{tabular}}
 \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]
 \end{tabular}}
 \end{cases}$\\
 the labels must refer to atom types or lists of atom types. Two examples for
 the use of shallow binders are the specification of lambda-terms, where a
 single name is bound, and type-schemes, where a finite set of names is
 bound:
+\begin{center}\small
-\begin{center}
 \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 \begin{tabular}{@ {}l}
 \isacommand{nominal\_datatype} @{text lam} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
 \hspace{5mm}$\mid$~@{text "App lam lam"}\\
 must be given in the binding function part of the scheme shown in
 \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
 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"}\\
 \hspace{5mm}$\mid$~@{term "App trm trm"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"}
 binders \emph{recursive}.  To see the purpose of such recursive binders,
 compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
 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"}
 \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
 \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
 for every argument of a term-constructor that is \emph{not}
 already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
 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"}
 \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
 \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
 given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
 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
+we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
-\begin{center}
-@{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
-\end{center}
-\noindent
 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"}.
 The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
 non-empty and the types in the constructors only occur in positive
 Once we feel confident about such binding modes, our implementation
 can be easily extended to accommodate them.
 \medskip
 \noindent
-{\bf Acknowledgements:} We are very grateful to Andrew Pitts for
+{\bf Acknowledgements:} %We are very grateful to Andrew Pitts for
-many discussions about Nominal Isabelle. We also thank Peter Sewell 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
+%Stephanie Weirich suggested to separate the subgrammars
-of kinds and types in our Core-Haskell example.
+%of kinds and types in our Core-Haskell example.
 *}
 (*<*)
 end

changeset 2511	2ccf3086142b
parent 2510	734341a79028
child 2512	b5cb3183409e