src/HOL/Complex/NSComplex.thy

 
 lemma hcomplex_hypreal_number_of: 
   "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)
 
 lemma hcomplex_number_of_hcmod [simp]: