equal
deleted
inserted
replaced
402 |
402 |
403 (* |
403 (* |
404 Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N"; |
404 Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N"; |
405 *) |
405 *) |
406 |
406 |
407 Goalw [hypnat_of_nat_def] |
407 Goal "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"; |
408 "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"; |
|
409 by (res_inst_tac [("z","Z")] eq_Abs_hcomplex 1); |
408 by (res_inst_tac [("z","Z")] eq_Abs_hcomplex 1); |
410 by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC])); |
409 by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC,hypnat_of_nat_eq])); |
411 qed "starfunC_hcpow"; |
410 qed "starfunC_hcpow"; |
412 |
411 |
413 Goal "( *fc* (%h. f (x + h))) xa = ( *fc* f) (hcomplex_of_complex x + xa)"; |
412 Goal "( *fc* (%h. f (x + h))) xa = ( *fc* f) (hcomplex_of_complex x + xa)"; |
414 by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); |
413 by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); |
415 by (auto_tac (claset(),simpset() addsimps [starfunC, |
414 by (auto_tac (claset(),simpset() addsimps [starfunC, |