--- 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}.
*}