[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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and