Up to index of Isabelle/HOL/HOL-Algebra/example_Bicomplex
theory example_Bicomplex(* Title: code_generation/example_Bicomplex.thy
ID: $Id: example_Bicomplex.thy $
Author: Jesus Aransay
*)
theory example_Bicomplex
imports
"~~/src/HOL/Real/Float"
"Matrix/SparseMatrix" (*There is a problem in the
Matrix.thy file in Isabelle 2008 with the "(overloaded)" definition of @{text "zero_matrix_def"}
that we avoid using our own files. New releases of Isabelle fix this problem.*)
"Matrix/cplex/MatrixLP"
"BPL_classes_2008"
"~~/src/HOL/Library/Eval" (*This library provides better support of the @{term "value"} tool*)
"~~/src/HOL/Library/Efficient_Nat" (*This must be always the last library to be loaded*)
begin
section{*An example of the BPL based on bicomplexes.*}
text{*We fit a concrete example of the BPL into the code previously generated*}
text{*The example is as follows:
we have a "big" differential group $D$ which will be represented
as matrices of any dimension of integers, with usual addition of matrices
(two matrices of different dimension can be added obtaining as result
a matrix with the greatest number of rows and the greatest number of columns
between the two matrices being added), and where the null matrix is any
matrix containing exclusively zeros.*}
text{*The minus operation is the result of applying minus to every component
of a matrix. Such structure can be proved to be an abelian group.*}
text{*Then, the differential $d_{D}$ is defined
over the matrices by considering various particular cases
(by means of an @{text "if"} structure). The homology operator $h$ and
the perturbation $\delta_{D}$ are also defined over matrices.*}
text{*The nilpotency condition is locally satisfied for the number of columns
of a matrix plus one.*}
text{*The small differential group $C$ is null.*}
text{*Then, $f$ and $g$ are also null.*}
lemma "- (- x) = (x::'a::lordered_ring)"
using minus_minus [of x] by simp
lemma assumes x_n_0: "x ≠ 0"
shows "(- x) ≠ (0::'a::lordered_ring)"
using x_n_0 by simp
lemma assumes x_n_0: "(- x) ≠ 0"
shows "x ≠ (0::'a::lordered_ring)"
using x_n_0 by simp
lemma nonzero_positions_minus_f:
fixes f:: "'a::lordered_ring matrix => 'b::lordered_ring matrix"
shows "nonzero_positions (Rep_matrix (f A))
= nonzero_positions (Rep_matrix ((- f) A))"
unfolding nonzero_positions_def
unfolding fun_Compl_def
using Rep_minus [of "f A"] by simp
subsection{*Definition of the differential.*}
definition diff_infmatrix :: "'a::{zero} infmatrix => 'a infmatrix"
where diff_infmatrix_def :
"diff_infmatrix A = (%i::nat. %j::nat. if ((i + j) mod 2 = 1) then 0
else (A i (j + 1)))"
definition diff_inv :: "(nat × nat) => (nat × nat)"
where diff_inv_def : "diff_inv pos = ((fst pos, (snd pos) + 1))"
lemma diff_infmatrix_finite[simp]:
shows "finite (nonzero_positions (diff_infmatrix (Rep_matrix x)))"
proof (rule finite_imageD [of diff_inv])
let ?B = "nonzero_positions (diff_infmatrix (Rep_matrix x))"
show "finite (diff_inv ` ?B)"
proof (rule finite_subset [of _ "{i. Rep_matrix x (fst i) (snd i) ≠ 0}"])
show "diff_inv` ?B ⊆ {i. Rep_matrix x (fst i) (snd i) ≠ 0}"
unfolding image_def
unfolding diff_inv_def
unfolding diff_infmatrix_def
unfolding if_def
unfolding nonzero_positions_def by force
show "finite {i::nat × nat. Rep_matrix x (fst i) (snd i) ≠ (0::'a)}"
using finite_nonzero_positions [of x]
unfolding nonzero_positions_def [of "Rep_matrix x"] by simp
qed
show "inj_on diff_inv ?B"
unfolding inj_on_def
unfolding diff_inv_def by auto
qed
lemma diff_infmatrix_matrix:
shows "(diff_infmatrix (Rep_matrix (x::'a::zero matrix))) ∈ matrix"
unfolding matrix_def using diff_infmatrix_finite by simp
lemma diff_infmatrix_closed[simp]:
"Rep_matrix (Abs_matrix (diff_infmatrix (Rep_matrix x)))
= diff_infmatrix (Rep_matrix x)"
using Abs_matrix_inverse [OF diff_infmatrix_matrix [of x]] .
lemma diff_infmatrix_is_matrix: assumes as: "A ∈ matrix"
shows "diff_infmatrix A ∈ matrix"
unfolding matrix_def
unfolding mem_Collect_eq
proof (rule finite_imageD [of diff_inv])
let ?B = "nonzero_positions (diff_infmatrix A)"
show "finite (diff_inv ` ?B)"
proof (rule finite_subset [of _ "{i. A (fst i) (snd i) ≠ 0}"])
show "diff_inv` ?B ⊆ {i. A (fst i) (snd i) ≠ 0}"
unfolding image_def
unfolding diff_inv_def
unfolding diff_infmatrix_def
unfolding if_def
unfolding nonzero_positions_def by force
show "finite {i::nat × nat. A (fst i) (snd i) ≠ (0::'a)}"
using as
unfolding matrix_def
unfolding nonzero_positions_def
unfolding mem_Collect_eq .
qed
show "inj_on diff_inv ?B"
unfolding inj_on_def
unfolding diff_inv_def by auto
qed
lemma diff_infmatrix_twice [simp]:
shows "diff_infmatrix (diff_infmatrix A) = (Rep_matrix 0)"
unfolding diff_infmatrix_def
by (rule ext, rule ext, auto simp add: Rep_matrix_inject) arith
text{*The name @{term "diff_matrix"} is already used to
express the difference between two matrices*}
definition diff_matrix1 :: "'a::lordered_ring matrix => 'a matrix"
where diff_matrix1_def: "diff_matrix1 = Abs_matrix o diff_infmatrix o Rep_matrix"
lemma combine_infmatrix_matrix:
shows "f 0 0 = 0 ==> combine_infmatrix f (Rep_matrix A) (Rep_matrix B) ∈ matrix"
unfolding matrix_def
using finite_subset[of _ "(nonzero_positions (Rep_matrix A))
∪ (nonzero_positions (Rep_matrix B))"]
by simp
lemma combine_infmatrix_diff_infmatrix_matrix[simp]:
"f 0 0 = 0 ==> combine_infmatrix f
(diff_infmatrix (Rep_matrix A)) (diff_infmatrix (Rep_matrix B)) ∈ matrix"
unfolding matrix_def
using finite_subset [of _ "(nonzero_positions (diff_infmatrix (Rep_matrix A))) ∪
(nonzero_positions (diff_infmatrix (Rep_matrix B)))"] by simp
lemma diff_infmatrix_combine_infmatrix_matrix[simp]:
"f 0 0 = 0 ==> diff_infmatrix (combine_infmatrix f (Rep_matrix A)
(Rep_matrix B)) ∈ matrix"
proof (unfold matrix_def, simp, rule finite_imageD [of diff_inv])
let ?B = "nonzero_positions (diff_infmatrix (combine_infmatrix
f (Rep_matrix A) (Rep_matrix B)))"
assume f_0: "f (0::'b) (0::'c) = (0::'a)"
show "finite (diff_inv ` ?B)"
proof -
have "diff_inv` ?B ⊆ {i. f (Rep_matrix A (fst i) (snd i))
(Rep_matrix B (fst i) (snd i)) ≠ 0}"
unfolding diff_infmatrix_def
unfolding combine_infmatrix_def
unfolding image_def
unfolding nonzero_positions_def
unfolding diff_inv_def
unfolding if_def by force
with combine_infmatrix_matrix [of f] f_0 show ?thesis
unfolding matrix_def
unfolding combine_infmatrix_def
unfolding nonzero_positions_def by (simp add: finite_subset)
qed
show "inj_on diff_inv ?B" unfolding inj_on_def diff_inv_def by auto
qed
subsection{*Matrices as an instance of differential group.*}
lemma Abs_matrix_inject2:
assumes x: "x ∈ matrix" and y: "y ∈ matrix" and eq: "x = y"
shows "Abs_matrix x = Abs_matrix y"
using Abs_matrix_inject [OF x y] using eq by simp
lemma diff_matrix1_hom:
shows "diff_matrix1 (A + B) = diff_matrix1 A + diff_matrix1 B"
unfolding plus_matrix_def combine_matrix_def diff_matrix_def diff_matrix1_def
proof (simp add: expand_fun_eq)
show "Abs_matrix (diff_infmatrix (combine_infmatrix op + (Rep_matrix A)
(Rep_matrix B))) =
Abs_matrix (combine_infmatrix op +
(diff_infmatrix (Rep_matrix A)) (diff_infmatrix (Rep_matrix B)))"
proof (rule Abs_matrix_inject2)
show "combine_infmatrix op + (diff_infmatrix (Rep_matrix A))
(diff_infmatrix (Rep_matrix B)) ∈ matrix"
using combine_infmatrix_diff_infmatrix_matrix [of "op + :: 'a => 'a => 'a"]
by simp
show diff_matrix: "diff_infmatrix (combine_infmatrix op + (Rep_matrix A)
(Rep_matrix B)) ∈ matrix"
using diff_infmatrix_combine_infmatrix_matrix [of "op + :: 'a => 'a => 'a"]
by simp
show "diff_infmatrix (combine_infmatrix op + (Rep_matrix A) (Rep_matrix B)) =
combine_infmatrix op + (diff_infmatrix (Rep_matrix A))
(diff_infmatrix (Rep_matrix B))"
unfolding combine_infmatrix_def
unfolding diff_infmatrix_def by (rule ext)+ auto
qed
qed
lemma diff_matrix1_twice:
shows "diff_matrix1 (diff_matrix1 A) = (0::('a::lordered_ring matrix))"
unfolding diff_matrix1_def by simp
instantiation matrix :: (lordered_ring) diff_group_add
begin
definition diff_matrix_def: "diff A == diff_matrix1 A"
instance
proof
fix A B :: "'a matrix"
show "d (A + B) = d A + d B"
using diff_matrix1_hom [of A B] unfolding diff_matrix_def .
show "diff_group_add_class.diff o diff_group_add_class.diff
= (λx::'a::lordered_ring matrix. 0::'a matrix)"
apply (rule ext)
unfolding o_apply
unfolding diff_matrix_def
unfolding diff_matrix1_twice ..
qed
end
subsection{*Definition of the perturbation $\delta_{D}$.*}
definition pert_infmatrix :: "'a::{zero} infmatrix => 'a infmatrix"
where pert_infmatrix_def : "pert_infmatrix A =
(%i::nat. %j::nat. if ((i + j) mod 2 = 1) then 0
else (A (i + 1) j))"
definition pert_inv :: "(nat × nat) => (nat × nat)"
where pert_inv_def : "pert_inv pos = ((fst pos) + 1, snd pos)"
lemma pert_infmatrix_finite[simp]:
shows "finite (nonzero_positions (pert_infmatrix (Rep_matrix x)))"
proof (rule finite_imageD [of pert_inv])
let ?B = "nonzero_positions (pert_infmatrix (Rep_matrix x))"
show "finite (pert_inv ` ?B)"
proof (rule finite_subset [of _ "{i. Rep_matrix x (fst i) (snd i) ≠ 0}"])
show "pert_inv` ?B ⊆ {i. Rep_matrix x (fst i) (snd i) ≠ 0}"
unfolding pert_infmatrix_def
unfolding image_def
unfolding nonzero_positions_def
unfolding pert_inv_def
unfolding if_def by force
show "finite {i::nat × nat. Rep_matrix x (fst i) (snd i) ≠ (0::'a)}"
using finite_nonzero_positions [of x]
unfolding nonzero_positions_def [of "Rep_matrix x"] .
qed
show "inj_on pert_inv ?B" unfolding inj_on_def pert_inv_def by auto
qed
lemma pert_infmatrix_matrix:
shows "(pert_infmatrix (Rep_matrix (x::'a::zero matrix))) ∈ matrix"
unfolding matrix_def by (simp add: pert_infmatrix_finite)
lemma pert_infmatrix_closed[simp]:
"Rep_matrix (Abs_matrix (pert_infmatrix (Rep_matrix x)))
= pert_infmatrix (Rep_matrix x)"
by (rule Abs_matrix_inverse) (simp only: pert_infmatrix_matrix)
lemma pert_infmatrix_is_matrix: assumes as: "A ∈ matrix"
shows "pert_infmatrix A ∈ matrix"
unfolding matrix_def
unfolding mem_Collect_eq
proof (rule finite_imageD [of pert_inv])
let ?B = "nonzero_positions (pert_infmatrix A)"
show "finite (pert_inv ` ?B)"
proof (rule finite_subset [of _ "{i. A (fst i) (snd i) ≠ 0}"])
show "pert_inv` ?B ⊆ {i. A (fst i) (snd i) ≠ 0}"
unfolding image_def
unfolding pert_inv_def
unfolding pert_infmatrix_def
unfolding if_def
unfolding nonzero_positions_def by force
show "finite {i::nat × nat. A (fst i) (snd i) ≠ (0::'a)}"
using as
unfolding matrix_def
unfolding nonzero_positions_def
unfolding mem_Collect_eq .
qed
show "inj_on pert_inv ?B"
unfolding inj_on_def
unfolding pert_inv_def by auto
qed
lemma pert_infmatrix_twice [simp]:
shows "pert_infmatrix (pert_infmatrix A) = (Rep_matrix 0)"
unfolding pert_infmatrix_def
by (rule ext, rule ext, auto simp add: Rep_matrix_inject) arith
text{*We will use the name @{term "pert_matrix1"} to define the
perturbation in this context, leaving thus the name
@{term "pert_matrix"} to be used inside of the instance
@{text "matrix::diff_group_add_pert"}.*}
definition pert_matrix1 :: "'a::lordered_ring matrix => 'a matrix"
where pert_matrix1_def: "pert_matrix1 == Abs_matrix o pert_infmatrix o Rep_matrix"
lemma combine_infmatrix_pert_infmatrix_matrix[simp]:
"f 0 0 = 0 ==> combine_infmatrix f (pert_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix B)) ∈ matrix"
unfolding matrix_def
using finite_subset[of _ "(nonzero_positions (pert_infmatrix (Rep_matrix A)))
∪ (nonzero_positions (pert_infmatrix (Rep_matrix B)))"] by simp_all
lemma pert_infmatrix_combine_infmatrix_matrix[simp]:
"f 0 0 = 0 ==> pert_infmatrix (combine_infmatrix f (Rep_matrix A)
(Rep_matrix B)) ∈ matrix"
proof (unfold matrix_def, simp, rule finite_imageD [of pert_inv])
let ?B = "nonzero_positions (pert_infmatrix (combine_infmatrix f
(Rep_matrix A) (Rep_matrix B)))"
assume f_0: "f (0::'b) (0::'c) = (0::'a)"
show "finite (pert_inv ` ?B)"
proof -
have "pert_inv` ?B ⊆ {i. f (Rep_matrix A (fst i) (snd i))
(Rep_matrix B (fst i) (snd i)) ≠ 0}"
unfolding pert_infmatrix_def
unfolding combine_infmatrix_def
unfolding image_def nonzero_positions_def
unfolding pert_inv_def if_def by force
with combine_infmatrix_matrix [of f] f_0 show ?thesis
unfolding matrix_def combine_infmatrix_def nonzero_positions_def
by (simp add: finite_subset)
qed
show "inj_on pert_inv ?B" unfolding inj_on_def pert_inv_def by auto
qed
lemma combine_diff_pert_matrix[simp]:
"f 0 0 = 0 ==> (combine_infmatrix f (diff_infmatrix
(combine_infmatrix f (Rep_matrix A) (Rep_matrix B)))
(pert_infmatrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B)))) ∈ matrix"
using diff_infmatrix_combine_infmatrix_matrix [of f]
using pert_infmatrix_combine_infmatrix_matrix [of f]
unfolding matrix_def
by (simp add: finite_subset [of _ "(nonzero_positions
(diff_infmatrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))))
∪ (nonzero_positions (pert_infmatrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))))"])
lemma combine_diff_pert_matrix_1 [simp]:
"f 0 0 = 0 ==> (combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A))) ∈ matrix"
unfolding matrix_def
by (simp add: finite_subset [of _ "(nonzero_positions (diff_infmatrix (Rep_matrix A)))
∪ (nonzero_positions (pert_infmatrix (Rep_matrix A)))"])
lemma combine_diff_pert_matrix_2 [simp]:
"f 0 0 = 0 ==> (combine_infmatrix f
(combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A)))
(combine_infmatrix f (diff_infmatrix (Rep_matrix B)) (pert_infmatrix (Rep_matrix B)))) ∈ matrix"
using combine_diff_pert_matrix_1 [of f A]
using combine_diff_pert_matrix_1 [of f B]
unfolding matrix_def
by (simp add: finite_subset [of _ "(nonzero_positions (combine_infmatrix f
(diff_infmatrix (Rep_matrix A)) (pert_infmatrix (Rep_matrix A))))
∪ (nonzero_positions (combine_infmatrix f (diff_infmatrix (Rep_matrix B))
(pert_infmatrix (Rep_matrix B))))"])
lemma combine_diff_pert_matrix_3 [simp]:
"f 0 0 = 0 ==> (diff_infmatrix (combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A)))) ∈ matrix"
proof (unfold matrix_def, simp, rule finite_imageD [of diff_inv])
let ?B = "nonzero_positions (diff_infmatrix (combine_infmatrix f
(diff_infmatrix (Rep_matrix A)) (pert_infmatrix (Rep_matrix A))))"
assume f_0: "f (0::'b) (0::'b) = (0::'a)"
show "inj_on diff_inv ?B" unfolding inj_on_def diff_inv_def by auto
show "finite (diff_inv `?B)"
proof -
have "diff_inv` ?B ⊆ {i. combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A)) (fst i) (snd i) ≠ 0}"
unfolding diff_infmatrix_def
unfolding pert_infmatrix_def
unfolding combine_infmatrix_def
unfolding image_def nonzero_positions_def
unfolding diff_inv_def
unfolding if_def by force
with combine_diff_pert_matrix_1 [of f] f_0
show ?thesis
unfolding matrix_def
unfolding nonzero_positions_def by (simp add: finite_subset)
qed
qed
lemma combine_diff_pert_matrix_4 [simp]:
"f 0 0 = 0 ==> (pert_infmatrix (combine_infmatrix f
(diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A)))) ∈ matrix"
proof (unfold matrix_def, simp, rule finite_imageD [of pert_inv])
let ?B = "nonzero_positions (pert_infmatrix (combine_infmatrix f
(diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A))))"
assume f_0: "f (0::'b) (0::'b) = (0::'a)"
show "inj_on pert_inv ?B" unfolding inj_on_def pert_inv_def by auto
show "finite (pert_inv `?B)"
proof -
have "pert_inv` ?B ⊆ {i. combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A)) (fst i) (snd i) ≠ 0}"
unfolding diff_infmatrix_def
unfolding pert_infmatrix_def
unfolding combine_infmatrix_def
unfolding image_def
unfolding nonzero_positions_def
unfolding pert_inv_def
unfolding if_def by force
with combine_diff_pert_matrix_1 [of f] f_0
show ?thesis unfolding matrix_def nonzero_positions_def by (simp add: finite_subset)
qed
qed
lemma combine_diff_pert_matrix_5 [simp]:
"f 0 0 = 0 ==> (combine_infmatrix f (diff_infmatrix (combine_infmatrix f
(diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A))))
(pert_infmatrix (combine_infmatrix
f (diff_infmatrix (Rep_matrix A)) (pert_infmatrix (Rep_matrix A))))) ∈ matrix"
using combine_diff_pert_matrix_3 [of f A]
using combine_diff_pert_matrix_4 [of f A]
unfolding matrix_def
by (simp add: finite_subset [of _
"(nonzero_positions (diff_infmatrix (combine_infmatrix f
(diff_infmatrix (Rep_matrix A)) (pert_infmatrix (Rep_matrix A)))))
∪ (nonzero_positions (pert_infmatrix (combine_infmatrix f
(diff_infmatrix (Rep_matrix A)) (pert_infmatrix (Rep_matrix A)))))"])
subsection{*Matrices as an instance of differential group with a perturbation.*}
lemma pert_matrix1_hom: shows "pert_matrix1 (A + B) = pert_matrix1 A + pert_matrix1 B"
unfolding plus_matrix_def combine_matrix_def pert_matrix1_def
proof (simp add: expand_fun_eq)
show "Abs_matrix (pert_infmatrix (combine_infmatrix op + (Rep_matrix A)
(Rep_matrix B))) =
Abs_matrix (combine_infmatrix op + (pert_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix B)))"
proof (rule Abs_matrix_inject2)
show "combine_infmatrix op + (pert_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix B)) ∈ matrix"
using combine_infmatrix_pert_infmatrix_matrix [of "op + :: 'a => 'a => 'a"]
by simp
show "pert_infmatrix (combine_infmatrix op + (Rep_matrix A)
(Rep_matrix B)) ∈ matrix"
using combine_infmatrix_pert_infmatrix_matrix [of "op + :: 'a => 'a => 'a"]
by simp
show " pert_infmatrix (combine_infmatrix op + (Rep_matrix A) (Rep_matrix B)) =
combine_infmatrix op + (pert_infmatrix (Rep_matrix A)) (pert_infmatrix (Rep_matrix B))"
unfolding combine_infmatrix_def pert_infmatrix_def
apply (rule ext)+ by auto
qed
qed
lemma pert_matrix1_twice:
shows "pert_matrix1 (pert_matrix1 A) = (0::('a::lordered_ring matrix))"
unfolding pert_matrix1_def by simp
lemma diff_matrix1_pert_matrix1_is_zero: "diff_matrix1 (pert_matrix1 A) = 0"
unfolding zero_matrix_def
unfolding diff_matrix1_def
unfolding pert_matrix1_def
apply auto
proof -
show "Abs_matrix (diff_infmatrix (pert_infmatrix (Rep_matrix A))) =
Abs_matrix (λj i. 0)"
proof (rule Abs_matrix_inject2)
show "(λ(j::nat) i::nat. 0::'a) ∈ matrix"
unfolding zero_fun_def
unfolding matrix_def
unfolding nonzero_positions_def by auto
show "diff_infmatrix (pert_infmatrix (Rep_matrix A)) ∈ matrix"
using diff_infmatrix_is_matrix [OF pert_infmatrix_matrix [of A]] .
show "diff_infmatrix (pert_infmatrix (Rep_matrix A)) = (λj i. 0)"
unfolding pert_infmatrix_def
unfolding diff_infmatrix_def
apply (rule ext)+ by arith
qed
qed
lemma pert_matrix1_diff_matrix1_is_zero: "pert_matrix1 (diff_matrix1 A) = 0"
unfolding zero_matrix_def
unfolding diff_matrix1_def
unfolding pert_matrix1_def
apply auto
proof -
show "Abs_matrix (pert_infmatrix (diff_infmatrix (Rep_matrix A))) =
Abs_matrix (λj i. 0)"
proof (rule Abs_matrix_inject2)
show "(λ(j::nat) i::nat. 0::'a) ∈ matrix"
unfolding zero_fun_def
unfolding matrix_def
unfolding nonzero_positions_def by auto
show "pert_infmatrix (diff_infmatrix (Rep_matrix A)) ∈ matrix"
using pert_infmatrix_is_matrix [OF diff_infmatrix_matrix [of A]] .
show "pert_infmatrix (diff_infmatrix (Rep_matrix A)) = (λj i. 0)"
unfolding pert_infmatrix_def
unfolding diff_infmatrix_def
apply (rule ext)+ by arith
qed
qed
instantiation matrix :: (lordered_ring) diff_group_add_pert
begin
definition pert_matrix_def: "pert A == pert_matrix1 A"
instance
proof
fix A B :: "'a matrix"
show "δ (A + B) = δ A + δ B"
unfolding pert_matrix_def using pert_matrix1_hom [of A B] by simp
next
show "diff_group_add op - uminus (0::'a matrix) op + (λx::'a matrix. d x + δ x)"
proof (intro_locales, unfold diff_group_add_axioms_def,
intro conjI, rule allI, rule allI)
fix A B :: "'a matrix"
show "d (A + B) + δ (A + B) = d A + δ A + (d B + δ B)"
unfolding diff_matrix_def unfolding diff_matrix1_hom [of A B]
unfolding pert_matrix_def unfolding pert_matrix1_hom [of A B] by simp
next
show "(λA::'a matrix. d A + δ A) o (λA::'a matrix. d A + δ A) = (λA::'a matrix. 0)"
proof (simp add: expand_fun_eq, rule allI)
fix A :: "'a matrix"
show "d (d A + δ A) + δ (d A + δ A) = 0"
unfolding diff_matrix_def
unfolding diff_matrix1_hom
unfolding pert_matrix_def
unfolding pert_matrix1_hom
unfolding diff_matrix1_twice [of A]
unfolding pert_matrix1_twice [of A]
unfolding diff_matrix1_pert_matrix1_is_zero
unfolding pert_matrix1_diff_matrix1_is_zero by simp
qed
qed
qed
end
subsection{*Definition of the homotopy operator $h$.*}
definition hom_oper_infmatrix :: "'a::{zero} infmatrix => 'a infmatrix"
where hom_oper_infmatrix_def : "hom_oper_infmatrix A =
(%i::nat. %j::nat. if (j = 0) then 0 else (if ((i + j) mod (2::nat) = 0) then (0::'a)
else (A i (j - 1))))"
definition hom_oper_inv :: "(nat × nat) => (nat × nat)"
where hom_oper_inv_def : "hom_oper_inv pos = (fst pos, (snd pos) - 1)"
lemma hom_oper_infmatrix_finite[simp]:
shows "finite (nonzero_positions (hom_oper_infmatrix (Rep_matrix x)))"
proof (rule finite_imageD [of hom_oper_inv])
let ?B = "nonzero_positions (hom_oper_infmatrix (Rep_matrix x))"
show "finite (hom_oper_inv ` ?B)"
proof (rule finite_subset [of _ "{i. Rep_matrix x (fst i) (snd i) ≠ 0}"])
show "hom_oper_inv` ?B ⊆ {i. Rep_matrix x (fst i) (snd i) ≠ 0}"
unfolding hom_oper_infmatrix_def
unfolding image_def
unfolding nonzero_positions_def
unfolding hom_oper_inv_def
unfolding if_def by force
show "finite {i. Rep_matrix x (fst i) (snd i) ≠ 0}"
using finite_nonzero_positions [of x]
unfolding nonzero_positions_def [of "Rep_matrix x"] .
qed
show "inj_on hom_oper_inv ?B"
proof (unfold inj_on_def hom_oper_inv_def, auto)
fix a b c :: nat
assume "(a, b) ∈ nonzero_positions (hom_oper_infmatrix (Rep_matrix x))"
and "(a, c) ∈ nonzero_positions (hom_oper_infmatrix (Rep_matrix x))"
then have b_ge_1: "1 ≤ b" and c_ge_1: "1 ≤ c"
unfolding nonzero_positions_def
unfolding hom_oper_infmatrix_def
unfolding if_def by force+
assume "b - Suc (0::nat) = c - Suc (0::nat)"
with eq_diff_iff [OF b_ge_1 c_ge_1] show "b = c" by simp
qed
qed
lemma hom_oper_infmatrix_matrix:
shows "(hom_oper_infmatrix (Rep_matrix (x::'a::zero matrix))) ∈ matrix"
by (unfold matrix_def) (simp add: hom_oper_infmatrix_finite)
lemma hom_oper_infmatrix_closed[simp]:
"Rep_matrix (Abs_matrix (hom_oper_infmatrix (Rep_matrix x))) = hom_oper_infmatrix (Rep_matrix x)"
using Abs_matrix_inverse [OF hom_oper_infmatrix_matrix [of x]] .
lemma hom_oper_infmatrix_is_matrix: assumes as: "A ∈ matrix"
shows "hom_oper_infmatrix A ∈ matrix"
unfolding matrix_def
unfolding mem_Collect_eq
proof (rule finite_imageD [of hom_oper_inv])
let ?B = "nonzero_positions (hom_oper_infmatrix A)"
show "finite (hom_oper_inv ` ?B)"
proof (rule finite_subset [of _ "{i. A (fst i) (snd i) ≠ 0}"])
show "hom_oper_inv` ?B ⊆ {i. A (fst i) (snd i) ≠ 0}"
unfolding image_def
unfolding hom_oper_inv_def
unfolding hom_oper_infmatrix_def
unfolding if_def
unfolding nonzero_positions_def by force
show "finite {i::nat × nat. A (fst i) (snd i) ≠ (0::'a)}"
using as
unfolding matrix_def
unfolding nonzero_positions_def
unfolding mem_Collect_eq .
qed
show "inj_on hom_oper_inv ?B"
proof (unfold inj_on_def hom_oper_inv_def, auto)
fix a b c :: nat
assume "(a, b) ∈ nonzero_positions (hom_oper_infmatrix A)"
and "(a, c) ∈ nonzero_positions (hom_oper_infmatrix A)"
then have b_ge_1: "1 ≤ b" and c_ge_1: "1 ≤ c"
unfolding nonzero_positions_def
unfolding hom_oper_infmatrix_def
unfolding if_def by force+
assume "b - Suc (0::nat) = c - Suc (0::nat)"
with eq_diff_iff [OF b_ge_1 c_ge_1] show "b = c" by simp
qed
qed
definition hom_oper_matrix1 :: "'a::lordered_ring matrix => 'a matrix"
where hom_oper_matrix1_def:
"hom_oper_matrix1 = Abs_matrix o hom_oper_infmatrix o Rep_matrix"
lemma hom_oper_infmatrix_twice [simp]:
"hom_oper_infmatrix (hom_oper_infmatrix A) = (Rep_matrix 0)"
unfolding hom_oper_infmatrix_def
apply (rule ext)+
apply (auto simp add: Rep_matrix_inject) by arith
lemma combine_infmatrix_hom_oper_infmatrix_matrix[simp]:
"f 0 0 = 0 ==> combine_infmatrix f (hom_oper_infmatrix (Rep_matrix A))
(hom_oper_infmatrix (Rep_matrix B)) ∈ matrix"
unfolding matrix_def
using finite_subset[of _ "(nonzero_positions (hom_oper_infmatrix (Rep_matrix A)))
∪ (nonzero_positions (hom_oper_infmatrix (Rep_matrix B)))"]
by simp
lemma hom_oper_infmatrix_combine_infmatrix_matrix[simp]:
"f 0 0 = 0 ==> hom_oper_infmatrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B)) ∈ matrix"
proof (unfold matrix_def, simp, rule finite_imageD [of hom_oper_inv])
let ?B = "nonzero_positions (hom_oper_infmatrix (combine_infmatrix f (Rep_matrix A)
(Rep_matrix B)))"
assume f_0: "f (0::'b) (0::'c) = (0::'a)"
show "finite (hom_oper_inv ` ?B)"
proof (rule finite_subset [of _ "{i. f (Rep_matrix A (fst i) (snd i))
(Rep_matrix B (fst i) (snd i)) ≠ 0}"])
show "hom_oper_inv` ?B ⊆ {i. f (Rep_matrix A (fst i) (snd i)) (Rep_matrix B (fst i) (snd i)) ≠ 0}"
unfolding hom_oper_infmatrix_def
unfolding combine_infmatrix_def
unfolding image_def
unfolding nonzero_positions_def
unfolding hom_oper_inv_def
unfolding if_def by force
show "finite {i. f (Rep_matrix A (fst i) (snd i))
(Rep_matrix B (fst i) (snd i)) ≠ 0}"
using combine_infmatrix_matrix [of f] f_0
unfolding matrix_def
unfolding combine_infmatrix_def
unfolding nonzero_positions_def
unfolding mem_Collect_eq .
qed
show "inj_on hom_oper_inv ?B"
proof (unfold inj_on_def hom_oper_inv_def, auto)
fix a b c :: nat
assume "(a, b) ∈ ?B" and "(a, c) ∈ ?B"
then have b_ge_1: "1 ≤ b" and c_ge_1: "1 ≤ c"
unfolding nonzero_positions_def
unfolding hom_oper_infmatrix_def
unfolding if_def by force+
assume "b - Suc (0::nat) = c - Suc (0::nat)"
with eq_diff_iff [OF b_ge_1 c_ge_1] show "b = c" by simp
qed
qed
subsection{*Matrices as an instance of differential group with a homotopy operator.*}
text{*Matrices with the given operations for differential,
perturbation and homotopy operator are an instance of the
type class representing differential groups with a perturbation and a homotpy operator:*}
lemma hom_oper_matrix1_hom:
"hom_oper_matrix1 (A + B) = hom_oper_matrix1 A + hom_oper_matrix1 B"
unfolding plus_matrix_def
unfolding combine_matrix_def
unfolding hom_oper_matrix1_def
apply simp
proof -
show "Abs_matrix (hom_oper_infmatrix (combine_infmatrix op + (Rep_matrix A)
(Rep_matrix B))) =
Abs_matrix (combine_infmatrix op + (hom_oper_infmatrix (Rep_matrix A))
(hom_oper_infmatrix (Rep_matrix B)))"
proof (rule Abs_matrix_inject2)
show "combine_infmatrix op + (hom_oper_infmatrix (Rep_matrix A))
(hom_oper_infmatrix (Rep_matrix B)) ∈ matrix"
using combine_infmatrix_hom_oper_infmatrix_matrix [of "op + :: 'a => 'a => 'a"]
by simp
show "hom_oper_infmatrix (combine_infmatrix op + (Rep_matrix A) (Rep_matrix B)) ∈ matrix"
using hom_oper_infmatrix_combine_infmatrix_matrix [of "op + :: 'a => 'a => 'a"]
by simp
show "hom_oper_infmatrix (combine_infmatrix op + (Rep_matrix A) (Rep_matrix B)) =
combine_infmatrix op + (hom_oper_infmatrix (Rep_matrix A))
(hom_oper_infmatrix (Rep_matrix B))"
unfolding combine_infmatrix_def
unfolding hom_oper_infmatrix_def by (rule ext)+ simp
qed
qed
lemma hom_oper_matrix1_twice:
shows "hom_oper_matrix1 (hom_oper_matrix1 A) = (0::('a::lordered_ring matrix))"
unfolding hom_oper_matrix1_def by simp
instantiation matrix :: (lordered_ring) diff_group_add_pert_hom
begin
definition hom_oper_matrix_def: "hom_oper A == hom_oper_matrix1 A"
instance
proof
fix A B :: "'a matrix"
show "hom_oper o hom_oper = (λx::'a matrix. 0)"
apply (rule ext)
unfolding o_apply
unfolding hom_oper_matrix_def
using hom_oper_matrix1_twice by auto
next
fix A B:: "'a matrix"
show "h (A + B) = h A + h B"
unfolding hom_oper_matrix_def
using hom_oper_matrix1_hom [of A B].
qed
end
subsection{*Local nilpotency condition of the previous definitions.*}
lemma hom_oper_closed:
shows "Rep_matrix o Abs_matrix o hom_oper_infmatrix o Rep_matrix
= hom_oper_infmatrix o Rep_matrix"
by (simp add: expand_fun_eq)
lemma pert_infmatrix_hom_oper_infmatrix_finite[simp]:
shows "finite (nonzero_positions (pert_infmatrix (hom_oper_infmatrix (Rep_matrix x))))"
proof (rule finite_imageD [of "pert_inv"])
let ?B = "nonzero_positions (pert_infmatrix (hom_oper_infmatrix (Rep_matrix x)))"
show "finite ((pert_inv) ` ?B)"
proof -
have "(pert_inv)` ?B ⊆ {i. hom_oper_infmatrix (Rep_matrix x) (fst i) (snd i) ≠ 0}"
unfolding pert_infmatrix_def
unfolding image_def
unfolding nonzero_positions_def
unfolding pert_inv_def
unfolding if_def by force
from finite_subset [OF this] hom_oper_infmatrix_finite [of x] show ?thesis
unfolding nonzero_positions_def [of "(hom_oper_infmatrix (Rep_matrix x))"]
by simp
qed
show "inj_on pert_inv ?B"
unfolding inj_on_def
unfolding pert_inv_def by auto
qed
lemma pert_infmatrix_hom_oper_infmatrix_matrix:
shows "(pert_infmatrix (hom_oper_infmatrix (Rep_matrix (x::'a::zero matrix))))
∈ matrix"
unfolding matrix_def
unfolding mem_Collect_eq
using pert_infmatrix_hom_oper_infmatrix_finite .
lemma pert_infmatrix_hom_oper_infmatrix_closed[simp]:
shows "Rep_matrix (Abs_matrix (pert_infmatrix (hom_oper_infmatrix (Rep_matrix A)))) =
pert_infmatrix (hom_oper_infmatrix (Rep_matrix A))"
using Abs_matrix_inverse [OF pert_infmatrix_hom_oper_infmatrix_matrix [of A]] .
lemma hom_oper_infmatrix_pert_infmatrix_finite[simp]:
shows "finite (nonzero_positions (hom_oper_infmatrix (pert_infmatrix (Rep_matrix x))))"
proof (rule finite_imageD [of "hom_oper_inv"])
let ?B = "nonzero_positions (hom_oper_infmatrix (pert_infmatrix (Rep_matrix x)))"
show "finite ((hom_oper_inv) ` ?B)"
proof -
have "(hom_oper_inv)` ?B ⊆ {i. pert_infmatrix (Rep_matrix x) (fst i) (snd i) ≠ 0}"
unfolding hom_oper_infmatrix_def
unfolding image_def
unfolding nonzero_positions_def
unfolding hom_oper_inv_def
unfolding if_def by force
from finite_subset [OF this] pert_infmatrix_finite [of x]
show ?thesis
unfolding nonzero_positions_def [of "(pert_infmatrix (Rep_matrix x))"]
by simp
qed
show "inj_on hom_oper_inv ?B"
proof (unfold inj_on_def hom_oper_inv_def, auto)
fix a b c :: nat
assume "(a, b) ∈ nonzero_positions (hom_oper_infmatrix (pert_infmatrix (Rep_matrix x)))"
and "(a, c) ∈ nonzero_positions (hom_oper_infmatrix (pert_infmatrix (Rep_matrix x)))"
then have b_ge_1: "1 ≤ b" and c_ge_1: "1 ≤ c"
unfolding nonzero_positions_def
unfolding pert_infmatrix_def
unfolding hom_oper_infmatrix_def
unfolding if_def by force+
assume "b - Suc (0::nat) = c - Suc (0::nat)"
with eq_diff_iff [OF b_ge_1 c_ge_1] show "b = c" by simp
qed
qed
lemma hom_oper_infmatrix_pert_infmatrix_matrix:
shows "(hom_oper_infmatrix (pert_infmatrix (Rep_matrix (x::'a::zero matrix))))
∈ matrix"
unfolding matrix_def
unfolding mem_Collect_eq
using hom_oper_infmatrix_pert_infmatrix_finite .
lemma hom_oper_infmatrix_pert_infmatrix_closed[simp]:
shows "Rep_matrix (Abs_matrix (hom_oper_infmatrix (pert_infmatrix (Rep_matrix A)))) =
hom_oper_infmatrix (pert_infmatrix (Rep_matrix A))"
using Abs_matrix_inverse [OF hom_oper_infmatrix_pert_infmatrix_matrix [of A]] .
lemma f_1_n: shows "f ((f^n) a) = (f^(n + 1)) a"
using sym [OF funpow_add [of f 1 n]] by auto
text{*This is the crucial lemma to prove the local nilpotency condition;
the result states that there is
no infinite strictly descending chain of natural numbers.
Applied to matrices, it states that there is
no infinite descending path across a matrix of finite dimension, and thus,
being @{term [locale=diff_group_add_pert_hom] "α = (pert o hom_oper)"} strictly
decreasing with repect to the dimension of matrices, the local nilpotency condition holds.*}
lemma infinite_descending_chain_false:
fixes g :: "nat => nat"
assumes n_inf_decr: "!!n. g (Suc n) < g n" shows "False"
proof -
obtain a where g0_finite: "a = g (0::nat)" by simp
have less_relat: "!!n::nat. g (Suc n) < a - n"
proof (induct_tac n)
fix n::nat
show "g (Suc 0) < a - 0" unfolding g0_finite using n_inf_decr [of 0] by simp
next
fix n::nat assume hypo: "g (Suc n) < a - n"
show "g (Suc (Suc n)) < a - (Suc n)"
using hypo n_inf_decr [of "Suc n"] by arith
qed
from less_relat [of a] have "g (Suc a) < (0::nat)" by arith
then show False by arith
qed
text{*Making use of the previous result, if the number of rows is strictly decreasing,
finally matrix @{term "0::'a::zero matrix"} is reached.*}
lemma P_strict_decr:
fixes f :: "'a::lordered_ring matrix => 'a matrix"
and P :: "'a matrix => nat"
assumes P_decr: "!!A. A ≠ 0 ==> (P (f A) < P A)" and P_0: "P 0 = 0"
shows "∃n::nat. P ((f^n) A) = 0"
proof -
have decr_step: "!!n. ((f^n) A) ≠ 0 ==> P ((f^(n+1)) A) < P ((f^n) A)"
proof -
fix n::nat
show "((f^n) A) ≠ 0 ==> P ((f^(n+1)) A) < P ((f^n) A)"
proof (induct n)
case 0
assume "(f^(0::nat)) A ≠ 0"
then have A_nz: "A ≠ 0"
unfolding funpow.simps (1) [of f]
unfolding id_apply .
show ?case using P_decr [OF A_nz] by simp
next
case Suc fix n :: nat
assume hypo: "(f^n) A ≠ 0 ==> P ((f^(n+1)) A) < P ((f^n) A)"
and not_zero: "((f^(Suc n)) A) ≠ 0"
show "P ((f^((Suc n)+1)) A) < P ((f^(Suc n)) A)"
unfolding sym [OF f_1_n [of f "Suc m" A]]
using P_decr [OF not_zero] by simp
qed
qed
let ?P = "P A"
have finite: "finite {..?P}" using finite_atMost [of "P A"] .
from finite decr_step show ?thesis
proof (cases "∃n. ((f^n) A) = 0")
case True show ?thesis
proof -
from True obtain n where fn_0: "((f^n) A) = 0" by auto
show ?thesis apply (rule exI [of _ n])
unfolding fn_0 unfolding P_0 ..
qed
next
case False show ?thesis
proof (rule ccontr)
let ?g = "(λn::nat. P ((f^n) A))"
have "!!n::nat. P ((f^(n+1)) A) < P ((f^n) A)"
using decr_step and False by simp
then have infinite_descending_chain: "!!n::nat. ?g (Suc n) < ?g n" by simp
with infinite_descending_chain_false [of ?g] show False by simp
qed
qed
qed
lemma nrows_strict_decr:
fixes f :: "'a::lordered_ring matrix => 'a matrix"
assumes nrows_decr: "!!A. A ≠ 0 ==> (nrows (f A) < nrows A)"
shows "∃n::nat. nrows ( (f^n) A) = 0"
proof (rule P_strict_decr [of nrows f A])
show "!!A. A ≠ 0 ==> (nrows (f A) < nrows A)" using nrows_decr .
show "nrows 0 = 0" by simp
qed
lemma ncols_strict_decr:
fixes f :: "'a::lordered_ring matrix => 'a matrix"
assumes ncols_decr: "!!A. A ≠ 0 ==> (ncols (f A) < ncols A)"
shows "∃n::nat. ncols ( (f^n) A) = 0"
proof (rule P_strict_decr [of ncols f A])
show "!!A. A ≠ 0 ==> (ncols (f A) < ncols A)" using ncols_decr .
show "ncols 0 = 0" by simp
qed
lemma nonzero_empty_set:
shows "nonzero_positions (Rep_matrix (0::'a::lordered_ring matrix)) = {}"
unfolding nonzero_positions_def by simp
lemma Rep_matrix_inject2:
assumes R_A_B: "Rep_matrix A = Rep_matrix B"
shows "A = B"
using Rep_matrix_inject [of A B] R_A_B ..
lemma nonzero_imp_zero_matrix:
assumes nz_p: "nonzero_positions (Rep_matrix (A::'a::lordered_ring matrix)) = {}"
shows "A = 0"
proof (rule Rep_matrix_inject2)
show "Rep_matrix A = Rep_matrix 0"
proof -
from nz_p have "∀a b. Rep_matrix A a b = 0"
unfolding nonzero_positions_def by simp
then show "Rep_matrix A = Rep_matrix 0"
unfolding expand_fun_eq
unfolding Rep_zero_matrix_def .
qed
qed
lemma nrows_zero_impl_zero:
assumes nrows_0: "nrows (A::'a::lordered_ring matrix) = (0::nat)"
shows "A = 0"
proof (rule nonzero_imp_zero_matrix)
show "nonzero_positions (Rep_matrix A) = {}"
proof (rule ccontr)
assume ne: "nonzero_positions (Rep_matrix A) ≠ {}"
then have "nrows A > 0"
unfolding nrows_def by simp
with nrows_0 show False by arith
qed
qed
lemma ncols_zero_impl_zero:
assumes ncols_0: "ncols (A::'a::lordered_ring matrix) = (0::nat)"
shows "A = 0"
proof (rule nonzero_imp_zero_matrix)
show "nonzero_positions (Rep_matrix A) = {}"
proof (rule ccontr)
assume ne: "nonzero_positions (Rep_matrix A) ≠ {}"
then have "ncols A > 0"
unfolding ncols_def by simp
with ncols_0 show False by arith
qed
qed
lemma not_zero_impl_exist:
assumes A_not_null: "(A::'a::lordered_ring matrix) ≠ 0"
shows "∃m n::nat. Rep_matrix A m n ≠ 0"
proof (rule ccontr)
assume neg: "¬ (∃m n::nat. Rep_matrix A m n ≠ 0)"
then have "∀m n. Rep_matrix A m n = 0" by auto
with nonzero_imp_zero_matrix [of A] nonzero_positions_def
have "A = 0" by auto
with A_not_null show False by simp
qed
corollary not_zero_impl_nonzero_pos:
assumes A_not_null: "(A::'a::lordered_ring matrix) ≠ 0"
shows "nonzero_positions (Rep_matrix A) ≠ {}"
using not_zero_impl_exist [OF A_not_null]
unfolding nonzero_positions_def [of "Rep_matrix A"] by auto
corollary not_zero_impl_nrows_g_0:
assumes A_not_null: "(A::'a::lordered_ring matrix) ≠ 0"
shows "nrows A > 0"
using not_zero_impl_exist [OF A_not_null]
unfolding nrows_def
unfolding nonzero_positions_def by auto
corollary not_zero_impl_ncols_g_0:
assumes A_not_null: "(A::'a::lordered_ring matrix) ≠ 0"
shows "ncols A > 0"
using not_zero_impl_exist [OF A_not_null]
unfolding ncols_def
unfolding nonzero_positions_def by auto
lemma hom_oper_nonzero_positions:
assumes a_b_1: "(a, b + 1) ∈ nonzero_positions (Rep_matrix A)"
and b_n_0: "(0::nat) < b"
and ab_even: "(a + b) mod 2 ≠ (0::nat)"
shows "(a, b + 2) ∈ nonzero_positions (hom_oper_infmatrix (Rep_matrix A))"
using a_b_1 b_n_0 ab_even
unfolding hom_oper_infmatrix_def
unfolding nonzero_positions_def by auto
lemma pert_nonzero_positions:
assumes a_b_1: "(a + 1, b) ∈ nonzero_positions (Rep_matrix A)"
and ab_pair: "(a + b) mod 2 = (0::nat)"
shows "(a, b) ∈ nonzero_positions (pert_infmatrix (Rep_matrix A))"
using a_b_1 ab_pair
unfolding pert_infmatrix_def
unfolding nonzero_positions_def by auto
lemma pert_nonzero_incr:
assumes ab_nonzero: "(a, b) ∈ nonzero_positions (pert_infmatrix (Rep_matrix A))"
shows "(a + 1, b) ∈ nonzero_positions (Rep_matrix A)"
proof (rule ccontr)
assume contr: "(a + (1::nat), b) ∉ nonzero_positions (Rep_matrix A)"
then have Rep_m: "Rep_matrix A (a + 1) b = 0"
unfolding nonzero_positions_def unfolding mem_Collect_eq by simp
then have "pert_infmatrix (Rep_matrix A) a b = 0"
unfolding pert_infmatrix_def by simp
with ab_nonzero show False
unfolding nonzero_positions_def
unfolding mem_Collect_eq by simp
qed
lemma pert_hom_oper_nonzero_ncols_g_1:
assumes ab_nonzero: "(a, b) ∈ nonzero_positions
(pert_infmatrix (hom_oper_infmatrix (Rep_matrix A)))"
shows "1 ≤ b"
proof (rule ccontr)
assume contr: "¬ (1::nat) ≤ b" then have b_0: "b = 0" by arith
have Rep_m: "(pert_infmatrix (hom_oper_infmatrix (Rep_matrix A))) a b = 0"
unfolding hom_oper_infmatrix_def
unfolding pert_infmatrix_def using b_0 by auto
with ab_nonzero show False unfolding nonzero_positions_def unfolding mem_Collect_eq
by simp
qed
lemma pert_hom_oper_nonzero_incr_rows:
assumes ab_nonzero: "(a, b) ∈ nonzero_positions
(pert_infmatrix (hom_oper_infmatrix (Rep_matrix A)))"
shows "(a + 1, b - 1) ∈ nonzero_positions (Rep_matrix A)"
proof (rule ccontr)
assume contr: "(a + 1, b - 1) ∉ nonzero_positions (Rep_matrix A)"
then have Rep_m: "Rep_matrix A (a + 1) (b - 1) = 0"
unfolding nonzero_positions_def by simp
have "pert_infmatrix (hom_oper_infmatrix (Rep_matrix A)) a b = 0"
unfolding hom_oper_infmatrix_def
unfolding pert_infmatrix_def using Rep_m by auto
with ab_nonzero show False unfolding nonzero_positions_def unfolding mem_Collect_eq
by simp
qed
lemma hom_oper_pert_nonzero_incr_rows:
assumes ab_nonzero: "(a, b) ∈ nonzero_positions
(hom_oper_infmatrix (pert_infmatrix (Rep_matrix A)))"
shows "(a + 1, b - 1) ∈ nonzero_positions (Rep_matrix A)"
proof (rule ccontr)
assume contr: "(a + 1, b - 1) ∉ nonzero_positions (Rep_matrix A)"
then have Rep_m: "Rep_matrix A (a + 1) (b - 1) = 0"
unfolding nonzero_positions_def by simp
have "hom_oper_infmatrix (pert_infmatrix (Rep_matrix A)) a b = 0"
unfolding hom_oper_infmatrix_def
unfolding pert_infmatrix_def using Rep_m by auto
with ab_nonzero
show False
unfolding nonzero_positions_def
unfolding mem_Collect_eq
by simp
qed
lemma Max_A_B:
assumes exist: "∃m>Max B. m ∈ A"
and fin_A: "finite A" and fin_B: "finite B"shows "Max B < Max A"
proof -
from exist obtain m where m_prop: "m ∈ A ∧ (m>Max B)" by auto
from m_prop Max_ge [OF fin_A, of m] have "m ≤ Max A" by auto
with m_prop show "Max B < Max A" by auto
qed
lemma nrows_pert_decre:
assumes A_not_null: "(A::'a::lordered_ring matrix) ≠ 0"
shows "nrows ( (- (pert_matrix1)) A) < nrows A"
(is "nrows ((- ?f) A) < nrows A")
proof (cases "(- ?f) A = 0")
case True
have fA_0: "nrows ((- ?f) A) = (0::nat)"
unfolding True
using zero_matrix_def_nrows .
with not_zero_impl_nrows_g_0 [OF A_not_null] show ?thesis by arith
next
case False
show "nrows ((- ?f) A) < nrows A"
proof -
from not_zero_impl_nonzero_pos [OF A_not_null]
have nrows_A: "nrows A = Suc (Max (fst ` nonzero_positions (Rep_matrix A)))"
unfolding nrows_def by simp
from not_zero_impl_nonzero_pos [OF False]
have "nrows ((- ?f) A) = Suc (Max (fst ` nonzero_positions (Rep_matrix ((- ?f) A))))"
unfolding nrows_def by simp
also from nonzero_positions_minus_f [of ?f A]
have "… = Suc (Max (fst ` nonzero_positions (Rep_matrix (?f A))))"
by simp
also have "… = Suc (Max (fst ` nonzero_positions ((pert_infmatrix o Rep_matrix) A)))"
unfolding pert_matrix1_def by simp
finally
have nrows_fA: "nrows ((- ?f) A) =
Suc (Max (fst ` nonzero_positions ((pert_infmatrix o Rep_matrix) A)))" by simp
have Max_l: "Max (fst ` nonzero_positions ((pert_infmatrix o Rep_matrix) A))
< Max (fst ` nonzero_positions (Rep_matrix A))"
proof (rule Max_A_B)
let ?n = "Max (fst ` nonzero_positions ((pert_infmatrix o Rep_matrix) A))"
show "∃m>?n .(m ∈ (fst ` nonzero_positions (Rep_matrix A)))"
proof (rule exI [of _ "Suc ?n"], intro conjI, simp)
have "nonzero_positions (Rep_matrix ((- ?f) A)) ≠ {}"
using not_zero_impl_nonzero_pos [OF False] .
with nonzero_positions_minus_f [of ?f A]
have non_empty: "nonzero_positions ((pert_infmatrix o Rep_matrix) A) ≠ {}"
unfolding pert_matrix1_def by simp
from Max_in [OF finite_imageI [OF pert_infmatrix_finite, of "fst" A]] non_empty
have Max_in_set: "?n ∈ (fst ` nonzero_positions ((pert_infmatrix o Rep_matrix) A))"
unfolding image_def by auto
from Max_in_set obtain a
where A_a_n_0: "(pert_infmatrix (Rep_matrix A)) ?n a ≠ 0"
unfolding nonzero_positions_def image_def by auto
with pert_nonzero_incr [of ?n a]
have "(Suc ?n, a) ∈ nonzero_positions (Rep_matrix A)"
unfolding nonzero_positions_def image_def by auto
then show "Suc ?n ∈ fst ` nonzero_positions (Rep_matrix A)"
unfolding image_def [of fst] by force
qed
show "finite (fst ` nonzero_positions (Rep_matrix A))"
using finite_imageI [OF finite_nonzero_positions [of A], of fst] .
show "finite (fst ` nonzero_positions ((pert_infmatrix o Rep_matrix) A))"
using finite_imageI [OF pert_infmatrix_finite [of A], of fst]
unfolding o_apply .
qed
with nrows_A nrows_fA show ?thesis by simp
qed
qed
lemma nrows_pert_hom_oper_decre:
assumes A_not_null: "(A::'a::lordered_ring matrix) ≠ 0"
shows "nrows ((- (pert_matrix1 o hom_oper_matrix1)) A) < nrows A"
(is "nrows ((- ?f) A) < nrows A")
proof (cases "(- ?f) A = 0")
case True
have fA_0: "nrows ((- ?f) A) = (0::nat)"
unfolding True
using zero_matrix_def_nrows .
with not_zero_impl_nrows_g_0 [OF A_not_null]
show ?thesis by arith
next
case False
show "nrows ((- ?f) A) < nrows A"
proof -
have nrows_A: "nrows A = Suc (Max (fst ` nonzero_positions (Rep_matrix A)))"
using not_zero_impl_nonzero_pos [OF A_not_null]
unfolding nrows_def by simp
have "nrows ((- ?f) A) = Suc (Max (fst ` nonzero_positions (Rep_matrix ((- ?f) A))))"
using not_zero_impl_nonzero_pos [OF False]
unfolding nrows_def by simp
also have "… = Suc (Max (fst ` nonzero_positions (Rep_matrix (?f A))))"
unfolding sym [OF nonzero_positions_minus_f [of ?f A]] ..
also have "… = Suc (Max (fst ` nonzero_positions (((
pert_infmatrix o hom_oper_infmatrix) o Rep_matrix) A)))"
unfolding pert_matrix1_def hom_oper_matrix1_def by simp
finally have nrows_fA: "nrows ((- ?f) A) =
Suc (Max (fst ` nonzero_positions (((pert_infmatrix
o hom_oper_infmatrix) o Rep_matrix) A)))"
by simp
have Max_l: "(Max (fst ` nonzero_positions (Rep_matrix (?f A))))
< Max (fst ` nonzero_positions (Rep_matrix A))"
proof (rule Max_A_B)
let ?n = "Max (fst ` nonzero_positions (Rep_matrix (?f A)))"
show "∃m>?n .(m ∈ (fst ` nonzero_positions (Rep_matrix A)))"
proof (rule exI [of _ "Suc ?n"], intro conjI, simp)
have non_empty: "nonzero_positions (((pert_infmatrix
o hom_oper_infmatrix) o Rep_matrix) A) ≠ {}"
using nonzero_positions_minus_f [of ?f A]
using not_zero_impl_nonzero_pos [OF False]
unfolding pert_matrix1_def
unfolding hom_oper_matrix1_def by simp
have Max_in_set:
"?n ∈ (fst ` nonzero_positions (((pert_infmatrix
o hom_oper_infmatrix) o Rep_matrix) A))"
using Max_in [OF finite_imageI
[OF pert_infmatrix_hom_oper_infmatrix_finite, of "fst" A]]
using non_empty
unfolding image_def
unfolding pert_matrix1_def hom_oper_matrix1_def
by auto
from Max_in_set obtain a
where A_a_n_0: "(pert_infmatrix (hom_oper_infmatrix (Rep_matrix A))) ?n a ≠ 0"
unfolding nonzero_positions_def image_def by auto
with pert_hom_oper_nonzero_incr_rows [of ?n a]
have "(Suc ?n, a - 1) ∈ nonzero_positions (Rep_matrix A)"
unfolding nonzero_positions_def image_def by auto
then show "Suc ?n ∈ fst ` nonzero_positions (Rep_matrix A)"
unfolding image_def [of fst] by force
qed
show "finite (fst ` nonzero_positions (Rep_matrix A))"
using finite_imageI [OF finite_nonzero_positions [of A], of fst] .
show "finite (fst ` nonzero_positions (Rep_matrix ((pert_matrix1 o hom_oper_matrix1) A)))"
unfolding o_apply
using finite_imageI by simp
qed
with nrows_A nrows_fA show ?thesis unfolding pert_matrix1_def hom_oper_matrix1_def by simp
qed
qed
corollary nrows_alpha_decre:
assumes A_not_null: "(A::'a::lordered_ring matrix) ≠ 0"
shows "nrows (α A) < nrows A"
using nrows_pert_hom_oper_decre [OF A_not_null]
unfolding α_def
unfolding pert_matrix_def
unfolding hom_oper_matrix_def
unfolding fun_Compl_def
unfolding o_apply .
subsection{*Matrices as an instance of differential
group satisfying the local nilpotency condition.*}
text{*With the previous results, we can finally prove that matrices are an instance
of differential group with a perturbation and a homotpy operator that additionally
satisfies the local nilpotency condition.*}
instantiation matrix :: (lordered_ring) diff_group_add_pert_hom_bound_exist
begin
lemma α_matrix_definition: "α = - (pert_matrix1 o hom_oper_matrix1)"
unfolding α_def
unfolding fun_Compl_def
unfolding o_apply
unfolding hom_oper_matrix_def
unfolding pert_matrix_def ..
instance
proof (default, rule allI)
fix A :: "'a matrix"
show "∃n::nat. ((α::'a matrix => 'a matrix)^ n) A = 0"
proof (cases "A = 0")
case True then show ?thesis using funpow.simps (1) [of α] using exI [of _ "0::nat"] by auto
next
case False
obtain n where coeff_nilp: "nrows (((- (pert_matrix1 o hom_oper_matrix1))^n) A) = 0"
using nrows_strict_decr [of "(- (pert_matrix1 o hom_oper_matrix1))"]
using nrows_pert_hom_oper_decre
using False by force
show ?thesis
unfolding α_matrix_definition
using nrows_zero_impl_zero [OF coeff_nilp] ..
qed
qed
end
text{*Unfortunately, the previous type @{text matrix} cannot be used with
the code generation facility. In order to get code generation, it is not
enoguh to prove the instances, but also the underlying types need to have
an executable counterpart.*}
text{*Thus, we used new definitions based on \emph{sparse matrices},
which are based on lists and can be used
with the code generation facility.*}
text{*Unfortunately, sparse matrices cannot be proved to be an instance
of the previous type classes, since the results required are not equations
or definitional theorems, but more elaborated ones.*}
subsection {*Definition of the operations over sparse matrices.*}
fun transpose_spmat :: "('a::lordered_ring) spmat => 'a spmat"
where
transpose_spmat_Em: "transpose_spmat [] = []"
| transpose_spmat_C_cons: "transpose_spmat ((i,v)#vs) =
(let m = map (λ (j, x). (j, [(i, x)])) v;
M = transpose_spmat vs
in add_spmat (m, M))"
text{*Unfortunately,
the following definition of @{term "differ_spmat"} does not preserve
the sortedness of the input matrix,
as it is shown in the lemmas below*}
fun differ_spmat :: "('a::lordered_ring) spmat => 'a spmat"
where
differ_spmat_Em: "differ_spmat [] = []"
| differ_spmat_C_cons: "differ_spmat ((i,v)#vs) =
(let
m = map (λ (j, x). (if (j = 0) then (j, 0)
else (if ((i + j) mod 2 = 0)
then (j - 1, (0::'a))
else (j - 1, x)))) v;
M = differ_spmat vs
in add_spmat ([(i, m)], M))"
text{*Let's see what happens with @{term "differ_spmat"} which has degree $-1$
and should not preserve the order of the colums*}
text{*In the first lemma it canbe seen that the predicate @{term "sorted_spvec"}
holds for @{term "differ_spmat"}.
This means that it keeps th sortedness of rows. This will be later proved.*}
text{*Unfortunately, @{term differ_spmat} doesnot preserve @{term "sorted_spmat"},
which is the predicate checking that the elements in
each column are sorted.*}
(*definition foo_def: "foo == (0::nat, (0::nat, 5::int) # (2, - 9) # (6, 8) # [])
# (1::nat, (1::nat, 4::int) # (2, 0) # (8, 8) # [])
# (2::nat, (2::nat, 6::int) # (3, 7) # (9, 23) # [])
# (29::nat, (3::nat, 5::int) # (4, 6) # (7, 8) # []) # []"
definition foo2_def: "foo2 = (3::nat, (2::nat, 4::int) # []) # []"
value "differ_spmat foo2"
lemma "sorted_spvec (differ_spmat foo) = True"
unfolding foo_def
unfolding differ_spmat.simps
unfolding Let_def apply simp
unfolding sorted_spvec.simps by simp
lemma "sorted_spmat (differ_spmat (differ_spmat foo)) = False"
unfolding foo_def
unfolding differ_spmat.simps
unfolding Let_def
apply simp
unfolding Let_def
apply simp unfolding sorted_spmat.simps unfolding sorted_spvec.simps by auto*)
text{*A lemma proving that @{term differ_spmat} is distributive
with respect to the appending of lists.*}
lemma differ_spmat_dist: "differ_spmat ((a, b) # A) = add_spmat (
([(a, (map (λ (j, x). if (j = 0) then (j, (0::'a::lordered_ring))
else (if ((a + j) mod 2 = 0) then (j - 1, (0::'a))
else (j - 1, x))) b))]), differ_spmat A)"
unfolding differ_spmat_C_cons unfolding Let_def ..
text{*The following definition @{term "differ_spmat'"} is equal to the one of
@{term "differ_spmat"} after the application of function @{term "sparse_row_matrix"}.
This means that both functions produce similar results over terms of @{term matrix} type.*}
text{*We used @{term differ_spmat'} for some induction methods since it produces always
elements of type @{typ "nat × ((nat × int) list)"}
which somehow simplify induction proofs*}
text{*Later we will introduce a third operation @{term "differ_smat_sort"},
which is also equivalent to these two
in producing terms of @{term "matrix"} type and which additionally
preserves sortedness of vectors.*}
fun differ_spmat' :: "('a::lordered_ring) spmat => 'a spmat"
where
differ_spmat'_Em: "differ_spmat' [] = []"
| differ_spmat'_C_cons: "differ_spmat' ((i,v)#vs) =
(let
m = map (λ (j, x). if (j = 0) then (i, [(j, (0::'a))])
else (if ((i + j) mod 2 = 0) then (i, [(j - 1, (0::'a))])
else ((i, [(j - 1, x)])))) v;
M = differ_spmat' vs
in add_spmat (m, M))"
lemma differ_spmat'_dist: "differ_spmat' ((a, b) # A) = add_spmat (
map (λ (j, x). if (j = 0) then (a, [(j, (0::'a::lordered_ring))])
else (if ((a + j) mod 2 = 0) then (a, [(j - 1, (0::'a))])
else (a, [(j - 1, x)]))) b, differ_spmat' A)"
unfolding differ_spmat'_C_cons unfolding Let_def by simp
text{*A similar situation arises with @{term "pert_spmat"} and @{term "pert_spmat'"};
one is better in preserving sortedness and the other one is better for induction proofs.*}
text{*The following definition reiles on the fact that the result of evaluating
@{term "(0::nat) - 1"} over the natural numbers is equal to @{term "0::nat"}*}
fun pert_spmat :: "('a::lordered_ring) spmat => 'a spmat"
where
pert_spmat_Em: "pert_spmat [] = []"
| pert_spmat_C_cons: "pert_spmat ((i,v)#vs) =
(let
m = map (λ (j, x). if (i = 0) then (j, (0::'a)) else
if ((i + j) mod 2 = 0) then (j, (0::'a))
else (j, x)) v;
M = pert_spmat vs
in add_spmat ([(i - 1, m)], M))"
lemma pert_spmat_dist: "pert_spmat ((a, b) # A) = add_spmat (
([(a - 1, map (λ (j, x). if (a = 0) then (j, (0::'a::lordered_ring)) else
if ((a + j) mod 2 = 0) then (j, (0::'a))
else (j, x)) b)]) , pert_spmat A)"
using pert_spmat_C_cons unfolding Let_def by simp
fun pert_spmat' :: "('a::lordered_ring) spmat => 'a spmat"
where
pert_spmat'_Em: "pert_spmat' [] = []"
| pert_spmat'_C_cons: "pert_spmat' ((i,v)#vs) =
(let
m = map (λ (j, x). if (i = 0) then (i - 1, [(j, (0::'a))]) else
if ((i + j) mod 2 = 0) then (i - 1, [(j, (0::'a))])
else (i - 1, [(j, x)])) v;
M = pert_spmat' vs
in add_spmat (m, M))"
(*definition foo_def: "foo == (0::nat, (0::nat, 5::int) # (2, - 9) # (6, 8) # [])
# (1::nat, (1::nat, 4::int) # (2, 0) # (8, 8) # [])
# (2::nat, (2::nat, 6::int) # (3, 7) # (9, 23) # [])
# (29::nat, (3::nat, 5::int) # (4, 6) # (7, 8) # []) # []"
definition foo2_def: "foo2 = (0::nat, (7::nat, 4::int) # []) # []"
value "add_spmat ((pert_spmat foo), (minus_spmat (pert_spmat' foo)))"*)
lemma pert_spmat'_dist: "pert_spmat' ((a, b) # A) = add_spmat (
(map (λ (j, x). if (a = 0) then (a - 1, [(j, (0::'a::lordered_ring))]) else
if ((a + j) mod 2 = 0) then (a - 1, [(j, (0::'a))])
else (a - 1, [(j, x)])) b) , pert_spmat' A)"
using pert_spmat'_C_cons unfolding Let_def by simp
text{*In a similar way we provide two definitions for the @{term "hom_oper_spmat"} operation*}
fun hom_oper_spmat :: "('a::lordered_ring) spmat => 'a spmat"
where
hom_oper_spmat_Em: "hom_oper_spmat [] = []"
| hom_oper_spmat_C_cons: "hom_oper_spmat ((i,v)#vs) =
(let
m = map (λ (j, x). if ((i + j) mod (2::nat) = 1) then (j + 1, (0::'a))
else (j + 1, x)) v;
M = hom_oper_spmat vs
in add_spmat ((i, m) # [], M))"
fun hom_oper_spmat' :: "('a::lordered_ring) spmat => 'a spmat"
where
hom_oper_spmat'_Em: "hom_oper_spmat' [] = []"
| hom_oper_spmat'_C_cons: "hom_oper_spmat' ((i,v)#vs) =
(let
m = map (λ (j, x). if ((i + j) mod (2::nat) = 1) then (i, [(j + 1, (0::'a))])
else (i, [(j + 1, x)])) v;
M = hom_oper_spmat' vs
in add_spmat (m, M))"
lemma hom_oper_spmat_dist: "hom_oper_spmat ((a, b) # A) = add_spmat (
([(a, map (λ(j, x). if (a + j) mod 2 = 1 then (j + 1, 0::'a::lordered_ring)
else (j + 1, x)) b)],
hom_oper_spmat A))"
unfolding hom_oper_spmat_C_cons unfolding Let_def by simp
lemma hom_oper_spmat'_dist: "hom_oper_spmat' ((a, b) # A) = add_spmat (
map (λ (j, x). if ((a + j) mod 2 = 1) then (a, [(j + 1, (0::'a::lordered_ring))])
else (a, [(j + 1, x)])) b, hom_oper_spmat' A)"
unfolding hom_oper_spmat'_C_cons unfolding Let_def by simp
subsection{*Some auxiliary lemmas*}
lemma map_impl_existence:
assumes map_f_l: "map f l = a # l'"
shows "∃a'. a' mem l ∧ f a' = a"
using map_f_l by auto
lemma move_matrix_zero: shows "move_matrix 0 i j = 0"
unfolding move_matrix_def
unfolding zero_matrix_def
by (rule cong [of "Abs_matrix" "Abs_matrix"])
(auto simp add: expand_fun_eq RepAbs_matrix [of "(λj i. 0::'a)"])
lemma sparse_row_matrix_cons2:
"sparse_row_matrix [(i, (a::(nat×'a::lordered_ring)) # v)]
= singleton_matrix i (fst a) (snd a) + sparse_row_matrix [(i,v)]"
unfolding sparse_row_matrix_cons
unfolding sparse_row_matrix_empty
apply simp
unfolding move_matrix_add by simp
lemma sorted_spvec_trans:
assumes srtd: "sorted_spvec (a#b)" and c_in_b: "c mem b"
shows "fst a < fst c"
using srtd c_in_b proof (induct b)
case Nil
{
show ?case using Nil.prems (2) by auto
}
next
case Cons
{
fix aa list
assume hypo: "[|sorted_spvec (a # list); c mem list|] ==> fst a < fst c"
and prem1: "sorted_spvec (a # aa # list)" and prem2: "c mem aa # list"
show "fst a < fst c"
proof (cases "c mem list")
case True
{
show ?thesis
using hypo [OF sorted_spvec_cons2 [OF prem1] True] .
}
next
case False
{
have c_eq_aa: "c = aa"
using False prem2 by (cases "c = aa") simp+
show ?thesis
using prem1 unfolding sym [OF c_eq_aa]
unfolding sorted_spvec_step [of a "c#list"]
by simp
}
qed
}
qed
subsection{*Properties of the operation @{text "hom_oper_spmat"}*}
text{*The operation @{term "hom_oper_spmat"} preserves sortedness
of vectors and matrices.*}
text{*It is also equivalent to the operation @{term "hom_matrix1"}
that we introduced previously, under the operation
@{term "sparse_row_matrix"}.*}
lemma add_spmat_el[simp]: "add_spmat (a, []) = a"
by (cases a) auto
thm foldl_absorb0
text{*The following lemma is almost a copy of @{thm "foldl_absorb0"} except that it considers
different types in the arguments*}
lemma foldl_absorb0':
fixes l :: "nat × (nat × 'a::lordered_ring) list => 'a matrix"
shows "!!M. foldl (λ(m::'a::lordered_ring matrix) x::nat × (nat × 'a) list.
m + (l x) ) M arr =
M + foldl (λm x. m + (l x)) (0::'a matrix) arr"
proof (induct arr)
case Nil show ?case by simp
next
case Cons
fix a:: "nat × (nat × 'a) list"
fix arr :: "(nat × (nat × 'a) list) list"
fix M :: "'a matrix"
assume hypo: "!!M. foldl (λm x. m + l x) M arr = M + foldl (λm x. m + l x) 0 arr"
show " foldl (λm x. m + l x) M (a # arr) = M + foldl (λm x. m + l x) 0 (a # arr)"
unfolding foldl.simps (2)
unfolding hypo [of "M + l a"]
unfolding hypo [of "0 + l a"] by simp
qed
lemma sparse_row_matrix_hom_oper_spvec:
shows "sparse_row_matrix (hom_oper_spmat ((i, v)#[]))
= sparse_row_matrix (hom_oper_spmat' ((i, v)# []))"
proof (induct v)
case Nil show ?case
unfolding sparse_row_matrix_def apply simp
unfolding move_matrix_zero ..
next
case Cons
fix v::"(nat × 'a) list"
fix a:: "nat × 'a"
assume hypo: "sparse_row_matrix (hom_oper_spmat [(i, v)])
= sparse_row_matrix (hom_oper_spmat' [(i, v)])"
obtain p x where a_split: "a = (p, x)" by force
show "sparse_row_matrix (hom_oper_spmat [(i, a#v)])
= sparse_row_matrix (hom_oper_spmat' [(i, a#v)])"
using hypo
unfolding a_split
unfolding sparse_row_matrix_def
unfolding hom_oper_spmat.simps (2)
unfolding hom_oper_spmat'.simps (2)
unfolding Let_def
unfolding hom_oper_spmat.simps (1)
unfolding hom_oper_spmat'.simps (1)
unfolding add_spmat.simps (2)
apply (cases "(i + p) mod 2 = 1")
apply auto
unfolding move_matrix_zero
apply (rule cong [of "foldl
(λm r. m + move_matrix (sparse_row_vector (snd r)) (int (fst r)) (0::int)) 0"])
apply fast
apply simp
unfolding move_matrix_add
unfolding move_matrix_singleton
apply simp
unfolding foldl_absorb0' [of _ "singleton_matrix i (nat ((1::int) + int p)) x"] ..
qed
text{*The following operation proves that the two operations @{term "hom_oper_spmat"}
and @{term "hom_oper_spmat'"} are equivalent under
the application of @{term "sparse_row_matrix"}.*}
lemma sparse_row_matrix_hom_oper_spmat:
"sparse_row_matrix (hom_oper_spmat A)
= sparse_row_matrix (hom_oper_spmat' A)"
proof (induct A)
case Nil
{
show ?case using hom_oper_spmat.simps (1) hom_oper_spmat'.simps (1) by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A:: "'a spmat"
assume hypo: "sparse_row_matrix (hom_oper_spmat A)
= sparse_row_matrix (hom_oper_spmat' A)"
show "sparse_row_matrix (hom_oper_spmat (a # A))
= sparse_row_matrix (hom_oper_spmat' (a # A))"
unfolding a_split
using sparse_row_matrix_hom_oper_spvec [of i v]
unfolding hom_oper_spmat_dist
unfolding hom_oper_spmat'_dist
unfolding sparse_row_add_spmat
using hypo by simp
}
qed
text{*The following lemma proves that @{term hom_oper_spmat}
preserves the sortedness of matrices w.r.t @{term hom_oper_spvec}.*}
lemma sorted_spvec_hom_oper:
assumes srtd_A: "sorted_spvec A"
shows "sorted_spvec (hom_oper_spmat A)"
using srtd_A proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sorted_spvec A ==> sorted_spvec (hom_oper_spmat A)"
and prem: "sorted_spvec (a # A)"
have sorted_spvec_hos: "sorted_spvec (hom_oper_spmat A)"
using hypo [OF sorted_spvec_cons1 [OF prem]] .
show "sorted_spvec (hom_oper_spmat (a # A))"
unfolding a_split
unfolding hom_oper_spmat.simps
unfolding Let_def
by (rule sorted_spvec_add_spmat [OF _ sorted_spvec_hos],
induct v,
simp_all add: sorted_spvec.simps)
}
qed
lemma sorted_spvec_singleton[simp]: "sorted_spvec [(i, v)]"
using sorted_spvec.simps (2) [of "(i, v)" "[]"] by simp
lemma sorted_spvec_hom_oper_vec: assumes ss_v: "sorted_spvec v"
shows "sorted_spvec (map (λ(j, x). if (i + j) mod 2 = Suc 0
then (j + 1, 0::'a::lordered_ring) else (j + 1, x)) v)"
(is "sorted_spvec (map ?f v)")
using ss_v proof (induct v)
case Nil show ?case by simp
next
case Cons
fix a :: "(nat × 'a)"
obtain i va where a_split: "a = (i, va)" by force
fix v :: "(nat × 'a) list"
assume hypo: "sorted_spvec v ==> sorted_spvec (map ?f v)"
and prem: "sorted_spvec (a # v)"
have ss_v': "sorted_spvec v"
using prem unfolding sorted_spvec.simps (2) by (cases v) auto
have ss_fv': "sorted_spvec (map ?f v)" using hypo [OF ss_v'] .
show "sorted_spvec (map ?f (a # v))"
proof (unfold map.simps)
show "sorted_spvec ((?f a) # (map ?f v))"
proof (cases "map ?f v")
case Nil
{
show ?thesis
unfolding Nil
unfolding a_split
unfolding split_conv by simp
}
next
case Cons
{
fix c :: "nat × 'a"
fix lista :: "(nat × 'a) list"
assume hypo_cons: "map ?f v = c # lista"
show "sorted_spvec ((?f a) # (map ?f v))"
proof -
have "sorted_spvec (c # lista)"
using ss_fv'
unfolding hypo_cons .
moreover have " fst (?f a) < fst c"
proof -
obtain c' where c'_def: "(c' mem v) ∧ (?f c' = c)"
using hypo_cons using map_impl_existence [of ?f v c lista] by auto
with prem have fstb_l_fstc': "fst a < fst c'"
using sorted_spvec_trans [of a v c'] by simp
with c'_def show ?thesis proof auto
have lhs: "fst (?f (fst a, snd a)) = (fst a) + 1" by force
have rhs: "fst (?f (fst c', snd c')) = (fst c') + 1" by force
from lhs rhs and fstb_l_fstc' show "fst (?f a) < fst (?f c')" by simp
qed
qed
ultimately show ?thesis
unfolding hypo_cons
unfolding sorted_spvec.simps (2) by simp
qed
}
qed
qed
qed
lemma sorted_spmat_hom_oper:
assumes sorted_spmat_A: "sorted_spmat A"
shows "sorted_spmat (hom_oper_spmat A)"
using sorted_spmat_A proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sorted_spmat A ==> sorted_spmat (hom_oper_spmat A)"
and prem: "sorted_spmat (a # A)"
have sspm: "sorted_spmat (hom_oper_spmat A)"
using sorted_spmat.simps (2) [of a A] using prem using hypo by fast
have stsp: "sorted_spvec v" using prem unfolding a_split
unfolding sorted_spmat.simps (2) unfolding snd_conv ..
show "sorted_spmat (hom_oper_spmat (a # A))"
unfolding a_split
unfolding hom_oper_spmat_dist
apply (rule sorted_spmat_add_spmat [OF _ sspm])
apply simp
using sorted_spvec_hom_oper_vec [OF stsp, of i] .
}
qed
subsection{*Properties of the function @{term "differ_spmat"}*}
lemma sparse_row_matrix_differ_spvec:
"sparse_row_matrix (differ_spmat ((i, v)#[]))
= sparse_row_matrix (differ_spmat' ((i, v)# []))"
proof (induct v)
case Nil show ?case
unfolding sparse_row_matrix_def apply simp
unfolding move_matrix_zero ..
next
case Cons
fix v::"(nat × 'a) list"
fix a:: "nat × 'a"
assume hypo: "sparse_row_matrix (differ_spmat [(i, v)])
= sparse_row_matrix (differ_spmat' [(i, v)])"
obtain p x where a_split: "a = (p, x)" by force
show "sparse_row_matrix (differ_spmat [(i, a#v)])
= sparse_row_matrix (differ_spmat' [(i, a#v)])"
using hypo
unfolding a_split
unfolding sparse_row_matrix_def
unfolding differ_spmat.simps (2)
unfolding differ_spmat'.simps (2)
unfolding Let_def
unfolding differ_spmat.simps (1)
unfolding hom_oper_spmat'.simps (1)
unfolding add_spmat.simps (2)
apply (cases "p = 0")
apply auto
unfolding move_matrix_zero apply simp
apply (cases "(i + p) mod 2 = 0")
apply auto
unfolding move_matrix_add
unfolding move_matrix_singleton
apply simp
unfolding foldl_absorb0' [of _ "singleton_matrix i (p - Suc 0) x"] ..
qed
lemma sparse_row_matrix_differ_spmat:
"sparse_row_matrix (differ_spmat A)
= sparse_row_matrix (differ_spmat' A)"
proof (induct A)
case Nil
{
show ?case using differ_spmat.simps (1) differ_spmat'.simps (1) by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A:: "'a spmat"
assume hypo: "sparse_row_matrix (differ_spmat A)
= sparse_row_matrix (differ_spmat' A)"
show "sparse_row_matrix (differ_spmat (a # A))
= sparse_row_matrix (differ_spmat' (a # A))"
unfolding a_split
using sparse_row_matrix_differ_spvec [of i v]
unfolding differ_spmat_dist
unfolding differ_spmat'_dist
unfolding sparse_row_add_spmat
using hypo by simp
}
qed
text{*This lemma might be omitted.
@{term "differ_spmat"} preserves the sortedness of the rows but not the one
of vectors, so this is why we will later introduce @{term "differ_spmat_sort"}*}
lemma sorted_spvec_differ:
assumes srtd_A: "sorted_spvec A"
shows "sorted_spvec (differ_spmat A)"
using srtd_A proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sorted_spvec A ==> sorted_spvec (differ_spmat A)"
and prem: "sorted_spvec (a # A)"
have ss_d: "sorted_spvec (differ_spmat A)"
using prem unfolding sorted_spvec.simps (2)
using hypo by (cases A) auto
show "sorted_spvec (differ_spmat (a # A))"
unfolding a_split
unfolding differ_spmat.simps (2)
unfolding Let_def
apply (rule sorted_spvec_add_spmat)
using sorted_spvec_singleton [of i "map (λ(j, x).
if j = 0 then (j, 0::'a) else if (i + j) mod 2 = 0
then (j - 1, 0::'a) else (j - 1, x)) v"]
using ss_d .
}
qed
subsection{*Some ideas to keep sorted vectors inside a matrix*}
text{*We will define two functions to keep vectors sorted.
The first one, @{text insert_sorted} inserts a pair
in a list in its right position.*}
text{*From the definition it can be seen that it does not
pay attention to whether the list was originally sorted or not.*}
primrec insert_sorted:: "(nat × 'a::lordered_ring) => 'a spvec => 'a spvec"
where
insert_sorted_nil: "insert_sorted a [] = [a]"
| insert_sorted_cons: "insert_sorted a (b # c) =
(if (fst a < fst b) then (a # b # c) else
(if fst a = fst b then (fst a, snd a + snd b) # c
else b # (insert_sorted a c)))"
lemma [simp]: "sorted_spvec [a]"
unfolding sorted_spvec.simps (2) [of a "[]"] by simp
text{*The following lemma proves that the @{term insert_sorted}
preserves sortedness of vectors.*}
lemma insert_preserves_sorted:
assumes sorted_spvec_v: "sorted_spvec v"
shows "sorted_spvec (insert_sorted a v)"
using sorted_spvec_v proof (induct v)
case Nil
{
show ?case unfolding insert_sorted_nil unfolding sorted_spvec.simps by simp
}
next
case Cons
{
fix u :: "nat × 'a"
fix w :: "(nat × 'a) list"
assume hypo: "sorted_spvec w ==> sorted_spvec (insert_sorted a w)"
and prem: "sorted_spvec (u # w)"
have ss_w: "sorted_spvec w"
using sorted_spvec_cons1 [OF prem] .
have ssi_a_w: "sorted_spvec (insert_sorted a w)"
using hypo [OF ss_w].
show "sorted_spvec (insert_sorted a (u # w))"
proof (cases "fst a < fst u")
case True
{
show ?thesis
unfolding insert_sorted.simps (2)
using True
using if_True
apply simp
unfolding sorted_spvec.simps (2) [of a "u # w"]
using prem by auto
}
next
case False note nl_a_u = False
{
show ?thesis
proof (cases "fst a = fst u")
case True
{
show ?thesis
unfolding insert_sorted.simps
using nl_a_u
using True apply simp using prem unfolding sorted_spvec.simps
by (cases w) auto
}
next
case False note ne_a_u = False
{
have sorted: "sorted_spvec (u # (insert_sorted a w))"
proof (cases w)
case Nil
{
show ?thesis
unfolding Nil
unfolding insert_sorted.simps (1)
unfolding sorted_spvec.simps (2) [of u "[a]"]
using nl_a_u False by simp
}
next
case Cons
{
fix wa wlist
assume hypow: "w = wa # wlist"
show "sorted_spvec (u # insert_sorted a w)"
proof (cases "fst a < fst wa")
case True
{
have helper: "insert_sorted a w = a # w"
using True
unfolding hypow
unfolding insert_sorted.simps (2) [of a wa wlist]
by simp
show ?thesis
unfolding helper
unfolding sorted_spvec.simps (2) [of u "a # w"]
unfolding hypow
apply simp
unfolding sorted_spvec.simps (2) [of a "wa # wlist"]
using hypow using ss_w True
using nl_a_u ne_a_u by simp
}
next
case False note a_eq_wa = False
{
show ?thesis
proof (cases "fst a = fst wa")
case True
{
have helper: "insert_sorted a w = (fst a, snd a + snd wa) # wlist"
using True and a_eq_wa
unfolding hypow
unfolding insert_sorted.simps (2) by simp
show ?thesis
unfolding helper
unfolding sorted_spvec.simps (2) [of u "(fst a, snd a + snd wa) # wlist"]
using ss_w using nl_a_u ne_a_u
using hypow
apply simp
unfolding True unfolding sorted_spvec.simps
by (cases wlist) auto
}
next
case False
{
have helper: "insert_sorted a w = wa # insert_sorted a wlist"
using False and a_eq_wa
unfolding hypow
unfolding insert_sorted.simps (2) by simp
show ?thesis
unfolding helper
using ssi_a_w
unfolding hypow
unfolding insert_sorted.simps (2) [of a ]
using False a_eq_wa
apply simp
using sorted_spvec_cons1 [of wa "insert_sorted a wlist"]
unfolding sorted_spvec.simps (2) [of u "wa # insert_sorted a wlist"]
apply simp using prem
unfolding hypow unfolding sorted_spvec.simps (2) [of u "wa # wlist"]
by simp
}
qed
}
qed
}
qed
}
then show ?thesis
using nl_a_u False
unfolding insert_sorted.simps (2) by simp
qed
}
qed
}
qed
text{*The following operation, @{term "sort_spvec"},
takes the first element of a list and introduces it in its corresponding position,
by means of the @{term "insert_sort"} operation.*}
text{*Applying this process recursively, we get to sort the vector.*}
primrec sort_spvec :: "'a::lordered_ring spvec => 'a spvec"
where
sort_spvec_nil: "sort_spvec [] = []"
| sort_spvec_cons: "sort_spvec (a # b) = (insert_sorted a (sort_spvec b))"
lemma sort_is_sorted: shows "sorted_spvec (sort_spvec v)"
proof (induct v)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a w
assume hypo: "sorted_spvec (sort_spvec w)"
show "sorted_spvec (sort_spvec (a # w))"
unfolding sort_spvec.simps (2)
using insert_preserves_sorted [OF hypo, of a] .
}
qed
text{*The operation of sorting is compatible with the addition of sparse vectors*}
lemma insert_pair_add_pair:
shows "insert_sorted (a, b) v = add_spvec ([(a, b)], v)"
proof (induct v)
case Nil show ?case by simp
next
case Cons
{
fix i :: "nat × 'a"
obtain j c where i_split: "i = (j, c)" by force
fix v :: "(nat × 'a) list"
assume hypo: "insert_sorted (a, b) v = add_spvec ([(a, b)], v)"
show "insert_sorted (a, b) (i # v) = add_spvec ([(a, b)], i # v)"
unfolding i_split
proof (cases "a < j")
case True
{
show "insert_sorted (a, b) ((j, c) # v) = add_spvec ([(a, b)], (j, c) # v)"
using True by simp
}
next
case False note a_nl_aa = False
{
show "insert_sorted (a, b) ((j, c) # v) = add_spvec ([(a, b)], (j, c) # v)"
proof (cases "a = j")
case True
{
show ?thesis using True a_nl_aa by simp
}
next
case False
{
show ?thesis using False a_nl_aa apply simp unfolding hypo ..
}
qed
}
qed
}
qed
text{*The following operation is similar to @{term differ_spmat}
except that it applies @{term sort_spvec} to every vector.*}
fun differ_spmat_sort :: "('a::lordered_ring) spmat => 'a spmat"
where
differ_spmat_sort_Em: "differ_spmat_sort [] = []"
| differ_spmat_sort_C_cons: "differ_spmat_sort ((i,v)#vs) =
(let
m = sort_spvec (map (λ (j, x). if j = 0 then (j, 0)
else if (i + j) mod 2 = 0 then (j - 1, 0) else (j - 1, x)) v);
M = differ_spmat_sort vs
in add_spmat ([(i, m)], M))"
lemma differ_spmat_sort_dist:
shows "differ_spmat_sort ((i, v) # vs) = add_spmat (
([(i, sort_spvec (
map (λ (j, x::'a::lordered_ring). if j = 0 then (j, 0)
else if (i + j) mod 2 = 0 then (j - 1, 0)
else (j - 1, x)) v))]), differ_spmat_sort vs)"
unfolding differ_spmat_sort_C_cons unfolding Let_def ..
lemma sorted_spvec_differ_spmat_sort:
assumes srtd_A: "sorted_spvec A"
shows "sorted_spvec (differ_spmat_sort A)"
using srtd_A proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sorted_spvec A ==> sorted_spvec (differ_spmat_sort A)"
and prem: "sorted_spvec (a # A)"
show "sorted_spvec (differ_spmat_sort (a # A))"
unfolding a_split
unfolding differ_spmat_sort.simps (2) [of i v A]
unfolding Let_def
apply (rule sorted_spvec_add_spmat)
using sorted_spvec_singleton [of i _] apply simp
using prem hypo
unfolding sorted_spvec.simps (2)
apply (cases A) by auto
}
qed
text{*As it may be seen in the following lemma, as far as we now have
the operation @{term sort_spvec} sorting every vector,
the lemma does not require the premise of @{term A} being previously sorted.*}
lemma sorted_spmat_differ_spmat_sort:
shows "sorted_spmat (differ_spmat_sort A)"
proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sorted_spmat (differ_spmat_sort A)"
show "sorted_spmat (differ_spmat_sort (a # A))"
unfolding a_split
unfolding differ_spmat_sort_dist
apply (rule sorted_spmat_add_spmat [OF _ _])
unfolding sorted_spmat.simps (2)
unfolding sorted_spmat.simps (1)
unfolding snd_conv apply simp
using sort_is_sorted using hypo .
}
qed
primrec sort_spvec_spmat :: "'a::lordered_ring spmat => 'a spmat"
where
sort_spvec_spmat_nil: "sort_spvec_spmat [] = []"
| sort_spvec_spmat_cons: "sort_spvec_spmat (a # as)
= (fst a, sort_spvec (snd a)) # (sort_spvec_spmat as)"
lemma sort_spvec_spmat_impl_sorted_spmat:
shows "sorted_spmat (sort_spvec_spmat A)"
proof (induct A)
case Nil show ?case by simp
next
case Cons
fix a A
assume hypo: "sorted_spmat (sort_spvec_spmat A)"
show "sorted_spmat (sort_spvec_spmat (a # A))"
unfolding sort_spvec_spmat.simps (2)
unfolding sorted_spmat.simps (2)
apply (rule conjI)
unfolding snd_conv
using sort_is_sorted [of "snd a"] using hypo .
qed
text{*The following lemma shows that even in the cases
where @{term "differ_spmat"} produces non sorted matrices,
they are equal to the ones obtained with @{term "differ_spmat_sort"}
under the application @{term "sparse_row_matrix"}*}
text{*We illustrate this fact with an example with @{term foo}.*}
(*definition foo_def: "foo == (0::nat, (0::nat, 5::int) # (2, - 9) # (6, 8) # [])
# (1::nat, (1::nat, 4::int) # (2, 0) # (8, 8) # [])
# (2::nat, (2::nat, 6::int) # (3, 7) # (9, 23) # [])
# (29::nat, (3::nat, 5::int) # (4, 6) # (7, 8) # []) # []"
lemma "sparse_row_matrix (differ_spmat (differ_spmat foo))
= sparse_row_matrix (differ_spmat_sort (differ_spmat_sort foo))"
unfolding foo_def
apply (simp add: differ_spmat.simps differ_spmat_sort.simps Let_def)
unfolding sparse_row_matrix_def by simp
*)
lemma sparse_row_vector_not_sorted:
shows "sparse_row_vector (a # b # []) = sparse_row_vector (b # a # [])"
unfolding sparse_row_vector_cons by simp
lemma sparse_row_vector_dist:
shows "sparse_row_vector ([(i, j + k)]) = sparse_row_vector ((i, j) # [(i, k)])"
unfolding sparse_row_vector_cons apply simp
unfolding singleton_matrix_def
unfolding plus_matrix_def
unfolding combine_matrix_def
apply (rule comb [of "Abs_matrix" "Abs_matrix"], simp)
unfolding combine_infmatrix_def
using RepAbs_matrix [of "(λm n. if 0 = m ∧ i = n then j else (0::'a))"]
using exI [of "(λm. ∀ja ia. m ≤ ja --> (if 0 = ja ∧ i = ia
then j else (0::'a)) = (0::'a))" "Suc 0"]
using exI [of "(λn. ∀ja ia. n ≤ ia --> (if (0::nat) = ja ∧ i = ia
then j else (0::'a)) = (0::'a))" "Suc i"]
apply auto
using RepAbs_matrix [of "(λm n. if 0 = m ∧ i = n then k else (0::'a))"]
using exI [of "(λm. ∀ja ia. m ≤ ja -->
(if 0 = ja ∧ i = ia then k else (0::'a)) = (0::'a))" "Suc 0"]
using exI [of "(λn. ∀ja ia. n ≤ ia -->
(if (0::nat) = ja ∧ i = ia then k else (0::'a)) = (0::'a))" "Suc i"]
apply auto
unfolding expand_fun_eq by simp
lemma insert_sorted_preserves_sparse_row_vector:
shows "sparse_row_vector (a # v) = sparse_row_vector (insert_sorted a v)"
proof (induct v)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix b :: "nat × 'a"
fix v :: "(nat × 'a) list"
assume hypo: "sparse_row_vector (a # v)
= sparse_row_vector (insert_sorted a v)"
show "sparse_row_vector (a # b # v)
= sparse_row_vector (insert_sorted a (b # v))"
proof (cases "fst a < fst b")
case True
{
show ?thesis
unfolding insert_sorted.simps using True by simp
}
next
case False note a_nl_b = False
{
show ?thesis
proof (cases "fst a = fst b")
case True
{
show ?thesis
unfolding insert_sorted.simps using a_nl_b using True
apply simp
using sparse_row_vector_dist [of "fst b" "snd a" "snd b"]
unfolding sparse_row_vector_cons by simp
}
next
case False
{
show ?thesis
unfolding insert_sorted.simps
using a_nl_b False apply simp
unfolding sym [OF sparse_row_vector_cons]
using hypo by simp
}
qed
}
qed
}
qed
lemma sort_spvec_eq_sparse_row_vector:
shows "sparse_row_vector v = sparse_row_vector (sort_spvec v)"
proof (induct v)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a
fix v
assume hypo: "sparse_row_vector v = sparse_row_vector (sort_spvec v)"
show "sparse_row_vector (a # v) = sparse_row_vector (sort_spvec (a # v))"
unfolding sort_spvec.simps
unfolding sym [OF insert_sorted_preserves_sparse_row_vector]
unfolding sparse_row_vector_cons
unfolding hypo ..
}
qed
lemma sort_spvec_eq_sparse_row_matrix:
shows "sparse_row_matrix [(i, v)]
= sparse_row_matrix [(i, sort_spvec v)]"
unfolding sparse_row_matrix_def
using sort_spvec_eq_sparse_row_vector [of v] by simp
lemma sparse_row_matrix_differ_spmat_differ_spmat_sort:
shows "sparse_row_matrix (differ_spmat A)
= sparse_row_matrix (differ_spmat_sort A)"
proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sparse_row_matrix (differ_spmat A)
= sparse_row_matrix (differ_spmat_sort A)"
show "sparse_row_matrix (differ_spmat (a # A))
= sparse_row_matrix (differ_spmat_sort (a # A))"
unfolding a_split
unfolding differ_spmat_dist
unfolding differ_spmat_sort_dist
unfolding sparse_row_add_spmat
unfolding hypo
using sort_spvec_eq_sparse_row_matrix by auto
}
qed
subsection{*Properties of the perturbation operator*}
lemma sparse_row_matrix_pert_spvec:
shows "sparse_row_matrix (pert_spmat ((i, v)#[]))
= sparse_row_matrix (pert_spmat' ((i, v)# []))"
proof (induct v)
case Nil show ?case
unfolding sparse_row_matrix_def apply simp
unfolding move_matrix_zero ..
next
case Cons
fix v::"(nat × 'a) list"
fix a:: "nat × 'a"
assume hypo: "sparse_row_matrix (pert_spmat [(i, v)])
= sparse_row_matrix (pert_spmat' [(i, v)])"
obtain p x where a_split: "a = (p, x)" by force
show "sparse_row_matrix (pert_spmat [(i, a#v)])
= sparse_row_matrix (pert_spmat' [(i, a#v)])"
using hypo
unfolding a_split
unfolding sparse_row_matrix_def
unfolding pert_spmat.simps (2)
unfolding pert_spmat'.simps (2)
unfolding Let_def
unfolding pert_spmat.simps (1)
unfolding hom_oper_spmat'.simps (1)
unfolding add_spmat.simps (2)
apply (cases "i = 0")
apply auto
apply (cases "(i + p) mod 2 = 0")
apply auto
unfolding move_matrix_zero
apply (rule cong [of "foldl
(λm r. m + move_matrix (sparse_row_vector (snd r)) (int (fst r)) (0::int)) 0"])
apply fast
apply simp
unfolding move_matrix_add
unfolding move_matrix_singleton
apply simp
unfolding foldl_absorb0' [of _ "singleton_matrix (i - Suc 0) p x"] ..
qed
lemma sparse_row_matrix_pert_spmat:
shows "sparse_row_matrix (pert_spmat A) = sparse_row_matrix (pert_spmat' A)"
proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sparse_row_matrix (pert_spmat A)
= sparse_row_matrix (pert_spmat' A)"
show "sparse_row_matrix (pert_spmat (a # A))
= sparse_row_matrix (pert_spmat' (a # A))"
unfolding a_split
unfolding pert_spmat_dist
unfolding pert_spmat'_dist
unfolding sparse_row_add_spmat
unfolding hypo
using sparse_row_matrix_pert_spvec [of i v]
unfolding pert_spmat.simps
unfolding pert_spmat'.simps
unfolding Let_def by simp
}
qed
text{*The following oepration is equivalent to
@{term pert_spmat} except that it sorts every vector.*}
fun pert_spmat_sort :: "('a::lordered_ring) spmat => 'a spmat"
where
pert_spmat_sort_Em: "pert_spmat_sort [] = []"
| pert_spmat_sort_C_cons: "pert_spmat_sort ((i,v)#vs) =
(let
m = sort_spvec (map (λ (j, x). if i = 0 then (j, 0) else
if (i + j) mod 2 = 0 then (j, 0) else (j, x)) v);
M = pert_spmat_sort vs
in add_spmat ([(i - 1, m)], M))"
lemma pert_spmat_sort_dist: "pert_spmat_sort ((i, v) # vs) = add_spmat (
([(i - 1, sort_spvec (map (λ (j, x). if i = 0 then (j, 0) else
if (i + j) mod 2 = 0 then (j, 0) else (j, x)) v))]), pert_spmat_sort vs)"
using pert_spmat_sort_C_cons [of i v vs] unfolding Let_def .
text{*Once again, the premise of @{term A} being sorted can
be avoided in the following lemma since @{term pert_spmat_sort}
will do the job*}
lemma sorted_spmat_pert_spmat_sort:
shows "sorted_spmat (pert_spmat_sort A)"
proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sorted_spmat (pert_spmat_sort A)"
show "sorted_spmat (pert_spmat_sort (a # A))"
unfolding a_split
unfolding pert_spmat_sort_dist
apply (rule sorted_spmat_add_spmat [OF _ _])
unfolding sorted_spmat.simps (2)
unfolding sorted_spmat.simps (1)
unfolding snd_conv apply simp
using sort_is_sorted using hypo .
}
qed
text{*The following lemma proves that both @{term pert_spmat} and
@{text pert_spmat_sort} produce the same result
under the application of @{term sparse_row_matrix}, or,
in other words, as terms of @{term matrix} type.*}
lemma sparse_row_matrix_pert_spmat_eq_pert_spmat_sort:
shows "sparse_row_matrix (pert_spmat A) = sparse_row_matrix (pert_spmat_sort A)"
proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sparse_row_matrix (pert_spmat A)
= sparse_row_matrix (pert_spmat_sort A)"
show "sparse_row_matrix (pert_spmat (a # A))
= sparse_row_matrix (pert_spmat_sort (a # A))"
unfolding a_split
unfolding pert_spmat_dist
unfolding pert_spmat_sort_dist
unfolding sparse_row_add_spmat
unfolding hypo
using sort_spvec_eq_sparse_row_matrix by auto
}
qed
lemma sorted_spvec_pert_spmat_sort:
assumes srtd_A: "sorted_spvec A"
shows "sorted_spvec (pert_spmat_sort A)"
using srtd_A proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sorted_spvec A ==> sorted_spvec (pert_spmat_sort A)"
and prem: "sorted_spvec (a # A)"
show "sorted_spvec (pert_spmat_sort (a # A))"
unfolding a_split
unfolding pert_spmat_sort.simps (2) [of i v A]
unfolding Let_def
apply (rule sorted_spvec_add_spmat)
using sorted_spvec_singleton [of i _] apply simp
using prem hypo
unfolding sorted_spvec.simps (2)
apply (cases A) by auto
}
qed
text{*The followig lemma may be omitted since we do not
care about the properties of @{term pert_spmat}, but of the ones from
@{term pert_spmat_sort}*}
lemma sorted_spvec_pert:
assumes srtd_A: "sorted_spvec A"
shows "sorted_spvec (pert_spmat A)"
using srtd_A proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "sorted_spvec A ==> sorted_spvec (pert_spmat A)"
and prem: "sorted_spvec (a # A)"
have sorted_spvec_ps: "sorted_spvec (pert_spmat A)"
using hypo [OF sorted_spvec_cons1 [OF prem]] .
show "sorted_spvec (pert_spmat (a # A))"
unfolding a_split
unfolding pert_spmat.simps
unfolding Let_def
by (rule sorted_spvec_add_spmat [OF _ sorted_spvec_ps],
induct v,
simp_all add: sorted_spvec.simps)
}
qed
section{*Equivalence between operations over matrices and sparse matrices.*}
lemma diff_matrix1_zero_eq_zero: "diff_matrix1 0 = 0"
apply (unfold zero_matrix_def diff_matrix1_def)
apply (simp add: RepAbs_matrix)
apply (unfold diff_infmatrix_def)
apply (subst Rep_matrix_inject [symmetric])
apply (simp add: RepAbs_matrix)
done
lemma foldl_zero_matrix:
shows "foldl (λ(m::'a matrix) x::nat × 'a. m) (0::'a::lordered_ring matrix) v = 0"
by (induct v, simp_all)
lemma Rep_Abs_zero_func:
shows "Rep_matrix (Abs_matrix (λm n::nat. 0::'a::lordered_ring)) p q
= (0::'a)"
apply(fold zero_matrix_def)
using Rep_zero_matrix_def [of p q] .
lemma is_matrix_i_j:
shows "Rep_matrix (Abs_matrix (λ(m::nat) n::nat. if i = m ∧ j = n then v else 0)) =
(λm n. if i = m ∧ j = n then v else (0::'b::lordered_ring))"
using RepAbs_matrix [of "(λm n. if i = m ∧ j = n then v else 0)"]
using exI [of _ "i + 1"] using exI [of _ "j + 1"] by auto
lemma diff_matrix1_singleton:
shows "diff_matrix1 (singleton_matrix i j v) =
Abs_matrix (λk l. if (k + l) mod 2 = 1 then 0::'a::lordered_ring
else if i = k ∧ j = l + 1 then v else 0)"
unfolding diff_matrix1_def
unfolding o_apply
unfolding diff_infmatrix_def
unfolding singleton_matrix_def
unfolding is_matrix_i_j
apply (rule comb [of "Abs_matrix" "Abs_matrix"])
unfolding expand_fun_eq by auto
lemma comb_matrix:
assumes f_eq: "f = g" and matrix_eq: "(A::'a matrix) = B"
and x_eq: "(x::int) = x'" and y_eq: "(y::int) = y'"
shows "f A x y = g B x' y'"
using f_eq matrix_eq x_eq y_eq by simp
lemma diff_matrix1_execute_sparse:
shows "diff_matrix1 (sparse_row_matrix A)
= sparse_row_matrix (differ_spmat' A)"
proof (induct A)
show "diff_matrix1 (sparse_row_matrix [])
= sparse_row_matrix (differ_spmat' [])"
using diff_matrix1_zero_eq_zero by simp
next
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "diff_matrix1 (sparse_row_matrix A)
= sparse_row_matrix (differ_spmat' A)"
show "diff_matrix1 (sparse_row_matrix (a # A))
= sparse_row_matrix (differ_spmat' (a # A))"
unfolding a_split
unfolding sparse_row_matrix_cons [of _ A]
unfolding fst_conv snd_conv
unfolding differ_spmat'_dist [of _ _ "A"]
unfolding sparse_row_add_spmat [of _ "differ_spmat' A"]
unfolding diff_matrix1_hom [of _ "sparse_row_matrix A"]
unfolding hypo apply simp
proof -
show "diff_matrix1 (move_matrix (sparse_row_vector v) (int i) 0) =
sparse_row_matrix
(map (λ(j, x).
if j = 0 then (i, [(j, 0::'a)])
else if (i + j) mod 2 = 0 then (i, [(j - 1, 0::'a)]) else (i, [(j - 1, x)]))
v)"
(is "_ = sparse_row_matrix (map ?f v)")
proof (induct v)
case Nil
show ?case
unfolding sparse_row_vector_empty
unfolding move_matrix_zero
unfolding diff_matrix1_zero_eq_zero
unfolding map.simps (1)
unfolding sparse_row_matrix_empty ..
next
case Cons
fix a :: "nat × 'a"
obtain j x where a_split: "a = (j, x)" by force
fix v :: "(nat × 'a) list"
assume hyps: "diff_matrix1 (move_matrix (sparse_row_vector v) (int i) 0) =
sparse_row_matrix (map ?f v)"
show "diff_matrix1 (move_matrix (sparse_row_vector (a # v)) (int i) 0) =
sparse_row_matrix (map ?f (a # v))"
unfolding map.simps
unfolding sparse_row_vector_cons
unfolding move_matrix_add
unfolding diff_matrix1_hom
unfolding sparse_row_matrix_cons
unfolding hyps apply simp
unfolding a_split
unfolding fst_conv snd_conv
unfolding split_conv
unfolding diff_matrix1_def
unfolding o_apply
unfolding diff_infmatrix_def
unfolding move_matrix_def
apply (rule cong [of "Abs_matrix" "Abs_matrix"])
apply simp
apply (auto simp add: expand_fun_eq)
apply arith apply arith
unfolding neg_def by arith
qed
qed
qed
lemma hom_oper_matrix1_zero_eq_zero: "hom_oper_matrix1 0 = 0"
apply (unfold zero_matrix_def hom_oper_matrix1_def)
apply (simp add: RepAbs_matrix)
apply (unfold hom_oper_infmatrix_def)
apply (subst Rep_matrix_inject [symmetric])
apply (simp add: RepAbs_matrix expand_fun_eq)
done
lemma hom_oper_matrix1_singleton:
shows "hom_oper_matrix1 (singleton_matrix k l v) =
Abs_matrix (λi j. if (j = 0) then 0 else
if ((i + j) mod 2 = 0) then 0 else
if (k = i ∧ l = j - (1::nat)) then v
else (0::'b::lordered_ring))"
unfolding hom_oper_matrix1_def
unfolding o_apply
unfolding hom_oper_infmatrix_def
unfolding singleton_matrix_def
unfolding is_matrix_i_j ..
lemma hom_oper_matrix1_execute_sparse:
shows "hom_oper_matrix1 (sparse_row_matrix A)
= sparse_row_matrix (hom_oper_spmat' A)"
proof (induct A)
show "hom_oper_matrix1 (sparse_row_matrix [])
= sparse_row_matrix (hom_oper_spmat' [])"
using hom_oper_matrix1_zero_eq_zero by simp
next
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "hom_oper_matrix1 (sparse_row_matrix A)
= sparse_row_matrix (hom_oper_spmat' A)"
show "hom_oper_matrix1 (sparse_row_matrix (a # A))
= sparse_row_matrix (hom_oper_spmat' (a # A))"
unfolding a_split
unfolding sparse_row_matrix_cons [of _ A]
unfolding fst_conv snd_conv
unfolding hom_oper_spmat'_dist [of _ _ "A"]
unfolding sparse_row_add_spmat [of _ "hom_oper_spmat' A"]
unfolding hom_oper_matrix1_hom [of _ "sparse_row_matrix A"]
unfolding hypo apply simp
proof -
show "hom_oper_matrix1 (move_matrix (sparse_row_vector v) (int i) (0::int)) =
sparse_row_matrix
(map (λ(j::nat, x::'a).
if (i + j) mod (2::nat) = Suc (0::nat) then (i, [(j + (1::nat), 0::'a)])
else (i, [(j + (1::nat), x)])) v)"
(is "_ = sparse_row_matrix (map ?f v)")
proof (induct v)
case Nil
show ?case
unfolding sparse_row_vector_empty
unfolding move_matrix_zero
unfolding hom_oper_matrix1_zero_eq_zero
unfolding map.simps (1)
unfolding sparse_row_matrix_empty ..
next
case Cons
fix a :: "nat × 'a"
obtain j x where a_split: "a = (j, x)" by force
fix v :: "(nat × 'a) list"
assume hyps: " hom_oper_matrix1 (move_matrix (sparse_row_vector v) (int i) (0::int)) =
sparse_row_matrix
(map (λ(j::nat, x::'a).
if (i + j) mod (2::nat) = Suc (0::nat) then (i, [(j + (1::nat), 0::'a)])
else (i, [(j + (1::nat), x)])) v)"
show "hom_oper_matrix1 (move_matrix (sparse_row_vector (a # v)) (int i) (0::int)) =
sparse_row_matrix
(map (λ(j::nat, x::'a).
if (i + j) mod (2::nat) = Suc (0::nat) then (i, [(j + (1::nat), 0::'a)])
else (i, [(j + (1::nat), x)]))
(a # v))"
unfolding map.simps
unfolding sparse_row_vector_cons
unfolding move_matrix_add
unfolding hom_oper_matrix1_hom
unfolding sparse_row_matrix_cons
unfolding hyps apply simp
unfolding a_split
unfolding fst_conv snd_conv
unfolding split_conv
unfolding hom_oper_matrix1_def
unfolding o_apply
unfolding hom_oper_infmatrix_def
unfolding move_matrix_def
apply (rule cong [of "Abs_matrix" "Abs_matrix"])
apply simp
apply (auto simp add: expand_fun_eq)
apply arith apply arith
unfolding neg_def apply arith by arith
qed
qed
qed
lemma hom_oper_matrix1_execute_sparse_simp:
shows "hom_oper_matrix1 (sparse_row_matrix A)
= sparse_row_matrix (hom_oper_spmat A)"
unfolding hom_oper_matrix1_execute_sparse
unfolding sym [OF sparse_row_matrix_hom_oper_spmat] ..
lemma pert_matrix1_zero_eq_zero: "pert_matrix1 0 = 0"
apply (unfold zero_matrix_def pert_matrix1_def, auto)
apply (simp add: RepAbs_matrix)
apply (unfold pert_infmatrix_def)
apply (rule comb [of Abs_matrix Abs_matrix])
apply simp
apply (unfold expand_fun_eq, simp)
done
lemma pert_matrix1_singleton:
shows "pert_matrix1 (singleton_matrix k l v) =
Abs_matrix (λi j. if ((i + j) mod 2 = 1) then 0 else
if (k = i + (1::nat) ∧ l = j) then v
else (0::'b::lordered_ring))"
unfolding pert_matrix1_def
unfolding o_apply
unfolding pert_infmatrix_def
unfolding singleton_matrix_def
unfolding is_matrix_i_j ..
lemma pert_matrix1_execute_sparse:
shows "pert_matrix1 (sparse_row_matrix A)
= sparse_row_matrix (pert_spmat' A)"
proof (induct A)
show "pert_matrix1 (sparse_row_matrix [])
= sparse_row_matrix (pert_spmat' [])"
using pert_matrix1_zero_eq_zero by simp
next
fix a :: "nat × (nat × 'a) list"
obtain i v where a_split: "a = (i, v)" by force
fix A :: "'a spmat"
assume hypo: "pert_matrix1 (sparse_row_matrix A)
= sparse_row_matrix (pert_spmat' A)"
show "pert_matrix1 (sparse_row_matrix (a # A))
= sparse_row_matrix (pert_spmat' (a # A))"
unfolding a_split
unfolding sparse_row_matrix_cons [of _ A]
unfolding fst_conv snd_conv
unfolding pert_spmat'_dist [of _ _ "A"]
unfolding sparse_row_add_spmat [of _ "pert_spmat' A"]
unfolding pert_matrix1_hom [of _ "sparse_row_matrix A"]
unfolding hypo apply simp
proof -
show " pert_matrix1 (move_matrix (sparse_row_vector v) (int i) (0::int)) =
sparse_row_matrix
(map (λ(j::nat, x::'a).
if i = (0::nat) then (i - (1::nat), [(j, 0::'a)])
else if (i + j) mod (2::nat) = (0::nat) then (i - (1::nat), [(j, 0::'a)])
else (i - (1::nat), [(j, x)])) v)"
(is "_ = sparse_row_matrix (map ?f v)")
proof (induct v)
case Nil
show ?case
unfolding sparse_row_vector_empty
unfolding move_matrix_zero
unfolding pert_matrix1_zero_eq_zero
unfolding map.simps (1)
unfolding sparse_row_matrix_empty ..
next
case Cons
fix a :: "nat × 'a"
obtain j x where a_split: "a = (j, x)" by force
fix v :: "(nat × 'a) list"
assume hyps: "pert_matrix1 (move_matrix (sparse_row_vector v) (int i) 0) =
sparse_row_matrix (map ?f v)"
show "pert_matrix1 (move_matrix (sparse_row_vector (a # v)) (int i) 0) =
sparse_row_matrix (map ?f (a # v))"
unfolding map.simps
unfolding sparse_row_vector_cons
unfolding move_matrix_add
unfolding pert_matrix1_hom
unfolding sparse_row_matrix_cons
unfolding hyps apply simp
unfolding a_split
unfolding fst_conv snd_conv
unfolding split_conv
unfolding pert_matrix1_def
unfolding o_apply
unfolding pert_infmatrix_def
unfolding move_matrix_def
apply (rule cong [of "Abs_matrix" "Abs_matrix"])
apply simp
apply (auto simp add: expand_fun_eq)
apply arith apply arith
unfolding neg_def by arith
qed
qed
qed
lemma pert_matrix1_execute_sparse_simp:
shows "pert_matrix1 (sparse_row_matrix A)
= sparse_row_matrix (pert_spmat_sort A)"
unfolding pert_matrix1_execute_sparse
unfolding sym [OF sparse_row_matrix_pert_spmat]
unfolding sparse_row_matrix_pert_spmat_eq_pert_spmat_sort ..
subsection{*Zero as sparse matrix*}
text{*In order to get the bound of a function we need a notion of a zero matrix,
up to which the bound is computed.*}
text{*In sparse matrices there is no single zero matrix,
but any matrix containing only zeros will be such.*}
text{*We provide a function that computes the number
of non-zero elements of a vector.*}
text{*If the number of non-zero positions of a vector is zero,
this should be the null vector.*}
primrec non_zero_spvec :: "'a::zero spvec => nat"
where "non_zero_spvec [] = 0"
| "non_zero_spvec (a#b) = (if snd a ≠ 0 then Suc (non_zero_spvec b)
else non_zero_spvec b)"
lemma non_zero_spvec_ge_0: "(0::nat) ≤ non_zero_spvec a" ..
text{*We have proven the following lemma in terms of sets
since automatic methods apply much better than with Lists and functions
@{term "op mem"} or @{term "ListMem"}*}
lemma non_zero_spvec_g_0:
assumes non_zero_a: "non_zero_spvec (a::'a::zero spvec) ≠ 0"
shows "∃pair. pair ∈ set a ∧ snd pair ≠ (0::'a::zero)"
proof (rule ccontr)
assume contrad: "¬ (∃pair. pair ∈ set a ∧ snd pair ≠ (0::'a))"
have null_comp: "!!pair. pair ∈ set a ==> snd pair = 0"
proof -
fix pair :: "nat × 'a"
assume pair_in_list: "pair ∈ set a"
show "snd pair = 0"
proof -
have "!!b c. (b,c) ∈ set a ==> c = 0"
using contrad by simp
then have "(fst pair, snd pair) ∈ set a ==> snd pair = 0"
by fast
with pair_in_list show ?thesis by force
qed
qed
have "non_zero_spvec (a::'a::zero spvec) = 0"
using null_comp by (induct a) auto
with non_zero_a show False ..
qed
text{*Based on the previous function for vectors,
a function for matrices is defined.*}
text{*This function will be later used in the computation
of the bound of nilpotency of a matrix.*}
primrec non_zero_spmat:: "'a::zero spmat => nat"
where "non_zero_spmat [] = 0"
| "non_zero_spmat (a#b) = non_zero_spvec (snd a) + non_zero_spmat b"
lemma non_zero_spmat_g_0:
assumes non_zero_a: "non_zero_spmat (a::'a::zero spmat) ≠ 0"
shows "∃list. list ∈ set a ∧ non_zero_spvec (snd list) ≠ 0"
proof (rule ccontr)
assume contrad: "¬ (∃list. list ∈ set a
∧ non_zero_spvec (snd list) ≠ 0)"
have null_comp: "!!list. list ∈ set a ==> non_zero_spvec (snd list) = 0"
using contrad by auto
show False
using null_comp
using non_zero_a
using non_zero_spmat.simps by (induct a) auto
qed
lemma non_zero_spvec_impl_sp_rw_vector:
assumes non_zero_spvec: "non_zero_spvec A = 0"
shows "sparse_row_vector A = (0::'a::lordered_ring matrix)"
using non_zero_spvec proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "(nat × 'a)"
fix A :: "(nat × 'a) list"
assume hypo: "non_zero_spvec A = 0 ==> sparse_row_vector A = 0"
and prem: "non_zero_spvec (a # A) = 0"
show "sparse_row_vector (a # A) = 0"
proof -
have nz_A_0: "non_zero_spvec A = (0::nat)"
using prem unfolding non_zero_spvec.simps
by (cases "snd a = 0") auto
have sa_0: "snd a = 0"
using prem unfolding non_zero_spvec.simps
by (cases "snd a = 0") auto
have srv: "sparse_row_vector A = 0" using hypo [OF nz_A_0] .
show ?thesis
unfolding sparse_row_vector_cons
unfolding srv
using prem
unfolding non_zero_spvec.simps (2)
unfolding sa_0
unfolding singleton_matrix_zero [of 0 "fst a"] by simp
qed
}
qed
lemma Rep_matrix_inject_exp:
shows "(A = B) = (∀j i. Rep_matrix A j i = Rep_matrix B j i)"
unfolding sym [OF Rep_matrix_inject [of "A" "B"]]
unfolding expand_fun_eq by simp
lemma move_matrix_zero_le2:
assumes j: "0 ≤ j" and i: "0 ≤ i"
shows "(0 = move_matrix A j i) = ((0::('a::{order,zero}) matrix) = A)"
unfolding Rep_matrix_inject_exp [of "0" "move_matrix A j i"]
unfolding Rep_matrix_inject_exp [of "0" "A"]
apply (auto simp add: neg_def)
apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
using i j by auto
lemma Abs_matrix_inject3:
assumes x: "x ∈ matrix"
and y: "y ∈ matrix"
and eq: "Abs_matrix x = Abs_matrix y"
shows "x = y"
using Abs_matrix_inject [OF x y] using eq ..
lemma Abs_matrix_ne:
assumes x: "x ∈ matrix"
and y: "y ∈ matrix"
and eq: "x ≠ y"
shows "Abs_matrix x ≠ Abs_matrix y"
proof (rule ccontr)
assume contr: "¬ Abs_matrix x ≠ Abs_matrix y"
show False using contr Abs_matrix_inject3 [OF x y] eq by simp
qed
lemma singl_mat_zero:
assumes singl_mat: "singleton_matrix i j x = 0"
shows "x = (0::'a::zero)"
proof (rule ccontr)
assume contr: "x ≠ 0"
have singl_mat_ne: "singleton_matrix i j x ≠ 0"
proof -
have "{pos. (if i = fst pos ∧ j = snd pos
then x else 0) ≠ 0} ⊆ {(i,j)}" using contr by auto
moreover have "finite {(i, j)}" by simp
ultimately have "finite {pos. (if i = fst pos ∧ j = snd pos
then x else 0) ≠ 0}"
using finite_subset [of _ "{(i, j)}"] by simp
then have "(λm n. if i = m ∧ j = n then x else 0) ∈ matrix"
unfolding matrix_def unfolding nonzero_positions_def
unfolding mem_Collect_eq .
moreover have "(λj i. 0::'a) ∈ matrix"
unfolding matrix_def unfolding nonzero_positions_def
by simp
moreover have "(λm n. if i = m ∧ j = n then x else 0) ≠ (λj i. 0::'a)"
using contr by (simp add: expand_fun_eq)
ultimately have "Abs_matrix (λm n. if i = m ∧ j = n then x else 0) ≠
Abs_matrix (λj i. 0::'a)" using Abs_matrix_ne by auto
then show ?thesis
unfolding singleton_matrix_def
unfolding zero_matrix_def .
qed
thus False using singl_mat ..
qed
lemma zero_impl_sing_mat_zero:
assumes x_zero: "x = (0::'a::zero)"
shows "singleton_matrix i j x = 0"
unfolding singleton_matrix_def
unfolding zero_matrix_def
by (rule cong [of "Abs_matrix" "Abs_matrix"]) (simp_all add: expand_fun_eq x_zero)
lemma singl_mat_not_zero:
assumes singl_mat: "singleton_matrix i j x ≠ 0"
shows "x ≠ (0::'a::zero)"
proof (rule ccontr)
assume contr: "¬ x ≠ (0::'a)"
show False
using contr
using zero_impl_sing_mat_zero [of x i j]
using singl_mat by fast
qed
text{*The following lemma is the first one where we had to add the
sortedness property of vectors.*}
text{*The following lemmas will allow us to relate our definition of the zero
matrix for the type @{typ "'a spmat"}, i.e., @{term "non_zero_spmat"},
with the one of the zero matrix for type @{typ "'a matrix"}.*}
lemma sparse_row_vector_zero_impl_non_zero_spvec:
assumes sp_r: "sparse_row_vector A = 0"
and srtd: "sorted_spvec A"
shows "non_zero_spvec A = 0"
using sp_r srtd proof (induct A)
case Nil
{
show ?case by simp
}
next
case Cons
{
fix a :: "(nat × 'a)"
fix A :: "(nat × 'a) list"
assume hyp: "[| sparse_row_vector A = 0; sorted_spvec A |]
==> non_zero_spvec A = 0"
and prem1: "sparse_row_vector (a # A) = 0"
and prem2: "sorted_spvec (a # A)"
show "non_zero_spvec (a # A) = 0"
proof (cases "sparse_row_vector A = 0")
case True
{
have n_z_sp: "non_zero_spvec A = 0"
using hyp [OF True sorted_spvec_cons1 [OF prem2]] .
have snd_a_0: "snd a = 0"
using prem1
unfolding sparse_row_vector_cons
unfolding True
using singl_mat_zero [of 0 "fst a" "snd a"] by simp
show ?thesis
using n_z_sp
using snd_a_0 non_zero_spvec.simps (2) [of a A] by simp
}
next
case False
{
have "0 = singleton_matrix 0 (fst a) (snd a) + sparse_row_vector A"
using sparse_row_vector_cons [of a A] prem1 by simp
also have "… = singleton_matrix 0 (fst a) (snd a) - (- sparse_row_vector A)"
by simp
finally have "0 = singleton_matrix 0 (fst a) (snd a) - (- sparse_row_vector A)"
by simp
with eq_iff_diff_eq_0 [of "singleton_matrix 0 (fst a) (snd a)"
"- sparse_row_vector A"]
have "- sparse_row_vector A = singleton_matrix 0 (fst a) (snd a)"
by simp
then have "- (- sparse_row_vector A) = - singleton_matrix 0 (fst a) (snd a)"
by simp
then have sp_row_vector_A: "sparse_row_vector A = - (singleton_matrix 0 (fst a) (snd a))"
by simp
have snd_a_not_zero: "snd a ≠ 0"
using sp_row_vector_A
using False
using singl_mat_not_zero [of 0 "fst a" "snd a"] by simp
have disj_matr: "disj_matrices (sparse_row_vector A) (singleton_matrix 0 (fst a) (snd a))"
using disj_sparse_row_singleton [of "fst a" "fst a" "snd a" "A" "snd a"]
using prem2 by simp
then have False
unfolding sp_row_vector_A
using snd_a_not_zero
unfolding disj_matrices_def apply auto
using spec2 [of "(λj i. (if j = 0 ∧ fst a = i then snd a else 0) = 0)" 0 "fst a"]
by simp
thus ?thesis ..
}
qed
}
qed
lemma sorted_sparse_matrix_cons2:
assumes srtd: "sorted_sparse_matrix (a # b # A)"
shows "sorted_sparse_matrix (a # A)"
using srtd
unfolding sorted_sparse_matrix_def
using sorted_spvec_cons2 [of a b A]
unfolding sorted_spmat.simps by fast
lemma disj_matrices_A_minus_A:
assumes A_not_zero: "(A::'a::lordered_ring matrix) ≠ 0"
shows "¬ (disj_matrices A (- A))"
proof -
have ne: "∃i j. Rep_matrix A i j ≠ 0"
proof (rule ccontr)
assume not_ex: "¬ (∃i j. Rep_matrix A i j ≠ (0::'a))"
then have "∀i j. Rep_matrix A i j = 0" by simp
then have "Rep_matrix A = (λi j. 0)"
unfolding expand_fun_eq .
then have "Rep_matrix A = Rep_matrix (Abs_matrix (λi j. 0))"
using sym [OF RepAbs_matrix [of "(λi j. (0::'a))"]] by auto
then have "A = Abs_matrix (λi j. 0)"
using Rep_matrix_inject [of A "Abs_matrix (λi j. 0::'a)"] by fast
with A_not_zero show False unfolding zero_matrix_def ..
qed
then obtain i j where Rep_not_zero: "Rep_matrix A i j ≠ 0" by fast
then have Rep_minus_A_not_zero: "Rep_matrix (- A) i j ≠ 0"
unfolding Rep_minus [of A i j] by simp
show ?thesis
using Rep_not_zero
using Rep_minus_A_not_zero
unfolding disj_matrices_def by auto
qed
lemma sorted_sparse_matrix_cons:
assumes srtd: "sorted_sparse_matrix (a # A)"
shows "sorted_sparse_matrix A"
using srtd
unfolding sorted_sparse_matrix_def
using sorted_spvec_cons1 [of a A]
using sorted_spmat.simps (2) [of a A] by fast
text{*The following lemma proves the equivalence between the zero matrix
and our definition of zero as a sparse matrix. The lemma requires
the sparse matrix to be sorted.*}
lemma sparse_row_matrix_zero_eq_non_zero_spmat_zero:
assumes sorted_sp_mat_A: "sorted_sparse_matrix A"
shows "(sparse_row_matrix A = (0::'a::lordered_ring matrix))
= (non_zero_spmat A = (0::nat))"
using sorted_sp_mat_A proof (induct A)
case Nil
{
show "?case" by simp
}
next
case Cons
{
fix a :: "nat × 'a spvec"
fix A :: "'a spmat"
assume hypo: "sorted_sparse_matrix A ==>
(sparse_row_matrix A = 0) = (non_zero_spmat A = 0)"
and prem: "sorted_sparse_matrix (a # A)"
show "(sparse_row_matrix (a # A) = 0) = (non_zero_spmat (a # A) = 0)"
proof (rule iffI)
show "non_zero_spmat (a # A) = 0 ==> sparse_row_matrix (a # A) = 0"
proof -
assume non_zero_spmat: "non_zero_spmat (a # A) = 0"
show "sparse_row_matrix (a # A) = 0"
proof (cases "non_zero_spmat A = 0")
case False
{
have False
using False
using non_zero_spmat
using non_zero_spmat.simps
using non_zero_spvec.simps by simp
then show ?thesis ..
}
next
case True
{
have sp_r_mat_A: "sparse_row_matrix A = 0"
using True
using prem
using hypo
using sorted_sparse_matrix_cons [of a A] by simp
have non_zero_a: "non_zero_spvec (snd a) = 0"
using non_zero_spmat by simp
have sp_row_zero: "sparse_row_vector (snd a) = 0"
using non_zero_spvec_impl_sp_rw_vector [OF non_zero_a] .
show ?thesis
unfolding sparse_row_matrix_cons [of a A]
unfolding sp_r_mat_A apply simp
unfolding sp_row_zero unfolding move_matrix_def
unfolding Rep_zero_matrix_def
unfolding zero_matrix_def
apply (rule cong [of "Abs_matrix" "Abs_matrix"])
unfolding expand_fun_eq by auto
}
qed
qed
next
show "sparse_row_matrix (a # A) = 0 ==> non_zero_spmat (a # A) = 0"
proof -
assume sp_row_matrix: "sparse_row_matrix (a # A) = 0"
have srtd: "sorted_spvec (snd a)"
using prem
unfolding sorted_sparse_matrix_def
unfolding sorted_spmat.simps (2) by fast
show "non_zero_spmat (a # A) = 0"
proof (cases "sparse_row_matrix A = 0")
case True
{
have non_zero_spmat_A: "non_zero_spmat A = 0"
using hypo [OF sorted_sparse_matrix_cons [OF prem]]
using True ..
have m_m: "move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0 = 0"
using sparse_row_matrix_cons [of a A]
unfolding True
unfolding sp_row_matrix by simp
have sp_ro_vc_0: "(sparse_row_vector (snd a)) = 0"
using move_matrix_zero_le2 [of "int (fst a)" 0 "sparse_row_vector (snd a)"]
using m_m by simp
show "non_zero_spmat (a # A) = 0"
unfolding non_zero_spmat.simps (2)
unfolding non_zero_spmat_A
unfolding sparse_row_vector_zero_impl_non_zero_spvec [OF sp_ro_vc_0 srtd]
by simp
}
next
case False
{
have srtd_spmat: "sorted_spmat (a # A)"
using prem
unfolding sorted_sparse_matrix_def ..
then have srtd_spvec: "sorted_spvec (snd a)"
unfolding sorted_spmat.simps (2) ..
have disj_matrices_move_matrix:
"disj_matrices (move_matrix (sparse_row_vector (snd a))
(int (fst a)) 0)
(sparse_row_matrix A)"
using srtd_spvec proof (induct "snd a")
case Nil
{
show ?case
unfolding sparse_row_vector_empty
unfolding move_matrix_zero
using disj_matrices_zero1 .
}
next
case Cons
{
fix b :: "(nat × 'a)"
fix v :: "(nat × 'a) list"
assume hypo: "sorted_spvec v
==> disj_matrices (move_matrix (sparse_row_vector v)
(int (fst a)) 0) (sparse_row_matrix A)"
assume prem_induct: "sorted_spvec (b # v)"
have disj_matrix: "disj_matrices (move_matrix (sparse_row_vector v)
(int (fst a)) 0) (sparse_row_matrix A)"
using hypo [OF sorted_spvec_cons1 [OF prem_induct]] .
show "disj_matrices (move_matrix (sparse_row_vector (b # v))
(int (fst a)) 0) (sparse_row_matrix A)"
unfolding sparse_row_vector_cons
unfolding move_matrix_add
unfolding move_matrix_singleton
apply simp
apply (cases "snd b = 0", auto simp add: disj_matrix)
unfolding disj_matrices_commute
apply (rule disj_matrices_x_add)
prefer 2
using disj_matrix
unfolding disj_matrices_commute apply simp
using prem proof (induct A)
case Nil
{
show ?case
unfolding sparse_row_matrix_empty by simp
}
next
case Cons
{
fix c :: "nat × (nat × 'a) list"
fix C :: "'a spmat"
assume hypo: "[|snd b ≠ 0; sorted_sparse_matrix (a # C)|] ==>
disj_matrices (sparse_row_matrix C)
(singleton_matrix (fst a) (fst b) (snd b))"
and snd_b: "snd b ≠ 0"
and srtd_hypo: "sorted_sparse_matrix (a # c # C)"
show "disj_matrices (sparse_row_matrix (c # C))
(singleton_matrix (fst a) (fst b) (snd b))"
unfolding sparse_row_matrix_cons
unfolding move_matrix_add
unfolding disj_matrices_commute
apply (rule disj_matrices_x_add)
proof -
show "disj_matrices (singleton_matrix (fst a) (fst b) (snd b))
(sparse_row_matrix C)"
using hypo [OF snd_b sorted_sparse_matrix_cons2 [OF srtd_hypo]]
unfolding disj_matrices_commute .
show "disj_matrices (singleton_matrix (fst a) (fst b) (snd b))
(move_matrix (sparse_row_vector (snd c)) (int (fst c)) 0)"
using snd_b srtd_hypo
unfolding disj_matrices_def
unfolding sorted_sparse_matrix_def
unfolding sorted_spmat.simps
using sorted_spvec_cons3 [of a c C]
apply auto unfolding neg_def by arith
qed
}
qed
}
qed
have "0 = (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0)
+ (sparse_row_matrix A)"
using sp_row_matrix
unfolding sparse_row_matrix_cons ..
also have "… = (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0)
- (- (sparse_row_matrix A))" by simp
finally have "0 = (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0)
- (- (sparse_row_matrix A))" by simp
then have "- sparse_row_matrix A
= (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0)"
using eq_iff_diff_eq_0 [of "(move_matrix (sparse_row_vector (snd a))
(int (fst a)) 0)" "- sparse_row_matrix A"] by simp
then have "- (- sparse_row_matrix A) =
- (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0)"
by simp
then have sp_minus_move: "sparse_row_matrix A
= - (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0)"
by simp
have False
using disj_matrices_A_minus_A [OF False]
unfolding disj_matrices_commute [of "sparse_row_matrix A"]
using disj_matrices_move_matrix
unfolding sp_minus_move by simp
then show ?thesis ..
}
qed
qed
qed
}
qed
text{*The computation of the bound is now made by means of a For loop,
where the terminating condition is to get to a null matrix.*}
text{*The process is similar to the one applied in the constructive version in the BPL,
but using sparse matrices instead of matrices.*}
definition local_bound_gen_spmat ::
"(('a::lordered_ring) spmat => 'a spmat) => ('a spmat) => nat => nat"
where "local_bound_gen_spmat f A n
= For (λ y. non_zero_spmat y ≠ 0) f (λ y n. n + (1::nat)) A n"
definition local_bound_spmat ::
"(('a::lordered_ring) spmat => 'a spmat) => ('a spmat) => nat"
where "local_bound_spmat f A ≡ local_bound_gen_spmat f A 0"
text{*We also need a definition of the summation of the power series
of a given matrix up to a given bound.*}
primrec fin_sum_spmat
:: "(('a::lordered_ring) spmat => 'a spmat) => ('a spmat) => nat => 'a spmat"
where "fin_sum_spmat f A 0 = A"
| "fin_sum_spmat f A (Suc n) = add_spmat ((f^(Suc n)) A, fin_sum_spmat f A n)"
text{*With the previous definitions we are ready to give
the definition of @{term "α"} and @{term "Φ"} for sparse matrices.*}
definition α_spmat :: "('a::lordered_ring) spmat => 'a spmat"
where "α_spmat A = (minus_spmat (pert_spmat_sort (hom_oper_spmat A)))"
text{*The following definition is the one to be
later compared to the one of @{term Φ}*}
definition Φ_spmat :: "('a::lordered_ring) spmat => 'a spmat"
where "Φ_spmat A = fin_sum_spmat α_spmat A (local_bound_spmat α_spmat A)"
definition example_zero :: "int spmat"
where "example_zero == [(3::nat, [((3::nat), (5::int))])]"
definition example_one :: "int spmat"
where"example_one ==
(0::nat, (0::nat, 5::int) # (2, - 9) # (6, 8) # [])
# (1::nat, (1::nat, 4::int) # (2, 0) # (8, 8) # [])
# (2::nat, (2::nat, 6::int) # (3, 7) # (9, 23) # [])
# (16::nat, (13::nat, -8::int) # (19, 12) # [])
# (29::nat, (3::nat, 5::int) # (4, 6) # (7, 8) # [])
# []"
definition example_one' :: "int spmat"
where "example_one' == (0::nat, (0::nat, 0::int) # (2, 0) # (6, 0) # [])
# (1::nat, (1::nat, 0::int) # (2, 0) # (8, 0) # [])
# (2::nat, (2::nat, 0::int) # (3, 0) # (9, 0) # [])
# (29::nat, (3::nat, 0::int) # (4, 0) # (7, 0) # [])
# []"
lemma alpha_execute_sparse:
shows "α (sparse_row_matrix (A::'a::lordered_ring spmat))
= sparse_row_matrix (α_spmat A)"
unfolding α_spmat_def
unfolding sparse_row_matrix_minus [of "pert_spmat_sort (hom_oper_spmat A)"]
unfolding sym [OF sparse_row_matrix_pert_spmat_eq_pert_spmat_sort
[of "(hom_oper_spmat A)"]]
unfolding sparse_row_matrix_pert_spmat
unfolding sym [OF pert_matrix1_execute_sparse [of "(hom_oper_spmat A)"]]
unfolding sparse_row_matrix_hom_oper_spmat
unfolding sym [OF hom_oper_matrix1_execute_sparse [of A]]
unfolding α_def unfolding hom_oper_matrix_def unfolding pert_matrix_def ..
lemma fun_matrix_add:
shows "((f::'a matrix => 'a matrix) + g) (A::'a::lordered_ring matrix) = f A + g A"
unfolding plus_fun_def by simp
lemma nth_power_execute_sparse:
fixes f :: "'a matrix => 'a::lordered_ring matrix"
fixes f_spmat :: "'a spmat => 'a spmat"
assumes f_exec: "!!A. f (sparse_row_matrix A)
= sparse_row_matrix (f_spmat A)"
shows "(f ^ n) (sparse_row_matrix A)
= sparse_row_matrix ((f_spmat^n) A)"
proof (induct n)
case 0
{
show "(f^ 0) (sparse_row_matrix A)
= sparse_row_matrix ((f_spmat ^ 0) A)" by simp
}
next
case Suc
{
fix n::nat
assume hyps: "(f ^ n) (sparse_row_matrix A)
= sparse_row_matrix ((f_spmat ^ n) A)"
show "(f ^ (Suc n)) (sparse_row_matrix A)
= sparse_row_matrix ((f_spmat ^ (Suc n)) A)"
using hyps
apply simp
using f_exec [of "(f_spmat ^ n) A"] by simp
}
qed
corollary alpha_nth_power_execute_sparse:
shows "(α ^ n) (sparse_row_matrix A)
= sparse_row_matrix ((α_spmat^n) A)"
using alpha_execute_sparse
using nth_power_execute_sparse [of α α_spmat] by auto
lemma fin_sum_alpha_up_to_n_execute_sparse:
shows "fin_sum α n (sparse_row_matrix A)
= sparse_row_matrix (fin_sum_spmat α_spmat A n)"
proof (induct n)
case 0
show ?case by simp
next
case Suc
fix n
assume hyps: "fin_sum α n (sparse_row_matrix A)
= sparse_row_matrix (fin_sum_spmat α_spmat A n)"
show "fin_sum α (Suc n) (sparse_row_matrix A)
= sparse_row_matrix (fin_sum_spmat α_spmat A (Suc n))"
unfolding fin_sum.simps(2) [of "α" "n"]
unfolding fin_sum_spmat.simps(2)
unfolding sparse_row_add_spmat
unfolding fun_matrix_add
unfolding hyps
unfolding alpha_nth_power_execute_sparse [of "Suc n" A] ..
qed
lemma fin_sum_up_to_n_execute_sparse':
assumes m_eq_n: "m = n"
shows "fin_sum α m (sparse_row_matrix A)
= sparse_row_matrix (fin_sum_spmat α_spmat A n)"
using fin_sum_alpha_up_to_n_execute_sparse m_eq_n by simp
lemma sorted_sparse_matrix_add_spmat:
assumes srtd_A: "sorted_sparse_matrix A"
and srtd_B: "sorted_sparse_matrix B"
shows "sorted_sparse_matrix (add_spmat (A, B))"
using srtd_A srtd_B
unfolding sorted_sparse_matrix_def
using sorted_spvec_add_spmat [of A B]
using sorted_spmat_add_spmat [of A B] by simp
text{*As we have proved, the @{text "hom_oper_spmat"} operation preserves order*}
lemma "sorted_spvec (α_spmat example_one)"
unfolding α_spmat_def
unfolding example_one_def
apply (simp only: hom_oper_spmat.simps Let_def)
apply (simp del: pert_spmat.simps minus_spmat.simps)
apply (simp only: pert_spmat.simps Let_def)
apply (simp del: minus_spmat.simps)
apply (simp del:sorted_spvec.simps)
unfolding sorted_spvec.simps by simp
lemma sorted_spvec_alpha_spmat:
assumes srtd: "sorted_spvec A"
shows "sorted_spvec (α_spmat A)"
unfolding α_spmat_def
using sorted_spvec_minus_spmat
[OF sorted_spvec_pert_spmat_sort
[OF sorted_spvec_hom_oper [OF srtd]]] .
lemma sorted_spvec_alpha_spmat_nth:
assumes srtd: "sorted_spvec A"
shows "sorted_spvec ((α_spmat^n) A)"
proof (induct n)
case 0 show ?case by simp
next
case Suc
fix n
assume hypo: "sorted_spvec ((α_spmat^n) A)"
show "sorted_spvec ((α_spmat^(Suc n)) A)"
using sorted_spvec_alpha_spmat [OF hypo] by simp
qed
lemma sorted_spmat_alpha_spmat:
shows "sorted_spmat (α_spmat A)"
unfolding α_spmat_def
using sorted_spmat_minus_spmat
[OF sorted_spmat_pert_spmat_sort
[of "hom_oper_spmat A"]] .
lemma sorted_spmat_alpha_spmat_nth:
assumes srtd_A: "sorted_spmat A"
shows "sorted_spmat ((α_spmat^n) A)"
proof (induct n)
case 0
{
show ?case
using srtd_A by simp
}
next
case Suc
{
fix n
assume hypo: "sorted_spmat ((α_spmat^n) A)"
show "sorted_spmat ((α_spmat ^ Suc n) A)"
using sorted_spmat_alpha_spmat by simp
}
qed
lemma sorted_sparse_matrix_alpha:
assumes ssm: "sorted_sparse_matrix A"
shows "sorted_sparse_matrix (α_spmat A)"
using ssm
unfolding sorted_sparse_matrix_def
using sorted_spvec_alpha_spmat [of A]
using sorted_spmat_alpha_spmat [of A] by fast
lemma sorted_sparse_matrix_alpha_nth:
assumes ssm: "sorted_sparse_matrix A"
shows "sorted_sparse_matrix ((α_spmat^n) A)"
using ssm
unfolding sorted_sparse_matrix_def
using sorted_spvec_alpha_spmat_nth [of A]
using sorted_spmat_alpha_spmat_nth [of A] by fast
subsection{*Equivalence between the local nilpotency bound
for sparse matrices and matrices.*}
lemma local_bounded_func_α_matrix:
shows "local_bounded_func (α::'a::lordered_ring matrix => 'a matrix)"
unfolding local_bounded_func_def
using nrows_strict_decr [OF nrows_alpha_decre]
using nrows_zero_impl_zero by auto
corollary α_matrix_terminates:
shows "terminates ((λy. y ≠ 0),
α::'a::lordered_ring matrix => 'a matrix,
sparse_row_matrix A)"
using local_bounded_func_α_matrix
unfolding local_bounded_func_impl_terminates_loop ..
lemma local_bound_spmat:
shows "local_bound α (sparse_row_matrix A)
= (LEAST n. sparse_row_matrix (
(α_spmat ^ n) (A::'a::lordered_ring spmat)) = (0::'a matrix))"
unfolding local_bounded_func_impl_local_bound_is_Least
[OF local_bounded_func_α_matrix, of "sparse_row_matrix A"]
unfolding alpha_nth_power_execute_sparse ..
lemma local_bound_spmat_termin:
shows "local_bound α (sparse_row_matrix A) =
(LEAST n. sparse_row_matrix (
(α_spmat ^ n) (A::'a::lordered_ring spmat)) = (0::'a matrix))"
unfolding local_bound_correct [OF α_matrix_terminates]
unfolding alpha_nth_power_execute_sparse [of _ A] ..
lemma least_eq:
assumes eq: "∀n::nat. f n = g n"
shows "(LEAST n. f n) = (LEAST n. g n)"
using eq by simp
lemma LEAST_execute_sparse:
assumes ssm: "sorted_sparse_matrix A"
shows "(LEAST n. sparse_row_matrix
((α_spmat ^ n) (A::'a::lordered_ring spmat)) = (0::'a matrix)) =
(LEAST n. non_zero_spmat
((α_spmat ^ n) (A::'a::lordered_ring spmat)) = (0::nat))"
proof (rule least_eq, rule allI)
fix n
show "(sparse_row_matrix ((α_spmat ^ n) A) = 0)
= (non_zero_spmat ((α_spmat ^ n) A) = 0)"
using sparse_row_matrix_zero_eq_non_zero_spmat_zero
[OF sorted_sparse_matrix_alpha_nth [OF ssm, of n]] .
qed
lemma local_bound_alpha_spmat:
assumes ssm: "sorted_sparse_matrix A"
shows "local_bound α (sparse_row_matrix A)
= (LEAST n. non_zero_spmat (
(α_spmat ^ n) (A::'a::lordered_ring spmat)) = (0::nat))"
unfolding local_bound_spmat
unfolding LEAST_execute_sparse [OF ssm] ..
text{*Make the simplification rule for @{term "local_bound_gen"}: *}
lemmas local_bound_gen_spmat_simp =
For_simp[of "(λ y. non_zero_spmat y ≠ (0::nat))" _ "λ y n. n+(1::nat)",
simplified local_bound_gen_spmat_def[symmetric]]
text{*Now, we connect the neccesary termination of
For with our termination condition, @{term local_bounded_func}. *}
text{*Then, under the @{term local_bounded_func} premise
the loop will be terminating.*}
lemma local_bounded_func_alpha_impl_terminates_loop:
"local_bounded_func (α::'a matrix => 'a matrix)
= (∀ x. terminates (λ y. y ≠ 0, α, (x::'a::lordered_ring matrix)))"
unfolding local_bounded_func_impl_terminates_loop ..
text{*The following lemma transfers the condition of termination
from matrices to sparse matrices.*}
lemma local_bounded_func_alpha_impl_terminates_loop_spmat:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
shows "terminates (λy. y ≠ 0, α, sparse_row_matrix A)
= terminates (λy. non_zero_spmat y ≠ (0::nat), α_spmat, A)"
unfolding terminates.simps
unfolding Orbit_def
unfolding alpha_nth_power_execute_sparse
using sparse_row_matrix_zero_eq_non_zero_spmat_zero
[OF sorted_sparse_matrix_alpha_nth [OF ssm]] by auto
lemma local_bounded_func_impl_terminates_spmat_loop:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
shows "terminates (λ y. non_zero_spmat y ≠ (0::nat), α_spmat, A)"
using local_bounded_func_α_matrix
unfolding local_bounded_func_alpha_impl_terminates_loop
using local_bounded_func_alpha_impl_terminates_loop_spmat [OF ssm]
by auto
lemma LEAST_local_bound_non_zero_spmat:
assumes is_zero: "non_zero_spmat A = 0"
shows "(LEAST n::nat. non_zero_spmat ((α_spmat ^ n) A) = (0::nat)) = 0"
using Least_le [of "λn. non_zero_spmat ((α_spmat ^n) A) = 0" 0]
using is_zero by simp
lemma local_bound_gen_spmat_correct:
"terminates (λ y. non_zero_spmat y ≠ (0::nat), α_spmat, A)
==> local_bound_gen_spmat α_spmat A m
= m + (LEAST n::nat. non_zero_spmat ((α_spmat^n) A) = 0)"
unfolding local_bound_gen_spmat_def
proof (rule For_pinduct
[where i=A
and s=m
and Ac="λ y n. n+1"
and continue="λy. non_zero_spmat y ≠ (0::nat)"
and f="α_spmat"])
show "terminates (λy. non_zero_spmat y ≠ 0, α_spmat, A)
==> terminates (λy. non_zero_spmat y ≠ 0, α_spmat, A)" .
next
fix i s
assume termin_A: "terminates (λy. non_zero_spmat y ≠ 0, α_spmat, A)"
and termin_i: "terminates (λy. non_zero_spmat y ≠ 0, α_spmat, i)"
and hypo: "non_zero_spmat i ≠ 0 ==>
For (λy. non_zero_spmat y ≠ 0)
α_spmat (λy n. n + 1) (α_spmat i) (s + 1) =
s + 1 + (LEAST n. non_zero_spmat ((α_spmat ^ n)
(α_spmat i)) = 0)"
show "For (λy. non_zero_spmat y ≠ 0) α_spmat (λy n. n + 1) i s
= s + (LEAST n. non_zero_spmat ((α_spmat ^ n) i) = 0)"
proof (cases "non_zero_spmat i = 0")
case True
{
show ?thesis
unfolding LEAST_local_bound_non_zero_spmat [OF True]
using True
using For_simp [of "(λy. non_zero_spmat y ≠ 0)" α_spmat "(λy n. n + 1)" i s]
by simp
}
next
case False
{
from hypo and False
have For_rew:
"For (λy. non_zero_spmat y ≠ 0)
α_spmat (λy n. n + 1) (α_spmat i) (s + 1) =
s + 1 + (LEAST n. non_zero_spmat
((α_spmat ^ n) (α_spmat i)) = 0)" by simp
obtain m where vanish_i: "non_zero_spmat ((α_spmat ^ m) i) = 0"
using terminates_implies [OF termin_i] by auto
have "0 < m"
using False
using vanish_i by (cases "m = 0") auto
from this and vanish_i
have vanish_alpha_i: "non_zero_spmat ((α_spmat ^ (m - 1)) (α_spmat i)) = 0"
using funpow_zip [of "α_spmat" "m - 1" i] by auto
show ?thesis
unfolding For_simp [of "(λy. non_zero_spmat y ≠ 0)"
α_spmat "(λy n. n + 1)" i s]
unfolding For_rew
apply (simp add: False)
proof (rule Least_Suc2[symmetric, of _ m _ "m - 1"])
show "non_zero_spmat ((α_spmat ^ m) i) = 0"
using vanish_i by simp
show "non_zero_spmat ((α_spmat ^ (m - 1)) (α_spmat i)) = 0"
using vanish_alpha_i by simp
show "non_zero_spmat ((α_spmat ^ 0) i) ≠ 0"
using False by simp
show "∀k. (non_zero_spmat ((α_spmat ^ Suc k) i) = 0)
= (non_zero_spmat ((α_spmat ^ k) (α_spmat i)) = 0)"
using funpow_zip [of α_spmat _ i] by auto
qed
}
qed
qed
text{*The following lemma exactly represents the difference between our
old definitions, with which we proved the BPL, and the new ones,
from which we are trying to generate code;
under the termination premise, both
@{term "(LEAST n::nat. (f^n) (x::'a::ab_group_add) = 0)"},
the old definition of local nilpotency,
and @{term [locale=ab_group_add] "local_bound f x"}, the loop computing the lower bound,
are equivalent*}
text{*Whereas @{term "(LEAST n::nat. (f^n) (x::'a::ab_group_add) = 0)"}
does not have a computable interpretation,
@{term [locale=ab_group_add] "local_bound f x"} does have it,
and code can be generated from it.*}
lemma local_bound_spmat_correct:
"terminates (λ y. non_zero_spmat y ≠ (0::nat), α_spmat, A) ==>
local_bound_spmat α_spmat A = (LEAST n::nat. non_zero_spmat ((α_spmat^n) A) = 0)"
unfolding local_bound_spmat_def
unfolding local_bound_gen_spmat_correct [of A 0] by arith
lemma local_bounded_func_impl_local_bound_spmat_is_Least:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
shows "local_bound_spmat α_spmat A
= (LEAST n::nat. non_zero_spmat ((α_spmat^n) A) = 0)"
unfolding local_bound_spmat_correct
[OF local_bounded_func_impl_terminates_spmat_loop
[OF ssm]] ..
lemma local_bound_eq_local_bound_spmat:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
shows "local_bound_spmat α_spmat A
= local_bound α (sparse_row_matrix A)"
unfolding local_bounded_func_impl_local_bound_spmat_is_Least
[OF ssm]
unfolding sym [OF local_bound_alpha_spmat [OF ssm]] ..
lemma phi_execute_sparse:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
shows "sparse_row_matrix (Φ_spmat A)
= (Φ::'a::lordered_ring matrix => 'a matrix) (sparse_row_matrix A)"
unfolding Φ_def
unfolding sym [OF local_bound_eq_local_bound_spmat [OF ssm]]
unfolding fin_sum_alpha_up_to_n_execute_sparse
unfolding Φ_spmat_def ..
subsection{*Some examples of code generation.*}
text{*It must be noted that these examples execute the definitions over sparse matrices,
and are carried out by means of Haftmann',s code generation tool.*}
text{*Consequently, they are not computed directly over the definitions on
@{typ "'a matrix"}, which were the ones proved to be an instance of the BPL.*}
text{*Later we will use the HCL to carry out computations with the definitions
over the type @{typ "'a matrix"}.*}
text{*The value operator is rather slow even for easy examples*}
value example_zero
value "α_spmat example_zero"
definition foos:: "int spmat"
where "foos == transpose_spmat [(3::nat, [((4::nat), (5::int))])]"
definition foos1:: "int spmat"
where "foos1 == (α_spmat^(1::nat)) example_zero"
definition foos2:: "int spmat"
where"foos2 == (α_spmat^(2::nat)) example_zero"
definition foos3:: "int spmat"
where "foos3 == (α_spmat^(3::nat)) example_zero"
definition foos4:: "int spmat"
where "foos4 == (α_spmat^(4::nat)) example_zero"
definition foos5:: "int spmat"
where "foos5 == (α_spmat^(5::nat)) example_zero"
definition foos6:: "int spmat"
where "foos6 == (α_spmat^(6::nat)) example_zero"
definition foos7:: "int spmat"
where "foos7 == (α_spmat^(7::nat)) example_zero"
definition foos_local_bound :: "nat"
where "foos_local_bound == local_bound_spmat α_spmat example_zero"
definition foos_Phi:: "int spmat"
where "foos_Phi == Φ_spmat example_zero"
definition goos:: "int spmat"
where "goos == transpose_spmat example_one"
definition goos1:: "int spmat"
where "goos1 == (α_spmat^(1::nat)) example_one"
definition goos2:: "int spmat"
where "goos2 == (α_spmat^(2::nat)) example_one"
definition goos3:: "int spmat"
where "goos3 == (α_spmat^(3::nat)) example_one"
definition goos4:: "int spmat"
where "goos4 == (α_spmat^(4::nat)) example_one"
definition goos5:: "int spmat"
where "goos5 == (α_spmat^(5::nat)) example_one"
definition goos6:: "int spmat"
where "goos6 == (α_spmat^(6::nat)) example_one"
definition goos7:: "int spmat"
where "goos7 == (α_spmat^(7::nat)) example_one"
definition goos30:: "int spmat"
where "goos30 == (α_spmat^(local_bound_spmat α_spmat example_one)) example_one"
text{*We can also compare a matrix to the zero matrix*}
definition goos30_eq_0:: "bool"
where "goos30_eq_0 = (non_zero_spmat ((α_spmat^(local_bound_spmat
α_spmat example_one)) example_one) = (0::nat))"
definition goos_local_bound::nat
where "goos_local_bound = local_bound_spmat α_spmat example_one"
definition goos_Phi:: "int spmat"
where "goos_Phi == Φ_spmat example_one"
definition blaa :: "int spmat"
where "blaa == hom_oper_spmat example_one"
definition blaa_square:: "int spmat"
where "blaa_square == (hom_oper_spmat^2) example_one"
definition blaa_three:: "int spmat"
where "blaa_three == (hom_oper_spmat^3) example_one"
definition blaas:: "int spmat"
where "blaas == pert_spmat example_one"
definition blaas_square:: "int spmat"
where "blaas_square == (pert_spmat^2) example_one"
text{*The following are just examples of the code generated from the
Isabelle definitions over sparse matrices in order to check
that they are compatible with the code generation facility.*}
export_code blaa blaa_square blaa_three blaas blaas_square
goos goos1 goos2 goos3 goos4 goos5 goos6 goos7 goos30
goos30_eq_0
goos_local_bound goos_Phi
foos foos1 foos2 foos3 foos4 foos5 foos6 foos7
foos_local_bound foos_Phi
in SML module_name "example_Bicomplex"
file "example_Bicomplex.ML"
use "example_Bicomplex.ML"
ML "open example_Bicomplex"
ML "blaa"
ML "blaa_square"
ML "blaas"
ML "blaas_square"
ML "blaa_three"
ML "foos"
ML "foos1"
ML "foos2"
ML "foos3"
ML "foos4"
ML "foos5"
ML "foos6"
ML "foos7"
ML "foos_local_bound"
ML "foos_Phi"
ML "goos"
ML "goos1"
ML "goos2"
ML "goos3"
ML "goos4"
ML "goos5"
ML "goos6"
ML "goos7"
ML "goos30"
ML "goos_local_bound"
ML "goos30_eq_0"
ML "goos_Phi"
subsection{*Some lemmas to get code generation in Obua's way*}
text{*In this Section we will pay attention to get
to execute the definitions over which
we have proved the instance before,
for instance, @{term "Φ::'a::lordered_ring matrix => 'a matrix"}.*}
text{*Before executing them, we have to provide the HXL with the lemmas that
link such definitions with the definitions over sparse matrices, such as
@{term α_spmat}.*}
text{*Some preliminar results are also required to get executions in the HCL.*}
lemma neg_int: "neg ((number_of x)::int) = neg x"
using number_of_is_id [of x] by simp
lemma split_apply: "split f (a, b) = f a b"
by simp
definition add_3:: "nat => nat"
where "add_3 x = x + (3::nat)"
lemma funpow_rec: "f^n = (if n = (0::nat) then id else f o (f^(n - 1)))"
by (case_tac n) simp_all
lemma funpow_rec_calc:
"f^(number_of w)
= (if (number_of w = (0::nat)) then id else f o (f^((number_of w) - 1)))"
by (rule funpow_rec)
lemma comp_calc: "(f o g) x = (f (g x))"
by auto
lemma id_calc: "id x = x"
by auto
lemmas compute_iterative =
add_3_def
funpow_rec_calc
comp_calc
id_calc
compute_hol
compute_numeral
NatBin.mod_nat_number_of
NatBin.div_nat_number_of
NatBin.nat_number_of
ML{* val computer =
PCompute.make Compute.BARRAS @{theory}
(ComputeHOL.prep_thms (@{thms "compute_iterative"})) []
fun compute ct = hd (PCompute.rewrite computer [ct])*}
ML{*compute @{cterm "(add_3 (6::nat))"}*}
ML{*compute @{cterm "((add_3^4) (6::nat))"}*}
lemma fin_sum_spmat_rec:
"fin_sum_spmat f A n =
(if n = 0 then A else add_spmat (((f^n) A), fin_sum_spmat f A (n - 1)))"
proof (cases n)
case 0
{
show ?thesis
using 0 by simp
}
next
case Suc
{
obtain m where n_eq: "n = Suc m"
using Suc by simp
show ?thesis
unfolding n_eq
unfolding fin_sum_spmat.simps (2) [of f A m]
by simp
}
qed
lemma fin_sum_spmat_rec_calc:
"fin_sum_spmat f A (number_of n) =
(if (number_of n = (0::nat)) then A
else add_spmat (((f^(number_of n)) A),
fin_sum_spmat f A ((number_of n) - 1)))"
unfolding fin_sum_spmat_rec [of f A "number_of n"] ..
lemmas compute_phi_sparse =
-- "The set of lemmas we use from this theory"
-- "The lemma computing @{term Φ}"
sym [OF phi_execute_sparse]
Φ_spmat_def
-- "The lemmas computing the bound"
sym [OF local_bound_eq_local_bound_spmat]
local_bound_spmat_def
local_bound_gen_spmat_def
For_simp
non_zero_spmat.simps
non_zero_spvec.simps
-- "The lemmas dealing with the termination predicate"
terminates_rec
-- "The lemmas computing the finite sum of sparse matrices"
fin_sum_spmat_rec
fin_sum_spmat_rec_calc
-- "The lemma computing addition of matrices"
add_spmat.simps
-- "The lemmas computing function powers"
funpow_rec_calc comp_calc
id_calc
alpha_nth_power_execute_sparse
-- "The lemmas computing alpha"
alpha_execute_sparse
α_spmat_def
-- "The lemmas computing the differential"
diff_matrix1_execute_sparse
sym [OF sparse_row_matrix_differ_spmat]
sparse_row_matrix_differ_spmat_differ_spmat_sort
differ_spmat_sort.simps
-- "The lemmas computing the homotopy operator"
hom_oper_matrix1_execute_sparse_simp
hom_oper_spmat.simps
-- "The lemmas computing the perturbation operator"
pert_matrix1_execute_sparse_simp
pert_spmat_sort.simps
-- "Lemma for the minus operation over matrices"
minus_spmat.simps
-- "Some aditional library lemmas also required"
sort_spvec.simps
insert_sorted.simps
compute_hol
compute_numeral
NatBin.mod_nat_number_of
NatBin.div_nat_number_of
NatBin.nat_number_of
neg_int
sorted_sp_simps
sparse_row_matrix_arith_simps
map.simps
split_apply
-- "And of course, some matrices:"
example_one_def
example_one'_def
example_zero_def
text{*The BARRAS mode seems to be a more flexible way for code generation,
where, for instance, lambda abstractions are allowed in the definitions.*}
text{*Apparently is also slower.*}
ML{* val computer =
PCompute.make
Compute.BARRAS @{theory}
(ComputeHOL.prep_thms (@{thms "compute_phi_sparse"})) []
fun compute ct = hd (PCompute.rewrite computer [ct])*}
ML{*compute
@{cterm "terminates (λ y. non_zero_spmat y ≠ (0::nat),
α_spmat,
example_one)"}*}
ML{*compute
@{cterm "(α^(6::nat))
(sparse_row_matrix
[(0, [(0, 35::int), (1, 46)]),
(1, [(0, 103), (1, 98)]),
(23, [(7, 14), (8, 16)])])"}*}
ML{*compute
@{cterm "local_bound_spmat α_spmat
[(0, [(0, 1::int), (1, 2)]),
(2, [(0, 3), (2, 4)])]"}*}
ML{*compute @{cterm
"(α^(1::nat))
(sparse_row_matrix
[(0, [(0, 1::int), (1, 2)]),
(2, [(0, 3), (2, 4)])])"}*}
text{*Different ways to compute the local bound:*}
ML{*compute
@{cterm
"diff_matrix1 (sparse_row_matrix
[(2, [(2, 5::int)])])"}*}
ML{*compute
@{cterm
"α (sparse_row_matrix [(1, [(2, 5::int)])])"}*}
ML{*compute
@{cterm
"hom_oper_matrix1 (sparse_row_matrix [(0, [(3, 5::int)])])"}*}
ML{*compute
@{cterm
"(α^(2::nat)) (sparse_row_matrix [(2, [(1, 5::int)])])"}*}
ML{*compute
@{cterm
"local_bound α (sparse_row_matrix example_one)"}*}
ML{*compute
@{cterm
"local_bound α (sparse_row_matrix example_zero)"}*}
ML{*compute
@{cterm
"local_bound α (sparse_row_matrix example_one')"}*}
ML{*compute
@{cterm
"(α^(30::nat)) (sparse_row_matrix example_one)"}*}
ML{*compute
@{cterm
"local_bound_spmat α_spmat example_one"}*}
text{*Different ways to compute the result
of applying @{term "Φ"} to the matrix @{term example_one}.*}
ML{*compute @{cterm "Φ_spmat example_one"}*}
ML{*compute @{cterm "Φ (sparse_row_matrix example_one)"}*}
ML{*compute @{cterm
"Φ (sparse_row_matrix
[(0, [(2, 5), (0, - 9), (6, (8::int))]),
(1, [(1, 4), (2, 0), (8, 8)]),
(2, [(2, 6), (3, 7), (9, 23)]),
(29, [(3, 5), (4, 6), (7, 8)])])"}*}
ML{*compute
@{cterm
"local_bound_spmat α_spmat
[(0, [(0, 1::int), (1, 2)]),
(1, [(0, 3), (1, 4)])]"}*}
ML{*compute
@{cterm
"diff_matrix1 (sparse_row_matrix
[(0, [(0, 35::int), (1, 46)]),
(1, [(0, 103), (1, 98)]),
(23, [(7, 14), (8, 16)])])"}*}
text{*Some other experiments making use of the SML mode of the HCL,
instead of the BARRAS mode.*}
ML{*val computer =
PCompute.make Compute.SML @{theory}
(ComputeHOL.prep_thms (@{thms "compute_phi_sparse"})) []
fun compute ct = hd (PCompute.rewrite computer [ct])*}
ML{*compute @{cterm
"α_spmat (
[(0, [(0, 1::int), (1, 2)]),
(1, [(0, 3), (1, 4)])])"}*}
ML{*compute
@{cterm
"local_bound_spmat α_spmat (
[(0, [(0, 1::int), (1, 2)]),
(1, [(0, 3), (1, 4)])])"}*}
ML{*compute
@{cterm
"α (sparse_row_matrix
[(0, [(0, 1::int), (1, 2)]),
(1, [(0, 3), (1, 4)])])"}*}
ML{*compute
@{cterm
"Φ_spmat ([(0, [(0, 1::int), (1, 2)]),
(1, [(0, 3), (1, 4)])])"}*}
subsection{*Code generation formt the series @{term "Ψ::'a matrix => 'a::lordered_ring matrix"}*}
text{*The following results will permit us to apply
code generation also from the series @{term "Ψ"}.*}
text{*They are similar to the ones already proved for @{term "α"} and @{term "Φ"}.*}
text{*The following definition is the one to be
compared with @{term "β::'a::lordered_ring matrix => 'a matrix"}.*}
definition β_spmat :: "('a::lordered_ring) spmat => 'a spmat"
where "β_spmat A = (minus_spmat (hom_oper_spmat (pert_spmat_sort A)))"
text{*The following definition is the one to be later
compared with the one of @{term "Ψ::'a::lordered_ring matrix => 'a matrix"}.*}
definition Ψ_spmat :: "('a::lordered_ring) spmat => 'a spmat"
where "Ψ_spmat A == fin_sum_spmat β_spmat A (local_bound_spmat β_spmat A)"
lemma beta_equiv: "β = (λA. - (h (δ A)))"
unfolding β_def
unfolding fun_Compl_def
unfolding o_apply ..
lemma sorted_spvec_beta_spmat:
assumes srtd: "sorted_spvec A"
shows "sorted_spvec (β_spmat A)"
unfolding β_spmat_def
using sorted_spvec_minus_spmat
[OF sorted_spvec_hom_oper
[OF sorted_spvec_pert_spmat_sort
[OF srtd]]] .
lemma sorted_spvec_beta_spmat_nth:
assumes srtd: "sorted_spvec A"
shows "sorted_spvec ((β_spmat^n) A)"
proof (induct n)
case 0 show ?case by simp
next
case Suc
fix n
assume hypo: "sorted_spvec ((β_spmat^n) A)"
show "sorted_spvec ((β_spmat^(Suc n)) A)"
using sorted_spvec_beta_spmat [OF hypo]
by simp
qed
lemma sorted_spmat_beta_spmat:
shows "sorted_spmat (β_spmat A)"
unfolding β_spmat_def
using sorted_spmat_minus_spmat
[OF sorted_spmat_hom_oper
[OF sorted_spmat_pert_spmat_sort
[of A]]] .
lemma sorted_spmat_beta_spmat_nth:
assumes srtd_A: "sorted_spmat A"
shows "sorted_spmat ((β_spmat^n) A)"
proof (induct n)
case 0
{
show ?case
using srtd_A
unfolding funpow.simps (1)
unfolding id_apply .
}
next
case Suc
{
fix n :: nat
assume hypo: "sorted_spmat ((β_spmat^n) A)"
show "sorted_spmat ((β_spmat ^ Suc n) A)"
using sorted_spmat_beta_spmat
by simp
}
qed
lemma sorted_sparse_matrix_beta:
assumes ssm: "sorted_sparse_matrix A"
shows "sorted_sparse_matrix (β_spmat A)"
using ssm unfolding sorted_sparse_matrix_def
using sorted_spvec_beta_spmat [of A]
using sorted_spmat_beta_spmat [of A] by simp
lemma sorted_sparse_matrix_beta_nth:
assumes ssm: "sorted_sparse_matrix A"
shows "sorted_sparse_matrix ((β_spmat^n) A)"
using ssm
unfolding sorted_sparse_matrix_def
using sorted_spvec_beta_spmat_nth [of A]
using sorted_spmat_beta_spmat_nth [of A] by auto
lemma beta_execute_sparse:
"β (sparse_row_matrix A) = sparse_row_matrix (β_spmat A)"
unfolding β_spmat_def
unfolding sparse_row_matrix_minus [of "hom_oper_spmat (pert_spmat_sort A)"]
unfolding sparse_row_matrix_hom_oper_spmat
unfolding sym [OF hom_oper_matrix1_execute_sparse [of ]]
unfolding sym [OF sparse_row_matrix_pert_spmat_eq_pert_spmat_sort [of ]]
unfolding sparse_row_matrix_pert_spmat
unfolding sym [OF pert_matrix1_execute_sparse [of ]]
unfolding beta_equiv
unfolding hom_oper_matrix_def
unfolding pert_matrix_def ..
corollary beta_nth_power_execute_sparse:
shows "(β ^ n) (sparse_row_matrix A)
= sparse_row_matrix ((β_spmat^n) A)"
using beta_execute_sparse
using nth_power_execute_sparse [of β β_spmat] by auto
lemma fin_sum_beta_up_to_n_execute_sparse:
shows "fin_sum β n (sparse_row_matrix A)
= sparse_row_matrix (fin_sum_spmat β_spmat A n)"
proof (induct n)
case 0
show ?case by simp
next
case Suc
fix n
assume hyps: "fin_sum β n (sparse_row_matrix A)
= sparse_row_matrix (fin_sum_spmat β_spmat A n)"
show "fin_sum β (Suc n) (sparse_row_matrix A)
= sparse_row_matrix (fin_sum_spmat β_spmat A (Suc n))"
unfolding fin_sum.simps(2) [of β "n"]
unfolding fin_sum_spmat.simps(2)
unfolding sparse_row_add_spmat
unfolding fun_matrix_add
unfolding hyps
unfolding beta_nth_power_execute_sparse [of "Suc n" A] ..
qed
lemma local_bound_spmat_beta:
assumes bounded_β: "local_bounded_func (β::'a::lordered_ring matrix => 'a matrix)"
shows "local_bound β (sparse_row_matrix (A::'a::lordered_ring spmat))
= (LEAST n. sparse_row_matrix ((β_spmat ^ n) A) = 0)"
using local_bounded_func_impl_local_bound_is_Least
[OF bounded_β, of "sparse_row_matrix A"]
unfolding beta_nth_power_execute_sparse [of _ A] .
lemma LEAST_execute_sparse_beta:
assumes ssm: "sorted_sparse_matrix A"
shows "(LEAST n. sparse_row_matrix ((β_spmat ^ n)
(A::'a::lordered_ring spmat))
= (0::'a matrix)) =
(LEAST n. non_zero_spmat ((β_spmat ^ n) A) = (0::nat))"
proof (rule least_eq, rule allI)
fix n
show "(sparse_row_matrix ((β_spmat ^ n) A) = 0)
= (non_zero_spmat ((β_spmat ^ n) A) = 0)"
using sparse_row_matrix_zero_eq_non_zero_spmat_zero
[OF sorted_sparse_matrix_beta_nth [OF ssm, of n]] .
qed
lemma local_bound_beta_spmat:
assumes bounded_β: "local_bounded_func
(β::'a::lordered_ring matrix => 'a matrix)"
and ssm: "sorted_sparse_matrix A"
shows "local_bound β (sparse_row_matrix A)
= (LEAST n. non_zero_spmat ((β_spmat ^ n)
(A::'a::lordered_ring spmat)) = (0::nat))"
unfolding local_bound_spmat_beta [OF bounded_β]
unfolding LEAST_execute_sparse_beta [OF ssm] ..
text{*We make the simplification rule for @{term "local_bound_gen"}: *}
text{*Now, we connect the neccesary termination of For
with our termination condition, @{term local_bounded_func}. *}
text{*Then, under the @{term local_bounded_func} premise
the loop will be terminating.*}
lemma local_bounded_func_beta_impl_terminates_loop:
"local_bounded_func (β::'a matrix => 'a matrix)
= (∀ x. terminates (λ y. y ≠ 0, β, (x::'a::lordered_ring matrix)))"
unfolding local_bounded_func_impl_terminates_loop ..
text{*The following lemma transfers the condition
of termination from matrices to sparse matrices.*}
lemma local_bounded_func_beta_impl_terminates_loop_spmat:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
shows "terminates (λy. y ≠ 0, β, sparse_row_matrix A)
= terminates (λy. non_zero_spmat y ≠ (0::nat), β_spmat, A)"
unfolding terminates.simps
unfolding Orbit_def
unfolding beta_nth_power_execute_sparse
apply simp
using sparse_row_matrix_zero_eq_non_zero_spmat_zero
[OF sorted_sparse_matrix_beta_nth [OF ssm]] by auto
lemma local_bounded_func_impl_terminates_beta_spmat_loop:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
and locbf: "local_bounded_func (β::'a::lordered_ring matrix => 'a matrix)"
shows "terminates (λ y. non_zero_spmat y ≠ (0::nat), β_spmat, A)"
using locbf
unfolding local_bounded_func_beta_impl_terminates_loop
using local_bounded_func_beta_impl_terminates_loop_spmat
[OF ssm] by simp
lemma LEAST_local_bound_beta_non_zero_spmat:
assumes is_zero: "non_zero_spmat A = 0"
shows "(LEAST n::nat. non_zero_spmat ((β_spmat ^ n) A)
= (0::nat)) = 0"
using Least_le
[of "λn. non_zero_spmat ((β_spmat ^n) A) = 0" 0]
using is_zero by simp
lemma local_bound_gen_spmat_beta_correct:
shows "terminates (λ y. non_zero_spmat y ≠ (0::nat), β_spmat, A)
==> local_bound_gen_spmat β_spmat A m
= m + (LEAST n::nat. non_zero_spmat ((β_spmat^n) A) = 0)"
unfolding local_bound_gen_spmat_def
proof (rule For_pinduct [
where i=A
and s=m
and Ac="λ y n. n+1"
and continue="λy. non_zero_spmat y ≠ (0::nat)"
and f="β_spmat"])
show "terminates (λy. non_zero_spmat y ≠ 0, β_spmat, A)
==> terminates (λy. non_zero_spmat y ≠ 0, β_spmat, A)" .
next
fix i s
assume termin_A: "terminates (λy. non_zero_spmat y ≠ 0, β_spmat, A)"
and termin_i: "terminates (λy. non_zero_spmat y ≠ 0, β_spmat, i)"
and hypo: "non_zero_spmat i ≠ 0 ==>
For (λy. non_zero_spmat y ≠ 0)
β_spmat (λy n. n + 1) (β_spmat i) (s + 1) =
s + 1 + (LEAST n. non_zero_spmat ((β_spmat ^ n) (β_spmat i)) = 0)"
show "For (λy. non_zero_spmat y ≠ 0) β_spmat (λy n. n + 1) i s
= s + (LEAST n. non_zero_spmat ((β_spmat ^ n) i) = 0)"
proof (cases "non_zero_spmat i = 0")
case True
{
show ?thesis
unfolding LEAST_local_bound_beta_non_zero_spmat [OF True]
using True
using For_simp [of "(λy. non_zero_spmat y ≠ 0)"
β_spmat "(λy n. n + 1)" i s]
by simp
}
next
case False
{
have For_rew: "For (λy. non_zero_spmat y ≠ 0) β_spmat
(λy n. n + 1) (β_spmat i) (s + 1) =
s + 1 + (LEAST n. non_zero_spmat (
(β_spmat ^ n) (β_spmat i)) = 0)"
using hypo
using False by simp
obtain m where vanish_i: "non_zero_spmat ((β_spmat ^ m) i) = 0"
using terminates_implies [OF termin_i] by auto
have "0 < m" using False vanish_i by (cases "m = 0") auto
from this and vanish_i
have vanish_beta_i: "non_zero_spmat ((β_spmat ^ (m - 1))
(β_spmat i)) = 0"
using funpow_zip [of "β_spmat" "m - 1" i] by auto
show ?thesis
unfolding For_simp [of "(λy. non_zero_spmat y ≠ 0)"
β_spmat "(λy n. n + 1)" i s]
unfolding For_rew
apply (simp add: False)
proof (rule Least_Suc2[symmetric, of _ m _ "m - 1"])
show "non_zero_spmat ((β_spmat ^ m) i) = 0"
using vanish_i by simp
show " non_zero_spmat ((β_spmat ^ (m - 1)) (β_spmat i)) = 0"
using vanish_beta_i by simp
show "non_zero_spmat ((β_spmat ^ 0) i) ≠ 0"
using False by simp
show "∀k. (non_zero_spmat ((β_spmat ^ Suc k) i) = 0)
= (non_zero_spmat ((β_spmat ^ k) (β_spmat i)) = 0)"
using funpow_zip [of β_spmat _ i] by auto
qed
}
qed
qed
text{*The following lemma exactly represents the difference
between our old definitions, with which we proved the BPL, and the new ones,
from which we are trying to generate code;
under the termination premise, both
@{term "(LEAST n::nat. (f^n) (x::'a::ab_group_add) = 0)"},
the old definition of local nilpotency, and
@{term [locale=ab_group_add] "local_bound f x"}, the loop computing the lower bound,
are equivalent*}
text{*Whereas @{term "(LEAST n::nat. (f^n) (x::'a::ab_group_add) = 0)"}
does not have a computable interpretation,
@{term [locale=ab_group_add] "local_bound f x"} does have it,
and code can be generated from it.*}
lemma local_bound_beta_spmat_correct:
"terminates (λ y. non_zero_spmat y ≠ (0::nat), β_spmat, A) ==>
local_bound_spmat β_spmat A
= (LEAST n::nat. non_zero_spmat ((β_spmat^n) A) = 0)"
unfolding local_bound_spmat_def
using local_bound_gen_spmat_beta_correct [of A 0] by simp
lemma nrows_hom_oper_pert_decre:
assumes A_not_null: "(A::'a::lordered_ring matrix) ≠ 0"
shows "nrows ((- (hom_oper_matrix1 o pert_matrix1)) A) < nrows A"
(is "nrows ((- ?f) A) < nrows A")
proof (cases "(- ?f) A = 0")
case True
have fA_0: "nrows ((- ?f) A) = (0::nat)"
unfolding True
using zero_matrix_def_nrows .
with not_zero_impl_nrows_g_0 [OF A_not_null]
show ?thesis by arith
next
case False
show "nrows ((- ?f) A) < nrows A"
proof -
have nrows_A: "nrows A = Suc (Max (fst ` nonzero_positions (Rep_matrix A)))"
using not_zero_impl_nonzero_pos [OF A_not_null]
unfolding nrows_def by simp
have "nrows ((- ?f) A) = Suc (Max (fst ` nonzero_positions (Rep_matrix ((- ?f) A))))"
using not_zero_impl_nonzero_pos [OF False]
unfolding nrows_def by simp
also have "… = Suc (Max (fst ` nonzero_positions (Rep_matrix (?f A))))"
unfolding sym [OF nonzero_positions_minus_f [of ?f A]] ..
also have "… = Suc (Max (fst ` nonzero_positions (((
hom_oper_infmatrix o pert_infmatrix) o Rep_matrix) A)))"
unfolding pert_matrix1_def
unfolding hom_oper_matrix1_def by simp
finally have nrows_fA: "nrows ((- ?f) A) =
Suc (Max (fst ` nonzero_positions (((hom_oper_infmatrix
o pert_infmatrix) o Rep_matrix) A)))"
by simp
have Max_l: "(Max (fst ` nonzero_positions (Rep_matrix (?f A))))
< Max (fst ` nonzero_positions (Rep_matrix A))"
proof (rule Max_A_B)
let ?n = "Max (fst ` nonzero_positions (Rep_matrix (?f A)))"
show "∃m>?n .(m ∈ (fst ` nonzero_positions (Rep_matrix A)))"
proof (rule exI [of _ "Suc ?n"], intro conjI, simp)
have non_empty: "nonzero_positions (((hom_oper_infmatrix
o pert_infmatrix) o Rep_matrix) A) ≠ {}"
using nonzero_positions_minus_f [of ?f A]
using not_zero_impl_nonzero_pos [OF False]
unfolding pert_matrix1_def
unfolding hom_oper_matrix1_def by simp
have Max_in_set:
"?n ∈ (fst ` nonzero_positions (((hom_oper_infmatrix
o pert_infmatrix) o Rep_matrix) A))"
using Max_in [OF finite_imageI
[OF hom_oper_infmatrix_pert_infmatrix_finite, of "fst" A]]
using non_empty
unfolding image_def
unfolding pert_matrix1_def hom_oper_matrix1_def
by auto
from Max_in_set obtain a
where A_a_n_0: "(hom_oper_infmatrix (pert_infmatrix (Rep_matrix A))) ?n a ≠ 0"
unfolding nonzero_positions_def image_def by auto
with hom_oper_pert_nonzero_incr_rows [of ?n a]
have "(Suc ?n, a - 1) ∈ nonzero_positions (Rep_matrix A)"
unfolding nonzero_positions_def image_def by auto
then show "Suc ?n ∈ fst ` nonzero_positions (Rep_matrix A)"
unfolding image_def [of fst] by force
qed
show "finite (fst ` nonzero_positions (Rep_matrix A))"
using finite_imageI [OF finite_nonzero_positions [of A], of fst] .
show "finite (fst ` nonzero_positions (Rep_matrix ((hom_oper_matrix1 o pert_matrix1) A)))"
unfolding o_apply
using finite_imageI by simp
qed
with nrows_A nrows_fA
show ?thesis
unfolding pert_matrix1_def hom_oper_matrix1_def by simp
qed
qed
corollary nrows_beta_decre:
assumes A_not_null: "(A::'a::lordered_ring matrix) ≠ 0"
shows "nrows (β A) < nrows A"
using nrows_hom_oper_pert_decre [OF A_not_null]
unfolding β_def
unfolding fun_Compl_def
unfolding o_apply
unfolding pert_matrix_def
unfolding hom_oper_matrix_def .
lemma local_bounded_func_β_matrix:
shows "local_bounded_func (β::'a::lordered_ring matrix => 'a matrix)"
unfolding local_bounded_func_def
using nrows_strict_decr [OF nrows_beta_decre]
using nrows_zero_impl_zero by auto
lemma local_bounded_func_beta_impl_local_bound_spmat_is_Least:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
shows "local_bound_spmat β_spmat A
= (LEAST n::nat. non_zero_spmat ((β_spmat^n) A) = 0)"
using local_bound_beta_spmat_correct
[OF local_bounded_func_impl_terminates_beta_spmat_loop
[OF ssm local_bounded_func_β_matrix]] .
lemma local_bound_eq_local_bound_spmat_beta:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
shows "local_bound_spmat β_spmat A = local_bound β (sparse_row_matrix A)"
unfolding local_bounded_func_beta_impl_local_bound_spmat_is_Least
[OF ssm]
unfolding sym [OF local_bound_beta_spmat
[OF local_bounded_func_β_matrix ssm]] ..
lemma psi_execute_sparse:
assumes ssm: "sorted_sparse_matrix (A::'a::lordered_ring spmat)"
shows "sparse_row_matrix (Ψ_spmat A)
= (Ψ::'a::lordered_ring matrix => 'a matrix) (sparse_row_matrix A)"
unfolding Ψ_def
unfolding sym
[OF local_bound_eq_local_bound_spmat_beta
[OF ssm]]
unfolding fin_sum_beta_up_to_n_execute_sparse
unfolding Ψ_spmat_def ..
lemmas compute_phi_psi_sparse =
-- "The set of lemmas we use from this theory"
-- "The lemma computing @{term Φ}"
sym [OF phi_execute_sparse]
Φ_spmat_def
-- "The lemma computing @{term Ψ}"
sym [OF psi_execute_sparse]
Ψ_spmat_def
-- "The lemma computing the bound for @{term α}"
sym [OF local_bound_eq_local_bound_spmat]
-- "The lemma computing the bound for @{term β}"
sym [OF local_bound_eq_local_bound_spmat_beta]
-- "The generic lemmas computing the bound"
local_bound_spmat_def
local_bound_gen_spmat_def
For_simp
non_zero_spmat.simps
non_zero_spvec.simps
-- "The lemmas dealing with the termination predicate"
terminates_rec
-- "The lemmas computing the finite sum of sparse matrices"
fin_sum_spmat_rec
fin_sum_spmat_rec_calc
-- "The lemma computing addition of matrices"
add_spmat.simps
-- "The lemmas computing function powers"
funpow_rec_calc
comp_calc
id_calc
alpha_nth_power_execute_sparse
beta_nth_power_execute_sparse
-- "The lemmas computing beta"
alpha_execute_sparse
α_spmat_def
-- "The lemmas computing beta"
beta_execute_sparse
β_spmat_def
-- "The lemmas computing the differential"
diff_matrix1_execute_sparse
sym [OF sparse_row_matrix_differ_spmat]
sparse_row_matrix_differ_spmat_differ_spmat_sort
differ_spmat_sort.simps
-- "The lemmas computing the homotopy operator"
hom_oper_matrix1_execute_sparse_simp
hom_oper_spmat.simps
-- "The lemmas computing the perturbation operator"
pert_matrix1_execute_sparse_simp
pert_spmat_sort.simps
-- "Lemma for the minus operation over matrices"
minus_spmat.simps
-- "Some aditional library lemmas also required"
sort_spvec.simps
insert_sorted.simps
compute_hol
compute_numeral
NatBin.mod_nat_number_of
NatBin.div_nat_number_of
NatBin.nat_number_of
neg_int
sorted_sp_simps
sparse_row_matrix_arith_simps
map.simps
split_apply
-- "And of course, some matrices:"
example_one_def
example_one'_def
example_zero_def
text{*The BARRAS mode seems to be a more flexible way for code generation,
where, for instance, lambda abstractions are allowed in the definitions.*}
text{*Apparently is also slower.*}
ML{* val computer =
PCompute.make
Compute.BARRAS @{theory}
(ComputeHOL.prep_thms (@{thms "compute_phi_psi_sparse"})) []
fun compute ct = hd (PCompute.rewrite computer [ct])*}
ML{*compute
@{cterm "terminates (λ y. non_zero_spmat y ≠ (0::nat),
β_spmat,
example_one)"}*}
ML{*compute
@{cterm "(β^(6::nat))
(sparse_row_matrix
[(0, [(0, 35::int), (1, 46)]),
(1, [(0, 103), (1, 98)]),
(23, [(7, 14), (8, 16)])])"}*}
ML{*compute
@{cterm "local_bound_spmat β_spmat
[(0, [(0, 1::int), (1, 2)]),
(2, [(0, 3), (2, 4)])]"}*}
ML{*compute @{cterm
"(β^(1::nat))
(sparse_row_matrix
[(0, [(0, 1::int), (1, 2)]),
(2, [(0, 3), (2, 4)])])"}*}
text{*Different ways to compute the local bound:*}
ML{*compute
@{cterm
"diff_matrix1 (sparse_row_matrix
[(2, [(2, 5::int)])])"}*}
ML{*compute
@{cterm
"β (sparse_row_matrix [(1, [(2, 5::int)])])"}*}
ML{*compute
@{cterm
"hom_oper_matrix1 (sparse_row_matrix [(0, [(3, 5::int)])])"}*}
ML{*compute
@{cterm
"(β^(2::nat)) (sparse_row_matrix [(2, [(1, 5::int)])])"}*}
ML{*compute
@{cterm
"(α^(2::nat)) (sparse_row_matrix [(2, [(1, 5::int)])])"}*}
ML{*compute
@{cterm
"example_one"}*}
ML{*compute
@{cterm
"local_bound β (sparse_row_matrix example_one)"}*}
ML{*compute
@{cterm
"local_bound α (sparse_row_matrix example_one)"}*}
ML{*compute
@{cterm
"local_bound β (sparse_row_matrix example_zero)"}*}
ML{*compute
@{cterm
"local_bound α (sparse_row_matrix example_one')"}*}
ML{*compute
@{cterm
"(α^(30::nat)) (sparse_row_matrix example_one)"}*}
ML{*compute
@{cterm
"(β^(29::nat)) (sparse_row_matrix example_one)"}*}
ML{*compute
@{cterm
"(β^(30::nat)) (sparse_row_matrix example_one)"}*}
text{*Different ways to compute the result
of applying @{term "Φ"} to the matrix @{term example_one}.*}
ML{*compute @{cterm "Φ (sparse_row_matrix example_one)"}*}
ML{*compute @{cterm "Ψ (sparse_row_matrix example_one)"}*}
ML{*compute @{cterm
"Φ (sparse_row_matrix
[(0, [(2, 5), (0, - 9), (6, (8::int))]),
(1, [(1, 4), (2, 0), (8, 8)]),
(2, [(2, 6), (3, 7), (9, 23)]),
(29, [(3, 5), (4, 6), (7, 8)])])"}*}
lemma funpow_equiv:
shows "(g o f)^(Suc n) = g o ((f o g)^n) o f"
proof (induct n)
case 0 show ?case by simp
next
case Suc
fix n
assume hypo: "(g o f) ^ Suc n = g o (f o g) ^ n o f"
then show "(g o f) ^ Suc (Suc n) = g o (f o g) ^ Suc n o f"
unfolding funpow.simps (2) [of "g o f" "(Suc n)"]
by (simp add: o_assoc)
qed
lemma f_id: "f o id = f"
by simp
lemma fun_Compl_equiv: "- (f o g) = (- f) o g"
unfolding fun_Compl_def
unfolding expand_fun_eq
by simp
lemma funpow_zip_next:
"f^(n + 1) = f^n o f"
using funpow_zip [symmetric, of f n]
unfolding expand_fun_eq by simp
code_datatype sparse_row_vector sparse_row_matrix
declare zero_matrix_def [code func del]
lemmas [code func] = sparse_row_vector_empty [symmetric]
declare plus_matrix_def [code func del]
lemmas [code func] = sparse_row_add_spmat [symmetric]
lemmas [code func] = sparse_row_vector_add [symmetric]
term "0::'a::zero matrix"
export_code
"0::'a::zero matrix"
"op +::('a::{plus,zero} matrix => 'a matrix => 'a matrix)"
in Haskell file -
declare pert_matrix1_def [code func del]
lemmas [code func] =
pert_matrix1_execute_sparse_simp
pert_spmat_sort.simps
declare hom_oper_matrix1_def [code func del]
lemmas [code func] =
hom_oper_matrix1_execute_sparse_simp
hom_oper_spmat.simps
declare fun_Compl_def [code func del]
lemmas [code func] = fun_Compl_def
text{*As far as alpha is defined for multiple types,
we have to somehow restrict its definition to the appropiate one*}
text{*Thus, we first delete its definition:*}
lemma [code func, code func del]: "α = α" ..
text{*Then we provide a new definition for it with the appropriate data type*}
definition alpha_matrix ::
"'a::lordered_ring matrix => 'a matrix"
where [code post, code func del]: "alpha_matrix = α"
text{*Then we add the inline tag that will make our
definition display each time we use alpha*}
lemmas [code inline] = alpha_matrix_def [symmetric]
text{*And finally we make use of the required lemmas for code generation*}
lemmas [code func] = alpha_execute_sparse [folded alpha_matrix_def]
lemmas [code func] = α_spmat_def
declare Φ_def [code func del]
text{*At the following lemma we cannot go further using code generation's tool
by Haftmann, since we have a conditional rule, not an equation.*}
text{*Contrarily, HCL can execute the premises, and succeed with the computation.*}
(*lemmas [code func] = phi_execute_sparse*)
definition "foox = (α :: 'a::lordered_ring matrix => _) o α"
code_thms foox
export_code
"0::'a::zero matrix"
"op +::('a::{plus,zero} matrix => 'a matrix => 'a matrix)"
"pert_matrix1"
"op - ::'a::lordered_ring => 'a => 'a"
"hom_oper_matrix1"
"alpha_matrix::('a::lordered_ring matrix => 'a matrix)"
in Haskell file -
end
lemma
- (- x) = x
lemma
x ≠ (0::'a) ==> - x ≠ (0::'a)
lemma
- x ≠ (0::'a) ==> x ≠ (0::'a)
lemma nonzero_positions_minus_f:
nonzero_positions (Rep_matrix (f A)) = nonzero_positions (Rep_matrix ((- f) A))
lemma diff_infmatrix_finite:
finite (nonzero_positions (diff_infmatrix (Rep_matrix x)))
lemma diff_infmatrix_matrix:
diff_infmatrix (Rep_matrix x) ∈ matrix
lemma diff_infmatrix_closed:
Rep_matrix (Abs_matrix (diff_infmatrix (Rep_matrix x))) =
diff_infmatrix (Rep_matrix x)
lemma diff_infmatrix_is_matrix:
A ∈ matrix ==> diff_infmatrix A ∈ matrix
lemma diff_infmatrix_twice:
diff_infmatrix (diff_infmatrix A) = Rep_matrix 0
lemma combine_infmatrix_matrix:
f (0::'b) (0::'c) = (0::'a)
==> combine_infmatrix f (Rep_matrix A) (Rep_matrix B) ∈ matrix
lemma combine_infmatrix_diff_infmatrix_matrix:
f (0::'b) (0::'c) = (0::'a)
==> combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(diff_infmatrix (Rep_matrix B))
∈ matrix
lemma diff_infmatrix_combine_infmatrix_matrix:
f (0::'b) (0::'c) = (0::'a)
==> diff_infmatrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B)) ∈ matrix
lemma Abs_matrix_inject2:
[| x ∈ matrix; y ∈ matrix; x = y |] ==> Abs_matrix x = Abs_matrix y
lemma diff_matrix1_hom:
diff_matrix1 (A + B) = diff_matrix1 A + diff_matrix1 B
lemma diff_matrix1_twice:
diff_matrix1 (diff_matrix1 A) = 0
lemma pert_infmatrix_finite:
finite (nonzero_positions (pert_infmatrix (Rep_matrix x)))
lemma pert_infmatrix_matrix:
pert_infmatrix (Rep_matrix x) ∈ matrix
lemma pert_infmatrix_closed:
Rep_matrix (Abs_matrix (pert_infmatrix (Rep_matrix x))) =
pert_infmatrix (Rep_matrix x)
lemma pert_infmatrix_is_matrix:
A ∈ matrix ==> pert_infmatrix A ∈ matrix
lemma pert_infmatrix_twice:
pert_infmatrix (pert_infmatrix A) = Rep_matrix 0
lemma combine_infmatrix_pert_infmatrix_matrix:
f (0::'b) (0::'c) = (0::'a)
==> combine_infmatrix f (pert_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix B))
∈ matrix
lemma pert_infmatrix_combine_infmatrix_matrix:
f (0::'b) (0::'c) = (0::'a)
==> pert_infmatrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B)) ∈ matrix
lemma combine_diff_pert_matrix:
f (0::'a) (0::'a) = (0::'a)
==> combine_infmatrix f
(diff_infmatrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B)))
(pert_infmatrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B)))
∈ matrix
lemma combine_diff_pert_matrix_1:
f (0::'b) (0::'b) = (0::'a)
==> combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A))
∈ matrix
lemma combine_diff_pert_matrix_2:
f (0::'a) (0::'a) = (0::'a)
==> combine_infmatrix f
(combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A)))
(combine_infmatrix f (diff_infmatrix (Rep_matrix B))
(pert_infmatrix (Rep_matrix B)))
∈ matrix
lemma combine_diff_pert_matrix_3:
f (0::'b) (0::'b) = (0::'a)
==> diff_infmatrix
(combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A)))
∈ matrix
lemma combine_diff_pert_matrix_4:
f (0::'b) (0::'b) = (0::'a)
==> pert_infmatrix
(combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A)))
∈ matrix
lemma combine_diff_pert_matrix_5:
f (0::'a) (0::'a) = (0::'a)
==> combine_infmatrix f
(diff_infmatrix
(combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A))))
(pert_infmatrix
(combine_infmatrix f (diff_infmatrix (Rep_matrix A))
(pert_infmatrix (Rep_matrix A))))
∈ matrix
lemma pert_matrix1_hom:
pert_matrix1 (A + B) = pert_matrix1 A + pert_matrix1 B
lemma pert_matrix1_twice:
pert_matrix1 (pert_matrix1 A) = 0
lemma diff_matrix1_pert_matrix1_is_zero:
diff_matrix1 (pert_matrix1 A) = 0
lemma pert_matrix1_diff_matrix1_is_zero:
pert_matrix1 (diff_matrix1 A) = 0
lemma hom_oper_infmatrix_finite:
finite (nonzero_positions (hom_oper_infmatrix (Rep_matrix x)))
lemma hom_oper_infmatrix_matrix:
hom_oper_infmatrix (Rep_matrix x) ∈ matrix
lemma hom_oper_infmatrix_closed:
Rep_matrix (Abs_matrix (hom_oper_infmatrix (Rep_matrix x))) =
hom_oper_infmatrix (Rep_matrix x)
lemma hom_oper_infmatrix_is_matrix:
A ∈ matrix ==> hom_oper_infmatrix A ∈ matrix
lemma hom_oper_infmatrix_twice:
hom_oper_infmatrix (hom_oper_infmatrix A) = Rep_matrix 0
lemma combine_infmatrix_hom_oper_infmatrix_matrix:
f (0::'b) (0::'c) = (0::'a)
==> combine_infmatrix f (hom_oper_infmatrix (Rep_matrix A))
(hom_oper_infmatrix (Rep_matrix B))
∈ matrix
lemma hom_oper_infmatrix_combine_infmatrix_matrix:
f (0::'b) (0::'c) = (0::'a)
==> hom_oper_infmatrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))
∈ matrix
lemma hom_oper_matrix1_hom:
hom_oper_matrix1 (A + B) = hom_oper_matrix1 A + hom_oper_matrix1 B
lemma hom_oper_matrix1_twice:
hom_oper_matrix1 (hom_oper_matrix1 A) = 0
lemma hom_oper_closed:
Rep_matrix o Abs_matrix o hom_oper_infmatrix o Rep_matrix =
hom_oper_infmatrix o Rep_matrix
lemma pert_infmatrix_hom_oper_infmatrix_finite:
finite (nonzero_positions (pert_infmatrix (hom_oper_infmatrix (Rep_matrix x))))
lemma pert_infmatrix_hom_oper_infmatrix_matrix:
pert_infmatrix (hom_oper_infmatrix (Rep_matrix x)) ∈ matrix
lemma pert_infmatrix_hom_oper_infmatrix_closed:
Rep_matrix (Abs_matrix (pert_infmatrix (hom_oper_infmatrix (Rep_matrix A)))) =
pert_infmatrix (hom_oper_infmatrix (Rep_matrix A))
lemma hom_oper_infmatrix_pert_infmatrix_finite:
finite (nonzero_positions (hom_oper_infmatrix (pert_infmatrix (Rep_matrix x))))
lemma hom_oper_infmatrix_pert_infmatrix_matrix:
hom_oper_infmatrix (pert_infmatrix (Rep_matrix x)) ∈ matrix
lemma hom_oper_infmatrix_pert_infmatrix_closed:
Rep_matrix (Abs_matrix (hom_oper_infmatrix (pert_infmatrix (Rep_matrix A)))) =
hom_oper_infmatrix (pert_infmatrix (Rep_matrix A))
lemma f_1_n:
f ((f ^ n) a) = (f ^ (n + 1)) a
lemma infinite_descending_chain_false:
(!!n. g (Suc n) < g n) ==> False
lemma P_strict_decr:
[| !!A. A ≠ 0 ==> P (f A) < P A; P 0 = 0 |] ==> ∃n. P ((f ^ n) A) = 0
lemma nrows_strict_decr:
(!!A. A ≠ 0 ==> nrows (f A) < nrows A) ==> ∃n. nrows ((f ^ n) A) = 0
lemma ncols_strict_decr:
(!!A. A ≠ 0 ==> ncols (f A) < ncols A) ==> ∃n. ncols ((f ^ n) A) = 0
lemma nonzero_empty_set:
nonzero_positions (Rep_matrix 0) = {}
lemma Rep_matrix_inject2:
Rep_matrix A = Rep_matrix B ==> A = B
lemma nonzero_imp_zero_matrix:
nonzero_positions (Rep_matrix A) = {} ==> A = 0
lemma nrows_zero_impl_zero:
nrows A = 0 ==> A = 0
lemma ncols_zero_impl_zero:
ncols A = 0 ==> A = 0
lemma not_zero_impl_exist:
A ≠ 0 ==> ∃m n. Rep_matrix A m n ≠ (0::'a)
corollary not_zero_impl_nonzero_pos:
A ≠ 0 ==> nonzero_positions (Rep_matrix A) ≠ {}
corollary not_zero_impl_nrows_g_0:
A ≠ 0 ==> 0 < nrows A
corollary not_zero_impl_ncols_g_0:
A ≠ 0 ==> 0 < ncols A
lemma hom_oper_nonzero_positions:
[| (a, b + 1) ∈ nonzero_positions (Rep_matrix A); 0 < b; (a + b) mod 2 ≠ 0 |]
==> (a, b + 2) ∈ nonzero_positions (hom_oper_infmatrix (Rep_matrix A))
lemma pert_nonzero_positions:
[| (a + 1, b) ∈ nonzero_positions (Rep_matrix A); (a + b) mod 2 = 0 |]
==> (a, b) ∈ nonzero_positions (pert_infmatrix (Rep_matrix A))
lemma pert_nonzero_incr:
(a, b) ∈ nonzero_positions (pert_infmatrix (Rep_matrix A))
==> (a + 1, b) ∈ nonzero_positions (Rep_matrix A)
lemma pert_hom_oper_nonzero_ncols_g_1:
(a, b) ∈ nonzero_positions (pert_infmatrix (hom_oper_infmatrix (Rep_matrix A)))
==> 1 ≤ b
lemma pert_hom_oper_nonzero_incr_rows:
(a, b) ∈ nonzero_positions (pert_infmatrix (hom_oper_infmatrix (Rep_matrix A)))
==> (a + 1, b - 1) ∈ nonzero_positions (Rep_matrix A)
lemma hom_oper_pert_nonzero_incr_rows:
(a, b) ∈ nonzero_positions (hom_oper_infmatrix (pert_infmatrix (Rep_matrix A)))
==> (a + 1, b - 1) ∈ nonzero_positions (Rep_matrix A)
lemma Max_A_B:
[| ∃m>Max B. m ∈ A; finite A; finite B |] ==> Max B < Max A
lemma nrows_pert_decre:
A ≠ 0 ==> nrows ((- pert_matrix1) A) < nrows A
lemma nrows_pert_hom_oper_decre:
A ≠ 0 ==> nrows ((- (pert_matrix1 o hom_oper_matrix1)) A) < nrows A
corollary nrows_alpha_decre:
A ≠ 0 ==> nrows (α A) < nrows A
lemma α_matrix_definition:
α = - (pert_matrix1 o hom_oper_matrix1)
lemma differ_spmat_dist:
differ_spmat ((a, b) # A) =
add_spmat
([(a, map (λ(j, x).
if j = 0 then (j, 0::'a)
else if (a + j) mod 2 = 0 then (j - 1, 0::'a) else (j - 1, x))
b)],
differ_spmat A)
lemma differ_spmat'_dist:
differ_spmat' ((a, b) # A) =
add_spmat
(map (λ(j, x).
if j = 0 then (a, [(j, 0::'a)])
else if (a + j) mod 2 = 0 then (a, [(j - 1, 0::'a)])
else (a, [(j - 1, x)]))
b,
differ_spmat' A)
lemma pert_spmat_dist:
pert_spmat ((a, b) # A) =
add_spmat
([(a - 1,
map (λ(j, x).
if a = 0 then (j, 0::'a)
else if (a + j) mod 2 = 0 then (j, 0::'a) else (j, x))
b)],
pert_spmat A)
lemma pert_spmat'_dist:
pert_spmat' ((a, b) # A) =
add_spmat
(map (λ(j, x).
if a = 0 then (a - 1, [(j, 0::'a)])
else if (a + j) mod 2 = 0 then (a - 1, [(j, 0::'a)])
else (a - 1, [(j, x)]))
b,
pert_spmat' A)
lemma hom_oper_spmat_dist:
hom_oper_spmat ((a, b) # A) =
add_spmat
([(a, map (λ(j, x). if (a + j) mod 2 = 1 then (j + 1, 0::'a) else (j + 1, x))
b)],
hom_oper_spmat A)
lemma hom_oper_spmat'_dist:
hom_oper_spmat' ((a, b) # A) =
add_spmat
(map (λ(j, x).
if (a + j) mod 2 = 1 then (a, [(j + 1, 0::'a)])
else (a, [(j + 1, x)]))
b,
hom_oper_spmat' A)
lemma map_impl_existence:
map f l = a # l' ==> ∃a'. a' mem l ∧ f a' = a
lemma move_matrix_zero:
move_matrix 0 i j = 0
lemma sparse_row_matrix_cons2:
sparse_row_matrix [(i, a # v)] =
singleton_matrix i (fst a) (snd a) + sparse_row_matrix [(i, v)]
lemma sorted_spvec_trans:
[| sorted_spvec (a # b); c mem b |] ==> fst a < fst c
lemma add_spmat_el:
add_spmat (a, []) = a
lemma foldl_absorb0':
foldl (λm x. m + l x) M arr = M + foldl (λm x. m + l x) 0 arr
lemma sparse_row_matrix_hom_oper_spvec:
sparse_row_matrix (hom_oper_spmat [(i, v)]) =
sparse_row_matrix (hom_oper_spmat' [(i, v)])
lemma sparse_row_matrix_hom_oper_spmat:
sparse_row_matrix (hom_oper_spmat A) = sparse_row_matrix (hom_oper_spmat' A)
lemma sorted_spvec_hom_oper:
sorted_spvec A ==> sorted_spvec (hom_oper_spmat A)
lemma sorted_spvec_singleton:
sorted_spvec [(i, v)]
lemma sorted_spvec_hom_oper_vec:
sorted_spvec v
==> sorted_spvec
(map (λ(j, x).
if (i + j) mod 2 = Suc 0 then (j + 1, 0::'a) else (j + 1, x))
v)
lemma sorted_spmat_hom_oper:
sorted_spmat A ==> sorted_spmat (hom_oper_spmat A)
lemma sparse_row_matrix_differ_spvec:
sparse_row_matrix (differ_spmat [(i, v)]) =
sparse_row_matrix (differ_spmat' [(i, v)])
lemma sparse_row_matrix_differ_spmat:
sparse_row_matrix (differ_spmat A) = sparse_row_matrix (differ_spmat' A)
lemma sorted_spvec_differ:
sorted_spvec A ==> sorted_spvec (differ_spmat A)
lemma
sorted_spvec [a]
lemma insert_preserves_sorted:
sorted_spvec v ==> sorted_spvec (insert_sorted a v)
lemma sort_is_sorted:
sorted_spvec (sort_spvec v)
lemma insert_pair_add_pair:
insert_sorted (a, b) v = add_spvec ([(a, b)], v)
lemma differ_spmat_sort_dist:
differ_spmat_sort ((i, v) # vs) =
add_spmat
([(i, sort_spvec
(map (λ(j, x).
if j = 0 then (j, 0::'a)
else if (i + j) mod 2 = 0 then (j - 1, 0::'a) else (j - 1, x))
v))],
differ_spmat_sort vs)
lemma sorted_spvec_differ_spmat_sort:
sorted_spvec A ==> sorted_spvec (differ_spmat_sort A)
lemma sorted_spmat_differ_spmat_sort:
sorted_spmat (differ_spmat_sort A)
lemma sort_spvec_spmat_impl_sorted_spmat:
sorted_spmat (sort_spvec_spmat A)
lemma sparse_row_vector_not_sorted:
sparse_row_vector [a, b] = sparse_row_vector [b, a]
lemma sparse_row_vector_dist:
sparse_row_vector [(i, j + k)] = sparse_row_vector [(i, j), (i, k)]
lemma insert_sorted_preserves_sparse_row_vector:
sparse_row_vector (a # v) = sparse_row_vector (insert_sorted a v)
lemma sort_spvec_eq_sparse_row_vector:
sparse_row_vector v = sparse_row_vector (sort_spvec v)
lemma sort_spvec_eq_sparse_row_matrix:
sparse_row_matrix [(i, v)] = sparse_row_matrix [(i, sort_spvec v)]
lemma sparse_row_matrix_differ_spmat_differ_spmat_sort:
sparse_row_matrix (differ_spmat A) = sparse_row_matrix (differ_spmat_sort A)
lemma sparse_row_matrix_pert_spvec:
sparse_row_matrix (pert_spmat [(i, v)]) =
sparse_row_matrix (pert_spmat' [(i, v)])
lemma sparse_row_matrix_pert_spmat:
sparse_row_matrix (pert_spmat A) = sparse_row_matrix (pert_spmat' A)
lemma pert_spmat_sort_dist:
pert_spmat_sort ((i, v) # vs) =
add_spmat
([(i - 1,
sort_spvec
(map (λ(j, x).
if i = 0 then (j, 0::'a)
else if (i + j) mod 2 = 0 then (j, 0::'a) else (j, x))
v))],
pert_spmat_sort vs)
lemma sorted_spmat_pert_spmat_sort:
sorted_spmat (pert_spmat_sort A)
lemma sparse_row_matrix_pert_spmat_eq_pert_spmat_sort:
sparse_row_matrix (pert_spmat A) = sparse_row_matrix (pert_spmat_sort A)
lemma sorted_spvec_pert_spmat_sort:
sorted_spvec A ==> sorted_spvec (pert_spmat_sort A)
lemma sorted_spvec_pert:
sorted_spvec A ==> sorted_spvec (pert_spmat A)
lemma diff_matrix1_zero_eq_zero:
diff_matrix1 0 = 0
lemma foldl_zero_matrix:
foldl (λm x. m) 0 v = 0
lemma Rep_Abs_zero_func:
Rep_matrix (Abs_matrix (λm n. 0::'a)) p q = (0::'a)
lemma is_matrix_i_j:
Rep_matrix (Abs_matrix (λm n. if i = m ∧ j = n then v else 0::'b)) =
(λm n. if i = m ∧ j = n then v else 0::'b)
lemma diff_matrix1_singleton:
diff_matrix1 (singleton_matrix i j v) =
Abs_matrix
(λk l. if (k + l) mod 2 = 1 then 0::'a
else if i = k ∧ j = l + 1 then v else 0::'a)
lemma comb_matrix:
[| f = g; A = B; x = x'; y = y' |] ==> f A x y = g B x' y'
lemma diff_matrix1_execute_sparse:
diff_matrix1 (sparse_row_matrix A) = sparse_row_matrix (differ_spmat' A)
lemma hom_oper_matrix1_zero_eq_zero:
hom_oper_matrix1 0 = 0
lemma hom_oper_matrix1_singleton:
hom_oper_matrix1 (singleton_matrix k l v) =
Abs_matrix
(λi j. if j = 0 then 0::'b
else if (i + j) mod 2 = 0 then 0::'b
else if k = i ∧ l = j - 1 then v else 0::'b)
lemma hom_oper_matrix1_execute_sparse:
hom_oper_matrix1 (sparse_row_matrix A) = sparse_row_matrix (hom_oper_spmat' A)
lemma hom_oper_matrix1_execute_sparse_simp:
hom_oper_matrix1 (sparse_row_matrix A) = sparse_row_matrix (hom_oper_spmat A)
lemma pert_matrix1_zero_eq_zero:
pert_matrix1 0 = 0
lemma pert_matrix1_singleton:
pert_matrix1 (singleton_matrix k l v) =
Abs_matrix
(λi j. if (i + j) mod 2 = 1 then 0::'b
else if k = i + 1 ∧ l = j then v else 0::'b)
lemma pert_matrix1_execute_sparse:
pert_matrix1 (sparse_row_matrix A) = sparse_row_matrix (pert_spmat' A)
lemma pert_matrix1_execute_sparse_simp:
pert_matrix1 (sparse_row_matrix A) = sparse_row_matrix (pert_spmat_sort A)
lemma non_zero_spvec_ge_0:
0 ≤ non_zero_spvec a
lemma non_zero_spvec_g_0:
non_zero_spvec a ≠ 0 ==> ∃pair. pair ∈ set a ∧ snd pair ≠ (0::'a)
lemma non_zero_spmat_g_0:
non_zero_spmat a ≠ 0 ==> ∃list. list ∈ set a ∧ non_zero_spvec (snd list) ≠ 0
lemma non_zero_spvec_impl_sp_rw_vector:
non_zero_spvec A = 0 ==> sparse_row_vector A = 0
lemma Rep_matrix_inject_exp:
(A = B) = (∀j i. Rep_matrix A j i = Rep_matrix B j i)
lemma move_matrix_zero_le2:
[| 0 ≤ j; 0 ≤ i |] ==> (0 = move_matrix A j i) = (0 = A)
lemma Abs_matrix_inject3:
[| x ∈ matrix; y ∈ matrix; Abs_matrix x = Abs_matrix y |] ==> x = y
lemma Abs_matrix_ne:
[| x ∈ matrix; y ∈ matrix; x ≠ y |] ==> Abs_matrix x ≠ Abs_matrix y
lemma singl_mat_zero:
singleton_matrix i j x = 0 ==> x = (0::'a)
lemma zero_impl_sing_mat_zero:
x = (0::'a) ==> singleton_matrix i j x = 0
lemma singl_mat_not_zero:
singleton_matrix i j x ≠ 0 ==> x ≠ (0::'a)
lemma sparse_row_vector_zero_impl_non_zero_spvec:
[| sparse_row_vector A = 0; sorted_spvec A |] ==> non_zero_spvec A = 0
lemma sorted_sparse_matrix_cons2:
sorted_sparse_matrix (a # b # A) ==> sorted_sparse_matrix (a # A)
lemma disj_matrices_A_minus_A:
A ≠ 0 ==> ¬ disj_matrices A (- A)
lemma sorted_sparse_matrix_cons:
sorted_sparse_matrix (a # A) ==> sorted_sparse_matrix A
lemma sparse_row_matrix_zero_eq_non_zero_spmat_zero:
sorted_sparse_matrix A ==> (sparse_row_matrix A = 0) = (non_zero_spmat A = 0)
lemma alpha_execute_sparse:
α (sparse_row_matrix A) = sparse_row_matrix (α_spmat A)
lemma fun_matrix_add:
(f + g) A = f A + g A
lemma nth_power_execute_sparse:
(!!A. f (sparse_row_matrix A) = sparse_row_matrix (f_spmat A))
==> (f ^ n) (sparse_row_matrix A) = sparse_row_matrix ((f_spmat ^ n) A)
corollary alpha_nth_power_execute_sparse:
(α ^ n) (sparse_row_matrix A) = sparse_row_matrix ((α_spmat ^ n) A)
lemma fin_sum_alpha_up_to_n_execute_sparse:
fin_sum α n (sparse_row_matrix A) =
sparse_row_matrix (fin_sum_spmat α_spmat A n)
lemma fin_sum_up_to_n_execute_sparse':
m = n
==> fin_sum α m (sparse_row_matrix A) =
sparse_row_matrix (fin_sum_spmat α_spmat A n)
lemma sorted_sparse_matrix_add_spmat:
[| sorted_sparse_matrix A; sorted_sparse_matrix B |]
==> sorted_sparse_matrix (add_spmat (A, B))
lemma
sorted_spvec (α_spmat example_one)
lemma sorted_spvec_alpha_spmat:
sorted_spvec A ==> sorted_spvec (α_spmat A)
lemma sorted_spvec_alpha_spmat_nth:
sorted_spvec A ==> sorted_spvec ((α_spmat ^ n) A)
lemma sorted_spmat_alpha_spmat:
sorted_spmat (α_spmat A)
lemma sorted_spmat_alpha_spmat_nth:
sorted_spmat A ==> sorted_spmat ((α_spmat ^ n) A)
lemma sorted_sparse_matrix_alpha:
sorted_sparse_matrix A ==> sorted_sparse_matrix (α_spmat A)
lemma sorted_sparse_matrix_alpha_nth:
sorted_sparse_matrix A ==> sorted_sparse_matrix ((α_spmat ^ n) A)
lemma local_bounded_func_α_matrix:
local_bounded_func α
corollary α_matrix_terminates:
terminates (λy. y ≠ 0, α, sparse_row_matrix A)
lemma local_bound_spmat:
local_bound α (sparse_row_matrix A) =
(LEAST n. sparse_row_matrix ((α_spmat ^ n) A) = 0)
lemma local_bound_spmat_termin:
local_bound α (sparse_row_matrix A) =
(LEAST n. sparse_row_matrix ((α_spmat ^ n) A) = 0)
lemma least_eq:
∀n. f n = g n ==> (LEAST n. f n) = (LEAST n. g n)
lemma LEAST_execute_sparse:
sorted_sparse_matrix A
==> (LEAST n. sparse_row_matrix ((α_spmat ^ n) A) = 0) =
(LEAST n. non_zero_spmat ((α_spmat ^ n) A) = 0)
lemma local_bound_alpha_spmat:
sorted_sparse_matrix A
==> local_bound α (sparse_row_matrix A) =
(LEAST n. non_zero_spmat ((α_spmat ^ n) A) = 0)
lemma local_bound_gen_spmat_simp:
For (λy. non_zero_spmat y ≠ 0) f (λy n. n + 1) x ac =
(if non_zero_spmat x ≠ 0
then For (λy. non_zero_spmat y ≠ 0) f (λy n. n + 1) (f x) (ac + 1) else ac)
lemma local_bounded_func_alpha_impl_terminates_loop:
local_bounded_func α = (∀x. terminates (λy. y ≠ 0, α, x))
lemma local_bounded_func_alpha_impl_terminates_loop_spmat:
sorted_sparse_matrix A
==> terminates (λy. y ≠ 0, α, sparse_row_matrix A) =
terminates (λy. non_zero_spmat y ≠ 0, α_spmat, A)
lemma local_bounded_func_impl_terminates_spmat_loop:
sorted_sparse_matrix A ==> terminates (λy. non_zero_spmat y ≠ 0, α_spmat, A)
lemma LEAST_local_bound_non_zero_spmat:
non_zero_spmat A = 0 ==> (LEAST n. non_zero_spmat ((α_spmat ^ n) A) = 0) = 0
lemma local_bound_gen_spmat_correct:
terminates (λy. non_zero_spmat y ≠ 0, α_spmat, A)
==> local_bound_gen_spmat α_spmat A m =
m + (LEAST n. non_zero_spmat ((α_spmat ^ n) A) = 0)
lemma local_bound_spmat_correct:
terminates (λy. non_zero_spmat y ≠ 0, α_spmat, A)
==> local_bound_spmat α_spmat A =
(LEAST n. non_zero_spmat ((α_spmat ^ n) A) = 0)
lemma local_bounded_func_impl_local_bound_spmat_is_Least:
sorted_sparse_matrix A
==> local_bound_spmat α_spmat A =
(LEAST n. non_zero_spmat ((α_spmat ^ n) A) = 0)
lemma local_bound_eq_local_bound_spmat:
sorted_sparse_matrix A
==> local_bound_spmat α_spmat A = local_bound α (sparse_row_matrix A)
lemma phi_execute_sparse:
sorted_sparse_matrix A
==> sparse_row_matrix (Φ_spmat A) = Φ (sparse_row_matrix A)
lemma neg_int:
neg (number_of x) = neg x
lemma split_apply:
split f (a, b) = f a b
lemma funpow_rec:
f ^ n = (if n = 0 then id else f o f ^ (n - 1))
lemma funpow_rec_calc:
f ^ number_of w = (if number_of w = 0 then id else f o f ^ (number_of w - 1))
lemma comp_calc:
(f o g) x = f (g x)
lemma id_calc:
id x = x
lemma compute_iterative:
add_3 x = x + 3
f ^ number_of w = (if number_of w = 0 then id else f o f ^ (number_of w - 1))
(f o g) x = f (g x)
id x = x
If True = (λx y. x)
If False = (λx y. y)
(¬ True) = False
(¬ False) = True
(P ∧ True) = P
(True ∧ P) = P
(P ∧ False) = False
(False ∧ P) = False
(P ∨ True) = True
(True ∨ P) = True
(P ∨ False) = P
(False ∨ P) = P
(True --> P) = P
(P --> True) = True
(True --> P) = P
(P --> False) = (¬ P)
(False --> P) = True
(False = False) = True
(True = True) = True
(False = True) = False
(True = False) = False
fst (x, y) = x
snd (x, y) = y
((a, b) = (c, d)) = (a = c ∧ b = d)
prod_case f (x, y) = f x y
the (Some x) = x
(None = Some x) = False
(Some x = None) = False
(None = None) = True
(Some x = Some y) = (x = y)
option_case = (λa f opt. option_case_compute opt a f)
option_case_compute None = (λa f. a)
option_case_compute (Some x) = (λa f. f x)
list_case = (λa f l. list_case_compute l a f)
list_case_compute [] = (λa f. a)
list_case_compute (u # v) = (λa f. f u v)
length [] = 0
length (x # xs) = 1 + length xs
(x # xs) ! n = (if n = 0 then x else xs ! (n - 1))
Let s f == f s
If True = (λx y. x)
If False = (λx y. y)
Let s f == f s
fst (x, y) = x
snd (x, y) = y
((a, b) = (c, d)) = (a = c ∧ b = d)
prod_case f (x, y) = f x y
(¬ True) = False
(¬ False) = True
(P ∧ True) = P
(True ∧ P) = P
(P ∧ False) = False
(False ∧ P) = False
(P ∨ True) = True
(True ∨ P) = True
(P ∨ False) = P
(False ∨ P) = P
(True --> P) = P
(P --> True) = True
(True --> P) = P
(P --> False) = (¬ P)
(False --> P) = True
(False = False) = True
(True = True) = True
(False = True) = False
(True = False) = False
Int.Bit0 Int.Pls = Int.Pls
Int.Bit1 Int.Min = Int.Min
iszero Int.Pls = True
iszero Int.Min = False
iszero (Int.Bit0 x) = iszero x
iszero (Int.Bit1 x) = False
neg Int.Pls = False
neg Int.Min = True
neg (Int.Bit0 x) = neg x
neg (Int.Bit1 x) = neg x
lezero Int.Pls = True
lezero Int.Min = True
lezero (Int.Bit0 x) = lezero x
lezero (Int.Bit1 x) = neg x
(Int.Pls = Int.Pls) = True
(Int.Min = Int.Min) = True
(Int.Pls = Int.Min) = False
(Int.Min = Int.Pls) = False
(Int.Bit0 x = Int.Bit0 y) = (x = y)
(Int.Bit1 x = Int.Bit1 y) = (x = y)
(Int.Bit0 x = Int.Bit1 y) = False
(Int.Bit1 x = Int.Bit0 y) = False
(Int.Pls = Int.Bit0 x) = (Int.Pls = x)
(Int.Pls = Int.Bit1 x) = False
(Int.Min = Int.Bit0 x) = False
(Int.Min = Int.Bit1 x) = (Int.Min = x)
(Int.Bit0 x = Int.Pls) = (x = Int.Pls)
(Int.Bit1 x = Int.Pls) = False
(Int.Bit0 x = Int.Min) = False
(Int.Bit1 x = Int.Min) = (x = Int.Min)
(Int.Pls < Int.Min) = False
(Int.Pls < Int.Pls) = False
(Int.Min < Int.Pls) = True
(Int.Min < Int.Min) = False
(Int.Bit0 x < Int.Bit0 y) = (x < y)
(Int.Bit1 x < Int.Bit1 y) = (x < y)
(Int.Bit0 x < Int.Bit1 y) = (x ≤ y)
(Int.Bit1 x < Int.Bit0 y) = (x < y)
(Int.Pls < Int.Bit0 x) = (Int.Pls < x)
(Int.Pls < Int.Bit1 x) = (Int.Pls ≤ x)
(Int.Min < Int.Bit0 x) = (Int.Pls ≤ x)
(Int.Min < Int.Bit1 x) = (Int.Min < x)
(Int.Bit0 x < Int.Pls) = (x < Int.Pls)
(Int.Bit1 x < Int.Pls) = (x < Int.Pls)
(Int.Bit0 x < Int.Min) = (x < Int.Pls)
(Int.Bit1 x < Int.Min) = (x < Int.Min)
(Int.Pls ≤ Int.Min) = False
(Int.Pls ≤ Int.Pls) = True
(Int.Min ≤ Int.Pls) = True
(Int.Min ≤ Int.Min) = True
(Int.Bit0 x ≤ Int.Bit0 y) = (x ≤ y)
(Int.Bit1 x ≤ Int.Bit1 y) = (x ≤ y)
(Int.Bit0 x ≤ Int.Bit1 y) = (x ≤ y)
(Int.Bit1 x ≤ Int.Bit0 y) = (x < y)
(Int.Pls ≤ Int.Bit0 x) = (Int.Pls ≤ x)
(Int.Pls ≤ Int.Bit1 x) = (Int.Pls ≤ x)
(Int.Min ≤ Int.Bit0 x) = (Int.Pls ≤ x)
(Int.Min ≤ Int.Bit1 x) = (Int.Min ≤ x)
(Int.Bit0 x ≤ Int.Pls) = (x ≤ Int.Pls)
(Int.Bit1 x ≤ Int.Pls) = (x < Int.Pls)
(Int.Bit0 x ≤ Int.Min) = (x < Int.Pls)
(Int.Bit1 x ≤ Int.Min) = (x ≤ Int.Min)
Int.succ Int.Pls = Int.Bit1 Int.Pls
Int.succ Int.Min = Int.Pls
Int.succ (Int.Bit0 k) = Int.Bit1 k
Int.succ (Int.Bit1 k) = Int.Bit0 (Int.succ k)
Int.pred Int.Pls = Int.Min
Int.pred Int.Min = Int.Bit0 Int.Min
Int.pred (Int.Bit0 k) = Int.Bit1 (Int.pred k)
Int.pred (Int.Bit1 k) = Int.Bit0 k
- Int.Pls = Int.Pls
- Int.Min = Int.Bit1 Int.Pls
- Int.Bit0 k = Int.Bit0 (- k)
- Int.Bit1 k = Int.Bit1 (Int.pred (- k))
Int.Pls + k = k
Int.Min + k = Int.pred k
k + Int.Pls = k
k + Int.Min = Int.pred k
Int.Bit0 k + Int.Bit0 l = Int.Bit0 (k + l)
Int.Bit0 k + Int.Bit1 l = Int.Bit1 (k + l)
Int.Bit1 k + Int.Bit0 l = Int.Bit1 (k + l)
Int.Bit1 k + Int.Bit1 l = Int.Bit0 (k + Int.succ l)
Int.Pls * w = Int.Pls
Int.Min * k = - k
x * Int.Pls = Int.Pls
x * Int.Min = - x
Int.Bit0 x * y = Int.Bit0 (x * y)
x * Int.Bit0 y = Int.Bit0 (x * y)
Int.Bit1 x * Int.Bit1 y = Int.Bit1 (Int.Bit0 (x * y) + x + y)
0 = Numeral0
1 = Numeral1
nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)
Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))
number_of x + number_of y =
(if neg x then number_of y
else if neg y then number_of x else number_of (x + y))
number_of x - number_of y =
(if neg x then 0
else if neg y then number_of x else nat_norm_number_of (number_of (x + - y)))
number_of x * number_of y =
(if neg x then 0 else if neg y then 0 else number_of (x * y))
(number_of x = number_of y) = (lezero x ∧ lezero y ∨ x = y)
(number_of x < number_of y) = (x < y ∧ ¬ lezero y)
(number_of x ≤ number_of y) = (y < x --> lezero x)
natfac n = (if n = 0 then 1 else n * natfac (n - 1))
- number_of w = number_of (- w)
number_of v + number_of w = number_of (v + w)
number_of x - number_of y = number_of (x + - y)
number_of v * number_of w = number_of (v * w)
(0::'a) = Numeral0
(1::'a) = Numeral1
(number_of x = number_of y) = (x = y)
(number_of x ≤ number_of y) = (x ≤ y)
(number_of x < number_of y) = (x < y)
max a b = (if a ≤ b then b else a)
min a b = (if a ≤ b then a else b)
real (number_of v) = (if neg v then 0 else number_of v)
nat (number_of v) = number_of v
real (number_of v) = number_of v
z ^ number_of (Int.Bit0 w) = (let w = z ^ number_of w in w * w)
z ^ number_of (Int.Bit1 w) =
(if Numeral0 ≤ number_of w then let w = z ^ number_of w in z * w * w
else Numeral1)
z ^ Numeral0 = Numeral1
z ^ -1 = Numeral1
a div b = fst (divAlg (a, b))
a mod b = snd (divAlg (a, b))
divAlg (a, b) =
(if 0 ≤ a
then if 0 ≤ b then posDivAlg a b
else if a = 0 then 0N else negateSnd (negDivAlg (- a) (- b))
else if 0 < b then negDivAlg a b else negateSnd (posDivAlg (- a) (- b)))
adjust b (q, r) = (if 0 ≤ r - b then (2 * q + 1, r - b) else (2 * q, r))
negateSnd (q, r) = (q, - r)
posDivAlg a b =
(if a < b ∨ b ≤ 0 then (0, a) else adjust b (posDivAlg a (2 * b)))
negDivAlg a b =
(if 0 ≤ a + b ∨ b ≤ 0 then (-1, a + b) else adjust b (negDivAlg a (2 * b)))
even Int.Pls = True
even Int.Min = False
even (Int.Bit0 x) = True
even (Int.Bit1 x) = False
even (number_of w) = even w
number_of v mod number_of v' =
(if neg (number_of v) then 0
else if neg (number_of v') then number_of v
else nat (number_of v mod number_of v'))
number_of v div number_of v' =
(if neg (number_of v) then 0 else nat (number_of v div number_of v'))
nat (number_of w) = number_of w
lemma fin_sum_spmat_rec:
fin_sum_spmat f A n =
(if n = 0 then A else add_spmat ((f ^ n) A, fin_sum_spmat f A (n - 1)))
lemma fin_sum_spmat_rec_calc:
fin_sum_spmat f A (number_of n) =
(if number_of n = 0 then A
else add_spmat ((f ^ number_of n) A, fin_sum_spmat f A (number_of n - 1)))
lemma compute_phi_sparse:
sorted_sparse_matrix A1
==> Φ (sparse_row_matrix A1) = sparse_row_matrix (Φ_spmat A1)
Φ_spmat A = fin_sum_spmat α_spmat A (local_bound_spmat α_spmat A)
sorted_sparse_matrix A1
==> local_bound α (sparse_row_matrix A1) = local_bound_spmat α_spmat A1
local_bound_spmat f A == local_bound_gen_spmat f A 0
local_bound_gen_spmat f A n = For (λy. non_zero_spmat y ≠ 0) f (λy n. n + 1) A n
For continue f Ac x ac =
(if continue x then For continue f Ac (f x) (Ac x ac) else ac)
non_zero_spmat [] = 0
non_zero_spmat (a # b) = non_zero_spvec (snd a) + non_zero_spmat b
non_zero_spvec [] = 0
non_zero_spvec (a # b) =
(if snd a ≠ (0::'a) then Suc (non_zero_spvec b) else non_zero_spvec b)
terminates (continue, f, x) =
(if continue x then terminates (continue, f, f x) else True)
fin_sum_spmat f A n =
(if n = 0 then A else add_spmat ((f ^ n) A, fin_sum_spmat f A (n - 1)))
fin_sum_spmat f A (number_of n) =
(if number_of n = 0 then A
else add_spmat ((f ^ number_of n) A, fin_sum_spmat f A (number_of n - 1)))
add_spmat ([], bs) = bs
add_spmat (w # x, []) = w # x
add_spmat (a # as, b # bs) =
(if fst a < fst b then a # add_spmat (as, b # bs)
else if fst b < fst a then b # add_spmat (a # as, bs)
else (fst a, add_spvec (snd a, snd b)) # add_spmat (as, bs))
f ^ number_of w = (if number_of w = 0 then id else f o f ^ (number_of w - 1))
(f o g) x = f (g x)
id x = x
(α ^ n) (sparse_row_matrix A) = sparse_row_matrix ((α_spmat ^ n) A)
α (sparse_row_matrix A) = sparse_row_matrix (α_spmat A)
α_spmat A = minus_spmat (pert_spmat_sort (hom_oper_spmat A))
diff_matrix1 (sparse_row_matrix A) = sparse_row_matrix (differ_spmat' A)
sparse_row_matrix (differ_spmat' A1) = sparse_row_matrix (differ_spmat A1)
sparse_row_matrix (differ_spmat A) = sparse_row_matrix (differ_spmat_sort A)
differ_spmat_sort [] = []
differ_spmat_sort ((i, v) # vs) =
(let m = sort_spvec
(map (λ(j, x).
if j = 0 then (j, 0::'a)
else if (i + j) mod 2 = 0 then (j - 1, 0::'a)
else (j - 1, x))
v);
M = differ_spmat_sort vs
in add_spmat ([(i, m)], M))
hom_oper_matrix1 (sparse_row_matrix A) = sparse_row_matrix (hom_oper_spmat A)
hom_oper_spmat [] = []
hom_oper_spmat ((i, v) # vs) =
(let m = map (λ(j, x). if (i + j) mod 2 = 1 then (j + 1, 0::'a) else (j + 1, x))
v;
M = hom_oper_spmat vs
in add_spmat ([(i, m)], M))
pert_matrix1 (sparse_row_matrix A) = sparse_row_matrix (pert_spmat_sort A)
pert_spmat_sort [] = []
pert_spmat_sort ((i, v) # vs) =
(let m = sort_spvec
(map (λ(j, x).
if i = 0 then (j, 0::'a)
else if (i + j) mod 2 = 0 then (j, 0::'a) else (j, x))
v);
M = pert_spmat_sort vs
in add_spmat ([(i - 1, m)], M))
minus_spmat [] = []
minus_spmat (a # as) = (fst a, minus_spvec (snd a)) # minus_spmat as
sort_spvec [] = []
sort_spvec (a # b) = insert_sorted a (sort_spvec b)
insert_sorted a [] = [a]
insert_sorted a (b # c) =
(if fst a < fst b then a # b # c
else if fst a = fst b then (fst a, snd a + snd b) # c
else b # insert_sorted a c)
If True = (λx y. x)
If False = (λx y. y)
(¬ True) = False
(¬ False) = True
(P ∧ True) = P
(True ∧ P) = P
(P ∧ False) = False
(False ∧ P) = False
(P ∨ True) = True
(True ∨ P) = True
(P ∨ False) = P
(False ∨ P) = P
(True --> P) = P
(P --> True) = True
(True --> P) = P
(P --> False) = (¬ P)
(False --> P) = True
(False = False) = True
(True = True) = True
(False = True) = False
(True = False) = False
fst (x, y) = x
snd (x, y) = y
((a, b) = (c, d)) = (a = c ∧ b = d)
prod_case f (x, y) = f x y
the (Some x) = x
(None = Some x) = False
(Some x = None) = False
(None = None) = True
(Some x = Some y) = (x = y)
option_case = (λa f opt. option_case_compute opt a f)
option_case_compute None = (λa f. a)
option_case_compute (Some x) = (λa f. f x)
list_case = (λa f l. list_case_compute l a f)
list_case_compute [] = (λa f. a)
list_case_compute (u # v) = (λa f. f u v)
length [] = 0
length (x # xs) = 1 + length xs
(x # xs) ! n = (if n = 0 then x else xs ! (n - 1))
Let s f == f s
If True = (λx y. x)
If False = (λx y. y)
Let s f == f s
fst (x, y) = x
snd (x, y) = y
((a, b) = (c, d)) = (a = c ∧ b = d)
prod_case f (x, y) = f x y
(¬ True) = False
(¬ False) = True
(P ∧ True) = P
(True ∧ P) = P
(P ∧ False) = False
(False ∧ P) = False
(P ∨ True) = True
(True ∨ P) = True
(P ∨ False) = P
(False ∨ P) = P
(True --> P) = P
(P --> True) = True
(True --> P) = P
(P --> False) = (¬ P)
(False --> P) = True
(False = False) = True
(True = True) = True
(False = True) = False
(True = False) = False
Int.Bit0 Int.Pls = Int.Pls
Int.Bit1 Int.Min = Int.Min
iszero Int.Pls = True
iszero Int.Min = False
iszero (Int.Bit0 x) = iszero x
iszero (Int.Bit1 x) = False
neg Int.Pls = False
neg Int.Min = True
neg (Int.Bit0 x) = neg x
neg (Int.Bit1 x) = neg x
lezero Int.Pls = True
lezero Int.Min = True
lezero (Int.Bit0 x) = lezero x
lezero (Int.Bit1 x) = neg x
(Int.Pls = Int.Pls) = True
(Int.Min = Int.Min) = True
(Int.Pls = Int.Min) = False
(Int.Min = Int.Pls) = False
(Int.Bit0 x = Int.Bit0 y) = (x = y)
(Int.Bit1 x = Int.Bit1 y) = (x = y)
(Int.Bit0 x = Int.Bit1 y) = False
(Int.Bit1 x = Int.Bit0 y) = False
(Int.Pls = Int.Bit0 x) = (Int.Pls = x)
(Int.Pls = Int.Bit1 x) = False
(Int.Min = Int.Bit0 x) = False
(Int.Min = Int.Bit1 x) = (Int.Min = x)
(Int.Bit0 x = Int.Pls) = (x = Int.Pls)
(Int.Bit1 x = Int.Pls) = False
(Int.Bit0 x = Int.Min) = False
(Int.Bit1 x = Int.Min) = (x = Int.Min)
(Int.Pls < Int.Min) = False
(Int.Pls < Int.Pls) = False
(Int.Min < Int.Pls) = True
(Int.Min < Int.Min) = False
(Int.Bit0 x < Int.Bit0 y) = (x < y)
(Int.Bit1 x < Int.Bit1 y) = (x < y)
(Int.Bit0 x < Int.Bit1 y) = (x ≤ y)
(Int.Bit1 x < Int.Bit0 y) = (x < y)
(Int.Pls < Int.Bit0 x) = (Int.Pls < x)
(Int.Pls < Int.Bit1 x) = (Int.Pls ≤ x)
(Int.Min < Int.Bit0 x) = (Int.Pls ≤ x)
(Int.Min < Int.Bit1 x) = (Int.Min < x)
(Int.Bit0 x < Int.Pls) = (x < Int.Pls)
(Int.Bit1 x < Int.Pls) = (x < Int.Pls)
(Int.Bit0 x < Int.Min) = (x < Int.Pls)
(Int.Bit1 x < Int.Min) = (x < Int.Min)
(Int.Pls ≤ Int.Min) = False
(Int.Pls ≤ Int.Pls) = True
(Int.Min ≤ Int.Pls) = True
(Int.Min ≤ Int.Min) = True
(Int.Bit0 x ≤ Int.Bit0 y) = (x ≤ y)
(Int.Bit1 x ≤ Int.Bit1 y) = (x ≤ y)
(Int.Bit0 x ≤ Int.Bit1 y) = (x ≤ y)
(Int.Bit1 x ≤ Int.Bit0 y) = (x < y)
(Int.Pls ≤ Int.Bit0 x) = (Int.Pls ≤ x)
(Int.Pls ≤ Int.Bit1 x) = (Int.Pls ≤ x)
(Int.Min ≤ Int.Bit0 x) = (Int.Pls ≤ x)
(Int.Min ≤ Int.Bit1 x) = (Int.Min ≤ x)
(Int.Bit0 x ≤ Int.Pls) = (x ≤ Int.Pls)
(Int.Bit1 x ≤ Int.Pls) = (x < Int.Pls)
(Int.Bit0 x ≤ Int.Min) = (x < Int.Pls)
(Int.Bit1 x ≤ Int.Min) = (x ≤ Int.Min)
Int.succ Int.Pls = Int.Bit1 Int.Pls
Int.succ Int.Min = Int.Pls
Int.succ (Int.Bit0 k) = Int.Bit1 k
Int.succ (Int.Bit1 k) = Int.Bit0 (Int.succ k)
Int.pred Int.Pls = Int.Min
Int.pred Int.Min = Int.Bit0 Int.Min
Int.pred (Int.Bit0 k) = Int.Bit1 (Int.pred k)
Int.pred (Int.Bit1 k) = Int.Bit0 k
- Int.Pls = Int.Pls
- Int.Min = Int.Bit1 Int.Pls
- Int.Bit0 k = Int.Bit0 (- k)
- Int.Bit1 k = Int.Bit1 (Int.pred (- k))
Int.Pls + k = k
Int.Min + k = Int.pred k
k + Int.Pls = k
k + Int.Min = Int.pred k
Int.Bit0 k + Int.Bit0 l = Int.Bit0 (k + l)
Int.Bit0 k + Int.Bit1 l = Int.Bit1 (k + l)
Int.Bit1 k + Int.Bit0 l = Int.Bit1 (k + l)
Int.Bit1 k + Int.Bit1 l = Int.Bit0 (k + Int.succ l)
Int.Pls * w = Int.Pls
Int.Min * k = - k
x * Int.Pls = Int.Pls
x * Int.Min = - x
Int.Bit0 x * y = Int.Bit0 (x * y)
x * Int.Bit0 y = Int.Bit0 (x * y)
Int.Bit1 x * Int.Bit1 y = Int.Bit1 (Int.Bit0 (x * y) + x + y)
0 = Numeral0
1 = Numeral1
nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)
Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))
number_of x + number_of y =
(if neg x then number_of y
else if neg y then number_of x else number_of (x + y))
number_of x - number_of y =
(if neg x then 0
else if neg y then number_of x else nat_norm_number_of (number_of (x + - y)))
number_of x * number_of y =
(if neg x then 0 else if neg y then 0 else number_of (x * y))
(number_of x = number_of y) = (lezero x ∧ lezero y ∨ x = y)
(number_of x < number_of y) = (x < y ∧ ¬ lezero y)
(number_of x ≤ number_of y) = (y < x --> lezero x)
natfac n = (if n = 0 then 1 else n * natfac (n - 1))
- number_of w = number_of (- w)
number_of v + number_of w = number_of (v + w)
number_of x - number_of y = number_of (x + - y)
number_of v * number_of w = number_of (v * w)
(0::'a) = Numeral0
(1::'a) = Numeral1
(number_of x = number_of y) = (x = y)
(number_of x ≤ number_of y) = (x ≤ y)
(number_of x < number_of y) = (x < y)
max a b = (if a ≤ b then b else a)
min a b = (if a ≤ b then a else b)
real (number_of v) = (if neg v then 0 else number_of v)
nat (number_of v) = number_of v
real (number_of v) = number_of v
z ^ number_of (Int.Bit0 w) = (let w = z ^ number_of w in w * w)
z ^ number_of (Int.Bit1 w) =
(if Numeral0 ≤ number_of w then let w = z ^ number_of w in z * w * w
else Numeral1)
z ^ Numeral0 = Numeral1
z ^ -1 = Numeral1
a div b = fst (divAlg (a, b))
a mod b = snd (divAlg (a, b))
divAlg (a, b) =
(if 0 ≤ a
then if 0 ≤ b then posDivAlg a b
else if a = 0 then 0N else negateSnd (negDivAlg (- a) (- b))
else if 0 < b then negDivAlg a b else negateSnd (posDivAlg (- a) (- b)))
adjust b (q, r) = (if 0 ≤ r - b then (2 * q + 1, r - b) else (2 * q, r))
negateSnd (q, r) = (q, - r)
posDivAlg a b =
(if a < b ∨ b ≤ 0 then (0, a) else adjust b (posDivAlg a (2 * b)))
negDivAlg a b =
(if 0 ≤ a + b ∨ b ≤ 0 then (-1, a + b) else adjust b (negDivAlg a (2 * b)))
even Int.Pls = True
even Int.Min = False
even (Int.Bit0 x) = True
even (Int.Bit1 x) = False
even (number_of w) = even w
number_of v mod number_of v' =
(if neg (number_of v) then 0
else if neg (number_of v') then number_of v
else nat (number_of v mod number_of v'))
number_of v div number_of v' =
(if neg (number_of v) then 0 else nat (number_of v div number_of v'))
nat (number_of w) = number_of w
neg (number_of x) = neg x
sorted_spvec [] = True
sorted_spvec (a # as) =
(case as of [] => True | b # bs => fst a < fst b ∧ sorted_spvec as)
sorted_spmat [] = True
sorted_spmat (a # as) = (sorted_spvec (snd a) ∧ sorted_spmat as)
sorted_sparse_matrix A == sorted_spvec A ∧ sorted_spmat A
mult_spmat [] A = []
mult_spmat (a # as) A =
(fst a, mult_spvec_spmat ([], snd a, A)) # mult_spmat as A
mult_spvec_spmat (c, [], brr) = c
mult_spvec_spmat (c, y # z, []) = c
mult_spvec_spmat (c, a # arr, b # brr) =
(if fst a < fst b then mult_spvec_spmat (c, arr, b # brr)
else if fst b < fst a then mult_spvec_spmat (c, a # arr, brr)
else mult_spvec_spmat (addmult_spvec (snd a, c, snd b), arr, brr))
addmult_spvec (y, arr, []) = arr
addmult_spvec (y, [], ae # af) = smult_spvec y (ae # af)
addmult_spvec (y, a # arr, b # brr) =
(if fst a < fst b then a # addmult_spvec (y, arr, b # brr)
else if fst b < fst a then (fst b, y * snd b) # addmult_spvec (y, a # arr, brr)
else (fst a, snd a + y * snd b) # addmult_spvec (y, arr, brr))
smult_spvec y [] = []
smult_spvec y (a # arr) = (fst a, y * snd a) # smult_spvec y arr
add_spmat ([], bs) = bs
add_spmat (w # x, []) = w # x
add_spmat (a # as, b # bs) =
(if fst a < fst b then a # add_spmat (as, b # bs)
else if fst b < fst a then b # add_spmat (a # as, bs)
else (fst a, add_spvec (snd a, snd b)) # add_spmat (as, bs))
add_spvec (arr, []) = arr
add_spvec ([], ab # ac) = ab # ac
add_spvec (a # arr, b # brr) =
(if fst a < fst b then a # add_spvec (arr, b # brr)
else if fst b < fst a then b # add_spvec (a # arr, brr)
else (fst a, snd a + snd b) # add_spvec (arr, brr))
minus_spmat [] = []
minus_spmat (a # as) = (fst a, minus_spvec (snd a)) # minus_spmat as
minus_spvec [] = []
minus_spvec (a # as) = (fst a, - snd a) # minus_spvec as
abs_spmat [] = []
abs_spmat (a # as) = (fst a, abs_spvec (snd a)) # abs_spmat as
abs_spvec [] = []
abs_spvec (a # as) = (fst a, ¦snd a¦) # abs_spvec as
diff_spmat A B == add_spmat (A, minus_spmat B)
le_spmat ([], []) = True
le_spmat (a # as, []) = (le_spvec (snd a, []) ∧ le_spmat (as, []))
le_spmat ([], b # bs) = (le_spvec ([], snd b) ∧ le_spmat ([], bs))
le_spmat (a # as, b # bs) =
(if fst a < fst b then le_spvec (snd a, []) ∧ le_spmat (as, b # bs)
else if fst b < fst a then le_spvec ([], snd b) ∧ le_spmat (a # as, bs)
else le_spvec (snd a, snd b) ∧ le_spmat (as, bs))
le_spvec ([], []) = True
le_spvec (a # as, []) = (snd a ≤ (0::'a) ∧ le_spvec (as, []))
le_spvec ([], b # bs) = ((0::'a) ≤ snd b ∧ le_spvec ([], bs))
le_spvec (a # as, b # bs) =
(if fst a < fst b then snd a ≤ (0::'a) ∧ le_spvec (as, b # bs)
else if fst b < fst a then (0::'a) ≤ snd b ∧ le_spvec (a # as, bs)
else snd a ≤ snd b ∧ le_spvec (as, bs))
pprt_spmat [] = []
pprt_spmat (a # as) = (fst a, pprt_spvec (snd a)) # pprt_spmat as
pprt_spvec [] = []
pprt_spvec (a # as) = (fst a, pprt (snd a)) # pprt_spvec as
nprt_spmat [] = []
nprt_spmat (a # as) = (fst a, nprt_spvec (snd a)) # nprt_spmat as
nprt_spvec [] = []
nprt_spvec (a # as) = (fst a, nprt (snd a)) # nprt_spvec as
mult_est_spmat r1.0 r2.0 s1.0 s2.0 ==
add_spmat
(mult_spmat (pprt_spmat s2.0) (pprt_spmat r2.0),
add_spmat
(mult_spmat (pprt_spmat s1.0) (nprt_spmat r2.0),
add_spmat
(mult_spmat (nprt_spmat s2.0) (pprt_spmat r1.0),
mult_spmat (nprt_spmat s1.0) (nprt_spmat r1.0))))
map f [] = []
map f (x # xs) = f x # map f xs
split f (a, b) = f a b
example_one ==
[(0, [(0, 5), (2, - 9), (6, 8)]), (1, [(1, 4), (2, 0), (8, 8)]),
(2, [(2, 6), (3, 7), (9, 23)]), (16, [(13, -8), (19, 12)]),
(29, [(3, 5), (4, 6), (7, 8)])]
example_one' ==
[(0, [(0, 0), (2, 0), (6, 0)]), (1, [(1, 0), (2, 0), (8, 0)]),
(2, [(2, 0), (3, 0), (9, 0)]), (29, [(3, 0), (4, 0), (7, 0)])]
example_zero == [(3, [(3, 5)])]
lemma beta_equiv:
β = (λA. - (h (δ A)))
lemma sorted_spvec_beta_spmat:
sorted_spvec A ==> sorted_spvec (β_spmat A)
lemma sorted_spvec_beta_spmat_nth:
sorted_spvec A ==> sorted_spvec ((β_spmat ^ n) A)
lemma sorted_spmat_beta_spmat:
sorted_spmat (β_spmat A)
lemma sorted_spmat_beta_spmat_nth:
sorted_spmat A ==> sorted_spmat ((β_spmat ^ n) A)
lemma sorted_sparse_matrix_beta:
sorted_sparse_matrix A ==> sorted_sparse_matrix (β_spmat A)
lemma sorted_sparse_matrix_beta_nth:
sorted_sparse_matrix A ==> sorted_sparse_matrix ((β_spmat ^ n) A)
lemma beta_execute_sparse:
β (sparse_row_matrix A) = sparse_row_matrix (β_spmat A)
corollary beta_nth_power_execute_sparse:
(β ^ n) (sparse_row_matrix A) = sparse_row_matrix ((β_spmat ^ n) A)
lemma fin_sum_beta_up_to_n_execute_sparse:
fin_sum β n (sparse_row_matrix A) =
sparse_row_matrix (fin_sum_spmat β_spmat A n)
lemma local_bound_spmat_beta:
local_bounded_func β
==> local_bound β (sparse_row_matrix A) =
(LEAST n. sparse_row_matrix ((β_spmat ^ n) A) = 0)
lemma LEAST_execute_sparse_beta:
sorted_sparse_matrix A
==> (LEAST n. sparse_row_matrix ((β_spmat ^ n) A) = 0) =
(LEAST n. non_zero_spmat ((β_spmat ^ n) A) = 0)
lemma local_bound_beta_spmat:
[| local_bounded_func β; sorted_sparse_matrix A |]
==> local_bound β (sparse_row_matrix A) =
(LEAST n. non_zero_spmat ((β_spmat ^ n) A) = 0)
lemma local_bounded_func_beta_impl_terminates_loop:
local_bounded_func β = (∀x. terminates (λy. y ≠ 0, β, x))
lemma local_bounded_func_beta_impl_terminates_loop_spmat:
sorted_sparse_matrix A
==> terminates (λy. y ≠ 0, β, sparse_row_matrix A) =
terminates (λy. non_zero_spmat y ≠ 0, β_spmat, A)
lemma local_bounded_func_impl_terminates_beta_spmat_loop:
[| sorted_sparse_matrix A; local_bounded_func β |]
==> terminates (λy. non_zero_spmat y ≠ 0, β_spmat, A)
lemma LEAST_local_bound_beta_non_zero_spmat:
non_zero_spmat A = 0 ==> (LEAST n. non_zero_spmat ((β_spmat ^ n) A) = 0) = 0
lemma local_bound_gen_spmat_beta_correct:
terminates (λy. non_zero_spmat y ≠ 0, β_spmat, A)
==> local_bound_gen_spmat β_spmat A m =
m + (LEAST n. non_zero_spmat ((β_spmat ^ n) A) = 0)
lemma local_bound_beta_spmat_correct:
terminates (λy. non_zero_spmat y ≠ 0, β_spmat, A)
==> local_bound_spmat β_spmat A =
(LEAST n. non_zero_spmat ((β_spmat ^ n) A) = 0)
lemma nrows_hom_oper_pert_decre:
A ≠ 0 ==> nrows ((- (hom_oper_matrix1 o pert_matrix1)) A) < nrows A
corollary nrows_beta_decre:
A ≠ 0 ==> nrows (β A) < nrows A
lemma local_bounded_func_β_matrix:
local_bounded_func β
lemma local_bounded_func_beta_impl_local_bound_spmat_is_Least:
sorted_sparse_matrix A
==> local_bound_spmat β_spmat A =
(LEAST n. non_zero_spmat ((β_spmat ^ n) A) = 0)
lemma local_bound_eq_local_bound_spmat_beta:
sorted_sparse_matrix A
==> local_bound_spmat β_spmat A = local_bound β (sparse_row_matrix A)
lemma psi_execute_sparse:
sorted_sparse_matrix A
==> sparse_row_matrix (Ψ_spmat A) = Ψ (sparse_row_matrix A)
lemma compute_phi_psi_sparse:
sorted_sparse_matrix A1
==> Φ (sparse_row_matrix A1) = sparse_row_matrix (Φ_spmat A1)
Φ_spmat A = fin_sum_spmat α_spmat A (local_bound_spmat α_spmat A)
sorted_sparse_matrix A1
==> Ψ (sparse_row_matrix A1) = sparse_row_matrix (Ψ_spmat A1)
Ψ_spmat A == fin_sum_spmat β_spmat A (local_bound_spmat β_spmat A)
sorted_sparse_matrix A1
==> local_bound α (sparse_row_matrix A1) = local_bound_spmat α_spmat A1
sorted_sparse_matrix A1
==> local_bound β (sparse_row_matrix A1) = local_bound_spmat β_spmat A1
local_bound_spmat f A == local_bound_gen_spmat f A 0
local_bound_gen_spmat f A n = For (λy. non_zero_spmat y ≠ 0) f (λy n. n + 1) A n
For continue f Ac x ac =
(if continue x then For continue f Ac (f x) (Ac x ac) else ac)
non_zero_spmat [] = 0
non_zero_spmat (a # b) = non_zero_spvec (snd a) + non_zero_spmat b
non_zero_spvec [] = 0
non_zero_spvec (a # b) =
(if snd a ≠ (0::'a) then Suc (non_zero_spvec b) else non_zero_spvec b)
terminates (continue, f, x) =
(if continue x then terminates (continue, f, f x) else True)
fin_sum_spmat f A n =
(if n = 0 then A else add_spmat ((f ^ n) A, fin_sum_spmat f A (n - 1)))
fin_sum_spmat f A (number_of n) =
(if number_of n = 0 then A
else add_spmat ((f ^ number_of n) A, fin_sum_spmat f A (number_of n - 1)))
add_spmat ([], bs) = bs
add_spmat (w # x, []) = w # x
add_spmat (a # as, b # bs) =
(if fst a < fst b then a # add_spmat (as, b # bs)
else if fst b < fst a then b # add_spmat (a # as, bs)
else (fst a, add_spvec (snd a, snd b)) # add_spmat (as, bs))
f ^ number_of w = (if number_of w = 0 then id else f o f ^ (number_of w - 1))
(f o g) x = f (g x)
id x = x
(α ^ n) (sparse_row_matrix A) = sparse_row_matrix ((α_spmat ^ n) A)
(β ^ n) (sparse_row_matrix A) = sparse_row_matrix ((β_spmat ^ n) A)
α (sparse_row_matrix A) = sparse_row_matrix (α_spmat A)
α_spmat A = minus_spmat (pert_spmat_sort (hom_oper_spmat A))
β (sparse_row_matrix A) = sparse_row_matrix (β_spmat A)
β_spmat A = minus_spmat (hom_oper_spmat (pert_spmat_sort A))
diff_matrix1 (sparse_row_matrix A) = sparse_row_matrix (differ_spmat' A)
sparse_row_matrix (differ_spmat' A1) = sparse_row_matrix (differ_spmat A1)
sparse_row_matrix (differ_spmat A) = sparse_row_matrix (differ_spmat_sort A)
differ_spmat_sort [] = []
differ_spmat_sort ((i, v) # vs) =
(let m = sort_spvec
(map (λ(j, x).
if j = 0 then (j, 0::'a)
else if (i + j) mod 2 = 0 then (j - 1, 0::'a)
else (j - 1, x))
v);
M = differ_spmat_sort vs
in add_spmat ([(i, m)], M))
hom_oper_matrix1 (sparse_row_matrix A) = sparse_row_matrix (hom_oper_spmat A)
hom_oper_spmat [] = []
hom_oper_spmat ((i, v) # vs) =
(let m = map (λ(j, x). if (i + j) mod 2 = 1 then (j + 1, 0::'a) else (j + 1, x))
v;
M = hom_oper_spmat vs
in add_spmat ([(i, m)], M))
pert_matrix1 (sparse_row_matrix A) = sparse_row_matrix (pert_spmat_sort A)
pert_spmat_sort [] = []
pert_spmat_sort ((i, v) # vs) =
(let m = sort_spvec
(map (λ(j, x).
if i = 0 then (j, 0::'a)
else if (i + j) mod 2 = 0 then (j, 0::'a) else (j, x))
v);
M = pert_spmat_sort vs
in add_spmat ([(i - 1, m)], M))
minus_spmat [] = []
minus_spmat (a # as) = (fst a, minus_spvec (snd a)) # minus_spmat as
sort_spvec [] = []
sort_spvec (a # b) = insert_sorted a (sort_spvec b)
insert_sorted a [] = [a]
insert_sorted a (b # c) =
(if fst a < fst b then a # b # c
else if fst a = fst b then (fst a, snd a + snd b) # c
else b # insert_sorted a c)
If True = (λx y. x)
If False = (λx y. y)
(¬ True) = False
(¬ False) = True
(P ∧ True) = P
(True ∧ P) = P
(P ∧ False) = False
(False ∧ P) = False
(P ∨ True) = True
(True ∨ P) = True
(P ∨ False) = P
(False ∨ P) = P
(True --> P) = P
(P --> True) = True
(True --> P) = P
(P --> False) = (¬ P)
(False --> P) = True
(False = False) = True
(True = True) = True
(False = True) = False
(True = False) = False
fst (x, y) = x
snd (x, y) = y
((a, b) = (c, d)) = (a = c ∧ b = d)
prod_case f (x, y) = f x y
the (Some x) = x
(None = Some x) = False
(Some x = None) = False
(None = None) = True
(Some x = Some y) = (x = y)
option_case = (λa f opt. option_case_compute opt a f)
option_case_compute None = (λa f. a)
option_case_compute (Some x) = (λa f. f x)
list_case = (λa f l. list_case_compute l a f)
list_case_compute [] = (λa f. a)
list_case_compute (u # v) = (λa f. f u v)
length [] = 0
length (x # xs) = 1 + length xs
(x # xs) ! n = (if n = 0 then x else xs ! (n - 1))
Let s f == f s
If True = (λx y. x)
If False = (λx y. y)
Let s f == f s
fst (x, y) = x
snd (x, y) = y
((a, b) = (c, d)) = (a = c ∧ b = d)
prod_case f (x, y) = f x y
(¬ True) = False
(¬ False) = True
(P ∧ True) = P
(True ∧ P) = P
(P ∧ False) = False
(False ∧ P) = False
(P ∨ True) = True
(True ∨ P) = True
(P ∨ False) = P
(False ∨ P) = P
(True --> P) = P
(P --> True) = True
(True --> P) = P
(P --> False) = (¬ P)
(False --> P) = True
(False = False) = True
(True = True) = True
(False = True) = False
(True = False) = False
Int.Bit0 Int.Pls = Int.Pls
Int.Bit1 Int.Min = Int.Min
iszero Int.Pls = True
iszero Int.Min = False
iszero (Int.Bit0 x) = iszero x
iszero (Int.Bit1 x) = False
neg Int.Pls = False
neg Int.Min = True
neg (Int.Bit0 x) = neg x
neg (Int.Bit1 x) = neg x
lezero Int.Pls = True
lezero Int.Min = True
lezero (Int.Bit0 x) = lezero x
lezero (Int.Bit1 x) = neg x
(Int.Pls = Int.Pls) = True
(Int.Min = Int.Min) = True
(Int.Pls = Int.Min) = False
(Int.Min = Int.Pls) = False
(Int.Bit0 x = Int.Bit0 y) = (x = y)
(Int.Bit1 x = Int.Bit1 y) = (x = y)
(Int.Bit0 x = Int.Bit1 y) = False
(Int.Bit1 x = Int.Bit0 y) = False
(Int.Pls = Int.Bit0 x) = (Int.Pls = x)
(Int.Pls = Int.Bit1 x) = False
(Int.Min = Int.Bit0 x) = False
(Int.Min = Int.Bit1 x) = (Int.Min = x)
(Int.Bit0 x = Int.Pls) = (x = Int.Pls)
(Int.Bit1 x = Int.Pls) = False
(Int.Bit0 x = Int.Min) = False
(Int.Bit1 x = Int.Min) = (x = Int.Min)
(Int.Pls < Int.Min) = False
(Int.Pls < Int.Pls) = False
(Int.Min < Int.Pls) = True
(Int.Min < Int.Min) = False
(Int.Bit0 x < Int.Bit0 y) = (x < y)
(Int.Bit1 x < Int.Bit1 y) = (x < y)
(Int.Bit0 x < Int.Bit1 y) = (x ≤ y)
(Int.Bit1 x < Int.Bit0 y) = (x < y)
(Int.Pls < Int.Bit0 x) = (Int.Pls < x)
(Int.Pls < Int.Bit1 x) = (Int.Pls ≤ x)
(Int.Min < Int.Bit0 x) = (Int.Pls ≤ x)
(Int.Min < Int.Bit1 x) = (Int.Min < x)
(Int.Bit0 x < Int.Pls) = (x < Int.Pls)
(Int.Bit1 x < Int.Pls) = (x < Int.Pls)
(Int.Bit0 x < Int.Min) = (x < Int.Pls)
(Int.Bit1 x < Int.Min) = (x < Int.Min)
(Int.Pls ≤ Int.Min) = False
(Int.Pls ≤ Int.Pls) = True
(Int.Min ≤ Int.Pls) = True
(Int.Min ≤ Int.Min) = True
(Int.Bit0 x ≤ Int.Bit0 y) = (x ≤ y)
(Int.Bit1 x ≤ Int.Bit1 y) = (x ≤ y)
(Int.Bit0 x ≤ Int.Bit1 y) = (x ≤ y)
(Int.Bit1 x ≤ Int.Bit0 y) = (x < y)
(Int.Pls ≤ Int.Bit0 x) = (Int.Pls ≤ x)
(Int.Pls ≤ Int.Bit1 x) = (Int.Pls ≤ x)
(Int.Min ≤ Int.Bit0 x) = (Int.Pls ≤ x)
(Int.Min ≤ Int.Bit1 x) = (Int.Min ≤ x)
(Int.Bit0 x ≤ Int.Pls) = (x ≤ Int.Pls)
(Int.Bit1 x ≤ Int.Pls) = (x < Int.Pls)
(Int.Bit0 x ≤ Int.Min) = (x < Int.Pls)
(Int.Bit1 x ≤ Int.Min) = (x ≤ Int.Min)
Int.succ Int.Pls = Int.Bit1 Int.Pls
Int.succ Int.Min = Int.Pls
Int.succ (Int.Bit0 k) = Int.Bit1 k
Int.succ (Int.Bit1 k) = Int.Bit0 (Int.succ k)
Int.pred Int.Pls = Int.Min
Int.pred Int.Min = Int.Bit0 Int.Min
Int.pred (Int.Bit0 k) = Int.Bit1 (Int.pred k)
Int.pred (Int.Bit1 k) = Int.Bit0 k
- Int.Pls = Int.Pls
- Int.Min = Int.Bit1 Int.Pls
- Int.Bit0 k = Int.Bit0 (- k)
- Int.Bit1 k = Int.Bit1 (Int.pred (- k))
Int.Pls + k = k
Int.Min + k = Int.pred k
k + Int.Pls = k
k + Int.Min = Int.pred k
Int.Bit0 k + Int.Bit0 l = Int.Bit0 (k + l)
Int.Bit0 k + Int.Bit1 l = Int.Bit1 (k + l)
Int.Bit1 k + Int.Bit0 l = Int.Bit1 (k + l)
Int.Bit1 k + Int.Bit1 l = Int.Bit0 (k + Int.succ l)
Int.Pls * w = Int.Pls
Int.Min * k = - k
x * Int.Pls = Int.Pls
x * Int.Min = - x
Int.Bit0 x * y = Int.Bit0 (x * y)
x * Int.Bit0 y = Int.Bit0 (x * y)
Int.Bit1 x * Int.Bit1 y = Int.Bit1 (Int.Bit0 (x * y) + x + y)
0 = Numeral0
1 = Numeral1
nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)
Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))
number_of x + number_of y =
(if neg x then number_of y
else if neg y then number_of x else number_of (x + y))
number_of x - number_of y =
(if neg x then 0
else if neg y then number_of x else nat_norm_number_of (number_of (x + - y)))
number_of x * number_of y =
(if neg x then 0 else if neg y then 0 else number_of (x * y))
(number_of x = number_of y) = (lezero x ∧ lezero y ∨ x = y)
(number_of x < number_of y) = (x < y ∧ ¬ lezero y)
(number_of x ≤ number_of y) = (y < x --> lezero x)
natfac n = (if n = 0 then 1 else n * natfac (n - 1))
- number_of w = number_of (- w)
number_of v + number_of w = number_of (v + w)
number_of x - number_of y = number_of (x + - y)
number_of v * number_of w = number_of (v * w)
(0::'a) = Numeral0
(1::'a) = Numeral1
(number_of x = number_of y) = (x = y)
(number_of x ≤ number_of y) = (x ≤ y)
(number_of x < number_of y) = (x < y)
max a b = (if a ≤ b then b else a)
min a b = (if a ≤ b then a else b)
real (number_of v) = (if neg v then 0 else number_of v)
nat (number_of v) = number_of v
real (number_of v) = number_of v
z ^ number_of (Int.Bit0 w) = (let w = z ^ number_of w in w * w)
z ^ number_of (Int.Bit1 w) =
(if Numeral0 ≤ number_of w then let w = z ^ number_of w in z * w * w
else Numeral1)
z ^ Numeral0 = Numeral1
z ^ -1 = Numeral1
a div b = fst (divAlg (a, b))
a mod b = snd (divAlg (a, b))
divAlg (a, b) =
(if 0 ≤ a
then if 0 ≤ b then posDivAlg a b
else if a = 0 then 0N else negateSnd (negDivAlg (- a) (- b))
else if 0 < b then negDivAlg a b else negateSnd (posDivAlg (- a) (- b)))
adjust b (q, r) = (if 0 ≤ r - b then (2 * q + 1, r - b) else (2 * q, r))
negateSnd (q, r) = (q, - r)
posDivAlg a b =
(if a < b ∨ b ≤ 0 then (0, a) else adjust b (posDivAlg a (2 * b)))
negDivAlg a b =
(if 0 ≤ a + b ∨ b ≤ 0 then (-1, a + b) else adjust b (negDivAlg a (2 * b)))
even Int.Pls = True
even Int.Min = False
even (Int.Bit0 x) = True
even (Int.Bit1 x) = False
even (number_of w) = even w
number_of v mod number_of v' =
(if neg (number_of v) then 0
else if neg (number_of v') then number_of v
else nat (number_of v mod number_of v'))
number_of v div number_of v' =
(if neg (number_of v) then 0 else nat (number_of v div number_of v'))
nat (number_of w) = number_of w
neg (number_of x) = neg x
sorted_spvec [] = True
sorted_spvec (a # as) =
(case as of [] => True | b # bs => fst a < fst b ∧ sorted_spvec as)
sorted_spmat [] = True
sorted_spmat (a # as) = (sorted_spvec (snd a) ∧ sorted_spmat as)
sorted_sparse_matrix A == sorted_spvec A ∧ sorted_spmat A
mult_spmat [] A = []
mult_spmat (a # as) A =
(fst a, mult_spvec_spmat ([], snd a, A)) # mult_spmat as A
mult_spvec_spmat (c, [], brr) = c
mult_spvec_spmat (c, y # z, []) = c
mult_spvec_spmat (c, a # arr, b # brr) =
(if fst a < fst b then mult_spvec_spmat (c, arr, b # brr)
else if fst b < fst a then mult_spvec_spmat (c, a # arr, brr)
else mult_spvec_spmat (addmult_spvec (snd a, c, snd b), arr, brr))
addmult_spvec (y, arr, []) = arr
addmult_spvec (y, [], ae # af) = smult_spvec y (ae # af)
addmult_spvec (y, a # arr, b # brr) =
(if fst a < fst b then a # addmult_spvec (y, arr, b # brr)
else if fst b < fst a then (fst b, y * snd b) # addmult_spvec (y, a # arr, brr)
else (fst a, snd a + y * snd b) # addmult_spvec (y, arr, brr))
smult_spvec y [] = []
smult_spvec y (a # arr) = (fst a, y * snd a) # smult_spvec y arr
add_spmat ([], bs) = bs
add_spmat (w # x, []) = w # x
add_spmat (a # as, b # bs) =
(if fst a < fst b then a # add_spmat (as, b # bs)
else if fst b < fst a then b # add_spmat (a # as, bs)
else (fst a, add_spvec (snd a, snd b)) # add_spmat (as, bs))
add_spvec (arr, []) = arr
add_spvec ([], ab # ac) = ab # ac
add_spvec (a # arr, b # brr) =
(if fst a < fst b then a # add_spvec (arr, b # brr)
else if fst b < fst a then b # add_spvec (a # arr, brr)
else (fst a, snd a + snd b) # add_spvec (arr, brr))
minus_spmat [] = []
minus_spmat (a # as) = (fst a, minus_spvec (snd a)) # minus_spmat as
minus_spvec [] = []
minus_spvec (a # as) = (fst a, - snd a) # minus_spvec as
abs_spmat [] = []
abs_spmat (a # as) = (fst a, abs_spvec (snd a)) # abs_spmat as
abs_spvec [] = []
abs_spvec (a # as) = (fst a, ¦snd a¦) # abs_spvec as
diff_spmat A B == add_spmat (A, minus_spmat B)
le_spmat ([], []) = True
le_spmat (a # as, []) = (le_spvec (snd a, []) ∧ le_spmat (as, []))
le_spmat ([], b # bs) = (le_spvec ([], snd b) ∧ le_spmat ([], bs))
le_spmat (a # as, b # bs) =
(if fst a < fst b then le_spvec (snd a, []) ∧ le_spmat (as, b # bs)
else if fst b < fst a then le_spvec ([], snd b) ∧ le_spmat (a # as, bs)
else le_spvec (snd a, snd b) ∧ le_spmat (as, bs))
le_spvec ([], []) = True
le_spvec (a # as, []) = (snd a ≤ (0::'a) ∧ le_spvec (as, []))
le_spvec ([], b # bs) = ((0::'a) ≤ snd b ∧ le_spvec ([], bs))
le_spvec (a # as, b # bs) =
(if fst a < fst b then snd a ≤ (0::'a) ∧ le_spvec (as, b # bs)
else if fst b < fst a then (0::'a) ≤ snd b ∧ le_spvec (a # as, bs)
else snd a ≤ snd b ∧ le_spvec (as, bs))
pprt_spmat [] = []
pprt_spmat (a # as) = (fst a, pprt_spvec (snd a)) # pprt_spmat as
pprt_spvec [] = []
pprt_spvec (a # as) = (fst a, pprt (snd a)) # pprt_spvec as
nprt_spmat [] = []
nprt_spmat (a # as) = (fst a, nprt_spvec (snd a)) # nprt_spmat as
nprt_spvec [] = []
nprt_spvec (a # as) = (fst a, nprt (snd a)) # nprt_spvec as
mult_est_spmat r1.0 r2.0 s1.0 s2.0 ==
add_spmat
(mult_spmat (pprt_spmat s2.0) (pprt_spmat r2.0),
add_spmat
(mult_spmat (pprt_spmat s1.0) (nprt_spmat r2.0),
add_spmat
(mult_spmat (nprt_spmat s2.0) (pprt_spmat r1.0),
mult_spmat (nprt_spmat s1.0) (nprt_spmat r1.0))))
map f [] = []
map f (x # xs) = f x # map f xs
split f (a, b) = f a b
example_one ==
[(0, [(0, 5), (2, - 9), (6, 8)]), (1, [(1, 4), (2, 0), (8, 8)]),
(2, [(2, 6), (3, 7), (9, 23)]), (16, [(13, -8), (19, 12)]),
(29, [(3, 5), (4, 6), (7, 8)])]
example_one' ==
[(0, [(0, 0), (2, 0), (6, 0)]), (1, [(1, 0), (2, 0), (8, 0)]),
(2, [(2, 0), (3, 0), (9, 0)]), (29, [(3, 0), (4, 0), (7, 0)])]
example_zero == [(3, [(3, 5)])]
lemma funpow_equiv:
(g o f) ^ Suc n = g o (f o g) ^ n o f
lemma f_id:
f o id = f
lemma fun_Compl_equiv:
- (f o g) = - f o g
lemma funpow_zip_next:
f ^ (n + 1) = f ^ n o f
lemma
0 = sparse_row_vector []
lemma
sparse_row_matrix A + sparse_row_matrix B = sparse_row_matrix (add_spmat (A, B))
lemma
sparse_row_vector a + sparse_row_vector b = sparse_row_vector (add_spvec (a, b))
lemma
pert_matrix1 (sparse_row_matrix A) = sparse_row_matrix (pert_spmat_sort A)
pert_spmat_sort [] = []
pert_spmat_sort ((i, v) # vs) =
(let m = sort_spvec
(map (λ(j, x).
if i = 0 then (j, 0::'a)
else if (i + j) mod 2 = 0 then (j, 0::'a) else (j, x))
v);
M = pert_spmat_sort vs
in add_spmat ([(i - 1, m)], M))
lemma
hom_oper_matrix1 (sparse_row_matrix A) = sparse_row_matrix (hom_oper_spmat A)
hom_oper_spmat [] = []
hom_oper_spmat ((i, v) # vs) =
(let m = map (λ(j, x). if (i + j) mod 2 = 1 then (j + 1, 0::'a) else (j + 1, x))
v;
M = hom_oper_spmat vs
in add_spmat ([(i, m)], M))
lemma
- A = (λx. - A x)
lemma
α = α
lemma
α = alpha_matrix
lemma
alpha_matrix (sparse_row_matrix A) = sparse_row_matrix (α_spmat A)
lemma
α_spmat A = minus_spmat (pert_spmat_sort (hom_oper_spmat A))