[isabelle] Theory Design Question
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!
(Sorry for any duplication)
This archive was generated by a fusion of
Pipermail (Mailman edition) and