Re: [isabelle] Comparing two graphs

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.