nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:05843094273e
+:1cd509cba23f
 the following term-constructor
 \begin{center}
 \begin{tabular}{ll}
 @{text "Foo x::name y::name t::lam"} &
 \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
 \isacommand{bind} @{text y} \isacommand{in} @{text t}
 \end{tabular}
 \end{center}
 \noindent
 then we have to make sure the modes of the binders agree. We cannot
 coerces a name into the generic atom type of Nominal Isabelle. This allows
 us to treat binders of different atom type uniformly.
 As will shortly become clear, we cannot return an atom in a binding function
 that is also bound in the corresponding term-constructor. That means in the
-example above that the term-constructors PVar and PTup must not have a
+example above that the term-constructors @{text PVar} and @{text PTup} must not have a
 binding clause.  In the present version of Nominal Isabelle, we also adopted
 the restriction from the Ott-tool that binding functions can only return:
-the empty set or empty list (as in case PNil), a singleton set or singleton
+the empty set or empty list (as in case @{text PNil}), a singleton set or singleton
-list containing an atom (case PVar), or unions of atom sets or appended atom
+list containing an atom (case @{text PVar}), or unions of atom sets or appended atom
-lists (case PTup). This restriction will simplify proofs later on.
+lists (case @{text PTup}). This restriction will simplify proofs later on.
 The most drastic restriction we have to impose on deep binders is that
 we cannot have ``overlapping'' deep binders. Consider for example the
 term-constructors:
 binding clauses and the labels on 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 user. In our implementation we just use an affix @{text "_raw"}.
 For the purpose of the paper we just use superscripts to indicate a
 notion defined over alpha-equivalence classes and leave out the superscript
-for the corresponding notion on the ``raw'' level. So for example:
+for the corresponding notion on the ``raw'' level. So for example we have
 \begin{center}
-@{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
+@{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
 \end{center}
 \noindent
 The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
 non-empty and the types in the constructors only occur in positive
 %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 types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
+functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
-we need to define the free-variable functions
+we need to define free-variable functions
 \begin{center}
-@{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
+@{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set    \<dots>    fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
 \end{center}
 \noindent
 We define them together with the auxiliary free variable functions for
-binding functions. Given binding functions of types
+binding functions. Given binding functions for raw types
-@{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
+@{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"} we need to define
 \begin{center}
-@{text "fv_bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> atom set"}
+@{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
 \end{center}
 \noindent
 The basic idea behind these free-variable functions is to collect all atoms
 that are not bound in a term constructor, but because of the rather
 complicated binding mechanisms the details are somewhat involved.
-Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with
+Given a term-constructor @{text "C"} of type @{text ty} with argument types
-some  binding clauses, the function @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
+@{text "ty\<^isub>1 \<dots> ty\<^isub>n"} and some binding clauses, the function
-the union of the values defined below for each argument, say @{text "x\<^isub>i"} with type @{text "ty\<^isub>i"}.
+@{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
-From the binding clause of this term constructor, we can determine whether the
+defined below for each argument. From the binding clause of this term
-argument @{text "x\<^isub>i"} is a shallow or deep binder, and in the latter case also
+constructor, we can determine whether the argument is a shallow or deep
-whether it is a recursive or non-recursive of a binder. In these cases the value is:
+binder, and in the latter case also whether it is a recursive or
+non-recursive binder. In case the argument, say @{text "x\<^isub>i"} with
+type @{text "ty\<^isub>i"}, is a binder, the value is:
 \begin{center}
 \begin{tabular}{cp{7cm}}
 $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
-$\bullet$ & @{text "fv_bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+$\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
-non-recursive binder with the auxiliary function @{text "bn\<^isub>j"}\\
+non-recursive binder with the auxiliary function @{text "bn_ty\<^isub>i"}\\
-$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is
+$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is
-a deep recursive binder with the auxiliary function @{text "bn\<^isub>j"}
+a deep recursive binder with the auxiliary function @{text "bn_ty\<^isub>i"}
 \end{tabular}
 \end{center}
 \noindent
 In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of
-one or more abstractions. Let @{text "bnds"} be the bound atoms computed
+one or more abstractions. Let @{text "bnds"} be the set of bound atoms calculated
 as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{term "{}"}.
 Otherwise there are two cases: either the
 corresponding binders are all shallow or there is a single deep binder.
 In the former case we build the union of all shallow binders; in the
-later case we just take set or list of atoms the specified binding
+later case we just take the set of atoms specified binding
 function returns. With @{text "bnds"} computed as above the value of
 for @{text "x\<^isub>i"} is given by:
 \begin{center}
 \begin{tabular}{cp{7cm}}
 $\bullet$ & @{text "{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 "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
-$\bullet$ & @{text "(fv_ty\<^isub>m x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes
+$\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes
-we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\
+we are defining with the free variable function @{text "fv_ty\<^isub>i"}\\
 %  $\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
 \end{tabular}
 \end{center}
-\noindent Next, for each binding function @{text "bn"} we define a
+\noindent
-free variable function @{text "fv_bn"}. The basic idea behind this
+Next, for each binding function @{text "bn_ty"} we define a
-function is to compute all the free atoms under this binding
+free variable function @{text "fv_bn_ty"}. The basic idea behind this
+function is to compute all the free atoms that are not bound by the binding
 function. So given that @{text "bn"} is a binding function for type
 @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the
 omission of the arguments present in @{text "bn"}.
 For a binding function clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"},

changeset 1723	1cd509cba23f
parent 1722	05843094273e
child 1724	8c788ad71752