Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems using subclasses

Email Gateway (Aug 19 2022 at 12:11):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,

I stumbled upon the following problem: it seems, that it is not possible
to access generic lemmas with sort-constraints for proving a subclass
relation:

theory Test
imports Main
begin

consts P :: "'a => 'a => bool"
consts Q :: "'a => 'a => bool"

class A =
fixes foo :: "'a => 'a"

class B = A +
fixes bar :: "'a => 'a"
assumes P: "P (x :: 'a) (foo x)"
begin
lemma PQ: "P (x :: 'a) y ==> Q x y" sorry
end

lemma Q: "Q (x :: 'a :: B) (foo x)"
using P[of x] PQ by auto

class C = A +
assumes QQ: "? y. Q (x :: 'a) y"

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 *)

note P[of x] PQ[of x]
(* one can access lemmas from B like P and PQ which have been
defined within the context *)

show "? y. Q x y" using Q[of x] ..
(* delivers "Type unification failed: Variable 'a::type not of sort B" *)
(* but not lemmas like Q, which are defined outside the class via
sort constraints *)
qed
end

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.

Best regards,
René

PS: I used Isabelle2013-1-RC3

Email Gateway (Aug 19 2022 at 12:11):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.

Email Gateway (Aug 19 2022 at 12:12):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Andreas,

thanks for the clarifying answer and the link to the Isar-Ref manual.

Best,
René

Last updated: Nov 21 2024 at 12:39 UTC