header {* Two-dimensional spaces *}

theory Vec2 = Set + Transcendental + VectorSpace + Integration: 

section{* 
  A formalisation of two-dimensional vector spaces, polar coordinates and 
  analytic functions. *}

types 
 vector    = "real*real" 
 angle     = real
 point     = "vector"
 pose      = "(point * angle)"   

subsection {* Two-Dimensional Vector spaces *}

text {* The vector space ${\mathbb R}^2  *}


text {* Norm and orientation *}
constdefs
  norm         :: "vector => real"             ("|_|" [50] 50)
 "norm == %(vx, vy). sqrt (vx^2 + vy^2)"
  orient :: "vector => angle"
 "orient == %(vx, vy). arctan (vy/vx)"

text {* Addition, negation, subtraction *}
constdefs
  vadd         :: "vector => vector => vector"         (infixr "++" 62)
 "vadd == %(vx, vy) (wx, wy).(vx+ wx, vy+ wy)"
  vneg    :: "vector => vector"                        ("-- _" [40] 40)
 "vneg == %(vx, vy). (-vx, -vy)"
  vminus       :: "vector => vector => vector"         (infixl "--" 62)
 "vminus v w == v ++ (-- w)"

text {* Distance *}
constdefs
  dist         :: "vector => vector => real"
 "dist v w == |w -- v|"

text {* Scalar multiplication and inner product *}
constdefs
  smult        :: "real => vector => vector"     (infixr "·" 70)
 "smult x == %(vx, vy). (x* vx, x* vy)"
  innerProd    :: "vector => vector => real"     (infixr "**" 65)
 "innerProd == %(vx, vy) (wx, wy). (vx* wx+ vy* wy)"

text {* Null and unit vector *}
constdefs
  null         :: vector
 "null == (0, 0)"
  unit         :: vector
 "unit == (1, 1)"

subsection{* Rotation *}

constdefs 
  rot :: "angle => vector => vector"
 "rot a == %(vx, vy). (vx* cos a- vy* sin a, vx*sin a+ vy* cos a)"

subsection{* Polar Coordinates *}

types 
  pvector = "real* angle"


constdefs
  abs :: "pvector =>  real"
 "abs v == fst v"
  dir :: "pvector => angle"
 "dir v == snd v"

constdefs
  polar :: "vector => pvector"
 "polar v == ( |v|, orient v)"

constdefs
  cartesian :: "pvector => vector"
 "cartesian v == ((abs v) * (cos (dir v)), (abs v)  * (sin (dir v)))"


end