3 \usepackage{isabelle} |
3 \usepackage{isabelle} |
4 \usepackage{isabellesym} |
4 \usepackage{isabellesym} |
5 \usepackage{amsmath} |
5 \usepackage{amsmath} |
6 \usepackage{amssymb} |
6 \usepackage{amssymb} |
7 \usepackage{longtable} |
7 \usepackage{longtable} |
|
8 \usepackage{graphics} |
|
9 \usepackage{pdfsetup} |
8 |
10 |
9 |
|
10 \usepackage{pdfsetup} |
|
11 \urlstyle{rm} |
11 \urlstyle{rm} |
12 \isabellestyle{it} |
12 \isabellestyle{it} |
13 \renewcommand{\isastyle}{\isastyleminor} |
13 \renewcommand{\isastyle}{\isastyleminor} |
14 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
14 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
15 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
15 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
16 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
16 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
17 \renewcommand{\isasymequiv}{$\dn$} |
17 \renewcommand{\isasymequiv}{$\dn$} |
18 \renewcommand{\isasymiota}{} |
18 \renewcommand{\isasymiota}{} |
19 \renewcommand{\isasymrightleftharpoons}{} |
19 \renewcommand{\isasymrightleftharpoons}{} |
20 \renewcommand{\isasymemptyset}{$\varnothing$} |
20 \renewcommand{\isasymemptyset}{$\varnothing$} |
|
21 \newcommand{\isasymallatoms}{\ensuremath{\mathbb{A}}} |
21 |
22 |
22 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
23 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
23 |
24 \newcommand\new[0]{\reflectbox{\ensuremath{\mathsf{N}}}} |
24 |
25 |
25 \begin{document} |
26 \begin{document} |
26 |
27 |
27 \title{Implementing the Nominal Logic Work in Isabelle/HOL} |
28 \title{Implementing the Nominal Logic Work in Isabelle/HOL} |
28 \author{Christian Urban \and Brian Huffman} |
29 \author{Christian Urban \and Brian Huffman} |
31 \date{Received: date / Accepted: date} |
32 \date{Received: date / Accepted: date} |
32 |
33 |
33 \maketitle |
34 \maketitle |
34 |
35 |
35 \begin{abstract} |
36 \begin{abstract} |
36 Pitts et al introduced a beautiful theory about names and binding based on the |
37 In his nominal logic work, Pitts introduced a beautiful theory about names and |
37 notions of atoms, permutations and support. The engineering challenge is to |
38 binding based on the notions of atoms, permutations and support. The |
38 smoothly adapt this theory to a theorem prover environment, in our case |
39 engineering challenge is to smoothly adapt this theory to a theorem prover |
39 Isabelle/HOL. For this we have to formulate the theory so that it is |
40 environment, in our case Isabelle/HOL. For this we have to formulate the |
40 compatible with HOL, which the original formulation by Pitts is not. We |
41 theory so that it is compatible with HOL, which the original formulation by |
41 present a formalisation that is based on a unified atom type |
42 Pitts is not. We achieve this by not requiring that every object in our |
42 and that represents permutations by bijective functions from atoms to atoms. |
43 discourse has finite support. We present a formalisation that is based on a |
43 Interestingly, we allow swappings, which are permutations build from two |
44 unified atom type and that represents permutations by bijective functions from |
44 atoms, to be ill-sorted. We also describe a formalisation of two |
45 atoms to atoms. Interestingly, we allow swappings, which are permutations |
45 abstraction operators that bind sets of names. |
46 build from two atoms, to be ill-sorted. We also describe a formalisation of |
|
47 two abstraction operators that bind sets of names. |
46 \end{abstract} |
48 \end{abstract} |
47 |
49 |
48 % generated text of all theories |
50 % generated text of all theories |
49 \input{session} |
51 \input{session} |
50 |
52 |