nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:1b53c9e8719f
+:8de43bd80bc2
 equal ("=") and
 alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 alpha_abs_lst ("_ \<approx>\<^raw:{$\,_{\textit{abs\_list}}$}> _") and
 alpha_abs_res ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set+}}$}> _") and
 Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
-Abs_lst ("[_]\<^bsub>list\<^esub>._") and
+Abs_lst ("[_]\<^bsub>list\<^esub>._" [20, 101] 999) and
-Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
+Abs_dist ("[_]\<^bsub>#list\<^esub>._" [20, 101] 999) and
 Abs_res ("[_]\<^bsub>set+\<^esub>._") and
 Abs_print ("_\<^bsub>set\<^esub>._") and
 Cons ("_::_" [78,77] 73) and
 supp_set ("aux _" [1000] 10) and
 alpha_bn ("_ \<approx>bn _")
 wealth of experience we gained with the older version of Nominal Isabelle:
 for non-trivial properties, reasoning with alpha-equated terms is much
 easier than reasoning with raw terms. The fundamental reason for this is
 that the HOL-logic underlying Nominal Isabelle allows us to replace
 ``equals-by-equals''. In contrast, replacing
-``alpha-equals-by-alpha-equals'' in a representation based on raw terms
+``alpha-equals-by-alpha-equals'' in a representation based on ``raw'' terms
 requires a lot of extra reasoning work.
 Although in informal settings a reasoning infrastructure for alpha-equated
 terms is nearly always taken for granted, establishing it automatically in
 Isabelle/HOL is a rather non-trivial task. For every
 "\<CASE>"}-expressions. In these patterns we do not know in advance how many
 variables need to be bound. Another example is the algorithm W,
 which includes multiple binders in type-schemes.\medskip
 \noindent
-{\bf Contributions:}  We provide three new definitions for when terms
+{\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
-proofs, we establish a reasoning infrastructure for alpha-equated
+proofs, we establish a reasoning infrastructure for alpha-equated terms,
-terms, including properties about support, freshness and equality
+including properties about support, freshness and equality conditions for
-conditions for alpha-equated terms. We are also able to derive strong
+alpha-equated terms. We are also able to automatically derive strong
 induction principles that have the variable convention already built in.
-The method behind our specification of general binders is taken
+For this we simplify the earlier automated proofs by using the proof tools
-from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
+from the function package~\cite{Krauss09} of Isabelle/HOL.  The method
-that our specifications make sense for reasoning about alpha-equated terms.
+behind our specification of general binders is taken from the Ott-tool, but
-The main improvement over Ott is that we introduce three binding modes
+we introduce crucial restrictions, and also extensions, so that our
-(only one is present in Ott), provide formalised definitions for alpha-equivalence and
+specifications make sense for reasoning about alpha-equated terms.  The main
+improvement over Ott is that we introduce three binding modes (only one is
+present in Ott), provide formalised definitions for alpha-equivalence and
 for free variables of our terms, and also derive a reasoning infrastructure
 for our specifications from ``first principles'' inside a theorem prover.
-\begin{figure}
+\begin{figure}[t]
 \begin{boxedminipage}{\linewidth}
 \begin{center}
 \begin{tabular}{@ {\hspace{8mm}}r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
 \multicolumn{3}{@ {}l}{Type Kinds}\\
 @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
 @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}.
 Note that @{term "supp x \<sharp>* \<pi>"}
 is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate
-Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction', however the
+Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction'; however the
 reasoning infrastructure of Nominal Isabelle is set up so that it provides more
 automation for the formulation given above.
 Most properties given in this section are described in detail in \cite{HuffmanUrban10}
 and all are formalised in Isabelle/HOL. In the next sections we will make
 where @{term set} is the function that coerces a list of atoms into a set of atoms.
 Now the last clause ensures that the order of the binders matters (since @{text as}
 and @{text bs} are lists of atoms).
 If we do not want to make any difference between the order of binders \emph{and}
-also allow vacuous binders, that means according to Pitts \emph{restrict} names
+also allow vacuous binders, that means according to Pitts~\cite{Pitts04}
-\cite{Pitts04}, then we keep sets of binders, but drop
+\emph{restrict} names, then we keep sets of binders, but drop
 condition {\it (iv)} in Definition~\ref{alphaset}:
 \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
 \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
 @{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
 permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
 (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
 shown that all three notions of alpha-equivalence coincide, if we only
 abstract a single atom.
-In the rest of this section we are going to show that the alpha-equivalences really
+In the rest of this section we are going to show that the alpha-equivalences
-lead to abstractions where some atoms are bound (more precisely removed from the
+really lead to abstractions where some atoms are bound (more precisely
-support).  For this we are going to introduce
+removed from the support).  For this we will consider three abstraction
-three abstraction types that are quotients of the relations
+types that are quotients of the relations
 \begin{equation}
 \begin{array}{r}
 @{term "alpha_set_ex (as, x) equal supp (bs, y)"}\smallskip\\
 @{term "alpha_res_ex (as, x) equal supp (bs, y)"}\smallskip\\
 \]\smallskip
 \end{thm}
 \noindent
 In effect, this theorem states that the atoms @{text "as"} are bound in the
-abstraction. As stated earlier, this can be seen as test that our
+abstraction. As stated earlier, this can be seen as litmus test that our
 Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the
 idea of alpha-equivalence relations. Below we will give the proof for the
 first equation of Theorem \ref{suppabs}. The others follow by similar
 arguments. By definition of the abstraction type @{text
 "abs\<^bsub>set\<^esub>"} we have
 @{thm (concl) Abs_swap1(1)[where bs="as", no_vars]}
 \end{lem}
 \begin{proof}
 If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b) = 0"}.
-Also in the other case it is straightforward using \eqref{abseqiff} and
+Also in the other case the lemma is straightforward using \eqref{abseqiff}
-observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
+and observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
-(supp x - as)"}.  We therefore can use as permutation the swapping @{term
+(supp x - as)"}.  We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"}. as
-"(a \<rightleftharpoons> b)"}.
+the permutation fpr the proof obligation.
 \end{proof}
 \noindent
 Assuming that @{text "x"} has finite support, this lemma together
 with \eqref{absperm} allows us to show
 This is because for every finite sets of atoms, say @{text "bs"}, we have
 @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
 Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
 the first equation of Theorem~\ref{suppabs}.
-Recall the definition of support in \eqref{suppdef}, and note the difference between
+Recall the definition of support given in \eqref{suppdef}, and note the difference between
 the support of a ``raw'' pair and an abstraction
 \[
 @{term "supp (as, x) = supp as \<union> supp x"}\hspace{15mm}
 @{term "supp (Abs_set as x) = supp x - as"}
 \]\smallskip
 \noindent
 While the permutation operations behave in both cases the same (a permutation
 is just moved to the arguments), the notion of equality is different for pairs and
-abstractions. Therefore we have different supports.
+abstractions. Therefore we have different supports. In case of abstractions,
+we have established that bound atoms are removed from the support of the
+abstractions' bodies.
 The method of first considering abstractions of the form @{term "Abs_set as
 x"} etc is motivated by the fact that we can conveniently establish at the
 Isabelle/HOL level properties about them.  It would be extremely laborious
 to write custom ML-code that derives automatically such properties for every
 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 @{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 in the ``raw'' type @{text "ty"},
+@{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the ``raw'' type @{text "ty"},
-respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor in @{text "ty\<^sup>\<alpha>"}.
+respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor of @{text "ty\<^sup>\<alpha>"}.
 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
 position (see \cite{Berghofer99} for an in-depth description of the datatype package
 in Isabelle/HOL).
 \begin{equation}\label{ceqvt}
 @{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
 \end{equation}\smallskip
 \noindent
-We need this operation later when we define the notion of alpha-equivalence.
+We will need this operation later when we define the notion of alpha-equivalence.
 The first non-trivial step we have to perform is the generation of
 \emph{free-atom functions} from the specifications.\footnote{Admittedly, the
 details of our definitions will be somewhat involved. However they are still
 conceptually simple in comparison with the ``positional'' approach taken in
 \]\smallskip
 \noindent
 where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the
 specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function
-we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}}. The reason
+we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i \<equiv> supp"}}. The reason
 for the latter is that @{text "ty"}$_i$ is not a type that is part of the specification, and
-we assume @{text supp} is the generic notion that characterises the free variables of
+we assume @{text supp} is the generic function that characterises the free variables of
 a type (in fact in the next section we will show that the free-variable functions we
 define here, are equal to the support once lifted to alpha-equivalence classes).
 In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
 for atom types to which shallow binders may refer\\[-4mm]
 \noindent
 In this case we define a premise @{text P} using the relation
 $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ given in Section~\ref{sec:binders} (similarly
 $\approx_{\,\textit{set+}}^{\textit{R}, \textit{fa}}$ and
 $\approx_{\,\textit{list}}^{\textit{R}, \textit{fa}}$ for the other
-binding modes). This premise defines alpha-equivalence of two abstractions
+binding modes). As above, we first build the tuples @{text "D"} and
-involving multiple binders. As above, we first build the tuples @{text "D"} and
 @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
 compound alpha-relation @{text "R"} (shown in \eqref{rempty}).
 For $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$  we also need
 a compound free-atom function for the bodies defined as
 clause. However, in case the binders have non-recursive deep binders, this
 premise is not enough: we also have to ``propagate'' alpha-equivalence
 inside the structure of these binders. An example is @{text "Let"} where we
 have to make sure the right-hand sides of assignments are
 alpha-equivalent. For this we use relations @{text "\<approx>bn"}$_{1..m}$ (which we
-will formally define shortly).  Let us assume the non-recursive deep binders
+will define shortly).  Let us assume the non-recursive deep binders
 in @{text "bc\<^isub>i"} are
 \[
 @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
 \]\smallskip
 non-empty ones (we just have to unfold the definition of
 $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ and take @{text "0"}
 for the existentially quantified permutation).
 Again let us take a look at a concrete example for these definitions. For
-the specification given in \eqref{letrecs}
+the specification shown in \eqref{letrecs}
 we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$ with the following rules:
 \begin{equation}\label{rawalpha}\mbox{
 \begin{tabular}{@ {}c @ {}}
 clause for @{text "Let"} (which has
 a non-recursive binder).
 The underlying reason is that the terms inside an assignment are not meant
 to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
 because there all components of an assignment are ``under'' the binder.
-Note also that in case of more than one body (that is in the @{text "Let_rec"}-case)
+Note also that in case of more than one body (that is in the @{text "Let_rec"}-case above)
 we need to parametrise the relation $\approx_{\textit{list}}$ with a compound
 equivalence relation and a compound free-atom function. This is because the
 corresponding binding clause specifies a binder with two bodies, namely
 @{text "as"} and @{text "t"}.
 *}
 @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.
 \]\smallskip
 \noindent
 We call these conditions as \emph{quasi-injectivity}. They correspond to the
-premises in our alpha-equiva\-lence relations, with the exception that the
+premises in our alpha-equiva\-lence relations, except that the
 relations @{text "\<approx>ty"}$_{1..n}$ are all replaced by equality (and similarly
 the free-atom and binding functions are replaced by their lifted
 counterparts). Recall the alpha-equivalence rules for @{text "Let"} and
 @{text "Let_rec"} shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and
 @{text "Let_rec\<^sup>\<alpha>"} we have
 @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. P\<^isub>r x\<^isub>r \<and> \<dots> \<and> P\<^isub>s x\<^isub>s \<Rightarrow> P (C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l)"}\\
 \end{array}}
 \end{equation}\smallskip
 \noindent
-whereby the @{text P}$_{1..n}$ are the properties established by the induction
+whereby the @{text P}$_{1..n}$ are the properties established by the
-and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$. Note that
+induction, and the @{text y}$_{1..n}$ are of type @{text
-the induction principle has for the term constructors @{text "C"}$^\alpha_1$ a
+"ty\<AL>"}$_{1..n}$. Note that for the term constructors @{text
-hypothesis of the form
+"C"}$^\alpha_1$ the induction principle has a hypothesis of the form
 \[
 \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^sub>1 x\<^isub>1 \<dots> x\<^isub>k)"}}
 \]\smallskip
 recursive arguments of this term constructor (similarly for the other
 term-constructors).
 Recall the lambda-calculus with @{text "Let"}-patterns shown in
 \eqref{letpat}. The cases lemmas and the induction principle shown in
-\eqref{cases} and \eqref{induct} boil down to the following three inference
+\eqref{cases} and \eqref{induct} boil down in this example to the following three inference
 rules (the cases lemmas are on the left-hand side; the induction principle
 on the right):
 \begin{equation}\label{inductex}\mbox{
 \begin{tabular}{c}
 \]\smallskip
 \noindent
 This allows us to prove using the induction principle for  @{text "ty\<AL>"}$_{1..n}$
 that every element of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported
-(using Prop.~\ref{supportsprop}{\it (i)}).
+(using Proposition~\ref{supportsprop}{\it (i)}).
 Similarly, we can establish by induction that the free-atom functions and binding
 functions are equivariant, namely
 \[\mbox{
 \begin{tabular}{rcl}
 \]\smallskip
 \noindent
 Lastly, we can show that the support of elements in @{text
-"ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.  This fact
+"ty\<AL>"}$_{1..n}$ is the same as the free atom functions @{text
-is important in the nominal setting where the general theory is formulated
+"fa_ty\<AL>"}$_{1..n}$.  This fact is important in the nominal setting where
-in terms of support and freshness, but also provides evidence that our
+the general theory is formulated in terms of support and freshness, but also
-notions of free-atoms and alpha-equivalence ``match up''.
+provides evidence that our notions of free-atoms and alpha-equivalence
+``match up'' correctly.
 \begin{thm}\label{suppfa}
 For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
 @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.
 \end{thm}
 for which we have to know that every body of an abstraction is finitely supported.
 This, we have proved earlier.
 \end{proof}
 \noindent
-Consequently we can simplify the quasi-injection lemmas, for example the ones
+Consequently, we can replace the free atom functions by @{text "supp"} in
-given in \eqref{alphalift} for @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"} to
+our quasi-injection lemmas. In the examples shown in \eqref{alphalift}, for instance,
+we obtain for @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"}
 \[\mbox{
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "Let\<^sup>\<alpha> as t = Let\<^sup>\<alpha> as' t'"}}
 {@{term "alpha_lst_ex (bn_al as, t) equal supp (bn_al as', t')"} &
 {@{term "alpha_lst_ex (bn_al as, ast) equ2 supp2 (bn_al as', ast')"}}}\\
 \end{tabular}}
 \]\smallskip
 \noindent
-Taking the fact into account that the compound equivalence relation @{term
+Taking into account that the compound equivalence relation @{term
 "equ2"} and the compound free-atom function @{term "supp2"} are by
 definition equal to @{term "equal"} and @{term "supp"}, respectively, the
-above rules simplify even further to
+above rules simplify further to
 \[\mbox{
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "Let\<^sup>\<alpha> as t = Let\<^sup>\<alpha> as' t'"}}
 {@{term "Abs_lst (bn_al as) t = Abs_lst (bn_al as') t'"} &
 \]\smallskip
 \noindent
 using the support of abstractions derived in Theorem~\ref{suppabs}.
+To sum up this section, we have established a reasoning infrastructure for the
-To sum up this section, we can establish a reasoning infrastructure for the
 types @{text "ty\<AL>"}$_{1..n}$ by first lifting definitions from the
 ``raw'' level to the quotient level and then by proving facts about
 these lifted definitions. All necessary proofs are generated automatically
 by custom ML-code.
 *}
 section {* Strong Induction Principles *}
 text {*
 In the previous section we derived induction principles for alpha-equated
 terms (see \eqref{induct} for the general form and \eqref{inductex} for an
-instance). This was done by lifting the corresponding inductions principles
+example). This was done by lifting the corresponding inductions principles
 for ``raw'' terms.  We already employed these induction principles for
-deriving several facts for alpha-equated terms, including the property that
+deriving several facts about alpha-equated terms, including the property that
 the free-variable functions and the notion of support coincide. Still, we
 call these induction principles \emph{weak}, because for a term-constructor,
 say \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction
 hypothesis requires us to establish (under some assumptions) a property
 @{text "P (C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text
-"x"}$_{1..r}$. The problem is that in the presence of binders we cannot make
+"x"}$_{1..r}$. The problem with this is that in the presence of binders we cannot make
 any assumptions about the atoms that are bound. One obvious way around this
 problem is to rename them. Unfortunately, this leads to very clunky proofs
-and makes formalisations grievous experiences (especially in the case for
+and makes formalisations grievous experiences (especially in the context of
 multiple bound atoms).
+For the older versions of Nominal Isabelle we described in \cite{Urban08} a
-For the older versions of Nominal Isabelle we described in
+method for automatically strengthening weak induction principles. These
-\cite{Urban08} a method for automatically strengthening weak induction
+stronger induction principles allow the user to make additional assumptions
-principles. These stronger induction principles allow the user to make
+about bound atoms. The advantage of these assumptions is that they make in
-additional assumptions about bound atoms. The advantage of these assumptions
+most cases any renaming of bound atoms unnecessary.  To explain how the
-is that they make in most cases any renaming of bound atoms unnecessary.  To
+strengthening works, we use as running example the lambda-calculus with
-explain how the strengthening works in the presence of multiple binders, we
+@{text "Let"}-patterns shown in \eqref{letpat}. Its weak induction principle
-use as running example the lambda-calculus with @{text "Let"}-patterns shown
+is given in \eqref{inductex}.  The stronger induction principle is as
-in \eqref{letpat}. Its weak induction principle is given in
+follows:
-\eqref{inductex}.  The stronger induction principle is as follows:
 \begin{equation}\label{stronginduct}
 \mbox{
 \begin{tabular}{@ {}c@ {}}
 \infer{@{text "P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"}}
 \end{tabular}}
 \end{equation}\smallskip
 \noindent
-Instead of establishing the two properties @{text " P\<^bsub>trm\<^esub>
+Notice that instead of establishing two properties of the form @{text "
-y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}, as the weak one does, the
+P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}, as the
-stronger induction principle establishes the properties @{text "
+weak one does, the stronger induction principle establishes the properties
-P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"} in
+of the form @{text " P\<^bsub>trm\<^esub> c y\<^isub>1 \<and>
-which the additional parameter @{text c} is assumed to be of finite
+P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional parameter @{text
-support. The purpose of @{text "c"} is to ``control'' which freshness
+c} is assumed to be of finite support. The purpose of @{text "c"} is to
-assumptions the binders should satisfy in the @{text "Lam\<^sup>\<alpha>"} and
+``control'' which freshness assumptions the binders should satisfy in the
-@{text "Let_pat\<^sup>\<alpha>"} cases: for @{text "Lam\<^sup>\<alpha>"} we can assume the
+@{text "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases: for @{text
-bound atom @{text "x\<^isub>1"} is fresh for @{text "c"}; for @{text
+"Lam\<^sup>\<alpha>"} we can assume the bound atom @{text "x\<^isub>1"} is fresh
-"Let_pat\<^sup>\<alpha>"} we can assume all bound atoms from an assignment are fresh
+for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume
-for @{text "c"}. If @{text "c"} is instantiated appropriately, the user can
+all bound atoms from an assignment are fresh for @{text "c"} (fourth
-mimic the ``pencil-and-paper'' reasoning employing the usual variable
+line). If @{text "c"} is instantiated appropriately in the strong induction
-convention \cite{Urban08}.
+principle, the user can mimic the usual ``pencil-and-paper'' reasoning
+employing the variable convention about bound and free variables being
-In what follows we will show that the induction principle in
+distinct \cite{Urban08}.
-\eqref{inductex} implies \eqref{stronginduct}. This fact was established for
+In what follows we will show that the weak induction principle in
+\eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for
 single binders in \cite{Urban08} by some quite involved, nevertheless
 automated, induction proof. In this paper we simplify the proof by
-leveraging the automated proof methods from the function package of
+leveraging the automated proving methods from the function package of
 Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these methods
 is well-founded induction. To use them in our setting, we have to discharge
 two proof obligations: one is that we have well-founded measures (one for
 each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
 step and the other is that we have covered all cases in the induction
 principle. Once these two proof obligations are discharged, the reasoning
 infrastructure in the function package will automatically derive the
-stronger induction principle. This considerably simplifies the work we have
+stronger induction principle. This way of establishing the stronger induction
-to do here.
+principle is considerably simpler than the work presented \cite{Urban08}.
 As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
 which we lifted in the previous section and which are all well-founded. It
 is straightforward to establish that the sizes decrease in every
 induction step. What is left to show is that we covered all cases.
 \end{array}}
 \end{tabular}}
 \]\smallskip
 \noindent
-They are stronger in the sense that they allow us to assume that the bound
+They are stronger in the sense that they allow us to assume in the @{text
-atoms avoid a context @{text "c"} (which is assumed to be finitely
+"Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms
-supported). This is similar with the stronger induction principles.
+avoid a context @{text "c"} (which is assumed to be finitely supported).
 These stronger cases lemmas need to be derived from the `weak' cases lemmas
 given in \eqref{inductex}. This is trivial in case of patterns (the one on
 the right-hand side) since the weak and strong cases lemma coincide (there
 is no binding in patterns).  Interesting are only the cases for @{text
 "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"}, where we have some binders and
-therefore have an addition assumption.  Let us show first establish the case
+therefore have an addition assumption about avoiding @{text "c"}.  Let us
-for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma \eqref{inductex} we can
+first establish the case for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma
-assume that
+\eqref{inductex} we can assume that
 \begin{equation}\label{assm}
 @{text "y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
 \end{equation}\smallskip
 \noindent
-holds and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the
+holds, and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the
 corresponding implication
 \begin{equation}\label{imp}
 @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}
 \end{equation}\smallskip
 \noindent
-which we can use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
+which we must use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
 use this implication directly, because we have no information whether @{text
 "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
-\ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: We know
+\ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know
 by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
 x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 -
-{atom x\<^isub>1}"}). Property \ref{avoiding} provides us therefore with a
+{atom x\<^isub>1}"}). Property \ref{avoiding} provides us then with a
 permutation @{text "\<pi>"}, such that @{text "{atom (\<pi> \<bullet> x\<^isub>1)} #\<^sup>*
 c"} and \mbox{@{text "supp (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2) #\<^sup>* \<pi>"}} hold.
-By using Property \ref{supppermeq}, we can infer from the latter that @{text
+By using Property \ref{supppermeq}, we can infer from the latter that
-"Lam\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"} holds. We can use this equation in
-the assumption \eqref{assm} and then use \eqref{imp} with the renamed @{text "\<pi> \<bullet> x\<^isub>1"}
+\[
-and @{text "\<pi> \<bullet> x\<^isub>2"} in order to conclude this case.
+@{text "Lam\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
+\]\smallskip
+\noindent
+holds. We can use this equation in the assumption \eqref{assm}, and hence
+use the implication \eqref{imp} with the renamed @{text "\<pi> \<bullet> x\<^isub>1"}
+and @{text "\<pi> \<bullet> x\<^isub>2"} for concluding this case.
 The @{text "Let_pat\<^sup>\<alpha>"}-case involving a deep binder is slightly more complicated.
 We have the assumption
 \begin{equation}\label{assmtwo}
 @{text "y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
 \end{equation}\smallskip
 \noindent
-and the implication
+and the implication from the stronger cases lemma
-\[
+\begin{equation}\label{impletpat}
 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
-\]\smallskip
+\end{equation}\smallskip
 \noindent
 The reason that this case is more complicated is that we cannot apply directly Property
 \ref{avoiding} for obtaining a renaming permutation. Property \ref{avoiding} requires
 that the binders are fresh for the term in which we want to perform the renaming. But
 \[
 @{text "Let (x, y) := (x, y) in (x, y)"}
 \]\smallskip
 \noindent
-Although @{text x} and @{text y} are bound in this term, they are also free
+where @{text x} and @{text y} are bound in the term, but they are also free
-in the assignment. We can, however, obtain obtain such a renaming
+in the assignment. We can, however, obtain such a renaming permutation, say
-permutation, say @{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al
+@{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1)
-x\<^isub>1) x\<^isub>3"}. So we have \mbox{@{term "set (bn_al (\<pi> \<bullet>
+x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\<pi> \<bullet> x\<^isub>1))
-x\<^isub>1)) \<sharp>* c"}} and @{term "Abs_lst (bn_al (\<pi> \<bullet> x\<^isub>1)) (\<pi> \<bullet>
+\<sharp>* c"}} and @{term "Abs_lst (bn_al (\<pi> \<bullet> x\<^isub>1)) (\<pi> \<bullet> x\<^isub>3) =
-x\<^isub>3) = Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text "bn\<^sup>\<alpha>"} are equivariant).
+Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text
-Now the quasi-injective property for @{text "Let_pat\<^sup>\<alpha>"} states
+"bn\<^sup>\<alpha>"} are equivariant).  Now the quasi-injective property for @{text
+"Let_pat\<^sup>\<alpha>"} states that
 \[
 \infer{@{text "Let_pat\<^sup>\<alpha> p t\<^isub>1 t\<^isub>2 = Let_pat\<^sup>\<alpha> p\<PRIME> t\<PRIME>\<^isub>1 t\<PRIME>\<^isub>2"}}
 {@{text "[bn\<^sup>\<alpha> p]\<^bsub>list\<^esub>. t\<^isub>2 = [bn\<^sup>\<alpha> p']\<^bsub>list\<^esub>. t\<PRIME>\<^isub>2"}\;\; &
 @{text "p \<approx>\<AL>\<^bsub>bn\<^esub> p\<PRIME>"}\;\; & @{text "t\<^isub>1 = t\<PRIME>\<^isub>1"}}
 \]\smallskip
 \noindent
-Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\<alpha>"}
+Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\<alpha>"}, we can infer
-(hence @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}), we can infer the
+@{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}. Therefore we have that
-equation
 \[
 @{text "Let_pat\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) x\<^isub>2 (\<pi> \<bullet> x\<^isub>3) = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
 \]\smallskip
 \noindent
-Taking the left-hand side as our assumption in \eqref{assmtwo}, we can use
+Taking the left-hand side in the assumption from \eqref{assmtwo}, we can use
-the implication from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed.
+the implication \eqref{impletpat} from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed.
 The remaining difficulty is when a deep binder contains atoms that are
-bound, but also atoms that are free. An example is @{text "Let\<^sup>\<alpha>"} in \eqref{}.
+bound, but also some that are free. An example is @{text "Let\<^sup>\<alpha>"} in
-Then @{text "(\<pi> \<bullet> x\<^isub>1)
+the example \eqref{letrecs}.  In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
-\<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. In such
+\<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea is
-cases, however, we only want to rename binders that will become bound, which
+that we only want to rename binders that will become bound. This does not
-does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. The problem is that the
+affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. However, the problem is that the
-permutation operation @{text "\<bullet>"} permutes all of them. The remedy is to
+permutation operation @{text "_ \<bullet> _"} applies to all of them. To avoid this
-introduce an auxiliary permutation operation, written @{text "_
+we introduce an auxiliary permutation operations, written @{text "_
-\<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permute bound atoms and
+\<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or
-leaves the other atoms unchanged. Like the @{text
+more precisely the atoms specified by the @{text "bn"}-functions) and leaves
-"fa_bn"}$_{1..m}$-functions, we can define this operation over raw terms
+the other atoms unchanged. Like the @{text "fa_bn"}$_{1..m}$-functions, we
-analysing how the @{text "bn"}$_{1..m}$-functions are defined and then lift
+can define these operations over raw terms analysing how the @{text
-them to alpha-equivalent terms. Assuming the user specified a clause
+"bn"}$_{1..m}$-functions are defined. Assuming the user specified a clause
 \[
 @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}
 \]\smallskip
 \noindent
 Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} functions to
 alpha-equated terms. Moreover we can prove the following two properties
 \begin{lem}\label{permutebn}
-Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text "\<pi>"}\\
+Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text "\<pi>"}\smallskip\\
 {\it (i)} @{text "\<pi> \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and\\
 {\it (ii)} @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x) \<approx>\<AL>\<^bsub>bn\<^esub> x"}.
 \end{lem}
 \begin{proof}
-By induction on @{text x}. The properties follow by simple unfolding
+By induction on @{text x}. The properties follow by unfolding of the
-of the definitions.
+definitions.
 \end{proof}
 \noindent
-The first property states that a permutation applied to a binding function is
+The first property states that a permutation applied to a binding function
-equivalent to first permuting the binders and then calculating the bound
+is equivalent to first permuting the binders and then calculating the bound
-atoms. The main point of the auxiliary permutation
+atoms. The second states that @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} preserves
-functions is that it allows us to rename just the binders in a term,
+@{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}.  The main point of the auxiliary
-without changing anything else.
+permutation functions is that they allow us to rename just the binders in a
+term, without changing anything else.
 Having the auxiliary permutation function in place, we can now solve all remaining cases.
-For @{text "Let\<^sup>\<alpha>"} term-constructor, for example, we can by Property \ref{avoiding}
+For the @{text "Let\<^sup>\<alpha>"} term-constructor, for example, we can by Property \ref{avoiding}
 obtain a @{text "\<pi>"} such that
 \[
 @{text "(\<pi> \<bullet> (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c"} \hspace{10mm}
 @{text "\<pi> \<bullet> [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2 = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}
 \noindent
 hold. Using Lemma \ref{permutebn}{\it (i)} we can simplify this
 to @{text "set (bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and
 @{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}. Since
-@{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by Lemma \ref{permutebn}{\it (ii)}
+@{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by Lemma \ref{permutebn}{\it (ii)},
 we can infer that
 \[
 @{text "Let\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
 \]\smallskip
 \noindent
-are alpha-equivalent. This allows us to use the implication from the strong cases
+holds. This allows us to use the implication from the strong cases
-lemma and we can discharge all proof-obligations to do with having covered all
+lemma.
-cases.
+Conseqently,  we can discharge all proof-obligations to do with having covered all
-This completes the proof showing that the weak induction principles imply
+cases. This completes the proof showing that the weak induction principles imply
-the strong induction principles. We have automated the reasoning for all
+the strong induction principles.
-term-calculi the user might specify. The feature of the function package
-by Krauss \cite{Krauss09} that allows us to establish an induction principle
-by just finding decreasing measures and showing that the induction principle
-covers all cases, tremendously helped us in implementing the automation.
 *}
 section {* Related Work\label{related} *}
 to impose some restrictions (like a single binding function for a deep
 binder) that are not present in Ott. Our expectation is that we can still
 cover many interesting term-calculi from programming language research, for
 example Core-Haskell (see Figure~\ref{nominalcorehas}).
-\begin{figure}[p!]
+\begin{figure}[t]
 \begin{boxedminipage}{\linewidth}
 \small
 \begin{tabular}{l}
 \isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
 \isacommand{nominal\_datatype}~@{text "tkind ="}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
 \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. 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,
-one obtains automatically a reasoning infrastructure for Core-Haskell.
+one obtains automatically a reasoning infrastructure for Core-Haskell.\bigskip\bigskip
 \label{nominalcorehas}}
 \end{figure}
 Pottier presents a programming language, called C$\alpha$ml, for

changeset 3021	8de43bd80bc2
parent 3019	10fa937255da
child 3022	4de1d6ab04f7