nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:be28f7b4b97b
+:468c3c1adcba
 fresh ("_ # _" [51, 51] 50) and
 fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
 supp ("supp _" [78] 73) and
 uminus ("-_" [78] 73) and
 If  ("if _ then _ else _" 10) and
-alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_,_,_\<^esup> _") and
+alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
-alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_,_,_\<^esup> _") and
+alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
-alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") and
+alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
 abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 fv ("fv'(_')" [100] 100) and
 equal ("=") and
 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and
 Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
 Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
 Cons ("_::_" [78,77] 73) and
 supp_gen ("aux _" [1000] 10) and
 alpha_bn ("_ \<approx>bn _")
 (*>*)
 section {* Introduction *}
 text {*
+@{text "(1, (2, 3))"}
 So far, Nominal Isabelle provides a mechanism for constructing
 alpha-equated terms, for example
 \begin{center}
 @{text "t ::= x | t t | \<lambda>x. t"}
 \noindent
 (similarly for $\approx_{\textit{abs\_list}}$
 and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence
 relations and equivariant.
-\begin{lemma}\label{alphaeq} The relations
+\begin{lemma}\label{alphaeq}
-$\approx_{\textit{abs\_set}}$,
+The relations $\approx_{\textit{abs\_set}}$, $\approx_{\textit{abs\_list}}$
-$\approx_{\textit{abs\_list}}$
+and $\approx_{\textit{abs\_res}}$ are equivalence relations, and if @{term
-and $\approx_{\textit{abs\_res}}$
+"abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
-are equivalence
+bs, p \<bullet> y)"} (similarly for the other two relations).
-relations, and if @{term "abs_set (as, x) (bs, y)"} then also
-@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for
-the other two relations).
 \end{lemma}
 \begin{proof}
 Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
 a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
 be easier to analyse these pairs according to  ``clusters'' of the binding clauses.
 Therefore we distinguish the following cases:
 *}
 (*<*)
 consts alpha_ty ::'a
-notation alpha_ty ("\<approx>ty")
+consts alpha_trm ::'a
+consts fv_trm :: 'a
+consts alpha_trm2 ::'a
+consts fv_trm2 :: 'a
+notation (latex output)
+alpha_ty ("\<approx>ty") and
+alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
+fv_trm ("fv\<^bsub>trm\<^esub>") and
+alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
+fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>")
 (*>*)
 text {*
 \begin{itemize}
 \item The @{text "(x\<^isub>i, y\<^isub>i)"} are bodies of shallow binders with type @{text "ty"}. We assume the
 \mbox{@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"}} are the corresponding binders. For the binding mode
 neither a binder nor a body. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"}  provided
 the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are
 recursive arguments of the term-constructor. If they are non-recursive arguments
 then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
-TODO
+{\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
 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
 occuring in @{text "rhs"} under the binding function @{text "bn\<^isub>m"}\\
 $\bullet$ & @{text "x\<^isub>j \<approx> y\<^isub>j"} otherwise\\
 \end{tabular}
 \end{center}
+Again lets take a look at an example for these definitions. For \eqref{letrecs}
+we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
+$\approx_{\textit{bn}}$, with the clauses as follows:
+\begin{center}
+\begin{tabular}{@ {}c @ {}}
+\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
+{@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fv_trm p (bn as', t')"}}\smallskip\\
+\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 fv_trm2 p (bn as', (as', t'))"}}
+\end{tabular}
+\end{center}
+\begin{center}
+\begin{tabular}{@ {}c @ {}}
+\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
+\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'"}}\medskip\\
+\end{tabular}
+\end{center}
+\begin{center}
+\begin{tabular}{@ {}c @ {}}
+\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
+\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'"}}\medskip\\
+\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
+a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is
+a non-recursive binder), since the terms inside an assignment are not meant
+to be under the binder. Such a premise is not needed in @{text "Let_rec"},
+because there everything from the assignment is under the binder.
 *}
-section {* The Lifting of Definitions and Properties *}
+section {* Establishing the Reasoning Infrastructure *}
 text {*
-To define the quotient types we first need to show that the defined
+Having made all these definition for raw terms, we can start to introduce
-relations are equivalence relations.
+the resoning infrastructure for the specified types. For this we first
+have to show that the alpha-equivalence relation defined in the previous
-\begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"}
+sections are indeed equivalence relations.
-defined as above are equivalence relations and are equivariant.
+\begin{lemma}
+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
+@{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant.
 \end{lemma}
-\begin{proof} Reflexivity by induction on the raw datatype. Symmetry,
-transitivity and equivariance by induction on the alpha equivalence
+\begin{proof}
-relation. Using lemma \ref{alphaeq}, the conditions follow by simple
+The proof is by induction over the definitions. The non-trivial
-calculations.  \end{proof}
+cases involves premises build up by $\approx_{\textit{set}}$,
+$\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They
-\noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
+can be dealt with like in Lemma~\ref{alphaeq}.
+\end{proof}
+\noindent
+We can feed this lemma into our quotient package and obtain new types @{text
+"ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text
+"ty"}$_{1..n}$. We also obtain definitions for the term-constructors @{text
+"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
+Introduction).
+{\bf TODO below.}
+then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
 the raw definitions to the quotient type, we need to prove that they
 \emph{respect} the relation. We follow the definition of respectfullness given
 by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition
 is that when a function (or constructor) is given arguments that are
 alpha-equivalent the results are also alpha equivalent. For arguments that are
 \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"}.
 \end{proof}
 *}
-(* @{thm "ACons_subst[no_vars]"}*)
-text {*
-%%% FIXME: The restricions should have already been described in previous sections?
-Restrictions
-\begin{itemize}
-\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 all bindings must have the same mode
-\end{itemize}
-*}
-section {* Examples *}
 text {*
 \begin{figure}
 \begin{boxedminipage}{\linewidth}
 \phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
 $|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
 $|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
 $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
 $|$~@{text "Lam v::var ty t::trm"}  \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
-$|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~{text x}~\isacommand{in}~{text t}\\
+$|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
 $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
 \isacommand{and}~@{text "assoc_lst ="}\\
 \phantom{$|$}~@{text ANil}~%
 $|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
 \isacommand{and}~@{text "pat ="}\\
 $|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
 $|$~@{text "bv3 TVCKNil = []"}\\
 $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
 \end{tabular}
 \end{boxedminipage}
-\caption{\label{nominalcorehas}}
+\caption{The nominal datatype declaration for Core-Haskell. At the moment we
+do not support nested types; therefore we explicitly have to unfold the
+lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
+in a future version of Nominal Isabelle. Apart from that, the
+declaration follows closely the original in Figure~\ref{corehas}. The
+point of our work is that having made such a declaration one obtains
+automatically a reasoning infrastructure for Core-Haskell.\label{nominalcorehas}}
 \end{figure}
 *}
+(* @{thm "ACons_subst[no_vars]"}*)
-section {* Adequacy *}
+section {* Strong Induction Principles *}
 section {* Related Work *}
 text {*
 To our knowledge the earliest usage of general binders in a theorem prover setting is
 An attempt of representing general binders in the old version of Isabelle
 based also on iterating single binders is described in \cite{BengtsonParow09}.
 The reasoning there turned out to be quite complex.
 Ott is better with list dot specifications; subgrammars, is untyped;
 *}
+text {*
+%%% FIXME: The restricions should have already been described in previous sections?
+Restrictions
+\begin{itemize}
+\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 all bindings must have the same mode
+\end{itemize}
+*}
 section {* Conclusion *}
 text {*
 The formalisation presented here will eventually become part of the
 Isabelle distribution, but for the moment it can be downloaded from
 the Mercurial repository linked at
 \href{http://isabelle.in.tum.de/nominal/download}
 {http://isabelle.in.tum.de/nominal/download}.\medskip
-*}
-text {*
 \noindent
 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for
 many discussions about Nominal Isabelle. We thank Peter Sewell for
 making the informal notes \cite{SewellBestiary} available to us and
 also for patiently explaining some of the finer points about the abstract
 definitions and about the implementation of the Ott-tool. We
 also thank Stephanie Weirich for suggesting to separate the subgrammars
 of kinds and types in our Core-Haskell example.
 *}
 (*<*)

changeset 1739	468c3c1adcba
parent 1737	8b6a285ad480
child 1740	2afee29cf81c