Re: [isabelle] Type class instantiation without using Isar syntax



Hi Liam,

> I have recently migrated to Isabelle 2009. I have a Haskell code base that
> produces Isabelle code automatically, however it does not produce Isar code.

just a correction of terminology: you *are* producing Isar code, just
one which is not suitable for Isabelle 2009 any longer.

> instance MyType:: eqv
>   by (intro_classes)
> 
> defs (overloaded)
>   myType_sim_def : "eqv x y == (eq x y)"
> 
> instance MyType:: equiv
>   apply (intro_classes)
>   apply (unfold myType_sim_def)
>   apply (auto)
>   done

You would translate this as follows (*):

instantiation MyType :: eqv
begin

definition
  myType_sim_def: "(eqv :: MyType => MyType => bool) = (eq x y)"

instance by intro_classes

end

instance MyType :: equiv
  apply (intro_classes)
  apply (unfold myType_sim_def)
  apply (auto)
  done

Note that the type inside the definition is necessary in some situations
for disambiguation.

With the new infrastructure, you can also abolish the class eqv, putting
both operations and specifications in the same class (*):

class equiv =
  fixes eqv :: "'a => 'a => bool"
  assumes <whatever>

instantiation MyType :: equiv
begin

definition
  myType_sim_def: "(eqv :: MyType => MyType => bool) = (eq x y)"

instance MyType :: equiv
  apply (intro_classes)
  apply (unfold myType_sim_def)
  apply (auto)
  done


Hope this helps,
	Florian

(*) this text is not checked for typos

-- 

Home:
http://www.in.tum.de/~haftmann

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.