Theory PairVector (Isabelle repository version)

header {* Pairs as Vector Spaces *}

theory PairVector
imports GradientDeriv
begin

subsection {* Vector arithmetic *}

instantiation "*" :: (zero, zero) zero
begin

definition
  zero_prod_def: "0 = (0, 0)"

instance ..
end

instantiation "*" :: (plus, plus) plus
begin

definition
  plus_prod_def: "A + B = (fst A + fst B, snd A + snd B)"

instance ..
end

instantiation "*" :: (minus, minus) minus
begin

definition
  minus_prod_def: "A - B = (fst A - fst B, snd A - snd B)"

instance ..
end

instantiation "*" :: (uminus, uminus) uminus
begin

definition
  uminus_prod_def: "- A = (- fst A, - snd A)"

instance ..
end

instantiation "*" :: (scaleR, scaleR) scaleR
begin

definition
  scaleR_prod_def: "scaleR r A = (scaleR r (fst A), scaleR r (snd A))"

instance ..
end

instantiation "*" :: (norm, norm) norm
begin

definition
  norm_prod_def: "norm A = sqrt ((norm (fst A))² + (norm (snd A))²)"

instance ..
end

instantiation "*" :: (inner, inner) inner
begin

definition
  inner_prod_def: "inner A B = inner (fst A) (fst B) + inner (snd A) (snd B)"

instance ..
end

instantiation "*" :: (sgn_div_norm, sgn_div_norm) sgn_div_norm
begin

definition
  sgn_prod_def: "sgn (x::'a × 'b) = scaleR (inverse (norm x)) x"

instance
by default (rule sgn_prod_def)

end

lemma fst_zero [simp]: "fst 0 = 0"
  unfolding zero_prod_def by simp

lemma snd_zero [simp]: "snd 0 = 0"
  unfolding zero_prod_def by simp

lemma fst_add [simp]: "fst (A + B) = fst A + fst B"
  unfolding plus_prod_def by simp

lemma snd_add [simp]: "snd (A + B) = snd A + snd B"
  unfolding plus_prod_def by simp

lemma add_Pair [simp]: "(a, b) + (c, d) = (a + c, b + d)"
  unfolding plus_prod_def by simp

lemma fst_diff [simp]: "fst (A - B) = fst A - fst B"
  unfolding minus_prod_def by simp

lemma snd_diff [simp]: "snd (A - B) = snd A - snd B"
  unfolding minus_prod_def by simp

lemma diff_Pair [simp]: "(a, b) - (c, d) = (a - c, b - d)"
  unfolding minus_prod_def by simp

lemma fst_uminus [simp]: "fst (- A) = - fst A"
  unfolding uminus_prod_def by simp

lemma snd_uminus [simp]: "snd (- A) = - snd A"
  unfolding uminus_prod_def by simp

lemma uminus_Pair [simp]: "- (a, b) = (- a, - b)"
  unfolding uminus_prod_def by simp

lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)"
  unfolding scaleR_prod_def by simp

lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)"
  unfolding scaleR_prod_def by simp

lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
  unfolding scaleR_prod_def by simp

lemma norm_Pair [simp]: "norm (a, b) = sqrt ((norm a)² + (norm b)²)"
  unfolding norm_prod_def by simp

lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
  unfolding inner_prod_def by simp

lemmas expand_prod_eq = Pair_fst_snd_eq

instance "*" :: (semigroup_add, semigroup_add) semigroup_add
  by (intro_classes, simp add: expand_prod_eq add_assoc)

instance "*" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
  by (intro_classes, simp add: expand_prod_eq add_commute)

instance "*" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
  by (intro_classes, simp add: expand_prod_eq)

instance "*" :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
  by (intro_classes, simp_all add: expand_prod_eq)

instance "*" :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
  by (intro_classes, simp add: expand_prod_eq)

instance "*" :: (ab_group_add, ab_group_add) ab_group_add
  by (intro_classes, simp_all add: expand_prod_eq)

instance "*" :: (real_vector, real_vector) real_vector
  apply (intro_classes)
  apply (simp_all add: expand_prod_eq)
  apply (simp add: scaleR_right_distrib)
  apply (simp add: scaleR_left_distrib)
  done

subsection {* Product is a normed vector space *}

instance "*" :: (real_normed_vector, real_normed_vector) real_normed_vector
proof
  fix r :: real
  fix A B :: "'a::real_normed_vector × 'b::real_normed_vector"
  show "0 ≤ norm A"
    unfolding norm_prod_def by simp
  show "(norm A = 0) = (A = 0)"
    by (induct A) (simp add: expand_prod_eq)
  show "norm (A + B) ≤ norm A + norm B"
    unfolding norm_prod_def
    apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
    apply (simp add: add_mono power_mono norm_triangle_ineq)
    done
  show "norm (scaleR r A) = ¦r¦ * norm A"
    unfolding norm_prod_def
    apply (simp add: norm_scaleR power_mult_distrib)
    apply (simp add: right_distrib [symmetric])
    apply (simp add: real_sqrt_mult_distrib)
    done
qed

interpretation fst: bounded_linear [fst]
  apply (unfold_locales)
  apply (rule fst_add)
  apply (rule fst_scaleR)
  apply (rule_tac x="1" in exI, simp)
  done

interpretation snd: bounded_linear [snd]
  apply (unfold_locales)
  apply (rule snd_add)
  apply (rule snd_scaleR)
  apply (rule_tac x="1" in exI, simp)
  done

lemma LIMSEQ_Pair:
    "[|X ----> a; Y ----> b|] ==> (λn. (X n, Y n)) ----> (a, b)"
  apply (rule LIMSEQ_I)
  apply (subgoal_tac "0 < r / sqrt 2")
  apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
  apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
  apply (rename_tac M N, rule_tac x="max M N" in exI, safe)
  apply (simp add: real_sqrt_sum_squares_less)
  apply (simp add: divide_pos_pos)
  done

lemma Cauchy_Pair:
    "[|Cauchy X; Cauchy Y|] ==> Cauchy (λn. (X n, Y n))"
  apply (rule CauchyI)
  apply (subgoal_tac "0 < e / sqrt 2")
  apply (drule_tac e="e / sqrt 2" in CauchyD, safe)
  apply (drule_tac e="e / sqrt 2" in CauchyD, safe)
  apply (rename_tac M N, rule_tac x="max M N" in exI, safe)
  apply (simp add: real_sqrt_sum_squares_less)
  apply (simp add: divide_pos_pos)
  done

instance "*" :: (banach, banach) banach
proof
  fix X :: "nat => 'a × 'b"
  assume X: "Cauchy X"
  have 1: "(λn. fst (X n)) ----> lim (λn. fst (X n))"
    using fst.Cauchy [OF X]
    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
  have 2: "(λn. snd (X n)) ----> lim (λn. snd (X n))"
    using snd.Cauchy [OF X]
    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
  have "X ----> (lim (λn. fst (X n)), lim (λn. snd (X n)))"
    using LIMSEQ_Pair [OF 1 2] by simp
  thus "convergent X"
    by (rule convergentI)
qed

subsection {* Product is an inner product space *}

instance "*" :: (real_inner, real_inner) real_inner
proof
  fix r :: real
  fix A B C :: "'a::real_inner * 'b::real_inner"
  show "inner A B = inner B A"
    unfolding inner_prod_def
    by (simp add: inner_commute)
  show "inner (A + B) C = inner A C + inner B C"
    unfolding inner_prod_def
    by (simp add: inner_left_distrib)
  show "inner (scaleR r A) B = r * inner A B"
    unfolding inner_prod_def
    by (simp add: inner_scaleR_left right_distrib)
  show "0 ≤ inner A A"
    unfolding inner_prod_def
    by (intro add_nonneg_nonneg inner_ge_zero)
  show "(inner A A = 0) = (A = 0)"
    unfolding inner_prod_def
    apply (simp add: add_nonneg_eq_0_iff inner_ge_zero)
    apply (simp add: inner_eq_zero expand_prod_eq)
    done
  show "norm A = sqrt (inner A A)"
    unfolding norm_prod_def inner_prod_def
    by (simp add: norm_squared_eq_inner)
qed

end