2748
|
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 |
(*>*)
|