Method rule_tac understands Isar contexts: documentation.
authorballarin
Fri Aug 29 15:40:11 2003 +0200 (2003-08-29)
changeset 14175dbd16ebaf907
parent 14174 f3cafd2929d5
child 14176 716fec31f9ea
Method rule_tac understands Isar contexts: documentation.
NEWS
doc-src/IsarRef/generic.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/refcard.tex
     1.1 --- a/NEWS	Fri Aug 29 15:19:02 2003 +0200
     1.2 +++ b/NEWS	Fri Aug 29 15:40:11 2003 +0200
     1.3 @@ -17,6 +17,22 @@
     1.4    symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
     1.5    existing theory and ML files.
     1.6  
     1.7 +*** Isar ***
     1.8 +
     1.9 +* Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
    1.10 +
    1.11 +  - Now understand static (Isar) contexts.  As a consequence, users of Isar
    1.12 +    locales are no longer forced to write Isar proof scripts.
    1.13 +    For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
    1.14 +    emulations.
    1.15 +  - INCOMPATIBILITY: names of variables to be instantiated may no
    1.16 +    longer be enclosed in quotes.  Instead, precede variable names containing
    1.17 +    dots with `?'.  This is consistent with the instantiation attribute
    1.18 +    "where".
    1.19 +
    1.20 +* HOL: Tactic emulation methods induct_tac and case_tac understand static
    1.21 +  (Isar) contexts.
    1.22 +
    1.23  *** HOL ***
    1.24  
    1.25  * 'specification' command added, allowing for definition by
     2.1 --- a/doc-src/IsarRef/generic.tex	Fri Aug 29 15:19:02 2003 +0200
     2.2 +++ b/doc-src/IsarRef/generic.tex	Fri Aug 29 15:40:11 2003 +0200
     2.3 @@ -437,7 +437,7 @@
     2.4  
     2.5  \indexisaratt{tagged}\indexisaratt{untagged}
     2.6  \indexisaratt{THEN}\indexisaratt{COMP}
     2.7 -\indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded}
     2.8 +\indexisaratt{unfolded}\indexisaratt{folded}
     2.9  \indexisaratt{standard}\indexisarattof{Pure}{elim-format}
    2.10  \indexisaratt{no-vars}
    2.11  \begin{matharray}{rcl}
    2.12 @@ -445,7 +445,6 @@
    2.13    untagged & : & \isaratt \\[0.5ex]
    2.14    THEN & : & \isaratt \\
    2.15    COMP & : & \isaratt \\[0.5ex]
    2.16 -  where & : & \isaratt \\[0.5ex]
    2.17    unfolded & : & \isaratt \\
    2.18    folded & : & \isaratt \\[0.5ex]
    2.19    elim_format & : & \isaratt \\
    2.20 @@ -460,8 +459,6 @@
    2.21    ;
    2.22    ('THEN' | 'COMP') ('[' nat ']')? thmref
    2.23    ;
    2.24 -  'where' (name '=' term * 'and')
    2.25 -  ;
    2.26    ('unfolded' | 'folded') thmrefs
    2.27    ;
    2.28  \end{rail}
    2.29 @@ -480,11 +477,6 @@
    2.30    normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
    2.31    \cite[\S5]{isabelle-ref}).
    2.32  
    2.33 -\item [$where~\vec x = \vec t$] perform named instantiation of schematic
    2.34 -  variables occurring in a theorem.  Unlike instantiation tactics such as
    2.35 -  $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
    2.36 -  have to be specified on the left-hand side (e.g.\ $\Var{x@3}$).
    2.37 -
    2.38  \item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
    2.39    given meta-level definitions throughout a rule.
    2.40  
    2.41 @@ -513,15 +505,23 @@
    2.42  dynamic instantiation within the scope of some subgoal.
    2.43  
    2.44  \begin{warn}
    2.45 -  Dynamic instantiations are read and type-checked according to a subgoal of
    2.46 -  the current dynamic goal state, rather than the static proof context!  In
    2.47 -  particular, locally fixed variables and term abbreviations may not be
    2.48 -  included in the term specifications.  Thus schematic variables are left to
    2.49 -  be solved by unification with certain parts of the subgoal involved.
    2.50 +  Dynamic instantiations refer to universally quantified parameters of
    2.51 +  a subgoal (the dynamic context) rather than fixed variables and term
    2.52 +  abbreviations of a (static) Isar context.
    2.53  \end{warn}
    2.54  
    2.55 +Tactic emulation methods, unlike their ML counterparts, admit
    2.56 +simultaneous instantiation from both dynamic and static contexts.  If
    2.57 +names occur in both contexts goal parameters hide locally fixed
    2.58 +variables.  Likewise, schematic variables refer to term abbreviations,
    2.59 +if present in the static context.  Otherwise the schematic variable is
    2.60 +interpreted as a schematic variable and left to be solved by unification
    2.61 +with certain parts of the subgoal.
    2.62 +
    2.63  Note that the tactic emulation proof methods in Isabelle/Isar are consistently
    2.64 -named $foo_tac$.
    2.65 +named $foo_tac$.  Note also that variable names occurring on left hand sides
    2.66 +of instantiations must be preceded by a question mark if they contain dots.
    2.67 +This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}).
    2.68  
    2.69  \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
    2.70  \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
     3.1 --- a/doc-src/IsarRef/pure.tex	Fri Aug 29 15:19:02 2003 +0200
     3.2 +++ b/doc-src/IsarRef/pure.tex	Fri Aug 29 15:40:11 2003 +0200
     3.3 @@ -963,7 +963,7 @@
     3.4  \indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
     3.5  \indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
     3.6  \indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
     3.7 -\indexisaratt{OF}\indexisaratt{of}
     3.8 +\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
     3.9  \begin{matharray}{rcl}
    3.10    - & : & \isarmeth \\
    3.11    assumption & : & \isarmeth \\
    3.12 @@ -976,6 +976,7 @@
    3.13    rule & : & \isaratt \\[0.5ex]
    3.14    OF & : & \isaratt \\
    3.15    of & : & \isaratt \\
    3.16 +  where & : & \isaratt \\
    3.17  \end{matharray}
    3.18  
    3.19  \begin{rail}
    3.20 @@ -993,6 +994,8 @@
    3.21    ;
    3.22    'of' insts ('concl' ':' insts)?
    3.23    ;
    3.24 +  'where' (name '=' term * 'and')
    3.25 +  ;
    3.26  \end{rail}
    3.27  
    3.28  \begin{descr}
    3.29 @@ -1058,6 +1061,11 @@
    3.30    following a ``$concl\colon$'' specification refer to positions of the
    3.31    conclusion of a rule.
    3.32    
    3.33 +\item [$where~\vec x = \vec t$] performs named instantiation of schematic
    3.34 +  variables occurring in a theorem.  Schematic variables
    3.35 +  have to be specified on the left-hand side (e.g.\ $?x1\!.\!3$).  The
    3.36 +  question mark may be omitted if the variable name does not contain a dot.
    3.37 +
    3.38  \end{descr}
    3.39  
    3.40  
     4.1 --- a/doc-src/IsarRef/refcard.tex	Fri Aug 29 15:19:02 2003 +0200
     4.2 +++ b/doc-src/IsarRef/refcard.tex	Fri Aug 29 15:40:11 2003 +0200
     4.3 @@ -118,8 +118,9 @@
     4.4  
     4.5  \begin{tabular}{ll}
     4.6    \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
     4.7 -  $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\
     4.8 -  $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
     4.9 +  $OF~\vec a$ & rule resolved with facts (skipping ``$_$'') \\
    4.10 +  $of~\vec t$ & rule instantiated with terms (skipping ``$_$'') \\
    4.11 +  $where~\vec x = \vec t$ & rule instantiated with terms, by variable name \\
    4.12    $symmetric$ & resolution with symmetry rule \\
    4.13    $THEN~b$ & resolution with another rule \\
    4.14    $rule_format$ & result put into standard rule format \\