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