# HG changeset patch # User wenzelm # Date 1327608971 -3600 # Node ID bc9479cada965ba7dfbc365120e7e11270355779 # Parent a9694a4e39e543033e23523bb190c46061325f14 moved HEADGOAL; added RANGE; diff -r a9694a4e39e5 -r bc9479cada96 doc-src/IsarImplementation/Thy/Isar.thy --- a/doc-src/IsarImplementation/Thy/Isar.thy Thu Jan 26 15:29:11 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Isar.thy Thu Jan 26 21:16:11 2012 +0100 @@ -311,7 +311,6 @@ @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\ @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\ @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\ - @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\ @{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\ @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser -> string -> theory -> theory"} \\ @@ -336,13 +335,9 @@ applied. \item @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that - addresses a specific subgoal as simple proof method. Goal facts are - already inserted into the first subgoal before @{text "tactic"} is - applied to the same. - - \item @{ML HEADGOAL}~@{text "tactic"} applies @{text "tactic"} to - the first subgoal. This is convenient to reproduce part the @{ML - SIMPLE_METHOD'} wrapping within regular @{ML METHOD}, for example. + addresses a specific subgoal as simple proof method that operates on + subgoal 1. Goal facts are inserted into the subgoal then the @{text + "tactic"} is applied. \item @{ML Method.insert_tac}~@{text "facts i"} inserts @{text "facts"} into subgoal @{text "i"}. This is convenient to reproduce diff -r a9694a4e39e5 -r bc9479cada96 doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 15:29:11 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 21:16:11 2012 +0100 @@ -575,13 +575,13 @@ *} -subsection {* Scanning for a subgoal by number *} +subsection {* Applying tactics to subgoal ranges *} text {* Tactics with explicit subgoal addressing @{ML_type "int -> tactic"} can be used together with tacticals that act like ``subgoal quantifiers'': guided by success of the body tactic a certain range of subgoals is covered. Thus the body tactic - is applied to all subgoals, for example. + is applied to \emph{all} subgoals, \emph{some} subgoal etc. Suppose that the goal state has @{text "n \ 0"} subgoals. Many of these tacticals address subgoal ranges counting downwards from @@ -595,8 +595,10 @@ @{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\ @{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\ @{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\ + @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\ @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\ @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\ + @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\ \end{mldecls} \begin{description} @@ -613,12 +615,20 @@ 1"}~@{ML_op ORELSE}~@{text "\"}~@{ML_op ORELSE}~@{text "tac n"}. It applies @{text "tac"} to one subgoal, counting upwards. + \item @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}. + It applies @{text "tac"} unconditionally to the first subgoal. + \item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or more to a subgoal, counting downwards. \item @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or more to a subgoal, counting upwards. + \item @{ML RANGE}~@{text "[tac\<^sub>1, \, tac\<^sub>k] i"} is equivalent to + @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\"}~@{ML_op + THEN}~@{text "tac\<^sub>1 i"}. It applies the given list of tactics to the + corresponding range of subgoals, counting downwards. + \end{description} *} diff -r a9694a4e39e5 -r bc9479cada96 doc-src/IsarImplementation/Thy/document/Isar.tex --- a/doc-src/IsarImplementation/Thy/document/Isar.tex Thu Jan 26 15:29:11 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Thu Jan 26 21:16:11 2012 +0100 @@ -428,7 +428,6 @@ \indexdef{}{ML}{METHOD}\verb|METHOD: (thm list -> tactic) -> Proof.method| \\ \indexdef{}{ML}{SIMPLE\_METHOD}\verb|SIMPLE_METHOD: tactic -> Proof.method| \\ \indexdef{}{ML}{SIMPLE\_METHOD'}\verb|SIMPLE_METHOD': (int -> tactic) -> Proof.method| \\ - \indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\ \indexdef{}{ML}{Method.insert\_tac}\verb|Method.insert_tac: thm list -> int -> tactic| \\ \indexdef{}{ML}{Method.setup}\verb|Method.setup: binding -> (Proof.context -> Proof.method) context_parser ->|\isasep\isanewline% \verb| string -> theory -> theory| \\ @@ -452,12 +451,8 @@ applied. \item \verb|SIMPLE_METHOD'|~\isa{tactic} wraps a tactic that - addresses a specific subgoal as simple proof method. Goal facts are - already inserted into the first subgoal before \isa{tactic} is - applied to the same. - - \item \verb|HEADGOAL|~\isa{tactic} applies \isa{tactic} to - the first subgoal. This is convenient to reproduce part the \verb|SIMPLE_METHOD'| wrapping within regular \verb|METHOD|, for example. + addresses a specific subgoal as simple proof method that operates on + subgoal 1. Goal facts are inserted into the subgoal then the \isa{tactic} is applied. \item \verb|Method.insert_tac|~\isa{facts\ i} inserts \isa{facts} into subgoal \isa{i}. This is convenient to reproduce part of the \verb|SIMPLE_METHOD| or \verb|SIMPLE_METHOD'| wrapping diff -r a9694a4e39e5 -r bc9479cada96 doc-src/IsarImplementation/Thy/document/Tactic.tex --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 15:29:11 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 21:16:11 2012 +0100 @@ -715,7 +715,7 @@ % \endisadelimML % -\isamarkupsubsection{Scanning for a subgoal by number% +\isamarkupsubsection{Applying tactics to subgoal ranges% } \isamarkuptrue% % @@ -724,7 +724,7 @@ \verb|int -> tactic| can be used together with tacticals that act like ``subgoal quantifiers'': guided by success of the body tactic a certain range of subgoals is covered. Thus the body tactic - is applied to all subgoals, for example. + is applied to \emph{all} subgoals, \emph{some} subgoal etc. Suppose that the goal state has \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}} subgoals. Many of these tacticals address subgoal ranges counting downwards from @@ -746,8 +746,10 @@ \indexdef{}{ML}{ALLGOALS}\verb|ALLGOALS: (int -> tactic) -> tactic| \\ \indexdef{}{ML}{SOMEGOAL}\verb|SOMEGOAL: (int -> tactic) -> tactic| \\ \indexdef{}{ML}{FIRSTGOAL}\verb|FIRSTGOAL: (int -> tactic) -> tactic| \\ + \indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\ \indexdef{}{ML}{REPEAT\_SOME}\verb|REPEAT_SOME: (int -> tactic) -> tactic| \\ \indexdef{}{ML}{REPEAT\_FIRST}\verb|REPEAT_FIRST: (int -> tactic) -> tactic| \\ + \indexdef{}{ML}{RANGE}\verb|RANGE: (int -> tactic) list -> int -> tactic| \\ \end{mldecls} \begin{description} @@ -761,12 +763,19 @@ \item \verb|FIRSTGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ n}. It applies \isa{tac} to one subgoal, counting upwards. + \item \verb|HEADGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}. + It applies \isa{tac} unconditionally to the first subgoal. + \item \verb|REPEAT_SOME|~\isa{tac} applies \isa{tac} once or more to a subgoal, counting downwards. \item \verb|REPEAT_FIRST|~\isa{tac} applies \isa{tac} once or more to a subgoal, counting upwards. + \item \verb|RANGE|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{5D}{\isacharbrackright}}\ i} is equivalent to + \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}. It applies the given list of tactics to the + corresponding range of subgoals, counting downwards. + \end{description}% \end{isamarkuptext}% \isamarkuptrue%