|
1 (*<*) |
|
2 theory MainDoc |
|
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 |
|
12 val _ = ThyOutput.add_commands |
|
13 [("term_type_only", ThyOutput.args (Args.term -- Args.typ_abbrev) (ThyOutput.output pretty_term_type_only))]; |
|
14 *} |
|
15 (*>*) |
|
16 text{* |
|
17 |
|
18 \begin{abstract} |
|
19 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. |
|
20 \end{abstract} |
|
21 |
|
22 \section{HOL} |
|
23 |
|
24 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"}. |
|
25 |
|
26 Overloaded operators: |
|
27 |
|
28 \begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
29 @{text "0"} & @{typeof HOL.zero}\\ |
|
30 @{text "1"} & @{typeof HOL.one}\\ |
|
31 @{const HOL.plus} & @{typeof HOL.plus}\\ |
|
32 @{const HOL.minus} & @{typeof HOL.minus}\\ |
|
33 @{const HOL.uminus} & @{typeof HOL.uminus}\\ |
|
34 @{const HOL.times} & @{typeof HOL.times}\\ |
|
35 @{const HOL.inverse} & @{typeof HOL.inverse}\\ |
|
36 @{const HOL.divide} & @{typeof HOL.divide}\\ |
|
37 @{const HOL.abs} & @{typeof HOL.abs}\\ |
|
38 @{const HOL.sgn} & @{typeof HOL.sgn}\\ |
|
39 @{const HOL.less_eq} & @{typeof HOL.less_eq}\\ |
|
40 @{const HOL.less} & @{typeof HOL.less}\\ |
|
41 @{const HOL.default} & @{typeof HOL.default}\\ |
|
42 @{const HOL.undefined} & @{typeof HOL.undefined}\\ |
|
43 \end{supertabular} |
|
44 |
|
45 \subsubsection*{Syntax} |
|
46 |
|
47 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
48 @{term"~(x = y)"} & @{term[source]"\<not> (x = y)"}\\ |
|
49 @{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"}\\ |
|
50 @{term"If x y z"} & @{term[source]"If x y z"}\\ |
|
51 @{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\<lambda>x. e\<^isub>2)"}\\ |
|
52 @{term"abs x"} & @{term[source]"abs x"}\\ |
|
53 @{term"uminus x"} & @{term[source]"uminus x"}\\ |
|
54 \end{supertabular} |
|
55 |
|
56 \section{Orderings} |
|
57 |
|
58 A collection of classes constraining @{text"\<le>"} and @{text"<"}: |
|
59 preorders, partial orders, linear orders, dense linear orders and wellorders. |
|
60 |
|
61 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
62 @{const Orderings.Least} & @{typeof Orderings.Least}\\ |
|
63 @{const Orderings.min} & @{typeof Orderings.min}\\ |
|
64 @{const Orderings.max} & @{typeof Orderings.max}\\ |
|
65 @{const Orderings.mono} & @{typeof Orderings.mono}\\ |
|
66 \end{tabular} |
|
67 |
|
68 \subsubsection*{Syntax} |
|
69 |
|
70 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
71 @{term[source]"x \<ge> y"} & @{term"x \<ge> y"}\\ |
|
72 @{term[source]"x > y"} & @{term"x > y"}\\ |
|
73 @{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\ |
|
74 @{term"ALL x<y. P"} & @{term[source]"\<forall>x. x < y \<longrightarrow> P"}\\ |
|
75 @{term"ALL x>=y. P"} & @{term[source]"\<forall>x. x \<ge> y \<longrightarrow> P"}\\ |
|
76 @{term"ALL x>y. P"} & @{term[source]"\<forall>x. x > y \<longrightarrow> P"}\\ |
|
77 @{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\ |
|
78 \end{supertabular} |
|
79 |
|
80 Similar for @{text"\<exists>"} instead of @{text"\<forall>"}. |
|
81 |
|
82 \section{Set} |
|
83 |
|
84 Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"} |
|
85 \bigskip |
|
86 |
|
87 \begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
88 @{const "{}"} & @{term_type_only "{}" "'a set"}\\ |
|
89 @{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\ |
|
90 @{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\ |
|
91 @{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"}\\ |
|
92 @{const "op Un"} & @{term_type_only "op Un" "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"}\\ |
|
93 @{const "op Int"} & @{term_type_only "op Int" "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"}\\ |
|
94 @{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
|
95 @{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ |
|
96 @{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\ |
|
97 @{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\ |
|
98 @{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\ |
|
99 @{const UNIV} & @{term_type_only UNIV "'a set"}\\ |
|
100 @{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\ |
|
101 @{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ |
|
102 @{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ |
|
103 \end{supertabular} |
|
104 |
|
105 \subsubsection*{Syntax} |
|
106 |
|
107 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
108 @{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\ |
|
109 @{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\ |
|
110 @{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\ |
|
111 @{term"A \<subset> B"} & @{term[source]"A < B"}\\ |
|
112 @{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\ |
|
113 @{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\ |
|
114 @{term"{x. P}"} & @{term[source]"Collect(\<lambda>x. P)"}\\ |
|
115 @{term"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\ |
|
116 @{term"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\ |
|
117 @{term"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\ |
|
118 @{term"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\ |
|
119 @{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\ |
|
120 @{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\ |
|
121 @{term"range f"} & @{term[source]"f ` UNIV"}\\ |
|
122 \end{supertabular} |
|
123 |
|
124 |
|
125 \section{Fun} |
|
126 |
|
127 \begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
128 @{const "Fun.id"} & @{typeof Fun.id}\\ |
|
129 @{const "Fun.comp"} & @{typeof Fun.comp}\\ |
|
130 @{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\ |
|
131 @{const "Fun.inj"} & @{typeof Fun.inj}\\ |
|
132 @{const "Fun.surj"} & @{typeof Fun.surj}\\ |
|
133 @{const "Fun.bij"} & @{typeof Fun.bij}\\ |
|
134 @{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\ |
|
135 @{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ |
|
136 \end{supertabular} |
|
137 |
|
138 \subsubsection*{Syntax} |
|
139 |
|
140 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
141 @{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ |
|
142 @{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)"}\\ |
|
143 \end{tabular} |
|
144 |
|
145 |
|
146 \section{Fixed Points} |
|
147 |
|
148 Theory: @{theory Inductive}. |
|
149 |
|
150 Least and greatest fixed points in a complete lattice @{typ 'a}: |
|
151 |
|
152 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
153 @{const Inductive.lfp} & @{typeof Inductive.lfp}\\ |
|
154 @{const Inductive.gfp} & @{typeof Inductive.gfp}\\ |
|
155 \end{tabular} |
|
156 |
|
157 Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices. |
|
158 |
|
159 \section{Sum\_Type} |
|
160 |
|
161 Type constructor @{text"+"}. |
|
162 |
|
163 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
164 @{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ |
|
165 @{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ |
|
166 @{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"} |
|
167 \end{tabular} |
|
168 |
|
169 |
|
170 \section{Product\_Type} |
|
171 |
|
172 Types @{typ unit} and @{text"\<times>"}. |
|
173 |
|
174 \begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
175 @{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ |
|
176 @{const Pair} & @{typeof Pair}\\ |
|
177 @{const fst} & @{typeof fst}\\ |
|
178 @{const snd} & @{typeof snd}\\ |
|
179 @{const split} & @{typeof split}\\ |
|
180 @{const curry} & @{typeof curry}\\ |
|
181 @{const Product_Type.Times} & @{typeof Product_Type.Times}\\ |
|
182 @{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\ |
|
183 \end{supertabular} |
|
184 |
|
185 \subsubsection*{Syntax} |
|
186 |
|
187 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
188 @{term"Pair a b"} & @{term[source]"Pair a b"}\\ |
|
189 @{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\ |
|
190 \end{tabular} |
|
191 |
|
192 Pairs may be nested. Nesting to the right is printed as a tuple, |
|
193 e.g.\ \mbox{@{term"(a,b,c)"}} is really @{text"(a,(b,c))"}. |
|
194 Pattern matching with pairs and tuples extends to all binders, |
|
195 e.g.\ @{prop"ALL (x,y):A. P"}, @{term"{(x,y). P}"}, etc. |
|
196 |
|
197 |
|
198 \section{Relation} |
|
199 |
|
200 \begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
201 @{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\ |
|
202 @{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('c*'a)set\<Rightarrow>('c*'b)set"}\\ |
|
203 @{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\ |
|
204 @{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\ |
|
205 @{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\ |
|
206 @{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\ |
|
207 @{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\ |
|
208 @{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\ |
|
209 @{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\ |
|
210 @{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ |
|
211 @{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\ |
|
212 @{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\ |
|
213 @{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\ |
|
214 @{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\ |
|
215 @{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\ |
|
216 @{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ |
|
217 @{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\ |
|
218 \end{supertabular} |
|
219 |
|
220 \subsubsection*{Syntax} |
|
221 |
|
222 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
223 @{term"converse r"} & @{term[source]"converse r"} |
|
224 \end{tabular} |
|
225 |
|
226 \section{Equiv\_Relations} |
|
227 |
|
228 \begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
229 @{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\ |
|
230 @{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\ |
|
231 @{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\ |
|
232 @{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"}\\ |
|
233 %@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ |
|
234 \end{supertabular} |
|
235 |
|
236 \subsubsection*{Syntax} |
|
237 |
|
238 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
239 @{term"congruent r f"} & @{term[source]"congruent r f"}\\ |
|
240 @{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\ |
|
241 \end{tabular} |
|
242 |
|
243 |
|
244 \section{Transitive\_Closure} |
|
245 |
|
246 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
247 @{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
248 @{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
249 @{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
250 \end{tabular} |
|
251 |
|
252 \subsubsection*{Syntax} |
|
253 |
|
254 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
255 @{term"rtrancl r"} & @{term[source]"rtrancl r"}\\ |
|
256 @{term"trancl r"} & @{term[source]"trancl r"}\\ |
|
257 @{term"reflcl r"} & @{term[source]"reflcl r"} |
|
258 \end{tabular} |
|
259 |
|
260 |
|
261 \section{Algebra} |
|
262 |
|
263 Theories @{theory OrderedGroup} and @{theory Ring_and_Field} define a large |
|
264 collection of classes describing common algebraic structures from semigroups |
|
265 up to fields. Everything is done in terms of @{const plus}, @{const times} |
|
266 and other overloaded operators. |
|
267 |
|
268 |
|
269 \section{Nat} |
|
270 |
|
271 @{datatype nat} |
|
272 \bigskip |
|
273 |
|
274 \begin{tabular}{@ {} lllllll @ {}} |
|
275 @{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
276 @{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
277 @{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
278 @{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
279 @{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}& |
|
280 @{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}& |
|
281 @{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\ |
|
282 @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} & |
|
283 @{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} & |
|
284 @{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
285 @{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} & |
|
286 @{term "Min :: nat set \<Rightarrow> nat"} & |
|
287 @{term "Max :: nat set \<Rightarrow> nat"}\\ |
|
288 \end{tabular} |
|
289 |
|
290 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
291 @{const Nat.of_nat} & @{typeof Nat.of_nat} |
|
292 \end{tabular} |
|
293 |
|
294 \section{Int} |
|
295 |
|
296 Type @{typ int} |
|
297 \bigskip |
|
298 |
|
299 \begin{tabular}{@ {} llllllll @ {}} |
|
300 @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
301 @{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
302 @{term "uminus :: int \<Rightarrow> int"} & |
|
303 @{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
304 @{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} & |
|
305 @{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}& |
|
306 @{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}& |
|
307 @{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\ |
|
308 @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} & |
|
309 @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} & |
|
310 @{term "min :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
311 @{term "max :: int \<Rightarrow> int \<Rightarrow> int"} & |
|
312 @{term "Min :: int set \<Rightarrow> int"} & |
|
313 @{term "Max :: int set \<Rightarrow> int"}\\ |
|
314 @{term "abs :: int \<Rightarrow> int"} & |
|
315 @{term "sgn :: int \<Rightarrow> int"}\\ |
|
316 \end{tabular} |
|
317 |
|
318 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
319 @{const Int.nat} & @{typeof Int.nat}\\ |
|
320 @{const Int.of_int} & @{typeof Int.of_int}\\ |
|
321 @{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"}\\ |
|
322 \end{tabular} |
|
323 |
|
324 \subsubsection*{Syntax} |
|
325 |
|
326 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
327 @{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\ |
|
328 \end{tabular} |
|
329 |
|
330 |
|
331 \section{Wellfounded} |
|
332 |
|
333 \begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
334 @{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\ |
|
335 @{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\<Rightarrow>bool"}\\ |
|
336 @{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\ |
|
337 @{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\ |
|
338 @{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\ |
|
339 @{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\ |
|
340 @{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ |
|
341 @{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ |
|
342 \end{supertabular} |
|
343 |
|
344 |
|
345 \section{Power} |
|
346 |
|
347 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
348 @{const Power.power} & @{typeof Power.power} |
|
349 \end{tabular} |
|
350 |
|
351 |
|
352 \section{Iterated Functions and Relations} |
|
353 |
|
354 Theory: @{theory Relation_Power} |
|
355 |
|
356 Iterated functions \ @{term[source]"(f::'a\<Rightarrow>'a) ^ n"} \ |
|
357 and relations \ @{term[source]"(r::('a\<times>'a)set) ^ n"}. |
|
358 |
|
359 |
|
360 \section{Option} |
|
361 |
|
362 @{datatype option} |
|
363 \bigskip |
|
364 |
|
365 \begin{tabular}{@ {} l @ {~::~} l @ {}} |
|
366 @{const Option.the} & @{typeof Option.the}\\ |
|
367 @{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\ |
|
368 @{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"} |
|
369 \end{tabular} |
|
370 |
|
371 \section{List} |
|
372 |
|
373 @{datatype list} |
|
374 \bigskip |
|
375 |
|
376 \begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
377 @{const List.append} & @{typeof List.append}\\ |
|
378 @{const List.butlast} & @{typeof List.butlast}\\ |
|
379 @{const List.concat} & @{typeof List.concat}\\ |
|
380 @{const List.distinct} & @{typeof List.distinct}\\ |
|
381 @{const List.drop} & @{typeof List.drop}\\ |
|
382 @{const List.dropWhile} & @{typeof List.dropWhile}\\ |
|
383 @{const List.filter} & @{typeof List.filter}\\ |
|
384 @{const List.foldl} & @{typeof List.foldl}\\ |
|
385 @{const List.foldr} & @{typeof List.foldr}\\ |
|
386 @{const List.hd} & @{typeof List.hd}\\ |
|
387 @{const List.last} & @{typeof List.last}\\ |
|
388 @{const List.length} & @{typeof List.length}\\ |
|
389 @{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
390 @{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
391 @{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\ |
|
392 @{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
393 @{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ |
|
394 @{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\ |
|
395 @{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\ |
|
396 @{const List.listsum} & @{typeof List.listsum}\\ |
|
397 @{const List.list_all2} & @{typeof List.list_all2}\\ |
|
398 @{const List.list_update} & @{typeof List.list_update}\\ |
|
399 @{const List.map} & @{typeof List.map}\\ |
|
400 @{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\ |
|
401 @{const List.remdups} & @{typeof List.remdups}\\ |
|
402 @{const List.removeAll} & @{typeof List.removeAll}\\ |
|
403 @{const List.remove1} & @{typeof List.remove1}\\ |
|
404 @{const List.replicate} & @{typeof List.replicate}\\ |
|
405 @{const List.rev} & @{typeof List.rev}\\ |
|
406 @{const List.rotate} & @{typeof List.rotate}\\ |
|
407 @{const List.rotate1} & @{typeof List.rotate1}\\ |
|
408 @{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\ |
|
409 @{const List.sort} & @{typeof List.sort}\\ |
|
410 @{const List.sorted} & @{typeof List.sorted}\\ |
|
411 @{const List.splice} & @{typeof List.splice}\\ |
|
412 @{const List.sublist} & @{typeof List.sublist}\\ |
|
413 @{const List.take} & @{typeof List.take}\\ |
|
414 @{const List.takeWhile} & @{typeof List.takeWhile}\\ |
|
415 @{const List.tl} & @{typeof List.tl}\\ |
|
416 @{const List.upt} & @{typeof List.upt}\\ |
|
417 @{const List.upto} & @{typeof List.upto}\\ |
|
418 @{const List.zip} & @{typeof List.zip}\\ |
|
419 \end{supertabular} |
|
420 |
|
421 \subsubsection*{Syntax} |
|
422 |
|
423 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
424 @{text"[x\<^isub>1,\<dots>,x\<^isub>n]"} & @{text"x\<^isub>1 # \<dots> # x\<^isub>n # []"}\\ |
|
425 @{term"[m..<n]"} & @{term[source]"upt m n"}\\ |
|
426 @{term"[i..j]"} & @{term[source]"upto i j"}\\ |
|
427 @{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\ |
|
428 @{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\ |
|
429 @{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ |
|
430 @{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\ |
|
431 \end{supertabular} |
|
432 \medskip |
|
433 |
|
434 Comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each |
|
435 qualifier @{text q\<^isub>i} is either a generator @{text"pat \<leftarrow> e"} or a |
|
436 guard, i.e.\ boolean expression. |
|
437 |
|
438 \section{Map} |
|
439 |
|
440 Maps model partial functions and are often used as finite tables. However, |
|
441 the domain of a map may be infinite. |
|
442 |
|
443 @{text"'a \<rightharpoonup> 'b = 'a \<Rightarrow> 'b option"} |
|
444 \bigskip |
|
445 |
|
446 \begin{supertabular}{@ {} l @ {~::~} l @ {}} |
|
447 @{const Map.empty} & @{typeof Map.empty}\\ |
|
448 @{const Map.map_add} & @{typeof Map.map_add}\\ |
|
449 @{const Map.map_comp} & @{typeof Map.map_comp}\\ |
|
450 @{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\ |
|
451 @{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\ |
|
452 @{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\ |
|
453 @{const Map.map_le} & @{typeof Map.map_le}\\ |
|
454 @{const Map.map_of} & @{typeof Map.map_of}\\ |
|
455 @{const Map.map_upds} & @{typeof Map.map_upds}\\ |
|
456 \end{supertabular} |
|
457 |
|
458 \subsubsection*{Syntax} |
|
459 |
|
460 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} |
|
461 @{text"empty"} & @{term"\<lambda>x. None"}\\ |
|
462 @{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ |
|
463 @{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)"}\\ |
|
464 @{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ |
|
465 \end{tabular} |
|
466 |
|
467 *} |
|
468 (*<*) |
|
469 end |
|
470 (*>*) |