Re: [isabelle] Questions about . method
On Mon, 19 Apr 2010, Christian Sternagel wrote:
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
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.
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and