src/HOL/Library/Euclidean_Space.thy
 changeset 30582 638b088bb840 parent 30549 d2d7874648bd child 30655 88131f2807b6 child 30661 54858c8ad226
equal inserted replaced
30581:ac50e7dedf6d 30582:638b088bb840
`    11   uses ("normarith.ML")`
`    11   uses ("normarith.ML")`
`    12 begin`
`    12 begin`
`    13 `
`    13 `
`    14 text{* Some common special cases.*}`
`    14 text{* Some common special cases.*}`
`    15 `
`    15 `
`    16 lemma forall_1: "(\<forall>(i::'a::{order,one}). 1 <= i \<and> i <= 1 --> P i) \<longleftrightarrow> P 1"`
`    16 lemma forall_1: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"`
`    17   by (metis order_eq_iff)`
`    17   by (metis num1_eq_iff)`
`    18 lemma forall_dimindex_1: "(\<forall>i \<in> {1..dimindex(UNIV:: 1 set)}. P i) \<longleftrightarrow> P 1"`
`    18 `
`    19   by (simp add: dimindex_def)`
`    19 lemma exhaust_2:`
`    20 `
`    20   fixes x :: 2 shows "x = 1 \<or> x = 2"`
`    21 lemma forall_2: "(\<forall>(i::nat). 1 <= i \<and> i <= 2 --> P i) \<longleftrightarrow> P 1 \<and> P 2"`
`    21 proof (induct x)`
`    22 proof-`
`    22   case (of_int z)`
`    23   have "\<And>i::nat. 1 <= i \<and> i <= 2 \<longleftrightarrow> i = 1 \<or> i = 2" by arith`
`    23   then have "0 <= z" and "z < 2" by simp_all`
`    24   thus ?thesis by metis`
`    24   then have "z = 0 | z = 1" by arith`
`    25 qed`
`    25   then show ?case by auto`
`    26 `
`    26 qed`
`    27 lemma forall_3: "(\<forall>(i::nat). 1 <= i \<and> i <= 3 --> P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"`
`    27 `
`    28 proof-`
`    28 lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"`
`    29   have "\<And>i::nat. 1 <= i \<and> i <= 3 \<longleftrightarrow> i = 1 \<or> i = 2 \<or> i = 3" by arith`
`    29   by (metis exhaust_2)`
`    30   thus ?thesis by metis`
`    30 `
`    31 qed`
`    31 lemma exhaust_3:`
`    32 `
`    32   fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"`
`    33 lemma setsum_singleton[simp]: "setsum f {x} = f x" by simp`
`    33 proof (induct x)`
`    34 lemma setsum_1: "setsum f {(1::'a::{order,one})..1} = f 1"`
`    34   case (of_int z)`
`    35   by (simp add: atLeastAtMost_singleton)`
`    35   then have "0 <= z" and "z < 3" by simp_all`
`    36 `
`    36   then have "z = 0 \<or> z = 1 \<or> z = 2" by arith`
`    37 lemma setsum_2: "setsum f {1::nat..2} = f 1 + f 2"`
`    37   then show ?case by auto`
`    38   by (simp add: nat_number  atLeastAtMostSuc_conv add_commute)`
`    38 qed`
`    39 `
`    39 `
`    40 lemma setsum_3: "setsum f {1::nat..3} = f 1 + f 2 + f 3"`
`    40 lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"`
`    41   by (simp add: nat_number  atLeastAtMostSuc_conv add_commute)`
`    41   by (metis exhaust_3)`
`       `
`    42 `
`       `
`    43 lemma UNIV_1: "UNIV = {1::1}"`
`       `
`    44   by (auto simp add: num1_eq_iff)`
`       `
`    45 `
`       `
`    46 lemma UNIV_2: "UNIV = {1::2, 2::2}"`
`       `
`    47   using exhaust_2 by auto`
`       `
`    48 `
`       `
`    49 lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"`
`       `
`    50   using exhaust_3 by auto`
`       `
`    51 `
`       `
`    52 lemma setsum_1: "setsum f (UNIV::1 set) = f 1"`
`       `
`    53   unfolding UNIV_1 by simp`
`       `
`    54 `
`       `
`    55 lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"`
`       `
`    56   unfolding UNIV_2 by simp`
`       `
`    57 `
`       `
`    58 lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"`
`       `
`    59   unfolding UNIV_3 by (simp add: add_ac)`
`    42 `
`    60 `
`    43 subsection{* Basic componentwise operations on vectors. *}`
`    61 subsection{* Basic componentwise operations on vectors. *}`
`    44 `
`    62 `
`    45 instantiation "^" :: (plus,type) plus`
`    63 instantiation "^" :: (plus,type) plus`
`    46 begin`
`    64 begin`
`    74 end`
`    92 end`
`    75 `
`    93 `
`    76 instantiation "^" :: (ord,type) ord`
`    94 instantiation "^" :: (ord,type) ord`
`    77  begin`
`    95  begin`
`    78 definition vector_less_eq_def:`
`    96 definition vector_less_eq_def:`
`    79   "less_eq (x :: 'a ^'b) y = (ALL i : {1 .. dimindex (UNIV :: 'b set)}.`
`    97   "less_eq (x :: 'a ^'b) y = (ALL i. x\$i <= y\$i)"`
`    80   x\$i <= y\$i)"`
`    98 definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x\$i < y\$i)"`
`    81 definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i : {1 ..`
`       `
`    82   dimindex (UNIV :: 'b set)}. x\$i < y\$i)"`
`       `
`    83 `
`    99 `
`    84 instance by (intro_classes)`
`   100 instance by (intro_classes)`
`    85 end`
`   101 end`
`    86 `
`   102 `
`    87 instantiation "^" :: (scaleR, type) scaleR`
`   103 instantiation "^" :: (scaleR, type) scaleR`
`   100 definition "vec x = (\<chi> i. x)"`
`   116 definition "vec x = (\<chi> i. x)"`
`   101 `
`   117 `
`   102 text{* Dot products. *}`
`   118 text{* Dot products. *}`
`   103 `
`   119 `
`   104 definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where`
`   120 definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where`
`   105   "x \<bullet> y = setsum (\<lambda>i. x\$i * y\$i) {1 .. dimindex (UNIV:: 'n set)}"`
`   121   "x \<bullet> y = setsum (\<lambda>i. x\$i * y\$i) UNIV"`
`       `
`   122 `
`   106 lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x\$1) * (y\$1)"`
`   123 lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x\$1) * (y\$1)"`
`   107   by (simp add: dot_def dimindex_def)`
`   124   by (simp add: dot_def setsum_1)`
`   108 `
`   125 `
`   109 lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \<bullet> y = (x\$1) * (y\$1) + (x\$2) * (y\$2)"`
`   126 lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \<bullet> y = (x\$1) * (y\$1) + (x\$2) * (y\$2)"`
`   110   by (simp add: dot_def dimindex_def nat_number)`
`   127   by (simp add: dot_def setsum_2)`
`   111 `
`   128 `
`   112 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)"`
`   129 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)"`
`   113   by (simp add: dot_def dimindex_def nat_number)`
`   130   by (simp add: dot_def setsum_3)`
`   114 `
`   131 `
`   115 subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}`
`   132 subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}`
`   116 `
`   133 `
`   118 method_setup vector = {*`
`   134 method_setup vector = {*`
`   119 let`
`   135 let`
`   120   val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym,`
`   136   val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym,`
`   121   @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},`
`   137   @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},`
`   122   @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]`
`   138   @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]`
`   123   val ss2 = @{simpset} addsimps`
`   139   val ss2 = @{simpset} addsimps`
`   124              [@{thm vector_add_def}, @{thm vector_mult_def},`
`   140              [@{thm vector_add_def}, @{thm vector_mult_def},`
`   125               @{thm vector_minus_def}, @{thm vector_uminus_def},`
`   141               @{thm vector_minus_def}, @{thm vector_uminus_def},`
`   126               @{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},`
`   142               @{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},`
`   127               @{thm vector_scaleR_def},`
`   143               @{thm vector_scaleR_def},`
`   128               @{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}]`
`   144               @{thm Cart_lambda_beta}, @{thm vector_scalar_mult_def}]`
`   129  fun vector_arith_tac ths =`
`   145  fun vector_arith_tac ths =`
`   130    simp_tac ss1`
`   146    simp_tac ss1`
`   131    THEN' (fn i => rtac @{thm setsum_cong2} i`
`   147    THEN' (fn i => rtac @{thm setsum_cong2} i`
`   132          ORELSE rtac @{thm setsum_0'} i`
`   148          ORELSE rtac @{thm setsum_0'} i`
`   133          ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i)`
`   149          ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i)`
`   143 `
`   159 `
`   144 `
`   160 `
`   145 `
`   161 `
`   146 text{* Obvious "component-pushing". *}`
`   162 text{* Obvious "component-pushing". *}`
`   147 `
`   163 `
`   148 lemma vec_component: " i \<in> {1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (vec x :: 'a ^ 'n)\$i = x"`
`   164 lemma vec_component [simp]: "(vec x :: 'a ^ 'n)\$i = x"`
`   149   by (vector vec_def)`
`   165   by (vector vec_def)`
`   150 `
`   166 `
`   151 lemma vector_add_component:`
`   167 lemma vector_add_component [simp]:`
`   152   fixes x y :: "'a::{plus} ^ 'n"  assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}"`
`   168   fixes x y :: "'a::{plus} ^ 'n"`
`   153   shows "(x + y)\$i = x\$i + y\$i"`
`   169   shows "(x + y)\$i = x\$i + y\$i"`
`   154   using i by vector`
`   170   by vector`
`   155 `
`   171 `
`   156 lemma vector_minus_component:`
`   172 lemma vector_minus_component [simp]:`
`   157   fixes x y :: "'a::{minus} ^ 'n"  assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}"`
`   173   fixes x y :: "'a::{minus} ^ 'n"`
`   158   shows "(x - y)\$i = x\$i - y\$i"`
`   174   shows "(x - y)\$i = x\$i - y\$i"`
`   159   using i  by vector`
`   175   by vector`
`   160 `
`   176 `
`   161 lemma vector_mult_component:`
`   177 lemma vector_mult_component [simp]:`
`   162   fixes x y :: "'a::{times} ^ 'n"  assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}"`
`   178   fixes x y :: "'a::{times} ^ 'n"`
`   163   shows "(x * y)\$i = x\$i * y\$i"`
`   179   shows "(x * y)\$i = x\$i * y\$i"`
`   164   using i by vector`
`   180   by vector`
`   165 `
`   181 `
`   166 lemma vector_smult_component:`
`   182 lemma vector_smult_component [simp]:`
`   167   fixes y :: "'a::{times} ^ 'n"  assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}"`
`   183   fixes y :: "'a::{times} ^ 'n"`
`   168   shows "(c *s y)\$i = c * (y\$i)"`
`   184   shows "(c *s y)\$i = c * (y\$i)"`
`   169   using i by vector`
`   185   by vector`
`   170 `
`   186 `
`   171 lemma vector_uminus_component:`
`   187 lemma vector_uminus_component [simp]:`
`   172   fixes x :: "'a::{uminus} ^ 'n"  assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}"`
`   188   fixes x :: "'a::{uminus} ^ 'n"`
`   173   shows "(- x)\$i = - (x\$i)"`
`   189   shows "(- x)\$i = - (x\$i)"`
`   174   using i by vector`
`   190   by vector`
`   175 `
`   191 `
`   176 lemma vector_scaleR_component:`
`   192 lemma vector_scaleR_component [simp]:`
`   177   fixes x :: "'a::scaleR ^ 'n"`
`   193   fixes x :: "'a::scaleR ^ 'n"`
`   179   shows "(scaleR r x)\$i = scaleR r (x\$i)"`
`   194   shows "(scaleR r x)\$i = scaleR r (x\$i)"`
`   180   using i by vector`
`   195   by vector`
`   181 `
`   196 `
`   182 lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector`
`   197 lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector`
`   183 `
`   198 `
`   184 lemmas vector_component =`
`   199 lemmas vector_component =`
`   185   vec_component vector_add_component vector_mult_component`
`   200   vec_component vector_add_component vector_mult_component`
`   248   apply (intro_classes) by (vector ring_simps)+`
`   263   apply (intro_classes) by (vector ring_simps)+`
`   249 `
`   264 `
`   250 instance "^" :: (semiring_0,type) semiring_0`
`   265 instance "^" :: (semiring_0,type) semiring_0`
`   251   apply (intro_classes) by (vector ring_simps)+`
`   266   apply (intro_classes) by (vector ring_simps)+`
`   252 instance "^" :: (semiring_1,type) semiring_1`
`   267 instance "^" :: (semiring_1,type) semiring_1`
`   253   apply (intro_classes) apply vector using dimindex_ge_1 by auto`
`   268   apply (intro_classes) by vector`
`   254 instance "^" :: (comm_semiring,type) comm_semiring`
`   269 instance "^" :: (comm_semiring,type) comm_semiring`
`   255   apply (intro_classes) by (vector ring_simps)+`
`   270   apply (intro_classes) by (vector ring_simps)+`
`   256 `
`   271 `
`   257 instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes)`
`   272 instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes)`
`   258 instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add ..`
`   273 instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add ..`
`   272   done`
`   287   done`
`   273 `
`   288 `
`   274 instance "^" :: (real_algebra_1,type) real_algebra_1 ..`
`   289 instance "^" :: (real_algebra_1,type) real_algebra_1 ..`
`   275 `
`   290 `
`   276 lemma of_nat_index:`
`   291 lemma of_nat_index:`
`   277   "i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n"`
`   292   "(of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n"`
`   278   apply (induct n)`
`   293   apply (induct n)`
`   279   apply vector`
`   294   apply vector`
`   280   apply vector`
`   295   apply vector`
`   281   done`
`   296   done`
`   282 lemma zero_index[simp]:`
`   297 lemma zero_index[simp]:`
`   283   "i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (0 :: 'a::zero ^'n)\$i = 0" by vector`
`   298   "(0 :: 'a::zero ^'n)\$i = 0" by vector`
`   284 `
`   299 `
`   285 lemma one_index[simp]:`
`   300 lemma one_index[simp]:`
`   286   "i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (1 :: 'a::one ^'n)\$i = 1" by vector`
`   301   "(1 :: 'a::one ^'n)\$i = 1" by vector`
`   287 `
`   302 `
`   288 lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \<noteq> 0"`
`   303 lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \<noteq> 0"`
`   289 proof-`
`   304 proof-`
`   290   have "(1::'a) + of_nat n = 0 \<longleftrightarrow> of_nat 1 + of_nat n = (of_nat 0 :: 'a)" by simp`
`   305   have "(1::'a) + of_nat n = 0 \<longleftrightarrow> of_nat 1 + of_nat n = (of_nat 0 :: 'a)" by simp`
`   291   also have "\<dots> \<longleftrightarrow> 1 + n = 0" by (simp only: of_nat_add[symmetric] of_nat_eq_iff)`
`   306   also have "\<dots> \<longleftrightarrow> 1 + n = 0" by (simp only: of_nat_add[symmetric] of_nat_eq_iff)`
`   294 `
`   309 `
`   295 instance "^" :: (semiring_char_0,type) semiring_char_0`
`   310 instance "^" :: (semiring_char_0,type) semiring_char_0`
`   296 proof (intro_classes)`
`   311 proof (intro_classes)`
`   297   fix m n ::nat`
`   312   fix m n ::nat`
`   298   show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"`
`   313   show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"`
`   299   proof(induct m arbitrary: n)`
`   314     by (simp add: Cart_eq of_nat_index)`
`   300     case 0 thus ?case apply vector`
`       `
`   301       apply (induct n,auto simp add: ring_simps)`
`       `
`   302       using dimindex_ge_1 apply auto`
`       `
`   303       apply vector`
`       `
`   304       by (auto simp add: of_nat_index one_plus_of_nat_neq_0)`
`       `
`   305   next`
`       `
`   306     case (Suc n m)`
`       `
`   307     thus ?case  apply vector`
`       `
`   308       apply (induct m, auto simp add: ring_simps of_nat_index zero_index)`
`       `
`   309       using dimindex_ge_1 apply simp apply blast`
`       `
`   310       apply (simp add: one_plus_of_nat_neq_0)`
`       `
`   311       using dimindex_ge_1 apply simp apply blast`
`       `
`   312       apply (simp add: vector_component one_index of_nat_index)`
`       `
`   313       apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff)`
`       `
`   314       using  dimindex_ge_1 apply simp apply blast`
`       `
`   315       apply (simp add: vector_component one_index of_nat_index)`
`       `
`   316       apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff)`
`       `
`   317       using dimindex_ge_1 apply simp apply blast`
`       `
`   318       apply (simp add: vector_component one_index of_nat_index)`
`       `
`   319       done`
`       `
`   320   qed`
`       `
`   321 qed`
`   315 qed`
`   322 `
`   316 `
`   323 instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes`
`   317 instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes`
`   324 instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes`
`   318 instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes`
`   325 `
`   319 `
`   339 lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector`
`   333 lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector`
`   340 lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"`
`   334 lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"`
`   341   by (vector ring_simps)`
`   335   by (vector ring_simps)`
`   342 `
`   336 `
`   343 lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"`
`   337 lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"`
`   344   apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta )`
`   338   by (simp add: Cart_eq)`
`   345   using dimindex_ge_1 apply auto done`
`       `
`   346 `
`   339 `
`   347 subsection {* Square root of sum of squares *}`
`   340 subsection {* Square root of sum of squares *}`
`   348 `
`   341 `
`   349 definition`
`   342 definition`
`   350   "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"`
`   343   "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"`
`   511   apply simp`
`   504   apply simp`
`   512   done`
`   505   done`
`   513 `
`   506 `
`   514 subsection {* Norms *}`
`   507 subsection {* Norms *}`
`   515 `
`   508 `
`   516 instantiation "^" :: (real_normed_vector, type) real_normed_vector`
`   509 instantiation "^" :: (real_normed_vector, finite) real_normed_vector`
`   517 begin`
`   510 begin`
`   518 `
`   511 `
`   519 definition vector_norm_def:`
`   512 definition vector_norm_def:`
`   520   "norm (x::'a^'b) = setL2 (\<lambda>i. norm (x\$i)) {1 .. dimindex (UNIV:: 'b set)}"`
`   513   "norm (x::'a^'b) = setL2 (\<lambda>i. norm (x\$i)) UNIV"`
`   521 `
`   514 `
`   522 definition vector_sgn_def:`
`   515 definition vector_sgn_def:`
`   523   "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"`
`   516   "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"`
`   524 `
`   517 `
`   525 instance proof`
`   518 instance proof`
`   531     unfolding vector_norm_def`
`   524     unfolding vector_norm_def`
`   532     by (simp add: setL2_eq_0_iff Cart_eq)`
`   525     by (simp add: setL2_eq_0_iff Cart_eq)`
`   533   show "norm (x + y) \<le> norm x + norm y"`
`   526   show "norm (x + y) \<le> norm x + norm y"`
`   534     unfolding vector_norm_def`
`   527     unfolding vector_norm_def`
`   535     apply (rule order_trans [OF _ setL2_triangle_ineq])`
`   528     apply (rule order_trans [OF _ setL2_triangle_ineq])`
`   536     apply (rule setL2_mono)`
`   529     apply (simp add: setL2_mono norm_triangle_ineq)`
`   537     apply (simp add: vector_component norm_triangle_ineq)`
`       `
`   538     apply simp`
`       `
`   539     done`
`   530     done`
`   540   show "norm (scaleR a x) = \<bar>a\<bar> * norm x"`
`   531   show "norm (scaleR a x) = \<bar>a\<bar> * norm x"`
`   541     unfolding vector_norm_def`
`   532     unfolding vector_norm_def`
`   542     by (simp add: vector_component norm_scaleR setL2_right_distrib`
`   533     by (simp add: norm_scaleR setL2_right_distrib)`
`   543              cong: strong_setL2_cong)`
`       `
`   544   show "sgn x = scaleR (inverse (norm x)) x"`
`   534   show "sgn x = scaleR (inverse (norm x)) x"`
`   545     by (rule vector_sgn_def)`
`   535     by (rule vector_sgn_def)`
`   546 qed`
`   536 qed`
`   547 `
`   537 `
`   548 end`
`   538 end`
`   549 `
`   539 `
`   550 subsection {* Inner products *}`
`   540 subsection {* Inner products *}`
`   551 `
`   541 `
`   552 instantiation "^" :: (real_inner, type) real_inner`
`   542 instantiation "^" :: (real_inner, finite) real_inner`
`   553 begin`
`   543 begin`
`   554 `
`   544 `
`   555 definition vector_inner_def:`
`   545 definition vector_inner_def:`
`   556   "inner x y = setsum (\<lambda>i. inner (x\$i) (y\$i)) {1 .. dimindex(UNIV::'b set)}"`
`   546   "inner x y = setsum (\<lambda>i. inner (x\$i) (y\$i)) UNIV"`
`   557 `
`   547 `
`   558 instance proof`
`   548 instance proof`
`   559   fix r :: real and x y z :: "'a ^ 'b"`
`   549   fix r :: real and x y z :: "'a ^ 'b"`
`   560   show "inner x y = inner y x"`
`   550   show "inner x y = inner y x"`
`   561     unfolding vector_inner_def`
`   551     unfolding vector_inner_def`
`   562     by (simp add: inner_commute)`
`   552     by (simp add: inner_commute)`
`   563   show "inner (x + y) z = inner x z + inner y z"`
`   553   show "inner (x + y) z = inner x z + inner y z"`
`   564     unfolding vector_inner_def`
`   554     unfolding vector_inner_def`
`   565     by (vector inner_left_distrib)`
`   555     by (simp add: inner_left_distrib setsum_addf)`
`   566   show "inner (scaleR r x) y = r * inner x y"`
`   556   show "inner (scaleR r x) y = r * inner x y"`
`   567     unfolding vector_inner_def`
`   557     unfolding vector_inner_def`
`   568     by (vector inner_scaleR_left)`
`   558     by (simp add: inner_scaleR_left setsum_right_distrib)`
`   569   show "0 \<le> inner x x"`
`   559   show "0 \<le> inner x x"`
`   570     unfolding vector_inner_def`
`   560     unfolding vector_inner_def`
`   571     by (simp add: setsum_nonneg)`
`   561     by (simp add: setsum_nonneg)`
`   572   show "inner x x = 0 \<longleftrightarrow> x = 0"`
`   562   show "inner x x = 0 \<longleftrightarrow> x = 0"`
`   573     unfolding vector_inner_def`
`   563     unfolding vector_inner_def`
`   611   have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis`
`   601   have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis`
`   612   from sum_nonneg_eq_zero_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)`
`   602   from sum_nonneg_eq_zero_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)`
`   613   show ?case by (simp add: h)`
`   603   show ?case by (simp add: h)`
`   614 qed`
`   604 qed`
`   615 `
`   605 `
`   616 lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0"`
`   606 lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) = 0"`
`   617 proof-`
`   607   by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq)`
`   618   {assume f: "finite (UNIV :: 'n set)"`
`   608 `
`   619     let ?S = "{Suc 0 .. card (UNIV :: 'n set)}"`
`   609 lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]`
`   620     have fS: "finite ?S" using f by simp`
`       `
`   621     have fp: "\<forall> i\<in> ?S. x\$i * x\$i>= 0" by simp`
`       `
`   622     have ?thesis by (vector dimindex_def f setsum_squares_eq_0_iff[OF fS fp])}`
`       `
`   623   moreover`
`       `
`   624   {assume "\<not> finite (UNIV :: 'n set)" then have ?thesis by (vector dimindex_def)}`
`       `
`   625   ultimately show ?thesis by metis`
`       `
`   626 qed`
`       `
`   627 `
`       `
`   628 lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]`
`       `
`   629   by (auto simp add: le_less)`
`   610   by (auto simp add: le_less)`
`   630 `
`   611 `
`   631 subsection{* The collapse of the general concepts to dimension one. *}`
`   612 subsection{* The collapse of the general concepts to dimension one. *}`
`   632 `
`   613 `
`   633 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x\$1))"`
`   614 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x\$1))"`
`   634   by (vector dimindex_def)`
`   615   by (simp add: Cart_eq forall_1)`
`   635 `
`   616 `
`   636 lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"`
`   617 lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"`
`   637   apply auto`
`   618   apply auto`
`   638   apply (erule_tac x= "x\$1" in allE)`
`   619   apply (erule_tac x= "x\$1" in allE)`
`   639   apply (simp only: vector_one[symmetric])`
`   620   apply (simp only: vector_one[symmetric])`
`   640   done`
`   621   done`
`   641 `
`   622 `
`   642 lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)"`
`   623 lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)"`
`   643   by (simp add: vector_norm_def dimindex_def)`
`   624   by (simp add: vector_norm_def UNIV_1)`
`   644 `
`   625 `
`   645 lemma norm_real: "norm(x::real ^ 1) = abs(x\$1)"`
`   626 lemma norm_real: "norm(x::real ^ 1) = abs(x\$1)"`
`   646   by (simp add: norm_vector_1)`
`   627   by (simp add: norm_vector_1)`
`   647 `
`   628 `
`   648 text{* Metric *}`
`   629 text{* Metric *}`
`   649 `
`   630 `
`   650 text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *}`
`   631 text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *}`
`   651 definition dist:: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real" where`
`   632 definition dist:: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real" where`
`   652   "dist x y = norm (x - y)"`
`   633   "dist x y = norm (x - y)"`
`   653 `
`   634 `
`   654 lemma dist_real: "dist(x::real ^ 1) y = abs((x\$1) - (y\$1))"`
`   635 lemma dist_real: "dist(x::real ^ 1) y = abs((x\$1) - (y\$1))"`
`   655   using dimindex_ge_1[of "UNIV :: 1 set"]`
`   636   by (auto simp add: norm_real dist_def)`
`   656   by (auto simp add: norm_real dist_def vector_component Cart_lambda_beta[where ?'a = "1"] )`
`       `
`   657 `
`   637 `
`   658 subsection {* A connectedness or intermediate value lemma with several applications. *}`
`   638 subsection {* A connectedness or intermediate value lemma with several applications. *}`
`   659 `
`   639 `
`   660 lemma connected_real_lemma:`
`   640 lemma connected_real_lemma:`
`   661   fixes f :: "real \<Rightarrow> real ^ 'n"`
`   641   fixes f :: "real \<Rightarrow> real ^ 'n::finite"`
`   662   assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"`
`   642   assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"`
`   663   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"`
`   643   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"`
`   664   and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"`
`   644   and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"`
`   665   and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"`
`   645   and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"`
`   666   and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"`
`   646   and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"`
`   756   apply (simp add: inverse_eq_divide real_sqrt_ge_0_iff field_simps)`
`   736   apply (simp add: inverse_eq_divide real_sqrt_ge_0_iff field_simps)`
`   757   done`
`   737   done`
`   758 `
`   738 `
`   759 text{* Hence derive more interesting properties of the norm. *}`
`   739 text{* Hence derive more interesting properties of the norm. *}`
`   760 `
`   740 `
`   761 lemma norm_0[simp]: "norm (0::real ^ 'n) = 0"`
`   741 text {*`
`       `
`   742   This type-specific version is only here`
`       `
`   743   to make @{text normarith.ML} happy.`
`       `
`   744 *}`
`       `
`   745 lemma norm_0: "norm (0::real ^ _) = 0"`
`   762   by (rule norm_zero)`
`   746   by (rule norm_zero)`
`   763 `
`   747 `
`   764 lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"`
`   748 lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"`
`   765   by (simp add: vector_norm_def vector_component setL2_right_distrib`
`   749   by (simp add: vector_norm_def vector_component setL2_right_distrib`
`   766            abs_mult cong: strong_setL2_cong)`
`   750            abs_mult cong: strong_setL2_cong)`
`   768   by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)`
`   752   by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)`
`   769 lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"`
`   753 lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"`
`   770   by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)`
`   754   by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)`
`   771 lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"`
`   755 lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"`
`   772   by (simp add: real_vector_norm_def)`
`   756   by (simp add: real_vector_norm_def)`
`   773 lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)`
`   757 lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n::finite)" by (metis norm_eq_zero)`
`   774 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"`
`   758 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"`
`   775   by vector`
`   759   by vector`
`   776 lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"`
`   760 lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"`
`   777   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)`
`   761   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)`
`   778 lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"`
`   762 lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"`
`   779   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)`
`   763   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)`
`   780 lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"`
`   764 lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"`
`   781   by (metis vector_mul_lcancel)`
`   765   by (metis vector_mul_lcancel)`
`   782 lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"`
`   766 lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"`
`   783   by (metis vector_mul_rcancel)`
`   767   by (metis vector_mul_rcancel)`
`   784 lemma norm_cauchy_schwarz: "x \<bullet> y <= norm x * norm y"`
`   768 lemma norm_cauchy_schwarz:`
`       `
`   769   fixes x y :: "real ^ 'n::finite"`
`       `
`   770   shows "x \<bullet> y <= norm x * norm y"`
`   785 proof-`
`   771 proof-`
`   786   {assume "norm x = 0"`
`   772   {assume "norm x = 0"`
`   787     hence ?thesis by (simp add: dot_lzero dot_rzero)}`
`   773     hence ?thesis by (simp add: dot_lzero dot_rzero)}`
`   788   moreover`
`   774   moreover`
`   789   {assume "norm y = 0"`
`   775   {assume "norm y = 0"`
`   800       by (simp add: field_simps)`
`   786       by (simp add: field_simps)`
`   801     hence ?thesis using h by (simp add: power2_eq_square)}`
`   787     hence ?thesis using h by (simp add: power2_eq_square)}`
`   802   ultimately show ?thesis by metis`
`   788   ultimately show ?thesis by metis`
`   803 qed`
`   789 qed`
`   804 `
`   790 `
`   805 lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"`
`   791 lemma norm_cauchy_schwarz_abs:`
`       `
`   792   fixes x y :: "real ^ 'n::finite"`
`       `
`   793   shows "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"`
`   806   using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]`
`   794   using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]`
`   807   by (simp add: real_abs_def dot_rneg)`
`   795   by (simp add: real_abs_def dot_rneg)`
`   808 `
`   796 `
`   809 lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)"`
`   797 lemma norm_triangle_sub: "norm (x::real ^'n::finite) <= norm(y) + norm(x - y)"`
`   810   using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)`
`   798   using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)`
`   811 lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e"`
`   799 lemma norm_triangle_le: "norm(x::real ^'n::finite) + norm y <= e ==> norm(x + y) <= e"`
`   812   by (metis order_trans norm_triangle_ineq)`
`   800   by (metis order_trans norm_triangle_ineq)`
`   813 lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e"`
`   801 lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e"`
`   814   by (metis basic_trans_rules(21) norm_triangle_ineq)`
`   802   by (metis basic_trans_rules(21) norm_triangle_ineq)`
`   815 `
`   803 `
`   816 lemma component_le_norm: "i \<in> {1 .. dimindex(UNIV :: 'n set)} ==> \<bar>x\$i\<bar> <= norm (x::real ^ 'n)"`
`   804 lemma setsum_delta:`
`       `
`   805   assumes fS: "finite S"`
`       `
`   806   shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"`
`       `
`   807 proof-`
`       `
`   808   let ?f = "(\<lambda>k. if k=a then b k else 0)"`
`       `
`   809   {assume a: "a \<notin> S"`
`       `
`   810     hence "\<forall> k\<in> S. ?f k = 0" by simp`
`       `
`   811     hence ?thesis  using a by simp}`
`       `
`   812   moreover`
`       `
`   813   {assume a: "a \<in> S"`
`       `
`   814     let ?A = "S - {a}"`
`       `
`   815     let ?B = "{a}"`
`       `
`   816     have eq: "S = ?A \<union> ?B" using a by blast`
`       `
`   817     have dj: "?A \<inter> ?B = {}" by simp`
`       `
`   818     from fS have fAB: "finite ?A" "finite ?B" by auto`
`       `
`   819     have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"`
`       `
`   820       using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]`
`       `
`   821       by simp`
`       `
`   822     then have ?thesis  using a by simp}`
`       `
`   823   ultimately show ?thesis by blast`
`       `
`   824 qed`
`       `
`   825 `
`       `
`   826 lemma component_le_norm: "\<bar>x\$i\<bar> <= norm (x::real ^ 'n::finite)"`
`   817   apply (simp add: vector_norm_def)`
`   827   apply (simp add: vector_norm_def)`
`   818   apply (rule member_le_setL2, simp_all)`
`   828   apply (rule member_le_setL2, simp_all)`
`   819   done`
`   829   done`
`   820 `
`   830 `
`   821 lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e`
`   831 lemma norm_bound_component_le: "norm(x::real ^ 'n::finite) <= e`
`   822                 ==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x\$i\<bar> <= e"`
`   832                 ==> \<bar>x\$i\<bar> <= e"`
`   823   by (metis component_le_norm order_trans)`
`   833   by (metis component_le_norm order_trans)`
`   824 `
`   834 `
`   825 lemma norm_bound_component_lt: "norm(x::real ^ 'n) < e`
`   835 lemma norm_bound_component_lt: "norm(x::real ^ 'n::finite) < e`
`   826                 ==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x\$i\<bar> < e"`
`   836                 ==> \<bar>x\$i\<bar> < e"`
`   827   by (metis component_le_norm basic_trans_rules(21))`
`   837   by (metis component_le_norm basic_trans_rules(21))`
`   828 `
`   838 `
`   829 lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\<lambda>i. \<bar>x\$i\<bar>) {1..dimindex(UNIV::'n set)}"`
`   839 lemma norm_le_l1: "norm (x:: real ^'n::finite) <= setsum(\<lambda>i. \<bar>x\$i\<bar>) UNIV"`
`   830   by (simp add: vector_norm_def setL2_le_setsum)`
`   840   by (simp add: vector_norm_def setL2_le_setsum)`
`   831 `
`   841 `
`   832 lemma real_abs_norm[simp]: "\<bar> norm x\<bar> = norm (x :: real ^'n)"`
`   842 lemma real_abs_norm: "\<bar>norm x\<bar> = norm (x :: real ^ _)"`
`   833   by (rule abs_norm_cancel)`
`   843   by (rule abs_norm_cancel)`
`   834 lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n) - norm y\<bar> <= norm(x - y)"`
`   844 lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n::finite) - norm y\<bar> <= norm(x - y)"`
`   835   by (rule norm_triangle_ineq3)`
`   845   by (rule norm_triangle_ineq3)`
`   836 lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"`
`   846 lemma norm_le: "norm(x::real ^ _) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"`
`   837   by (simp add: real_vector_norm_def)`
`   847   by (simp add: real_vector_norm_def)`
`   838 lemma norm_lt: "norm(x::real ^'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"`
`   848 lemma norm_lt: "norm(x::real ^ _) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"`
`   839   by (simp add: real_vector_norm_def)`
`   849   by (simp add: real_vector_norm_def)`
`   840 lemma norm_eq: "norm (x::real ^'n) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"`
`   850 lemma norm_eq: "norm (x::real ^ _) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"`
`   841   by (simp add: order_eq_iff norm_le)`
`   851   by (simp add: order_eq_iff norm_le)`
`   842 lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \<longleftrightarrow> x \<bullet> x = 1"`
`   852 lemma norm_eq_1: "norm(x::real ^ _) = 1 \<longleftrightarrow> x \<bullet> x = 1"`
`   843   by (simp add: real_vector_norm_def)`
`   853   by (simp add: real_vector_norm_def)`
`   844 `
`   854 `
`   845 text{* Squaring equations and inequalities involving norms.  *}`
`   855 text{* Squaring equations and inequalities involving norms.  *}`
`   846 `
`   856 `
`   847 lemma dot_square_norm: "x \<bullet> x = norm(x)^2"`
`   857 lemma dot_square_norm: "x \<bullet> x = norm(x)^2"`
`   848   by (simp add: real_vector_norm_def  dot_pos_le )`
`   858   by (simp add: real_vector_norm_def)`
`   849 `
`   859 `
`   850 lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"`
`   860 lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"`
`   851   by (auto simp add: real_vector_norm_def)`
`   861   by (auto simp add: real_vector_norm_def)`
`   852 `
`   862 `
`   853 lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"`
`   863 lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"`
`   883   by (simp add: norm_pow_2 dot_ladd dot_radd dot_lsub dot_rsub dot_sym)`
`   893   by (simp add: norm_pow_2 dot_ladd dot_radd dot_lsub dot_rsub dot_sym)`
`   884 `
`   894 `
`   885 `
`   895 `
`   886 text{* Equality of vectors in terms of @{term "op \<bullet>"} products.    *}`
`   896 text{* Equality of vectors in terms of @{term "op \<bullet>"} products.    *}`
`   887 `
`   897 `
`   888 lemma vector_eq: "(x:: real ^ 'n) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs")`
`   898 lemma vector_eq: "(x:: real ^ 'n::finite) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs")`
`   889 proof`
`   899 proof`
`   890   assume "?lhs" then show ?rhs by simp`
`   900   assume "?lhs" then show ?rhs by simp`
`   891 next`
`   901 next`
`   892   assume ?rhs`
`   902   assume ?rhs`
`   893   then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y\<bullet> y = 0" by simp`
`   903   then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y\<bullet> y = 0" by simp`
`   905   apply (rule mult_mono1)`
`   915   apply (rule mult_mono1)`
`   906   apply simp_all`
`   916   apply simp_all`
`   907   done`
`   917   done`
`   908 `
`   918 `
`   909   (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)`
`   919   (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)`
`   910 lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)"`
`   920 lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n::finite) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)"`
`   911   apply (rule norm_triangle_le) by simp`
`   921   apply (rule norm_triangle_le) by simp`
`   912 `
`   922 `
`   913 lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \<ge> b == a - b \<ge> 0"`
`   923 lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \<ge> b == a - b \<ge> 0"`
`   914   by (simp add: ring_simps)`
`   924   by (simp add: ring_simps)`
`   915 `
`   925 `
`   934   "(c *s x + z) + d *s y == d *s y + (c *s x + z)"`
`   944   "(c *s x + z) + d *s y == d *s y + (c *s x + z)"`
`   935   "c *s x + (d *s y + z) == d *s y + (c *s x + z)"`
`   945   "c *s x + (d *s y + z) == d *s y + (c *s x + z)"`
`   936   "(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+`
`   946   "(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+`
`   937 lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector`
`   947 lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector`
`   938 `
`   948 `
`   939 lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"`
`   949 lemma norm_imp_pos_and_ge: "norm (x::real ^ _) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"`
`   940   by (atomize) (auto simp add: norm_ge_zero)`
`   950   by (atomize) (auto simp add: norm_ge_zero)`
`   941 `
`   951 `
`   942 lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith`
`   952 lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith`
`   943 `
`   953 `
`   944 lemma norm_pths:`
`   954 lemma norm_pths:`
`   945   "(x::real ^'n) = y \<longleftrightarrow> norm (x - y) \<le> 0"`
`   955   "(x::real ^'n::finite) = y \<longleftrightarrow> norm (x - y) \<le> 0"`
`   946   "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"`
`   956   "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"`
`   947   using norm_ge_zero[of "x - y"] by auto`
`   957   using norm_ge_zero[of "x - y"] by auto`
`   948 `
`   958 `
`   949 use "normarith.ML"`
`   959 use "normarith.ML"`
`   950 `
`   960 `
`   986 `
`   996 `
`   987 lemma dist_triangle_add_half: " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm`
`   997 lemma dist_triangle_add_half: " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm`
`   988 `
`   998 `
`   989 lemma dist_le_0[simp]: "dist x y <= 0 \<longleftrightarrow> x = y" by norm`
`   999 lemma dist_le_0[simp]: "dist x y <= 0 \<longleftrightarrow> x = y" by norm`
`   990 `
`  1000 `
`       `
`  1001 lemma setsum_component [simp]:`
`       `
`  1002   fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"`
`       `
`  1003   shows "(setsum f S)\$i = setsum (\<lambda>x. (f x)\$i) S"`
`       `
`  1004   by (cases "finite S", induct S set: finite, simp_all)`
`       `
`  1005 `
`   991 lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)\$i ) S)"`
`  1006 lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)\$i ) S)"`
`   992   apply vector`
`  1007   by (simp add: Cart_eq)`
`   993   apply auto`
`       `
`   994   apply (cases "finite S")`
`       `
`   995   apply (rule finite_induct[of S])`
`       `
`   996   apply (auto simp add: vector_component zero_index)`
`       `
`   997   done`
`       `
`   998 `
`  1008 `
`   999 lemma setsum_clauses:`
`  1009 lemma setsum_clauses:`
`  1000   shows "setsum f {} = 0"`
`  1010   shows "setsum f {} = 0"`
`  1001   and "finite S \<Longrightarrow> setsum f (insert x S) =`
`  1011   and "finite S \<Longrightarrow> setsum f (insert x S) =`
`  1002                  (if x \<in> S then setsum f S else f x + setsum f S)"`
`  1012                  (if x \<in> S then setsum f S else f x + setsum f S)"`
`  1003   by (auto simp add: insert_absorb)`
`  1013   by (auto simp add: insert_absorb)`
`  1004 `
`  1014 `
`  1005 lemma setsum_cmul:`
`  1015 lemma setsum_cmul:`
`  1006   fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"`
`  1016   fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"`
`  1007   shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"`
`  1017   shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"`
`  1008   by (simp add: setsum_eq Cart_eq Cart_lambda_beta vector_component setsum_right_distrib)`
`  1018   by (simp add: Cart_eq setsum_right_distrib)`
`  1009 `
`       `
`  1010 lemma setsum_component:`
`       `
`  1011   fixes f:: " 'a \<Rightarrow> ('b::semiring_1) ^'n"`
`       `
`  1012   assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}"`
`       `
`  1013   shows "(setsum f S)\$i = setsum (\<lambda>x. (f x)\$i) S"`
`       `
`  1014   using i by (simp add: setsum_eq Cart_lambda_beta)`
`       `
`  1015 `
`  1019 `
`  1016 lemma setsum_norm:`
`  1020 lemma setsum_norm:`
`  1017   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"`
`  1021   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"`
`  1018   assumes fS: "finite S"`
`  1022   assumes fS: "finite S"`
`  1019   shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"`
`  1023   shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"`
`  1026     using "2.hyps" by simp`
`  1030     using "2.hyps" by simp`
`  1027   finally  show ?case  using "2.hyps" by simp`
`  1031   finally  show ?case  using "2.hyps" by simp`
`  1028 qed`
`  1032 qed`
`  1029 `
`  1033 `
`  1030 lemma real_setsum_norm:`
`  1034 lemma real_setsum_norm:`
`  1031   fixes f :: "'a \<Rightarrow> real ^'n"`
`  1035   fixes f :: "'a \<Rightarrow> real ^'n::finite"`
`  1032   assumes fS: "finite S"`
`  1036   assumes fS: "finite S"`
`  1033   shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"`
`  1037   shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"`
`  1034 proof(induct rule: finite_induct[OF fS])`
`  1038 proof(induct rule: finite_induct[OF fS])`
`  1035   case 1 thus ?case by simp`
`  1039   case 1 thus ?case by simp`
`  1036 next`
`  1040 next`
`  1052   then show ?thesis using setsum_norm[OF fS, of f] fg`
`  1056   then show ?thesis using setsum_norm[OF fS, of f] fg`
`  1053     by arith`
`  1057     by arith`
`  1054 qed`
`  1058 qed`
`  1055 `
`  1059 `
`  1056 lemma real_setsum_norm_le:`
`  1060 lemma real_setsum_norm_le:`
`  1057   fixes f :: "'a \<Rightarrow> real ^ 'n"`
`  1061   fixes f :: "'a \<Rightarrow> real ^ 'n::finite"`
`  1058   assumes fS: "finite S"`
`  1062   assumes fS: "finite S"`
`  1059   and fg: "\<forall>x \<in> S. norm (f x) \<le> g x"`
`  1063   and fg: "\<forall>x \<in> S. norm (f x) \<le> g x"`
`  1060   shows "norm (setsum f S) \<le> setsum g S"`
`  1064   shows "norm (setsum f S) \<le> setsum g S"`
`  1061 proof-`
`  1065 proof-`
`  1062   from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S"`
`  1066   from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S"`
`  1072   shows "norm (setsum f S) \<le> of_nat (card S) * K"`
`  1076   shows "norm (setsum f S) \<le> of_nat (card S) * K"`
`  1073   using setsum_norm_le[OF fS K] setsum_constant[symmetric]`
`  1077   using setsum_norm_le[OF fS K] setsum_constant[symmetric]`
`  1074   by simp`
`  1078   by simp`
`  1075 `
`  1079 `
`  1076 lemma real_setsum_norm_bound:`
`  1080 lemma real_setsum_norm_bound:`
`  1077   fixes f :: "'a \<Rightarrow> real ^ 'n"`
`  1081   fixes f :: "'a \<Rightarrow> real ^ 'n::finite"`
`  1078   assumes fS: "finite S"`
`  1082   assumes fS: "finite S"`
`  1079   and K: "\<forall>x \<in> S. norm (f x) \<le> K"`
`  1083   and K: "\<forall>x \<in> S. norm (f x) \<le> K"`
`  1080   shows "norm (setsum f S) \<le> of_nat (card S) * K"`
`  1084   shows "norm (setsum f S) \<le> of_nat (card S) * K"`
`  1081   using real_setsum_norm_le[OF fS K] setsum_constant[symmetric]`
`  1085   using real_setsum_norm_le[OF fS K] setsum_constant[symmetric]`
`  1082   by simp`
`  1086   by simp`
`  1153 apply (subst setsum_image_gen[OF fS, of g f])`
`  1157 apply (subst setsum_image_gen[OF fS, of g f])`
`  1154 apply (rule setsum_mono_zero_right[OF fT fST])`
`  1158 apply (rule setsum_mono_zero_right[OF fT fST])`
`  1155 by (auto intro: setsum_0')`
`  1159 by (auto intro: setsum_0')`
`  1156 `
`  1160 `
`  1157 lemma vsum_norm_allsubsets_bound:`
`  1161 lemma vsum_norm_allsubsets_bound:`
`  1158   fixes f:: "'a \<Rightarrow> real ^'n"`
`  1162   fixes f:: "'a \<Rightarrow> real ^'n::finite"`
`  1159   assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"`
`  1163   assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"`
`  1160   shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real (dimindex(UNIV :: 'n set)) *  e"`
`  1164   shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"`
`  1161 proof-`
`  1165 proof-`
`  1162   let ?d = "real (dimindex (UNIV ::'n set))"`
`  1166   let ?d = "real CARD('n)"`
`  1163   let ?nf = "\<lambda>x. norm (f x)"`
`  1167   let ?nf = "\<lambda>x. norm (f x)"`
`  1164   let ?U = "{1 .. dimindex (UNIV :: 'n set)}"`
`  1168   let ?U = "UNIV :: 'n set"`
`  1165   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"`
`  1169   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"`
`  1166     by (rule setsum_commute)`
`  1170     by (rule setsum_commute)`
`  1167   have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def)`
`  1171   have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def)`
`  1168   have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x \$ i\<bar>) ?U) P"`
`  1172   have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x \$ i\<bar>) ?U) P"`
`  1169     apply (rule setsum_mono)`
`  1173     apply (rule setsum_mono)`
`  1176     let ?Pn = "{x. x \<in> P \<and> f x \$ i < 0}"`
`  1180     let ?Pn = "{x. x \<in> P \<and> f x \$ i < 0}"`
`  1177     have thp: "P = ?Pp \<union> ?Pn" by auto`
`  1181     have thp: "P = ?Pp \<union> ?Pn" by auto`
`  1178     have thp0: "?Pp \<inter> ?Pn ={}" by auto`
`  1182     have thp0: "?Pp \<inter> ?Pn ={}" by auto`
`  1179     have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+`
`  1183     have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+`
`  1180     have Ppe:"setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pp \<le> e"`
`  1184     have Ppe:"setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pp \<le> e"`
`  1181       using i component_le_norm[OF i, of "setsum (\<lambda>x. f x) ?Pp"]  fPs[OF PpP]`
`  1185       using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i]  fPs[OF PpP]`
`  1182       by (auto simp add: setsum_component intro: abs_le_D1)`
`  1186       by (auto intro: abs_le_D1)`
`  1183     have Pne: "setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pn \<le> e"`
`  1187     have Pne: "setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pn \<le> e"`
`  1184       using i component_le_norm[OF i, of "setsum (\<lambda>x. - f x) ?Pn"]  fPs[OF PnP]`
`  1188       using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i]  fPs[OF PnP]`
`  1185       by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1)`
`  1189       by (auto simp add: setsum_negf intro: abs_le_D1)`
`  1186     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"`
`  1190     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"`
`  1187       apply (subst thp)`
`  1191       apply (subst thp)`
`  1188       apply (rule setsum_Un_zero)`
`  1192       apply (rule setsum_Un_zero)`
`  1189       using fP thp0 by auto`
`  1193       using fP thp0 by auto`
`  1190     also have "\<dots> \<le> 2*e" using Pne Ppe by arith`
`  1194     also have "\<dots> \<le> 2*e" using Pne Ppe by arith`
`  1202 subsection{* Basis vectors in coordinate directions. *}`
`  1206 subsection{* Basis vectors in coordinate directions. *}`
`  1203 `
`  1207 `
`  1204 `
`  1208 `
`  1205 definition "basis k = (\<chi> i. if i = k then 1 else 0)"`
`  1209 definition "basis k = (\<chi> i. if i = k then 1 else 0)"`
`  1206 `
`  1210 `
`       `
`  1211 lemma basis_component [simp]: "basis k \$ i = (if k=i then 1 else 0)"`
`       `
`  1212   unfolding basis_def by simp`
`       `
`  1213 `
`  1207 lemma delta_mult_idempotent:`
`  1214 lemma delta_mult_idempotent:`
`  1208   "(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)`
`  1215   "(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)`
`  1209 `
`  1216 `
`  1210 lemma norm_basis:`
`  1217 lemma norm_basis:`
`  1211   assumes k: "k \<in> {1 .. dimindex (UNIV :: 'n set)}"`
`  1218   shows "norm (basis k :: real ^'n::finite) = 1"`
`  1212   shows "norm (basis k :: real ^'n) = 1"`
`       `
`  1213   using k`
`       `
`  1214   apply (simp add: basis_def real_vector_norm_def dot_def)`
`  1219   apply (simp add: basis_def real_vector_norm_def dot_def)`
`  1215   apply (vector delta_mult_idempotent)`
`  1220   apply (vector delta_mult_idempotent)`
`  1216   using setsum_delta[of "{1 .. dimindex (UNIV :: 'n set)}" "k" "\<lambda>k. 1::real"]`
`  1221   using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"]`
`  1217   apply auto`
`  1222   apply auto`
`  1218   done`
`  1223   done`
`  1219 `
`  1224 `
`  1220 lemma norm_basis_1: "norm(basis 1 :: real ^'n) = 1"`
`  1225 lemma norm_basis_1: "norm(basis 1 :: real ^'n::{finite,one}) = 1"`
`  1221   apply (simp add: basis_def real_vector_norm_def dot_def)`
`  1226   by (rule norm_basis)`
`  1222   apply (vector delta_mult_idempotent)`
`  1227 `
`  1223   using setsum_delta[of "{1 .. dimindex (UNIV :: 'n set)}" "1" "\<lambda>k. 1::real"] dimindex_nonzero[of "UNIV :: 'n set"]`
`  1228 lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n::finite). norm x = c"`
`  1224   apply auto`
`  1229   apply (rule exI[where x="c *s basis arbitrary"])`
`  1225   done`
`  1230   by (simp only: norm_mul norm_basis)`
`  1226 `
`       `
`  1227 lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n). norm x = c"`
`       `
`  1228   apply (rule exI[where x="c *s basis 1"])`
`       `
`  1229   by (simp only: norm_mul norm_basis_1)`
`       `
`  1230 `
`  1231 `
`  1231 lemma vector_choose_dist: assumes e: "0 <= e"`
`  1232 lemma vector_choose_dist: assumes e: "0 <= e"`
`  1232   shows "\<exists>(y::real^'n). dist x y = e"`
`  1233   shows "\<exists>(y::real^'n::finite). dist x y = e"`
`  1233 proof-`
`  1234 proof-`
`  1234   from vector_choose_size[OF e] obtain c:: "real ^'n"  where "norm c = e"`
`  1235   from vector_choose_size[OF e] obtain c:: "real ^'n"  where "norm c = e"`
`  1235     by blast`
`  1236     by blast`
`  1236   then have "dist x (x - c) = e" by (simp add: dist_def)`
`  1237   then have "dist x (x - c) = e" by (simp add: dist_def)`
`  1237   then show ?thesis by blast`
`  1238   then show ?thesis by blast`
`  1238 qed`
`  1239 qed`
`  1239 `
`  1240 `
`  1240 lemma basis_inj: "inj_on (basis :: nat \<Rightarrow> real ^'n) {1 .. dimindex (UNIV :: 'n set)}"`
`  1241 lemma basis_inj: "inj (basis :: 'n \<Rightarrow> real ^'n::finite)"`
`  1241   by (auto simp add: inj_on_def basis_def Cart_eq Cart_lambda_beta)`
`  1242   by (simp add: inj_on_def Cart_eq)`
`  1242 `
`       `
`  1243 lemma basis_component: "i \<in> {1 .. dimindex(UNIV:: 'n set)} ==> (basis k ::('a::semiring_1)^'n)\$i = (if k=i then 1 else 0)"`
`       `
`  1244   by (simp add: basis_def Cart_lambda_beta)`
`       `
`  1245 `
`  1243 `
`  1246 lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)"`
`  1244 lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)"`
`  1247   by auto`
`  1245   by auto`
`  1248 `
`  1246 `
`  1249 lemma basis_expansion:`
`  1247 lemma basis_expansion:`
`  1250   "setsum (\<lambda>i. (x\$i) *s basis i) {1 .. dimindex (UNIV :: 'n set)} = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _")`
`  1248   "setsum (\<lambda>i. (x\$i) *s basis i) UNIV = (x::('a::ring_1) ^'n::finite)" (is "?lhs = ?rhs" is "setsum ?f ?S = _")`
`  1251   by (auto simp add: Cart_eq basis_component[where ?'n = "'n"] setsum_component vector_component cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong)`
`  1249   by (auto simp add: Cart_eq cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong)`
`  1252 `
`  1250 `
`  1253 lemma basis_expansion_unique:`
`  1251 lemma basis_expansion_unique:`
`  1254   "setsum (\<lambda>i. f i *s basis i) {1 .. dimindex (UNIV :: 'n set)} = (x::('a::comm_ring_1) ^'n) \<longleftrightarrow> (\<forall>i\<in>{1 .. dimindex(UNIV:: 'n set)}. f i = x\$i)"`
`  1252   "setsum (\<lambda>i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n::finite) \<longleftrightarrow> (\<forall>i. f i = x\$i)"`
`  1255   by (simp add: Cart_eq setsum_component vector_component basis_component setsum_delta cond_value_iff cong del: if_weak_cong)`
`  1253   by (simp add: Cart_eq setsum_delta cond_value_iff cong del: if_weak_cong)`
`  1256 `
`  1254 `
`  1257 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"`
`  1255 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"`
`  1258   by auto`
`  1256   by auto`
`  1259 `
`  1257 `
`  1260 lemma dot_basis:`
`  1258 lemma dot_basis:`
`  1261   assumes i: "i \<in> {1 .. dimindex (UNIV :: 'n set)}"`
`  1259   shows "basis i \<bullet> x = x\$i" "x \<bullet> (basis i :: 'a^'n::finite) = (x\$i :: 'a::semiring_1)"`
`  1262   shows "basis i \<bullet> x = x\$i" "x \<bullet> (basis i :: 'a^'n) = (x\$i :: 'a::semiring_1)"`
`  1260   by (auto simp add: dot_def basis_def cond_application_beta  cond_value_iff setsum_delta cong del: if_weak_cong)`
`  1263   using i`
`  1261 `
`  1264   by (auto simp add: dot_def basis_def Cart_lambda_beta cond_application_beta  cond_value_iff setsum_delta cong del: if_weak_cong)`
`  1262 lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> False"`
`  1265 `
`  1263   by (auto simp add: Cart_eq)`
`  1266 lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> i \<notin> {1..dimindex(UNIV ::'n set)}"`
`       `
`  1267   by (auto simp add: Cart_eq basis_component zero_index)`
`       `
`  1268 `
`  1264 `
`  1269 lemma basis_nonzero:`
`  1265 lemma basis_nonzero:`
`  1271   shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)"`
`  1266   shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)"`
`  1272   using k by (simp add: basis_eq_0)`
`  1267   by (simp add: basis_eq_0)`
`  1273 `
`  1268 `
`  1274 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n)"`
`  1269 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n::finite)"`
`  1275   apply (auto simp add: Cart_eq dot_basis)`
`  1270   apply (auto simp add: Cart_eq dot_basis)`
`  1276   apply (erule_tac x="basis i" in allE)`
`  1271   apply (erule_tac x="basis i" in allE)`
`  1277   apply (simp add: dot_basis)`
`  1272   apply (simp add: dot_basis)`
`  1278   apply (subgoal_tac "y = z")`
`  1273   apply (subgoal_tac "y = z")`
`  1279   apply simp`
`  1274   apply simp`
`  1280   apply vector`
`  1275   apply (simp add: Cart_eq)`
`  1281   done`
`  1276   done`
`  1282 `
`  1277 `
`  1283 lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::'a::semiring_1^'n)"`
`  1278 lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::'a::semiring_1^'n::finite)"`
`  1284   apply (auto simp add: Cart_eq dot_basis)`
`  1279   apply (auto simp add: Cart_eq dot_basis)`
`  1285   apply (erule_tac x="basis i" in allE)`
`  1280   apply (erule_tac x="basis i" in allE)`
`  1286   apply (simp add: dot_basis)`
`  1281   apply (simp add: dot_basis)`
`  1287   apply (subgoal_tac "x = y")`
`  1282   apply (subgoal_tac "x = y")`
`  1288   apply simp`
`  1283   apply simp`
`  1289   apply vector`
`  1284   apply (simp add: Cart_eq)`
`  1290   done`
`  1285   done`
`  1291 `
`  1286 `
`  1292 subsection{* Orthogonality. *}`
`  1287 subsection{* Orthogonality. *}`
`  1293 `
`  1288 `
`  1294 definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)"`
`  1289 definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)"`
`  1295 `
`  1290 `
`  1296 lemma orthogonal_basis:`
`  1291 lemma orthogonal_basis:`
`  1297   assumes i:"i \<in> {1 .. dimindex(UNIV ::'n set)}"`
`  1292   shows "orthogonal (basis i :: 'a^'n::finite) x \<longleftrightarrow> x\$i = (0::'a::ring_1)"`
`  1298   shows "orthogonal (basis i :: 'a^'n) x \<longleftrightarrow> x\$i = (0::'a::ring_1)"`
`  1293   by (auto simp add: orthogonal_def dot_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong)`
`  1299   using i`
`       `
`  1300   by (auto simp add: orthogonal_def dot_def basis_def Cart_lambda_beta cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong)`
`       `
`  1301 `
`  1294 `
`  1302 lemma orthogonal_basis_basis:`
`  1295 lemma orthogonal_basis_basis:`
`  1303   assumes i:"i \<in> {1 .. dimindex(UNIV ::'n set)}"`
`  1296   shows "orthogonal (basis i :: 'a::ring_1^'n::finite) (basis j) \<longleftrightarrow> i \<noteq> j"`
`  1304   and j: "j \<in> {1 .. dimindex(UNIV ::'n set)}"`
`  1297   unfolding orthogonal_basis[of i] basis_component[of j] by simp`
`  1305   shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \<longleftrightarrow> i \<noteq> j"`
`       `
`  1306   unfolding orthogonal_basis[OF i] basis_component[OF i] by simp`
`       `
`  1307 `
`  1298 `
`  1308   (* FIXME : Maybe some of these require less than comm_ring, but not all*)`
`  1299   (* FIXME : Maybe some of these require less than comm_ring, but not all*)`
`  1309 lemma orthogonal_clauses:`
`  1300 lemma orthogonal_clauses:`
`  1310   "orthogonal a (0::'a::comm_ring ^'n)"`
`  1301   "orthogonal a (0::'a::comm_ring ^'n)"`
`  1311   "orthogonal a x ==> orthogonal a (c *s x)"`
`  1302   "orthogonal a x ==> orthogonal a (c *s x)"`
`  1324 lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \<longleftrightarrow> orthogonal y x"`
`  1315 lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \<longleftrightarrow> orthogonal y x"`
`  1325   by (simp add: orthogonal_def dot_sym)`
`  1316   by (simp add: orthogonal_def dot_sym)`
`  1326 `
`  1317 `
`  1327 subsection{* Explicit vector construction from lists. *}`
`  1318 subsection{* Explicit vector construction from lists. *}`
`  1328 `
`  1319 `
`  1329 lemma Cart_lambda_beta_1[simp]: "(Cart_lambda g)\$1 = g 1"`
`  1320 primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"`
`  1330   apply (rule Cart_lambda_beta[rule_format])`
`  1321 where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"`
`  1331   using dimindex_ge_1 apply auto done`
`  1322 `
`  1332 `
`  1323 lemma from_nat [simp]: "from_nat = of_nat"`
`  1333 lemma Cart_lambda_beta_1'[simp]: "(Cart_lambda g)\$(Suc 0) = g 1"`
`  1324 by (rule ext, induct_tac x, simp_all)`
`  1334   by (simp only: One_nat_def[symmetric] Cart_lambda_beta_1)`
`  1325 `
`  1335 `
`  1326 primrec`
`  1336 definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"`
`  1327   list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"`
`       `
`  1328 where`
`       `
`  1329   "list_fun n [] = (\<lambda>x. 0)"`
`       `
`  1330 | "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"`
`       `
`  1331 `
`       `
`  1332 definition "vector l = (\<chi> i. list_fun 1 l i)"`
`       `
`  1333 (*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)`
`  1337 `
`  1334 `
`  1338 lemma vector_1: "(vector[x]) \$1 = x"`
`  1335 lemma vector_1: "(vector[x]) \$1 = x"`
`  1339   using dimindex_ge_1`
`  1336   unfolding vector_def by simp`
`  1340   by (auto simp add: vector_def Cart_lambda_beta[rule_format])`
`       `
`  1341 lemma dimindex_2[simp]: "2 \<in> {1 .. dimindex (UNIV :: 2 set)}"`
`       `
`  1342   by (auto simp add: dimindex_def)`
`       `
`  1343 lemma dimindex_2'[simp]: "2 \<in> {Suc 0 .. dimindex (UNIV :: 2 set)}"`
`       `
`  1344   by (auto simp add: dimindex_def)`
`       `
`  1345 lemma dimindex_3[simp]: "2 \<in> {1 .. dimindex (UNIV :: 3 set)}" "3 \<in> {1 .. dimindex (UNIV :: 3 set)}"`
`       `
`  1346   by (auto simp add: dimindex_def)`
`       `
`  1347 `
`       `
`  1348 lemma dimindex_3'[simp]: "2 \<in> {Suc 0 .. dimindex (UNIV :: 3 set)}" "3 \<in> {Suc 0 .. dimindex (UNIV :: 3 set)}"`
`       `
`  1349   by (auto simp add: dimindex_def)`
`       `
`  1350 `
`  1337 `
`  1351 lemma vector_2:`
`  1338 lemma vector_2:`
`  1352  "(vector[x,y]) \$1 = x"`
`  1339  "(vector[x,y]) \$1 = x"`
`  1353  "(vector[x,y] :: 'a^2)\$2 = (y::'a::zero)"`
`  1340  "(vector[x,y] :: 'a^2)\$2 = (y::'a::zero)"`
`  1354   apply (simp add: vector_def)`
`  1341   unfolding vector_def by simp_all`
`  1355   using Cart_lambda_beta[rule_format, OF dimindex_2, of "\<lambda>i. if i \<le> length [x,y] then [x,y] ! (i - 1) else (0::'a)"]`
`       `
`  1356   apply (simp only: vector_def )`
`       `
`  1357   apply auto`
`       `
`  1358   done`
`       `
`  1359 `
`  1342 `
`  1360 lemma vector_3:`
`  1343 lemma vector_3:`
`  1361  "(vector [x,y,z] ::('a::zero)^3)\$1 = x"`
`  1344  "(vector [x,y,z] ::('a::zero)^3)\$1 = x"`
`  1362  "(vector [x,y,z] ::('a::zero)^3)\$2 = y"`
`  1345  "(vector [x,y,z] ::('a::zero)^3)\$2 = y"`
`  1363  "(vector [x,y,z] ::('a::zero)^3)\$3 = z"`
`  1346  "(vector [x,y,z] ::('a::zero)^3)\$3 = z"`
`  1364 apply (simp_all add: vector_def Cart_lambda_beta dimindex_3)`
`  1347   unfolding vector_def by simp_all`
`  1365   using Cart_lambda_beta[rule_format, OF dimindex_3(1), of "\<lambda>i. if i \<le> length [x,y,z] then [x,y,z] ! (i - 1) else (0::'a)"]   using Cart_lambda_beta[rule_format, OF dimindex_3(2), of "\<lambda>i. if i \<le> length [x,y,z] then [x,y,z] ! (i - 1) else (0::'a)"]`
`       `
`  1366   by simp_all`
`       `
`  1367 `
`  1348 `
`  1368 lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"`
`  1349 lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"`
`  1369   apply auto`
`  1350   apply auto`
`  1370   apply (erule_tac x="v\$1" in allE)`
`  1351   apply (erule_tac x="v\$1" in allE)`
`  1371   apply (subgoal_tac "vector [v\$1] = v")`
`  1352   apply (subgoal_tac "vector [v\$1] = v")`
`  1372   apply simp`
`  1353   apply simp`
`  1373   by (vector vector_def dimindex_def)`
`  1354   apply (vector vector_def)`
`       `
`  1355   apply (simp add: forall_1)`
`       `
`  1356   done`
`  1374 `
`  1357 `
`  1375 lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"`
`  1358 lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"`
`  1376   apply auto`
`  1359   apply auto`
`  1377   apply (erule_tac x="v\$1" in allE)`
`  1360   apply (erule_tac x="v\$1" in allE)`
`  1378   apply (erule_tac x="v\$2" in allE)`
`  1361   apply (erule_tac x="v\$2" in allE)`
`  1379   apply (subgoal_tac "vector [v\$1, v\$2] = v")`
`  1362   apply (subgoal_tac "vector [v\$1, v\$2] = v")`
`  1380   apply simp`
`  1363   apply simp`
`  1381   apply (vector vector_def dimindex_def)`
`  1364   apply (vector vector_def)`
`  1382   apply auto`
`  1365   apply (simp add: forall_2)`
`  1383   apply (subgoal_tac "i = 1 \<or> i =2", auto)`
`       `
`  1384   done`
`  1366   done`
`  1385 `
`  1367 `
`  1386 lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"`
`  1368 lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"`
`  1387   apply auto`
`  1369   apply auto`
`  1388   apply (erule_tac x="v\$1" in allE)`
`  1370   apply (erule_tac x="v\$1" in allE)`
`  1389   apply (erule_tac x="v\$2" in allE)`
`  1371   apply (erule_tac x="v\$2" in allE)`
`  1390   apply (erule_tac x="v\$3" in allE)`
`  1372   apply (erule_tac x="v\$3" in allE)`
`  1391   apply (subgoal_tac "vector [v\$1, v\$2, v\$3] = v")`
`  1373   apply (subgoal_tac "vector [v\$1, v\$2, v\$3] = v")`
`  1392   apply simp`
`  1374   apply simp`
`  1393   apply (vector vector_def dimindex_def)`
`  1375   apply (vector vector_def)`
`  1394   apply auto`
`  1376   apply (simp add: forall_3)`
`  1395   apply (subgoal_tac "i = 1 \<or> i =2 \<or> i = 3", auto)`
`       `
`  1396   done`
`  1377   done`
`  1397 `
`  1378 `
`  1398 subsection{* Linear functions. *}`
`  1379 subsection{* Linear functions. *}`
`  1399 `
`  1380 `
`  1400 definition "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *s x) = c *s f x)"`
`  1381 definition "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *s x) = c *s f x)"`
`  1401 `
`  1382 `
`  1402 lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. (c::'a::comm_semiring) *s f x)"`
`  1383 lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. (c::'a::comm_semiring) *s f x)"`
`  1403   by (vector linear_def Cart_eq Cart_lambda_beta[rule_format] ring_simps)`
`  1384   by (vector linear_def Cart_eq ring_simps)`
`  1404 `
`  1385 `
`  1405 lemma linear_compose_neg: "linear (f :: 'a ^'n \<Rightarrow> 'a::comm_ring ^'m) ==> linear (\<lambda>x. -(f(x)))" by (vector linear_def Cart_eq)`
`  1386 lemma linear_compose_neg: "linear (f :: 'a ^'n \<Rightarrow> 'a::comm_ring ^'m) ==> linear (\<lambda>x. -(f(x)))" by (vector linear_def Cart_eq)`
`  1406 `
`  1387 `
`  1407 lemma linear_compose_add: "linear (f :: 'a ^'n \<Rightarrow> 'a::semiring_1 ^'m) \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"`
`  1388 lemma linear_compose_add: "linear (f :: 'a ^'n \<Rightarrow> 'a::semiring_1 ^'m) \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"`
`  1408   by (vector linear_def Cart_eq ring_simps)`
`  1389   by (vector linear_def Cart_eq ring_simps)`
`  1424   apply (induct rule: finite_induct[OF fS])`
`  1405   apply (induct rule: finite_induct[OF fS])`
`  1425   by (auto simp add: linear_zero intro: linear_compose_add)`
`  1406   by (auto simp add: linear_zero intro: linear_compose_add)`
`  1426 `
`  1407 `
`  1427 lemma linear_vmul_component:`
`  1408 lemma linear_vmul_component:`
`  1428   fixes f:: "'a::semiring_1^'m \<Rightarrow> 'a^'n"`
`  1409   fixes f:: "'a::semiring_1^'m \<Rightarrow> 'a^'n"`
`  1429   assumes lf: "linear f" and k: "k \<in> {1 .. dimindex (UNIV :: 'n set)}"`
`  1410   assumes lf: "linear f"`
`  1430   shows "linear (\<lambda>x. f x \$ k *s v)"`
`  1411   shows "linear (\<lambda>x. f x \$ k *s v)"`
`  1431   using lf k`
`  1412   using lf`
`  1432   apply (auto simp add: linear_def )`
`  1413   apply (auto simp add: linear_def )`
`  1433   by (vector ring_simps)+`
`  1414   by (vector ring_simps)+`
`  1434 `
`  1415 `
`  1435 lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n)"`
`  1416 lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n)"`
`  1436   unfolding linear_def`
`  1417   unfolding linear_def`
`  1483   also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)" by auto`
`  1464   also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)" by auto`
`  1484   finally show ?thesis .`
`  1465   finally show ?thesis .`
`  1485 qed`
`  1466 qed`
`  1486 `
`  1467 `
`  1487 lemma linear_bounded:`
`  1468 lemma linear_bounded:`
`  1488   fixes f:: "real ^'m \<Rightarrow> real ^'n"`
`  1469   fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"`
`  1489   assumes lf: "linear f"`
`  1470   assumes lf: "linear f"`
`  1490   shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"`
`  1471   shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"`
`  1491 proof-`
`  1472 proof-`
`  1492   let ?S = "{1..dimindex(UNIV:: 'm set)}"`
`  1473   let ?S = "UNIV:: 'm set"`
`  1493   let ?B = "setsum (\<lambda>i. norm(f(basis i))) ?S"`
`  1474   let ?B = "setsum (\<lambda>i. norm(f(basis i))) ?S"`
`  1494   have fS: "finite ?S" by simp`
`  1475   have fS: "finite ?S" by simp`
`  1495   {fix x:: "real ^ 'm"`
`  1476   {fix x:: "real ^ 'm"`
`  1496     let ?g = "(\<lambda>i::nat. (x\$i) *s (basis i) :: real ^ 'm)"`
`  1477     let ?g = "(\<lambda>i. (x\$i) *s (basis i) :: real ^ 'm)"`
`  1497     have "norm (f x) = norm (f (setsum (\<lambda>i. (x\$i) *s (basis i)) ?S))"`
`  1478     have "norm (f x) = norm (f (setsum (\<lambda>i. (x\$i) *s (basis i)) ?S))"`
`  1498       by (simp only:  basis_expansion)`
`  1479       by (simp only:  basis_expansion)`
`  1499     also have "\<dots> = norm (setsum (\<lambda>i. (x\$i) *s f (basis i))?S)"`
`  1480     also have "\<dots> = norm (setsum (\<lambda>i. (x\$i) *s f (basis i))?S)"`
`  1500       using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf]`
`  1481       using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf]`
`  1501       by auto`
`  1482       by auto`
`  1502     finally have th0: "norm (f x) = norm (setsum (\<lambda>i. (x\$i) *s f (basis i))?S)" .`
`  1483     finally have th0: "norm (f x) = norm (setsum (\<lambda>i. (x\$i) *s f (basis i))?S)" .`
`  1503     {fix i assume i: "i \<in> ?S"`
`  1484     {fix i assume i: "i \<in> ?S"`
`  1504       from component_le_norm[OF i, of x]`
`  1485       from component_le_norm[of x i]`
`  1505       have "norm ((x\$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x"`
`  1486       have "norm ((x\$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x"`
`  1506       unfolding norm_mul`
`  1487       unfolding norm_mul`
`  1507       apply (simp only: mult_commute)`
`  1488       apply (simp only: mult_commute)`
`  1508       apply (rule mult_mono)`
`  1489       apply (rule mult_mono)`
`  1509       by (auto simp add: ring_simps norm_ge_zero) }`
`  1490       by (auto simp add: ring_simps norm_ge_zero) }`
`  1512     have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}`
`  1493     have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}`
`  1513   then show ?thesis by blast`
`  1494   then show ?thesis by blast`
`  1514 qed`
`  1495 qed`
`  1515 `
`  1496 `
`  1516 lemma linear_bounded_pos:`
`  1497 lemma linear_bounded_pos:`
`  1517   fixes f:: "real ^'n \<Rightarrow> real ^ 'm"`
`  1498   fixes f:: "real ^'n::finite \<Rightarrow> real ^ 'm::finite"`
`  1518   assumes lf: "linear f"`
`  1499   assumes lf: "linear f"`
`  1519   shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"`
`  1500   shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"`
`  1520 proof-`
`  1501 proof-`
`  1521   from linear_bounded[OF lf] obtain B where`
`  1502   from linear_bounded[OF lf] obtain B where`
`  1522     B: "\<forall>x. norm (f x) \<le> B * norm x" by blast`
`  1503     B: "\<forall>x. norm (f x) \<le> B * norm x" by blast`
`  1593     using bh fT by (auto simp add: bilinear_def)`
`  1574     using bh fT by (auto simp add: bilinear_def)`
`  1594   finally show ?thesis unfolding setsum_cartesian_product .`
`  1575   finally show ?thesis unfolding setsum_cartesian_product .`
`  1595 qed`
`  1576 qed`
`  1596 `
`  1577 `
`  1597 lemma bilinear_bounded:`
`  1578 lemma bilinear_bounded:`
`  1598   fixes h:: "real ^'m \<Rightarrow> real^'n \<Rightarrow> real ^ 'k"`
`  1579   fixes h:: "real ^'m::finite \<Rightarrow> real^'n::finite \<Rightarrow> real ^ 'k::finite"`
`  1599   assumes bh: "bilinear h"`
`  1580   assumes bh: "bilinear h"`
`  1600   shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"`
`  1581   shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"`
`  1601 proof-`
`  1582 proof-`
`  1602   let ?M = "{1 .. dimindex (UNIV :: 'm set)}"`
`  1583   let ?M = "UNIV :: 'm set"`
`  1603   let ?N = "{1 .. dimindex (UNIV :: 'n set)}"`
`  1584   let ?N = "UNIV :: 'n set"`
`  1604   let ?B = "setsum (\<lambda>(i,j). norm (h (basis i) (basis j))) (?M \<times> ?N)"`
`  1585   let ?B = "setsum (\<lambda>(i,j). norm (h (basis i) (basis j))) (?M \<times> ?N)"`
`  1605   have fM: "finite ?M" and fN: "finite ?N" by simp_all`
`  1586   have fM: "finite ?M" and fN: "finite ?N" by simp_all`
`  1606   {fix x:: "real ^ 'm" and  y :: "real^'n"`
`  1587   {fix x:: "real ^ 'm" and  y :: "real^'n"`
`  1607     have "norm (h x y) = norm (h (setsum (\<lambda>i. (x\$i) *s basis i) ?M) (setsum (\<lambda>i. (y\$i) *s basis i) ?N))" unfolding basis_expansion ..`
`  1588     have "norm (h x y) = norm (h (setsum (\<lambda>i. (x\$i) *s basis i) ?M) (setsum (\<lambda>i. (y\$i) *s basis i) ?N))" unfolding basis_expansion ..`
`  1608     also have "\<dots> = norm (setsum (\<lambda> (i,j). h ((x\$i) *s basis i) ((y\$j) *s basis j)) (?M \<times> ?N))"  unfolding bilinear_setsum[OF bh fM fN] ..`
`  1589     also have "\<dots> = norm (setsum (\<lambda> (i,j). h ((x\$i) *s basis i) ((y\$j) *s basis j)) (?M \<times> ?N))"  unfolding bilinear_setsum[OF bh fM fN] ..`
`  1620       done}`
`  1601       done}`
`  1621   then show ?thesis by metis`
`  1602   then show ?thesis by metis`
`  1622 qed`
`  1603 qed`
`  1623 `
`  1604 `
`  1624 lemma bilinear_bounded_pos:`
`  1605 lemma bilinear_bounded_pos:`
`  1625   fixes h:: "real ^'m \<Rightarrow> real^'n \<Rightarrow> real ^ 'k"`
`  1606   fixes h:: "real ^'m::finite \<Rightarrow> real^'n::finite \<Rightarrow> real ^ 'k::finite"`
`  1626   assumes bh: "bilinear h"`
`  1607   assumes bh: "bilinear h"`
`  1627   shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"`
`  1608   shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"`
`  1628 proof-`
`  1609 proof-`
`  1629   from bilinear_bounded[OF bh] obtain B where`
`  1610   from bilinear_bounded[OF bh] obtain B where`
`  1630     B: "\<forall>x y. norm (h x y) \<le> B * norm x * norm y" by blast`
`  1611     B: "\<forall>x y. norm (h x y) \<le> B * norm x * norm y" by blast`
`  1647 definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"`
`  1628 definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"`
`  1648 `
`  1629 `
`  1649 lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis`
`  1630 lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis`
`  1650 `
`  1631 `
`  1651 lemma adjoint_works_lemma:`
`  1632 lemma adjoint_works_lemma:`
`  1652   fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^ 'm"`
`  1633   fixes f:: "'a::ring_1 ^'n::finite \<Rightarrow> 'a ^ 'm::finite"`
`  1653   assumes lf: "linear f"`
`  1634   assumes lf: "linear f"`
`  1654   shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y"`
`  1635   shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y"`
`  1655 proof-`
`  1636 proof-`
`  1656   let ?N = "{1 .. dimindex (UNIV :: 'n set)}"`
`  1637   let ?N = "UNIV :: 'n set"`
`  1657   let ?M = "{1 .. dimindex (UNIV :: 'm set)}"`
`  1638   let ?M = "UNIV :: 'm set"`
`  1658   have fN: "finite ?N" by simp`
`  1639   have fN: "finite ?N" by simp`
`  1659   have fM: "finite ?M" by simp`
`  1640   have fM: "finite ?M" by simp`
`  1660   {fix y:: "'a ^ 'm"`
`  1641   {fix y:: "'a ^ 'm"`
`  1661     let ?w = "(\<chi> i. (f (basis i) \<bullet> y)) :: 'a ^ 'n"`
`  1642     let ?w = "(\<chi> i. (f (basis i) \<bullet> y)) :: 'a ^ 'n"`
`  1662     {fix x`
`  1643     {fix x`
`  1665       also have "\<dots> = (setsum (\<lambda>i. (x\$i) *s f (basis i)) ?N) \<bullet> y"`
`  1646       also have "\<dots> = (setsum (\<lambda>i. (x\$i) *s f (basis i)) ?N) \<bullet> y"`
`  1666 	unfolding linear_setsum[OF lf fN]`
`  1647 	unfolding linear_setsum[OF lf fN]`
`  1667 	by (simp add: linear_cmul[OF lf])`
`  1648 	by (simp add: linear_cmul[OF lf])`
`  1668       finally have "f x \<bullet> y = x \<bullet> ?w"`
`  1649       finally have "f x \<bullet> y = x \<bullet> ?w"`
`  1669 	apply (simp only: )`
`  1650 	apply (simp only: )`
`  1670 	apply (simp add: dot_def setsum_component Cart_lambda_beta setsum_left_distrib setsum_right_distrib vector_component setsum_commute[of _ ?M ?N] ring_simps del: One_nat_def)`
`  1651 	apply (simp add: dot_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] ring_simps)`
`  1671 	done}`
`  1652 	done}`
`  1672   }`
`  1653   }`
`  1673   then show ?thesis unfolding adjoint_def`
`  1654   then show ?thesis unfolding adjoint_def`
`  1674     some_eq_ex[of "\<lambda>f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y"]`
`  1655     some_eq_ex[of "\<lambda>f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y"]`
`  1675     using choice_iff[of "\<lambda>a b. \<forall>x. f x \<bullet> a = x \<bullet> b "]`
`  1656     using choice_iff[of "\<lambda>a b. \<forall>x. f x \<bullet> a = x \<bullet> b "]`
`  1676     by metis`
`  1657     by metis`
`  1677 qed`
`  1658 qed`
`  1678 `
`  1659 `
`  1679 lemma adjoint_works:`
`  1660 lemma adjoint_works:`
`  1680   fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^ 'm"`
`  1661   fixes f:: "'a::ring_1 ^'n::finite \<Rightarrow> 'a ^ 'm::finite"`
`  1681   assumes lf: "linear f"`
`  1662   assumes lf: "linear f"`
`  1682   shows "x \<bullet> adjoint f y = f x \<bullet> y"`
`  1663   shows "x \<bullet> adjoint f y = f x \<bullet> y"`
`  1683   using adjoint_works_lemma[OF lf] by metis`
`  1664   using adjoint_works_lemma[OF lf] by metis`
`  1684 `
`  1665 `
`  1685 `
`  1666 `
`  1686 lemma adjoint_linear:`
`  1667 lemma adjoint_linear:`
`  1687   fixes f :: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^ 'm"`
`  1668   fixes f :: "'a::comm_ring_1 ^'n::finite \<Rightarrow> 'a ^ 'm::finite"`
`  1688   assumes lf: "linear f"`
`  1669   assumes lf: "linear f"`
`  1689   shows "linear (adjoint f)"`
`  1670   shows "linear (adjoint f)"`
`  1690   by (simp add: linear_def vector_eq_ldot[symmetric] dot_radd dot_rmult adjoint_works[OF lf])`
`  1671   by (simp add: linear_def vector_eq_ldot[symmetric] dot_radd dot_rmult adjoint_works[OF lf])`
`  1691 `
`  1672 `
`  1692 lemma adjoint_clauses:`
`  1673 lemma adjoint_clauses:`
`  1693   fixes f:: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^ 'm"`
`  1674   fixes f:: "'a::comm_ring_1 ^'n::finite \<Rightarrow> 'a ^ 'm::finite"`
`  1694   assumes lf: "linear f"`
`  1675   assumes lf: "linear f"`
`  1695   shows "x \<bullet> adjoint f y = f x \<bullet> y"`
`  1676   shows "x \<bullet> adjoint f y = f x \<bullet> y"`
`  1696   and "adjoint f y \<bullet> x = y \<bullet> f x"`
`  1677   and "adjoint f y \<bullet> x = y \<bullet> f x"`
`  1697   by (simp_all add: adjoint_works[OF lf] dot_sym )`
`  1678   by (simp_all add: adjoint_works[OF lf] dot_sym )`
`  1698 `
`  1679 `
`  1699 lemma adjoint_adjoint:`
`  1680 lemma adjoint_adjoint:`
`  1700   fixes f:: "'a::comm_ring_1 ^ 'n \<Rightarrow> _"`
`  1681   fixes f:: "'a::comm_ring_1 ^ 'n::finite \<Rightarrow> 'a ^ 'm::finite"`
`  1701   assumes lf: "linear f"`
`  1682   assumes lf: "linear f"`
`  1702   shows "adjoint (adjoint f) = f"`
`  1683   shows "adjoint (adjoint f) = f"`
`  1703   apply (rule ext)`
`  1684   apply (rule ext)`
`  1704   by (simp add: vector_eq_ldot[symmetric] adjoint_clauses[OF adjoint_linear[OF lf]] adjoint_clauses[OF lf])`
`  1685   by (simp add: vector_eq_ldot[symmetric] adjoint_clauses[OF adjoint_linear[OF lf]] adjoint_clauses[OF lf])`
`  1705 `
`  1686 `
`  1706 lemma adjoint_unique:`
`  1687 lemma adjoint_unique:`
`  1707   fixes f:: "'a::comm_ring_1 ^ 'n \<Rightarrow> 'a ^ 'm"`
`  1688   fixes f:: "'a::comm_ring_1 ^ 'n::finite \<Rightarrow> 'a ^ 'm::finite"`
`  1708   assumes lf: "linear f" and u: "\<forall>x y. f' x \<bullet> y = x \<bullet> f y"`
`  1689   assumes lf: "linear f" and u: "\<forall>x y. f' x \<bullet> y = x \<bullet> f y"`
`  1709   shows "f' = adjoint f"`
`  1690   shows "f' = adjoint f"`
`  1710   apply (rule ext)`
`  1691   apply (rule ext)`
`  1711   using u`
`  1692   using u`
`  1712   by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf])`
`  1693   by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf])`
`  1714 text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}`
`  1695 text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}`
`  1715 `
`  1696 `
`  1716 consts generic_mult :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" (infixr "\<star>" 75)`
`  1697 consts generic_mult :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" (infixr "\<star>" 75)`
`  1717 `
`  1698 `
`  1718 defs (overloaded)`
`  1699 defs (overloaded)`
`  1719 matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^'n^'m) \<star> (m' :: 'a ^'p^'n) \<equiv> (\<chi> i j. setsum (\<lambda>k. ((m\$i)\$k) * ((m'\$k)\$j)) {1 .. dimindex (UNIV :: 'n set)}) ::'a ^ 'p ^'m"`
`  1700 matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^'n^'m) \<star> (m' :: 'a ^'p^'n) \<equiv> (\<chi> i j. setsum (\<lambda>k. ((m\$i)\$k) * ((m'\$k)\$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"`
`  1720 `
`  1701 `
`  1721 abbreviation`
`  1702 abbreviation`
`  1722   matrix_matrix_mult' :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"  (infixl "**" 70)`
`  1703   matrix_matrix_mult' :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"  (infixl "**" 70)`
`  1723   where "m ** m' == m\<star> m'"`
`  1704   where "m ** m' == m\<star> m'"`
`  1724 `
`  1705 `
`  1725 defs (overloaded)`
`  1706 defs (overloaded)`
`  1726   matrix_vector_mult_def: "(m::('a::semiring_1) ^'n^'m) \<star> (x::'a ^'n) \<equiv> (\<chi> i. setsum (\<lambda>j. ((m\$i)\$j) * (x\$j)) {1..dimindex(UNIV ::'n set)}) :: 'a^'m"`
`  1707   matrix_vector_mult_def: "(m::('a::semiring_1) ^'n^'m) \<star> (x::'a ^'n) \<equiv> (\<chi> i. setsum (\<lambda>j. ((m\$i)\$j) * (x\$j)) (UNIV ::'n set)) :: 'a^'m"`
`  1727 `
`  1708 `
`  1728 abbreviation`
`  1709 abbreviation`
`  1729   matrix_vector_mult' :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"  (infixl "*v" 70)`
`  1710   matrix_vector_mult' :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"  (infixl "*v" 70)`
`  1730   where`
`  1711   where`
`  1731   "m *v v == m \<star> v"`
`  1712   "m *v v == m \<star> v"`
`  1732 `
`  1713 `
`  1733 defs (overloaded)`
`  1714 defs (overloaded)`
`  1734   vector_matrix_mult_def: "(x::'a^'m) \<star> (m::('a::semiring_1) ^'n^'m) \<equiv> (\<chi> j. setsum (\<lambda>i. ((m\$i)\$j) * (x\$i)) {1..dimindex(UNIV :: 'm set)}) :: 'a^'n"`
`  1715   vector_matrix_mult_def: "(x::'a^'m) \<star> (m::('a::semiring_1) ^'n^'m) \<equiv> (\<chi> j. setsum (\<lambda>i. ((m\$i)\$j) * (x\$i)) (UNIV :: 'm set)) :: 'a^'n"`
`  1735 `
`  1716 `
`  1736 abbreviation`
`  1717 abbreviation`
`  1737   vactor_matrix_mult' :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "  (infixl "v*" 70)`
`  1718   vactor_matrix_mult' :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "  (infixl "v*" 70)`
`  1738   where`
`  1719   where`
`  1739   "v v* m == v \<star> m"`
`  1720   "v v* m == v \<star> m"`
`  1740 `
`  1721 `
`  1741 definition "(mat::'a::zero => 'a ^'n^'m) k = (\<chi> i j. if i = j then k else 0)"`
`  1722 definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"`
`  1742 definition "(transp::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A\$j)\$i))"`
`  1723 definition "(transp::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A\$j)\$i))"`
`  1743 definition "(row::nat => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A\$i)\$j))"`
`  1724 definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A\$i)\$j))"`
`  1744 definition "(column::nat =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A\$i)\$j))"`
`  1725 definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A\$i)\$j))"`
`  1745 definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> {1 .. dimindex(UNIV :: 'm set)}}"`
`  1726 definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"`
`  1746 definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> {1 .. dimindex(UNIV :: 'n set)}}"`
`  1727 definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"`
`  1747 `
`  1728 `
`  1748 lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)`
`  1729 lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)`
`  1749 lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \<star> B) + (A \<star> C)"`
`  1730 lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \<star> B) + (A \<star> C)"`
`  1750   by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps)`
`  1731   by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps)`
`  1751 `
`  1732 `
`  1754   "setsum (\<lambda>k. if a = k then b k else 0) S =`
`  1735   "setsum (\<lambda>k. if a = k then b k else 0) S =`
`  1755      (if a\<in> S then b a else 0)"`
`  1736      (if a\<in> S then b a else 0)"`
`  1756   using setsum_delta[OF fS, of a b, symmetric]`
`  1737   using setsum_delta[OF fS, of a b, symmetric]`
`  1757   by (auto intro: setsum_cong)`
`  1738   by (auto intro: setsum_cong)`
`  1758 `
`  1739 `
`  1759 lemma matrix_mul_lid: "mat 1 ** A = A"`
`  1740 lemma matrix_mul_lid:`
`       `
`  1741   fixes A :: "'a::semiring_1 ^ 'm ^ 'n::finite"`
`       `
`  1742   shows "mat 1 ** A = A"`
`  1760   apply (simp add: matrix_matrix_mult_def mat_def)`
`  1743   apply (simp add: matrix_matrix_mult_def mat_def)`
`  1761   apply vector`
`  1744   apply vector`
`  1762   by (auto simp only: cond_value_iff cond_application_beta setsum_delta'[OF finite_atLeastAtMost]  mult_1_left mult_zero_left if_True)`
`  1745   by (auto simp only: cond_value_iff cond_application_beta setsum_delta'[OF finite]  mult_1_left mult_zero_left if_True UNIV_I)`
`  1763 `
`  1746 `
`  1764 `
`  1747 `
`  1765 lemma matrix_mul_rid: "A ** mat 1 = A"`
`  1748 lemma matrix_mul_rid:`
`       `
`  1749   fixes A :: "'a::semiring_1 ^ 'm::finite ^ 'n"`
`       `
`  1750   shows "A ** mat 1 = A"`
`  1766   apply (simp add: matrix_matrix_mult_def mat_def)`
`  1751   apply (simp add: matrix_matrix_mult_def mat_def)`
`  1767   apply vector`
`  1752   apply vector`
`  1768   by (auto simp only: cond_value_iff cond_application_beta setsum_delta[OF finite_atLeastAtMost]  mult_1_right mult_zero_right if_True cong: if_cong)`
`  1753   by (auto simp only: cond_value_iff cond_application_beta setsum_delta[OF finite]  mult_1_right mult_zero_right if_True UNIV_I cong: if_cong)`
`  1769 `
`  1754 `
`  1770 lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"`
`  1755 lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"`
`  1771   apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)`
`  1756   apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)`
`  1772   apply (subst setsum_commute)`
`  1757   apply (subst setsum_commute)`
`  1773   apply simp`
`  1758   apply simp`
`  1777   apply (vector matrix_matrix_mult_def matrix_vector_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)`
`  1762   apply (vector matrix_matrix_mult_def matrix_vector_mult_def setsum_right_distrib setsum_left_distrib mult_assoc)`
`  1778   apply (subst setsum_commute)`
`  1763   apply (subst setsum_commute)`
`  1779   apply simp`
`  1764   apply simp`
`  1780   done`
`  1765   done`
`  1781 `
`  1766 `
`  1782 lemma matrix_vector_mul_lid: "mat 1 *v x = x"`
`  1767 lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n::finite)"`
`  1783   apply (vector matrix_vector_mult_def mat_def)`
`  1768   apply (vector matrix_vector_mult_def mat_def)`
`  1784   by (simp add: cond_value_iff cond_application_beta`
`  1769   by (simp add: cond_value_iff cond_application_beta`
`  1785     setsum_delta' cong del: if_weak_cong)`
`  1770     setsum_delta' cong del: if_weak_cong)`
`  1786 `
`  1771 `
`  1787 lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^'m^'n)"`
`  1772 lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^'m^'n)"`
`  1788   by (simp add: matrix_matrix_mult_def transp_def Cart_eq Cart_lambda_beta mult_commute)`
`  1773   by (simp add: matrix_matrix_mult_def transp_def Cart_eq mult_commute)`
`  1789 `
`  1774 `
`  1790 lemma matrix_eq: "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")`
`  1775 lemma matrix_eq:`
`       `
`  1776   fixes A B :: "'a::semiring_1 ^ 'n::finite ^ 'm"`
`       `
`  1777   shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")`
`  1791   apply auto`
`  1778   apply auto`
`  1792   apply (subst Cart_eq)`
`  1779   apply (subst Cart_eq)`
`  1793   apply clarify`
`  1780   apply clarify`
`  1794   apply (clarsimp simp add: matrix_vector_mult_def basis_def cond_value_iff cond_application_beta Cart_eq Cart_lambda_beta cong del: if_weak_cong)`
`  1781   apply (clarsimp simp add: matrix_vector_mult_def basis_def cond_value_iff cond_application_beta Cart_eq cong del: if_weak_cong)`
`  1795   apply (erule_tac x="basis ia" in allE)`
`  1782   apply (erule_tac x="basis ia" in allE)`
`  1796   apply (erule_tac x="i" in ballE)`
`  1783   apply (erule_tac x="i" in allE)`
`  1797   by (auto simp add: basis_def cond_value_iff cond_application_beta Cart_lambda_beta setsum_delta[OF finite_atLeastAtMost] cong del: if_weak_cong)`
`  1784   by (auto simp add: basis_def cond_value_iff cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong)`
`  1798 `
`  1785 `
`  1799 lemma matrix_vector_mul_component:`
`  1786 lemma matrix_vector_mul_component:`
`  1801   shows "((A::'a::semiring_1^'n'^'m) *v x)\$k = (A\$k) \<bullet> x"`
`  1787   shows "((A::'a::semiring_1^'n'^'m) *v x)\$k = (A\$k) \<bullet> x"`
`  1802   using k`
`  1788   by (simp add: matrix_vector_mult_def dot_def)`
`  1803   by (simp add: matrix_vector_mult_def Cart_lambda_beta dot_def)`
`       `
`  1804 `
`  1789 `
`  1805 lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^'n) v* A) \<bullet> y = x \<bullet> (A *v y)"`
`  1790 lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^'n) v* A) \<bullet> y = x \<bullet> (A *v y)"`
`  1806   apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib Cart_lambda_beta mult_ac)`
`  1791   apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)`
`  1807   apply (subst setsum_commute)`
`  1792   apply (subst setsum_commute)`
`  1808   by simp`
`  1793   by simp`
`  1809 `
`  1794 `
`  1810 lemma transp_mat: "transp (mat n) = mat n"`
`  1795 lemma transp_mat: "transp (mat n) = mat n"`
`  1811   by (vector transp_def mat_def)`
`  1796   by (vector transp_def mat_def)`
`  1813 lemma transp_transp: "transp(transp A) = A"`
`  1798 lemma transp_transp: "transp(transp A) = A"`
`  1814   by (vector transp_def)`
`  1799   by (vector transp_def)`
`  1815 `
`  1800 `
`  1816 lemma row_transp:`
`  1801 lemma row_transp:`
`  1817   fixes A:: "'a::semiring_1^'n^'m"`
`  1802   fixes A:: "'a::semiring_1^'n^'m"`
`  1819   shows "row i (transp A) = column i A"`
`  1803   shows "row i (transp A) = column i A"`
`  1820   using i`
`  1804   by (simp add: row_def column_def transp_def Cart_eq)`
`  1821   by (simp add: row_def column_def transp_def Cart_eq Cart_lambda_beta)`
`       `
`  1822 `
`  1805 `
`  1823 lemma column_transp:`
`  1806 lemma column_transp:`
`  1824   fixes A:: "'a::semiring_1^'n^'m"`
`  1807   fixes A:: "'a::semiring_1^'n^'m"`
`  1826   shows "column i (transp A) = row i A"`
`  1808   shows "column i (transp A) = row i A"`
`  1827   using i`
`  1809   by (simp add: row_def column_def transp_def Cart_eq)`
`  1828   by (simp add: row_def column_def transp_def Cart_eq Cart_lambda_beta)`
`       `
`  1829 `
`  1810 `
`  1830 lemma rows_transp: "rows(transp (A::'a::semiring_1^'n^'m)) = columns A"`
`  1811 lemma rows_transp: "rows(transp (A::'a::semiring_1^'n^'m)) = columns A"`
`  1831 apply (auto simp add: rows_def columns_def row_transp intro: set_ext)`
`  1812 by (auto simp add: rows_def columns_def row_transp intro: set_ext)`
`  1832 apply (rule_tac x=i in exI)`
`       `
`  1833 apply (auto simp add: row_transp)`
`       `
`  1834 done`
`       `
`  1835 `
`  1813 `
`  1836 lemma columns_transp: "columns(transp (A::'a::semiring_1^'n^'m)) = rows A" by (metis transp_transp rows_transp)`
`  1814 lemma columns_transp: "columns(transp (A::'a::semiring_1^'n^'m)) = rows A" by (metis transp_transp rows_transp)`
`  1837 `
`  1815 `
`  1838 text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}`
`  1816 text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}`
`  1839 `
`  1817 `
`  1840 lemma matrix_mult_dot: "A *v x = (\<chi> i. A\$i \<bullet> x)"`
`  1818 lemma matrix_mult_dot: "A *v x = (\<chi> i. A\$i \<bullet> x)"`
`  1841   by (simp add: matrix_vector_mult_def dot_def)`
`  1819   by (simp add: matrix_vector_mult_def dot_def)`
`  1842 `
`  1820 `
`  1843 lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x\$i) *s column i A) {1 .. dimindex(UNIV:: 'n set)}"`
`  1821 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)"`
`  1844   by (simp add: matrix_vector_mult_def Cart_eq setsum_component Cart_lambda_beta vector_component column_def mult_commute)`
`  1822   by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute)`
`  1845 `
`  1823 `
`  1846 lemma vector_componentwise:`
`  1824 lemma vector_componentwise:`
`  1847   "(x::'a::ring_1^'n) = (\<chi> j. setsum (\<lambda>i. (x\$i) * (basis i :: 'a^'n)\$j) {1..dimindex(UNIV :: 'n set)})"`
`  1825   "(x::'a::ring_1^'n::finite) = (\<chi> j. setsum (\<lambda>i. (x\$i) * (basis i :: 'a^'n)\$j) (UNIV :: 'n set))"`
`  1848   apply (subst basis_expansion[symmetric])`
`  1826   apply (subst basis_expansion[symmetric])`
`  1849   by (vector Cart_eq Cart_lambda_beta setsum_component)`
`  1827   by (vector Cart_eq setsum_component)`
`  1850 `
`  1828 `
`  1851 lemma linear_componentwise:`
`  1829 lemma linear_componentwise:`
`  1852   fixes f:: "'a::ring_1 ^ 'm \<Rightarrow> 'a ^ 'n"`
`  1830   fixes f:: "'a::ring_1 ^ 'm::finite \<Rightarrow> 'a ^ 'n"`
`  1853   assumes lf: "linear f" and j: "j \<in> {1 .. dimindex (UNIV :: 'n set)}"`
`  1831   assumes lf: "linear f"`
`  1854   shows "(f x)\$j = setsum (\<lambda>i. (x\$i) * (f (basis i)\$j)) {1 .. dimindex (UNIV :: 'm set)}" (is "?lhs = ?rhs")`
`  1832   shows "(f x)\$j = setsum (\<lambda>i. (x\$i) * (f (basis i)\$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")`
`  1855 proof-`
`  1833 proof-`
`  1856   let ?M = "{1 .. dimindex (UNIV :: 'm set)}"`
`  1834   let ?M = "(UNIV :: 'm set)"`
`  1857   let ?N = "{1 .. dimindex (UNIV :: 'n set)}"`
`  1835   let ?N = "(UNIV :: 'n set)"`
`  1858   have fM: "finite ?M" by simp`
`  1836   have fM: "finite ?M" by simp`
`  1859   have "?rhs = (setsum (\<lambda>i.(x\$i) *s f (basis i) ) ?M)\$j"`
`  1837   have "?rhs = (setsum (\<lambda>i.(x\$i) *s f (basis i) ) ?M)\$j"`
`  1860     unfolding vector_smult_component[OF j, symmetric]`
`  1838     unfolding vector_smult_component[symmetric]`
`  1861     unfolding setsum_component[OF j, of "(\<lambda>i.(x\$i) *s f (basis i :: 'a^'m))" ?M]`
`  1839     unfolding setsum_component[of "(\<lambda>i.(x\$i) *s f (basis i :: 'a^'m))" ?M]`
`  1862     ..`
`  1840     ..`
`  1863   then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion ..`
`  1841   then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion ..`
`  1864 qed`
`  1842 qed`
`  1865 `
`  1843 `
`  1866 text{* Inverse matrices  (not necessarily square) *}`
`  1844 text{* Inverse matrices  (not necessarily square) *}`
`  1874 `
`  1852 `
`  1875 definition matrix:: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"`
`  1853 definition matrix:: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"`
`  1876 where "matrix f = (\<chi> i j. (f(basis j))\$i)"`
`  1854 where "matrix f = (\<chi> i j. (f(basis j))\$i)"`
`  1877 `
`  1855 `
`  1878 lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::'a::comm_semiring_1 ^ 'n))"`
`  1856 lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::'a::comm_semiring_1 ^ 'n))"`
`  1879   by (simp add: linear_def matrix_vector_mult_def Cart_eq Cart_lambda_beta vector_component ring_simps setsum_right_distrib setsum_addf)`
`  1857   by (simp add: linear_def matrix_vector_mult_def Cart_eq ring_simps setsum_right_distrib setsum_addf)`
`  1880 `
`  1858 `
`  1881 lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n)"`
`  1859 lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n::finite)"`
`  1882 apply (simp add: matrix_def matrix_vector_mult_def Cart_eq Cart_lambda_beta mult_commute del: One_nat_def)`
`  1860 apply (simp add: matrix_def matrix_vector_mult_def Cart_eq mult_commute)`
`  1883 apply clarify`
`  1861 apply clarify`
`  1884 apply (rule linear_componentwise[OF lf, symmetric])`
`  1862 apply (rule linear_componentwise[OF lf, symmetric])`
`  1886 done`
`  1863 done`
`  1887 `
`  1864 `
`  1888 lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::'a::comm_ring_1 ^ 'n))" by (simp add: ext matrix_works)`
`  1865 lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::'a::comm_ring_1 ^ 'n::finite))" by (simp add: ext matrix_works)`
`  1889 `
`  1866 `
`  1890 lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: 'a:: comm_ring_1 ^ 'n)) = A"`
`  1867 lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: 'a:: comm_ring_1 ^ 'n::finite)) = A"`
`  1891   by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)`
`  1868   by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)`
`  1892 `
`  1869 `
`  1893 lemma matrix_compose:`
`  1870 lemma matrix_compose:`
`  1894   assumes lf: "linear (f::'a::comm_ring_1^'n \<Rightarrow> _)" and lg: "linear g"`
`  1871   assumes lf: "linear (f::'a::comm_ring_1^'n::finite \<Rightarrow> 'a^'m::finite)"`
`       `
`  1872   and lg: "linear (g::'a::comm_ring_1^'m::finite \<Rightarrow> 'a^'k)"`
`  1895   shows "matrix (g o f) = matrix g ** matrix f"`
`  1873   shows "matrix (g o f) = matrix g ** matrix f"`
`  1896   using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]]`
`  1874   using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]]`
`  1897   by (simp  add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)`
`  1875   by (simp  add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)`
`  1898 `
`  1876 `
`  1899 lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x\$i) *s ((transp A)\$i)) {1..dimindex(UNIV:: 'n set)}"`
`  1877 lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x\$i) *s ((transp A)\$i)) (UNIV:: 'n set)"`
`  1900   by (simp add: matrix_vector_mult_def transp_def Cart_eq Cart_lambda_beta setsum_component vector_component mult_commute)`
`  1878   by (simp add: matrix_vector_mult_def transp_def Cart_eq mult_commute)`
`  1901 `
`  1879 `
`  1902 lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n^'m) *v x) = (\<lambda>x. transp A *v x)"`
`  1880 lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n::finite^'m::finite) *v x) = (\<lambda>x. transp A *v x)"`
`  1903   apply (rule adjoint_unique[symmetric])`
`  1881   apply (rule adjoint_unique[symmetric])`
`  1904   apply (rule matrix_vector_mul_linear)`
`  1882   apply (rule matrix_vector_mul_linear)`
`  1905   apply (simp add: transp_def dot_def Cart_lambda_beta matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)`
`  1883   apply (simp add: transp_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)`
`  1906   apply (subst setsum_commute)`
`  1884   apply (subst setsum_commute)`
`  1907   apply (auto simp add: mult_ac)`
`  1885   apply (auto simp add: mult_ac)`
`  1908   done`
`  1886   done`
`  1909 `
`  1887 `
`  1910 lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \<Rightarrow> 'a ^ 'm)"`
`  1888 lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n::finite \<Rightarrow> 'a ^ 'm::finite)"`
`  1911   shows "matrix(adjoint f) = transp(matrix f)"`
`  1889   shows "matrix(adjoint f) = transp(matrix f)"`
`  1912   apply (subst matrix_vector_mul[OF lf])`
`  1890   apply (subst matrix_vector_mul[OF lf])`
`  1913   unfolding adjoint_matrix matrix_of_matrix_vector_mul ..`
`  1891   unfolding adjoint_matrix matrix_of_matrix_vector_mul ..`
`  1914 `
`  1892 `
`  1915 subsection{* Interlude: Some properties of real sets *}`
`  1893 subsection{* Interlude: Some properties of real sets *}`
`  1978   from y z have yz: "y + z \<ge> 0" by arith`
`  1956   from y z have yz: "y + z \<ge> 0" by arith`
`  1979   from power2_le_imp_le[OF th yz] show ?thesis .`
`  1957   from power2_le_imp_le[OF th yz] show ?thesis .`
`  1980 qed`
`  1958 qed`
`  1981 `
`  1959 `
`  1982 `
`  1960 `
`  1983 lemma lambda_skolem: "(\<forall>i \<in> {1 .. dimindex(UNIV :: 'n set)}. \<exists>x. P i x) \<longleftrightarrow>`
`  1961 lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>`
`  1984    (\<exists>x::'a ^ 'n. \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. P i (x\$i))" (is "?lhs \<longleftrightarrow> ?rhs")`
`  1962    (\<exists>x::'a ^ 'n. \<forall>i. P i (x\$i))" (is "?lhs \<longleftrightarrow> ?rhs")`
`  1985 proof-`
`  1963 proof-`
`  1986   let ?S = "{1 .. dimindex(UNIV :: 'n set)}"`
`  1964   let ?S = "(UNIV :: 'n set)"`
`  1987   {assume H: "?rhs"`
`  1965   {assume H: "?rhs"`
`  1988     then have ?lhs by auto}`
`  1966     then have ?lhs by auto}`
`  1989   moreover`
`  1967   moreover`
`  1990   {assume H: "?lhs"`
`  1968   {assume H: "?lhs"`
`  1991     then obtain f where f:"\<forall>i\<in> ?S. P i (f i)" unfolding Ball_def choice_iff by metis`
`  1969     then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis`
`  1992     let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"`
`  1970     let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"`
`  1993     {fix i assume i: "i \<in> ?S"`
`  1971     {fix i`
`  1994       with f i have "P i (f i)" by metis`
`  1972       from f have "P i (f i)" by metis`
`  1995       then have "P i (?x\$i)" using Cart_lambda_beta[of f, rule_format, OF i] by auto`
`  1973       then have "P i (?x\$i)" by auto`
`  1996     }`
`  1974     }`
`  1997     hence "\<forall>i \<in> ?S. P i (?x\$i)" by metis`
`  1975     hence "\<forall>i. P i (?x\$i)" by metis`
`  1998     hence ?rhs by metis }`
`  1976     hence ?rhs by metis }`
`  1999   ultimately show ?thesis by metis`
`  1977   ultimately show ?thesis by metis`
`  2000 qed`
`  1978 qed`
`  2001 `
`  1979 `
`  2002 (* Supremum and infimum of real sets *)`
`  1980 (* Supremum and infimum of real sets *)`
`  2235 subsection{* Operator norm. *}`
`  2213 subsection{* Operator norm. *}`
`  2236 `
`  2214 `
`  2237 definition "onorm f = rsup {norm (f x)| x. norm x = 1}"`
`  2215 definition "onorm f = rsup {norm (f x)| x. norm x = 1}"`
`  2238 `
`  2216 `
`  2239 lemma norm_bound_generalize:`
`  2217 lemma norm_bound_generalize:`
`  2240   fixes f:: "real ^'n \<Rightarrow> real^'m"`
`  2218   fixes f:: "real ^'n::finite \<Rightarrow> real^'m::finite"`
`  2241   assumes lf: "linear f"`
`  2219   assumes lf: "linear f"`
`  2242   shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)" (is "?lhs \<longleftrightarrow> ?rhs")`
`  2220   shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)" (is "?lhs \<longleftrightarrow> ?rhs")`
`  2243 proof-`
`  2221 proof-`
`  2244   {assume H: ?rhs`
`  2222   {assume H: ?rhs`
`  2245     {fix x :: "real^'n" assume x: "norm x = 1"`
`  2223     {fix x :: "real^'n" assume x: "norm x = 1"`
`  2246       from H[rule_format, of x] x have "norm (f x) \<le> b" by simp}`
`  2224       from H[rule_format, of x] x have "norm (f x) \<le> b" by simp}`
`  2247     then have ?lhs by blast }`
`  2225     then have ?lhs by blast }`
`  2248 `
`  2226 `
`  2249   moreover`
`  2227   moreover`
`  2250   {assume H: ?lhs`
`  2228   {assume H: ?lhs`
`  2251     from H[rule_format, of "basis 1"]`
`  2229     from H[rule_format, of "basis arbitrary"]`
`  2252     have bp: "b \<ge> 0" using norm_ge_zero[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]`
`  2230     have bp: "b \<ge> 0" using norm_ge_zero[of "f (basis arbitrary)"]`
`  2253       by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])`
`  2231       by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])`
`  2254     {fix x :: "real ^'n"`
`  2232     {fix x :: "real ^'n"`
`  2255       {assume "x = 0"`
`  2233       {assume "x = 0"`
`  2256 	then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}`
`  2234 	then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}`
`  2257       moreover`
`  2235       moreover`
`  2268     then have ?rhs by blast}`
`  2246     then have ?rhs by blast}`
`  2269   ultimately show ?thesis by blast`
`  2247   ultimately show ?thesis by blast`
`  2270 qed`
`  2248 qed`
`  2271 `
`  2249 `
`  2272 lemma onorm:`
`  2250 lemma onorm:`
`  2273   fixes f:: "real ^'n \<Rightarrow> real ^'m"`
`  2251   fixes f:: "real ^'n::finite \<Rightarrow> real ^'m::finite"`
`  2274   assumes lf: "linear f"`
`  2252   assumes lf: "linear f"`
`  2275   shows "norm (f x) <= onorm f * norm x"`
`  2253   shows "norm (f x) <= onorm f * norm x"`
`  2276   and "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"`
`  2254   and "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"`
`  2277 proof-`
`  2255 proof-`
`  2278   {`
`  2256   {`
`  2279     let ?S = "{norm (f x) |x. norm x = 1}"`
`  2257     let ?S = "{norm (f x) |x. norm x = 1}"`
`  2280     have Se: "?S \<noteq> {}" using  norm_basis_1 by auto`
`  2258     have Se: "?S \<noteq> {}" using  norm_basis by auto`
`  2281     from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"`
`  2259     from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"`
`  2282       unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)`
`  2260       unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)`
`  2283     {from rsup[OF Se b, unfolded onorm_def[symmetric]]`
`  2261     {from rsup[OF Se b, unfolded onorm_def[symmetric]]`
`  2284       show "norm (f x) <= onorm f * norm x"`
`  2262       show "norm (f x) <= onorm f * norm x"`
`  2285 	apply -`
`  2263 	apply -`
`  2292 	unfolding norm_bound_generalize[OF lf, symmetric]`
`  2270 	unfolding norm_bound_generalize[OF lf, symmetric]`
`  2293 	by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}`
`  2271 	by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}`
`  2294   }`
`  2272   }`
`  2295 qed`
`  2273 qed`
`  2296 `
`  2274 `
`  2297 lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" shows "0 <= onorm f"`
`  2275 lemma onorm_pos_le: assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)" shows "0 <= onorm f"`
`  2298   using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp`
`  2276   using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis arbitrary"], unfolded norm_basis] by simp`
`  2299 `
`  2277 `
`  2300 lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"`
`  2278 lemma onorm_eq_0: assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)"`
`  2301   shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"`
`  2279   shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"`
`  2302   using onorm[OF lf]`
`  2280   using onorm[OF lf]`
`  2303   apply (auto simp add: onorm_pos_le)`
`  2281   apply (auto simp add: onorm_pos_le)`
`  2304   apply atomize`
`  2282   apply atomize`
`  2305   apply (erule allE[where x="0::real"])`
`  2283   apply (erule allE[where x="0::real"])`
`  2306   using onorm_pos_le[OF lf]`
`  2284   using onorm_pos_le[OF lf]`
`  2307   apply arith`
`  2285   apply arith`
`  2308   done`
`  2286   done`
`  2309 `
`  2287 `
`  2310 lemma onorm_const: "onorm(\<lambda>x::real^'n. (y::real ^ 'm)) = norm y"`
`  2288 lemma onorm_const: "onorm(\<lambda>x::real^'n::finite. (y::real ^ 'm::finite)) = norm y"`
`  2311 proof-`
`  2289 proof-`
`  2312   let ?f = "\<lambda>x::real^'n. (y::real ^ 'm)"`
`  2290   let ?f = "\<lambda>x::real^'n. (y::real ^ 'm)"`
`  2313   have th: "{norm (?f x)| x. norm x = 1} = {norm y}"`
`  2291   have th: "{norm (?f x)| x. norm x = 1} = {norm y}"`
`  2314     by(auto intro: vector_choose_size set_ext)`
`  2292     by(auto intro: vector_choose_size set_ext)`
`  2315   show ?thesis`
`  2293   show ?thesis`
`  2316     unfolding onorm_def th`
`  2294     unfolding onorm_def th`
`  2317     apply (rule rsup_unique) by (simp_all  add: setle_def)`
`  2295     apply (rule rsup_unique) by (simp_all  add: setle_def)`
`  2318 qed`
`  2296 qed`
`  2319 `
`  2297 `
`  2320 lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n \<Rightarrow> real ^'m)"`
`  2298 lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \<Rightarrow> real ^'m::finite)"`
`  2321   shows "0 < onorm f \<longleftrightarrow> ~(\<forall>x. f x = 0)"`
`  2299   shows "0 < onorm f \<longleftrightarrow> ~(\<forall>x. f x = 0)"`
`  2322   unfolding onorm_eq_0[OF lf, symmetric]`
`  2300   unfolding onorm_eq_0[OF lf, symmetric]`
`  2323   using onorm_pos_le[OF lf] by arith`
`  2301   using onorm_pos_le[OF lf] by arith`
`  2324 `
`  2302 `
`  2325 lemma onorm_compose:`
`  2303 lemma onorm_compose:`
`  2326   assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" and lg: "linear g"`
`  2304   assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)"`
`       `
`  2305   and lg: "linear (g::real^'k::finite \<Rightarrow> real^'n::finite)"`
`  2327   shows "onorm (f o g) <= onorm f * onorm g"`
`  2306   shows "onorm (f o g) <= onorm f * onorm g"`
`  2328   apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])`
`  2307   apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])`
`  2329   unfolding o_def`
`  2308   unfolding o_def`
`  2330   apply (subst mult_assoc)`
`  2309   apply (subst mult_assoc)`
`  2331   apply (rule order_trans)`
`  2310   apply (rule order_trans)`
`  2333   apply (rule mult_mono1)`
`  2312   apply (rule mult_mono1)`
`  2334   apply (rule onorm(1)[OF lg])`
`  2313   apply (rule onorm(1)[OF lg])`
`  2335   apply (rule onorm_pos_le[OF lf])`
`  2314   apply (rule onorm_pos_le[OF lf])`
`  2336   done`
`  2315   done`
`  2337 `
`  2316 `
`  2338 lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"`
`  2317 lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real^'m::finite)"`
`  2339   shows "onorm (\<lambda>x. - f x) \<le> onorm f"`
`  2318   shows "onorm (\<lambda>x. - f x) \<le> onorm f"`
`  2340   using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]`
`  2319   using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]`
`  2341   unfolding norm_minus_cancel by metis`
`  2320   unfolding norm_minus_cancel by metis`
`  2342 `
`  2321 `
`  2343 lemma onorm_neg: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"`
`  2322 lemma onorm_neg: assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real^'m::finite)"`
`  2344   shows "onorm (\<lambda>x. - f x) = onorm f"`
`  2323   shows "onorm (\<lambda>x. - f x) = onorm f"`
`  2345   using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]`
`  2324   using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]`
`  2346   by simp`
`  2325   by simp`
`  2347 `
`  2326 `
`  2348 lemma onorm_triangle:`
`  2327 lemma onorm_triangle:`
`  2349   assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" and lg: "linear g"`
`  2328   assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)" and lg: "linear g"`
`  2350   shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"`
`  2329   shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"`
`  2351   apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])`
`  2330   apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])`
`  2352   apply (rule order_trans)`
`  2331   apply (rule order_trans)`
`  2353   apply (rule norm_triangle_ineq)`
`  2332   apply (rule norm_triangle_ineq)`
`  2354   apply (simp add: distrib)`
`  2333   apply (simp add: distrib)`
`  2355   apply (rule add_mono)`
`  2334   apply (rule add_mono)`
`  2356   apply (rule onorm(1)[OF lf])`
`  2335   apply (rule onorm(1)[OF lf])`
`  2357   apply (rule onorm(1)[OF lg])`
`  2336   apply (rule onorm(1)[OF lg])`
`  2358   done`
`  2337   done`
`  2359 `
`  2338 `
`  2360 lemma onorm_triangle_le: "linear (f::real ^'n \<Rightarrow> real ^'m) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) <= e`
`  2339 lemma onorm_triangle_le: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) <= e`
`  2361   \<Longrightarrow> onorm(\<lambda>x. f x + g x) <= e"`
`  2340   \<Longrightarrow> onorm(\<lambda>x. f x + g x) <= e"`
`  2362   apply (rule order_trans)`
`  2341   apply (rule order_trans)`
`  2363   apply (rule onorm_triangle)`
`  2342   apply (rule onorm_triangle)`
`  2364   apply assumption+`
`  2343   apply assumption+`
`  2365   done`
`  2344   done`
`  2366 `
`  2345 `
`  2367 lemma onorm_triangle_lt: "linear (f::real ^'n \<Rightarrow> real ^'m) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) < e`
`  2346 lemma onorm_triangle_lt: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) < e`
`  2368   ==> onorm(\<lambda>x. f x + g x) < e"`
`  2347   ==> onorm(\<lambda>x. f x + g x) < e"`
`  2369   apply (rule order_le_less_trans)`
`  2348   apply (rule order_le_less_trans)`
`  2370   apply (rule onorm_triangle)`
`  2349   apply (rule onorm_triangle)`
`  2371   by assumption+`
`  2350   by assumption+`
`  2372 `
`  2351 `
`  2379 `
`  2358 `
`  2380 lemma vec1_component[simp]: "(vec1 x)\$1 = x"`
`  2359 lemma vec1_component[simp]: "(vec1 x)\$1 = x"`
`  2381   by (simp add: vec1_def)`
`  2360   by (simp add: vec1_def)`
`  2382 `
`  2361 `
`  2383 lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"`
`  2362 lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"`
`  2384   by (simp_all add: vec1_def dest_vec1_def Cart_eq Cart_lambda_beta dimindex_def del: One_nat_def)`
`  2363   by (simp_all add: vec1_def dest_vec1_def Cart_eq forall_1)`
`  2385 `
`  2364 `
`  2386 lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))" by (metis vec1_dest_vec1)`
`  2365 lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))" by (metis vec1_dest_vec1)`
`  2387 `
`  2366 `
`  2388 lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))" by (metis vec1_dest_vec1)`
`  2367 lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))" by (metis vec1_dest_vec1)`
`  2389 `
`  2368 `
`  2449 lemma linear_vmul_dest_vec1:`
`  2428 lemma linear_vmul_dest_vec1:`
`  2450   fixes f:: "'a::semiring_1^'n \<Rightarrow> 'a^1"`
`  2429   fixes f:: "'a::semiring_1^'n \<Rightarrow> 'a^1"`
`  2451   shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"`
`  2430   shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"`
`  2452   unfolding dest_vec1_def`
`  2431   unfolding dest_vec1_def`
`  2453   apply (rule linear_vmul_component)`
`  2432   apply (rule linear_vmul_component)`
`  2454   by (auto simp add: dimindex_def)`
`  2433   by auto`
`  2455 `
`  2434 `
`  2456 lemma linear_from_scalars:`
`  2435 lemma linear_from_scalars:`
`  2457   assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^'n)"`
`  2436   assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^'n)"`
`  2458   shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"`
`  2437   shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"`
`  2459   apply (rule ext)`
`  2438   apply (rule ext)`
`  2460   apply (subst matrix_works[OF lf, symmetric])`
`  2439   apply (subst matrix_works[OF lf, symmetric])`
`  2461   apply (auto simp add: Cart_eq matrix_vector_mult_def dest_vec1_def column_def Cart_lambda_beta vector_component dimindex_def mult_commute del: One_nat_def )`
`  2440   apply (auto simp add: Cart_eq matrix_vector_mult_def dest_vec1_def column_def  mult_commute UNIV_1)`
`  2462   done`
`  2441   done`
`  2463 `
`  2442 `
`  2464 lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \<Rightarrow> 'a^1)"`
`  2443 lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n::finite \<Rightarrow> 'a^1)"`
`  2465   shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"`
`  2444   shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"`
`  2466   apply (rule ext)`
`  2445   apply (rule ext)`
`  2467   apply (subst matrix_works[OF lf, symmetric])`
`  2446   apply (subst matrix_works[OF lf, symmetric])`
`  2468   apply (auto simp add: Cart_eq matrix_vector_mult_def vec1_def row_def Cart_lambda_beta vector_component dimindex_def dot_def mult_commute)`
`  2447   apply (simp add: Cart_eq matrix_vector_mult_def vec1_def row_def dot_def mult_commute forall_1)`
`  2469   done`
`  2448   done`
`  2470 `
`  2449 `
`  2471 lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"`
`  2450 lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"`
`  2472   by (simp add: dest_vec1_eq[symmetric])`
`  2451   by (simp add: dest_vec1_eq[symmetric])`
`  2473 `
`  2452 `
`  2483   done`
`  2462   done`
`  2484 `
`  2463 `
`  2485 text{* Pasting vectors. *}`
`  2464 text{* Pasting vectors. *}`
`  2486 `
`  2465 `
`  2487 lemma linear_fstcart: "linear fstcart"`
`  2466 lemma linear_fstcart: "linear fstcart"`
`  2488   by (auto simp add: linear_def fstcart_def Cart_eq Cart_lambda_beta vector_component dimindex_finite_sum)`
`  2467   by (auto simp add: linear_def Cart_eq)`
`  2489 `
`  2468 `
`  2490 lemma linear_sndcart: "linear sndcart"`
`  2469 lemma linear_sndcart: "linear sndcart"`
`  2491   by (auto simp add: linear_def sndcart_def Cart_eq Cart_lambda_beta vector_component dimindex_finite_sum)`
`  2470   by (auto simp add: linear_def Cart_eq)`
`  2492 `
`  2471 `
`  2493 lemma fstcart_vec[simp]: "fstcart(vec x) = vec x"`
`  2472 lemma fstcart_vec[simp]: "fstcart(vec x) = vec x"`
`  2494   by (vector fstcart_def vec_def dimindex_finite_sum)`
`  2473   by (simp add: Cart_eq)`
`  2495 `
`  2474 `
`  2496 lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b,'c) finite_sum) + fstcart y"`
`  2475 lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b + 'c)) + fstcart y"`
`  2497   using linear_fstcart[unfolded linear_def] by blast`
`  2476   by (simp add: Cart_eq)`
`  2498 `
`  2477 `
`  2499 lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b,'c) finite_sum)"`
`  2478 lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b + 'c))"`
`  2500   using linear_fstcart[unfolded linear_def] by blast`
`  2479   by (simp add: Cart_eq)`
`  2501 `
`  2480 `
`  2502 lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^('b,'c) finite_sum)"`
`  2481 lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^('b + 'c))"`
`  2503 unfolding vector_sneg_minus1 fstcart_cmul ..`
`  2482   by (simp add: Cart_eq)`
`  2504 `
`  2483 `
`  2505 lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^('b,'c) finite_sum) - fstcart y"`
`  2484 lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^('b + 'c)) - fstcart y"`
`  2506   unfolding diff_def fstcart_add fstcart_neg  ..`
`  2485   by (simp add: Cart_eq)`
`  2507 `
`  2486 `
`  2508 lemma fstcart_setsum:`
`  2487 lemma fstcart_setsum:`
`  2509   fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"`
`  2488   fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"`
`  2510   assumes fS: "finite S"`
`  2489   assumes fS: "finite S"`
`  2511   shows "fstcart (setsum f S) = setsum (\<lambda>i. fstcart (f i)) S"`
`  2490   shows "fstcart (setsum f S) = setsum (\<lambda>i. fstcart (f i)) S"`
`  2512   by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0)`
`  2491   by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0)`
`  2513 `
`  2492 `
`  2514 lemma sndcart_vec[simp]: "sndcart(vec x) = vec x"`
`  2493 lemma sndcart_vec[simp]: "sndcart(vec x) = vec x"`
`  2515   by (vector sndcart_def vec_def dimindex_finite_sum)`
`  2494   by (simp add: Cart_eq)`
`  2516 `
`  2495 `
`  2517 lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^('b,'c) finite_sum) + sndcart y"`
`  2496 lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^('b + 'c)) + sndcart y"`
`  2518   using linear_sndcart[unfolded linear_def] by blast`
`  2497   by (simp add: Cart_eq)`
`  2519 `
`  2498 `
`  2520 lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^('b,'c) finite_sum)"`
`  2499 lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^('b + 'c))"`
`  2521   using linear_sndcart[unfolded linear_def] by blast`
`  2500   by (simp add: Cart_eq)`
`  2522 `
`  2501 `
`  2523 lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^('b,'c) finite_sum)"`
`  2502 lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^('b + 'c))"`
`  2524 unfolding vector_sneg_minus1 sndcart_cmul ..`
`  2503   by (simp add: Cart_eq)`
`  2525 `
`  2504 `
`  2526 lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^('b,'c) finite_sum) - sndcart y"`
`  2505 lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^('b + 'c)) - sndcart y"`
`  2527   unfolding diff_def sndcart_add sndcart_neg  ..`
`  2506   by (simp add: Cart_eq)`
`  2528 `
`  2507 `
`  2529 lemma sndcart_setsum:`
`  2508 lemma sndcart_setsum:`
`  2530   fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"`
`  2509   fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"`
`  2531   assumes fS: "finite S"`
`  2510   assumes fS: "finite S"`
`  2532   shows "sndcart (setsum f S) = setsum (\<lambda>i. sndcart (f i)) S"`
`  2511   shows "sndcart (setsum f S) = setsum (\<lambda>i. sndcart (f i)) S"`
`  2533   by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0)`
`  2512   by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0)`
`  2534 `
`  2513 `
`  2535 lemma pastecart_vec[simp]: "pastecart (vec x) (vec x) = vec x"`
`  2514 lemma pastecart_vec[simp]: "pastecart (vec x) (vec x) = vec x"`
`  2536   by (simp add: pastecart_eq fstcart_vec sndcart_vec fstcart_pastecart sndcart_pastecart)`
`  2515   by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)`
`  2537 `
`  2516 `
`  2538 lemma pastecart_add[simp]:"pastecart (x1::'a::{plus,times}^_) y1 + pastecart x2 y2 = pastecart (x1 + x2) (y1 + y2)"`
`  2517 lemma pastecart_add[simp]:"pastecart (x1::'a::{plus,times}^_) y1 + pastecart x2 y2 = pastecart (x1 + x2) (y1 + y2)"`
`  2539   by (simp add: pastecart_eq fstcart_add sndcart_add fstcart_pastecart sndcart_pastecart)`
`  2518   by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)`
`  2540 `
`  2519 `
`  2541 lemma pastecart_cmul[simp]: "pastecart (c *s (x1::'a::{plus,times}^_)) (c *s y1) = c *s pastecart x1 y1"`
`  2520 lemma pastecart_cmul[simp]: "pastecart (c *s (x1::'a::{plus,times}^_)) (c *s y1) = c *s pastecart x1 y1"`
`  2542   by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)`
`  2521   by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)`
`  2543 `
`  2522 `
`  2544 lemma pastecart_neg[simp]: "pastecart (- (x::'a::ring_1^_)) (- y) = - pastecart x y"`
`  2523 lemma pastecart_neg[simp]: "pastecart (- (x::'a::ring_1^_)) (- y) = - pastecart x y"`
`  2551   fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"`
`  2530   fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"`
`  2552   assumes fS: "finite S"`
`  2531   assumes fS: "finite S"`
`  2553   shows "pastecart (setsum f S) (setsum g S) = setsum (\<lambda>i. pastecart (f i) (g i)) S"`
`  2532   shows "pastecart (setsum f S) (setsum g S) = setsum (\<lambda>i. pastecart (f i) (g i)) S"`
`  2554   by (simp  add: pastecart_eq fstcart_setsum[OF fS] sndcart_setsum[OF fS] fstcart_pastecart sndcart_pastecart)`
`  2533   by (simp  add: pastecart_eq fstcart_setsum[OF fS] sndcart_setsum[OF fS] fstcart_pastecart sndcart_pastecart)`
`  2555 `
`  2534 `
`  2556 lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n,'m) finite_sum)"`
`  2535 lemma setsum_Plus:`
`  2557 proof-`
`  2536   "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow>`
`  2558   let ?n = "dimindex (UNIV :: 'n set)"`
`  2537     (\<Sum>x\<in>A <+> B. g x) = (\<Sum>x\<in>A. g (Inl x)) + (\<Sum>x\<in>B. g (Inr x))"`
`  2559   let ?m = "dimindex (UNIV :: 'm set)"`
`  2538   unfolding Plus_def`
`  2560   let ?N = "{1 .. ?n}"`
`  2539   by (subst setsum_Un_disjoint, auto simp add: setsum_reindex)`
`  2561   let ?M = "{1 .. ?m}"`
`  2540 `
`  2562   let ?NM = "{1 .. dimindex (UNIV :: ('n,'m) finite_sum set)}"`
`  2541 lemma setsum_UNIV_sum:`
`  2563   have th_0: "1 \<le> ?n +1" by simp`
`  2542   fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"`
`       `
`  2543   shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"`
`       `
`  2544   apply (subst UNIV_Plus_UNIV [symmetric])`
`       `
`  2545   apply (rule setsum_Plus [OF finite finite])`
`       `
`  2546   done`
`       `
`  2547 `
`       `
`  2548 lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n::finite + 'm::finite))"`
`       `
`  2549 proof-`
`  2564   have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"`
`  2550   have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"`
`  2565     by (simp add: pastecart_fst_snd)`
`  2551     by (simp add: pastecart_fst_snd)`
`  2566   have th1: "fstcart x \<bullet> fstcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"`
`  2552   have th1: "fstcart x \<bullet> fstcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"`
`  2567     by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square del: One_nat_def)`
`  2553     by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg)`
`  2568   then show ?thesis`
`  2554   then show ?thesis`
`  2569     unfolding th0`
`  2555     unfolding th0`
`  2570     unfolding real_vector_norm_def real_sqrt_le_iff id_def`
`  2556     unfolding real_vector_norm_def real_sqrt_le_iff id_def`
`  2571     by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)`
`  2557     by (simp add: dot_def)`
`  2572 qed`
`  2558 qed`
`  2573 `
`  2559 `
`  2574 lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"`
`  2560 lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"`
`  2575   by (metis dist_def fstcart_sub[symmetric] norm_fstcart)`
`  2561   by (metis dist_def fstcart_sub[symmetric] norm_fstcart)`
`  2576 `
`  2562 `
`  2577 lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n,'m) finite_sum)"`
`  2563 lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"`
`  2578 proof-`
`  2564 proof-`
`  2579   let ?n = "dimindex (UNIV :: 'n set)"`
`       `
`  2580   let ?m = "dimindex (UNIV :: 'm set)"`
`       `
`  2581   let ?N = "{1 .. ?n}"`
`       `
`  2582   let ?M = "{1 .. ?m}"`
`       `
`  2583   let ?nm = "dimindex (UNIV :: ('n,'m) finite_sum set)"`
`       `
`  2584   let ?NM = "{1 .. ?nm}"`
`       `
`  2585   have thnm[simp]: "?nm = ?n + ?m" by (simp add: dimindex_finite_sum)`
`       `
`  2586   have th_0: "1 \<le> ?n +1" by simp`
`       `
`  2587   have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"`
`  2565   have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"`
`  2588     by (simp add: pastecart_fst_snd)`
`  2566     by (simp add: pastecart_fst_snd)`
`  2598   have th1: "sndcart x \<bullet> sndcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"`
`  2567   have th1: "sndcart x \<bullet> sndcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"`
`  2599     by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square setsum_reindex[OF finj, unfolded fS] del: One_nat_def)`
`  2568     by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg)`
`  2600   then show ?thesis`
`  2569   then show ?thesis`
`  2601     unfolding th0`
`  2570     unfolding th0`
`  2602     unfolding real_vector_norm_def real_sqrt_le_iff id_def`
`  2571     unfolding real_vector_norm_def real_sqrt_le_iff id_def`
`  2603     by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)`
`  2572     by (simp add: dot_def)`
`  2604 qed`
`  2573 qed`
`  2605 `
`  2574 `
`  2606 lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"`
`  2575 lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"`
`  2607   by (metis dist_def sndcart_sub[symmetric] norm_sndcart)`
`  2576   by (metis dist_def sndcart_sub[symmetric] norm_sndcart)`
`  2608 `
`  2577 `
`  2609 lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n) (x2::'a::{times,comm_monoid_add}^'m)) \<bullet> (pastecart y1 y2) =  x1 \<bullet> y1 + x2 \<bullet> y2"`
`  2578 lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \<bullet> (pastecart y1 y2) =  x1 \<bullet> y1 + x2 \<bullet> y2"`
`  2610 proof-`
`  2579   by (simp add: dot_def setsum_UNIV_sum pastecart_def)`
`  2611   let ?n = "dimindex (UNIV :: 'n set)"`
`  2580 `
`  2612   let ?m = "dimindex (UNIV :: 'm set)"`
`  2581 lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ 'm::finite) + norm(y::real^'n::finite)"`
`  2613   let ?N = "{1 .. ?n}"`
`       `
`  2614   let ?M = "{1 .. ?m}"`
`       `
`  2615   let ?nm = "dimindex (UNIV :: ('n,'m) finite_sum set)"`
`       `
`  2616   let ?NM = "{1 .. ?nm}"`
`       `
`  2617   have thnm: "?nm = ?n + ?m" by (simp add: dimindex_finite_sum)`
`       `
`  2618   have th_0: "1 \<le> ?n +1" by simp`
`       `
`  2619   have th_1: "\<And>i. i \<in> {?m + 1 .. ?nm} \<Longrightarrow> i - ?m \<in> ?N" apply (simp add: thnm) by arith`
`       `
`  2620   let ?f = "\<lambda>a b i. (a\$i) * (b\$i)"`
`       `
`  2621   let ?g = "?f (pastecart x1 x2) (pastecart y1 y2)"`
`       `
`  2622   let ?S = "{?n +1 .. ?nm}"`
`       `
`  2623   {fix i`
`       `
`  2624     assume i: "i \<in> ?N"`
`       `
`  2625     have "?g i = ?f x1 y1 i"`
`       `
`  2626       using i`
`       `
`  2627       apply (simp add: pastecart_def Cart_lambda_beta thnm) done`
`       `
`  2628   }`
`       `
`  2629   hence th2: "setsum ?g ?N = setsum (?f x1 y1) ?N"`
`       `
`  2630     apply -`
`       `
`  2631     apply (rule setsum_cong)`
`       `
`  2632     apply auto`
`       `
`  2633     done`
`       `
`  2634   {fix i`
`       `
`  2635     assume i: "i \<in> ?S"`
`       `
`  2636     have "?g i = ?f x2 y2 (i - ?n)"`
`       `
`  2637       using i`
`       `
`  2638       apply (simp add: pastecart_def Cart_lambda_beta thnm) done`
`       `
`  2639   }`
`       `
`  2640   hence th3: "setsum ?g ?S = setsum (\<lambda>i. ?f x2 y2 (i -?n)) ?S"`
`       `
`  2641     apply -`
`       `
`  2642     apply (rule setsum_cong)`
`       `
`  2643     apply auto`
`       `
`  2644     done`
`       `
`  2645   let ?r = "\<lambda>n. n - ?n"`
`       `
`  2646   have rinj: "inj_on ?r ?S" apply (simp add: inj_on_def Ball_def thnm) by arith`
`       `
`  2647   have rS: "?r ` ?S = ?M" apply (rule set_ext)`
`       `
`  2648     apply (simp add: thnm image_iff Bex_def) by arith`
`       `
`  2649   have "pastecart x1 x2 \<bullet> (pastecart y1 y2) = setsum ?g ?NM" by (simp add: dot_def)`
`       `
`  2650   also have "\<dots> = setsum ?g ?N + setsum ?g ?S"`
`       `
`  2651     by (simp add: dot_def thnm setsum_add_split[OF th_0, of _ ?m] del: One_nat_def)`
`       `
`  2652   also have "\<dots> = setsum (?f x1 y1) ?N + setsum (?f x2 y2) ?M"`
`       `
`  2653     unfolding setsum_reindex[OF rinj, unfolded rS o_def] th2 th3 ..`
`       `
`  2654   finally`
`       `
`  2655   show ?thesis by (simp add: dot_def)`
`       `
`  2656 qed`
`       `
`  2657 `
`       `
`  2658 lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ _) + norm(y)"`
`       `
`  2659   unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def`
`  2582   unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def`
`  2660   apply (rule power2_le_imp_le)`
`  2583   apply (rule power2_le_imp_le)`
`  2661   apply (simp add: real_sqrt_pow2[OF add_nonneg_nonneg[OF dot_pos_le[of x] dot_pos_le[of y]]])`
`  2584   apply (simp add: real_sqrt_pow2[OF add_nonneg_nonneg[OF dot_pos_le[of x] dot_pos_le[of y]]])`
`  2662   apply (auto simp add: power2_eq_square ring_simps)`
`  2585   apply (auto simp add: power2_eq_square ring_simps)`
`  2663   apply (simp add: power2_eq_square[symmetric])`
`  2586   apply (simp add: power2_eq_square[symmetric])`
`  3417 qed`
`  3340 qed`
`  3418 `
`  3341 `
`  3419 `
`  3342 `
`  3420 (* Standard bases are a spanning set, and obviously finite.                  *)`
`  3343 (* Standard bases are a spanning set, and obviously finite.                  *)`
`  3421 `
`  3344 `
`  3422 lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n | i. i \<in> {1 .. dimindex(UNIV :: 'n set)}} = UNIV"`
`  3345 lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n::finite | i. i \<in> (UNIV :: 'n set)} = UNIV"`
`  3423 apply (rule set_ext)`
`  3346 apply (rule set_ext)`
`  3424 apply auto`
`  3347 apply auto`
`  3425 apply (subst basis_expansion[symmetric])`
`  3348 apply (subst basis_expansion[symmetric])`
`  3426 apply (rule span_setsum)`
`  3349 apply (rule span_setsum)`
`  3427 apply simp`
`  3350 apply simp`
`  3429 apply (rule span_mul)`
`  3352 apply (rule span_mul)`
`  3430 apply (rule span_superset)`
`  3353 apply (rule span_superset)`
`  3431 apply (auto simp add: Collect_def mem_def)`
`  3354 apply (auto simp add: Collect_def mem_def)`
`  3432 done`
`  3355 done`
`  3433 `
`  3356 `
`  3434 `
`  3357 lemma has_size_stdbasis: "{basis i ::real ^'n::finite | i. i \<in> (UNIV :: 'n set)} hassize CARD('n)" (is "?S hassize ?n")`
`  3435 lemma has_size_stdbasis: "{basis i ::real ^'n | i. i \<in> {1 .. dimindex (UNIV :: 'n set)}} hassize (dimindex(UNIV :: 'n set))" (is "?S hassize ?n")`
`  3358 proof-`
`  3436 proof-`
`  3359   have eq: "?S = basis ` UNIV" by blast`
`  3437   have eq: "?S = basis ` {1 .. ?n}" by blast`
`       `
`  3438   show ?thesis unfolding eq`
`  3360   show ?thesis unfolding eq`
`  3439     apply (rule hassize_image_inj[OF basis_inj])`
`  3361     apply (rule hassize_image_inj[OF basis_inj])`
`  3440     by (simp add: hassize_def)`
`  3362     by (simp add: hassize_def)`
`  3441 qed`
`  3363 qed`
`  3442 `
`  3364 `
`  3443 lemma finite_stdbasis: "finite {basis i ::real^'n |i. i\<in> {1 .. dimindex(UNIV:: 'n set)}}"`
`  3365 lemma finite_stdbasis: "finite {basis i ::real^'n::finite |i. i\<in> (UNIV:: 'n set)}"`
`  3444   using has_size_stdbasis[unfolded hassize_def]`
`  3366   using has_size_stdbasis[unfolded hassize_def]`
`  3445   ..`
`  3367   ..`
`  3446 `
`  3368 `
`  3447 lemma card_stdbasis: "card {basis i ::real^'n |i. i\<in> {1 .. dimindex(UNIV :: 'n set)}} = dimindex(UNIV :: 'n set)"`
`  3369 lemma card_stdbasis: "card {basis i ::real^'n::finite |i. i\<in> (UNIV :: 'n set)} = CARD('n)"`
`  3448   using has_size_stdbasis[unfolded hassize_def]`
`  3370   using has_size_stdbasis[unfolded hassize_def]`
`  3449   ..`
`  3371   ..`
`  3450 `
`  3372 `
`  3451 lemma independent_stdbasis_lemma:`
`  3373 lemma independent_stdbasis_lemma:`
`  3452   assumes x: "(x::'a::semiring_1 ^ 'n) \<in> span (basis ` S)"`
`  3374   assumes x: "(x::'a::semiring_1 ^ 'n) \<in> span (basis ` S)"`
`  3454   and iS: "i \<notin> S"`
`  3375   and iS: "i \<notin> S"`
`  3455   shows "(x\$i) = 0"`
`  3376   shows "(x\$i) = 0"`
`  3456 proof-`
`  3377 proof-`
`  3457   let ?n = "dimindex (UNIV :: 'n set)"`
`  3378   let ?U = "UNIV :: 'n set"`
`  3458   let ?U = "{1 .. ?n}"`
`       `
`  3459   let ?B = "basis ` S"`
`  3379   let ?B = "basis ` S"`
`  3460   let ?P = "\<lambda>(x::'a^'n). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x\$i =0"`
`  3380   let ?P = "\<lambda>(x::'a^'n). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x\$i =0"`
`  3461  {fix x::"'a^'n" assume xS: "x\<in> ?B"`
`  3381  {fix x::"'a^'n" assume xS: "x\<in> ?B"`
`  3462    from xS have "?P x" by (auto simp add: basis_component)}`
`  3382    from xS have "?P x" by auto}`
`  3463  moreover`
`  3383  moreover`
`  3464  have "subspace ?P"`
`  3384  have "subspace ?P"`
`  3465    by (auto simp add: subspace_def Collect_def mem_def zero_index vector_component)`
`  3385    by (auto simp add: subspace_def Collect_def mem_def)`
`  3466  ultimately show ?thesis`
`  3386  ultimately show ?thesis`
`  3467    using x span_induct[of ?B ?P x] i iS by blast`
`  3387    using x span_induct[of ?B ?P x] iS by blast`
`  3468 qed`
`  3388 qed`
`  3469 `
`  3389 `
`  3470 lemma independent_stdbasis: "independent {basis i ::real^'n |i. i\<in> {1 .. dimindex(UNIV :: 'n set)}}"`
`  3390 lemma independent_stdbasis: "independent {basis i ::real^'n::finite |i. i\<in> (UNIV :: 'n set)}"`
`  3471 proof-`
`  3391 proof-`
`  3472   let ?n = "dimindex (UNIV :: 'n set)"`
`  3392   let ?I = "UNIV :: 'n set"`
`  3473   let ?I = "{1 .. ?n}"`
`  3393   let ?b = "basis :: _ \<Rightarrow> real ^'n"`
`  3474   let ?b = "basis :: nat \<Rightarrow> real ^'n"`
`       `
`  3475   let ?B = "?b ` ?I"`
`  3394   let ?B = "?b ` ?I"`
`  3476   have eq: "{?b i|i. i \<in> ?I} = ?B"`
`  3395   have eq: "{?b i|i. i \<in> ?I} = ?B"`
`  3477     by auto`
`  3396     by auto`
`  3478   {assume d: "dependent ?B"`
`  3397   {assume d: "dependent ?B"`
`  3479     then obtain k where k: "k \<in> ?I" "?b k \<in> span (?B - {?b k})"`
`  3398     then obtain k where k: "k \<in> ?I" "?b k \<in> span (?B - {?b k})"`
`  3482     have eq2: "?B - {?b k} = ?b ` (?I - {k})"`
`  3401     have eq2: "?B - {?b k} = ?b ` (?I - {k})"`
`  3483       unfolding eq1`
`  3402       unfolding eq1`
`  3484       apply (rule inj_on_image_set_diff[symmetric])`
`  3403       apply (rule inj_on_image_set_diff[symmetric])`
`  3485       apply (rule basis_inj) using k(1) by auto`
`  3404       apply (rule basis_inj) using k(1) by auto`
`  3486     from k(2) have th0: "?b k \<in> span (?b ` (?I - {k}))" unfolding eq2 .`
`  3405     from k(2) have th0: "?b k \<in> span (?b ` (?I - {k}))" unfolding eq2 .`
`  3487     from independent_stdbasis_lemma[OF th0 k(1), simplified]`
`  3406     from independent_stdbasis_lemma[OF th0, of k, simplified]`
`  3488     have False by (simp add: basis_component[OF k(1), of k])}`
`  3407     have False by simp}`
`  3489   then show ?thesis unfolding eq dependent_def ..`
`  3408   then show ?thesis unfolding eq dependent_def ..`
`  3490 qed`
`  3409 qed`
`  3491 `
`  3410 `
`  3492 (* This is useful for building a basis step-by-step.                         *)`
`  3411 (* This is useful for building a basis step-by-step.                         *)`
`  3493 `
`  3412 `
`  3663     apply (rule finite_imageI)`
`  3582     apply (rule finite_imageI)`
`  3664     apply (rule finite_intvl)`
`  3583     apply (rule finite_intvl)`
`  3665     done`
`  3584     done`
`  3666 qed`
`  3585 qed`
`  3667 `
`  3586 `
`  3668 lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> {(i::nat) .. j}}"`
`  3587 lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"`
`  3669 proof-`
`  3588 proof-`
`  3670   have eq: "{f x |x. x\<in> {i .. j}} = f ` {i .. j}" by auto`
`  3589   have eq: "{f x |x. x\<in> UNIV} = f ` UNIV" by auto`
`  3671   show ?thesis unfolding eq`
`  3590   show ?thesis unfolding eq`
`  3672     apply (rule finite_imageI)`
`  3591     apply (rule finite_imageI)`
`  3673     apply (rule finite_atLeastAtMost)`
`  3592     apply (rule finite)`
`  3674     done`
`  3593     done`
`  3675 qed`
`  3594 qed`
`  3676 `
`  3595 `
`  3677 `
`  3596 `
`  3678 lemma independent_bound:`
`  3597 lemma independent_bound:`
`  3679   fixes S:: "(real^'n) set"`
`  3598   fixes S:: "(real^'n::finite) set"`
`  3680   shows "independent S \<Longrightarrow> finite S \<and> card S <= dimindex(UNIV :: 'n set)"`
`  3599   shows "independent S \<Longrightarrow> finite S \<and> card S <= CARD('n)"`
`  3681   apply (subst card_stdbasis[symmetric])`
`  3600   apply (subst card_stdbasis[symmetric])`
`  3682   apply (rule independent_span_bound)`
`  3601   apply (rule independent_span_bound)`
`  3683   apply (rule finite_Atleast_Atmost_nat)`
`  3602   apply (rule finite_Atleast_Atmost_nat)`
`  3684   apply assumption`
`  3603   apply assumption`
`  3685   unfolding span_stdbasis`
`  3604   unfolding span_stdbasis`
`  3686   apply (rule subset_UNIV)`
`  3605   apply (rule subset_UNIV)`
`  3687   done`
`  3606   done`
`  3688 `
`  3607 `
`  3689 lemma dependent_biggerset: "(finite (S::(real ^'n) set) ==> card S > dimindex(UNIV:: 'n set)) ==> dependent S"`
`  3608 lemma dependent_biggerset: "(finite (S::(real ^'n::finite) set) ==> card S > CARD('n)) ==> dependent S"`
`  3690   by (metis independent_bound not_less)`
`  3609   by (metis independent_bound not_less)`
`  3691 `
`  3610 `
`  3692 (* Hence we can create a maximal independent subset.                         *)`
`  3611 (* Hence we can create a maximal independent subset.                         *)`
`  3693 `
`  3612 `
`  3694 lemma maximal_independent_subset_extend:`
`  3613 lemma maximal_independent_subset_extend:`
`  3695   assumes sv: "(S::(real^'n) set) \<subseteq> V" and iS: "independent S"`
`  3614   assumes sv: "(S::(real^'n::finite) set) \<subseteq> V" and iS: "independent S"`
`  3696   shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"`
`  3615   shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"`
`  3697   using sv iS`
`  3616   using sv iS`
`  3698 proof(induct d\<equiv> "dimindex (UNIV :: 'n set) - card S" arbitrary: S rule: nat_less_induct)`
`  3617 proof(induct d\<equiv> "CARD('n) - card S" arbitrary: S rule: nat_less_induct)`
`  3699   fix n and S:: "(real^'n) set"`
`  3618   fix n and S:: "(real^'n) set"`
`  3700   assume H: "\<forall>m<n. \<forall>S \<subseteq> V. independent S \<longrightarrow> m = dimindex (UNIV::'n set) - card S \<longrightarrow>`
`  3619   assume H: "\<forall>m<n. \<forall>S \<subseteq> V. independent S \<longrightarrow> m = CARD('n) - card S \<longrightarrow>`
`  3701               (\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B)"`
`  3620               (\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B)"`
`  3702     and sv: "S \<subseteq> V" and i: "independent S" and n: "n = dimindex (UNIV :: 'n set) - card S"`
`  3621     and sv: "S \<subseteq> V" and i: "independent S" and n: "n = CARD('n) - card S"`
`  3703   let ?P = "\<lambda>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"`
`  3622   let ?P = "\<lambda>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"`
`  3704   let ?ths = "\<exists>x. ?P x"`
`  3623   let ?ths = "\<exists>x. ?P x"`
`  3705   let ?d = "dimindex (UNIV :: 'n set)"`
`  3624   let ?d = "CARD('n)"`
`  3706   {assume "V \<subseteq> span S"`
`  3625   {assume "V \<subseteq> span S"`
`  3707     then have ?ths  using sv i by blast }`
`  3626     then have ?ths  using sv i by blast }`
`  3708   moreover`
`  3627   moreover`
`  3709   {assume VS: "\<not> V \<subseteq> span S"`
`  3628   {assume VS: "\<not> V \<subseteq> span S"`
`  3710     from VS obtain a where a: "a \<in> V" "a \<notin> span S" by blast`
`  3629     from VS obtain a where a: "a \<in> V" "a \<notin> span S" by blast`
`  3711     from a have aS: "a \<notin> S" by (auto simp add: span_superset)`
`  3630     from a have aS: "a \<notin> S" by (auto simp add: span_superset)`
`  3712     have th0: "insert a S \<subseteq> V" using a sv by blast`
`  3631     have th0: "insert a S \<subseteq> V" using a sv by blast`
`  3713     from independent_insert[of a S]  i a`
`  3632     from independent_insert[of a S]  i a`
`  3714     have th1: "independent (insert a S)" by auto`
`  3633     have th1: "independent (insert a S)" by auto`
`  3715     have mlt: "?d - card (insert a S) < n"`
`  3634     have mlt: "?d - card (insert a S) < n"`
`  3716       using aS a n independent_bound[OF th1] dimindex_ge_1[of "UNIV :: 'n set"]`
`  3635       using aS a n independent_bound[OF th1]`
`  3717       by auto`
`  3636       by auto`
`  3718 `
`  3637 `
`  3719     from H[rule_format, OF mlt th0 th1 refl]`
`  3638     from H[rule_format, OF mlt th0 th1 refl]`
`  3720     obtain B where B: "insert a S \<subseteq> B" "B \<subseteq> V" "independent B" " V \<subseteq> span B"`
`  3639     obtain B where B: "insert a S \<subseteq> B" "B \<subseteq> V" "independent B" " V \<subseteq> span B"`
`  3721       by blast`
`  3640       by blast`
`  3723     then have ?ths by blast}`
`  3642     then have ?ths by blast}`
`  3724   ultimately show ?ths by blast`
`  3643   ultimately show ?ths by blast`
`  3725 qed`
`  3644 qed`
`  3726 `
`  3645 `
`  3727 lemma maximal_independent_subset:`
`  3646 lemma maximal_independent_subset:`
`  3728   "\<exists>(B:: (real ^'n) set). B\<subseteq> V \<and> independent B \<and> V \<subseteq> span B"`
`  3647   "\<exists>(B:: (real ^'n::finite) set). B\<subseteq> V \<and> independent B \<and> V \<subseteq> span B"`
`  3729   by (metis maximal_independent_subset_extend[of "{}:: (real ^'n) set"] empty_subsetI independent_empty)`
`  3648   by (metis maximal_independent_subset_extend[of "{}:: (real ^'n) set"] empty_subsetI independent_empty)`
`  3730 `
`  3649 `
`  3731 (* Notion of dimension.                                                      *)`
`  3650 (* Notion of dimension.                                                      *)`
`  3732 `
`  3651 `
`  3733 definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (B hassize n))"`
`  3652 definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (B hassize n))"`
`  3734 `
`  3653 `
`  3735 lemma basis_exists:  "\<exists>B. (B :: (real ^'n) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (B hassize dim V)"`
`  3654 lemma basis_exists:  "\<exists>B. (B :: (real ^'n::finite) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (B hassize dim V)"`
`  3736 unfolding dim_def some_eq_ex[of "\<lambda>n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (B hassize n)"]`
`  3655 unfolding dim_def some_eq_ex[of "\<lambda>n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (B hassize n)"]`
`  3737 unfolding hassize_def`
`  3656 unfolding hassize_def`
`  3738 using maximal_independent_subset[of V] independent_bound`
`  3657 using maximal_independent_subset[of V] independent_bound`
`  3739 by auto`
`  3658 by auto`
`  3740 `
`  3659 `
`  3741 (* Consequences of independence or spanning for cardinality.                 *)`
`  3660 (* Consequences of independence or spanning for cardinality.                 *)`
`  3742 `
`  3661 `
`  3743 lemma independent_card_le_dim: "(B::(real ^'n) set) \<subseteq> V \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B \<le> dim V"`
`  3662 lemma independent_card_le_dim: "(B::(real ^'n::finite) set) \<subseteq> V \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B \<le> dim V"`
`  3744 by (metis basis_exists[of V] independent_span_bound[where ?'a=real] hassize_def subset_trans)`
`  3663 by (metis basis_exists[of V] independent_span_bound[where ?'a=real] hassize_def subset_trans)`
`  3745 `
`  3664 `
`  3746 lemma span_card_ge_dim:  "(B::(real ^'n) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B"`
`  3665 lemma span_card_ge_dim:  "(B::(real ^'n::finite) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B"`
`  3747   by (metis basis_exists[of V] independent_span_bound hassize_def subset_trans)`
`  3666   by (metis basis_exists[of V] independent_span_bound hassize_def subset_trans)`
`  3748 `
`  3667 `
`  3749 lemma basis_card_eq_dim:`
`  3668 lemma basis_card_eq_dim:`
`  3750   "B \<subseteq> (V:: (real ^'n) set) \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"`
`  3669   "B \<subseteq> (V:: (real ^'n::finite) set) \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"`
`  3751   by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_mono)`
`  3670   by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_mono)`
`  3752 `
`  3671 `
`  3753 lemma dim_unique: "(B::(real ^'n) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> B hassize n \<Longrightarrow> dim V = n"`
`  3672 lemma dim_unique: "(B::(real ^'n::finite) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> B hassize n \<Longrightarrow> dim V = n"`
`  3754   by (metis basis_card_eq_dim hassize_def)`
`  3673   by (metis basis_card_eq_dim hassize_def)`
`  3755 `
`  3674 `
`  3756 (* More lemmas about dimension.                                              *)`
`  3675 (* More lemmas about dimension.                                              *)`
`  3757 `
`  3676 `
`  3758 lemma dim_univ: "dim (UNIV :: (real^'n) set) = dimindex (UNIV :: 'n set)"`
`  3677 lemma dim_univ: "dim (UNIV :: (real^'n::finite) set) = CARD('n)"`
`  3759   apply (rule dim_unique[of "{basis i |i. i\<in> {1 .. dimindex (UNIV :: 'n set)}}"])`
`  3678   apply (rule dim_unique[of "{basis i |i. i\<in> (UNIV :: 'n set)}"])`
`  3760   by (auto simp only: span_stdbasis has_size_stdbasis independent_stdbasis)`
`  3679   by (auto simp only: span_stdbasis has_size_stdbasis independent_stdbasis)`
`  3761 `
`  3680 `
`  3762 lemma dim_subset:`
`  3681 lemma dim_subset:`
`  3763   "(S:: (real ^'n) set) \<subseteq> T \<Longrightarrow> dim S \<le> dim T"`
`  3682   "(S:: (real ^'n::finite) set) \<subseteq> T \<Longrightarrow> dim S \<le> dim T"`
`  3764   using basis_exists[of T] basis_exists[of S]`
`  3683   using basis_exists[of T] basis_exists[of S]`
`  3765   by (metis independent_span_bound[where ?'a = real and ?'n = 'n] subset_eq hassize_def)`
`  3684   by (metis independent_span_bound[where ?'a = real and ?'n = 'n] subset_eq hassize_def)`
`  3766 `
`  3685 `
`  3767 lemma dim_subset_univ: "dim (S:: (real^'n) set) \<le> dimindex (UNIV :: 'n set)"`
`  3686 lemma dim_subset_univ: "dim (S:: (real^'n::finite) set) \<le> CARD('n)"`
`  3768   by (metis dim_subset subset_UNIV dim_univ)`
`  3687   by (metis dim_subset subset_UNIV dim_univ)`
`  3769 `
`  3688 `
`  3770 (* Converses to those.                                                       *)`
`  3689 (* Converses to those.                                                       *)`
`  3771 `
`  3690 `
`  3772 lemma card_ge_dim_independent:`
`  3691 lemma card_ge_dim_independent:`
`  3773   assumes BV:"(B::(real ^'n) set) \<subseteq> V" and iB:"independent B" and dVB:"dim V \<le> card B"`
`  3692   assumes BV:"(B::(real ^'n::finite) set) \<subseteq> V" and iB:"independent B" and dVB:"dim V \<le> card B"`
`  3774   shows "V \<subseteq> span B"`
`  3693   shows "V \<subseteq> span B"`
`  3775 proof-`
`  3694 proof-`
`  3776   {fix a assume aV: "a \<in> V"`
`  3695   {fix a assume aV: "a \<in> V"`
`  3777     {assume aB: "a \<notin> span B"`
`  3696     {assume aB: "a \<notin> span B"`
`  3778       then have iaB: "independent (insert a B)" using iB aV  BV by (simp add: independent_insert)`
`  3697       then have iaB: "independent (insert a B)" using iB aV  BV by (simp add: independent_insert)`
`  3782     then have "a \<in> span B"  by blast}`
`  3701     then have "a \<in> span B"  by blast}`
`  3783   then show ?thesis by blast`
`  3702   then show ?thesis by blast`
`  3784 qed`
`  3703 qed`
`  3785 `
`  3704 `
`  3786 lemma card_le_dim_spanning:`
`  3705 lemma card_le_dim_spanning:`
`  3787   assumes BV: "(B:: (real ^'n) set) \<subseteq> V" and VB: "V \<subseteq> span B"`
`  3706   assumes BV: "(B:: (real ^'n::finite) set) \<subseteq> V" and VB: "V \<subseteq> span B"`
`  3788   and fB: "finite B" and dVB: "dim V \<ge> card B"`
`  3707   and fB: "finite B" and dVB: "dim V \<ge> card B"`
`  3789   shows "independent B"`
`  3708   shows "independent B"`
`  3790 proof-`
`  3709 proof-`
`  3791   {fix a assume a: "a \<in> B" "a \<in> span (B -{a})"`
`  3710   {fix a assume a: "a \<in> B" "a \<in> span (B -{a})"`
`  3792     from a fB have c0: "card B \<noteq> 0" by auto`
`  3711     from a fB have c0: "card B \<noteq> 0" by auto`
`  3803     have c: "dim V \<le> card (B -{a})" .`
`  3722     have c: "dim V \<le> card (B -{a})" .`
`  3804     from c c0 dVB cb have False by simp}`
`  3723     from c c0 dVB cb have False by simp}`
`  3805   then show ?thesis unfolding dependent_def by blast`
`  3724   then show ?thesis unfolding dependent_def by blast`
`  3806 qed`
`  3725 qed`
`  3807 `
`  3726 `
`  3808 lemma card_eq_dim: "(B:: (real ^'n) set) \<subseteq> V \<Longrightarrow> B hassize dim V \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"`
`  3727 lemma card_eq_dim: "(B:: (real ^'n::finite) set) \<subseteq> V \<Longrightarrow> B hassize dim V \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"`
`  3809   by (metis hassize_def order_eq_iff card_le_dim_spanning`
`  3728   by (metis hassize_def order_eq_iff card_le_dim_spanning`
`  3810     card_ge_dim_independent)`
`  3729     card_ge_dim_independent)`
`  3811 `
`  3730 `
`  3812 (* ------------------------------------------------------------------------- *)`
`  3731 (* ------------------------------------------------------------------------- *)`
`  3813 (* More general size bound lemmas.                                           *)`
`  3732 (* More general size bound lemmas.                                           *)`
`  3814 (* ------------------------------------------------------------------------- *)`
`  3733 (* ------------------------------------------------------------------------- *)`
`  3815 `
`  3734 `
`  3816 lemma independent_bound_general:`
`  3735 lemma independent_bound_general:`
`  3817   "independent (S:: (real^'n) set) \<Longrightarrow> finite S \<and> card S \<le> dim S"`
`  3736   "independent (S:: (real^'n::finite) set) \<Longrightarrow> finite S \<and> card S \<le> dim S"`
`  3818   by (metis independent_card_le_dim independent_bound subset_refl)`
`  3737   by (metis independent_card_le_dim independent_bound subset_refl)`
`  3819 `
`  3738 `
`  3820 lemma dependent_biggerset_general: "(finite (S:: (real^'n) set) \<Longrightarrow> card S > dim S) \<Longrightarrow> dependent S"`
`  3739 lemma dependent_biggerset_general: "(finite (S:: (real^'n::finite) set) \<Longrightarrow> card S > dim S) \<Longrightarrow> dependent S"`
`  3821   using independent_bound_general[of S] by (metis linorder_not_le)`
`  3740   using independent_bound_general[of S] by (metis linorder_not_le)`
`  3822 `
`  3741 `
`  3823 lemma dim_span: "dim (span (S:: (real ^'n) set)) = dim S"`
`  3742 lemma dim_span: "dim (span (S:: (real ^'n::finite) set)) = dim S"`
`  3824 proof-`
`  3743 proof-`
`  3825   have th0: "dim S \<le> dim (span S)"`
`  3744   have th0: "dim S \<le> dim (span S)"`
`  3826     by (auto simp add: subset_eq intro: dim_subset span_superset)`
`  3745     by (auto simp add: subset_eq intro: dim_subset span_superset)`
`  3827   from basis_exists[of S]`
`  3746   from basis_exists[of S]`
`  3828   obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "B hassize dim S" by blast`
`  3747   obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "B hassize dim S" by blast`
`  3831   have sssB: "span S \<subseteq> span B" using span_mono[OF B(3)] by (simp add: span_span)`
`  3750   have sssB: "span S \<subseteq> span B" using span_mono[OF B(3)] by (simp add: span_span)`
`  3832   from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis`
`  3751   from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis`
`  3833     using fB(2)  by arith`
`  3752     using fB(2)  by arith`
`  3834 qed`
`  3753 qed`
`  3835 `
`  3754 `
`  3836 lemma subset_le_dim: "(S:: (real ^'n) set) \<subseteq> span T \<Longrightarrow> dim S \<le> dim T"`
`  3755 lemma subset_le_dim: "(S:: (real ^'n::finite) set) \<subseteq> span T \<Longrightarrow> dim S \<le> dim T"`
`  3837   by (metis dim_span dim_subset)`
`  3756   by (metis dim_span dim_subset)`
`  3838 `
`  3757 `
`  3839 lemma span_eq_dim: "span (S:: (real ^'n) set) = span T ==> dim S = dim T"`
`  3758 lemma span_eq_dim: "span (S:: (real ^'n::finite) set) = span T ==> dim S = dim T"`
`  3840   by (metis dim_span)`
`  3759   by (metis dim_span)`
`  3841 `
`  3760 `
`  3842 lemma spans_image:`
`  3761 lemma spans_image:`
`  3843   assumes lf: "linear (f::'a::semiring_1^'n \<Rightarrow> _)" and VB: "V \<subseteq> span B"`
`  3762   assumes lf: "linear (f::'a::semiring_1^'n \<Rightarrow> _)" and VB: "V \<subseteq> span B"`
`  3844   shows "f ` V \<subseteq> span (f ` B)"`
`  3763   shows "f ` V \<subseteq> span (f ` B)"`
`  3845   unfolding span_linear_image[OF lf]`
`  3764   unfolding span_linear_image[OF lf]`
`  3846   by (metis VB image_mono)`
`  3765   by (metis VB image_mono)`
`  3847 `
`  3766 `
`  3848 lemma dim_image_le: assumes lf: "linear f" shows "dim (f ` S) \<le> dim (S:: (real ^'n) set)"`
`  3767 lemma dim_image_le:`
`       `
`  3768   fixes f :: "real^'n::finite \<Rightarrow> real^'m::finite"`
`       `
`  3769   assumes lf: "linear f" shows "dim (f ` S) \<le> dim (S:: (real ^'n::finite) set)"`
`  3849 proof-`
`  3770 proof-`
`  3850   from basis_exists[of S] obtain B where`
`  3771   from basis_exists[of S] obtain B where`
`  3851     B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "B hassize dim S" by blast`
`  3772     B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "B hassize dim S" by blast`
`  3852   from B have fB: "finite B" "card B = dim S" unfolding hassize_def by blast+`
`  3773   from B have fB: "finite B" "card B = dim S" unfolding hassize_def by blast+`
`  3853   have "dim (f ` S) \<le> card (f ` B)"`
`  3774   have "dim (f ` S) \<le> card (f ` B)"`
`  3887 (* Picking an orthogonal replacement for a spanning set.                     *)`
`  3808 (* Picking an orthogonal replacement for a spanning set.                     *)`
`  3888 (* ------------------------------------------------------------------------- *)`
`  3809 (* ------------------------------------------------------------------------- *)`
`  3889     (* FIXME : Move to some general theory ?*)`
`  3810     (* FIXME : Move to some general theory ?*)`
`  3890 definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"`
`  3811 definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"`
`  3891 `
`  3812 `
`  3892 lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n) \<bullet> (x - ((b \<bullet> x) / (b\<bullet>b)) *s b) = 0"`
`  3813 lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n::finite) \<bullet> (x - ((b \<bullet> x) / (b\<bullet>b)) *s b) = 0"`
`  3893   apply (cases "b = 0", simp)`
`  3814   apply (cases "b = 0", simp)`
`  3894   apply (simp add: dot_rsub dot_rmult)`
`  3815   apply (simp add: dot_rsub dot_rmult)`
`  3895   unfolding times_divide_eq_right[symmetric]`
`  3816   unfolding times_divide_eq_right[symmetric]`
`  3896   by (simp add: field_simps dot_eq_0)`
`  3817   by (simp add: field_simps dot_eq_0)`
`  3897 `
`  3818 `
`  3898 lemma basis_orthogonal:`
`  3819 lemma basis_orthogonal:`
`  3899   fixes B :: "(real ^'n) set"`
`  3820   fixes B :: "(real ^'n::finite) set"`
`  3900   assumes fB: "finite B"`
`  3821   assumes fB: "finite B"`
`  3901   shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"`
`  3822   shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"`
`  3902   (is " \<exists>C. ?P B C")`
`  3823   (is " \<exists>C. ?P B C")`
`  3903 proof(induct rule: finite_induct[OF fB])`
`  3824 proof(induct rule: finite_induct[OF fB])`
`  3904   case 1 thus ?case apply (rule exI[where x="{}"]) by (auto simp add: pairwise_def)`
`  3825   case 1 thus ?case apply (rule exI[where x="{}"]) by (auto simp add: pairwise_def)`
`  3970   from fC cC SC CPO have "?P (insert a B) ?C" by blast`
`  3891   from fC cC SC CPO have "?P (insert a B) ?C" by blast`
`  3971   then show ?case by blast`
`  3892   then show ?case by blast`
`  3972 qed`
`  3893 qed`
`  3973 `
`  3894 `
`  3974 lemma orthogonal_basis_exists:`
`  3895 lemma orthogonal_basis_exists:`
`  3975   fixes V :: "(real ^'n) set"`
`  3896   fixes V :: "(real ^'n::finite) set"`
`  3976   shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and> (B hassize dim V) \<and> pairwise orthogonal B"`
`  3897   shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and> (B hassize dim V) \<and> pairwise orthogonal B"`
`  3977 proof-`
`  3898 proof-`
`  3978   from basis_exists[of V] obtain B where B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "B hassize dim V" by blast`
`  3899   from basis_exists[of V] obtain B where B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "B hassize dim V" by blast`
`  3979   from B have fB: "finite B" "card B = dim V" by (simp_all add: hassize_def)`
`  3900   from B have fB: "finite B" "card B = dim V" by (simp_all add: hassize_def)`
`  3980   from basis_orthogonal[OF fB(1)] obtain C where`
`  3901   from basis_orthogonal[OF fB(1)] obtain C where`
`  3998 (* Low-dimensional subset is in a hyperplane (weak orthogonal complement).   *)`
`  3919 (* Low-dimensional subset is in a hyperplane (weak orthogonal complement).   *)`
`  3999 (* ------------------------------------------------------------------------- *)`
`  3920 (* ------------------------------------------------------------------------- *)`
`  4000 `
`  3921 `
`  4001 lemma span_not_univ_orthogonal:`
`  3922 lemma span_not_univ_orthogonal:`
`  4002   assumes sU: "span S \<noteq> UNIV"`
`  3923   assumes sU: "span S \<noteq> UNIV"`
`  4003   shows "\<exists>(a:: real ^'n). a \<noteq>0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"`
`  3924   shows "\<exists>(a:: real ^'n::finite). a \<noteq>0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"`
`  4004 proof-`
`  3925 proof-`
`  4005   from sU obtain a where a: "a \<notin> span S" by blast`
`  3926   from sU obtain a where a: "a \<notin> span S" by blast`
`  4006   from orthogonal_basis_exists obtain B where`
`  3927   from orthogonal_basis_exists obtain B where`
`  4007     B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B" "B hassize dim S" "pairwise orthogonal B"`
`  3928     B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B" "B hassize dim S" "pairwise orthogonal B"`
`  4008     by blast`
`  3929     by blast`
`  4037   qed`
`  3958   qed`
`  4038   with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"])`
`  3959   with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"])`
`  4039 qed`
`  3960 qed`
`  4040 `
`  3961 `
`  4041 lemma span_not_univ_subset_hyperplane:`
`  3962 lemma span_not_univ_subset_hyperplane:`
`  4042   assumes SU: "span S \<noteq> (UNIV ::(real^'n) set)"`
`  3963   assumes SU: "span S \<noteq> (UNIV ::(real^'n::finite) set)"`
`  4043   shows "\<exists> a. a \<noteq>0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"`
`  3964   shows "\<exists> a. a \<noteq>0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"`
`  4044   using span_not_univ_orthogonal[OF SU] by auto`
`  3965   using span_not_univ_orthogonal[OF SU] by auto`
`  4045 `
`  3966 `
`  4046 lemma lowdim_subset_hyperplane:`
`  3967 lemma lowdim_subset_hyperplane:`
`  4047   assumes d: "dim S < dimindex (UNIV :: 'n set)"`
`  3968   assumes d: "dim S < CARD('n::finite)"`
`  4048   shows "\<exists>(a::real ^'n). a  \<noteq> 0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"`
`  3969   shows "\<exists>(a::real ^'n::finite). a  \<noteq> 0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"`
`  4049 proof-`
`  3970 proof-`
`  4050   {assume "span S = UNIV"`
`  3971   {assume "span S = UNIV"`
`  4051     hence "dim (span S) = dim (UNIV :: (real ^'n) set)" by simp`
`  3972     hence "dim (span S) = dim (UNIV :: (real ^'n) set)" by simp`
`  4052     hence "dim S = dimindex (UNIV :: 'n set)" by (simp add: dim_span dim_univ)`
`  3973     hence "dim S = CARD('n)" by (simp add: dim_span dim_univ)`
`  4053     with d have False by arith}`
`  3974     with d have False by arith}`
`  4054   hence th: "span S \<noteq> UNIV" by blast`
`  3975   hence th: "span S \<noteq> UNIV" by blast`
`  4055   from span_not_univ_subset_hyperplane[OF th] show ?thesis .`
`  3976   from span_not_univ_subset_hyperplane[OF th] show ?thesis .`
`  4056 qed`
`  3977 qed`
`  4057 `
`  3978 `
`  4194     ultimately have "?g x = f x" using x by blast }`
`  4115     ultimately have "?g x = f x" using x by blast }`
`  4195   ultimately show ?case apply - apply (rule exI[where x="?g"]) by blast`
`  4116   ultimately show ?case apply - apply (rule exI[where x="?g"]) by blast`
`  4196 qed`
`  4117 qed`
`  4197 `
`  4118 `
`  4198 lemma linear_independent_extend:`
`  4119 lemma linear_independent_extend:`
`  4199   assumes iB: "independent (B:: (real ^'n) set)"`
`  4120   assumes iB: "independent (B:: (real ^'n::finite) set)"`
`  4200   shows "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"`
`  4121   shows "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"`
`  4201 proof-`
`  4122 proof-`
`  4202   from maximal_independent_subset_extend[of B UNIV] iB`
`  4123   from maximal_independent_subset_extend[of B UNIV] iB`
`  4203   obtain C where C: "B \<subseteq> C" "independent C" "\<And>x. x \<in> span C" by auto`
`  4124   obtain C where C: "B \<subseteq> C" "independent C" "\<And>x. x \<in> span C" by auto`
`  4204 `
`  4125 `
`  4247   hence "B - A = {}" unfolding card_eq_0_iff using fA fB by simp`
`  4168   hence "B - A = {}" unfolding card_eq_0_iff using fA fB by simp`
`  4248   with AB show "A = B" by blast`
`  4169   with AB show "A = B" by blast`
`  4249 qed`
`  4170 qed`
`  4250 `
`  4171 `
`  4251 lemma subspace_isomorphism:`
`  4172 lemma subspace_isomorphism:`
`  4252   assumes s: "subspace (S:: (real ^'n) set)" and t: "subspace T"`
`  4173   assumes s: "subspace (S:: (real ^'n::finite) set)"`
`       `
`  4174   and t: "subspace (T :: (real ^ 'm::finite) set)"`
`  4253   and d: "dim S = dim T"`
`  4175   and d: "dim S = dim T"`
`  4254   shows "\<exists>f. linear f \<and> f ` S = T \<and> inj_on f S"`
`  4176   shows "\<exists>f. linear f \<and> f ` S = T \<and> inj_on f S"`
`  4255 proof-`
`  4177 proof-`
`  4256   from basis_exists[of S] obtain B where`
`  4178   from basis_exists[of S] obtain B where`
`  4257     B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "B hassize dim S" by blast`
`  4179     B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "B hassize dim S" by blast`
`  4322   from linear_eq_0[OF linear_compose_sub[OF lf lg] S fg']`
`  4244   from linear_eq_0[OF linear_compose_sub[OF lf lg] S fg']`
`  4323   show ?thesis by simp`
`  4245   show ?thesis by simp`
`  4324 qed`
`  4246 qed`
`  4325 `
`  4247 `
`  4326 lemma linear_eq_stdbasis:`
`  4248 lemma linear_eq_stdbasis:`
`  4327   assumes lf: "linear (f::'a::ring_1^'m \<Rightarrow> 'a^'n)" and lg: "linear g"`
`  4249   assumes lf: "linear (f::'a::ring_1^'m::finite \<Rightarrow> 'a^'n::finite)" and lg: "linear g"`
`  4328   and fg: "\<forall>i \<in> {1 .. dimindex(UNIV :: 'm set)}. f (basis i) = g(basis i)"`
`  4250   and fg: "\<forall>i. f (basis i) = g(basis i)"`
`  4329   shows "f = g"`
`  4251   shows "f = g"`
`  4330 proof-`
`  4252 proof-`
`  4331   let ?U = "UNIV :: 'm set"`
`  4253   let ?U = "UNIV :: 'm set"`
`  4332   let ?I = "{basis i:: 'a^'m|i. i \<in> {1 .. dimindex ?U}}"`
`  4254   let ?I = "{basis i:: 'a^'m|i. i \<in> ?U}"`
`  4333   {fix x assume x: "x \<in> (UNIV :: ('a^'m) set)"`
`  4255   {fix x assume x: "x \<in> (UNIV :: ('a^'m) set)"`
`  4334     from equalityD2[OF span_stdbasis]`
`  4256     from equalityD2[OF span_stdbasis]`
`  4335     have IU: " (UNIV :: ('a^'m) set) \<subseteq> span ?I" by blast`
`  4257     have IU: " (UNIV :: ('a^'m) set) \<subseteq> span ?I" by blast`
`  4336     from linear_eq[OF lf lg IU] fg x`
`  4258     from linear_eq[OF lf lg IU] fg x`
`  4337     have "f x = g x" unfolding Collect_def  Ball_def mem_def by metis}`
`  4259     have "f x = g x" unfolding Collect_def  Ball_def mem_def by metis}`
`  4367     by(auto simp add: span_0 mem_def bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro:  bilinear_ladd[OF bf])`
`  4289     by(auto simp add: span_0 mem_def bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro:  bilinear_ladd[OF bf])`
`  4368   then show ?thesis using SB TC by (auto intro: ext)`
`  4290   then show ?thesis using SB TC by (auto intro: ext)`
`  4369 qed`
`  4291 qed`
`  4370 `
`  4292 `
`  4371 lemma bilinear_eq_stdbasis:`
`  4293 lemma bilinear_eq_stdbasis:`
`  4372   assumes bf: "bilinear (f:: 'a::ring_1^'m \<Rightarrow> 'a^'n \<Rightarrow> 'a^'p)"`
`  4294   assumes bf: "bilinear (f:: 'a::ring_1^'m::finite \<Rightarrow> 'a^'n::finite \<Rightarrow> 'a^'p)"`
`  4373   and bg: "bilinear g"`
`  4295   and bg: "bilinear g"`
`  4374   and fg: "\<forall>i\<in> {1 .. dimindex (UNIV :: 'm set)}. \<forall>j\<in>  {1 .. dimindex (UNIV :: 'n set)}. f (basis i) (basis j) = g (basis i) (basis j)"`
`  4296   and fg: "\<forall>i j. f (basis i) (basis j) = g (basis i) (basis j)"`
`  4375   shows "f = g"`
`  4297   shows "f = g"`
`  4376 proof-`
`  4298 proof-`
`  4377   from fg have th: "\<forall>x \<in> {basis i| i. i\<in> {1 .. dimindex (UNIV :: 'm set)}}. \<forall>y\<in>  {basis j |j. j \<in> {1 .. dimindex (UNIV :: 'n set)}}. f x y = g x y" by blast`
`  4299   from fg have th: "\<forall>x \<in> {basis i| i. i\<in> (UNIV :: 'm set)}. \<forall>y\<in>  {basis j |j. j \<in> (UNIV :: 'n set)}. f x y = g x y" by blast`
`  4378   from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext)`
`  4300   from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext)`
`  4379 qed`
`  4301 qed`
`  4380 `
`  4302 `
`  4381 (* Detailed theorems about left and right invertibility in general case.     *)`
`  4303 (* Detailed theorems about left and right invertibility in general case.     *)`
`  4382 `
`  4304 `
`  4387 lemma right_invertible_transp:`
`  4309 lemma right_invertible_transp:`
`  4388   "(\<exists>(B::'a^'n^'m). transp (A::'a^'n^'m) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B::'a^'m^'n). B ** A = mat 1)"`
`  4310   "(\<exists>(B::'a^'n^'m). transp (A::'a^'n^'m) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B::'a^'m^'n). B ** A = mat 1)"`
`  4389   by (metis matrix_transp_mul transp_mat transp_transp)`
`  4311   by (metis matrix_transp_mul transp_mat transp_transp)`
`  4390 `
`  4312 `
`  4391 lemma linear_injective_left_inverse:`
`  4313 lemma linear_injective_left_inverse:`
`  4392   assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" and fi: "inj f"`
`  4314   assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)" and fi: "inj f"`
`  4393   shows "\<exists>g. linear g \<and> g o f = id"`
`  4315   shows "\<exists>g. linear g \<and> g o f = id"`
`  4394 proof-`
`  4316 proof-`
`  4395   from linear_independent_extend[OF independent_injective_image, OF independent_stdbasis, OF lf fi]`
`  4317   from linear_independent_extend[OF independent_injective_image, OF independent_stdbasis, OF lf fi]`
`  4396   obtain h:: "real ^'m \<Rightarrow> real ^'n" where h: "linear h" " \<forall>x \<in> f ` {basis i|i. i \<in> {1 .. dimindex (UNIV::'n set)}}. h x = inv f x" by blast`
`  4318   obtain h:: "real ^'m \<Rightarrow> real ^'n" where h: "linear h" " \<forall>x \<in> f ` {basis i|i. i \<in> (UNIV::'n set)}. h x = inv f x" by blast`
`  4397   from h(2)`
`  4319   from h(2)`
`  4398   have th: "\<forall>i\<in>{1..dimindex (UNIV::'n set)}. (h \<circ> f) (basis i) = id (basis i)"`
`  4320   have th: "\<forall>i. (h \<circ> f) (basis i) = id (basis i)"`
`  4399     using inv_o_cancel[OF fi, unfolded stupid_ext[symmetric] id_def o_def]`
`  4321     using inv_o_cancel[OF fi, unfolded stupid_ext[symmetric] id_def o_def]`
`  4402     by auto`
`  4322     by auto`
`  4403 `
`  4323 `
`  4404   from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th]`
`  4324   from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th]`
`  4405   have "h o f = id" .`
`  4325   have "h o f = id" .`
`  4406   then show ?thesis using h(1) by blast`
`  4326   then show ?thesis using h(1) by blast`
`  4407 qed`
`  4327 qed`
`  4408 `
`  4328 `
`  4409 lemma linear_surjective_right_inverse:`
`  4329 lemma linear_surjective_right_inverse:`
`  4410   assumes lf: "linear (f:: real ^'m \<Rightarrow> real ^'n)" and sf: "surj f"`
`  4330   assumes lf: "linear (f:: real ^'m::finite \<Rightarrow> real ^'n::finite)" and sf: "surj f"`
`  4411   shows "\<exists>g. linear g \<and> f o g = id"`
`  4331   shows "\<exists>g. linear g \<and> f o g = id"`
`  4412 proof-`
`  4332 proof-`
`  4413   from linear_independent_extend[OF independent_stdbasis]`
`  4333   from linear_independent_extend[OF independent_stdbasis]`
`  4414   obtain h:: "real ^'n \<Rightarrow> real ^'m" where`
`  4334   obtain h:: "real ^'n \<Rightarrow> real ^'m" where`
`  4415     h: "linear h" "\<forall> x\<in> {basis i| i. i\<in> {1 .. dimindex (UNIV :: 'n set)}}. h x = inv f x" by blast`
`  4335     h: "linear h" "\<forall> x\<in> {basis i| i. i\<in> (UNIV :: 'n set)}. h x = inv f x" by blast`
`  4416   from h(2)`
`  4336   from h(2)`
`  4417   have th: "\<forall>i\<in>{1..dimindex (UNIV::'n set)}. (f o h) (basis i) = id (basis i)"`
`  4337   have th: "\<forall>i. (f o h) (basis i) = id (basis i)"`
`  4418     using sf`
`  4338     using sf`
`  4419     apply (auto simp add: surj_iff o_def stupid_ext[symmetric])`
`  4339     apply (auto simp add: surj_iff o_def stupid_ext[symmetric])`
`  4420     apply (erule_tac x="basis i" in allE)`
`  4340     apply (erule_tac x="basis i" in allE)`
`  4421     by auto`
`  4341     by auto`
`  4422 `
`  4342 `
`  4424   have "f o h = id" .`
`  4344   have "f o h = id" .`
`  4425   then show ?thesis using h(1) by blast`
`  4345   then show ?thesis using h(1) by blast`
`  4426 qed`
`  4346 qed`
`  4427 `
`  4347 `
`  4428 lemma matrix_left_invertible_injective:`
`  4348 lemma matrix_left_invertible_injective:`
`  4429 "(\<exists>B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)"`
`  4349 "(\<exists>B. (B::real^'m^'n) ** (A::real^'n::finite^'m::finite) = mat 1) \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)"`
`  4430 proof-`
`  4350 proof-`
`  4431   {fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"`
`  4351   {fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"`
`  4432     from xy have "B*v (A *v x) = B *v (A*v y)" by simp`
`  4352     from xy have "B*v (A *v x) = B *v (A*v y)" by simp`
`  4433     hence "x = y"`
`  4353     hence "x = y"`
`  4434       unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid .}`
`  4354       unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid .}`
`  4443     then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast}`
`  4363     then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast}`
`  4444   ultimately show ?thesis by blast`
`  4364   ultimately show ?thesis by blast`
`  4445 qed`
`  4365 qed`
`  4446 `
`  4366 `
`  4447 lemma matrix_left_invertible_ker:`
`  4367 lemma matrix_left_invertible_ker:`
`  4448   "(\<exists>B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"`
`  4368   "(\<exists>B. (B::real ^'m::finite^'n::finite) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"`
`  4449   unfolding matrix_left_invertible_injective`
`  4369   unfolding matrix_left_invertible_injective`
`  4450   using linear_injective_0[OF matrix_vector_mul_linear, of A]`
`  4370   using linear_injective_0[OF matrix_vector_mul_linear, of A]`
`  4451   by (simp add: inj_on_def)`
`  4371   by (simp add: inj_on_def)`
`  4452 `
`  4372 `
`  4453 lemma matrix_right_invertible_surjective:`
`  4373 lemma matrix_right_invertible_surjective:`
`  4454 "(\<exists>B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"`
`  4374 "(\<exists>B. (A::real^'n::finite^'m::finite) ** (B::real^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"`
`  4455 proof-`
`  4375 proof-`
`  4456   {fix B :: "real ^'m^'n"  assume AB: "A ** B = mat 1"`
`  4376   {fix B :: "real ^'m^'n"  assume AB: "A ** B = mat 1"`
`  4457     {fix x :: "real ^ 'm"`
`  4377     {fix x :: "real ^ 'm"`
`  4458       have "A *v (B *v x) = x"`
`  4378       have "A *v (B *v x) = x"`
`  4459 	by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB)}`
`  4379 	by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB)}`
`  4473   }`
`  4393   }`
`  4474   ultimately show ?thesis unfolding surj_def by blast`
`  4394   ultimately show ?thesis unfolding surj_def by blast`
`  4475 qed`
`  4395 qed`
`  4476 `
`  4396 `
`  4477 lemma matrix_left_invertible_independent_columns:`
`  4397 lemma matrix_left_invertible_independent_columns:`
`  4478   fixes A :: "real^'n^'m"`
`  4398   fixes A :: "real^'n::finite^'m::finite"`
`  4479   shows "(\<exists>(B::real ^'m^'n). B ** A = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s column i A) {1 .. dimindex(UNIV :: 'n set)} = 0 \<longrightarrow> (\<forall>i\<in> {1 .. dimindex (UNIV :: 'n set)}. c i = 0))"`
`  4399   shows "(\<exists>(B::real ^'m^'n). B ** A = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"`
`  4480    (is "?lhs \<longleftrightarrow> ?rhs")`
`  4400    (is "?lhs \<longleftrightarrow> ?rhs")`
`  4481 proof-`
`  4401 proof-`
`  4482   let ?U = "{1 .. dimindex(UNIV :: 'n set)}"`
`  4402   let ?U = "UNIV :: 'n set"`
`  4483   {assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"`
`  4403   {assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"`
`  4484     {fix c i assume c: "setsum (\<lambda>i. c i *s column i A) ?U = 0"`
`  4404     {fix c i assume c: "setsum (\<lambda>i. c i *s column i A) ?U = 0"`
`  4485       and i: "i \<in> ?U"`
`  4405       and i: "i \<in> ?U"`
`  4486       let ?x = "\<chi> i. c i"`
`  4406       let ?x = "\<chi> i. c i"`
`  4487       have th0:"A *v ?x = 0"`
`  4407       have th0:"A *v ?x = 0"`
`  4488 	using c`
`  4408 	using c`
`  4489 	unfolding matrix_mult_vsum Cart_eq`
`  4409 	unfolding matrix_mult_vsum Cart_eq`
`  4490 	by (auto simp add: vector_component zero_index setsum_component Cart_lambda_beta)`
`  4410 	by auto`
`  4491       from k[rule_format, OF th0] i`
`  4411       from k[rule_format, OF th0] i`
`  4492       have "c i = 0" by (vector Cart_eq)}`
`  4412       have "c i = 0" by (vector Cart_eq)}`
`  4493     hence ?rhs by blast}`
`  4413     hence ?rhs by blast}`
`  4494   moreover`
`  4414   moreover`
`  4495   {assume H: ?rhs`
`  4415   {assume H: ?rhs`
`  4499       have "x = 0" by vector}}`
`  4419       have "x = 0" by vector}}`
`  4500   ultimately show ?thesis unfolding matrix_left_invertible_ker by blast`
`  4420   ultimately show ?thesis unfolding matrix_left_invertible_ker by blast`
`  4501 qed`
`  4421 qed`
`  4502 `
`  4422 `
`  4503 lemma matrix_right_invertible_independent_rows:`
`  4423 lemma matrix_right_invertible_independent_rows:`
`  4504   fixes A :: "real^'n^'m"`
`  4424   fixes A :: "real^'n::finite^'m::finite"`
`  4505   shows "(\<exists>(B::real^'m^'n). A ** B = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s row i A) {1 .. dimindex(UNIV :: 'm set)} = 0 \<longrightarrow> (\<forall>i\<in> {1 .. dimindex (UNIV :: 'm set)}. c i = 0))"`
`  4425   shows "(\<exists>(B::real^'m^'n). A ** B = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"`
`  4506   unfolding left_invertible_transp[symmetric]`
`  4426   unfolding left_invertible_transp[symmetric]`
`  4507     matrix_left_invertible_independent_columns`
`  4427     matrix_left_invertible_independent_columns`
`  4508   by (simp add: column_transp)`
`  4428   by (simp add: column_transp)`
`  4509 `
`  4429 `
`  4510 lemma matrix_right_invertible_span_columns:`
`  4430 lemma matrix_right_invertible_span_columns:`
`  4511   "(\<exists>(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> span (columns A) = UNIV" (is "?lhs = ?rhs")`
`  4431   "(\<exists>(B::real ^'n::finite^'m::finite). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> span (columns A) = UNIV" (is "?lhs = ?rhs")`
`  4512 proof-`
`  4432 proof-`
`  4513   let ?U = "{1 .. dimindex (UNIV :: 'm set)}"`
`  4433   let ?U = "UNIV :: 'm set"`
`  4514   have fU: "finite ?U" by simp`
`  4434   have fU: "finite ?U" by simp`
`  4515   have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). setsum (\<lambda>i. (x\$i) *s column i A) ?U = y)"`
`  4435   have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). setsum (\<lambda>i. (x\$i) *s column i A) ?U = y)"`
`  4516     unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def`
`  4436     unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def`
`  4517     apply (subst eq_commute) ..`
`  4437     apply (subst eq_commute) ..`
`  4518   have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> span (columns A))" by blast`
`  4438   have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> span (columns A))" by blast`
`  4543 	  unfolding columns_def by blast`
`  4463 	  unfolding columns_def by blast`
`  4544 	from y2 obtain x:: "real ^'m" where`
`  4464 	from y2 obtain x:: "real ^'m" where`
`  4545 	  x: "setsum (\<lambda>i. (x\$i) *s column i A) ?U = y2" by blast`
`  4465 	  x: "setsum (\<lambda>i. (x\$i) *s column i A) ?U = y2" by blast`
`  4546 	let ?x = "(\<chi> j. if j = i then c + (x\$i) else (x\$j))::real^'m"`
`  4466 	let ?x = "(\<chi> j. if j = i then c + (x\$i) else (x\$j))::real^'m"`
`  4547 	show "?P (c*s y1 + y2)"`
`  4467 	show "?P (c*s y1 + y2)"`
`  4548 	  proof(rule exI[where x= "?x"], vector, auto simp add: i x[symmetric]Cart_lambda_beta setsum_component cond_value_iff right_distrib cond_application_beta vector_component cong del: if_weak_cong, simp only: One_nat_def[symmetric])`
`  4468 	  proof(rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] cond_value_iff right_distrib cond_application_beta cong del: if_weak_cong)`
`  4549 	    fix j`
`  4469 	    fix j`
`  4550 	    have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x\$i)) * ((column xa A)\$j)`
`  4470 	    have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x\$i)) * ((column xa A)\$j)`
`  4551            else (x\$xa) * ((column xa A\$j))) = (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))" using i(1)`
`  4471            else (x\$xa) * ((column xa A\$j))) = (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))" using i(1)`
`  4552 	      by (simp add: ring_simps)`
`  4472 	      by (simp add: ring_simps)`
`  4553 	    have "setsum (\<lambda>xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j)`
`  4473 	    have "setsum (\<lambda>xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j)`
`  4568     then have ?lhs unfolding lhseq ..}`
`  4488     then have ?lhs unfolding lhseq ..}`
`  4569   ultimately show ?thesis by blast`
`  4489   ultimately show ?thesis by blast`
`  4570 qed`
`  4490 qed`
`  4571 `
`  4491 `
`  4572 lemma matrix_left_invertible_span_rows:`
`  4492 lemma matrix_left_invertible_span_rows:`
`  4573   "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"`
`  4493   "(\<exists>(B::real^'m::finite^'n::finite). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"`
`  4574   unfolding right_invertible_transp[symmetric]`
`  4494   unfolding right_invertible_transp[symmetric]`
`  4575   unfolding columns_transp[symmetric]`
`  4495   unfolding columns_transp[symmetric]`
`  4576   unfolding matrix_right_invertible_span_columns`
`  4496   unfolding matrix_right_invertible_span_columns`
`  4577  ..`
`  4497  ..`
`  4578 `
`  4498 `
`  4579 (* An injective map real^'n->real^'n is also surjective.                       *)`
`  4499 (* An injective map real^'n->real^'n is also surjective.                       *)`
`  4580 `
`  4500 `
`  4581 lemma linear_injective_imp_surjective:`
`  4501 lemma linear_injective_imp_surjective:`
`  4582   assumes lf: "linear (f:: real ^'n \<Rightarrow> real ^'n)" and fi: "inj f"`
`  4502   assumes lf: "linear (f:: real ^'n::finite \<Rightarrow> real ^'n)" and fi: "inj f"`
`  4583   shows "surj f"`
`  4503   shows "surj f"`
`  4584 proof-`
`  4504 proof-`
`  4585   let ?U = "UNIV :: (real ^'n) set"`
`  4505   let ?U = "UNIV :: (real ^'n) set"`
`  4586   from basis_exists[of ?U] obtain B`
`  4506   from basis_exists[of ?U] obtain B`
`  4587     where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "B hassize dim ?U"`
`  4507     where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "B hassize dim ?U"`
`  4639     then have ?lhs by blast}`
`  4559     then have ?lhs by blast}`
`  4640   ultimately show ?thesis by blast`
`  4560   ultimately show ?thesis by blast`
`  4641 qed`
`  4561 qed`
`  4642 `
`  4562 `
`  4643 lemma linear_surjective_imp_injective:`
`  4563 lemma linear_surjective_imp_injective:`
`  4644   assumes lf: "linear (f::real ^'n => real ^'n)" and sf: "surj f"`
`  4564   assumes lf: "linear (f::real ^'n::finite => real ^'n)" and sf: "surj f"`
`  4645   shows "inj f"`
`  4565   shows "inj f"`
`  4646 proof-`
`  4566 proof-`
`  4647   let ?U = "UNIV :: (real ^'n) set"`
`  4567   let ?U = "UNIV :: (real ^'n) set"`
`  4648   from basis_exists[of ?U] obtain B`
`  4568   from basis_exists[of ?U] obtain B`
`  4649     where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "B hassize dim ?U"`
`  4569     where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "B hassize dim ?U"`
`  4699 lemma isomorphism_expand:`
`  4619 lemma isomorphism_expand:`
`  4700   "f o g = id \<and> g o f = id \<longleftrightarrow> (\<forall>x. f(g x) = x) \<and> (\<forall>x. g(f x) = x)"`
`  4620   "f o g = id \<and> g o f = id \<longleftrightarrow> (\<forall>x. f(g x) = x) \<and> (\<forall>x. g(f x) = x)"`
`  4701   by (simp add: expand_fun_eq o_def id_def)`
`  4621   by (simp add: expand_fun_eq o_def id_def)`
`  4702 `
`  4622 `
`  4703 lemma linear_injective_isomorphism:`
`  4623 lemma linear_injective_isomorphism:`
`  4704   assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'n)" and fi: "inj f"`
`  4624   assumes lf: "linear (f :: real^'n::finite \<Rightarrow> real ^'n)" and fi: "inj f"`
`  4705   shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"`
`  4625   shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"`
`  4706 unfolding isomorphism_expand[symmetric]`
`  4626 unfolding isomorphism_expand[symmetric]`
`  4707 using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]] linear_injective_left_inverse[OF lf fi]`
`  4627 using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]] linear_injective_left_inverse[OF lf fi]`
`  4708 by (metis left_right_inverse_eq)`
`  4628 by (metis left_right_inverse_eq)`
`  4709 `
`  4629 `
`  4710 lemma linear_surjective_isomorphism:`
`  4630 lemma linear_surjective_isomorphism:`
`  4711   assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'n)" and sf: "surj f"`
`  4631   assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'n)" and sf: "surj f"`
`  4712   shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"`
`  4632   shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"`
`  4713 unfolding isomorphism_expand[symmetric]`
`  4633 unfolding isomorphism_expand[symmetric]`
`  4714 using linear_surjective_right_inverse[OF lf sf] linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]]`
`  4634 using linear_surjective_right_inverse[OF lf sf] linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]]`
`  4715 by (metis left_right_inverse_eq)`
`  4635 by (metis left_right_inverse_eq)`
`  4716 `
`  4636 `
`  4717 (* Left and right inverses are the same for R^N->R^N.                        *)`
`  4637 (* Left and right inverses are the same for R^N->R^N.                        *)`
`  4718 `
`  4638 `
`  4719 lemma linear_inverse_left:`
`  4639 lemma linear_inverse_left:`
`  4720   assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'n)" and lf': "linear f'"`
`  4640   assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'n)" and lf': "linear f'"`
`  4721   shows "f o f' = id \<longleftrightarrow> f' o f = id"`
`  4641   shows "f o f' = id \<longleftrightarrow> f' o f = id"`
`  4722 proof-`
`  4642 proof-`
`  4723   {fix f f':: "real ^'n \<Rightarrow> real ^'n"`
`  4643   {fix f f':: "real ^'n \<Rightarrow> real ^'n"`
`  4724     assume lf: "linear f" "linear f'" and f: "f o f' = id"`
`  4644     assume lf: "linear f" "linear f'" and f: "f o f' = id"`
`  4725     from f have sf: "surj f"`
`  4645     from f have sf: "surj f"`
`  4733 qed`
`  4653 qed`
`  4734 `
`  4654 `
`  4735 (* Moreover, a one-sided inverse is automatically linear.                    *)`
`  4655 (* Moreover, a one-sided inverse is automatically linear.                    *)`
`  4736 `
`  4656 `
`  4737 lemma left_inverse_linear:`
`  4657 lemma left_inverse_linear:`
`  4738   assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'n)" and gf: "g o f = id"`
`  4658   assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'n)" and gf: "g o f = id"`
`  4739   shows "linear g"`
`  4659   shows "linear g"`
`  4740 proof-`
`  4660 proof-`
`  4741   from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def stupid_ext[symmetric])`
`  4661   from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def stupid_ext[symmetric])`
`  4742     by metis`
`  4662     by metis`
`  4743   from linear_injective_isomorphism[OF lf fi]`
`  4663   from linear_injective_isomorphism[OF lf fi]`
`  4748     by metis`
`  4668     by metis`
`  4749   with h(1) show ?thesis by blast`
`  4669   with h(1) show ?thesis by blast`
`  4750 qed`
`  4670 qed`
`  4751 `
`  4671 `
`  4752 lemma right_inverse_linear:`
`  4672 lemma right_inverse_linear:`
`  4753   assumes lf: "linear (f:: real ^'n \<Rightarrow> real ^'n)" and gf: "f o g = id"`
`  4673   assumes lf: "linear (f:: real ^'n::finite \<Rightarrow> real ^'n)" and gf: "f o g = id"`
`  4754   shows "linear g"`
`  4674   shows "linear g"`
`  4755 proof-`
`  4675 proof-`
`  4756   from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def stupid_ext[symmetric])`
`  4676   from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def stupid_ext[symmetric])`
`  4757     by metis`
`  4677     by metis`
`  4758   from linear_surjective_isomorphism[OF lf fi]`
`  4678   from linear_surjective_isomorphism[OF lf fi]`
`  4765 qed`
`  4685 qed`
`  4766 `
`  4686 `
`  4767 (* The same result in terms of square matrices.                              *)`
`  4687 (* The same result in terms of square matrices.                              *)`
`  4768 `
`  4688 `
`  4769 lemma matrix_left_right_inverse:`
`  4689 lemma matrix_left_right_inverse:`
`  4770   fixes A A' :: "real ^'n^'n"`
`  4690   fixes A A' :: "real ^'n::finite^'n"`
`  4771   shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"`
`  4691   shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"`
`  4772 proof-`
`  4692 proof-`
`  4773   {fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1"`
`  4693   {fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1"`
`  4774     have sA: "surj (op *v A)"`
`  4694     have sA: "surj (op *v A)"`
`  4775       unfolding surj_def`
`  4695       unfolding surj_def`
`  4794 `
`  4714 `
`  4795 definition "columnvector v = (\<chi> i j. (v\$i))"`
`  4715 definition "columnvector v = (\<chi> i j. (v\$i))"`
`  4796 `
`  4716 `
`  4797 lemma transp_columnvector:`
`  4717 lemma transp_columnvector:`
`  4798  "transp(columnvector v) = rowvector v"`
`  4718  "transp(columnvector v) = rowvector v"`
`  4799   by (simp add: transp_def rowvector_def columnvector_def Cart_eq Cart_lambda_beta)`
`  4719   by (simp add: transp_def rowvector_def columnvector_def Cart_eq)`
`  4800 `
`  4720 `
`  4801 lemma transp_rowvector: "transp(rowvector v) = columnvector v"`
`  4721 lemma transp_rowvector: "transp(rowvector v) = columnvector v"`
`  4802   by (simp add: transp_def columnvector_def rowvector_def Cart_eq Cart_lambda_beta)`
`  4722   by (simp add: transp_def columnvector_def rowvector_def Cart_eq)`
`  4803 `
`  4723 `
`  4804 lemma dot_rowvector_columnvector:`
`  4724 lemma dot_rowvector_columnvector:`
`  4805   "columnvector (A *v v) = A ** columnvector v"`
`  4725   "columnvector (A *v v) = A ** columnvector v"`
`  4806   by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)`
`  4726   by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)`
`  4807 `
`  4727 `
`  4808 lemma dot_matrix_product: "(x::'a::semiring_1^'n) \<bullet> y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))\$1)\$1"`
`  4728 lemma dot_matrix_product: "(x::'a::semiring_1^'n::finite) \<bullet> y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))\$1)\$1"`
`  4809   apply (vector matrix_matrix_mult_def rowvector_def columnvector_def dot_def)`
`  4729   by (vector matrix_matrix_mult_def rowvector_def columnvector_def dot_def)`
`  4810   by (simp add: Cart_lambda_beta)`
`       `
`  4811 `
`  4730 `
`  4812 lemma dot_matrix_vector_mul:`
`  4731 lemma dot_matrix_vector_mul:`
`  4813   fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"`
`  4732   fixes A B :: "real ^'n::finite ^'n" and x y :: "real ^'n"`
`  4814   shows "(A *v x) \<bullet> (B *v y) =`
`  4733   shows "(A *v x) \<bullet> (B *v y) =`
`  4815       (((rowvector x :: real^'n^1) ** ((transp A ** B) ** (columnvector y :: real ^1^'n)))\$1)\$1"`
`  4734       (((rowvector x :: real^'n^1) ** ((transp A ** B) ** (columnvector y :: real ^1^'n)))\$1)\$1"`
`  4816 unfolding dot_matrix_product transp_columnvector[symmetric]`
`  4735 unfolding dot_matrix_product transp_columnvector[symmetric]`
`  4817   dot_rowvector_columnvector matrix_transp_mul matrix_mul_assoc ..`
`  4736   dot_rowvector_columnvector matrix_transp_mul matrix_mul_assoc ..`
`  4818 `
`  4737 `
`  4819 (* Infinity norm.                                                            *)`
`  4738 (* Infinity norm.                                                            *)`
`  4820 `
`  4739 `
`  4821 definition "infnorm (x::real^'n) = rsup {abs(x\$i) |i. i\<in> {1 .. dimindex(UNIV :: 'n set)}}"`
`  4740 definition "infnorm (x::real^'n::finite) = rsup {abs(x\$i) |i. i\<in> (UNIV :: 'n set)}"`
`  4822 `
`  4741 `
`  4823 lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> {1 .. dimindex (UNIV :: 'n set)}"`
`  4742 lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"`
`  4824   using dimindex_ge_1 by auto`
`  4743   by auto`
`  4825 `
`  4744 `
`  4826 lemma infnorm_set_image:`
`  4745 lemma infnorm_set_image:`
`  4827   "{abs(x\$i) |i. i\<in> {1 .. dimindex(UNIV :: 'n set)}} =`
`  4746   "{abs(x\$i) |i. i\<in> (UNIV :: 'n set)} =`
`  4828   (\<lambda>i. abs(x\$i)) ` {1 .. dimindex(UNIV :: 'n set)}" by blast`
`  4747   (\<lambda>i. abs(x\$i)) ` (UNIV :: 'n set)" by blast`
`  4829 `
`  4748 `
`  4830 lemma infnorm_set_lemma:`
`  4749 lemma infnorm_set_lemma:`
`  4831   shows "finite {abs((x::'a::abs ^'n)\$i) |i. i\<in> {1 .. dimindex(UNIV :: 'n set)}}"`
`  4750   shows "finite {abs((x::'a::abs ^'n::finite)\$i) |i. i\<in> (UNIV :: 'n set)}"`
`  4832   and "{abs(x\$i) |i. i\<in> {1 .. dimindex(UNIV :: 'n set)}} \<noteq> {}"`
`  4751   and "{abs(x\$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"`
`  4833   unfolding infnorm_set_image`
`  4752   unfolding infnorm_set_image`
`  4835   by (auto intro: finite_imageI)`
`  4753   by (auto intro: finite_imageI)`
`  4836 `
`  4754 `
`  4837 lemma infnorm_pos_le: "0 \<le> infnorm x"`
`  4755 lemma infnorm_pos_le: "0 \<le> infnorm (x::real^'n::finite)"`
`  4838   unfolding infnorm_def`
`  4756   unfolding infnorm_def`
`  4839   unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]`
`  4757   unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]`
`  4840   unfolding infnorm_set_image`
`  4758   unfolding infnorm_set_image`
`  4842   by auto`
`  4759   by auto`
`  4843 `
`  4760 `
`  4844 lemma infnorm_triangle: "infnorm ((x::real^'n) + y) \<le> infnorm x + infnorm y"`
`  4761 lemma infnorm_triangle: "infnorm ((x::real^'n::finite) + y) \<le> infnorm x + infnorm y"`
`  4845 proof-`
`  4762 proof-`
`  4846   have th: "\<And>x y (z::real). x - y <= z \<longleftrightarrow> x - z <= y" by arith`
`  4763   have th: "\<And>x y (z::real). x - y <= z \<longleftrightarrow> x - z <= y" by arith`
`  4847   have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast`
`  4764   have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast`
`  4848   have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith`
`  4765   have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith`
`  4849   show ?thesis`
`  4766   show ?thesis`
`  4855   apply (subst th)`
`  4772   apply (subst th)`
`  4856   unfolding th1`
`  4773   unfolding th1`
`  4857   unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]`
`  4774   unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]`
`  4858 `
`  4775 `
`  4859   unfolding infnorm_set_image ball_simps bex_simps`
`  4776   unfolding infnorm_set_image ball_simps bex_simps`
`  4860   apply (simp add: vector_add_component)`
`  4777   apply simp`
`  4861   apply (metis numseg_dimindex_nonempty th2)`
`  4778   apply (metis th2)`
`  4862   done`
`  4779   done`
`  4863 qed`
`  4780 qed`
`  4864 `
`  4781 `
`  4865 lemma infnorm_eq_0: "infnorm x = 0 \<longleftrightarrow> (x::real ^'n) = 0"`
`  4782 lemma infnorm_eq_0: "infnorm x = 0 \<longleftrightarrow> (x::real ^'n::finite) = 0"`
`  4866 proof-`
`  4783 proof-`
`  4867   have "infnorm x <= 0 \<longleftrightarrow> x = 0"`
`  4784   have "infnorm x <= 0 \<longleftrightarrow> x = 0"`
`  4868     unfolding infnorm_def`
`  4785     unfolding infnorm_def`
`  4869     unfolding rsup_finite_le_iff[OF infnorm_set_lemma]`
`  4786     unfolding rsup_finite_le_iff[OF infnorm_set_lemma]`
`  4870     unfolding infnorm_set_image ball_simps`
`  4787     unfolding infnorm_set_image ball_simps`
`  4878 lemma infnorm_neg: "infnorm (- x) = infnorm x"`
`  4795 lemma infnorm_neg: "infnorm (- x) = infnorm x"`
`  4879   unfolding infnorm_def`
`  4796   unfolding infnorm_def`
`  4880   apply (rule cong[of "rsup" "rsup"])`
`  4797   apply (rule cong[of "rsup" "rsup"])`
`  4881   apply blast`
`  4798   apply blast`
`  4882   apply (rule set_ext)`
`  4799   apply (rule set_ext)`
`  4883   apply (auto simp add: vector_component abs_minus_cancel)`
`  4800   apply auto`
`  4884   apply (rule_tac x="i" in exI)`
`       `
`  4885   apply (simp add: vector_component)`
`       `
`  4886   done`
`  4801   done`
`  4887 `
`  4802 `
`  4888 lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"`
`  4803 lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"`
`  4889 proof-`
`  4804 proof-`
`  4890   have "y - x = - (x - y)" by simp`
`  4805   have "y - x = - (x - y)" by simp`
`  4903 qed`
`  4818 qed`
`  4904 `
`  4819 `
`  4905 lemma real_abs_infnorm: " \<bar>infnorm x\<bar> = infnorm x"`
`  4820 lemma real_abs_infnorm: " \<bar>infnorm x\<bar> = infnorm x"`
`  4906   using infnorm_pos_le[of x] by arith`
`  4821   using infnorm_pos_le[of x] by arith`
`  4907 `
`  4822 `
`  4908 lemma component_le_infnorm: assumes i: "i \<in> {1 .. dimindex (UNIV :: 'n set)}"`
`  4823 lemma component_le_infnorm:`
`  4909   shows "\<bar>x\$i\<bar> \<le> infnorm (x::real^'n)"`
`  4824   shows "\<bar>x\$i\<bar> \<le> infnorm (x::real^'n::finite)"`
`  4910 proof-`
`  4825 proof-`
`  4911   let ?U = "{1 .. dimindex (UNIV :: 'n set)}"`
`  4826   let ?U = "UNIV :: 'n set"`
`  4912   let ?S = "{\<bar>x\$i\<bar> |i. i\<in> ?U}"`
`  4827   let ?S = "{\<bar>x\$i\<bar> |i. i\<in> ?U}"`
`  4913   have fS: "finite ?S" unfolding image_Collect[symmetric]`
`  4828   have fS: "finite ?S" unfolding image_Collect[symmetric]`
`  4914     apply (rule finite_imageI) unfolding Collect_def mem_def by simp`
`  4829     apply (rule finite_imageI) unfolding Collect_def mem_def by simp`
`  4915   have S0: "?S \<noteq> {}" using numseg_dimindex_nonempty by blast`
`  4830   have S0: "?S \<noteq> {}" by blast`
`  4916   have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast`
`  4831   have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast`
`  4917   from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0] i`
`  4832   from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0]`
`  4918   show ?thesis unfolding infnorm_def isUb_def setle_def`
`  4833   show ?thesis unfolding infnorm_def isUb_def setle_def`
`  4919     unfolding infnorm_set_image ball_simps by auto`
`  4834     unfolding infnorm_set_image ball_simps by auto`
`  4920 qed`
`  4835 qed`
`  4921 `
`  4836 `
`  4922 lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"`
`  4837 lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"`
`  4923   apply (subst infnorm_def)`
`  4838   apply (subst infnorm_def)`
`  4924   unfolding rsup_finite_le_iff[OF infnorm_set_lemma]`
`  4839   unfolding rsup_finite_le_iff[OF infnorm_set_lemma]`
`  4925   unfolding infnorm_set_image ball_simps`
`  4840   unfolding infnorm_set_image ball_simps`
`  4926   apply (simp add: abs_mult vector_component del: One_nat_def)`
`  4841   apply (simp add: abs_mult)`
`  4927   apply (rule ballI)`
`  4842   apply (rule allI)`
`  4928   apply (drule component_le_infnorm[of _ x])`
`  4843   apply (cut_tac component_le_infnorm[of x])`
`  4929   apply (rule mult_mono)`
`  4844   apply (rule mult_mono)`
`  4930   apply auto`
`  4845   apply auto`
`  4931   done`
`  4846   done`
`  4932 `
`  4847 `
`  4933 lemma infnorm_mul: "infnorm(a *s x) = abs a * infnorm x"`
`  4848 lemma infnorm_mul: "infnorm(a *s x) = abs a * infnorm x"`
`  4956 lemma infnorm_le_norm: "infnorm x \<le> norm x"`
`  4871 lemma infnorm_le_norm: "infnorm x \<le> norm x"`
`  4957   unfolding infnorm_def rsup_finite_le_iff[OF infnorm_set_lemma]`
`  4872   unfolding infnorm_def rsup_finite_le_iff[OF infnorm_set_lemma]`
`  4958   unfolding infnorm_set_image  ball_simps`
`  4873   unfolding infnorm_set_image  ball_simps`
`  4959   by (metis component_le_norm)`
`  4874   by (metis component_le_norm)`
`  4960 lemma card_enum: "card {1 .. n} = n" by auto`
`  4875 lemma card_enum: "card {1 .. n} = n" by auto`
`  4961 lemma norm_le_infnorm: "norm(x) <= sqrt(real (dimindex(UNIV ::'n set))) * infnorm(x::real ^'n)"`
`  4876 lemma norm_le_infnorm: "norm(x) <= sqrt(real CARD('n)) * infnorm(x::real ^'n::finite)"`
`  4962 proof-`
`  4877 proof-`
`  4963   let ?d = "dimindex(UNIV ::'n set)"`
`  4878   let ?d = "CARD('n)"`
`  4964   have d: "?d = card {1 .. ?d}" by auto`
`       `
`  4965   have "real ?d \<ge> 0" by simp`
`  4879   have "real ?d \<ge> 0" by simp`
`  4966   hence d2: "(sqrt (real ?d))^2 = real ?d"`
`  4880   hence d2: "(sqrt (real ?d))^2 = real ?d"`
`  4967     by (auto intro: real_sqrt_pow2)`
`  4881     by (auto intro: real_sqrt_pow2)`
`  4968   have th: "sqrt (real ?d) * infnorm x \<ge> 0"`
`  4882   have th: "sqrt (real ?d) * infnorm x \<ge> 0"`
`  4969     by (simp add: dimindex_ge_1 zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le)`
`  4883     by (simp add: zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le)`
`  4970   have th1: "x\<bullet>x \<le> (sqrt (real ?d) * infnorm x)^2"`
`  4884   have th1: "x\<bullet>x \<le> (sqrt (real ?d) * infnorm x)^2"`
`  4971     unfolding power_mult_distrib d2`
`  4885     unfolding power_mult_distrib d2`
`  4973     apply (subst power2_abs[symmetric])`
`  4886     apply (subst power2_abs[symmetric])`
`  4974     unfolding real_of_nat_def dot_def power2_eq_square[symmetric]`
`  4887     unfolding real_of_nat_def dot_def power2_eq_square[symmetric]`
`  4975     apply (subst power2_abs[symmetric])`
`  4888     apply (subst power2_abs[symmetric])`
`  4976     apply (rule setsum_bounded)`
`  4889     apply (rule setsum_bounded)`
`  4977     apply (rule power_mono)`
`  4890     apply (rule power_mono)`
`  4984   show ?thesis unfolding real_vector_norm_def id_def .`
`  4897   show ?thesis unfolding real_vector_norm_def id_def .`
`  4985 qed`
`  4898 qed`
`  4986 `
`  4899 `
`  4987 (* Equality in Cauchy-Schwarz and triangle inequalities.                     *)`
`  4900 (* Equality in Cauchy-Schwarz and triangle inequalities.                     *)`
`  4988 `
`  4901 `
`  4989 lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")`
`  4902 lemma norm_cauchy_schwarz_eq: "(x::real ^'n::finite) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")`
`  4990 proof-`
`  4903 proof-`
`  4991   {assume h: "x = 0"`
`  4904   {assume h: "x = 0"`
`  4992     hence ?thesis by simp}`
`  4905     hence ?thesis by simp}`
`  4993   moreover`
`  4906   moreover`
`  4994   {assume h: "y = 0"`
`  4907   {assume h: "y = 0"`
`  5010       by metis`
`  4923       by metis`
`  5011     finally have ?thesis by blast}`
`  4924     finally have ?thesis by blast}`
`  5012   ultimately show ?thesis by blast`
`  4925   ultimately show ?thesis by blast`
`  5013 qed`
`  4926 qed`
`  5014 `
`  4927 `
`  5015 lemma norm_cauchy_schwarz_abs_eq: "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow>`
`  4928 lemma norm_cauchy_schwarz_abs_eq:`
`       `
`  4929   fixes x y :: "real ^ 'n::finite"`
`       `
`  4930   shows "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow>`
`  5016                 norm x *s y = norm y *s x \<or> norm(x) *s y = - norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")`
`  4931                 norm x *s y = norm y *s x \<or> norm(x) *s y = - norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")`
`  5017 proof-`
`  4932 proof-`
`  5018   have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a" by arith`
`  4933   have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a" by arith`
`  5019   have "?rhs \<longleftrightarrow> norm x *s y = norm y *s x \<or> norm (- x) *s y = norm y *s (- x)"`
`  4934   have "?rhs \<longleftrightarrow> norm x *s y = norm y *s x \<or> norm (- x) *s y = norm y *s (- x)"`
`  5020     apply simp by vector`
`  4935     apply simp by vector`
`  5027     unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg`
`  4942     unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg`
`  5028     by arith`
`  4943     by arith`
`  5029   finally show ?thesis ..`
`  4944   finally show ?thesis ..`
`  5030 qed`
`  4945 qed`
`  5031 `
`  4946 `
`  5032 lemma norm_triangle_eq: "norm(x + y) = norm x + norm y \<longleftrightarrow> norm x *s y = norm y *s x"`
`  4947 lemma norm_triangle_eq:`
`       `
`  4948   fixes x y :: "real ^ 'n::finite"`
`       `
`  4949   shows "norm(x + y) = norm x + norm y \<longleftrightarrow> norm x *s y = norm y *s x"`
`  5033 proof-`
`  4950 proof-`
`  5034   {assume x: "x =0 \<or> y =0"`
`  4951   {assume x: "x =0 \<or> y =0"`
`  5035     hence ?thesis by (cases "x=0", simp_all)}`
`  4952     hence ?thesis by (cases "x=0", simp_all)}`
`  5036   moreover`
`  4953   moreover`
`  5037   {assume x: "x \<noteq> 0" and y: "y \<noteq> 0"`
`  4954   {assume x: "x \<noteq> 0" and y: "y \<noteq> 0"`
`  5105 	done}`
`  5022 	done}`
`  5106     ultimately have ?thesis by blast}`
`  5023     ultimately have ?thesis by blast}`
`  5107   ultimately show ?thesis by blast`
`  5024   ultimately show ?thesis by blast`
`  5108 qed`
`  5025 qed`
`  5109 `
`  5026 `
`  5110 lemma norm_cauchy_schwarz_equal: "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {(0::real^'n),x,y}"`
`  5027 lemma norm_cauchy_schwarz_equal:`
`       `
`  5028   fixes x y :: "real ^ 'n::finite"`
`       `
`  5029   shows "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {(0::real^'n),x,y}"`
`  5111 unfolding norm_cauchy_schwarz_abs_eq`
`  5030 unfolding norm_cauchy_schwarz_abs_eq`
`  5112 apply (cases "x=0", simp_all add: collinear_2)`
`  5031 apply (cases "x=0", simp_all add: collinear_2)`
`  5113 apply (cases "y=0", simp_all add: collinear_2 insert_commute)`
`  5032 apply (cases "y=0", simp_all add: collinear_2 insert_commute)`
`  5114 unfolding collinear_lemma`
`  5033 unfolding collinear_lemma`
`  5115 apply simp`
`  5034 apply simp`