# HG changeset patch # User ballarin # Date 1062164411 -7200 # Node ID dbd16ebaf907f587053a34bca68866442dad867b # Parent f3cafd2929d5b9b4d3690536021c97418865c423 Method rule_tac understands Isar contexts: documentation. diff -r f3cafd2929d5 -r dbd16ebaf907 NEWS --- 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 diff -r f3cafd2929d5 -r dbd16ebaf907 doc-src/IsarRef/generic.tex --- 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} diff -r f3cafd2929d5 -r dbd16ebaf907 doc-src/IsarRef/pure.tex --- 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} diff -r f3cafd2929d5 -r dbd16ebaf907 doc-src/IsarRef/refcard.tex --- 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 \\