[isabelle] classes and interpretations
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 +
.... (axioms which ensures the existence of an infimum operation)
"inf_l a b = ..."
interpretation semilattice_inf "op <=" "op <" "inf_l";
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
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
interpretation, is available when proving lemma l1, but not when
proving lemma l2.
How should I state the interpretation such that it becomes available
a lemma like l2?
This archive was generated by a fusion of
Pipermail (Mailman edition) and