# HG changeset patch # User wenzelm # Date 1236798666 -3600 # Node ID 28b487cd9e1582b2f3c2bc17b3215c6ab87305c8 # Parent d21bc48823b7fb13b8610f0486b91caac4753747 basic setup for "main" as generated Isabelle manual; diff -r d21bc48823b7 -r 28b487cd9e15 doc-src/Main/Docs/Main_Doc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/Docs/Main_Doc.thy Wed Mar 11 20:11:06 2009 +0100 @@ -0,0 +1,572 @@ +(*<*) +theory Main_Doc +imports Main +begin + +ML {* +fun pretty_term_type_only ctxt (t, T) = + (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then () + else error "term_type_only: type mismatch"; + Syntax.pretty_typ ctxt T) + +val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev) + (fn {source, context, ...} => fn arg => + ThyOutput.output + (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg])); +*} +(*>*) +text{* + +\begin{abstract} +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/}. +\end{abstract} + +\section{HOL} + +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"}. +\smallskip + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const HOL.undefined} & @{typeof HOL.undefined}\\ +@{const HOL.default} & @{typeof HOL.default}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term"~(x = y)"} & @{term[source]"\ (x = y)"} & (\verb$~=$)\\ +@{term[source]"P \ Q"} & @{term"P \ Q"} \\ +@{term"If x y z"} & @{term[source]"If x y z"}\\ +@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\x. e\<^isub>2)"}\\ +\end{supertabular} + + +\section{Orderings} + +A collection of classes defining basic orderings: +preorder, partial order, linear order, dense linear order and wellorder. +\smallskip + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +@{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\ +@{const HOL.less} & @{typeof HOL.less}\\ +@{const Orderings.Least} & @{typeof Orderings.Least}\\ +@{const Orderings.min} & @{typeof Orderings.min}\\ +@{const Orderings.max} & @{typeof Orderings.max}\\ +@{const[source] top} & @{typeof Orderings.top}\\ +@{const[source] bot} & @{typeof Orderings.bot}\\ +@{const Orderings.mono} & @{typeof Orderings.mono}\\ +@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term[source]"x \ y"} & @{term"x \ y"} & (\verb$>=$)\\ +@{term[source]"x > y"} & @{term"x > y"}\\ +@{term"ALL x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ +@{term"EX x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ +@{term"LEAST x. P"} & @{term[source]"Least (\x. P)"}\\ +\end{supertabular} + + +\section{Lattices} + +Classes semilattice, lattice, distributive lattice and complete lattice (the +latter in theory @{theory Set}). + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Lattices.inf} & @{typeof Lattices.inf}\\ +@{const Lattices.sup} & @{typeof Lattices.sup}\\ +@{const Set.Inf} & @{term_type_only Set.Inf "'a set \ 'a::complete_lattice"}\\ +@{const Set.Sup} & @{term_type_only Set.Sup "'a set \ 'a::complete_lattice"}\\ +\end{tabular} + +\subsubsection*{Syntax} + +Available by loading theory @{text Lattice_Syntax} in directory @{text +Library}. + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{text[source]"x \ y"} & @{term"x \ y"}\\ +@{text[source]"x \ y"} & @{term"x < y"}\\ +@{text[source]"x \ y"} & @{term"inf x y"}\\ +@{text[source]"x \ y"} & @{term"sup x y"}\\ +@{text[source]"\ A"} & @{term"Sup A"}\\ +@{text[source]"\ A"} & @{term"Inf A"}\\ +@{text[source]"\"} & @{term[source] top}\\ +@{text[source]"\"} & @{term[source] bot}\\ +\end{supertabular} + + +\section{Set} + +Sets are predicates: @{text[source]"'a set = 'a \ bool"} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ +@{const insert} & @{term_type_only insert "'a\'a set\'a set"}\\ +@{const Collect} & @{term_type_only Collect "('a\bool)\'a set"}\\ +@{const "op :"} & @{term_type_only "op :" "'a\'a set\bool"} & (\texttt{:})\\ +@{const Set.Un} & @{term_type_only Set.Un "'a set\'a set \ 'a set"} & (\texttt{Un})\\ +@{const Set.Int} & @{term_type_only Set.Int "'a set\'a set \ 'a set"} & (\texttt{Int})\\ +@{const UNION} & @{term_type_only UNION "'a set\('a \ 'b set) \ 'b set"}\\ +@{const INTER} & @{term_type_only INTER "'a set\('a \ 'b set) \ 'b set"}\\ +@{const Union} & @{term_type_only Union "'a set set\'a set"}\\ +@{const Inter} & @{term_type_only Inter "'a set set\'a set"}\\ +@{const Pow} & @{term_type_only Pow "'a set \'a set set"}\\ +@{const UNIV} & @{term_type_only UNIV "'a set"}\\ +@{const image} & @{term_type_only image "('a\'b)\'a set\'b set"}\\ +@{const Ball} & @{term_type_only Ball "'a set\('a\bool)\bool"}\\ +@{const Bex} & @{term_type_only Bex "'a set\('a\bool)\bool"}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{text"{x\<^isub>1,\,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\ (insert x\<^isub>n {})\)"}\\ +@{term"x ~: A"} & @{term[source]"\(x \ A)"}\\ +@{term"A \ B"} & @{term[source]"A \ B"}\\ +@{term"A \ B"} & @{term[source]"A < B"}\\ +@{term[source]"A \ B"} & @{term[source]"B \ A"}\\ +@{term[source]"A \ B"} & @{term[source]"B < A"}\\ +@{term"{x. P}"} & @{term[source]"Collect (\x. P)"}\\ +@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\x. A)"} & (\texttt{UN})\\ +@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ +@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\x. A)"} & (\texttt{INT})\\ +@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\x. A)"}\\ +@{term"ALL x:A. P"} & @{term[source]"Ball A (\x. P)"}\\ +@{term"EX x:A. P"} & @{term[source]"Bex A (\x. P)"}\\ +@{term"range f"} & @{term[source]"f ` UNIV"}\\ +\end{supertabular} + + +\section{Fun} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const "Fun.id"} & @{typeof Fun.id}\\ +@{const "Fun.comp"} & @{typeof Fun.comp}\\ +@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\'b)\'a set\bool"}\\ +@{const "Fun.inj"} & @{typeof Fun.inj}\\ +@{const "Fun.surj"} & @{typeof Fun.surj}\\ +@{const "Fun.bij"} & @{typeof Fun.bij}\\ +@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\'b)\'a set\'b set\bool"}\\ +@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ +@{text"f(x\<^isub>1:=y\<^isub>1,\,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\(x\<^isub>n:=y\<^isub>n)"}\\ +\end{tabular} + + +\section{Fixed Points} + +Theory: @{theory Inductive}. + +Least and greatest fixed points in a complete lattice @{typ 'a}: + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ +@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ +\end{tabular} + +Note that in particular sets (@{typ"'a \ bool"}) are complete lattices. + +\section{Sum\_Type} + +Type constructor @{text"+"}. + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ +@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ +@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\'b set\('a+'b)set"} +\end{tabular} + + +\section{Product\_Type} + +Types @{typ unit} and @{text"\"}. + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ +@{const Pair} & @{typeof Pair}\\ +@{const fst} & @{typeof fst}\\ +@{const snd} & @{typeof snd}\\ +@{const split} & @{typeof split}\\ +@{const curry} & @{typeof curry}\\ +@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\('a\'b set)\('a*'b)set"}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} +@{term"Pair a b"} & @{term[source]"Pair a b"}\\ +@{term"split (\x y. t)"} & @{term[source]"split (\x y. t)"}\\ +@{term"A <*> B"} & @{text"Sigma A (\\<^raw:\_>. B)"} & (\verb$<*>$) +\end{tabular} + +Pairs may be nested. Nesting to the right is printed as a tuple, +e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{@{text"(a, (b, c))"}.} +Pattern matching with pairs and tuples extends to all binders, +e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc. + + +\section{Relation} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \ ('b*'a)set"}\\ +@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\('c*'a)set\('c*'b)set"}\\ +@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\'a set\'b set"}\\ +@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\('b\'a)\('b*'b)set"}\\ +@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\('a*'a)set"}\\ +@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\ +@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\'a set"}\\ +@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\'b set"}\\ +@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\'a set"}\\ +@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\('a*'a)set\bool"}\\ +@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\bool"}\\ +@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\bool"}\\ +@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\bool"}\\ +@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\bool"}\\ +@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\bool"}\\ +@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\('a*'a)set\bool"}\\ +@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\bool"}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$) +\end{tabular} + +\section{Equiv\_Relations} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \ ('a*'a)set\bool"}\\ +@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \ ('a \ 'a) set \ 'a set set"}\\ +@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\('a\'b)\bool"}\\ +@{const Equiv_Relations.congruent2} & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\('b*'b)set\('a\'b\'c)\bool"}\\ +%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"congruent r f"} & @{term[source]"congruent r f"}\\ +@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\ +\end{tabular} + + +\section{Transitive\_Closure} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\('a*'a)set"}\\ +@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\('a*'a)set"}\\ +@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\('a*'a)set"}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\verb$^*$)\\ +@{term"trancl r"} & @{term[source]"trancl r"} & (\verb$^+$)\\ +@{term"reflcl r"} & @{term[source]"reflcl r"} & (\verb$^=$) +\end{tabular} + + +\section{Algebra} + +Theories @{theory OrderedGroup}, @{theory Ring_and_Field} and @{theory +Divides} define a large collection of classes describing common algebraic +structures from semigroups up to fields. Everything is done in terms of +overloaded operators: + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +@{text "0"} & @{typeof zero}\\ +@{text "1"} & @{typeof one}\\ +@{const plus} & @{typeof plus}\\ +@{const minus} & @{typeof minus}\\ +@{const uminus} & @{typeof uminus} & (\verb$-$)\\ +@{const times} & @{typeof times}\\ +@{const inverse} & @{typeof inverse}\\ +@{const divide} & @{typeof divide}\\ +@{const abs} & @{typeof abs}\\ +@{const sgn} & @{typeof sgn}\\ +@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\ +@{const div_class.div} & @{typeof "div_class.div"}\\ +@{const div_class.mod} & @{typeof "div_class.mod"}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"abs x"} & @{term[source]"abs x"} +\end{tabular} + + +\section{Nat} + +@{datatype nat} +\bigskip + +\begin{tabular}{@ {} lllllll @ {}} +@{term "op + :: nat \ nat \ nat"} & +@{term "op - :: nat \ nat \ nat"} & +@{term "op * :: nat \ nat \ nat"} & +@{term "op ^ :: nat \ nat \ nat"} & +@{term "op div :: nat \ nat \ nat"}& +@{term "op mod :: nat \ nat \ nat"}& +@{term "op dvd :: nat \ nat \ bool"}\\ +@{term "op \ :: nat \ nat \ bool"} & +@{term "op < :: nat \ nat \ bool"} & +@{term "min :: nat \ nat \ nat"} & +@{term "max :: nat \ nat \ nat"} & +@{term "Min :: nat set \ nat"} & +@{term "Max :: nat set \ nat"}\\ +\end{tabular} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Nat.of_nat} & @{typeof Nat.of_nat} +\end{tabular} + +\section{Int} + +Type @{typ int} +\bigskip + +\begin{tabular}{@ {} llllllll @ {}} +@{term "op + :: int \ int \ int"} & +@{term "op - :: int \ int \ int"} & +@{term "uminus :: int \ int"} & +@{term "op * :: int \ int \ int"} & +@{term "op ^ :: int \ nat \ int"} & +@{term "op div :: int \ int \ int"}& +@{term "op mod :: int \ int \ int"}& +@{term "op dvd :: int \ int \ bool"}\\ +@{term "op \ :: int \ int \ bool"} & +@{term "op < :: int \ int \ bool"} & +@{term "min :: int \ int \ int"} & +@{term "max :: int \ int \ int"} & +@{term "Min :: int set \ int"} & +@{term "Max :: int set \ int"}\\ +@{term "abs :: int \ int"} & +@{term "sgn :: int \ int"}\\ +\end{tabular} + +\begin{tabular}{@ {} l @ {~::~} l l @ {}} +@{const Int.nat} & @{typeof Int.nat}\\ +@{const Int.of_int} & @{typeof Int.of_int}\\ +@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\verb$Ints$) +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"of_nat::nat\int"} & @{term[source]"of_nat"}\\ +\end{tabular} + + +\section{Finite\_Set} + + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\bool"}\\ +@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\ +@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b"}\\ +@{const Finite_Set.fold_image} & @{typ "('b \ 'b \ 'b) \ ('a \ 'b) \ 'b \ 'a set \ 'b"}\\ +@{const Finite_Set.setsum} & @{term_type_only Finite_Set.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\ +@{const Finite_Set.setprod} & @{term_type_only Finite_Set.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\ +\end{supertabular} + + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term"setsum (%x. x) A"} & @{term[source]"setsum (\x. x) A"} & (\verb$SUM$)\\ +@{term"setsum (%x. t) A"} & @{term[source]"setsum (\x. t) A"}\\ +@{term[source]"\x|P. t"} & @{term"\x|P. t"}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\"} instead of @{text"\"}} & (\verb$PROD$)\\ +\end{supertabular} + + +\section{Wellfounded} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\bool"}\\ +@{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\bool"}\\ +@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\'a set"}\\ +@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\nat)\('a*'a)set"}\\ +@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\('b*'b)set\(('a*'b)*('a*'b))set"}\\ +@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\nat)\('a*'a)set\('a*'a)set"}\\ +@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ +@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ +\end{supertabular} + + +\section{SetInterval} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const lessThan} & @{term_type_only lessThan "'a::ord \ 'a set"}\\ +@{const atMost} & @{term_type_only atMost "'a::ord \ 'a set"}\\ +@{const greaterThan} & @{term_type_only greaterThan "'a::ord \ 'a set"}\\ +@{const atLeast} & @{term_type_only atLeast "'a::ord \ 'a set"}\\ +@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \ 'a \ 'a set"}\\ +@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \ 'a \ 'a set"}\\ +@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \ 'a \ 'a set"}\\ +@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \ 'a \ 'a set"}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term "lessThan y"} & @{term[source] "lessThan y"}\\ +@{term "atMost y"} & @{term[source] "atMost y"}\\ +@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\ +@{term "atLeast x"} & @{term[source] "atLeast x"}\\ +@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\ +@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\ +@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\ +@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\ +@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\ i \ {..n}. A"}\\ +@{term[mode=xsymbols] "UN i:{.. i \ {.."} instead of @{text"\"}}\\ +@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\x. t) {a..b}"}\\ +@{term "setsum (%x. t) {a..x. t) {a..x. t) {..b}"}\\ +@{term "setsum (%x. t) {..x. t) {.."} instead of @{text"\"}}\\ +\end{supertabular} + + +\section{Power} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Power.power} & @{typeof Power.power} +\end{tabular} + + +\section{Iterated Functions and Relations} + +Theory: @{theory Relation_Power} + +Iterated functions \ @{term[source]"(f::'a\'a) ^ n"} \ +and relations \ @{term[source]"(r::('a\'a)set) ^ n"}. + + +\section{Option} + +@{datatype option} +\bigskip + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Option.the} & @{typeof Option.the}\\ +@{const Option.map} & @{typ[source]"('a \ 'b) \ 'a option \ 'b option"}\\ +@{const Option.set} & @{term_type_only Option.set "'a option \ 'a set"} +\end{tabular} + +\section{List} + +@{datatype list} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const List.append} & @{typeof List.append}\\ +@{const List.butlast} & @{typeof List.butlast}\\ +@{const List.concat} & @{typeof List.concat}\\ +@{const List.distinct} & @{typeof List.distinct}\\ +@{const List.drop} & @{typeof List.drop}\\ +@{const List.dropWhile} & @{typeof List.dropWhile}\\ +@{const List.filter} & @{typeof List.filter}\\ +@{const List.foldl} & @{typeof List.foldl}\\ +@{const List.foldr} & @{typeof List.foldr}\\ +@{const List.hd} & @{typeof List.hd}\\ +@{const List.last} & @{typeof List.last}\\ +@{const List.length} & @{typeof List.length}\\ +@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\('a list * 'a list)set"}\\ +@{const List.lex} & @{term_type_only List.lex "('a*'a)set\('a list * 'a list)set"}\\ +@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\nat\('a list * 'a list)set"}\\ +@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\('a list * 'a list)set"}\\ +@{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\('a list * 'a list)set"}\\ +@{const List.lists} & @{term_type_only List.lists "'a set\'a list set"}\\ +@{const List.listset} & @{term_type_only List.listset "'a set list \ 'a list set"}\\ +@{const List.listsum} & @{typeof List.listsum}\\ +@{const List.list_all2} & @{typeof List.list_all2}\\ +@{const List.list_update} & @{typeof List.list_update}\\ +@{const List.map} & @{typeof List.map}\\ +@{const List.measures} & @{term_type_only List.measures "('a\nat)list\('a*'a)set"}\\ +@{const List.remdups} & @{typeof List.remdups}\\ +@{const List.removeAll} & @{typeof List.removeAll}\\ +@{const List.remove1} & @{typeof List.remove1}\\ +@{const List.replicate} & @{typeof List.replicate}\\ +@{const List.rev} & @{typeof List.rev}\\ +@{const List.rotate} & @{typeof List.rotate}\\ +@{const List.rotate1} & @{typeof List.rotate1}\\ +@{const List.set} & @{term_type_only List.set "'a list \ 'a set"}\\ +@{const List.sort} & @{typeof List.sort}\\ +@{const List.sorted} & @{typeof List.sorted}\\ +@{const List.splice} & @{typeof List.splice}\\ +@{const List.sublist} & @{typeof List.sublist}\\ +@{const List.take} & @{typeof List.take}\\ +@{const List.takeWhile} & @{typeof List.takeWhile}\\ +@{const List.tl} & @{typeof List.tl}\\ +@{const List.upt} & @{typeof List.upt}\\ +@{const List.upto} & @{typeof List.upto}\\ +@{const List.zip} & @{typeof List.zip}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{text"[x\<^isub>1,\,x\<^isub>n]"} & @{text"x\<^isub>1 # \ # x\<^isub>n # []"}\\ +@{term"[m.. xs]"} & @{term"map (%x. e) xs"}\\ +@{term"[x \ xs. b]"} & @{term[source]"filter (\x. b) xs"} \\ +@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ +@{term"\x\xs. e"} & @{term[source]"listsum (map (\x. e) xs)"}\\ +\end{supertabular} +\medskip + +List comprehension: @{text"[e. q\<^isub>1, \, q\<^isub>n]"} where each +qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \ e"}} or a +guard, i.e.\ boolean expression. + +\section{Map} + +Maps model partial functions and are often used as finite tables. However, +the domain of a map may be infinite. + +@{text"'a \ 'b = 'a \ 'b option"} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Map.empty} & @{typeof Map.empty}\\ +@{const Map.map_add} & @{typeof Map.map_add}\\ +@{const Map.map_comp} & @{typeof Map.map_comp}\\ +@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\'b option)\'a set\('a\'b option)"}\\ +@{const Map.dom} & @{term_type_only Map.dom "('a\'b option)\'a set"}\\ +@{const Map.ran} & @{term_type_only Map.ran "('a\'b option)\'b set"}\\ +@{const Map.map_le} & @{typeof Map.map_le}\\ +@{const Map.map_of} & @{typeof Map.map_of}\\ +@{const Map.map_upds} & @{typeof Map.map_upds}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"Map.empty"} & @{term"\x. None"}\\ +@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ +@{text"m(x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n)"} & @{text[source]"m(x\<^isub>1\y\<^isub>1)\(x\<^isub>n\y\<^isub>n)"}\\ +@{text"[x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n]"} & @{text[source]"Map.empty(x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n)"}\\ +@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ +\end{tabular} + +*} +(*<*) +end +(*>*) \ No newline at end of file diff -r d21bc48823b7 -r 28b487cd9e15 doc-src/Main/Docs/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/Docs/ROOT.ML Wed Mar 11 20:11:06 2009 +0100 @@ -0,0 +1,1 @@ +use_thy "Main_Doc"; diff -r d21bc48823b7 -r 28b487cd9e15 doc-src/Main/Docs/document/Main_Doc.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/Docs/document/Main_Doc.tex Wed Mar 11 20:11:06 2009 +0100 @@ -0,0 +1,597 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Main{\isacharunderscore}Doc}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isadelimML +% +\endisadelimML +% +\isatagML +% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\begin{isamarkuptext}% +\begin{abstract} +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/}. +\end{abstract} + +\section{HOL} + +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}. +\smallskip + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{undefined} & \isa{{\isacharprime}a}\\ +\isa{default} & \isa{{\isacharprime}a}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{x\ {\isasymnoteq}\ y} & \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}} & (\verb$~=$)\\ +\isa{{\isachardoublequote}P\ {\isasymlongleftrightarrow}\ Q{\isachardoublequote}} & \isa{P\ {\isacharequal}\ Q} \\ +\isa{if\ x\ then\ y\ else\ z} & \isa{{\isachardoublequote}If\ x\ y\ z{\isachardoublequote}}\\ +\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}}\\ +\end{supertabular} + + +\section{Orderings} + +A collection of classes defining basic orderings: +preorder, partial order, linear order, dense linear order and wellorder. +\smallskip + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\isa{op\ {\isasymle}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (\verb$<=$)\\ +\isa{op\ {\isacharless}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\ +\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{min} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{max} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{top} & \isa{{\isacharprime}a}\\ +\isa{bot} & \isa{{\isacharprime}a}\\ +\isa{mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{strict{\isacharunderscore}mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{{\isachardoublequote}x\ {\isasymge}\ y{\isachardoublequote}} & \isa{y\ {\isasymle}\ x} & (\verb$>=$)\\ +\isa{{\isachardoublequote}x\ {\isachargreater}\ y{\isachardoublequote}} & \isa{y\ {\isacharless}\ x}\\ +\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P{\isachardoublequote}}\\ +\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P{\isachardoublequote}}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ +\isa{LEAST\ x{\isachardot}\ P} & \isa{{\isachardoublequote}Least\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ +\end{supertabular} + + +\section{Lattices} + +Classes semilattice, lattice, distributive lattice and complete lattice (the +latter in theory \isa{Set}). + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{inf} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{sup} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{Inf} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{Sup} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\end{tabular} + +\subsubsection*{Syntax} + +Available by loading theory \isa{Lattice{\isacharunderscore}Syntax} in directory \isa{Library}. + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{{\isachardoublequote}x\ {\isasymsqsubseteq}\ y{\isachardoublequote}} & \isa{x\ {\isasymle}\ y}\\ +\isa{{\isachardoublequote}x\ {\isasymsqsubset}\ y{\isachardoublequote}} & \isa{x\ {\isacharless}\ y}\\ +\isa{{\isachardoublequote}x\ {\isasymsqinter}\ y{\isachardoublequote}} & \isa{inf\ x\ y}\\ +\isa{{\isachardoublequote}x\ {\isasymsqunion}\ y{\isachardoublequote}} & \isa{sup\ x\ y}\\ +\isa{{\isachardoublequote}{\isasymSqinter}\ A{\isachardoublequote}} & \isa{Sup\ A}\\ +\isa{{\isachardoublequote}{\isasymSqunion}\ A{\isachardoublequote}} & \isa{Inf\ A}\\ +\isa{{\isachardoublequote}{\isasymtop}{\isachardoublequote}} & \isa{top}\\ +\isa{{\isachardoublequote}{\isasymbottom}{\isachardoublequote}} & \isa{bot}\\ +\end{supertabular} + + +\section{Set} + +Sets are predicates: \isa{{\isachardoublequote}{\isacharprime}a\ set\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\isa{{\isacharbraceleft}{\isacharbraceright}} & \isa{{\isacharprime}a\ set}\\ +\isa{insert} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{Collect} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{op\ {\isasymin}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool} & (\texttt{:})\\ +\isa{op\ {\isasymunion}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Un})\\ +\isa{op\ {\isasyminter}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Int})\\ +\isa{UNION} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{INTER} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{Union} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{Inter} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{Pow} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\ +\isa{UNIV} & \isa{{\isacharprime}a\ set}\\ +\isa{op\ {\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{Ball} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{Bex} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\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}}\\ +\isa{x\ {\isasymnotin}\ A} & \isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isasymin}\ A{\isacharparenright}{\isachardoublequote}}\\ +\isa{A\ {\isasymsubseteq}\ B} & \isa{{\isachardoublequote}A\ {\isasymle}\ B{\isachardoublequote}}\\ +\isa{A\ {\isasymsubset}\ B} & \isa{{\isachardoublequote}A\ {\isacharless}\ B{\isachardoublequote}}\\ +\isa{{\isachardoublequote}A\ {\isasymsupseteq}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isasymle}\ A{\isachardoublequote}}\\ +\isa{{\isachardoublequote}A\ {\isasymsupset}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isacharless}\ A{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}} & \isa{{\isachardoublequote}Collect\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ +\isa{{\isasymUnion}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{UN})\\ +\isa{{\isasymUnion}x{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\ +\isa{{\isasymInter}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{INT})\\ +\isa{{\isasymInter}x{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\ +\isa{{\isasymforall}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Ball\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ +\isa{{\isasymexists}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Bex\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ +\isa{range\ f} & \isa{{\isachardoublequote}f\ {\isacharbackquote}\ UNIV{\isachardoublequote}}\\ +\end{supertabular} + + +\section{Fun} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{id} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\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}\\ +\isa{inj{\isacharunderscore}on} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\ +\isa{inj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{surj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{bij} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{bij{\isacharunderscore}betw} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ bool}\\ +\isa{fun{\isacharunderscore}upd} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{f{\isacharparenleft}x\ {\isacharcolon}{\isacharequal}\ y{\isacharparenright}} & \isa{{\isachardoublequote}fun{\isacharunderscore}upd\ f\ x\ y{\isachardoublequote}}\\ +\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}}\\ +\end{tabular} + + +\section{Fixed Points} + +Theory: \isa{Inductive}. + +Least and greatest fixed points in a complete lattice \isa{{\isacharprime}a}: + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{lfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{gfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\end{tabular} + +Note that in particular sets (\isa{{\isacharprime}a\ {\isasymRightarrow}\ bool}) are complete lattices. + +\section{Sum\_Type} + +Type constructor \isa{{\isacharplus}}. + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{Inl} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isacharplus}\ {\isacharprime}b}\\ +\isa{Inr} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isacharplus}\ {\isacharprime}a}\\ +\isa{op\ {\isacharless}{\isacharplus}{\isachargreater}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharplus}\ {\isacharprime}b{\isacharparenright}\ set} +\end{tabular} + + +\section{Product\_Type} + +Types \isa{unit} and \isa{{\isasymtimes}}. + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{{\isacharparenleft}{\isacharparenright}} & \isa{unit}\\ +\isa{Pair} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}\\ +\isa{fst} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{snd} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{split} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\ +\isa{curry} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\ +\isa{Sigma} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} +\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}} & \isa{{\isachardoublequote}Pair\ a\ b{\isachardoublequote}}\\ +\isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} & \isa{{\isachardoublequote}split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}{\isachardoublequote}}\\ +\isa{A\ {\isasymtimes}\ B} & \isa{Sigma\ A\ {\isacharparenleft}{\isasymlambda}\_{\isachardot}\ B{\isacharparenright}} & (\verb$<*>$) +\end{tabular} + +Pairs may be nested. Nesting to the right is printed as a tuple, +e.g.\ \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ c{\isacharparenright}}} is really \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ {\isacharparenleft}b{\isacharcomma}\ c{\isacharparenright}{\isacharparenright}}.} +Pattern matching with pairs and tuples extends to all binders, +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. + + +\section{Relation} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{converse} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\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}\\ +\isa{op\ {\isacharbackquote}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\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}\\ +\isa{Id{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{Id} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{Domain} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{Range} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{Field} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{refl{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{refl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{sym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{antisym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{trans} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{irrefl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{total{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{total} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{r{\isasyminverse}} & \isa{{\isachardoublequote}converse\ r{\isachardoublequote}} & (\verb$^-1$) +\end{tabular} + +\section{Equiv\_Relations} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{equiv} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{op\ {\isacharslash}{\isacharslash}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\ +\isa{congruent} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\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}\\ +%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{f\ respects\ r} & \isa{{\isachardoublequote}congruent\ r\ f{\isachardoublequote}}\\ +\isa{f\ respects{\isadigit{2}}\ r} & \isa{{\isachardoublequote}congruent{\isadigit{2}}\ r\ r\ f{\isachardoublequote}}\\ +\end{tabular} + + +\section{Transitive\_Closure} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{rtrancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{trancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{reflcl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{r\isactrlsup {\isacharasterisk}} & \isa{{\isachardoublequote}rtrancl\ r{\isachardoublequote}} & (\verb$^*$)\\ +\isa{r\isactrlsup {\isacharplus}} & \isa{{\isachardoublequote}trancl\ r{\isachardoublequote}} & (\verb$^+$)\\ +\isa{r\isactrlsup {\isacharequal}} & \isa{{\isachardoublequote}reflcl\ r{\isachardoublequote}} & (\verb$^=$) +\end{tabular} + + +\section{Algebra} + +Theories \isa{OrderedGroup}, \isa{Ring{\isacharunderscore}and{\isacharunderscore}Field} and \isa{Divides} define a large collection of classes describing common algebraic +structures from semigroups up to fields. Everything is done in terms of +overloaded operators: + +\begin{supertabular}{@ {} l @ {~::~} l l @ {}} +\isa{{\isadigit{0}}} & \isa{{\isacharprime}a}\\ +\isa{{\isadigit{1}}} & \isa{{\isacharprime}a}\\ +\isa{op\ {\isacharplus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{op\ {\isacharminus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{uminus} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (\verb$-$)\\ +\isa{op\ {\isacharasterisk}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{inverse} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{op\ {\isacharslash}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{abs} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{sgn} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{op\ dvd} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\ +\isa{op\ div} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{op\ mod} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{{\isasymbar}x{\isasymbar}} & \isa{{\isachardoublequote}abs\ x{\isachardoublequote}} +\end{tabular} + + +\section{Nat} + +\isa{\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat} +\bigskip + +\begin{tabular}{@ {} lllllll @ {}} +\isa{op\ {\isacharplus}} & +\isa{op\ {\isacharminus}} & +\isa{op\ {\isacharasterisk}} & +\isa{op\ {\isacharcircum}} & +\isa{op\ div}& +\isa{op\ mod}& +\isa{op\ dvd}\\ +\isa{op\ {\isasymle}} & +\isa{op\ {\isacharless}} & +\isa{min} & +\isa{max} & +\isa{Min} & +\isa{Max}\\ +\end{tabular} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a} +\end{tabular} + +\section{Int} + +Type \isa{int} +\bigskip + +\begin{tabular}{@ {} llllllll @ {}} +\isa{op\ {\isacharplus}} & +\isa{op\ {\isacharminus}} & +\isa{uminus} & +\isa{op\ {\isacharasterisk}} & +\isa{op\ {\isacharcircum}} & +\isa{op\ div}& +\isa{op\ mod}& +\isa{op\ dvd}\\ +\isa{op\ {\isasymle}} & +\isa{op\ {\isacharless}} & +\isa{min} & +\isa{max} & +\isa{Min} & +\isa{Max}\\ +\isa{abs} & +\isa{sgn}\\ +\end{tabular} + +\begin{tabular}{@ {} l @ {~::~} l l @ {}} +\isa{nat} & \isa{int\ {\isasymRightarrow}\ nat}\\ +\isa{of{\isacharunderscore}int} & \isa{int\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{{\isasymint}} & \isa{{\isacharprime}a\ set} & (\verb$Ints$) +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{int} & \isa{{\isachardoublequote}of{\isacharunderscore}nat{\isachardoublequote}}\\ +\end{tabular} + + +\section{Finite\_Set} + + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{finite} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\ +\isa{card} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ nat}\\ +\isa{fold} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\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}\\ +\isa{setsum} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{setprod} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\end{supertabular} + + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +\isa{{\isasymSum}A} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x{\isacharparenright}\ A{\isachardoublequote}} & (\verb$SUM$)\\ +\isa{{\isasymSum}x{\isasymin}A{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ A{\isachardoublequote}}\\ +\isa{{\isachardoublequote}{\isasymSum}x{\isacharbar}P{\isachardot}\ t{\isachardoublequote}} & \isa{{\isasymSum}x{\isasymin}{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}{\isachardot}\ t}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}} & (\verb$PROD$)\\ +\end{supertabular} + + +\section{Wellfounded} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{wf} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{acyclic} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ +\isa{acc} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{measure} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\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}\\ +\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}\\ +\isa{less{\isacharunderscore}than} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\ +\isa{pred{\isacharunderscore}nat} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\ +\end{supertabular} + + +\section{SetInterval} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{lessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{atMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{greaterThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{atLeast} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{greaterThanLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{atLeastLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{greaterThanAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{atLeastAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{{\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}lessThan\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atMost\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThan\ x{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}atLeast\ x{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanLessThan\ x\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastLessThan\ x\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanAtMost\ x\ y{\isachardoublequote}}\\ +\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastAtMost\ x\ y{\isachardoublequote}}\\ +\isa{{\isasymUnion}\ i{\isasymle}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\ +\isa{{\isasymUnion}\ i{\isacharless}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymInter}} instead of \isa{{\isasymUnion}}}\\ +\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}}\\ +\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}}\\ +\isa{{\isasymSum}x{\isasymle}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\ +\isa{{\isasymSum}x{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}}\\ +\end{supertabular} + + +\section{Power} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{op\ {\isacharcircum}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} +\end{tabular} + + +\section{Iterated Functions and Relations} + +Theory: \isa{Relation{\isacharunderscore}Power} + +Iterated functions \ \isa{{\isachardoublequote}{\isacharparenleft}f{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isasymRightarrow}{\isacharprime}a{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}} \ +and relations \ \isa{{\isachardoublequote}{\isacharparenleft}r{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}a{\isacharparenright}set{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}}. + + +\section{Option} + +\isa{\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a} +\bigskip + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +\isa{the} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{Option{\isachardot}map} & \isa{{\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequote}}\\ +\isa{Option{\isachardot}set} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a\ set} +\end{tabular} + +\section{List} + +\isa{\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ op\ {\isacharhash}\ {\isacharprime}a\ {\isacharparenleft}{\isacharprime}a\ list{\isacharparenright}} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{op\ {\isacharat}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{butlast} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{concat} & \isa{{\isacharprime}a\ list\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{distinct} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\ +\isa{drop} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{dropWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{filter} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{foldl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{foldr} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\ +\isa{hd} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{last} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\isa{length} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat}\\ +\isa{lenlex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{lex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{lexn} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{lexord} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{listrel} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ +\isa{lists} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\ +\isa{listset} & \isa{{\isacharprime}a\ set\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\ +\isa{listsum} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ +\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}\\ +\isa{list{\isacharunderscore}update} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{map} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list}\\ +\isa{measures} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ +\isa{remdups} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{removeAll} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{remove{\isadigit{1}}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{replicate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{rev} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{rotate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{rotate{\isadigit{1}}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{set} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{sort} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{sorted} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\ +\isa{splice} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{sublist} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{take} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{takeWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{tl} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{upt} & \isa{nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ list}\\ +\isa{upto} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ +\isa{zip} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\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}}\\ +\isa{{\isacharbrackleft}m{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}} & \isa{{\isachardoublequote}upt\ m\ n{\isachardoublequote}}\\ +\isa{{\isacharbrackleft}i{\isachardot}{\isachardot}j{\isacharbrackright}} & \isa{{\isachardoublequote}upto\ i\ j{\isachardoublequote}}\\ +\isa{{\isacharbrackleft}e{\isachardot}\ x\ {\isasymleftarrow}\ xs{\isacharbrackright}} & \isa{map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs}\\ +\isa{{\isacharbrackleft}x{\isasymleftarrow}xs\ {\isachardot}\ b{\isacharbrackright}} & \isa{{\isachardoublequote}filter\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}\ xs{\isachardoublequote}} \\ +\isa{xs{\isacharbrackleft}n\ {\isacharcolon}{\isacharequal}\ x{\isacharbrackright}} & \isa{{\isachardoublequote}list{\isacharunderscore}update\ xs\ n\ x{\isachardoublequote}}\\ +\isa{{\isasymSum}x{\isasymleftarrow}xs{\isachardot}\ e} & \isa{{\isachardoublequote}listsum\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}}\\ +\end{supertabular} +\medskip + +List comprehension: \isa{{\isacharbrackleft}e{\isachardot}\ q\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ q\isactrlisub n{\isacharbrackright}} where each +qualifier \isa{q\isactrlisub i} is either a generator \mbox{\isa{pat\ {\isasymleftarrow}\ e}} or a +guard, i.e.\ boolean expression. + +\section{Map} + +Maps model partial functions and are often used as finite tables. However, +the domain of a map may be infinite. + +\isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +\isa{Map{\isachardot}empty} & \isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ +\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}\\ +\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}\\ +\isa{op\ {\isacharbar}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ +\isa{dom} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ +\isa{ran} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ +\isa{op\ {\isasymsubseteq}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ +\isa{map{\isacharunderscore}of} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ +\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}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +\isa{Map{\isachardot}empty} & \isa{{\isasymlambda}x{\isachardot}\ None}\\ +\isa{m{\isacharparenleft}x\ {\isasymmapsto}\ y{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x{\isacharcolon}{\isacharequal}Some\ y{\isacharparenright}{\isachardoublequote}}\\ +\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}}\\ +\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}}\\ +\isa{m{\isacharparenleft}xs\ {\isacharbrackleft}{\isasymmapsto}{\isacharbrackright}\ ys{\isacharparenright}} & \isa{{\isachardoublequote}map{\isacharunderscore}upds\ m\ xs\ ys{\isachardoublequote}}\\ +\end{tabular}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r d21bc48823b7 -r 28b487cd9e15 doc-src/Main/IsaMakefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/IsaMakefile Wed Mar 11 20:11:06 2009 +0100 @@ -0,0 +1,31 @@ + +## targets + +default: HOL-Docs +images: +test: HOL-Docs + +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src +OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document + + +## sessions + +HOL-Docs: $(LOG)/HOL-Docs.gz + +$(LOG)/HOL-Docs.gz: Docs/Main_Doc.thy Docs/ROOT.ML + @$(USEDIR) HOL Docs + + +## clean + +clean: + @rm -f $(LOG)/HOL-Docs.gz diff -r d21bc48823b7 -r 28b487cd9e15 doc-src/Main/Main_Doc.tex --- a/doc-src/Main/Main_Doc.tex Wed Mar 11 20:09:23 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,597 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{Main{\isacharunderscore}Doc}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -% -\begin{isamarkuptext}% -\begin{abstract} -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/}. -\end{abstract} - -\section{HOL} - -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}. -\smallskip - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{undefined} & \isa{{\isacharprime}a}\\ -\isa{default} & \isa{{\isacharprime}a}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{x\ {\isasymnoteq}\ y} & \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}} & (\verb$~=$)\\ -\isa{{\isachardoublequote}P\ {\isasymlongleftrightarrow}\ Q{\isachardoublequote}} & \isa{P\ {\isacharequal}\ Q} \\ -\isa{if\ x\ then\ y\ else\ z} & \isa{{\isachardoublequote}If\ x\ y\ z{\isachardoublequote}}\\ -\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}}\\ -\end{supertabular} - - -\section{Orderings} - -A collection of classes defining basic orderings: -preorder, partial order, linear order, dense linear order and wellorder. -\smallskip - -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} -\isa{op\ {\isasymle}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (\verb$<=$)\\ -\isa{op\ {\isacharless}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\ -\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{min} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{max} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{top} & \isa{{\isacharprime}a}\\ -\isa{bot} & \isa{{\isacharprime}a}\\ -\isa{mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ -\isa{strict{\isacharunderscore}mono} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{{\isachardoublequote}x\ {\isasymge}\ y{\isachardoublequote}} & \isa{y\ {\isasymle}\ x} & (\verb$>=$)\\ -\isa{{\isachardoublequote}x\ {\isachargreater}\ y{\isachardoublequote}} & \isa{y\ {\isacharless}\ x}\\ -\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P{\isachardoublequote}}\\ -\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P{\isachardoublequote}}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ -\isa{LEAST\ x{\isachardot}\ P} & \isa{{\isachardoublequote}Least\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ -\end{supertabular} - - -\section{Lattices} - -Classes semilattice, lattice, distributive lattice and complete lattice (the -latter in theory \isa{Set}). - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{inf} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{sup} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{Inf} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{Sup} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\end{tabular} - -\subsubsection*{Syntax} - -Available by loading theory \isa{Lattice{\isacharunderscore}Syntax} in directory \isa{Library}. - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{{\isachardoublequote}x\ {\isasymsqsubseteq}\ y{\isachardoublequote}} & \isa{x\ {\isasymle}\ y}\\ -\isa{{\isachardoublequote}x\ {\isasymsqsubset}\ y{\isachardoublequote}} & \isa{x\ {\isacharless}\ y}\\ -\isa{{\isachardoublequote}x\ {\isasymsqinter}\ y{\isachardoublequote}} & \isa{inf\ x\ y}\\ -\isa{{\isachardoublequote}x\ {\isasymsqunion}\ y{\isachardoublequote}} & \isa{sup\ x\ y}\\ -\isa{{\isachardoublequote}{\isasymSqinter}\ A{\isachardoublequote}} & \isa{Sup\ A}\\ -\isa{{\isachardoublequote}{\isasymSqunion}\ A{\isachardoublequote}} & \isa{Inf\ A}\\ -\isa{{\isachardoublequote}{\isasymtop}{\isachardoublequote}} & \isa{top}\\ -\isa{{\isachardoublequote}{\isasymbottom}{\isachardoublequote}} & \isa{bot}\\ -\end{supertabular} - - -\section{Set} - -Sets are predicates: \isa{{\isachardoublequote}{\isacharprime}a\ set\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}} -\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} -\isa{{\isacharbraceleft}{\isacharbraceright}} & \isa{{\isacharprime}a\ set}\\ -\isa{insert} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{Collect} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{op\ {\isasymin}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool} & (\texttt{:})\\ -\isa{op\ {\isasymunion}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Un})\\ -\isa{op\ {\isasyminter}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set} & (\texttt{Int})\\ -\isa{UNION} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ -\isa{INTER} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ -\isa{Union} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{Inter} & \isa{{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{Pow} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\ -\isa{UNIV} & \isa{{\isacharprime}a\ set}\\ -\isa{op\ {\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ -\isa{Ball} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ -\isa{Bex} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\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}}\\ -\isa{x\ {\isasymnotin}\ A} & \isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isasymin}\ A{\isacharparenright}{\isachardoublequote}}\\ -\isa{A\ {\isasymsubseteq}\ B} & \isa{{\isachardoublequote}A\ {\isasymle}\ B{\isachardoublequote}}\\ -\isa{A\ {\isasymsubset}\ B} & \isa{{\isachardoublequote}A\ {\isacharless}\ B{\isachardoublequote}}\\ -\isa{{\isachardoublequote}A\ {\isasymsupseteq}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isasymle}\ A{\isachardoublequote}}\\ -\isa{{\isachardoublequote}A\ {\isasymsupset}\ B{\isachardoublequote}} & \isa{{\isachardoublequote}B\ {\isacharless}\ A{\isachardoublequote}}\\ -\isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}} & \isa{{\isachardoublequote}Collect\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ -\isa{{\isasymUnion}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{UN})\\ -\isa{{\isasymUnion}x{\isachardot}\ A} & \isa{{\isachardoublequote}UNION\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\ -\isa{{\isasymInter}x{\isasymin}I{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ I\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}} & (\texttt{INT})\\ -\isa{{\isasymInter}x{\isachardot}\ A} & \isa{{\isachardoublequote}INTER\ UNIV\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ A{\isacharparenright}{\isachardoublequote}}\\ -\isa{{\isasymforall}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Ball\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ -\isa{{\isasymexists}x{\isasymin}A{\isachardot}\ P} & \isa{{\isachardoublequote}Bex\ A\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ P{\isacharparenright}{\isachardoublequote}}\\ -\isa{range\ f} & \isa{{\isachardoublequote}f\ {\isacharbackquote}\ UNIV{\isachardoublequote}}\\ -\end{supertabular} - - -\section{Fun} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{id} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\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}\\ -\isa{inj{\isacharunderscore}on} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\ -\isa{inj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ -\isa{surj} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ -\isa{bij} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ -\isa{bij{\isacharunderscore}betw} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ bool}\\ -\isa{fun{\isacharunderscore}upd} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{f{\isacharparenleft}x\ {\isacharcolon}{\isacharequal}\ y{\isacharparenright}} & \isa{{\isachardoublequote}fun{\isacharunderscore}upd\ f\ x\ y{\isachardoublequote}}\\ -\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}}\\ -\end{tabular} - - -\section{Fixed Points} - -Theory: \isa{Inductive}. - -Least and greatest fixed points in a complete lattice \isa{{\isacharprime}a}: - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{lfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{gfp} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\end{tabular} - -Note that in particular sets (\isa{{\isacharprime}a\ {\isasymRightarrow}\ bool}) are complete lattices. - -\section{Sum\_Type} - -Type constructor \isa{{\isacharplus}}. - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{Inl} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isacharplus}\ {\isacharprime}b}\\ -\isa{Inr} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isacharplus}\ {\isacharprime}a}\\ -\isa{op\ {\isacharless}{\isacharplus}{\isachargreater}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharplus}\ {\isacharprime}b{\isacharparenright}\ set} -\end{tabular} - - -\section{Product\_Type} - -Types \isa{unit} and \isa{{\isasymtimes}}. - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{{\isacharparenleft}{\isacharparenright}} & \isa{unit}\\ -\isa{Pair} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}\\ -\isa{fst} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{snd} & \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\ -\isa{split} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\ -\isa{curry} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c}\\ -\isa{Sigma} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} -\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}} & \isa{{\isachardoublequote}Pair\ a\ b{\isachardoublequote}}\\ -\isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} & \isa{{\isachardoublequote}split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}{\isachardoublequote}}\\ -\isa{A\ {\isasymtimes}\ B} & \isa{Sigma\ A\ {\isacharparenleft}{\isasymlambda}\_{\isachardot}\ B{\isacharparenright}} & (\verb$<*>$) -\end{tabular} - -Pairs may be nested. Nesting to the right is printed as a tuple, -e.g.\ \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharcomma}\ c{\isacharparenright}}} is really \mbox{\isa{{\isacharparenleft}a{\isacharcomma}\ {\isacharparenleft}b{\isacharcomma}\ c{\isacharparenright}{\isacharparenright}}.} -Pattern matching with pairs and tuples extends to all binders, -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. - - -\section{Relation} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{converse} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ -\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}\\ -\isa{op\ {\isacharbackquote}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ -\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}\\ -\isa{Id{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ -\isa{Id} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ -\isa{Domain} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{Range} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ -\isa{Field} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{refl{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{refl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{sym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{antisym} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{trans} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{irrefl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{total{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{total} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{r{\isasyminverse}} & \isa{{\isachardoublequote}converse\ r{\isachardoublequote}} & (\verb$^-1$) -\end{tabular} - -\section{Equiv\_Relations} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{equiv} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{op\ {\isacharslash}{\isacharslash}} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set}\\ -\isa{congruent} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ -\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}\\ -%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{f\ respects\ r} & \isa{{\isachardoublequote}congruent\ r\ f{\isachardoublequote}}\\ -\isa{f\ respects{\isadigit{2}}\ r} & \isa{{\isachardoublequote}congruent{\isadigit{2}}\ r\ r\ f{\isachardoublequote}}\\ -\end{tabular} - - -\section{Transitive\_Closure} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{rtrancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ -\isa{trancl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ -\isa{reflcl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{r\isactrlsup {\isacharasterisk}} & \isa{{\isachardoublequote}rtrancl\ r{\isachardoublequote}} & (\verb$^*$)\\ -\isa{r\isactrlsup {\isacharplus}} & \isa{{\isachardoublequote}trancl\ r{\isachardoublequote}} & (\verb$^+$)\\ -\isa{r\isactrlsup {\isacharequal}} & \isa{{\isachardoublequote}reflcl\ r{\isachardoublequote}} & (\verb$^=$) -\end{tabular} - - -\section{Algebra} - -Theories \isa{OrderedGroup}, \isa{Ring{\isacharunderscore}and{\isacharunderscore}Field} and \isa{Divides} define a large collection of classes describing common algebraic -structures from semigroups up to fields. Everything is done in terms of -overloaded operators: - -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} -\isa{{\isadigit{0}}} & \isa{{\isacharprime}a}\\ -\isa{{\isadigit{1}}} & \isa{{\isacharprime}a}\\ -\isa{op\ {\isacharplus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{op\ {\isacharminus}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{uminus} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (\verb$-$)\\ -\isa{op\ {\isacharasterisk}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{inverse} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{op\ {\isacharslash}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{abs} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{sgn} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{op\ dvd} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool}\\ -\isa{op\ div} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{op\ mod} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{{\isasymbar}x{\isasymbar}} & \isa{{\isachardoublequote}abs\ x{\isachardoublequote}} -\end{tabular} - - -\section{Nat} - -\isa{\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat} -\bigskip - -\begin{tabular}{@ {} lllllll @ {}} -\isa{op\ {\isacharplus}} & -\isa{op\ {\isacharminus}} & -\isa{op\ {\isacharasterisk}} & -\isa{op\ {\isacharcircum}} & -\isa{op\ div}& -\isa{op\ mod}& -\isa{op\ dvd}\\ -\isa{op\ {\isasymle}} & -\isa{op\ {\isacharless}} & -\isa{min} & -\isa{max} & -\isa{Min} & -\isa{Max}\\ -\end{tabular} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{of{\isacharunderscore}nat} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a} -\end{tabular} - -\section{Int} - -Type \isa{int} -\bigskip - -\begin{tabular}{@ {} llllllll @ {}} -\isa{op\ {\isacharplus}} & -\isa{op\ {\isacharminus}} & -\isa{uminus} & -\isa{op\ {\isacharasterisk}} & -\isa{op\ {\isacharcircum}} & -\isa{op\ div}& -\isa{op\ mod}& -\isa{op\ dvd}\\ -\isa{op\ {\isasymle}} & -\isa{op\ {\isacharless}} & -\isa{min} & -\isa{max} & -\isa{Min} & -\isa{Max}\\ -\isa{abs} & -\isa{sgn}\\ -\end{tabular} - -\begin{tabular}{@ {} l @ {~::~} l l @ {}} -\isa{nat} & \isa{int\ {\isasymRightarrow}\ nat}\\ -\isa{of{\isacharunderscore}int} & \isa{int\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{{\isasymint}} & \isa{{\isacharprime}a\ set} & (\verb$Ints$) -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{int} & \isa{{\isachardoublequote}of{\isacharunderscore}nat{\isachardoublequote}}\\ -\end{tabular} - - -\section{Finite\_Set} - - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{finite} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ bool}\\ -\isa{card} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ nat}\\ -\isa{fold} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ -\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}\\ -\isa{setsum} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ -\isa{setprod} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b}\\ -\end{supertabular} - - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{{\isasymSum}A} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x{\isacharparenright}\ A{\isachardoublequote}} & (\verb$SUM$)\\ -\isa{{\isasymSum}x{\isasymin}A{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ A{\isachardoublequote}}\\ -\isa{{\isachardoublequote}{\isasymSum}x{\isacharbar}P{\isachardot}\ t{\isachardoublequote}} & \isa{{\isasymSum}x{\isasymin}{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}{\isachardot}\ t}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}} & (\verb$PROD$)\\ -\end{supertabular} - - -\section{Wellfounded} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{wf} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{acyclic} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ bool}\\ -\isa{acc} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{measure} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ -\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}\\ -\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}\\ -\isa{less{\isacharunderscore}than} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\ -\isa{pred{\isacharunderscore}nat} & \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set}\\ -\end{supertabular} - - -\section{SetInterval} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{lessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{atMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{greaterThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{atLeast} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{greaterThanLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{atLeastLessThan} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{greaterThanAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{atLeastAtMost} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{{\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}lessThan\ y{\isachardoublequote}}\\ -\isa{{\isacharbraceleft}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atMost\ y{\isachardoublequote}}\\ -\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThan\ x{\isachardoublequote}}\\ -\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharbraceright}} & \isa{{\isachardoublequote}atLeast\ x{\isachardoublequote}}\\ -\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanLessThan\ x\ y{\isachardoublequote}}\\ -\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}{\isacharless}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastLessThan\ x\ y{\isachardoublequote}}\\ -\isa{{\isacharbraceleft}x{\isacharless}{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}greaterThanAtMost\ x\ y{\isachardoublequote}}\\ -\isa{{\isacharbraceleft}x{\isachardot}{\isachardot}y{\isacharbraceright}} & \isa{{\isachardoublequote}atLeastAtMost\ x\ y{\isachardoublequote}}\\ -\isa{{\isasymUnion}\ i{\isasymle}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\ -\isa{{\isasymUnion}\ i{\isacharless}n{\isachardot}\ A} & \isa{{\isachardoublequote}{\isasymUnion}\ i\ {\isasymin}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardot}\ A{\isachardoublequote}}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymInter}} instead of \isa{{\isasymUnion}}}\\ -\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}}\\ -\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}}\\ -\isa{{\isasymSum}x{\isasymle}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}b{\isacharbraceright}{\isachardoublequote}}\\ -\isa{{\isasymSum}x{\isacharless}b{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}b{\isacharbraceright}{\isachardoublequote}}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}}\\ -\end{supertabular} - - -\section{Power} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{op\ {\isacharcircum}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} -\end{tabular} - - -\section{Iterated Functions and Relations} - -Theory: \isa{Relation{\isacharunderscore}Power} - -Iterated functions \ \isa{{\isachardoublequote}{\isacharparenleft}f{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isasymRightarrow}{\isacharprime}a{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}} \ -and relations \ \isa{{\isachardoublequote}{\isacharparenleft}r{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}a{\isacharparenright}set{\isacharparenright}\ {\isacharcircum}\ n{\isachardoublequote}}. - - -\section{Option} - -\isa{\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a} -\bigskip - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{the} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{Option{\isachardot}map} & \isa{{\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}b\ option{\isachardoublequote}}\\ -\isa{Option{\isachardot}set} & \isa{{\isacharprime}a\ option\ {\isasymRightarrow}\ {\isacharprime}a\ set} -\end{tabular} - -\section{List} - -\isa{\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ op\ {\isacharhash}\ {\isacharprime}a\ {\isacharparenleft}{\isacharprime}a\ list{\isacharparenright}} -\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{op\ {\isacharat}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{butlast} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{concat} & \isa{{\isacharprime}a\ list\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{distinct} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\ -\isa{drop} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{dropWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{filter} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{foldl} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{foldr} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}\\ -\isa{hd} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{last} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\isa{length} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat}\\ -\isa{lenlex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ -\isa{lex} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ -\isa{lexn} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ -\isa{lexord} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ -\isa{listrel} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ list\ {\isasymtimes}\ {\isacharprime}a\ list{\isacharparenright}\ set}\\ -\isa{lists} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\ -\isa{listset} & \isa{{\isacharprime}a\ set\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ set}\\ -\isa{listsum} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a}\\ -\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}\\ -\isa{list{\isacharunderscore}update} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{map} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list}\\ -\isa{measures} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ -\isa{remdups} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{removeAll} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{remove{\isadigit{1}}} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{replicate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{rev} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{rotate} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{rotate{\isadigit{1}}} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{set} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{sort} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{sorted} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ bool}\\ -\isa{splice} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{sublist} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{take} & \isa{nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{takeWhile} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{tl} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{upt} & \isa{nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ list}\\ -\isa{upto} & \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list}\\ -\isa{zip} & \isa{{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}b\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\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}}\\ -\isa{{\isacharbrackleft}m{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}} & \isa{{\isachardoublequote}upt\ m\ n{\isachardoublequote}}\\ -\isa{{\isacharbrackleft}i{\isachardot}{\isachardot}j{\isacharbrackright}} & \isa{{\isachardoublequote}upto\ i\ j{\isachardoublequote}}\\ -\isa{{\isacharbrackleft}e{\isachardot}\ x\ {\isasymleftarrow}\ xs{\isacharbrackright}} & \isa{map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs}\\ -\isa{{\isacharbrackleft}x{\isasymleftarrow}xs\ {\isachardot}\ b{\isacharbrackright}} & \isa{{\isachardoublequote}filter\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}\ xs{\isachardoublequote}} \\ -\isa{xs{\isacharbrackleft}n\ {\isacharcolon}{\isacharequal}\ x{\isacharbrackright}} & \isa{{\isachardoublequote}list{\isacharunderscore}update\ xs\ n\ x{\isachardoublequote}}\\ -\isa{{\isasymSum}x{\isasymleftarrow}xs{\isachardot}\ e} & \isa{{\isachardoublequote}listsum\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ e{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}}\\ -\end{supertabular} -\medskip - -List comprehension: \isa{{\isacharbrackleft}e{\isachardot}\ q\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ q\isactrlisub n{\isacharbrackright}} where each -qualifier \isa{q\isactrlisub i} is either a generator \mbox{\isa{pat\ {\isasymleftarrow}\ e}} or a -guard, i.e.\ boolean expression. - -\section{Map} - -Maps model partial functions and are often used as finite tables. However, -the domain of a map may be infinite. - -\isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b\ \ {\isacharequal}\ \ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ option} -\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{Map{\isachardot}empty} & \isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ -\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}\\ -\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}\\ -\isa{op\ {\isacharbar}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ -\isa{dom} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set}\\ -\isa{ran} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ -\isa{op\ {\isasymsubseteq}\isactrlsub m} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ bool}\\ -\isa{map{\isacharunderscore}of} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharprime}b}\\ -\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}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{Map{\isachardot}empty} & \isa{{\isasymlambda}x{\isachardot}\ None}\\ -\isa{m{\isacharparenleft}x\ {\isasymmapsto}\ y{\isacharparenright}} & \isa{{\isachardoublequote}m{\isacharparenleft}x{\isacharcolon}{\isacharequal}Some\ y{\isacharparenright}{\isachardoublequote}}\\ -\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}}\\ -\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}}\\ -\isa{m{\isacharparenleft}xs\ {\isacharbrackleft}{\isasymmapsto}{\isacharbrackright}\ ys{\isacharparenright}} & \isa{{\isachardoublequote}map{\isacharunderscore}upds\ m\ xs\ ys{\isachardoublequote}}\\ -\end{tabular}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: diff -r d21bc48823b7 -r 28b487cd9e15 doc-src/Main/Makefile --- a/doc-src/Main/Makefile Wed Mar 11 20:09:23 2009 +0100 +++ b/doc-src/Main/Makefile Wed Mar 11 20:11:06 2009 +0100 @@ -1,6 +1,3 @@ -# -# $Id$ -# ## targets @@ -11,12 +8,10 @@ include ../Makefile.in -SRC = ../../src/HOL/Docs/generated - NAME = main -FILES = $(NAME).tex Main_Doc.tex \ - isabelle.sty isabellesym.sty pdfsetup.sty +FILES = ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty $(NAME).tex \ + Docs/document/Main_Doc.tex dvi: $(NAME).dvi @@ -27,19 +22,3 @@ $(NAME).pdf: $(FILES) $(PDFLATEX) $(NAME) - $(FIXBOOKMARKS) $(NAME).out - $(PDFLATEX) $(NAME) - $(PDFLATEX) $(NAME) - -isabelle.sty: - ln ../isabelle.sty . - -isabellesym.sty: - ln ../isabellesym.sty . - -pdfsetup.sty: - ln ../pdfsetup.sty . - -copy: - cp $(SRC)/Main_Doc.tex Main_Doc.tex - cp $(SRC)/root.tex main.tex diff -r d21bc48823b7 -r 28b487cd9e15 doc-src/Main/main.tex --- a/doc-src/Main/main.tex Wed Mar 11 20:09:23 2009 +0100 +++ b/doc-src/Main/main.tex Wed Mar 11 20:11:06 2009 +0100 @@ -8,7 +8,7 @@ \headsep=0mm \textheight=234mm -\usepackage{isabelle,isabellesym} +\usepackage{../isabelle,../isabellesym} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed @@ -36,7 +36,7 @@ %for \, \ % this should be the last package used -\usepackage{pdfsetup} +\usepackage{../pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} @@ -56,7 +56,7 @@ \date{\today} \maketitle -\input{Main_Doc} +\input{Docs/document/Main_Doc.tex} % optional bibliography %\bibliographystyle{abbrv} diff -r d21bc48823b7 -r 28b487cd9e15 doc/Contents --- a/doc/Contents Wed Mar 11 20:09:23 2009 +0100 +++ b/doc/Contents Wed Mar 11 20:11:06 2009 +0100 @@ -8,6 +8,7 @@ sugar LaTeX sugar for proof documents Reference Manuals + main What's in Main isar-ref The Isabelle/Isar Reference Manual implementation The Isabelle/Isar Implementation Manual system The Isabelle System Manual diff -r d21bc48823b7 -r 28b487cd9e15 src/HOL/Docs/Main_Doc.thy --- a/src/HOL/Docs/Main_Doc.thy Wed Mar 11 20:09:23 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,572 +0,0 @@ -(*<*) -theory Main_Doc -imports Main -begin - -ML {* -fun pretty_term_type_only ctxt (t, T) = - (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then () - else error "term_type_only: type mismatch"; - Syntax.pretty_typ ctxt T) - -val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev) - (fn {source, context, ...} => fn arg => - ThyOutput.output - (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg])); -*} -(*>*) -text{* - -\begin{abstract} -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/}. -\end{abstract} - -\section{HOL} - -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"}. -\smallskip - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const HOL.undefined} & @{typeof HOL.undefined}\\ -@{const HOL.default} & @{typeof HOL.default}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -@{term"~(x = y)"} & @{term[source]"\ (x = y)"} & (\verb$~=$)\\ -@{term[source]"P \ Q"} & @{term"P \ Q"} \\ -@{term"If x y z"} & @{term[source]"If x y z"}\\ -@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\x. e\<^isub>2)"}\\ -\end{supertabular} - - -\section{Orderings} - -A collection of classes defining basic orderings: -preorder, partial order, linear order, dense linear order and wellorder. -\smallskip - -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} -@{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\ -@{const HOL.less} & @{typeof HOL.less}\\ -@{const Orderings.Least} & @{typeof Orderings.Least}\\ -@{const Orderings.min} & @{typeof Orderings.min}\\ -@{const Orderings.max} & @{typeof Orderings.max}\\ -@{const[source] top} & @{typeof Orderings.top}\\ -@{const[source] bot} & @{typeof Orderings.bot}\\ -@{const Orderings.mono} & @{typeof Orderings.mono}\\ -@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -@{term[source]"x \ y"} & @{term"x \ y"} & (\verb$>=$)\\ -@{term[source]"x > y"} & @{term"x > y"}\\ -@{term"ALL x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ -@{term"EX x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ -@{term"LEAST x. P"} & @{term[source]"Least (\x. P)"}\\ -\end{supertabular} - - -\section{Lattices} - -Classes semilattice, lattice, distributive lattice and complete lattice (the -latter in theory @{theory Set}). - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Lattices.inf} & @{typeof Lattices.inf}\\ -@{const Lattices.sup} & @{typeof Lattices.sup}\\ -@{const Set.Inf} & @{term_type_only Set.Inf "'a set \ 'a::complete_lattice"}\\ -@{const Set.Sup} & @{term_type_only Set.Sup "'a set \ 'a::complete_lattice"}\\ -\end{tabular} - -\subsubsection*{Syntax} - -Available by loading theory @{text Lattice_Syntax} in directory @{text -Library}. - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{text[source]"x \ y"} & @{term"x \ y"}\\ -@{text[source]"x \ y"} & @{term"x < y"}\\ -@{text[source]"x \ y"} & @{term"inf x y"}\\ -@{text[source]"x \ y"} & @{term"sup x y"}\\ -@{text[source]"\ A"} & @{term"Sup A"}\\ -@{text[source]"\ A"} & @{term"Inf A"}\\ -@{text[source]"\"} & @{term[source] top}\\ -@{text[source]"\"} & @{term[source] bot}\\ -\end{supertabular} - - -\section{Set} - -Sets are predicates: @{text[source]"'a set = 'a \ bool"} -\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} -@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ -@{const insert} & @{term_type_only insert "'a\'a set\'a set"}\\ -@{const Collect} & @{term_type_only Collect "('a\bool)\'a set"}\\ -@{const "op :"} & @{term_type_only "op :" "'a\'a set\bool"} & (\texttt{:})\\ -@{const Set.Un} & @{term_type_only Set.Un "'a set\'a set \ 'a set"} & (\texttt{Un})\\ -@{const Set.Int} & @{term_type_only Set.Int "'a set\'a set \ 'a set"} & (\texttt{Int})\\ -@{const UNION} & @{term_type_only UNION "'a set\('a \ 'b set) \ 'b set"}\\ -@{const INTER} & @{term_type_only INTER "'a set\('a \ 'b set) \ 'b set"}\\ -@{const Union} & @{term_type_only Union "'a set set\'a set"}\\ -@{const Inter} & @{term_type_only Inter "'a set set\'a set"}\\ -@{const Pow} & @{term_type_only Pow "'a set \'a set set"}\\ -@{const UNIV} & @{term_type_only UNIV "'a set"}\\ -@{const image} & @{term_type_only image "('a\'b)\'a set\'b set"}\\ -@{const Ball} & @{term_type_only Ball "'a set\('a\bool)\bool"}\\ -@{const Bex} & @{term_type_only Bex "'a set\('a\bool)\bool"}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -@{text"{x\<^isub>1,\,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\ (insert x\<^isub>n {})\)"}\\ -@{term"x ~: A"} & @{term[source]"\(x \ A)"}\\ -@{term"A \ B"} & @{term[source]"A \ B"}\\ -@{term"A \ B"} & @{term[source]"A < B"}\\ -@{term[source]"A \ B"} & @{term[source]"B \ A"}\\ -@{term[source]"A \ B"} & @{term[source]"B < A"}\\ -@{term"{x. P}"} & @{term[source]"Collect (\x. P)"}\\ -@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\x. A)"} & (\texttt{UN})\\ -@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ -@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\x. A)"} & (\texttt{INT})\\ -@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\x. A)"}\\ -@{term"ALL x:A. P"} & @{term[source]"Ball A (\x. P)"}\\ -@{term"EX x:A. P"} & @{term[source]"Bex A (\x. P)"}\\ -@{term"range f"} & @{term[source]"f ` UNIV"}\\ -\end{supertabular} - - -\section{Fun} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const "Fun.id"} & @{typeof Fun.id}\\ -@{const "Fun.comp"} & @{typeof Fun.comp}\\ -@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\'b)\'a set\bool"}\\ -@{const "Fun.inj"} & @{typeof Fun.inj}\\ -@{const "Fun.surj"} & @{typeof Fun.surj}\\ -@{const "Fun.bij"} & @{typeof Fun.bij}\\ -@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\'b)\'a set\'b set\bool"}\\ -@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ -@{text"f(x\<^isub>1:=y\<^isub>1,\,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\(x\<^isub>n:=y\<^isub>n)"}\\ -\end{tabular} - - -\section{Fixed Points} - -Theory: @{theory Inductive}. - -Least and greatest fixed points in a complete lattice @{typ 'a}: - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ -@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ -\end{tabular} - -Note that in particular sets (@{typ"'a \ bool"}) are complete lattices. - -\section{Sum\_Type} - -Type constructor @{text"+"}. - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ -@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ -@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\'b set\('a+'b)set"} -\end{tabular} - - -\section{Product\_Type} - -Types @{typ unit} and @{text"\"}. - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ -@{const Pair} & @{typeof Pair}\\ -@{const fst} & @{typeof fst}\\ -@{const snd} & @{typeof snd}\\ -@{const split} & @{typeof split}\\ -@{const curry} & @{typeof curry}\\ -@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\('a\'b set)\('a*'b)set"}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} -@{term"Pair a b"} & @{term[source]"Pair a b"}\\ -@{term"split (\x y. t)"} & @{term[source]"split (\x y. t)"}\\ -@{term"A <*> B"} & @{text"Sigma A (\\<^raw:\_>. B)"} & (\verb$<*>$) -\end{tabular} - -Pairs may be nested. Nesting to the right is printed as a tuple, -e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{@{text"(a, (b, c))"}.} -Pattern matching with pairs and tuples extends to all binders, -e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc. - - -\section{Relation} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \ ('b*'a)set"}\\ -@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\('c*'a)set\('c*'b)set"}\\ -@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\'a set\'b set"}\\ -@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\('b\'a)\('b*'b)set"}\\ -@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\('a*'a)set"}\\ -@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\ -@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\'a set"}\\ -@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\'b set"}\\ -@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\'a set"}\\ -@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\('a*'a)set\bool"}\\ -@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\bool"}\\ -@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\bool"}\\ -@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\bool"}\\ -@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\bool"}\\ -@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\bool"}\\ -@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\('a*'a)set\bool"}\\ -@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\bool"}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -@{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$) -\end{tabular} - -\section{Equiv\_Relations} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \ ('a*'a)set\bool"}\\ -@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \ ('a \ 'a) set \ 'a set set"}\\ -@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\('a\'b)\bool"}\\ -@{const Equiv_Relations.congruent2} & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\('b*'b)set\('a\'b\'c)\bool"}\\ -%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"congruent r f"} & @{term[source]"congruent r f"}\\ -@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\ -\end{tabular} - - -\section{Transitive\_Closure} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\('a*'a)set"}\\ -@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\('a*'a)set"}\\ -@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\('a*'a)set"}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\verb$^*$)\\ -@{term"trancl r"} & @{term[source]"trancl r"} & (\verb$^+$)\\ -@{term"reflcl r"} & @{term[source]"reflcl r"} & (\verb$^=$) -\end{tabular} - - -\section{Algebra} - -Theories @{theory OrderedGroup}, @{theory Ring_and_Field} and @{theory -Divides} define a large collection of classes describing common algebraic -structures from semigroups up to fields. Everything is done in terms of -overloaded operators: - -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} -@{text "0"} & @{typeof zero}\\ -@{text "1"} & @{typeof one}\\ -@{const plus} & @{typeof plus}\\ -@{const minus} & @{typeof minus}\\ -@{const uminus} & @{typeof uminus} & (\verb$-$)\\ -@{const times} & @{typeof times}\\ -@{const inverse} & @{typeof inverse}\\ -@{const divide} & @{typeof divide}\\ -@{const abs} & @{typeof abs}\\ -@{const sgn} & @{typeof sgn}\\ -@{const dvd_class.dvd} & @{typeof "dvd_class.dvd"}\\ -@{const div_class.div} & @{typeof "div_class.div"}\\ -@{const div_class.mod} & @{typeof "div_class.mod"}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"abs x"} & @{term[source]"abs x"} -\end{tabular} - - -\section{Nat} - -@{datatype nat} -\bigskip - -\begin{tabular}{@ {} lllllll @ {}} -@{term "op + :: nat \ nat \ nat"} & -@{term "op - :: nat \ nat \ nat"} & -@{term "op * :: nat \ nat \ nat"} & -@{term "op ^ :: nat \ nat \ nat"} & -@{term "op div :: nat \ nat \ nat"}& -@{term "op mod :: nat \ nat \ nat"}& -@{term "op dvd :: nat \ nat \ bool"}\\ -@{term "op \ :: nat \ nat \ bool"} & -@{term "op < :: nat \ nat \ bool"} & -@{term "min :: nat \ nat \ nat"} & -@{term "max :: nat \ nat \ nat"} & -@{term "Min :: nat set \ nat"} & -@{term "Max :: nat set \ nat"}\\ -\end{tabular} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Nat.of_nat} & @{typeof Nat.of_nat} -\end{tabular} - -\section{Int} - -Type @{typ int} -\bigskip - -\begin{tabular}{@ {} llllllll @ {}} -@{term "op + :: int \ int \ int"} & -@{term "op - :: int \ int \ int"} & -@{term "uminus :: int \ int"} & -@{term "op * :: int \ int \ int"} & -@{term "op ^ :: int \ nat \ int"} & -@{term "op div :: int \ int \ int"}& -@{term "op mod :: int \ int \ int"}& -@{term "op dvd :: int \ int \ bool"}\\ -@{term "op \ :: int \ int \ bool"} & -@{term "op < :: int \ int \ bool"} & -@{term "min :: int \ int \ int"} & -@{term "max :: int \ int \ int"} & -@{term "Min :: int set \ int"} & -@{term "Max :: int set \ int"}\\ -@{term "abs :: int \ int"} & -@{term "sgn :: int \ int"}\\ -\end{tabular} - -\begin{tabular}{@ {} l @ {~::~} l l @ {}} -@{const Int.nat} & @{typeof Int.nat}\\ -@{const Int.of_int} & @{typeof Int.of_int}\\ -@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\verb$Ints$) -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"of_nat::nat\int"} & @{term[source]"of_nat"}\\ -\end{tabular} - - -\section{Finite\_Set} - - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\bool"}\\ -@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\ -@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b"}\\ -@{const Finite_Set.fold_image} & @{typ "('b \ 'b \ 'b) \ ('a \ 'b) \ 'b \ 'a set \ 'b"}\\ -@{const Finite_Set.setsum} & @{term_type_only Finite_Set.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\ -@{const Finite_Set.setprod} & @{term_type_only Finite_Set.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\ -\end{supertabular} - - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -@{term"setsum (%x. x) A"} & @{term[source]"setsum (\x. x) A"} & (\verb$SUM$)\\ -@{term"setsum (%x. t) A"} & @{term[source]"setsum (\x. t) A"}\\ -@{term[source]"\x|P. t"} & @{term"\x|P. t"}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\"} instead of @{text"\"}} & (\verb$PROD$)\\ -\end{supertabular} - - -\section{Wellfounded} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\bool"}\\ -@{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\bool"}\\ -@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\'a set"}\\ -@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\nat)\('a*'a)set"}\\ -@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\('b*'b)set\(('a*'b)*('a*'b))set"}\\ -@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\nat)\('a*'a)set\('a*'a)set"}\\ -@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ -@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ -\end{supertabular} - - -\section{SetInterval} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const lessThan} & @{term_type_only lessThan "'a::ord \ 'a set"}\\ -@{const atMost} & @{term_type_only atMost "'a::ord \ 'a set"}\\ -@{const greaterThan} & @{term_type_only greaterThan "'a::ord \ 'a set"}\\ -@{const atLeast} & @{term_type_only atLeast "'a::ord \ 'a set"}\\ -@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \ 'a \ 'a set"}\\ -@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \ 'a \ 'a set"}\\ -@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \ 'a \ 'a set"}\\ -@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \ 'a \ 'a set"}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term "lessThan y"} & @{term[source] "lessThan y"}\\ -@{term "atMost y"} & @{term[source] "atMost y"}\\ -@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\ -@{term "atLeast x"} & @{term[source] "atLeast x"}\\ -@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\ -@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\ -@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\ -@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\ -@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\ i \ {..n}. A"}\\ -@{term[mode=xsymbols] "UN i:{.. i \ {.."} instead of @{text"\"}}\\ -@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\x. t) {a..b}"}\\ -@{term "setsum (%x. t) {a..x. t) {a..x. t) {..b}"}\\ -@{term "setsum (%x. t) {..x. t) {.."} instead of @{text"\"}}\\ -\end{supertabular} - - -\section{Power} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Power.power} & @{typeof Power.power} -\end{tabular} - - -\section{Iterated Functions and Relations} - -Theory: @{theory Relation_Power} - -Iterated functions \ @{term[source]"(f::'a\'a) ^ n"} \ -and relations \ @{term[source]"(r::('a\'a)set) ^ n"}. - - -\section{Option} - -@{datatype option} -\bigskip - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Option.the} & @{typeof Option.the}\\ -@{const Option.map} & @{typ[source]"('a \ 'b) \ 'a option \ 'b option"}\\ -@{const Option.set} & @{term_type_only Option.set "'a option \ 'a set"} -\end{tabular} - -\section{List} - -@{datatype list} -\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const List.append} & @{typeof List.append}\\ -@{const List.butlast} & @{typeof List.butlast}\\ -@{const List.concat} & @{typeof List.concat}\\ -@{const List.distinct} & @{typeof List.distinct}\\ -@{const List.drop} & @{typeof List.drop}\\ -@{const List.dropWhile} & @{typeof List.dropWhile}\\ -@{const List.filter} & @{typeof List.filter}\\ -@{const List.foldl} & @{typeof List.foldl}\\ -@{const List.foldr} & @{typeof List.foldr}\\ -@{const List.hd} & @{typeof List.hd}\\ -@{const List.last} & @{typeof List.last}\\ -@{const List.length} & @{typeof List.length}\\ -@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\('a list * 'a list)set"}\\ -@{const List.lex} & @{term_type_only List.lex "('a*'a)set\('a list * 'a list)set"}\\ -@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\nat\('a list * 'a list)set"}\\ -@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\('a list * 'a list)set"}\\ -@{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\('a list * 'a list)set"}\\ -@{const List.lists} & @{term_type_only List.lists "'a set\'a list set"}\\ -@{const List.listset} & @{term_type_only List.listset "'a set list \ 'a list set"}\\ -@{const List.listsum} & @{typeof List.listsum}\\ -@{const List.list_all2} & @{typeof List.list_all2}\\ -@{const List.list_update} & @{typeof List.list_update}\\ -@{const List.map} & @{typeof List.map}\\ -@{const List.measures} & @{term_type_only List.measures "('a\nat)list\('a*'a)set"}\\ -@{const List.remdups} & @{typeof List.remdups}\\ -@{const List.removeAll} & @{typeof List.removeAll}\\ -@{const List.remove1} & @{typeof List.remove1}\\ -@{const List.replicate} & @{typeof List.replicate}\\ -@{const List.rev} & @{typeof List.rev}\\ -@{const List.rotate} & @{typeof List.rotate}\\ -@{const List.rotate1} & @{typeof List.rotate1}\\ -@{const List.set} & @{term_type_only List.set "'a list \ 'a set"}\\ -@{const List.sort} & @{typeof List.sort}\\ -@{const List.sorted} & @{typeof List.sorted}\\ -@{const List.splice} & @{typeof List.splice}\\ -@{const List.sublist} & @{typeof List.sublist}\\ -@{const List.take} & @{typeof List.take}\\ -@{const List.takeWhile} & @{typeof List.takeWhile}\\ -@{const List.tl} & @{typeof List.tl}\\ -@{const List.upt} & @{typeof List.upt}\\ -@{const List.upto} & @{typeof List.upto}\\ -@{const List.zip} & @{typeof List.zip}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{text"[x\<^isub>1,\,x\<^isub>n]"} & @{text"x\<^isub>1 # \ # x\<^isub>n # []"}\\ -@{term"[m.. xs]"} & @{term"map (%x. e) xs"}\\ -@{term"[x \ xs. b]"} & @{term[source]"filter (\x. b) xs"} \\ -@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ -@{term"\x\xs. e"} & @{term[source]"listsum (map (\x. e) xs)"}\\ -\end{supertabular} -\medskip - -List comprehension: @{text"[e. q\<^isub>1, \, q\<^isub>n]"} where each -qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \ e"}} or a -guard, i.e.\ boolean expression. - -\section{Map} - -Maps model partial functions and are often used as finite tables. However, -the domain of a map may be infinite. - -@{text"'a \ 'b = 'a \ 'b option"} -\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const Map.empty} & @{typeof Map.empty}\\ -@{const Map.map_add} & @{typeof Map.map_add}\\ -@{const Map.map_comp} & @{typeof Map.map_comp}\\ -@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\'b option)\'a set\('a\'b option)"}\\ -@{const Map.dom} & @{term_type_only Map.dom "('a\'b option)\'a set"}\\ -@{const Map.ran} & @{term_type_only Map.ran "('a\'b option)\'b set"}\\ -@{const Map.map_le} & @{typeof Map.map_le}\\ -@{const Map.map_of} & @{typeof Map.map_of}\\ -@{const Map.map_upds} & @{typeof Map.map_upds}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"Map.empty"} & @{term"\x. None"}\\ -@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ -@{text"m(x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n)"} & @{text[source]"m(x\<^isub>1\y\<^isub>1)\(x\<^isub>n\y\<^isub>n)"}\\ -@{text"[x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n]"} & @{text[source]"Map.empty(x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n)"}\\ -@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ -\end{tabular} - -*} -(*<*) -end -(*>*) \ No newline at end of file diff -r d21bc48823b7 -r 28b487cd9e15 src/HOL/Docs/ROOT.ML --- a/src/HOL/Docs/ROOT.ML Wed Mar 11 20:09:23 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thy "Main_Doc"; diff -r d21bc48823b7 -r 28b487cd9e15 src/HOL/Docs/document/root.tex --- a/src/HOL/Docs/document/root.tex Wed Mar 11 20:09:23 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,65 +0,0 @@ -\documentclass[12pt,a4paper]{article} - -\oddsidemargin=4.6mm -\evensidemargin=4.6mm -\textwidth=150mm -\topmargin=4.6mm -\headheight=0mm -\headsep=0mm -\textheight=234mm - -\usepackage{isabelle,isabellesym} - -% further packages required for unusual symbols (see also -% isabellesym.sty), use only when needed - -\usepackage{amssymb} - %for \, \, \, \, \, \, - %\, \, \, \, \, - %\, \, \ - -%\usepackage[greek,english]{babel} - %option greek for \ - %option english (default language) for \, \ - -%\usepackage[latin1]{inputenc} - %for \, \, \, \, - %\, \, \ - -\usepackage[only,bigsqcap]{stmaryrd} - %for \ - -%\usepackage{eufrak} - %for \ ... \, \ ... \ (also included in amssymb) - -%\usepackage{textcomp} - %for \, \ - -% this should be the last package used -\usepackage{pdfsetup} - -% urls in roman style, theory text in math-similar italics -\urlstyle{rm} -\isabellestyle{it} - -% for uniform font size -\renewcommand{\isastyle}{\isastyleminor} - -\parindent 0pt\parskip 0.5ex - -\usepackage{supertabular} - -\begin{document} - -\title{What's in Main} -\author{Tobias Nipkow} -\date{\today} -\maketitle - -\input{Main_Doc} - -% optional bibliography -%\bibliographystyle{abbrv} -%\bibliography{root} - -\end{document} diff -r d21bc48823b7 -r 28b487cd9e15 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Mar 11 20:09:23 2009 +0100 +++ b/src/HOL/IsaMakefile Wed Mar 11 20:11:06 2009 +0100 @@ -15,7 +15,6 @@ HOL-Auth \ HOL-Bali \ HOL-Decision_Procs \ - HOL-Docs \ HOL-Extraction \ HOL-HahnBanach \ HOL-Hoare \