
diff -r 014f0ea2381c -r 65452cf6f5ae LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Fri Sep 16 08:00:15 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Fri Sep 16 10:13:52 2011 +0200
@@ -74,7 +74,7 @@
   ast' ("'(as', t\<PRIME> ')") and
   equ2 ("'(=, =')") and
   supp2 ("'(supp, supp')") and
-  bn_al ("bn\<^sup>\<alpha> _")
+  bn_al ("bn\<^sup>\<alpha> _" [100] 100)
 (*>*)
 
 
@@ -1038,7 +1038,7 @@
 
   
   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
+  comparison to Ott. The main idea behind these restrictions is
   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
@@ -1086,7 +1086,7 @@
 
 
   \noindent
-  In these specifications @{text "name"} refers to an atom type, and @{text
+  In these specifications @{text "name"} refers to a (concrete) atom type, and @{text
   "fset"} to the type of finite sets.  Note that for @{text Lam} it does not
   matter which binding mode we use. The reason is that we bind only a single
   @{text name}, in which case all three binding modes coincide. However, having 
@@ -1113,7 +1113,7 @@
   \hspace{5mm}$\mid$~@{term "App trm trm"}\\
   \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} 
      \;\;\isacommand{binds} @{text x} \isacommand{in} @{text t}\\
-  \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} 
+  \hspace{5mm}$\mid$~@{text "Let_pat p::pat trm t::trm"} 
      \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\
   \isacommand{and} @{text pat} $=$\\
   \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
@@ -1957,37 +1957,35 @@
   on the right):
 
   \begin{equation}\label{inductex}\mbox{
-  \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {}}
-  \begin{tabular}{@ {}c@ {}}
+  \begin{tabular}{c}
+  \multicolumn{1}{@ {\hspace{-5mm}}l}{cases lemmas:}\smallskip\\
   \infer{@{text "P\<^bsub>trm\<^esub>"}}
   {\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 x\<^isub>3. y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
-   \end{array}}\medskip\\
+   @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+   \end{array}}\hspace{10mm}
 
   \infer{@{text "P\<^bsub>pat\<^esub>"}}
   {\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} 
-  &
+  \end{array}}\medskip\\
+
+  \multicolumn{1}{@ {\hspace{-5mm}}l}{induction principle:}\smallskip\\
   
-  \begin{tabular}{@ {}c@ {}}
   \infer{@{text "P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}}
   {\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 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 "\<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_pat\<^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}
   \end{tabular}}
   \end{equation}\smallskip
 
@@ -2116,8 +2114,8 @@
   multiple bound atoms).
 
 
-  For the older versions of Nominal Isabelle we introduced in
-  \cite{UrbanTasson05} a method for automatically strengthening weak induction
+  For the older versions of Nominal Isabelle we described in
+  \cite{Urban08} a method for automatically strengthening weak induction
   principles. These stronger induction principles allow the user to make
   additional assumptions about bound atoms. The advantage of these assumptions
   is that they make in most cases any renaming of bound atoms unnecessary.  To
@@ -2135,7 +2133,7 @@
    @{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 # 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 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)"}\\
+   \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_pat\<^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)"}
@@ -2152,42 +2150,44 @@
   which the additional parameter @{text c} is assumed to be of finite
   support. The purpose of @{text "c"} is to ``control'' which freshness
   assumptions the binders should satisfy in the @{text "Lam\<^sup>\<alpha>"} and
-  @{text "Let\<^sup>\<alpha>"} cases: for @{text "Lam\<^sup>\<alpha>"} we can assume the
+  @{text "Let_pat\<^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
+  "Let_pat\<^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.
+  convention \cite{Urban08}.
 
   In what follows we will show that the induction principle in
   \eqref{inductex} implies \eqref{stronginduct}. This fact was established for
-  single binders in \cite{UrbanTasson05} by some quite involved, nevertheless
+  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
   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. 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.
+  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
+  to do here.
+
 
   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. 
   To do so, we have to derive stronger cases lemmas, which look in our
-  running example as follows:
+  running example are as follows:
 
   \[\mbox{
-  \begin{tabular}{@ {}c@ {\hspace{6mm}}c@ {}}
+  \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
   \infer{@{text "P\<^bsub>trm\<^esub>"}}
   {\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. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-   @{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>"}
+   @{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>"}
    \end{array}} &
 
   \infer{@{text "P\<^bsub>pat\<^esub>"}}
@@ -2200,22 +2200,26 @@
   \]\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
+  They are stronger in the sense that they allow us to assume that the bound
+  atoms avoid a context @{text "c"} (which is assumed to be finitely
+  supported). This is similar with the stronger induction principles. 
+  
+  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
+  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 
+  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>"}
@@ -2225,32 +2229,74 @@
   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
+  \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.
+  "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.
 
-  The @{text "Let\<^sup>\<alpha>"}-case involving a (non-recursive) deep binder is more complicated.
+  The @{text "Let_pat\<^sup>\<alpha>"}-case involving a deep binder is slightly more complicated.
   We have the assumption
 
-  \begin{equation}\label{assm}
-  @{text "y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
+  \begin{equation}\label{assmtwo}
+  @{text "y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
   \end{equation}\smallskip
 
   \noindent
-  and as implication
+  and the implication
+
+  \[
+  @{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
+
+  \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
+  this is not true in cases like (using informal notation)
 
   \[
+  @{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
+  in the assignment. We can, however, obtain obtain such a renaming
+  permutation, say @{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al
+  x\<^isub>1) x\<^isub>3"}. So we have \mbox{@{term "set (bn_al (\<pi> \<bullet>
+  x\<^isub>1)) \<sharp>* c"}} and @{term "Abs_lst (bn_al (\<pi> \<bullet> x\<^isub>1)) (\<pi> \<bullet>
+  x\<^isub>3) = Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text "bn\<^sup>\<alpha>"} are equivariant).  
+  Now the quasi-injective property for @{text "Let_pat\<^sup>\<alpha>"} states
+
+  \[
+  \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>"} 
+  (hence @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}), we can infer the 
+  equation
 
-  The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
+  \[
+  @{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
+  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




