Re: [isabelle] Implicitly referring to previous facts in the moreover-ultimately paradigm



> I don't see anything unnatural or unnecessary about it. On the
> contrary
> too much implicit fact management can make Isar proofs hard to read
> and
> hard to maintain, also hard to explain to casual readers who are not
> familiar with the language.

In my opinion, it is indeed a bit strange that the moreover-ultimately
construction chains the implicit facts (so they are available for your
last proof) but you cannot name them.

    ultimately have "D" by (blast intro: foo)

which the more experienced Isabelle user might be tempted to write is
not exactly clearer than

    using foo[OF ...] .

So we have a construct that provides some nice implicit fact management
for the complicated cases, but not for the simpler cases, where a
simple forward proof does work.



--
  Peter








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