src/Doc/ProgProve/Logic.thy
changeset 51784 89fb9f4abf84
parent 51436 790310525e97
child 52361 7d5ad23b8245
     1.1 --- a/src/Doc/ProgProve/Logic.thy	Fri Apr 26 07:49:38 2013 +0200
     1.2 +++ b/src/Doc/ProgProve/Logic.thy	Fri Apr 26 09:01:45 2013 +0200
     1.3 @@ -105,6 +105,20 @@
     1.4  Sets also allow bounded quantifications @{prop"ALL x : A. P"} and
     1.5  @{prop"EX x : A. P"}.
     1.6  
     1.7 +Some more frequently useful functions on sets:
     1.8 +\begin{center}
     1.9 +\begin{tabular}{ll}
    1.10 +@{const_typ set} & converts a list to the set of its elements\\
    1.11 +@{const_typ finite} & is true iff its argument is finite\\
    1.12 +@{const_typ card} & is the cardinality of a finite set\\
    1.13 + & and is @{text 0} for all infinite sets\\
    1.14 +@{thm image_def} & is the image of a function over a set
    1.15 +\end{tabular}
    1.16 +\end{center}
    1.17 +
    1.18 +See \cite{Nipkow-Main} for the wealth of further predefined functions in theory
    1.19 +@{theory Main}.
    1.20 +
    1.21  \section{Proof automation}
    1.22  
    1.23  So far we have only seen @{text simp} and @{text auto}: Both perform