Theory Notation

(*  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‹
HOL conforms largely to everyday mathematical notation.
This section introduces further non-standard notation and in particular
a few basic data types with their primitive operations.
\sloppy
\begin{description}

\item[Types] The type of truth values is called @{typ bool}.  The
space of total functions is denoted by ‹⇒›. Type variables
start 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›,
written @{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 ‹@›
that appends two lists, and the conversion function @{term set} from
lists to sets.  Variable names ending in ``s'' usually stand for
lists.

\item[Records] are constructed like this ‹⦇f⇩₁ = v⇩₁, …⦈›
and updated like this \mbox{‹r⦇f⇩_i := v⇩_i, …⦈›},
where the ‹f⇩_i› are the field names,
the ‹v⇩_i› the values and ‹r› is a record.

\end{description}\fussy
Datatype ‹option› is defined like this
\begin{center}
\isacommand{datatype} ‹'a option = None | Some 'a›
\end{center}
and adjoins a new element @{term None} to a type @{typ 'a}. For
succinctness we write @{term"Some a"} instead of @{term[source]"Some a"}.

Note that ‹⟦A⇩₁; …; A⇩_n⟧ ⟹ A›
abbreviates ‹A⇩₁ ⟹ … ⟹ A⇩_n ⟹ A›, which is the same as
``If ‹A⇩₁› and \dots\ and ‹A⇩_n› then ‹A›''.
›

(*<*)
end
(*>*)