--- a/src/HOL/Complex/NSComplex.thy Wed Jun 11 15:40:44 2008 +0200
+++ b/src/HOL/Complex/NSComplex.thy Wed Jun 11 15:41:08 2008 +0200
@@ -655,108 +655,6 @@
"hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
by transfer (rule of_real_number_of_eq [symmetric])
-(*
-Goal "z + hcnj z =
- hcomplex_of_hypreal (2 * hRe(z))"
-by (res_inst_tac [("z","z")] eq_Abs_star 1);
-by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,star_n_add,
- hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
-qed "star_n_add_hcnj";
-
-Goal "z - hcnj z = \
-\ hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii";
-by (res_inst_tac [("z","z")] eq_Abs_star 1);
-by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
- hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
- complex_diff_cnj,iii_def,star_n_mult]));
-qed "hcomplex_diff_hcnj";
-*)
-
-
-(*** Real and imaginary stuff ***)
-
-(*Convert???
-Goalw [hcomplex_number_of_def]
- "((number_of xa :: hcomplex) + iii * number_of ya =
- number_of xb + iii * number_of yb) =
- (((number_of xa :: hcomplex) = number_of xb) &
- ((number_of ya :: hcomplex) = number_of yb))"
-by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff,
- hcomplex_hypreal_number_of]));
-qed "hcomplex_number_of_eq_cancel_iff";
-Addsimps [hcomplex_number_of_eq_cancel_iff];
-
-Goalw [hcomplex_number_of_def]
- "((number_of xa :: hcomplex) + number_of ya * iii = \
-\ number_of xb + number_of yb * iii) = \
-\ (((number_of xa :: hcomplex) = number_of xb) & \
-\ ((number_of ya :: hcomplex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA,
- hcomplex_hypreal_number_of]));
-qed "hcomplex_number_of_eq_cancel_iffA";
-Addsimps [hcomplex_number_of_eq_cancel_iffA];
-
-Goalw [hcomplex_number_of_def]
- "((number_of xa :: hcomplex) + number_of ya * iii = \
-\ number_of xb + iii * number_of yb) = \
-\ (((number_of xa :: hcomplex) = number_of xb) & \
-\ ((number_of ya :: hcomplex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB,
- hcomplex_hypreal_number_of]));
-qed "hcomplex_number_of_eq_cancel_iffB";
-Addsimps [hcomplex_number_of_eq_cancel_iffB];
-
-Goalw [hcomplex_number_of_def]
- "((number_of xa :: hcomplex) + iii * number_of ya = \
-\ number_of xb + number_of yb * iii) = \
-\ (((number_of xa :: hcomplex) = number_of xb) & \
-\ ((number_of ya :: hcomplex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC,
- hcomplex_hypreal_number_of]));
-qed "hcomplex_number_of_eq_cancel_iffC";
-Addsimps [hcomplex_number_of_eq_cancel_iffC];
-
-Goalw [hcomplex_number_of_def]
- "((number_of xa :: hcomplex) + iii * number_of ya = \
-\ number_of xb) = \
-\ (((number_of xa :: hcomplex) = number_of xb) & \
-\ ((number_of ya :: hcomplex) = 0))";
-by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2,
- hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
-qed "hcomplex_number_of_eq_cancel_iff2";
-Addsimps [hcomplex_number_of_eq_cancel_iff2];
-
-Goalw [hcomplex_number_of_def]
- "((number_of xa :: hcomplex) + number_of ya * iii = \
-\ number_of xb) = \
-\ (((number_of xa :: hcomplex) = number_of xb) & \
-\ ((number_of ya :: hcomplex) = 0))";
-by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a,
- hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
-qed "hcomplex_number_of_eq_cancel_iff2a";
-Addsimps [hcomplex_number_of_eq_cancel_iff2a];
-
-Goalw [hcomplex_number_of_def]
- "((number_of xa :: hcomplex) + iii * number_of ya = \
-\ iii * number_of yb) = \
-\ (((number_of xa :: hcomplex) = 0) & \
-\ ((number_of ya :: hcomplex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3,
- hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
-qed "hcomplex_number_of_eq_cancel_iff3";
-Addsimps [hcomplex_number_of_eq_cancel_iff3];
-
-Goalw [hcomplex_number_of_def]
- "((number_of xa :: hcomplex) + number_of ya * iii= \
-\ iii * number_of yb) = \
-\ (((number_of xa :: hcomplex) = 0) & \
-\ ((number_of ya :: hcomplex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a,
- hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
-qed "hcomplex_number_of_eq_cancel_iff3a";
-Addsimps [hcomplex_number_of_eq_cancel_iff3a];
-*)
-
lemma hcomplex_number_of_hcnj [simp]:
"hcnj (number_of v :: hcomplex) = number_of v"
by transfer (rule complex_cnj_number_of)