nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:68c894c513f6
+:3c8d3aaf292c
 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
 want to make a distinction about the order of the bound variables. Therefore
-we would like to regard the first pair of type-schemes as alpha-equivalent,
+we would like to regard below the first pair of type-schemes as alpha-equivalent,
 but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
 the second pair should \emph{not} be alpha-equivalent:
 \begin{equation}\label{ex1}
 @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}
 clause states that all the names the function @{text "bn(as)"} returns
 should be bound in @{text s}.  This style of specifying terms and bindings
 is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work
 extends Ott in several aspects: one is that we support three binding
 modes---Ott has only one, namely the one where the order of binders matters.
-Another is that our reasoning infrastructure, like the notion of support and
+Another is that our reasoning infrastructure, like strong induction principles
-strong induction principles, is derived from first principles within the
+and the notion of free variables, is derived from first principles within
-Isabelle/HOL theorem prover.
+the Isabelle/HOL theorem prover.
 However, we will not be able to cope with all specifications that are
 allowed by Ott. One reason is that Ott lets the user specify ``empty'' types
 like \mbox{@{text "t ::= t t | \<lambda>x. t"}} where no clause for variables is
 given. Arguably, such specifications make some sense in the context of Coq's
 \end{tabular}}
 \]\smallskip
 \noindent
 then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
-operating on quotients, or alpha-equivalence classes of lambda-terms. This
+operating on quotients, that is alpha-equivalence classes of lambda-terms. This
 lifted function is characterised by the equations
 \[
 \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l}
 @{text "fv\<^sup>\<alpha>(x)"}     & @{text "="} & @{text "{x}"}\\
 The examples we have in mind where our reasoning infrastructure will be
 helpful includes the term language of Core-Haskell (see
 Figure~\ref{corehas}). This term language involves patterns that have lists
 of type-, coercion- and term-variables, all of which are bound in @{text
 "\<CASE>"}-expressions. In these patterns we do not know in advance how many
-variables need to be bound. Another example is the specification of SML,
+variables need to be bound. Another example is the algorithm W
-which includes includes bindings as in type-schemes.\medskip
+which includes multiple binders in type-schemes.\medskip
 \noindent
 {\bf Contributions:}  We provide three new definitions for when terms
 involving general binders are alpha-equivalent. These definitions are
 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
 \cite{HuffmanUrban10} (including proofs). We shall briefly review this work
 to aid the description of what follows.
 Two central notions in the nominal logic work are sorted atoms and
 sort-respecting permutations of atoms. We will use the letters @{text "a,
-b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
+b, c, \<dots>"} to stand for atoms and @{text "\<pi>, \<dots>"} to stand for
 permutations. The purpose of atoms is to represent variables, be they bound or free.
 The sorts of atoms can be used to represent different kinds of
 variables, such as the term-, coercion- and type-variables in Core-Haskell.
 It is assumed that there is an infinite supply of atoms for each
 sort. In the interest of brevity, we shall restrict ourselves
 two-place permutation operation written
 @{text "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 where the generic type @{text "\<beta>"} is 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"}},
+the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}},
-and the inverse permutation of @{term p} as @{text "- p"}. The permutation
+and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
 operation is defined over the type-hierarchy \cite{HuffmanUrban10};
 for example permutations acting on products, lists, sets, functions and booleans are
 given by:
 \begin{equation}\label{permute}
 \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 \begin{tabular}{@ {}l@ {}}
-@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
+@{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]
-@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
+@{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
+@{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
 \end{tabular} &
 \begin{tabular}{@ {}l@ {}}
-@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
+@{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
+@{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\
-@{thm permute_bool_def[no_vars, THEN eq_reflection]}
+@{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}
 \end{tabular}
 \end{tabular}}
-\end{equation}
+\end{equation}\smallskip
-\begin{center}
-\mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}}
-\begin{tabular}{@ {}l@ {}}
-@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\
-@{thm permute_bool_def[no_vars, THEN eq_reflection]}
-\end{tabular} &
-\begin{tabular}{@ {}l@ {}}
-@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
-@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
-\end{tabular} &
-\begin{tabular}{@ {}l@ {}}
-@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
-@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
-\end{tabular}
-\end{tabular}}
-\end{center}
 \noindent
 Concrete permutations in Nominal Isabelle are built up from swappings,
 written as \mbox{@{text "(a b)"}}, which are permutations that behave
 as follows:
-\begin{center}
+\[
 @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
-\end{center}
+\]\smallskip
 The most original aspect of the nominal logic work of Pitts is a general
 definition for the notion of the ``set of free variables of an object @{text
 "x"}''.  This notion, written @{term "supp x"}, is general in the sense that
 it applies not only to lambda-terms (alpha-equated or not), but also to lists,
 @{thm supp_def[no_vars, THEN eq_reflection]}
 \end{equation}
 \noindent
 There is also the derived notion for when an atom @{text a} is \emph{fresh}
-for an @{text x}, defined as @{thm fresh_def[no_vars]}.
+for an @{text x}, defined as
+\[
+@{thm fresh_def[no_vars]}
+\]\smallskip
+\noindent
 We use for sets of atoms the abbreviation
 @{thm (lhs) fresh_star_def[no_vars]}, defined as
 @{thm (rhs) fresh_star_def[no_vars]}.
 A striking consequence of these definitions is that we can prove
 without knowing anything about the structure of @{term x} that
 swapping two fresh atoms, say @{text a} and @{text b}, leaves
-@{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
+@{text x} unchanged, namely
-then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
 \begin{prop}\label{swapfreshfresh}
-@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
+If @{thm (prem 1) swap_fresh_fresh[no_vars]} and @{thm (prem 2) swap_fresh_fresh[no_vars]}
+then @{thm (concl) swap_fresh_fresh[no_vars]}
 \end{prop}
 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}
+\[\mbox{
 \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 "{}"}\\
 \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}"}
+@{term "supp \<pi>"} & $=$ & @{term "{a. \<pi> \<bullet> a \<noteq> a}"}
 \end{tabular}
-\end{tabular}
+\end{tabular}}
-\end{center}
+\]\smallskip
 \noindent
 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 function applications
+above). Reasoning about such approximations can be simplified with the
-Reasoning about
+notion \emph{supports}, defined as follows:
-such approximations can be simplified with the notion \emph{supports}, defined
-as follows:
 \begin{defi}
 A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
 not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
 \end{defi}

changeset 3000	3c8d3aaf292c
parent 2991	8146b0ad8212
child 3001	8d7d85e915b5