src/HOL/Library/Inner_Product.thy
changeset 30067 84205156ca8a
parent 30046 49f603f92c47
child 30663 0b6aff7451b2
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Sun Feb 22 08:52:44 2009 -0800
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Sun Feb 22 10:53:10 2009 -0800
     1.3 @@ -21,19 +21,10 @@
     1.4  begin
     1.5  
     1.6  lemma inner_zero_left [simp]: "inner 0 x = 0"
     1.7 -proof -
     1.8 -  have "inner 0 x = inner (0 + 0) x" by simp
     1.9 -  also have "\<dots> = inner 0 x + inner 0 x" by (rule inner_left_distrib)
    1.10 -  finally show "inner 0 x = 0" by simp
    1.11 -qed
    1.12 +  using inner_left_distrib [of 0 0 x] by simp
    1.13  
    1.14  lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
    1.15 -proof -
    1.16 -  have "inner (- x) y + inner x y = inner (- x + x) y"
    1.17 -    by (rule inner_left_distrib [symmetric])
    1.18 -  also have "\<dots> = - inner x y + inner x y" by simp
    1.19 -  finally show "inner (- x) y = - inner x y" by simp
    1.20 -qed
    1.21 +  using inner_left_distrib [of x "- x" y] by simp
    1.22  
    1.23  lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    1.24    by (simp add: diff_minus inner_left_distrib)