--- a/Nominal/NewParser.thy Thu Jul 15 09:40:05 2010 +0100
+++ b/Nominal/NewParser.thy Fri Jul 16 02:38:19 2010 +0100
@@ -359,7 +359,8 @@
val (alpha_distincts, alpha_bn_distincts) =
mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info
- (* definition of raw_alpha_eq_iff lemmas *)
+ (* definition of alpha_eq_iff lemmas *)
+ (* they have a funny shape for the simplifier *)
val _ = warning "Eq-iff theorems";
val alpha_eq_iff =
if get_STEPS lthy > 5
@@ -470,10 +471,18 @@
(* respectfulness proofs *)
(* HERE *)
+
+ val (_, lthy8') = lthy8
+ |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts)
+ ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff)
+ ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs)
+ ||>> Local_Theory.note ((@{binding "perm_defs"}, []), raw_perm_defs)
+ ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps)
+
val _ =
if get_STEPS lthy > 16
- then true else raise TEST lthy8
+ then true else raise TEST lthy8'
(* old stuff *)
--- a/Paper/Paper.thy Thu Jul 15 09:40:05 2010 +0100
+++ b/Paper/Paper.thy Fri Jul 16 02:38:19 2010 +0100
@@ -308,7 +308,7 @@
\noindent
We take as the starting point a definition of raw terms (defined as a
- datatype in Isabelle/HOL); identify then the $\alpha$-equivalence classes in
+ datatype in Isabelle/HOL); then identify the $\alpha$-equivalence classes in
the type of sets of raw terms according to our $\alpha$-equivalence relation,
and finally define the new type as these $\alpha$-equivalence classes
(non-emptiness is satisfied whenever the raw terms are definable as datatype
@@ -1599,16 +1599,19 @@
text {*
Having made all necessary definitions for raw terms, we can start
- introducing the reasoning infrastructure for the $\alpha$-equated types the
- user originally specified. We sketch in this section the facts we need for establishing
- this reasoning infrastructure. First we have to show that the
+ with establishing the reasoning infrastructure for the $\alpha$-equated types
+ @{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch
+ in this section the proofs we need for establishing this infrastructure. One
+ main point of our work is that we have completely automated these proofs in Isabelle/HOL.
+
+ First we establish that the
$\alpha$-equivalence relations defined in the previous section are
equivalence relations.
\begin{lemma}\label{equiv}
- Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
- @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and
- @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant.
+ Given the raw types @{text "ty"}$_{1..n}$ and binding functions
+ @{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and
+ @{text "\<approx>bn"}$_{1..m}$ are equivalence relations and equivariant.
\end{lemma}
\begin{proof}
@@ -1622,191 +1625,182 @@
We can feed this lemma into our quotient package and obtain new types @{text
"ty"}$^\alpha_{1..n}$ representing $\alpha$-equated terms of types @{text "ty"}$_{1..n}$.
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-atom functions @{text
- "fa_ty"}$^\alpha_{1..n}$ and the binding functions @{text
- "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the
+ "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
+ "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
+ "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text
+ "bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the
user, since they are given in terms of the isomorphisms we obtained by
creating new types in Isabelle/HOL (recall the picture shown in the
Introduction).
- The first useful property to the user is the fact that term-constructors are
- distinct, that is
+ The first useful property for the user is the fact that distinct
+ term-constructors are not
+ equal, that is
%
\begin{equation}\label{distinctalpha}
- \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"}
- @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.}
+ \mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \<dots> x\<^isub>r"}~@{text "\<noteq>"}~%
+ @{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}}
\end{equation}
\noindent
- By definition of $\alpha$-equivalence we can show that
- for the raw term-constructors
+ whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.
+ In order to derive this fact, we use the definition of $\alpha$-equivalence
+ and establish that
%
\begin{equation}\label{distinctraw}
- \mbox{@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;$\not\approx$@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.}
+ \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}
\end{equation}
\noindent
- In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient
- package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"}
+ holds for the corresponding raw term-constructors.
+ In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
+ package needs to know that the raw term-constructors @{text "C"} and @{text "D"}
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 "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that
+ Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types
+ @{text "ty"}$_{1..r}$, respectfulness amounts to showing that
%
\begin{center}
- @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}
+ @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
\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 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
- %
- \begin{center}
- @{text "x \<approx>ty\<^isub>i y"} implies @{text "x \<approx>bn\<^isub>i y"}
- \end{center}
-
- \noindent
- This can be established by induction on the definition of @{text "\<approx>ty\<^isub>i"}.
-
- 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 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"}$_{1..n}$ fall into this category. So we can also add to our infrastructure
- induction principles that establish
-
- \begin{center}
- @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>1 y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^esub>\<^isub>n y\<^isub>n "}
- \end{center}
-
- \noindent
- for all @{text "y\<^isub>i"} whereby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties
- defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of
- these induction principles look
- as follows
-
- \begin{center}
- @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<AL>\<^esub>\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<AL>\<^esub>\<^isub>j x\<^isub>j \<Rightarrow> P\<^bsub>ty\<AL>\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
- \end{center}
-
- \noindent
- where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}.
- Next we lift the permutation operations defined in \eqref{ceqvt} for
- the raw term-constructors @{text "C"}. These facts contain, in addition
- to the term-constructors, also permutation operations. In order to make the
- lifting go through,
- 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 establish the equations
-
- \begin{equation}\label{calphaeqvt}
- @{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
- for our infrastructure. In a similar fashion we can lift the equations
- characterising the free-atom functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fa_bn\<AL>\<^isub>k"}, and the
- binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for these
- lifting are the properties:
+ holds under the assumptions that we have \mbox{@{text
+ "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
+ and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
+ @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this
+ implication by applying the corresponding rule in our $\alpha$-equivalence
+ definition and by establishing the following auxiliary facts
%
\begin{equation}\label{fnresp}
\mbox{%
\begin{tabular}{l}
- @{text "x \<approx>ty\<^isub>j y"} implies @{text "fa_ty\<^isub>j x = fa_ty\<^isub>j y"}\\
- @{text "x \<approx>ty\<^isub>k y"} implies @{text "fa_bn\<^isub>k x = fa_bn\<^isub>k y"}\\
- @{text "x \<approx>ty\<^isub>k y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"}
+ @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~implies~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"}\\
+ @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"}\\
+ @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
+ @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
\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 we defined the free-atom
- 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
- atom. Then the third property is just not true. However, our
- restrictions imposed on the binding functions
- exclude this possibility.
+ They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first,
+ second and last implication are true by how we stated our definitions, the
+ third \emph{only} holds because of our restriction
+ imposed on the form of the binding functions---namely \emph{not} returning
+ any bound atoms. In Ott, in contrast, the user may
+ define @{text "bn"}$_{1..m}$ so that they return bound
+ atoms and in this case the third implication is \emph{not} true. A
+ result is that the lifing of the corresponding binding functions to $\alpha$-equated
+ terms is impossible.
- Having the facts \eqref{fnresp} at our disposal, we can lift the
- definitions that characterise when two terms of the form
-
+ Having established respectfulness for the raw term-constructors, the
+ quotient package is able to automatically deduce \eqref{distinctalpha} from
+ \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can
+ also lift properties that characterise when two raw terms of the form
+ %
\begin{center}
- @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
+ @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
\end{center}
\noindent
are $\alpha$-equivalent. This gives us conditions when the corresponding
$\alpha$-equated terms are \emph{equal}, namely
-
+ %
\begin{center}
- @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}
+ @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
\end{center}
\noindent
- We call these conditions as \emph{quasi-injectivity}. Except for one function, which
- we have to lift in the next section, we completed
- the lifting part of establishing the reasoning infrastructure.
+ We call these conditions as \emph{quasi-injectivity}. They correspond to
+ the premises in our $\alpha$-equivalence relations.
+
+ Next we can lift the permutation
+ operations defined in \eqref{ceqvt}. In order to make this
+ lifting to go through, we have to show that the permutation operations are respectful.
+ 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
+ %
+ \begin{equation}\label{calphaeqvt}
+ @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}
+ \end{equation}
+
+ \noindent
+ to our infrastructure. In a similar fashion we can lift the defining equations
+ of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and
+ @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
+ "bn\<AL>"}$_{1..m}$ and of the size functions @{text "size_ty\<AL>"}$_{1..n}$.
+ The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
+ by the datatype package of Isabelle/HOL.
- By working now completely on the $\alpha$-equated level, we can first show that
- the free-atom functions and binding functions
- are equivariant, namely
+ Finally we can add to our infrastructure a structural induction principle
+ for the types @{text "ty\<AL>"}$_{i..n}$ whose
+ conclusion of the form
+ %
+ \begin{equation}\label{weakinduct}
+ \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
+ \end{equation}
+ \noindent
+ whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$
+ have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each
+ term constructor @{text "C"}$^\alpha$ a premise of the form
+ %
+ \begin{equation}\label{weakprem}
+ \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}}
+ \end{equation}
+
+ \noindent
+ in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are
+ the recursive arguments of @{text "C\<AL>"}.
+
+ By working now completely on the $\alpha$-equated level, we
+ can first show that the free-atom functions and binding functions are
+ equivariant, namely
+ %
\begin{center}
\begin{tabular}{rcl}
- @{text "p \<bullet> (fa_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fa_ty\<^sup>\<alpha> (p \<bullet> x)"}\\
- @{text "p \<bullet> (fa_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fa_bn\<^sup>\<alpha> (p \<bullet> x)"}\\
- @{text "p \<bullet> (bn\<^sup>\<alpha> x)"} & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"}
+ @{text "p \<bullet> (fa_ty\<AL>\<^isub>i x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"}\\
+ @{text "p \<bullet> (fa_bn\<AL>\<^isub>j x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\
+ @{text "p \<bullet> (bn\<AL>\<^isub>j x)"} & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}
\end{tabular}
\end{center}
\noindent
- 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 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
+ These properties can be established using the induction principle
+ in \eqref{weakinduct}.
+ Having these equivariant properties established, 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>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
\end{center}
\noindent
holds. This together with Property~\ref{supportsprop} allows us to show
-
- \begin{center}
- @{text "finite (supp x\<^isub>i)"}
- \end{center}
-
- \noindent
- by a structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types
- @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in
- @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fa_ty\<AL>\<^bsub>1..n\<^esub>"}.
+ for every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported,
+ namely @{text "finite (supp x)"}. This can be again shown by induction
+ over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of
+ elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
+ This important fact provides evidence that our notions of free-atoms and
+ $\alpha$-equivalence are correct.
\begin{lemma}
- For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that
- @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"} holds.
+ For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have
+ @{text "supp x = fa_ty\<AL>\<^isub>i x"}.
\end{lemma}
\begin{proof}
- The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case
+ The proof is by induction. In each case
we unfold the definition of @{text "supp"}, move the swapping inside the
- term-constructors and the use then quasi-injectivity lemmas in order to complete the
+ term-constructors and then use the 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, we can established automatically a reasoning infrastructure
- for the types @{text "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}
+ for the types @{text "ty\<AL>"}$_{1..n}$
by first lifting definitions from the raw level to the quotient level and
- then establish facts about these lifted definitions. All necessary proofs
+ then by establishing facts about these lifted definitions. All necessary proofs
are generated automatically by custom ML-code. This code can deal with
specifications like the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
@@ -1814,9 +1808,7 @@
\begin{boxedminipage}{\linewidth}
\small
\begin{tabular}{l}
- \isacommand{atom\_decl}~@{text "var"}\\
- \isacommand{atom\_decl}~@{text "cvar"}\\
- \isacommand{atom\_decl}~@{text "tvar"}\\[1mm]
+ \isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
\isacommand{nominal\_datatype}~@{text "tkind ="}\\
\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
\isacommand{and}~@{text "ckind ="}\\
@@ -1888,16 +1880,9 @@
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-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}
- @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
- \end{equation}
-
- \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 it.
+ We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
+ the induction hypothesis requires us to establish the implications \eqref{weakprem}.
+ The problem with these implications is that in general they are not easy to establish.
The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}
(for example we cannot assume the variable convention for them).
@@ -1914,13 +1899,7 @@
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 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}
-
- \noindent
- with @{text "y\<^isub>i"} determined as follows:
+ we define @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"} with @{text "y\<^isub>i"} determined as follows:
%
\begin{center}
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
@@ -1967,7 +1946,7 @@
This fact will be crucial when establishing the strong induction principles.
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)"}
\end{center}
@@ -2013,7 +1992,7 @@
\noindent
hold. The latter fact and \eqref{renaming} give us
-
+ %
\begin{center}
\begin{tabular}{l}
@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
@@ -2023,17 +2002,11 @@
\noindent
So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
- establish
-
- \begin{center}
- @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}
- \end{center}
-
- \noindent
+ establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
To do so, we will use the implication \eqref{strong} of the strong induction
principle, which requires us to discharge
the following four proof obligations:
-
+ %
\begin{center}
\begin{tabular}{rl}
{\it i)} & @{text "set (bn (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
@@ -2063,8 +2036,8 @@
text {*
To our knowledge the earliest usage of general binders in a theorem prover
is described in \cite{NaraschewskiNipkow99} about a formalisation of the
- algorithm W. This formalisation implements binding in type schemes using a
- de-Bruijn indices representation. Since type schemes in W contain only a single
+ algorithm W. This formalisation implements binding in type-schemes using a
+ de-Bruijn indices representation. Since type-schemes in W contain only a single
place where variables are bound, different indices do not refer to different binders (as in the usual
de-Bruijn representation), but to different bound variables. A similar idea
has been recently explored for general binders in the locally nameless
@@ -2192,19 +2165,6 @@
section {* Conclusion *}
text {*
-We can also see that
- %
- \begin{equation}\label{bnprop}
- @{text "fa_ty x = bn x \<union> fa_bn x"}.
- \end{equation}
-
- \noindent
- holds for any @{text "bn"}-function defined for the type @{text "ty"}.
-
-*}
-
-
-text {*
We have presented an extension of Nominal Isabelle for deriving
automatically a convenient reasoning infrastructure that can deal with
general binders, that is term-constructors binding multiple variables at
@@ -2213,10 +2173,10 @@
earlier work that derives strong induction principles which have the usual
variable convention already built in. For the moment we can do so only with manual help,
but future work will automate them completely. The code underlying the presented
- extension will become part of the Isabelle distribution, but for the moment
+ extension will become part of the Isabelle distribution.\footnote{For the moment
it can be downloaded from the Mercurial repository linked at
\href{http://isabelle.in.tum.de/nominal/download}
- {http://isabelle.in.tum.de/nominal/download}.
+ {http://isabelle.in.tum.de/nominal/download}.}
We have left out a discussion about how functions can be defined over
$\alpha$-equated terms that involve general binders. In earlier versions of Nominal
@@ -2237,31 +2197,31 @@
simple-minded form for binding functions that we adopted from Ott. At the moment, binding
functions can only return the empty set, a singleton atom set or unions
of atom sets (similarly for lists). It remains to be seen whether
- properties like \eqref{bnprop} provide us with means to support more interesting
+ properties like
+ %
+ \begin{center}
+ @{text "fa_ty x = bn x \<union> fa_bn x"}.
+ \end{center}
+
+ \noindent
+ provide us with means to support more interesting
binding functions.
We have also not yet played with other binding modes. For example we can
- imagine that there is need for a binding mode \isacommand{bind\_\#list} with
- an associated abstraction of the form
- %
- \begin{center}
- @{term "Abs_dist as x"}
- \end{center}
-
- \noindent
+ imagine that there is need for a binding mode
where instead of lists, we abstract lists of distinct elements.
Once we feel confident about such binding modes, our implementation
can be easily extended to accommodate them.
- \medskip
- \noindent
- {\bf Acknowledgements:} We are very grateful to Andrew Pitts for
- many discussions about Nominal Isabelle. We also thank Peter Sewell for
- making the informal notes \cite{SewellBestiary} available to us and
- also for patiently explaining some of the finer points of the work on the Ott-tool.
- Stephanie Weirich suggested to separate the subgrammars
- of kinds and types in our Core-Haskell example.
+ %\medskip
+ %\noindent
+ %{\bf Acknowledgements:} We are very grateful to Andrew Pitts for
+ %many discussions about Nominal Isabelle. We also thank Peter Sewell for
+ %making the informal notes \cite{SewellBestiary} available to us and
+ %also for patiently explaining some of the finer points of the work on the Ott-tool.
+ %Stephanie Weirich suggested to separate the subgrammars
+ %of kinds and types in our Core-Haskell example.
*}