Email Gateway (Aug 18 2022 at 09:37): Email Gateway (Aug 18 2022 at 09:37):From: Joao Marcos <jmarcos@dimap.ufrn.br>
Dear ALL:
We still have some trouble adapting some theories that we have
developed for Isabelle 2004 so as to make them work in the 2005
distribution. Specifically, this time we had a reformulation of the
classic theory of sequents that initiates with:
SPROP = Sequents +
...
The thing is that we use at the end of the file two lines of ML code
intended to translate in between the internal and the external
representation of sequents in Isabelle, namely:
val parse_translation = [("TruepropExt",Sequents.two_seq_tr "Trueprop")];
val print_translation = [("Trueprop",Sequents.two_seq_tr' "TruepropExt")];
But these do not work anymore. When we call our theory SPROP.thy
inside Isabelle we receive the message:
Loading theory "SPROP"
### Non-Isar file format for theory "SPROP" -- deprecated
Error: in '/tmp/isabelle-jmarcos5522/SPROP_thy.ML', line 14.
Structure (Sequents) has not been declared
Found near [ ( "TruepropExt", Sequents.two_seq_tr("Trueprop"))]
Error: in '/tmp/isabelle-jmarcos5522/SPROP_thy.ML', line 15.
Structure (Sequents) has not been declared
Found near [ ( "Trueprop", Sequents.two_seq_tr'("TruepropExt"))]
Exception- Fail "Static errors (pass2)" raised
Can anyone suggest a corrective measure?
Thanx in advance!
Joao Marcos
Email Gateway (Aug 18 2022 at 09:37):From: Makarius <makarius@sketis.net>
On Tue, 5 Sep 2006, Joao Marcos wrote:
Loading theory "SPROP"
### Non-Isar file format for theory "SPROP" -- deprecated
Error: in '/tmp/isabelle-jmarcos5522/SPROP_thy.ML', line 14.
Structure (Sequents) has not been declared
Found near [ ( "TruepropExt", Sequents.two_seq_tr("Trueprop"))]Error: in '/tmp/isabelle-jmarcos5522/SPROP_thy.ML', line 15.
Structure (Sequents) has not been declared
Found near [ ( "Trueprop", Sequents.two_seq_tr'("TruepropExt"))]
As usual, fgrep -r will do the job:
fgrep -r two_seq_tr Isabelle2005/src/Sequents
Isabelle2005/src/Sequents/ILL.thy: ("@Context", two_seq_tr "Context"),
Isabelle2005/src/Sequents/ILL.thy: ("Context", two_seq_tr'"@Context"),
Isabelle2005/src/Sequents/LK0.thy:parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
Isabelle2005/src/Sequents/LK0.thy:print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
Isabelle2005/src/Sequents/Sequents.thy:fun two_seq_tr c [s1,s2] =
Isabelle2005/src/Sequents/Sequents.thy:fun two_seq_tr' c [s1, s2] =
In other words these ML translations functions are now pervasive, the
Sequents structure has disappeared.
BTW, any kind of ML programming works much better with the new theory
format. Just use the commands 'print_translation' or 'parse_translation'
here (see also the isar-ref manual).
Makarius
Email Gateway (Aug 18 2022 at 09:37):From: Makarius <makarius@sketis.net>
It became a nonterminal, see the declaration in Sequents.thy
You probably still have 'consts' with non-logical types. Changing this
into 'syntax' should do the job.
Makarius
Email Gateway (Aug 18 2022 at 09:37):From: Joao Marcos <jmarcos@dimap.ufrn.br>
Many thanx for the quick reply. I definitely need to study the
isar-ref manual carefully. I wish there was somewhere a summary "for
dummies" of all the modifications introduced by the new theory
format...
Now, the declarations I had for Trueprop and TruepropExt were the following:
Trueprop :: [seq'=>seq',seq'=>seq']=>prop
TruepropExt :: [seq,seq]=>prop ("((_)/ |- (_))" [6,6] 5)
The error message I now get, when reading my theory after taking your
explanation about the pervasiveness of Sequents, is the following:
### Non-Isar file format for theory "SPROP" -- deprecated
*** Illegal occurrence of syntactic type: "seq"
*** The error(s) above occurred in type "[seq , seq ] => prop "
*** in declaration of constant "TruepropExt"
Exception- ERROR raised
Exception- ERROR raised
I have opened both Sequents.thy and the isar-ref manual to see if I
can understand, but I still wonder: what in the world has happened
with the type "seq"??
Thanks in advance, again, for the help. Best,
JM
Last updated: May 03 2024 at 04:19 UTC