Stream: Beginner Questions

Topic: ✔ rule_tac vs [where ..]


view this post on Zulip Robert Soeldner (Sep 01 2021 at 20:07):

Is there any difference in writing rule_tac x = "" in exI or exI[where x = ""] ?

view this post on Zulip Wenda Li (Sep 02 2021 at 06:35):

Not much difference to me, but I believe people may slightly favour the latter as the former is sometimes considered 'improper' proof methods.

"The following improper proof methods emulate traditional tactics. These admit direct access to the goal state, which is normally considered harmful!" ---isar-ref, p169.

view this post on Zulip Robert Soeldner (Sep 02 2021 at 17:31):

thank you :)

view this post on Zulip Notification Bot (Sep 02 2021 at 17:31):

Robert Soeldner has marked this topic as resolved.

view this post on Zulip Mathias Fleury (Sep 06 2021 at 05:14):

There is a key difference: rule_tac x = x in exI can refer to a bound variable (like x in !!x. P x), while the where cannot.


Last updated: Sep 25 2022 at 23:25 UTC