# HG changeset patch # User nipkow # Date 1236604807 -3600 # Node ID 3934d42344e01f88951574e22bd9ed88606141c7 # Parent 8befa897bebbaad4cfb4ffa4512558136f17b366 Docs diff -r 8befa897bebb -r 3934d42344e0 src/HOL/Docs/MainDoc.thy --- a/src/HOL/Docs/MainDoc.thy Mon Mar 09 12:24:19 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,503 +0,0 @@ -(*<*) -theory MainDoc -imports Main -begin - -ML {* -fun pretty_term_type_only ctxt (t, T) = - (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then () - else error "term_type_only: type mismatch"; - Syntax.pretty_typ ctxt T) - -val _ = ThyOutput.add_commands - [("term_type_only", ThyOutput.args (Args.term -- Args.typ_abbrev) (ThyOutput.output pretty_term_type_only))]; -*} -(*>*) -text{* - -\begin{abstract} -This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisicated class structure is only hinted at. -\end{abstract} - -\section{HOL} - -The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. - -Overloaded operators: - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{text "0"} & @{typeof HOL.zero}\\ -@{text "1"} & @{typeof HOL.one}\\ -@{const HOL.plus} & @{typeof HOL.plus}\\ -@{const HOL.minus} & @{typeof HOL.minus}\\ -@{const HOL.uminus} & @{typeof HOL.uminus}\\ -@{const HOL.times} & @{typeof HOL.times}\\ -@{const HOL.inverse} & @{typeof HOL.inverse}\\ -@{const HOL.divide} & @{typeof HOL.divide}\\ -@{const HOL.abs} & @{typeof HOL.abs}\\ -@{const HOL.sgn} & @{typeof HOL.sgn}\\ -@{const HOL.less_eq} & @{typeof HOL.less_eq}\\ -@{const HOL.less} & @{typeof HOL.less}\\ -@{const HOL.default} & @{typeof HOL.default}\\ -@{const HOL.undefined} & @{typeof HOL.undefined}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} 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\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\x. e\<^isub>2)"}\\ -@{term"abs x"} & @{term[source]"abs x"}\\ -@{term"uminus x"} & @{term[source]"uminus x"}\\ -\end{supertabular} - -\section{Orderings} - -A collection of classes constraining @{text"\"} and @{text"<"}: -preorders, partial orders, linear orders, dense linear orders and wellorders. - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Orderings.Least} & @{typeof Orderings.Least}\\ -@{const Orderings.min} & @{typeof Orderings.min}\\ -@{const Orderings.max} & @{typeof Orderings.max}\\ -@{const Orderings.mono} & @{typeof Orderings.mono}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term[source]"x \ y"} & @{term"x \ y"}\\ -@{term[source]"x > y"} & @{term"x > y"}\\ -@{term"ALL x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ -@{term"ALL xx. x < y \ P"}\\ -@{term"ALL x>=y. P"} & @{term[source]"\x. x \ y \ P"}\\ -@{term"ALL x>y. P"} & @{term[source]"\x. x > y \ P"}\\ -\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\"} instead of @{text"\"}}\\ -@{term"LEAST x. P"} & @{term[source]"Least (\x. P)"}\\ -\end{supertabular} - -\section{Set} - -Sets are predicates: @{text[source]"'a set = 'a \ bool"} -\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ -@{const insert} & @{term_type_only insert "'a\'a set\'a set"}\\ -@{const Collect} & @{term_type_only Collect "('a\bool)\'a set"}\\ -@{const "op :"} & @{term_type_only "op :" "'a\'a set\bool"} \qquad(\textsc{ascii} @{text":"})\\ -@{const Set.Un} & @{term_type_only Set.Un "'a set\'a set \ 'a set"} \qquad(\textsc{ascii} @{text"Un"})\\ -@{const Set.Int} & @{term_type_only Set.Int "'a set\'a set \ 'a set"} \qquad(\textsc{ascii} @{text"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 @ {}} -@{text"{x\<^isub>1,\,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\ (insert x\<^isub>n {})$"}\\ -@{term"x ~: A"} & @{term[source]"\(x \ A)"}\\ -@{term"A \ B"} & @{term[source]"A \ B"}\\ -@{term"A \ B"} & @{term[source]"A < B"}\\ -@{term[source]"A \ B"} & @{term[source]"B \ A"}\\ -@{term[source]"A \ B"} & @{term[source]"B < A"}\\ -@{term"{x. P}"} & @{term[source]"Collect(\x. P)"}\\ -@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\x. A)"}\\ -@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ -@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\x. A)"}\\ -@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\x. A)"}\\ -@{term"ALL x:A. P"} & @{term[source]"Ball A (\x. P)"}\\ -@{term"EX x:A. P"} & @{term[source]"Bex A (\x. P)"}\\ -@{term"range f"} & @{term[source]"f ` UNIV"}\\ -\end{supertabular} - - -\section{Fun} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const "Fun.id"} & @{typeof Fun.id}\\ -@{const "Fun.comp"} & @{typeof Fun.comp}\\ -@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\'b)\'a set\bool"}\\ -@{const "Fun.inj"} & @{typeof Fun.inj}\\ -@{const "Fun.surj"} & @{typeof Fun.surj}\\ -@{const "Fun.bij"} & @{typeof Fun.bij}\\ -@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\'b)\'a set\'b set\bool"}\\ -@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ -@{text"f(x\<^isub>1:=y\<^isub>1,\,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\(x\<^isub>n:=y\<^isub>n)"}\\ -\end{tabular} - - -\section{Fixed Points} - -Theory: @{theory Inductive}. - -Least and greatest fixed points in a complete lattice @{typ 'a}: - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ -@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ -\end{tabular} - -Note that in particular sets (@{typ"'a \ bool"}) are complete lattices. - -\section{Sum\_Type} - -Type constructor @{text"+"}. - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ -@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ -@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\'b set\('a+'b)set"} -\end{tabular} - - -\section{Product\_Type} - -Types @{typ unit} and @{text"\"}. - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ -@{const Pair} & @{typeof Pair}\\ -@{const fst} & @{typeof fst}\\ -@{const snd} & @{typeof snd}\\ -@{const split} & @{typeof split}\\ -@{const curry} & @{typeof curry}\\ -@{const Product_Type.Times} & @{typeof Product_Type.Times}\\ -@{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} l @ {}} -@{term"Pair a b"} & @{term[source]"Pair a b"}\\ -@{term"split (\x y. t)"} & @{term[source]"split (\x y. t)"}\\ -\end{tabular} - -Pairs may be nested. Nesting to the right is printed as a tuple, -e.g.\ \mbox{@{term"(a,b,c)"}} is really @{text"(a,(b,c))"}. -Pattern matching with pairs and tuples extends to all binders, -e.g.\ @{prop"ALL (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.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\('c*'a)set\('c*'b)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 @ {}} -@{term"converse r"} & @{term[source]"converse r"} -\end{tabular} - -\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"}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} 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 OrderedGroup} and @{theory Ring_and_Field} define a large -collection of classes describing common algebraic structures from semigroups -up to fields. Everything is done in terms of @{const plus}, @{const times} -and other overloaded operators. - - -\section{Nat} - -@{datatype nat} -\bigskip - -\begin{tabular}{@ {} lllllll @ {}} -@{term "op + :: nat \ nat \ nat"} & -@{term "op - :: nat \ nat \ nat"} & -@{term "op * :: nat \ nat \ nat"} & -@{term "op ^ :: nat \ nat \ nat"} & -@{term "op div :: nat \ nat \ nat"}& -@{term "op mod :: nat \ nat \ nat"}& -@{term "op dvd :: nat \ nat \ bool"}\\ -@{term "op \ :: nat \ nat \ bool"} & -@{term "op < :: nat \ nat \ bool"} & -@{term "min :: nat \ nat \ nat"} & -@{term "max :: nat \ nat \ nat"} & -@{term "Min :: nat set \ nat"} & -@{term "Max :: nat set \ nat"}\\ -\end{tabular} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Nat.of_nat} & @{typeof Nat.of_nat} -\end{tabular} - -\section{Int} - -Type @{typ int} -\bigskip - -\begin{tabular}{@ {} llllllll @ {}} -@{term "op + :: int \ int \ int"} & -@{term "op - :: int \ int \ int"} & -@{term "uminus :: int \ int"} & -@{term "op * :: int \ int \ int"} & -@{term "op ^ :: int \ nat \ int"} & -@{term "op div :: int \ int \ int"}& -@{term "op mod :: int \ int \ int"}& -@{term "op dvd :: int \ int \ bool"}\\ -@{term "op \ :: int \ int \ bool"} & -@{term "op < :: int \ int \ bool"} & -@{term "min :: int \ int \ int"} & -@{term "max :: int \ int \ int"} & -@{term "Min :: int set \ int"} & -@{term "Max :: int set \ int"}\\ -@{term "abs :: int \ int"} & -@{term "sgn :: int \ int"}\\ -\end{tabular} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{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"}\\ -\end{tabular} - -\subsubsection*{Syntax} - -\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"of_nat::nat\int"} & @{term[source]"of_nat"}\\ -\end{tabular} - - -\section{Wellfounded} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\bool"}\\ -@{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\bool"}\\ -@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\'a set"}\\ -@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\nat)\('a*'a)set"}\\ -@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\('b*'b)set\(('a*'b)*('a*'b))set"}\\ -@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\nat)\('a*'a)set\('a*'a)set"}\\ -@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ -@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ -\end{supertabular} - - -\section{SetInterval} - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const lessThan} & @{term_type_only lessThan "'a::ord \ 'a set"}\\ -@{const atMost} & @{term_type_only atMost "'a::ord \ 'a set"}\\ -@{const greaterThan} & @{term_type_only greaterThan "'a::ord \ 'a set"}\\ -@{const atLeast} & @{term_type_only atLeast "'a::ord \ 'a set"}\\ -@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \ 'a \ 'a set"}\\ -@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \ 'a \ 'a set"}\\ -@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \ 'a \ 'a set"}\\ -@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \ 'a \ 'a set"}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term "lessThan y"} & @{term[source] "lessThan y"}\\ -@{term "atMost y"} & @{term[source] "atMost y"}\\ -@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\ -@{term "atLeast x"} & @{term[source] "atLeast x"}\\ -@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\ -@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\ -@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\ -@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\ -@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\ i \ {..n}. A"}\\ -@{term[mode=xsymbols] "UN i:{.. i \ {.."} instead of @{text"\"}}\\ -@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\x. t) {a..b}"}\\ -@{term "setsum (%x. t) {a..x. t) {a.."} instead of @{text"\"}}\\ -\end{supertabular} - -??????? - -\section{Power} - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Power.power} & @{typeof Power.power} -\end{tabular} - - -\section{Iterated Functions and Relations} - -Theory: @{theory Relation_Power} - -Iterated functions \ @{term[source]"(f::'a\'a) ^ n"} \ -and relations \ @{term[source]"(r::('a\'a)set) ^ n"}. - - -\section{Option} - -@{datatype option} -\bigskip - -\begin{tabular}{@ {} l @ {~::~} l @ {}} -@{const Option.the} & @{typeof Option.the}\\ -@{const Option.map} & @{typ[source]"('a \ 'b) \ 'a option \ 'b option"}\\ -@{const Option.set} & @{term_type_only Option.set "'a option \ 'a set"} -\end{tabular} - -\section{List} - -@{datatype list} -\bigskip - -\begin{supertabular}{@ {} l @ {~::~} l @ {}} -@{const List.append} & @{typeof List.append}\\ -@{const List.butlast} & @{typeof List.butlast}\\ -@{const List.concat} & @{typeof List.concat}\\ -@{const List.distinct} & @{typeof List.distinct}\\ -@{const List.drop} & @{typeof List.drop}\\ -@{const List.dropWhile} & @{typeof List.dropWhile}\\ -@{const List.filter} & @{typeof List.filter}\\ -@{const List.foldl} & @{typeof List.foldl}\\ -@{const List.foldr} & @{typeof List.foldr}\\ -@{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*'a)set\('a list * 'a list)set"}\\ -@{const List.lists} & @{term_type_only List.lists "'a set\'a list set"}\\ -@{const List.listset} & @{term_type_only List.listset "'a set list \ 'a list set"}\\ -@{const List.listsum} & @{typeof List.listsum}\\ -@{const List.list_all2} & @{typeof List.list_all2}\\ -@{const List.list_update} & @{typeof List.list_update}\\ -@{const List.map} & @{typeof List.map}\\ -@{const List.measures} & @{term_type_only List.measures "('a\nat)list\('a*'a)set"}\\ -@{const List.remdups} & @{typeof List.remdups}\\ -@{const List.removeAll} & @{typeof List.removeAll}\\ -@{const List.remove1} & @{typeof List.remove1}\\ -@{const List.replicate} & @{typeof List.replicate}\\ -@{const List.rev} & @{typeof List.rev}\\ -@{const List.rotate} & @{typeof List.rotate}\\ -@{const List.rotate1} & @{typeof List.rotate1}\\ -@{const List.set} & @{term_type_only List.set "'a list \ 'a set"}\\ -@{const List.sort} & @{typeof List.sort}\\ -@{const List.sorted} & @{typeof List.sorted}\\ -@{const List.splice} & @{typeof List.splice}\\ -@{const List.sublist} & @{typeof List.sublist}\\ -@{const List.take} & @{typeof List.take}\\ -@{const List.takeWhile} & @{typeof List.takeWhile}\\ -@{const List.tl} & @{typeof List.tl}\\ -@{const List.upt} & @{typeof List.upt}\\ -@{const List.upto} & @{typeof List.upto}\\ -@{const List.zip} & @{typeof List.zip}\\ -\end{supertabular} - -\subsubsection*{Syntax} - -\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{text"[x\<^isub>1,\,x\<^isub>n]"} & @{text"x\<^isub>1 # \ # x\<^isub>n # []"}\\ -@{term"[m.. xs]"} & @{term"map (%x. e) xs"}\\ -@{term"[x \ xs. b]"} & @{term[source]"filter (\x. b) xs"} \\ -@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ -@{term"\x\xs. e"} & @{term[source]"listsum (map (\x. e) xs)"}\\ -\end{supertabular} -\medskip - -Comprehension: @{text"[e. q\<^isub>1, \, q\<^isub>n]"} where each -qualifier @{text q\<^isub>i} is either a generator @{text"pat \ e"} or a -guard, i.e.\ boolean expression. - -\section{Map} - -Maps model partial functions and are often used as finite tables. However, -the domain of a map may be infinite. - -@{text"'a \ 'b = 'a \ 'b option"} -\bigskip - -\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 @ {}} -@{text"empty"} & @{term"\x. None"}\\ -@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ -@{text"m(x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n)"} & @{text[source]"m(x\<^isub>1\y\<^isub>1)\(x\<^isub>n\y\<^isub>n)"}\\ -@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ -\end{tabular} - -*} -(*<*) -end -(*>*) \ No newline at end of file diff -r 8befa897bebb -r 3934d42344e0 src/HOL/Docs/Main_Doc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Docs/Main_Doc.thy Mon Mar 09 14:20:07 2009 +0100 @@ -0,0 +1,501 @@ +(*<*) +theory MainDoc +imports Main +begin + +ML {* +fun pretty_term_type_only ctxt (t, T) = + (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then () + else error "term_type_only: type mismatch"; + Syntax.pretty_typ ctxt T) + +val _ = ThyOutput.add_commands + [("term_type_only", ThyOutput.args (Args.term -- Args.typ_abbrev) (ThyOutput.output pretty_term_type_only))]; +*} +(*>*) +text{* + +\begin{abstract} +This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisicated class structure is only hinted at. +\end{abstract} + +\section{HOL} + +The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. + +Overloaded operators: + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{text "0"} & @{typeof HOL.zero}\\ +@{text "1"} & @{typeof HOL.one}\\ +@{const HOL.plus} & @{typeof HOL.plus}\\ +@{const HOL.minus} & @{typeof HOL.minus}\\ +@{const HOL.uminus} & @{typeof HOL.uminus}\\ +@{const HOL.times} & @{typeof HOL.times}\\ +@{const HOL.inverse} & @{typeof HOL.inverse}\\ +@{const HOL.divide} & @{typeof HOL.divide}\\ +@{const HOL.abs} & @{typeof HOL.abs}\\ +@{const HOL.sgn} & @{typeof HOL.sgn}\\ +@{const HOL.less_eq} & @{typeof HOL.less_eq}\\ +@{const HOL.less} & @{typeof HOL.less}\\ +@{const HOL.default} & @{typeof HOL.default}\\ +@{const HOL.undefined} & @{typeof HOL.undefined}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} 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\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\x. e\<^isub>2)"}\\ +@{term"abs x"} & @{term[source]"abs x"}\\ +@{term"uminus x"} & @{term[source]"uminus x"}\\ +\end{supertabular} + +\section{Orderings} + +A collection of classes constraining @{text"\"} and @{text"<"}: +preorders, partial orders, linear orders, dense linear orders and wellorders. + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Orderings.Least} & @{typeof Orderings.Least}\\ +@{const Orderings.min} & @{typeof Orderings.min}\\ +@{const Orderings.max} & @{typeof Orderings.max}\\ +@{const Orderings.mono} & @{typeof Orderings.mono}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term[source]"x \ y"} & @{term"x \ y"}\\ +@{term[source]"x > y"} & @{term"x > y"}\\ +@{term"ALL x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ +\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$, and for @{text"\"}}\\ +@{term"LEAST x. P"} & @{term[source]"Least (\x. P)"}\\ +\end{supertabular} + +\section{Set} + +Sets are predicates: @{text[source]"'a set = 'a \ bool"} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ +@{const insert} & @{term_type_only insert "'a\'a set\'a set"}\\ +@{const Collect} & @{term_type_only Collect "('a\bool)\'a set"}\\ +@{const "op :"} & @{term_type_only "op :" "'a\'a set\bool"} \qquad(\textsc{ascii} @{text":"})\\ +@{const Set.Un} & @{term_type_only Set.Un "'a set\'a set \ 'a set"} \qquad(\textsc{ascii} @{text"Un"})\\ +@{const Set.Int} & @{term_type_only Set.Int "'a set\'a set \ 'a set"} \qquad(\textsc{ascii} @{text"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 @ {}} +@{text"{x\<^isub>1,\,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\ (insert x\<^isub>n {})$"}\\ +@{term"x ~: A"} & @{term[source]"\(x \ A)"}\\ +@{term"A \ B"} & @{term[source]"A \ B"}\\ +@{term"A \ B"} & @{term[source]"A < B"}\\ +@{term[source]"A \ B"} & @{term[source]"B \ A"}\\ +@{term[source]"A \ B"} & @{term[source]"B < A"}\\ +@{term"{x. P}"} & @{term[source]"Collect(\x. P)"}\\ +@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\x. A)"}\\ +@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ +@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\x. A)"}\\ +@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\x. A)"}\\ +@{term"ALL x:A. P"} & @{term[source]"Ball A (\x. P)"}\\ +@{term"EX x:A. P"} & @{term[source]"Bex A (\x. P)"}\\ +@{term"range f"} & @{term[source]"f ` UNIV"}\\ +\end{supertabular} + + +\section{Fun} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const "Fun.id"} & @{typeof Fun.id}\\ +@{const "Fun.comp"} & @{typeof Fun.comp}\\ +@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\'b)\'a set\bool"}\\ +@{const "Fun.inj"} & @{typeof Fun.inj}\\ +@{const "Fun.surj"} & @{typeof Fun.surj}\\ +@{const "Fun.bij"} & @{typeof Fun.bij}\\ +@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\'b)\'a set\'b set\bool"}\\ +@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ +@{text"f(x\<^isub>1:=y\<^isub>1,\,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\(x\<^isub>n:=y\<^isub>n)"}\\ +\end{tabular} + + +\section{Fixed Points} + +Theory: @{theory Inductive}. + +Least and greatest fixed points in a complete lattice @{typ 'a}: + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ +@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ +\end{tabular} + +Note that in particular sets (@{typ"'a \ bool"}) are complete lattices. + +\section{Sum\_Type} + +Type constructor @{text"+"}. + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ +@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ +@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\'b set\('a+'b)set"} +\end{tabular} + + +\section{Product\_Type} + +Types @{typ unit} and @{text"\"}. + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ +@{const Pair} & @{typeof Pair}\\ +@{const fst} & @{typeof fst}\\ +@{const snd} & @{typeof snd}\\ +@{const split} & @{typeof split}\\ +@{const curry} & @{typeof curry}\\ +@{const Product_Type.Times} & @{typeof Product_Type.Times}\\ +@{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} l @ {}} +@{term"Pair a b"} & @{term[source]"Pair a b"}\\ +@{term"split (\x y. t)"} & @{term[source]"split (\x y. t)"}\\ +\end{tabular} + +Pairs may be nested. Nesting to the right is printed as a tuple, +e.g.\ \mbox{@{term"(a,b,c)"}} is really @{text"(a,(b,c))"}. +Pattern matching with pairs and tuples extends to all binders, +e.g.\ @{prop"ALL (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.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\('c*'a)set\('c*'b)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 @ {}} +@{term"converse r"} & @{term[source]"converse r"} +\end{tabular} + +\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"}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} 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 OrderedGroup} and @{theory Ring_and_Field} define a large +collection of classes describing common algebraic structures from semigroups +up to fields. Everything is done in terms of @{const plus}, @{const times} +and other overloaded operators. + + +\section{Nat} + +@{datatype nat} +\bigskip + +\begin{tabular}{@ {} lllllll @ {}} +@{term "op + :: nat \ nat \ nat"} & +@{term "op - :: nat \ nat \ nat"} & +@{term "op * :: nat \ nat \ nat"} & +@{term "op ^ :: nat \ nat \ nat"} & +@{term "op div :: nat \ nat \ nat"}& +@{term "op mod :: nat \ nat \ nat"}& +@{term "op dvd :: nat \ nat \ bool"}\\ +@{term "op \ :: nat \ nat \ bool"} & +@{term "op < :: nat \ nat \ bool"} & +@{term "min :: nat \ nat \ nat"} & +@{term "max :: nat \ nat \ nat"} & +@{term "Min :: nat set \ nat"} & +@{term "Max :: nat set \ nat"}\\ +\end{tabular} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Nat.of_nat} & @{typeof Nat.of_nat} +\end{tabular} + +\section{Int} + +Type @{typ int} +\bigskip + +\begin{tabular}{@ {} llllllll @ {}} +@{term "op + :: int \ int \ int"} & +@{term "op - :: int \ int \ int"} & +@{term "uminus :: int \ int"} & +@{term "op * :: int \ int \ int"} & +@{term "op ^ :: int \