improved att names;
authorwenzelm
Thu Sep 07 21:06:55 2000 +0200 (2000-09-07)
changeset 990514a71104a498
parent 9904 09253f667beb
child 9906 5c027cca6262
improved att names;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/hol.tex
doc-src/IsarRef/refcard.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Sep 07 20:59:37 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Sep 07 21:06:55 2000 +0200
     1.3 @@ -305,43 +305,41 @@
     1.4  
     1.5  
     1.6  \indexisaratt{standard}
     1.7 -\indexisaratt{elimify}
     1.8 +\indexisaratt{elimified}
     1.9  \indexisaratt{no-vars}
    1.10  
    1.11  \indexisaratt{THEN}\indexisaratt{COMP}
    1.12 -\indexisaratt{where}
    1.13 -\indexisaratt{tag}\indexisaratt{untag}
    1.14 -\indexisaratt{export}
    1.15 -\indexisaratt{unfold}\indexisaratt{fold}
    1.16 +\indexisaratt{where}\indexisaratt{tagged}\indexisaratt{untagged}
    1.17 +\indexisaratt{unfolded}\indexisaratt{folded}\indexisaratt{exported}
    1.18  \begin{matharray}{rcl}
    1.19 -  tag & : & \isaratt \\
    1.20 -  untag & : & \isaratt \\[0.5ex]
    1.21 +  tagged & : & \isaratt \\
    1.22 +  untagged & : & \isaratt \\[0.5ex]
    1.23    THEN & : & \isaratt \\
    1.24    COMP & : & \isaratt \\[0.5ex]
    1.25    where & : & \isaratt \\[0.5ex]
    1.26 -  unfold & : & \isaratt \\
    1.27 -  fold & : & \isaratt \\[0.5ex]
    1.28 +  unfolded & : & \isaratt \\
    1.29 +  folded & : & \isaratt \\[0.5ex]
    1.30    standard & : & \isaratt \\
    1.31 -  elimify & : & \isaratt \\
    1.32 +  elimified & : & \isaratt \\
    1.33    no_vars & : & \isaratt \\
    1.34 -  export^* & : & \isaratt \\
    1.35 +  exported^* & : & \isaratt \\
    1.36  \end{matharray}
    1.37  
    1.38  \begin{rail}
    1.39 -  'tag' (nameref+)
    1.40 +  'tagged' (nameref+)
    1.41    ;
    1.42 -  'untag' name
    1.43 +  'untagged' name
    1.44    ;
    1.45    ('THEN' | 'COMP') nat? thmref
    1.46    ;
    1.47    'where' (name '=' term * 'and')
    1.48    ;
    1.49 -  ('unfold' | 'fold') thmrefs
    1.50 +  ('unfolded' | 'folded') thmrefs
    1.51    ;
    1.52  \end{rail}
    1.53  
    1.54  \begin{descr}
    1.55 -\item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
    1.56 +\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
    1.57    theorem.  Tags may be any list of strings that serve as comment for some
    1.58    tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
    1.59    result).  The first string is considered the tag name, the rest its
    1.60 @@ -354,24 +352,18 @@
    1.61    variables occurring in a theorem.  Unlike instantiation tactics such as
    1.62    $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
    1.63    have to be specified (e.g.\ $\Var{x@3}$).
    1.64 -
    1.65 -\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
    1.66 -  meta-level definitions throughout a rule.
    1.67 -
    1.68 +\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
    1.69 +  given meta-level definitions throughout a rule.
    1.70  \item [$standard$] puts a theorem into the standard form of object-rules, just
    1.71    as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
    1.72 -
    1.73 -\item [$elimify$] turns an destruction rule into an elimination, just as the
    1.74 +\item [$elimified$] turns an destruction rule into an elimination, just as the
    1.75    ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
    1.76 -
    1.77  \item [$no_vars$] replaces schematic variables by free ones; this is mainly
    1.78    for tuning output of pretty printed theorems.
    1.79 -
    1.80 -\item [$export$] lifts a local result out of the current proof context,
    1.81 +\item [$exported$] lifts a local result out of the current proof context,
    1.82    generalizing all fixed variables and discharging all assumptions.  Note that
    1.83    proper incremental export is already done as part of the basic Isar
    1.84    machinery.  This attribute is mainly for experimentation.
    1.85 -
    1.86  \end{descr}
    1.87  
    1.88  
    1.89 @@ -601,21 +593,30 @@
    1.90  
    1.91  \subsection{Forward simplification}
    1.92  
    1.93 -\indexisaratt{simplify}\indexisaratt{asm-simplify}
    1.94 -\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
    1.95 +\indexisaratt{simplified}
    1.96  \begin{matharray}{rcl}
    1.97 -  simplify & : & \isaratt \\
    1.98 -  asm_simplify & : & \isaratt \\
    1.99 -  full_simplify & : & \isaratt \\
   1.100 -  asm_full_simplify & : & \isaratt \\
   1.101 +  simplified & : & \isaratt \\
   1.102  \end{matharray}
   1.103  
   1.104 -These attributes provide forward rules for simplification, which should be
   1.105 -used only very rarely.  There are no separate options for declaring
   1.106 -simplification rules locally.
   1.107 +\begin{rail}
   1.108 +  'simplified' opt?
   1.109 +  ;
   1.110 +
   1.111 +  opt: '(' (noasm | noasmsimp | noasmuse) ')'
   1.112 +  ;
   1.113 +\end{rail}
   1.114  
   1.115 -See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
   1.116 -information.
   1.117 +\begin{descr}
   1.118 +\item [$simplified$] causes a theorem to be simplified according to the
   1.119 +  current Simplifier context (there are no separate arguments for declaring
   1.120 +  additional rules).  By default the result is fully simplified, including
   1.121 +  assumptions and conclusion.  The options $no_asm$ etc.\ restrict the
   1.122 +  Simplifier in the same way as the for the $simp$ method (see
   1.123 +  \S\ref{sec:simp}).
   1.124 +  
   1.125 +  The $simplified$ operation should be used only very rarely, usually for
   1.126 +  experimentation only.
   1.127 +\end{descr}
   1.128  
   1.129  
   1.130  \section{Basic equational reasoning}\label{sec:basic-eq}
   1.131 @@ -818,7 +819,7 @@
   1.132  
   1.133  \item [$delrule$] deletes introduction or elimination rules from the context.
   1.134    Note that destruction rules would have to be turned into elimination rules
   1.135 -  first, e.g.\ by using the $elimify$ attribute.
   1.136 +  first, e.g.\ by using the $elimified$ attribute.
   1.137  \end{descr}
   1.138  
   1.139  
     2.1 --- a/doc-src/IsarRef/hol.tex	Thu Sep 07 20:59:37 2000 +0200
     2.2 +++ b/doc-src/IsarRef/hol.tex	Thu Sep 07 21:06:55 2000 +0200
     2.3 @@ -3,22 +3,23 @@
     2.4  
     2.5  \section{Miscellaneous attributes}
     2.6  
     2.7 -\indexisaratt{rulify}\indexisaratt{rulify-prems}
     2.8 +\indexisaratt{rulified}
     2.9  \begin{matharray}{rcl}
    2.10 -  rulify & : & \isaratt \\
    2.11 -  rulify_prems & : & \isaratt \\
    2.12 +  rulified & : & \isaratt \\
    2.13  \end{matharray}
    2.14  
    2.15 +\begin{rail}
    2.16 +  'rulified' ('(' noasm ')')?
    2.17 +  ;
    2.18 +\end{rail}
    2.19 +
    2.20  \begin{descr}
    2.21    
    2.22 -\item [$rulify$] puts a theorem into object-rule form, replacing implication
    2.23 -  and universal quantification of HOL by the corresponding meta-logical
    2.24 -  connectives.  This is the same operation as performed in
    2.25 -  \texttt{qed_spec_mp} in ML.
    2.26 -  
    2.27 -\item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a
    2.28 -  rule.
    2.29 -
    2.30 +\item [$rulified$] causes a theorem to be put into standard object-rule form,
    2.31 +  replacing implication and (bounded) universal quantification of HOL by the
    2.32 +  corresponding meta-logical connectives.  By default, the result is fully
    2.33 +  normalized, including assumptions and conclusions at any depth.  The
    2.34 +  $no_asm$ option restricts the transformation to the conclusion of a rule.
    2.35  \end{descr}
    2.36  
    2.37  
     3.1 --- a/doc-src/IsarRef/refcard.tex	Thu Sep 07 20:59:37 2000 +0200
     3.2 +++ b/doc-src/IsarRef/refcard.tex	Thu Sep 07 21:06:55 2000 +0200
     3.3 @@ -113,21 +113,21 @@
     3.4  \section{Attributes}
     3.5  
     3.6  \begin{tabular}{ll}
     3.7 -  \multicolumn{2}{l}{\textbf{Manipulate rules}} \\[0.5ex]
     3.8 -  $OF~\vec a$ & apply rule to facts (skipping ``$_$'') \\
     3.9 -  $of~\vec t$ & apply rule to terms (skipping ``$_$'') \\
    3.10 -  $THEN~b$ & resolve fact with rule \\
    3.11 -  $symmetric$ & apply symmetry of equality \\
    3.12 -  $standard$ & put into standard result form \\
    3.13 -  $rulify$ & put into object-rule form \\
    3.14 -  $elimify$ & put destruction rule into elimination form \\[1ex]
    3.15 +  \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
    3.16 +  $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\
    3.17 +  $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
    3.18 +  $symmetric$ & resolution with symmetry of equality \\
    3.19 +  $THEN~b$ & resolution with other rule \\
    3.20 +  $rulified$ & result put into standard rule form \\
    3.21 +  $elimified$ & destruct rule turned into elimination rule \\
    3.22 +  $standard$ & result put into standard form \\[1ex]
    3.23  
    3.24 -  \multicolumn{2}{l}{\textbf{Declare rules}} \\[0.5ex]
    3.25 -  $simp$ & declare Simplifier rules \\
    3.26 -  $split$ & declare Splitter rules \\
    3.27 -  $intro$, $elim$, $dest$ & declare Classical Reasoner rules (also ``!'' or ``?'') \\
    3.28 -  $iff$ & declare Simplifier + Classical Reasoner rules \\
    3.29 -  $trans$ & declare calculational rules (general transitivity) \\
    3.30 +  \multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
    3.31 +  $simp$ & Simplifier rule \\
    3.32 +  $intro$, $elim$, $dest$ & Classical Reasoner rule \\
    3.33 +  $iff$ & Simplifier + Classical Reasoner rule \\
    3.34 +  $split$ & case split rule \\
    3.35 +  $trans$ & transitivity rule \\
    3.36  \end{tabular}
    3.37  
    3.38