Theory CrossProduct

header {* Cross Products *}

theory CrossProduct
imports PairVector
begin

types 'a triple = "'a * 'a * 'a"

types R3 = "real * real * real"

lemma "norm ((2,3,6)::R3) = 7"
by (simp add: real_sqrt_unique)

lemma "inner ((1,2,3)::R3) (4,5,6) = ?x"
by simp

definition
  cross :: "real triple => real triple => real triple" where
  "cross = (λ(a, b, c). λ(x, y, z).
     (b*z - c*y, c*x - a*z, a*y - b*x))"

lemma cross_Pair:
  "cross (a, b, c) (x, y, z) = (b*z - c*y, c*x - a*z, a*y - b*x)"
  unfolding cross_def by simp

lemma left_cross_distrib: "cross (A + B) C = cross A C + cross B C"
by (cases A, cases B, cases C, simp add: cross_Pair left_distrib)

lemma right_cross_distrib: "cross A (B + C) = cross A B + cross A C"
by (cases A, cases B, cases C, simp add: cross_Pair right_distrib)

lemma cross_scaleR_left:
  "cross (scaleR r A) B = scaleR r (cross A B)"
by (cases A, cases B, simp add: cross_Pair right_diff_distrib)

lemma cross_scaleR_right:
  "cross A (scaleR r B) = scaleR r (cross A B)"
by (cases A, cases B, simp add: cross_Pair right_diff_distrib)

lemma Lagrange_identity:
  "(norm A)² * (norm B)² = (norm (inner A B))² + (norm (cross A B))²"
  apply (simp add: norm_squared_eq_inner)
  apply (cases A, cases B, rename_tac a b c x y z)
  apply (simp add: power2_eq_square)
  apply (simp add: cross_Pair)
  apply (simp add: left_diff_distrib right_diff_distrib)
  apply (simp add: ring_simps)
  done

lemma norm_cross_ineq: "norm (cross A B) ≤ norm A * norm B"
  apply (rule power2_le_imp_le)
  prefer 2 apply (simp add: mult_nonneg_nonneg real_sqrt_ge_zero add_nonneg_nonneg)
  apply (simp add: power_mult_distrib)
  apply (simp only: Lagrange_identity)
  apply simp
  done

interpretation bounded_bilinear_cross: bounded_bilinear [cross]
  apply (unfold_locales)
  apply (rule left_cross_distrib)
  apply (rule right_cross_distrib)
  apply (rule cross_scaleR_left)
  apply (rule cross_scaleR_right)
  apply (rule_tac x="1" in exI)
  apply (simp add: norm_cross_ineq)
  done

lemma cross_anticommute: "cross A B = - cross B A"
  apply (cases A, cases B, rename_tac a b c x y z)
  apply (simp add: cross_Pair)
  done

end