Theory Compare_Complex

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
subsection ‹Compare Instance for Complex Numbers›

text ‹We define some code equations for complex numbers, provide a comparator for complex
  numbers, and register complex numbers for the container framework.›

theory Compare_Complex
imports 
  HOL.Complex
  Polynomial_Interpolation.Missing_Unsorted
  Deriving.Compare_Real
  Containers.Set_Impl
begin

declare [[code drop: Gcd_fin]]
declare [[code drop: Lcm_fin]]

definition gcds :: "'a::semiring_gcd list ⇒ 'a"
  where [simp, code_abbrev]: "gcds xs = gcd_list xs"

lemma [code]:
  "gcds xs = fold gcd xs 0"
  by (simp add: Gcd_fin.set_eq_fold)

definition lcms :: "'a::semiring_gcd list ⇒ 'a"
  where [simp, code_abbrev]: "lcms xs = lcm_list xs"

lemma [code]:
  "lcms xs = fold lcm xs 1"
  by (simp add: Lcm_fin.set_eq_fold)

lemma in_reals_code [code_unfold]:
  "x ∈ ℝ ⟷ Im x = 0" 
  by (fact complex_is_Real_iff)

definition is_norm_1 :: "complex ⇒ bool" where
  "is_norm_1 z = ((Re z)⇧2 + (Im z)⇧2 = 1)"

lemma is_norm_1[simp]: "is_norm_1 x = (norm x = 1)"
  unfolding is_norm_1_def norm_complex_def by simp

definition is_norm_le_1 :: "complex ⇒ bool" where
  "is_norm_le_1 z = ((Re z)⇧2 + (Im z)⇧2 ≤ 1)"

lemma is_norm_le_1[simp]: "is_norm_le_1 x = (norm x ≤ 1)"
  unfolding is_norm_le_1_def norm_complex_def by simp

instantiation complex :: finite_UNIV
begin
definition "finite_UNIV = Phantom(complex) False"
instance
  by (intro_classes, unfold finite_UNIV_complex_def, simp add: infinite_UNIV_char_0)
end

instantiation complex :: compare
begin
definition compare_complex :: "complex ⇒ complex ⇒ order" where
  "compare_complex x y = compare (Re x, Im x) (Re y, Im y)"

instance 
proof (intro_classes, unfold_locales; unfold compare_complex_def)
  fix x y z :: complex
  let ?c = "compare :: (real × real) comparator"
  interpret comparator ?c by (rule comparator_compare)
  show "invert_order (?c (Re x, Im x) (Re y, Im y)) = ?c (Re y, Im y) (Re x, Im x)"
    by (rule sym)
  {
    assume "?c (Re x, Im x) (Re y, Im y) = Lt"
      "?c (Re y, Im y) (Re z, Im z) = Lt"
    thus "?c (Re x, Im x) (Re z, Im z) = Lt"
      by (rule comp_trans)
  }
  {
    assume "?c (Re x, Im x) (Re y, Im y) = Eq"
    from weak_eq[OF this] show "x = y" unfolding complex_eq_iff by auto
  }
qed
end

derive (eq) ceq complex real
derive (compare) ccompare complex
derive (compare) ccompare real
derive (dlist) set_impl complex real
 
end