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