1 |
|
2 \documentclass[11pt,a4paper,fleqn]{article} |
|
3 \usepackage{bbb,../pdfsetup} |
|
4 |
|
5 \makeatletter |
|
6 |
|
7 |
|
8 %%% layout |
|
9 |
|
10 \sloppy |
|
11 |
|
12 \parindent 0pt |
|
13 \parskip 0.5ex |
|
14 |
|
15 |
|
16 %%% text mode |
|
17 |
|
18 \newcommand{\B}[1]{\textbf{#1}} |
|
19 \newcommand{\TT}[1]{\ifmmode\mbox{\texttt{#1}}\else\texttt{#1}\fi} |
|
20 \newcommand{\E}[1]{\emph{#1}} |
|
21 \renewcommand{\P}[1]{\textsc{#1}} |
|
22 |
|
23 |
|
24 \renewcommand{\labelenumi}{(\theenumi)} |
|
25 \newcommand{\dfn}[1]{{\bf #1}} |
|
26 |
|
27 \newcommand{\thy}[1]{\mbox{\sc #1}} |
|
28 %\newcommand{\thy}[1]{\mbox{\textsc{#1}}} |
|
29 \newcommand{\IHOL}{\thy{ihol}} |
|
30 \newcommand{\SIHOL}{\thy{sihol}} |
|
31 \newcommand{\HOL}{\thy{hol}} |
|
32 \newcommand{\HOLBB}{\thy{hol88}} |
|
33 \newcommand{\FOL}{\thy{fol}} |
|
34 \newcommand{\SET}{\thy{set}} |
|
35 \newcommand{\Pure}{\thy{Pure}} |
|
36 |
|
37 |
|
38 \newcommand{\secref}[1]{\S\ref{#1}} |
|
39 |
|
40 \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]} |
|
41 |
|
42 |
|
43 %from alltt.sty |
|
44 \def\docspecials{\do\ \do\$\do\&% |
|
45 \do\#\do\^\do\^^K\do\_\do\^^A\do\%\do\~} |
|
46 |
|
47 \newenvironment{asc}{\small\trivlist \item[]\if@minipage\else\vskip\parskip\fi |
|
48 \leftskip\@totalleftmargin\rightskip\z@ |
|
49 \parindent\z@\parfillskip\@flushglue\parskip\z@ |
|
50 \@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par} |
|
51 \obeylines \tt \catcode``=13 \@noligs \let\do\@makeother \docspecials |
|
52 \frenchspacing\@vobeyspaces}{\endtrivlist} |
|
53 |
|
54 \newenvironment{ascbox}{\vbox\bgroup\begin{asc}}{\end{asc}\egroup} |
|
55 \newcommand{\brk}{\end{ascbox}\vskip-20pt\begin{ascbox}} |
|
56 |
|
57 \newcommand{\out}[1]{{\fontfamily{cmtt}\fontseries{m}\fontshape{sl}\selectfont\ \ #1}} |
|
58 |
|
59 |
|
60 % warning environment |
|
61 \newcommand{\dbend}{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}} |
|
62 \newenvironment{warning}{\medskip\medbreak\begingroup \clubpenalty=10000 |
|
63 \noindent \hangindent1.5em \hangafter=-2 |
|
64 \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}% |
|
65 {\par\endgroup\medbreak} |
|
66 |
|
67 \newcommand{\Isa}{{\sc Isabelle}} |
|
68 \newcommand{\ML}{{\sc ml}} |
|
69 \newcommand{\Haskell}{{\rm Haskell}} |
|
70 |
|
71 \newcommand{\IMP}{"`$\Longrightarrow$"'} |
|
72 \newcommand{\PMI}{"`$\Longleftarrow$"'} |
|
73 |
|
74 |
|
75 |
|
76 %%% math mode |
|
77 |
|
78 %% generic defs |
|
79 |
|
80 \newcommand{\nquad}{\hskip-1em} |
|
81 |
|
82 \newcommand{\fct}[1]{\mathop{\rm #1}\nolimits} |
|
83 \newcommand{\idt}[1]{{\mathord{\it #1}}} |
|
84 \newcommand{\syn}[1]{{\mathord{\it #1}}} |
|
85 \newcommand{\text}[1]{\mbox{#1}} |
|
86 \newcommand{\rmtext}[1]{\mbox{\rm #1}} |
|
87 %\newcommand{\mtt}[1]{\mbox{\tt #1}} |
|
88 |
|
89 \newcommand{\falls}{\text{falls }} |
|
90 \newcommand{\sonst}{\text{sonst}} |
|
91 |
|
92 \newcommand{\Bool}{\bbbB} |
|
93 \newcommand{\Nat}{\bbbN} |
|
94 \newcommand{\Natz}{{\bbbN_0}} |
|
95 \newcommand{\Rat}{\bbbQ} |
|
96 \newcommand{\Real}{\bbbR} |
|
97 |
|
98 \newcommand{\dt}{{\mathpunct.}} |
|
99 |
|
100 \newcommand{\Gam}{\Gamma} |
|
101 \renewcommand{\epsilon}{\varepsilon} |
|
102 \renewcommand{\phi}{\varphi} |
|
103 \renewcommand{\rho}{\varrho} |
|
104 \newcommand{\eset}{{\{\}}} |
|
105 \newcommand{\etuple}{{\langle\rangle}} |
|
106 |
|
107 \newcommand{\dfneq}{\mathbin{\mathord:\mathord=}} |
|
108 \newcommand{\impl}{\Longrightarrow} |
|
109 \renewcommand{\iff}{{\;\;\mathord{\Longleftrightarrow}\;\;}} |
|
110 \newcommand{\dfniff}{{\;\;\mathord:\mathord{\Longleftrightarrow}\;\;}} |
|
111 \renewcommand{\land}{\mathrel{\,\wedge\,}} |
|
112 \renewcommand{\lor}{\mathrel{\,\vee\,}} |
|
113 \newcommand{\iso}{\cong} |
|
114 |
|
115 \newcommand{\union}{\cup} |
|
116 \newcommand{\sunion}{\mathbin{\;\cup\;}} |
|
117 \newcommand{\dunion}{\mathbin{\dot\union}} |
|
118 \newcommand{\Union}{\bigcup} |
|
119 \newcommand{\inter}{\cap} |
|
120 \newcommand{\where}{\mathrel|} |
|
121 \newcommand{\pto}{\rightharpoonup} |
|
122 \newcommand{\comp}{\circ} |
|
123 \newcommand{\aaast}{{\mathord*\mathord*\mathord*}} |
|
124 |
|
125 \newcommand{\all}[1]{\forall #1\dt\;} |
|
126 \newcommand{\ex}[1]{\exists #1\dt\;} |
|
127 \newcommand{\lam}[1]{\mathop{\lambda} #1\dt} |
|
128 |
|
129 \newcommand\lbrakk{\mathopen{[\![}} |
|
130 \newcommand\rbrakk{\mathclose{]\!]}} |
|
131 |
|
132 \newcommand{\unif}{\mathrel{=^?}} |
|
133 \newcommand{\notunif}{\mathrel{{\not=}^?}} |
|
134 \newcommand{\incompat}{\mathrel{\#}} |
|
135 |
|
136 |
|
137 %% specific defs |
|
138 |
|
139 \newcommand{\PLUS}{\mathord{\langle{+}\rangle}} |
|
140 \newcommand{\TIMES}{\mathord{\langle{*}\rangle}} |
|
141 |
|
142 |
|
143 % IHOL |
|
144 |
|
145 \newcommand{\TV}{\fct{TV}} |
|
146 \newcommand{\FV}{\fct{FV}} |
|
147 \newcommand{\BV}{\fct{BV}} |
|
148 \newcommand{\VN}{\fct{VN}} |
|
149 \newcommand{\AT}{\fct{AT}} |
|
150 \newcommand{\STV}{\fct{STV}} |
|
151 |
|
152 \newcommand{\TyVars}{\syn{TyVars}} |
|
153 \newcommand{\TyNames}{\syn{TyNames}} |
|
154 \newcommand{\TyCons}{\syn{TyCons}} |
|
155 \newcommand{\TyConsSg}{\TyCons_\Sigma} |
|
156 \newcommand{\Types}{\syn{Types}} |
|
157 \newcommand{\TypesSg}{\Types_\Sigma} |
|
158 \newcommand{\GrTypes}{\syn{GrTypes}} |
|
159 \newcommand{\GrTypesSg}{\GrTypes_\Sigma} |
|
160 \newcommand{\VarNames}{\syn{VarNames}} |
|
161 \newcommand{\Vars}{\syn{Vars}} |
|
162 \newcommand{\VarsSg}{\Vars_\Sigma} |
|
163 \newcommand{\GrVars}{\syn{GrVars}} |
|
164 \newcommand{\GrVarsSg}{\GrVars_\Sigma} |
|
165 \newcommand{\ConstNames}{\syn{ConstNames}} |
|
166 \newcommand{\Consts}{\syn{Consts}} |
|
167 \newcommand{\ConstsSg}{\Consts_\Sigma} |
|
168 \newcommand{\GrConsts}{\syn{GrConsts}} |
|
169 \newcommand{\GrConstsSg}{\GrConsts_\Sigma} |
|
170 \newcommand{\Terms}{\syn{Terms}} |
|
171 \newcommand{\TermsSg}{\Terms_\Sigma} |
|
172 \newcommand{\GrTerms}{\syn{GrTerms}} |
|
173 \newcommand{\GrTermsSg}{\GrTerms_\Sigma} |
|
174 \newcommand{\Forms}{\syn{Forms}} |
|
175 \newcommand{\FormsTh}{\Forms_\Theta} |
|
176 \newcommand{\Seqs}{\syn{Seqs}} |
|
177 \newcommand{\SeqsTh}{\Seqs_\Theta} |
|
178 \newcommand{\Axms}{\syn{Axms}} |
|
179 \newcommand{\AxmsTh}{\Axms_\Theta} |
|
180 \newcommand{\Thms}{\syn{Thms}} |
|
181 \newcommand{\ThmsTh}{\Thms_\Theta} |
|
182 |
|
183 |
|
184 \newcommand{\U}{{\cal U}} |
|
185 \newcommand{\UU}{\bbbU} |
|
186 |
|
187 \newcommand{\ty}{{\mathbin{\,:\,}}} |
|
188 \newcommand{\typ}[1]{{\mathord{\sl #1}}} |
|
189 \newcommand{\tap}{\mathord{\,}} |
|
190 \newcommand{\prop}{\typ{prop}} |
|
191 \newcommand{\itself}{\typ{itself}} |
|
192 |
|
193 \newcommand{\cnst}[1]{{\mathord{\sl #1}}} |
|
194 \newcommand{\ap}{\mathbin{}} |
|
195 \newcommand{\To}{\Rightarrow} |
|
196 \newcommand{\Eq}{\equiv} |
|
197 \newcommand{\Impl}{\Rightarrow} |
|
198 \newcommand{\Forall}{\mathop{\textstyle\bigwedge}} |
|
199 \newcommand{\All}[1]{\Forall #1\dt} |
|
200 \newcommand{\True}{\top} |
|
201 \newcommand{\False}{\bot} |
|
202 \newcommand{\Univ}{{\top\!\!\!\!\top}} |
|
203 \newcommand{\Conj}{\wedge} |
|
204 \newcommand{\TYPE}{\cnst{TYPE}} |
|
205 |
|
206 |
|
207 % rules |
|
208 |
|
209 \newcommand{\Axm}{\rmtext{Axm}} |
|
210 \newcommand{\Assm}{\rmtext{Assm}} |
|
211 \newcommand{\Mon}{\rmtext{Mon}} |
|
212 \newcommand{\ImplI}{\mathord{\Impl}\rmtext{I}} |
|
213 \newcommand{\ImplE}{\mathord{\Impl}\rmtext{E}} |
|
214 \newcommand{\ImplMP}{\rmtext{MP}} |
|
215 \newcommand{\ImplRefl}{\mathord{\Impl}\rmtext{Refl}} |
|
216 \newcommand{\ImplTrans}{\mathord{\Impl}\rmtext{Trans}} |
|
217 \newcommand{\EqRefl}{\mathord{\Eq}\rmtext{Refl}} |
|
218 \newcommand{\EqTrans}{\mathord{\Eq}\rmtext{Trans}} |
|
219 \newcommand{\EqSym}{\mathord{\Eq}\rmtext{Sym}} |
|
220 \newcommand{\EqApp}{\mathord{\Eq}\rmtext{App}} |
|
221 \newcommand{\EqAbs}{\mathord{\Eq}\rmtext{Abs}} |
|
222 \newcommand{\Eqa}{\mathord{\Eq}\alpha} |
|
223 \newcommand{\Eqb}{\mathord{\Eq}\beta} |
|
224 \newcommand{\Eqe}{\mathord{\Eq}\eta} |
|
225 \newcommand{\Ext}{\rmtext{Ext}} |
|
226 \newcommand{\EqI}{\mathord{\Eq}\rmtext{I}} |
|
227 \newcommand{\EqMP}{\mathord{\Eq}\rmtext{MP}} |
|
228 \newcommand{\EqUnfold}{\mathord{\Eq}\rmtext{Unfold}} |
|
229 \newcommand{\EqFold}{\mathord{\Eq}\rmtext{Fold}} |
|
230 \newcommand{\AllI}{\mathord{\Forall}\rmtext{I}} |
|
231 \newcommand{\AllE}{\mathord{\Forall}\rmtext{E}} |
|
232 \newcommand{\TypInst}{\rmtext{TypInst}} |
|
233 \newcommand{\Inst}{\rmtext{Inst}} |
|
234 \newcommand{\TrueI}{\True\rmtext{I}} |
|
235 \newcommand{\FalseE}{\False\rmtext{E}} |
|
236 \newcommand{\UnivI}{\Univ\rmtext{I}} |
|
237 \newcommand{\ConjI}{\mathord{\Conj}\rmtext{I}} |
|
238 \newcommand{\ConjE}{\mathord{\Conj}\rmtext{E}} |
|
239 \newcommand{\ConjProj}{\mathord{\Conj}\rmtext{Proj}} |
|
240 \newcommand{\ImplCurry}{\mathord{\Impl}\rmtext{Curry}} |
|
241 \newcommand{\ImplUncurry}{\mathord{\Impl}\rmtext{Uncurry}} |
|
242 \newcommand{\CImplI}{\mathord{\Conj}\mathord{\Impl}\rmtext{I}} |
|
243 \newcommand{\CImplE}{\mathord{\Conj}\mathord{\Impl}\rmtext{E}} |
|
244 \newcommand{\Subclass}{\rmtext{Subclass}} |
|
245 \newcommand{\Subsort}{\rmtext{Subsort}} |
|
246 \newcommand{\VarSort}{\rmtext{VarSort}} |
|
247 \newcommand{\Arity}{\rmtext{Arity}} |
|
248 \newcommand{\SortMP}{\rmtext{SortMP}} |
|
249 \newcommand{\TopSort}{\rmtext{TopSort}} |
|
250 \newcommand{\OfSort}{\rmtext{OfSort}} |
|
251 |
|
252 \newcommand{\infr}{{\mathrel/}} |
|
253 \newcommand{\einfr}{{}{\mathrel/}} |
|
254 |
|
255 \newcommand{\drv}{\mathrel{\vdash}} |
|
256 \newcommand{\Drv}[1]{\mathrel{\mathord{\drv}_{#1}}} |
|
257 \newcommand{\Gdrv}{\Gam\drv} |
|
258 \newcommand{\edrv}{\mathop{\drv}\nolimits} |
|
259 \newcommand{\Edrv}[1]{\mathop{\drv}\nolimits_{#1}} |
|
260 \newcommand{\notEdrv}[1]{\mathop{\not\drv}\nolimits_{#1}} |
|
261 |
|
262 \newcommand{\lsem}{\lbrakk} |
|
263 \newcommand{\rsem}{\rbrakk} |
|
264 \newcommand{\sem}[1]{{\lsem #1\rsem}} |
|
265 |
|
266 \newcommand{\vld}{\mathrel{\models}} |
|
267 \newcommand{\Vld}[1]{\mathrel{\mathord{\models}_#1}} |
|
268 \newcommand{\Evld}[1]{\mathop{\vld}\nolimits_{#1}} |
|
269 \newcommand{\notEvld}[1]{\mathop{\not\vld}\nolimits_{#1}} |
|
270 |
|
271 \newcommand{\EQ}{\fct{EQ}} |
|
272 \newcommand{\IMPL}{\fct{IMPL}} |
|
273 \newcommand{\ALL}{\fct{ALL}} |
|
274 |
|
275 \newcommand{\extcv}{\mathrel{\unlhd}} |
|
276 \newcommand{\weakth}{\preceq} |
|
277 \newcommand{\eqvth}{\approx} |
|
278 \newcommand{\extdcli}{\mathrel{<_{\rm dcl}^1}} |
|
279 \newcommand{\extdcl}{\mathrel{\le_{\rm dcl}}} |
|
280 \newcommand{\extdfni}{\mathrel{<_{\rm dfn}^1}} |
|
281 \newcommand{\extdfn}{\mathrel{\le_{\rm dfn}}} |
|
282 \newcommand{\extsdfn}{\mathrel{\le_{\rm sdfn}}} |
|
283 \newcommand{\extqdfn}{\mathrel{\le_{\rm qdfn}}} |
|
284 |
|
285 \newcommand{\lvarbl}{\langle} |
|
286 \newcommand{\rvarbl}{\rangle} |
|
287 \newcommand{\varbl}[1]{{\lvarbl #1\rvarbl}} |
|
288 \newcommand{\up}{{\scriptstyle\mathord\uparrow}} |
|
289 \newcommand{\down}{{\scriptstyle\mathord\downarrow}} |
|
290 \newcommand{\Down}{{\mathord\downarrow}} |
|
291 |
|
292 |
|
293 \newcommand{\Sle}{{\mathrel{\le_S}}} |
|
294 \newcommand{\Classes}{\syn{Classes}} |
|
295 \newcommand{\ClassNames}{\syn{ClassNames}} |
|
296 \newcommand{\Sorts}{\syn{Sorts}} |
|
297 \newcommand{\TyVarNames}{\syn{TyVarNames}} |
|
298 \newcommand{\STyVars}{\syn{STyVars}} |
|
299 \newcommand{\STyArities}{\syn{STyArities}} |
|
300 \newcommand{\STypes}{\syn{STypes}} |
|
301 \newcommand{\SVars}{\syn{SVars}} |
|
302 \newcommand{\SConsts}{\syn{SConsts}} |
|
303 \newcommand{\STerms}{\syn{STerms}} |
|
304 \newcommand{\SForms}{\syn{SForms}} |
|
305 \newcommand{\SAxms}{\syn{SAxms}} |
|
306 \newcommand{\T}{{\cal T}} |
|
307 |
|
308 \newcommand{\cls}[1]{{\mathord{\sl #1}}} |
|
309 \newcommand{\intsrt}{\sqcap} |
|
310 \newcommand{\Intsrt}{{\mathop\sqcap}} |
|
311 \newcommand{\subcls}{\preceq} |
|
312 \newcommand{\Subcls}[1]{\mathrel{\subcls_{#1}}} |
|
313 \newcommand{\subsrt}{\sqsubseteq} |
|
314 \newcommand{\Subsrt}[1]{\mathrel{\subsrt_{#1}}} |
|
315 \newcommand{\subsrtp}{\sqsubset} |
|
316 \newcommand{\eqvsrt}{\approx} |
|
317 \newcommand{\topsrt}{\top} |
|
318 \newcommand{\srt}{\ty} |
|
319 |
|
320 \newcommand{\sct}[1]{{\bf #1}} |
|
321 \newcommand{\CLASSES}{\sct{classes}} |
|
322 \newcommand{\CLASSREL}{\sct{classrel}} |
|
323 \newcommand{\TYPES}{\sct{types}} |
|
324 \newcommand{\ARITIES}{\sct{arities}} |
|
325 \newcommand{\CONSTS}{\sct{consts}} |
|
326 \newcommand{\AXIOMS}{\sct{axioms}} |
|
327 \newcommand{\DEFNS}{\sct{defns}} |
|
328 \newcommand{\AXCLASS}{\sct{axclass}} |
|
329 \newcommand{\INSTANCE}{\sct{instance}} |
|
330 |
|
331 \newcommand{\Srt}{{\mathbin{\,:\,}}} |
|
332 \newcommand{\insrt}[2]{{\mathopen{(\!|} #1 \Srt #2 \mathclose{|\!)}}} |
|
333 \newcommand{\ofsrt}[2]{{\mathopen{\langle\!|} #1 \Srt #2 \mathclose{|\!\rangle}}} |
|
334 |
|
335 \newcommand{\injV}{{\iota_V}} |
|
336 \newcommand{\inj}{\iota} |
|
337 \newcommand{\injC}{{\iota_C}} |
|
338 \newcommand{\I}{{\cal I}} |
|
339 \newcommand{\C}{{\cal C}} |
|
340 |
|
341 \newcommand{\Sdrv}{\mathrel{\vdash\!\!\!\vdash}} |
|
342 \newcommand{\SDrv}[1]{\mathrel{\mathord{\Sdrv}_{#1}}} |
|
343 \newcommand{\SGdrv}{\Gam\Sdrv} |
|
344 \newcommand{\Sedrv}{\mathop{\Sdrv}\nolimits} |
|
345 \newcommand{\SEdrv}[1]{\mathop{\Sdrv}\nolimits_{#1}} |
|
346 |
|
347 \newcommand{\SSubclass}{\rmtext{S-Subclass}} |
|
348 \newcommand{\SSubsort}{\rmtext{S-Subsort}} |
|
349 \newcommand{\SVarSort}{\rmtext{S-VarSort}} |
|
350 \newcommand{\SArity}{\rmtext{S-Arity}} |
|
351 \newcommand{\SSortMP}{\rmtext{S-SortMP}} |
|
352 \newcommand{\STopSort}{\rmtext{S-TopSort}} |
|
353 \newcommand{\SOfSort}{\rmtext{S-OfSort}} |
|
354 |
|
355 |
|
356 \makeatother |
|
357 |
|
358 |
|
359 %%% Local Variables: |
|
360 %%% mode: latex |
|
361 %%% TeX-master: t |
|
362 %%% End: |
|