Re: [isabelle] apply x apply y vs. by x y
On Mon, 27 Jul 2015, Lars Hupel wrote:
I have a proof state which can be solved by the subsequent application
of two methods, i.e.
have "P x"
apply (induct x)
If I rewrite this to
have "P x"
by (induct x) auto
the proof fails. Unfortunately I haven't been able to distill a small
example exhibiting this behaviour. Now, I know that "by x y" is
equivalent to "proof x qed y", but I always thought that is in turn
equivalent to "apply x apply y". Funnily enough, "by (x, y)" works. The
chained facts appear not to be significant here (I tried some variations).
(Back to this old thread.)
The above situation is indeed a bit odd. Too bad that there is not an
isolated experimental setup to test theories what is going on.
In principle the following equivalences of proof snippets hold:
by method1 method2
But there are various fine points, notably backtracking: "by" composes all
possibilities with the Seq.THEN / Seq.EVERY combinator, while the "apply"
script takes each step separately and uses only the first result.
In PIDE interaction, there is also a difference in forked proofs: the
proof state for "by" looks technically a bit different. Well-behaved
proof methods should not be able to discern that, but who know what really
happens here. Note that in batch mode, both the "by" and "apply" proofs
are forked uniformly.
If you still happen to have that situation at hand, we could try to
explore it further.
This archive was generated by a fusion of
Pipermail (Mailman edition) and