Theory Blinfun_To_Matrix

theory Blinfun_To_Matrix
  imports 
    "Jordan_Normal_Form.Matrix"  
    "Perron_Frobenius.HMA_Connect" 
    "MDP-Rewards.Blinfun_Util"
begin
unbundle no vec_syntax
hide_const Finite_Cartesian_Product.vec
hide_type Finite_Cartesian_Product.vec

subsubsection ‹Gauss Seidel is a Regular Splitting›

abbreviation "mat_inv m ≡ the (mat_inverse m)"

lemma all_imp_Max:
  assumes "finite X" "X ≠ {}" "∀x ∈ X. P (f x)" 
  shows "P (MAX x ∈ X. f x)"
proof -
  have "(MAX x ∈ X. f x) ∈ f ` X"
    using assms
    by auto
  thus ?thesis
    using assms by force
qed

lemma vec_add: "Matrix.vec n (λi. f i + g i) = Matrix.vec n f + Matrix.vec n g"
  by auto

lemma vec_scale: "Matrix.vec n (λi. r * f i) = r ⋅v (Matrix.vec n f)"
  by auto


lift_definition bfun_mat :: "real mat ⇒ (nat ⇒b real) ⇒ (nat ⇒b real)" is "(λm v i. 
    if i < dim_row m  then (m *v (Matrix.vec (dim_col m) (apply_bfun v))) $ i else 0)"
proof 
  fix m :: "real mat" and v
  have "norm(if i < dim_row m then (m *v Matrix.vec (dim_col m) (apply_bfun v)) $v i else 0) ≤ 
    (if dim_row m = 0 then 0 else (MAX i ∈ {0..<dim_row m}. ¦(m *v Matrix.vec (dim_col m) (apply_bfun v)) $v i¦))" for i
    by (force  simp: Max_ge_iff)
  thus "bounded (range (λi. if i < dim_row m then (m *v Matrix.vec (dim_col m) (apply_bfun v)) $v i else 0))"
    by (blast intro!: boundedI)
qed

definition "blinfun_to_mat m n (f :: (nat ⇒b real) ⇒L (nat ⇒b _)) = 
  Matrix.mat m n (λ(i, j). f (Bfun (λk. if j = k then 1 else 0)) i)"

lemma bounded_mult: 
  assumes "bounded ((f :: 'c ⇒ real) ` X)" "bounded (g ` X)"
  shows "bounded ((λx. f x * g x) ` X)"
proof -
  obtain a b :: real where "∀x∈X. norm (f x) ≤ a"  "∀x∈X. norm (g x) ≤ b"  
    using assms  by (auto simp: bounded_iff)
  hence "norm (f x * g x) ≤ a * b" if "x ∈ X" for x
    using that by (auto simp: abs_mult intro!: mult_mono)
  thus ?thesis
    by (fastforce intro!: boundedI)
qed

lift_definition mat_to_blinfun :: "real mat ⇒  (nat ⇒b real) ⇒L (nat ⇒b real)" is bfun_mat
proof
  show "bfun_mat m (x + y) = bfun_mat m x + bfun_mat m y" for m x y
    by (auto simp: vec_add bfun_mat.rep_eq scalar_prod_add_distrib[of _ "dim_col m"])
  show "bfun_mat m (x *R y) = x *R bfun_mat m y" for m x y
    by (auto simp: vec_scale bfun_mat.rep_eq)
  have aux: "0 ≤ Max (abs ` elements_mat (m::real mat))"  if "0 < dim_row m" "0 < dim_col m" for m
    using that by (auto intro: all_imp_Max abs_le_norm_bfun simp: elements_mat_def)
    
  have 1: "¦∑i = 0..<dim_col (m::real mat). m $$ (n, i) * apply_bfun x i¦ ≤ (∑i = 0..<dim_col m. ¦m $$ (n, i) * apply_bfun x i¦)" for x m n
    by (rule sum_abs)
  have 2: "(∑i = 0..<dim_col m. ¦(m::real mat) $$ (n, i) * apply_bfun x i¦) ≤ (∑i = 0..<dim_col m. Max (abs ` elements_mat m) * ¦apply_bfun x i¦) " if "n < dim_row m" for x m n
    unfolding abs_mult elements_mat_def using that by (fastforce intro!: mult_right_mono sum_mono Max_ge)
  have 3: "(∑ i = 0..<dim_col m. Max (abs ` elements_mat m) * ¦apply_bfun x i¦) ≤ (∑i = 0..<dim_col m. Max (abs ` elements_mat m) * norm x)" if "n < dim_row m" for x m n
    using that aux by (intro sum_mono) (auto intro!:  mult_left_mono abs_le_norm_bfun )

  have 4: "(∑i = 0..<dim_col (m::real mat). Max (abs ` elements_mat m) * norm (x :: (_  ⇒b _))) = norm x * dim_col m *  Max (abs ` (elements_mat m))" if "n < dim_row m" for n x m
    using that by auto

  have "¦∑i = 0..<dim_col (m::real mat). m $$ (n, i) * apply_bfun x i¦ ≤ norm x * dim_col m *  Max (abs ` (elements_mat m))" if "n < dim_row m" for x m n
    using order.trans[OF order.trans[OF 1 2[OF that]] 3]  that unfolding 4[OF that] by auto
  hence "norm (bfun_mat m x) ≤ norm x * (if (dim_col m = 0 ∨ dim_row m = 0) then 0 else dim_col m * Max (abs ` (elements_mat m)))" for m x
    using aux 
    by (auto intro!: cSup_least bfun_eqI simp: norm_bfun_def'[of "bfun_mat _ _"] bfun_mat.rep_eq scalar_prod_def mult.assoc)
  thus "∃K. ∀x. norm (bfun_mat m x) ≤ norm x * K" for m
    by auto
qed

lemma mat_to_blinfun_mult: "mat_to_blinfun m (v :: nat ⇒b real) i = bfun_mat m v i"
  by (simp add: mat_to_blinfun.rep_eq)

lemma blinfun_to_mat_add_scale: "blinfun_to_mat n m (v + b *R u) = blinfun_to_mat n m v + b ⋅m (blinfun_to_mat n m u)"
  unfolding blinfun_to_mat_def blinfun.add_left blinfun.scaleR_left
  by auto

lemma mat_scale_one[simp]: "1 ⋅m (m::real mat) = m"
  unfolding smult_mat_def
  by (auto simp: map_mat_def mat_eq_iff)

lemma blinfun_to_mat_add: "(blinfun_to_mat n m (v + u) :: real mat) = blinfun_to_mat n m v + (blinfun_to_mat n m u)"
  using blinfun_to_mat_add_scale[where b = 1]
  by auto

lemma blinfun_to_mat_sub: "(blinfun_to_mat n m (v - u) :: real mat) = blinfun_to_mat n m v - blinfun_to_mat n m u"
   using blinfun_to_mat_add_scale[where b = "-1"]
   by auto  

lemma blinfun_to_mat_zero[simp]: "blinfun_to_mat n m 0 = 0m n m"
  by (auto simp: blinfun_to_mat_def)

lemma blinfun_to_mat_scale: "(blinfun_to_mat n m (r *R v) :: real mat) = r ⋅m (blinfun_to_mat n m v)"
   using blinfun_to_mat_add_scale[where v = 0, where b = "r"]
   by (auto simp add: blinfun_to_mat_def)

lemma Bfun_if[simp]: "apply_bfun (bfun.Bfun (λk. if b k then a else c)) = (λk. if b k then a else c)"
  by (auto intro!: Bfun_inverse)

lemma blinfun_to_mat_correct: "blinfun_to_mat (dim_row v) (dim_col v) (mat_to_blinfun v) = v"
    unfolding blinfun_to_mat_def mat_to_blinfun.rep_eq bfun_mat.rep_eq
    by (auto simp: mult_mat_vec_def Matrix.mat_eq_iff scalar_prod_def if_distrib cong: if_cong)


lemma blinfun_to_mat_id: "blinfun_to_mat n n id_blinfun = 1m n"
  by (auto simp: blinfun_to_mat_def)

lemma nonneg_mult_vec_mono:
  assumes "0m (dim_row X) (dim_col X) ≤ X" "v ≤ u" "dim_vec v = dim_col X"
  shows "X *v (v :: real vec) ≤ X *v u"
  using assms
  unfolding Matrix.less_eq_mat_def Matrix.less_eq_vec_def
  by (auto simp: Matrix.scalar_prod_def intro!: sum_mono mult_left_mono)
  
unbundle no vec_syntax

lemma nonneg_blinfun_mat: "nonneg_blinfun (mat_to_blinfun M) ⟷ (0m (dim_row M) (dim_col M) ≤ M)"
proof
  assume "nonneg_blinfun (mat_to_blinfun M)"
  hence "v ≥ 0 ⟹ 0 ≤ mat_to_blinfun M v" for v unfolding nonneg_blinfun_def by auto
  hence aux: "v ≥ 0 ⟹ 0 ≤ bfun_mat M v" for v unfolding mat_to_blinfun.rep_eq by auto
  hence aux: "(⋀x. apply_bfun v x ≥ 0) ⟹ 0 ≤ bfun_mat M v x" for v x  unfolding less_eq_bfun_def by auto

  have "0 ≤ M $$ (i, j)" if "i < dim_row M" and "j < dim_col M" for i j
    using aux[of "Bfun (λk. if k = j then 1 else 0)"] that
    unfolding bfun_mat.rep_eq
    by (auto cong: if_cong simp: Matrix.mult_mat_vec_def scalar_prod_def if_distrib)
  thus "0m (dim_row M) (dim_col M) ≤ M"
    unfolding less_eq_mat_def by auto
next
  assume "(0m (dim_row M) (dim_col M) ≤ M)"
  hence "0 ≤ M $$ (i,j)" if "i < dim_row M" and "j < dim_col M" for i j
    unfolding less_eq_mat_def using that by auto
  thus "nonneg_blinfun (mat_to_blinfun M)"
    unfolding nonneg_blinfun_def mat_to_blinfun.rep_eq less_eq_bfun_def bfun_mat.rep_eq
    by (auto simp: scalar_prod_def intro!: sum_nonneg)
qed

lemma mat_row_sub: "X ∈ carrier_mat n m ⟹ Y ∈ carrier_mat n m ⟹ i < n ⟹ Matrix.row (X - Y) i = Matrix.row X i - Matrix.row Y i"
  unfolding Matrix.row_def by auto

lemma mat_to_blinfun_sub: "X ∈ carrier_mat n m ⟹ Y ∈ carrier_mat n m ⟹ mat_to_blinfun (X - Y) = mat_to_blinfun X - mat_to_blinfun Y"
  by (auto intro!: blinfun_eqI simp: minus_scalar_prod_distrib[of _ m] mat_row_sub mat_to_blinfun.rep_eq blinfun.diff_left bfun_mat.rep_eq)
 
definition "inverse_mats C D ⟷ (∃n. C ∈ carrier_mat n n ∧ D ∈ carrier_mat n n) ∧ inverts_mat C D ∧ inverts_mat D C"

lemma inverse_mats_sym: "inverse_mats C D ⟹ inverse_mats D C"
  unfolding inverse_mats_def by auto

lemma inverse_mats_unique: 
  assumes "inverse_mats C D" "inverse_mats C E" shows "D = E"
proof -
  have "D = D * (C * E)"
    using assms unfolding inverse_mats_def inverts_mat_def by auto
  also have "… = (D * C) * E"
    using assms unfolding inverse_mats_def by auto
  finally show ?thesis
    using assms unfolding inverse_mats_def inverts_mat_def by auto
qed

definition "inverse_mat D = (THE E. inverse_mats D E)"

lemma invertible_mat_iff_inverse: "invertible_mat M ⟷ (∃N. inverse_mats M N)"
proof
  show "invertible_mat M ⟹ ∃N. inverse_mats M N"
  unfolding invertible_mat_def inverts_mat_def inverse_mats_def
  by (metis carrier_matI index_mult_mat(3) index_one_mat(3) square_mat.elims(2))
  show "∃N. inverse_mats M N ⟹ invertible_mat M "
    unfolding inverse_mats_def invertible_mat_def
    by (metis carrier_matD(1) carrier_matD(2)  square_mat.elims(1))
qed

lemma mat_inverse_eq_inverse_mat:
  assumes "D ∈ carrier_mat n n" "invertible_mat (D :: real mat)" 
  shows "(mat_inverse D) = Some (inverse_mat D)"
proof (cases "mat_inverse D")
  case None
  have "D ∉ Units (ring_mat TYPE(real) n n)"
    by (simp add: assms(1) None mat_inverse) 
  hence "x * D ≠ 1m n ∨ D * x ≠ 1m n" if "x∈carrier_mat n n" for x 
    using assms that by (simp add: Units_def ring_mat_simps)
  hence "¬invertible_mat D" 
    unfolding invertible_mat_iff_inverse
    by (metis assms(1) carrier_matD(1) inverse_mats_def inverts_mat_def)
  then show ?thesis
    using assms by auto
next
  case (Some a)
  hence "inverse_mats D a"
    using assms(1) mat_inverse(2) unfolding inverse_mats_def inverts_mat_def by auto
  thus ?thesis
    unfolding inverse_mat_def local.Some
    using inverse_mats_unique 
    by (auto intro: HOL.the1_equality[symmetric])
qed

lemma invertible_inverse_mats: 
  assumes "invertible_mat M" 
  shows "inverse_mats M (inverse_mat M)"
  by (metis assms inverse_mat_def inverse_mats_unique invertible_mat_iff_inverse theI_unique)

definition "bfun_to_vec n v = Matrix.vec n (apply_bfun v)"

lemma blinfun_to_mat_mult:
  "(blinfun_to_mat n m A) *v (bfun_to_vec m v) = bfun_to_vec n (A (bfun_if (λi. i < m) v 0))"
proof -
  have "(∑ia = 0..<m. (A (bfun.Bfun (λk. if ia = k then 1 else 0))) i * v ia) = (A (bfun_if (λk. k < m) v 0)) i" for i
  proof -
  have "(∑ia = 0..<m. (A (bfun.Bfun (λk. if ia = k then 1 else 0))) i * v ia)  =
    (∑ia = 0..<m. (A (v ia *R bfun.Bfun (λk. if ia = k then 1 else 0)) i))"
    by (auto intro!: sum.cong simp add: blinfun.scaleR_right)
  also have "… = (∑ia = 0..<m. (A (v ia *R bfun.Bfun (λk. if ia = k then 1 else 0)))) i"
    by (induction m) auto
  also have "… = (A  (∑ia = 0..<m. (v ia *R bfun.Bfun (λk. if ia = k then 1 else 0)))) i"
    unfolding blinfun.sum_right by auto
      also have "… = blinfun_apply A (bfun_if (λk. k < m) v 0) i"
      proof -
        have "(∑ia = 0..<m. (v ia *R bfun.Bfun (λk. if ia = k then 1 else 0))) = 
              (∑i = 0..<m. bfun_if (λk. k = i) v 0)"
          by (auto simp: bfun_if.rep_eq intro!: sum.cong)
        also have "… = bfun_if (λk. k < m) v 0"
          by (induction m arbitrary: v) (auto simp add: bfun_eqI bfun_if.rep_eq)
        finally show ?thesis by auto
      qed
      finally show ?thesis.
    qed
    thus ?thesis
  unfolding blinfun_to_mat_def bfun_to_vec_def mult_mat_vec_def scalar_prod_def
  by auto
qed

lemma Max_geI: 
  assumes "finite X" "(y::_:: linorder) ∈ X" "x ≤ y" shows "x ≤ Max X"
  using assms Max_ge_iff by auto

lift_definition vec_to_bfun :: "real vec ⇒ (nat ⇒b real)" is
  "λv i. if i < dim_vec v then v $ i else 0"
proof -
  fix n and v :: "real vec"
  show "(λi. if i < n then v $ i else 0) ∈ bfun"
    by (rule bfun_normI[of _ "if n = 0 then 0 else Max (abs ` (($) v) ` {..<n})"]) (auto intro!: Max_geI)
qed

lemma vec_to_bfun_to_vec[simp]: "bfun_to_vec (dim_vec v) (vec_to_bfun v) = v"
  by (auto simp: bfun_to_vec_def vec_to_bfun.rep_eq)

lemma bfun_to_vec_to_bfun[simp]: "vec_to_bfun (bfun_to_vec m v) = bfun_if (λi. i < m) v 0"
  by (auto simp: bfun_to_vec_def vec_to_bfun.rep_eq bfun_if.rep_eq)
  
lemma bfun_if_vec_to_bfun[simp]: "(bfun_if (λi. i < dim_vec v) (vec_to_bfun v) 0) = vec_to_bfun v"
  by (auto simp: bfun_if.rep_eq vec_to_bfun.rep_eq)

lemma blinfun_to_mat_mult':
  shows "(blinfun_to_mat n (dim_vec v) A) *v v = bfun_to_vec n (blinfun_apply A (vec_to_bfun v))"
  using blinfun_to_mat_mult[of n "dim_vec v" A "vec_to_bfun v"]
  by auto

lemma blinfun_to_mat_mult'':
  assumes "m = dim_vec v"
  shows "(blinfun_to_mat n m A) *v v = bfun_to_vec n (blinfun_apply A (vec_to_bfun v))"
  using blinfun_to_mat_mult' assms
  by auto

lemma matrix_eqI:
  fixes A :: "real mat"
  assumes "⋀v. v ∈ carrier_vec m ⟹ A *v v = B *v v" "A ∈ carrier_mat n m" "B ∈ carrier_mat n m"
  shows "A = B"
proof -
  have "A *v Matrix.vec m (λj. if i = j then 1 else 0) = Matrix.col A i" "B *v Matrix.vec m (λj. if i = j then 1 else 0) = Matrix.col B i"
      if  "i < m" for i
    using assms that
    by (auto simp: mult_mat_vec_def scalar_prod_def if_distrib cong: if_cong)
  thus ?thesis
    using assms
    by (auto intro: Matrix.mat_col_eqI)
qed

lemma blinfun_to_mat_in_carrier[simp]: "blinfun_to_mat m p A ∈ carrier_mat m p"
  unfolding blinfun_to_mat_def
  by auto

lemma blinfun_to_mat_dim_col[simp]: "dim_col (blinfun_to_mat m p A) = p"
  unfolding blinfun_to_mat_def
  by auto

lemma blinfun_to_mat_dim_row[simp]: "dim_row (blinfun_to_mat m p A) = m"
  unfolding blinfun_to_mat_def
  by auto

lemma bfun_to_vec_carrier[simp]: "bfun_to_vec m v ∈ carrier_vec m"
  by (simp add: bfun_to_vec_def)

lemma vec_cong: "(⋀i. i < n ⟹ f i = g i) ⟹ vec n f = vec n g"
  by auto

lemma mat_to_blinfun_compose: 
  assumes "dim_col A = dim_row B"
  shows "(mat_to_blinfun A oL mat_to_blinfun B) = mat_to_blinfun (A * B)"
proof (intro blinfun_eqI bfun_eqI)
  fix i x
  show "apply_bfun (blinfun_apply (mat_to_blinfun A oL mat_to_blinfun B) i) x = apply_bfun (blinfun_apply (mat_to_blinfun (A * B)) i) x "
  proof (cases "x < dim_row A")
    case True
  have "(mat_to_blinfun A oL mat_to_blinfun B) i x = (bfun_mat A (bfun_mat B i)) x"
    by (auto simp: mat_to_blinfun.rep_eq)
  also have "… = Matrix.row A x ∙ vec (dim_col A) (λia. Matrix.row B ia ∙ vec (dim_col B) i)"
    using assms by (auto simp: bfun_mat.rep_eq True cong: vec_cong)
  also have "… = vec (dim_col B) (λj. Matrix.row A x ∙ col B j) ∙ vec (dim_col B) i"
    using assms by (auto simp add: carrier_vecI assoc_scalar_prod[of _ "dim_col A"])    
  also have "… = Matrix.row (A * B) x ∙ vec (dim_col B) (apply_bfun i)"
    by (subst Matrix.row_mult) (auto simp add: assms True)
  also have "… = mat_to_blinfun (A * B) i x"
    by (simp add: mat_to_blinfun.rep_eq bfun_mat.rep_eq True)
  finally show ?thesis.
qed (simp add: bfun_mat.rep_eq mat_to_blinfun_mult)
qed

lemma blinfun_to_mat_compose:
  fixes A B :: "(nat ⇒b real) ⇒L (nat ⇒b real)"
  assumes 
    "⋀v v' j. (⋀i. i < m ⟹ apply_bfun v i = apply_bfun v' i) ⟹ j < n ⟹ A v j = A v' j"
  shows "blinfun_to_mat n m A * blinfun_to_mat m p B = blinfun_to_mat n p (A oL B)"
proof  (rule matrix_eqI[of p _ _ n])
  fix v :: "real vec"
  assume v[simp, intro]: "v ∈ carrier_vec p" 
  hence "blinfun_to_mat n m A * blinfun_to_mat m p B *v v = bfun_to_vec n (A (vec_to_bfun (blinfun_to_mat m p B *v v)))"
    by (auto simp: blinfun_to_mat_mult'' blinfun_to_mat_mult assoc_mult_mat_vec[of _ n m _ p])
  also have "…  = bfun_to_vec n (A (vec_to_bfun (bfun_to_vec m (B (vec_to_bfun v)))))"
    using v by (fastforce simp: blinfun_to_mat_mult'' dest!: carrier_vecD)+
  also have "… = bfun_to_vec n ((A oL B) (vec_to_bfun v))"
    unfolding bfun_to_vec_to_bfun
    using assms by (fastforce simp add: bfun_if.rep_eq bfun_to_vec_def intro!: vec_cong)
  also have "… = blinfun_to_mat n p (A oL B) *v v "
    using v by (fastforce simp: blinfun_to_mat_mult'' dest!: carrier_vecD)+
  finally show "blinfun_to_mat n m A * blinfun_to_mat m p B *v v = blinfun_to_mat n p (A oL B) *v v".
qed auto

lemma invertible_mat_dims: "invertible_mat A ⟹ dim_col A = dim_row A"
  by (simp add: invertible_mat_def)

lemma invertible_mat_square: "invertible_mat A ⟹ square_mat A"
  by (simp add: invertible_mat_dims)

lemma inverse_mat_dims: 
  assumes "invertible_mat A" 
  shows "dim_col (inverse_mat A) = dim_col A" "dim_row (inverse_mat A) = dim_row A"
  using assms inverse_mats_def invertible_inverse_mats by auto

lemma inverse_mat_mult[simp]:
  assumes "invertible_mat A"
  shows "inverse_mat A * A = 1m (dim_row A)" "A * inverse_mat A = 1m (dim_row A)"
  using assms invertible_inverse_mats[OF assms] inverse_mat_dims
  unfolding inverts_mat_def inverse_mats_def
  by auto

lemma invertible_mult:
  assumes "invertible_mat m" "dim_vec a = dim_col m" "dim_vec b = dim_col m"
  shows "a = b ⟷ m *v a = m *v b"
proof -
  have "(inverse_mat m * m) *v a = a" "(inverse_mat m * m) *v b = b"
    by (metis assms carrier_vec_dim_vec inverse_mat_mult(1) invertible_mat_dims one_mult_mat_vec)+
  thus ?thesis
    by (metis assms assoc_mult_mat_vec carrier_mat_triv carrier_vec_dim_vec inverse_mat_dims(1) invertible_mat_dims)
qed

lemma inverse_mult_iff:
  assumes "invertible_mat m" 
  and "dim_vec v = dim_col m" "dim_vec b = dim_row m" 
  shows "v = inverse_mat m *v b ⟷ m *v v = b"
proof -
  have "v = inverse_mat m *v b ⟷ m *v v =  m *v (inverse_mat m *v b)"
    using invertible_mult by (metis assms dim_mult_mat_vec inverse_mat_dims(2) invertible_mat_dims)
  also have "… ⟷   m *v v = (m * inverse_mat m) *v b"
    by (subst assoc_mult_mat_vec[of _ "dim_col m" "dim_col m" _ "dim_col m"])
       (auto simp add: assms carrier_vecI inverse_mat_dims invertible_mat_dims)
  also have "… ⟷ m *v v = b"
    by (metis assms(1) assms(3) carrier_vecI inverse_mat_mult(2) one_mult_mat_vec)
  finally show ?thesis.
qed

lemma inverse_blinfun_to_mat:
  fixes A :: "(nat ⇒b real) ⇒L (nat ⇒b real)"
  assumes "invertibleL A"
  assumes "(⋀v v' j. (⋀i. i < m ⟹ apply_bfun v i = apply_bfun v' i) ⟹ j < m ⟹ (A v) j = (A v') j)" 
  assumes "(⋀v v' j. (⋀i. i < m ⟹ apply_bfun v i = apply_bfun v' i) ⟹ j < m ⟹ (invL A v) j = (invL A v') j)"
  shows "blinfun_to_mat m m (invL A) = (inverse_mat (blinfun_to_mat m m A))" "invertible_mat (blinfun_to_mat m m A)" 
proof -
  have *: "blinfun_to_mat m m A * blinfun_to_mat m m (invL A) = 1m m"
    by (subst blinfun_to_mat_compose) (fastforce simp:  blinfun_to_mat_id assms(1) intro: assms(2))+
  moreover have **: "blinfun_to_mat m m (invL A) * blinfun_to_mat m m A = 1m m"
    by (subst blinfun_to_mat_compose) (fastforce simp:   blinfun_to_mat_id assms(1) intro: assms(3))+
  ultimately have ***: "invertible_mat (blinfun_to_mat m m A)"
    by (metis blinfun_to_mat_dim_col blinfun_to_mat_dim_row invertible_mat_def inverts_mat_def square_mat.elims(1))
  
  have "inverse_mats (blinfun_to_mat m m A) (blinfun_to_mat m m (invL A))"
    unfolding inverse_mats_def inverts_mat_def using * ** by force
  hence "inverse_mat (blinfun_to_mat m m A) = blinfun_to_mat m m (invL A)"
    using *** inverse_mats_unique invertible_inverse_mats by blast
  thus "blinfun_to_mat m m (invL A) = inverse_mat (blinfun_to_mat m m A)" "invertible_mat (blinfun_to_mat m m A)"  
    using ‹invertible_mat (blinfun_to_mat m m A)› by auto
qed

end