1.1 --- a/doc-src/IsarRef/pure.tex Tue Mar 05 18:54:55 2002 +0100
1.2 +++ b/doc-src/IsarRef/pure.tex Tue Mar 05 18:55:46 2002 +0100
1.3 @@ -291,19 +291,20 @@
1.4 \end{rail}
1.5
1.6 \begin{descr}
1.7 +
1.8 \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
1.9 except that the actual logical signature extension is omitted. Thus the
1.10 context free grammar of Isabelle's inner syntax may be augmented in
1.11 arbitrary ways, independently of the logic. The $mode$ argument refers to
1.12 - the print mode that the grammar rules belong; unless the \texttt{output}
1.13 - flag is given, all productions are added both to the input and output
1.14 - grammar.
1.15 + the print mode that the grammar rules belong; unless the
1.16 + $\isarkeyword{output}$ indicator is given, all productions are added both to
1.17 + the input and output grammar.
1.18 +
1.19 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
1.20 - rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==} or
1.21 - \isasymrightleftharpoons), parse rules (\texttt{=>} or
1.22 - \isasymrightharpoonup), or print rules (\texttt{<=} or
1.23 - \isasymleftharpoondown). Translation patterns may be prefixed by the
1.24 - syntactic category to be used for parsing; the default is \texttt{logic}.
1.25 + rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse
1.26 + rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).
1.27 + Translation patterns may be prefixed by the syntactic category to be used
1.28 + for parsing; the default is $logic$.
1.29 \end{descr}
1.30
1.31
1.32 @@ -333,7 +334,7 @@
1.33 Everyday work is typically done the hard way, with proper definitions and
1.34 actual proven theorems.
1.35
1.36 -\item [$\isarkeyword{lemmas}~a = \vec b$] restrieves and stores existing facts
1.37 +\item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores existing facts
1.38 in the theory context, or the specified locale (see also
1.39 \S\ref{sec:locale}). Typical applications would also involve attributes, to
1.40 declare Simplifier rules, for example.
1.41 @@ -933,43 +934,59 @@
1.42 object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
1.43 \ref{ch:logics}).
1.44
1.45 -\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
1.46 -\indexisaratt{OF}\indexisaratt{of}
1.47 +\indexisarmeth{$-$}\indexisarmeth{assumption}
1.48 +\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
1.49 \indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
1.50 \indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
1.51 +\indexisaratt{OF}\indexisaratt{of}
1.52 \begin{matharray}{rcl}
1.53 + - & : & \isarmeth \\
1.54 assumption & : & \isarmeth \\
1.55 this & : & \isarmeth \\
1.56 rule & : & \isarmeth \\
1.57 - - & : & \isarmeth \\
1.58 - OF & : & \isaratt \\
1.59 - of & : & \isaratt \\
1.60 + rules & : & \isarmeth \\[0.5ex]
1.61 intro & : & \isaratt \\
1.62 elim & : & \isaratt \\
1.63 dest & : & \isaratt \\
1.64 - rule & : & \isaratt \\
1.65 + rule & : & \isaratt \\[0.5ex]
1.66 + OF & : & \isaratt \\
1.67 + of & : & \isaratt \\
1.68 \end{matharray}
1.69
1.70 -%FIXME intro!, intro, intro?
1.71 -
1.72 \begin{rail}
1.73 'rule' thmrefs?
1.74 ;
1.75 + 'rules' ('!' ?) (rulemod *)
1.76 + ;
1.77 + rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
1.78 + ;
1.79 + ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
1.80 + ;
1.81 + 'rule' 'del'
1.82 + ;
1.83 'OF' thmrefs
1.84 ;
1.85 'of' insts ('concl' ':' insts)?
1.86 ;
1.87 - 'rule' 'del'
1.88 - ;
1.89 \end{rail}
1.90
1.91 \begin{descr}
1.92 +
1.93 +\item [``$-$''] does nothing but insert the forward chaining facts as premises
1.94 + into the goal. Note that command $\PROOFNAME$ without any method actually
1.95 + performs a single reduction step using the $rule$ method; thus a plain
1.96 + \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$
1.97 + alone.
1.98 +
1.99 \item [$assumption$] solves some goal by a single assumption step. Any facts
1.100 given (${} \le 1$) are guaranteed to participate in the refinement. Recall
1.101 that $\QEDNAME$ (see \S\ref{sec:proof-steps}) already concludes any
1.102 - remaining sub-goals by assumption.
1.103 + remaining sub-goals by assumption, so structured proofs usually need not
1.104 + quote the $assumption$ method at all.
1.105 +
1.106 \item [$this$] applies all of the current facts directly as rules. Recall
1.107 that ``$\DOT$'' (dot) abbreviates $\BY{this}$.
1.108 +
1.109 \item [$rule~\vec a$] applies some rule given as argument in backward manner;
1.110 facts are used to reduce the rule before applying it to the goal. Thus
1.111 $rule$ without facts is plain \emph{introduction}, while with facts it
1.112 @@ -980,27 +997,41 @@
1.113 $elim$, $dest$ attributes (see below). This is the default behavior of
1.114 $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
1.115 \S\ref{sec:proof-steps}).
1.116 -\item [``$-$''] does nothing but insert the forward chaining facts as premises
1.117 - into the goal. Note that command $\PROOFNAME$ without any method actually
1.118 - performs a single reduction step using the $rule$ method; thus a plain
1.119 - \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$
1.120 - alone.
1.121 +
1.122 +\item [$rules$] performs intuitionistic proof search, depending on
1.123 + specifically declared rules from the context, or given as explicit
1.124 + arguments. Chained facts are inserted into the goal before commencing proof
1.125 + search; $rules!$ means to include the current $prems$ as well.
1.126 +
1.127 + Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$''
1.128 + indicator refers to ``safe'' rules, which may be applied aggressively
1.129 + (without considering back-tracking later). Rules declared with ``$?$'' are
1.130 + ignored in proof search (the single-step $rule$ method still observes
1.131 + these). An explicit weight annotation may be given as well; otherwise the
1.132 + number of rule premises will be taken into account.
1.133 +
1.134 +\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
1.135 + destruct rules, to be used with the $rule$ and $rules$ methods. Note that
1.136 + the latter will ignore rules declare with ``$?$'', while ``$!$'' are used
1.137 + most aggressively.
1.138 +
1.139 + The classical reasoner (see \S\ref{sec:classical-basic}) introduces its own
1.140 + variants of these attributes; use qualified names to access the present
1.141 + versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$.
1.142 +
1.143 +\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
1.144 +
1.145 \item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in
1.146 parallel). This corresponds to the \texttt{MRS} operator in ML
1.147 \cite[\S5]{isabelle-ref}, but note the reversed order. Positions may be
1.148 skipped by including ``$\_$'' (underscore) as argument.
1.149 +
1.150 \item [$of~\vec t$] performs positional instantiation. The terms $\vec t$ are
1.151 substituted for any schematic variables occurring in a theorem from left to
1.152 right; ``\texttt{_}'' (underscore) indicates to skip a position. Arguments
1.153 following a ``$concl\colon$'' specification refer to positions of the
1.154 conclusion of a rule.
1.155 -\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
1.156 - destruct rules, respectively. Note that the classical reasoner (see
1.157 - \S\ref{sec:classical-basic}) introduces different versions of these
1.158 - attributes, and the $rule$ method, too. In object-logics with classical
1.159 - reasoning enabled, the latter version should be used all the time to avoid
1.160 - confusion!
1.161 -\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
1.162 +
1.163 \end{descr}
1.164
1.165