method setup for Classical steps;
authorwenzelm
Sat Nov 17 19:46:32 2012 +0100 (2012-11-17)
changeset 50108f171b5240c31
parent 50107 289181e3e524
child 50109 c13dc0b1841c
method setup for Classical steps;
src/Doc/IsarRef/Generic.thy
src/HOL/Algebra/abstract/Ring2.thy
src/Provers/classical.ML
     1.1 --- a/src/Doc/IsarRef/Generic.thy	Sat Nov 17 17:55:52 2012 +0100
     1.2 +++ b/src/Doc/IsarRef/Generic.thy	Sat Nov 17 19:46:32 2012 +0100
     1.3 @@ -1753,7 +1753,7 @@
     1.4    It is deterministic, with at most one outcome.
     1.5  
     1.6    \item @{method clarify} performs a series of safe steps without
     1.7 -  splitting subgoals; see also @{ML clarify_step_tac}.
     1.8 +  splitting subgoals; see also @{method clarify_step}.
     1.9  
    1.10    \item @{method clarsimp} acts like @{method clarify}, but also does
    1.11    simplification.  Note that if the Simplifier context includes a
    1.12 @@ -1766,13 +1766,13 @@
    1.13  subsection {* Single-step tactics *}
    1.14  
    1.15  text {*
    1.16 -  \begin{mldecls}
    1.17 -    @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
    1.18 -    @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
    1.19 -    @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
    1.20 -    @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
    1.21 -    @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
    1.22 -  \end{mldecls}
    1.23 +  \begin{matharray}{rcl}
    1.24 +    @{method_def safe_step} & : & @{text method} \\
    1.25 +    @{method_def inst_step} & : & @{text method} \\
    1.26 +    @{method_def step} & : & @{text method} \\
    1.27 +    @{method_def slow_step} & : & @{text method} \\
    1.28 +    @{method_def clarify_step} & : &  @{text method} \\
    1.29 +  \end{matharray}
    1.30  
    1.31    These are the primitive tactics behind the automated proof methods
    1.32    of the Classical Reasoner.  By calling them yourself, you can
    1.33 @@ -1780,30 +1780,30 @@
    1.34  
    1.35    \begin{description}
    1.36  
    1.37 -  \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on
    1.38 -  subgoal @{text i}.  The safe wrapper tacticals are applied to a
    1.39 -  tactic that may include proof by assumption or Modus Ponens (taking
    1.40 -  care not to instantiate unknowns), or substitution.
    1.41 +  \item @{method safe_step} performs a safe step on the first subgoal.
    1.42 +  The safe wrapper tacticals are applied to a tactic that may include
    1.43 +  proof by assumption or Modus Ponens (taking care not to instantiate
    1.44 +  unknowns), or substitution.
    1.45  
    1.46 -  \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows
    1.47 +  \item @{method inst_step} is like @{method safe_step}, but allows
    1.48    unknowns to be instantiated.
    1.49  
    1.50 -  \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof
    1.51 -  procedure.  The unsafe wrapper tacticals are applied to a tactic
    1.52 -  that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe
    1.53 -  rule from the context.
    1.54 +  \item @{method step} is the basic step of the proof procedure, it
    1.55 +  operates on the first subgoal.  The unsafe wrapper tacticals are
    1.56 +  applied to a tactic that tries @{method safe}, @{method inst_step},
    1.57 +  or applies an unsafe rule from the context.
    1.58  
    1.59 -  \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows
    1.60 -  backtracking between using safe rules with instantiation (@{ML
    1.61 -  inst_step_tac}) and using unsafe rules.  The resulting search space
    1.62 -  is larger.
    1.63 +  \item @{method slow_step} resembles @{method step}, but allows
    1.64 +  backtracking between using safe rules with instantiation (@{method
    1.65 +  inst_step}) and using unsafe rules.  The resulting search space is
    1.66 +  larger.
    1.67  
    1.68 -  \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step
    1.69 -  on subgoal @{text i}.  No splitting step is applied; for example,
    1.70 -  the subgoal @{text "A \<and> B"} is left as a conjunction.  Proof by
    1.71 -  assumption, Modus Ponens, etc., may be performed provided they do
    1.72 -  not instantiate unknowns.  Assumptions of the form @{text "x = t"}
    1.73 -  may be eliminated.  The safe wrapper tactical is applied.
    1.74 +  \item @{method clarify_step} performs a safe step on the first
    1.75 +  subgoal; no splitting step is applied.  For example, the subgoal
    1.76 +  @{text "A \<and> B"} is left as a conjunction.  Proof by assumption,
    1.77 +  Modus Ponens, etc., may be performed provided they do not
    1.78 +  instantiate unknowns.  Assumptions of the form @{text "x = t"} may
    1.79 +  be eliminated.  The safe wrapper tactical is applied.
    1.80  
    1.81    \end{description}
    1.82  *}
    1.83 @@ -1839,10 +1839,10 @@
    1.84    The classical reasoning tools --- except @{method blast} --- allow
    1.85    to modify this basic proof strategy by applying two lists of
    1.86    arbitrary \emph{wrapper tacticals} to it.  The first wrapper list,
    1.87 -  which is considered to contain safe wrappers only, affects @{ML
    1.88 -  safe_step_tac} and all the tactics that call it.  The second one,
    1.89 -  which may contain unsafe wrappers, affects the unsafe parts of @{ML
    1.90 -  step_tac}, @{ML slow_step_tac}, and the tactics that call them.  A
    1.91 +  which is considered to contain safe wrappers only, affects @{method
    1.92 +  safe_step} and all the tactics that call it.  The second one, which
    1.93 +  may contain unsafe wrappers, affects the unsafe parts of @{method
    1.94 +  step}, @{method slow_step}, and the tactics that call them.  A
    1.95    wrapper transforms each step of the search, for example by
    1.96    attempting other tactics before or after the original step tactic.
    1.97    All members of a wrapper list are applied in turn to the respective
     2.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Sat Nov 17 17:55:52 2012 +0100
     2.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Sat Nov 17 19:46:32 2012 +0100
     2.3 @@ -468,7 +468,7 @@
     2.4  (* fields are integral domains *)
     2.5  
     2.6  lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
     2.7 -  apply (tactic "step_tac @{context} 1")
     2.8 +  apply step
     2.9    apply (rule_tac a = " (a*b) * inverse b" in box_equals)
    2.10      apply (rule_tac [3] refl)
    2.11     prefer 2
     3.1 --- a/src/Provers/classical.ML	Sat Nov 17 17:55:52 2012 +0100
     3.2 +++ b/src/Provers/classical.ML	Sat Nov 17 19:46:32 2012 +0100
     3.3 @@ -948,7 +948,17 @@
     3.4        >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
     3.5      "classical prover (iterative deepening)" #>
     3.6    Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
     3.7 -    "classical prover (apply safe rules)";
     3.8 +    "classical prover (apply safe rules)" #>
     3.9 +  Method.setup @{binding safe_step} (cla_method' safe_step_tac)
    3.10 +    "single classical step (safe rules)" #>
    3.11 +  Method.setup @{binding inst_step} (cla_method' inst_step_tac)
    3.12 +    "single classical step (safe rules, allow instantiations)" #>
    3.13 +  Method.setup @{binding step} (cla_method' step_tac)
    3.14 +    "single classical step (safe and unsafe rules)" #>
    3.15 +  Method.setup @{binding slow_step} (cla_method' slow_step_tac)
    3.16 +    "single classical step (safe and unsafe rules, allow backtracking)" #>
    3.17 +  Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
    3.18 +    "single classical step (safe rules, without splitting)";
    3.19  
    3.20  
    3.21