src/HOL/Real/RealVector.thy
author nipkow
Tue Oct 23 23:27:23 2007 +0200 (2007-10-23)
changeset 25162 ad4d5365d9d8
parent 25062 af5ef0d4d655
child 25571 c9e39eafc7a0
permissions -rw-r--r--
went back to >0
     1 (*  Title       : RealVector.thy
     2     ID:         $Id$
     3     Author      : Brian Huffman
     4 *)
     5 
     6 header {* Vector Spaces and Algebras over the Reals *}
     7 
     8 theory RealVector
     9 imports RealPow
    10 begin
    11 
    12 subsection {* Locale for additive functions *}
    13 
    14 locale additive =
    15   fixes f :: "'a::ab_group_add \<Rightarrow> 'b::ab_group_add"
    16   assumes add: "f (x + y) = f x + f y"
    17 
    18 lemma (in additive) zero: "f 0 = 0"
    19 proof -
    20   have "f 0 = f (0 + 0)" by simp
    21   also have "\<dots> = f 0 + f 0" by (rule add)
    22   finally show "f 0 = 0" by simp
    23 qed
    24 
    25 lemma (in additive) minus: "f (- x) = - f x"
    26 proof -
    27   have "f (- x) + f x = f (- x + x)" by (rule add [symmetric])
    28   also have "\<dots> = - f x + f x" by (simp add: zero)
    29   finally show "f (- x) = - f x" by (rule add_right_imp_eq)
    30 qed
    31 
    32 lemma (in additive) diff: "f (x - y) = f x - f y"
    33 by (simp add: diff_def add minus)
    34 
    35 lemma (in additive) setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
    36 apply (cases "finite A")
    37 apply (induct set: finite)
    38 apply (simp add: zero)
    39 apply (simp add: add)
    40 apply (simp add: zero)
    41 done
    42 
    43 
    44 subsection {* Real vector spaces *}
    45 
    46 class scaleR = type +
    47   fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
    48 begin
    49 
    50 abbreviation
    51   divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "'/\<^sub>R" 70)
    52 where
    53   "x /\<^sub>R r == scaleR (inverse r) x"
    54 
    55 end
    56 
    57 instance real :: scaleR
    58   real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
    59 
    60 class real_vector = scaleR + ab_group_add +
    61   assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
    62   and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
    63   and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
    64   and scaleR_one [simp]: "scaleR 1 x = x"
    65 
    66 class real_algebra = real_vector + ring +
    67   assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
    68   and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
    69 
    70 class real_algebra_1 = real_algebra + ring_1
    71 
    72 class real_div_algebra = real_algebra_1 + division_ring
    73 
    74 class real_field = real_div_algebra + field
    75 
    76 instance real :: real_field
    77 apply (intro_classes, unfold real_scaleR_def)
    78 apply (rule right_distrib)
    79 apply (rule left_distrib)
    80 apply (rule mult_assoc [symmetric])
    81 apply (rule mult_1_left)
    82 apply (rule mult_assoc)
    83 apply (rule mult_left_commute)
    84 done
    85 
    86 lemma scaleR_left_commute:
    87   fixes x :: "'a::real_vector"
    88   shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)"
    89 by (simp add: mult_commute)
    90 
    91 interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
    92 by unfold_locales (rule scaleR_left_distrib)
    93 
    94 interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
    95 by unfold_locales (rule scaleR_right_distrib)
    96 
    97 lemmas scaleR_zero_left [simp] = scaleR_left.zero
    98 
    99 lemmas scaleR_zero_right [simp] = scaleR_right.zero
   100 
   101 lemmas scaleR_minus_left [simp] = scaleR_left.minus
   102 
   103 lemmas scaleR_minus_right [simp] = scaleR_right.minus
   104 
   105 lemmas scaleR_left_diff_distrib = scaleR_left.diff
   106 
   107 lemmas scaleR_right_diff_distrib = scaleR_right.diff
   108 
   109 lemma scaleR_eq_0_iff [simp]:
   110   fixes x :: "'a::real_vector"
   111   shows "(scaleR a x = 0) = (a = 0 \<or> x = 0)"
   112 proof cases
   113   assume "a = 0" thus ?thesis by simp
   114 next
   115   assume anz [simp]: "a \<noteq> 0"
   116   { assume "scaleR a x = 0"
   117     hence "scaleR (inverse a) (scaleR a x) = 0" by simp
   118     hence "x = 0" by simp }
   119   thus ?thesis by force
   120 qed
   121 
   122 lemma scaleR_left_imp_eq:
   123   fixes x y :: "'a::real_vector"
   124   shows "\<lbrakk>a \<noteq> 0; scaleR a x = scaleR a y\<rbrakk> \<Longrightarrow> x = y"
   125 proof -
   126   assume nonzero: "a \<noteq> 0"
   127   assume "scaleR a x = scaleR a y"
   128   hence "scaleR a (x - y) = 0"
   129      by (simp add: scaleR_right_diff_distrib)
   130   hence "x - y = 0" by (simp add: nonzero)
   131   thus "x = y" by simp
   132 qed
   133 
   134 lemma scaleR_right_imp_eq:
   135   fixes x y :: "'a::real_vector"
   136   shows "\<lbrakk>x \<noteq> 0; scaleR a x = scaleR b x\<rbrakk> \<Longrightarrow> a = b"
   137 proof -
   138   assume nonzero: "x \<noteq> 0"
   139   assume "scaleR a x = scaleR b x"
   140   hence "scaleR (a - b) x = 0"
   141      by (simp add: scaleR_left_diff_distrib)
   142   hence "a - b = 0" by (simp add: nonzero)
   143   thus "a = b" by simp
   144 qed
   145 
   146 lemma scaleR_cancel_left:
   147   fixes x y :: "'a::real_vector"
   148   shows "(scaleR a x = scaleR a y) = (x = y \<or> a = 0)"
   149 by (auto intro: scaleR_left_imp_eq)
   150 
   151 lemma scaleR_cancel_right:
   152   fixes x y :: "'a::real_vector"
   153   shows "(scaleR a x = scaleR b x) = (a = b \<or> x = 0)"
   154 by (auto intro: scaleR_right_imp_eq)
   155 
   156 lemma nonzero_inverse_scaleR_distrib:
   157   fixes x :: "'a::real_div_algebra" shows
   158   "\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
   159 by (rule inverse_unique, simp)
   160 
   161 lemma inverse_scaleR_distrib:
   162   fixes x :: "'a::{real_div_algebra,division_by_zero}"
   163   shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
   164 apply (case_tac "a = 0", simp)
   165 apply (case_tac "x = 0", simp)
   166 apply (erule (1) nonzero_inverse_scaleR_distrib)
   167 done
   168 
   169 
   170 subsection {* Embedding of the Reals into any @{text real_algebra_1}:
   171 @{term of_real} *}
   172 
   173 definition
   174   of_real :: "real \<Rightarrow> 'a::real_algebra_1" where
   175   "of_real r = scaleR r 1"
   176 
   177 lemma scaleR_conv_of_real: "scaleR r x = of_real r * x"
   178 by (simp add: of_real_def)
   179 
   180 lemma of_real_0 [simp]: "of_real 0 = 0"
   181 by (simp add: of_real_def)
   182 
   183 lemma of_real_1 [simp]: "of_real 1 = 1"
   184 by (simp add: of_real_def)
   185 
   186 lemma of_real_add [simp]: "of_real (x + y) = of_real x + of_real y"
   187 by (simp add: of_real_def scaleR_left_distrib)
   188 
   189 lemma of_real_minus [simp]: "of_real (- x) = - of_real x"
   190 by (simp add: of_real_def)
   191 
   192 lemma of_real_diff [simp]: "of_real (x - y) = of_real x - of_real y"
   193 by (simp add: of_real_def scaleR_left_diff_distrib)
   194 
   195 lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y"
   196 by (simp add: of_real_def mult_commute)
   197 
   198 lemma nonzero_of_real_inverse:
   199   "x \<noteq> 0 \<Longrightarrow> of_real (inverse x) =
   200    inverse (of_real x :: 'a::real_div_algebra)"
   201 by (simp add: of_real_def nonzero_inverse_scaleR_distrib)
   202 
   203 lemma of_real_inverse [simp]:
   204   "of_real (inverse x) =
   205    inverse (of_real x :: 'a::{real_div_algebra,division_by_zero})"
   206 by (simp add: of_real_def inverse_scaleR_distrib)
   207 
   208 lemma nonzero_of_real_divide:
   209   "y \<noteq> 0 \<Longrightarrow> of_real (x / y) =
   210    (of_real x / of_real y :: 'a::real_field)"
   211 by (simp add: divide_inverse nonzero_of_real_inverse)
   212 
   213 lemma of_real_divide [simp]:
   214   "of_real (x / y) =
   215    (of_real x / of_real y :: 'a::{real_field,division_by_zero})"
   216 by (simp add: divide_inverse)
   217 
   218 lemma of_real_power [simp]:
   219   "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n"
   220 by (induct n) (simp_all add: power_Suc)
   221 
   222 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
   223 by (simp add: of_real_def scaleR_cancel_right)
   224 
   225 lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
   226 
   227 lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
   228 proof
   229   fix r
   230   show "of_real r = id r"
   231     by (simp add: of_real_def)
   232 qed
   233 
   234 text{*Collapse nested embeddings*}
   235 lemma of_real_of_nat_eq [simp]: "of_real (of_nat n) = of_nat n"
   236 by (induct n) auto
   237 
   238 lemma of_real_of_int_eq [simp]: "of_real (of_int z) = of_int z"
   239 by (cases z rule: int_diff_cases, simp)
   240 
   241 lemma of_real_number_of_eq:
   242   "of_real (number_of w) = (number_of w :: 'a::{number_ring,real_algebra_1})"
   243 by (simp add: number_of_eq)
   244 
   245 text{*Every real algebra has characteristic zero*}
   246 instance real_algebra_1 < ring_char_0
   247 proof
   248   fix m n :: nat
   249   have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)"
   250     by (simp only: of_real_eq_iff of_nat_eq_iff)
   251   thus "(of_nat m = (of_nat n::'a)) = (m = n)"
   252     by (simp only: of_real_of_nat_eq)
   253 qed
   254 
   255 
   256 subsection {* The Set of Real Numbers *}
   257 
   258 definition
   259   Reals :: "'a::real_algebra_1 set" where
   260   "Reals \<equiv> range of_real"
   261 
   262 notation (xsymbols)
   263   Reals  ("\<real>")
   264 
   265 lemma Reals_of_real [simp]: "of_real r \<in> Reals"
   266 by (simp add: Reals_def)
   267 
   268 lemma Reals_of_int [simp]: "of_int z \<in> Reals"
   269 by (subst of_real_of_int_eq [symmetric], rule Reals_of_real)
   270 
   271 lemma Reals_of_nat [simp]: "of_nat n \<in> Reals"
   272 by (subst of_real_of_nat_eq [symmetric], rule Reals_of_real)
   273 
   274 lemma Reals_number_of [simp]:
   275   "(number_of w::'a::{number_ring,real_algebra_1}) \<in> Reals"
   276 by (subst of_real_number_of_eq [symmetric], rule Reals_of_real)
   277 
   278 lemma Reals_0 [simp]: "0 \<in> Reals"
   279 apply (unfold Reals_def)
   280 apply (rule range_eqI)
   281 apply (rule of_real_0 [symmetric])
   282 done
   283 
   284 lemma Reals_1 [simp]: "1 \<in> Reals"
   285 apply (unfold Reals_def)
   286 apply (rule range_eqI)
   287 apply (rule of_real_1 [symmetric])
   288 done
   289 
   290 lemma Reals_add [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a + b \<in> Reals"
   291 apply (auto simp add: Reals_def)
   292 apply (rule range_eqI)
   293 apply (rule of_real_add [symmetric])
   294 done
   295 
   296 lemma Reals_minus [simp]: "a \<in> Reals \<Longrightarrow> - a \<in> Reals"
   297 apply (auto simp add: Reals_def)
   298 apply (rule range_eqI)
   299 apply (rule of_real_minus [symmetric])
   300 done
   301 
   302 lemma Reals_diff [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a - b \<in> Reals"
   303 apply (auto simp add: Reals_def)
   304 apply (rule range_eqI)
   305 apply (rule of_real_diff [symmetric])
   306 done
   307 
   308 lemma Reals_mult [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a * b \<in> Reals"
   309 apply (auto simp add: Reals_def)
   310 apply (rule range_eqI)
   311 apply (rule of_real_mult [symmetric])
   312 done
   313 
   314 lemma nonzero_Reals_inverse:
   315   fixes a :: "'a::real_div_algebra"
   316   shows "\<lbrakk>a \<in> Reals; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Reals"
   317 apply (auto simp add: Reals_def)
   318 apply (rule range_eqI)
   319 apply (erule nonzero_of_real_inverse [symmetric])
   320 done
   321 
   322 lemma Reals_inverse [simp]:
   323   fixes a :: "'a::{real_div_algebra,division_by_zero}"
   324   shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
   325 apply (auto simp add: Reals_def)
   326 apply (rule range_eqI)
   327 apply (rule of_real_inverse [symmetric])
   328 done
   329 
   330 lemma nonzero_Reals_divide:
   331   fixes a b :: "'a::real_field"
   332   shows "\<lbrakk>a \<in> Reals; b \<in> Reals; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
   333 apply (auto simp add: Reals_def)
   334 apply (rule range_eqI)
   335 apply (erule nonzero_of_real_divide [symmetric])
   336 done
   337 
   338 lemma Reals_divide [simp]:
   339   fixes a b :: "'a::{real_field,division_by_zero}"
   340   shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
   341 apply (auto simp add: Reals_def)
   342 apply (rule range_eqI)
   343 apply (rule of_real_divide [symmetric])
   344 done
   345 
   346 lemma Reals_power [simp]:
   347   fixes a :: "'a::{real_algebra_1,recpower}"
   348   shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
   349 apply (auto simp add: Reals_def)
   350 apply (rule range_eqI)
   351 apply (rule of_real_power [symmetric])
   352 done
   353 
   354 lemma Reals_cases [cases set: Reals]:
   355   assumes "q \<in> \<real>"
   356   obtains (of_real) r where "q = of_real r"
   357   unfolding Reals_def
   358 proof -
   359   from `q \<in> \<real>` have "q \<in> range of_real" unfolding Reals_def .
   360   then obtain r where "q = of_real r" ..
   361   then show thesis ..
   362 qed
   363 
   364 lemma Reals_induct [case_names of_real, induct set: Reals]:
   365   "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q"
   366   by (rule Reals_cases) auto
   367 
   368 
   369 subsection {* Real normed vector spaces *}
   370 
   371 class norm = type +
   372   fixes norm :: "'a \<Rightarrow> real"
   373 
   374 instance real :: norm
   375   real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
   376 
   377 class sgn_div_norm = scaleR + norm + sgn +
   378   assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
   379 
   380 class real_normed_vector = real_vector + sgn_div_norm +
   381   assumes norm_ge_zero [simp]: "0 \<le> norm x"
   382   and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
   383   and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
   384   and norm_scaleR: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
   385 
   386 class real_normed_algebra = real_algebra + real_normed_vector +
   387   assumes norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
   388 
   389 class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
   390   assumes norm_one [simp]: "norm 1 = 1"
   391 
   392 class real_normed_div_algebra = real_div_algebra + real_normed_vector +
   393   assumes norm_mult: "norm (x * y) = norm x * norm y"
   394 
   395 class real_normed_field = real_field + real_normed_div_algebra
   396 
   397 instance real_normed_div_algebra < real_normed_algebra_1
   398 proof
   399   fix x y :: 'a
   400   show "norm (x * y) \<le> norm x * norm y"
   401     by (simp add: norm_mult)
   402 next
   403   have "norm (1 * 1::'a) = norm (1::'a) * norm (1::'a)"
   404     by (rule norm_mult)
   405   thus "norm (1::'a) = 1" by simp
   406 qed
   407 
   408 instance real :: real_normed_field
   409 apply (intro_classes, unfold real_norm_def real_scaleR_def)
   410 apply (simp add: real_sgn_def)
   411 apply (rule abs_ge_zero)
   412 apply (rule abs_eq_0)
   413 apply (rule abs_triangle_ineq)
   414 apply (rule abs_mult)
   415 apply (rule abs_mult)
   416 done
   417 
   418 lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0"
   419 by simp
   420 
   421 lemma zero_less_norm_iff [simp]:
   422   fixes x :: "'a::real_normed_vector"
   423   shows "(0 < norm x) = (x \<noteq> 0)"
   424 by (simp add: order_less_le)
   425 
   426 lemma norm_not_less_zero [simp]:
   427   fixes x :: "'a::real_normed_vector"
   428   shows "\<not> norm x < 0"
   429 by (simp add: linorder_not_less)
   430 
   431 lemma norm_le_zero_iff [simp]:
   432   fixes x :: "'a::real_normed_vector"
   433   shows "(norm x \<le> 0) = (x = 0)"
   434 by (simp add: order_le_less)
   435 
   436 lemma norm_minus_cancel [simp]:
   437   fixes x :: "'a::real_normed_vector"
   438   shows "norm (- x) = norm x"
   439 proof -
   440   have "norm (- x) = norm (scaleR (- 1) x)"
   441     by (simp only: scaleR_minus_left scaleR_one)
   442   also have "\<dots> = \<bar>- 1\<bar> * norm x"
   443     by (rule norm_scaleR)
   444   finally show ?thesis by simp
   445 qed
   446 
   447 lemma norm_minus_commute:
   448   fixes a b :: "'a::real_normed_vector"
   449   shows "norm (a - b) = norm (b - a)"
   450 proof -
   451   have "norm (- (b - a)) = norm (b - a)"
   452     by (rule norm_minus_cancel)
   453   thus ?thesis by simp
   454 qed
   455 
   456 lemma norm_triangle_ineq2:
   457   fixes a b :: "'a::real_normed_vector"
   458   shows "norm a - norm b \<le> norm (a - b)"
   459 proof -
   460   have "norm (a - b + b) \<le> norm (a - b) + norm b"
   461     by (rule norm_triangle_ineq)
   462   thus ?thesis by simp
   463 qed
   464 
   465 lemma norm_triangle_ineq3:
   466   fixes a b :: "'a::real_normed_vector"
   467   shows "\<bar>norm a - norm b\<bar> \<le> norm (a - b)"
   468 apply (subst abs_le_iff)
   469 apply auto
   470 apply (rule norm_triangle_ineq2)
   471 apply (subst norm_minus_commute)
   472 apply (rule norm_triangle_ineq2)
   473 done
   474 
   475 lemma norm_triangle_ineq4:
   476   fixes a b :: "'a::real_normed_vector"
   477   shows "norm (a - b) \<le> norm a + norm b"
   478 proof -
   479   have "norm (a + - b) \<le> norm a + norm (- b)"
   480     by (rule norm_triangle_ineq)
   481   thus ?thesis
   482     by (simp only: diff_minus norm_minus_cancel)
   483 qed
   484 
   485 lemma norm_diff_ineq:
   486   fixes a b :: "'a::real_normed_vector"
   487   shows "norm a - norm b \<le> norm (a + b)"
   488 proof -
   489   have "norm a - norm (- b) \<le> norm (a - - b)"
   490     by (rule norm_triangle_ineq2)
   491   thus ?thesis by simp
   492 qed
   493 
   494 lemma norm_diff_triangle_ineq:
   495   fixes a b c d :: "'a::real_normed_vector"
   496   shows "norm ((a + b) - (c + d)) \<le> norm (a - c) + norm (b - d)"
   497 proof -
   498   have "norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))"
   499     by (simp add: diff_minus add_ac)
   500   also have "\<dots> \<le> norm (a - c) + norm (b - d)"
   501     by (rule norm_triangle_ineq)
   502   finally show ?thesis .
   503 qed
   504 
   505 lemma abs_norm_cancel [simp]:
   506   fixes a :: "'a::real_normed_vector"
   507   shows "\<bar>norm a\<bar> = norm a"
   508 by (rule abs_of_nonneg [OF norm_ge_zero])
   509 
   510 lemma norm_add_less:
   511   fixes x y :: "'a::real_normed_vector"
   512   shows "\<lbrakk>norm x < r; norm y < s\<rbrakk> \<Longrightarrow> norm (x + y) < r + s"
   513 by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono])
   514 
   515 lemma norm_mult_less:
   516   fixes x y :: "'a::real_normed_algebra"
   517   shows "\<lbrakk>norm x < r; norm y < s\<rbrakk> \<Longrightarrow> norm (x * y) < r * s"
   518 apply (rule order_le_less_trans [OF norm_mult_ineq])
   519 apply (simp add: mult_strict_mono')
   520 done
   521 
   522 lemma norm_of_real [simp]:
   523   "norm (of_real r :: 'a::real_normed_algebra_1) = \<bar>r\<bar>"
   524 unfolding of_real_def by (simp add: norm_scaleR)
   525 
   526 lemma norm_number_of [simp]:
   527   "norm (number_of w::'a::{number_ring,real_normed_algebra_1})
   528     = \<bar>number_of w\<bar>"
   529 by (subst of_real_number_of_eq [symmetric], rule norm_of_real)
   530 
   531 lemma norm_of_int [simp]:
   532   "norm (of_int z::'a::real_normed_algebra_1) = \<bar>of_int z\<bar>"
   533 by (subst of_real_of_int_eq [symmetric], rule norm_of_real)
   534 
   535 lemma norm_of_nat [simp]:
   536   "norm (of_nat n::'a::real_normed_algebra_1) = of_nat n"
   537 apply (subst of_real_of_nat_eq [symmetric])
   538 apply (subst norm_of_real, simp)
   539 done
   540 
   541 lemma nonzero_norm_inverse:
   542   fixes a :: "'a::real_normed_div_algebra"
   543   shows "a \<noteq> 0 \<Longrightarrow> norm (inverse a) = inverse (norm a)"
   544 apply (rule inverse_unique [symmetric])
   545 apply (simp add: norm_mult [symmetric])
   546 done
   547 
   548 lemma norm_inverse:
   549   fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
   550   shows "norm (inverse a) = inverse (norm a)"
   551 apply (case_tac "a = 0", simp)
   552 apply (erule nonzero_norm_inverse)
   553 done
   554 
   555 lemma nonzero_norm_divide:
   556   fixes a b :: "'a::real_normed_field"
   557   shows "b \<noteq> 0 \<Longrightarrow> norm (a / b) = norm a / norm b"
   558 by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
   559 
   560 lemma norm_divide:
   561   fixes a b :: "'a::{real_normed_field,division_by_zero}"
   562   shows "norm (a / b) = norm a / norm b"
   563 by (simp add: divide_inverse norm_mult norm_inverse)
   564 
   565 lemma norm_power_ineq:
   566   fixes x :: "'a::{real_normed_algebra_1,recpower}"
   567   shows "norm (x ^ n) \<le> norm x ^ n"
   568 proof (induct n)
   569   case 0 show "norm (x ^ 0) \<le> norm x ^ 0" by simp
   570 next
   571   case (Suc n)
   572   have "norm (x * x ^ n) \<le> norm x * norm (x ^ n)"
   573     by (rule norm_mult_ineq)
   574   also from Suc have "\<dots> \<le> norm x * norm x ^ n"
   575     using norm_ge_zero by (rule mult_left_mono)
   576   finally show "norm (x ^ Suc n) \<le> norm x ^ Suc n"
   577     by (simp add: power_Suc)
   578 qed
   579 
   580 lemma norm_power:
   581   fixes x :: "'a::{real_normed_div_algebra,recpower}"
   582   shows "norm (x ^ n) = norm x ^ n"
   583 by (induct n) (simp_all add: power_Suc norm_mult)
   584 
   585 
   586 subsection {* Sign function *}
   587 
   588 lemma norm_sgn:
   589   "norm (sgn(x::'a::real_normed_vector)) = (if x = 0 then 0 else 1)"
   590 by (simp add: sgn_div_norm norm_scaleR)
   591 
   592 lemma sgn_zero [simp]: "sgn(0::'a::real_normed_vector) = 0"
   593 by (simp add: sgn_div_norm)
   594 
   595 lemma sgn_zero_iff: "(sgn(x::'a::real_normed_vector) = 0) = (x = 0)"
   596 by (simp add: sgn_div_norm)
   597 
   598 lemma sgn_minus: "sgn (- x) = - sgn(x::'a::real_normed_vector)"
   599 by (simp add: sgn_div_norm)
   600 
   601 lemma sgn_scaleR:
   602   "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))"
   603 by (simp add: sgn_div_norm norm_scaleR mult_ac)
   604 
   605 lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
   606 by (simp add: sgn_div_norm)
   607 
   608 lemma sgn_of_real:
   609   "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)"
   610 unfolding of_real_def by (simp only: sgn_scaleR sgn_one)
   611 
   612 lemma sgn_mult:
   613   fixes x y :: "'a::real_normed_div_algebra"
   614   shows "sgn (x * y) = sgn x * sgn y"
   615 by (simp add: sgn_div_norm norm_mult mult_commute)
   616 
   617 lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
   618 by (simp add: sgn_div_norm divide_inverse)
   619 
   620 lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
   621 unfolding real_sgn_eq by simp
   622 
   623 lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
   624 unfolding real_sgn_eq by simp
   625 
   626 
   627 subsection {* Bounded Linear and Bilinear Operators *}
   628 
   629 locale bounded_linear = additive +
   630   constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   631   assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
   632   assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
   633 
   634 lemma (in bounded_linear) pos_bounded:
   635   "\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K"
   636 proof -
   637   obtain K where K: "\<And>x. norm (f x) \<le> norm x * K"
   638     using bounded by fast
   639   show ?thesis
   640   proof (intro exI impI conjI allI)
   641     show "0 < max 1 K"
   642       by (rule order_less_le_trans [OF zero_less_one le_maxI1])
   643   next
   644     fix x
   645     have "norm (f x) \<le> norm x * K" using K .
   646     also have "\<dots> \<le> norm x * max 1 K"
   647       by (rule mult_left_mono [OF le_maxI2 norm_ge_zero])
   648     finally show "norm (f x) \<le> norm x * max 1 K" .
   649   qed
   650 qed
   651 
   652 lemma (in bounded_linear) nonneg_bounded:
   653   "\<exists>K\<ge>0. \<forall>x. norm (f x) \<le> norm x * K"
   654 proof -
   655   from pos_bounded
   656   show ?thesis by (auto intro: order_less_imp_le)
   657 qed
   658 
   659 locale bounded_bilinear =
   660   fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
   661                  \<Rightarrow> 'c::real_normed_vector"
   662     (infixl "**" 70)
   663   assumes add_left: "prod (a + a') b = prod a b + prod a' b"
   664   assumes add_right: "prod a (b + b') = prod a b + prod a b'"
   665   assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)"
   666   assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)"
   667   assumes bounded: "\<exists>K. \<forall>a b. norm (prod a b) \<le> norm a * norm b * K"
   668 
   669 lemma (in bounded_bilinear) pos_bounded:
   670   "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
   671 apply (cut_tac bounded, erule exE)
   672 apply (rule_tac x="max 1 K" in exI, safe)
   673 apply (rule order_less_le_trans [OF zero_less_one le_maxI1])
   674 apply (drule spec, drule spec, erule order_trans)
   675 apply (rule mult_left_mono [OF le_maxI2])
   676 apply (intro mult_nonneg_nonneg norm_ge_zero)
   677 done
   678 
   679 lemma (in bounded_bilinear) nonneg_bounded:
   680   "\<exists>K\<ge>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
   681 proof -
   682   from pos_bounded
   683   show ?thesis by (auto intro: order_less_imp_le)
   684 qed
   685 
   686 lemma (in bounded_bilinear) additive_right: "additive (\<lambda>b. prod a b)"
   687 by (rule additive.intro, rule add_right)
   688 
   689 lemma (in bounded_bilinear) additive_left: "additive (\<lambda>a. prod a b)"
   690 by (rule additive.intro, rule add_left)
   691 
   692 lemma (in bounded_bilinear) zero_left: "prod 0 b = 0"
   693 by (rule additive.zero [OF additive_left])
   694 
   695 lemma (in bounded_bilinear) zero_right: "prod a 0 = 0"
   696 by (rule additive.zero [OF additive_right])
   697 
   698 lemma (in bounded_bilinear) minus_left: "prod (- a) b = - prod a b"
   699 by (rule additive.minus [OF additive_left])
   700 
   701 lemma (in bounded_bilinear) minus_right: "prod a (- b) = - prod a b"
   702 by (rule additive.minus [OF additive_right])
   703 
   704 lemma (in bounded_bilinear) diff_left:
   705   "prod (a - a') b = prod a b - prod a' b"
   706 by (rule additive.diff [OF additive_left])
   707 
   708 lemma (in bounded_bilinear) diff_right:
   709   "prod a (b - b') = prod a b - prod a b'"
   710 by (rule additive.diff [OF additive_right])
   711 
   712 lemma (in bounded_bilinear) bounded_linear_left:
   713   "bounded_linear (\<lambda>a. a ** b)"
   714 apply (unfold_locales)
   715 apply (rule add_left)
   716 apply (rule scaleR_left)
   717 apply (cut_tac bounded, safe)
   718 apply (rule_tac x="norm b * K" in exI)
   719 apply (simp add: mult_ac)
   720 done
   721 
   722 lemma (in bounded_bilinear) bounded_linear_right:
   723   "bounded_linear (\<lambda>b. a ** b)"
   724 apply (unfold_locales)
   725 apply (rule add_right)
   726 apply (rule scaleR_right)
   727 apply (cut_tac bounded, safe)
   728 apply (rule_tac x="norm a * K" in exI)
   729 apply (simp add: mult_ac)
   730 done
   731 
   732 lemma (in bounded_bilinear) prod_diff_prod:
   733   "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
   734 by (simp add: diff_left diff_right)
   735 
   736 interpretation mult:
   737   bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
   738 apply (rule bounded_bilinear.intro)
   739 apply (rule left_distrib)
   740 apply (rule right_distrib)
   741 apply (rule mult_scaleR_left)
   742 apply (rule mult_scaleR_right)
   743 apply (rule_tac x="1" in exI)
   744 apply (simp add: norm_mult_ineq)
   745 done
   746 
   747 interpretation mult_left:
   748   bounded_linear ["(\<lambda>x::'a::real_normed_algebra. x * y)"]
   749 by (rule mult.bounded_linear_left)
   750 
   751 interpretation mult_right:
   752   bounded_linear ["(\<lambda>y::'a::real_normed_algebra. x * y)"]
   753 by (rule mult.bounded_linear_right)
   754 
   755 interpretation divide:
   756   bounded_linear ["(\<lambda>x::'a::real_normed_field. x / y)"]
   757 unfolding divide_inverse by (rule mult.bounded_linear_left)
   758 
   759 interpretation scaleR: bounded_bilinear ["scaleR"]
   760 apply (rule bounded_bilinear.intro)
   761 apply (rule scaleR_left_distrib)
   762 apply (rule scaleR_right_distrib)
   763 apply simp
   764 apply (rule scaleR_left_commute)
   765 apply (rule_tac x="1" in exI)
   766 apply (simp add: norm_scaleR)
   767 done
   768 
   769 interpretation scaleR_left: bounded_linear ["\<lambda>r. scaleR r x"]
   770 by (rule scaleR.bounded_linear_left)
   771 
   772 interpretation scaleR_right: bounded_linear ["\<lambda>x. scaleR r x"]
   773 by (rule scaleR.bounded_linear_right)
   774 
   775 interpretation of_real: bounded_linear ["\<lambda>r. of_real r"]
   776 unfolding of_real_def by (rule scaleR.bounded_linear_left)
   777 
   778 end