basic setup for "main" as generated Isabelle manual;
authorwenzelm
Wed Mar 11 20:11:06 2009 +0100 (2009-03-11)
changeset 3045728b487cd9e15
parent 30456 d21bc48823b7
child 30458 804de935c328
basic setup for "main" as generated Isabelle manual;
doc-src/Main/Docs/Main_Doc.thy
doc-src/Main/Docs/ROOT.ML
doc-src/Main/Docs/document/Main_Doc.tex
doc-src/Main/IsaMakefile
doc-src/Main/Main_Doc.tex
doc-src/Main/Makefile
doc-src/Main/main.tex
doc/Contents
src/HOL/Docs/Main_Doc.thy
src/HOL/Docs/ROOT.ML
src/HOL/Docs/document/root.tex
src/HOL/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Main/Docs/Main_Doc.thy	Wed Mar 11 20:11:06 2009 +0100
     1.3 @@ -0,0 +1,572 @@
     1.4 +(*<*)
     1.5 +theory Main_Doc
     1.6 +imports Main
     1.7 +begin
     1.8 +
     1.9 +ML {*
    1.10 +fun pretty_term_type_only ctxt (t, T) =
    1.11 +  (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then ()
    1.12 +   else error "term_type_only: type mismatch";
    1.13 +   Syntax.pretty_typ ctxt T)
    1.14 +
    1.15 +val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
    1.16 +  (fn {source, context, ...} => fn arg =>
    1.17 +    ThyOutput.output
    1.18 +      (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg]));
    1.19 +*}
    1.20 +(*>*)
    1.21 +text{*
    1.22 +
    1.23 +\begin{abstract}
    1.24 +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/}.
    1.25 +\end{abstract}
    1.26 +
    1.27 +\section{HOL}
    1.28 +
    1.29 +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"}.
    1.30 +\smallskip
    1.31 +
    1.32 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
    1.33 +@{const HOL.undefined} & @{typeof HOL.undefined}\\
    1.34 +@{const HOL.default} & @{typeof HOL.default}\\
    1.35 +\end{tabular}
    1.36 +
    1.37 +\subsubsection*{Syntax}
    1.38 +
    1.39 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
    1.40 +@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"} & (\verb$~=$)\\
    1.41 +@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\
    1.42 +@{term"If x y z"} & @{term[source]"If x y z"}\\
    1.43 +@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\<lambda>x. e\<^isub>2)"}\\
    1.44 +\end{supertabular}
    1.45 +
    1.46 +
    1.47 +\section{Orderings}
    1.48 +
    1.49 +A collection of classes defining basic orderings:
    1.50 +preorder, partial order, linear order, dense linear order and wellorder.
    1.51 +\smallskip
    1.52 +
    1.53 +\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
    1.54 +@{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\
    1.55 +@{const HOL.less} & @{typeof HOL.less}\\
    1.56 +@{const Orderings.Least} & @{typeof Orderings.Least}\\
    1.57 +@{const Orderings.min} & @{typeof Orderings.min}\\
    1.58 +@{const Orderings.max} & @{typeof Orderings.max}\\
    1.59 +@{const[source] top} & @{typeof Orderings.top}\\
    1.60 +@{const[source] bot} & @{typeof Orderings.bot}\\
    1.61 +@{const Orderings.mono} & @{typeof Orderings.mono}\\
    1.62 +@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\
    1.63 +\end{supertabular}
    1.64 +
    1.65 +\subsubsection*{Syntax}
    1.66 +
    1.67 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
    1.68 +@{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\verb$>=$)\\
    1.69 +@{term[source]"x > y"} & @{term"x > y"}\\
    1.70 +@{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\
    1.71 +@{term"EX x<=y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\
    1.72 +\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
    1.73 +@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
    1.74 +\end{supertabular}
    1.75 +
    1.76 +
    1.77 +\section{Lattices}
    1.78 +
    1.79 +Classes semilattice, lattice, distributive lattice and complete lattice (the
    1.80 +latter in theory @{theory Set}).
    1.81 +
    1.82 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
    1.83 +@{const Lattices.inf} & @{typeof Lattices.inf}\\
    1.84 +@{const Lattices.sup} & @{typeof Lattices.sup}\\
    1.85 +@{const Set.Inf} & @{term_type_only Set.Inf "'a set \<Rightarrow> 'a::complete_lattice"}\\
    1.86 +@{const Set.Sup} & @{term_type_only Set.Sup "'a set \<Rightarrow> 'a::complete_lattice"}\\
    1.87 +\end{tabular}
    1.88 +
    1.89 +\subsubsection*{Syntax}
    1.90 +
    1.91 +Available by loading theory @{text Lattice_Syntax} in directory @{text
    1.92 +Library}.
    1.93 +
    1.94 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
    1.95 +@{text[source]"x \<sqsubseteq> y"} & @{term"x \<le> y"}\\
    1.96 +@{text[source]"x \<sqsubset> y"} & @{term"x < y"}\\
    1.97 +@{text[source]"x \<sqinter> y"} & @{term"inf x y"}\\
    1.98 +@{text[source]"x \<squnion> y"} & @{term"sup x y"}\\
    1.99 +@{text[source]"\<Sqinter> A"} & @{term"Sup A"}\\
   1.100 +@{text[source]"\<Squnion> A"} & @{term"Inf A"}\\
   1.101 +@{text[source]"\<top>"} & @{term[source] top}\\
   1.102 +@{text[source]"\<bottom>"} & @{term[source] bot}\\
   1.103 +\end{supertabular}
   1.104 +
   1.105 +
   1.106 +\section{Set}
   1.107 +
   1.108 +Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
   1.109 +\bigskip
   1.110 +
   1.111 +\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
   1.112 +@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
   1.113 +@{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
   1.114 +@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
   1.115 +@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
   1.116 +@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
   1.117 +@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
   1.118 +@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
   1.119 +@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
   1.120 +@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
   1.121 +@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\
   1.122 +@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\
   1.123 +@{const UNIV} & @{term_type_only UNIV "'a set"}\\
   1.124 +@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\
   1.125 +@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
   1.126 +@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
   1.127 +\end{supertabular}
   1.128 +
   1.129 +\subsubsection*{Syntax}
   1.130 +
   1.131 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   1.132 +@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\
   1.133 +@{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\
   1.134 +@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
   1.135 +@{term"A \<subset> B"} & @{term[source]"A < B"}\\
   1.136 +@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
   1.137 +@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
   1.138 +@{term"{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
   1.139 +@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
   1.140 +@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
   1.141 +@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
   1.142 +@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
   1.143 +@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
   1.144 +@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
   1.145 +@{term"range f"} & @{term[source]"f ` UNIV"}\\
   1.146 +\end{supertabular}
   1.147 +
   1.148 +
   1.149 +\section{Fun}
   1.150 +
   1.151 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.152 +@{const "Fun.id"} & @{typeof Fun.id}\\
   1.153 +@{const "Fun.comp"} & @{typeof Fun.comp}\\
   1.154 +@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\
   1.155 +@{const "Fun.inj"} & @{typeof Fun.inj}\\
   1.156 +@{const "Fun.surj"} & @{typeof Fun.surj}\\
   1.157 +@{const "Fun.bij"} & @{typeof Fun.bij}\\
   1.158 +@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\
   1.159 +@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\
   1.160 +\end{supertabular}
   1.161 +
   1.162 +\subsubsection*{Syntax}
   1.163 +
   1.164 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   1.165 +@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\
   1.166 +@{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)"}\\
   1.167 +\end{tabular}
   1.168 +
   1.169 +
   1.170 +\section{Fixed Points}
   1.171 +
   1.172 +Theory: @{theory Inductive}.
   1.173 +
   1.174 +Least and greatest fixed points in a complete lattice @{typ 'a}:
   1.175 +
   1.176 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   1.177 +@{const Inductive.lfp} & @{typeof Inductive.lfp}\\
   1.178 +@{const Inductive.gfp} & @{typeof Inductive.gfp}\\
   1.179 +\end{tabular}
   1.180 +
   1.181 +Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices.
   1.182 +
   1.183 +\section{Sum\_Type}
   1.184 +
   1.185 +Type constructor @{text"+"}.
   1.186 +
   1.187 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   1.188 +@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\
   1.189 +@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\
   1.190 +@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"}
   1.191 +\end{tabular}
   1.192 +
   1.193 +
   1.194 +\section{Product\_Type}
   1.195 +
   1.196 +Types @{typ unit} and @{text"\<times>"}.
   1.197 +
   1.198 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.199 +@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\
   1.200 +@{const Pair} & @{typeof Pair}\\
   1.201 +@{const fst} & @{typeof fst}\\
   1.202 +@{const snd} & @{typeof snd}\\
   1.203 +@{const split} & @{typeof split}\\
   1.204 +@{const curry} & @{typeof curry}\\
   1.205 +@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\
   1.206 +\end{supertabular}
   1.207 +
   1.208 +\subsubsection*{Syntax}
   1.209 +
   1.210 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
   1.211 +@{term"Pair a b"} & @{term[source]"Pair a b"}\\
   1.212 +@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\
   1.213 +@{term"A <*> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
   1.214 +\end{tabular}
   1.215 +
   1.216 +Pairs may be nested. Nesting to the right is printed as a tuple,
   1.217 +e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{@{text"(a, (b, c))"}.}
   1.218 +Pattern matching with pairs and tuples extends to all binders,
   1.219 +e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
   1.220 +
   1.221 +
   1.222 +\section{Relation}
   1.223 +
   1.224 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.225 +@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
   1.226 +@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('c*'a)set\<Rightarrow>('c*'b)set"}\\
   1.227 +@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\
   1.228 +@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\
   1.229 +@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\
   1.230 +@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\
   1.231 +@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\
   1.232 +@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\
   1.233 +@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\
   1.234 +@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
   1.235 +@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\
   1.236 +@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\
   1.237 +@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\
   1.238 +@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\
   1.239 +@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\
   1.240 +@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
   1.241 +@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\
   1.242 +\end{supertabular}
   1.243 +
   1.244 +\subsubsection*{Syntax}
   1.245 +
   1.246 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   1.247 +@{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$)
   1.248 +\end{tabular}
   1.249 +
   1.250 +\section{Equiv\_Relations}
   1.251 +
   1.252 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.253 +@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\
   1.254 +@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\
   1.255 +@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\
   1.256 +@{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"}\\
   1.257 +%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\
   1.258 +\end{supertabular}
   1.259 +
   1.260 +\subsubsection*{Syntax}
   1.261 +
   1.262 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   1.263 +@{term"congruent r f"} & @{term[source]"congruent r f"}\\
   1.264 +@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\
   1.265 +\end{tabular}
   1.266 +
   1.267 +
   1.268 +\section{Transitive\_Closure}
   1.269 +
   1.270 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   1.271 +@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
   1.272 +@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
   1.273 +@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
   1.274 +\end{tabular}
   1.275 +
   1.276 +\subsubsection*{Syntax}
   1.277 +
   1.278 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   1.279 +@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\verb$^*$)\\
   1.280 +@{term"trancl r"} & @{term[source]"trancl r"} & (\verb$^+$)\\
   1.281 +@{term"reflcl r"} & @{term[source]"reflcl r"} & (\verb$^=$)
   1.282 +\end{tabular}
   1.283 +
   1.284 +
   1.285 +\section{Algebra}
   1.286 +
   1.287 +Theories @{theory OrderedGroup}, @{theory Ring_and_Field} and @{theory
   1.288 +Divides} define a large collection of classes describing common algebraic
   1.289 +structures from semigroups up to fields. Everything is done in terms of
   1.290 +overloaded operators:
   1.291 +
   1.292 +\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
   1.293 +@{text "0"} & @{typeof zero}\\
   1.294 +@{text "1"} & @{typeof one}\\
   1.295 +@{const plus} & @{typeof plus}\\
   1.296 +@{const minus} & @{typeof minus}\\
   1.297 +@{const uminus} & @{typeof uminus} & (\verb$-$)\\
   1.298 +@{const times} & @{typeof times}\\
   1.299 +@{const inverse} & @{typeof inverse}\\
   1.300 +@{const divide} & @{typeof divide}\\
   1.301 +@{const abs} & @{typeof abs}\\
   1.302 +@{const sgn} & @{typeof sgn}\\
   1.303 +@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\
   1.304 +@{const div_class.div} & @{typeof "div_class.div"}\\
   1.305 +@{const div_class.mod} & @{typeof "div_class.mod"}\\
   1.306 +\end{supertabular}
   1.307 +
   1.308 +\subsubsection*{Syntax}
   1.309 +
   1.310 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   1.311 +@{term"abs x"} & @{term[source]"abs x"}
   1.312 +\end{tabular}
   1.313 +
   1.314 +
   1.315 +\section{Nat}
   1.316 +
   1.317 +@{datatype nat}
   1.318 +\bigskip
   1.319 +
   1.320 +\begin{tabular}{@ {} lllllll @ {}}
   1.321 +@{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   1.322 +@{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   1.323 +@{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   1.324 +@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   1.325 +@{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
   1.326 +@{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
   1.327 +@{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\
   1.328 +@{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
   1.329 +@{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
   1.330 +@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   1.331 +@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   1.332 +@{term "Min :: nat set \<Rightarrow> nat"} &
   1.333 +@{term "Max :: nat set \<Rightarrow> nat"}\\
   1.334 +\end{tabular}
   1.335 +
   1.336 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   1.337 +@{const Nat.of_nat} & @{typeof Nat.of_nat}
   1.338 +\end{tabular}
   1.339 +
   1.340 +\section{Int}
   1.341 +
   1.342 +Type @{typ int}
   1.343 +\bigskip
   1.344 +
   1.345 +\begin{tabular}{@ {} llllllll @ {}}
   1.346 +@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} &
   1.347 +@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} &
   1.348 +@{term "uminus :: int \<Rightarrow> int"} &
   1.349 +@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} &
   1.350 +@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} &
   1.351 +@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}&
   1.352 +@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}&
   1.353 +@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\
   1.354 +@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} &
   1.355 +@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} &
   1.356 +@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} &
   1.357 +@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} &
   1.358 +@{term "Min :: int set \<Rightarrow> int"} &
   1.359 +@{term "Max :: int set \<Rightarrow> int"}\\
   1.360 +@{term "abs :: int \<Rightarrow> int"} &
   1.361 +@{term "sgn :: int \<Rightarrow> int"}\\
   1.362 +\end{tabular}
   1.363 +
   1.364 +\begin{tabular}{@ {} l @ {~::~} l l @ {}}
   1.365 +@{const Int.nat} & @{typeof Int.nat}\\
   1.366 +@{const Int.of_int} & @{typeof Int.of_int}\\
   1.367 +@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\verb$Ints$)
   1.368 +\end{tabular}
   1.369 +
   1.370 +\subsubsection*{Syntax}
   1.371 +
   1.372 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   1.373 +@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\
   1.374 +\end{tabular}
   1.375 +
   1.376 +
   1.377 +\section{Finite\_Set}
   1.378 +
   1.379 +
   1.380 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.381 +@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\
   1.382 +@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\
   1.383 +@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
   1.384 +@{const Finite_Set.fold_image} & @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
   1.385 +@{const Finite_Set.setsum} & @{term_type_only Finite_Set.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
   1.386 +@{const Finite_Set.setprod} & @{term_type_only Finite_Set.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
   1.387 +\end{supertabular}
   1.388 +
   1.389 +
   1.390 +\subsubsection*{Syntax}
   1.391 +
   1.392 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   1.393 +@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\verb$SUM$)\\
   1.394 +@{term"setsum (%x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\
   1.395 +@{term[source]"\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\
   1.396 +\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}} & (\verb$PROD$)\\
   1.397 +\end{supertabular}
   1.398 +
   1.399 +
   1.400 +\section{Wellfounded}
   1.401 +
   1.402 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.403 +@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\
   1.404 +@{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\<Rightarrow>bool"}\\
   1.405 +@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\
   1.406 +@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\
   1.407 +@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\
   1.408 +@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\
   1.409 +@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\
   1.410 +@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\
   1.411 +\end{supertabular}
   1.412 +
   1.413 +
   1.414 +\section{SetInterval}
   1.415 +
   1.416 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.417 +@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
   1.418 +@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\
   1.419 +@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\
   1.420 +@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\
   1.421 +@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
   1.422 +@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
   1.423 +@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
   1.424 +@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
   1.425 +\end{supertabular}
   1.426 +
   1.427 +\subsubsection*{Syntax}
   1.428 +
   1.429 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   1.430 +@{term "lessThan y"} & @{term[source] "lessThan y"}\\
   1.431 +@{term "atMost y"} & @{term[source] "atMost y"}\\
   1.432 +@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\
   1.433 +@{term "atLeast x"} & @{term[source] "atLeast x"}\\
   1.434 +@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\
   1.435 +@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\
   1.436 +@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\
   1.437 +@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\
   1.438 +@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
   1.439 +@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\
   1.440 +\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
   1.441 +@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
   1.442 +@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
   1.443 +@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\
   1.444 +@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\
   1.445 +\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
   1.446 +\end{supertabular}
   1.447 +
   1.448 +
   1.449 +\section{Power}
   1.450 +
   1.451 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   1.452 +@{const Power.power} & @{typeof Power.power}
   1.453 +\end{tabular}
   1.454 +
   1.455 +
   1.456 +\section{Iterated Functions and Relations}
   1.457 +
   1.458 +Theory: @{theory Relation_Power}
   1.459 +
   1.460 +Iterated functions \ @{term[source]"(f::'a\<Rightarrow>'a) ^ n"} \
   1.461 +and relations \ @{term[source]"(r::('a\<times>'a)set) ^ n"}.
   1.462 +
   1.463 +
   1.464 +\section{Option}
   1.465 +
   1.466 +@{datatype option}
   1.467 +\bigskip
   1.468 +
   1.469 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   1.470 +@{const Option.the} & @{typeof Option.the}\\
   1.471 +@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
   1.472 +@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}
   1.473 +\end{tabular}
   1.474 +
   1.475 +\section{List}
   1.476 +
   1.477 +@{datatype list}
   1.478 +\bigskip
   1.479 +
   1.480 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.481 +@{const List.append} & @{typeof List.append}\\
   1.482 +@{const List.butlast} & @{typeof List.butlast}\\
   1.483 +@{const List.concat} & @{typeof List.concat}\\
   1.484 +@{const List.distinct} & @{typeof List.distinct}\\
   1.485 +@{const List.drop} & @{typeof List.drop}\\
   1.486 +@{const List.dropWhile} & @{typeof List.dropWhile}\\
   1.487 +@{const List.filter} & @{typeof List.filter}\\
   1.488 +@{const List.foldl} & @{typeof List.foldl}\\
   1.489 +@{const List.foldr} & @{typeof List.foldr}\\
   1.490 +@{const List.hd} & @{typeof List.hd}\\
   1.491 +@{const List.last} & @{typeof List.last}\\
   1.492 +@{const List.length} & @{typeof List.length}\\
   1.493 +@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   1.494 +@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   1.495 +@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\
   1.496 +@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   1.497 +@{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   1.498 +@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
   1.499 +@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
   1.500 +@{const List.listsum} & @{typeof List.listsum}\\
   1.501 +@{const List.list_all2} & @{typeof List.list_all2}\\
   1.502 +@{const List.list_update} & @{typeof List.list_update}\\
   1.503 +@{const List.map} & @{typeof List.map}\\
   1.504 +@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\
   1.505 +@{const List.remdups} & @{typeof List.remdups}\\
   1.506 +@{const List.removeAll} & @{typeof List.removeAll}\\
   1.507 +@{const List.remove1} & @{typeof List.remove1}\\
   1.508 +@{const List.replicate} & @{typeof List.replicate}\\
   1.509 +@{const List.rev} & @{typeof List.rev}\\
   1.510 +@{const List.rotate} & @{typeof List.rotate}\\
   1.511 +@{const List.rotate1} & @{typeof List.rotate1}\\
   1.512 +@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\
   1.513 +@{const List.sort} & @{typeof List.sort}\\
   1.514 +@{const List.sorted} & @{typeof List.sorted}\\
   1.515 +@{const List.splice} & @{typeof List.splice}\\
   1.516 +@{const List.sublist} & @{typeof List.sublist}\\
   1.517 +@{const List.take} & @{typeof List.take}\\
   1.518 +@{const List.takeWhile} & @{typeof List.takeWhile}\\
   1.519 +@{const List.tl} & @{typeof List.tl}\\
   1.520 +@{const List.upt} & @{typeof List.upt}\\
   1.521 +@{const List.upto} & @{typeof List.upto}\\
   1.522 +@{const List.zip} & @{typeof List.zip}\\
   1.523 +\end{supertabular}
   1.524 +
   1.525 +\subsubsection*{Syntax}
   1.526 +
   1.527 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   1.528 +@{text"[x\<^isub>1,\<dots>,x\<^isub>n]"} & @{text"x\<^isub>1 # \<dots> # x\<^isub>n # []"}\\
   1.529 +@{term"[m..<n]"} & @{term[source]"upt m n"}\\
   1.530 +@{term"[i..j]"} & @{term[source]"upto i j"}\\
   1.531 +@{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\
   1.532 +@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\
   1.533 +@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
   1.534 +@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
   1.535 +\end{supertabular}
   1.536 +\medskip
   1.537 +
   1.538 +List comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each
   1.539 +qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \<leftarrow> e"}} or a
   1.540 +guard, i.e.\ boolean expression.
   1.541 +
   1.542 +\section{Map}
   1.543 +
   1.544 +Maps model partial functions and are often used as finite tables. However,
   1.545 +the domain of a map may be infinite.
   1.546 +
   1.547 +@{text"'a \<rightharpoonup> 'b  =  'a \<Rightarrow> 'b option"}
   1.548 +\bigskip
   1.549 +
   1.550 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.551 +@{const Map.empty} & @{typeof Map.empty}\\
   1.552 +@{const Map.map_add} & @{typeof Map.map_add}\\
   1.553 +@{const Map.map_comp} & @{typeof Map.map_comp}\\
   1.554 +@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\
   1.555 +@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\
   1.556 +@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\
   1.557 +@{const Map.map_le} & @{typeof Map.map_le}\\
   1.558 +@{const Map.map_of} & @{typeof Map.map_of}\\
   1.559 +@{const Map.map_upds} & @{typeof Map.map_upds}\\
   1.560 +\end{supertabular}
   1.561 +
   1.562 +\subsubsection*{Syntax}
   1.563 +
   1.564 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   1.565 +@{term"Map.empty"} & @{term"\<lambda>x. None"}\\
   1.566 +@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\
   1.567 +@{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)"}\\
   1.568 +@{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)"}\\
   1.569 +@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\
   1.570 +\end{tabular}
   1.571 +
   1.572 +*}
   1.573 +(*<*)
   1.574 +end
   1.575 +(*>*)
   1.576 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/Main/Docs/ROOT.ML	Wed Mar 11 20:11:06 2009 +0100
     2.3 @@ -0,0 +1,1 @@
     2.4 +use_thy "Main_Doc";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/Main/Docs/document/Main_Doc.tex	Wed Mar 11 20:11:06 2009 +0100
     3.3 @@ -0,0 +1,597 @@
     3.4 +%
     3.5 +\begin{isabellebody}%
     3.6 +\def\isabellecontext{Main{\isacharunderscore}Doc}%
     3.7 +%
     3.8 +\isadelimtheory
     3.9 +%
    3.10 +\endisadelimtheory
    3.11 +%
    3.12 +\isatagtheory
    3.13 +%
    3.14 +\endisatagtheory
    3.15 +{\isafoldtheory}%
    3.16 +%
    3.17 +\isadelimtheory
    3.18 +%
    3.19 +\endisadelimtheory
    3.20 +%
    3.21 +\isadelimML
    3.22 +%
    3.23 +\endisadelimML
    3.24 +%
    3.25 +\isatagML
    3.26 +%
    3.27 +\endisatagML
    3.28 +{\isafoldML}%
    3.29 +%
    3.30 +\isadelimML
    3.31 +%
    3.32 +\endisadelimML
    3.33 +%
    3.34 +\begin{isamarkuptext}%
    3.35 +\begin{abstract}
    3.36 +This document lists the main types, functions and syntax provided by theory \isa{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/}.
    3.37 +\end{abstract}
    3.38 +
    3.39 +\section{HOL}
    3.40 +
    3.41 +The basic logic: \isa{x\ {\isacharequal}\ y}, \isa{True}, \isa{False}, \isa{{\isasymnot}\ P}, \isa{P\ {\isasymand}\ Q}, \isa{P\ {\isasymor}\ Q}, \isa{P\ {\isasymlongrightarrow}\ Q}, \isa{{\isasymforall}x{\isachardot}\ P}, \isa{{\isasymexists}x{\isachardot}\ P}, \isa{{\isasymexists}{\isacharbang}x{\isachardot}\ P}, \isa{THE\ x{\isachardot}\ P}.
    3.42 +\smallskip
    3.43 +
    3.44 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
    3.45 +\isa{undefined} & \isa{{\isacharprime}a}\\
    3.46 +\isa{default} & \isa{{\isacharprime}a}\\
    3.47 +\end{tabular}
    3.48 +
    3.49 +\subsubsection*{Syntax}
    3.50 +
    3.51 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
    3.52 +\isa{x\ {\isasymnoteq}\ y} & \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}} & (\verb$~=$)\\
    3.53 +\isa{{\isachardoublequote}P\ {\isasymlongleftrightarrow}\ Q{\isachardoublequote}} & \isa{P\ {\isacharequal}\ Q} \\
    3.54 +\isa{if\ x\ then\ y\ else\ z} & \isa{{\isachardoublequote}If\ x\ y\ z{\isachardoublequote}}\\
    3.55 +\isa{let\ x\ {\isacharequal}\ e\isactrlisub {\isadigit{1}}\ in\ e\isactrlisub {\isadigit{2}}} & \isa{{\isachardoublequote}Let\ e\isactrlisub {\isadigit{1}}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequote}}\\
    3.56 +\end{supertabular}
    3.57 +
    3.58 +
    3.59 +\section{Orderings}
    3.60 +
    3.61 +A collection of classes defining basic orderings:
    3.62 +preorder, partial order, linear order, dense linear order and wellorder.
    3.63 +\smallskip
    3.64 +
    3.65 +\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
    3.66 +\isa{op\ {\isasymle}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (\verb$<=$)\\
    3.67 +\isa{op\ {\isacharless}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\
    3.68 +\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\
    3.69 +\isa{min} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
    3.70 +\isa{max} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
    3.71 +\isa{top} & \isa{{\isacharprime}a}\\
    3.72 +\isa{bot} & \isa{{\isacharprime}a}\\
    3.73 +\isa{mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
    3.74 +\isa{strict{\isacharunderscore}mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
    3.75 +\end{supertabular}
    3.76 +
    3.77 +\subsubsection*{Syntax}
    3.78 +
    3.79 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
    3.80 +\isa{{\isachardoublequote}x\ {\isasymge}\ y{\isachardoublequote}} & \isa{y\ {\isasymle}\ x} & (\verb$>=$)\\
    3.81 +\isa{{\isachardoublequote}x\ {\isachargreater}\ y{\isachardoublequote}} & \isa{y\ {\isacharless}\ x}\\
    3.82 +\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P{\isachardoublequote}}\\
    3.83 +\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P{\isachardoublequote}}\\
    3.84 +\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
    3.85 +\isa{LEAST\ x{\isachardot}\ P} & \isa{{\isachardoublequote}Least\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\
    3.86 +\end{supertabular}
    3.87 +
    3.88 +
    3.89 +\section{Lattices}
    3.90 +
    3.91 +Classes semilattice, lattice, distributive lattice and complete lattice (the
    3.92 +latter in theory \isa{Set}).
    3.93 +
    3.94 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
    3.95 +\isa{inf} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
    3.96 +\isa{sup} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
    3.97 +\isa{Inf} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\
    3.98 +\isa{Sup} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\
    3.99 +\end{tabular}
   3.100 +
   3.101 +\subsubsection*{Syntax}
   3.102 +
   3.103 +Available by loading theory \isa{Lattice{\isacharunderscore}Syntax} in directory \isa{Library}.
   3.104 +
   3.105 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   3.106 +\isa{{\isachardoublequote}x\ {\isasymsqsubseteq}\ y{\isachardoublequote}} & \isa{x\ {\isasymle}\ y}\\
   3.107 +\isa{{\isachardoublequote}x\ {\isasymsqsubset}\ y{\isachardoublequote}} & \isa{x\ {\isacharless}\ y}\\
   3.108 +\isa{{\isachardoublequote}x\ {\isasymsqinter}\ y{\isachardoublequote}} & \isa{inf\ x\ y}\\
   3.109 +\isa{{\isachardoublequote}x\ {\isasymsqunion}\ y{\isachardoublequote}} & \isa{sup\ x\ y}\\
   3.110 +\isa{{\isachardoublequote}{\isasymSqinter}\ A{\isachardoublequote}} & \isa{Sup\ A}\\
   3.111 +\isa{{\isachardoublequote}{\isasymSqunion}\ A{\isachardoublequote}} & \isa{Inf\ A}\\
   3.112 +\isa{{\isachardoublequote}{\isasymtop}{\isachardoublequote}} & \isa{top}\\
   3.113 +\isa{{\isachardoublequote}{\isasymbottom}{\isachardoublequote}} & \isa{bot}\\
   3.114 +\end{supertabular}
   3.115 +
   3.116 +
   3.117 +\section{Set}
   3.118 +
   3.119 +Sets are predicates: \isa{{\isachardoublequote}{\isacharprime}a\ set\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}}
   3.120 +\bigskip
   3.121 +
   3.122 +\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
   3.123 +\isa{{\isacharbraceleft}{\isacharbraceright}} & \isa{{\isacharprime}a\ set}\\
   3.124 +\isa{insert} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.125 +\isa{Collect} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.126 +\isa{op\ {\isasymin}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool} & (\texttt{:})\\
   3.127 +\isa{op\ {\isasymunion}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Un})\\
   3.128 +\isa{op\ {\isasyminter}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Int})\\
   3.129 +\isa{UNION} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   3.130 +\isa{INTER} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   3.131 +\isa{Union} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.132 +\isa{Inter} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.133 +\isa{Pow} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\
   3.134 +\isa{UNIV} & \isa{{\isacharprime}a\ set}\\
   3.135 +\isa{op\ {\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   3.136 +\isa{Ball} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   3.137 +\isa{Bex} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   3.138 +\end{supertabular}
   3.139 +
   3.140 +\subsubsection*{Syntax}
   3.141 +
   3.142 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   3.143 +\isa{{\isacharbraceleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharbraceright}} & \isa{insert\ x\isactrlisub {\isadigit{1}}\ {\isacharparenleft}{\isasymdots}\ {\isacharparenleft}insert\ x\isactrlisub n\ {\isacharbraceleft}{\isacharbraceright}{\isacharparenright}{\isasymdots}{\isacharparenright}}\\
   3.144 +\isa{x\ {\isasymnotin}\ A} & \isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isasymin}\ A{\isacharparenright}{\isachardoublequote}}\\
   3.145 +\isa{A\ {\isasymsubseteq}\ B} & \isa{{\isachardoublequote}A\ {\isasymle}\ B{\isachardoublequote}}\\
   3.146 +\isa{A\ {\isasymsubset}\ B} & \isa{{\isachardoublequote}A\ {\isacharless}\ B{\isachardoublequote}}\\
   3.147 +\isa{{\isachardoublequote}A\ {\isasymsupseteq}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isasymle}\ A{\isachardoublequote}}\\
   3.148 +\isa{{\isachardoublequote}A\ {\isasymsupset}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isacharless}\ A{\isachardoublequote}}\\
   3.149 +\isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}} & \isa{{\isachardoublequote}Collect\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\
   3.150 +\isa{{\isasymUnion}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{UN})\\
   3.151 +\isa{{\isasymUnion}x{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\
   3.152 +\isa{{\isasymInter}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{INT})\\
   3.153 +\isa{{\isasymInter}x{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\
   3.154 +\isa{{\isasymforall}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Ball\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\
   3.155 +\isa{{\isasymexists}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Bex\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\
   3.156 +\isa{range\ f} & \isa{{\isachardoublequote}f\ {\isacharbackquote}\ UNIV{\isachardoublequote}}\\
   3.157 +\end{supertabular}
   3.158 +
   3.159 +
   3.160 +\section{Fun}
   3.161 +
   3.162 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   3.163 +\isa{id} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.164 +\isa{op\ {\isasymcirc}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}b}\\
   3.165 +\isa{inj{\isacharunderscore}on} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\
   3.166 +\isa{inj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   3.167 +\isa{surj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   3.168 +\isa{bij} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   3.169 +\isa{bij{\isacharunderscore}betw} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ bool}\\
   3.170 +\isa{fun{\isacharunderscore}upd} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b}\\
   3.171 +\end{supertabular}
   3.172 +
   3.173 +\subsubsection*{Syntax}
   3.174 +
   3.175 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   3.176 +\isa{f{\isacharparenleft}x\ {\isacharcolon}{\isacharequal}\ y{\isacharparenright}} & \isa{{\isachardoublequote}fun{\isacharunderscore}upd\ f\ x\ y{\isachardoublequote}}\\
   3.177 +\isa{f{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharequal}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharcolon}{\isacharequal}y\isactrlisub n{\isacharparenright}} & \isa{f{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharequal}y\isactrlisub {\isadigit{1}}{\isacharparenright}{\isasymdots}{\isacharparenleft}x\isactrlisub n{\isacharcolon}{\isacharequal}y\isactrlisub n{\isacharparenright}}\\
   3.178 +\end{tabular}
   3.179 +
   3.180 +
   3.181 +\section{Fixed Points}
   3.182 +
   3.183 +Theory: \isa{Inductive}.
   3.184 +
   3.185 +Least and greatest fixed points in a complete lattice \isa{{\isacharprime}a}:
   3.186 +
   3.187 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   3.188 +\isa{lfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.189 +\isa{gfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.190 +\end{tabular}
   3.191 +
   3.192 +Note that in particular sets (\isa{{\isacharprime}a\ {\isasymRightarrow}\ bool}) are complete lattices.
   3.193 +
   3.194 +\section{Sum\_Type}
   3.195 +
   3.196 +Type constructor \isa{{\isacharplus}}.
   3.197 +
   3.198 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   3.199 +\isa{Inl} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isacharplus}\ {\isacharprime}b}\\
   3.200 +\isa{Inr} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isacharplus}\ {\isacharprime}a}\\
   3.201 +\isa{op\ {\isacharless}{\isacharplus}{\isachargreater}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharplus}\ {\isacharprime}b{\isacharparenright}\ set}
   3.202 +\end{tabular}
   3.203 +
   3.204 +
   3.205 +\section{Product\_Type}
   3.206 +
   3.207 +Types \isa{unit} and \isa{{\isasymtimes}}.
   3.208 +
   3.209 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   3.210 +\isa{{\isacharparenleft}{\isacharparenright}} & \isa{unit}\\
   3.211 +\isa{Pair} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}\\
   3.212 +\isa{fst} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.213 +\isa{snd} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\
   3.214 +\isa{split} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\
   3.215 +\isa{curry} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\
   3.216 +\isa{Sigma} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
   3.217 +\end{supertabular}
   3.218 +
   3.219 +\subsubsection*{Syntax}
   3.220 +
   3.221 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
   3.222 +\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}} & \isa{{\isachardoublequote}Pair\ a\ b{\isachardoublequote}}\\
   3.223 +\isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} & \isa{{\isachardoublequote}split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}{\isachardoublequote}}\\
   3.224 +\isa{A\ {\isasymtimes}\ B} &  \isa{Sigma\ A\ {\isacharparenleft}{\isasymlambda}\_{\isachardot}\ B{\isacharparenright}} & (\verb$<*>$)
   3.225 +\end{tabular}
   3.226 +
   3.227 +Pairs may be nested. Nesting to the right is printed as a tuple,
   3.228 +e.g.\ \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ c{\isacharparenright}}} is really \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ {\isacharparenleft}b{\isacharcomma}\ c{\isacharparenright}{\isacharparenright}}.}
   3.229 +Pattern matching with pairs and tuples extends to all binders,
   3.230 +e.g.\ \mbox{\isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ P},} \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ P{\isacharbraceright}}, etc.
   3.231 +
   3.232 +
   3.233 +\section{Relation}
   3.234 +
   3.235 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   3.236 +\isa{converse} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   3.237 +\isa{op\ O} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
   3.238 +\isa{op\ {\isacharbackquote}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   3.239 +\isa{inv{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
   3.240 +\isa{Id{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   3.241 +\isa{Id} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   3.242 +\isa{Domain} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.243 +\isa{Range} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   3.244 +\isa{Field} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.245 +\isa{refl{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.246 +\isa{refl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.247 +\isa{sym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.248 +\isa{antisym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.249 +\isa{trans} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.250 +\isa{irrefl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.251 +\isa{total{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.252 +\isa{total} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.253 +\end{supertabular}
   3.254 +
   3.255 +\subsubsection*{Syntax}
   3.256 +
   3.257 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   3.258 +\isa{r{\isasyminverse}} & \isa{{\isachardoublequote}converse\ r{\isachardoublequote}} & (\verb$^-1$)
   3.259 +\end{tabular}
   3.260 +
   3.261 +\section{Equiv\_Relations}
   3.262 +
   3.263 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   3.264 +\isa{equiv} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.265 +\isa{op\ {\isacharslash}{\isacharslash}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\
   3.266 +\isa{congruent} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   3.267 +\isa{congruent{\isadigit{2}}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   3.268 +%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\
   3.269 +\end{supertabular}
   3.270 +
   3.271 +\subsubsection*{Syntax}
   3.272 +
   3.273 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   3.274 +\isa{f\ respects\ r} & \isa{{\isachardoublequote}congruent\ r\ f{\isachardoublequote}}\\
   3.275 +\isa{f\ respects{\isadigit{2}}\ r} & \isa{{\isachardoublequote}congruent{\isadigit{2}}\ r\ r\ f{\isachardoublequote}}\\
   3.276 +\end{tabular}
   3.277 +
   3.278 +
   3.279 +\section{Transitive\_Closure}
   3.280 +
   3.281 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   3.282 +\isa{rtrancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   3.283 +\isa{trancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   3.284 +\isa{reflcl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   3.285 +\end{tabular}
   3.286 +
   3.287 +\subsubsection*{Syntax}
   3.288 +
   3.289 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   3.290 +\isa{r\isactrlsup {\isacharasterisk}} & \isa{{\isachardoublequote}rtrancl\ r{\isachardoublequote}} & (\verb$^*$)\\
   3.291 +\isa{r\isactrlsup {\isacharplus}} & \isa{{\isachardoublequote}trancl\ r{\isachardoublequote}} & (\verb$^+$)\\
   3.292 +\isa{r\isactrlsup {\isacharequal}} & \isa{{\isachardoublequote}reflcl\ r{\isachardoublequote}} & (\verb$^=$)
   3.293 +\end{tabular}
   3.294 +
   3.295 +
   3.296 +\section{Algebra}
   3.297 +
   3.298 +Theories \isa{OrderedGroup}, \isa{Ring{\isacharunderscore}and{\isacharunderscore}Field} and \isa{Divides} define a large collection of classes describing common algebraic
   3.299 +structures from semigroups up to fields. Everything is done in terms of
   3.300 +overloaded operators:
   3.301 +
   3.302 +\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
   3.303 +\isa{{\isadigit{0}}} & \isa{{\isacharprime}a}\\
   3.304 +\isa{{\isadigit{1}}} & \isa{{\isacharprime}a}\\
   3.305 +\isa{op\ {\isacharplus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.306 +\isa{op\ {\isacharminus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.307 +\isa{uminus} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (\verb$-$)\\
   3.308 +\isa{op\ {\isacharasterisk}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.309 +\isa{inverse} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.310 +\isa{op\ {\isacharslash}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.311 +\isa{abs} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.312 +\isa{sgn} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.313 +\isa{op\ dvd} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\
   3.314 +\isa{op\ div} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.315 +\isa{op\ mod} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.316 +\end{supertabular}
   3.317 +
   3.318 +\subsubsection*{Syntax}
   3.319 +
   3.320 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   3.321 +\isa{{\isasymbar}x{\isasymbar}} & \isa{{\isachardoublequote}abs\ x{\isachardoublequote}}
   3.322 +\end{tabular}
   3.323 +
   3.324 +
   3.325 +\section{Nat}
   3.326 +
   3.327 +\isa{\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat}
   3.328 +\bigskip
   3.329 +
   3.330 +\begin{tabular}{@ {} lllllll @ {}}
   3.331 +\isa{op\ {\isacharplus}} &
   3.332 +\isa{op\ {\isacharminus}} &
   3.333 +\isa{op\ {\isacharasterisk}} &
   3.334 +\isa{op\ {\isacharcircum}} &
   3.335 +\isa{op\ div}&
   3.336 +\isa{op\ mod}&
   3.337 +\isa{op\ dvd}\\
   3.338 +\isa{op\ {\isasymle}} &
   3.339 +\isa{op\ {\isacharless}} &
   3.340 +\isa{min} &
   3.341 +\isa{max} &
   3.342 +\isa{Min} &
   3.343 +\isa{Max}\\
   3.344 +\end{tabular}
   3.345 +
   3.346 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   3.347 +\isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a}
   3.348 +\end{tabular}
   3.349 +
   3.350 +\section{Int}
   3.351 +
   3.352 +Type \isa{int}
   3.353 +\bigskip
   3.354 +
   3.355 +\begin{tabular}{@ {} llllllll @ {}}
   3.356 +\isa{op\ {\isacharplus}} &
   3.357 +\isa{op\ {\isacharminus}} &
   3.358 +\isa{uminus} &
   3.359 +\isa{op\ {\isacharasterisk}} &
   3.360 +\isa{op\ {\isacharcircum}} &
   3.361 +\isa{op\ div}&
   3.362 +\isa{op\ mod}&
   3.363 +\isa{op\ dvd}\\
   3.364 +\isa{op\ {\isasymle}} &
   3.365 +\isa{op\ {\isacharless}} &
   3.366 +\isa{min} &
   3.367 +\isa{max} &
   3.368 +\isa{Min} &
   3.369 +\isa{Max}\\
   3.370 +\isa{abs} &
   3.371 +\isa{sgn}\\
   3.372 +\end{tabular}
   3.373 +
   3.374 +\begin{tabular}{@ {} l @ {~::~} l l @ {}}
   3.375 +\isa{nat} & \isa{int\ {\isasymRightarrow}\ nat}\\
   3.376 +\isa{of{\isacharunderscore}int} & \isa{int\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.377 +\isa{{\isasymint}} & \isa{{\isacharprime}a\ set} & (\verb$Ints$)
   3.378 +\end{tabular}
   3.379 +
   3.380 +\subsubsection*{Syntax}
   3.381 +
   3.382 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   3.383 +\isa{int} & \isa{{\isachardoublequote}of{\isacharunderscore}nat{\isachardoublequote}}\\
   3.384 +\end{tabular}
   3.385 +
   3.386 +
   3.387 +\section{Finite\_Set}
   3.388 +
   3.389 +
   3.390 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   3.391 +\isa{finite} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\
   3.392 +\isa{card} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ nat}\\
   3.393 +\isa{fold} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\
   3.394 +\isa{fold{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\
   3.395 +\isa{setsum} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\
   3.396 +\isa{setprod} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\
   3.397 +\end{supertabular}
   3.398 +
   3.399 +
   3.400 +\subsubsection*{Syntax}
   3.401 +
   3.402 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   3.403 +\isa{{\isasymSum}A} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x{\isacharparenright}\ A{\isachardoublequote}} & (\verb$SUM$)\\
   3.404 +\isa{{\isasymSum}x{\isasymin}A{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ A{\isachardoublequote}}\\
   3.405 +\isa{{\isachardoublequote}{\isasymSum}x{\isacharbar}P{\isachardot}\ t{\isachardoublequote}} & \isa{{\isasymSum}x{\isasymin}{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}{\isachardot}\ t}\\
   3.406 +\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}} & (\verb$PROD$)\\
   3.407 +\end{supertabular}
   3.408 +
   3.409 +
   3.410 +\section{Wellfounded}
   3.411 +
   3.412 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   3.413 +\isa{wf} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.414 +\isa{acyclic} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   3.415 +\isa{acc} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.416 +\isa{measure} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   3.417 +\isa{op\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
   3.418 +\isa{op\ {\isacharless}{\isacharasterisk}mlex{\isacharasterisk}{\isachargreater}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   3.419 +\isa{less{\isacharunderscore}than} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\
   3.420 +\isa{pred{\isacharunderscore}nat} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\
   3.421 +\end{supertabular}
   3.422 +
   3.423 +
   3.424 +\section{SetInterval}
   3.425 +
   3.426 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   3.427 +\isa{lessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.428 +\isa{atMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.429 +\isa{greaterThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.430 +\isa{atLeast} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.431 +\isa{greaterThanLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.432 +\isa{atLeastLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.433 +\isa{greaterThanAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.434 +\isa{atLeastAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.435 +\end{supertabular}
   3.436 +
   3.437 +\subsubsection*{Syntax}
   3.438 +
   3.439 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   3.440 +\isa{{\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}lessThan\ y{\isachardoublequote}}\\
   3.441 +\isa{{\isacharbraceleft}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atMost\ y{\isachardoublequote}}\\
   3.442 +\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThan\ x{\isachardoublequote}}\\
   3.443 +\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}atLeast\ x{\isachardoublequote}}\\
   3.444 +\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanLessThan\ x\ y{\isachardoublequote}}\\
   3.445 +\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastLessThan\ x\ y{\isachardoublequote}}\\
   3.446 +\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanAtMost\ x\ y{\isachardoublequote}}\\
   3.447 +\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastAtMost\ x\ y{\isachardoublequote}}\\
   3.448 +\isa{{\isasymUnion}\ i{\isasymle}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\
   3.449 +\isa{{\isasymUnion}\ i{\isacharless}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\
   3.450 +\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymInter}} instead of \isa{{\isasymUnion}}}\\
   3.451 +\isa{{\isasymSum}x\ {\isacharequal}\ a{\isachardot}{\isachardot}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}a{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\
   3.452 +\isa{{\isasymSum}x\ {\isacharequal}\ a{\isachardot}{\isachardot}{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}a{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\
   3.453 +\isa{{\isasymSum}x{\isasymle}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\
   3.454 +\isa{{\isasymSum}x{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\
   3.455 +\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}}\\
   3.456 +\end{supertabular}
   3.457 +
   3.458 +
   3.459 +\section{Power}
   3.460 +
   3.461 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   3.462 +\isa{op\ {\isacharcircum}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a}
   3.463 +\end{tabular}
   3.464 +
   3.465 +
   3.466 +\section{Iterated Functions and Relations}
   3.467 +
   3.468 +Theory: \isa{Relation{\isacharunderscore}Power}
   3.469 +
   3.470 +Iterated functions \ \isa{{\isachardoublequote}{\isacharparenleft}f{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isasymRightarrow}{\isacharprime}a{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}} \
   3.471 +and relations \ \isa{{\isachardoublequote}{\isacharparenleft}r{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}a{\isacharparenright}set{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}}.
   3.472 +
   3.473 +
   3.474 +\section{Option}
   3.475 +
   3.476 +\isa{\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a}
   3.477 +\bigskip
   3.478 +
   3.479 +\begin{tabular}{@ {} l @ {~::~} l @ {}}
   3.480 +\isa{the} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.481 +\isa{Option{\isachardot}map} & \isa{{\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequote}}\\
   3.482 +\isa{Option{\isachardot}set} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a\ set}
   3.483 +\end{tabular}
   3.484 +
   3.485 +\section{List}
   3.486 +
   3.487 +\isa{\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ op\ {\isacharhash}\ {\isacharprime}a\ {\isacharparenleft}{\isacharprime}a\ list{\isacharparenright}}
   3.488 +\bigskip
   3.489 +
   3.490 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   3.491 +\isa{op\ {\isacharat}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.492 +\isa{butlast} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.493 +\isa{concat} & \isa{{\isacharprime}a\ list\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.494 +\isa{distinct} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\
   3.495 +\isa{drop} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.496 +\isa{dropWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.497 +\isa{filter} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.498 +\isa{foldl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.499 +\isa{foldr} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\
   3.500 +\isa{hd} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.501 +\isa{last} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.502 +\isa{length} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat}\\
   3.503 +\isa{lenlex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   3.504 +\isa{lex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   3.505 +\isa{lexn} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   3.506 +\isa{lexord} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   3.507 +\isa{listrel} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   3.508 +\isa{lists} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\
   3.509 +\isa{listset} & \isa{{\isacharprime}a\ set\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\
   3.510 +\isa{listsum} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\
   3.511 +\isa{list{\isacharunderscore}all{\isadigit{2}}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ bool}\\
   3.512 +\isa{list{\isacharunderscore}update} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.513 +\isa{map} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list}\\
   3.514 +\isa{measures} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   3.515 +\isa{remdups} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.516 +\isa{removeAll} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.517 +\isa{remove{\isadigit{1}}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.518 +\isa{replicate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.519 +\isa{rev} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.520 +\isa{rotate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.521 +\isa{rotate{\isadigit{1}}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.522 +\isa{set} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.523 +\isa{sort} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.524 +\isa{sorted} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\
   3.525 +\isa{splice} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.526 +\isa{sublist} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.527 +\isa{take} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.528 +\isa{takeWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.529 +\isa{tl} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.530 +\isa{upt} & \isa{nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ list}\\
   3.531 +\isa{upto} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   3.532 +\isa{zip} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list}\\
   3.533 +\end{supertabular}
   3.534 +
   3.535 +\subsubsection*{Syntax}
   3.536 +
   3.537 +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   3.538 +\isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharbrackright}} & \isa{x\isactrlisub {\isadigit{1}}\ {\isacharhash}\ {\isasymdots}\ {\isacharhash}\ x\isactrlisub n\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}\\
   3.539 +\isa{{\isacharbrackleft}m{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}} & \isa{{\isachardoublequote}upt\ m\ n{\isachardoublequote}}\\
   3.540 +\isa{{\isacharbrackleft}i{\isachardot}{\isachardot}j{\isacharbrackright}} & \isa{{\isachardoublequote}upto\ i\ j{\isachardoublequote}}\\
   3.541 +\isa{{\isacharbrackleft}e{\isachardot}\ x\ {\isasymleftarrow}\ xs{\isacharbrackright}} & \isa{map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs}\\
   3.542 +\isa{{\isacharbrackleft}x{\isasymleftarrow}xs\ {\isachardot}\ b{\isacharbrackright}} & \isa{{\isachardoublequote}filter\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}\ xs{\isachardoublequote}} \\
   3.543 +\isa{xs{\isacharbrackleft}n\ {\isacharcolon}{\isacharequal}\ x{\isacharbrackright}} & \isa{{\isachardoublequote}list{\isacharunderscore}update\ xs\ n\ x{\isachardoublequote}}\\
   3.544 +\isa{{\isasymSum}x{\isasymleftarrow}xs{\isachardot}\ e} & \isa{{\isachardoublequote}listsum\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}}\\
   3.545 +\end{supertabular}
   3.546 +\medskip
   3.547 +
   3.548 +List comprehension: \isa{{\isacharbrackleft}e{\isachardot}\ q\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ q\isactrlisub n{\isacharbrackright}} where each
   3.549 +qualifier \isa{q\isactrlisub i} is either a generator \mbox{\isa{pat\ {\isasymleftarrow}\ e}} or a
   3.550 +guard, i.e.\ boolean expression.
   3.551 +
   3.552 +\section{Map}
   3.553 +
   3.554 +Maps model partial functions and are often used as finite tables. However,
   3.555 +the domain of a map may be infinite.
   3.556 +
   3.557 +\isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option}
   3.558 +\bigskip
   3.559 +
   3.560 +\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   3.561 +\isa{Map{\isachardot}empty} & \isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   3.562 +\isa{op\ {\isacharplus}{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   3.563 +\isa{op\ {\isasymcirc}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymrightharpoonup}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   3.564 +\isa{op\ {\isacharbar}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   3.565 +\isa{dom} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   3.566 +\isa{ran} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   3.567 +\isa{op\ {\isasymsubseteq}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   3.568 +\isa{map{\isacharunderscore}of} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   3.569 +\isa{map{\isacharunderscore}upds} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   3.570 +\end{supertabular}
   3.571 +
   3.572 +\subsubsection*{Syntax}
   3.573 +
   3.574 +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   3.575 +\isa{Map{\isachardot}empty} & \isa{{\isasymlambda}x{\isachardot}\ None}\\
   3.576 +\isa{m{\isacharparenleft}x\ {\isasymmapsto}\ y{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x{\isacharcolon}{\isacharequal}Some\ y{\isacharparenright}{\isachardoublequote}}\\
   3.577 +\isa{m{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharparenright}{\isasymdots}{\isacharparenleft}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}{\isachardoublequote}}\\
   3.578 +\isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharbrackright}} & \isa{{\isachardoublequote}Map{\isachardot}empty{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}{\isachardoublequote}}\\
   3.579 +\isa{m{\isacharparenleft}xs\ {\isacharbrackleft}{\isasymmapsto}{\isacharbrackright}\ ys{\isacharparenright}} & \isa{{\isachardoublequote}map{\isacharunderscore}upds\ m\ xs\ ys{\isachardoublequote}}\\
   3.580 +\end{tabular}%
   3.581 +\end{isamarkuptext}%
   3.582 +\isamarkuptrue%
   3.583 +%
   3.584 +\isadelimtheory
   3.585 +%
   3.586 +\endisadelimtheory
   3.587 +%
   3.588 +\isatagtheory
   3.589 +%
   3.590 +\endisatagtheory
   3.591 +{\isafoldtheory}%
   3.592 +%
   3.593 +\isadelimtheory
   3.594 +%
   3.595 +\endisadelimtheory
   3.596 +\end{isabellebody}%
   3.597 +%%% Local Variables:
   3.598 +%%% mode: latex
   3.599 +%%% TeX-master: "root"
   3.600 +%%% End:
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/Main/IsaMakefile	Wed Mar 11 20:11:06 2009 +0100
     4.3 @@ -0,0 +1,31 @@
     4.4 +
     4.5 +## targets
     4.6 +
     4.7 +default: HOL-Docs
     4.8 +images:
     4.9 +test: HOL-Docs
    4.10 +
    4.11 +all: images test
    4.12 +
    4.13 +
    4.14 +## global settings
    4.15 +
    4.16 +SRC = $(ISABELLE_HOME)/src
    4.17 +OUT = $(ISABELLE_OUTPUT)
    4.18 +LOG = $(OUT)/log
    4.19 +
    4.20 +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    4.21 +
    4.22 +
    4.23 +## sessions
    4.24 +
    4.25 +HOL-Docs: $(LOG)/HOL-Docs.gz
    4.26 +
    4.27 +$(LOG)/HOL-Docs.gz: Docs/Main_Doc.thy Docs/ROOT.ML
    4.28 +	@$(USEDIR) HOL Docs
    4.29 +
    4.30 +
    4.31 +## clean
    4.32 +
    4.33 +clean:
    4.34 +	@rm -f $(LOG)/HOL-Docs.gz
     5.1 --- a/doc-src/Main/Main_Doc.tex	Wed Mar 11 20:09:23 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,597 +0,0 @@
     5.4 -%
     5.5 -\begin{isabellebody}%
     5.6 -\def\isabellecontext{Main{\isacharunderscore}Doc}%
     5.7 -%
     5.8 -\isadelimtheory
     5.9 -%
    5.10 -\endisadelimtheory
    5.11 -%
    5.12 -\isatagtheory
    5.13 -%
    5.14 -\endisatagtheory
    5.15 -{\isafoldtheory}%
    5.16 -%
    5.17 -\isadelimtheory
    5.18 -%
    5.19 -\endisadelimtheory
    5.20 -%
    5.21 -\isadelimML
    5.22 -%
    5.23 -\endisadelimML
    5.24 -%
    5.25 -\isatagML
    5.26 -%
    5.27 -\endisatagML
    5.28 -{\isafoldML}%
    5.29 -%
    5.30 -\isadelimML
    5.31 -%
    5.32 -\endisadelimML
    5.33 -%
    5.34 -\begin{isamarkuptext}%
    5.35 -\begin{abstract}
    5.36 -This document lists the main types, functions and syntax provided by theory \isa{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/}.
    5.37 -\end{abstract}
    5.38 -
    5.39 -\section{HOL}
    5.40 -
    5.41 -The basic logic: \isa{x\ {\isacharequal}\ y}, \isa{True}, \isa{False}, \isa{{\isasymnot}\ P}, \isa{P\ {\isasymand}\ Q}, \isa{P\ {\isasymor}\ Q}, \isa{P\ {\isasymlongrightarrow}\ Q}, \isa{{\isasymforall}x{\isachardot}\ P}, \isa{{\isasymexists}x{\isachardot}\ P}, \isa{{\isasymexists}{\isacharbang}x{\isachardot}\ P}, \isa{THE\ x{\isachardot}\ P}.
    5.42 -\smallskip
    5.43 -
    5.44 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
    5.45 -\isa{undefined} & \isa{{\isacharprime}a}\\
    5.46 -\isa{default} & \isa{{\isacharprime}a}\\
    5.47 -\end{tabular}
    5.48 -
    5.49 -\subsubsection*{Syntax}
    5.50 -
    5.51 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
    5.52 -\isa{x\ {\isasymnoteq}\ y} & \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}} & (\verb$~=$)\\
    5.53 -\isa{{\isachardoublequote}P\ {\isasymlongleftrightarrow}\ Q{\isachardoublequote}} & \isa{P\ {\isacharequal}\ Q} \\
    5.54 -\isa{if\ x\ then\ y\ else\ z} & \isa{{\isachardoublequote}If\ x\ y\ z{\isachardoublequote}}\\
    5.55 -\isa{let\ x\ {\isacharequal}\ e\isactrlisub {\isadigit{1}}\ in\ e\isactrlisub {\isadigit{2}}} & \isa{{\isachardoublequote}Let\ e\isactrlisub {\isadigit{1}}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequote}}\\
    5.56 -\end{supertabular}
    5.57 -
    5.58 -
    5.59 -\section{Orderings}
    5.60 -
    5.61 -A collection of classes defining basic orderings:
    5.62 -preorder, partial order, linear order, dense linear order and wellorder.
    5.63 -\smallskip
    5.64 -
    5.65 -\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
    5.66 -\isa{op\ {\isasymle}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (\verb$<=$)\\
    5.67 -\isa{op\ {\isacharless}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\
    5.68 -\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\
    5.69 -\isa{min} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
    5.70 -\isa{max} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
    5.71 -\isa{top} & \isa{{\isacharprime}a}\\
    5.72 -\isa{bot} & \isa{{\isacharprime}a}\\
    5.73 -\isa{mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
    5.74 -\isa{strict{\isacharunderscore}mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
    5.75 -\end{supertabular}
    5.76 -
    5.77 -\subsubsection*{Syntax}
    5.78 -
    5.79 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
    5.80 -\isa{{\isachardoublequote}x\ {\isasymge}\ y{\isachardoublequote}} & \isa{y\ {\isasymle}\ x} & (\verb$>=$)\\
    5.81 -\isa{{\isachardoublequote}x\ {\isachargreater}\ y{\isachardoublequote}} & \isa{y\ {\isacharless}\ x}\\
    5.82 -\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P{\isachardoublequote}}\\
    5.83 -\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P{\isachardoublequote}}\\
    5.84 -\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
    5.85 -\isa{LEAST\ x{\isachardot}\ P} & \isa{{\isachardoublequote}Least\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\
    5.86 -\end{supertabular}
    5.87 -
    5.88 -
    5.89 -\section{Lattices}
    5.90 -
    5.91 -Classes semilattice, lattice, distributive lattice and complete lattice (the
    5.92 -latter in theory \isa{Set}).
    5.93 -
    5.94 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
    5.95 -\isa{inf} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
    5.96 -\isa{sup} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
    5.97 -\isa{Inf} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\
    5.98 -\isa{Sup} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\
    5.99 -\end{tabular}
   5.100 -
   5.101 -\subsubsection*{Syntax}
   5.102 -
   5.103 -Available by loading theory \isa{Lattice{\isacharunderscore}Syntax} in directory \isa{Library}.
   5.104 -
   5.105 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   5.106 -\isa{{\isachardoublequote}x\ {\isasymsqsubseteq}\ y{\isachardoublequote}} & \isa{x\ {\isasymle}\ y}\\
   5.107 -\isa{{\isachardoublequote}x\ {\isasymsqsubset}\ y{\isachardoublequote}} & \isa{x\ {\isacharless}\ y}\\
   5.108 -\isa{{\isachardoublequote}x\ {\isasymsqinter}\ y{\isachardoublequote}} & \isa{inf\ x\ y}\\
   5.109 -\isa{{\isachardoublequote}x\ {\isasymsqunion}\ y{\isachardoublequote}} & \isa{sup\ x\ y}\\
   5.110 -\isa{{\isachardoublequote}{\isasymSqinter}\ A{\isachardoublequote}} & \isa{Sup\ A}\\
   5.111 -\isa{{\isachardoublequote}{\isasymSqunion}\ A{\isachardoublequote}} & \isa{Inf\ A}\\
   5.112 -\isa{{\isachardoublequote}{\isasymtop}{\isachardoublequote}} & \isa{top}\\
   5.113 -\isa{{\isachardoublequote}{\isasymbottom}{\isachardoublequote}} & \isa{bot}\\
   5.114 -\end{supertabular}
   5.115 -
   5.116 -
   5.117 -\section{Set}
   5.118 -
   5.119 -Sets are predicates: \isa{{\isachardoublequote}{\isacharprime}a\ set\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}}
   5.120 -\bigskip
   5.121 -
   5.122 -\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
   5.123 -\isa{{\isacharbraceleft}{\isacharbraceright}} & \isa{{\isacharprime}a\ set}\\
   5.124 -\isa{insert} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.125 -\isa{Collect} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.126 -\isa{op\ {\isasymin}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool} & (\texttt{:})\\
   5.127 -\isa{op\ {\isasymunion}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Un})\\
   5.128 -\isa{op\ {\isasyminter}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Int})\\
   5.129 -\isa{UNION} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   5.130 -\isa{INTER} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   5.131 -\isa{Union} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.132 -\isa{Inter} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.133 -\isa{Pow} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\
   5.134 -\isa{UNIV} & \isa{{\isacharprime}a\ set}\\
   5.135 -\isa{op\ {\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   5.136 -\isa{Ball} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   5.137 -\isa{Bex} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   5.138 -\end{supertabular}
   5.139 -
   5.140 -\subsubsection*{Syntax}
   5.141 -
   5.142 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   5.143 -\isa{{\isacharbraceleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharbraceright}} & \isa{insert\ x\isactrlisub {\isadigit{1}}\ {\isacharparenleft}{\isasymdots}\ {\isacharparenleft}insert\ x\isactrlisub n\ {\isacharbraceleft}{\isacharbraceright}{\isacharparenright}{\isasymdots}{\isacharparenright}}\\
   5.144 -\isa{x\ {\isasymnotin}\ A} & \isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isasymin}\ A{\isacharparenright}{\isachardoublequote}}\\
   5.145 -\isa{A\ {\isasymsubseteq}\ B} & \isa{{\isachardoublequote}A\ {\isasymle}\ B{\isachardoublequote}}\\
   5.146 -\isa{A\ {\isasymsubset}\ B} & \isa{{\isachardoublequote}A\ {\isacharless}\ B{\isachardoublequote}}\\
   5.147 -\isa{{\isachardoublequote}A\ {\isasymsupseteq}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isasymle}\ A{\isachardoublequote}}\\
   5.148 -\isa{{\isachardoublequote}A\ {\isasymsupset}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isacharless}\ A{\isachardoublequote}}\\
   5.149 -\isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}} & \isa{{\isachardoublequote}Collect\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\
   5.150 -\isa{{\isasymUnion}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{UN})\\
   5.151 -\isa{{\isasymUnion}x{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\
   5.152 -\isa{{\isasymInter}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{INT})\\
   5.153 -\isa{{\isasymInter}x{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\
   5.154 -\isa{{\isasymforall}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Ball\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\
   5.155 -\isa{{\isasymexists}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Bex\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\
   5.156 -\isa{range\ f} & \isa{{\isachardoublequote}f\ {\isacharbackquote}\ UNIV{\isachardoublequote}}\\
   5.157 -\end{supertabular}
   5.158 -
   5.159 -
   5.160 -\section{Fun}
   5.161 -
   5.162 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   5.163 -\isa{id} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.164 -\isa{op\ {\isasymcirc}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymRightarrow}\ {\isacharprime}b}\\
   5.165 -\isa{inj{\isacharunderscore}on} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\
   5.166 -\isa{inj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   5.167 -\isa{surj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   5.168 -\isa{bij} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   5.169 -\isa{bij{\isacharunderscore}betw} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ bool}\\
   5.170 -\isa{fun{\isacharunderscore}upd} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b}\\
   5.171 -\end{supertabular}
   5.172 -
   5.173 -\subsubsection*{Syntax}
   5.174 -
   5.175 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   5.176 -\isa{f{\isacharparenleft}x\ {\isacharcolon}{\isacharequal}\ y{\isacharparenright}} & \isa{{\isachardoublequote}fun{\isacharunderscore}upd\ f\ x\ y{\isachardoublequote}}\\
   5.177 -\isa{f{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharequal}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharcolon}{\isacharequal}y\isactrlisub n{\isacharparenright}} & \isa{f{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcolon}{\isacharequal}y\isactrlisub {\isadigit{1}}{\isacharparenright}{\isasymdots}{\isacharparenleft}x\isactrlisub n{\isacharcolon}{\isacharequal}y\isactrlisub n{\isacharparenright}}\\
   5.178 -\end{tabular}
   5.179 -
   5.180 -
   5.181 -\section{Fixed Points}
   5.182 -
   5.183 -Theory: \isa{Inductive}.
   5.184 -
   5.185 -Least and greatest fixed points in a complete lattice \isa{{\isacharprime}a}:
   5.186 -
   5.187 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   5.188 -\isa{lfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.189 -\isa{gfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.190 -\end{tabular}
   5.191 -
   5.192 -Note that in particular sets (\isa{{\isacharprime}a\ {\isasymRightarrow}\ bool}) are complete lattices.
   5.193 -
   5.194 -\section{Sum\_Type}
   5.195 -
   5.196 -Type constructor \isa{{\isacharplus}}.
   5.197 -
   5.198 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   5.199 -\isa{Inl} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isacharplus}\ {\isacharprime}b}\\
   5.200 -\isa{Inr} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isacharplus}\ {\isacharprime}a}\\
   5.201 -\isa{op\ {\isacharless}{\isacharplus}{\isachargreater}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharplus}\ {\isacharprime}b{\isacharparenright}\ set}
   5.202 -\end{tabular}
   5.203 -
   5.204 -
   5.205 -\section{Product\_Type}
   5.206 -
   5.207 -Types \isa{unit} and \isa{{\isasymtimes}}.
   5.208 -
   5.209 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   5.210 -\isa{{\isacharparenleft}{\isacharparenright}} & \isa{unit}\\
   5.211 -\isa{Pair} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}\\
   5.212 -\isa{fst} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.213 -\isa{snd} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\
   5.214 -\isa{split} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\
   5.215 -\isa{curry} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\
   5.216 -\isa{Sigma} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
   5.217 -\end{supertabular}
   5.218 -
   5.219 -\subsubsection*{Syntax}
   5.220 -
   5.221 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
   5.222 -\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}} & \isa{{\isachardoublequote}Pair\ a\ b{\isachardoublequote}}\\
   5.223 -\isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} & \isa{{\isachardoublequote}split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}{\isachardoublequote}}\\
   5.224 -\isa{A\ {\isasymtimes}\ B} &  \isa{Sigma\ A\ {\isacharparenleft}{\isasymlambda}\_{\isachardot}\ B{\isacharparenright}} & (\verb$<*>$)
   5.225 -\end{tabular}
   5.226 -
   5.227 -Pairs may be nested. Nesting to the right is printed as a tuple,
   5.228 -e.g.\ \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ c{\isacharparenright}}} is really \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ {\isacharparenleft}b{\isacharcomma}\ c{\isacharparenright}{\isacharparenright}}.}
   5.229 -Pattern matching with pairs and tuples extends to all binders,
   5.230 -e.g.\ \mbox{\isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ P},} \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ P{\isacharbraceright}}, etc.
   5.231 -
   5.232 -
   5.233 -\section{Relation}
   5.234 -
   5.235 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   5.236 -\isa{converse} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   5.237 -\isa{op\ O} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
   5.238 -\isa{op\ {\isacharbackquote}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   5.239 -\isa{inv{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
   5.240 -\isa{Id{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   5.241 -\isa{Id} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   5.242 -\isa{Domain} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.243 -\isa{Range} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   5.244 -\isa{Field} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.245 -\isa{refl{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.246 -\isa{refl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.247 -\isa{sym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.248 -\isa{antisym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.249 -\isa{trans} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.250 -\isa{irrefl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.251 -\isa{total{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.252 -\isa{total} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.253 -\end{supertabular}
   5.254 -
   5.255 -\subsubsection*{Syntax}
   5.256 -
   5.257 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   5.258 -\isa{r{\isasyminverse}} & \isa{{\isachardoublequote}converse\ r{\isachardoublequote}} & (\verb$^-1$)
   5.259 -\end{tabular}
   5.260 -
   5.261 -\section{Equiv\_Relations}
   5.262 -
   5.263 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   5.264 -\isa{equiv} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.265 -\isa{op\ {\isacharslash}{\isacharslash}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\
   5.266 -\isa{congruent} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   5.267 -\isa{congruent{\isadigit{2}}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   5.268 -%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\
   5.269 -\end{supertabular}
   5.270 -
   5.271 -\subsubsection*{Syntax}
   5.272 -
   5.273 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   5.274 -\isa{f\ respects\ r} & \isa{{\isachardoublequote}congruent\ r\ f{\isachardoublequote}}\\
   5.275 -\isa{f\ respects{\isadigit{2}}\ r} & \isa{{\isachardoublequote}congruent{\isadigit{2}}\ r\ r\ f{\isachardoublequote}}\\
   5.276 -\end{tabular}
   5.277 -
   5.278 -
   5.279 -\section{Transitive\_Closure}
   5.280 -
   5.281 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   5.282 -\isa{rtrancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   5.283 -\isa{trancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   5.284 -\isa{reflcl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   5.285 -\end{tabular}
   5.286 -
   5.287 -\subsubsection*{Syntax}
   5.288 -
   5.289 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   5.290 -\isa{r\isactrlsup {\isacharasterisk}} & \isa{{\isachardoublequote}rtrancl\ r{\isachardoublequote}} & (\verb$^*$)\\
   5.291 -\isa{r\isactrlsup {\isacharplus}} & \isa{{\isachardoublequote}trancl\ r{\isachardoublequote}} & (\verb$^+$)\\
   5.292 -\isa{r\isactrlsup {\isacharequal}} & \isa{{\isachardoublequote}reflcl\ r{\isachardoublequote}} & (\verb$^=$)
   5.293 -\end{tabular}
   5.294 -
   5.295 -
   5.296 -\section{Algebra}
   5.297 -
   5.298 -Theories \isa{OrderedGroup}, \isa{Ring{\isacharunderscore}and{\isacharunderscore}Field} and \isa{Divides} define a large collection of classes describing common algebraic
   5.299 -structures from semigroups up to fields. Everything is done in terms of
   5.300 -overloaded operators:
   5.301 -
   5.302 -\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
   5.303 -\isa{{\isadigit{0}}} & \isa{{\isacharprime}a}\\
   5.304 -\isa{{\isadigit{1}}} & \isa{{\isacharprime}a}\\
   5.305 -\isa{op\ {\isacharplus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.306 -\isa{op\ {\isacharminus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.307 -\isa{uminus} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (\verb$-$)\\
   5.308 -\isa{op\ {\isacharasterisk}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.309 -\isa{inverse} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.310 -\isa{op\ {\isacharslash}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.311 -\isa{abs} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.312 -\isa{sgn} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.313 -\isa{op\ dvd} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\
   5.314 -\isa{op\ div} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.315 -\isa{op\ mod} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.316 -\end{supertabular}
   5.317 -
   5.318 -\subsubsection*{Syntax}
   5.319 -
   5.320 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   5.321 -\isa{{\isasymbar}x{\isasymbar}} & \isa{{\isachardoublequote}abs\ x{\isachardoublequote}}
   5.322 -\end{tabular}
   5.323 -
   5.324 -
   5.325 -\section{Nat}
   5.326 -
   5.327 -\isa{\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat}
   5.328 -\bigskip
   5.329 -
   5.330 -\begin{tabular}{@ {} lllllll @ {}}
   5.331 -\isa{op\ {\isacharplus}} &
   5.332 -\isa{op\ {\isacharminus}} &
   5.333 -\isa{op\ {\isacharasterisk}} &
   5.334 -\isa{op\ {\isacharcircum}} &
   5.335 -\isa{op\ div}&
   5.336 -\isa{op\ mod}&
   5.337 -\isa{op\ dvd}\\
   5.338 -\isa{op\ {\isasymle}} &
   5.339 -\isa{op\ {\isacharless}} &
   5.340 -\isa{min} &
   5.341 -\isa{max} &
   5.342 -\isa{Min} &
   5.343 -\isa{Max}\\
   5.344 -\end{tabular}
   5.345 -
   5.346 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   5.347 -\isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a}
   5.348 -\end{tabular}
   5.349 -
   5.350 -\section{Int}
   5.351 -
   5.352 -Type \isa{int}
   5.353 -\bigskip
   5.354 -
   5.355 -\begin{tabular}{@ {} llllllll @ {}}
   5.356 -\isa{op\ {\isacharplus}} &
   5.357 -\isa{op\ {\isacharminus}} &
   5.358 -\isa{uminus} &
   5.359 -\isa{op\ {\isacharasterisk}} &
   5.360 -\isa{op\ {\isacharcircum}} &
   5.361 -\isa{op\ div}&
   5.362 -\isa{op\ mod}&
   5.363 -\isa{op\ dvd}\\
   5.364 -\isa{op\ {\isasymle}} &
   5.365 -\isa{op\ {\isacharless}} &
   5.366 -\isa{min} &
   5.367 -\isa{max} &
   5.368 -\isa{Min} &
   5.369 -\isa{Max}\\
   5.370 -\isa{abs} &
   5.371 -\isa{sgn}\\
   5.372 -\end{tabular}
   5.373 -
   5.374 -\begin{tabular}{@ {} l @ {~::~} l l @ {}}
   5.375 -\isa{nat} & \isa{int\ {\isasymRightarrow}\ nat}\\
   5.376 -\isa{of{\isacharunderscore}int} & \isa{int\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.377 -\isa{{\isasymint}} & \isa{{\isacharprime}a\ set} & (\verb$Ints$)
   5.378 -\end{tabular}
   5.379 -
   5.380 -\subsubsection*{Syntax}
   5.381 -
   5.382 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   5.383 -\isa{int} & \isa{{\isachardoublequote}of{\isacharunderscore}nat{\isachardoublequote}}\\
   5.384 -\end{tabular}
   5.385 -
   5.386 -
   5.387 -\section{Finite\_Set}
   5.388 -
   5.389 -
   5.390 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   5.391 -\isa{finite} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\
   5.392 -\isa{card} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ nat}\\
   5.393 -\isa{fold} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\
   5.394 -\isa{fold{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\
   5.395 -\isa{setsum} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\
   5.396 -\isa{setprod} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\
   5.397 -\end{supertabular}
   5.398 -
   5.399 -
   5.400 -\subsubsection*{Syntax}
   5.401 -
   5.402 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   5.403 -\isa{{\isasymSum}A} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x{\isacharparenright}\ A{\isachardoublequote}} & (\verb$SUM$)\\
   5.404 -\isa{{\isasymSum}x{\isasymin}A{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ A{\isachardoublequote}}\\
   5.405 -\isa{{\isachardoublequote}{\isasymSum}x{\isacharbar}P{\isachardot}\ t{\isachardoublequote}} & \isa{{\isasymSum}x{\isasymin}{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}{\isachardot}\ t}\\
   5.406 -\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}} & (\verb$PROD$)\\
   5.407 -\end{supertabular}
   5.408 -
   5.409 -
   5.410 -\section{Wellfounded}
   5.411 -
   5.412 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   5.413 -\isa{wf} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.414 -\isa{acyclic} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\
   5.415 -\isa{acc} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.416 -\isa{measure} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   5.417 -\isa{op\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\
   5.418 -\isa{op\ {\isacharless}{\isacharasterisk}mlex{\isacharasterisk}{\isachargreater}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   5.419 -\isa{less{\isacharunderscore}than} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\
   5.420 -\isa{pred{\isacharunderscore}nat} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\
   5.421 -\end{supertabular}
   5.422 -
   5.423 -
   5.424 -\section{SetInterval}
   5.425 -
   5.426 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   5.427 -\isa{lessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.428 -\isa{atMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.429 -\isa{greaterThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.430 -\isa{atLeast} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.431 -\isa{greaterThanLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.432 -\isa{atLeastLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.433 -\isa{greaterThanAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.434 -\isa{atLeastAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.435 -\end{supertabular}
   5.436 -
   5.437 -\subsubsection*{Syntax}
   5.438 -
   5.439 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   5.440 -\isa{{\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}lessThan\ y{\isachardoublequote}}\\
   5.441 -\isa{{\isacharbraceleft}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atMost\ y{\isachardoublequote}}\\
   5.442 -\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThan\ x{\isachardoublequote}}\\
   5.443 -\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}atLeast\ x{\isachardoublequote}}\\
   5.444 -\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanLessThan\ x\ y{\isachardoublequote}}\\
   5.445 -\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastLessThan\ x\ y{\isachardoublequote}}\\
   5.446 -\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanAtMost\ x\ y{\isachardoublequote}}\\
   5.447 -\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastAtMost\ x\ y{\isachardoublequote}}\\
   5.448 -\isa{{\isasymUnion}\ i{\isasymle}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\
   5.449 -\isa{{\isasymUnion}\ i{\isacharless}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\
   5.450 -\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymInter}} instead of \isa{{\isasymUnion}}}\\
   5.451 -\isa{{\isasymSum}x\ {\isacharequal}\ a{\isachardot}{\isachardot}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}a{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\
   5.452 -\isa{{\isasymSum}x\ {\isacharequal}\ a{\isachardot}{\isachardot}{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}a{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\
   5.453 -\isa{{\isasymSum}x{\isasymle}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\
   5.454 -\isa{{\isasymSum}x{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\
   5.455 -\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}}\\
   5.456 -\end{supertabular}
   5.457 -
   5.458 -
   5.459 -\section{Power}
   5.460 -
   5.461 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   5.462 -\isa{op\ {\isacharcircum}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a}
   5.463 -\end{tabular}
   5.464 -
   5.465 -
   5.466 -\section{Iterated Functions and Relations}
   5.467 -
   5.468 -Theory: \isa{Relation{\isacharunderscore}Power}
   5.469 -
   5.470 -Iterated functions \ \isa{{\isachardoublequote}{\isacharparenleft}f{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isasymRightarrow}{\isacharprime}a{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}} \
   5.471 -and relations \ \isa{{\isachardoublequote}{\isacharparenleft}r{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}a{\isacharparenright}set{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}}.
   5.472 -
   5.473 -
   5.474 -\section{Option}
   5.475 -
   5.476 -\isa{\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a}
   5.477 -\bigskip
   5.478 -
   5.479 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   5.480 -\isa{the} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.481 -\isa{Option{\isachardot}map} & \isa{{\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequote}}\\
   5.482 -\isa{Option{\isachardot}set} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a\ set}
   5.483 -\end{tabular}
   5.484 -
   5.485 -\section{List}
   5.486 -
   5.487 -\isa{\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ op\ {\isacharhash}\ {\isacharprime}a\ {\isacharparenleft}{\isacharprime}a\ list{\isacharparenright}}
   5.488 -\bigskip
   5.489 -
   5.490 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   5.491 -\isa{op\ {\isacharat}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.492 -\isa{butlast} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.493 -\isa{concat} & \isa{{\isacharprime}a\ list\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.494 -\isa{distinct} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\
   5.495 -\isa{drop} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.496 -\isa{dropWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.497 -\isa{filter} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.498 -\isa{foldl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.499 -\isa{foldr} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\
   5.500 -\isa{hd} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.501 -\isa{last} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.502 -\isa{length} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat}\\
   5.503 -\isa{lenlex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   5.504 -\isa{lex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   5.505 -\isa{lexn} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   5.506 -\isa{lexord} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   5.507 -\isa{listrel} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\
   5.508 -\isa{lists} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\
   5.509 -\isa{listset} & \isa{{\isacharprime}a\ set\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\
   5.510 -\isa{listsum} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\
   5.511 -\isa{list{\isacharunderscore}all{\isadigit{2}}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ bool}\\
   5.512 -\isa{list{\isacharunderscore}update} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.513 -\isa{map} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list}\\
   5.514 -\isa{measures} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\
   5.515 -\isa{remdups} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.516 -\isa{removeAll} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.517 -\isa{remove{\isadigit{1}}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.518 -\isa{replicate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.519 -\isa{rev} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.520 -\isa{rotate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.521 -\isa{rotate{\isadigit{1}}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.522 -\isa{set} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.523 -\isa{sort} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.524 -\isa{sorted} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\
   5.525 -\isa{splice} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.526 -\isa{sublist} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.527 -\isa{take} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.528 -\isa{takeWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.529 -\isa{tl} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.530 -\isa{upt} & \isa{nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ list}\\
   5.531 -\isa{upto} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\
   5.532 -\isa{zip} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list}\\
   5.533 -\end{supertabular}
   5.534 -
   5.535 -\subsubsection*{Syntax}
   5.536 -
   5.537 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   5.538 -\isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isacharbrackright}} & \isa{x\isactrlisub {\isadigit{1}}\ {\isacharhash}\ {\isasymdots}\ {\isacharhash}\ x\isactrlisub n\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}\\
   5.539 -\isa{{\isacharbrackleft}m{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}} & \isa{{\isachardoublequote}upt\ m\ n{\isachardoublequote}}\\
   5.540 -\isa{{\isacharbrackleft}i{\isachardot}{\isachardot}j{\isacharbrackright}} & \isa{{\isachardoublequote}upto\ i\ j{\isachardoublequote}}\\
   5.541 -\isa{{\isacharbrackleft}e{\isachardot}\ x\ {\isasymleftarrow}\ xs{\isacharbrackright}} & \isa{map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs}\\
   5.542 -\isa{{\isacharbrackleft}x{\isasymleftarrow}xs\ {\isachardot}\ b{\isacharbrackright}} & \isa{{\isachardoublequote}filter\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}\ xs{\isachardoublequote}} \\
   5.543 -\isa{xs{\isacharbrackleft}n\ {\isacharcolon}{\isacharequal}\ x{\isacharbrackright}} & \isa{{\isachardoublequote}list{\isacharunderscore}update\ xs\ n\ x{\isachardoublequote}}\\
   5.544 -\isa{{\isasymSum}x{\isasymleftarrow}xs{\isachardot}\ e} & \isa{{\isachardoublequote}listsum\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}}\\
   5.545 -\end{supertabular}
   5.546 -\medskip
   5.547 -
   5.548 -List comprehension: \isa{{\isacharbrackleft}e{\isachardot}\ q\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ q\isactrlisub n{\isacharbrackright}} where each
   5.549 -qualifier \isa{q\isactrlisub i} is either a generator \mbox{\isa{pat\ {\isasymleftarrow}\ e}} or a
   5.550 -guard, i.e.\ boolean expression.
   5.551 -
   5.552 -\section{Map}
   5.553 -
   5.554 -Maps model partial functions and are often used as finite tables. However,
   5.555 -the domain of a map may be infinite.
   5.556 -
   5.557 -\isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option}
   5.558 -\bigskip
   5.559 -
   5.560 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   5.561 -\isa{Map{\isachardot}empty} & \isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   5.562 -\isa{op\ {\isacharplus}{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   5.563 -\isa{op\ {\isasymcirc}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymrightharpoonup}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}c\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   5.564 -\isa{op\ {\isacharbar}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   5.565 -\isa{dom} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\
   5.566 -\isa{ran} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\
   5.567 -\isa{op\ {\isasymsubseteq}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\
   5.568 -\isa{map{\isacharunderscore}of} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   5.569 -\isa{map{\isacharunderscore}upds} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\
   5.570 -\end{supertabular}
   5.571 -
   5.572 -\subsubsection*{Syntax}
   5.573 -
   5.574 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   5.575 -\isa{Map{\isachardot}empty} & \isa{{\isasymlambda}x{\isachardot}\ None}\\
   5.576 -\isa{m{\isacharparenleft}x\ {\isasymmapsto}\ y{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x{\isacharcolon}{\isacharequal}Some\ y{\isacharparenright}{\isachardoublequote}}\\
   5.577 -\isa{m{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharparenright}{\isasymdots}{\isacharparenleft}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}{\isachardoublequote}}\\
   5.578 -\isa{{\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharbrackright}} & \isa{{\isachardoublequote}Map{\isachardot}empty{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isasymmapsto}y\isactrlisub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlisub n{\isasymmapsto}y\isactrlisub n{\isacharparenright}{\isachardoublequote}}\\
   5.579 -\isa{m{\isacharparenleft}xs\ {\isacharbrackleft}{\isasymmapsto}{\isacharbrackright}\ ys{\isacharparenright}} & \isa{{\isachardoublequote}map{\isacharunderscore}upds\ m\ xs\ ys{\isachardoublequote}}\\
   5.580 -\end{tabular}%
   5.581 -\end{isamarkuptext}%
   5.582 -\isamarkuptrue%
   5.583 -%
   5.584 -\isadelimtheory
   5.585 -%
   5.586 -\endisadelimtheory
   5.587 -%
   5.588 -\isatagtheory
   5.589 -%
   5.590 -\endisatagtheory
   5.591 -{\isafoldtheory}%
   5.592 -%
   5.593 -\isadelimtheory
   5.594 -%
   5.595 -\endisadelimtheory
   5.596 -\end{isabellebody}%
   5.597 -%%% Local Variables:
   5.598 -%%% mode: latex
   5.599 -%%% TeX-master: "root"
   5.600 -%%% End:
     6.1 --- a/doc-src/Main/Makefile	Wed Mar 11 20:09:23 2009 +0100
     6.2 +++ b/doc-src/Main/Makefile	Wed Mar 11 20:11:06 2009 +0100
     6.3 @@ -1,6 +1,3 @@
     6.4 -#
     6.5 -# $Id$
     6.6 -#
     6.7  
     6.8  ## targets
     6.9  
    6.10 @@ -11,12 +8,10 @@
    6.11  
    6.12  include ../Makefile.in
    6.13  
    6.14 -SRC = ../../src/HOL/Docs/generated
    6.15 -
    6.16  NAME = main
    6.17  
    6.18 -FILES = $(NAME).tex Main_Doc.tex \
    6.19 -  isabelle.sty isabellesym.sty pdfsetup.sty
    6.20 +FILES = ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty $(NAME).tex	\
    6.21 +  Docs/document/Main_Doc.tex
    6.22  
    6.23  dvi: $(NAME).dvi
    6.24  
    6.25 @@ -27,19 +22,3 @@
    6.26  
    6.27  $(NAME).pdf: $(FILES)
    6.28  	$(PDFLATEX) $(NAME)
    6.29 -	$(FIXBOOKMARKS) $(NAME).out
    6.30 -	$(PDFLATEX) $(NAME)
    6.31 -	$(PDFLATEX) $(NAME)
    6.32 -
    6.33 -isabelle.sty:
    6.34 -	ln ../isabelle.sty .
    6.35 -
    6.36 -isabellesym.sty:
    6.37 -	ln ../isabellesym.sty .
    6.38 -
    6.39 -pdfsetup.sty:
    6.40 -	ln ../pdfsetup.sty .
    6.41 -
    6.42 -copy:
    6.43 -	cp $(SRC)/Main_Doc.tex Main_Doc.tex
    6.44 -	cp $(SRC)/root.tex main.tex
     7.1 --- a/doc-src/Main/main.tex	Wed Mar 11 20:09:23 2009 +0100
     7.2 +++ b/doc-src/Main/main.tex	Wed Mar 11 20:11:06 2009 +0100
     7.3 @@ -8,7 +8,7 @@
     7.4  \headsep=0mm
     7.5  \textheight=234mm
     7.6  
     7.7 -\usepackage{isabelle,isabellesym}
     7.8 +\usepackage{../isabelle,../isabellesym}
     7.9  
    7.10  % further packages required for unusual symbols (see also
    7.11  % isabellesym.sty), use only when needed
    7.12 @@ -36,7 +36,7 @@
    7.13    %for \<cent>, \<currency>
    7.14  
    7.15  % this should be the last package used
    7.16 -\usepackage{pdfsetup}
    7.17 +\usepackage{../pdfsetup}
    7.18  
    7.19  % urls in roman style, theory text in math-similar italics
    7.20  \urlstyle{rm}
    7.21 @@ -56,7 +56,7 @@
    7.22  \date{\today}
    7.23  \maketitle
    7.24  
    7.25 -\input{Main_Doc}
    7.26 +\input{Docs/document/Main_Doc.tex}
    7.27  
    7.28  % optional bibliography
    7.29  %\bibliographystyle{abbrv}
     8.1 --- a/doc/Contents	Wed Mar 11 20:09:23 2009 +0100
     8.2 +++ b/doc/Contents	Wed Mar 11 20:11:06 2009 +0100
     8.3 @@ -8,6 +8,7 @@
     8.4    sugar           LaTeX sugar for proof documents
     8.5  
     8.6  Reference Manuals
     8.7 +  main            What's in Main
     8.8    isar-ref        The Isabelle/Isar Reference Manual
     8.9    implementation  The Isabelle/Isar Implementation Manual
    8.10    system          The Isabelle System Manual
     9.1 --- a/src/HOL/Docs/Main_Doc.thy	Wed Mar 11 20:09:23 2009 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,572 +0,0 @@
     9.4 -(*<*)
     9.5 -theory Main_Doc
     9.6 -imports Main
     9.7 -begin
     9.8 -
     9.9 -ML {*
    9.10 -fun pretty_term_type_only ctxt (t, T) =
    9.11 -  (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then ()
    9.12 -   else error "term_type_only: type mismatch";
    9.13 -   Syntax.pretty_typ ctxt T)
    9.14 -
    9.15 -val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
    9.16 -  (fn {source, context, ...} => fn arg =>
    9.17 -    ThyOutput.output
    9.18 -      (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg]));
    9.19 -*}
    9.20 -(*>*)
    9.21 -text{*
    9.22 -
    9.23 -\begin{abstract}
    9.24 -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/}.
    9.25 -\end{abstract}
    9.26 -
    9.27 -\section{HOL}
    9.28 -
    9.29 -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"}.
    9.30 -\smallskip
    9.31 -
    9.32 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
    9.33 -@{const HOL.undefined} & @{typeof HOL.undefined}\\
    9.34 -@{const HOL.default} & @{typeof HOL.default}\\
    9.35 -\end{tabular}
    9.36 -
    9.37 -\subsubsection*{Syntax}
    9.38 -
    9.39 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
    9.40 -@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"} & (\verb$~=$)\\
    9.41 -@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\
    9.42 -@{term"If x y z"} & @{term[source]"If x y z"}\\
    9.43 -@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\<lambda>x. e\<^isub>2)"}\\
    9.44 -\end{supertabular}
    9.45 -
    9.46 -
    9.47 -\section{Orderings}
    9.48 -
    9.49 -A collection of classes defining basic orderings:
    9.50 -preorder, partial order, linear order, dense linear order and wellorder.
    9.51 -\smallskip
    9.52 -
    9.53 -\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
    9.54 -@{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\
    9.55 -@{const HOL.less} & @{typeof HOL.less}\\
    9.56 -@{const Orderings.Least} & @{typeof Orderings.Least}\\
    9.57 -@{const Orderings.min} & @{typeof Orderings.min}\\
    9.58 -@{const Orderings.max} & @{typeof Orderings.max}\\
    9.59 -@{const[source] top} & @{typeof Orderings.top}\\
    9.60 -@{const[source] bot} & @{typeof Orderings.bot}\\
    9.61 -@{const Orderings.mono} & @{typeof Orderings.mono}\\
    9.62 -@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\
    9.63 -\end{supertabular}
    9.64 -
    9.65 -\subsubsection*{Syntax}
    9.66 -
    9.67 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
    9.68 -@{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\verb$>=$)\\
    9.69 -@{term[source]"x > y"} & @{term"x > y"}\\
    9.70 -@{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\
    9.71 -@{term"EX x<=y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\
    9.72 -\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
    9.73 -@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
    9.74 -\end{supertabular}
    9.75 -
    9.76 -
    9.77 -\section{Lattices}
    9.78 -
    9.79 -Classes semilattice, lattice, distributive lattice and complete lattice (the
    9.80 -latter in theory @{theory Set}).
    9.81 -
    9.82 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
    9.83 -@{const Lattices.inf} & @{typeof Lattices.inf}\\
    9.84 -@{const Lattices.sup} & @{typeof Lattices.sup}\\
    9.85 -@{const Set.Inf} & @{term_type_only Set.Inf "'a set \<Rightarrow> 'a::complete_lattice"}\\
    9.86 -@{const Set.Sup} & @{term_type_only Set.Sup "'a set \<Rightarrow> 'a::complete_lattice"}\\
    9.87 -\end{tabular}
    9.88 -
    9.89 -\subsubsection*{Syntax}
    9.90 -
    9.91 -Available by loading theory @{text Lattice_Syntax} in directory @{text
    9.92 -Library}.
    9.93 -
    9.94 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
    9.95 -@{text[source]"x \<sqsubseteq> y"} & @{term"x \<le> y"}\\
    9.96 -@{text[source]"x \<sqsubset> y"} & @{term"x < y"}\\
    9.97 -@{text[source]"x \<sqinter> y"} & @{term"inf x y"}\\
    9.98 -@{text[source]"x \<squnion> y"} & @{term"sup x y"}\\
    9.99 -@{text[source]"\<Sqinter> A"} & @{term"Sup A"}\\
   9.100 -@{text[source]"\<Squnion> A"} & @{term"Inf A"}\\
   9.101 -@{text[source]"\<top>"} & @{term[source] top}\\
   9.102 -@{text[source]"\<bottom>"} & @{term[source] bot}\\
   9.103 -\end{supertabular}
   9.104 -
   9.105 -
   9.106 -\section{Set}
   9.107 -
   9.108 -Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
   9.109 -\bigskip
   9.110 -
   9.111 -\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
   9.112 -@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
   9.113 -@{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
   9.114 -@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
   9.115 -@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
   9.116 -@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
   9.117 -@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
   9.118 -@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
   9.119 -@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
   9.120 -@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
   9.121 -@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\
   9.122 -@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\
   9.123 -@{const UNIV} & @{term_type_only UNIV "'a set"}\\
   9.124 -@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\
   9.125 -@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
   9.126 -@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
   9.127 -\end{supertabular}
   9.128 -
   9.129 -\subsubsection*{Syntax}
   9.130 -
   9.131 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   9.132 -@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\
   9.133 -@{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\
   9.134 -@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
   9.135 -@{term"A \<subset> B"} & @{term[source]"A < B"}\\
   9.136 -@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
   9.137 -@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
   9.138 -@{term"{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
   9.139 -@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
   9.140 -@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
   9.141 -@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
   9.142 -@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
   9.143 -@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
   9.144 -@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
   9.145 -@{term"range f"} & @{term[source]"f ` UNIV"}\\
   9.146 -\end{supertabular}
   9.147 -
   9.148 -
   9.149 -\section{Fun}
   9.150 -
   9.151 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   9.152 -@{const "Fun.id"} & @{typeof Fun.id}\\
   9.153 -@{const "Fun.comp"} & @{typeof Fun.comp}\\
   9.154 -@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\
   9.155 -@{const "Fun.inj"} & @{typeof Fun.inj}\\
   9.156 -@{const "Fun.surj"} & @{typeof Fun.surj}\\
   9.157 -@{const "Fun.bij"} & @{typeof Fun.bij}\\
   9.158 -@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\
   9.159 -@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\
   9.160 -\end{supertabular}
   9.161 -
   9.162 -\subsubsection*{Syntax}
   9.163 -
   9.164 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   9.165 -@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\
   9.166 -@{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)"}\\
   9.167 -\end{tabular}
   9.168 -
   9.169 -
   9.170 -\section{Fixed Points}
   9.171 -
   9.172 -Theory: @{theory Inductive}.
   9.173 -
   9.174 -Least and greatest fixed points in a complete lattice @{typ 'a}:
   9.175 -
   9.176 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   9.177 -@{const Inductive.lfp} & @{typeof Inductive.lfp}\\
   9.178 -@{const Inductive.gfp} & @{typeof Inductive.gfp}\\
   9.179 -\end{tabular}
   9.180 -
   9.181 -Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices.
   9.182 -
   9.183 -\section{Sum\_Type}
   9.184 -
   9.185 -Type constructor @{text"+"}.
   9.186 -
   9.187 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   9.188 -@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\
   9.189 -@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\
   9.190 -@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"}
   9.191 -\end{tabular}
   9.192 -
   9.193 -
   9.194 -\section{Product\_Type}
   9.195 -
   9.196 -Types @{typ unit} and @{text"\<times>"}.
   9.197 -
   9.198 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   9.199 -@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\
   9.200 -@{const Pair} & @{typeof Pair}\\
   9.201 -@{const fst} & @{typeof fst}\\
   9.202 -@{const snd} & @{typeof snd}\\
   9.203 -@{const split} & @{typeof split}\\
   9.204 -@{const curry} & @{typeof curry}\\
   9.205 -@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\
   9.206 -\end{supertabular}
   9.207 -
   9.208 -\subsubsection*{Syntax}
   9.209 -
   9.210 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
   9.211 -@{term"Pair a b"} & @{term[source]"Pair a b"}\\
   9.212 -@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\
   9.213 -@{term"A <*> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
   9.214 -\end{tabular}
   9.215 -
   9.216 -Pairs may be nested. Nesting to the right is printed as a tuple,
   9.217 -e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{@{text"(a, (b, c))"}.}
   9.218 -Pattern matching with pairs and tuples extends to all binders,
   9.219 -e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
   9.220 -
   9.221 -
   9.222 -\section{Relation}
   9.223 -
   9.224 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   9.225 -@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
   9.226 -@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('c*'a)set\<Rightarrow>('c*'b)set"}\\
   9.227 -@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\
   9.228 -@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\
   9.229 -@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\
   9.230 -@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\
   9.231 -@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\
   9.232 -@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\
   9.233 -@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\
   9.234 -@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
   9.235 -@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\
   9.236 -@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\
   9.237 -@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\
   9.238 -@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\
   9.239 -@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\
   9.240 -@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
   9.241 -@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\
   9.242 -\end{supertabular}
   9.243 -
   9.244 -\subsubsection*{Syntax}
   9.245 -
   9.246 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   9.247 -@{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$)
   9.248 -\end{tabular}
   9.249 -
   9.250 -\section{Equiv\_Relations}
   9.251 -
   9.252 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   9.253 -@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\
   9.254 -@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\
   9.255 -@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\
   9.256 -@{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"}\\
   9.257 -%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\
   9.258 -\end{supertabular}
   9.259 -
   9.260 -\subsubsection*{Syntax}
   9.261 -
   9.262 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   9.263 -@{term"congruent r f"} & @{term[source]"congruent r f"}\\
   9.264 -@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\
   9.265 -\end{tabular}
   9.266 -
   9.267 -
   9.268 -\section{Transitive\_Closure}
   9.269 -
   9.270 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   9.271 -@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
   9.272 -@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
   9.273 -@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
   9.274 -\end{tabular}
   9.275 -
   9.276 -\subsubsection*{Syntax}
   9.277 -
   9.278 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   9.279 -@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\verb$^*$)\\
   9.280 -@{term"trancl r"} & @{term[source]"trancl r"} & (\verb$^+$)\\
   9.281 -@{term"reflcl r"} & @{term[source]"reflcl r"} & (\verb$^=$)
   9.282 -\end{tabular}
   9.283 -
   9.284 -
   9.285 -\section{Algebra}
   9.286 -
   9.287 -Theories @{theory OrderedGroup}, @{theory Ring_and_Field} and @{theory
   9.288 -Divides} define a large collection of classes describing common algebraic
   9.289 -structures from semigroups up to fields. Everything is done in terms of
   9.290 -overloaded operators:
   9.291 -
   9.292 -\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
   9.293 -@{text "0"} & @{typeof zero}\\
   9.294 -@{text "1"} & @{typeof one}\\
   9.295 -@{const plus} & @{typeof plus}\\
   9.296 -@{const minus} & @{typeof minus}\\
   9.297 -@{const uminus} & @{typeof uminus} & (\verb$-$)\\
   9.298 -@{const times} & @{typeof times}\\
   9.299 -@{const inverse} & @{typeof inverse}\\
   9.300 -@{const divide} & @{typeof divide}\\
   9.301 -@{const abs} & @{typeof abs}\\
   9.302 -@{const sgn} & @{typeof sgn}\\
   9.303 -@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\
   9.304 -@{const div_class.div} & @{typeof "div_class.div"}\\
   9.305 -@{const div_class.mod} & @{typeof "div_class.mod"}\\
   9.306 -\end{supertabular}
   9.307 -
   9.308 -\subsubsection*{Syntax}
   9.309 -
   9.310 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   9.311 -@{term"abs x"} & @{term[source]"abs x"}
   9.312 -\end{tabular}
   9.313 -
   9.314 -
   9.315 -\section{Nat}
   9.316 -
   9.317 -@{datatype nat}
   9.318 -\bigskip
   9.319 -
   9.320 -\begin{tabular}{@ {} lllllll @ {}}
   9.321 -@{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   9.322 -@{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   9.323 -@{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   9.324 -@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   9.325 -@{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
   9.326 -@{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
   9.327 -@{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\
   9.328 -@{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
   9.329 -@{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
   9.330 -@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   9.331 -@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
   9.332 -@{term "Min :: nat set \<Rightarrow> nat"} &
   9.333 -@{term "Max :: nat set \<Rightarrow> nat"}\\
   9.334 -\end{tabular}
   9.335 -
   9.336 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   9.337 -@{const Nat.of_nat} & @{typeof Nat.of_nat}
   9.338 -\end{tabular}
   9.339 -
   9.340 -\section{Int}
   9.341 -
   9.342 -Type @{typ int}
   9.343 -\bigskip
   9.344 -
   9.345 -\begin{tabular}{@ {} llllllll @ {}}
   9.346 -@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} &
   9.347 -@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} &
   9.348 -@{term "uminus :: int \<Rightarrow> int"} &
   9.349 -@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} &
   9.350 -@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} &
   9.351 -@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}&
   9.352 -@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}&
   9.353 -@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\
   9.354 -@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} &
   9.355 -@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} &
   9.356 -@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} &
   9.357 -@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} &
   9.358 -@{term "Min :: int set \<Rightarrow> int"} &
   9.359 -@{term "Max :: int set \<Rightarrow> int"}\\
   9.360 -@{term "abs :: int \<Rightarrow> int"} &
   9.361 -@{term "sgn :: int \<Rightarrow> int"}\\
   9.362 -\end{tabular}
   9.363 -
   9.364 -\begin{tabular}{@ {} l @ {~::~} l l @ {}}
   9.365 -@{const Int.nat} & @{typeof Int.nat}\\
   9.366 -@{const Int.of_int} & @{typeof Int.of_int}\\
   9.367 -@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\verb$Ints$)
   9.368 -\end{tabular}
   9.369 -
   9.370 -\subsubsection*{Syntax}
   9.371 -
   9.372 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   9.373 -@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\
   9.374 -\end{tabular}
   9.375 -
   9.376 -
   9.377 -\section{Finite\_Set}
   9.378 -
   9.379 -
   9.380 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   9.381 -@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\
   9.382 -@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\
   9.383 -@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
   9.384 -@{const Finite_Set.fold_image} & @{typ "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
   9.385 -@{const Finite_Set.setsum} & @{term_type_only Finite_Set.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
   9.386 -@{const Finite_Set.setprod} & @{term_type_only Finite_Set.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
   9.387 -\end{supertabular}
   9.388 -
   9.389 -
   9.390 -\subsubsection*{Syntax}
   9.391 -
   9.392 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
   9.393 -@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\verb$SUM$)\\
   9.394 -@{term"setsum (%x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\
   9.395 -@{term[source]"\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\
   9.396 -\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}} & (\verb$PROD$)\\
   9.397 -\end{supertabular}
   9.398 -
   9.399 -
   9.400 -\section{Wellfounded}
   9.401 -
   9.402 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   9.403 -@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\
   9.404 -@{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\<Rightarrow>bool"}\\
   9.405 -@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\
   9.406 -@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\
   9.407 -@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\
   9.408 -@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\
   9.409 -@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\
   9.410 -@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\
   9.411 -\end{supertabular}
   9.412 -
   9.413 -
   9.414 -\section{SetInterval}
   9.415 -
   9.416 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   9.417 -@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
   9.418 -@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\
   9.419 -@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\
   9.420 -@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\
   9.421 -@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
   9.422 -@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
   9.423 -@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
   9.424 -@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
   9.425 -\end{supertabular}
   9.426 -
   9.427 -\subsubsection*{Syntax}
   9.428 -
   9.429 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   9.430 -@{term "lessThan y"} & @{term[source] "lessThan y"}\\
   9.431 -@{term "atMost y"} & @{term[source] "atMost y"}\\
   9.432 -@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\
   9.433 -@{term "atLeast x"} & @{term[source] "atLeast x"}\\
   9.434 -@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\
   9.435 -@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\
   9.436 -@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\
   9.437 -@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\
   9.438 -@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
   9.439 -@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\
   9.440 -\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
   9.441 -@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
   9.442 -@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
   9.443 -@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\
   9.444 -@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\
   9.445 -\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
   9.446 -\end{supertabular}
   9.447 -
   9.448 -
   9.449 -\section{Power}
   9.450 -
   9.451 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   9.452 -@{const Power.power} & @{typeof Power.power}
   9.453 -\end{tabular}
   9.454 -
   9.455 -
   9.456 -\section{Iterated Functions and Relations}
   9.457 -
   9.458 -Theory: @{theory Relation_Power}
   9.459 -
   9.460 -Iterated functions \ @{term[source]"(f::'a\<Rightarrow>'a) ^ n"} \
   9.461 -and relations \ @{term[source]"(r::('a\<times>'a)set) ^ n"}.
   9.462 -
   9.463 -
   9.464 -\section{Option}
   9.465 -
   9.466 -@{datatype option}
   9.467 -\bigskip
   9.468 -
   9.469 -\begin{tabular}{@ {} l @ {~::~} l @ {}}
   9.470 -@{const Option.the} & @{typeof Option.the}\\
   9.471 -@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
   9.472 -@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}
   9.473 -\end{tabular}
   9.474 -
   9.475 -\section{List}
   9.476 -
   9.477 -@{datatype list}
   9.478 -\bigskip
   9.479 -
   9.480 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   9.481 -@{const List.append} & @{typeof List.append}\\
   9.482 -@{const List.butlast} & @{typeof List.butlast}\\
   9.483 -@{const List.concat} & @{typeof List.concat}\\
   9.484 -@{const List.distinct} & @{typeof List.distinct}\\
   9.485 -@{const List.drop} & @{typeof List.drop}\\
   9.486 -@{const List.dropWhile} & @{typeof List.dropWhile}\\
   9.487 -@{const List.filter} & @{typeof List.filter}\\
   9.488 -@{const List.foldl} & @{typeof List.foldl}\\
   9.489 -@{const List.foldr} & @{typeof List.foldr}\\
   9.490 -@{const List.hd} & @{typeof List.hd}\\
   9.491 -@{const List.last} & @{typeof List.last}\\
   9.492 -@{const List.length} & @{typeof List.length}\\
   9.493 -@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   9.494 -@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   9.495 -@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\
   9.496 -@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   9.497 -@{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
   9.498 -@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
   9.499 -@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
   9.500 -@{const List.listsum} & @{typeof List.listsum}\\
   9.501 -@{const List.list_all2} & @{typeof List.list_all2}\\
   9.502 -@{const List.list_update} & @{typeof List.list_update}\\
   9.503 -@{const List.map} & @{typeof List.map}\\
   9.504 -@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\
   9.505 -@{const List.remdups} & @{typeof List.remdups}\\
   9.506 -@{const List.removeAll} & @{typeof List.removeAll}\\
   9.507 -@{const List.remove1} & @{typeof List.remove1}\\
   9.508 -@{const List.replicate} & @{typeof List.replicate}\\
   9.509 -@{const List.rev} & @{typeof List.rev}\\
   9.510 -@{const List.rotate} & @{typeof List.rotate}\\
   9.511 -@{const List.rotate1} & @{typeof List.rotate1}\\
   9.512 -@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\
   9.513 -@{const List.sort} & @{typeof List.sort}\\
   9.514 -@{const List.sorted} & @{typeof List.sorted}\\
   9.515 -@{const List.splice} & @{typeof List.splice}\\
   9.516 -@{const List.sublist} & @{typeof List.sublist}\\
   9.517 -@{const List.take} & @{typeof List.take}\\
   9.518 -@{const List.takeWhile} & @{typeof List.takeWhile}\\
   9.519 -@{const List.tl} & @{typeof List.tl}\\
   9.520 -@{const List.upt} & @{typeof List.upt}\\
   9.521 -@{const List.upto} & @{typeof List.upto}\\
   9.522 -@{const List.zip} & @{typeof List.zip}\\
   9.523 -\end{supertabular}
   9.524 -
   9.525 -\subsubsection*{Syntax}
   9.526 -
   9.527 -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   9.528 -@{text"[x\<^isub>1,\<dots>,x\<^isub>n]"} & @{text"x\<^isub>1 # \<dots> # x\<^isub>n # []"}\\
   9.529 -@{term"[m..<n]"} & @{term[source]"upt m n"}\\
   9.530 -@{term"[i..j]"} & @{term[source]"upto i j"}\\
   9.531 -@{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\
   9.532 -@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\
   9.533 -@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
   9.534 -@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
   9.535 -\end{supertabular}
   9.536 -\medskip
   9.537 -
   9.538 -List comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each
   9.539 -qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \<leftarrow> e"}} or a
   9.540 -guard, i.e.\ boolean expression.
   9.541 -
   9.542 -\section{Map}
   9.543 -
   9.544 -Maps model partial functions and are often used as finite tables. However,
   9.545 -the domain of a map may be infinite.
   9.546 -
   9.547 -@{text"'a \<rightharpoonup> 'b  =  'a \<Rightarrow> 'b option"}
   9.548 -\bigskip
   9.549 -
   9.550 -\begin{supertabular}{@ {} l @ {~::~} l @ {}}
   9.551 -@{const Map.empty} & @{typeof Map.empty}\\
   9.552 -@{const Map.map_add} & @{typeof Map.map_add}\\
   9.553 -@{const Map.map_comp} & @{typeof Map.map_comp}\\
   9.554 -@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\
   9.555 -@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\
   9.556 -@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\
   9.557 -@{const Map.map_le} & @{typeof Map.map_le}\\
   9.558 -@{const Map.map_of} & @{typeof Map.map_of}\\
   9.559 -@{const Map.map_upds} & @{typeof Map.map_upds}\\
   9.560 -\end{supertabular}
   9.561 -
   9.562 -\subsubsection*{Syntax}
   9.563 -
   9.564 -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
   9.565 -@{term"Map.empty"} & @{term"\<lambda>x. None"}\\
   9.566 -@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\
   9.567 -@{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)"}\\
   9.568 -@{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)"}\\
   9.569 -@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\
   9.570 -\end{tabular}
   9.571 -
   9.572 -*}
   9.573 -(*<*)
   9.574 -end
   9.575 -(*>*)
   9.576 \ No newline at end of file
    10.1 --- a/src/HOL/Docs/ROOT.ML	Wed Mar 11 20:09:23 2009 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,1 +0,0 @@
    10.4 -use_thy "Main_Doc";
    11.1 --- a/src/HOL/Docs/document/root.tex	Wed Mar 11 20:09:23 2009 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,65 +0,0 @@
    11.4 -\documentclass[12pt,a4paper]{article}
    11.5 -
    11.6 -\oddsidemargin=4.6mm
    11.7 -\evensidemargin=4.6mm
    11.8 -\textwidth=150mm
    11.9 -\topmargin=4.6mm
   11.10 -\headheight=0mm
   11.11 -\headsep=0mm
   11.12 -\textheight=234mm
   11.13 -
   11.14 -\usepackage{isabelle,isabellesym}
   11.15 -
   11.16 -% further packages required for unusual symbols (see also
   11.17 -% isabellesym.sty), use only when needed
   11.18 -
   11.19 -\usepackage{amssymb}
   11.20 -  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   11.21 -  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   11.22 -  %\<triangleq>, \<yen>, \<lozenge>
   11.23 -
   11.24 -%\usepackage[greek,english]{babel}
   11.25 -  %option greek for \<euro>
   11.26 -  %option english (default language) for \<guillemotleft>, \<guillemotright>
   11.27 -
   11.28 -%\usepackage[latin1]{inputenc}
   11.29 -  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
   11.30 -  %\<threesuperior>, \<threequarters>, \<degree>
   11.31 -
   11.32 -\usepackage[only,bigsqcap]{stmaryrd}
   11.33 -  %for \<Sqinter>
   11.34 -
   11.35 -%\usepackage{eufrak}
   11.36 -  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
   11.37 -
   11.38 -%\usepackage{textcomp}
   11.39 -  %for \<cent>, \<currency>
   11.40 -
   11.41 -% this should be the last package used
   11.42 -\usepackage{pdfsetup}
   11.43 -
   11.44 -% urls in roman style, theory text in math-similar italics
   11.45 -\urlstyle{rm}
   11.46 -\isabellestyle{it}
   11.47 -
   11.48 -% for uniform font size
   11.49 -\renewcommand{\isastyle}{\isastyleminor}
   11.50 -
   11.51 -\parindent 0pt\parskip 0.5ex
   11.52 -
   11.53 -\usepackage{supertabular}
   11.54 -
   11.55 -\begin{document}
   11.56 -
   11.57 -\title{What's in Main}
   11.58 -\author{Tobias Nipkow}
   11.59 -\date{\today}
   11.60 -\maketitle
   11.61 -
   11.62 -\input{Main_Doc}
   11.63 -
   11.64 -% optional bibliography
   11.65 -%\bibliographystyle{abbrv}
   11.66 -%\bibliography{root}
   11.67 -
   11.68 -\end{document}
    12.1 --- a/src/HOL/IsaMakefile	Wed Mar 11 20:09:23 2009 +0100
    12.2 +++ b/src/HOL/IsaMakefile	Wed Mar 11 20:11:06 2009 +0100
    12.3 @@ -15,7 +15,6 @@
    12.4    HOL-Auth \
    12.5    HOL-Bali \
    12.6    HOL-Decision_Procs \
    12.7 -  HOL-Docs \
    12.8    HOL-Extraction \
    12.9    HOL-HahnBanach \
   12.10    HOL-Hoare \