author  haftmann 
Tue, 09 Feb 2010 08:28:12 +0100  
changeset 35061  be1e25a62ec8 
parent 35007  8c339c73495c 
child 35277  f228929a6fab 
permissions  rwrr 
30293  1 
(*<*) 
30401  2 
theory Main_Doc 
30293  3 
imports Main 
4 
begin 

5 

6 
ML {* 

7 
fun pretty_term_type_only ctxt (t, T) = 

8 
(if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then () 

9 
else error "term_type_only: type mismatch"; 

10 
Syntax.pretty_typ ctxt T) 

11 

30392
9fe4bbb90297
adapted to simplified ThyOutput.antiquotation interface;
wenzelm
parents:
30386
diff
changeset

12 
val _ = ThyOutput.antiquotation "term_type_only" (Args.term  Args.typ_abbrev) 
9fe4bbb90297
adapted to simplified ThyOutput.antiquotation interface;
wenzelm
parents:
30386
diff
changeset

13 
(fn {source, context, ...} => fn arg => 
9fe4bbb90297
adapted to simplified ThyOutput.antiquotation interface;
wenzelm
parents:
30386
diff
changeset

14 
ThyOutput.output 
9fe4bbb90297
adapted to simplified ThyOutput.antiquotation interface;
wenzelm
parents:
30386
diff
changeset

15 
(ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg])); 
30293  16 
*} 
17 
(*>*) 

18 
text{* 

19 

20 
\begin{abstract} 

30442  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. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/dist/library/HOL/}. 
30293  22 
\end{abstract} 
23 

24 
\section{HOL} 

25 

30440  26 
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"}. 
27 
\smallskip 

28 

29 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

30 
@{const HOL.undefined} & @{typeof HOL.undefined}\\ 

31 
@{const HOL.default} & @{typeof HOL.default}\\ 

32 
\end{tabular} 

33 

34 
\subsubsection*{Syntax} 

30293  35 

30440  36 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
37 
@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"} & (\verb$~=$)\\ 

38 
@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\ 

39 
@{term"If x y z"} & @{term[source]"If x y z"}\\ 

40 
@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\<lambda>x. e\<^isub>2)"}\\ 

41 
\end{supertabular} 

42 

43 

44 
\section{Orderings} 

45 

46 
A collection of classes defining basic orderings: 

47 
preorder, partial order, linear order, dense linear order and wellorder. 

48 
\smallskip 

30293  49 

30425  50 
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 
35007  51 
@{const Algebras.less_eq} & @{typeof Algebras.less_eq} & (\verb$<=$)\\ 
52 
@{const Algebras.less} & @{typeof Algebras.less}\\ 

30440  53 
@{const Orderings.Least} & @{typeof Orderings.Least}\\ 
54 
@{const Orderings.min} & @{typeof Orderings.min}\\ 

55 
@{const Orderings.max} & @{typeof Orderings.max}\\ 

56 
@{const[source] top} & @{typeof Orderings.top}\\ 

57 
@{const[source] bot} & @{typeof Orderings.bot}\\ 

58 
@{const Orderings.mono} & @{typeof Orderings.mono}\\ 

59 
@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\ 

30293  60 
\end{supertabular} 
61 

62 
\subsubsection*{Syntax} 

63 

30440  64 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
65 
@{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\verb$>=$)\\ 

30293  66 
@{term[source]"x > y"} & @{term"x > y"}\\ 
67 
@{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\ 

30440  68 
@{term"EX x<=y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\ 
69 
\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ 

30293  70 
@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\ 
71 
\end{supertabular} 

72 

30401  73 

74 
\section{Lattices} 

75 

76 
Classes semilattice, lattice, distributive lattice and complete lattice (the 

77 
latter in theory @{theory Set}). 

78 

79 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

80 
@{const Lattices.inf} & @{typeof Lattices.inf}\\ 

81 
@{const Lattices.sup} & @{typeof Lattices.sup}\\ 

32885  82 
@{const Complete_Lattice.Inf} & @{term_type_only Complete_Lattice.Inf "'a set \<Rightarrow> 'a::Inf"}\\ 
83 
@{const Complete_Lattice.Sup} & @{term_type_only Complete_Lattice.Sup "'a set \<Rightarrow> 'a::Sup"}\\ 

30401  84 
\end{tabular} 
85 

86 
\subsubsection*{Syntax} 

87 

30440  88 
Available by loading theory @{text Lattice_Syntax} in directory @{text 
89 
Library}. 

30401  90 

91 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

92 
@{text[source]"x \<sqsubseteq> y"} & @{term"x \<le> y"}\\ 

93 
@{text[source]"x \<sqsubset> y"} & @{term"x < y"}\\ 

94 
@{text[source]"x \<sqinter> y"} & @{term"inf x y"}\\ 

95 
@{text[source]"x \<squnion> y"} & @{term"sup x y"}\\ 

96 
@{text[source]"\<Sqinter> A"} & @{term"Sup A"}\\ 

97 
@{text[source]"\<Squnion> A"} & @{term"Inf A"}\\ 

30440  98 
@{text[source]"\<top>"} & @{term[source] top}\\ 
99 
@{text[source]"\<bottom>"} & @{term[source] bot}\\ 

30401  100 
\end{supertabular} 
101 

102 

30293  103 
\section{Set} 
104 

105 
Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"} 

106 
\bigskip 

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"}\\ 
30425  112 
@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\ 
32208  113 
@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\ 
114 
@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\ 

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 @ {}} 
30293  129 
@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\ 
130 
@{term"x ~: 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"}\\ 

133 
@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\ 

134 
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\ 

30440  135 
@{term"{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\ 
30425  136 
@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\ 
30370  137 
@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\ 
30425  138 
@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\ 
30370  139 
@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\ 
30293  140 
@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\ 
141 
@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\ 

142 
@{term"range f"} & @{term[source]"f ` UNIV"}\\ 

143 
\end{supertabular} 

144 

145 

146 
\section{Fun} 

147 

32933  148 
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 
30293  149 
@{const "Fun.id"} & @{typeof Fun.id}\\ 
32933  150 
@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\ 
30293  151 
@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\ 
152 
@{const "Fun.inj"} & @{typeof Fun.inj}\\ 

153 
@{const "Fun.surj"} & @{typeof Fun.surj}\\ 

154 
@{const "Fun.bij"} & @{typeof Fun.bij}\\ 

155 
@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\ 

156 
@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ 

157 
\end{supertabular} 

158 

159 
\subsubsection*{Syntax} 

160 

161 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

162 
@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ 

163 
@{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)"}\\ 

164 
\end{tabular} 

165 

166 

33019  167 
\section{Hilbert\_Choice} 
168 

169 
Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}. 

170 
\smallskip 

171 

172 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

33057  173 
@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"} 
33019  174 
\end{tabular} 
175 

176 
\subsubsection*{Syntax} 

177 

178 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

33057  179 
@{term inv} & @{term[source]"inv_into UNIV"} 
33019  180 
\end{tabular} 
181 

30293  182 
\section{Fixed Points} 
183 

184 
Theory: @{theory Inductive}. 

185 

186 
Least and greatest fixed points in a complete lattice @{typ 'a}: 

187 

188 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

189 
@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ 

190 
@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ 

191 
\end{tabular} 

192 

193 
Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices. 

194 

195 
\section{Sum\_Type} 

196 

197 
Type constructor @{text"+"}. 

198 

199 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

200 
@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ 

201 
@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ 

202 
@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"} 

203 
\end{tabular} 

204 

205 

206 
\section{Product\_Type} 

207 

208 
Types @{typ unit} and @{text"\<times>"}. 

209 

210 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

211 
@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ 

212 
@{const Pair} & @{typeof Pair}\\ 

213 
@{const fst} & @{typeof fst}\\ 

214 
@{const snd} & @{typeof snd}\\ 

215 
@{const split} & @{typeof split}\\ 

216 
@{const curry} & @{typeof curry}\\ 

217 
@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\ 

218 
\end{supertabular} 

219 

220 
\subsubsection*{Syntax} 

221 

30440  222 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} 
30293  223 
@{term"Pair a b"} & @{term[source]"Pair a b"}\\ 
224 
@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\ 

30440  225 
@{term"A <*> B"} & @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$) 
30293  226 
\end{tabular} 
227 

228 
Pairs may be nested. Nesting to the right is printed as a tuple, 

30440  229 
e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{@{text"(a, (b, c))"}.} 
30293  230 
Pattern matching with pairs and tuples extends to all binders, 
30440  231 
e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc. 
30293  232 

233 

234 
\section{Relation} 

235 

30440  236 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 
30293  237 
@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\ 
32243  238 
@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('b*'c)set\<Rightarrow>('a*'c)set"}\\ 
30293  239 
@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\ 
240 
@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\ 

241 
@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\ 

242 
@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\ 

243 
@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\ 

244 
@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\ 

245 
@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\ 

246 
@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ 

247 
@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\ 

248 
@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\ 

249 
@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\ 

250 
@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\ 

251 
@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\ 

252 
@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ 

30440  253 
@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\ 
254 
\end{supertabular} 

30293  255 

256 
\subsubsection*{Syntax} 

257 

30440  258 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
259 
@{term"converse r"} & @{term[source]"converse r"} & (\verb$^1$) 

30293  260 
\end{tabular} 
261 

262 
\section{Equiv\_Relations} 

263 

264 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

265 
@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\ 

266 
@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\ 

267 
@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\ 

268 
@{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"}\\ 

269 
%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ 

270 
\end{supertabular} 

271 

272 
\subsubsection*{Syntax} 

273 

274 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

275 
@{term"congruent r f"} & @{term[source]"congruent r f"}\\ 

276 
@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\ 

277 
\end{tabular} 

278 

279 

280 
\section{Transitive\_Closure} 

281 

282 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

283 
@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ 

284 
@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ 

285 
@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ 

30988  286 
@{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  287 
\end{tabular} 
288 

289 
\subsubsection*{Syntax} 

290 

30440  291 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
292 
@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\verb$^*$)\\ 

293 
@{term"trancl r"} & @{term[source]"trancl r"} & (\verb$^+$)\\ 

294 
@{term"reflcl r"} & @{term[source]"reflcl r"} & (\verb$^=$) 

30293  295 
\end{tabular} 
296 

297 

298 
\section{Algebra} 

299 

35061  300 
Theories @{theory Groups}, @{theory Rings}, @{theory Fields} and @{theory 
30440  301 
Divides} define a large collection of classes describing common algebraic 
302 
structures from semigroups up to fields. Everything is done in terms of 

303 
overloaded operators: 

304 

305 
\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 

306 
@{text "0"} & @{typeof zero}\\ 

307 
@{text "1"} & @{typeof one}\\ 

308 
@{const plus} & @{typeof plus}\\ 

309 
@{const minus} & @{typeof minus}\\ 

310 
@{const uminus} & @{typeof uminus} & (\verb$$)\\ 

311 
@{const times} & @{typeof times}\\ 

312 
@{const inverse} & @{typeof inverse}\\ 

313 
@{const divide} & @{typeof divide}\\ 

314 
@{const abs} & @{typeof abs}\\ 

315 
@{const sgn} & @{typeof sgn}\\ 

316 
@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\ 

317 
@{const div_class.div} & @{typeof "div_class.div"}\\ 

318 
@{const div_class.mod} & @{typeof "div_class.mod"}\\ 

319 
\end{supertabular} 

320 

321 
\subsubsection*{Syntax} 

322 

323 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

324 
@{term"abs x"} & @{term[source]"abs x"} 

325 
\end{tabular} 

30293  326 

327 

328 
\section{Nat} 

329 

330 
@{datatype nat} 

331 
\bigskip 

332 

333 
\begin{tabular}{@ {} lllllll @ {}} 

334 
@{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

335 
@{term "op  :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

336 
@{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

337 
@{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}& 

338 
@{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}& 

339 
@{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\ 

340 
@{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} & 

341 
@{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} & 

342 
@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

343 
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 

344 
@{term "Min :: nat set \<Rightarrow> nat"} & 

345 
@{term "Max :: nat set \<Rightarrow> nat"}\\ 

346 
\end{tabular} 

347 

348 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

30988  349 
@{const Nat.of_nat} & @{typeof Nat.of_nat}\\ 
350 
@{term "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} & 

351 
@{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} 

30293  352 
\end{tabular} 
353 

354 
\section{Int} 

355 

356 
Type @{typ int} 

357 
\bigskip 

358 

359 
\begin{tabular}{@ {} llllllll @ {}} 

360 
@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} & 

361 
@{term "op  :: int \<Rightarrow> int \<Rightarrow> int"} & 

362 
@{term "uminus :: int \<Rightarrow> int"} & 

363 
@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} & 

364 
@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} & 

365 
@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}& 

366 
@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}& 

367 
@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\ 

368 
@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} & 

369 
@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} & 

370 
@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} & 

371 
@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} & 

372 
@{term "Min :: int set \<Rightarrow> int"} & 

373 
@{term "Max :: int set \<Rightarrow> int"}\\ 

374 
@{term "abs :: int \<Rightarrow> int"} & 

375 
@{term "sgn :: int \<Rightarrow> int"}\\ 

376 
\end{tabular} 

377 

30440  378 
\begin{tabular}{@ {} l @ {~::~} l l @ {}} 
30293  379 
@{const Int.nat} & @{typeof Int.nat}\\ 
380 
@{const Int.of_int} & @{typeof Int.of_int}\\ 

30440  381 
@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\verb$Ints$) 
30293  382 
\end{tabular} 
383 

384 
\subsubsection*{Syntax} 

385 

386 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

387 
@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\ 

388 
\end{tabular} 

389 

390 

30401  391 
\section{Finite\_Set} 
392 

393 

394 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

395 
@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\ 

396 
@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\ 

397 
@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\ 

398 
@{const Finite_Set.fold_image} & @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\ 

399 
@{const Finite_Set.setsum} & @{term_type_only Finite_Set.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\ 

400 
@{const Finite_Set.setprod} & @{term_type_only Finite_Set.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\ 

401 
\end{supertabular} 

402 

403 

404 
\subsubsection*{Syntax} 

405 

30440  406 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 
407 
@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\verb$SUM$)\\ 

30401  408 
@{term"setsum (%x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\ 
409 
@{term[source]"\<Sum>xP. t"} & @{term"\<Sum>xP. t"}\\ 

30440  410 
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}} & (\verb$PROD$)\\ 
30401  411 
\end{supertabular} 
412 

413 

30293  414 
\section{Wellfounded} 
415 

416 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

417 
@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\ 

418 
@{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\<Rightarrow>bool"}\\ 

419 
@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\ 

420 
@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\ 

421 
@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\ 

422 
@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\ 

423 
@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ 

424 
@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ 

425 
\end{supertabular} 

426 

427 

30384  428 
\section{SetInterval} 
30321  429 

430 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

30370  431 
@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\ 
432 
@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\ 

433 
@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\ 

434 
@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\ 

435 
@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 

436 
@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 

437 
@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 

438 
@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 

30321  439 
\end{supertabular} 
440 

441 
\subsubsection*{Syntax} 

442 

443 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

444 
@{term "lessThan y"} & @{term[source] "lessThan y"}\\ 

445 
@{term "atMost y"} & @{term[source] "atMost y"}\\ 

446 
@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\ 

447 
@{term "atLeast x"} & @{term[source] "atLeast x"}\\ 

448 
@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\ 

449 
@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\ 

450 
@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\ 

451 
@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\ 

30370  452 
@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\ 
453 
@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\ 

454 
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\ 

30321  455 
@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\ 
30370  456 
@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\ 
30386  457 
@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\ 
458 
@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\ 

30372  459 
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\ 
30321  460 
\end{supertabular} 
461 

462 

30293  463 
\section{Power} 
464 

465 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

466 
@{const Power.power} & @{typeof Power.power} 

467 
\end{tabular} 

468 

469 

470 
\section{Option} 

471 

472 
@{datatype option} 

473 
\bigskip 

474 

475 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 

476 
@{const Option.the} & @{typeof Option.the}\\ 

477 
@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\ 

478 
@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"} 

479 
\end{tabular} 

480 

481 
\section{List} 

482 

483 
@{datatype list} 

484 
\bigskip 

485 

486 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

487 
@{const List.append} & @{typeof List.append}\\ 

488 
@{const List.butlast} & @{typeof List.butlast}\\ 

489 
@{const List.concat} & @{typeof List.concat}\\ 

490 
@{const List.distinct} & @{typeof List.distinct}\\ 

491 
@{const List.drop} & @{typeof List.drop}\\ 

492 
@{const List.dropWhile} & @{typeof List.dropWhile}\\ 

493 
@{const List.filter} & @{typeof List.filter}\\ 

494 
@{const List.foldl} & @{typeof List.foldl}\\ 

495 
@{const List.foldr} & @{typeof List.foldr}\\ 

496 
@{const List.hd} & @{typeof List.hd}\\ 

497 
@{const List.last} & @{typeof List.last}\\ 

498 
@{const List.length} & @{typeof List.length}\\ 

499 
@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 

500 
@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 

501 
@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\ 

502 
@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 

503 
@{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 

504 
@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\ 

505 
@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\ 

506 
@{const List.listsum} & @{typeof List.listsum}\\ 

507 
@{const List.list_all2} & @{typeof List.list_all2}\\ 

508 
@{const List.list_update} & @{typeof List.list_update}\\ 

509 
@{const List.map} & @{typeof List.map}\\ 

510 
@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\ 

32933  511 
@{const List.nth} & @{typeof List.nth}\\ 
30293  512 
@{const List.remdups} & @{typeof List.remdups}\\ 
513 
@{const List.removeAll} & @{typeof List.removeAll}\\ 

514 
@{const List.remove1} & @{typeof List.remove1}\\ 

515 
@{const List.replicate} & @{typeof List.replicate}\\ 

516 
@{const List.rev} & @{typeof List.rev}\\ 

517 
@{const List.rotate} & @{typeof List.rotate}\\ 

518 
@{const List.rotate1} & @{typeof List.rotate1}\\ 

519 
@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\ 

520 
@{const List.sort} & @{typeof List.sort}\\ 

521 
@{const List.sorted} & @{typeof List.sorted}\\ 

522 
@{const List.splice} & @{typeof List.splice}\\ 

523 
@{const List.sublist} & @{typeof List.sublist}\\ 

524 
@{const List.take} & @{typeof List.take}\\ 

525 
@{const List.takeWhile} & @{typeof List.takeWhile}\\ 

526 
@{const List.tl} & @{typeof List.tl}\\ 

527 
@{const List.upt} & @{typeof List.upt}\\ 

528 
@{const List.upto} & @{typeof List.upto}\\ 

529 
@{const List.zip} & @{typeof List.zip}\\ 

530 
\end{supertabular} 

531 

532 
\subsubsection*{Syntax} 

533 

534 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

535 
@{text"[x\<^isub>1,\<dots>,x\<^isub>n]"} & @{text"x\<^isub>1 # \<dots> # x\<^isub>n # []"}\\ 

536 
@{term"[m..<n]"} & @{term[source]"upt m n"}\\ 

537 
@{term"[i..j]"} & @{term[source]"upto i j"}\\ 

538 
@{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\ 

539 
@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\ 

540 
@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ 

541 
@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\ 

542 
\end{supertabular} 

543 
\medskip 

544 

30440  545 
List comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each 
546 
qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \<leftarrow> e"}} or a 

30293  547 
guard, i.e.\ boolean expression. 
548 

549 
\section{Map} 

550 

551 
Maps model partial functions and are often used as finite tables. However, 

552 
the domain of a map may be infinite. 

553 

554 
@{text"'a \<rightharpoonup> 'b = 'a \<Rightarrow> 'b option"} 

555 
\bigskip 

556 

557 
\begin{supertabular}{@ {} l @ {~::~} l @ {}} 

558 
@{const Map.empty} & @{typeof Map.empty}\\ 

559 
@{const Map.map_add} & @{typeof Map.map_add}\\ 

560 
@{const Map.map_comp} & @{typeof Map.map_comp}\\ 

561 
@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\ 

562 
@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\ 

563 
@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\ 

564 
@{const Map.map_le} & @{typeof Map.map_le}\\ 

565 
@{const Map.map_of} & @{typeof Map.map_of}\\ 

566 
@{const Map.map_upds} & @{typeof Map.map_upds}\\ 

567 
\end{supertabular} 

568 

569 
\subsubsection*{Syntax} 

570 

571 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 

30403  572 
@{term"Map.empty"} & @{term"\<lambda>x. None"}\\ 
30293  573 
@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ 
574 
@{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  575 
@{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  576 
@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ 
577 
\end{tabular} 

578 

579 
*} 

580 
(*<*) 

581 
end 

582 
(*>*) 