# HG changeset patch # User wenzelm # Date 1327696177 -3600 # Node ID e1b5460f1725b54ac1e90be493bc36d1f4fa3286 # Parent 4ab175c85d570ac2f123dceecf219b4b6951f09a updated subgoal_tac; diff -r 4ab175c85d57 -r e1b5460f1725 doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 22:21:33 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Fri Jan 27 21:29:37 2012 +0100 @@ -364,7 +364,8 @@ @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ - @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\[1ex] + @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ + @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\ @{index_ML rename_tac: "string list -> int -> tactic"} \\ \end{mldecls} @@ -383,6 +384,10 @@ \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that the selected assumption is not deleted. + \item @{ML subgoal_tac}~@{text "ctxt \ i"} adds the proposition + @{text "\"} as local premise to subgoal @{text "i"}, and poses the + same as a new subgoal @{text "i + 1"} (in the original context). + \item @{ML rename_tac}~@{text "names i"} renames the innermost parameters of subgoal @{text i} according to the provided @{text names} (which need to be distinct indentifiers). diff -r 4ab175c85d57 -r e1b5460f1725 doc-src/IsarImplementation/Thy/document/Tactic.tex --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 22:21:33 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Fri Jan 27 21:29:37 2012 +0100 @@ -432,7 +432,8 @@ \indexdef{}{ML}{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ \indexdef{}{ML}{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ \indexdef{}{ML}{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ - \indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex] + \indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ + \indexdef{}{ML}{subgoal\_tac}\verb|subgoal_tac: Proof.context -> string -> int -> tactic| \\ \indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\ \end{mldecls} @@ -451,6 +452,10 @@ \item \verb|forw_inst_tac| is like \verb|dres_inst_tac| except that the selected assumption is not deleted. + \item \verb|subgoal_tac|~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} adds the proposition + \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as local premise to subgoal \isa{i}, and poses the + same as a new subgoal \isa{i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}} (in the original context). + \item \verb|rename_tac|~\isa{names\ i} renames the innermost parameters of subgoal \isa{i} according to the provided \isa{names} (which need to be distinct indentifiers). diff -r 4ab175c85d57 -r e1b5460f1725 doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Thu Jan 26 22:21:33 2012 +0100 +++ b/doc-src/IsarRef/Thy/Generic.thy Fri Jan 27 21:29:37 2012 +0100 @@ -339,9 +339,9 @@ from a subgoal; note that @{text \} may contain schematic variables. See also @{ML thin_tac} in \cite{isabelle-implementation}. - \item @{method subgoal_tac}~@{text \} adds @{text \} as an - assumption to a subgoal. See also @{ML subgoal_tac} and @{ML - subgoals_tac} in \cite{isabelle-implementation}. + \item @{method subgoal_tac}~@{text "\\<^sub>1 \ \\<^sub>n"} adds the propositions + @{text "\\<^sub>1 \ \\<^sub>n"} as local premises to a subgoal, and poses the same + as new subgoals (in the original context). \item @{method rename_tac}~@{text "x\<^sub>1 \ x\<^sub>n"} renames parameters of a goal according to the list @{text "x\<^sub>1, \, x\<^sub>n"}, which refers to the diff -r 4ab175c85d57 -r e1b5460f1725 doc-src/IsarRef/Thy/document/Generic.tex --- a/doc-src/IsarRef/Thy/document/Generic.tex Thu Jan 26 22:21:33 2012 +0100 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Fri Jan 27 21:29:37 2012 +0100 @@ -541,8 +541,9 @@ from a subgoal; note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain schematic variables. See also \verb|thin_tac| in \cite{isabelle-implementation}. - \item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} adds \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as an - assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite{isabelle-implementation}. + \item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} adds the propositions + \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} as local premises to a subgoal, and poses the same + as new subgoals (in the original context). \item \hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} renames parameters of a goal according to the list \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, which refers to the diff -r 4ab175c85d57 -r e1b5460f1725 doc-src/Ref/tactic.tex --- a/doc-src/Ref/tactic.tex Thu Jan 26 22:21:33 2012 +0100 +++ b/doc-src/Ref/tactic.tex Fri Jan 27 21:29:37 2012 +0100 @@ -9,8 +9,6 @@ \begin{ttbox} cut_facts_tac : thm list -> int -> tactic cut_inst_tac : (string*string)list -> thm -> int -> tactic -subgoal_tac : string -> int -> tactic -subgoals_tac : string list -> int -> tactic \end{ttbox} These tactics add assumptions to a subgoal. \begin{ttdescription} @@ -28,13 +26,6 @@ described in {\S}\ref{res_inst_tac}. It adds the resulting theorem as a new assumption to subgoal~$i$. -\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] -adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same -{\it formula} as a new subgoal, $i+1$. - -\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}] - uses {\tt subgoal_tac} to add the members of the list of {\it - formulae} as assumptions to subgoal~$i$. \end{ttdescription} @@ -91,8 +82,7 @@ \item[\tdx{cut_rl}] is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting -assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac} -and {\tt subgoal_tac}. +assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}. \end{ttdescription}