--- a/Nominal/Nominal2_Supp.thy Thu Mar 18 10:15:57 2010 +0100
+++ b/Nominal/Nominal2_Supp.thy Thu Mar 18 11:33:37 2010 +0100
@@ -17,23 +17,23 @@
definition
fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)
where
- "xs \<sharp>* c \<equiv> \<forall>x \<in> xs. x \<sharp> c"
+ "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"
lemma fresh_star_prod:
- fixes xs::"atom set"
- shows "xs \<sharp>* (a, b) = (xs \<sharp>* a \<and> xs \<sharp>* b)"
+ fixes as::"atom set"
+ shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)"
by (auto simp add: fresh_star_def fresh_Pair)
lemma fresh_star_union:
- shows "(xs \<union> ys) \<sharp>* c = (xs \<sharp>* c \<and> ys \<sharp>* c)"
+ shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
by (auto simp add: fresh_star_def)
lemma fresh_star_insert:
- shows "(insert x ys) \<sharp>* c = (x \<sharp> c \<and> ys \<sharp>* c)"
+ shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"
by (auto simp add: fresh_star_def)
lemma fresh_star_Un_elim:
- "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
+ "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"
unfolding fresh_star_def
apply(rule)
apply(erule meta_mp)
@@ -41,12 +41,12 @@
done
lemma fresh_star_insert_elim:
- "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
+ "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"
unfolding fresh_star_def
by rule (simp_all add: fresh_star_def)
lemma fresh_star_empty_elim:
- "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
+ "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"
by (simp add: fresh_star_def)
lemma fresh_star_unit_elim:
--- a/Paper/Paper.thy Thu Mar 18 10:15:57 2010 +0100
+++ b/Paper/Paper.thy Thu Mar 18 11:33:37 2010 +0100
@@ -1,11 +1,12 @@
(*<*)
theory Paper
-imports "../Nominal/Test"
+imports "../Nominal/Test" "LaTeXsugar"
begin
notation (latex output)
swap ("'(_ _')" [1000, 1000] 1000) and
fresh ("_ # _" [51, 51] 50) and
+ fresh_star ("_ #* _" [51, 51] 50) and
supp ("supp _" [78] 73) and
uminus ("-_" [78] 73) and
If ("if _ then _ else _" 10)
@@ -20,20 +21,44 @@
where ...
The difficulty can be appreciated by considering that the
- definition given by Leroy in [] is incorrect (it omits a
+ definition given by Leroy in \cite{Leroy92} is incorrect (it omits a
side-condition).
Examples: type-schemes, Spi-calculus
Contributions: We provide definitions for when terms
involving general bindings are alpha-equivelent.
+
+ %\begin{center}
+ %\begin{pspicture}(0.5,0.0)(8,2.5)
+ %%\showgrid
+ %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5)
+ %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6}
+ %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9)
+
+ %\pcline[linewidth=0.4mm]{->}(2.6,1.5)(4.8,1.5)
+
+ %\pcline[linewidth=0.2mm](2.2,2.1)(6,2.1)
+ %\pcline[linewidth=0.2mm](2.2,0.9)(6,0.9)
+
+ %\rput(7.3,2.2){$\mathtt{phi}$}
+ %\rput(6,1.5){$\lama$}
+ %\rput[l](7.6,2.05){\begin{tabular}{l}existing\\[-1.6mm]type\end{tabular}}
+ %\rput[r](1.2,1.5){\begin{tabular}{l}new\\[-1.6mm]type\end{tabular}}
+ %\rput(6.1,0.5){\begin{tabular}{l}non-empty\\[-1.6mm]subset\end{tabular}}
+ %\rput[c](1.7,1.5){$\lama$}
+ %\rput(3.7,1.75){isomorphism}
+ %\end{pspicture}
+ %\end{center}
+
+
*}
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}. The central notions in this work are sorted atoms and
+ \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.
@@ -44,7 +69,7 @@
the identity everywhere except on a finite number of atoms. There is a
two-place permutation operation written
- @{text [display,indent=5] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+ @{text[display,indent=5] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
\noindent
with a generic type in which @{text "\<alpha>"} stands for the type of atoms
@@ -62,20 +87,28 @@
only on the permutation operation and on the notion of equality defined for
the type of @{text x}, namely:
- @{thm [display,indent=5] supp_def[no_vars, THEN eq_reflection]}
+ @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]}
\noindent
There is also the derived notion for when an atom @{text a} is \emph{fresh}
for an @{text x}, defined as
- @{thm [display,indent=5] fresh_def[no_vars]}
+ @{thm[display,indent=5] fresh_def[no_vars]}
\noindent
+ We also use for sets of atoms the abbreviation @{thm 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. For the proof we use the following lemma
- about swappings applied to an @{text x}:
+ @{text x} unchanged.
+
+ \begin{Property}
+ @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
+ \end{Property}
+
+ \begin{Property}
+ @{thm[mode=IfThen] at_set_avoiding[no_vars]}
+ \end{Property}
*}
@@ -91,9 +124,10 @@
text {*
\noindent
- {\bf Acknowledgements:} We thank Andrew Pitts for the many discussions
- about the topic. We thank Peter Sewell for making [] available
- to us and explaining some of the finer points of the OTT tool.
+ {\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.
*}
--- a/Paper/ROOT.ML Thu Mar 18 10:15:57 2010 +0100
+++ b/Paper/ROOT.ML Thu Mar 18 11:33:37 2010 +0100
@@ -1,2 +1,3 @@
quick_and_dirty := true;
+no_document use_thys ["LaTeXsugar"];
use_thys ["Paper"];
\ No newline at end of file
--- a/Paper/document/root.bib Thu Mar 18 10:15:57 2010 +0100
+++ b/Paper/document/root.bib Thu Mar 18 11:33:37 2010 +0100
@@ -5,6 +5,20 @@
year = {2010}
}
+@PhdThesis{Leroy92,
+ author = {X.~Leroy},
+ title = {{P}olymorphic {T}yping of an {A}lgorithmic {L}anguage},
+ school = {University Paris 7},
+ year = {1992},
+ note = {INRIA Research Report, No~1778}
+}
+
+@Unpublished{SewellBestiary,
+ author = {P.~Sewell},
+ title = {{A} {B}inding {B}estiary},
+ note = {Personal communication.}
+}
+
@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 Thu Mar 18 10:15:57 2010 +0100
+++ b/Paper/document/root.tex Thu Mar 18 11:33:37 2010 +0100
@@ -3,11 +3,10 @@
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
+\usepackage{tikz}
+\usepackage{pgf}
+\usepackage{pdfsetup}
-%\ConferenceShortName{ICFP}
-%\ConferenceName{International Conference on Functional Programming}
-
-\usepackage{pdfsetup}
\urlstyle{rm}
\isabellestyle{it}
@@ -19,10 +18,9 @@
\renewcommand{\isasymemptyset}{$\varnothing$}
-% for uniform font size
-%\renewcommand{\isastyle}{\isastyleminor}
%----------------- theorem definitions ----------
+\newtheorem{Property}{Theorem}[section]
\newtheorem{Theorem}{Theorem}[section]
\newtheorem{Definition}[Theorem]{Definition}
\newtheorem{Example}{\it Example}[section]
@@ -41,18 +39,18 @@
\maketitle
\begin{abstract}
Nominal Isabelle is a definitional extension of the Isabelle/HOL
-theorem prover. It provides a reasoning infrastructure for formalisations
-of programming language calculi. In this paper we present an extension
-of Nominal Isabelle with general binding constructs. Such constructs
-are important in formalisation ...
+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.
\end{abstract}
-%\begin{keywords}
-%Language formalisations, Isabelle/HOL, POPLmark
-%\end{keywords}
-
-% generated text of all theories
\input{session}
\bibliographystyle{plain}