(* Title: Notation for hotel key card system
Author: Tobias Nipkow, TU Muenchen
*)
(*<*)
theory Notation
imports "HOL-Library.LaTeXsugar"
begin
abbreviation
"SomeFloor" (‹(⌊_⌋)›) where "⌊x⌋ ≡ Some x"
(*>*)
subsection‹Notation›
text‹
conforms largely to everyday mathematical notation.
section introduces further non-standard notation and in particular
few basic data types with their primitive operations.
sloppy
begin{description}
item[Types] The type of truth values is called @{typ bool}. The
of total functions is denoted by ‹→›. Type variables
with a quote, as in @{typ"'a"}, @{typ"'b"} etc. The notation
t$~‹::›~$\tau$ means that term $t$ has type $\tau$.
item[Functions] can be updated at ‹x› with new value ‹y›,
@{term"f(x:=y)"}. The range of a function is @{term"range f"},
{prop"inj f"} means ‹f› is injective.
item[Pairs] come with the two projection functions
‹fst :: 'a × 'b → 'a› and ‹snd :: 'a × 'b → 'b›.
item[Sets] have type @{typ"'a set"}.
item[Lists] (type @{typ"'a list"}) come with the empty list
{term"[]"}, the infix constructor ‹⋅›, the infix ‹@›
appends two lists, and the conversion function @{term set} from
to sets. Variable names ending in ``s'' usually stand for
.
item[Records] are constructed like this ‹(f1 = v1, …)›
updated like this \mbox{‹r(fi := vi, …)›},
the ‹fi› are the field names,
‹vi› the values and ‹r› is a record.
end{description}\fussy
‹option› is defined like this
begin{center}
isacommand{datatype} ‹'a option = None | Some 'a›
end{center}
adjoins a new element @{term None} to a type @{typ 'a}. For
we write @{term"Some a"} instead of @{term[source]"Some a"}.
that ‹[A1; …; An] ==> A›
‹A1 ==> … ==> An ==> A›, which is the same as
`If ‹A1› and \dots\ and ‹An› then ‹A›''.
›
(*<*)
end
(*>*)
¤ Dauer der Verarbeitung: 0.3 Sekunden
¤
*© Formatika GbR, Deutschland
