Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Schematic goal

Email Gateway (Aug 18 2022 at 15:46):

From: Michael Chan <mchan@inf.ed.ac.uk>
Hello,

I have a quick question about schematic goal statements in 2009-2. Are
they allowed? I believe 2009-1 allows them, e.g., "EX (x::?'a)...". Now
in 2009-2, I keep getting an error saying "Illegal schematic goal
statement".

Any pointer will be appreciated. Thanks.

Michael

Email Gateway (Aug 18 2022 at 15:46):

From: Tobias Nipkow <nipkow@in.tum.de>

From the NEWS:

• Schematic theorem statements need to be explicitly markup as such,
  via commands 'schematic_lemma', 'schematic_theorem',
  'schematic_corollary'. Thus the relevance of the proof is made
  syntactically clear, which impacts performance in a parallel or
  asynchronous interactive environment. Minor INCOMPATIBILITY.

I was caught unawares by that as well recently.

Tobias

Michael Chan schrieb:

Hello,

I have a quick question about schematic goal statements in 2009-2. Are
they allowed? I believe 2009-1 allows them, e.g., "EX (x::?'a)...". Now
in 2009-2, I keep getting an error saying "Illegal schematic goal
statement".

Any pointer will be appreciated. Thanks.

Michael

Email Gateway (Aug 18 2022 at 15:46):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hello Michael,

since Isabelle2009-2, goal statements that involve schematic variables
must be marked explicitly: Use schematic_lemma instead of lemma,
schematic_theorem instead of theorem, etc. See also the NEWS file for
this change.

Also note that you only need schematic type variables if you want to
instantiate the type only during the proof and are too lazy to write
this type down in full in the goal statement. If you want your lemma to
be polymorphic, just omit the question mark and use an ordinary type
variable. Existential type quantification is not possible in HOL anyway.

"EX (x::'a). ..."

Hope this helps,
Andreas

Michael Chan schrieb:

Email Gateway (Aug 18 2022 at 15:47):

From: Makarius <makarius@sketis.net>
This means the explicit 'schematic_lemma' commands not only help the
system in performance tuning, but also users to prevent accidental use of
schematic variables. In particular, schematic types in goal statements
make various proof tools do unexpected things. (Often they stem from
copying the printed version of existing facts.)

The normal way is to give fixed statements, and let the system produce
a general result in the very end.

Makarius

Last updated: Apr 19 2024 at 01:05 UTC