Re: [isabelle] Problems with multiple patterns in simproc_setup

On 24/10/2019 10:44, lammich at wrote:
> Another common beginner's trap is the simultaneous type inference on
> lemmas. At some point, you write down a list of statements in a single
> lemma. This perfectly makes sense if the statements are related and are
> proved with the same by (auto...) method. However it is all too easy to
> have such lemmas a less general type than intended, due to all
> statements being typed simultaneously. I still run into this trap
> occasionally...

The "list of statements" is actually just a single big statement of the
general form:

     fixes xs
     assumes a: As and b: Bs
     shows c: Cs and d: Ds

where everything is simultaneously inferred -- without that there would
be a lot of confusion in applications, as empirically proven 20 years ago.

A special case is the following multi-conclusion statement:

  lemma c: Cs and d: Ds

That is still a single lemma, not multiple ones. The concept of such
simultanous facts stems from 'assume' and 'have' in Isar, which mostly
behave the same way.

By explaining complex statements properly, user confusion can be
minimized. An alternative is to teach users early on to rely on the
Prover IDE for the details.


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