[isabelle] classes and interpretations



 Hello,

I am trying to use the class mechanism for a collection of algebraic
structures and I got into the following problem:

class A = ord + times + one +
  assumes
    .... (axioms which ensures the existence of an infimum operation)
begin
  definition
     "inf_l a b = ..."
end

interpretation semilattice_inf "op <=" "op <" "inf_l";
  by ...

The problem is now when I state some lemmas:

lemma l1: "inf_l (a:'a::A) b <= a"
lemma (in A) l2: "inf_l a b <= a"

The first problem is that although lemmas l1 and l2 seem similar, they cannot
be applied in the same contexts. Lemma l2 seem more general than lemma l1.

The second problem. The fact that inf_l is an infimum operation, given by the interpretation, is available when proving lemma l1, but not when proving lemma l2. How should I state the interpretation such that it becomes available when proving
a lemma like l2?

Best regards,

Viorel Preoteasa









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