Re: [isabelle] Problems using subclasses



Hi René,

subclass (in B) C
proof
   fix x :: 'a
   have "bar x = bar x" by simp
   (* since the term "bar x" is accepted, definitely, x
      has sort B *)
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.

   note P[of x] PQ[of x]
   (* one can access lemmas from B like P and PQ which have been
      defined within the context *)
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.

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.
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 this respect.

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 from C.

Best,
Andreas

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 MHonArc.