30293

1 
(*<*)


2 
theory MainDoc


3 
imports Main


4 
begin


5 


6 
ML {*


7 
fun pretty_term_type_only ctxt (t, T) =


8 
(if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then ()


9 
else error "term_type_only: type mismatch";


10 
Syntax.pretty_typ ctxt T)


11 


12 
val _ = ThyOutput.add_commands


13 
[("term_type_only", ThyOutput.args (Args.term  Args.typ_abbrev) (ThyOutput.output pretty_term_type_only))];


14 
*}


15 
(*>*)


16 
text{*


17 


18 
\begin{abstract}


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.


20 
\end{abstract}


21 


22 
\section{HOL}


23 


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"}.


25 


26 
Overloaded operators:


27 


28 
\begin{supertabular}{@ {} l @ {~::~} l @ {}}


29 
@{text "0"} & @{typeof HOL.zero}\\


30 
@{text "1"} & @{typeof HOL.one}\\


31 
@{const HOL.plus} & @{typeof HOL.plus}\\


32 
@{const HOL.minus} & @{typeof HOL.minus}\\


33 
@{const HOL.uminus} & @{typeof HOL.uminus}\\


34 
@{const HOL.times} & @{typeof HOL.times}\\


35 
@{const HOL.inverse} & @{typeof HOL.inverse}\\


36 
@{const HOL.divide} & @{typeof HOL.divide}\\


37 
@{const HOL.abs} & @{typeof HOL.abs}\\


38 
@{const HOL.sgn} & @{typeof HOL.sgn}\\


39 
@{const HOL.less_eq} & @{typeof HOL.less_eq}\\


40 
@{const HOL.less} & @{typeof HOL.less}\\


41 
@{const HOL.default} & @{typeof HOL.default}\\


42 
@{const HOL.undefined} & @{typeof HOL.undefined}\\


43 
\end{supertabular}


44 


45 
\subsubsection*{Syntax}


46 


47 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


48 
@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"}\\


49 
@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"}\\


50 
@{term"If x y z"} & @{term[source]"If x y z"}\\


51 
@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\<lambda>x. e\<^isub>2)"}\\


52 
@{term"abs x"} & @{term[source]"abs x"}\\


53 
@{term"uminus x"} & @{term[source]"uminus x"}\\


54 
\end{supertabular}


55 


56 
\section{Orderings}


57 


58 
A collection of classes constraining @{text"\<le>"} and @{text"<"}:


59 
preorders, partial orders, linear orders, dense linear orders and wellorders.


60 


61 
\begin{tabular}{@ {} l @ {~::~} l @ {}}


62 
@{const Orderings.Least} & @{typeof Orderings.Least}\\


63 
@{const Orderings.min} & @{typeof Orderings.min}\\


64 
@{const Orderings.max} & @{typeof Orderings.max}\\


65 
@{const Orderings.mono} & @{typeof Orderings.mono}\\


66 
\end{tabular}


67 


68 
\subsubsection*{Syntax}


69 


70 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


71 
@{term[source]"x \<ge> y"} & @{term"x \<ge> y"}\\


72 
@{term[source]"x > y"} & @{term"x > y"}\\


73 
@{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\


74 
@{term"ALL x<y. P"} & @{term[source]"\<forall>x. x < y \<longrightarrow> P"}\\


75 
@{term"ALL x>=y. P"} & @{term[source]"\<forall>x. x \<ge> y \<longrightarrow> P"}\\


76 
@{term"ALL x>y. P"} & @{term[source]"\<forall>x. x > y \<longrightarrow> P"}\\


77 
@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\


78 
\end{supertabular}


79 


80 
Similar for @{text"\<exists>"} instead of @{text"\<forall>"}.


81 


82 
\section{Set}


83 


84 
Sets are predicates: @{text[source]"'a set = 'a \<Rightarrow> bool"}


85 
\bigskip


86 


87 
\begin{supertabular}{@ {} l @ {~::~} l @ {}}


88 
@{const "{}"} & @{term_type_only "{}" "'a set"}\\


89 
@{const insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\


90 
@{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\


91 
@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"}\\


92 
@{const "op Un"} & @{term_type_only "op Un" "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"}\\


93 
@{const "op Int"} & @{term_type_only "op Int" "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"}\\


94 
@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\


95 
@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\


96 
@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\


97 
@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\


98 
@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\


99 
@{const UNIV} & @{term_type_only UNIV "'a set"}\\


100 
@{const image} & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\


101 
@{const Ball} & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\


102 
@{const Bex} & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\


103 
\end{supertabular}


104 


105 
\subsubsection*{Syntax}


106 


107 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


108 
@{text"{x\<^isub>1,\<dots>,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\<dots> (insert x\<^isub>n {})\<dots>)"}\\


109 
@{term"x ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\


110 
@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\


111 
@{term"A \<subset> B"} & @{term[source]"A < B"}\\


112 
@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\


113 
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\


114 
@{term"{x. P}"} & @{term[source]"Collect(\<lambda>x. P)"}\\


115 
@{term"UN x:I. A"} & @{term[source]"UNION I (\<lambda>x. A)"}\\


116 
@{term"UN x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\


117 
@{term"INT x:I. A"} & @{term[source]"INTER I (\<lambda>x. A)"}\\


118 
@{term"INT x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\


119 
@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\


120 
@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\


121 
@{term"range f"} & @{term[source]"f ` UNIV"}\\


122 
\end{supertabular}


123 


124 


125 
\section{Fun}


126 


127 
\begin{supertabular}{@ {} l @ {~::~} l @ {}}


128 
@{const "Fun.id"} & @{typeof Fun.id}\\


129 
@{const "Fun.comp"} & @{typeof Fun.comp}\\


130 
@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\


131 
@{const "Fun.inj"} & @{typeof Fun.inj}\\


132 
@{const "Fun.surj"} & @{typeof Fun.surj}\\


133 
@{const "Fun.bij"} & @{typeof Fun.bij}\\


134 
@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\


135 
@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\


136 
\end{supertabular}


137 


138 
\subsubsection*{Syntax}


139 


140 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


141 
@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\


142 
@{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)"}\\


143 
\end{tabular}


144 


145 


146 
\section{Fixed Points}


147 


148 
Theory: @{theory Inductive}.


149 


150 
Least and greatest fixed points in a complete lattice @{typ 'a}:


151 


152 
\begin{tabular}{@ {} l @ {~::~} l @ {}}


153 
@{const Inductive.lfp} & @{typeof Inductive.lfp}\\


154 
@{const Inductive.gfp} & @{typeof Inductive.gfp}\\


155 
\end{tabular}


156 


157 
Note that in particular sets (@{typ"'a \<Rightarrow> bool"}) are complete lattices.


158 


159 
\section{Sum\_Type}


160 


161 
Type constructor @{text"+"}.


162 


163 
\begin{tabular}{@ {} l @ {~::~} l @ {}}


164 
@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\


165 
@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\


166 
@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\<Rightarrow>'b set\<Rightarrow>('a+'b)set"}


167 
\end{tabular}


168 


169 


170 
\section{Product\_Type}


171 


172 
Types @{typ unit} and @{text"\<times>"}.


173 


174 
\begin{supertabular}{@ {} l @ {~::~} l @ {}}


175 
@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\


176 
@{const Pair} & @{typeof Pair}\\


177 
@{const fst} & @{typeof fst}\\


178 
@{const snd} & @{typeof snd}\\


179 
@{const split} & @{typeof split}\\


180 
@{const curry} & @{typeof curry}\\


181 
@{const Product_Type.Times} & @{typeof Product_Type.Times}\\


182 
@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\


183 
\end{supertabular}


184 


185 
\subsubsection*{Syntax}


186 


187 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


188 
@{term"Pair a b"} & @{term[source]"Pair a b"}\\


189 
@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\


190 
\end{tabular}


191 


192 
Pairs may be nested. Nesting to the right is printed as a tuple,


193 
e.g.\ \mbox{@{term"(a,b,c)"}} is really @{text"(a,(b,c))"}.


194 
Pattern matching with pairs and tuples extends to all binders,


195 
e.g.\ @{prop"ALL (x,y):A. P"}, @{term"{(x,y). P}"}, etc.


196 


197 


198 
\section{Relation}


199 


200 
\begin{supertabular}{@ {} l @ {~::~} l @ {}}


201 
@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \<Rightarrow> ('b*'a)set"}\\


202 
@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\<Rightarrow>('c*'a)set\<Rightarrow>('c*'b)set"}\\


203 
@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\<Rightarrow>'a set\<Rightarrow>'b set"}\\


204 
@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\<Rightarrow>('b\<Rightarrow>'a)\<Rightarrow>('b*'b)set"}\\


205 
@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\<Rightarrow>('a*'a)set"}\\


206 
@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\


207 
@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\<Rightarrow>'a set"}\\


208 
@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\<Rightarrow>'b set"}\\


209 
@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\<Rightarrow>'a set"}\\


210 
@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\


211 
@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\<Rightarrow>bool"}\\


212 
@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\<Rightarrow>bool"}\\


213 
@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\<Rightarrow>bool"}\\


214 
@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\<Rightarrow>bool"}\\


215 
@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\<Rightarrow>bool"}\\


216 
@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\<Rightarrow>('a*'a)set\<Rightarrow>bool"}\\


217 
@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\<Rightarrow>bool"}\\


218 
\end{supertabular}


219 


220 
\subsubsection*{Syntax}


221 


222 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


223 
@{term"converse r"} & @{term[source]"converse r"}


224 
\end{tabular}


225 


226 
\section{Equiv\_Relations}


227 


228 
\begin{supertabular}{@ {} l @ {~::~} l @ {}}


229 
@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\


230 
@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\


231 
@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\


232 
@{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"}\\


233 
%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\


234 
\end{supertabular}


235 


236 
\subsubsection*{Syntax}


237 


238 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


239 
@{term"congruent r f"} & @{term[source]"congruent r f"}\\


240 
@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\


241 
\end{tabular}


242 


243 


244 
\section{Transitive\_Closure}


245 


246 
\begin{tabular}{@ {} l @ {~::~} l @ {}}


247 
@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\


248 
@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\


249 
@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\


250 
\end{tabular}


251 


252 
\subsubsection*{Syntax}


253 


254 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


255 
@{term"rtrancl r"} & @{term[source]"rtrancl r"}\\


256 
@{term"trancl r"} & @{term[source]"trancl r"}\\


257 
@{term"reflcl r"} & @{term[source]"reflcl r"}


258 
\end{tabular}


259 


260 


261 
\section{Algebra}


262 


263 
Theories @{theory OrderedGroup} and @{theory Ring_and_Field} define a large


264 
collection of classes describing common algebraic structures from semigroups


265 
up to fields. Everything is done in terms of @{const plus}, @{const times}


266 
and other overloaded operators.


267 


268 


269 
\section{Nat}


270 


271 
@{datatype nat}


272 
\bigskip


273 


274 
\begin{tabular}{@ {} lllllll @ {}}


275 
@{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} &


276 
@{term "op  :: nat \<Rightarrow> nat \<Rightarrow> nat"} &


277 
@{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} &


278 
@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} &


279 
@{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}&


280 
@{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}&


281 
@{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\


282 
@{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} &


283 
@{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} &


284 
@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} &


285 
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} &


286 
@{term "Min :: nat set \<Rightarrow> nat"} &


287 
@{term "Max :: nat set \<Rightarrow> nat"}\\


288 
\end{tabular}


289 


290 
\begin{tabular}{@ {} l @ {~::~} l @ {}}


291 
@{const Nat.of_nat} & @{typeof Nat.of_nat}


292 
\end{tabular}


293 


294 
\section{Int}


295 


296 
Type @{typ int}


297 
\bigskip


298 


299 
\begin{tabular}{@ {} llllllll @ {}}


300 
@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} &


301 
@{term "op  :: int \<Rightarrow> int \<Rightarrow> int"} &


302 
@{term "uminus :: int \<Rightarrow> int"} &


303 
@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} &


304 
@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} &


305 
@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}&


306 
@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}&


307 
@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\


308 
@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} &


309 
@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} &


310 
@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} &


311 
@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} &


312 
@{term "Min :: int set \<Rightarrow> int"} &


313 
@{term "Max :: int set \<Rightarrow> int"}\\


314 
@{term "abs :: int \<Rightarrow> int"} &


315 
@{term "sgn :: int \<Rightarrow> int"}\\


316 
\end{tabular}


317 


318 
\begin{tabular}{@ {} l @ {~::~} l @ {}}


319 
@{const Int.nat} & @{typeof Int.nat}\\


320 
@{const Int.of_int} & @{typeof Int.of_int}\\


321 
@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"}\\


322 
\end{tabular}


323 


324 
\subsubsection*{Syntax}


325 


326 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


327 
@{term"of_nat::nat\<Rightarrow>int"} & @{term[source]"of_nat"}\\


328 
\end{tabular}


329 


330 


331 
\section{Wellfounded}


332 


333 
\begin{supertabular}{@ {} l @ {~::~} l @ {}}


334 
@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\


335 
@{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\<Rightarrow>bool"}\\


336 
@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\


337 
@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\


338 
@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>(('a*'b)*('a*'b))set"}\\


339 
@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\


340 
@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\


341 
@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\


342 
\end{supertabular}


343 


344 


345 
\section{Power}


346 


347 
\begin{tabular}{@ {} l @ {~::~} l @ {}}


348 
@{const Power.power} & @{typeof Power.power}


349 
\end{tabular}


350 


351 


352 
\section{Iterated Functions and Relations}


353 


354 
Theory: @{theory Relation_Power}


355 


356 
Iterated functions \ @{term[source]"(f::'a\<Rightarrow>'a) ^ n"} \


357 
and relations \ @{term[source]"(r::('a\<times>'a)set) ^ n"}.


358 


359 


360 
\section{Option}


361 


362 
@{datatype option}


363 
\bigskip


364 


365 
\begin{tabular}{@ {} l @ {~::~} l @ {}}


366 
@{const Option.the} & @{typeof Option.the}\\


367 
@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\


368 
@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}


369 
\end{tabular}


370 


371 
\section{List}


372 


373 
@{datatype list}


374 
\bigskip


375 


376 
\begin{supertabular}{@ {} l @ {~::~} l @ {}}


377 
@{const List.append} & @{typeof List.append}\\


378 
@{const List.butlast} & @{typeof List.butlast}\\


379 
@{const List.concat} & @{typeof List.concat}\\


380 
@{const List.distinct} & @{typeof List.distinct}\\


381 
@{const List.drop} & @{typeof List.drop}\\


382 
@{const List.dropWhile} & @{typeof List.dropWhile}\\


383 
@{const List.filter} & @{typeof List.filter}\\


384 
@{const List.foldl} & @{typeof List.foldl}\\


385 
@{const List.foldr} & @{typeof List.foldr}\\


386 
@{const List.hd} & @{typeof List.hd}\\


387 
@{const List.last} & @{typeof List.last}\\


388 
@{const List.length} & @{typeof List.length}\\


389 
@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\


390 
@{const List.lex} & @{term_type_only List.lex "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\


391 
@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a list * 'a list)set"}\\


392 
@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\


393 
@{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\


394 
@{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\


395 
@{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\


396 
@{const List.listsum} & @{typeof List.listsum}\\


397 
@{const List.list_all2} & @{typeof List.list_all2}\\


398 
@{const List.list_update} & @{typeof List.list_update}\\


399 
@{const List.map} & @{typeof List.map}\\


400 
@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\


401 
@{const List.remdups} & @{typeof List.remdups}\\


402 
@{const List.removeAll} & @{typeof List.removeAll}\\


403 
@{const List.remove1} & @{typeof List.remove1}\\


404 
@{const List.replicate} & @{typeof List.replicate}\\


405 
@{const List.rev} & @{typeof List.rev}\\


406 
@{const List.rotate} & @{typeof List.rotate}\\


407 
@{const List.rotate1} & @{typeof List.rotate1}\\


408 
@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\


409 
@{const List.sort} & @{typeof List.sort}\\


410 
@{const List.sorted} & @{typeof List.sorted}\\


411 
@{const List.splice} & @{typeof List.splice}\\


412 
@{const List.sublist} & @{typeof List.sublist}\\


413 
@{const List.take} & @{typeof List.take}\\


414 
@{const List.takeWhile} & @{typeof List.takeWhile}\\


415 
@{const List.tl} & @{typeof List.tl}\\


416 
@{const List.upt} & @{typeof List.upt}\\


417 
@{const List.upto} & @{typeof List.upto}\\


418 
@{const List.zip} & @{typeof List.zip}\\


419 
\end{supertabular}


420 


421 
\subsubsection*{Syntax}


422 


423 
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


424 
@{text"[x\<^isub>1,\<dots>,x\<^isub>n]"} & @{text"x\<^isub>1 # \<dots> # x\<^isub>n # []"}\\


425 
@{term"[m..<n]"} & @{term[source]"upt m n"}\\


426 
@{term"[i..j]"} & @{term[source]"upto i j"}\\


427 
@{text"[e. x \<leftarrow> xs]"} & @{term"map (%x. e) xs"}\\


428 
@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\


429 
@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\


430 
@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\


431 
\end{supertabular}


432 
\medskip


433 


434 
Comprehension: @{text"[e. q\<^isub>1, \<dots>, q\<^isub>n]"} where each


435 
qualifier @{text q\<^isub>i} is either a generator @{text"pat \<leftarrow> e"} or a


436 
guard, i.e.\ boolean expression.


437 


438 
\section{Map}


439 


440 
Maps model partial functions and are often used as finite tables. However,


441 
the domain of a map may be infinite.


442 


443 
@{text"'a \<rightharpoonup> 'b = 'a \<Rightarrow> 'b option"}


444 
\bigskip


445 


446 
\begin{supertabular}{@ {} l @ {~::~} l @ {}}


447 
@{const Map.empty} & @{typeof Map.empty}\\


448 
@{const Map.map_add} & @{typeof Map.map_add}\\


449 
@{const Map.map_comp} & @{typeof Map.map_comp}\\


450 
@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\<Rightarrow>'b option)\<Rightarrow>'a set\<Rightarrow>('a\<Rightarrow>'b option)"}\\


451 
@{const Map.dom} & @{term_type_only Map.dom "('a\<Rightarrow>'b option)\<Rightarrow>'a set"}\\


452 
@{const Map.ran} & @{term_type_only Map.ran "('a\<Rightarrow>'b option)\<Rightarrow>'b set"}\\


453 
@{const Map.map_le} & @{typeof Map.map_le}\\


454 
@{const Map.map_of} & @{typeof Map.map_of}\\


455 
@{const Map.map_upds} & @{typeof Map.map_upds}\\


456 
\end{supertabular}


457 


458 
\subsubsection*{Syntax}


459 


460 
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}


461 
@{text"empty"} & @{term"\<lambda>x. None"}\\


462 
@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\


463 
@{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)"}\\


464 
@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\


465 
\end{tabular}


466 


467 
*}


468 
(*<*)


469 
end


470 
(*>*) 