nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:26e44bcddb5b
+:3e71af53cedb
 \noindent
 The scope of the binding is indicated by labels given to the types, for
 example @{text "s::trm"}, and a binding clause, in this case
 \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
-clause states to bind in @{text s} all the names the function call @{text
+clause states to bind in @{text s} all the names the function @{text
 "bn(as)"} returns.  This style of specifying terms and bindings is heavily
 inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 However, we will not be able to cope with all specifications that are
 allowed by Ott. One reason is that Ott lets the user to specify ``empty''
 @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
 \end{equation}
 \noindent
 From property \eqref{equivariancedef} and the definition of @{text supp}, we
-can be easily deduce that equivariant functions have empty support.
+can be easily deduce that equivariant functions have empty support. There is
+also a similar notion for equivariant relations, say @{text R}, namely the property
+that
+%
+\begin{center}
+@{text "x R y"} \;\;implies\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+\end{center}
 Finally, the nominal logic work provides us with convenient means to rename
 binders. While in the older version of Nominal Isabelle, we used extensively
 Property~\ref{swapfreshfresh} for renaming single binders, this property
 proved unwieldy for dealing with multiple binders. For such binders the
 (possibly empty) list of \emph{binding clauses}, which indicate the binders
 and their scope in a term-constructor.  They come in three \emph{modes}:
 \begin{center}
 \begin{tabular}{l}
-\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+\isacommand{bind}\; {\it binder}\; \isacommand{in}\; {\it label}\\
-\isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+\isacommand{bind\_set}\; {\it binder}\; \isacommand{in}\; {\it label}\\
-\isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+\isacommand{bind\_res}\; {\it binder}\; \isacommand{in}\; {\it label}\\
 \end{tabular}
 \end{center}
 \noindent
 The first mode is for binding lists of atoms (the order of binders matters);
 extract datatype definitions from the specification and then define
 expicitly an alpha-equivalence relation over them.
 The datatype definition can be obtained by stripping off the
-binding clauses and the labels on the types. We also have to invent
+binding clauses and the labels from the types. We also have to invent
 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
 given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
-But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate
+But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate
 that a notion is defined over alpha-equivalence classes and leave it out
 for the corresponding notion defined on the ``raw'' level. So for example
 we have
 \begin{center}
 %
 \begin{equation}\label{ceqvt}
 @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
 \end{equation}
-% TODO: we did not define permutation types
-%\noindent
-%From this definition we can easily show that the raw datatypes are
-%all permutation types (Def ??) by a simple structural induction over
-%the @{text "ty"}s.
 The first non-trivial step we have to perform is the generation free-variable
 functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
 we need to define free-variable functions
 \begin{center}
 \end{center}
 \noindent
 We define them together with auxiliary free-variable functions for
 the binding functions. Given binding functions
-@{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we need to define
+@{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define
 %
 \begin{center}
 @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
 \end{center}
 \noindent
 The reason for this setup is that in a deep binder not all atoms have to be
-bound, as we shall see in an example below. We need therefore a function
+bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
 that calculates those unbound atoms.
 While the idea behind these
 free-variable functions is clear (they just collect all atoms that are not bound),
 because of our rather complicated binding mechanisms their definitions are
 somewhat involved.
 Given a term-constructor @{text "C"} of type @{text ty} with argument types
 \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
-@{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
+@{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values, @{text v},
 calculated below for each argument.
 First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses,
 we can determine whether the argument is a shallow or deep
 binder, and in the latter case also whether it is a recursive or
 non-recursive binder.
 %
 \begin{equation}\label{deepbinder}
 \mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-$\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
+$\bullet$ & @{term "v = {}"} provided @{text "x\<^isub>i"} is a shallow binder\\
-$\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+$\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
 non-recursive binder with the auxiliary binding function @{text "bn"}\\
-$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
+$\bullet$ & @{text "v = fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
 a deep recursive binder with the auxiliary binding function @{text "bn"}
 \end{tabular}}
 \end{equation}
 \noindent
 corresponding binding function. The value for @{text "x\<^isub>i"} is then given by:
 %
 \begin{equation}\label{deepbody}
 \mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-$\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
+$\bullet$ & @{text "v = {atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
-$\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
+$\bullet$ & @{text "v = (atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
-$\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
+$\bullet$ & @{text "v = (atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
-$\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
+$\bullet$ & @{text "v = (fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
 corresponding to the types specified by the user\\
 %  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
 %     with a free-variable function @{text "fv\<^isup>\<alpha>"}\\
-$\bullet$ & @{term "{}"} otherwise
+$\bullet$ & @{term "v = {}"} otherwise
 \end{tabular}}
 \end{equation}
 \noindent
 Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces
 appear in @{text "rhs"} we generate the premise according to the
 rules for @{text "fv_ty"} described above in (\ref{deepbinder}--\ref{deepbody}). Otherwise:
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-$\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
+$\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
 recursive call @{text "bn x\<^isub>i"}\medskip\\
-$\bullet$ & @{term "{}"} provided @{text "rhs"} contains
+$\bullet$ & @{term "v = {}"} provided @{text "rhs"} contains
 @{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type.
 \end{tabular}
 \end{center}
 \noindent
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
 \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
-{@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}\medskip\\
+{@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
 \end{tabular}
 \end{center}
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
 \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
-{@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\medskip\\
+{@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
 \end{tabular}
 \end{center}
 \noindent
 Note the difference between  $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of
 the components in an assignment that are \emph{not} bound. Therefore we have
 a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is
-a non-recursive binder). The reason is that the terms inside an assignment are not meant
+a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant
 to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
 because there everything from the assignment is under the binder.
 *}
 section {* Establishing the Reasoning Infrastructure *}
 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\<AL>\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
+"ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
 induction principles that establish
 \begin{center}
-@{text "P\<^bsub>ty\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<^isub>n\<^esub> y\<^isub>n "}
+@{text "P\<^bsub>ty\<AL>\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^isub>n\<^esub> y\<^isub>n "}
 \end{center}
 \noindent
-for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<^isub>i\<^esub>"} stand for properties
+for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^isub>i\<^esub>"} 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\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
+@{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<AL>\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<AL>\<^isub>j\<^esub> 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
 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
 \end{center}
 \noindent
 are alpha-equivalent. This gives us conditions when the corresponding
-alpha-equated terms are equal, namely
+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"}
 \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.
-Working bow completely on the alpha-equated level, we can first show that
+By working now 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}
 \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.
-The reason is we cannot make any assumption about the binders in @{text "C\<^sup>\<alpha>"}
+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).
 In \cite{UrbanTasson05} we introduced a method for automatically
 strengthening weak induction principles for terms containing single
 binders. These stronger induction principles allow the user to make additional
-assumptions about binders when proving the induction hypotheses.
+assumptions about binders.
 These additional assumptions amount to a formal
 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
+the general binders presented here. We will indeed be able to so, but for this we need an
 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.
 Assuming a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
 $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
 \end{tabular}
 \end{center}
 \noindent
-Using the quotient package again we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
+Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
 alpha-equated terms. We can then prove the following two facts
 \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}
 \begin{proof}
-By induction on @{text x}. The equation follow by simple unfolding
+By induction on @{text x}. The equations follow by simple unfolding
 of the definitions.
 \end{proof}
 \noindent
 The first property states that a permutation applied to a binding function is
 to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the
 @{text "Let"} term-constructor from the example shown
 \eqref{letpat} this means for a permutation @{text "r"}:
 %
 \begin{equation}\label{renaming}
-\mbox{if @{term "supp (Abs_lst (bn p) t)  \<sharp>* r"}
+\begin{array}{l}
-then @{text "Let p t = Let (r \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) (r \<bullet> t)"}}
+\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\
-\end{equation}
+\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
+\end{array}
-\noindent
+\end{equation}
-This fact will be used when establishing the strong induction principles.
+\noindent
+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. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t)"}
+@{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}
 \noindent
 it is sufficient to establish the following implication
 %
 \begin{equation}\label{strong}
 \mbox{\begin{tabular}{l}
-@{text "\<forall>p t c."}\\
+@{text "\<forall>p t\<^isub>1 t\<^isub>2 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{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
-\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}
+\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)"}
 \end{tabular}}
 \end{equation}
 \noindent
 While this implication contains an additional argument, namely @{text c}, and
 @{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)"}
+For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}
-assuming \eqref{hyps} as induction hypotheses. By Property~\ref{avoiding} we
+assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}).
+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"}
+@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
 \end{equation}
 \noindent
 hold. The latter fact and \eqref{renaming} give us
 \begin{center}
-@{text "Let (q \<bullet> p) (q \<bullet> t) = Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (r \<bullet> (q \<bullet> t))"}
+\begin{tabular}{l}
-\end{center}
+@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
+\hspace{15mm}@{text "Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
-\noindent
+\end{tabular}
-So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t)"}, we are can equally
+\end{center}
+\noindent
+So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, 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)))"}
+@{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
 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:
+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"}\\
 {\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))"}\\
+{\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
+{\it iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
 \end{tabular}
 \end{center}
 \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
+others from the induction hypotheses in \eqref{hyps} (in the fourth case
-we have to use the fact that @{term "(r \<bullet> (q \<bullet> t)) = (r + q) \<bullet> t"}).
+we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
 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
+so that with little effort we can even derive them for
 Core-Haskell given in Figure~\ref{nominalcorehas}.
 *}
 section {* Related Work *}
 de-Bruijn representation), but to different bound variables. A similar idea
 has been recently explored for general binders in the locally nameless
 approach to binding \cite{chargueraud09}.  There, de-Bruijn indices consist
 of two numbers, one referring to the place where a variable is bound and the
 other to which variable is bound. The reasoning infrastructure for both
-representations of bindings comes for free in the theorem provers Isabelle/HOL and
+representations of bindings comes for free in the theorem provers, like Isabelle/HOL or
-Coq, for example, as the corresponding term-calculi can be implemented as ``normal''
+Coq, as the corresponding term-calculi can be implemented as ``normal''
 datatypes.  However, in both approaches it seems difficult to achieve our
 fine-grained control over the ``semantics'' of bindings (i.e.~whether the
 order of binders should matter, or vacuous binders should be taken into
 account). To do so, one would require additional predicates that filter out
 unwanted terms. Our guess is that such predicates results in rather
 meaning in a HOL-based theorem prover.
 Because of how we set up our definitions, we had to impose restrictions,
 like excluding overlapping deep binders, that are not present in Ott. Our
 expectation is that we can still cover many interesting term-calculi from
-programming language research, for example Core-Haskell. For prviding support
+programming language research, for example Core-Haskell. For providing support
 of neat features in Ott, such as subgrammars, the existing datatype
 infrastructure in Isabelle/HOL is unfortunately not powerful enough. On the
 other hand, we are not aware that Ott can make the distinction between our
 three different binding modes. Also, definitions for notions like the free
 variables of a term are work in progress in Ott.
 other. We have not yet been able to find a way to avoid such interferences.
 On the other hand, such bindings can be made sense of informally \cite{SewellBestiary}.
 This suggest there should be an approriate notion of alpha-equivalence.
 Another interesting line of investigation is whether we can go beyond the
-simple-minded form of binding function we adopted from Ott. At the moment, binding
+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
 binding functions.

changeset 1771	3e71af53cedb
parent 1770	26e44bcddb5b
child 1775	86122d793f32