--- a/doc-src/IsarRef/generic.tex Thu Sep 07 20:59:37 2000 +0200
+++ b/doc-src/IsarRef/generic.tex Thu Sep 07 21:06:55 2000 +0200
@@ -305,43 +305,41 @@
\indexisaratt{standard}
-\indexisaratt{elimify}
+\indexisaratt{elimified}
\indexisaratt{no-vars}
\indexisaratt{THEN}\indexisaratt{COMP}
-\indexisaratt{where}
-\indexisaratt{tag}\indexisaratt{untag}
-\indexisaratt{export}
-\indexisaratt{unfold}\indexisaratt{fold}
+\indexisaratt{where}\indexisaratt{tagged}\indexisaratt{untagged}
+\indexisaratt{unfolded}\indexisaratt{folded}\indexisaratt{exported}
\begin{matharray}{rcl}
- tag & : & \isaratt \\
- untag & : & \isaratt \\[0.5ex]
+ tagged & : & \isaratt \\
+ untagged & : & \isaratt \\[0.5ex]
THEN & : & \isaratt \\
COMP & : & \isaratt \\[0.5ex]
where & : & \isaratt \\[0.5ex]
- unfold & : & \isaratt \\
- fold & : & \isaratt \\[0.5ex]
+ unfolded & : & \isaratt \\
+ folded & : & \isaratt \\[0.5ex]
standard & : & \isaratt \\
- elimify & : & \isaratt \\
+ elimified & : & \isaratt \\
no_vars & : & \isaratt \\
- export^* & : & \isaratt \\
+ exported^* & : & \isaratt \\
\end{matharray}
\begin{rail}
- 'tag' (nameref+)
+ 'tagged' (nameref+)
;
- 'untag' name
+ 'untagged' name
;
('THEN' | 'COMP') nat? thmref
;
'where' (name '=' term * 'and')
;
- ('unfold' | 'fold') thmrefs
+ ('unfolded' | 'folded') thmrefs
;
\end{rail}
\begin{descr}
-\item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
+\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
theorem. Tags may be any list of strings that serve as comment for some
tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
result). The first string is considered the tag name, the rest its
@@ -354,24 +352,18 @@
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 (e.g.\ $\Var{x@3}$).
-
-\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
- meta-level definitions throughout a rule.
-
+\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
+ given meta-level definitions throughout a rule.
\item [$standard$] puts a theorem into the standard form of object-rules, just
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
-
-\item [$elimify$] turns an destruction rule into an elimination, just as the
+\item [$elimified$] turns an destruction rule into an elimination, just as the
ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
-
\item [$no_vars$] replaces schematic variables by free ones; this is mainly
for tuning output of pretty printed theorems.
-
-\item [$export$] lifts a local result out of the current proof context,
+\item [$exported$] lifts a local result out of the current proof context,
generalizing all fixed variables and discharging all assumptions. Note that
proper incremental export is already done as part of the basic Isar
machinery. This attribute is mainly for experimentation.
-
\end{descr}
@@ -601,21 +593,30 @@
\subsection{Forward simplification}
-\indexisaratt{simplify}\indexisaratt{asm-simplify}
-\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
+\indexisaratt{simplified}
\begin{matharray}{rcl}
- simplify & : & \isaratt \\
- asm_simplify & : & \isaratt \\
- full_simplify & : & \isaratt \\
- asm_full_simplify & : & \isaratt \\
+ simplified & : & \isaratt \\
\end{matharray}
-These attributes provide forward rules for simplification, which should be
-used only very rarely. There are no separate options for declaring
-simplification rules locally.
+\begin{rail}
+ 'simplified' opt?
+ ;
+
+ opt: '(' (noasm | noasmsimp | noasmuse) ')'
+ ;
+\end{rail}
-See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
-information.
+\begin{descr}
+\item [$simplified$] causes a theorem to be simplified according to the
+ current Simplifier context (there are no separate arguments for declaring
+ additional rules). By default the result is fully simplified, including
+ assumptions and conclusion. The options $no_asm$ etc.\ restrict the
+ Simplifier in the same way as the for the $simp$ method (see
+ \S\ref{sec:simp}).
+
+ The $simplified$ operation should be used only very rarely, usually for
+ experimentation only.
+\end{descr}
\section{Basic equational reasoning}\label{sec:basic-eq}
@@ -818,7 +819,7 @@
\item [$delrule$] deletes introduction or elimination rules from the context.
Note that destruction rules would have to be turned into elimination rules
- first, e.g.\ by using the $elimify$ attribute.
+ first, e.g.\ by using the $elimified$ attribute.
\end{descr}
--- a/doc-src/IsarRef/hol.tex Thu Sep 07 20:59:37 2000 +0200
+++ b/doc-src/IsarRef/hol.tex Thu Sep 07 21:06:55 2000 +0200
@@ -3,22 +3,23 @@
\section{Miscellaneous attributes}
-\indexisaratt{rulify}\indexisaratt{rulify-prems}
+\indexisaratt{rulified}
\begin{matharray}{rcl}
- rulify & : & \isaratt \\
- rulify_prems & : & \isaratt \\
+ rulified & : & \isaratt \\
\end{matharray}
+\begin{rail}
+ 'rulified' ('(' noasm ')')?
+ ;
+\end{rail}
+
\begin{descr}
-\item [$rulify$] puts a theorem into object-rule form, replacing implication
- and universal quantification of HOL by the corresponding meta-logical
- connectives. This is the same operation as performed in
- \texttt{qed_spec_mp} in ML.
-
-\item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a
- rule.
-
+\item [$rulified$] causes a theorem to be put into standard object-rule form,
+ replacing implication and (bounded) universal quantification of HOL by the
+ corresponding meta-logical connectives. By default, the result is fully
+ normalized, including assumptions and conclusions at any depth. The
+ $no_asm$ option restricts the transformation to the conclusion of a rule.
\end{descr}
--- a/doc-src/IsarRef/refcard.tex Thu Sep 07 20:59:37 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex Thu Sep 07 21:06:55 2000 +0200
@@ -113,21 +113,21 @@
\section{Attributes}
\begin{tabular}{ll}
- \multicolumn{2}{l}{\textbf{Manipulate rules}} \\[0.5ex]
- $OF~\vec a$ & apply rule to facts (skipping ``$_$'') \\
- $of~\vec t$ & apply rule to terms (skipping ``$_$'') \\
- $THEN~b$ & resolve fact with rule \\
- $symmetric$ & apply symmetry of equality \\
- $standard$ & put into standard result form \\
- $rulify$ & put into object-rule form \\
- $elimify$ & put destruction rule into elimination form \\[1ex]
+ \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
+ $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\
+ $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
+ $symmetric$ & resolution with symmetry of equality \\
+ $THEN~b$ & resolution with other rule \\
+ $rulified$ & result put into standard rule form \\
+ $elimified$ & destruct rule turned into elimination rule \\
+ $standard$ & result put into standard form \\[1ex]
- \multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex]
- $simp$ & declare Simplifier rules \\
- $split$ & declare Splitter rules \\
- $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``!'' or ``?'') \\
- $iff$ & declare Simplifier + Classical Reasoner rules \\
- $trans$ & declare calculational rules (general transitivity) \\
+ \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
+ $simp$ & Simplifier rule \\
+ $intro$, $elim$, $dest$ & Classical Reasoner rule \\
+ $iff$ & Simplifier + Classical Reasoner rule \\
+ $split$ & case split rule \\
+ $trans$ & transitivity rule \\
\end{tabular}