Re: [isabelle] Problems using subclasses
No, 'a has sort type, not B, as can be seen by showing the sorts with [[show_sorts]].
Inside a class context, occurrences of class parameters are mapped to the locally fixed
class parameter whenever type inference says that this is possible.
subclass (in B) C
fix x :: 'a
have "bar x = bar x" by simp
(* since the term "bar x" is accepted, definitely, x
has sort B *)
Fact names from class contexts are localised similarly. You can refer to the global
version of these facts with Test.P and Test.PQ. Then, type unification will fail.
note P[of x] PQ[of x]
(* one can access lemmas from B like P and PQ which have been
defined within the context *)
This is a known problem. And for this reason, as many theorems as possible should be
proven inside the class context. However, many theories have yet not been "optimised" in
Is this is known limitation, or did I make some mistake?
In my concrete application, I would have liked to use
ex_le_of_nat in src/HOL/Archimedean_Field to prove a subclass
relation, but could not. Instead I currently use ex_le_of_int
and copied the proof for ex_le_of_nat to finish the subclass proof,
which works, but is a bit unsatisfactory.
Alternatively, you can do an instance declaration instead of a subclass declaration:
instance B \<subseteq> C
Then, the type variable 'a has sort B in the proof, and you can use all you need. The
difference to subclass is that you do not get the sublocale declaration B < C, that
subclass implicitly issues, i.e., inside the context of B, you cannot refer to theorems
PS: All this is explained in the Isar-Ref manual, section 5.7.
This archive was generated by a fusion of
Pipermail (Mailman edition) and