# Theory Algebraic_Numbers_External_Code

```(*
Author:      René Thiemann
*)
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)"

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
```