(*<*)

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

(*>*)