equal
deleted
inserted
replaced
102 fixes x :: "'a::real_normed_vector" shows |
102 fixes x :: "'a::real_normed_vector" shows |
103 "x = y \<longleftrightarrow> norm (x - y) \<le> 0" |
103 "x = y \<longleftrightarrow> norm (x - y) \<le> 0" |
104 "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)" |
104 "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)" |
105 using norm_ge_zero[of "x - y"] by auto |
105 using norm_ge_zero[of "x - y"] by auto |
106 |
106 |
|
107 lemmas arithmetic_simps = |
|
108 arith_simps |
|
109 add_numeral_special |
|
110 add_neg_numeral_special |
|
111 add_0_left |
|
112 add_0_right |
|
113 mult_zero_left |
|
114 mult_zero_right |
|
115 mult_1_left |
|
116 mult_1_right |
|
117 |
107 use "normarith.ML" |
118 use "normarith.ML" |
108 |
119 |
109 method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) |
120 method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) |
110 *} "prove simple linear statements about vector norms" |
121 *} "prove simple linear statements about vector norms" |
111 |
122 |