(*<*)+ −
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+ −
(*>*)+ −