Lines Matching defs:linear
641 val linear = ``\f. ?m b. !x. f x = m * x + b:int``;
642 val add = prove(``^linear f /\ ^linear g ==> ^linear (\x. f x + g x)``,
646 val mul1 = prove(``^linear f ==> ^linear (\x. f x * c)``,
650 val mul2 = prove(``^linear f ==> ^linear (\x. c * f x)``,
654 val sub = prove(``^linear (\x. a x + ~b x) ==> ^linear (\x. a x - b x)``,
656 val neg = prove(``^linear f ==> ^linear (\x. ~ f x)``,
659 val id = prove(``^linear (\x.x)``,
662 val const = prove(``^linear(\x.c)``,