summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Sun, 22 Feb 2009 10:53:10 -0800 | |

changeset 30067 | 84205156ca8a |

parent 30066 | 9223483cc927 |

child 30068 | eb9bdc4292be |

simplify some proofs

--- a/src/HOL/Library/Inner_Product.thy Sun Feb 22 08:52:44 2009 -0800 +++ b/src/HOL/Library/Inner_Product.thy Sun Feb 22 10:53:10 2009 -0800 @@ -21,19 +21,10 @@ begin lemma inner_zero_left [simp]: "inner 0 x = 0" -proof - - have "inner 0 x = inner (0 + 0) x" by simp - also have "\<dots> = inner 0 x + inner 0 x" by (rule inner_left_distrib) - finally show "inner 0 x = 0" by simp -qed + using inner_left_distrib [of 0 0 x] by simp lemma inner_minus_left [simp]: "inner (- x) y = - inner x y" -proof - - have "inner (- x) y + inner x y = inner (- x + x) y" - by (rule inner_left_distrib [symmetric]) - also have "\<dots> = - inner x y + inner x y" by simp - finally show "inner (- x) y = - inner x y" by simp -qed + using inner_left_distrib [of x "- x" y] by simp lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z" by (simp add: diff_minus inner_left_distrib)