Theory Homogeneous_Coordinates
section ‹Homogeneous coordinates in extended complex plane›
text ‹Extended complex plane $\mathbb{\overline{C}}$ is complex plane with an additional element
(treated as the infinite point). The extended complex plane $\mathbb{\overline{C}}$ is identified
with a complex projective line (the one-dimensional projective space over the complex field, sometimes denoted by $\mathbb{C}P^1$).
Each point of $\mathbb{\overline{C}}$ is represented by a pair of complex homogeneous coordinates (not
both equal to zero), and two pairs of homogeneous coordinates represent the same
point in $\mathbb{\overline{C}}$ iff they are proportional by a non-zero complex factor.›
theory Homogeneous_Coordinates
imports More_Complex Matrices
begin
subsection ‹Definition of homogeneous coordinates›
text ‹Two complex vectors are equivalent iff they are proportional.›
definition complex_cvec_eq :: "complex_vec ⇒ complex_vec ⇒ bool" (infix ‹≈⇩v› 50) where
[simp]: "z1 ≈⇩v z2 ⟷ (∃ k. k ≠ (0::complex) ∧ z2 = k *⇩s⇩v z1)"
lemma complex_cvec_eq_mix:
assumes "(z1, z2) ≠ vec_zero" and "(w1, w2) ≠ vec_zero"
shows "(z1, z2) ≈⇩v (w1, w2) ⟷ z1*w2 = z2*w1"
proof safe
assume "(z1, z2) ≈⇩v (w1, w2)"
thus "z1 * w2 = z2 * w1"
by auto
next
assume *: "z1 * w2 = z2 * w1"
show "(z1, z2) ≈⇩v (w1, w2)"
proof (cases "z2 = 0")
case True
thus ?thesis
using * assms
by auto
next
case False
hence "w1 = (w2/z2)*z1 ∧ w2 = (w2/z2)*z2" "w2/z2 ≠ 0"
using * assms
by (auto simp add: field_simps)
thus "(z1, z2) ≈⇩v (w1, w2)"
by (metis complex_cvec_eq_def mult_sv.simps)
qed
qed
lemma complex_eq_cvec_reflp [simp]:
shows "reflp (≈⇩v)"
unfolding reflp_def complex_cvec_eq_def
by safe (rule_tac x="1" in exI, simp)
lemma complex_eq_cvec_symp [simp]:
shows "symp (≈⇩v)"
unfolding symp_def complex_cvec_eq_def
by safe (rule_tac x="1/k" in exI, simp)
lemma complex_eq_cvec_transp [simp]:
shows "transp (≈⇩v)"
unfolding transp_def complex_cvec_eq_def
by safe (rule_tac x="k*ka" in exI, simp)
lemma complex_eq_cvec_equivp [simp]:
shows "equivp (≈⇩v)"
by (auto intro: equivpI)
text ‹Non-zero pairs of complex numbers (also treated as non-zero complex vectors)›
typedef complex_homo_coords = "{v::complex_vec. v ≠ vec_zero}"
by (rule_tac x="(1, 0)" in exI, simp)
setup_lifting type_definition_complex_homo_coords
lift_definition complex_homo_coords_eq :: "complex_homo_coords ⇒ complex_homo_coords ⇒ bool" (infix ‹≈› 50) is complex_cvec_eq
done
lemma complex_homo_coords_eq_reflp [simp]:
shows "reflp (≈)"
using complex_eq_cvec_reflp
unfolding reflp_def
by transfer blast
lemma complex_homo_coords_eq_symp [simp]:
shows "symp (≈)"
using complex_eq_cvec_symp
unfolding symp_def
by transfer blast
lemma complex_homo_coords_eq_transp [simp]:
shows "transp (≈)"
using complex_eq_cvec_transp
unfolding transp_def
by transfer blast
lemma complex_homo_coords_eq_equivp:
shows "equivp (≈)"
by (auto intro: equivpI)
lemma complex_homo_coords_eq_refl [simp]:
shows "z ≈ z"
using complex_homo_coords_eq_reflp
unfolding reflp_def refl_on_def
by blast
lemma complex_homo_coords_eq_sym:
assumes "z1 ≈ z2"
shows "z2 ≈ z1"
using assms complex_homo_coords_eq_symp
unfolding symp_def
by blast
lemma complex_homo_coords_eq_trans:
assumes "z1 ≈ z2" and "z2 ≈ z3"
shows "z1 ≈ z3"
using assms complex_homo_coords_eq_transp
unfolding transp_def
by blast
text ‹Quotient type of homogeneous coordinates›
quotient_type
complex_homo = complex_homo_coords / "complex_homo_coords_eq"
by (rule complex_homo_coords_eq_equivp)
subsection ‹Some characteristic points in $\mathbb{C}P^1$›
text ‹Infinite point›
definition inf_cvec :: "complex_vec" (‹∞⇩v›) where
[simp]: "inf_cvec = (1, 0)"
lift_definition inf_hcoords :: "complex_homo_coords" (‹∞⇩h⇩c›) is inf_cvec
by simp
lift_definition inf :: "complex_homo" (‹∞⇩h›) is inf_hcoords
done
lemma inf_cvec_z2_zero_iff:
assumes "(z1, z2) ≠ vec_zero"
shows "(z1, z2) ≈⇩v ∞⇩v ⟷ z2 = 0"
using assms
by auto
text ‹Zero›
definition zero_cvec :: "complex_vec" (‹0⇩v›) where
[simp]: "zero_cvec = (0, 1)"
lift_definition zero_hcoords :: "complex_homo_coords" (‹0⇩h⇩c›) is zero_cvec
by simp
lift_definition zero :: "complex_homo" (‹0⇩h›) is zero_hcoords
done
lemma zero_cvec_z1_zero_iff:
assumes "(z1, z2) ≠ vec_zero"
shows "(z1, z2) ≈⇩v 0⇩v ⟷ z1 = 0"
using assms
by auto
text ‹One›
definition one_cvec :: "complex_vec" (‹1⇩v›)where
[simp]: "one_cvec = (1, 1)"
lift_definition one_hcoords :: "complex_homo_coords" (‹1⇩h⇩c›) is one_cvec
by simp
lift_definition one :: "complex_homo" (‹1⇩h›) is one_hcoords
done
lemma zero_one_infty_not_equal [simp]:
shows "1⇩h ≠ ∞⇩h" and "0⇩h ≠ ∞⇩h" and "0⇩h ≠ 1⇩h" and "1⇩h ≠ 0⇩h" and "∞⇩h ≠ 0⇩h" and "∞⇩h ≠ 1⇩h"
by (transfer, transfer, simp)+
text ‹Imaginary unit›
definition ii_cvec :: "complex_vec" (‹ii⇩v›) where
[simp]: "ii_cvec = (𝗂, 1)"
lift_definition ii_hcoords :: "complex_homo_coords" (‹ii⇩h⇩c›) is ii_cvec
by simp
lift_definition ii :: "complex_homo" (‹ii⇩h›) is ii_hcoords
done
lemma ex_3_different_points:
fixes z::complex_homo
shows "∃ z1 z2. z ≠ z1 ∧ z1 ≠ z2 ∧ z ≠ z2"
proof (cases "z ≠ 0⇩h ∧ z ≠ 1⇩h")
case True
thus ?thesis
by (rule_tac x="0⇩h" in exI, rule_tac x="1⇩h" in exI, auto)
next
case False
hence "z = 0⇩h ∨ z = 1⇩h"
by simp
thus ?thesis
proof
assume "z = 0⇩h"
thus ?thesis
by (rule_tac x="∞⇩h" in exI, rule_tac x="1⇩h" in exI, auto)
next
assume "z = 1⇩h"
thus ?thesis
by (rule_tac x="∞⇩h" in exI, rule_tac x="0⇩h" in exI, auto)
qed
qed
subsection ‹Connection to ordinary complex plane $\mathbb{C}$›
text ‹Conversion from complex›
definition of_complex_cvec :: "complex ⇒ complex_vec" where
[simp]: "of_complex_cvec z = (z, 1)"
lift_definition of_complex_hcoords :: "complex ⇒ complex_homo_coords" is of_complex_cvec
by simp
lift_definition of_complex :: "complex ⇒ complex_homo" is of_complex_hcoords
done
lemma of_complex_inj:
assumes "of_complex x = of_complex y"
shows "x = y"
using assms
by (transfer, transfer, simp)
lemma of_complex_image_inj:
assumes "of_complex ` A = of_complex ` B"
shows "A = B"
using assms
using of_complex_inj
by auto
lemma of_complex_not_inf [simp]:
shows "of_complex x ≠ ∞⇩h"
by (transfer, transfer, simp)
lemma inf_not_of_complex [simp]:
shows "∞⇩h ≠ of_complex x"
by (transfer, transfer, simp)
lemma inf_or_of_complex:
shows "z = ∞⇩h ∨ (∃ x. z = of_complex x)"
proof (transfer, transfer)
fix z :: complex_vec
obtain z1 z2 where *: "z = (z1, z2)"
by (cases z) auto
assume "z ≠ vec_zero"
thus "z ≈⇩v ∞⇩v ∨ (∃x. z ≈⇩v of_complex_cvec x)"
using *
by (cases "z2 = 0", auto)
qed
lemma of_complex_zero [simp]:
shows "of_complex 0 = 0⇩h"
by (transfer, transfer, simp)
lemma of_complex_one [simp]:
shows "of_complex 1 = 1⇩h"
by (transfer, transfer, simp)
lemma of_complex_ii [simp]:
shows "of_complex 𝗂 = ii⇩h"
by (transfer, transfer, simp)
lemma of_complex_zero_iff [simp]:
shows "of_complex x = 0⇩h ⟷ x = 0"
by (subst of_complex_zero[symmetric]) (auto simp add: of_complex_inj)
lemma of_complex_one_iff [simp]:
shows "of_complex x = 1⇩h ⟷ x = 1"
by (subst of_complex_one[symmetric]) (auto simp add: of_complex_inj)
lemma of_complex_ii_iff [simp]:
shows "of_complex x = ii⇩h ⟷ x = 𝗂"
by (subst of_complex_ii[symmetric]) (auto simp add: of_complex_inj)
text ‹Conversion to complex›
definition to_complex_cvec :: "complex_vec ⇒ complex" where
[simp]: "to_complex_cvec z = (let (z1, z2) = z in z1/z2)"
lift_definition to_complex_homo_coords :: "complex_homo_coords ⇒ complex" is to_complex_cvec
done
lift_definition to_complex :: "complex_homo ⇒ complex" is to_complex_homo_coords
proof-
fix z w
assume "z ≈ w"
thus "to_complex_homo_coords z = to_complex_homo_coords w"
by transfer auto
qed
lemma to_complex_of_complex [simp]:
shows "to_complex (of_complex z) = z"
by (transfer, transfer, simp)
lemma of_complex_to_complex [simp]:
assumes "z ≠ ∞⇩h"
shows "(of_complex (to_complex z)) = z"
using assms
proof (transfer, transfer)
fix z :: complex_vec
obtain z1 z2 where *: "z = (z1, z2)"
by (cases z, auto)
assume "z ≠ vec_zero" "¬ z ≈⇩v ∞⇩v"
hence "z2 ≠ 0"
using *
by (simp, erule_tac x="1/z1" in allE, auto)
thus "(of_complex_cvec (to_complex_cvec z)) ≈⇩v z"
using *
by simp
qed
lemma to_complex_zero_zero [simp]:
shows "to_complex 0⇩h = 0"
by (metis of_complex_zero to_complex_of_complex)
lemma to_complex_one_one [simp]:
shows "to_complex 1⇩h = 1"
by (metis of_complex_one to_complex_of_complex)
lemma to_complex_img_one [simp]:
shows "to_complex ii⇩h = 𝗂"
by (metis of_complex_ii to_complex_of_complex)
subsection ‹Arithmetic operations›
text ‹Due to the requirement of HOL that all functions are total, we could not define the function
only for the well-defined cases, and in the lifting proofs we must also handle the ill-defined
cases. For example, $\infty_h +_h \infty_h$ is ill-defined, but we must define it, so we define it
arbitrarily to be $\infty_h$.›
subsubsection ‹Addition›
text ‹$\infty_h\ +_h\ \infty_h$ is ill-defined. Since functions must be total, for formal reasons we
define it arbitrarily to be $\infty_h$.›
definition add_cvec :: "complex_vec ⇒ complex_vec ⇒ complex_vec" (infixl ‹+⇩v› 60) where
[simp]: "add_cvec z w = (let (z1, z2) = z; (w1, w2) = w
in if z2 ≠ 0 ∨ w2 ≠ 0 then
(z1*w2 + w1*z2, z2*w2)
else
(1, 0))"
lift_definition add_hcoords :: "complex_homo_coords ⇒ complex_homo_coords ⇒ complex_homo_coords" (infixl ‹+⇩h⇩c› 60) is add_cvec
by (auto split: if_split_asm)
lift_definition add :: "complex_homo ⇒ complex_homo ⇒ complex_homo" (infixl ‹+⇩h› 60) is add_hcoords
proof transfer
fix z w z' w' :: complex_vec
obtain z1 z2 w1 w2 z'1 z'2 w'1 w'2 where
*: "z = (z1, z2)" "w = (w1, w2)" "z' = (z'1, z'2)" "w' = (w'1, w'2)"
by (cases z, auto, cases w, auto, cases z', auto, cases w', auto)
assume **:
"z ≠ vec_zero" "w ≠ vec_zero" "z ≈⇩v z'"
"z' ≠ vec_zero" "w' ≠ vec_zero" "w ≈⇩v w'"
show "z +⇩v w ≈⇩v z' +⇩v w'"
proof (cases "z2 ≠ 0 ∨ w2 ≠ 0")
case True
hence "z'2 ≠ 0 ∨ w'2 ≠ 0"
using * **
by auto
show ?thesis
using ‹z2 ≠ 0 ∨ w2 ≠ 0› ‹z'2 ≠ 0 ∨ w'2 ≠ 0›
using * **
by simp ((erule exE)+, rule_tac x="k*ka" in exI, simp add: field_simps)
next
case False
hence "z'2 = 0 ∨ w'2 = 0"
using * **
by auto
show ?thesis
using ‹¬ (z2 ≠ 0 ∨ w2 ≠ 0)› ‹z'2 = 0 ∨ w'2 = 0›
using * **
by auto
qed
qed
lemma add_commute:
shows "z +⇩h w = w +⇩h z"
apply (transfer, transfer)
unfolding complex_cvec_eq_def
by (rule_tac x="1" in exI, auto split: if_split_asm)
lemma add_zero_right [simp]:
shows "z +⇩h 0⇩h = z"
by (transfer, transfer, force)
lemma add_zero_left [simp]:
shows "0⇩h +⇩h z = z"
by (subst add_commute) simp
lemma of_complex_add_of_complex [simp]:
shows "(of_complex x) +⇩h (of_complex y) = of_complex (x + y)"
by (transfer, transfer, simp)
lemma of_complex_add_inf [simp]:
shows "(of_complex x) +⇩h ∞⇩h = ∞⇩h"
by (transfer, transfer, simp)
lemma inf_add_of_complex [simp]:
shows "∞⇩h +⇩h (of_complex x) = ∞⇩h"
by (subst add_commute) simp
lemma inf_add_right:
assumes "z ≠ ∞⇩h"
shows "z +⇩h ∞⇩h = ∞⇩h"
using assms
using inf_or_of_complex[of z]
by auto
lemma inf_add_left:
assumes "z ≠ ∞⇩h"
shows "∞⇩h +⇩h z = ∞⇩h"
using assms
by (subst add_commute) (rule inf_add_right, simp)
text ‹This is ill-defined, but holds by our definition›
lemma inf_add_inf:
shows "∞⇩h +⇩h ∞⇩h = ∞⇩h"
by (transfer, transfer, simp)
subsubsection ‹Unary minus›
definition uminus_cvec :: "complex_vec ⇒ complex_vec" (‹~⇩v›) where
[simp]: "~⇩v z = (let (z1, z2) = z in (-z1, z2))"
lift_definition uminus_hcoords :: "complex_homo_coords ⇒ complex_homo_coords" (‹~⇩h⇩c›) is uminus_cvec
by auto
lift_definition uminus :: "complex_homo ⇒ complex_homo" (‹~⇩h›) is uminus_hcoords
by transfer auto
lemma uminus_of_complex [simp]:
shows "~⇩h (of_complex z) = of_complex (-z)"
by (transfer, transfer, simp)
lemma uminus_zero [simp]:
shows "~⇩h 0⇩h = 0⇩h"
by (transfer, transfer, simp)
lemma uminus_inf [simp]:
shows "~⇩h ∞⇩h = ∞⇩h"
apply (transfer, transfer)
unfolding complex_cvec_eq_def
by (rule_tac x="-1" in exI, simp)
lemma uminus_inf_iff:
shows "~⇩h z = ∞⇩h ⟷ z = ∞⇩h"
apply (transfer, transfer)
by auto (rule_tac x="-1/a" in exI, auto)
lemma uminus_id_iff:
shows "~⇩h z = z ⟷ z = 0⇩h ∨ z = ∞⇩h"
apply (transfer, transfer)
apply auto
apply (erule_tac x="1/a" in allE, simp)
apply (rule_tac x="-1" in exI, simp)
done
subsubsection ‹Subtraction›
text ‹Operation $\infty_h\ -_h\ \infty_h$ is ill-defined, but we define it arbitrarily to $0_h$. It breaks the connection between
subtraction with addition and unary minus, but seems more intuitive.›
definition sub :: "complex_homo ⇒ complex_homo ⇒ complex_homo" (infixl ‹-⇩h› 60) where
"z -⇩h w = (if z = ∞⇩h ∧ w = ∞⇩h then 0⇩h else z +⇩h (~⇩h w))"
lemma of_complex_sub_of_complex [simp]:
shows "(of_complex x) -⇩h (of_complex y) = of_complex (x - y)"
unfolding sub_def
by simp
lemma zero_sub_right[simp]:
shows "z -⇩h 0⇩h = z"
unfolding sub_def
by simp
lemma zero_sub_left[simp]:
shows "0⇩h -⇩h of_complex x = of_complex (-x)"
by (subst of_complex_zero[symmetric], simp del: of_complex_zero)
lemma zero_sub_one[simp]:
shows "0⇩h -⇩h 1⇩h = of_complex (-1)"
by (metis of_complex_one zero_sub_left)
lemma of_complex_sub_one [simp]:
shows "of_complex x -⇩h 1⇩h = of_complex (x - 1)"
by (metis of_complex_one of_complex_sub_of_complex)
lemma sub_eq_zero [simp]:
assumes "z ≠ ∞⇩h"
shows "z -⇩h z = 0⇩h"
using assms
using inf_or_of_complex[of z]
by auto
lemma sub_eq_zero_iff:
assumes "z ≠ ∞⇩h ∨ w ≠ ∞⇩h"
shows "z -⇩h w = 0⇩h ⟷ z = w"
proof
assume "z -⇩h w = 0⇩h"
thus "z = w"
using assms
unfolding sub_def
proof (transfer, transfer)
fix z w :: complex_vec
obtain z1 z2 w1 w2 where *: "z = (z1, z2)" "w = (w1, w2)"
by (cases z, auto, cases w, auto)
assume "z ≠ vec_zero" "w ≠ vec_zero" "¬ z ≈⇩v ∞⇩v ∨ ¬ w ≈⇩v ∞⇩v" and
**: "(if z ≈⇩v ∞⇩v ∧ w ≈⇩v ∞⇩v then 0⇩v else z +⇩v ~⇩v w) ≈⇩v 0⇩v"
have "z2 ≠ 0 ∨ w2 ≠ 0"
using * ‹¬ z ≈⇩v ∞⇩v ∨ ¬ w ≈⇩v ∞⇩v› ‹z ≠ vec_zero› ‹w ≠ vec_zero›
apply auto
apply (erule_tac x="1/z1" in allE, simp)
apply (erule_tac x="1/w1" in allE, simp)
done
thus "z ≈⇩v w"
using * **
by simp (rule_tac x="w2/z2" in exI, auto simp add: field_simps)
qed
next
assume "z = w"
thus "z -⇩h w = 0⇩h"
using sub_eq_zero[of z] assms
by auto
qed
lemma inf_sub_left [simp]:
assumes "z ≠ ∞⇩h"
shows "∞⇩h -⇩h z = ∞⇩h"
using assms
using uminus_inf_iff
using inf_or_of_complex
unfolding sub_def
by force
lemma inf_sub_right [simp]:
assumes "z ≠ ∞⇩h"
shows "z -⇩h ∞⇩h = ∞⇩h"
using assms
using inf_or_of_complex
unfolding sub_def
by force
text ‹This is ill-defined, but holds by our definition›
lemma inf_sub_inf:
shows "∞⇩h -⇩h ∞⇩h = 0⇩h"
unfolding sub_def
by simp
lemma sub_noteq_inf:
assumes "z ≠ ∞⇩h" and "w ≠ ∞⇩h"
shows "z -⇩h w ≠ ∞⇩h"
using assms
using inf_or_of_complex[of z]
using inf_or_of_complex[of w]
using inf_or_of_complex[of "z -⇩h w"]
using of_complex_sub_of_complex
by auto
lemma sub_eq_inf:
assumes "z -⇩h w = ∞⇩h"
shows "z = ∞⇩h ∨ w = ∞⇩h"
using assms sub_noteq_inf
by blast
subsubsection ‹Multiplication›
text ‹Operations $0_h \cdot_h \infty_h$ and $\infty_h \cdot_h 0_h$ are ill defined. Since all
functions must be total, for formal reasons we define it arbitrarily to be $1_h$.›
definition mult_cvec :: "complex_vec ⇒ complex_vec ⇒ complex_vec" (infixl ‹*⇩v› 70) where
[simp]: "z *⇩v w = (let (z1, z2) = z; (w1, w2) = w
in if (z1 = 0 ∧ w2 = 0) ∨ (w1 = 0 ∧ z2 = 0) then
(1, 1)
else
(z1*w1, z2*w2))"
lift_definition mult_hcoords :: "complex_homo_coords ⇒ complex_homo_coords ⇒ complex_homo_coords" (infixl ‹*⇩h⇩c› 70) is mult_cvec
by (auto split: if_split_asm)
lift_definition mult :: "complex_homo ⇒ complex_homo ⇒ complex_homo" (infixl ‹*⇩h› 70) is mult_hcoords
proof transfer
fix z w z' w' :: complex_vec
obtain z1 z2 w1 w2 z'1 z'2 w'1 w'2 where
*: "z = (z1, z2)" "w = (w1, w2)" "z' = (z'1, z'2)" "w' = (w'1, w'2)"
by (cases z, auto, cases w, auto, cases z', auto, cases w', auto)
assume **:
"z ≠ vec_zero" "w ≠ vec_zero" "z ≈⇩v z'"
"z' ≠ vec_zero" "w' ≠ vec_zero" "w ≈⇩v w'"
show "z *⇩v w ≈⇩v z' *⇩v w'"
proof (cases "(z1 = 0 ∧ w2 = 0) ∨ (w1 = 0 ∧ z2 = 0)")
case True
hence "(z'1 = 0 ∧ w'2 = 0) ∨ (w'1 = 0 ∧ z'2 = 0)"
using * **
by auto
show ?thesis
using ‹(z1 = 0 ∧ w2 = 0) ∨ (w1 = 0 ∧ z2 = 0)› ‹(z'1 = 0 ∧ w'2 = 0) ∨ (w'1 = 0 ∧ z'2 = 0)›
using * **
by simp
next
case False
hence "¬((z'1 = 0 ∧ w'2 = 0) ∨ (w'1 = 0 ∧ z'2 = 0))"
using * **
by auto
hence ***: "z *⇩v w = (z1*w1, z2*w2)" "z' *⇩v w' = (z'1*w'1, z'2*w'2)"
using ‹¬((z1 = 0 ∧ w2 = 0) ∨ (w1 = 0 ∧ z2 = 0))› ‹¬((z'1 = 0 ∧ w'2 = 0) ∨ (w'1 = 0 ∧ z'2 = 0))›
using *
by auto
show ?thesis
apply (subst ***)+
using * **
by simp ((erule exE)+, rule_tac x="k*ka" in exI, simp)
qed
qed
lemma of_complex_mult_of_complex [simp]:
shows "(of_complex z1) *⇩h (of_complex z2) = of_complex (z1 * z2)"
by (transfer, transfer, simp)
lemma mult_commute:
shows "z1 *⇩h z2 = z2 *⇩h z1"
apply (transfer, transfer)
unfolding complex_cvec_eq_def
by (rule_tac x="1" in exI, auto split: if_split_asm)
lemma mult_zero_left [simp]:
assumes "z ≠ ∞⇩h"
shows "0⇩h *⇩h z = 0⇩h"
using assms
proof (transfer, transfer)
fix z :: complex_vec
obtain z1 z2 where *: "z = (z1, z2)"
by (cases z, auto)
assume "z ≠ vec_zero" "¬ (z ≈⇩v ∞⇩v)"
hence "z2 ≠ 0"
using *
by force
thus "0⇩v *⇩v z ≈⇩v 0⇩v"
using *
by simp
qed
lemma mult_zero_right [simp]:
assumes "z ≠ ∞⇩h"
shows "z *⇩h 0⇩h = 0⇩h"
using mult_zero_left[OF assms]
by (simp add: mult_commute)
lemma mult_inf_right [simp]:
assumes "z ≠ 0⇩h"
shows "z *⇩h ∞⇩h = ∞⇩h"
using assms
proof (transfer, transfer)
fix z :: complex_vec
obtain z1 z2 where *: "z = (z1, z2)"
by (cases z, auto)
assume "z ≠ vec_zero" "¬ (z ≈⇩v 0⇩v)"
hence "z1 ≠ 0"
using *
by force
thus "z *⇩v ∞⇩v ≈⇩v ∞⇩v"
using *
by simp
qed
lemma mult_inf_left [simp]:
assumes "z ≠ 0⇩h"
shows "∞⇩h *⇩h z = ∞⇩h"
using mult_inf_right[OF assms]
by (simp add: mult_commute)
lemma mult_one_left [simp]:
shows "1⇩h *⇩h z = z"
by (transfer, transfer, force)
lemma mult_one_right [simp]:
shows "z *⇩h 1⇩h = z"
using mult_one_left[of z]
by (simp add: mult_commute)
text ‹This is ill-defined, but holds by our definition›
lemma inf_mult_zero:
shows "∞⇩h *⇩h 0⇩h = 1⇩h"
by (transfer, transfer, simp)
lemma zero_mult_inf:
shows "0⇩h *⇩h ∞⇩h = 1⇩h"
by (transfer, transfer, simp)
lemma mult_eq_inf:
assumes "z *⇩h w = ∞⇩h"
shows "z = ∞⇩h ∨ w = ∞⇩h"
using assms
using inf_or_of_complex[of z]
using inf_or_of_complex[of w]
using inf_or_of_complex[of "z *⇩h w"]
using of_complex_mult_of_complex
by auto
lemma mult_noteq_inf:
assumes "z ≠ ∞⇩h" and "w ≠ ∞⇩h"
shows "z *⇩h w ≠ ∞⇩h"
using assms mult_eq_inf
by blast
subsubsection ‹Reciprocal›
definition reciprocal_cvec :: "complex_vec ⇒ complex_vec" where
[simp]: "reciprocal_cvec z = (let (z1, z2) = z in (z2, z1))"
lift_definition reciprocal_hcoords :: "complex_homo_coords ⇒ complex_homo_coords" is reciprocal_cvec
by auto
lift_definition reciprocal :: "complex_homo ⇒ complex_homo" is reciprocal_hcoords
by transfer auto
lemma reciprocal_involution [simp]: "reciprocal (reciprocal z) = z"
by (transfer, transfer, auto)
lemma reciprocal_zero [simp]: "reciprocal 0⇩h = ∞⇩h"
by (transfer, transfer, simp)
lemma reciprocal_inf [simp]: "reciprocal ∞⇩h = 0⇩h"
by (transfer, transfer, simp)
lemma reciprocal_one [simp]: "reciprocal 1⇩h = 1⇩h"
by (transfer, transfer, simp)
lemma reciprocal_inf_iff [iff]: "reciprocal z = ∞⇩h ⟷ z = 0⇩h"
by (transfer, transfer, auto)
lemma reciprocal_zero_iff [iff]: "reciprocal z = 0⇩h ⟷ z = ∞⇩h"
by (transfer, transfer, auto)
lemma reciprocal_of_complex [simp]:
assumes "z ≠ 0"
shows "reciprocal (of_complex z) = of_complex (1 / z)"
using assms
by (transfer, transfer, simp)
lemma reciprocal_real:
assumes "is_real (to_complex z)" and "z ≠ 0⇩h" and "z ≠ ∞⇩h"
shows "Re (to_complex (reciprocal z)) = 1 / Re (to_complex z)"
proof-
obtain c where "z = of_complex c" "c ≠ 0" "is_real c"
using assms inf_or_of_complex[of z]
by auto
thus ?thesis
by (simp add: Re_divide_real)
qed
lemma reciprocal_id_iff:
shows "reciprocal z = z ⟷ z = of_complex 1 ∨ z = of_complex (-1)"
proof (cases "z = 0⇩h")
case True
thus ?thesis
by (metis inf_not_of_complex of_complex_zero_iff reciprocal_inf_iff zero_neq_neg_one zero_neq_one)
next
case False
thus ?thesis
using inf_or_of_complex[of z]
by (smt complex_sqrt_1 of_complex_zero_iff reciprocal_inf_iff reciprocal_of_complex to_complex_of_complex)
qed
subsubsection ‹Division›
text ‹Operations $0_h :_h 0_h$ and $\infty_h :_h \infty_h$ are ill-defined. For formal reasons they
are defined to be $1_h$ (by the definition of multiplication).›
definition divide :: "complex_homo ⇒ complex_homo ⇒ complex_homo" (infixl ‹:⇩h› 70) where
"x :⇩h y = x *⇩h (reciprocal y)"
lemma divide_zero_right [simp]:
assumes "z ≠ 0⇩h"
shows "z :⇩h 0⇩h = ∞⇩h"
using assms
unfolding divide_def
by simp
lemma divide_zero_left [simp]:
assumes "z ≠ 0⇩h"
shows "0⇩h :⇩h z = 0⇩h"
using assms
unfolding divide_def
by simp
lemma divide_inf_right [simp]:
assumes "z ≠ ∞⇩h"
shows "z :⇩h ∞⇩h = 0⇩h"
using assms
unfolding divide_def
by simp
lemma divide_inf_left [simp]:
assumes "z ≠ ∞⇩h"
shows "∞⇩h :⇩h z = ∞⇩h"
using assms reciprocal_zero_iff[of z] mult_inf_left
unfolding divide_def
by simp
lemma divide_eq_inf:
assumes "z :⇩h w = ∞⇩h"
shows "z = ∞⇩h ∨ w = 0⇩h"
using assms
using reciprocal_inf_iff[of w] mult_eq_inf
unfolding divide_def
by auto
lemma inf_divide_zero [simp]:
shows "∞⇩h :⇩h 0⇩h = ∞⇩h"
unfolding divide_def
by (transfer, simp)
lemma zero_divide_inf [simp]:
shows "0⇩h :⇩h ∞⇩h = 0⇩h"
unfolding divide_def
by (transfer, simp)
lemma divide_one_right [simp]:
shows "z :⇩h 1⇩h = z"
unfolding divide_def
by simp
lemma of_complex_divide_of_complex [simp]:
assumes "z2 ≠ 0"
shows "(of_complex z1) :⇩h (of_complex z2) = of_complex (z1 / z2)"
using assms
unfolding divide_def
apply transfer
apply transfer
by (simp, rule_tac x="1/z2" in exI, simp)
lemma one_div_of_complex [simp]:
assumes "x ≠ 0"
shows "1⇩h :⇩h of_complex x = of_complex (1 / x)"
using assms
unfolding divide_def
by simp
text ‹ This is ill-defined, but holds by our definition›
lemma inf_divide_inf:
shows "∞⇩h :⇩h ∞⇩h = 1⇩h"
unfolding divide_def
by (simp add: inf_mult_zero)
text ‹ This is ill-defined, but holds by our definition›
lemma zero_divide_zero:
shows "0⇩h :⇩h 0⇩h = 1⇩h"
unfolding divide_def
by (simp add: zero_mult_inf)
subsubsection ‹Conjugate›
definition conjugate_cvec :: "complex_vec ⇒ complex_vec" where
[simp]: "conjugate_cvec z = vec_cnj z"
lift_definition conjugate_hcoords :: "complex_homo_coords ⇒ complex_homo_coords" is conjugate_cvec
by (auto simp add: vec_cnj_def)
lift_definition conjugate :: "complex_homo ⇒ complex_homo" is conjugate_hcoords
by transfer (auto simp add: vec_cnj_def)
lemma conjugate_involution [simp]:
shows "conjugate (conjugate z) = z"
by (transfer, transfer, auto)
lemma conjugate_conjugate_comp [simp]:
shows "conjugate ∘ conjugate = id"
by (rule ext, simp)
lemma inv_conjugate [simp]:
shows "inv conjugate = conjugate"
using inv_unique_comp[of conjugate conjugate]
by simp
lemma conjugate_of_complex [simp]:
shows "conjugate (of_complex z) = of_complex (cnj z)"
by (transfer, transfer, simp add: vec_cnj_def)
lemma conjugate_inf [simp]:
shows "conjugate ∞⇩h = ∞⇩h"
by (transfer, transfer, simp add: vec_cnj_def)
lemma conjugate_zero [simp]:
shows "conjugate 0⇩h = 0⇩h"
by (transfer, transfer, simp add: vec_cnj_def)
lemma conjugate_one [simp]:
shows "conjugate 1⇩h = 1⇩h"
by (transfer, transfer, simp add: vec_cnj_def)
lemma conjugate_inj:
assumes "conjugate x = conjugate y"
shows "x = y"
using assms
using conjugate_involution[of x] conjugate_involution[of y]
by metis
lemma bij_conjugate [simp]:
shows "bij conjugate"
unfolding bij_def inj_on_def
proof auto
fix x y
assume "conjugate x = conjugate y"
thus "x = y"
by (simp add: conjugate_inj)
next
fix x
show "x ∈ range conjugate"
by (metis conjugate_involution range_eqI)
qed
lemma conjugate_id_iff:
shows "conjugate a = a ⟷ is_real (to_complex a) ∨ a = ∞⇩h"
using inf_or_of_complex[of a]
by (metis conjugate_inf conjugate_of_complex eq_cnj_iff_real to_complex_of_complex)
subsubsection ‹Inversion›
text ‹Geometric inversion wrt. the unit circle›
definition inversion where
"inversion = conjugate ∘ reciprocal"
lemma inversion_sym:
shows "inversion = reciprocal ∘ conjugate"
unfolding inversion_def
apply (rule ext, simp)
apply transfer
apply transfer
apply (auto simp add: vec_cnj_def)
using one_neq_zero
by blast+
lemma inversion_involution [simp]:
shows "inversion (inversion z) = z"
proof-
have *: "conjugate ∘ reciprocal = reciprocal ∘ conjugate"
using inversion_sym
by (simp add: inversion_def)
show ?thesis
unfolding inversion_def
by (subst *) simp
qed
lemma inversion_inversion_id [simp]:
shows "inversion ∘ inversion = id"
by (rule ext, simp)
lemma inversion_zero [simp]:
shows "inversion 0⇩h = ∞⇩h"
by (simp add: inversion_def)
lemma inversion_infty [simp]:
shows "inversion ∞⇩h = 0⇩h"
by (simp add: inversion_def)
lemma inversion_of_complex [simp]:
assumes "z ≠ 0"
shows "inversion (of_complex z) = of_complex (1 / cnj z)"
using assms
by (simp add: inversion_def)
lemma is_real_inversion:
assumes "is_real x" and "x ≠ 0"
shows "is_real (to_complex (inversion (of_complex x)))"
using assms eq_cnj_iff_real[of x]
by simp
lemma inversion_id_iff:
shows "a = inversion a ⟷ a ≠ ∞⇩h ∧ (to_complex a) * cnj (to_complex a) = 1" (is "?lhs = ?rhs")
proof
assume "a = inversion a"
thus ?rhs
unfolding inversion_def
using inf_or_of_complex[of a]
by (metis (full_types) comp_apply complex_cnj_cancel_iff complex_cnj_zero inversion_def inversion_infty inversion_of_complex inversion_sym nonzero_eq_divide_eq of_complex_zero reciprocal_zero to_complex_of_complex zero_one_infty_not_equal(5))
next
assume ?rhs
thus ?lhs
using inf_or_of_complex[of a]
by (metis inversion_of_complex mult_not_zero nonzero_mult_div_cancel_right one_neq_zero to_complex_of_complex)
qed
subsection ‹Ratio and cross-ratio›
subsubsection ‹Ratio›
text ‹Ratio of points $z$, $v$ and $w$ is usually defined as
$\frac{z-v}{z-w}$. Our definition introduces it in homogeneous
coordinates. It is well-defined if $z_1 \neq z_2 \vee z_1 \neq z_3$ and $z_1 \neq \infty_h$ and
$z_2 \neq \infty_h \vee z_3 \neq \infty_h$›
definition ratio :: "complex_homo ⇒ complex_homo ⇒ complex_homo ⇒ complex_homo" where
"ratio za zb zc = (za -⇩h zb) :⇩h (za -⇩h zc)"
text ‹This is ill-defined, but holds by our definition›
lemma
assumes "zb ≠ ∞⇩h" and "zc ≠ ∞⇩h"
shows "ratio ∞⇩h zb zc = 1⇩h"
using assms
using inf_sub_left[OF assms(1)]
using inf_sub_left[OF assms(2)]
unfolding ratio_def
by (simp add: inf_divide_inf)
lemma
assumes "za ≠ ∞⇩h" and "zc ≠ ∞⇩h"
shows "ratio za ∞⇩h zc = ∞⇩h"
using assms
unfolding ratio_def
using inf_sub_right[OF assms(1)]
using sub_noteq_inf[OF assms]
using divide_inf_left
by simp
lemma
assumes "za ≠ ∞⇩h" and "zb ≠ ∞⇩h"
shows "ratio za zb ∞⇩h = 0⇩h"
unfolding ratio_def
using sub_noteq_inf[OF assms]
using inf_sub_right[OF assms(1)]
using divide_inf_right
by simp
lemma
assumes "z1 ≠ z2" and "z1 ≠ ∞⇩h"
shows "ratio z1 z2 z1 = ∞⇩h"
using assms
unfolding ratio_def
using divide_zero_right[of "z1 -⇩h z2"]
using sub_eq_zero_iff[of z1 z2]
by simp
subsubsection ‹Cross-ratio›
text ‹The cross-ratio is defined over 4 points $(z, u, v, w)$, usually as
$\frac{(z-u)(v-w)}{(z-w)(v-u)}$. We define it using homogeneous coordinates. Cross ratio is
ill-defined when $z = u \vee v = w$ and $z = w$ and $v = u$ i.e. when 3 points are equal. Since
function must be total, in that case we define it arbitrarily to 1.›
definition cross_ratio_cvec :: "complex_vec ⇒ complex_vec ⇒ complex_vec ⇒ complex_vec ⇒ complex_vec" where
[simp]: "cross_ratio_cvec z u v w =
(let (z', z'') = z;
(u', u'') = u;
(v', v'') = v;
(w', w'') = w;
n1 = z'*u'' - u'*z'';
n2 = v'*w'' - w'*v'';
d1 = z'*w'' - w'*z'';
d2 = v'*u'' - u'*v''
in
if n1 * n2 ≠ 0 ∨ d1 * d2 ≠ 0 then
(n1 * n2, d1 * d2)
else
(1, 1))"
lift_definition cross_ratio_hcoords :: "complex_homo_coords ⇒ complex_homo_coords ⇒ complex_homo_coords ⇒ complex_homo_coords ⇒ complex_homo_coords" is cross_ratio_cvec
by (auto split: if_split_asm)
lift_definition cross_ratio :: "complex_homo ⇒ complex_homo ⇒ complex_homo ⇒ complex_homo ⇒ complex_homo" is cross_ratio_hcoords
proof transfer
fix z u v w z' u' v' w' :: complex_vec
obtain z1 z2 u1 u2 v1 v2 w1 w2 z'1 z'2 u'1 u'2 v'1 v'2 w'1 w'2
where *: "z = (z1, z2)" "u = (u1, u2)" "v = (v1, v2)" "w = (w1, w2)"
"z' = (z'1, z'2)" "u' = (u'1, u'2)" "v' = (v'1, v'2)" "w' = (w'1, w'2)"
by (cases z, auto, cases u, auto, cases v, auto, cases w, auto,
cases z', auto, cases u', auto, cases v', auto, cases w', auto)
let ?n1 = "z1*u2 - u1*z2"
let ?n2 = "v1*w2 - w1*v2"
let ?d1 = "z1*w2 - w1*z2"
let ?d2 = "v1*u2 - u1*v2"
let ?n1' = "z'1*u'2 - u'1*z'2"
let ?n2' = "v'1*w'2 - w'1*v'2"
let ?d1' = "z'1*w'2 - w'1*z'2"
let ?d2' = "v'1*u'2 - u'1*v'2"
assume **:
"z ≠ vec_zero" "u ≠ vec_zero" "v ≠ vec_zero" "w ≠ vec_zero"
"z' ≠ vec_zero" "u' ≠ vec_zero" "v' ≠ vec_zero" "w' ≠ vec_zero"
"z ≈⇩v z'" "v ≈⇩v v'" "u ≈⇩v u'" "w ≈⇩v w'"
show "cross_ratio_cvec z u v w ≈⇩v cross_ratio_cvec z' u' v' w'"
proof (cases "?n1*?n2 ≠ 0 ∨ ?d1*?d2 ≠ 0")
case True
hence "?n1'*?n2' ≠ 0 ∨ ?d1'*?d2' ≠ 0"
using * **
by simp ((erule exE)+, simp)
show ?thesis
using ‹?n1*?n2 ≠ 0 ∨ ?d1*?d2 ≠ 0›
using ‹?n1'*?n2' ≠ 0 ∨ ?d1'*?d2' ≠ 0›
using * **
by simp ((erule exE)+, rule_tac x="k*ka*kb*kc" in exI, simp add: field_simps)
next
case False
hence "¬ (?n1'*?n2' ≠ 0 ∨ ?d1'*?d2' ≠ 0)"
using * **
by simp ((erule exE)+, simp)
show ?thesis
using ‹¬ (?n1*?n2 ≠ 0 ∨ ?d1*?d2 ≠ 0)›
using ‹¬ (?n1'*?n2' ≠ 0 ∨ ?d1'*?d2' ≠ 0)›
using * **
by simp blast
qed
qed
lemma cross_ratio_01inf_id [simp]:
shows "cross_ratio z 0⇩h 1⇩h ∞⇩h = z"
proof (transfer, transfer)
fix z :: complex_vec
obtain z1 z2 where *: "z = (z1, z2)"
by (cases z, auto)
assume "z ≠ vec_zero"
thus "cross_ratio_cvec z 0⇩v 1⇩v ∞⇩v ≈⇩v z"
using *
by simp (rule_tac x="-1" in exI, simp)
qed
lemma cross_ratio_0:
assumes "u ≠ v" and "u ≠ w"
shows "cross_ratio u u v w = 0⇩h"
using assms
proof (transfer, transfer)
fix u v w :: complex_vec
obtain u1 u2 v1 v2 w1 w2
where *: "u = (u1, u2)" "v = (v1, v2)" "w = (w1, w2)"
by (cases u, auto, cases v, auto, cases w, auto)
assume "u ≠ vec_zero" "v ≠ vec_zero" "w ≠ vec_zero" "¬ u ≈⇩v v" "¬ u ≈⇩v w"
thus "cross_ratio_cvec u u v w ≈⇩v 0⇩v"
using * complex_cvec_eq_mix[of u1 u2 v1 v2] complex_cvec_eq_mix[of u1 u2 w1 w2]
by (force simp add: mult.commute)
qed
lemma cross_ratio_1:
assumes "u ≠ v" and "v ≠ w"
shows "cross_ratio v u v w = 1⇩h"
using assms
proof (transfer, transfer)
fix u v w :: complex_vec
obtain u1 u2 v1 v2 w1 w2
where *: "u = (u1, u2)" "v = (v1, v2)" "w = (w1, w2)"
by (cases u, auto, cases v, auto, cases w, auto)
let ?n1 = "v1*u2 - u1*v2"
let ?n2 = "v1*w2 - w1*v2"
assume "u ≠ vec_zero" "v ≠ vec_zero" "w ≠ vec_zero" "¬ u ≈⇩v v" "¬ v ≈⇩v w"
hence "?n1 ≠ 0 ∧ ?n2 ≠ 0"
using * complex_cvec_eq_mix[of u1 u2 v1 v2] complex_cvec_eq_mix[of v1 v2 w1 w2]
by (auto simp add: field_simps)
thus "cross_ratio_cvec v u v w ≈⇩v 1⇩v"
using *
by simp (rule_tac x="1 / (?n1 * ?n2)" in exI, simp)
qed
lemma cross_ratio_inf:
assumes "u ≠ w" and "v ≠ w"
shows "cross_ratio w u v w = ∞⇩h"
using assms
proof (transfer, transfer)
fix u v w :: complex_vec
obtain u1 u2 v1 v2 w1 w2
where *: "u = (u1, u2)" "v = (v1, v2)" "w = (w1, w2)"
by (cases u, auto, cases v, auto, cases w, auto)
let ?n1 = "w1*u2 - u1*w2"
let ?n2 = "v1*w2 - w1*v2"
assume "u ≠ vec_zero" "v ≠ vec_zero" "w ≠ vec_zero" "¬ u ≈⇩v w" "¬ v ≈⇩v w"
hence "?n1 ≠ 0 ∧ ?n2 ≠ 0"
using * complex_cvec_eq_mix[of u1 u2 w1 w2] complex_cvec_eq_mix[of v1 v2 w1 w2]
by (auto simp add: field_simps)
thus "cross_ratio_cvec w u v w ≈⇩v ∞⇩v"
using *
by simp
qed
lemma cross_ratio_0inf:
assumes "y ≠ 0"
shows "cross_ratio (of_complex x) 0⇩h (of_complex y) ∞⇩h = (of_complex (x / y))"
using assms
by (transfer, transfer) (simp, rule_tac x="-1/y" in exI, simp)
lemma cross_ratio_commute_13:
shows "cross_ratio z u v w = reciprocal (cross_ratio v u z w)"
by (transfer, transfer, case_tac z, case_tac u, case_tac v, case_tac w, simp)
lemma cross_ratio_commute_24:
shows "cross_ratio z u v w = reciprocal (cross_ratio z w v u)"
by (transfer, transfer, case_tac z, case_tac u, case_tac v, case_tac w, simp)
lemma cross_ratio_not_inf:
assumes "z ≠ w" and "u ≠ v"
shows "cross_ratio z u v w ≠ ∞⇩h"
using assms
proof (transfer, transfer)
fix z u v w
assume nz: "z ≠ vec_zero" "u ≠ vec_zero" "v ≠ vec_zero" "w ≠ vec_zero"
obtain z1 z2 u1 u2 v1 v2 w1 w2 where *: "z = (z1, z2)" "u = (u1, u2)" "v = (v1, v2)" "w = (w1, w2)"
by (cases z, cases u, cases v, cases w, auto)
obtain x1 x2 where **: "cross_ratio_cvec z u v w = (x1, x2)"
by (cases "cross_ratio_cvec z u v w", auto)
assume "¬ z ≈⇩v w" "¬ u ≈⇩v v"
hence "z1*w2 ≠ z2*w1" "u1*v2 ≠ u2*v1"
using * nz complex_cvec_eq_mix
by blast+
hence "x2 ≠ 0"
using * **
by (auto split: if_split_asm) (simp add: field_simps)
thus "¬ cross_ratio_cvec z u v w ≈⇩v ∞⇩v"
using inf_cvec_z2_zero_iff * **
by simp
qed
lemma cross_ratio_not_zero:
assumes "z ≠ u" and "v ≠ w"
shows "cross_ratio z u v w ≠ 0⇩h"
using assms
proof (transfer, transfer)
fix z u v w
assume nz: "z ≠ vec_zero" "u ≠ vec_zero" "v ≠ vec_zero" "w ≠ vec_zero"
obtain z1 z2 u1 u2 v1 v2 w1 w2 where *: "z = (z1, z2)" "u = (u1, u2)" "v = (v1, v2)" "w = (w1, w2)"
by (cases z, cases u, cases v, cases w, auto)
obtain x1 x2 where **: "cross_ratio_cvec z u v w = (x1, x2)"
by (cases "cross_ratio_cvec z u v w", auto)
assume "¬ z ≈⇩v u" "¬ v ≈⇩v w"
hence "z1*u2 ≠ z2*u1" "v1*w2 ≠ v2*w1"
using * nz complex_cvec_eq_mix
by blast+
hence "x1 ≠ 0"
using * **
by (auto split: if_split_asm)
thus "¬ cross_ratio_cvec z u v w ≈⇩v 0⇩v"
using zero_cvec_z1_zero_iff * **
by simp
qed
lemma cross_ratio_real:
assumes "is_real z" and "is_real u" and "is_real v" and "is_real w"
assumes "z ≠ u ∧ v ≠ w ∨ z ≠ w ∧ u ≠ v"
shows "is_real (to_complex (cross_ratio (of_complex z) (of_complex u) (of_complex v) (of_complex w)))"
using assms
by (transfer, transfer, auto)
lemma cross_ratio:
assumes "(z ≠ u ∧ v ≠ w) ∨ (z ≠ w ∧ u ≠ v)" and
"z ≠ ∞⇩h" and "u ≠ ∞⇩h" and "v ≠ ∞⇩h" and "w ≠ ∞⇩h"
shows "cross_ratio z u v w = ((z -⇩h u) *⇩h (v -⇩h w)) :⇩h ((z -⇩h w) *⇩h (v -⇩h u))"
unfolding sub_def divide_def
using assms
apply transfer
apply simp
apply transfer
proof-
fix z u v w :: complex_vec
obtain z1 z2 u1 u2 v1 v2 w1 w2
where *: "z = (z1, z2)" "u = (u1, u2)" "v = (v1, v2)" "w = (w1, w2)"
by (cases z, auto, cases u, auto, cases v, auto, cases w, auto)
let ?n1 = "z1*u2 - u1*z2"
let ?n2 = "v1*w2 - w1*v2"
let ?d1 = "z1*w2 - w1*z2"
let ?d2 = "v1*u2 - u1*v2"
assume **: "z ≠ vec_zero" "u ≠ vec_zero" "v ≠ vec_zero" "w ≠ vec_zero"
"¬ z ≈⇩v u ∧ ¬ v ≈⇩v w ∨ ¬ z ≈⇩v w ∧ ¬ u ≈⇩v v"
"¬ z ≈⇩v ∞⇩v" "¬ u ≈⇩v ∞⇩v" "¬ v ≈⇩v ∞⇩v" "¬ w ≈⇩v ∞⇩v"
hence ***: "?n1 * ?n2 ≠ 0 ∨ ?d1 * ?d2 ≠ 0"
using *
using complex_cvec_eq_mix[of z1 z2 u1 u2] complex_cvec_eq_mix[of v1 v2 w1 w2]
using complex_cvec_eq_mix[of z1 z2 w1 w2] complex_cvec_eq_mix[of u1 u2 v1 v2]
by (metis eq_iff_diff_eq_0 mult.commute mult_eq_0_iff)
have ****: "z2 ≠ 0" "w2 ≠ 0" "u2 ≠ 0" "v2 ≠ 0"
using * **(1-4) **(6-9)
using inf_cvec_z2_zero_iff[of z1 z2]
using inf_cvec_z2_zero_iff[of u1 u2]
using inf_cvec_z2_zero_iff[of v1 v2]
using inf_cvec_z2_zero_iff[of w1 w2]
by blast+
have "cross_ratio_cvec z u v w = (?n1*?n2, ?d1*?d2)"
using * ***
by simp
moreover
let ?k = "z2*u2*v2*w2"
have "(z +⇩v ~⇩v u) *⇩v (v +⇩v ~⇩v w) *⇩v reciprocal_cvec ((z +⇩v ~⇩v w) *⇩v (v +⇩v ~⇩v u)) = (?k * ?n1 * ?n2, ?k * ?d1 * ?d2)"
using * *** ****
by auto
ultimately
show "cross_ratio_cvec z u v w ≈⇩v
(z +⇩v ~⇩v u) *⇩v (v +⇩v ~⇩v w) *⇩v reciprocal_cvec ((z +⇩v ~⇩v w) *⇩v (v +⇩v ~⇩v u))"
using ****
unfolding complex_cvec_eq_def
by (rule_tac x="?k" in exI) simp
qed
end