Quelle  Main_Doc.thy   Sprache: Isabelle

(*<*)
theory Main_Doc
imports Main
begin

setup ‹
  Document_Output.antiquotation_pretty_source 🍋‹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 🍋‹expanded_typ› Args.typ
    Syntax.pretty_typ
›
(*>*)
text‹

\begin{abstract}
This document lists the main types, functions and syntax provided by 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: 🍋‹x = y›, 🍋‹True›, 🍋‹False›, 🍋‹¬ P›, 🍋‹P ∧ Q›,
🍋‹P ∨ Q›, 🍋‹P ⟶ Q›, 🍋‹∀x. P›, 🍋‹∃x. P›, 🍋‹∃! x. P›,
🍋‹THE x. P›.
🚫

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

\subsubsection*{Syntax}

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

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
@{term[source]"x \ y"} & 🍋‹x ≥ y› & (🍋‹>=›)\\
@{term[source]"x > y"} & 🍋‹x > y›\\
🍋‹∀x≤y. P› & @{term[source]"\x. x \ y \ P"}\\
🍋‹∃x≤y. P› & @{term[source]"\x. x \ y \ P"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
🍋‹LEAST x. P› & @{term[source]"Least (\x. P)"}\\
🍋‹GREATEST x. P› & @{term[source]"Greatest (\x. P)"}\\
\end{tabular}


\section*{Lattices}

Classes semilattice, lattice, distributive lattice and complete lattice (the
latter in theory 🍋‹HOL.Set›).

\begin{tabular}{@ {} l @ {~::~} l @ {}}
🍋‹Lattices.inf› & 🚫‹Lattices.inf›\\
🍋‹Lattices.sup› & 🚫‹Lattices.sup›\\
🍋‹Complete_Lattices.Inf› & @{term_type_only Complete_Lattices.Inf "'a set \ 'a::Inf"}\\
🍋‹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"} & 🍋‹x ≤ y›\\
@{text[source]"x \ y"} & 🍋‹x < y›\\
@{text[source]"x \ y"} & 🍋‹inf x y›\\
@{text[source]"x \ y"} & 🍋‹sup x y›\\
@{text[source]"\A"} & 🍋‹Inf A›\\
@{text[source]"\A"} & 🍋‹Sup A›\\
@{text[source]"\"} & @{term[source] top}\\
@{text[source]"\"} & @{term[source] bot}\\
\end{supertabular}


\section*{Set}

\begin{tabular}{@ {} l @ {~::~} l l @ {}}
🍋‹Set.empty› & @{term_type_only "Set.empty" "'a set"}\\
🍋‹Set.insert› & @{term_type_only insert "'a\'a set\'a set"}\\
🍋‹Collect› & @{term_type_only Collect "('a\bool)\'a set"}\\
🍋‹Set.member› & @{term_type_only Set.member "'a\'a set\bool"} & (🍋‹:›)\\
🍋‹Set.union› & @{term_type_only Set.union "'a set\'a set \ 'a set"} & (🍋‹Un›)\\
🍋‹Set.inter› & @{term_type_only Set.inter "'a set\'a set \ 'a set"} & (🍋‹Int›)\\
🍋‹Union› & @{term_type_only Union "'a set set\'a set"}\\
🍋‹Inter› & @{term_type_only Inter "'a set set\'a set"}\\
🍋‹Pow› & @{term_type_only Pow "'a set \'a set set"}\\
🍋‹UNIV› & @{term_type_only UNIV "'a set"}\\
🍋‹image› & @{term_type_only image "('a\'b)\'a set\'b set"}\\
🍋‹Ball› & @{term_type_only Ball "'a set\('a\bool)\bool"}\\
🍋‹Bex› & @{term_type_only Bex "'a set\('a\bool)\bool"}\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
‹{a🚫1,…,a🚫n}› & ‹insert a🚫1 (… (insert a🚫n {})…)›\\
🍋‹a ∉ A› & @{term[source]"\(x \ A)"}\\
🍋‹A ⊆ B› & @{term[source]"A \ B"}\\
🍋‹A ⊂ B› & @{term[source]"A < B"}\\
@{term[source]"A \ B"} & @{term[source]"B \ A"}\\
@{term[source]"A \ B"} & @{term[source]"B < A"}\\
🍋‹{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]"\((\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)"}\\
🍋‹∀x∈A. P› & @{term[source]"Ball A (\x. P)"}\\
🍋‹∃x∈A. P› & @{term[source]"Bex A (\x. P)"}\\
🍋‹range f› & @{term[source]"f ` UNIV"}\\
\end{tabular}


\section*{Fun}

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

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
🍋‹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 @ {}}
🍋‹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 @ {}}
🍋‹inv› & @{term[source]"inv_into UNIV"}
\end{tabular}

\section*{Fixed Points}

Theory: 🍋‹HOL.Inductive›.

Least and greatest fixed points in a complete lattice 🍋‹'a\:

\begin{tabular}{@ {} l @ {~::~} l @ {}}
🍋‹Inductive.lfp› & 🚫‹Inductive.lfp›\\
🍋‹Inductive.gfp› & 🚫‹Inductive.gfp›\\
\end{tabular}

Note that in particular sets (🍋‹'a \ bool\) are complete lattices.

\section*{Sum\_Type}

Type constructor ‹+›.

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


\section*{Product\_Type}

Types 🍋‹unit› and ‹×›.

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

Pairs may be nested. Nesting to the right is printed as a tuple,
e.g.\ \mbox{🍋‹(a,b,c)›} is really \mbox{‹(a, (b, c))›.}
Pattern matching with pairs and tuples extends to all binders,
e.g.\ \mbox{🍋‹∀(x,y)∈A. P›,} 🍋‹{(x,y). P}›, etc.


\section*{Relation}

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

\subsubsection*{Syntax}

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

\noindent
Type synonym \ 🍋‹'a rel\ \=\ @{expanded_typ "'a rel"}

\section*{Equiv\_Relations}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
🍋‹Equiv_Relations.equiv› & @{term_type_only Equiv_Relations.equiv "'a set \ ('a*'a)set\bool"}\\
🍋‹Equiv_Relations.quotient› & @{term_type_only Equiv_Relations.quotient "'a set \ ('a \ 'a) set \ 'a set set"}\\
🍋‹Equiv_Relations.congruent› & @{term_type_only Equiv_Relations.congruent "('a*'a)set\('a\'b)\bool"}\\
🍋‹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 @ {}}
🍋‹congruent r f› & @{term[source]"congruent r f"}\\
🍋‹congruent2 r r f› & @{term[source]"congruent2 r r f"}\\
\end{tabular}


\section*{Transitive\_Closure}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
🍋‹Transitive_Closure.rtrancl› & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\('a*'a)set"}\\
🍋‹Transitive_Closure.trancl› & @{term_type_only Transitive_Closure.trancl "('a*'a)set\('a*'a)set"}\\
🍋‹Transitive_Closure.reflcl› & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\('a*'a)set"}\\
🍋‹Transitive_Closure.acyclic› & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\bool"}\\
🍋‹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 @ {}}
🍋‹rtrancl r› & @{term[source]"rtrancl r"} & (🍋‹^*›)\\
🍋‹trancl r› & @{term[source]"trancl r"} & (🍋‹^+›)\\
🍋‹reflcl r› & @{term[source]"reflcl r"} & (🍋‹^=›)
\end{tabular}


\section*{Algebra}

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

\subsubsection*{Syntax}

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


\section*{Nat}

🚫‹nat›
🚫

\begin{tabular}{@ {} lllllll @ {}}
🍋‹(+) :: nat ==> nat ==> nat› &
🍋‹(-) :: nat ==> nat ==> nat› &
🍋‹(*) :: nat \<Rightarrow> nat \<Rightarrow> nat\<close> &
🍋‹(^) :: nat ==> nat ==> nat› &
🍋‹(div) :: nat ==> nat ==> nat›&
🍋‹(mod) :: nat ==> nat ==> nat›&
🍋‹(dvd) :: nat ==> nat ==> bool›\\
🍋‹(≤) :: nat ==> nat ==> bool› &
🍋‹(<) :: nat ==> nat ==> bool› &
🍋‹min :: nat ==> nat ==> nat› &
🍋‹max :: nat ==> nat ==> nat› &
🍋‹Min :: nat set ==> nat› &
🍋‹Max :: nat set ==> nat›\\
\end{tabular}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
🍋‹Nat.of_nat› & 🚫‹Nat.of_nat›\\
🍋‹(^^) :: ('a \ 'a) ==> nat ==> 'a \ 'a› &
  @{term_type_only "(^^) :: ('a \ 'a) \ nat \ 'a \ 'a" "('a \ 'a) \ nat \ 'a \ 'a"}
\end{tabular}

\section*{Int}

Type 🍋‹int›
🚫

\begin{tabular}{@ {} llllllll @ {}}
🍋‹(+) :: int ==> int ==> int› &
🍋‹(-) :: int ==> int ==> int› &
🍋‹uminus :: int ==> int› &
🍋‹(*) :: int \<Rightarrow> int \<Rightarrow> int\<close> &
🍋‹(^) :: int ==> nat ==> int› &
🍋‹(div) :: int ==> int ==> int›&
🍋‹(mod) :: int ==> int ==> int›&
🍋‹(dvd) :: int ==> int ==> bool›\\
🍋‹(≤) :: int ==> int ==> bool› &
🍋‹(<) :: int ==> int ==> bool› &
🍋‹min :: int ==> int ==> int› &
🍋‹max :: int ==> int ==> int› &
🍋‹Min :: int set ==> int› &
🍋‹Max :: int set ==> int›\\
🍋‹abs :: int ==> int› &
🍋‹sgn :: int ==> int›\\
\end{tabular}

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

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
🍋‹of_nat::nat==>int› & @{term[source]"of_nat"}\\
\end{tabular}


\section*{Finite\_Set}

\begin{tabular}{@ {} l @ {~::~} l @ {}}
🍋‹Finite_Set.finite› & @{term_type_only Finite_Set.finite "'a set\bool"}\\
🍋‹Finite_Set.card› & @{term_type_only Finite_Set.card "'a set \ nat"}\\
🍋‹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 @ {}}
🍋‹Lattices_Big.Min› & 🚫‹Lattices_Big.Min›\\
🍋‹Lattices_Big.Max› & 🚫‹Lattices_Big.Max›\\
🍋‹Lattices_Big.arg_min› & 🚫‹Lattices_Big.arg_min›\\
🍋‹Lattices_Big.is_arg_min› & 🚫‹Lattices_Big.is_arg_min›\\
🍋‹Lattices_Big.arg_max› & 🚫‹Lattices_Big.arg_max›\\
🍋‹Lattices_Big.is_arg_max› & 🚫‹Lattices_Big.is_arg_max›\\
\end{tabular}

\subsubsection*{Syntax}

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


\section*{Groups\_Big}

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


\section*{Wellfounded}

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


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

\begin{tabular}{@ {} l @ {~::~} l @ {}}
🍋‹lessThan› & @{term_type_only lessThan "'a::ord \ 'a set"}\\
🍋‹atMost› & @{term_type_only atMost "'a::ord \ 'a set"}\\
🍋‹greaterThan› & @{term_type_only greaterThan "'a::ord \ 'a set"}\\
🍋‹atLeast› & @{term_type_only atLeast "'a::ord \ 'a set"}\\
🍋‹greaterThanLessThan› & @{term_type_only greaterThanLessThan "'a::ord \ 'a \ 'a set"}\\
🍋‹atLeastLessThan› & @{term_type_only atLeastLessThan "'a::ord \ 'a \ 'a set"}\\
🍋‹greaterThanAtMost› & @{term_type_only greaterThanAtMost "'a::ord \ 'a \ 'a set"}\\
🍋‹atLeastAtMost› & @{term_type_only atLeastAtMost "'a::ord \ 'a \ 'a set"}\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
🍋‹lessThan y› & @{term[source] "lessThan y"}\\
🍋‹atMost y› & @{term[source] "atMost y"}\\
🍋‹greaterThan x› & @{term[source] "greaterThan x"}\\
🍋‹atLeast x› & @{term[source] "atLeast x"}\\
🍋‹greaterThanLessThan x y› & @{term[source] "greaterThanLessThan x y"}\\
🍋‹atLeastLessThan x y› & @{term[source] "atLeastLessThan x y"}\\
🍋‹greaterThanAtMost x y› & @{term[source] "greaterThanAtMost x y"}\\
🍋‹atLeastAtMost x y› & @{term[source] "atLeastAtMost x y"}\\
@{term[source] "\i\n. A"} & @{term[source] "\i \ {..n}. A"}\\
@{term[source] "\i} & @{term[source] "\i \ {..}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for ‹∩› instead of ‹∪›}\\
🍋‹sum (λx. t) {a..b}› & @{term[source] "sum (\x. t) {a..b}"}\\
🍋‹sum (λx. t) {a..<b}› & @{term[source] "sum (\x. t) {a..}\\
🍋‹sum (λx. t) {..b}› & @{term[source] "sum (\x. t) {..b}"}\\
🍋‹sum (λx. t) {..<b}› & @{term[source] "sum (\x. t) {..}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for ‹∏› instead of ‹∑›}\\
\end{tabular}


\section*{Power}

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


\section*{Option}

🚫‹option›
🚫

\begin{tabular}{@ {} l @ {~::~} l @ {}}
🍋‹Option.the› & 🚫‹Option.the›\\
🍋‹map_option› & @{typ[source]"('a \ 'b) \ 'a option \ 'b option"}\\
🍋‹set_option› & @{term_type_only set_option "'a option \ 'a set"}\\
🍋‹Option.bind› & @{term_type_only Option.bind "'a option \ ('a \ 'b option) \ 'b option"}
\end{tabular}

\section*{List}

🚫‹list›
🚫

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

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
‹[x🚫1,…,x🚫n]› & ‹x🚫1 # … # x🚫n # []›\\
🍋‹[m..<n]› & @{term[source]"upt m n"}\\
🍋‹[i..j]› & @{term[source]"upto i j"}\\
🍋‹xs[n := x]› & @{term[source]"list_update xs n x"}\\
🍋‹∑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 🍋‹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{tabular}{@ {} l @ {~::~} l @ {}}
🍋‹Map.empty› & 🚫‹Map.empty›\\
🍋‹Map.map_add› & 🚫‹Map.map_add›\\
🍋‹Map.map_comp› & 🚫‹Map.map_comp›\\
🍋‹Map.restrict_map› & @{term_type_only Map.restrict_map "('a\'b option)\'a set\('a\'b option)"}\\
🍋‹Map.dom› & @{term_type_only Map.dom "('a\'b option)\'a set"}\\
🍋‹Map.ran› & @{term_type_only Map.ran "('a\'b option)\'b set"}\\
🍋‹Map.map_le› & 🚫‹Map.map_le›\\
🍋‹Map.map_of› & 🚫‹Map.map_of›\\
🍋‹Map.map_upds› & 🚫‹Map.map_upds›\\
\end{tabular}

\subsubsection*{Syntax}

\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
🍋‹Map.empty› & @{term[source] "\_. None"}\\
🍋‹m(x:=Some y)› & @{term[source]"m(x:=Some y)"}\\
‹m(x🚫1↦y🚫1,…,x🚫n↦y🚫n)› & @{text[source]"m(x\<^sub>1\y\<^sub>1)\(x\<^sub>n\y\<^sub>n)"}\\
‹[x🚫1↦y🚫1,…,x🚫n↦y🚫n]› & @{text[source]"Map.empty(x\<^sub>1\y\<^sub>1,\,x\<^sub>n\y\<^sub>n)"}\\
🍋‹map_upds m xs ys› & @{term[source]"map_upds m xs ys"}\\
\end{tabular}

\section*{Infix operators in Main} % 🍋‹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
(*>*)