781 |
781 |
782 \begin{thm}[Support of Abstractions]\label{suppabs} |
782 \begin{thm}[Support of Abstractions]\label{suppabs} |
783 Assuming @{text x} has finite support, then\\[-6mm] |
783 Assuming @{text x} has finite support, then\\[-6mm] |
784 \begin{center} |
784 \begin{center} |
785 \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
785 \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
786 @{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\ |
786 @{thm (lhs) supp_Abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(1)[no_vars]}\\ |
787 @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\ |
787 @{thm (lhs) supp_Abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(2)[no_vars]}\\ |
788 @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]} |
788 @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]} |
789 \end{tabular} |
789 \end{tabular} |
790 \end{center} |
790 \end{center} |
791 \end{thm} |
791 \end{thm} |
792 |
792 |
793 \noindent |
793 \noindent |
794 Below we will show the first equation. The others |
794 Below we will show the first equation. The others |
795 follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
795 follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
796 we have |
796 we have |
797 % |
797 % |
798 \begin{equation}\label{abseqiff} |
798 \begin{equation}\label{abseqiff} |
799 @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; |
799 @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; |
800 @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} |
800 @{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} |
801 \end{equation} |
801 \end{equation} |
802 |
802 |
803 \noindent |
803 \noindent |
804 and also |
804 and also |
805 % |
805 % |
812 \eqref{permute} and $\alpha$-equivalence being equivariant |
812 \eqref{permute} and $\alpha$-equivalence being equivariant |
813 (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show |
813 (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show |
814 the following lemma about swapping two atoms in an abstraction. |
814 the following lemma about swapping two atoms in an abstraction. |
815 |
815 |
816 \begin{lemma} |
816 \begin{lemma} |
817 @{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]} |
817 @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]} |
818 \end{lemma} |
818 \end{lemma} |
819 |
819 |
820 \begin{proof} |
820 \begin{proof} |
821 This lemma is straightforward using \eqref{abseqiff} and observing that |
821 This lemma is straightforward using \eqref{abseqiff} and observing that |
822 the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}. |
822 the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}. |
826 \noindent |
826 \noindent |
827 Assuming that @{text "x"} has finite support, this lemma together |
827 Assuming that @{text "x"} has finite support, this lemma together |
828 with \eqref{absperm} allows us to show |
828 with \eqref{absperm} allows us to show |
829 % |
829 % |
830 \begin{equation}\label{halfone} |
830 \begin{equation}\label{halfone} |
831 @{thm abs_supports(1)[no_vars]} |
831 @{thm Abs_supports(1)[no_vars]} |
832 \end{equation} |
832 \end{equation} |
833 |
833 |
834 \noindent |
834 \noindent |
835 which by Property~\ref{supportsprop} gives us ``one half'' of |
835 which by Property~\ref{supportsprop} gives us ``one half'' of |
836 Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish |
836 Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish |
854 \noindent |
854 \noindent |
855 using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set, |
855 using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set, |
856 we further obtain |
856 we further obtain |
857 % |
857 % |
858 \begin{equation}\label{halftwo} |
858 \begin{equation}\label{halftwo} |
859 @{thm (concl) supp_abs_subset1(1)[no_vars]} |
859 @{thm (concl) Abs_supp_subset1(1)[no_vars]} |
860 \end{equation} |
860 \end{equation} |
861 |
861 |
862 \noindent |
862 \noindent |
863 since for finite sets of atoms, @{text "bs"}, we have |
863 since for finite sets of atoms, @{text "bs"}, we have |
864 @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. |
864 @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. |