nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:8f142ae324e2
+:46f753eeb0b8
 Abs_res ("[_]\<^bsub>res\<^esub>._") and
 Abs_print ("_\<^bsub>set\<^esub>._") and
 Cons ("_::_" [78,77] 73) and
 supp_gen ("aux _" [1000] 10) and
 alpha_bn ("_ \<approx>bn _")
+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_trm ("\<approx>\<^bsub>trm\<^esub>") and
+fa_trm ("fa\<^bsub>trm\<^esub>") and
+alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and
+fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and
+ast ("'(as, t')") and
+ast' ("'(as', t\<PRIME> ')")
 (*>*)
 section {* Introduction *}
 \noindent
 The first mode is for binding lists of atoms (the order of binders matters);
 the second is for sets of binders (the order does not matter, but the
 cardinality does) and the last is for sets of binders (with vacuous binders
-preserving $\alpha$-equivalence). As indicated, the ``\isacommand{in}-part'' of a binding
+preserving $\alpha$-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
 clause will be called \emph{bodies}; the
 ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
 Ott, we allow multiple labels in binders and bodies. For example we allow
 binding clauses of the form:
 \end{center}
 \noindent
 Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick
 out different atoms to become bound, respectively be free, in @{text "p"}.
-(Since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit
+(Since the Ott-tool does not derive a reasoning infrastructure for
-such specifications.)
+$\alpha$-equated terms, it can permit such specifications.)
 We also need to restrict the form of the binding functions in order
 to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
 terms. The main restriction is that we cannot return an atom in a binding function that is also
 bound in the corresponding term-constructor. That means in \eqref{letpat}
 that the term-constructors @{text PVar} and @{text PTup} may
 not have a binding clause (all arguments are used to define @{text "bn"}).
 In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
 may have a binding clause involving the argument @{text t} (the only one that
 is \emph{not} used in the definition of the binding function). This restriction
-is sufficient for defining the binding function over $\alpha$-equated terms.
+is sufficient for having the binding function over $\alpha$-equated terms.
 In the version of
 Nominal Isabelle described here, we also adopted the restriction from the
 Ott-tool that binding functions can only return: the empty set or empty list
 (as in case @{text PNil}), a singleton set or singleton list containing an
 $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other
 binding modes). This premise defines $\alpha$-equivalence of two abstractions
 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
+For $\approx_{\,\textit{set}}$ (respectively $\approx_{\,\textit{list}}$ and
+$\approx_{\,\textit{res}}$)  we also need
 a compound free-atom function for the bodies defined as
 %
 \begin{center}
 \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
 \end{center}
 \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
 \end{center}
 \noindent
 This premise accounts for $\alpha$-equivalence of the bodies of the binding
-clause. Similarly for the other binding modes.
+clause.
 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
+right-hand sides of assignments are $\alpha$-equivalent. For this we use
 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 tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})
+and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}.
 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"}
+@{text "prems(bc\<^isub>i) \<equiv> P  \<and>   L R' L'"}
 \end{center}
 \noindent
-where the auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$
+The auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$
-are defined as follows: assuming a @{text bn}-clause is of the form
+in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form
 %
 \begin{center}
 @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
 \end{center}
 \noindent
 where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
-then the $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
+then the corresponding $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
 %
 \begin{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
 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"}
 for the existentially quantified permutation).
-*}
-(*<*)
+Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}
-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>, \<approx>\<^bsub>trm\<^esub>')") and
-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'"}}
 {@{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'"}}
+\makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-{@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}
+{@{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 @ {}}
-\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
+\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\smallskip\\
 \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'"}}
 \end{tabular}
 \end{center}
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
-\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
+\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\smallskip\\
 \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'"}}
 \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
+the components in an assignment that are \emph{not} bound. This is needed in the
-a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is
+in the clause for @{text "Let"} (which is has
 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.
 *}
 text {*
 Having made all necessary definitions for raw terms, we can start
 introducing the reasoning infrastructure for the $\alpha$-equated types the
 user originally specified. We sketch in this section the facts we need for establishing
 this reasoning infrastructure. First we have to show that the
-$\alpha$-equivalence relations defined in the previous section are indeed
+$\alpha$-equivalence relations defined in the previous section are
 equivalence relations.
 \begin{lemma}\label{equiv}
 Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
 @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and
 can be dealt with as in Lemma~\ref{alphaeq}.
 \end{proof}
 \noindent
 We can feed this lemma into our quotient package and obtain new types @{text
-"ty\<AL>\<^bsub>1..n\<^esub>"} representing $\alpha$-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain
+"ty"}$^\alpha_{1..n}$ representing $\alpha$-equated terms of types @{text "ty"}$_{1..n}$.
-definitions for the term-constructors @{text
+We also obtain definitions for the term-constructors @{text
 "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
 "C"}$_{1..m}$, and similar definitions for the free-atom functions @{text
 "fa_ty"}$^\alpha_{1..n}$ and the binding functions @{text
 "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the
 user, since they are given in terms of the isomorphisms we obtained by
 In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient
 package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"}
 are \emph{respectful} w.r.t.~the $\alpha$-equivalence relations (see \cite{Homeier05}).
 Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
 @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that
+%
 \begin{center}
 @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}
 \end{center}
 \noindent
 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\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
+"ty"}$_{1..n}$ fall into this category. So we can also add to our infrastructure
 induction principles that establish
 \begin{center}
 @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>1 y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^esub>\<^isub>n y\<^isub>n "}
 \end{center}

changeset 2359	46f753eeb0b8
parent 2350	0a5320c6a7e6
child 2360	99134763d03e