1(*<*) 2theory Main_Doc 3imports Main 4begin 5 6setup \<open> 7 Thy_Output.antiquotation_pretty_source @{binding term_type_only} (Args.term -- Args.typ_abbrev) 8 (fn ctxt => fn (t, T) => 9 (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () 10 else error "term_type_only: type mismatch"; 11 Syntax.pretty_typ ctxt T)) 12\<close> 13setup \<open> 14 Thy_Output.antiquotation_pretty_source @{binding expanded_typ} Args.typ 15 Syntax.pretty_typ 16\<close> 17(*>*) 18text\<open> 19 20\begin{abstract} 21This 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 \<^url>\<open>https://isabelle.in.tum.de/library/HOL\<close>. 22\end{abstract} 23 24\section*{HOL} 25 26The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop "\<not> P"}, @{prop"P \<and> Q"}, 27@{prop "P \<or> Q"}, @{prop "P \<longrightarrow> Q"}, @{prop "\<forall>x. P"}, @{prop "\<exists>x. P"}, @{prop"\<exists>! x. P"}, 28@{term"THE x. P"}. 29\<^smallskip> 30 31\begin{tabular}{@ {} l @ {~::~} l @ {}} 32@{const HOL.undefined} & @{typeof HOL.undefined}\\ 33@{const HOL.default} & @{typeof HOL.default}\\ 34\end{tabular} 35 36\subsubsection*{Syntax} 37 38\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 39@{term"\<not> (x = y)"} & @{term[source]"\<not> (x = y)"} & (\<^verbatim>\<open>~=\<close>)\\ 40@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\ 41@{term"If x y z"} & @{term[source]"If x y z"}\\ 42@{term"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"} & @{term[source]"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"}\\ 43\end{supertabular} 44 45 46\section*{Orderings} 47 48A collection of classes defining basic orderings: 49preorder, partial order, linear order, dense linear order and wellorder. 50\<^smallskip> 51 52\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 53@{const Orderings.less_eq} & @{typeof Orderings.less_eq} & (\<^verbatim>\<open><=\<close>)\\ 54@{const Orderings.less} & @{typeof Orderings.less}\\ 55@{const Orderings.Least} & @{typeof Orderings.Least}\\ 56@{const Orderings.Greatest} & @{typeof Orderings.Greatest}\\ 57@{const Orderings.min} & @{typeof Orderings.min}\\ 58@{const Orderings.max} & @{typeof Orderings.max}\\ 59@{const[source] top} & @{typeof Orderings.top}\\ 60@{const[source] bot} & @{typeof Orderings.bot}\\ 61@{const Orderings.mono} & @{typeof Orderings.mono}\\ 62@{const Orderings.strict_mono} & @{typeof Orderings.strict_mono}\\ 63\end{supertabular} 64 65\subsubsection*{Syntax} 66 67\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 68@{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\<^verbatim>\<open>>=\<close>)\\ 69@{term[source]"x > y"} & @{term"x > y"}\\ 70@{term "\<forall>x\<le>y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\ 71@{term "\<exists>x\<le>y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\ 72\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ 73@{term "LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\ 74@{term "GREATEST x. P"} & @{term[source]"Greatest (\<lambda>x. P)"}\\ 75\end{supertabular} 76 77 78\section*{Lattices} 79 80Classes semilattice, lattice, distributive lattice and complete lattice (the 81latter in theory @{theory HOL.Set}). 82 83\begin{tabular}{@ {} l @ {~::~} l @ {}} 84@{const Lattices.inf} & @{typeof Lattices.inf}\\ 85@{const Lattices.sup} & @{typeof Lattices.sup}\\ 86@{const Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\ 87@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \<Rightarrow> 'a::Sup"}\\ 88\end{tabular} 89 90\subsubsection*{Syntax} 91 92Available by loading theory \<open>Lattice_Syntax\<close> in directory \<open>Library\<close>. 93 94\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 95@{text[source]"x \<sqsubseteq> y"} & @{term"x \<le> y"}\\ 96@{text[source]"x \<sqsubset> y"} & @{term"x < y"}\\ 97@{text[source]"x \<sqinter> y"} & @{term"inf x y"}\\ 98@{text[source]"x \<squnion> y"} & @{term"sup x y"}\\ 99@{text[source]"\<Sqinter>A"} & @{term"Inf A"}\\ 100@{text[source]"\<Squnion>A"} & @{term"Sup A"}\\ 101@{text[source]"\<top>"} & @{term[source] top}\\ 102@{text[source]"\<bottom>"} & @{term[source] bot}\\ 103\end{supertabular} 104 105 106\section*{Set} 107 108\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 109@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\ 110@{const Set.insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\ 111@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\ 112@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\<^verbatim>\<open>:\<close>)\\ 113@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Un\<close>)\\ 114@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Int\<close>)\\ 115@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ 116@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\ 117@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\ 118@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\ 119@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\ 120@{const UNIV} & @{term_type_only UNIV "'a set"}\\ 121@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\ 122@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ 123@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\ 124\end{supertabular} 125 126\subsubsection*{Syntax} 127 128\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 129\<open>{a\<^sub>1,\<dots>,a\<^sub>n}\<close> & \<open>insert a\<^sub>1 (\<dots> (insert a\<^sub>n {})\<dots>)\<close>\\ 130@{term "a \<notin> A"} & @{term[source]"\<not>(x \<in> A)"}\\ 131@{term "A \<subseteq> B"} & @{term[source]"A \<le> B"}\\ 132@{term "A \<subset> B"} & @{term[source]"A < B"}\\ 133@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\ 134@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\ 135@{term "{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\ 136\<open>{t | x\<^sub>1 \<dots> x\<^sub>n. P}\<close> & \<open>{v. \<exists>x\<^sub>1 \<dots> x\<^sub>n. v = t \<and> P}\<close>\\ 137@{term[source]"\<Union>x\<in>I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\ 138@{term[source]"\<Union>x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\ 139@{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\ 140@{term[source]"\<Inter>x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\ 141@{term "\<forall>x\<in>A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\ 142@{term "\<exists>x\<in>A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\ 143@{term "range f"} & @{term[source]"f ` UNIV"}\\ 144\end{supertabular} 145 146 147\section*{Fun} 148 149\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 150@{const "Fun.id"} & @{typeof Fun.id}\\ 151@{const "Fun.comp"} & @{typeof Fun.comp} & (\texttt{o})\\ 152@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\ 153@{const "Fun.inj"} & @{typeof Fun.inj}\\ 154@{const "Fun.surj"} & @{typeof Fun.surj}\\ 155@{const "Fun.bij"} & @{typeof Fun.bij}\\ 156@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\ 157@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ 158\end{supertabular} 159 160\subsubsection*{Syntax} 161 162\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 163@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ 164\<open>f(x\<^sub>1:=y\<^sub>1,\<dots>,x\<^sub>n:=y\<^sub>n)\<close> & \<open>f(x\<^sub>1:=y\<^sub>1)\<dots>(x\<^sub>n:=y\<^sub>n)\<close>\\ 165\end{tabular} 166 167 168\section*{Hilbert\_Choice} 169 170Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}. 171\<^smallskip> 172 173\begin{tabular}{@ {} l @ {~::~} l @ {}} 174@{const Hilbert_Choice.inv_into} & @{term_type_only Hilbert_Choice.inv_into "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"} 175\end{tabular} 176 177\subsubsection*{Syntax} 178 179\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 180@{term inv} & @{term[source]"inv_into UNIV"} 181\end{tabular} 182 183\section*{Fixed Points} 184 185Theory: @{theory HOL.Inductive}. 186 187Least and greatest fixed points in a complete lattice @{typ 'a}: 188 189\begin{tabular}{@ {} l @ {~::~} l @ {}} 190@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ 191@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ 192\end{tabular} 193 194Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices. 195 196\section*{Sum\_Type} 197 198Type constructor \<open>+\<close>. 199 200\begin{tabular}{@ {} l @ {~::~} l @ {}} 201@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ 202@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ 203@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"} 204\end{tabular} 205 206 207\section*{Product\_Type} 208 209Types @{typ unit} and \<open>\<times>\<close>. 210 211\begin{supertabular}{@ {} l @ {~::~} l @ {}} 212@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ 213@{const Pair} & @{typeof Pair}\\ 214@{const fst} & @{typeof fst}\\ 215@{const snd} & @{typeof snd}\\ 216@{const case_prod} & @{typeof case_prod}\\ 217@{const curry} & @{typeof curry}\\ 218@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\ 219\end{supertabular} 220 221\subsubsection*{Syntax} 222 223\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} 224@{term "Pair a b"} & @{term[source]"Pair a b"}\\ 225@{term "case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\ 226@{term "A \<times> B"} & \<open>Sigma A (\<lambda>\<^latex>\<open>\_\<close>. B)\<close> 227\end{tabular} 228 229Pairs may be nested. Nesting to the right is printed as a tuple, 230e.g.\ \mbox{@{term "(a,b,c)"}} is really \mbox{\<open>(a, (b, c))\<close>.} 231Pattern matching with pairs and tuples extends to all binders, 232e.g.\ \mbox{@{prop "\<forall>(x,y)\<in>A. P"},} @{term "{(x,y). P}"}, etc. 233 234 235\section*{Relation} 236 237\begin{tabular}{@ {} l @ {~::~} l @ {}} 238@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\ 239@{const Relation.relcomp} & @{term_type_only Relation.relcomp "('a*'b)set\<Rightarrow>('b*'c)set\<Rightarrow>('a*'c)set"}\\ 240@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\ 241@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\ 242@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\ 243@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\ 244@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\ 245@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\ 246@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\ 247@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ 248@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\ 249@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\ 250@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\ 251@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\ 252@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\ 253@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\ 254@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\ 255\end{tabular} 256 257\subsubsection*{Syntax} 258 259\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 260@{term"converse r"} & @{term[source]"converse r"} & (\<^verbatim>\<open>^-1\<close>) 261\end{tabular} 262\<^medskip> 263 264\noindent 265Type synonym \ @{typ"'a rel"} \<open>=\<close> @{expanded_typ "'a rel"} 266 267\section*{Equiv\_Relations} 268 269\begin{supertabular}{@ {} l @ {~::~} l @ {}} 270@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\ 271@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\ 272@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\ 273@{const Equiv_Relations.congruent2} & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>('a\<Rightarrow>'b\<Rightarrow>'c)\<Rightarrow>bool"}\\ 274%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ 275\end{supertabular} 276 277\subsubsection*{Syntax} 278 279\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 280@{term"congruent r f"} & @{term[source]"congruent r f"}\\ 281@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\ 282\end{tabular} 283 284 285\section*{Transitive\_Closure} 286 287\begin{tabular}{@ {} l @ {~::~} l @ {}} 288@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ 289@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ 290@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\ 291@{const Transitive_Closure.acyclic} & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\<Rightarrow>bool"}\\ 292@{const compower} & @{term_type_only "(^^) :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\ 293\end{tabular} 294 295\subsubsection*{Syntax} 296 297\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 298@{term"rtrancl r"} & @{term[source]"rtrancl r"} & (\<^verbatim>\<open>^*\<close>)\\ 299@{term"trancl r"} & @{term[source]"trancl r"} & (\<^verbatim>\<open>^+\<close>)\\ 300@{term"reflcl r"} & @{term[source]"reflcl r"} & (\<^verbatim>\<open>^=\<close>) 301\end{tabular} 302 303 304\section*{Algebra} 305 306Theories @{theory HOL.Groups}, @{theory HOL.Rings}, @{theory HOL.Fields} and @{theory 307HOL.Divides} define a large collection of classes describing common algebraic 308structures from semigroups up to fields. Everything is done in terms of 309overloaded operators: 310 311\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 312\<open>0\<close> & @{typeof zero}\\ 313\<open>1\<close> & @{typeof one}\\ 314@{const plus} & @{typeof plus}\\ 315@{const minus} & @{typeof minus}\\ 316@{const uminus} & @{typeof uminus} & (\<^verbatim>\<open>-\<close>)\\ 317@{const times} & @{typeof times}\\ 318@{const inverse} & @{typeof inverse}\\ 319@{const divide} & @{typeof divide}\\ 320@{const abs} & @{typeof abs}\\ 321@{const sgn} & @{typeof sgn}\\ 322@{const Rings.dvd} & @{typeof Rings.dvd}\\ 323@{const divide} & @{typeof divide}\\ 324@{const modulo} & @{typeof modulo}\\ 325\end{supertabular} 326 327\subsubsection*{Syntax} 328 329\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 330@{term "\<bar>x\<bar>"} & @{term[source] "abs x"} 331\end{tabular} 332 333 334\section*{Nat} 335 336@{datatype nat} 337\<^bigskip> 338 339\begin{tabular}{@ {} lllllll @ {}} 340@{term "(+) :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 341@{term "(-) :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 342@{term "( * ) :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 343@{term "(^) :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 344@{term "(div) :: nat \<Rightarrow> nat \<Rightarrow> nat"}& 345@{term "(mod) :: nat \<Rightarrow> nat \<Rightarrow> nat"}& 346@{term "(dvd) :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\ 347@{term "(\<le>) :: nat \<Rightarrow> nat \<Rightarrow> bool"} & 348@{term "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool"} & 349@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 350@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} & 351@{term "Min :: nat set \<Rightarrow> nat"} & 352@{term "Max :: nat set \<Rightarrow> nat"}\\ 353\end{tabular} 354 355\begin{tabular}{@ {} l @ {~::~} l @ {}} 356@{const Nat.of_nat} & @{typeof Nat.of_nat}\\ 357@{term "(^^) :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} & 358 @{term_type_only "(^^) :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} 359\end{tabular} 360 361\section*{Int} 362 363Type @{typ int} 364\<^bigskip> 365 366\begin{tabular}{@ {} llllllll @ {}} 367@{term "(+) :: int \<Rightarrow> int \<Rightarrow> int"} & 368@{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} & 369@{term "uminus :: int \<Rightarrow> int"} & 370@{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} & 371@{term "(^) :: int \<Rightarrow> nat \<Rightarrow> int"} & 372@{term "(div) :: int \<Rightarrow> int \<Rightarrow> int"}& 373@{term "(mod) :: int \<Rightarrow> int \<Rightarrow> int"}& 374@{term "(dvd) :: int \<Rightarrow> int \<Rightarrow> bool"}\\ 375@{term "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"} & 376@{term "(<) :: int \<Rightarrow> int \<Rightarrow> bool"} & 377@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} & 378@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} & 379@{term "Min :: int set \<Rightarrow> int"} & 380@{term "Max :: int set \<Rightarrow> int"}\\ 381@{term "abs :: int \<Rightarrow> int"} & 382@{term "sgn :: int \<Rightarrow> int"}\\ 383\end{tabular} 384 385\begin{tabular}{@ {} l @ {~::~} l l @ {}} 386@{const Int.nat} & @{typeof Int.nat}\\ 387@{const Int.of_int} & @{typeof Int.of_int}\\ 388@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"} & (\<^verbatim>\<open>Ints\<close>) 389\end{tabular} 390 391\subsubsection*{Syntax} 392 393\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 394@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\ 395\end{tabular} 396 397 398\section*{Finite\_Set} 399 400\begin{supertabular}{@ {} l @ {~::~} l @ {}} 401@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\ 402@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set \<Rightarrow> nat"}\\ 403@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\ 404\end{supertabular} 405 406 407\section*{Lattices\_Big} 408 409\begin{supertabular}{@ {} l @ {~::~} l l @ {}} 410@{const Lattices_Big.Min} & @{typeof Lattices_Big.Min}\\ 411@{const Lattices_Big.Max} & @{typeof Lattices_Big.Max}\\ 412@{const Lattices_Big.arg_min} & @{typeof Lattices_Big.arg_min}\\ 413@{const Lattices_Big.is_arg_min} & @{typeof Lattices_Big.is_arg_min}\\ 414@{const Lattices_Big.arg_max} & @{typeof Lattices_Big.arg_max}\\ 415@{const Lattices_Big.is_arg_max} & @{typeof Lattices_Big.is_arg_max}\\ 416\end{supertabular} 417 418\subsubsection*{Syntax} 419 420\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 421@{term "ARG_MIN f x. P"} & @{term[source]"arg_min f (\<lambda>x. P)"}\\ 422@{term "ARG_MAX f x. P"} & @{term[source]"arg_max f (\<lambda>x. P)"}\\ 423\end{supertabular} 424 425 426\section*{Groups\_Big} 427 428\begin{supertabular}{@ {} l @ {~::~} l @ {}} 429@{const Groups_Big.sum} & @{term_type_only Groups_Big.sum "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_add"}\\ 430@{const Groups_Big.prod} & @{term_type_only Groups_Big.prod "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_mult"}\\ 431\end{supertabular} 432 433 434\subsubsection*{Syntax} 435 436\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} 437@{term "sum (\<lambda>x. x) A"} & @{term[source]"sum (\<lambda>x. x) A"} & (\<^verbatim>\<open>SUM\<close>)\\ 438@{term "sum (\<lambda>x. t) A"} & @{term[source]"sum (\<lambda>x. t) A"}\\ 439@{term[source] "\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\ 440\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>} & (\<^verbatim>\<open>PROD\<close>)\\ 441\end{supertabular} 442 443 444\section*{Wellfounded} 445 446\begin{supertabular}{@ {} l @ {~::~} l @ {}} 447@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\ 448@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\ 449@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\ 450@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\ 451@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\ 452@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ 453@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ 454\end{supertabular} 455 456 457\section*{Set\_Interval} % @{theory HOL.Set_Interval} 458 459\begin{supertabular}{@ {} l @ {~::~} l @ {}} 460@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\ 461@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\ 462@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\ 463@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\ 464@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 465@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 466@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 467@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\ 468\end{supertabular} 469 470\subsubsection*{Syntax} 471 472\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 473@{term "lessThan y"} & @{term[source] "lessThan y"}\\ 474@{term "atMost y"} & @{term[source] "atMost y"}\\ 475@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\ 476@{term "atLeast x"} & @{term[source] "atLeast x"}\\ 477@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\ 478@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\ 479@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\ 480@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\ 481@{term[source] "\<Union>i\<le>n. A"} & @{term[source] "\<Union>i \<in> {..n}. A"}\\ 482@{term[source] "\<Union>i<n. A"} & @{term[source] "\<Union>i \<in> {..<n}. A"}\\ 483\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Inter>\<close> instead of \<open>\<Union>\<close>}\\ 484@{term "sum (\<lambda>x. t) {a..b}"} & @{term[source] "sum (\<lambda>x. t) {a..b}"}\\ 485@{term "sum (\<lambda>x. t) {a..<b}"} & @{term[source] "sum (\<lambda>x. t) {a..<b}"}\\ 486@{term "sum (\<lambda>x. t) {..b}"} & @{term[source] "sum (\<lambda>x. t) {..b}"}\\ 487@{term "sum (\<lambda>x. t) {..<b}"} & @{term[source] "sum (\<lambda>x. t) {..<b}"}\\ 488\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>}\\ 489\end{supertabular} 490 491 492\section*{Power} 493 494\begin{tabular}{@ {} l @ {~::~} l @ {}} 495@{const Power.power} & @{typeof Power.power} 496\end{tabular} 497 498 499\section*{Option} 500 501@{datatype option} 502\<^bigskip> 503 504\begin{tabular}{@ {} l @ {~::~} l @ {}} 505@{const Option.the} & @{typeof Option.the}\\ 506@{const map_option} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\ 507@{const set_option} & @{term_type_only set_option "'a option \<Rightarrow> 'a set"}\\ 508@{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"} 509\end{tabular} 510 511\section*{List} 512 513@{datatype list} 514\<^bigskip> 515 516\begin{supertabular}{@ {} l @ {~::~} l @ {}} 517@{const List.append} & @{typeof List.append}\\ 518@{const List.butlast} & @{typeof List.butlast}\\ 519@{const List.concat} & @{typeof List.concat}\\ 520@{const List.distinct} & @{typeof List.distinct}\\ 521@{const List.drop} & @{typeof List.drop}\\ 522@{const List.dropWhile} & @{typeof List.dropWhile}\\ 523@{const List.filter} & @{typeof List.filter}\\ 524@{const List.find} & @{typeof List.find}\\ 525@{const List.fold} & @{typeof List.fold}\\ 526@{const List.foldr} & @{typeof List.foldr}\\ 527@{const List.foldl} & @{typeof List.foldl}\\ 528@{const List.hd} & @{typeof List.hd}\\ 529@{const List.last} & @{typeof List.last}\\ 530@{const List.length} & @{typeof List.length}\\ 531@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 532@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 533@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\ 534@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 535@{const List.listrel} & @{term_type_only List.listrel "('a*'b)set\<Rightarrow>('a list * 'b list)set"}\\ 536@{const List.listrel1} & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\ 537@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\ 538@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\ 539@{const Groups_List.sum_list} & @{typeof Groups_List.sum_list}\\ 540@{const Groups_List.prod_list} & @{typeof Groups_List.prod_list}\\ 541@{const List.list_all2} & @{typeof List.list_all2}\\ 542@{const List.list_update} & @{typeof List.list_update}\\ 543@{const List.map} & @{typeof List.map}\\ 544@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\ 545@{const List.nth} & @{typeof List.nth}\\ 546@{const List.nths} & @{typeof List.nths}\\ 547@{const List.remdups} & @{typeof List.remdups}\\ 548@{const List.removeAll} & @{typeof List.removeAll}\\ 549@{const List.remove1} & @{typeof List.remove1}\\ 550@{const List.replicate} & @{typeof List.replicate}\\ 551@{const List.rev} & @{typeof List.rev}\\ 552@{const List.rotate} & @{typeof List.rotate}\\ 553@{const List.rotate1} & @{typeof List.rotate1}\\ 554@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\ 555@{const List.shuffle} & @{typeof List.shuffle}\\ 556@{const List.sort} & @{typeof List.sort}\\ 557@{const List.sorted} & @{typeof List.sorted}\\ 558@{const List.sorted_wrt} & @{typeof List.sorted_wrt}\\ 559@{const List.splice} & @{typeof List.splice}\\ 560@{const List.take} & @{typeof List.take}\\ 561@{const List.takeWhile} & @{typeof List.takeWhile}\\ 562@{const List.tl} & @{typeof List.tl}\\ 563@{const List.upt} & @{typeof List.upt}\\ 564@{const List.upto} & @{typeof List.upto}\\ 565@{const List.zip} & @{typeof List.zip}\\ 566\end{supertabular} 567 568\subsubsection*{Syntax} 569 570\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 571\<open>[x\<^sub>1,\<dots>,x\<^sub>n]\<close> & \<open>x\<^sub>1 # \<dots> # x\<^sub>n # []\<close>\\ 572@{term"[m..<n]"} & @{term[source]"upt m n"}\\ 573@{term"[i..j]"} & @{term[source]"upto i j"}\\ 574@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ 575@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\ 576\end{supertabular} 577\<^medskip> 578 579Filter input syntax \<open>[pat \<leftarrow> e. b]\<close>, where 580\<open>pat\<close> is a tuple pattern, which stands for @{term "filter (\<lambda>pat. b) e"}. 581 582List comprehension input syntax: \<open>[e. q\<^sub>1, \<dots>, q\<^sub>n]\<close> where each 583qualifier \<open>q\<^sub>i\<close> is either a generator \mbox{\<open>pat \<leftarrow> e\<close>} or a 584guard, i.e.\ boolean expression. 585 586\section*{Map} 587 588Maps model partial functions and are often used as finite tables. However, 589the domain of a map may be infinite. 590 591\begin{supertabular}{@ {} l @ {~::~} l @ {}} 592@{const Map.empty} & @{typeof Map.empty}\\ 593@{const Map.map_add} & @{typeof Map.map_add}\\ 594@{const Map.map_comp} & @{typeof Map.map_comp}\\ 595@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\ 596@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\ 597@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\ 598@{const Map.map_le} & @{typeof Map.map_le}\\ 599@{const Map.map_of} & @{typeof Map.map_of}\\ 600@{const Map.map_upds} & @{typeof Map.map_upds}\\ 601\end{supertabular} 602 603\subsubsection*{Syntax} 604 605\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} 606@{term"Map.empty"} & @{term"\<lambda>x. None"}\\ 607@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ 608\<open>m(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)\<close> & @{text[source]"m(x\<^sub>1\<mapsto>y\<^sub>1)\<dots>(x\<^sub>n\<mapsto>y\<^sub>n)"}\\ 609\<open>[x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n]\<close> & @{text[source]"Map.empty(x\<^sub>1\<mapsto>y\<^sub>1,\<dots>,x\<^sub>n\<mapsto>y\<^sub>n)"}\\ 610@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ 611\end{tabular} 612 613\section*{Infix operators in Main} % @{theory Main} 614 615\begin{center} 616\begin{tabular}{llll} 617 & Operator & precedence & associativity \\ 618\hline 619Meta-logic & \<open>\<Longrightarrow>\<close> & 1 & right \\ 620& \<open>\<equiv>\<close> & 2 \\ 621\hline 622Logic & \<open>\<and>\<close> & 35 & right \\ 623&\<open>\<or>\<close> & 30 & right \\ 624&\<open>\<longrightarrow>\<close>, \<open>\<longleftrightarrow>\<close> & 25 & right\\ 625&\<open>=\<close>, \<open>\<noteq>\<close> & 50 & left\\ 626\hline 627Orderings & \<open>\<le>\<close>, \<open><\<close>, \<open>\<ge>\<close>, \<open>>\<close> & 50 \\ 628\hline 629Sets & \<open>\<subseteq>\<close>, \<open>\<subset>\<close>, \<open>\<supseteq>\<close>, \<open>\<supset>\<close> & 50 \\ 630&\<open>\<in>\<close>, \<open>\<notin>\<close> & 50 \\ 631&\<open>\<inter>\<close> & 70 & left \\ 632&\<open>\<union>\<close> & 65 & left \\ 633\hline 634Functions and Relations & \<open>\<circ>\<close> & 55 & left\\ 635&\<open>`\<close> & 90 & right\\ 636&\<open>O\<close> & 75 & right\\ 637&\<open>``\<close> & 90 & right\\ 638&\<open>^^\<close> & 80 & right\\ 639\hline 640Numbers & \<open>+\<close>, \<open>-\<close> & 65 & left \\ 641&\<open>*\<close>, \<open>/\<close> & 70 & left \\ 642&\<open>div\<close>, \<open>mod\<close> & 70 & left\\ 643&\<open>^\<close> & 80 & right\\ 644&\<open>dvd\<close> & 50 \\ 645\hline 646Lists & \<open>#\<close>, \<open>@\<close> & 65 & right\\ 647&\<open>!\<close> & 100 & left 648\end{tabular} 649\end{center} 650\<close> 651(*<*) 652end 653(*>*) 654