equal
deleted
inserted
replaced
762 apply (subgoal_tac "0 < u") |
762 apply (subgoal_tac "0 < u") |
763 prefer 2 apply arith |
763 prefer 2 apply arith |
764 apply (subgoal_tac "0 < v") |
764 apply (subgoal_tac "0 < v") |
765 prefer 2 apply arith |
765 prefer 2 apply arith |
766 apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v") |
766 apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v") |
767 apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) |
|
768 apply (simp add: power2_eq_square) |
767 apply (simp add: power2_eq_square) |
|
768 ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *) |
|
769 apply (rule_tac lemma_sqrt_hcomplex_capprox, auto) |
|
770 ML {* fast_arith_split_limit := 9; *} (* FIXME *) |
769 done |
771 done |
770 |
772 |
771 lemma CFinite_HFinite_iff: |
773 lemma CFinite_HFinite_iff: |
772 "(star_n X \<in> CFinite) = |
774 "(star_n X \<in> CFinite) = |
773 (star_n (%n. Re(X n)) \<in> HFinite & |
775 (star_n (%n. Re(X n)) \<in> HFinite & |