# HG changeset patch # User wenzelm # Date 1346095818 -7200 # Node ID ac15a85e92824b9f0eafcec183f8842af40838ef # Parent 54da920baf383d273c4764c3f849b8cc0c835e3a more standard document preparation within session context; diff -r 54da920baf38 -r ac15a85e9282 doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Mon Aug 27 21:19:16 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,596 +0,0 @@ -(*<*) -theory Main_Doc -imports Main -begin - -setup {* - let - fun pretty_term_type_only ctxt (t, T) = - (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () - else error "term_type_only: type mismatch"; - Syntax.pretty_typ ctxt T) - in - Thy_Output.antiquotation @{binding term_type_only} - (Args.term -- Args.typ_abbrev) - (fn {source, context = ctxt, ...} => fn arg => - Thy_Output.output ctxt - (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg])) - end -*} -setup {* - Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single) - (fn {source, context, ...} => Thy_Output.output context o - Thy_Output.maybe_pretty_source Syntax.pretty_typ context source) -*} -(*>*) -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/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 Orderings.less_eq} & @{typeof Orderings.less_eq} & (\verb$<=$)\\ -@{const Orderings.less} & @{typeof Orderings.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 Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \ 'a::Inf"}\\ -@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \ 'a::Sup"}\\ -\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 Set.insert} & @{term_type_only insert "'a\'a set\'a set"}\\ -@{const Collect} & @{term_type_only Collect "('a\bool)\'a set"}\\ -@{const Set.member} & @{term_type_only Set.member "'a\'a set\bool"} & (\texttt{:})\\ -@{const Set.union} & @{term_type_only Set.union "'a set\'a set \ 'a set"} & (\texttt{Un})\\ -@{const Set.inter} & @{term_type_only Set.inter "'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 l @ {}} -@{const "Fun.id"} & @{typeof Fun.id}\\ -@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\ -@{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{Hilbert\_Choice} - -Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}. -\smallskip - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \ ('a \ 'b) \ ('b \ 'a)"} -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term inv} & @{term[source]"inv_into UNIV"} -\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{tabular}{@ {} l @ {~::~} l @ {}} -@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \ ('b*'a)set"}\\ -@{const Relation.relcomp} & @{term_type_only Relation.relcomp "('a*'b)set\('b*'c)set\('a*'c)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{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -@{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$) -\end{tabular} -\medskip - -\noindent -Type synonym \ @{typ"'a rel"} @{text"="} @{expanded_typ "'a rel"} - -\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"}\\ -@{const Transitive_Closure.acyclic} & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\bool"}\\ -@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\nat\('a*'a)set" "('a*'a)set\nat\('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 Groups}, @{theory Rings}, @{theory Fields} 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}\\ -@{term "op ^^ :: ('a \ 'a) \ nat \ 'a \ 'a"} & - @{term_type_only "op ^^ :: ('a \ 'a) \ nat \ 'a \ 'a" "('a \ 'a) \ nat \ 'a \ 'a"} -\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 Big_Operators.setsum} & @{term_type_only Big_Operators.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\ -@{const Big_Operators.setprod} & @{term_type_only Big_Operators.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.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{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"}\\ -@{const Option.bind} & @{term_type_only Option.bind "'a option \ ('a \ 'b option) \ 'b option"} -\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.find} & @{typeof List.find}\\ -@{const List.fold} & @{typeof List.fold}\\ -@{const List.foldr} & @{typeof List.foldr}\\ -@{const List.foldl} & @{typeof List.foldl}\\ -@{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*'b)set\('a list * 'b list)set"}\\ -@{const List.listrel1} & @{term_type_only List.listrel1 "('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.nth} & @{typeof List.nth}\\ -@{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. - -\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 54da920baf38 -r ac15a85e9282 doc-src/Main/Docs/document/Main_Doc.tex --- a/doc-src/Main/Docs/document/Main_Doc.tex Mon Aug 27 21:19:16 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,613 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{Main{\isaliteral{5F}{\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/library/HOL/}. -\end{abstract} - -\section{HOL} - -The basic logic: \isa{x\ {\isaliteral{3D}{\isacharequal}}\ y}, \isa{True}, \isa{False}, \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P}, \isa{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}, \isa{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}, \isa{P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q}, \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P}, \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P}, \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{21}{\isacharbang}}x{\isaliteral{2E}{\isachardot}}\ P}, \isa{THE\ x{\isaliteral{2E}{\isachardot}}\ P}. -\smallskip - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{undefined} & \isa{{\isaliteral{27}{\isacharprime}}a}\\ -\isa{default} & \isa{{\isaliteral{27}{\isacharprime}}a}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & (\verb$~=$)\\ -\isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}} & \isa{P\ {\isaliteral{3D}{\isacharequal}}\ Q} \\ -\isa{if\ x\ then\ y\ else\ z} & \isa{{\isaliteral{22}{\isachardoublequote}}If\ x\ y\ z{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{let\ x\ {\isaliteral{3D}{\isacharequal}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ in\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} & \isa{{\isaliteral{22}{\isachardoublequote}}Let\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\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\ {\isaliteral{5C3C6C653E}{\isasymle}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} & (\verb$<=$)\\ -\isa{op\ {\isaliteral{3C}{\isacharless}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{Least} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{min} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{max} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{top} & \isa{{\isaliteral{27}{\isacharprime}}a}\\ -\isa{bot} & \isa{{\isaliteral{27}{\isacharprime}}a}\\ -\isa{mono} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{strict{\isaliteral{5F}{\isacharunderscore}}mono} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C67653E}{\isasymge}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{y\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x} & (\verb$>=$)\\ -\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3E}{\isachargreater}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{y\ {\isaliteral{3C}{\isacharless}}\ x}\\ -\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C6C653E}{\isasymle}}y{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{5C3C6C653E}{\isasymle}}y{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ P{\isaliteral{22}{\isachardoublequote}}}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ -\isa{LEAST\ x{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}Least\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\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{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{sup} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{Inf} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{Sup} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\end{tabular} - -\subsubsection*{Syntax} - -Available by loading theory \isa{Lattice{\isaliteral{5F}{\isacharunderscore}}Syntax} in directory \isa{Library}. - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C73717375627365743E}{\isasymsqsubset}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{x\ {\isaliteral{3C}{\isacharless}}\ y}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C7371696E7465723E}{\isasymsqinter}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{inf\ x\ y}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C7371756E696F6E3E}{\isasymsqunion}}\ y{\isaliteral{22}{\isachardoublequote}}} & \isa{sup\ x\ y}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C5371696E7465723E}{\isasymSqinter}}\ A{\isaliteral{22}{\isachardoublequote}}} & \isa{Sup\ A}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C5371756E696F6E3E}{\isasymSqunion}}\ A{\isaliteral{22}{\isachardoublequote}}} & \isa{Inf\ A}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C746F703E}{\isasymtop}}{\isaliteral{22}{\isachardoublequote}}} & \isa{top}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626F74746F6D3E}{\isasymbottom}}{\isaliteral{22}{\isachardoublequote}}} & \isa{bot}\\ -\end{supertabular} - - -\section{Set} - -%Sets are predicates: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ set\ \ {\isaliteral{3D}{\isacharequal}}\ \ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequote}}} -%\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} -\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{insert} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{Collect} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{op\ {\isaliteral{5C3C696E3E}{\isasymin}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} & (\texttt{:})\\ -\isa{op\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set} & (\texttt{Un})\\ -\isa{op\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set} & (\texttt{Int})\\ -\isa{UNION} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\ -\isa{INTER} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\ -\isa{Union} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{Inter} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{Pow} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ set}\\ -\isa{UNIV} & \isa{{\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{op\ {\isaliteral{60}{\isacharbackquote}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\ -\isa{Ball} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{Bex} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{{\isaliteral{7B}{\isacharbraceleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}} & \isa{insert\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{28}{\isacharparenleft}}insert\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}}\\ -\isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B} & \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{A\ {\isaliteral{5C3C7375627365743E}{\isasymsubset}}\ B} & \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3C}{\isacharless}}\ B{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ B{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}B\ {\isaliteral{5C3C6C653E}{\isasymle}}\ A{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C7375707365743E}{\isasymsupset}}\ B{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}B\ {\isaliteral{3C}{\isacharless}}\ A{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}Collect\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}x{\isaliteral{5C3C696E3E}{\isasymin}}I{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}UNION\ I\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & (\texttt{UN})\\ -\isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}x{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}UNION\ UNIV\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C496E7465723E}{\isasymInter}}x{\isaliteral{5C3C696E3E}{\isasymin}}I{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}INTER\ I\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & (\texttt{INT})\\ -\isa{{\isaliteral{5C3C496E7465723E}{\isasymInter}}x{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}INTER\ UNIV\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}Ball\ A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P} & \isa{{\isaliteral{22}{\isachardoublequote}}Bex\ A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{range\ f} & \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{60}{\isacharbackquote}}\ UNIV{\isaliteral{22}{\isachardoublequote}}}\\ -\end{supertabular} - - -\section{Fun} - -\begin{supertabular}{@ {} l @ {~::~} l l @ {}} -\isa{id} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{op\ {\isaliteral{5C3C636972633E}{\isasymcirc}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}c\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b} & (\texttt{o})\\ -\isa{inj{\isaliteral{5F}{\isacharunderscore}}on} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{inj} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{surj} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{bij} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{bij{\isaliteral{5F}{\isacharunderscore}}betw} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{fun{\isaliteral{5F}{\isacharunderscore}}upd} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{f{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}fun{\isaliteral{5F}{\isacharunderscore}}upd\ f\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{f{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} & \isa{f{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}}\\ -\end{tabular} - - -\section{Hilbert\_Choice} - -Hilbert's selection ($\varepsilon$) operator: \isa{SOME\ x{\isaliteral{2E}{\isachardot}}\ P}. -\smallskip - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{inv{\isaliteral{5F}{\isacharunderscore}}into} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a} -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{inv} & \isa{{\isaliteral{22}{\isachardoublequote}}inv{\isaliteral{5F}{\isacharunderscore}}into\ UNIV{\isaliteral{22}{\isachardoublequote}}} -\end{tabular} - -\section{Fixed Points} - -Theory: \isa{Inductive}. - -Least and greatest fixed points in a complete lattice \isa{{\isaliteral{27}{\isacharprime}}a}: - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{lfp} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{gfp} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\end{tabular} - -Note that in particular sets (\isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}) are complete lattices. - -\section{Sum\_Type} - -Type constructor \isa{{\isaliteral{2B}{\isacharplus}}}. - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{Inl} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\isa{Inr} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{3E}{\isachargreater}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set} -\end{tabular} - - -\section{Product\_Type} - -Types \isa{unit} and \isa{{\isaliteral{5C3C74696D65733E}{\isasymtimes}}}. - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}} & \isa{unit}\\ -\isa{Pair} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\isa{fst} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{snd} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\isa{split} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c}\\ -\isa{curry} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c}\\ -\isa{Sigma} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} -\isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}Pair\ a\ b{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}split\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{A\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ B} & \isa{Sigma\ A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\_{\isaliteral{2E}{\isachardot}}\ B{\isaliteral{29}{\isacharparenright}}} & (\verb$<*>$) -\end{tabular} - -Pairs may be nested. Nesting to the right is printed as a tuple, -e.g.\ \mbox{\isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{29}{\isacharparenright}}}} is really \mbox{\isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.} -Pattern matching with pairs and tuples extends to all binders, -e.g.\ \mbox{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P},} \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}}, etc. - - -\section{Relation} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{converse} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{op\ O} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{op\ {\isaliteral{60}{\isacharbackquote}}{\isaliteral{60}{\isacharbackquote}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\ -\isa{inv{\isaliteral{5F}{\isacharunderscore}}image} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{Id{\isaliteral{5F}{\isacharunderscore}}on} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{Id} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{Domain} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{Range} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\ -\isa{Field} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{refl{\isaliteral{5F}{\isacharunderscore}}on} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{refl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{sym} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{antisym} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{trans} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{irrefl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{total{\isaliteral{5F}{\isacharunderscore}}on} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{total} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{r{\isaliteral{5C3C696E76657273653E}{\isasyminverse}}} & \isa{{\isaliteral{22}{\isachardoublequote}}converse\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^-1$) -\end{tabular} -\medskip - -\noindent -Type synonym \ \isa{{\isaliteral{27}{\isacharprime}}a\ rel} \isa{{\isaliteral{3D}{\isacharequal}}} \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set} - -\section{Equiv\_Relations} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{equiv} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{op\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2F}{\isacharslash}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ set}\\ -\isa{congruent} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{congruent{\isadigit{2}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\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{{\isaliteral{22}{\isachardoublequote}}congruent\ r\ f{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{f\ respects{\isadigit{2}}\ r} & \isa{{\isaliteral{22}{\isachardoublequote}}congruent{\isadigit{2}}\ r\ r\ f{\isaliteral{22}{\isachardoublequote}}}\\ -\end{tabular} - - -\section{Transitive\_Closure} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{rtrancl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{trancl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{reflcl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{acyclic} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{op\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} & \isa{{\isaliteral{22}{\isachardoublequote}}rtrancl\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^*$)\\ -\isa{r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2B}{\isacharplus}}} & \isa{{\isaliteral{22}{\isachardoublequote}}trancl\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^+$)\\ -\isa{r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{3D}{\isacharequal}}} & \isa{{\isaliteral{22}{\isachardoublequote}}reflcl\ r{\isaliteral{22}{\isachardoublequote}}} & (\verb$^=$) -\end{tabular} - - -\section{Algebra} - -Theories \isa{Groups}, \isa{Rings}, \isa{Fields} 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{{\isaliteral{27}{\isacharprime}}a}\\ -\isa{{\isadigit{1}}} & \isa{{\isaliteral{27}{\isacharprime}}a}\\ -\isa{op\ {\isaliteral{2B}{\isacharplus}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{op\ {\isaliteral{2D}{\isacharminus}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{uminus} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a} & (\verb$-$)\\ -\isa{op\ {\isaliteral{2A}{\isacharasterisk}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{inverse} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{op\ {\isaliteral{2F}{\isacharslash}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{abs} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{sgn} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{op\ dvd} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{op\ div} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{op\ mod} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{{\isaliteral{5C3C6261723E}{\isasymbar}}x{\isaliteral{5C3C6261723E}{\isasymbar}}} & \isa{{\isaliteral{22}{\isachardoublequote}}abs\ x{\isaliteral{22}{\isachardoublequote}}} -\end{tabular} - - -\section{Nat} - -\isa{\isacommand{datatype}\ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ Suc\ nat} -\bigskip - -\begin{tabular}{@ {} lllllll @ {}} -\isa{op\ {\isaliteral{2B}{\isacharplus}}} & -\isa{op\ {\isaliteral{2D}{\isacharminus}}} & -\isa{op\ {\isaliteral{2A}{\isacharasterisk}}} & -\isa{op\ {\isaliteral{5E}{\isacharcircum}}} & -\isa{op\ div}& -\isa{op\ mod}& -\isa{op\ dvd}\\ -\isa{op\ {\isaliteral{5C3C6C653E}{\isasymle}}} & -\isa{op\ {\isaliteral{3C}{\isacharless}}} & -\isa{min} & -\isa{max} & -\isa{Min} & -\isa{Max}\\ -\end{tabular} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{of{\isaliteral{5F}{\isacharunderscore}}nat} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{op\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}} & - \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a} -\end{tabular} - -\section{Int} - -Type \isa{int} -\bigskip - -\begin{tabular}{@ {} llllllll @ {}} -\isa{op\ {\isaliteral{2B}{\isacharplus}}} & -\isa{op\ {\isaliteral{2D}{\isacharminus}}} & -\isa{uminus} & -\isa{op\ {\isaliteral{2A}{\isacharasterisk}}} & -\isa{op\ {\isaliteral{5E}{\isacharcircum}}} & -\isa{op\ div}& -\isa{op\ mod}& -\isa{op\ dvd}\\ -\isa{op\ {\isaliteral{5C3C6C653E}{\isasymle}}} & -\isa{op\ {\isaliteral{3C}{\isacharless}}} & -\isa{min} & -\isa{max} & -\isa{Min} & -\isa{Max}\\ -\isa{abs} & -\isa{sgn}\\ -\end{tabular} - -\begin{tabular}{@ {} l @ {~::~} l l @ {}} -\isa{nat} & \isa{int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat}\\ -\isa{of{\isaliteral{5F}{\isacharunderscore}}int} & \isa{int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{{\isaliteral{5C3C696E743E}{\isasymint}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ set} & (\verb$Ints$) -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{int} & \isa{{\isaliteral{22}{\isachardoublequote}}of{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{22}{\isachardoublequote}}}\\ -\end{tabular} - - -\section{Finite\_Set} - - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{finite} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{card} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat}\\ -\isa{Finite{\isaliteral{5F}{\isacharunderscore}}Set{\isaliteral{2E}{\isachardot}}fold} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\isa{fold{\isaliteral{5F}{\isacharunderscore}}image} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\isa{setsum} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\isa{setprod} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\end{supertabular} - - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}A} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{29}{\isacharparenright}}\ A{\isaliteral{22}{\isachardoublequote}}} & (\verb$SUM$)\\ -\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ A{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{7C}{\isacharbar}}P{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x\ {\isaliteral{7C}{\isacharbar}}\ P{\isaliteral{2E}{\isachardot}}\ t}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isaliteral{5C3C50726F643E}{\isasymProd}}} instead of \isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}}} & (\verb$PROD$)\\ -\end{supertabular} - - -\section{Wellfounded} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{wf} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{acc} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{measure} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{2A}{\isacharasterisk}}lex{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3E}{\isachargreater}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{2A}{\isacharasterisk}}mlex{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3E}{\isachargreater}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{less{\isaliteral{5F}{\isacharunderscore}}than} & \isa{{\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ nat{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{pred{\isaliteral{5F}{\isacharunderscore}}nat} & \isa{{\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ nat{\isaliteral{29}{\isacharparenright}}\ set}\\ -\end{supertabular} - - -\section{SetInterval} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{lessThan} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{atMost} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{greaterThan} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{atLeast} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{greaterThanLessThan} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{atLeastLessThan} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{greaterThanAtMost} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{atLeastAtMost} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}lessThan\ y{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}atMost\ y{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{3C}{\isacharless}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}greaterThan\ x{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}atLeast\ x{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{3C}{\isacharless}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}greaterThanLessThan\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}atLeastLessThan\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{3C}{\isacharless}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}greaterThanAtMost\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}y{\isaliteral{7D}{\isacharbraceright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}atLeastAtMost\ x\ y{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}\ i{\isaliteral{5C3C6C653E}{\isasymle}}n{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}\ i{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}\ i\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}n{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2E}{\isachardot}}\ A{\isaliteral{22}{\isachardoublequote}}}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isaliteral{5C3C496E7465723E}{\isasymInter}}} instead of \isa{{\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}}}\\ -\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}b{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}b{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}b{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}b{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{5C3C6C653E}{\isasymle}}b{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}b{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{3C}{\isacharless}}b{\isaliteral{2E}{\isachardot}}\ t} & \isa{{\isaliteral{22}{\isachardoublequote}}setsum\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}b{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isaliteral{5C3C50726F643E}{\isasymProd}}} instead of \isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}}}\\ -\end{supertabular} - - -\section{Power} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{op\ {\isaliteral{5E}{\isacharcircum}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a} -\end{tabular} - - -\section{Option} - -\isa{\isacommand{datatype}\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{3D}{\isacharequal}}\ None\ {\isaliteral{7C}{\isacharbar}}\ Some\ {\isaliteral{27}{\isacharprime}}a} -\bigskip - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -\isa{the} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{Option{\isaliteral{2E}{\isachardot}}map} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{Option{\isaliteral{2E}{\isachardot}}set} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{Option{\isaliteral{2E}{\isachardot}}bind} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option} -\end{tabular} - -\section{List} - -\isa{\isacommand{datatype}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ op\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}} -\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{op\ {\isaliteral{40}{\isacharat}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{butlast} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{concat} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{distinct} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{drop} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{dropWhile} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{filter} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{List{\isaliteral{2E}{\isachardot}}find} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option}\\ -\isa{fold} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\isa{foldr} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\ -\isa{foldl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{hd} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{last} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{length} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat}\\ -\isa{lenlex} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{lex} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{lexn} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{lexord} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{listrel} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ list{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{listrel{\isadigit{1}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{lists} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ set}\\ -\isa{listset} & \isa{{\isaliteral{27}{\isacharprime}}a\ set\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ set}\\ -\isa{listsum} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{list{\isaliteral{5F}{\isacharunderscore}}all{\isadigit{2}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{list{\isaliteral{5F}{\isacharunderscore}}update} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{map} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list}\\ -\isa{measures} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set}\\ -\isa{op\ {\isaliteral{21}{\isacharbang}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\ -\isa{remdups} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{removeAll} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{remove{\isadigit{1}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{replicate} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{rev} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{rotate} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{rotate{\isadigit{1}}} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{set} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{sort} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{sorted} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{splice} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{sublist} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{take} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{takeWhile} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{tl} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\ -\isa{upt} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ list}\\ -\isa{upto} & \isa{int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ list}\\ -\isa{zip} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{{\isaliteral{5B}{\isacharbrackleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{23}{\isacharhash}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}\\ -\isa{{\isaliteral{5B}{\isacharbrackleft}}m{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}n{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}upt\ m\ n{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5B}{\isacharbrackleft}}i{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}j{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}upto\ i\ j{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5B}{\isacharbrackleft}}e{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs{\isaliteral{5D}{\isacharbrackright}}} & \isa{map\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ e{\isaliteral{29}{\isacharparenright}}\ xs}\\ -\isa{{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}xs\ {\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}filter\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}\ xs{\isaliteral{22}{\isachardoublequote}}} \\ -\isa{xs{\isaliteral{5B}{\isacharbrackleft}}n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}list{\isaliteral{5F}{\isacharunderscore}}update\ xs\ n\ x{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}xs{\isaliteral{2E}{\isachardot}}\ e} & \isa{{\isaliteral{22}{\isachardoublequote}}listsum\ {\isaliteral{28}{\isacharparenleft}}map\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ e{\isaliteral{29}{\isacharparenright}}\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\end{supertabular} -\medskip - -List comprehension: \isa{{\isaliteral{5B}{\isacharbrackleft}}e{\isaliteral{2E}{\isachardot}}\ q\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ q\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}} where each -qualifier \isa{q\isaliteral{5C3C5E697375623E}{}\isactrlisub i} is either a generator \mbox{\isa{pat\ {\isaliteral{5C3C6C6566746172726F773E}{\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. - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -\isa{Map{\isaliteral{2E}{\isachardot}}empty} & \isa{{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\ -\isa{op\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\ -\isa{op\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}c\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\ -\isa{op\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{60}{\isacharbackquote}}} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\ -\isa{dom} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\ -\isa{ran} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ set}\\ -\isa{op\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}\\ -\isa{map{\isaliteral{5F}{\isacharunderscore}}of} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\ -\isa{map{\isaliteral{5F}{\isacharunderscore}}upds} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -\isa{Map{\isaliteral{2E}{\isachardot}}empty} & \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ None}\\ -\isa{m{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ y{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}Some\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{m{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{{\isaliteral{5B}{\isacharbrackleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}Map{\isaliteral{2E}{\isachardot}}empty{\isaliteral{28}{\isacharparenleft}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}y\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ -\isa{m{\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{5D}{\isacharbrackright}}\ ys{\isaliteral{29}{\isacharparenright}}} & \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{5F}{\isacharunderscore}}upds\ m\ xs\ ys{\isaliteral{22}{\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 54da920baf38 -r ac15a85e9282 doc-src/Main/Main_Doc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/Main_Doc.thy Mon Aug 27 21:30:18 2012 +0200 @@ -0,0 +1,596 @@ +(*<*) +theory Main_Doc +imports Main +begin + +setup {* + let + fun pretty_term_type_only ctxt (t, T) = + (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () + else error "term_type_only: type mismatch"; + Syntax.pretty_typ ctxt T) + in + Thy_Output.antiquotation @{binding term_type_only} + (Args.term -- Args.typ_abbrev) + (fn {source, context = ctxt, ...} => fn arg => + Thy_Output.output ctxt + (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg])) + end +*} +setup {* + Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single) + (fn {source, context, ...} => Thy_Output.output context o + Thy_Output.maybe_pretty_source Syntax.pretty_typ context source) +*} +(*>*) +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/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 Orderings.less_eq} & @{typeof Orderings.less_eq} & (\verb$<=$)\\ +@{const Orderings.less} & @{typeof Orderings.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 Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \ 'a::Inf"}\\ +@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \ 'a::Sup"}\\ +\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 Set.insert} & @{term_type_only insert "'a\'a set\'a set"}\\ +@{const Collect} & @{term_type_only Collect "('a\bool)\'a set"}\\ +@{const Set.member} & @{term_type_only Set.member "'a\'a set\bool"} & (\texttt{:})\\ +@{const Set.union} & @{term_type_only Set.union "'a set\'a set \ 'a set"} & (\texttt{Un})\\ +@{const Set.inter} & @{term_type_only Set.inter "'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 l @ {}} +@{const "Fun.id"} & @{typeof Fun.id}\\ +@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\ +@{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{Hilbert\_Choice} + +Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}. +\smallskip + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \ ('a \ 'b) \ ('b \ 'a)"} +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term inv} & @{term[source]"inv_into UNIV"} +\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{tabular}{@ {} l @ {~::~} l @ {}} +@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \ ('b*'a)set"}\\ +@{const Relation.relcomp} & @{term_type_only Relation.relcomp "('a*'b)set\('b*'c)set\('a*'c)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{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} +@{term"converse r"} & @{term[source]"converse r"} & (\verb$^-1$) +\end{tabular} +\medskip + +\noindent +Type synonym \ @{typ"'a rel"} @{text"="} @{expanded_typ "'a rel"} + +\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"}\\ +@{const Transitive_Closure.acyclic} & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\bool"}\\ +@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\nat\('a*'a)set" "('a*'a)set\nat\('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 Groups}, @{theory Rings}, @{theory Fields} 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}\\ +@{term "op ^^ :: ('a \ 'a) \ nat \ 'a \ 'a"} & + @{term_type_only "op ^^ :: ('a \ 'a) \ nat \ 'a \ 'a" "('a \ 'a) \ nat \ 'a \ 'a"} +\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 Big_Operators.setsum} & @{term_type_only Big_Operators.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\ +@{const Big_Operators.setprod} & @{term_type_only Big_Operators.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.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{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"}\\ +@{const Option.bind} & @{term_type_only Option.bind "'a option \ ('a \ 'b option) \ 'b option"} +\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.find} & @{typeof List.find}\\ +@{const List.fold} & @{typeof List.fold}\\ +@{const List.foldr} & @{typeof List.foldr}\\ +@{const List.foldl} & @{typeof List.foldl}\\ +@{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*'b)set\('a list * 'b list)set"}\\ +@{const List.listrel1} & @{term_type_only List.listrel1 "('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.nth} & @{typeof List.nth}\\ +@{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. + +\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 54da920baf38 -r ac15a85e9282 doc-src/Main/Makefile --- a/doc-src/Main/Makefile Mon Aug 27 21:19:16 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ - -## targets - -default: dvi - - -## dependencies - -include ../Makefile.in - -NAME = main - -FILES = ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty $(NAME).tex \ - Docs/document/Main_Doc.tex - -dvi: $(NAME).dvi - -$(NAME).dvi: $(FILES) - $(LATEX) $(NAME) - -pdf: $(NAME).pdf - -$(NAME).pdf: $(FILES) - $(PDFLATEX) $(NAME) diff -r 54da920baf38 -r ac15a85e9282 doc-src/Main/document/build --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/document/build Mon Aug 27 21:30:18 2012 +0200 @@ -0,0 +1,11 @@ +#!/bin/bash + +set -e + +FORMAT="$1" +VARIANT="$2" + +"$ISABELLE_TOOL" latex -o sty +"$ISABELLE_TOOL" latex -o "$FORMAT" +"$ISABELLE_TOOL" latex -o "$FORMAT" + diff -r 54da920baf38 -r ac15a85e9282 doc-src/Main/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Main/document/root.tex Mon Aug 27 21:30:18 2012 +0200 @@ -0,0 +1,38 @@ +\documentclass[12pt,a4paper]{article} + +\oddsidemargin=4.6mm +\evensidemargin=4.6mm +\textwidth=150mm +\topmargin=4.6mm +\headheight=0mm +\headsep=0mm +\textheight=234mm + +\usepackage{isabelle,isabellesym} +\usepackage{amssymb} +\usepackage[only,bigsqcap]{stmaryrd} + +% 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.tex} + +\end{document} diff -r 54da920baf38 -r ac15a85e9282 doc-src/Main/main.tex --- a/doc-src/Main/main.tex Mon Aug 27 21:19:16 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -\documentclass[12pt,a4paper]{article} - -\oddsidemargin=4.6mm -\evensidemargin=4.6mm -\textwidth=150mm -\topmargin=4.6mm -\headheight=0mm -\headsep=0mm -\textheight=234mm - -\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym} -\usepackage{amssymb} -\usepackage[only,bigsqcap]{stmaryrd} - -% 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{Docs/document/Main_Doc.tex} - -% optional bibliography -%\bibliographystyle{abbrv} -%\bibliography{root} - -\end{document} diff -r 54da920baf38 -r ac15a85e9282 doc-src/ROOT --- a/doc-src/ROOT Mon Aug 27 21:19:16 2012 +0200 +++ b/doc-src/ROOT Mon Aug 27 21:30:18 2012 +0200 @@ -123,10 +123,12 @@ "document/build" "document/root.tex" -session Main (doc) in "Main/Docs" = HOL + - options [browser_info = false, document = false, - document_dump = document, document_dump_mode = "tex"] +session Main (doc) in "Main" = HOL + + options [document_variants = "main"] theories Main_Doc + files + "document/build" + "document/root.tex" session ProgProve (doc) in "ProgProve/Thys" = HOL + options [browser_info = false, document = false,