Re: [isabelle] Comparing two graphs
Am Mittwoch, den 12.09.2012, 17:38 +0100 schrieb John Munroe:
> 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
> Does anyone know of a good way of achieving this kind of comparison?
> Thanks a lot for your time.
This archive was generated by a fusion of
Pipermail (Mailman edition) and