theory Main_Doc
imports Main
begin
setup ‹
Thy_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 ‹
Thy_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›.
\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{supertabular}{@ {} 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 e⇩1 (λx. e⇩2)"} & @{term[source]"Let e⇩1 (λx. e⇩2)"}\\
\end{supertabular}
\section*{Orderings}
A collection of classes defining basic orderings:
preorder, partial order, linear order, dense linear order and wellorder.
┈
\begin{supertabular}{@ {} 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}\\
@{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"} & (▩‹>=›)\\
@{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{supertabular}
\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 by loading theory ‹Lattice_Syntax› in directory ‹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"Inf A"}\\
@{text[source]"⨆A"} & @{term"Sup A"}\\
@{text[source]"⊤"} & @{term[source] top}\\
@{text[source]"⊥"} & @{term[source] bot}\\
\end{supertabular}
\section*{Set}
\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"} & (▩‹:›)\\
@{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⇒('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 @ {}}
‹{a⇩1,…,a⇩n}› & ‹insert a⇩1 (… (insert a⇩n {})…)›\\
@{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 | x⇩1 … x⇩n. P}› & ‹{v. ∃x⇩1 … x⇩n. v = t ∧ P}›\\
@{term[source]"⋃x∈I. A"} & @{term[source]"UNION I (λx. A)"} & (\texttt{UN})\\
@{term[source]"⋃x. A"} & @{term[source]"UNION UNIV (λx. A)"}\\
@{term[source]"⋂x∈I. A"} & @{term[source]"INTER I (λx. A)"} & (\texttt{INT})\\
@{term[source]"⋂x. A"} & @{term[source]"INTER UNIV (λx. A)"}\\
@{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{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"}\\
‹f(x⇩1:=y⇩1,…,x⇩n:=y⇩n)› & ‹f(x⇩1:=y⇩1)…(x⇩n:=y⇩n)›\\
\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{supertabular}{@ {} 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{supertabular}
\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{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"} & (▩‹^-1›)
\end{tabular}
┉
\noindent
Type synonym \ @{typ"'a rel"} ‹=› @{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 "(^^) :: ('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.Fields} and @{theory
HOL.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 @ {}}
‹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{supertabular}
\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{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"}\\
\end{supertabular}
\section*{Lattices\_Big}
\begin{supertabular}{@ {} 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{supertabular}
\subsubsection*{Syntax}
\begin{supertabular}{@ {} 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{supertabular}
\section*{Groups\_Big}
\begin{supertabular}{@ {} 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{supertabular}
\subsubsection*{Syntax}
\begin{supertabular}{@ {} 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{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*{Set\_Interval} % @{theory HOL.Set_Interval}
\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[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{supertabular}
\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 Groups_List.sum_list} & @{typeof Groups_List.sum_list}\\
@{const Groups_List.prod_list} & @{typeof Groups_List.prod_list}\\
@{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 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.shuffle} & @{typeof List.shuffle}\\
@{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 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 @ {}}
‹[x⇩1,…,x⇩n]› & ‹x⇩1 # … # x⇩n # []›\\
@{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{supertabular}
┉
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. q⇩1, …, q⇩n]› where each
qualifier ‹q⇩i› 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{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)"}\\
‹m(x⇩1↦y⇩1,…,x⇩n↦y⇩n)› & @{text[source]"m(x⇩1↦y⇩1)…(x⇩n↦y⇩n)"}\\
‹[x⇩1↦y⇩1,…,x⇩n↦y⇩n]› & @{text[source]"Map.empty(x⇩1↦y⇩1,…,x⇩n↦y⇩n)"}\\
@{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