src/HOL/Real/RealVector.thy
changeset 25571 c9e39eafc7a0
parent 25062 af5ef0d4d655
child 27435 b3f8e9bdf9a7
equal deleted inserted replaced
25570:fdfbbb92dadf 25571:c9e39eafc7a0
    52 where
    52 where
    53   "x /\<^sub>R r == scaleR (inverse r) x"
    53   "x /\<^sub>R r == scaleR (inverse r) x"
    54 
    54 
    55 end
    55 end
    56 
    56 
    57 instance real :: scaleR
    57 instantiation real :: scaleR
    58   real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
    58 begin
       
    59 
       
    60 definition
       
    61   real_scaleR_def [simp]: "scaleR a x = a * x"
       
    62 
       
    63 instance ..
       
    64 
       
    65 end
    59 
    66 
    60 class real_vector = scaleR + ab_group_add +
    67 class real_vector = scaleR + ab_group_add +
    61   assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
    68   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"
    69   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"
    70   and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
   369 subsection {* Real normed vector spaces *}
   376 subsection {* Real normed vector spaces *}
   370 
   377 
   371 class norm = type +
   378 class norm = type +
   372   fixes norm :: "'a \<Rightarrow> real"
   379   fixes norm :: "'a \<Rightarrow> real"
   373 
   380 
   374 instance real :: norm
   381 instantiation real :: norm
   375   real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
   382 begin
       
   383 
       
   384 definition
       
   385   real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
       
   386 
       
   387 instance ..
       
   388 
       
   389 end
   376 
   390 
   377 class sgn_div_norm = scaleR + norm + sgn +
   391 class sgn_div_norm = scaleR + norm + sgn +
   378   assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
   392   assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
   379 
   393 
   380 class real_normed_vector = real_vector + sgn_div_norm +
   394 class real_normed_vector = real_vector + sgn_div_norm +