Theory Gauss_Jordan_Examples

theory Gauss_Jordan_Examples
imports 
  "Gauss_Jordan"
  "Code_Set" (*This file (in which some code equations are removed) is necessary to allow the computation of Gauss-Jordan*)
begin

(*  
    Title:      Gauss_Jordan_Examples.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)


text{*Definitions to transform a matrix to a list of list and vice versa*}
definition vec_to_list :: "'a^'n::{finite, enum} => 'a list"
  where "vec_to_list A = map (op $ A) (enum_class.enum::'n list)"

definition matrix_to_list_of_list :: "'a^'n::{finite, enum}^'m::{finite, enum} => 'a list list"
  where "matrix_to_list_of_list A = map (vec_to_list) (map (op $ A) (enum_class.enum::'m list))"

text{*This definition should be equivalent to @{thm "vector_def"} (in suitable types)*}
definition list_to_vec :: "'a list => 'a^'n::{finite, enum, mod_type}"
  where "list_to_vec xs = vec_lambda (% i. xs ! (to_nat i))"

lemma [code abstract]: "vec_nth (list_to_vec xs) = (%i. xs ! (to_nat i))"
  unfolding list_to_vec_def by fastforce

definition list_of_list_to_matrix :: "'a list list => 'a^'n::{finite, enum, mod_type}^'m::{finite, enum, mod_type}"
  where "list_of_list_to_matrix xs = vec_lambda (%i. list_to_vec (xs ! (to_nat i)))"

lemma [code abstract]: "vec_nth (list_of_list_to_matrix xs) = (%i. list_to_vec (xs ! (to_nat i)))"
  unfolding list_of_list_to_matrix_def by auto

(*
text{*Examples:*}
value[code] "matrix_to_list_of_list (Gauss_Jordan (list_of_list_to_matrix ([[1,0,0,0,0,0],[0,1,0,0,0,0],[0,0,0,0,0,0],[0,0,0,0,8,2]])::real^6^4))"
value[code] "matrix_to_list_of_list (Gauss_Jordan (list_of_list_to_matrix ([[1,-2,1,-3,0],[3,-6,2,-7,0]])::real^5^2))"
value[code] "(reduced_row_echelon_form_upt_k (list_of_list_to_matrix ([[1,0,8],[0,1,9],[0,0,0]])::real^3^3)) 3"
value[code] "matrix_to_list_of_list (Gauss_Jordan (list_of_list_to_matrix [[Complex 1 1,Complex 1 -1, Complex 0 0],[Complex 2 -1,Complex 1 3, Complex 7 3]]::complex^3^2))"
value[code] "DIM(real^5)"
value[code] "DIM(real^5^4)"
value[code] "row_rank (list_of_list_to_matrix [[1,0,0,7,5],[1,0,4,8,-1],[1,0,0,9,8],[1,2,3,6,5]]::real^5^4)"
value[code] "dim (row_space (list_of_list_to_matrix [[1,0,0,7,5],[1,0,4,8,-1],[1,0,0,9,8],[1,2,3,6,5]]::real^5^4))"
value[code] "col_rank (list_of_list_to_matrix [[1,0,0,7,5],[1,0,4,8,-1],[1,0,0,9,8],[1,2,3,6,5]]::real^5^4)"
value[code] "dim (col_space (list_of_list_to_matrix [[1,0,0,7,5],[1,0,4,8,-1],[1,0,0,9,8],[1,2,3,6,5]]::real^5^4))"
value[code] "rank (list_of_list_to_matrix [[1,0,0,7,5],[1,0,4,8,-1],[1,0,0,9,8],[1,2,3,6,5]]::real^5^4)"
value[code] "dim (null_space (list_of_list_to_matrix [[1,0,0,7,5],[1,0,4,8,-1],[1,0,0,9,8],[1,2,3,6,5]]::real^5^4))"
*)

end