Email Gateway (Aug 23 2022 at 08:27): Email Gateway (Aug 23 2022 at 08:27):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
What is the difference between by (method_1, method_2),
by method_1 method_2, and apply method_1 by method_2?
I have a situation where by (simp, blast) doesn’t finish but both
by simp blast and apply simp by blast work. If I understand
correctly, the second variant allows for backtracking across both
methods, which might be the reason why it succeeds in my case. However,
I would expect the first and third variant to show the same behavior,
but they don’t.
All the best,
Wolfgang
Email Gateway (Aug 23 2022 at 08:27):From: Makarius <makarius@sketis.net>
On 12/02/2020 22:48, Wolfgang Jeltsch wrote:
What is the difference between
by (method_1, method_2),
by method_1 method_2, andapply method_1 by method_2?
The 'by' command in Isar has two arguments: initial method (which uses chained
facts), terminal method.
The comma form is a single method expression: both parts will see the facts.
If there are no facts, "by (m1, m1)" and "by m1 m2" happen to be the same, but
it would be very opportunistic (and confusing) to exploit that. So "by (cases,
auto)" is bad, it should be "by cases auto".
In rare situations, you need to feed facts to particular subexpressions in
methods. The "use" method combinator does that. It is also possible to say
"use nothing ...".
I have a situation where
by (simp, blast)doesn’t finish but both
by simp blastandapply simp by blastwork. If I understand
correctly, the second variant allows for backtracking across both
methods, which might be the reason why it succeeds in my case. However,
I would expect the first and third variant to show the same behavior,
but they don’t.
Backtracking is yet another detail. Between commands (e.g. 'apply', 'by')
there is none, but between parts of a closed method expression you get the
usual composition of possibilities.
All this is documented in the isar-ref manual (scattered over some places).
Makarius
Last updated: Nov 21 2024 at 12:39 UTC