src/HOL/Analysis/Finite_Cartesian_Product.thy
author nipkow
Sat Dec 29 15:43:53 2018 +0100 (6 months ago)
changeset 69529 4ab9657b3257
parent 69517 dc20f278e8f3
child 69597 ff784d5a5bfb
permissions -rw-r--r--
capitalize proper names in lemma names
     1 (*  Title:      HOL/Analysis/Finite_Cartesian_Product.thy
     2     Author:     Amine Chaieb, University of Cambridge
     3 *)
     4 
     5 section%important \<open>Definition of Finite Cartesian Product Type\<close>
     6 
     7 theory Finite_Cartesian_Product
     8 imports
     9   Euclidean_Space
    10   L2_Norm
    11   "HOL-Library.Numeral_Type"
    12   "HOL-Library.Countable_Set"
    13   "HOL-Library.FuncSet"
    14 begin
    15 
    16 subsection%unimportant \<open>Finite Cartesian products, with indexing and lambdas\<close>
    17 
    18 typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
    19   morphisms vec_nth vec_lambda ..
    20 
    21 declare vec_lambda_inject [simplified, simp]
    22 
    23 bundle vec_syntax begin
    24 notation
    25   vec_nth (infixl "$" 90) and
    26   vec_lambda (binder "\<chi>" 10)
    27 end
    28 
    29 bundle no_vec_syntax begin
    30 no_notation
    31   vec_nth (infixl "$" 90) and
    32   vec_lambda (binder "\<chi>" 10)
    33 end
    34 
    35 unbundle vec_syntax
    36 
    37 text \<open>
    38   Concrete syntax for \<open>('a, 'b) vec\<close>:
    39     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
    40     \<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
    41 \<close>
    42 syntax "_vec_type" :: "type \<Rightarrow> type \<Rightarrow> type" (infixl "^" 15)
    43 parse_translation \<open>
    44   let
    45     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
    46     fun finite_vec_tr [t, u] =
    47       (case Term_Position.strip_positions u of
    48         v as Free (x, _) =>
    49           if Lexicon.is_tid x then
    50             vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
    51               Syntax.const @{class_syntax finite})
    52           else vec t u
    53       | _ => vec t u)
    54   in
    55     [(@{syntax_const "_vec_type"}, K finite_vec_tr)]
    56   end
    57 \<close>
    58 
    59 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
    60   by (simp add: vec_nth_inject [symmetric] fun_eq_iff)
    61 
    62 lemma vec_lambda_beta [simp]: "vec_lambda g $ i = g i"
    63   by (simp add: vec_lambda_inverse)
    64 
    65 lemma vec_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> vec_lambda g = f"
    66   by (auto simp add: vec_eq_iff)
    67 
    68 lemma vec_lambda_eta [simp]: "(\<chi> i. (g$i)) = g"
    69   by (simp add: vec_eq_iff)
    70 
    71 subsection%important \<open>Cardinality of vectors\<close>
    72 
    73 instance vec :: (finite, finite) finite
    74 proof
    75   show "finite (UNIV :: ('a, 'b) vec set)"
    76   proof (subst bij_betw_finite)
    77     show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
    78       by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
    79     have "finite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
    80       by (intro finite_PiE) auto
    81     also have "(PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set)) = Pi UNIV (\<lambda>_. UNIV)"
    82       by auto
    83     finally show "finite \<dots>" .
    84   qed
    85 qed
    86 
    87 lemma countable_PiE:
    88   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
    89   by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
    90 
    91 instance vec :: (countable, finite) countable
    92 proof
    93   have "countable (UNIV :: ('a, 'b) vec set)"
    94   proof (rule countableI_bij2)
    95     show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
    96       by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
    97     have "countable (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
    98       by (intro countable_PiE) auto
    99     also have "(PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set)) = Pi UNIV (\<lambda>_. UNIV)"
   100       by auto
   101     finally show "countable \<dots>" .
   102   qed
   103   thus "\<exists>t::('a, 'b) vec \<Rightarrow> nat. inj t"
   104     by (auto elim!: countableE)
   105 qed
   106 
   107 lemma%important infinite_UNIV_vec:
   108   assumes "infinite (UNIV :: 'a set)"
   109   shows   "infinite (UNIV :: ('a^'b) set)"
   110 proof%unimportant (subst bij_betw_finite)
   111   show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
   112     by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
   113   have "infinite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" (is "infinite ?A")
   114   proof
   115     assume "finite ?A"
   116     hence "finite ((\<lambda>f. f undefined) ` ?A)"
   117       by (rule finite_imageI)
   118     also have "(\<lambda>f. f undefined) ` ?A = UNIV"
   119       by auto
   120     finally show False 
   121       using \<open>infinite (UNIV :: 'a set)\<close> by contradiction
   122   qed
   123   also have "?A = Pi UNIV (\<lambda>_. UNIV)" 
   124     by auto
   125   finally show "infinite (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" .
   126 qed
   127 
   128 lemma%important CARD_vec [simp]:
   129   "CARD('a^'b) = CARD('a) ^ CARD('b)"
   130 proof%unimportant (cases "finite (UNIV :: 'a set)")
   131   case True
   132   show ?thesis
   133   proof (subst bij_betw_same_card)
   134     show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
   135       by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
   136     have "CARD('a) ^ CARD('b) = card (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
   137       (is "_ = card ?A")
   138       by (subst card_PiE) (auto simp: prod_constant)
   139     
   140     also have "?A = Pi UNIV (\<lambda>_. UNIV)" 
   141       by auto
   142     finally show "card \<dots> = CARD('a) ^ CARD('b)" ..
   143   qed
   144 qed (simp_all add: infinite_UNIV_vec)
   145 
   146 lemma%unimportant countable_vector:
   147   fixes B:: "'n::finite \<Rightarrow> 'a set"
   148   assumes "\<And>i. countable (B i)"
   149   shows "countable {V. \<forall>i::'n::finite. V $ i \<in> B i}"
   150 proof -
   151   have "f \<in> ($) ` {V. \<forall>i. V $ i \<in> B i}" if "f \<in> Pi\<^sub>E UNIV B" for f
   152   proof -
   153     have "\<exists>W. (\<forall>i. W $ i \<in> B i) \<and> ($) W = f"
   154       by (metis that PiE_iff UNIV_I vec_lambda_inverse)
   155     then show "f \<in> ($) ` {v. \<forall>i. v $ i \<in> B i}"
   156       by blast
   157   qed
   158   then have "Pi\<^sub>E UNIV B = vec_nth ` {V. \<forall>i::'n. V $ i \<in> B i}"
   159     by blast
   160   then have "countable (vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
   161     by (metis finite_class.finite_UNIV countable_PiE assms)
   162   then have "countable (vec_lambda ` vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
   163     by auto
   164   then show ?thesis
   165     by (simp add: image_comp o_def vec_nth_inverse)
   166 qed
   167 
   168 subsection%unimportant \<open>Group operations and class instances\<close>
   169 
   170 instantiation vec :: (zero, finite) zero
   171 begin
   172   definition "0 \<equiv> (\<chi> i. 0)"
   173   instance ..
   174 end
   175 
   176 instantiation vec :: (plus, finite) plus
   177 begin
   178   definition "(+) \<equiv> (\<lambda> x y. (\<chi> i. x$i + y$i))"
   179   instance ..
   180 end
   181 
   182 instantiation vec :: (minus, finite) minus
   183 begin
   184   definition "(-) \<equiv> (\<lambda> x y. (\<chi> i. x$i - y$i))"
   185   instance ..
   186 end
   187 
   188 instantiation vec :: (uminus, finite) uminus
   189 begin
   190   definition "uminus \<equiv> (\<lambda> x. (\<chi> i. - (x$i)))"
   191   instance ..
   192 end
   193 
   194 lemma zero_index [simp]: "0 $ i = 0"
   195   unfolding zero_vec_def by simp
   196 
   197 lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i"
   198   unfolding plus_vec_def by simp
   199 
   200 lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i"
   201   unfolding minus_vec_def by simp
   202 
   203 lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)"
   204   unfolding uminus_vec_def by simp
   205 
   206 instance vec :: (semigroup_add, finite) semigroup_add
   207   by standard (simp add: vec_eq_iff add.assoc)
   208 
   209 instance vec :: (ab_semigroup_add, finite) ab_semigroup_add
   210   by standard (simp add: vec_eq_iff add.commute)
   211 
   212 instance vec :: (monoid_add, finite) monoid_add
   213   by standard (simp_all add: vec_eq_iff)
   214 
   215 instance vec :: (comm_monoid_add, finite) comm_monoid_add
   216   by standard (simp add: vec_eq_iff)
   217 
   218 instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add
   219   by standard (simp_all add: vec_eq_iff)
   220 
   221 instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add
   222   by standard (simp_all add: vec_eq_iff diff_diff_eq)
   223 
   224 instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
   225 
   226 instance vec :: (group_add, finite) group_add
   227   by standard (simp_all add: vec_eq_iff)
   228 
   229 instance vec :: (ab_group_add, finite) ab_group_add
   230   by standard (simp_all add: vec_eq_iff)
   231 
   232 
   233 subsection%unimportant\<open>Basic componentwise operations on vectors\<close>
   234 
   235 instantiation vec :: (times, finite) times
   236 begin
   237 
   238 definition "(*) \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"
   239 instance ..
   240 
   241 end
   242 
   243 instantiation vec :: (one, finite) one
   244 begin
   245 
   246 definition "1 \<equiv> (\<chi> i. 1)"
   247 instance ..
   248 
   249 end
   250 
   251 instantiation vec :: (ord, finite) ord
   252 begin
   253 
   254 definition "x \<le> y \<longleftrightarrow> (\<forall>i. x$i \<le> y$i)"
   255 definition "x < (y::'a^'b) \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
   256 instance ..
   257 
   258 end
   259 
   260 text\<open>The ordering on one-dimensional vectors is linear.\<close>
   261 
   262 class cart_one =
   263   assumes UNIV_one: "card (UNIV :: 'a set) = Suc 0"
   264 begin
   265 
   266 subclass finite
   267 proof
   268   from UNIV_one show "finite (UNIV :: 'a set)"
   269     by (auto intro!: card_ge_0_finite)
   270 qed
   271 
   272 end
   273 
   274 instance vec:: (order, finite) order
   275   by standard (auto simp: less_eq_vec_def less_vec_def vec_eq_iff
   276       intro: order.trans order.antisym order.strict_implies_order)
   277 
   278 instance vec :: (linorder, cart_one) linorder
   279 proof
   280   obtain a :: 'b where all: "\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a"
   281   proof -
   282     have "card (UNIV :: 'b set) = Suc 0" by (rule UNIV_one)
   283     then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq)
   284     then have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P b" by auto
   285     then show thesis by (auto intro: that)
   286   qed
   287   fix x y :: "'a^'b::cart_one"
   288   note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps
   289   show "x \<le> y \<or> y \<le> x" by auto
   290 qed
   291 
   292 text\<open>Constant Vectors\<close>
   293 
   294 definition "vec x = (\<chi> i. x)"
   295 
   296 text\<open>Also the scalar-vector multiplication.\<close>
   297 
   298 definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
   299   where "c *s x = (\<chi> i. c * (x$i))"
   300 
   301 text \<open>scalar product\<close>
   302 
   303 definition scalar_product :: "'a :: semiring_1 ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" where
   304   "scalar_product v w = (\<Sum> i \<in> UNIV. v $ i * w $ i)"
   305 
   306 
   307 subsection%important \<open>Real vector space\<close>
   308 
   309 instantiation%unimportant vec :: (real_vector, finite) real_vector
   310 begin
   311 
   312 definition%important "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
   313 
   314 lemma%important vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)"
   315   unfolding scaleR_vec_def by simp
   316 
   317 instance%unimportant
   318   by standard (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)
   319 
   320 end
   321 
   322 
   323 subsection%important \<open>Topological space\<close>
   324 
   325 instantiation%unimportant vec :: (topological_space, finite) topological_space
   326 begin
   327 
   328 definition%important [code del]:
   329   "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
   330     (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
   331       (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
   332 
   333 instance proof%unimportant
   334   show "open (UNIV :: ('a ^ 'b) set)"
   335     unfolding open_vec_def by auto
   336 next
   337   fix S T :: "('a ^ 'b) set"
   338   assume "open S" "open T" thus "open (S \<inter> T)"
   339     unfolding open_vec_def
   340     apply clarify
   341     apply (drule (1) bspec)+
   342     apply (clarify, rename_tac Sa Ta)
   343     apply (rule_tac x="\<lambda>i. Sa i \<inter> Ta i" in exI)
   344     apply (simp add: open_Int)
   345     done
   346 next
   347   fix K :: "('a ^ 'b) set set"
   348   assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
   349     unfolding open_vec_def
   350     apply clarify
   351     apply (drule (1) bspec)
   352     apply (drule (1) bspec)
   353     apply clarify
   354     apply (rule_tac x=A in exI)
   355     apply fast
   356     done
   357 qed
   358 
   359 end
   360 
   361 lemma%unimportant open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}"
   362   unfolding open_vec_def by auto
   363 
   364 lemma%unimportant open_vimage_vec_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)"
   365   unfolding open_vec_def
   366   apply clarify
   367   apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)
   368   done
   369 
   370 lemma%unimportant closed_vimage_vec_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
   371   unfolding closed_open vimage_Compl [symmetric]
   372   by (rule open_vimage_vec_nth)
   373 
   374 lemma%unimportant closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
   375 proof -
   376   have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto
   377   thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
   378     by (simp add: closed_INT closed_vimage_vec_nth)
   379 qed
   380 
   381 lemma%important tendsto_vec_nth [tendsto_intros]:
   382   assumes "((\<lambda>x. f x) \<longlongrightarrow> a) net"
   383   shows "((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
   384 proof%unimportant (rule topological_tendstoI)
   385   fix S assume "open S" "a $ i \<in> S"
   386   then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
   387     by (simp_all add: open_vimage_vec_nth)
   388   with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net"
   389     by (rule topological_tendstoD)
   390   then show "eventually (\<lambda>x. f x $ i \<in> S) net"
   391     by simp
   392 qed
   393 
   394 lemma%unimportant isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
   395   unfolding isCont_def by (rule tendsto_vec_nth)
   396 
   397 lemma%important vec_tendstoI:
   398   assumes "\<And>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
   399   shows "((\<lambda>x. f x) \<longlongrightarrow> a) net"
   400 proof%unimportant (rule topological_tendstoI)
   401   fix S assume "open S" and "a \<in> S"
   402   then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i"
   403     and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S"
   404     unfolding open_vec_def by metis
   405   have "\<And>i. eventually (\<lambda>x. f x $ i \<in> A i) net"
   406     using assms A by (rule topological_tendstoD)
   407   hence "eventually (\<lambda>x. \<forall>i. f x $ i \<in> A i) net"
   408     by (rule eventually_all_finite)
   409   thus "eventually (\<lambda>x. f x \<in> S) net"
   410     by (rule eventually_mono, simp add: S)
   411 qed
   412 
   413 lemma%unimportant tendsto_vec_lambda [tendsto_intros]:
   414   assumes "\<And>i. ((\<lambda>x. f x i) \<longlongrightarrow> a i) net"
   415   shows "((\<lambda>x. \<chi> i. f x i) \<longlongrightarrow> (\<chi> i. a i)) net"
   416   using assms by (simp add: vec_tendstoI)
   417 
   418 lemma%important open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
   419 proof%unimportant (rule openI)
   420   fix a assume "a \<in> (\<lambda>x. x $ i) ` S"
   421   then obtain z where "a = z $ i" and "z \<in> S" ..
   422   then obtain A where A: "\<forall>i. open (A i) \<and> z $ i \<in> A i"
   423     and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
   424     using \<open>open S\<close> unfolding open_vec_def by auto
   425   hence "A i \<subseteq> (\<lambda>x. x $ i) ` S"
   426     by (clarsimp, rule_tac x="\<chi> j. if j = i then x else z $ j" in image_eqI,
   427       simp_all)
   428   hence "open (A i) \<and> a \<in> A i \<and> A i \<subseteq> (\<lambda>x. x $ i) ` S"
   429     using A \<open>a = z $ i\<close> by simp
   430   then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by - (rule exI)
   431 qed
   432 
   433 instance vec :: (perfect_space, finite) perfect_space
   434 proof
   435   fix x :: "'a ^ 'b" show "\<not> open {x}"
   436   proof
   437     assume "open {x}"
   438     hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth)
   439     hence "\<forall>i. open {x $ i}" by simp
   440     thus "False" by (simp add: not_open_singleton)
   441   qed
   442 qed
   443 
   444 
   445 subsection%important \<open>Metric space\<close>
   446 (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
   447 
   448 instantiation%unimportant vec :: (metric_space, finite) dist
   449 begin
   450 
   451 definition%important
   452   "dist x y = L2_set (\<lambda>i. dist (x$i) (y$i)) UNIV"
   453 
   454 instance ..
   455 end
   456 
   457 instantiation%unimportant vec :: (metric_space, finite) uniformity_dist
   458 begin
   459 
   460 definition%important [code del]:
   461   "(uniformity :: (('a^'b::_) \<times> ('a^'b::_)) filter) =
   462     (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
   463 
   464 instance%unimportant
   465   by standard (rule uniformity_vec_def)
   466 end
   467 
   468 declare uniformity_Abort[where 'a="'a :: metric_space ^ 'b :: finite", code]
   469 
   470 instantiation%unimportant vec :: (metric_space, finite) metric_space
   471 begin
   472 
   473 lemma%important dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
   474   unfolding dist_vec_def by (rule member_le_L2_set) simp_all
   475 
   476 instance proof%unimportant
   477   fix x y :: "'a ^ 'b"
   478   show "dist x y = 0 \<longleftrightarrow> x = y"
   479     unfolding dist_vec_def
   480     by (simp add: L2_set_eq_0_iff vec_eq_iff)
   481 next
   482   fix x y z :: "'a ^ 'b"
   483   show "dist x y \<le> dist x z + dist y z"
   484     unfolding dist_vec_def
   485     apply (rule order_trans [OF _ L2_set_triangle_ineq])
   486     apply (simp add: L2_set_mono dist_triangle2)
   487     done
   488 next
   489   fix S :: "('a ^ 'b) set"
   490   have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   491   proof
   492     assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
   493     proof
   494       fix x assume "x \<in> S"
   495       obtain A where A: "\<forall>i. open (A i)" "\<forall>i. x $ i \<in> A i"
   496         and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
   497         using \<open>open S\<close> and \<open>x \<in> S\<close> unfolding open_vec_def by metis
   498       have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i"
   499         using A unfolding open_dist by simp
   500       hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)"
   501         by (rule finite_set_choice [OF finite])
   502       then obtain r where r1: "\<forall>i. 0 < r i"
   503         and r2: "\<forall>i y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i" by fast
   504       have "0 < Min (range r) \<and> (\<forall>y. dist y x < Min (range r) \<longrightarrow> y \<in> S)"
   505         by (simp add: r1 r2 S le_less_trans [OF dist_vec_nth_le])
   506       thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" ..
   507     qed
   508   next
   509     assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S"
   510     proof (unfold open_vec_def, rule)
   511       fix x assume "x \<in> S"
   512       then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S"
   513         using * by fast
   514       define r where [abs_def]: "r i = e / sqrt (of_nat CARD('b))" for i :: 'b
   515       from \<open>0 < e\<close> have r: "\<forall>i. 0 < r i"
   516         unfolding r_def by simp_all
   517       from \<open>0 < e\<close> have e: "e = L2_set r UNIV"
   518         unfolding r_def by (simp add: L2_set_constant)
   519       define A where "A i = {y. dist (x $ i) y < r i}" for i
   520       have "\<forall>i. open (A i) \<and> x $ i \<in> A i"
   521         unfolding A_def by (simp add: open_ball r)
   522       moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S"
   523         by (simp add: A_def S dist_vec_def e L2_set_strict_mono dist_commute)
   524       ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and>
   525         (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
   526     qed
   527   qed
   528   show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
   529     unfolding * eventually_uniformity_metric
   530     by (simp del: split_paired_All add: dist_vec_def dist_commute)
   531 qed
   532 
   533 end
   534 
   535 lemma%important Cauchy_vec_nth:
   536   "Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)"
   537   unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_vec_nth_le])
   538 
   539 lemma%important vec_CauchyI:
   540   fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"
   541   assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"
   542   shows "Cauchy (\<lambda>n. X n)"
   543 proof%unimportant (rule metric_CauchyI)
   544   fix r :: real assume "0 < r"
   545   hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp
   546   define N where "N i = (LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s)" for i
   547   define M where "M = Max (range N)"
   548   have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
   549     using X \<open>0 < ?s\<close> by (rule metric_CauchyD)
   550   hence "\<And>i. \<forall>m\<ge>N i. \<forall>n\<ge>N i. dist (X m $ i) (X n $ i) < ?s"
   551     unfolding N_def by (rule LeastI_ex)
   552   hence M: "\<And>i. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < ?s"
   553     unfolding M_def by simp
   554   {
   555     fix m n :: nat
   556     assume "M \<le> m" "M \<le> n"
   557     have "dist (X m) (X n) = L2_set (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
   558       unfolding dist_vec_def ..
   559     also have "\<dots> \<le> sum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV"
   560       by (rule L2_set_le_sum [OF zero_le_dist])
   561     also have "\<dots> < sum (\<lambda>i::'n. ?s) UNIV"
   562       by (rule sum_strict_mono, simp_all add: M \<open>M \<le> m\<close> \<open>M \<le> n\<close>)
   563     also have "\<dots> = r"
   564       by simp
   565     finally have "dist (X m) (X n) < r" .
   566   }
   567   hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r"
   568     by simp
   569   then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" ..
   570 qed
   571 
   572 instance vec :: (complete_space, finite) complete_space
   573 proof
   574   fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X"
   575   have "\<And>i. (\<lambda>n. X n $ i) \<longlonglongrightarrow> lim (\<lambda>n. X n $ i)"
   576     using Cauchy_vec_nth [OF \<open>Cauchy X\<close>]
   577     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   578   hence "X \<longlonglongrightarrow> vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))"
   579     by (simp add: vec_tendstoI)
   580   then show "convergent X"
   581     by (rule convergentI)
   582 qed
   583 
   584 
   585 subsection%important \<open>Normed vector space\<close>
   586 
   587 instantiation%unimportant vec :: (real_normed_vector, finite) real_normed_vector
   588 begin
   589 
   590 definition%important "norm x = L2_set (\<lambda>i. norm (x$i)) UNIV"
   591 
   592 definition%important "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
   593 
   594 instance proof%unimportant
   595   fix a :: real and x y :: "'a ^ 'b"
   596   show "norm x = 0 \<longleftrightarrow> x = 0"
   597     unfolding norm_vec_def
   598     by (simp add: L2_set_eq_0_iff vec_eq_iff)
   599   show "norm (x + y) \<le> norm x + norm y"
   600     unfolding norm_vec_def
   601     apply (rule order_trans [OF _ L2_set_triangle_ineq])
   602     apply (simp add: L2_set_mono norm_triangle_ineq)
   603     done
   604   show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
   605     unfolding norm_vec_def
   606     by (simp add: L2_set_right_distrib)
   607   show "sgn x = scaleR (inverse (norm x)) x"
   608     by (rule sgn_vec_def)
   609   show "dist x y = norm (x - y)"
   610     unfolding dist_vec_def norm_vec_def
   611     by (simp add: dist_norm)
   612 qed
   613 
   614 end
   615 
   616 lemma%unimportant norm_nth_le: "norm (x $ i) \<le> norm x"
   617 unfolding norm_vec_def
   618 by (rule member_le_L2_set) simp_all
   619 
   620 lemma%important norm_le_componentwise_cart:
   621   fixes x :: "'a::real_normed_vector^'n"
   622   assumes "\<And>i. norm(x$i) \<le> norm(y$i)"
   623   shows "norm x \<le> norm y"
   624   unfolding%unimportant norm_vec_def
   625   by%unimportant (rule L2_set_mono) (auto simp: assms)
   626 
   627 lemma%unimportant component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
   628   apply (simp add: norm_vec_def)
   629   apply (rule member_le_L2_set, simp_all)
   630   done
   631 
   632 lemma%unimportant norm_bound_component_le_cart: "norm x \<le> e ==> \<bar>x$i\<bar> \<le> e"
   633   by (metis component_le_norm_cart order_trans)
   634 
   635 lemma%unimportant norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
   636   by (metis component_le_norm_cart le_less_trans)
   637 
   638 lemma%unimportant norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
   639   by (simp add: norm_vec_def L2_set_le_sum)
   640 
   641 lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
   642 apply standard
   643 apply (rule vector_add_component)
   644 apply (rule vector_scaleR_component)
   645 apply (rule_tac x="1" in exI, simp add: norm_nth_le)
   646 done
   647 
   648 instance vec :: (banach, finite) banach ..
   649 
   650 
   651 subsection%important \<open>Inner product space\<close>
   652 
   653 instantiation%unimportant vec :: (real_inner, finite) real_inner
   654 begin
   655 
   656 definition%important "inner x y = sum (\<lambda>i. inner (x$i) (y$i)) UNIV"
   657 
   658 instance proof%unimportant
   659   fix r :: real and x y z :: "'a ^ 'b"
   660   show "inner x y = inner y x"
   661     unfolding inner_vec_def
   662     by (simp add: inner_commute)
   663   show "inner (x + y) z = inner x z + inner y z"
   664     unfolding inner_vec_def
   665     by (simp add: inner_add_left sum.distrib)
   666   show "inner (scaleR r x) y = r * inner x y"
   667     unfolding inner_vec_def
   668     by (simp add: sum_distrib_left)
   669   show "0 \<le> inner x x"
   670     unfolding inner_vec_def
   671     by (simp add: sum_nonneg)
   672   show "inner x x = 0 \<longleftrightarrow> x = 0"
   673     unfolding inner_vec_def
   674     by (simp add: vec_eq_iff sum_nonneg_eq_0_iff)
   675   show "norm x = sqrt (inner x x)"
   676     unfolding inner_vec_def norm_vec_def L2_set_def
   677     by (simp add: power2_norm_eq_inner)
   678 qed
   679 
   680 end
   681 
   682 
   683 subsection%important \<open>Euclidean space\<close>
   684 
   685 text \<open>Vectors pointing along a single axis.\<close>
   686 
   687 definition%important "axis k x = (\<chi> i. if i = k then x else 0)"
   688 
   689 lemma%unimportant axis_nth [simp]: "axis i x $ i = x"
   690   unfolding axis_def by simp
   691 
   692 lemma%unimportant axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0"
   693   unfolding axis_def vec_eq_iff by auto
   694 
   695 lemma%unimportant inner_axis_axis:
   696   "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)"
   697   unfolding inner_vec_def
   698   apply (cases "i = j")
   699   apply clarsimp
   700   apply (subst sum.remove [of _ j], simp_all)
   701   apply (rule sum.neutral, simp add: axis_def)
   702   apply (rule sum.neutral, simp add: axis_def)
   703   done
   704 
   705 lemma%unimportant inner_axis: "inner x (axis i y) = inner (x $ i) y"
   706   by (simp add: inner_vec_def axis_def sum.remove [where x=i])
   707 
   708 lemma%unimportant inner_axis': "inner(axis i y) x = inner y (x $ i)"
   709   by (simp add: inner_axis inner_commute)
   710 
   711 instantiation%unimportant vec :: (euclidean_space, finite) euclidean_space
   712 begin
   713 
   714 definition%important "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"
   715 
   716 instance proof%unimportant
   717   show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
   718     unfolding Basis_vec_def by simp
   719 next
   720   show "finite (Basis :: ('a ^ 'b) set)"
   721     unfolding Basis_vec_def by simp
   722 next
   723   fix u v :: "'a ^ 'b"
   724   assume "u \<in> Basis" and "v \<in> Basis"
   725   thus "inner u v = (if u = v then 1 else 0)"
   726     unfolding Basis_vec_def
   727     by (auto simp add: inner_axis_axis axis_eq_axis inner_Basis)
   728 next
   729   fix x :: "'a ^ 'b"
   730   show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
   731     unfolding Basis_vec_def
   732     by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
   733 qed
   734 
   735 lemma%important DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
   736 proof%unimportant -
   737   have "card (\<Union>i::'b. \<Union>u::'a\<in>Basis. {axis i u}) = (\<Sum>i::'b\<in>UNIV. card (\<Union>u::'a\<in>Basis. {axis i u}))"
   738     by (rule card_UN_disjoint) (auto simp: axis_eq_axis) 
   739   also have "... = CARD('b) * DIM('a)"
   740     by (subst card_UN_disjoint) (auto simp: axis_eq_axis)
   741   finally show ?thesis
   742     by (simp add: Basis_vec_def)
   743 qed
   744 
   745 end
   746 
   747 lemma%unimportant norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
   748   by (simp add: inner_axis' norm_eq_1)
   749 
   750 lemma%important sum_norm_allsubsets_bound_cart:
   751   fixes f:: "'a \<Rightarrow> real ^'n"
   752   assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (sum f Q) \<le> e"
   753   shows "sum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
   754   using%unimportant sum_norm_allsubsets_bound[OF assms]
   755   by%unimportant simp
   756 
   757 lemma%unimportant cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
   758   by (simp add: inner_axis)
   759 
   760 lemma%unimportant axis_eq_0_iff [simp]:
   761   shows "axis m x = 0 \<longleftrightarrow> x = 0"
   762   by (simp add: axis_def vec_eq_iff)
   763 
   764 lemma%unimportant axis_in_Basis_iff [simp]: "axis i a \<in> Basis \<longleftrightarrow> a \<in> Basis"
   765   by (auto simp: Basis_vec_def axis_eq_axis)
   766 
   767 text\<open>Mapping each basis element to the corresponding finite index\<close>
   768 definition axis_index :: "('a::comm_ring_1)^'n \<Rightarrow> 'n" where "axis_index v \<equiv> SOME i. v = axis i 1"
   769 
   770 lemma%unimportant axis_inverse:
   771   fixes v :: "real^'n"
   772   assumes "v \<in> Basis"
   773   shows "\<exists>i. v = axis i 1"
   774 proof -
   775   have "v \<in> (\<Union>n. \<Union>r\<in>Basis. {axis n r})"
   776     using assms Basis_vec_def by blast
   777   then show ?thesis
   778     by (force simp add: vec_eq_iff)
   779 qed
   780 
   781 lemma%unimportant axis_index:
   782   fixes v :: "real^'n"
   783   assumes "v \<in> Basis"
   784   shows "v = axis (axis_index v) 1"
   785   by (metis (mono_tags) assms axis_inverse axis_index_def someI_ex)
   786 
   787 lemma%unimportant axis_index_axis [simp]:
   788   fixes UU :: "real^'n"
   789   shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)"
   790   by (simp add: axis_eq_axis axis_index_def)
   791 
   792 subsection%unimportant \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>
   793 
   794 lemma%unimportant sum_cong_aux:
   795   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> sum f A = sum g A"
   796   by (auto intro: sum.cong)
   797 
   798 hide_fact (open) sum_cong_aux
   799 
   800 method_setup vector = \<open>
   801 let
   802   val ss1 =
   803     simpset_of (put_simpset HOL_basic_ss @{context}
   804       addsimps [@{thm sum.distrib} RS sym,
   805       @{thm sum_subtractf} RS sym, @{thm sum_distrib_left},
   806       @{thm sum_distrib_right}, @{thm sum_negf} RS sym])
   807   val ss2 =
   808     simpset_of (@{context} addsimps
   809              [@{thm plus_vec_def}, @{thm times_vec_def},
   810               @{thm minus_vec_def}, @{thm uminus_vec_def},
   811               @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def},
   812               @{thm scaleR_vec_def},
   813               @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}])
   814   fun vector_arith_tac ctxt ths =
   815     simp_tac (put_simpset ss1 ctxt)
   816     THEN' (fn i => resolve_tac ctxt @{thms Finite_Cartesian_Product.sum_cong_aux} i
   817          ORELSE resolve_tac ctxt @{thms sum.neutral} i
   818          ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i)
   819     (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
   820     THEN' asm_full_simp_tac (put_simpset ss2 ctxt addsimps ths)
   821 in
   822   Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (vector_arith_tac ctxt ths))
   823 end
   824 \<close> "lift trivial vector statements to real arith statements"
   825 
   826 lemma%unimportant vec_0[simp]: "vec 0 = 0" by vector
   827 lemma%unimportant vec_1[simp]: "vec 1 = 1" by vector
   828 
   829 lemma%unimportant vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
   830 
   831 lemma%unimportant vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
   832 
   833 lemma%unimportant vec_add: "vec(x + y) = vec x + vec y"  by vector
   834 lemma%unimportant vec_sub: "vec(x - y) = vec x - vec y" by vector
   835 lemma%unimportant vec_cmul: "vec(c * x) = c *s vec x " by vector
   836 lemma%unimportant vec_neg: "vec(- x) = - vec x " by vector
   837 
   838 lemma%unimportant vec_scaleR: "vec(c * x) = c *\<^sub>R vec x"
   839   by vector
   840 
   841 lemma%unimportant vec_sum:
   842   assumes "finite S"
   843   shows "vec(sum f S) = sum (vec \<circ> f) S"
   844   using assms
   845 proof induct
   846   case empty
   847   then show ?case by simp
   848 next
   849   case insert
   850   then show ?case by (auto simp add: vec_add)
   851 qed
   852 
   853 text\<open>Obvious "component-pushing".\<close>
   854 
   855 lemma%unimportant vec_component [simp]: "vec x $ i = x"
   856   by vector
   857 
   858 lemma%unimportant vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
   859   by vector
   860 
   861 lemma%unimportant vector_smult_component [simp]: "(c *s y)$i = c * (y$i)"
   862   by vector
   863 
   864 lemma%unimportant cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
   865 
   866 lemmas%unimportant vector_component =
   867   vec_component vector_add_component vector_mult_component
   868   vector_smult_component vector_minus_component vector_uminus_component
   869   vector_scaleR_component cond_component
   870 
   871 
   872 subsection%unimportant \<open>Some frequently useful arithmetic lemmas over vectors\<close>
   873 
   874 instance vec :: (semigroup_mult, finite) semigroup_mult
   875   by standard (vector mult.assoc)
   876 
   877 instance vec :: (monoid_mult, finite) monoid_mult
   878   by standard vector+
   879 
   880 instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult
   881   by standard (vector mult.commute)
   882 
   883 instance vec :: (comm_monoid_mult, finite) comm_monoid_mult
   884   by standard vector
   885 
   886 instance vec :: (semiring, finite) semiring
   887   by standard (vector field_simps)+
   888 
   889 instance vec :: (semiring_0, finite) semiring_0
   890   by standard (vector field_simps)+
   891 instance vec :: (semiring_1, finite) semiring_1
   892   by standard vector
   893 instance vec :: (comm_semiring, finite) comm_semiring
   894   by standard (vector field_simps)+
   895 
   896 instance vec :: (comm_semiring_0, finite) comm_semiring_0 ..
   897 instance vec :: (semiring_0_cancel, finite) semiring_0_cancel ..
   898 instance vec :: (comm_semiring_0_cancel, finite) comm_semiring_0_cancel ..
   899 instance vec :: (ring, finite) ring ..
   900 instance vec :: (semiring_1_cancel, finite) semiring_1_cancel ..
   901 instance vec :: (comm_semiring_1, finite) comm_semiring_1 ..
   902 
   903 instance vec :: (ring_1, finite) ring_1 ..
   904 
   905 instance vec :: (real_algebra, finite) real_algebra
   906   by standard (simp_all add: vec_eq_iff)
   907 
   908 instance vec :: (real_algebra_1, finite) real_algebra_1 ..
   909 
   910 lemma of_nat_index: "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"
   911 proof (induct n)
   912   case 0
   913   then show ?case by vector
   914 next
   915   case Suc
   916   then show ?case by vector
   917 qed
   918 
   919 lemma one_index [simp]: "(1 :: 'a :: one ^ 'n) $ i = 1"
   920   by vector
   921 
   922 lemma neg_one_index [simp]: "(- 1 :: 'a :: {one, uminus} ^ 'n) $ i = - 1"
   923   by vector
   924 
   925 instance vec :: (semiring_char_0, finite) semiring_char_0
   926 proof
   927   fix m n :: nat
   928   show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"
   929     by (auto intro!: injI simp add: vec_eq_iff of_nat_index)
   930 qed
   931 
   932 instance vec :: (numeral, finite) numeral ..
   933 instance vec :: (semiring_numeral, finite) semiring_numeral ..
   934 
   935 lemma numeral_index [simp]: "numeral w $ i = numeral w"
   936   by (induct w) (simp_all only: numeral.simps vector_add_component one_index)
   937 
   938 lemma neg_numeral_index [simp]: "- numeral w $ i = - numeral w"
   939   by (simp only: vector_uminus_component numeral_index)
   940 
   941 instance vec :: (comm_ring_1, finite) comm_ring_1 ..
   942 instance vec :: (ring_char_0, finite) ring_char_0 ..
   943 
   944 lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
   945   by (vector mult.assoc)
   946 lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x"
   947   by (vector field_simps)
   948 lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y"
   949   by (vector field_simps)
   950 lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector
   951 lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector
   952 lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y"
   953   by (vector field_simps)
   954 lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector
   955 lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector
   956 lemma vector_sneg_minus1: "-x = (-1::'a::ring_1) *s x" by vector
   957 lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector
   958 lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"
   959   by (vector field_simps)
   960 
   961 lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
   962   by (simp add: vec_eq_iff)
   963 
   964 lemma Vector_Spaces_linear_vec [simp]: "Vector_Spaces.linear (*) vector_scalar_mult vec"
   965   by unfold_locales (vector algebra_simps)+
   966 
   967 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
   968   by vector
   969 
   970 lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::'a::field) \<or> x = y"
   971   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
   972 
   973 lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::'a::field) = b \<or> x = 0"
   974   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
   975 
   976 lemma scalar_mult_eq_scaleR [abs_def]: "c *s x = c *\<^sub>R x"
   977   unfolding scaleR_vec_def vector_scalar_mult_def by simp
   978 
   979 lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
   980   unfolding dist_norm scalar_mult_eq_scaleR
   981   unfolding scaleR_right_diff_distrib[symmetric] by simp
   982 
   983 lemma sum_component [simp]:
   984   fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
   985   shows "(sum f S)$i = sum (\<lambda>x. (f x)$i) S"
   986 proof (cases "finite S")
   987   case True
   988   then show ?thesis by induct simp_all
   989 next
   990   case False
   991   then show ?thesis by simp
   992 qed
   993 
   994 lemma sum_eq: "sum f S = (\<chi> i. sum (\<lambda>x. (f x)$i ) S)"
   995   by (simp add: vec_eq_iff)
   996 
   997 lemma sum_cmul:
   998   fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"
   999   shows "sum (\<lambda>x. c *s f x) S = c *s sum f S"
  1000   by (simp add: vec_eq_iff sum_distrib_left)
  1001 
  1002 lemma linear_vec [simp]: "linear vec"
  1003   using Vector_Spaces_linear_vec
  1004   apply (auto )
  1005   by unfold_locales (vector algebra_simps)+
  1006 
  1007 subsection%important \<open>Matrix operations\<close>
  1008 
  1009 text\<open>Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"}\<close>
  1010 
  1011 definition%important map_matrix::"('a \<Rightarrow> 'b) \<Rightarrow> (('a, 'i::finite)vec, 'j::finite) vec \<Rightarrow> (('b, 'i)vec, 'j) vec" where
  1012   "map_matrix f x = (\<chi> i j. f (x $ i $ j))"
  1013 
  1014 lemma%unimportant nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)"
  1015   by (simp add: map_matrix_def)
  1016 
  1017 definition%important matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
  1018     (infixl "**" 70)
  1019   where "m ** m' == (\<chi> i j. sum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
  1020 
  1021 definition%important matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm"
  1022     (infixl "*v" 70)
  1023   where "m *v x \<equiv> (\<chi> i. sum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"
  1024 
  1025 definition%important vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "
  1026     (infixl "v*" 70)
  1027   where "v v* m == (\<chi> j. sum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
  1028 
  1029 definition%unimportant "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
  1030 definition%unimportant transpose where
  1031   "(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
  1032 definition%unimportant "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
  1033 definition%unimportant "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
  1034 definition%unimportant "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
  1035 definition%unimportant "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
  1036 
  1037 lemma%unimportant times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" 
  1038   by (simp add: matrix_matrix_mult_def zero_vec_def)
  1039 
  1040 lemma%unimportant times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" 
  1041   by (simp add: matrix_matrix_mult_def zero_vec_def)
  1042 
  1043 lemma%unimportant mat_0[simp]: "mat 0 = 0" by (vector mat_def)
  1044 lemma%unimportant matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
  1045   by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)
  1046 
  1047 lemma%unimportant matrix_mul_lid [simp]:
  1048   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
  1049   shows "mat 1 ** A = A"
  1050   apply (simp add: matrix_matrix_mult_def mat_def)
  1051   apply vector
  1052   apply (auto simp only: if_distrib if_distribR sum.delta'[OF finite]
  1053     mult_1_left mult_zero_left if_True UNIV_I)
  1054   done
  1055 
  1056 lemma%unimportant matrix_mul_rid [simp]:
  1057   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
  1058   shows "A ** mat 1 = A"
  1059   apply (simp add: matrix_matrix_mult_def mat_def)
  1060   apply vector
  1061   apply (auto simp only: if_distrib if_distribR sum.delta[OF finite]
  1062     mult_1_right mult_zero_right if_True UNIV_I cong: if_cong)
  1063   done
  1064 
  1065 lemma%unimportant matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
  1066   apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
  1067   apply (subst sum.swap)
  1068   apply simp
  1069   done
  1070 
  1071 lemma%unimportant matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
  1072   apply (vector matrix_matrix_mult_def matrix_vector_mult_def
  1073     sum_distrib_left sum_distrib_right mult.assoc)
  1074   apply (subst sum.swap)
  1075   apply simp
  1076   done
  1077 
  1078 lemma%unimportant scalar_matrix_assoc:
  1079   fixes A :: "('a::real_algebra_1)^'m^'n"
  1080   shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B"
  1081   by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right)
  1082 
  1083 lemma%unimportant matrix_scalar_ac:
  1084   fixes A :: "('a::real_algebra_1)^'m^'n"
  1085   shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B"
  1086   by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
  1087 
  1088 lemma%unimportant matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
  1089   apply (vector matrix_vector_mult_def mat_def)
  1090   apply (simp add: if_distrib if_distribR sum.delta' cong del: if_weak_cong)
  1091   done
  1092 
  1093 lemma%unimportant matrix_transpose_mul:
  1094     "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
  1095   by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute)
  1096 
  1097 lemma%unimportant matrix_eq:
  1098   fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
  1099   shows "A = B \<longleftrightarrow>  (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
  1100   apply auto
  1101   apply (subst vec_eq_iff)
  1102   apply clarify
  1103   apply (clarsimp simp add: matrix_vector_mult_def if_distrib if_distribR vec_eq_iff cong del: if_weak_cong)
  1104   apply (erule_tac x="axis ia 1" in allE)
  1105   apply (erule_tac x="i" in allE)
  1106   apply (auto simp add: if_distrib if_distribR axis_def
  1107     sum.delta[OF finite] cong del: if_weak_cong)
  1108   done
  1109 
  1110 lemma%unimportant matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x"
  1111   by (simp add: matrix_vector_mult_def inner_vec_def)
  1112 
  1113 lemma%unimportant dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)"
  1114   apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
  1115   apply (subst sum.swap)
  1116   apply simp
  1117   done
  1118 
  1119 lemma%unimportant transpose_mat [simp]: "transpose (mat n) = mat n"
  1120   by (vector transpose_def mat_def)
  1121 
  1122 lemma%unimportant transpose_transpose [simp]: "transpose(transpose A) = A"
  1123   by (vector transpose_def)
  1124 
  1125 lemma%unimportant row_transpose [simp]: "row i (transpose A) = column i A"
  1126   by (simp add: row_def column_def transpose_def vec_eq_iff)
  1127 
  1128 lemma%unimportant column_transpose [simp]: "column i (transpose A) = row i A"
  1129   by (simp add: row_def column_def transpose_def vec_eq_iff)
  1130 
  1131 lemma%unimportant rows_transpose [simp]: "rows(transpose A) = columns A"
  1132   by (auto simp add: rows_def columns_def intro: set_eqI)
  1133 
  1134 lemma%unimportant columns_transpose [simp]: "columns(transpose A) = rows A"
  1135   by (metis transpose_transpose rows_transpose)
  1136 
  1137 lemma%unimportant transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A"
  1138   unfolding transpose_def
  1139   by (simp add: vec_eq_iff)
  1140 
  1141 lemma%unimportant transpose_iff [iff]: "transpose A = transpose B \<longleftrightarrow> A = B"
  1142   by (metis transpose_transpose)
  1143 
  1144 lemma%unimportant matrix_mult_sum:
  1145   "(A::'a::comm_semiring_1^'n^'m) *v x = sum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
  1146   by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute)
  1147 
  1148 lemma%unimportant vector_componentwise:
  1149   "(x::'a::ring_1^'n) = (\<chi> j. \<Sum>i\<in>UNIV. (x$i) * (axis i 1 :: 'a^'n) $ j)"
  1150   by (simp add: axis_def if_distrib sum.If_cases vec_eq_iff)
  1151 
  1152 lemma%unimportant basis_expansion: "sum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)"
  1153   by (auto simp add: axis_def vec_eq_iff if_distrib sum.If_cases cong del: if_weak_cong)
  1154 
  1155 
  1156 text\<open>Correspondence between matrices and linear operators.\<close>
  1157 
  1158 definition%important matrix :: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
  1159   where "matrix f = (\<chi> i j. (f(axis j 1))$i)"
  1160 
  1161 lemma%unimportant matrix_id_mat_1: "matrix id = mat 1"
  1162   by (simp add: mat_def matrix_def axis_def)
  1163 
  1164 lemma%unimportant matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r"
  1165   by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
  1166 
  1167 lemma%unimportant matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
  1168   by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left
  1169       sum.distrib scaleR_right.sum)
  1170 
  1171 lemma%unimportant vector_matrix_left_distrib [algebra_simps]:
  1172   shows "(x + y) v* A = x v* A + y v* A"
  1173   unfolding vector_matrix_mult_def
  1174   by (simp add: algebra_simps sum.distrib vec_eq_iff)
  1175 
  1176 lemma%unimportant matrix_vector_right_distrib [algebra_simps]:
  1177   "A *v (x + y) = A *v x + A *v y"
  1178   by (vector matrix_vector_mult_def sum.distrib distrib_left)
  1179 
  1180 lemma%unimportant matrix_vector_mult_diff_distrib [algebra_simps]:
  1181   fixes A :: "'a::ring_1^'n^'m"
  1182   shows "A *v (x - y) = A *v x - A *v y"
  1183   by (vector matrix_vector_mult_def sum_subtractf right_diff_distrib)
  1184 
  1185 lemma%unimportant matrix_vector_mult_scaleR[algebra_simps]:
  1186   fixes A :: "real^'n^'m"
  1187   shows "A *v (c *\<^sub>R x) = c *\<^sub>R (A *v x)"
  1188   using linear_iff matrix_vector_mul_linear by blast
  1189 
  1190 lemma%unimportant matrix_vector_mult_0_right [simp]: "A *v 0 = 0"
  1191   by (simp add: matrix_vector_mult_def vec_eq_iff)
  1192 
  1193 lemma%unimportant matrix_vector_mult_0 [simp]: "0 *v w = 0"
  1194   by (simp add: matrix_vector_mult_def vec_eq_iff)
  1195 
  1196 lemma%unimportant matrix_vector_mult_add_rdistrib [algebra_simps]:
  1197   "(A + B) *v x = (A *v x) + (B *v x)"
  1198   by (vector matrix_vector_mult_def sum.distrib distrib_right)
  1199 
  1200 lemma%unimportant matrix_vector_mult_diff_rdistrib [algebra_simps]:
  1201   fixes A :: "'a :: ring_1^'n^'m"
  1202   shows "(A - B) *v x = (A *v x) - (B *v x)"
  1203   by (vector matrix_vector_mult_def sum_subtractf left_diff_distrib)
  1204 
  1205 lemma%unimportant matrix_vector_column:
  1206   "(A::'a::comm_semiring_1^'n^_) *v x = sum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
  1207   by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute)
  1208 
  1209 subsection%important\<open>Inverse matrices  (not necessarily square)\<close>
  1210 
  1211 definition%important
  1212   "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
  1213 
  1214 definition%important
  1215   "matrix_inv(A:: 'a::semiring_1^'n^'m) =
  1216     (SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
  1217 
  1218 lemma%unimportant inj_matrix_vector_mult:
  1219   fixes A::"'a::field^'n^'m"
  1220   assumes "invertible A"
  1221   shows "inj ((*v) A)"
  1222   by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
  1223 
  1224 lemma%important scalar_invertible:
  1225   fixes A :: "('a::real_algebra_1)^'m^'n"
  1226   assumes "k \<noteq> 0" and "invertible A"
  1227   shows "invertible (k *\<^sub>R A)"
  1228 proof%unimportant -
  1229   obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
  1230     using assms unfolding invertible_def by auto
  1231   with \<open>k \<noteq> 0\<close>
  1232   have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
  1233     by (simp_all add: assms matrix_scalar_ac)
  1234   thus "invertible (k *\<^sub>R A)"
  1235     unfolding invertible_def by auto
  1236 qed
  1237 
  1238 lemma%unimportant scalar_invertible_iff:
  1239   fixes A :: "('a::real_algebra_1)^'m^'n"
  1240   assumes "k \<noteq> 0" and "invertible A"
  1241   shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
  1242   by (simp add: assms scalar_invertible)
  1243 
  1244 lemma%unimportant vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
  1245   unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
  1246   by simp
  1247 
  1248 lemma%unimportant transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
  1249   unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
  1250   by simp
  1251 
  1252 lemma%unimportant vector_scalar_commute:
  1253   fixes A :: "'a::{field}^'m^'n"
  1254   shows "A *v (c *s x) = c *s (A *v x)"
  1255   by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left)
  1256 
  1257 lemma%unimportant scalar_vector_matrix_assoc:
  1258   fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
  1259   shows "(k *s x) v* A = k *s (x v* A)"
  1260   by (metis transpose_matrix_vector vector_scalar_commute)
  1261  
  1262 lemma%unimportant vector_matrix_mult_0 [simp]: "0 v* A = 0"
  1263   unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
  1264 
  1265 lemma%unimportant vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
  1266   unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
  1267 
  1268 lemma%unimportant vector_matrix_mul_rid [simp]:
  1269   fixes v :: "('a::semiring_1)^'n"
  1270   shows "v v* mat 1 = v"
  1271   by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
  1272 
  1273 lemma%unimportant scaleR_vector_matrix_assoc:
  1274   fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
  1275   shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
  1276   by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
  1277 
  1278 lemma%important vector_scaleR_matrix_ac:
  1279   fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
  1280   shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
  1281 proof%unimportant -
  1282   have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
  1283     unfolding vector_matrix_mult_def
  1284     by (simp add: algebra_simps)
  1285   with scaleR_vector_matrix_assoc
  1286   show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
  1287     by auto
  1288 qed
  1289 
  1290 end