Theory Matrix_Comparison
section ‹Comparison of Matrices›
text ‹We use matrices over ordered semirings to again define ordered semirings.
There are two instances, one for ordinary semirings (where addition is monotone w.r.t. the
strict ordering in a single argument);
and one for semirings like the arctic one, where addition is interpreted
as maximum, and therefore monotonicity of the strict ordering in a single argument is no
longer provided.
Both ordered semirings are used for checking termination proofs, where at the moment only
the ordinary semirings is supported for checking complexity proofs.›
theory Matrix_Comparison
imports
Matrix
Matrix.Ordered_Semiring
begin
context ord
begin
definition mat_ge :: "'a mat ⇒ 'a mat ⇒ bool" (infix "≥⇩m" 50) where
"A ≥⇩m B = (∀ i < dim_row A. ∀ j < dim_col A. A $$ (i,j) ≥ B $$ (i,j))"
lemma mat_geI[intro]: assumes "A ∈ carrier_mat nr nc"
"⋀ i j. i < nr ⟹ j < nc ⟹ A $$ (i,j) ≥ B $$ (i,j)"
shows "A ≥⇩m B"
using assms unfolding mat_ge_def by auto
lemma mat_geD[dest]: assumes "A ≥⇩m B" and "i < dim_row A" "j < dim_col A"
shows "A $$ (i,j) ≥ B $$ (i,j)"
using assms unfolding mat_ge_def by auto
definition mat_gt :: "('a ⇒ 'a ⇒ bool) ⇒ nat ⇒ 'a mat ⇒ 'a mat ⇒ bool" where
"mat_gt gt sd A B = (A ≥⇩m B ∧ (∃ i < sd. ∃ j < sd. gt (A $$ (i,j)) (B $$ (i,j))))"
lemma mat_gtI[intro]: assumes "A ≥⇩m B"
and "i < sd" "j < sd" "gt (A $$ (i,j)) (B $$ (i,j))"
shows "mat_gt gt sd A B"
using assms unfolding mat_gt_def by auto
lemma mat_gtD[dest]: assumes "mat_gt gt sd A B"
shows "A ≥⇩m B" "∃ i < sd. ∃ j < sd. gt (A $$ (i,j)) (B $$ (i,j))"
using assms unfolding mat_gt_def by auto
definition mat_max :: "'a mat ⇒ 'a mat ⇒ 'a mat" ("max⇩m") where
"max⇩m A B = mat (dim_row A) (dim_col A) (λ ij. max (A $$ ij) (B $$ ij))"
lemma mat_max_carrier[simp]:
"max⇩m A B ∈ carrier_mat (dim_row A) (dim_col A)"
unfolding mat_max_def by auto
lemma mat_max_closed[intro]:
"A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ max⇩m A B ∈ carrier_mat nr nc"
unfolding mat_max_def by auto
lemma mat_max_index:
assumes "i < dim_row A" "j < dim_col A"
shows "(mat_max A B) $$ (i,j) = max (A $$ (i,j)) (B $$ (i,j))"
unfolding mat_max_def using index_mat assms by auto
definition (in zero) mat_default :: "'a ⇒ nat ⇒ 'a mat" ("default⇩m") where
"default⇩m d n = mat n n (λ (i,j). if i = j then d else 0)"
lemma mat_default_carrier[simp]: "default⇩m d n ∈ carrier_mat n n"
unfolding mat_default_def by auto
end
definition mat_mono :: "('a ⇒ bool) ⇒ nat ⇒ 'a mat ⇒ bool"
where "mat_mono P sd A = (∀ j < sd. ∃ i < sd. P (A $$ (i,j)))"
context non_strict_order
begin
lemma mat_ge_trans: assumes "A ≥⇩m B" "B ≥⇩m C"
and "A ∈ carrier_mat nr nc" "B ∈ carrier_mat nr nc"
shows "A ≥⇩m C"
using assms ge_trans[of "B $$ (i,j)" "A $$ (i,j)" for i j]
unfolding mat_ge_def carrier_mat_def by auto
lemma mat_ge_refl: "A ≥⇩m A"
unfolding mat_ge_def by (auto simp: ge_refl)
lemma mat_max_comm: "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ max⇩m A B = max⇩m B A"
unfolding mat_max_def by (intro eq_matI, auto simp: max_comm)
lemma mat_max_ge: "max⇩m A B ≥⇩m A"
unfolding mat_max_def by (intro mat_geI[of _ "dim_row A" "dim_col A"], auto)
lemma mat_max_ge_0: "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ A ≥⇩m B ⟹ max⇩m A B = A"
unfolding mat_max_def by (intro eq_matI, auto simp: max_id)
lemma mat_max_mono: "A ≥⇩m B ⟹
A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ C ∈ carrier_mat nr nc ⟹
max⇩m C A ≥⇩m max⇩m C B"
by (intro mat_geI[of _ nr nc], auto simp: max_mono mat_max_def)
end
lemma mat_plus_left_mono: "A ≥⇩m (B :: 'a :: ordered_ab_semigroup mat)
⟹ A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ C ∈ carrier_mat nr nc
⟹ A + C ≥⇩m B + C"
by (intro mat_geI[of _ nr nc], auto simp: plus_left_mono)
lemma mat_plus_right_mono: "B ≥⇩m (C :: 'a :: ordered_ab_semigroup mat)
⟹ A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ C ∈ carrier_mat nr nc
⟹ A + B ≥⇩m A + C"
by (intro mat_geI[of _ nr nc], auto simp: plus_right_mono)
lemma plus_mono: "x⇩1 ≥ (x⇩2 :: 'a :: ordered_ab_semigroup) ⟹
y⇩1 ≥ y⇩2 ⟹ x⇩1 + y⇩1 ≥ x⇩2 + y⇩2"
using ge_trans[OF plus_left_mono[of x⇩2 x⇩1] plus_right_mono[of y⇩2 y⇩1]] .
text ‹Since one cannot use @{thm sum_mono} (it requires other
class constraints like @{class order}), we make our own copy of this
fact.›
lemma sum_mono_ge:
assumes ge: "⋀i. i∈K ⟹ f (i::'a) ≥ ((g i)::('b::ordered_semiring_0))"
shows "(∑i∈K. f i) ≥ (∑i∈K. g i)"
proof (cases "finite K")
case True
thus ?thesis using ge
proof induct
case empty
show ?case by (simp add: ge_refl)
next
case insert
thus ?case using plus_mono by fastforce
qed
next
case False then show ?thesis by (simp add: ge_refl)
qed
lemma (in one_mono_ordered_semiring_1) sum_mono_gt:
assumes le: "⋀i. i∈K ⟹ f (i::'b) ≥ ((g i)::'a)"
and i: "i ∈ K"
and gt: "f i ≻ g i"
and K: "finite K"
shows "(∑i∈K. f i) ≻ (∑i∈K. g i)"
proof -
have id: "⋀ f. (∑i∈K. f i) = f i + (∑i∈ K - {i}. f i)"
by (rule sum.remove[OF K i])
have ge: "(∑i∈ K - {i}. f i) ≥ (∑i∈ K - {i}. g i)"
by (rule sum_mono_ge[OF le], auto)
show ?thesis unfolding id using compat[OF plus_right_mono[OF ge] plus_gt_left_mono[OF gt]] .
qed
lemma scalar_left_mono: assumes
"u ∈ carrier_vec n" "v ∈ carrier_vec n" "w ∈ carrier_vec n"
and "⋀ i. i < n ⟹ u $ i ≥ v $ i"
and "⋀ i. i < n ⟹ w $ i ≥ (0 :: 'a :: ordered_semiring_0)"
shows "u ∙ w ≥ v ∙ w" unfolding scalar_prod_def
by (intro sum_mono_ge times_left_mono, insert assms, auto)
lemma scalar_right_mono: assumes
"u ∈ carrier_vec n" "v ∈ carrier_vec n" "w ∈ carrier_vec n"
and "⋀ i. i < n ⟹ v $ i ≥ w $ i"
and "⋀ i. i < n ⟹ u $ i ≥ (0 :: 'a :: ordered_semiring_0)"
shows "u ∙ v ≥ u ∙ w"
proof -
have dim: "dim_vec v = dim_vec w" using assms by auto
show ?thesis unfolding scalar_prod_def dim
by (intro sum_mono_ge times_right_mono, insert assms, auto)
qed
lemma mat_mult_left_mono: assumes C0: "C ≥⇩m 0⇩m n n"
and AB: "A ≥⇩m (B :: 'a :: ordered_semiring_0 mat)"
and carr: "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "C ∈ carrier_mat n n"
shows "A * C ≥⇩m B * C"
proof -
{
fix i j
assume i: "i < n" "j < n"
have "row A i ∙ col C j ≥ row B i ∙ col C j"
by (rule scalar_left_mono[of _ n], insert C0 AB carr i, auto)
}
thus ?thesis
by (intro mat_geI[of _ n n], insert carr, auto)
qed
lemma mat_mult_right_mono: assumes A0: "A ≥⇩m 0⇩m n n"
and BC: "B ≥⇩m (C :: 'a :: ordered_semiring_0 mat)"
and carr: "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "C ∈ carrier_mat n n"
shows "A * B ≥⇩m A * C"
proof -
{
fix i j
assume i: "i < n" "j < n"
have "row A i ∙ col B j ≥ row A i ∙ col C j"
by (rule scalar_right_mono[of _ n], insert A0 BC carr i, auto)
}
thus ?thesis
by (intro mat_geI[of _ n n], insert carr, auto)
qed
lemma one_mat_ge_zero: "(1⇩m n :: 'a :: ordered_semiring_1 mat) ≥⇩m 0⇩m n n"
by (intro mat_geI[of _ n n], auto simp: one_ge_zero ge_refl)
context order_pair
begin
lemma mat_ge_gt_trans: assumes sd: "sd ≤ n" and AB: "A ≥⇩m B" and BC: "mat_gt gt sd B C"
and A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n"
shows "mat_gt gt sd A C"
proof -
from mat_gtD[OF BC] obtain i j where ij: "i < sd" "j < sd" and gt: "B $$ (i, j) ≻ C $$ (i, j)"
and BC: "B ≥⇩m C" by auto
from mat_ge_trans[OF AB BC A B] have AC: "A ≥⇩m C" .
from mat_geD[OF AB, of i j] A sd ij have ge: "A $$ (i,j) ≥ B $$ (i,j)" by auto
from compat[OF ge gt] have gt: "A $$ (i, j) ≻ C $$ (i, j)" .
with ij AC show ?thesis by auto
qed
lemma mat_gt_ge_trans: assumes sd: "sd ≤ n" and AB: "mat_gt gt sd A B" and BC: "B ≥⇩m C"
and A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n"
shows "mat_gt gt sd A C"
proof -
from mat_gtD[OF AB] obtain i j where ij: "i < sd" "j < sd" and gt: "A $$ (i, j) ≻ B $$ (i, j)"
and AB: "A ≥⇩m B" by auto
from mat_ge_trans[OF AB BC A B] have AC: "A ≥⇩m C" .
from mat_geD[OF BC, of i j] B sd ij have ge: "B $$ (i,j) ≥ C $$ (i,j)" by auto
from compat2[OF gt ge] have gt: "A $$ (i, j) ≻ C $$ (i, j)" .
with ij AC show ?thesis by auto
qed
lemma mat_gt_imp_mat_ge: "mat_gt gt sd A B ⟹ A ≥⇩m B"
by (rule mat_gtD)
lemma mat_gt_trans: assumes sd: "sd ≤ n" and AB: "mat_gt gt sd A B" and BC: "mat_gt gt sd B C"
and A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n"
shows "mat_gt gt sd A C"
using mat_ge_gt_trans[OF sd mat_gt_imp_mat_ge[OF AB] BC A B] .
lemma mat_default_ge_0: "default⇩m default n ≥⇩m 0⇩m n n"
by (intro mat_geI[of _ n n], auto simp: mat_default_def default_ge_zero ge_refl)
end
definition mat_ordered_semiring :: "nat ⇒ nat ⇒ ('a :: ordered_semiring_1 ⇒ 'a ⇒ bool) ⇒ 'b ⇒ ('a mat,'b) ordered_semiring_scheme" where
"mat_ordered_semiring n sd gt b ≡ ring_mat TYPE('a) n ⦇
ordered_semiring.geq = (≥⇩m),
gt = mat_gt gt sd,
max = max⇩m,
… = b⦈"
lemma (in one_mono_ordered_semiring_1) mat_ordered_semiring: assumes sd_n: "sd ≤ n"
shows "ordered_semiring
(mat_ordered_semiring n sd (≻) b :: ('a mat,'b) ordered_semiring_scheme)"
(is "ordered_semiring ?R")
proof -
interpret semiring ?R unfolding mat_ordered_semiring_def by (rule semiring_mat)
show ?thesis
by (unfold_locales, unfold ring_mat_def mat_ordered_semiring_def ordered_semiring_record_simps,
auto intro: mat_ge_trans mat_ge_refl mat_ge_gt_trans[OF sd_n] mat_gt_ge_trans[OF sd_n] mat_max_comm
mat_max_ge mat_max_ge_0 mat_max_mono one_mat_ge_zero mat_gt_trans[OF sd_n] mat_gt_imp_mat_ge
mat_plus_left_mono mat_mult_left_mono mat_mult_right_mono)
qed
context weak_SN_strict_mono_ordered_semiring_1
begin
lemma weak_mat_gt_mono: assumes sd_n: "sd ≤ n" and
orient: "⋀ A B. A ∈ carrier_mat n n ⟹ B ∈ carrier_mat n n ⟹ (A,B) ∈ set ABs ⟹ mat_gt weak_gt sd A B"
shows "∃ gt. SN_strict_mono_ordered_semiring_1 default gt mono ∧
(∀ A B. A ∈ carrier_mat n n ⟶ B ∈ carrier_mat n n ⟶ (A, B) ∈ set ABs ⟶ mat_gt gt sd A B)"
proof -
let ?n = "[0 ..< n]"
let ?m1x = "[ A $$ (i,j) . A <- map fst ABs, i <- ?n, j <- ?n]"
let ?m2y = "[ B $$ (i,j) . B <- map snd ABs, i <- ?n, j <- ?n]"
let ?pairs = "concat (map (λ x. map (λ y. (x,y)) ?m2y) ?m1x)"
let ?strict = "filter (λ (x,y). weak_gt x y) ?pairs"
have "∀ x y. (x,y) ∈ set ?strict ⟶ weak_gt x y" by auto
from weak_gt_mono[OF this] obtain gt where order: "SN_strict_mono_ordered_semiring_1 default gt mono"
and orient2: "⋀ x y. (x, y) ∈ set ?strict ⟹ gt x y" by auto
show ?thesis
proof (intro exI allI conjI impI, rule order)
fix A B
assume A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n"
and AB: "(A, B) ∈ set ABs"
from orient[OF this] have "mat_gt weak_gt sd A B" by auto
from mat_gtD[OF this] obtain i j where
ge: "A ≥⇩m B" and ij: "i < sd" "j < sd" and wgt: "weak_gt (A $$ (i,j)) (B $$ (i,j))"
by auto
from ij ‹sd ≤ n› have ij': "i < n" "j < n" by auto
have gt: "gt (A $$ (i,j)) (B $$ (i,j))"
by (rule orient2, insert ij' AB wgt, force)
show "mat_gt gt sd A B" using ij gt ge by auto
qed
qed
end
lemma sum_mat_mono:
assumes A: "A ∈ carrier_mat nr nc" and B: "B ∈ carrier_mat nr nc"
and AB: "A ≥⇩m (B :: 'a :: ordered_semiring_0 mat)"
shows "sum_mat A ≥ sum_mat B"
proof -
from A B have id: "dim_row B = dim_row A" "dim_col B = dim_col A" by auto
show ?thesis unfolding sum_mat_def id
by (rule sum_mono_ge, insert mat_geD[OF AB] id, auto)
qed
context one_mono_ordered_semiring_1
begin
lemma sum_mat_mono_gt:
assumes "sd ≤ n"
and A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n"
and AB: "mat_gt (≻) sd A (B :: 'a mat)"
shows "sum_mat A ≻ sum_mat B"
proof -
from A B have id: "dim_row B = dim_row A" "dim_col B = dim_col A" by auto
from mat_gtD[OF AB] obtain i j where AB: "A ≥⇩m B" and
ij: "i < sd" "j < sd" and gt: "A $$ (i,j) ≻ B $$ (i,j)" by auto
show ?thesis unfolding sum_mat_def id
by (rule sum_mono_gt[of _ _ _ "(i,j)"], insert ij gt mat_geD[OF AB] A B ‹sd ≤ n›, auto)
qed
lemma mat_plus_gt_left_mono: assumes sd_n: "sd ≤ n" and gt: "mat_gt (≻) sd A B"
and A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" and C: "C ∈ carrier_mat n n"
shows "mat_gt (≻) sd (A + C) (B + C)"
proof -
note wf = A B C
from mat_gtD[OF gt] obtain i j
where AB: "A ≥⇩m B" and ij: "i < sd" "j < sd" and gt: "A $$ (i,j) ≻ B $$ (i,j)" by auto
from plus_gt_left_mono[OF gt, of "C $$ (i,j)"]
show ?thesis
by (intro mat_gtI[OF mat_geI[of _ n n] ij], insert mat_geD[OF AB] wf ij sd_n, auto intro: plus_left_mono)
qed
lemma mat_gt_ge_mono: "sd ≤ n ⟹ mat_gt gt sd A B ⟹
mat_gt gt sd C D ⟹
A ∈ carrier_mat n n ⟹
B ∈ carrier_mat n n ⟹
C ∈ carrier_mat n n ⟹
D ∈ carrier_mat n n ⟹
mat_gt gt sd (A + C) (B + D)"
by (rule mat_gt_ge_trans[OF _ mat_plus_gt_left_mono mat_plus_right_mono[OF mat_gt_imp_mat_ge]],
auto)
lemma mat_default_gt_mat0: assumes sd_pos: "sd > 0" and sd_n: "sd ≤ n"
shows "mat_gt (≻) sd (default⇩m default n) (0⇩m n n)"
proof -
from assms have n: "n > 0" by auto
show ?thesis
by (intro mat_gtI[OF mat_default_ge_0 sd_pos sd_pos], insert sd_pos sd_n, auto simp: mat_default_def default_gt_zero)
qed
end
context SN_one_mono_ordered_semiring_1
begin
abbreviation mat_s :: "'a mat ⇒ nat ⇒ nat ⇒ 'a mat ⇒ bool" ("(_ ≻⇩m _ _ _)" [51,51,51,51] 50)
where "A ≻⇩m n sd B ≡ (A ∈ carrier_mat n n ∧ B ∈ carrier_mat n n ∧ B ≥⇩m 0⇩m n n ∧ mat_gt (≻) sd A B)"
lemma mat_gt_SN: assumes sd_n: "sd ≤ n" shows "SN {(m1,m2) . m1 ≻⇩m n sd m2}"
proof
fix A
assume "∀ i. (A i, A (Suc i)) ∈ {(m1,m2). m1 ≻⇩m n sd m2}"
hence "⋀ i. (A i, A (Suc i)) ∈ {(m1,m2). m1 ≻⇩m n sd m2}" by blast
hence A: "⋀ i. A i ∈ carrier_mat n n"
and ge: "⋀ i. A (Suc i) ≥⇩m 0⇩m n n"
and gt: "⋀ i. mat_gt (≻) sd (A i) (A (Suc i))" by auto
define s where "s = (λ i. sum_mat (A i))"
{
fix i
from sum_mat_mono_gt[OF sd_n A A gt[of i]]
have gt: "s i ≻ s (Suc i)" unfolding s_def .
from sum_mat_mono[OF A _ ge[of i]]
have ge: "s (Suc i) ≥ 0" unfolding s_def by auto
note ge gt
}
with SN show False by auto
qed
end
context SN_strict_mono_ordered_semiring_1
begin
lemma mat_mono: assumes sd_n: "sd ≤ n" and A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" and C: "C ∈ carrier_mat n n"
and gt: "mat_gt (≻) sd B C" and gez: "A ≥⇩m 0⇩m n n" and mmono: "mat_mono mono sd A"
shows "mat_gt (≻) sd (A * B) (A * C)" (is "mat_gt _ _ ?AB ?AC")
proof -
from mat_gtD[OF gt] obtain i j where
i: "i < sd" and j: "j < sd" and gt: "B $$ (i,j) ≻ C $$ (i,j)" and BC: "B ≥⇩m C" by auto
from mat_mult_right_mono[OF gez BC A B C] have ge: "?AB ≥⇩m ?AC" .
from mmono[unfolded mat_mono_def] i obtain k where k: "k < sd" and mon: "mono (A $$ (k,i))" by auto
from mat_geD[OF gez] k i sd_n A have "A $$ (k, i) ≥ 0" by auto
note mono = mono[OF mon gt this]
have id: "dim_vec (col B j) = n" "dim_vec (col C j) = n" using j sd_n B C by auto
{
fix i
assume "i < n"
hence "row A k $ i * col B j $ i ≥ row A k $ i * col C j $ i"
by (intro times_right_mono, insert j k sd_n A B C mat_geD[OF gez] mat_geD[OF BC], auto)
} note sge = this
have gt: "row A k ∙ col B j ≻ row A k ∙ col C j" unfolding scalar_prod_def id
by (rule sum_mono_gt[of _ _ _ i, OF sge], insert mono k i j A B C sd_n, auto)
show ?thesis
by (rule mat_gtI[OF ge k j], insert k j sd_n A B C gt, auto)
qed
end
definition mat_comp_all :: "('a ⇒ 'a ⇒ bool) ⇒ 'a mat ⇒ 'a mat ⇒ bool"
where "mat_comp_all r A B =
(∀ i < dim_row A. ∀ j < dim_col A. r (A $$ (i,j)) (B $$ (i,j)))"
lemma mat_comp_allI:
assumes "A ∈ carrier_mat nr nc" "B ∈ carrier_mat nr nc"
and "⋀ i j. i < nr ⟹ j < nc ⟹ r (A $$(i,j)) (B $$ (i,j))"
shows "mat_comp_all r A B"
unfolding mat_comp_all_def using assms by simp
lemma mat_comp_allE:
assumes "mat_comp_all r A B"
and "A ∈ carrier_mat nr nc" "B ∈ carrier_mat nr nc"
shows "⋀ i j. i < nr ⟹ j < nc ⟹ r (A $$ (i,j)) (B $$(i,j))"
using assms unfolding mat_comp_all_def by auto
context weak_SN_both_mono_ordered_semiring_1
begin
abbreviation weak_mat_gt_arc :: "'a mat ⇒ 'a mat ⇒ bool"
where "weak_mat_gt_arc ≡ mat_comp_all weak_gt"
lemma weak_mat_gt_both_mono:
assumes ABs: "set ABs ⊆ carrier_mat n n × carrier_mat n n"
and orient: "∀(A,B) ∈ set ABs. weak_mat_gt_arc A B"
shows "∃ gt. SN_both_mono_ordered_semiring_1 default gt arc_pos ∧
(∀(A,B) ∈ set ABs. mat_comp_all gt A B)"
proof -
let ?pairs = "[ (fst AB $$ (i,j), snd AB $$ (i,j)) . AB <- ABs, i <- [0 ..< n], j <- [0 ..< n]]"
let ?strict = "filter (λ (x,y). weak_gt x y) ?pairs"
have "∀ x y. (x,y) ∈ set ?strict ⟶ weak_gt x y" by auto
from weak_gt_both_mono[OF this]
obtain gt
where order: "SN_both_mono_ordered_semiring_1 default gt arc_pos"
and orient2: "⋀ x y. (x, y) ∈ set ?strict ⟹ gt x y"
by auto
{
fix A B assume AB: "(A,B) ∈ set ABs"
hence A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n"
using AB ABs by auto
have "mat_comp_all gt A B"
proof (rule mat_comp_allI[OF A B])
fix i j
assume i: "i < n" and j: "j < n"
from mat_comp_allE[OF _ A B this] orient AB
have weak_gt: "weak_gt (A $$(i,j)) (B $$ (i,j))" (is "weak_gt ?x ?y") by auto
have "(?x,?y) ∈ set ?pairs" using A AB i j by force
with weak_gt
have gt: "(?x,?y) ∈ set ?strict" by simp
show "gt ?x ?y" by (rule orient2[OF gt])
qed
}
hence "∀(A, B)∈set ABs. mat_comp_all gt A B" by auto
thus ?thesis using order by auto
qed
end
definition mat_both_ordered_semiring :: "nat ⇒ ('a :: ordered_semiring_1 ⇒ 'a ⇒ bool) ⇒ 'b ⇒ ('a mat,'b) ordered_semiring_scheme" where
"mat_both_ordered_semiring n gt b ≡ ring_mat TYPE('a) n ⦇
ordered_semiring.geq = mat_ge,
gt = mat_comp_all gt,
max = mat_max,
… = b⦈"
definition mat_arc_posI :: "('a ⇒ bool) ⇒ 'a mat ⇒ bool"
where "mat_arc_posI ap A ≡ ap (A $$ (0,0))"
context both_mono_ordered_semiring_1
begin
abbreviation mat_gt_arc :: "'a mat ⇒ 'a mat ⇒ bool"
where "mat_gt_arc ≡ mat_comp_all gt"
abbreviation mat_arc_pos :: "'a mat ⇒ bool"
where "mat_arc_pos ≡ mat_arc_posI arc_pos"
lemma mat_max_id: fixes A :: "'a mat"
assumes ge: "mat_ge A B"
and A: "A ∈ carrier_mat nr nc"
and B: "B ∈ carrier_mat nr nc"
shows "mat_max A B = A"
using mat_max_ge_0[OF A B ge] .
lemma mat_gt_arc_trans:
assumes A_B: "mat_gt_arc A B"
and B_C: "mat_gt_arc B C"
and A: "A ∈ carrier_mat nr nc"
and B: "B ∈ carrier_mat nr nc"
and C: "C ∈ carrier_mat nr nc"
shows "mat_gt_arc A C"
proof (rule mat_comp_allI[OF A C])
fix i j
assume i: "i < nr" and j: "j < nc"
from mat_comp_allE[OF A_B A B i j] mat_comp_allE[OF B_C B C i j]
show "A $$ (i,j) ≻ C $$ (i,j)" by (rule gt_trans)
qed
lemma mat_gt_arc_compat:
assumes ge: "mat_ge A B"
and gt: "mat_gt_arc B C"
and A: "A ∈ carrier_mat nr nc"
and B: "B ∈ carrier_mat nr nc"
and C: "C ∈ carrier_mat nr nc"
shows "mat_gt_arc A C"
proof (rule mat_comp_allI[OF A C])
fix i j assume i: "i < nr" and j: "j < nc"
have "A $$ (i,j) ≥ B $$ (i,j)" using ge A i j by auto
also have "B $$ (i,j) ≻ C $$ (i,j)"
using mat_comp_allE[OF gt B C i j] by auto
finally show "A $$ (i,j) ≻ C $$ (i,j)" by auto
qed
lemma mat_gt_arc_compat2:
assumes gt: "mat_gt_arc A B"
and ge: "mat_ge B C"
and A: "A ∈ carrier_mat nr nc"
and B: "B ∈ carrier_mat nr nc"
and C: "C ∈ carrier_mat nr nc"
shows "mat_gt_arc A C"
proof (rule mat_comp_allI[OF A C])
fix i j assume i: "i < nr" and j: "j < nc"
have "A $$ (i,j) ≻ B $$ (i,j)"
using mat_comp_allE[OF gt] A B i j by auto
also have "B $$ (i,j) ≥ C $$ (i,j)"
using ge B i j by auto
finally show "A $$ (i,j) ≻ C $$ (i,j)" by auto
qed
lemma mat_gt_arc_imp_mat_ge:
assumes gt: "mat_gt_arc A B"
and A: "A ∈ carrier_mat nr nc"
and B: "B ∈ carrier_mat nr nc"
shows "mat_ge A B"
using subst mat_geI[OF A]
using mat_comp_allE[OF gt A B] gt_imp_ge by auto
lemma (in both_mono_ordered_semiring_1) mat_both_ordered_semiring: assumes n: "n > 0"
shows "ordered_semiring
(mat_both_ordered_semiring n (≻) b :: ('a mat,'b) ordered_semiring_scheme)"
(is "ordered_semiring ?R")
proof -
interpret semiring ?R unfolding mat_both_ordered_semiring_def by (rule semiring_mat)
show ?thesis
apply (unfold_locales)
unfolding ring_mat_def mat_both_ordered_semiring_def ordered_semiring_record_simps
apply(
auto intro: mat_max_comm mat_ge_trans
mat_plus_left_mono mat_mult_left_mono mat_mult_right_mono mat_ge_refl
one_mat_ge_zero mat_max_mono mat_max_ge mat_max_id
mat_gt_arc_trans mat_gt_arc_imp_mat_ge
mat_gt_arc_compat mat_gt_arc_compat2)
done
qed
lemma mat0_leastI:
assumes A: "A ∈ carrier_mat nr nc"
shows "mat_gt_arc A (0⇩m nr nc)"
proof (rule mat_comp_allI[OF A])
fix i j
assume i: "i < nr" and j: "j < nc"
thus "A $$ (i,j) ≻ 0⇩m nr nc $$ (i,j)" by (auto simp: zero_leastI)
qed auto
lemma mat0_leastII:
assumes gt: "mat_gt_arc (0⇩m nr nc) A"
and A: "A ∈ carrier_mat nr nc"
shows "A = 0⇩m nr nc"
apply (rule eq_matI)
unfolding index_zero_mat
using A
proof -
fix i j
assume i: "i < nr" and j: "j < nc"
show "A $$ (i,j) = 0"
using zero_leastII mat_comp_allE[OF gt _ A] i j by auto
qed auto
lemma mat0_leastIII:
assumes A: "A ∈ carrier_mat nr nc"
shows "mat_ge A ((0⇩m nr nc) :: 'a mat)"
proof (rule mat_geI[OF A]; unfold index_zero_mat)
fix i j
assume i: "i < nr" and j: "j < nc"
show "A $$ (i,j) ≥ 0" using zero_leastIII by simp
qed
lemma mat_max_0_id: fixes A :: "'a mat"
assumes A: "A ∈ carrier_mat nr nc"
shows "mat_max (0⇩m nr nc) A = A"
unfolding mat_max_comm[OF zero_carrier_mat A]
by (rule mat_max_id[OF mat0_leastIII[OF A] A], simp)
lemma mat_arc_pos_one:
assumes n0: "n > 0"
shows "mat_arc_posI arc_pos (1⇩m n)"
unfolding mat_arc_posI_def
unfolding arc_pos_one index_one_mat(1)[OF n0 n0]
using arc_pos_one by simp
lemma mat_arc_pos_zero:
assumes n0: "n > 0"
shows "¬ mat_arc_posI arc_pos (0⇩m n n)"
unfolding mat_arc_posI_def
unfolding index_zero_mat(1)[OF n0 n0] using arc_pos_zero by simp
lemma mat_gt_arc_plus_mono:
assumes gt1: "mat_gt_arc A B"
and gt2: "mat_gt_arc C D"
and A: "(A::'a mat) ∈ carrier_mat nr nc"
and B: "(B::'a mat) ∈ carrier_mat nr nc"
and C: "(C::'a mat) ∈ carrier_mat nr nc"
and D: "(D::'a mat) ∈ carrier_mat nr nc"
shows "mat_gt_arc (A + C) (B + D)" (is "mat_gt_arc ?AC ?BD")
proof -
show ?thesis
proof (rule mat_comp_allI)
fix i j
assume i: "i < nr" and j: "j < nc"
hence ijC: "i < dim_row C" "j < dim_col C"
and ijD: "i < dim_row D" "j < dim_col D"
using C D by auto
show "?AC $$ (i,j) ≻ ?BD $$ (i,j)"
unfolding index_add_mat(1)[OF ijC]
unfolding index_add_mat(1)[OF ijD]
using plus_gt_both_mono
using mat_comp_allE[OF gt1 A B] mat_comp_allE[OF gt2 C D] i j by auto
qed (insert A B C D, auto)
qed
definition vec_comp_all :: "('a ⇒ 'a ⇒ bool) ⇒ 'a vec ⇒ 'a vec ⇒ bool"
where "vec_comp_all r v w ≡ ∀i < dim_vec v. r (v $ i) (w $ i)"
lemma vec_comp_allI:
assumes "⋀i. i < dim_vec v ⟹ r (v $ i) (w $ i)"
shows "vec_comp_all r v w"
unfolding vec_comp_all_def using assms by auto
lemma vec_comp_allE:
"vec_comp_all r v w ⟹ i < dim_vec v ⟹ r (v $ i) (w $ i)"
unfolding vec_comp_all_def by auto
lemma scalar_prod_left_mono:
assumes u: "u ∈ carrier_vec n"
and v: "v ∈ carrier_vec n"
and w: "w ∈ carrier_vec n"
and uv: "vec_comp_all gt u v"
shows "scalar_prod u w ≻ scalar_prod v w"
proof -
{ fix m assume "m ≤ n"
hence "(∑i<m. (u $ i) * (w $ i)) ≻ (∑i<m. (v $ i) * (w $ i))"
proof (induct m)
case 0 show ?case using zero_leastI by simp next
case (Suc m)
hence uv: "u $ m ≻ v $ m"
using vec_comp_allE[OF uv] u by auto
show ?case
unfolding sum.lessThan_Suc
apply (subst plus_gt_both_mono)
using times_gt_left_mono Suc times_gt_left_mono[OF uv] by auto
qed
}
from this[OF order.refl]
show ?thesis
unfolding scalar_prod_def atLeast0LessThan
using w by auto
qed
lemma scalar_prod_right_mono:
assumes u: "u ∈ carrier_vec n"
and v: "v ∈ carrier_vec n"
and w: "w ∈ carrier_vec n"
and vw: "vec_comp_all gt v w"
shows "scalar_prod u v ≻ scalar_prod u w"
proof -
{ fix m assume "m ≤ n"
hence "(∑i<m. (u $ i) * (v $ i)) ≻ (∑i<m. (u $ i) * (w $ i))"
proof (induct m)
case 0 show ?case using zero_leastI by simp next
case (Suc m)
hence vw: "v $ m ≻ w $ m"
using vec_comp_allE[OF vw] v by auto
show ?case
unfolding sum.lessThan_Suc
apply (subst plus_gt_both_mono)
using times_gt_left_mono Suc times_gt_right_mono[OF vw] by auto
qed
}
from this[OF order.refl]
show ?thesis
unfolding scalar_prod_def atLeast0LessThan
using v w by auto
qed
lemma mat_gt_arc_mult_left_mono:
assumes gt1: "mat_gt_arc A B"
and A: "(A::'a mat) ∈ carrier_mat nr n"
and B: "(B::'a mat) ∈ carrier_mat nr n"
and C: "(C::'a mat) ∈ carrier_mat n nc"
shows "mat_gt_arc (A * C) (B * C)" (is "mat_gt_arc ?AC ?BC")
proof (rule mat_comp_allI)
fix i j assume i: "i < nr" and j: "j < nc"
hence iA: "i < dim_row A"
and iB: "i < dim_row B"
and jC: "j < dim_col C"
using A B C by auto
show "?AC $$ (i,j) ≻ ?BC $$ (i,j)"
unfolding index_mult_mat(1)[OF iA jC]
unfolding index_mult_mat(1)[OF iB jC]
proof(rule scalar_prod_left_mono)
show "row A i ∈ carrier_vec n" using A by auto
show "row B i ∈ carrier_vec n" using B by auto
show "col C j ∈ carrier_vec n" using C by auto
show rowAB: "vec_comp_all (≻) (row A i) (row B i)"
proof (intro vec_comp_allI)
fix j assume j: "j < dim_vec (row A i)"
have "A $$ (i,j) ≻ B $$ (i,j)"
using mat_comp_allE[OF gt1 A B i] j A by simp
thus "row A i $ j ≻ row B i $ j"
using A B C i j by simp
qed
qed
qed (insert A B C, auto)
lemma mat_gt_arc_mult_right_mono:
assumes gt1: "mat_gt_arc B C"
and A: "(A::'a mat) ∈ carrier_mat nr n"
and B: "(B::'a mat) ∈ carrier_mat n nc"
and C: "(C::'a mat) ∈ carrier_mat n nc"
shows "mat_gt_arc (A * B) (A * C)" (is "mat_gt_arc ?AB ?AC")
proof (rule mat_comp_allI)
fix i j assume i: "i < nr" and j: "j < nc"
hence iA: "i < dim_row A"
and jB: "j < dim_col B"
and jC: "j < dim_col C"
using A B C by auto
show "?AB $$ (i,j) ≻ ?AC $$ (i,j)"
unfolding index_mult_mat(1)[OF iA jB]
unfolding index_mult_mat(1)[OF iA jC]
proof(rule scalar_prod_right_mono)
show "row A i ∈ carrier_vec n" using A by auto
show "col B j ∈ carrier_vec n" using B by auto
show "col C j ∈ carrier_vec n" using C by auto
show rowAB: "vec_comp_all (≻) (col B j) (col C j)"
proof (intro vec_comp_allI)
fix i assume i: "i < dim_vec (col B j)"
have "B $$ (i,j) ≻ C $$ (i,j)"
using mat_comp_allE[OF gt1 B C] i j B by simp
thus "col B j $ i ≻ col C j $ i"
using A B C i j by simp
qed
qed
qed (insert A B C, auto)
lemma mat_arc_pos_plus:
assumes n0: "n > 0"
and A: "A ∈ carrier_mat n n"
and B: "B ∈ carrier_mat n n"
and arc_pos: "mat_arc_pos A"
shows "mat_arc_pos (A + B)"
unfolding mat_arc_posI_def
apply (subst index_add_mat(1))
using arc_pos_plus[OF arc_pos[unfolded mat_arc_posI_def]]
assms by auto
lemma scalar_prod_split_head: assumes
"A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "n > 0"
shows "row A 0 ∙ col B 0 = A $$ (0,0) * B $$ (0,0) + (∑i = 1..<n. A $$ (0, i) * B $$ (i, 0))"
unfolding scalar_prod_def
using assms sum.atLeast_Suc_lessThan by auto
lemma mat_arc_pos_mult:
assumes n0: "n > 0"
and A: "A ∈ carrier_mat n n"
and B: "B ∈ carrier_mat n n"
and apA: "mat_arc_pos A"
and apB: "mat_arc_pos B"
shows "mat_arc_pos (A * B)"
unfolding mat_arc_posI_def
apply(subst index_mult_mat(1))
proof -
let ?prod = "row A 0 ∙ col B 0"
let ?head = "A $$ (0,0) * B $$ (0,0)"
let ?rest = "∑i = 1..<n. A $$ (0, i) * B $$ (i, 0)"
have ap: "arc_pos ?head"
using apA apB
unfolding mat_arc_posI_def
using arc_pos_mult by auto
have split: "?prod = ?head + ?rest"
by (rule scalar_prod_split_head[OF A B n0])
show "arc_pos (row A 0 ∙ col B 0)"
unfolding split
using ap arc_pos_plus by auto
qed (insert A B n0, auto)
lemma mat_arc_pos_mat_default:
assumes n0: "n > 0" shows "mat_arc_pos (mat_default default n)"
unfolding mat_arc_posI_def
unfolding mat_default_def
unfolding index_mat(1)[OF n0 n0]
using arc_pos_default by simp
lemma mat_not_all_ge:
assumes n_pos: "n > 0"
and A: "A ∈ carrier_mat n n"
and B: "B ∈ carrier_mat n n"
and apB: "mat_arc_pos B"
shows "∃C. C ∈ carrier_mat n n ∧ mat_ge C (0⇩m n n) ∧ mat_arc_pos C ∧ ¬ mat_ge A (B * C)"
proof -
define c where "c = A $$ (0,0)"
from apB have "arc_pos (B $$ (0,0))" unfolding mat_arc_posI_def .
from not_all_ge[OF this, of c] obtain e where e0: "e ≥ 0" and ae: "arc_pos e"
and nc: "¬ c ≥ B $$ (0,0) * e" by auto
let ?f = "λ i j. if i = 0 ∧ j = 0 then e else 0"
let ?C = "mat n n (λ (i,j). ?f i j)"
have C: "?C ∈ carrier_mat n n" by auto
have C00: "?C $$ (0,0) = e" using n_pos by auto
show ?thesis
proof(intro exI conjI)
show "?C ≥⇩m 0⇩m n n"
by (rule mat_geI[of _ n n], auto simp: ge_refl e0)
show "mat_arc_pos ?C"
unfolding mat_arc_posI_def
unfolding C00 by (rule ae)
let ?mult = "B * ?C"
from n_pos obtain nn where n: "n = Suc nn" by (cases n, auto)
have col: "col ?C 0 = vec n (?f 0)" using n_pos by auto
let ?prod = "row B 0 ∙ col ?C 0"
let ?head = "B $$ (0,0) * ?C $$ (0,0)"
let ?rest = "∑i = 1..<n. B $$ (0, i) * ?C $$ (i, 0)"
from n_pos B have "?mult $$ (0,0) = ?prod" by auto
also have "… = ?head + ?rest"
by (rule scalar_prod_split_head[OF B C n_pos])
also have "?rest = 0"
by (rule sum.neutral, auto)
finally have "?mult $$ (0,0) = B $$ (0,0) * e" using n_pos by simp
with nc c_def have not_ge: "¬ A $$ (0,0) ≥ ?mult $$ (0,0)" by simp
show "¬ A ≥⇩m ?mult"
proof
assume "A ≥⇩m ?mult"
from mat_geD[OF this, of 0 0] A B not_ge n_pos show False by auto
qed
qed auto
qed
end
context SN_both_mono_ordered_semiring_1
begin
lemma mat_gt_arc_SN:
assumes n_pos: "n > 0"
shows "SN {(A,B) ∈ carrier_mat n n × carrier_mat n n. mat_arc_pos B ∧ mat_gt_arc A B}"
(is "SN ?rel")
proof (rule ccontr)
assume "¬ SN ?rel"
then obtain f A where "f (0 :: nat) = A" and steps: "∀ i. (f i, f (Suc i)) ∈ ?rel" unfolding SN_defs by blast
hence pos: "∀ i. arc_pos (f (Suc i) $$ (0,0))" unfolding mat_arc_posI_def by blast
have gt: "∀ i. f i $$ (0,0) ≻ f (Suc i) $$ (0,0)"
proof
fix i
from steps
have wf1: "f i ∈ carrier_mat n n"
and wf2: "f (Suc i) ∈ carrier_mat n n"
and gt: "mat_gt_arc (f i) (f (Suc i))" by auto
show "f i $$ (0,0) ≻ f (Suc i) $$ (0,0)"
using mat_comp_allE[OF gt wf1 wf2]
using index_zero_mat n_pos by force
qed
from pos gt SN show False unfolding SN_defs by force
qed
end
end