src/HOL/Real/Hyperreal/HyperDef.ML

 qed "FreeUltrafilterNat_Compl";
 
 Goal "X~: FreeUltrafilterNat ==> -X : FreeUltrafilterNat";
 by (cut_facts_tac [FreeUltrafilterNat_mem RS (FreeUltrafilter_iff RS iffD1)] 1);
 by (Step_tac 1 THEN dres_inst_tac [("x","X")] bspec 1);
-by (auto_tac (claset(),simpset() addsimps [UNIV_diff_Compl]));
+by (auto_tac (claset(), simpset() addsimps [UNIV_diff_Compl]));
 qed "FreeUltrafilterNat_Compl_mem";
 
 Goal "(X ~: FreeUltrafilterNat) = (-X: FreeUltrafilterNat)";
 by (blast_tac (claset() addDs [FreeUltrafilterNat_Compl,
 			       FreeUltrafilterNat_Compl_mem]) 1);

 by (rtac ccontr 1 THEN rotate_tac 1 1);
 by (Asm_full_simp_tac 1);
 qed "FreeUltrafilterNat_Ex_P";
 
 Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat";
-by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set],simpset()));
+by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set], simpset()));
 qed "FreeUltrafilterNat_all";
 
 (*-------------------------------------------------------
      Define and use Ultrafilter tactics
  -------------------------------------------------------*)

 
 AddSIs [hyprelI];
 AddSEs [hyprelE];
 
 Goalw [hyprel_def] "(x,x): hyprel";
-by (auto_tac (claset(),simpset() addsimps 
-         [FreeUltrafilterNat_Nat_set]));
+by (auto_tac (claset(),
+              simpset() addsimps [FreeUltrafilterNat_Nat_set]));
 qed "hyprel_refl";
 
 Goal "{n. X n = Y n} = {n. Y n = X n}";
 by Auto_tac;
 qed "lemma_perm";
 
 Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel";
-by (auto_tac (claset() addIs [lemma_perm RS subst],simpset()));
+by (auto_tac (claset() addIs [lemma_perm RS subst], simpset()));
 qed_spec_mp "hyprel_sym";
 
 Goalw [hyprel_def]
       "(x,y): hyprel --> (y,z):hyprel --> (x,z):hyprel";
 by Auto_tac;

 by (rtac Rep_hypreal_inverse 1);
 qed "inj_Rep_hypreal";
 
 Goalw [hyprel_def] "x: hyprel ^^ {x}";
 by (Step_tac 1);
-by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
+by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
 qed "lemma_hyprel_refl";
 
 Addsimps [lemma_hyprel_refl];
 
 Goalw [hypreal_def] "{} ~: hypreal";

 by Safe_tac;
 by (ALLGOALS Ultra_tac);
 qed "hypreal_minus_congruent";
 
 Goalw [hypreal_minus_def]
-      "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})";
+   "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
-   [hyprel_in_hypreal RS Abs_hypreal_inverse,
-    [equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1);
+      [hyprel_in_hypreal RS Abs_hypreal_inverse,
+       [equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1);
 qed "hypreal_minus";
 
 Goal "- (- z) = (z::hypreal)";
 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
 by (asm_simp_tac (simpset() addsimps [hypreal_minus]) 1);

 qed "inj_hypreal_minus";
 
 Goalw [hypreal_zero_def] "-0 = (0::hypreal)";
 by (simp_tac (simpset() addsimps [hypreal_minus]) 1);
 qed "hypreal_minus_zero";
-
 Addsimps [hypreal_minus_zero];
 
 Goal "(-x = 0) = (x = (0::hypreal))"; 
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
-    hypreal_minus] @ real_add_ac));
+by (auto_tac (claset(),
+       simpset() addsimps [hypreal_zero_def, hypreal_minus, eq_commute] @ 
+                          real_add_ac));
 qed "hypreal_minus_zero_iff";
 
 Addsimps [hypreal_minus_zero_iff];
+
+
+(**** hyperreal addition: hypreal_add  ****)
+
+Goalw [congruent2_def]
+    "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})";
+by Safe_tac;
+by (ALLGOALS(Ultra_tac));
+qed "hypreal_add_congruent2";
+
+Goalw [hypreal_add_def]
+  "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \
+\  Abs_hypreal(hyprel^^{%n. X n + Y n})";
+by (simp_tac (simpset() addsimps 
+         [[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1);
+qed "hypreal_add";
+
+Goal "(z::hypreal) + w = w + z";
+by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
+by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1);
+qed "hypreal_add_commute";
+
+Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)";
+by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
+by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1);
+qed "hypreal_add_assoc";
+
+(*For AC rewriting*)
+Goal "(x::hypreal)+(y+z)=y+(x+z)";
+by (rtac (hypreal_add_commute RS trans) 1);
+by (rtac (hypreal_add_assoc RS trans) 1);
+by (rtac (hypreal_add_commute RS arg_cong) 1);
+qed "hypreal_add_left_commute";
+
+(* hypreal addition is an AC operator *)
+bind_thms ("hypreal_add_ac", [hypreal_add_assoc,hypreal_add_commute,
+                      hypreal_add_left_commute]);
+
+Goalw [hypreal_zero_def] "(0::hypreal) + z = z";
+by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
+by (asm_full_simp_tac (simpset() addsimps 
+    [hypreal_add]) 1);
+qed "hypreal_add_zero_left";
+
+Goal "z + (0::hypreal) = z";
+by (simp_tac (simpset() addsimps 
+    [hypreal_add_zero_left,hypreal_add_commute]) 1);
+qed "hypreal_add_zero_right";
+
+Goalw [hypreal_zero_def] "z + -z = (0::hypreal)";
+by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_minus, hypreal_add]) 1);
+qed "hypreal_add_minus";
+
+Goal "-z + z = (0::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_add_commute, hypreal_add_minus]) 1);
+qed "hypreal_add_minus_left";
+
+Addsimps [hypreal_add_minus,hypreal_add_minus_left,
+          hypreal_add_zero_left,hypreal_add_zero_right];
+
+Goal "EX y. (x::hypreal) + y = 0";
+by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
+qed "hypreal_minus_ex";
+
+Goal "EX! y. (x::hypreal) + y = 0";
+by (auto_tac (claset() addIs [hypreal_add_minus], simpset()));
+by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
+qed "hypreal_minus_ex1";
+
+Goal "EX! y. y + (x::hypreal) = 0";
+by (auto_tac (claset() addIs [hypreal_add_minus_left], simpset()));
+by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
+qed "hypreal_minus_left_ex1";
+
+Goal "x + y = (0::hypreal) ==> x = -y";
+by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
+by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
+by (Blast_tac 1);
+qed "hypreal_add_minus_eq_minus";
+
+Goal "EX y::hypreal. x = -y";
+by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
+by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
+by (Fast_tac 1);
+qed "hypreal_as_add_inverse_ex";
+
+Goal "-(x + (y::hypreal)) = -x + -y";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),
+              simpset() addsimps [hypreal_minus, hypreal_add,
+                                  real_minus_add_distrib]));
+qed "hypreal_minus_add_distrib";
+Addsimps [hypreal_minus_add_distrib];
+
+Goal "-(y + -(x::hypreal)) = x + -y";
+by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
+qed "hypreal_minus_distrib1";
+
+Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
+by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1);
+by (simp_tac (simpset() addsimps [hypreal_add_left_commute,
+                                  hypreal_add_assoc]) 1);
+by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
+qed "hypreal_add_minus_cancel1";
+
+Goal "((x::hypreal) + y = x + z) = (y = z)";
+by (Step_tac 1);
+by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
+qed "hypreal_add_left_cancel";
+
+Goal "z + (x + (y + -z)) = x + (y::hypreal)";
+by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
+qed "hypreal_add_minus_cancel2";
+Addsimps [hypreal_add_minus_cancel2];
+
+Goal "y + -(x + y) = -(x::hypreal)";
+by (Full_simp_tac 1);
+by (rtac (hypreal_add_left_commute RS subst) 1);
+by (Full_simp_tac 1);
+qed "hypreal_add_minus_cancel";
+Addsimps [hypreal_add_minus_cancel];
+
+Goal "y + -(y + x) = -(x::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
+qed "hypreal_add_minus_cancelc";
+Addsimps [hypreal_add_minus_cancelc];
+
+Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
+by (full_simp_tac
+    (simpset() addsimps [hypreal_minus_add_distrib RS sym, 
+                         hypreal_add_left_cancel] @ hypreal_add_ac 
+               delsimps [hypreal_minus_add_distrib]) 1); 
+qed "hypreal_add_minus_cancel3";
+Addsimps [hypreal_add_minus_cancel3];
+
+Goal "(y + (x::hypreal)= z + x) = (y = z)";
+by (simp_tac (simpset() addsimps [hypreal_add_commute,
+                                  hypreal_add_left_cancel]) 1);
+qed "hypreal_add_right_cancel";
+
+Goal "z + (y + -z) = (y::hypreal)";
+by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
+qed "hypreal_add_minus_cancel4";
+Addsimps [hypreal_add_minus_cancel4];
+
+Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)";
+by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
+qed "hypreal_add_minus_cancel5";
+Addsimps [hypreal_add_minus_cancel5];
+
+Goal "z + ((- z) + w) = (w::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
+qed "hypreal_add_minus_cancelA";
+
+Goal "(-z) + (z + w) = (w::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
+qed "hypreal_minus_add_cancelA";
+
+Addsimps [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA];
+
+(**** hyperreal multiplication: hypreal_mult  ****)
+
+Goalw [congruent2_def]
+    "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})";
+by Safe_tac;
+by (ALLGOALS(Ultra_tac));
+qed "hypreal_mult_congruent2";
+
+Goalw [hypreal_mult_def]
+  "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \
+\  Abs_hypreal(hyprel^^{%n. X n * Y n})";
+by (simp_tac (simpset() addsimps 
+      [[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1);
+qed "hypreal_mult";
+
+Goal "(z::hypreal) * w = w * z";
+by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
+by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1);
+qed "hypreal_mult_commute";
+
+Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)";
+by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
+by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
+qed "hypreal_mult_assoc";
+
+qed_goal "hypreal_mult_left_commute" (the_context ())
+    "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
+ (fn _ => [rtac (hypreal_mult_commute RS trans) 1, 
+           rtac (hypreal_mult_assoc RS trans) 1,
+           rtac (hypreal_mult_commute RS arg_cong) 1]);
+
+(* hypreal multiplication is an AC operator *)
+bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute, 
+                       hypreal_mult_left_commute]);
+
+Goalw [hypreal_one_def] "1hr * z = z";
+by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
+qed "hypreal_mult_1";
+
+Goal "z * 1hr = z";
+by (simp_tac (simpset() addsimps [hypreal_mult_commute,
+    hypreal_mult_1]) 1);
+qed "hypreal_mult_1_right";
+
+Goalw [hypreal_zero_def] "0 * z = (0::hypreal)";
+by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1);
+qed "hypreal_mult_0";
+
+Goal "z * 0 = (0::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_mult_commute, hypreal_mult_0]) 1);
+qed "hypreal_mult_0_right";
+
+Addsimps [hypreal_mult_0,hypreal_mult_0_right];
+
+Goal "-(x * y) = -x * (y::hypreal)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [hypreal_minus, hypreal_mult] 
+                                 @ real_mult_ac @ real_add_ac));
+qed "hypreal_minus_mult_eq1";
+
+Goal "-(x * y) = (x::hypreal) * -y";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_mult] 
+                                           @ real_mult_ac @ real_add_ac));
+qed "hypreal_minus_mult_eq2";
+
+(*Pull negations out*)
+Addsimps [hypreal_minus_mult_eq2 RS sym, hypreal_minus_mult_eq1 RS sym];
+
+Goal "-x*y = (x::hypreal)*-y";
+by Auto_tac;
+qed "hypreal_minus_mult_commute";
+
+(*-----------------------------------------------------------------------------
+    A few more theorems
+ ----------------------------------------------------------------------------*)
+Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
+by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
+qed "hypreal_add_assoc_cong";
+
+Goal "(z::hypreal) + (v + w) = v + (z + w)";
+by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1));
+qed "hypreal_add_assoc_swap";
+
+Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)";
+by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
+by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add,
+     real_add_mult_distrib]) 1);
+qed "hypreal_add_mult_distrib";
+
+val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute;
+
+Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)";
+by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
+qed "hypreal_add_mult_distrib2";
+
+bind_thms ("hypreal_mult_simps", [hypreal_mult_1, hypreal_mult_1_right]);
+Addsimps hypreal_mult_simps;
+
+(* 07/00 *)
+
+Goalw [hypreal_diff_def] "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)";
+by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1);
+qed "hypreal_diff_mult_distrib";
+
+Goal "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)";
+by (simp_tac (simpset() addsimps [hypreal_mult_commute', 
+				  hypreal_diff_mult_distrib]) 1);
+qed "hypreal_diff_mult_distrib2";
+
+(*** one and zero are distinct ***)
+Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr";
+by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one]));
+qed "hypreal_zero_not_eq_one";
+
+
 (**** multiplicative inverse on hypreal ****)
 
 Goalw [congruent_def]
   "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else inverse(X n)})";
 by (Auto_tac THEN Ultra_tac 1);

 by (simp_tac (simpset() addsimps 
    [hyprel_in_hypreal RS Abs_hypreal_inverse,
     [equiv_hyprel, hypreal_inverse_congruent] MRS UN_equiv_class]) 1);
 qed "hypreal_inverse";
 
-Goal "z ~= 0 ==> inverse (inverse (z::hypreal)) = z";
+Goal "inverse 0 = (0::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_inverse, hypreal_zero_def]) 1);
+qed "HYPREAL_INVERSE_ZERO";
+
+Goal "a / (0::hypreal) = 0";
+by (simp_tac
+    (simpset() addsimps [hypreal_divide_def, HYPREAL_INVERSE_ZERO]) 1);
+qed "HYPREAL_DIVISION_BY_ZERO";  (*NOT for adding to default simpset*)
+
+fun hypreal_div_undefined_case_tac s i =
+  case_tac s i THEN 
+  asm_simp_tac 
+       (simpset() addsimps [HYPREAL_DIVISION_BY_ZERO, HYPREAL_INVERSE_ZERO]) i;
+
+Goal "inverse (inverse (z::hypreal)) = z";
+by (hypreal_div_undefined_case_tac "z=0" 1);
 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (rotate_tac 1 1);
 by (asm_full_simp_tac (simpset() addsimps 
-    [hypreal_inverse,hypreal_zero_def] addsplits [split_if]) 1);
-by (ultra_tac (claset() addDs (map rename_numerals [real_inverse_not_zero]),
-	       simpset() addsimps [real_inverse_inverse]) 1);
+                       [hypreal_inverse, hypreal_zero_def]) 1);
 qed "hypreal_inverse_inverse";
-
 Addsimps [hypreal_inverse_inverse];
 
 Goalw [hypreal_one_def] "inverse(1hr) = 1hr";
 by (full_simp_tac (simpset() addsimps [hypreal_inverse,
                                        real_zero_not_eq_one RS not_sym]) 1);
 qed "hypreal_inverse_1";
 Addsimps [hypreal_inverse_1];
 
-(**** hyperreal addition: hypreal_add  ****)
-
-Goalw [congruent2_def]
-    "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})";
-by Safe_tac;
-by (ALLGOALS(Ultra_tac));
-qed "hypreal_add_congruent2";
-
-Goalw [hypreal_add_def]
-  "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \
-\  Abs_hypreal(hyprel^^{%n. X n + Y n})";
-by (simp_tac (simpset() addsimps 
-         [[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1);
-qed "hypreal_add";
-
-Goal "(z::hypreal) + w = w + z";
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
-by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1);
-qed "hypreal_add_commute";
-
-Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1);
-qed "hypreal_add_assoc";
-
-(*For AC rewriting*)
-Goal "(x::hypreal)+(y+z)=y+(x+z)";
-by (rtac (hypreal_add_commute RS trans) 1);
-by (rtac (hypreal_add_assoc RS trans) 1);
-by (rtac (hypreal_add_commute RS arg_cong) 1);
-qed "hypreal_add_left_commute";
-
-(* hypreal addition is an AC operator *)
-bind_thms ("hypreal_add_ac", [hypreal_add_assoc,hypreal_add_commute,
-                      hypreal_add_left_commute]);
-
-Goalw [hypreal_zero_def] "(0::hypreal) + z = z";
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (asm_full_simp_tac (simpset() addsimps 
-    [hypreal_add]) 1);
-qed "hypreal_add_zero_left";
-
-Goal "z + (0::hypreal) = z";
-by (simp_tac (simpset() addsimps 
-    [hypreal_add_zero_left,hypreal_add_commute]) 1);
-qed "hypreal_add_zero_right";
-
-Goalw [hypreal_zero_def] "z + -z = (0::hypreal)";
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_minus, hypreal_add]) 1);
-qed "hypreal_add_minus";
-
-Goal "-z + z = (0::hypreal)";
-by (simp_tac (simpset() addsimps [hypreal_add_commute, hypreal_add_minus]) 1);
-qed "hypreal_add_minus_left";
-
-Addsimps [hypreal_add_minus,hypreal_add_minus_left,
-          hypreal_add_zero_left,hypreal_add_zero_right];
-
-Goal "EX y. (x::hypreal) + y = 0";
-by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
-qed "hypreal_minus_ex";
-
-Goal "EX! y. (x::hypreal) + y = 0";
-by (auto_tac (claset() addIs [hypreal_add_minus],simpset()));
-by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "hypreal_minus_ex1";
-
-Goal "EX! y. y + (x::hypreal) = 0";
-by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset()));
-by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "hypreal_minus_left_ex1";
-
-Goal "x + y = (0::hypreal) ==> x = -y";
-by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
-by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
-by (Blast_tac 1);
-qed "hypreal_add_minus_eq_minus";
-
-Goal "EX y::hypreal. x = -y";
-by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
-by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
-by (Fast_tac 1);
-qed "hypreal_as_add_inverse_ex";
-
-Goal "-(x + (y::hypreal)) = -x + -y";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
-              simpset() addsimps [hypreal_minus, hypreal_add,
-                                  real_minus_add_distrib]));
-qed "hypreal_minus_add_distrib";
-Addsimps [hypreal_minus_add_distrib];
-
-Goal "-(y + -(x::hypreal)) = x + -y";
-by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "hypreal_minus_distrib1";
-
-Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
-by (res_inst_tac [("w1","y")] (hypreal_add_commute RS subst) 1);
-by (simp_tac (simpset() addsimps [hypreal_add_left_commute,
-                                  hypreal_add_assoc]) 1);
-by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "hypreal_add_minus_cancel1";
-
-Goal "((x::hypreal) + y = x + z) = (y = z)";
-by (Step_tac 1);
-by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
-qed "hypreal_add_left_cancel";
-
-Goal "z + (x + (y + -z)) = x + (y::hypreal)";
-by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
-qed "hypreal_add_minus_cancel2";
-Addsimps [hypreal_add_minus_cancel2];
-
-Goal "y + -(x + y) = -(x::hypreal)";
-by (Full_simp_tac 1);
-by (rtac (hypreal_add_left_commute RS subst) 1);
-by (Full_simp_tac 1);
-qed "hypreal_add_minus_cancel";
-Addsimps [hypreal_add_minus_cancel];
-
-Goal "y + -(y + x) = -(x::hypreal)";
-by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
-qed "hypreal_add_minus_cancelc";
-Addsimps [hypreal_add_minus_cancelc];
-
-Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
-by (full_simp_tac
-    (simpset() addsimps [hypreal_minus_add_distrib RS sym, 
-                         hypreal_add_left_cancel] @ hypreal_add_ac 
-               delsimps [hypreal_minus_add_distrib]) 1); 
-qed "hypreal_add_minus_cancel3";
-Addsimps [hypreal_add_minus_cancel3];
-
-Goal "(y + (x::hypreal)= z + x) = (y = z)";
-by (simp_tac (simpset() addsimps [hypreal_add_commute,
-                                  hypreal_add_left_cancel]) 1);
-qed "hypreal_add_right_cancel";
-
-Goal "z + (y + -z) = (y::hypreal)";
-by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
-qed "hypreal_add_minus_cancel4";
-Addsimps [hypreal_add_minus_cancel4];
-
-Goal "z + (w + (x + (-z + y))) = w + x + (y::hypreal)";
-by (simp_tac (simpset() addsimps hypreal_add_ac) 1);
-qed "hypreal_add_minus_cancel5";
-Addsimps [hypreal_add_minus_cancel5];
-
-Goal "z + ((- z) + w) = (w::hypreal)";
-by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
-qed "hypreal_add_minus_cancelA";
-
-Goal "(-z) + (z + w) = (w::hypreal)";
-by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
-qed "hypreal_minus_add_cancelA";
-
-Addsimps [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA];
-
-(**** hyperreal multiplication: hypreal_mult  ****)
-
-Goalw [congruent2_def]
-    "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})";
-by Safe_tac;
-by (ALLGOALS(Ultra_tac));
-qed "hypreal_mult_congruent2";
-
-Goalw [hypreal_mult_def]
-  "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \
-\  Abs_hypreal(hyprel^^{%n. X n * Y n})";
-by (simp_tac (simpset() addsimps 
-      [[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1);
-qed "hypreal_mult";
-
-Goal "(z::hypreal) * w = w * z";
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
-by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1);
-qed "hypreal_mult_commute";
-
-Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
-qed "hypreal_mult_assoc";
-
-qed_goal "hypreal_mult_left_commute" (the_context ())
-    "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
- (fn _ => [rtac (hypreal_mult_commute RS trans) 1, 
-           rtac (hypreal_mult_assoc RS trans) 1,
-           rtac (hypreal_mult_commute RS arg_cong) 1]);
-
-(* hypreal multiplication is an AC operator *)
-bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute, 
-                       hypreal_mult_left_commute]);
-
-Goalw [hypreal_one_def] "1hr * z = z";
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
-qed "hypreal_mult_1";
-
-Goal "z * 1hr = z";
-by (simp_tac (simpset() addsimps [hypreal_mult_commute,
-    hypreal_mult_1]) 1);
-qed "hypreal_mult_1_right";
-
-Goalw [hypreal_zero_def] "0 * z = (0::hypreal)";
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1);
-qed "hypreal_mult_0";
-
-Goal "z * 0 = (0::hypreal)";
-by (simp_tac (simpset() addsimps [hypreal_mult_commute,
-    hypreal_mult_0]) 1);
-qed "hypreal_mult_0_right";
-
-Addsimps [hypreal_mult_0,hypreal_mult_0_right];
-
-Goal "-(x * y) = -x * (y::hypreal)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [hypreal_minus, hypreal_mult] 
-                                 @ real_mult_ac @ real_add_ac));
-qed "hypreal_minus_mult_eq1";
-
-Goal "-(x * y) = (x::hypreal) * -y";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
-					   hypreal_mult] 
-                                           @ real_mult_ac @ real_add_ac));
-qed "hypreal_minus_mult_eq2";
-
-(*Pull negations out*)
-Addsimps [hypreal_minus_mult_eq2 RS sym, hypreal_minus_mult_eq1 RS sym];
-
-Goal "-x*y = (x::hypreal)*-y";
-by Auto_tac;
-qed "hypreal_minus_mult_commute";
-
-(*-----------------------------------------------------------------------------
-    A few more theorems
- ----------------------------------------------------------------------------*)
-Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
-by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
-qed "hypreal_add_assoc_cong";
-
-Goal "(z::hypreal) + (v + w) = v + (z + w)";
-by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1));
-qed "hypreal_add_assoc_swap";
-
-Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)";
-by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add,
-     real_add_mult_distrib]) 1);
-qed "hypreal_add_mult_distrib";
-
-val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute;
-
-Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)";
-by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
-qed "hypreal_add_mult_distrib2";
-
-bind_thms ("hypreal_mult_simps", [hypreal_mult_1, hypreal_mult_1_right]);
-Addsimps hypreal_mult_simps;
-
-(* 07/00 *)
-
-Goalw [hypreal_diff_def] "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)";
-by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1);
-qed "hypreal_diff_mult_distrib";
-
-Goal "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)";
-by (simp_tac (simpset() addsimps [hypreal_mult_commute', 
-				  hypreal_diff_mult_distrib]) 1);
-qed "hypreal_diff_mult_distrib2";
-
-(*** one and zero are distinct ***)
-Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr";
-by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
-qed "hypreal_zero_not_eq_one";
 
 (*** existence of inverse ***)
+
 Goalw [hypreal_one_def,hypreal_zero_def] 
-          "x ~= 0 ==> x*inverse(x) = 1hr";
+     "x ~= 0 ==> x*inverse(x) = 1hr";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse,
-    hypreal_mult] addsplits [split_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
 by (dtac FreeUltrafilterNat_Compl_mem 1);
 by (blast_tac (claset() addSIs [real_mult_inv_right,
     FreeUltrafilterNat_subset]) 1);
 qed "hypreal_mult_inverse";
 
 Goal "x ~= 0 ==> inverse(x)*x = 1hr";
 by (asm_simp_tac (simpset() addsimps [hypreal_mult_inverse,
 				      hypreal_mult_commute]) 1);
 qed "hypreal_mult_inverse_left";
-
-Goal "x ~= 0 ==> EX y. x * y = 1hr";
-by (fast_tac (claset() addDs [hypreal_mult_inverse]) 1);
-qed "hypreal_inverse_ex";
-
-Goal "x ~= 0 ==> EX y. y * x = 1hr";
-by (fast_tac (claset() addDs [hypreal_mult_inverse_left]) 1);
-qed "hypreal_inverse_left_ex";
-
-Goal "x ~= 0 ==> EX! y. x * y = 1hr";
-by (auto_tac (claset() addIs [hypreal_mult_inverse],simpset()));
-by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
-qed "hypreal_inverse_ex1";
-
-Goal "x ~= 0 ==> EX! y. y * x = 1hr";
-by (auto_tac (claset() addIs [hypreal_mult_inverse_left],simpset()));
-by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
-qed "hypreal_inverse_left_ex1";
-
-Goal "[| y~= 0; x * y = 1hr |]  ==> x = inverse y";
-by (forw_inst_tac [("x","y")] hypreal_mult_inverse_left 1);
-by (res_inst_tac [("x1","y")] (hypreal_inverse_left_ex1 RS ex1E) 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-qed "hypreal_mult_inv_inverse";
-
-Goal "x ~= 0 ==> EX y. x = inverse (y::hypreal)";
-by (forw_inst_tac [("x","x")] hypreal_inverse_left_ex 1);
-by (etac exE 1 THEN 
-    forw_inst_tac [("x","y")] hypreal_mult_inv_inverse 1);
-by (res_inst_tac [("x","y")] exI 2);
-by Auto_tac;
-qed "hypreal_as_inverse_ex";
 
 Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)";
 by Auto_tac;
 by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac)  1);

 by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac)  1);
 qed "hypreal_mult_right_cancel";
 
 Goalw [hypreal_zero_def] "x ~= 0 ==> inverse (x::hypreal) ~= 0";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse,
-    hypreal_mult] addsplits [split_if]) 1);
-by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
-by (ultra_tac (claset() addIs [ccontr]
-                        addDs [rename_numerals real_inverse_not_zero],
-	       simpset()) 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
 qed "hypreal_inverse_not_zero";
 
 Addsimps [hypreal_mult_inverse,hypreal_mult_inverse_left];
 
 Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::hypreal)";

 qed "hypreal_mult_not_0";
 
 bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
 
 Goal "x*y = (0::hypreal) ==> x = 0 | y = 0";
-by (auto_tac (claset() addIs [ccontr] addDs 
-    [hypreal_mult_not_0],simpset()));
+by (auto_tac (claset() addIs [ccontr] addDs [hypreal_mult_not_0],
+              simpset()));
 qed "hypreal_mult_zero_disj";
 
 Goal "x ~= 0 ==> x * x ~= (0::hypreal)";
 by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
 qed "hypreal_mult_self_not_zero";
 
 Goal "[| x ~= 0; y ~= 0 |] ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)";
 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
-    hypreal_mult_not_0]));
+by (auto_tac (claset(),
+        simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
 by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0]));
+by (auto_tac (claset(),
+        simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
+by (auto_tac (claset(),
+        simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
 qed "inverse_mult_eq";
 
-Goal "x ~= 0 ==> inverse(-x) = -inverse(x::hypreal)";
+Goal "inverse(-x) = -inverse(x::hypreal)";
+by (hypreal_div_undefined_case_tac "x=0" 1);
 by (rtac (hypreal_mult_right_cancel RS iffD1) 1);
 by (stac hypreal_mult_inverse_left 2);
 by Auto_tac;
 qed "hypreal_minus_inverse";
 
-Goal "[| x ~= 0; y ~= 0 |] \
-\     ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)";
+Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
+by (hypreal_div_undefined_case_tac "x=0" 1);
+by (hypreal_div_undefined_case_tac "y=0" 1);
 by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
 by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_mult_assoc RS sym]));
 by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_commute]));
 by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
 qed "hypreal_inverse_distrib";
 
 (*------------------------------------------------------------------
                    Theorems for ordering 

 by (Fast_tac 1);
 qed "hypreal_lessD";
 
 Goal "~ (R::hypreal) < R";
 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_less_def]));
 by (Ultra_tac 1);
 qed "hypreal_less_not_refl";
 
 (*** y < y ==> P ***)
 bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
 AddSEs [hypreal_less_irrefl];
 
 Goal "!!(x::hypreal). x < y ==> x ~= y";
-by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_less_not_refl]));
 qed "hypreal_not_refl2";
 
 Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
 by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSIs [exI],simpset() 
-     addsimps [hypreal_less_def]));
-by (ultra_tac (claset() addIs [real_less_trans],simpset()) 1);
+by (auto_tac (claset() addSIs [exI], simpset() addsimps [hypreal_less_def]));
+by (ultra_tac (claset() addIs [real_less_trans], simpset()) 1);
 qed "hypreal_less_trans";
 
 Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P";
 by (dtac hypreal_less_trans 1 THEN assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps 

  -------------------------------------------------------*)
 Goalw [hypreal_less_def]
       "(Abs_hypreal(hyprel^^{%n. X n}) < \
 \           Abs_hypreal(hyprel^^{%n. Y n})) = \
 \      ({n. X n < Y n} : FreeUltrafilterNat)";
-by (auto_tac (claset() addSIs [lemma_hyprel_refl],simpset()));
+by (auto_tac (claset() addSIs [lemma_hyprel_refl], simpset()));
 by (Ultra_tac 1);
 qed "hypreal_less";
 
 (*---------------------------------------------------------------------------------
              Hyperreals as a linearly ordered field

   --------------------------------------------------------------------------------*)
 
 Goalw [hyprel_def] "EX x. x: hyprel ^^ {%n. #0}";
 by (res_inst_tac [("x","%n. #0")] exI 1);
 by (Step_tac 1);
-by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
+by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
 qed "lemma_hyprel_0r_mem";
 
 Goalw [hypreal_zero_def]"0 <  x | x = 0 | x < (0::hypreal)";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));

 
 Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real  r";
 by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
 qed "hypreal_of_real_minus";
 
+(*DON'T insert this or the next one as default simprules.
+  They are used in both orientations and anyway aren't the ones we finally
+  need, which would use binary literals.*)
 Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  #1 = 1hr";
 by (Step_tac 1);
 qed "hypreal_of_real_one";
 
-Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  #0 = 0";
+Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real #0 = 0";
 by (Step_tac 1);
 qed "hypreal_of_real_zero";
 
-Goal "(hypreal_of_real  r = 0) = (r = #0)";
+Goal "(hypreal_of_real r = 0) = (r = #0)";
 by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
     simpset() addsimps [hypreal_of_real_def,
-    hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
+                        hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
 qed "hypreal_of_real_zero_iff";
 
-Goal "(hypreal_of_real  r ~= 0) = (r ~= #0)";
+(*FIXME: delete*)
+Goal "(hypreal_of_real r ~= 0) = (r ~= #0)";
 by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
 qed "hypreal_of_real_not_zero_iff";
 
-Goal "r ~= #0 ==> inverse (hypreal_of_real r) = \
-\          hypreal_of_real (inverse r)";
-by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
+Goal "inverse (hypreal_of_real r) = hypreal_of_real (inverse r)";
+by (case_tac "r=#0" 1);
+by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO, INVERSE_ZERO, 
+                              HYPREAL_INVERSE_ZERO, hypreal_of_real_zero]) 1);
+by (res_inst_tac [("c1","hypreal_of_real r")] 
+    (hypreal_mult_left_cancel RS iffD1) 1);
 by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
 by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one]));
+by (auto_tac (claset(),
+      simpset() addsimps [hypreal_of_real_one, hypreal_of_real_mult RS sym]));
 qed "hypreal_of_real_inverse";
-
-Goal "hypreal_of_real r ~= 0 ==> inverse (hypreal_of_real r) = \
-\          hypreal_of_real (inverse r)";
-by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_inverse) 1);
-qed "hypreal_of_real_inverse2";
 
 Goal "x+x=x*(1hr+1hr)";
 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
 qed "hypreal_add_self";
 
+(*FIXME: DELETE (used in Lim.ML) *)
 Goal "(z::hypreal) ~= 0 ==> x*y = (x*inverse(z))*(z*y)";
 by (asm_simp_tac (simpset() addsimps hypreal_mult_ac)  1);
 qed "lemma_chain";
 
 Goal "[|(x::hypreal) ~= 0; y ~= 0 |] ==> \