--- 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)
--- 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
--- 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
--- 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);
--- 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;
--- 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}
--- 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);
--- 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