Re: [isabelle] Auto-expand fixed constant in type class

Hi Manuel,

> 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”.

Theorems in type classes are always directly mapped to the theory level:

class normalize

lemma "P ['a]
  -- {* yields `P [?'a::normalize]` in the background theory *}


It sounds to me that you might want to formalize normalization (wrt. to
divisibility units, I guess) using a locale

locale normalize =
  fixes normalize :: "'a => 'a"
  assumes …



interpretation nat!: normalize "%n::nat. n"

interpretation int!: normalize "abs :: int => int"

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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