Theory Algebraic_Number_Tests
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