(* Author: R. Thiemann *)
section ‹Elimination of CARD('n)›

text ‹In the following theory we provide a method which modifies theorems
  of the form $P[CARD('n)]$ into $n != 0 \Longrightarrow P[n]$, so that they can more
  easily be applied.
  
  Known issues: there might be problems with nested meta-implications and meta-quantification.›

theory Cancel_Card_Constraint
imports 
  "HOL-Types_To_Sets.Types_To_Sets"
  "HOL-Library.Cardinality"
begin

lemma n_zero_nonempty: "n ≠ 0 ⟹ {0 ..< n :: nat} ≠ {}" by auto

lemma type_impl_card_n: assumes "∃(Rep :: 'a ⇒ nat) Abs. type_definition Rep Abs {0 ..< n :: nat}"
  shows "class.finite (TYPE('a)) ∧ CARD('a) = n"
proof -
  from assms obtain rep :: "'a ⇒ nat" and abs :: "nat ⇒ 'a" where t: "type_definition rep abs {0 ..< n}" by auto
  have "card (UNIV :: 'a set) = card {0 ..< n}" using t by (rule type_definition.card)
  also have "… = n" by auto
  finally have bn: "CARD ('a) = n" .
  have "finite (abs ` {0 ..< n})" by auto
  also have "abs ` {0 ..< n} = UNIV" using t by (rule type_definition.Abs_image)
  finally have "class.finite (TYPE('a))" unfolding class.finite_def .
  with bn show ?thesis by blast
qed  

ML_file ‹cancel_card_constraint.ML›


(* below you find an example what the attribute cancel_card_constraint can do and how
   it works internally *)

(*
(* input: some type based lemma with CARD inside, like t0 *)
consts P :: "nat ⇒ nat ⇒ bool" 
axiomatization where t0: "P (CARD ('a :: finite)) (CARD('a) * m)"

(* t0 is converted into a property without the cardinality constraint via the new attribute *)
lemma t_1_to_6: "n ≠ 0 ⟹ P n (n * m)"
  by (rule t0[cancel_card_constraint])

(* The internal steps are as follows. *)

(* 1st step: pull out CARD and introduce new variable n *)
lemma t1: "CARD('a :: finite) = n ⟹ P n (n * m)" 
  using t0[where 'a = 'a] by blast

(* 2nd step: get rid of sorts *)
lemma t2: "class.finite TYPE('a) ⟹ CARD('a) = n ⟹ P n (n * m)"
  by (rule t1[internalize_sort "?'a::finite"])

(* 3rd step: restructure thm so that first two assumptions are merged into one *)
lemma t3: "class.finite TYPE('a) ∧ CARD('a) = n ⟹ P n (n * m)" 
  using t2 by blast

(* 4th step: choose an appropriate carrier set *)
lemma t4: "∃Rep Abs. type_definition Rep Abs {0..<n} ⟹ P n (n * m)"
  by (rule t3[OF type_impl_card_n])

(* 5th step: cancel type definition *)
lemma t5: "{0..<n} ≠ {} ⟹ P n (n * m)"
  by (rule t4[cancel_type_definition])

(* 6th step: simplify non-empty assumption to obtain final theorem *)
lemma t6: "n ≠ 0 ⟹ P n (n * m)" 
  by (rule t5[OF n_zero_nonempty])
*)

end

signature CARD_ELIMINATION =
sig
  val cancel_card_constraint: thm -> thm
  val cancel_card_constraint_attr: attribute
end

structure Card_Elimination : CARD_ELIMINATION =
struct

  (* turns A ==> B[CARD('a)] ==> C[CARD('a), CARD('b)] ==> ... ==> Z 
    into CARD('a) = n1 ==> CARD('b) = n2 ==> A ==> B[n1] ==> C[n1,n2] ==> ... ==> Z *)
  fun extract_card_type ctxt thm = let
    val prop = Thm.prop_of thm 
    fun add_match_terms f t = (if f t then insert (op =) t else I) #>
      (case t of         
        t1 $ t2 => add_match_terms f t1 #> add_match_terms f t2
      | Abs (_,_,t1) => add_match_terms f t1
      | _ => I)
    fun replace_terms xys t = (case AList.lookup (op =) xys t of SOME y => y
      | NONE => case t of
        t1 $ t2 => replace_terms xys t1 $ replace_terms xys t2
      | Abs (a,b,t1) => Abs (a,b,replace_terms xys t1)
      | _ => t)
    fun find_card (Const (c,_) $ Const (t,_)) = (c = @{const_name Finite_Set.card} 
          andalso t = @{const_name Orderings.top_class.top}) 
      | find_card _ = false    
    val card_ts = add_match_terms find_card prop []
    val vars = Term.add_vars prop []
    val all_tvars = Term.add_tvars prop []
    val all_tfrees = map TFree (Variable.variant_frees ctxt [prop] (map (apfst fst) all_tvars))
    val ns = map_index (fn (i,_) => ("n" ^ string_of_int i, @{typ nat})) card_ts
    val substT_map = map fst all_tvars ~~ all_tfrees
    val substT = I subst_TVars substT_map
    val free_ns = Variable.variant_frees ctxt [prop] (map (apfst fst) vars @ ns)
    val all_frees = map (substT o Free) free_ns
    val ns = drop (length vars) all_frees
    val subst = subst_vars (substT_map, map fst vars ~~ (take (length vars) all_frees))
    val prop' = subst prop
    val match_card_ns = add_match_terms find_card prop' [] ~~ rev ns
    val prop'' = replace_terms match_card_ns prop'
    val eqs = map (HOLogic.mk_eq #> HOLogic.mk_Trueprop) match_card_ns |> rev
    val new_thm = Goal.prove ctxt (map fst free_ns) eqs prop'' (fn {prems = prems, context = ctxt} => 
      unfold_tac ctxt (map (fn thm => @{thm sym} OF [thm]) prems)
      THEN resolve_tac ctxt [thm] 1
      THEN (REPEAT (assume_tac ctxt 1))) 
  in 
    (length ns, new_thm)
  end

  (* turns A ==> B ==> C into A /\ B ==> C *)
  (* does not properly work in case of nested meta-implications and meta-quantification *)
  (* TODO: fix and simplify *)
  fun combine_first_prems ctxt thm = let
    val prop = Thm.prop_of thm
    val (p1 :: p2 :: prems) = Thm.prems_of thm
    val concl = Thm.concl_of thm
    val all_tvars = Term.add_tvars prop []
    val all_tfrees = map TFree (Variable.variant_frees ctxt [prop] (map (apfst fst) all_tvars))
    val substT_map = map fst all_tvars ~~ all_tfrees
    val prop' = subst_TVars substT_map prop
    val all_vars = Term.add_vars prop' []
    val free_ns = Variable.variant_frees ctxt [prop'] (map (apfst fst) all_vars)
    val all_frees = map Free free_ns
    val subst = subst_vars (substT_map, map fst all_vars ~~ all_frees)
    
    val p1 = subst p1
    val p2 = subst p2
    val prems = map subst prems
    val concl = subst concl
    val p = HOLogic.mk_conj (HOLogic.dest_Trueprop p1, HOLogic.dest_Trueprop p2)
      |> HOLogic.mk_Trueprop
  in
    Goal.prove ctxt (map fst free_ns) (p :: prems) concl (fn {prems = prems, context = ctxt} =>
      let 
        val p = hd prems
        val p1 = @{thm conjunct1} OF [p]
        val p2 = @{thm conjunct2} OF [p]
        val prems = tl prems
      in           
        resolve_tac ctxt [thm OF (p1 :: p2 :: prems)] 1       
      end)
  end

  (* turns CARD('a) = n1 ==> A ==> B ==> C into
        A ==> B ==> n1 != 0 ==> C *)
  fun eliminate_card_constraint ctxt thm = let
    val v = Thm.ctyp_of ctxt (Thm.prems_of thm |> hd |> (fn t => Term.add_tvars t [] |> hd) |> TVar)
    val thm = Internalize_Sort.internalize_sort v thm |> snd
    val thm = combine_first_prems ctxt thm
    val thm = (thm OF @{thms type_impl_card_n}) |> Local_Typedef.cancel_type_definition
    val thm = thm OF @{thms n_zero_nonempty}
    val thm = rotate_prems 1 thm
  in 
    thm
  end

  (* turns CARD('a) = n1 ==> ... ==> CARD('z) = n_z ==> A ==> B ==> C into
        A ==> B ==> n1 != 0 ==> ... ==> n_z != 0 ==> C *)
  fun eliminate_card_constraints ctxt thm n = 
    fold (K (eliminate_card_constraint ctxt)) (replicate n true) thm
    
  (* turns A ==> B[CARD('a)] ==> C[CARD('a), CARD('b)] ==> ... ==> Z 
    into A ==> B[n1] ==> C[n1,n2] ==> ... ==> n1 != 0 ==> n2 != 0 ==> Z *)
  fun cancel_card_constraint thm = let
    val ctxt = Proof_Context.init_global (Thm.theory_of_thm thm)
    val (n,thm) = extract_card_type ctxt thm
  in 
    eliminate_card_constraints ctxt thm n
  end

  val cancel_card_constraint_attr = Thm.rule_attribute [] (K cancel_card_constraint);

  val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_card_constraint} 
    (Scan.succeed cancel_card_constraint_attr) "cancels carrier constraints")) 
end

(*
  Authors: J. Divasón, R. Thiemann, A. Yamada
*)
section ‹Connecting HMA-matrices with JNF-matrices›

text ‹The following theories provide a connection between the type-based representation of vectors
  and matrices in HOL multivariate-analysis (HMA) with the set-based representation of vectors and matrices
  with integer indices in the Jordan-normal-form (JNF) development.›

subsection ‹Bijections between index types of HMA and natural numbers›

text ‹At the core of HMA-connect, there has to be a translation between indices
  of vectors and matrices, which are via index-types on the one hand, and natural
  numbers on the other hand.

  We some unspecified bijection in our application, and not the conversions
  to-nat and from-nat in theory 
  Rank-Nullity-Theorem/Mod-Type, since our definitions
  below do not enforce any further type constraints.›

theory Bij_Nat
imports 
  "HOL-Library.Cardinality"
  "HOL-Library.Numeral_Type"
begin

lemma finite_set_to_list: "∃ xs :: 'a :: finite list. distinct xs ∧ set xs = Y"
proof -
  have "finite Y" by simp
  thus ?thesis 
  proof (induct Y rule: finite_induct)
    case (insert y Y)
    then obtain xs where xs: "distinct xs" "set xs = Y" by auto
    show ?case
      by (rule exI[of _ "y # xs"], insert xs insert(2), auto)
  qed simp
qed

definition univ_list :: "'a :: finite list" where
  "univ_list = (SOME xs. distinct xs ∧ set xs = UNIV)"

lemma univ_list: "distinct (univ_list :: 'a list)" "set univ_list = (UNIV :: 'a :: finite set)"
proof -
  let ?xs = "univ_list :: 'a list"
  have "distinct ?xs ∧ set ?xs = UNIV"
    unfolding univ_list_def
    by (rule someI_ex, rule finite_set_to_list)
  thus "distinct ?xs" "set ?xs = UNIV" by auto
qed

definition to_nat :: "'a :: finite ⇒ nat" where
  "to_nat a = (SOME i. univ_list ! i = a ∧ i < length (univ_list :: 'a list))"

definition from_nat :: "nat ⇒ 'a :: finite" where
  "from_nat i = univ_list ! i"

lemma length_univ_list_card: "length (univ_list :: 'a :: finite list) = CARD('a)"
  using distinct_card[of "univ_list :: 'a list", symmetric] 
  by (auto simp: univ_list)

lemma to_nat_ex: "∃! i. univ_list ! i = (a :: 'a :: finite) ∧ i < length (univ_list :: 'a list)"
proof -
  let ?ul = "univ_list :: 'a list"
  have a_in_set: "a ∈ set ?ul" unfolding univ_list by auto
  from this [unfolded set_conv_nth] 
  obtain i where i1: "?ul ! i = a ∧ i < length ?ul" by auto
  show ?thesis
  proof (rule ex1I, rule i1)
    fix j
    assume "?ul ! j = a ∧ j < length ?ul"
    moreover have "distinct ?ul" by (simp add: univ_list)
    ultimately show "j = i" using i1 nth_eq_iff_index_eq by blast
  qed
qed
  
lemma to_nat_less_card: "to_nat (a :: 'a :: finite) < CARD('a)"
proof -
  let ?ul = "univ_list :: 'a list"
  from to_nat_ex[of a] obtain i where 
  i1: "univ_list ! i = a ∧ i<length (univ_list::'a list)" by auto
  show ?thesis unfolding to_nat_def
  proof (rule someI2, rule i1)
   fix x
   assume x: "?ul ! x = a ∧ x < length ?ul"
   thus "x < CARD ('a)" using x by (simp add: univ_list length_univ_list_card)
  qed
qed

lemma to_nat_from_nat_id: 
  assumes i: "i < CARD('a :: finite)" 
  shows "to_nat (from_nat i :: 'a) = i"
  unfolding to_nat_def from_nat_def
proof (rule some_equality, simp)
  have l: "length (univ_list::'a list) = card (set (univ_list::'a list))" 
    by (rule distinct_card[symmetric], simp add: univ_list)
  thus i2: "i < length (univ_list::'a list)"
    using i unfolding univ_list by simp
   fix n 
   assume n: "(univ_list::'a list) ! n = (univ_list::'a list) ! i ∧ n < length (univ_list::'a list)"
   have d: "distinct (univ_list::'a list)" using univ_list by simp      
   show "n = i" using nth_eq_iff_index_eq[OF d _ i2] n by auto
qed

lemma from_nat_inj: assumes i: "i < CARD('a :: finite)"
  and j: "j < CARD('a :: finite)"
  and id: "(from_nat i :: 'a) = from_nat j"
  shows "i = j"
proof -
  from arg_cong[OF id, of to_nat]
  show ?thesis using i j by (simp add: to_nat_from_nat_id)
qed

lemma from_nat_to_nat_id[simp]:
  "(from_nat (to_nat a)) = (a::'a :: finite)"
proof -
  have a_in_set: "a ∈ set (univ_list)" unfolding univ_list by auto
  from this [unfolded set_conv_nth] 
  obtain i where i1: "univ_list ! i = a ∧ i<length (univ_list::'a list)" by auto
  show ?thesis 
  unfolding to_nat_def from_nat_def
  by (rule someI2, rule i1, simp)
qed

lemma to_nat_inj[simp]: assumes "to_nat a = to_nat b"
  shows "a = b"
proof -
  from to_nat_ex[of a] to_nat_ex[of b]
  show "a = b" unfolding to_nat_def by (metis assms from_nat_to_nat_id)
qed

lemma range_to_nat: "range (to_nat :: 'a :: finite ⇒ nat) = {0 ..< CARD('a)}" (is "?l = ?r")
proof -
  {
    fix i
    assume "i ∈ ?l"
    hence "i ∈ ?r" using to_nat_less_card[where 'a = 'a] by auto
  }
  moreover
  {
    fix i
    assume "i ∈ ?r"
    hence "i < CARD('a)" by auto
    from to_nat_from_nat_id[OF this] 
    have "i ∈ ?l" by (metis range_eqI)
  }
  ultimately show ?thesis by auto
qed

lemma inj_to_nat: "inj to_nat" by (simp add: inj_on_def)

lemma bij_to_nat: "bij_betw to_nat (UNIV :: 'a :: finite set) {0 ..< CARD('a)}"
  unfolding bij_betw_def by (auto simp: range_to_nat inj_to_nat)


lemma numeral_nat: "(numeral m1 :: nat) * numeral n1 ≡ numeral (m1 * n1)" 
  "(numeral m1 :: nat) + numeral n1 ≡ numeral (m1 + n1)" by simp_all

lemmas card_num_simps = 
  card_num1 card_bit0 card_bit1 
  mult_num_simps
  add_num_simps 
  eq_num_simps
  mult_Suc_right mult_0_right One_nat_def add.right_neutral 
  numeral_nat Suc_numeral 

end

(*
  Authors: J. Divasón, R. Thiemann, A. Yamada, O. Kunčar
*)

subsection ‹Transfer rules to convert theorems from JNF to HMA and vice-versa.›

theory HMA_Connect
imports 
  Jordan_Normal_Form.Spectral_Radius 
  "HOL-Analysis.Determinants"
  "HOL-Analysis.Cartesian_Euclidean_Space"
  Bij_Nat
  Cancel_Card_Constraint
  "HOL-Eisbach.Eisbach" 
begin

text ‹Prefer certain constants and lemmas without prefix.›

hide_const (open) Matrix.mat
hide_const (open) Matrix.row
hide_const (open) Determinant.det

lemmas mat_def = Finite_Cartesian_Product.mat_def
lemmas det_def = Determinants.det_def
lemmas row_def = Finite_Cartesian_Product.row_def

notation vec_index (infixl "$v" 90)
notation vec_nth (infixl "$h" 90)


text ‹Forget that @{typ "'a mat"}, @{typ "'a Matrix.vec"}, and @{typ "'a poly"} 
  have been defined via lifting›


(* TODO: add to end of matrix theory, stores lifting + transfer setup *)
lifting_forget vec.lifting
lifting_forget mat.lifting

lifting_forget poly.lifting

text ‹Some notions which we did not find in the HMA-world.›
definition eigen_vector :: "'a::comm_ring_1 ^ 'n ^ 'n ⇒ 'a ^ 'n ⇒ 'a ⇒ bool" where
  "eigen_vector A v ev = (v ≠ 0 ∧ A *v v = ev *s v)"

definition eigen_value :: "'a :: comm_ring_1 ^ 'n ^ 'n ⇒ 'a ⇒ bool" where
  "eigen_value A k = (∃ v. eigen_vector A v k)"

definition similar_matrix_wit 
  :: "'a :: semiring_1 ^ 'n ^ 'n ⇒ 'a ^ 'n ^ 'n ⇒ 'a ^ 'n ^ 'n ⇒ 'a ^ 'n ^ 'n ⇒ bool" where
  "similar_matrix_wit A B P Q = (P ** Q = mat 1 ∧ Q ** P = mat 1 ∧ A = P ** B ** Q)"

definition similar_matrix 
  :: "'a :: semiring_1 ^ 'n ^ 'n ⇒ 'a ^ 'n ^ 'n ⇒ bool" where
  "similar_matrix A B = (∃ P Q. similar_matrix_wit A B P Q)"

definition spectral_radius :: "complex ^ 'n ^ 'n ⇒ real" where
  "spectral_radius A = Max { norm ev | v ev. eigen_vector A v ev}"

definition Spectrum :: "'a :: field ^ 'n ^ 'n ⇒ 'a set" where
  "Spectrum A = Collect (eigen_value A)" 

definition vec_elements_h :: "'a ^ 'n ⇒ 'a set" where
  "vec_elements_h v = range (vec_nth v)"

lemma vec_elements_h_def': "vec_elements_h v = {v $h i | i. True}"
  unfolding vec_elements_h_def by auto

definition elements_mat_h :: "'a ^ 'nc ^ 'nr ⇒ 'a set" where
  "elements_mat_h A = range (λ (i,j). A $h i $h j)"

lemma elements_mat_h_def': "elements_mat_h A = {A $h i $h j | i j. True}"
  unfolding elements_mat_h_def by auto

definition map_vector :: "('a ⇒ 'b) ⇒ 'a ^'n ⇒ 'b ^'n" where 
  "map_vector f v ≡ χ i. f (v $h i)"

definition map_matrix :: "('a ⇒ 'b) ⇒ 'a ^ 'n ^ 'm ⇒ 'b ^ 'n ^ 'm" where 
  "map_matrix f A ≡ χ i. map_vector f (A $h i)"

definition normbound :: "'a :: real_normed_field ^ 'nc ^ 'nr ⇒ real ⇒ bool" where
  "normbound A b ≡ ∀ x ∈ elements_mat_h A. norm x ≤ b"

lemma spectral_radius_ev_def: "spectral_radius A = Max (norm ` (Collect (eigen_value A)))"
  unfolding spectral_radius_def eigen_value_def[abs_def]
  by (rule arg_cong[where f = Max], auto) 

lemma elements_mat: "elements_mat A = {A $$ (i,j) | i j. i < dim_row A ∧ j < dim_col A}"
  unfolding elements_mat_def by force

definition vec_elements :: "'a Matrix.vec ⇒ 'a set"
  where "vec_elements v = set [v $ i. i <- [0 ..< dim_vec v]]"

lemma vec_elements: "vec_elements v = { v $ i | i. i < dim_vec v}"
  unfolding vec_elements_def by auto


(* TODO: restore a bundle, for e.g., for matrix_impl *)
context includes vec.lifting 
begin
end

definition from_hma⇩v :: "'a ^ 'n  ⇒ 'a Matrix.vec" where
  "from_hma⇩v v = Matrix.vec CARD('n) (λ i. v $h from_nat i)"

definition from_hma⇩m :: "'a ^ 'nc ^ 'nr ⇒ 'a Matrix.mat" where
  "from_hma⇩m a = Matrix.mat CARD('nr) CARD('nc) (λ (i,j). a $h from_nat i $h from_nat j)"

definition to_hma⇩v :: "'a Matrix.vec ⇒ 'a ^ 'n" where
  "to_hma⇩v v = (χ i. v $v to_nat i)"

definition to_hma⇩m :: "'a Matrix.mat ⇒ 'a ^ 'nc  ^ 'nr " where
  "to_hma⇩m a = (χ i j. a $$ (to_nat i, to_nat j))"

declare vec_lambda_eta[simp]

lemma to_hma_from_hma⇩v[simp]: "to_hma⇩v (from_hma⇩v v) = v"
  by (auto simp: to_hma⇩v_def from_hma⇩v_def to_nat_less_card)

lemma to_hma_from_hma⇩m[simp]: "to_hma⇩m (from_hma⇩m v) = v"
  by (auto simp: to_hma⇩m_def from_hma⇩m_def to_nat_less_card)

lemma from_hma_to_hma⇩v[simp]:
  "v ∈ carrier_vec (CARD('n)) ⟹ from_hma⇩v (to_hma⇩v v :: 'a ^ 'n) = v"
  by (auto simp: to_hma⇩v_def from_hma⇩v_def to_nat_from_nat_id)

lemma from_hma_to_hma⇩m[simp]:
  "A ∈ carrier_mat (CARD('nr)) (CARD('nc)) ⟹ from_hma⇩m (to_hma⇩m A :: 'a ^ 'nc  ^ 'nr) = A"
  by (auto simp: to_hma⇩m_def from_hma⇩m_def to_nat_from_nat_id)

lemma from_hma⇩v_inj[simp]: "from_hma⇩v x = from_hma⇩v y ⟷ x = y"
  by (intro iffI, insert to_hma_from_hma⇩v[of x], auto)

lemma from_hma⇩m_inj[simp]: "from_hma⇩m x = from_hma⇩m y ⟷ x = y"
  by(intro iffI, insert to_hma_from_hma⇩m[of x], auto)

definition HMA_V :: "'a Matrix.vec ⇒ 'a ^ 'n  ⇒ bool" where 
  "HMA_V = (λ v w. v = from_hma⇩v w)"

definition HMA_M :: "'a Matrix.mat ⇒ 'a ^ 'nc  ^ 'nr  ⇒ bool" where 
  "HMA_M = (λ a b. a = from_hma⇩m b)"

definition HMA_I :: "nat ⇒ 'n :: finite ⇒ bool" where
  "HMA_I = (λ i a. i = to_nat a)"

context includes lifting_syntax
begin

lemma Domainp_HMA_V [transfer_domain_rule]: 
  "Domainp (HMA_V :: 'a Matrix.vec ⇒ 'a ^ 'n ⇒ bool) = (λ v. v ∈ carrier_vec (CARD('n )))"
  by(intro ext iffI, insert from_hma_to_hma⇩v[symmetric], auto simp: from_hma⇩v_def HMA_V_def)

lemma Domainp_HMA_M [transfer_domain_rule]: 
  "Domainp (HMA_M :: 'a Matrix.mat ⇒ 'a ^ 'nc  ^ 'nr  ⇒ bool) 
  = (λ A. A ∈ carrier_mat CARD('nr) CARD('nc))"
  by (intro ext iffI, insert from_hma_to_hma⇩m[symmetric], auto simp: from_hma⇩m_def HMA_M_def)

lemma Domainp_HMA_I [transfer_domain_rule]: 
  "Domainp (HMA_I :: nat ⇒ 'n :: finite ⇒ bool) = (λ i. i < CARD('n))" (is "?l = ?r")
proof (intro ext)
  fix i :: nat
  show "?l i = ?r i"
    unfolding HMA_I_def Domainp_iff
    by (auto intro: exI[of _ "from_nat i"] simp: to_nat_from_nat_id to_nat_less_card)
qed

lemma bi_unique_HMA_V [transfer_rule]: "bi_unique HMA_V" "left_unique HMA_V" "right_unique HMA_V"
  unfolding HMA_V_def bi_unique_def left_unique_def right_unique_def by auto

lemma bi_unique_HMA_M [transfer_rule]: "bi_unique HMA_M" "left_unique HMA_M" "right_unique HMA_M"
  unfolding HMA_M_def bi_unique_def left_unique_def right_unique_def by auto

lemma bi_unique_HMA_I [transfer_rule]: "bi_unique HMA_I" "left_unique HMA_I" "right_unique HMA_I"
  unfolding HMA_I_def bi_unique_def left_unique_def right_unique_def by auto

lemma right_total_HMA_V [transfer_rule]: "right_total HMA_V"
  unfolding HMA_V_def right_total_def by simp

lemma right_total_HMA_M [transfer_rule]: "right_total HMA_M"
  unfolding HMA_M_def right_total_def by simp

lemma right_total_HMA_I [transfer_rule]: "right_total HMA_I"
  unfolding HMA_I_def right_total_def by simp

lemma HMA_V_index [transfer_rule]: "(HMA_V ===> HMA_I ===> (=)) ($v) ($h)"
  unfolding rel_fun_def HMA_V_def HMA_I_def from_hma⇩v_def
  by (auto simp: to_nat_less_card)

text ‹We introduce the index function to have pointwise access to 
  HMA-matrices by a constant. Otherwise, the transfer rule 
  with @{term "λ A i j. A $h i $h j"} instead of index is not applicable.›

definition "index_hma A i j ≡ A $h i $h j"

lemma HMA_M_index [transfer_rule]:
  "(HMA_M ===> HMA_I ===> HMA_I ===> (=)) (λ A i j. A $$ (i,j)) index_hma"
  by (intro rel_funI, simp add: index_hma_def to_nat_less_card HMA_M_def HMA_I_def from_hma⇩m_def)  

lemma HMA_V_0 [transfer_rule]: "HMA_V (0⇩v CARD('n)) (0 :: 'a :: zero ^ 'n)"
  unfolding HMA_V_def from_hma⇩v_def by auto

lemma HMA_M_0 [transfer_rule]: 
  "HMA_M (0⇩m CARD('nr) CARD('nc)) (0 :: 'a :: zero ^ 'nc  ^ 'nr )"
  unfolding HMA_M_def from_hma⇩m_def by auto

lemma HMA_M_1[transfer_rule]:
  "HMA_M (1⇩m (CARD('n))) (mat 1 :: 'a::{zero,one}^'n^'n)"
  unfolding HMA_M_def
  by (auto simp add: mat_def from_hma⇩m_def from_nat_inj)

lemma from_hma⇩v_add: "from_hma⇩v v + from_hma⇩v w = from_hma⇩v (v + w)"
  unfolding from_hma⇩v_def by auto

lemma HMA_V_add [transfer_rule]: "(HMA_V ===> HMA_V ===> HMA_V) (+) (+) "
  unfolding rel_fun_def HMA_V_def
  by (auto simp: from_hma⇩v_add)

lemma from_hma⇩v_diff: "from_hma⇩v v - from_hma⇩v w = from_hma⇩v (v - w)"
  unfolding from_hma⇩v_def by auto

lemma HMA_V_diff [transfer_rule]: "(HMA_V ===> HMA_V ===> HMA_V) (-) (-)"
  unfolding rel_fun_def HMA_V_def
  by (auto simp: from_hma⇩v_diff)

lemma from_hma⇩m_add: "from_hma⇩m a + from_hma⇩m b = from_hma⇩m (a + b)"
  unfolding from_hma⇩m_def by auto

lemma HMA_M_add [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (+) (+) "
  unfolding rel_fun_def HMA_M_def
  by (auto simp: from_hma⇩m_add)

lemma from_hma⇩m_diff: "from_hma⇩m a - from_hma⇩m b = from_hma⇩m (a - b)"
  unfolding from_hma⇩m_def by auto

lemma HMA_M_diff [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (-) (-) "
  unfolding rel_fun_def HMA_M_def
  by (auto simp: from_hma⇩m_diff)

lemma scalar_product: fixes v :: "'a :: semiring_1 ^ 'n "
  shows "scalar_prod (from_hma⇩v v) (from_hma⇩v w) = scalar_product v w"
  unfolding scalar_product_def scalar_prod_def from_hma⇩v_def dim_vec
  by (simp add: sum.reindex[OF inj_to_nat, unfolded range_to_nat])

lemma [simp]:
  "from_hma⇩m (y :: 'a ^ 'nc  ^ 'nr) ∈ carrier_mat (CARD('nr)) (CARD('nc))"
  "dim_row (from_hma⇩m (y :: 'a ^ 'nc  ^ 'nr )) = CARD('nr)"
  "dim_col (from_hma⇩m (y :: 'a ^ 'nc  ^ 'nr )) = CARD('nc)"
  unfolding from_hma⇩m_def by simp_all

lemma [simp]:
  "from_hma⇩v (y :: 'a ^ 'n) ∈ carrier_vec (CARD('n))"
  "dim_vec (from_hma⇩v (y :: 'a ^ 'n)) = CARD('n)"
  unfolding from_hma⇩v_def by simp_all

declare rel_funI [intro!]

lemma HMA_scalar_prod [transfer_rule]:
  "(HMA_V ===> HMA_V ===> (=)) scalar_prod scalar_product"
  by (auto simp: HMA_V_def scalar_product)

lemma HMA_row [transfer_rule]: "(HMA_I ===> HMA_M ===> HMA_V) (λ i a. Matrix.row a i) row"
  unfolding HMA_M_def HMA_I_def HMA_V_def
  by (auto simp: from_hma⇩m_def from_hma⇩v_def to_nat_less_card row_def)

lemma HMA_col [transfer_rule]: "(HMA_I ===> HMA_M ===> HMA_V) (λ i a. col a i) column"
  unfolding HMA_M_def HMA_I_def HMA_V_def
  by (auto simp: from_hma⇩m_def from_hma⇩v_def to_nat_less_card column_def)

definition mk_mat :: "('i ⇒ 'j ⇒ 'c) ⇒ 'c^'j^'i" where
  "mk_mat f = (χ i j. f i j)"

definition mk_vec :: "('i ⇒ 'c) ⇒ 'c^'i" where
  "mk_vec f = (χ i. f i)"

lemma HMA_M_mk_mat[transfer_rule]: "((HMA_I ===> HMA_I ===> (=)) ===> HMA_M) 
  (λ f. Matrix.mat (CARD('nr)) (CARD('nc)) (λ (i,j). f i j)) 
  (mk_mat :: (('nr ⇒ 'nc ⇒ 'a) ⇒ 'a^'nc^'nr))"
proof-
  {
    fix x y i j
    assume id: "∀ (ya :: 'nr) (yb :: 'nc). (x (to_nat ya) (to_nat yb) :: 'a) = y ya yb"
       and i: "i < CARD('nr)" and j: "j < CARD('nc)"
    from to_nat_from_nat_id[OF i] to_nat_from_nat_id[OF j] id[rule_format, of "from_nat i" "from_nat j"]
    have "x i j = y (from_nat i) (from_nat j)" by auto
  }
  thus ?thesis
    unfolding rel_fun_def mk_mat_def HMA_M_def HMA_I_def from_hma⇩m_def by auto
qed

lemma HMA_M_mk_vec[transfer_rule]: "((HMA_I ===> (=)) ===> HMA_V) 
  (λ f. Matrix.vec (CARD('n)) (λ i. f i)) 
  (mk_vec :: (('n ⇒ 'a) ⇒ 'a^'n))"
proof-
  {
    fix x y i
    assume id: "∀ (ya :: 'n). (x (to_nat ya) :: 'a) = y ya"
       and i: "i < CARD('n)" 
    from to_nat_from_nat_id[OF i] id[rule_format, of "from_nat i"]
    have "x i = y (from_nat i)" by auto
  }
  thus ?thesis
    unfolding rel_fun_def mk_vec_def HMA_V_def HMA_I_def from_hma⇩v_def by auto
qed


lemma mat_mult_scalar: "A ** B = mk_mat (λ i j. scalar_product (row i A) (column j B))"
  unfolding vec_eq_iff matrix_matrix_mult_def scalar_product_def mk_mat_def
  by (auto simp: row_def column_def)

lemma mult_mat_vec_scalar: "A *v v = mk_vec (λ i. scalar_product (row i A) v)"
  unfolding vec_eq_iff matrix_vector_mult_def scalar_product_def mk_mat_def mk_vec_def
  by (auto simp: row_def column_def)

lemma dim_row_transfer_rule: 
  "HMA_M A (A' :: 'a ^ 'nc ^ 'nr) ⟹ (=) (dim_row A) (CARD('nr))"
  unfolding HMA_M_def by auto

lemma dim_col_transfer_rule: 
  "HMA_M A (A' :: 'a ^ 'nc ^ 'nr) ⟹ (=) (dim_col A) (CARD('nc))"
  unfolding HMA_M_def by auto

lemma HMA_M_mult [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) ((*)) ((**))"
proof -
  {
    fix A B :: "'a :: semiring_1 mat" and A' :: "'a ^ 'n  ^ 'nr" and B' :: "'a ^ 'nc ^ 'n"
    assume 1[transfer_rule]: "HMA_M A A'" "HMA_M B B'"
    note [transfer_rule] = dim_row_transfer_rule[OF 1(1)] dim_col_transfer_rule[OF 1(2)]
    have "HMA_M (A * B) (A' ** B')"
      unfolding times_mat_def mat_mult_scalar
      by (transfer_prover_start, transfer_step+, transfer, auto)
  }
  thus ?thesis by blast
qed
      

lemma HMA_V_smult [transfer_rule]: "((=) ===> HMA_V ===> HMA_V) (⋅⇩v) ((*s))"
  unfolding smult_vec_def 
  unfolding rel_fun_def HMA_V_def from_hma⇩v_def
  by auto

lemma HMA_M_mult_vec [transfer_rule]: "(HMA_M ===> HMA_V ===> HMA_V) ((*⇩v)) ((*v))"
proof -
  {
    fix A :: "'a :: semiring_1 mat" and v :: "'a Matrix.vec"
      and A' :: "'a ^ 'nc  ^ 'nr" and v' :: "'a ^ 'nc"
    assume 1[transfer_rule]: "HMA_M A A'" "HMA_V v v'"
    note [transfer_rule] = dim_row_transfer_rule
    have "HMA_V (A *⇩v v) (A' *v v')"
      unfolding mult_mat_vec_def mult_mat_vec_scalar
      by (transfer_prover_start, transfer_step+, transfer, auto)
  }
  thus ?thesis by blast  
qed

lemma HMA_det [transfer_rule]: "(HMA_M ===> (=)) Determinant.det 
  (det :: 'a :: comm_ring_1 ^ 'n ^ 'n ⇒ 'a)"
proof -
  {
    fix a :: "'a ^ 'n ^ 'n"
    let ?tn = "to_nat :: 'n :: finite ⇒ nat"
    let ?fn = "from_nat :: nat ⇒ 'n"
    let ?zn = "{0..< CARD('n)}"
    let ?U = "UNIV :: 'n set"
    let ?p1 = "{p. p permutes ?zn}"
    let ?p2 = "{p. p permutes ?U}"  
    let ?f= "λ p i. if i ∈ ?U then ?fn (p (?tn i)) else i"
    let ?g = "λ p i. ?fn (p (?tn i))"
    have fg: "⋀ a b c. (if a ∈ ?U then b else c) = b" by auto
    have "?p2 = ?f ` ?p1" 
      by (rule permutes_bij', auto simp: to_nat_less_card to_nat_from_nat_id)
    hence id: "?p2 = ?g ` ?p1" by simp
    have inj_g: "inj_on ?g ?p1"
      unfolding inj_on_def
    proof (intro ballI impI ext, auto)
      fix p q i
      assume p: "p permutes ?zn" and q: "q permutes ?zn"
        and id: "(λ i. ?fn (p (?tn i))) = (λ i. ?fn (q (?tn i)))"
      {
        fix i
        from permutes_in_image[OF p] have pi: "p (?tn i) < CARD('n)" by (simp add: to_nat_less_card)
        from permutes_in_image[OF q] have qi: "q (?tn i) < CARD('n)" by (simp add: to_nat_less_card)
        from fun_cong[OF id] have "?fn (p (?tn i))  = from_nat (q (?tn i))" .
        from arg_cong[OF this, of ?tn] have "p (?tn i) = q (?tn i)"
          by (simp add: to_nat_from_nat_id pi qi)
      } note id = this             
      show "p i = q i"
      proof (cases "i < CARD('n)")
        case True
        hence "?tn (?fn i) = i" by (simp add: to_nat_from_nat_id)
        from id[of "?fn i", unfolded this] show ?thesis .
      next
        case False
        thus ?thesis using p q unfolding permutes_def by simp
      qed
    qed
    have mult_cong: "⋀ a b c d. a = b ⟹ c = d ⟹ a * c = b * d" by simp
    have "sum (λ p. 
      signof p * (∏i∈?zn. a $h ?fn i $h ?fn (p i))) ?p1
      = sum (λ p. of_int (sign p) * (∏i∈UNIV. a $h i $h p i)) ?p2"
      unfolding id sum.reindex[OF inj_g]
    proof (rule sum.cong[OF refl], unfold mem_Collect_eq o_def, rule mult_cong)
      fix p
      assume p: "p permutes ?zn"
      let ?q = "λ i. ?fn (p (?tn i))"
      from id p have q: "?q permutes ?U" by auto
      from p have pp: "permutation p" unfolding permutation_permutes by auto
      let ?ft = "λ p i. ?fn (p (?tn i))"
      have fin: "finite ?zn" by simp
      have "sign p = sign ?q ∧ p permutes ?zn"
      using p fin proof (induction rule: permutes_induct)
        case id
        show ?case by (auto simp: sign_id[unfolded id_def] permutes_id[unfolded id_def])
      next
        case (swap a b p)
        then have ‹permutation p›
          by (auto intro: permutes_imp_permutation)
        let ?sab = "Fun.swap a b id"
        let ?sfab = "Fun.swap (?fn a) (?fn b) id"
        have p_sab: "permutation ?sab" by (rule permutation_swap_id)
        have p_sfab: "permutation ?sfab" by (rule permutation_swap_id)
        from swap(4) have IH1: "p permutes ?zn" and IH2: "sign p = sign (?ft p)" by auto
        have sab_perm: "?sab permutes ?zn" using swap(1-2) by (rule permutes_swap_id)
        from permutes_compose[OF IH1 this] have perm1: "?sab o p permutes ?zn" .
        from IH1 have p_p1: "p ∈ ?p1" by simp
        hence "?ft p ∈ ?ft ` ?p1" by (rule imageI)
        from this[folded id] have "?ft p permutes ?U" by simp
        hence p_ftp: "permutation (?ft p)" unfolding permutation_permutes by auto
        {
          fix a b
          assume a: "a ∈ ?zn" and b: "b ∈ ?zn"
          hence "(?fn a = ?fn b) = (a = b)" using swap(1-2)
            by (auto simp: from_nat_inj)
        } note inj = this
        from inj[OF swap(1-2)] have id2: "sign ?sfab = sign ?sab" unfolding sign_swap_id by simp
        have id: "?ft (Fun.swap a b id ∘ p) = Fun.swap (?fn a) (?fn b) id ∘ ?ft p"
        proof
          fix c 
          show "?ft (Fun.swap a b id ∘ p) c = (Fun.swap (?fn a) (?fn b) id ∘ ?ft p) c"
          proof (cases "p (?tn c) = a ∨ p (?tn c) = b")
            case True
            thus ?thesis by (cases, auto simp add: swap_id_eq)
          next
            case False
            hence neq: "p (?tn c) ≠ a" "p (?tn c) ≠ b" by auto
            have pc: "p (?tn c) ∈ ?zn" unfolding permutes_in_image[OF IH1] 
              by (simp add: to_nat_less_card)
            from neq[folded inj[OF pc swap(1)] inj[OF pc swap(2)]]
            have "?fn (p (?tn c)) ≠ ?fn a" "?fn (p (?tn c)) ≠ ?fn b" .
            with neq show ?thesis by (auto simp: swap_id_eq)
          qed
        qed
        show ?case unfolding IH2 id sign_compose[OF p_sab ‹permutation p›] sign_compose[OF p_sfab p_ftp] id2
          by (rule conjI[OF refl perm1])
      qed
      thus "signof p = of_int (sign ?q)" unfolding signof_def sign_def by auto
      show "(∏i = 0..<CARD('n). a $h ?fn i $h ?fn (p i)) =
           (∏i∈UNIV. a $h i $h ?q i)" unfolding 
           range_to_nat[symmetric] prod.reindex[OF inj_to_nat]
        by (rule prod.cong[OF refl], unfold o_def, simp)
    qed   
  }
  thus ?thesis unfolding HMA_M_def 
    by (auto simp: from_hma⇩m_def Determinant.det_def det_def)
qed

lemma HMA_mat[transfer_rule]: "((=) ===> HMA_M) (λ k. k ⋅⇩m 1⇩m CARD('n)) 
  (Finite_Cartesian_Product.mat :: 'a::semiring_1 ⇒ 'a^'n^'n)"
  unfolding Finite_Cartesian_Product.mat_def[abs_def] rel_fun_def HMA_M_def
  by (auto simp: from_hma⇩m_def from_nat_inj)


lemma HMA_mat_minus[transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) 
  (λ A B. A + map_mat uminus B) ((-) :: 'a :: group_add ^'nc^'nr ⇒ 'a^'nc^'nr ⇒ 'a^'nc^'nr)"
  unfolding rel_fun_def HMA_M_def from_hma⇩m_def by auto

definition mat2matofpoly where "mat2matofpoly A = (χ i j. [: A $ i $ j :])"

definition charpoly where charpoly_def: "charpoly A = det (mat (monom 1 (Suc 0)) - mat2matofpoly A)"

definition erase_mat :: "'a :: zero ^ 'nc ^ 'nr ⇒ 'nr ⇒ 'nc ⇒ 'a ^ 'nc ^ 'nr" 
  where "erase_mat A i j = (χ i'. χ  j'. if i' = i ∨ j' = j then 0 else A $ i' $ j')" 

definition sum_UNIV_type :: "('n :: finite ⇒ 'a :: comm_monoid_add) ⇒ 'n itself ⇒ 'a" where
  "sum_UNIV_type f _ = sum f UNIV" 

definition sum_UNIV_set :: "(nat ⇒ 'a :: comm_monoid_add) ⇒ nat ⇒ 'a" where
  "sum_UNIV_set f n = sum f {..<n}" 

definition HMA_T :: "nat ⇒ 'n :: finite itself ⇒ bool" where
  "HMA_T n _ = (n = CARD('n))" 

lemma HMA_mat2matofpoly[transfer_rule]: "(HMA_M ===> HMA_M) (λx. map_mat (λa. [:a:]) x) mat2matofpoly"
  unfolding rel_fun_def HMA_M_def from_hma⇩m_def mat2matofpoly_def by auto

lemma HMA_char_poly [transfer_rule]: 
  "((HMA_M :: ('a:: comm_ring_1 mat ⇒ 'a^'n^'n ⇒ bool)) ===> (=)) char_poly charpoly"
proof -
  {
    fix A :: "'a mat" and A' :: "'a^'n^'n"
    assume [transfer_rule]: "HMA_M A A'"
    hence [simp]: "dim_row A = CARD('n)" by (simp add: HMA_M_def)
    have [simp]: "monom 1 (Suc 0) = [:0, 1 :: 'a :]"
      by (simp add: monom_Suc)
    have [simp]: "map_mat uminus (map_mat (λa. [:a:]) A) = map_mat (λa. [:-a:]) A"
      by (rule eq_matI, auto)
    have "char_poly A = charpoly A'"
      unfolding char_poly_def[abs_def] char_poly_matrix_def charpoly_def[abs_def]
      by (transfer, simp)
  }
  thus ?thesis by blast
qed
 

lemma HMA_eigen_vector [transfer_rule]: "(HMA_M ===> HMA_V ===> (=)) eigenvector eigen_vector"
proof -
  { 
    fix A :: "'a mat" and v :: "'a Matrix.vec" 
    and A' :: "'a ^ 'n ^ 'n" and v' :: "'a ^ 'n" and k :: 'a
    assume 1[transfer_rule]: "HMA_M A A'" and 2[transfer_rule]: "HMA_V v v'"
    hence [simp]: "dim_row A = CARD('n)" "dim_vec v = CARD('n)" by (auto simp add: HMA_V_def HMA_M_def)
    have [simp]: "v ∈ carrier_vec CARD('n)" using 2 unfolding HMA_V_def by simp
    have "eigenvector A v = eigen_vector A' v'" 
      unfolding eigenvector_def[abs_def] eigen_vector_def[abs_def] 
      by (transfer, simp)
  }
  thus ?thesis by blast
qed


lemma HMA_eigen_value [transfer_rule]: "(HMA_M ===> (=) ===> (=)) eigenvalue eigen_value"
proof -
  {
    fix A :: "'a mat" and A' :: "'a ^ 'n  ^ 'n" and k
    assume 1[transfer_rule]: "HMA_M A A'"
    hence [simp]: "dim_row A = CARD('n)" by (simp add: HMA_M_def)
    note [transfer_rule] = dim_row_transfer_rule[OF 1(1)]    
    have "(eigenvalue A k) = (eigen_value A' k)"
      unfolding eigenvalue_def[abs_def] eigen_value_def[abs_def] 
      by (transfer, auto simp add: eigenvector_def)
  }
  thus ?thesis by blast
qed


lemma HMA_spectral_radius [transfer_rule]: 
  "(HMA_M ===> (=)) Spectral_Radius.spectral_radius spectral_radius"
  unfolding Spectral_Radius.spectral_radius_def[abs_def] spectrum_def 
    spectral_radius_ev_def[abs_def]
  by transfer_prover

lemma HMA_elements_mat[transfer_rule]: "((HMA_M :: ('a mat ⇒ 'a ^ 'nc ^ 'nr ⇒ bool))  ===> (=)) 
  elements_mat elements_mat_h"
proof -
  {
    fix y :: "'a ^ 'nc ^ 'nr" and i j :: nat
    assume i: "i < CARD('nr)" and j: "j < CARD('nc)"
    hence "from_hma⇩m y $$ (i, j) ∈ range (λ(i, ya). y $h i $h ya)"      
      using to_nat_from_nat_id[OF i] to_nat_from_nat_id[OF j] by (auto simp: from_hma⇩m_def)
  }
  moreover
  {
    fix y :: "'a ^ 'nc ^ 'nr" and a b
    have "∃i j. y $h a $h b = from_hma⇩m y $$ (i, j) ∧ i < CARD('nr) ∧ j < CARD('nc)"
      unfolding from_hma⇩m_def
      by (rule exI[of _ "Bij_Nat.to_nat a"], rule exI[of _ "Bij_Nat.to_nat b"], auto
        simp: to_nat_less_card)
  }
  ultimately show ?thesis
    unfolding elements_mat[abs_def] elements_mat_h_def[abs_def] HMA_M_def
    by auto
qed  

lemma HMA_vec_elements[transfer_rule]: "((HMA_V :: ('a Matrix.vec ⇒ 'a ^ 'n ⇒ bool))  ===> (=)) 
  vec_elements vec_elements_h"
proof -
  {
    fix y :: "'a ^ 'n" and i :: nat
    assume i: "i < CARD('n)" 
    hence "from_hma⇩v y $ i ∈ range (vec_nth y)"      
      using to_nat_from_nat_id[OF i] by (auto simp: from_hma⇩v_def)
  }
  moreover
  {
    fix y :: "'a ^ 'n" and a
    have "∃i. y $h a = from_hma⇩v y $ i ∧ i < CARD('n)"
      unfolding from_hma⇩v_def
      by (rule exI[of _ "Bij_Nat.to_nat a"], auto simp: to_nat_less_card)
  }
  ultimately show ?thesis
    unfolding vec_elements[abs_def] vec_elements_h_def[abs_def] rel_fun_def HMA_V_def
    by auto
qed  
  
lemma norm_bound_elements_mat: "norm_bound A b = (∀ x ∈ elements_mat A. norm x ≤ b)"
  unfolding norm_bound_def elements_mat by auto

lemma HMA_normbound [transfer_rule]: 
  "((HMA_M :: 'a :: real_normed_field mat ⇒ 'a ^ 'nc ^ 'nr ⇒ bool) ===> (=) ===> (=))
  norm_bound normbound"
  unfolding normbound_def[abs_def] norm_bound_elements_mat[abs_def]
  by (transfer_prover)

lemma HMA_map_matrix [transfer_rule]: 
  "((=) ===> HMA_M ===> HMA_M) map_mat map_matrix"
  unfolding map_vector_def map_matrix_def[abs_def] map_mat_def[abs_def] HMA_M_def from_hma⇩m_def
  by auto

lemma HMA_transpose_matrix [transfer_rule]: 
  "(HMA_M ===> HMA_M) transpose_mat transpose"
  unfolding transpose_mat_def transpose_def HMA_M_def from_hma⇩m_def by auto

lemma HMA_map_vector [transfer_rule]: 
  "((=) ===> HMA_V ===> HMA_V) map_vec map_vector"
  unfolding map_vector_def[abs_def] map_vec_def[abs_def] HMA_V_def from_hma⇩v_def
  by auto

lemma HMA_similar_mat_wit [transfer_rule]: 
  "((HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'n ^ 'n ⇒ _) ===> HMA_M ===> HMA_M ===> HMA_M ===> (=)) 
  similar_mat_wit similar_matrix_wit"
proof (intro rel_funI, goal_cases)
  case (1 a A b B c C d D)  
  note [transfer_rule] = this
  hence id: "dim_row a = CARD('n)" by (auto simp: HMA_M_def)
  have *: "(c * d = 1⇩m (dim_row a) ∧ d * c = 1⇩m (dim_row a) ∧ a = c * b * d) =
    (C ** D = mat 1 ∧ D ** C = mat 1 ∧ A = C ** B ** D)" unfolding id
    by (transfer, simp)
  show ?case unfolding similar_mat_wit_def Let_def similar_matrix_wit_def *
    using 1 by (auto simp: HMA_M_def)
qed

lemma HMA_similar_mat [transfer_rule]: 
  "((HMA_M :: _ ⇒ 'a :: comm_ring_1 ^ 'n ^ 'n ⇒ _) ===> HMA_M ===> (=)) 
  similar_mat similar_matrix"
proof (intro rel_funI, goal_cases)
  case (1 a A b B)
  note [transfer_rule] = this
  hence id: "dim_row a = CARD('n)" by (auto simp: HMA_M_def)
  {
    fix c d
    assume "similar_mat_wit a b c d" 
    hence "{c,d} ⊆ carrier_mat CARD('n) CARD('n)" unfolding similar_mat_wit_def id Let_def by auto
  } note * = this
  show ?case unfolding similar_mat_def similar_matrix_def
    by (transfer, insert *, blast)
qed

lemma HMA_spectrum[transfer_rule]: "(HMA_M ===> (=)) spectrum Spectrum"
  unfolding spectrum_def[abs_def] Spectrum_def[abs_def]
  by transfer_prover

lemma HMA_M_erase_mat[transfer_rule]: "(HMA_M ===> HMA_I ===> HMA_I ===> HMA_M) mat_erase erase_mat" 
  unfolding mat_erase_def[abs_def] erase_mat_def[abs_def]
  by (auto simp: HMA_M_def HMA_I_def from_hma⇩m_def to_nat_from_nat_id intro!: eq_matI)

lemma HMA_M_sum_UNIV[transfer_rule]: 
  "((HMA_I ===> (=)) ===> HMA_T ===> (=)) sum_UNIV_set sum_UNIV_type"
  unfolding rel_fun_def 
proof (clarify, rename_tac f fT n nT)
  fix f and fT :: "'b ⇒ 'a" and n and nT :: "'b itself" 
  assume f: "∀x y. HMA_I x y ⟶ f x = fT y"
    and n: "HMA_T n nT" 
  let ?f = "from_nat :: nat ⇒ 'b" 
  let ?t = "to_nat :: 'b ⇒ nat" 
  from n[unfolded HMA_T_def] have n: "n = CARD('b)" .
  from to_nat_from_nat_id[where 'a = 'b, folded n]
  have tf: "i < n ⟹ ?t (?f i) = i" for i by auto
  have "sum_UNIV_set f n = sum f (?t ` ?f ` {..<n})" 
    unfolding sum_UNIV_set_def
    by (rule arg_cong[of _ _ "sum f"], insert tf, force)
  also have "… = sum (f ∘ ?t) (?f ` {..<n})" 
    by (rule sum.reindex, insert tf n, auto simp: inj_on_def)
  also have "?f ` {..<n} = UNIV" 
    using range_to_nat[where 'a = 'b, folded n] by force
  also have "sum (f ∘ ?t) UNIV = sum fT UNIV" 
  proof (rule sum.cong[OF refl])
    fix i :: 'b
    show "(f ∘ ?t) i = fT i" unfolding o_def 
      by (rule f[rule_format], auto simp: HMA_I_def)
  qed
  also have "… = sum_UNIV_type fT nT" 
    unfolding sum_UNIV_type_def ..
  finally show "sum_UNIV_set f n = sum_UNIV_type fT nT" .
qed
end

text ‹Setup a method to easily convert theorems from JNF into HMA.›

method transfer_hma uses rule = (
  (fold index_hma_def)?, (* prepare matrix access for transfer *)
  transfer,
  rule rule, 
  (unfold carrier_vec_def carrier_mat_def)?, 
  auto)

text ‹Now it becomes easy to transfer results which are not yet proven in HMA, such as:›

lemma matrix_add_vect_distrib: "(A + B) *v v = A *v v + B *v v"
  by (transfer_hma rule: add_mult_distrib_mat_vec)

lemma matrix_vector_right_distrib: "M *v (v + w) = M *v v + M *v w"
  by (transfer_hma rule: mult_add_distrib_mat_vec)

lemma matrix_vector_right_distrib_diff: "(M :: 'a :: ring_1 ^ 'nr ^ 'nc) *v (v - w) = M *v v - M *v w"
  by (transfer_hma rule: mult_minus_distrib_mat_vec)

lemma eigen_value_root_charpoly: 
  "eigen_value A k ⟷ poly (charpoly (A :: 'a :: field ^ 'n ^ 'n)) k = 0"
  by (transfer_hma rule: eigenvalue_root_char_poly)

lemma finite_spectrum: fixes A :: "'a :: field ^ 'n ^ 'n"
  shows "finite (Collect (eigen_value A))" 
  by (transfer_hma rule: card_finite_spectrum(1)[unfolded spectrum_def])

lemma non_empty_spectrum: fixes A :: "complex ^ 'n ^ 'n"
  shows "Collect (eigen_value A) ≠ {}"
  by (transfer_hma rule: spectrum_non_empty[unfolded spectrum_def])

lemma charpoly_transpose: "charpoly (transpose A :: 'a :: field ^ 'n ^ 'n) = charpoly A"
  by (transfer_hma rule: char_poly_transpose_mat)

lemma eigen_value_transpose: "eigen_value (transpose A :: 'a :: field ^ 'n ^ 'n) v = eigen_value A v" 
  unfolding eigen_value_root_charpoly charpoly_transpose by simp

lemma matrix_diff_vect_distrib: "(A - B) *v v = A *v v - B *v (v :: 'a :: ring_1 ^ 'n)"
  by (transfer_hma rule: minus_mult_distrib_mat_vec)

lemma similar_matrix_charpoly: "similar_matrix A B ⟹ charpoly A = charpoly B" 
  by (transfer_hma rule: char_poly_similar)

lemma pderiv_char_poly_erase_mat: fixes A :: "'a :: idom ^ 'n ^ 'n" 
  shows "monom 1 1 * pderiv (charpoly A) = sum (λ i. charpoly (erase_mat A i i)) UNIV" 
proof -
  let ?A = "from_hma⇩m A" 
  let ?n = "CARD('n)" 
  have tA[transfer_rule]: "HMA_M ?A A" unfolding HMA_M_def by simp
  have tN[transfer_rule]: "HMA_T ?n TYPE('n)" unfolding HMA_T_def by simp
  have A: "?A ∈ carrier_mat ?n ?n" unfolding from_hma⇩m_def by auto
  have id: "sum (λ i. charpoly (erase_mat A i i)) UNIV = 
    sum_UNIV_type (λ i. charpoly (erase_mat A i i)) TYPE('n)"
    unfolding sum_UNIV_type_def ..
  show ?thesis unfolding id
    by (transfer, insert pderiv_char_poly_mat_erase[OF A], simp add: sum_UNIV_set_def)
qed

lemma degree_monic_charpoly: fixes A :: "'a :: comm_ring_1 ^ 'n ^ 'n" 
  shows "degree (charpoly A) = CARD('n) ∧ monic (charpoly A)" 
proof (transfer, goal_cases)
  case 1
  from degree_monic_char_poly[OF 1] show ?case by auto
qed

end