src/HOL/Complex/Complex.thy
 changeset 15085 5693a977a767 parent 15013 34264f5e4691 child 15131 c69542757a4d
equal 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 `