Theory Quaternion (Isabelle repository version)

header {* Quaternions *}

theory Quaternion
imports InnerProduct
begin

subsection {* Definition *}

datatype quaternion = Quaternion complex complex

subsection {* Addition and Subtraction *}

instantiation quaternion :: ab_group_add
begin

definition
  zero_quaternion_def: "0 = Quaternion 0 0"

fun plus_quaternion where
  quaternion_plus:
    "Quaternion a b + Quaternion c d = Quaternion (a + c) (b + d)"

fun minus_quaternion where
  quaternion_minus:
    "Quaternion a b - Quaternion c d = Quaternion (a - c) (b - d)"

fun uminus_quaternion where
  quaternion_uminus:
    "- Quaternion a b = Quaternion (- a) (- b)"

instance proof
  fix a b c :: quaternion
  show "(a + b) + c = a + (b + c)"
    by (induct a, induct b, induct c, simp)
  show "a + b = b + a"
    by (induct a, induct b, simp)
  show "0 + a = a"
    unfolding zero_quaternion_def
    by (induct a, simp)
  show "- a + a = 0"
    unfolding zero_quaternion_def
    by (induct a, simp)
  show "a - b = a + - b"
    by (induct a, induct b, simp)
qed

end

lemma quaternion_eq_zero [simp]:
  "Quaternion a b = 0 <-> a = 0 ∧ b = 0"
by (simp add: zero_quaternion_def)

subsection {* Multiplication *}

lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
by (simp add: scaleR_conv_of_real complex_cnj_mult)

lemmas complex_cnj_simps =
  complex_cnj_add
  complex_cnj_diff
  complex_cnj_minus
  complex_cnj_mult
  complex_cnj_divide
  complex_cnj_inverse
  complex_cnj_scaleR

lemmas ring_distribs =
  left_distrib
  right_distrib
  left_diff_distrib
  right_diff_distrib

instantiation quaternion :: ring_1
begin

fun times_quaternion where
  quaternion_times:
    "Quaternion a b * Quaternion c d =
      Quaternion (a * c - d * cnj b) (cnj a * d + c * b)"

definition
  one_quaternion_def: "1 = Quaternion 1 0"

instance proof
  fix x y z :: quaternion
  show "(x * y) * z = x * (y * z)"
    by (induct x, induct y, induct z,
        simp add: complex_cnj_simps ring_distribs)
  show "1 * x = x"
    unfolding one_quaternion_def by (induct x, simp)
  show "x * 1 = x"
    unfolding one_quaternion_def by (induct x, simp)
  show "(x + y) * z = x * z + y * z"
    by (induct x, induct y, induct z,
        simp add: complex_cnj_simps ring_distribs)
  show "x * (y + z) = x * y + x * z"
    by (induct x, induct y, induct z,
        simp add: complex_cnj_simps ring_distribs)
  show "(0::quaternion) ≠ 1"
    unfolding one_quaternion_def zero_quaternion_def by simp
qed

end

subsection {* Vector space *}

lemmas scaleR_distribs = 
  scaleR_left_distrib
  scaleR_right_distrib
  scaleR_left_diff_distrib
  scaleR_right_diff_distrib

instantiation quaternion :: real_algebra_1
begin

fun scaleR_quaternion where
  quaternion_scaleR:
    "scaleR r (Quaternion a b) = Quaternion (scaleR r a) (scaleR r b)"

instance proof
  fix r s :: real and x y :: quaternion
  show "scaleR r (x + y) = scaleR r x + scaleR r y"
    by (induct x, induct y, simp add: scaleR_right_distrib)
  show "scaleR (r + s) x = scaleR r x + scaleR s x"
    by (induct x, induct y, simp add: scaleR_left_distrib)
  show "scaleR r (scaleR s x) = scaleR (r * s) x"
    by (induct x, induct y, simp)
  show "scaleR 1 x = x"
    by (induct x, simp)
  show "scaleR r x * y = scaleR r (x * y)"
    by (induct x, induct y, simp add: complex_cnj_simps scaleR_distribs)
  show "x * scaleR r y = scaleR r (x * y)"
    by (induct x, induct y, simp add: complex_cnj_simps scaleR_distribs)
qed

end

lemma quaternion_of_real_eq:
  "of_real r = Quaternion (of_real r) 0"
unfolding of_real_def one_quaternion_def by simp


subsection {* Norm and inner product *}

instantiation quaternion :: real_inner
begin

fun inner_quaternion where
  quaternion_inner:
    "inner (Quaternion a b) (Quaternion c d) = inner a c + inner b d"

fun norm_quaternion where
  quaternion_norm:
    "norm (Quaternion a b) = sqrt ((norm a)² + (norm b)²)"

definition
  sgn_quaternion_def:
    "sgn (x::quaternion) = scaleR (inverse (norm x)) x"

instance proof
  fix r :: real and x y z :: quaternion
  show "sgn x = scaleR (inverse (norm x)) x"
    by (rule sgn_quaternion_def)
  show "inner x y = inner y x"
    by (induct x, induct y)
       (simp add: inner_commute)
  show "inner (x + y) z = inner x z + inner y z"
    by (induct x, induct y, induct z)
       (simp add: inner_left_distrib)
  show "inner (scaleR r x) y = r * inner x y"
    by (induct x, induct y)
       (simp add: inner_scaleR_left right_distrib)
  show "0 ≤ inner x x"
    by (induct x)
       (simp add: add_nonneg_nonneg inner_ge_zero)
  show "inner x x = 0 <-> x = 0"
    by (induct x)
       (simp add: add_nonneg_eq_0_iff inner_ge_zero inner_eq_zero)
  show "norm x = sqrt (inner x x)"
    by (induct x)
       (simp add: norm_eq_sqrt_inner inner_ge_zero)
qed

end

subsection {* Conjugate *}

fun
  qcnj :: "quaternion => quaternion"
where
  quaternion_cnj:
    "qcnj (Quaternion a b) = Quaternion (cnj a) (- b)"

lemma complex_cnj_mult: "cnj x * x = of_real ((norm x)²)"
unfolding complex_of_real_def
by (induct x, simp add: power2_eq_square [symmetric])

lemma complex_mult_cnj: "x * cnj x = of_real ((norm x)²)"
unfolding complex_of_real_def
by (induct x, simp add: power2_eq_square [symmetric])

lemma quaternion_cnj_mult: "qcnj x * x = of_real ((norm x)²)"
unfolding quaternion_of_real_eq
by (induct x, simp add: complex_cnj_simps complex_cnj_mult complex_mult_cnj)

lemma quaternion_mult_cnj: "x * qcnj x = of_real ((norm x)²)"
unfolding quaternion_of_real_eq
by (induct x, simp add: complex_cnj_simps complex_cnj_mult complex_mult_cnj)

subsection {* Inverse *}

instantiation quaternion :: division_ring
begin

definition
  inverse_quaternion_def:
    "inverse x = scaleR (inverse ((norm x)²)) (qcnj x)"

instance proof
  fix x :: quaternion
  assume "x ≠ 0"
  thus "inverse x * x = 1"
    unfolding inverse_quaternion_def
    by (simp add: quaternion_cnj_mult of_real_def)
next
  fix x :: quaternion
  assume "x ≠ 0"
  thus "x * inverse x = 1"
    unfolding inverse_quaternion_def
    by (simp add: quaternion_mult_cnj of_real_def)
qed

end

instance quaternion :: real_normed_div_algebra
proof
  fix x y :: quaternion
  show "norm (x * y) = norm x * norm y"
    apply (induct x, induct y, simp)
    apply (rename_tac a b c d)
    apply (simp add: real_sqrt_mult [symmetric])
    apply (simp add: norm_squared_eq_inner)
    apply (simp add: inner_diff inner_distrib)
    apply (simp add: ring_distribs)
    apply (simp add: norm_squared_eq_inner [symmetric])
    apply (simp only: norm_mult power_mult_distrib)
    apply (simp add: inner_commute)
    apply (simp add: inner_complex_def)
    apply (simp add: ring_simps)
    done
qed

end