Theory VectorType

header {* Finite-Dimensional Vectors *}

theory VectorType
imports InnerProduct
begin

subsection {* Type definition *}

typedef (open) ('a,'n) vec (infixl "^" 80) = "UNIV :: ('n => 'a) set" ..

declare Abs_vec_inverse [simplified, iff]

lemma expand_vec_eq:
  "x = y <-> (∀i. Rep_vec x i = Rep_vec y i)"
by (simp add: Rep_vec_inject [symmetric] expand_fun_eq)

lemma vec_ext:
  "(!!i. Rep_vec x i = Rep_vec y i) ==> x = y"
by (simp add: expand_vec_eq)

subsection {* Vector arithmetic *}

instantiation vec :: (zero, type) zero
begin

definition
  zero_vec_def: "0 = Abs_vec (λi. 0)"

instance ..
end

instantiation vec :: (plus, type) plus
begin

definition
  plus_vec_def: "x + y = Abs_vec (λi. Rep_vec x i + Rep_vec y i)"

instance ..
end

instantiation vec :: (minus, type) minus
begin

definition
  minus_vec_def: "x - y = Abs_vec (λi. Rep_vec x i - Rep_vec y i)"

instance ..
end

instantiation vec :: (uminus, type) uminus
begin

definition
  uminus_vec_def: "- x = Abs_vec (λi. - Rep_vec x i)"

instance ..
end

lemma Rep_vec_zero [simp]: "Rep_vec 0 i = 0"
  unfolding zero_vec_def by simp

lemma Rep_vec_add [simp]:
  "Rep_vec (x + y) i = Rep_vec x i + Rep_vec y i"
  unfolding plus_vec_def by simp

lemma Rep_vec_diff [simp]:
  "Rep_vec (x - y) i = Rep_vec x i - Rep_vec y i"
  unfolding minus_vec_def by simp

lemma Rep_vec_uminus [simp]:
  "Rep_vec (- x) i = - Rep_vec x i"
  unfolding uminus_vec_def by simp

text "Addition is associative"
instance vec :: (semigroup_add, type) semigroup_add
by (intro_classes, simp add: expand_vec_eq add_assoc)

text "Addition is commutative"
instance vec :: (ab_semigroup_add, type) ab_semigroup_add
by (intro_classes, simp add: expand_vec_eq add_commute)

text "Zero is additive identity"
instance vec :: (comm_monoid_add, type) comm_monoid_add
by (intro_classes, simp add: expand_vec_eq)

text "Addition has cancellation property"
instance vec :: (cancel_semigroup_add, type) cancel_semigroup_add
by (intro_classes, simp_all add: expand_vec_eq)

instance vec :: (cancel_ab_semigroup_add, type) cancel_ab_semigroup_add
by (intro_classes, simp add: expand_vec_eq)

text "Negation is additive inverse"
instance vec :: (ab_group_add, type) ab_group_add
by (intro_classes, simp_all add: expand_vec_eq)


subsection {* Vector is a real vector space *}

instantiation vec :: (scaleR, type) scaleR
begin

definition
  scaleR_vec_def: "scaleR r x = Abs_vec (λi. scaleR r (Rep_vec x i))"

instance ..
end

lemma Rep_vec_scaleR [simp]:
  "Rep_vec (scaleR r x) i = scaleR r (Rep_vec x i)"
  unfolding scaleR_vec_def by simp

instance vec :: (real_vector, type) real_vector
apply (intro_classes)
apply (simp_all add: expand_vec_eq)
apply (simp add: scaleR_right_distrib)
apply (simp add: scaleR_left_distrib)
done


subsection {* Square root of sum of squares *}

definition
  "set_l2 f A = sqrt (∑i∈A. (f i)²)"

lemma set_l2_infinite [simp]: "¬ finite A ==> set_l2 f A = 0"
unfolding set_l2_def by simp

lemma set_l2_empty [simp]: "set_l2 f {} = 0"
unfolding set_l2_def by simp

lemma set_l2_insert [simp]:
  "[|finite F; a ∉ F|] ==>
   set_l2 f (insert a F) = sqrt ((f a)² + (set_l2 f F)²)"
unfolding set_l2_def by (simp add: setsum_nonneg)

lemma set_l2_nonneg [simp]: "0 ≤ set_l2 f A"
unfolding set_l2_def by (simp add: setsum_nonneg)

lemma set_l2_0': "∀a∈A. f a = 0 ==> set_l2 f A = 0"
unfolding set_l2_def by simp

lemma set_l2_mono:
  assumes "!!i. i ∈ K ==> f i ≤ g i"
  assumes "!!i. i ∈ K ==> 0 ≤ f i"
  shows "set_l2 f K ≤ set_l2 g K"
unfolding set_l2_def
by (simp add: setsum_nonneg setsum_mono power_mono prems)

lemma set_l2_right_distrib:
  "0 ≤ r ==> r * set_l2 f A = set_l2 (λx. r * f x) A"
unfolding set_l2_def
apply (simp add: power_mult_distrib)
apply (simp add: setsum_right_distrib [symmetric])
apply (simp add: real_sqrt_mult setsum_nonneg)
done

lemma set_l2_left_distrib:
  "0 ≤ r ==> set_l2 f A * r = set_l2 (λx. f x * r) A"
unfolding set_l2_def
apply (simp add: power_mult_distrib)
apply (simp add: setsum_left_distrib [symmetric])
apply (simp add: real_sqrt_mult setsum_nonneg)
done

lemma setsum_nonneg_eq_0_iff:
  fixes f :: "'a => 'b::pordered_ab_group_add"
  shows "[|finite A; ∀x∈A. 0 ≤ f x|] ==> setsum f A = 0 <-> (∀x∈A. f x = 0)"
apply (induct set: finite, simp)
apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
done

lemma set_l2_eq_0_iff: "finite A ==> set_l2 f A = 0 <-> (∀x∈A. f x = 0)"
unfolding set_l2_def
by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)

lemma set_l2_triangle_ineq:
  shows "set_l2 (λi. f i + g i) A ≤ set_l2 f A + set_l2 g A"
proof (cases "finite A")
  case False
  thus ?thesis by simp
next
  case True
  thus ?thesis
  proof (induct set: finite)
    case empty
    show ?case by simp
  next
    case (insert x F)
    hence "sqrt ((f x + g x)² + (set_l2 (λi. f i + g i) F)²) ≤
           sqrt ((f x + g x)² + (set_l2 f F + set_l2 g F)²)"
      by (intro real_sqrt_le_mono add_left_mono power_mono insert
                set_l2_nonneg add_increasing zero_le_power2)
    also have
      "… ≤ sqrt ((f x)² + (set_l2 f F)²) + sqrt ((g x)² + (set_l2 g F)²)"
      by (rule real_sqrt_sum_squares_triangle_ineq)
    finally show ?case
      using insert by simp
  qed
qed

lemma sqrt_sum_squares_le_sum:
  "[|0 ≤ x; 0 ≤ y|] ==> sqrt (x² + y²) ≤ x + y"
apply (rule power2_le_imp_le)
apply (simp add: power2_sum)
apply (simp add: mult_nonneg_nonneg)
apply (simp add: add_nonneg_nonneg)
done

lemma set_l2_le_setsum [rule_format]:
  "(∀i∈A. 0 ≤ f i) --> set_l2 f A ≤ setsum f A"
apply (cases "finite A")
apply (induct set: finite)
apply simp
apply clarsimp
apply (erule order_trans [OF sqrt_sum_squares_le_sum])
apply simp
apply simp
apply simp
done

lemma sqrt_sum_squares_le_sum_abs: "sqrt (x² + y²) ≤ ¦x¦ + ¦y¦"
apply (rule power2_le_imp_le)
apply (simp add: power2_sum)
apply (simp add: mult_nonneg_nonneg)
apply (simp add: add_nonneg_nonneg)
done

lemma set_l2_le_setsum_abs: "set_l2 f A ≤ (∑i∈A. ¦f i¦)"
apply (cases "finite A")
apply (induct set: finite)
apply simp
apply simp
apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
apply simp
apply simp
done

lemma set_l2_mult_ineq_lemma:
  fixes a b c d :: real
  shows "2 * (a * c) * (b * d) ≤ a² * d² + b² * c²"
proof -
  have "0 ≤ (a * d - b * c)²" by simp
  also have "… = a² * d² + b² * c² - 2 * (a * d) * (b * c)"
    by (simp only: power2_diff power_mult_distrib)
  also have "… = a² * d² + b² * c² - 2 * (a * c) * (b * d)"
    by simp
  finally show "2 * (a * c) * (b * d) ≤ a² * d² + b² * c²"
    by simp
qed

lemma set_l2_mult_ineq: "(∑i∈A. ¦f i¦ * ¦g i¦) ≤ set_l2 f A * set_l2 g A"
apply (cases "finite A")
apply (induct set: finite)
apply simp
apply (rule power2_le_imp_le, simp)
apply (rule order_trans)
apply (rule power_mono)
apply (erule add_left_mono)
apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg)
apply (simp add: power2_sum)
apply (simp add: power_mult_distrib)
apply (simp add: right_distrib left_distrib)
apply (rule ord_le_eq_trans)
apply (rule set_l2_mult_ineq_lemma)
apply simp
apply (intro mult_nonneg_nonneg set_l2_nonneg)
apply simp
done

lemma member_le_set_l2: "[|finite A; i ∈ A|] ==> f i ≤ set_l2 f A"
apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
apply fast
apply (subst set_l2_insert)
apply simp
apply simp
apply simp
done


subsection {* Vectors are a real normed vector space *}

instantiation vec :: (norm, finite) norm
begin

definition
  norm_vec_def: "norm x = set_l2 (λi. norm (Rep_vec x i)) UNIV"

instance ..
end

lemma vec_norm_ge_zero:
  fixes x :: "'a::real_normed_vector ^ 'n::finite"
  shows "0 ≤ norm x"
unfolding norm_vec_def by (rule set_l2_nonneg)

lemma vec_norm_eq_zero:
  fixes x :: "'a::real_normed_vector ^ 'n::finite"
  shows "(norm x = 0) = (x = 0)"
unfolding norm_vec_def
by (simp add: set_l2_eq_0_iff expand_vec_eq)

lemma vec_norm_triangle_ineq:
  fixes x y :: "'a::real_normed_vector ^ 'n::finite"
  shows "norm (x + y) ≤ norm x + norm y"
unfolding norm_vec_def
apply (rule order_trans [OF _ set_l2_triangle_ineq])
apply (simp add: set_l2_mono norm_triangle_ineq)
done

lemma vec_norm_scaleR:
  fixes x :: "'a::real_normed_vector ^ 'n::finite"
  shows "norm (scaleR r x) = ¦r¦ * norm x"
unfolding norm_vec_def
by (simp add: norm_scaleR set_l2_right_distrib)

instantiation vec :: (real_normed_vector, finite) real_normed_vector
begin

definition
  sgn_vec_def: "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"

instance
apply (intro_classes)
apply (rule sgn_vec_def)
apply (rule vec_norm_ge_zero)
apply (rule vec_norm_eq_zero)
apply (rule vec_norm_triangle_ineq)
apply (rule vec_norm_scaleR)
done

end

lemma norm_Rep_vec_le: "norm (Rep_vec x i) ≤ norm x"
unfolding norm_vec_def
by (rule member_le_set_l2 [OF finite], simp)

interpretation Rep_vec: bounded_linear ["λx. Rep_vec x i"]
apply (unfold_locales)
apply (rule Rep_vec_add)
apply (rule Rep_vec_scaleR)
apply (rule_tac x=1 in exI)
apply (simp add: norm_Rep_vec_le)
done


subsection {* Vectors are an inner product space *}

instantiation vec :: (inner, finite) inner
begin

definition
  inner_vec_def: "inner x y = (∑i∈UNIV. inner (Rep_vec x i) (Rep_vec y i))"

instance ..
end

lemma vec_inner_commute:
  fixes x y :: "'a::real_inner ^ 'n::finite"
  shows "inner x y = inner y x"
unfolding inner_vec_def by (simp add: inner_commute)

lemma vec_inner_left_distrib:
  fixes x y z :: "'a::real_inner ^ 'n::finite"
  shows "inner (x + y) z = inner x z + inner y z"
unfolding inner_vec_def
by (simp add: inner_left_distrib setsum_addf)

lemma vec_inner_scaleR_left:
  fixes x y :: "'a::real_inner ^ 'n::finite"
  shows "inner (scaleR r x) y = r * inner x y"
unfolding inner_vec_def
by (simp add: inner_scaleR_left setsum_right_distrib)

lemma vec_inner_ge_zero:
  fixes x :: "'a::real_inner ^ 'n::finite"
  shows "0 ≤ inner x x"
unfolding inner_vec_def
by (simp add: setsum_nonneg inner_ge_zero)

lemma vec_inner_eq_zero:
  fixes x :: "'a::real_inner ^ 'n::finite"
  shows "(inner x x = 0) = (x = 0)"
unfolding inner_vec_def
apply (simp add: setsum_nonneg_eq_0_iff finite inner_ge_zero)
apply (simp add: inner_eq_zero expand_vec_eq)
done

lemma vec_norm_eq_sqrt_inner:
  fixes x :: "'a::real_inner ^ 'n::finite"
  shows "norm x = sqrt (inner x x)"
unfolding norm_vec_def inner_vec_def
unfolding set_l2_def
by (simp add: norm_squared_eq_inner)

instance vec :: (real_inner, finite) real_inner
apply (intro_classes)
apply (rule vec_inner_commute)
apply (rule vec_inner_left_distrib)
apply (rule vec_inner_scaleR_left)
apply (rule vec_inner_ge_zero)
apply (rule vec_inner_eq_zero)
apply (rule vec_norm_eq_sqrt_inner)
done


subsection {* Vector is a functor *}

definition
  vec_map :: "('a => 'b) => 'a ^ 'n::finite => 'b ^ 'n" where
  "vec_map f x = Abs_vec (λi. f (Rep_vec x i))"

lemma Rep_vec_vec_map [simp]: "Rep_vec (vec_map f x) i = f (Rep_vec x i)"
unfolding vec_map_def by simp

lemma vec_map_id: "vec_map id = id"
by (rule ext, rule vec_ext, simp)

lemma vec_map_o: "vec_map (f o g) = vec_map f o vec_map g"
by (rule ext, rule vec_ext, simp)

lemma vec_map_ident [simp]: "vec_map (λa. a) = (λx. x)"
by (rule ext, rule vec_ext, simp)

lemma vec_map_map: "vec_map f (vec_map g x) = vec_map (λa. f (g a)) x"
by (rule vec_ext, simp)


subsection {* Vector dot product *}

definition
  dot :: "'a^'n => 'a^'n::finite => 'a::semiring_0" where
  "dot x y = (∑i∈UNIV. Rep_vec x i * Rep_vec y i)"

lemma dot_right_distrib: "dot x (y + z) = dot x y + dot x z"
unfolding dot_def by (simp add: right_distrib setsum_addf)

lemma dot_left_distrib: "dot (x + y) z = dot x z + dot y z"
unfolding dot_def by (simp add: left_distrib setsum_addf)

lemma dot_right_scaleR:
  fixes x y :: "'a::real_algebra ^ 'n::finite"
  shows "dot x (scaleR r y) = scaleR r (dot x y)"
unfolding dot_def by (simp add: scaleR_right.setsum)

lemma dot_left_scaleR:
  fixes x y :: "'a::real_algebra ^ 'n::finite"
  shows "dot (scaleR r x) y = scaleR r (dot x y)"
unfolding dot_def by (simp add: scaleR_right.setsum)

lemma norm_dot_ineq:
  fixes x y :: "'a::real_normed_algebra ^ 'n::finite"
  shows "norm (dot x y) ≤ norm x * norm y"
unfolding norm_vec_def dot_def
apply (rule order_trans)
apply (rule norm_setsum)
apply (rule order_trans)
apply (rule setsum_mono)
apply (rule norm_mult_ineq)
apply (rule ord_eq_le_trans [OF _ set_l2_mult_ineq])
apply simp
done

interpretation dot:
  bounded_bilinear ["λx y. dot x y::'a::real_normed_algebra"]
apply (unfold_locales)
apply (rule dot_left_distrib)
apply (rule dot_right_distrib)
apply (rule dot_left_scaleR)
apply (rule dot_right_scaleR)
apply (rule_tac x=1 in exI)
apply (simp add: norm_dot_ineq)
done

lemma dot_right_zero: "dot x 0 = 0"
unfolding dot_def by simp

lemma dot_left_zero: "dot 0 y = 0"
unfolding dot_def by simp


subsection {* Single-component vectors *}

definition
  vec1 :: "'n::finite => 'a::zero => 'a ^ 'n" where
  "vec1 j x = Abs_vec (λi. if i = j then x else 0)"

lemma Rep_vec_vec1 [simp]:
  "Rep_vec (vec1 j x) i = (if i = j then x else 0)"
unfolding vec1_def by simp

lemma vec1_zero [simp]: "vec1 j 0 = 0"
by (rule vec_ext, simp)

lemma vec1_add:
  fixes x y :: "'a::comm_monoid_add"
  shows "vec1 j (x + y) = vec1 j x + vec1 j y"
by (rule vec_ext, simp)

lemma vec1_diff:
  fixes x y :: "'a::ab_group_add"
  shows "vec1 j (x - y) = vec1 j x - vec1 j y"
by (rule vec_ext, simp)

lemma vec1_scaleR:
  fixes x :: "'a::real_vector"
  shows "vec1 j (scaleR r x) = scaleR r (vec1 j x)"
by (rule vec_ext, simp)

interpretation vec1: additive ["λx::'a::ab_group_add. vec1 j x"]
by unfold_locales (rule vec1_add)

lemma norm_vec1 [simp]:
  fixes a :: "'a::real_normed_vector"
  shows "norm (vec1 j a) = norm a"
unfolding norm_vec_def
apply (rule_tac s="insert j (UNIV - {j})" and t="UNIV" in subst)
apply fast
apply (subst set_l2_insert)
apply (rule finite)
apply simp
apply (simp add: set_l2_0')
done

interpretation vec1:
  bounded_linear ["λx::'a::real_normed_vector. vec1 j x"]
apply (unfold_locales)
apply (rule vec1_scaleR)
apply (rule_tac x=1 in exI, simp)
done

lemma Rep_vec_setsum: "Rep_vec (setsum f A) i = (∑x∈A. Rep_vec (f x) i)"
by (cases "finite A", induct set: finite, simp_all)

lemma setsum_vec1: "(∑i∈UNIV. vec1 i (f i)) = Abs_vec f"
apply (rule vec_ext, simp)
apply (simp add: Rep_vec_setsum)
apply (cut_tac x="i" in UNIV_I)
apply (erule setsum_diff1' [OF finite, THEN ssubst])
apply simp
done

end