Re: [isabelle] rule Unifies With Chained Facts?
On Mon, Apr 4, 2011 at 1:27 AM, Makarius <makarius at sketis.net> wrote:
> On Sun, 3 Apr 2011, Jun Inoue wrote:
>> I was trying "by (-, rule foo)", but now I see why that was no good. :)
>> For the record, if anyone reads this in the archives: "by - (rule foo)"
>> performs two separate method calls, a no-op and (rule foo), which
>> automatically induces a "stick assumptions into the premises" step in
>> between, whereas "by (-, rule foo)" performs one call to a single, composite
>> method which does nothing special in between the no-op and (rule foo).
> Yes, the initial proof method of 'by' is just one big expressen, where every
> participant receives the same facts.
By anyone's standard, I would be considered an "expert" Isabelle
user... and in my years of experience with Isar I never knew this! How
did that happen?
> You often see this mistake in the
> by (method1, method2)
> where it really should be
> by method1 method2
Now that I think about it, I can remember many situations where I had
written something like
by (method1, rule foo, method 2)
and it failed for some reason that I didn't understand. Now it makes sense.
Unfortunately, my usual first reaction was to rewrite this as
apply - by (method1, rule foo, method 2)
making it *less* structured, instead of as
by method1 (rule foo, method 2)
which I suppose would be considered more "proper".
How are average users expected to learn these things?
This archive was generated by a fusion of
Pipermail (Mailman edition) and