summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 21 Jun 2013 16:20:47 +0200 | |

changeset 52404 | 33524382335b |

parent 52403 | 140ae824ea4a |

child 52405 | 3dd63180cdbf |

more set theory

--- a/src/Doc/ProgProve/Logic.thy Fri Jun 21 12:41:08 2013 +0200 +++ b/src/Doc/ProgProve/Logic.thy Fri Jun 21 16:20:47 2013 +0200 @@ -41,7 +41,9 @@ Quantifiers need to be enclosed in parentheses if they are nested within other constructs (just like @{text "if"}, @{text case} and @{text let}). \end{warn} -The most frequent logical symbols have the following ASCII representations: +The most frequent logical symbols and their ASCII representations are shown +in Fig.~\ref{fig:log-symbols}. +\begin{figure} \begin{center} \begin{tabular}{l@ {\qquad}l@ {\qquad}l} @{text "\<forall>"} & \xsymbol{forall} & \texttt{ALL}\\ @@ -55,9 +57,16 @@ @{text "\<noteq>"} & \xsymbol{noteq} & \texttt{\char`~=} \end{tabular} \end{center} -The first column shows the symbols, the second column ASCII representations -that Isabelle interfaces convert into the corresponding symbol, -and the third column shows ASCII representations that stay fixed. +\caption{Logical symbols and their ASCII forms} +\label{fig:log-symbols} +\end{figure} +The first column shows the symbols, the other columns ASCII representations. +The \texttt{\char`\\}\texttt{<...>} form is always converted into the symbolic form +by the Isabelle interfaces, the treatment of the other ASCII forms +depends on the interface. The ASCII forms \texttt{/\char`\\} and +\texttt{\char`\\/} +are special in that they are merely keyboard shortcuts for the interface and +not logical symbols by themselves. \begin{warn} The implication @{text"\<Longrightarrow>"} is part of the Isabelle framework. It structures theorems and proof states, separating assumptions from conclusions. @@ -105,9 +114,23 @@ Sets also allow bounded quantifications @{prop"ALL x : A. P"} and @{prop"EX x : A. P"}. -Some more frequently useful functions on sets: +For the more ambitious, there are also @{text"\<Union>"} and @{text"\<Inter>"}: +\begin{center} +@{thm Union_eq} \qquad @{thm Inter_eq} +\end{center} +The ASCII forms of @{text"\<Union>"} are \texttt{\char`\\\char`\<Union>} and \texttt{Union}, +those of @{text"\<Inter>"} are \texttt{\char`\\\char`\<Inter>} and \texttt{Inter}. +There are also indexed unions and intersections: \begin{center} -\begin{tabular}{ll} +@{thm UNION_eq} \\ @{thm INTER_eq} +\end{center} +The ASCII forms are \ \texttt{UN x:A.~B} \ and \ \texttt{INT x:A. B} \ +where \texttt{x} may occur in \texttt{B}. +If \texttt{A} is \texttt{UNIV} you can just write \ \texttt{UN x.~B} \ and \ \texttt{INT x. B}. + +Some other frequently useful functions on sets are the following: +\begin{center} +\begin{tabular}{l@ {\quad}l} @{const_typ set} & converts a list to the set of its elements\\ @{const_typ finite} & is true iff its argument is finite\\ @{const_typ card} & is the cardinality of a finite set\\ @@ -115,7 +138,6 @@ @{thm image_def} & is the image of a function over a set \end{tabular} \end{center} - See \cite{Nipkow-Main} for the wealth of further predefined functions in theory @{theory Main}.