# HG changeset patch # User nipkow # Date 1332943937 -7200 # Node ID da9a2d9e1143099a725f9f20a6988213b2242954 # Parent 9756bcb8882987d131732a4df4e01092e0407b21# Parent 97db4b6b6a2c3e73da42b91ee1d20fcb71a90c68 merged diff -r 9756bcb88829 -r da9a2d9e1143 doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Wed Mar 28 14:54:33 2012 +0200 +++ b/doc-src/Main/Docs/Main_Doc.thy Wed Mar 28 16:12:17 2012 +0200 @@ -105,8 +105,8 @@ \section{Set} -Sets are predicates: @{text[source]"'a set = 'a \ bool"} -\bigskip +%Sets are predicates: @{text[source]"'a set = 'a \ bool"} +%\bigskip \begin{supertabular}{@ {} l @ {~::~} l l @ {}} @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ @@ -236,7 +236,7 @@ \section{Relation} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} 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\('b*'c)set\('a*'c)set"}\\ @{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\'a set\'b set"}\\ @@ -254,13 +254,17 @@ @{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{supertabular} +\end{tabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} @{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$) \end{tabular} +\medskip + +\noindent +Type synonym @{typ"'a rel"} @{text"="} @{typ "('a * 'a)set"} \section{Equiv\_Relations} @@ -338,6 +342,7 @@ @{term "op + :: nat \ nat \ nat"} & @{term "op - :: nat \ nat \ nat"} & @{term "op * :: nat \ nat \ nat"} & +@{term "op ^ :: nat \ nat \ nat"} & @{term "op div :: nat \ nat \ nat"}& @{term "op mod :: nat \ nat \ nat"}& @{term "op dvd :: nat \ nat \ bool"}\\ @@ -495,6 +500,7 @@ @{const List.drop} & @{typeof List.drop}\\ @{const List.dropWhile} & @{typeof List.dropWhile}\\ @{const List.filter} & @{typeof List.filter}\\ +@{const List.find} & @{typeof List.find}\\ @{const List.fold} & @{typeof List.fold}\\ @{const List.foldr} & @{typeof List.foldr}\\ @{const List.foldl} & @{typeof List.foldl}\\ @@ -557,9 +563,6 @@ Maps model partial functions and are often used as finite tables. However, the domain of a map may be infinite. -@{text"'a \ 'b = 'a \ 'b option"} -\bigskip - \begin{supertabular}{@ {} l @ {~::~} l @ {}} @{const Map.empty} & @{typeof Map.empty}\\ @{const Map.map_add} & @{typeof Map.map_add}\\ diff -r 9756bcb88829 -r da9a2d9e1143 doc-src/Main/Docs/document/Main_Doc.tex --- a/doc-src/Main/Docs/document/Main_Doc.tex Wed Mar 28 14:54:33 2012 +0200 +++ b/doc-src/Main/Docs/document/Main_Doc.tex Wed Mar 28 16:12:17 2012 +0200 @@ -113,8 +113,8 @@ \section{Set} -Sets are predicates: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ set\ \ {\isaliteral{3D}{\isacharequal}}\ \ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequote}}} -\bigskip +%Sets are predicates: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ set\ \ {\isaliteral{3D}{\isacharequal}}\ \ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequote}}} +%\bigskip \begin{supertabular}{@ {} l @ {~::~} l l @ {}} \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set}\\ @@ -244,7 +244,7 @@ \section{Relation} -\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\begin{tabular}{@ {} l @ {~::~} l @ {}} \isa{converse} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ \isa{op\ O} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ set}\\ \isa{op\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\ @@ -262,13 +262,17 @@ \isa{irrefl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ \isa{total{\isaliteral{5F}{\isacharunderscore}}on} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ \isa{total} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\end{supertabular} +\end{tabular} \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \isa{r{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}} & \isa{{\isaliteral{22}{\isachardoublequote}}converse\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^-1$) \end{tabular} +\medskip + +\noindent +Type synonym \isa{{\isaliteral{27}{\isacharprime}}a\ rel} \isa{{\isaliteral{3D}{\isacharequal}}} \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set} \section{Equiv\_Relations} @@ -345,6 +349,7 @@ \isa{op\ {\isaliteral{2B}{\isacharplus}}} & \isa{op\ {\isaliteral{2D}{\isacharminus}}} & \isa{op\ {\isaliteral{2A}{\isacharasterisk}}} & +\isa{op\ {\isaliteral{5E}{\isacharcircum}}} & \isa{op\ div}& \isa{op\ mod}& \isa{op\ dvd}\\ @@ -502,6 +507,7 @@ \isa{drop} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ \isa{dropWhile} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ \isa{filter} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ +\isa{List{\isaliteral{2E}{\isachardot}}find} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option}\\ \isa{fold} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ \isa{foldr} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ \isa{foldl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ @@ -564,9 +570,6 @@ Maps model partial functions and are often used as finite tables. However, the domain of a map may be infinite. -\isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C7269676874686172706F6F6E75703E}{\isasymrightharpoonup}}\ {\isaliteral{27}{\isacharprime}}b\ \ {\isaliteral{3D}{\isacharequal}}\ \ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option} -\bigskip - \begin{supertabular}{@ {} l @ {~::~} l @ {}} \isa{Map{\isaliteral{2E}{\isachardot}}empty} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\ \isa{op\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\