# [isabelle] Auto-expand fixed constant in type class

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Auto-expand fixed constant in type class
*From*: Manuel Eberl <eberlm at in.tum.de>
*Date*: Sun, 19 Jan 2014 18:18:19 +0100
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

Hallo,
I have a typeclass that fixes a function “normalise :: 'a ⇒ 'a” and some
other stuff, and provides some lemmas involving “normalise”. Now let's
say I have an instantiation for nat, in which normalise is “λx. x” and
one for int, in which it is “abs”.
Let's say the typeclass proves the lemma foo: “normalise x = normalise y
⟷ associated x y”
I would now like to have the lemmas from the typeclass directly
available for nat and int, and without any appearance of “normalise”;
any occurrence of “normalise” in the lemmas should automatically be
replaced by “λx. x” resp. “abs”, i.e. I would like to have lemmas
foo_nat: “(x::nat) = y ⟷ associated x y” and foo_int: “abs (x::int) = y
⟷ associated x y”.
Is that possible?
Cheers,
Manuel

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