[isabelle] Comparing two graphs


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

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 MHonArc.