# Theory Octonions

```(* Title:      Octonions.thy
Author:     Angeliki Koutsoukou-Argyraki, University of Cambridge
Date:       September 2018
*)
section‹Theory of Octonions›
theory Octonions
imports Cross_Product_7
begin

subsection‹Basic definitions›

text‹As with the complex numbers, coinduction is convenient.›

codatatype octo =
Octo (Ree: real) (Im1: real) (Im2: real) (Im3: real) (Im4: real)
(Im5: real) (Im6: real) (Im7: real)

lemma octo_eqI [intro?]:
"⟦Ree x = Ree y; Im1 x = Im1 y; Im2 x = Im2 y; Im3 x = Im3 y;
Im4 x = Im4 y;Im5 x = Im5 y;  Im6 x = Im6 y; Im7 x = Im7 y⟧ ⟹ x = y"
by (rule octo.expand) simp

lemma octo_eq_iff:
"x = y ⟷ Ree x = Ree y ∧ Im1 x = Im1 y ∧ Im2 x = Im2 y ∧ Im3 x = Im3 y ∧
Im4 x = Im4 y ∧ Im5 x = Im5 y ∧ Im6 x = Im6 y  ∧ Im7 x = Im7 y"
by (auto intro: octo.expand)

context
begin

primcorec octo_e0 :: octo ("e0")
where "Ree e0 = 1" | "Im1 e0 = 0" | "Im2 e0 = 0" | "Im3 e0 = 0"
| "Im4 e0 = 0" | "Im5 e0 = 0" | "Im6 e0 = 0" | "Im7 e0 = 0"

primcorec octo_e1 :: octo  ("e1")
where "Ree e1 = 0" | "Im1 e1 = 1" | "Im2 e1 = 0" | "Im3 e1 = 0"
| "Im4 e1 = 0" | "Im5 e1 = 0" | "Im6 e1 = 0" | "Im7 e1 = 0"

primcorec octo_e2 :: octo  ("e2")
where "Ree e2 = 0" | "Im1 e2 = 0" | "Im2 e2 = 1" | "Im3 e2 = 0"
| "Im4 e2 = 0" | "Im5 e2 = 0" | "Im6 e2 = 0" | "Im7 e2 = 0"

primcorec octo_e3 :: octo ("e3")
where "Ree e3 = 0" | "Im1 e3 = 0" | "Im2 e3 = 0" | "Im3 e3 = 1"
| "Im4 e3 = 0" | "Im5 e3 = 0" | "Im6 e3 = 0" | "Im7 e3 = 0"

primcorec octo_e4 :: octo ("e4")
where "Ree e4 = 0" | "Im1 e4 = 0" | "Im2 e4 = 0" | "Im3 e4 = 0"
| "Im4 e4 = 1" | "Im5 e4 = 0" | "Im6 e4 = 0" | "Im7 e4 = 0"

primcorec octo_e5 :: octo ("e5")
where "Ree e5 = 0" | "Im1 e5 = 0" | "Im2 e5 = 0" | "Im3 e5 = 0"
| "Im4 e5 = 0" | "Im5 e5 = 1" | "Im6 e5 = 0" | "Im7 e5 = 0"

primcorec octo_e6 :: octo ("e6")
where "Ree e6 = 0" | "Im1 e6 = 0" | "Im2 e6 = 0" | "Im3 e6 = 0"
| "Im4 e6 = 0" | "Im5 e6 = 0" | "Im6 e6 = 1" | "Im7 e6 = 0"

primcorec octo_e7 :: octo ("e7")
where "Ree e7 = 0" | "Im1 e7 = 0" | "Im2 e7 = 0" | "Im3 e7 = 0"
| "Im4 e7 = 0" | "Im5 e7 = 0" | "Im6 e7 = 0" | "Im7 e7 = 1"
end

subsection ‹Addition and Subtraction: An Abelian Group›

begin

primcorec zero_octo
where "Ree 0 = 0" |"Im1 0 = 0" | "Im2 0 = 0" | "Im3 0 = 0"
|"Im4 0 = 0" | "Im5 0 = 0" | "Im6 0 = 0" | "Im7 0 = 0"

primcorec plus_octo
where
"Ree (x + y) = Ree x + Ree y"
| "Im1 (x + y) = Im1 x + Im1 y"
| "Im2 (x + y) = Im2 x + Im2 y"
| "Im3 (x + y) = Im3 x + Im3 y"
| "Im4 (x + y) = Im4 x + Im4 y"
| "Im5 (x + y) = Im5 x + Im5 y"
| "Im6 (x + y) = Im6 x + Im6 y"
| "Im7 (x + y) = Im7 x + Im7 y"

primcorec uminus_octo
where
"Ree (- x) = - Ree x"
| "Im1 (- x) = - Im1 x"
| "Im2 (- x) = - Im2 x"
| "Im3 (- x) = - Im3 x"
| "Im4 (- x) = - Im4 x"
| "Im5 (- x) = - Im5 x"
| "Im6 (- x) = - Im6 x"
| "Im7 (- x) = - Im7 x"

primcorec minus_octo
where
"Ree (x - y) = Ree x - Ree y"
| "Im1 (x - y) = Im1 x - Im1 y"
| "Im2 (x - y) = Im2 x - Im2 y"
| "Im3 (x - y) = Im3 x - Im3 y"
| "Im4 (x - y) = Im4 x - Im4 y"
| "Im5 (x - y) = Im5 x - Im5 y"
| "Im6 (x - y) = Im6 x - Im6 y"
| "Im7 (x - y) = Im7 x - Im7 y"

instance

end

lemma octo_eq_0_iff:
"x = 0 ⟷ Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2 +
Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^ 2  = 0"
proof
assume "(octo.Ree x)⇧2 + (Im1 x)⇧2 + (Im2 x)⇧2 + (Im3 x)⇧2 + (Im4 x)⇧2 + (Im5 x)⇧2 + (Im6 x)⇧2
+ (Im7 x)⇧2 = 0"
then have "∀qa. qa - x = qa"
then show "x = 0"
by simp
qed auto

subsection ‹A Normed Vector Space›

instantiation octo :: real_vector

begin

primcorec scaleR_octo
where
"Ree (scaleR r x) = r * Ree x"
| "Im1 (scaleR r x) = r * Im1 x"
| "Im2 (scaleR r x) = r * Im2 x"
| "Im3 (scaleR r x) = r * Im3 x"
| "Im4 (scaleR r x) = r * Im4 x"
| "Im5 (scaleR r x) = r * Im5 x"
| "Im6 (scaleR r x) = r * Im6 x"
| "Im7 (scaleR r x) = r * Im7 x"

instance
by standard (auto simp: octo_eq_iff distrib_left distrib_right  scaleR_add_right)

end

instantiation octo::one
begin
primcorec one_octo

where
"Ree 1 = 1" |  "Im1 1 = 0"  | "Im2 1 = 0" |  "Im3 1 = 0" |
"Im4 1 = 0" |  "Im5 1 = 0"  | "Im6 1 = 0" | "Im7 1 = 0"

instance by standard
end

fun octo_proj
where
"octo_proj x 0 = ( Ree (x))"
| "octo_proj x (Suc 0) = ( Im1(x))"
| "octo_proj x (Suc (Suc 0)) = ( Im2 ( x))"
| "octo_proj x (Suc (Suc (Suc 0))) = ( Im3( x))"
| "octo_proj x (Suc (Suc (Suc (Suc 0)))) = ( Im4( x))"
| "octo_proj x (Suc(Suc (Suc (Suc (Suc 0))))) = ( Im5( x))"
| "octo_proj x (Suc(Suc (Suc (Suc (Suc (Suc 0)))))) = ( Im6( x))"
| "octo_proj x (Suc( Suc(Suc (Suc (Suc (Suc (Suc 0))))))) = ( Im7( x))"

assumes "i ≤ 7"
shows "octo_proj (x+y) i = octo_proj x i + octo_proj y i"

proof -
consider "i = 0" | "i = 1" | "i = 2" | "i = 3" | "i = 4" | "i = 5" | "i = 6" | "i = 7"
using  assms by force

then show ?thesis
by cases (auto simp:  numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5
numeral_6_eq_6  numeral_7_eq_7 numeral_7_eq_7)
qed

instantiation octo ::real_normed_vector
begin

definition  "norm x = sqrt ((Ree x)⇧2 + (Im1 x)⇧2 + (Im2 x)⇧2 + (Im3 x)⇧2  +
(Im4 x)⇧2 + (Im5 x)⇧2 + (Im6 x)⇧2+ (Im7 x)⇧2  )" for x::octo

definition "sgn x = x /⇩R norm x" for x :: octo

definition "dist x y = norm (x - y)" for x y :: octo

definition [code del]:
"(uniformity :: (octo × octo) filter) = (INF e∈{0 <..}. principal {(x, y). dist x y < e})"

definition [code del]:
"open (U :: octo set) ⟷ (∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"

lemma norm_eq_L2: "norm x = L2_set (octo_proj x) {..7}"
by (simp add: norm_octo_def L2_set_def eval_nat_numeral)

instance proof
fix r :: real and x y :: octo and S :: "octo set"
show "(norm x = 0) ⟷ (x = 0)"
have eq: "L2_set (octo_proj (x + y)) {..7} = L2_set (λi. octo_proj x i + octo_proj y i) {..7}"
by (rule L2_set_cong) (auto simp: octo_proj_add)
show "norm (x + y) ≤ norm x + norm y"
by (simp add: norm_eq_L2 eq L2_set_triangle_ineq)
show "norm (scaleR r x) = ¦r¦ * norm x"
power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
qed (rule sgn_octo_def dist_octo_def open_octo_def uniformity_octo_def)+

end

lemma norm_octo_squared:
"norm x ^ 2 = Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2 +
Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^ 2"

instantiation octo :: real_inner
begin

definition inner_octo where
"inner_octo x y = Ree x * Ree y + Im1 x * Im1 y + Im2 x * Im2 y + Im3 x * Im3 y
+ Im4 x * Im4 y + Im5 x * Im5 y + Im6 x * Im6 y +  Im7 x * Im7 y " for x y::octo

instance
by standard (auto simp: inner_octo_def algebra_simps norm_octo_def

end

lemma octo_inner_1 [simp]: "inner 1 x = Ree x"
and octo_inner_1_right [simp]: "inner x 1 = Ree x"
unfolding inner_octo_def by simp_all

lemma octo_inner_e1_left [simp]: "inner e1 x = Im1 x"
and octo_inner_e1_right [simp]: "inner x e1 = Im1 x"
unfolding inner_octo_def by simp_all

lemma octo_inner_e2_left [simp]: "inner e2 x = Im2 x"
and octo_inner_e2_right [simp]: "inner x e2 = Im2 x"
unfolding inner_octo_def by simp_all

lemma octo_inner_e3_left [simp]: "inner e3 x = Im3 x"
and  octo_inner_e3_right [simp]: "inner x e3 = Im3 x"
unfolding inner_octo_def by simp_all

lemma octo_inner_e4_left [simp]: "inner e4 x  = Im4 x"
and octo_inner_e4_right [simp]: "inner x e4 = Im4 x"
unfolding inner_octo_def by simp_all

lemma octo_inner_e5_left [simp]: "inner e5 x  = Im5 x"
and  octo_inner_e5_right [simp]: "inner x e5 = Im5 x"
unfolding inner_octo_def by simp_all

lemma octo_inner_e6_left [simp]: "inner e6 x  = Im6 x"
and octo_inner_e6_right [simp]: "inner x e6 = Im6 x"
unfolding inner_octo_def by simp_all

lemma octo_inner_e7_left [simp]: "inner e7 x  = Im7 x"
and octo_inner_e7_right [simp]: "inner x e7 = Im7 x"
unfolding inner_octo_def by simp_all

lemma octo_norm_pow_2_inner: "(norm x) ^ 2 = inner x x " for x::octo

lemma octo_norm_property:
"inner x y = (1/2)* ((norm(x+y))^2 - (norm(x))^2 - (norm(y))^2) " for x y ::octo

subsection ‹The Octonionic product and related properties and lemmas›

text‹The multiplication is defined following one of the 480 equivalent multiplication tables
in an analogy to the definition of the 7D cross product. ›

instantiation octo :: times
begin

definition times_octo :: "[octo, octo] ⇒ octo"
where
"(a * b) =  (let
t0 = Ree a * Ree b - Im1 a * Im1 b - Im2 a * Im2 b- Im3 a * Im3 b
- Im4 a * Im4 b  - Im5 a * Im5 b - Im6 a * Im6 b  -Im7 a * Im7 b ;
t1 =  Ree a * Im1 b +   Im1 a * Ree b + Im2 a * Im4 b +Im3 a * Im7 b -
Im4 a * Im2  b  +Im5 a * Im6 b - Im6 a * Im5 b - Im7 a * Im3 b ;
t2 =  Ree a *  Im2 b - Im1 a * Im4 b+ Im2 a  * Ree b + Im3 a * Im5 b
+ Im4 a * Im1 b  - Im5 a * Im3 b + Im6 a * Im7 b - Im7 a *Im6 b  ;
t3 =  Ree a * Im3 b -Im1 a * Im7 b -Im2 a *Im5 b +Im3 a * Ree b + Im4 a * Im6 b
+  Im5 a *Im2 b  - Im6 a * Im4 b + Im7 a * Im1 b ;
t4 = Ree a * Im4 b + Im1 a * Im2 b - Im2 a * Im1 b -Im3 a * Im6 b + Im4 a * Ree b
+Im5 a * Im7 b +Im6 a * Im3 b -Im7 a * Im5 b ;
t5 = Ree a * Im5 b - Im1 a * Im6 b +Im2 a * Im3 b -Im3 a * Im2 b -Im4 a * Im7 b
+Im5 a * Ree b  +Im6 a * Im1 b + Im7 a  * Im4 b;
t6 = Ree a * Im6 b + Im1 a * Im5 b - Im2 a * Im7 b +Im3 a * Im4 b - Im4 a * Im3 b
-Im5 a * Im1 b + Im6 a * Ree b + Im7 a * Im2 b  ;
t7 = Ree a * Im7 b + Im1 a * Im3 b +Im2 a * Im6 b - Im3 a * Im1 b + Im4 a * Im5 b
-Im5 a * Im4 b - Im6 a * Im2 b +Im7 a * Ree b
in Octo t0 t1 t2 t3 t4 t5 t6 t7)"

instance by standard

end

instantiation octo ::inverse
begin

primcorec inverse_octo
where
"Ree (inverse x) = Ree x / (Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2
+Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^2   )"
| "Im1 (inverse x) = - (Im1 x) / (Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2
+Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^2)"
| "Im2 (inverse x) = - (Im2 x) / (Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2
+Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^2 )"
| "Im3 (inverse x) = - (Im3 x) / (Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2
+Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^2    )"
| "Im4 (inverse x) = - (Im4 x) / (Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2
+Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^2    )"
| "Im5 (inverse x) = - (Im5 x) / (Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2
+Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^2)"
| "Im6 (inverse x) = - (Im6 x) / (Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2
+Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^2    )"
| "Im7 (inverse x) = - (Im7 x) / (Ree x ^ 2 + Im1 x ^ 2 + Im2 x ^ 2 + Im3 x ^ 2
+Im4 x ^ 2 + Im5 x ^ 2 + Im6 x ^ 2 + Im7 x ^2    )"

definition "x div y = x  * ( inverse y)" for x y :: octo

instance by standard

end

lemma octo_mult_components:
"Ree (x *  y ) =  Ree x *  Ree y - Im1 x * Im1 y -  Im2 x * Im2 y - Im3 x * Im3 y
- Im4 x * Im4 y - Im5 x * Im5 y - Im6 x * Im6 y-  Im7 x * Im7 y"
"Im1 (x  *  y )  =  Ree x * Im1 y +   Im1 x * Ree y + Im2 x * Im4 y +Im3 x * Im7 y -
Im4 x * Im2 y    +Im5 x * Im6 y - Im6 x * Im5 y - Im7 x * Im3 y "
" Im2 (x  *  y )  =  Ree x *  Im2 y - Im1 x * Im4 y+ Im2 x  * Ree y + Im3 x * Im5 y
+ Im4 x * Im1 y  - Im5 x * Im3 y + Im6 x * Im7 y - Im7 x *Im6 y  "
" Im3 (x * y ) =  Ree x * Im3 y -Im1 x * Im7 y -Im2 x *Im5 y +Im3 x * Ree y + Im4 x * Im6 y
+  Im5 x *Im2 y  - Im6 x * Im4 y + Im7 x * Im1 y "
"Im4  (x *y ) =  Ree x * Im4 y + Im1 x * Im2 y - Im2 x * Im1 y -Im3 x * Im6 y + Im4 x * Ree y
+Im5 x * Im7 y +Im6 x * Im3 y -Im7 x * Im5 y  "
"Im5  (x * y ) = Ree x * Im5 y - Im1 x * Im6 y +Im2 x * Im3 y -Im3 x * Im2 y -Im4 x * Im7 y
+Im5 x * Ree y  +Im6 x * Im1 y + Im7 x  * Im4 y  "
" Im6  (x *  y) = Ree x * Im6 y + Im1 x * Im5 y - Im2 x * Im7 y +Im3 x * Im4 y - Im4 x * Im3 y
-Im5 x * Im1 y + Im6 x * Ree y + Im7 x * Im2 y   "
"Im7 (x * y)  = Ree x * Im7 y + Im1 x * Im3 y +Im2 x * Im6 y - Im3 x * Im1 y + Im4 x * Im5 y
-Im5 x * Im4 y - Im6 x * Im2 y +Im7 x * Ree y  "
unfolding times_octo_def by auto

lemma octo_distrib_left :
"a * (b + c) = a * b + a * c" for a b c ::octo
unfolding times_octo_def  plus_octo_def minus_octo_def uminus_octo_def scaleR_octo_def
by (simp add: octo_eq_iff octo_mult_components algebra_simps)

lemma octo_distrib_right :
"(b + c) * a = b * a + c * a" for a b c ::octo
unfolding times_octo_def  plus_octo_def minus_octo_def uminus_octo_def scaleR_octo_def
by (simp add: octo_eq_iff octo_mult_components algebra_simps)

lemma multiplicative_norm_octo: "norm (x * y) = norm x * norm y" for x y ::octo
proof -
have "norm (x * y) ^ 2 = norm x ^ 2 * norm y ^ 2"
unfolding norm_octo_squared octo_mult_components by algebra
also have "... = (norm x * norm y) ^ 2"
finally show ?thesis by simp
qed

lemma mult_1_right_octo [simp]: "x * 1 = (x :: octo)"
and mult_1_left_octo [simp]: "1 * x = (x :: octo)"

instance octo :: power ..

lemma power2_eq_square_octo: "x ^ 2 = (x * x :: octo)"

lemma octo_product_alternative_left: "x * (x * y) = (x * x :: octo) * y"
unfolding octo_eq_iff octo_mult_components by algebra

lemma octo_product_alternative_right: "x * (y * y) = (x * y :: octo) * y"
unfolding octo_eq_iff octo_mult_components by algebra

lemma octo_product_flexible: "(x * y) * x = x * (y * x :: octo)"
unfolding octo_eq_iff octo_mult_components by algebra

lemma octo_power_commutes: "x ^ y * x = x * (x ^ y :: octo)"
by (induction y) (simp_all add: octo_product_flexible)

lemma octo_product_noncommutative: "¬(∀x y::octo. (x * y = y * x))"
by (auto simp: times_octo_def)
(metis (no_types, lifting) Im1_def add_0 mult.commute mult_1 mult_zero_left octo.case
octo_e5.simps(2) octo_e5.simps(3) octo_e5.simps(4) octo_e5.simps(5) octo_e5.simps(6)
octo_e5.simps(8) zero_neq_numeral)

lemma octo_product_nonassociative :
"¬(∀ x y z::octo. x * (y * z) = (x * y) * z)"
proof-
define x where "x = Octo 1 0 0 0 1 0 0 0"
define y where "y = Octo 1 3 0 0 0 1 0 0"
define z where "z = Octo 0 1 0 1 1 1 0 0"
have "x * (y * z) ≠ (x * y) * z"
by (simp add: octo_eq_iff octo_mult_components x_def y_def z_def)
thus ?thesis by blast
qed

subsection ‹Embedding of the Reals into the Octonions›

definition octo_of_real :: "real ⇒  octo"
where "octo_of_real r = scaleR r 1"

definition octo_of_nat :: "nat ⇒  octo"
where "octo_of_nat r = scaleR r 1"

definition octo_of_int :: "int ⇒  octo"
where "octo_of_int r = scaleR r 1"

lemma octo_of_nat_sel [simp]:
"Ree (octo_of_nat x) = of_nat x" "Im1 (octo_of_nat x) = 0" "Im2 (octo_of_nat x) = 0"
"Im3 (octo_of_nat x) = 0" "Im4 (octo_of_nat x) = 0" "Im5 (octo_of_nat x) = 0"
"Im6 (octo_of_nat x) = 0" "Im7 (octo_of_nat x) = 0"

lemma octo_of_real_sel [simp]:
"Ree (octo_of_real x) = x" "Im1 (octo_of_real x) = 0" "Im2 (octo_of_real x) = 0"
"Im3 (octo_of_real x) = 0" "Im4 (octo_of_real x) = 0" "Im5 (octo_of_real x) = 0"
"Im6 (octo_of_real x) = 0" "Im7 (octo_of_real x) = 0"

lemma octo_of_int_sel [simp]:
"Ree (octo_of_int x) = of_int x" "Im1 (octo_of_int x) = 0" "Im2 (octo_of_int x) = 0"
"Im3 (octo_of_int x) = 0" "Im4 (octo_of_int x) = 0" "Im5 (octo_of_int x) = 0"
"Im6 (octo_of_int x) = 0" "Im7 (octo_of_int x) = 0"

lemma scaleR_conv_octo_of_real: "scaleR r x = octo_of_real r * x"
by (simp add: octo_eq_iff octo_mult_components octo_of_real_def)

lemma octo_of_real_0 [simp]: "octo_of_real 0 = 0"

lemma octo_of_real_1 [simp]: "octo_of_real 1 = 1"

lemma octo_of_real_add [simp]: "octo_of_real (x + y) = octo_of_real x + octo_of_real y"

lemma octo_of_real_minus [simp]: "octo_of_real (- x) = - octo_of_real x"

lemma octo_of_real_diff [simp]: "octo_of_real (x - y) = octo_of_real x - octo_of_real y"

lemma octo_of_real_mult [simp]: "octo_of_real (x * y) = octo_of_real x * octo_of_real y"
using octo_of_real_def
by (metis scaleR_conv_octo_of_real scaleR_scaleR)

lemma octo_of_real_sum[simp]: "octo_of_real (sum f s) = (∑x∈s. octo_of_real (f x))"
by (induct s rule: infinite_finite_induct) auto

lemma octo_of_real_power [simp]:
"octo_of_real (x ^ y) = (octo_of_real x :: octo) ^ y"
by (induct y)(simp_all)

lemma octo_of_real_eq_iff [simp]: "octo_of_real x = octo_of_real y ⟷ x = y"
using octo_of_real_def
by (simp add: octo_of_real_def one_octo.code zero_octo.code)

lemmas octo_of_real_eq_0_iff [simp] = octo_of_real_eq_iff [of _ 0, simplified]
lemmas octo_of_real_eq_1_iff [simp] = octo_of_real_eq_iff [of _ 1, simplified]

lemma minus_octo_of_real_eq_octo_of_real_iff [simp]: "-octo_of_real x = octo_of_real y ⟷ -x = y"
using octo_of_real_eq_iff[of "-x" y] by (simp only: octo_of_real_minus)

lemma octo_of_real_eq_minus_of_real_iff [simp]: "octo_of_real x = -octo_of_real y ⟷ x = -y"
using octo_of_real_eq_iff[of x "-y"] by (simp only: octo_of_real_minus)

lemma octo_of_real_of_nat_eq [simp]: "octo_of_real (of_nat x) = octo_of_nat x"
unfolding octo_of_real_def

lemma octo_of_real_of_int_eq [simp]: "octo_of_real (of_int z) = octo_of_int z"
unfolding octo_of_real_def

lemma octo_of_int_of_nat:  "octo_of_int (of_nat n) = octo_of_nat n"

lemma octo_of_nat_add [simp]: "octo_of_nat (a + b) = octo_of_nat a + octo_of_nat b"
and octo_of_nat_mult [simp]: "octo_of_nat (a * b) = octo_of_nat a * octo_of_nat b"
and octo_of_nat_diff [simp]: "b ≤ a ⟹ octo_of_nat (a - b) = octo_of_nat a - octo_of_nat b"
and octo_of_nat_0 [simp]: "octo_of_nat 0 = 0"
and octo_of_nat_1 [simp]: "octo_of_nat 1 = 1"
and octo_of_nat_Suc_0 [simp]: "octo_of_nat (Suc 0) = 1"

lemma octo_of_int_add [simp]: "octo_of_int (a + b) = octo_of_int a + octo_of_int b"
and octo_of_int_mult [simp]: "octo_of_int (a * b) = octo_of_int a * octo_of_int b"
and octo_of_int_diff [simp]: "b ≤ a ⟹ octo_of_int (a - b) = octo_of_int a - octo_of_int b"
and octo_of_int_0 [simp]: "octo_of_int 0 = 0"
and octo_of_int_1 [simp]: "octo_of_int 1 = 1"

instance octo :: numeral ..

lemma numeral_octo_conv_of_nat: "numeral x = octo_of_nat (numeral x)"
proof (induction x)
case(Bit0 x)
have "numeral x+ numeral x = octo_of_nat(numeral x+ numeral x)"
thus ?case by (simp add: numeral_Bit0)
next
case(Bit1 x)
have "numeral x+ numeral x + numeral num.One=
octo_of_nat (numeral x + numeral x + numeral num.One)"
thus ?case by (simp add: numeral_Bit1)
qed auto

lemma numeral_octo_sel [simp]:
"Ree (numeral n) = numeral n" "Im1 (numeral n) = 0" "Im2 (numeral n) = 0"
"Im3 (numeral n) = 0" "Im4 (numeral n) = 0" "Im5 (numeral n) = 0"
"Im6 (numeral n) = 0" "Im7 (numeral n) = 0"

lemma octo_of_real_numeral [simp]: "octo_of_real (numeral w) = numeral w"
by (simp add: numeral_octo_conv_of_nat octo_of_real_def octo_of_nat_def)

lemma octo_of_real_neg_numeral [simp]: "octo_of_real (- numeral w) = - numeral w"
by simp

lemma octo_of_real_times_commute: "octo_of_real r * q = q * octo_of_real r"
using octo_of_real_def times_octo_def by simp

lemma octo_of_real_times_conv_scaleR: "octo_of_real x * y = scaleR x y"

lemma octo_mult_scaleR_left: "(r *⇩R x) * y = r *⇩R (x * y :: octo)"
by (simp add: octo_eq_iff octo_mult_components algebra_simps)

lemma octo_mult_scaleR_right: "x * (r *⇩R y) = r *⇩R (x * y :: octo)"
by (simp add: octo_eq_iff octo_mult_components algebra_simps)

lemma scaleR_octo_of_real [simp]: "scaleR r (octo_of_real s) = octo_of_real (r * s)"

lemma octo_of_real_times_left_commute: "octo_of_real r * (x * q) = x * (octo_of_real r * q)"
unfolding octo_of_real_times_conv_scaleR by (simp add: octo_mult_scaleR_right)

lemma nonzero_octo_of_real_inverse:
"x ≠ 0 ⟹ octo_of_real (inverse x) = inverse (octo_of_real x :: octo)"
by (simp add: octo_eq_iff power2_eq_square divide_simps)

lemma octo_of_real_inverse [simp]:
"octo_of_real (inverse x) = inverse (octo_of_real x )"
by (simp add: octo_eq_iff power2_eq_square divide_simps)

lemma nonzero_octo_of_real_divide:
"y ≠ 0 ⟹ octo_of_real (x / y) = (octo_of_real x / octo_of_real y ::octo)"

lemma octo_of_real_divide [simp]:
"octo_of_real (x / y) = (octo_of_real x / octo_of_real y :: octo)"
using divide_inverse divide_octo_def octo_of_real_def octo_of_real_inverse
by (metis octo_of_real_mult)

lemma octo_of_real_inverse_collapse [simp]:
assumes "c ≠ 0"
shows   "octo_of_real c * octo_of_real (inverse c) = 1"
"octo_of_real (inverse c) * octo_of_real c = 1"
using assms by (simp_all add: octo_eq_iff octo_mult_components power2_eq_square)

lemma octo_divide_numeral:
fixes x::octo shows "x / numeral y = x /⇩R numeral y"
using octo_of_real_times_commute[of "inverse (numeral y)"]
by (simp add: scaleR_conv_octo_of_real divide_octo_def flip: octo_of_real_numeral)

lemma octo_divide_numeral_sel [simp]:
"Ree (x / numeral w) = Ree x / numeral w"
"Im1 (x / numeral w) = Im1 x / numeral w"
"Im2 (x / numeral w) = Im2 x / numeral w"
"Im3 (x / numeral w) = Im3 x / numeral w"
"Im4 (x / numeral w) = Im4 x / numeral w"
"Im5 (x / numeral w) = Im5 x / numeral w"
"Im6 (x / numeral w) = Im6 x / numeral w"
"Im7 (x / numeral w) = Im7 x / numeral w"
unfolding octo_divide_numeral by simp_all

lemma octo_norm_units [simp]:
"norm octo_e1 = 1" "norm (e2::octo) = 1" "norm (e3::octo) = 1"
"norm (e4::octo) = 1 "  "norm (e5::octo) = 1"   "norm (e6::octo) = 1" "norm (e7::octo) = 1"
by (auto simp: norm_octo_def)

lemma e1_nz [simp]: "e1 ≠ 0"
and e2_nz [simp]: "e2 ≠ 0"
and e3_nz [simp]: "e3 ≠ 0"
and e4_nz [simp]: "e4 ≠ 0"
and e5_nz [simp]: "e5 ≠ 0"
and e6_nz [simp]: "e6 ≠ 0"
and e7_nz [simp]: "e7 ≠ 0"

subsection ‹"Expansion" into the traditional notation›

lemma octo_unfold:
"q = (Ree q) *⇩R e0 + (Im1 q) *⇩R e1 + (Im2 q) *⇩R e2 + (Im3 q) *⇩R e3
+ (Im4 q) *⇩R e4 + (Im5 q) *⇩R e5 + (Im6 q) *⇩R e6 + (Im7 q) *⇩R  e7"

lemma octo_trad: "Octo x y z w u v q g =
x *⇩R e0 + y *⇩R e1 +  z *⇩R e2  +  w *⇩R e3  +  u *⇩R e4 +  v *⇩R e5 +  q *⇩R e6  +  g*⇩R e7 "

lemma octo_of_real_eq_Octo: "octo_of_real a = Octo a 0 0 0 0 0 0 0 "

lemma e1_squared [simp]: "e1 ^ 2 = -1"
and e2_squared [simp]: "e2 ^ 2 = -1"
and e3_squared [simp]: "e3 ^ 2 = -1"
and e4_squared [simp]: "e4 ^ 2 = -1"
and e5_squared [simp]: "e5 ^ 2 = -1"
and e6_squared [simp]: "e6 ^ 2 = -1"
and e7_squared [simp]: "e7 ^ 2 = -1"
by (simp_all add: octo_eq_iff power2_eq_square_octo octo_mult_components)

lemma inverse_e1 [simp]: "inverse e1 = -e1"
and inverse_e2 [simp]: "inverse e2 = -e2"
and inverse_e3 [simp]: "inverse e3 = -e3"
and inverse_e4 [simp]: "inverse e4 = -e4"
and inverse_e5 [simp]: "inverse e5 = -e5"
and inverse_e6 [simp]: "inverse e6 = -e6"
and inverse_e7 [simp]: "inverse e7 = -e7"

subsection ‹Conjugate of an octonion and related properties.›

primcorec cnj :: "octo ⇒ octo"
where
"Ree (cnj z) = Ree z"
| "Im1 (cnj z) = - Im1 z"
| "Im2 (cnj z) = - Im2 z"
| "Im3 (cnj z) = - Im3 z"
| "Im4 (cnj z) = - Im4 z"
| "Im5 (cnj z) = - Im5 z"
| "Im6 (cnj z) = - Im6 z"
| "Im7 (cnj z) = - Im7 z"

lemma cnj_cancel_iff [simp]: "cnj x = cnj y ⟷ x = y"

proof
show "cnj x = cnj y ⟹ x = y"
qed auto

lemma cnj_cnj [simp]:
"cnj(cnj q) = q"

lemma cnj_of_real [simp]: "cnj(octo_of_real x) = octo_of_real x"
using  octo_eq_iff

lemma cnj_zero [simp]: "cnj 0 = 0"

lemma cnj_zero_iff [iff]: "cnj z = 0 ⟷ z = 0"
using cnj_cnj   by (metis cnj_zero)

lemma cnj_one [simp]: "cnj 1 = 1"

lemma cnj_one_iff [simp]: "cnj z = 1 ⟷ z = 1"

lemma octo_norm_cnj [simp]: "norm(cnj q) = norm q"

lemma cnj_add [simp]: "cnj (x + y) = cnj x + cnj y"
using  octo_eq_iff inner_real_def of_real_0 of_real_inner_1  by simp

lemma cnj_sum [simp]: "cnj (sum f S) = (∑x∈S. cnj (f x))"
by (induct S rule: infinite_finite_induct) auto

lemma cnj_diff [simp]: "cnj (x - y) = cnj x - cnj y"
using  octo_eq_iff

lemma cnj_minus [simp]: "cnj (- x) = - cnj x"
using  octo_eq_iff  cnj_cnj by auto

lemma cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)" for x y ::octo
using  octo_eq_iff inner_real_def real_inner_1_right  by auto

lemma cnj_mult [simp]: "cnj (x * y) = cnj y * cnj x" for x y ::octo
using octo_eq_iff  times_octo_def octo_mult_components cnj_cnj
mult_not_zero nonzero_inverse_mult_distrib  by simp

lemma cnj_divide [simp]: "cnj (x / y) = (inverse (cnj y) ) *  cnj x"
for x y ::octo
unfolding  divide_octo_def times_octo_def
using cnj_inverse cnj_mult octo_mult_components  by (metis times_octo_def)

lemma cnj_power [simp]: "cnj (x ^ y) = (cnj x) ^ y"  for x::octo
by (induction y) (simp_all add: octo_power_commutes)

lemma cnj_of_nat [simp]: "cnj (octo_of_nat x) = octo_of_nat( x)"
using cnj_of_real octo_of_real_of_nat_eq by metis

lemma cnj_of_int [simp]: "cnj (octo_of_int x) = octo_of_nat( x)"
using  octo_of_real_def  octo_of_real_of_int_eq  octo_of_int_def octo_of_nat_def
cnj_of_real by auto

lemma cnj_numeral [simp]: "cnj (numeral x) = numeral x"

lemma cnj_neg_numeral [simp]: "cnj (- numeral x) = - numeral x"

lemma cnj_scaleR [simp]: "cnj (scaleR r x) = scaleR r (cnj x)"
using octo_eq_iff inner_real_def ln_one of_real_inner_1 by simp

lemma cnj_units [simp]: "cnj e1 = -e1" "cnj e2 = -e2" "cnj e3 = -e3"
"cnj e4 = -e4"   "cnj e5 = -e5"   "cnj e6 = -e6"  "cnj e7 = -e7"

lemma cnj_eq_of_real: "cnj q = octo_of_real x ⟷ q = octo_of_real x"
proof
show "cnj q = octo_of_real x ⟹ q = octo_of_real x"
by (metis cnj_of_real cnj_cnj)
qed auto

lemma octo_trad_cnj : "cnj q = (Ree q) *⇩R e0 - (Im1 q) *⇩R e1 - (Im2 q)*⇩R e2  - (Im3 q) *⇩R e3  -
(Im4 q) *⇩R e4 -  (Im5 q) *⇩R e5 -  (Im6 q) *⇩R e6  -  (Im7 q)*⇩R e7 " for q::octo
using cnj_cnj octo_unfold octo_trad cnj_def Octonions.cnj.code by auto

lemma octonion_conjugate_property:
"cnj x = -(1/6) *⇩R (x + (e1 * x) *  e1  +  (e2 * x) * e2 +  (e3 * x) * e3 +
(e4 * x) * e4 + (e5 * x) * e5 +  ( e6 * x) * e6 + (e7 * x) * e7)"

lemma octo_add_cnj: "q + cnj q = 2 *⇩R (Ree q) *⇩R e0" "cnj q + q = (2*⇩R (Ree q)*⇩R e0)"

lemma octo_add_cnj1: "q + cnj q = octo_of_real (2*⇩R (Ree q))"
"cnj q + q = octo_of_real (2*⇩R (Ree q))"
by (auto simp: octo_eq_iff octo_mult_components)

lemma octo_subtract_cnj:
"q - cnj q = 2 *⇩R (Im1 q *⇩R e1 + Im2 q *⇩R e2 + Im3 q *⇩R e3 +
Im4 q *⇩R e4 + Im5 q *⇩R e5 + Im6 q*⇩R e6 + Im7 q *⇩R e7)"

lemma octo_mult_cnj_commute: "cnj x * x = x * cnj x"
using times_octo_def by auto

lemma octo_cnj_mult_conv_norm: "cnj x * x = octo_of_real (norm x) ^ 2"
by (simp add: octo_eq_iff octo_mult_components norm_octo_def power2_eq_square
flip: octo_of_real_power)

lemma octo_mult_cnj_conv_norm: "x * cnj x = octo_of_real (norm x) ^ 2"
by (simp add: octo_eq_iff octo_mult_components norm_octo_def power2_eq_square
flip: octo_of_real_power)

lemma octo_mult_cnj_conv_norm_aux: "octo_of_real (norm x ^ 2) = x * cnj x "
using octo_mult_cnj_conv_norm[of x] by (simp add: octo_mult_cnj_commute)

lemma octo_norm_conj: "octo_of_real ( inner x y) = (1/2) *⇩R (x * (cnj y) + y * (cnj x))"
by (simp add: octo_eq_iff octo_mult_components inner_octo_def)

lemma octo_inverse_cnj: "inverse x = cnj x /⇩R (norm x ^ 2)"
by (auto simp: octo_eq_iff norm_octo_def field_simps)

lemma inverse_octo_1: "x ≠ 0 ⟹ x * inverse x = (1 :: octo)"
by (simp add: octo_mult_scaleR_right octo_mult_cnj_conv_norm_aux [symmetric]
divide_simps octo_inverse_cnj
del: octo_of_real_power)

lemma inverse_octo_1_sym: "x ≠ 0 ⟹ inverse x * x = (1 :: octo)"
by (metis cnj_cnj cnj_inverse cnj_mult cnj_one cnj_zero inverse_octo_1)

lemma inverse_0_octo [simp]: "inverse 0 = (0 :: octo)"

lemma inverse_octo_commutes: "inverse x * x = x * (inverse x :: octo)"
by (cases "x = 0") (simp_all add: inverse_octo_1 inverse_octo_1_sym)

lemma octo_inverse_mult: "inverse (x * y) = inverse y * inverse x" for x y::octo
proof-
have "inverse (x * y) = (cnj y * cnj x) /⇩R (norm (x * y) ^ 2)"
also have "… = (cnj y /⇩R norm y ^ 2) * (cnj x /⇩R norm x ^ 2)"
by (simp add: octo_mult_scaleR_left octo_mult_scaleR_right multiplicative_norm_octo
power2_eq_square)
also have "… = inverse y * inverse x"
finally show ?thesis .
qed

lemma octo_inverse_eq_cnj: "norm q = 1 ⟹ inverse q = cnj q" for q::octo

lemma octo_in_Reals_if_Re: fixes q ::real shows " Ree( octo_of_real(q)) = q"
by simp

lemma octo_in_Reals_if_Re_con: assumes "Ree (octo_of_real q) = q"
shows "q ∈ Reals"
by (metis Reals_of_real inner_real_def mult.right_neutral of_real_inner_1)

lemma octo_in_Reals_if_cnj: fixes q:: real shows " cnj( octo_of_real( q)) = octo_of_real q"
by simp

lemma octo_in_Reals_if_cnj_con: assumes " cnj( octo_of_real( q)) = octo_of_real q"
shows "q ∈ Reals "
by (metis Reals_of_real inner_real_def mult.right_neutral of_real_inner_1)

lemma norm_power2: "norm q ^ 2 = Ree (cnj q * q)"
by (simp add: octo_mult_components norm_octo_def power2_eq_square)

lemma norm_power2_cnj: "norm q ^ 2 = Ree (q * cnj q)"
by (simp add: octo_mult_components norm_octo_def power2_eq_square)

lemma octo_norm_imaginary: "Ree x = 0 ⟹ x * x = -(octo_of_real (norm x))⇧2"
by (simp add: octo_eq_iff octo_mult_components norm_octo_def power2_eq_square
flip: octo_of_real_power octo_of_real_mult)

subsection‹ Linearity and continuity of the components.›

lemma bounded_linear_Ree: "bounded_linear Ree"
and bounded_linear_Im1: "bounded_linear Im1"
and bounded_linear_Im2: "bounded_linear Im2"
and bounded_linear_Im3: "bounded_linear Im3"
and bounded_linear_Im4: "bounded_linear Im4"
and bounded_linear_Im5: "bounded_linear Im5"
and bounded_linear_Im6: "bounded_linear Im6"
and bounded_linear_Im7: "bounded_linear Im7"

lemmas Cauchy_Ree = bounded_linear.Cauchy [OF bounded_linear_Ree]
lemmas Cauchy_Im1 = bounded_linear.Cauchy [OF bounded_linear_Im1]
lemmas Cauchy_Im2 = bounded_linear.Cauchy [OF bounded_linear_Im2]
lemmas Cauchy_Im3 = bounded_linear.Cauchy [OF bounded_linear_Im3]
lemmas Cauchy_Im4 = bounded_linear.Cauchy [OF bounded_linear_Im4]
lemmas Cauchy_Im5 = bounded_linear.Cauchy [OF bounded_linear_Im5]
lemmas Cauchy_Im6 = bounded_linear.Cauchy [OF bounded_linear_Im6]
lemmas Cauchy_Im7 = bounded_linear.Cauchy [OF bounded_linear_Im7]

lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Ree]
lemmas tendsto_Im1 [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im1]
lemmas tendsto_Im2 [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im2]
lemmas tendsto_Im3 [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im3]
lemmas tendsto_Im4 [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im4]
lemmas tendsto_Im5 [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im5]
lemmas tendsto_Im6 [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im6]
lemmas tendsto_Im7 [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im7]

lemmas isCont_Ree [simp] = bounded_linear.isCont [OF bounded_linear_Ree]
lemmas isCont_Im1 [simp] = bounded_linear.isCont [OF bounded_linear_Im1]
lemmas isCont_Im2 [simp] = bounded_linear.isCont [OF bounded_linear_Im2]
lemmas isCont_Im3 [simp] = bounded_linear.isCont [OF bounded_linear_Im3]
lemmas isCont_Im4 [simp] = bounded_linear.isCont [OF bounded_linear_Im4]
lemmas isCont_Im5 [simp] = bounded_linear.isCont [OF bounded_linear_Im5]
lemmas isCont_Im6 [simp] = bounded_linear.isCont [OF bounded_linear_Im6]
lemmas isCont_Im7 [simp] = bounded_linear.isCont [OF bounded_linear_Im7]

lemmas continuous_Ree [simp] = bounded_linear.continuous [OF bounded_linear_Ree]
lemmas continuous_Im1 [simp] = bounded_linear.continuous [OF bounded_linear_Im1]
lemmas continuous_Im2 [simp] = bounded_linear.continuous [OF bounded_linear_Im2]
lemmas continuous_Im3 [simp] = bounded_linear.continuous [OF bounded_linear_Im3]
lemmas continuous_Im4 [simp] = bounded_linear.continuous [OF bounded_linear_Im4]
lemmas continuous_Im5 [simp] = bounded_linear.continuous [OF bounded_linear_Im5]
lemmas continuous_Im6 [simp] = bounded_linear.continuous [OF bounded_linear_Im6]
lemmas continuous_Im7 [simp] = bounded_linear.continuous [OF bounded_linear_Im7]

lemmas continuous_on_Ree [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Ree]
lemmas continuous_on_Im1 [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im1]
lemmas continuous_on_Im2 [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im2]
lemmas continuous_on_Im3 [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im3]
lemmas continuous_on_Im4 [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im4]
lemmas continuous_on_Im5 [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im5]
lemmas continuous_on_Im6 [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im6]
lemmas continuous_on_Im7 [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im7]

lemmas has_derivative_Ree [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Ree]
lemmas has_derivative_Im1 [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im1]
lemmas has_derivative_Im2 [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im2]
lemmas has_derivative_Im3 [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im3]
lemmas has_derivative_Im4 [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im4]
lemmas has_derivative_Im5 [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im5]
lemmas has_derivative_Im6 [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im6]
lemmas has_derivative_Im7 [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im7]

lemmas sums_Ree = bounded_linear.sums [OF bounded_linear_Ree]
lemmas sums_Im1 = bounded_linear.sums [OF bounded_linear_Im1]
lemmas sums_Im2 = bounded_linear.sums [OF bounded_linear_Im2]
lemmas sums_Im3 = bounded_linear.sums [OF bounded_linear_Im3]
lemmas sums_Im4 = bounded_linear.sums [OF bounded_linear_Im4]
lemmas sums_Im5 = bounded_linear.sums [OF bounded_linear_Im5]
lemmas sums_Im6 = bounded_linear.sums [OF bounded_linear_Im6]
lemmas sums_Im7 = bounded_linear.sums [OF bounded_linear_Im7]

subsubsection‹ Octonionic-specific theorems about sums.                                ›

lemma Ree_sum [simp]: "Ree (sum f S) = sum (λx.  Ree(f x)) S"
and Im1_sum [simp]: "Im1 (sum f S) = sum (λx. Im1 (f x)) S"
and Im2_sum [simp]: "Im2 (sum f S) = sum (λx. Im2 (f x)) S"
and Im3_sum [simp]: "Im3 (sum f S) = sum (λx. Im3 (f x)) S"
and Im4_sum [simp]: "Im4 (sum f S) = sum (λx. Im4 (f x)) S"
and Im5_sum [simp]: "Im5 (sum f S) = sum (λx. Im5 (f x)) S"
and Im6_sum [simp]: "Im6 (sum f S) = sum (λx. Im6 (f x)) S"
and Im7_sum [simp]: "Im7 (sum f S) = sum (λx. Im7 (f x)) S"
by (induct S rule: infinite_finite_induct; simp)+

subsubsection‹ Bound results for real and imaginary components of limits.                ›

lemma Ree_tendsto_upperbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. octo.Ree (f x) ≤ b; net ≠ bot⟧ ⟹ Ree limit ≤ b"
by (blast intro: tendsto_upperbound [OF tendsto_Re])

lemma Im1_tendsto_upperbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. Im1 (f x) ≤ b; net ≠ bot⟧ ⟹ Im1 limit ≤ b"
by (blast intro: tendsto_upperbound [OF tendsto_Im1])

lemma Im2_tendsto_upperbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. Im2 (f x) ≤ b; net ≠ bot⟧ ⟹ Im2 limit ≤ b"
by (blast intro: tendsto_upperbound [OF tendsto_Im2])

lemma Im3_tendsto_upperbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. Im3 (f x) ≤ b; net ≠ bot⟧ ⟹ Im3 limit ≤ b"
by (blast intro: tendsto_upperbound [OF tendsto_Im3])

lemma Im4_tendsto_upperbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. Im4 (f x) ≤ b; net ≠ bot⟧ ⟹ Im4 limit ≤ b"
by (blast intro: tendsto_upperbound [OF tendsto_Im4])

lemma Im5_tendsto_upperbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. Im5 (f x) ≤ b; net ≠ bot⟧ ⟹ Im5 limit ≤ b"
by (blast intro: tendsto_upperbound [OF tendsto_Im5])

lemma Im6_tendsto_upperbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. Im6 (f x) ≤ b; net ≠ bot⟧ ⟹ Im6 limit ≤ b"
by (blast intro: tendsto_upperbound [OF tendsto_Im6])

lemma Im7_tendsto_upperbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. Im7 (f x) ≤ b; net ≠ bot⟧ ⟹ Im7 limit ≤ b"
by (blast intro: tendsto_upperbound [OF tendsto_Im7])

lemma Ree_tendsto_lowerbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. b ≤ octo.Ree (f x); net ≠ bot⟧ ⟹ b ≤ Ree limit"
by (blast intro: tendsto_lowerbound [OF tendsto_Re])

lemma Im1_tendsto_lowerbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. b ≤ Im1 (f x); net ≠ bot⟧ ⟹ b ≤ Im1 limit"
by (blast intro: tendsto_lowerbound [OF tendsto_Im1])

lemma Im2_tendsto_lowerbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. b ≤ Im2 (f x); net ≠ bot⟧ ⟹ b ≤ Im2 limit"
by (blast intro: tendsto_lowerbound [OF tendsto_Im2])

lemma Im3_tendsto_lowerbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. b ≤ Im3 (f x); net ≠ bot⟧ ⟹ b ≤ Im3 limit"
by (blast intro: tendsto_lowerbound [OF tendsto_Im3])

lemma Im4_tendsto_lowerbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. b ≤ Im4 (f x); net ≠ bot⟧ ⟹ b ≤ Im4 limit"
by (blast intro: tendsto_lowerbound [OF tendsto_Im4])

lemma Im5_tendsto_lowerbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. b ≤ Im5 (f x); net ≠ bot⟧ ⟹ b ≤ Im5 limit"
by (blast intro: tendsto_lowerbound [OF tendsto_Im5])

lemma Im6_tendsto_lowerbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. b ≤ Im6 (f x); net ≠ bot⟧ ⟹ b ≤ Im6 limit"
by (blast intro: tendsto_lowerbound [OF tendsto_Im6])

lemma Im7_tendsto_lowerbound:
"⟦(f ⤏ limit) net; ∀⇩F x in net. b ≤ Im7 (f x); net ≠ bot⟧ ⟹ b ≤ Im7 limit"
by (blast intro: tendsto_lowerbound [OF tendsto_Im7])

lemma octo_of_real_continuous [continuous_intros]:
"continuous net f ⟹ continuous net (λx. octo_of_real (f x))"
by (auto simp: octo_of_real_def intro: continuous_intros)

lemma octo_of_real_continuous_on [continuous_intros]:
"continuous_on S f ⟹ continuous_on S (λx. octo_of_real (f x))"
by (auto simp: octo_of_real_def intro: continuous_intros)

lemma of_real_continuous_iff: "continuous net (λx. octo_of_real (f x)) ⟷ continuous net f"
proof safe
assume "continuous net (λx. octo_of_real (f x))"
hence "continuous net (λx. Ree (octo_of_real (f x)))"
by (rule continuous_Ree)
thus "continuous net f" by simp
qed (auto intro: continuous_intros)

lemma of_real_continuous_on_iff:
"continuous_on S (λx. octo_of_real(f x)) ⟷ continuous_on S f"
proof safe
assume "continuous_on S (λx. octo_of_real (f x))"
hence "continuous_on S (λx. Ree (octo_of_real (f x)))"
by (rule continuous_on_Ree)
thus "continuous_on S f" by simp
qed (auto intro: continuous_intros)

subsection‹Octonions for describing 7D isometries›

subsubsection‹The ‹HIm› operator›

definition HIm :: "octo ⇒ real^7" where
"HIm q ≡ vector[Im1 q, Im2 q, Im3 q, Im4 q, Im5 q, Im6 q, Im7 q]"

lemma HIm_Octo: "HIm (Octo w x y z u v q g) = vector[x,y,z, u, v, q, g]"

lemma him_eq: "HIm a = HIm b ⟷ Im1 a = Im1 b ∧ Im2 a = Im2 b ∧ Im3 a = Im3 b
∧ Im4 a = Im4 b ∧ Im5 a = Im5 b ∧ Im6 a = Im6 b ∧ Im7 a = Im7 b"

by (metis HIm_def vector_7)

lemma him_of_real [simp]: "HIm(octo_of_real a) = 0"
by (simp add:octo_of_real_eq_Octo HIm_Octo vec_eq_iff vector_def)

lemma him_0 [simp]: "HIm 0 = 0"
by (metis him_of_real octo_of_real_0)

lemma him_1 [simp]: "HIm 1 = 0"
using HIm_def him_0 by auto

lemma him_cnj: "HIm(cnj q) = - HIm q"
by (simp add: HIm_def vec_eq_iff vector_def)

lemma him_mult_left [simp]: "HIm (a *⇩R q) = a  *⇩R HIm q"
by (simp add: HIm_def vec_eq_iff vector_def)

lemma him_mult_right [simp]: "HIm (q * octo_of_real a) = HIm q * of_real a"
by (metis Octonions.scaleR_conv_octo_of_real Real_Vector_Spaces.scaleR_conv_of_real
him_mult_left octo_of_real_times_commute semiring_normalization_rules(7))

lemma him_add [simp]: "HIm (x + y) = HIm x + HIm y"
and  him_minus [simp]: "HIm (-x) = - HIm x"
and  him_diff [simp]: "HIm (x - y) = HIm x - HIm y"
by (simp_all add: HIm_def vec_eq_iff vector_def)

lemma him_sum [simp]: "HIm (sum f S) = (∑x∈S. HIm (f x))"
by (induct S rule: infinite_finite_induct) auto

lemma linear_him: "linear HIm"

subsubsection‹The ‹Hv› operator›

definition Hv :: "real^7 ⇒ octo" where
"Hv v ≡ Octo 0 (v\$1) (v\$2) (v\$3) (v\$4) (v\$5) (v\$6) (v\$7)  "

lemma Hv_sel [simp]:
"Ree (Hv v) = 0" "Im1 (Hv v) = v \$ 1" "Im2 (Hv v) = v \$ 2" "Im3 (Hv v) = v \$ 3"
"Im4 (Hv v) = v \$ 4" "Im5 (Hv v) = v \$ 5" "Im6 (Hv v) = v \$ 6" "Im7 (Hv v) = v \$ 7"

lemma hv_vec: "Hv(vec r) = Octo 0 r r r r r r r "

lemma hv_eq_zero [simp]: "Hv v = 0 ⟷ v = 0"
by (simp add: octo_eq_iff vec_eq_iff) (metis exhaust_7)

lemma hv_zero [simp]: "Hv 0 = 0"
by simp

lemma hv_vector [simp]: "Hv(vector[x,y,z,u,v,q,g]) = Octo 0 x y z u v q g"

lemma hv_basis:
"Hv(axis 1 1) = e1" "Hv(axis 2 1) = e2" "Hv(axis 3 1) = e3"
"Hv(axis 4 1) = e4" "Hv(axis 5 1) = e5" "Hv(axis 6 1) = e6"  "Hv(axis 7 1) = e7"

lemma hv_add [simp]: "Hv(x + y) = Hv x + Hv y"

lemma hv_minus [simp]: "Hv(-x) = -Hv x"

lemma hv_diff [simp]: "Hv(x - y) = Hv x - Hv y"

lemma hv_cmult [simp]:
"Hv(scaleR a   x) = scaleR a  ( Hv x)"

lemma hv_sum [simp]: "Hv (sum f S) = (∑x∈S. Hv (f x))"
by (induct S rule: infinite_finite_induct) auto

lemma hv_inj: "Hv x = Hv y ⟷ x = y"
by (simp add: Hv_def octo_eq_iff vec_eq_iff) (metis (full_types) exhaust_7)

lemma linear_hv: "linear Hv"
using octo_of_real_def by (simp add: linearI)

lemma him_hv [simp]: "HIm(Hv x) = x"
using HIm_def hv_inj octo_eq_iff by fastforce

lemma cnj_hv [simp]: "cnj(Hv v) = -Hv v"

lemma hv_him: "Hv(HIm q) = Octo 0 (Im1 q) (Im2 q) (Im3 q)  (Im4 q) (Im5 q) (Im6 q)  (Im7 q)  "

lemma hv_him_eq: "Hv(HIm q) = q ⟷ Ree q = 0"

lemma dot_hv [simp]: "Hv u ∙ Hv v = u ∙ v"
by (simp add: Hv_def inner_octo_def inner_vec_def sum_7)

lemma norm_hv [simp]: "norm (Hv v) = norm v"

subsubsection‹Related basic identities ›

lemma mult_hv_eq_cross_dot: "Hv x * Hv y = Hv(x  ×⇩7 y) - octo_of_real (inner x y)"
by (simp add: octo_eq_iff inner_octo_def cross7_components octo_mult_components
inner_vec_def sum_7)

lemma octonion_identity1_cross7 :
"Hv (x ×⇩7 y) = (1/2) *⇩R (Hv x * Hv y - Hv y * Hv x)"
by (simp add: octo_eq_iff octo_mult_components cross7_components)

lemma octonion_identity2_cross7:
"Hv (x ×⇩7 (y ×⇩7 z) + y ×⇩7 (z ×⇩7 x) + z ×⇩7 (x ×⇩7 y)) =
-(3/2) *⇩R ((Hv x * Hv y) * Hv z - Hv x * (Hv y * Hv z))"
unfolding ```