author  nipkow 
Mon, 09 Mar 2009 23:29:13 +0100  
changeset 30403  042641837e79 
parent 30402  c47e0189013b 
child 30425  eacaf2f86bb5 
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} 

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 sophisicated class structure is only hinted at. 

22 
\end{abstract} 

23 

24 
\section{HOL} 

25 

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 

28 
Overloaded operators: 

29 

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

31 
@{text "0"} & @{typeof HOL.zero}\\ 

32 
@{text "1"} & @{typeof HOL.one}\\ 

33 
@{const HOL.plus} & @{typeof HOL.plus}\\ 

34 
@{const HOL.minus} & @{typeof HOL.minus}\\ 

35 
@{const HOL.uminus} & @{typeof HOL.uminus}\\ 

36 
@{const HOL.times} & @{typeof HOL.times}\\ 

37 
@{const HOL.inverse} & @{typeof HOL.inverse}\\ 

38 
@{const HOL.divide} & @{typeof HOL.divide}\\ 

39 
@{const HOL.abs} & @{typeof HOL.abs}\\ 

40 
@{const HOL.sgn} & @{typeof HOL.sgn}\\ 

41 
@{const HOL.less_eq} & @{typeof HOL.less_eq}\\ 

42 
@{const HOL.less} & @{typeof HOL.less}\\ 

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

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

45 
\end{supertabular} 

46 

47 
\subsubsection*{Syntax} 

48 

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

50 
@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"}\\ 

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

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

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

54 
@{term"abs x"} & @{term[source]"abs x"}\\ 

55 
@{term"uminus x"} & @{term[source]"uminus x"}\\ 

56 
\end{supertabular} 

57 

58 
\section{Orderings} 

59 

60 
A collection of classes constraining @{text"\<le>"} and @{text"<"}: 

30401  61 
preorder, partial order, linear order, dense linear order and wellorder. 
30293  62 

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

64 
@{const Orderings.Least} & @{typeof Orderings.Least}\\ 

65 
@{const Orderings.min} & @{typeof Orderings.min}\\ 

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

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

68 
\end{tabular} 

69 

70 
\subsubsection*{Syntax} 

71 

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

73 
@{term[source]"x \<ge> y"} & @{term"x \<ge> y"}\\ 

74 
@{term[source]"x > y"} & @{term"x > y"}\\ 

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

30386  76 
\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$, and for @{text"\<exists>"}}\\ 
30293  77 
@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\ 
78 
\end{supertabular} 

79 

30401  80 

81 
\section{Lattices} 

82 

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

84 
latter in theory @{theory Set}). 

85 

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

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

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

89 
@{const Set.Inf} & @{term_type_only Set.Inf "'a set \<Rightarrow> 'a::complete_lattice"}\\ 

90 
@{const Set.Sup} & @{term_type_only Set.Sup "'a set \<Rightarrow> 'a::complete_lattice"}\\ 

91 
\end{tabular} 

92 

93 
\subsubsection*{Syntax} 

94 

95 
Only available locally: 

96 

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

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

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

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

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

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

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

104 
\end{supertabular} 

105 

106 

30293  107 
\section{Set} 
108 

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

110 
\bigskip 

111 

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

30370  113 
@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ 
30293  114 
@{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\ 
115 
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\ 

30370  116 
@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} \qquad(\textsc{ascii} @{text":"})\\ 
117 
@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Un"})\\ 

118 
@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Int"})\\ 

30293  119 
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ 
120 
@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ 

121 
@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\ 

122 
@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\ 

123 
@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\ 

124 
@{const UNIV} & @{term_type_only UNIV "'a set"}\\ 

125 
@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\ 

126 
@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ 

127 
@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ 

128 
\end{supertabular} 

129 

130 
\subsubsection*{Syntax} 

131 

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

133 
@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\ 

134 
@{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\ 

135 
@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\ 

136 
@{term"A \<subset> B"} & @{term[source]"A < B"}\\ 

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

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

139 
@{term"{x. P}"} & @{term[source]"Collect(\<lambda>x. P)"}\\ 

30370  140 
@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\ 
141 
@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\ 

142 
@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\ 

143 
@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\ 

30293  144 
@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\ 
145 
@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\ 

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

147 
\end{supertabular} 

148 

149 

150 
\section{Fun} 

151 

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

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

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

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

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

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

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

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

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

161 
\end{supertabular} 

162 

163 
\subsubsection*{Syntax} 

164 

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

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

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

168 
\end{tabular} 

169 

170 

171 
\section{Fixed Points} 

172 

173 
Theory: @{theory Inductive}. 

174 

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

176 

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

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

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

180 
\end{tabular} 

181 

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

183 

184 
\section{Sum\_Type} 

185 

186 
Type constructor @{text"+"}. 

187 

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

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

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

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

192 
\end{tabular} 

193 

194 

195 
\section{Product\_Type} 

196 

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

198 

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

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

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

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

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

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

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

206 
@{const Product_Type.Times} & @{typeof Product_Type.Times}\\ 

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

208 
\end{supertabular} 

209 

210 
\subsubsection*{Syntax} 

211 

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

213 
@{term"Pair a b"} & @{term[source]"Pair a b"}\\ 

214 
@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\ 

215 
\end{tabular} 

216 

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

218 
e.g.\ \mbox{@{term"(a,b,c)"}} is really @{text"(a,(b,c))"}. 

219 
Pattern matching with pairs and tuples extends to all binders, 

220 
e.g.\ @{prop"ALL (x,y):A. P"}, @{term"{(x,y). P}"}, etc. 

221 

222 

223 
\section{Relation} 

224 

30401  225 
\begin{tabular}{@ {} l @ {~::~} l @ {}} 
30293  226 
@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\ 
227 
@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('c*'a)set\<Rightarrow>('c*'b)set"}\\ 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

30401  242 
@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"} 
243 
\end{tabular} 

30293  244 

245 
\subsubsection*{Syntax} 

246 

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

248 
@{term"converse r"} & @{term[source]"converse r"} 

249 
\end{tabular} 

250 

251 
\section{Equiv\_Relations} 

252 

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

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

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

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

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

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

259 
\end{supertabular} 

260 

261 
\subsubsection*{Syntax} 

262 

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

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

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

266 
\end{tabular} 

267 

268 

269 
\section{Transitive\_Closure} 

270 

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

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

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

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

275 
\end{tabular} 

276 

277 
\subsubsection*{Syntax} 

278 

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

280 
@{term"rtrancl r"} & @{term[source]"rtrancl r"}\\ 

281 
@{term"trancl r"} & @{term[source]"trancl r"}\\ 

282 
@{term"reflcl r"} & @{term[source]"reflcl r"} 

283 
\end{tabular} 

284 

285 

286 
\section{Algebra} 

287 

288 
Theories @{theory OrderedGroup} and @{theory Ring_and_Field} define a large 

289 
collection of classes describing common algebraic structures from semigroups 

290 
up to fields. Everything is done in terms of @{const plus}, @{const times} 

291 
and other overloaded operators. 

292 

293 

294 
\section{Nat} 

295 

296 
@{datatype nat} 

297 
\bigskip 

298 

299 
\begin{tabular}{@ {} lllllll @ {}} 

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

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

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

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

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

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

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

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

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

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

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

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

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

313 
\end{tabular} 

314 

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

316 
@{const Nat.of_nat} & @{typeof Nat.of_nat} 

317 
\end{tabular} 

318 

319 
\section{Int} 

320 

321 
Type @{typ int} 

322 
\bigskip 

323 

324 
\begin{tabular}{@ {} llllllll @ {}} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

341 
\end{tabular} 

342 

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

344 
@{const Int.nat} & @{typeof Int.nat}\\ 

345 
@{const Int.of_int} & @{typeof Int.of_int}\\ 

346 
@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"}\\ 

347 
\end{tabular} 

348 

349 
\subsubsection*{Syntax} 

350 

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

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

353 
\end{tabular} 

354 

355 

30401  356 
\section{Finite\_Set} 
357 

358 

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

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

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

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

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

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

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

366 
\end{supertabular} 

367 

368 

369 
\subsubsection*{Syntax} 

370 

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

372 
@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"}\\ 

373 
@{term"setsum (%x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\ 

374 
@{term[source]"\<Sum>xP. t"} & @{term"\<Sum>xP. t"}\\ 

375 
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\ 

376 
\end{supertabular} 

377 

378 

30293  379 
\section{Wellfounded} 
380 

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

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

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

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

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

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

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

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

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

390 
\end{supertabular} 

391 

392 

30384  393 
\section{SetInterval} 
30321  394 

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

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

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

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

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

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

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

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

30321  404 
\end{supertabular} 
405 

406 
\subsubsection*{Syntax} 

407 

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

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

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

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

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

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

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

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

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

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

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

30321  420 
@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\ 
30370  421 
@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\ 
30386  422 
@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\ 
423 
@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\ 

30372  424 
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\ 
30321  425 
\end{supertabular} 
426 

427 

30293  428 
\section{Power} 
429 

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

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

432 
\end{tabular} 

433 

434 

435 
\section{Iterated Functions and Relations} 

436 

437 
Theory: @{theory Relation_Power} 

438 

439 
Iterated functions \ @{term[source]"(f::'a\<Rightarrow>'a) ^ n"} \ 

440 
and relations \ @{term[source]"(r::('a\<times>'a)set) ^ n"}. 

441 

442 

443 
\section{Option} 

444 

445 
@{datatype option} 

446 
\bigskip 

447 

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

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

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

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

452 
\end{tabular} 

453 

454 
\section{List} 

455 

456 
@{datatype list} 

457 
\bigskip 

458 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

484 
@{const List.remdups} & @{typeof List.remdups}\\ 

485 
@{const List.removeAll} & @{typeof List.removeAll}\\ 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

502 
\end{supertabular} 

503 

504 
\subsubsection*{Syntax} 

505 

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

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

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

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

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

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

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

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

514 
\end{supertabular} 

515 
\medskip 

516 

517 
Comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each 

518 
qualifier @{text q\<^isub>i} is either a generator @{text"pat \<leftarrow> e"} or a 

519 
guard, i.e.\ boolean expression. 

520 

521 
\section{Map} 

522 

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

524 
the domain of a map may be infinite. 

525 

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

527 
\bigskip 

528 

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

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

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

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

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

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

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

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

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

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

539 
\end{supertabular} 

540 

541 
\subsubsection*{Syntax} 

542 

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

30403  544 
@{term"Map.empty"} & @{term"\<lambda>x. None"}\\ 
30293  545 
@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ 
546 
@{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)"}\\ 

547 
@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ 

548 
\end{tabular} 

549 

550 
*} 

551 
(*<*) 

552 
end 

553 
(*>*) 