Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] type classes and assumptions

Email Gateway (Aug 22 2022 at 21:13):

From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
Hi,
I am using the type class

class not_singleton =
assumes not_singleton_card: "∃x. ∃y. x ≠ y"

I have proved the following result

lemma onorm_open_ball_scaled_not_singleton:
fixes f :: ‹'a::{real_normed_vector, not_singleton} ⇒ 'b::real_normed_vector›
and r :: real
assumes ‹r > 0› and ‹bounded_linear f›
shows ‹onorm f = (1/r) * Sup {norm (f x) | x. norm x < r}›

Now, I would like to use onorm_open_ball_scaled_not_singleton in order to deduce the following result

lemma onorm_open_ball_scaled_not_singleton2:
fixes f :: ‹'a::real_normed_vector ⇒ 'b::real_normed_vector›
and r :: real
assumes ‹r > 0› and ‹bounded_linear f› and ‹∃ x::'a. ∃ y::'a. x ≠ y›
shows ‹onorm f = (1/r) * Sup {norm (f x) | x. norm x < r}›
using assms
onorm_open_ball_scaled_not_singleton

Nevertheless, there is a problem, because

'a is of type real_normed_vector and not of type {real_normed_vector, not_singleton}

From a purely mathematical point of view, this question is never asked (just abuse the notation), but it is relevant for the formalization in Isabelle/HOL.

Thank you in advance for any suggestions.
José M.

Email Gateway (Aug 22 2022 at 21:14):

From: Peter Lammich <lammich@in.tum.de>
Hi Jose,

a

subclass (in real_normed_vector) not_singleton

might help.

Email Gateway (Aug 22 2022 at 21:14):

From: Dominique Unruh <unruh@ut.ee>
Hi,

subclass (in real_normed_vector) not_singleton

That will not work because a real_normed_vector can have cardinality 1.
(The zero space.)

I believe the only way to get from onorm_open_ball_scaled_not_singleton
to onorm_open_ball_scaled_not_singleton2 is to use the Types_To_Sets
extension of Isabelle/HOL.

Then *onorm_open_ball_scaled_not_singleton[internalize_sort
"'a::{real_normed_vector, not_singleton}"] *gives you a theorem that is
logically sufficient for showing onorm_open_ball_scaled_not_singleton2.

(Try *thm * *onorm_open_ball_scaled_not_singleton[internalize_sort
"'a::{real_normed_vector, not_singleton}"] *to see it.)

Best wishes,
Dominique.

**

might help.

--
Peter

On Tue, 2020-01-14 at 03:06 +0000, Jose Manuel Rodriguez Caballero
wrote:

Hi,
I am using the type class

class not_singleton =
assumes not_singleton_card: "∃x. ∃y. x ≠ y"

I have proved the following result

lemma onorm_open_ball_scaled_not_singleton:
fixes f :: ‹'a::{real_normed_vector, not_singleton} ⇒
'b::real_normed_vector›
and r :: real
assumes ‹r > 0› and ‹bounded_linear f›
shows ‹onorm f = (1/r) * Sup {norm (f x) | x. norm x < r}›

Now, I would like to use onorm_open_ball_scaled_not_singleton in
order to deduce the following result

lemma onorm_open_ball_scaled_not_singleton2:
fixes f :: ‹'a::real_normed_vector ⇒ 'b::real_normed_vector›
and r :: real
assumes ‹r > 0› and ‹bounded_linear f› and ‹∃ x::'a. ∃ y::'a. x ≠
y›
shows ‹onorm f = (1/r) * Sup {norm (f x) | x. norm x < r}›
using assms
onorm_open_ball_scaled_not_singleton

Nevertheless, there is a problem, because

'a is of type real_normed_vector and not of
type {real_normed_vector, not_singleton}

From a purely mathematical point of view, this question is never
asked (just abuse the notation), but it is relevant for the
formalization in Isabelle/HOL.

Thank you in advance for any suggestions.
José M.

--

José Manuel Rodríguez Caballero

arvutiteaduse instituut / Institute of Computer Science
Tartu Ülikool / University of Tartu

Personal Research Page: https://josephcmac.github.io/

Email Gateway (Aug 22 2022 at 21:14):

From: Peter Lammich <lammich@in.tum.de>
Ah, OK.

You will have to decide where to use type-classes or explicit
assumptions:

getting an explicit assumption from a type-class is easy,
but getting a type-class from an explicit assumption is not possible
(or maybe requires the type-to-sets extension, as indicated by
Dominique).

Email Gateway (Aug 22 2022 at 21:14):

From: Dominique Unruh <unruh@ut.ee>
Hi,

but getting a type-class from an explicit assumption is not possible
(or maybe requires the type-to-sets extension, as indicated by Dominique).

As an additional clarification: To my understanding, Types_To_Sets is a
true extension of HOL in the sense that it introduces additional proof
rules (that are, I hope, conservative extensions).

However, the specific attribute "internalize_sort" is (that replaces
type-classes by explicit premises stating the properties of those type
classes), as far as I can tell, not an extension. There is
Thm.unconstrainT in the Isabelle kernel that does more or less the same
thing (but in a less user-friendly way). And the internalize_sort
attribute is just a more convenient wrapper around the existing
low-level functionality.

Best wishes,
Dominique.

Email Gateway (Aug 22 2022 at 21:14):

From: Lawrence Paulson <lp15@cam.ac.uk>
You’ve done these in the wrong order. First prove onorm_open_ball_scaled_not_singleton2 (your old proof should work with only tiny changes) and then onorm_open_ball_scaled_not_singleton should be a trivial corollary.

Larry Paulson

Last updated: Apr 18 2024 at 12:27 UTC