# Theory Conjugate

```(*
Author:      René Thiemann
*)
theory Conjugate
imports HOL.Complex "HOL-Library.Complex_Order"
begin

class conjugate =
fixes conjugate :: "'a ⇒ 'a"
assumes conjugate_id[simp]: "conjugate (conjugate a) = a"
and conjugate_cancel_iff[simp]: "conjugate a = conjugate b ⟷ a = b"

class conjugatable_ring = ring + conjugate +
assumes conjugate_dist_mul: "conjugate (a * b) = conjugate a * conjugate b"
and conjugate_dist_add: "conjugate (a + b) = conjugate a + conjugate b"
and conjugate_neg: "conjugate (-a) = - conjugate a"
and conjugate_zero[simp]: "conjugate 0 = 0"
begin
lemma conjugate_zero_iff[simp]: "conjugate a = 0 ⟷ a = 0"
using conjugate_cancel_iff[of _ 0, unfolded conjugate_zero].
end

class conjugatable_field = conjugatable_ring + field

lemma sum_conjugate:
fixes f :: "'b ⇒ 'a :: conjugatable_ring"
assumes finX: "finite X"
shows "conjugate (sum f X) = sum (λx. conjugate (f x)) X"
using finX by (induct set:finite, auto simp: conjugate_dist_add)

class conjugatable_ordered_ring = conjugatable_ring + ordered_comm_monoid_add +
assumes conjugate_square_positive: "a * conjugate a ≥ 0"

class conjugatable_ordered_field = conjugatable_ordered_ring + field
begin
subclass conjugatable_field..
end

lemma conjugate_square_0:
fixes a :: "'a :: {conjugatable_ordered_ring, semiring_no_zero_divisors}"
shows "a * conjugate a = 0 ⟹ a = 0" by auto

subsection ‹Instantiations›

instantiation complex :: conjugatable_ordered_field
begin
definition [simp]: "conjugate ≡ cnj"

instance
by intro_classes (auto simp: less_eq_complex_def)

end

instantiation real :: conjugatable_ordered_field
begin
definition [simp]: "conjugate (x::real) ≡ x"
instance by (intro_classes, auto)
end

instantiation rat :: conjugatable_ordered_field
begin
definition [simp]: "conjugate (x::rat) ≡ x"
instance by (intro_classes, auto)
end

instantiation int :: conjugatable_ordered_ring
begin
definition [simp]: "conjugate (x::int) ≡ x"
instance by (intro_classes, auto)
end

lemma conjugate_square_eq_0 [simp]:
fixes x :: "'a :: {conjugatable_ring,semiring_no_zero_divisors}"
shows "x * conjugate x = 0 ⟷ x = 0" "conjugate x * x = 0 ⟷ x = 0"
by auto

lemma conjugate_square_greater_0 [simp]:
fixes x :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors}"
shows "x * conjugate x > 0 ⟷ x ≠ 0"
using conjugate_square_positive[of x]
by (auto simp: le_less)

lemma conjugate_square_smaller_0 [simp]:
fixes x :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors}"
shows "¬ x * conjugate x < 0"
using conjugate_square_positive[of x] by auto

end
```