Theory Gauss_Jordan.Inverse_IArrays
section‹Inverse of a matrix using the Gauss Jordan algorithm over nested IArrays›
theory Inverse_IArrays
imports
Inverse
Gauss_Jordan_PA_IArrays
begin
subsection‹Definitions›
definition "invertible_iarray A = (rank_iarray A = nrows_iarray A)"
definition "inverse_matrix_iarray A = (if invertible_iarray A then Some(fst(Gauss_Jordan_iarrays_PA A)) else None)"
definition "matrix_to_iarray_option A = (if A ≠ None then Some (matrix_to_iarray (the A)) else None)"
subsection‹Some lemmas and code generation›
lemma matrix_inv_Gauss_Jordan_iarrays_PA:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes inv_A: "invertible A"
shows "matrix_to_iarray (matrix_inv A) = fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))"
by (metis inv_A matrix_inv_Gauss_Jordan_PA matrix_to_iarray_fst_Gauss_Jordan_PA)
lemma matrix_to_iarray_invertible[code_unfold]:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "invertible A = invertible_iarray (matrix_to_iarray A)"
unfolding invertible_iarray_def invertible_eq_full_rank[of A] matrix_to_iarray_rank matrix_to_iarray_nrows ..
lemma matrix_to_iarray_option_inverse_matrix:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "matrix_to_iarray_option (inverse_matrix A) = (inverse_matrix_iarray (matrix_to_iarray A))"
proof (unfold inverse_matrix_def, auto)
assume inv_A: "invertible A"
show "matrix_to_iarray_option (Some (matrix_inv A)) = inverse_matrix_iarray (matrix_to_iarray A)"
unfolding matrix_to_iarray_option_def unfolding inverse_matrix_iarray_def using inv_A unfolding matrix_to_iarray_invertible
using matrix_inv_Gauss_Jordan_iarrays_PA[OF inv_A] by auto
next
assume not_inv_A: "¬ invertible A"
show "matrix_to_iarray_option None = inverse_matrix_iarray (matrix_to_iarray A)"
unfolding matrix_to_iarray_option_def inverse_matrix_iarray_def
using not_inv_A unfolding matrix_to_iarray_invertible by simp
qed
lemma matrix_to_iarray_option_inverse_matrix_code[code_unfold]:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "matrix_to_iarray_option (inverse_matrix A) = (let matrix_to_iarray_A = matrix_to_iarray A; GJ = Gauss_Jordan_iarrays_PA matrix_to_iarray_A
in if nrows_iarray matrix_to_iarray_A = length [x←IArray.list_of (snd GJ) . ¬ is_zero_iarray x] then Some (fst GJ) else None)"
unfolding matrix_to_iarray_option_inverse_matrix
unfolding inverse_matrix_iarray_def
unfolding invertible_iarray_def
unfolding rank_iarrays_code
unfolding Let_def
unfolding matrix_to_iarray_snd_Gauss_Jordan_PA[symmetric]
unfolding Gauss_Jordan_PA_eq
unfolding matrix_to_iarray_Gauss_Jordan by presburger
lemma[code_unfold]:
shows "inverse_matrix_iarray A = (let A' = (Gauss_Jordan_iarrays_PA A); nrows = IArray.length A in
(if length [x←IArray.list_of (snd A') . ¬ is_zero_iarray x] = nrows
then Some (fst A') else None))"
unfolding inverse_matrix_iarray_def invertible_iarray_def rank_iarrays_code Let_def
unfolding nrows_iarray_def snd_Gauss_Jordan_iarrays_PA_eq ..
end