# HG changeset patch # User wenzelm # Date 1434370241 -7200 # Node ID 98ee8635435416c42df37b7352a6b8027054da31 # Parent 9a566f4ac20a91226804635a72dcb73cfa9b6e2b moved sections; diff -r 9a566f4ac20a -r 98ee86354354 src/Doc/Isar_Ref/Generic.thy --- 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 @@ \ -subsection \Further tactic emulations \label{sec:tactics}\ - -text \ - 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 \ - (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} | - @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \ - (@{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} - \} - -\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 \} deletes the specified premise - from a subgoal. Note that @{text \} 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 "\\<^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 - \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} -\ - - section \The Simplifier \label{sec:simplifier}\ text \The Simplifier performs conditional and unconditional diff -r 9a566f4ac20a -r 98ee86354354 src/Doc/Isar_Ref/Proof.thy --- 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 @@ \ -subsection \Emulating tactic scripts \label{sec:tactic-commands}\ - -text \ - \begin{matharray}{rcl} - @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \ proof(prove)"} \\ - @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \ proof(prove)"} \\ - @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \ proof(state)"} \\ - @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \ proof(state) | local_theory | theory"} \\ - @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \ proof"} \\ - @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \ proof"} \\ - @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \ 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 \ - @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and') - ; - ( @@{command apply} | @@{command apply_end} ) @{syntax method} - ; - @@{command defer} @{syntax nat}? - ; - @@{command prefer} @{syntax nat} - \} - - \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. -\ - - subsection \Defining proof methods\ text \ diff -r 9a566f4ac20a -r 98ee86354354 src/Doc/Isar_Ref/Proof_Script.thy --- /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 \Proof scripts\ + +text \ + 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}). +\ + + +section \Commands for step-wise refinement \label{sec:tactic-commands}\ + +text \ + \begin{matharray}{rcl} + @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \ proof(prove)"} \\ + @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \ proof(prove)"} \\ + @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \ proof(state)"} \\ + @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \ proof(state) | local_theory | theory"} \\ + @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \ proof"} \\ + @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \ proof"} \\ + @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \ proof"} \\ + \end{matharray} + + @{rail \ + @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and') + ; + ( @@{command apply} | @@{command apply_end} ) @{syntax method} + ; + @@{command defer} @{syntax nat}? + ; + @@{command prefer} @{syntax nat} + \} + + \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} +\ + + +section \Tactics: improper proof methods \label{sec:tactics}\ + +text \ + 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 \ + (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} | + @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \ + (@{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} + \} + +\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 \} deletes the specified premise + from a subgoal. Note that @{text \} 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 "\\<^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 + \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} +\ + +end \ No newline at end of file diff -r 9a566f4ac20a -r 98ee86354354 src/Doc/Isar_Ref/document/root.tex --- 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} diff -r 9a566f4ac20a -r 98ee86354354 src/Doc/ROOT --- 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