Method rule_tac understands Isar contexts: documentation.
--- a/NEWS Fri Aug 29 15:19:02 2003 +0200
+++ b/NEWS Fri Aug 29 15:40:11 2003 +0200
@@ -17,6 +17,22 @@
symbols. Call 'isatool fixgreek' to try to fix parsing errors in
existing theory and ML files.
+*** Isar ***
+
+* Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
+
+ - Now understand static (Isar) contexts. As a consequence, users of Isar
+ locales are no longer forced to write Isar proof scripts.
+ For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
+ emulations.
+ - INCOMPATIBILITY: names of variables to be instantiated may no
+ longer be enclosed in quotes. Instead, precede variable names containing
+ dots with `?'. This is consistent with the instantiation attribute
+ "where".
+
+* HOL: Tactic emulation methods induct_tac and case_tac understand static
+ (Isar) contexts.
+
*** HOL ***
* 'specification' command added, allowing for definition by
--- a/doc-src/IsarRef/generic.tex Fri Aug 29 15:19:02 2003 +0200
+++ b/doc-src/IsarRef/generic.tex Fri Aug 29 15:40:11 2003 +0200
@@ -437,7 +437,7 @@
\indexisaratt{tagged}\indexisaratt{untagged}
\indexisaratt{THEN}\indexisaratt{COMP}
-\indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded}
+\indexisaratt{unfolded}\indexisaratt{folded}
\indexisaratt{standard}\indexisarattof{Pure}{elim-format}
\indexisaratt{no-vars}
\begin{matharray}{rcl}
@@ -445,7 +445,6 @@
untagged & : & \isaratt \\[0.5ex]
THEN & : & \isaratt \\
COMP & : & \isaratt \\[0.5ex]
- where & : & \isaratt \\[0.5ex]
unfolded & : & \isaratt \\
folded & : & \isaratt \\[0.5ex]
elim_format & : & \isaratt \\
@@ -460,8 +459,6 @@
;
('THEN' | 'COMP') ('[' nat ']')? thmref
;
- 'where' (name '=' term * 'and')
- ;
('unfolded' | 'folded') thmrefs
;
\end{rail}
@@ -480,11 +477,6 @@
normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
\cite[\S5]{isabelle-ref}).
-\item [$where~\vec x = \vec t$] perform named instantiation of schematic
- variables occurring in a theorem. Unlike instantiation tactics such as
- $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
- have to be specified on the left-hand side (e.g.\ $\Var{x@3}$).
-
\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
given meta-level definitions throughout a rule.
@@ -513,15 +505,23 @@
dynamic instantiation within the scope of some subgoal.
\begin{warn}
- Dynamic instantiations are read and type-checked according to a subgoal of
- the current dynamic goal state, rather than the static proof context! In
- particular, locally fixed variables and term abbreviations may not be
- included in the term specifications. Thus schematic variables are left to
- be solved by unification with certain parts of the subgoal involved.
+ Dynamic instantiations refer to universally quantified parameters of
+ a subgoal (the dynamic context) rather than fixed variables and term
+ abbreviations of a (static) Isar context.
\end{warn}
+Tactic emulation methods, unlike their ML counterparts, admit
+simultaneous instantiation from both dynamic and static contexts. If
+names occur in both contexts goal parameters hide locally fixed
+variables. Likewise, schematic variables refer to term abbreviations,
+if present in the static context. Otherwise the schematic variable is
+interpreted as a schematic variable and left to be solved by unification
+with certain parts of the subgoal.
+
Note that the tactic emulation proof methods in Isabelle/Isar are consistently
-named $foo_tac$.
+named $foo_tac$. Note also that variable names occurring on left hand sides
+of instantiations must be preceded by a question mark if they contain dots.
+This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}).
\indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
\indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
--- a/doc-src/IsarRef/pure.tex Fri Aug 29 15:19:02 2003 +0200
+++ b/doc-src/IsarRef/pure.tex Fri Aug 29 15:40:11 2003 +0200
@@ -963,7 +963,7 @@
\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
-\indexisaratt{OF}\indexisaratt{of}
+\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
\begin{matharray}{rcl}
- & : & \isarmeth \\
assumption & : & \isarmeth \\
@@ -976,6 +976,7 @@
rule & : & \isaratt \\[0.5ex]
OF & : & \isaratt \\
of & : & \isaratt \\
+ where & : & \isaratt \\
\end{matharray}
\begin{rail}
@@ -993,6 +994,8 @@
;
'of' insts ('concl' ':' insts)?
;
+ 'where' (name '=' term * 'and')
+ ;
\end{rail}
\begin{descr}
@@ -1058,6 +1061,11 @@
following a ``$concl\colon$'' specification refer to positions of the
conclusion of a rule.
+\item [$where~\vec x = \vec t$] performs named instantiation of schematic
+ variables occurring in a theorem. Schematic variables
+ have to be specified on the left-hand side (e.g.\ $?x1\!.\!3$). The
+ question mark may be omitted if the variable name does not contain a dot.
+
\end{descr}
--- a/doc-src/IsarRef/refcard.tex Fri Aug 29 15:19:02 2003 +0200
+++ b/doc-src/IsarRef/refcard.tex Fri Aug 29 15:40:11 2003 +0200
@@ -118,8 +118,9 @@
\begin{tabular}{ll}
\multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
- $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\
- $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
+ $OF~\vec a$ & rule resolved with facts (skipping ``$_$'') \\
+ $of~\vec t$ & rule instantiated with terms (skipping ``$_$'') \\
+ $where~\vec x = \vec t$ & rule instantiated with terms, by variable name \\
$symmetric$ & resolution with symmetry rule \\
$THEN~b$ & resolution with another rule \\
$rule_format$ & result put into standard rule format \\