--- a/Nominal/Test.thy Fri Mar 19 00:35:20 2010 +0100
+++ b/Nominal/Test.thy Fri Mar 19 00:35:58 2010 +0100
@@ -62,7 +62,7 @@
fixes c::"'a::fs"
assumes a1: "\<And>name c. P c (Vr name)"
and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
- and a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+ and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
shows "P c lm"
proof -
have "\<And>p. P c (p \<bullet> lm)"
@@ -87,6 +87,7 @@
apply(simp add: fresh_Pair)
apply(simp)
apply(rule a3)
+ apply(simp add: fresh_Pair)
apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
apply(simp)
apply(simp add: fresh_def)
@@ -99,6 +100,38 @@
qed
+lemma
+ fixes c::"'a::fs"
+ assumes a1: "\<And>name c. P c (Vr name)"
+ and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+ and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+ shows "P c lm"
+proof -
+ have "\<And>p. P c (p \<bullet> lm)"
+ apply(induct lm arbitrary: c rule: lm.induct)
+ apply(simp only: lm.perm)
+ apply(rule a1)
+ apply(simp only: lm.perm)
+ apply(rule a2)
+ apply(blast)[1]
+ apply(assumption)
+ thm at_set_avoiding
+ apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
+ apply(erule exE)
+ apply(rule_tac t="p \<bullet> Lm name lm" and
+ s="q \<bullet> p \<bullet> Lm name lm" in subst)
+ defer
+ apply(simp add: lm.perm)
+ apply(rule a3)
+ apply(simp add: eqvts fresh_star_def)
+ apply(drule_tac x="q + p" in meta_spec)
+ apply(simp)
+ sorry
+ then have "P c (0 \<bullet> lm)" by blast
+ then show "P c lm" by simp
+qed
+
+
nominal_datatype lam =
VAR "name"
| APP "lam" "lam"
@@ -418,14 +451,6 @@
ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
-lemma supports_subset:
- fixes S1 S2 :: "atom set"
- assumes a: "S1 supports x"
- and b: "S1 \<subseteq> S2"
- shows "S2 supports x"
- using a b
- by (auto simp add: supports_def)
-
lemma finite_fv_t_tyS:
fixes T::"t"
and S::"tyS"
@@ -473,6 +498,10 @@
(* example 1 from Terms.thy *)
+
+
+
+
nominal_datatype trm1 =
Vr1 "name"
| Ap1 "trm1" "trm1"
@@ -622,6 +651,28 @@
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
+lemma
+"fv_mexp j = supp j \<and> fv_body k = supp k \<and>
+(fv_defn c = supp c \<and> fv_cbinders c = {a. infinite {b. \<not>alpha_cbinders ((a \<rightleftharpoons> b) \<bullet> c) c}}) \<and>
+fv_sexp d = supp d \<and> fv_sbody e = supp e \<and>
+(fv_spec l = supp l \<and> fv_Cbinders l = {a. infinite {b. \<not>alpha_Cbinders ((a \<rightleftharpoons> b) \<bullet> l) l}}) \<and>
+fv_tyty g = supp g \<and> fv_path h = supp h \<and> fv_trmtrm i = supp i"
+apply(induct rule: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct)
+apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv)
+apply(simp_all only: supp_Abs[symmetric])
+apply(simp_all (no_asm) only: supp_def)
+apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm)
+apply(simp_all only: permute_ABS)
+apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff Abs_eq_iff)
+apply(simp_all only: alpha_gen)
+apply(simp_all only: eqvts[symmetric] supp_Pair)
+apply(simp_all only: eqvts Pair_eq)
+apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
+apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
+apply(simp_all only: de_Morgan_conj[symmetric])
+apply simp_all
+done
+
(* example 3 from Peter Sewell's bestiary *)
nominal_datatype exp =
--- a/Paper/Paper.thy Fri Mar 19 00:35:20 2010 +0100
+++ b/Paper/Paper.thy Fri Mar 19 00:35:58 2010 +0100
@@ -15,17 +15,148 @@
section {* Introduction *}
text {*
+ So far, Nominal Isabelle provides a mechanism for constructing
+ automatically alpha-equated terms such as
- It has not yet fared so well in the POPLmark challenge
- as the second part contain a formalisation of records
- where ...
+ \begin{center}
+ $t ::= x \mid t\;t \mid \lambda x. t$
+ \end{center}
+
+ \noindent
+ For such terms it derives automatically a reasoning
+ infrastructure, which has been used in formalisations of an equivalence
+ checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
+ Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
+ \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result
+ for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been
+ used by Pollack for formalisations in the locally-nameless approach to
+ binding \cite{SatoPollack10}.
+
+ However, Nominal Isabelle fared less well in a formalisation of
+ the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
+ are of the form
+
+ \begin{center}
+ \begin{tabular}{l}
+ $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ and the quantification abstracts over a finite (possibly empty) set of type variables.
+ While it is possible to formalise such abstractions by iterating single bindings,
+ it leads to a very clumsy formalisation of W. This need of iterating single binders
+ for representing multiple binders is also the reason why Nominal Isabelle and other
+ theorem provers have not fared extremely well with the more advanced tasks
+ in the POPLmark challenge \cite{challenge05}, because also there one would be able
+ to aviod clumsy reasoning if there were a mechanisms for abstracting several variables
+ at once.
+
+ To see this, let us point out some interesting properties of binders abstracting multiple
+ variables. First, in the case of type-schemes, we do not like to make a distinction
+ about the order of the bound variables. Therefore we would like to regard the following two
+ type-schemes as alpha-equivalent
+
+ \begin{center}
+ $\forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$
+ \end{center}
+
+ \noindent
+ but the following two should \emph{not} be alpha-equivalent
+
+ \begin{center}
+ $\forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$
+ \end{center}
+
+ \noindent
+ assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as
+ alpha-equivalent, if they differ only on \emph{vacuous} binders, such as
+
+ \begin{center}
+ $\forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$
+ \end{center}
+
+ \noindent
+ In this paper we will give a general abstraction mechanism and associated
+ notion of alpha-equivalence that can be used to faithfully represent
+ type-schemes in Nominal Isabelle. The difficulty of finding the right notion
+ for alpha-equivalence in this case can be appreciated by considering that the
+ definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
+
+
- The difficulty can be appreciated by considering that the
- definition given by Leroy in \cite{Leroy92} is incorrect (it omits a
- side-condition).
+ However, the notion of alpha-equivalence that is preserved by vacuous binders is not
+ alway wanted. For example in terms like
+
+ \begin{center}
+ $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$
+ \end{center}
+
+ \noindent
+ we might not care in which order the assignments $x = 3$ and $y = 2$ are
+ given, but it would be unusual to regard the above term as alpha-equivalent
+ with
+
+ \begin{center}
+ $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,\backslash\,y \END$
+ \end{center}
+
+ \noindent
+ Therefore we will also provide a separate abstraction mechanism for cases
+ in which the order of binders does not matter, but the ``cardinality'' of the
+ binders has to be the same.
+
+ However, we found that this is still not sufficient for covering language
+ constructs frequently occuring in programming language research. For example
+ in $\mathtt{let}$s involving patterns
+
+ \begin{center}
+ $\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END$
+ \end{center}
+
+ \noindent
+ we want to bind all variables from the pattern (there might be an arbitrary
+ number of them) inside the body of the $\mathtt{let}$, but we also care about
+ the order of these variables, since we do not want to identify the above term
+ with
- Examples: type-schemes, Spi-calculus
+ \begin{center}
+ $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$
+ \end{center}
+
+ \noindent
+ As a result, we provide three general abstraction mechanisms for multiple binders
+ and allow the user to chose which one is intended when formalising a
+ programming language calculus.
+
+ By providing these general abstraction mechanisms, however, we have to work around
+ a problem that has been pointed out by Pottier in \cite{Pottier06}: in
+ $\mathtt{let}$-constructs of the form
+
+ \begin{center}
+ $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
+ \end{center}
+ \noindent
+ which bind all the $x_i$ in $s$, we might not care about the order in
+ which the $x_i = t_i$ are given, but we do care about the information that there are
+ as many $x_i$ as there are $t_i$. We lose this information if we represent the
+ $\mathtt{let}$-constructor as something like
+
+ \begin{center}
+ $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$
+ \end{center}
+
+ \noindent
+ where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes bound
+ in $s$. In this representation we need additional predicates to ensure
+ that the two lists are of equal length. This can result into very
+ unintelligible reasoning (see for example~\cite{BengtsonParow09}).
+
+
+
+
+
Contributions: We provide definitions for when terms
involving general bindings are alpha-equivelent.
@@ -51,19 +182,21 @@
%\end{pspicture}
%\end{center}
-
+ quotient package \cite{Homeier05}
*}
section {* A Short Review of the Nominal Logic Work *}
text {*
At its core, Nominal Isabelle is based on the nominal logic work by Pitts
- \cite{Pitts03}. Two central notions in this work are sorted atoms and
- permutations of atoms. The sorted atoms represent different
- kinds of variables, such as term- and type-variables in Core-Haskell, and it
- is assumed that there is an infinite supply of atoms for each sort.
- However, in order to simplify the description of our work, we shall
- assume in this paper that there is only a single sort of atoms.
+ \cite{Pitts03}. The implementation of this work are described in
+ \cite{HuffmanUrban10}, which we review here briefly to aid the description
+ of what follows in the next sections. Two central notions in the nominal
+ logic work are sorted atoms and permutations of atoms. The sorted atoms
+ represent different kinds of variables, such as term- and type-variables in
+ Core-Haskell, and it is assumed that there is an infinite supply of atoms
+ for each sort. However, in order to simplify the description of our work, we
+ shall assume in this paper that there is only a single sort of atoms.
Permutations are bijective functions from atoms to atoms that are
the identity everywhere except on a finite number of atoms. There is a
@@ -96,38 +229,72 @@
@{thm[display,indent=5] fresh_def[no_vars]}
\noindent
- We also use for sets of atoms the abbreviation @{thm fresh_star_def[no_vars]}.
+ We also use for sets of atoms the abbreviation
+ @{thm (lhs) fresh_star_def[no_vars]} defined as
+ @{thm (rhs) fresh_star_def[no_vars]}.
A striking consequence of these definitions is that we can prove
without knowing anything about the structure of @{term x} that
swapping two fresh atoms, say @{text a} and @{text b}, leave
@{text x} unchanged.
- \begin{Property}
+ \begin{property}
@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
- \end{Property}
+ \end{property}
- \begin{Property}
+ \noindent
+ For a proof see \cite{HuffmanUrban10}.
+
+ \begin{property}
@{thm[mode=IfThen] at_set_avoiding[no_vars]}
- \end{Property}
+ \end{property}
*}
section {* Abstractions *}
+text {*
+ General notion of alpha-equivalence (depends on a free-variable
+ function and a relation).
+*}
+
section {* Alpha-Equivalence and Free Variables *}
+text {*
+ Restrictions
+
+ \begin{itemize}
+ \item non-emptyness
+ \item positive datatype definitions
+ \item finitely supported abstractions
+ \item respectfulness of the bn-functions\bigskip
+ \item binders can only have a ``single scope''
+ \end{itemize}
+*}
+
section {* Examples *}
+section {* Adequacy *}
+
+section {* Related Work *}
+
section {* Conclusion *}
text {*
+ Complication when the single scopedness restriction is lifted (two
+ overlapping permutations)
+*}
+
+text {*
+
+ TODO: function definitions:
+ \medskip
\noindent
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for the
many discussions about Nominal Isabelle. We thank Peter Sewell for
making the informal notes \cite{SewellBestiary} available to us and
- also explaining some of the finer points of the OTT-tool.
+ also for explaining some of the finer points of the OTT-tool.
*}
--- a/Paper/document/root.bib Fri Mar 19 00:35:20 2010 +0100
+++ b/Paper/document/root.bib Fri Mar 19 00:35:58 2010 +0100
@@ -1,7 +1,30 @@
+@InProceedings{Homeier05,
+ author = {P.~Homeier},
+ title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients},
+ booktitle = {Proc.~of the 18th International Conference on Theorem
+ Proving in Higher Order Logics (TPHOLs)},
+ pages = {130--146},
+ year = {2005},
+ volume = {3603},
+ series = {LNCS}
+}
+
+@INPROCEEDINGS{Pottier06,
+ author = {F.~Pottier},
+ title = {{A}n {O}verview of {C$\alpha$ml}},
+ year = {2006},
+ booktitle = {ACM Workshop on ML},
+ pages = {27--52},
+ volume = {148},
+ number = {2},
+ series = {ENTCS}
+}
+
@Unpublished{HuffmanUrban10,
author = {B.~Huffman and C.~Urban},
title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},
- note = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
+ note = {To appear at ITP 2010},
+ annote = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
year = {2010}
}
@@ -19,6 +42,21 @@
note = {Personal communication.}
}
+@InProceedings{challenge05,
+ author = {B.~E.~Aydemir and A.~Bohannon and M.~Fairbairn and
+ J.~N.~Foster and B.~C.~Pierce and P.~Sewell and
+ D.~Vytiniotis and G.~Washburn and S.~Weirich and
+ S.~Zdancewic},
+ title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark
+ {C}hallenge},
+ booktitle = {Proc.~of the 18th International Conference on Theorem Proving in Higher-Order
+ Logics (TPHOLs)},
+ pages = {50--65},
+ year = {2005},
+ volume = {3603},
+ series = {LNCS}
+}
+
@Unpublished{SatoPollack10,
author = {M.~Sato and R.~Pollack},
title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},
--- a/Paper/document/root.tex Fri Mar 19 00:35:20 2010 +0100
+++ b/Paper/document/root.tex Fri Mar 19 00:35:58 2010 +0100
@@ -6,21 +6,28 @@
\usepackage{tikz}
\usepackage{pgf}
\usepackage{pdfsetup}
+\usepackage{ot1patch}
\urlstyle{rm}
\isabellestyle{it}
+\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
+\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymiota}{}
\renewcommand{\isasymemptyset}{$\varnothing$}
+\newcommand{\LET}{\;\mathtt{let}\;}
+\newcommand{\IN}{\;\mathtt{in}\;}
+\newcommand{\END}{\;\mathtt{end}\;}
+\newcommand{\AND}{\;\mathtt{and}\;}
%----------------- theorem definitions ----------
-\newtheorem{Property}{Theorem}[section]
+\newtheorem{property}{Property}[section]
\newtheorem{Theorem}{Theorem}[section]
\newtheorem{Definition}[Theorem]{Definition}
\newtheorem{Example}{\it Example}[section]
@@ -38,16 +45,16 @@
\maketitle
\begin{abstract}
-Nominal Isabelle is a definitional extension of the Isabelle/HOL
-theorem prover. It provides a proving infrastructure for
-conveninet reasoning about programming language calculi. In this paper
-we present an extension of Nominal Isabelle for dealing with general binding
-structures. Such structures are ubiquitous in programming language research
-and only very poorly handled by the well-known single abstraction in the
-lambda-calculus. We give definitions for alpha-equivalence and establish
-the reasoning structure for alpha-equated terms. For example we provide
-a strong induction principle that has the variable convention already
-built in.
+Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
+prover. It provides a proving infrastructure for convenient reasoning about
+programming language calculi. In this paper we present an extension of Nominal
+Isabelle in order to deal with general binding structures. Such binding structures
+are ubiquitous in programming language research and only very poorly supported
+with single binders, as for example found in the lambda-calculus. For our
+extension we introduce novel definitions of alpha-equivalence and establish
+automatically the reasoning infrastructure for alpha-equated terms. This
+includes a strong induction principle which has the variable convention
+already built in.
\end{abstract}