added table of infix operators
authornipkow
Mon Dec 17 18:23:08 2012 +0100 (2012-12-17)
changeset 505810eaefd4306d7
parent 50580 fbb973a53106
child 50582 001a0e12d7f1
added table of infix operators
src/Doc/Main/Main_Doc.thy
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Mon Dec 17 17:19:21 2012 +0100
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Mon Dec 17 18:23:08 2012 +0100
     1.3 @@ -26,10 +26,10 @@
     1.4  text{*
     1.5  
     1.6  \begin{abstract}
     1.7 -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 sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/library/HOL/}.
     1.8 +This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/library/HOL/}.
     1.9  \end{abstract}
    1.10  
    1.11 -\section{HOL}
    1.12 +\section*{HOL}
    1.13  
    1.14  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"}.
    1.15  \smallskip
    1.16 @@ -49,7 +49,7 @@
    1.17  \end{supertabular}
    1.18  
    1.19  
    1.20 -\section{Orderings}
    1.21 +\section*{Orderings}
    1.22  
    1.23  A collection of classes defining basic orderings:
    1.24  preorder, partial order, linear order, dense linear order and wellorder.
    1.25 @@ -79,7 +79,7 @@
    1.26  \end{supertabular}
    1.27  
    1.28  
    1.29 -\section{Lattices}
    1.30 +\section*{Lattices}
    1.31  
    1.32  Classes semilattice, lattice, distributive lattice and complete lattice (the
    1.33  latter in theory @{theory Set}).
    1.34 @@ -108,10 +108,7 @@
    1.35  \end{supertabular}
    1.36  
    1.37  
    1.38 -\section{Set}
    1.39 -
    1.40 -%Sets are predicates: @{text[source]"'a set  =  'a \<Rightarrow> bool"}
    1.41 -%\bigskip
    1.42 +\section*{Set}
    1.43  
    1.44  \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
    1.45  @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
    1.46 @@ -151,7 +148,7 @@
    1.47  \end{supertabular}
    1.48  
    1.49  
    1.50 -\section{Fun}
    1.51 +\section*{Fun}
    1.52  
    1.53  \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
    1.54  @{const "Fun.id"} & @{typeof Fun.id}\\
    1.55 @@ -172,7 +169,7 @@
    1.56  \end{tabular}
    1.57  
    1.58  
    1.59 -\section{Hilbert\_Choice}
    1.60 +\section*{Hilbert\_Choice}
    1.61  
    1.62  Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}.
    1.63  \smallskip
    1.64 @@ -187,7 +184,7 @@
    1.65  @{term inv} & @{term[source]"inv_into UNIV"}
    1.66  \end{tabular}
    1.67  
    1.68 -\section{Fixed Points}
    1.69 +\section*{Fixed Points}
    1.70  
    1.71  Theory: @{theory Inductive}.
    1.72  
    1.73 @@ -200,7 +197,7 @@
    1.74  
    1.75  Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices.
    1.76  
    1.77 -\section{Sum\_Type}
    1.78 +\section*{Sum\_Type}
    1.79  
    1.80  Type constructor @{text"+"}.
    1.81  
    1.82 @@ -211,7 +208,7 @@
    1.83  \end{tabular}
    1.84  
    1.85  
    1.86 -\section{Product\_Type}
    1.87 +\section*{Product\_Type}
    1.88  
    1.89  Types @{typ unit} and @{text"\<times>"}.
    1.90  
    1.91 @@ -239,7 +236,7 @@
    1.92  e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
    1.93  
    1.94  
    1.95 -\section{Relation}
    1.96 +\section*{Relation}
    1.97  
    1.98  \begin{tabular}{@ {} l @ {~::~} l @ {}}
    1.99  @{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\
   1.100 @@ -271,7 +268,7 @@
   1.101  \noindent
   1.102  Type synonym \ @{typ"'a rel"} @{text"="} @{expanded_typ "'a rel"}
   1.103  
   1.104 -\section{Equiv\_Relations}
   1.105 +\section*{Equiv\_Relations}
   1.106  
   1.107  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.108  @{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\
   1.109 @@ -289,7 +286,7 @@
   1.110  \end{tabular}
   1.111  
   1.112  
   1.113 -\section{Transitive\_Closure}
   1.114 +\section*{Transitive\_Closure}
   1.115  
   1.116  \begin{tabular}{@ {} l @ {~::~} l @ {}}
   1.117  @{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
   1.118 @@ -308,7 +305,7 @@
   1.119  \end{tabular}
   1.120  
   1.121  
   1.122 -\section{Algebra}
   1.123 +\section*{Algebra}
   1.124  
   1.125  Theories @{theory Groups}, @{theory Rings}, @{theory Fields} and @{theory
   1.126  Divides} define a large collection of classes describing common algebraic
   1.127 @@ -338,7 +335,7 @@
   1.128  \end{tabular}
   1.129  
   1.130  
   1.131 -\section{Nat}
   1.132 +\section*{Nat}
   1.133  
   1.134  @{datatype nat}
   1.135  \bigskip
   1.136 @@ -365,7 +362,7 @@
   1.137    @{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"}
   1.138  \end{tabular}
   1.139  
   1.140 -\section{Int}
   1.141 +\section*{Int}
   1.142  
   1.143  Type @{typ int}
   1.144  \bigskip
   1.145 @@ -402,7 +399,7 @@
   1.146  \end{tabular}
   1.147  
   1.148  
   1.149 -\section{Finite\_Set}
   1.150 +\section*{Finite\_Set}
   1.151  
   1.152  
   1.153  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.154 @@ -425,7 +422,7 @@
   1.155  \end{supertabular}
   1.156  
   1.157  
   1.158 -\section{Wellfounded}
   1.159 +\section*{Wellfounded}
   1.160  
   1.161  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.162  @{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\
   1.163 @@ -438,7 +435,7 @@
   1.164  \end{supertabular}
   1.165  
   1.166  
   1.167 -\section{SetInterval}
   1.168 +\section*{Set\_Interval} % @{theory Set_Interval}
   1.169  
   1.170  \begin{supertabular}{@ {} l @ {~::~} l @ {}}
   1.171  @{const lessThan} & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
   1.172 @@ -473,14 +470,14 @@
   1.173  \end{supertabular}
   1.174  
   1.175  
   1.176 -\section{Power}
   1.177 +\section*{Power}
   1.178  
   1.179  \begin{tabular}{@ {} l @ {~::~} l @ {}}
   1.180  @{const Power.power} & @{typeof Power.power}
   1.181  \end{tabular}
   1.182  
   1.183  
   1.184 -\section{Option}
   1.185 +\section*{Option}
   1.186  
   1.187  @{datatype option}
   1.188  \bigskip
   1.189 @@ -492,7 +489,7 @@
   1.190  @{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
   1.191  \end{tabular}
   1.192  
   1.193 -\section{List}
   1.194 +\section*{List}
   1.195  
   1.196  @{datatype list}
   1.197  \bigskip
   1.198 @@ -563,7 +560,7 @@
   1.199  qualifier @{text q\<^isub>i} is either a generator \mbox{@{text"pat \<leftarrow> e"}} or a
   1.200  guard, i.e.\ boolean expression.
   1.201  
   1.202 -\section{Map}
   1.203 +\section*{Map}
   1.204  
   1.205  Maps model partial functions and are often used as finite tables. However,
   1.206  the domain of a map may be infinite.
   1.207 @@ -590,6 +587,35 @@
   1.208  @{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\
   1.209  \end{tabular}
   1.210  
   1.211 +\section*{Infix operators in Main} % @{theory Main}
   1.212 +
   1.213 +\begin{center}
   1.214 +\begin{tabular}{lll}
   1.215 +Operator & precedence & associativity \\
   1.216 +@{text"="}, @{text"\<noteq>"} & 50 & left\\
   1.217 +@{text"\<le>"}, @{text"<"}, @{text"\<ge>"}, @{text">"} & 50 \\
   1.218 +@{text"\<and>"} & 35 & right \\
   1.219 +@{text"\<or>"} & 30 & right \\
   1.220 +@{text"\<longrightarrow>"}, @{text"\<longleftrightarrow>"} & 25 & right\\
   1.221 +@{text"\<subseteq>"}, @{text"\<subset>"}, @{text"\<supseteq>"}, @{text"\<supset>"} & 50 \\
   1.222 +@{text"\<in>"}, @{text"\<notin>"} & 50 \\
   1.223 +@{text"\<inter>"} & 70 & left \\
   1.224 +@{text"\<union>"} & 65 & left \\
   1.225 +@{text"\<circ>"} & 55 & left\\
   1.226 +@{text"`"} & 90 & right\\
   1.227 +@{text"O"} & 75 & right\\
   1.228 +@{text"``"} & 90 & right\\
   1.229 +@{text"+"}, @{text"-"} & 65 & left \\
   1.230 +@{text"*"}, @{text"/"} & 70 & left \\
   1.231 +@{text"div"}, @{text"mod"} & 70 & left\\
   1.232 +@{text"^"} & 80 & right\\
   1.233 +@{text"^^"} & 80 & right\\
   1.234 +@{text"dvd"} & 50 \\
   1.235 +@{text"#"}, @{text"@"} & 65 & right\\
   1.236 +@{text"!"} & 100 & left\\
   1.237 +@{text"++"} & 100 & left\\
   1.238 +\end{tabular}
   1.239 +\end{center}
   1.240  *}
   1.241  (*<*)
   1.242  end