src/HOL/Complex.thy
changeset 31292 d24b2692562f
parent 31021 53642251a04f
child 31413 729d90a531e4
equal deleted inserted replaced
31291:a2f737a72655 31292:d24b2692562f
   276   "cmod \<equiv> norm"
   276   "cmod \<equiv> norm"
   277 
   277 
   278 definition
   278 definition
   279   complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
   279   complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
   280 
   280 
       
   281 definition
       
   282   dist_complex_def: "dist x y = cmod (x - y)"
       
   283 
   281 lemmas cmod_def = complex_norm_def
   284 lemmas cmod_def = complex_norm_def
   282 
   285 
   283 lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
   286 lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
   284   by (simp add: complex_norm_def)
   287   by (simp add: complex_norm_def)
   285 
   288 
   297     by (induct x)
   300     by (induct x)
   298        (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
   301        (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
   299   show "norm (x * y) = norm x * norm y"
   302   show "norm (x * y) = norm x * norm y"
   300     by (induct x, induct y)
   303     by (induct x, induct y)
   301        (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
   304        (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
   302   show "sgn x = x /\<^sub>R cmod x" by(simp add: complex_sgn_def)
   305   show "sgn x = x /\<^sub>R cmod x"
       
   306     by (rule complex_sgn_def)
       
   307   show "dist x y = cmod (x - y)"
       
   308     by (rule dist_complex_def)
   303 qed
   309 qed
   304 
   310 
   305 end
   311 end
   306 
   312 
   307 lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
   313 lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"