nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:799769b40f0e
+:014f0ea2381c
 @{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 it is straightforward using \eqref{abseqiff} 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
 "(a \<rightleftharpoons> b)"}.
 \end{proof}
 an example.
 There are also some restrictions we need to impose on our binding clauses in
 comparison to the ones of Ott. The main idea behind these restrictions is
-that we obtain a sensible notion of alpha-equivalence where it is ensured
+that we obtain a notion of alpha-equivalence where it is ensured
 that within a given scope an atom occurrence cannot be both bound and free
 at the same time.  The first restriction is that a body can only occur in
 \emph{one} binding clause of a term constructor. So for example
 \[\mbox{
 \end{tabular}}
 \end{equation}\smallskip
 \noindent
 In this example the term constructor @{text "ACons'"} has four arguments with
-a binding clause for two of them. This constructor is also used in the definition
+a binding clause involving two of them. This constructor is also used in the definition
 of the binding function. The restriction we have to impose is that the
-binding function can only return free atoms, that is the ones that are not
+binding function can only return free atoms, that is the ones that are \emph{not}
 mentioned in a binding clause.  Therefore @{text "y"} cannot be used in the
 binding function @{text "bn"} (since it is bound in @{text "ACons'"} by the
 binding clause), but @{text x} can (since it is a free atom). This
 restriction is sufficient for lifting the binding function to alpha-equated
-terms. If we would permit that @{text "bn"} can also return @{text "y"},
+terms. If we would permit @{text "bn"} to return @{text "y"},
-then it would not be respectful and therefore cannot be lifted.
+then it would not be respectful and therefore cannot be lifted to
+alpha-equated lambda-terms.
 In the version of Nominal Isabelle described here, we also adopted the
 restriction from the Ott-tool that binding functions can only return: the
 empty set or empty list (as in case @{text ANil'}), a singleton set or
 singleton list containing an atom (case @{text PVar} in \eqref{letpat}), or
 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 on the ``raw'' type @{text "ty"}.
+@{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor in the ``raw'' type @{text "ty"},
+respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor in @{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).
 @{text "fa_bn"}\mbox{$_{1..m}$}.
 \]\smallskip
 \noindent
 The reason for this setup is that in a deep binder not all atoms have to be
-bound, as we saw in the example with ``plain'' @{text Let}s. We need
+bound, as we saw in \eqref{letrecs} with the example of ``plain'' @{text Let}s. We need
 therefore functions that calculate those free atoms in deep binders.
 While the idea behind these free-atom functions is simple (they just
 collect all atoms that are not bound), because of our rather complicated
 binding mechanisms their definitions are somewhat involved.  Given
 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}
 we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
-$\approx_{\textit{bn}}$ with the following clauses:
+$\approx_{\textit{bn}}$ with the following rules:
 \begin{equation}\label{rawalpha}\mbox{
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
 {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} &
 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 (e.g.~in the @{text "Let_rec"}-case)
+Note also that in case of more than one body (that is in the @{text "Let_rec"}-case)
 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.
+corresponding binding clause specifies a binder with two bodies, namely
+@{text "as"} and @{text "t"}.
 *}
 section {* Establishing the Reasoning Infrastructure *}
 text {*
 The relations @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ are
 equivalence relations.
 \end{lem}
 \begin{proof}
-The proof is by induction over the definitions. The non-trivial
+The proofs are by induction. The non-trivial
 cases involve premises built up by $\approx_{\textit{set}}$,
 $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They
 can be dealt with as in Lemma~\ref{alphaeq}. However, the transitivity
 case needs in addition the fact that the relations are equivariant.
 \end{proof}
 restriction imposed on the form of the binding functions---namely \emph{not}
 to return any bound atoms. In Ott, in contrast, the user may define @{text
 "bn"}$_{1..m}$ so that they return bound atoms and in this case the third
 implication is \emph{not} true. A result is that in general the lifting of the
 corresponding binding functions in Ott to alpha-equated terms is impossible.
 Having established respectfulness for the ``raw'' term-constructors, the
 quotient package is able to automatically deduce \eqref{distinctalpha} from
-\eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can
+\eqref{distinctraw}.
-also lift properties that characterise when two ``raw'' terms of the form
+Next we can lift the permutation operations defined in \eqref{ceqvt}. In
+order to make this lifting to go through, we have to show that the
+permutation operations are respectful. This amounts to showing that the
+alpha-equivalence relations are equivariant, which
+we already established in Lemma~\ref{equiv}. As a result we can add the
+equations
+\begin{equation}\label{calphaeqvt}
+@{text "\<pi> \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) \<dots> (\<pi> \<bullet> x\<^isub>r)"}
+\end{equation}\smallskip
+\noindent
+to our infrastructure. In a similar fashion we can lift the defining equations
+of the free-atom functions @{text "fa_ty\<AL>"}$_{1..n}$ and
+@{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
+"bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.
+The latter are defined automatically for the ``raw'' types @{text "ty"}$_{1..n}$
+by the datatype package of Isabelle/HOL.
+We also need to lift the properties that characterise when two ``raw'' terms of the form
 \[
 \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
 \]\smallskip
 \[
 @{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
+We call these conditions as \emph{quasi-injectivity}. They correspond to the
-the premises in our alpha-equiva\-lence relations, with the exception that
+premises in our alpha-equiva\-lence relations, with the exception that the
-in case of binders the relations @{text "\<approx>ty"}$_{1..n}$ are all replaced
+relations @{text "\<approx>ty"}$_{1..n}$ are all replaced by equality (and similarly
-by equality. Recall the alpha-equivalence rules for @{text "Let"} and @{text "Let_rec"}
+the free-atom and binding functions are replaced by their lifted
-shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"} we have
+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
 \begin{equation}\label{alphalift}\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 fa_trm_al (bn as', t')"} &
 \makebox[0mm]{\infer{@{text "Let_rec\<^sup>\<alpha> as t = Let_rec\<^sup>\<alpha> as' t'"}}
 {@{term "alpha_lst_ex (bn_al as, ast) equ2 fa_trm2_al (bn_al as', ast')"}}}\\
 \end{tabular}}
 \end{equation}\smallskip
-\noindent
+We can also add to our infrastructure cases lemmas and a (mutual)
-where @{text "\<approx>\<^bsub>trm\<^esub>"} and @{text "\<approx>\<^bsub>assn\<^esub>"} are replaced by @{text "="} (and similarly
-the free-atom and binding functions are replaced by their lifted counterparts).
-Next we can lift the permutation operations defined in \eqref{ceqvt}. In
-order to make this lifting to go through, we have to show that the
-permutation operations are respectful. This amounts to showing that the
-alpha-equivalence relations are equivariant, which
-we already established in Lemma~\ref{equiv}. As a result we can add the
-equations
-\begin{equation}\label{calphaeqvt}
-@{text "\<pi> \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) \<dots> (\<pi> \<bullet> x\<^isub>r)"}
-\end{equation}\smallskip
-\noindent
-to our infrastructure. In a similar fashion we can lift the defining equations
-of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and
-@{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
-"bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.
-The latter are defined automatically for the ``raw'' types @{text "ty"}$_{1..n}$
-by the datatype package of Isabelle/HOL.
-Finally we can add to our infrastructure cases lemmas and a (mutual)
 induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases
 lemmas allow the user to deduce a property @{text "P"} by exhaustively
 analysing how an element in a type, say @{text "ty\<AL>"}$_i$, can be
 constructed (that means one case for each of the term-constructors in @{text
 "ty\<AL>"}$_i\,$). The lifted cases lemma for the type @{text
 \noindent
 whereby the @{text P}$_{1..n}$ are the properties established by the induction
 and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$. Note that
 the induction principle has for the term constructors @{text "C"}$^\alpha_1$ a
-premise of the form
+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
 \eqref{cases} and \eqref{induct} boil down 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@ {\hspace{10mm}}c}
+\begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {}}
 \begin{tabular}{@ {}c@ {}}
 \infer{@{text "P\<^bsub>trm\<^esub>"}}
-{\begin{array}{l}
+{\begin{array}{@ {}l@ {}}
 @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-@{text "\<forall>x\<^isub>1 x\<^isub>2. y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
 \end{array}}\medskip\\
 \infer{@{text "P\<^bsub>pat\<^esub>"}}
-{\begin{array}{l}
+{\begin{array}{@ {}l@ {}}
 @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
 @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
 \end{array}}
 \end{tabular}
 &
 \begin{tabular}{@ {}c@ {}}
 \infer{@{text "P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}}
-{\begin{array}{l}
+{\begin{array}{@ {}l@ {}}
 @{text "\<forall>x. P\<^bsub>trm\<^esub> (Var\<^sup>\<alpha> x)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-@{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
 @{text "P\<^bsub>pat\<^esub> (PNil\<^sup>\<alpha>)"}\\
 @{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
 \end{array}}
 \end{tabular}
 "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.  This fact
 is important in the nominal setting where the general theory is formulated
 in terms of support and freshness, but also provides evidence that our
 notions of free-atoms and alpha-equivalence ``match up''.
-\begin{thm}
+\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}
 \begin{proof}
-The proof is by induction. In each case
+The proof is by induction on @{text "x"}$_{1..n}$. In each case
 we unfold the definition of @{text "supp"}, move the swapping inside the
 term-constructors and then use the quasi-injectivity lemmas in order to complete the
 proof. For the abstraction cases we use then the facts derived in Theorem~\ref{suppabs},
 for which we have to know that every body of an abstraction is finitely supported.
 This, we have proved earlier.
 {@{term "alpha_lst_ex (bn_al as, ast) equ2 supp2 (bn_al as', ast')"}}}\\
 \end{tabular}}
 \]\smallskip
 \noindent
-Taking the fact into account that @{term "equ2"} and @{term "supp2"} are
+Taking the fact into account that the compound equivalence relation @{term
-by definition equal to @{term "equal"} and @{term "supp"}, respectively,
+"equ2"} and the compound free-atom function @{term "supp2"} are by
-the above rules simplify even further to
+definition equal to @{term "equal"} and @{term "supp"}, respectively, the
+above rules simplify even 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'"} &
 {@{term "Abs_lst (bn_al as) ast = Abs_lst (bn_al as') ast'"}}}\\
 \end{tabular}}
 \]\smallskip
 \noindent
-which means we can characterise equality between term-constructors in terms
+which means we can characterise equality between term-constructors (on the
-of equality between the abstractions defined in Section~\ref{sec:binders}. From this
+alpha-equated level) in terms of equality between the abstractions defined
-we can derive the support for @{text "Let\<^sup>\<alpha>"} and
+in Section~\ref{sec:binders}. From this we can deduce the support for @{text
-@{text "Let_rec\<^sup>\<alpha>"}, namely
+"Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"}, namely
 \[\mbox{
 \begin{tabular}{l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
 @{text "supp (Let\<^sup>\<alpha> as t)"} & @{text "="} & @{text "(supp t - set (bn\<^sup>\<alpha> as)) \<union> fa\<AL>\<^bsub>bn\<^esub> as"}\\
 @{text "supp (Let_rec\<^sup>\<alpha> as t)"} & @{text "="} & @{text "(supp t \<union> supp as) - set (bn\<^sup>\<alpha> as)"}\\
 section {* Strong Induction Principles *}
 text {*
 In the previous section we derived induction principles for alpha-equated
-terms (see \eqref{induct} and \eqref{inductex}). This was done by lifting
+terms (see \eqref{induct} for the general form and \eqref{inductex} for an
-the corresponding inductions principles for ``raw'' terms.  We already
+instance). This was done by lifting the corresponding inductions principles
-employed these induction principles in order to derive several facts for
+for ``raw'' terms.  We already employed these induction principles for
-alpha-equated terms, including the property that the free-variable functions
+deriving several facts for alpha-equated terms, including the property that
-and the notion of support coincide. Still, we call these induction
+the free-variable functions and the notion of support coincide. Still, we
-principles \emph{weak}, because for a term-constructor, say \mbox{@{text
+call these induction principles \emph{weak}, because for a term-constructor,
-"C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction hypothesis requires us to
+say \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction
-establish (under some assumptions) a property @{text "P (C\<^sup>\<alpha>
+hypothesis requires us to establish (under some assumptions) a property
-x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text "x"}$_{1..r}$. The problem is that in the
+@{text "P (C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text
-presence of binders we cannot make any assumptions about the atoms that are
+"x"}$_{1..r}$. The problem is that in the presence of binders we cannot make
-bound, and we have to potentially rename them. This renaming has to be
+any assumptions about the atoms that are bound. One obvious way around this
-done manually and is often very cumbersome (especially in the case for
+problem is to rename them. Unfortunately, this leads to very clunky proofs
+and makes formalisations grievous experiences (especially in the case for
 multiple bound atoms).
 For the older versions of Nominal Isabelle we introduced in
 \cite{UrbanTasson05} a method for automatically strengthening weak induction
-principles in case of single binders. These stronger induction principles
+principles. These stronger induction principles allow the user to make
-allow the user to make additional assumptions about bound atoms. The main
+additional assumptions about bound atoms. The advantage of these assumptions
-point is that these additional assumptions amount to a formal version of the
+is that they make in most cases any renaming of bound atoms unnecessary.  To
-informal variable convention for binders and nearly always make manual
+explain how the strengthening works in the presence of multiple binders, we
-renaming of binders unnecessary.
+use as running example the lambda-calculus with @{text "Let"}-patterns shown
+in \eqref{letpat}. Its weak induction principle is given in
-To explain how the strengthening works in the presence of multiple binders,
+\eqref{inductex}.  The stronger induction principle is as follows:
-we use as running example the lambda-calculus with @{text "Let"}-patterns
-shown in \eqref{letpat}. Its weak induction principle is given in \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"}}
 {\begin{array}{l}
 @{text "\<forall>x c. P\<^bsub>trm\<^esub> c (Var\<^sup>\<alpha> x)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-@{text "\<forall>x\<^isub>1 x\<^isub>2 c. {atom x\<^isub>1} #\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+@{text "\<forall>x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-@{text "\<forall>x\<^isub>1 x\<^isub>2 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and>"}\\
+\hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
 @{text "\<forall>c. P\<^bsub>pat\<^esub> c (PNil\<^sup>\<alpha>)"}\\
 @{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\
 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
 \end{array}}
 \end{tabular}}
 \end{equation}\smallskip
 \noindent
-Instead of establishing the two properties @{text " P\<^bsub>trm\<^esub> y\<^isub>1 \<and>
+Instead of establishing the two properties @{text " P\<^bsub>trm\<^esub>
-P\<^bsub>pat\<^esub> y\<^isub>2"}, as the weak one does, the stronger
+y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}, as the weak one does, the
-induction principle establishes the properties @{text " P\<^bsub>trm\<^esub> c
+stronger induction principle establishes the properties @{text "
-y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional
+P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"} in
-parameter @{text c} is assumed to be of finite support. The purpose of
+which the additional parameter @{text c} is assumed to be of finite
-@{text "c"} is to ``control'' which freshness assumptions the binders should
+support. The purpose of @{text "c"} is to ``control'' which freshness
-satisfy in the @{text "Lam\<^sup>\<alpha>"} and @{text "Let\<^sup>\<alpha>"} cases (these are the cases
+assumptions the binders should satisfy in the @{text "Lam\<^sup>\<alpha>"} and
-where the user specified some binding clauses).
+@{text "Let\<^sup>\<alpha>"} cases: for @{text "Lam\<^sup>\<alpha>"} we can assume the
+bound atom @{text "x\<^isub>1"} is fresh for @{text "c"}; for @{text
+"Let\<^sup>\<alpha>"} we can assume all bound atoms from an assignment are fresh
+for @{text "c"}. If @{text "c"} is instantiated appropriately, the user can
+mimic the ``pencil-and-paper'' reasoning employing the usual variable
+convention.
 In what follows we will show that the induction principle in
-\eqref{inductex} implies \eqref{stronginduct}. This fact was established in
+\eqref{inductex} implies \eqref{stronginduct}. This fact was established for
-\cite{UrbanTasson05} by some quite involved, nevertheless automated,
+single binders in \cite{UrbanTasson05} by some quite involved, nevertheless
-induction proof. In this paper we simplify the proof by leveraging the
+automated, induction proof. In this paper we simplify the proof by
-automated proof methods from the function package of Isabelle/HOL
+leveraging the automated proof methods from the function package of
-\cite{Krauss09}. The reasoning principle behind these methods is
+Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these methods
-well-founded induction. To use them in our setting, we have to discharge two
+is well-founded induction. To use them in our setting, we have to discharge
-proof obligations: one is that we have well-founded measures (one for each type
+two proof obligations: one is that we have well-founded measures (one for
-@{text "ty"}$^\alpha_{1..n}$) that decrease in every induction step and the
+each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
-other is that we have covered all cases.
+step and the other is that we have covered all cases. 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 to do.
 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 these measures decrease in every
+is straightforward to establish that the sizes decrease in every
 induction step. What is left to show is that we covered all cases.
-To do so, we use a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat}
+To do so, we have to derive stronger cases lemmas, which look in our
-this lemma is of the form
+running example as follows:
-\begin{equation}\label{weakcases}
+\[\mbox{
+\begin{tabular}{@ {}c@ {\hspace{6mm}}c@ {}}
 \infer{@{text "P\<^bsub>trm\<^esub>"}}
-{\begin{array}{l@ {\hspace{9mm}}l}
+{\begin{array}{@ {}l@ {}}
-@{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+@{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-@{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+@{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-\end{array}}\\[-1mm]
+@{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}
+@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+\end{array}} &
-where we have a premise for each term-constructor.
-The idea behind such cases lemmas is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
+\infer{@{text "P\<^bsub>pat\<^esub>"}}
-provided we can show that this property holds if we substitute for @{text "t"} all
+{\begin{array}{@ {}l@ {}}
-possible term-constructors.
+@{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
+@{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
+@{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
+\end{array}}
+\end{tabular}}
+\]\smallskip
+\noindent
+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 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\<^sup>\<alpha>"}. There the
+stronger cases lemma allow us to assume that the bound atoms avoid the context @{text "c"}
+(which is assumed to be finitely supported).
+Let us show first establish the simpler case for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma
+\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 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
+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
+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
+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
+"Lam\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}. We can use this in the assumption
+\eqref{assm} and then use \eqref{imp} to conclude this case.
+The @{text "Let\<^sup>\<alpha>"}-case involving a (non-recursive) deep binder is more complicated.
+We have the assumption
+\begin{equation}\label{assm}
+@{text "y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
+\end{equation}\smallskip
+\noindent
+and as implication
+\[
+\]\smallskip
+The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
+because @{text p} might contain names bound by @{text bn}, but also some that are
+free. To solve this problem we have to introduce a permutation function that only
+permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
+by lifting. For a
+clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define
+{\bf NOT DONE YET}
+{\it
 The only remaining difficulty is that in order to derive the stronger induction
 principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that
 in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and
 \emph{all} @{text Let}-terms.
 What we need instead is a cases lemma where we only have to consider terms that have
 binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications
-\begin{center}
-\begin{tabular}{l}
-@{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-@{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\[-2mm]
-\end{tabular}
-\end{center}
-\noindent
-which however can be relatively easily be derived from the implications in \eqref{weakcases}
-by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know
-that @{text "{atom a} \<FRESH>\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with
-a permutation @{text q}, such that @{text "{atom (q \<bullet> a)} \<FRESH>\<^sup>* c"} and
-@{text "supp (Lam a t) \<FRESH>\<^sup>* q"} hold.
-By using Property \ref{supppermeq}, we can infer from the latter
-that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"}
-and we are done with this case.
-The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated.
-The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
-because @{text p} might contain names bound by @{text bn}, but also some that are
-free. To solve this problem we have to introduce a permutation function that only
-permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
-by lifting. For a
-clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define
 \begin{center}
 @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}  with
 $\begin{cases}
 \text{@{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\
 is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}.
 These facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
 completes the non-trivial cases in \eqref{letpat} for strengthening the corresponding induction
 principle.
-A natural question is
-whether we can also strengthen the weak induction principles involving
-the general binders presented here. We will indeed be able to so, but for this we need an
-additional notion for permuting deep binders.
 Given a binding function @{text "bn"} we define an auxiliary permutation
 operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
 Assuming a clause of @{text bn} is given as
 \noindent
 This fact will be crucial when establishing the strong induction principles below.
-In our running example about @{text "Let"}, the strong induction
-principle means that instead
-of establishing the implication
-\begin{center}
-@{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
-\end{center}
-\noindent
-it is sufficient to establish the following implication
-\begin{equation}\label{strong}
-\mbox{\begin{tabular}{l}
-@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
-\hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
-\hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
-\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
-\end{tabular}}
-\end{equation}
-\noindent
-While this implication contains an additional argument, namely @{text c}, and
-also additional universal quantifications, it is usually easier to establish.
-The reason is that we have the freshness
-assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily
-chosen by the user as long as it has finite support.
-Let us now show how we derive the strong induction principles from the
-weak ones. In case of the @{text "Let"}-example we derive by the weak
-induction the following two properties
-\begin{equation}\label{hyps}
-@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm}
-@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
-\end{equation}
-\noindent
-For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}
-assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}).
-By Property~\ref{avoiding} we
-obtain a permutation @{text "r"} such that
-\begin{equation}\label{rprops}
-@{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
-@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
-\end{equation}
-\noindent
-hold. The latter fact and \eqref{renaming} give us
-\begin{center}
-\begin{tabular}{l}
-@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
-\hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
-\end{tabular}
-\end{center}
-\noindent
-So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
-establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
-To do so, we will use the implication \eqref{strong} of the strong induction
-principle, which requires us to discharge
-the following four proof obligations:
-\begin{center}
-\begin{tabular}{rl}
-{\it (i)} &   @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
-{\it (ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
-{\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
-{\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
-\end{tabular}
-\end{center}
-\noindent
-The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the
-others from the induction hypotheses in \eqref{hyps} (in the fourth case
-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 weak induction principles imply
 the strong induction principles.
+}
 *}
 section {* Related Work\label{related} *}

changeset 3017	014f0ea2381c
parent 3016	799769b40f0e
child 3018	65452cf6f5ae