[isabelle] Theory Design Question



Hello all,

I was just wondering if anyone could provide some advice for the following design goal: take an existing type and instantiate it to some theory without endlessly wrapping/unwrapping things.

For example, I may create a type:

 int_func :: int => int

Then I later want to instantiate it in some theory, I can't have such a type synonym, so I wrap it in a datatype constructor. However, this tends to mean that I have to reproduce all the conceptually simpler proofs on "int => int" to "IntFunc"-wrapped version of it, duplicating my proofs for seemingly no reason.

Is there a nice way to lift proofs automatically, or somehow avoid this issue entirely? Thanks!

Regards,
Scott West

(Sorry for any duplication)





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