Theory Algebraic_Number_Tests

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Algebraic Number Tests›

text ‹We provide a sequence of examples which demonstrate what can be done with 
  the implementation of algebraic numbers.›

theory Algebraic_Number_Tests
imports
  Jordan_Normal_Form.Char_Poly
  Jordan_Normal_Form.Determinant_Impl
  Show.Show_Complex
  "HOL-Library.Code_Target_Nat"
  "HOL-Library.Code_Target_Int"
  Berlekamp_Zassenhaus.Factorize_Rat_Poly 
  Complex_Algebraic_Numbers
  Show_Real_Precise  
begin

subsection ‹Stand-Alone Examples›

abbreviation (input) "show_lines x  shows_lines x Nil"

fun show_factorization :: "'a :: {semiring_1,show} × (('a poly × nat)list)  string" where
  "show_factorization (c,[]) = show c" 
| "show_factorization (c,((p,i) # ps)) = show_factorization (c,ps) @ '' * ('' @ show p @ '')'' @
  (if i = 1 then [] else ''^'' @ show i)"

definition show_sf_factorization :: "'a :: {semiring_1,show} × (('a poly × nat)list)  string" where
  "show_sf_factorization x = show_factorization (map_prod id (map (map_prod id Suc)) x)
     " 

text ‹Determine the roots over the rational, real, and complex numbers.›

definition "testpoly = [:5/2, -7/2, 1/2, -5, 7, -1, 5/2, -7/2, 1/2:]"
definition "test = show_lines (   real_roots_of_rat_poly testpoly)"

value [code] "show_lines (        roots_of_rat_poly testpoly)"
value [code] "show_lines (   real_roots_of_rat_poly testpoly)"
value [code] "show_lines (complex_roots_of_rat_poly testpoly)"


text ‹Compute real and complex roots of a polynomial with rational coefficients.›

value [code] "show (complex_roots_of_rat_poly testpoly)"
value [code] "show (real_roots_of_rat_poly testpoly)"


text ‹A sequence of calculations.›

value [code] "show (- sqrt 2 - sqrt 3)"
lemma "root 3 4 > sqrt (root 4 3) + 1/10 * root 3 7" by eval
lemma "csqrt (4 + 3 * 𝗂)  " by eval
value [code] "show (csqrt (4 + 3 * 𝗂))"
value [code] "show (csqrt (1 + 𝗂))"

subsection ‹Example Application: Compute Norms of Eigenvalues›

text ‹For complexity analysis of some matrix $A$ it is important to compute the spectral
  radius of a matrix, i.e., the maximal norm of all complex eigenvalues, 
  since the spectral radius determines
  the growth rates of matrix-powers $A^n$, cf.~cite"JNF-AFP" for a formalized statement
  of this fact.›

definition eigenvalues :: "rat mat  complex list" where
  "eigenvalues A = complex_roots_of_rat_poly (char_poly A)"

definition "testmat = mat_of_rows_list 3 [
  [1,-4,2],
  [1/5,7,9],
  [7,1,5 :: rat]
  ]"

definition "spectral_radius_test = show (Max (set [ norm ev. ev  eigenvalues testmat]))"
value [code] "char_poly testmat"
value [code] spectral_radius_test

end