Email Gateway (Aug 17 2022 at 13:28): Email Gateway (Aug 17 2022 at 13:28):From: John Matthews <matthews@galois.com>
Thanks, Makarius. Unfortunately, the code I wrote isn't being
executed by Isar. I've attached two files that illustrate the
problem. The isar.thy file installs the new theorem attribute, and
isar_test.thy tries to use it. I've instrumented the theorem
attributes with "print" instructions, but none of them seem to fire.
Also, what is the difference between "local" and "global" theorem
attributes? That is, when should I use Classical.put_local_claset
versus Classical.put_global_claset?
Thanks in advance,
-john
isar.thy
isar_test.thy
Email Gateway (Aug 17 2022 at 13:28):From: Makarius <makarius@sketis.net>
On Mon, 28 Nov 2005, John Matthews wrote:
The isar.thy file installs the new theorem attribute, and isar_test.thy
tries to use it. I've instrumented the theorem attributes with "print"
instructions, but none of them seem to fire.
Oddly, there seems to be something wrong with print being used here --
maybe the compiler removes this from encapsulated toplevel expressions.
I do use PolyML.print regularly, but usually from actual ML files, rather
than immediate ML code as encountered here. Using Isabelle's own functions
does work, e.g. warning or writeln.
I also see your solver stemming from the D2 rule in the claset.
Also note that attribute names quoted in a theory need to conform to the
identifier syntax given in the isar-ref manual. This is quite liberal,
but does not include a bang as part of a word. The attributes in
Provers/classical.ML do this by parsing there own arguments (cf.
occurences of Args.bang, Args.bang_colon).
Also, what is the difference between "local" and "global" theorem
attributes? That is, when should I use Classical.put_local_claset versus
Classical.put_global_claset?
Attributes operate either in a theory (global) of proof context (local). A
global attribute should change the theory -- there is no proof context
available anyway, a local attribute should change the proof context (in
purely functional manner).
Makarius
Last updated: Nov 21 2024 at 12:39 UTC