# Theory Ring_Hom_Matrix

```(*
Author:      René Thiemann
*)
section ‹Matrix Conversions›

text ‹Essentially, the idea is to use the JNF results to estimate the growth rates of
matrices. Since the results in JNF are only applicable for real normed fields,
we cannot directly use them for matrices over the integers or the rational numbers.
To this end, we define a homomorphism which allows us to first convert all numbers
to real numbers, and then do the analysis.›

theory Ring_Hom_Matrix
imports
Matrix
Polynomial_Interpolation.Ring_Hom
begin

locale ord_ring_hom = idom_hom hom for
hom :: "'a :: linordered_idom ⇒ 'b :: floor_ceiling" +
assumes hom_le: "hom x ≤ z ⟹ x ≤ of_int ⌈z⌉"

text ‹Now a class based variant especially for homomorphisms into the reals.›
class real_embedding = linordered_idom +
fixes real_of :: "'a ⇒ real"
assumes
real_add: "real_of ((x :: 'a) + y) = real_of x + real_of y" and
real_mult: "real_of (x * y) = real_of x * real_of y" and
real_zero: "real_of 0 = 0" and
real_one: "real_of 1 = 1" and
real_le: "real_of x ≤ z ⟹ x ≤ of_int ⌈z⌉"

interpretation real_embedding: ord_ring_hom "(real_of :: 'a :: real_embedding ⇒ real)"
by (unfold_locales; fact real_add real_mult real_zero real_one real_le)

instantiation real :: real_embedding
begin
definition real_of_real :: "real ⇒ real" where
"real_of_real x = x"

instance
by (intro_classes, auto simp: real_of_real_def, linarith)
end

instantiation int :: real_embedding
begin

definition real_of_int :: "int ⇒ real" where
"real_of_int x = x"

instance
by (intro_classes, auto simp: real_of_int_def, linarith)
end

lemma real_of_rat_ineq: assumes "real_of_rat x ≤ z"
shows "x ≤ of_int ⌈z⌉"
proof -
have "z ≤ of_int ⌈z⌉" by linarith
from order_trans[OF assms this]
have "real_of_rat x ≤ real_of_rat (of_int ⌈z⌉)" by auto
thus "x ≤ of_int ⌈z⌉" using of_rat_less_eq by blast
qed

instantiation rat :: real_embedding
begin
definition real_of_rat :: "rat ⇒ real" where
"real_of_rat x = of_rat x"

instance
by (intro_classes, auto simp: real_of_rat_def of_rat_add of_rat_mult real_of_rat_ineq)
end

abbreviation mat_real ("mat⇩ℝ") where "mat⇩ℝ ≡ map_mat (real_of :: 'a :: real_embedding ⇒ real)"

end
```