--- a/src/Doc/Isar_Ref/Generic.thy Mon Jun 15 13:29:57 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Mon Jun 15 14:10:41 2015 +0200
@@ -255,120 +255,6 @@
\<close>
-subsection \<open>Further tactic emulations \label{sec:tactics}\<close>
-
-text \<open>
- The following improper proof methods emulate traditional tactics.
- These admit direct access to the goal state, which is normally
- considered harmful! In particular, this may involve both numbered
- goal addressing (default 1), and dynamic instantiation within the
- scope of some subgoal.
-
- \begin{warn}
- 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 @{text foo_tac}. Note also that variable names
- occurring on left hand sides of instantiations must be preceded by a
- question mark if they coincide with a keyword or contain dots. This
- is consistent with the attribute @{attribute "where"} (see
- \secref{sec:pure-meth-att}).
-
- \begin{matharray}{rcl}
- @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
- \end{matharray}
-
- @{rail \<open>
- (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
- @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
- (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
- ;
- @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
- ;
- @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
- ;
- @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
- ;
- @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
- ;
- (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
- \<close>}
-
-\begin{description}
-
- \item @{method rule_tac} etc. do resolution of rules with explicit
- instantiation. This works the same way as the ML tactics @{ML
- Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
-
- Multiple rules may be only given if there is no instantiation; then
- @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
- @{cite "isabelle-implementation"}).
-
- \item @{method cut_tac} inserts facts into the proof state as
- assumption of a subgoal; instantiations may be given as well. Note
- that the scope of schematic variables is spread over the main goal
- statement and rule premises are turned into new subgoals. This is
- in contrast to the regular method @{method insert} which inserts
- closed rule statements.
-
- \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
- from a subgoal. Note that @{text \<phi>} may contain schematic
- variables, to abbreviate the intended proposition; the first
- matching subgoal premise will be deleted. Removing useless premises
- from a subgoal increases its readability and can make search tactics
- run faster.
-
- \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
- @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^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 \<dots> x\<^sub>n"} renames parameters of a
- goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
- \emph{suffix} of variables.
-
- \item @{method rotate_tac}~@{text n} rotates the premises of a
- subgoal by @{text n} positions: from right to left if @{text n} is
- positive, and from left to right if @{text n} is negative; the
- default value is 1.
-
- \item @{method tactic}~@{text "text"} produces a proof method from
- any ML text of type @{ML_type tactic}. Apart from the usual ML
- environment and the current proof context, the ML code may refer to
- the locally bound values @{ML_text facts}, which indicates any
- current facts used for forward-chaining.
-
- \item @{method raw_tactic} is similar to @{method tactic}, but
- presents the goal state in its raw internal form, where simultaneous
- subgoals appear as conjunction of the logical framework instead of
- the usual split into several subgoals. While feature this is useful
- for debugging of complex method definitions, it should not never
- appear in production theories.
-
- \end{description}
-\<close>
-
-
section \<open>The Simplifier \label{sec:simplifier}\<close>
text \<open>The Simplifier performs conditional and unconditional
--- a/src/Doc/Isar_Ref/Proof.thy Mon Jun 15 13:29:57 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Mon Jun 15 14:10:41 2015 +0200
@@ -953,90 +953,6 @@
\<close>
-subsection \<open>Emulating tactic scripts \label{sec:tactic-commands}\<close>
-
-text \<open>
- \begin{matharray}{rcl}
- @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
- @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
- @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
- @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
- @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
- @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
- \end{matharray}
-
- The Isar language provides separate commands to accommodate tactic-style
- proof scripts within the same system. While being outside the
- orthodox Isar proof language, these might come in handy for
- interactive exploration and debugging, or even actual tactical proof
- within new-style theories (to benefit from document preparation, for
- example). See also \secref{sec:tactics} for actual tactics, that
- have been encapsulated as proof methods. Proper proof methods may
- be used in scripts, too.
-
- @{rail \<open>
- @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
- ;
- ( @@{command apply} | @@{command apply_end} ) @{syntax method}
- ;
- @@{command defer} @{syntax nat}?
- ;
- @@{command prefer} @{syntax nat}
- \<close>}
-
- \begin{description}
-
- \item @{command "supply"} supports fact definitions during goal
- refinement: it is similar to @{command "note"}, but it operates in
- backwards mode and does not have any impact on chained facts.
-
- \item @{command "apply"}~@{text m} applies proof method @{text m} in
- initial position, but unlike @{command "proof"} it retains ``@{text
- "proof(prove)"}'' mode. Thus consecutive method applications may be
- given just as in tactic scripts.
-
- Facts are passed to @{text m} as indicated by the goal's
- forward-chain mode, and are \emph{consumed} afterwards. Thus any
- further @{command "apply"} command would always work in a purely
- backward manner.
-
- \item @{command "apply_end"}~@{text "m"} applies proof method @{text
- m} as if in terminal position. Basically, this simulates a
- multi-step tactic script for @{command "qed"}, but may be given
- anywhere within the proof body.
-
- No facts are passed to @{text m} here. Furthermore, the static
- context is that of the enclosing goal (as for actual @{command
- "qed"}). Thus the proof method may not refer to any assumptions
- introduced in the current body, for example.
-
- \item @{command "done"} completes a proof script, provided that the
- current goal state is solved completely. Note that actual
- structured proof commands (e.g.\ ``@{command "."}'' or @{command
- "sorry"}) may be used to conclude proof scripts as well.
-
- \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
- shuffle the list of pending goals: @{command "defer"} puts off
- sub-goal @{text n} to the end of the list (@{text "n = 1"} by
- default), while @{command "prefer"} brings sub-goal @{text n} to the
- front.
-
- \item @{command "back"} does back-tracking over the result sequence
- of the latest proof command. Any proof command may return multiple
- results, and this command explores the possibilities step-by-step.
- It is mainly useful for experimentation and interactive exploration,
- and should be avoided in finished proofs.
-
- \end{description}
-
- Any proper Isar proof method may be used with tactic script commands
- such as @{command "apply"}. A few additional emulations of actual
- tactics are provided as well; these would be never used in actual
- structured proofs, of course.
-\<close>
-
-
subsection \<open>Defining proof methods\<close>
text \<open>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Mon Jun 15 14:10:41 2015 +0200
@@ -0,0 +1,204 @@
+theory Proof_Script
+imports Base Main
+begin
+
+chapter \<open>Proof scripts\<close>
+
+text \<open>
+ Interactive theorem proving is traditionally associated with ``proof
+ scripts'', but Isabelle/Isar is centered around structured \emph{proof
+ documents} instead (see also \chref{ch:proofs}).
+
+ Nonetheless, it is possible to emulate proof scripts by sequential
+ refinements of a proof state in backwards mode, notably with the @{command
+ apply} command (see \secref{sec:tactic-commands}). There are also various
+ proof methods that allow to refer to implicit goal state information that
+ is normally not accessible to structured Isar proofs (see
+ \secref{sec:tactics}).
+\<close>
+
+
+section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
+
+text \<open>
+ \begin{matharray}{rcl}
+ @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
+ @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
+ @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
+ @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
+ @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
+ @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
+ \end{matharray}
+
+ @{rail \<open>
+ @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+ ;
+ ( @@{command apply} | @@{command apply_end} ) @{syntax method}
+ ;
+ @@{command defer} @{syntax nat}?
+ ;
+ @@{command prefer} @{syntax nat}
+ \<close>}
+
+ \begin{description}
+
+ \item @{command "supply"} supports fact definitions during goal
+ refinement: it is similar to @{command "note"}, but it operates in
+ backwards mode and does not have any impact on chained facts.
+
+ \item @{command "apply"}~@{text m} applies proof method @{text m} in
+ initial position, but unlike @{command "proof"} it retains ``@{text
+ "proof(prove)"}'' mode. Thus consecutive method applications may be
+ given just as in tactic scripts.
+
+ Facts are passed to @{text m} as indicated by the goal's
+ forward-chain mode, and are \emph{consumed} afterwards. Thus any
+ further @{command "apply"} command would always work in a purely
+ backward manner.
+
+ \item @{command "apply_end"}~@{text "m"} applies proof method @{text
+ m} as if in terminal position. Basically, this simulates a
+ multi-step tactic script for @{command "qed"}, but may be given
+ anywhere within the proof body.
+
+ No facts are passed to @{text m} here. Furthermore, the static
+ context is that of the enclosing goal (as for actual @{command
+ "qed"}). Thus the proof method may not refer to any assumptions
+ introduced in the current body, for example.
+
+ \item @{command "done"} completes a proof script, provided that the
+ current goal state is solved completely. Note that actual
+ structured proof commands (e.g.\ ``@{command "."}'' or @{command
+ "sorry"}) may be used to conclude proof scripts as well.
+
+ \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
+ shuffle the list of pending goals: @{command "defer"} puts off
+ sub-goal @{text n} to the end of the list (@{text "n = 1"} by
+ default), while @{command "prefer"} brings sub-goal @{text n} to the
+ front.
+
+ \item @{command "back"} does back-tracking over the result sequence
+ of the latest proof command. Any proof command may return multiple
+ results, and this command explores the possibilities step-by-step.
+ It is mainly useful for experimentation and interactive exploration,
+ and should be avoided in finished proofs.
+
+ \end{description}
+\<close>
+
+
+section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
+
+text \<open>
+ The following improper proof methods emulate traditional tactics.
+ These admit direct access to the goal state, which is normally
+ considered harmful! In particular, this may involve both numbered
+ goal addressing (default 1), and dynamic instantiation within the
+ scope of some subgoal.
+
+ \begin{warn}
+ 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 @{text foo_tac}. Note also that variable names
+ occurring on left hand sides of instantiations must be preceded by a
+ question mark if they coincide with a keyword or contain dots. This
+ is consistent with the attribute @{attribute "where"} (see
+ \secref{sec:pure-meth-att}).
+
+ \begin{matharray}{rcl}
+ @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
+ \end{matharray}
+
+ @{rail \<open>
+ (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
+ @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
+ (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
+ ;
+ @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
+ ;
+ @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
+ ;
+ @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
+ ;
+ @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
+ ;
+ (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
+ \<close>}
+
+\begin{description}
+
+ \item @{method rule_tac} etc. do resolution of rules with explicit
+ instantiation. This works the same way as the ML tactics @{ML
+ Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
+
+ Multiple rules may be only given if there is no instantiation; then
+ @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
+ @{cite "isabelle-implementation"}).
+
+ \item @{method cut_tac} inserts facts into the proof state as
+ assumption of a subgoal; instantiations may be given as well. Note
+ that the scope of schematic variables is spread over the main goal
+ statement and rule premises are turned into new subgoals. This is
+ in contrast to the regular method @{method insert} which inserts
+ closed rule statements.
+
+ \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
+ from a subgoal. Note that @{text \<phi>} may contain schematic
+ variables, to abbreviate the intended proposition; the first
+ matching subgoal premise will be deleted. Removing useless premises
+ from a subgoal increases its readability and can make search tactics
+ run faster.
+
+ \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
+ @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^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 \<dots> x\<^sub>n"} renames parameters of a
+ goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
+ \emph{suffix} of variables.
+
+ \item @{method rotate_tac}~@{text n} rotates the premises of a
+ subgoal by @{text n} positions: from right to left if @{text n} is
+ positive, and from left to right if @{text n} is negative; the
+ default value is 1.
+
+ \item @{method tactic}~@{text "text"} produces a proof method from
+ any ML text of type @{ML_type tactic}. Apart from the usual ML
+ environment and the current proof context, the ML code may refer to
+ the locally bound values @{ML_text facts}, which indicates any
+ current facts used for forward-chaining.
+
+ \item @{method raw_tactic} is similar to @{method tactic}, but
+ presents the goal state in its raw internal form, where simultaneous
+ subgoals appear as conjunction of the logical framework instead of
+ the usual split into several subgoals. While feature this is useful
+ for debugging of complex method definitions, it should not never
+ appear in production theories.
+
+ \end{description}
+\<close>
+
+end
\ No newline at end of file
--- a/src/Doc/Isar_Ref/document/root.tex Mon Jun 15 13:29:57 2015 +0200
+++ b/src/Doc/Isar_Ref/document/root.tex Mon Jun 15 14:10:41 2015 +0200
@@ -74,6 +74,7 @@
\input{Document_Preparation.tex}
\input{Spec.tex}
\input{Proof.tex}
+\input{Proof_Script.tex}
\input{Inner_Syntax.tex}
\input{Misc.tex}
\input{Generic.tex}
--- a/src/Doc/ROOT Mon Jun 15 13:29:57 2015 +0200
+++ b/src/Doc/ROOT Mon Jun 15 14:10:41 2015 +0200
@@ -164,6 +164,7 @@
Document_Preparation
Spec
Proof
+ Proof_Script
Inner_Syntax
Misc
Generic