[isabelle] Instantiating type variables within a modified definition declaration.



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
theory TestDef imports Main
begin
end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.