diff -r 6ca795b1cd76 -r 26e44bcddb5b Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Apr 02 07:59:03 2010 +0200
+++ b/Paper/Paper.thy	Fri Apr 02 13:12:10 2010 +0200
@@ -1485,7 +1485,7 @@
 
   \noindent 
   We can feed this lemma into our quotient package and obtain new types @{text
-  "ty"}$^\alpha_{1..n}$ representing alpha-equated terms. We also obtain 
+  "ty\<AL>\<^bsub>1..n\<^esub>"} representing alpha-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain 
   definitions for the term-constructors @{text
   "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
   "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text
@@ -1516,16 +1516,16 @@
   package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} 
   are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
   Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
-  @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, then respectfulness amounts to showing
+  @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that
   
   \begin{center}
-  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
+  @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}
   \end{center}  
 
   \noindent
   are alpha-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
-  and  @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments. We can prove this by 
-  analysing the definition of @{text "\<approx>ty"}. For this to succeed we have to establish 
+  and  @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments of @{text "C\<^isub>i"}. We can prove this by 
+  analysing the definition of @{text "\<approx>ty"}. For this proof to succeed we have to establish 
   the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined 
   for the type @{text ty\<^isub>i}, we have that
   %
@@ -1538,10 +1538,10 @@
    
   Having established respectfulness for every raw term-constructor, the 
   quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.
-  In fact we can from now on lift any fact from the raw level to the alpha-equated level that
-  apart from variables only contains the raw term-constructors. The 
-  induction principles derived by the datatype package in Isabelle/HOL for teh types @{text
-  "ty"}$^\alpha_{1..n}$ fall into this category. So we can also add to our infrastructure
+  In fact we can from now on lift facts from the raw level to the alpha-equated level
+  as long as they contain raw term-constructors only. The 
+  induction principles derived by the datatype package in Isabelle/HOL for the types @{text
+  "ty\<AL>\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
   induction principles that establish
 
   \begin{center}
@@ -1550,7 +1550,7 @@
 
   \noindent
   for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<^isub>i\<^esub>"} stand for properties
-  defined over the types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. The premises of 
+  defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of 
   these induction principles look
   as follows
 
@@ -1567,32 +1567,33 @@
   we have to know that the permutation operations are respectful 
   w.r.t.~alpha-equivalence. 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
+  in Lemma~\ref{equiv}. As a result we can establish the equations
   
   \begin{equation}\label{ceqvt}
   @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
   \end{equation}
 
   \noindent
-  to our infrastructure. In a similar fashion we can lift the equations
-  characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and the 
+  for our infrastructure. In a similar fashion we can lift the equations
+  characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the 
   binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for this
-  lifting are the two properties:
+  lifting are the properties:
   %
   \begin{equation}\label{fnresp}
   \mbox{%
   \begin{tabular}{l}
   @{text "x \<approx>ty\<^isub>j y"} implies @{text "fv_ty\<^isub>j x = fv_ty\<^isub>j y"}\\
-  @{text "x \<approx>ty\<^isub>j y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"}
+  @{text "x \<approx>ty\<^isub>k y"} implies @{text "fv_bn\<^isub>k x = fv_bn\<^isub>k y"}\\
+  @{text "x \<approx>ty\<^isub>k y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"}
   \end{tabular}}
   \end{equation}
 
   \noindent
   which can be established by induction on @{text "\<approx>ty"}. Whereas the first
   property is always true by the way how we defined the free-variable
-  functions, the second does \emph{not} hold in general. There is, in principle, 
+  functions for types, the second and third do \emph{not} hold in general. There is, in principle, 
   the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound
-  variable. Then the second property is just not true. However, our 
+  variable. Then the third property is just not true. However, our 
   restrictions imposed on the binding functions
   exclude this possibility.
 
@@ -1613,36 +1614,38 @@
 
   \noindent
   We call these conditions as \emph{quasi-injectivity}. Except for one function, which
-  we have to lift in the next section, this stage completes
-  the lifting part of establishing the reasoning infrastructure. From
-  now on, we can almost completely ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only
-  reason about @{text "ty\<AL>\<^bsub>1..n\<^esub>"}.
+  we have to lift in the next section, we completed
+  the lifting part of establishing the reasoning infrastructure. 
 
-  We can first show that the free-variable functions and binding functions
+  Working bow completely on the alpha-equated level, we can first show that 
+  the free-variable functions and binding functions
   are equivariant, namely
 
   \begin{center}
   \begin{tabular}{rcl}
   @{text "p \<bullet> (fv_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fv_ty\<^sup>\<alpha> (p \<bullet> x)"}\\
+  @{text "p \<bullet> (fv_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fv_bn\<^sup>\<alpha> (p \<bullet> x)"}\\
   @{text "p \<bullet> (bn\<^sup>\<alpha> x)"}    & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"}
   \end{tabular}
   \end{center}
 
   \noindent
-  These two properties can be established by structural induction over the @{text x}.
+  These properties can be established by structural induction over the @{text x}
+  (using the induction principles we lifted above for the types @{text "ty\<AL>\<^bsub>1..n\<^esub>"}).
 
-  Until now we have not yet derived any fact about the support of the 
-  alpha-equated terms. Using the equivariance properties in \eqref{ceqvt} we can
+  Until now we have not yet derived anything about the support of the 
+  alpha-equated terms. This however will be necessary in order to derive
+  the strong induction principles in the next section.
+  Using the equivariance properties in \eqref{ceqvt} we can
   show for every term-constructor @{text "C\<^sup>\<alpha>"} that 
 
   \begin{center}
-  @{text "supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}.
+  @{text "(supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
   \end{center}
  
   \noindent
-  This together with Property~\ref{supportsprop} allows us to show
+  holds. This together with Property~\ref{supportsprop} allows us to show
  
-
   \begin{center}
   @{text "finite (supp x\<^isub>i)"}
   \end{center}
@@ -1660,16 +1663,16 @@
   \begin{proof}
   The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case
   we unfold the definition of @{text "supp"}, move the swapping inside the 
-  term-constructors and the use the quasi-injectivity lemmas in order to complete the
-  proof.
+  term-constructors and the use then quasi-injectivity lemmas in order to complete the
+  proof. For the abstraction cases we use the facts derived in Theorem~\ref{suppabs}.
   \end{proof}
 
   \noindent
-  To sum up this section, we established a reasoning infrastructure
+  To sum up, we can established automatically a reasoning infrastructure
   for the types @{text "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"} 
   by first lifting definitions from the raw level to the quotient level and
   then establish facts about these lifted definitions. All necessary proofs
-  are generated automatically by custom ML-code we implemented. This code can deal with 
+  are generated automatically by custom ML-code. This code can deal with 
   specifications like the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.  
 
   \begin{figure}[t!]
@@ -1750,7 +1753,7 @@
 text {*
   In the previous section we were able to provide induction principles that 
   allow us to perform structural inductions over alpha-equated terms. 
-  We call such induction principles \emph{weak}, because in case of a term-contructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},
+  We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},
   the induction hypothesis requires us to establish the implication
   %
   \begin{equation}\label{weakprem}
@@ -1759,10 +1762,9 @@
 
   \noindent
   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 
-  The problem with this implication is that in general it is not easy to establish this
-  implication
+  The problem with this implication is that in general it is not easy to establish it.
   The reason is we cannot make any assumption about the binders in @{text "C\<^sup>\<alpha>"} 
-  (for example we cannot assume the variable convention).
+  (for example we cannot assume the variable convention for them).
 
   In \cite{UrbanTasson05} we introduced a method for automatically
   strengthening weak induction principles for terms containing single
@@ -1772,12 +1774,12 @@
   version of the informal variable convention for binders. A natural question is
   whether we can also strengthen the weak induction principles involving
   general binders. We will indeed be able to so, but for this we need an 
-  additional notion of permuting deep binders. 
+  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.
-  Given a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
-  %
+  Assuming a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
+  we define  %
   \begin{center}
   @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"}
   \end{center}
@@ -1795,9 +1797,10 @@
   
   \noindent
   Using the quotient package again we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
-  alpha-equated terms. We can then prove:
+  alpha-equated terms. We can then prove the following two facts
 
-  \begin{lemma} Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
+  \begin{lemma}\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>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"} and {\it ii)}
     @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.
   \end{lemma}
@@ -1814,96 +1817,103 @@
   effect on the free-variable 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, without ``changing'' the term. In case of the 
+  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:
-
-  \begin{center}
-  if @{term "supp (Abs_lst (bn p) t)  \<sharp>* q"} then @{text "Let p t = Let (q \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) (q \<bullet> t)"}
-  \end{center}
+  \eqref{letpat} this means for a permutation @{text "r"}:
+  %
+  \begin{equation}\label{renaming}
+  \mbox{if @{term "supp (Abs_lst (bn p) t)  \<sharp>* r"} 
+  then @{text "Let p t = Let (r \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) (r \<bullet> t)"}}
+  \end{equation}
 
   \noindent
   This fact will be used when establishing the strong induction principles. 
-  They state that instead of establishing the implication 
+  
+
+  In our running example about @{text "Let"}, they state 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)"}
+  @{text "\<forall>p t. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t)"}
   \end{center}
 
   \noindent
   it is sufficient to establish the following implication
-  
+  %
+  \begin{equation}\label{strong}
+  \mbox{\begin{tabular}{l}
+  @{text "\<forall>p t c."}\\
+  \hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t)"}\\
+  \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}
+  \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 can make 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>\<^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)"} 
+  assuming \eqref{hyps} as induction hypotheses. 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)) \<sharp>* r"}
+  \end{equation}
+
+  \noindent
+  hold. The latter fact and \eqref{renaming} give us
+
   \begin{center}
-  \begin{tabular}{l}
-  @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
-  \hspace{5mm}@{text "set (bn\<^sup>\<alpha> 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)"}
+  @{text "Let (q \<bullet> p) (q \<bullet> t) = Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (r \<bullet> (q \<bullet> t))"}
+  \end{center}
+
+  \noindent
+  So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t)"}, we are can equally
+  establish
+
+  \begin{center}
+  @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (r \<bullet> (q \<bullet> t)))"}
+  \end{center}
+
+  \noindent
+  To do so, we will use the implication \eqref{strong} of the strong induction
+  principle, which requires us to discharge
+  the following three proof obligations:
+
+  \begin{center}
+  \begin{tabular}{rl}
+  {\it i)} &   @{text "set (bn (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
+  {\it ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
+  {\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t))"}\\
   \end{tabular}
   \end{center}
 
-  \noindent 
-  While this implication contains an additional argument, @{text c}, and 
-  also additional universal quantifications, it is usually easier to establish.
-  The reason is that in the case of @{text "Let"} we can make the freshness 
-  assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, wherby @{text c} can be arbitrarily 
-  chosen by the user as long as it has finite support.
-
-  With the help of @{text "\<bullet>bn"} functions defined in the previous section
-  we can show that binders can be substituted in term constructors. We show
-  this only for the specification from Figure~\ref{nominalcorehas}. The only
-  constructor with a complicated binding structure is @{text "ACons"}. For this
-  constructor we prove:
-  \begin{eqnarray}
-  \lefteqn{@{text "supp (Abs_lst (bv pat) trm) \<sharp>* \<pi> \<Longrightarrow>"}} \nonumber \\
-  & & @{text "ACons pat trm al = ACons (\<pi> \<bullet>bv pat) (\<pi> \<bullet> trm) al"} \nonumber
-  \end{eqnarray}
-
-  \noindent With the Property~\ref{avoiding} we can prove a strong induction principle
-  which we show again only for the interesting constructors in the Core Haskell
-  example. We first show the weak induction principle for comparison:
+  \noindent
+  The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it i)}; the 
+  second and third from the induction hypotheses in \eqref{hyps} (in the latter case
+  we have to use the fact that @{term "(r \<bullet> (q \<bullet> t)) = (r + q) \<bullet> t"}).
 
-\begin{equation}\nonumber
-\infer
-{
-  \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}
-}{
-  \begin{tabular}{cp{7cm}}
-%%  @{text "P1 KStar"}\\
-%%  @{text "\<forall>tk1 tk2. \<^raw:\big(>P1 tk1 \<and> P1 tk2\<^raw:\big)> \<Longrightarrow> P1 (KFun tk1 tk2)"}\\
-%%  @{text "\<dots>"}\\
-  @{text "\<forall>v ty t1 t2. \<^raw:\big(>P3 ty \<and> P7 t1 \<and> P7 t2\<^raw:\big)> \<Longrightarrow> P7 (Let v ty t1 t2)"}\\
-  @{text "\<forall>p t al. \<^raw:\big(>P9 p \<and> P7 t \<and> P8 al\<^raw:\big)> \<Longrightarrow> P8 (ACons p t al)"}\\
-  @{text "\<dots>"}
-  \end{tabular}
-}
-\end{equation}
-
-
-  \noindent In comparison, the cases for the same constructors in the derived strong
-  induction principle are:
-
-\begin{equation}\nonumber
-\infer
-{
-  \begin{tabular}{cp{7cm}}
-  \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}\\
-  \textrm{ avoiding any atoms in a given }@{text "y"}
-  \end{tabular}
-}{
-  \begin{tabular}{cp{7cm}}
-%%  @{text "\<forall>b. P1 b KStar"}\\
-%%  @{text "\<forall>tk1 tk2 b. \<^raw:\big(>\<forall>c. P1 c tk1 \<and> \<forall>c. P1 c tk2\<^raw:\big)> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\
-%%  @{text "\<dots>"}\\
-  @{text "\<forall>v ty t1 t2 b. \<^raw:\big(>\<forall>c. P3 c ty \<and> \<forall>c. P7 c t1 \<and> \<forall>c. P7 c t2 \<and>"}\\
-  @{text "\<^raw:\hfill>\<and> atom var \<sharp> b\<^raw:\big)> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\
-  @{text "\<forall>p t al b. \<^raw:\big(>\<forall>c. P9 c p \<and> \<forall>c. P7 c t \<and> \<forall>c. P8 c al \<and>"}\\
-  @{text "\<^raw:\hfill>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\
-  @{text "\<dots>"}
-  \end{tabular}
-}
-\end{equation}
-
+  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 strong induction principle derives from
+  the weak induction principle. At the moment we can derive the difficult cases of 
+  the strong induction principles only by hand, but they are very schematically 
+  so that with little effort we can even derive the strong induction principle for 
+  Core-Haskell given in Figure~\ref{nominalcorehas}. 
 *}