src/HOL/Complex/Complex.thy
changeset 15085 5693a977a767
parent 15013 34264f5e4691
child 15131 c69542757a4d
equal deleted inserted replaced
15084:07f7b158ef32 15085:5693a977a767
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     6 *)
     6 *)
     7 
     7 
     8 header {* Complex Numbers: Rectangular and Polar Representations *}
     8 header {* Complex Numbers: Rectangular and Polar Representations *}
     9 
     9 
    10 theory Complex = HLog:
    10 theory Complex = "../Hyperreal/HLog":
    11 
    11 
    12 datatype complex = Complex real real
    12 datatype complex = Complex real real
    13 
    13 
    14 instance complex :: "{zero, one, plus, times, minus, inverse, power}" ..
    14 instance complex :: "{zero, one, plus, times, minus, inverse, power}" ..
    15 
    15 
   438 
   438 
   439 subsection{*Modulus*}
   439 subsection{*Modulus*}
   440 
   440 
   441 lemma complex_mod_eq_zero_cancel [simp]: "(cmod x = 0) = (x = 0)"
   441 lemma complex_mod_eq_zero_cancel [simp]: "(cmod x = 0) = (x = 0)"
   442 apply (induct x)
   442 apply (induct x)
   443 apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2
   443 apply (auto iff: real_0_le_add_iff 
       
   444             intro: real_sum_squares_cancel real_sum_squares_cancel2
   444             simp add: complex_mod complex_zero_def power2_eq_square)
   445             simp add: complex_mod complex_zero_def power2_eq_square)
   445 done
   446 done
   446 
   447 
   447 lemma complex_mod_complex_of_real_of_nat [simp]:
   448 lemma complex_mod_complex_of_real_of_nat [simp]:
   448      "cmod (complex_of_real(real (n::nat))) = real n"
   449      "cmod (complex_of_real(real (n::nat))) = real n"
   451 lemma complex_mod_minus [simp]: "cmod (-x) = cmod(x)"
   452 lemma complex_mod_minus [simp]: "cmod (-x) = cmod(x)"
   452 by (induct x, simp add: complex_mod complex_minus power2_eq_square)
   453 by (induct x, simp add: complex_mod complex_minus power2_eq_square)
   453 
   454 
   454 lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
   455 lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
   455 apply (induct z, simp add: complex_mod complex_cnj complex_mult)
   456 apply (induct z, simp add: complex_mod complex_cnj complex_mult)
   456 apply (simp add: power2_eq_square abs_if linorder_not_less)
   457 apply (simp add: power2_eq_square abs_if linorder_not_less real_0_le_add_iff)
   457 done
   458 done
   458 
   459 
   459 lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2"
   460 lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2"
   460 by (simp add: cmod_def)
   461 by (simp add: cmod_def)
   461 
   462 
   508 by (rule order_trans [OF _ complex_mod_ge_zero], simp)
   509 by (rule order_trans [OF _ complex_mod_ge_zero], simp)
   509 
   510 
   510 lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \<le> cmod(x) + cmod(y)"
   511 lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \<le> cmod(x) + cmod(y)"
   511 apply (rule_tac n = 1 in realpow_increasing)
   512 apply (rule_tac n = 1 in realpow_increasing)
   512 apply (auto intro:  order_trans [OF _ complex_mod_ge_zero]
   513 apply (auto intro:  order_trans [OF _ complex_mod_ge_zero]
   513             simp add: power2_eq_square [symmetric])
   514             simp add: add_increasing power2_eq_square [symmetric])
   514 done
   515 done
   515 
   516 
   516 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
   517 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
   517 by (insert complex_mod_triangle_ineq [THEN add_right_mono, of b a"-cmod b"], simp)
   518 by (insert complex_mod_triangle_ineq [THEN add_right_mono, of b a"-cmod b"], simp)
   518 
   519