src/HOL/Library/Euclidean_Space.thy
changeset 30582 638b088bb840
parent 30549 d2d7874648bd
child 30655 88131f2807b6
child 30661 54858c8ad226
equal deleted 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 
   117 lemmas Cart_lambda_beta' = Cart_lambda_beta[rule_format]
       
   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"
   178   assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}"
       
   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:
  1270   assumes k: "k \<in> {1 .. dimindex(UNIV ::'n set)}"
       
  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:
  1800   assumes k: "k \<in> {1.. dimindex (UNIV :: 'm set)}"
       
  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"
  1818   assumes i: "i \<in> {1.. dimindex (UNIV :: 'n set)}"
       
  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"
  1825   assumes i: "i \<in> {1.. dimindex (UNIV :: 'm set)}"
       
  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])
  1885 apply simp
       
  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)
  2589   let ?f = "\<lambda>n. n - ?n"
       
  2590   let ?S = "{?n+1 .. ?nm}"
       
  2591   have finj:"inj_on ?f ?S"
       
  2592     using dimindex_nonzero[of "UNIV :: 'n set"] dimindex_nonzero[of "UNIV :: 'm set"]
       
  2593     apply (simp add: Ball_def atLeastAtMost_iff inj_on_def dimindex_finite_sum del: One_nat_def)
       
  2594     by arith
       
  2595   have fS: "?f ` ?S = ?M"
       
  2596     apply (rule set_ext)
       
  2597     apply (simp add: image_iff Bex_def) using dimindex_nonzero[of "UNIV :: 'n set"] dimindex_nonzero[of "UNIV :: 'm set"] by arith
       
  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)"
  3453   and i: "i \<in> {1 .. dimindex (UNIV :: 'n set)}"
       
  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]
  4400     apply auto
       
  4401     apply (erule_tac x="basis i" in allE)
       
  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
  4834   using dimindex_ge_1[of "UNIV :: 'n set"]
       
  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
  4841   using dimindex_ge_1
       
  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
  4972     apply (subst d)
       
  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