--- a/doc-src/Intro/getting.tex Tue Apr 07 13:46:34 1998 +0200
+++ b/doc-src/Intro/getting.tex Thu Apr 09 12:29:39 1998 +0200
@@ -17,9 +17,17 @@
tacticals have function types such as {\tt tactic->tactic}. Isabelle
users can operate on these data structures by writing \ML{} programs.
+
\section{Forward proof}\label{sec:forward} \index{forward proof|(}
This section describes the concrete syntax for types, terms and theorems,
-and demonstrates forward proof.
+and demonstrates forward proof. The examples are set in first-order logic.
+The command to start Isabelle running first-order logic is
+\begin{ttbox}
+isabelle FOL
+\end{ttbox}
+Note that just typing \texttt{isabelle} usually brings up higher-order logic
+(\HOL) by default.
+
\subsection{Lexical matters}
\index{identifiers}\index{reserved words}
@@ -76,16 +84,15 @@
\index{*:: symbol}\index{*=> symbol}
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
\index{*[ symbol}\index{*] symbol}
-\begin{array}{lll}
- \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
- \alpha "::" C & \alpha :: C & \hbox{class constraint} \\
+\begin{array}{ll}
+ \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline
+ \alpha "::" C & \hbox{class constraint} \\
\alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &
- \alpha :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\
- \sigma " => " \tau & \sigma\To\tau & \hbox{function type} \\
- "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
- [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\
- "(" \tau@1"," \ldots "," \tau@n ")" tycon &
- (\tau@1, \ldots, \tau@n)tycon & \hbox{type construction}
+ \hbox{sort constraint} \\
+ \sigma " => " \tau & \hbox{function type } \sigma\To\tau \\
+ "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau
+ & \hbox{$n$-argument function type} \\
+ "(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction}
\end{array}
\]
Terms are those of the typed $\lambda$-calculus.
@@ -93,16 +100,19 @@
\[\dquotes
\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions}
\index{*:: symbol}
-\begin{array}{lll}
- \multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
- t "::" \sigma & t :: \sigma & \hbox{type constraint} \\
- "\%" x "." t & \lambda x.t & \hbox{abstraction} \\
- "\%" x@1\ldots x@n "." t & \lambda x@1\ldots x@n.t &
- \hbox{curried abstraction} \\
- t "(" u@1"," \ldots "," u@n ")" &
- t (u@1, \ldots, u@n) & \hbox{curried application}
+\begin{array}{ll}
+ \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
+ t "::" \sigma & \hbox{type constraint} \\
+ "\%" x "." t & \hbox{abstraction } \lambda x.t \\
+ "\%" x@1\ldots x@n "." t & \hbox{abstraction over several arguments} \\
+ t "(" u@1"," \ldots "," u@n ")" &
+ \hbox{application to several arguments (FOL and ZF)} \\
+ t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}
\end{array}
\]
+Note that \HOL{} uses its traditional ``higher-order'' syntax for application,
+which differs from that used in \FOL\@.
+
The theorems and rules of an object-logic are represented by theorems in
the meta-logic, which are expressed using meta-formulae. Since the
meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}
--- a/doc-src/Intro/intro.ind Tue Apr 07 13:46:34 1998 +0200
+++ b/doc-src/Intro/intro.ind Thu Apr 09 12:29:39 1998 +0200
@@ -1,27 +1,27 @@
\begin{theindex}
- \item {\tt !!} symbol, 25
+ \item {\tt !!} symbol, 26
\subitem in main goal, 46
\item {\tt\%} symbol, 25
\item {\tt ::} symbol, 25
- \item {\tt ==} symbol, 25
- \item {\tt ==>} symbol, 25
+ \item {\tt ==} symbol, 26
+ \item {\tt ==>} symbol, 26
\item {\tt =>} symbol, 25
- \item {\tt =?=} symbol, 25
+ \item {\tt =?=} symbol, 26
\item {\tt [} symbol, 25
- \item {\tt [|} symbol, 25
+ \item {\tt [|} symbol, 26
\item {\tt ]} symbol, 25
\item {\tt\ttlbrace} symbol, 25
\item {\tt\ttrbrace} symbol, 25
- \item {\tt |]} symbol, 25
+ \item {\tt |]} symbol, 26
\indexspace
- \item {\tt allI} theorem, 37
+ \item {\tt allI} theorem, 38
\item arities
\subitem declaring, 4, \bold{49}
\item {\tt Asm_simp_tac}, 60
- \item {\tt assume_tac}, 30, 32, 37, 47
+ \item {\tt assume_tac}, 30, 32, 38, 47
\item assumptions
\subitem deleting, 20
\subitem discharge of, 7
@@ -39,13 +39,13 @@
\subitem Prolog style, 62
\item {\tt bd}, 31
\item {\tt be}, 31
- \item {\tt Blast_tac}, 39
+ \item {\tt Blast_tac}, 39, 40
\item {\tt br}, 31
- \item {\tt by}, 30
+ \item {\tt by}, 31
\indexspace
- \item {\tt choplev}, 37, 65
+ \item {\tt choplev}, 37, 38, 65
\item classes, 3
\subitem built-in, \bold{25}
\item classical reasoner, 39
@@ -65,7 +65,7 @@
\item destruct-resolution, 22, 30
\item {\tt disjE} theorem, 31
\item {\tt dres_inst_tac}, 57
- \item {\tt dresolve_tac}, 30, 32, 33, 38
+ \item {\tt dresolve_tac}, 30, 33, 39
\indexspace
@@ -74,22 +74,22 @@
\item equality
\subitem polymorphic, 3
\item {\tt eres_inst_tac}, 57
- \item {\tt eresolve_tac}, 30, 32, 33, 39, 47
+ \item {\tt eresolve_tac}, 30, 33, 39, 47
\item examples
\subitem of deriving rules, 41
\subitem of induction, 57, 58
\subitem of simplification, 60
\subitem of tacticals, 37
\subitem of theories, 48, 50--54, 56, 61
- \subitem propositional, 17, 31, 32
- \subitem with quantifiers, 18, 34, 35, 38
+ \subitem propositional, 17, 31, 33
+ \subitem with quantifiers, 18, 34, 36, 38
\item {\tt exE} theorem, 38
\indexspace
\item {\tt FalseE} theorem, 45
\item first-order logic, 1
- \item flex-flex constraints, 6, 25, \bold{28}
+ \item flex-flex constraints, 6, 26, \bold{29}
\item {\tt flexflex_rule}, 29
\item forward proof, 21, 24--30
\item {\tt fun} type, 1, 4
@@ -132,9 +132,9 @@
\item {\tt Match} exception, 42
\item meta-assumptions
\subitem syntax of, 22
- \item meta-equality, \bold{5}, 25
- \item meta-implication, \bold{5}, 7, 25
- \item meta-quantifiers, \bold{5}, 8, 25
+ \item meta-equality, \bold{5}, 26
+ \item meta-implication, \bold{5}, 7, 26
+ \item meta-quantifiers, \bold{5}, 8, 26
\item meta-rewriting, 43
\item mixfix declarations, 52, 53, 56
\item ML, i
@@ -181,7 +181,7 @@
\item {\tt read_instantiate}, 29
\item {\tt refl} theorem, 29
- \item {\tt REPEAT}, 33, 38, 62, 64
+ \item {\tt REPEAT}, 34, 38, 62, 64
\item {\tt res_inst_tac}, 57, 60
\item reserved words, 24
\item resolution, 10, \bold{12}
@@ -213,7 +213,7 @@
\item simplification sets, 60
\item sort constraints, 25
\item sorts, \bold{5}
- \item {\tt spec} theorem, 28, 36, 37
+ \item {\tt spec} theorem, 28, 36, 38
\item {\tt standard}, 27
\item substitution, \bold{8}
\item {\tt Suc_inject}, 58
@@ -237,10 +237,10 @@
\subitem defining, 47--57
\item {\tt thm} ML type, 27
\item {\tt topthm}, 42
- \item {\tt Trueprop} constant, 6, 7, 25
+ \item {\tt Trueprop} constant, 6, 7, 26
\item type constraints, 25
\item type constructors, 1
- \item type identifiers, 24
+ \item type identifiers, 25
\item type synonyms, \bold{51}
\item types
\subitem declaring, \bold{49}
@@ -252,12 +252,12 @@
\indexspace
- \item {\tt undo}, 30
+ \item {\tt undo}, 31
\item unification
\subitem higher-order, \bold{11}, 58
\subitem incompleteness of, 11
- \item unknowns, 10, 24, 34
- \subitem function, \bold{11}, 28, 34
+ \item unknowns, 10, 25, 34
+ \subitem function, \bold{11}, 29, 34
\item {\tt use_thy}, \bold{47, 48}
\indexspace