(*<*)

theory Paper

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)

(*>*)

section {* Introduction *}

text {*

  It has not yet fared so well in the POPLmark challenge

  as the second part contain a formalisation of records 

  where ...

  The difficulty can be appreciated by considering that the

  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

  Permutations are bijective functions from atoms to atoms that are 

  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>"}

  \noindent 

  with a generic type in which @{text "\<alpha>"} stands for the type of atoms 

  and @{text "\<beta>"} for the type of the objects on which the permutation 

  acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"},

  the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}} 

  and the inverse permutation @{term p} as @{text "- p"}. The permutation

  operation is defined for products, lists, sets, functions, booleans etc 

  (see \cite{HuffmanUrban10}).

  The most original aspect of the nominal logic work of Pitts et al is a general

  definition for ``the set of free variables of an object @{text "x"}''.  This

  definition is general in the sense that it applies not only to lambda-terms,

  but also to lists, products, sets and even functions. The definition depends

  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]}

  \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]}

  \noindent

  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. 

  @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}

  @{thm[mode=IfThen] at_set_avoiding[no_vars]}

*}

section {* Abstractions *}

section {* Alpha-Equivalence and Free Variables *}

section {* Examples *}

section {* Conclusion *}

text {*

  \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 

*}

(*<*)

end

(*>*)