Theory HOL-Library.Complex_Order

(*
  Title:    HOL/Library/Complex_Order.thy
  Author:   Dominique Unruh, University of Tartu

  Instantiation of complex numbers as an ordered set.
*)

theory Complex_Order
  imports Complex_Main
begin

instantiation complex :: order begin

definition x < y  Re x < Re y  Im x = Im y
definition x  y  Re x  Re y  Im x = Im y

instance
  apply standard
  by (auto simp: less_complex_def less_eq_complex_def complex_eq_iff)
end

lemma nonnegative_complex_is_real: (x::complex)  0  x  
  by (simp add: complex_is_Real_iff less_eq_complex_def)

lemma complex_is_real_iff_compare0: (x::complex)    x  0  x  0
  using complex_is_Real_iff less_eq_complex_def by auto

instance complex :: ordered_comm_ring
  apply standard
  by (auto simp: less_complex_def less_eq_complex_def complex_eq_iff mult_left_mono mult_right_mono)

instance complex :: ordered_real_vector
  apply standard
  by (auto simp: less_complex_def less_eq_complex_def mult_left_mono mult_right_mono)

instance complex :: ordered_cancel_comm_semiring
  by standard

end