Email Gateway (Aug 19 2022 at 13:33): Email Gateway (Aug 19 2022 at 13:33):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 19 2022 at 13:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Manuel,
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
signature.asc
Last updated: Apr 19 2024 at 12:27 UTC