Re: [isabelle] Questions about . method
On Mon, Apr 19, 2010 at 3:28 AM, Christian Sternagel
<christian.sternagel at uibk.ac.at> wrote:
> Wouldn't it be nice, to have a short way of
> proving such simple statements (where one of the current facts solves the
> goal). E.g.,
> lemma assumes "A" and "B" shows "A' using assms .
> And indeed, isn't that, what the documentation claims? In isar-ref.pdf on
> page 88, I read "this applies all of the current facts directly as rules."
I think the documentation means to say that "." can use multiple facts
to prove multiple goals. Here's an example:
assumes "A" and "B"
shows "B" and "A"
from assms show "A" and "B" .
By the way, you can get a fairly short proof using "rule", like this:
lemma assumes "A" and "B" shows "A" by (rule assms)
Of course, this relies on having a named set of facts. To use the
chained facts in this way you would need something like
have "A" and "B" by ...
note foo = this
show "A" by (rule foo)
which isn't quite as nice. I agree that a proof method with the
semantics you described would be useful. It probably wouldn't take too
much code to implement; why don't you try writing one?
This archive was generated by a fusion of
Pipermail (Mailman edition) and