Re: [isabelle] Question about classes



Hi Viorel,

> I have also tried to have the function pair defined by the class,
> but then it was not possible to be of the type:
> pair:: 'b * 'c => 'a.

something like

class pair_ord =
  fixes pair_less_eq :: "'a * 'b => 'a * 'b => bool"
  assumes ...

is indeed beyond the rather restricted Isabelle polymorphism.

Perhaps a possible solution is to formulate this order as locale and
develope your specfication relative to this:

locale pair_ord =
  fixes pair_less_eq :: "'a * 'b => 'a * 'b => bool"
  assumes ...
begin

definition ...

lemma ...

primrec ...

...

end

This could then be interpreted on different pair order predicates:

definition pair_less_eq_nat_int :: "nat * int => nat * int => bool"
where ...

definition pair_less_eq_list_unit :: 'a list * unit => 'a list * unit =>
bool" where ...

interpretation pair_ord_nat_int: pair_ord pair_less_eq_nat_int ...

interpretation pair_ord_list_unit: pair_ord pair_less_eq_list_unit ...


Hope this helps,
	Florian

-- 

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.