diff -r fb201e383f1b -r da575186d492 ESOP-Paper/Appendix.thy
--- a/ESOP-Paper/Appendix.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-(*<*)
-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
-(*>*)