src/HOL/Analysis/Euclidean_Space.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69597 ff784d5a5bfb
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Euclidean_Space.thy
huffman@44133
     2
    Author:     Johannes Hölzl, TU München
huffman@44133
     3
    Author:     Brian Huffman, Portland State University
himmelma@33175
     4
*)
himmelma@33175
     5
wenzelm@60420
     6
section \<open>Finite-Dimensional Inner Product Spaces\<close>
himmelma@33175
     7
himmelma@33175
     8
theory Euclidean_Space
himmelma@33175
     9
imports
immler@69511
    10
  L2_Norm
immler@69511
    11
  Inner_Product
immler@69511
    12
  Product_Vector
hoelzl@37489
    13
begin
hoelzl@37489
    14
immler@69516
    15
immler@69516
    16
subsection%unimportant \<open>Interlude: Some properties of real sets\<close>
immler@69516
    17
immler@69516
    18
lemma seq_mono_lemma:
immler@69516
    19
  assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
immler@69516
    20
    and "\<forall>n \<ge> m. e n \<le> e m"
immler@69516
    21
  shows "\<forall>n \<ge> m. d n < e m"
immler@69516
    22
  using assms by force
immler@69516
    23
immler@69516
    24
wenzelm@60420
    25
subsection \<open>Type class of Euclidean spaces\<close>
hoelzl@37489
    26
nipkow@68617
    27
class euclidean_space = real_inner +
huffman@44166
    28
  fixes Basis :: "'a set"
huffman@44166
    29
  assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
huffman@44166
    30
  assumes finite_Basis [simp]: "finite Basis"
huffman@44166
    31
  assumes inner_Basis:
huffman@44166
    32
    "\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)"
huffman@44166
    33
  assumes euclidean_all_zero_iff:
huffman@44166
    34
    "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
huffman@44166
    35
wenzelm@63141
    36
syntax "_type_dimension" :: "type \<Rightarrow> nat"  ("(1DIM/(1'(_')))")
wenzelm@63141
    37
translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
wenzelm@63141
    38
typed_print_translation \<open>
wenzelm@69597
    39
  [(\<^const_syntax>\<open>card\<close>,
wenzelm@69597
    40
    fn ctxt => fn _ => fn [Const (\<^const_syntax>\<open>Basis\<close>, Type (\<^type_name>\<open>set\<close>, [T]))] =>
wenzelm@69597
    41
      Syntax.const \<^syntax_const>\<open>_type_dimension\<close> $ Syntax_Phases.term_of_typ ctxt T)]
wenzelm@63141
    42
\<close>
hoelzl@37489
    43
hoelzl@50526
    44
lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1"
huffman@44166
    45
  unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)
huffman@44166
    46
hoelzl@50526
    47
lemma (in euclidean_space) inner_same_Basis[simp]: "u \<in> Basis \<Longrightarrow> inner u u = 1"
hoelzl@50526
    48
  by (simp add: inner_Basis)
hoelzl@50526
    49
hoelzl@50526
    50
lemma (in euclidean_space) inner_not_same_Basis: "u \<in> Basis \<Longrightarrow> v \<in> Basis \<Longrightarrow> u \<noteq> v \<Longrightarrow> inner u v = 0"
hoelzl@50526
    51
  by (simp add: inner_Basis)
hoelzl@50526
    52
huffman@44166
    53
lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
hoelzl@50526
    54
  unfolding sgn_div_norm by (simp add: scaleR_one)
huffman@44166
    55
huffman@44166
    56
lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
huffman@44166
    57
proof
huffman@44166
    58
  assume "0 \<in> Basis" thus "False"
huffman@44166
    59
    using inner_Basis [of 0 0] by simp
huffman@44166
    60
qed
huffman@44166
    61
huffman@44166
    62
lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0"
huffman@44166
    63
  by clarsimp
huffman@44166
    64
hoelzl@50526
    65
lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
hoelzl@50526
    66
  by (metis ex_in_conv nonempty_Basis someI_ex)
huffman@44166
    67
lp15@64773
    68
lemma norm_some_Basis [simp]: "norm (SOME i. i \<in> Basis) = 1"
lp15@64773
    69
  by (simp add: SOME_Basis)
lp15@64773
    70
nipkow@64267
    71
lemma (in euclidean_space) inner_sum_left_Basis[simp]:
hoelzl@50526
    72
    "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
nipkow@64267
    73
  by (simp add: inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.If_cases)
huffman@44166
    74
hoelzl@50526
    75
lemma (in euclidean_space) euclidean_eqI:
hoelzl@50526
    76
  assumes b: "\<And>b. b \<in> Basis \<Longrightarrow> inner x b = inner y b" shows "x = y"
hoelzl@37489
    77
proof -
hoelzl@50526
    78
  from b have "\<forall>b\<in>Basis. inner (x - y) b = 0"
hoelzl@50526
    79
    by (simp add: inner_diff_left)
hoelzl@50526
    80
  then show "x = y"
hoelzl@50526
    81
    by (simp add: euclidean_all_zero_iff)
hoelzl@37489
    82
qed
hoelzl@37489
    83
hoelzl@50526
    84
lemma (in euclidean_space) euclidean_eq_iff:
hoelzl@50526
    85
  "x = y \<longleftrightarrow> (\<forall>b\<in>Basis. inner x b = inner y b)"
huffman@44129
    86
  by (auto intro: euclidean_eqI)
huffman@44129
    87
nipkow@64267
    88
lemma (in euclidean_space) euclidean_representation_sum:
hoelzl@50526
    89
  "(\<Sum>i\<in>Basis. f i *\<^sub>R i) = b \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
hoelzl@50526
    90
  by (subst euclidean_eq_iff) simp
hoelzl@37489
    91
nipkow@64267
    92
lemma (in euclidean_space) euclidean_representation_sum':
immler@54776
    93
  "b = (\<Sum>i\<in>Basis. f i *\<^sub>R i) \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
nipkow@64267
    94
  by (auto simp add: euclidean_representation_sum[symmetric])
immler@54776
    95
hoelzl@50526
    96
lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
nipkow@64267
    97
  unfolding euclidean_representation_sum by simp
huffman@44129
    98
immler@67685
    99
lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (inner x b) * (inner y b))"
immler@67685
   100
  by (subst (1 2) euclidean_representation [symmetric])
immler@67685
   101
    (simp add: inner_sum_right inner_Basis ac_simps)
immler@67685
   102
hoelzl@50526
   103
lemma (in euclidean_space) choice_Basis_iff:
hoelzl@50526
   104
  fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
hoelzl@50526
   105
  shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
hoelzl@50526
   106
  unfolding bchoice_iff
hoelzl@50526
   107
proof safe
hoelzl@50526
   108
  fix f assume "\<forall>i\<in>Basis. P i (f i)"
hoelzl@50526
   109
  then show "\<exists>x. \<forall>i\<in>Basis. P i (inner x i)"
hoelzl@50526
   110
    by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
hoelzl@50526
   111
qed auto
hoelzl@37489
   112
lp15@63952
   113
lemma (in euclidean_space) bchoice_Basis_iff:
lp15@63952
   114
  fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
lp15@63952
   115
  shows "(\<forall>i\<in>Basis. \<exists>x\<in>A. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. inner x i \<in> A \<and> P i (inner x i))"
lp15@63952
   116
by (simp add: choice_Basis_iff Bex_def)
lp15@63952
   117
nipkow@64267
   118
lemma (in euclidean_space) euclidean_representation_sum_fun:
lp15@60974
   119
    "(\<lambda>x. \<Sum>b\<in>Basis. inner (f x) b *\<^sub>R b) = f"
nipkow@64267
   120
  by (rule ext) (simp add: euclidean_representation_sum)
lp15@60974
   121
lp15@60974
   122
lemma euclidean_isCont:
lp15@60974
   123
  assumes "\<And>b. b \<in> Basis \<Longrightarrow> isCont (\<lambda>x. (inner (f x) b) *\<^sub>R b) x"
lp15@60974
   124
    shows "isCont f x"
nipkow@64267
   125
  apply (subst euclidean_representation_sum_fun [symmetric])
nipkow@64267
   126
  apply (rule isCont_sum)
lp15@60974
   127
  apply (blast intro: assms)
lp15@60974
   128
  done
lp15@60974
   129
lp15@63938
   130
lemma DIM_positive [simp]: "0 < DIM('a::euclidean_space)"
hoelzl@50526
   131
  by (simp add: card_gt_0_iff)
huffman@44628
   132
lp15@63938
   133
lemma DIM_ge_Suc0 [simp]: "Suc 0 \<le> card Basis"
lp15@63007
   134
  by (meson DIM_positive Suc_leI)
lp15@63007
   135
lp15@63114
   136
nipkow@64267
   137
lemma sum_inner_Basis_scaleR [simp]:
lp15@63114
   138
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_vector"
lp15@63114
   139
  assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) *\<^sub>R f i) = f b"
nipkow@64267
   140
  by (simp add: comm_monoid_add_class.sum.remove [OF finite_Basis assms]
nipkow@64267
   141
         assms inner_not_same_Basis comm_monoid_add_class.sum.neutral)
lp15@63114
   142
nipkow@64267
   143
lemma sum_inner_Basis_eq [simp]:
lp15@63114
   144
  assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) * f i) = f b"
nipkow@64267
   145
  by (simp add: comm_monoid_add_class.sum.remove [OF finite_Basis assms]
nipkow@64267
   146
         assms inner_not_same_Basis comm_monoid_add_class.sum.neutral)
lp15@63114
   147
lp15@66154
   148
lemma sum_if_inner [simp]:
lp15@66154
   149
  assumes "i \<in> Basis" "j \<in> Basis"
lp15@66154
   150
    shows "inner (\<Sum>k\<in>Basis. if k = i then f i *\<^sub>R i else g k *\<^sub>R k) j = (if j=i then f j else g j)"
lp15@66154
   151
proof (cases "i=j")
lp15@66154
   152
  case True
lp15@66154
   153
  with assms show ?thesis
lp15@66154
   154
    by (auto simp: inner_sum_left if_distrib [of "\<lambda>x. inner x j"] inner_Basis cong: if_cong)
lp15@66154
   155
next
lp15@66154
   156
  case False
lp15@66154
   157
  have "(\<Sum>k\<in>Basis. inner (if k = i then f i *\<^sub>R i else g k *\<^sub>R k) j) =
lp15@66154
   158
        (\<Sum>k\<in>Basis. if k = j then g k else 0)"
lp15@66154
   159
    apply (rule sum.cong)
lp15@66154
   160
    using False assms by (auto simp: inner_Basis)
lp15@66154
   161
  also have "... = g j"
lp15@66154
   162
    using assms by auto
lp15@66154
   163
  finally show ?thesis
lp15@66154
   164
    using False by (auto simp: inner_sum_left)
lp15@66154
   165
qed
lp15@66154
   166
immler@68072
   167
lemma norm_le_componentwise:
immler@68072
   168
   "(\<And>b. b \<in> Basis \<Longrightarrow> abs(inner x b) \<le> abs(inner y b)) \<Longrightarrow> norm x \<le> norm y"
immler@68072
   169
  by (auto simp: norm_le euclidean_inner [of x x] euclidean_inner [of y y] abs_le_square_iff power2_eq_square intro!: sum_mono)
immler@68072
   170
immler@68072
   171
lemma Basis_le_norm: "b \<in> Basis \<Longrightarrow> \<bar>inner x b\<bar> \<le> norm x"
immler@68072
   172
  by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
immler@68072
   173
immler@68072
   174
lemma norm_bound_Basis_le: "b \<in> Basis \<Longrightarrow> norm x \<le> e \<Longrightarrow> \<bar>inner x b\<bar> \<le> e"
immler@68072
   175
  by (metis Basis_le_norm order_trans)
immler@68072
   176
immler@68072
   177
lemma norm_bound_Basis_lt: "b \<in> Basis \<Longrightarrow> norm x < e \<Longrightarrow> \<bar>inner x b\<bar> < e"
immler@68072
   178
  by (metis Basis_le_norm le_less_trans)
immler@68072
   179
immler@68072
   180
lemma norm_le_l1: "norm x \<le> (\<Sum>b\<in>Basis. \<bar>inner x b\<bar>)"
immler@68072
   181
  apply (subst euclidean_representation[of x, symmetric])
immler@68072
   182
  apply (rule order_trans[OF norm_sum])
immler@68072
   183
  apply (auto intro!: sum_mono)
immler@68072
   184
  done
immler@68072
   185
immler@68072
   186
lemma sum_norm_allsubsets_bound:
immler@68072
   187
  fixes f :: "'a \<Rightarrow> 'n::euclidean_space"
immler@68072
   188
  assumes fP: "finite P"
immler@68072
   189
    and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (sum f Q) \<le> e"
immler@68072
   190
  shows "(\<Sum>x\<in>P. norm (f x)) \<le> 2 * real DIM('n) * e"
immler@68072
   191
proof -
immler@68072
   192
  have "(\<Sum>x\<in>P. norm (f x)) \<le> (\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>inner (f x) b\<bar>)"
immler@68072
   193
    by (rule sum_mono) (rule norm_le_l1)
immler@68072
   194
  also have "(\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>inner (f x) b\<bar>) = (\<Sum>b\<in>Basis. \<Sum>x\<in>P. \<bar>inner (f x) b\<bar>)"
immler@68072
   195
    by (rule sum.swap)
immler@68072
   196
  also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
immler@68072
   197
  proof (rule sum_bounded_above)
immler@68072
   198
    fix i :: 'n
immler@68072
   199
    assume i: "i \<in> Basis"
immler@68072
   200
    have "norm (\<Sum>x\<in>P. \<bar>inner (f x) i\<bar>) \<le>
immler@68072
   201
      norm (inner (\<Sum>x\<in>P \<inter> - {x. inner (f x) i < 0}. f x) i) + norm (inner (\<Sum>x\<in>P \<inter> {x. inner (f x) i < 0}. f x) i)"
immler@68072
   202
      by (simp add: abs_real_def sum.If_cases[OF fP] sum_negf norm_triangle_ineq4 inner_sum_left
immler@68072
   203
        del: real_norm_def)
immler@68072
   204
    also have "\<dots> \<le> e + e"
immler@68072
   205
      unfolding real_norm_def
immler@68072
   206
      by (intro add_mono norm_bound_Basis_le i fPs) auto
immler@68072
   207
    finally show "(\<Sum>x\<in>P. \<bar>inner (f x) i\<bar>) \<le> 2*e" by simp
immler@68072
   208
  qed
immler@68072
   209
  also have "\<dots> = 2 * real DIM('n) * e" by simp
immler@68072
   210
  finally show ?thesis .
immler@68072
   211
qed
immler@68072
   212
immler@68072
   213
immler@67962
   214
subsection%unimportant \<open>Subclass relationships\<close>
huffman@44571
   215
huffman@44571
   216
instance euclidean_space \<subseteq> perfect_space
huffman@44571
   217
proof
huffman@44571
   218
  fix x :: 'a show "\<not> open {x}"
huffman@44571
   219
  proof
huffman@44571
   220
    assume "open {x}"
huffman@44571
   221
    then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x"
huffman@44571
   222
      unfolding open_dist by fast
wenzelm@63040
   223
    define y where "y = x + scaleR (e/2) (SOME b. b \<in> Basis)"
hoelzl@50526
   224
    have [simp]: "(SOME b. b \<in> Basis) \<in> Basis"
hoelzl@50526
   225
      by (rule someI_ex) (auto simp: ex_in_conv)
wenzelm@60420
   226
    from \<open>0 < e\<close> have "y \<noteq> x"
hoelzl@50526
   227
      unfolding y_def by (auto intro!: nonzero_Basis)
wenzelm@60420
   228
    from \<open>0 < e\<close> have "dist y x < e"
huffman@53939
   229
      unfolding y_def by (simp add: dist_norm)
wenzelm@60420
   230
    from \<open>y \<noteq> x\<close> and \<open>dist y x < e\<close> show "False"
huffman@44571
   231
      using e by simp
huffman@44571
   232
  qed
huffman@44571
   233
qed
huffman@44571
   234
wenzelm@60420
   235
subsection \<open>Class instances\<close>
himmelma@33175
   236
wenzelm@69597
   237
subsubsection%unimportant \<open>Type \<^typ>\<open>real\<close>\<close>
hoelzl@37489
   238
nipkow@68617
   239
instantiation real :: euclidean_space
hoelzl@37489
   240
begin
huffman@44129
   241
hoelzl@63627
   242
definition
hoelzl@50526
   243
  [simp]: "Basis = {1::real}"
huffman@44129
   244
huffman@44129
   245
instance
wenzelm@61169
   246
  by standard auto
huffman@44129
   247
huffman@44129
   248
end
hoelzl@37489
   249
hoelzl@50526
   250
lemma DIM_real[simp]: "DIM(real) = 1"
hoelzl@50526
   251
  by simp
hoelzl@50526
   252
wenzelm@69597
   253
subsubsection%unimportant \<open>Type \<^typ>\<open>complex\<close>\<close>
hoelzl@37489
   254
nipkow@68617
   255
instantiation complex :: euclidean_space
hoelzl@37489
   256
begin
huffman@44129
   257
wenzelm@63589
   258
definition Basis_complex_def: "Basis = {1, \<i>}"
huffman@44166
   259
huffman@44166
   260
instance
nipkow@62390
   261
  by standard (auto simp add: Basis_complex_def intro: complex_eqI split: if_split_asm)
huffman@44129
   262
huffman@44129
   263
end
huffman@44129
   264
hoelzl@37489
   265
lemma DIM_complex[simp]: "DIM(complex) = 2"
hoelzl@50526
   266
  unfolding Basis_complex_def by simp
hoelzl@37489
   267
lp15@68310
   268
lemma complex_Basis_1 [iff]: "(1::complex) \<in> Basis"
lp15@68310
   269
  by (simp add: Basis_complex_def)
lp15@68310
   270
lp15@68310
   271
lemma complex_Basis_i [iff]: "\<i> \<in> Basis"
lp15@68310
   272
  by (simp add: Basis_complex_def)
lp15@68310
   273
wenzelm@69597
   274
subsubsection%unimportant \<open>Type \<^typ>\<open>'a \<times> 'b\<close>\<close>
hoelzl@38656
   275
immler@69511
   276
instantiation prod :: (real_inner, real_inner) real_inner
immler@69511
   277
begin
immler@69511
   278
immler@69511
   279
definition inner_prod_def:
immler@69511
   280
  "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
immler@69511
   281
immler@69511
   282
lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
immler@69511
   283
  unfolding inner_prod_def by simp
immler@69511
   284
immler@69511
   285
instance
immler@69511
   286
proof
immler@69511
   287
  fix r :: real
immler@69511
   288
  fix x y z :: "'a::real_inner \<times> 'b::real_inner"
immler@69511
   289
  show "inner x y = inner y x"
immler@69511
   290
    unfolding inner_prod_def
immler@69511
   291
    by (simp add: inner_commute)
immler@69511
   292
  show "inner (x + y) z = inner x z + inner y z"
immler@69511
   293
    unfolding inner_prod_def
immler@69511
   294
    by (simp add: inner_add_left)
immler@69511
   295
  show "inner (scaleR r x) y = r * inner x y"
immler@69511
   296
    unfolding inner_prod_def
immler@69511
   297
    by (simp add: distrib_left)
immler@69511
   298
  show "0 \<le> inner x x"
immler@69511
   299
    unfolding inner_prod_def
immler@69511
   300
    by (intro add_nonneg_nonneg inner_ge_zero)
immler@69511
   301
  show "inner x x = 0 \<longleftrightarrow> x = 0"
immler@69511
   302
    unfolding inner_prod_def prod_eq_iff
immler@69511
   303
    by (simp add: add_nonneg_eq_0_iff)
immler@69511
   304
  show "norm x = sqrt (inner x x)"
immler@69511
   305
    unfolding norm_prod_def inner_prod_def
immler@69511
   306
    by (simp add: power2_norm_eq_inner)
immler@69511
   307
qed
immler@69511
   308
immler@69511
   309
end
immler@69511
   310
immler@69511
   311
lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
immler@69511
   312
    by (cases x, simp)+
immler@69511
   313
nipkow@68617
   314
instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
hoelzl@38656
   315
begin
hoelzl@38656
   316
huffman@44129
   317
definition
huffman@44166
   318
  "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"
huffman@44166
   319
nipkow@64267
   320
lemma sum_Basis_prod_eq:
immler@54781
   321
  fixes f::"('a*'b)\<Rightarrow>('a*'b)"
nipkow@64267
   322
  shows "sum f Basis = sum (\<lambda>i. f (i, 0)) Basis + sum (\<lambda>i. f (0, i)) Basis"
immler@54781
   323
proof -
immler@54781
   324
  have "inj_on (\<lambda>u. (u::'a, 0::'b)) Basis" "inj_on (\<lambda>u. (0::'a, u::'b)) Basis"
immler@54781
   325
    by (auto intro!: inj_onI Pair_inject)
immler@54781
   326
  thus ?thesis
immler@54781
   327
    unfolding Basis_prod_def
nipkow@64267
   328
    by (subst sum.union_disjoint) (auto simp: Basis_prod_def sum.reindex)
immler@54781
   329
qed
immler@54781
   330
huffman@44129
   331
instance proof
huffman@44166
   332
  show "(Basis :: ('a \<times> 'b) set) \<noteq> {}"
huffman@44166
   333
    unfolding Basis_prod_def by simp
huffman@44129
   334
next
huffman@44166
   335
  show "finite (Basis :: ('a \<times> 'b) set)"
huffman@44166
   336
    unfolding Basis_prod_def by simp
huffman@44129
   337
next
huffman@44166
   338
  fix u v :: "'a \<times> 'b"
huffman@44166
   339
  assume "u \<in> Basis" and "v \<in> Basis"
huffman@44166
   340
  thus "inner u v = (if u = v then 1 else 0)"
huffman@44166
   341
    unfolding Basis_prod_def inner_prod_def
nipkow@62390
   342
    by (auto simp add: inner_Basis split: if_split_asm)
huffman@44129
   343
next
huffman@44129
   344
  fix x :: "'a \<times> 'b"
huffman@44166
   345
  show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
huffman@44166
   346
    unfolding Basis_prod_def ball_Un ball_simps
huffman@44166
   347
    by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
hoelzl@38656
   348
qed
huffman@44129
   349
hoelzl@50526
   350
lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('a) + DIM('b)"
hoelzl@50526
   351
  unfolding Basis_prod_def
nipkow@67399
   352
  by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="(+)"] inj_onI)
hoelzl@50526
   353
hoelzl@37489
   354
end
hoelzl@38656
   355
immler@68072
   356
immler@68072
   357
subsection \<open>Locale instances\<close>
immler@68072
   358
immler@68072
   359
lemma finite_dimensional_vector_space_euclidean:
nipkow@69064
   360
  "finite_dimensional_vector_space (*\<^sub>R) Basis"
immler@68072
   361
proof unfold_locales
immler@68072
   362
  show "finite (Basis::'a set)" by (metis finite_Basis)
immler@68072
   363
  show "real_vector.independent (Basis::'a set)"
immler@68072
   364
    unfolding dependent_def dependent_raw_def[symmetric]
immler@68072
   365
    apply (subst span_finite)
immler@68072
   366
    apply simp
immler@68072
   367
    apply clarify
immler@68072
   368
    apply (drule_tac f="inner a" in arg_cong)
immler@68072
   369
    apply (simp add: inner_Basis inner_sum_right eq_commute)
immler@68072
   370
    done
nipkow@69064
   371
  show "module.span (*\<^sub>R) Basis = UNIV"
immler@68072
   372
    unfolding span_finite [OF finite_Basis] span_raw_def[symmetric]
immler@68072
   373
    by (auto intro!: euclidean_representation[symmetric])
immler@68072
   374
qed
immler@68072
   375
immler@68072
   376
interpretation eucl?: finite_dimensional_vector_space "scaleR :: real => 'a => 'a::euclidean_space" "Basis"
nipkow@69064
   377
  rewrites "module.dependent (*\<^sub>R) = dependent"
nipkow@69064
   378
    and "module.representation (*\<^sub>R) = representation"
nipkow@69064
   379
    and "module.subspace (*\<^sub>R) = subspace"
nipkow@69064
   380
    and "module.span (*\<^sub>R) = span"
nipkow@69064
   381
    and "vector_space.extend_basis (*\<^sub>R) = extend_basis"
nipkow@69064
   382
    and "vector_space.dim (*\<^sub>R) = dim"
nipkow@69064
   383
    and "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
nipkow@69064
   384
    and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
immler@68072
   385
    and "finite_dimensional_vector_space.dimension Basis = DIM('a)"
immler@68072
   386
    and "dimension = DIM('a)"
immler@68072
   387
  by (auto simp add: dependent_raw_def representation_raw_def
immler@68072
   388
      subspace_raw_def span_raw_def extend_basis_raw_def dim_raw_def linear_def
immler@68072
   389
      real_scaleR_def[abs_def]
immler@68072
   390
      finite_dimensional_vector_space.dimension_def
immler@68072
   391
      intro!: finite_dimensional_vector_space.dimension_def
immler@68072
   392
      finite_dimensional_vector_space_euclidean)
immler@68072
   393
immler@68620
   394
interpretation eucl?: finite_dimensional_vector_space_pair_1
immler@68620
   395
  "scaleR::real\<Rightarrow>'a::euclidean_space\<Rightarrow>'a" Basis
immler@68620
   396
  "scaleR::real\<Rightarrow>'b::real_vector \<Rightarrow> 'b"
immler@68620
   397
  by unfold_locales
immler@68620
   398
immler@68072
   399
interpretation eucl?: finite_dimensional_vector_space_prod scaleR scaleR Basis Basis
immler@68072
   400
  rewrites "Basis_pair = Basis"
nipkow@69064
   401
    and "module_prod.scale (*\<^sub>R) (*\<^sub>R) = (scaleR::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
immler@68072
   402
proof -
nipkow@69064
   403
  show "finite_dimensional_vector_space_prod (*\<^sub>R) (*\<^sub>R) Basis Basis"
immler@68072
   404
    by unfold_locales
nipkow@69064
   405
  interpret finite_dimensional_vector_space_prod "(*\<^sub>R)" "(*\<^sub>R)" "Basis::'a set" "Basis::'b set"
immler@68072
   406
    by fact
immler@68072
   407
  show "Basis_pair = Basis"
immler@68072
   408
    unfolding Basis_pair_def Basis_prod_def by auto
nipkow@69064
   409
  show "module_prod.scale (*\<^sub>R) (*\<^sub>R) = scaleR"
immler@68072
   410
    by (fact module_prod_scale_eq_scaleR)
immler@68072
   411
qed
immler@68072
   412
hoelzl@38656
   413
end