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