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