(*<*)
theory Appendix
imports "../Nominal/Nominal2" "~~/src/HOL/Library/LaTeXsugar"
begin

consts
  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 ::'a
consts fa_trm :: 'a
consts alpha_trm2 ::'a
consts fa_trm2 :: 'a
consts ast :: 'a
consts ast' :: 'a
notation (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
(*>*)