Re: [isabelle] Question about classes

Hello Florian,

Thank you for your answer. In my development I need the order
on 'a types as well as on  pairs 'a * 'b, and I have a general
result using a order on 'a which is instantiated later to a order on pairs.

I think that I have finally reached a conclusion which is flexible enough,
and also sound.

I will define the class of well founded and transitive relations

class well_founded_transitive = ord +
 assumes order_trans1: "x < y /\ y < z ==> x < z"

I will also declare an uninterpreted constant

 pair:: "'a => 'b => 'c::well_founded_transitive"

and I will prove all results based on these facts

Later for concrete examples I instantiate both the
class for pairs, as well as I define the pair
using an axiom:

instantiation "*":: (well_founded_transitive, well_founded_transitive) well_founded_transitive
begin ...end

axioms pair_def: "pair a b = (a, b)";

I have tested this approach and it seems to work. I also
think that I am not introducing inconsistencies, because
I only introduce this axiom once after I instantiate
the class for pairs.


Florian Haftmann wrote:
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 ...

definition ...

lemma ...

primrec ...



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,

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