nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:26c4653d76d1
+:ec0afa89aab3
 section {* Introduction *}
 text {*
-@{text "(1, (2, 3))"}
+%%%  @{text "(1, (2, 3))"}
 So far, Nominal Isabelle provides a mechanism for constructing
 alpha-equated terms, for example
 \begin{center}
 whether the @{text "x\<^isub>i"} is the body of one or more binding clauses.
 In this case we first calculate the set @{text "bnds"} as follows:
 either the corresponding binders are all shallow or there is a single deep binder.
 In the former case we take @{text bnds} to be the union of all shallow
 binders; in the latter case, we just take the set of atoms specified by the
-corrsponding binding function. The value for @{text "x\<^isub>i"} is then given by:
+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\\
 "Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in
 @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
 "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
 free in @{text "as"}. This is what the purpose of the function @{text
 "fv\<^bsub>bn\<^esub>"} is.  In contrast, in @{text "Let_rec"} we have a
-recursive binder where we want to also bind all occurences of the atoms
+recursive binder where we want to also bind all occurrences of the atoms
 @{text "bn as"} inside @{text "as"}. Therefore we have to subtract @{text
 "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from
 @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
 that an assignment ``alone'' does not have any bound variables. Only in the
 context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.
 then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
 {\bf TODO (I do not understand the definition below yet).}
 The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
-for their respective types, the difference is that they ommit checking the arguments that
+for their respective types, the difference is that they omit checking the arguments that
 are bound. We assumed that there are no bindings in the type on which the binding function
 is defined so, there are no permutations involved. For a binding function clause
 @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:
 \begin{center}
 "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
 "C"}$_{1..m}$. Similarly for the free-variable functions @{text
 "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
 "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the
 user, since the are formulated in terms of the isomorphism we obtained by
-cerating a new type in Isabelle/HOL (remember the picture shown in the
+creating a new type in Isabelle/HOL (remember the picture shown in the
 Introduction).
 {\bf TODO below.}
 then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
 \end{proof}
 % Very vague...
 \begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"}
 of this type:
-\begin{center}
+\begin{equation}
 @{term "supp x = fv_ty\<^isup>\<alpha>\<^isub>i x"}.
-\end{center}
+\end{equation}
 \end{lemma}
 \begin{proof}
 We will show this by induction together with equations that characterize
 @{term "fv_bn\<^isup>\<alpha>\<^isub>"} in terms of @{term "alpha_bn\<^isup>\<alpha>"}. For each of @{text "fv_bn\<^isup>\<alpha>"}
-functions this equaton is:
+functions this equation is:
 \begin{center}
 @{term "{a. infinite {b. \<not> alpha_bn\<^isup>\<alpha> ((a \<rightleftharpoons> b) \<bullet> x) x}} = fv_bn\<^isup>\<alpha> x"}
 \end{center}
 In the induction we need to show these equations together with the goal
 $\bullet$ & @{text "\<pi> \<bullet>bn\<^isub>k x\<^isub>i"} provided @{text "bn\<^isub>k x\<^isub>i"} is @{text "rhs"}\\
 \end{tabular}
 \end{center}
 The definition of @{text "\<bullet>bn"} is respectful (simple induction) so we can lift it
-and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this defnition is correct is:
+and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this definition is correct is:
 %% We could get this from ExLet/perm_bn lemma.
 \begin{lemma} For every bn function  @{text "bn\<^isup>\<alpha>\<^isub>i"},
-\begin{center}
+\begin{eqnarray}
-@{text "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i l = bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i l)"}
+@{term "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i x"} & = & @{term "bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}\\
-\end{center}
+@{term "fv_bn\<^isup>\<alpha>\<^isub>i x"} & = & @{term "fv_bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}
+\end{eqnarray}
 \end{lemma}
 \begin{proof} By induction on the lifted type it follows from the definitions of
-permutations on the lifted type and the lifted defining eqautions of @{text "\<bullet>bn"}.
+permutations on the lifted type and the lifted defining equations of @{text "\<bullet>bn"}
+and @{text "fv_bn"}.
 \end{proof}
 *}
 text {*
 \item non-emptiness
 \item positive datatype definitions
 \item finitely supported abstractions
 \item respectfulness of the bn-functions\bigskip
 \item binders can only have a ``single scope''
+\item in particular "bind a in b, bind b in c" is not allowed.
 \item all bindings must have the same mode
 \end{itemize}
 *}
 (*<*)

changeset 1746	ec0afa89aab3
parent 1743	925a5e9aa832
child 1747	4abb95a7264b