author | wenzelm |
Mon, 27 Aug 2012 21:30:18 +0200 | |
changeset 48944 | ac15a85e9282 |
parent 47870 | doc-src/Main/Docs/Main_Doc.thy@ec815d64573f |
permissions | -rw-r--r-- |
30293 | 1 |
(*<*) |
30401 | 2 |
theory Main_Doc |
30293 | 3 |
imports Main |
4 |
begin |
|
5 |
||
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
6 |
setup {* |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
7 |
let |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
8 |
fun pretty_term_type_only ctxt (t, T) = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
9 |
(if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
10 |
else error "term_type_only: type mismatch"; |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
11 |
Syntax.pretty_typ ctxt T) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
12 |
in |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
13 |
Thy_Output.antiquotation @{binding term_type_only} |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
14 |
(Args.term -- Args.typ_abbrev) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
15 |
(fn {source, context = ctxt, ...} => fn arg => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
16 |
Thy_Output.output ctxt |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
17 |
(Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg])) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset
|
18 |
end |
30293 | 19 |
*} |
47189
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset
|
20 |
setup {* |
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset
|
21 |
Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single) |
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset
|
22 |
(fn {source, context, ...} => Thy_Output.output context o |
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset
|
23 |
Thy_Output.maybe_pretty_source Syntax.pretty_typ context source) |
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset
|
24 |
*} |
30293 | 25 |
(*>*) |
26 |
text{* |
|
27 |
||
28 |
\begin{abstract} |
|
47870
ec815d64573f
prefer http://isabelle.in.tum.de/library alias, which is available at TUM only;
wenzelm
parents:
47682
diff
changeset
|
29 |
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/library/HOL/}. |
30293 | 30 |
\end{abstract} |
31 |
||
32 |
\section{HOL} |
|
33 |
||
30440 | 34 |
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"}. |
35 |
\smallskip |
|
36 |
||
37 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
38 |
@{const HOL.undefined} & @{typeof HOL.undefined}\\ |
|
39 |
@{const HOL.default} & @{typeof HOL.default}\\ |
|
40 |
\end{tabular} |
|
41 |
||
42 |
\subsubsection*{Syntax} |
|
30293 | 43 |
|
30440 | 44 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
45 |
@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"} & (\verb$~=$)\\ |
|
46 |
@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\ |
|
47 |
@{term"If x y z"} & @{term[source]"If x y z"}\\ |
|
48 |
@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\<lambda>x. e\<^isub>2)"}\\ |
|
49 |
\end{supertabular} |
|
50 |
||
51 |
||
52 |
\section{Orderings} |
|
53 |
||
54 |
A collection of classes defining basic orderings: |
|
55 |
preorder, partial order, linear order, dense linear order and wellorder. |
|
56 |
\smallskip |
|
30293 | 57 |
|
30425 | 58 |
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
35277 | 59 |
@{const Orderings.less_eq} & @{typeof Orderings.less_eq} & (\verb$<=$)\\ |
60 |
@{const Orderings.less} & @{typeof Orderings.less}\\ |
|
30440 | 61 |
@{const Orderings.Least} & @{typeof Orderings.Least}\\ |
62 |
@{const Orderings.min} & @{typeof Orderings.min}\\ |
|
63 |
@{const Orderings.max} & @{typeof Orderings.max}\\ |
|
64 |
@{const[source] top} & @{typeof Orderings.top}\\ |
|
65 |
@{const[source] bot} & @{typeof Orderings.bot}\\ |
|
66 |
@{const Orderings.mono} & @{typeof Orderings.mono}\\ |
|
67 |
@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\ |
|
30293 | 68 |
\end{supertabular} |
69 |
||
70 |
\subsubsection*{Syntax} |
|
71 |
||
30440 | 72 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
73 |
@{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\verb$>=$)\\ |
|
30293 | 74 |
@{term[source]"x > y"} & @{term"x > y"}\\ |
75 |
@{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\ |
|
30440 | 76 |
@{term"EX x<=y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\ |
77 |
\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ |
|
30293 | 78 |
@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\ |
79 |
\end{supertabular} |
|
80 |
||
30401 | 81 |
|
82 |
\section{Lattices} |
|
83 |
||
84 |
Classes semilattice, lattice, distributive lattice and complete lattice (the |
|
85 |
latter in theory @{theory Set}). |
|
86 |
||
87 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
88 |
@{const Lattices.inf} & @{typeof Lattices.inf}\\ |
|
89 |
@{const Lattices.sup} & @{typeof Lattices.sup}\\ |
|
44969 | 90 |
@{const Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\ |
91 |
@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \<Rightarrow> 'a::Sup"}\\ |
|
30401 | 92 |
\end{tabular} |
93 |
||
94 |
\subsubsection*{Syntax} |
|
95 |
||
30440 | 96 |
Available by loading theory @{text Lattice_Syntax} in directory @{text |
97 |
Library}. |
|
30401 | 98 |
|
99 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
100 |
@{text[source]"x \<sqsubseteq> y"} & @{term"x \<le> y"}\\ |
|
101 |
@{text[source]"x \<sqsubset> y"} & @{term"x < y"}\\ |
|
102 |
@{text[source]"x \<sqinter> y"} & @{term"inf x y"}\\ |
|
103 |
@{text[source]"x \<squnion> y"} & @{term"sup x y"}\\ |
|
104 |
@{text[source]"\<Sqinter> A"} & @{term"Sup A"}\\ |
|
105 |
@{text[source]"\<Squnion> A"} & @{term"Inf A"}\\ |
|
30440 | 106 |
@{text[source]"\<top>"} & @{term[source] top}\\ |
107 |
@{text[source]"\<bottom>"} & @{term[source] bot}\\ |
|
30401 | 108 |
\end{supertabular} |
109 |
||
110 |
||
30293 | 111 |
\section{Set} |
112 |
||
47187 | 113 |
%Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"} |
114 |
%\bigskip |
|
30293 | 115 |
|
30425 | 116 |
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
30370 | 117 |
@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ |
32142 | 118 |
@{const Set.insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\ |
30293 | 119 |
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\ |
38323 | 120 |
@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\ |
32208 | 121 |
@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\ |
122 |
@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\ |
|
30293 | 123 |
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
124 |
@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
|
125 |
@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\ |
|
126 |
@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\ |
|
127 |
@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\ |
|
128 |
@{const UNIV} & @{term_type_only UNIV "'a set"}\\ |
|
129 |
@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\ |
|
130 |
@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ |
|
131 |
@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ |
|
132 |
\end{supertabular} |
|
133 |
||
134 |
\subsubsection*{Syntax} |
|
135 |
||
30425 | 136 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
30293 | 137 |
@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\ |
138 |
@{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\ |
|
139 |
@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\ |
|
140 |
@{term"A \<subset> B"} & @{term[source]"A < B"}\\ |
|
141 |
@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\ |
|
142 |
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\ |
|
30440 | 143 |
@{term"{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\ |
30425 | 144 |
@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\ |
30370 | 145 |
@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\ |
30425 | 146 |
@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\ |
30370 | 147 |
@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\ |
30293 | 148 |
@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\ |
149 |
@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\ |
|
150 |
@{term"range f"} & @{term[source]"f ` UNIV"}\\ |
|
151 |
\end{supertabular} |
|
152 |
||
153 |
||
154 |
\section{Fun} |
|
155 |
||
32933 | 156 |
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
30293 | 157 |
@{const "Fun.id"} & @{typeof Fun.id}\\ |
32933 | 158 |
@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\ |
30293 | 159 |
@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\ |
160 |
@{const "Fun.inj"} & @{typeof Fun.inj}\\ |
|
161 |
@{const "Fun.surj"} & @{typeof Fun.surj}\\ |
|
162 |
@{const "Fun.bij"} & @{typeof Fun.bij}\\ |
|
163 |
@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\ |
|
164 |
@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ |
|
165 |
\end{supertabular} |
|
166 |
||
167 |
\subsubsection*{Syntax} |
|
168 |
||
169 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
170 |
@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ |
|
171 |
@{text"f(x\<^isub>1:=y\<^isub>1,\<dots>,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\<dots>(x\<^isub>n:=y\<^isub>n)"}\\ |
|
172 |
\end{tabular} |
|
173 |
||
174 |
||
33019 | 175 |
\section{Hilbert\_Choice} |
176 |
||
177 |
Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}. |
|
178 |
\smallskip |
|
179 |
||
180 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
33057 | 181 |
@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"} |
33019 | 182 |
\end{tabular} |
183 |
||
184 |
\subsubsection*{Syntax} |
|
185 |
||
186 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
33057 | 187 |
@{term inv} & @{term[source]"inv_into UNIV"} |
33019 | 188 |
\end{tabular} |
189 |
||
30293 | 190 |
\section{Fixed Points} |
191 |
||
192 |
Theory: @{theory Inductive}. |
|
193 |
||
194 |
Least and greatest fixed points in a complete lattice @{typ 'a}: |
|
195 |
||
196 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
197 |
@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ |
|
198 |
@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ |
|
199 |
\end{tabular} |
|
200 |
||
201 |
Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices. |
|
202 |
||
203 |
\section{Sum\_Type} |
|
204 |
||
205 |
Type constructor @{text"+"}. |
|
206 |
||
207 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
208 |
@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ |
|
209 |
@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ |
|
210 |
@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"} |
|
211 |
\end{tabular} |
|
212 |
||
213 |
||
214 |
\section{Product\_Type} |
|
215 |
||
216 |
Types @{typ unit} and @{text"\<times>"}. |
|
217 |
||
218 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
219 |
@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ |
|
220 |
@{const Pair} & @{typeof Pair}\\ |
|
221 |
@{const fst} & @{typeof fst}\\ |
|
222 |
@{const snd} & @{typeof snd}\\ |
|
223 |
@{const split} & @{typeof split}\\ |
|
224 |
@{const curry} & @{typeof curry}\\ |
|
225 |
@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\ |
|
226 |
\end{supertabular} |
|
227 |
||
228 |
\subsubsection*{Syntax} |
|
229 |
||
30440 | 230 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} |
30293 | 231 |
@{term"Pair a b"} & @{term[source]"Pair a b"}\\ |
232 |
@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\ |
|
30440 | 233 |
@{term"A <*> B"} & @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$) |
30293 | 234 |
\end{tabular} |
235 |
||
236 |
Pairs may be nested. Nesting to the right is printed as a tuple, |
|
30440 | 237 |
e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{@{text"(a, (b, c))"}.} |
30293 | 238 |
Pattern matching with pairs and tuples extends to all binders, |
30440 | 239 |
e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc. |
30293 | 240 |
|
241 |
||
242 |
\section{Relation} |
|
243 |
||
47187 | 244 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
30293 | 245 |
@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\ |
47682 | 246 |
@{const Relation.relcomp} & @{term_type_only Relation.relcomp "('a*'b)set\<Rightarrow>('b*'c)set\<Rightarrow>('a*'c)set"}\\ |
30293 | 247 |
@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\ |
248 |
@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\ |
|
249 |
@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\ |
|
250 |
@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\ |
|
251 |
@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\ |
|
252 |
@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\ |
|
253 |
@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\ |
|
254 |
@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ |
|
255 |
@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\ |
|
256 |
@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\ |
|
257 |
@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\ |
|
258 |
@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\ |
|
259 |
@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\ |
|
260 |
@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ |
|
30440 | 261 |
@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\ |
47187 | 262 |
\end{tabular} |
30293 | 263 |
|
264 |
\subsubsection*{Syntax} |
|
265 |
||
30440 | 266 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
267 |
@{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$) |
|
30293 | 268 |
\end{tabular} |
47187 | 269 |
\medskip |
270 |
||
271 |
\noindent |
|
47189
e9a3dd1c4cf9
improved robustness with new antiquoation by Makarius
nipkow
parents:
47187
diff
changeset
|
272 |
Type synonym \ @{typ"'a rel"} @{text"="} @{expanded_typ "'a rel"} |
30293 | 273 |
|
274 |
\section{Equiv\_Relations} |
|
275 |
||
276 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
277 |
@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\ |
|
278 |
@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\ |
|
279 |
@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\ |
|
280 |
@{const Equiv_Relations.congruent2} & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>('a\<Rightarrow>'b\<Rightarrow>'c)\<Rightarrow>bool"}\\ |
|
281 |
%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ |
|
282 |
\end{supertabular} |
|
283 |
||
284 |
\subsubsection*{Syntax} |
|
285 |
||
286 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
287 |
@{term"congruent r f"} & @{term[source]"congruent r f"}\\ |
|
288 |
@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\ |
|
289 |
\end{tabular} |
|
290 |
||
291 |
||
292 |
\section{Transitive\_Closure} |
|
293 |
||
294 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
295 |
@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
296 |
@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
297 |
@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
45618 | 298 |
@{const Transitive_Closure.acyclic} & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\<Rightarrow>bool"}\\ |
30988 | 299 |
@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\ |
30293 | 300 |
\end{tabular} |
301 |
||
302 |
\subsubsection*{Syntax} |
|
303 |
||
30440 | 304 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
305 |
@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\verb$^*$)\\ |
|
306 |
@{term"trancl r"} & @{term[source]"trancl r"} & (\verb$^+$)\\ |
|
307 |
@{term"reflcl r"} & @{term[source]"reflcl r"} & (\verb$^=$) |
|
30293 | 308 |
\end{tabular} |
309 |
||
310 |
||
311 |
\section{Algebra} |
|
312 |
||
35061 | 313 |
Theories @{theory Groups}, @{theory Rings}, @{theory Fields} and @{theory |
30440 | 314 |
Divides} define a large collection of classes describing common algebraic |
315 |
structures from semigroups up to fields. Everything is done in terms of |
|
316 |
overloaded operators: |
|
317 |
||
318 |
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
|
319 |
@{text "0"} & @{typeof zero}\\ |
|
320 |
@{text "1"} & @{typeof one}\\ |
|
321 |
@{const plus} & @{typeof plus}\\ |
|
322 |
@{const minus} & @{typeof minus}\\ |
|
323 |
@{const uminus} & @{typeof uminus} & (\verb$-$)\\ |
|
324 |
@{const times} & @{typeof times}\\ |
|
325 |
@{const inverse} & @{typeof inverse}\\ |
|
326 |
@{const divide} & @{typeof divide}\\ |
|
327 |
@{const abs} & @{typeof abs}\\ |
|
328 |
@{const sgn} & @{typeof sgn}\\ |
|
329 |
@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\ |
|
330 |
@{const div_class.div} & @{typeof "div_class.div"}\\ |
|
331 |
@{const div_class.mod} & @{typeof "div_class.mod"}\\ |
|
332 |
\end{supertabular} |
|
333 |
||
334 |
\subsubsection*{Syntax} |
|
335 |
||
336 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
337 |
@{term"abs x"} & @{term[source]"abs x"} |
|
338 |
\end{tabular} |
|
30293 | 339 |
|
340 |
||
341 |
\section{Nat} |
|
342 |
||
343 |
@{datatype nat} |
|
344 |
\bigskip |
|
345 |
||
346 |
\begin{tabular}{@ {} lllllll @ {}} |
|
347 |
@{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
348 |
@{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
349 |
@{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
47187 | 350 |
@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
30293 | 351 |
@{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}& |
352 |
@{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}& |
|
353 |
@{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\ |
|
354 |
@{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} & |
|
355 |
@{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} & |
|
356 |
@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
357 |
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
358 |
@{term "Min :: nat set \<Rightarrow> nat"} & |
|
359 |
@{term "Max :: nat set \<Rightarrow> nat"}\\ |
|
360 |
\end{tabular} |
|
361 |
||
362 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
30988 | 363 |
@{const Nat.of_nat} & @{typeof Nat.of_nat}\\ |
364 |
@{term "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} & |
|
365 |
@{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} |
|
30293 | 366 |
\end{tabular} |
367 |
||
368 |
\section{Int} |
|
369 |
||
370 |
Type @{typ int} |
|
371 |
\bigskip |
|
372 |
||
373 |
\begin{tabular}{@ {} llllllll @ {}} |
|
374 |
@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
375 |
@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
376 |
@{term "uminus :: int \<Rightarrow> int"} & |
|
377 |
@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
378 |
@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} & |
|
379 |
@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}& |
|
380 |
@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}& |
|
381 |
@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\ |
|
382 |
@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} & |
|
383 |
@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} & |
|
384 |
@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
385 |
@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
386 |
@{term "Min :: int set \<Rightarrow> int"} & |
|
387 |
@{term "Max :: int set \<Rightarrow> int"}\\ |
|
388 |
@{term "abs :: int \<Rightarrow> int"} & |
|
389 |
@{term "sgn :: int \<Rightarrow> int"}\\ |
|
390 |
\end{tabular} |
|
391 |
||
30440 | 392 |
\begin{tabular}{@ {} l @ {~::~} l l @ {}} |
30293 | 393 |
@{const Int.nat} & @{typeof Int.nat}\\ |
394 |
@{const Int.of_int} & @{typeof Int.of_int}\\ |
|
30440 | 395 |
@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\verb$Ints$) |
30293 | 396 |
\end{tabular} |
397 |
||
398 |
\subsubsection*{Syntax} |
|
399 |
||
400 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
401 |
@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\ |
|
402 |
\end{tabular} |
|
403 |
||
404 |
||
30401 | 405 |
\section{Finite\_Set} |
406 |
||
407 |
||
408 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
409 |
@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\ |
|
410 |
@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\ |
|
411 |
@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\ |
|
412 |
@{const Finite_Set.fold_image} & @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\ |
|
35805 | 413 |
@{const Big_Operators.setsum} & @{term_type_only Big_Operators.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\ |
414 |
@{const Big_Operators.setprod} & @{term_type_only Big_Operators.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\ |
|
30401 | 415 |
\end{supertabular} |
416 |
||
417 |
||
418 |
\subsubsection*{Syntax} |
|
419 |
||
30440 | 420 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
421 |
@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\verb$SUM$)\\ |
|
30401 | 422 |
@{term"setsum (%x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\ |
423 |
@{term[source]"\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\ |
|
30440 | 424 |
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}} & (\verb$PROD$)\\ |
30401 | 425 |
\end{supertabular} |
426 |
||
427 |
||
30293 | 428 |
\section{Wellfounded} |
429 |
||
430 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
431 |
@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\ |
|
432 |
@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\ |
|
433 |
@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\ |
|
434 |
@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\ |
|
435 |
@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
436 |
@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ |
|
437 |
@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ |
|
438 |
\end{supertabular} |
|
439 |
||
440 |
||
30384 | 441 |
\section{SetInterval} |
30321 | 442 |
|
443 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
30370 | 444 |
@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\ |
445 |
@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\ |
|
446 |
@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\ |
|
447 |
@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\ |
|
448 |
@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ |
|
449 |
@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ |
|
450 |
@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ |
|
451 |
@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ |
|
30321 | 452 |
\end{supertabular} |
453 |
||
454 |
\subsubsection*{Syntax} |
|
455 |
||
456 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
457 |
@{term "lessThan y"} & @{term[source] "lessThan y"}\\ |
|
458 |
@{term "atMost y"} & @{term[source] "atMost y"}\\ |
|
459 |
@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\ |
|
460 |
@{term "atLeast x"} & @{term[source] "atLeast x"}\\ |
|
461 |
@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\ |
|
462 |
@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\ |
|
463 |
@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\ |
|
464 |
@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\ |
|
30370 | 465 |
@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\ |
466 |
@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\ |
|
467 |
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\ |
|
30321 | 468 |
@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\ |
30370 | 469 |
@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\ |
30386 | 470 |
@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\ |
471 |
@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\ |
|
30372 | 472 |
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\ |
30321 | 473 |
\end{supertabular} |
474 |
||
475 |
||
30293 | 476 |
\section{Power} |
477 |
||
478 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
479 |
@{const Power.power} & @{typeof Power.power} |
|
480 |
\end{tabular} |
|
481 |
||
482 |
||
483 |
\section{Option} |
|
484 |
||
485 |
@{datatype option} |
|
486 |
\bigskip |
|
487 |
||
488 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
489 |
@{const Option.the} & @{typeof Option.the}\\ |
|
490 |
@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\ |
|
41532 | 491 |
@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}\\ |
492 |
@{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"} |
|
30293 | 493 |
\end{tabular} |
494 |
||
495 |
\section{List} |
|
496 |
||
497 |
@{datatype list} |
|
498 |
\bigskip |
|
499 |
||
500 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
501 |
@{const List.append} & @{typeof List.append}\\ |
|
502 |
@{const List.butlast} & @{typeof List.butlast}\\ |
|
503 |
@{const List.concat} & @{typeof List.concat}\\ |
|
504 |
@{const List.distinct} & @{typeof List.distinct}\\ |
|
505 |
@{const List.drop} & @{typeof List.drop}\\ |
|
506 |
@{const List.dropWhile} & @{typeof List.dropWhile}\\ |
|
507 |
@{const List.filter} & @{typeof List.filter}\\ |
|
47187 | 508 |
@{const List.find} & @{typeof List.find}\\ |
46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
45618
diff
changeset
|
509 |
@{const List.fold} & @{typeof List.fold}\\ |
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
45618
diff
changeset
|
510 |
@{const List.foldr} & @{typeof List.foldr}\\ |
30293 | 511 |
@{const List.foldl} & @{typeof List.foldl}\\ |
512 |
@{const List.hd} & @{typeof List.hd}\\ |
|
513 |
@{const List.last} & @{typeof List.last}\\ |
|
514 |
@{const List.length} & @{typeof List.length}\\ |
|
515 |
@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
516 |
@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
517 |
@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\ |
|
518 |
@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
46488 | 519 |
@{const List.listrel} & @{term_type_only List.listrel "('a*'b)set\<Rightarrow>('a list * 'b list)set"}\\ |
40272 | 520 |
@{const List.listrel1} & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
30293 | 521 |
@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\ |
522 |
@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\ |
|
523 |
@{const List.listsum} & @{typeof List.listsum}\\ |
|
524 |
@{const List.list_all2} & @{typeof List.list_all2}\\ |
|
525 |
@{const List.list_update} & @{typeof List.list_update}\\ |
|
526 |
@{const List.map} & @{typeof List.map}\\ |
|
527 |
@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\ |
|
32933 | 528 |
@{const List.nth} & @{typeof List.nth}\\ |
30293 | 529 |
@{const List.remdups} & @{typeof List.remdups}\\ |
530 |
@{const List.removeAll} & @{typeof List.removeAll}\\ |
|
531 |
@{const List.remove1} & @{typeof List.remove1}\\ |
|
532 |
@{const List.replicate} & @{typeof List.replicate}\\ |
|
533 |
@{const List.rev} & @{typeof List.rev}\\ |
|
534 |
@{const List.rotate} & @{typeof List.rotate}\\ |
|
535 |
@{const List.rotate1} & @{typeof List.rotate1}\\ |
|
536 |
@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\ |
|
537 |
@{const List.sort} & @{typeof List.sort}\\ |
|
538 |
@{const List.sorted} & @{typeof List.sorted}\\ |
|
539 |
@{const List.splice} & @{typeof List.splice}\\ |
|
540 |
@{const List.sublist} & @{typeof List.sublist}\\ |
|
541 |
@{const List.take} & @{typeof List.take}\\ |
|
542 |
@{const List.takeWhile} & @{typeof List.takeWhile}\\ |
|
543 |
@{const List.tl} & @{typeof List.tl}\\ |
|
544 |
@{const List.upt} & @{typeof List.upt}\\ |
|
545 |
@{const List.upto} & @{typeof List.upto}\\ |
|
546 |
@{const List.zip} & @{typeof List.zip}\\ |
|
547 |
\end{supertabular} |
|
548 |
||
549 |
\subsubsection*{Syntax} |
|
550 |
||
551 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
552 |
@{text"[x\<^isub>1,\<dots>,x\<^isub>n]"} & @{text"x\<^isub>1 # \<dots> # x\<^isub>n # []"}\\ |
|
553 |
@{term"[m..<n]"} & @{term[source]"upt m n"}\\ |
|
554 |
@{term"[i..j]"} & @{term[source]"upto i j"}\\ |
|
555 |
@{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\ |
|
556 |
@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\ |
|
557 |
@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ |
|
558 |
@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\ |
|
559 |
\end{supertabular} |
|
560 |
\medskip |
|
561 |
||
30440 | 562 |
List comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each |
563 |
qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \<leftarrow> e"}} or a |
|
30293 | 564 |
guard, i.e.\ boolean expression. |
565 |
||
566 |
\section{Map} |
|
567 |
||
568 |
Maps model partial functions and are often used as finite tables. However, |
|
569 |
the domain of a map may be infinite. |
|
570 |
||
571 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
572 |
@{const Map.empty} & @{typeof Map.empty}\\ |
|
573 |
@{const Map.map_add} & @{typeof Map.map_add}\\ |
|
574 |
@{const Map.map_comp} & @{typeof Map.map_comp}\\ |
|
575 |
@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\ |
|
576 |
@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\ |
|
577 |
@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\ |
|
578 |
@{const Map.map_le} & @{typeof Map.map_le}\\ |
|
579 |
@{const Map.map_of} & @{typeof Map.map_of}\\ |
|
580 |
@{const Map.map_upds} & @{typeof Map.map_upds}\\ |
|
581 |
\end{supertabular} |
|
582 |
||
583 |
\subsubsection*{Syntax} |
|
584 |
||
585 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
30403 | 586 |
@{term"Map.empty"} & @{term"\<lambda>x. None"}\\ |
30293 | 587 |
@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ |
588 |
@{text"m(x\<^isub>1\<mapsto>y\<^isub>1,\<dots>,x\<^isub>n\<mapsto>y\<^isub>n)"} & @{text[source]"m(x\<^isub>1\<mapsto>y\<^isub>1)\<dots>(x\<^isub>n\<mapsto>y\<^isub>n)"}\\ |
|
30440 | 589 |
@{text"[x\<^isub>1\<mapsto>y\<^isub>1,\<dots>,x\<^isub>n\<mapsto>y\<^isub>n]"} & @{text[source]"Map.empty(x\<^isub>1\<mapsto>y\<^isub>1,\<dots>,x\<^isub>n\<mapsto>y\<^isub>n)"}\\ |
30293 | 590 |
@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ |
591 |
\end{tabular} |
|
592 |
||
593 |
*} |
|
594 |
(*<*) |
|
595 |
end |
|
596 |
(*>*) |