1.1 --- a/doc-src/Main/Docs/Main_Doc.thy Wed Mar 28 08:25:51 2012 +0200
1.2 +++ b/doc-src/Main/Docs/Main_Doc.thy Wed Mar 28 16:12:10 2012 +0200
1.3 @@ -105,8 +105,8 @@
1.4
1.5 \section{Set}
1.6
1.7 -Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"}
1.8 -\bigskip
1.9 +%Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"}
1.10 +%\bigskip
1.11
1.12 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
1.13 @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
1.14 @@ -236,7 +236,7 @@
1.15
1.16 \section{Relation}
1.17
1.18 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
1.19 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
1.20 @{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
1.21 @{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('b*'c)set\<Rightarrow>('a*'c)set"}\\
1.22 @{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\
1.23 @@ -254,13 +254,17 @@
1.24 @{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\
1.25 @{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
1.26 @{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\
1.27 -\end{supertabular}
1.28 +\end{tabular}
1.29
1.30 \subsubsection*{Syntax}
1.31
1.32 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
1.33 @{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$)
1.34 \end{tabular}
1.35 +\medskip
1.36 +
1.37 +\noindent
1.38 +Type synonym @{typ"'a rel"} @{text"="} @{typ "('a * 'a)set"}
1.39
1.40 \section{Equiv\_Relations}
1.41
1.42 @@ -338,6 +342,7 @@
1.43 @{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
1.44 @{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
1.45 @{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
1.46 +@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
1.47 @{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
1.48 @{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
1.49 @{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\
1.50 @@ -495,6 +500,7 @@
1.51 @{const List.drop} & @{typeof List.drop}\\
1.52 @{const List.dropWhile} & @{typeof List.dropWhile}\\
1.53 @{const List.filter} & @{typeof List.filter}\\
1.54 +@{const List.find} & @{typeof List.find}\\
1.55 @{const List.fold} & @{typeof List.fold}\\
1.56 @{const List.foldr} & @{typeof List.foldr}\\
1.57 @{const List.foldl} & @{typeof List.foldl}\\
1.58 @@ -557,9 +563,6 @@
1.59 Maps model partial functions and are often used as finite tables. However,
1.60 the domain of a map may be infinite.
1.61
1.62 -@{text"'a \<rightharpoonup> 'b = 'a \<Rightarrow> 'b option"}
1.63 -\bigskip
1.64 -
1.65 \begin{supertabular}{@ {} l @ {~::~} l @ {}}
1.66 @{const Map.empty} & @{typeof Map.empty}\\
1.67 @{const Map.map_add} & @{typeof Map.map_add}\\
2.1 --- a/doc-src/Main/Docs/document/Main_Doc.tex Wed Mar 28 08:25:51 2012 +0200
2.2 +++ b/doc-src/Main/Docs/document/Main_Doc.tex Wed Mar 28 16:12:10 2012 +0200
2.3 @@ -113,8 +113,8 @@
2.4
2.5 \section{Set}
2.6
2.7 -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}}}
2.8 -\bigskip
2.9 +%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}}}
2.10 +%\bigskip
2.11
2.12 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
2.13 \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set}\\
2.14 @@ -244,7 +244,7 @@
2.15
2.16 \section{Relation}
2.17
2.18 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
2.19 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
2.20 \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}\\
2.21 \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}\\
2.22 \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}\\
2.23 @@ -262,13 +262,17 @@
2.24 \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}\\
2.25 \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}\\
2.26 \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}\\
2.27 -\end{supertabular}
2.28 +\end{tabular}
2.29
2.30 \subsubsection*{Syntax}
2.31
2.32 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
2.33 \isa{r{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}} & \isa{{\isaliteral{22}{\isachardoublequote}}converse\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^-1$)
2.34 \end{tabular}
2.35 +\medskip
2.36 +
2.37 +\noindent
2.38 +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}
2.39
2.40 \section{Equiv\_Relations}
2.41
2.42 @@ -345,6 +349,7 @@
2.43 \isa{op\ {\isaliteral{2B}{\isacharplus}}} &
2.44 \isa{op\ {\isaliteral{2D}{\isacharminus}}} &
2.45 \isa{op\ {\isaliteral{2A}{\isacharasterisk}}} &
2.46 +\isa{op\ {\isaliteral{5E}{\isacharcircum}}} &
2.47 \isa{op\ div}&
2.48 \isa{op\ mod}&
2.49 \isa{op\ dvd}\\
2.50 @@ -502,6 +507,7 @@
2.51 \isa{drop} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
2.52 \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}\\
2.53 \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}\\
2.54 +\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}\\
2.55 \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}\\
2.56 \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}\\
2.57 \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}\\
2.58 @@ -564,9 +570,6 @@
2.59 Maps model partial functions and are often used as finite tables. However,
2.60 the domain of a map may be infinite.
2.61
2.62 -\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}
2.63 -\bigskip
2.64 -
2.65 \begin{supertabular}{@ {} l @ {~::~} l @ {}}
2.66 \isa{Map{\isaliteral{2E}{\isachardot}}empty} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\
2.67 \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}\\