Next:The module system Up:Natural Commands Previous:The syntax of the Contents

Semantics

$\begin{definition}A natural command is simple if {\tt show} is followed by the empty command. \end{definition}$

A simple command in a goal is interpreted as a rule that needs to be proved derivable automatically by PhoX. A natural command can be seen as a tree of simple command and is therefore interpreted as a tree of derivable rule, that is a derivable rule itself.

We will just describe the interpretation of a simple command: let us assume the current goal is $\Gamma \vdash A$ then a simple command is interpreted as a rule whose conclusion is $\Gamma \vdash A$ and whose premises are defined by induction on the structure of the command. Thus, we only need to prove the premises to prove the current goal.

First some syntactic sugar can be elliminated:

$\hbox{\tt let } I \hbox{ \tt and } I'$ is interpreted as $\hbox{\tt let } I \hbox{ \tt let } I'$
$\hbox{\tt let } x_1,\dots,x_n \star P$ (where $\star$ is or an infix symbol is interpreted as $\hbox{\tt let } x_1 \star P \dots \hbox{\tt let } x_n \star P$
$\hbox{\tt let } x : P$ is interpreted as $\hbox{\tt let } x \hbox{ \tt assume } P x$
$\hbox{\tt let } x \star P$ is interpreted as $\hbox{\tt let } x \hbox{ \tt assume } x \star P$ where $\star$ is an infix symbol.
The keyword deduce is interpreted as assume.
$\hbox{\tt assume } A_1 \hbox{ \tt and } \dots \hbox{ \tt and } A_n$ is interpreted as $\hbox{\tt assume } A_1 \hbox{ \tt assume } \dots \hbox{ \tt assume } A_n$

Then the set of premises $\vert C\vert$ associated to the simple command if the current goal is $\Gamma \vdash A$ is defined by

$\begin{displaymath} \begin{array}{lcl} \vert\hbox{\tt let } x \; C\vert &=& \ver... ...\tt begin } C \hbox{\tt end }\vert &=& \vert C\vert \end{array}\end{displaymath}$

Next:The module system Up:Natural Commands Previous:The syntax of the Contents

Christophe Raffalli 2005-03-02