Commit 3ad08fbe authored by Gerwin Klein's avatar Gerwin Klein
Browse files

make Nominal2 a full entry

parent 9a4ebc4f6e05
......@@ -3567,3 +3567,22 @@ abstract =
a procedure for computing such implicates and establish its soundness
and completeness.
[Nominal2]
title = Nominal 2
author = Christian Urban <http://www.inf.kcl.ac.uk/staff/urbanc/>, Stefan Berghofer <http://www.in.tum.de/~berghofe>, Cezary Kaliszyk <>
date = 2013-02-21
topic = Tools
abstract =
<p>Dealing with binders, renaming of bound variables, capture-avoiding
substitution, etc., is very often a major problem in formal
proofs, especially in proofs by structural and rule
induction. Nominal Isabelle is designed to make such proofs easy to
formalise: it provides an infrastructure for declaring nominal
datatypes (that is alpha-equivalence classes) and for defining
functions over them by structural recursion. It also provides
induction principles that have Barendregt’s variable convention
already built in.
</p><p>
This entry can be used as a more advanced replacement for
HOL/Nominal in the Isabelle distribution.
</p>
......@@ -46,7 +46,7 @@ val simp_attr = Attrib.internal (K Simplifier.simp_add)
val induct_attr = Attrib.internal (K Induct.induct_simp_add)
*}
section{* Interface for nominal_datatype *}
section{* Interface for @{text nominal_datatype} *}
ML {*
fun get_cnstrs dts =
......@@ -64,7 +64,7 @@ fun get_bn_fun_strs bn_funs =
*}
text {* Infrastructure for adding "_raw" to types and terms *}
text {* Infrastructure for adding @{text "_raw"} to types and terms *}
ML {*
fun add_raw s = s ^ "_raw"
......
......@@ -18,7 +18,7 @@ declare [[typedef_overloaded]]
section {* Atoms and Sorts *}
text {* A simple implementation for atom_sorts is strings. *}
text {* A simple implementation for @{text atom_sorts} is strings. *}
(* types atom_sort = string *)
text {* To deal with Church-like binding we use trees of
......@@ -762,7 +762,7 @@ instance int :: pure
proof qed (rule permute_int_def)
section {* Infrastructure for Equivariance and Perm_simp *}
section {* Infrastructure for Equivariance and @{text Perm_simp} *}
subsection {* Basic functions about permutations *}
......@@ -792,7 +792,7 @@ lemmas [eqvt] =
(* multisets *)
permute_multiset
subsection {* perm_simp infrastructure *}
subsection {* @{text perm_simp} infrastructure *}
definition
"unpermute p = permute (- p)"
......@@ -812,7 +812,7 @@ lemma eqvt_bound:
shows "p \<bullet> unpermute p x \<equiv> x"
unfolding unpermute_def by simp
text {* provides perm_simp methods *}
text {* provides @{text perm_simp} methods *}
ML_file "nominal_permeq.ML"
......@@ -1906,7 +1906,7 @@ simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") =
end
*}
subsection {* helper functions for nominal_functions *}
subsection {* helper functions for @{text nominal_functions} *}
lemma THE_defaultI2:
assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
......@@ -3121,7 +3121,7 @@ lemma flip_at_base_simps [simp]:
unfolding atom_eqvt [symmetric]
by simp_all
text {* the following two lemmas do not hold for at_base,
text {* the following two lemmas do not hold for @{text at_base},
only for single sort atoms from at *}
lemma flip_triple:
......
This is not a regular AFP entry!
This Nominal2 module is expected to disappear from the AFP and be merged into
the Isabelle distribution before the next Isabelle release.
chapter AFP
session "Nominal2" (AFP) = HOL +
options [document = false]
theories
options [timeout = 600]
theories [document = false]
"~~/src/HOL/Library/Old_Datatype"
"~~/src/HOL/Library/Cardinality"
"~~/src/HOL/Library/FinFun"
"~~/src/HOL/Library/Infinite_Set"
"~~/src/HOL/Library/Phantom_Type"
(* cannot depend on HOL-Library image because of name clash with Library/FSet: *)
"~~/src/HOL/Quotient_Examples/FSet"
theories
"Nominal2"
"Atoms"
"Eqvt"
document_files
"root.tex"
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
\begin{document}
\title{Nominal 2}
\author{Christian Urban, Stefan Berghofer, and Cezary Kaliszyk}
\maketitle
\begin{abstract}
Dealing with binders, renaming of bound variables, capture-avoiding
substitution, etc., is very often a major problem in formal
proofs, especially in proofs by structural and rule
induction. Nominal Isabelle is designed to make such proofs easy to
formalise: it provides an infrastructure for declaring nominal
datatypes (that is alpha-equivalence classes) and for defining
functions over them by structural recursion. It also provides
induction principles that have Barendregt’s variable convention
already built in.
This entry can be used as a more advanced replacement for
HOL/Nominal in the Isabelle distribution.
\end{abstract}
\tableofcontents
% include generated text of all theories
\input{session}
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
......@@ -68,7 +68,7 @@ However, other technical problems had to be solved in order to complete the argu
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="HereditarilyFinite.shtml">HereditarilyFinite</a></td></tr>
<td class="data"><a href="HereditarilyFinite.shtml">HereditarilyFinite</a>, <a href="Nominal2.shtml">Nominal2</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
......
......@@ -77,6 +77,10 @@ In his seminal paper "Natural Semantics for Lazy Evaluation", John Launchbury pr
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Nominal2.shtml">Nominal2</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
......
<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<table width="100%">
<tbody>
<tr>
<td width="20%" align="center" valign="top">
<!-- navigation -->
<!--#include file="nav.html"-->
</td>
<td width="80%" valign="top">
<!-- content -->
<div align="center">
<p>&nbsp;</p>
<h1><font class="first">N</font>ominal
2
</h1>
<p></p>
<table width="80%" class="data">
<tbody>
<tr><td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Nominal 2</td></tr>
<tr><td class="datahead">Author:</td>
<td class="data"><a href="http://www.inf.kcl.ac.uk/staff/urbanc/">Christian Urban</a>, <a href="http://www.in.tum.de/~berghofe">Stefan Berghofer</a> and Cezary Kaliszyk</td></tr>
<tr><td class="datahead">Submission date:</td>
<td class="data">2013-02-21</td></tr>
<tr><td class="datahead" valign="top">Abstract:</td>
<td class="abstract">
<p>Dealing with binders, renaming of bound variables, capture-avoiding
substitution, etc., is very often a major problem in formal
proofs, especially in proofs by structural and rule
induction. Nominal Isabelle is designed to make such proofs easy to
formalise: it provides an infrastructure for declaring nominal
datatypes (that is alpha-equivalence classes) and for defining
functions over them by structural recursion. It also provides
induction principles that have Barendregt’s variable convention
already built in.
</p><p>
This entry can be used as a more advanced replacement for
HOL/Nominal in the Isabelle distribution.
</p>
</td></tr>
<tr><td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Nominal2-AFP,
author = {Christian Urban and Stefan Berghofer and Cezary Kaliszyk},
title = {Nominal 2},
journal = {Archive of Formal Proofs},
month = feb,
year = 2013,
note = {\url{http://isa-afp.org/entries/Nominal2.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->
</tbody>
</table>
<p></p>
<!--#set var="name" value="Nominal2" -->
<!--#set var="binfo" value="../browser_info/current/AFP/${name}" -->
<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="<!--#echo var="outline" -->">Proof outline</a><br>
<a href="<!--#echo var="doc" -->">Proof document</a>
</td>
<!-- link to README.hmtl if no document exists -->
</tr>
<tr>
<td class="links">
<a href="<!--#echo var="browse" -->">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="<!--#echo var="tar" -->">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None </td></tr>
</tbody>
</table>
<!-- entry data end -->
</td> </tr> </table>
</body>
</html>
......@@ -1086,6 +1086,15 @@ Wenda Li
<a href="http://www.infsec.ethz.ch/people/andreloc">Andreas Lochbihler</a>
</td></tr>
<tr><td class="entry">
2013-02-21:
<a href="entries/Nominal2.shtml">Nominal 2</a>
<br>Author:
<a href="http://www.inf.kcl.ac.uk/staff/urbanc/">Christian Urban</a>,
<a href="http://www.in.tum.de/~berghofe">Stefan Berghofer</a> and
Cezary Kaliszyk
</td></tr>
<tr><td class="entry">
2013-01-31:
<a href="entries/Launchbury.shtml">The Correctness of Launchbury's Natural Semantics for Lazy Evaluation</a>
......
......@@ -458,6 +458,7 @@
<div class="list">
<a href="entries/Case_Labeling.shtml">Case_Labeling</a> &nbsp;
<a href="entries/DPT-SAT-Solver.shtml">DPT-SAT-Solver</a> &nbsp;
<a href="entries/Nominal2.shtml">Nominal2</a> &nbsp;
</div>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment