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


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

On 11/10/2016 12:38 PM, Viorel Preoteasa wrote:
I think that I sent an empty theory file. Here I send it

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

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