# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1316164874 -7200
# Node ID 10fa937255da919710a25fece101a5e83731def6
# Parent  65452cf6f5ae34a0d6187546581b7ebdab4c1ba4
all material

diff -r 65452cf6f5ae -r 10fa937255da LMCS-Paper/Paper.thy
--- 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. 
 *}