nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:09b476c20fe1
+:eaf5209669de
 \begin{center}
 @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}
 \end{center}
 \noindent
-with none of the @{text "l"}$_{1..r}$ being among the bodies @{text
+with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the
+@{text "l"}$_{1..r}$ being among the bodies @{text
 "d"}$_{1..q}$. The set @{text "B'"} is defined as
 %
 \begin{center}
 @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
 \end{center}
 \noindent
 This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$.
 Note that for non-recursive deep binders, we have to add in \eqref{fadef}
 the set of atoms that are left unbound by the binding functions @{text
-"bn"}$_{1..m}$. We use for the definition of
+"bn"}$_{1..m}$. We used for the definition of
 this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual
 recursion. Assume the user specified a @{text bn}-clause of the form
 %
 \begin{center}
 @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
 @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
 \end{tabular}
 \end{center}
 \noindent
-For these definitions, recall that @{text ANil} and @{text "ACons"} have no
+Recall that @{text ANil} and @{text "ACons"} have no
 binding clause in the specification. The corresponding free-atom
 function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
 occurring in an assignment (in case of @{text "ACons"}, they are given by
 calls to @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}).
 The binding only takes place in @{text Let} and
 in contrast with @{text "Let_rec"} where we have a recursive
 binder to bind all occurrences of the atoms in @{text
 "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
 @{text "set (bn as)"} from both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}.
 Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the
-list of assignments, but instead returns the free atoms, that means in this
+list of assignments, but instead returns the free atoms, which means in this
 example the free atoms in the argument @{text "t"}.
 An interesting point in this
 example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any
 atoms, even if the binding function is specified over assignments.
 \noindent
 In this case we define a premise @{text P} using the relation
 $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
 $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other
 binding modes). This premise defines $\alpha$-equivalence of two abstractions
-involving multiple binders. We first define as above the tuples @{text "D"} and
+involving multiple binders. As above, we first build the tuples @{text "D"} and
 @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
 compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}).
 For $\approx_{\,\textit{set}}$ we also need
 a compound free-atom function for the bodies defined as
 %
 \noindent
 Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This
 lets us formally define the premise @{text P} for a non-empty binding clause as:
 %
-\begin{equation}\label{pprem}
+\begin{center}
 \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
-\end{equation}
+\end{center}
 \noindent
 This premise accounts for $\alpha$-equivalence of the bodies of the binding
-clause. However, in case the binders have non-recursive deep binders, then
+clause. Similarly for the other binding modes.
+However, in case the binders have non-recursive deep binders, this premise
+is not enough:
 we also have to ``propagate'' $\alpha$-equivalence inside the structure of
 these binders. An example is @{text "Let"} where we have to make sure the
 right-hand sides of assignments are $\alpha$-equivalent. For this we use the
 relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).
 Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
 \begin{center}
 @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
 \end{center}
 \noindent
-The premises for @{text "bc\<^isub>i"} are then defined as
+All premises for @{text "bc\<^isub>i"} are then given by
 %
 \begin{center}
 @{text "prems(bc\<^isub>i) \<equiv> P  \<and>  l\<^isub>1 \<approx>bn\<^isub>1 l\<PRIME>\<^isub>1  \<and> ... \<and>  l\<^isub>r \<approx>bn\<^isub>r l\<PRIME>\<^isub>r"}
 \end{center}
 \noindent
-where @{text "P"} is defined in \eqref{pprem}.
+where the auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$
+are defined as follows: assuming a @{text bn}-clause is of the form
-The $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$ are defined as follows:
-given a @{text bn}-clause of the form
 %
 \begin{center}
 @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
 \end{center}
 \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
 {@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}
 \end{center}
 \noindent
-whereby the relations @{text "R"}$_{1..s}$ are given by
+In this clause the relations @{text "R"}$_{1..s}$ are given by
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 $\bullet$ & @{text "z\<^isub>i \<approx>ty z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and
 is a recursive argument of @{text C},\\
 \noindent
 This completes the definition of $\alpha$-equivalence. As a sanity check, we can show
 that the premises of empty binding clauses are a special case of the clauses for
 non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
-as the permutation).
+for the existentially quantified permutation).
 *}
-(*<*)consts alpha_ty ::'a
+(*<*)
+consts alpha_ty ::'a
 consts alpha_trm ::'a
 consts fa_trm :: 'a
 consts alpha_trm2 ::'a
 consts fa_trm2 :: 'a
+(*consts ast :: 'a
+consts ast' :: 'a*)
+(*
 notation (latex output)
 alpha_ty ("\<approx>ty") and
 alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
 fa_trm ("fa\<^bsub>trm\<^esub>") and
-alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
+alpha_trm2 ("\<approx>\<^bsub>assn\<^esub>\<approx>\<^bsub>trm\<^esub>") and
-fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>")(*>*)
+fa_trm2 ("fa\<^bsub>assn\<^esub>fa\<^bsub>trm\<^esub>") and
+ast ("'(as, t')") and
+ast' ("'(as', t\<PRIME> ')")
+*)
+(*>*)
 text {*
 Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}
 we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$ with the following clauses:
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
-\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
+%  \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-{@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
+%  {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
-\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
+%  \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-{@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fa_trm2 p (bn as', (as', t'))"}}
+%  {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}
 \end{tabular}
 \end{center}
 \begin{center}
 \begin{tabular}{@ {}c @ {}}

changeset 2349	eaf5209669de
parent 2348	09b476c20fe1
child 2350	0a5320c6a7e6