tidying up hcomplex arithmetic

--- a/src/HOL/Complex/CLim.ML	Tue Dec 23 14:45:23 2003 +0100
+++ b/src/HOL/Complex/CLim.ML	Tue Dec 23 14:45:47 2003 +0100
@@ -468,12 +468,12 @@
 by Auto_tac;
 by (dres_inst_tac [("x","hcomplex_of_complex a + x")] spec 1);
 by (dres_inst_tac [("x","- hcomplex_of_complex a + x")] spec 2);
-by (Step_tac 1);
+by Safe_tac;
 by (Asm_full_simp_tac 1);
 by (rtac ((mem_cinfmal_iff RS iffD2) RS 
     (CInfinitesimal_add_capprox_self RS capprox_sym)) 1);
 by (rtac (capprox_minus_iff2 RS iffD1) 4);
-by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute]) 3);
+by (asm_full_simp_tac (simpset() addsimps compare_rls@[hcomplex_add_commute]) 3);
 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2);
 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 4);
 by (auto_tac (claset(),
@@ -747,7 +747,8 @@
 by (auto_tac (claset(),simpset() addsimps [isNSContc_NSCLIM_iff,
     NSCLIM_def,hcomplex_diff_def]));
 by (dtac (capprox_minus_iff RS iffD1) 1);
-by (dtac (CLAIM "x ~= a ==> x + - a ~= (0::hcomplex)") 1);
+by (subgoal_tac "xa + - (hcomplex_of_complex x) ~= 0" 1);
+ by (asm_full_simp_tac (simpset() addsimps compare_rls) 2);
 by (dres_inst_tac [("x","- hcomplex_of_complex x + xa")] bspec 1);
 by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 2);
 by (auto_tac (claset(),simpset() addsimps 
@@ -1041,12 +1042,14 @@
 by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1);
 qed "NSCDERIV_pow";
 
-Goal "\\<lbrakk> CDERIV f x :> D; D = E \\<rbrakk> \\<Longrightarrow> CDERIV f x :> E";
+Goal "[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E";
 by Auto_tac;
 qed "lemma_CDERIV_subst";
 
 (*used once, in NSCDERIV_inverse*)
 Goal "[| h: CInfinitesimal; x ~= 0 |] ==> hcomplex_of_complex x + h ~= 0";
+by (Clarify_tac 1);
+by (dtac (thm"equals_zero_I") 1);
 by Auto_tac;  
 qed "CInfinitesimal_add_not_zero";
 
@@ -1062,7 +1065,7 @@
                delsimps [hcomplex_minus_mult_eq1 RS sym,
                          hcomplex_minus_mult_eq2 RS sym]));
 by (asm_simp_tac
-     (simpset() addsimps [hcomplex_inverse_add,
+     (simpset() addsimps [inverse_add,
           inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym] 
           @ hcomplex_add_ac @ hcomplex_mult_ac 
        delsimps [thm"Ring_and_Field.inverse_minus_eq",

--- a/src/HOL/Complex/NSCA.ML	Tue Dec 23 14:45:23 2003 +0100
+++ b/src/HOL/Complex/NSCA.ML	Tue Dec 23 14:45:47 2003 +0100
@@ -1252,7 +1252,7 @@
 by (forward_tac [CFinite_minus_iff RS iffD2] 1);
 by (rtac hcomplex_add_minus_eq_minus 1);
 by (dtac (stc_add RS sym) 1 THEN assume_tac 1);
-by Auto_tac;  
+by (asm_simp_tac (simpset() addsimps [add_commute]) 1); 
 qed "stc_minus";
 
 Goalw [hcomplex_diff_def]

--- a/src/HOL/Complex/NSCA.thy	Tue Dec 23 14:45:23 2003 +0100
+++ b/src/HOL/Complex/NSCA.thy	Tue Dec 23 14:45:47 2003 +0100
@@ -4,7 +4,7 @@
     Description : Infinite, infinitesimal complex number etc! 
 *)
 
-NSCA = NSComplexArith0 + 
+NSCA = NSComplexArith + 
 
 consts   
 

--- a/src/HOL/Complex/NSComplex.thy	Tue Dec 23 14:45:23 2003 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Tue Dec 23 14:45:47 2003 +0100
@@ -1761,13 +1761,13 @@
 done
 declare hcomplex_of_complex_minus [simp]
 
-lemma hcomplex_of_complex_one:
+lemma hcomplex_of_complex_one [simp]:
       "hcomplex_of_complex 1 = 1"
 apply (unfold hcomplex_of_complex_def hcomplex_one_def)
 apply auto
 done
 
-lemma hcomplex_of_complex_zero:
+lemma hcomplex_of_complex_zero [simp]:
       "hcomplex_of_complex 0 = 0"
 apply (unfold hcomplex_of_complex_def hcomplex_zero_def)
 apply (simp (no_asm))

--- a/src/HOL/Complex/NSComplexArith0.ML	Tue Dec 23 14:45:23 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,328 +0,0 @@
-(*  Title:       NSComplexArith0.ML
-    Author:      Jacques D. Fleuriot
-    Copyright:   2001  University of Edinburgh
-    Description: Assorted facts that need binary literals 
-		 Also, common factor cancellation (see e.g. HyperArith0)
-*)
-
-(****
-Goal "((x * y = #0) = (x = #0 | y = (#0::hcomplex)))";
-by (auto_tac (claset(),simpset() addsimps [rename_numerals hcomplex_mult_zero_iff]));
-qed "hcomplex_mult_is_0";
-AddIffs [hcomplex_mult_is_0];
-****)
-
-(** Division and inverse **)
-
-Goal "0/x = (0::hcomplex)";
-by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); 
-qed "hcomplex_0_divide";
-Addsimps [hcomplex_0_divide];
-
-Goalw [hcomplex_divide_def] "x/(0::hcomplex) = 0";
-by (stac HCOMPLEX_INVERSE_ZERO 1); 
-by (Simp_tac 1); 
-qed "HCOMPLEX_DIVIDE_ZERO";
-
-Goal "inverse (x::hcomplex) = 1/x";
-by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); 
-qed "hcomplex_inverse_eq_divide";
-
-Goal "(inverse(x::hcomplex) = 0) = (x = 0)";
-by (Simp_tac 1);
-qed "hcomplex_inverse_zero_iff";
-Addsimps [hcomplex_inverse_zero_iff];
-
-Goal "(x/y = 0) = (x=0 | y=(0::hcomplex))";
-by (auto_tac (claset(), simpset() addsimps [hcomplex_divide_def]));  
-qed "hcomplex_divide_eq_0_iff";
-Addsimps [hcomplex_divide_eq_0_iff];
-
-Goal "h ~= (0::hcomplex) ==> h/h = 1";
-by (asm_simp_tac 
-    (simpset() addsimps [hcomplex_divide_def]) 1);
-qed "hcomplex_divide_self_eq"; 
-Addsimps [hcomplex_divide_self_eq];
-
-bind_thm ("hcomplex_mult_minus_right", hcomplex_minus_mult_eq2 RS sym);
-
-Goal "!!k::hcomplex. (k*m = k*n) = (k = 0 | m=n)";
-by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [hcomplex_mult_left_cancel]));  
-qed "hcomplex_mult_eq_cancel1";
-
-Goal "!!k::hcomplex. (m*k = n*k) = (k = 0 | m=n)";
-by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [hcomplex_mult_right_cancel]));  
-qed "hcomplex_mult_eq_cancel2";
-
-Goal "!!k::hcomplex. k~=0 ==> (k*m) / (k*n) = (m/n)";
-by (asm_simp_tac
-    (simpset() addsimps [hcomplex_divide_def, inverse_mult_distrib]) 1); 
-by (subgoal_tac "k * m * (inverse k * inverse n) = \
-\                (k * inverse k) * (m * inverse n)" 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (HOL_ss addsimps hcomplex_mult_ac) 1); 
-qed "hcomplex_mult_div_cancel1";
-
-(*For ExtractCommonTerm*)
-Goal "(k*m) / (k*n) = (if k = (0::hcomplex) then 0 else m/n)";
-by (simp_tac (simpset() addsimps [hcomplex_mult_div_cancel1]) 1); 
-qed "hcomplex_mult_div_cancel_disj";
-
-
-local
-  open HComplex_Numeral_Simprocs
-in
-
-val rel_hcomplex_number_of = [eq_hcomplex_number_of];
-
-
-structure CancelNumeralFactorCommon =
-  struct
-  val mk_coeff		= mk_coeff
-  val dest_coeff	= dest_coeff 1
-  val trans_tac         = Real_Numeral_Simprocs.trans_tac
-  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps @ mult_1s))
-                 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps))
-                 THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_mult_ac))
-  val numeral_simp_tac	= 
-         ALLGOALS (simp_tac (HOL_ss addsimps rel_hcomplex_number_of@bin_simps))
-  val simplify_meta_eq  = simplify_meta_eq
-  end
-
-
-structure DivCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "HOL.divide"
-  val dest_bal = HOLogic.dest_bin "HOL.divide" hcomplexT
-  val cancel = hcomplex_mult_div_cancel1 RS trans
-  val neg_exchanges = false
-)
-
-
-structure EqCancelNumeralFactor = CancelNumeralFactorFun
- (open CancelNumeralFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" hcomplexT
-  val cancel = hcomplex_mult_eq_cancel1 RS trans
-  val neg_exchanges = false
-)
-
-
-val hcomplex_cancel_numeral_factors_relations = 
-  map prep_simproc
-   [("hcomplexeq_cancel_numeral_factor",
-    ["(l::hcomplex) * m = n", "(l::hcomplex) = m * n"], 
-     EqCancelNumeralFactor.proc)];
-
-val hcomplex_cancel_numeral_factors_divide = prep_simproc
-	("hcomplexdiv_cancel_numeral_factor", 
-	 ["((l::hcomplex) * m) / n", "(l::hcomplex) / (m * n)", 
-                     "((number_of v)::hcomplex) / (number_of w)"], 
-	 DivCancelNumeralFactor.proc);
-
-val hcomplex_cancel_numeral_factors = 
-    hcomplex_cancel_numeral_factors_relations @ 
-    [hcomplex_cancel_numeral_factors_divide];
-
-end;
-
-
-Addsimprocs hcomplex_cancel_numeral_factors;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1)); 
-
-
-test "#9*x = #12 * (y::hcomplex)";
-test "(#9*x) / (#12 * (y::hcomplex)) = z";
-
-test "#-99*x = #132 * (y::hcomplex)";
-
-test "#999*x = #-396 * (y::hcomplex)";
-test "(#999*x) / (#-396 * (y::hcomplex)) = z";
-
-test "#-99*x = #-81 * (y::hcomplex)";
-test "(#-99*x) / (#-81 * (y::hcomplex)) = z";
-
-test "#-2 * x = #-1 * (y::hcomplex)";
-test "#-2 * x = -(y::hcomplex)";
-test "(#-2 * x) / (#-1 * (y::hcomplex)) = z";
-
-*)
-
-
-(** Declarations for ExtractCommonTerm **)
-
-local
-  open HComplex_Numeral_Simprocs
-in
-
-structure CancelFactorCommon =
-  struct
-  val mk_sum    	= long_mk_prod
-  val dest_sum		= dest_prod
-  val mk_coeff		= mk_coeff
-  val dest_coeff	= dest_coeff
-  val find_first	= find_first []
-  val trans_tac         = Real_Numeral_Simprocs.trans_tac
-  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hcomplex_mult_ac))
-  end;
-
-
-structure EqCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" hcomplexT
-  val simplify_meta_eq  = cancel_simplify_meta_eq hcomplex_mult_eq_cancel1
-);
-
-
-structure DivideCancelFactor = ExtractCommonTermFun
- (open CancelFactorCommon
-  val prove_conv = Bin_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binop "HOL.divide"
-  val dest_bal = HOLogic.dest_bin "HOL.divide" hcomplexT
-  val simplify_meta_eq  = cancel_simplify_meta_eq hcomplex_mult_div_cancel_disj
-);
-
-val hcomplex_cancel_factor = 
-  map prep_simproc
-   [("hcomplex_eq_cancel_factor", ["(l::hcomplex) * m = n", "(l::hcomplex) = m * n"], 
-     EqCancelFactor.proc),
-    ("hcomplex_divide_cancel_factor", ["((l::hcomplex) * m) / n", "(l::hcomplex) / (m * n)"], 
-     DivideCancelFactor.proc)];
-
-end;
-
-Addsimprocs hcomplex_cancel_factor;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Asm_simp_tac 1)); 
-
-test "x*k = k*(y::hcomplex)";
-test "k = k*(y::hcomplex)"; 
-test "a*(b*c) = (b::hcomplex)";
-test "a*(b*c) = d*(b::hcomplex)*(x*a)";
-
-
-test "(x*k) / (k*(y::hcomplex)) = (uu::hcomplex)";
-test "(k) / (k*(y::hcomplex)) = (uu::hcomplex)"; 
-test "(a*(b*c)) / ((b::hcomplex)) = (uu::hcomplex)";
-test "(a*(b*c)) / (d*(b::hcomplex)*(x*a)) = (uu::hcomplex)";
-
-(*FIXME: what do we do about this?*)
-test "a*(b*c)/(y*z) = d*(b::hcomplex)*(x*a)/z";
-*)
-
-
-Goal "z~=0 ==> ((x::hcomplex) = y/z) = (x*z = y)";
-by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_mult_assoc]) 2); 
-by (etac ssubst 1);
-by (stac hcomplex_mult_eq_cancel2 1); 
-by (Asm_simp_tac 1); 
-qed "hcomplex_eq_divide_eq";
-Addsimps [inst "z" "number_of ?w" hcomplex_eq_divide_eq];
-
-Goal "z~=0 ==> (y/z = (x::hcomplex)) = (y = x*z)";
-by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_mult_assoc]) 2); 
-by (etac ssubst 1);
-by (stac hcomplex_mult_eq_cancel2 1); 
-by (Asm_simp_tac 1); 
-qed "hcomplex_divide_eq_eq";
-Addsimps [inst "z" "number_of ?w" hcomplex_divide_eq_eq];
-
-Goal "(m/k = n/k) = (k = 0 | m = (n::hcomplex))";
-by (case_tac "k=0" 1);
-by (asm_simp_tac (simpset() addsimps [HCOMPLEX_DIVIDE_ZERO]) 1); 
-by (asm_simp_tac (simpset() addsimps [hcomplex_divide_eq_eq, hcomplex_eq_divide_eq, 
-                                      hcomplex_mult_eq_cancel2]) 1); 
-qed "hcomplex_divide_eq_cancel2";
-
-Goal "(k/m = k/n) = (k = 0 | m = (n::hcomplex))";
-by (case_tac "m=0 | n = 0" 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [HCOMPLEX_DIVIDE_ZERO, hcomplex_divide_eq_eq, 
-                                  hcomplex_eq_divide_eq, hcomplex_mult_eq_cancel1]));  
-qed "hcomplex_divide_eq_cancel1";
-
-(** Division by 1, -1 **)
-
-Goal "(x::hcomplex)/1 = x";
-by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); 
-qed "hcomplex_divide_1";
-Addsimps [hcomplex_divide_1];
-
-Goal "x/-1 = -(x::hcomplex)";
-by (Simp_tac 1); 
-qed "hcomplex_divide_minus1";
-Addsimps [hcomplex_divide_minus1];
-
-Goal "-1/(x::hcomplex) = - (1/x)";
-by (simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_minus_inverse]) 1); 
-qed "hcomplex_minus1_divide";
-Addsimps [hcomplex_minus1_divide];
-
-
-Goal "(x = - y) = (y = - (x::hcomplex))";
-by Auto_tac;
-qed "hcomplex_equation_minus";
-
-Goal "(- x = y) = (- (y::hcomplex) = x)";
-by Auto_tac;
-qed "hcomplex_minus_equation";
-
-Goal "(x + - a = (0::hcomplex)) = (x=a)";
-by (simp_tac (simpset() addsimps [hcomplex_diff_eq_eq,symmetric hcomplex_diff_def]) 1);
-qed "hcomplex_add_minus_iff";
-Addsimps [hcomplex_add_minus_iff];
-
-Goal "(-b = -a) = (b = (a::hcomplex))";
-by Auto_tac;
-qed "hcomplex_minus_eq_cancel";
-Addsimps [hcomplex_minus_eq_cancel];
-
-(*Distributive laws for literals*)
-Addsimps (map (inst "w" "number_of ?v")
-	  [hcomplex_add_mult_distrib, hcomplex_add_mult_distrib2,
-	   hcomplex_diff_mult_distrib, hcomplex_diff_mult_distrib2]);
-
-Addsimps [inst "x" "number_of ?v" hcomplex_equation_minus];
-
-Addsimps [inst "y" "number_of ?v" hcomplex_minus_equation];
-
-Goal "(x+y = (0::hcomplex)) = (y = -x)";
-by Auto_tac;
-by (dtac (sym RS (hcomplex_diff_eq_eq RS iffD2)) 1);
-by Auto_tac;  
-qed "hcomplex_add_eq_0_iff";
-AddIffs [hcomplex_add_eq_0_iff];
-
-Goalw [hcomplex_diff_def]"-(x-y) = y - (x::hcomplex)";
-by (auto_tac (claset(),simpset() addsimps [hcomplex_add_commute]));
-qed "hcomplex_minus_diff_eq";
-Addsimps [hcomplex_minus_diff_eq];
-
-Addsimps [inst "x" "number_of ?w" hcomplex_inverse_eq_divide];
-
-Goal "[|(x::hcomplex) ~= 0;  y ~= 0 |]  \
-\     ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)";
-by (asm_full_simp_tac (simpset() addsimps [inverse_mult_distrib,
-                    hcomplex_add_mult_distrib,hcomplex_mult_assoc RS sym]) 1);
-qed "hcomplex_inverse_add";
-
-Addsimps [hcomplex_of_complex_zero,hcomplex_of_complex_one];

--- a/src/HOL/Complex/NSComplexArith0.thy	Tue Dec 23 14:45:23 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-NSComplexArith0 = NSComplexBin
-
-
-

--- a/src/HOL/Complex/NSComplexBin.ML	Tue Dec 23 14:45:23 2003 +0100
+++ b/src/HOL/Complex/NSComplexBin.ML	Tue Dec 23 14:45:47 2003 +0100
@@ -24,11 +24,11 @@
 qed "hcomplex_hypreal_number_of";
 
 Goalw [hcomplex_number_of_def] "Numeral0 = (0::hcomplex)";
-by (simp_tac (simpset() addsimps [hcomplex_of_complex_zero RS sym]) 1);
+by(Simp_tac 1);
 qed "hcomplex_numeral_0_eq_0";
 
 Goalw [hcomplex_number_of_def] "Numeral1 = (1::hcomplex)";
-by (simp_tac (simpset() addsimps [hcomplex_of_complex_one RS sym]) 1);
+by(Simp_tac 1);
 qed "hcomplex_numeral_1_eq_1";
 
 (*

--- a/src/HOL/IsaMakefile	Tue Dec 23 14:45:23 2003 +0100
+++ b/src/HOL/IsaMakefile	Tue Dec 23 14:45:47 2003 +0100
@@ -174,7 +174,7 @@
   Complex/ComplexBin.ML Complex/ComplexBin.thy\
   Complex/NSCA.ML Complex/NSCA.thy\
   Complex/NSComplex.thy\
-  Complex/NSComplexArith0.ML Complex/NSComplexArith0.thy\
+  Complex/hcomplex_arith.ML Complex/NSComplexArith.thy\
   Complex/NSComplexBin.ML Complex/NSComplexBin.thy
 	@cd Complex; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Complex