header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}

theory Cartesian_Euclidean_Space

imports Finite_Cartesian_Product Integration

begin

lemma delta_mult_idempotent:

  "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto)

lemma setsum_Plus:

  "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow>

    (\<Sum>x\<in>A <+> B. g x) = (\<Sum>x\<in>A. g (Inl x)) + (\<Sum>x\<in>B. g (Inr x))"

  unfolding Plus_def

  by (subst setsum_Un_disjoint, auto simp add: setsum_reindex)

lemma setsum_UNIV_sum:

  fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"

  shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"

  apply (subst UNIV_Plus_UNIV [symmetric])

  apply (rule setsum_Plus [OF finite finite])

  done

lemma setsum_mult_product:

  "setsum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"

  unfolding sumr_group[of h B A, unfolded atLeast0LessThan, symmetric]

proof (rule setsum_cong, simp, rule setsum_reindex_cong)

  fix i show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI)

  show "{i * B..<i * B + B} = (\<lambda>j. j + i * B) ` {..<B}"

  proof safe

    fix j assume "j \<in> {i * B..<i * B + B}"

    thus "j \<in> (\<lambda>j. j + i * B) ` {..<B}"

      by (auto intro!: image_eqI[of _ _ "j - i * B"])

  qed simp

qed simp

subsection{* Basic componentwise operations on vectors. *}

instantiation cart :: (times,finite) times

begin

  definition vector_mult_def : "op * \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"

  instance ..

end

instantiation cart :: (one,finite) one

begin

  definition vector_one_def : "1 \<equiv> (\<chi> i. 1)"

  instance ..

end

instantiation cart :: (ord,finite) ord

begin

  definition vector_le_def:

    "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"

  definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"

  instance by (intro_classes)

end

text{* The ordering on one-dimensional vectors is linear. *}

class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"

begin

  subclass finite

  proof from UNIV_one show "finite (UNIV :: 'a set)"

      by (auto intro!: card_ge_0_finite) qed

end

instantiation cart :: (linorder,cart_one) linorder begin

instance proof

  guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+

  hence *:"UNIV = {a}" by auto

  have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P a" unfolding * by auto hence all:"\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a" by auto

  fix x y z::"'a^'b::cart_one" note * = vector_le_def vector_less_def all Cart_eq

  show "x\<le>x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x\<le>y \<or> y\<le>x" unfolding * by(auto simp only:field_simps)

  { assume "x\<le>y" "y\<le>z" thus "x\<le>z" unfolding * by(auto simp only:field_simps) }

  { assume "x\<le>y" "y\<le>x" thus "x=y" unfolding * by(auto simp only:field_simps) }

qed end

text{* Constant Vectors *} 

definition "vec x = (\<chi> i. x)"

text{* Also the scalar-vector multiplication. *}

definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)

  where "c *s x = (\<chi> i. c * (x$i))"

subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}

method_setup vector = {*

let

  val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym,

  @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},

  @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]

  val ss2 = @{simpset} addsimps

             [@{thm vector_add_def}, @{thm vector_mult_def},

              @{thm vector_minus_def}, @{thm vector_uminus_def},

              @{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},

              @{thm vector_scaleR_def},

              @{thm Cart_lambda_beta}, @{thm vector_scalar_mult_def}]

 fun vector_arith_tac ths =

   simp_tac ss1

   THEN' (fn i => rtac @{thm setsum_cong2} i

         ORELSE rtac @{thm setsum_0'} i

         ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i)

   (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)

   THEN' asm_full_simp_tac (ss2 addsimps ths)

 in

  Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))

 end

*} "lift trivial vector statements to real arith statements"

lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)

lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def)

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

lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto

lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)

lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)

lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)

lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)

lemma vec_setsum: assumes fS: "finite S"

  shows "vec(setsum f S) = setsum (vec o f) S"

  apply (induct rule: finite_induct[OF fS])

  apply (simp)

  apply (auto simp add: vec_add)

  done

text{* Obvious "component-pushing". *}

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

  by (vector vec_def)

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 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 {* Some frequently useful arithmetic lemmas over vectors. *}

instance cart :: (semigroup_mult,finite) semigroup_mult

  apply (intro_classes) by (vector mult_assoc)

instance cart :: (monoid_mult,finite) monoid_mult

  apply (intro_classes) by vector+

instance cart :: (ab_semigroup_mult,finite) ab_semigroup_mult

  apply (intro_classes) by (vector mult_commute)

instance cart :: (ab_semigroup_idem_mult,finite) ab_semigroup_idem_mult

  apply (intro_classes) by (vector mult_idem)

instance cart :: (comm_monoid_mult,finite) comm_monoid_mult

  apply (intro_classes) by vector

instance cart :: (semiring,finite) semiring

  apply (intro_classes) by (vector field_simps)+

instance cart :: (semiring_0,finite) semiring_0

  apply (intro_classes) by (vector field_simps)+

instance cart :: (semiring_1,finite) semiring_1

  apply (intro_classes) by vector

instance cart :: (comm_semiring,finite) comm_semiring

  apply (intro_classes) by (vector field_simps)+

instance cart :: (comm_semiring_0,finite) comm_semiring_0 by (intro_classes)

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

instance cart :: (semiring_0_cancel,finite) semiring_0_cancel by (intro_classes)

instance cart :: (comm_semiring_0_cancel,finite) comm_semiring_0_cancel by (intro_classes)

instance cart :: (ring,finite) ring by (intro_classes)

instance cart :: (semiring_1_cancel,finite) semiring_1_cancel by (intro_classes)

instance cart :: (comm_semiring_1,finite) comm_semiring_1 by (intro_classes)

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

instance cart :: (real_algebra,finite) real_algebra

  apply intro_classes

  apply (simp_all add: vector_scaleR_def field_simps)

  apply vector

  apply vector

  done

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

lemma of_nat_index:

  "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"

  apply (induct n)

  apply vector

  apply vector

  done

lemma one_index[simp]:

  "(1 :: 'a::one ^'n)$i = 1" by vector

instance cart :: (semiring_char_0, finite) semiring_char_0

proof

  fix m n :: nat

  show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"

    by (auto intro!: injI simp add: Cart_eq of_nat_index)

qed

instance cart :: (comm_ring_1,finite) comm_ring_1 ..

instance cart :: (ring_char_0,finite) ring_char_0 ..

instance cart :: (real_vector,finite) real_vector ..

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) \<longleftrightarrow> (m = n)"

  by (simp add: Cart_eq)

lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)

lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"

  by vector

lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> 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 \<longleftrightarrow> (a::real) = b \<or> x = 0"

  by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)

lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"

  by (metis vector_mul_lcancel)

lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"

  by (metis vector_mul_rcancel)

lemma component_le_norm_cart: "\<bar>x$i\<bar> <= norm x"

  apply (simp add: norm_vector_def)

  apply (rule member_le_setL2, simp_all)

  done

lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x$i\<bar> <= e"

  by (metis component_le_norm_cart order_trans)

lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"

  by (metis component_le_norm_cart basic_trans_rules(21))

lemma norm_le_l1_cart: "norm x <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV"

  by (simp add: norm_vector_def setL2_le_setsum)

lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x"

  unfolding vector_scaleR_def vector_scalar_mult_def by simp

lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"

  unfolding dist_norm scalar_mult_eq_scaleR

  unfolding scaleR_right_diff_distrib[symmetric] by simp

lemma setsum_component [simp]:

  fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"

  shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S"

  by (cases "finite S", induct S set: finite, simp_all)

lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)"

  by (simp add: Cart_eq)

lemma setsum_cmul:

  fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"

  shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"

  by (simp add: Cart_eq setsum_right_distrib)

(* TODO: use setsum_norm_allsubsets_bound *)

lemma setsum_norm_allsubsets_bound_cart:

  fixes f:: "'a \<Rightarrow> real ^'n"

  assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"

  shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"

proof-

  let ?d = "real CARD('n)"

  let ?nf = "\<lambda>x. norm (f x)"

  let ?U = "UNIV :: 'n set"

  have th0: "setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $ i\<bar>) ?U) P = setsum (\<lambda>i. setsum (\<lambda>x. \<bar>f x $ i\<bar>) P) ?U"

    by (rule setsum_commute)

  have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def)

  have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $ i\<bar>) ?U) P"

    apply (rule setsum_mono)    by (rule norm_le_l1_cart)

  also have "\<dots> \<le> 2 * ?d * e"

    unfolding th0 th1

  proof(rule setsum_bounded)

    fix i assume i: "i \<in> ?U"

    let ?Pp = "{x. x\<in> P \<and> f x $ i \<ge> 0}"

    let ?Pn = "{x. x \<in> P \<and> f x $ i < 0}"

    have thp: "P = ?Pp \<union> ?Pn" by auto

    have thp0: "?Pp \<inter> ?Pn ={}" by auto

    have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+

    have Ppe:"setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp \<le> e"

      using component_le_norm_cart[of "setsum (\<lambda>x. f x) ?Pp" i]  fPs[OF PpP]

      by (auto intro: abs_le_D1)

    have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e"

      using component_le_norm_cart[of "setsum (\<lambda>x. - f x) ?Pn" i]  fPs[OF PnP]

      by (auto simp add: setsum_negf intro: abs_le_D1)

    have "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn"

      apply (subst thp)

      apply (rule setsum_Un_zero)

      using fP thp0 by auto

    also have "\<dots> \<le> 2*e" using Pne Ppe by arith

    finally show "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P \<le> 2*e" .

  qed

  finally show ?thesis .

qed

subsection {* A bijection between 'n::finite and {..<CARD('n)} *}

definition cart_bij_nat :: "nat \<Rightarrow> ('n::finite)" where

  "cart_bij_nat = (SOME p. bij_betw p {..<CARD('n)} (UNIV::'n set) )"

abbreviation "\<pi> \<equiv> cart_bij_nat"

definition "\<pi>' = inv_into {..<CARD('n)} (\<pi>::nat \<Rightarrow> ('n::finite))"

lemma bij_betw_pi:

  "bij_betw \<pi> {..<CARD('n::finite)} (UNIV::('n::finite) set)"

  using ex_bij_betw_nat_finite[of "UNIV::'n set"]

  by (auto simp: cart_bij_nat_def atLeast0LessThan

    intro!: someI_ex[of "\<lambda>x. bij_betw x {..<CARD('n)} (UNIV::'n set)"])

lemma bij_betw_pi'[intro]: "bij_betw \<pi>' (UNIV::'n set) {..<CARD('n::finite)}"

  using bij_betw_inv_into[OF bij_betw_pi] unfolding \<pi>'_def by auto

lemma pi'_inj[intro]: "inj \<pi>'"

  using bij_betw_pi' unfolding bij_betw_def by auto

lemma pi'_range[intro]: "\<And>i::'n. \<pi>' i < CARD('n::finite)"

  using bij_betw_pi' unfolding bij_betw_def by auto

lemma \<pi>\<pi>'[simp]: "\<And>i::'n::finite. \<pi> (\<pi>' i) = i"

  using bij_betw_pi by (auto intro!: f_inv_into_f simp: \<pi>'_def bij_betw_def)

lemma \<pi>'\<pi>[simp]: "\<And>i. i\<in>{..<CARD('n::finite)} \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"

  using bij_betw_pi by (auto intro!: inv_into_f_eq simp: \<pi>'_def bij_betw_def)

lemma \<pi>\<pi>'_alt[simp]: "\<And>i. i<CARD('n::finite) \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"

  by auto

lemma \<pi>_inj_on: "inj_on (\<pi>::nat\<Rightarrow>'n::finite) {..<CARD('n)}"

  using bij_betw_pi[where 'n='n] by (simp add: bij_betw_def)

instantiation cart :: (real_basis,finite) real_basis

begin

definition "(basis i::'a^'b) =

  (if i < (CARD('b) * DIM('a))

  then (\<chi> j::'b. if j = \<pi>(i div DIM('a)) then basis (i mod DIM('a)) else 0)

  else 0)"

lemma basis_eq:

  assumes "i < CARD('b)" and "j < DIM('a)"

  shows "basis (j + i * DIM('a)) = (\<chi> k. if k = \<pi> i then basis j else 0)"

proof -

  have "j + i * DIM('a) <  DIM('a) * (i + 1)" using assms by (auto simp: field_simps)

  also have "\<dots> \<le> DIM('a) * CARD('b)" using assms unfolding mult_le_cancel1 by auto

  finally show ?thesis

    unfolding basis_cart_def using assms by (auto simp: Cart_eq not_less field_simps)

qed

lemma basis_eq_pi':

  assumes "j < DIM('a)"

  shows "basis (j + \<pi>' i * DIM('a)) $ k = (if k = i then basis j else 0)"

  apply (subst basis_eq)

  using pi'_range assms by simp_all

lemma split_times_into_modulo[consumes 1]:

  fixes k :: nat

  assumes "k < A * B"

  obtains i j where "i < A" and "j < B" and "k = j + i * B"

proof

  have "A * B \<noteq> 0"

  proof assume "A * B = 0" with assms show False by simp qed

  hence "0 < B" by auto

  thus "k mod B < B" using `0 < B` by auto

next

  have "k div B * B \<le> k div B * B + k mod B" by (rule le_add1)

  also have "... < A * B" using assms by simp

  finally show "k div B < A" by auto

qed simp

lemma split_CARD_DIM[consumes 1]:

  fixes k :: nat

  assumes k: "k < CARD('b) * DIM('a)"

  obtains i and j::'b where "i < DIM('a)" "k = i + \<pi>' j * DIM('a)"

proof -

  from split_times_into_modulo[OF k] guess i j . note ij = this

  show thesis

  proof

    show "j < DIM('a)" using ij by simp

    show "k = j + \<pi>' (\<pi> i :: 'b) * DIM('a)"

      using ij by simp

  qed

qed

lemma linear_less_than_times:

  fixes i j A B :: nat assumes "i < B" "j < A"

  shows "j + i * A < B * A"

proof -

  have "i * A + j < (Suc i)*A" using `j < A` by simp

  also have "\<dots> \<le> B * A" using `i < B` unfolding mult_le_cancel2 by simp

  finally show ?thesis by simp

qed

instance

proof

  let ?b = "basis :: nat \<Rightarrow> 'a^'b"

  let ?b' = "basis :: nat \<Rightarrow> 'a"

  have setsum_basis:

    "\<And>f. (\<Sum>x\<in>range basis. f (x::'a)) = f 0 + (\<Sum>i<DIM('a). f (basis i))"

    unfolding range_basis apply (subst setsum.insert)

    by (auto simp: basis_eq_0_iff setsum.insert setsum_reindex[OF basis_inj])

  have inj: "inj_on ?b {..<CARD('b)*DIM('a)}"

    by (auto intro!: inj_onI elim!: split_CARD_DIM split: split_if_asm

             simp add: Cart_eq basis_eq_pi' all_conj_distrib basis_neq_0

                       inj_on_iff[OF basis_inj])

  moreover

  hence indep: "independent (?b ` {..<CARD('b) * DIM('a)})"

  proof (rule independent_eq_inj_on[THEN iffD2], safe elim!: split_CARD_DIM del: notI)

    fix j and i :: 'b and u :: "'a^'b \<Rightarrow> real" assume "j < DIM('a)"

    let ?x = "j + \<pi>' i * DIM('a)"

    show "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) \<noteq> ?b ?x"

      unfolding Cart_eq not_all

    proof

      have "(\<lambda>j. j + \<pi>' i*DIM('a))`({..<DIM('a)}-{j}) =

        {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)} - {?x}"(is "?S = ?I - _")

      proof safe

        fix y assume "y \<in> ?I"

        moreover def k \<equiv> "y - \<pi>' i*DIM('a)"

        ultimately have "k < DIM('a)" and "y = k + \<pi>' i * DIM('a)" by auto

        moreover assume "y \<notin> ?S"

        ultimately show "y = j + \<pi>' i * DIM('a)" by auto

      qed auto

      have "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) $ i =

          (\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k $ i)" by simp

      also have "\<dots> = (\<Sum>k\<in>?S. u(?b k) *\<^sub>R ?b k $ i)"

        unfolding `?S = ?I - {?x}`

      proof (safe intro!: setsum_mono_zero_cong_right)

        fix y assume "y \<in> {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)}"

        moreover have "Suc (\<pi>' i) * DIM('a) \<le> CARD('b) * DIM('a)"

          unfolding mult_le_cancel2 using pi'_range[of i] by simp

        ultimately show "y < CARD('b) * DIM('a)" by simp

      next

        fix y assume "y < CARD('b) * DIM('a)"

        with split_CARD_DIM guess l k . note y = this

        moreover assume "u (?b y) *\<^sub>R ?b y $ i \<noteq> 0"

        ultimately show "y \<in> {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)}"

          by (auto simp: basis_eq_pi' split: split_if_asm)

      qed simp

      also have "\<dots> = (\<Sum>k\<in>{..<DIM('a)} - {j}. u (?b (k + \<pi>' i*DIM('a))) *\<^sub>R (?b' k))"

        by (subst setsum_reindex) (auto simp: basis_eq_pi' intro!: inj_onI)

      also have "\<dots> \<noteq> ?b ?x $ i"

      proof -

        note independent_eq_inj_on[THEN iffD1, OF basis_inj independent_basis, rule_format]

        note this[of j "\<lambda>v. u (\<chi> ka::'b. if ka = i then v else (0\<Colon>'a))"]

        thus ?thesis by (simp add: `j < DIM('a)` basis_eq pi'_range)

      qed

      finally show "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) $ i \<noteq> ?b ?x $ i" .

    qed

  qed

  ultimately

  show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"

    by (auto intro!: exI[of _ "CARD('b) * DIM('a)"] simp: basis_cart_def)

  from indep have exclude_0: "0 \<notin> ?b ` {..<CARD('b) * DIM('a)}"

    using dependent_0[of "?b ` {..<CARD('b) * DIM('a)}"] by blast

  show "span (range ?b) = UNIV"

  proof -

    { fix x :: "'a^'b"

      let "?if i y" = "(\<chi> k::'b. if k = i then ?b' y else (0\<Colon>'a))"

      have The_if: "\<And>i j. j < DIM('a) \<Longrightarrow> (THE k. (?if i j) $ k \<noteq> 0) = i"

        by (rule the_equality) (simp_all split: split_if_asm add: basis_neq_0)

      { fix x :: 'a

        have "x \<in> span (range basis)"

          using span_basis by (auto simp: range_basis)

        hence "\<exists>u. (\<Sum>x<DIM('a). u (?b' x) *\<^sub>R ?b' x) = x"

          by (subst (asm) span_finite) (auto simp: setsum_basis) }

      hence "\<forall>i. \<exists>u. (\<Sum>x<DIM('a). u (?b' x) *\<^sub>R ?b' x) = i" by auto

      then obtain u where u: "\<forall>i. (\<Sum>x<DIM('a). u i (?b' x) *\<^sub>R ?b' x) = i"

        by (auto dest: choice)

      have "\<exists>u. \<forall>i. (\<Sum>j<DIM('a). u (?if i j) *\<^sub>R ?b' j) = x $ i"

        apply (rule exI[of _ "\<lambda>v. let i = (THE i. v$i \<noteq> 0) in u (x$i) (v$i)"])

        using The_if u by simp }

    moreover

    have "\<And>i::'b. {..<CARD('b)} \<inter> {x. i = \<pi> x} = {\<pi>' i}"

      using pi'_range[where 'n='b] by auto

    moreover

    have "range ?b = {0} \<union> ?b ` {..<CARD('b) * DIM('a)}"

      by (auto simp: image_def basis_cart_def)

    ultimately

    show ?thesis

      by (auto simp add: Cart_eq setsum_reindex[OF inj] range_basis

          setsum_mult_product basis_eq if_distrib setsum_cases span_finite

          setsum_reindex[OF basis_inj])

  qed

qed

end

lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a::real_basis)"

proof (safe intro!: dimension_eq elim!: split_times_into_modulo del: notI)

  fix i j assume *: "i < CARD('b)" "j < DIM('a)"

  hence A: "(i * DIM('a) + j) div DIM('a) = i"

    by (subst div_add1_eq) simp

  from * have B: "(i * DIM('a) + j) mod DIM('a) = j"

    unfolding mod_mult_self3 by simp

  show "basis (j + i * DIM('a)) \<noteq> (0::'a^'b)" unfolding basis_cart_def

    using * basis_finite[where 'a='a]

      linear_less_than_times[of i "CARD('b)" j "DIM('a)"]

    by (auto simp: A B field_simps Cart_eq basis_eq_0_iff)

qed (auto simp: basis_cart_def)

lemma if_distr: "(if P then f else g) $ i = (if P then f $ i else g $ i)" by simp

lemma split_dimensions'[consumes 1]:

  assumes "k < DIM('a::real_basis^'b)"

  obtains i j where "i < CARD('b::finite)" and "j < DIM('a::real_basis)" and "k = j + i * DIM('a::real_basis)"

using split_times_into_modulo[OF assms[simplified]] .

lemma cart_euclidean_bound[intro]:

  assumes j:"j < DIM('a::{real_basis})"

  shows "j + \<pi>' (i::'b::finite) * DIM('a) < CARD('b) * DIM('a::real_basis)"

  using linear_less_than_times[OF pi'_range j, of i] .

instance cart :: (real_basis_with_inner,finite) real_basis_with_inner ..

lemma (in real_basis) forall_CARD_DIM:

  "(\<forall>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<forall>(i::'b::finite) j. j<DIM('a) \<longrightarrow> P (j + \<pi>' i * DIM('a)))"

   (is "?l \<longleftrightarrow> ?r")

proof (safe elim!: split_times_into_modulo)

  fix i :: 'b and j assume "j < DIM('a)"

  note linear_less_than_times[OF pi'_range[of i] this]

  moreover assume "?l"

  ultimately show "P (j + \<pi>' i * DIM('a))" by auto

next

  fix i j assume "i < CARD('b)" "j < DIM('a)" and "?r"

  from `?r`[rule_format, OF `j < DIM('a)`, of "\<pi> i"] `i < CARD('b)`

  show "P (j + i * DIM('a))" by simp

qed

lemma (in real_basis) exists_CARD_DIM:

  "(\<exists>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<exists>i::'b::finite. \<exists>j<DIM('a). P (j + \<pi>' i * DIM('a)))"

  using forall_CARD_DIM[where 'b='b, of "\<lambda>x. \<not> P x"] by blast

lemma forall_CARD:

  "(\<forall>i<CARD('b). P i) \<longleftrightarrow> (\<forall>i::'b::finite. P (\<pi>' i))"

  using forall_CARD_DIM[where 'a=real, of P] by simp

lemma exists_CARD:

  "(\<exists>i<CARD('b). P i) \<longleftrightarrow> (\<exists>i::'b::finite. P (\<pi>' i))"

  using exists_CARD_DIM[where 'a=real, of P] by simp

lemmas cart_simps = forall_CARD_DIM exists_CARD_DIM forall_CARD exists_CARD

lemma cart_euclidean_nth[simp]:

  fixes x :: "('a::real_basis_with_inner, 'b::finite) cart"

  assumes j:"j < DIM('a)"

  shows "x $$ (j + \<pi>' i * DIM('a)) = x $ i $$ j"

  unfolding euclidean_component_def inner_vector_def basis_eq_pi'[OF j] if_distrib cond_application_beta

  by (simp add: setsum_cases)

lemma real_euclidean_nth:

  fixes x :: "real^'n"

  shows "x $$ \<pi>' i = (x $ i :: real)"

  using cart_euclidean_nth[where 'a=real, of 0 x i] by simp

lemmas nth_conv_component = real_euclidean_nth[symmetric]

lemma mult_split_eq:

  fixes A :: nat assumes "x < A" "y < A"

  shows "x + i * A = y + j * A \<longleftrightarrow> x = y \<and> i = j"

proof

  assume *: "x + i * A = y + j * A"

  { fix x y i j assume "i < j" "x < A" and *: "x + i * A = y + j * A"

    hence "x + i * A < Suc i * A" using `x < A` by simp

    also have "\<dots> \<le> j * A" using `i < j` unfolding mult_le_cancel2 by simp

    also have "\<dots> \<le> y + j * A" by simp

    finally have "i = j" using * by simp }

  note eq = this

  have "i = j"

  proof (cases rule: linorder_cases)

    assume "i < j" from eq[OF this `x < A` *] show "i = j" by simp

  next

    assume "j < i" from eq[OF this `y < A` *[symmetric]] show "i = j" by simp

  qed simp

  thus "x = y \<and> i = j" using * by simp

qed simp

instance cart :: (euclidean_space,finite) euclidean_space

proof (default, safe elim!: split_dimensions')

  let ?b = "basis :: nat \<Rightarrow> 'a^'b"

  have if_distrib_op: "\<And>f P Q a b c d.

    f (if P then a else b) (if Q then c else d) =

      (if P then if Q then f a c else f a d else if Q then f b c else f b d)"

    by simp

  fix i j k l

  assume "i < CARD('b)" "k < CARD('b)" "j < DIM('a)" "l < DIM('a)"

  thus "?b (j + i * DIM('a)) \<bullet> ?b (l + k * DIM('a)) =

    (if j + i * DIM('a) = l + k * DIM('a) then 1 else 0)"

    using inj_on_iff[OF \<pi>_inj_on[where 'n='b], of k i]

    by (auto simp add: basis_eq inner_vector_def if_distrib_op[of inner] setsum_cases basis_orthonormal mult_split_eq)

qed

instance cart :: (ordered_euclidean_space,finite) ordered_euclidean_space

proof

  fix x y::"'a^'b"

  show "(x \<le> y) = (\<forall>i<DIM(('a, 'b) cart). x $$ i \<le> y $$ i)"

    unfolding vector_le_def apply(subst eucl_le) by (simp add: cart_simps)

  show"(x < y) = (\<forall>i<DIM(('a, 'b) cart). x $$ i < y $$ i)"

    unfolding vector_less_def apply(subst eucl_less) by (simp add: cart_simps)

qed

subsection{* Basis vectors in coordinate directions. *}

definition "cart_basis k = (\<chi> i. if i = k then 1 else 0)"

lemma basis_component [simp]: "cart_basis k $ i = (if k=i then 1 else 0)"

  unfolding cart_basis_def by simp

lemma norm_basis[simp]:

  shows "norm (cart_basis k :: real ^'n) = 1"

  apply (simp add: cart_basis_def norm_eq_sqrt_inner) unfolding inner_vector_def

  apply (vector delta_mult_idempotent)

  using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"] by auto

lemma norm_basis_1: "norm(cart_basis 1 :: real ^'n::{finite,one}) = 1"

  by (rule norm_basis)

lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n). norm x = c"

  by (rule exI[where x="c *\<^sub>R cart_basis arbitrary"]) simp

lemma vector_choose_dist: assumes e: "0 <= e"

  shows "\<exists>(y::real^'n). dist x y = e"

proof-

  from vector_choose_size[OF e] obtain c:: "real ^'n"  where "norm c = e"

    by blast

  then have "dist x (x - c) = e" by (simp add: dist_norm)

  then show ?thesis by blast

qed

lemma basis_inj[intro]: "inj (cart_basis :: 'n \<Rightarrow> real ^'n)"

  by (simp add: inj_on_def Cart_eq)

lemma basis_expansion:

  "setsum (\<lambda>i. (x$i) *s cart_basis i) UNIV = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _")

  by (auto simp add: Cart_eq if_distrib setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong)

lemma smult_conv_scaleR: "c *s x = scaleR c x"

  unfolding vector_scalar_mult_def vector_scaleR_def by simp

lemma basis_expansion':

  "setsum (\<lambda>i. (x$i) *\<^sub>R cart_basis i) UNIV = x"

  by (rule basis_expansion [where 'a=real, unfolded smult_conv_scaleR])

lemma basis_expansion_unique:

  "setsum (\<lambda>i. f i *s cart_basis i) UNIV = (x::('a::comm_ring_1) ^'n) \<longleftrightarrow> (\<forall>i. f i = x$i)"

  by (simp add: Cart_eq setsum_delta if_distrib cong del: if_weak_cong)

lemma dot_basis:

  shows "cart_basis i \<bullet> x = x$i" "x \<bullet> (cart_basis i) = (x$i)"

  by (auto simp add: inner_vector_def cart_basis_def cond_application_beta if_distrib setsum_delta

           cong del: if_weak_cong)

lemma inner_basis:

  fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n"

  shows "inner (cart_basis i) x = inner 1 (x $ i)"

    and "inner x (cart_basis i) = inner (x $ i) 1"

  unfolding inner_vector_def cart_basis_def

  by (auto simp add: cond_application_beta if_distrib setsum_delta cong del: if_weak_cong)

lemma basis_eq_0: "cart_basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> False"

  by (auto simp add: Cart_eq)

lemma basis_nonzero:

  shows "cart_basis k \<noteq> (0:: 'a::semiring_1 ^'n)"

  by (simp add: basis_eq_0)

text {* some lemmas to map between Eucl and Cart *}

lemma basis_real_n[simp]:"(basis (\<pi>' i)::real^'a) = cart_basis i"

  unfolding basis_cart_def using pi'_range[where 'n='a]

  by (auto simp: Cart_eq Cart_lambda_beta)

subsection {* Orthogonality on cartesian products *}

lemma orthogonal_basis:

  shows "orthogonal (cart_basis i) x \<longleftrightarrow> x$i = (0::real)"

  by (auto simp add: orthogonal_def inner_vector_def cart_basis_def if_distrib

                     cond_application_beta setsum_delta cong del: if_weak_cong)

lemma orthogonal_basis_basis:

  shows "orthogonal (cart_basis i :: real^'n) (cart_basis j) \<longleftrightarrow> i \<noteq> j"

  unfolding orthogonal_basis[of i] basis_component[of j] by simp

subsection {* Linearity on cartesian products *}

lemma linear_vmul_component:

  assumes lf: "linear f"

  shows "linear (\<lambda>x. f x $ k *\<^sub>R v)"

  using lf

  by (auto simp add: linear_def algebra_simps)

subsection{* Adjoints on cartesian products *}

text {* TODO: The following lemmas about adjoints should hold for any

Hilbert space (i.e. complete inner product space).

(see \url{http://en.wikipedia.org/wiki/Hermitian_adjoint})

*}

lemma adjoint_works_lemma:

  fixes f:: "real ^'n \<Rightarrow> real ^'m"

  assumes lf: "linear f"

  shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y"

proof-

  let ?N = "UNIV :: 'n set"

  let ?M = "UNIV :: 'm set"

  have fN: "finite ?N" by simp

  have fM: "finite ?M" by simp

  {fix y:: "real ^ 'm"

    let ?w = "(\<chi> i. (f (cart_basis i) \<bullet> y)) :: real ^ 'n"

    {fix x

      have "f x \<bullet> y = f (setsum (\<lambda>i. (x$i) *\<^sub>R cart_basis i) ?N) \<bullet> y"

        by (simp only: basis_expansion')

      also have "\<dots> = (setsum (\<lambda>i. (x$i) *\<^sub>R f (cart_basis i)) ?N) \<bullet> y"

        unfolding linear_setsum[OF lf fN]

        by (simp add: linear_cmul[OF lf])

      finally have "f x \<bullet> y = x \<bullet> ?w"

        apply (simp only: )

        apply (simp add: inner_vector_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] field_simps)

        done}

  }

  then show ?thesis unfolding adjoint_def

    some_eq_ex[of "\<lambda>f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y"]

    using choice_iff[of "\<lambda>a b. \<forall>x. f x \<bullet> a = x \<bullet> b "]

    by metis

qed

lemma adjoint_works:

  fixes f:: "real ^'n \<Rightarrow> real ^'m"

  assumes lf: "linear f"

  shows "x \<bullet> adjoint f y = f x \<bullet> y"

  using adjoint_works_lemma[OF lf] by metis

lemma adjoint_linear:

  fixes f:: "real ^'n \<Rightarrow> real ^'m"

  assumes lf: "linear f"

  shows "linear (adjoint f)"

  unfolding linear_def vector_eq_ldot[where 'a="real^'n", symmetric] apply safe

  unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto

lemma adjoint_clauses:

  fixes f:: "real ^'n \<Rightarrow> real ^'m"

  assumes lf: "linear f"

  shows "x \<bullet> adjoint f y = f x \<bullet> y"

  and "adjoint f y \<bullet> x = y \<bullet> f x"

  by (simp_all add: adjoint_works[OF lf] inner_commute)

lemma adjoint_adjoint:

  fixes f:: "real ^'n \<Rightarrow> real ^'m"

  assumes lf: "linear f"

  shows "adjoint (adjoint f) = f"

  by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])

subsection {* Matrix operations *}

text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}

definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"  (infixl "**" 70)

  where "m ** m' == (\<chi> i j. setsum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"

definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"  (infixl "*v" 70)

  where "m *v x \<equiv> (\<chi> i. setsum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"

definition vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "  (infixl "v*" 70)

  where "v v* m == (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"

definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"

definition transpose where 

  "(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"

definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"

definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"

definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"

definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"

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 setsum_addf[symmetric] field_simps)

lemma matrix_mul_lid:

  fixes A :: "'a::semiring_1 ^ 'm ^ 'n"

  shows "mat 1 ** A = A"

  apply (simp add: matrix_matrix_mult_def mat_def)

  apply vector

  by (auto simp only: if_distrib cond_application_beta setsum_delta'[OF finite]  mult_1_left mult_zero_left if_True UNIV_I)

lemma matrix_mul_rid:

  fixes A :: "'a::semiring_1 ^ 'm ^ 'n"

  shows "A ** mat 1 = A"

  apply (simp add: matrix_matrix_mult_def mat_def)

  apply vector

  by (auto simp only: if_distrib cond_application_beta setsum_delta[OF finite]  mult_1_right mult_zero_right if_True UNIV_I cong: if_cong)

lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"

  apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)

  apply (subst setsum_commute)

  apply simp

  done

lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"

  apply (vector matrix_matrix_mult_def matrix_vector_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)

  apply (subst setsum_commute)

  apply simp

  done

lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"

  apply (vector matrix_vector_mult_def mat_def)

  by (simp add: if_distrib cond_application_beta

    setsum_delta' cong del: if_weak_cong)

lemma matrix_transpose_mul: "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"

  by (simp add: matrix_matrix_mult_def transpose_def Cart_eq mult_commute)

lemma matrix_eq:

  fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"

  shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")

  apply auto

  apply (subst Cart_eq)

  apply clarify

  apply (clarsimp simp add: matrix_vector_mult_def cart_basis_def if_distrib cond_application_beta Cart_eq cong del: if_weak_cong)

  apply (erule_tac x="cart_basis ia" in allE)

  apply (erule_tac x="i" in allE)

  by (auto simp add: cart_basis_def if_distrib cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong)

lemma matrix_vector_mul_component:

  shows "((A::real^_^_) *v x)$k = (A$k) \<bullet> x"

  by (simp add: matrix_vector_mult_def inner_vector_def)

lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"

  apply (simp add: inner_vector_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)

  apply (subst setsum_commute)

  by simp

lemma transpose_mat: "transpose (mat n) = mat n"

  by (vector transpose_def mat_def)

lemma transpose_transpose: "transpose(transpose A) = A"

  by (vector transpose_def)

lemma row_transpose:

  fixes A:: "'a::semiring_1^_^_"

  shows "row i (transpose A) = column i A"

  by (simp add: row_def column_def transpose_def Cart_eq)

lemma column_transpose:

  fixes A:: "'a::semiring_1^_^_"

  shows "column i (transpose A) = row i A"

  by (simp add: row_def column_def transpose_def Cart_eq)

lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"

by (auto simp add: rows_def columns_def row_transpose intro: set_eqI)

lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose)

text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}

lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"

  by (simp add: matrix_vector_mult_def inner_vector_def)

lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"

  by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute)

lemma vector_componentwise:

  "(x::'a::ring_1^'n) = (\<chi> j. setsum (\<lambda>i. (x$i) * (cart_basis i :: 'a^'n)$j) (UNIV :: 'n set))"

  apply (subst basis_expansion[symmetric])

  by (vector Cart_eq setsum_component)

lemma linear_componentwise:

  fixes f:: "real ^'m \<Rightarrow> real ^ _"

  assumes lf: "linear f"

  shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (cart_basis i)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")

proof-

  let ?M = "(UNIV :: 'm set)"

  let ?N = "(UNIV :: 'n set)"

  have fM: "finite ?M" by simp

  have "?rhs = (setsum (\<lambda>i.(x$i) *\<^sub>R f (cart_basis i) ) ?M)$j"

    unfolding vector_smult_component[symmetric] smult_conv_scaleR

    unfolding setsum_component[of "(\<lambda>i.(x$i) *\<^sub>R f (cart_basis i :: real^'m))" ?M]

    ..

  then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion' ..

qed

text{* Inverse matrices  (not necessarily square) *}

definition "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"

definition "matrix_inv(A:: 'a::semiring_1^'n^'m) =

        (SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"

text{* Correspondence between matrices and linear operators. *}

definition matrix:: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"

where "matrix f = (\<chi> i j. (f(cart_basis j))$i)"

lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"

  by (simp add: linear_def matrix_vector_mult_def Cart_eq field_simps setsum_right_distrib setsum_addf)

lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::real ^ 'n)"

apply (simp add: matrix_def matrix_vector_mult_def Cart_eq mult_commute)

apply clarify

apply (rule linear_componentwise[OF lf, symmetric])

done

lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))" by (simp add: ext matrix_works)

lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"

  by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)

lemma matrix_compose:

  assumes lf: "linear (f::real^'n \<Rightarrow> real^'m)"

  and lg: "linear (g::real^'m \<Rightarrow> real^_)"

  shows "matrix (g o f) = matrix g ** matrix f"

  using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]]

  by (simp  add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)

lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"

  by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute)

lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"

  apply (rule adjoint_unique)

  apply (simp add: transpose_def inner_vector_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)

  apply (subst setsum_commute)

  apply (auto simp add: mult_ac)

  done

lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"

  shows "matrix(adjoint f) = transpose(matrix f)"

  apply (subst matrix_vector_mul[OF lf])

  unfolding adjoint_matrix matrix_of_matrix_vector_mul ..

section {* lambda skolemization on cartesian products *}

(* FIXME: rename do choice_cart *)

lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>

   (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs")

proof-

  let ?S = "(UNIV :: 'n set)"

  {assume H: "?rhs"

    then have ?lhs by auto}

  moreover

  {assume H: "?lhs"

    then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis

    let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"

    {fix i

      from f have "P i (f i)" by metis

      then have "P i (?x $ i)" by auto

    }

    hence "\<forall>i. P i (?x$i)" by metis

    hence ?rhs by metis }

  ultimately show ?thesis by metis

qed

subsection {* Standard bases are a spanning set, and obviously finite. *}

lemma span_stdbasis:"span {cart_basis i :: real^'n | i. i \<in> (UNIV :: 'n set)} = UNIV"

apply (rule set_eqI)

apply auto

apply (subst basis_expansion'[symmetric])

apply (rule span_setsum)

apply simp