# HG changeset patch # User kleing # Date 1521273116 -39600 # Node ID 730fa992da38447dcea42acf9676599355d8d191 # Parent 736673784fac9fdde9d1785c1300742dc905f433 additional Eisbach combinators and utility methods (by Daniel Matichuck) diff -r 736673784fac -r 730fa992da38 src/HOL/Eisbach/Eisbach.thy --- a/src/HOL/Eisbach/Eisbach.thy Sat Mar 17 21:54:33 2018 +0100 +++ b/src/HOL/Eisbach/Eisbach.thy Sat Mar 17 18:51:56 2018 +1100 @@ -20,6 +20,116 @@ ML_file "eisbach_rule_insts.ML" ML_file "match_method.ML" + method solves methods m = (m; fail) +method repeat_new methods m = (m ; (repeat_new \m\)?) + + +section \Debugging methods\ + +method_setup print_raw_goal = \Scan.succeed (fn ctxt => fn facts => + (fn (ctxt, st) => ( + Output.writeln (Thm.string_of_thm ctxt st); + Seq.make_results (Seq.single (ctxt, st)))))\ + +method_setup print_headgoal = + \Scan.succeed (fn ctxt => fn _ => fn (ctxt', thm) => + ((SUBGOAL (fn (t,_) => + (Output.writeln + (Pretty.string_of (Syntax.pretty_term ctxt t)); all_tac)) 1 thm); + (Seq.make_results (Seq.single (ctxt', thm)))))\ + +ML \fun method_evaluate text ctxt facts = + Method.NO_CONTEXT_TACTIC ctxt + (Method.evaluate_runtime text ctxt facts)\ + +method_setup timeit = + \Method.text_closure >> (fn m => fn ctxt => fn facts => + let + fun timed_tac st seq = Seq.make (fn () => Option.map (apsnd (timed_tac st)) + (timeit (fn () => (Seq.pull seq)))); + + fun tac st' = + timed_tac st' (method_evaluate m ctxt facts st'); + + in SIMPLE_METHOD tac [] end) +\ + + +section \Simple Combinators\ + +method_setup defer_tac = \Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))\ +method_setup prefer_last = \Scan.succeed (fn _ => SIMPLE_METHOD (PRIMITIVE (Thm.permute_prems 0 ~1)))\ + +method_setup all = + \Method.text_closure >> (fn m => fn ctxt => fn facts => + let + fun tac i st' = + Goal.restrict i 1 st' + |> method_evaluate m ctxt facts + |> Seq.map (Goal.unrestrict i) + + in SIMPLE_METHOD (ALLGOALS tac) facts end) +\ + +method_setup determ = + \Method.text_closure >> (fn m => fn ctxt => fn facts => + let + fun tac st' = method_evaluate m ctxt facts st' + + in SIMPLE_METHOD (DETERM tac) facts end) +\ + +method_setup changed = + \Method.text_closure >> (fn m => fn ctxt => fn facts => + let + fun tac st' = method_evaluate m ctxt facts st' + + in SIMPLE_METHOD (CHANGED tac) facts end) +\ + + +text \The following @{text fails} and @{text succeeds} methods protect the goal from the effect + of a method, instead simply determining whether or not it can be applied to the current goal. + The @{text fails} method inverts success, only succeeding if the given method would fail.\ + +method_setup fails = + \Method.text_closure >> (fn m => fn ctxt => fn facts => + let + fun fail_tac st' = + (case Seq.pull (method_evaluate m ctxt facts st') of + SOME _ => Seq.empty + | NONE => Seq.single st') + + in SIMPLE_METHOD fail_tac facts end) +\ + +method_setup succeeds = + \Method.text_closure >> (fn m => fn ctxt => fn facts => + let + fun can_tac st' = + (case Seq.pull (method_evaluate m ctxt facts st') of + SOME (st'',_) => Seq.single st' + | NONE => Seq.empty) + + in SIMPLE_METHOD can_tac facts end) +\ + + + +text \Finding a goal based on successful application of a method\ + +method_setup find_goal = + \Method.text_closure >> (fn m => fn ctxt => fn facts => + let + fun prefer_first i = SELECT_GOAL + (fn st' => + (case Seq.pull (method_evaluate m ctxt facts st') of + SOME (st'',_) => Seq.single st'' + | NONE => Seq.empty)) i THEN prefer_tac i + + in SIMPLE_METHOD (FIRSTGOAL prefer_first) facts end)\ + + end