(*<*)theory Appendiximports "../Nominal/Nominal2" "~~/src/HOL/Library/LaTeXsugar"beginconsts fv :: "'a \<Rightarrow> 'b" abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool" abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c" Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" definition "equal \<equiv> (op =)" notation (latex output) swap ("'(_ _')" [1000, 1000] 1000) and fresh ("_ # _" [51, 51] 50) and fresh_star ("_ #\<^sup>* _" [51, 51] 50) and supp ("supp _" [78] 73) and uminus ("-_" [78] 73) and If ("if _ then _ else _" 10) and alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and fv ("fa'(_')" [100] 100) and equal ("=") and alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and Abs_lst ("[_]\<^bsub>list\<^esub>._") and Abs_dist ("[_]\<^bsub>#list\<^esub>._") and Abs_res ("[_]\<^bsub>res\<^esub>._") and Abs_print ("_\<^bsub>set\<^esub>._") and Cons ("_::_" [78,77] 73) and supp_set ("aux _" [1000] 10) and alpha_bn ("_ \<approx>bn _")consts alpha_trm ::'aconsts fa_trm :: 'aconsts alpha_trm2 ::'aconsts fa_trm2 :: 'aconsts ast :: 'aconsts ast' :: 'anotation (latex output) alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and fa_trm ("fa\<^bsub>trm\<^esub>") and alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and ast ("'(as, t')") and ast' ("'(as', t\<PRIME> ')")(*>*)text {*\appendix\section*{Appendix} Details for one case in Theorem \ref{suppabs}, which the reader might like to ignore. By definition of the abstraction type @{text "abs_set"} we have % \begin{equation}\label{abseqiff} @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; @{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \end{equation} \noindent and also \begin{equation}\label{absperm} @{thm permute_Abs(1)[no_vars]}% \end{equation} \noindent The second fact derives from the definition of permutations acting on pairs and $\alpha$-equivalence being equivariant. With these two facts at our disposal, we can show the following lemma about swapping two atoms in an abstraction. \begin{lemma} @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]} \end{lemma} \begin{proof} This lemma is straightforward using \eqref{abseqiff} and observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}. Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}). \end{proof} \noindent Assuming that @{text "x"} has finite support, this lemma together with \eqref{absperm} allows us to show \begin{equation}\label{halfone} @{thm Abs_supports(1)[no_vars]} \end{equation} \noindent which gives us ``one half'' of Theorem~\ref{suppabs} (the notion of supports is defined in \cite{HuffmanUrban10}). The ``other half'' is a bit more involved. To establish it, we use a trick from \cite{Pitts04} and first define an auxiliary function @{text aux}, taking an abstraction as argument: @{thm supp_set.simps[THEN eq_reflection, no_vars]}. We can show that @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. This in turn means \begin{center} @{text "supp (aux ([as]\<^bsub>set\<^esub>. x)) \<subseteq> supp ([as]\<^bsub>set\<^esub> x)"} \end{center} \noindent Assuming @{term "supp x - as"} is a finite set, we further obtain \begin{equation}\label{halftwo} @{thm (concl) Abs_supp_subset1(1)[no_vars]} \end{equation} \noindent since for finite sets of atoms, @{text "bs"}, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes Theorem~\ref{suppabs}. *}(*<*)end(*>*)