# $Id: tpoint.n3,v 1.2 2001/10/01 00:12:36 amdus Exp $

# given a circle with center x0, y0 and radius r
# given a line going through a point x1, y1
# what are the tangent points x, y
#
# some mathematical formula conventions
#   [ :sum a, b, ...]     --> a + b + ...
#   [ :product a, b, ...] --> a * b * ...
#   [ :minus a]           --> -a
#   [ :slash a]           --> 1/a
#   [ :square a]          --> a**2
#   [ :sqrt a]            --> a**1/2

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <tpoint#>.

{{[:center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]]}
  log:implies
 {[ :center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]] :slope [ :product
    [ :sum [ :minus [ :product :2, :x1, [ :sum :y1, [ :minus :y0]]]],
      [ :sqrt [ :sum [ :product :4, [ :square :x1], [ :square [ :sum :y1, [ :minus :y0]]]],
        [ :minus [ :product :4, [ :sum [ :square :r], [ :minus [ :square [ :sum :x0, [ :minus :x1]]]]],
          [ :sum [ :square :r], [ :minus [ :square [ :sum :y0, :y1]]],
            [ :product :2, :y0, [ :sum :x0, [ :minus :y1]]]]]]]]],
    [ :slash [ :product :2, [ :sum [ :square :r], [ :minus [ :square [ :sum :x0, [ :minus :x1]]]]]]]]}}
  a log:Truth; log:forAll :x0, :y0, :x1, :y1, :r.

{{[:center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]]}
  log:implies
 {[ :center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]] :slope [ :product
    [ :sum [ :minus [ :product :2, :x1, [ :sum :y1, [ :minus :y0]]]],
      [ :minus [ :sqrt [ :sum [ :product :4, [ :square :x1], [ :square [ :sum :y1, [ :minus :y0]]]],
        [ :minus [ :product :4, [ :sum [ :square :r], [ :minus [ :square [ :sum :x0, [ :minus :x1]]]]],
          [ :sum [ :square :r], [ :minus [ :square [ :sum :y0, :y1]]],
            [ :product :2, :y0, [ :sum :x0, [ :minus :y1]]]]]]]]]],
    [ :slash [ :product :2, [ :sum [ :square :r], [ :minus [ :square [ :sum :x0, [ :minus :x1]]]]]]]]}}
  a log:Truth; log:forAll :x0, :y0, :x1, :y1, :r.

{{[ :center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]] :slope :m}
  log:implies
 {[ :center [ :X :x0; :Y :y0]; :radius :r; :apoint [ :X :x1; :Y :y1]] :tpoint
    [ :X [ :product [ :sum [ :product [ :square :m], :x1], [ :minus [ :product :m, :y1]], :x0, [ :product :m, :y0]],
      [ :slash [ :sum [ :square :m], :1]]];
      :Y [ :product [ :sum [ :product :m, :x0], [ :product [ :square :m], :y0], [ :minus [ :product :m, :x1]], :y1],
      [ :slash [ :sum [ :square :m], :1]]]]}}
  a log:Truth; log:forAll :m, :x0, :y0, :x1, :y1, :r.