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)
   apply auto
   done

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

    ==

  apply method1
  apply method2
  .

    ==

  apply method1
  apply method2
  apply assumption*
  done

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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.