nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:d74e08799b63
+:4648bd6930e4
 \emph{one} binding clause of a term constructor.
 For binders we distinguish between \emph{shallow} and \emph{deep} binders.
 Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
 \isacommand{in}\; {\it labels'} (similar for the other two modes). The
-restriction we impose on shallow binders is that in case of
+restrictions we impose on shallow binders are that in case of
 \isacommand{bind\_set} and \isacommand{bind\_res} the {\it labels} must
 either refer to atom types or to sets of atom types; in case of
-\isacommand{bind} we allow labels to refer to atom types or lists of atom types. Two
+\isacommand{bind} we allow labels to refer to atom types or lists of atom types.
-examples for the use of shallow binders are the specification of
+Two examples for the use of shallow binders are the specification of
 lambda-terms, where a single name is bound, and type-schemes, where a finite
 set of names is bound:
 \begin{center}
 \begin{tabular}{@ {}cc@ {}}
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
-Note that for @{text lam} we have a choice which mode we use. The reason is that
+Note that for @{text lam} it does not matter which binding mode we use. The reason is that
-we bind only a single @{text name}. Having \isacommand{bind\_set} in the second
+we bind only a single @{text name}. However, having \isacommand{bind\_set}, or even
+\isacommand{bind}, in the second
 case changes the semantics of the specification.
 Note also that in these specifications @{text "name"} refers to an atom type, and
 @{text "fset"} to the type of finite sets.
-The restrictions are as follows:
+A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
-Shallow binders can occur in the binding part of several binding clauses.
-A \emph{deep} binder, on the other hand, uses an auxiliary binding function that ``picks'' out
 the atoms in one argument of the term-constructor, which can be bound in
 other arguments and also in the same argument (we will
 call such binders \emph{recursive}, see below).
 The corresponding binding functions are expected to return either a set of atoms
 (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms
 \noindent
 In this specification the function @{text "bn"} determines which atoms of @{text  p} are
 bound in the argument @{text "t"}. Note that in the second-last @{text bn}-clause the
 function @{text "atom"}
-coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows
+coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}.
+This allows
 us to treat binders of different atom type uniformly.
 The most drastic restriction we have to impose on deep binders is that
-we cannot have ``overlapping'' deep binders. Consider for example the
+we cannot have more than one binding function for one binder. Consider for example the
 term-constructors:
 \begin{center}
 \begin{tabular}{ll}
 @{text "Foo\<^isub>1 p::pat q::pat t::trm"} &
 induction principles derived by the datatype package in Isabelle/HOL for the types @{text
 "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\<AL>\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^isub>n\<^esub> y\<^isub>n "}
+@{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"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^isub>i\<^esub>"} stand for properties
+for all @{text "y\<^isub>i"} wherby 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>\<^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)"}
+@{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
 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)}
+{\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"} and {\it ii)}
-@{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.
+@{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
 \end{lemma}
 \begin{proof}
 By induction on @{text x}. The equations follow by simple unfolding
 of the definitions.
 \eqref{letpat} this means for a permutation @{text "r"}:
 %
 \begin{equation}\label{renaming}
 \begin{array}{l}
 \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\
-\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)"}}
+\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bnpat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
 \end{array}
 \end{equation}
 \noindent
 This fact will be crucial when establishing the strong induction principles.

changeset 2134	4648bd6930e4
parent 2128	abd46dfc0212
child 2139	dff8bd922812