1 (*<*)

     2 theory Appendix

     3 imports "../Nominal/Nominal2" "~~/src/HOL/Library/LaTeXsugar"

     4 begin

     5 

     6 consts

     7   fv :: "'a \<Rightarrow> 'b"

     8   abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"

     9   alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    10   abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"

    11   Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 

    12   Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 

    13 

    14 definition

    15  "equal \<equiv> (op =)" 

    16 

    17 notation (latex output)

    18   swap ("'(_ _')" [1000, 1000] 1000) and

    19   fresh ("_ # _" [51, 51] 50) and

    20   fresh_star ("_ #\<^sup>* _" [51, 51] 50) and

    21   supp ("supp _" [78] 73) and

    22   uminus ("-_" [78] 73) and

    23   If  ("if _ then _ else _" 10) and

    24   alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and

    25   alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and

    26   alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and

    27   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and

    28   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and

    29   fv ("fa'(_')" [100] 100) and

    30   equal ("=") and

    31   alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 

    32   Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and

    33   Abs_lst ("[_]\<^bsub>list\<^esub>._") and

    34   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and

    35   Abs_res ("[_]\<^bsub>res\<^esub>._") and

    36   Abs_print ("_\<^bsub>set\<^esub>._") and

    37   Cons ("_::_" [78,77] 73) and

    38   supp_set ("aux _" [1000] 10) and

    39   alpha_bn ("_ \<approx>bn _")

    40 

    41 consts alpha_trm ::'a

    42 consts fa_trm :: 'a

    43 consts alpha_trm2 ::'a

    44 consts fa_trm2 :: 'a

    45 consts ast :: 'a

    46 consts ast' :: 'a

    47 notation (latex output) 

    48   alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and

    49   fa_trm ("fa\<^bsub>trm\<^esub>") and

    50   alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and

    51   fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and

    52   ast ("'(as, t')") and

    53   ast' ("'(as', t\<PRIME> ')")

    54 

    55 (*>*)

    56 

    57 text {*

    58 \appendix

    59 \section*{Appendix}

    60 

    61   Details for one case in Theorem \ref{suppabs}, which the reader might like to ignore. 

    62   By definition of the abstraction type @{text "abs_set"} 

    63   we have 

    64   %

    65   \begin{equation}\label{abseqiff}

    66   @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 

    67   @{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}

    68   \end{equation}

    69   

    70   \noindent

    71   and also

    72   

    73   \begin{equation}\label{absperm}

    74   @{thm permute_Abs(1)[no_vars]}%

    75   \end{equation}

    76 

    77   \noindent

    78   The second fact derives from the definition of permutations acting on pairs 

    79   and $\alpha$-equivalence being equivariant. With these two facts at our disposal, we can show 

    80   the following lemma about swapping two atoms in an abstraction.

    81   

    82   \begin{lemma}

    83   @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}

    84   \end{lemma}

    85   

    86   \begin{proof}

    87   This lemma is straightforward using \eqref{abseqiff} and observing that

    88   the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.

    89   Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).

    90   \end{proof}

    91   

    92   \noindent

    93   Assuming that @{text "x"} has finite support, this lemma together 

    94   with \eqref{absperm} allows us to show

    95   

    96   \begin{equation}\label{halfone}

    97   @{thm Abs_supports(1)[no_vars]}

    98   \end{equation}

    99   

   100   \noindent

   101   which gives us ``one half'' of

   102   Theorem~\ref{suppabs} (the notion of supports is defined in \cite{HuffmanUrban10}). 

   103   The ``other half'' is a bit more involved. To establish 

   104   it, we use a trick from \cite{Pitts04} and first define an auxiliary 

   105   function @{text aux}, taking an abstraction as argument:

   106   @{thm supp_set.simps[THEN eq_reflection, no_vars]}.

   107   

   108   We can show that 

   109   @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = (supp (p \<bullet> x)) - (p \<bullet> as)"}) 

   110   and therefore has empty support. 

   111   This in turn means

   112   

   113   \begin{center}

   114   @{text "supp (aux ([as]\<^bsub>set\<^esub>. x)) \<subseteq> supp ([as]\<^bsub>set\<^esub> x)"}

   115   \end{center}

   116   

   117   \noindent

   118   Assuming @{term "supp x - as"} is a finite set,

   119   we further obtain

   120   

   121   \begin{equation}\label{halftwo}

   122   @{thm (concl) Abs_supp_subset1(1)[no_vars]}

   123   \end{equation}

   124   

   125   \noindent

   126   since for finite sets of atoms, @{text "bs"}, we have 

   127   @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.

   128   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 

   129   Theorem~\ref{suppabs}. 

   130 

   131 *}

   132 

   133 (*<*)

   134 end

   135 (*>*)