equal
deleted
inserted
replaced
279 "sgn x = x /\<^sub>R cmod x" |
279 "sgn x = x /\<^sub>R cmod x" |
280 |
280 |
281 definition dist_complex_def: |
281 definition dist_complex_def: |
282 "dist x y = cmod (x - y)" |
282 "dist x y = cmod (x - y)" |
283 |
283 |
284 definition open_complex_def: |
284 definition topo_complex_def: |
285 "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::complex. dist y x < e \<longrightarrow> y \<in> S)" |
285 "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}" |
286 |
286 |
287 lemmas cmod_def = complex_norm_def |
287 lemmas cmod_def = complex_norm_def |
288 |
288 |
289 lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)" |
289 lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)" |
290 by (simp add: complex_norm_def) |
290 by (simp add: complex_norm_def) |
291 |
291 |
292 instance proof |
292 instance proof |
293 fix r :: real and x y :: complex and S :: "complex set" |
293 fix r :: real and x y :: complex |
294 show "0 \<le> norm x" |
294 show "0 \<le> norm x" |
295 by (induct x) simp |
295 by (induct x) simp |
296 show "(norm x = 0) = (x = 0)" |
296 show "(norm x = 0) = (x = 0)" |
297 by (induct x) simp |
297 by (induct x) simp |
298 show "norm (x + y) \<le> norm x + norm y" |
298 show "norm (x + y) \<le> norm x + norm y" |
306 (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps) |
306 (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps) |
307 show "sgn x = x /\<^sub>R cmod x" |
307 show "sgn x = x /\<^sub>R cmod x" |
308 by (rule complex_sgn_def) |
308 by (rule complex_sgn_def) |
309 show "dist x y = cmod (x - y)" |
309 show "dist x y = cmod (x - y)" |
310 by (rule dist_complex_def) |
310 by (rule dist_complex_def) |
311 show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" |
311 show "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}" |
312 by (rule open_complex_def) |
312 by (rule topo_complex_def) |
313 qed |
313 qed |
314 |
314 |
315 end |
315 end |
316 |
316 |
317 lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1" |
317 lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1" |