Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Quick question about rule+


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 12:29 UTC