Stream: Isabelle/ML

Topic: ✔ Solving a list of trivial goals


view this post on Zulip Ciarán Dunne (Apr 19 2022 at 08:30):

Suppose I have xs : thm list and a proof state whose subgoals are the members of xs. Is there any easy Isabelle/ML way to solve each subgoal? Currently I'm using insert_tac, and global_immediate_proof. Thanks!

view this post on Zulip Dmitriy Traytel (Apr 19 2022 at 08:32):

Doesn't resolve_tac ctxt xs work?

view this post on Zulip Jan van Brügge (Apr 19 2022 at 08:47):

Probably REPEAT_DETERM o resolve_tac ctxt xs if there are multiple subgoals

view this post on Zulip Ciarán Dunne (Apr 19 2022 at 09:00):

Thanks @Jan van Brügge and @Dmitriy Traytel, using the REPEAT_DETERM tactical on resolve did the job!

view this post on Zulip Notification Bot (Apr 24 2022 at 16:42):

Ciarán Dunne has marked this topic as resolved.


Last updated: Mar 28 2024 at 16:17 UTC