nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:edf10db61708
+:23e3dc4f2c59
 in which the generic type @{text "\<beta>"} stands for the type of the object
 over which the permutation
 acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
 and the inverse permutation of @{term p} as @{text "- p"}. The permutation
-operation is defined by induction over the type-hierarchy (see \cite{HuffmanUrban10});
+operation is defined by induction over the type-hierarchy \cite{HuffmanUrban10};
 for example permutations acting on products, lists, sets, functions and booleans is
 given by:
 %
 \begin{equation}\label{permute}
 \mbox{\begin{tabular}{@ {}cc@ {}}
 first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
 are intended to represent the abstraction, or binding, of the set @{text
 "as"} in the body @{text "x"}.
 The first question we have to answer is when two pairs @{text "(as, x)"} and
-@{text "(bs, y)"} are alpha-equivalent? (At the moment we are interested in
+@{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in
 the notion of alpha-equivalence that is \emph{not} preserved by adding
 vacuous binders.) To answer this, we identify four conditions: {\it i)}
 given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
 set"}}, then @{text x} and @{text y} need to have the same set of free
 variables; moreover there must be a permutation @{text p} such that {\it
 \wedge     & @{text "(p \<bullet> x) R y"}\\
 \end{array}
 \end{equation}
 It might be useful to consider some examples for how these definitions of alpha-equivalence
-pan out in practise.
+pan out in practice.
 For this consider the case of abstracting a set of variables over types (as in type-schemes).
 We set @{text R} to be the equality and for @{text "fv(T)"} we define
 \begin{center}
 @{text "fv(x) = {x}"}  \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}
 \begin{thm}[Support of Abstractions]\label{suppabs}
 Assuming @{text x} has finite support, then\\[-6mm]
 \begin{center}
 \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\
-@{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\
+@{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}\\
-@{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}
+@{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}
 \end{tabular}
 \end{center}
 \end{thm}
 \noindent
 @{thm permute_Abs[no_vars]}
 \end{equation}
 \noindent
 The second fact derives from the definition of permutations acting on pairs
-(see \eqref{permute}) and alpha-equivalence being equivariant
+\eqref{permute} and alpha-equivalence being equivariant
 (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
 the following lemma about swapping two atoms.
 \begin{lemma}
 @{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
 @{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type.
 \end{tabular}
 \end{center}
 \noindent
-To see how these definitions work in practise, let us reconsider the term-constructors
+To see how these definitions work in practice, let us reconsider the term-constructors
 @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}.
 For this specification we need to define three free-variable functions, namely
 @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows:
 %
 \begin{center}
 $|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
 $|$~@{text "bv3 TVCKNil = []"}\\
 $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
 \end{tabular}
 \end{boxedminipage}
-\caption{The nominal datatype declaration for Core-Haskell. At the moment we
+\caption{The nominal datatype declaration for Core-Haskell. For the moment we
 do not support nested types; therefore we explicitly have to unfold the
 lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
 in a future version of Nominal Isabelle. Apart from that, the
 declaration follows closely the original in Figure~\ref{corehas}. The
 point of our work is that having made such a declaration in Nominal Isabelle,
 we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
 Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
 we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
 This completes the proof showing that the strong induction principle derives from
-the weak induction principle. At the moment we can derive the difficult cases of
+the weak induction principle. For the moment we can derive the difficult cases of
 the strong induction principles only by hand, but they are very schematically
 so that with little effort we can even derive them for
 Core-Haskell given in Figure~\ref{nominalcorehas}.
 *}
 automatically a convenient reasoning infrastructure that can deal with
 general binders, that is term-constructors binding multiple variables at
 once. This extension has been tried out with the Core-Haskell
 term-calculus. For such general binders, we can also extend
 earlier work that derives strong induction principles which have the usual
-variable convention already built in. At the moment we can do so only with manual help,
+variable convention already built in. For the moment we can do so only with manual help,
 but future work will automate them completely.  The code underlying the presented
 extension will become part of the Isabelle distribution, but for the moment
 it can be downloaded from the Mercurial repository linked at
 \href{http://isabelle.in.tum.de/nominal/download}
 {http://isabelle.in.tum.de/nominal/download}.

changeset 1890	23e3dc4f2c59
parent 1859	900ef226973e
child 1926	e42bd9d95f09