tidying up hcomplex arithmetic
authorpaulson
Tue Dec 23 14:45:47 2003 +0100 (2003-12-23)
changeset 14320fb7a114826be
parent 14319 255190be18c0
child 14321 55c688d2eefa
tidying up hcomplex arithmetic
src/HOL/Complex/CLim.ML
src/HOL/Complex/NSCA.ML
src/HOL/Complex/NSCA.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Complex/NSComplexArith0.ML
src/HOL/Complex/NSComplexArith0.thy
src/HOL/Complex/NSComplexBin.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Complex/CLim.ML	Tue Dec 23 14:45:23 2003 +0100
     1.2 +++ b/src/HOL/Complex/CLim.ML	Tue Dec 23 14:45:47 2003 +0100
     1.3 @@ -468,12 +468,12 @@
     1.4  by Auto_tac;
     1.5  by (dres_inst_tac [("x","hcomplex_of_complex a + x")] spec 1);
     1.6  by (dres_inst_tac [("x","- hcomplex_of_complex a + x")] spec 2);
     1.7 -by (Step_tac 1);
     1.8 +by Safe_tac;
     1.9  by (Asm_full_simp_tac 1);
    1.10  by (rtac ((mem_cinfmal_iff RS iffD2) RS 
    1.11      (CInfinitesimal_add_capprox_self RS capprox_sym)) 1);
    1.12  by (rtac (capprox_minus_iff2 RS iffD1) 4);
    1.13 -by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute]) 3);
    1.14 +by (asm_full_simp_tac (simpset() addsimps compare_rls@[hcomplex_add_commute]) 3);
    1.15  by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2);
    1.16  by (res_inst_tac [("z","x")] eq_Abs_hcomplex 4);
    1.17  by (auto_tac (claset(),
    1.18 @@ -747,7 +747,8 @@
    1.19  by (auto_tac (claset(),simpset() addsimps [isNSContc_NSCLIM_iff,
    1.20      NSCLIM_def,hcomplex_diff_def]));
    1.21  by (dtac (capprox_minus_iff RS iffD1) 1);
    1.22 -by (dtac (CLAIM "x ~= a ==> x + - a ~= (0::hcomplex)") 1);
    1.23 +by (subgoal_tac "xa + - (hcomplex_of_complex x) ~= 0" 1);
    1.24 + by (asm_full_simp_tac (simpset() addsimps compare_rls) 2);
    1.25  by (dres_inst_tac [("x","- hcomplex_of_complex x + xa")] bspec 1);
    1.26  by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 2);
    1.27  by (auto_tac (claset(),simpset() addsimps 
    1.28 @@ -1041,12 +1042,14 @@
    1.29  by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1);
    1.30  qed "NSCDERIV_pow";
    1.31  
    1.32 -Goal "\\<lbrakk> CDERIV f x :> D; D = E \\<rbrakk> \\<Longrightarrow> CDERIV f x :> E";
    1.33 +Goal "[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E";
    1.34  by Auto_tac;
    1.35  qed "lemma_CDERIV_subst";
    1.36  
    1.37  (*used once, in NSCDERIV_inverse*)
    1.38  Goal "[| h: CInfinitesimal; x ~= 0 |] ==> hcomplex_of_complex x + h ~= 0";
    1.39 +by (Clarify_tac 1);
    1.40 +by (dtac (thm"equals_zero_I") 1);
    1.41  by Auto_tac;  
    1.42  qed "CInfinitesimal_add_not_zero";
    1.43  
    1.44 @@ -1062,7 +1065,7 @@
    1.45                 delsimps [hcomplex_minus_mult_eq1 RS sym,
    1.46                           hcomplex_minus_mult_eq2 RS sym]));
    1.47  by (asm_simp_tac
    1.48 -     (simpset() addsimps [hcomplex_inverse_add,
    1.49 +     (simpset() addsimps [inverse_add,
    1.50            inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym] 
    1.51            @ hcomplex_add_ac @ hcomplex_mult_ac 
    1.52         delsimps [thm"Ring_and_Field.inverse_minus_eq",
     2.1 --- a/src/HOL/Complex/NSCA.ML	Tue Dec 23 14:45:23 2003 +0100
     2.2 +++ b/src/HOL/Complex/NSCA.ML	Tue Dec 23 14:45:47 2003 +0100
     2.3 @@ -1252,7 +1252,7 @@
     2.4  by (forward_tac [CFinite_minus_iff RS iffD2] 1);
     2.5  by (rtac hcomplex_add_minus_eq_minus 1);
     2.6  by (dtac (stc_add RS sym) 1 THEN assume_tac 1);
     2.7 -by Auto_tac;  
     2.8 +by (asm_simp_tac (simpset() addsimps [add_commute]) 1); 
     2.9  qed "stc_minus";
    2.10  
    2.11  Goalw [hcomplex_diff_def]
     3.1 --- a/src/HOL/Complex/NSCA.thy	Tue Dec 23 14:45:23 2003 +0100
     3.2 +++ b/src/HOL/Complex/NSCA.thy	Tue Dec 23 14:45:47 2003 +0100
     3.3 @@ -4,7 +4,7 @@
     3.4      Description : Infinite, infinitesimal complex number etc! 
     3.5  *)
     3.6  
     3.7 -NSCA = NSComplexArith0 + 
     3.8 +NSCA = NSComplexArith + 
     3.9  
    3.10  consts   
    3.11  
     4.1 --- a/src/HOL/Complex/NSComplex.thy	Tue Dec 23 14:45:23 2003 +0100
     4.2 +++ b/src/HOL/Complex/NSComplex.thy	Tue Dec 23 14:45:47 2003 +0100
     4.3 @@ -1761,13 +1761,13 @@
     4.4  done
     4.5  declare hcomplex_of_complex_minus [simp]
     4.6  
     4.7 -lemma hcomplex_of_complex_one:
     4.8 +lemma hcomplex_of_complex_one [simp]:
     4.9        "hcomplex_of_complex 1 = 1"
    4.10  apply (unfold hcomplex_of_complex_def hcomplex_one_def)
    4.11  apply auto
    4.12  done
    4.13  
    4.14 -lemma hcomplex_of_complex_zero:
    4.15 +lemma hcomplex_of_complex_zero [simp]:
    4.16        "hcomplex_of_complex 0 = 0"
    4.17  apply (unfold hcomplex_of_complex_def hcomplex_zero_def)
    4.18  apply (simp (no_asm))
     5.1 --- a/src/HOL/Complex/NSComplexArith0.ML	Tue Dec 23 14:45:23 2003 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,328 +0,0 @@
     5.4 -(*  Title:       NSComplexArith0.ML
     5.5 -    Author:      Jacques D. Fleuriot
     5.6 -    Copyright:   2001  University of Edinburgh
     5.7 -    Description: Assorted facts that need binary literals 
     5.8 -		 Also, common factor cancellation (see e.g. HyperArith0)
     5.9 -*)
    5.10 -
    5.11 -(****
    5.12 -Goal "((x * y = #0) = (x = #0 | y = (#0::hcomplex)))";
    5.13 -by (auto_tac (claset(),simpset() addsimps [rename_numerals hcomplex_mult_zero_iff]));
    5.14 -qed "hcomplex_mult_is_0";
    5.15 -AddIffs [hcomplex_mult_is_0];
    5.16 -****)
    5.17 -
    5.18 -(** Division and inverse **)
    5.19 -
    5.20 -Goal "0/x = (0::hcomplex)";
    5.21 -by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); 
    5.22 -qed "hcomplex_0_divide";
    5.23 -Addsimps [hcomplex_0_divide];
    5.24 -
    5.25 -Goalw [hcomplex_divide_def] "x/(0::hcomplex) = 0";
    5.26 -by (stac HCOMPLEX_INVERSE_ZERO 1); 
    5.27 -by (Simp_tac 1); 
    5.28 -qed "HCOMPLEX_DIVIDE_ZERO";
    5.29 -
    5.30 -Goal "inverse (x::hcomplex) = 1/x";
    5.31 -by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); 
    5.32 -qed "hcomplex_inverse_eq_divide";
    5.33 -
    5.34 -Goal "(inverse(x::hcomplex) = 0) = (x = 0)";
    5.35 -by (Simp_tac 1);
    5.36 -qed "hcomplex_inverse_zero_iff";
    5.37 -Addsimps [hcomplex_inverse_zero_iff];
    5.38 -
    5.39 -Goal "(x/y = 0) = (x=0 | y=(0::hcomplex))";
    5.40 -by (auto_tac (claset(), simpset() addsimps [hcomplex_divide_def]));  
    5.41 -qed "hcomplex_divide_eq_0_iff";
    5.42 -Addsimps [hcomplex_divide_eq_0_iff];
    5.43 -
    5.44 -Goal "h ~= (0::hcomplex) ==> h/h = 1";
    5.45 -by (asm_simp_tac 
    5.46 -    (simpset() addsimps [hcomplex_divide_def]) 1);
    5.47 -qed "hcomplex_divide_self_eq"; 
    5.48 -Addsimps [hcomplex_divide_self_eq];
    5.49 -
    5.50 -bind_thm ("hcomplex_mult_minus_right", hcomplex_minus_mult_eq2 RS sym);
    5.51 -
    5.52 -Goal "!!k::hcomplex. (k*m = k*n) = (k = 0 | m=n)";
    5.53 -by (case_tac "k=0" 1);
    5.54 -by (auto_tac (claset(), simpset() addsimps [hcomplex_mult_left_cancel]));  
    5.55 -qed "hcomplex_mult_eq_cancel1";
    5.56 -
    5.57 -Goal "!!k::hcomplex. (m*k = n*k) = (k = 0 | m=n)";
    5.58 -by (case_tac "k=0" 1);
    5.59 -by (auto_tac (claset(), simpset() addsimps [hcomplex_mult_right_cancel]));  
    5.60 -qed "hcomplex_mult_eq_cancel2";
    5.61 -
    5.62 -Goal "!!k::hcomplex. k~=0 ==> (k*m) / (k*n) = (m/n)";
    5.63 -by (asm_simp_tac
    5.64 -    (simpset() addsimps [hcomplex_divide_def, inverse_mult_distrib]) 1); 
    5.65 -by (subgoal_tac "k * m * (inverse k * inverse n) = \
    5.66 -\                (k * inverse k) * (m * inverse n)" 1);
    5.67 -by (Asm_full_simp_tac 1);
    5.68 -by (asm_full_simp_tac (HOL_ss addsimps hcomplex_mult_ac) 1); 
    5.69 -qed "hcomplex_mult_div_cancel1";
    5.70 -
    5.71 -(*For ExtractCommonTerm*)
    5.72 -Goal "(k*m) / (k*n) = (if k = (0::hcomplex) then 0 else m/n)";
    5.73 -by (simp_tac (simpset() addsimps [hcomplex_mult_div_cancel1]) 1); 
    5.74 -qed "hcomplex_mult_div_cancel_disj";
    5.75 -
    5.76 -
    5.77 -local
    5.78 -  open HComplex_Numeral_Simprocs
    5.79 -in
    5.80 -
    5.81 -val rel_hcomplex_number_of = [eq_hcomplex_number_of];
    5.82 -
    5.83 -
    5.84 -structure CancelNumeralFactorCommon =
    5.85 -  struct
    5.86 -  val mk_coeff		= mk_coeff
    5.87 -  val dest_coeff	= dest_coeff 1
    5.88 -  val trans_tac         = Real_Numeral_Simprocs.trans_tac
    5.89 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps @ mult_1s))
    5.90 -                 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps))
    5.91 -                 THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_mult_ac))
    5.92 -  val numeral_simp_tac	= 
    5.93 -         ALLGOALS (simp_tac (HOL_ss addsimps rel_hcomplex_number_of@bin_simps))
    5.94 -  val simplify_meta_eq  = simplify_meta_eq
    5.95 -  end
    5.96 -
    5.97 -
    5.98 -structure DivCancelNumeralFactor = CancelNumeralFactorFun
    5.99 - (open CancelNumeralFactorCommon
   5.100 -  val prove_conv = Bin_Simprocs.prove_conv
   5.101 -  val mk_bal   = HOLogic.mk_binop "HOL.divide"
   5.102 -  val dest_bal = HOLogic.dest_bin "HOL.divide" hcomplexT
   5.103 -  val cancel = hcomplex_mult_div_cancel1 RS trans
   5.104 -  val neg_exchanges = false
   5.105 -)
   5.106 -
   5.107 -
   5.108 -structure EqCancelNumeralFactor = CancelNumeralFactorFun
   5.109 - (open CancelNumeralFactorCommon
   5.110 -  val prove_conv = Bin_Simprocs.prove_conv
   5.111 -  val mk_bal   = HOLogic.mk_eq
   5.112 -  val dest_bal = HOLogic.dest_bin "op =" hcomplexT
   5.113 -  val cancel = hcomplex_mult_eq_cancel1 RS trans
   5.114 -  val neg_exchanges = false
   5.115 -)
   5.116 -
   5.117 -
   5.118 -val hcomplex_cancel_numeral_factors_relations = 
   5.119 -  map prep_simproc
   5.120 -   [("hcomplexeq_cancel_numeral_factor",
   5.121 -    ["(l::hcomplex) * m = n", "(l::hcomplex) = m * n"], 
   5.122 -     EqCancelNumeralFactor.proc)];
   5.123 -
   5.124 -val hcomplex_cancel_numeral_factors_divide = prep_simproc
   5.125 -	("hcomplexdiv_cancel_numeral_factor", 
   5.126 -	 ["((l::hcomplex) * m) / n", "(l::hcomplex) / (m * n)", 
   5.127 -                     "((number_of v)::hcomplex) / (number_of w)"], 
   5.128 -	 DivCancelNumeralFactor.proc);
   5.129 -
   5.130 -val hcomplex_cancel_numeral_factors = 
   5.131 -    hcomplex_cancel_numeral_factors_relations @ 
   5.132 -    [hcomplex_cancel_numeral_factors_divide];
   5.133 -
   5.134 -end;
   5.135 -
   5.136 -
   5.137 -Addsimprocs hcomplex_cancel_numeral_factors;
   5.138 -
   5.139 -
   5.140 -(*examples:
   5.141 -print_depth 22;
   5.142 -set timing;
   5.143 -set trace_simp;
   5.144 -fun test s = (Goal s; by (Simp_tac 1)); 
   5.145 -
   5.146 -
   5.147 -test "#9*x = #12 * (y::hcomplex)";
   5.148 -test "(#9*x) / (#12 * (y::hcomplex)) = z";
   5.149 -
   5.150 -test "#-99*x = #132 * (y::hcomplex)";
   5.151 -
   5.152 -test "#999*x = #-396 * (y::hcomplex)";
   5.153 -test "(#999*x) / (#-396 * (y::hcomplex)) = z";
   5.154 -
   5.155 -test "#-99*x = #-81 * (y::hcomplex)";
   5.156 -test "(#-99*x) / (#-81 * (y::hcomplex)) = z";
   5.157 -
   5.158 -test "#-2 * x = #-1 * (y::hcomplex)";
   5.159 -test "#-2 * x = -(y::hcomplex)";
   5.160 -test "(#-2 * x) / (#-1 * (y::hcomplex)) = z";
   5.161 -
   5.162 -*)
   5.163 -
   5.164 -
   5.165 -(** Declarations for ExtractCommonTerm **)
   5.166 -
   5.167 -local
   5.168 -  open HComplex_Numeral_Simprocs
   5.169 -in
   5.170 -
   5.171 -structure CancelFactorCommon =
   5.172 -  struct
   5.173 -  val mk_sum    	= long_mk_prod
   5.174 -  val dest_sum		= dest_prod
   5.175 -  val mk_coeff		= mk_coeff
   5.176 -  val dest_coeff	= dest_coeff
   5.177 -  val find_first	= find_first []
   5.178 -  val trans_tac         = Real_Numeral_Simprocs.trans_tac
   5.179 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hcomplex_mult_ac))
   5.180 -  end;
   5.181 -
   5.182 -
   5.183 -structure EqCancelFactor = ExtractCommonTermFun
   5.184 - (open CancelFactorCommon
   5.185 -  val prove_conv = Bin_Simprocs.prove_conv
   5.186 -  val mk_bal   = HOLogic.mk_eq
   5.187 -  val dest_bal = HOLogic.dest_bin "op =" hcomplexT
   5.188 -  val simplify_meta_eq  = cancel_simplify_meta_eq hcomplex_mult_eq_cancel1
   5.189 -);
   5.190 -
   5.191 -
   5.192 -structure DivideCancelFactor = ExtractCommonTermFun
   5.193 - (open CancelFactorCommon
   5.194 -  val prove_conv = Bin_Simprocs.prove_conv
   5.195 -  val mk_bal   = HOLogic.mk_binop "HOL.divide"
   5.196 -  val dest_bal = HOLogic.dest_bin "HOL.divide" hcomplexT
   5.197 -  val simplify_meta_eq  = cancel_simplify_meta_eq hcomplex_mult_div_cancel_disj
   5.198 -);
   5.199 -
   5.200 -val hcomplex_cancel_factor = 
   5.201 -  map prep_simproc
   5.202 -   [("hcomplex_eq_cancel_factor", ["(l::hcomplex) * m = n", "(l::hcomplex) = m * n"], 
   5.203 -     EqCancelFactor.proc),
   5.204 -    ("hcomplex_divide_cancel_factor", ["((l::hcomplex) * m) / n", "(l::hcomplex) / (m * n)"], 
   5.205 -     DivideCancelFactor.proc)];
   5.206 -
   5.207 -end;
   5.208 -
   5.209 -Addsimprocs hcomplex_cancel_factor;
   5.210 -
   5.211 -
   5.212 -(*examples:
   5.213 -print_depth 22;
   5.214 -set timing;
   5.215 -set trace_simp;
   5.216 -fun test s = (Goal s; by (Asm_simp_tac 1)); 
   5.217 -
   5.218 -test "x*k = k*(y::hcomplex)";
   5.219 -test "k = k*(y::hcomplex)"; 
   5.220 -test "a*(b*c) = (b::hcomplex)";
   5.221 -test "a*(b*c) = d*(b::hcomplex)*(x*a)";
   5.222 -
   5.223 -
   5.224 -test "(x*k) / (k*(y::hcomplex)) = (uu::hcomplex)";
   5.225 -test "(k) / (k*(y::hcomplex)) = (uu::hcomplex)"; 
   5.226 -test "(a*(b*c)) / ((b::hcomplex)) = (uu::hcomplex)";
   5.227 -test "(a*(b*c)) / (d*(b::hcomplex)*(x*a)) = (uu::hcomplex)";
   5.228 -
   5.229 -(*FIXME: what do we do about this?*)
   5.230 -test "a*(b*c)/(y*z) = d*(b::hcomplex)*(x*a)/z";
   5.231 -*)
   5.232 -
   5.233 -
   5.234 -Goal "z~=0 ==> ((x::hcomplex) = y/z) = (x*z = y)";
   5.235 -by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
   5.236 -by (asm_simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_mult_assoc]) 2); 
   5.237 -by (etac ssubst 1);
   5.238 -by (stac hcomplex_mult_eq_cancel2 1); 
   5.239 -by (Asm_simp_tac 1); 
   5.240 -qed "hcomplex_eq_divide_eq";
   5.241 -Addsimps [inst "z" "number_of ?w" hcomplex_eq_divide_eq];
   5.242 -
   5.243 -Goal "z~=0 ==> (y/z = (x::hcomplex)) = (y = x*z)";
   5.244 -by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
   5.245 -by (asm_simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_mult_assoc]) 2); 
   5.246 -by (etac ssubst 1);
   5.247 -by (stac hcomplex_mult_eq_cancel2 1); 
   5.248 -by (Asm_simp_tac 1); 
   5.249 -qed "hcomplex_divide_eq_eq";
   5.250 -Addsimps [inst "z" "number_of ?w" hcomplex_divide_eq_eq];
   5.251 -
   5.252 -Goal "(m/k = n/k) = (k = 0 | m = (n::hcomplex))";
   5.253 -by (case_tac "k=0" 1);
   5.254 -by (asm_simp_tac (simpset() addsimps [HCOMPLEX_DIVIDE_ZERO]) 1); 
   5.255 -by (asm_simp_tac (simpset() addsimps [hcomplex_divide_eq_eq, hcomplex_eq_divide_eq, 
   5.256 -                                      hcomplex_mult_eq_cancel2]) 1); 
   5.257 -qed "hcomplex_divide_eq_cancel2";
   5.258 -
   5.259 -Goal "(k/m = k/n) = (k = 0 | m = (n::hcomplex))";
   5.260 -by (case_tac "m=0 | n = 0" 1);
   5.261 -by (auto_tac (claset(), 
   5.262 -              simpset() addsimps [HCOMPLEX_DIVIDE_ZERO, hcomplex_divide_eq_eq, 
   5.263 -                                  hcomplex_eq_divide_eq, hcomplex_mult_eq_cancel1]));  
   5.264 -qed "hcomplex_divide_eq_cancel1";
   5.265 -
   5.266 -(** Division by 1, -1 **)
   5.267 -
   5.268 -Goal "(x::hcomplex)/1 = x";
   5.269 -by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); 
   5.270 -qed "hcomplex_divide_1";
   5.271 -Addsimps [hcomplex_divide_1];
   5.272 -
   5.273 -Goal "x/-1 = -(x::hcomplex)";
   5.274 -by (Simp_tac 1); 
   5.275 -qed "hcomplex_divide_minus1";
   5.276 -Addsimps [hcomplex_divide_minus1];
   5.277 -
   5.278 -Goal "-1/(x::hcomplex) = - (1/x)";
   5.279 -by (simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_minus_inverse]) 1); 
   5.280 -qed "hcomplex_minus1_divide";
   5.281 -Addsimps [hcomplex_minus1_divide];
   5.282 -
   5.283 -
   5.284 -Goal "(x = - y) = (y = - (x::hcomplex))";
   5.285 -by Auto_tac;
   5.286 -qed "hcomplex_equation_minus";
   5.287 -
   5.288 -Goal "(- x = y) = (- (y::hcomplex) = x)";
   5.289 -by Auto_tac;
   5.290 -qed "hcomplex_minus_equation";
   5.291 -
   5.292 -Goal "(x + - a = (0::hcomplex)) = (x=a)";
   5.293 -by (simp_tac (simpset() addsimps [hcomplex_diff_eq_eq,symmetric hcomplex_diff_def]) 1);
   5.294 -qed "hcomplex_add_minus_iff";
   5.295 -Addsimps [hcomplex_add_minus_iff];
   5.296 -
   5.297 -Goal "(-b = -a) = (b = (a::hcomplex))";
   5.298 -by Auto_tac;
   5.299 -qed "hcomplex_minus_eq_cancel";
   5.300 -Addsimps [hcomplex_minus_eq_cancel];
   5.301 -
   5.302 -(*Distributive laws for literals*)
   5.303 -Addsimps (map (inst "w" "number_of ?v")
   5.304 -	  [hcomplex_add_mult_distrib, hcomplex_add_mult_distrib2,
   5.305 -	   hcomplex_diff_mult_distrib, hcomplex_diff_mult_distrib2]);
   5.306 -
   5.307 -Addsimps [inst "x" "number_of ?v" hcomplex_equation_minus];
   5.308 -
   5.309 -Addsimps [inst "y" "number_of ?v" hcomplex_minus_equation];
   5.310 -
   5.311 -Goal "(x+y = (0::hcomplex)) = (y = -x)";
   5.312 -by Auto_tac;
   5.313 -by (dtac (sym RS (hcomplex_diff_eq_eq RS iffD2)) 1);
   5.314 -by Auto_tac;  
   5.315 -qed "hcomplex_add_eq_0_iff";
   5.316 -AddIffs [hcomplex_add_eq_0_iff];
   5.317 -
   5.318 -Goalw [hcomplex_diff_def]"-(x-y) = y - (x::hcomplex)";
   5.319 -by (auto_tac (claset(),simpset() addsimps [hcomplex_add_commute]));
   5.320 -qed "hcomplex_minus_diff_eq";
   5.321 -Addsimps [hcomplex_minus_diff_eq];
   5.322 -
   5.323 -Addsimps [inst "x" "number_of ?w" hcomplex_inverse_eq_divide];
   5.324 -
   5.325 -Goal "[|(x::hcomplex) ~= 0;  y ~= 0 |]  \
   5.326 -\     ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)";
   5.327 -by (asm_full_simp_tac (simpset() addsimps [inverse_mult_distrib,
   5.328 -                    hcomplex_add_mult_distrib,hcomplex_mult_assoc RS sym]) 1);
   5.329 -qed "hcomplex_inverse_add";
   5.330 -
   5.331 -Addsimps [hcomplex_of_complex_zero,hcomplex_of_complex_one];
     6.1 --- a/src/HOL/Complex/NSComplexArith0.thy	Tue Dec 23 14:45:23 2003 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,4 +0,0 @@
     6.4 -NSComplexArith0 = NSComplexBin
     6.5 -
     6.6 -
     6.7 -
     7.1 --- a/src/HOL/Complex/NSComplexBin.ML	Tue Dec 23 14:45:23 2003 +0100
     7.2 +++ b/src/HOL/Complex/NSComplexBin.ML	Tue Dec 23 14:45:47 2003 +0100
     7.3 @@ -24,11 +24,11 @@
     7.4  qed "hcomplex_hypreal_number_of";
     7.5  
     7.6  Goalw [hcomplex_number_of_def] "Numeral0 = (0::hcomplex)";
     7.7 -by (simp_tac (simpset() addsimps [hcomplex_of_complex_zero RS sym]) 1);
     7.8 +by(Simp_tac 1);
     7.9  qed "hcomplex_numeral_0_eq_0";
    7.10  
    7.11  Goalw [hcomplex_number_of_def] "Numeral1 = (1::hcomplex)";
    7.12 -by (simp_tac (simpset() addsimps [hcomplex_of_complex_one RS sym]) 1);
    7.13 +by(Simp_tac 1);
    7.14  qed "hcomplex_numeral_1_eq_1";
    7.15  
    7.16  (*
     8.1 --- a/src/HOL/IsaMakefile	Tue Dec 23 14:45:23 2003 +0100
     8.2 +++ b/src/HOL/IsaMakefile	Tue Dec 23 14:45:47 2003 +0100
     8.3 @@ -174,7 +174,7 @@
     8.4    Complex/ComplexBin.ML Complex/ComplexBin.thy\
     8.5    Complex/NSCA.ML Complex/NSCA.thy\
     8.6    Complex/NSComplex.thy\
     8.7 -  Complex/NSComplexArith0.ML Complex/NSComplexArith0.thy\
     8.8 +  Complex/hcomplex_arith.ML Complex/NSComplexArith.thy\
     8.9    Complex/NSComplexBin.ML Complex/NSComplexBin.thy
    8.10  	@cd Complex; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Complex
    8.11