Theory Main_Doc

(*<*)
theory Main_Doc
imports Main
begin

setup Document_Output.antiquotation_pretty_source bindingterm_type_only (Args.term -- Args.typ_abbrev)
    (fn ctxt => fn (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))
setup Document_Output.antiquotation_pretty_source bindingexpanded_typ Args.typ
    Syntax.pretty_typ
(*>*)
text‹

\begin{abstract}
This document lists the main types, functions and syntax provided by theory theoryMain. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see 🌐‹https://isabelle.in.tum.de/library/HOL/HOL›.
\end{abstract}

\section*{HOL}

The basic logic: propx = y, constTrue, constFalse, prop¬ P, propP  Q,
propP  Q, propP  Q, propx. P, propx. P, prop∃! x. P,
termTHE x. P.


\begin{tabular}{@ {} l @ {~::~} l @ {}}
constHOL.undefined & typeofHOL.undefined\\
constHOL.default & typeofHOL.default\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
term¬ (x = y) & @{term[source]"¬ (x = y)"} & (‹~=›)\\
@{term[source]"P  Q"} & termP  Q \\
termIf x y z & @{term[source]"If x y z"}\\
termLet e1 (λx. e2) & @{term[source]"Let e1 (λx. e2)"}\\
\end{tabular}


\section*{Orderings}

A collection of classes defining basic orderings:
preorder, partial order, linear order, dense linear order and wellorder.


\begin{tabular}{@ {} l @ {~::~} l l @ {}}
constOrderings.less_eq & typeofOrderings.less_eq & (‹<=›)\\
constOrderings.less & typeofOrderings.less\\
constOrderings.Least & typeofOrderings.Least\\
constOrderings.Greatest & typeofOrderings.Greatest\\
constOrderings.min & typeofOrderings.min\\
constOrderings.max & typeofOrderings.max\\
@{const[source] top} & typeofOrderings.top\\
@{const[source] bot} & typeofOrderings.bot\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
@{term[source]"x  y"} & termx  y & (‹>=›)\\
@{term[source]"x > y"} & termx > y\\
termxy. P & @{term[source]"x. x  y  P"}\\
termxy. P & @{term[source]"x. x  y  P"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
termLEAST x. P & @{term[source]"Least (λx. P)"}\\
termGREATEST x. P & @{term[source]"Greatest (λx. P)"}\\
\end{tabular}


\section*{Lattices}

Classes semilattice, lattice, distributive lattice and complete lattice (the
latter in theory theoryHOL.Set).

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constLattices.inf & typeofLattices.inf\\
constLattices.sup & typeofLattices.sup\\
constComplete_Lattices.Inf & @{term_type_only Complete_Lattices.Inf "'a set  'a::Inf"}\\
constComplete_Lattices.Sup & @{term_type_only Complete_Lattices.Sup "'a set  'a::Sup"}\\
\end{tabular}

\subsubsection*{Syntax}

Available via unbundle lattice_syntax›.

\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
@{text[source]"x ⊑ y"} & termx  y\\
@{text[source]"x ⊏ y"} & termx < y\\
@{text[source]"x ⊓ y"} & terminf x y\\
@{text[source]"x ⊔ y"} & termsup x y\\
@{text[source]"⨅A"} & termInf A\\
@{text[source]"⨆A"} & termSup A\\
@{text[source]"⊤"} & @{term[source] top}\\
@{text[source]"⊥"} & @{term[source] bot}\\
\end{supertabular}


\section*{Set}

\begin{tabular}{@ {} l @ {~::~} l l @ {}}
constSet.empty & @{term_type_only "Set.empty" "'a set"}\\
constSet.insert & @{term_type_only insert "'a'a set'a set"}\\
constCollect & @{term_type_only Collect "('abool)'a set"}\\
constSet.member & @{term_type_only Set.member "'a'a setbool"} & (‹:›)\\
constSet.union & @{term_type_only Set.union "'a set'a set  'a set"} & (‹Un›)\\
constSet.inter & @{term_type_only Set.inter "'a set'a set  'a set"} & (‹Int›)\\
constUnion & @{term_type_only Union "'a set set'a set"}\\
constInter & @{term_type_only Inter "'a set set'a set"}\\
constPow & @{term_type_only Pow "'a set 'a set set"}\\
constUNIV & @{term_type_only UNIV "'a set"}\\
constimage & @{term_type_only image "('a'b)'a set'b set"}\\
constBall & @{term_type_only Ball "'a set('abool)bool"}\\
constBex & @{term_type_only Bex "'a set('abool)bool"}\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
{a1,…,an}› & insert a1 (… (insert an {})…)›\\
terma  A & @{term[source]"¬(x  A)"}\\
termA  B & @{term[source]"A  B"}\\
termA  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)"}\\
{t | x1 … xn. P}› & {v. ∃x1 … xn. v = t ∧ P}›\\
@{term[source]"xI. A"} & @{term[source]"((λx. A) ` I)"} & (\texttt{UN})\\
@{term[source]"x. A"} & @{term[source]"((λx. A) ` UNIV)"}\\
@{term[source]"xI. A"} & @{term[source]"((λx. A) ` I)"} & (\texttt{INT})\\
@{term[source]"x. A"} & @{term[source]"((λx. A) ` UNIV)"}\\
termxA. P & @{term[source]"Ball A (λx. P)"}\\
termxA. P & @{term[source]"Bex A (λx. P)"}\\
termrange f & @{term[source]"f ` UNIV"}\\
\end{tabular}


\section*{Fun}

\begin{tabular}{@ {} l @ {~::~} l l @ {}}
constFun.id & typeofFun.id\\
constFun.comp & typeofFun.comp & (\texttt{o})\\
constFun.inj_on & @{term_type_only Fun.inj_on "('a'b)'a setbool"}\\
constFun.inj & typeofFun.inj\\
constFun.surj & typeofFun.surj\\
constFun.bij & typeofFun.bij\\
constFun.bij_betw & @{term_type_only Fun.bij_betw "('a'b)'a set'b setbool"}\\
constFun.monotone_on & typeofFun.monotone_on\\
constFun.monotone & typeofFun.monotone\\
constFun.mono_on & typeofFun.mono_on\\
constFun.mono & typeofFun.mono\\
constFun.strict_mono_on & typeofFun.strict_mono_on\\
constFun.strict_mono & typeofFun.strict_mono\\
constFun.antimono & typeofFun.antimono\\
constFun.fun_upd & typeofFun.fun_upd\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
termfun_upd f x y & @{term[source]"fun_upd f x y"}\\
f(x1:=y1,…,xn:=yn)› & f(x1:=y1)…(xn:=yn)›\\
\end{tabular}


\section*{Hilbert\_Choice}

Hilbert's selection ($\varepsilon$) operator: termSOME x. P.


\begin{tabular}{@ {} l @ {~::~} l @ {}}
constHilbert_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 @ {}}
terminv & @{term[source]"inv_into UNIV"}
\end{tabular}

\section*{Fixed Points}

Theory: theoryHOL.Inductive.

Least and greatest fixed points in a complete lattice typ'a:

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constInductive.lfp & typeofInductive.lfp\\
constInductive.gfp & typeofInductive.gfp\\
\end{tabular}

Note that in particular sets (typ'a  bool) are complete lattices.

\section*{Sum\_Type}

Type constructor +›.

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constSum_Type.Inl & typeofSum_Type.Inl\\
constSum_Type.Inr & typeofSum_Type.Inr\\
constSum_Type.Plus & @{term_type_only Sum_Type.Plus "'a set'b set('a+'b)set"}
\end{tabular}


\section*{Product\_Type}

Types typunit and ×›.

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constProduct_Type.Unity & typeofProduct_Type.Unity\\
constPair & typeofPair\\
constfst & typeoffst\\
constsnd & typeofsnd\\
constcase_prod & typeofcase_prod\\
constcurry & typeofcurry\\
constProduct_Type.Sigma & @{term_type_only Product_Type.Sigma "'a set('a'b set)('a*'b)set"}\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
termPair a b & @{term[source]"Pair a b"}\\
termcase_prod (λx y. t) & @{term[source]"case_prod (λx y. t)"}\\
termA × B &  Sigma A (λlatex‹\_›. B)›
\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{(a, (b, c))›.}
Pattern matching with pairs and tuples extends to all binders,
e.g.\ \mbox{prop(x,y)A. P,} term{(x,y). P}, etc.


\section*{Relation}

\begin{supertabular}{@ {} l @ {~::~} l @ {}}
constRelation.converse & @{term_type_only Relation.converse "('a * 'b)set  ('b*'a)set"}\\
constRelation.relcomp & @{term_type_only Relation.relcomp "('a*'b)set('b*'c)set('a*'c)set"}\\
constRelation.Image & @{term_type_only Relation.Image "('a*'b)set'a set'b set"}\\
constRelation.inv_image & @{term_type_only Relation.inv_image "('a*'a)set('b'a)('b*'b)set"}\\
constRelation.Id_on & @{term_type_only Relation.Id_on "'a set('a*'a)set"}\\
constRelation.Id & @{term_type_only Relation.Id "('a*'a)set"}\\
constRelation.Domain & @{term_type_only Relation.Domain "('a*'b)set'a set"}\\
constRelation.Range & @{term_type_only Relation.Range "('a*'b)set'b set"}\\
constRelation.Field & @{term_type_only Relation.Field "('a*'a)set'a set"}\\
constRelation.refl_on & @{term_type_only Relation.refl_on "'a set('a*'a)setbool"}\\
constRelation.refl & @{term_type_only Relation.refl "('a*'a)setbool"}\\
constRelation.sym & @{term_type_only Relation.sym "('a*'a)setbool"}\\
constRelation.antisym & @{term_type_only Relation.antisym "('a*'a)setbool"}\\
constRelation.trans & @{term_type_only Relation.trans "('a*'a)setbool"}\\
constRelation.irrefl & @{term_type_only Relation.irrefl "('a*'a)setbool"}\\
constRelation.total_on & @{term_type_only Relation.total_on "'a set('a*'a)setbool"}\\
constRelation.total & @{term_type_only Relation.total "('a*'a)setbool"}\\
\end{supertabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
termconverse r & @{term[source]"converse r"} & (‹^-1›)
\end{tabular}


\noindent
Type synonym \ typ'a rel =› @{expanded_typ "'a rel"}

\section*{Equiv\_Relations}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constEquiv_Relations.equiv & @{term_type_only Equiv_Relations.equiv "'a set  ('a*'a)setbool"}\\
constEquiv_Relations.quotient & @{term_type_only Equiv_Relations.quotient "'a set  ('a × 'a) set  'a set set"}\\
constEquiv_Relations.congruent & @{term_type_only Equiv_Relations.congruent "('a*'a)set('a'b)bool"}\\
constEquiv_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{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
termcongruent r f & @{term[source]"congruent r f"}\\
termcongruent2 r r f & @{term[source]"congruent2 r r f"}\\
\end{tabular}


\section*{Transitive\_Closure}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constTransitive_Closure.rtrancl & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set('a*'a)set"}\\
constTransitive_Closure.trancl & @{term_type_only Transitive_Closure.trancl "('a*'a)set('a*'a)set"}\\
constTransitive_Closure.reflcl & @{term_type_only Transitive_Closure.reflcl "('a*'a)set('a*'a)set"}\\
constTransitive_Closure.acyclic & @{term_type_only Transitive_Closure.acyclic "('a*'a)setbool"}\\
constcompower & @{term_type_only "(^^) :: ('a*'a)setnat('a*'a)set" "('a*'a)setnat('a*'a)set"}\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
termrtrancl r & @{term[source]"rtrancl r"} & (‹^*›)\\
termtrancl r & @{term[source]"trancl r"} & (‹^+›)\\
termreflcl r & @{term[source]"reflcl r"} & (‹^=›)
\end{tabular}


\section*{Algebra}

Theories theoryHOL.Groups, theoryHOL.Rings, theoryHOL.Fields and theoryHOL.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{tabular}{@ {} l @ {~::~} l l @ {}}
0› & typeofzero\\
1› & typeofone\\
constplus & typeofplus\\
constminus & typeofminus\\
constuminus & typeofuminus & (‹-›)\\
consttimes & typeoftimes\\
constinverse & typeofinverse\\
constdivide & typeofdivide\\
constabs & typeofabs\\
constsgn & typeofsgn\\
constRings.dvd & typeofRings.dvd\\
constdivide & typeofdivide\\
constmodulo & typeofmodulo\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
term¦x¦ & @{term[source] "abs x"}
\end{tabular}


\section*{Nat}

datatypenat


\begin{tabular}{@ {} lllllll @ {}}
term(+) :: nat  nat  nat &
term(-) :: nat  nat  nat &
term(*) :: nat  nat  nat &
term(^) :: nat  nat  nat &
term(div) :: nat  nat  nat&
term(mod) :: nat  nat  nat&
term(dvd) :: nat  nat  bool\\
term(≤) :: nat  nat  bool &
term(<) :: nat  nat  bool &
termmin :: nat  nat  nat &
termmax :: nat  nat  nat &
termMin :: nat set  nat &
termMax :: nat set  nat\\
\end{tabular}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constNat.of_nat & typeofNat.of_nat\\
term(^^) :: ('a  'a)  nat  'a  'a &
  @{term_type_only "(^^) :: ('a  'a)  nat  'a  'a" "('a  'a)  nat  'a  'a"}
\end{tabular}

\section*{Int}

Type typint


\begin{tabular}{@ {} llllllll @ {}}
term(+) :: int  int  int &
term(-) :: int  int  int &
termuminus :: int  int &
term(*) :: int  int  int &
term(^) :: int  nat  int &
term(div) :: int  int  int&
term(mod) :: int  int  int&
term(dvd) :: int  int  bool\\
term(≤) :: int  int  bool &
term(<) :: int  int  bool &
termmin :: int  int  int &
termmax :: int  int  int &
termMin :: int set  int &
termMax :: int set  int\\
termabs :: int  int &
termsgn :: int  int\\
\end{tabular}

\begin{tabular}{@ {} l @ {~::~} l l @ {}}
constInt.nat & typeofInt.nat\\
constInt.of_int & typeofInt.of_int\\
constInt.Ints & @{term_type_only Int.Ints "'a::ring_1 set"} & (‹Ints›)
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
termof_nat::natint & @{term[source]"of_nat"}\\
\end{tabular}


\section*{Finite\_Set}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constFinite_Set.finite & @{term_type_only Finite_Set.finite "'a setbool"}\\
constFinite_Set.card & @{term_type_only Finite_Set.card "'a set  nat"}\\
constFinite_Set.fold & @{term_type_only Finite_Set.fold "('a  'b  'b)  'b  'a set  'b"}\\
\end{tabular}


\section*{Lattices\_Big}

\begin{tabular}{@ {} l @ {~::~} l l @ {}}
constLattices_Big.Min & typeofLattices_Big.Min\\
constLattices_Big.Max & typeofLattices_Big.Max\\
constLattices_Big.arg_min & typeofLattices_Big.arg_min\\
constLattices_Big.is_arg_min & typeofLattices_Big.is_arg_min\\
constLattices_Big.arg_max & typeofLattices_Big.arg_max\\
constLattices_Big.is_arg_max & typeofLattices_Big.is_arg_max\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
termARG_MIN f x. P & @{term[source]"arg_min f (λx. P)"}\\
termARG_MAX f x. P & @{term[source]"arg_max f (λx. P)"}\\
\end{tabular}


\section*{Groups\_Big}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constGroups_Big.sum & @{term_type_only Groups_Big.sum "('a  'b)  'a set  'b::comm_monoid_add"}\\
constGroups_Big.prod & @{term_type_only Groups_Big.prod "('a  'b)  'a set  'b::comm_monoid_mult"}\\
\end{tabular}


\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
termsum (λx. x) A & @{term[source]"sum (λx. x) A"} & (‹SUM›)\\
termsum (λx. t) A & @{term[source]"sum (λx. t) A"}\\
@{term[source] "x|P. t"} & termx|P. t\\
\multicolumn{2}{@ {}l@ {}}{Similarly for ∏› instead of ∑›} & (‹PROD›)\\
\end{tabular}


\section*{Wellfounded}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constWellfounded.wf & @{term_type_only Wellfounded.wf "('a*'a)setbool"}\\
constWellfounded.acc & @{term_type_only Wellfounded.acc "('a*'a)set'a set"}\\
constWellfounded.measure & @{term_type_only Wellfounded.measure "('anat)('a*'a)set"}\\
constWellfounded.lex_prod & @{term_type_only Wellfounded.lex_prod "('a*'a)set('b*'b)set(('a*'b)*('a*'b))set"}\\
constWellfounded.mlex_prod & @{term_type_only Wellfounded.mlex_prod "('anat)('a*'a)set('a*'a)set"}\\
constWellfounded.less_than & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\
constWellfounded.pred_nat & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\
\end{tabular}


\section*{Set\_Interval} % theoryHOL.Set_Interval

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constlessThan & @{term_type_only lessThan "'a::ord  'a set"}\\
constatMost & @{term_type_only atMost "'a::ord  'a set"}\\
constgreaterThan & @{term_type_only greaterThan "'a::ord  'a set"}\\
constatLeast & @{term_type_only atLeast "'a::ord  'a set"}\\
constgreaterThanLessThan & @{term_type_only greaterThanLessThan "'a::ord  'a  'a set"}\\
constatLeastLessThan & @{term_type_only atLeastLessThan "'a::ord  'a  'a set"}\\
constgreaterThanAtMost & @{term_type_only greaterThanAtMost "'a::ord  'a  'a set"}\\
constatLeastAtMost & @{term_type_only atLeastAtMost "'a::ord  'a  'a set"}\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
termlessThan y & @{term[source] "lessThan y"}\\
termatMost y & @{term[source] "atMost y"}\\
termgreaterThan x & @{term[source] "greaterThan x"}\\
termatLeast x & @{term[source] "atLeast x"}\\
termgreaterThanLessThan x y & @{term[source] "greaterThanLessThan x y"}\\
termatLeastLessThan x y & @{term[source] "atLeastLessThan x y"}\\
termgreaterThanAtMost x y & @{term[source] "greaterThanAtMost x y"}\\
termatLeastAtMost x y & @{term[source] "atLeastAtMost x y"}\\
@{term[source] "in. A"} & @{term[source] "i  {..n}. A"}\\
@{term[source] "i<n. A"} & @{term[source] "i  {..<n}. A"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for ⋂› instead of ⋃›}\\
termsum (λx. t) {a..b} & @{term[source] "sum (λx. t) {a..b}"}\\
termsum (λx. t) {a..<b} & @{term[source] "sum (λx. t) {a..<b}"}\\
termsum (λx. t) {..b} & @{term[source] "sum (λx. t) {..b}"}\\
termsum (λx. t) {..<b} & @{term[source] "sum (λx. t) {..<b}"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for ∏› instead of ∑›}\\
\end{tabular}


\section*{Power}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
constPower.power & typeofPower.power
\end{tabular}


\section*{Option}

datatypeoption


\begin{tabular}{@ {} l @ {~::~} l @ {}}
constOption.the & typeofOption.the\\
constmap_option & @{typ[source]"('a  'b)  'a option  'b option"}\\
constset_option & @{term_type_only set_option "'a option  'a set"}\\
constOption.bind & @{term_type_only Option.bind "'a option  ('a  'b option)  'b option"}
\end{tabular}

\section*{List}

datatypelist


\begin{supertabular}{@ {} l @ {~::~} l @ {}}
constList.append & typeofList.append\\
constList.butlast & typeofList.butlast\\
constList.concat & typeofList.concat\\
constList.distinct & typeofList.distinct\\
constList.drop & typeofList.drop\\
constList.dropWhile & typeofList.dropWhile\\
constList.filter & typeofList.filter\\
constList.find & typeofList.find\\
constList.fold & typeofList.fold\\
constList.foldr & typeofList.foldr\\
constList.foldl & typeofList.foldl\\
constList.hd & typeofList.hd\\
constList.last & typeofList.last\\
constList.length & typeofList.length\\
constList.lenlex & @{term_type_only List.lenlex "('a*'a)set('a list * 'a list)set"}\\
constList.lex & @{term_type_only List.lex "('a*'a)set('a list * 'a list)set"}\\
constList.lexn & @{term_type_only List.lexn "('a*'a)setnat('a list * 'a list)set"}\\
constList.lexord & @{term_type_only List.lexord "('a*'a)set('a list * 'a list)set"}\\
constList.listrel & @{term_type_only List.listrel "('a*'b)set('a list * 'b list)set"}\\
constList.listrel1 & @{term_type_only List.listrel1 "('a*'a)set('a list * 'a list)set"}\\
constList.lists & @{term_type_only List.lists "'a set'a list set"}\\
constList.listset & @{term_type_only List.listset "'a set list  'a list set"}\\
constList.list_all2 & typeofList.list_all2\\
constList.list_update & typeofList.list_update\\
constList.map & typeofList.map\\
constList.measures & @{term_type_only List.measures "('anat)list('a*'a)set"}\\
constList.nth & typeofList.nth\\
constList.nths & typeofList.nths\\
constGroups_List.prod_list & typeofGroups_List.prod_list\\
constList.remdups & typeofList.remdups\\
constList.removeAll & typeofList.removeAll\\
constList.remove1 & typeofList.remove1\\
constList.replicate & typeofList.replicate\\
constList.rev & typeofList.rev\\
constList.rotate & typeofList.rotate\\
constList.rotate1 & typeofList.rotate1\\
constList.set & @{term_type_only List.set "'a list  'a set"}\\
constList.shuffles & typeofList.shuffles\\
constList.sort & typeofList.sort\\
constList.sorted & typeofList.sorted\\
constList.sorted_wrt & typeofList.sorted_wrt\\
constList.splice & typeofList.splice\\
constGroups_List.sum_list & typeofGroups_List.sum_list\\
constList.take & typeofList.take\\
constList.takeWhile & typeofList.takeWhile\\
constList.tl & typeofList.tl\\
constList.upt & typeofList.upt\\
constList.upto & typeofList.upto\\
constList.zip & typeofList.zip\\
\end{supertabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
[x1,…,xn]› & x1 # … # xn # []›\\
term[m..<n] & @{term[source]"upt m n"}\\
term[i..j] & @{term[source]"upto i j"}\\
termxs[n := x] & @{term[source]"list_update xs n x"}\\
termxxs. e & @{term[source]"listsum (map (λx. e) xs)"}\\
\end{tabular}


Filter input syntax [pat ← e. b]›, where
pat› is a tuple pattern, which stands for termfilter (λpat. b) e.

List comprehension input syntax: [e. q1, …, qn]› where each
qualifier qi is either a generator \mbox{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{tabular}{@ {} l @ {~::~} l @ {}}
constMap.empty & typeofMap.empty\\
constMap.map_add & typeofMap.map_add\\
constMap.map_comp & typeofMap.map_comp\\
constMap.restrict_map & @{term_type_only Map.restrict_map "('a'b option)'a set('a'b option)"}\\
constMap.dom & @{term_type_only Map.dom "('a'b option)'a set"}\\
constMap.ran & @{term_type_only Map.ran "('a'b option)'b set"}\\
constMap.map_le & typeofMap.map_le\\
constMap.map_of & typeofMap.map_of\\
constMap.map_upds & typeofMap.map_upds\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
termMap.empty & @{term[source] "λ_. None"}\\
termm(x:=Some y) & @{term[source]"m(x:=Some y)"}\\
m(x1↦y1,…,xn↦yn)› & @{text[source]"m(x1↦y1)…(xn↦yn)"}\\
[x1↦y1,…,xn↦yn]› & @{text[source]"Map.empty(x1↦y1,…,xn↦yn)"}\\
termmap_upds m xs ys & @{term[source]"map_upds m xs ys"}\\
\end{tabular}

\section*{Infix operators in Main} % theoryMain

\begin{center}
\begin{tabular}{llll}
 & Operator & precedence & associativity \\
\hline
Meta-logic & ⟹› & 1 & right \\
& ≡› & 2 \\
\hline
Logic & ∧› & 35 & right \\
&∨› & 30 & right \\
&⟶›, ⟷› & 25 & right\\
&=›, ≠› & 50 & left\\
\hline
Orderings & ≤›, <›, ≥›, >› & 50 \\
\hline
Sets & ⊆›, ⊂›, ⊇›, ⊃› & 50 \\
&∈›, ∉› & 50 \\
&∩› & 70 & left \\
&∪› & 65 & left \\
\hline
Functions and Relations & ∘› & 55 & left\\
&`› & 90 & right\\
&O› & 75 & right\\
&``› & 90 & right\\
&^^› & 80 & right\\
\hline
Numbers & +›, -› & 65 & left \\
&*›, /› & 70 & left \\
&div›, mod› & 70 & left\\
&^› & 80 & right\\
&dvd› & 50 \\
\hline
Lists & #›, @› & 65 & right\\
&!› & 100 & left
\end{tabular}
\end{center}
›
(*<*)
end
(*>*)