Theory Algebraic_Numbers_External_Code

(*  
    Author:      René Thiemann 
    License:     BSD
*)
section ‹Explicit Constants for External Code›

theory Algebraic_Numbers_External_Code
  imports Algebraic_Number_Tests
begin

text ‹We define constants for most operations on real- and complex- algebraic numbers, so that
  they are easily accessible in target languages. In particular, we use target languages 
  integers, pairs of integers, strings, and integer lists, resp., 
  in order to represent the Isabelle types @{typ int}/@{typ nat}, @{typ rat}, @{typ string},
  and @{typ "int poly"}, resp.›

definition "decompose_rat = map_prod integer_of_int integer_of_int o quotient_of" 

subsection ‹Operations on Real Algebraic Numbers›

definition "zero_ra = (0 :: real_alg)"
definition "one_ra = (1 :: real_alg)" 
definition "of_integer_ra = (of_int o int_of_integer :: integer ⇒ real_alg)" 
definition "of_rational_ra = ((λ (num, denom). of_rat_real_alg (Rat.Fract (int_of_integer num) (int_of_integer denom))) 
  :: integer × integer ⇒ real_alg)" 
definition "plus_ra = ((+) :: real_alg ⇒ real_alg ⇒ real_alg)" 
definition "minus_ra = ((-) :: real_alg ⇒ real_alg ⇒ real_alg)" 
definition "uminus_ra = (uminus :: real_alg ⇒ real_alg)" 
definition "times_ra = ((*) :: real_alg ⇒ real_alg ⇒ real_alg)"
definition "divide_ra = ((/) :: real_alg ⇒ real_alg ⇒ real_alg)"
definition "inverse_ra = (inverse :: real_alg ⇒ real_alg)"
definition "abs_ra = (abs :: real_alg ⇒ real_alg)"
definition "floor_ra = (integer_of_int o floor :: real_alg ⇒ integer)"
definition "ceiling_ra = (integer_of_int o ceiling :: real_alg ⇒ integer)"
definition "minimum_ra = (min :: real_alg ⇒ real_alg ⇒ real_alg)"
definition "maximum_ra = (max :: real_alg ⇒ real_alg ⇒ real_alg)"
definition "equals_ra = ((=) :: real_alg ⇒ real_alg ⇒ bool)"
definition "less_ra = ((<) :: real_alg ⇒ real_alg ⇒ bool)"
definition "less_equal_ra = ((≤) :: real_alg ⇒ real_alg ⇒ bool)"
definition "compare_ra = (compare :: real_alg ⇒ real_alg ⇒ order)"
definition "roots_of_poly_ra = (roots_of_real_alg o poly_of_list o map int_of_integer :: integer list ⇒ real_alg list)" 
definition "root_ra = (root_real_alg o nat_of_integer :: integer ⇒ real_alg ⇒ real_alg)" 
definition "show_ra = ((String.implode o show) :: real_alg ⇒ String.literal)" 
definition "is_rational_ra = (is_rat_real_alg :: real_alg ⇒ bool)" 
definition "to_rational_ra = (decompose_rat o to_rat_real_alg :: real_alg ⇒ integer × integer)" 
definition "sign_ra = (fst o to_rational_ra o sgn :: real_alg ⇒ integer)" 
definition "decompose_ra = (map_sum decompose_rat (map_prod (map integer_of_int o coeffs) integer_of_nat) o info_real_alg
  :: real_alg ⇒ integer × integer + integer list × integer)" 


subsection ‹Operations on Complex Algebraic Numbers›

definition "zero_ca = (0 :: complex)" 
definition "one_ca = (1 :: complex)" 
definition "imag_unit_ca = (𝗂 :: complex)" 
definition "of_integer_ca = (of_int o int_of_integer :: integer ⇒ complex)" 
definition "of_rational_ca = ((λ (num, denom). of_rat (Rat.Fract (int_of_integer num) (int_of_integer denom))) 
  :: integer × integer ⇒ complex)" 
definition "of_real_imag_ca = ((λ (real, imag). Complex (real_of real) (real_of imag)) :: real_alg × real_alg ⇒ complex)" 
definition "plus_ca = ((+) :: complex ⇒ complex ⇒ complex)" 
definition "minus_ca = ((-) :: complex ⇒ complex ⇒ complex)" 
definition "uminus_ca = (uminus :: complex ⇒ complex)" 
definition "times_ca = ((*) :: complex ⇒ complex ⇒ complex)"
definition "divide_ca = ((/) :: complex ⇒ complex ⇒ complex)"
definition "inverse_ca = (inverse :: complex ⇒ complex)"
definition "equals_ca = ((=) :: complex ⇒ complex ⇒ bool)"
definition "roots_of_poly_ca = (complex_roots_of_int_poly o poly_of_list o map int_of_integer :: integer list ⇒ complex list)" 
definition "csqrt_ca = (csqrt :: complex ⇒ complex)" 
definition "show_ca = ((String.implode o show) :: complex ⇒ String.literal)" 
definition "real_of_ca = (real_alg_of_real o Re :: complex ⇒ real_alg)" 
definition "imag_of_ca = (real_alg_of_real o Im :: complex ⇒ real_alg)" 

subsection ‹Export Constants in Haskell›

export_code 
  (* preliminary operations *)
  order.Eq order.Lt order.Gt ― ‹for comparison›
  Inl Inr ― ‹make disjoint sums available for decomposition information›

  (* real algebraic operations *)
  zero_ra
  one_ra
  of_integer_ra
  of_rational_ra
  plus_ra
  minus_ra
  uminus_ra
  times_ra
  divide_ra
  inverse_ra
  abs_ra
  floor_ra
  ceiling_ra
  minimum_ra
  maximum_ra
  equals_ra
  less_ra
  less_equal_ra
  compare_ra  
  roots_of_poly_ra
  root_ra
  show_ra
  is_rational_ra
  to_rational_ra
  sign_ra
  decompose_ra

  (* complex algebraic operations *)
  zero_ca
  one_ca
  imag_unit_ca
  of_integer_ca
  of_rational_ca
  of_real_imag_ca
  plus_ca
  minus_ca
  uminus_ca
  times_ca
  divide_ca
  inverse_ca
  equals_ca
  roots_of_poly_ca
  csqrt_ca
  show_ca
  real_of_ca
  imag_of_ca
  
in Haskell module_name Algebraic_Numbers (* file ‹~/Code/Algebraic_Numbers› *)

end