# Theory Jordan_Normal_Form.Conjugate

(*
Author:      René Thiemann
Akihisa Yamada
License:     BSD
*)
theory Conjugate
imports HOL.Complex
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]:
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 ::
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 ::
shows "x * conjugate x = 0  x = 0" "conjugate x * x = 0  x = 0"
by auto

lemma conjugate_square_greater_0 [simp]:
fixes x ::
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 ::
shows "¬ x * conjugate x < 0"
using conjugate_square_positive[of x] by auto

end