*To*: cl-isabelle-users at lists.cam.ac.uk, Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Auto-expand fixed constant in type class*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sun, 19 Jan 2014 21:31:10 +0100*In-reply-to*: <52DC08DB.9040308@in.tum.de>*Organization*: TU Munich*References*: <52DC08DB.9040308@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

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 begin lemma "P ['a] <prf> -- {* yields `P [?'a::normalize]` in the background theory *} end 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 … begin … end interpretation nat!: normalize "%n::nat. n" <prf> interpretation int!: normalize "abs :: int => int" <prf> Hope this helps, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Auto-expand fixed constant in type class***From:*Manuel Eberl

- Previous by Date: [isabelle] Auto-expand fixed constant in type class
- Next by Date: Re: [isabelle] conflicting versions
- Previous by Thread: [isabelle] Auto-expand fixed constant in type class
- Next by Thread: [isabelle] Isabelle/jEdit - default logic
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list