Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Comparing two graphs

Email Gateway (Aug 19 2022 at 08:48):

From: John Munroe <munddr@gmail.com>
Hi,

I have two graphs, f :: real => (real * real) and g :: real => (real * real) -- the output is simply the x and y value for the input x value.

Now, if if I have a lemma "f < g", I get an error saying

"No type arity prod :: ord"

I see that two pairs can't be compared with each other, but in my
situation I'd like to say that one is less than another if its y
(second) value is lower. As for comparing two such graphs, then it's a
matter of summing up all of the y (second) values and see which is
smaller.

Does anyone know of a good way of achieving this kind of comparison?

Thanks a lot for your time.

John

Email Gateway (Aug 19 2022 at 08:48):

From: Johannes Hölzl <hoelzl@in.tum.de>
Am Mittwoch, den 12.09.2012, 17:38 +0100 schrieb John Munroe:

Hi,

I have two graphs, f :: real => (real * real) and g :: real => (real * real) -- the output is simply the x and y value for the input x value.

Now, if if I have a lemma "f < g", I get an error saying

"No type arity prod :: ord"

When you load Multivariate_Analysis you get it for free.

Here the order on pairs of reals is overwritten:
(x :: real, y :: real) < (a, b) <-> x < a /\ y < b

and for the function you have:

f < g <-> ALL x. f x < g x

If you don't want to import Multivariate_Analysis why not just comparing

(snd o f) < (snd o g)

this compares the second components of f and g.

I see that two pairs can't be compared with each other, but in my
situation I'd like to say that one is less than another if its y
(second) value is lower. As for comparing two such graphs, then it's a
matter of summing up all of the y (second) values and see which is
smaller.

Does anyone know of a good way of achieving this kind of comparison?

Thanks a lot for your time.

John

Email Gateway (Aug 19 2022 at 08:50):

From: John Munroe <munddr@gmail.com>

Here the order on pairs of reals is overwritten:
(x :: real, y :: real) < (a, b) <-> x < a /\ y < b

and for the function you have:

f < g <-> ALL x. f x < g x

If you don't want to import Multivariate_Analysis why not just comparing

(snd o f) < (snd o g)

this compares the second components of f and g.

Thanks. If my notion of < compares the snd of each pair, should I
import Multivariate_Analysis and then overwrite < or should I just
define my own < without Multivariate_Analysis?

Thanks

John

I see that two pairs can't be compared with each other, but in my
situation I'd like to say that one is less than another if its y
(second) value is lower. As for comparing two such graphs, then it's a
matter of summing up all of the y (second) values and see which is
smaller.

Does anyone know of a good way of achieving this kind of comparison?

Thanks a lot for your time.

John

Last updated: Apr 25 2024 at 08:20 UTC