--- a/LMCS-Paper/Paper.thy Fri Sep 16 10:13:52 2011 +0200
+++ b/LMCS-Paper/Paper.thy Fri Sep 16 11:21:14 2011 +0200
@@ -2292,127 +2292,88 @@
Taking the left-hand side as our assumption in \eqref{assmtwo}, we can use
the implication 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 that are free.
-
-
- to the whole term @{text "Let_pat x\<^isub>1 x\<^isub>2 x\<^isub>3"},
- 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}
+ 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{}.
+ Then @{text "(\<pi> \<bullet> x\<^isub>1)
+ \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. In such
+ cases, however, we only want to rename binders that will become bound, which
+ does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. The problem is that the
+ permutation operation @{text "\<bullet>"} permutes all of them. The remedy is to
+ introduce an auxiliary permutation operation, written @{text "_
+ \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permute bound atoms and
+ leaves the other atoms unchanged. Like the @{text
+ "fa_bn"}$_{1..m}$-functions, we can define this operation over raw terms
+ analysing how the @{text "bn"}$_{1..m}$-functions are defined and then lift
+ them to alpha-equivalent terms. Assuming the user specified a clause
- {\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
+ \[
+ @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}
+ \]\smallskip
-
-
- \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"}}\\
- \text{@{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\
- \text{@{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise}
- \end{cases}$
- \end{center}
-
\noindent
- with @{text "y\<^isub>i"} determined as follows:
-
- \begin{center}
+ we define @{text "\<pi> \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} with @{text "y\<^isub>i"} determined as follows:
+
+ \[\mbox{
\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
- $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
- $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
- \end{tabular}
- \end{center}
-
- \noindent
- Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
- @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
- 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.
-
-
- 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
-
- \begin{center}
- @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"},
- \end{center}
+ $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+ $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet> x\<^isub>i"} otherwise
+ \end{tabular}}
+ \]\smallskip
- \noindent
- then 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"}
- \end{center}
-
\noindent
- with @{text "y\<^isub>i"} determined as follows:
-
- \begin{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
- $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
- $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
- \end{tabular}
- \end{center}
-
- \noindent
- Using again the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
- alpha-equated terms. We can then prove the following two facts
+ 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 p}
- {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
- @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
+ Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text "\<pi>"}\\
+ {\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 equations follow by simple unfolding
+ By induction on @{text x}. The properties follow by simple unfolding
of the definitions.
\end{proof}
\noindent
The first property states that a permutation applied to a binding function is
equivalent to first permuting the binders and then calculating the bound
- atoms. The second amounts to the fact that permuting the binders has no
- effect on the free-atom function. The main point of this permutation
- function, however, is that if we have a permutation that is fresh
- for the support of an object @{text x}, then we can use this permutation
- to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the
- @{text "Let"} term-constructor from the example shown
- in \eqref{letpat} this means for a permutation @{text "r"}
+ atoms. The main point of the auxiliary permutation
+ functions is that it allows us to rename just the binders in a term,
+ without changing anything else.
- \begin{equation}\label{renaming}
- \begin{array}{l}
- \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \<sharp>* r"}}\\
- \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
- \end{array}
- \end{equation}
+ 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}
+ 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"}
+ \]\smallskip
\noindent
- This fact will be crucial when establishing the strong induction principles below.
+ 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)}
+ 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
+ lemma and we can discharge all proof-obligations to do with having covered all
+ cases.
This completes the proof showing that the weak induction principles imply
- the strong induction principles.
- }
+ the strong induction principles. We have automated the reasoning for all
+ 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.
*}