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
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
Description: OpenPGP digital signature



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