# HG changeset patch # User wenzelm # Date 1353177992 -3600 # Node ID f171b5240c31fb9ec3121827bda1ce7066c62bc2 # Parent 289181e3e524dcfdfa58265e9cca69c7ddb7cd3f method setup for Classical steps; diff -r 289181e3e524 -r f171b5240c31 src/Doc/IsarRef/Generic.thy --- a/src/Doc/IsarRef/Generic.thy Sat Nov 17 17:55:52 2012 +0100 +++ b/src/Doc/IsarRef/Generic.thy Sat Nov 17 19:46:32 2012 +0100 @@ -1753,7 +1753,7 @@ It is deterministic, with at most one outcome. \item @{method clarify} performs a series of safe steps without - splitting subgoals; see also @{ML clarify_step_tac}. + splitting subgoals; see also @{method clarify_step}. \item @{method clarsimp} acts like @{method clarify}, but also does simplification. Note that if the Simplifier context includes a @@ -1766,13 +1766,13 @@ subsection {* Single-step tactics *} text {* - \begin{mldecls} - @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\ - @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\ - @{index_ML step_tac: "Proof.context -> int -> tactic"} \\ - @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\ - @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\ - \end{mldecls} + \begin{matharray}{rcl} + @{method_def safe_step} & : & @{text method} \\ + @{method_def inst_step} & : & @{text method} \\ + @{method_def step} & : & @{text method} \\ + @{method_def slow_step} & : & @{text method} \\ + @{method_def clarify_step} & : & @{text method} \\ + \end{matharray} These are the primitive tactics behind the automated proof methods of the Classical Reasoner. By calling them yourself, you can @@ -1780,30 +1780,30 @@ \begin{description} - \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on - subgoal @{text i}. The safe wrapper tacticals are applied to a - tactic that may include proof by assumption or Modus Ponens (taking - care not to instantiate unknowns), or substitution. + \item @{method safe_step} performs a safe step on the first subgoal. + The safe wrapper tacticals are applied to a tactic that may include + proof by assumption or Modus Ponens (taking care not to instantiate + unknowns), or substitution. - \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows + \item @{method inst_step} is like @{method safe_step}, but allows unknowns to be instantiated. - \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof - procedure. The unsafe wrapper tacticals are applied to a tactic - that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe - rule from the context. + \item @{method step} is the basic step of the proof procedure, it + operates on the first subgoal. The unsafe wrapper tacticals are + applied to a tactic that tries @{method safe}, @{method inst_step}, + or applies an unsafe rule from the context. - \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows - backtracking between using safe rules with instantiation (@{ML - inst_step_tac}) and using unsafe rules. The resulting search space - is larger. + \item @{method slow_step} resembles @{method step}, but allows + backtracking between using safe rules with instantiation (@{method + inst_step}) and using unsafe rules. The resulting search space is + larger. - \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step - on subgoal @{text i}. No splitting step is applied; for example, - the subgoal @{text "A \ B"} is left as a conjunction. Proof by - assumption, Modus Ponens, etc., may be performed provided they do - not instantiate unknowns. Assumptions of the form @{text "x = t"} - may be eliminated. The safe wrapper tactical is applied. + \item @{method clarify_step} performs a safe step on the first + subgoal; no splitting step is applied. For example, the subgoal + @{text "A \ B"} is left as a conjunction. Proof by assumption, + Modus Ponens, etc., may be performed provided they do not + instantiate unknowns. Assumptions of the form @{text "x = t"} may + be eliminated. The safe wrapper tactical is applied. \end{description} *} @@ -1839,10 +1839,10 @@ The classical reasoning tools --- except @{method blast} --- allow to modify this basic proof strategy by applying two lists of arbitrary \emph{wrapper tacticals} to it. The first wrapper list, - which is considered to contain safe wrappers only, affects @{ML - safe_step_tac} and all the tactics that call it. The second one, - which may contain unsafe wrappers, affects the unsafe parts of @{ML - step_tac}, @{ML slow_step_tac}, and the tactics that call them. A + which is considered to contain safe wrappers only, affects @{method + safe_step} and all the tactics that call it. The second one, which + may contain unsafe wrappers, affects the unsafe parts of @{method + step}, @{method slow_step}, and the tactics that call them. A wrapper transforms each step of the search, for example by attempting other tactics before or after the original step tactic. All members of a wrapper list are applied in turn to the respective diff -r 289181e3e524 -r f171b5240c31 src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Sat Nov 17 17:55:52 2012 +0100 +++ b/src/HOL/Algebra/abstract/Ring2.thy Sat Nov 17 19:46:32 2012 +0100 @@ -468,7 +468,7 @@ (* fields are integral domains *) lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0" - apply (tactic "step_tac @{context} 1") + apply step apply (rule_tac a = " (a*b) * inverse b" in box_equals) apply (rule_tac [3] refl) prefer 2 diff -r 289181e3e524 -r f171b5240c31 src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Nov 17 17:55:52 2012 +0100 +++ b/src/Provers/classical.ML Sat Nov 17 19:46:32 2012 +0100 @@ -948,7 +948,17 @@ >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n))) "classical prover (iterative deepening)" #> Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac)) - "classical prover (apply safe rules)"; + "classical prover (apply safe rules)" #> + Method.setup @{binding safe_step} (cla_method' safe_step_tac) + "single classical step (safe rules)" #> + Method.setup @{binding inst_step} (cla_method' inst_step_tac) + "single classical step (safe rules, allow instantiations)" #> + Method.setup @{binding step} (cla_method' step_tac) + "single classical step (safe and unsafe rules)" #> + Method.setup @{binding slow_step} (cla_method' slow_step_tac) + "single classical step (safe and unsafe rules, allow backtracking)" #> + Method.setup @{binding clarify_step} (cla_method' clarify_step_tac) + "single classical step (safe rules, without splitting)";