Re: [isabelle] Questions about . method



On Mon, 19 Apr 2010, Christian Sternagel wrote:

But with

 lemma assumes "A" and "B" shows "A"

it doesn't work any longer. 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."

The above gives you a goal A and rules `A` and `B` which are all applied as rules (in the order of the text). After the first rule application, there are no goals left, so the attempt to apply `B` fails. Example situations where several rules actually can be applied: multiple goals, or single goals with facts that have premises.

The general idea of proper Isar proof methods (as opposed to semi-automated tools like "simp", or old tactic emulations like "rule_tac") is to try to take the given structure of the problem seriously. The aim is to get a text that faithfully represents the reasoning, not to accept as much as possible.

For example

  from `A` and `B` have A by this

reads to me like both A and B somehow contribute to the result, not that the second one is silently ignored. In practice there are many corner causes of proof methods, and often one could define certain fine points one way or the other, such as "this" vs. "assumption". On the spot, I do not recall all the details that lead up all details in basic Isar methods -- it always takes several rounds of in-depth studies of various mechanisms to make things fit together in the end.


Anyway, using "assumption" like methods for trivial proofs is slightly old-style since the "fact" method has come up some years ago. E.g. this works:

  lemma assumes "A" and "B" shows "A' by fact

Here the implicit scope for trivial facts is the whole of the visible proof text. You can also use (fact my_facts) to limit the scope explicitly.


	Makarius





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