|
1 (*<*) |
|
2 theory Slides2 |
|
3 imports "LaTeXsugar" "Nominal" |
|
4 begin |
|
5 |
|
6 notation (latex output) |
|
7 set ("_") and |
|
8 Cons ("_::/_" [66,65] 65) |
|
9 |
|
10 (*>*) |
|
11 |
|
12 |
|
13 text_raw {* |
|
14 \renewcommand{\slidecaption}{TU Munich, 28.~May 2010} |
|
15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
16 \mode<presentation>{ |
|
17 \begin{frame}<1>[t] |
|
18 \frametitle{% |
|
19 \begin{tabular}{@ {\hspace{-3mm}}c@ {}} |
|
20 \\ |
|
21 \huge Nominal 2\\[-2mm] |
|
22 \large Or, How to Reason Conveniently with\\[-5mm] |
|
23 \large General Bindings in Isabelle\\[15mm] |
|
24 \end{tabular}} |
|
25 \begin{center} |
|
26 joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] |
|
27 \end{center} |
|
28 \end{frame}} |
|
29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
30 |
|
31 *} |
|
32 |
|
33 text_raw {* |
|
34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
35 \mode<presentation>{ |
|
36 \begin{frame}<1-2> |
|
37 \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}} |
|
38 \mbox{}\\[-3mm] |
|
39 |
|
40 \begin{itemize} |
|
41 \item sorted atoms and sort-respecting permutations\medskip |
|
42 |
|
43 \onslide<2->{ |
|
44 \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip |
|
45 |
|
46 \begin{center} |
|
47 \begin{tabular}{c@ {\hspace{7mm}}c} |
|
48 $[]\;\act\;c \dn c$ & |
|
49 $(a\;b)\!::\!\pi\;\act\;c \dn$ |
|
50 $\begin{cases} |
|
51 b & \text{if}\; \pi \act c = a\\ |
|
52 a & \text{if}\; \pi \act c = b\\ |
|
53 \pi \act c & \text{otherwise} |
|
54 \end{cases}$ |
|
55 \end{tabular} |
|
56 \end{center}} |
|
57 \end{itemize} |
|
58 |
|
59 \end{frame}} |
|
60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
61 *} |
|
62 |
|
63 text_raw {* |
|
64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
65 \mode<presentation>{ |
|
66 \begin{frame}<1> |
|
67 \frametitle{\begin{tabular}{c}Problems\end{tabular}} |
|
68 \mbox{}\\[-3mm] |
|
69 |
|
70 \begin{itemize} |
|
71 \item @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip |
|
72 |
|
73 \item @{text "supp _ :: \<beta> \<Rightarrow> \<alpha> set"} |
|
74 |
|
75 \begin{center} |
|
76 $\text{finite} (\text{supp}\;x)_{\,\alpha_1\,\text{set}}$ \ldots |
|
77 $\text{finite} (\text{supp}\;x)_{\,\alpha_n\,\text{set}}$ |
|
78 \end{center}\bigskip |
|
79 |
|
80 \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip |
|
81 |
|
82 \item type-classes |
|
83 \end{itemize} |
|
84 |
|
85 \end{frame}} |
|
86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
87 *} |
|
88 |
|
89 text_raw {* |
|
90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
91 \mode<presentation>{ |
|
92 \begin{frame}<1-4> |
|
93 \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}} |
|
94 \mbox{}\\[-3mm] |
|
95 *} |
|
96 datatype atom = Atom string nat |
|
97 |
|
98 text_raw {* |
|
99 \mbox{}\bigskip |
|
100 \begin{itemize} |
|
101 \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"} |
|
102 |
|
103 \begin{itemize} |
|
104 \item sort-respecting \hspace{5mm}($\forall a.\;\text{sort}(f a) = \text{sort}(a)$) |
|
105 \item finite domain \hspace{5mm}($\text{finite} \{a.\;f a \not= a\}$) |
|
106 \end{itemize}\medskip |
|
107 |
|
108 \item<3-> swappings: |
|
109 \small |
|
110 \[ |
|
111 \begin{array}{l@ {\hspace{1mm}}l} |
|
112 (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\ |
|
113 & \text{then}\;\lambda c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\; |
|
114 \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\ |
|
115 & \text{else}\;\only<3>{\mbox{\textcolor{red}{\bf ?}}}\only<4->{\text{id}} |
|
116 \end{array} |
|
117 \] |
|
118 \end{itemize} |
|
119 |
|
120 \end{frame}} |
|
121 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
122 *} |
|
123 |
|
124 text_raw {* |
|
125 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
126 \mode<presentation>{ |
|
127 \begin{frame}<1-6> |
|
128 \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}} |
|
129 \mbox{}\\[-3mm] |
|
130 |
|
131 \begin{itemize} |
|
132 \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip |
|
133 |
|
134 \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip |
|
135 |
|
136 \item<5-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip |
|
137 |
|
138 \begin{itemize} |
|
139 \item $0\;\act\;x = x$\\ |
|
140 \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$ |
|
141 \end{itemize} |
|
142 |
|
143 \small |
|
144 \onslide<6->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$} |
|
145 \end{itemize} |
|
146 |
|
147 \only<4>{ |
|
148 \begin{textblock}{6}(2.5,11) |
|
149 \begin{tikzpicture} |
|
150 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
151 {\normalsize\color{darkgray} |
|
152 \begin{minipage}{8cm}\raggedright |
|
153 This is slightly odd, since in general: |
|
154 \begin{center}$\pi_1 + \pi_2 \alert{\not=} \pi_2 + \pi_1$\end{center} |
|
155 \end{minipage}}; |
|
156 \end{tikzpicture} |
|
157 \end{textblock}} |
|
158 |
|
159 \end{frame}} |
|
160 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
161 *} |
|
162 |
|
163 text_raw {* |
|
164 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
165 \mode<presentation>{ |
|
166 \begin{frame}<1-3> |
|
167 \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}} |
|
168 \mbox{}\\[-3mm] |
|
169 |
|
170 \begin{itemize} |
|
171 \item \underline{concrete} atoms: |
|
172 \end{itemize} |
|
173 *} |
|
174 (*<*) |
|
175 consts sort :: "atom \<Rightarrow> string" |
|
176 (*>*) |
|
177 |
|
178 typedef name = "{a :: atom. sort a = ''name''}" (*<*)sorry(*>*) |
|
179 typedef ident = "{a :: atom. sort a = ''ident''}" (*<*)sorry(*>*) |
|
180 |
|
181 text_raw {* |
|
182 \mbox{}\bigskip\bigskip |
|
183 \begin{itemize} |
|
184 \item<2-> there is an overloaded function \underline{atom}, which injects concrete |
|
185 atoms into generic ones\medskip |
|
186 \begin{center} |
|
187 \begin{tabular}{l} |
|
188 $\text{atom}(a) \fresh x$\\ |
|
189 $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$ |
|
190 \end{tabular} |
|
191 \end{center}\bigskip\medskip |
|
192 |
|
193 \onslide<3-> |
|
194 {I would like to have $a \fresh x$, $(a\; b)$, \ldots} |
|
195 |
|
196 \end{itemize} |
|
197 |
|
198 \end{frame}} |
|
199 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
200 *} |
|
201 |
|
202 text_raw {* |
|
203 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
204 \mode<presentation>{ |
|
205 \begin{frame}<1-2>[c] |
|
206 \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}} |
|
207 \mbox{}\\[-3mm] |
|
208 |
|
209 \begin{itemize} |
|
210 \item the formalised version of the nominal theory is now much nicer to |
|
211 work with (sorts are occasionally explicit)\bigskip |
|
212 |
|
213 \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip |
|
214 |
|
215 \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity} |
|
216 \end{itemize} |
|
217 |
|
218 |
|
219 \end{frame}} |
|
220 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
221 *} |
|
222 |
|
223 (*<*) |
|
224 end |
|
225 (*>*) |