Theory Main_Doc

(*<*)
theory Main_Doc
imports Main
begin

setup ‹
  Document_Output.antiquotation_pretty_source binding‹term_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 binding‹expanded_typ› Args.typ
    Syntax.pretty_typ
›
(*>*)
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. 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: prop‹x = y›, const‹True›, const‹False›, prop‹¬ P›, prop‹P ∧ Q›,
prop‹P ∨ Q›, prop‹P ⟶ Q›, prop‹∀x. P›, prop‹∃x. P›, prop‹∃! x. P›,
term‹THE x. P›.
┈

\begin{tabular}{@ {} l @ {~::~} l @ {}}
const‹HOL.undefined› & typeof‹HOL.undefined›\\
const‹HOL.default› & typeof‹HOL.default›\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
term‹¬ (x = y)› & @{term[source]"¬ (x = y)"} & (▩‹~=›)\\
@{term[source]"P ⟷ Q"} & term‹P ⟷ Q› \\
term‹If x y z› & @{term[source]"If x y z"}\\
term‹Let 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 @ {}}
const‹Orderings.less_eq› & typeof‹Orderings.less_eq› & (▩‹<=›)\\
const‹Orderings.less› & typeof‹Orderings.less›\\
const‹Orderings.Least› & typeof‹Orderings.Least›\\
const‹Orderings.Greatest› & typeof‹Orderings.Greatest›\\
const‹Orderings.min› & typeof‹Orderings.min›\\
const‹Orderings.max› & typeof‹Orderings.max›\\
@{const[source] top} & typeof‹Orderings.top›\\
@{const[source] bot} & typeof‹Orderings.bot›\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
@{term[source]"x ≥ y"} & term‹x ≥ y› & (▩‹>=›)\\
@{term[source]"x > y"} & term‹x > y›\\
term‹∀x≤y. P› & @{term[source]"∀x. x ≤ y ⟶ P"}\\
term‹∃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)"}\\
term‹GREATEST x. P› & @{term[source]"Greatest (λx. P)"}\\
\end{tabular}


\section*{Lattices}

Classes semilattice, lattice, distributive lattice and complete lattice (the
latter in theory theory‹HOL.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 via ⬚‹unbundle lattice_syntax›.

\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‹Inf A›\\
@{text[source]"⨆A"} & term‹Sup A›\\
@{text[source]"⊤"} & @{term[source] top}\\
@{text[source]"⊥"} & @{term[source] bot}\\
\end{supertabular}


\section*{Set}

\begin{tabular}{@ {} 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"} & (▩‹:›)\\
const‹Set.union› & @{term_type_only Set.union "'a set⇒'a set ⇒ 'a set"} & (▩‹Un›)\\
const‹Set.inter› & @{term_type_only Set.inter "'a set⇒'a set ⇒ 'a set"} & (▩‹Int›)\\
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{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
‹{a1,…,an}› & ‹insert a1 (… (insert an {})…)›\\
term‹a ∉ 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)"}\\
‹{t | x1 … xn. P}› & ‹{v. ∃x1 … xn. v = t ∧ P}›\\
@{term[source]"⋃x∈I. A"} & @{term[source]"⋃((λx. A) ` I)"} & (\texttt{UN})\\
@{term[source]"⋃x. A"} & @{term[source]"⋃((λx. A) ` UNIV)"}\\
@{term[source]"⋂x∈I. A"} & @{term[source]"⋂((λx. A) ` I)"} & (\texttt{INT})\\
@{term[source]"⋂x. A"} & @{term[source]"⋂((λx. A) ` UNIV)"}\\
term‹∀x∈A. P› & @{term[source]"Ball A (λx. P)"}\\
term‹∃x∈A. P› & @{term[source]"Bex A (λx. P)"}\\
term‹range f› & @{term[source]"f ` UNIV"}\\
\end{tabular}


\section*{Fun}

\begin{tabular}{@ {} 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.monotone_on› & typeof‹Fun.monotone_on›\\
const‹Fun.monotone› & typeof‹Fun.monotone›\\
const‹Fun.mono_on› & typeof‹Fun.mono_on›\\
const‹Fun.mono› & typeof‹Fun.mono›\\
const‹Fun.strict_mono_on› & typeof‹Fun.strict_mono_on›\\
const‹Fun.strict_mono› & typeof‹Fun.strict_mono›\\
const‹Fun.antimono› & typeof‹Fun.antimono›\\
const‹Fun.fun_upd› & typeof‹Fun.fun_upd›\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
term‹fun_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: term‹SOME x. P›.
┈

\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‹HOL.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 ‹+›.

\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 ‹×›.

\begin{tabular}{@ {} l @ {~::~} l @ {}}
const‹Product_Type.Unity› & typeof‹Product_Type.Unity›\\
const‹Pair› & typeof‹Pair›\\
const‹fst› & typeof‹fst›\\
const‹snd› & typeof‹snd›\\
const‹case_prod› & typeof‹case_prod›\\
const‹curry› & typeof‹curry›\\
const‹Product_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 @ {}}
term‹Pair a b› & @{term[source]"Pair a b"}\\
term‹case_prod (λx y. t)› & @{term[source]"case_prod (λx y. t)"}\\
term‹A × 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 @ {}}
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{supertabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
term‹converse 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 @ {}}
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{tabular}

\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 "(^^) :: ('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"} & (▩‹^*›)\\
term‹trancl r› & @{term[source]"trancl r"} & (▩‹^+›)\\
term‹reflcl r› & @{term[source]"reflcl r"} & (▩‹^=›)
\end{tabular}


\section*{Algebra}

Theories theory‹HOL.Groups›, theory‹HOL.Rings›,
theory‹HOL.Euclidean_Rings› and theory‹HOL.Fields›
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› & typeof‹zero›\\
‹1› & typeof‹one›\\
const‹plus› & typeof‹plus›\\
const‹minus› & typeof‹minus›\\
const‹uminus› & typeof‹uminus› & (▩‹-›)\\
const‹times› & typeof‹times›\\
const‹inverse› & typeof‹inverse›\\
const‹divide› & typeof‹divide›\\
const‹abs› & typeof‹abs›\\
const‹sgn› & typeof‹sgn›\\
const‹Rings.dvd› & typeof‹Rings.dvd›\\
const‹divide› & typeof‹divide›\\
const‹modulo› & typeof‹modulo›\\
\end{tabular}

\subsubsection*{Syntax}

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


\section*{Nat}

datatype‹nat›
━

\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› &
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‹(^^) :: ('a ⇒ 'a) ⇒ nat ⇒ 'a ⇒ 'a› &
  @{term_type_only "(^^) :: ('a ⇒ 'a) ⇒ nat ⇒ 'a ⇒ 'a" "('a ⇒ 'a) ⇒ nat ⇒ 'a ⇒ 'a"}
\end{tabular}

\section*{Int}

Type typ‹int›
━

\begin{tabular}{@ {} llllllll @ {}}
term‹(+) :: int ⇒ int ⇒ int› &
term‹(-) :: int ⇒ int ⇒ int› &
term‹uminus :: 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› &
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"} & (▩‹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{tabular}{@ {} 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"}\\
\end{tabular}


\section*{Lattices\_Big}

\begin{tabular}{@ {} l @ {~::~} l l @ {}}
const‹Lattices_Big.Min› & typeof‹Lattices_Big.Min›\\
const‹Lattices_Big.Max› & typeof‹Lattices_Big.Max›\\
const‹Lattices_Big.arg_min› & typeof‹Lattices_Big.arg_min›\\
const‹Lattices_Big.is_arg_min› & typeof‹Lattices_Big.is_arg_min›\\
const‹Lattices_Big.arg_max› & typeof‹Lattices_Big.arg_max›\\
const‹Lattices_Big.is_arg_max› & typeof‹Lattices_Big.is_arg_max›\\
\end{tabular}

\subsubsection*{Syntax}

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


\section*{Groups\_Big}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
const‹Groups_Big.sum› & @{term_type_only Groups_Big.sum "('a ⇒ 'b) ⇒ 'a set ⇒ 'b::comm_monoid_add"}\\
const‹Groups_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 @ {}}
term‹sum (λx. x) A› & @{term[source]"sum (λx. x) A"} & (▩‹SUM›)\\
term‹sum (λx. t) A› & @{term[source]"sum (λx. t) A"}\\
@{term[source] "∑x|P. t"} & term‹∑x|P. t›\\
\multicolumn{2}{@ {}l@ {}}{Similarly for ‹∏› instead of ‹∑›} & (▩‹PROD›)\\
\end{tabular}


\section*{Wellfounded}

\begin{tabular}{@ {} 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{tabular}


\section*{Set\_Interval} % theory‹HOL.Set_Interval›

\begin{tabular}{@ {} 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{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} 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[source] "⋃i≤n. A"} & @{term[source] "⋃i ∈ {..n}. A"}\\
@{term[source] "⋃i<n. A"} & @{term[source] "⋃i ∈ {..<n}. A"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for ‹⋂› instead of ‹⋃›}\\
term‹sum (λx. t) {a..b}› & @{term[source] "sum (λx. t) {a..b}"}\\
term‹sum (λx. t) {a..<b}› & @{term[source] "sum (λx. t) {a..<b}"}\\
term‹sum (λx. t) {..b}› & @{term[source] "sum (λx. t) {..b}"}\\
term‹sum (λx. t) {..<b}› & @{term[source] "sum (λx. t) {..<b}"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for ‹∏› instead of ‹∑›}\\
\end{tabular}


\section*{Power}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
const‹Power.power› & typeof‹Power.power›
\end{tabular}


\section*{Option}

datatype‹option›
━

\begin{tabular}{@ {} l @ {~::~} l @ {}}
const‹Option.the› & typeof‹Option.the›\\
const‹map_option› & @{typ[source]"('a ⇒ 'b) ⇒ 'a option ⇒ 'b option"}\\
const‹set_option› & @{term_type_only set_option "'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›
━

\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.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.nths› & typeof‹List.nths›\\
const‹Groups_List.prod_list› & typeof‹Groups_List.prod_list›\\
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.shuffles› & typeof‹List.shuffles›\\
const‹List.sort› & typeof‹List.sort›\\
const‹List.sorted› & typeof‹List.sorted›\\
const‹List.sorted_wrt› & typeof‹List.sorted_wrt›\\
const‹List.splice› & typeof‹List.splice›\\
const‹Groups_List.sum_list› & typeof‹Groups_List.sum_list›\\
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{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"}\\
term‹xs[n := x]› & @{term[source]"list_update xs n x"}\\
term‹∑x←xs. 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 term‹filter (λ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 @ {}}
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{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
term‹Map.empty› & @{term[source] "λ_. None"}\\
term‹m(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)"}\\
term‹map_upds m xs ys› & @{term[source]"map_upds m xs ys"}\\
\end{tabular}

\section*{Infix operators in Main} % theory‹Main›

\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
(*>*)