Quelle Finite_Cartesian_Product.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Finite_Cartesian_Product.thy
    Author:     Amine Chaieb, University of Cambridge
*)

section \<open>Definition of Finite Cartesian Product Type\<close>

theory Finite_Cartesian_Product
imports
  Euclidean_Space
  L2_Norm
  "HOL-Library.Numeral_Type"
  "HOL-Library.Countable_Set"
  "HOL-Library.FuncSet"
begin

subsection\<^marker>\<open>tag unimportant\<close> \<open>Finite Cartesian products, with indexing and lambdas\<close>

typedef ('a, 'b) vec = "UNIV :: ('b::finite \ 'a) set"
  morphisms vec_nth vec_lambda ..

declare vec_lambda_inject [simplified, simp]

open_bundle vec_syntax
begin
notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
end

text \<open>
  Concrete syntax for \<open>('a, 'b) vec\<close>:
    \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
    \<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
\<close>
syntax "_vec_type" :: "type \ type \ type" (infixl \^\ 15)
syntax_types "_vec_type" \<rightleftharpoons> vec
parse_translation \<open>
  let
    fun vec t u = Syntax.const \<^type_syntax>\<open>vec\<close> $ t $ u;
    fun finite_vec_tr [t, u] =
      (case Term_Position.strip_positions u of
        v as Free (x, _) =>
          if Lexicon.is_tid x then
            vec t (Syntax.const \<^syntax_const>\<open>_ofsort\<close> $ v $
              Syntax.const \<^class_syntax>\<open>finite\<close>)
          else vec t u
      | _ => vec t u)
  in
    [(\<^syntax_const>\<open>_vec_type\<close>, K finite_vec_tr)]
  end
\<close>

lemma vec_eq_iff: "(x = y) \ (\i. x$i = y$i)"
  by (simp add: vec_nth_inject [symmetric] fun_eq_iff)

lemma vec_lambda_beta [simp]: "vec_lambda g $ i = g i"
  by (simp add: vec_lambda_inverse)

lemma vec_lambda_unique: "(\i. f$i = g i) \ vec_lambda g = f"
  by (auto simp add: vec_eq_iff)

lemma vec_lambda_eta [simp]: "(\ i. (g$i)) = g"
  by (simp add: vec_eq_iff)

subsection \<open>Cardinality of vectors\<close>

instance vec :: (finite, finite) finite
proof
  show "finite (UNIV :: ('a, 'b) vec set)"
  proof (subst bij_betw_finite)
    show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\_. UNIV :: 'a set))"
      by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
    have "finite (PiE (UNIV :: 'b set) (\_. UNIV :: 'a set))"
      by (intro finite_PiE) auto
    also have "(PiE (UNIV :: 'b set) (\_. UNIV :: 'a set)) = Pi UNIV (\_. UNIV)"
      by auto
    finally show "finite \" .
  qed
qed

lemma countable_PiE:
  "finite I \ (\i. i \ I \ countable (F i)) \ countable (Pi\<^sub>E I F)"
  by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)

instance vec :: (countable, finite) countable
proof
  have "countable (UNIV :: ('a, 'b) vec set)"
  proof (rule countableI_bij2)
    show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\_. UNIV :: 'a set))"
      by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
    have "countable (PiE (UNIV :: 'b set) (\_. UNIV :: 'a set))"
      by (intro countable_PiE) auto
    also have "(PiE (UNIV :: 'b set) (\_. UNIV :: 'a set)) = Pi UNIV (\_. UNIV)"
      by auto
    finally show "countable \" .
  qed
  thus "\t::('a, 'b) vec \ nat. inj t"
    by (auto elim!: countableE)
qed

lemma infinite_UNIV_vec:
  assumes "infinite (UNIV :: 'a set)"
  shows   "infinite (UNIV :: ('a^'b) set)"
proof (subst bij_betw_finite)
  show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\_. UNIV :: 'a set))"
    by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
  have "infinite (PiE (UNIV :: 'b set) (\_. UNIV :: 'a set))" (is "infinite ?A")
  proof
    assume "finite ?A"
    hence "finite ((\f. f undefined) ` ?A)"
      by (rule finite_imageI)
    also have "(\f. f undefined) ` ?A = UNIV"
      by auto
    finally show False
      using \<open>infinite (UNIV :: 'a set)\<close> by contradiction
  qed
  also have "?A = Pi UNIV (\_. UNIV)"
    by auto
  finally show "infinite (Pi (UNIV :: 'b set) (\_. UNIV :: 'a set))" .
qed

proposition CARD_vec [simp]:
  "CARD('a^'b) = CARD('a) ^ CARD('b)"
proof (cases "finite (UNIV :: 'a set)")
  case True
  show ?thesis
  proof (subst bij_betw_same_card)
    show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\_. UNIV :: 'a set))"
      by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
    have "CARD('a) ^ CARD('b) = card (PiE (UNIV :: 'b set) (\_. UNIV :: 'a set))"
      (is "_ = card ?A")
      by (subst card_PiE) (auto)
    also have "?A = Pi UNIV (\_. UNIV)"
      by auto
    finally show "card \ = CARD('a) ^ CARD('b)" ..
  qed
qed (simp_all add: infinite_UNIV_vec)

lemma countable_vector:
  fixes B:: "'n::finite \ 'a set"
  assumes "\i. countable (B i)"
  shows "countable {V. \i::'n::finite. V $ i \ B i}"
proof -
  have "f \ ($) ` {V. \i. V $ i \ B i}" if "f \ Pi\<^sub>E UNIV B" for f
  proof -
    have "\W. (\i. W $ i \ B i) \ ($) W = f"
      by (metis that PiE_iff UNIV_I vec_lambda_inverse)
    then show "f \ ($) ` {v. \i. v $ i \ B i}"
      by blast
  qed
  then have "Pi\<^sub>E UNIV B = vec_nth ` {V. \i::'n. V $ i \ B i}"
    by blast
  then have "countable (vec_nth ` {V. \i. V $ i \ B i})"
    by (metis finite_class.finite_UNIV countable_PiE assms)
  then have "countable (vec_lambda ` vec_nth ` {V. \i. V $ i \ B i})"
    by auto
  then show ?thesis
    by (simp add: image_comp o_def vec_nth_inverse)
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Group operations and class instances\<close>

instantiation vec :: (zero, finite) zero
begin
  definition "0 \ (\ i. 0)"
  instance ..
end

instantiation vec :: (plus, finite) plus
begin
  definition "(+) \ (\ x y. (\ i. x$i + y$i))"
  instance ..
end

instantiation vec :: (minus, finite) minus
begin
  definition "(-) \ (\ x y. (\ i. x$i - y$i))"
  instance ..
end

instantiation vec :: (uminus, finite) uminus
begin
  definition "uminus \ (\ x. (\ i. - (x$i)))"
  instance ..
end

lemma zero_index [simp]: "0 $ i = 0"
  unfolding zero_vec_def by simp

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

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

lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)"
  unfolding uminus_vec_def by simp

instance vec :: (semigroup_add, finite) semigroup_add
  by standard (simp add: vec_eq_iff add.assoc)

instance vec :: (ab_semigroup_add, finite) ab_semigroup_add
  by standard (simp add: vec_eq_iff add.commute)

instance vec :: (monoid_add, finite) monoid_add
  by standard (simp_all add: vec_eq_iff)

instance vec :: (comm_monoid_add, finite) comm_monoid_add
  by standard (simp add: vec_eq_iff)

instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add
  by standard (simp_all add: vec_eq_iff)

instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add
  by standard (simp_all add: vec_eq_iff diff_diff_eq)

instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..

instance vec :: (group_add, finite) group_add
  by standard (simp_all add: vec_eq_iff)

instance vec :: (ab_group_add, finite) ab_group_add
  by standard (simp_all add: vec_eq_iff)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Basic componentwise operations on vectors\<close>

instantiation vec :: (times, finite) times
begin

definition "(*) \ (\ x y. (\ i. (x$i) * (y$i)))"
instance ..

end

instantiation vec :: (one, finite) one
begin

definition "1 \ (\ i. 1)"
instance ..

end

instantiation vec :: (ord, finite) ord
begin

definition "x \ y \ (\i. x$i \ y$i)"
definition "x < (y::'a^'b) \ x \ y \ \ y \ x"
instance ..

end

text\<open>The ordering on one-dimensional vectors is linear.\<close>

instance vec:: (order, finite) order
  by standard (auto simp: less_eq_vec_def less_vec_def vec_eq_iff
      intro: order.trans order.antisym order.strict_implies_order)

instance vec :: (linorder, CARD_1) linorder
proof
  obtain a :: 'b where all: "\P. (\i. P i) \ P a"
  proof -
    have "CARD ('b) = 1" by (rule CARD_1)
    then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq)
    then have "\P. (\i\UNIV. P i) \ P b" by auto
    then show thesis by (auto intro: that)
  qed
  fix x y :: "'a^'b::CARD_1"
  note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps
  show "x \ y \ y \ x" by auto
qed

text\<open>Constant Vectors\<close>

definition "vec x = (\ i. x)"

text\<open>Also the scalar-vector multiplication.\<close>

definition vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl \*s\ 70)
  where "c *s x = (\ i. c * (x$i))"

text \<open>scalar product\<close>

definition scalar_product :: "'a :: semiring_1 ^ 'n \ 'a ^ 'n \ 'a" where
  "scalar_product v w = (\ i \ UNIV. v $ i * w $ i)"

subsection \<open>Real vector space\<close>

instantiation\<^marker>\<open>tag unimportant\<close> vec :: (real_vector, finite) real_vector
begin

definition\<^marker>\<open>tag important\<close> "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"

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

instance\<^marker>\<open>tag unimportant\<close>
  by standard (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)

end

subsection \<open>Topological space\<close>

instantiation\<^marker>\<open>tag unimportant\<close> vec :: (topological_space, finite) topological_space
begin

definition\<^marker>\<open>tag important\<close> [code del]:
  "open (S :: ('a ^ 'b) set) \
    (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
      (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"

instance\<^marker>\<open>tag unimportant\<close> proof
  show "open (UNIV :: ('a ^ 'b) set)"
    unfolding open_vec_def by auto
next
  fix S T :: "('a ^ 'b) set"
  assume "open S" "open T" thus "open (S \ T)"
    unfolding open_vec_def
    apply clarify
    apply (drule (1) bspec)+
    apply (clarify, rename_tac Sa Ta)
    apply (rule_tac x="\i. Sa i \ Ta i" in exI)
    apply (simp add: open_Int)
    done
next
  fix K :: "('a ^ 'b) set set"
  assume "\S\K. open S" thus "open (\K)"
    unfolding open_vec_def
    by (metis Union_iff)
qed

end

lemma open_vector_box: "\i. open (S i) \ open {x. \i. x $ i \ S i}"
  unfolding open_vec_def by auto

lemma open_vimage_vec_nth: "open S \ open ((\x. x $ i) -` S)"
  unfolding open_vec_def
  apply clarify
  apply (rule_tac x="\k. if k = i then S else UNIV" in exI, simp)
  done

lemma closed_vimage_vec_nth: "closed S \ closed ((\x. x $ i) -` S)"
  unfolding closed_open vimage_Compl [symmetric]
  by (rule open_vimage_vec_nth)

lemma closed_vector_box: "\i. closed (S i) \ closed {x. \i. x $ i \ S i}"
proof -
  have "{x. \i. x $ i \ S i} = (\i. (\x. x $ i) -` S i)" by auto
  thus "\i. closed (S i) \ closed {x. \i. x $ i \ S i}"
    by (simp add: closed_INT closed_vimage_vec_nth)
qed

lemma tendsto_vec_nth [tendsto_intros]:
  assumes "((\x. f x) \ a) net"
  shows "((\x. f x $ i) \ a $ i) net"
proof (rule topological_tendstoI)
  fix S assume "open S" "a $ i \ S"
  then have "open ((\y. y $ i) -` S)" "a \ ((\y. y $ i) -` S)"
    by (simp_all add: open_vimage_vec_nth)
  with assms have "eventually (\x. f x \ (\y. y $ i) -` S) net"
    by (rule topological_tendstoD)
  then show "eventually (\x. f x $ i \ S) net"
    by simp
qed

lemma isCont_vec_nth [simp]: "isCont f a \ isCont (\x. f x $ i) a"
  unfolding isCont_def by (rule tendsto_vec_nth)

lemma vec_tendstoI:
  assumes "\i. ((\x. f x $ i) \ a $ i) net"
  shows "((\x. f x) \ a) net"
proof (rule topological_tendstoI)
  fix S assume "open S" and "a \ S"
  then obtain A where A: "\i. open (A i)" "\i. a $ i \ A i"
    and S: "\y. \i. y $ i \ A i \ y \ S"
    unfolding open_vec_def by metis
  have "\i. eventually (\x. f x $ i \ A i) net"
    using assms A by (rule topological_tendstoD)
  hence "eventually (\x. \i. f x $ i \ A i) net"
    by (rule eventually_all_finite)
  thus "eventually (\x. f x \ S) net"
    by (rule eventually_mono, simp add: S)
qed

lemma tendsto_vec_lambda [tendsto_intros]:
  assumes "\i. ((\x. f x i) \ a i) net"
  shows "((\x. \ i. f x i) \ (\ i. a i)) net"
  using assms by (simp add: vec_tendstoI)

lemma open_image_vec_nth: assumes "open S" shows "open ((\x. x $ i) ` S)"
proof (rule openI)
  fix a assume "a \ (\x. x $ i) ` S"
  then obtain z where "a = z $ i" and "z \ S" ..
  then obtain A where A: "\i. open (A i) \ z $ i \ A i"
    and S: "\y. (\i. y $ i \ A i) \ y \ S"
    using \<open>open S\<close> unfolding open_vec_def by auto
  hence "A i \ (\x. x $ i) ` S"
    by (clarsimp, rule_tac x="\ j. if j = i then x else z $ j" in image_eqI,
      simp_all)
  hence "open (A i) \ a \ A i \ A i \ (\x. x $ i) ` S"
    using A \<open>a = z $ i\<close> by simp
  then show "\T. open T \ a \ T \ T \ (\x. x $ i) ` S" by - (rule exI)
qed

instance\<^marker>\<open>tag unimportant\<close> vec :: (perfect_space, finite) perfect_space
proof
  fix x :: "'a ^ 'b" show "\ open {x}"
  proof
    assume "open {x}"
    hence "\i. open ((\x. x $ i) ` {x})" by (fast intro: open_image_vec_nth)
    hence "\i. open {x $ i}" by simp
    thus "False" by (simp add: not_open_singleton)
  qed
qed

subsection \<open>Metric space\<close>
(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)

instantiation\<^marker>\<open>tag unimportant\<close> vec :: (metric_space, finite) dist
begin

definition\<^marker>\<open>tag important\<close>
  "dist x y = L2_set (\i. dist (x$i) (y$i)) UNIV"

instance ..
end

instantiation\<^marker>\<open>tag unimportant\<close> vec :: (metric_space, finite) uniformity_dist
begin

definition\<^marker>\<open>tag important\<close> [code del]:
  "(uniformity :: (('a^'b::_) \ ('a^'b::_)) filter) =
    (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"

instance\<^marker>\<open>tag unimportant\<close>
  by standard (rule uniformity_vec_def)
end

declare uniformity_Abort[where 'a="'a :: metric_space ^ 'b :: finite", code]

instantiation\<^marker>\<open>tag unimportant\<close> vec :: (metric_space, finite) metric_space
begin

proposition dist_vec_nth_le: "dist (x $ i) (y $ i) \ dist x y"
  unfolding dist_vec_def by (rule member_le_L2_set) simp_all

instance proof
  fix x y :: "'a ^ 'b"
  show "dist x y = 0 \ x = y"
    unfolding dist_vec_def
    by (simp add: L2_set_eq_0_iff vec_eq_iff)
next
  fix x y z :: "'a ^ 'b"
  show "dist x y \ dist x z + dist y z"
    unfolding dist_vec_def
    apply (rule order_trans [OF _ L2_set_triangle_ineq])
    apply (simp add: L2_set_mono dist_triangle2)
    done
next
  fix S :: "('a ^ 'b) set"
  have *: "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)"
  proof
    assume "open S" show "\x\S. \e>0. \y. dist y x < e \ y \ S"
    proof
      fix x assume "x \ S"
      obtain A where A: "\i. open (A i)" "\i. x $ i \ A i"
        and S: "\y. (\i. y $ i \ A i) \ y \ S"
        using \<open>open S\<close> and \<open>x \<in> S\<close> unfolding open_vec_def by metis
      have "\i\UNIV. \r>0. \y. dist y (x $ i) < r \ y \ A i"
        using A unfolding open_dist by simp
      hence "\r. \i\UNIV. 0 < r i \ (\y. dist y (x $ i) < r i \ y \ A i)"
        by (rule finite_set_choice [OF finite])
      then obtain r where r1: "\i. 0 < r i"
        and r2: "\i y. dist y (x $ i) < r i \ y \ A i" by fast
      have "0 < Min (range r) \ (\y. dist y x < Min (range r) \ y \ S)"
        by (simp add: r1 r2 S le_less_trans [OF dist_vec_nth_le])
      thus "\e>0. \y. dist y x < e \ y \ S" ..
    qed
  next
    assume *: "\x\S. \e>0. \y. dist y x < e \ y \ S" show "open S"
    proof (unfold open_vec_def, rule)
      fix x assume "x \ S"
      then obtain e where "0 < e" and S: "\y. dist y x < e \ y \ S"
        using * by fast
      define r where [abs_def]: "r i = e / sqrt (of_nat CARD('b))" for i :: 'b
      from \<open>0 < e\<close> have r: "\<forall>i. 0 < r i"
        unfolding r_def by simp_all
      from \<open>0 < e\<close> have e: "e = L2_set r UNIV"
        unfolding r_def by (simp add: L2_set_constant)
      define A where "A i = {y. dist (x $ i) y < r i}" for i
      have "\i. open (A i) \ x $ i \ A i"
        unfolding A_def by (simp add: open_ball r)
      moreover have "\y. (\i. y $ i \ A i) \ y \ S"
        by (simp add: A_def S dist_vec_def e L2_set_strict_mono dist_commute)
      ultimately show "\A. (\i. open (A i) \ x $ i \ A i) \
        (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
    qed
  qed
  show "open S = (\x\S. \\<^sub>F (x', y) in uniformity. x' = x \ y \ S)"
    unfolding * eventually_uniformity_metric
    by (simp del: split_paired_All add: dist_vec_def dist_commute)
qed

end

lemma Cauchy_vec_nth:
  "Cauchy (\n. X n) \ Cauchy (\n. X n $ i)"
  unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_vec_nth_le])

lemma vec_CauchyI:
  fixes X :: "nat \ 'a::metric_space ^ 'n"
  assumes X: "\i. Cauchy (\n. X n $ i)"
  shows "Cauchy (\n. X n)"
proof (rule metric_CauchyI)
  fix r :: real assume "0 < r"
  hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp
  define N where "N i = (LEAST N. \m\N. \n\N. dist (X m $ i) (X n $ i) < ?s)" for i
  define M where "M = Max (range N)"
  have "\i. \N. \m\N. \n\N. dist (X m $ i) (X n $ i) < ?s"
    using X \<open>0 < ?s\<close> by (rule metric_CauchyD)
  hence "\i. \m\N i. \n\N i. dist (X m $ i) (X n $ i) < ?s"
    unfolding N_def by (rule LeastI_ex)
  hence M: "\i. \m\M. \n\M. dist (X m $ i) (X n $ i) < ?s"
    unfolding M_def by simp
  {
    fix m n :: nat
    assume "M \ m" "M \ n"
    have "dist (X m) (X n) = L2_set (\i. dist (X m $ i) (X n $ i)) UNIV"
      unfolding dist_vec_def ..
    also have "\ \ sum (\i. dist (X m $ i) (X n $ i)) UNIV"
      by (rule L2_set_le_sum [OF zero_le_dist])
    also have "\ < sum (\i::'n. ?s) UNIV"
      by (rule sum_strict_mono, simp_all add: M \<open>M \<le> m\<close> \<open>M \<le> n\<close>)
    also have "\ = r"
      by simp
    finally have "dist (X m) (X n) < r" .
  }
  hence "\m\M. \n\M. dist (X m) (X n) < r"
    by simp
  then show "\M. \m\M. \n\M. dist (X m) (X n) < r" ..
qed

instance\<^marker>\<open>tag unimportant\<close> vec :: (complete_space, finite) complete_space
proof
  fix X :: "nat \ 'a ^ 'b" assume "Cauchy X"
  have "\i. (\n. X n $ i) \ lim (\n. X n $ i)"
    using Cauchy_vec_nth [OF \<open>Cauchy X\<close>]
    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
  hence "X \ vec_lambda (\i. lim (\n. X n $ i))"
    by (simp add: vec_tendstoI)
  then show "convergent X"
    by (rule convergentI)
qed

subsection \<open>Normed vector space\<close>

instantiation\<^marker>\<open>tag unimportant\<close> vec :: (real_normed_vector, finite) real_normed_vector
begin

definition\<^marker>\<open>tag important\<close> "norm x = L2_set (\<lambda>i. norm (x$i)) UNIV"

definition\<^marker>\<open>tag important\<close> "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"

instance\<^marker>\<open>tag unimportant\<close> proof
  fix a :: real and x y :: "'a ^ 'b"
  show "norm x = 0 \ x = 0"
    unfolding norm_vec_def
    by (simp add: L2_set_eq_0_iff vec_eq_iff)
  show "norm (x + y) \ norm x + norm y"
    unfolding norm_vec_def
    apply (rule order_trans [OF _ L2_set_triangle_ineq])
    apply (simp add: L2_set_mono norm_triangle_ineq)
    done
  show "norm (scaleR a x) = \a\ * norm x"
    unfolding norm_vec_def
    by (simp add: L2_set_right_distrib)
  show "sgn x = scaleR (inverse (norm x)) x"
    by (rule sgn_vec_def)
  show "dist x y = norm (x - y)"
    unfolding dist_vec_def norm_vec_def
    by (simp add: dist_norm)
qed

end

lemma norm_nth_le: "norm (x $ i) \ norm x"
unfolding norm_vec_def
by (rule member_le_L2_set) simp_all

lemma norm_le_componentwise_cart:
  fixes x :: "'a::real_normed_vector^'n"
  assumes "\i. norm(x$i) \ norm(y$i)"
  shows "norm x \ norm y"
  unfolding norm_vec_def
  by (rule L2_set_mono) (auto simp: assms)

lemma component_le_norm_cart: "\x$i\ \ norm x"
  by (metis norm_nth_le real_norm_def)

lemma norm_bound_component_le_cart: "norm x \ e ==> \x$i\ \ e"
  by (metis component_le_norm_cart order_trans)

lemma norm_bound_component_lt_cart: "norm x < e ==> \x$i\ < e"
  by (metis component_le_norm_cart le_less_trans)

lemma norm_le_l1_cart: "norm x \ sum(\i. \x$i\) UNIV"
  by (simp add: norm_vec_def L2_set_le_sum)

lemma bounded_linear_vec_nth[intro]: "bounded_linear (\x. x $ i)"
proof
  show "\K. \x. norm (x $ i) \ norm x * K"
    by (metis mult.commute mult.left_neutral norm_nth_le)
qed auto

instance vec :: (banach, finite) banach ..

subsection \<open>Inner product space\<close>

instantiation\<^marker>\<open>tag unimportant\<close> vec :: (real_inner, finite) real_inner
begin

definition\<^marker>\<open>tag important\<close> "inner x y = sum (\<lambda>i. inner (x$i) (y$i)) UNIV"

instance\<^marker>\<open>tag unimportant\<close> proof
  fix r :: real and x y z :: "'a ^ 'b"
  show "inner x y = inner y x"
    unfolding inner_vec_def
    by (simp add: inner_commute)
  show "inner (x + y) z = inner x z + inner y z"
    unfolding inner_vec_def
    by (simp add: inner_add_left sum.distrib)
  show "inner (scaleR r x) y = r * inner x y"
    unfolding inner_vec_def
    by (simp add: sum_distrib_left)
  show "0 \ inner x x"
    unfolding inner_vec_def
    by (simp add: sum_nonneg)
  show "inner x x = 0 \ x = 0"
    unfolding inner_vec_def
    by (simp add: vec_eq_iff sum_nonneg_eq_0_iff)
  show "norm x = sqrt (inner x x)"
    unfolding inner_vec_def norm_vec_def L2_set_def
    by (simp add: power2_norm_eq_inner)
qed

end

subsection \<open>Euclidean space\<close>

text \<open>Vectors pointing along a single axis.\<close>

definition\<^marker>\<open>tag important\<close> "axis k x = (\<chi> i. if i = k then x else 0)"

lemma axis_nth [simp]: "axis i x $ i = x"
  unfolding axis_def by simp

lemma axis_eq_axis: "axis i x = axis j y \ x = y \ i = j \ x = 0 \ y = 0"
  unfolding axis_def vec_eq_iff by auto

lemma inner_axis_axis:
  "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)"
  by (simp add: inner_vec_def axis_def sum.neutral sum.remove [of _ j])

lemma inner_axis: "inner x (axis i y) = inner (x $ i) y"
  by (simp add: inner_vec_def axis_def sum.remove [where x=i])

lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
  by (simp add: inner_axis inner_commute)

instantiation\<^marker>\<open>tag unimportant\<close> vec :: (euclidean_space, finite) euclidean_space
begin

definition\<^marker>\<open>tag important\<close> "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"

instance\<^marker>\<open>tag unimportant\<close> proof
  show "(Basis :: ('a ^ 'b) set) \ {}"
    unfolding Basis_vec_def by simp
next
  show "finite (Basis :: ('a ^ 'b) set)"
    unfolding Basis_vec_def by simp
next
  fix u v :: "'a ^ 'b"
  assume "u \ Basis" and "v \ Basis"
  thus "inner u v = (if u = v then 1 else 0)"
    unfolding Basis_vec_def
    by (auto simp add: inner_axis_axis axis_eq_axis inner_Basis)
next
  fix x :: "'a ^ 'b"
  show "(\u\Basis. inner x u = 0) \ x = 0"
    unfolding Basis_vec_def
    by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
qed

proposition DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
proof -
  have "card (\i::'b. \u::'a\Basis. {axis i u}) = (\i::'b\UNIV. card (\u::'a\Basis. {axis i u}))"
    by (rule card_UN_disjoint) (auto simp: axis_eq_axis)
  also have "... = CARD('b) * DIM('a)"
    by (subst card_UN_disjoint) (auto simp: axis_eq_axis)
  finally show ?thesis
    by (simp add: Basis_vec_def)
qed

end

lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
  by (simp add: inner_axis' norm_eq_1)

lemma sum_norm_allsubsets_bound_cart:
  fixes f:: "'a \ real ^'n"
  assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (sum f Q) \ e"
  shows "sum (\x. norm (f x)) P \ 2 * real CARD('n) * e"
  using sum_norm_allsubsets_bound[OF assms]
  by simp

lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
  by (simp add: inner_axis)

lemma axis_eq_0_iff [simp]:
  shows "axis m x = 0 \ x = 0"
  by (simp add: axis_def vec_eq_iff)

lemma axis_in_Basis_iff [simp]: "axis i a \ Basis \ a \ Basis"
  by (auto simp: Basis_vec_def axis_eq_axis)

text\<open>Mapping each basis element to the corresponding finite index\<close>
definition axis_index :: "('a::comm_ring_1)^'n \ 'n" where "axis_index v \ SOME i. v = axis i 1"

lemma axis_inverse:
  fixes v :: "real^'n"
  assumes "v \ Basis"
  shows "\i. v = axis i 1"
proof -
  have "v \ (\n. \r\Basis. {axis n r})"
    using assms Basis_vec_def by blast
  then show ?thesis
    by (force simp add: vec_eq_iff)
qed

lemma axis_index:
  fixes v :: "real^'n"
  assumes "v \ Basis"
  shows "v = axis (axis_index v) 1"
  by (metis (mono_tags) assms axis_inverse axis_index_def someI_ex)

lemma axis_index_axis [simp]:
  fixes UU :: "real^'n"
  shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)"
  by (simp add: axis_eq_axis axis_index_def)

subsection\<^marker>\<open>tag unimportant\<close> \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>

lemma sum_cong_aux:
  "(\x. x \ A \ f x = g x) \ sum f A = sum g A"
  by (auto intro: sum.cong)

hide_fact (open) sum_cong_aux

method_setup vector = \<open>
let
  val ss1 =
    simpset_of (put_simpset HOL_basic_ss \<^context>
      |> Simplifier.add_simps [@{thm sum.distrib} RS sym,
          @{thm sum_subtractf} RS sym, @{thm sum_distrib_left},
          @{thm sum_distrib_right}, @{thm sum_negf} RS sym])
  val ss2 =
    simpset_of (\<^context>
      |> Simplifier.add_simps
         [@{thm plus_vec_def}, @{thm times_vec_def},
          @{thm minus_vec_def}, @{thm uminus_vec_def},
          @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def},
          @{thm scaleR_vec_def}, @{thm vector_scalar_mult_def}])
  fun vector_arith_tac ctxt ths =
    simp_tac (put_simpset ss1 ctxt)
    THEN' (fn i => resolve_tac ctxt @{thms Finite_Cartesian_Product.sum_cong_aux} i
         ORELSE resolve_tac ctxt @{thms sum.neutral} i
         ORELSE simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simp @{thm vec_eq_iff}) i)
    (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
    THEN' asm_full_simp_tac (put_simpset ss2 ctxt |> Simplifier.add_simps ths)
in
  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (vector_arith_tac ctxt ths))
end
\<close> "lift trivial vector statements to real arith statements"

lemma vec_0[simp]: "vec 0 = 0" by vector
lemma vec_1[simp]: "vec 1 = 1" by vector

lemma vec_inj[simp]: "vec x = vec y \ x = y" by vector

lemma vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto

lemma vec_add: "vec(x + y) = vec x + vec y"  by vector
lemma vec_sub: "vec(x - y) = vec x - vec y" by vector
lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
lemma vec_neg: "vec(- x) = - vec x " by vector

lemma vec_scaleR: "vec(c * x) = c *\<^sub>R vec x"
  by vector

lemma vec_sum:
  assumes "finite S"
  shows "vec(sum f S) = sum (vec \ f) S"
  using assms
proof induct
  case empty
  then show ?case by simp
next
  case insert
  then show ?case by (auto simp add: vec_add)
qed

text\<open>Obvious "component-pushing".\<close>

lemma vec_component [simp]: "vec x $ i = x"
  by vector

lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
  by vector

lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)"
  by vector

lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector

lemmas\<^marker>\<open>tag unimportant\<close> vector_component =
  vec_component vector_add_component vector_mult_component
  vector_smult_component vector_minus_component vector_uminus_component
  vector_scaleR_component cond_component

subsection\<^marker>\<open>tag unimportant\<close> \<open>Some frequently useful arithmetic lemmas over vectors\<close>

instance vec :: (semigroup_mult, finite) semigroup_mult
  by standard (vector mult.assoc)

instance vec :: (monoid_mult, finite) monoid_mult
  by standard vector+

instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult
  by standard (vector mult.commute)

instance vec :: (comm_monoid_mult, finite) comm_monoid_mult
  by standard vector

instance vec :: (semiring, finite) semiring
  by standard (vector field_simps)+

instance vec :: (semiring_0, finite) semiring_0
  by standard (vector field_simps)+
instance vec :: (semiring_1, finite) semiring_1
  by standard vector
instance vec :: (comm_semiring, finite) comm_semiring
  by standard (vector field_simps)+

instance vec :: (comm_semiring_0, finite) comm_semiring_0 ..
instance vec :: (semiring_0_cancel, finite) semiring_0_cancel ..
instance vec :: (comm_semiring_0_cancel, finite) comm_semiring_0_cancel ..
instance vec :: (ring, finite) ring ..
instance vec :: (semiring_1_cancel, finite) semiring_1_cancel ..
instance vec :: (comm_semiring_1, finite) comm_semiring_1 ..

instance vec :: (ring_1, finite) ring_1 ..

instance vec :: (real_algebra, finite) real_algebra
  by standard (simp_all add: vec_eq_iff)

instance vec :: (real_algebra_1, finite) real_algebra_1 ..

lemma of_nat_index: "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"
proof (induct n)
  case 0
  then show ?case by vector
next
  case Suc
  then show ?case by vector
qed

lemma one_index [simp]: "(1 :: 'a :: one ^ 'n) $ i = 1"
  by vector

lemma neg_one_index [simp]: "(- 1 :: 'a :: {one, uminus} ^ 'n) $ i = - 1"
  by vector

instance vec :: (semiring_char_0, finite) semiring_char_0
proof
  fix m n :: nat
  show "inj (of_nat :: nat \ 'a ^ 'b)"
    by (auto intro!: injI simp add: vec_eq_iff of_nat_index)
qed

instance vec :: (numeral, finite) numeral ..
instance vec :: (semiring_numeral, finite) semiring_numeral ..

lemma numeral_index [simp]: "numeral w $ i = numeral w"
  by (induct w) (simp_all only: numeral.simps vector_add_component one_index)

lemma neg_numeral_index [simp]: "- numeral w $ i = - numeral w"
  by (simp only: vector_uminus_component numeral_index)

instance vec :: (comm_ring_1, finite) comm_ring_1 ..
instance vec :: (ring_char_0, finite) ring_char_0 ..

lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
  by (vector mult.assoc)
lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x"
  by (vector field_simps)
lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y"
  by (vector field_simps)
lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector
lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector
lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y"
  by (vector field_simps)
lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector
lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector
lemma vector_sneg_minus1: "-x = (-1::'a::ring_1) *s x" by vector
lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector
lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"
  by (vector field_simps)

lemma vec_eq[simp]: "(vec m = vec n) \ (m = n)"
  by (simp add: vec_eq_iff)

lemma Vector_Spaces_linear_vec [simp]: "Vector_Spaces.linear (*) vector_scalar_mult vec"
  by unfold_locales (vector algebra_simps)+

lemma vector_mul_eq_0[simp]: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0"
  by vector

lemma vector_mul_lcancel[simp]: "a *s x = a *s y \ a = (0::'a::field) \ x = y"
  by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)

lemma vector_mul_rcancel[simp]: "a *s x = b *s x \ (a::'a::field) = b \ x = 0"
  by (subst eq_iff_diff_eq_0, subst vector_sub_rdistrib [symmetric]) simp

lemma scalar_mult_eq_scaleR [abs_def]: "c *s x = c *\<^sub>R x"
  unfolding scaleR_vec_def vector_scalar_mult_def by simp

lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \c\ * dist x y"
  unfolding dist_norm scalar_mult_eq_scaleR
  unfolding scaleR_right_diff_distrib[symmetric] by simp

lemma sum_component [simp]:
  fixes f:: " 'a \ ('b::comm_monoid_add) ^'n"
  shows "(sum f S)$i = sum (\x. (f x)$i) S"
proof (cases "finite S")
  case True
  then show ?thesis by induct simp_all
next
  case False
  then show ?thesis by simp
qed

lemma sum_eq: "sum f S = (\ i. sum (\x. (f x)$i ) S)"
  by (simp add: vec_eq_iff)

lemma sum_cmul:
  fixes f:: "'c \ ('a::semiring_1)^'n"
  shows "sum (\x. c *s f x) S = c *s sum f S"
  by (simp add: vec_eq_iff sum_distrib_left)

lemma linear_vec [simp]: "linear vec"
  using Vector_Spaces_linear_vec
  by unfold_locales (vector algebra_simps)+

subsection \<open>Matrix operations\<close>

text\<open>Matrix notation. NB: an MxN matrix is of type \<^typ>\<open>'a^'n^'m\<close>, not \<^typ>\<open>'a^'m^'n\<close>\<close>

definition\<^marker>\<open>tag important\<close> map_matrix::"('a \<Rightarrow> 'b) \<Rightarrow> (('a, 'i::finite)vec, 'j::finite) vec \<Rightarrow> (('b, 'i)vec, 'j) vec" where
  "map_matrix f x = (\ i j. f (x $ i $ j))"

lemma nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)"
  by (simp add: map_matrix_def)

definition\<^marker>\<open>tag important\<close> matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
    (infixl \<open>**\<close> 70)
  where "m ** m' == (\ i j. sum (\k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"

definition\<^marker>\<open>tag important\<close> matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"
    (infixl \<open>*v\<close> 70)
  where "m *v x \ (\ i. sum (\j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"

definition\<^marker>\<open>tag important\<close> vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "
    (infixl \<open>v*\<close> 70)
  where "v v* m == (\ j. sum (\i. ((v$i) * (m$i)$j)) (UNIV :: 'm set)) :: 'a^'n"

definition\<^marker>\<open>tag unimportant\<close> "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
definition\<^marker>\<open>tag unimportant\<close> transpose where
  "(transpose::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A$j)$i))"
definition\<^marker>\<open>tag unimportant\<close> "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
definition\<^marker>\<open>tag unimportant\<close> "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
definition\<^marker>\<open>tag unimportant\<close> "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
definition\<^marker>\<open>tag unimportant\<close> "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"

lemma times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0"
  by (simp add: matrix_matrix_mult_def zero_vec_def)

lemma times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0"
  by (simp add: matrix_matrix_mult_def zero_vec_def)

lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
  by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)

lemma matrix_mul_lid [simp]:
  fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
  shows "mat 1 ** A = A"
  unfolding matrix_matrix_mult_def mat_def
  by (auto simp: if_distrib if_distribR sum.delta'[OF finite] cong: if_cong)

lemma matrix_mul_rid [simp]:
  fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
  shows "A ** mat 1 = A"
  unfolding matrix_matrix_mult_def mat_def
  by (auto simp: if_distrib if_distribR sum.delta'[OF finite] cong: if_cong)

lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
  apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
  using sum.swap by fastforce

lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
  apply (vector matrix_matrix_mult_def matrix_vector_mult_def
    sum_distrib_left sum_distrib_right mult.assoc)
  using sum.swap by fastforce

lemma vector_matrix_mul_assoc: "(x v* A) v* B = x v* (A**B)"
  apply (vector matrix_matrix_mult_def vector_matrix_mult_def
    sum_distrib_left sum_distrib_right mult.assoc)
  using sum.swap by fastforce

lemma scalar_matrix_assoc:
  fixes A :: "('a::real_algebra_1)^'m^'n"
  shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B"
  by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right)

lemma matrix_scalar_ac:
  fixes A :: "('a::real_algebra_1)^'m^'n"
  shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B"
  by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)

lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
  apply (vector matrix_vector_mult_def mat_def)
  apply (simp add: if_distrib if_distribR cong del: if_weak_cong)
  done

lemma vector_matrix_mul_rid [simp]:
  fixes v :: "('a::semiring_1)^'n"
  shows "v v* mat 1 = v"
  apply (vector vector_matrix_mult_def mat_def)
  apply (simp add: if_distrib if_distribR cong del: if_weak_cong)
  done

lemma matrix_transpose_mul:
    "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
  by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute)

lemma matrix_mult_transpose_dot_column:
  shows "transpose A ** A = (\ i j. inner (column i A) (column j A))"
  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)

lemma matrix_mult_transpose_dot_row:
  shows "A ** transpose A = (\ i j. inner (row i A) (row j A))"
  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)

lemma matrix_eq:
  fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
  shows "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs")
proof
  assume ?rhs
  then show ?lhs
    apply (subst vec_eq_iff)
    apply (clarsimp simp add: matrix_vector_mult_def if_distrib if_distribR vec_eq_iff cong: if_cong)
    apply (erule_tac x="axis ia 1" in allE)
    apply (erule_tac x="i" in allE)
    apply (auto simp add: if_distrib if_distribR axis_def
        sum.delta[OF finite] cong del: if_weak_cong)
    done
qed auto

lemma matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x"
  by (simp add: matrix_vector_mult_def inner_vec_def)

lemma dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)"
  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
  apply (subst sum.swap)
  apply simp
  done

lemma transpose_mat [simp]: "transpose (mat n) = mat n"
  by (vector transpose_def mat_def)

lemma transpose_transpose [simp]: "transpose(transpose A) = A"
  by (vector transpose_def)

lemma row_transpose [simp]: "row i (transpose A) = column i A"
  by (simp add: row_def column_def transpose_def vec_eq_iff)

lemma column_transpose [simp]: "column i (transpose A) = row i A"
  by (simp add: row_def column_def transpose_def vec_eq_iff)

lemma rows_transpose [simp]: "rows(transpose A) = columns A"
  by (auto simp add: rows_def columns_def intro: set_eqI)

lemma columns_transpose [simp]: "columns(transpose A) = rows A"
  by (metis transpose_transpose rows_transpose)

lemma transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A"
  unfolding transpose_def
  by (simp add: vec_eq_iff)

lemma transpose_iff [iff]: "transpose A = transpose B \ A = B"
  by (metis transpose_transpose)

lemma matrix_mult_sum:
  "(A::'a::comm_semiring_1^'n^'m) *v x = sum (\i. (x$i) *s column i A) (UNIV:: 'n set)"
  by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute)

lemma vector_componentwise:
  "(x::'a::ring_1^'n) = (\ j. \i\UNIV. (x$i) * (axis i 1 :: 'a^'n) $ j)"
  by (simp add: axis_def if_distrib sum.If_cases vec_eq_iff)

lemma basis_expansion: "sum (\i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)"
  by (auto simp add: axis_def vec_eq_iff if_distrib sum.If_cases cong del: if_weak_cong)

text\<open>Correspondence between matrices and linear operators.\<close>

definition\<^marker>\<open>tag important\<close> matrix :: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
  where "matrix f = (\ i j. (f(axis j 1))$i)"

lemma matrix_id_mat_1: "matrix id = mat 1"
  by (simp add: mat_def matrix_def axis_def)

lemma matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r"
  by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)

lemma matrix_vector_mul_linear[intro, simp]: "linear (\x. A *v (x::'a::real_algebra_1 ^ _))"
  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left
      sum.distrib scaleR_right.sum)

lemma vector_matrix_left_distrib [algebra_simps]:
  shows "(x + y) v* A = x v* A + y v* A"
  unfolding vector_matrix_mult_def
  by (simp add: algebra_simps sum.distrib vec_eq_iff)

lemma vector_matrix_mult_diff_distrib [algebra_simps]:
  fixes A :: "'a::ring_1^'n^'m"
  shows "(x - y) v* A = x v* A - y v* A"
  by (vector vector_matrix_mult_def sum_subtractf left_diff_distrib)

lemma matrix_vector_right_distrib [algebra_simps]:
  "A *v (x + y) = A *v x + A *v y"
  by (vector matrix_vector_mult_def sum.distrib distrib_left)

lemma matrix_vector_mult_diff_distrib [algebra_simps]:
  fixes A :: "'a::ring_1^'n^'m"
  shows "A *v (x - y) = A *v x - A *v y"
  by (vector matrix_vector_mult_def sum_subtractf right_diff_distrib)

lemma matrix_vector_mult_scaleR[algebra_simps]:
  fixes A :: "real^'n^'m"
  shows "A *v (c *\<^sub>R x) = c *\<^sub>R (A *v x)"
  using linear_iff matrix_vector_mul_linear by blast

lemma matrix_vector_mult_0_right [simp]: "A *v 0 = 0"
  by (simp add: matrix_vector_mult_def vec_eq_iff)

lemma matrix_vector_mult_0 [simp]: "0 *v w = 0"
  by (simp add: matrix_vector_mult_def vec_eq_iff)

lemma matrix_vector_mult_add_rdistrib [algebra_simps]:
  "(A + B) *v x = (A *v x) + (B *v x)"
  by (vector matrix_vector_mult_def sum.distrib distrib_right)

lemma matrix_vector_mult_diff_rdistrib [algebra_simps]:
  fixes A :: "'a :: ring_1^'n^'m"
  shows "(A - B) *v x = (A *v x) - (B *v x)"
  by (vector matrix_vector_mult_def sum_subtractf left_diff_distrib)

lemma vector_matrix_mult_add_rdistrib [algebra_simps]:
  "x v* (A + B) = (x v* A) + (x v* B)"
  by (vector vector_matrix_mult_def sum.distrib distrib_left)

lemma  vector_matrix_mult_diff_rdistrib [algebra_simps]:
  fixes A :: "'a :: ring_1^'n^'m"
  shows "x v* (A - B) = (x v* A) - (x v* B)"
  by (vector vector_matrix_mult_def sum_subtractf right_diff_distrib)

lemma matrix_vector_column:
  "(A::'a::comm_semiring_1^'n^_) *v x = sum (\i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
  by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute)

subsection\<open>Inverse matrices  (not necessarily square)\<close>

definition\<^marker>\<open>tag important\<close>
  "invertible(A::'a::semiring_1^'n^'m) \ (\A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)"

definition\<^marker>\<open>tag important\<close>
  "matrix_inv(A:: 'a::semiring_1^'n^'m) =
    (SOME A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)"

lemma inj_matrix_vector_mult:
  fixes A::"'a::field^'n^'m"
  assumes "invertible A"
  shows "inj ((*v) A)"
  by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)

lemma scalar_invertible:
  fixes A :: "('a::real_algebra_1)^'m^'n"
  assumes "k \ 0" and "invertible A"
  shows "invertible (k *\<^sub>R A)"
proof -
  obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
    using assms unfolding invertible_def by auto
  with \<open>k \<noteq> 0\<close>
  have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
    by (simp_all add: assms matrix_scalar_ac)
  thus "invertible (k *\<^sub>R A)"
    unfolding invertible_def by auto
qed

lemma scalar_invertible_iff:
  fixes A :: "('a::real_algebra_1)^'m^'n"
  assumes "k \ 0" and "invertible A"
  shows "invertible (k *\<^sub>R A) \ k \ 0 \ invertible A"
  by (simp add: assms scalar_invertible)

lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v (x:: 'a::{comm_semiring_1}^'n)"
  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
  by (simp add: mult.commute)

lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* (A:: 'a::{comm_semiring_1}^'m^'n)"
  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
  by (simp add: mult.commute)

lemma vector_scalar_commute:
  fixes A :: "'a::{field}^'m^'n"
  shows "A *v (c *s x) = c *s (A *v x)"
  by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left)

lemma scalar_vector_matrix_assoc:
  fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
  shows "(k *s x) v* A = k *s (x v* A)"
  by (metis transpose_matrix_vector vector_scalar_commute)

lemma vector_matrix_mult_0 [simp]: "0 v* A = 0"
  unfolding vector_matrix_mult_def by (simp add: zero_vec_def)

lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
  unfolding vector_matrix_mult_def by (simp add: zero_vec_def)

lemma scaleR_vector_matrix_assoc:
  fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
  shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
  by (metis matrix_vector_mult_scaleR transpose_matrix_vector)

lemma vector_scaleR_matrix_ac:
  fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
  shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
proof -
  have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
    by (simp add: vector_matrix_mult_def algebra_simps)
  with scaleR_vector_matrix_assoc
  show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
    by auto
qed

end

quality95%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.