# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270130934 -7200
# Node ID 39a6c6db90f6cbabc3ec0c647252061dacbe5475
# Parent  0ce4f938e8cc5458f3705a52eeaac19e208ccbca
fixed alpha_bn

diff -r 0ce4f938e8cc -r 39a6c6db90f6 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Apr 01 15:41:48 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 16:08:54 2010 +0200
@@ -1407,15 +1407,20 @@
   then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
 
 
-  The definition of the alpha-equivalence relations @{text "\<approx>bn"} for binding functions 
-  are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}. We
-  need to generate premises for each pair @{text "(x\<^isub>i, y\<^isub>i)"} depending on whether @{text "x\<^isub>i"} 
-  occurs in @{text "rhs"} of  the clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:
+  The definitions of the alpha-equivalence relations @{text "\<approx>bn"} for binding functions 
+  are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}
+  and need to generate appropriate premises. We generate first premises according to the first three
+  rules given above. Only the ``left-over'' pairs  @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated 
+  differently. They depend on whether @{text "x\<^isub>i"}  occurs in @{text "rhs"} of  the 
+  clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
   $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
-  and the type of @{text "x\<^isub>i"} is @{text "ty"}\\
+  and the type of @{text "x\<^isub>i"} is @{text ty} and @{text "x\<^isub>i"} is a recursive argument 
+  in the term-constructor\\
+  $\bullet$ & @{text "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
+  and @{text "x\<^isub>i"} is not a recursive argument in the term-constructor\\
   $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} occurs in @{text rhs}
   with the recursive call @{text "bn x\<^isub>i"}\\
   $\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not
@@ -1423,7 +1428,7 @@
   \end{tabular}
   \end{center}
 
-   Again lets take a look at an example for these definitions. For \eqref{letrecs}
+  Again lets take a look at an example for these definitions. For \eqref{letrecs}
   we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
   $\approx_{\textit{bn}}$, with the clauses as follows: