Theory Gyrotrigonometry

theory Gyrotrigonometry
imports Main GyroVectorSpace
begin

datatype 'a otriangle = M_gyrotriangle (A:'a) (B:'a) (C:'a)

context pre_gyrovector_space
begin

definition unit :: "'a ⇒ 'b" where
  "unit a = to_carrier a /⇩R ⟪a⟫"

lemma norm_inner_le_1:
  fixes a b :: 'b
  assumes "norm a ≤ 1" "norm b ≤ 1"
  shows "norm (inner a b) ≤ 1"
  using assms
  by (smt (verit, ccfv_SIG) Cauchy_Schwarz_ineq2 mult_le_one norm_ge_zero real_norm_def)

lemma norm_inner_unit:
  shows "norm (inner (unit (⊖ a ⊕ b)) (unit (⊖ a ⊕ c))) ≤ 1"
proof-
  have "norm (unit (⊖ a ⊕ b)) = ⟪⊖ a ⊕ b⟫ / ⟪⊖ a ⊕ b⟫"
    by (simp add: unit_def gyronorm_def)
  then have "norm (unit (⊖ a ⊕ b)) ≤ 1"
    by simp
  moreover
  have "norm (unit (⊖ a ⊕ c)) = ⟪⊖ a ⊕ c⟫ / ⟪⊖ a ⊕ c⟫"
    by (simp add: unit_def gyronorm_def)
  then have "norm (unit (⊖ a ⊕ c)) ≤ 1"
    by simp
  ultimately
  show ?thesis
    using norm_inner_le_1 
    by blast
qed

definition angle :: "'a ⇒ 'a ⇒ 'a ⇒ real" where 
  "angle a b c = arccos (inner (unit (⊖ a ⊕ b)) (unit (⊖ a ⊕ c)))"

definition o_ray :: "'a ⇒ 'a ⇒ 'a set" where
  "o_ray x p = {s::'a. ∃t::real. t ≥ 0 ∧ s = (x ⊕ t ⊗ (⊖ x ⊕ p))}"

lemma T8_5:
  assumes "b2 ∈ o_ray a1 b1" "b2 ≠ a1" 
          "c2 ∈ o_ray a1 c1" "c2 ≠ a1"
  shows "angle a1 b1 c1 = angle a1 b2 c2"
proof-
  obtain t1::real where t1: "t1 > 0" "b2 = a1 ⊕ t1 ⊗ (⊖ a1 ⊕ b1)"
    using assms less_eq_real_def o_ray_def by auto
  then have "⊖ a1 ⊕ b2 = t1 ⊗ (⊖ a1 ⊕ b1)"
     using gyro_left_cancel' by simp

  obtain t2::real where t2: "t2 > 0" "c2 = a1 ⊕ t2 ⊗ (⊖ a1 ⊕ c1)"
    using assms less_eq_real_def o_ray_def by auto
  then have "⊖ a1 ⊕ c2 = t2 ⊗ (⊖ a1 ⊕ c1)"
    using gyro_left_cancel' by simp

  have "angle a1 b2 c2 =  arccos (inner (to_carrier (⊖ a1 ⊕ b2) /⇩R ⟪⊖ a1 ⊕ b2⟫)
                                        (to_carrier (⊖ a1 ⊕ c2) /⇩R ⟪⊖ a1 ⊕ c2⟫))"
    using angle_def unit_def by presburger
  also have "… =
              arccos (inner (to_carrier (t1 ⊗ (⊖ a1 ⊕ b1)) /⇩R ⟪t1 ⊗ (⊖ a1 ⊕ b1)⟫)
                            (to_carrier (t2 ⊗ (⊖ a1 ⊕ c1)) /⇩R ⟪t2 ⊗ (⊖ a1 ⊕ c1)⟫))"
    using ‹⊖ a1 ⊕ b2 = t1 ⊗ (⊖ a1 ⊕ b1)› ‹⊖ a1 ⊕ c2 = t2 ⊗ (⊖ a1 ⊕ c1)› by auto
  finally show ?thesis
    unfolding angle_def unit_def
    using t1 t2
    by (smt (verit, best) scale_prop1 times_zero)
qed

definition get_a :: "'a otriangle ⇒ 'a" where
  "get_a t = ⊖ (C t) ⊕ (B t)"
definition get_b :: "'a otriangle ⇒ 'a" where
  "get_b t = ⊖ (C t) ⊕ (A t)"
definition get_c :: "'a otriangle ⇒ 'a" where
  "get_c t = ⊖ (B t) ⊕ (A t)"

definition get_alpha :: "'a otriangle ⇒ real" where
  "get_alpha t = angle (A t) (B t) (C t)"
definition get_beta :: "'a otriangle ⇒ real" where
  "get_beta t = angle (B t) (C t) (A t)"
definition get_gamma :: "'a otriangle ⇒ real" where
  "get_gamma t = angle (C t) (A t) (B t)"

definition cong_gyrotriangles :: "'a otriangle ⇒ 'a otriangle ⇒ bool" where
  "cong_gyrotriangles t1 t2 ⟷ 
     (⟪get_a t1⟫ = ⟪get_a t2⟫ ∧ ⟪get_b t1⟫ = ⟪get_b t2⟫ ∧ ⟪get_c t1⟫ = ⟪get_c t2⟫ ∧ 
      (get_alpha t1 = get_alpha t2) ∧ (get_beta t1 = get_beta t2) ∧ (get_gamma t1 = get_gamma t2))"
end

end