Theory MTX_Preliminaries
section ‹ Mathematical Preliminaries ›
text ‹This section adds useful syntax, abbreviations and theorems to the Isabelle distribution. ›
theory MTX_Preliminaries
imports Hybrid_Systems_VCs.HS_Preliminaries
begin
subsection ‹ Syntax ›
abbreviation "𝖾 k ≡ axis k 1"
syntax
"_ivl_integral" :: "real ⇒ real ⇒ 'a ⇒ pttrn ⇒ bool" ("(3∫⇩_⇧_ (_)∂/_)" [0, 0, 10] 10)
translations
"∫⇩a⇧b f ∂x" ⇌ "CONST ivl_integral a b (λx. f)"
notation matrix_inv ("_⇧-⇧1" [90])
abbreviation "entries (A::'a^'n^'m) ≡ {A $ i $ j | i j. i ∈ UNIV ∧ j ∈ UNIV}"
subsection ‹ Topology and sets ›
lemmas compact_imp_bdd_above = compact_imp_bounded[THEN bounded_imp_bdd_above]
lemma comp_cont_image_spec: "continuous_on T f ⟹ compact T ⟹ compact {f t |t. t ∈ T}"
using compact_continuous_image by (simp add: Setcompr_eq_image)
lemmas bdd_above_cont_comp_spec = compact_imp_bdd_above[OF comp_cont_image_spec]
lemmas bdd_above_norm_cont_comp = continuous_on_norm[THEN bdd_above_cont_comp_spec]
lemma open_cballE: "t⇩0 ∈ T ⟹ open T ⟹ ∃e>0. cball t⇩0 e ⊆ T"
using open_contains_cball by blast
lemma open_ballE: "t⇩0 ∈ T ⟹ open T ⟹ ∃e>0. ball t⇩0 e ⊆ T"
using open_contains_ball by blast
lemma funcset_UNIV: "f ∈ A → UNIV"
by auto
lemma finite_image_of_finite[simp]:
fixes f::"'a::finite ⇒ 'b"
shows "finite {x. ∃i. x = f i}"
using finite_Atleast_Atmost_nat by force
lemma finite_image_of_finite2:
fixes f :: "'a::finite ⇒ 'b::finite ⇒ 'c"
shows "finite {f x y |x y. P x y}"
proof-
have "finite (⋃x. {f x y|y. P x y})"
by simp
moreover have "{f x y|x y. P x y} = (⋃x. {f x y|y. P x y})"
by auto
ultimately show ?thesis
by simp
qed
subsection ‹ Functions ›
lemma finite_sum_univ_singleton: "(sum g UNIV) = sum g {i::'a::finite} + sum g (UNIV - {i})"
by (metis add.commute finite_class.finite_UNIV sum.subset_diff top_greatest)
lemma suminfI:
fixes f :: "nat ⇒ 'a::{t2_space,comm_monoid_add}"
shows "f sums k ⟹ suminf f = k"
unfolding sums_iff by simp
lemma suminf_eq_sum:
fixes f :: "nat ⇒ ('a::real_normed_vector)"
assumes "⋀n. n > m ⟹ f n = 0"
shows "(∑n. f n) = (∑n ≤ m. f n)"
using assms by (meson atMost_iff finite_atMost not_le suminf_finite)
lemma suminf_multr: "summable f ⟹ (∑n. f n * c) = (∑n. f n) * c" for c::"'a::real_normed_algebra"
by (rule bounded_linear.suminf [OF bounded_linear_mult_left, symmetric])
lemma sum_if_then_else_simps[simp]:
fixes q :: "('a::semiring_0)" and i :: "'n::finite"
shows "(∑j∈UNIV. f j * (if j = i then q else 0)) = f i * q"
and "(∑j∈UNIV. f j * (if i = j then q else 0)) = f i * q"
and "(∑j∈UNIV. (if i = j then q else 0) * f j) = q * f i"
and "(∑j∈UNIV. (if j = i then q else 0) * f j) = q * f i"
by (auto simp: finite_sum_univ_singleton[of _ i])
subsection ‹ Suprema ›
lemma le_max_image_of_finite[simp]:
fixes f::"'a::finite ⇒ 'b::linorder"
shows "(f i) ≤ Max {x. ∃i. x = f i}"
by (rule Max.coboundedI, simp_all) (rule_tac x=i in exI, simp)
lemma cSup_eq:
fixes c::"'a::conditionally_complete_lattice"
assumes "∀x ∈ X. x ≤ c" and "∃x ∈ X. c ≤ x"
shows "Sup X = c"
by (metis assms cSup_eq_maximum order_class.order.antisym)
lemma cSup_mem_eq:
"c ∈ X ⟹ ∀x ∈ X. x ≤ c ⟹ Sup X = c" for c::"'a::conditionally_complete_lattice"
by (rule cSup_eq, auto)
lemma cSup_finite_ex:
"finite X ⟹ X ≠ {} ⟹ ∃x∈X. Sup X = x" for X::"'a::conditionally_complete_linorder set"
by (metis (full_types) bdd_finite(1) cSup_upper finite_Sup_less_iff order_less_le)
lemma cMax_finite_ex:
"finite X ⟹ X ≠ {} ⟹ ∃x∈X. Max X = x" for X::"'a::conditionally_complete_linorder set"
apply(subst cSup_eq_Max[symmetric])
using cSup_finite_ex by auto
lemma finite_nat_minimal_witness:
fixes P :: "('a::finite) ⇒ nat ⇒ bool"
assumes "∀i. ∃N::nat. ∀n ≥ N. P i n"
shows "∃N. ∀i. ∀n ≥ N. P i n"
proof-
let "?bound i" = "(LEAST N. ∀n ≥ N. P i n)"
let ?N = "Max {?bound i |i. i ∈ UNIV}"
{fix n::nat and i::'a
assume "n ≥ ?N"
obtain M where "∀n ≥ M. P i n"
using assms by blast
hence obs: "∀ m ≥ ?bound i. P i m"
using LeastI[of "λN. ∀n ≥ N. P i n"] by blast
have "finite {?bound i |i. i ∈ UNIV}"
by simp
hence "?N ≥ ?bound i"
using Max_ge by blast
hence "n ≥ ?bound i"
using ‹n ≥ ?N› by linarith
hence "P i n"
using obs by blast}
thus "∃N. ∀i n. N ≤ n ⟶ P i n"
by blast
qed
subsection ‹ Real numbers ›
named_theorems field_power_simps "simplification rules for powers to the nth"
declare semiring_normalization_rules(18) [field_power_simps]
and semiring_normalization_rules(26) [field_power_simps]
and semiring_normalization_rules(27) [field_power_simps]
and semiring_normalization_rules(28) [field_power_simps]
and semiring_normalization_rules(29) [field_power_simps]
text ‹WARNING: Adding @{thm semiring_normalization_rules(27)} to our tactic makes
its combination with simp to loop infinitely in some proofs.›
lemma sq_le_cancel:
shows "(a::real) ≥ 0 ⟹ b ≥ 0 ⟹ a^2 ≤ b * a ⟹ a ≤ b"
and "(a::real) ≥ 0 ⟹ b ≥ 0 ⟹ a^2 ≤ a * b ⟹ a ≤ b"
apply (metis less_eq_real_def mult.commute mult_le_cancel_left semiring_normalization_rules(29))
by (metis less_eq_real_def mult_le_cancel_left semiring_normalization_rules(29))
lemma frac_diff_eq1: "a ≠ b ⟹ a / (a - b) - b / (a - b) = 1" for a::real
by (metis (no_types) ab_left_minus add.commute add_left_cancel
diff_divide_distrib diff_minus_eq_add div_self)
lemma exp_add: "x * y - y * x = 0 ⟹ exp (x + y) = exp x * exp y"
by (rule exp_add_commuting) (simp add: ac_simps)
lemmas mult_exp_exp = exp_add[symmetric]
subsection ‹ Vectors and matrices ›
lemma sum_axis[simp]:
fixes q :: "('a::semiring_0)"
shows "(∑j∈UNIV. f j * axis i q $ j) = f i * q"
and "(∑j∈UNIV. axis i q $ j * f j) = q * f i"
unfolding axis_def by(auto simp: vec_eq_iff)
lemma sum_scalar_nth_axis: "sum (λi. (x $ i) *s 𝖾 i) UNIV = x" for x :: "('a::semiring_1)^'n"
unfolding vec_eq_iff axis_def by simp
lemma scalar_eq_scaleR[simp]: "c *s x = c *⇩R x"
unfolding vec_eq_iff by simp
lemma matrix_add_rdistrib: "((B + C) ** A) = (B ** A) + (C ** A)"
by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)
lemma vec_mult_inner: "(A *v v) ∙ w = v ∙ (transpose A *v w)" for A :: "real ^'n^'n"
unfolding matrix_vector_mult_def transpose_def inner_vec_def
apply(simp add: sum_distrib_right sum_distrib_left)
apply(subst sum.swap)
apply(subgoal_tac "∀i j. A $ i $ j * v $ j * w $ i = v $ j * (A $ i $ j * w $ i)")
by presburger simp
lemma uminus_axis_eq[simp]: "- axis i k = axis i (-k)" for k :: "'a::ring"
unfolding axis_def by(simp add: vec_eq_iff)
lemma norm_axis_eq[simp]: "∥axis i k∥ = ∥k∥"
proof(simp add: axis_def norm_vec_def L2_set_def)
let "?δ⇩K" = "λi j k. if i = j then k else 0"
have "(∑j∈UNIV. (∥(?δ⇩K j i k)∥)⇧2) = (∑j∈{i}. (∥(?δ⇩K j i k)∥)⇧2) + (∑j∈(UNIV-{i}). (∥(?δ⇩K j i k)∥)⇧2)"
using finite_sum_univ_singleton by blast
also have "... = (∥k∥)⇧2"
by simp
finally show "sqrt (∑j∈UNIV. (norm (if j = i then k else 0))⇧2) = norm k"
by simp
qed
lemma matrix_axis_0:
fixes A :: "('a::idom)^'n^'m"
assumes "k ≠ 0 " and h:"∀i. (A *v (axis i k)) = 0"
shows "A = 0"
proof-
{fix i::'n
have "0 = (∑j∈UNIV. (axis i k) $ j *s column j A)"
using h matrix_mult_sum[of A "axis i k"] by simp
also have "... = k *s column i A"
by (simp add: axis_def vector_scalar_mult_def column_def vec_eq_iff mult.commute)
finally have "k *s column i A = 0"
unfolding axis_def by simp
hence "column i A = 0"
using vector_mul_eq_0 ‹k ≠ 0› by blast}
thus "A = 0"
unfolding column_def vec_eq_iff by simp
qed
lemma scaleR_norm_sgn_eq: "(∥x∥) *⇩R sgn x = x"
by (metis divideR_right norm_eq_zero scale_eq_0_iff sgn_div_norm)
lemma vector_scaleR_commute: "A *v c *⇩R x = c *⇩R (A *v x)" for x :: "('a::real_normed_algebra_1)^'n"
unfolding scaleR_vec_def matrix_vector_mult_def by(auto simp: vec_eq_iff scaleR_right.sum)
lemma scaleR_vector_assoc: "c *⇩R (A *v x) = (c *⇩R A) *v x" for x :: "('a::real_normed_algebra_1)^'n"
unfolding matrix_vector_mult_def by(auto simp: vec_eq_iff scaleR_right.sum)
lemma mult_norm_matrix_sgn_eq:
fixes x :: "('a::real_normed_algebra_1)^'n"
shows "(∥A *v sgn x∥) * (∥x∥) = ∥A *v x∥"
proof-
have "∥A *v x∥ = ∥A *v ((∥x∥) *⇩R sgn x)∥"
by(simp add: scaleR_norm_sgn_eq)
also have "... = (∥A *v sgn x∥) * (∥x∥)"
by(simp add: vector_scaleR_commute)
finally show ?thesis ..
qed
subsection‹ Diagonalization ›
lemma invertibleI: "A ** B = mat 1 ⟹ B ** A = mat 1 ⟹ invertible A"
unfolding invertible_def by auto
lemma invertibleD[simp]:
assumes "invertible A"
shows "A⇧-⇧1 ** A = mat 1" and "A ** A⇧-⇧1 = mat 1"
using assms unfolding matrix_inv_def invertible_def
by (simp_all add: verit_sko_ex')
lemma matrix_inv_unique:
assumes "A ** B = mat 1" and "B ** A = mat 1"
shows "A⇧-⇧1 = B"
by (metis assms invertibleD(2) invertibleI matrix_mul_assoc matrix_mul_lid)
lemma invertible_matrix_inv: "invertible A ⟹ invertible (A⇧-⇧1)"
using invertibleD invertibleI by blast
lemma matrix_inv_idempotent[simp]: "invertible A ⟹ A⇧-⇧1⇧-⇧1 = A"
using invertibleD matrix_inv_unique by blast
lemma matrix_inv_matrix_mul:
assumes "invertible A" and "invertible B"
shows "(A ** B)⇧-⇧1 = B⇧-⇧1 ** A⇧-⇧1"
proof(rule matrix_inv_unique)
have "A ** B ** (B⇧-⇧1 ** A⇧-⇧1) = A ** (B ** B⇧-⇧1) ** A⇧-⇧1"
by (simp add: matrix_mul_assoc)
also have "... = mat 1"
using assms by simp
finally show "A ** B ** (B⇧-⇧1 ** A⇧-⇧1) = mat 1" .
next
have "B⇧-⇧1 ** A⇧-⇧1 ** (A ** B) = B⇧-⇧1 ** (A⇧-⇧1 ** A) ** B"
by (simp add: matrix_mul_assoc)
also have "... = mat 1"
using assms by simp
finally show "B⇧-⇧1 ** A⇧-⇧1 ** (A ** B) = mat 1" .
qed
lemma mat_inverse_simps[simp]:
fixes c :: "'a::division_ring"
assumes "c ≠ 0"
shows "mat (inverse c) ** mat c = mat 1"
and "mat c ** mat (inverse c) = mat 1"
unfolding matrix_matrix_mult_def mat_def by (auto simp: vec_eq_iff assms)
lemma matrix_inv_mat[simp]: "c ≠ 0 ⟹ (mat c)⇧-⇧1 = mat (inverse c)" for c :: "'a::division_ring"
by (simp add: matrix_inv_unique)
lemma invertible_mat[simp]: "c ≠ 0 ⟹ invertible (mat c)" for c :: "'a::division_ring"
using invertibleI mat_inverse_simps(1) mat_inverse_simps(2) by blast
lemma matrix_inv_mat_1: "(mat (1::'a::division_ring))⇧-⇧1 = mat 1"
by simp
lemma invertible_mat_1: "invertible (mat (1::'a::division_ring))"
by simp
definition similar_matrix :: "('a::semiring_1)^'m^'m ⇒ ('a::semiring_1)^'n^'n ⇒ bool" (infixr "∼" 25)
where "similar_matrix A B ⟷ (∃ P. invertible P ∧ A = P⇧-⇧1 ** B ** P)"
lemma similar_matrix_refl[simp]: "A ∼ A" for A :: "'a::division_ring^'n^'n"
by (unfold similar_matrix_def, rule_tac x="mat 1" in exI, simp)
lemma similar_matrix_simm: "A ∼ B ⟹ B ∼ A" for A B :: "('a::semiring_1)^'n^'n"
apply(unfold similar_matrix_def, clarsimp)
apply(rule_tac x="P⇧-⇧1" in exI, simp add: invertible_matrix_inv)
by (metis invertible_def matrix_inv_unique matrix_mul_assoc matrix_mul_lid matrix_mul_rid)
lemma similar_matrix_trans: "A ∼ B ⟹ B ∼ C ⟹ A ∼ C" for A B C :: "('a::semiring_1)^'n^'n"
proof(unfold similar_matrix_def, clarsimp)
fix P Q
assume "A = P⇧-⇧1 ** (Q⇧-⇧1 ** C ** Q) ** P" and "B = Q⇧-⇧1 ** C ** Q"
let ?R = "Q ** P"
assume inverts: "invertible Q" "invertible P"
hence "?R⇧-⇧1 = P⇧-⇧1 ** Q⇧-⇧1"
by (rule matrix_inv_matrix_mul)
also have "invertible ?R"
using inverts invertible_mult by blast
ultimately show "∃R. invertible R ∧ P⇧-⇧1 ** (Q⇧-⇧1 ** C ** Q) ** P = R⇧-⇧1 ** C ** R"
by (metis matrix_mul_assoc)
qed
lemma mat_vec_nth_simps[simp]:
"i = j ⟹ mat c $ i $ j = c"
"i ≠ j ⟹ mat c $ i $ j = 0"
by (simp_all add: mat_def)
definition "diag_mat f = (χ i j. if i = j then f i else 0)"
lemma diag_mat_vec_nth_simps[simp]:
"i = j ⟹ diag_mat f $ i $ j = f i"
"i ≠ j ⟹ diag_mat f $ i $ j = 0"
unfolding diag_mat_def by simp_all
lemma diag_mat_const_eq[simp]: "diag_mat (λi. c) = mat c"
unfolding mat_def diag_mat_def by simp
lemma matrix_vector_mul_diag_mat: "diag_mat f *v s = (χ i. f i * s$i)"
unfolding diag_mat_def matrix_vector_mult_def by simp
lemma matrix_vector_mul_diag_axis[simp]: "diag_mat f *v (axis i k) = axis i (f i * k)"
by (simp add: matrix_vector_mul_diag_mat axis_def fun_eq_iff)
lemma matrix_mul_diag_matl: "diag_mat f ** A = (χ i j. f i * A$i$j)"
unfolding diag_mat_def matrix_matrix_mult_def by simp
lemma matrix_matrix_mul_diag_matr: "A ** diag_mat f = (χ i j. A$i$j * f j)"
unfolding diag_mat_def matrix_matrix_mult_def apply(clarsimp simp: fun_eq_iff)
subgoal for i j
by (auto simp: finite_sum_univ_singleton[of _ j])
done
lemma matrix_mul_diag_diag: "diag_mat f ** diag_mat g = diag_mat (λi. f i * g i)"
unfolding diag_mat_def matrix_matrix_mult_def vec_eq_iff by simp
lemma compow_matrix_mul_diag_mat_eq: "((**) (diag_mat f) ^^ n) (mat 1) = diag_mat (λi. f i^n)"
apply(induct n, simp_all add: matrix_mul_diag_matl)
by (auto simp: vec_eq_iff diag_mat_def)
lemma compow_similar_diag_mat_eq:
assumes "invertible P"
and "A = P⇧-⇧1 ** (diag_mat f) ** P"
shows "((**) A ^^ n) (mat 1) = P⇧-⇧1 ** (diag_mat (λi. f i^n)) ** P"
proof(induct n, simp_all add: assms)
fix n::nat
have "P⇧-⇧1 ** diag_mat f ** P ** (P⇧-⇧1 ** diag_mat (λi. f i ^ n) ** P) =
P⇧-⇧1 ** diag_mat f ** diag_mat (λi. f i ^ n) ** P" (is "?lhs = _")
by (metis (no_types, lifting) assms(1) invertibleD(2) matrix_mul_rid matrix_mul_assoc)
also have "... = P⇧-⇧1 ** diag_mat (λi. f i * f i ^ n) ** P" (is "_ = ?rhs")
by (metis (full_types) matrix_mul_assoc matrix_mul_diag_diag)
finally show "?lhs = ?rhs" .
qed
lemma compow_similar_diag_mat:
assumes "A ∼ (diag_mat f)"
shows "((**) A ^^ n) (mat 1) ∼ diag_mat (λi. f i^n)"
proof(unfold similar_matrix_def)
obtain P where "invertible P" and "A = P⇧-⇧1 ** (diag_mat f) ** P"
using assms unfolding similar_matrix_def by blast
thus "∃P. invertible P ∧ ((**) A ^^ n) (mat 1) = P⇧-⇧1 ** diag_mat (λi. f i ^ n) ** P"
using compow_similar_diag_mat_eq by blast
qed
no_notation matrix_inv ("_⇧-⇧1" [90])
and similar_matrix (infixr "∼" 25)
end