Beweren en bewijzen/de zuilen/Taal/3. Syntax en semantiek/latex

%<source lang="tex">

\documentclass[a4paper,12pt]{article} \usepackage[english,dutch]{babel}

\usepackage{a4wide} \pagestyle{empty}

\newcommand{\forget}[1]{\addtolength{\textheight}{#1}\setlength{#1}{0pt}} \forget{\headheight} \forget{\headsep} \forget{\footskip}

\usepackage{amssymb, amsmath} \usepackage[dutch,english]{babel} \selectlanguage{dutch}

\renewcommand{\implies}{\rightarrow} \renewcommand{\impliedby}{\leftarrow} \renewcommand{\iff}{\leftrightarrow}

\newcommand{\vb}[1]{\fbox{\scriptsize $#1$}} \newcommand{\tp}[1]{$^{\,#1}$} \newcommand{\ra}{\rightarrow} \newcommand{\alt}{|} \newcommand{\Alt}Sjabloon:\bf\ \ \ $ \newcommand{\nat}{{\mathbb{N}}} \newcommand{\zed}{{\mathbb{Z}}} \newcommand{\bew}{{\mathbb{B}}} \newcommand{\real}{{\mathbb{R}}} \newcommand{\lit}[1]{\textup{\textsf{#1}}}

\begin{document}

\subsection*{Grammatica \tiny{(versie 30/06/14)}} Legenda: De letters $\sigma$ en $\tau$ worden gebruikt om willekeurige types aan te geven. De letter $\rho$ wordt specifiek gebruikt om $\zed$ of $\real$ aan te geven. \\ \textsf{\textit{formule}}\tp{\bew\alt\tau} genereert formules van type $\bew$, en via een tweede alternatief (meer) formules van type $\tau$.\\ \begin{sffamily} \begin{itshape} \begin{tabular}{ll} sectie & naamgeving sectie \Alt naamgeving \\ naamgeving & \lit{Variable} naam\tp{\tau} \lit{:} type\tp{\tau} \lit{.} \hfill \textrm{een punt ter afsluiting}\\ & \Alt \lit{Definition} naam\tp{\tau} abstractie\tp{\tau} \lit{.} \\ & \Alt \lit{Theorem} naam\tp{\bew} \lit{:} formule\tp{\bew} \lit{.} \\ &\qquad \vb{\mathsf{Variable}\;\mathit{neerslag}: R.} \\ &\qquad \vb{\mathsf{Variable}\;\mathit{Mens}: \mathsf{Set}.} \hfill \textrm{maakt een nieuw type `Mens'} \\ &\qquad \vb{\mathsf{Variable}\;\mathit{BSN}: \mathit{Mens}\ra\mathit{Z}.} \\ &\qquad \vb{\mathsf{Definition}\;P\;(m:Z)\;:= \neg(\exists p:Z, 1<p \land p<m \land (\exists q:Z, m=p\times q)).} \smallskip\\ abstractie\tp{\tau\alt\sigma\ra\tau} & \lit{:=} formule\tp{\tau} \Alt parameter\tp{\sigma} abstractie\tp{\tau}\\ parameter\tp{\tau} & \lit{(} naam\tp{\tau} \lit{:} type\tp{\tau} \lit{)} \smallskip\\ \hline formule\tp{\bew\alt\tau} & kwantor naam\tp{\sigma} \lit{:} type\tp{\sigma} \lit{,} formule\tp{\bew} \Alt equivalentie\tp{\tau} \rule{0pt}{\bigskipamount}\\ &\qquad \vb{\forall m:Z, P\;m \implies (\exists n:Z, P\;n \land m<n)} \smallskip\\ & \hfill \textrm{een komma in plaats van de gebruikelijke punt}\\ equivalentie\tp{\bew\alt\tau} & equivalentie\tp{\bew} $\iff$ implicatie\tp{\bew} \Alt implicatie\tp{\tau} \\ &\qquad \vb{x \land y \iff \neg x \land \neg y} \smallskip\\ implicatie\tp{\bew\alt\tau} & disjunctie\tp{\bew} $\implies$ implicatie\tp{\bew} \Alt disjunctie\tp{\tau} \\ &\qquad \vb{a \implies b \implies a} \\ disjunctie\tp{\bew\alt\tau} & conjunctie\tp{\bew} $\lor$ disjunctie\tp{\bew} \Alt conjunctie\tp{\tau}\\ &\qquad \vb{p \land \neg q \lor \neg p \land q} \smallskip\\ conjunctie\tp{\bew\alt\tau} & negatie\tp{\bew} $\land$ conjunctie\tp{\bew} \Alt negatie\tp{\tau} \\ negatie\tp{\bew\alt\tau} & $\neg$ negatie\tp{\bew} \Alt vergelijking\tp{\tau} \\ &\qquad \vb{\neg(\forall n:Z, P\;n \implies P\;(n{+}2))} \smallskip\\ \hline vergelijking\tp{\bew\alt\tau} & som\tp{\tau} gelijkongelijk som\tp{\tau} \Alt som\tp{\rho} kleinergelijkgroter som\tp{\rho} \rule{0pt}{\bigskipamount} \\ & \Alt som\tp{\rho} $\in$ interval\tp{\mathcal{P}(\rho)} \Alt som\tp{\tau} \hfill \textrm{met $\rho\in\{\zed,\real\}$}\\ &\qquad \vb{a\times(x+2) + b\times x + c = 0} \smallskip\\ interval\tp{\mathcal{P}(\rho)} & \lit{[} som\tp{\rho} \lit{,} som\tp{\rho} \lit{]} \Alt \lit{[} som\tp{\rho} \lit{,} som\tp{\rho} \lit{)} \\ & \Alt \lit{(} som\tp{\rho} \lit{,} som\tp{\rho} \lit{]} \Alt \lit{(} som\tp{\rho} \lit{,} som\tp{\rho} \lit{)} \hfill \textrm{met $\rho\in\{\zed,\real\}$} \\ som\tp{\rho\alt\tau} & som\tp{\rho} plusminus product\tp{\rho} \Alt product\tp{\tau} \hfill \textrm{met $\rho\in\{\zed,\real\}$}\\ product\tp{\rho\alt\tau} & product\tp{\rho} maaldoor negatief\tp{\rho} \Alt negatief\tp{\tau} \qquad\hfill \textrm{met $\rho\in\{\zed,\real\}$}\\ &\qquad \vb{(p+q) \times (p-q)} \smallskip\\ negatief\tp{\rho\alt\tau} & $-$ negatief\tp{\rho} \Alt macht\tp{\tau} \hfill \textrm{met $\rho\in\{\zed,\real\}$} \\ &\qquad \vb{-5} \smallskip\\ macht\tp{\rho\alt\tau} & term\tp{\rho} \^{} macht\tp{\nat} \Alt term\tp{\tau} \hfill \textrm{met $\rho\in\{\zed,\real\}$}\\ &\qquad \vb{2 $\^{}$ 2 $\^{}$ k} \smallskip\\ \hline term\tp{\tau} & term\tp{\sigma\ra\tau} waarde\tp{\sigma} \Alt waarde\tp{\tau} \rule{0pt}{\bigskipamount}\\ &\qquad \vb{\mathit{max}\;3\;m} \vb{\mathit{Verkeerslicht\;linksaf\; groen}\;(\mathit{nu}{+}5)} \smallskip\\ waarde\tp{\rho\alt\tau} & constante\tp{\rho} \Alt naam\tp{\tau} \Alt \lit{(} formule\tp{\tau} \lit{)} \\ \end{tabular}

\begin{tabular}{ll} type\tp{\sigma\ra\tau \alt \tau} & basistype\tp{\sigma} $\ra$ type\tp{\tau} \Alt basistype\tp{\tau} \\ &\qquad \vb{Z\ra(Z\ra Z)\ra B} \smallskip\\ basistype\tp{\bew\alt\zed\alt\real\alt\text{naam}\alt\tau} & \lit{B} \Alt \lit{Z} \Alt \lit{R} \Alt naam\tp{\mathsf{Set}} \Alt \lit{(} type\tp{\tau} \lit{)} \smallskip\\ &\qquad \vb{\mathit{Mens}} \vb{(\mathit{Mens} \ra Z)} \smallskip\\ %& \hfill \textrm{`naam' is dus een zelf gemaakt type}\\ \hline constante\tp{\rho} & $0\ldots9$ \Alt constante\tp{\rho} $0\ldots9$ \quad \hfill \textrm{met $\rho\in\{\zed,\real\}$}\rule{0pt}{\bigskipamount}\\ naam\tp{\tau} & eersteteken \Alt eersteteken etcetera\\ &\qquad \vb{\mathit{melk2S\_L\_A\_G\_R\_O\_O\_M}} \\ etcetera & overigteken \Alt overigteken etcetera\\

eersteteken & $a\ldots z$ \Alt $A\ldots Z$ \Alt $\_$\\ overigteken & $a\ldots z$ \Alt $A\ldots Z$ \Alt $0\ldots 9$ \Alt $\_$ \Alt $'$\\

kwantor & $\forall$ \Alt $\exists$ \\ gelijkongelijk & $=$ \Alt $\neq$ \\ kleinergelijkgroter & $<$ \Alt $\leq$ \Alt $>$ \Alt $\geq$ \\ plusminus & $+$ \Alt $-$ \\ maaldoor & $\times$ \Alt $/$ \\ \end{tabular}

\end{itshape} \end{sffamily}

\end{document} %</source>