summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Mon, 04 Apr 1994 17:09:45 +0200 | |

changeset 307 | 994dbab40849 |

parent 306 | eee166d4a532 |

child 308 | f4cecad9b6a0 |

modifications towards final draft

--- a/doc-src/Intro/advanced.tex Wed Mar 30 17:31:18 1994 +0200 +++ b/doc-src/Intro/advanced.tex Mon Apr 04 17:09:45 1994 +0200 @@ -36,15 +36,15 @@ \label{deriving-example} \index{examples!of deriving rules} -The subgoal module supports the derivation of rules. The \ttindex{goal} -command, when supplied a goal of the form $\List{\theta@1; \ldots; -\theta@k} \Imp \phi$, creates $\phi\Imp\phi$ as the initial proof state and -returns a list consisting of the theorems -${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These meta-assumptions are -also recorded internally, allowing \ttindex{result} to discharge them in the -original order. +The subgoal module supports the derivation of rules, as discussed in +\S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of the +form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$ +as the initial proof state and returns a list consisting of the theorems +${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These meta-assumptions +are also recorded internally, allowing \ttindex{result} to discharge them +in the original order. -Let us derive $\conj$ elimination~(\S\ref{deriving}) using Isabelle. +Let us derive $\conj$ elimination using Isabelle. Until now, calling \ttindex{goal} has returned an empty list, which we have thrown away. In this example, the list contains the two premises of the rule. We bind them to the \ML\ identifiers {\tt major} and {\tt @@ -353,7 +353,7 @@ The {\ML} section contains code to perform arbitrary syntactic transformations. The main declaration forms are discussed below. The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the - appendix of the {\it Reference Manual}}{Appendix~\ref{app:TheorySyntax}}. + appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}. All the declaration parts can be omitted. In the simplest case, $T$ is just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one @@ -518,28 +518,26 @@ translator passes them verbatim to the {\ML} output file. \end{warn} -\subsection{Type synonyms} -\indexbold{types!synonyms}\index{types!abbreviations|see{synonyms}} - +\subsection{Type synonyms}\indexbold{types!synonyms} Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar -to those found in ML. Such synonyms are defined in the type declaration part +to those found in \ML. Such synonyms are defined in the type declaration part and are fairly self explanatory: \begin{ttbox} -types gate = "[o,o] => o" - 'a pred = "'a => o" +types gate = "[o,o] => o" + 'a pred = "'a => o" ('a,'b)nuf = "'b => 'a" \end{ttbox} Type declarations and synonyms can be mixed arbitrarily: \begin{ttbox} types nat 'a stream = "nat => 'a" - signal = "nat stream" + signal = "nat stream" 'a list \end{ttbox} -A synonym is merely an abbreviation for some existing type expression. Hence -synonyms may not be recursive! Internally all synonyms are fully expanded. As -a consequence Isabelle output never contains synonyms. Their main purpose is -to improve the readability of theories. Synonyms can be used just like any +A synonym is merely an abbreviation for some existing type expression. Hence +synonyms may not be recursive! Internally all synonyms are fully expanded. As +a consequence Isabelle output never contains synonyms. Their main purpose is +to improve the readability of theories. Synonyms can be used just like any other type: \begin{ttbox} consts and,or :: "gate" @@ -641,7 +639,7 @@ \(id\) < \(c@1\), \ldots, \(c@k\) \end{ttbox} Type classes allow constants to be overloaded. As suggested in -\S\ref{polymorphic}, let us define the class $arith$ of ``arithmetic'' +\S\ref{polymorphic}, let us define the class $arith$ of arithmetic types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::} \alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of $term$ and add the three polymorphic constants of this class. @@ -699,7 +697,7 @@ including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$. Let us introduce the Peano axioms for mathematical induction and the freeness of $0$ and~$Suc$: -\[ \vcenter{\infer[(induct)*]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}} +\[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}} \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$} \] \[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad @@ -752,7 +750,9 @@ \index{examples!of theories} Let us create the theory \ttindexbold{Nat} starting from theory~\verb$FOL$, which contains only classical logic with no natural numbers. We declare -the 0-place type constructor $nat$ and the constants $rec$ and~$Suc$: +the 0-place type constructor $nat$ and the associated constants. Note that +the constant~0 requires a mixfix annotation because~0 is not a legal +identifier, and could not otherwise be written in terms: \begin{ttbox} Nat = FOL + types nat @@ -835,7 +835,7 @@ \end{description} The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$, where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule --- -with no leading question marks!! --- and $e@1$, \ldots, $e@n$ are +with no leading question marks! --- and $e@1$, \ldots, $e@n$ are expressions giving their instantiations. The expressions are type-checked in the context of a particular subgoal: free variables receive the same types as they have in the subgoal, and parameters may appear. Type