// ---------------------------------------------------------------- // $Id: circle.txt,v 1.4 1999/07/13 06:39:49 schreine Exp $ // circles in the plane // // (c) 1999, Wolfgang Schreiner, see file COPYRIGHT // http://www.risc.uni-linz.ac.at/software/formal // ---------------------------------------------------------------- option silent = true; // p is a point pred Point(p) <=> and(Tuple(p), =(2, length(p)), Nat(.0(p)), Nat(.1(p))); // the center and the image range fun c = tuple(50, 25); fun rangeX = nat(-(.0(c), .1(c)), +(.0(c), .1(c))); fun rangeY = nat(0, *(2, .1(c))); // the square of the difference of a and b fun -^2(a: Nat, b: Nat) = let (d = if (<=(a, b), -(b, a), -(a, b)): *(d, d)); // approximate equality of a and b pred ~=(a: Nat, b: Nat) <=> let (diff = 25: if (<=(a, b), <=(-(b, a), diff), <=(-(a, b), diff))); // p and q are approximately on same circle pred ~(p: Point, q: Point) <=> let (r = +(-^2(.0(p), .0(c)), -^2(.1(p), .1(c))), s = +(-^2(.0(q), .0(c)), -^2(.1(q), .1(c))): ~=(r, s)); // the circle that goes through p fun circle(p: Point) = set(x in rangeX, y in rangeY, q = tuple(x, y): ~(p, q), q); option silent = false; // ---------------------------------------------------------------- // $Id: circle.txt,v 1.4 1999/07/13 06:39:49 schreine Exp $ // ----------------------------------------------------------------