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