author | nipkow |
Wed, 03 Oct 2018 11:09:08 +0200 | |
changeset 69108 | e2780bb26395 |
parent 69065 | 440f7a575760 |
child 69313 | b021008c5397 |
permissions | -rw-r--r-- |
30293 | 1 |
(*<*) |
30401 | 2 |
theory Main_Doc |
30293 | 3 |
imports Main |
4 |
begin |
|
5 |
||
61996 | 6 |
setup \<open> |
67463 | 7 |
Thy_Output.antiquotation_pretty_source @{binding term_type_only} (Args.term -- Args.typ_abbrev) |
8 |
(fn ctxt => fn (t, T) => |
|
43564
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"; |
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67463
diff
changeset
|
11 |
Syntax.pretty_typ ctxt T)) |
61996 | 12 |
\<close> |
13 |
setup \<open> |
|
67463 | 14 |
Thy_Output.antiquotation_pretty_source @{binding expanded_typ} Args.typ |
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67463
diff
changeset
|
15 |
Syntax.pretty_typ |
61996 | 16 |
\<close> |
30293 | 17 |
(*>*) |
61996 | 18 |
text\<open> |
30293 | 19 |
|
20 |
\begin{abstract} |
|
68224 | 21 |
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. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see \<^url>\<open>https://isabelle.in.tum.de/library/HOL\<close>. |
30293 | 22 |
\end{abstract} |
23 |
||
50581 | 24 |
\section*{HOL} |
30293 | 25 |
|
63902 | 26 |
The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop "\<not> P"}, @{prop"P \<and> Q"}, |
27 |
@{prop "P \<or> Q"}, @{prop "P \<longrightarrow> Q"}, @{prop "\<forall>x. P"}, @{prop "\<exists>x. P"}, @{prop"\<exists>! x. P"}, |
|
28 |
@{term"THE x. P"}. |
|
61996 | 29 |
\<^smallskip> |
30440 | 30 |
|
31 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
32 |
@{const HOL.undefined} & @{typeof HOL.undefined}\\ |
|
33 |
@{const HOL.default} & @{typeof HOL.default}\\ |
|
34 |
\end{tabular} |
|
35 |
||
36 |
\subsubsection*{Syntax} |
|
30293 | 37 |
|
30440 | 38 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
63902 | 39 |
@{term"\<not> (x = y)"} & @{term[source]"\<not> (x = y)"} & (\<^verbatim>\<open>~=\<close>)\\ |
30440 | 40 |
@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\ |
41 |
@{term"If x y z"} & @{term[source]"If x y z"}\\ |
|
63902 | 42 |
@{term"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"} & @{term[source]"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"}\\ |
30440 | 43 |
\end{supertabular} |
44 |
||
45 |
||
50581 | 46 |
\section*{Orderings} |
30440 | 47 |
|
48 |
A collection of classes defining basic orderings: |
|
49 |
preorder, partial order, linear order, dense linear order and wellorder. |
|
61996 | 50 |
\<^smallskip> |
30293 | 51 |
|
30425 | 52 |
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
61996 | 53 |
@{const Orderings.less_eq} & @{typeof Orderings.less_eq} & (\<^verbatim>\<open><=\<close>)\\ |
35277 | 54 |
@{const Orderings.less} & @{typeof Orderings.less}\\ |
30440 | 55 |
@{const Orderings.Least} & @{typeof Orderings.Least}\\ |
65964 | 56 |
@{const Orderings.Greatest} & @{typeof Orderings.Greatest}\\ |
30440 | 57 |
@{const Orderings.min} & @{typeof Orderings.min}\\ |
58 |
@{const Orderings.max} & @{typeof Orderings.max}\\ |
|
59 |
@{const[source] top} & @{typeof Orderings.top}\\ |
|
60 |
@{const[source] bot} & @{typeof Orderings.bot}\\ |
|
61 |
@{const Orderings.mono} & @{typeof Orderings.mono}\\ |
|
62 |
@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\ |
|
30293 | 63 |
\end{supertabular} |
64 |
||
65 |
\subsubsection*{Syntax} |
|
66 |
||
30440 | 67 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
61996 | 68 |
@{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\<^verbatim>\<open>>=\<close>)\\ |
30293 | 69 |
@{term[source]"x > y"} & @{term"x > y"}\\ |
63902 | 70 |
@{term "\<forall>x\<le>y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\ |
71 |
@{term "\<exists>x\<le>y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\ |
|
30440 | 72 |
\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ |
63902 | 73 |
@{term "LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\ |
65964 | 74 |
@{term "GREATEST x. P"} & @{term[source]"Greatest (\<lambda>x. P)"}\\ |
30293 | 75 |
\end{supertabular} |
76 |
||
30401 | 77 |
|
50581 | 78 |
\section*{Lattices} |
30401 | 79 |
|
80 |
Classes semilattice, lattice, distributive lattice and complete lattice (the |
|
68484 | 81 |
latter in theory @{theory HOL.Set}). |
30401 | 82 |
|
83 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
84 |
@{const Lattices.inf} & @{typeof Lattices.inf}\\ |
|
85 |
@{const Lattices.sup} & @{typeof Lattices.sup}\\ |
|
44969 | 86 |
@{const Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\ |
87 |
@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \<Rightarrow> 'a::Sup"}\\ |
|
30401 | 88 |
\end{tabular} |
89 |
||
90 |
\subsubsection*{Syntax} |
|
91 |
||
61996 | 92 |
Available by loading theory \<open>Lattice_Syntax\<close> in directory \<open>Library\<close>. |
30401 | 93 |
|
94 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
95 |
@{text[source]"x \<sqsubseteq> y"} & @{term"x \<le> y"}\\ |
|
96 |
@{text[source]"x \<sqsubset> y"} & @{term"x < y"}\\ |
|
97 |
@{text[source]"x \<sqinter> y"} & @{term"inf x y"}\\ |
|
98 |
@{text[source]"x \<squnion> y"} & @{term"sup x y"}\\ |
|
62204 | 99 |
@{text[source]"\<Sqinter>A"} & @{term"Inf A"}\\ |
100 |
@{text[source]"\<Squnion>A"} & @{term"Sup A"}\\ |
|
30440 | 101 |
@{text[source]"\<top>"} & @{term[source] top}\\ |
102 |
@{text[source]"\<bottom>"} & @{term[source] bot}\\ |
|
30401 | 103 |
\end{supertabular} |
104 |
||
105 |
||
50581 | 106 |
\section*{Set} |
30293 | 107 |
|
30425 | 108 |
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
30370 | 109 |
@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ |
32142 | 110 |
@{const Set.insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\ |
30293 | 111 |
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\ |
61996 | 112 |
@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\<^verbatim>\<open>:\<close>)\\ |
113 |
@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Un\<close>)\\ |
|
114 |
@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Int\<close>)\\ |
|
30293 | 115 |
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
116 |
@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
|
117 |
@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\ |
|
118 |
@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\ |
|
119 |
@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\ |
|
120 |
@{const UNIV} & @{term_type_only UNIV "'a set"}\\ |
|
121 |
@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\ |
|
122 |
@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ |
|
123 |
@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ |
|
124 |
\end{supertabular} |
|
125 |
||
126 |
\subsubsection*{Syntax} |
|
127 |
||
30425 | 128 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
61996 | 129 |
\<open>{a\<^sub>1,\<dots>,a\<^sub>n}\<close> & \<open>insert a\<^sub>1 (\<dots> (insert a\<^sub>n {})\<dots>)\<close>\\ |
63902 | 130 |
@{term "a \<notin> A"} & @{term[source]"\<not>(x \<in> A)"}\\ |
131 |
@{term "A \<subseteq> B"} & @{term[source]"A \<le> B"}\\ |
|
132 |
@{term "A \<subset> B"} & @{term[source]"A < B"}\\ |
|
30293 | 133 |
@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\ |
134 |
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\ |
|
63902 | 135 |
@{term "{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\ |
61996 | 136 |
\<open>{t | x\<^sub>1 \<dots> x\<^sub>n. P}\<close> & \<open>{v. \<exists>x\<^sub>1 \<dots> x\<^sub>n. v = t \<and> P}\<close>\\ |
61995
74709e9c4f17
clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms;
wenzelm
parents:
61943
diff
changeset
|
137 |
@{term[source]"\<Union>x\<in>I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\ |
74709e9c4f17
clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms;
wenzelm
parents:
61943
diff
changeset
|
138 |
@{term[source]"\<Union>x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\ |
74709e9c4f17
clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms;
wenzelm
parents:
61943
diff
changeset
|
139 |
@{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\ |
74709e9c4f17
clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms;
wenzelm
parents:
61943
diff
changeset
|
140 |
@{term[source]"\<Inter>x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\ |
63902 | 141 |
@{term "\<forall>x\<in>A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\ |
142 |
@{term "\<exists>x\<in>A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\ |
|
143 |
@{term "range f"} & @{term[source]"f ` UNIV"}\\ |
|
30293 | 144 |
\end{supertabular} |
145 |
||
146 |
||
50581 | 147 |
\section*{Fun} |
30293 | 148 |
|
32933 | 149 |
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
30293 | 150 |
@{const "Fun.id"} & @{typeof Fun.id}\\ |
32933 | 151 |
@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\ |
30293 | 152 |
@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\ |
153 |
@{const "Fun.inj"} & @{typeof Fun.inj}\\ |
|
154 |
@{const "Fun.surj"} & @{typeof Fun.surj}\\ |
|
155 |
@{const "Fun.bij"} & @{typeof Fun.bij}\\ |
|
156 |
@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\ |
|
157 |
@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ |
|
158 |
\end{supertabular} |
|
159 |
||
160 |
\subsubsection*{Syntax} |
|
161 |
||
162 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
163 |
@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ |
|
61996 | 164 |
\<open>f(x\<^sub>1:=y\<^sub>1,\<dots>,x\<^sub>n:=y\<^sub>n)\<close> & \<open>f(x\<^sub>1:=y\<^sub>1)\<dots>(x\<^sub>n:=y\<^sub>n)\<close>\\ |
30293 | 165 |
\end{tabular} |
166 |
||
167 |
||
50581 | 168 |
\section*{Hilbert\_Choice} |
33019 | 169 |
|
170 |
Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}. |
|
61996 | 171 |
\<^smallskip> |
33019 | 172 |
|
173 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
33057 | 174 |
@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"} |
33019 | 175 |
\end{tabular} |
176 |
||
177 |
\subsubsection*{Syntax} |
|
178 |
||
179 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
33057 | 180 |
@{term inv} & @{term[source]"inv_into UNIV"} |
33019 | 181 |
\end{tabular} |
182 |
||
50581 | 183 |
\section*{Fixed Points} |
30293 | 184 |
|
68484 | 185 |
Theory: @{theory HOL.Inductive}. |
30293 | 186 |
|
187 |
Least and greatest fixed points in a complete lattice @{typ 'a}: |
|
188 |
||
189 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
190 |
@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ |
|
191 |
@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ |
|
192 |
\end{tabular} |
|
193 |
||
194 |
Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices. |
|
195 |
||
50581 | 196 |
\section*{Sum\_Type} |
30293 | 197 |
|
61996 | 198 |
Type constructor \<open>+\<close>. |
30293 | 199 |
|
200 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
201 |
@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ |
|
202 |
@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ |
|
203 |
@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"} |
|
204 |
\end{tabular} |
|
205 |
||
206 |
||
50581 | 207 |
\section*{Product\_Type} |
30293 | 208 |
|
61996 | 209 |
Types @{typ unit} and \<open>\<times>\<close>. |
30293 | 210 |
|
211 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
212 |
@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ |
|
213 |
@{const Pair} & @{typeof Pair}\\ |
|
214 |
@{const fst} & @{typeof fst}\\ |
|
215 |
@{const snd} & @{typeof snd}\\ |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
60352
diff
changeset
|
216 |
@{const case_prod} & @{typeof case_prod}\\ |
30293 | 217 |
@{const curry} & @{typeof curry}\\ |
218 |
@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\ |
|
219 |
\end{supertabular} |
|
220 |
||
221 |
\subsubsection*{Syntax} |
|
222 |
||
30440 | 223 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} |
63902 | 224 |
@{term "Pair a b"} & @{term[source]"Pair a b"}\\ |
225 |
@{term "case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\ |
|
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63902
diff
changeset
|
226 |
@{term "A \<times> B"} & \<open>Sigma A (\<lambda>\<^latex>\<open>\_\<close>. B)\<close> |
30293 | 227 |
\end{tabular} |
228 |
||
229 |
Pairs may be nested. Nesting to the right is printed as a tuple, |
|
63902 | 230 |
e.g.\ \mbox{@{term "(a,b,c)"}} is really \mbox{\<open>(a, (b, c))\<close>.} |
30293 | 231 |
Pattern matching with pairs and tuples extends to all binders, |
63902 | 232 |
e.g.\ \mbox{@{prop "\<forall>(x,y)\<in>A. P"},} @{term "{(x,y). P}"}, etc. |
30293 | 233 |
|
234 |
||
50581 | 235 |
\section*{Relation} |
30293 | 236 |
|
47187 | 237 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
30293 | 238 |
@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\ |
47682 | 239 |
@{const Relation.relcomp} & @{term_type_only Relation.relcomp "('a*'b)set\<Rightarrow>('b*'c)set\<Rightarrow>('a*'c)set"}\\ |
30293 | 240 |
@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\ |
241 |
@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\ |
|
242 |
@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\ |
|
243 |
@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\ |
|
244 |
@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\ |
|
245 |
@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\ |
|
246 |
@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\ |
|
247 |
@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ |
|
248 |
@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\ |
|
249 |
@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\ |
|
250 |
@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\ |
|
251 |
@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\ |
|
252 |
@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\ |
|
253 |
@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ |
|
30440 | 254 |
@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\ |
47187 | 255 |
\end{tabular} |
30293 | 256 |
|
257 |
\subsubsection*{Syntax} |
|
258 |
||
30440 | 259 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
61996 | 260 |
@{term"converse r"} & @{term[source]"converse r"} & (\<^verbatim>\<open>^-1\<close>) |
30293 | 261 |
\end{tabular} |
61996 | 262 |
\<^medskip> |
47187 | 263 |
|
264 |
\noindent |
|
61996 | 265 |
Type synonym \ @{typ"'a rel"} \<open>=\<close> @{expanded_typ "'a rel"} |
30293 | 266 |
|
50581 | 267 |
\section*{Equiv\_Relations} |
30293 | 268 |
|
269 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
270 |
@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\ |
|
271 |
@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\ |
|
272 |
@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\ |
|
273 |
@{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"}\\ |
|
274 |
%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ |
|
275 |
\end{supertabular} |
|
276 |
||
277 |
\subsubsection*{Syntax} |
|
278 |
||
279 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
280 |
@{term"congruent r f"} & @{term[source]"congruent r f"}\\ |
|
281 |
@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\ |
|
282 |
\end{tabular} |
|
283 |
||
284 |
||
50581 | 285 |
\section*{Transitive\_Closure} |
30293 | 286 |
|
287 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
288 |
@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
289 |
@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
290 |
@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
45618 | 291 |
@{const Transitive_Closure.acyclic} & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\<Rightarrow>bool"}\\ |
67399 | 292 |
@{const compower} & @{term_type_only "(^^) :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\ |
30293 | 293 |
\end{tabular} |
294 |
||
295 |
\subsubsection*{Syntax} |
|
296 |
||
30440 | 297 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
61996 | 298 |
@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\<^verbatim>\<open>^*\<close>)\\ |
299 |
@{term"trancl r"} & @{term[source]"trancl r"} & (\<^verbatim>\<open>^+\<close>)\\ |
|
300 |
@{term"reflcl r"} & @{term[source]"reflcl r"} & (\<^verbatim>\<open>^=\<close>) |
|
30293 | 301 |
\end{tabular} |
302 |
||
303 |
||
50581 | 304 |
\section*{Algebra} |
30293 | 305 |
|
68484 | 306 |
Theories @{theory HOL.Groups}, @{theory HOL.Rings}, @{theory HOL.Fields} and @{theory |
307 |
HOL.Divides} define a large collection of classes describing common algebraic |
|
30440 | 308 |
structures from semigroups up to fields. Everything is done in terms of |
309 |
overloaded operators: |
|
310 |
||
311 |
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
|
61996 | 312 |
\<open>0\<close> & @{typeof zero}\\ |
313 |
\<open>1\<close> & @{typeof one}\\ |
|
30440 | 314 |
@{const plus} & @{typeof plus}\\ |
315 |
@{const minus} & @{typeof minus}\\ |
|
61996 | 316 |
@{const uminus} & @{typeof uminus} & (\<^verbatim>\<open>-\<close>)\\ |
30440 | 317 |
@{const times} & @{typeof times}\\ |
318 |
@{const inverse} & @{typeof inverse}\\ |
|
319 |
@{const divide} & @{typeof divide}\\ |
|
320 |
@{const abs} & @{typeof abs}\\ |
|
321 |
@{const sgn} & @{typeof sgn}\\ |
|
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63935
diff
changeset
|
322 |
@{const Rings.dvd} & @{typeof Rings.dvd}\\ |
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63935
diff
changeset
|
323 |
@{const divide} & @{typeof divide}\\ |
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63935
diff
changeset
|
324 |
@{const modulo} & @{typeof modulo}\\ |
30440 | 325 |
\end{supertabular} |
326 |
||
327 |
\subsubsection*{Syntax} |
|
328 |
||
329 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
63902 | 330 |
@{term "\<bar>x\<bar>"} & @{term[source] "abs x"} |
30440 | 331 |
\end{tabular} |
30293 | 332 |
|
333 |
||
50581 | 334 |
\section*{Nat} |
30293 | 335 |
|
336 |
@{datatype nat} |
|
61996 | 337 |
\<^bigskip> |
30293 | 338 |
|
339 |
\begin{tabular}{@ {} lllllll @ {}} |
|
67399 | 340 |
@{term "(+) :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
341 |
@{term "(-) :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
69065 | 342 |
@{term "(*) :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
67399 | 343 |
@{term "(^) :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
344 |
@{term "(div) :: nat \<Rightarrow> nat \<Rightarrow> nat"}& |
|
345 |
@{term "(mod) :: nat \<Rightarrow> nat \<Rightarrow> nat"}& |
|
346 |
@{term "(dvd) :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\ |
|
347 |
@{term "(\<le>) :: nat \<Rightarrow> nat \<Rightarrow> bool"} & |
|
348 |
@{term "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool"} & |
|
30293 | 349 |
@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
350 |
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
351 |
@{term "Min :: nat set \<Rightarrow> nat"} & |
|
352 |
@{term "Max :: nat set \<Rightarrow> nat"}\\ |
|
353 |
\end{tabular} |
|
354 |
||
355 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
30988 | 356 |
@{const Nat.of_nat} & @{typeof Nat.of_nat}\\ |
67399 | 357 |
@{term "(^^) :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} & |
358 |
@{term_type_only "(^^) :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} |
|
30293 | 359 |
\end{tabular} |
360 |
||
50581 | 361 |
\section*{Int} |
30293 | 362 |
|
363 |
Type @{typ int} |
|
61996 | 364 |
\<^bigskip> |
30293 | 365 |
|
366 |
\begin{tabular}{@ {} llllllll @ {}} |
|
67399 | 367 |
@{term "(+) :: int \<Rightarrow> int \<Rightarrow> int"} & |
368 |
@{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
30293 | 369 |
@{term "uminus :: int \<Rightarrow> int"} & |
69065 | 370 |
@{term "(*) :: int \<Rightarrow> int \<Rightarrow> int"} & |
67399 | 371 |
@{term "(^) :: int \<Rightarrow> nat \<Rightarrow> int"} & |
372 |
@{term "(div) :: int \<Rightarrow> int \<Rightarrow> int"}& |
|
373 |
@{term "(mod) :: int \<Rightarrow> int \<Rightarrow> int"}& |
|
374 |
@{term "(dvd) :: int \<Rightarrow> int \<Rightarrow> bool"}\\ |
|
375 |
@{term "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"} & |
|
376 |
@{term "(<) :: int \<Rightarrow> int \<Rightarrow> bool"} & |
|
30293 | 377 |
@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} & |
378 |
@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
379 |
@{term "Min :: int set \<Rightarrow> int"} & |
|
380 |
@{term "Max :: int set \<Rightarrow> int"}\\ |
|
381 |
@{term "abs :: int \<Rightarrow> int"} & |
|
382 |
@{term "sgn :: int \<Rightarrow> int"}\\ |
|
383 |
\end{tabular} |
|
384 |
||
30440 | 385 |
\begin{tabular}{@ {} l @ {~::~} l l @ {}} |
30293 | 386 |
@{const Int.nat} & @{typeof Int.nat}\\ |
387 |
@{const Int.of_int} & @{typeof Int.of_int}\\ |
|
61996 | 388 |
@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\<^verbatim>\<open>Ints\<close>) |
30293 | 389 |
\end{tabular} |
390 |
||
391 |
\subsubsection*{Syntax} |
|
392 |
||
393 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
394 |
@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\ |
|
395 |
\end{tabular} |
|
396 |
||
397 |
||
50581 | 398 |
\section*{Finite\_Set} |
30401 | 399 |
|
400 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
401 |
@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\ |
|
63902 | 402 |
@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set \<Rightarrow> nat"}\\ |
30401 | 403 |
@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\ |
64281
bfc2e92d9b4c
restored document structure after theory refactoring
haftmann
parents:
64272
diff
changeset
|
404 |
\end{supertabular} |
bfc2e92d9b4c
restored document structure after theory refactoring
haftmann
parents:
64272
diff
changeset
|
405 |
|
bfc2e92d9b4c
restored document structure after theory refactoring
haftmann
parents:
64272
diff
changeset
|
406 |
|
65952 | 407 |
\section*{Lattices\_Big} |
408 |
||
409 |
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} |
|
410 |
@{const Lattices_Big.Min} & @{typeof Lattices_Big.Min}\\ |
|
411 |
@{const Lattices_Big.Max} & @{typeof Lattices_Big.Max}\\ |
|
412 |
@{const Lattices_Big.arg_min} & @{typeof Lattices_Big.arg_min}\\ |
|
65953 | 413 |
@{const Lattices_Big.is_arg_min} & @{typeof Lattices_Big.is_arg_min}\\ |
65954 | 414 |
@{const Lattices_Big.arg_max} & @{typeof Lattices_Big.arg_max}\\ |
415 |
@{const Lattices_Big.is_arg_max} & @{typeof Lattices_Big.is_arg_max}\\ |
|
65952 | 416 |
\end{supertabular} |
417 |
||
418 |
\subsubsection*{Syntax} |
|
419 |
||
420 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
|
421 |
@{term "ARG_MIN f x. P"} & @{term[source]"arg_min f (\<lambda>x. P)"}\\ |
|
65954 | 422 |
@{term "ARG_MAX f x. P"} & @{term[source]"arg_max f (\<lambda>x. P)"}\\ |
65952 | 423 |
\end{supertabular} |
424 |
||
425 |
||
64281
bfc2e92d9b4c
restored document structure after theory refactoring
haftmann
parents:
64272
diff
changeset
|
426 |
\section*{Groups\_Big} |
bfc2e92d9b4c
restored document structure after theory refactoring
haftmann
parents:
64272
diff
changeset
|
427 |
|
bfc2e92d9b4c
restored document structure after theory refactoring
haftmann
parents:
64272
diff
changeset
|
428 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
64267 | 429 |
@{const Groups_Big.sum} & @{term_type_only Groups_Big.sum "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_add"}\\ |
64272 | 430 |
@{const Groups_Big.prod} & @{term_type_only Groups_Big.prod "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_mult"}\\ |
30401 | 431 |
\end{supertabular} |
432 |
||
433 |
||
434 |
\subsubsection*{Syntax} |
|
435 |
||
30440 | 436 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} |
64267 | 437 |
@{term "sum (\<lambda>x. x) A"} & @{term[source]"sum (\<lambda>x. x) A"} & (\<^verbatim>\<open>SUM\<close>)\\ |
438 |
@{term "sum (\<lambda>x. t) A"} & @{term[source]"sum (\<lambda>x. t) A"}\\ |
|
63902 | 439 |
@{term[source] "\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\ |
61996 | 440 |
\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>} & (\<^verbatim>\<open>PROD\<close>)\\ |
30401 | 441 |
\end{supertabular} |
442 |
||
443 |
||
50581 | 444 |
\section*{Wellfounded} |
30293 | 445 |
|
446 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
447 |
@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\ |
|
448 |
@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\ |
|
449 |
@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\ |
|
450 |
@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\ |
|
451 |
@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
452 |
@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ |
|
453 |
@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ |
|
454 |
\end{supertabular} |
|
455 |
||
456 |
||
68484 | 457 |
\section*{Set\_Interval} % @{theory HOL.Set_Interval} |
30321 | 458 |
|
459 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
30370 | 460 |
@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\ |
461 |
@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\ |
|
462 |
@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\ |
|
463 |
@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\ |
|
464 |
@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ |
|
465 |
@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ |
|
466 |
@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ |
|
467 |
@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ |
|
30321 | 468 |
\end{supertabular} |
469 |
||
470 |
\subsubsection*{Syntax} |
|
471 |
||
472 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
473 |
@{term "lessThan y"} & @{term[source] "lessThan y"}\\ |
|
474 |
@{term "atMost y"} & @{term[source] "atMost y"}\\ |
|
475 |
@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\ |
|
476 |
@{term "atLeast x"} & @{term[source] "atLeast x"}\\ |
|
477 |
@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\ |
|
478 |
@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\ |
|
479 |
@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\ |
|
480 |
@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\ |
|
61995
74709e9c4f17
clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms;
wenzelm
parents:
61943
diff
changeset
|
481 |
@{term[source] "\<Union>i\<le>n. A"} & @{term[source] "\<Union>i \<in> {..n}. A"}\\ |
74709e9c4f17
clarified print modes: Isabelle symbols are used by default, but "latex" mode needs to be for some syntax forms;
wenzelm
parents:
61943
diff
changeset
|
482 |
@{term[source] "\<Union>i<n. A"} & @{term[source] "\<Union>i \<in> {..<n}. A"}\\ |
61996 | 483 |
\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Inter>\<close> instead of \<open>\<Union>\<close>}\\ |
64267 | 484 |
@{term "sum (\<lambda>x. t) {a..b}"} & @{term[source] "sum (\<lambda>x. t) {a..b}"}\\ |
485 |
@{term "sum (\<lambda>x. t) {a..<b}"} & @{term[source] "sum (\<lambda>x. t) {a..<b}"}\\ |
|
486 |
@{term "sum (\<lambda>x. t) {..b}"} & @{term[source] "sum (\<lambda>x. t) {..b}"}\\ |
|
487 |
@{term "sum (\<lambda>x. t) {..<b}"} & @{term[source] "sum (\<lambda>x. t) {..<b}"}\\ |
|
61996 | 488 |
\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>}\\ |
30321 | 489 |
\end{supertabular} |
490 |
||
491 |
||
50581 | 492 |
\section*{Power} |
30293 | 493 |
|
494 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
495 |
@{const Power.power} & @{typeof Power.power} |
|
496 |
\end{tabular} |
|
497 |
||
498 |
||
50581 | 499 |
\section*{Option} |
30293 | 500 |
|
501 |
@{datatype option} |
|
61996 | 502 |
\<^bigskip> |
30293 | 503 |
|
504 |
\begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
505 |
@{const Option.the} & @{typeof Option.the}\\ |
|
55466 | 506 |
@{const map_option} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\ |
55518
1ddb2edf5ceb
folded 'Option.set' into BNF-generated 'set_option'
blanchet
parents:
55466
diff
changeset
|
507 |
@{const set_option} & @{term_type_only set_option "'a option \<Rightarrow> 'a set"}\\ |
41532 | 508 |
@{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"} |
30293 | 509 |
\end{tabular} |
510 |
||
50581 | 511 |
\section*{List} |
30293 | 512 |
|
513 |
@{datatype list} |
|
61996 | 514 |
\<^bigskip> |
30293 | 515 |
|
516 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
517 |
@{const List.append} & @{typeof List.append}\\ |
|
518 |
@{const List.butlast} & @{typeof List.butlast}\\ |
|
519 |
@{const List.concat} & @{typeof List.concat}\\ |
|
520 |
@{const List.distinct} & @{typeof List.distinct}\\ |
|
521 |
@{const List.drop} & @{typeof List.drop}\\ |
|
522 |
@{const List.dropWhile} & @{typeof List.dropWhile}\\ |
|
523 |
@{const List.filter} & @{typeof List.filter}\\ |
|
47187 | 524 |
@{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
|
525 |
@{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
|
526 |
@{const List.foldr} & @{typeof List.foldr}\\ |
30293 | 527 |
@{const List.foldl} & @{typeof List.foldl}\\ |
528 |
@{const List.hd} & @{typeof List.hd}\\ |
|
529 |
@{const List.last} & @{typeof List.last}\\ |
|
530 |
@{const List.length} & @{typeof List.length}\\ |
|
531 |
@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
532 |
@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
533 |
@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\ |
|
534 |
@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
46488 | 535 |
@{const List.listrel} & @{term_type_only List.listrel "('a*'b)set\<Rightarrow>('a list * 'b list)set"}\\ |
40272 | 536 |
@{const List.listrel1} & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
30293 | 537 |
@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\ |
538 |
@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\ |
|
63884 | 539 |
@{const Groups_List.sum_list} & @{typeof Groups_List.sum_list}\\ |
540 |
@{const Groups_List.prod_list} & @{typeof Groups_List.prod_list}\\ |
|
30293 | 541 |
@{const List.list_all2} & @{typeof List.list_all2}\\ |
542 |
@{const List.list_update} & @{typeof List.list_update}\\ |
|
543 |
@{const List.map} & @{typeof List.map}\\ |
|
544 |
@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\ |
|
32933 | 545 |
@{const List.nth} & @{typeof List.nth}\\ |
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset
|
546 |
@{const List.nths} & @{typeof List.nths}\\ |
30293 | 547 |
@{const List.remdups} & @{typeof List.remdups}\\ |
548 |
@{const List.removeAll} & @{typeof List.removeAll}\\ |
|
549 |
@{const List.remove1} & @{typeof List.remove1}\\ |
|
550 |
@{const List.replicate} & @{typeof List.replicate}\\ |
|
551 |
@{const List.rev} & @{typeof List.rev}\\ |
|
552 |
@{const List.rotate} & @{typeof List.rotate}\\ |
|
553 |
@{const List.rotate1} & @{typeof List.rotate1}\\ |
|
554 |
@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\ |
|
69108 | 555 |
@{const List.shuffles} & @{typeof List.shuffles}\\ |
30293 | 556 |
@{const List.sort} & @{typeof List.sort}\\ |
557 |
@{const List.sorted} & @{typeof List.sorted}\\ |
|
66435 | 558 |
@{const List.sorted_wrt} & @{typeof List.sorted_wrt}\\ |
30293 | 559 |
@{const List.splice} & @{typeof List.splice}\\ |
560 |
@{const List.take} & @{typeof List.take}\\ |
|
561 |
@{const List.takeWhile} & @{typeof List.takeWhile}\\ |
|
562 |
@{const List.tl} & @{typeof List.tl}\\ |
|
563 |
@{const List.upt} & @{typeof List.upt}\\ |
|
564 |
@{const List.upto} & @{typeof List.upto}\\ |
|
565 |
@{const List.zip} & @{typeof List.zip}\\ |
|
566 |
\end{supertabular} |
|
567 |
||
568 |
\subsubsection*{Syntax} |
|
569 |
||
570 |
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
61996 | 571 |
\<open>[x\<^sub>1,\<dots>,x\<^sub>n]\<close> & \<open>x\<^sub>1 # \<dots> # x\<^sub>n # []\<close>\\ |
30293 | 572 |
@{term"[m..<n]"} & @{term[source]"upt m n"}\\ |
573 |
@{term"[i..j]"} & @{term[source]"upto i j"}\\ |
|
574 |
@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ |
|
575 |
@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\ |
|
576 |
\end{supertabular} |
|
61996 | 577 |
\<^medskip> |
30293 | 578 |
|
68364 | 579 |
Filter input syntax \<open>[pat \<leftarrow> e. b]\<close>, where |
580 |
\<open>pat\<close> is a tuple pattern, which stands for @{term "filter (\<lambda>pat. b) e"}. |
|
581 |
||
582 |
List comprehension input syntax: \<open>[e. q\<^sub>1, \<dots>, q\<^sub>n]\<close> where each |
|
61996 | 583 |
qualifier \<open>q\<^sub>i\<close> is either a generator \mbox{\<open>pat \<leftarrow> e\<close>} or a |
30293 | 584 |
guard, i.e.\ boolean expression. |
585 |
||
50581 | 586 |
\section*{Map} |
30293 | 587 |
|
588 |
Maps model partial functions and are often used as finite tables. However, |
|
589 |
the domain of a map may be infinite. |
|
590 |
||
591 |
\begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
592 |
@{const Map.empty} & @{typeof Map.empty}\\ |
|
593 |
@{const Map.map_add} & @{typeof Map.map_add}\\ |
|
594 |
@{const Map.map_comp} & @{typeof Map.map_comp}\\ |
|
595 |
@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\ |
|
596 |
@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\ |
|
597 |
@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\ |
|
598 |
@{const Map.map_le} & @{typeof Map.map_le}\\ |
|
599 |
@{const Map.map_of} & @{typeof Map.map_of}\\ |
|
600 |
@{const Map.map_upds} & @{typeof Map.map_upds}\\ |
|
601 |
\end{supertabular} |
|
602 |
||
603 |
\subsubsection*{Syntax} |
|
604 |
||
605 |
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
30403 | 606 |
@{term"Map.empty"} & @{term"\<lambda>x. None"}\\ |
30293 | 607 |
@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ |
61996 | 608 |
\<open>m(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)\<close> & @{text[source]"m(x\<^sub>1\<mapsto>y\<^sub>1)\<dots>(x\<^sub>n\<mapsto>y\<^sub>n)"}\\ |
609 |
\<open>[x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n]\<close> & @{text[source]"Map.empty(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)"}\\ |
|
30293 | 610 |
@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ |
611 |
\end{tabular} |
|
612 |
||
50581 | 613 |
\section*{Infix operators in Main} % @{theory Main} |
614 |
||
615 |
\begin{center} |
|
50605 | 616 |
\begin{tabular}{llll} |
617 |
& Operator & precedence & associativity \\ |
|
618 |
\hline |
|
61996 | 619 |
Meta-logic & \<open>\<Longrightarrow>\<close> & 1 & right \\ |
620 |
& \<open>\<equiv>\<close> & 2 \\ |
|
50605 | 621 |
\hline |
61996 | 622 |
Logic & \<open>\<and>\<close> & 35 & right \\ |
623 |
&\<open>\<or>\<close> & 30 & right \\ |
|
624 |
&\<open>\<longrightarrow>\<close>, \<open>\<longleftrightarrow>\<close> & 25 & right\\ |
|
625 |
&\<open>=\<close>, \<open>\<noteq>\<close> & 50 & left\\ |
|
50605 | 626 |
\hline |
61996 | 627 |
Orderings & \<open>\<le>\<close>, \<open><\<close>, \<open>\<ge>\<close>, \<open>>\<close> & 50 \\ |
50605 | 628 |
\hline |
61996 | 629 |
Sets & \<open>\<subseteq>\<close>, \<open>\<subset>\<close>, \<open>\<supseteq>\<close>, \<open>\<supset>\<close> & 50 \\ |
630 |
&\<open>\<in>\<close>, \<open>\<notin>\<close> & 50 \\ |
|
631 |
&\<open>\<inter>\<close> & 70 & left \\ |
|
632 |
&\<open>\<union>\<close> & 65 & left \\ |
|
50605 | 633 |
\hline |
61996 | 634 |
Functions and Relations & \<open>\<circ>\<close> & 55 & left\\ |
635 |
&\<open>`\<close> & 90 & right\\ |
|
636 |
&\<open>O\<close> & 75 & right\\ |
|
637 |
&\<open>``\<close> & 90 & right\\ |
|
638 |
&\<open>^^\<close> & 80 & right\\ |
|
50605 | 639 |
\hline |
61996 | 640 |
Numbers & \<open>+\<close>, \<open>-\<close> & 65 & left \\ |
641 |
&\<open>*\<close>, \<open>/\<close> & 70 & left \\ |
|
642 |
&\<open>div\<close>, \<open>mod\<close> & 70 & left\\ |
|
643 |
&\<open>^\<close> & 80 & right\\ |
|
644 |
&\<open>dvd\<close> & 50 \\ |
|
50605 | 645 |
\hline |
61996 | 646 |
Lists & \<open>#\<close>, \<open>@\<close> & 65 & right\\ |
647 |
&\<open>!\<close> & 100 & left |
|
50581 | 648 |
\end{tabular} |
649 |
\end{center} |
|
61996 | 650 |
\<close> |
30293 | 651 |
(*<*) |
652 |
end |
|
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65954
diff
changeset
|
653 |
(*>*) |