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}
@{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}