[isabelle] Auto-expand fixed constant in type class



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.