# HG changeset patch
# User paulson
# Date 1071136361 -3600
# Node ID 84fda1b3994719ca4e3f1caaa3e87f941f823861
# Parent  deb8e1e62002adf0d36fc15e2e60d68ee2ed47b3
removal of abel_cancel from Real

diff -r deb8e1e62002 -r 84fda1b39947 src/HOL/Complex/ComplexBin.ML
--- a/src/HOL/Complex/ComplexBin.ML	Wed Dec 10 16:47:50 2003 +0100
+++ b/src/HOL/Complex/ComplexBin.ML	Thu Dec 11 10:52:41 2003 +0100
@@ -427,10 +427,6 @@
 Addsimprocs Complex_Numeral_Simprocs.cancel_numerals;
 Addsimprocs [Complex_Numeral_Simprocs.combine_numerals];
 
-(*The Abel_Cancel simprocs are now obsolete
-Delsimprocs [Complex_Cancel.sum_conv, Complex_Cancel.rel_conv];
-*)
-
 (*examples:
 print_depth 22;
 set timing;
diff -r deb8e1e62002 -r 84fda1b39947 src/HOL/Integ/Int.thy
--- a/src/HOL/Integ/Int.thy	Wed Dec 10 16:47:50 2003 +0100
+++ b/src/HOL/Integ/Int.thy	Thu Dec 11 10:52:41 2003 +0100
@@ -235,7 +235,7 @@
 apply (simp_all (no_asm_simp))
 done
 
-lemma zle_iff_zadd: "(w \<le> z) = (EX n. z = w + int n)"
+lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
 by (force intro: exI [of _ "0::nat"] 
             intro!: not_sym [THEN not0_implies_Suc]
             simp add: zless_iff_Suc_zadd int_le_less)
@@ -321,44 +321,9 @@
  by (rule Ring_and_Field.mult_cancel_left)
 
 
-subsection{*For the @{text abel_cancel} Simproc (DELETE)*}
-
-(* Lemmas needed for the simprocs *)
-
-(** The idea is to cancel like terms on opposite sides by subtraction **)
-
-lemma zless_eqI: "(x::int) - y = x' - y' ==> (x<y) = (x'<y')"
-by (simp add: zless_def)
-
-lemma zle_eqI: "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')"
-apply (drule zless_eqI)
-apply (simp (no_asm_simp) add: zle_def)
-done
-
-lemma zeq_eqI: "(x::int) - y = x' - y' ==> (x=y) = (x'=y')"
-apply safe
-apply (simp_all add: eq_diff_eq diff_eq_eq)
-done
-
-(*Deletion of other terms in the formula, seeking the -x at the front of z*)
-lemma zadd_cancel_21: "((x::int) + (y + z) = y + u) = ((x + z) = u)"
-apply (subst zadd_left_commute)
-apply (rule zadd_left_cancel)
-done
-
-(*A further rule to deal with the case that
-  everything gets cancelled on the right.*)
-lemma zadd_cancel_end: "((x::int) + (y + z) = y) = (x = -z)"
-apply (subst zadd_left_commute)
-apply (rule_tac t = y in zadd_0_right [THEN subst], subst zadd_left_cancel)
-apply (simp add: eq_diff_eq [symmetric])
-done
-
-
-
 text{*A case theorem distinguishing non-negative and negative int*}
 
-lemma negD: "neg x ==> EX n. x = - (int (Suc n))"
+lemma negD: "neg x ==> \<exists>n. x = - (int (Suc n))"
 by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd 
                    diff_eq_eq [symmetric] zdiff_def)
 
@@ -376,10 +341,6 @@
 val zabs_def = thm "zabs_def"
 val nat_def  = thm "nat_def"
 
-val zless_eqI = thm "zless_eqI";
-val zle_eqI = thm "zle_eqI";
-val zeq_eqI = thm "zeq_eqI";
-
 val int_0 = thm "int_0";
 val int_1 = thm "int_1";
 val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
diff -r deb8e1e62002 -r 84fda1b39947 src/HOL/Real/RealArith.thy
--- a/src/HOL/Real/RealArith.thy	Wed Dec 10 16:47:50 2003 +0100
+++ b/src/HOL/Real/RealArith.thy	Thu Dec 11 10:52:41 2003 +0100
@@ -1,9 +1,6 @@
 theory RealArith = RealArith0
 files ("real_arith.ML"):
 
-lemma real_divide_1: "(x::real)/1 = x"
-by (simp add: real_divide_def)
-
 use "real_arith.ML"
 
 setup real_arith_setup
@@ -285,6 +282,7 @@
 done
 
 
+
 ML
 {*
 val real_0_le_divide_iff = thm"real_0_le_divide_iff";
diff -r deb8e1e62002 -r 84fda1b39947 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Wed Dec 10 16:47:50 2003 +0100
+++ b/src/HOL/Real/RealBin.ML	Thu Dec 11 10:52:41 2003 +0100
@@ -156,11 +156,11 @@
 (** Simplification of arithmetic when nested to the right **)
 
 Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::real)";
-by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [add_assoc RS sym]) 1); 
 qed "real_add_number_of_left";
 
 Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::real)";
-by (simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
+by (simp_tac (simpset() addsimps [mult_assoc RS sym]) 1);
 qed "real_mult_number_of_left";
 
 Goalw [real_diff_def]
@@ -171,7 +171,7 @@
 Goal "number_of v + (c - number_of w) = \
 \     number_of (bin_add v (bin_minus w)) + (c::real)";
 by (stac (diff_real_number_of RS sym) 1);
-by Auto_tac;
+by (asm_full_simp_tac (HOL_ss addsimps [real_diff_def]@add_ac) 1); 
 qed "real_add_number_of_diff2";
 
 Addsimps [real_add_number_of_left, real_mult_number_of_left,
@@ -206,7 +206,7 @@
 (** For combine_numerals **)
 
 Goal "i*u + (j*u + k) = (i+j)*u + (k::real)";
-by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib]) 1);
+by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib] @ add_ac) 1);
 qed "left_real_add_mult_distrib";
 
 
@@ -544,9 +544,6 @@
 Addsimprocs Real_Numeral_Simprocs.cancel_numerals;
 Addsimprocs [Real_Numeral_Simprocs.combine_numerals];
 
-(*The Abel_Cancel simprocs are now obsolete*)
-Delsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
-
 (*examples:
 print_depth 22;
 set timing;
diff -r deb8e1e62002 -r 84fda1b39947 src/HOL/Real/RealInt.thy
--- a/src/HOL/Real/RealInt.thy	Wed Dec 10 16:47:50 2003 +0100
+++ b/src/HOL/Real/RealInt.thy	Thu Dec 11 10:52:41 2003 +0100
@@ -85,7 +85,7 @@
 declare real_of_int_mult [symmetric, simp]
 
 lemma real_of_int_Suc: "real (int (Suc n)) = real (int n) + (1::real)"
-by (simp add: real_of_one [symmetric] zadd_int zadd_ac)
+by (simp add: real_of_one [symmetric] zadd_int add_ac)
 
 declare real_of_one [simp]
 
@@ -105,6 +105,10 @@
 lemma real_of_int_less_cancel: "real (x::int) < real y ==> x < y"
 apply (rule ccontr, drule linorder_not_less [THEN iffD1])
 apply (auto simp add: zle_iff_zadd real_of_int_add [symmetric] real_of_int_real_of_nat linorder_not_le [symmetric])
+apply (subgoal_tac "~ real y + 0 \<le> real y + real n") 
+ prefer 2 apply (simp add: ); 
+apply (simp only: add_le_cancel_left) 
+apply (simp add: ); 
 done
 
 lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)"
diff -r deb8e1e62002 -r 84fda1b39947 src/HOL/Real/RealOrd.thy
--- a/src/HOL/Real/RealOrd.thy	Wed Dec 10 16:47:50 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy	Thu Dec 11 10:52:41 2003 +0100
@@ -423,157 +423,6 @@
 done
 
 
-ML
-{*
-val real_add_cancel_21 = thm "real_add_cancel_21";
-val real_add_cancel_end = thm "real_add_cancel_end";
-val real_add_left_cancel = thm"real_add_left_cancel";
-val real_eq_diff_eq = thm"eq_diff_eq";
-val real_less_eqI = thm"real_less_eqI";
-val real_le_eqI = thm"real_le_eqI";
-val real_eq_eqI = thm"real_eq_eqI";
-val real_add_minus_cancel = thm"real_add_minus_cancel";
-val real_minus_add_cancel = thm"real_minus_add_cancel";
-val real_minus_add_distrib = thm"real_minus_add_distrib";
-
-structure Real_Cancel_Data =
-struct
-  val ss		= HOL_ss
-  val eq_reflection	= eq_reflection
-
-  val sg_ref		= Sign.self_ref (Theory.sign_of (the_context ()))
-  val T			= HOLogic.realT
-  val zero		= Const ("0", T)
-  val restrict_to_left  = restrict_to_left
-  val add_cancel_21	= real_add_cancel_21
-  val add_cancel_end	= real_add_cancel_end
-  val add_left_cancel	= real_add_left_cancel
-  val add_assoc		= real_add_assoc
-  val add_commute	= real_add_commute
-  val add_left_commute	= real_add_left_commute
-  val add_0		= real_add_zero_left
-  val add_0_right	= real_add_zero_right
-
-  val eq_diff_eq	= real_eq_diff_eq
-  val eqI_rules		= [real_less_eqI, real_eq_eqI, real_le_eqI]
-  fun dest_eqI th = 
-      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
-	      (HOLogic.dest_Trueprop (concl_of th)))
-
-  val diff_def		= real_diff_def
-  val minus_add_distrib	= real_minus_add_distrib
-  val minus_minus	= real_minus_minus
-  val minus_0		= real_minus_zero
-  val add_inverses	= [real_add_minus, real_add_minus_left]
-  val cancel_simps	= [real_add_minus_cancel, real_minus_add_cancel]
-end;
-
-structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
-
-Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
-*}
-
-
-subsection{*An Embedding of the Naturals in the Reals*}
-
-lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)"
-by (simp add: real_of_posnat_def pnat_one_iff [symmetric]
-              real_of_preal_def symmetric real_one_def)
-
-lemma real_of_posnat_two: "real_of_posnat (Suc 0) = (1::real) + (1::real)"
-by (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq
-                 real_add
-            prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric]
-            pnat_add_ac)
-
-lemma real_of_posnat_add: 
-     "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)"
-apply (unfold real_of_posnat_def)
-apply (simp (no_asm_use) add: real_of_posnat_one [symmetric] real_of_posnat_def real_of_preal_add [symmetric] preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add)
-done
-
-lemma real_of_posnat_add_one: "real_of_posnat (n + 1) = real_of_posnat n + (1::real)"
-apply (rule_tac x1 = " (1::real) " in real_add_right_cancel [THEN iffD1])
-apply (rule real_of_posnat_add [THEN subst])
-apply (simp (no_asm_use) add: real_of_posnat_two real_add_assoc)
-done
-
-lemma real_of_posnat_Suc: "real_of_posnat (Suc n) = real_of_posnat n + (1::real)"
-by (subst real_of_posnat_add_one [symmetric], simp)
-
-lemma inj_real_of_posnat: "inj(real_of_posnat)"
-apply (rule inj_onI)
-apply (unfold real_of_posnat_def)
-apply (drule inj_real_of_preal [THEN injD])
-apply (drule inj_preal_of_prat [THEN injD])
-apply (drule inj_prat_of_pnat [THEN injD])
-apply (erule inj_pnat_of_nat [THEN injD])
-done
-
-lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
-by (simp add: real_of_nat_def real_of_posnat_one)
-
-lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
-by (simp add: real_of_nat_def real_of_posnat_two real_add_assoc)
-
-lemma real_of_nat_add [simp]: 
-     "real (m + n) = real (m::nat) + real n"
-apply (simp add: real_of_nat_def add_ac)
-apply (simp add: real_of_posnat_add real_add_assoc [symmetric])
-done
-
-(*Not for addsimps: often the LHS is used to represent a positive natural*)
-lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
-by (simp add: real_of_nat_def real_of_posnat_Suc real_add_ac)
-
-lemma real_of_nat_less_iff [iff]: 
-     "(real (n::nat) < real m) = (n < m)"
-by (auto simp add: real_of_nat_def real_of_posnat_def)
-
-lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
-by (simp add: linorder_not_less [symmetric])
-
-lemma inj_real_of_nat: "inj (real :: nat => real)"
-apply (rule inj_onI)
-apply (auto intro!: inj_real_of_posnat [THEN injD]
-            simp add: real_of_nat_def real_add_right_cancel)
-done
-
-lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
-apply (induct_tac "n")
-apply (auto simp add: real_of_nat_Suc)
-apply (drule real_add_le_less_mono)
-apply (rule real_zero_less_one)
-apply (simp add: order_less_imp_le)
-done
-
-lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
-apply (induct_tac "m")
-apply (auto simp add: real_of_nat_Suc real_add_mult_distrib real_add_commute)
-done
-
-lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
-by (auto dest: inj_real_of_nat [THEN injD])
-
-lemma real_of_nat_diff [rule_format]:
-     "n \<le> m --> real (m - n) = real (m::nat) - real n"
-apply (induct_tac "m")
-apply (auto simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc real_of_nat_zero real_add_ac)
-done
-
-lemma real_of_nat_zero_iff: "(real (n::nat) = 0) = (n = 0)"
-  proof 
-    assume "real n = 0"
-    have "real n = real (0::nat)" by simp
-    then show "n = 0" by (simp only: real_of_nat_inject)
-  next
-    show "n = 0 \<Longrightarrow> real n = 0" by simp
-  qed
-
-lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0"
-by (simp add: neg_nat real_of_nat_zero)
-
-
 subsection{*Inverse and Division*}
 
 lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)"
@@ -672,6 +521,110 @@
 done
 
 
+subsection{*An Embedding of the Naturals in the Reals*}
+
+lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)"
+by (simp add: real_of_posnat_def pnat_one_iff [symmetric]
+              real_of_preal_def symmetric real_one_def)
+
+lemma real_of_posnat_two: "real_of_posnat (Suc 0) = (1::real) + (1::real)"
+by (simp add: real_of_posnat_def real_of_preal_def real_one_def pnat_two_eq
+                 real_add
+            prat_of_pnat_add [symmetric] preal_of_prat_add [symmetric]
+            pnat_add_ac)
+
+lemma real_of_posnat_add: 
+     "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + (1::real)"
+apply (unfold real_of_posnat_def)
+apply (simp (no_asm_use) add: real_of_posnat_one [symmetric] real_of_posnat_def real_of_preal_add [symmetric] preal_of_prat_add [symmetric] prat_of_pnat_add [symmetric] pnat_of_nat_add)
+done
+
+lemma real_of_posnat_add_one: "real_of_posnat (n + 1) = real_of_posnat n + (1::real)"
+apply (rule_tac x1 = " (1::real) " in real_add_right_cancel [THEN iffD1])
+apply (rule real_of_posnat_add [THEN subst])
+apply (simp (no_asm_use) add: real_of_posnat_two real_add_assoc)
+done
+
+lemma real_of_posnat_Suc: "real_of_posnat (Suc n) = real_of_posnat n + (1::real)"
+by (subst real_of_posnat_add_one [symmetric], simp)
+
+lemma inj_real_of_posnat: "inj(real_of_posnat)"
+apply (rule inj_onI)
+apply (unfold real_of_posnat_def)
+apply (drule inj_real_of_preal [THEN injD])
+apply (drule inj_preal_of_prat [THEN injD])
+apply (drule inj_prat_of_pnat [THEN injD])
+apply (erule inj_pnat_of_nat [THEN injD])
+done
+
+lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
+by (simp add: real_of_nat_def real_of_posnat_one)
+
+lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
+by (simp add: real_of_nat_def real_of_posnat_two real_add_assoc)
+
+lemma real_of_nat_add [simp]: 
+     "real (m + n) = real (m::nat) + real n"
+apply (simp add: real_of_nat_def add_ac)
+apply (simp add: real_of_posnat_add add_assoc [symmetric])
+apply (simp add: add_commute) 
+apply (simp add: add_assoc [symmetric])
+done
+
+(*Not for addsimps: often the LHS is used to represent a positive natural*)
+lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
+by (simp add: real_of_nat_def real_of_posnat_Suc real_add_ac)
+
+lemma real_of_nat_less_iff [iff]: 
+     "(real (n::nat) < real m) = (n < m)"
+by (auto simp add: real_of_nat_def real_of_posnat_def)
+
+lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
+by (simp add: linorder_not_less [symmetric])
+
+lemma inj_real_of_nat: "inj (real :: nat => real)"
+apply (rule inj_onI)
+apply (auto intro!: inj_real_of_posnat [THEN injD]
+            simp add: real_of_nat_def real_add_right_cancel)
+done
+
+lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
+apply (induct_tac "n")
+apply (auto simp add: real_of_nat_Suc)
+apply (drule real_add_le_less_mono)
+apply (rule real_zero_less_one)
+apply (simp add: order_less_imp_le)
+done
+
+lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
+apply (induct_tac "m")
+apply (auto simp add: real_of_nat_Suc real_add_mult_distrib real_add_commute)
+done
+
+lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
+by (auto dest: inj_real_of_nat [THEN injD])
+
+lemma real_of_nat_diff [rule_format]:
+     "n \<le> m --> real (m - n) = real (m::nat) - real n"
+apply (induct_tac "m")
+apply (simp add: );
+apply (simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc add_ac)
+apply (simp add: add_left_commute [of _ "- 1"]) 
+done
+
+lemma real_of_nat_zero_iff: "(real (n::nat) = 0) = (n = 0)"
+  proof 
+    assume "real n = 0"
+    have "real n = real (0::nat)" by simp
+    then show "n = 0" by (simp only: real_of_nat_inject)
+  next
+    show "n = 0 \<Longrightarrow> real n = 0" by simp
+  qed
+
+lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0"
+by (simp add: neg_nat real_of_nat_zero)
+
+
 subsection{*Results About @{term real_of_posnat}: to be Deleted*}
 
 lemma real_of_posnat_gt_zero: "0 < real_of_posnat n"
@@ -697,7 +650,10 @@
 lemma real_of_posnat_ge_one: "1 <= real_of_posnat n"
 apply (simp (no_asm) add: real_of_posnat_one [symmetric])
 apply (induct_tac "n")
-apply (auto simp add: real_of_posnat_Suc real_of_posnat_one order_less_imp_le)
+apply (simp add: ); 
+apply (simp add: real_of_posnat_Suc real_of_posnat_one order_less_imp_le)
+apply (rule add_le_cancel_right [THEN iffD1, of _ "- 1"]) 
+apply (simp add: add_assoc); 
 done
 declare real_of_posnat_ge_one [simp]
 
@@ -825,9 +781,11 @@
 
 lemma real_of_nat_num_if: "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))"
 apply (case_tac "n")
-apply (auto simp add: real_of_nat_Suc)
+apply (simp add: ); 
+apply (simp add: real_of_nat_Suc add_commute)
 done
 
+
 ML
 {*
 val real_abs_def = thm "real_abs_def";
@@ -949,6 +907,40 @@
 val real_le_square = thm "real_le_square";
 val real_mult_less_mono1 = thm "real_mult_less_mono1";
 val real_mult_less_mono2 = thm "real_mult_less_mono2";
+
+val real_inverse_gt_0 = thm "real_inverse_gt_0";
+val real_inverse_less_0 = thm "real_inverse_less_0";
+val real_mult_less_iff1 = thm "real_mult_less_iff1";
+val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
+val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
+val real_mult_less_mono = thm "real_mult_less_mono";
+val real_mult_less_mono' = thm "real_mult_less_mono'";
+val real_inverse_less_swap = thm "real_inverse_less_swap";
+val real_mult_is_0 = thm "real_mult_is_0";
+val real_inverse_add = thm "real_inverse_add";
+val real_sum_squares_cancel = thm "real_sum_squares_cancel";
+val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";
+val real_0_less_mult_iff = thm "real_0_less_mult_iff";
+val real_0_le_mult_iff = thm "real_0_le_mult_iff";
+val real_mult_less_0_iff = thm "real_mult_less_0_iff";
+val real_mult_le_0_iff = thm "real_mult_le_0_iff";
+
+val INVERSE_ZERO = thm"INVERSE_ZERO";
+val DIVISION_BY_ZERO = thm"DIVISION_BY_ZERO";
+val real_mult_left_cancel = thm"real_mult_left_cancel";
+val real_mult_right_cancel = thm"real_mult_right_cancel";
+val real_mult_left_cancel_ccontr = thm"real_mult_left_cancel_ccontr";
+val real_mult_right_cancel_ccontr = thm"real_mult_right_cancel_ccontr";
+val real_inverse_not_zero = thm"real_inverse_not_zero";
+val real_mult_not_zero = thm"real_mult_not_zero";
+val real_inverse_inverse = thm"real_inverse_inverse";
+val real_inverse_1 = thm"real_inverse_1";
+val real_minus_inverse = thm"real_minus_inverse";
+val real_inverse_distrib = thm"real_inverse_distrib";
+val real_minus_divide_eq = thm"real_minus_divide_eq";
+val real_divide_minus_eq = thm"real_divide_minus_eq";
+val real_add_divide_distrib = thm"real_add_divide_distrib";
+
 val real_of_posnat_one = thm "real_of_posnat_one";
 val real_of_posnat_two = thm "real_of_posnat_two";
 val real_of_posnat_add = thm "real_of_posnat_add";
@@ -968,22 +960,6 @@
 val real_of_nat_diff = thm "real_of_nat_diff";
 val real_of_nat_zero_iff = thm "real_of_nat_zero_iff";
 val real_of_nat_neg_int = thm "real_of_nat_neg_int";
-val real_inverse_gt_0 = thm "real_inverse_gt_0";
-val real_inverse_less_0 = thm "real_inverse_less_0";
-val real_mult_less_iff1 = thm "real_mult_less_iff1";
-val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
-val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
-val real_mult_less_mono = thm "real_mult_less_mono";
-val real_mult_less_mono' = thm "real_mult_less_mono'";
-val real_inverse_less_swap = thm "real_inverse_less_swap";
-val real_mult_is_0 = thm "real_mult_is_0";
-val real_inverse_add = thm "real_inverse_add";
-val real_sum_squares_cancel = thm "real_sum_squares_cancel";
-val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";
-val real_0_less_mult_iff = thm "real_0_less_mult_iff";
-val real_0_le_mult_iff = thm "real_0_le_mult_iff";
-val real_mult_less_0_iff = thm "real_mult_less_0_iff";
-val real_mult_le_0_iff = thm "real_mult_le_0_iff";
 
 val real_of_posnat_gt_zero = thm "real_of_posnat_gt_zero";
 val real_inv_real_of_posnat_gt_zero = thm "real_inv_real_of_posnat_gt_zero";
@@ -1012,21 +988,10 @@
 val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
 val real_of_nat_num_if = thm "real_of_nat_num_if";
 
-val INVERSE_ZERO = thm"INVERSE_ZERO";
-val DIVISION_BY_ZERO = thm"DIVISION_BY_ZERO";
-val real_mult_left_cancel = thm"real_mult_left_cancel";
-val real_mult_right_cancel = thm"real_mult_right_cancel";
-val real_mult_left_cancel_ccontr = thm"real_mult_left_cancel_ccontr";
-val real_mult_right_cancel_ccontr = thm"real_mult_right_cancel_ccontr";
-val real_inverse_not_zero = thm"real_inverse_not_zero";
-val real_mult_not_zero = thm"real_mult_not_zero";
-val real_inverse_inverse = thm"real_inverse_inverse";
-val real_inverse_1 = thm"real_inverse_1";
-val real_minus_inverse = thm"real_minus_inverse";
-val real_inverse_distrib = thm"real_inverse_distrib";
-val real_minus_divide_eq = thm"real_minus_divide_eq";
-val real_divide_minus_eq = thm"real_divide_minus_eq";
-val real_add_divide_distrib = thm"real_add_divide_distrib";
+val real_minus_add_distrib = thm"real_minus_add_distrib";
+val real_add_left_cancel = thm"real_add_left_cancel";
+val real_add_minus_cancel = thm"real_add_minus_cancel";
+val real_minus_add_cancel = thm"real_minus_add_cancel";
 *}
 
 end