src/HOL/Docs/MainDoc.thy
author nipkow
Mon, 09 Mar 2009 12:24:01 +0100
changeset 30384 2f24531b2d3e
parent 30372 96d508968153
permissions -rw-r--r--
fixed typing of UN/INT syntax
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
     1
(*<*)
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
     2
theory MainDoc
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
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
     6
ML {*
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
     7
fun pretty_term_type_only ctxt (t, T) =
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
     8
  (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then ()
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
     9
   else error "term_type_only: type mismatch";
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    10
   Syntax.pretty_typ ctxt T)
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    11
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    12
val _ = ThyOutput.add_commands
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    13
  [("term_type_only", ThyOutput.args (Args.term -- Args.typ_abbrev) (ThyOutput.output pretty_term_type_only))];
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    14
*}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    15
(*>*)
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    16
text{*
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    17
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    18
\begin{abstract}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    19
This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisicated class structure is only hinted at.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    20
\end{abstract}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    21
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    22
\section{HOL}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    23
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    24
The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    25
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    26
Overloaded operators:
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    27
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    28
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    29
@{text "0"} & @{typeof HOL.zero}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    30
@{text "1"} & @{typeof HOL.one}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    31
@{const HOL.plus} & @{typeof HOL.plus}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    32
@{const HOL.minus} & @{typeof HOL.minus}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    33
@{const HOL.uminus} & @{typeof HOL.uminus}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    34
@{const HOL.times} & @{typeof HOL.times}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    35
@{const HOL.inverse} & @{typeof HOL.inverse}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    36
@{const HOL.divide} & @{typeof HOL.divide}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    37
@{const HOL.abs} & @{typeof HOL.abs}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    38
@{const HOL.sgn} & @{typeof HOL.sgn}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    39
@{const HOL.less_eq} & @{typeof HOL.less_eq}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    40
@{const HOL.less} & @{typeof HOL.less}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    41
@{const HOL.default} & @{typeof HOL.default}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    42
@{const HOL.undefined} & @{typeof HOL.undefined}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    43
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    44
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    45
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    46
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    47
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    48
@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    49
@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    50
@{term"If x y z"} & @{term[source]"If x y z"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    51
@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\<lambda>x. e\<^isub>2)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    52
@{term"abs x"} & @{term[source]"abs x"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    53
@{term"uminus x"} & @{term[source]"uminus x"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    54
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    55
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    56
\section{Orderings}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    57
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    58
A collection of classes constraining @{text"\<le>"} and @{text"<"}:
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    59
preorders, partial orders, linear orders, dense linear orders and wellorders.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    60
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    61
\begin{tabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    62
@{const Orderings.Least} & @{typeof Orderings.Least}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    63
@{const Orderings.min} & @{typeof Orderings.min}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    64
@{const Orderings.max} & @{typeof Orderings.max}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    65
@{const Orderings.mono} & @{typeof Orderings.mono}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    66
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    67
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    68
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    69
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    70
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    71
@{term[source]"x \<ge> y"} & @{term"x \<ge> y"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    72
@{term[source]"x > y"} & @{term"x > y"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    73
@{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    74
@{term"ALL x<y. P"} & @{term[source]"\<forall>x. x < y \<longrightarrow> P"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    75
@{term"ALL x>=y. P"} & @{term[source]"\<forall>x. x \<ge> y \<longrightarrow> P"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    76
@{term"ALL x>y. P"} & @{term[source]"\<forall>x. x > y \<longrightarrow> P"}\\
30370
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
    77
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<exists>"} instead of @{text"\<forall>"}}\\
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    78
@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    79
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    80
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    81
\section{Set}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    82
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    83
Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    84
\bigskip
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    85
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    86
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
30370
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
    87
@{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    88
@{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    89
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
30370
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
    90
@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} \qquad(\textsc{ascii} @{text":"})\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
    91
@{const Set.Un} & @{term_type_only Set.Un "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Un"})\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
    92
@{const Set.Int} & @{term_type_only Set.Int "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} \qquad(\textsc{ascii} @{text"Int"})\\
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    93
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    94
@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    95
@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    96
@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    97
@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    98
@{const UNIV} & @{term_type_only UNIV "'a set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    99
@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   100
@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   101
@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   102
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   103
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   104
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   105
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   106
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   107
@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   108
@{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   109
@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   110
@{term"A \<subset> B"} & @{term[source]"A < B"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   111
@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   112
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   113
@{term"{x. P}"} & @{term[source]"Collect(\<lambda>x. P)"}\\
30370
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   114
@{term[mode=xsymbols]"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   115
@{term[mode=xsymbols]"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   116
@{term[mode=xsymbols]"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   117
@{term[mode=xsymbols]"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   118
@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   119
@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   120
@{term"range f"} & @{term[source]"f ` UNIV"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   121
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   122
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   123
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   124
\section{Fun}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   125
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   126
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   127
@{const "Fun.id"} & @{typeof Fun.id}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   128
@{const "Fun.comp"} & @{typeof Fun.comp}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   129
@{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
   130
@{const "Fun.inj"} & @{typeof Fun.inj}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   131
@{const "Fun.surj"} & @{typeof Fun.surj}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   132
@{const "Fun.bij"} & @{typeof Fun.bij}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   133
@{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
   134
@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   135
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   136
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   137
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   138
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   139
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   140
@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   141
@{text"f(x\<^isub>1:=y\<^isub>1,\<dots>,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\<dots>(x\<^isub>n:=y\<^isub>n)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   142
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   143
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   144
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   145
\section{Fixed Points}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   146
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   147
Theory: @{theory Inductive}.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   148
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   149
Least and greatest fixed points in a complete lattice @{typ 'a}:
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   150
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   151
\begin{tabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   152
@{const Inductive.lfp} & @{typeof Inductive.lfp}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   153
@{const Inductive.gfp} & @{typeof Inductive.gfp}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   154
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   155
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   156
Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   157
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   158
\section{Sum\_Type}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   159
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   160
Type constructor @{text"+"}.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   161
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   162
\begin{tabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   163
@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   164
@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   165
@{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
   166
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   167
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   168
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   169
\section{Product\_Type}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   170
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   171
Types @{typ unit} and @{text"\<times>"}.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   172
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   173
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   174
@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   175
@{const Pair} & @{typeof Pair}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   176
@{const fst} & @{typeof fst}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   177
@{const snd} & @{typeof snd}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   178
@{const split} & @{typeof split}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   179
@{const curry} & @{typeof curry}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   180
@{const Product_Type.Times} & @{typeof Product_Type.Times}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   181
@{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
   182
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   183
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   184
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   185
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   186
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   187
@{term"Pair a b"} & @{term[source]"Pair a b"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   188
@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   189
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   190
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   191
Pairs may be nested. Nesting to the right is printed as a tuple,
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   192
e.g.\ \mbox{@{term"(a,b,c)"}} is really @{text"(a,(b,c))"}.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   193
Pattern matching with pairs and tuples extends to all binders,
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   194
e.g.\ @{prop"ALL (x,y):A. P"}, @{term"{(x,y). P}"}, etc.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   195
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   196
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   197
\section{Relation}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   198
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   199
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   200
@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   201
@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('c*'a)set\<Rightarrow>('c*'b)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   202
@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   203
@{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
   204
@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   205
@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   206
@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   207
@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   208
@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   209
@{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
   210
@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   211
@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   212
@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   213
@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   214
@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   215
@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   216
@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\
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
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   221
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   222
@{term"converse r"} & @{term[source]"converse r"}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   223
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   224
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   225
\section{Equiv\_Relations}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   226
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   227
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   228
@{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
   229
@{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
   230
@{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
   231
@{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
   232
%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   233
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   234
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   235
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   236
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   237
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   238
@{term"congruent r f"} & @{term[source]"congruent r f"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   239
@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   240
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   241
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   242
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   243
\section{Transitive\_Closure}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   244
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   245
\begin{tabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   246
@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   247
@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   248
@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   249
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   250
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   251
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   252
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   253
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   254
@{term"rtrancl r"} & @{term[source]"rtrancl r"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   255
@{term"trancl r"} & @{term[source]"trancl r"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   256
@{term"reflcl r"} & @{term[source]"reflcl r"}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   257
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   258
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   259
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   260
\section{Algebra}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   261
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   262
Theories @{theory OrderedGroup} and @{theory Ring_and_Field} define a large
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   263
collection of classes describing common algebraic structures from semigroups
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   264
up to fields. Everything is done in terms of @{const plus}, @{const times}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   265
and other overloaded operators.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   266
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   267
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   268
\section{Nat}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   269
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   270
@{datatype nat}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   271
\bigskip
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   272
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   273
\begin{tabular}{@ {} lllllll @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   274
@{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   275
@{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   276
@{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   277
@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   278
@{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   279
@{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   280
@{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   281
@{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   282
@{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   283
@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   284
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   285
@{term "Min :: nat set \<Rightarrow> nat"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   286
@{term "Max :: nat set \<Rightarrow> nat"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   287
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   288
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   289
\begin{tabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   290
@{const Nat.of_nat} & @{typeof Nat.of_nat}
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
\section{Int}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   294
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   295
Type @{typ int}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   296
\bigskip
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   297
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   298
\begin{tabular}{@ {} llllllll @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   299
@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   300
@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   301
@{term "uminus :: int \<Rightarrow> int"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   302
@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   303
@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   304
@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}&
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   305
@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}&
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   306
@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   307
@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   308
@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   309
@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   310
@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   311
@{term "Min :: int set \<Rightarrow> int"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   312
@{term "Max :: int set \<Rightarrow> int"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   313
@{term "abs :: int \<Rightarrow> int"} &
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   314
@{term "sgn :: int \<Rightarrow> int"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   315
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   316
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   317
\begin{tabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   318
@{const Int.nat} & @{typeof Int.nat}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   319
@{const Int.of_int} & @{typeof Int.of_int}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   320
@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   321
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   322
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   323
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   324
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   325
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   326
@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   327
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   328
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   329
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   330
\section{Wellfounded}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   331
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   332
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   333
@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   334
@{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\<Rightarrow>bool"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   335
@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   336
@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   337
@{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
   338
@{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
   339
@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   340
@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   341
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   342
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   343
30384
2f24531b2d3e fixed typing of UN/INT syntax
nipkow
parents: 30372
diff changeset
   344
\section{SetInterval}
30321
nipkow
parents: 30293
diff changeset
   345
nipkow
parents: 30293
diff changeset
   346
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
30370
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   347
@{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   348
@{const atMost} & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   349
@{const greaterThan} & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   350
@{const atLeast} & @{term_type_only atLeast "'a::ord \<Rightarrow> 'a set"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   351
@{const greaterThanLessThan} & @{term_type_only greaterThanLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   352
@{const atLeastLessThan} & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   353
@{const greaterThanAtMost} & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   354
@{const atLeastAtMost} & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
30321
nipkow
parents: 30293
diff changeset
   355
\end{supertabular}
nipkow
parents: 30293
diff changeset
   356
nipkow
parents: 30293
diff changeset
   357
\subsubsection*{Syntax}
nipkow
parents: 30293
diff changeset
   358
nipkow
parents: 30293
diff changeset
   359
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
nipkow
parents: 30293
diff changeset
   360
@{term "lessThan y"} & @{term[source] "lessThan y"}\\
nipkow
parents: 30293
diff changeset
   361
@{term "atMost y"} & @{term[source] "atMost y"}\\
nipkow
parents: 30293
diff changeset
   362
@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\
nipkow
parents: 30293
diff changeset
   363
@{term "atLeast x"} & @{term[source] "atLeast x"}\\
nipkow
parents: 30293
diff changeset
   364
@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\
nipkow
parents: 30293
diff changeset
   365
@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\
nipkow
parents: 30293
diff changeset
   366
@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\
nipkow
parents: 30293
diff changeset
   367
@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\
30370
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   368
@{term[mode=xsymbols] "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   369
@{term[mode=xsymbols] "UN i:{..<n}. A"} & @{term[source] "\<Union> i \<in> {..<n}. A"}\\
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   370
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Inter>"} instead of @{text"\<Union>"}}\\
30321
nipkow
parents: 30293
diff changeset
   371
@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
30370
79a7491ac1fd Docs updates
nipkow
parents: 30321
diff changeset
   372
@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
30372
96d508968153 UN syntax fix
nipkow
parents: 30370
diff changeset
   373
\multicolumn{2}{@ {}l@ {}}{Similarly for @{text"\<Prod>"} instead of @{text"\<Sum>"}}\\
30321
nipkow
parents: 30293
diff changeset
   374
\end{supertabular}
nipkow
parents: 30293
diff changeset
   375
nipkow
parents: 30293
diff changeset
   376
???????
nipkow
parents: 30293
diff changeset
   377
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   378
\section{Power}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   379
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   380
\begin{tabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   381
@{const Power.power} & @{typeof Power.power}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   382
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   383
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   384
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   385
\section{Iterated Functions and Relations}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   386
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   387
Theory: @{theory Relation_Power}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   388
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   389
Iterated functions \ @{term[source]"(f::'a\<Rightarrow>'a) ^ n"} \
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   390
and relations \ @{term[source]"(r::('a\<times>'a)set) ^ n"}.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   391
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   392
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   393
\section{Option}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   394
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   395
@{datatype option}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   396
\bigskip
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   397
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   398
\begin{tabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   399
@{const Option.the} & @{typeof Option.the}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   400
@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   401
@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   402
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   403
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   404
\section{List}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   405
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   406
@{datatype list}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   407
\bigskip
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   408
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   409
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   410
@{const List.append} & @{typeof List.append}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   411
@{const List.butlast} & @{typeof List.butlast}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   412
@{const List.concat} & @{typeof List.concat}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   413
@{const List.distinct} & @{typeof List.distinct}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   414
@{const List.drop} & @{typeof List.drop}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   415
@{const List.dropWhile} & @{typeof List.dropWhile}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   416
@{const List.filter} & @{typeof List.filter}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   417
@{const List.foldl} & @{typeof List.foldl}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   418
@{const List.foldr} & @{typeof List.foldr}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   419
@{const List.hd} & @{typeof List.hd}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   420
@{const List.last} & @{typeof List.last}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   421
@{const List.length} & @{typeof List.length}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   422
@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   423
@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   424
@{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
   425
@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   426
@{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   427
@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   428
@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   429
@{const List.listsum} & @{typeof List.listsum}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   430
@{const List.list_all2} & @{typeof List.list_all2}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   431
@{const List.list_update} & @{typeof List.list_update}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   432
@{const List.map} & @{typeof List.map}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   433
@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   434
@{const List.remdups} & @{typeof List.remdups}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   435
@{const List.removeAll} & @{typeof List.removeAll}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   436
@{const List.remove1} & @{typeof List.remove1}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   437
@{const List.replicate} & @{typeof List.replicate}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   438
@{const List.rev} & @{typeof List.rev}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   439
@{const List.rotate} & @{typeof List.rotate}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   440
@{const List.rotate1} & @{typeof List.rotate1}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   441
@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   442
@{const List.sort} & @{typeof List.sort}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   443
@{const List.sorted} & @{typeof List.sorted}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   444
@{const List.splice} & @{typeof List.splice}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   445
@{const List.sublist} & @{typeof List.sublist}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   446
@{const List.take} & @{typeof List.take}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   447
@{const List.takeWhile} & @{typeof List.takeWhile}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   448
@{const List.tl} & @{typeof List.tl}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   449
@{const List.upt} & @{typeof List.upt}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   450
@{const List.upto} & @{typeof List.upto}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   451
@{const List.zip} & @{typeof List.zip}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   452
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   453
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   454
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   455
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   456
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   457
@{text"[x\<^isub>1,\<dots>,x\<^isub>n]"} & @{text"x\<^isub>1 # \<dots> # x\<^isub>n # []"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   458
@{term"[m..<n]"} & @{term[source]"upt m n"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   459
@{term"[i..j]"} & @{term[source]"upto i j"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   460
@{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   461
@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   462
@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   463
@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   464
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   465
\medskip
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   466
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   467
Comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   468
qualifier @{text q\<^isub>i} is either a generator @{text"pat \<leftarrow> e"} or a
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   469
guard, i.e.\ boolean expression.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   470
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   471
\section{Map}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   472
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   473
Maps model partial functions and are often used as finite tables. However,
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   474
the domain of a map may be infinite.
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   475
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   476
@{text"'a \<rightharpoonup> 'b  =  'a \<Rightarrow> 'b option"}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   477
\bigskip
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   478
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   479
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   480
@{const Map.empty} & @{typeof Map.empty}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   481
@{const Map.map_add} & @{typeof Map.map_add}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   482
@{const Map.map_comp} & @{typeof Map.map_comp}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   483
@{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
   484
@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   485
@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   486
@{const Map.map_le} & @{typeof Map.map_le}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   487
@{const Map.map_of} & @{typeof Map.map_of}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   488
@{const Map.map_upds} & @{typeof Map.map_upds}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   489
\end{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   490
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   491
\subsubsection*{Syntax}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   492
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   493
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   494
@{text"empty"} & @{term"\<lambda>x. None"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   495
@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   496
@{text"m(x\<^isub>1\<mapsto>y\<^isub>1,\<dots>,x\<^isub>n\<mapsto>y\<^isub>n)"} & @{text[source]"m(x\<^isub>1\<mapsto>y\<^isub>1)\<dots>(x\<^isub>n\<mapsto>y\<^isub>n)"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   497
@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   498
\end{tabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   499
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   500
*}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   501
(*<*)
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   502
end
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
   503
(*>*)