# HG changeset patch # User wenzelm # Date 1236790261 -3600 # Node ID 62139eb64bfe54fa9fbead7ce4a240a9d83b892a # Parent c2d49315b93bec69821f89b8dcd05a18f05b0d46# Parent 873fa77be5f0990680c755665245d9dc00981bf7 merged diff -r c2d49315b93b -r 62139eb64bfe NEWS --- a/NEWS Wed Mar 11 16:36:27 2009 +0100 +++ b/NEWS Wed Mar 11 17:51:01 2009 +0100 @@ -244,7 +244,8 @@ * Theory HOL/Decisioin_Procs/Approximation.thy provides the new proof method "approximation". It proves formulas on real values by using interval arithmetic. In the formulas are also the transcendental functions sin, cos, tan, atan, ln, -exp and the constant pi are allowed. For examples see HOL/ex/ApproximationEx.thy. +exp and the constant pi are allowed. For examples see +HOL/Descision_Procs/ex/Approximation_Ex.thy. * Theory "Reflection" now resides in HOL/Library. diff -r c2d49315b93b -r 62139eb64bfe doc-src/Dirs --- a/doc-src/Dirs Wed Mar 11 16:36:27 2009 +0100 +++ b/doc-src/Dirs Wed Mar 11 17:51:01 2009 +0100 @@ -1,1 +1,1 @@ -Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions +Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Main diff -r c2d49315b93b -r 62139eb64bfe doc-src/Main/Main_Doc.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/Main_Doc.tex Wed Mar 11 17:51:01 2009 +0100 @@ -0,0 +1,597 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Main{\isacharunderscore}Doc}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\begin{isamarkuptext}% +\begin{abstract} +This document lists the main types, functions and syntax provided by theory \isa{Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/dist/library/HOL/}. +\end{abstract} + +\section{HOL} + +The basic logic: \isa{x\ {\isacharequal}\ y}, \isa{True}, \isa{False}, \isa{{\isasymnot}\ P}, \isa{P\ {\isasymand}\ Q}, \isa{P\ {\isasymor}\ Q}, \isa{P\ {\isasymlongrightarrow}\ Q}, \isa{{\isasymforall}x{\isachardot}\ P}, \isa{{\isasymexists}x{\isachardot}\ P}, \isa{{\isasymexists}{\isacharbang}x{\isachardot}\ P}, \isa{THE\ x{\isachardot}\ P}. +\smallskip + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{undefined} & \isa{{\isacharprime}a}\\ +\isa{default} & \isa{{\isacharprime}a}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{x\ {\isasymnoteq}\ y} & \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}} & (\verb$~=$)\\ +\isa{{\isachardoublequote}P\ {\isasymlongleftrightarrow}\ Q{\isachardoublequote}} & \isa{P\ {\isacharequal}\ Q} \\ +\isa{if\ x\ then\ y\ else\ z} & \isa{{\isachardoublequote}If\ x\ y\ z{\isachardoublequote}}\\ +\isa{let\ x\ {\isacharequal}\ e\isactrlisub {\isadigit{1}}\ in\ e\isactrlisub {\isadigit{2}}} & \isa{{\isachardoublequote}Let\ e\isactrlisub {\isadigit{1}}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequote}}\\ +\end{supertabular} + + +\section{Orderings} + +A collection of classes defining basic orderings: +preorder, partial order, linear order, dense linear order and wellorder. +\smallskip + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\isa{op\ {\isasymle}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (\verb$<=$)\\ +\isa{op\ {\isacharless}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\ +\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{min} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{max} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{top} & \isa{{\isacharprime}a}\\ +\isa{bot} & \isa{{\isacharprime}a}\\ +\isa{mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{strict{\isacharunderscore}mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{{\isachardoublequote}x\ {\isasymge}\ y{\isachardoublequote}} & \isa{y\ {\isasymle}\ x} & (\verb$>=$)\\ +\isa{{\isachardoublequote}x\ {\isachargreater}\ y{\isachardoublequote}} & \isa{y\ {\isacharless}\ x}\\ +\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P{\isachardoublequote}}\\ +\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P{\isachardoublequote}}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ +\isa{LEAST\ x{\isachardot}\ P} & \isa{{\isachardoublequote}Least\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ +\end{supertabular} + + +\section{Lattices} + +Classes semilattice, lattice, distributive lattice and complete lattice (the +latter in theory \isa{Set}). + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{inf} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{sup} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{Inf} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{Sup} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\end{tabular} + +\subsubsection*{Syntax} + +Available by loading theory \isa{Lattice{\isacharunderscore}Syntax} in directory \isa{Library}. + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{{\isachardoublequote}x\ {\isasymsqsubseteq}\ y{\isachardoublequote}} & \isa{x\ {\isasymle}\ y}\\ +\isa{{\isachardoublequote}x\ {\isasymsqsubset}\ y{\isachardoublequote}} & \isa{x\ {\isacharless}\ y}\\ +\isa{{\isachardoublequote}x\ {\isasymsqinter}\ y{\isachardoublequote}} & \isa{inf\ x\ y}\\ +\isa{{\isachardoublequote}x\ {\isasymsqunion}\ y{\isachardoublequote}} & \isa{sup\ x\ y}\\ +\isa{{\isachardoublequote}{\isasymSqinter}\ A{\isachardoublequote}} & \isa{Sup\ A}\\ +\isa{{\isachardoublequote}{\isasymSqunion}\ A{\isachardoublequote}} & \isa{Inf\ A}\\ +\isa{{\isachardoublequote}{\isasymtop}{\isachardoublequote}} & \isa{top}\\ +\isa{{\isachardoublequote}{\isasymbottom}{\isachardoublequote}} & \isa{bot}\\ +\end{supertabular} + + +\section{Set} + +Sets are predicates: \isa{{\isachardoublequote}{\isacharprime}a\ set\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\isa{{\isacharbraceleft}{\isacharbraceright}} & \isa{{\isacharprime}a\ set}\\ +\isa{insert} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{Collect} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{op\ {\isasymin}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool} & (\texttt{:})\\ +\isa{op\ {\isasymunion}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Un})\\ +\isa{op\ {\isasyminter}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Int})\\ +\isa{UNION} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{INTER} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{Union} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{Inter} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{Pow} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\ +\isa{UNIV} & \isa{{\isacharprime}a\ set}\\ +\isa{op\ {\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{Ball} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{Bex} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{{\isacharbraceleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharbraceright}} & \isa{insert\ x\isactrlisub {\isadigit{1}}\ {\isacharparenleft}{\isasymdots}\ {\isacharparenleft}insert\ x\isactrlisub n\ {\isacharbraceleft}{\isacharbraceright}{\isacharparenright}{\isasymdots}{\isacharparenright}}\\ +\isa{x\ {\isasymnotin}\ A} & \isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isasymin}\ A{\isacharparenright}{\isachardoublequote}}\\ +\isa{A\ {\isasymsubseteq}\ B} & \isa{{\isachardoublequote}A\ {\isasymle}\ B{\isachardoublequote}}\\ +\isa{A\ {\isasymsubset}\ B} & \isa{{\isachardoublequote}A\ {\isacharless}\ B{\isachardoublequote}}\\ +\isa{{\isachardoublequote}A\ {\isasymsupseteq}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isasymle}\ A{\isachardoublequote}}\\ +\isa{{\isachardoublequote}A\ {\isasymsupset}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isacharless}\ A{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}} & \isa{{\isachardoublequote}Collect\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ +\isa{{\isasymUnion}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{UN})\\ +\isa{{\isasymUnion}x{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\ +\isa{{\isasymInter}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{INT})\\ +\isa{{\isasymInter}x{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\ +\isa{{\isasymforall}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Ball\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ +\isa{{\isasymexists}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Bex\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ +\isa{range\ f} & \isa{{\isachardoublequote}f\ {\isacharbackquote}\ UNIV{\isachardoublequote}}\\ +\end{supertabular} + + +\section{Fun} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{id} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{op\ {\isasymcirc}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{inj{\isacharunderscore}on} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\ +\isa{inj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{surj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{bij} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{bij{\isacharunderscore}betw} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ bool}\\ +\isa{fun{\isacharunderscore}upd} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{f{\isacharparenleft}x\ {\isacharcolon}{\isacharequal}\ y{\isacharparenright}} & \isa{{\isachardoublequote}fun{\isacharunderscore}upd\ f\ x\ y{\isachardoublequote}}\\ +\isa{f{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharequal}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharcolon}{\isacharequal}y\isactrlisub n{\isacharparenright}} & \isa{f{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharequal}y\isactrlisub {\isadigit{1}}{\isacharparenright}{\isasymdots}{\isacharparenleft}x\isactrlisub n{\isacharcolon}{\isacharequal}y\isactrlisub n{\isacharparenright}}\\ +\end{tabular} + + +\section{Fixed Points} + +Theory: \isa{Inductive}. + +Least and greatest fixed points in a complete lattice \isa{{\isacharprime}a}: + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{lfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{gfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\end{tabular} + +Note that in particular sets (\isa{{\isacharprime}a\ {\isasymRightarrow}\ bool}) are complete lattices. + +\section{Sum\_Type} + +Type constructor \isa{{\isacharplus}}. + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{Inl} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isacharplus}\ {\isacharprime}b}\\ +\isa{Inr} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isacharplus}\ {\isacharprime}a}\\ +\isa{op\ {\isacharless}{\isacharplus}{\isachargreater}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharplus}\ {\isacharprime}b{\isacharparenright}\ set} +\end{tabular} + + +\section{Product\_Type} + +Types \isa{unit} and \isa{{\isasymtimes}}. + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{{\isacharparenleft}{\isacharparenright}} & \isa{unit}\\ +\isa{Pair} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}\\ +\isa{fst} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{snd} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{split} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\ +\isa{curry} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\ +\isa{Sigma} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} +\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}} & \isa{{\isachardoublequote}Pair\ a\ b{\isachardoublequote}}\\ +\isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} & \isa{{\isachardoublequote}split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}{\isachardoublequote}}\\ +\isa{A\ {\isasymtimes}\ B} & \isa{Sigma\ A\ {\isacharparenleft}{\isasymlambda}\_{\isachardot}\ B{\isacharparenright}} & (\verb$<*>$) +\end{tabular} + +Pairs may be nested. Nesting to the right is printed as a tuple, +e.g.\ \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ c{\isacharparenright}}} is really \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ {\isacharparenleft}b{\isacharcomma}\ c{\isacharparenright}{\isacharparenright}}.} +Pattern matching with pairs and tuples extends to all binders, +e.g.\ \mbox{\isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ P},} \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ P{\isacharbraceright}}, etc. + + +\section{Relation} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{converse} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{op\ O} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\ +\isa{op\ {\isacharbackquote}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{inv{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\ +\isa{Id{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{Id} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{Domain} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{Range} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{Field} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{refl{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{refl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{sym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{antisym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{trans} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{irrefl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{total{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{total} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{r{\isasyminverse}} & \isa{{\isachardoublequote}converse\ r{\isachardoublequote}} & (\verb$^-1$) +\end{tabular} + +\section{Equiv\_Relations} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{equiv} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{op\ {\isacharslash}{\isacharslash}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\ +\isa{congruent} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{congruent{\isadigit{2}}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{f\ respects\ r} & \isa{{\isachardoublequote}congruent\ r\ f{\isachardoublequote}}\\ +\isa{f\ respects{\isadigit{2}}\ r} & \isa{{\isachardoublequote}congruent{\isadigit{2}}\ r\ r\ f{\isachardoublequote}}\\ +\end{tabular} + + +\section{Transitive\_Closure} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{rtrancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{trancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{reflcl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{r\isactrlsup {\isacharasterisk}} & \isa{{\isachardoublequote}rtrancl\ r{\isachardoublequote}} & (\verb$^*$)\\ +\isa{r\isactrlsup {\isacharplus}} & \isa{{\isachardoublequote}trancl\ r{\isachardoublequote}} & (\verb$^+$)\\ +\isa{r\isactrlsup {\isacharequal}} & \isa{{\isachardoublequote}reflcl\ r{\isachardoublequote}} & (\verb$^=$) +\end{tabular} + + +\section{Algebra} + +Theories \isa{OrderedGroup}, \isa{Ring{\isacharunderscore}and{\isacharunderscore}Field} and \isa{Divides} define a large collection of classes describing common algebraic +structures from semigroups up to fields. Everything is done in terms of +overloaded operators: + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\isa{{\isadigit{0}}} & \isa{{\isacharprime}a}\\ +\isa{{\isadigit{1}}} & \isa{{\isacharprime}a}\\ +\isa{op\ {\isacharplus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{op\ {\isacharminus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{uminus} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (\verb$-$)\\ +\isa{op\ {\isacharasterisk}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{inverse} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{op\ {\isacharslash}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{abs} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{sgn} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{op\ dvd} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\ +\isa{op\ div} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{op\ mod} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{{\isasymbar}x{\isasymbar}} & \isa{{\isachardoublequote}abs\ x{\isachardoublequote}} +\end{tabular} + + +\section{Nat} + +\isa{\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat} +\bigskip + +\begin{tabular}{@ {} lllllll @ {}} +\isa{op\ {\isacharplus}} & +\isa{op\ {\isacharminus}} & +\isa{op\ {\isacharasterisk}} & +\isa{op\ {\isacharcircum}} & +\isa{op\ div}& +\isa{op\ mod}& +\isa{op\ dvd}\\ +\isa{op\ {\isasymle}} & +\isa{op\ {\isacharless}} & +\isa{min} & +\isa{max} & +\isa{Min} & +\isa{Max}\\ +\end{tabular} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a} +\end{tabular} + +\section{Int} + +Type \isa{int} +\bigskip + +\begin{tabular}{@ {} llllllll @ {}} +\isa{op\ {\isacharplus}} & +\isa{op\ {\isacharminus}} & +\isa{uminus} & +\isa{op\ {\isacharasterisk}} & +\isa{op\ {\isacharcircum}} & +\isa{op\ div}& +\isa{op\ mod}& +\isa{op\ dvd}\\ +\isa{op\ {\isasymle}} & +\isa{op\ {\isacharless}} & +\isa{min} & +\isa{max} & +\isa{Min} & +\isa{Max}\\ +\isa{abs} & +\isa{sgn}\\ +\end{tabular} + +\begin{tabular}{@ {} l @ {~::~} l l @ {}} +\isa{nat} & \isa{int\ {\isasymRightarrow}\ nat}\\ +\isa{of{\isacharunderscore}int} & \isa{int\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{{\isasymint}} & \isa{{\isacharprime}a\ set} & (\verb$Ints$) +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{int} & \isa{{\isachardoublequote}of{\isacharunderscore}nat{\isachardoublequote}}\\ +\end{tabular} + + +\section{Finite\_Set} + + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{finite} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\ +\isa{card} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ nat}\\ +\isa{fold} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{fold{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{setsum} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{setprod} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\end{supertabular} + + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{{\isasymSum}A} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x{\isacharparenright}\ A{\isachardoublequote}} & (\verb$SUM$)\\ +\isa{{\isasymSum}x{\isasymin}A{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ A{\isachardoublequote}}\\ +\isa{{\isachardoublequote}{\isasymSum}x{\isacharbar}P{\isachardot}\ t{\isachardoublequote}} & \isa{{\isasymSum}x{\isasymin}{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}{\isachardot}\ t}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}} & (\verb$PROD$)\\ +\end{supertabular} + + +\section{Wellfounded} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{wf} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{acyclic} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{acc} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{measure} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{op\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\ +\isa{op\ {\isacharless}{\isacharasterisk}mlex{\isacharasterisk}{\isachargreater}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{less{\isacharunderscore}than} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\ +\isa{pred{\isacharunderscore}nat} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\ +\end{supertabular} + + +\section{SetInterval} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{lessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{atMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{greaterThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{atLeast} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{greaterThanLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{atLeastLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{greaterThanAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{atLeastAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{{\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}lessThan\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atMost\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThan\ x{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}atLeast\ x{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanLessThan\ x\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastLessThan\ x\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanAtMost\ x\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastAtMost\ x\ y{\isachardoublequote}}\\ +\isa{{\isasymUnion}\ i{\isasymle}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\ +\isa{{\isasymUnion}\ i{\isacharless}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymInter}} instead of \isa{{\isasymUnion}}}\\ +\isa{{\isasymSum}x\ {\isacharequal}\ a{\isachardot}{\isachardot}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}a{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\ +\isa{{\isasymSum}x\ {\isacharequal}\ a{\isachardot}{\isachardot}{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}a{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\ +\isa{{\isasymSum}x{\isasymle}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\ +\isa{{\isasymSum}x{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}}\\ +\end{supertabular} + + +\section{Power} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{op\ {\isacharcircum}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} +\end{tabular} + + +\section{Iterated Functions and Relations} + +Theory: \isa{Relation{\isacharunderscore}Power} + +Iterated functions \ \isa{{\isachardoublequote}{\isacharparenleft}f{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isasymRightarrow}{\isacharprime}a{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}} \ +and relations \ \isa{{\isachardoublequote}{\isacharparenleft}r{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}a{\isacharparenright}set{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}}. + + +\section{Option} + +\isa{\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a} +\bigskip + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{the} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{Option{\isachardot}map} & \isa{{\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequote}}\\ +\isa{Option{\isachardot}set} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a\ set} +\end{tabular} + +\section{List} + +\isa{\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ op\ {\isacharhash}\ {\isacharprime}a\ {\isacharparenleft}{\isacharprime}a\ list{\isacharparenright}} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{op\ {\isacharat}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{butlast} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{concat} & \isa{{\isacharprime}a\ list\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{distinct} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\ +\isa{drop} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{dropWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{filter} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{foldl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{foldr} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{hd} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{last} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{length} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat}\\ +\isa{lenlex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{lex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{lexn} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{lexord} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{listrel} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{lists} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\ +\isa{listset} & \isa{{\isacharprime}a\ set\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\ +\isa{listsum} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{list{\isacharunderscore}all{\isadigit{2}}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ bool}\\ +\isa{list{\isacharunderscore}update} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{map} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list}\\ +\isa{measures} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{remdups} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{removeAll} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{remove{\isadigit{1}}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{replicate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{rev} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{rotate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{rotate{\isadigit{1}}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{set} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{sort} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{sorted} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\ +\isa{splice} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{sublist} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{take} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{takeWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{tl} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{upt} & \isa{nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ list}\\ +\isa{upto} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{zip} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharbrackright}} & \isa{x\isactrlisub {\isadigit{1}}\ {\isacharhash}\ {\isasymdots}\ {\isacharhash}\ x\isactrlisub n\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}\\ +\isa{{\isacharbrackleft}m{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}} & \isa{{\isachardoublequote}upt\ m\ n{\isachardoublequote}}\\ +\isa{{\isacharbrackleft}i{\isachardot}{\isachardot}j{\isacharbrackright}} & \isa{{\isachardoublequote}upto\ i\ j{\isachardoublequote}}\\ +\isa{{\isacharbrackleft}e{\isachardot}\ x\ {\isasymleftarrow}\ xs{\isacharbrackright}} & \isa{map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs}\\ +\isa{{\isacharbrackleft}x{\isasymleftarrow}xs\ {\isachardot}\ b{\isacharbrackright}} & \isa{{\isachardoublequote}filter\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}\ xs{\isachardoublequote}} \\ +\isa{xs{\isacharbrackleft}n\ {\isacharcolon}{\isacharequal}\ x{\isacharbrackright}} & \isa{{\isachardoublequote}list{\isacharunderscore}update\ xs\ n\ x{\isachardoublequote}}\\ +\isa{{\isasymSum}x{\isasymleftarrow}xs{\isachardot}\ e} & \isa{{\isachardoublequote}listsum\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}}\\ +\end{supertabular} +\medskip + +List comprehension: \isa{{\isacharbrackleft}e{\isachardot}\ q\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ q\isactrlisub n{\isacharbrackright}} where each +qualifier \isa{q\isactrlisub i} is either a generator \mbox{\isa{pat\ {\isasymleftarrow}\ e}} or a +guard, i.e.\ boolean expression. + +\section{Map} + +Maps model partial functions and are often used as finite tables. However, +the domain of a map may be infinite. + +\isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{Map{\isachardot}empty} & \isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ +\isa{op\ {\isacharplus}{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ +\isa{op\ {\isasymcirc}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymrightharpoonup}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ +\isa{op\ {\isacharbar}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ +\isa{dom} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{ran} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{op\ {\isasymsubseteq}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{map{\isacharunderscore}of} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ +\isa{map{\isacharunderscore}upds} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{Map{\isachardot}empty} & \isa{{\isasymlambda}x{\isachardot}\ None}\\ +\isa{m{\isacharparenleft}x\ {\isasymmapsto}\ y{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x{\isacharcolon}{\isacharequal}Some\ y{\isacharparenright}{\isachardoublequote}}\\ +\isa{m{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharparenright}{\isasymdots}{\isacharparenleft}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}{\isachardoublequote}}\\ +\isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharbrackright}} & \isa{{\isachardoublequote}Map{\isachardot}empty{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}{\isachardoublequote}}\\ +\isa{m{\isacharparenleft}xs\ {\isacharbrackleft}{\isasymmapsto}{\isacharbrackright}\ ys{\isacharparenright}} & \isa{{\isachardoublequote}map{\isacharunderscore}upds\ m\ xs\ ys{\isachardoublequote}}\\ +\end{tabular}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r c2d49315b93b -r 62139eb64bfe doc-src/Main/Makefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/Makefile Wed Mar 11 17:51:01 2009 +0100 @@ -0,0 +1,45 @@ +# +# $Id$ +# + +## targets + +default: dvi + + +## dependencies + +include ../Makefile.in + +SRC = ../../src/HOL/Docs/generated + +NAME = main + +FILES = $(NAME).tex Main_Doc.tex \ + isabelle.sty isabellesym.sty pdfsetup.sty + +dvi: $(NAME).dvi + +$(NAME).dvi: $(FILES) + $(LATEX) $(NAME) + +pdf: $(NAME).pdf + +$(NAME).pdf: $(FILES) + $(PDFLATEX) $(NAME) + $(FIXBOOKMARKS) $(NAME).out + $(PDFLATEX) $(NAME) + $(PDFLATEX) $(NAME) + +isabelle.sty: + ln ../isabelle.sty . + +isabellesym.sty: + ln ../isabellesym.sty . + +pdfsetup.sty: + ln ../pdfsetup.sty . + +copy: + cp $(SRC)/Main_Doc.tex Main_Doc.tex + cp $(SRC)/root.tex main.tex diff -r c2d49315b93b -r 62139eb64bfe doc-src/Main/main.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/main.tex Wed Mar 11 17:51:01 2009 +0100 @@ -0,0 +1,65 @@ +\documentclass[12pt,a4paper]{article} + +\oddsidemargin=4.6mm +\evensidemargin=4.6mm +\textwidth=150mm +\topmargin=4.6mm +\headheight=0mm +\headsep=0mm +\textheight=234mm + +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage[greek,english]{babel} + %option greek for \ + %option english (default language) for \, \ + +%\usepackage[latin1]{inputenc} + %for \, \, \, \, + %\, \, \ + +\usepackage[only,bigsqcap]{stmaryrd} + %for \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +\renewcommand{\isastyle}{\isastyleminor} + +\parindent 0pt\parskip 0.5ex + +\usepackage{supertabular} + +\begin{document} + +\title{What's in Main} +\author{Tobias Nipkow} +\date{\today} +\maketitle + +\input{Main_Doc} + +% optional bibliography +%\bibliographystyle{abbrv} +%\bibliography{root} + +\end{document} diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed Mar 11 17:51:01 2009 +0100 @@ -1,6 +1,4 @@ -(* Title: HOL/Reflection/Approximation.thy - Author: Johannes Hoelzl 2008 / 2009 -*) +(* Author: Johannes Hoelzl 2008 / 2009 *) header {* Prove unequations about real numbers by computation *} @@ -2408,20 +2406,15 @@ lemma bounded_divr: assumes "x \ Ifloat a / Ifloat b" shows "x \ Ifloat (float_divr p a b)" by (rule order_trans[OF assms _], rule float_divr) lemma bounded_num: shows "Ifloat (Float 5 1) = 10" and "Ifloat (Float 0 0) = 0" and "Ifloat (Float 1 0) = 1" and "Ifloat (Float (number_of n) 0) = (number_of n)" and "0 * pow2 e = Ifloat (Float 0 e)" and "1 * pow2 e = Ifloat (Float 1 e)" and "number_of m * pow2 e = Ifloat (Float (number_of m) e)" - by (auto simp add: Ifloat.simps pow2_def) + and "Ifloat (Float (number_of A) (int B)) = (number_of A) * 2^B" + and "Ifloat (Float 1 (int B)) = 2^B" + and "Ifloat (Float (number_of A) (- int B)) = (number_of A) / 2^B" + and "Ifloat (Float 1 (- int B)) = 1 / 2^B" + by (auto simp add: Ifloat.simps pow2_def real_divide_def) lemmas bounded_by_equations = bounded_by_Cons bounded_by_Nil float_power bounded_divl bounded_divr bounded_num HOL.simp_thms lemmas uneq_equations = uneq.simps Ifloatarith.simps Ifloatarith_num Ifloatarith_divide Ifloatarith_diff Ifloatarith_tan Ifloatarith_powr Ifloatarith_log -lemma "x div (0::int) = 0" by auto -- "What happens in the zero case for div" -lemma "x mod (0::int) = x" by auto -- "What happens in the zero case for mod" - -text {* The following equations must hold for div & mod - -- see "The Definition of Standard ML" by R. Milner, M. Tofte and R. Harper (pg. 79) *} -lemma "d * (i div d) + i mod d = (i::int)" by auto -lemma "0 < (d :: int) \ 0 \ i mod d \ i mod d < d" by auto -lemma "(d :: int) < 0 \ d < i mod d \ i mod d \ 0" by auto - ML {* val uneq_equations = PureThy.get_thms @{theory} "uneq_equations"; val bounded_by_equations = PureThy.get_thms @{theory} "bounded_by_equations"; @@ -2438,24 +2431,37 @@ val to_natc = conv_num @{typ "nat"} #> Thm.cterm_of (ProofContext.theory_of ctxt) val to_nat = conv_num @{typ "nat"} val to_int = conv_num @{typ "int"} + fun int_to_float A = @{term "Float"} $ to_int A $ @{term "0 :: int"} val prec' = to_nat prec fun bot_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp)) = @{term "Float"} $ to_int mantisse $ to_int exp - | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp)) - = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power (Float 5 1)"} $ to_nat exp) - | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ ten) - = @{term "float_divl"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"} - | bot_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"} + | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ (@{term "power 2 :: nat \ real"} $ exp)) + = @{term "Float"} $ to_int mantisse $ (@{term "uminus :: int \ int"} $ (@{term "int :: nat \ int"} $ to_nat exp)) + | bot_float (Const (@{const_name "times"}, _) $ mantisse $ (@{term "power 2 :: nat \ real"} $ exp)) + = @{term "Float"} $ to_int mantisse $ (@{term "int :: nat \ int"} $ to_nat exp) + | bot_float (Const (@{const_name "divide"}, _) $ A $ (@{term "power 10 :: nat \ real"} $ exp)) + = @{term "float_divl"} $ prec' $ (int_to_float A) $ (@{term "power (Float 5 1)"} $ to_nat exp) + | bot_float (Const (@{const_name "divide"}, _) $ A $ B) + = @{term "float_divl"} $ prec' $ int_to_float A $ int_to_float B + | bot_float (@{term "power 2 :: nat \ real"} $ exp) + = @{term "Float 1"} $ (@{term "int :: nat \ int"} $ to_nat exp) + | bot_float A = int_to_float A fun top_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp)) = @{term "Float"} $ to_int mantisse $ to_int exp - | top_float (Const (@{const_name "divide"}, _) $ mantisse $ (Const (@{const_name "power"}, _) $ ten $ exp)) - = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ (@{term "power (Float 5 1)"} $ to_nat exp) - | top_float (Const (@{const_name "divide"}, _) $ mantisse $ ten) - = @{term "float_divr"} $ prec' $ (@{term "Float"} $ to_int mantisse $ @{term "0 :: int"}) $ @{term "Float 5 1"} - | top_float mantisse = @{term "Float"} $ to_int mantisse $ @{term "0 :: int"} + | top_float (Const (@{const_name "divide"}, _) $ mantisse $ (@{term "power 2 :: nat \ real"} $ exp)) + = @{term "Float"} $ to_int mantisse $ (@{term "uminus :: int \ int"} $ (@{term "int :: nat \ int"} $ to_nat exp)) + | top_float (Const (@{const_name "times"}, _) $ mantisse $ (@{term "power 2 :: nat \ real"} $ exp)) + = @{term "Float"} $ to_int mantisse $ (@{term "int :: nat \ int"} $ to_nat exp) + | top_float (Const (@{const_name "divide"}, _) $ A $ (@{term "power 10 :: nat \ real"} $ exp)) + = @{term "float_divr"} $ prec' $ (int_to_float A) $ (@{term "power (Float 5 1)"} $ to_nat exp) + | top_float (Const (@{const_name "divide"}, _) $ A $ B) + = @{term "float_divr"} $ prec' $ int_to_float A $ int_to_float B + | top_float (@{term "power 2 :: nat \ real"} $ exp) + = @{term "Float 1"} $ (@{term "int :: nat \ int"} $ to_nat exp) + | top_float A = int_to_float A val goal' : term = List.nth (prems_of thm, i - 1) @@ -2464,7 +2470,7 @@ bottom $ (Free (name, _))) $ (Const (@{const_name "less_eq"}, _) $ _ $ top))) = ((name, HOLogic.mk_prod (bot_float bottom, top_float top)) - handle TERM (txt, ts) => raise TERM ("Premisse needs format ' <= & <= ', but found " ^ + handle TERM (txt, ts) => raise TERM ("Invalid bound number format: " ^ (Syntax.string_of_term ctxt t), [t])) | lift_bnd t = raise TERM ("Premisse needs format ' <= & <= ', but found " ^ (Syntax.string_of_term ctxt t), [t]) @@ -2501,5 +2507,5 @@ THEN (gen_eval_tac eval_oracle ctxt) i)) end) *} "real number approximation" - + end diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Decision_Procs/Cooper.thy Wed Mar 11 17:51:01 2009 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Reflection/Cooper.thy +(* Title: HOL/Decision_Procs/Cooper.thy Author: Amine Chaieb *) diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Mar 11 17:51:01 2009 +0100 @@ -1,4 +1,4 @@ -(* Title : HOL/Dense_Linear_Order.thy +(* Title : HOL/Decision_Procs/Dense_Linear_Order.thy Author : Amine Chaieb, TU Muenchen *) diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Mar 11 17:51:01 2009 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Reflection/Ferrack.thy +(* Title: HOL/Decision_Procs/Ferrack.thy Author: Amine Chaieb *) diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Wed Mar 11 17:51:01 2009 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Reflection/MIR.thy +(* Title: HOL/Decision_Procs/MIR.thy Author: Amine Chaieb *) diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Mar 11 17:51:01 2009 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Reflection/cooper_tac.ML +(* Title: HOL/Decision_Procs/cooper_tac.ML Author: Amine Chaieb, TU Muenchen *) diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Decision_Procs/ex/Approximation_Ex.thy --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Mar 11 17:51:01 2009 +0100 @@ -1,6 +1,4 @@ -(* Title: HOL/ex/ApproximationEx.thy - Author: Johannes Hoelzl 2009 -*) +(* Author: Johannes Hoelzl 2009 *) theory Approximation_Ex imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" @@ -42,7 +40,7 @@ lemma "0.49 \ x \ x \ 4.49 \ \ arctan x - 0.91 \ < 0.455" by (approximation 20) -lemma "1 * pow2 -1 \ x \ x \ 9 * pow2 -1 \ \ arctan x - 0.91 \ < 0.455" +lemma "1 / 2^1 \ x \ x \ 9 / 2^1 \ \ arctan x - 0.91 \ < 0.455" by (approximation 10) lemma "0 \ x \ x \ 1 \ 0 \ sin x" diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Mar 11 17:51:01 2009 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Reflection/ferrack_tac.ML +(* Title: HOL/Decision_Procs/ferrack_tac.ML Author: Amine Chaieb, TU Muenchen *) diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Mar 11 17:51:01 2009 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Reflection/mir_tac.ML +(* Title: HOL/Decision_Procs/mir_tac.ML Author: Amine Chaieb, TU Muenchen *) diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Docs/Main_Doc.thy --- a/src/HOL/Docs/Main_Doc.thy Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Docs/Main_Doc.thy Wed Mar 11 17:51:01 2009 +0100 @@ -18,62 +18,55 @@ text{* \begin{abstract} -This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. +This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/dist/library/HOL/}. \end{abstract} \section{HOL} -The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. (\textsc{ascii}: \verb$~$, \verb$&$, \verb$|$, \verb$-->$, \texttt{ALL}, \texttt{EX}) +The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. +\smallskip + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const HOL.undefined} & @{typeof HOL.undefined}\\ +@{const HOL.default} & @{typeof HOL.default}\\ +\end{tabular} + +\subsubsection*{Syntax} -Overloaded operators: +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term"~(x = y)"} & @{term[source]"\ (x = y)"} & (\verb$~=$)\\ +@{term[source]"P \ Q"} & @{term"P \ Q"} \\ +@{term"If x y z"} & @{term[source]"If x y z"}\\ +@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\x. e\<^isub>2)"}\\ +\end{supertabular} + + +\section{Orderings} + +A collection of classes defining basic orderings: +preorder, partial order, linear order, dense linear order and wellorder. +\smallskip \begin{supertabular}{@ {} l @ {~::~} l l @ {}} -@{text "0"} & @{typeof HOL.zero}\\ -@{text "1"} & @{typeof HOL.one}\\ -@{const HOL.plus} & @{typeof HOL.plus}\\ -@{const HOL.minus} & @{typeof HOL.minus}\\ -@{const HOL.uminus} & @{typeof HOL.uminus}\\ -@{const HOL.times} & @{typeof HOL.times}\\ -@{const HOL.inverse} & @{typeof HOL.inverse}\\ -@{const HOL.divide} & @{typeof HOL.divide}\\ -@{const HOL.abs} & @{typeof HOL.abs}\\ -@{const HOL.sgn} & @{typeof HOL.sgn}\\ @{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\ @{const HOL.less} & @{typeof HOL.less}\\ -@{const HOL.default} & @{typeof HOL.default}\\ -@{const HOL.undefined} & @{typeof HOL.undefined}\\ +@{const Orderings.Least} & @{typeof Orderings.Least}\\ +@{const Orderings.min} & @{typeof Orderings.min}\\ +@{const Orderings.max} & @{typeof Orderings.max}\\ +@{const[source] top} & @{typeof Orderings.top}\\ +@{const[source] bot} & @{typeof Orderings.bot}\\ +@{const Orderings.mono} & @{typeof Orderings.mono}\\ +@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\ \end{supertabular} \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"~(x = y)"} & @{term[source]"\ (x = y)"}\\ -@{term[source]"P \ Q"} & @{term"P \ Q"}\\ -@{term"If x y z"} & @{term[source]"If x y z"}\\ -@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\x. e\<^isub>2)"}\\ -@{term"abs x"} & @{term[source]"abs x"}\\ -@{term"uminus x"} & @{term[source]"uminus x"}\\ -\end{supertabular} - -\section{Orderings} - -A collection of classes constraining @{text"\"} and @{text"<"}: -preorder, partial order, linear order, dense linear order and wellorder. - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Orderings.Least} & @{typeof Orderings.Least}\\ -@{const Orderings.min} & @{typeof Orderings.min}\\ -@{const Orderings.max} & @{typeof Orderings.max}\\ -@{const Orderings.mono} & @{typeof Orderings.mono}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term[source]"x \ y"} & @{term"x \ y"}\\ +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term[source]"x \ y"} & @{term"x \ y"} & (\verb$>=$)\\ @{term[source]"x > y"} & @{term"x > y"}\\ @{term"ALL x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$, and for @{text"\"}}\\ +@{term"EX x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ @{term"LEAST x. P"} & @{term[source]"Least (\x. P)"}\\ \end{supertabular} @@ -92,7 +85,8 @@ \subsubsection*{Syntax} -Only available locally: +Available by loading theory @{text Lattice_Syntax} in directory @{text +Library}. \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} @{text[source]"x \ y"} & @{term"x \ y"}\\ @@ -101,6 +95,8 @@ @{text[source]"x \ y"} & @{term"sup x y"}\\ @{text[source]"\ A"} & @{term"Sup A"}\\ @{text[source]"\ A"} & @{term"Inf A"}\\ +@{text[source]"\"} & @{term[source] top}\\ +@{text[source]"\"} & @{term[source] bot}\\ \end{supertabular} @@ -136,7 +132,7 @@ @{term"A \ B"} & @{term[source]"A < B"}\\ @{term[source]"A \ B"} & @{term[source]"B \ A"}\\ @{term[source]"A \ B"} & @{term[source]"B < A"}\\ -@{term"{x. P}"} & @{term[source]"Collect(\x. P)"}\\ +@{term"{x. P}"} & @{term[source]"Collect (\x. P)"}\\ @{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\x. A)"} & (\texttt{UN})\\ @{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ @{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\x. A)"} & (\texttt{INT})\\ @@ -203,26 +199,26 @@ @{const snd} & @{typeof snd}\\ @{const split} & @{typeof split}\\ @{const curry} & @{typeof curry}\\ -@{const Product_Type.Times} & @{typeof Product_Type.Times}\\ @{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\('a\'b set)\('a*'b)set"}\\ \end{supertabular} \subsubsection*{Syntax} -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} @{term"Pair a b"} & @{term[source]"Pair a b"}\\ @{term"split (\x y. t)"} & @{term[source]"split (\x y. t)"}\\ +@{term"A <*> B"} & @{text"Sigma A (\\<^raw:\_>. B)"} & (\verb$<*>$) \end{tabular} Pairs may be nested. Nesting to the right is printed as a tuple, -e.g.\ \mbox{@{term"(a,b,c)"}} is really @{text"(a,(b,c))"}. +e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{@{text"(a, (b, c))"}.} Pattern matching with pairs and tuples extends to all binders, -e.g.\ @{prop"ALL (x,y):A. P"}, @{term"{(x,y). P}"}, etc. +e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc. \section{Relation} -\begin{tabular}{@ {} l @ {~::~} l @ {}} +\begin{supertabular}{@ {} l @ {~::~} l @ {}} @{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \ ('b*'a)set"}\\ @{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\('c*'a)set\('c*'b)set"}\\ @{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\'a set\'b set"}\\ @@ -239,13 +235,13 @@ @{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\bool"}\\ @{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\bool"}\\ @{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\('a*'a)set\bool"}\\ -@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\bool"} -\end{tabular} +@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\bool"}\\ +\end{supertabular} \subsubsection*{Syntax} -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"converse r"} & @{term[source]"converse r"} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$) \end{tabular} \section{Equiv\_Relations} @@ -276,19 +272,41 @@ \subsubsection*{Syntax} -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"rtrancl r"} & @{term[source]"rtrancl r"}\\ -@{term"trancl r"} & @{term[source]"trancl r"}\\ -@{term"reflcl r"} & @{term[source]"reflcl r"} +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\verb$^*$)\\ +@{term"trancl r"} & @{term[source]"trancl r"} & (\verb$^+$)\\ +@{term"reflcl r"} & @{term[source]"reflcl r"} & (\verb$^=$) \end{tabular} \section{Algebra} -Theories @{theory OrderedGroup} and @{theory Ring_and_Field} define a large -collection of classes describing common algebraic structures from semigroups -up to fields. Everything is done in terms of @{const plus}, @{const times} -and other overloaded operators. +Theories @{theory OrderedGroup}, @{theory Ring_and_Field} and @{theory +Divides} define a large collection of classes describing common algebraic +structures from semigroups up to fields. Everything is done in terms of +overloaded operators: + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +@{text "0"} & @{typeof zero}\\ +@{text "1"} & @{typeof one}\\ +@{const plus} & @{typeof plus}\\ +@{const minus} & @{typeof minus}\\ +@{const uminus} & @{typeof uminus} & (\verb$-$)\\ +@{const times} & @{typeof times}\\ +@{const inverse} & @{typeof inverse}\\ +@{const divide} & @{typeof divide}\\ +@{const abs} & @{typeof abs}\\ +@{const sgn} & @{typeof sgn}\\ +@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\ +@{const div_class.div} & @{typeof "div_class.div"}\\ +@{const div_class.mod} & @{typeof "div_class.mod"}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"abs x"} & @{term[source]"abs x"} +\end{tabular} \section{Nat} @@ -340,10 +358,10 @@ @{term "sgn :: int \ int"}\\ \end{tabular} -\begin{tabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l l @ {}} @{const Int.nat} & @{typeof Int.nat}\\ @{const Int.of_int} & @{typeof Int.of_int}\\ -@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"}\\ +@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\verb$Ints$) \end{tabular} \subsubsection*{Syntax} @@ -368,11 +386,11 @@ \subsubsection*{Syntax} -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"setsum (%x. x) A"} & @{term[source]"setsum (\x. x) A"}\\ +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term"setsum (%x. x) A"} & @{term[source]"setsum (\x. x) A"} & (\verb$SUM$)\\ @{term"setsum (%x. t) A"} & @{term[source]"setsum (\x. t) A"}\\ @{term[source]"\x|P. t"} & @{term"\x|P. t"}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\"} instead of @{text"\"}}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\"} instead of @{text"\"}} & (\verb$PROD$)\\ \end{supertabular} @@ -514,8 +532,8 @@ \end{supertabular} \medskip -Comprehension: @{text"[e. q\<^isub>1, \, q\<^isub>n]"} where each -qualifier @{text q\<^isub>i} is either a generator @{text"pat \ e"} or a +List comprehension: @{text"[e. q\<^isub>1, \, q\<^isub>n]"} where each +qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \ e"}} or a guard, i.e.\ boolean expression. \section{Map} @@ -544,6 +562,7 @@ @{term"Map.empty"} & @{term"\x. None"}\\ @{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ @{text"m(x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n)"} & @{text[source]"m(x\<^isub>1\y\<^isub>1)\(x\<^isub>n\y\<^isub>n)"}\\ +@{text"[x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n]"} & @{text[source]"Map.empty(x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n)"}\\ @{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ \end{tabular} diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Docs/ROOT.ML --- a/src/HOL/Docs/ROOT.ML Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Docs/ROOT.ML Wed Mar 11 17:51:01 2009 +0100 @@ -1,2 +1,1 @@ use_thy "Main_Doc"; - diff -r c2d49315b93b -r 62139eb64bfe src/HOL/Docs/document/root.tex --- a/src/HOL/Docs/document/root.tex Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/Docs/document/root.tex Wed Mar 11 17:51:01 2009 +0100 @@ -1,4 +1,13 @@ -\documentclass[11pt,a4paper]{article} +\documentclass[12pt,a4paper]{article} + +\oddsidemargin=4.6mm +\evensidemargin=4.6mm +\textwidth=150mm +\topmargin=4.6mm +\headheight=0mm +\headsep=0mm +\textheight=234mm + \usepackage{isabelle,isabellesym} % further packages required for unusual symbols (see also @@ -44,22 +53,13 @@ \title{What's in Main} \author{Tobias Nipkow} -\date{} +\date{\today} \maketitle -%\setcounter{tocdepth}{1} -%\tableofcontents - -% generated text of all theories -\input{session} +\input{Main_Doc} % optional bibliography %\bibliographystyle{abbrv} %\bibliography{root} \end{document} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff -r c2d49315b93b -r 62139eb64bfe src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Mar 11 16:36:27 2009 +0100 +++ b/src/HOL/IsaMakefile Wed Mar 11 17:51:01 2009 +0100 @@ -692,7 +692,7 @@ $(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \ Docs/document/root.tex - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Docs + @$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs ## HOL-Lambda