Email Gateway (Aug 22 2022 at 15:06): Email Gateway (Aug 22 2022 at 15:06):From: Esseger <esseger@free.fr>
Dear all,
When trying to prove that a class C is a subclass of a class B, say, I
am having trouble using lemmas that I have proved in C. The following
stupid example illustrates it well:
class A = fixes f g::"'a ⇒ 'a" assumes HA: "f x = g x"
class B = A + assumes HB: "f x = x"
class C = A + assumes HC: "g x = x"
lemma lemmaC: "g x = (x::'a::C)" using HC by auto
subclass (in C) B
proof
(fix x::'a show "f x = x" using HA[of x] HC[of x] by auto)
fix x::'a show "f x = x" using HA[of x] lemmaC[of x] by auto
qed
The proof fails, complaining that lemmaC[of x] makes no sense as the
type 'a of x is not of class C (while it is...). On the other hand, the
commented line succeeds. I do not understand what is going on here, as
to me HC and lemmaC are the same statement.
In my real use case, I want to use serious lemmas that I have proved in
C, should I use another syntax for this?
Esseger
Email Gateway (Aug 22 2022 at 15:07):From: Manuel Eberl <eberlm@in.tum.de>
The problem is that lemmaC is /not/ proved in the class C; it is proved
without any surrounding context, but with a sort constraint C on the
type 'a. This is, unfortunately, something different insofar as you
cannot use such facts from within the context of the class.
It is therefore advisable to prove facts like this within the class
context whenever possible, e.g.:
class C = A + assumes HC: "g x = x"
begin
lemma lemmaC: "g x = x"
…
end
or
context C
begin
lemma lemmaC: "g x = x"
…
end
or
lemma (in C) lemmaC: "g x = x"
…
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 15:08):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Esseger and Manuel,
In real-world cases, proving theorems within the class context may be require more work
than outside. For example, all theorems about the Isabelle constant mono live in the
global context, because mono's type is too polymorphic (two type variables) for a class
context. This means that you cannot use any theorem about mono in a subclass proof, even
if the concrete instance just contains one type variable. :-(
Fortunately, Types_To_Sets from Isabelle2016-1 can help in such cases. Import
"~~/src/HOL/Types_To_Sets/Types_To_Sets" and put the following lines outside of any
context. Then, you get a version lemmaC'' in the class context.
setup ‹Sign.add_const_constraint (@{const_name "g"}, SOME @{typ "'a ⇒ 'a"})›
setup ‹Sign.add_const_constraint (@{const_name "f"}, SOME @{typ "'a ⇒ 'a"})›
lemmas lemmaC' = lemmaC[internalize_sort "'a :: C",
unoverload "g :: 'a ⇒ 'a", unoverload "f :: 'a ⇒ 'a"]
lemma (in C) lemmaC'': "g x = x" by(rule lemmaC') unfold_locales
All this is still very experimental, but it works if you absolutely need it.
Best,
Andreas
Last updated: Apr 25 2024 at 20:15 UTC