Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Instantiating type variables within a modified...

Email Gateway (Aug 22 2022 at 14:36):

From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,

I am trying to introduce syntax for a definition like
construct, that in addition to creating the definition,
would also insatiate all type variables to a given type
(bool for simplicity)

For example the declaration:

mydef "TestDefA a = (a = a)"

will create the theorem TestDefA_def:

"TestDefA (a::bool) = (a = a)"

I am trying to do this in the following way:

- generalize the type variables using Thm.generalize
- Drule.instantiate_normalize to instantiate the schematic type to bool

This works on a theorem that has been generated with
Simplifier.rewrite, but it does not work when I try to
apply it to the theorem within the code for creating the
definition, just before Local_Theory.notes.
When I try to generalize the type variables I get the error:

exception THM 0 raised (line 1127 of "thm.ML"):
generalize: variable free in assumptions
TestDefA ?a = (?a = ?a) [TestDefA ≡ ??.TestDef.TestDefA]

While writing this I realized, that it is not enough
just to change the theorem of the definition to work
on bool, but I also need to change the constant to
work on bool only.

Attached is the theory where I try to define this
new type of definition.

Any help would be appreciated.

Best regards,

Viorel Preoteasa
TestDef.thy

Email Gateway (Aug 22 2022 at 14:36):

From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
I think that I sent an empty theory file. Here I send it
again.

Best regards,

Viorel Preoteasa

onstruct, that in addition to creating the definition,
would also insatiate all type variables to a given type
(bool for simplicity)

For example the declaration:

mydef "TestDefA a = (a = a)"

will create the theorem TestDefA_def:

"TestDefA (a::bool) = (a = a)"

I am trying to do this in the following way:

- generalize the type variables using Thm.generalize
- Drule.instantiate_normalize to instantiate the schematic type to bool

This works on a theorem that has been generated with
Simplifier.rewrite, but it does not work when I try to
apply it to the theorem within the code for creating the
definition, just before Local_Theory.notes.
When I try to generalize the type variables I get the error:

exception THM 0 raised (line 1127 of "thm.ML"):
generalize: variable free in assumptions
TestDefA ?a = (?a = ?a) [TestDefA ≡ ??.TestDef.TestDefA]

While writing this I realized, that it is not enough
just to change the theorem of the definition to work
on bool, but I also need to change the constant to
work on bool only.

Attached is the theory where I try to define this
new type of definition.

Any help would be appreciated.

Best regards,

Viorel Preoteasa
TestDef.thy

Email Gateway (Aug 22 2022 at 14:37):

From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,

I figured out now the solution to my problem. It seems enough
just to change all type variables to the given type
in prop just before calling:

val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;

in function gen_def

Best regards,

Viorel Preoteasa

Last updated: Apr 20 2024 at 08:16 UTC