diff -r a5da7b6aff8f -r 6f38e357b337 ESOP-Paper/Appendix.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ESOP-Paper/Appendix.thy	Tue Mar 29 23:52:14 2011 +0200
@@ -0,0 +1,135 @@
+(*<*)
+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
+(*>*)