Theory Matrices

(*
   Mike Stannett
   Date: June 2020
   Updated: Jan 2023
*)

section ‹ Matrices ›

text ‹This theory defines $4 \times 4$ matrices.›

theory Matrices
  imports Vectors
begin


record 'a Matrix =
  trow :: "'a Point"
  xrow :: "'a Point"
  yrow :: "'a Point"
  zrow :: "'a Point"

class Matrices = Vectors
begin

fun applyMatrix :: "'a Matrix ⇒ 'a Point ⇒ 'a Point"
  where "applyMatrix m p = ⦇ tval = dot (trow m) p, xval = dot (xrow m) p,
                             yval = dot (yrow m) p, zval = dot (zrow m) p ⦈"

fun tcol :: "'a Matrix ⇒ 'a Point"
  where "tcol m = ⦇ tval = tval (trow m), xval = tval (xrow m), 
                    yval = tval (yrow m), zval = tval (zrow m) ⦈"

fun xcol :: "'a Matrix ⇒ 'a Point"
  where "xcol m = ⦇ tval = xval (trow m), xval = xval (xrow m), 
                    yval = xval (yrow m), zval = xval (zrow m) ⦈" 

fun ycol :: "'a Matrix ⇒ 'a Point"
  where "ycol m = ⦇ tval = yval (trow m), xval = yval (xrow m), 
                    yval = yval (yrow m), zval = yval (zrow m) ⦈"

fun zcol :: "'a Matrix ⇒ 'a Point"
  where "zcol m = ⦇ tval = zval (trow m), xval = zval (xrow m), 
                    yval = zval (yrow m), zval = zval (zrow m) ⦈"

fun transpose :: "'a Matrix ⇒ 'a Matrix"
  where "transpose m = ⦇ trow = (tcol m), xrow = (xcol m), 
                         yrow = (ycol m), zrow = (zcol m) ⦈"

fun mprod :: "'a Matrix ⇒ 'a Matrix ⇒ 'a Matrix"
  where "mprod m1 m2 = 
           transpose ⦇ trow = applyMatrix m1 (tcol m2), xrow = applyMatrix m1 (xcol m2),
                       yrow = applyMatrix m1 (ycol m2), zrow = applyMatrix m1 (zcol m2) ⦈"

end (* of class Matrices *)


end (* of theory Matrices *)