643 |
625 |
644 lemma hcis: "hcis (star_n X) = star_n (%n. cis (X n))" |
626 lemma hcis: "hcis (star_n X) = star_n (%n. cis (X n))" |
645 by (simp add: hcis_def starfun) |
627 by (simp add: hcis_def starfun) |
646 |
628 |
647 lemma hcis_eq: |
629 lemma hcis_eq: |
648 "hcis a = |
630 "!!a. hcis a = |
649 (hcomplex_of_hypreal(( *f* cos) a) + |
631 (hcomplex_of_hypreal(( *f* cos) a) + |
650 iii * hcomplex_of_hypreal(( *f* sin) a))" |
632 iii * hcomplex_of_hypreal(( *f* sin) a))" |
651 apply (cases a) |
633 by (transfer, simp add: cis_def) |
652 apply (simp add: starfun hcis hcomplex_of_hypreal iii_def star_of_def star_n_mult star_n_add cis_def star_n_eq_iff) |
|
653 done |
|
654 |
634 |
655 lemma hrcis: "hrcis (star_n X) (star_n Y) = star_n (%n. rcis (X n) (Y n))" |
635 lemma hrcis: "hrcis (star_n X) (star_n Y) = star_n (%n. rcis (X n) (Y n))" |
656 by (simp add: hrcis_def hcomplex_of_hypreal star_n_mult hcis rcis_def) |
636 by (simp add: hrcis_def Ifun2_of_def star_of_def Ifun_star_n) |
657 |
637 |
658 lemma hrcis_Ex: "\<exists>r a. z = hrcis r a" |
638 lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a" |
659 apply (simp add: hrcis_def hcis_eq hcomplex_of_hypreal_mult_HComplex [symmetric]) |
639 by (transfer, rule rcis_Ex) |
660 apply (rule hcomplex_split_polar) |
|
661 done |
|
662 |
640 |
663 lemma hRe_hcomplex_polar [simp]: |
641 lemma hRe_hcomplex_polar [simp]: |
664 "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
642 "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
665 r * ( *f* cos) a" |
643 r * ( *f* cos) a" |
666 by (simp add: hcomplex_of_hypreal_mult_HComplex) |
644 by (simp add: hcomplex_of_hypreal_mult_HComplex) |
667 |
645 |
668 lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a" |
646 lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a" |
669 by (simp add: hrcis_def hcis_eq) |
647 by (transfer, rule Re_rcis) |
670 |
648 |
671 lemma hIm_hcomplex_polar [simp]: |
649 lemma hIm_hcomplex_polar [simp]: |
672 "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
650 "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
673 r * ( *f* sin) a" |
651 r * ( *f* sin) a" |
674 by (simp add: hcomplex_of_hypreal_mult_HComplex) |
652 by (simp add: hcomplex_of_hypreal_mult_HComplex) |
675 |
653 |
676 lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a" |
654 lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a" |
677 by (simp add: hrcis_def hcis_eq) |
655 by (transfer, rule Im_rcis) |
678 |
656 |
679 |
657 |
680 lemma hcmod_unit_one [simp]: |
658 lemma hcmod_unit_one [simp]: |
681 "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1" |
659 "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1" |
682 by (transfer, simp) |
660 by (transfer, simp) |
683 |
661 |
684 lemma hcmod_complex_polar [simp]: |
662 lemma hcmod_complex_polar [simp]: |
685 "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
663 "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
686 abs r" |
664 abs r" |
687 apply (simp only: hcmod_mult hcmod_unit_one, simp) |
665 by (simp only: hcmod_mult hcmod_unit_one, simp) |
688 done |
666 |
689 |
667 lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r" |
690 lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r" |
668 by (transfer, rule complex_mod_rcis) |
691 by (simp add: hrcis_def hcis_eq) |
|
692 |
669 |
693 (*---------------------------------------------------------------------------*) |
670 (*---------------------------------------------------------------------------*) |
694 (* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) |
671 (* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) |
695 (*---------------------------------------------------------------------------*) |
672 (*---------------------------------------------------------------------------*) |
696 |
673 |
697 lemma hcis_hrcis_eq: "hcis a = hrcis 1 a" |
674 lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a" |
698 by (simp add: hrcis_def) |
675 by (transfer, rule cis_rcis_eq) |
699 declare hcis_hrcis_eq [symmetric, simp] |
676 declare hcis_hrcis_eq [symmetric, simp] |
700 |
677 |
701 lemma hrcis_mult: |
678 lemma hrcis_mult: |
702 "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)" |
679 "!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)" |
703 apply (simp add: hrcis_def, rule_tac z=r1 in eq_Abs_star, rule_tac z=r2 in eq_Abs_star, cases a, cases b) |
680 by (transfer, rule rcis_mult) |
704 apply (simp add: hrcis hcis star_n_add star_n_mult hcomplex_of_hypreal |
681 |
705 star_n_mult cis_mult [symmetric]) |
682 lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)" |
706 done |
683 by (transfer, rule cis_mult) |
707 |
|
708 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)" |
|
709 apply (cases a, cases b) |
|
710 apply (simp add: hcis star_n_mult star_n_add cis_mult) |
|
711 done |
|
712 |
684 |
713 lemma hcis_zero [simp]: "hcis 0 = 1" |
685 lemma hcis_zero [simp]: "hcis 0 = 1" |
714 by (simp add: star_n_one_num hcis star_n_zero_num) |
686 by (transfer, rule cis_zero) |
715 |
687 |
716 lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0" |
688 lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0" |
717 apply (simp add: star_n_zero_num, cases a) |
689 by (transfer, rule rcis_zero_mod) |
718 apply (simp add: hrcis star_n_zero_num) |
690 |
719 done |
691 lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r" |
720 |
692 by (transfer, rule rcis_zero_arg) |
721 lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r" |
|
722 apply (cases r) |
|
723 apply (simp add: hrcis star_n_zero_num hcomplex_of_hypreal) |
|
724 done |
|
725 |
693 |
726 lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x" |
694 lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x" |
727 by (simp add: mult_assoc [symmetric]) |
695 by (simp add: mult_assoc [symmetric]) |
728 |
696 |
729 lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x" |
697 lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x" |
730 by simp |
698 by simp |
731 |
699 |
732 lemma hcis_hypreal_of_nat_Suc_mult: |
700 lemma hcis_hypreal_of_nat_Suc_mult: |
733 "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)" |
701 "!!a. hcis (hypreal_of_nat (Suc n) * a) = |
734 apply (cases a) |
702 hcis a * hcis (hypreal_of_nat n * a)" |
735 apply (simp add: hypreal_of_nat hcis star_n_mult star_n_mult cis_real_of_nat_Suc_mult) |
703 apply (unfold hypreal_of_nat_def) |
|
704 apply transfer |
|
705 apply (fold real_of_nat_def) |
|
706 apply (rule cis_real_of_nat_Suc_mult) |
736 done |
707 done |
737 |
708 |
738 lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)" |
709 lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)" |
739 apply (induct_tac "n") |
710 apply (induct_tac "n") |
740 apply (simp_all add: hcis_hypreal_of_nat_Suc_mult) |
711 apply (simp_all add: hcis_hypreal_of_nat_Suc_mult) |
741 done |
712 done |
742 |
713 |
743 lemma hcis_hypreal_of_hypnat_Suc_mult: |
714 lemma hcis_hypreal_of_hypnat_Suc_mult: |
744 "hcis (hypreal_of_hypnat (n + 1) * a) = |
715 "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) = |
745 hcis a * hcis (hypreal_of_hypnat n * a)" |
716 hcis a * hcis (hypreal_of_hypnat n * a)" |
746 apply (cases a, cases n) |
717 by (transfer, simp add: cis_real_of_nat_Suc_mult) |
747 apply (simp add: hcis hypreal_of_hypnat star_n_add star_n_one_num star_n_mult star_n_mult cis_real_of_nat_Suc_mult) |
718 |
|
719 lemma NSDeMoivre_ext: |
|
720 "!!a n. (hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)" |
|
721 by (transfer, rule DeMoivre) |
|
722 |
|
723 lemma NSDeMoivre2: |
|
724 "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" |
|
725 apply (unfold hypreal_of_nat_def) |
|
726 apply transfer |
|
727 apply (fold real_of_nat_def) |
|
728 apply (rule DeMoivre2) |
748 done |
729 done |
749 |
730 |
750 lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)" |
|
751 apply (cases a, cases n) |
|
752 apply (simp add: hcis hypreal_of_hypnat star_n_mult hcpow DeMoivre) |
|
753 done |
|
754 |
|
755 lemma DeMoivre2: |
|
756 "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" |
|
757 apply (simp add: hrcis_def power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow) |
|
758 done |
|
759 |
|
760 lemma DeMoivre2_ext: |
731 lemma DeMoivre2_ext: |
761 "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
732 "!! a r n. (hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
762 apply (simp add: hrcis_def hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow) |
733 by (transfer, rule DeMoivre2) |
763 done |
734 |
764 |
735 lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)" |
765 lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)" |
736 by (transfer, simp) |
766 apply (cases a) |
737 |
767 apply (simp add: star_n_inverse2 hcis star_n_minus) |
738 lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)" |
768 done |
739 by (transfer, simp add: rcis_inverse inverse_eq_divide [symmetric]) |
769 |
740 |
770 lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)" |
741 lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a" |
771 apply (cases a, cases r) |
742 by (transfer, rule Re_cis) |
772 apply (simp add: star_n_inverse2 hrcis star_n_minus rcis_inverse star_n_eq_iff, ultra) |
743 |
773 apply (simp add: real_divide_def) |
744 lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a" |
774 done |
745 by (transfer, rule Im_cis) |
775 |
|
776 lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a" |
|
777 apply (cases a) |
|
778 apply (simp add: hcis starfun hRe) |
|
779 done |
|
780 |
|
781 lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a" |
|
782 apply (cases a) |
|
783 apply (simp add: hcis starfun hIm) |
|
784 done |
|
785 |
746 |
786 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" |
747 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" |
787 by (simp add: NSDeMoivre) |
748 by (simp add: NSDeMoivre) |
788 |
749 |
789 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
750 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
793 by (simp add: NSDeMoivre_ext) |
754 by (simp add: NSDeMoivre_ext) |
794 |
755 |
795 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" |
756 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" |
796 by (simp add: NSDeMoivre_ext) |
757 by (simp add: NSDeMoivre_ext) |
797 |
758 |
798 lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)" |
759 lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)" |
799 apply (simp add: hexpi_def, cases a, cases b) |
760 by (transfer, rule expi_add) |
800 apply (simp add: hcis hRe hIm star_n_add star_n_mult star_n_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult star_n_eq_iff) |
|
801 done |
|
802 |
761 |
803 |
762 |
804 subsection{*@{term hcomplex_of_complex}: the Injection from |
763 subsection{*@{term hcomplex_of_complex}: the Injection from |
805 type @{typ complex} to to @{typ hcomplex}*} |
764 type @{typ complex} to to @{typ hcomplex}*} |
806 |
765 |
807 lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)" |
766 lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)" |
808 by (rule inj_onI, simp) |
767 by (rule inj_onI, simp) |
809 |
768 |
810 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" |
769 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" |
811 by (simp add: iii_def star_of_def star_n_def) |
770 by (simp add: iii_def) |
812 |
|
813 lemma hcomplex_of_complex_add: |
|
814 "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2" |
|
815 by simp |
|
816 |
|
817 lemma hcomplex_of_complex_mult: |
|
818 "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2" |
|
819 by simp |
|
820 |
|
821 lemma hcomplex_of_complex_eq_iff: |
|
822 "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)" |
|
823 by simp |
|
824 |
|
825 lemma hcomplex_of_complex_minus: |
|
826 "hcomplex_of_complex (-r) = - hcomplex_of_complex r" |
|
827 by simp |
|
828 |
|
829 lemma hcomplex_of_complex_one: "hcomplex_of_complex 1 = 1" |
|
830 by simp |
|
831 |
|
832 lemma hcomplex_of_complex_zero: "hcomplex_of_complex 0 = 0" |
|
833 by simp |
|
834 |
|
835 lemma hcomplex_of_complex_zero_iff: |
|
836 "(hcomplex_of_complex r = 0) = (r = 0)" |
|
837 by simp |
|
838 |
|
839 lemma hcomplex_of_complex_inverse: |
|
840 "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)" |
|
841 by simp |
|
842 |
|
843 lemma hcomplex_of_complex_divide: |
|
844 "hcomplex_of_complex (z1 / z2) = |
|
845 hcomplex_of_complex z1 / hcomplex_of_complex z2" |
|
846 by simp |
|
847 |
771 |
848 lemma hRe_hcomplex_of_complex: |
772 lemma hRe_hcomplex_of_complex: |
849 "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" |
773 "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" |
850 by (simp add: star_of_def hRe) |
774 by (transfer, rule refl) |
851 |
775 |
852 lemma hIm_hcomplex_of_complex: |
776 lemma hIm_hcomplex_of_complex: |
853 "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)" |
777 "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)" |
854 by (simp add: star_of_def hIm) |
778 by (transfer, rule refl) |
855 |
779 |
856 lemma hcmod_hcomplex_of_complex: |
780 lemma hcmod_hcomplex_of_complex: |
857 "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)" |
781 "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)" |
858 by (simp add: star_of_def hcmod) |
782 by (transfer, rule refl) |
859 |
783 |
860 |
784 |
861 subsection{*Numerals and Arithmetic*} |
785 subsection{*Numerals and Arithmetic*} |
862 |
786 |
863 lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)" |
787 lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)" |
864 by (transfer, rule number_of_eq [THEN eq_reflection]) |
788 by (transfer, rule number_of_eq [THEN eq_reflection]) |
865 |
|
866 lemma hcomplex_of_complex_of_nat: |
|
867 "hcomplex_of_complex (of_nat n) = of_nat n" |
|
868 by (rule star_of_of_nat) |
|
869 |
|
870 lemma hcomplex_of_complex_of_int: |
|
871 "hcomplex_of_complex (of_int z) = of_int z" |
|
872 by (rule star_of_of_int) |
|
873 |
|
874 lemma hcomplex_number_of: |
|
875 "hcomplex_of_complex (number_of w) = number_of w" |
|
876 by (rule star_of_number_of) |
|
877 |
789 |
878 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: |
790 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: |
879 "hcomplex_of_hypreal (hypreal_of_real x) = |
791 "hcomplex_of_hypreal (hypreal_of_real x) = |
880 hcomplex_of_complex (complex_of_real x)" |
792 hcomplex_of_complex (complex_of_real x)" |
881 by (simp add: hcomplex_of_hypreal star_of_def |
793 by (transfer, rule refl) |
882 complex_of_real_def) |
|
883 |
794 |
884 lemma hcomplex_hypreal_number_of: |
795 lemma hcomplex_hypreal_number_of: |
885 "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)" |
796 "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)" |
886 by (simp only: complex_number_of [symmetric] star_of_number_of [symmetric] |
797 by (transfer, rule complex_number_of [symmetric]) |
887 hcomplex_of_hypreal_eq_hcomplex_of_complex) |
|
888 |
798 |
889 text{*This theorem is necessary because theorems such as |
799 text{*This theorem is necessary because theorems such as |
890 @{text iszero_number_of_0} only hold for ordered rings. They cannot |
800 @{text iszero_number_of_0} only hold for ordered rings. They cannot |
891 be generalized to fields in general because they fail for finite fields. |
801 be generalized to fields in general because they fail for finite fields. |
892 They work for type complex because the reals can be embedded in them.*} |
802 They work for type complex because the reals can be embedded in them.*} |
893 lemma iszero_hcomplex_number_of [simp]: |
803 lemma iszero_hcomplex_number_of [simp]: |
894 "iszero (number_of w :: hcomplex) = iszero (number_of w :: real)" |
804 "iszero (number_of w :: hcomplex) = iszero (number_of w :: real)" |
895 apply (simp only: iszero_complex_number_of [symmetric]) |
805 by (transfer iszero_def, simp) |
896 apply (simp only: hcomplex_of_complex_zero_iff hcomplex_number_of [symmetric] |
|
897 iszero_def) |
|
898 done |
|
899 |
806 |
900 |
807 |
901 (* |
808 (* |
902 Goal "z + hcnj z = |
809 Goal "z + hcnj z = |
903 hcomplex_of_hypreal (2 * hRe(z))" |
810 hcomplex_of_hypreal (2 * hRe(z))" |