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