Email Gateway (Aug 18 2022 at 13:59): Email Gateway (Aug 18 2022 at 13:59):From: Steve W <s.wong.731@googlemail.com>
Hi,
I'm wondering what apply rule+ does. I can't seem to find any mention of
rule+ in the reference manual. Could someone please give some pointers?
Thanks
Steve
Email Gateway (Aug 18 2022 at 14:00):From: Peter Lammich <peter.lammich@uni-muenster.de>
Steve W wrote:
rule tries to apply a rule that has an "intro?" attribute.
()+ is a tactic that repeats its argument tactic until it fails, at
least once.
cf §6.3.1 and §6.3.3 of Isabelle/Isar Reference manual.
Hope this helps,
Peter
Email Gateway (Aug 18 2022 at 14:00):From: Makarius <makarius@sketis.net>
The "+" Operator repeats any proof method, not just "rule". See 6.3.1
"Proof method expressions" in the isar-ref manual.
Makarius
Email Gateway (Aug 18 2022 at 14:00):From: Makarius <makarius@sketis.net>
Note that a "tactic" is just a low-level refinement operation on a goal
state. In Isabelle type tactic = thm -> thm Seq.seq, i.e. lazy map from
state to any number of possible successor states. (Each state is of the
form subgoals ==> main_goal.)
A "tactical" is a higher-order tactic combinator, such as THEN, REPEAT,
etc.
In Isar, a "method" is a bit like a "rich tactic", with extra information
about context and used facts, and with potential results of "cases" (as in
the "induct" method).
So the "+" operator above would be a "methodical", but this terminology is
not used.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC