# HG changeset patch
# User blanchet
# Date 1265747577 -3600
# Node ID 342888d802d83435dc521ea48a0efba49fd9ad71
# Parent  894e82be8d05ccb8b7390dfa0e967655c1610b7b# Parent  592edca1dfb3015066abdbc3d8fc5f4ff7545a55
merged

diff -r 592edca1dfb3 -r 342888d802d8 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Feb 09 17:06:05 2010 +0100
+++ b/src/HOL/Nat.thy	Tue Feb 09 21:32:57 2010 +0100
@@ -176,7 +176,7 @@
 
 end
 
-hide (open) fact add_0_right
+hide (open) fact add_0 add_0_right diff_0
 
 instantiation nat :: comm_semiring_1_cancel
 begin
@@ -1491,6 +1491,8 @@
 lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
 by (simp split add: nat_diff_split)
 
+hide (open) fact diff_diff_eq
+
 lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
 by (auto split add: nat_diff_split)
 
diff -r 592edca1dfb3 -r 342888d802d8 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Tue Feb 09 17:06:05 2010 +0100
+++ b/src/HOL/Rational.thy	Tue Feb 09 21:32:57 2010 +0100
@@ -1083,14 +1083,6 @@
   finally show ?thesis using assms by simp
 qed
 
-lemma (in linordered_idom) sgn_greater [simp]:
-  "0 < sgn a \<longleftrightarrow> 0 < a"
-  unfolding sgn_if by auto
-
-lemma (in linordered_idom) sgn_less [simp]:
-  "sgn a < 0 \<longleftrightarrow> a < 0"
-  unfolding sgn_if by auto
-
 lemma rat_le_eq_code [code]:
   "Fract a b < Fract c d \<longleftrightarrow> (if b = 0
        then sgn c * sgn d > 0
diff -r 592edca1dfb3 -r 342888d802d8 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Feb 09 17:06:05 2010 +0100
+++ b/src/HOL/Real.thy	Tue Feb 09 21:32:57 2010 +0100
@@ -9,21 +9,18 @@
 proof (rule ccontr)
   assume xy: "\<not> x \<le> y"
   hence "(x-y)/2 > 0"
-    by (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy)
+    by simp
   hence "x \<le> y + (x - y) / 2"
     by (rule e [of "(x-y)/2"])
   also have "... = (x - y + 2*y)/2"
-    by auto
-       (metis add_less_cancel_left add_numeral_0_right class_semiring.add_c xy e
-           diff_add_cancel gt_half_sum less_half_sum linorder_not_le number_of_Pls)
+    by (simp add: diff_divide_distrib)
   also have "... = (x + y) / 2" 
-    by auto
+    by simp
   also have "... < x" using xy 
-    by auto
+    by simp
   finally have "x<x" .
   thus False
-    by auto 
+    by simp
 qed
 
-
 end
diff -r 592edca1dfb3 -r 342888d802d8 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Tue Feb 09 17:06:05 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Tue Feb 09 21:32:57 2010 +0100
@@ -153,7 +153,7 @@
 
     val ctxt = ProofContext.init thy';
 
-    val simpset1 = HOL_basic_ss addsimps @{thm add_0} :: @{thm Nat.add_0_right} ::
+    val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
       size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
     val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
 
diff -r 592edca1dfb3 -r 342888d802d8 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Feb 09 17:06:05 2010 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Feb 09 21:32:57 2010 +0100
@@ -60,7 +60,7 @@
   (Simplifier.rewrite 
     (HOL_basic_ss 
        addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
-             @ [if_False, if_True, @{thm add_0}, @{thm add_Suc},
+             @ [if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc},
                  @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
              @ map (fn th => th RS sym) @{thms numerals}));
 
@@ -634,7 +634,7 @@
 
 val nat_arith = @{thms "nat_arith"};
 val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps})
-                              addsimps [Let_def, if_False, if_True, @{thm add_0}, @{thm add_Suc}];
+                              addsimps [Let_def, if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}];
 
 fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
 
diff -r 592edca1dfb3 -r 342888d802d8 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Tue Feb 09 17:06:05 2010 +0100
+++ b/src/HOL/Tools/nat_arith.ML	Tue Feb 09 21:32:57 2010 +0100
@@ -51,7 +51,7 @@
   val dest_sum = dest_sum;
   val prove_conv = Arith_Data.prove_conv2;
   val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
-    @{thm add_0}, @{thm Nat.add_0_right}];
+    @{thm Nat.add_0}, @{thm Nat.add_0_right}];
   val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
   fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
   fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
diff -r 592edca1dfb3 -r 342888d802d8 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Feb 09 17:06:05 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Feb 09 21:32:57 2010 +0100
@@ -124,7 +124,7 @@
 
 
 (*Simplify 1*n and n*1 to n*)
-val add_0s  = map rename_numerals [@{thm add_0}, @{thm Nat.add_0_right}];
+val add_0s  = map rename_numerals [@{thm Nat.add_0}, @{thm Nat.add_0_right}];
 val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
 
 (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
@@ -136,7 +136,7 @@
 
 val simplify_meta_eq =
     Arith_Data.simplify_meta_eq
-        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm Nat.add_0_right},
+        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right},
           @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
 
 
diff -r 592edca1dfb3 -r 342888d802d8 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Feb 09 17:06:05 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Feb 09 21:32:57 2010 +0100
@@ -373,7 +373,7 @@
     [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq
-    [@{thm add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left},
+    [@{thm Nat.add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left},
       @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
   end