522   A striking consequence of these definitions is that we can prove

   522   A striking consequence of these definitions is that we can prove

   523   without knowing anything about the structure of @{term x} that

   523   without knowing anything about the structure of @{term x} that

   524   swapping two fresh atoms, say @{text a} and @{text b}, leaves 

   524   swapping two fresh atoms, say @{text a} and @{text b}, leaves 

   525   @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}

   525   @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}

   526   then @{term "(a \<rightleftharpoons> b) \<bullet> x"}.

   526   then @{term "(a \<rightleftharpoons> b) \<bullet> x"}.

   528   %\begin{myproperty}\label{swapfreshfresh}

   528   %\begin{myproperty}\label{swapfreshfresh}

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

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

   530   %\end{myproperty}

   530   %\end{myproperty}

   532   %While often the support of an object can be relatively easily 

   532   %While often the support of an object can be relatively easily 

   533   %described, for example for atoms, products, lists, function applications, 

   533   %described, for example for atoms, products, lists, function applications, 

   534   %booleans and permutations as follows

   534   %booleans and permutations as follows

   535   %%

   535   %%

   536   %\begin{center}

   536   %\begin{center}

   551   %\end{center}

   551   %\end{center}

   552   %

   552   %

   553   %\noindent 

   553   %\noindent 

   554   %in some cases it can be difficult to characterise the support precisely, and

   554   %in some cases it can be difficult to characterise the support precisely, and

   555   %only an approximation can be established (as for functions above). 

   555   %only an approximation can be established (as for functions above). 

   557   %Reasoning about

   557   %Reasoning about

   558   %such approximations can be simplified with the notion \emph{supports}, defined 

   558   %such approximations can be simplified with the notion \emph{supports}, defined 

   559   %as follows:

   559   %as follows:

   560   %

   560   %

   561   %\begin{definition}

   561   %\begin{definition}

   601   %\end{center}

   601   %\end{center}

   602   %

   602   %

   603   %Using freshness, the nominal logic work provides us with general means for renaming 

   603   %Using freshness, the nominal logic work provides us with general means for renaming 

   604   %binders. 

   604   %binders. 

   605   %

   605   %

   607   While in the older version of Nominal Isabelle, we used extensively 

   607   While in the older version of Nominal Isabelle, we used extensively 

   608   %Property~\ref{swapfreshfresh}

   608   %Property~\ref{swapfreshfresh}

   609   this property to rename single binders, it %%this property 

   609   this property to rename single binders, it %%this property 

   610   proved too unwieldy for dealing with multiple binders. For such binders the 

   610   proved too unwieldy for dealing with multiple binders. For such binders the 

   611   following generalisations turned out to be easier to use.

   611   following generalisations turned out to be easier to use.