\begin{ttbox}

 \begin{ttbox}

 EXP = Pure +

 EXP = Pure +

 types

 types

   exp

   exp

 syntax

 syntax

 end

 end

 \end{ttbox}

 \end{ttbox}

 If you put this into a file {\tt EXP.thy} and load it via {\tt use_thy"EXP"},

 If you put this into a file {\tt EXP.thy} and load it via {\tt use_thy"EXP"},

 you can run some tests:

 you can run some tests:

 \begin{ttbox}

 \begin{ttbox}

 \subsection{Infixes}

 \subsection{Infixes}

 \indexbold{infixes}

 \indexbold{infixes}

 Infix operators associating to the left or right can be declared

 Infix operators associating to the left or right can be declared

 using {\tt infixl} or {\tt infixr}.

 using {\tt infixl} or {\tt infixr}.

 abbreviates the mixfix declarations

 abbreviates the mixfix declarations

 \begin{ttbox}

 \begin{ttbox}

 \end{ttbox}

 \end{ttbox}

 The infix operator is declared as a constant with the prefix {\tt op}.

 The infix operator is declared as a constant with the prefix {\tt op}.

 Thus, prefixing infixes with \sdx{op} makes them behave like ordinary

 Thus, prefixing infixes with \sdx{op} makes them behave like ordinary

 function symbols, as in \ML.  Special characters occurring in~$c$ must be

 function symbols, as in \ML.  Special characters occurring in~$c$ must be

 escaped, as in delimiters, using a single quote.

 escaped, as in delimiters, using a single quote.

 \begingroup

 \begingroup

 \def\Q{{\cal Q}}

 \def\Q{{\cal Q}}

 A {\bf binder} is a variable-binding construct such as a quantifier.  The

 A {\bf binder} is a variable-binding construct such as a quantifier.  The

 constant declaration

 constant declaration

 \begin{ttbox}

 \begin{ttbox}

 \end{ttbox}

 \end{ttbox}

 introduces a constant~$c$ of type~$\sigma$, which must have the form

 introduces a constant~$c$ of type~$\sigma$, which must have the form

 $(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where

 $(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where

 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$

 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$

 and the whole term has type~$\tau@3$. The optional integer $pb$

 and the whole term has type~$\tau@3$. The optional integer $pb$

 specifies the body's priority, by default~$p$.  Special characters

 specifies the body's priority, by default~$p$.  Special characters

 in $\Q$ must be escaped using a single quote.

 in $\Q$ must be escaped using a single quote.

 The declaration is expanded internally to something like

 The declaration is expanded internally to something like

 \begin{ttbox}

 \begin{ttbox}

 \end{ttbox}

 \end{ttbox}

 Here \ndx{idts} is the nonterminal symbol for a list of identifiers with

 Here \ndx{idts} is the nonterminal symbol for a list of identifiers with

 \index{type constraints}

 \index{type constraints}

 optional type constraints (see Fig.\ts\ref{fig:pure_gram}).  The

 optional type constraints (see Fig.\ts\ref{fig:pure_gram}).  The

 declaration also installs a parse translation\index{translations!parse}

 declaration also installs a parse translation\index{translations!parse}

 \[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \]

 \[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \]

 \medskip

 \medskip

 For example, let us declare the quantifier~$\forall$:\index{quantifiers}

 For example, let us declare the quantifier~$\forall$:\index{quantifiers}

 \begin{ttbox}

 \begin{ttbox}

 \end{ttbox}

 \end{ttbox}

 This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL

 This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL

   $x$.$P$}.  When printing, Isabelle prefers the latter form, but must fall

   $x$.$P$}.  When printing, Isabelle prefers the latter form, but must fall

 back on ${\tt All}(P)$ if $P$ is not an abstraction.  Both $P$ and {\tt ALL

 back on ${\tt All}(P)$ if $P$ is not an abstraction.  Both $P$ and {\tt ALL

   $x$.$P$} have type~$o$, the type of formulae, while the bound variable

   $x$.$P$} have type~$o$, the type of formulae, while the bound variable

 types

 types

   o

   o

 arities

 arities

   o :: logic

   o :: logic

 consts

 consts

 end

 end

 \end{ttbox}

 \end{ttbox}

 The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible

 The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible

 coercion function.  Assuming this definition resides in a file {\tt Base.thy},

 coercion function.  Assuming this definition resides in a file {\tt Base.thy},

 you have to load it with the command {\tt use_thy "Base"}.

 you have to load it with the command {\tt use_thy "Base"}.

 implication.  Its definition in Isabelle needs no advanced features but

 implication.  Its definition in Isabelle needs no advanced features but

 illustrates the overall mechanism nicely:

 illustrates the overall mechanism nicely:

 \begin{ttbox}

 \begin{ttbox}

 Hilbert = Base +

 Hilbert = Base +

 consts

 consts

 rules

 rules

   K     "P --> Q --> P"

   K     "P --> Q --> P"

   S     "(P --> Q --> R) --> (P --> Q) --> P --> R"

   S     "(P --> Q --> R) --> (P --> Q) --> P --> R"

   MP    "[| P --> Q; P |] ==> Q"

   MP    "[| P --> Q; P |] ==> Q"

 end

 end

 define but difficult to use.  The following natural deduction formulation is

 define but difficult to use.  The following natural deduction formulation is

 better:

 better:

 \begin{ttbox}

 \begin{ttbox}

 MinI = Base +

 MinI = Base +

 consts

 consts

 rules

 rules

   impI  "(P ==> Q) ==> P --> Q"

   impI  "(P ==> Q) ==> P --> Q"

   impE  "[| P --> Q; P |] ==> Q"

   impE  "[| P --> Q; P |] ==> Q"

 end

 end

 \end{ttbox}

 \end{ttbox}

 We may easily extend minimal logic with falsity:

 We may easily extend minimal logic with falsity:

 \begin{ttbox}

 \begin{ttbox}

 MinIF = MinI +

 MinIF = MinI +

 consts

 consts

 rules

 rules

   FalseE "False ==> P"

   FalseE "False ==> P"

 end

 end

 \end{ttbox}

 \end{ttbox}

 On the other hand, we may wish to introduce conjunction only:

 On the other hand, we may wish to introduce conjunction only:

 \begin{ttbox}

 \begin{ttbox}

 MinC = Base +

 MinC = Base +

 consts

 consts

 \ttbreak

 \ttbreak

 rules

 rules

   conjI  "[| P; Q |] ==> P & Q"

   conjI  "[| P; Q |] ==> P & Q"

   conjE1 "P & Q ==> P"

   conjE1 "P & Q ==> P"

   conjE2 "P & Q ==> Q"

   conjE2 "P & Q ==> Q"