[isabelle] Instantiating type variables within a modified definition declaration.
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.
theory TestDef imports Main
This archive was generated by a fusion of
Pipermail (Mailman edition) and