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
> sources:
>
>  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?

- Brian





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