--- a/NEWS Wed Jun 14 15:47:27 2023 +0200
+++ b/NEWS Thu Jun 15 17:20:09 2023 +1000
@@ -25,6 +25,8 @@
class.preorder.of_class.intro ~> preorder.intro_of_class
class.order.of_class.intro ~> order.intro_of_class
+* The Eisbach 'method' command now takes an optional description for
+display with print_methods, similar to the 'method_setup' command.
*** Document preparation ***
--- a/src/Doc/Eisbach/Manual.thy Wed Jun 14 15:47:27 2023 +0200
+++ b/src/Doc/Eisbach/Manual.thy Thu Jun 15 17:20:09 2023 +1000
@@ -11,14 +11,15 @@
methods by combining existing ones with their usual syntax. Specifically it
allows compound proof methods to be named, and to extend the name space of
basic methods accordingly. Method definitions may abstract over parameters:
- terms, facts, or other methods.
+ terms, facts, or other methods. They may also provide an optional text
+ description for display in @{command_ref print_methods}.
\<^medskip>
The syntax diagram below refers to some syntactic categories that are
further defined in \<^cite>\<open>"isabelle-isar-ref"\<close>.
\<^rail>\<open>
- @@{command method} name args @'=' method
+ @@{command method} name args description @'=' method
;
args: term_args? method_args? \<newline> fact_args? decl_args?
;
@@ -29,6 +30,8 @@
fact_args: @'uses' (name+)
;
decl_args: @'declares' (name+)
+ ;
+ description: @{syntax text}?
\<close>
\<close>
@@ -60,8 +63,13 @@
once when the method is defined and cannot be changed later. This makes the
method stable in the sense of \<^emph>\<open>static scoping\<close>: naming another fact \<open>impI\<close>
in a later context won't affect the behaviour of \<open>prop_solver\<^sub>1\<close>.
+
+ The following example defines the same method and gives it a description for the
+ @{command_ref print_methods} command.
\<close>
+ method prop_solver\<^sub>2 \<open>solver for propositional formulae\<close> =
+ ((rule impI, (erule conjE)?) | assumption)+
section \<open>Term abstraction\<close>
--- a/src/HOL/Eisbach/Eisbach.thy Wed Jun 14 15:47:27 2023 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Thu Jun 15 17:20:09 2023 +1000
@@ -20,10 +20,11 @@
ML_file \<open>eisbach_rule_insts.ML\<close>
ML_file \<open>match_method.ML\<close>
+method solves methods m \<open>Apply method only when it solves the goal\<close> = m; fail
-method solves methods m = (m; fail)
-
-method repeat_new methods m = (m ; (repeat_new \<open>m\<close>)?)
+method repeat_new methods m
+ \<open>apply method recursively to the subgoals it generates\<close> =
+ (m ; (repeat_new \<open>m\<close>)?)
section \<open>Debugging methods\<close>
@@ -32,6 +33,7 @@
(fn (ctxt, st) => (
Output.writeln (Thm.string_of_thm ctxt st);
Seq.make_results (Seq.single (ctxt, st)))))\<close>
+ \<open>print the entire goal statement\<close>
method_setup print_headgoal =
\<open>Scan.succeed (fn ctxt => fn _ => fn (ctxt', thm) =>
@@ -39,6 +41,7 @@
(Output.writeln
(Pretty.string_of (Syntax.pretty_term ctxt t)); all_tac)) 1 thm);
(Seq.make_results (Seq.single (ctxt', thm)))))\<close>
+ \<open>print the first subgoal\<close>
ML \<open>fun method_evaluate text ctxt facts =
NO_CONTEXT_TACTIC ctxt
@@ -54,13 +57,20 @@
timed_tac st' (method_evaluate m ctxt facts st');
in SIMPLE_METHOD tac [] end)
-\<close>
+ \<close>
+ \<open>print timing information from running the parameter method\<close>
section \<open>Simple Combinators\<close>
-method_setup defer_tac = \<open>Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))\<close>
-method_setup prefer_last = \<open>Scan.succeed (fn _ => SIMPLE_METHOD (PRIMITIVE (Thm.permute_prems 0 ~1)))\<close>
+method_setup defer_tac =
+ \<open>Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))\<close>
+ \<open>make first subgoal the last subgoal. Like "defer" but as proof method\<close>
+
+method_setup prefer_last =
+ \<open>Scan.succeed (fn _ => SIMPLE_METHOD (PRIMITIVE (Thm.permute_prems 0 ~1)))\<close>
+ \<open>make last subgoal the first subgoal.\<close>
+
method_setup all =
\<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
@@ -71,7 +81,8 @@
|> Seq.map (Goal.unrestrict i)
in SIMPLE_METHOD (ALLGOALS tac) facts end)
-\<close>
+ \<close>
+ \<open>apply parameter method to all subgoals\<close>
method_setup determ =
\<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
@@ -79,7 +90,8 @@
fun tac st' = method_evaluate m ctxt facts st'
in SIMPLE_METHOD (DETERM tac) facts end)
-\<close>
+ \<close>
+ \<open>constrain result sequence to 0 or 1 elements\<close>
method_setup changed =
\<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
@@ -87,7 +99,8 @@
fun tac st' = method_evaluate m ctxt facts st'
in SIMPLE_METHOD (CHANGED tac) facts end)
-\<close>
+ \<close>
+ \<open>fail if the proof state has not changed after parameter method has run\<close>
text \<open>The following \<open>fails\<close> and \<open>succeeds\<close> methods protect the goal from the effect
@@ -103,7 +116,8 @@
| NONE => Seq.single st')
in SIMPLE_METHOD fail_tac facts end)
-\<close>
+ \<close>
+ \<open>succeed if the parameter method fails\<close>
method_setup succeeds =
\<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
@@ -114,7 +128,8 @@
| NONE => Seq.empty)
in SIMPLE_METHOD can_tac facts end)
-\<close>
+ \<close>
+ \<open>succeed without proof state change if the parameter method has non-empty result sequence\<close>
@@ -130,6 +145,6 @@
| NONE => Seq.empty)) i THEN prefer_tac i
in SIMPLE_METHOD (FIRSTGOAL prefer_first) facts end)\<close>
-
+ \<open>find first subgoal where parameter method succeeds, make this the first subgoal, and run method\<close>
end
--- a/src/HOL/Eisbach/method_closure.ML Wed Jun 14 15:47:27 2023 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Thu Jun 15 17:20:09 2023 +1000
@@ -13,9 +13,9 @@
val apply_method: Proof.context -> string -> term list -> thm list list ->
(Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic
val method: binding -> (binding * typ option * mixfix) list -> binding list ->
- binding list -> binding list -> Token.src -> local_theory -> string * local_theory
+ binding list -> binding list -> string -> Token.src -> local_theory -> string * local_theory
val method_cmd: binding -> (binding * string option * mixfix) list -> binding list ->
- binding list -> binding list -> Token.src -> local_theory -> string * local_theory
+ binding list -> binding list -> string -> Token.src -> local_theory -> string * local_theory
end;
structure Method_Closure: METHOD_CLOSURE =
@@ -174,7 +174,7 @@
| rep (m :: ms) x = ((Method.text_closure >> pair m) ::: rep ms) x;
in rep method_args >> fold bind_method end;
-fun gen_method add_fixes name vars uses declares methods source lthy =
+fun gen_method add_fixes name vars uses declares methods cmt source lthy =
let
val (uses_internal, lthy1) = lthy
|> Proof_Context.concealed
@@ -228,7 +228,7 @@
|> Method.local_setup name
(Args.context :|-- (fn ctxt =>
let val {body, vars, ...} = get_closure ctxt full_name in
- parser vars (recursive_method full_name vars body) end)) ""
+ parser vars (recursive_method full_name vars body) end)) cmt
|> pair full_name
end;
@@ -245,8 +245,9 @@
((Scan.optional (\<^keyword>\<open>methods\<close> |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
(Scan.optional (\<^keyword>\<open>uses\<close> |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) --
(Scan.optional (\<^keyword>\<open>declares\<close> |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
+ (Scan.optional Parse.embedded "") --
Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.args1 (K true)) >>
- (fn ((((name, vars), (methods, uses)), declares), src) =>
- #2 o method_cmd name vars uses declares methods src));
+ (fn (((((name, vars), (methods, uses)), declares), cmt), src) =>
+ #2 o method_cmd name vars uses declares methods cmt src));
end;