(*  Title:      Library/Euclidean_Space

    Author:     Amine Chaieb, University of Cambridge

*)

header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}

theory Euclidean_Space

imports

  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"

  Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type

  Inner_Product

uses "positivstellensatz.ML" ("normarith.ML")

begin

text{* Some common special cases.*}

lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"

  by (metis num1_eq_iff)

lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"

  by auto (metis num1_eq_iff)

lemma exhaust_2:

  fixes x :: 2 shows "x = 1 \<or> x = 2"

proof (induct x)

  case (of_int z)

  then have "0 <= z" and "z < 2" by simp_all

  then have "z = 0 | z = 1" by arith

  then show ?case by auto

qed

lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"

  by (metis exhaust_2)

lemma exhaust_3:

  fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"

proof (induct x)

  case (of_int z)

  then have "0 <= z" and "z < 3" by simp_all

  then have "z = 0 \<or> z = 1 \<or> z = 2" by arith

  then show ?case by auto

qed

lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"

  by (metis exhaust_3)

lemma UNIV_1: "UNIV = {1::1}"

  by (auto simp add: num1_eq_iff)

lemma UNIV_2: "UNIV = {1::2, 2::2}"

  using exhaust_2 by auto

lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"

  using exhaust_3 by auto

lemma setsum_1: "setsum f (UNIV::1 set) = f 1"

  unfolding UNIV_1 by simp

lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"

  unfolding UNIV_2 by simp

lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"

  unfolding UNIV_3 by (simp add: add_ac)

subsection{* Basic componentwise operations on vectors. *}

instantiation cart :: (plus,finite) plus

begin

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

instance ..

end

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 :: (minus,finite) minus begin

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

instance ..

end

instantiation cart :: (uminus,finite) uminus begin

  definition vector_uminus_def : "uminus \<equiv> (\<lambda> x.  (\<chi> i. - (x$i)))"

instance ..

end

instantiation cart :: (zero,finite) zero begin

  definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)"

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

instantiation cart :: (scaleR, finite) scaleR

begin

definition vector_scaleR_def: "scaleR = (\<lambda> r x.  (\<chi> i. scaleR r (x$i)))"

instance ..

end

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))"

text{* Constant Vectors *} 

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

text{* Dot products. *}

definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where

  "x \<bullet> y = setsum (\<lambda>i. x$i * y$i) UNIV"

lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x$1) * (y$1)"

  by (simp add: dot_def setsum_1)

lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2)"

  by (simp add: dot_def setsum_2)

lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)"

  by (simp add: dot_def setsum_3)

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 dot_def}, @{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

*} "Lifts 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)

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

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

  by (vector vec_def)

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

  by vector

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

  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 vector_uminus_component [simp]: "(- x)$i = - (x$i)"

  by vector

lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$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_add,finite) semigroup_add

  apply (intro_classes) by (vector add_assoc)

instance cart :: (monoid_add,finite) monoid_add

  apply (intro_classes) by vector+

instance cart :: (group_add,finite) group_add

  apply (intro_classes) by (vector algebra_simps)+

instance cart :: (ab_semigroup_add,finite) ab_semigroup_add

  apply (intro_classes) by (vector add_commute)

instance cart :: (comm_monoid_add,finite) comm_monoid_add

  apply (intro_classes) by vector

instance cart :: (ab_group_add,finite) ab_group_add

  apply (intro_classes) by vector+

instance cart :: (cancel_semigroup_add,finite) cancel_semigroup_add

  apply (intro_classes)

  by (vector Cart_eq)+

instance cart :: (cancel_ab_semigroup_add,finite) cancel_ab_semigroup_add

  apply (intro_classes)

  by (vector Cart_eq)

instance cart :: (real_vector, finite) real_vector

  by default (vector scaleR_left_distrib scaleR_right_distrib)+

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

fun vector_power where

  "vector_power x 0 = 1"

  | "vector_power x (Suc n) = x * vector_power x n"

instance cart :: (semiring,finite) semiring

  apply (intro_classes) by (vector ring_simps)+

instance cart :: (semiring_0,finite) semiring_0

  apply (intro_classes) by (vector ring_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 ring_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 ring_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 zero_index[simp]:

  "(0 :: 'a::zero ^'n)$i = 0" by vector

lemma one_index[simp]:

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

lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \<noteq> 0"

proof-

  have "(1::'a) + of_nat n = 0 \<longleftrightarrow> of_nat 1 + of_nat n = (of_nat 0 :: 'a)" by simp

  also have "\<dots> \<longleftrightarrow> 1 + n = 0" by (simp only: of_nat_add[symmetric] of_nat_eq_iff)

  finally show ?thesis by simp

qed

instance cart :: (semiring_char_0,finite) semiring_char_0

proof (intro_classes)

  fix m n ::nat

  show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"

    by (simp add: Cart_eq of_nat_index)

qed

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

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

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 ring_simps)

lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y"

  by (vector ring_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 ring_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 ring_simps)

lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"

  by (simp add: Cart_eq)

subsection {* Topological space *}

instantiation cart :: (topological_space, finite) topological_space

begin

definition open_vector_def:

  "open (S :: ('a ^ 'b) set) \<longleftrightarrow>

    (\<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 proof

  show "open (UNIV :: ('a ^ 'b) set)"

    unfolding open_vector_def by auto

next

  fix S T :: "('a ^ 'b) set"

  assume "open S" "open T" thus "open (S \<inter> T)"

    unfolding open_vector_def

    apply clarify

    apply (drule (1) bspec)+

    apply (clarify, rename_tac Sa Ta)

    apply (rule_tac x="\<lambda>i. Sa i \<inter> Ta i" in exI)

    apply (simp add: open_Int)

    done

next

  fix K :: "('a ^ 'b) set set"

  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"

    unfolding open_vector_def

    apply clarify

    apply (drule (1) bspec)

    apply (drule (1) bspec)

    apply clarify

    apply (rule_tac x=A in exI)

    apply fast

    done

qed

end

lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}"

unfolding open_vector_def by auto

lemma open_vimage_Cart_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)"

unfolding open_vector_def

apply clarify

apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)

done

lemma closed_vimage_Cart_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"

unfolding closed_open vimage_Compl [symmetric]

by (rule open_vimage_Cart_nth)

lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"

proof -

  have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto

  thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"

    by (simp add: closed_INT closed_vimage_Cart_nth)

qed

lemma tendsto_Cart_nth [tendsto_intros]:

  assumes "((\<lambda>x. f x) ---> a) net"

  shows "((\<lambda>x. f x $ i) ---> a $ i) net"

proof (rule topological_tendstoI)

  fix S assume "open S" "a $ i \<in> S"

  then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"

    by (simp_all add: open_vimage_Cart_nth)

  with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net"

    by (rule topological_tendstoD)

  then show "eventually (\<lambda>x. f x $ i \<in> S) net"

    by simp

qed

subsection {* Square root of sum of squares *}

definition

  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"

lemma setL2_cong:

  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"

  unfolding setL2_def by simp

lemma strong_setL2_cong:

  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"

  unfolding setL2_def simp_implies_def by simp

lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"

  unfolding setL2_def by simp

lemma setL2_empty [simp]: "setL2 f {} = 0"

  unfolding setL2_def by simp

lemma setL2_insert [simp]:

  "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>

    setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)"

  unfolding setL2_def by (simp add: setsum_nonneg)

lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"

  unfolding setL2_def by (simp add: setsum_nonneg)

lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"

  unfolding setL2_def by simp

lemma setL2_constant: "setL2 (\<lambda>x. y) A = sqrt (of_nat (card A)) * \<bar>y\<bar>"

  unfolding setL2_def by (simp add: real_sqrt_mult)

lemma setL2_mono:

  assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"

  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"

  shows "setL2 f K \<le> setL2 g K"

  unfolding setL2_def

  by (simp add: setsum_nonneg setsum_mono power_mono prems)

lemma setL2_strict_mono:

  assumes "finite K" and "K \<noteq> {}"

  assumes "\<And>i. i \<in> K \<Longrightarrow> f i < g i"

  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"

  shows "setL2 f K < setL2 g K"

  unfolding setL2_def

  by (simp add: setsum_strict_mono power_strict_mono assms)

lemma setL2_right_distrib:

  "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"

  unfolding setL2_def

  apply (simp add: power_mult_distrib)

  apply (simp add: setsum_right_distrib [symmetric])

  apply (simp add: real_sqrt_mult setsum_nonneg)

  done

lemma setL2_left_distrib:

  "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"

  unfolding setL2_def

  apply (simp add: power_mult_distrib)

  apply (simp add: setsum_left_distrib [symmetric])

  apply (simp add: real_sqrt_mult setsum_nonneg)

  done

lemma setsum_nonneg_eq_0_iff:

  fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"

  shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"

  apply (induct set: finite, simp)

  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)

  done

lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"

  unfolding setL2_def

  by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)

lemma setL2_triangle_ineq:

  shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"

proof (cases "finite A")

  case False

  thus ?thesis by simp

next

  case True

  thus ?thesis

  proof (induct set: finite)

    case empty

    show ?case by simp

  next

    case (insert x F)

    hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le>

           sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)"

      by (intro real_sqrt_le_mono add_left_mono power_mono insert

                setL2_nonneg add_increasing zero_le_power2)

    also have

      "\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)"

      by (rule real_sqrt_sum_squares_triangle_ineq)

    finally show ?case

      using insert by simp

  qed

qed

lemma sqrt_sum_squares_le_sum:

  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"

  apply (rule power2_le_imp_le)

  apply (simp add: power2_sum)

  apply (simp add: mult_nonneg_nonneg)

  apply (simp add: add_nonneg_nonneg)

  done

lemma setL2_le_setsum [rule_format]:

  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A"

  apply (cases "finite A")

  apply (induct set: finite)

  apply simp

  apply clarsimp

  apply (erule order_trans [OF sqrt_sum_squares_le_sum])

  apply simp

  apply simp

  apply simp

  done

lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"

  apply (rule power2_le_imp_le)

  apply (simp add: power2_sum)

  apply (simp add: mult_nonneg_nonneg)

  apply (simp add: add_nonneg_nonneg)

  done

lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"

  apply (cases "finite A")

  apply (induct set: finite)

  apply simp

  apply simp

  apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])

  apply simp

  apply simp

  done

lemma setL2_mult_ineq_lemma:

  fixes a b c d :: real

  shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"

proof -

  have "0 \<le> (a * d - b * c)\<twosuperior>" by simp

  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * d) * (b * c)"

    by (simp only: power2_diff power_mult_distrib)

  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * c) * (b * d)"

    by simp

  finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"

    by simp

qed

lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"

  apply (cases "finite A")

  apply (induct set: finite)

  apply simp

  apply (rule power2_le_imp_le, simp)

  apply (rule order_trans)

  apply (rule power_mono)

  apply (erule add_left_mono)

  apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg)

  apply (simp add: power2_sum)

  apply (simp add: power_mult_distrib)

  apply (simp add: right_distrib left_distrib)

  apply (rule ord_le_eq_trans)

  apply (rule setL2_mult_ineq_lemma)

  apply simp

  apply (intro mult_nonneg_nonneg setL2_nonneg)

  apply simp

  done

lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"

  apply (rule_tac s="insert i (A - {i})" and t="A" in subst)

  apply fast

  apply (subst setL2_insert)

  apply simp

  apply simp

  apply simp

  done

subsection {* Metric *}

(* TODO: move somewhere else *)

lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"

apply (induct set: finite, simp_all)

apply (clarify, rename_tac y)

apply (rule_tac x="f(x:=y)" in exI, simp)

done

instantiation cart :: (metric_space, finite) metric_space

begin

definition dist_vector_def:

  "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"

lemma dist_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"

unfolding dist_vector_def

by (rule member_le_setL2) simp_all

instance proof

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

  show "dist x y = 0 \<longleftrightarrow> x = y"

    unfolding dist_vector_def

    by (simp add: setL2_eq_0_iff Cart_eq)

next

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

  show "dist x y \<le> dist x z + dist y z"

    unfolding dist_vector_def

    apply (rule order_trans [OF _ setL2_triangle_ineq])

    apply (simp add: setL2_mono dist_triangle2)

    done

next

  (* FIXME: long proof! *)

  fix S :: "('a ^ 'b) set"

  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"

    unfolding open_vector_def open_dist

    apply safe

     apply (drule (1) bspec)

     apply clarify

     apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i")

      apply clarify

      apply (rule_tac x=e in exI, clarify)

      apply (drule spec, erule mp, clarify)

      apply (drule spec, drule spec, erule mp)

      apply (erule le_less_trans [OF dist_nth_le])

     apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i")

      apply (drule finite_choice [OF finite], clarify)

      apply (rule_tac x="Min (range f)" in exI, simp)

     apply clarify

     apply (drule_tac x=i in spec, clarify)

     apply (erule (1) bspec)

    apply (drule (1) bspec, clarify)

    apply (subgoal_tac "\<exists>r. (\<forall>i::'b. 0 < r i) \<and> e = setL2 r UNIV")

     apply clarify

     apply (rule_tac x="\<lambda>i. {y. dist y (x$i) < r i}" in exI)

     apply (rule conjI)

      apply clarify

      apply (rule conjI)

       apply (clarify, rename_tac y)

       apply (rule_tac x="r i - dist y (x$i)" in exI, rule conjI, simp)

       apply clarify

       apply (simp only: less_diff_eq)

       apply (erule le_less_trans [OF dist_triangle])

      apply simp

     apply clarify

     apply (drule spec, erule mp)

     apply (simp add: dist_vector_def setL2_strict_mono)

    apply (rule_tac x="\<lambda>i. e / sqrt (of_nat CARD('b))" in exI)

    apply (simp add: divide_pos_pos setL2_constant)

    done

qed

end

lemma LIMSEQ_Cart_nth:

  "(X ----> a) \<Longrightarrow> (\<lambda>n. X n $ i) ----> a $ i"

unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth)

lemma LIM_Cart_nth:

  "(f -- x --> y) \<Longrightarrow> (\<lambda>x. f x $ i) -- x --> y $ i"

unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth)

lemma Cauchy_Cart_nth:

  "Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)"

unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le])

lemma LIMSEQ_vector:

  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"

  assumes X: "\<And>i. (\<lambda>n. X n $ i) ----> (a $ i)"

  shows "X ----> a"

proof (rule metric_LIMSEQ_I)

  fix r :: real assume "0 < r"

  then have "0 < r / of_nat CARD('n)" (is "0 < ?s")

    by (simp add: divide_pos_pos)

  def N \<equiv> "\<lambda>i. LEAST N. \<forall>n\<ge>N. dist (X n $ i) (a $ i) < ?s"

  def M \<equiv> "Max (range N)"

  have "\<And>i. \<exists>N. \<forall>n\<ge>N. dist (X n $ i) (a $ i) < ?s"

    using X `0 < ?s` by (rule metric_LIMSEQ_D)

  hence "\<And>i. \<forall>n\<ge>N i. dist (X n $ i) (a $ i) < ?s"

    unfolding N_def by (rule LeastI_ex)

  hence M: "\<And>i. \<forall>n\<ge>M. dist (X n $ i) (a $ i) < ?s"

    unfolding M_def by simp

  {

    fix n :: nat assume "M \<le> n"

    have "dist (X n) a = setL2 (\<lambda>i. dist (X n $ i) (a $ i)) UNIV"

      unfolding dist_vector_def ..

    also have "\<dots> \<le> setsum (\<lambda>i. dist (X n $ i) (a $ i)) UNIV"

      by (rule setL2_le_setsum [OF zero_le_dist])

    also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV"

      by (rule setsum_strict_mono, simp_all add: M `M \<le> n`)

    also have "\<dots> = r"

      by simp

    finally have "dist (X n) a < r" .

  }

  hence "\<forall>n\<ge>M. dist (X n) a < r"

    by simp

  then show "\<exists>M. \<forall>n\<ge>M. dist (X n) a < r" ..

qed

lemma Cauchy_vector:

  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"

  assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"

  shows "Cauchy (\<lambda>n. X n)"

proof (rule metric_CauchyI)

  fix r :: real assume "0 < r"

  then have "0 < r / of_nat CARD('n)" (is "0 < ?s")

    by (simp add: divide_pos_pos)

  def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"

  def M \<equiv> "Max (range N)"

  have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"

    using X `0 < ?s` by (rule metric_CauchyD)

  hence "\<And>i. \<forall>m\<ge>N i. \<forall>n\<ge>N i. dist (X m $ i) (X n $ i) < ?s"

    unfolding N_def by (rule LeastI_ex)

  hence M: "\<And>i. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < ?s"

    unfolding M_def by simp

  {

    fix m n :: nat

    assume "M \<le> m" "M \<le> n"

    have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"

      unfolding dist_vector_def ..

    also have "\<dots> \<le> setsum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"

      by (rule setL2_le_setsum [OF zero_le_dist])

    also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV"

      by (rule setsum_strict_mono, simp_all add: M `M \<le> m` `M \<le> n`)

    also have "\<dots> = r"

      by simp

    finally have "dist (X m) (X n) < r" .

  }

  hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r"

    by simp

  then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" ..

qed

instance cart :: (complete_space, finite) complete_space

proof

  fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X"

  have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)"

    using Cauchy_Cart_nth [OF `Cauchy X`]

    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)

  hence "X ----> Cart_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))"

    by (simp add: LIMSEQ_vector)

  then show "convergent X"

    by (rule convergentI)

qed

subsection {* Norms *}

instantiation cart :: (real_normed_vector, finite) real_normed_vector

begin

definition norm_vector_def:

  "norm (x::'a^'b) = setL2 (\<lambda>i. norm (x$i)) UNIV"

definition vector_sgn_def:

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

instance proof

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

  show "0 \<le> norm x"

    unfolding norm_vector_def

    by (rule setL2_nonneg)

  show "norm x = 0 \<longleftrightarrow> x = 0"

    unfolding norm_vector_def

    by (simp add: setL2_eq_0_iff Cart_eq)

  show "norm (x + y) \<le> norm x + norm y"

    unfolding norm_vector_def

    apply (rule order_trans [OF _ setL2_triangle_ineq])

    apply (simp add: setL2_mono norm_triangle_ineq)

    done

  show "norm (scaleR a x) = \<bar>a\<bar> * norm x"

    unfolding norm_vector_def

    by (simp add: setL2_right_distrib)

  show "sgn x = scaleR (inverse (norm x)) x"

    by (rule vector_sgn_def)

  show "dist x y = norm (x - y)"

    unfolding dist_vector_def norm_vector_def

    by (simp add: dist_norm)

qed

end

lemma norm_nth_le: "norm (x $ i) \<le> norm x"

unfolding norm_vector_def

by (rule member_le_setL2) simp_all

interpretation Cart_nth: bounded_linear "\<lambda>x. x $ i"

apply default

apply (rule vector_add_component)

apply (rule vector_scaleR_component)

apply (rule_tac x="1" in exI, simp add: norm_nth_le)

done

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

subsection {* Inner products *}

instantiation cart :: (real_inner, finite) real_inner

begin

definition inner_vector_def:

  "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV"

instance proof

  fix r :: real and x y z :: "'a ^ 'b"

  show "inner x y = inner y x"

    unfolding inner_vector_def

    by (simp add: inner_commute)

  show "inner (x + y) z = inner x z + inner y z"

    unfolding inner_vector_def

    by (simp add: inner_add_left setsum_addf)

  show "inner (scaleR r x) y = r * inner x y"

    unfolding inner_vector_def

    by (simp add: setsum_right_distrib)

  show "0 \<le> inner x x"

    unfolding inner_vector_def

    by (simp add: setsum_nonneg)

  show "inner x x = 0 \<longleftrightarrow> x = 0"

    unfolding inner_vector_def

    by (simp add: Cart_eq setsum_nonneg_eq_0_iff)

  show "norm x = sqrt (inner x x)"

    unfolding inner_vector_def norm_vector_def setL2_def

    by (simp add: power2_norm_eq_inner)

qed

end

subsection{* Properties of the dot product.  *}

lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"

  by (vector mult_commute)

lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)"

  by (vector ring_simps)

lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n)) = (x \<bullet> y) + (x \<bullet> z)"

  by (vector ring_simps)

lemma dot_lsub: "((x::'a::ring ^ 'n) - y) \<bullet> z = (x \<bullet> z) - (y \<bullet> z)"

  by (vector ring_simps)

lemma dot_rsub: "(x::'a::ring ^ 'n) \<bullet> (y - z) = (x \<bullet> y) - (x \<bullet> z)"

  by (vector ring_simps)

lemma dot_lmult: "(c *s x) \<bullet> y = (c::'a::ring) * (x \<bullet> y)" by (vector ring_simps)

lemma dot_rmult: "x \<bullet> (c *s y) = (c::'a::comm_ring) * (x \<bullet> y)" by (vector ring_simps)

lemma dot_lneg: "(-x) \<bullet> (y::'a::ring ^ 'n) = -(x \<bullet> y)" by vector

lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (-y) = -(x \<bullet> y)" by vector

lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector

lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector

lemma dot_pos_le[simp]: "(0::'a\<Colon>linordered_ring_strict) <= x \<bullet> x"

  by (simp add: dot_def setsum_nonneg)

lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)"

using fS fp setsum_nonneg[OF fp]

proof (induct set: finite)

  case empty thus ?case by simp

next

  case (insert x F)

  from insert.prems have Fx: "f x \<ge> 0" and Fp: "\<forall> a \<in> F. f a \<ge> 0" by simp_all

  from insert.hyps Fp setsum_nonneg[OF Fp]

  have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis

  from add_nonneg_eq_0_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)

  show ?case by (simp add: h)

qed

lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0"

  by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq)

lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]

  by (auto simp add: le_less)

subsection{* The collapse of the general concepts to dimension one. *}

lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"

  by (simp add: Cart_eq forall_1)

lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"

  apply auto

  apply (erule_tac x= "x$1" in allE)

  apply (simp only: vector_one[symmetric])

  done

lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"

  by (simp add: norm_vector_def UNIV_1)

lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"

  by (simp add: norm_vector_1)

lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"

  by (auto simp add: norm_real dist_norm)

subsection {* A connectedness or intermediate value lemma with several applications. *}

lemma connected_real_lemma:

  fixes f :: "real \<Rightarrow> 'a::metric_space"

  assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"

  and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"

  and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"

  and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"

  and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"

  shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")

proof-

  let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"

  have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa)

  have Sub: "\<exists>y. isUb UNIV ?S y"

    apply (rule exI[where x= b])

    using ab fb e12 by (auto simp add: isUb_def setle_def)

  from reals_complete[OF Se Sub] obtain l where

    l: "isLub UNIV ?S l"by blast

  have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12

    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)

    by (metis linorder_linear)

  have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l

    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)

    by (metis linorder_linear not_le)

    have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith

    have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith

    have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by dlo

    {assume le2: "f l \<in> e2"

      from le2 fa fb e12 alb have la: "l \<noteq> a" by metis

      hence lap: "l - a > 0" using alb by arith

      from e2[rule_format, OF le2] obtain e where

        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis

      from dst[OF alb e(1)] obtain d where

        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis

      have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" using lap d(1)

        apply ferrack by arith

      then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis

      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis

      from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto

      moreover

      have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto

      ultimately have False using e12 alb d' by auto}

    moreover

    {assume le1: "f l \<in> e1"

    from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis

      hence blp: "b - l > 0" using alb by arith

      from e1[rule_format, OF le1] obtain e where

        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis

      from dst[OF alb e(1)] obtain d where

        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis

      have "\<exists>d'. d' < d \<and> d' >0" using d(1) by dlo

      then obtain d' where d': "d' > 0" "d' < d" by metis

      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto

      hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto

      with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto

      with l d' have False

        by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }

    ultimately show ?thesis using alb by metis

qed

text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case @{typ "real^1"} *}

lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"

proof-

  have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith

  thus ?thesis by (simp add: ring_simps power2_eq_square)

qed

lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)"

  using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] apply (auto simp add: power2_eq_square)

  apply (rule_tac x="s" in exI)

  apply auto

  apply (erule_tac x=y in allE)

  apply auto

  done

lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y"

  using real_sqrt_le_iff[of x "y^2"] by simp

lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y"

  using real_sqrt_le_mono[of "x^2" y] by simp

lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y"

  using real_sqrt_less_mono[of "x^2" y] by simp

lemma sqrt_even_pow2: assumes n: "even n"

  shows "sqrt(2 ^ n) = 2 ^ (n div 2)"

proof-

  from n obtain m where m: "n = 2*m" unfolding even_nat_equiv_def2

    by (auto simp add: nat_number)

  from m  have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)"

    by (simp only: power_mult[symmetric] mult_commute)

  then show ?thesis  using m by simp

qed

lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)"

  apply (cases "x = 0", simp_all)

  using sqrt_divide_self_eq[of x]

  apply (simp add: inverse_eq_divide real_sqrt_ge_0_iff field_simps)

  done

text{* Hence derive more interesting properties of the norm. *}

text {*

  This type-specific version is only here

  to make @{text normarith.ML} happy.

*}

lemma norm_0: "norm (0::real ^ _) = 0"

  by (rule norm_zero)

lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"

  by (simp add: norm_vector_def vector_component setL2_right_distrib

           abs_mult cong: strong_setL2_cong)