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:

lemma
  assumes "A" and "B"
  shows "B" and "A"
proof -
  from assms show "A" and "B" .
qed

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?

- Brian





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