1.1 --- a/doc-src/Ref/tactic.tex Fri Nov 21 15:40:56 1997 +0100
1.2 +++ b/doc-src/Ref/tactic.tex Fri Nov 21 15:41:27 1997 +0100
1.3 @@ -437,7 +437,7 @@
1.4 \end{ttdescription}
1.5
1.6
1.7 -\section{Managing lots of rules}
1.8 +\section{*Managing lots of rules}
1.9 These operations are not intended for interactive use. They are concerned
1.10 with the processing of large numbers of rules in automatic proof
1.11 strategies. Higher-order resolution involving a long list of rules is
1.12 @@ -559,17 +559,17 @@
1.13 \end{ttdescription}
1.14
1.15
1.16 -\section{Programming tools for proof strategies}
1.17 +\section{*Programming tools for proof strategies}
1.18 Do not consider using the primitives discussed in this section unless you
1.19 really need to code tactics from scratch.
1.20
1.21 \subsection{Operations on type {\tt tactic}}
1.22 \index{tactics!primitives for coding} A tactic maps theorems to sequences of
1.23 theorems. The type constructor for sequences (lazy lists) is called
1.24 -\mltydx{Sequence.seq}. To simplify the types of tactics and tacticals,
1.25 +\mltydx{Seq.seq}. To simplify the types of tactics and tacticals,
1.26 Isabelle defines a type abbreviation:
1.27 \begin{ttbox}
1.28 -type tactic = thm -> thm Sequence.seq
1.29 +type tactic = thm -> thm Seq.seq
1.30 \end{ttbox}
1.31 The following operations provide means for coding tactics in a clean style.
1.32 \begin{ttbox}
1.33 @@ -616,90 +616,82 @@
1.34 \end{ttdescription}
1.35
1.36
1.37 -\section{Sequences}
1.38 +\section{*Sequences}
1.39 \index{sequences (lazy lists)|bold}
1.40 -The module {\tt Sequence} declares a type of lazy lists. It uses
1.41 +The module {\tt Seq} declares a type of lazy lists. It uses
1.42 Isabelle's type \mltydx{option} to represent the possible presence
1.43 (\ttindexbold{Some}) or absence (\ttindexbold{None}) of
1.44 a value:
1.45 \begin{ttbox}
1.46 datatype 'a option = None | Some of 'a;
1.47 \end{ttbox}
1.48 -For clarity, the module name {\tt Sequence} is omitted from the signature
1.49 -specifications below; for instance, {\tt null} appears instead of {\tt
1.50 - Sequence.null}.
1.51 +The {\tt Seq} structure is supposed to be accessed via fully qualified
1.52 +names and should not be \texttt{open}ed.
1.53
1.54 \subsection{Basic operations on sequences}
1.55 \begin{ttbox}
1.56 -null : 'a seq
1.57 -seqof : (unit -> ('a * 'a seq) option) -> 'a seq
1.58 -single : 'a -> 'a seq
1.59 -pull : 'a seq -> ('a * 'a seq) option
1.60 +Seq.empty : 'a seq
1.61 +Seq.make : (unit -> ('a * 'a seq) option) -> 'a seq
1.62 +Seq.single : 'a -> 'a seq
1.63 +Seq.pull : 'a seq -> ('a * 'a seq) option
1.64 \end{ttbox}
1.65 \begin{ttdescription}
1.66 -\item[Sequence.null]
1.67 -is the empty sequence.
1.68 +\item[Seq.empty] is the empty sequence.
1.69
1.70 -\item[\tt Sequence.seqof (fn()=> Some($x$,$s$))]
1.71 -constructs the sequence with head~$x$ and tail~$s$, neither of which is
1.72 -evaluated.
1.73 +\item[\tt Seq.make (fn () => Some ($x$, $xq$))] constructs the
1.74 + sequence with head~$x$ and tail~$xq$, neither of which is evaluated.
1.75
1.76 -\item[Sequence.single $x$]
1.77 +\item[Seq.single $x$]
1.78 constructs the sequence containing the single element~$x$.
1.79
1.80 -\item[Sequence.pull $s$]
1.81 -returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the
1.82 -sequence has head~$x$ and tail~$s'$. Warning: calling \hbox{Sequence.pull
1.83 -$s$} again will {\it recompute\/} the value of~$x$; it is not stored!
1.84 +\item[Seq.pull $xq$] returns {\tt None} if the sequence is empty and
1.85 + {\tt Some ($x$, $xq'$)} if the sequence has head~$x$ and tail~$xq'$.
1.86 + Warning: calling \hbox{Seq.pull $xq$} again will {\it recompute\/}
1.87 + the value of~$x$; it is not stored!
1.88 \end{ttdescription}
1.89
1.90
1.91 \subsection{Converting between sequences and lists}
1.92 \begin{ttbox}
1.93 -chop : int * 'a seq -> 'a list * 'a seq
1.94 -list_of_s : 'a seq -> 'a list
1.95 -s_of_list : 'a list -> 'a seq
1.96 +Seq.chop : int * 'a seq -> 'a list * 'a seq
1.97 +Seq.list_of : 'a seq -> 'a list
1.98 +Seq.of_list : 'a list -> 'a seq
1.99 \end{ttbox}
1.100 \begin{ttdescription}
1.101 -\item[Sequence.chop($n$,$s$)]
1.102 -returns the first~$n$ elements of~$s$ as a list, paired with the remaining
1.103 -elements of~$s$. If $s$ has fewer than~$n$ elements, then so will the
1.104 -list.
1.105 -
1.106 -\item[Sequence.list_of_s $s$]
1.107 -returns the elements of~$s$, which must be finite, as a list.
1.108 -
1.109 -\item[Sequence.s_of_list $l$]
1.110 -creates a sequence containing the elements of~$l$.
1.111 +\item[Seq.chop ($n$, $xq$)] returns the first~$n$ elements of~$xq$ as a
1.112 + list, paired with the remaining elements of~$xq$. If $xq$ has fewer
1.113 + than~$n$ elements, then so will the list.
1.114 +
1.115 +\item[Seq.list_of $xq$] returns the elements of~$xq$, which must be
1.116 + finite, as a list.
1.117 +
1.118 +\item[Seq.of_list $xs$] creates a sequence containing the elements
1.119 + of~$xs$.
1.120 \end{ttdescription}
1.121
1.122
1.123 \subsection{Combining sequences}
1.124 \begin{ttbox}
1.125 -append : 'a seq * 'a seq -> 'a seq
1.126 -interleave : 'a seq * 'a seq -> 'a seq
1.127 -flats : 'a seq seq -> 'a seq
1.128 -maps : ('a -> 'b) -> 'a seq -> 'b seq
1.129 -filters : ('a -> bool) -> 'a seq -> 'a seq
1.130 +Seq.append : 'a seq * 'a seq -> 'a seq
1.131 +Seq.interleave : 'a seq * 'a seq -> 'a seq
1.132 +Seq.flat : 'a seq seq -> 'a seq
1.133 +Seq.map : ('a -> 'b) -> 'a seq -> 'b seq
1.134 +Seq.filter : ('a -> bool) -> 'a seq -> 'a seq
1.135 \end{ttbox}
1.136 \begin{ttdescription}
1.137 -\item[Sequence.append($s@1$,$s@2$)]
1.138 -concatenates $s@1$ to $s@2$.
1.139 -
1.140 -\item[Sequence.interleave($s@1$,$s@2$)]
1.141 -joins $s@1$ with $s@2$ by interleaving their elements. The result contains
1.142 -all the elements of the sequences, even if both are infinite.
1.143 -
1.144 -\item[Sequence.flats $ss$]
1.145 -concatenates a sequence of sequences.
1.146 -
1.147 -\item[Sequence.maps $f$ $s$]
1.148 -applies $f$ to every element of~$s=x@1,x@2,\ldots$, yielding the sequence
1.149 -$f(x@1),f(x@2),\ldots$.
1.150 -
1.151 -\item[Sequence.filters $p$ $s$]
1.152 -returns the sequence consisting of all elements~$x$ of~$s$ such that $p(x)$
1.153 -is {\tt true}.
1.154 +\item[Seq.append ($xq$, $yq$)] concatenates $xq$ to $yq$.
1.155 +
1.156 +\item[Seq.interleave ($xq$, $yq$)] joins $xq$ with $yq$ by
1.157 + interleaving their elements. The result contains all the elements
1.158 + of the sequences, even if both are infinite.
1.159 +
1.160 +\item[Seq.flat $xqq$] concatenates a sequence of sequences.
1.161 +
1.162 +\item[Seq.map $f$ $xq$] applies $f$ to every element
1.163 + of~$xq=x@1,x@2,\ldots$, yielding the sequence $f(x@1),f(x@2),\ldots$.
1.164 +
1.165 +\item[Seq.filter $p$ $xq$] returns the sequence consisting of all
1.166 + elements~$x$ of~$xq$ such that $p(x)$ is {\tt true}.
1.167 \end{ttdescription}
1.168
1.169 \index{tactics|)}