introduced classes
authorhaftmann
Sat Sep 15 19:27:43 2007 +0200 (2007-09-15)
changeset 24588ed9a1254d674
parent 24587 4f2cbf6e563f
child 24589 d3fca349736c
introduced classes
src/HOL/Real/RealVector.thy
     1.1 --- a/src/HOL/Real/RealVector.thy	Sat Sep 15 19:27:42 2007 +0200
     1.2 +++ b/src/HOL/Real/RealVector.thy	Sat Sep 15 19:27:43 2007 +0200
     1.3 @@ -60,21 +60,21 @@
     1.4  instance real :: scaleR
     1.5    real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
     1.6  
     1.7 -axclass real_vector < scaleR, ab_group_add
     1.8 -  scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
     1.9 -  scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
    1.10 -  scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
    1.11 -  scaleR_one [simp]: "scaleR 1 x = x"
    1.12 +class real_vector = scaleR + ab_group_add +
    1.13 +  assumes scaleR_right_distrib: "scaleR a (x \<^loc>+ y) = scaleR a x \<^loc>+ scaleR a y"
    1.14 +  and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x \<^loc>+ scaleR b x"
    1.15 +  and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
    1.16 +  and scaleR_one [simp]: "scaleR 1 x = x"
    1.17  
    1.18 -axclass real_algebra < real_vector, ring
    1.19 -  mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
    1.20 -  mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
    1.21 +class real_algebra = real_vector + ring +
    1.22 +  assumes mult_scaleR_left [simp]: "scaleR a x \<^loc>* y = scaleR a (x \<^loc>* y)"
    1.23 +  and mult_scaleR_right [simp]: "x \<^loc>* scaleR a y = scaleR a (x \<^loc>* y)"
    1.24  
    1.25 -axclass real_algebra_1 < real_algebra, ring_1
    1.26 +class real_algebra_1 = real_algebra + ring_1
    1.27  
    1.28 -axclass real_div_algebra < real_algebra_1, division_ring
    1.29 +class real_div_algebra = real_algebra_1 + division_ring
    1.30  
    1.31 -axclass real_field < real_div_algebra, field
    1.32 +class real_field = real_div_algebra + field
    1.33  
    1.34  instance real :: real_field
    1.35  apply (intro_classes, unfold real_scaleR_def)
    1.36 @@ -380,22 +380,22 @@
    1.37  class sgn_div_norm = scaleR + norm + sgn +
    1.38    assumes sgn_div_norm: "sgn x = x /# norm x"
    1.39  
    1.40 -axclass real_normed_vector < real_vector, sgn_div_norm
    1.41 -  norm_ge_zero [simp]: "0 \<le> norm x"
    1.42 -  norm_eq_zero [simp]: "(norm x = 0) = (x = 0)"
    1.43 -  norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
    1.44 -  norm_scaleR: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
    1.45 +class real_normed_vector = real_vector + sgn_div_norm +
    1.46 +  assumes norm_ge_zero [simp]: "0 \<le> norm x"
    1.47 +  and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = \<^loc>0"
    1.48 +  and norm_triangle_ineq: "norm (x \<^loc>+ y) \<le> norm x + norm y"
    1.49 +  and norm_scaleR: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
    1.50  
    1.51 -axclass real_normed_algebra < real_algebra, real_normed_vector
    1.52 -  norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
    1.53 +class real_normed_algebra = real_algebra + real_normed_vector +
    1.54 +  assumes norm_mult_ineq: "norm (x \<^loc>* y) \<le> norm x * norm y"
    1.55  
    1.56 -axclass real_normed_algebra_1 < real_algebra_1, real_normed_algebra
    1.57 -  norm_one [simp]: "norm 1 = 1"
    1.58 +class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
    1.59 +  assumes norm_one [simp]: "norm \<^loc>1 = 1"
    1.60  
    1.61 -axclass real_normed_div_algebra < real_div_algebra, real_normed_vector
    1.62 -  norm_mult: "norm (x * y) = norm x * norm y"
    1.63 +class real_normed_div_algebra = real_div_algebra + real_normed_vector +
    1.64 +  assumes norm_mult: "norm (x \<^loc>* y) = norm x * norm y"
    1.65  
    1.66 -axclass real_normed_field < real_field, real_normed_div_algebra
    1.67 +class real_normed_field = real_field + real_normed_div_algebra
    1.68  
    1.69  instance real_normed_div_algebra < real_normed_algebra_1
    1.70  proof