# HG changeset patch
# User huffman
# Date 1165964573 -3600
# Node ID 4b93e949ac33d717242881de387bb729047d249a
# Parent  be0a6e6905d9f741640d02afa11f7ea655f7b632
remove uses of scaleR infix syntax; add lemma Reals_number_of

diff -r be0a6e6905d9 -r 4b93e949ac33 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Tue Dec 12 21:25:14 2006 +0100
+++ b/src/HOL/Real/RealVector.thy	Wed Dec 13 00:02:53 2006 +0100
@@ -42,7 +42,7 @@
 
 abbreviation
   divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a::scaleR" (infixl "'/#" 70) where
-  "x /# r == inverse r *# x"
+  "x /# r == scaleR (inverse r) x"
 
 notation (xsymbols)
   scaleR (infixr "*\<^sub>R" 75) and
@@ -51,17 +51,17 @@
 instance real :: scaleR ..
 
 defs (overloaded)
-  real_scaleR_def: "a *# x \<equiv> a * x"
+  real_scaleR_def: "scaleR a x \<equiv> a * x"
 
 axclass real_vector < scaleR, ab_group_add
-  scaleR_right_distrib: "a *# (x + y) = a *# x + a *# y"
-  scaleR_left_distrib: "(a + b) *# x = a *# x + b *# x"
-  scaleR_scaleR [simp]: "a *# b *# x = (a * b) *# x"
-  scaleR_one [simp]: "1 *# x = x"
+  scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
+  scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
+  scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
+  scaleR_one [simp]: "scaleR 1 x = x"
 
 axclass real_algebra < real_vector, ring
-  mult_scaleR_left [simp]: "a *# x * y = a *# (x * y)"
-  mult_scaleR_right [simp]: "x * a *# y = a *# (x * y)"
+  mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
+  mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
 
 axclass real_algebra_1 < real_algebra, ring_1
 
@@ -81,13 +81,13 @@
 
 lemma scaleR_left_commute:
   fixes x :: "'a::real_vector"
-  shows "a *# b *# x = b *# a *# x"
+  shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)"
 by (simp add: mult_commute)
 
-lemma additive_scaleR_right: "additive (\<lambda>x. a *# x :: 'a::real_vector)"
+lemma additive_scaleR_right: "additive (\<lambda>x. scaleR a x::'a::real_vector)"
 by (rule additive.intro, rule scaleR_right_distrib)
 
-lemma additive_scaleR_left: "additive (\<lambda>a. a *# x :: 'a::real_vector)"
+lemma additive_scaleR_left: "additive (\<lambda>a. scaleR a x::'a::real_vector)"
 by (rule additive.intro, rule scaleR_left_distrib)
 
 lemmas scaleR_zero_left [simp] =
@@ -110,24 +110,24 @@
 
 lemma scaleR_eq_0_iff:
   fixes x :: "'a::real_vector"
-  shows "(a *# x = 0) = (a = 0 \<or> x = 0)"
+  shows "(scaleR a x = 0) = (a = 0 \<or> x = 0)"
 proof cases
   assume "a = 0" thus ?thesis by simp
 next
   assume anz [simp]: "a \<noteq> 0"
-  { assume "a *# x = 0"
-    hence "inverse a *# a *# x = 0" by simp
+  { assume "scaleR a x = 0"
+    hence "scaleR (inverse a) (scaleR a x) = 0" by simp
     hence "x = 0" by simp }
   thus ?thesis by force
 qed
 
 lemma scaleR_left_imp_eq:
   fixes x y :: "'a::real_vector"
-  shows "\<lbrakk>a \<noteq> 0; a *# x = a *# y\<rbrakk> \<Longrightarrow> x = y"
+  shows "\<lbrakk>a \<noteq> 0; scaleR a x = scaleR a y\<rbrakk> \<Longrightarrow> x = y"
 proof -
   assume nonzero: "a \<noteq> 0"
-  assume "a *# x = a *# y"
-  hence "a *# (x - y) = 0"
+  assume "scaleR a x = scaleR a y"
+  hence "scaleR a (x - y) = 0"
      by (simp add: scaleR_right_diff_distrib)
   hence "x - y = 0"
      by (simp add: scaleR_eq_0_iff nonzero)
@@ -136,11 +136,11 @@
 
 lemma scaleR_right_imp_eq:
   fixes x y :: "'a::real_vector"
-  shows "\<lbrakk>x \<noteq> 0; a *# x = b *# x\<rbrakk> \<Longrightarrow> a = b"
+  shows "\<lbrakk>x \<noteq> 0; scaleR a x = scaleR b x\<rbrakk> \<Longrightarrow> a = b"
 proof -
   assume nonzero: "x \<noteq> 0"
-  assume "a *# x = b *# x"
-  hence "(a - b) *# x = 0"
+  assume "scaleR a x = scaleR b x"
+  hence "scaleR (a - b) x = 0"
      by (simp add: scaleR_left_diff_distrib)
   hence "a - b = 0"
      by (simp add: scaleR_eq_0_iff nonzero)
@@ -149,22 +149,22 @@
 
 lemma scaleR_cancel_left:
   fixes x y :: "'a::real_vector"
-  shows "(a *# x = a *# y) = (x = y \<or> a = 0)"
+  shows "(scaleR a x = scaleR a y) = (x = y \<or> a = 0)"
 by (auto intro: scaleR_left_imp_eq)
 
 lemma scaleR_cancel_right:
   fixes x y :: "'a::real_vector"
-  shows "(a *# x = b *# x) = (a = b \<or> x = 0)"
+  shows "(scaleR a x = scaleR b x) = (a = b \<or> x = 0)"
 by (auto intro: scaleR_right_imp_eq)
 
 lemma nonzero_inverse_scaleR_distrib:
-  fixes x :: "'a::real_div_algebra"
-  shows "\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (a *# x) = inverse a *# inverse x"
+  fixes x :: "'a::real_div_algebra" shows
+  "\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
 by (rule inverse_unique, simp)
 
 lemma inverse_scaleR_distrib:
   fixes x :: "'a::{real_div_algebra,division_by_zero}"
-  shows "inverse (a *# x) = inverse a *# inverse x"
+  shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
 apply (case_tac "a = 0", simp)
 apply (case_tac "x = 0", simp)
 apply (erule (1) nonzero_inverse_scaleR_distrib)
@@ -176,9 +176,9 @@
 
 definition
   of_real :: "real \<Rightarrow> 'a::real_algebra_1" where
-  "of_real r = r *# 1"
+  "of_real r = scaleR r 1"
 
-lemma scaleR_conv_of_real: "r *# x = of_real r * x"
+lemma scaleR_conv_of_real: "scaleR r x = of_real r * x"
 by (simp add: of_real_def)
 
 lemma of_real_0 [simp]: "of_real 0 = 0"
@@ -256,14 +256,18 @@
 notation (xsymbols)
   Reals  ("\<real>")
 
-lemma of_real_in_Reals [simp]: "of_real r \<in> Reals"
+lemma Reals_of_real [simp]: "of_real r \<in> Reals"
 by (simp add: Reals_def)
 
-lemma of_int_in_Reals [simp]: "of_int z \<in> Reals"
-by (subst of_real_of_int_eq [symmetric], rule of_real_in_Reals)
+lemma Reals_of_int [simp]: "of_int z \<in> Reals"
+by (subst of_real_of_int_eq [symmetric], rule Reals_of_real)
 
-lemma of_nat_in_Reals [simp]: "of_nat n \<in> Reals"
-by (subst of_real_of_nat_eq [symmetric], rule of_real_in_Reals)
+lemma Reals_of_nat [simp]: "of_nat n \<in> Reals"
+by (subst of_real_of_nat_eq [symmetric], rule Reals_of_real)
+
+lemma Reals_number_of [simp]:
+  "(number_of w::'a::{number_ring,real_algebra_1}) \<in> Reals"
+by (subst of_real_number_of_eq [symmetric], rule Reals_of_real)
 
 lemma Reals_0 [simp]: "0 \<in> Reals"
 apply (unfold Reals_def)
@@ -372,7 +376,7 @@
   norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
 
 axclass real_normed_vector < real_vector, normed
-  norm_scaleR: "norm (a *# x) = \<bar>a\<bar> * norm x"
+  norm_scaleR: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
 
 axclass real_normed_algebra < real_algebra, real_normed_vector
   norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
@@ -386,11 +390,11 @@
 instance real_normed_div_algebra < real_normed_algebra
 proof
   fix a :: real and x :: 'a
-  have "norm (a *# x) = norm (of_real a * x)"
-    by (simp add: of_real_def mult_scaleR_left)
+  have "norm (scaleR a x) = norm (of_real a * x)"
+    by (simp add: of_real_def)
   also have "\<dots> = abs a * norm x"
     by (simp add: norm_mult norm_of_real)
-  finally show "norm (a *# x) = abs a * norm x" .
+  finally show "norm (scaleR a x) = abs a * norm x" .
 next
   fix x y :: 'a
   show "norm (x * y) \<le> norm x * norm y"
@@ -422,7 +426,7 @@
   fixes x :: "'a::real_normed_vector"
   shows "norm (- x) = norm x"
 proof -
-  have "norm (- x) = norm (- 1 *# x)"
+  have "norm (- x) = norm (scaleR (- 1) x)"
     by (simp only: scaleR_minus_left scaleR_one)
   also have "\<dots> = \<bar>- 1\<bar> * norm x"
     by (rule norm_scaleR)